English
If f is a nilpotent endomorphism on a module and hp ≤ hq hold for submodules p ⊆ q, then restricting f to p or q preserves nilpotency under suitable maps.
Русский
Если дужа есть нильпотентный эндоморфизм и ограничение по подмодулям сохраняет структурные условия, то ограничение сохраняет нильпотентность.
LaTeX
$$IsNilpotent (f.restrict hq) → IsNilpotent (f.restrict hp)$$
Lean4
theorem isNilpotent_restrict_of_le {f : End R M} {p q : Submodule R M} {hp : MapsTo f p p} {hq : MapsTo f q q}
(h : p ≤ q) (hf : IsNilpotent (f.restrict hq)) : IsNilpotent (f.restrict hp) :=
by
obtain ⟨n, hn⟩ := hf
use n
ext ⟨x, hx⟩
replace hn := DFunLike.congr_fun hn ⟨x, h hx⟩
simp_rw [LinearMap.zero_apply, ZeroMemClass.coe_zero, ZeroMemClass.coe_eq_zero] at hn ⊢
rw [Module.End.pow_restrict, LinearMap.restrict_apply] at hn ⊢
ext
exact (congr_arg Subtype.val hn :)
