Commit 2026-06-30 09:15 967fd0f0

View on Github →

feat(CategoryTheory): add shrinkCoyoneda (#41150) Add API for the co-Yoneda embedding of locally small categories, dual to the existing shrinkYoneda.

Estimated changes

Modified Mathlib/CategoryTheory/ShrinkYoneda.lean

added theorem CategoryTheory.map_shrinkCoyonedaEquiv

added def CategoryTheory.shrinkCoyonedaCorepresentableBy

added theorem CategoryTheory.shrinkCoyonedaEquiv_comp

added theorem CategoryTheory.shrinkCoyonedaEquiv_naturality

added theorem CategoryTheory.shrinkCoyonedaEquiv_shrinkCoyoneda_map

added theorem CategoryTheory.shrinkCoyonedaEquiv_symm_app_shrinkCoyonedaObjObjEquiv_symm

added theorem CategoryTheory.shrinkCoyonedaEquiv_symm_map

added def CategoryTheory.shrinkCoyonedaIsoCoyoneda

added theorem CategoryTheory.shrinkCoyonedaObjObjEquiv_map_app

added theorem CategoryTheory.shrinkCoyonedaObjObjEquiv_obj_map

added theorem CategoryTheory.shrinkCoyonedaObjObjEquiv_symm_comp

added def CategoryTheory.shrinkCoyonedaUliftFunctorIso

added theorem CategoryTheory.shrinkCoyoneda_map

added theorem CategoryTheory.shrinkCoyoneda_map_app_shrinkCoyonedaObjObjEquiv_symm

added theorem CategoryTheory.shrinkCoyoneda_obj

added theorem CategoryTheory.shrinkCoyoneda_obj_map_shrinkCoyonedaObjObjEquiv_symm