Commit 2021-07-02 19:46 9e9dfc26

View on Github →

feat(category_theory/adjunction/fully_faithful): Converses to unit_is_iso_of_L_fully_faithful and counit_is_iso_of_R_fully_faithful (#8181) Add a converse to unit_is_iso_of_L_fully_faithful and to counit_is_iso_of_R_fully_faithful

Estimated changes

Modified src/category_theory/adjunction/fully_faithful.lean

added theorem category_theory.L_faithful_of_unit_is_iso

added def category_theory.L_full_of_unit_is_iso

added theorem category_theory.R_faithful_of_counit_is_iso

added def category_theory.R_full_of_counit_is_iso

added theorem category_theory.inv_counit_map

added theorem category_theory.inv_map_unit