mathlib3 documentation

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 #

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] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L 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] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L 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] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) :
theorem lie_submodule.normalizer_inf {R : Type u_1} {L : Type u_2} {M : Type u_3} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] {N₁ N₂ : lie_submodule R L M} :
(N₁ N₂).normalizer = N₁.normalizer N₂.normalizer
@[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] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group M'] [module R M'] [lie_ring_module L M'] [lie_module R L M'] (N : lie_submodule R L 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] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N N' : lie_submodule R L M) :
def lie_subalgebra.normalizer {R : Type u_1} {L : Type u_2} [comm_ring R] [lie_ring L] [lie_algebra R L] (H : lie_subalgebra R 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] [lie_algebra R L] (H : lie_subalgebra R 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] [lie_algebra R L] (H : lie_subalgebra R 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] [lie_algebra R L] (H : lie_subalgebra R L) :
theorem lie_subalgebra.lie_mem_sup_of_mem_normalizer {R : Type u_1} {L : Type u_2} [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) :
theorem lie_subalgebra.ideal_in_normalizer {R : Type u_1} {L : Type u_2} [comm_ring R] [lie_ring L] [lie_algebra R L] {H : lie_subalgebra R 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] [lie_algebra R L] {H K : lie_subalgebra R L} (h₁ : H K) (h₂ : K H.normalizer) :

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