Commit 2020-10-02 18:01 2634c1b5

View on Github →

feat(category_theory/cones): map_cone_inv as an equivalence (#4253) When G is an equivalence, we have G.map_cone_inv : cone (F ⋙ G) → cone F, and that this is an inverse to G.map_cone, but not quite that these constitute an equivalence of categories. This PR fixes that.

Estimated changes

Modified src/category_theory/equivalence.lean

added theorem category_theory.equivalence.counit_app_functor

deleted theorem category_theory.equivalence.counit_functor

added theorem category_theory.equivalence.counit_inv_app_functor

deleted theorem category_theory.equivalence.functor_unit

deleted theorem category_theory.equivalence.inverse_counit

added theorem category_theory.equivalence.unit_app_inverse

added theorem category_theory.equivalence.unit_inv_app_inverse

deleted theorem category_theory.equivalence.unit_inverse

Modified src/category_theory/limits/cones.lean

added def category_theory.functor.map_cocone_inv

added def category_theory.functor.map_cocone_inv_map_cocone

added def category_theory.functor.map_cocone_map_cocone_inv

added def category_theory.limits.cocones.functoriality_equivalence

added def category_theory.limits.cones.functoriality_equivalence

Modified src/category_theory/limits/limits.lean

Modified src/category_theory/monoidal/transport.lean