chore(category_theory/yoneda): doc-strings (#4429)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/category_theory/products/basic.lean

@@ -101,6 +101,11 @@ end prod
 section
 variables (C : Type u₁) [category.{v₁} C] (D : Type u₂) [category.{v₂} D]
 
+/--
+The "evaluation at `X`" functor, such that
+`(evaluation.obj X).obj F = F.obj X`,
+which is functorial in both `X` and `F`.
+-/
 @[simps] def evaluation : C ⥤ (C ⥤ D) ⥤ D :=
 { obj := λ X,
   { obj := λ F, F.obj X,
@@ -109,6 +114,10 @@ variables (C : Type u₁) [category.{v₁} C] (D : Type u₂) [category.{v₂} D
   { app := λ F, F.map f,
     naturality' := λ F G α, eq.symm (α.naturality f) } }
 
+/--
+The "evaluation of `F` at `X`" functor,
+as a functor `C × (C ⥤ D) ⥤ D`.
+-/
 @[simps] def evaluation_uncurried : C × (C ⥤ D) ⥤ D :=
 { obj := λ p, p.2.obj p.1,
   map := λ x y f, (x.2.map f.1) ≫ (f.2.app y.1),

src/category_theory/yoneda.lean

@@ -96,6 +96,9 @@ def ext (X Y : C)
 @preimage_iso _ _ _ _ yoneda _ _ _ _
   (nat_iso.of_components (λ Z, { hom := p, inv := q, }) (by tidy))
 
+/--
+If `yoneda.map f` is an isomorphism, so was `f`.
+-/
 def is_iso {X Y : C} (f : X ⟶ Y) [is_iso (yoneda.map f)] : is_iso f :=
 is_iso_of_fully_faithful yoneda f
 
@@ -118,6 +121,9 @@ instance coyoneda_faithful : faithful (@coyoneda C _) :=
     simpa using congr_arg has_hom.hom.op t,
   end }
 
+/--
+If `coyoneda.map f` is an isomorphism, so was `f`.
+-/
 def is_iso {X Y : Cᵒᵖ} (f : X ⟶ Y) [is_iso (coyoneda.map f)] : is_iso f :=
 is_iso_of_fully_faithful coyoneda f
 
@@ -154,13 +160,21 @@ category_theory.prod.{v₁ (max u₁ v₁)} Cᵒᵖ (Cᵒᵖ ⥤ Type v₁)
 
 open yoneda
 
+/--
+The "Yoneda evaluation" functor, which sends `X : Cᵒᵖ` and `F : Cᵒᵖ ⥤ Type`
+to `F.obj X`, functorially in both `X` and `F`.
+-/
 def yoneda_evaluation : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁) ⥤ Type (max u₁ v₁) :=
 evaluation_uncurried Cᵒᵖ (Type v₁) ⋙ ulift_functor.{u₁}
 
 @[simp] lemma yoneda_evaluation_map_down
   (P Q : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)) (α : P ⟶ Q) (x : (yoneda_evaluation C).obj P) :
   ((yoneda_evaluation C).map α x).down = α.2.app Q.1 (P.2.map α.1 x.down) := rfl
 
+/--
+The "Yoneda pairing" functor, which sends `X : Cᵒᵖ` and `F : Cᵒᵖ ⥤ Type`
+to `yoneda.op.obj X ⟶ F`, functorially in both `X` and `F`.
+-/
 def yoneda_pairing : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁) ⥤ Type (max u₁ v₁) :=
 functor.prod yoneda.op (𝟭 (Cᵒᵖ ⥤ Type v₁)) ⋙ functor.hom (Cᵒᵖ ⥤ Type v₁)
 
@@ -213,10 +227,19 @@ def yoneda_lemma : yoneda_pairing C ≅ yoneda_evaluation C :=
 
 variables {C}
 
+/--
+The isomorphism between `yoneda.obj X ⟶ F` and `F.obj (op X)`
+(we need to insert a `ulift` to get the universes right!)
+given by the Yoneda lemma.
+-/
 @[simp] def yoneda_sections (X : C) (F : Cᵒᵖ ⥤ Type v₁) :
   (yoneda.obj X ⟶ F) ≅ ulift.{u₁} (F.obj (op X)) :=
 (yoneda_lemma C).app (op X, F)
 
+/--
+When `C` is a small category, we can restate the isomorphism from `yoneda_sections`
+without having to change universes.
+-/
 @[simp] def yoneda_sections_small {C : Type u₁} [small_category C] (X : C) (F : Cᵒᵖ ⥤ Type u₁) :
   (yoneda.obj X ⟶ F) ≅ F.obj (op X) :=
 yoneda_sections X F ≪≫ ulift_trivial _