English
There is an instance asserting that the zero weight space is nilpotent as an L-module when X are nilpotent and module is Noetherian.
Русский
Существует инстанс нильпотентности нулевого весового пространства как L-части модуля при нильпотентности и Noetherian условиях.
LaTeX
$$IsNilpotent L (genWeightSpace M (0 : L → R))$$
Lean4
theorem isNilpotent_toEnd_sub_algebraMap [IsNoetherian R M] (χ : L → R) (x : L) :
_root_.IsNilpotent <| toEnd R L (genWeightSpace M χ) x - algebraMap R _ (χ x) :=
by
have :
toEnd R L (genWeightSpace M χ) x - algebraMap R _ (χ x) =
(toEnd R L M x - algebraMap R _ (χ x)).restrict
(fun m hm ↦ sub_mem (LieSubmodule.lie_mem _ hm) (Submodule.smul_mem _ _ hm)) :=
by rfl
obtain ⟨k, hk⟩ := exists_genWeightSpace_le_ker_of_isNoetherian M χ x
use k
ext ⟨m, hm⟩
simp only [this, Module.End.pow_restrict _, LinearMap.zero_apply, ZeroMemClass.coe_zero, ZeroMemClass.coe_eq_zero]
exact ZeroMemClass.coe_eq_zero.mp (hk hm)
