feat(CategoryTheory/Yoneda): add curried version of Yoneda lemma for heterogeneous universes, and other version of homNatIso (#27819)

Prove a curried version of `yonedaCompUliftFunctorEquiv`, ie a completely functorial version of the Yoneda lemma with heterogeneous universes. Dually, prove a curried version of `coyonedaCompUliftFunctorEquiv`, ie a completely functorial version of the coYoneda lemma with heterogeneous universes.

In addition, prove a functorial version of `FullyFaithful.natEquiv` using `coyoneda` instead of `yoneda` (previously, the only functorial version of `FullyFaithful.natEquiv` were `homNatIso`, which is written using `yoneda`).

Co-authored-by: Benoît Guillemet <benoit@guillemet.org>

Author: BGuillemet

Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean

@@ -111,8 +111,8 @@ lemma exists_pushouts
     ∃ (X' : C) (i : X ⟶ X') (p' : X' ⟶ Y) (_ : (generatingMonomorphisms G).pushouts i)
       (_ : ¬ IsIso i) (_ : Mono p'), i ≫ p' = p := by
   rw [hG.isDetector.isIso_iff_of_mono] at hp
-  simp only [ObjectProperty.singleton_iff, Function.Surjective, coyoneda_obj_obj,
-    coyoneda_obj_map, forall_eq', not_forall, not_exists] at hp
+  simp only [ObjectProperty.singleton_iff, Function.Surjective, Functor.flip_obj_obj,
+    yoneda_obj_obj, Functor.flip_obj_map, forall_eq', not_forall, not_exists] at hp
   -- `f : G ⟶ Y` is a monomorphism the image of which is not contained in `X`
   obtain ⟨f, hf⟩ := hp
   -- we use the subobject `X'` of `Y` that is generated by the images of `p : X ⟶ Y`

Mathlib/CategoryTheory/Filtered/Final.lean

@@ -236,7 +236,7 @@ theorem Functor.Final.exists_coeq_of_locally_small [IsFilteredOrEmpty C] [Final
   obtain ⟨c', t₁, t₂, h⟩ := (Types.FilteredColimit.colimit_eq_iff.{v₁, v₁, v₁} _).mp this
   refine ⟨IsFiltered.coeq t₁ t₂, t₁ ≫ IsFiltered.coeqHom t₁ t₂, ?_⟩
   conv_rhs => rw [IsFiltered.coeq_condition t₁ t₂]
-  dsimp only [comp_obj, coyoneda_obj_obj, unop_op, Functor.comp_map, coyoneda_obj_map] at h
+  dsimp only [comp_obj, flip_obj_obj, yoneda_obj_obj, comp_map, flip_obj_map, yoneda_map_app] at h
   simp [reassoc_of% h]
 
 end LocallySmall

Mathlib/CategoryTheory/Limits/IndYoneda.lean

@@ -68,15 +68,15 @@ noncomputable def colimitHomIsoLimitYoneda
 @[reassoc (attr := simp)]
 lemma colimitHomIsoLimitYoneda_hom_comp_π [HasLimitsOfShape Iᵒᵖ (Type u₂)] (A : C) (i : I) :
     (colimitHomIsoLimitYoneda F A).hom ≫ limit.π (F.op ⋙ yoneda.obj A) ⟨i⟩ =
-      (coyoneda.map (colimit.ι F i).op).app A := by
+      (yoneda.obj A).map (colimit.ι F i).op := by
   simp only [colimitHomIsoLimitYoneda, Iso.trans_hom, Iso.app_hom, Category.assoc]
   erw [limitObjIsoLimitCompEvaluation_hom_π]
   change ((coyonedaOpColimitIsoLimitCoyoneda F).hom ≫ _).app A = _
-  rw [coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π]
+  rw [coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π, Functor.flip_map_app]
 
 @[reassoc (attr := simp)]
 lemma colimitHomIsoLimitYoneda_inv_comp_π [HasLimitsOfShape Iᵒᵖ (Type u₂)] (A : C) (i : I) :
-    (colimitHomIsoLimitYoneda F A).inv ≫ (coyoneda.map (colimit.ι F i).op).app A =
+    (colimitHomIsoLimitYoneda F A).inv ≫ (yoneda.obj A).map (colimit.ι F i).op =
       limit.π (F.op ⋙ yoneda.obj A) ⟨i⟩ := by
   rw [← colimitHomIsoLimitYoneda_hom_comp_π, ← Category.assoc,
     Iso.inv_hom_id, Category.id_comp]
@@ -115,16 +115,16 @@ noncomputable def colimitHomIsoLimitYoneda' [HasLimitsOfShape I (Type u₂)] (A
 @[reassoc (attr := simp)]
 lemma colimitHomIsoLimitYoneda'_hom_comp_π [HasLimitsOfShape I (Type u₂)] (A : C) (i : I) :
     (colimitHomIsoLimitYoneda' F A).hom ≫ limit.π (F.rightOp ⋙ yoneda.obj A) i =
-      (coyoneda.map (colimit.ι F ⟨i⟩).op).app A := by
+      (yoneda.obj A).map (colimit.ι F ⟨i⟩).op := by
   simp only [colimitHomIsoLimitYoneda', Iso.trans_hom,
     Iso.app_hom, Category.assoc]
   erw [limitObjIsoLimitCompEvaluation_hom_π]
   change ((coyonedaOpColimitIsoLimitCoyoneda' F).hom ≫ _).app A = _
-  rw [coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π]
+  rw [coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π, Functor.flip_map_app]
 
 @[reassoc (attr := simp)]
 lemma colimitHomIsoLimitYoneda'_inv_comp_π [HasLimitsOfShape I (Type u₂)] (A : C) (i : I) :
-    (colimitHomIsoLimitYoneda' F A).inv ≫ (coyoneda.map (colimit.ι F ⟨i⟩).op).app A =
+    (colimitHomIsoLimitYoneda' F A).inv ≫ (yoneda.obj A).map (colimit.ι F ⟨i⟩).op =
       limit.π (F.rightOp ⋙ yoneda.obj A) i := by
   rw [← colimitHomIsoLimitYoneda'_hom_comp_π, ← Category.assoc,
     Iso.inv_hom_id, Category.id_comp]

Mathlib/CategoryTheory/Limits/Indization/FilteredColimits.lean

@@ -126,9 +126,9 @@ theorem isFiltered [IsFiltered I] (hF : ∀ i, IsIndObject (F.obj i)) :
   -- faithful, `lim_j Hom_{Over (colimit F)}(yGj, yHk) ≅`
   --   `lim_j Hom_{CostructuredArrow yoneda (colimit F)}(Gj, Hk)` and so `Hk` is the object we're
   -- looking for.
-  let q := htO.homNatIsoMaxRight
+  let q := fun X => isoWhiskerLeft _ (uliftYonedaIsoYoneda.symm.app _) ≪≫ htO.homNatIso X
   obtain ⟨t'⟩ := Nonempty.map (limMap (isoWhiskerLeft G.op (q _)).hom) hk
-  exact ⟨_, ⟨((preservesLimitIso uliftFunctor.{u, v} _).inv t').down⟩⟩
+  exact ⟨_, ⟨((preservesLimitIso uliftFunctor.{max u v, v} _).inv t').down⟩⟩
 
 end IndizationClosedUnderFilteredColimitsAux
 

Mathlib/CategoryTheory/Limits/Yoneda.lean

@@ -44,8 +44,8 @@ def colimitCoconeIsColimit (X : Cᵒᵖ) : IsColimit (colimitCocone X) where
   fac s Y := by
     funext f
     convert congr_fun (s.w f).symm (𝟙 (unop X))
-    simp only [coyoneda_obj_obj, Functor.const_obj_obj, types_comp_apply,
-      coyoneda_obj_map, Category.id_comp]
+    simp only [Functor.flip_obj_obj, yoneda_obj_obj, Functor.const_obj_obj, Functor.flip_obj_map,
+      types_comp_apply, yoneda_map_app, Category.id_comp]
   uniq s m w := by
     apply funext; rintro ⟨⟩
     rw [← w]

Mathlib/CategoryTheory/Monoidal/Braided/Reflection.lean

@@ -122,8 +122,8 @@ theorem isIso_tfae : List.TFAE
     have w₁ : (coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c = (adj.homEquiv _ _).symm ∘
         (coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c) ∘ adj.homEquiv _ _ := by ext; simp
     rw [w₁, isIso_iff_bijective]
-    simp only [comp_obj, coyoneda_obj_obj, id_obj, EquivLike.comp_bijective,
-      EquivLike.bijective_comp]
+    simp only [comp_obj, flip_obj_obj, yoneda_obj_obj, id_obj, op_tensorObj, unop_tensorObj,
+      EquivLike.comp_bijective, EquivLike.bijective_comp]
     -- We commute the tensor product using the auxiliary commutative square `w₂`.
     have w₂ : ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c)) =
         ((yoneda.obj (R.obj c)).mapIso (β_ _ _)).hom ∘
@@ -135,12 +135,11 @@ theorem isIso_tfae : List.TFAE
         ((ihom.adjunction d').homEquiv _ _).symm ∘
           ((coyoneda.map (adj.unit.app _).op).app _) ∘ (ihom.adjunction d').homEquiv _ _ := by
       ext
-      simp only [id_obj, op_tensorObj, coyoneda_obj_obj, unop_tensorObj, comp_obj,
-        coyoneda_map_app, Quiver.Hom.unop_op, Function.comp_apply,
-        Adjunction.homEquiv_unit, Adjunction.homEquiv_counit]
+      simp only [id_obj, op_tensorObj, flip_obj_obj, yoneda_obj_obj, unop_tensorObj, comp_obj,
+        flip_map_app, Function.comp_apply, Adjunction.homEquiv_unit, Adjunction.homEquiv_counit]
       simp
     rw [w₃, isIso_iff_bijective]
-    simp only [comp_obj, op_tensorObj, coyoneda_obj_obj, unop_tensorObj, id_obj,
+    simp only [comp_obj, op_tensorObj, flip_obj_obj, yoneda_obj_obj, unop_tensorObj, id_obj,
       yoneda_obj_obj, curriedTensor_obj_obj, EquivLike.comp_bijective, EquivLike.bijective_comp]
     have w₄ : (coyoneda.map (adj.unit.app d).op).app ((ihom d').obj (R.obj c)) ≫
         (coyoneda.obj ⟨d⟩).map (adj.unit.app ((ihom d').obj (R.obj c))) =
@@ -156,9 +155,9 @@ theorem isIso_tfae : List.TFAE
     -- We give the inverse of the bottom map in the stack of commutative squares:
     refine ⟨fun f ↦ R.map ((adj.homEquiv _ _).symm f), ?_, by ext; simp⟩
     ext f
-    simp only [comp_obj, coyoneda_obj_obj, id_obj, Adjunction.homEquiv_counit,
-      map_comp, types_comp_apply, coyoneda_map_app, Quiver.Hom.unop_op, Category.assoc,
-      types_id_apply]
+    simp only [comp_obj, flip_obj_obj, yoneda_obj_obj, id_obj, flip_map_app,
+      Adjunction.homEquiv_counit, map_comp, types_comp_apply, yoneda_obj_map, Quiver.Hom.unop_op,
+      Category.assoc]
     have : f = R.map (R.preimage f) := by simp
     rw [this]
     simp [← map_comp, -map_preimage]
@@ -180,8 +179,8 @@ theorem isIso_tfae : List.TFAE
       rw [← Function.comp_assoc, ((ihom.adjunction ((L ⋙ R).obj d)).homEquiv _ _).eq_comp_symm]
       ext
       simp only [id_obj, yoneda_obj_obj, comp_obj, Function.comp_apply,
-        yoneda_map_app, op_tensorObj, coyoneda_obj_obj, unop_tensorObj, op_whiskerRight,
-        coyoneda_map_app, unop_whiskerRight, Quiver.Hom.unop_op]
+        yoneda_map_app, op_tensorObj, flip_obj_obj, yoneda_obj_obj, unop_tensorObj, op_whiskerRight,
+        flip_map_app]
       rw [Adjunction.homEquiv_unit, Adjunction.homEquiv_unit]
       simp
     rw [w₂, w₁, isIso_iff_bijective, isIso_iff_bijective]

Mathlib/CategoryTheory/Sites/DenseSubsite/Basic.lean

@@ -389,7 +389,7 @@ theorem sheafHom_restrict_eq (α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val) :
   · exact (pushforwardFamily_compatible _ _)
   intro Y f hf
   conv_lhs => rw [← hf.some.fac]
-  simp only [pushforwardFamily, Functor.comp_map, yoneda_map_app, coyoneda_obj_map, op_comp,
+  simp only [pushforwardFamily, Functor.comp_map, yoneda_map_app, flip_obj_map, op_comp,
     FunctorToTypes.map_comp_apply, homOver_app]
   congr 1
   simp only [Category.assoc]