Weights of the diagonal torus of the general linear group

A vector w of a representation ρ of GL n k has weight l : Fin n → ℤ when every invertible diagonal matrix diagGL t scales it by ∏ i, tᵢ ^ lᵢ. The vectors of weight l form the weight space TauCeti.weightSpace ρ l, and this file builds that space and the two facts that make weights a decomposition rather than a labelling: the weight spaces are independent, and the standard representation is the internal direct sum of its weight spaces, which are its coordinate lines.

The scalar ∏ i, tᵢ ^ lᵢ is the split-torus character TauCeti.weightChar k l, built in TauCeti.LinearAlgebra.Basis.DiagonalTorus.Basic. The weight space is an intersection of eigenspaces, one for each point of the torus, so independence is that of the joint eigenspaces of a representation indexed by characters — TauCeti.iSupIndep_iInf_eigenspace_unitHom — transported along l ↦ TauCeti.weightChar k l. That transport needs the map to be injective, and that is where the coefficients enter: over 𝔽₂ the torus is trivial (TauCeti.diagonalTorus_eq_bot), every l gives the same character, and the whole module is a weight space for every weight at once, so nothing is independent. Rather than fix the coefficients, every statement below that separates weights takes Function.Injective (weightChar k) as a hypothesis. TauCeti.weightChar_injective discharges it over an infinite field, and TauCeti.weightChar_injective_of_algebraRat over a field that is a ℚ-algebra.

The definitions themselves need only a commutative ring, and are stated there.

Main definitions

• TauCeti.weightSpace: the space of vectors on which the diagonal torus acts through TauCeti.weightChar.

Main results

• TauCeti.iSupIndep_weightSpace: the weight spaces of a representation of GL n k are independent, as soon as distinct weights give distinct characters.
• TauCeti.weightSpace_stdRep_single and TauCeti.weightSpace_stdRep_eq_bot: the weight spaces of the standard representation are exactly its coordinate lines, the line k ∙ eᵢ carrying the weight Pi.single i 1 and every other weight space vanishing.
• TauCeti.isInternal_weightSpace_of_iSup_eq_top: a representation whose weight spaces span it is their internal direct sum, as soon as distinct weights give distinct characters.
• TauCeti.isInternal_weightSpace_stdRep: the standard representation is the internal direct sum of its weight spaces.
• TauCeti.weightSpace_detPowerRep: all of det ^ m has the constant weight m, that is, its weight space at the constant sequence m is ⊤. Over a general commutative ring this says nothing about the other weight spaces — over 𝔽₂ all of them are ⊤ as well.
• TauCeti.map_weightSpace_le_of_commute: an operator commuting with the torus action preserves every weight space, so when the ambient representation is the internal direct sum of its weight spaces, a subrepresentation the operator cuts out inherits that decomposition.
• Subrepresentation.weightSpace_toRepresentation: the weight spaces of a subrepresentation are the traces of the ambient ones, with Subrepresentation.weightSpace_toRepresentation_eq_bot_iff giving the criterion for a weight not to occur in the subrepresentation.
• Representation.IntertwiningMap.map_weightSpace_le and Representation.Equiv.map_weightSpace: intertwining maps preserve weights, and an equivalence of representations matches their weight spaces, so that the weights of a representation are an isomorphism invariant (Representation.Equiv.weightSpace_eq_bot_iff).
• TauCeti.eq_of_forall_sum_filter_lt_le and Representation.Equiv.eq_of_forall_sum_filter_lt_le: the dominance order on integer weights is antisymmetric, and hence a highest weight is an isomorphism invariant.

Implementation notes

The weight space is indexed by l : Fin n → ℤ, not by a character of the torus, because that is the index the highest-weight theory runs on; TauCeti.weightChar is the translation between the two, and the separation hypothesis says the translation is faithful.

The intersection defining TauCeti.weightSpace runs over t : Fin n → kˣ rather than over TauCeti.diagonalTorus k n itself: TauCeti.diagGL is onto the torus (TauCeti.mem_diagonalTorus_iff_exists_diagGL), so the two conditions agree, and the coordinatewise form is the one every computation below uses.

Weight spaces are intersections of honest eigenspaces, not of generalised ones: a torus element acts on a weight vector by an honest scalar, and independence is available in that form already.

References

• W. Fulton and J. Harris, Representation Theory: A First Course (1991), Lecture 15.

The weight spaces of a representation

