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} [Category.{v, u} C] {J : Type v} [SmallCategory J] {A : Functor Cᵒᵖ (Type v)} (F : Functor J (Over A)) : (toOver yoneda A).op.comp (yoneda.obj (Limits.colimit F)) ≅ (toOver yoneda A).op.comp (Limits.colimit (F.comp 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.