The normalizer of Lie submodules and subalgebras.

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

• LieSubmodule.normalizer
• LieSubalgebra.normalizer
• LieSubmodule.gc_top_lie_normalizer

Tags

lie algebra, normalizer

def LieSubmodule.normalizer {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) : LieSubmodule R L M

The normalizer of a Lie submodule.

See also LieSubmodule.idealizer.

Equations

• N.normalizer = { carrier := {m : M | ∀ (x : L), ⁅x, m⁆ ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯, lie_mem := ⋯ }

@[simp]

theorem LieSubmodule.mem_normalizer {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) (m : M) : m ∈ N.normalizer ↔ ∀ (x : L), ⁅x, m⁆ ∈ N

@[simp]

theorem LieSubmodule.le_normalizer {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) : N ≤ N.normalizer

theorem LieSubmodule.normalizer_inf {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {N₁ : LieSubmodule R L M} {N₂ : LieSubmodule R L M} : (N₁ ⊓ N₂).normalizer = N₁.normalizer ⊓ N₂.normalizer

theorem LieSubmodule.normalizer_mono {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {N₁ : LieSubmodule R L M} {N₂ : LieSubmodule R L M} (h : N₁ ≤ N₂) : N₁.normalizer ≤ N₂.normalizer

theorem LieSubmodule.monotone_normalizer {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : Monotone LieSubmodule.normalizer

@[simp]

theorem LieSubmodule.comap_normalizer {R : Type u_1} {L : Type u_2} {M : Type u_3} {M' : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] [LieModule R L M'] (N : LieSubmodule R L M) (f : M' →ₗ⁅R,L⁆ M) : LieSubmodule.comap f N.normalizer = (LieSubmodule.comap f N).normalizer

theorem LieSubmodule.top_lie_le_iff_le_normalizer {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) (N' : LieSubmodule R L M) : ⁅⊤, N⁆ ≤ N' ↔ N ≤ N'.normalizer

theorem LieSubmodule.gc_top_lie_normalizer {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : GaloisConnection (fun (N : LieSubmodule R L M) => ⁅⊤, N⁆) LieSubmodule.normalizer

theorem LieSubmodule.normalizer_bot_eq_maxTrivSubmodule (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : ⊥.normalizer = LieModule.maxTrivSubmodule R L M

def LieSubmodule.idealizer {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) : LieIdeal R L

The idealizer of a Lie submodule.

See also LieSubmodule.normalizer.

Equations

• N.idealizer = { carrier := {x : L | ∀ (m : M), ⁅x, m⁆ ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯, lie_mem := ⋯ }

@[simp]

theorem LieSubmodule.mem_idealizer {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) {x : L} : x ∈ N.idealizer ↔ ∀ (m : M), ⁅x, m⁆ ∈ N

@[simp]

theorem LieIdeal.idealizer_eq_normalizer {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : LieSubmodule.idealizer I = LieSubmodule.normalizer I

def LieSubalgebra.normalizer {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) : LieSubalgebra R L

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

Equations

• H.normalizer = let __src := H.toLieSubmodule.normalizer; { toSubmodule := ↑__src, lie_mem' := ⋯ }

theorem LieSubalgebra.mem_normalizer_iff' {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) (x : L) : x ∈ H.normalizer ↔ ∀ y ∈ H, ⁅y, x⁆ ∈ H

theorem LieSubalgebra.mem_normalizer_iff {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) (x : L) : x ∈ H.normalizer ↔ ∀ y ∈ H, ⁅x, y⁆ ∈ H

theorem LieSubalgebra.le_normalizer {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) : H ≤ H.normalizer

theorem LieSubalgebra.coe_normalizer_eq_normalizer {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) : ↑H.toLieSubmodule.normalizer = H.normalizer.toSubmodule

theorem LieSubalgebra.lie_mem_sup_of_mem_normalizer {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} {x : L} {y : L} {z : L} (hx : x ∈ H.normalizer) (hy : y ∈ Submodule.span R {x} ⊔ H.toSubmodule) (hz : z ∈ Submodule.span R {x} ⊔ H.toSubmodule) : ⁅y, z⁆ ∈ Submodule.span R {x} ⊔ H.toSubmodule

theorem LieSubalgebra.ideal_in_normalizer {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} {x : L} {y : L} (hx : x ∈ H.normalizer) (hy : y ∈ H) : ⁅x, y⁆ ∈ H

A Lie subalgebra is an ideal of its normalizer.

theorem LieSubalgebra.exists_nested_lieIdeal_ofLe_normalizer {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} {K : LieSubalgebra R L} (h₁ : H ≤ K) (h₂ : K ≤ H.normalizer) : ∃ (I : LieIdeal R ↥K), lieIdealSubalgebra R (↥K) I = LieSubalgebra.ofLe h₁

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

theorem LieSubalgebra.normalizer_eq_self_iff {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) : H.normalizer = H ↔ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule) = ⊥