def TauCeti.weightSpace {k : Type u} [CommRing k] {n : ℕ} {W : Type v} [AddCommGroup W] [Module k W] (ρ : Representation k (GL (Fin n) k) W) (l : Fin n → ℤ) : Submodule k W

The weight space of weight l : Fin n → ℤ: the vectors that every invertible diagonal matrix diagGL t scales by ∏ i, tᵢ ^ lᵢ.

@[simp]

theorem TauCeti.mem_weightSpace_iff {k : Type u} [CommRing k] {n : ℕ} {W : Type v} [AddCommGroup W] [Module k W] (ρ : Representation k (GL (Fin n) k) W) (l : Fin n → ℤ) (w : W) : w ∈ weightSpace ρ l ↔ ∀ (t : Fin n → kˣ), (ρ (diagGL t)) w = ↑((weightChar k l) t) • w

Membership in a weight space is the eigen-relation at every point of the torus.

theorem TauCeti.weightSpace_le_eigenspace {k : Type u} [CommRing k] {n : ℕ} {W : Type v} [AddCommGroup W] [Module k W] (ρ : Representation k (GL (Fin n) k) W) (l : Fin n → ℤ) (t : Fin n → kˣ) : weightSpace ρ l ≤ Module.End.eigenspace (ρ (diagGL t)) ↑((weightChar k l) t)

A weight vector is an eigenvector for each individual point of the torus.

theorem TauCeti.apply_of_mem_weightSpace {k : Type u} [CommRing k] {n : ℕ} {W : Type v} [AddCommGroup W] [Module k W] {ρ : Representation k (GL (Fin n) k) W} {l : Fin n → ℤ} {w : W} (hw : w ∈ weightSpace ρ l) (t : Fin n → kˣ) : (ρ (diagGL t)) w = ↑((weightChar k l) t) • w

The action of a torus element on a weight vector.

theorem TauCeti.apply_scalar_of_mem_weightSpace {k : Type u} [CommRing k] {n : ℕ} {W : Type v} [AddCommGroup W] [Module k W] {ρ : Representation k (GL (Fin n) k) W} {l : Fin n → ℤ} {w : W} (hw : w ∈ weightSpace ρ l) (z : kˣ) : (ρ ((Matrix.GeneralLinearGroup.scalar (Fin n)) z)) w = ↑(z ^ ∑ i : Fin n, l i) • w

A scalar matrix acts on a weight vector by the scalar raised to the weight's coordinate sum.

theorem TauCeti.map_weightSpace_le_of_commute {k : Type u} [CommRing k] {n : ℕ} {W : Type v} [AddCommGroup W] [Module k W] {ρ : Representation k (GL (Fin n) k) W} (l : Fin n → ℤ) {φ : Module.End k W} (hφ : ∀ (t : Fin n → kˣ), Commute φ (ρ (diagGL t))) : Submodule.map φ (weightSpace ρ l) ≤ weightSpace ρ l

An operator commuting with the torus action preserves every weight space. A weight space is a joint eigenspace of the torus, and an operator commuting with an endomorphism carries each of its eigenvectors to an eigenvector of the same eigenvalue.

The operator therefore acts on each weight space separately, which is how a subrepresentation cut out of W by such an operator inherits a weight decomposition of W — when W has one, that is; the statement itself says nothing about whether the weight spaces of W span it or are independent.

The weight spaces of a subrepresentation

theorem Subrepresentation.weightSpace_toRepresentation {k : Type u} [CommRing k] {n : ℕ} {W : Type v} [AddCommGroup W] [Module k W] {ρ : Representation k (GL (Fin n) k) W} (S : Subrepresentation ρ) (l : Fin n → ℤ) : TauCeti.weightSpace S.toRepresentation l = Submodule.comap S.toSubmodule.subtype (TauCeti.weightSpace ρ l)

The weight spaces of a subrepresentation are the traces of the ambient ones: a vector of a subrepresentation has weight l exactly when it has weight l in the ambient representation, the torus acting on it by the same scalar either way.

theorem Subrepresentation.weightSpace_toRepresentation_eq_bot_iff {k : Type u} [CommRing k] {n : ℕ} {W : Type v} [AddCommGroup W] [Module k W] {ρ : Representation k (GL (Fin n) k) W} (S : Subrepresentation ρ) (l : Fin n → ℤ) : TauCeti.weightSpace S.toRepresentation l = ⊥ ↔ S.toSubmodule ⊓ TauCeti.weightSpace ρ l = ⊥

