The power sums and the permutation characters of Sₙ

Let ψ^ν be the character of the Young permutation module M^ν, the permutation representation of Sₙ on the ν-tabloids. These characters are the coefficients of the power-sum product p_ρ of a partition ρ of n in the monomial symmetric polynomials m_ν,

p_ρ = ∑_{ν ⊢ n} ψ^ν(ρ) m_ν,

where ψ^ν(ρ) is the value of ψ^ν at any permutation of cycle type ρ. Equivalently, the coefficient of x^d in p_ρ, when d.degree = n, is the number of tabloids fixed by such a permutation, for the shape obtained by sorting the exponents of x^d.

The proof reads both sides as counts of invariant colourings. A ν-tabloid is a colouring of Fin n by the rows of ν (TauCeti.quotientFiberSubgroupEquiv, applied to the row map TauCeti.youngBlock ν), and it is fixed by π exactly when the colouring is constant on the cycles of π; on the other side, the coefficient of x^d in p_ρ counts the colourings constant on the cycles of π with d i points of colour i (TauCeti.coeff_psumPart_partition). Writing the rows of ν as letters of the alphabet puts the two counts side by side at the sorted monomial of ν, and the symmetry of p_ρ moves any other monomial of degree n there (TauCeti.coeff_eq_coeff_partWeight).

Combined with Young's rule, ψ^ν = ∑_λ K_{λν} χ^λ (TauCeti.char_permutationModule_eq_sum_kostkaNumber_mul_spechtChar), and the monomial expansion of the Schur polynomials s_λ = ∑_ν K_{λν} m_ν (TauCeti.schurPoly_eq_sum_kostkaNumber_smul_msymm), this expansion is Frobenius's formula p_ρ = ∑_λ χ^λ(ρ) s_λ for the irreducible characters.

Summing the power sums against a permutation character instead gives n! times a product of complete homogeneous symmetric polynomials: ∑_π ψ^ν(π) p_{ρ(π)} = n! h_ν. Read at the sorted monomial of a second partition ξ, this computes ∑_π ψ^ν(π) ψ^ξ(π) through the coefficients of h_ν, which is how Young's rule is proved.

Main results

• TauCeti.coeff_partWeight_psumPart_partition: the coefficient of the power-sum product over the cycle type of π at the sorted monomial of ν counts the ν-tabloids fixed by π.
• TauCeti.coeff_psumPart_eq_card_fixedPoints: the coefficient of p_ρ at any monomial of degree n counts the tabloids fixed by a permutation of cycle type ρ, for the shape of the monomial.
• TauCeti.psumPart_eq_sum_card_fixedPoints_smul_msymm: the monomial expansion of p_ρ, with the fixed-tabloid counts as coefficients.
• TauCeti.psumPart_eq_sum_character_smul_msymm: the same expansion over ℚ, with the characters of the Young permutation modules as coefficients.
• TauCeti.sum_card_fixedPoints_smul_psumPart_partition: ∑_π ψ^ν(π) • p_{ρ(π)} = n! • h_ν, the power-sum form of the statement that the Frobenius characteristic of ψ^ν is h_ν.

References

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

The rows of a partition as letters

theorem TauCeti.psumPart_eq_psumPart_partition {σ : Type u_1} [Fintype σ] (R : Type u_2) [CommSemiring R] {n : ℕ} {ρ : n.Partition} {π : Equiv.Perm (Fin n)} (hπ : ConjClasses.mk π = (partitionEquivConjClasses n) ρ) : MvPolynomial.psumPart σ R ρ = MvPolynomial.psumPart σ R π.partition

The power-sum product of the partition indexing the class of π is the power-sum product over the cycle type of π: both take one power sum per cycle.

The coefficients of a power-sum product

