The Yoneda lemma for categories

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

Created on 2023-09-18.
Last modified on 2024-02-08.

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)

See also

Recent changes