Distinctness of Specht modules

The rational Specht modules of two partitions of the same integer are isomorphic only when their shapes agree. This is the irredundancy half of the classification of the irreducible representations of the symmetric group.

References

• G. D. James, The Representation Theory of the Symmetric Groups, Chapter 4.
• B. E. Sagan, The Symmetric Group, 2nd ed. (2001), Section 2.4.
• Schur--Weyl roadmap, Layer 4, "Distinctness and completeness".

@[simp]

theorem TauCeti.spechtModule_iso_iff {n : ℕ} (μ ν : n.Partition) : Nonempty (spechtModule μ ≅ spechtModule ν) ↔ μ = ν

Specht modules have distinct partition labels. Two rational Specht modules for Sₙ are isomorphic if and only if their indexing partitions are equal.