mathlib documentation

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 #

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] [lie_algebra R L] (k : ) :
lie_ideal R Llie_ideal 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 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] [lie_algebra R L] (I : lie_ideal R L) :
@[reducible]
def lie_algebra.derived_series (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (k : ) :

The derived series of Lie ideals of a Lie algebra.

theorem lie_algebra.derived_series_of_ideal_le {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {I J : lie_ideal R L} {k l : } (h₁ : I J) (h₂ : l k) :
theorem lie_algebra.derived_series_of_ideal_le_self {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (I : lie_ideal R L) (k : ) :
theorem lie_ideal.derived_series_add_eq_bot {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {k l : } {I J : lie_ideal R L} (hI : lie_algebra.derived_series R I k = ) (hJ : lie_algebra.derived_series R J l = ) :
theorem lie_ideal.derived_series_map_le {R : Type u} {L : Type v} {L' : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] {f : L' →ₗ⁅R L} (k : ) :
theorem lie_ideal.derived_series_map_eq {R : Type u} {L : Type v} {L' : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] {f : L' →ₗ⁅R L} (k : ) (h : function.surjective f) :
@[class]
structure lie_algebra.is_solvable (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :
Prop

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

Instances of this typeclass
@[protected, instance]
def lie_algebra.is_solvable_bot (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :
@[protected, instance]
def lie_algebra.is_solvable_add (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] {I J : lie_ideal R L} [hI : lie_algebra.is_solvable R I] [hJ : lie_algebra.is_solvable R J] :
theorem function.injective.lie_algebra_is_solvable {R : Type u} {L : Type v} {L' : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] {f : L' →ₗ⁅R L} [h₁ : lie_algebra.is_solvable R 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] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] {f : L' →ₗ⁅R L} [h₁ : lie_algebra.is_solvable R 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] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (f : L' →ₗ⁅R L) [h : lie_algebra.is_solvable R L'] :
theorem lie_algebra.solvable_iff_equiv_solvable {R : Type u} {L : Type v} {L' : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (e : L' ≃ₗ⁅R L) :
theorem lie_algebra.le_solvable_ideal_solvable {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {I J : lie_ideal R L} (h₁ : I J) (h₂ : lie_algebra.is_solvable R J) :
@[protected, instance]
def lie_algebra.radical (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :

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

Equations
Instances for lie_algebra.radical
@[protected, instance]

The radical of a Noetherian Lie algebra is solvable.

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

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

noncomputable def lie_algebra.derived_abelian_of_ideal {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (I : lie_ideal 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