feat(category_theory/*): Fully faithful functors induces equivalence (#…

…9322)

Needed for AffineSchemes ≌ CommRingᵒᵖ.



Co-authored-by: erdOne <36414270+erdOne@users.noreply.github.com>

src/category_theory/equivalence.lean

@@ -549,6 +549,11 @@ noncomputable
 instance induced_functor_of_equiv {C' : Type*} (e : C' ≃ D) : is_equivalence (induced_functor e) :=
 equivalence.of_fully_faithfully_ess_surj _
 
+noncomputable
+instance fully_faithful_to_ess_image (F : C ⥤ D) [full F] [faithful F] :
+  is_equivalence F.to_ess_image :=
+of_fully_faithfully_ess_surj F.to_ess_image
+
 end equivalence
 
 end category_theory

src/category_theory/essential_image.lean

@@ -86,7 +86,7 @@ The functor `F` factorises through its essential image, where the first functor
 surjective and the second is fully faithful.
 -/
 @[simps]
-def to_ess_image_comp_essential_image_inclusion :
+def to_ess_image_comp_essential_image_inclusion (F : C ⥤ D) :
   F.to_ess_image ⋙ F.ess_image_inclusion ≅ F :=
 nat_iso.of_components (λ X, iso.refl _) (by tidy)
 
@@ -115,4 +115,17 @@ def functor.obj_preimage (Y : D) : C := (ess_surj.mem_ess_image F Y).witness
 def functor.obj_obj_preimage_iso (Y : D) : F.obj (F.obj_preimage Y) ≅ Y :=
 (ess_surj.mem_ess_image F Y).get_iso
 
+
+/-- The induced functor of a faithful functor is faithful -/
+instance faithful.to_ess_image (F : C ⥤ D) [faithful F] : faithful F.to_ess_image :=
+faithful.of_comp_iso F.to_ess_image_comp_essential_image_inclusion
+
+/-- The induced functor of a full functor is full -/
+instance full.to_ess_image (F : C ⥤ D) [full F] : full F.to_ess_image :=
+begin
+  haveI := full.of_iso F.to_ess_image_comp_essential_image_inclusion.symm,
+  exactI full.of_comp_faithful F.to_ess_image F.ess_image_inclusion
+end
+
+
 end category_theory

src/category_theory/fully_faithful.lean

@@ -206,6 +206,11 @@ lemma faithful.div_faithful (F : C ⥤ E) [faithful F] (G : D ⥤ E) [faithful G
 instance full.comp [full F] [full G] : full (F ⋙ G) :=
 { preimage := λ _ _ f, F.preimage (G.preimage f) }
 
+/-- If `F ⋙ G` is full and `G` is faithful, then `F` is full -/
+def full.of_comp_faithful [full $ F ⋙ G] [faithful G] : full F :=
+{ preimage := λ X Y f, (F ⋙ G).preimage (G.map f),
+  witness' := λ X Y f, G.map_injective ((F ⋙ G).image_preimage _) }
+
 /--
 Given a natural isomorphism between `F ⋙ H` and `G ⋙ H` for a fully faithful functor `H`, we
 can 'cancel' it to give a natural iso between `F` and `G`.