Power sums over the cycle type of a permutation

Let π be a permutation of a finite set α, with cycle lengths ρ₁, ρ₂, … (fixed points counted as cycles of length one), and let p_ρ = ∏ᵢ p_{ρᵢ} be the corresponding product of power sums in the variables x_i, i ∈ σ. Expanding the product chooses one variable for each cycle of π, that is, a colouring f : α → σ constant on the cycles of π:

p_ρ = ∑_{f : α → σ, f ∘ π = f} ∏_{a ∈ α} x_{f a}.

So the coefficient of x^d in p_ρ is the number of π-invariant colourings of α using each colour i exactly d i times. This is the combinatorial half of the Frobenius formula for the permutation characters of the symmetric group: an invariant colouring with prescribed colour multiplicities is a tabloid fixed by π, so these coefficients are the values of the permutation characters of the Young permutation modules.

Main results

• TauCeti.psumPart_isSymmetric and TauCeti.isHomogeneous_psumPart: a product of power sums over a partition of n is symmetric and homogeneous of degree n.
• TauCeti.psumPart_partition_eq_sum_prod_X: the power-sum product over the cycle type of π is the generating function of the π-invariant colourings.
• TauCeti.coeff_psumPart_partition: its coefficient at x^d counts the π-invariant colourings with d i points of each colour i.
• TauCeti.sum_card_smul_psumPart_partition: averaged over Equiv.Perm α against the number of invariant colourings with fiber sizes r, the power-sum products give (card α)! • ∏ᵢ h_{r i}.

References

• I. G. Macdonald, Symmetric Functions and Hall Polynomials, Chapter I, Section 7.
• R. P. Stanley, Enumerative Combinatorics, Vol. 2, Proposition 7.7.1 and Section 7.18.

theorem TauCeti.psumPart_isSymmetric {σ : Type u_1} (R : Type u_2) [CommSemiring R] [Fintype σ] {n : ℕ} (μ : n.Partition) : (MvPolynomial.psumPart σ R μ).IsSymmetric

A product of power sums is a symmetric polynomial, each factor being symmetric.

theorem TauCeti.isHomogeneous_psum {σ : Type u_1} (R : Type u_2) [CommSemiring R] [Fintype σ] (k : ℕ) : (MvPolynomial.psum σ R k).IsHomogeneous k

The power sum p_k = ∑ᵢ xᵢ ^ k is homogeneous of degree k.

theorem TauCeti.isHomogeneous_psumPart {σ : Type u_1} (R : Type u_2) [CommSemiring R] [Fintype σ] {n : ℕ} (μ : n.Partition) : (MvPolynomial.psumPart σ R μ).IsHomogeneous n

A product of power sums is homogeneous, of degree the number its partition partitions.

@[instance_reducible]

noncomputable def TauCeti.instDecidableEqPowerSumColour {σ : Type u_1} : DecidableEq σ

Local decidable equality for colourings in the power-sum expansion.

Equations

• TauCeti.instDecidableEqPowerSumColour = Classical.decEq σ

theorem TauCeti.psumPart_partition_eq_sum_prod_X {σ : Type u_1} (R : Type u_2) [CommSemiring R] {α : Type u_3} [Fintype α] [DecidableEq α] [Fintype σ] (π : Equiv.Perm α) : MvPolynomial.psumPart σ R π.partition = ∑ f : α → σ with f ∘ ⇑π = f, ∏ a : α, MvPolynomial.X (f a)

The power-sum product over the cycle type of π is the generating function of the π-invariant colourings: p_ρ = ∑_{f ∘ π = f} ∏_a x_{f a}, where ρ is the cycle type of π with its fixed points counted as parts equal to one.

theorem TauCeti.coeff_psumPart_partition {σ : Type u_1} (R : Type u_2) [CommSemiring R] {α : Type u_3} [Fintype α] [DecidableEq α] [Fintype σ] (π : Equiv.Perm α) (d : σ →₀ ℕ) : (MvPolynomial.psumPart σ R π.partition).coeff d = ↑{f : α → σ | f ∘ ⇑π = f ∧ ∀ (i : σ), {a : α | f a = i}.card = d i}.card

The coefficients of the power-sum product over the cycle type of π count invariant colourings: the coefficient of x^d is the number of colourings f : α → σ fixed by π that use each colour i exactly d i times.

Averaging over the symmetric group

theorem TauCeti.sum_card_smul_psumPart_partition {σ : Type u_1} (R : Type u_2) [CommSemiring R] {α : Type u_3} [Fintype α] [DecidableEq α] [Fintype σ] [DecidableEq σ] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (r : ι → ℕ) (hr : ∑ i : ι, r i = Fintype.card α) : ∑ π : Equiv.Perm α, {c : α → ι | c ∘ ⇑π = c ∧ ∀ (i : ι), {a : α | c a = i}.card = r i}.card • MvPolynomial.psumPart σ R π.partition = (Fintype.card α).factorial • ∏ i : ι, MvPolynomial.hsymm σ R (r i)

Averaging power sums against invariant colourings gives complete homogeneous polynomials: for r : ι → ℕ with total card α,

∑_π #{c : α → ι | c ∘ π = c, c has fibers of sizes r} • p_{ρ(π)} = (card α)! • ∏ᵢ h_{r i}.

The count on the left is the value at π of the permutation character on the colourings with fiber sizes r, so this is the statement that the Frobenius characteristic of that permutation representation is the product ∏ᵢ h_{r i}. Both sides expand over colourings of α by pairs ι × σ: the left side counts each pair colouring once for every permutation preserving it, and TauCeti.sum_natCard_fiberSubgroup_smul evaluates that count.