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.derivedSeriesOfIdealLieAlgebra.derivedSeriesLieAlgebra.IsSolvableLieAlgebra.isSolvableAddLieAlgebra.radicalLieAlgebra.radicalIsSolvableLieAlgebra.derivedLengthOfIdealLieAlgebra.derivedLengthLieAlgebra.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 : ℕ)
:
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.
Instances For
@[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⁆
@[inline, reducible]
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 ⊤
Instances For
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 : LieIdeal R L}
{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 : LieIdeal R L}
{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 : LieIdeal R L)
(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 (LieIdeal.incl I) (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 (LieIdeal.incl I) (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 : LieIdeal R L}
{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
A Lie algebra is solvable if its derived series reaches 0 (in a finite number of steps).
- solvable : ∃ (k : ℕ), LieAlgebra.derivedSeries R L k = ⊥
Instances
instance
LieAlgebra.isSolvableBot
(R : Type u)
(L : Type v)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
:
Equations
- ⋯ = ⋯
instance
LieAlgebra.isSolvableAdd
(R : Type u)
(L : Type v)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{I : LieIdeal R L}
{J : LieIdeal R L}
[hI : LieAlgebra.IsSolvable R ↥↑I]
[hJ : LieAlgebra.IsSolvable R ↥↑J]
:
LieAlgebra.IsSolvable R ↥(I + J)
Equations
- ⋯ = ⋯
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)
:
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)
:
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']
:
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 : LieIdeal R L}
{J : LieIdeal R L}
(h₁ : I ≤ J)
:
LieAlgebra.IsSolvable R ↥↑J → LieAlgebra.IsSolvable R ↥↑I
instance
LieAlgebra.ofAbelianIsSolvable
(R : Type u)
(L : Type v)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[IsLieAbelian 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}
Instances For
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.instIsSolvableSubtypeMemLieSubalgebraInstMembershipInstSetLikeLieSubalgebraTopInstTopLieSubalgebraLieRingLieAlgebra
(R : Type u)
(L : Type v)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsSolvable R L]
:
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 = ⊥}
Instances For
@[inline, reducible]
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
Instances For
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 => ⊥ | Nat.succ k => LieAlgebra.derivedSeriesOfIdeal R L k I
Instances For
theorem
LieAlgebra.abelian_derivedAbelianOfIdeal
{R : Type u}
{L : Type v}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(I : LieIdeal R L)
:
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]
: