# Documentation

Mathlib.Algebra.Lie.Normalizer

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

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) :
∀ (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) :
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} :
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) :
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) :
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 => , 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] :
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.

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} :
∀ (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.

Instances For
theorem LieSubalgebra.mem_normalizer_iff' {R : Type u_1} {L : Type u_2} [] [] [] (H : ) (x : L) :
∀ (y : L), y Hy, x H
theorem LieSubalgebra.mem_normalizer_iff {R : Type u_1} {L : Type u_2} [] [] [] (H : ) (x : L) :
∀ (y : L), y Hx, y H
theorem LieSubalgebra.le_normalizer {R : Type u_1} {L : Type u_2} [] [] [] (H : ) :
theorem LieSubalgebra.coe_normalizer_eq_normalizer {R : Type u_1} {L : Type u_2} [] [] [] (H : ) :
= ().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 : ) (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 : ) (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₂ : ) :
I, R { x // x 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 : ) :