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 #
lie_submodule.is_ucs_limitlie_subalgebra.is_cartan_subalgebralie_subalgebra.is_cartan_subalgebra_iff_is_ucs_limit
Tags #
lie subalgebra, normalizer, idealizer, cartan subalgebra
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.
@[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
- nilpotent : lie_algebra.is_nilpotent R ↥H
- self_normalizing : H.normalizer = H
A Cartan subalgebra is a nilpotent, self-normalizing subalgebra.
Instances of this typeclass
@[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] :
@[simp]
theorem
lie_subalgebra.centralizer_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] :
@[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 : ℕ) :
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) :
@[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 = ⊤
@[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] :
A nilpotent Lie algebra is its own Cartan subalgebra.