The complex Specht modules classify the irreducible complex representations of Sₙ

The Specht module S^μ is defined over ℚ, and this file extends its scalars to ℂ: TauCeti.spechtModuleℂ μ is ℂ ⊗_ℚ S^μ, an object of FDRep ℂ Sₙ. The point of the file is that nothing is lost and nothing is gained in the passage — the complex Specht modules are again simple, again pairwise non-isomorphic, and again all of the simple objects — so the partitions of n classify the irreducible complex representations of the symmetric group exactly as they classify the rational ones (TauCeti.partitionEquivSimpleFDRepClasses).

Simplicity is where the rational theory could fail and does not, and the reason is absolute irreducibility: irreducibility over ℚ alone says nothing about ℂ ⊗_ℚ S^μ, but TauCeti.spechtModuleIntertwiningEndAlgEquiv says the intertwiner algebra of S^μ is ℚ itself, one-dimensional, and the intertwiner space is the kernel of a linear map, so its dimension is unchanged by the flat extension ℚ → ℂ (Representation.finrank_intertwiningMap_baseChange). So the complex endomorphism algebra is one-dimensional too, which over ℂ is simplicity (FDRep.simple_iff_char_is_norm_one). The same dimension count with two different partitions is 0 on the rational side by Schur's lemma, hence 0 on the complex side, which is distinctness; and the partitions of n are as many as the conjugacy classes of Sₙ, which bounds the number of isomorphism classes of simple objects over a field whose group algebra is semisimple, as ℂ[Sₙ] is, so distinctness already forces exhaustion.

Because the character of S^μ is integer-valued (TauCeti.spechtChar), the complex characters are the same integers read in ℂ, and the integer-valued character table of Sₙ (TauCeti.symmetricCharacterTable, a Matrix (Nat.Partition n) (Nat.Partition n) ℤ), whose casts recover the rational character values, therefore records the complex ones just as well: the irreducible complex characters of Sₙ are exactly the χ^μ.

Main definitions

• TauCeti.spechtModuleℂ: the complex Specht module ℂ ⊗_ℚ S^μ.
• TauCeti.spechtModuleℂFDRepClass: its isomorphism class as a simple object of FDRep ℂ Sₙ.
• TauCeti.partitionEquivSimpleFDRepClassesℂ: the classification, μ ↦ ℂ ⊗_ℚ S^μ as a bijection from Nat.Partition n to the isomorphism classes of simple objects of FDRep ℂ Sₙ.

Main results

• TauCeti.character_spechtModuleℂ and TauCeti.character_spechtModuleℂ_intCast: the complex character is the rational character, equivalently the integer character χ^μ, read in ℂ.
• TauCeti.finrank_spechtModuleℂ: extending the scalars does not change the dimension.
• TauCeti.instSimpleSpechtModuleℂ: the complex Specht module is simple.
• TauCeti.spechtModuleℂ_iso_iff: complex Specht modules of distinct shapes are non-isomorphic.
• TauCeti.existsUnique_nonempty_iso_spechtModuleℂ: every simple object of FDRep ℂ Sₙ is a complex Specht module for exactly one partition.
• TauCeti.existsUnique_character_eq_spechtChar: the ℂ-corollary — the irreducible complex characters of Sₙ are exactly the integer characters χ^μ, one for each partition of n.

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.

The complex Specht module

noncomputable def TauCeti.spechtModuleℂ {n : ℕ} (μ : n.Partition) : FDRep ℂ (Equiv.Perm (Fin n))

The complex Specht module ℂ ⊗_ℚ S^μ, the scalar extension of the rational Specht module TauCeti.spechtModule to ℂ. It is simple (TauCeti.instSimpleSpechtModuleℂ), and as μ ranges over the partitions of n these exhaust the simple objects of FDRep ℂ Sₙ without repetition (TauCeti.partitionEquivSimpleFDRepClassesℂ).

Equations

• TauCeti.spechtModuleℂ μ = FDRep.of (Representation.baseChange ℂ (TauCeti.spechtModule μ).ρ)

theorem TauCeti.spechtModuleℂ_def {n : ℕ} (μ : n.Partition) : spechtModuleℂ μ = FDRep.of (Representation.baseChange ℂ (spechtModule μ).ρ)

The complex Specht module is the object of FDRep ℂ Sₙ carrying the base change of the rational Specht representation.

theorem TauCeti.character_spechtModuleℂ {n : ℕ} (μ : n.Partition) (σ : Equiv.Perm (Fin n)) : (spechtModuleℂ μ).character σ = (algebraMap ℚ ℂ) ((spechtModule μ).character σ)

The complex character is the rational character read in ℂ.

@[simp]