A subrepresentation has no vector of weight l exactly when it meets the ambient weight space trivially. This is the form in which a weight is ruled out for a subrepresentation cut out of a weight-decomposed module.

theorem Representation.IntertwiningMap.map_weightSpace_le {k : Type u} [CommRing k] {n : ℕ} {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] {ρ : Representation k (GL (Fin n) k) V} {σ : Representation k (GL (Fin n) k) W} (f : ρ.IntertwiningMap σ) (l : Fin n → ℤ) : Submodule.map f.toLinearMap (TauCeti.weightSpace ρ l) ≤ TauCeti.weightSpace σ l

An intertwining map carries vectors of weight l to vectors of weight l: it commutes with every torus element, so it maps each joint eigenvector to a joint eigenvector with the same eigenvalues.

theorem Representation.IntertwiningMap.iSup_weightSpace_eq_top_of_surjective {k : Type u} [CommRing k] {n : ℕ} {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] {ρ : Representation k (GL (Fin n) k) V} {σ : Representation k (GL (Fin n) k) W} (f : ρ.IntertwiningMap σ) (hf : Function.Surjective ⇑f) (hρ : ⨆ (l : Fin n → ℤ), TauCeti.weightSpace ρ l = ⊤) : ⨆ (l : Fin n → ℤ), TauCeti.weightSpace σ l = ⊤

Integer weight spaces spanning a representation also span any equivariant quotient.

theorem TauCeti.eq_of_forall_sum_filter_lt_le {n : ℕ} {a b : Fin n → ℤ} (hab : ∀ (m : ℕ), ∑ j : Fin n with ↑j < m, a j ≤ ∑ j : Fin n with ↑j < m, b j) (hba : ∀ (m : ℕ), ∑ j : Fin n with ↑j < m, b j ≤ ∑ j : Fin n with ↑j < m, a j) : a = b

The dominance order on integer vectors is antisymmetric: two vectors each of whose partial sums ∑_{j < m} bounds the other's agree.

theorem Representation.Equiv.map_weightSpace {k : Type u} [CommRing k] {n : ℕ} {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] {ρ : Representation k (GL (Fin n) k) V} {σ : Representation k (GL (Fin n) k) W} (e : ρ.Equiv σ) (l : Fin n → ℤ) : Submodule.map (↑e.toLinearEquiv) (TauCeti.weightSpace ρ l) = TauCeti.weightSpace σ l

An equivalence of representations of GL n k carries each weight space onto the weight space of the same weight, so isomorphic representations have the same weights, with the same multiplicities.

theorem Representation.Equiv.weightSpace_eq_bot_iff {k : Type u} [CommRing k] {n : ℕ} {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] {ρ : Representation k (GL (Fin n) k) V} {σ : Representation k (GL (Fin n) k) W} (e : ρ.Equiv σ) (l : Fin n → ℤ) : TauCeti.weightSpace ρ l = ⊥ ↔ TauCeti.weightSpace σ l = ⊥

Isomorphic representations of GL n k have the same weights: a weight space of one vanishes exactly when the corresponding weight space of the other does.

theorem Representation.Equiv.eq_of_forall_sum_filter_lt_le {k : Type u} [CommRing k] {n : ℕ} {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] {ρ : Representation k (GL (Fin n) k) V} {σ : Representation k (GL (Fin n) k) W} (e : ρ.Equiv σ) {a b : Fin n → ℤ} (ha : TauCeti.weightSpace ρ a ≠ ⊥) (hρ : ∀ (l : Fin n → ℤ), TauCeti.weightSpace ρ l ≠ ⊥ → ∀ (m : ℕ), ∑ j : Fin n with ↑j < m, l j ≤ ∑ j : Fin n with ↑j < m, a j) (hb : TauCeti.weightSpace σ b ≠ ⊥) (hσ : ∀ (l : Fin n → ℤ), TauCeti.weightSpace σ l ≠ ⊥ → ∀ (m : ℕ), ∑ j : Fin n with ↑j < m, l j ≤ ∑ j : Fin n with ↑j < m, b j) : a = b

A highest weight is an isomorphism invariant. If the weight a occurs in ρ and dominates every weight of ρ, and b plays the same role for σ, then a representation equivalence e : ρ ≃ σ forces a = b.

The standard representation and the determinant powers

theorem TauCeti.basisFun_mem_weightSpace_stdRep {k : Type u} [CommRing k] {n : ℕ} (i : Fin n) : (Pi.basisFun k (Fin n)) i ∈ weightSpace (stdRep k n) (Pi.single i 1)

