The orbit factorization of a fixed-colouring sum

For a permutation π of Fin n, the sum of colouring weights over the colourings fixed by π factorizes over the orbit space: each orbit is coloured uniformly, contributing a power sum in its size.

noncomputable def RS.cycleProd (t : ℕ → ℂ) {n : ℕ} (π : Equiv.Perm (Fin n)) : ℂ

The completed cycle-type product of a prospective power-sum sequence: the product over the full cycle type, fixed points included.

Equations

• RS.cycleProd t π = (Multiset.map t π.cycleType).prod * t 1 ^ (n - π.cycleType.sum)

theorem RS.sum_fixedFun_eq_prod_orbits {n N : ℕ} (x : Fin N → ℂ) (π : Equiv.Perm (Fin n)) : ∑ f : { f : Fin n → Fin N // f ∘ ⇑π = f }, ∏ i : Fin n, x (↑f i) = ∏ O : OrbitSpace π, pVal x (orbCard π O)

The orbit factorization: the fixed-colouring weight sum of a permutation is the product of the power sums of its orbit sizes.