feat: another characterization of filtered categories in terms of typ…

…e-valued limits (leanprover-community#10665)

Mathlib/CategoryTheory/Filtered/Basic.lean

@@ -52,6 +52,10 @@ categories.
 In `CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit` we show that filtered colimits
 commute with finite limits.
 
+There is another characterization of filtered categories, namely that whenever `F : J ⥤ C` is a
+functor from a finite category, there is `X : C` such that `Nonempty (limit (F.op ⋙ yoneda.obj X))`.
+This is shown in `CategoryTheory.Limits.Filtered`.
+
 -/
 
 

Mathlib/CategoryTheory/Limits/Filtered.lean

@@ -3,13 +3,18 @@ Copyright (c) 2022 Markus Himmel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
-import Mathlib.CategoryTheory.Filtered.Basic
 import Mathlib.CategoryTheory.Limits.HasLimits
+import Mathlib.CategoryTheory.Limits.Types
 
 #align_import category_theory.limits.filtered from "leanprover-community/mathlib"@"e4ee4e30418efcb8cf304ba76ad653aeec04ba6e"
 
 /-!
-# Possession of filtered colimits
+# Filtered categories and limits
+
+In this file , we show that `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.
+
+Furthermore, we define the type classes `HasCofilteredLimitsOfSize` and `HasFilteredColimitsOfSize`.
 -/
 
 
@@ -21,7 +26,41 @@ open CategoryTheory
 
 variable {C : Type u} [Category.{v} C]
 
-namespace CategoryTheory.Limits
+namespace CategoryTheory
+
+section NonemptyLimit
+
+open CategoryTheory.Limits Opposite
+
+/-- `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 IsFiltered.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 ι⟩⟩
+
+/-- `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 IsCofiltered.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 π⟩⟩
+
+end NonemptyLimit
+
+namespace Limits
 
 section
 
@@ -55,4 +94,6 @@ instance (priority := 100) hasColimitsOfShape_of_has_filtered_colimits
   HasFilteredColimitsOfSize.HasColimitsOfShape _
 #align category_theory.limits.has_colimits_of_shape_of_has_filtered_colimits CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits
 
-end CategoryTheory.Limits
+end Limits
+
+end CategoryTheory