The character of a Weyl module is a Schur polynomial

The Weyl module 𝕊^μ(kⁿ) = TauCeti.weylModuleOfShape k n μ is the subrepresentation of (kⁿ)^{⊗|μ|} cut out by a Young symmetrizer of the shape μ, and the classical statement about its character is that on the diagonal torus TauCeti.diagGL it is the Schur polynomial of μ:

char (𝕊^μ(kⁿ)) (diag t) = s_μ(t₀, …, t_{n-1}).

Over a field of characteristic zero this file proves that identity for every partition μ (TauCeti.char_weylRepOfShape_ofPartition_diagonal). The character of 𝕊^μ(kⁿ) on the torus is (1 / d!) · ∑_{σ ∈ S_d} χ^μ(σ) · p_{ρ(σ)}, the Specht character χ^μ weighting the power sums over the cycle types (TauCeti.char_weylRepOfShape_ofPartition_diagonal_eq_sum_spechtChar), and the inverse of Frobenius's formula (TauCeti.sum_spechtChar_smul_psumPart) identifies that average with s_μ. Read at the identity element, the identity is a dimension count: the Weyl module of μ has dimension the number of semistandard tableaux of shape μ with entries below n.

The two extreme shapes need no separate statement. For a shape with at most one row the Weyl module is a symmetric power of the standard representation and the formula reads s_{(d)} = h_d, a complete homogeneous symmetric polynomial; for a shape with at most one column it is an exterior power and the formula reads s_{(1^d)} = e_d, an elementary symmetric polynomial.

Main results

• TauCeti.char_weylRepOfShape_ofPartition_diagonal and its bundled form TauCeti.char_weylFDRepOfShape_ofPartition_diagonal: the character of the Weyl module of a partition μ is the Schur polynomial s_μ on the diagonal torus.
• TauCeti.char_weylRepOfShape_diagonal_eq_eval_diagramSchurPoly and TauCeti.char_weylFDRepOfShape_diagonal_eq_eval_diagramSchurPoly: the same formula for every Young diagram, expressed using TauCeti.diagramSchurPoly.
• TauCeti.finrank_weylModuleOfShape: the dimension of the Weyl module of a Young diagram is the number of semistandard tableaux of its shape in the n-letter alphabet, the value of its Schur polynomial at one.

The k = ℂ case of the bundled statements is the statement for TauCeti.schurFunctor, which is a definitional re-export of TauCeti.weylFDRepOfShape over ℂ, so it needs no separate declaration.

References

• W. Fulton and J. Harris, Representation Theory: A First Course (1991), Lecture 6, §6.1, where the character of 𝕊_λ V is shown to be the Schur polynomial through Frobenius's formula, and Appendix A.1 for the Schur polynomials of the extreme shapes, s_{(d)} = h_d and s_{(1^d)} = e_d.
• I. G. Macdonald, Symmetric Functions and Hall Polynomials, 2nd ed., Chapter I, Section 7.

Every partition

@[simp]

theorem TauCeti.char_weylRepOfShape_ofPartition_diagonal (k : Type u) [Field k] [CharZero k] (n : ℕ) {d : ℕ} (μ : d.Partition) (t : Fin n → kˣ) : (weylRepOfShape k n (YoungDiagram.ofPartition μ)).character (diagGL t) = (MvPolynomial.eval fun (i : Fin n) => ↑(t i)) (schurPoly (Fin n) k μ)

The character of the Weyl module of a partition is its Schur polynomial: for a partition μ of d, the character of 𝕊^μ(kⁿ) at the diagonal matrix diag t is s_μ(t₀, …, t_{n-1}). When μ has more than n parts both sides vanish.

@[simp]

theorem TauCeti.char_weylFDRepOfShape_ofPartition_diagonal (k : Type u) [Field k] [CharZero k] (n : ℕ) {d : ℕ} (μ : d.Partition) (t : Fin n → kˣ) : (weylFDRepOfShape k n (YoungDiagram.ofPartition μ)).character (diagGL t) = (MvPolynomial.eval fun (i : Fin n) => ↑(t i)) (schurPoly (Fin n) k μ)

The character of the bundled Weyl module of a partition is its Schur polynomial, evaluated at the diagonal entries.

theorem TauCeti.char_weylRepOfShape_diagonal_eq_eval_diagramSchurPoly (k : Type u) [Field k] [CharZero k] (n : ℕ) (μ : YoungDiagram) (t : Fin n → kˣ) : (weylRepOfShape k n μ).character (diagGL t) = (MvPolynomial.eval fun (i : Fin n) => ↑(t i)) (diagramSchurPoly n k μ)

The character of the Weyl module of any Young diagram is its Schur polynomial, evaluated at the diagonal entries.

theorem TauCeti.char_weylFDRepOfShape_diagonal_eq_eval_diagramSchurPoly (k : Type u) [Field k] [CharZero k] (n : ℕ) (μ : YoungDiagram) (t : Fin n → kˣ) : (weylFDRepOfShape k n μ).character (diagGL t) = (MvPolynomial.eval fun (i : Fin n) => ↑(t i)) (diagramSchurPoly n k μ)

The character of the bundled Weyl module of any Young diagram is its Schur polynomial, evaluated at the diagonal entries.

theorem TauCeti.finrank_weylModuleOfShape (k : Type u) [Field k] [CharZero k] (n : ℕ) (μ : YoungDiagram) : Module.finrank k ↥(weylModuleOfShape k n μ).toSubmodule = Nat.card (BoundedSSYT n μ)

The dimension of the Weyl module of a Young diagram μ is the number of semistandard tableaux of shape μ in the alphabet {0, …, n - 1}: the character at the identity is the dimension, and the Schur polynomial of the partition with diagram μ counts those tableaux at one. When μ has more than n rows both sides vanish.