The integrability relation of a highest weight module

Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over a field of characteristic zero, H a splitting Cartan subalgebra, b a base of its root system, and M a module generated by a highest weight vector v of weight lam. Fix a simple root αᵢ and suppose the highest weight is integral along it, lam (αᵢ^∨) = n for a natural number n. This file proves the integrability relation: the vector

w = fᵢ^{n + 1} · v

obtained by lowering v to degree n + 1 in its αᵢ-string is again a highest weight vector, of weight lam - (n + 1) αᵢ, as soon as it is nonzero. Consequently it is zero whenever M is irreducible: an irreducible module has highest weight vectors of only one weight.

The relation is the mechanism by which dominance makes a highest weight module small. In the Verma module M(lam) the vector w is nonzero, for a nonzero lowering vector fᵢ, and the submodule it generates is then a proper submodule, hence one contained in the maximal submodule that the irreducible quotient L(lam) divides out; in L(lam) the vector itself vanishes. This relation on the highest-weight generator is the first step toward proving local nilpotence along every simple root. The vanishing is proved here for every irreducible highest weight module, which is what L(lam) will be.

The argument

Three facts have to be checked about w, and they use different parts of the theory.

• H acts through lam - (n + 1) αᵢ. Lowering by a root vector of -αᵢ subtracts αᵢ from the weight, one step at a time; this is Ado.lie_pow_toEnd_eq_smul_of_mem_rootSpace, an induction on the number of steps out of the Leibniz rule.
• The root space of αᵢ annihilates w. This is the rank-one statement, and it is exactly Mathlib's IsSl2Triple.HasPrimitiveVectorWith.lie_e_pow_succ_toEnd_f: raising fᵢ^{k + 1} v returns (k + 1)(n - k) times fᵢ^k v, which vanishes at k = n. Both root spaces are lines, so the normalized triple of αᵢ computes the whole of them.
• Every other positive root space annihilates w. Here the rank-one theory says nothing, and the input is the geometry of the weight cone. A positive root αⱼ would move w to the weight lam - (n + 1) αᵢ + αⱼ, and the weights of a highest weight module lie in lam - Q⁺, so (n + 1) αᵢ - αⱼ would have to be a nonnegative combination of simple roots. By Ado.eq_of_nsmul_root_sub_root_mem_posRootCone that forces αⱼ = αᵢ, which is the case already treated.

Main results

• Ado.isHighestWeightVector_pow_toEnd_of_lieSpan_eq_top_of_ne_zero: the integrability relation, that fᵢ^{n + 1} v is a highest weight vector of weight lam - (n + 1) αᵢ when it is nonzero.
• Ado.pow_toEnd_mem_maximalSubmodule_of_isHighestWeightVector_of_lieSpan_eq_top: it lies in the maximal submodule of a highest weight module, so it dies in the irreducible quotient.
• Ado.pow_toEnd_eq_zero_of_isHighestWeightVector_of_isIrreducible: in an irreducible highest weight module it is therefore zero.

References

This is the "integrability relation" milestone of Layer 4, "the classification of finite-dimensional irreducibles", of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md.

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §21.2 and §21.4.

The integrability relation

theorem Ado.lie_pow_toEnd_eq_zero_of_isHighestWeightVector {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} {lam : Module.Dual K ↥H} {v : M} (hv : IsHighestWeightVector b lam v) {i : ↥LieSubalgebra.root} (hi : i ∈ posRoots (LieAlgebra.IsKilling.rootSystem H) b) {n : ℕ} (hn : lam ((LieAlgebra.IsKilling.rootSystem H).coroot i) = ↑n) {e f : L} (he : e ∈ LieAlgebra.rootSpace H ⇑↑i) (hf : f ∈ LieAlgebra.rootSpace H ⇑(-↑i)) : ⁅e, ((LieModule.toEnd K L M) f ^ (n + 1)) v⁆ = 0

The rank-one half of the integrability relation: for a positive root αᵢ along which the highest weight is integral, the root space of αᵢ annihilates fᵢ^{n + 1} v.

