Semisimple Lie algebras

In this file we define simple and semisimple Lie algebras, together with related concepts.

Main declarations

• LieModule.IsIrreducible
• LieAlgebra.IsSimple
• LieAlgebra.HasTrivialRadical
• LieAlgebra.IsSemisimple

Tags

lie algebra, radical, simple, semisimple

@[reducible, inline]

abbrev LieModule.IsIrreducible (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : Prop

A nontrivial Lie module is irreducible if its only Lie submodules are ⊥ and ⊤.

Equations

• LieModule.IsIrreducible R L M = IsSimpleOrder (LieSubmodule R L M)

class LieAlgebra.HasTrivialRadical (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : Prop

A Lie algebra has trivial radical if its radical is trivial. This is equivalent to having no non-trivial solvable ideals, and further equivalent to having no non-trivial abelian ideals.

In characteristic zero, it is also equivalent to LieAlgebra.IsSemisimple.

Note that the label 'semisimple' is apparently not universally agreed upon for general coefficients.

For example Seligman, page 15 uses the label for LieAlgebra.HasTrivialRadical, whereas we reserve it for Lie algebras that are a direct sum of simple Lie algebras.

• radical_eq_bot : LieAlgebra.radical R L = ⊥

@[simp]

theorem LieAlgebra.HasTrivialRadical.radical_eq_bot {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] [self : LieAlgebra.HasTrivialRadical R L] : LieAlgebra.radical R L = ⊥

class LieAlgebra.IsSimple (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : 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.

• eq_bot_or_eq_top : ∀ (I : LieIdeal R L), I = ⊥ ∨ I = ⊤
• non_abelian : ¬IsLieAbelian L

theorem LieAlgebra.IsSimple.eq_bot_or_eq_top {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] [self : LieAlgebra.IsSimple R L] (I : LieIdeal R L) : I = ⊥ ∨ I = ⊤

theorem LieAlgebra.IsSimple.non_abelian (R : Type u_1) {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] [self : LieAlgebra.IsSimple R L] : ¬IsLieAbelian L

class LieAlgebra.IsSemisimple (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : Prop

A semisimple Lie algebra is one that is a direct sum of non-abelian atomic ideals. These ideals are simple Lie algebras, by LieAlgebra.IsSemisimple.isSimple_of_isAtom.

Note that the label 'semisimple' is apparently not universally agreed upon for general coefficients.

For example Seligman, page 15 uses the label for LieAlgebra.HasTrivialRadical, the weakest of the various properties which are all equivalent over a field of characteristic zero.

• sSup_atoms_eq_top : sSup {I : LieIdeal R L | IsAtom I} = ⊤

  In a semisimple Lie algebra, the supremum of the atoms is the whole Lie algebra.

• setIndependent_isAtom : CompleteLattice.SetIndependent {I : LieIdeal R L | IsAtom I}

  In a semisimple Lie algebra, the atoms are independent.

• non_abelian_of_isAtom : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian ↥↑I

  In a semisimple Lie algebra, the atoms are non-abelian.

theorem LieAlgebra.IsSemisimple.sSup_atoms_eq_top {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] [self : LieAlgebra.IsSemisimple R L] : sSup {I : LieIdeal R L | IsAtom I} = ⊤

In a semisimple Lie algebra, the supremum of the atoms is the whole Lie algebra.

theorem LieAlgebra.IsSemisimple.setIndependent_isAtom {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] [self : LieAlgebra.IsSemisimple R L] : CompleteLattice.SetIndependent {I : LieIdeal R L | IsAtom I}

In a semisimple Lie algebra, the atoms are independent.

theorem LieAlgebra.IsSemisimple.non_abelian_of_isAtom {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] [self : LieAlgebra.IsSemisimple R L] (I : LieIdeal R L) : IsAtom I → ¬IsLieAbelian ↥↑I

In a semisimple Lie algebra, the atoms are non-abelian.