Relative Yoneda preserves certain colimits

In this file we turn the statement yonedaYonedaColimit from CategoryTheory.Limits.Preserves.Yoneda from a functor F : J ⥤ Cᵒᵖ ⥤ Type v into a statement about families of presheaves over A, i.e., functors F : J ⥤ Over A.

noncomputable def CategoryTheory.CostructuredArrow.toOverCompYonedaColimit {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type v} [CategoryTheory.SmallCategory J] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (F : CategoryTheory.Functor J (CategoryTheory.Over A)) : (CategoryTheory.CostructuredArrow.toOver CategoryTheory.yoneda A).op.comp (CategoryTheory.yoneda.obj (CategoryTheory.Limits.colimit F)) ≅ (CategoryTheory.CostructuredArrow.toOver CategoryTheory.yoneda A).op.comp (CategoryTheory.Limits.colimit (F.comp CategoryTheory.yoneda))

Naturally in X, we have Hom(YX, colim_i Fi) ≅ colim_i Hom(YX, Fi), where Y is the "Yoneda embedding" CostructuredArrow.toOver yoneda A. This is a relative version of yonedaYonedaColimit.

Equations

• One or more equations did not get rendered due to their size.