feat(CategoryTheory/Limits/Shapes/End): functoriality of (co)ends (#27079)

We define basic functoriality properties of the construction `F ↦ end_ F`, and bundle it as a functor whenever all ends exist.

The same is done for coends.

Author: robin-carlier

Mathlib/CategoryTheory/Limits/Shapes/End.lean

@@ -216,13 +216,45 @@ noncomputable def end_.lift : X ⟶ end_ F :=
 lemma end_.lift_π (j : J) : lift f hf ≫ π F j = f j := by
   apply IsLimit.fac
 
+variable {F' : Jᵒᵖ ⥤ J ⥤ C} [HasEnd F'] (f : F ⟶ F')
+
+/-- A natural transformation of functors F ⟶ F' induces a map end_ F ⟶ end_ F'. -/
+noncomputable def end_.map : end_ F ⟶ end_ F' :=
+  end_.lift (fun x ↦ end_.π _ _ ≫ (f.app (op x)).app x) (fun j j' φ ↦ by
+    have e := (f.app (op j)).naturality φ
+    simp only [Category.assoc]
+    rw [← e, reassoc_of% end_.condition F φ]
+    simp)
+
+@[reassoc (attr := simp)]
+lemma end_.map_π (j : J) :
+    end_.map f ≫ end_.π F' j = end_.π _ _ ≫ (f.app (op j)).app j := by
+  simp [end_.map]
+
+@[reassoc (attr := simp)]
+lemma end_.map_comp {F'' : Jᵒᵖ ⥤ J ⥤ C} [HasEnd F''] (g : F' ⟶ F'') :
+    end_.map f ≫ end_.map g = end_.map (f ≫ g) := by
+  aesop_cat
+
+@[simp]
+lemma end_.map_id : end_.map (𝟙 F) = 𝟙 _ := by aesop_cat
+
 end
 
+variable (J C) in
+/-- If all bifunctors `Jᵒᵖ ⥤ J ⥤ C` have an end, then the construction
+`F ↦ end_ F` defines a functor `(Jᵒᵖ ⥤ J ⥤ C) ⥤ C`. -/
+@[simps]
+noncomputable def endFunctor [∀ (F : Jᵒᵖ ⥤ J ⥤ C), HasEnd F] :
+    (Jᵒᵖ ⥤ J ⥤ C) ⥤ C where
+  obj F := end_ F
+  map f := end_.map f
+
 end End
 
 section Coend
 
-/-- Given `F : Jᵒᵖ ⥤ J ⥤ C`, this property asserts the existence of the end of `F`. -/
+/-- Given `F : Jᵒᵖ ⥤ J ⥤ C`, this property asserts the existence of the coend of `F`. -/
 abbrev HasCoend := HasMulticoequalizer (multispanIndexCoend F)
 
 variable [HasCoend F]
@@ -252,16 +284,45 @@ section
 variable {X : C} (f : ∀ j, (F.obj (op j)).obj j ⟶ X)
   (hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), (F.map g.op).app i ≫ f i = (F.obj (op j)).map g ≫ f j)
 
-/-- Constructor for morphisms to the end of a functor. -/
+/-- Constructor for morphisms to the coend of a functor. -/
 noncomputable def coend.desc : coend F ⟶ X :=
   Cowedge.IsColimit.desc (colimit.isColimit _) f hf
 
 @[reassoc (attr := simp)]
 lemma coend.ι_desc (j : J) : ι F j ≫ desc f hf = f j := by
   apply IsColimit.fac
 
+variable {F' : Jᵒᵖ ⥤ J ⥤ C} [HasCoend F'] (f : F ⟶ F')
+
+/-- A natural transformation of functors F ⟶ F' induces a map coend F ⟶ coend F'. -/
+noncomputable def coend.map : coend F ⟶ coend F' :=
+  coend.desc (fun x ↦ (f.app (op x)).app x ≫ coend.ι _ _ ) (fun j j' φ ↦ by
+    simp [coend.condition])
+
+@[reassoc (attr := simp)]
+lemma coend.ι_map (j : J) :
+    coend.ι _ _ ≫ coend.map f = (f.app (op j)).app j ≫ coend.ι _ _ := by
+  simp [coend.map]
+
+@[reassoc (attr := simp)]
+lemma coend.map_comp {F'' : Jᵒᵖ ⥤ J ⥤ C} [HasCoend F''] (g : F' ⟶ F'') :
+    coend.map f ≫ coend.map g = coend.map (f ≫ g) := by
+  aesop_cat
+
+@[simp]
+lemma coend.map_id : coend.map (𝟙 F) = 𝟙 _ := by aesop_cat
+
 end
 
+variable (J C) in
+/-- If all bifunctors `Jᵒᵖ ⥤ J ⥤ C` have a coend, then the construction
+`F ↦ coend F` defines a functor `(Jᵒᵖ ⥤ J ⥤ C) ⥤ C`. -/
+@[simps]
+noncomputable def coendFunctor [∀ (F : Jᵒᵖ ⥤ J ⥤ C), HasCoend F] :
+    (Jᵒᵖ ⥤ J ⥤ C) ⥤ C where
+  obj F := coend F
+  map f := coend.map f
+
 end Coend
 
 end Limits