The normalizer of Lie submodules and subalgebras. #

Given a Lie module M over a Lie subalgebra L, the normalizer of a Lie submodule N ⊆ M is the Lie submodule with underlying set { m | ∀ (x : L), ⁅x, m⁆ ∈ N }.

The lattice of Lie submodules thus has two natural operations, the normalizer: N ↦ N.normalizer and the ideal operation: N ↦ ⁅⊤, N⁆; these are adjoint, i.e., they form a Galois connection. This adjointness is the reason that we may define nilpotency in terms of either the upper or lower central series.

Given a Lie subalgebra H ⊆ L, we may regard H as a Lie submodule of L over H, and thus consider the normalizer. This turns out to be a Lie subalgebra.

Main definitions #

• LieSubmodule.normalizer
• LieSubalgebra.normalizer
• LieSubmodule.gc_top_lie_normalizer

Tags #

lie algebra, normalizer

def LieSubmodule.normalizer {R : Type u_1} {L : Type u_2} {M : Type u_3} [] [] [] [] [Module R M] [] [LieModule R L M] (N : LieSubmodule R L M) :

The normalizer of a Lie submodule.

See also LieSubmodule.idealizer.

Equations
• N.normalizer = { carrier := {m : M | ∀ (x : L), x, m N}, add_mem' := , zero_mem' := , smul_mem' := , lie_mem := }
Instances For
@[simp]
theorem LieSubmodule.mem_normalizer {R : Type u_1} {L : Type u_2} {M : Type u_3} [] [] [] [] [Module R M] [] [LieModule R L M] (N : LieSubmodule R L M) (m : M) :
m N.normalizer ∀ (x : L), x, m N
@[simp]
theorem LieSubmodule.le_normalizer {R : Type u_1} {L : Type u_2} {M : Type u_3} [] [] [] [] [Module R M] [] [LieModule R L M] (N : LieSubmodule R L M) :
N N.normalizer
theorem LieSubmodule.normalizer_inf {R : Type u_1} {L : Type u_2} {M : Type u_3} [] [] [] [] [Module R M] [] [LieModule R L M] {N₁ : LieSubmodule R L M} {N₂ : LieSubmodule R L M} :
(N₁ N₂).normalizer = N₁.normalizer N₂.normalizer
theorem LieSubmodule.normalizer_mono {R : Type u_1} {L : Type u_2} {M : Type u_3} [] [] [] [] [Module R M] [] [LieModule R L M] {N₁ : LieSubmodule R L M} {N₂ : LieSubmodule R L M} (h : N₁ N₂) :
N₁.normalizer N₂.normalizer
theorem LieSubmodule.monotone_normalizer {R : Type u_1} {L : Type u_2} {M : Type u_3} [] [] [] [] [Module R M] [] [LieModule R L M] :
Monotone LieSubmodule.normalizer
@[simp]
theorem LieSubmodule.comap_normalizer {R : Type u_1} {L : Type u_2} {M : Type u_3} {M' : Type u_4} [] [] [] [] [Module R M] [] [LieModule R L M] [] [Module R M'] [] [LieModule R L M'] (N : LieSubmodule R L M) (f : M' →ₗ⁅R,L M) :
LieSubmodule.comap f N.normalizer = ().normalizer
theorem LieSubmodule.top_lie_le_iff_le_normalizer {R : Type u_1} {L : Type u_2} {M : Type u_3} [] [] [] [] [Module R M] [] [LieModule R L M] (N : LieSubmodule R L M) (N' : LieSubmodule R L M) :
, N N' N N'.normalizer
theorem LieSubmodule.gc_top_lie_normalizer {R : Type u_1} {L : Type u_2} {M : Type u_3} [] [] [] [] [Module R M] [] [LieModule R L M] :
GaloisConnection (fun (N : LieSubmodule R L M) => , N) LieSubmodule.normalizer
theorem LieSubmodule.normalizer_bot_eq_maxTrivSubmodule (R : Type u_1) (L : Type u_2) (M : Type u_3) [] [] [] [] [Module R M] [] [LieModule R L M] :
.normalizer =
def LieSubmodule.idealizer {R : Type u_1} {L : Type u_2} {M : Type u_3} [] [] [] [] [Module R M] [] [LieModule R L M] (N : LieSubmodule R L M) :

The idealizer of a Lie submodule.

See also LieSubmodule.normalizer.

Equations
• N.idealizer = { carrier := {x : L | ∀ (m : M), x, m N}, add_mem' := , zero_mem' := , smul_mem' := , lie_mem := }
Instances For
@[simp]
theorem LieSubmodule.mem_idealizer {R : Type u_1} {L : Type u_2} {M : Type u_3} [] [] [] [] [Module R M] [] [LieModule R L M] (N : LieSubmodule R L M) {x : L} :
x N.idealizer ∀ (m : M), x, m N
@[simp]
theorem LieIdeal.idealizer_eq_normalizer {R : Type u_1} {L : Type u_2} [] [] [] (I : LieIdeal R L) :
def LieSubalgebra.normalizer {R : Type u_1} {L : Type u_2} [] [] [] (H : ) :

Regarding a Lie subalgebra H ⊆ L as a module over itself, its normalizer is in fact a Lie subalgebra.

Equations
• H.normalizer = let __src := H.toLieSubmodule.normalizer; { toSubmodule := __src, lie_mem' := }
Instances For
theorem LieSubalgebra.mem_normalizer_iff' {R : Type u_1} {L : Type u_2} [] [] [] (H : ) (x : L) :
x H.normalizer yH, y, x H
theorem LieSubalgebra.mem_normalizer_iff {R : Type u_1} {L : Type u_2} [] [] [] (H : ) (x : L) :
x H.normalizer yH, x, y H
theorem LieSubalgebra.le_normalizer {R : Type u_1} {L : Type u_2} [] [] [] (H : ) :
H H.normalizer
theorem LieSubalgebra.coe_normalizer_eq_normalizer {R : Type u_1} {L : Type u_2} [] [] [] (H : ) :
H.toLieSubmodule.normalizer = H.normalizer.toSubmodule
theorem LieSubalgebra.lie_mem_sup_of_mem_normalizer {R : Type u_1} {L : Type u_2} [] [] [] {H : } {x : L} {y : L} {z : L} (hx : x H.normalizer) (hy : y Submodule.span R {x} H.toSubmodule) (hz : z Submodule.span R {x} H.toSubmodule) :
y, z Submodule.span R {x} H.toSubmodule
theorem LieSubalgebra.ideal_in_normalizer {R : Type u_1} {L : Type u_2} [] [] [] {H : } {x : L} {y : L} (hx : x H.normalizer) (hy : y H) :

A Lie subalgebra is an ideal of its normalizer.

theorem LieSubalgebra.exists_nested_lieIdeal_ofLe_normalizer {R : Type u_1} {L : Type u_2} [] [] [] {H : } {K : } (h₁ : H K) (h₂ : K H.normalizer) :
∃ (I : LieIdeal R K), lieIdealSubalgebra R (K) I =

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

theorem LieSubalgebra.normalizer_eq_self_iff {R : Type u_1} {L : Type u_2} [] [] [] (H : ) :
H.normalizer = H LieModule.maxTrivSubmodule R (H) (L H.toLieSubmodule) =