The integer character of a Specht module, and the character table of Sₙ

The Specht module S^μ is a representation of Sₙ over ℚ, so its character (spechtModule μ).character takes values in ℚ. Those values are in fact integers: a character value at an element of finite order is an algebraic integer, and a rational algebraic integer is an integer. That refinement is what this file records, as TauCeti.spechtChar μ : Equiv.Perm (Fin n) → ℤ, together with the cast TauCeti.spechtChar_cast back to the rational character; integrality is a theorem, not part of the definition.

A character is a class function, and the conjugacy classes of Sₙ are the partitions of n (TauCeti.partitionEquivConjClasses), so spechtChar μ descends to a function of a partition ν, its character value TauCeti.spechtCharValue μ ν. Both indices being partitions of n, these values assemble into a square integer matrix, the character table of the symmetric group TauCeti.symmetricCharacterTable n. Its rows are indexed by the Specht modules, which are precisely the irreducible rational representations of Sₙ (TauCeti.partitionEquivSimpleModuleClasses), and its columns by the conjugacy classes; the column of the identity holds the degrees.

The general half of the argument is stated for an arbitrary rational representation of a finite group, as FDRep.intCharacter, and is what this file specializes. Nothing here computes an entry of the table: the recursion that does is the Murnaghan--Nakayama rule, which needs rim hooks and is not proved here. The comparison with the library's general TauCeti.characterTable k G, which lives over an algebraically closed field and enumerates its rows by Fin (Nat.card (ConjClasses G)), and the table properties that one carries — the orthogonality relations and the specification TauCeti.IsCharacterTableSpec — are in TauCeti/RepresentationTheory/Symmetric/Specht/Orthogonality.lean.

Main definitions

• TauCeti.spechtChar: the ℤ-valued character χ^μ of the Specht module S^μ.
• TauCeti.spechtCharConjClasses: its descent to the conjugacy classes of Sₙ.
• TauCeti.spechtCharValue: its value on the class of cycle type ν.
• TauCeti.symmetricCharacterTable: the character table of Sₙ, a Matrix (Nat.Partition n) (Nat.Partition n) ℤ.

Main results

• TauCeti.character_spechtModule_apply: the character of the partition-indexed S^μ is that of the diagram-indexed Specht module of diagramOf μ.
• TauCeti.spechtChar_cast: the integer character casts to the rational character of S^μ.
• TauCeti.spechtChar_eq_of_partition_eq: it depends only on the cycle type.
• TauCeti.spechtChar_one: the value at the identity is the degree dim_ℚ S^μ.
• TauCeti.spechtChar_one_pos: that degree is positive.
• TauCeti.spechtChar_shapePartition: the character of the Specht module of a Young diagram D is χ^μ for the shape partition μ of D.
• TauCeti.spechtChar_eq_value: the character is read off the character table.
• TauCeti.intCast_symmetricCharacterTable_apply: conversely the table recovers the rational character, so no information is lost in passing to ℤ.
• TauCeti.symmetricCharacterTable_one: the column of the identity class holds the degrees.

References

• G. D. James, The Representation Theory of the Symmetric Groups, Chapter 6.
• B. E. Sagan, The Symmetric Group, 2nd ed. (2001), Section 4.10.
• Schur--Weyl roadmap, Layer 6, "The Specht character".

theorem TauCeti.character_spechtModule_apply {n : ℕ} (μ : n.Partition) (σ : Equiv.Perm (Fin n)) : (spechtModule μ).character σ = (spechtSubrepresentation (diagramOf μ)).toRepresentation.character ((finCongr ⋯).permCongr σ)

The character of S^μ is the character of the diagram-indexed Specht module TauCeti.spechtSubrepresentation (diagramOf μ), read through the identification of Sₙ with the permutations of the (diagramOf μ).card = n cells.

The integer character

noncomputable def TauCeti.spechtChar {n : ℕ} (μ : n.Partition) : Equiv.Perm (Fin n) → ℤ

The integer character χ^μ of the Specht module S^μ. The character of S^μ takes rational values, and those values are integers (FDRep.intCharacter); this is the integer-valued refinement, related to the rational character by TauCeti.spechtChar_cast.

Equations

• TauCeti.spechtChar μ = (TauCeti.spechtModule μ).intCharacter

theorem TauCeti.spechtChar_def {n : ℕ} (μ : n.Partition) (σ : Equiv.Perm (Fin n)) : spechtChar μ σ = (spechtModule μ).intCharacter σ

@[simp]

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

The integer character of S^μ casts to its rational character. This is the whole content of TauCeti.spechtChar: the character of a Specht module is integer-valued.

@[simp]

theorem TauCeti.spechtChar_conj {n : ℕ} (μ : n.Partition) (σ τ : Equiv.Perm (Fin n)) : spechtChar μ (τ * σ * τ⁻¹) = spechtChar μ σ

The integer character is a class function.

theorem TauCeti.spechtChar_eq_of_isConj {n : ℕ} (μ : n.Partition) {σ τ : Equiv.Perm (Fin n)} (h : IsConj σ τ) : spechtChar μ σ = spechtChar μ τ

Conjugate permutations have the same integer character.

theorem TauCeti.spechtChar_eq_of_partition_eq {n : ℕ} (μ : n.Partition) {σ τ : Equiv.Perm (Fin n)} (h : σ.partition = τ.partition) : spechtChar μ σ = spechtChar μ τ

The integer character depends only on the cycle type, two permutations of Fin n being conjugate exactly when they have the same partition.

@[simp]

