Highest weight zero and the trivial module

Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over a field of characteristic zero. This file proves that a finite-dimensional highest weight module generated by a vector of weight zero is trivial.

For each positive root, its sl₂ triple makes a highest weight vector of weight zero a primitive vector of sl₂-weight zero. The finite-dimensional sl₂ string therefore stops immediately, so the corresponding negative root space annihilates the vector. The Cartan and the positive nilradical already annihilate it by the definition of highest weight zero, and the triangular decomposition then shows that all of L annihilates it. If the vector generates the module, the whole action is trivial.

Main results

• TauCeti.IsHighestWeightVector.lie_eq_zero_of_weight_zero: every element of L annihilates a highest weight vector of weight zero in a finite-dimensional module.
• TauCeti.isTrivial_of_isHighestWeightVector_weight_zero_of_lieSpan_eq_top: a finite-dimensional highest weight module of highest weight zero is trivial.
• TauCeti.isTrivial_of_isHighestWeightVector_weight_zero_of_isIrreducible: an irreducible with a highest weight vector of weight zero is trivial.

References

This is the zero-weight separation step in Layer 5, "Weyl's complete reducibility theorem", of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md. Humphreys, Introduction to Lie Algebras and Representation Theory, §6 supplies the model for the subsequent Casimir-splitting argument; the rank-one zero-highest-weight argument used here is from §§7.2 and 21.1.

theorem TauCeti.IsHighestWeightVector.lie_eq_zero_of_weight_zero {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {v : M} [FiniteDimensional K M] (hv : IsHighestWeightVector b 0 v) (x : L) : ⁅x, v⁆ = 0

Every element of L annihilates a highest weight vector of weight zero in a finite-dimensional module.

theorem TauCeti.isTrivial_of_isHighestWeightVector_weight_zero_of_lieSpan_eq_top {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {v : M} [FiniteDimensional K M] (hv : IsHighestWeightVector b 0 v) (hgen : LieSubmodule.lieSpan K L {v} = ⊤) : LieModule.IsTrivial L M

A finite-dimensional highest weight module generated in weight zero is a trivial Lie module.

theorem TauCeti.isTrivial_of_isHighestWeightVector_weight_zero_of_isIrreducible {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {v : M} [LieModule.IsIrreducible K L M] (hv : IsHighestWeightVector b 0 v) : LieModule.IsTrivial L M

An irreducible module with a highest weight vector of weight zero is trivial.