English
Let C be a cofiltered category and F : C ⥤ D a functor. Suppose that for every object d in D there exists an object c in C and a morphism F.obj c ⟶ d, and that for all d ∈ D and for every pair of arrows s,s' : F.obj c ⟶ d there exists c' ∈ C and t : c' ⟶ c such that F.map t ≫ s = F.map t ≫ s'. Then F is a final functor.
Русский
Пусть C — кофильтрованная категория и F: C → D — функтор. Предположим, что для каждого объекта d в D существует объект c в C и морфизм F(c) → d, а для любых d и любых стрел s,s' : F(c) → d найдётся c' в C и t: c' → c such that F(t) ∘ s = F(t) ∘ s'. Тогда F является финальным функтором.
LaTeX
$$$\\text{Final}(F) \\quad\\text{при условии } [\\text{IsCofilteredOrEmpty } C]\\text{ и } (\\forall d, \\exists c, F(c) \\to d) \\land (\\forall d,c \\; (s,s' : F(c) \\to d), \\exists c', t: c' \\to c, F(t) \\circ s = F(t) \\circ s')$$$
Lean4
/-- If `C` is cofiltered, then we can give an explicit condition for a functor `F : C ⥤ D` to
be final. The converse is also true, see `initial_iff_of_isCofiltered`. -/
theorem initial_of_exists_of_isCofiltered [IsCofilteredOrEmpty C] (h₁ : ∀ d, ∃ c, Nonempty (F.obj c ⟶ d))
(h₂ : ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s') :
Functor.Initial F :=
by
suffices ∀ d, IsCofiltered (CostructuredArrow F d) from initial_of_isCofiltered_costructuredArrow F
exact isCofiltered_costructuredArrow_of_isCofiltered_of_exists F h₁ h₂
