Highest-weight vectors from a Lie algebra basis

This file connects a LieAlgebra.Basis to the positive-system definition of a highest-weight vector. The positive-nilradical and Borel bridge is developed in TauCeti.Algebra.Lie.Basis.Borel; here it reduces the highest-weight-vector condition to annihilation by the raising operators eᵢ.

Main results

• LieAlgebra.Basis.isHighestWeightVector_iff_forall_e reduces the highest-weight condition to annihilation by the raising operators.

theorem LieAlgebra.Basis.isHighestWeightVector_iff_forall_e {ι : Type u_1} [Fintype ι] {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] (b : Basis ι H) {lam : Module.Dual K ↥H} {v : M} : TauCeti.IsHighestWeightVector b.base lam v ↔ v ≠ 0 ∧ (∀ (x : ↥H), ⁅↑x, v⁆ = lam x • v) ∧ ∀ (i : ι), ⁅b.e i, v⁆ = 0

A vector is highest weight for the base of a Lie algebra basis exactly when it is a nonzero weight vector annihilated by every raising operator.