The class group is the braid group modulo the trivial braids (Theorem 3.7)
ProvedHGL.quotient_isoThe class group is isomorphic to the quotient of the surface braid group by the normal subgroup of link-homotopically trivial braids. The composite of the inclusion of the braid group into the monoid of generalized string links with the class map is a homomorphism onto the class group - surjective because every generalized string link is link-homotopic to a braid, by Theorem 3.5 - and its kernel is exactly the subgroup of link-homotopically trivial braids. This identifies the abstract class group with the concrete quotient of Theorem 3.7.
import Mathlib import Definitions.Def_HGL_alg import Definitions.Def_HGL_tor
namespace HGL
/-! Milestone 5 (Theorem 3.7, isomorphism): the group of link-homotopy
classes of generalized string links is isomorphic to the quotient of the
braid group by the normal subgroup of link-homotopically trivial braids.
The inclusion of the braid group followed by the class map is a surjective
homomorphism - by Theorem 3.5 every generalized string link is
link-homotopic to a braid - whose kernel is exactly the subgroup of trivial
braids. -/
theorem quotient_iso {n g : ℕ} {B S Cl : Type*} [Group B] [Monoid S] [Group Cl]
(W : LinkHomotopyWorld n g B S Cl) :
∃ e : B →* Cl, (∀ b : B, e b = W.cls (W.incl b)) ∧
(∀ c : Cl, ∃ b : B, e b = c) ∧
(∀ b : B, e b = 1 ↔ 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 is a homomorphism from the braid group to the class group that maps each braid to the class of its image under the inclusion, that hits every class, and whose kernel is exactly the set of braids whose images are link-homotopic to the identity. Hypotheses: the world is given; no further hypotheses appear.