Differentiating weight vectors of a rational representation of GL n

A rational representation ρ of GL n ℂ differentiates to a representation dρ = TauCeti.IsRationalRep.differential of the matrix Lie algebra 𝔤𝔩ₙ(ℂ). This file computes dρ on the two kinds of vectors the group-level highest-weight theory produces, so that a highest weight vector of ρ (TauCeti.IsRationalRep.exists_highestWeightVector) is one of dρ as well:

• a weight vector w of weight l : Fin n → ℤ, on which every diagonal matrix diag(t) acts by ∏ᵢ tᵢ ^ lᵢ, is an eigenvector of every diagonal matrix diag(a) in 𝔤𝔩ₙ, with eigenvalue ∑ᵢ aᵢ lᵢ: the group character t ↦ ∏ᵢ tᵢ ^ lᵢ differentiates to the linear functional diag(a) ↦ ∑ᵢ lᵢ aᵢ on the diagonal Cartan subalgebra;
• a vector fixed by the root subgroup c ↦ xᵢⱼ(c) = 1 + c Eᵢⱼ is killed by the root vector Eᵢⱼ.

The argument

Both statements restrict the comodule of ρ along a one-parameter subgroup of GLₙ and differentiate there, using that the differential commutes with restriction (TauCeti.Comodule.differential_corestrict).

For the root vector the subgroup is the root subgroup xᵢⱼ : 𝔾ₐ → GLₙ, whose differential is Eᵢⱼ (TauCeti.GeneralLinear.tangentMatrix_derivationComp_rootSubgroup). A vector fixed by every complex point of 𝔾ₐ is fixed by its coaction, the coordinate ring of 𝔾ₐ being reduced and of finite type over the algebraically closed field ℂ (TauCeti.Comodule.coact_eq_tmul_one_iff_forall_basePointsRepresentation_eq), and a fixed vector of a comodule is killed by every tangent vector.

For the diagonal the subgroup is the cocharacter 𝔾ₘ → GLₙ, t ↦ diag(1, …, t, …, 1) with t in place i, whose differential is Eᵢᵢ (TauCeti.GeneralLinear.tangentMatrix_derivationComp_weightCocharacter). Pairing with a linear functional φ, the matrix coefficient of w along it is a Laurent polynomial which agrees with φ(w) Tˡⁱ at every complex point, hence equals it, and the tangent vector d/dT at T = 1 takes it to lᵢ φ(w).

Main results

• TauCeti.IsRationalRep.differential_single_self_apply_of_mem_weightSpace: on a vector of weight l, the matrix unit Eᵢᵢ acts by the scalar lᵢ.
• TauCeti.IsRationalRep.differential_diagonal_apply_of_mem_weightSpace: on a vector of weight l, the diagonal matrix diag(a) acts by the scalar ∑ᵢ aᵢ lᵢ.
• TauCeti.IsRationalRep.differential_single_apply_eq_zero: a vector fixed by the root subgroup xᵢⱼ is killed by Eᵢⱼ.
• TauCeti.IsRationalRep.isGlHighestWeightVector_differential: a highest weight vector for the transvections is a highest weight vector for 𝔤𝔩ₙ through the differential.
• TauCeti.IsRationalRep.nonempty_lieModuleEquiv_glIrreducible: an irreducible rational representation with a highest weight vector of dominant weight λ differentiates to the named irreducible 𝔤𝔩ₙ-module TauCeti.glIrreducible n λ.
• TauCeti.nonempty_lieModuleEquiv_glIrreducible_rowLen_iff: Young diagrams with at most n rows are determined by the isomorphism classes of their named irreducibles.

References

• J. C. Jantzen, Representations of Algebraic Groups, Part I, Chapter 7.
• W. Fulton and J. Harris, Representation Theory: A First Course (1991), Lecture 15.

