The Specht character from the coefficients of a Young symmetrizer

Let t be a tableau of shape μ with n cells, c_t its Young symmetrizer, χ^μ the character of the Specht module S^μ and f^μ = dim S^μ. Averaging the coefficients of c_t over a conjugacy class of Sₙ gives the character value there:

n! · χ^μ(g) = f^μ · ∑_{σ ∈ Sₙ} c_t(σ g σ⁻¹).

Equivalently, pairing c_t with a class function φ of Sₙ is pairing χ^μ with it, up to the factor f^μ:

∑_g χ^μ(g) φ(g) = f^μ · ∑_g c_t(g) φ(g).

The second form is how this enters the character theory of the Weyl modules c_t · V^{⊗n}: their characters are sums (f^μ/n!) ∑_g c_t(g) φ(g) with φ(g) the power sum of the cycle type of g, and the identity turns these into the class-function expansion (1/n!) ∑_g χ^μ(g) φ(g) that Frobenius's formula identifies with the Schur polynomial s_μ.

The proof reads S^μ as the left ideal ℚ[Sₙ] c_t (TauCeti.YoungTableau.character_spechtIdeal_eq_spechtSubrepresentation) and applies the character formula for the left ideal of a quasi-idempotent, Representation.mul_char_ofModule'_span_singleton, to c_t * c_t = (n! / f^μ) • c_t (TauCeti.YoungTableau.youngSymmetrizer_sq). That formula sums the coefficients over the conjugates of g⁻¹; in Sₙ every element is conjugate to its inverse, which turns them into the conjugates of g.

Main results

• TauCeti.YoungTableau.factorial_mul_char_spechtSubrepresentation: n! · χ^μ(g) is f^μ times the sum of the coefficients of c_t over the conjugates σ g σ⁻¹.
• TauCeti.YoungTableau.sum_char_spechtSubrepresentation_smul: pairing χ^μ with a class function is f^μ times pairing c_t with it.
• Representation.factorial_mul_finrank_range_asAlgebraHom_youngSymmetrizerOver: for a finite-dimensional representation M of Sₙ in characteristic zero, n! · dim (c_t M) = ∑_σ χ^μ(σ) χ_M(σ), since the action of c_t is a scaled projection.
• Nat.Partition.youngSymmetrizer_mul_self: the Young symmetrizer c_μ of a partition satisfies c_μ² = (n! / f^μ) c_μ.
• Nat.Partition.finrank_span_youngSymmetrizer: dim (k[Sₙ] c_μ) = f^μ.

References

• W. Fulton and J. Harris, Representation Theory: A First Course (1991), Lecture 4.
• I. G. Macdonald, Symmetric Functions and Hall Polynomials, 2nd ed., Chapter I, Section 7.

theorem TauCeti.YoungTableau.factorial_mul_char_spechtSubrepresentation {μ : YoungDiagram} (t : YoungTableau μ) (g : Equiv.Perm (Fin μ.card)) : ↑μ.card.factorial * (spechtSubrepresentation μ).toRepresentation.character g = ↑(Module.finrank ℚ ↥(spechtSubrepresentation μ).toSubmodule) * ∑ σ : Equiv.Perm (Fin μ.card), t.youngSymmetrizer.coeff (σ * g * σ⁻¹)

The Specht character from the Young symmetrizer. For a tableau t of shape μ with n cells, n! times the character of S^μ at g is dim S^μ times the sum of the coefficients of the Young symmetrizer c_t over the conjugates σ g σ⁻¹.

theorem TauCeti.YoungTableau.sum_char_spechtSubrepresentation_smul {μ : YoungDiagram} (t : YoungTableau μ) {M : Type u_1} [AddCommGroup M] [Module ℚ M] (φ : Equiv.Perm (Fin μ.card) → M) (hφ : ∀ (g σ : Equiv.Perm (Fin μ.card)), φ (σ * g * σ⁻¹) = φ g) : ∑ g : Equiv.Perm (Fin μ.card), (spechtSubrepresentation μ).toRepresentation.character g • φ g = ↑(Module.finrank ℚ ↥(spechtSubrepresentation μ).toSubmodule) • ∑ g : Equiv.Perm (Fin μ.card), t.youngSymmetrizer.coeff g • φ g

Pairing a class function with the Young symmetrizer. For a tableau t of shape μ and a function φ on the permutations that is constant on conjugacy classes, pairing φ with the character of S^μ gives dim S^μ times pairing it with the coefficients of c_t.

theorem Nat.Partition.youngSymmetrizer_mul_self {d : ℕ} (μ : d.Partition) (k : Type u_1) [CommSemiring k] [Algebra ℚ k] : μ.youngSymmetrizer k * μ.youngSymmetrizer k = (algebraMap ℚ k) (↑d.factorial / ↑(Module.finrank ℚ ↑(TauCeti.spechtModule μ).V)) • μ.youngSymmetrizer k

The Young symmetrizer is quasi-idempotent: c_μ² = (d! / f^μ) c_μ, where f^μ is the dimension of the Specht module S^μ.

theorem Nat.Partition.finrank_span_youngSymmetrizer {d : ℕ} (μ : d.Partition) (k : Type u_1) [Field k] [CharZero k] : Module.finrank k ↥(Ideal.span {μ.youngSymmetrizer k}) = Module.finrank ℚ ↑(TauCeti.spechtModule μ).V

The left ideal k[S_d] c_μ has the dimension f^μ of the Specht module. Its character at the identity, multiplied by d! / f^μ, is d! times the coefficient 1 of the identity in c_μ (Representation.mul_char_ofModule'_span_singleton).

theorem Representation.factorial_mul_finrank_range_asAlgebraHom_youngSymmetrizerOver {k : Type u_1} [Field k] [CharZero k] {M : Type u_2} [AddCommGroup M] [Module k M] [FiniteDimensional k M] {D : YoungDiagram} (t : TauCeti.YoungTableau D) (ρ : Representation k (Equiv.Perm (Fin D.card)) M) : ↑D.card.factorial * ↑(Module.finrank k ↥(LinearMap.range (ρ.asAlgebraHom (TauCeti.YoungTableau.youngSymmetrizerOver k t)))) = ∑ σ : Equiv.Perm (Fin D.card), (TauCeti.spechtSubrepresentation D).toRepresentation.character σ • ρ.character σ

The dimension of the image of the Young symmetrizer of a tableau, through the Specht character: for a tableau t of shape μ and a finite-dimensional representation M of S_{|μ|}, |μ|! · dim (c_t M) = ∑_σ χ^μ(σ) χ_M(σ).