Normal closure of a central element is its cyclic subgroup

Proved

BurauFaithful.normalClosure_singleton_center

by lt9 · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

braid-groupsburaumodular-group

Normal closure of a central element. Let $G$ be a group and $g\in G$ an element of its centre. Then the normal closure of $\{g\}$ is nothing but the cyclic subgroup generated by $g$ :

\bigl\langle\!\langle g\rangle\!\bigr\rangle \;=\; \langle g\rangle .

Indeed every conjugate $y\,g\,y^{-1}$ of a central element equals $g$ , so the normal closure adds nothing to the cyclic subgroup; conversely $\langle g\rangle\subseteq\langle\!\langle g\rangle\!\rangle$ always.

This is the last step of the assembly in the proof of faithfulness of the Burau representation for three strands: once a braid $\beta$ is known to lie in the normal closure of $\Delta^4=(\sigma_1\sigma_2)^6$ — which is what the injectivity of the specialization at $t=-1$ gives — the present lemma turns that into an explicit statement $\beta=(\sigma_1\sigma_2)^{6k}$ , because $\Delta^4$ is central in $B_3$ (the full twist squared $\Delta^2=(\sigma_1\sigma_2)^3$ generates the centre; the Garside identity gives $\Delta^4=(\sigma_1\sigma_2)^6$ ).

Formalization Note The proof avoids closure-inclusion lemmas entirely: membership in the cyclic subgroup is rewritten by Subgroup.mem_closure_singleton as x = g ^ n, centrality of the power comes from Subgroup.zpow_mem (Subgroup.center G), and both inclusions are then produced with Subgroup.normalClosure_le_normal (with a local normality instance for the cyclic subgroup) and Subgroup.mem_closure_singleton.mpr.

Preamble

/-
`BurauFaithful.normalClosure_singleton_center`: for a **central** element, its normal closure is just
the cyclic subgroup it generates.

This is the last step of the assembly in NOTES_BURAU.md (SESSION 14/15): from the injectivity of
`B_3/⟨Δ⁴⟩ → SL(2,ℤ)` one learns that `β` lies in the normal closure of `Δ⁴ = (σ₀σ₁)⁶`; since
`Δ⁴ = (Δ²)²` is central (Proved: `BurauFaithful.braid_three_fullTwist_central` for `Δ²`, plus the
Garside identity `BurauFaithful.braid_three_garside_pow`), that normal closure is the cyclic
subgroup `⟨Δ⁴⟩`, which is exactly the conclusion `∃ k, β = (σ₀σ₁)^{6k}` of
`BurauFaithful.spec_reduced_kernel_le`.

The proof avoids every closure-inclusion lemma: membership in `closure {g}` is rewritten with
`Subgroup.mem_closure_singleton` as `x = g ^ n`, and membership is then produced by
`Subgroup.zpow_mem` from the centrality of `g` (`Subgroup.mem_center_iff`). Verified names in this
Mathlib: `Subgroup.mem_closure_singleton` (`Algebra/Group/Subgroup/Lattice.lean:468`),
`Subgroup.zpow_mem (H) (hx) (n)`, `Subgroup.mem_center_iff` (`GroupTheory/Subgroup/Center.lean:58`),
`Subgroup.normalClosure_le_normal` (`GroupTheory/Subgroup/Basic.lean:646`).
-/
import Definitions.Def_BurauFaithful_UnreducedBurau

set_option autoImplicit false

Formal statement

theorem BurauFaithful.normalClosure_singleton_center (G : Type*) [Group G] (g : G) (hg : g ∈ Subgroup.center G) :
    Subgroup.normalClosure ({g} : Set G) = Subgroup.closure ({g} : Set G) := by sorry

Source

J. S. Birman, *Braids, Links, and Mapping Class Groups*, Ann. of Math. Studies 82, Princeton Univ. Press, 1974, §3.3, pp. 129-130.

View graph