Nilpotent Lie algebras #
Like groups, Lie algebras admit a natural concept of nilpotency. More generally, any Lie module carries a natural concept of nilpotency. We define these here via the lower central series.
Main definitions #
Tags #
lie algebra, lower central series, nilpotent
A generalisation of the lower central series. The zeroth term is a specified Lie submodule of
a Lie module. In the case when we specify the top ideal ⊤
of the Lie algebra, regarded as a Lie
module over itself, we get the usual lower central series of a Lie algebra.
It can be more convenient to work with this generalisation when considering the lower central series of a Lie submodule, regarded as a Lie module in its own right, since it provides a type-theoretic expression of the fact that the terms of the Lie submodule's lower central series are also Lie submodules of the enclosing Lie module.
See also lie_module.lower_central_series_eq_lcs_comap
and
lie_module.lower_central_series_map_eq_lcs
below, as well as lie_submodule.ucs
.
Equations
- lie_submodule.lcs k = ((λ (N : lie_submodule R L M), ⁅⊤,N⁆)^[k])
The lower central series of Lie submodules of a Lie module.
Equations
- lie_module.lower_central_series R L M k = lie_submodule.lcs k ⊤
- nilpotent : ∃ (k : ℕ), lie_module.lower_central_series R L M k = ⊥
A Lie module is nilpotent if its lower central series reaches 0 (in a finite number of steps).
For a nilpotent Lie module, the weight space of the 0 weight is the whole module.
This result will be used downstream to show that weight spaces are Lie submodules, at which time it will be possible to state it in the language of weight spaces.
If the quotient of a Lie module M
by a Lie submodule on which the Lie algebra acts trivially
is nilpotent then M
is nilpotent.
This is essentially the Lie module equivalent of the fact that a central
extension of nilpotent Lie algebras is nilpotent. See lie_algebra.nilpotent_of_nilpotent_quotient
below for the corresponding result for Lie algebras.
Given a nilpotent Lie module M
with lower central series M = C₀ ≥ C₁ ≥ ⋯ ≥ Cₖ = ⊥
, this is
the natural number k
(the number of inclusions).
For a non-nilpotent module, we use the junk value 0.
Equations
- lie_module.nilpotency_length R L M = has_Inf.Inf {k : ℕ | lie_module.lower_central_series R L M k = ⊥}
Given a non-trivial nilpotent Lie module M
with lower central series
M = C₀ ≥ C₁ ≥ ⋯ ≥ Cₖ = ⊥
, this is the k-1
th term in the lower central series (the last
non-trivial term).
For a trivial or non-nilpotent module, this is the bottom submodule, ⊥
.
Equations
- lie_module.lower_central_series_last R L M = lie_module.lower_central_series_last._match_1 R L M (lie_module.nilpotency_length R L M)
- lie_module.lower_central_series_last._match_1 R L M (k + 1) = lie_module.lower_central_series R L M k
- lie_module.lower_central_series_last._match_1 R L M 0 = ⊥
The upper (aka ascending) central series.
See also lie_submodule.lcs
.
Equations
If a Lie module M
contains a self-centralizing Lie submodule N
, then all terms of the upper
central series of M
are contained in N
.
An important instance of this situation arises from a Cartan subalgebra H ⊆ L
with the roles of
L
, M
, N
played by H
, L
, H
, respectively.
We say a Lie algebra is nilpotent when it is nilpotent as a Lie module over itself via the adjoint representation.
Given an ideal I
of a Lie algebra L
, the lower central series of L ⧸ I
is the same
whether we regard L ⧸ I
as an L
module or an L ⧸ I
module.
TODO: This result obviously generalises but the generalisation requires the missing definition of morphisms between Lie modules over different Lie algebras.
Note that the below inequality can be strict. For example the ideal of strictly-upper-triangular
2x2 matrices inside the Lie algebra of upper-triangular 2x2 matrices with k = 1
.
A central extension of nilpotent Lie algebras is nilpotent.
Note that this result is not quite a special case of
lie_module.is_nilpotent_range_to_endomorphism_iff
which concerns nilpotency of the
(ad R L).range
-module L
, whereas this result concerns nilpotency of the (ad R L).range
-module
(ad R L).range
.
Given a Lie module M
over a Lie algebra L
together with an ideal I
of L
, this is the
lower central series of M
as an I
-module. The advantage of using this definition instead of
lie_module.lower_central_series R I M
is that its terms are Lie submodules of M
as an
L
-module, rather than just as an I
-module.
See also lie_ideal.coe_lcs_eq
.