Adjacent-transposition words for permutations of Fin n

Every permutation of Fin n is a product of adjacent transpositions. We construct this factorisation explicitly as a list of positions (an "adjacent-transposition word") and prove it correct.

Strategy

We use mathlib's Equiv.Perm.decomposeFin, which decomposes σ : Perm (Fin (n+1)) into a pair (p, σ') with σ = swap 0 p * extPerm σ' where extPerm σ' is the permutation of Fin (n+1) that fixes 0 and acts as σ' on successors.

We then express swap 0 p as adjacent transpositions by the conjugation identity swap 0 (k+2) = swap 0 (k+1) * swap (k+1) (k+2) * swap 0 (k+1), and lift the recursive word for σ' by mapping positions through Fin.succ.

def RS.adjTrans {n : ℕ} (i : Fin n) : Equiv.Perm (Fin (n + 1))

The adjacent transposition at position i: swaps i and i + 1.

Equations

• RS.adjTrans i = Equiv.swap i.castSucc i.succ

theorem RS.perm_fin_one (σ : Equiv.Perm (Fin 1)) : σ = 1

Permutations of Fin 0 and Fin 1 are trivial.

The 0-fixing extension

Adjacent-transposition word for swap 0 p

def RS.swap0WordAux (n k : ℕ) : k ≤ n → List (Fin n)

Auxiliary: adjacent-transposition word for swap 0 ⟨k, _⟩ in Perm (Fin (n+1)). Recursion on k:

• k = 0: identity, word = []
• k+1: swap0WordAux k ++ [k] ++ swap0WordAux k (conjugation: swap 0 (k+1) = swap 0 k * swap k (k+1) * swap 0 k)

Equations

• RS.swap0WordAux n 0 x_2 = []
• RS.swap0WordAux n k.succ hk = RS.swap0WordAux n k ⋯ ++ [⟨k, ⋯⟩] ++ RS.swap0WordAux n k ⋯

def RS.swap0Word {n : ℕ} (p : Fin (n + 1)) : List (Fin n)

Adjacent-transposition word for swap 0 p.

Equations

• RS.swap0Word p = RS.swap0WordAux n ↑p ⋯

The factorisation

The main construction

noncomputable def RS.adjWord {n : ℕ} (σ : Equiv.Perm (Fin (n + 1))) : List (Fin n)

An adjacent-transposition word for a permutation.

Equations

• RS.adjWord x = []
• RS.adjWord σ_2 = match Equiv.Perm.decomposeFin σ_2 with | (p, σ') => RS.swap0Word p ++ List.map Fin.succ (RS.adjWord σ')

theorem RS.adjWord_spec {n : ℕ} (σ : Equiv.Perm (Fin (n + 1))) : (List.map adjTrans (adjWord σ)).prod = σ

The word composes to the permutation.