mathlib3 documentation

algebra.lie.semisimple

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

source
@[class]
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] :
Prop

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

Instances of this typeclass
source
@[class]
structure lie_algebra.is_simple (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra 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.

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

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
source
theorem lie_algebra.is_semisimple_iff_no_solvable_ideals (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :
lie_algebra.is_semisimple R L ↔ ∀ (I : lie_ideal R L), lie_algebra.is_solvable R ↥I → I = ⊥
source
theorem lie_algebra.is_semisimple_iff_no_abelian_ideals (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :
lie_algebra.is_semisimple R L ↔ ∀ (I : lie_ideal R L), is_lie_abelian ↥I → I = ⊥
source
@[simp]
theorem lie_algebra.center_eq_bot_of_semisimple (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] [h : lie_algebra.is_semisimple R L] :
lie_algebra.center R L = ⊥
source
@[protected, instance]
def lie_algebra.is_semisimple_of_is_simple (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] [h : lie_algebra.is_simple R L] :
lie_algebra.is_semisimple R L

A simple Lie algebra is semisimple.

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

A semisimple Abelian Lie algebra is trivial.

source
theorem lie_algebra.abelian_radical_of_semisimple (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_algebra.is_semisimple R L] :
is_lie_abelian ↥(lie_algebra.radical R L)
source
theorem lie_algebra.abelian_radical_iff_solvable_is_abelian (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] [is_noetherian R L] :
is_lie_abelian ↥(lie_algebra.radical R L) ↔ ∀ (I : lie_ideal R L), lie_algebra.is_solvable R ↥I → is_lie_abelian ↥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.

source
theorem lie_algebra.ad_ker_eq_bot_of_semisimple (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_algebra.is_semisimple R L] :
(lie_algebra.ad R L).ker = ⊥