Commit 2024-06-19 18:17 feba7083

View on Github →

chore(CategoryTheory/Adjunction): dualize some of the API for reflective functors (#13948)

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

Modified Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean

added theorem CategoryTheory.Adjunction.mem_essImage_of_counit_isIso

added theorem CategoryTheory.Adjunction.mem_essImage_of_unit_isIso

Modified Mathlib/CategoryTheory/Adjunction/Reflective.lean

added theorem CategoryTheory.Functor.essImage.counit_isIso

added def CategoryTheory.Functor.fullyFaithfulOfCoreflective

added def CategoryTheory.coreflector

added def CategoryTheory.coreflectorAdjunction

added theorem CategoryTheory.counit_obj_eq_map_counit

added theorem CategoryTheory.mem_essImage_of_counit_isSplitEpi

deleted theorem CategoryTheory.mem_essImage_of_unit_isIso