English
For a Noetherian module M and endomorphism f, the join of kernels and the meet of ranges form a complementary pair: IsCompl(⨆ n ker(f^n), ⨅ n range(f^n)).
Русский
Пусть M — Noetherian модуль и f — эндоморфизм. Тогда сумма подмодулей ker(f^n) по всем n и пересечение range(f^n) по всем n образуют дополняющую пару: IsCompl(⨆ n ker(f^n), ⨅ n range(f^n)).
LaTeX
$$$ [IsNoetherian\\; R\\; M] \\Rightarrow IsCompl \\left(\\bigl\\lceil\\ker(f^n)\\bigr\rceil_{n}, \\bigl\\lfloor\\operatorname{range}(f^n)\\bigr\rceil_{n}\\right). $$$
Lean4
/-- This is the Fitting decomposition of the module `M` with respect to the endomorphism `f`.
See also `LinearMap.eventually_isCompl_ker_pow_range_pow` for an alternative spelling. -/
theorem isCompl_iSup_ker_pow_iInf_range_pow [IsNoetherian R M] (f : M →ₗ[R] M) :
IsCompl (⨆ n, LinearMap.ker (f ^ n)) (⨅ n, LinearMap.range (f ^ n)) :=
by
obtain ⟨k, hk⟩ :=
eventually_atTop.mp <|
f.eventually_isCompl_ker_pow_range_pow.and <| f.eventually_iInf_range_pow_eq.and f.eventually_iSup_ker_pow_eq
obtain ⟨h₁, h₂, h₃⟩ := hk k (le_refl k)
rwa [h₂, h₃]
