Dominant weights and highest weight vectors for gl n

Weights of gl n R for the diagonal Cartan subalgebra are tuples μ : n → R (TauCeti.glWeightEquiv). This file adds the two predicates that highest weight theory for gl n is stated against, both in the matrix unit positive system of TauCeti/Algebra/Lie/GeneralLinear/Borel.lean.

The first is dominance. For gl n it is a condition on differences, not on the entries themselves: a tuple μ : Fin n → R over a ring of characteristic zero is dominant integral when each consecutive difference μ i - μ (i+1) is a natural number — characteristic zero is what makes "is a natural number" a real condition, since over ZMod p every element is a natural number cast and every tuple would qualify. The entries are unconstrained, and that slack is exactly the central direction: adding a constant tuple c · (1, …, 1) — the weight of the centre of gl n — preserves dominance for every c : R. The staircase (N - 1/2, N - 3/2, …, 1/2) over ℚ is dominant with no integer entry at all, which is what makes the slack visible, and the weakly decreasing integer tuples sit inside the dominant ones as the weights of the rational representations of the group.

The second is being a highest weight vector of weight μ: a nonzero vector which the diagonal matrix units Eᵢᵢ scale by μ i and which the raising matrix units Eᵢⱼ, i < j, annihilate. Those two families are coordinates for the diagonal Cartan subalgebra and generators of the positive nilpotent subalgebra 𝔫⁺ of strictly upper triangular matrices — which is a Lie ideal of the standard Borel subalgebra, not of gl n itself — so the elementwise conditions are equivalent to the two coordinate-free ones: the whole Cartan acts by the weight TauCeti.glWeightEquiv R n μ, and the whole of 𝔫⁺ annihilates (TauCeti.isGlHighestWeightVector_iff_forall_mem).

Main definitions

• TauCeti.IsGlDominantIntegral μ: the consecutive differences of μ : Fin n → R are natural numbers, for R of characteristic zero.
• TauCeti.glStaircase N: the staircase tuple (N - 1/2, N - 3/2, …, 1/2) : Fin N → ℚ.
• TauCeti.glHalfStaircase F N: the formula N - 1/2 - i over any field; when two is invertible, this is the same half-shifted staircase.
• Fin.natCast_rev_add_one_div_two_eq_glHalfStaircase: the reverse finite index, cast to a field and shifted by one half, is the corresponding half-staircase entry.
• TauCeti.IsGlHighestWeightVector μ v: v is nonzero, the diagonal matrix unit Eᵢᵢ acts on it by μ i, and every raising matrix unit Eᵢⱼ with i < j annihilates it.

Main results

