The character of a Weyl module as a sum of power sums

The Weyl module 𝕊_t(kⁿ) = c_t · (kⁿ)^{⊗d} of a μ-tableau t is the image of the Young symmetrizer c_t acting on the tensor power by permuting tensor factors. This file computes its character on the diagonal torus of GL n k in terms of the coefficients of c_t and the power sums p_k = ∑ᵢ xᵢ^k:

char 𝕊_t(kⁿ) (diag x) = (f^μ / d!) · ∑_{σ ∈ S_d} c_t(σ) · p_{ρ(σ)}(x),

where ρ(σ) is the cycle type of σ, p_ρ = ∏ᵢ p_{ρᵢ}, and f^μ is the dimension of the Specht module ℚ[S_d] c_t.

Two facts combine. First, a permutation σ composed with a diagonal matrix diag x acting on (kⁿ)^{⊗d} has trace p_{ρ(σ)}(x): in the monomial basis e_f = e_{f 1} ⊗ ⋯ ⊗ e_{f d} the diagonal entry at e_f is ∏ⱼ x_{f j} when f is constant on the cycles of σ and zero otherwise, and summing over such f expands the product of power sums (TauCeti.psumPart_partition_eq_sum_prod_X). Second, c_t is essentially idempotent, c_t² = (d! / f^μ) c_t (TauCeti.YoungTableau.youngSymmetrizerOver_sq), and it commutes with the action of GL n k, so the trace of g on the image of c_t is f^μ / d! times the trace of c_t g on the whole tensor power (TauCeti.LinearMap.trace_mul_eq_mul_trace_restrict_range).

Every ingredient of the right-hand side lives in the symmetric group: the coefficients of c_t, the dimension f^μ, and the cycle types. So the classical statement that this character is the Schur polynomial s_μ becomes an identity about the symmetric group alone, between the Young symmetrizer and the power-sum expansion of s_μ. That identity is Frobenius's, and the conclusion is drawn in TauCeti/RepresentationTheory/ClassicalGroups/WeylModule/Character.lean (TauCeti.char_weylRepOfShape_ofPartition_diagonal).

Main results

• TauCeti.trace_permTensorAction_mul_tensorPowerRep_diagGL: the trace of a permutation of the tensor factors composed with a diagonal matrix is the power-sum product over the cycle type of the permutation.
• TauCeti.YoungTableau.char_weylRep_eq_sum: the character of a Weyl module at any element of GL n k, as a combination of traces on the tensor power weighted by the coefficients of the Young symmetrizer.
• TauCeti.YoungTableau.char_weylRep_diagonal: the character of a Weyl module on the diagonal torus is the power-sum expansion displayed above.
• TauCeti.char_weylRepOfShape_diagonal: the same for the Weyl module of a shape, with the Young symmetrizer of any tableau of that shape.

References

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

Permutations composed with diagonal matrices on the tensor power

theorem TauCeti.trace_permTensorAction_mul_tensorPowerRep_diagGL {k : Type u} [CommRing k] {n d : ℕ} (σ : Equiv.Perm (Fin d)) (x : Fin n → kˣ) : (LinearMap.trace k (PiTensorProduct k fun (x : Fin d) => Fin n → k)) ((permTensorAction k n d) σ * (tensorPowerRep k n d) (diagGL x)) = (MvPolynomial.eval fun (i : Fin n) => ↑(x i)) (MvPolynomial.psumPart (Fin n) k σ.partition)

The trace of a permutation of the tensor factors composed with a diagonal matrix is the product of power sums over the cycle type of the permutation, evaluated at the diagonal entries: tr(σ ∘ (diag x)^{⊗d}) = p_{ρ(σ)}(x). At σ = 1 this is the character of the tensor power on the torus, (x₁ + ⋯ + xₙ)^d.

The character of a Weyl module

theorem TauCeti.YoungTableau.char_weylRep_eq_sum {k : Type u} [Field k] [Algebra ℚ k] {n : ℕ} {μ : YoungDiagram} (t : YoungTableau μ) (g : GL (Fin n) k) : (weylRep k n t).character g = ↑(Module.finrank ℚ ↥t.spechtIdeal) / ↑μ.card.factorial * ∑ σ : Equiv.Perm (Fin μ.card), (youngSymmetrizerOver k t).coeff σ * (LinearMap.trace k (PiTensorProduct k fun (x : Fin μ.card) => Fin n → k)) ((permTensorAction k n μ.card) σ * (tensorPowerRep k n μ.card) g)

The character of a Weyl module at g is f^μ / d! times the sum, over the permutations σ of the tensor factors, of the coefficient of σ in the Young symmetrizer c_t times the trace of σ ∘ g^{⊗d} on the tensor power. Here f^μ is the dimension of the Specht module ℚ[S_d] c_t.

theorem TauCeti.YoungTableau.char_weylRep_diagonal {k : Type u} [Field k] [Algebra ℚ k] {n : ℕ} {μ : YoungDiagram} (t : YoungTableau μ) (x : Fin n → kˣ) : (weylRep k n t).character (diagGL x) = ↑(Module.finrank ℚ ↥t.spechtIdeal) / ↑μ.card.factorial * (MvPolynomial.eval fun (i : Fin n) => ↑(x i)) (∑ σ : Equiv.Perm (Fin μ.card), (youngSymmetrizerOver k t).coeff σ • MvPolynomial.psumPart (Fin n) k σ.partition)

The character of a Weyl module on the diagonal torus is a sum of power-sum products:

char 𝕊_t(kⁿ) (diag x) = (f^μ / d!) · ∑_σ c_t(σ) · p_{ρ(σ)}(x),

where c_t(σ) is the coefficient of σ in the Young symmetrizer, ρ(σ) is the cycle type of σ, and f^μ is the dimension of the Specht module ℚ[S_d] c_t.

theorem TauCeti.char_weylRepOfShape_diagonal {k : Type u} [Field k] [Algebra ℚ k] {n : ℕ} {μ : YoungDiagram} (t : YoungTableau μ) (x : Fin n → kˣ) : (weylRepOfShape k n μ).character (diagGL x) = ↑(Module.finrank ℚ ↥t.spechtIdeal) / ↑μ.card.factorial * (MvPolynomial.eval fun (i : Fin n) => ↑(x i)) (∑ σ : Equiv.Perm (Fin μ.card), (YoungTableau.youngSymmetrizerOver k t).coeff σ • MvPolynomial.psumPart (Fin n) k σ.partition)

The character of the Weyl module of a shape on the diagonal torus is the power-sum expansion of TauCeti.YoungTableau.char_weylRep_diagonal, computed with the Young symmetrizer of any tableau t of that shape.