# mathlibdocumentation

algebra.lie.centralizer

# The centralizer of a Lie submodule and the normalizer of a Lie subalgebra. #

Given a Lie module M over a Lie subalgebra L, the centralizer 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 centralizer: N ↦ N.centralizer 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 centralizer. This turns out to be a Lie subalgebra and is known as the normalizer.

## Main definitions #

• lie_submodule.centralizer
• lie_subalgebra.normalizer
• lie_submodule.gc_top_lie_centralizer

## Tags #

lie algebra, centralizer, normalizer

def lie_submodule.centralizer {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 centralizer of a Lie submodule.

Equations
@[simp]
theorem lie_submodule.mem_centralizer {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.centralizer ∀ (x : L), x,m N
theorem lie_submodule.le_centralizer {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.centralizer_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₂).centralizer = N₁.centralizer N₂.centralizer
theorem lie_submodule.monotone_centalizer {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_centralizer {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_centralizer {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_centralizer {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.centralizer_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 centralizer is in fact a Lie subalgebra. This is called the normalizer of the 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 Hy,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 Hx,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_centralizer_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) :
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) :