# 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 #

• LieModule.IsIrreducible
• LieAlgebra.IsSimple
• LieAlgebra.IsSemisimple
• LieAlgebra.isSemisimple_iff_no_solvable_ideals
• LieAlgebra.isSemisimple_iff_no_abelian_ideals
• LieAlgebra.abelian_radical_iff_solvable_is_abelian

## Tags #

class LieModule.IsIrreducible (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] :

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

Instances
class LieAlgebra.IsSimple (R : Type u) (L : Type v) [] [] [] extends :

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
class LieAlgebra.IsSemisimple (R : Type u) (L : Type v) [] [] [] :
• semisimple :

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
theorem LieAlgebra.isSemisimple_iff_no_solvable_ideals (R : Type u) (L : Type v) [] [] [] :
∀ (I : LieIdeal R L), LieAlgebra.IsSolvable R { x // x I }I =
theorem LieAlgebra.isSemisimple_iff_no_abelian_ideals (R : Type u) (L : Type v) [] [] [] :
∀ (I : LieIdeal R L), IsLieAbelian { x // x I }I =
@[simp]
theorem LieAlgebra.center_eq_bot_of_semisimple (R : Type u) (L : Type v) [] [] [] [h : ] :
instance LieAlgebra.isSemisimpleOfIsSimple (R : Type u) (L : Type v) [] [] [] [h : ] :

A simple Lie algebra is semisimple.

theorem LieAlgebra.subsingleton_of_semisimple_lie_abelian (R : Type u) (L : Type v) [] [] [] [] [h : ] :

A semisimple Abelian Lie algebra is trivial.

theorem LieAlgebra.abelian_radical_of_semisimple (R : Type u) (L : Type v) [] [] [] [] :
IsLieAbelian { x // x ↑() }
theorem LieAlgebra.abelian_radical_iff_solvable_is_abelian (R : Type u) (L : Type v) [] [] [] [] :
IsLieAbelian { x // x ↑() } ∀ (I : LieIdeal R L), LieAlgebra.IsSolvable R { x // x I }IsLieAbelian { x // x 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_semisimple (R : Type u) (L : Type v) [] [] [] [] :