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 #
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]
[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) :
lie_submodule R L M
The centralizer of a Lie submodule.
@[simp]
theorem
lie_submodule.mem_centralizer
{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) :
theorem
lie_submodule.le_centralizer
{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) :
N ≤ N.centralizer
theorem
lie_submodule.centralizer_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₂).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]
[lie_algebra R L]
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R 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]
[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_centralizer
{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) :
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]
[lie_algebra R L]
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R L M] :
galois_connection (λ (N : lie_submodule R L M), ⁅⊤,N⁆) lie_submodule.centralizer
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]
[lie_algebra R L]
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module 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) :
lie_subalgebra R 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
- H.normalizer = {to_submodule := {carrier := H.to_lie_submodule.centralizer.carrier, add_mem' := _, zero_mem' := _, smul_mem' := _}, lie_mem' := _}
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) :
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) :
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) :
H ≤ H.normalizer
theorem
lie_subalgebra.coe_centralizer_eq_normalizer
{R : Type u_1}
{L : Type u_2}
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
(H : lie_subalgebra R L) :
↑(H.to_lie_submodule.centralizer) = ↑(H.normalizer)
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) :
∃ (I : lie_ideal R ↥K), ↑I = lie_subalgebra.of_le h₁
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]
[lie_algebra R L]
(H : lie_subalgebra R L) :
H.normalizer = H ↔ lie_module.max_triv_submodule R ↥H (L ⧸ H.to_lie_submodule) = ⊥