The kernel generator $\Delta^4=(\sigma_1\sigma_2)^6$ is central in $

Proved

BurauFaithful.braid_three_garside_sixth_central

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

braid-groupsburaumodular-group

The kernel generator $\Delta^4=(\sigma_1\sigma_2)^6$ is central in $B_3$ . The full twist $\Delta^2=(\sigma_1\sigma_2)^3$ of the three-strand braid group is central (this is the Garside element squared; it is the Proved statement that $\Delta^2$ lies in $Z(B_3)$ ), and the centre of a group is a subgroup, hence closed under powers. Therefore

(\sigma_1\sigma_2)^6=\bigl((\sigma_1\sigma_2)^3\bigr)^2\in Z(B_3).

This is the B $_3$ -side input of the assembly proving that the kernel of the specialization at $t=-1$ of the reduced Burau representation is generated by $\Delta^4$ : the remaining step uses the general fact that the normal closure of a central element is just the cyclic subgroup it generates, so a braid lying in the normal closure of $(\sigma_1\sigma_2)^6$ is equal to a power $(\sigma_1\sigma_2)^{6k}$ — precisely the conclusion required for faithfulness of the Burau representation of $B_3$ (Birman, Braids, Links, and Mapping Class Groups, Ann. of Math. Studies 82, §3.3, pp. 129–130; W. Magnus and A. Peluso, On a theorem of V. I. Arnol'd, Comm. Pure Appl. Math. 22 (1969)).

Formalization Note The statement is obtained from the published Proved theorem for $\Delta^2$ by Subgroup.pow_mem on the centre together with the arithmetic identity $(g^3)^2=g^6$ .

Preamble

/-
`BurauFaithful.braid_three_garside_sixth_central`: the kernel generator `(σ₀σ₁)⁶ = Δ⁴` is central
in `B₃`.

This is the B₃-side input of the assembly in NOTES_BURAU.md (SESSION 14/15): the conclusion of
`BurauFaithful.spec_reduced_kernel_le` is `∃ k, β = (σ₀σ₁)^{6k}`, obtained by applying the general
lemma `BurauFaithful.normalClosure_singleton_center` (normal closure of a *central* element = its
cyclic subgroup) to `g = (σ₀σ₁)⁶`.

Immediate from the Proved platform node `BurauFaithful.braid_three_fullTwist_central`
(`(σ₀σ₁)³` is central): the centre is a subgroup, hence closed under squares, and
`((σ₀σ₁)³)² = (σ₀σ₁)⁶`.
-/
import Definitions.Def_BraidsLinksMCG_ArtinBraidGroup
import Theorems.Thm_BurauFaithful_braid_three_fullTwist_central

set_option autoImplicit false

Formal statement

theorem BurauFaithful.braid_three_garside_sixth_central :
    (BraidsLinksMCG.sigma (n := 3) ⟨0, by decide⟩ *
        BraidsLinksMCG.sigma (n := 3) ⟨1, by decide⟩) ^ 6 ∈
      Subgroup.center (BraidsLinksMCG.ArtinBraidGroup 3) := 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

The kernel generator Δ4=(σ1σ2)6\Delta^4=(\sigma_1\sigma_2)^6Δ4=(σ1​σ2​)6 is central in $

The kernel generator $\Delta^4=(\sigma_1\sigma_2)^6$ is central in $