Locally nilpotent and locally finite vectors of a Lie module

Let L be a Lie algebra over a commutative ring R and let M be an L-module. Two finiteness conditions on a vector of M are collected here, both of them conditions that hold on a Lie submodule and are therefore either vacuous or universal on an irreducible module.

• x : L acts locally nilpotently at m when x^k annihilates m for some k. The set of such m is the generalized 0-eigenspace of the action of x, and it is a Lie submodule as soon as ad x acts locally nilpotently on L: this is Mathlib's LieModule.lie_mem_maxGenEigenspace_toEnd at the eigenvalue 0 + 0.
• A set S ⊆ L acts locally finitely at m when m lies in a finitely generated R-submodule of M stable under bracketing with every element of S. The set of such m is a Lie submodule whenever L itself is a finite R-module: if N is finitely generated and S-stable then so is N + ⁅L, N⁆, and the latter contains ⁅y, m⁆ for every y : L.

Both statements are the mechanism behind an "integrability" argument: an irreducible module containing a single vector with the finiteness property has the property everywhere. The motivating instance is the highest weight vector of an irreducible highest weight module, which is annihilated by a power of each simple root vector; see TauCeti/Algebra/Lie/HighestWeight/Integrable.lean.

Main definitions

• Ado.locallyNilpotentSubmodule: the vectors annihilated by a power of a fixed element whose adjoint action is locally nilpotent, as a Lie submodule.
• Ado.locallyFiniteSubmodule: the vectors lying in a finitely generated subspace stable under a fixed set of elements, as a Lie submodule.

Main results

• Ado.exists_pow_toEnd_eq_zero_of_isIrreducible: on an irreducible module, an element whose adjoint action is locally nilpotent and which is locally nilpotent at one nonzero vector is locally nilpotent everywhere.
• Ado.locallyFiniteSubmodule_span: only the span of S matters, so the condition may be stated against a generating set and consumed against the subalgebra it generates.
• Ado.locallyFiniteSubmodule_eq_top_of_isIrreducible: on an irreducible module, a set that acts locally finitely at one nonzero vector acts locally finitely everywhere.

Implementation notes

The underlying subspace of Ado.locallyNilpotentSubmodule is Mathlib's Module.End.maxGenEigenspace of the action of x at the eigenvalue 0, which Mathlib itself promotes to a Lie submodule only as LieModule.genWeightSpaceOf, under the hypothesis that L is a nilpotent Lie algebra. That hypothesis fails for the semisimple Lie algebras this file is written for, and the local nilpotence of ad x replaces it: it is what makes every element of L lie in the generalized 0-eigenspace of ad x, which is all the argument of genWeightSpaceOf ever uses.

References

• 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.

Locally nilpotent vectors

def Ado.locallyNilpotentSubmodule (R : Type u) {L : Type v} (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (hx : ∀ (y : L), ∃ (k : ℕ), ((LieAlgebra.ad R L) x ^ k) y = 0) : LieSubmodule R L M

The vectors of M annihilated by some power of the action of x, as a Lie submodule.

The underlying subspace is the generalized 0-eigenspace of x acting on M; it is stable under all of L because ad x is assumed locally nilpotent, so that every element of L lies in the generalized 0-eigenspace of ad x.

Equations

• Ado.locallyNilpotentSubmodule R M x hx = { toSubmodule := ((LieModule.toEnd R L M) x).maxGenEigenspace 0, lie_mem := ⋯ }

@[simp]

theorem Ado.mem_locallyNilpotentSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {x : L} {hx : ∀ (y : L), ∃ (k : ℕ), ((LieAlgebra.ad R L) x ^ k) y = 0} {m : M} : m ∈ locallyNilpotentSubmodule R M x hx ↔ ∃ (k : ℕ), ((LieModule.toEnd R L M) x ^ k) m = 0

theorem Ado.exists_pow_toEnd_eq_zero_of_isIrreducible {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieModule.IsIrreducible R L M] {x : L} (hx : ∀ (y : L), ∃ (k : ℕ), ((LieAlgebra.ad R L) x ^ k) y = 0) {m₀ : M} (hm₀ : m₀ ≠ 0) {k₀ : ℕ} (hk₀ : ((LieModule.toEnd R L M) x ^ k₀) m₀ = 0) (m : M) : ∃ (k : ℕ), ((LieModule.toEnd R L M) x ^ k) m = 0

Local nilpotence spreads over an irreducible module. If ad x is locally nilpotent and some nonzero vector of an irreducible module M is annihilated by a power of x, then every vector of M is.

Locally finite vectors

def Ado.locallyFiniteSubmodule (R : Type u) {L : Type v} (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Finite R L] (S : Set L) : LieSubmodule R L M

The vectors of M lying in some finitely generated R-submodule stable under bracketing with every element of S, as a Lie submodule of M.

Stability under all of L uses that L is a finite R-module: if N is finitely generated and S-stable, then N + ⁅L, N⁆ is again finitely generated and S-stable, and it contains ⁅y, m⁆ for every y : L and m ∈ N.

Equations

• Ado.locallyFiniteSubmodule R M S = { carrier := {m : M | ∃ (N : Submodule R M), N.FG ∧ (∀ x ∈ S, ∀ u ∈ N, ⁅x, u⁆ ∈ N) ∧ m ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯, lie_mem := ⋯ }

@[simp]

theorem Ado.mem_locallyFiniteSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Finite R L] {S : Set L} {m : M} : m ∈ locallyFiniteSubmodule R M S ↔ ∃ (N : Submodule R M), N.FG ∧ (∀ x ∈ S, ∀ u ∈ N, ⁅x, u⁆ ∈ N) ∧ m ∈ N

@[simp]

theorem Ado.locallyFiniteSubmodule_span {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Finite R L] (S : Set L) : locallyFiniteSubmodule R M ↑(Submodule.span R S) = locallyFiniteSubmodule R M S

Only the span of S matters: a subspace stable under S is stable under the R-submodule that S generates, the stability condition being linear in the bracketing element.

theorem Ado.locallyFiniteSubmodule_eq_top_of_isIrreducible {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Finite R L] [LieModule.IsIrreducible R L M] {S : Set L} {N₀ : Submodule R M} (hfg₀ : N₀.FG) (hst₀ : ∀ x ∈ S, ∀ u ∈ N₀, ⁅x, u⁆ ∈ N₀) {m₀ : M} (hm₀ : m₀ ≠ 0) (hmem₀ : m₀ ∈ N₀) : locallyFiniteSubmodule R M S = ⊤

Local finiteness spreads over an irreducible module. If some nonzero vector of an irreducible module lies in a finitely generated S-stable subspace, then every vector does.