• TauCeti.IsGlDominantIntegral.exists_natCast_sub_of_le: dominance propagates from consecutive indices to all pairs, μ i - μ j ∈ ℕ whenever i ≤ j, and TauCeti.isGlDominantIntegral_iff_forall_le records the two forms as equivalent.
• TauCeti.isGlDominantIntegral_intCast: an antitone integer tuple is dominant — the weights of the group level sit inside the dominant ones.
• TauCeti.IsGlDominantIntegral.add_const: dominance is invariant under the central direction, and TauCeti.IsGlDominantIntegral.exists_antitone_natCast_add_const is the converse decomposition: every dominant weight is an antitone tuple of natural numbers translated along that direction. TauCeti.IsGlDominantIntegral.antitone_of_eq_natCast_add_const recovers antitonicity when that translated tuple is prescribed.
• TauCeti.isGlDominantIntegral_glStaircase and TauCeti.glStaircase_ne_intCast: the staircase is dominant and no entry of it is an integer, so dominance genuinely does not force integrality.
• TauCeti.isGlDominantIntegral_glHalfStaircase: the field-valued half-staircase is dominant in characteristic zero.
• TauCeti.sum_glStaircase: the sum of the staircase entries after mapping to a characteristic-zero field.
• TauCeti.sum_glHalfStaircase: the corresponding sum over any field in which two is invertible.
• TauCeti.IsGlHighestWeightVector.lie_eq_glWeightEquiv_smul and TauCeti.IsGlHighestWeightVector.lie_eq_zero_of_mem_strictUpperTriangular: the whole diagonal Cartan subalgebra acts by the weight, and the whole positive nilpotent subalgebra 𝔫⁺ annihilates.
• TauCeti.isGlHighestWeightVector_iff_forall_mem: those two conditions characterise a highest weight vector, so the elementwise definition loses nothing.
• TauCeti.IsGlHighestWeightVector.weight_eq: a vector is a highest weight vector for at most one weight.
• TauCeti.IsGlHighestWeightVector.map and TauCeti.IsGlHighestWeightVector.congr: highest weight vectors transport along module morphisms that preserve nonzeroness, in particular equivalences.
• TauCeti.isGlHighestWeightVector_coe_iff: a vector of a Lie submodule is a highest weight vector of that submodule exactly when it is one of the ambient module.
• TauCeti.forall_one_lie_eq_sum_smul_of_isGlHighestWeightVector: on an irreducible module carrying a highest weight vector, the identity matrix acts by the sum of the entries of that weight.
• TauCeti.isGlHighestWeightVector_single_bot_top: the highest root vector E_{⊥⊤} is a highest weight vector of the adjoint module, of weight ε_⊥ - ε_⊤, so the predicate is not vacuous.

Implementation notes

Both predicates are stated as the conjunctions pinned by the roadmap rather than as structures, so that they are definitionally the classical conditions; because the bodies are not exposed, the Iff restatements TauCeti.isGlDominantIntegral_iff and TauCeti.isGlHighestWeightVector_iff are how they are introduced and eliminated downstream, with TauCeti.IsGlHighestWeightVector.ne_zero, TauCeti.IsGlHighestWeightVector.lie_single_self_eq_smul and TauCeti.IsGlHighestWeightVector.lie_single_eq_zero as the projections.

Dominance is stated for Fin n, since "consecutive" refers to the successor on the indices, while the highest weight condition needs only a linearly ordered index type and is stated for one, as TauCeti.strictUpperTriangular is. Neither needs a field or an algebraically closed field, so both are over a commutative ring and the roadmap's field case is the instance R = K; dominance additionally asks for CharZero R, because "the difference is a natural number" is a condition on R only when the cast ℕ → R is injective — in characteristic p every element of ZMod p is such a cast and the predicate would be satisfied by every tuple. That hypothesis is used in the definition itself, through the injective Nat.castEmbedding rather than the bare Nat.cast, so that no shape of the predicate can drift away from it; TauCeti.isGlDominantIntegral_iff puts the condition back in the plain form ∃ k : ℕ, μ i - μ j = k. The two statements that read a scalar back off a vector — uniqueness of the weight, and that rescaling preserves the predicate — are the ones needing more, namely the hypotheses IsCancelMulZero R and Module.IsTorsionFree R M of Mathlib's smul_left_injective, without which a torsion vector could carry several weights at once.

As in TauCeti/Algebra/Lie/GeneralLinear/Basic.lean, LieRing.ofAssociativeRing is a local instance, Mathlib not registering it globally; the Lie module hypotheses on M are stated against it, so a downstream file must install it too before mentioning IsGlHighestWeightVector.

References

This implements the two predicates of the "diagonal Cartan and gl_n weights" item of Layer 9 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md: "dominance is a condition on differences (IsGlDominantIntegral: consecutive differences in ℕ, entries free in K), and a highest weight vector is a simultaneous eigenvector of the diagonal killed by the strict upper triangle (IsGlHighestWeightVector)", together with the staircase example that item names and the integral points of that layer's "dictionary to the group level". The classification statements made against them are not proved here.

• W. Fulton, J. Harris, Representation Theory: A First Course, Springer GTM 129 (1991), §15.

Dominant integral weights of gl n

