English
For a Noetherian M and a linear map f: M → M, there exists n such that ker(f^m) = ker(f^n) for all m ≥ n.
Русский
Для модуля M и линейного отображения f: M → M существует n, такое что для всех m ≥ n выполняется ker(f^m) = ker(f^n).
LaTeX
$$$\\exists n: \\mathbb{N}, \\forall m \\ge n, \\ker(f^m) = \\ker(f^n)$$$
Lean4
theorem eventually_iSup_ker_pow_eq (f : M →ₗ[R] M) :
∀ᶠ n in atTop, ⨆ m, LinearMap.ker (f ^ m) = LinearMap.ker (f ^ n) :=
by
obtain ⟨n, hn : ∀ m, n ≤ m → ker (f ^ n) = ker (f ^ m)⟩ :=
monotone_stabilizes_iff_noetherian.mpr inferInstance f.iterateKer
refine eventually_atTop.mpr ⟨n, fun m hm ↦ ?_⟩
refine le_antisymm (iSup_le fun l ↦ ?_) (le_iSup (fun i ↦ LinearMap.ker (f ^ i)) m)
rcases le_or_gt m l with h | h
· rw [← hn _ (hm.trans h), hn _ hm]
· exact f.iterateKer.monotone h.le
