Commit 2026-03-08 20:06 fd7333f6

View on Github →

chore(CategoryTheory/ShrinkYoneda): shrinkYoneda.obj X is representable (#36292)

Estimated changes

Modified Mathlib/CategoryTheory/ShrinkYoneda.lean

added def CategoryTheory.FunctorToTypes.shrinkCompUliftFunctorIso

added def CategoryTheory.shrinkYonedaRepresentableBy

added def CategoryTheory.shrinkYonedaUliftFunctorIso

Modified Mathlib/CategoryTheory/Yoneda.lean

added def CategoryTheory.Functor.CorepresentableBy.id

added theorem CategoryTheory.Functor.CorepresentableBy.id_homEquiv_apply

added theorem CategoryTheory.Functor.CorepresentableBy.id_homEquiv_symm_apply

modified theorem CategoryTheory.corepresentable_of_natIso

modified theorem CategoryTheory.isRepresentable_of_natIso