The image of the disk classes lies in the kernel of the descended loop-reading map (Lemma 3.3)
ProvedESL.image_in_kernelThe image of the descended inclusion lies in the kernel of the descended loop-reading map: the loop tuple of the image of a disk braid is trivial, by Goldberg's theorem on the disk, so the descended loop-reading map kills every class in the image of the descended inclusion. This is Lemma 3.3 of the paper, the right-exactness ingredient of Theorem 3.1.
import Mathlib import Definitions.Def_ESL_alg import Definitions.Def_ESL_tor
namespace ESL
/-! Milestone 5 (Lemma 3.3): the image of f-hat lies in the kernel of
theta-hat. The square commutes with theta_n by Goldberg's theorem used in
the proof: theta_n (f_n x) = 1 for every pure braid x of the disk, so
theta-hat kills every class in the image of f-hat. -/
theorem image_in_kernel {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)) →
∀ thetahat : HhatM →* Pi, (∀ x : PB_M, thetahat (W.qM x) = W.theta x) →
∀ y : HhatM, (∃ x : HhatD, fhat x = y) → thetahat y = 1 := 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, for any descended inclusion of the disk classes and any descended loop-reading map, every element of the image of the former is carried to the identity by the latter. Hypotheses: the world is given; the two homomorphisms are assumed to satisfy their descent commutations; no further hypotheses appear.