Commit 2024-05-01 00:06 dc034b59

View on Github →

feat(CategoryTheory/Yoneda): dualize yoneda lemma (#12041) Refactors yonedaLemma. Also dualizes all definitions and results related to yonedaLemma to obtain coyonedaLemma and friends.

Estimated changes

Modified Mathlib/CategoryTheory/Closed/FunctorCategory.lean

Modified Mathlib/CategoryTheory/Elements.lean

Modified Mathlib/CategoryTheory/Limits/FunctorCategory.lean

Modified Mathlib/CategoryTheory/Limits/Presheaf.lean

Modified Mathlib/CategoryTheory/Sites/IsSheafFor.lean

Modified Mathlib/CategoryTheory/Subobject/Lattice.lean

Modified Mathlib/CategoryTheory/Yoneda.lean

added def CategoryTheory.coyonedaCompUliftFunctorEquiv

added def CategoryTheory.coyonedaEquiv

added theorem CategoryTheory.coyonedaEquiv_apply

added theorem CategoryTheory.coyonedaEquiv_comp

added theorem CategoryTheory.coyonedaEquiv_coyoneda_map

added theorem CategoryTheory.coyonedaEquiv_naturality

added theorem CategoryTheory.coyonedaEquiv_symm_app_apply

added theorem CategoryTheory.coyonedaEquiv_symm_map

added def CategoryTheory.coyonedaEvaluation

added theorem CategoryTheory.coyonedaEvaluation_map_down

added def CategoryTheory.coyonedaLemma

added def CategoryTheory.coyonedaPairing

added theorem CategoryTheory.coyonedaPairingExt

added theorem CategoryTheory.coyonedaPairing_map

added def CategoryTheory.curriedCoyonedaLemma'

added def CategoryTheory.curriedCoyonedaLemma

added theorem CategoryTheory.isIso_of_coyoneda_map_bijective

modified def CategoryTheory.yonedaEquiv

deleted theorem CategoryTheory.yonedaEquiv_comp'

modified theorem CategoryTheory.yonedaEquiv_naturality

modified def CategoryTheory.yonedaLemma

deleted def CategoryTheory.yonedaSections

deleted def CategoryTheory.yonedaSectionsSmall

deleted theorem CategoryTheory.yonedaSectionsSmall_hom

deleted theorem CategoryTheory.yonedaSectionsSmall_inv_app_apply

Modified Mathlib/Logic/Equiv/Basic.lean

added theorem Equiv.ulift_symm_down