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.

• LieSubalgebra.normalizer_eq_self_of_engel_le: Lie subalgebras containing an Engel subalgebra are self-normalizing, provided the ambient Lie algebra is Artinian.
• LieSubalgebra.isNilpotent_of_forall_le_engel: A Lie subalgebra of a Noetherian Lie algebra is nilpotent if it is contained in the Engel subalgebra of all its elements.

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

• LieSubalgebra.engel R x = { toSubmodule := ((LieAlgebra.ad R L) x).maxGenEigenspace 0, lie_mem' := ⋯ }

@[simp]

theorem LieSubalgebra.engel_carrier (R : Type u_1) {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) : ↑(LieSubalgebra.engel R x) = ⋂ s ∈ fun (x_1 : Submodule R L) => ∀ (a : ℕ), LinearMap.ker ((LieAlgebra.ad R L) x ^ a) ≤ x_1, ↑s

theorem LieSubalgebra.mem_engel_iff (R : Type u_1) {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) (y : L) : y ∈ LieSubalgebra.engel R x ↔ ∃ (n : ℕ), ((LieAlgebra.ad R L) x ^ n) y = 0

theorem LieSubalgebra.self_mem_engel (R : Type u_1) {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) : x ∈ LieSubalgebra.engel R x

@[simp]

theorem LieSubalgebra.engel_zero (R : Type u_1) {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] : LieSubalgebra.engel R 0 = ⊤

@[simp]

theorem LieSubalgebra.normalizer_engel (R : Type u_1) {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) : (LieSubalgebra.engel R x).normalizer = LieSubalgebra.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.

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 : LieSubalgebra.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.

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 ≤ LieSubalgebra.engel R x) : LieAlgebra.IsNilpotent R ↥H

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