The descended inclusion of the disk classes is injective, by Goldsmith (Lemma 3.2)
ProvedESL.f_hat_injectiveThe descended inclusion of the disk classes is injective: if two link-homotopy classes of pure braids of the disk have the same image on the surface, they are equal. Indeed, a class mapped to the trivial class is represented by a pure braid whose image on the surface is link-homotopically trivial; by the disk-triviality theorem of Goldsmith the braid itself is link-homotopically trivial on the disk, so its class is trivial. This is Lemma 3.2 of the paper.
import Mathlib import Definitions.Def_ESL_alg import Definitions.Def_ESL_tor
namespace ESL
/-! Milestone 4 (Lemma 3.2): the induced homomorphism f-hat is injective.
A pure braid of the disk whose class maps to the trivial class on the
surface has its image in the trivial subgroup of the surface, so the
Goldsmith disk-triviality property forces the braid itself to be trivial on
the disk, and its class is trivial. -/
theorem f_hat_injective {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) :
∀ fhat : HhatD →* HhatM, (∀ x : PB_D, fhat (W.qD x) = W.qM (W.f x)) →
∀ y z : HhatD, fhat y = fhat z → y = z := 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 disk quotient to the surface quotient commuting with the inclusion-induced map sends two classes with the same image to equal classes - formally, whenever the images of two classes coincide, the classes coincide. Hypotheses: the world is given; the homomorphism is assumed to satisfy the descent commutation; no further hypotheses appear.