Solvable Lie algebras #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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_ideallie_algebra.derived_serieslie_algebra.is_solvablelie_algebra.is_solvable_addlie_algebra.radicallie_algebra.radical_is_solvablelie_algebra.derived_length_of_ideallie_algebra.derived_lengthlie_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]
[lie_algebra R L]
(k : ℕ) :
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.
@[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) :
lie_algebra.derived_series_of_ideal R L 0 I = I
@[simp]
theorem
lie_algebra.derived_series_of_ideal_succ
(R : Type u)
(L : Type v)
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
(I : lie_ideal R L)
(k : ℕ) :
lie_algebra.derived_series_of_ideal R L (k + 1) I = ⁅lie_algebra.derived_series_of_ideal R L k I, lie_algebra.derived_series_of_ideal R L k I⁆
@[reducible]
def
lie_algebra.derived_series
(R : Type u)
(L : Type v)
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
(k : ℕ) :
lie_ideal R 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]
[lie_algebra R L]
(k : ℕ) :
theorem
lie_algebra.derived_series_of_ideal_add
{R : Type u}
{L : Type v}
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
(I : lie_ideal R L)
(k l : ℕ) :
lie_algebra.derived_series_of_ideal R L (k + l) I = lie_algebra.derived_series_of_ideal R L k (lie_algebra.derived_series_of_ideal R L l I)
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) :
lie_algebra.derived_series_of_ideal R L k I ≤ lie_algebra.derived_series_of_ideal R L l J
theorem
lie_algebra.derived_series_of_ideal_succ_le
{R : Type u}
{L : Type v}
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
(I : lie_ideal R L)
(k : ℕ) :
lie_algebra.derived_series_of_ideal R L (k + 1) I ≤ lie_algebra.derived_series_of_ideal R L k I
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 : ℕ) :
lie_algebra.derived_series_of_ideal R L k I ≤ I
theorem
lie_algebra.derived_series_of_ideal_mono
{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)
(k : ℕ) :
lie_algebra.derived_series_of_ideal R L k I ≤ lie_algebra.derived_series_of_ideal R L k J
theorem
lie_algebra.derived_series_of_ideal_antitone
{R : Type u}
{L : Type v}
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
(I : lie_ideal R L)
{k l : ℕ}
(h : l ≤ k) :
lie_algebra.derived_series_of_ideal R L k I ≤ lie_algebra.derived_series_of_ideal R L l I
theorem
lie_algebra.derived_series_of_ideal_add_le_add
{R : Type u}
{L : Type v}
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
(I J : lie_ideal R L)
(k l : ℕ) :
lie_algebra.derived_series_of_ideal R L (k + l) (I + J) ≤ lie_algebra.derived_series_of_ideal R L k I + lie_algebra.derived_series_of_ideal R L l J
theorem
lie_algebra.derived_series_of_bot_eq_bot
{R : Type u}
{L : Type v}
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
(k : ℕ) :
theorem
lie_algebra.abelian_iff_derived_one_eq_bot
{R : Type u}
{L : Type v}
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
(I : lie_ideal R L) :
is_lie_abelian ↥I ↔ lie_algebra.derived_series_of_ideal R L 1 I = ⊥
theorem
lie_algebra.abelian_iff_derived_succ_eq_bot
{R : Type u}
{L : Type v}
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
(I : lie_ideal R L)
(k : ℕ) :
is_lie_abelian ↥(lie_algebra.derived_series_of_ideal R L k I) ↔ lie_algebra.derived_series_of_ideal R L (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]
[lie_algebra R L]
(I : lie_ideal R L)
(k : ℕ) :
lie_algebra.derived_series R ↥I k = lie_ideal.comap I.incl (lie_algebra.derived_series_of_ideal R L k I)
theorem
lie_ideal.derived_series_eq_derived_series_of_ideal_map
{R : Type u}
{L : Type v}
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
(I : lie_ideal R L)
(k : ℕ) :
lie_ideal.map I.incl (lie_algebra.derived_series R ↥I k) = lie_algebra.derived_series_of_ideal R L k I
theorem
lie_ideal.derived_series_eq_bot_iff
{R : Type u}
{L : Type v}
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
(I : lie_ideal R L)
(k : ℕ) :
lie_algebra.derived_series R ↥I k = ⊥ ↔ lie_algebra.derived_series_of_ideal R L k I = ⊥
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 : ℕ) :
lie_ideal.map f (lie_algebra.derived_series R L' k) ≤ lie_algebra.derived_series 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) :
lie_ideal.map f (lie_algebra.derived_series R L' k) = lie_algebra.derived_series R L k
@[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).
@[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] :
lie_algebra.is_solvable R ↥(I + 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.of_abelian_is_solvable
(R : Type u)
(L : Type v)
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
[is_lie_abelian L] :
def
lie_algebra.radical
(R : Type u)
(L : Type v)
[comm_ring R]
[lie_ring L]
[lie_algebra R L] :
lie_ideal R L
The (solvable) radical of Lie algebra is the Sup of all solvable ideals.
Equations
- lie_algebra.radical R L = has_Sup.Sup {I : lie_ideal R L | lie_algebra.is_solvable R ↥I}
Instances for ↥lie_algebra.radical
@[protected, instance]
def
lie_algebra.radical_is_solvable
(R : Type u)
(L : Type v)
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
[is_noetherian R 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]
[lie_algebra R L]
[is_noetherian R L]
(I : lie_ideal R L) :
lie_algebra.is_solvable R ↥I ↔ I ≤ lie_algebra.radical R 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]
[lie_algebra R L] :
lie_algebra.center R L ≤ lie_algebra.radical R L
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
- lie_algebra.derived_length_of_ideal R L I = has_Inf.Inf {k : ℕ | lie_algebra.derived_series_of_ideal R L k I = ⊥}
@[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.
theorem
lie_algebra.derived_series_of_derived_length_succ
(R : Type u)
(L : Type v)
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
(I : lie_ideal R L)
(k : ℕ) :
lie_algebra.derived_length_of_ideal R L I = k + 1 ↔ is_lie_abelian ↥(lie_algebra.derived_series_of_ideal R L k I) ∧ lie_algebra.derived_series_of_ideal R L k I ≠ ⊥
theorem
lie_algebra.derived_length_eq_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) :
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) :
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
- lie_algebra.derived_abelian_of_ideal I = lie_algebra.derived_abelian_of_ideal._match_1 I (lie_algebra.derived_length_of_ideal R L I)
- lie_algebra.derived_abelian_of_ideal._match_1 I (k + 1) = lie_algebra.derived_series_of_ideal R L k I
- 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]
[lie_algebra R L]
(I : lie_ideal R L) :
theorem
lie_algebra.derived_length_zero
{R : Type u}
{L : Type v}
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
(I : lie_ideal R L)
[hI : lie_algebra.is_solvable R ↥I] :
lie_algebra.derived_length_of_ideal R L I = 0 ↔ I = ⊥
theorem
lie_algebra.abelian_of_solvable_ideal_eq_bot_iff
{R : Type u}
{L : Type v}
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
(I : lie_ideal R L)
[h : lie_algebra.is_solvable R ↥I] :