English
Let H be a nilpotent Lie subalgebra of L over R. Then the normalizer of the zero root subalgebra of H in L coincides with the zero root subalgebra itself, i.e. N_L(zeroRootSubalgebra(R,L,H)) = zeroRootSubalgebra(R,L,H).
Русский
Пусть H — нильпотентная подалгебра Ли внутри L над R. Тогда нормализатор нулевой корневой подсалалгебры H в L совпадает с самой нулевой корневой подсалалгеброй: N_L(zeroRootSubalgebra(R,L,H)) = zeroRootSubalgebra(R,L,H).
LaTeX
$$$\bigl(\operatorname{zeroRootSubalgebra}(R,L,H)\bigr).normalizer = \operatorname{zeroRootSubalgebra}(R,L,H)$$$
Lean4
@[simp]
theorem zeroRootSubalgebra_normalizer_eq_self : (zeroRootSubalgebra R L H).normalizer = zeroRootSubalgebra R L H :=
by
refine le_antisymm ?_ (LieSubalgebra.le_normalizer _)
intro x hx
rw [LieSubalgebra.mem_normalizer_iff] at hx
rw [mem_zeroRootSubalgebra]
rintro ⟨y, hy⟩
specialize hx y (le_zeroRootSubalgebra R L H hy)
rw [mem_zeroRootSubalgebra] at hx
obtain ⟨k, hk⟩ := hx ⟨y, hy⟩
rw [← lie_skew, LinearMap.map_neg, neg_eq_zero] at hk
use k + 1
rw [Module.End.iterate_succ, LinearMap.coe_comp, Function.comp_apply, toEnd_apply_apply,
LieSubalgebra.coe_bracket_of_module, Submodule.coe_mk, hk]
