mathlib3 documentation


Semisimple Lie algebras #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

Tags #

lie algebra, radical, simple, semisimple

structure lie_module.is_irreducible (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] :

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

Instances of this typeclass
structure lie_algebra.is_simple (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :

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

structure lie_algebra.is_semisimple (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :

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
@[protected, instance]

A simple Lie algebra is semisimple.

A semisimple Abelian Lie algebra is trivial.

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.