mathlibdocumentation

algebra.lie.cartan_subalgebra

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.

Tags #

lie subalgebra, normalizer, idealizer, cartan subalgebra

def lie_subalgebra.normalizer {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (H : L) :

The normalizer of a Lie subalgebra H is the set of elements of the Lie algebra whose bracket with any element of H lies in H. It is the Lie algebra equivalent of the group-theoretic normalizer (see subgroup.normalizer) and is an idealizer in the sense of abstract algebra.

Equations
theorem lie_subalgebra.mem_normalizer_iff {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (H : L) (x : L) :
x H.normalizer ∀ (y : L), y Hx,y H
theorem lie_subalgebra.mem_normalizer_iff' {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (H : L) (x : L) :
x H.normalizer ∀ (y : L), y Hy,x H
theorem lie_subalgebra.le_normalizer {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (H : L) :
theorem lie_subalgebra.ideal_in_normalizer {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (H : L) (x y : L) :
x H.normalizery Hx,y H

A Lie subalgebra is an ideal of its normalizer.

theorem lie_subalgebra.le_normalizer_of_ideal {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (H : L) {N : L} (h : ∀ (x y : L), x Ny Hx,y H) :

The normalizer of a Lie subalgebra H is the maximal Lie subalgebra in which H is a Lie ideal.

theorem lie_subalgebra.normalizer_eq_self_iff {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (H : L) :
@[class]
structure lie_subalgebra.is_cartan_subalgebra {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (H : L) :
Prop

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

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

A nilpotent Lie algebra is its own Cartan subalgebra.