feat(CategoryTheory): combine pullback cones in the functor category (#32618)

Author: dagurtomas

Mathlib/CategoryTheory/Limits/FunctorCategory/Shapes/Pullbacks.lean

@@ -25,6 +25,35 @@ variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
 
 section Pullback
 
+/-- Given functors `F G H` and natural transformations `f : F ⟶ H` and `g : g : G ⟶ H`, together
+with a collection of limiting pullback cones for each cospan `F X ⟶ H X, G X ⟶ H X`, we can stich
+them together to give a pullback cone for the cospan formed by `f` and `g`.
+`combinePullbackConesIsLimit` shows that this pullback cone is limiting. -/
+@[simps!]
+def PullbackCone.combine (f : F ⟶ H) (g : G ⟶ H) (c : ∀ X, PullbackCone (f.app X) (g.app X))
+    (hc : ∀ X, IsLimit (c X)) : PullbackCone f g :=
+  PullbackCone.mk (W := {
+    obj X := (c X).pt
+    map {X Y} h := (hc Y).lift ⟨_, (c X).π ≫ cospanHomMk (H.map h) (F.map h) (G.map h)⟩
+    map_id _ := (hc _).hom_ext <| by rintro (_ | _ | _); all_goals simp
+    map_comp _ _ := (hc _).hom_ext <| by rintro (_ | _ | _); all_goals simp })
+    { app X := (c X).fst }
+    { app X := (c X).snd }
+    (by ext; simp [(c _).condition])
+
+/--
+The pullback cone `combinePullbackCones` is limiting.
+-/
+def PullbackCone.combineIsLimit (f : F ⟶ H) (g : G ⟶ H)
+    (c : ∀ X, PullbackCone (f.app X) (g.app X)) (hc : ∀ X, IsLimit (c X)) :
+    IsLimit (combine f g c hc) :=
+  evaluationJointlyReflectsLimits _ fun k ↦ by
+    refine IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_ (hc k)
+    · exact cospanIsoMk (Iso.refl _) (Iso.refl _) (Iso.refl _)
+    · refine Cones.ext (Iso.refl _) ?_
+      rintro (_ | _ | _)
+      all_goals cat_disch
+
 variable [HasPullbacks C]
 
 /-- Evaluating a pullback amounts to taking the pullback of the evaluations. -/

Mathlib/CategoryTheory/Limits/Shapes/Pullback/Cospan.lean

@@ -327,14 +327,32 @@ variable {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z')
 
 section
 
+/-- Constructor for natural transformations between cospans. -/
+@[simps]
+def cospanHomMk {F G : WalkingCospan ⥤ C}
+    (z : F.obj .one ⟶ G.obj .one) (l : F.obj .left ⟶ G.obj .left)
+    (r : F.obj .right ⟶ G.obj .right)
+    (hl : F.map inl ≫ z = l ≫ G.map inl := by cat_disch)
+    (hr : F.map inr ≫ z = r ≫ G.map inr := by cat_disch) : F ⟶ G where
+  app := by rintro (_ | _ | _); exacts [z, l, r]
+  naturality := by rintro (_ | _ | _ ) (_ | _ | _) (_ | _); all_goals cat_disch
+
+/-- Constructor for natural isomorphisms between cospans. -/
+@[simps!]
+def cospanIsoMk {F G : WalkingCospan ⥤ C}
+    (z : F.obj .one ≅ G.obj .one) (l : F.obj .left ≅ G.obj .left)
+    (r : F.obj .right ≅ G.obj .right)
+    (hl : F.map inl ≫ z.hom = l.hom ≫ G.map inl := by cat_disch)
+    (hr : F.map inr ≫ z.hom = r.hom ≫ G.map inr := by cat_disch) : F ≅ G :=
+  NatIso.ofComponents (by rintro (_ | _ | _); exacts [z, l, r])
+    (by rintro (_ | _ | _ ) (_ | _ | _) (_ | _); all_goals cat_disch)
+
 variable {f : X ⟶ Z} {g : Y ⟶ Z} {f' : X' ⟶ Z'} {g' : Y' ⟶ Z'}
 
 /-- Construct an isomorphism of cospans from components. -/
 def cospanExt (wf : iX.hom ≫ f' = f ≫ iZ.hom) (wg : iY.hom ≫ g' = g ≫ iZ.hom) :
     cospan f g ≅ cospan f' g' :=
-  NatIso.ofComponents
-    (by rintro (⟨⟩ | ⟨⟨⟩⟩); exacts [iZ, iX, iY])
-    (by rintro (⟨⟩ | ⟨⟨⟩⟩) (⟨⟩ | ⟨⟨⟩⟩) f <;> cases f <;> simp [wf, wg])
+  cospanIsoMk iZ iX iY
 
 variable (wf : iX.hom ≫ f' = f ≫ iZ.hom) (wg : iY.hom ≫ g' = g ≫ iZ.hom)
 
@@ -375,13 +393,32 @@ end
 
 section
 
+/-- Constructor for natural transformations between spans. -/
+@[simps]
+def spanHomMk {F G : WalkingSpan ⥤ C}
+    (z : F.obj .zero ⟶ G.obj .zero) (l : F.obj .left ⟶ G.obj .left)
+    (r : F.obj .right ⟶ G.obj .right)
+    (hl : F.map fst ≫ l = z ≫ G.map fst := by cat_disch)
+    (hr : F.map snd ≫ r = z ≫ G.map snd := by cat_disch) : F ⟶ G where
+  app := by rintro (_ | _ | _); exacts [z, l, r]
+  naturality := by rintro (_ | _ | _ ) (_ | _ | _) (_ | _); all_goals cat_disch
+
+/-- Constructor for natural isomorphisms between spans. -/
+@[simps!]
+def spanIsoMk {F G : WalkingSpan ⥤ C}
+    (z : F.obj .zero ≅ G.obj .zero) (l : F.obj .left ≅ G.obj .left)
+    (r : F.obj .right ≅ G.obj .right)
+    (hl : F.map fst ≫ l.hom = z.hom ≫ G.map fst := by cat_disch)
+    (hr : F.map snd ≫ r.hom = z.hom ≫ G.map snd := by cat_disch) : F ≅ G :=
+  NatIso.ofComponents (by rintro (_ | _ | _); exacts [z, l, r])
+    (by rintro (_ | _ | _ ) (_ | _ | _) (_ | _); all_goals cat_disch)
+
 variable {f : X ⟶ Y} {g : X ⟶ Z} {f' : X' ⟶ Y'} {g' : X' ⟶ Z'}
 
 /-- Construct an isomorphism of spans from components. -/
 def spanExt (wf : iX.hom ≫ f' = f ≫ iY.hom) (wg : iX.hom ≫ g' = g ≫ iZ.hom) :
     span f g ≅ span f' g' :=
-  NatIso.ofComponents (by rintro (⟨⟩ | ⟨⟨⟩⟩); exacts [iX, iY, iZ])
-    (by rintro (⟨⟩ | ⟨⟨⟩⟩) (⟨⟩ | ⟨⟨⟩⟩) f <;> cases f <;> simp [wf, wg])
+  spanIsoMk iX iY iZ
 
 variable (wf : iX.hom ≫ f' = f ≫ iY.hom) (wg : iX.hom ≫ g' = g ≫ iZ.hom)