Documentation

Mathlib.Algebra.Lie.Normalizer

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 #

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) :

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 := }
Instances For
    @[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] :
    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) :

    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 := }
    Instances For
      @[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
      def LieSubalgebra.normalizer {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (H : 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 = { toSubmodule := H.toLieSubmodule.normalizer, lie_mem' := }
      Instances For
        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 yH, 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 yH, 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) :

        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) =