English
Let H be a Lie subalgebra of L, x ∈ L, and suppose engel(R, x) ≤ H. If L is Artinian, then H is self-normalizing; i.e., normalizer(H) = H.
Русский
Пусть H ‑ подалгебра Ли и engel(R, x) ≤ H. Пусть L искусственна Артинова. Тогда H нормализуется самим собой: normalizer(H) = H.
LaTeX
$$$[\IsArtinian R L] \,(H: LieSubalgebra R L) \,(x: L) \,(h: engel(R,x) \le H) \Rightarrow \operatorname{normalizer}(H) = H$$$
Lean4
/-- 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 normalizer_eq_self_of_engel_le [IsArtinian R L] (H : LieSubalgebra R L) (x : L) (h : engel R x ≤ H) :
normalizer H = H := by
set N := normalizer H
apply le_antisymm _ (le_normalizer H)
calc
N.toSubmodule ≤ (engel R x).toSubmodule ⊔ H.toSubmodule := ?_
_ = H := by rwa [sup_eq_right]
have aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H := by
intro n hn
rw [mem_normalizer_iff] at hn
specialize hn x (h (self_mem_engel R x))
rwa [← lie_skew, neg_mem_iff (G := L)]
have aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N := fun n hn ↦ le_normalizer H (aux₁ _ hn)
let dx : N →ₗ[R] N := (ad R L x).restrict aux₂
obtain ⟨k, hk⟩ : ∃ a, ∀ b ≥ a, Codisjoint (LinearMap.ker (dx ^ b)) (LinearMap.range (dx ^ b)) :=
eventually_atTop.mp <| dx.eventually_codisjoint_ker_pow_range_pow
specialize hk (k + 1) (Nat.le_add_right k 1)
rw [← Submodule.map_subtype_top N.toSubmodule, Submodule.map_le_iff_le_comap]
apply hk
· rw [← Submodule.map_le_iff_le_comap]
apply le_sup_of_le_left
rw [Submodule.map_le_iff_le_comap]
intro y hy
simp only [Submodule.mem_comap, mem_engel_iff, mem_toSubmodule]
use k + 1
clear hk; revert hy
generalize k + 1 = k
induction k generalizing y with
| zero =>
cases y; intro hy; simp only [pow_zero, Module.End.one_apply]
exact (AddSubmonoid.mk_eq_zero N.toAddSubmonoid).mp hy
| succ k ih => solve_by_elim
· rw [← Submodule.map_le_iff_le_comap]
apply le_sup_of_le_right
rw [Submodule.map_le_iff_le_comap]
rintro _ ⟨y, rfl⟩
simp only [pow_succ', Module.End.mul_apply, Submodule.mem_comap, mem_toSubmodule]
apply aux₁
simp only [Submodule.coe_subtype, SetLike.coe_mem]
