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 prove basic results abot simple and semisimple Lie algebras.

Main declarations

• LieAlgebra.IsSemisimple.instHasTrivialRadical: A semisimple Lie algebra has trivial radical.
• LieAlgebra.IsSemisimple.instBooleanAlgebra: The lattice of ideals in a semisimple Lie algebra is a boolean algebra. In particular, this implies that the lattice of ideals is atomistic: every ideal is a direct sum of atoms (simple ideals) in a unique way.
• LieAlgebra.hasTrivialRadical_iff_no_solvable_ideals
• LieAlgebra.hasTrivialRadical_iff_no_abelian_ideals
• LieAlgebra.abelian_radical_iff_solvable_is_abelian

Tags

lie algebra, radical, simple, semisimple

theorem LieModule.nontrivial_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] : Nontrivial M

theorem LieAlgebra.HasTrivialRadical.eq_bot_of_isSolvable {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.HasTrivialRadical R L] (I : LieIdeal R L) [hI : LieAlgebra.IsSolvable R ↥↑I] : I = ⊥

@[simp]

theorem LieAlgebra.HasTrivialRadical.center_eq_bot (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.HasTrivialRadical R L] : LieAlgebra.center R L = ⊥

theorem LieAlgebra.hasTrivialRadical_of_no_solvable_ideals {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (h : ∀ (I : LieIdeal R L), LieAlgebra.IsSolvable R ↥↑I → I = ⊥) : LieAlgebra.HasTrivialRadical R L

theorem LieAlgebra.hasTrivialRadical_iff_no_solvable_ideals (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : LieAlgebra.HasTrivialRadical R L ↔ ∀ (I : LieIdeal R L), LieAlgebra.IsSolvable R ↥↑I → I = ⊥

theorem LieAlgebra.hasTrivialRadical_iff_no_abelian_ideals (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : LieAlgebra.HasTrivialRadical R L ↔ ∀ (I : LieIdeal R L), IsLieAbelian ↥↑I → I = ⊥

instance LieAlgebra.IsSimple.instIsIrreducible (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsSimple R L] : LieModule.IsIrreducible R L L

Equations

• ⋯ = ⋯

theorem LieAlgebra.IsSimple.eq_top_of_isAtom {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsSimple R L] (I : LieIdeal R L) (hI : IsAtom I) : I = ⊤

theorem LieAlgebra.IsSimple.isAtom_top (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsSimple R L] : IsAtom ⊤

@[simp]

theorem LieAlgebra.IsSimple.isAtom_iff_eq_top {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsSimple R L] (I : LieIdeal R L) : IsAtom I ↔ I = ⊤

instance LieAlgebra.IsSimple.instHasTrivialRadical (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsSimple R L] : LieAlgebra.HasTrivialRadical R L

Equations

• ⋯ = ⋯

theorem LieAlgebra.IsSemisimple.isSimple_of_isAtom {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsSemisimple R L] (I : LieIdeal R L) (hI : IsAtom I) : LieAlgebra.IsSimple R ↥↑I

theorem LieAlgebra.IsSemisimple.booleanGenerators (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsSemisimple R L] : IsCompactlyGenerated.BooleanGenerators {I : LieIdeal R L | IsAtom I}

@[instance 100]

instance LieAlgebra.IsSemisimple.instDistribLattice {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsSemisimple R L] : DistribLattice (LieIdeal R L)

Equations

• LieAlgebra.IsSemisimple.instDistribLattice = ⋯.distribLattice_of_sSup_eq_top ⋯

@[instance 100]

noncomputable instance LieAlgebra.IsSemisimple.instBooleanAlgebra {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsSemisimple R L] : BooleanAlgebra (LieIdeal R L)

Equations

• LieAlgebra.IsSemisimple.instBooleanAlgebra = ⋯.booleanAlgebra_of_sSup_eq_top ⋯

@[instance 100]

instance LieAlgebra.IsSemisimple.instHasTrivialRadical {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsSemisimple R L] : LieAlgebra.HasTrivialRadical R L

A semisimple Lie algebra has trivial radical.

Equations

• ⋯ = ⋯

@[instance 100]

instance LieAlgebra.IsSimple.instIsSemisimple (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsSimple R L] : LieAlgebra.IsSemisimple R L

A simple Lie algebra is semisimple.

Equations

• ⋯ = ⋯

theorem LieAlgebra.subsingleton_of_hasTrivialRadical_lie_abelian (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.HasTrivialRadical R L] [h : IsLieAbelian L] : Subsingleton L

An abelian Lie algebra with trivial radical is trivial.

theorem LieAlgebra.abelian_radical_of_hasTrivialRadical (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.HasTrivialRadical R L] : IsLieAbelian ↥↑(LieAlgebra.radical R L)

theorem LieAlgebra.abelian_radical_iff_solvable_is_abelian (R : Type u_1) (L : Type u_2) [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.

theorem LieAlgebra.ad_ker_eq_bot_of_hasTrivialRadical (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.HasTrivialRadical R L] : (LieAlgebra.ad R L).ker = ⊥