Commit 2023-02-22 19:59 484f3e9f

View on Github →

feat: port CategoryTheory.Adjunction.FullyFaithful (#2418)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Adjunction/Basic.lean

modified theorem CategoryTheory.Adjunction.left_triangle

modified theorem CategoryTheory.Adjunction.right_triangle

Created Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean

added def CategoryTheory.Adjunction.restrictFullyFaithful

added theorem CategoryTheory.L_faithful_of_unit_isIso

added theorem CategoryTheory.R_faithful_of_counit_isIso

added theorem CategoryTheory.inv_counit_map

added theorem CategoryTheory.inv_map_unit