An irreducible highest weight module of dominant integral weight is integrable

Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over a field of characteristic zero, let H be a splitting Cartan subalgebra, let b be a base of its root system and let M be an irreducible L-module carrying a highest weight vector v of weight lam. This file proves that when lam is integral along a simple root αᵢ the module M is integrable in that direction:

• both root vectors of αᵢ act locally nilpotently on the whole of M, and
• every vector of M lies in a finitely generated subspace stable under the sl₂ triple of αᵢ, so that M is a locally finite module over that triple.

Integrability is the property that turns the weight cone lam - Q⁺ of TauCeti/Algebra/Lie/HighestWeight/Module.lean into a finite set: only for an integrable module is the set of weights stable under the Weyl group, and it is that stability, together with the cone, which bounds the weights and eventually makes L(lam) finite-dimensional.

The argument

Both statements have the same shape. The condition in question — being annihilated by a power of a fixed element, or lying in a finitely generated subspace stable under a fixed set of elements — holds on a Lie submodule of M, by TauCeti/Algebra/Lie/Submodule/LocallyFinite.lean; an irreducible module is therefore either everywhere or nowhere in that condition, and the highest weight vector settles which.

• For a positive root vector e nothing is needed beyond the definition of a highest weight vector: e annihilates v outright. The relevant Lie submodule contains v, hence is ⊤.
• For the simple lowering vector fᵢ the input is the integrability relation of TauCeti/Algebra/Lie/HighestWeight/Integrability.lean: in an irreducible highest weight module fᵢ^{n + 1} v = 0, where n = lam (αᵢ^∨).
• Local finiteness uses finite-dimensionality of L and the explicit stable weight-string submodule Ado.weightStringSubmodule; the integrability relation truncates its generating string to v, fᵢ v, …, fᵢ^n v, so its underlying submodule is finitely generated.

The local-nilpotence results also need ad of the root vector to be nilpotent, which is Mathlib's LieAlgebra.isNilpotent_ad_of_mem_rootSpace: a root vector moves the root spaces of L by a nonzero root, and L has only finitely many. The local-finiteness result does not use this hypothesis.

Main results

• Ado.exists_pow_toEnd_eq_zero_of_mem_posRoots: every positive root vector acts locally nilpotently on an irreducible highest weight module.
• Ado.exists_pow_toEnd_eq_zero_of_mem_rootSpace_neg: so does every lowering vector of a simple root along which the highest weight is integral, and Ado.exists_pow_toEnd_eq_zero_of_mem_rootSpace_neg_of_isDominantIntegral reads that off dominance.
• Ado.locallyFiniteSubmodule_eq_top_of_isSl2Triple: integrability, that every vector of the module lies in a finitely generated subspace stable under the sl₂ triple of such a simple root.

References

This is the local-nilpotence half of the "maximal integrable quotient and local nilpotence" 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.
• V. G. Kac, Infinite Dimensional Lie Algebras, 3rd ed., §3.6.

Local nilpotence of the root vectors

theorem Ado.exists_pow_toEnd_eq_zero_of_mem_posRoots {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 ∈ posRoots (LieAlgebra.IsKilling.rootSystem H) b) {e : L} (he : e ∈ LieAlgebra.rootSpace H ⇑↑i) (m : M) : ∃ (k : ℕ), ((LieModule.toEnd K L M) e ^ k) m = 0

A positive root vector acts locally nilpotently. On an irreducible module carrying a highest weight vector, every element of a positive root space is annihilated on every vector by one of its powers.

The positive root spaces annihilate the highest weight vector itself, and ad of a root vector is nilpotent, so the locally nilpotent vectors form a nonzero Lie submodule.

theorem Ado.exists_pow_toEnd_eq_zero_of_mem_rootSpace_neg {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)) (m : M) : ∃ (k : ℕ), ((LieModule.toEnd K L M) f ^ k) m = 0

The lowering vector of a simple root acts locally nilpotently. If the highest weight lam of an irreducible highest weight module takes the natural value n on the coroot of a simple root αᵢ, then every element of the -αᵢ root space is annihilated on every vector by one of its powers.

The integrability relation Ado.pow_toEnd_eq_zero_of_isHighestWeightVector_of_isIrreducible makes fᵢ^{n + 1} annihilate the highest weight vector, and the locally nilpotent vectors form a Lie submodule.

theorem Ado.exists_pow_toEnd_eq_zero_of_mem_rootSpace_neg_of_isDominantIntegral {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) (hlam : IsDominantIntegral b lam) {i : ↥LieSubalgebra.root} (hi : i ∈ b.support) {f : L} (hf : f ∈ LieAlgebra.rootSpace H ⇑(-↑i)) (m : M) : ∃ (k : ℕ), ((LieModule.toEnd K L M) f ^ k) m = 0

Local nilpotence of a lowering vector, from dominance. A dominant integral highest weight is integral along every simple root, so each simple lowering vector acts locally nilpotently on an irreducible highest weight module of that weight. The positive-root half is Ado.exists_pow_toEnd_eq_zero_of_mem_posRoots.

Local finiteness over the sl₂ triple of a simple root

theorem Ado.locallyFiniteSubmodule_eq_top_of_isSl2Triple {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) {h₀ e₀ f₀ : L} (t : IsSl2Triple h₀ e₀ f₀) (he₀ : e₀ ∈ LieAlgebra.rootSpace H ⇑↑i) (hf₀ : f₀ ∈ LieAlgebra.rootSpace H ⇑(-↑i)) : locallyFiniteSubmodule K M ↑(IsSl2Triple.toLieSubalgebra K t) = ⊤

Integrability of an irreducible highest weight module along a simple root. Let M be irreducible with a highest weight vector v of weight lam, let αᵢ be a simple root and suppose lam (αᵢ^∨) = n is a natural number. Then M is a locally finite module over the sl₂ triple of αᵢ: every vector lies in a finitely generated subspace stable under that triple.

The witness for v itself is the span of v, fᵢ v, …, fᵢ^n v: the ladder lemmas of Mathlib's Sl2.lean keep hᵢ and eᵢ inside it, and fᵢ walks along it and off its end into 0, by the integrability relation. Local finiteness holds on a Lie submodule, so irreducibility spreads it from v to all of M.