mathlib documentation

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.

Main definitions #

Tags #

lie subalgebra, normalizer, idealizer, cartan subalgebra

source
def lie_subalgebra.normalizer {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (H : lie_subalgebra R L) :
lie_subalgebra R 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
source
theorem lie_subalgebra.mem_normalizer_iff {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (H : lie_subalgebra R L) (x : L) :
x ∈ H.normalizer ↔ ∀ (y : L), y ∈ H → ⁅x,y⁆ ∈ H
source
theorem lie_subalgebra.mem_normalizer_iff' {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (H : lie_subalgebra R L) (x : L) :
x ∈ H.normalizer ↔ ∀ (y : L), y ∈ H → ⁅y,x⁆ ∈ H
source
theorem lie_subalgebra.le_normalizer {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (H : lie_subalgebra R L) :
H ≤ H.normalizer
source
theorem lie_subalgebra.ideal_in_normalizer {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (H : lie_subalgebra R L) (x y : L) :
x ∈ H.normalizer → y ∈ H → ⁅x,y⁆ ∈ H

A Lie subalgebra is an ideal of its normalizer.

source
theorem lie_subalgebra.le_normalizer_of_ideal {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (H : lie_subalgebra R L) {N : lie_subalgebra R L} (h : ∀ (x y : L), x ∈ N → y ∈ H → ⁅x,y⁆ ∈ H) :
N ≤ H.normalizer

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

source
theorem lie_subalgebra.normalizer_eq_self_iff {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (H : lie_subalgebra R L) :
H.normalizer = H ↔ lie_module.max_triv_submodule R ↥H (L ⧸ H.to_lie_submodule) = ⊥
source
@[class]
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) :
Prop

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

Instances
source
@[simp]
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) :
↑I.normalizer = ⊤
source
@[protected, instance]
def lie_algebra.top_is_cartan_subalgebra_of_nilpotent {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_algebra.is_nilpotent R L] :
⊤.is_cartan_subalgebra

A nilpotent Lie algebra is its own Cartan subalgebra.