mathlib3 documentation

algebra.lie.cartan_subalgebra

Cartan subalgebras #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_submodule.is_ucs_limit {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {M : Type u_1} [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) :
Prop

Given a Lie module M of a Lie algebra L, lie_submodule.is_ucs_limit 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 lie_subalgebra.is_cartan_subalgebra_iff_is_ucs_limit.

Equations
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 of this typeclass
source
@[protected, instance]
def lie_subalgebra.lie_algebra.is_nilpotent {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (H : lie_subalgebra R L) [H.is_cartan_subalgebra] :
lie_algebra.is_nilpotent R ↥H
source
@[simp]
theorem lie_subalgebra.normalizer_eq_self_of_is_cartan_subalgebra {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (H : lie_subalgebra R L) [H.is_cartan_subalgebra] :
H.to_lie_submodule.normalizer = H.to_lie_submodule
source
@[simp]
theorem lie_subalgebra.ucs_eq_self_of_is_cartan_subalgebra {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (H : lie_subalgebra R L) [H.is_cartan_subalgebra] (k : ℕ) :
lie_submodule.ucs k H.to_lie_submodule = H.to_lie_submodule
source
theorem lie_subalgebra.is_cartan_subalgebra_iff_is_ucs_limit {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (H : lie_subalgebra R L) :
H.is_cartan_subalgebra ↔ H.to_lie_submodule.is_ucs_limit
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.