Coxeter relation (T S)^3 = S^2 in the reduced braid group

Proved

burau_liftU_cube

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

braid-groupscoxeterpresentationsl2z

Coxeter relation $(\mathrm{liftT}\cdot\mathrm{liftS})^3=\mathrm{liftS}^2$ . With $\mathrm{liftS}=\overline{\sigma_0^2\sigma_1}$ and $\mathrm{liftT}=\overline{\sigma_0^{-1}}$ the images of the standard generators $S,T$ of $\mathrm{SL}(2,\mathbb Z)$ ,

(\mathrm{liftT}\cdot \mathrm{liftS})^3 = \mathrm{liftS}^2 ,

which is the image of the dictionary identity $\mathrm{uLift}^3=\mathrm{sLift}^2$ for the elements $\sigma_0\sigma_1$ and the half twist. Together with $\mathrm{liftS}^4=1$ this is the Coxeter presentation of the quotient.

Preamble

import Definitions.Def_burau_reduced_braid_group
import Definitions.Def_BurauFaithful_UnreducedBurau
import Theorems.Thm_BurauFaithful_braid_three_amalgam_dictionary

set_option autoImplicit false

Formal statement

theorem burau_liftU_cube :
    (BurauNC.liftT * BurauNC.liftS) ^ 3 = BurauNC.liftS ^ 2 := by sorry

Source

C. Moser, H. S. M. Coxeter, *Generators and relations for discrete groups* (1964), Ch. 3.

View graph