# mathlib3documentation

algebra.lie.normalizer

# The normalizer of a Lie submodules and subalgebras. #

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

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 #

• lie_submodule.normalizer
• lie_subalgebra.normalizer
• lie_submodule.gc_top_lie_normalizer

## Tags #

lie algebra, normalizer

def lie_submodule.normalizer {R : Type u_1} {L : Type u_2} {M : Type u_3} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) :
M

The normalizer of a Lie submodule.

Equations
@[simp]
theorem lie_submodule.mem_normalizer {R : Type u_1} {L : Type u_2} {M : Type u_3} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) (m : M) :
m N.normalizer (x : L), x, m N
theorem lie_submodule.le_normalizer {R : Type u_1} {L : Type u_2} {M : Type u_3} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) :
theorem lie_submodule.normalizer_inf {R : Type u_1} {L : Type u_2} {M : Type u_3} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] {N₁ N₂ : M} :
(N₁ N₂).normalizer = N₁.normalizer N₂.normalizer
theorem lie_submodule.monotone_normalizer {R : Type u_1} {L : Type u_2} {M : Type u_3} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
@[simp]
theorem lie_submodule.comap_normalizer {R : Type u_1} {L : Type u_2} {M : Type u_3} {M' : Type u_4} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] [add_comm_group M'] [ M'] [ M'] [ L M'] (N : M) (f : M' →ₗ⁅R,L M) :
theorem lie_submodule.top_lie_le_iff_le_normalizer {R : Type u_1} {L : Type u_2} {M : Type u_3} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N N' : M) :
theorem lie_submodule.gc_top_lie_normalizer {R : Type u_1} {L : Type u_2} {M : Type u_3} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
theorem lie_submodule.normalizer_bot_eq_max_triv_submodule (R : Type u_1) (L : Type u_2) (M : Type u_3) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
def lie_subalgebra.normalizer {R : Type u_1} {L : Type u_2} [comm_ring R] [lie_ring L] [ L] (H : L) :

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

Equations
theorem lie_subalgebra.mem_normalizer_iff' {R : Type u_1} {L : Type u_2} [comm_ring R] [lie_ring L] [ L] (H : L) (x : L) :
x H.normalizer (y : L), y H y, x H
theorem lie_subalgebra.mem_normalizer_iff {R : Type u_1} {L : Type u_2} [comm_ring R] [lie_ring L] [ L] (H : L) (x : L) :
x H.normalizer (y : L), y H x, y H
theorem lie_subalgebra.le_normalizer {R : Type u_1} {L : Type u_2} [comm_ring R] [lie_ring L] [ L] (H : L) :
theorem lie_subalgebra.coe_normalizer_eq_normalizer {R : Type u_1} {L : Type u_2} [comm_ring R] [lie_ring L] [ L] (H : L) :
theorem lie_subalgebra.lie_mem_sup_of_mem_normalizer {R : Type u_1} {L : Type u_2} [comm_ring R] [lie_ring L] [ L] {H : L} {x y z : L} (hx : x H.normalizer) (hy : y {x} H) (hz : z {x} H) :
y, z {x} H
theorem lie_subalgebra.ideal_in_normalizer {R : Type u_1} {L : Type u_2} [comm_ring R] [lie_ring L] [ L] {H : L} {x y : L} (hx : x H.normalizer) (hy : y H) :

A Lie subalgebra is an ideal of its normalizer.

theorem lie_subalgebra.exists_nested_lie_ideal_of_le_normalizer {R : Type u_1} {L : Type u_2} [comm_ring R] [lie_ring L] [ L] {H K : L} (h₁ : H K) (h₂ : K H.normalizer) :
(I : K),

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

theorem lie_subalgebra.normalizer_eq_self_iff {R : Type u_1} {L : Type u_2} [comm_ring R] [lie_ring L] [ L] (H : L) :