theorem TauCeti.spechtChar_one {n : ℕ} (μ : n.Partition) : spechtChar μ 1 = ↑(Module.finrank ℚ ↑(spechtModule μ).V)

The value at the identity is the degree dim_ℚ S^μ.

theorem TauCeti.spechtChar_one_pos {n : ℕ} (μ : n.Partition) : 0 < spechtChar μ 1

The value at the identity is positive, the Specht module S^μ being nonzero.

theorem TauCeti.spechtChar_shapePartition (D : YoungDiagram) (σ : Equiv.Perm (Fin D.card)) : ↑(spechtChar (shapePartition D) σ) = (spechtSubrepresentation D).toRepresentation.character σ

The character of the Specht module of a diagram: for a Young diagram D, the character of TauCeti.spechtSubrepresentation D, a representation of the permutations of its D.card cells, is the integer character of the Specht module of the shape partition of D. This is TauCeti.character_spechtModule_apply with the transport along diagramOf (shapePartition D) = D removed, which is what lets results about the diagram-indexed Specht modules be read against χ^μ.

Descent to the conjugacy classes

noncomputable def TauCeti.spechtCharConjClasses {n : ℕ} (μ : n.Partition) : ConjClasses (Equiv.Perm (Fin n)) → ℤ

The integer character as a function of the conjugacy class, the descent (TauCeti.ClassFunction.toConjClasses) of the class function FDRep.intClassFunction of S^μ.

Equations

• TauCeti.spechtCharConjClasses μ = TauCeti.ClassFunction.toConjClasses (TauCeti.spechtModule μ).intClassFunction

theorem TauCeti.spechtCharConjClasses_def {n : ℕ} (μ : n.Partition) : spechtCharConjClasses μ = ClassFunction.toConjClasses (spechtModule μ).intClassFunction

@[simp]

theorem TauCeti.spechtCharConjClasses_mk {n : ℕ} (μ : n.Partition) (σ : Equiv.Perm (Fin n)) : spechtCharConjClasses μ (ConjClasses.mk σ) = spechtChar μ σ

noncomputable def TauCeti.spechtCharValue {n : ℕ} (μ ν : n.Partition) : ℤ

The character value of S^μ on the class of cycle type ν, the entry χ^μ(ν) of the character table.

Equations

• TauCeti.spechtCharValue μ ν = TauCeti.spechtCharConjClasses μ ((TauCeti.partitionEquivConjClasses n) ν)

theorem TauCeti.spechtCharValue_def {n : ℕ} (μ ν : n.Partition) : spechtCharValue μ ν = spechtCharConjClasses μ ((partitionEquivConjClasses n) ν)

theorem TauCeti.spechtCharValue_eq_spechtChar {n : ℕ} (μ ν : n.Partition) {σ : Equiv.Perm (Fin n)} (hσ : ConjClasses.mk σ = (partitionEquivConjClasses n) ν) : spechtCharValue μ ν = spechtChar μ σ

The character value is computed at any permutation representing the class of ν.

theorem TauCeti.spechtChar_eq_value {n : ℕ} (μ : n.Partition) (σ : Equiv.Perm (Fin n)) : spechtChar μ σ = spechtCharValue μ ((partitionEquivConjClasses n).symm (ConjClasses.mk σ))

The integer character is read off the character table, at the partition indexing the class of the permutation.

The character table

noncomputable def TauCeti.symmetricCharacterTable (n : ℕ) : Matrix n.Partition n.Partition ℤ

The character table of the symmetric group Sₙ: the integer matrix whose (μ, ν) entry is the value χ^μ(ν) of the character of the Specht module S^μ on the conjugacy class of cycle type ν. Both indices are partitions of n, which index the irreducible rational representations (TauCeti.partitionEquivSimpleModuleClasses) and the conjugacy classes (TauCeti.partitionEquivConjClasses) respectively.

Implementation note: this is not the library's general TauCeti.characterTable k G, which is defined over an algebraically closed field, takes values there, and enumerates its rows by Fin (Nat.card (ConjClasses G)) through an arbitrary choice of ordering of the irreducible characters. This matrix is the ℤ-valued table of Sₙ re-indexed on both sides by the partitions of n; the comparison with TauCeti.characterTable ℂ (Equiv.Perm (Fin n)) and the table properties the general table carries — the orthogonality relations and the character-table specification TauCeti.IsCharacterTableSpec — are proved in TauCeti/RepresentationTheory/Symmetric/Specht/Orthogonality.lean.

Equations

• TauCeti.symmetricCharacterTable n = Matrix.of fun (μ ν : n.Partition) => TauCeti.spechtCharValue μ ν

@[simp]

theorem TauCeti.symmetricCharacterTable_apply {n : ℕ} (μ ν : n.Partition) : symmetricCharacterTable n μ ν = spechtCharValue μ ν

theorem TauCeti.intCast_symmetricCharacterTable_apply {n : ℕ} (μ : n.Partition) (σ : Equiv.Perm (Fin n)) : ↑(symmetricCharacterTable n μ ((partitionEquivConjClasses n).symm (ConjClasses.mk σ))) = (spechtModule μ).character σ

The character table recovers the rational characters of the Specht modules, so passing from ℚ to ℤ and from permutations to cycle types loses nothing.

theorem TauCeti.symmetricCharacterTable_one {n : ℕ} (μ : n.Partition) : symmetricCharacterTable n μ ((partitionEquivConjClasses n).symm (ConjClasses.mk 1)) = ↑(Module.finrank ℚ ↑(spechtModule μ).V)

The column of the identity holds the degrees dim_ℚ S^μ.