The character table of Sₙ is a character table, and its orthogonality relations

This file identifies the integer matrix TauCeti.symmetricCharacterTable n, whose (μ, ν) entry is the value χ^μ(ν) of the character of the Specht module S^μ on the class of cycle type ν, with the library's complex character table TauCeti.characterTable ℂ (Equiv.Perm (Fin n)). It then proves the specification TauCeti.IsCharacterTableSpec and the row and column orthogonality relations for the table.

The bridge is that the complex Specht modules are exactly the irreducible complex representations of Sₙ (TauCeti.existsUnique_character_eq_spechtChar), so each χ^μ, read in ℂ, is one of the enumerated irreducible characters, and μ ↦ (its index) is a bijection onto the row index of the complex character table. Both index sets have as many elements as Sₙ has conjugacy classes, so injectivity — which is the distinctness of the complex Specht modules — already gives the bijection. Reindexing the rows by that bijection and the columns by TauCeti.partitionEquivConjClasses turns the integer table into characterTable ℂ Sₙ on the nose, whence the specification and, entry by entry, the two orthogonality relations.

The orthogonality relations are stated over ℤ, where the values live: division by class sizes is avoided by weighting with the class size n ! / z_ν itself, which is exact by TauCeti.zPart_dvd_factorial. The rational form with the classical weights 1 / z_ν, TauCeti.sum_symmetricCharacterTable_mul_div_zPart, is the shape the Hall inner product of symmetric-function theory uses, and follows by dividing by n !. Complex conjugation, which is what the general relations over ℂ carry, disappears here: the entries are integers, so a row and its conjugate coincide.

Main definitions

• TauCeti.partitionEquivIrreducibleIndex: the bijection sending μ to the row of the complex character table of Sₙ carrying χ^μ.
• TauCeti.symmetricCharacterTableℂ: the integer character table of Sₙ read in ℂ and reindexed on both sides into the shape TauCeti.IsCharacterTableSpec asks for.

Main results