theorem TauCeti.coeff_partWeight_psumPart_partition {σ : Type u_1} [Fintype σ] (R : Type u_2) [CommSemiring R] {n : ℕ} (π : Equiv.Perm (Fin n)) (ν : n.Partition) (hν : ν.parts.card ≤ Fintype.card σ) : (MvPolynomial.psumPart σ R π.partition).coeff (partWeight σ ν) = ↑(Nat.card { q : Equiv.Perm (Fin n) ⧸ youngSubgroup ν // π • q = q })

The coefficient of p_ρ at the sorted monomial of ν counts the ν-tabloids fixed by a permutation π of cycle type ρ. Here ρ is the cycle type of π, fixed points included, and the alphabet has at least as many letters as ν has parts.

theorem TauCeti.sum_card_fixedPoints_smul_psumPart_partition {σ : Type u_1} [Fintype σ] (R : Type u_2) [CommSemiring R] {n : ℕ} [DecidableEq σ] (ν : n.Partition) : ∑ π : Equiv.Perm (Fin n), Nat.card { q : Equiv.Perm (Fin n) ⧸ youngSubgroup ν // π • q = q } • MvPolynomial.psumPart σ R π.partition = n.factorial • MvPolynomial.hsymmPart σ R ν

The permutation character of M^ν against the power sums is n! • h_ν: ∑_π ψ^ν(π) • p_{ρ(π)} = n! • h_ν, where ψ^ν(π) is the number of ν-tabloids fixed by π and h_ν = h_{ν₁} ⋯ h_{ν_k}. Dividing by n!, this says that the Frobenius characteristic of the permutation character ψ^ν is h_ν. It is TauCeti.sum_card_smul_psumPart_partition for the colouring of Fin n by the rows of ν.

@[instance_reducible]

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

Local decidable equality for alphabet-indexed monomials.

Equations

• TauCeti.instDecidableEqPermutationModuleColour = Classical.decEq σ

theorem TauCeti.coeff_psumPart_eq_card_fixedPoints {σ : Type u_1} [Fintype σ] (R : Type u_2) [CommSemiring R] {n : ℕ} {ρ : n.Partition} {π : Equiv.Perm (Fin n)} (hπ : ConjClasses.mk π = (partitionEquivConjClasses n) ρ) {d : σ →₀ ℕ} (h : Finsupp.degree d = n) : (MvPolynomial.psumPart σ R ρ).coeff d = ↑(Nat.card { q : Equiv.Perm (Fin n) ⧸ youngSubgroup (weightPartition d h) // π • q = q })

The coefficient of p_ρ at a monomial of degree n counts fixed tabloids: at x^d it is the number of tabloids fixed by a permutation π of cycle type ρ, for the shape obtained by sorting the exponents of x^d. That count is the value at π of the permutation character of the corresponding Young permutation module (TauCeti.char_permutationModule).

The monomial expansion

theorem TauCeti.psumPart_eq_sum_card_fixedPoints_smul_msymm {σ : Type u_1} [Fintype σ] (R : Type u_2) [CommSemiring R] {n : ℕ} {ρ : n.Partition} {π : Equiv.Perm (Fin n)} (hπ : ConjClasses.mk π = (partitionEquivConjClasses n) ρ) : MvPolynomial.psumPart σ R ρ = ∑ ν : n.Partition, ↑(Nat.card { q : Equiv.Perm (Fin n) ⧸ youngSubgroup ν // π • q = q }) • MvPolynomial.msymm σ R ν

The monomial expansion of a power-sum product: p_ρ = ∑_{ν ⊢ n} ψ^ν(π) m_ν for any permutation π of cycle type ρ, where ψ^ν(π) is the number of ν-tabloids fixed by π. The sum runs over every partition of n: those with more parts than the alphabet has letters contribute nothing, their monomial symmetric polynomial vanishing there.

theorem TauCeti.psumPart_eq_sum_character_smul_msymm {σ : Type u_1} [Fintype σ] {n : ℕ} {ρ : n.Partition} {π : Equiv.Perm (Fin n)} (hπ : ConjClasses.mk π = (partitionEquivConjClasses n) ρ) : MvPolynomial.psumPart σ ℚ ρ = ∑ ν : n.Partition, (permutationModule ν).ρ.character π • MvPolynomial.msymm σ ℚ ν

The monomial expansion of a power-sum product in terms of permutation characters: p_ρ = ∑_{ν ⊢ n} ψ^ν(π) m_ν over ℚ, where ψ^ν is the character of the Young permutation module M^ν and π is any permutation of cycle type ρ.