# mathlibdocumentation

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 #

• lie_module.is_irreducible
• lie_algebra.is_simple
• lie_algebra.is_semisimple
• lie_algebra.is_semisimple_iff_no_solvable_ideals
• lie_algebra.is_semisimple_iff_no_abelian_ideals
• lie_algebra.abelian_radical_iff_solvable_is_abelian

## Tags #

@[class]
structure lie_module.is_irreducible (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
Prop
• irreducible : ∀ (N : M), N N =

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

Instances of this typeclass
@[class]
structure lie_algebra.is_simple (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] :
Prop
• to_is_irreducible :
• non_abelian :

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

@[class]
structure lie_algebra.is_semisimple (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] :
Prop
• 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 of this typeclass
theorem lie_algebra.is_semisimple_iff_no_solvable_ideals (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] :
∀ (I : L), I =
theorem lie_algebra.is_semisimple_iff_no_abelian_ideals (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] :
∀ (I : L), I =
@[simp]
theorem lie_algebra.center_eq_bot_of_semisimple (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] [h : L] :
@[protected, instance]
def lie_algebra.is_semisimple_of_is_simple (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] [h : L] :

A simple Lie algebra is semisimple.

theorem lie_algebra.subsingleton_of_semisimple_lie_abelian (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] [h : is_lie_abelian L] :

A semisimple Abelian Lie algebra is trivial.

theorem lie_algebra.abelian_radical_of_semisimple (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L]  :
theorem lie_algebra.abelian_radical_iff_solvable_is_abelian (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] [ L] :
∀ (I : L),

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 lie_algebra.ad_ker_eq_bot_of_semisimple (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L]  :
L).ker =