English
A category C is cofiltered if and only if for every finite diagram J → C there exists an X ∈ C with a nonempty limit of coyoneda(X) composed with F.
Русский
Категория C ко-фильтрована тогда и только если для каждого конечного диаграммного объекта F: J → C существует X∈C такой, что предел coyoneda(X) ∘ F не пуст.
LaTeX
$$$ IsCofiltered\\ C \\iff \\forall {J} [SmallCategory J] [FinCategory J] (F : J \\to C), \\exists X, Nonempty (limit (F \\circ coyoneda.obj(\\mathrm{op} X))) $$$
Lean4
/-- `C` is cofiltered if and only if for every functor `F : J ⥤ C` from a finite category there is
some `X : C` such that `lim Hom(X, F·)` is nonempty. -/
theorem iff_nonempty_limit :
IsCofiltered C ↔
∀ {J : Type v} [SmallCategory J] [FinCategory J] (F : J ⥤ C),
∃ (X : C), Nonempty (limit (F ⋙ coyoneda.obj (op X))) :=
by
rw [IsCofiltered.iff_cone_nonempty.{v}]
refine ⟨fun h J _ _ F => ?_, fun h J _ _ F => ?_⟩
· obtain ⟨c⟩ := h F
exact ⟨c.pt, ⟨(limitCompCoyonedaIsoCone F c.pt).inv c.π⟩⟩
· obtain ⟨pt, ⟨π⟩⟩ := h F
exact ⟨⟨pt, (limitCompCoyonedaIsoCone F pt).hom π⟩⟩
