Documentation

Mathlib.Algebra.Lie.EngelSubalgebra

Engel subalgebras #

This file defines Engel subalgebras of a Lie algebra and provides basic related properties.

The Engel subalgebra LieSubalgebra.Engel R x consists of all y : L such that (ad R L x)^n kills y for some n.

Main results #

Engel subalgebras are self-normalizing (LieSubalgebra.normalizer_engel), and minimal ones are nilpotent (TODO), hence Cartan subalgebras.

source
def LieSubalgebra.engel (R : Type u_1) {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) :
LieSubalgebra R L

The Engel subalgebra Engel R x consists of all y : L such that (ad R L x)^n kills y for some n.

Engel subalgebras are self-normalizing (LieSubalgebra.normalizer_engel), and minimal ones are nilpotent, hence Cartan subalgebras.

Equations
    Instances For
      source
      @[simp]
      theorem LieSubalgebra.engel_carrier (R : Type u_1) {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) :
      ↑(engel R x) = ⋂ (s : Submodule R L), ⋂ (_ : ∀ (a : ℕ), LinearMap.ker ((LieAlgebra.ad R L) x ^ a) ≤ s), ↑s
      source
      theorem LieSubalgebra.mem_engel_iff (R : Type u_1) {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (x y : L) :
      y ∈ engel R x ↔ ∃ (n : ℕ), ((LieAlgebra.ad R L) x ^ n) y = 0
      source
      theorem LieSubalgebra.self_mem_engel (R : Type u_1) {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) :
      x ∈ engel R x
      source
      @[simp]
      theorem LieSubalgebra.engel_zero (R : Type u_1) {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] :
      engel R 0 = ⊤
      source
      @[simp]
      theorem LieSubalgebra.normalizer_engel (R : Type u_1) {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) :
      (engel R x).normalizer = engel R x

      Engel subalgebras are self-normalizing. See LieSubalgebra.normalizer_eq_self_of_engel_le for a proof that Lie-subalgebras containing an Engel subalgebra are also self-normalizing, provided that the ambient Lie algebra is artinina.

      source
      theorem LieSubalgebra.normalizer_eq_self_of_engel_le {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] [IsArtinian R L] (H : LieSubalgebra R L) (x : L) (h : engel R x ≤ H) :
      H.normalizer = H

      A Lie-subalgebra of an Artinian Lie algebra is self-normalizing if it contains an Engel subalgebra. See LieSubalgebra.normalizer_engel for a proof that Engel subalgebras are self-normalizing, avoiding the Artinian condition.

      source
      theorem LieSubalgebra.isNilpotent_of_forall_le_engel {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] [IsNoetherian R L] (H : LieSubalgebra R L) (h : ∀ x ∈ H, H ≤ engel R x) :
      LieRing.IsNilpotent ↥H

      A Lie subalgebra of a Noetherian Lie algebra is nilpotent if it is contained in the Engel subalgebra of all its elements.