The Yoneda lemma for precategories

Content created by Fredrik Bakke, Egbert Rijke, Emily Riehl, Daniel Gratzer, Elisabeth Stenholm, Julian KG, fernabnor and louismntnu.

Created on 2023-05-27.
Last modified on 2024-02-08.

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

open import foundation.action-on-identifications-functions
open import foundation.category-of-sets
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.subtypes
open import foundation.universe-levels

Idea

Given a precategory 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 : Precategory l1 l2) (c : obj-Precategory C)
  (F : copresheaf-Precategory C l3)
  where

  map-yoneda-Precategory :
    hom-copresheaf-Precategory C (representable-functor-Precategory C c) F →
    element-copresheaf-Precategory C F c
  map-yoneda-Precategory σ =
    hom-natural-transformation-Small-Large-Precategory
      ( C)
      ( Set-Large-Precategory)
      ( representable-functor-Precategory C c)
      ( F)
      ( σ)
      ( c)
      ( id-hom-Precategory C)

The inverse to the Yoneda map:

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

  naturality-extension-yoneda-Precategory :
    (u : element-copresheaf-Precategory C F c) →
    is-natural-transformation-Small-Large-Precategory
      C Set-Large-Precategory (representable-functor-Precategory C c) F
      ( hom-family-extension-yoneda-Precategory u)
  naturality-extension-yoneda-Precategory u g =
    eq-htpy
      ( λ f →
        htpy-eq
          ( inv
            ( preserves-comp-functor-Small-Large-Precategory
                C Set-Large-Precategory F g f))
          ( u))

  extension-yoneda-Precategory :
    element-copresheaf-Precategory C F c →
    hom-copresheaf-Precategory C (representable-functor-Precategory C c) F
  pr1 (extension-yoneda-Precategory u) =
    hom-family-extension-yoneda-Precategory u
  pr2 (extension-yoneda-Precategory u) =
    naturality-extension-yoneda-Precategory u

The inverse is an inverse:

  is-section-extension-yoneda-Precategory :
    ( map-yoneda-Precategory ∘
      extension-yoneda-Precategory) ~
    id
  is-section-extension-yoneda-Precategory =
    htpy-eq
      ( preserves-id-functor-Small-Large-Precategory
          C Set-Large-Precategory F c)

  is-retraction-extension-yoneda-Precategory :
    ( extension-yoneda-Precategory ∘
      map-yoneda-Precategory) ~
    id
  is-retraction-extension-yoneda-Precategory σ =
    eq-type-subtype
      ( is-natural-transformation-prop-Small-Large-Precategory
        ( C) Set-Large-Precategory (representable-functor-Precategory C c) F)
      ( eq-htpy
        ( λ x →
          eq-htpy
            ( λ f →
              ( htpy-eq
                ( pr2 σ f)
                ( id-hom-Precategory C)) ∙
              ( ap (pr1 σ x) (right-unit-law-comp-hom-Precategory C f)))))

  lemma-yoneda-Precategory : is-equiv map-yoneda-Precategory
  lemma-yoneda-Precategory =
    is-equiv-is-invertible
      ( extension-yoneda-Precategory)
      ( is-section-extension-yoneda-Precategory)
      ( is-retraction-extension-yoneda-Precategory)

  equiv-lemma-yoneda-Precategory :
    hom-copresheaf-Precategory C (representable-functor-Precategory C c) F ≃
    element-copresheaf-Precategory C F c
  pr1 equiv-lemma-yoneda-Precategory = map-yoneda-Precategory
  pr2 equiv-lemma-yoneda-Precategory = lemma-yoneda-Precategory

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 : Precategory l1 l2) (c d : obj-Precategory C)
  where

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

See also

Recent changes