• TauCeti.characterTable_partitionEquivIrreducibleIndex: the entries of the complex character table of Sₙ are the entries of TauCeti.symmetricCharacterTable.
• TauCeti.symmetricCharacterTableℂ_eq_characterTable and TauCeti.isCharacterTableSpec_symmetricCharacterTableℂ: the character table of Sₙ is the complex character table of Sₙ, and satisfies the character-table specification.
• TauCeti.symmetricCharacterTable_column_orthogonality: second (column) orthogonality, ∑_μ χ^μ(ν) χ^μ(ν') = z_ν when ν = ν' and 0 otherwise.
• TauCeti.symmetricCharacterTable_row_orthogonality: first (row) orthogonality, ∑_ν (n !/z_ν) χ^μ(ν) χ^μ'(ν) = n ! when μ = μ' and 0 otherwise, with TauCeti.sum_symmetricCharacterTable_mul_div_zPart its rational form ∑_ν χ^μ(ν) χ^μ'(ν)/z_ν.
• TauCeti.sum_finrank_spechtModule_sq: ∑_{μ ⊢ n} (f^μ)² = n !, column orthogonality at the identity class.
• TauCeti.sum_spechtChar_mul_spechtChar: column orthogonality read at two permutations.
• TauCeti.eq_sum_spechtChar: every rational class function of Sₙ is ∑_μ ⟨f, χ^μ⟩ χ^μ, so the Specht characters span the class functions.
• TauCeti.sum_finrank_spechtModule_mul_spechtChar: ∑_{μ ⊢ n} f^μ χ^μ(σ) is n ! at the identity and 0 elsewhere, column orthogonality against the identity class: the character of the regular representation is ∑_μ f^μ χ^μ.

References

• G. D. James, The Representation Theory of the Symmetric Groups, Chapter 6.
• B. E. Sagan, The Symmetric Group, 2nd ed. (2001), Sections 1.9 and 4.7.

The Specht character as an enumerated irreducible character

theorem TauCeti.spechtChar_mem_irreducibleCharacters {n : ℕ} (μ : n.Partition) : (fun (σ : Equiv.Perm (Fin n)) => ↑(spechtChar μ σ)) ∈ irreducibleCharacters ℂ (Equiv.Perm (Fin n))

The integer character χ^μ, read in ℂ, is an irreducible character of Sₙ. The complex Specht module is simple (TauCeti.instSimpleSpechtModuleℂ) and its character is χ^μ.

noncomputable def TauCeti.partitionEquivIrreducibleIndex (n : ℕ) : n.Partition ≃ Fin (Nat.card (ConjClasses (Equiv.Perm (Fin n))))

The partitions of n index the rows of the complex character table of Sₙ, by μ ↦ χ^μ: the row partitionEquivIrreducibleIndex n μ carries the character χ^μ (TauCeti.irreducibleCharacter_partitionEquivIrreducibleIndex), and every row is of this form exactly once.

Equations

• TauCeti.partitionEquivIrreducibleIndex n = Equiv.ofBijective TauCeti.spechtCharIndex✝ ⋯

@[simp]

theorem TauCeti.irreducibleCharacter_partitionEquivIrreducibleIndex {n : ℕ} (μ : n.Partition) (σ : Equiv.Perm (Fin n)) : irreducibleCharacter ℂ ((partitionEquivIrreducibleIndex n) μ) σ = ↑(spechtChar μ σ)

The character enumerated at the row TauCeti.partitionEquivIrreducibleIndex n μ is χ^μ, the character of the complex Specht module S^μ.

The integer table is the complex character table

@[simp]

theorem TauCeti.characterTable_partitionEquivIrreducibleIndex {n : ℕ} (μ ν : n.Partition) : characterTable ℂ (Equiv.Perm (Fin n)) ((partitionEquivIrreducibleIndex n) μ) ((partitionEquivConjClasses n) ν) = ↑(symmetricCharacterTable n μ ν)

The complex character table of Sₙ has the entries of TauCeti.symmetricCharacterTable, once its rows are indexed by TauCeti.partitionEquivIrreducibleIndex and its columns by TauCeti.partitionEquivConjClasses. The entry at a representative σ of the class, χ^μ(σ), is TauCeti.characterTable_apply followed by TauCeti.irreducibleCharacter_partitionEquivIrreducibleIndex.

noncomputable def TauCeti.symmetricCharacterTableℂ (n : ℕ) : Matrix (Fin (Nat.card (ConjClasses (Equiv.Perm (Fin n))))) (ConjClasses (Equiv.Perm (Fin n))) ℂ

The character table of Sₙ in the shape the specification asks for: the integer entries of TauCeti.symmetricCharacterTable read in ℂ, with the rows indexed by Fin (Nat.card (ConjClasses (Equiv.Perm (Fin n)))) and the columns by the conjugacy classes themselves. It is the complex character table (TauCeti.symmetricCharacterTableℂ_eq_characterTable).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.symmetricCharacterTableℂ_apply (n : ℕ) (i : Fin (Nat.card (ConjClasses (Equiv.Perm (Fin n))))) (C : ConjClasses (Equiv.Perm (Fin n))) : symmetricCharacterTableℂ n i C = ↑(symmetricCharacterTable n ((partitionEquivIrreducibleIndex n).symm i) ((partitionEquivConjClasses n).symm C))

The entries of the reindexed complex character table are the integer Specht character values read in ℂ.

theorem TauCeti.symmetricCharacterTableℂ_eq_characterTable (n : ℕ) : symmetricCharacterTableℂ n = characterTable ℂ (Equiv.Perm (Fin n))

The reindexed integer character table of Sₙ is the complex character table of Sₙ.

theorem TauCeti.isCharacterTableSpec_symmetricCharacterTableℂ (n : ℕ) : IsCharacterTableSpec (Equiv.Perm (Fin n)) (symmetricCharacterTableℂ n)

The character table of Sₙ satisfies the character-table specification: its identity column consists of positive divisors of n ! whose squares sum to n !, its rows are orthonormal for the class-size weighted Hermitian pairing, and its normalized rows are common left eigenrows of the class-multiplication matrices. By TauCeti.characterTable_unique_rows this pins the table down up to a permutation of its rows.

The orthogonality relations

theorem TauCeti.symmetricCharacterTable_column_orthogonality {n : ℕ} (ν ν' : n.Partition) : ∑ μ : n.Partition, symmetricCharacterTable n μ ν * symmetricCharacterTable n μ ν' = if ν = ν' then ↑(zPart ν) else 0

Second (column) orthogonality for Sₙ: two columns of the character table pair to the weight z_ν of their common cycle type, and to 0 when the cycle types differ. The weight is the order of the centralizer of a permutation of that cycle type (TauCeti.nat_card_centralizer_eq_zPart), which is n ! divided by the size of the class.

theorem TauCeti.symmetricCharacterTable_row_orthogonality {n : ℕ} (μ μ' : n.Partition) : ∑ ν : n.Partition, ↑(n.factorial / zPart ν) * symmetricCharacterTable n μ ν * symmetricCharacterTable n μ' ν = if μ = μ' then ↑n.factorial else 0

First (row) orthogonality for Sₙ, in a form free of division: two rows of the character table, paired with the class sizes n !/z_ν as weights, give n ! on the diagonal and 0 off it.

theorem TauCeti.sum_symmetricCharacterTable_mul_div_zPart {n : ℕ} (μ μ' : n.Partition) : ∑ ν : n.Partition, ↑(symmetricCharacterTable n μ ν) * ↑(symmetricCharacterTable n μ' ν) / ↑(zPart ν) = if μ = μ' then 1 else 0

First (row) orthogonality for Sₙ in its classical rational form: the characters are orthonormal for the pairing ⟨f, g⟩ = ∑_ν f(ν) g(ν) / z_ν. This is TauCeti.symmetricCharacterTable_row_orthogonality divided by n !, the divisions being exact by TauCeti.zPart_dvd_factorial.

theorem TauCeti.sum_finrank_spechtModule_mul_spechtChar {n : ℕ} (σ : Equiv.Perm (Fin n)) : ∑ μ : n.Partition, ↑(Module.finrank ℚ ↑(spechtModule μ).V) * spechtChar μ σ = if σ = 1 then ↑n.factorial else 0

Column orthogonality against the identity class: ∑_{μ ⊢ n} f^μ χ^μ(σ) is n ! when σ = 1 and 0 otherwise, where f^μ = dim_ℚ S^μ. This is the decomposition of the character of the regular representation of Sₙ into the Specht characters, each with multiplicity its degree.

theorem TauCeti.sum_finrank_spechtModule_sq (n : ℕ) : ∑ μ : n.Partition, Module.finrank ℚ ↑(spechtModule μ).V ^ 2 = n.factorial

The dimensions of the Specht modules square-sum to n !. This is column orthogonality at the class of the identity, whose weight z is the order of Sₙ and whose column holds the degrees f^μ = dim_ℚ S^μ: the value at σ = 1 of TauCeti.sum_finrank_spechtModule_mul_spechtChar.

Column orthogonality at permutations, and the expansion of class functions

theorem TauCeti.sum_spechtChar_mul_spechtChar {n : ℕ} (σ τ : Equiv.Perm (Fin n)) : ∑ μ : n.Partition, spechtChar μ σ * spechtChar μ τ = if IsConj σ τ then ↑(zPart σ.partition) else 0

Second (column) orthogonality for Sₙ, read at two permutations: ∑_μ χ^μ(σ) χ^μ(τ) is the centralizer order z_{ρ(σ)} when σ and τ are conjugate, and 0 otherwise.

theorem TauCeti.eq_sum_spechtChar {n : ℕ} (f : ↥(ClassFunction ℚ (Equiv.Perm (Fin n)))) (σ : Equiv.Perm (Fin n)) : ↑f σ = ∑ μ : n.Partition, ((↑n.factorial)⁻¹ * ∑ π : Equiv.Perm (Fin n), ↑f π * ↑(spechtChar μ π)) * ↑(spechtChar μ σ)

The Specht characters span the rational class functions of Sₙ: a class function f is ∑_μ ⟨f, χ^μ⟩ χ^μ, the coefficient of χ^μ being the character pairing ⟨f, χ^μ⟩ = (1 / n!) ∑_π f(π) χ^μ(π).