The link-homotopically trivial braids form a subgroup (Proposition 3.6)
ProvedHGL.trivial_braids_subgroupThe link-homotopically trivial braids form a subgroup of the surface braid group: there is a subgroup whose members are exactly the braids whose images under the inclusion are link-homotopic to the identity. Closure under multiplication follows from the congruence of the link-homotopy relation - the product of two trivial braids is trivial - and closure under inverses from the mirror operation, since the concatenation of a braid with its mirror is link-homotopic to the identity.
import Mathlib import Definitions.Def_HGL_alg import Definitions.Def_HGL_tor
namespace HGL
/-! Milestone 2: the link-homotopically trivial braids form a subgroup of
the braid group. The set of braids whose images under the inclusion are
equivalent to the identity under the link-homotopy closure is closed under
multiplication and inverses, using the congruence of Milestone 1 and the
mirror operation. -/
theorem trivial_braids_subgroup {n g : ℕ} {B S Cl : Type*} [Group B] [Monoid S] [Group Cl]
(W : LinkHomotopyWorld n g B S Cl) :
∃ H : Subgroup B, ∀ b : B, b ∈ H ↔ EqvGen W.moves (W.incl b) 1 := by sorry
end HGL
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: in a link-homotopy world, there exists a subgroup of the braid group such that a braid is a member exactly when its image under the inclusion is link-homotopic to the identity of the monoid of generalized string links. Hypotheses: the world is given; no further hypotheses appear.