The Euclidean descent word multiplies back to the matrix
Provedburau_sl2_descent_worddescenteuclidean-algorithmsl2z
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.
Preamble
import Definitions.Def_burau_descent_word set_option autoImplicit false
Formal statement
theorem burau_sl2_descent_word (M : BurauDescent.M2) (hd : M.det = 1) :
(BurauDescent.word M).prod = M := by sorry
Source
Euclidean algorithm in SL(2,Z); J. S. Birman, *Braids, Links, and Mapping Class Groups*, Ann. Math. Studies 82 (1974), §3.3.