The colour action of the model braidings

Assembling the three conjugation laws: the adjacent model braiding acts on the colouring model as the Koszul-signed adjacent swap, positionwise and wordwise.

theorem RS.toColour_powBraid {k ℓ : ℕ} (n i : ℕ) (h : i + 2 ≤ n) : toColour n (powBraid (stdSuperPair k ℓ) n i h) = colourSwap k ℓ n i h

The colour action: conjugating the adjacent braiding into the colouring model is the Koszul-signed adjacent swap.

theorem RS.toColour_powBraidWord {k ℓ n : ℕ} (w : List (Fin n)) : toColour (n + 1) (powBraidWord (stdSuperPair k ℓ) w) = colourSwapWord k ℓ w

The wordwise colour action.