English
For any x, the normalizer of engel(R, x) equals engel(R, x). In symbols: normalizer(engel(R, x)) = engel(R, x).
Русский
Нормализатор удобно совпадает с энгель-подалгеброй: normalizer(engel(R, x)) = engel(R, x).
LaTeX
$$$\operatorname{normalizer}(\operatorname{engel}(R,x)) = \operatorname{engel}(R,x)$$$
Lean4
/-- 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. -/
@[simp]
theorem normalizer_engel (x : L) : normalizer (engel R x) = engel R x :=
by
apply le_antisymm _ (le_normalizer _)
intro y hy
rw [mem_normalizer_iff] at hy
specialize hy x (self_mem_engel R x)
rw [← lie_skew, neg_mem_iff (G := L), mem_engel_iff] at hy
rcases hy with ⟨n, hn⟩
rw [mem_engel_iff]
use n + 1
rw [pow_succ, Module.End.mul_apply]
exact hn
