The Schur-Weyl decomposition of the character of a tensor power

The symmetric group S_d and the general linear group GL n k act on the tensor power (kⁿ)^{⊗d} with commuting actions, and Schur-Weyl duality decomposes it under their product as

(kⁿ)^{⊗d} ≅ ⊕_{μ ⊢ d} S^μ ⊗ 𝕊^μ(kⁿ),

with S^μ the Specht module and 𝕊^μ(kⁿ) the Weyl module. This file proves the shadow of that decomposition on characters of GL n k, over a field k of characteristic zero: for every g ∈ GL n k,

char (kⁿ)^{⊗d} (g) = ∑_{μ ⊢ d} f^μ · char 𝕊^μ(kⁿ) (g),

where f^μ = dim S^μ, and at g = 1 the dimension count n^d = ∑_{μ ⊢ d} f^μ · dim 𝕊^μ(kⁿ). Only the partitions with at most n parts contribute, the other Weyl modules being zero (TauCeti.weylModuleOfShape_eq_bot_iff).

The route is through the Specht characters χ^μ. The character of the Weyl module 𝕊_t(kⁿ) = c_t · (kⁿ)^{⊗d} of a μ-tableau t is f^μ / d! times the pairing of the coefficients of the Young symmetrizer c_t with the class function σ ↦ tr(σ ∘ g^{⊗d}) of S_d (TauCeti.YoungTableau.char_weylRep_eq_sum), and pairing c_t with a class function is pairing χ^μ with it up to the factor f^μ (TauCeti.YoungTableau.sum_char_spechtSubrepresentation_smul). So

char 𝕊^μ(kⁿ) (g) = (1 / d!) · ∑_{σ ∈ S_d} χ^μ(σ) · tr(σ ∘ g^{⊗d}),

which on the diagonal torus is the Frobenius-characteristic expression (1 / d!) · ∑_σ χ^μ(σ) · p_{ρ(σ)}(x) in the power sums. Summing against the degrees f^μ, column orthogonality against the identity class (TauCeti.sum_finrank_spechtModule_mul_spechtChar) leaves only σ = 1, whose term is the character of the tensor power.

That the character of 𝕊^μ(kⁿ) on the torus is the Schur polynomial s_μ is the identity (1 / d!) · ∑_σ χ^μ(σ) · p_{ρ(σ)} = s_μ of Frobenius (TauCeti.sum_spechtChar_smul_psumPart); the conclusion is drawn in TauCeti/RepresentationTheory/ClassicalGroups/WeylModule/Character.lean (TauCeti.char_weylRepOfShape_ofPartition_diagonal).

Main results

• TauCeti.YoungTableau.char_weylRep_eq_sum_character: the character of the Weyl module of a tableau as the pairing of the Specht character with traces on the tensor power.
• TauCeti.char_weylRepOfShape_ofPartition_eq_sum_spechtChar: the same for the Weyl module of a partition, with the integer character χ^μ of S_d.
• TauCeti.char_weylRepOfShape_ofPartition_diagonal_eq_sum_spechtChar: the character of 𝕊^μ(kⁿ) on the diagonal torus is (1 / d!) · ∑_σ χ^μ(σ) · p_{ρ(σ)}.
• TauCeti.sum_finrank_spechtModule_mul_char_weylRepOfShape_ofPartition: the character of (kⁿ)^{⊗d} is ∑_{μ ⊢ d} f^μ · char 𝕊^μ(kⁿ).
• TauCeti.char_weylFDRepOfShape_ofPartition_eq_sum_spechtChar, TauCeti.char_weylFDRepOfShape_ofPartition_diagonal_eq_sum_spechtChar and TauCeti.sum_finrank_spechtModule_mul_char_weylFDRepOfShape_ofPartition: the bundled forms of the last three, for TauCeti.weylFDRepOfShape and TauCeti.tensorPowerFDRep.
• TauCeti.sum_finrank_spechtModule_mul_finrank_weylModuleOfShape: ∑_{μ ⊢ d} f^μ · dim 𝕊^μ(kⁿ) = n^d.

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.

