The specialized reduced Burau generators $A,B$ generate $\mathrm{SL}(2,\mathbb Z)$

Proved

BurauFaithful.spec_reduced_generators_top

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

braid-groupsgroup-theorymodular-group

The two integral matrices that are the images of $\sigma_1,\sigma_2$ under the specialization at $t=-1$ of the 2-dimensional reduced Burau representation generate the homogeneous modular group $M_2=\mathrm{SL}(2,\mathbb Z)$ :

A=\begin{pmatrix}1&-1\\0&1\end{pmatrix},\qquad B=\begin{pmatrix}2&-1\\1&0\end{pmatrix},\qquad \langle A,B\rangle = M_2 .

This is the surjectivity half of the classical identification of $B_3/\langle\Delta^4\rangle$ with the modular group used by Birman in the proof of Theorem 3.15 (J. S. Birman, Braids, Links, and Mapping Class Groups, Ann. of Math. Studies 82, §3.3, pp. 129-130).

How it is proved. Mathlib's SpecialLinearGroup.SL2Z_generators states that the two classical matrices

S=\begin{pmatrix}0&-1\\1&0\end{pmatrix},\qquad T=\begin{pmatrix}1&1\\0&1\end{pmatrix}

generate SL(2, ℤ). One checks by a finite computation over the integers that $T = A^{-1}$ and $S = A^2 B$ ; hence $S$ and $T$ lie in the subgroup generated by $A$ and $B$ , so that subgroup is everything.

Formalization Note SL(2, ℤ) is written Matrix.SpecialLinearGroup (Fin 2) ℤ; the generators are the subtype elements with entries displayed as matrix literals.

Preamble

import Definitions.Def_BurauFaithful_UnreducedBurau

set_option autoImplicit false

Formal statement

theorem BurauFaithful.spec_reduced_generators_top :
    Subgroup.closure
      ({⟨!![1, -1; 0, 1], by decide⟩, ⟨!![2, -1; 1, 0], by decide⟩} :
        Set (Matrix.SpecialLinearGroup (Fin 2) ℤ)) = ⊤ := by sorry

Source

C. Moser, H. S. M. Coxeter, *Generators and relations for discrete groups*, 2nd ed., Springer 1964, p. 85 (S and T generate the homogeneous modular group); J. S. Birman, *Braids, Links, and Mapping Class Groups*, Ann. of Math. Studies 82, Princeton Univ. Press, 1974, §3.3, Theorem 3.15, pp. 129-130.

View graph

The specialized reduced Burau generators A,BA,BA,B generate SL(2,Z)\mathrm{SL}(2,\mathbb Z)SL(2,Z)

The specialized reduced Burau generators $A,B$ generate $\mathrm{SL}(2,\mathbb Z)$