The Euclidean descent word of a unimodular 2x2 matrix
Definitionburau_descent_worddescenteuclidean-algorithmmatricessl2z
The Euclidean descent of a unimodular matrix, written as a word in the
generators. Let and
, and for
iterate the Euclidean step , , recording at each
step the factor ; when reaches the two-element terminal word
closes the expansion. The node records that word, BurauDescent.word M, and the
statement proved here is
This is the combinatorial engine behind the descent section of the reduced braid quotient: it turns an arbitrary element of into an explicit product of the two generators, on which the multiplication rules for are checked generator by generator.
Definition code
import Mathlib
set_option autoImplicit false
open Matrix
namespace BurauDescent
abbrev M2 := Matrix (Fin 2) (Fin 2) ℤ
/-- `S = !![0,-1;1,0]`. -/
def Sm : M2 := !![0, -1; 1, 0]
/-- `T^n = !![1,n;0,1]`. -/
def Tm (n : ℤ) : M2 := !![1, n; 0, 1]
/-- `S⁻¹ = S³`. -/
def Sinv : M2 := Sm * Sm * Sm
/-- Generator word for the terminal case `M 0 0 = 0`. -/
noncomputable def baseWord (M : M2) : List M2 :=
if M 0 1 = -1 then [Sm, Tm (M 1 1)] else [Sm, Sm, Sm, Tm (-(M 1 1))]
/-- `k` steps of the Euclidean descent from `M`, followed by the terminal word. -/
noncomputable def iterWord : ℕ → M2 → List M2
| 0, M => baseWord M
| k + 1, M =>
if M 0 0 = 0 then baseWord M
else iterWord k ((M * Tm (-(M 0 1 / M 0 0))) * Sm) ++ [Sinv, Tm (M 0 1 / M 0 0)]
/-- The Euclidean descent word of `M`. -/
noncomputable def word (M : M2) : List M2 := iterWord (M 0 0).natAbs M
end BurauDescent
Source
Euclidean algorithm in SL(2,Z); J. S. Birman, *Braids, Links, and Mapping Class Groups*, Ann. Math. Studies 82 (1974), §3.3.