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) :
lie_submodule R L M
The normalizer of a Lie submodule.
@[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) :
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) :
N ≤ N.normalizer
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
theorem
lie_submodule.monotone_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] :
@[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) :
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]
[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.normalizer
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]
[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 normalizer is in fact a Lie
subalgebra.
Equations
- H.normalizer = {to_submodule := {carrier := H.to_lie_submodule.normalizer.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_normalizer_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.normalizer) = ↑(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) :
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) = ⊥