The weight-space decomposition of a rational representation

A rational representation of GL n ℂ is the internal direct sum of its weight spaces: the diagonal torus is simultaneously diagonalizable on it, and every joint eigencharacter occurring in it is among the monomial characters t ↦ ∏ i, tᵢ ^ lᵢ of the torus. Which of those characters actually occur — equivalently, which weight spaces are nonzero — is not determined here; the decomposition is indexed by all of Fin n → ℤ. This file proves that (TauCeti.IsRationalRep.isInternal_weightSpace), completing the decomposition that TauCeti.RepresentationTheory.ClassicalGroups.Weight.Basic establishes only for the standard representation.

Rationality is what carries the argument, and it cannot be dropped: an abstract representation of the torus (ℂˣ)ⁿ on a finite-dimensional space need not be diagonalizable at all, and even a diagonalizable one has joint eigencharacters that are arbitrary homomorphisms (ℂˣ)ⁿ → ℂˣ, almost none of which is a monomial t ↦ ∏ tᵢ ^ lᵢ. Rationality forces both.

The proof is the Laurent expansion of the torus action. Restricted along TauCeti.diagGL, the matrix entries of ρ are Laurent functions on the torus (TauCeti.comp_diagGL_mem_laurentFunctions), so ρ (diagGL t) is a finite sum ∑_l (∏ i, tᵢ ^ lᵢ) • A l with coefficients A l in Module.End ℂ W that do not depend on t (TauCeti.IsRationalRep.exists_forall_diagGL_eq_sum_smul). Comparing the expansion of ρ (diagGL (s * t)) with that of ρ (diagGL s) ∘ ρ (diagGL t) and using the linear independence of distinct characters (TauCeti.linearIndependent_weightCharHom) identifies the coefficients term by term: ρ (diagGL s) acts on the image of A l by the character of l, so that image lies in the weight space of l (TauCeti.apply_mem_weightSpace_of_forall_diagGL_eq_sum_smul). Evaluating the expansion at t = 1 writes the identity as ∑_l A l, so every vector is a sum of weight vectors.

The tensor, symmetric and exterior powers of the standard representation are polynomial (TauCeti.isPolynomialRep_tensorPowerRep and its companions), hence rational (TauCeti.IsPolynomialRep.isRationalRep), so their decompositions are instances of the theorem below and are not restated as separate declarations.

The pinned roadmap signature carries [FiniteDimensional ℂ W] as well. It is dropped here: it is implied by TauCeti.IsRationalRep.finite, and an unused hypothesis on the statement would be both weaker and flagged by the linter.

Main results

• TauCeti.IsRationalRep.exists_forall_diagGL_eq_sum_smul: the Laurent expansion of a rational representation on the diagonal torus.
• TauCeti.apply_mem_weightSpace_of_forall_diagGL_eq_sum_smul: the coefficients of such an expansion take their values in the weight space of their exponent. This step mentions no rationality, so it is stated over an arbitrary infinite field; only the three results whose hypothesis is the ℂ-pinned TauCeti.IsRationalRep are stated over ℂ.
• TauCeti.IsRationalRep.iSup_weightSpace_eq_top and TauCeti.IsRationalRep.isInternal_weightSpace: a rational representation of GL n ℂ is the internal direct sum of its weight spaces.

References

• Classical groups roadmap, Layer 3, "The maximal torus and weight spaces".
• W. Fulton and J. Harris, Representation Theory: A First Course (1991), Lecture 15.
• R. Goodman and N. R. Wallach, Symmetry, Representations, and Invariants (2009), Section 1.5.

theorem TauCeti.IsRationalRep.exists_forall_diagGL_eq_sum_smul {n : ℕ} {W : Type u} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (h : IsRationalRep ρ) : ∃ (S : Finset (Fin n → ℤ)) (A : (Fin n → ℤ) → Module.End ℂ W), ∀ (t : Fin n → ℂˣ), ρ (diagGL t) = ∑ l ∈ S, (weightCharHom ℂ l) t • A l

The Laurent expansion of a rational representation on the diagonal torus. The action of diagGL t is a finite sum ∑ l ∈ S, (∏ i, tᵢ ^ lᵢ) • A l whose coefficients A l do not depend on t: the matrix entries of ρ restrict to Laurent functions on the torus, and a Laurent function is a finite combination of characters.

theorem TauCeti.apply_mem_weightSpace_of_forall_diagGL_eq_sum_smul {n : ℕ} {K : Type v} [Field K] [Infinite K] {W : Type u} [AddCommGroup W] [Module K W] {ρ : Representation K (GL (Fin n) K) W} {S : Finset (Fin n → ℤ)} {A : (Fin n → ℤ) → Module.End K W} (hA : ∀ (t : Fin n → Kˣ), ρ (diagGL t) = ∑ l ∈ S, (weightCharHom K l) t • A l) {l : Fin n → ℤ} (hl : l ∈ S) (w : W) : (A l) w ∈ weightSpace ρ l

The coefficients of a Laurent expansion take their values in the weight spaces. If the torus acts through a finite sum ∑ l ∈ S, (∏ i, tᵢ ^ lᵢ) • A l, then every value of A l is a weight vector of weight l. Nothing is claimed here about A l being idempotent, or acting as the identity on the weight space of l; only its image is located.

Nothing in this statement refers to rationality, so the base field is an arbitrary infinite field: the argument only needs distinct characters of the torus to stay linearly independent.

theorem TauCeti.IsRationalRep.iSup_weightSpace_eq_top {n : ℕ} {W : Type u} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (h : IsRationalRep ρ) : ⨆ (l : Fin n → ℤ), weightSpace ρ l = ⊤

The weight spaces of a rational representation span it. Evaluating the Laurent expansion at the identity of the torus writes the identity endomorphism as the sum of the expansion coefficients, and each of those takes its values in a weight space.

theorem TauCeti.IsRationalRep.isInternal_weightSpace {n : ℕ} {W : Type u} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (h : IsRationalRep ρ) : DirectSum.IsInternal fun (l : Fin n → ℤ) => weightSpace ρ l

The weight-space decomposition. A rational representation of GL n ℂ is the internal direct sum of its weight spaces: the diagonal torus is simultaneously diagonalizable on it, and the decomposition is indexed by the integer weights l, the summand at l being the joint eigenspace of the character t ↦ ∏ i, tᵢ ^ lᵢ. The sum runs over all of Fin n → ℤ; which weights actually occur — that is, for which l the summand is nonzero — is not part of the statement. The roadmap pins this statement as weightSpace_isInternal; it is named for its conclusion here, matching the standard- representation case TauCeti.isInternal_weightSpace_stdRep.