Documentation

Mathlib.Algebra.Lie.Semisimple

Semisimple Lie algebras #

The famous Cartan-Dynkin-Killing classification of semisimple Lie algebras renders them one of the most important classes of Lie algebras. In this file we define simple and semisimple Lie algebras and prove some basic related results.

Main definitions #

Tags #

lie algebra, radical, simple, semisimple

source
class LieModule.IsIrreducible (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :
Prop

A Lie module is irreducible if it is zero or its only non-trivial Lie submodule is itself.

Instances
    source
    class LieAlgebra.IsSimple (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] extends LieModule.IsIrreducible :
    Prop

    A Lie algebra is simple if it is irreducible as a Lie module over itself via the adjoint action, and it is non-Abelian.

    Instances
      source
      class LieAlgebra.IsSemisimple (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :
      Prop

      A semisimple Lie algebra is one with trivial radical.

      Note that the label 'semisimple' is apparently not universally agreed upon for general coefficients. We are following Seligman, page 15 and using the label for the weakest of the various properties which are all equivalent over a field of characteristic zero.

      Instances
        source
        theorem LieAlgebra.isSemisimple_iff_no_solvable_ideals (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :
        LieAlgebra.IsSemisimple R L ↔ ∀ (I : LieIdeal R L), LieAlgebra.IsSolvable R ↥↑I → I = ⊥
        source
        theorem LieAlgebra.isSemisimple_iff_no_abelian_ideals (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :
        LieAlgebra.IsSemisimple R L ↔ ∀ (I : LieIdeal R L), IsLieAbelian ↥↑I → I = ⊥
        source
        @[simp]
        theorem LieAlgebra.center_eq_bot_of_semisimple (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [h : LieAlgebra.IsSemisimple R L] :
        LieAlgebra.center R L = ⊥
        source
        instance LieAlgebra.isSemisimpleOfIsSimple (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [h : LieAlgebra.IsSimple R L] :
        LieAlgebra.IsSemisimple R L

        A simple Lie algebra is semisimple.

        Equations
        source
        theorem LieAlgebra.subsingleton_of_semisimple_lie_abelian (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsSemisimple R L] [h : IsLieAbelian L] :
        Subsingleton L

        A semisimple Abelian Lie algebra is trivial.

        source
        theorem LieAlgebra.abelian_radical_of_semisimple (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsSemisimple R L] :
        IsLieAbelian ↥↑(LieAlgebra.radical R L)
        source
        theorem LieAlgebra.abelian_radical_iff_solvable_is_abelian (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsNoetherian R L] :
        IsLieAbelian ↥↑(LieAlgebra.radical R L) ↔ ∀ (I : LieIdeal R L), LieAlgebra.IsSolvable R ↥↑I → IsLieAbelian ↥↑I

        The two properties shown to be equivalent here are possible definitions for a Lie algebra to be reductive.

        Note that there is absolutely no agreement on what the label 'reductive' should mean when the coefficients are not a field of characteristic zero.

        source
        theorem LieAlgebra.ad_ker_eq_bot_of_semisimple (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsSemisimple R L] :
        LieHom.ker (LieAlgebra.ad R L) = ⊥