def TauCeti.IsGlDominantIntegral {R : Type u_1} [CommRing R] [CharZero R] {n : ℕ} (mu : Fin n → R) : Prop

A tuple μ : Fin n → R is dominant integral for gl n when each consecutive difference μ i - μ j, j the successor of i, is a natural number.

The scalars are required to have characteristic zero: that is what makes the condition say what it reads as. In characteristic p the cast ℕ → R is not injective — over ZMod p every element is the cast of a natural number — so every tuple would be dominant and the notion would be vacuous. Accordingly the cast is spelled through Nat.castEmbedding, which is Nat.cast bundled with its injectivity, so that the hypothesis is used by the statement itself; TauCeti.isGlDominantIntegral_iff restates the condition with the plain cast and is how the predicate is introduced and eliminated.

The entries themselves are unconstrained: dominance is a condition on differences only, so it is invariant under the central direction μ ↦ μ + c · (1, …, 1) (TauCeti.IsGlDominantIntegral.add_const) and does not force integrality (TauCeti.glStaircase_ne_intCast).

Equations

• TauCeti.IsGlDominantIntegral mu = ∀ (i j : Fin n), ↑i + 1 = ↑j → ∃ (k : ℕ), mu i - mu j = Nat.castEmbedding k

theorem TauCeti.isGlDominantIntegral_iff {R : Type u_1} [CommRing R] [CharZero R] {n : ℕ} {mu : Fin n → R} : IsGlDominantIntegral mu ↔ ∀ (i j : Fin n), ↑i + 1 = ↑j → ∃ (k : ℕ), mu i - mu j = ↑k

TauCeti.IsGlDominantIntegral unfolded. The predicate is not exposed, so this is how it is introduced and eliminated outside this file.

theorem TauCeti.IsGlDominantIntegral.exists_natCast_sub_of_add_eq {R : Type u_1} [CommRing R] [CharZero R] {n : ℕ} {mu : Fin n → R} (h : IsGlDominantIntegral mu) (d : ℕ) (i j : Fin n) : ↑i + d = ↑j → ∃ (k : ℕ), mu i - mu j = ↑k

Dominance propagates along a chain of consecutive steps: if i is d steps below j then μ i - μ j is a natural number, by adding up the d consecutive differences.

theorem TauCeti.IsGlDominantIntegral.exists_natCast_sub_of_le {R : Type u_1} [CommRing R] [CharZero R] {n : ℕ} {mu : Fin n → R} (h : IsGlDominantIntegral mu) {i j : Fin n} (hij : i ≤ j) : ∃ (k : ℕ), mu i - mu j = ↑k

Dominance is a condition on all differences, not just the consecutive ones: for a dominant μ and i ≤ j, the difference μ i - μ j is a natural number.

theorem TauCeti.isGlDominantIntegral_iff_forall_le {R : Type u_1} [CommRing R] [CharZero R] {n : ℕ} {mu : Fin n → R} : IsGlDominantIntegral mu ↔ ∀ (i j : Fin n), i ≤ j → ∃ (k : ℕ), mu i - mu j = ↑k

Dominance in its two equivalent forms: consecutive differences, or all differences along the order.

theorem TauCeti.isGlDominantIntegral_const {R : Type u_1} [CommRing R] [CharZero R] {n : ℕ} (c : R) : IsGlDominantIntegral fun (x : Fin n) => c

A constant tuple is dominant: this is the weight by which the centre of gl n acts.

