3.6. Yoneda's lemma
If C is a category (with morphisms in the universe v), the Yoneda embedding is
a fully-faithful embedding of C in the category of presheaves Cᵒᵖ ⥤ Type v. It sends
an object X : C to the presheaf yoneda.obj X that is represented by X:
this is the functor Cᵒᵖ ⥤ Type v which sends Y : C (considered as an object of Cᵒᵖ)
to the type Y ⟶ X:
variable {C : Type u} [Category.{v} C]
example : C ⥤ Cᵒᵖ ⥤ Type v := yoneda
example {X Y : C} :
(yoneda.obj X).obj (.op Y) = (Y ⟶ X) := C:Type uinst✝:Category.{v, u} CX:CY:C⊢ (yoneda.obj X).obj (Opposite.op Y) = (Y ⟶ X)
with_implicit All goals completed! 🐙
example : (yoneda : C ⥤ _).Faithful := inferInstance
example : (yoneda : C ⥤ _).Full := inferInstance
We used the Prop-valued typeclasses Functor.Faithful and Functor.Full in order to
state that yoneda : C ⥤ Cᵒᵖ ⥤ Type v is fully faithful, but we also have a structure
Functor.FullyFaithful which contains the data of preimages of morphisms by a functor.
example : (yoneda : C ⥤ _).FullyFaithful where
preimage {X Y} f := f.app _ (𝟙 X)
map_preimage {X Y} f := C:Type uinst✝:Category.{v, u} CX:CY:Cf:yoneda.obj X ⟶ yoneda.obj Y⊢ yoneda.map ((ConcreteCategory.hom (f.app (Opposite.op X))) (𝟙 X)) = f
C:Type uinst✝:Category.{v, u} CX:CY:Cf:yoneda.obj X ⟶ yoneda.obj Yx✝:Cᵒᵖg:(yoneda.obj X).obj x✝⊢ (ConcreteCategory.hom ((yoneda.map ((ConcreteCategory.hom (f.app (Opposite.op X))) (𝟙 X))).app x✝)).toFun g =
(ConcreteCategory.hom (f.app x✝)).toFun g
All goals completed! 🐙
More generally, if F : Cᵒᵖ ⥤ Type v is a presheaf of types and X : C,
there is a bijection between the type of natural transformations yoneda.obj X ⟶ F
and the type F.obj (.op X) of "sections" of F on X:
example {X : C} {F : Cᵒᵖ ⥤ Type v} :
(yoneda.obj X ⟶ F) ≃ F.obj (.op X) :=
yonedaEquiv
In addition to the yoneda bifunctor which is such that the target types are
in Type v (which is the universe where morphisms in the category C live),
we have a variant uliftYoneda which lift the types of morphisms into Type max v w,
and the more general variant shrinkYoneda which applies to locally w-small categories:
noncomputable example :
C ⥤ Cᵒᵖ ⥤ Type max v w :=
uliftYoneda
noncomputable example [LocallySmall.{w} C] :
C ⥤ Cᵒᵖ ⥤ Type w :=
shrinkYoneda