Specht multiplicities in Young permutation modules

For a Young diagram lam and a partition μ of its number of cells, the multiplicity of the Specht representation S^lam in the Young permutation module M^μ is the dimension of the intertwiner space

Hom_{Sₙ}(S^lam, M^μ).

This file defines that number as TauCeti.spechtMultiplicity lam μ and proves the unitriangular part of Young's rule:

• it vanishes unless the shape of lam dominates μ;
• it is one when μ is the shape of lam.

These results describe the diagonal and the zero region of the Kostka multiplicity matrix. In particular, they supply the unitriangular part of the multiplicity statement in Young's rule.

Main definitions

• TauCeti.spechtMultiplicity: the multiplicity of S^lam in M^μ.
• TauCeti.spechtSelfMultiplicityEquiv: the canonical equivalence ℚ ≃ₗ[ℚ] Hom_{Sₙ}(S^lam, M^lam) given by scalar multiples of the inclusion.

Main results

• TauCeti.spechtMultiplicity_eq_zero_of_not_dominates: the multiplicity vanishes outside the dominance cone.
• TauCeti.dominates_of_spechtMultiplicity_ne_zero: a nonzero multiplicity forces dominance.
• TauCeti.spechtMultiplicity_self: the diagonal multiplicity is one.

References

• G. D. James, The Representation Theory of the Symmetric Groups, Chapters 4 and 13.
• B. E. Sagan, The Symmetric Group, 2nd ed. (2001), Section 2.11.

noncomputable def TauCeti.spechtMultiplicity (lam : YoungDiagram) (μ : lam.card.Partition) : ℕ

The multiplicity of S^lam in the Young permutation module M^μ: the dimension of the space of equivariant linear maps from the Specht representation of lam to M^μ.

Over ℚ, the group algebra of the symmetric group is semisimple and the rational Specht modules are absolutely irreducible, so this intertwiner dimension is the number of copies of S^lam in M^μ. Young's rule identifies it with the Kostka number of the same two shapes.

Equations

• TauCeti.spechtMultiplicity lam μ = Module.finrank ℚ ((TauCeti.spechtSubrepresentation lam).toRepresentation.IntertwiningMap (TauCeti.permutationModule μ).ρ)

theorem TauCeti.spechtMultiplicity_def (lam : YoungDiagram) (μ : lam.card.Partition) : spechtMultiplicity lam μ = Module.finrank ℚ ((spechtSubrepresentation lam).toRepresentation.IntertwiningMap (permutationModule μ).ρ)

The Specht multiplicity is the dimension of the corresponding intertwiner space.

@[simp]

theorem TauCeti.spechtMultiplicity_eq_zero_of_not_dominates {lam : YoungDiagram} (μ : lam.card.Partition) (h : ¬Dominates (shapePartition lam) μ) : spechtMultiplicity lam μ = 0

The Specht multiplicity vanishes outside the dominance cone. This is the zero region of the unitriangular multiplicity matrix in Young's rule.

theorem TauCeti.dominates_of_spechtMultiplicity_ne_zero {lam : YoungDiagram} (μ : lam.card.Partition) (h : spechtMultiplicity lam μ ≠ 0) : Dominates (shapePartition lam) μ

A nonzero Specht multiplicity forces dominance.

The diagonal intertwiner space

noncomputable def TauCeti.spechtSelfMultiplicityEquiv (lam : YoungDiagram) : ℚ ≃ₗ[ℚ] (spechtSubrepresentation lam).toRepresentation.IntertwiningMap (permutationModule (shapePartition lam)).ρ

The diagonal intertwiner space is one-dimensional. The equivalence sends a scalar κ to κ times the canonical inclusion S^lam ↪ M^lam.

Equations

• TauCeti.spechtSelfMultiplicityEquiv lam = LinearEquiv.ofBijective (TauCeti.scalarToSpechtIntertwiningMap✝ lam) ⋯

@[simp]

theorem TauCeti.spechtSelfMultiplicityEquiv_apply (lam : YoungDiagram) (κ : ℚ) : (spechtSelfMultiplicityEquiv lam) κ = κ • (spechtSubrepresentation lam).subtype

The diagonal equivalence sends κ to κ times the inclusion.

@[simp]

theorem TauCeti.spechtMultiplicity_self (lam : YoungDiagram) : spechtMultiplicity lam (shapePartition lam) = 1

The diagonal Specht multiplicity is one. There is exactly one copy of S^lam in M^lam: every equivariant map S^lam → M^lam is a scalar multiple of the inclusion.