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 #
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
- lie_algebra.is_engelian R L = ∀ (M : Type u₄) [_inst_10 : add_comm_group M] [_inst_11 : module R M] [_inst_12 : lie_ring_module L M] [_inst_11_1 : lie_module R L M], (∀ (x : L), is_nilpotent (⇑(lie_module.to_endomorphism R L M) x)) → lie_module.is_nilpotent R L M
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.
Engel's theorem.
Engel's theorem.