The descended loop-reading homomorphism is surjective (Lemma 2.14)
ProvedESL.theta_hat_surjectiveEvery descent of the loop-reading homomorphism to the link-homotopy quotient is surjective: every element of the target group is the loop tuple of some pure braid of the surface, and every class is the class of some pure braid, so every element of the target is the image of some class under the descended map. This is the surjectivity part of Lemma 2.14.
import Mathlib import Definitions.Def_ESL_alg import Definitions.Def_ESL_tor
namespace ESL
/-! Milestone 2 (Lemma 2.14): the induced homomorphism theta-hat from the
link-homotopy classes of pure braids on the surface to the n-fold product
of the fundamental group is surjective. Every element of the product is
the image of a pure braid, and the quotient map is surjective, so the
descent is surjective as well. -/
theorem theta_hat_surjective {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) →
∀ y : Pi, ∃ c : HhatM, thetahat c = y := 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, any homomorphism from the link-homotopy quotient of the surface pure braid group to the target group that commutes with the quotient map as the loop-reading homomorphism does hits every element of the target group. Hypotheses: the world is given; the homomorphism is assumed to satisfy the descent commutation; no further hypotheses appear.