English
For an Artinian module M with an endomorphism f, there exists a level n0 such that for all n ≥ n0, ker(f^n) and range(f^n) are complementary in M.
Русский
Для артинанового модуля M с эндоморфизмом f существует такое n0, что для всех n ≥ n0 подмодули ker(f^n) и range(f^n) образуют разложение M в прямую сумму.
LaTeX
$$$ [IsArtinian R M] \\Rightarrow \\forall^\\infty n, IsCompl (\\ker (f^n)) (\\operatorname{range}(f^n)). $$$
Lean4
/-- For any endomorphism of an Artinian module, any sufficiently high iterate has codisjoint kernel
and range. -/
theorem eventually_codisjoint_ker_pow_range_pow (f : Module.End R M) :
∀ᶠ n in atTop, Codisjoint (LinearMap.ker (f ^ n)) (LinearMap.range (f ^ n)) :=
by
obtain ⟨n, hn : ∀ m, n ≤ m → LinearMap.range (f ^ n) = LinearMap.range (f ^ m)⟩ :=
IsArtinian.monotone_stabilizes f.iterateRange
refine eventually_atTop.mpr ⟨n, fun m hm ↦ codisjoint_iff.mpr ?_⟩
simp_rw [← hn _ hm, Submodule.eq_top_iff', Submodule.mem_sup]
intro x
rsuffices ⟨y, hy⟩ : ∃ y, (f ^ m) ((f ^ n) y) = (f ^ m) x
·
exact
⟨x - (f ^ n) y, by simp [hy], (f ^ n) y, by simp⟩
-- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to change `mem_range` into `mem_range (f := _)`
simp_rw [f.pow_apply n, f.pow_apply m, ← iterate_add_apply, ← f.pow_apply (m + n), ← f.pow_apply m, ←
mem_range (f := _), ← hn _ (n.le_add_left m), hn _ hm]
exact LinearMap.mem_range_self (f ^ m) x