theorem TauCeti.YoungTableau.char_weylRep_eq_sum_character {k : Type u} [Field k] [CharZero k] {n : ℕ} {μ : YoungDiagram} (t : YoungTableau μ) (g : GL (Fin n) k) : (weylRep k n t).character g = (↑μ.card.factorial)⁻¹ * ∑ σ : Equiv.Perm (Fin μ.card), (spechtSubrepresentation μ).toRepresentation.character σ • (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 through the Specht character. For a μ-tableau t with d cells and g ∈ GL n k,

char 𝕊_t(kⁿ) (g) = (1 / d!) · ∑_{σ ∈ S_d} χ^μ(σ) · tr(σ ∘ g^{⊗d}),

where χ^μ is the character of the Specht module S^μ.

theorem TauCeti.char_weylRepOfShape_ofPartition_eq_sum_spechtChar {k : Type u} [Field k] [CharZero k] {n d : ℕ} (μ : d.Partition) (g : GL (Fin n) k) : (weylRepOfShape k n (YoungDiagram.ofPartition μ)).character g = (↑d.factorial)⁻¹ * ∑ σ : Equiv.Perm (Fin d), spechtChar μ σ • (LinearMap.trace k (PiTensorProduct k fun (x : Fin d) => Fin n → k)) ((permTensorAction k n d) σ * (tensorPowerRep k n d) g)

The character of the Weyl module of a partition through the Specht character. For a partition μ of d and g ∈ GL n k,

char 𝕊^μ(kⁿ) (g) = (1 / d!) · ∑_{σ ∈ S_d} χ^μ(σ) · tr(σ ∘ g^{⊗d}).

theorem TauCeti.char_weylFDRepOfShape_ofPartition_eq_sum_spechtChar {k : Type u} [Field k] [CharZero k] {n d : ℕ} (μ : d.Partition) (g : GL (Fin n) k) : (weylFDRepOfShape k n (YoungDiagram.ofPartition μ)).character g = (↑d.factorial)⁻¹ * ∑ σ : Equiv.Perm (Fin d), spechtChar μ σ • (LinearMap.trace k (PiTensorProduct k fun (x : Fin d) => Fin n → k)) ((permTensorAction k n d) σ * (tensorPowerRep k n d) g)

The character of the bundled Weyl module of a partition through the Specht character: the FDRep form of TauCeti.char_weylRepOfShape_ofPartition_eq_sum_spechtChar.

theorem TauCeti.char_weylRepOfShape_ofPartition_diagonal_eq_sum_spechtChar {k : Type u} [Field k] [CharZero k] {n d : ℕ} (μ : d.Partition) (x : Fin n → kˣ) : (weylRepOfShape k n (YoungDiagram.ofPartition μ)).character (diagGL x) = (↑d.factorial)⁻¹ * (MvPolynomial.eval fun (i : Fin n) => ↑(x i)) (∑ σ : Equiv.Perm (Fin d), spechtChar μ σ • MvPolynomial.psumPart (Fin n) k σ.partition)

The character of the Weyl module of a partition on the diagonal torus is the Frobenius-characteristic expression in the power sums: for a partition μ of d,

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

where ρ(σ) is the cycle type of σ.

theorem TauCeti.char_weylFDRepOfShape_ofPartition_diagonal_eq_sum_spechtChar {k : Type u} [Field k] [CharZero k] {n d : ℕ} (μ : d.Partition) (x : Fin n → kˣ) : (weylFDRepOfShape k n (YoungDiagram.ofPartition μ)).character (diagGL x) = (↑d.factorial)⁻¹ * (MvPolynomial.eval fun (i : Fin n) => ↑(x i)) (∑ σ : Equiv.Perm (Fin d), spechtChar μ σ • MvPolynomial.psumPart (Fin n) k σ.partition)

The character of the bundled Weyl module of a partition on the diagonal torus is the Frobenius-characteristic expression in the power sums: the FDRep form of TauCeti.char_weylRepOfShape_ofPartition_diagonal_eq_sum_spechtChar.

theorem TauCeti.sum_finrank_spechtModule_mul_char_weylRepOfShape_ofPartition {k : Type u} [Field k] [CharZero k] {n : ℕ} (d : ℕ) (g : GL (Fin n) k) : ∑ μ : d.Partition, ↑(Module.finrank ℚ ↑(spechtModule μ).V) * (weylRepOfShape k n (YoungDiagram.ofPartition μ)).character g = (tensorPowerRep k n d).character g

The Schur-Weyl decomposition of the character of a tensor power. For every g ∈ GL n k, the character of (kⁿ)^{⊗d} at g is the sum over the partitions μ of d of the characters of the Weyl modules 𝕊^μ(kⁿ) at g, each weighted by the dimension f^μ of the Specht module S^μ.

theorem TauCeti.sum_finrank_spechtModule_mul_char_weylFDRepOfShape_ofPartition {k : Type u} [Field k] [CharZero k] {n : ℕ} (d : ℕ) (g : GL (Fin n) k) : ∑ μ : d.Partition, ↑(Module.finrank ℚ ↑(spechtModule μ).V) * (weylFDRepOfShape k n (YoungDiagram.ofPartition μ)).character g = (tensorPowerFDRep k n d).character g

The Schur-Weyl decomposition of the character of the bundled tensor power: the FDRep form of TauCeti.sum_finrank_spechtModule_mul_char_weylRepOfShape_ofPartition.

theorem TauCeti.sum_finrank_spechtModule_mul_finrank_weylModuleOfShape (k : Type u) [Field k] [CharZero k] (n d : ℕ) : ∑ μ : d.Partition, Module.finrank ℚ ↑(spechtModule μ).V * Module.finrank k ↥(weylModuleOfShape k n (YoungDiagram.ofPartition μ)).toSubmodule = n ^ d

The Schur-Weyl dimension count: ∑_{μ ⊢ d} f^μ · dim 𝕊^μ(kⁿ) = n^d, where f^μ is the dimension of the Specht module S^μ.