Young's rule

The Young permutation module M^ν of a partition ν of n, the permutation representation of Sₙ on the ν-tabloids, decomposes into Specht modules according to the Kostka numbers: the multiplicity of S^λ in M^ν is the number K_{λν} of semistandard tableaux of shape λ and content ν. This is Young's rule, proved here in three equivalent forms:

• TauCeti.spechtMultiplicity_eq_kostkaNumber: the dimension of the space of intertwiners from S^λ to M^ν, TauCeti.spechtMultiplicity, is K_{λν};
• TauCeti.sum_spechtChar_mul_char_permutationModule: the character pairing of χ^λ with the permutation character ψ^ν of M^ν is K_{λν};
• TauCeti.char_permutationModule_eq_sum_kostkaNumber_mul_spechtChar: ψ^ν = ∑_λ K_{λν} χ^λ.

The argument

Write m_{λν} = ⟨χ^λ, ψ^ν⟩ for the multiplicities. Both matrices m and K are unitriangular for the dominance order: K_{λν} vanishes unless λ dominates ν and K_{νν} = 1 (TauCeti.kostkaNumber_eq_zero_of_not_dominates, TauCeti.kostkaNumber_self), and the same holds for m (TauCeti.spechtMultiplicity_eq_zero_of_not_dominates, TauCeti.spechtMultiplicity_self). They also have the same Gram matrix. Expanding ψ^ν and ψ^ξ in the Specht characters (TauCeti.eq_sum_spechtChar) gives ∑_λ m_{λν} m_{λξ} = ⟨ψ^ν, ψ^ξ⟩. On the other side, ∑_π ψ^ν(π) p_{ρ(π)} = n! h_ν (TauCeti.sum_card_fixedPoints_smul_psumPart_partition), whose coefficient at the monomial of ξ is n! ⟨ψ^ν, ψ^ξ⟩ on the left and, by h_ν = ∑_μ K_{μν} s_μ, n! ∑_μ K_{μν} K_{μξ} on the right (TauCeti.sum_char_permutationModule_mul_char_permutationModule). A unitriangular matrix is determined by its Gram matrix (TauCeti.eq_of_transpose_mul_self_eq), so m = K.

Main results

• TauCeti.sum_char_permutationModule_mul_char_permutationModule: ∑_π ψ^ν(π) ψ^ξ(π) is n! ∑_μ K_{μν} K_{μξ}.
• TauCeti.sum_spechtChar_shapePartition_mul_char_permutationModule: the pairing of the Specht character of a diagram with a permutation character is the Specht multiplicity.
• TauCeti.sum_spechtChar_mul_char_permutationModule: ⟨χ^λ, ψ^ν⟩ = K_{λν}.
• TauCeti.spechtMultiplicity_eq_kostkaNumber: Young's rule, the Specht multiplicity in a Young permutation module is a Kostka number.
• TauCeti.char_permutationModule_eq_sum_kostkaNumber_mul_spechtChar: ψ^ν = ∑_λ K_{λν} χ^λ.

References

• G. D. James, The Representation Theory of the Symmetric Groups, Chapter 14.
• I. G. Macdonald, Symmetric Functions and Hall Polynomials, Chapter I, Sections 6 and 7.
• B. E. Sagan, The Symmetric Group, 2nd ed. (2001), Section 2.11.

theorem TauCeti.sum_char_permutationModule_mul_char_permutationModule {n : ℕ} (ν ξ : n.Partition) : ∑ π : Equiv.Perm (Fin n), (permutationModule ν).ρ.character π * (permutationModule ξ).ρ.character π = ↑n.factorial * ∑ μ : n.Partition, ↑(kostkaNumber μ ν) * ↑(kostkaNumber μ ξ)

The inner product of two permutation characters: ∑_π ψ^ν(π) ψ^ξ(π) = n! ∑_μ K_{μν} K_{μξ}. Both sides are the coefficient of the monomial of ξ in ∑_π ψ^ν(π) p_{ρ(π)} = n! h_ν, read on the left through the monomial expansion of the power sums and on the right through the Schur expansion h_ν = ∑_μ K_{μν} s_μ.

theorem TauCeti.sum_spechtChar_shapePartition_mul_char_permutationModule (D : YoungDiagram) (μ : D.card.Partition) : ∑ π : Equiv.Perm (Fin D.card), ↑(spechtChar (shapePartition D) π) * (permutationModule μ).ρ.character π = ↑D.card.factorial * ↑(spechtMultiplicity D μ)

The pairing of a Specht character with a permutation character is the Specht multiplicity: for a Young diagram D and a partition μ of its size, ∑_π χ^{D}(π) ψ^μ(π) = |D|! · m, where m = TauCeti.spechtMultiplicity D μ is the dimension of the space of intertwiners from the Specht module of D to M^μ.

theorem TauCeti.sum_spechtChar_mul_char_permutationModule {n : ℕ} (l ν : n.Partition) : ∑ π : Equiv.Perm (Fin n), ↑(spechtChar l π) * (permutationModule ν).ρ.character π = ↑n.factorial * ↑(kostkaNumber l ν)

Young's rule, as a character pairing: ∑_π χ^λ(π) ψ^ν(π) = n! K_{λν}, that is, the multiplicity ⟨χ^λ, ψ^ν⟩ of the Specht character χ^λ in the permutation character ψ^ν of M^ν is the Kostka number K_{λν}.

theorem TauCeti.spechtMultiplicity_eq_kostkaNumber (lam : YoungDiagram) (μ : lam.card.Partition) : spechtMultiplicity lam μ = kostkaNumber (shapePartition lam) μ

Young's rule: the multiplicity of the Specht module S^λ in the Young permutation module M^μ, the dimension of the space of intertwiners TauCeti.spechtMultiplicity λ μ, is the Kostka number K_{λμ}, the number of semistandard tableaux of shape λ and content μ.

theorem TauCeti.char_permutationModule_eq_sum_kostkaNumber_mul_spechtChar {n : ℕ} (ν : n.Partition) (σ : Equiv.Perm (Fin n)) : (permutationModule ν).ρ.character σ = ∑ l : n.Partition, ↑(kostkaNumber l ν) * ↑(spechtChar l σ)

Young's rule, on characters: the permutation character of M^ν is ψ^ν = ∑_λ K_{λν} χ^λ.