The kernel of the descended loop-reading map lies in the normal closure of the disk classes (Lemma 3.4)
ProvedESL.kernel_in_closureThe kernel of the descended loop-reading map is contained in the normal closure of the image of the descended inclusion: a class killed by the descended map is represented by a pure braid whose loop tuple is trivial, and by Goldberg's kernel characterization such a braid is a product of conjugates of images of disk braids; pushing this expression through the descent squares exhibits the class inside the normal closure. This is Lemma 3.4 of the paper.
import Mathlib import Definitions.Def_ESL_alg import Definitions.Def_ESL_tor
namespace ESL
/-! Milestone 6 (Lemma 3.4): the kernel of theta-hat is contained in the
normal closure of the image of f-hat. A class killed by theta-hat is
represented by a pure braid whose theta_n image is trivial; by Goldberg's
theorem such a braid lies in the normal closure of the image of f_n, and
passing to the quotient exhibits the class in the normal closure of the
image of f-hat. -/
theorem kernel_in_closure {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) →
MonoidHom.ker thetahat ≤ Subgroup.normalClosure (Set.range fhat) := 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 class killed by the latter lies in the normal closure of the set of images of classes under the former. Hypotheses: the world is given; the two homomorphisms are assumed to satisfy their descent commutations; no further hypotheses appear.