The colour-side braiding word

The word of signed adjacent swaps on the colouring model, with its evaluation: acting on a coordinate function reindexes the colouring along the word's permutation and multiplies by the word's Koszul sign, computed stepwise along the colouring's own trajectory.

noncomputable def RS.colourSwapWord (k ℓ : ℕ) {n : ℕ} : List (Fin n) → (colourPower k ℓ (n + 1) ⟶ colourPower k ℓ (n + 1))

The colour-side braiding word.

Equations

• RS.colourSwapWord k ℓ [] = CategoryTheory.CategoryStruct.id (RS.colourPower k ℓ (n + 1))
• RS.colourSwapWord k ℓ (i :: w) = CategoryTheory.CategoryStruct.comp (RS.colourSwapWord k ℓ w) (RS.colourSwap k ℓ (n + 1) ↑i ⋯)

def RS.wordSign {k ℓ n : ℕ} : List (Fin n) → MixedColouring k ℓ (n + 1) → ℂ

The Koszul sign of a word along a colouring's trajectory: each step contributes the adjacent sign at the colouring reached so far.

Equations

• RS.wordSign [] x✝ = 1
• RS.wordSign (i :: w) x✝ = RS.adjSign x✝ ⟨↑i, ⋯⟩ ⟨↑i + 1, ⋯⟩ * RS.wordSign w (x✝ ∘ ⇑(Equiv.swap ⟨↑i, ⋯⟩ ⟨↑i + 1, ⋯⟩))

def RS.wordPerm {n : ℕ} : List (Fin n) → Equiv.Perm (Fin (n + 1))

The permutation of a word of adjacent swaps.

Equations

• RS.wordPerm [] = 1
• RS.wordPerm (i :: w) = Equiv.swap ⟨↑i, ⋯⟩ ⟨↑i + 1, ⋯⟩ * RS.wordPerm w

theorem RS.colourSwapWord_evenMap {k ℓ n : ℕ} (w : List (Fin n)) (F : (colourPower k ℓ (n + 1)).even) (c : { c : MixedColouring k ℓ (n + 1) // c.IsEven }) : (colourSwapWord k ℓ w).evenMap F c = wordSign w ↑c * F ⟨↑c ∘ ⇑(wordPerm w), ⋯⟩

The word evaluation: the colour word acts on even coordinate functions by the word sign and the word reindex.

theorem RS.colourSwapWord_oddMap {k ℓ n : ℕ} (w : List (Fin n)) (F : (colourPower k ℓ (n + 1)).odd) (c : { c : MixedColouring k ℓ (n + 1) // ¬c.IsEven }) : (colourSwapWord k ℓ w).oddMap F c = wordSign w ↑c * F ⟨↑c ∘ ⇑(wordPerm w), ⋯⟩

The word evaluation on odd coordinate functions uses the same word sign and permutation of positions.