mathlib documentation


Cartan subalgebras #

Cartan subalgebras are one of the most important concepts in Lie theory. We define them here. The standard example is the set of diagonal matrices in the Lie algebra of matrices.

Main definitions #

Tags #

lie subalgebra, normalizer, idealizer, cartan subalgebra

structure lie_subalgebra.is_cartan_subalgebra {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (H : lie_subalgebra R L) :

A Cartan subalgebra is a nilpotent, self-normalizing subalgebra.

Instances of this typeclass
@[protected, instance]
theorem lie_ideal.normalizer_eq_top {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (I : lie_ideal R L) :
@[protected, instance]

A nilpotent Lie algebra is its own Cartan subalgebra.