We discuss the theory of Lie algebras in Lean’s Mathlib library. Using nilpotency as the theme, we outline a computer formalisation of Engel’s theorem and an application to root space theory. We emphasise that all arguments work with coefficients in any commutative ring.
Notes
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
1 Introduction
In previous work [6], we reported on the formalisation of Lie algebras in Lean’s Mathlib library [8]. Whereas the aim of [6] was to give a high-level overview of the state of Mathlib’s Lie theory, our goal here is to use a particular aspect of Lie theory (nilpotency) as a means for illustrating two of Mathlib’s most important virtues: generality and unity. For example we shall see that Mathlib’s version of Engel’s theorem unifies the various versions of this result appearing in the informal literature, while demanding weaker hypotheses and providing a stronger result.
This article also presents an opportunity to highlight certain additions to Mathlib’s Lie algebra theory that have been made since [6]. To be precise, Mathlib’s Lie theory has grown from c.6000 lines to c.7500 lines since [6]. The most important additions are the proof of Engel’s theorem and its corollary (4) characterising Cartan subalgebras.
Advertisement
We briefly summarise some key context and refer the reader to the references for further discussion. Lean is an open-source, dependently-typed functional programming language and proof assistant. The principal developer is Leonardo de Moura at Microsoft Research. It uses a type theory similar to that of Coq for its logical foundation, see e.g., [2].
Mathlib [8] is an open-source, massively-collaborative library of formal mathematics written using Lean. As of June 2022, it contains c.900,000 lines of code, is steadily growing, and contains large quantities of contemporary undergraduate- and graduate-level mathematics.
Lie algebras are an important class of algebras which arise throughout mathematics and physics. Well-known to geometers as an abstraction of infinitesimal symmetry, Lie algebras show up throughout mathematics, occupying prominent roles across the subject, from number theory to differential geometry. They are also essential for understanding much of 20th Century physics, especially the Standard Model in particle physics. In addition, the beautiful classification of semisimple Lie algebras and their representations has made them an object of study in their own right.
As outlined in [6], Mathlib contains a substantial body of Lie algebra theory. The starting point is a pair of typeclasses which permit one to make the statement that a type L carries the structure of a Lie algebra over1 a commutative ring R. For the benefit of non-specialists we emphasise that Lie rings are not required to be associative2 and so are not rings in the sense in which the term is most often used. The formal definitions in Mathlib are as follows [src]:
×
Advertisement
We emphasise that no assumptions are made about the coefficients R except that they form a commutative ring. Practictioners of formal mathematics will be familiar with the value of making definitions as general as reasonably possible. Of course, if one also seeks to make theorems correspondingly general, then new arguments are often required. One of the points of this article is that this extra effort may yield unexpected benefits.
Our case study is Engel’s theorem which turns out to be true for any commutative ring R and to apply to a generalisation of nilpotency to Lie modules. As we shall see, the generalisation of nilpotency, from algebras to modules, is especially convenient as it unifies the various versions of Engel’s theorem that appear in the literature. In addition we obtain a slightly more powerful result; this is useful when it comes to applications and we give an example of this for root spaces in Sect. 5.
2 Lie Modules
Given a Lie algebra L, Mathlib’s definition of a Lie module3M of L is [src]:
Observe that we denote the action of an element x of a Lie algebra L on an element m of a Lie module M by [x, m]. This permits a uniform notation when regarding a Lie algebra as a module over itself.
Nilpotency is an important concept in algebra, with applications beyond what one might naïvely expect from the definitions. In the case of Lie algebras, the representation theory of nilpotent Lie algebras is both especially simple and especially important since semisimple Lie algebras are best understood as representations of certain nilpotent subalgebras, namely, Cartan subalgebras.5
3.1 Ideal Operations and Nilpotent Lie Modules
Given a Lie module M of a Lie algebra L, recall ([6] section 3) that for any ideal \(I \subseteq L\) and Lie submodule \(N \subseteq M\) we can form a new Lie submodule [src]:
$$\begin{aligned}{}[I, N] \subseteq M. \end{aligned}$$
It is the smallest Lie submodule of M containing all elements of the form [x, m] for all \(x \in I\) and \(m \in N\).
Informally, the lower central series of a Lie module M is the sequence of Lie submodules of M defined recursively as:
The lower central series is important because it provides a convenient way to define nilpotency [src]:
×
Unwinding the definitions, informally a Lie module M is nilpotent if and only if there exists a natural number k such that for any \(x_1, x_2, \ldots , x_k\) in L and any m in M:
An element a of an associative6 ring A is said to be nilpotent if there exists a natural number k such that:
$$\begin{aligned} a^k = 0. \end{aligned}$$
Given a Lie module M of a Lie algebra L, this concept of nilpotency for elements of the ring \(A = {{\,\textrm{End}\,}}(M)\) plays a central role in Engel’s theorem:
Definition
We say a Lie algebra L acts nilpotently on a Lie module M if the image of the natural map:
A trivial but important observation is that if M is a nilpotent Lie module then L acts nilpotently. Indeed, given any x in L, taking the constant sequence:
(Engel’s theorem) Let M be a Lie module over a Lie algebra L with coefficients in a commutative ring R. Suppose that L is Noetherian as an R-module. Then M is nilpotent if and only if L acts nilpotently on M.
This should be compared with traditional versions appearing e.g. in Serre [7] (I.4, Theorems 1, 2, 2’), Bourbaki [1] (I, 4.2, Theorem 1, Corollaries 1, 3), Fulton, Harris, [4] (9.2, Theorem 9.9, Exercise 9.10). For the sake of definiteness we give such a statement.
Theorem
(Engel’s theorem, traditional version)
(a)
Let L be a finite-dimensional Lie algebra with coefficients in a field. Then L is nilpotent if and only if it acts nilpotently on itself.
(b)
Let M be a non-trivial finite-dimensional vector space and suppose that \(L \subseteq {{\,\textrm{End}\,}}(M)\) is a Lie subalgebra consisting of nilpotent elements. Then there exists a non-zero element \(m_0\) in M such that:
$$\begin{aligned}{}[x, m_0] = 0 \quad \text{ for } \text{ all } \text{ x } \text{ in } \text{ L. } \end{aligned}$$
Taking \(M = L\) in our version recovers part (a) in the traditional statement. As explained in the discussion of Eq. (2), part (b) is also a trivial corollary of our version. We have thus unified parts (a) and (b) in the traditional version into a single result. Demanding the stronger property that M is nilpotent also turns out to simplify the proof as we get a stronger inductive hypothesis at the key step in the proof.
4.1 Engelian Lie Algebras
It is convenient to introduce some terminology.
Definition
We say a Lie algebra L is Engelian if any Lie module M on which L acts nilpotently is nilpotent.
In fact, this exposes a rough edge of Lean 3: quantification over typeclasses requires use of the ‘by exactI \(\forall \) pattern’ as well as the explicit mention of typeclasses that could be inferred (like add_comm_group, module etc). One would prefer to write simply \(\forall \)(M: u\({_{4}}\)), [[lie_module R L M]] rather than the three lines appearing above. This situation is likely to improve after Mathlib is migrated to Lean 4.
Using this new language, the non-trivial part of Engel’s theorem is the statement that Noetherian Lie algebras are Engelian: [src]
×
4.2 Passing to the Image in End(M)
We now fix a Noetherian Lie algebra L together with a Lie module M on which it acts nilpotently. The first step in the proof is to note that we may replace L with its image:
$$\begin{aligned} L' = {{\,\textrm{range}\,}}\phi \subseteq {{\,\textrm{End}\,}}(M), \end{aligned}$$
under the natural map:
$$\begin{aligned} \phi : L \rightarrow {{\,\textrm{End}\,}}(M). \end{aligned}$$
The proof is essentially tautological but the observation is important and the lemma is a good example of Lean’s typeclass mechanism working well.
Without the user doing anything, Lean recognises that (to_endomorphism R L M).range, i.e. \(L'\), is a Lie algebra and that M is naturally a Lie module over \(L'\). All of this is achieved by typeclass instances registered far away, with no direct connection to Engel’s theorem.
The passage from L to \(L'\) is useful because of the following lemma [src]:
(Note that an associative algebra A is naturally also a Lie algebra [src] which is why we may write lie_subalgebra R A. See also [6] section 5.) The proof follows from the binomial theorem. Taking \(A = {{\,\textrm{End}\,}}(M)\) the lemma states that \(L'\) acts nilpotently on itself.
×
4.3 The Main Argument
We introduce the set:
$$\begin{aligned} s = \{K \subseteq L' ~|~ K \text{ is } \text{ an } \text{ Engelian } \text{ Lie } \text{ subalgebra } \}, \end{aligned}$$
Our goal is to show that s contains \(L'\), regarded as a Lie subalgebra of itself. This is the top element \(\top \) in the complete lattice of Lie subalgebras.
×
Since s is non-empty (it contains the trivial Lie subalgebra) and \(L'\) is Noetherian, s contains a maximal element. We thus need only show that an element of s cannot be maximal when it is a proper subalgebra. In other words we must justify the following claim appearing in the Mathlib proof [src]:
×
Thus let K be a proper Engelian Lie subalgebra and consider the Lie module \(L' / K\) over K. Because \(L'\) acts nilpotently on itself, \(K \subseteq L'\) acts nilpotently on \(L'\) and thus also on \(L' / K\). Since K is Engelian, \(L' / K\) is nilpotent and thus by (2) there exists \(x \in L' - K\) such that:
$$\begin{aligned}{}[K, x] \subseteq K. \end{aligned}$$
(3)
Finally let:
$$\begin{aligned} K' = \{ \lambda x + \mu k ~|~ k \in K; \lambda , \mu \in R \}. \end{aligned}$$
Using (3) and recalling that \([x, x] = 0\) we see that:
\(K'\) is a Lie subalgebra of \(L'\),
\(K'\) strictly contains K,
K is an ideal in \(K'\).
To finish the argument we need only show that \(K'\) is Engelian. We thus fix a Lie module \(M'\) over \(K'\) on which \(K'\) acts nilpotently. We must show that \(M'\) is nilpotent. To do so, we apply the following lemma (whose proof is a simple induction) [src]:
with the roles of I, L played by K, \(K'\).
×
We see that if the lower central series of \(M'\) as a Lie module over K reaches zero, then its lower central central series over \(K'\) must also reach zero. Thus nilpotency over K (which follows since K is Engelian) ensures nilpotency over \(K'\), as required.
5 The Zero Root Space
As noted in [6] section 11, Mathlib contains definitions of and basic results about weight spaces and root spaces. Engel’s theorem was added to Mathlib for the purpose of advancing this theory. It may be instructive to outline this application.
Given a nilpotent Lie subgalgebra \(H \subseteq L\), a distinguished role is played by the zero root space. In Mathlib this is root_space H (0: H \(\rightarrow \)R)[src]; informally it is:
$$\begin{aligned} L^0 = \{ x ~|~ \exists k, \forall y \in H, {{\,\textrm{ad}\,}}_y^k(x) = 0 \} \subseteq L. \end{aligned}$$
Any root space is a H-submodule of L but more is true for the zero root space; it is a Lie subalgebra [src]:
One always has \(H \subseteq L^0\) and it is easy to see that if \(H = L^0\) then H is a Cartan subalgebra. When L is Noetherian, Engel’s theorem shows that the converse holds:
$$\begin{aligned} H = L^0 \iff H \text{ is } \text{ a } \text{ Cartan } \text{ subalgebra. } \end{aligned}$$
(4)
The literature appears only to contain proofs of this result when the coefficients are a field. Moreover the arguments in the literature cannot be used since they argue inductively using dimension — a concept that does not exist over general coefficients. Fortunately with our version of Engel’s theorem, the proof is almost trivial.
The point is that if L is Noetherian, then H acts nilpotently on \(L^0\) and so by Engel’s theorem, \(L^0\) is nilpotent as a Lie module over H. Mathlib actually contains the following slightly more general result which holds for any Noetherian Lie module M[src]:
×
Once we know that \(L^0\) is nilpotent over H, the self-normalizing property of a Cartan subalgebra ensures that H cannot be a strict submodule and the result is immediate.
6 Conclusion
Having extolled the virtues of generality and unity, we should emphasise that in some sense they are two sides of the same coin. For example, the theory of root spaces discussed here depends on Mathlib’s theory of eigenspaces. This same theory of eigenspaces is also used in Mathlib’s library of functional analysis [3]. This is only possible because the theory of eigenspaces was developed quite generally (before either application existed). We thus enjoy a synergy: any lemma added by one consumer of the eigenspace theory is automatically available to the other.
Although we have stated the required finiteness condition for Engel’s theorem as the requirement that L be Noetherian as an R module, the argument actually needs only the weaker condition that the lattice of Lie subalgebras of L possesses a maximality property.9
Our version of Engel’s theorem seems not to exist in the literature. One notable close pass is an old paper of Zorn [10] where the result is proved for Lie rings (but not for their Lie modules). Another interesting paper is Jacobson [5]. In place of our:
$$\begin{aligned} L' \subseteq {{\,\textrm{End}\,}}(M), \end{aligned}$$
he proves Engel’s theorem for what he calls a \(\Phi \)-subring:
On the one hand Jacobson’s result is more general since the class of \(\Phi \)-subrings includes Lie subrings of associative rings as a special case. On the other hand it is less general since he obtains his result subject to the much more restrictive assumption that the lattice of ideals of the enclosing ring \(\mathfrak {U}\) possesses a minimality condition whereas we require only that the lattice of subalgebras of \(L'\) possesses a maximality condition.
Finally we should mention that there is an important setting where Engel-type results for Lie rings play a central role. See for example Zel’manov’s breakthrough [9].
Acknowledgements
I am grateful to Kevin Buzzard at Imperial College whose Excellence Fund in Frontier Research grant funded this work. I am also grateful to the anonymous referees for numerous helpful remarks. I declare that this article is the sole work of the named author and that I have no conflicts of interest pertaining to any of the work discussed here. All code is available in the master branch of the open-source Mathlib repository, with links appearing throughout the text.
Declarations
Competing Interests
The authors declare no competing interests.
Open AccessThis article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Most of the theory of semisimple Lie algebras has yet to be formalised. Adding this material to Mathlib following, say [7], would be a worthy endeavour.
We note in passing that the concept generalises to non-associative rings and that the relation \([x, x] = 0\) means that all elements x of a Lie algebra are nilpotent (taking \(k = 2\)). This fact is partly responsible for the elevated role that nilpotency plays in Lie theory.
The universe u\({_{4}}\) appearing is not significant and merely reflects Mathlib’s standard universe polymorphism. Lean can handle such polymorphism automatically so one could (and probably should) replace Type u\({_{4}}\) with Type*.