The sl₂ triple of αᵢ makes v a primitive vector of eigenvalue n, and Mathlib's IsSl2Triple.HasPrimitiveVectorWith.lie_e_pow_succ_toEnd_f evaluates the raising operator on the lowered vectors; the coefficient (n + 1)(n - n) vanishes. Since both root spaces are lines, one normalized triple computes the bracket for every choice of raising and lowering vector.

theorem Ado.isHighestWeightVector_pow_toEnd_of_lieSpan_eq_top_of_ne_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} {lam : Module.Dual K ↥H} {v : M} (hv : IsHighestWeightVector b lam v) (hgen : LieSubmodule.lieSpan K L {v} = ⊤) {i : ↥LieSubalgebra.root} (hi : i ∈ b.support) {n : ℕ} (hn : lam ((LieAlgebra.IsKilling.rootSystem H).coroot i) = ↑n) {f : L} (hf : f ∈ LieAlgebra.rootSpace H ⇑(-↑i)) (hw : ((LieModule.toEnd K L M) f ^ (n + 1)) v ≠ 0) : IsHighestWeightVector b (lam - (n + 1) • (LieAlgebra.IsKilling.rootSystem H).root i) (((LieModule.toEnd K L M) f ^ (n + 1)) v)

The integrability relation. Let M be a highest weight module of weight lam generated by v, let αᵢ be a simple root and suppose lam (αᵢ^∨) = n is a natural number. Then the lowered vector fᵢ^{n + 1} v is, whenever it is nonzero, again a highest weight vector, of weight lam - (n + 1) αᵢ.

Its H-eigenvalue is read off Ado.lie_pow_toEnd_eq_smul_of_mem_rootSpace. Of the positive root spaces, that of αᵢ annihilates it by the rank-one theory, and every other one does so because it would otherwise produce a weight above the cone lam - Q⁺ that bounds a highest weight module.

Vanishing in the irreducible quotient

theorem Ado.pow_toEnd_mem_maximalSubmodule_of_isHighestWeightVector_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} {lam : Module.Dual K ↥H} {v : M} (hv : IsHighestWeightVector b lam v) (hgen : LieSubmodule.lieSpan K L {v} = ⊤) {i : ↥LieSubalgebra.root} (hi : i ∈ b.support) {n : ℕ} (hn : lam ((LieAlgebra.IsKilling.rootSystem H).coroot i) = ↑n) {f : L} (hf : f ∈ LieAlgebra.rootSpace H ⇑(-↑i)) : ((LieModule.toEnd K L M) f ^ (n + 1)) v ∈ maximalSubmodule H M lam

The lowered vector dies in the irreducible quotient. In a highest weight module of weight lam generated by v, the vector fᵢ^{n + 1} v lies in the maximal submodule Ado.maximalSubmodule, so it maps to 0 in the irreducible quotient.

If it is nonzero it is a highest weight vector of weight lam - (n + 1) αᵢ, so the submodule it generates cannot be everything: a module is a highest weight module for at most one weight. The maximal submodule of a highest weight module is its greatest proper submodule, so that submodule lies inside it.

theorem Ado.pow_toEnd_eq_zero_of_isHighestWeightVector_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} {lam : Module.Dual K ↥H} {v : M} [LieModule.IsIrreducible K L M] (hv : IsHighestWeightVector b lam v) {i : ↥LieSubalgebra.root} (hi : i ∈ b.support) {n : ℕ} (hn : lam ((LieAlgebra.IsKilling.rootSystem H).coroot i) = ↑n) {f : L} (hf : f ∈ LieAlgebra.rootSpace H ⇑(-↑i)) : ((LieModule.toEnd K L M) f ^ (n + 1)) v = 0

The integrability relation in an irreducible highest weight module. If M is irreducible with highest weight vector v of weight lam, and lam (αᵢ^∨) = n is a natural number, then fᵢ^{n + 1} v = 0.

This is the integrability relation on the highest-weight generator. Were the lowered vector nonzero it would be a highest weight vector of weight lam - (n + 1) αᵢ, and an irreducible module carries highest weight vectors of only one weight (Ado.IsHighestWeightVector.unique_of_isIrreducible).