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.

@[simp]

theorem LieAlgebra.derivedSeriesOfIdeal_zero (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : 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 : ℕ) : derivedSeriesOfIdeal R L (k + 1) I = ⁅derivedSeriesOfIdeal R L k I, 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.

theorem LieAlgebra.derivedSeries_def (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (k : ℕ) : derivedSeries R L k = 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 : ℕ) : derivedSeriesOfIdeal R L (k + l) I = derivedSeriesOfIdeal R L k (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) : derivedSeriesOfIdeal R L k I ≤ 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 : ℕ) : derivedSeriesOfIdeal R L (k + 1) I ≤ 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 : ℕ) : 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 : ℕ) : derivedSeriesOfIdeal R L k I ≤ 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) : derivedSeriesOfIdeal R L k I ≤ 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 : ℕ) : derivedSeriesOfIdeal R L (k + l) (I + J) ≤ derivedSeriesOfIdeal R L k I + 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 : ℕ) : 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 ↔ 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 ↥(derivedSeriesOfIdeal R L k I) ↔ derivedSeriesOfIdeal R L (k + 1) I = ⊥

@[simp]

theorem LieAlgebra.derivedSeriesOfIdeal_baseChange {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) {A : Type u_1} [CommRing A] [Algebra R A] (k : ℕ) : derivedSeriesOfIdeal A (TensorProduct R A L) k (LieSubmodule.baseChange A I) = LieSubmodule.baseChange A (derivedSeriesOfIdeal R L k I)

@[simp]

theorem LieAlgebra.derivedSeries_baseChange {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {A : Type u_1} [CommRing A] [Algebra R A] (k : ℕ) : derivedSeries A (TensorProduct R A L) k = LieSubmodule.baseChange A (derivedSeries R L k)

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 = 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 : ℕ) : 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 : ℕ) : 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) : 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 = ⊤

theorem LieIdeal.coe_derivedSeries_eq_int {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (k : ℕ) : ↑(LieAlgebra.derivedSeries R L k) = ↑(LieAlgebra.derivedSeries ℤ L k)

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

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

• mk_int :: (
• solvable_int : ∃ (k : ℕ), derivedSeries ℤ L k = ⊥
• )

theorem LieAlgebra.isSolvable_iff_int (L : Type v) [LieRing L] : IsSolvable L ↔ ∃ (k : ℕ), derivedSeries ℤ L k = ⊥

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

theorem LieAlgebra.isSolvable_iff (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : IsSolvable L ↔ ∃ (k : ℕ), derivedSeries R L k = ⊥

theorem LieAlgebra.IsSolvable.solvable (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsSolvable L] : ∃ (k : ℕ), derivedSeries R L k = ⊥

theorem LieAlgebra.IsSolvable.mk {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {k : ℕ} (h : derivedSeries R L k = ⊥) : IsSolvable L

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

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

instance LieAlgebra.instIsSolvableTensorProduct (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {A : Type u_1} [CommRing A] [Algebra R A] [IsSolvable L] : IsSolvable (TensorProduct R A L)

theorem LieAlgebra.isSolvable_tensorProduct_iff (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {A : Type u_1} [CommRing A] [Algebra R A] [Module.FaithfullyFlat R A] : IsSolvable (TensorProduct R A L) ↔ IsSolvable L

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} [hL : LieAlgebra.IsSolvable L] (h : Injective ⇑f) : LieAlgebra.IsSolvable L'

instance Function.instIsSolvableSubtypeMemLieSubmodule {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (A : LieIdeal R L) [LieAlgebra.IsSolvable L] : LieAlgebra.IsSolvable ↥A

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} [hL' : LieAlgebra.IsSolvable L'] (h : Surjective ⇑f) : LieAlgebra.IsSolvable L

instance 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 L'] : LieAlgebra.IsSolvable ↥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) : IsSolvable L' ↔ IsSolvable 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) : IsSolvable ↥J → IsSolvable ↥I

@[instance 100]

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

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.

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

The radical of a Noetherian Lie algebra is solvable.

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) : IsSolvable ↥I ↔ I ≤ 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] : center R L ≤ radical R L

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

@[simp]

theorem LieAlgebra.radical_eq_top_of_isSolvable (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsSolvable L] : 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.

@[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.

theorem LieAlgebra.derivedSeries_of_derivedLength_succ (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (k : ℕ) : derivedLengthOfIdeal R L I = k + 1 ↔ IsLieAbelian ↥(derivedSeriesOfIdeal R L k I) ∧ 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) : derivedLength R ↥I = 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, ⊥.

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

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

theorem LieAlgebra.derivedLength_zero {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) [IsSolvable ↥I] : 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 : IsSolvable ↥I] : derivedAbelianOfIdeal I = ⊥ ↔ I = ⊥