The normal closure of the disk classes lies in the kernel of the descended loop-reading map (Lemma 3.3, closure form)

Proved

ESL.closure_in_kernel

by Lucas · Oct 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

kernelslink-homotopynormal-closure

The normal closure of the image of the descended inclusion is contained in the kernel of the descended loop-reading map: since the descended loop-reading map is a homomorphism killing every element of the image of the descended inclusion, it kills the entire normal closure generated by that image. This closes the exactness from the other side, complementing Lemma 3.4 with the normal-closure transport of Lemma 3.3.

Preamble

import Mathlib
import Definitions.Def_ESL_alg
import Definitions.Def_ESL_tor

Formal statement

namespace ESL

/-!  Milestone 7: the normal closure of the image of f-hat is contained in
the kernel of theta-hat. Since the image of f-hat consists of classes and
theta-hat is a homomorphism killing them by Lemma 3.3, the normal closure
of the image is killed as well. -/
theorem closure_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) →
        Subgroup.normalClosure (Set.range fhat) ≤ MonoidHom.ker thetahat := by sorry

end ESL

Source

J. R. T. Theodoro de Lima, An exact sequence for generalized string links over surfaces, LAJM - Latin-American Journal of Mathematics 2 (2023) no. 1, Section 3 (Lemma 3.3, transported to the normal closure).

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, the normal closure of the image of the former is contained in the kernel of the latter. Hypotheses: the world is given; the two homomorphisms are assumed to satisfy their descent commutations; no further hypotheses appear.

View graph