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.

Tags #

lie algebra, derived series, derived length, solvable, radical

def LieAlgebra.derivedSeriesOfIdeal (R : Type u) (L : Type v) [] [] [] (k : ) :
LieIdeal R LLieIdeal R L

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.

Equations
Instances For
@[simp]
theorem LieAlgebra.derivedSeriesOfIdeal_zero (R : Type u) (L : Type v) [] [] [] (I : LieIdeal R L) :
= I
@[simp]
theorem LieAlgebra.derivedSeriesOfIdeal_succ (R : Type u) (L : Type v) [] [] [] (I : LieIdeal R L) (k : ) :
@[reducible, inline]
abbrev LieAlgebra.derivedSeries (R : Type u) (L : Type v) [] [] [] (k : ) :

The derived series of Lie ideals of a Lie algebra.

Equations
Instances For
theorem LieAlgebra.derivedSeries_def (R : Type u) (L : Type v) [] [] [] (k : ) :
theorem LieAlgebra.derivedSeriesOfIdeal_add {R : Type u} {L : Type v} [] [] [] (I : LieIdeal R L) (k : ) (l : ) :
theorem LieAlgebra.derivedSeriesOfIdeal_le {R : Type u} {L : Type v} [] [] [] {I : LieIdeal R L} {J : LieIdeal R L} {k : } {l : } (h₁ : I J) (h₂ : l k) :
theorem LieAlgebra.derivedSeriesOfIdeal_succ_le {R : Type u} {L : Type v} [] [] [] (I : LieIdeal R L) (k : ) :
theorem LieAlgebra.derivedSeriesOfIdeal_le_self {R : Type u} {L : Type v} [] [] [] (I : LieIdeal R L) (k : ) :
I
theorem LieAlgebra.derivedSeriesOfIdeal_mono {R : Type u} {L : Type v} [] [] [] {I : LieIdeal R L} {J : LieIdeal R L} (h : I J) (k : ) :
theorem LieAlgebra.derivedSeriesOfIdeal_antitone {R : Type u} {L : Type v} [] [] [] (I : LieIdeal R L) {k : } {l : } (h : l k) :
theorem LieAlgebra.derivedSeriesOfIdeal_add_le_add {R : Type u} {L : Type v} [] [] [] (I : LieIdeal R L) (J : LieIdeal R L) (k : ) (l : ) :
theorem LieAlgebra.derivedSeries_of_bot_eq_bot {R : Type u} {L : Type v} [] [] [] (k : ) :
theorem LieAlgebra.abelian_iff_derived_one_eq_bot {R : Type u} {L : Type v} [] [] [] (I : LieIdeal R L) :
IsLieAbelian I
theorem LieAlgebra.abelian_iff_derived_succ_eq_bot {R : Type u} {L : Type v} [] [] [] (I : LieIdeal R L) (k : ) :
theorem LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_comap {R : Type u} {L : Type v} [] [] [] (I : LieIdeal R L) (k : ) :
LieAlgebra.derivedSeries R (I) k = LieIdeal.comap I.incl ()
theorem LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_map {R : Type u} {L : Type v} [] [] [] (I : LieIdeal R L) (k : ) :
LieIdeal.map I.incl (LieAlgebra.derivedSeries R (I) k) =
theorem LieIdeal.derivedSeries_eq_bot_iff {R : Type u} {L : Type v} [] [] [] (I : LieIdeal R L) (k : ) :
theorem LieIdeal.derivedSeries_add_eq_bot {R : Type u} {L : Type v} [] [] [] {k : } {l : } {I : LieIdeal R L} {J : LieIdeal R L} (hI : LieAlgebra.derivedSeries R (I) k = ) (hJ : LieAlgebra.derivedSeries R (J) l = ) :
LieAlgebra.derivedSeries R ((I + J)) (k + l) =
theorem LieIdeal.derivedSeries_map_le {R : Type u} {L : Type v} {L' : Type w₁} [] [] [] [LieRing L'] [LieAlgebra R L'] {f : L' →ₗ⁅R L} (k : ) :
theorem LieIdeal.derivedSeries_map_eq {R : Type u} {L : Type v} {L' : Type w₁} [] [] [] [LieRing L'] [LieAlgebra R L'] {f : L' →ₗ⁅R L} (k : ) (h : ) :
class LieAlgebra.IsSolvable (R : Type u) (L : Type v) [] [] [] :

A Lie algebra is solvable if its derived series reaches 0 (in a finite number of steps).

