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)

theorem LieModule.IsIrreducible.mk {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [Nontrivial M] (h : ∀ (N : LieSubmodule R L M), N ≠ ⊥ → N = ⊤) : IsIrreducible R L M

theorem LieSubmodule.eq_top_of_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] [LieModule.IsIrreducible R L M] (N : LieSubmodule R L M) [Nontrivial ↥N] : N = ⊤

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][seligman1967] 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 : radical R L = ⊥

theorem LieAlgebra.hasTrivialRadical_iff (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : HasTrivialRadical R L ↔ radical R L = ⊥

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

A Lie algebra has central radical if its radical coincides with its center. Such Lie algebras are called reductive, if the coefficients are a field of characteristic zero.

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

• radical_eq_center : radical R L = center R L

theorem LieAlgebra.hasCentralRadical_iff (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : HasCentralRadical R L ↔ radical R L = center R L

theorem LieAlgebra.hasCentralRadical_of_radical_le (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (h : radical R L ≤ center R L) : HasCentralRadical R L

instance LieAlgebra.instHasTrivialRadicalOfSubsingleton (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] [Subsingleton L] : HasTrivialRadical 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

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][seligman1967] 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.

• sSupIndep_isAtom : sSupIndep {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.