theorem TauCeti.IsRationalRep.differential_single_apply_eq_zero {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (hρ : IsRationalRep ρ) {i j : Fin n} (hij : i ≠ j) {w : W} (hw : ∀ (c : ℂ), (ρ (transvectionUnit hij c)) w = w) : (hρ.differential (Matrix.single i j 1)) w = 0

A vector fixed by a root subgroup is killed by its root vector: if every transvection xᵢⱼ(c) = 1 + c Eᵢⱼ fixes w, then the differential of ρ sends w to zero along Eᵢⱼ.

theorem TauCeti.IsRationalRep.differential_single_self_apply_of_mem_weightSpace {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (hρ : IsRationalRep ρ) {l : Fin n → ℤ} {w : W} (hw : w ∈ weightSpace ρ l) (i : Fin n) : (hρ.differential (Matrix.single i i 1)) w = ↑(l i) • w

A weight vector is an eigenvector of each diagonal matrix unit: if every diagonal matrix diag(t) acts on w by ∏ₖ tₖ ^ lₖ, then Eᵢᵢ acts on w through the differential of ρ by the scalar lᵢ.

theorem TauCeti.IsRationalRep.differential_diagonal_apply_of_mem_weightSpace {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (hρ : IsRationalRep ρ) {l : Fin n → ℤ} {w : W} (hw : w ∈ weightSpace ρ l) (a : Fin n → ℂ) : (hρ.differential (Matrix.diagonal a)) w = (∑ k : Fin n, a k * ↑(l k)) • w

A weight differentiates to a linear functional on the diagonal Cartan subalgebra: if every diagonal matrix diag(t) acts on w by ∏ₖ tₖ ^ lₖ, then diag(a) acts on w through the differential of ρ by the scalar ∑ₖ aₖ lₖ.

theorem TauCeti.IsRationalRep.isGlHighestWeightVector_differential {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (hρ : IsRationalRep ρ) {l : Fin n → ℤ} {w : W} (hw0 : w ≠ 0) (hwl : w ∈ weightSpace ρ l) (hw : ∀ (i j : Fin n) (hij : i < j) (c : ℂ), (ρ (transvectionUnit ⋯ c)) w = w) : IsGlHighestWeightVector (fun (k : Fin n) => ↑(l k)) w

A highest weight vector differentiates to a highest weight vector: a nonzero vector of weight l fixed by every transvection xᵢⱼ(c) with i < j is a highest weight vector of weight l for 𝔤𝔩ₙ(ℂ) through the differential of ρ.

theorem TauCeti.IsRationalRep.nonempty_lieModuleEquiv_glIrreducible {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (hρ : IsRationalRep ρ) [ρ.IsIrreducible] {l : DominantWeight n} {w : W} (hw0 : w ≠ 0) (hwl : w ∈ weightSpace ρ ↑l) (hw : ∀ (i j : Fin n) (hij : i < j) (c : ℂ), (ρ (transvectionUnit ⋯ c)) w = w) : Nonempty (W ≃ₗ⁅ℂ,Matrix (Fin n) (Fin n) ℂ⁆ glIrreducible n fun (i : Fin n) => ↑(↑l i))

An irreducible rational representation differentiates to the named irreducible 𝔤𝔩ₙ-module of its highest weight: if ρ is irreducible and has a highest weight vector of dominant weight λ (a nonzero vector of weight λ fixed by every transvection xᵢⱼ(c) with i < j), then W with the action of 𝔤𝔩ₙ(ℂ) through dρ is isomorphic to glIrreducible n λ.

theorem TauCeti.nonempty_lieModuleEquiv_glIrreducible_rowLen_iff {n : ℕ} {K : Type u_1} [Field K] [CharZero K] {μ ν : YoungDiagram} (hμ : μ.colLen 0 ≤ n) (hν : ν.colLen 0 ≤ n) : Nonempty ((glIrreducible n fun (i : Fin n) => ↑(μ.rowLen ↑i)) ≃ₗ⁅K,Matrix (Fin n) (Fin n) K⁆ glIrreducible n fun (i : Fin n) => ↑(ν.rowLen ↑i)) ↔ μ = ν

The named irreducibles of Young diagrams with at most n rows are pairwise non-isomorphic: for such diagrams μ and ν, the 𝔤𝔩ₙ-modules glIrreducible n μ and glIrreducible n ν are isomorphic exactly when μ = ν. This is the Lie counterpart of TauCeti.nonempty_equiv_rationalWeylRep_iff.