Garside identity: $\Delta^4 = (\sigma_1\sigma_2)^6$ in $B_3$

Proved

BurauFaithful.braid_three_garside_pow

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

braid-groupsgroup-theory

This is the classical Garside identity for the three-strand braid group, in the form needed to identify the Coxeter relation of the homogeneous modular group with the kernel generator of the specialization of the Burau representation at $t=-1$ (J. S. Birman, Braids, Links, and Mapping Class Groups, Annals of Mathematics Studies 82, §3.3, Theorem 3.15, pp. 129-130).

Let

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 $\Delta = \sigma_1\sigma_2\sigma_1$ be the Garside element. The theorem states

\Delta^4 = (\sigma_1\sigma_2)^6 .

Equivalently, $\Delta^2 = (\sigma_1\sigma_2)^3$ : the square of the Garside element is the full twist, which generates the centre of $B_3$ and acts on homology as multiplication by a scalar. The Coxeter relation $(s_1s_2s_1)^4 = 1$ of the homogeneous modular group $M_2 = \mathrm{SL}(2,\mathbb{Z})$ therefore corresponds, under $\sigma_i\mapsto s_i$ , to the relation $\Delta^4 = 1$ . This is exactly the relation that the Burau matrices satisfy after evaluation at $t=-1$ , and it is why the kernel of that specialization is the cyclic subgroup generated by $(\sigma_1\sigma_2)^6$ .

Formalization Note The group is BraidsLinksMCG.ArtinBraidGroup 3, the quotient of the free group on Fin 2 by the relation set BraidsLinksMCG.braidRels 3; the proof derives the braid relation as an equation between generators from the presentation and then performs the group computation $\Delta^2=(\sigma_1\sigma_2)^3$ .

Preamble

import Definitions.Def_BraidsLinksMCG_ArtinBraidGroup

set_option autoImplicit false

Formal statement

theorem BurauFaithful.braid_three_garside_pow :
    (BraidsLinksMCG.sigma (n := 3) ⟨0, by decide⟩ * BraidsLinksMCG.sigma (n := 3) ⟨1, by decide⟩ *
        BraidsLinksMCG.sigma (n := 3) ⟨0, by decide⟩) ^ 4 =
      (BraidsLinksMCG.sigma (n := 3) ⟨0, by decide⟩ *
        BraidsLinksMCG.sigma (n := 3) ⟨1, by decide⟩) ^ 6 := by sorry

Source

J. S. Birman, *Braids, Links, and Mapping Class Groups*, Ann. of Math. Studies 82, Princeton Univ. Press, 1974, Chapter 3, §3.3, Theorem 3.15, pp. 129-130 (generators and relations of the homogeneous modular group); the full-twist identity Delta^2 = (sigma_1 sigma_2)^3 is classical, cf. Birman, Chapter 1, and Kassel-Turaev, *Braid Groups*, GTM 247, Chapter 2.

View graph

Garside identity: Δ4=(σ1σ2)6\Delta^4 = (\sigma_1\sigma_2)^6Δ4=(σ1​σ2​)6 in B3B_3B3​

Garside identity: $\Delta^4 = (\sigma_1\sigma_2)^6$ in $B_3$