Engel's theorem

This file contains a proof of Engel's theorem providing necessary and sufficient conditions for Lie algebras and Lie modules to be nilpotent.

The key result LieModule.isNilpotent_iff_forall says that if M is a Lie module of a Noetherian Lie algebra L, then M is nilpotent iff the image of L → End(M) consists of nilpotent elements. In the special case that we have the adjoint representation M = L, this says that a Lie algebra is nilpotent iff ad x : End(L) is nilpotent for all x : L.

Engel's theorem is true for any coefficients (i.e., it is really a theorem about Lie rings) and so we work with coefficients in any commutative ring R throughout.

On the other hand, Engel's theorem is not true for infinite-dimensional Lie algebras and so a finite-dimensionality assumption is required. We prove the theorem subject to the assumption that the Lie algebra is Noetherian as an R-module, though actually we only need the slightly weaker property that the relation > is well-founded on the complete lattice of Lie subalgebras.

Remarks about the proof

Engel's theorem is usually proved in the special case that the coefficients are a field, and uses an inductive argument on the dimension of the Lie algebra. One begins by choosing either a maximal proper Lie subalgebra (in some proofs) or a maximal nilpotent Lie subalgebra (in other proofs, at the cost of obtaining a weaker end result).

Since we work with general coefficients, we cannot induct on dimension and an alternate approach must be taken. The key ingredient is the concept of nilpotency, not just for Lie algebras, but for Lie modules. Using this concept, we define an Engelian Lie algebra LieAlgebra.IsEngelian to be one for which a Lie module is nilpotent whenever the action consists of nilpotent endomorphisms. The argument then proceeds by selecting a maximal Engelian Lie subalgebra and showing that it cannot be proper.

The first part of the traditional statement of Engel's theorem consists of the statement that if M is a non-trivial R-module and L ⊆ End(M) is a finite-dimensional Lie subalgebra of nilpotent elements, then there exists a non-zero element m : M that is annihilated by every element of L. This follows trivially from the result established here LieModule.isNilpotent_iff_forall, that M is a nilpotent Lie module over L, since the last non-zero term in the lower central series will consist of such elements m (see: LieModule.nontrivial_max_triv_of_isNilpotent). It seems that this result has not previously been established at this level of generality.

The second part of the traditional statement of Engel's theorem concerns nilpotency of the Lie algebra and a proof of this for general coefficients appeared in the literature as long ago as 1937. This also follows trivially from LieModule.isNilpotent_iff_forall simply by taking M = L.

It is pleasing that the two parts of the traditional statements of Engel's theorem are thus unified into a single statement about nilpotency of Lie modules. This is not usually emphasised.

Main definitions

• LieAlgebra.IsEngelian
• LieAlgebra.isEngelian_of_isNoetherian
• LieModule.isNilpotent_iff_forall
• LieAlgebra.isNilpotent_iff_forall

theorem LieSubmodule.exists_smul_add_of_span_sup_eq_top {R : Type u₁} {L : Type u₂} [CommRing R] [LieRing L] [LieAlgebra R L] {I : LieIdeal R L} {x : L} (hxI : Submodule.span R {x} ⊔ (lieIdealSubalgebra R L I).toSubmodule = ⊤) (y : L) : ∃ (t : R), ∃ z ∈ I, y = t • x + z

theorem LieSubmodule.lie_top_eq_of_span_sup_eq_top {R : Type u₁} {L : Type u₂} {M : Type u₄} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {I : LieIdeal R L} {x : L} (hxI : Submodule.span R {x} ⊔ (lieIdealSubalgebra R L I).toSubmodule = ⊤) (N : LieSubmodule R L M) : ↑⁅⊤, N⁆ = Submodule.map ((LieModule.toEnd R L M) x) ↑N ⊔ ↑⁅I, N⁆

theorem LieSubmodule.lcs_le_lcs_of_is_nilpotent_span_sup_eq_top {R : Type u₁} {L : Type u₂} {M : Type u₄} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {I : LieIdeal R L} {x : L} (hxI : Submodule.span R {x} ⊔ (lieIdealSubalgebra R L I).toSubmodule = ⊤) {n : ℕ} {i : ℕ} {j : ℕ} (hxn : (LieModule.toEnd R L M) x ^ n = 0) (hIM : LieModule.lowerCentralSeries R L M i ≤ I.lcs M j) : LieModule.lowerCentralSeries R L M (i + n) ≤ I.lcs M (j + 1)

