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

• One or more equations did not get rendered due to their size.

@[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 ∈ LieSubmodule.normalizer N ↔ ∀ (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 ≤ LieSubmodule.normalizer N

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} : LieSubmodule.normalizer (N₁ ⊓ N₂) = LieSubmodule.normalizer N₁ ⊓ LieSubmodule.normalizer N₂

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 (LieSubmodule.normalizer N) = LieSubmodule.normalizer (LieSubmodule.comap f N)

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 ≤ LieSubmodule.normalizer N'

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] : LieSubmodule.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

• One or more equations did not get rendered due to their size.

@[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 ∈ LieSubmodule.idealizer N ↔ ∀ (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

• LieSubalgebra.normalizer H = let __src := LieSubmodule.normalizer (LieSubalgebra.toLieSubmodule H); { 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 ∈ LieSubalgebra.normalizer H ↔ ∀ 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 ∈ LieSubalgebra.normalizer H ↔ ∀ 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 ≤ LieSubalgebra.normalizer H

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) : ↑(LieSubmodule.normalizer (LieSubalgebra.toLieSubmodule H)) = (LieSubalgebra.normalizer H).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 ∈ LieSubalgebra.normalizer H) (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 ∈ LieSubalgebra.normalizer H) (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 ≤ LieSubalgebra.normalizer H) : ∃ (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) : LieSubalgebra.normalizer H = H ↔ LieModule.maxTrivSubmodule R (↥H) (L ⧸ LieSubalgebra.toLieSubmodule H) = ⊥