Prove2Me

The full twist (σ1σ2)3(\sigma_1\sigma_2)^3 lies in the centre of B3B_3

Proved
BurauFaithful.braid_three_fullTwist_central

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

braid-groupsgroup-theory

This states that the full twist lies in the centre of the three-strand braid group, in the form needed for the first step of Birman's proof of Theorem 3.15 (J. S. Birman, Braids, Links, and Mapping Class Groups, Annals of Mathematics Studies 82, §3.3, pp. 129-130).

Let

B3=⟨σ1,σ2  ∣  σ1σ2σ1=σ2σ1σ2⟩B_3 = \bigl\langle \sigma_1,\sigma_2 \;\bigm|\; \sigma_1\sigma_2\sigma_1 = \sigma_2\sigma_1\sigma_2 \bigr\rangle

and let Δ=σ1σ2σ1\Delta = \sigma_1\sigma_2\sigma_1 be the Garside element, so that Δ2=(σ1σ2)3\Delta^2 = (\sigma_1\sigma_2)^3 is the full twist. The theorem states

(σ1σ2)3∈Z(B3).(\sigma_1\sigma_2)^3 \in Z(B_3).

The full twist generates the centre of B3B_3; this is why the kernel of the specialization of the Burau representation at t=−1t=-1, which is generated by Δ4\Delta^4, is a cyclic subgroup of the centre, and why faithfulness can be decided by checking the centre alone.

Formalization Note Subgroup.center is the centre of the group and BraidsLinksMCG.ArtinBraidGroup 3 is the presented group with generators BraidsLinksMCG.sigma 0, BraidsLinksMCG.sigma 1; the proof uses the braid relation together with the fact that these two generators generate the group.

Preamble
import Definitions.Def_BraidsLinksMCG_ArtinBraidGroup

set_option autoImplicit false
Formal statement
theorem BurauFaithful.braid_three_fullTwist_central :
    (BraidsLinksMCG.sigma (n := 3) ⟨0, by decide⟩ *
        BraidsLinksMCG.sigma (n := 3) ⟨1, by decide⟩) ^ 3 ∈
      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, Chapter 1 (the full twist and the centre of the braid group) and §3.3, Theorem 3.15, pp. 129-130; cf. Kassel-Turaev, *Braid Groups*, GTM 247, Chapter 2.

View graph