mathlibdocumentation

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 #

• 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

def lie_algebra.derived_series_of_ideal (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] (k : ) :
L 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 lie_ideal.derived_series_eq_derived_series_of_ideal_comap and lie_ideal.derived_series_eq_derived_series_of_ideal_map below.

Equations
@[simp]
theorem lie_algebra.derived_series_of_ideal_zero (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] (I : L) :
= I
@[simp]
theorem lie_algebra.derived_series_of_ideal_succ (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] (I : L) (k : ) :
(k + 1) I =
def lie_algebra.derived_series (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] (k : ) :
L

The derived series of Lie ideals of a Lie algebra.

theorem lie_algebra.derived_series_def (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] (k : ) :
theorem lie_algebra.derived_series_of_ideal_add {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (I : L) (k l : ) :
(k + l) I =
theorem lie_algebra.derived_series_of_ideal_le {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] {I J : L} {k l : } (h₁ : I J) (h₂ : l k) :
theorem lie_algebra.derived_series_of_ideal_succ_le {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (I : L) (k : ) :
(k + 1) I
theorem lie_algebra.derived_series_of_ideal_le_self {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (I : L) (k : ) :
I
theorem lie_algebra.derived_series_of_ideal_mono {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] {I J : L} (h : I J) (k : ) :
theorem lie_algebra.derived_series_of_ideal_antitone {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (I : L) {k l : } (h : l k) :
theorem lie_algebra.derived_series_of_ideal_add_le_add {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (I J : L) (k l : ) :
(k + l) (I + J)
theorem lie_algebra.derived_series_of_bot_eq_bot {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (k : ) :
theorem lie_algebra.abelian_iff_derived_one_eq_bot {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (I : L) :
theorem lie_algebra.abelian_iff_derived_succ_eq_bot {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (I : L) (k : ) :
(k + 1) I =
theorem lie_ideal.derived_series_eq_derived_series_of_ideal_comap {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (I : L) (k : ) :
theorem lie_ideal.derived_series_eq_derived_series_of_ideal_map {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (I : L) (k : ) :
k) =
theorem lie_ideal.derived_series_eq_bot_iff {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (I : L) (k : ) :
theorem lie_ideal.derived_series_add_eq_bot {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] {k l : } {I J : L} (hI : = ) (hJ : = ) :
(I + J) (k + l) =
theorem lie_ideal.derived_series_map_le {R : Type u} {L : Type v} {L' : Type w₁} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] {f : L' →ₗ⁅R L} (k : ) :
k)
theorem lie_ideal.derived_series_map_eq {R : Type u} {L : Type v} {L' : Type w₁} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] {f : L' →ₗ⁅R L} (k : ) (h : function.surjective f) :
k) =
@[class]
structure lie_algebra.is_solvable (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] :
Prop
• solvable : ∃ (k : ),

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

Instances
@[protected, instance]
def lie_algebra.is_solvable_bot (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] :
@[protected, instance]
def lie_algebra.is_solvable_add (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] {I J : L} [hI : I] [hJ : J] :
(I + J)
theorem function.injective.lie_algebra_is_solvable {R : Type u} {L : Type v} {L' : Type w₁} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] {f : L' →ₗ⁅R L} [h₁ : L] (h₂ : function.injective f) :
theorem function.surjective.lie_algebra_is_solvable {R : Type u} {L : Type v} {L' : Type w₁} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] {f : L' →ₗ⁅R L} [h₁ : L'] (h₂ : function.surjective f) :
theorem lie_hom.is_solvable_range {R : Type u} {L : Type v} {L' : Type w₁} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] (f : L' →ₗ⁅R L) [h : L'] :
theorem lie_algebra.solvable_iff_equiv_solvable {R : Type u} {L : Type v} {L' : Type w₁} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] (e : L' ≃ₗ⁅R L) :
theorem lie_algebra.le_solvable_ideal_solvable {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] {I J : L} (h₁ : I J) (h₂ : J) :
@[protected, instance]
def lie_algebra.of_abelian_is_solvable (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L]  :
def lie_algebra.radical (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] :
L

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

Equations
@[protected, instance]
def lie_algebra.radical_is_solvable (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] [ L] :

The radical of a Noetherian Lie algebra is solvable.

theorem lie_algebra.lie_ideal.solvable_iff_le_radical (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] [ L] (I : L) :

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

theorem lie_algebra.center_le_radical (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] :
noncomputable def lie_algebra.derived_length_of_ideal (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] (I : 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
noncomputable def lie_algebra.derived_length (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] :

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.

theorem lie_algebra.derived_series_of_derived_length_succ (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] (I : L) (k : ) :
= k + 1
theorem lie_algebra.derived_length_eq_derived_length_of_ideal (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] (I : L) :
noncomputable def lie_algebra.derived_abelian_of_ideal {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (I : L) :
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
• = lie_algebra.derived_abelian_of_ideal._match_1 I
• lie_algebra.derived_abelian_of_ideal._match_1 I (k + 1) =
• lie_algebra.derived_abelian_of_ideal._match_1 I 0 =
theorem lie_algebra.abelian_derived_abelian_of_ideal {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (I : L) :
theorem lie_algebra.derived_length_zero {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (I : L) [hI : I] :
I =
theorem lie_algebra.abelian_of_solvable_ideal_eq_bot_iff {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (I : L) [h : I] :