feat(CategoryTheory/Limits): preservation of multicoequalizers (#22205)

Author: joelriou

Mathlib.lean

@@ -2137,6 +2137,7 @@ import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
 import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
 import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
 import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
+import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
 import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder
 import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
 import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Mathlib/CategoryTheory/Limits/Preserves/Shapes/Multiequalizer.lean

@@ -0,0 +1,79 @@
+/-
+Copyright (c) 2025 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
+
+/-!
+# Preservation of multicoequalizers
+
+Let `J : MultispanShape` and `d : MultispanIndex J C`.
+If `F : C ⥤ D`, we define `d.map F : MultispanIndex J D` and
+an isomorphism of functors `(d.map F).multispan ≅ d.multispan ⋙ F`
+(see `MultispanIndex.multispanMapIso`).
+If `c : Multicofork d`, we define `c.map F : Multicofork (d.map F)` and
+obtain a bijection `IsColimit (F.mapCocone c) ≃ IsColimit (c.map F)`
+(see `Multicofork.isColimitMapEquiv`). As a result, if `F` preserves
+the colimit of `d.multispan`, we deduce that if `c` is a colimit,
+then `c.map F` also is (see `Multicofork.isColimitMapOfPreserves`).
+
+-/
+
+universe w w' v u
+
+namespace CategoryTheory
+
+variable {C D : Type*} [Category C] [Category D]
+
+namespace Limits
+
+variable {J : MultispanShape.{w, w'}} (d : MultispanIndex J C)
+  (c : Multicofork d) (F : C ⥤ D)
+
+/-- The multispan index obtained by applying a functor. -/
+@[simps]
+def MultispanIndex.map : MultispanIndex J D where
+  left i := F.obj (d.left i)
+  right i := F.obj (d.right i)
+  fst i := F.map (d.fst i)
+  snd i := F.map (d.snd i)
+
+/-- If `d : MultispanIndex J C` and `F : C ⥤ D`, this is the obvious isomorphism
+`(d.map F).multispan ≅ d.multispan ⋙ F`. -/
+@[simps!]
+def MultispanIndex.multispanMapIso : (d.map F).multispan ≅ d.multispan ⋙ F :=
+  NatIso.ofComponents
+    (fun i ↦ match i with
+      | .left _ => Iso.refl _
+      | .right _ => Iso.refl _)
+    (by rintro _ _ (_ | _) <;> simp)
+
+variable {d}
+
+/-- If `d : MultispanIndex J C`, `c : Multicofork d` and `F : C ⥤ D`,
+this is the induced multicofork of `d.map F`. -/
+@[simps!]
+def Multicofork.map : Multicofork (d.map F) :=
+  Multicofork.ofπ _ (F.obj c.pt) (fun i ↦ F.map (c.π i)) (fun j ↦ by
+    dsimp
+    rw [← F.map_comp, ← F.map_comp, condition])
+
+/-- If `d : MultispanIndex J C`, `c : Multicofork d` and `F : C ⥤ D`,
+the cocone `F.mapCocone c` is colimit iff the multicofork `c.map F` is. -/
+def Multicofork.isColimitMapEquiv :
+    IsColimit (F.mapCocone c) ≃ IsColimit (c.map F) :=
+  (IsColimit.precomposeInvEquiv (d.multispanMapIso F).symm (F.mapCocone c)).symm.trans
+    (IsColimit.equivIsoColimit
+      (Multicofork.ext (Iso.refl _) (fun i ↦ by dsimp only [Multicofork.π]; simp)))
+
+/-- If `d : MultispanIndex J C`, `c : Multicofork d` is a colimit multicofork,
+and `F : C ⥤ D` is a functor which preserves the colimit of `d.multispan`,
+then the multicofork `c.map F` is colimit. -/
+noncomputable def Multicofork.isColimitMapOfPreserves
+    [PreservesColimit d.multispan F] (hc : IsColimit c) : IsColimit (c.map F) :=
+  (isColimitMapEquiv c F) (isColimitOfPreserves F hc)
+
+end Limits
+
+end CategoryTheory

Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean

@@ -666,6 +666,14 @@ theorem ofSigmaCofork_ι_app_right' (c : Cofork I.fstSigmaMap I.sndSigmaMap) (b)
     π (ofSigmaCofork I c) b = (Sigma.ι I.right b :) ≫ c.π :=
   rfl
 
+variable {I} in
+/-- Constructor for isomorphisms between multicoforks. -/
+@[simps!]
+def ext {K K' : Multicofork I}
+    (e : K.pt ≅ K'.pt) (h : ∀ (i : J.R), K.π i ≫ e.hom = K'.π i := by aesop_cat) :
+    K ≅ K' :=
+  Cocones.ext e (by rintro (i | j) <;> simp [h])
+
 end Multicofork
 
 namespace MultispanIndex