feat(category_theory): essential image of a functor (#5352)

Define essential image of a functor as a predicate and use it to re-express essential surjectivity.
Construct the essential image as a subcategory of the target and use it to factorise an arbitrary functor into a fully faithful functor and an essentially surjective functor.
Also shuffles the import hierarchy a little so that essential image can import full subcategories.

src/algebra/category/Group/Z_Module_equivalence.lean

@@ -29,7 +29,7 @@ instance : full (forget₂ (Module ℤ) AddCommGroup.{u}) :=
 
 /-- The forgetful functor from `ℤ` modules to `AddCommGroup` is essentially surjective. -/
 instance : ess_surj (forget₂ (Module ℤ) AddCommGroup.{u}) :=
-{ obj_preimage := λ A, ⟨Module.of ℤ A, ⟨{ hom := 𝟙 A, inv := 𝟙 A }⟩⟩}
+{ mem_ess_image := λ A, ⟨Module.of ℤ A, ⟨{ hom := 𝟙 A, inv := 𝟙 A }⟩⟩}
 
 noncomputable instance : is_equivalence (forget₂ (Module ℤ) AddCommGroup.{u}) :=
 equivalence_of_fully_faithfully_ess_surj (forget₂ (Module ℤ) AddCommGroup)

src/category_theory/Fintype.lean

@@ -81,7 +81,7 @@ def incl : skeleton ⥤ Fintype :=
 instance : full incl := { preimage := λ _ _ f, f }
 instance : faithful incl := {}
 instance : ess_surj incl :=
-{ obj_preimage := λ X,
+{ mem_ess_image := λ X,
   let F := trunc.out (fintype.equiv_fin X) in
   ⟨fintype.card X, ⟨⟨F.symm, F, F.self_comp_symm, F.symm_comp_self⟩⟩⟩ }
 

src/category_theory/concrete_category/basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Johannes Hölzl, Reid Barton, Sean Leather, Yury Kudryashov
 -/
 import category_theory.types
-import category_theory.full_subcategory
+import category_theory.epi_mono
 
 /-!
 # Concrete categories

src/category_theory/equivalence.lean

@@ -5,6 +5,7 @@ Authors: Tim Baumann, Stephen Morgan, Scott Morrison, Floris van Doorn
 -/
 import category_theory.fully_faithful
 import category_theory.whiskering
+import category_theory.essential_image
 import tactic.slice
 
 /-!
@@ -489,29 +490,6 @@ eq_of_inv_eq_inv (functor_unit_comp _ _)
 
 end is_equivalence
 
-/--
-A functor `F : C ⥤ D` is essentially surjective if for every `d : D`, there is some `c : C`
-so `F.obj c ≅ D`.
-
-See https://stacks.math.columbia.edu/tag/001C.
--/
-class ess_surj (F : C ⥤ D) : Prop :=
-(obj_preimage [] (d : D) : ∃ c, nonempty (F.obj c ≅ d))
-
-namespace functor
-/-- Given an essentially surjective functor, we can find a preimage for every object `d` in the
-    codomain. Applying the functor to this preimage will yield an object isomorphic to `d`, see
-    `fun_obj_preimage_iso`. -/
-noncomputable def obj_preimage (F : C ⥤ D) [sF : ess_surj F] (d : D) : C :=
-classical.some (ess_surj.obj_preimage F d)
-/-- Applying an essentially surjective functor to a preimage of `d` yields an object that is
-    isomorphic to `d`. -/
-noncomputable def fun_obj_preimage_iso (F : C ⥤ D) [sF : ess_surj F] (d : D) :
-  F.obj (F.obj_preimage d) ≅ d :=
-classical.choice (classical.some_spec (ess_surj.obj_preimage F d))
-
-end functor
-
 namespace equivalence
 
 /--
@@ -548,7 +526,7 @@ instance full_of_equivalence (F : C ⥤ D) [is_equivalence F] : full F :=
 
 @[simps] private noncomputable def equivalence_inverse (F : C ⥤ D) [full F] [faithful F] [ess_surj F] : D ⥤ C :=
 { obj  := λ X, F.obj_preimage X,
-  map := λ X Y f, F.preimage ((F.fun_obj_preimage_iso X).hom ≫ f ≫ (F.fun_obj_preimage_iso Y).inv),
+  map := λ X Y f, F.preimage ((F.obj_obj_preimage_iso X).hom ≫ f ≫ (F.obj_obj_preimage_iso Y).inv),
   map_id' := λ X, begin apply F.map_injective, tidy end,
   map_comp' := λ X Y Z f g, by apply F.map_injective; simp }
 
@@ -561,14 +539,16 @@ noncomputable def equivalence_of_fully_faithfully_ess_surj
   (F : C ⥤ D) [full F] [faithful F] [ess_surj F] : is_equivalence F :=
 is_equivalence.mk (equivalence_inverse F)
   (nat_iso.of_components
-    (λ X, (preimage_iso $ F.fun_obj_preimage_iso $ F.obj X).symm)
+    (λ X, (preimage_iso $ F.obj_obj_preimage_iso $ F.obj X).symm)
     (λ X Y f, by { apply F.map_injective, obviously }))
-  (nat_iso.of_components F.fun_obj_preimage_iso (by tidy))
+  (nat_iso.of_components F.obj_obj_preimage_iso (by tidy))
 
-@[simp] lemma functor_map_inj_iff (e : C ≌ D) {X Y : C} (f g : X ⟶ Y) : e.functor.map f = e.functor.map g ↔ f = g :=
+@[simp] lemma functor_map_inj_iff (e : C ≌ D) {X Y : C} (f g : X ⟶ Y) :
+  e.functor.map f = e.functor.map g ↔ f = g :=
 ⟨λ h, e.functor.map_injective h, λ h, h ▸ rfl⟩
 
-@[simp] lemma inverse_map_inj_iff (e : C ≌ D) {X Y : D} (f g : X ⟶ Y) : e.inverse.map f = e.inverse.map g ↔ f = g :=
+@[simp] lemma inverse_map_inj_iff (e : C ≌ D) {X Y : D} (f g : X ⟶ Y) :
+  e.inverse.map f = e.inverse.map g ↔ f = g :=
 functor_map_inj_iff e.symm f g
 
 end equivalence

src/category_theory/essential_image.lean

@@ -0,0 +1,118 @@
+/-
+Copyright (c) 2020 Bhavik Mehta. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bhavik Mehta
+-/
+import category_theory.natural_isomorphism
+import category_theory.full_subcategory
+
+/-!
+# Essential image of a functor
+
+The essential image `ess_image` of a functor consists of the objects in the target category which
+are isomorphic to an object in the image of the object function.
+This, for instance, allows us to talk about objects belonging to a subcategory expressed as a
+functor rather than a subtype, preserving the principle of equivalence. For example this lets us
+define exponential ideals.
+
+The essential image can also be seen as a subcategory of the target category, and witnesses that
+a functor decomposes into a essentially surjective functor and a fully faithful functor.
+(TODO: show that this decomposition forms an orthogonal factorisation system).
+-/
+universes v₁ v₂ u₁ u₂
+
+noncomputable theory
+
+namespace category_theory
+
+variables {C : Type u₁} {D : Type u₂} [category.{v₁} C] [category.{v₂} D] {F : C ⥤ D}
+
+namespace functor
+
+/--
+The essential image of a functor `F` consists of those objects in the target category which are
+isomorphic to an object in the image of the function `F.obj`. In other words, this is the closure
+under isomorphism of the function `F.obj`.
+This is the "non-evil" way of describing the image of a functor.
+-/
+def ess_image (F : C ⥤ D) : set D := λ Y, ∃ (X : C), nonempty (F.obj X ≅ Y)
+
+/-- Get the witnessing object that `Y` is in the subcategory given by `F`. -/
+def ess_image.witness {Y : D} (h : Y ∈ F.ess_image) : C := h.some
+
+/-- Extract the isomorphism between `F.obj h.witness` and `Y` itself. -/
+def ess_image.get_iso {Y : D} (h : Y ∈ F.ess_image) : F.obj h.witness ≅ Y :=
+classical.choice h.some_spec
+
+/-- Being in the essential image is a "hygenic" property: it is preserved under isomorphism. -/
+lemma ess_image.of_iso {Y Y' : D} (h : Y ≅ Y') (hY : Y ∈ ess_image F) :
+  Y' ∈ ess_image F :=
+hY.imp (λ B, nonempty.map (≪≫ h))
+
+/--
+If `Y` is in the essential image of `F` then it is in the essential image of `F'` as long as
+`F ≅ F'`.
+-/
+lemma ess_image.of_nat_iso {F' : C ⥤ D} (h : F ≅ F') {Y : D} (hY : Y ∈ ess_image F) :
+  Y ∈ ess_image F' :=
+hY.imp (λ X, nonempty.map (λ t, h.symm.app X ≪≫ t))
+
+/-- Isomorphic functors have equal essential images. -/
+lemma ess_image_eq_of_nat_iso {F' : C ⥤ D} (h : F ≅ F') :
+  ess_image F = ess_image F' :=
+set.ext $ λ A, ⟨ess_image.of_nat_iso h, ess_image.of_nat_iso h.symm⟩
+
+/-- An object in the image is in the essential image. -/
+lemma obj_mem_ess_image (F : D ⥤ C) (Y : D) : F.obj Y ∈ ess_image F := ⟨Y, ⟨iso.refl _⟩⟩
+
+instance : category F.ess_image := category_theory.full_subcategory _
+
+/-- The essential image as a subcategory has a fully faithful inclusion into the target category. -/
+@[derive [full, faithful], simps {rhs_md := semireducible}]
+def ess_image_inclusion (F : C ⥤ D) : F.ess_image ⥤ D :=
+full_subcategory_inclusion _
+
+/--
+Given a functor `F : C ⥤ D`, we have an (essentially surjective) functor from `C` to the essential
+image of `F`.
+-/
+@[simps]
+def to_ess_image (F : C ⥤ D) : C ⥤ F.ess_image :=
+{ obj := λ X, ⟨_, obj_mem_ess_image _ X⟩,
+  map := λ X Y f, (ess_image_inclusion F).preimage (F.map f) }
+
+/--
+The functor `F` factorises through its essential image, where the first functor is essentially
+surjective and the second is fully faithful.
+-/
+@[simps {rhs_md := semireducible}]
+def to_ess_image_comp_essential_image_inclusion :
+  F.to_ess_image ⋙ F.ess_image_inclusion ≅ F :=
+nat_iso.of_components (λ X, iso.refl _) (by tidy)
+
+end functor
+
+/--
+A functor `F : C ⥤ D` is essentially surjective if every object of `D` is in the essential image
+of `F`. In other words, for every `Y : D`, there is some `X : C` with `F.obj X ≅ Y`.
+
+See https://stacks.math.columbia.edu/tag/001C.
+-/
+class ess_surj (F : C ⥤ D) : Prop :=
+(mem_ess_image [] (Y : D) : Y ∈ F.ess_image)
+
+instance : ess_surj F.to_ess_image :=
+{ mem_ess_image := λ ⟨Y, hY⟩, ⟨_, ⟨⟨_, _, hY.get_iso.hom_inv_id, hY.get_iso.inv_hom_id⟩⟩⟩ }
+
+variables (F) [ess_surj F]
+
+/-- Given an essentially surjective functor, we can find a preimage for every object `Y` in the
+    codomain. Applying the functor to this preimage will yield an object isomorphic to `Y`, see
+    `obj_obj_preimage_iso`. -/
+def functor.obj_preimage (Y : D) : C := (ess_surj.mem_ess_image F Y).witness
+/-- Applying an essentially surjective functor to a preimage of `Y` yields an object that is
+    isomorphic to `Y`. -/
+def functor.obj_obj_preimage_iso (Y : D) : F.obj (F.obj_preimage Y) ≅ Y :=
+(ess_surj.mem_ess_image F Y).get_iso
+
+end category_theory

src/category_theory/full_subcategory.lean

@@ -3,7 +3,7 @@ Copyright (c) 2017 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Reid Barton
 -/
-import category_theory.groupoid
+import category_theory.fully_faithful
 
 namespace category_theory
 
@@ -74,12 +74,6 @@ instance induced_category.faithful : faithful (induced_functor F) := {}
 
 end induced
 
-instance induced_category.groupoid {C : Type u₁} (D : Type u₂) [groupoid.{v} D] (F : C → D) :
-   groupoid.{v} (induced_category D F) :=
-{ inv       := λ X Y f, groupoid.inv f,
-  inv_comp' := λ X Y f, groupoid.inv_comp f,
-  comp_inv' := λ X Y f, groupoid.comp_inv f,
-  .. induced_category.category F }
 
 section full_subcategory
 /- A full subcategory is the special case of an induced category with F = subtype.val. -/

src/category_theory/groupoid.lean

@@ -71,4 +71,11 @@ end
 
 end
 
+instance induced_category.groupoid {C : Type u} (D : Type u₂) [groupoid.{v} D] (F : C → D) :
+   groupoid.{v} (induced_category D F) :=
+{ inv       := λ X Y f, groupoid.inv f,
+  inv_comp' := λ X Y f, groupoid.inv_comp f,
+  comp_inv' := λ X Y f, groupoid.comp_inv f,
+  .. induced_category.category F }
+
 end category_theory

src/category_theory/limits/shapes/normal_mono.lean

@@ -11,9 +11,9 @@ import category_theory.limits.shapes.kernels
 
 A normal monomorphism is a morphism that is the kernel of some other morphism.
 
-We give the construction `normal_mono → regular_mono` (`category_theory.normal_mono.regular_mono`) 
-as well as the dual construction for normal epimorphisms. We show equivalences reflect normal 
-monomorphisms (`category_theory.equivalence_reflects_normal_mono`), and that the pullback of a 
+We give the construction `normal_mono → regular_mono` (`category_theory.normal_mono.regular_mono`)
+as well as the dual construction for normal epimorphisms. We show equivalences reflect normal
+monomorphisms (`category_theory.equivalence_reflects_normal_mono`), and that the pullback of a
 normal monomorphism is normal (`category_theory.normal_of_is_pullback_snd_of_normal`).
 -/
 
@@ -46,13 +46,13 @@ def equivalence_reflects_normal_mono {D : Type u₂} [category.{v₁} D] [has_ze
   (F : C ⥤ D) [is_equivalence F] {X Y : C} {f : X ⟶ Y} (hf : normal_mono (F.map f)) :
   normal_mono f :=
 { Z := F.obj_preimage hf.Z,
-  g := full.preimage (hf.g ≫ (F.fun_obj_preimage_iso hf.Z).inv),
+  g := full.preimage (hf.g ≫ (F.obj_obj_preimage_iso hf.Z).inv),
   w := faithful.map_injective F $ by simp [reassoc_of hf.w],
   is_limit := reflects_limit.reflects $
     is_limit.of_cone_equiv (cones.postcompose_equivalence (comp_nat_iso F)) $
       is_limit.of_iso_limit
         (by exact is_limit.of_iso_limit
-          (is_kernel.of_comp_iso _ _ (F.fun_obj_preimage_iso hf.Z) (by simp) hf.is_limit)
+          (is_kernel.of_comp_iso _ _ (F.obj_obj_preimage_iso hf.Z) (by simp) hf.is_limit)
           (of_ι_congr (category.comp_id _).symm)) (iso_of_ι _).symm }
 
 end
@@ -125,13 +125,13 @@ def equivalence_reflects_normal_epi {D : Type u₂} [category.{v₁} D] [has_zer
   (F : C ⥤ D) [is_equivalence F] {X Y : C} {f : X ⟶ Y} (hf : normal_epi (F.map f)) :
   normal_epi f :=
 { W := F.obj_preimage hf.W,
-  g := full.preimage ((F.fun_obj_preimage_iso hf.W).hom ≫ hf.g),
+  g := full.preimage ((F.obj_obj_preimage_iso hf.W).hom ≫ hf.g),
   w := faithful.map_injective F $ by simp [hf.w],
   is_colimit := reflects_colimit.reflects $
     is_colimit.of_cocone_equiv (cocones.precompose_equivalence (comp_nat_iso F).symm) $
       is_colimit.of_iso_colimit
         (by exact is_colimit.of_iso_colimit
-          (is_cokernel.of_iso_comp _ _ (F.fun_obj_preimage_iso hf.W).symm (by simp) hf.is_colimit)
+          (is_cokernel.of_iso_comp _ _ (F.obj_obj_preimage_iso hf.W).symm (by simp) hf.is_colimit)
             (of_π_congr (category.id_comp _).symm))
         (iso_of_π _).symm }
 

src/topology/category/Compactum.lean

@@ -433,7 +433,7 @@ noncomputable def iso_of_topological_space {D : CompHaus} :
 
 /-- The functor Compactum_to_CompHaus is essentially surjective. -/
 lemma ess_surj : ess_surj Compactum_to_CompHaus :=
-{ obj_preimage := λ X, ⟨Compactum.of_topological_space X, ⟨iso_of_topological_space⟩⟩ }
+{ mem_ess_image := λ X, ⟨Compactum.of_topological_space X, ⟨iso_of_topological_space⟩⟩ }
 
 /-- The functor Compactum_to_CompHaus is an equivalence of categories. -/
 noncomputable def is_equivalence : is_equivalence Compactum_to_CompHaus :=