Extension commutes with an adjacent colour swap

Extending a mixed colouring by one slot and swapping two adjacent colours are independent operations when the swapped pair lies below the new slot: the swap acts on the tail, the extension prepends, and the two commute on the nose (colourExtend_colourSwap).

The proof is the corresponding statement for the adjacency sign (adjSign_eq_tail) carried through the word and its permutation.

Computation lemmas for colourPowerStep applied at a point

How evenSplitEquiv interacts with swaps

Analogous lemmas for oddSplitEquiv

Main theorem

theorem RS.colourExtend_colourSwap {k ℓ : ℕ} (n i : ℕ) (h : i + 2 ≤ n + 1) : colourExtend (n + 1) (colourSwap k ℓ (n + 1) i h) = colourSwap k ℓ (n + 2) i ⋯

Extension compatibility of the signed swap: extending the adjacent Koszul swap by one position is the adjacent Koszul swap of the extended power.