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
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
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
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
The first part of the traditional statement of Engel's theorem consists of the statement that if
is a non-trivial
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
This follows trivially from the result established here
M is a nilpotent Lie module over
L, since the last non-zero term in the lower central series
will consist of such elements
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
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 #
A Lie algebra
L is said to be Engelian if a sufficient condition for any
be nilpotent is that the image of the map
L → End(M) consists of nilpotent elements.
lie_algebra.is_engelian_of_is_noetherian states that any Noetherian Lie algebra is