• solvable : ∃ (k : ),
Instances
theorem LieAlgebra.IsSolvable.solvable {R : Type u} {L : Type v} [] [] [] [self : ] :
∃ (k : ),
instance LieAlgebra.isSolvableBot (R : Type u) (L : Type v) [] [] [] :
Equations
• =
instance LieAlgebra.isSolvableAdd (R : Type u) (L : Type v) [] [] [] {I : LieIdeal R L} {J : LieIdeal R L} [hI : ] [hJ : ] :
Equations
• =
theorem Function.Injective.lieAlgebra_isSolvable {R : Type u} {L : Type v} {L' : Type w₁} [] [] [] [LieRing L'] [LieAlgebra R L'] {f : L' →ₗ⁅R L} [h₁ : ] (h₂ : ) :
theorem Function.Surjective.lieAlgebra_isSolvable {R : Type u} {L : Type v} {L' : Type w₁} [] [] [] [LieRing L'] [LieAlgebra R L'] {f : L' →ₗ⁅R L} [h₁ : ] (h₂ : ) :
theorem LieHom.isSolvable_range {R : Type u} {L : Type v} {L' : Type w₁} [] [] [] [LieRing L'] [LieAlgebra R L'] (f : L' →ₗ⁅R L) [] :
theorem LieAlgebra.solvable_iff_equiv_solvable {R : Type u} {L : Type v} {L' : Type w₁} [] [] [] [LieRing L'] [LieAlgebra R L'] (e : L' ≃ₗ⁅R L) :
theorem LieAlgebra.le_solvable_ideal_solvable {R : Type u} {L : Type v} [] [] [] {I : LieIdeal R L} {J : LieIdeal R L} (h₁ : I J) :
@[instance 100]
instance LieAlgebra.ofAbelianIsSolvable (R : Type u) (L : Type v) [] [] [] [] :
Equations
• =
def LieAlgebra.radical (R : Type u) (L : Type v) [] [] [] :

The (solvable) radical of Lie algebra is the sSup of all solvable ideals.

Equations
Instances For
instance LieAlgebra.radicalIsSolvable (R : Type u) (L : Type v) [] [] [] [] :

The radical of a Noetherian Lie algebra is solvable.

Equations
• =
theorem LieAlgebra.LieIdeal.solvable_iff_le_radical (R : Type u) (L : Type v) [] [] [] [] (I : LieIdeal R L) :
I

The direction of this lemma is actually true without the IsNoetherian assumption.

theorem LieAlgebra.center_le_radical (R : Type u) (L : Type v) [] [] [] :
instance LieAlgebra.instIsSolvableSubtypeMemLieSubalgebraTop (R : Type u) (L : Type v) [] [] [] [] :
Equations
• =
@[simp]
theorem LieAlgebra.radical_eq_top_of_isSolvable (R : Type u) (L : Type v) [] [] [] [] :
noncomputable def LieAlgebra.derivedLengthOfIdeal (R : Type u) (L : Type v) [] [] [] (I : LieIdeal R L) :

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
Instances For
@[reducible, inline]
noncomputable abbrev LieAlgebra.derivedLength (R : Type u) (L : Type v) [] [] [] :

The derived length of a Lie algebra is the derived length of its 'top' Lie ideal.

Equations
Instances For
theorem LieAlgebra.derivedSeries_of_derivedLength_succ (R : Type u) (L : Type v) [] [] [] (I : LieIdeal R L) (k : ) :
= k + 1 IsLieAbelian ()
theorem LieAlgebra.derivedLength_eq_derivedLengthOfIdeal (R : Type u) (L : Type v) [] [] [] (I : LieIdeal R L) :
noncomputable def LieAlgebra.derivedAbelianOfIdeal {R : Type u} {L : Type v} [] [] [] (I : LieIdeal R L) :

Given a solvable Lie ideal I with derived series I = D₀ ≥ D₁ ≥ ⋯ ≥ Dₖ = ⊥, this is the k-1th 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
• = match with | 0 => | k.succ =>
Instances For
theorem LieAlgebra.abelian_derivedAbelianOfIdeal {R : Type u} {L : Type v} [] [] [] (I : LieIdeal R L) :
theorem LieAlgebra.derivedLength_zero {R : Type u} {L : Type v} [] [] [] (I : LieIdeal R L) [hI : ] :
I =
theorem LieAlgebra.abelian_of_solvable_ideal_eq_bot_iff {R : Type u} {L : Type v} [] [] [] (I : LieIdeal R L) [h : ] :