# mathlib3documentation

algebra.lie.engel

# Engel's theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 lie_module.is_nilpotent_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 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 lie_algebra.is_engelian 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 lie_module.is_nilpotent_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: lie_module.nontrivial_max_triv_of_is_nilpotent). 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 lie_module.is_nilpotent_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 #

• lie_algebra.is_engelian
• lie_algebra.is_engelian_of_is_noetherian
• lie_module.is_nilpotent_iff_forall
• lie_algebra.is_nilpotent_iff_forall
theorem lie_submodule.exists_smul_add_of_span_sup_eq_top {R : Type u₁} {L : Type u₂} [comm_ring R] [lie_ring L] [ L] {I : L} {x : L} (hxI : {x} I = ) (y : L) :
(t : R) (z : L) (H : z I), y = t x + z
theorem lie_submodule.lie_top_eq_of_span_sup_eq_top {R : Type u₁} {L : Type u₂} {M : Type u₄} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] {I : L} {x : L} (hxI : {x} I = ) (N : M) :
theorem lie_submodule.lcs_le_lcs_of_is_nilpotent_span_sup_eq_top {R : Type u₁} {L : Type u₂} {M : Type u₄} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] {I : L} {x : L} (hxI : {x} I = ) {n i j : } (hxn : M) x ^ n = 0) (hIM : I.lcs M j) :
(i + n) I.lcs M (j + 1)
theorem lie_submodule.is_nilpotent_of_is_nilpotent_span_sup_eq_top {R : Type u₁} {L : Type u₂} {M : Type u₄} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] {I : L} {x : L} (hxI : {x} I = ) (hnp : is_nilpotent ( M) x)) (hIM : M) :
def lie_algebra.is_engelian (R : Type u₁) (L : Type u₂) [comm_ring R] [lie_ring L] [ 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 lie_algebra.is_engelian_of_is_noetherian states that any Noetherian Lie algebra is Engelian.

Equations
theorem lie_algebra.is_engelian_of_subsingleton {R : Type u₁} {L : Type u₂} [comm_ring R] [lie_ring L] [ L] [subsingleton L] :
theorem function.surjective.is_engelian {R : Type u₁} {L : Type u₂} {L₂ : Type u₃} [comm_ring R] [lie_ring L] [ L] [lie_ring L₂] [ L₂] {f : L →ₗ⁅R L₂} (hf : function.surjective f) (h : L) :
theorem lie_equiv.is_engelian_iff {R : Type u₁} {L : Type u₂} {L₂ : Type u₃} [comm_ring R] [lie_ring L] [ L] [lie_ring L₂] [ L₂] (e : L ≃ₗ⁅R L₂) :
theorem lie_algebra.exists_engelian_lie_subalgebra_of_lt_normalizer {R : Type u₁} {L : Type u₂} [comm_ring R] [lie_ring L] [ L] {K : L} (hK₁ : K) (hK₂ : K < K.normalizer) :
(K' : L) (hK' : , K < K'
theorem lie_algebra.is_engelian_of_is_noetherian {R : Type u₁} {L : Type u₂} [comm_ring R] [lie_ring L] [ L] [ L] :

Engel's theorem.

Note that this implies all traditional forms of Engel's theorem via lie_module.nontrivial_max_triv_of_is_nilpotent, lie_module.is_nilpotent_iff_forall, lie_algebra.is_nilpotent_iff_forall.

theorem lie_module.is_nilpotent_iff_forall {R : Type u₁} {L : Type u₂} {M : Type u₄} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] [ L] :
(x : L), is_nilpotent ( M) x)

Engel's theorem.

theorem lie_algebra.is_nilpotent_iff_forall {R : Type u₁} {L : Type u₂} [comm_ring R] [lie_ring L] [ L] [ L] :
(x : L), is_nilpotent ( L) x)

Engel's theorem.