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