theorem LieSubmodule.isNilpotentOfIsNilpotentSpanSupEqTop {R : Type u₁} {L : Type u₂} {M : Type u₄} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {I : LieIdeal R L} {x : L} (hxI : Submodule.span R {x} ⊔ (lieIdealSubalgebra R L I).toSubmodule = ⊤) (hnp : IsNilpotent ((LieModule.toEnd R L M) x)) (hIM : LieModule.IsNilpotent R (↥I) M) : LieModule.IsNilpotent R L M

def LieAlgebra.IsEngelian (R : Type u₁) (L : Type u₂) [CommRing R] [LieRing L] [LieAlgebra R L] : Prop

A Lie algebra L is said to be Engelian if a sufficient condition for any L-Lie module M to be nilpotent is that the image of the map L → End(M) consists of nilpotent elements.

Engel's theorem LieAlgebra.isEngelian_of_isNoetherian states that any Noetherian Lie algebra is Engelian.

Equations

• One or more equations did not get rendered due to their size.

theorem LieAlgebra.isEngelian_of_subsingleton {R : Type u₁} {L : Type u₂} [CommRing R] [LieRing L] [LieAlgebra R L] [Subsingleton L] : LieAlgebra.IsEngelian R L

theorem Function.Surjective.isEngelian {R : Type u₁} {L : Type u₂} {L₂ : Type u₃} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] {f : L →ₗ⁅R⁆ L₂} (hf : Function.Surjective ⇑f) (h : LieAlgebra.IsEngelian R L) : LieAlgebra.IsEngelian R L₂

theorem LieEquiv.isEngelian_iff {R : Type u₁} {L : Type u₂} {L₂ : Type u₃} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (e : L ≃ₗ⁅R⁆ L₂) : LieAlgebra.IsEngelian R L ↔ LieAlgebra.IsEngelian R L₂

theorem LieAlgebra.exists_engelian_lieSubalgebra_of_lt_normalizer {R : Type u₁} {L : Type u₂} [CommRing R] [LieRing L] [LieAlgebra R L] {K : LieSubalgebra R L} (hK₁ : LieAlgebra.IsEngelian R ↥K) (hK₂ : K < K.normalizer) : ∃ (K' : LieSubalgebra R L), LieAlgebra.IsEngelian R ↥K' ∧ K < K'

theorem LieAlgebra.isEngelian_of_isNoetherian {R : Type u₁} {L : Type u₂} [CommRing R] [LieRing L] [LieAlgebra R L] [IsNoetherian R L] : LieAlgebra.IsEngelian R L

Engel's theorem.

Note that this implies all traditional forms of Engel's theorem via LieModule.nontrivial_max_triv_of_isNilpotent, LieModule.isNilpotent_iff_forall, LieAlgebra.isNilpotent_iff_forall.

theorem LieModule.isNilpotent_iff_forall {R : Type u₁} {L : Type u₂} {M : Type u₄} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsNoetherian R L] : LieModule.IsNilpotent R L M ↔ ∀ (x : L), IsNilpotent ((LieModule.toEnd R L M) x)

Engel's theorem.

See also LieModule.isNilpotent_iff_forall' which assumes that M is Noetherian instead of L.

theorem LieModule.isNilpotent_iff_forall' {R : Type u₁} {L : Type u₂} {M : Type u₄} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsNoetherian R M] : LieModule.IsNilpotent R L M ↔ ∀ (x : L), IsNilpotent ((LieModule.toEnd R L M) x)

Engel's theorem.

theorem LieAlgebra.isNilpotent_iff_forall {R : Type u₁} {L : Type u₂} [CommRing R] [LieRing L] [LieAlgebra R L] [IsNoetherian R L] : LieAlgebra.IsNilpotent R L ↔ ∀ (x : L), IsNilpotent ((LieAlgebra.ad R L) x)

Engel's theorem.