Commit 2026-03-03 13:11 0b536267

View on Github →

feat(CategoryTheory/Elements): functors to types are colimits of corepresentable functors (#35759) If F : C ⥤ Type w and C is locally w-small, then F identifies a colimit of corepresentable functors, which we also state as an isomorphism with the composition shrinkYoneda ⋙ (Functor.whiskeringLeft _ _ _).obj (CategoryOfElements.π F).op ⋙ colim.

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Presheaf.lean

added theorem CategoryTheory.Functor.Elements.shrinkYonedaCompWhiskeringLeftObjπCompColimIso_inv_app_apply

added theorem CategoryTheory.Functor.Elements.shrinkYoneda_map_app_coconeπOpCompShrinkYonedaObj_ι_app