English
For a Noetherian module M and an endomorphism f, there exists N such that for all n ≥ N, the kernel of f^n and the range of f^n are disjoint.
Русский
Для нётеровского модуля M и эндоморфизма f существует N such that для всех n ≥ N, ядро f^n и образ f^n распр. пересечения пусты.
LaTeX
$$$\\exists N: \\mathbb{N}, \\forall n \\ge N, \\operatorname{Disjoint}(\\ker(f^n), \\operatorname{range}(f^n))$$$
Lean4
/-- For an endomorphism of a Noetherian module, any sufficiently large iterate has disjoint kernel
and range. -/
theorem eventually_disjoint_ker_pow_range_pow (f : End R M) :
∀ᶠ n in atTop, Disjoint (LinearMap.ker (f ^ n)) (LinearMap.range (f ^ n)) :=
by
obtain ⟨n, hn : ∀ m, n ≤ m → LinearMap.ker (f ^ n) = LinearMap.ker (f ^ m)⟩ :=
monotone_stabilizes_iff_noetherian.mpr inferInstance f.iterateKer
refine eventually_atTop.mpr ⟨n, fun m hm ↦ disjoint_iff.mpr ?_⟩
rw [← hn _ hm, Submodule.eq_bot_iff]
rintro - ⟨hx, ⟨x, rfl⟩⟩
apply pow_map_zero_of_le hm
replace hx : x ∈ LinearMap.ker (f ^ (n + m)) := by
simpa [f.pow_apply n, f.pow_apply m, ← f.pow_apply (n + m), ← iterate_add_apply] using hx
rwa [← hn _ (n.le_add_right m)] at hx
