refactor(CategoryTheory/Limits): split MultispanIndex into two structures (#20988)

Before this PR, multiequalizers were defined for a structure `MulticospanIndex C` which contained information about the shape of the diagram, and the diagram itself (objects and maps in a category `C`). In this PR, we introduce the shape `MulticospanShape` which consists of two types and two maps between these types. If `J : MulticospanShape` and `C` is a category, we now have `MultispanIndex J C` which contains the information about the multiequalizer diagram. If `I : MulticospanIndex J C`, we now have a functor `I.multicospan : WalkingMulticospan J ⥤ C`.

This refactor will ease the study of multiequalizers. For example, if `I` and `I'` are two terms in `MulticospanIndex J C`, it makes sense to show that the associated functors `WalkingMulticospan J ⥤ C` are isomorphic, etc.

Author: joelriou

Mathlib/CategoryTheory/GlueData.lean

@@ -122,32 +122,12 @@ def sigmaOpens [HasCoproduct D.U] : C :=
   ∐ D.U
 
 /-- (Implementation) The diagram to take colimit of. -/
-def diagram : MultispanIndex C where
-  L := D.J × D.J
-  R := D.J
-  fstFrom := _root_.Prod.fst
-  sndFrom := _root_.Prod.snd
+def diagram : MultispanIndex (.prod D.J) C where
   left := D.V
   right := D.U
   fst := fun ⟨i, j⟩ => D.f i j
   snd := fun ⟨i, j⟩ => D.t i j ≫ D.f j i
 
-@[simp]
-theorem diagram_l : D.diagram.L = (D.J × D.J) :=
-  rfl
-
-@[simp]
-theorem diagram_r : D.diagram.R = D.J :=
-  rfl
-
-@[simp]
-theorem diagram_fstFrom (i j : D.J) : D.diagram.fstFrom ⟨i, j⟩ = i :=
-  rfl
-
-@[simp]
-theorem diagram_sndFrom (i j : D.J) : D.diagram.sndFrom ⟨i, j⟩ = j :=
-  rfl
-
 @[simp]
 theorem diagram_fst (i j : D.J) : D.diagram.fst ⟨i, j⟩ = D.f i j :=
   rfl

Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean

@@ -249,9 +249,10 @@ section Multiequalizer
 
 variable [HasForget.{max w w' v} C]
 
-theorem multiequalizer_ext {I : MulticospanIndex.{w, w'} C} [HasMultiequalizer I]
+theorem multiequalizer_ext {J : MulticospanShape.{w, w'}}
+    {I : MulticospanIndex J C} [HasMultiequalizer I]
     [PreservesLimit I.multicospan (forget C)] (x y : ↑(multiequalizer I))
-    (h : ∀ t : I.L, Multiequalizer.ι I t x = Multiequalizer.ι I t y) : x = y := by
+    (h : ∀ t : J.L, Multiequalizer.ι I t x = Multiequalizer.ι I t y) : x = y := by
   apply Concrete.limit_ext
   rintro (a | b)
   · apply h
@@ -260,9 +261,9 @@ theorem multiequalizer_ext {I : MulticospanIndex.{w, w'} C} [HasMultiequalizer I
     simp [h]
 
 /-- An auxiliary equivalence to be used in `multiequalizerEquiv` below. -/
-def multiequalizerEquivAux (I : MulticospanIndex.{w, w'} C) :
+def multiequalizerEquivAux {J : MulticospanShape.{w, w'}} (I : MulticospanIndex J C) :
     (I.multicospan ⋙ forget C).sections ≃
-    { x : ∀ i : I.L, I.left i // ∀ i : I.R, I.fst i (x _) = I.snd i (x _) } where
+    { x : ∀ i : J.L, I.left i // ∀ i : J.R, I.fst i (x _) = I.snd i (x _) } where
   toFun x :=
     ⟨fun _ => x.1 (WalkingMulticospan.left _), fun i => by
       have a := x.2 (WalkingMulticospan.Hom.fst i)
@@ -293,19 +294,21 @@ def multiequalizerEquivAux (I : MulticospanIndex.{w, w'} C) :
 
 /-- The equivalence between the noncomputable multiequalizer and
 the concrete multiequalizer. -/
-noncomputable def multiequalizerEquiv (I : MulticospanIndex.{w, w'} C) [HasMultiequalizer I]
+noncomputable def multiequalizerEquiv {J : MulticospanShape.{w, w'}}
+    (I : MulticospanIndex J C) [HasMultiequalizer I]
     [PreservesLimit I.multicospan (forget C)] :
     (multiequalizer I : C) ≃
-      { x : ∀ i : I.L, I.left i // ∀ i : I.R, I.fst i (x _) = I.snd i (x _) } :=
+      { x : ∀ i : J.L, I.left i // ∀ i : J.R, I.fst i (x _) = I.snd i (x _) } :=
   letI h1 := limit.isLimit I.multicospan
   letI h2 := isLimitOfPreserves (forget C) h1
   letI E := h2.conePointUniqueUpToIso (Types.limitConeIsLimit.{max w w', v} _)
   Equiv.trans E.toEquiv (Concrete.multiequalizerEquivAux I)
 
 @[simp]
-theorem multiequalizerEquiv_apply (I : MulticospanIndex.{w, w'} C) [HasMultiequalizer I]
-    [PreservesLimit I.multicospan (forget C)] (x : ↑(multiequalizer I)) (i : I.L) :
-    ((Concrete.multiequalizerEquiv I) x : ∀ i : I.L, I.left i) i = Multiequalizer.ι I i x :=
+theorem multiequalizerEquiv_apply {J : MulticospanShape.{w, w'}}
+    (I : MulticospanIndex J C) [HasMultiequalizer I]
+    [PreservesLimit I.multicospan (forget C)] (x : ↑(multiequalizer I)) (i : J.L) :
+    ((Concrete.multiequalizerEquiv I) x : ∀ i : J.L, I.left i) i = Multiequalizer.ι I i x :=
   rfl
 
 end Multiequalizer

Mathlib/CategoryTheory/Limits/Shapes/End.lean

@@ -32,14 +32,19 @@ namespace Limits
 variable {J : Type u} [Category.{v} J] {C : Type u'} [Category.{v'} C]
   (F : Jᵒᵖ ⥤ J ⥤ C)
 
-/-- Given `F : Jᵒᵖ ⥤ J ⥤ C`, this is the multicospan index which shall be used
-to define the end of `F`. -/
+variable (J) in
+/-- The shape of multiequalizer diagrams involved in the definition of ends. -/
 @[simps]
-def multicospanIndexEnd : MulticospanIndex C where
+def multicospanShapeEnd : MulticospanShape where
   L := J
   R := Arrow J
-  fstTo f := f.left
-  sndTo f := f.right
+  fst f := f.left
+  snd f := f.right
+
+/-- Given `F : Jᵒᵖ ⥤ J ⥤ C`, this is the multicospan index which shall be used
+to define the end of `F`. -/
+@[simps]
+def multicospanIndexEnd : MulticospanIndex (multicospanShapeEnd J) C where
   left j := (F.obj (op j)).obj j
   right f := (F.obj (op f.left)).obj f.right
   fst f := (F.obj (op f.left)).map f.hom