feat: final functors with filtered domain (#10720)

Mathlib.lean

@@ -1070,6 +1070,7 @@ import Mathlib.CategoryTheory.EssentiallySmall
 import Mathlib.CategoryTheory.Extensive
 import Mathlib.CategoryTheory.Filtered.Basic
 import Mathlib.CategoryTheory.Filtered.Connected
+import Mathlib.CategoryTheory.Filtered.Final
 import Mathlib.CategoryTheory.Filtered.Small
 import Mathlib.CategoryTheory.FinCategory
 import Mathlib.CategoryTheory.FintypeCat

Mathlib/CategoryTheory/Filtered/Final.lean

@@ -0,0 +1,167 @@
+/-
+Copyright (c) 2024 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import Mathlib.CategoryTheory.Filtered.Connected
+import Mathlib.CategoryTheory.Limits.Final
+
+/-!
+# Final functors with filtered domain
+
+If `C` is a filtered category, then the usual equivalent conditions for a functor `F : C ⥤ D` to be
+final can be restated. We show:
+
+* `final_iff_of_isFiltered`: a concrete description of finality which is sometimes a convenient way
+  to show that a functor is final.
+* `final_iff_isFiltered_structuredArrow`: `F` is final if and only if `StructuredArrow d F` is
+  filtered for all `d : D`, which strengthens the usual statement that `F` is final if and only
+  if `StructuredArrow d F` is connected for all `d : D`.
+
+## References
+
+* [M. Kashiwara, P. Schapira, *Categories and Sheaves*][Kashiwara2006], Lemma 3.2.2
+
+-/
+
+universe v₁ v₂ u₁ u₂
+
+namespace CategoryTheory
+
+open CategoryTheory.Limits CategoryTheory.Functor Opposite
+
+section ArbitraryUniverses
+
+variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] (F : C ⥤ D)
+
+/-- If `StructuredArrow d F` is filtered for any `d : D`, then `F : C ⥤ D` is final. This is
+    simply because filtered categories are connected. More profoundly, the converse is also true if
+    `C` is filtered, see `final_iff_isFiltered_structuredArrow`. -/
+theorem Functor.final_of_isFiltered_structuredArrow [∀ d, IsFiltered (StructuredArrow d F)] :
+    Final F where
+  out _ := IsFiltered.isConnected _
+
+/-- If `CostructuredArrow F d` is filtered for any `d : D`, then `F : C ⥤ D` is initial. This is
+    simply because cofiltered categories are connectged. More profoundly, the converse is also true
+    if `C` is cofiltered, see `initial_iff_isCofiltered_costructuredArrow`. -/
+theorem Functor.initial_of_isCofiltered_costructuredArrow
+    [∀ d, IsCofiltered (CostructuredArrow F d)] : Initial F where
+  out _ := IsCofiltered.isConnected _
+
+theorem isFiltered_structuredArrow_of_isFiltered_of_exists [IsFilteredOrEmpty C]
+    (h₁ : ∀ d, ∃ c, Nonempty (d ⟶ F.obj c)) (h₂ : ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c),
+      ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t) (d : D) :
+    IsFiltered (StructuredArrow d F) := by
+  have : Nonempty (StructuredArrow d F) := by
+    obtain ⟨c, ⟨f⟩⟩ := h₁ d
+    exact ⟨.mk f⟩
+  suffices IsFilteredOrEmpty (StructuredArrow d F) from IsFiltered.mk
+  refine ⟨fun f g => ?_, fun f g η μ => ?_⟩
+  · obtain ⟨c, ⟨t, ht⟩⟩ := h₂ (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right))
+        (g.hom ≫ F.map (IsFiltered.rightToMax f.right g.right))
+    refine ⟨.mk (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right ≫ t)), ?_, ?_, trivial⟩
+    · exact StructuredArrow.homMk (IsFiltered.leftToMax _ _ ≫ t) rfl
+    · exact StructuredArrow.homMk (IsFiltered.rightToMax _ _ ≫ t) (by simpa using ht.symm)
+  · refine ⟨.mk (f.hom ≫ F.map (η.right ≫ IsFiltered.coeqHom η.right μ.right)),
+      StructuredArrow.homMk (IsFiltered.coeqHom η.right μ.right) (by simp), ?_⟩
+    simpa using IsFiltered.coeq_condition _ _
+
+theorem isCofiltered_costructuredArrow_of_isCofiltered_of_exists [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') (d : D) :
+    IsCofiltered (CostructuredArrow F d) := by
+  suffices IsFiltered (CostructuredArrow F d)ᵒᵖ from isCofiltered_of_isFiltered_op _
+  suffices IsFiltered (StructuredArrow (op d) F.op) from
+    IsFiltered.of_equivalence (costructuredArrowOpEquivalence _ _).symm
+  apply isFiltered_structuredArrow_of_isFiltered_of_exists
+  · intro d
+    obtain ⟨c, ⟨t⟩⟩ := h₁ d.unop
+    exact ⟨op c, ⟨Quiver.Hom.op t⟩⟩
+  · intro d c s s'
+    obtain ⟨c', t, ht⟩ := h₂ s.unop s'.unop
+    exact ⟨op c', Quiver.Hom.op t, Quiver.Hom.unop_inj ht⟩
+
+/-- If `C` is filtered, then we can give an explicit condition for a functor `F : C ⥤ D` to
+    be final. The converse is also true, see `final_iff_of_isFiltered`. -/
+theorem Functor.final_of_exists_of_isFiltered [IsFilteredOrEmpty C]
+    (h₁ : ∀ d, ∃ c, Nonempty (d ⟶ F.obj c)) (h₂ : ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c),
+      ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t) : Functor.Final F := by
+  suffices ∀ d, IsFiltered (StructuredArrow d F) from final_of_isFiltered_structuredArrow F
+  exact isFiltered_structuredArrow_of_isFiltered_of_exists F h₁ h₂
+
+/-- 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 Functor.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₂
+
+end ArbitraryUniverses
+
+section LocallySmall
+
+variable {C : Type v₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₁} D] (F : C ⥤ D)
+
+/-- If `C` is filtered, then we can give an explicit condition for a functor `F : C ⥤ D` to
+    be final. -/
+theorem Functor.final_iff_of_isFiltered [IsFilteredOrEmpty C] :
+    Final F ↔ (∀ d, ∃ c, Nonempty (d ⟶ F.obj c)) ∧ (∀ {d : D} {c : C} (s s' : d ⟶ F.obj c),
+      ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t) := by
+  refine ⟨fun hF => ⟨?_, ?_⟩, fun h => final_of_exists_of_isFiltered F h.1 h.2⟩
+  · intro d
+    obtain ⟨f⟩ : Nonempty (StructuredArrow d F) := IsConnected.is_nonempty
+    exact ⟨_, ⟨f.hom⟩⟩
+  · intro d c s s'
+    have : colimit.ι (F ⋙ coyoneda.obj (op d)) c s = colimit.ι (F ⋙ coyoneda.obj (op d)) c s' := by
+      apply (Final.colimitCompCoyonedaIso F d).toEquiv.injective
+      exact Subsingleton.elim _ _
+    obtain ⟨c', t₁, t₂, h⟩ := (Types.FilteredColimit.colimit_eq_iff.{v₁, v₁, v₁} _).mp this
+    refine ⟨IsFiltered.coeq t₁ t₂, t₁ ≫ IsFiltered.coeqHom t₁ t₂, ?_⟩
+    conv_rhs => rw [IsFiltered.coeq_condition t₁ t₂]
+    dsimp only [comp_obj, coyoneda_obj_obj, unop_op, Functor.comp_map, coyoneda_obj_map] at h
+    simp [reassoc_of% h]
+
+/-- If `C` is cofiltered, then we can give an explicit condition for a functor `F : C ⥤ D` to
+    be initial. -/
+theorem Functor.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⟩
+
+theorem Functor.Final.exists_coeq [IsFilteredOrEmpty C] [Final F] {d : D} {c : C}
+    (s s' : d ⟶ F.obj c) : ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t :=
+  ((final_iff_of_isFiltered F).1 inferInstance).2 s s'
+
+theorem Functor.Initial.exists_eq [IsCofilteredOrEmpty C] [Initial F] {d : D} {c : C}
+    (s s' : F.obj c ⟶ d) : ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s' :=
+  ((initial_iff_of_isCofiltered F).1 inferInstance).2 s s'
+
+/-- If `C` is filtered, then `F : C ⥤ D` is final if and only if `StructuredArrow d F` is filtered
+    for all `d : D`. -/
+theorem Functor.final_iff_isFiltered_structuredArrow [IsFilteredOrEmpty C] :
+    Final F ↔ ∀ d, IsFiltered (StructuredArrow d F) := by
+  refine ⟨?_, fun h => final_of_isFiltered_structuredArrow F⟩
+  rw [final_iff_of_isFiltered]
+  exact fun h => isFiltered_structuredArrow_of_isFiltered_of_exists F h.1 h.2
+
+/-- If `C` is cofiltered, then `F : C ⥤ D` is initial if and only if `CostructuredArrow F d` is
+    cofiltered for all `d : D`. -/
+theorem Functor.initial_iff_isCofiltered_costructuredArrow [IsCofilteredOrEmpty C] :
+    Initial F ↔ ∀ d, IsCofiltered (CostructuredArrow F d) := by
+  refine ⟨?_, fun h => initial_of_isCofiltered_costructuredArrow F⟩
+  rw [initial_iff_of_isCofiltered]
+  exact fun h => isCofiltered_costructuredArrow_of_isCofiltered_of_exists F h.1 h.2
+
+end LocallySmall
+
+end CategoryTheory

Mathlib/CategoryTheory/Limits/Final.lean

@@ -48,6 +48,10 @@ There is some discrepancy in the literature about naming; some say 'cofinal' ins
 The explanation for this is that the 'co' prefix here is *not* the usual category-theoretic one
 indicating duality, but rather indicating the sense of "along with".
 
+## See also
+In `CategoryTheory.Filtered.Final` we give additional equivalent conditions in the case that
+`C` is filtered.
+
 ## Future work
 Dualise condition 3 above and the implications 2 ⇒ 3 and 3 ⇒ 1 to initial functors.
 
@@ -445,12 +449,6 @@ theorem cofinal_of_isTerminal_colimit_comp_yoneda
   let b := IsTerminal.isTerminalObj ((evaluation _ _).obj (Opposite.op d)) _ h
   exact b.ofIso <| preservesColimitIso ((evaluation _ _).obj (Opposite.op d)) (F ⋙ yoneda)
 
-end LocallySmall
-
-section SmallCategory
-
-variable {C : Type v} [Category.{v} C] {D : Type v} [Category.{v} D] (F : C ⥤ D)
-
 /-- If the universal morphism `colimit (F ⋙ coyoneda.obj (op d)) ⟶ colimit (coyoneda.obj (op d))`
 is an isomorphism (as it always is when `F` is cofinal),
 then `colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit`
@@ -461,6 +459,12 @@ def Final.colimitCompCoyonedaIso (d : D) [IsIso (colimit.pre (coyoneda.obj (op d
   asIso (colimit.pre (coyoneda.obj (op d)) F) ≪≫ Coyoneda.colimitCoyonedaIso (op d)
 #align category_theory.functor.final.colimit_comp_coyoneda_iso CategoryTheory.Functor.Final.colimitCompCoyonedaIso
 
+end LocallySmall
+
+section SmallCategory
+
+variable {C : Type v} [Category.{v} C] {D : Type v} [Category.{v} D] (F : C ⥤ D)
+
 theorem final_iff_isIso_colimit_pre : Final F ↔ ∀ G : D ⥤ Type v, IsIso (colimit.pre G F) :=
   ⟨fun _ => inferInstance,
    fun _ => cofinal_of_colimit_comp_coyoneda_iso_pUnit _ fun _ => Final.colimitCompCoyonedaIso _ _⟩

Mathlib/CategoryTheory/Limits/Yoneda.lean

@@ -25,7 +25,7 @@ namespace CategoryTheory
 
 namespace Coyoneda
 
-variable {C : Type v} [SmallCategory C]
+variable {C : Type u} [Category.{v} C]
 
 /-- The colimit cocone over `coyoneda.obj X`, with cocone point `PUnit`.
 -/