The Specht modules classify the irreducible rational representations of Sₙ

The Specht modules S^μ are irreducible over ℚ (TauCeti.isIrreducible_spechtModule) and pairwise non-isomorphic (TauCeti.spechtModule_iso_iff). This file proves that there are no others: μ ↦ S^μ is a bijection from the partitions of n to the isomorphism classes of simple ℚ[Sₙ]-modules, so every irreducible rational representation of the symmetric group is a Specht module.

Only counting is left to do. The partitions of n index the conjugacy classes of Sₙ (TauCeti.partitionEquivConjClasses), and over any field with k[G] semisimple the isomorphism classes of simple k[G]-modules are at most as many as the conjugacy classes (TauCeti.card_simpleSubmoduleClasses_le_card_conjClasses). An injection from a finite set into a set of no greater size is a bijection.

Working over ℚ rather than over ℂ costs nothing here, because the counting bound is not a splitting-field statement: it bounds the simple modules over any field by the conjugacy classes, and the Specht modules already saturate the bound over ℚ. In particular the classification does not go through absolute irreducibility. The separate statement End_{ℚ[Sₙ]} S^μ ≅ ℚ is proved in TauCeti.RepresentationTheory.Symmetric.Specht.AbsoluteIrreducibility; it is the input a corresponding classification over ℂ will need.

The classification is stated in each of the three languages a consumer may already be working in: the isomorphism classes of simple ℚ[Sₙ]-modules, the irreducible representations, and the simple objects of FDRep ℚ Sₙ. Each language has a ∃! form, since the partition attached to a simple module or irreducible representation is what the classification is usually quoted as producing; the module and FDRep languages additionally have explicit bijections. The comparison of those two bijections is TauCeti.coe_simpleFDRepClassesEquivSimpleModuleClasses: the bijection between the two targets that the two classifications assemble to is the map sending a simple object to the module it carries, so the readings agree.

Main results

• TauCeti.spechtModuleClass: the isomorphism class of the simple ℚ[Sₙ]-module S^μ.
• TauCeti.partitionEquivSimpleModuleClasses: the classification, μ ↦ S^μ as a bijection from Nat.Partition n to the isomorphism classes of simple ℚ[Sₙ]-modules.
• TauCeti.existsUnique_nonempty_linearEquiv_spechtModule: every simple ℚ[Sₙ]-module is isomorphic to a Specht module for exactly one partition.
• TauCeti.existsUnique_nonempty_equiv_spechtModule: every irreducible rational representation of Sₙ is equivalent to a Specht module for exactly one partition.
• TauCeti.partitionEquivSimpleFDRepClasses: the classification in FDRep ℚ Sₙ, μ ↦ S^μ as a bijection from Nat.Partition n to the isomorphism classes of simple objects, with TauCeti.existsUnique_nonempty_iso_spechtModule its ∃! form.
• TauCeti.coe_simpleFDRepClassesEquivSimpleModuleClasses: the two classifications agree.

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".

noncomputable def TauCeti.spechtModuleClass {n : ℕ} (μ : n.Partition) : SimpleSubmoduleClasses (MonoidAlgebra ℚ (Equiv.Perm (Fin n))) (MonoidAlgebra ℚ (Equiv.Perm (Fin n)))

The isomorphism class of the Specht module S^μ, as a simple module over the rational group algebra of Sₙ.

That this is built as TauCeti.simpleModuleClass of the module S^μ carries is an implementation detail; use TauCeti.spechtModuleClass_def to see it.

Equations

• TauCeti.spechtModuleClass μ = TauCeti.simpleModuleClass (MonoidAlgebra ℚ (Equiv.Perm (Fin n))) (Representation.asModule (TauCeti.spechtModule μ).ρ)

@[simp]

theorem TauCeti.spechtModuleClass_def {n : ℕ} (μ : n.Partition) : spechtModuleClass μ = simpleModuleClass (MonoidAlgebra ℚ (Equiv.Perm (Fin n))) (Representation.asModule (spechtModule μ).ρ)

The defining equation of TauCeti.spechtModuleClass: it is the class of the ℚ[Sₙ]-module carried by the Specht module S^μ.

theorem TauCeti.nonempty_linearEquiv_spechtModule_asModule_iff {n : ℕ} (μ ν : n.Partition) : Nonempty (Representation.asModule (spechtModule μ).ρ ≃ₗ[MonoidAlgebra ℚ (Equiv.Perm (Fin n))] Representation.asModule (spechtModule ν).ρ) ↔ μ = ν

Specht modules with distinct shapes carry non-isomorphic modules. This is TauCeti.spechtModule_iso_iff read through the dictionary between isomorphism of representations and isomorphism of the ℚ[Sₙ]-modules they carry.

This is deliberately not a simp lemma: (spechtModule μ).ρ is not a simp normal form, because the simp lemma FDRep.of_ρ' unfolds it to the composite that spechtModule is built from, so simp would never see this left-hand side. The parallel TauCeti.spechtModule_iso_iff can carry the tag because its left-hand side mentions only the FDRep object.

theorem TauCeti.spechtModuleClass_injective {n : ℕ} : Function.Injective spechtModuleClass

Distinct partitions give distinct isomorphism classes: the irredundancy half of the classification.

theorem TauCeti.spechtModuleClass_bijective {n : ℕ} : Function.Bijective spechtModuleClass

The Specht modules exhaust the simple ℚ[Sₙ]-modules. They are as many as the conjugacy classes of Sₙ and pairwise non-isomorphic, and no field admits more isomorphism classes of simple modules over the group algebra than the group has conjugacy classes.

