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

def LieSubmodule.IsUcsLimit {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type u_1} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) :

Given a Lie module M of a Lie algebra L, LieSubmodule.IsUcsLimit is the proposition that a Lie submodule N ⊆ M is the limiting value for the upper central series.

This is a characteristic property of Cartan subalgebras with the roles of L, M, N played by H, L, H, respectively. See LieSubalgebra.isCartanSubalgebra_iff_isUcsLimit.

Instances For

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

      theorem LieIdeal.normalizer_eq_top {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) :

      A nilpotent Lie algebra is its own Cartan subalgebra.