# The Yoneda lemma for categories

Content created by Fredrik Bakke, Egbert Rijke, Daniel Gratzer and Elisabeth Stenholm.

Created on 2023-09-18.

module category-theory.yoneda-lemma-categories where

Imports
open import category-theory.categories
open import category-theory.copresheaf-categories
open import category-theory.natural-transformations-functors-from-small-to-large-categories
open import category-theory.representable-functors-categories
open import category-theory.yoneda-lemma-precategories

open import foundation.category-of-sets
open import foundation.equivalences
open import foundation.universe-levels


## Idea

Given a category C, an object c, and a functor F from C to the category of sets

  F : C → Set,


there is an equivalence between the set of natural transformations from the functor represented by c to F and the set F c.

  Nat(Hom(c , -) , F) ≃ F c


More precisely, the Yoneda lemma asserts that the map from the type of natural transformations to the type F c defined by evaluating the component of the natural transformation at the object c at the identity arrow on c is an equivalence.

## Theorem

### The Yoneda lemma into the large category of sets

module _
{l1 l2 l3 : Level} (C : Category l1 l2) (c : obj-Category C)
(F : copresheaf-Precategory (precategory-Category C) l3)
where

map-yoneda-Category :
hom-copresheaf-Precategory
( precategory-Category C) (representable-functor-Category C c) F →
element-copresheaf-Precategory (precategory-Category C) F c
map-yoneda-Category =
map-yoneda-Precategory (precategory-Category C) c F


The inverse to the Yoneda map:

  hom-family-extension-yoneda-Category :
(u : element-copresheaf-Precategory (precategory-Category C) F c) →
hom-family-functor-Small-Large-Category
C Set-Large-Category (representable-functor-Category C c) F
hom-family-extension-yoneda-Category =
hom-family-extension-yoneda-Precategory (precategory-Category C) c F

naturality-extension-yoneda-Category :
(u : element-copresheaf-Precategory (precategory-Category C) F c) →
is-natural-transformation-Small-Large-Category
C Set-Large-Category (representable-functor-Category C c) F
( hom-family-extension-yoneda-Category u)
naturality-extension-yoneda-Category =
naturality-extension-yoneda-Precategory (precategory-Category C) c F

extension-yoneda-Category :
element-copresheaf-Precategory (precategory-Category C) F c →
hom-copresheaf-Precategory
( precategory-Category C) (representable-functor-Category C c) F
extension-yoneda-Category =
extension-yoneda-Precategory (precategory-Category C) c F

lemma-yoneda-Category : is-equiv map-yoneda-Category
lemma-yoneda-Category = lemma-yoneda-Precategory (precategory-Category C) c F

equiv-lemma-yoneda-Category :
hom-copresheaf-Precategory
( precategory-Category C) (representable-functor-Category C c) F ≃
element-copresheaf-Precategory (precategory-Category C) F c
equiv-lemma-yoneda-Category =
equiv-lemma-yoneda-Precategory (precategory-Category C) c F


## Corollaries

### The Yoneda lemma for representable functors

An important special-case of the Yoneda lemma is when F is itself a representable functor F = Hom(-, d).

module _
{l1 l2 : Level} (C : Category l1 l2) (c d : obj-Category C)
where

equiv-lemma-yoneda-representable-Category :
hom-copresheaf-Precategory
( precategory-Category C)
( representable-functor-Category C c)
( representable-functor-Category C d) ≃
hom-Category C d c
equiv-lemma-yoneda-representable-Category =
equiv-lemma-yoneda-Category C c (representable-functor-Category C d)