theorem TauCeti.character_spechtModuleℂ_intCast {n : ℕ} (μ : n.Partition) (σ : Equiv.Perm (Fin n)) : (spechtModuleℂ μ).character σ = ↑(spechtChar μ σ)

The complex character is the integer character χ^μ read in ℂ. Combined with TauCeti.spechtChar_eq_value this says that the integer-valued character table of Sₙ, TauCeti.symmetricCharacterTable, whose casts recover the rational character values, records the complex ones too.

theorem TauCeti.finrank_spechtModuleℂ {n : ℕ} (μ : n.Partition) : Module.finrank ℂ ↑(spechtModuleℂ μ).V = Module.finrank ℚ ↑(spechtModule μ).V

Extending the scalars does not change the dimension.

Simplicity and distinctness

instance TauCeti.instSimpleSpechtModuleℂ {n : ℕ} (μ : n.Partition) : CategoryTheory.Simple (spechtModuleℂ μ)

The complex Specht module is simple. Its endomorphism algebra is one-dimensional, because that of the rational Specht module is (TauCeti.spechtModuleIntertwiningEndAlgEquiv) and the dimension survives complexification; over ℂ a one-dimensional endomorphism algebra is simplicity.

@[simp]

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

Complex Specht modules of distinct shapes are non-isomorphic.

theorem TauCeti.spechtModuleℂ_character_injective {n : ℕ} : Function.Injective fun (μ : n.Partition) => (spechtModuleℂ μ).character

A complex Specht module is determined by its character. A simple object of FDRep ℂ Sₙ is determined by its character (FDRep.nonempty_iso_of_character_eq_of_simple), and complex Specht modules of distinct shapes are non-isomorphic.

The classification

noncomputable def TauCeti.spechtModuleℂFDRepClass {n : ℕ} (μ : n.Partition) : SimpleFDRepClasses ℂ (Equiv.Perm (Fin n))

The isomorphism class of the complex Specht module ℂ ⊗_ℚ S^μ as a simple object of FDRep ℂ Sₙ. The complex counterpart of TauCeti.spechtModuleFDRepClass.

Equations

• TauCeti.spechtModuleℂFDRepClass μ = TauCeti.SimpleFDRepClasses.mk (TauCeti.spechtModuleℂ μ)

@[simp]

theorem TauCeti.spechtModuleℂFDRepClass_def {n : ℕ} (μ : n.Partition) : spechtModuleℂFDRepClass μ = SimpleFDRepClasses.mk (spechtModuleℂ μ)

theorem TauCeti.spechtModuleℂFDRepClass_bijective {n : ℕ} : Function.Bijective spechtModuleℂFDRepClass

The complex Specht modules exhaust the simple objects of FDRep ℂ Sₙ. They are pairwise non-isomorphic and as many as the conjugacy classes of Sₙ, and over a field whose group algebra is semisimple, as ℂ[Sₙ] is, the conjugacy classes bound the isomorphism classes of simple objects (TauCeti.SimpleFDRepClasses.bijective_of_injective_of_card_conjClasses_le), so there is no room for any other.

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

The classification of the irreducible complex representations of the symmetric group: μ ↦ ℂ ⊗_ℚ S^μ is a bijection from the partitions of n to the isomorphism classes of simple objects of FDRep ℂ Sₙ. It is the complex counterpart of TauCeti.partitionEquivSimpleFDRepClasses, indexed by the same partitions.

Equations

• TauCeti.partitionEquivSimpleFDRepClassesℂ n = Equiv.ofBijective TauCeti.spechtModuleℂFDRepClass ⋯

@[simp]

theorem TauCeti.partitionEquivSimpleFDRepClassesℂ_apply {n : ℕ} (μ : n.Partition) : (partitionEquivSimpleFDRepClassesℂ n) μ = spechtModuleℂFDRepClass μ

@[simp]

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

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

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 complex Specht module for exactly one partition.

theorem TauCeti.existsUnique_character_eq_spechtChar {n : ℕ} (X : FDRep ℂ (Equiv.Perm (Fin n))) [CategoryTheory.Simple X] : ∃! μ : n.Partition, X.character = fun (σ : Equiv.Perm (Fin n)) => ↑(spechtChar μ σ)

The ℂ-corollary: the irreducible complex characters of Sₙ are exactly the χ^μ. Every simple object of FDRep ℂ Sₙ has, for exactly one partition μ of n, the integer character TauCeti.spechtChar of the Specht module S^μ read in ℂ. With TauCeti.spechtChar_eq_value this identifies the integer-valued TauCeti.symmetricCharacterTable n, whose casts recover the rational character values, as recording the complex character table of Sₙ as well.