Commit 2023-02-20 11:53 189fab8c

View on Github →

feat port/CategoryTheory.Yoneda (#2299)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Yoneda.lean

added theorem CategoryTheory.Coyoneda.isIso

added theorem CategoryTheory.Coyoneda.naturality

added def CategoryTheory.Coyoneda.objOpOp

added def CategoryTheory.Coyoneda.punitIso

added theorem CategoryTheory.Functor.coreprW_app_hom

added theorem CategoryTheory.Functor.reprW_app_hom

added theorem CategoryTheory.Functor.reprW_hom

added def CategoryTheory.Yoneda.ext

added theorem CategoryTheory.Yoneda.isIso

added theorem CategoryTheory.Yoneda.naturality

added theorem CategoryTheory.Yoneda.obj_map_id

added theorem CategoryTheory.corepresentable_of_nat_iso

added def CategoryTheory.coyoneda

added def CategoryTheory.curriedYonedaLemma'

added def CategoryTheory.curriedYonedaLemma

added theorem CategoryTheory.representable_of_nat_iso

added def CategoryTheory.yoneda

added def CategoryTheory.yonedaEquiv

added theorem CategoryTheory.yonedaEquiv_apply

added theorem CategoryTheory.yonedaEquiv_naturality

added theorem CategoryTheory.yonedaEquiv_symm_app_apply

added def CategoryTheory.yonedaEvaluation

added theorem CategoryTheory.yonedaEvaluation_map_down

added def CategoryTheory.yonedaLemma

added def CategoryTheory.yonedaPairing

added theorem CategoryTheory.yonedaPairing_map

added def CategoryTheory.yonedaSections

added def CategoryTheory.yonedaSectionsSmall

added theorem CategoryTheory.yonedaSectionsSmall_hom

added theorem CategoryTheory.yonedaSectionsSmall_inv_app_apply