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

Author: dagurtomas

Mathlib/AlgebraicGeometry/AffineScheme.lean

@@ -71,7 +71,7 @@ def Scheme.isoSpec (X : Scheme) [IsAffine X] : X ≅ Scheme.Spec.obj (op <| Sche
 Also see `AffineScheme.of` for a typeclass version. -/
 @[simps]
 def AffineScheme.mk (X : Scheme) (_ : IsAffine X) : AffineScheme :=
-  ⟨X, mem_essImage_of_unit_isIso (adj := ΓSpec.adjunction) _⟩
+  ⟨X, ΓSpec.adjunction.mem_essImage_of_unit_isIso _⟩
 #align algebraic_geometry.AffineScheme.mk AlgebraicGeometry.AffineScheme.mk
 
 /-- Construct an affine scheme from a scheme. Also see `AffineScheme.mk` for a non-typeclass
@@ -88,7 +88,7 @@ def AffineScheme.ofHom {X Y : Scheme} [IsAffine X] [IsAffine Y] (f : X ⟶ Y) :
 
 theorem mem_Spec_essImage (X : Scheme) : X ∈ Scheme.Spec.essImage ↔ IsAffine X :=
   ⟨fun h => ⟨Functor.essImage.unit_isIso h⟩,
-    fun _ => mem_essImage_of_unit_isIso (adj := ΓSpec.adjunction) _⟩
+    fun _ => ΓSpec.adjunction.mem_essImage_of_unit_isIso _⟩
 #align algebraic_geometry.mem_Spec_ess_image AlgebraicGeometry.mem_Spec_essImage
 
 instance isAffineAffineScheme (X : AffineScheme.{u}) : IsAffine X.obj :=

Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean

@@ -171,6 +171,10 @@ lemma isIso_counit_app_iff_mem_essImage [L.Faithful] [L.Full] {X : D} :
     rw [NatTrans.isIso_app_iff_of_iso _ i.symm]
     infer_instance
 
+lemma mem_essImage_of_counit_isIso (A : D)
+    [IsIso (h.counit.app A)] : A ∈ L.essImage :=
+  ⟨R.obj A, ⟨asIso (h.counit.app A)⟩⟩
+
 lemma isIso_counit_app_of_iso [L.Faithful] [L.Full] {X : D} {Y : C} (e : X ≅ L.obj Y) :
     IsIso (h.counit.app X) :=
   (isIso_counit_app_iff_mem_essImage h).mpr ⟨Y, ⟨e.symm⟩⟩
@@ -190,6 +194,15 @@ lemma isIso_unit_app_iff_mem_essImage [R.Faithful] [R.Full] {Y : C} :
     rw [NatTrans.isIso_app_iff_of_iso _ i.symm]
     infer_instance
 
+/-- If `η_A` is an isomorphism, then `A` is in the essential image of `i`. -/
+theorem mem_essImage_of_unit_isIso (A : C)
+    [IsIso (h.unit.app A)] : A ∈ R.essImage :=
+  ⟨L.obj A, ⟨(asIso (h.unit.app A)).symm⟩⟩
+#align category_theory.mem_ess_image_of_unit_is_iso CategoryTheory.Adjunction.mem_essImage_of_unit_isIso
+
+@[deprecated (since := "2024-06-19")] alias _root_.CategoryTheory.mem_essImage_of_unit_isIso :=
+  mem_essImage_of_unit_isIso
+
 lemma isIso_unit_app_of_iso [R.Faithful] [R.Full] {X : D} {Y : C} (e : Y ≅ R.obj X) :
     IsIso (h.unit.app Y) :=
   (isIso_unit_app_iff_mem_essImage h).mpr ⟨X, ⟨e.symm⟩⟩

Mathlib/CategoryTheory/Adjunction/Reflective.lean

@@ -89,12 +89,6 @@ theorem Functor.essImage.unit_isIso [Reflective i] {A : C} (h : A ∈ i.essImage
   rwa [isIso_unit_app_iff_mem_essImage]
 #align category_theory.functor.ess_image.unit_is_iso CategoryTheory.Functor.essImage.unit_isIso
 
-/-- If `η_A` is an isomorphism, then `A` is in the essential image of `i`. -/
-theorem mem_essImage_of_unit_isIso {L : C ⥤ D} (adj : L ⊣ i) (A : C)
-    [IsIso (adj.unit.app A)] : A ∈ i.essImage :=
-  ⟨L.obj A, ⟨(asIso (adj.unit.app A)).symm⟩⟩
-#align category_theory.mem_ess_image_of_unit_is_iso CategoryTheory.mem_essImage_of_unit_isIso
-
 /-- If `η_A` is a split monomorphism, then `A` is in the reflective subcategory. -/
 theorem mem_essImage_of_unit_isSplitMono [Reflective i] {A : C}
     [IsSplitMono ((reflectorAdjunction i).unit.app A)] : A ∈ i.essImage := by
@@ -106,7 +100,7 @@ theorem mem_essImage_of_unit_isSplitMono [Reflective i] {A : C}
     rw [show retraction _ ≫ η.app A = _ from η.naturality (retraction (η.app A))]
     apply epi_comp (η.app (i.obj ((reflector i).obj A)))
   haveI := isIso_of_epi_of_isSplitMono (η.app A)
-  exact mem_essImage_of_unit_isIso (reflectorAdjunction i) A
+  exact (reflectorAdjunction i).mem_essImage_of_unit_isIso A
 #align category_theory.mem_ess_image_of_unit_is_split_mono CategoryTheory.mem_essImage_of_unit_isSplitMono
 
 /-- Composition of reflective functors. -/
@@ -228,4 +222,63 @@ def equivEssImageOfReflective [Reflective i] : D ≌ i.EssImageSubcategory where
     aesop_cat
 #align category_theory.equiv_ess_image_of_reflective CategoryTheory.equivEssImageOfReflective
 
+/--
+A functor is *coreflective*, or *a coreflective inclusion*, if it is fully faithful and left
+adjoint.
+-/
+class Coreflective (L : C ⥤ D) extends L.Full, L.Faithful where
+  /-- a choice of a right adjoint to `L` -/
+  R : D ⥤ C
+  /-- `L` is a left adjoint -/
+  adj : L ⊣ R
+
+variable (j : C ⥤ D)
+
+/-- The coreflector `D ⥤ C` when `L : C ⥤ D` is coreflective. -/
+def coreflector [Coreflective j] : D ⥤ C := Coreflective.R (L := j)
+
+/-- The adjunction `j ⊣ coreflector j` when `j` is coreflective. -/
+def coreflectorAdjunction [Coreflective j] : j ⊣ coreflector j := Coreflective.adj
+
+instance [Coreflective j] : j.IsLeftAdjoint := ⟨_, ⟨coreflectorAdjunction j⟩⟩
+
+instance [Coreflective j] : (coreflector j).IsRightAdjoint := ⟨_, ⟨coreflectorAdjunction j⟩⟩
+
+/-- A coreflective functor is fully faithful. -/
+def Functor.fullyFaithfulOfCoreflective [Coreflective j] : j.FullyFaithful :=
+  (coreflectorAdjunction j).fullyFaithfulLOfIsIsoUnit
+
+lemma counit_obj_eq_map_counit [Coreflective j] (X : D) :
+    (coreflectorAdjunction j).counit.app (j.obj ((coreflector j).obj X)) =
+      j.map ((coreflector j).map ((coreflectorAdjunction j).counit.app X)) := by
+  rw [← cancel_epi (j.map ((coreflectorAdjunction j).unit.app ((coreflector j).obj X))),
+    ← j.map_comp]
+  simp
+
+example [Coreflective j] {B : C} : IsIso ((coreflectorAdjunction j).counit.app (j.obj B)) :=
+  inferInstance
+
+variable {j}
+
+lemma Functor.essImage.counit_isIso [Coreflective j] {A : D} (h : A ∈ j.essImage) :
+    IsIso ((coreflectorAdjunction j).counit.app A) := by
+  rwa [isIso_counit_app_iff_mem_essImage]
+
+lemma mem_essImage_of_counit_isSplitEpi [Coreflective j] {A : D}
+    [IsSplitEpi ((coreflectorAdjunction j).counit.app A)] : A ∈ j.essImage := by
+  let ε : coreflector j ⋙ j ⟶ 𝟭 D  := (coreflectorAdjunction j).counit
+  haveI : IsIso (ε.app (j.obj ((coreflector j).obj A))) :=
+    Functor.essImage.counit_isIso ((j.obj_mem_essImage _))
+  have : Mono (ε.app A) := by
+    refine @mono_of_mono _ _ _ _ _ (ε.app A) (section_ (ε.app A)) ?_
+    rw [show ε.app A ≫ section_ _ = _ from (ε.naturality (section_ (ε.app A))).symm]
+    apply mono_comp _ (ε.app (j.obj ((coreflector j).obj A)))
+  haveI := isIso_of_mono_of_isSplitEpi (ε.app A)
+  exact (coreflectorAdjunction j).mem_essImage_of_counit_isIso A
+
+instance Coreflective.comp (F : C ⥤ D) (G : D ⥤ E) [Coreflective F] [Coreflective G] :
+    Coreflective (F ⋙ G) where
+  R := coreflector G ⋙ coreflector F
+  adj := (coreflectorAdjunction F).comp (coreflectorAdjunction G)
+
 end CategoryTheory