The T-rule for the Euclidean descent section

Proved

burau_rho_T

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

braid-groupscontinued-fractionsdescent-sectionsl2z

The $T$ -rule for the descent section. For every unimodular $2\times2$ integer matrix $M$ and every integer $j$ ,

\rho\bigl(M\cdot T^j\bigr) = \rho(M)\cdot \mathrm{liftT}^{\,j},

where $T^j=\left(\begin{smallmatrix}1&j\\0&1\end{smallmatrix}\right)$ and $\mathrm{liftT}=\overline{\sigma_0^{-1}}$ is the image of the standard generator $T$ of $\mathrm{SL}(2,\mathbb Z)$ in the reduced braid quotient $Q=B_3/\langle\!\langle\Delta^4\rangle\!\rangle$ . This is one of the two multiplication rules that turn the Euclidean descent section into a group-theoretic section of $q:B_3\to Q$ ; the companion $S$ -rule $\rho(M\cdot S)=\rho(M)\cdot\mathrm{liftS}$ is the continued-fraction identity isolated by this project.

Preamble

import Definitions.Def_burau_cf_list
import Definitions.Def_burau_rho
import Definitions.Def_burau_reduced_braid_group

set_option autoImplicit false

Formal statement

theorem burau_rho_T (M : BurauNC.M2) (j : ℤ) (hd : M.det = 1) :
    BurauNC.rho (M * BurauNC.Tm j) = BurauNC.rho M * BurauNC.liftT ^ j := by sorry

Source

Euclidean algorithm in SL(2,Z) and the reduced Burau representation; cf. C. Moser, H. S. M. Coxeter, *Generators and relations for discrete groups* (1964), Ch. 3; J. S. Birman, *Braids, Links, and Mapping Class Groups*, Ann. of Math. Studies 82 (1974), §3.3.

View graph