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

H.normalizer = {to_submodule := {carrier := {x : L | ∀ (y : L), y ∈ H → ⁅x,y⁆ ∈ H}, zero_mem' := _, add_mem' := _, smul_mem' := _}, lie_mem' := _}

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.lie_mem_sup_of_mem_normalizer {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {H : lie_subalgebra R L} {x y z : L} (hx : x ∈ H.normalizer) (hy : y ∈ submodule.span R {x} ⊔ ↑H) (hz : z ∈ submodule.span R {x} ⊔ ↑H) :

⁅y,z⁆ ∈ submodule.span R {x} ⊔ ↑H

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.exists_nested_lie_ideal_of_le_normalizer {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {H K : lie_subalgebra R L} (h₁ : H ≤ K) (h₂ : K ≤ H.normalizer) :

∃ (I : lie_ideal R ↥K), ↑I = lie_subalgebra.of_le h₁

A Lie subalgebra H is an ideal of any Lie subalgebra K containing H and contained in the normalizer of H.

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 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

nilpotent : lie_algebra.is_nilpotent R ↥H
self_normalizing : H.normalizer = H

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

Instances

lie_algebra.top_is_cartan_subalgebra_of_nilpotent

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.