Documentation

TauCeti.RepresentationTheory.ClassicalGroups.Weight.HighestWeight

Highest weight vectors of a rational representation of GL n #

A rational representation of GL n ℂ is the internal direct sum of its weight spaces (TauCeti.IsRationalRep.isInternal_weightSpace), so it has only finitely many weights (TauCeti.finite_setOf_weightSpace_ne_bot). This file produces a highest weight vector out of them: a nonzero weight vector, of a dominant weight, annihilated by the raising operators in the sense that every transvection xᵢⱼ(c) with i < j fixes it.

That is the group-level form of a vector killed by the positive nilradical, and it is the step the highest-weight classification of the irreducible rational representations of GL n rests on: the line it produces is the line a highest weight module is generated by.

Transvections raise weights #

Everything rests on one computation. Conjugating the transvection xᵢⱼ(c) by a diagonal matrix rescales its parameter by the value tᵢ tⱼ⁻¹ of the root εᵢ - εⱼ (TauCeti.diagGL_mul_transvectionUnit_mul_inv), so if w has weight l then xᵢⱼ(c) w transforms under the torus exactly as an expansion in the weights l + m (εᵢ - εⱼ) does.

Turning that into an identification of the individual terms needs the dependence on c to be polynomial, and this is where rationality enters and cannot be dropped: the transvection has determinant one and entries affine in c, so each matrix entry of ρ (xᵢⱼ(c)) is a polynomial in c (TauCeti.IsRationalRep.exists_forall_transvectionUnit_eq_sum_smul), and the coefficients of a polynomial identity over an infinite field are determined (TauCeti.eq_of_forall_sum_range_pow_smul_eq). The m-th coefficient then lands in the weight space of l + m (εᵢ - εⱼ). Only nonnegative m occur, and that is exactly what a rational — as opposed to merely torus-eigen — representation buys: the negative powers a Laurent expansion would allow are what would break the argument.

Consequently a weight vector all of whose raised weight spaces vanish is fixed by the whole root subgroup, and maximizing the height ∑ᵢ (n - i) lᵢ over the finitely many weights produces such a weight. The maximizer is weakly decreasing, since transposing two out-of-order entries raises the height while permutations of a weight are again weights (TauCeti.weightSpace_eq_bot_comp_perm_iff).

Main results #

References #

The character of a multiple of a root #

source
theorem TauCeti.weightChar_add_nsmul_single_sub_single {κ : Type u_1} [Fintype κ] [DecidableEq κ] {R : Type u_2} [CommRing R] (i j : κ) (l : κ → ℤ) (m : ℕ) (t : κ → Rˣ) :
(weightChar R (l + m • (Pi.single i 1 - Pi.single j 1))) t = (weightChar R l) t * (t i * (t j)⁻¹) ^ m

A multiple of the root εᵢ - εⱼ translates a weight character by a power of tᵢ tⱼ⁻¹. This is the only property of that root the raising computation below uses. Nothing here is special to the index type Fin n of GL n, nor does it need i and j to be distinct: it is split-torus character arithmetic for an arbitrary index type.

Transvections raise weights #

source
theorem TauCeti.apply_mem_weightSpace_of_forall_transvectionUnit_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} {i j : Fin n} (hij : i ≠ j) {d : ℕ} {A : ℕ → Module.End K W} (hA : ∀ (c : K), ρ (transvectionUnit hij c) = ∑ m ∈ Finset.range d, c ^ m • A m) {l : Fin n → ℤ} {w : W} (hw : w ∈ weightSpace ρ l) {m : ℕ} (hm : m < d) :
(A m) w ∈ weightSpace ρ (l + m • (Pi.single i 1 - Pi.single j 1))

The coefficients of the root-subgroup expansion raise the weight. If the action along the root subgroup of εᵢ - εⱼ expands as ∑ m < d, c ^ m • A m, then A m carries a vector of weight l into the weight space of l + m (εᵢ - εⱼ).

Nothing in this statement refers to rationality, so the base field is an arbitrary infinite field: the argument only needs the coefficients of a polynomial identity to be determined by its values.

The action along a root subgroup is polynomial #

