Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-19 03:04 2a48c690

View on Github →

feat(category_theory/yoneda): develop API for representable functors (#7962) Dualises and extends API for representable functors which was previously pretty minimal

Estimated changes

Modified src/category_theory/sites/canonical.lean

modified theorem category_theory.sheaf.is_sheaf_of_representable

Modified src/category_theory/sites/sheaf.lean

Modified src/category_theory/yoneda.lean

added theorem category_theory.corepresentable_of_nat_iso

deleted def category_theory.coyoneda.iso_comp_punit

added def category_theory.coyoneda.punit_iso

added theorem category_theory.functor.corepr_w_app_hom

added theorem category_theory.functor.repr_w_app_hom

added theorem category_theory.functor.repr_w_hom

added theorem category_theory.representable_of_nat_iso

modified def category_theory.yoneda_sections