English
If C is filtered-or-empty, then Final F is equivalent to a conjunction of two conditions: (i) for every d there exists c with a morphism d → F.obj c, and (ii) for all arrows s,s' : d → F.obj c there exists c' and t : c ⟶ c' with s ≫ F.map t = s' ≫ F.map t.
Русский
Если C фильтрована-или-пустая, тогда финальность F эквивалентна сочетанию условий: (i) для каждого d существует c с морфизм d → F(c); (ii) для любых стрел s,s' : d → F(c) существует c' и t : c ⟶ c' с s ≫ F(t) = s' ≫ F(t).
LaTeX
$$$\\text{Final}(F) \\iff \\bigl( \\forall d, \\exists c,\\nearrow d \\to F(obj\,c) \\bigr) \\land \\bigl( \\forall {d,c} (s,s') : d \\to F.obj c,\\ \\exists (c' : C)(t : c ⟶ c'),\\ s \\circ F.map t = s' \\circ F.map t \\bigr)$$$
Lean4
/-- If `C` is cofiltered, then we can give an explicit condition for a functor `F : C ⥤ D` to
be initial. -/
theorem initial_iff_of_isCofiltered [IsCofilteredOrEmpty C] :
Initial F ↔
(∀ d, ∃ c, Nonempty (F.obj c ⟶ d)) ∧
(∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s') :=
by
refine ⟨fun hF => ?_, fun h => initial_of_exists_of_isCofiltered F h.1 h.2⟩
obtain ⟨h₁, h₂⟩ := F.op.final_iff_of_isFiltered.mp inferInstance
refine ⟨?_, ?_⟩
· intro d
obtain ⟨c, ⟨t⟩⟩ := h₁ (op d)
exact ⟨c.unop, ⟨t.unop⟩⟩
· intro d c s s'
obtain ⟨c', t, ht⟩ := h₂ (Quiver.Hom.op s) (Quiver.Hom.op s')
exact ⟨c'.unop, t.unop, Quiver.Hom.op_inj ht⟩
