Commit 2023-02-24 18:15 ffc42486

View on Github →

feat: port CategoryTheory.Adjunction.Reflective (#2467)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Adjunction/Reflective.lean

added theorem CategoryTheory.Functor.essImage.unit_isIso

added def CategoryTheory.equivEssImageOfReflective

added def CategoryTheory.equivEssImageOfReflective_counitIso_app

added theorem CategoryTheory.equivEssImageOfReflective_map_counitIso_app_hom

added theorem CategoryTheory.equivEssImageOfReflective_map_counitIso_app_inv

added theorem CategoryTheory.mem_essImage_of_unit_isIso

added theorem CategoryTheory.mem_essImage_of_unit_isSplitMono

added def CategoryTheory.unitCompPartialBijective

added def CategoryTheory.unitCompPartialBijectiveAux

added theorem CategoryTheory.unitCompPartialBijectiveAux_symm_apply

added theorem CategoryTheory.unitCompPartialBijective_natural

added theorem CategoryTheory.unitCompPartialBijective_symm_apply

added theorem CategoryTheory.unitCompPartialBijective_symm_natural

added theorem CategoryTheory.unit_obj_eq_map_unit