One descent step of the section rho

Open

burau_rho_eq_rho_step

by lt9 · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

descent-sections-rulesl2z

One step of the Euclidean descent for the section $\rho$ . If $M_{00}\neq0$ then

\rho(M)=\rho\bigl((M\,T^{-n})S\bigr)\,\mathrm{liftS}^{-1}\,\mathrm{liftT}^{n},\qquad n=M_{01}/M_{00}.

This is the recursion the section is defined by, isolated as a reusable rewrite.

Preamble

import Definitions.Def_burau_cf_list
import Definitions.Def_burau_rho
import Definitions.Def_burau_srule_defs
import Definitions.Def_burau_srule_defs2
import Theorems.Thm_burau_rho_T
import Theorems.Thm_burau_liftS_conj_zpow
import Theorems.Thm_burau_rho_mul_Sm_terminal

set_option autoImplicit false

open BurauNC

Formal statement

theorem burau_rho_eq_rho_step (M : BurauNC.M2) (h0 : M 0 0 ≠ 0) :
    BurauNC.rho M =
      BurauNC.rho ((M * BurauNC.Tm (-(M 0 1 / M 0 0))) * BurauNC.Sm) *
        BurauNC.liftS⁻¹ * BurauNC.liftT ^ (M 0 1 / M 0 0) := 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.

View graph