feat: equalizers and coequalizers in the category of ind-objects (#21139)

We study parallel pairs of morphisms in `Ind C`, discover that they are always induced by natural transformations in a suitable indexing category, and deduce that ind-objects are closed under equalizers and the category of ind-objects has coequalizers.

Huge thanks to @javra and @datokrat. If they had not spent countless hours tirelessly PRing properties of comma categories and the Grothendieck construction to mathlib this PR would not have been possible, even though you can't see any of their results used in the PR (since they are applied by instance synthesis).



Co-authored-by: Markus Himmel <markus@lean-fro.org>

Author: TwoFX

Mathlib.lean

@@ -1932,6 +1932,7 @@ import Mathlib.CategoryTheory.Limits.Indization.Equalizers
 import Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
 import Mathlib.CategoryTheory.Limits.Indization.IndObject
 import Mathlib.CategoryTheory.Limits.Indization.LocallySmall
+import Mathlib.CategoryTheory.Limits.Indization.ParallelPair
 import Mathlib.CategoryTheory.Limits.Indization.Products
 import Mathlib.CategoryTheory.Limits.IsConnected
 import Mathlib.CategoryTheory.Limits.IsLimit

Mathlib/CategoryTheory/Limits/Indization/Category.lean

@@ -7,6 +7,7 @@ import Mathlib.CategoryTheory.Functor.Flat
 import Mathlib.CategoryTheory.Limits.Constructions.Filtered
 import Mathlib.CategoryTheory.Limits.FullSubcategory
 import Mathlib.CategoryTheory.Limits.Indization.LocallySmall
+import Mathlib.CategoryTheory.Limits.Indization.ParallelPair
 import Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
 import Mathlib.CategoryTheory.Limits.Indization.Products
 
@@ -30,7 +31,8 @@ Adopting the theorem numbering of [Kashiwara2006], we show that
 * if `C` has finite coproducts, then `Ind C` has small coproducts (6.1.18(ii)),
 * if `C` has products indexed by `α`, then `Ind C` has products indexed by `α`, and the functor
   `Ind C ⥤ Cᵒᵖ ⥤ Type v` creates such products (6.1.17)
-* the functor `C ⥤ Ind C` preserves small limits.
+* the functor `C ⥤ Ind C` preserves small limits,
+* if `C` has coequalizers, then `Ind C` has coequalizers (6.1.18(i)).
 
 More limit-colimit properties will follow.
 
@@ -43,7 +45,7 @@ Note that:
 * [M. Kashiwara, P. Schapira, *Categories and Sheaves*][Kashiwara2006], Chapter 6
 -/
 
-universe v u
+universe w v u
 
 namespace CategoryTheory
 
@@ -180,14 +182,14 @@ noncomputable def Ind.limCompInclusion {I : Type v} [SmallCategory I] [IsFiltere
   _ ≅ (whiskeringRight _ _ _).obj yoneda ⋙ colim :=
     isoWhiskerRight ((whiskeringRight _ _ _).mapIso (Ind.yonedaCompInclusion)) colim
 
-instance {α : Type v} [SmallCategory α] [FinCategory α] [HasLimitsOfShape α C] {I : Type v}
+instance {α : Type w} [SmallCategory α] [FinCategory α] [HasLimitsOfShape α C] {I : Type v}
     [SmallCategory I] [IsFiltered I] :
     PreservesLimitsOfShape α (Ind.lim I : (I ⥤ C) ⥤ _) :=
   haveI : PreservesLimitsOfShape α (Ind.lim I ⋙ Ind.inclusion C) :=
     preservesLimitsOfShape_of_natIso Ind.limCompInclusion.symm
   preservesLimitsOfShape_of_reflects_of_preserves _ (Ind.inclusion C)
 
-instance {α : Type v} [SmallCategory α] [FinCategory α] [HasColimitsOfShape α C] {I : Type v}
+instance {α : Type w} [SmallCategory α] [FinCategory α] [HasColimitsOfShape α C] {I : Type v}
     [SmallCategory I] [IsFiltered I] :
     PreservesColimitsOfShape α (Ind.lim I : (I ⥤ C) ⥤ _) :=
   inferInstanceAs (PreservesColimitsOfShape α (_ ⋙ colim))
@@ -209,11 +211,43 @@ instance {α : Type v} [Finite α] [HasColimitsOfShape (Discrete α) C] :
   -- ```
   -- from the fact that finite limits commute with filtered colimits and from the fact that
   -- `Ind.yoneda` preserves finite colimits.
-  apply hasColimitOfIso iso.symm
+  exact hasColimitOfIso iso.symm
 
 instance [HasFiniteCoproducts C] : HasCoproducts.{v} (Ind C) :=
   have : HasFiniteCoproducts (Ind C) :=
     ⟨fun _ => hasColimitsOfShape_of_equivalence (Discrete.equivalence Equiv.ulift)⟩
   hasCoproducts_of_finite_and_filtered
 
+/-- Given an `IndParallelPairPresentation f g`, we can understand the parallel pair `(f, g)` as
+the colimit of `(P.φ, P.ψ)` in `Ind C`. -/
+noncomputable def IndParallelPairPresentation.parallelPairIsoParallelPairCompIndYoneda
+    {A B : Ind C} {f g : A ⟶ B}
+    (P : IndParallelPairPresentation ((Ind.inclusion _).map f) ((Ind.inclusion _).map g)) :
+    parallelPair f g ≅ parallelPair P.φ P.ψ ⋙ Ind.lim P.I :=
+  ((whiskeringRight WalkingParallelPair _ _).obj (Ind.inclusion C)).preimageIso <|
+    diagramIsoParallelPair _ ≪≫
+      P.parallelPairIsoParallelPairCompYoneda ≪≫
+      isoWhiskerLeft (parallelPair _ _) Ind.limCompInclusion.symm
+
+instance [HasColimitsOfShape WalkingParallelPair C] :
+    HasColimitsOfShape WalkingParallelPair (Ind C) := by
+  refine ⟨fun F => ?_⟩
+  obtain ⟨P⟩ := nonempty_indParallelPairPresentation (F.obj WalkingParallelPair.zero).2
+    (F.obj WalkingParallelPair.one).2 (Ind.inclusion _ |>.map <| F.map WalkingParallelPairHom.left)
+    (Ind.inclusion _ |>.map <| F.map WalkingParallelPairHom.right)
+  exact hasColimitOfIso (diagramIsoParallelPair _ ≪≫ P.parallelPairIsoParallelPairCompIndYoneda)
+
+/-- A way to understand morphisms in `Ind C`: every morphism is induced by a natural transformation
+of diagrams. -/
+theorem Ind.exists_nonempty_arrow_mk_iso_ind_lim {A B : Ind C} {f : A ⟶ B} :
+    ∃ (I : Type v) (_ : SmallCategory I) (_ : IsFiltered I) (F G : I ⥤ C) (φ : F ⟶ G),
+      Nonempty (Arrow.mk f ≅ Arrow.mk ((Ind.lim _).map φ)) := by
+  obtain ⟨P⟩ := nonempty_indParallelPairPresentation A.2 B.2
+    (Ind.inclusion _ |>.map f) (Ind.inclusion _ |>.map f)
+  refine ⟨P.I, inferInstance, inferInstance, P.F₁, P.F₂, P.φ, ⟨Arrow.isoMk ?_ ?_ ?_⟩⟩
+  · exact P.parallelPairIsoParallelPairCompIndYoneda.app WalkingParallelPair.zero
+  · exact P.parallelPairIsoParallelPairCompIndYoneda.app WalkingParallelPair.one
+  · simpa using
+      (P.parallelPairIsoParallelPairCompIndYoneda.hom.naturality WalkingParallelPairHom.left).symm
+
 end CategoryTheory

Mathlib/CategoryTheory/Limits/Indization/Equalizers.lean

@@ -4,16 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
 import Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
+import Mathlib.CategoryTheory.Limits.FullSubcategory
+import Mathlib.CategoryTheory.Limits.Indization.ParallelPair
 
 /-!
 # Equalizers of ind-objects
 
-The eventual goal of this file is to show that if a category `C` has equalizers, then ind-objects
-are closed under equalizers. For now, it contains one of the main prerequisites, namely we show
-that under sufficient conditions the limit of a diagram in `I ⥤ C` taken in `Cᵒᵖ ⥤ Type v` is an
-ind-object.
+We show that if a category `C` has equalizers, then ind-objects are closed under equalizers.
 
-## References
+# References
 * [M. Kashiwara, P. Schapira, *Categories and Sheaves*][Kashiwara2006], Section 6.1
 -/
 
@@ -60,4 +59,21 @@ theorem isIndObject_limit_comp_yoneda_comp_colim
 
 end
 
+/-- If `C` has equalizers. then ind-objects are closed under equalizers.
+
+This is Proposition 6.1.17(i) in [Kashiwara2006].
+-/
+theorem closedUnderLimitsOfShape_walkingParallelPair_isIndObject [HasEqualizers C] :
+    ClosedUnderLimitsOfShape WalkingParallelPair (IsIndObject (C := C)) := by
+  apply closedUnderLimitsOfShape_of_limit
+  intro F hF h
+  obtain ⟨P⟩ := nonempty_indParallelPairPresentation (h WalkingParallelPair.zero)
+    (h WalkingParallelPair.one) (F.map WalkingParallelPairHom.left)
+    (F.map WalkingParallelPairHom.right)
+  exact IsIndObject.map
+    (HasLimit.isoOfNatIso (P.parallelPairIsoParallelPairCompYoneda.symm ≪≫
+      (diagramIsoParallelPair _).symm)).hom
+    (isIndObject_limit_comp_yoneda_comp_colim (parallelPair P.φ P.ψ)
+      (fun i => isIndObject_limit_comp_yoneda _))
+
 end CategoryTheory.Limits

Mathlib/CategoryTheory/Limits/Indization/ParallelPair.lean

@@ -0,0 +1,171 @@
+/-
+Copyright (c) 2025 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import Mathlib.CategoryTheory.Comma.Final
+import Mathlib.CategoryTheory.Limits.Indization.IndObject
+
+/-!
+# Parallel pairs of natural transformations between ind-objects
+
+We show that if `A` and `B` are ind-objects and `f` and `g` are natural transformations between
+`A` and `B`, then there is a small filtered category `I` such that `A`, `B`, `f` and `g` are
+commonly presented by diagrams and natural transformations in `I ⥤ C`.
+
+
+## References
+* [M. Kashiwara, P. Schapira, *Categories and Sheaves*][Kashiwara2006], Proposition 6.1.15 (though
+  our proof is more direct).
+-/
+
+universe v₁ v₂ v₃ u₁ u₂ u₃
+
+namespace CategoryTheory
+
+open Limits
+
+variable {C : Type u₁} [Category.{v₁} C]
+
+/-- Structure containing data exhibiting two parallel natural transformations `f` and `g` between
+presheaves `A` and `B` as induced by a natural transformation in a functor category exhibiting
+`A` and `B` as ind-objects. -/
+structure IndParallelPairPresentation {A B : Cᵒᵖ ⥤ Type v₁} (f g : A ⟶ B) where
+  /-- The indexing category. -/
+  I : Type v₁
+  /-- Category instance on the indexing category. -/
+  [ℐ : SmallCategory I]
+  [hI : IsFiltered I]
+  /-- The diagram presenting `A`. -/
+  F₁ : I ⥤ C
+  /-- The diagram presenting `B`. -/
+  F₂ : I ⥤ C
+  /-- The cocone on `F₁` with apex `A`. -/
+  ι₁ : F₁ ⋙ yoneda ⟶ (Functor.const I).obj A
+  /-- The cocone on `F₁` with apex `A` is a colimit cocone. -/
+  isColimit₁ : IsColimit (Cocone.mk A ι₁)
+  /-- The cocone on `F₂` with apex `B`. -/
+  ι₂ : F₂ ⋙ yoneda ⟶ (Functor.const I).obj B
+  /-- The cocone on `F₂` with apex `B` is a colimit cocone. -/
+  isColimit₂ : IsColimit (Cocone.mk B ι₂)
+  /-- The natural transformation presenting `f`. -/
+  φ : F₁ ⟶ F₂
+  /-- The natural transformation presenting `g`. -/
+  ψ : F₁ ⟶ F₂
+  /-- `f` is in fact presented by `φ`. -/
+  hf : f = IsColimit.map isColimit₁ (Cocone.mk B ι₂) (whiskerRight φ yoneda)
+  /-- `g` is in fact presented by `ψ`. -/
+  hg : g = IsColimit.map isColimit₁ (Cocone.mk B ι₂) (whiskerRight ψ yoneda)
+
+instance {A B : Cᵒᵖ ⥤ Type v₁} {f g : A ⟶ B} (P : IndParallelPairPresentation f g) :
+    SmallCategory P.I := P.ℐ
+instance {A B : Cᵒᵖ ⥤ Type v₁} {f g : A ⟶ B} (P : IndParallelPairPresentation f g) :
+    IsFiltered P.I := P.hI
+
+namespace NonemptyParallelPairPresentationAux
+
+variable {A B : Cᵒᵖ ⥤ Type v₁} (f g : A ⟶ B) (P₁ : IndObjectPresentation A)
+  (P₂ : IndObjectPresentation B)
+
+/-- Implementation; see `nonempty_indParallelPairPresentation`. -/
+abbrev K : Type v₁ :=
+  Comma ((P₁.toCostructuredArrow ⋙ CostructuredArrow.map f).prod'
+    (P₁.toCostructuredArrow ⋙ CostructuredArrow.map g))
+    (P₂.toCostructuredArrow.prod' P₂.toCostructuredArrow)
+
+/-- Implementation; see `nonempty_indParallelPairPresentation`. -/
+abbrev F₁ : K f g P₁ P₂ ⥤ C := Comma.fst _ _ ⋙ P₁.F
+/-- Implementation; see `nonempty_indParallelPairPresentation`. -/
+abbrev F₂ : K f g P₁ P₂ ⥤ C := Comma.snd _ _ ⋙ P₂.F
+
+/-- Implementation; see `nonempty_indParallelPairPresentation`. -/
+abbrev ι₁ : F₁ f g P₁ P₂ ⋙ yoneda ⟶ (Functor.const (K f g P₁ P₂)).obj A :=
+  whiskerLeft (Comma.fst _ _) P₁.ι
+
+/-- Implementation; see `nonempty_indParallelPairPresentation`. -/
+noncomputable abbrev isColimit₁ : IsColimit (Cocone.mk A (ι₁ f g P₁ P₂)) :=
+  (Functor.Final.isColimitWhiskerEquiv _ _).symm P₁.isColimit
+
+/-- Implementation; see `nonempty_indParallelPairPresentation`. -/
+abbrev ι₂ : F₂ f g P₁ P₂ ⋙ yoneda ⟶ (Functor.const (K f g P₁ P₂)).obj B :=
+  whiskerLeft (Comma.snd _ _) P₂.ι
+
+/-- Implementation; see `nonempty_indParallelPairPresentation`. -/
+noncomputable abbrev isColimit₂ : IsColimit (Cocone.mk B (ι₂ f g P₁ P₂)) :=
+  (Functor.Final.isColimitWhiskerEquiv _ _).symm P₂.isColimit
+
+/-- Implementation; see `nonempty_indParallelPairPresentation`. -/
+def ϕ : F₁ f g P₁ P₂ ⟶ F₂ f g P₁ P₂ where
+  app h := h.hom.1.left
+  naturality _ _ h := by
+    have := h.w
+    simp only [Functor.prod'_obj, Functor.comp_obj, prod_Hom, Functor.prod'_map, Functor.comp_map,
+      prod_comp, Prod.mk.injEq, CostructuredArrow.hom_eq_iff, CostructuredArrow.map_obj_left,
+      IndObjectPresentation.toCostructuredArrow_obj_left, CostructuredArrow.comp_left,
+      CostructuredArrow.map_map_left, IndObjectPresentation.toCostructuredArrow_map_left] at this
+    exact this.1
+
+theorem hf : f = IsColimit.map (isColimit₁ f g P₁ P₂)
+    (Cocone.mk B (ι₂ f g P₁ P₂)) (whiskerRight (ϕ f g P₁ P₂) yoneda) := by
+  refine (isColimit₁ f g P₁ P₂).hom_ext (fun i => ?_)
+  rw [IsColimit.ι_map]
+  simpa using i.hom.1.w.symm
+
+/-- Implementation; see `nonempty_indParallelPairPresentation`. -/
+def ψ : F₁ f g P₁ P₂ ⟶ F₂ f g P₁ P₂ where
+  app h := h.hom.2.left
+  naturality _ _ h := by
+    have := h.w
+    simp only [Functor.prod'_obj, Functor.comp_obj, prod_Hom, Functor.prod'_map, Functor.comp_map,
+      prod_comp, Prod.mk.injEq, CostructuredArrow.hom_eq_iff, CostructuredArrow.map_obj_left,
+      IndObjectPresentation.toCostructuredArrow_obj_left, CostructuredArrow.comp_left,
+      CostructuredArrow.map_map_left, IndObjectPresentation.toCostructuredArrow_map_left] at this
+    exact this.2
+
+theorem hg : g = IsColimit.map (isColimit₁ f g P₁ P₂)
+    (Cocone.mk B (ι₂ f g P₁ P₂)) (whiskerRight (ψ f g P₁ P₂) yoneda) := by
+  refine (isColimit₁ f g P₁ P₂).hom_ext (fun i => ?_)
+  rw [IsColimit.ι_map]
+  simpa using i.hom.2.w.symm
+
+attribute [local instance] Comma.isFiltered_of_final in
+/-- Implementation; see `nonempty_indParallelPairPresentation`. -/
+noncomputable def presentation : IndParallelPairPresentation f g where
+  I := K f g P₁ P₂
+  F₁ := F₁ f g P₁ P₂
+  F₂ := F₂ f g P₁ P₂
+  ι₁ := ι₁ f g P₁ P₂
+  isColimit₁ := isColimit₁ f g P₁ P₂
+  ι₂ := ι₂ f g P₁ P₂
+  isColimit₂ := isColimit₂ f g P₁ P₂
+  φ := ϕ f g P₁ P₂
+  ψ := ψ f g P₁ P₂
+  hf := hf f g P₁ P₂
+  hg := hg f g P₁ P₂
+
+end NonemptyParallelPairPresentationAux
+
+theorem nonempty_indParallelPairPresentation {A B : Cᵒᵖ ⥤ Type v₁} (hA : IsIndObject A)
+    (hB : IsIndObject B) (f g : A ⟶ B) : Nonempty (IndParallelPairPresentation f g) :=
+  ⟨NonemptyParallelPairPresentationAux.presentation f g hA.presentation hB.presentation⟩
+
+namespace IndParallelPairPresentation
+
+/-- Given an `IndParallelPairPresentation f g`, we can understand the parallel pair `(f, g)`
+as the colimit of `(P.φ, P.ψ)` in `Cᵒᵖ ⥤ Type v`. -/
+noncomputable def parallelPairIsoParallelPairCompYoneda {A B : Cᵒᵖ ⥤ Type v₁} {f g : A ⟶ B}
+    (P : IndParallelPairPresentation f g) :
+    parallelPair f g ≅ parallelPair P.φ P.ψ ⋙ (whiskeringRight _ _ _).obj yoneda ⋙ colim :=
+  parallelPair.ext
+    (P.isColimit₁.coconePointUniqueUpToIso (colimit.isColimit _))
+    (P.isColimit₂.coconePointUniqueUpToIso (colimit.isColimit _))
+    (P.isColimit₁.hom_ext (fun j => by
+      simp [P.hf, P.isColimit₁.ι_map_assoc, P.isColimit₁.comp_coconePointUniqueUpToIso_hom_assoc,
+        P.isColimit₂.comp_coconePointUniqueUpToIso_hom]))
+    (P.isColimit₁.hom_ext (fun j => by
+      simp [P.hg, P.isColimit₁.ι_map_assoc, P.isColimit₁.comp_coconePointUniqueUpToIso_hom_assoc,
+        P.isColimit₂.comp_coconePointUniqueUpToIso_hom]))
+
+end IndParallelPairPresentation
+
+end CategoryTheory