The S-rule from the L-rule

Open

burau_rho_mul_Sm_of_L_rule

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

descent-sections-rulesl2z

The milestone's $S$ -rule follows from the $L$ -rule. If the descent section $\rho$ is multiplicative against $L^k$ for every unimodular $X$ and every $k$ , then it is multiplicative against $S$ : $\rho(M\,S)=\rho(M)\,\mathrm{liftS}$ for every unimodular $M$ . The descent relation $M S = N\,L^{-e}$ turns the $S$ -rule at $M$ into the $L$ -rule at the successor $N$ with $e=M_{01}/M_{00}$ .

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_mul_Sm_of_L_rule
    (hL : ∀ X : BurauNC.M2, X.det = 1 → ∀ k : ℤ,
      BurauNC.rho (X * BurauNC.Lm k) =
        BurauNC.rho X * BurauNC.liftS⁻¹ * BurauNC.liftT ^ (-k) * BurauNC.liftS) :
    ∀ M : BurauNC.M2, M.det = 1 →
      BurauNC.rho (M * BurauNC.Sm) = BurauNC.rho M * BurauNC.liftS := 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