source
theorem TauCeti.IsRationalRep.exists_forall_transvectionUnit_eq_sum_smul {n : ℕ} {W : Type u} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (h : IsRationalRep ρ) {i j : Fin n} (hij : i ≠ j) :
∃ (d : ℕ) (A : ℕ → Module.End ℂ W), ∀ (c : ℂ), ρ (transvectionUnit hij c) = ∑ m ∈ Finset.range d, c ^ m • A m

The action along a root subgroup is polynomial in its parameter. The transvection xᵢⱼ(c) has determinant one and entries affine in c, so for a rational representation each matrix entry of ρ (xᵢⱼ(c)) is a polynomial in c, and the action is a finite sum ∑ m < d, c ^ m • A m whose coefficients do not depend on c.

source
theorem TauCeti.IsRationalRep.apply_transvectionUnit_eq_self {n : ℕ} {W : Type u} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (h : IsRationalRep ρ) {i j : Fin n} (hij : i ≠ j) {l : Fin n → ℤ} {w : W} (hw : w ∈ weightSpace ρ l) (hbot : ∀ (m : ℕ), 0 < m → weightSpace ρ (l + m • (Pi.single i 1 - Pi.single j 1)) = ⊥) (c : ℂ) :
(ρ (transvectionUnit hij c)) w = w

A weight vector all of whose raised weight spaces vanish is fixed by the root subgroup. This is the group-level form of a vector annihilated by a raising operator.

source
theorem TauCeti.IsRationalRep.apply_transvectionUnit_eq_self_of_forall_sum_le {n : ℕ} {W : Type u} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (h : IsRationalRep ρ) {l : Fin n → ℤ} (hl : ∀ (a : Fin n → ℤ), weightSpace ρ a ≠ ⊥ → ∀ (m : ℕ), ∑ k : Fin n with ↑k < m, a k ≤ ∑ k : Fin n with ↑k < m, l k) {i j : Fin n} (hij : i < j) {w : W} (hw : w ∈ weightSpace ρ l) (c : ℂ) :
(ρ (transvectionUnit ⋯ c)) w = w

A vector of a weight dominating every weight is fixed by the positive root subgroups. If every weight a of ρ is dominated by l, in the sense that each initial partial sum of a is at most the corresponding partial sum of l, then every transvection xᵢⱼ(c) with i < j fixes each vector of weight l: the raised weights l + m (εᵢ - εⱼ), m > 0, violate the dominance bound at the partial sum through i.

The highest weight #

source
theorem TauCeti.IsRationalRep.exists_highestWeightVector {n : ℕ} {W : Type u} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} [Nontrivial W] (h : IsRationalRep ρ) :
∃ (l : DominantWeight n) (w : W), w ≠ 0 ∧ w ∈ weightSpace ρ ↑l ∧ ∀ (i j : Fin n) (hij : i < j) (c : ℂ), (ρ (transvectionUnit ⋯ c)) w = w

A nonzero rational representation of GL n ℂ has a highest weight vector. There is a dominant weight l and a nonzero vector w of weight l that every transvection xᵢⱼ(c) with i < j fixes.

The weight is dominant, and the fixed vector nonzero, so this is the input to the highest-weight classification: the subrepresentation generated by w is a highest weight module of weight l.

An irreducible rational representation is determined by its highest weight #

source
theorem TauCeti.IsRationalRep.nonempty_equiv_of_highestWeightVector {n : ℕ} {W : Type u} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} {V : Type u_1} [AddCommGroup V] [Module ℂ V] {σ : Representation ℂ (GL (Fin n) ℂ) V} (hρ : IsRationalRep ρ) (hσ : IsRationalRep σ) [ρ.IsIrreducible] [σ.IsIrreducible] {l : Fin n → ℤ} {w : W} {v : V} (hw0 : w ≠ 0) (hwl : w ∈ weightSpace ρ l) (hw : ∀ (i j : Fin n) (hij : i < j) (c : ℂ), (ρ (transvectionUnit ⋯ c)) w = w) (hv0 : v ≠ 0) (hvl : v ∈ weightSpace σ l) (hv : ∀ (i j : Fin n) (hij : i < j) (c : ℂ), (σ (transvectionUnit ⋯ c)) v = v) :
Nonempty (ρ.Equiv σ)

An irreducible rational representation is determined by its highest weight: two irreducible rational representations of GL n ℂ, each with a nonzero vector of weight l fixed by every transvection xᵢⱼ(c) with i < j, are equivalent.