The kernel of a realization is normal in the total-space subgroup (Proposition 2.1 and Lemma 2.2)
ProvedCTB.kernel_normalThe kernel of a torus-bundle realization is normal in the total-space subgroup. If the pair of subgroups with the homomorphism realizes the abstract model group, and the total-space subgroup is torsion-free, then the kernel is stable under conjugation by the elements of the total-space subgroup, so the quotient is a group and the realization fits into the short exact sequence of the fibration. This is the idealized form of the normality step shared by Proposition 2.1 and Lemma 2.2 of the paper.
import Mathlib import Definitions.Def_CTB_alg import Definitions.Def_CTB_tor
namespace CTB
/-! Milestone 2 (Proposition 2.1 and Lemma 2.2, idealized): the kernel
of a torus-bundle realization is normal in the total-space subgroup.
If the pair of subgroups with the homomorphism f realizes the abstract
model group, and the total-space subgroup is torsion-free, then the
kernel is stable under conjugation by the elements of the total-space
subgroup, so that the quotient is a group and the realization fits into
the short exact sequence of the fibration. -/
theorem kernel_normal {n : ℕ} {Q : Type*} [Group Q] {G : Type*} [Group G]
(W : CrystallographicBraidWorld n Q)
(Gam Ker : Subgroup Q) (f : Q →* G)
(h : IsTorusBundleRealization W Gam Ker f) (hT : TorsionFree ↥Gam) :
∀ g ∈ Gam, ∀ k ∈ Ker, g * k * g⁻¹ ∈ Ker := by sorry
end CTB
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: in a crystallographic braid world, for a pair of subgroups and a homomorphism realizing a model group, if the total-space subgroup is torsion-free, then the conjugate of every element of the kernel by every element of the total-space subgroup lies in the kernel. Hypotheses: the world is given; the pair realizes the model group; the total-space subgroup is torsion-free; no further hypotheses appear.