The link-homotopy classes of generalized string links form a group (Theorem 3.7)
ProvedHGL.class_groupgroup-structurelink-homotopystring-links
The link-homotopy classes of generalized string links form a group under concatenation. Every class contains a generalized string link, and the class of the mirror of any representative is the group inverse of its class: the class of the concatenation of a link with its mirror is the identity. This is the group structure of the class group of Theorem 3.7, the group denoted B-hat of the paper.
Preamble
import Mathlib import Definitions.Def_HGL_alg import Definitions.Def_HGL_tor
Formal statement
namespace HGL
/-! Milestone 4 (Theorem 3.7, group structure): the link-homotopy classes
of generalized string links form a group under concatenation. Every class
is represented by a generalized string link, and the class of its mirror
is the group inverse of its class: the mirror of the concatenation with
itself is link-homotopic to the identity. -/
theorem class_group {n g : ℕ} {B S Cl : Type*} [Group B] [Monoid S] [Group Cl]
(W : LinkHomotopyWorld n g B S Cl) :
∀ c : Cl, ∃ s : S, W.cls s = c ∧ c⁻¹ = W.cls (W.mirror s) := by sorry
end HGL
Source
J. R. T. Theodoro de Lima, Homotopy of braids on surfaces: extending Goldsmith's answer to Artin, Journal of Knot Theory and Its Ramifications 28 (2019) 1950013, arXiv:1811.02006, Section 3 (Theorem 3.7, the group structure).
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: in a link-homotopy world, every element of the class group is the class of some generalized string link, and for every representative the class of its mirror equals the inverse of its class. Hypotheses: the world is given; no further hypotheses appear.