The total colouring coordinates

Combining the even and odd coordinate functions identifies the total tensor space with all functions on colour words. The model permutation acts there by reindexing and its odd-inversion sign.

def RS.colourSplit (k ℓ n : ℕ) : (MixedColouring k ℓ n → ℂ) ≃ₗ[ℂ] Tot (colourPower k ℓ n)

Splitting a colour function into its even and odd restrictions.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.colourTotalEquiv (k ℓ n : ℕ) : Tot (superPow (stdSuperPair k ℓ) n) ≃ₗ[ℂ] MixedColouring k ℓ n → ℂ

The total tensor space in coordinates indexed by all colour words.

Equations

• RS.colourTotalEquiv k ℓ n = (RS.colourPowerEquiv k ℓ n).evenEquiv.prodCongr (RS.colourPowerEquiv k ℓ n).oddEquiv ≪≫ₗ (RS.colourSplit k ℓ n).symm

theorem RS.colourTotalEquiv_modelPermMap {k ℓ n : ℕ} (σ : Equiv.Perm (Fin n)) (v : MixedColouring k ℓ n → ℂ) (c : MixedColouring k ℓ n) : (colourTotalEquiv k ℓ n) ((tot (modelPermMap σ)) ((colourTotalEquiv k ℓ n).symm v)) c = (-1) ^ oddInversions σ c * v (c ∘ ⇑σ)

The total model action has the Koszul monomial coordinates at every arity, including arity zero.