theorem TauCeti.IsGlDominantIntegral.add {R : Type u_1} [CommRing R] [CharZero R] {n : ℕ} {mu nu : Fin n → R} (h : IsGlDominantIntegral mu) (h' : IsGlDominantIntegral nu) : IsGlDominantIntegral (mu + nu)

Dominance is closed under addition.

theorem TauCeti.IsGlDominantIntegral.add_const {R : Type u_1} [CommRing R] [CharZero R] {n : ℕ} {mu : Fin n → R} (h : IsGlDominantIntegral mu) (c : R) : IsGlDominantIntegral fun (i : Fin n) => mu i + c

Dominance is invariant under the central direction. Adding the constant tuple c · (1, …, 1) — the weight of the centre of gl n, which is invisible to the differences — takes dominant weights to dominant weights.

theorem TauCeti.isGlDominantIntegral_intCast {R : Type u_1} [CommRing R] [CharZero R] {n : ℕ} {a : Fin n → ℤ} (ha : Antitone a) : IsGlDominantIntegral fun (i : Fin n) => ↑(a i)

The integral points. An antitone tuple of integers is dominant: the weakly decreasing integer tuples that index the rational representations of the group GL n sit inside the dominant weights of gl n, the extra directions being the non-integral ones.

theorem TauCeti.IsGlDominantIntegral.exists_antitone_natCast_add_const {R : Type u_1} [CommRing R] [CharZero R] {n : ℕ} {mu : Fin n → R} (hmu : IsGlDominantIntegral mu) : ∃ (a : Fin n → ℕ) (c : R), Antitone a ∧ mu = fun (i : Fin n) => ↑(a i) + c

A dominant weight is a tuple of natural numbers translated along the central direction, the converse of TauCeti.isGlDominantIntegral_intCast and TauCeti.IsGlDominantIntegral.add_const together. Subtracting the last entry c of a dominant μ leaves the differences μ i - c, which dominance makes natural numbers, and those decrease weakly because the differences μ i - μ j along the order are natural numbers too.

theorem TauCeti.IsGlDominantIntegral.antitone_of_eq_natCast_add_const {R : Type u_1} [CommRing R] [CharZero R] {n : ℕ} {mu : Fin n → R} (hmu : IsGlDominantIntegral mu) {a : Fin n → ℕ} {c : R} (h : mu = fun (i : Fin n) => ↑(a i) + c) : Antitone a

If a dominant integral weight is already expressed as a common translate of a natural tuple, that tuple is antitone. This is the prescribed-tuple counterpart to TauCeti.IsGlDominantIntegral.exists_antitone_natCast_add_const.

theorem TauCeti.isGlDominantIntegral_of_le_one {R : Type u_1} [CommRing R] [CharZero R] {n : ℕ} (hn : n ≤ 1) (mu : Fin n → R) : IsGlDominantIntegral mu

Over an index type with at most one element there is no consecutive pair, so every tuple is dominant.

The staircase weight

def TauCeti.glStaircase (N : ℕ) : Fin N → ℚ

The staircase weight (N - 1/2, N - 3/2, …, 1/2) : Fin N → ℚ, the standard witness that dominance for gl n does not force the entries to be integers: it is dominant (TauCeti.isGlDominantIntegral_glStaircase) and none of its entries is an integer (TauCeti.glStaircase_ne_intCast). Its consecutive differences are all 1, so it is the half-shift of the integral weight (N - 1, N - 2, …, 0) by the central direction 1/2 · (1, …, 1).

Equations

• TauCeti.glStaircase N i = ↑N - 1 / 2 - ↑↑i

@[simp]

theorem TauCeti.glStaircase_apply (N : ℕ) (i : Fin N) : glStaircase N i = ↑N - 1 / 2 - ↑↑i

def TauCeti.glHalfStaircase (F : Type u_2) [Field F] (N : ℕ) : Fin N → F

The formula N - 1/2 - i over a field. When two is invertible, this is the half-shifted staircase weight (N - 1/2, N - 3/2, …, 1/2). Unlike TauCeti.glStaircase, this definition does not require a map from the rationals, so it remains available in positive characteristic whenever two is invertible.

Equations

• TauCeti.glHalfStaircase F N i = ↑N - 1 / 2 - ↑↑i

@[simp]

theorem TauCeti.glHalfStaircase_apply {F : Type u_2} [Field F] (N : ℕ) (i : Fin N) : glHalfStaircase F N i = ↑N - 1 / 2 - ↑↑i

@[simp]

theorem Fin.natCast_rev_add_one_div_two_eq_glHalfStaircase {F : Type u_1} [Field F] [Invertible 2] {N : ℕ} (i : Fin N) : ↑↑i.rev + 1 / 2 = TauCeti.glHalfStaircase F N i

Casting a reverse finite index and adding the half-unit shift gives the corresponding entry of the half-shifted staircase.

theorem TauCeti.sum_glHalfStaircase {F : Type u_1} [Field F] [Invertible 2] (N : ℕ) : ∑ i : Fin N, glHalfStaircase F N i = ↑N ^ 2 / 2

The entries of the half-shifted staircase over a field in which two is invertible sum to N² / 2.

theorem TauCeti.sum_glStaircase {F : Type u_1} [Field F] [CharZero F] (N : ℕ) : ∑ i : Fin N, (algebraMap ℚ F) (glStaircase N i) = ↑N ^ 2 / 2

The entries of the staircase weight sum to N² / 2 after mapping from ℚ to any characteristic-zero field.

theorem TauCeti.isGlDominantIntegral_glStaircase (N : ℕ) : IsGlDominantIntegral (glStaircase N)

The staircase weight is dominant: its consecutive differences are all 1.

theorem TauCeti.isGlDominantIntegral_glHalfStaircase {F : Type u_1} [Field F] [CharZero F] (N : ℕ) : IsGlDominantIntegral (glHalfStaircase F N)

The half-staircase weight over a characteristic-zero field is dominant: as for the rational staircase, every consecutive difference is 1.

theorem TauCeti.isGlDominantIntegral_glHalfStaircase_sub_single {F : Type u_1} [Field F] [CharZero F] (N : ℕ) (t : Fin N) : IsGlDominantIntegral (glHalfStaircase F N - Pi.single t 1)

Lowering one entry of the half-shifted staircase preserves gl n dominance.

theorem TauCeti.glStaircase_ne_intCast {N : ℕ} (i : Fin N) (m : ℤ) : glStaircase N i ≠ ↑m

No entry of the staircase weight is an integer. Together with TauCeti.isGlDominantIntegral_glStaircase this pins the difference between dominance for gl n and dominance for a semisimple Lie algebra: the entries of a dominant gl n weight are free, only their differences are constrained.

Highest weight vectors for gl n

def TauCeti.IsGlHighestWeightVector {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule (Matrix n n R) M] (mu : n → R) (v : M) : Prop

A vector v of a gl n R-module is a highest weight vector of weight μ for the matrix unit positive system when it is nonzero, the diagonal matrix unit Eᵢᵢ acts on it by the scalar μ i, and every raising matrix unit Eᵢⱼ with i < j annihilates it.

The two elementwise families are coordinates for the diagonal Cartan subalgebra and generators of the positive nilpotent subalgebra 𝔫⁺ — the nilpotent ideal of the standard Borel subalgebra TauCeti.upperTriangular R n, not an ideal of gl n R — so this says exactly that v is a 𝔫⁺-annihilated weight vector of weight TauCeti.glWeightEquiv R n μ; see TauCeti.isGlHighestWeightVector_iff_forall_mem.

Equations

• TauCeti.IsGlHighestWeightVector mu v = (v ≠ 0 ∧ (∀ (i : n), ⁅Matrix.single i i 1, v⁆ = mu i • v) ∧ ∀ (i j : n), i < j → ⁅Matrix.single i j 1, v⁆ = 0)

theorem TauCeti.isGlHighestWeightVector_iff {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule (Matrix n n R) M] {mu : n → R} {v : M} : IsGlHighestWeightVector mu v ↔ v ≠ 0 ∧ (∀ (i : n), ⁅Matrix.single i i 1, v⁆ = mu i • v) ∧ ∀ (i j : n), i < j → ⁅Matrix.single i j 1, v⁆ = 0

TauCeti.IsGlHighestWeightVector unfolded. The predicate is not exposed, so this is how it is introduced outside this file; the three projections below are its elimination API.

theorem TauCeti.IsGlHighestWeightVector.ne_zero {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule (Matrix n n R) M] {mu : n → R} {v : M} (hv : IsGlHighestWeightVector mu v) : v ≠ 0

A highest weight vector is nonzero.

theorem TauCeti.IsGlHighestWeightVector.lie_single_self_eq_smul {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule (Matrix n n R) M] {mu : n → R} {v : M} (hv : IsGlHighestWeightVector mu v) (i : n) : ⁅Matrix.single i i 1, v⁆ = mu i • v

The diagonal matrix unit Eᵢᵢ scales a highest weight vector by the i-th entry of its weight.

theorem TauCeti.IsGlHighestWeightVector.lie_single_eq_zero {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule (Matrix n n R) M] {mu : n → R} {v : M} (hv : IsGlHighestWeightVector mu v) {i j : n} (hij : i < j) : ⁅Matrix.single i j 1, v⁆ = 0

The raising matrix units annihilate a highest weight vector.

theorem TauCeti.IsGlHighestWeightVector.map {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule (Matrix n n R) M] {mu : n → R} {v : M} {M' : Type u_4} [AddCommGroup M'] [Module R M'] [LieRingModule (Matrix n n R) M'] (f : M →ₗ⁅R,Matrix n n R⁆ M') (hf : f v ≠ 0) (hv : IsGlHighestWeightVector mu v) : IsGlHighestWeightVector mu (f v)

Transport along a map of gl n R-modules. The two weight conditions transport along any map; all that is asked of f is that it keep the vector nonzero, which for an injective f — an equivalence e, say — is automatic.

theorem TauCeti.IsGlHighestWeightVector.congr {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule (Matrix n n R) M] {mu : n → R} {v : M} {M' : Type u_4} [AddCommGroup M'] [Module R M'] [LieRingModule (Matrix n n R) M'] (hv : IsGlHighestWeightVector mu v) (e : M ≃ₗ⁅R,Matrix n n R⁆ M') : IsGlHighestWeightVector mu (e v)

Transport along an equivalence of gl n R-modules.

theorem TauCeti.IsGlHighestWeightVector.weight_eq {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule (Matrix n n R) M] {mu nu : n → R} {v : M} [IsCancelMulZero R] [Module.IsTorsionFree R M] (hv : IsGlHighestWeightVector mu v) (hv' : IsGlHighestWeightVector nu v) : mu = nu

A vector is a highest weight vector for at most one weight. The diagonal matrix units read the weight off the vector, so two weights of the same nonzero vector agree entry by entry.

theorem TauCeti.IsGlHighestWeightVector.lie_eq_smul_of_mem_diagonalCartan {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule (Matrix n n R) M] {mu : n → R} {v : M} [LieModule R (Matrix n n R) M] (hv : IsGlHighestWeightVector mu v) {A : Matrix n n R} (hA : A ∈ diagonalCartan R n) : ⁅A, v⁆ = (∑ i : n, mu i * A i i) • v

The whole diagonal Cartan subalgebra acts on a highest weight vector by its weight, not just the diagonal matrix units: ⁅A, v⁆ = (∑ i, μ i · Aᵢᵢ) • v for every diagonal A.

theorem TauCeti.IsGlHighestWeightVector.lie_eq_glWeightEquiv_smul {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule (Matrix n n R) M] {mu : n → R} {v : M} [LieModule R (Matrix n n R) M] (hv : IsGlHighestWeightVector mu v) (A : ↥(diagonalCartan R n)) : ⁅↑A, v⁆ = ((glWeightEquiv R n) mu) A • v

The coordinate-free form of TauCeti.IsGlHighestWeightVector.lie_eq_smul_of_mem_diagonalCartan: an element of the diagonal Cartan subalgebra acts on a highest weight vector by the value of the weight TauCeti.glWeightEquiv R n μ on it.

theorem TauCeti.IsGlHighestWeightVector.lie_eq_zero_of_mem_strictUpperTriangular {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule (Matrix n n R) M] {mu : n → R} {v : M} [LieModule R (Matrix n n R) M] (hv : IsGlHighestWeightVector mu v) {A : Matrix n n R} (hA : A ∈ strictUpperTriangular R n) : ⁅A, v⁆ = 0

The whole positive nilpotent subalgebra 𝔫⁺ annihilates a highest weight vector, not just the raising matrix units that span it.

theorem TauCeti.isGlHighestWeightVector_iff_forall_mem {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule (Matrix n n R) M] {mu : n → R} {v : M} [LieModule R (Matrix n n R) M] : IsGlHighestWeightVector mu v ↔ v ≠ 0 ∧ (∀ (A : ↥(diagonalCartan R n)), ⁅↑A, v⁆ = ((glWeightEquiv R n) mu) A • v) ∧ ∀ A ∈ strictUpperTriangular R n, ⁅A, v⁆ = 0

The subalgebra form of the definition: a highest weight vector is exactly a nonzero vector on which the diagonal Cartan subalgebra acts by the weight TauCeti.glWeightEquiv R n μ and which the positive nilpotent subalgebra 𝔫⁺ annihilates. The elementwise definition therefore loses nothing.

@[simp]

theorem TauCeti.isGlHighestWeightVector_coe_iff {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule (Matrix n n R) M] {mu : n → R} {P : LieSubmodule R (Matrix n n R) M} {w : ↥P} : IsGlHighestWeightVector mu ↑w ↔ IsGlHighestWeightVector mu w

A vector of a Lie submodule is a highest weight vector of that submodule exactly when it is one of the ambient module: both defining conditions are read off the ambient bracket.

theorem TauCeti.IsGlHighestWeightVector.smul {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule (Matrix n n R) M] {mu : n → R} {v : M} [LieModule R (Matrix n n R) M] [IsCancelMulZero R] [Module.IsTorsionFree R M] (hv : IsGlHighestWeightVector mu v) {c : R} (hc : c ≠ 0) : IsGlHighestWeightVector mu (c • v)

Rescaling a highest weight vector by a nonzero scalar gives a highest weight vector of the same weight.

theorem TauCeti.forall_one_lie_eq_sum_smul_of_isGlHighestWeightVector {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule (Matrix n n R) M] {mu : n → R} {v : M} [LieModule R (Matrix n n R) M] [LieModule.IsIrreducible R (Matrix n n R) M] (hv : IsGlHighestWeightVector mu v) (m : M) : ⁅1, m⁆ = (∑ i : n, mu i) • m

The identity matrix acts by the sum of the highest weight entries on any irreducible module carrying a highest weight vector. The scalar is read off the highest weight vector rather than produced by Schur's lemma, so a commutative ring of scalars is all this needs.

The highest root vector of the adjoint module

theorem TauCeti.isGlHighestWeightVector_single_bot_top {R : Type u_1} [CommRing R] [Nontrivial R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] [OrderBot n] [OrderTop n] : IsGlHighestWeightVector (Pi.single ⊥ 1 - Pi.single ⊤ 1) (Matrix.single ⊥ ⊤ 1)

The highest root vector is a highest weight vector, for the adjoint action of gl n R on itself: the matrix unit E_{⊥⊤} in the corner is nonzero, the diagonal acts on it by ε_⊥ - ε_⊤, and every raising matrix unit annihilates it, since E_{ij} E_{⊥⊤} needs j = ⊥ and E_{⊥⊤} E_{ij} needs i = ⊤, both impossible for i < j.

TauCeti.IsGlHighestWeightVector is therefore not vacuous. For an index type with more than one element the weight ε_⊥ - ε_⊤ is the highest root, the tuple (1, 0, …, 0, -1); for a singleton one the two matrix units coincide, the weight degenerates to 0, and the statement is the (still true) assertion that E_{⊥⊥} is a highest weight vector of weight 0 of the abelian gl 1.