English
If H is a Lie subalgebra of a Noetherian Lie algebra L and H is contained in engel(R, x) for every x ∈ H (i.e., H ≤ engel(R, x) for all x ∈ H), then H is nilpotent.
Русский
Если H ‑ подалгебра Noetherian-алгебры L и для каждого x ∈ H выполняется H ≤ engel(R, x), то H нильпотентна.
LaTeX
$$$[\IsNoetherian R L] \,(H: LieSubalgebra R L) \,(h: \forall x \in H, H \le engel(R,x)) \Rightarrow \operatorname{IsNilpotent} H$$
Lean4
/-- A Lie subalgebra of a Noetherian Lie algebra is nilpotent
if it is contained in the Engel subalgebra of all its elements. -/
theorem isNilpotent_of_forall_le_engel [IsNoetherian R L] (H : LieSubalgebra R L) (h : ∀ x ∈ H, H ≤ engel R x) :
LieRing.IsNilpotent H := by
rw [LieAlgebra.isNilpotent_iff_forall (R := R)]
intro x
let K : ℕ →o Submodule R H := ⟨fun n ↦ LinearMap.ker ((ad R H x) ^ n), fun m n hmn ↦ ?mono⟩
case mono =>
intro y hy
rw [LinearMap.mem_ker] at hy ⊢
exact Module.End.pow_map_zero_of_le hmn hy
obtain ⟨n, hn⟩ := monotone_stabilizes_iff_noetherian.mpr inferInstance K
use n
ext y
rw [coe_ad_pow]
specialize h x x.2 y.2
rw [mem_engel_iff] at h
obtain ⟨m, hm⟩ := h
obtain (hmn | hmn) : m ≤ n ∨ n ≤ m := le_total m n
· exact Module.End.pow_map_zero_of_le hmn hm
· have : ∀ k : ℕ, ((ad R L) x ^ k) y = 0 ↔ y ∈ K k := by simp [K, Subtype.ext_iff, coe_ad_pow]
rwa [this, ← hn m hmn, ← this] at hm