The i-th standard basis vector has weight Pi.single i 1: a diagonal matrix scales it by its i-th entry.

theorem TauCeti.span_basisFun_le_weightSpace_stdRep {k : Type u} [CommRing k] {n : ℕ} (i : Fin n) : k ∙ (Pi.basisFun k (Fin n)) i ≤ weightSpace (stdRep k n) (Pi.single i 1)

The coordinate line k ∙ eᵢ consists of vectors of weight Pi.single i 1.

theorem TauCeti.iSup_weightSpace_stdRep_eq_top {k : Type u} [CommRing k] {n : ℕ} : ⨆ (l : Fin n → ℤ), weightSpace (stdRep k n) l = ⊤

The weight spaces of the standard representation span it, being its coordinate lines.

@[simp]

theorem TauCeti.weightSpace_detPowerRep {k : Type u} [CommRing k] {n : ℕ} (m : ℤ) : (weightSpace (detPowerRep k n m) fun (x : Fin n) => m) = ⊤

All of det ^ m has weight the constant sequence m: a diagonal matrix acts on it by the m-th power of the product of its entries. Over a commutative ring this leaves the other weight spaces of det ^ m unconstrained — over 𝔽₂ the torus is trivial, so every one of them is ⊤ too.

The weight spaces of the standard representation

Here the coefficients must separate weights, in the sense that l ↦ weightChar k l is injective; TauCeti.weightChar_injective supplies that over an infinite field.

theorem TauCeti.eq_single_of_mem_weightSpace_stdRep {k : Type u} [CommRing k] [IsDomain k] {n : ℕ} (hchar : Function.Injective (weightChar k)) {l : Fin n → ℤ} {w : Fin n → k} (hw : w ∈ weightSpace (stdRep k n) l) {j : Fin n} (hj : w j ≠ 0) : l = Pi.single j 1

A nonzero coordinate pins the weight. If a vector of weight l in the standard representation has a nonzero j-th coordinate then l = Pi.single j 1.

theorem TauCeti.weightSpace_stdRep_eq_bot {k : Type u} [CommRing k] [IsDomain k] {n : ℕ} (hchar : Function.Injective (weightChar k)) {l : Fin n → ℤ} (hl : ∀ (i : Fin n), l ≠ Pi.single i 1) : weightSpace (stdRep k n) l = ⊥

Off the weights Pi.single i 1 the standard representation has no weight vectors.

theorem TauCeti.weightSpace_stdRep_single {k : Type u} [CommRing k] [IsDomain k] {n : ℕ} (hchar : Function.Injective (weightChar k)) (i : Fin n) : weightSpace (stdRep k n) (Pi.single i 1) = k ∙ (Pi.basisFun k (Fin n)) i

The weight spaces of the standard representation are its coordinate lines.

theorem TauCeti.iSupIndep_weightSpace {k : Type u} [Field k] {n : ℕ} {W : Type v} [AddCommGroup W] [Module k W] (hchar : Function.Injective (weightChar k)) (ρ : Representation k (GL (Fin n) k) W) : iSupIndep fun (l : Fin n → ℤ) => weightSpace ρ l

The weight spaces of a representation of GL n k are independent, as soon as distinct weights give distinct characters of the torus. The weight spaces are the joint eigenspaces of the representation t ↦ ρ (diagGL t) of the torus indexed by the characters weightChar k l, and those are independent; the hypothesis makes the weight recoverable from its character, so indexing by weights keeps them distinct.

theorem TauCeti.isInternal_weightSpace_of_iSup_eq_top {k : Type u} [Field k] {n : ℕ} {W : Type v} [AddCommGroup W] [Module k W] (hchar : Function.Injective (weightChar k)) {ρ : Representation k (GL (Fin n) k) W} (h : ⨆ (l : Fin n → ℤ), weightSpace ρ l = ⊤) : DirectSum.IsInternal fun (l : Fin n → ℤ) => weightSpace ρ l

Spanning is the whole of the weight-space decomposition. Once distinct weights give distinct characters, the weight spaces are independent for free, so a representation whose weight spaces span it is their internal direct sum.

theorem TauCeti.isInternal_weightSpace_stdRep {k : Type u} [Field k] {n : ℕ} (hchar : Function.Injective (weightChar k)) : DirectSum.IsInternal fun (l : Fin n → ℤ) => weightSpace (stdRep k n) l

The standard representation is the internal direct sum of its weight spaces: the weight-space decomposition in its smallest instance.