Documentation

Mathlib.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 LieAlgebra.derivedSeriesOfIdeal (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (k : ) :
LieIdeal R LLieIdeal 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.

Equations
Instances For
    @[reducible, inline]
    abbrev LieAlgebra.derivedSeries (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (k : ) :

    The derived series of Lie ideals of a Lie algebra.

    Equations
    Instances For
      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) :
      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 : ) :
      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) :
      class LieAlgebra.IsSolvable (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :

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

      Instances
        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] :
        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.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) :
        @[instance 100]
        Equations
        • =
        def LieAlgebra.radical (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :

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

        Equations
        Instances For

          The radical of a Noetherian Lie algebra is solvable.

          Equations
          • =

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

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

            Equations
            Instances For
              noncomputable def LieAlgebra.derivedAbelianOfIdeal {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 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
              Instances For