noncomputable def TauCeti.partitionEquivSimpleModuleClasses (n : ℕ) : n.Partition ≃ SimpleSubmoduleClasses (MonoidAlgebra ℚ (Equiv.Perm (Fin n))) (MonoidAlgebra ℚ (Equiv.Perm (Fin n)))

The classification of the irreducible rational representations of the symmetric group. Sending a partition of n to the isomorphism class of the Specht module S^μ is a bijection onto the isomorphism classes of simple ℚ[Sₙ]-modules.

Equations

• TauCeti.partitionEquivSimpleModuleClasses n = Equiv.ofBijective TauCeti.spechtModuleClass ⋯

@[simp]

theorem TauCeti.partitionEquivSimpleModuleClasses_apply {n : ℕ} (μ : n.Partition) : (partitionEquivSimpleModuleClasses n) μ = spechtModuleClass μ

theorem TauCeti.existsUnique_nonempty_linearEquiv_spechtModule {n : ℕ} (M : Type u_1) [AddCommGroup M] [Module (MonoidAlgebra ℚ (Equiv.Perm (Fin n))) M] [IsSimpleModule (MonoidAlgebra ℚ (Equiv.Perm (Fin n))) M] : ∃! μ : n.Partition, Nonempty (M ≃ₗ[MonoidAlgebra ℚ (Equiv.Perm (Fin n))] Representation.asModule (spechtModule μ).ρ)

Every simple ℚ[Sₙ]-module is a Specht module for exactly one partition.

theorem TauCeti.existsUnique_nonempty_equiv_spechtModule {n : ℕ} {V : Type u_1} [AddCommGroup V] [Module ℚ V] (ρ : Representation ℚ (Equiv.Perm (Fin n)) V) [ρ.IsIrreducible] : ∃! μ : n.Partition, Nonempty (ρ.Equiv (spechtModule μ).ρ)

Every irreducible rational representation of Sₙ is a Specht module for exactly one partition.

noncomputable def TauCeti.spechtModuleFDRepClass {n : ℕ} (μ : n.Partition) : SimpleFDRepClasses ℚ (Equiv.Perm (Fin n))

The isomorphism class of the Specht module S^μ as a simple object of FDRep ℚ Sₙ. The categorical counterpart of TauCeti.spechtModuleClass.

Equations

• TauCeti.spechtModuleFDRepClass μ = TauCeti.SimpleFDRepClasses.mk (TauCeti.spechtModule μ)

@[simp]

theorem TauCeti.spechtModuleFDRepClass_def {n : ℕ} (μ : n.Partition) : spechtModuleFDRepClass μ = SimpleFDRepClasses.mk (spechtModule μ)

theorem TauCeti.spechtModuleFDRepClass_bijective {n : ℕ} : Function.Bijective spechtModuleFDRepClass

The classification, read in FDRep ℚ Sₙ. Sending a partition of n to the isomorphism class of the Specht module S^μ is a bijection onto the isomorphism classes of simple objects of FDRep ℚ Sₙ.

noncomputable def TauCeti.partitionEquivSimpleFDRepClasses (n : ℕ) : n.Partition ≃ SimpleFDRepClasses ℚ (Equiv.Perm (Fin n))

The categorical classification of the irreducible rational representations of the symmetric group: μ ↦ S^μ is a bijection from the partitions of n to the isomorphism classes of simple objects of FDRep ℚ Sₙ.

Equations

• TauCeti.partitionEquivSimpleFDRepClasses n = Equiv.ofBijective TauCeti.spechtModuleFDRepClass ⋯

@[simp]

theorem TauCeti.partitionEquivSimpleFDRepClasses_apply {n : ℕ} (μ : n.Partition) : (partitionEquivSimpleFDRepClasses n) μ = spechtModuleFDRepClass μ

theorem TauCeti.existsUnique_nonempty_iso_spechtModule {n : ℕ} (X : FDRep ℚ (Equiv.Perm (Fin n))) [CategoryTheory.Simple X] : ∃! μ : n.Partition, Nonempty (X ≅ spechtModule μ)

Every simple object of FDRep ℚ Sₙ is a Specht module for exactly one partition. This is the classification in the language of the categorical representation API.

@[simp]

theorem TauCeti.partitionEquivSimpleFDRepClasses_symm_mk_spechtModule {n : ℕ} (μ : n.Partition) : (partitionEquivSimpleFDRepClasses n).symm (SimpleFDRepClasses.mk (spechtModule μ)) = μ

The partition a Specht module's class names is the partition it was built from: the symm companion of TauCeti.partitionEquivSimpleFDRepClasses_apply.

noncomputable def TauCeti.simpleFDRepClassesEquivSimpleModuleClasses (n : ℕ) : SimpleFDRepClasses ℚ (Equiv.Perm (Fin n)) ≃ SimpleSubmoduleClasses (MonoidAlgebra ℚ (Equiv.Perm (Fin n))) (MonoidAlgebra ℚ (Equiv.Perm (Fin n)))

The categorical classification and the module classification are the same bijection, read across μ ↦ S^μ.

Equations

• TauCeti.simpleFDRepClassesEquivSimpleModuleClasses n = (TauCeti.partitionEquivSimpleFDRepClasses n).symm.trans (TauCeti.partitionEquivSimpleModuleClasses n)

@[simp]

theorem TauCeti.coe_simpleFDRepClassesEquivSimpleModuleClasses {n : ℕ} : ⇑(simpleFDRepClassesEquivSimpleModuleClasses n) = SimpleFDRepClasses.toSimpleSubmoduleClasses

The abstract comparison of the two classifications is the concrete one: the bijection TauCeti.simpleFDRepClassesEquivSimpleModuleClasses, assembled from the two classification bijections, is the map sending a simple object of FDRep ℚ Sₙ to the isomorphism class of the ℚ[Sₙ]-module it carries.