From 8d27fbf359865a12c7bc7ed41bfe6ede9fd372a3 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@himmel-villmar.de>
Date: Sun, 20 Oct 2024 16:57:21 +0000
Subject: [PATCH] feat(CategoryTheory): pull colimits out of hom functors with
 Yoneda on the LHS (#17440)

A technical result on the way towards showing that Ind-objects are closed under filtered colimits.



Co-authored-by: Markus Himmel <markus@lean-fro.org>
---
 Mathlib.lean                                  |  1 +
 .../Limits/Preserves/Yoneda.lean              | 79 +++++++++++++++++++
 2 files changed, 80 insertions(+)
 create mode 100644 Mathlib/CategoryTheory/Limits/Preserves/Yoneda.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index de1b28985d7b6..ebba90f308a9c 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1682,6 +1682,7 @@ import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square
 import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
 import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
 import Mathlib.CategoryTheory.Limits.Preserves.Ulift
+import Mathlib.CategoryTheory.Limits.Preserves.Yoneda
 import Mathlib.CategoryTheory.Limits.Presheaf
 import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
 import Mathlib.CategoryTheory.Limits.Shapes.Biproducts
diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Yoneda.lean b/Mathlib/CategoryTheory/Limits/Preserves/Yoneda.lean
new file mode 100644
index 0000000000000..629c22852c6a5
--- /dev/null
+++ b/Mathlib/CategoryTheory/Limits/Preserves/Yoneda.lean
@@ -0,0 +1,79 @@
+/-
+Copyright (c) 2024 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import Mathlib.CategoryTheory.Limits.Preserves.Ulift
+import Mathlib.CategoryTheory.Limits.FunctorToTypes
+
+/-!
+# Yoneda preserves certain colimits
+
+Given a bifunctor `F : J ⥤ Cᵒᵖ ⥤ Type v`, we prove the isomorphism
+`Hom(YX, colim_j F(j, -)) ≅ colim_j Hom(YX, F(j, -))`, where `Y` is the Yoneda embedding.
+
+We state this in two ways. One is functorial in `X` and stated as a natural isomorphism of functors
+`yoneda.op ⋙ yoneda.obj (colimit F) ≅ yoneda.op ⋙ colimit (F ⋙ yoneda)`, and from this we
+deduce the more traditional preservation statement
+`PreservesColimit F (coyoneda.obj (op (yoneda.obj X)))`.
+
+The proof combines the Yoneda lemma with the fact that colimits in functor categories are computed
+pointwise.
+
+## See also
+
+There is also a relative version of this statement where `F : J ⥤ Over A` for some presheaf
+`A`, see `CategoryTheory.Comma.Presheaf`.
+
+-/
+
+universe v₁ v₂ v₃ u₁ u₂ u₃
+
+namespace CategoryTheory
+
+open CategoryTheory.Limits Opposite
+
+variable {C : Type u₁} [Category.{v₁} C]
+
+variable {J : Type u₂} [Category.{v₂} J] [HasColimitsOfShape J (Type v₁)]
+  [HasColimitsOfShape J (Type (max u₁ v₁))] (F : J ⥤ Cᵒᵖ ⥤ Type v₁)
+
+/-- Naturally in `X`, we have `Hom(YX, colim_i Fi) ≅ colim_i Hom(YX, Fi)`. -/
+noncomputable def yonedaYonedaColimit :
+    yoneda.op ⋙ yoneda.obj (colimit F) ≅ yoneda.op ⋙ colimit (F ⋙ yoneda) := calc
+  yoneda.op ⋙ yoneda.obj (colimit F)
+    ≅ colimit F ⋙ uliftFunctor.{u₁} := yonedaOpCompYonedaObj (colimit F)
+  _ ≅ F.flip ⋙ colim ⋙ uliftFunctor.{u₁} :=
+        isoWhiskerRight (colimitIsoFlipCompColim F) uliftFunctor.{u₁}
+  _ ≅ F.flip ⋙ (whiskeringRight _ _ _).obj uliftFunctor.{u₁} ⋙ colim :=
+        isoWhiskerLeft F.flip (preservesColimitNatIso uliftFunctor.{u₁})
+  _ ≅ (yoneda.op ⋙ coyoneda ⋙ (whiskeringLeft _ _ _).obj F) ⋙ colim := isoWhiskerRight
+        (isoWhiskerRight largeCurriedYonedaLemma.symm ((whiskeringLeft _ _ _).obj F)) colim
+  _ ≅ yoneda.op ⋙ colimit (F ⋙ yoneda) :=
+        isoWhiskerLeft yoneda.op (colimitIsoFlipCompColim (F ⋙ yoneda)).symm
+
+theorem yonedaYonedaColimit_app_inv {X : C} : ((yonedaYonedaColimit F).app (op X)).inv =
+    (colimitObjIsoColimitCompEvaluation _ _).hom ≫
+      (colimit.post F (coyoneda.obj (op (yoneda.obj X)))) := by
+  dsimp [yonedaYonedaColimit]
+  simp only [Category.id_comp, Iso.cancel_iso_hom_left]
+  apply colimit.hom_ext
+  intro j
+  rw [colimit.ι_post, ι_colimMap_assoc]
+  simp only [← CategoryTheory.Functor.assoc, comp_evaluation]
+  rw [ι_preservesColimitsIso_inv_assoc, ← Functor.map_comp_assoc]
+  simp only [← comp_evaluation]
+  rw [colimitObjIsoColimitCompEvaluation_ι_inv, whiskerLeft_app]
+  ext η Y f
+  simp [largeCurriedYonedaLemma, yonedaOpCompYonedaObj, FunctorToTypes.colimit.map_ι_apply,
+    map_yonedaEquiv]
+
+noncomputable instance {X : C} : PreservesColimit F (coyoneda.obj (op (yoneda.obj X))) := by
+  suffices IsIso (colimit.post F (coyoneda.obj (op (yoneda.obj X)))) from
+    preservesColimitOfIsIsoPost _ _
+  suffices colimit.post F (coyoneda.obj (op (yoneda.obj X))) =
+      (colimitObjIsoColimitCompEvaluation _ _).inv ≫ ((yonedaYonedaColimit F).app (op X)).inv from
+    this ▸ inferInstance
+  rw [yonedaYonedaColimit_app_inv, Iso.inv_hom_id_assoc]
+
+end CategoryTheory