English
For any X with IsNoetherianObject, every functor F: Nat ⥤ MonoOver X is eventually constant.
Русский
Если X является нётеровским, то любая подкатегория F: Nat ⥤ MonoOver X становится константной на хвосте.
LaTeX
$$$\text{IsNoetherianObject}(X) \Rightarrow \forall F:\mathbb{N} \to \mathrm{MonoOver}(X),\ \mathrm{IsFiltered.IsEventuallyConstant}(F).$$$
Lean4
theorem isNoetherianObject_iff_isEventuallyConstant :
IsNoetherianObject X ↔ ∀ (F : ℕ ⥤ MonoOver X), IsFiltered.IsEventuallyConstant F :=
by
rw [isNoetherianObject_iff_monotone_chain_condition]
refine ⟨fun h G ↦ ?_, fun h F ↦ ?_⟩
· obtain ⟨n, hn⟩ := h (G ⋙ (Subobject.equivMonoOver _).inverse).toOrderHom
refine ⟨n, fun m hm ↦ ?_⟩
rw [MonoOver.isIso_iff_subobjectMk_eq]
exact hn m (leOfHom hm)
· obtain ⟨n, hn⟩ := h (F.monotone.functor ⋙ Subobject.representative)
refine ⟨n, fun m hm ↦ ?_⟩
simpa [← MonoOver.isIso_iff_isIso_left, isIso_iff_of_reflects_iso, PartialOrder.isIso_iff_eq] using hn (homOfLE hm)
