# Documentation

Mathlib.Algebra.Lie.Solvable

# 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 #

• LieAlgebra.derivedSeriesOfIdeal
• LieAlgebra.derivedSeries
• LieAlgebra.IsSolvable
• LieAlgebra.isSolvableAdd
• LieAlgebra.radical
• LieAlgebra.radicalIsSolvable
• LieAlgebra.derivedLengthOfIdeal
• LieAlgebra.derivedLength
• LieAlgebra.derivedAbelianOfIdeal

## 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.

See also LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_comap and LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_map below.

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

The derived series of Lie ideals of a Lie algebra.

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 { x // x 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 { x // x I } k = LieIdeal.comap () ()
theorem LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_map {R : Type u} {L : Type v} [] [] [] (I : LieIdeal R L) (k : ) :
LieIdeal.map () (LieAlgebra.derivedSeries R { x // x I } k) =
theorem LieIdeal.derivedSeries_eq_bot_iff {R : Type u} {L : Type v} [] [] [] (I : LieIdeal R L) (k : ) :
LieAlgebra.derivedSeries R { x // x I } 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 { x // x I } k = ) (hJ : LieAlgebra.derivedSeries R { x // x J } l = ) :
LieAlgebra.derivedSeries R { x // x ↑(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) [] [] [] :
• solvable : k,

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

Instances
instance LieAlgebra.isSolvableBot (R : Type u) (L : Type v) [] [] [] :
instance LieAlgebra.isSolvableAdd (R : Type u) (L : Type v) [] [] [] {I : LieIdeal R L} {J : LieIdeal R L} [hI : LieAlgebra.IsSolvable R { x // x I }] [hJ : LieAlgebra.IsSolvable R { x // x J }] :
LieAlgebra.IsSolvable R { x // x I + J }
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) :
LieAlgebra.IsSolvable R { x // x J }LieAlgebra.IsSolvable R { x // x I }
instance LieAlgebra.ofAbelianIsSolvable (R : Type u) (L : Type v) [] [] [] [] :
def LieAlgebra.radical (R : Type u) (L : Type v) [] [] [] :

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

Instances For
instance LieAlgebra.radicalIsSolvable (R : Type u) (L : Type v) [] [] [] [] :
LieAlgebra.IsSolvable R { x // x ↑() }

The radical of a Noetherian Lie algebra is solvable.

theorem LieAlgebra.LieIdeal.solvable_iff_le_radical (R : Type u) (L : Type v) [] [] [] [] (I : LieIdeal R L) :
LieAlgebra.IsSolvable R { x // x I } I

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

theorem LieAlgebra.center_le_radical (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.

Instances For
@[inline, reducible]
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.

See also LieAlgebra.derivedLength_eq_derivedLengthOfIdeal.

Instances For
theorem LieAlgebra.derivedSeries_of_derivedLength_succ (R : Type u) (L : Type v) [] [] [] (I : LieIdeal R L) (k : ) :
= k + 1 IsLieAbelian { x // x ↑() }
theorem LieAlgebra.derivedLength_eq_derivedLengthOfIdeal (R : Type u) (L : Type v) [] [] [] (I : LieIdeal R L) :
LieAlgebra.derivedLength R { x // x I } =
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, ⊥.

Instances For
theorem LieAlgebra.abelian_derivedAbelianOfIdeal {R : Type u} {L : Type v} [] [] [] (I : LieIdeal R L) :
IsLieAbelian { x // }
theorem LieAlgebra.derivedLength_zero {R : Type u} {L : Type v} [] [] [] (I : LieIdeal R L) [hI : LieAlgebra.IsSolvable R { x // x I }] :
I =
theorem LieAlgebra.abelian_of_solvable_ideal_eq_bot_iff {R : Type u} {L : Type v} [] [] [] (I : LieIdeal R L) [h : LieAlgebra.IsSolvable R { x // x I }] :