The group of link-homotopically trivial braids is normal (Proposition 3.6)
ProvedHGL.trivial_braids_normalEvery subgroup of the surface braid group whose membership is link-homotopical triviality is normal: the conjugate of a link-homotopically trivial braid by any braid is again link-homotopically trivial. The group of trivial braids of Proposition 3.6 is therefore a normal subgroup of the surface braid group, and the quotient by it is a group.
import Mathlib import Definitions.Def_HGL_alg import Definitions.Def_HGL_tor
namespace HGL
/-! Milestone 3 (Proposition 3.6): the group H_n(M) of link-homotopically
trivial surface braids is a normal subgroup of the surface braid group
B_n(M). Any subgroup of the braid group whose membership is the triviality
under link homotopy is normal: conjugation of a trivial braid by a braid
remains trivial, because the class map is compatible with the braid group
multiplication. -/
theorem trivial_braids_normal {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) → H.Normal := 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, any subgroup of the braid group whose members are exactly the braids trivial under link homotopy is normal, that is, closed under conjugation by the elements of the braid group. Hypotheses: the world is given; the subgroup is assumed to have triviality as its exact membership criterion; no further hypotheses appear.