English
For a Noetherian module M and an endomorphism f, there exists an n such that ker(f^n) and range(f^n) are complementary, i.e., M = ker(f^n) ⊕ range(f^n).
Русский
Пусть M — Noetherian модуль и f — эндоморфизм. Тогда существует такое n, что M = ker(f^n) ⊕ range(f^n).
LaTeX
$$$ [IsNoetherian\\; R\\; M] \\Rightarrow \\exists n\\in\\mathbb{N}, IsCompl (\\ker (f^n)) (\\operatorname{range}(f^n)). $$$
Lean4
/-- This is the Fitting decomposition of the module `M` with respect to the endomorphism `f`.
See also `LinearMap.isCompl_iSup_ker_pow_iInf_range_pow` for an alternative spelling. -/
theorem eventually_isCompl_ker_pow_range_pow [IsNoetherian R M] (f : Module.End R M) :
∀ᶠ n in atTop, IsCompl (LinearMap.ker (f ^ n)) (LinearMap.range (f ^ n)) :=
by
filter_upwards [f.eventually_disjoint_ker_pow_range_pow.and f.eventually_codisjoint_ker_pow_range_pow] with n hn
simpa only [isCompl_iff]
