Documentation

Mathlib.CategoryTheory.Limits.Preserves.Yoneda

Yoneda preserves certain colimits #

Given a bifunctor F : J ⥤ Cᵒᵖ ⥤ Type v, we prove the isomorphism Hom(YX, colim_j F(j, -)) ≅ colim_j Hom(YX, F(j, -)), where Y is the Yoneda embedding.

We state this in two ways. One is functorial in X and stated as a natural isomorphism of functors yoneda.op ⋙ yoneda.obj (colimit F) ≅ yoneda.op ⋙ colimit (F ⋙ yoneda), and from this we deduce the more traditional preservation statement PreservesColimit F (coyoneda.obj (op (yoneda.obj X))).

The proof combines the Yoneda lemma with the fact that colimits in functor categories are computed pointwise.

See also #

There is also a relative version of this statement where F : J ⥤ Over A for some presheaf A, see CategoryTheory.Comma.Presheaf.Colimit.

source
noncomputable def CategoryTheory.yonedaYonedaColimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] [CategoryTheory.Limits.HasColimitsOfShape J (Type v₁)] [CategoryTheory.Limits.HasColimitsOfShape J (Type (max u₁ v₁))] (F : CategoryTheory.Functor J (CategoryTheory.Functor Cᵒᵖ (Type v₁))) :
CategoryTheory.yoneda.op.comp (CategoryTheory.yoneda.obj (CategoryTheory.Limits.colimit F)) ≅ CategoryTheory.yoneda.op.comp (CategoryTheory.Limits.colimit (F.comp CategoryTheory.yoneda))

Naturally in X, we have Hom(YX, colim_i Fi) ≅ colim_i Hom(YX, Fi).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem CategoryTheory.yonedaYonedaColimit_app_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] [CategoryTheory.Limits.HasColimitsOfShape J (Type v₁)] [CategoryTheory.Limits.HasColimitsOfShape J (Type (max u₁ v₁))] (F : CategoryTheory.Functor J (CategoryTheory.Functor Cᵒᵖ (Type v₁))) {X : C} :
    ((CategoryTheory.yonedaYonedaColimit F).app (Opposite.op X)).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation (F.comp CategoryTheory.yoneda) (CategoryTheory.yoneda.op.obj (Opposite.op X))).hom (CategoryTheory.Limits.colimit.post F (CategoryTheory.coyoneda.obj (Opposite.op (CategoryTheory.yoneda.obj X))))
    source
    noncomputable instance CategoryTheory.instPreservesColimitFunctorOppositeTypeObjCoyonedaOpYoneda {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] [CategoryTheory.Limits.HasColimitsOfShape J (Type v₁)] [CategoryTheory.Limits.HasColimitsOfShape J (Type (max u₁ v₁))] (F : CategoryTheory.Functor J (CategoryTheory.Functor Cᵒᵖ (Type v₁))) {X : C} :
    CategoryTheory.Limits.PreservesColimit F (CategoryTheory.coyoneda.obj (Opposite.op (CategoryTheory.yoneda.obj X)))
    Equations
    • ⋯ = ⋯