English
X is Artinian iff every functor F: Nat ⥤ (MonoOver X)ᵒᵖ is eventually constant.
Русский
X артиняннь, если каждый функтор F: Nat ⥤ (MonoOver X)ᵒᵖ в итоге становится константным.
LaTeX
$$$\\mathrm{IsArtinianObject}(X) \\iff \\forall F: \\mathbb{N} \\to (\\mathrm{MonoOver}(X))^{\\mathrm{op}}, \\mathrm{IsFiltered.IsEventuallyConstant}(F)$$$
Lean4
theorem isArtinianObject_iff_isEventuallyConstant :
IsArtinianObject X ↔ ∀ (F : ℕ ⥤ (MonoOver X)ᵒᵖ), IsFiltered.IsEventuallyConstant F :=
by
rw [isArtinianObject_iff_antitone_chain_condition]
refine ⟨fun h G ↦ ?_, fun h F ↦ ?_⟩
· obtain ⟨n, hn⟩ := h ⟨_, (G ⋙ (Subobject.equivMonoOver X).inverse.op ⋙ (orderDualEquivalence _).inverse).monotone⟩
refine ⟨n, fun m hm ↦ ?_⟩
rw [← isIso_unop_iff, MonoOver.isIso_iff_subobjectMk_eq]
exact (hn m (leOfHom hm)).symm
· obtain ⟨n, hn⟩ := h (F.monotone.functor ⋙ (orderDualEquivalence _).functor ⋙ Subobject.representative.op)
refine ⟨n, fun m hm ↦ Eq.symm ?_⟩
simpa [isIso_op_iff, isIso_iff_of_reflects_iso, PartialOrder.isIso_iff_eq] using hn (homOfLE hm)
