The permutation transport in coordinates

The model permutation map acts on coordinates by the adjacent-word sign and the permutation reindex.

theorem RS.wordPerm_eq_prod {n : ℕ} (w : List (Fin n)) : wordPerm w = (List.map adjTrans w).prod

The word of adjacent transpositions composes to its permutation.

theorem RS.wordPerm_adjWord {n : ℕ} (σ : Equiv.Perm (Fin (n + 1))) : wordPerm (adjWord σ) = σ

The adjacent word composes to its permutation.

theorem RS.coordOf_modelPermMap {k ℓ n : ℕ} (σ : Equiv.Perm (Fin (n + 1))) (v : (superPow (stdSuperPair k ℓ) (n + 1)).even) (c : MixedColouring k ℓ (n + 1)) : coordOf ((modelPermMap σ).evenMap v) c = wordSign (adjWord σ) c * coordOf v (c ∘ ⇑σ)

The permutation transport in coordinates.

theorem RS.coordOf_modelPermMap' {k ℓ n : ℕ} (σ : Equiv.Perm (Fin n)) (v : (superPow (stdSuperPair k ℓ) n).even) (c : MixedColouring k ℓ n) : coordOf ((modelPermMap σ).evenMap v) c = (-1) ^ oddInversions σ c * coordOf v (c ∘ ⇑σ)

The permutation transport in coordinates, arity-uniform form: the sign is the odd-inversion sign, valid at every arity including zero.