Word sign depends only on the word's permutation

We show that wordSign w c depends on w only through wordPerm w, by identifying it as (-1) ^ oddInversions (wordPerm w) c, where oddInversions σ c counts inversions of σ at odd-coloured positions.

def RS.oddInversions {k ℓ n : ℕ} (σ : Equiv.Perm (Fin n)) (c : MixedColouring k ℓ n) : ℕ

Count of inversions of σ restricted to odd-coloured positions: pairs (a, b) with a < b, σ a > σ b, and both c (σ a) and c (σ b) odd-coloured.

Equations

• RS.oddInversions σ c = {p : Fin n × Fin n | p.1 < p.2 ∧ σ p.1 > σ p.2 ∧ (c (σ p.1)).isRight = true ∧ (c (σ p.2)).isRight = true}.card

theorem RS.wordSign_eq_oddInversions {k ℓ n : ℕ} (w : List (Fin n)) (c : MixedColouring k ℓ (n + 1)) : wordSign w c = (-1) ^ oddInversions (wordPerm w) c

The word sign is an inversion count: it is (−1) to the number of inversions of the word's permutation at odd positions.