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) [CommRing R] [LieRing L] [LieAlgebra R L] (k : ℕ) : LieIdeal R L → LieIdeal 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.

Equations

• LieAlgebra.derivedSeriesOfIdeal R L k = (fun (I : LieIdeal R L) => ⁅I, I⁆)^[k]

@[simp]

theorem LieAlgebra.derivedSeriesOfIdeal_zero (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : LieAlgebra.derivedSeriesOfIdeal R L 0 I = I

@[simp]

theorem LieAlgebra.derivedSeriesOfIdeal_succ (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (k : ℕ) : LieAlgebra.derivedSeriesOfIdeal R L (k + 1) I = ⁅LieAlgebra.derivedSeriesOfIdeal R L k I, LieAlgebra.derivedSeriesOfIdeal R L k I⁆

@[reducible, inline]

abbrev LieAlgebra.derivedSeries (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (k : ℕ) : LieIdeal R L

The derived series of Lie ideals of a Lie algebra.

Equations

• LieAlgebra.derivedSeries R L k = LieAlgebra.derivedSeriesOfIdeal R L k ⊤

theorem LieAlgebra.derivedSeries_def (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (k : ℕ) : LieAlgebra.derivedSeries R L k = LieAlgebra.derivedSeriesOfIdeal R L k ⊤

theorem LieAlgebra.derivedSeriesOfIdeal_add {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (k l : ℕ) : LieAlgebra.derivedSeriesOfIdeal R L (k + l) I = LieAlgebra.derivedSeriesOfIdeal R L k (LieAlgebra.derivedSeriesOfIdeal R L l I)

theorem LieAlgebra.derivedSeriesOfIdeal_le {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {I J : LieIdeal R L} {k l : ℕ} (h₁ : I ≤ J) (h₂ : l ≤ k) : LieAlgebra.derivedSeriesOfIdeal R L k I ≤ LieAlgebra.derivedSeriesOfIdeal R L l J

theorem LieAlgebra.derivedSeriesOfIdeal_succ_le {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (k : ℕ) : LieAlgebra.derivedSeriesOfIdeal R L (k + 1) I ≤ LieAlgebra.derivedSeriesOfIdeal R L k I

theorem LieAlgebra.derivedSeriesOfIdeal_le_self {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (k : ℕ) : LieAlgebra.derivedSeriesOfIdeal R L k I ≤ I

theorem LieAlgebra.derivedSeriesOfIdeal_mono {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {I J : LieIdeal R L} (h : I ≤ J) (k : ℕ) : LieAlgebra.derivedSeriesOfIdeal R L k I ≤ LieAlgebra.derivedSeriesOfIdeal R L k J

theorem LieAlgebra.derivedSeriesOfIdeal_antitone {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) {k l : ℕ} (h : l ≤ k) : LieAlgebra.derivedSeriesOfIdeal R L k I ≤ LieAlgebra.derivedSeriesOfIdeal R L l I

theorem LieAlgebra.derivedSeriesOfIdeal_add_le_add {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I J : LieIdeal R L) (k l : ℕ) : LieAlgebra.derivedSeriesOfIdeal R L (k + l) (I + J) ≤ LieAlgebra.derivedSeriesOfIdeal R L k I + LieAlgebra.derivedSeriesOfIdeal R L l J

theorem LieAlgebra.derivedSeries_of_bot_eq_bot {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (k : ℕ) : LieAlgebra.derivedSeriesOfIdeal R L k ⊥ = ⊥

theorem LieAlgebra.abelian_iff_derived_one_eq_bot {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : IsLieAbelian ↥I ↔ LieAlgebra.derivedSeriesOfIdeal R L 1 I = ⊥

theorem LieAlgebra.abelian_iff_derived_succ_eq_bot {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (k : ℕ) : IsLieAbelian ↥(LieAlgebra.derivedSeriesOfIdeal R L k I) ↔ LieAlgebra.derivedSeriesOfIdeal R L (k + 1) I = ⊥

theorem LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_comap {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (k : ℕ) : LieAlgebra.derivedSeries R (↥I) k = LieIdeal.comap I.incl (LieAlgebra.derivedSeriesOfIdeal R L k I)

theorem LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_map {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (k : ℕ) : LieIdeal.map I.incl (LieAlgebra.derivedSeries R (↥I) k) = LieAlgebra.derivedSeriesOfIdeal R L k I

theorem LieIdeal.derivedSeries_eq_bot_iff {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (k : ℕ) : LieAlgebra.derivedSeries R (↥I) k = ⊥ ↔ LieAlgebra.derivedSeriesOfIdeal R L k I = ⊥

theorem LieIdeal.derivedSeries_add_eq_bot {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {k l : ℕ} {I 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₁} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L' →ₗ⁅R⁆ L} (k : ℕ) : LieIdeal.map f (LieAlgebra.derivedSeries R L' k) ≤ LieAlgebra.derivedSeries R L k

theorem LieIdeal.derivedSeries_map_eq {R : Type u} {L : Type v} {L' : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L' →ₗ⁅R⁆ L} (k : ℕ) (h : Function.Surjective ⇑f) : LieIdeal.map f (LieAlgebra.derivedSeries R L' k) = LieAlgebra.derivedSeries R L k

theorem LieIdeal.derivedSeries_succ_eq_top_iff {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) : LieAlgebra.derivedSeries R L (n + 1) = ⊤ ↔ LieAlgebra.derivedSeries R L 1 = ⊤

theorem LieIdeal.derivedSeries_eq_top {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) (h : LieAlgebra.derivedSeries R L 1 = ⊤) : LieAlgebra.derivedSeries R L n = ⊤

class LieAlgebra.IsSolvable (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : Prop

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

• solvable : ∃ (k : ℕ), LieAlgebra.derivedSeries R L k = ⊥

instance LieAlgebra.isSolvableBot (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : LieAlgebra.IsSolvable R ↥⊥

Equations

• ⋯ = ⋯

instance LieAlgebra.isSolvableAdd (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {I J : LieIdeal R L} [hI : LieAlgebra.IsSolvable R ↥I] [hJ : LieAlgebra.IsSolvable R ↥J] : LieAlgebra.IsSolvable R ↥(I + J)

Equations

• ⋯ = ⋯

theorem LieAlgebra.derivedSeries_lt_top_of_solvable (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsSolvable R L] [Nontrivial L] : LieAlgebra.derivedSeries R L 1 < ⊤

theorem Function.Injective.lieAlgebra_isSolvable {R : Type u} {L : Type v} {L' : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L' →ₗ⁅R⁆ L} [h₁ : LieAlgebra.IsSolvable R L] (h₂ : Function.Injective ⇑f) : LieAlgebra.IsSolvable R L'

theorem Function.Surjective.lieAlgebra_isSolvable {R : Type u} {L : Type v} {L' : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L' →ₗ⁅R⁆ L} [h₁ : LieAlgebra.IsSolvable R L'] (h₂ : Function.Surjective ⇑f) : LieAlgebra.IsSolvable R L

theorem LieHom.isSolvable_range {R : Type u} {L : Type v} {L' : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L' →ₗ⁅R⁆ L) [LieAlgebra.IsSolvable R L'] : LieAlgebra.IsSolvable R ↥f.range

theorem LieAlgebra.solvable_iff_equiv_solvable {R : Type u} {L : Type v} {L' : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (e : L' ≃ₗ⁅R⁆ L) : LieAlgebra.IsSolvable R L' ↔ LieAlgebra.IsSolvable R L

theorem LieAlgebra.le_solvable_ideal_solvable {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {I J : LieIdeal R L} (h₁ : I ≤ J) : LieAlgebra.IsSolvable R ↥J → LieAlgebra.IsSolvable R ↥I

@[instance 100]

instance LieAlgebra.ofAbelianIsSolvable (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsLieAbelian L] : LieAlgebra.IsSolvable R L

Equations

• ⋯ = ⋯

def LieAlgebra.radical (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : LieIdeal R L

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

Equations

• LieAlgebra.radical R L = sSup {I : LieIdeal R L | LieAlgebra.IsSolvable R ↥I}

instance LieAlgebra.radicalIsSolvable (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsNoetherian R L] : LieAlgebra.IsSolvable R ↥(LieAlgebra.radical R L)

The radical of a Noetherian Lie algebra is solvable.

Equations

• ⋯ = ⋯

theorem LieAlgebra.LieIdeal.solvable_iff_le_radical (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsNoetherian R L] (I : LieIdeal R L) : LieAlgebra.IsSolvable R ↥I ↔ I ≤ LieAlgebra.radical R L

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

theorem LieAlgebra.center_le_radical (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : LieAlgebra.center R L ≤ LieAlgebra.radical R L

instance LieAlgebra.instIsSolvableSubtypeMemLieSubalgebraTop (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsSolvable R L] : LieAlgebra.IsSolvable R ↥⊤

Equations

• ⋯ = ⋯

@[simp]

theorem LieAlgebra.radical_eq_top_of_isSolvable (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsSolvable R L] : LieAlgebra.radical R L = ⊤

noncomputable def LieAlgebra.derivedLengthOfIdeal (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (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

• LieAlgebra.derivedLengthOfIdeal R L I = sInf {k : ℕ | LieAlgebra.derivedSeriesOfIdeal R L k I = ⊥}

@[reducible, inline]

noncomputable abbrev LieAlgebra.derivedLength (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : ℕ

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

See also LieAlgebra.derivedLength_eq_derivedLengthOfIdeal.

Equations

• LieAlgebra.derivedLength R L = LieAlgebra.derivedLengthOfIdeal R L ⊤

theorem LieAlgebra.derivedSeries_of_derivedLength_succ (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (k : ℕ) : LieAlgebra.derivedLengthOfIdeal R L I = k + 1 ↔ IsLieAbelian ↥(LieAlgebra.derivedSeriesOfIdeal R L k I) ∧ LieAlgebra.derivedSeriesOfIdeal R L k I ≠ ⊥

theorem LieAlgebra.derivedLength_eq_derivedLengthOfIdeal (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : LieAlgebra.derivedLength R ↥I = LieAlgebra.derivedLengthOfIdeal R L I

noncomputable def LieAlgebra.derivedAbelianOfIdeal {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : 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

• LieAlgebra.derivedAbelianOfIdeal I = match LieAlgebra.derivedLengthOfIdeal R L I with | 0 => ⊥ | k.succ => LieAlgebra.derivedSeriesOfIdeal R L k I

instance LieAlgebra.instUniqueSubtypeMemLieIdealBot {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : Unique ↥⊥

Equations

• LieAlgebra.instUniqueSubtypeMemLieIdealBot = inferInstanceAs (Unique ↥⊥)

theorem LieAlgebra.abelian_derivedAbelianOfIdeal {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : IsLieAbelian ↥(LieAlgebra.derivedAbelianOfIdeal I)

theorem LieAlgebra.derivedLength_zero {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) [hI : LieAlgebra.IsSolvable R ↥I] : LieAlgebra.derivedLengthOfIdeal R L I = 0 ↔ I = ⊥

theorem LieAlgebra.abelian_of_solvable_ideal_eq_bot_iff {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) [h : LieAlgebra.IsSolvable R ↥I] : LieAlgebra.derivedAbelianOfIdeal I = ⊥ ↔ I = ⊥