Solvable Lie algebras #
Like groups, Lie algebras admit a natural concept of solvability. We define this here via the derived series and prove some related results. We also define the radical of a Lie algebra and prove that it is solvable when the Lie algebra is Noetherian.
Main definitions #
lie_algebra.derived_series_of_ideal
lie_algebra.derived_series
lie_algebra.is_solvable
lie_algebra.is_solvable_add
lie_algebra.radical
lie_algebra.radical_is_solvable
lie_algebra.derived_length_of_ideal
lie_algebra.derived_length
lie_algebra.derived_abelian_of_ideal
Tags #
lie algebra, derived series, derived length, solvable, radical
A generalisation of the derived series of a Lie algebra, whose zeroth term is a specified ideal.
It can be more convenient to work with this generalisation when considering the derived series of an ideal since it provides a type-theoretic expression of the fact that the terms of the ideal's derived series are also ideals of the enclosing algebra.
See also lie_ideal.derived_series_eq_derived_series_of_ideal_comap
and
lie_ideal.derived_series_eq_derived_series_of_ideal_map
below.
The derived series of Lie ideals of a Lie algebra.
- solvable : ∃ (k : ℕ), lie_algebra.derived_series R L k = ⊥
A Lie algebra is solvable if its derived series reaches 0 (in a finite number of steps).
The (solvable) radical of Lie algebra is the Sup
of all solvable ideals.
Equations
- lie_algebra.radical R L = has_Sup.Sup {I : lie_ideal R L | lie_algebra.is_solvable R ↥I}
Instances for ↥lie_algebra.radical
The radical of a Noetherian Lie algebra is solvable.
The →
direction of this lemma is actually true without the is_noetherian
assumption.
Given a solvable Lie ideal I
with derived series I = D₀ ≥ D₁ ≥ ⋯ ≥ Dₖ = ⊥
, this is the
natural number k
(the number of inclusions).
For a non-solvable ideal, the value is 0.
Equations
- lie_algebra.derived_length_of_ideal R L I = has_Inf.Inf {k : ℕ | lie_algebra.derived_series_of_ideal R L k I = ⊥}
The derived length of a Lie algebra is the derived length of its 'top' Lie ideal.
See also lie_algebra.derived_length_eq_derived_length_of_ideal
.
Given a solvable Lie ideal I
with derived series I = D₀ ≥ D₁ ≥ ⋯ ≥ Dₖ = ⊥
, this is the
k-1
th term in the derived series (and is therefore an Abelian ideal contained in I
).
For a non-solvable ideal, this is the zero ideal, ⊥
.
Equations
- lie_algebra.derived_abelian_of_ideal I = lie_algebra.derived_abelian_of_ideal._match_1 I (lie_algebra.derived_length_of_ideal R L I)
- lie_algebra.derived_abelian_of_ideal._match_1 I (k + 1) = lie_algebra.derived_series_of_ideal R L k I
- lie_algebra.derived_abelian_of_ideal._match_1 I 0 = ⊥