The loop-reading homomorphism descends to the link-homotopy quotient (Lemma 2.14)
ProvedESL.theta_hat_welldefinedThe homomorphism that reads off the loops traced by the strands of a pure braid of the surface descends to the link-homotopy quotient: there is an induced homomorphism from the quotient group of link-homotopy classes to the target group, carrying the class of a pure braid to the loop tuple of the braid itself. The descent is possible because the link-homotopically trivial braids are killed by the loop-reading homomorphism. This is the well-definedness part of Lemma 2.14.
import Mathlib import Definitions.Def_ESL_alg import Definitions.Def_ESL_tor
namespace ESL
/-! Milestone 1: the homomorphism theta_n descends to the
link-homotopy quotient of the pure braid group of the surface. Since the
trivial subgroup is contained in the kernel of theta_n, there is an induced
homomorphism theta-hat carrying the class of a pure braid to its theta_n
image. This is the well-definedness part of Lemma 2.14 of the source
paper. -/
theorem theta_hat_welldefined {n : ℕ} {PB_D PB_M HhatD HhatM Pi : Type*}
[Group PB_D] [Group PB_M] [Group HhatD] [Group HhatM] [Group Pi]
(W : StringLinkExactWorld n PB_D PB_M HhatD HhatM Pi) :
∃ thetahat : HhatM →* Pi, ∀ x : PB_M, thetahat (W.qM x) = W.theta x := by sorry
end ESL
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: in the world of the exact sequence, there exists a homomorphism from the link-homotopy quotient of the pure braid group of the surface to the target group such that the image of the class of a pure braid equals the image of the braid under the loop-reading homomorphism. Hypotheses: the world is given; no further hypotheses appear.