feat(category_theory/*): Curried yoneda lemma (#9579)

Provided curried versions of the Yoneda lemma when the category is small.



Co-authored-by: erdOne <36414270+erdOne@users.noreply.github.com>

src/category_theory/closed/cartesian.lean

@@ -145,12 +145,6 @@ def uncurry : (Y ⟶ A ⟹ X) → (A ⨯ Y ⟶ X) :=
 @[simp] lemma hom_equiv_symm_apply_eq (f : Y ⟶ A ⟹ X) :
   ((exp.adjunction A).hom_equiv _ _).symm f = uncurry f := rfl
 
-end cartesian_closed
-
-open cartesian_closed
-
-variables [has_finite_products C] [exponentiable A]
-
 @[reassoc]
 lemma curry_natural_left (f : X ⟶ X') (g : A ⨯ X' ⟶ Y) :
   curry (limits.prod.map (𝟙 _) f ≫ g) = f ≫ curry g :=
@@ -206,22 +200,27 @@ lemma curry_injective : function.injective (curry : (A ⨯ Y ⟶ X) → (Y ⟶ A
 lemma uncurry_injective : function.injective (uncurry : (Y ⟶ A ⟹ X) → (A ⨯ Y ⟶ X)) :=
 (closed.is_adj.adj.hom_equiv _ _).symm.injective
 
+end cartesian_closed
+
+open cartesian_closed
+variables [has_finite_products C] [exponentiable A]
+
 /--
 Show that the exponential of the terminal object is isomorphic to itself, i.e. `X^1 ≅ X`.
 
 The typeclass argument is explicit: any instance can be used.
 -/
 def exp_terminal_iso_self [exponentiable ⊤_ C] : (⊤_ C ⟹ X) ≅ X :=
 yoneda.ext (⊤_ C ⟹ X) X
-  (λ Y f, (prod.left_unitor Y).inv ≫ uncurry f)
-  (λ Y f, curry ((prod.left_unitor Y).hom ≫ f))
+  (λ Y f, (prod.left_unitor Y).inv ≫ cartesian_closed.uncurry f)
+  (λ Y f, cartesian_closed.curry ((prod.left_unitor Y).hom ≫ f))
   (λ Z g, by rw [curry_eq_iff, iso.hom_inv_id_assoc] )
   (λ Z g, by simp)
   (λ Z W f g, by rw [uncurry_natural_left, prod.left_unitor_inv_naturality_assoc f] )
 
 /-- The internal element which points at the given morphism. -/
 def internalize_hom (f : A ⟶ Y) : ⊤_ C ⟶ (A ⟹ Y) :=
-curry (limits.prod.fst ≫ f)
+cartesian_closed.curry (limits.prod.fst ≫ f)
 
 section pre
 
@@ -237,7 +236,7 @@ lemma prod_map_pre_app_comp_ev (f : B ⟶ A) [exponentiable B] (X : C) :
 transfer_nat_trans_self_counit _ _ (prod.functor.map f) X
 
 lemma uncurry_pre (f : B ⟶ A) [exponentiable B] (X : C) :
-  uncurry ((pre f).app X) = limits.prod.map f (𝟙 _) ≫ (ev A).app X :=
+  cartesian_closed.uncurry ((pre f).app X) = limits.prod.map f (𝟙 _) ≫ (ev A).app X :=
 begin
   rw [uncurry_eq, prod_map_pre_app_comp_ev]
 end
@@ -270,7 +269,7 @@ def zero_mul {I : C} (t : is_initial I) : A ⨯ I ≅ I :=
   inv := t.to _,
   hom_inv_id' :=
   begin
-    have: (limits.prod.snd : A ⨯ I ⟶ I) = uncurry (t.to _),
+    have: (limits.prod.snd : A ⨯ I ⟶ I) = cartesian_closed.uncurry (t.to _),
       rw ← curry_eq_iff,
       apply t.hom_ext,
     rw [this, ← uncurry_natural_right, ← eq_curry_iff],
@@ -285,7 +284,7 @@ limits.prod.braiding _ _ ≪≫ zero_mul t
 /-- If an initial object `0` exists in a CCC then `0^B ≅ 1` for any `B`. -/
 def pow_zero {I : C} (t : is_initial I) [cartesian_closed C] : I ⟹ B ≅ ⊤_ C :=
 { hom := default _,
-  inv := curry ((mul_zero t).hom ≫ t.to _),
+  inv := cartesian_closed.curry ((mul_zero t).hom ≫ t.to _),
   hom_inv_id' :=
   begin
     rw [← curry_natural_left, curry_eq_iff, ← cancel_epi (mul_zero t).inv],
@@ -300,7 +299,8 @@ def pow_zero {I : C} (t : is_initial I) [cartesian_closed C] : I ⟹ B ≅ ⊤_
 def prod_coprod_distrib [has_binary_coproducts C] [cartesian_closed C] (X Y Z : C) :
   (Z ⨯ X) ⨿ (Z ⨯ Y) ≅ Z ⨯ (X ⨿ Y) :=
 { hom := coprod.desc (limits.prod.map (𝟙 _) coprod.inl) (limits.prod.map (𝟙 _) coprod.inr),
-  inv := uncurry (coprod.desc (curry coprod.inl) (curry coprod.inr)),
+  inv := cartesian_closed.uncurry
+    (coprod.desc (cartesian_closed.curry coprod.inl) (cartesian_closed.curry coprod.inr)),
   hom_inv_id' :=
   begin
     apply coprod.hom_ext,

src/category_theory/closed/functor.lean

@@ -104,7 +104,8 @@ begin
 end
 
 lemma uncurry_exp_comparison (A B : C) :
-  uncurry ((exp_comparison F A).app B) = inv (prod_comparison F _ _) ≫ F.map ((ev _).app _) :=
+  cartesian_closed.uncurry ((exp_comparison F A).app B) =
+    inv (prod_comparison F _ _) ≫ F.map ((ev _).app _) :=
 by rw [uncurry_eq, exp_comparison_ev]
 
 /-- The exponential comparison map is natural in `A`. -/

src/category_theory/closed/ideal.lean

@@ -61,6 +61,8 @@ end⟩
 instance : exponential_ideal (𝟭 C) :=
 exponential_ideal.mk' _ (λ B A, ⟨_, ⟨iso.refl _⟩⟩)
 
+open cartesian_closed
+
 /-- The subcategory of subterminal objects is an exponential ideal. -/
 instance : exponential_ideal (subterminal_inclusion C) :=
 begin
@@ -112,6 +114,8 @@ lemma reflective_products [has_finite_products C] [reflective i] : has_finite_pr
 
 local attribute [instance, priority 10] reflective_products
 
+open cartesian_closed
+
 variables [has_finite_products C] [reflective i] [cartesian_closed C]
 
 /--

src/category_theory/types.lean

@@ -143,6 +143,12 @@ instance ulift_functor_faithful : faithful ulift_functor :=
 { map_injective' := λ X Y f g p, funext $ λ x,
     congr_arg ulift.down ((congr_fun p (ulift.up x)) : ((ulift.up (f x)) = (ulift.up (g x)))) }
 
+/--
+The functor embedding `Type u` into `Type u` via `ulift` is isomorphic to the identity functor.
+ -/
+def ulift_functor_trivial : ulift_functor.{u u} ≅ 𝟭 _ :=
+nat_iso.of_components ulift_trivial (by tidy)
+
 /-- Any term `x` of a type `X` corresponds to a morphism `punit ⟶ X`. -/
 -- TODO We should connect this to a general story about concrete categories
 -- whose forgetful functor is representable.

src/category_theory/yoneda.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import category_theory.hom_functor
+import category_theory.currying
+import category_theory.products.basic
 
 /-!
 # The Yoneda embedding
@@ -385,4 +387,20 @@ lemma yoneda_sections_small_inv_app_apply {C : Type u₁} [small_category C] (X
   ((yoneda_sections_small X F).inv t).app Y f = F.map f.op t :=
 rfl
 
+local attribute[ext] functor.ext
+
+/-- The curried version of yoneda lemma when `C` is small. -/
+def curried_yoneda_lemma {C : Type u₁} [small_category C] :
+  (yoneda.op ⋙ coyoneda : Cᵒᵖ ⥤ (Cᵒᵖ ⥤ Type u₁) ⥤ Type u₁) ≅ evaluation Cᵒᵖ (Type u₁) :=
+eq_to_iso (by tidy) ≪≫ curry.map_iso (yoneda_lemma C ≪≫
+  iso_whisker_left (evaluation_uncurried Cᵒᵖ (Type u₁)) ulift_functor_trivial) ≪≫
+    eq_to_iso (by tidy)
+
+/-- The curried version of yoneda lemma when `C` is small. -/
+def curried_yoneda_lemma' {C : Type u₁} [small_category C] :
+  yoneda ⋙ (whiskering_left Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)).obj yoneda.op ≅ 𝟭 (Cᵒᵖ ⥤ Type u₁) :=
+eq_to_iso (by tidy) ≪≫ curry.map_iso (iso_whisker_left (prod.swap _ _)
+  (yoneda_lemma C ≪≫ iso_whisker_left
+    (evaluation_uncurried Cᵒᵖ (Type u₁)) ulift_functor_trivial : _)) ≪≫ eq_to_iso (by tidy)
+
 end category_theory