/-
Copyright (c) 2020 Bhavik Mehta. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Bhavik Mehta
Ported by: Joël Riou

! This file was ported from Lean 3 source module category_theory.essential_image
! leanprover-community/mathlib commit 550b58538991c8977703fdeb7c9d51a5aa27df11
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.CategoryTheory.NatIso
import Mathlib.CategoryTheory.FullSubcategory

/-!
# Essential image of a functor

The essential image `essImage` 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).
-/


universe v₁ v₂ u₁ u₂

noncomputable section

namespace CategoryTheory

variable {
C: Type u₁
C : 
Type u₁: Type (u₁+1)
Type u₁} {
D: Type u₂
D : 
Type u₂: Type (u₂+1)
Type u₂} [
Category: Type ?u.698 → Type (max?u.698(v₁+1))
Category.{v₁} 
C: Type u₁
C] [
Category: Type ?u.192 → Type (max?u.192(v₂+1))
Category.{v₂} 
D: Type u₂
D] {
F: C ⥤ D
F : 
C: Type u₁
C ⥤ 
D: Type u₂
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 
essImage: C ⥤ D → Set D
essImage (
F: C ⥤ D
F : 
C: Type u₁
C ⥤ 
D: Type u₂
D) : 
Set: Type ?u.70 → Type ?u.70
Set 
D: Type u₂
D := fun 
Y: ?m.75
Y => ∃ 
X: C
X : 
C: Type u₁
C, 
Nonempty: Sort ?u.81 → Prop
Nonempty (
F: C ⥤ D
F.
obj: {V : Type ?u.119} → [inst : Quiver V] → {W : Type ?u.118} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
X: C
X ≅ 
Y: ?m.75
Y)
#align category_theory.functor.ess_image 
CategoryTheory.Functor.essImage: {C : Type u₁} → {D : Type u₂} → [inst : Category C] → [inst_1 : Category D] → C ⥤ D → Set D
CategoryTheory.Functor.essImage

/-- Get the witnessing object that `Y` is in the subcategory given by `F`. -/
def 
essImage.witness: {Y : D} → Y ∈ essImage F → C
essImage.witness {
Y: D
Y : 
D: Type u₂
D} (
h: Y ∈ essImage F
h : 
Y: D
Y ∈ 
F: C ⥤ D
F.
essImage: {C : Type ?u.229} → {D : Type ?u.228} → [inst : Category C] → [inst_1 : Category D] → C ⥤ D → Set D
essImage) : 
C: Type u₁
C :=
  
h: Y ∈ essImage F
h.
choose: {α : Sort ?u.270} → {p : α → Prop} → (∃ a, p a) → α
choose
#align category_theory.functor.ess_image.witness 
CategoryTheory.Functor.essImage.witness: {C : Type u₁} → {D : Type u₂} → [inst : Category C] → [inst_1 : Category D] → {F : C ⥤ D} → {Y : D} → Y ∈ essImage F → C
CategoryTheory.Functor.essImage.witness

/-- Extract the isomorphism between `F.obj h.witness` and `Y` itself. -/
-- Porting note: in the next, the dot notation `h.witness` no longer works
def 
essImage.getIso: {Y : D} → (h : Y ∈ essImage F) → F.obj (witness h) ≅ Y
essImage.getIso {
Y: D
Y : 
D: Type u₂
D} (
h: Y ∈ essImage F
h : 
Y: D
Y ∈ 
F: C ⥤ D
F.
essImage: {C : Type ?u.433} → {D : Type ?u.432} → [inst : Category C] → [inst_1 : Category D] → C ⥤ D → Set D
essImage) : 
F: C ⥤ D
F.
obj: {V : Type ?u.500} → [inst : Quiver V] → {W : Type ?u.499} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj (
essImage.witness: {C : Type ?u.540} →
  {D : Type ?u.539} → [inst : Category C] → [inst_1 : Category D] → {F : C ⥤ D} → {Y : D} → Y ∈ essImage F → C
essImage.witness 
h: Y ∈ essImage F
h) ≅ 
Y: D
Y :=
  
Classical.choice: {α : Sort ?u.596} → Nonempty α → α
Classical.choice 
h: Y ∈ essImage F
h.
choose_spec: ∀ {α : Sort ?u.598} {p : α → Prop} (P : ∃ a, p a), p (Exists.choose P)
choose_spec
#align category_theory.functor.ess_image.get_iso 
CategoryTheory.Functor.essImage.getIso: {C : Type u₁} →
  {D : Type u₂} →
    [inst : Category C] →
      [inst_1 : Category D] → {F : C ⥤ D} → {Y : D} → (h : Y ∈ essImage F) → F.obj (essImage.witness h) ≅ Y
CategoryTheory.Functor.essImage.getIso

/-- Being in the essential image is a "hygienic" property: it is preserved under isomorphism. -/
theorem 
essImage.ofIso: ∀ {Y Y' : D}, (Y ≅ Y') → Y ∈ essImage F → Y' ∈ essImage F
essImage.ofIso {
Y: D
Y 
Y': D
Y' : 
D: Type u₂
D} (
h: Y ≅ Y'
h : 
Y: D
Y ≅ 
Y': D
Y') (
hY: Y ∈ essImage F
hY : 
Y: D
Y ∈ 
essImage: {C : Type ?u.764} → {D : Type ?u.763} → [inst : Category C] → [inst_1 : Category D] → C ⥤ D → Set D
essImage 
F: C ⥤ D
F) : 
Y': D
Y' ∈ 
essImage: {C : Type ?u.844} → {D : Type ?u.843} → [inst : Category C] → [inst_1 : Category D] → C ⥤ D → Set D
essImage 
F: C ⥤ D
F :=
  
hY: Y ∈ essImage F
hY.
imp: ∀ {α : Sort ?u.896} {p q : α → Prop}, (∀ (a : α), p a → q a) → (∃ a, p a) → ∃ a, q a
imp fun 
_: ?m.912
_ => 
Nonempty.map: ∀ {α : Sort ?u.914} {β : Sort ?u.915}, (α → β) → Nonempty α → Nonempty β
Nonempty.map (· ≪≫ 
h: Y ≅ Y'
h)
#align category_theory.functor.ess_image.of_iso 
CategoryTheory.Functor.essImage.ofIso: ∀ {C : Type u₁} {D : Type u₂} [inst : Category C] [inst_1 : Category D] {F : C ⥤ D} {Y Y' : D},
  (Y ≅ Y') → Y ∈ essImage F → Y' ∈ essImage F
CategoryTheory.Functor.essImage.ofIso

/-- If `Y` is in the essential image of `F` then it is in the essential image of `F'` as long as
`F ≅ F'`.
-/
theorem 
essImage.ofNatIso: ∀ {C : Type u₁} {D : Type u₂} [inst : Category C] [inst_1 : Category D] {F F' : C ⥤ D},
  (F ≅ F') → ∀ {Y : D}, Y ∈ essImage F → Y ∈ essImage F'
essImage.ofNatIso {
F': C ⥤ D
F' : 
C: Type u₁
C ⥤ 
D: Type u₂
D} (
h: F ≅ F'
h : 
F: C ⥤ D
F ≅ 
F': C ⥤ D
F') {
Y: D
Y : 
D: Type u₂
D} (
hY: Y ∈ essImage F
hY : 
Y: D
Y ∈ 
essImage: {C : Type ?u.1084} → {D : Type ?u.1083} → [inst : Category C] → [inst_1 : Category D] → C ⥤ D → Set D
essImage 
F: C ⥤ D
F) :
    
Y: D
Y ∈ 
essImage: {C : Type ?u.1159} → {D : Type ?u.1158} → [inst : Category C] → [inst_1 : Category D] → C ⥤ D → Set D
essImage 
F': C ⥤ D
F' :=
  
hY: Y ∈ essImage F
hY.
imp: ∀ {α : Sort ?u.1211} {p q : α → Prop}, (∀ (a : α), p a → q a) → (∃ a, p a) → ∃ a, q a
imp fun 
X: ?m.1227
X => 
Nonempty.map: ∀ {α : Sort ?u.1229} {β : Sort ?u.1230}, (α → β) → Nonempty α → Nonempty β
Nonempty.map fun 
t: ?m.1240
t => 
h: F ≅ F'
h.
symm: {C : Type ?u.1268} → [inst : Category C] → {X Y : C} → (X ≅ Y) → (Y ≅ X)
symm.
app: {C : Type ?u.1292} →
  [inst : Category C] →
    {D : Type ?u.1291} → [inst_1 : Category D] → {F G : C ⥤ D} → (F ≅ G) → (X : C) → F.obj X ≅ G.obj X
app 
X: ?m.1227
X ≪≫ 
t: ?m.1240
t
#align category_theory.functor.ess_image.of_nat_iso 
CategoryTheory.Functor.essImage.ofNatIso: ∀ {C : Type u₁} {D : Type u₂} [inst : Category C] [inst_1 : Category D] {F F' : C ⥤ D},
  (F ≅ F') → ∀ {Y : D}, Y ∈ essImage F → Y ∈ essImage F'
CategoryTheory.Functor.essImage.ofNatIso

/-- Isomorphic functors have equal essential images. -/
theorem 
essImage_eq_of_natIso: ∀ {C : Type u₁} {D : Type u₂} [inst : Category C] [inst_1 : Category D] {F F' : C ⥤ D},
  (F ≅ F') → essImage F = essImage F'
essImage_eq_of_natIso {
F': C ⥤ D
F' : 
C: Type u₁
C ⥤ 
D: Type u₂
D} (
h: F ≅ F'
h : 
F: C ⥤ D
F ≅ 
F': C ⥤ D
F') : 
essImage: {C : Type ?u.1431} → {D : Type ?u.1430} → [inst : Category C] → [inst_1 : Category D] → C ⥤ D → Set D
essImage 
F: C ⥤ D
F = 
essImage: {C : Type ?u.1450} → {D : Type ?u.1449} → [inst : Category C] → [inst_1 : Category D] → C ⥤ D → Set D
essImage 
F': C ⥤ D
F' :=
  
funext: ∀ {α : Sort ?u.1470} {β : α → Sort ?u.1469} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext fun 
_: ?m.1482
_ => 
propext: ∀ {a b : Prop}, (a ↔ b) → a = b
propext ⟨
essImage.ofNatIso: ∀ {C : Type ?u.1498} {D : Type ?u.1497} [inst : Category C] [inst_1 : Category D] {F F' : C ⥤ D},
  (F ≅ F') → ∀ {Y : D}, Y ∈ essImage F → Y ∈ essImage F'
essImage.ofNatIso 
h: F ≅ F'
h, 
essImage.ofNatIso: ∀ {C : Type ?u.1539} {D : Type ?u.1538} [inst : Category C] [inst_1 : Category D] {F F' : C ⥤ D},
  (F ≅ F') → ∀ {Y : D}, Y ∈ essImage F → Y ∈ essImage F'
essImage.ofNatIso 
h: F ≅ F'
h.
symm: {C : Type ?u.1548} → [inst : Category C] → {X Y : C} → (X ≅ Y) → (Y ≅ X)
symm⟩
#align category_theory.functor.ess_image_eq_of_nat_iso 
CategoryTheory.Functor.essImage_eq_of_natIso: ∀ {C : Type u₁} {D : Type u₂} [inst : Category C] [inst_1 : Category D] {F F' : C ⥤ D},
  (F ≅ F') → essImage F = essImage F'
CategoryTheory.Functor.essImage_eq_of_natIso

/-- An object in the image is in the essential image. -/
theorem 
obj_mem_essImage: ∀ {C : Type u₁} {D : Type u₂} [inst : Category C] [inst_1 : Category D] (F : D ⥤ C) (Y : D), F.obj Y ∈ essImage F
obj_mem_essImage (
F: D ⥤ C
F : 
D: Type u₂
D ⥤ 
C: Type u₁
C) (
Y: D
Y : 
D: Type u₂
D) : 
F: D ⥤ C
F.
obj: {V : Type ?u.1677} → [inst : Quiver V] → {W : Type ?u.1676} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
Y: D
Y ∈ 
essImage: {C : Type ?u.1717} → {D : Type ?u.1716} → [inst : Category C] → [inst_1 : Category D] → C ⥤ D → Set D
essImage 
F: D ⥤ C
F :=
  ⟨
Y: D
Y, ⟨
Iso.refl: {C : Type ?u.1792} → [inst : Category C] → (X : C) → X ≅ X
Iso.refl 
_: ?m.1794
_⟩⟩
#align category_theory.functor.obj_mem_ess_image 
CategoryTheory.Functor.obj_mem_essImage: ∀ {C : Type u₁} {D : Type u₂} [inst : Category C] [inst_1 : Category D] (F : D ⥤ C) (Y : D), F.obj Y ∈ essImage F
CategoryTheory.Functor.obj_mem_essImage

/-- The essential image of a functor, interpreted of a full subcategory of the target category. -/
-- Porting note: no hasNonEmptyInstance linter yet
def 
EssImageSubcategory: (F : C ⥤ D) → ?m.1867 F
EssImageSubcategory (
F: C ⥤ D
F : 
C: Type u₁
C ⥤ 
D: Type u₂
D) :=
  
FullSubcategory: {C : Type ?u.1870} → (C → Prop) → Type ?u.1870
FullSubcategory 
F: C ⥤ D
F.
essImage: {C : Type ?u.1879} → {D : Type ?u.1878} → [inst : Category C] → [inst_1 : Category D] → C ⥤ D → Set D
essImage
#align category_theory.functor.ess_image_subcategory 
CategoryTheory.Functor.EssImageSubcategory: {C : Type u₁} → {D : Type u₂} → [inst : Category C] → [inst_1 : Category D] → C ⥤ D → Type u₂
CategoryTheory.Functor.EssImageSubcategory

-- Porting note: `deriving Category` is not able to derive this instance
instance: {C : Type u₁} →
  {D : Type u₂} → [inst : Category C] → [inst_1 : Category D] → {F : C ⥤ D} → Category (EssImageSubcategory F)
instance : 
Category: Type ?u.1937 → Type (max?u.1937(?u.1938+1))
Category (
EssImageSubcategory: {C : Type ?u.1940} → {D : Type ?u.1939} → [inst : Category C] → [inst_1 : Category D] → C ⥤ D → Type ?u.1939
EssImageSubcategory 
F: C ⥤ D
F) :=
  (
inferInstance: {α : Sort ?u.1997} → [i : α] → α
inferInstance : 
Category: Type ?u.1993 → Type (max?u.1993(v₂+1))
Category.{v₂} (
FullSubcategory: {C : Type ?u.1994} → (C → Prop) → Type ?u.1994
FullSubcategory 
_: ?m.1995 → Prop
_))

/-- The essential image as a subcategory has a fully faithful inclusion into the target category. -/
@[simps!]
def 
essImageInclusion: (F : C ⥤ D) → EssImageSubcategory F ⥤ D
essImageInclusion (
F: C ⥤ D
F : 
C: Type u₁
C ⥤ 
D: Type u₂
D) : 
F: C ⥤ D
F.
EssImageSubcategory: {C : Type ?u.2166} → {D : Type ?u.2165} → [inst : Category C] → [inst_1 : Category D] → C ⥤ D → Type ?u.2165
EssImageSubcategory ⥤ 
D: Type u₂
D :=
  
fullSubcategoryInclusion: {C : Type ?u.2220} → [inst : Category C] → (Z : C → Prop) → FullSubcategory Z ⥤ C
fullSubcategoryInclusion 
_: ?m.2222 → Prop
_
#align category_theory.functor.ess_image_inclusion 
CategoryTheory.Functor.essImageInclusion: {C : Type u₁} → {D : Type u₂} → [inst : Category C] → [inst_1 : Category D] → (F : C ⥤ D) → EssImageSubcategory F ⥤ D
CategoryTheory.Functor.essImageInclusion
#align category_theory.functor.ess_image_inclusion_obj 
CategoryTheory.Functor.essImageInclusion_obj: ∀ {C : Type u₁} {D : Type u₂} [inst : Category C] [inst_1 : Category D] (F : C ⥤ D)
  (self : FullSubcategory (essImage F)), (essImageInclusion F).obj self = self.obj
CategoryTheory.Functor.essImageInclusion_obj
#align category_theory.functor.ess_image_inclusion_map 
CategoryTheory.Functor.essImageInclusion_map: ∀ {C : Type u₁} {D : Type u₂} [inst : Category C] [inst_1 : Category D] (F : C ⥤ D)
  {X Y : InducedCategory D FullSubcategory.obj} (f : X ⟶ Y), (essImageInclusion F).map f = f
CategoryTheory.Functor.essImageInclusion_map

-- Porting note: `deriving Full` is not able to derive this instance
instance: {C : Type u₁} → {D : Type u₂} → [inst : Category C] → [inst_1 : Category D] → {F : C ⥤ D} → Full (essImageInclusion F)
instance : 
Full: {C : Type ?u.2390} →
  [inst : Category C] → {D : Type ?u.2389} → [inst_1 : Category D] → C ⥤ D → Type (max(max?u.2390?u.2392)?u.2391)
Full (
essImageInclusion: {C : Type ?u.2434} →
  {D : Type ?u.2433} → [inst : Category C] → [inst_1 : Category D] → (F : C ⥤ D) → EssImageSubcategory F ⥤ D
essImageInclusion 
F: C ⥤ D
F) :=
  (
inferInstance: {α : Sort ?u.2726} → [i : α] → α
inferInstance : 
Full: {C : Type ?u.2493} →
  [inst : Category C] → {D : Type ?u.2492} → [inst_1 : Category D] → C ⥤ D → Type (max(max?u.2493?u.2495)?u.2494)
Full (
fullSubcategoryInclusion: {C : Type ?u.2536} → [inst : Category C] → (Z : C → Prop) → FullSubcategory Z ⥤ C
fullSubcategoryInclusion 
_: ?m.2538 → Prop
_))

-- Porting note: `deriving Faithful` is not able to derive this instance
instance: ∀ {C : Type u₁} {D : Type u₂} [inst : Category C] [inst_1 : Category D] {F : C ⥤ D}, Faithful (essImageInclusion F)
instance : 
Faithful: {C : Type ?u.2957} → [inst : Category C] → {D : Type ?u.2956} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful (
essImageInclusion: {C : Type ?u.3001} →
  {D : Type ?u.3000} → [inst : Category C] → [inst_1 : Category D] → (F : C ⥤ D) → EssImageSubcategory F ⥤ D
essImageInclusion 
F: C ⥤ D
F) :=
  (
inferInstance: ∀ {α : Sort ?u.3293} [i : α], α
inferInstance : 
Faithful: {C : Type ?u.3060} → [inst : Category C] → {D : Type ?u.3059} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful (
fullSubcategoryInclusion: {C : Type ?u.3103} → [inst : Category C] → (Z : C → Prop) → FullSubcategory Z ⥤ C
fullSubcategoryInclusion 
_: ?m.3105 → Prop
_))

/--
Given a functor `F : C ⥤ D`, we have an (essentially surjective) functor from `C` to the essential
image of `F`.
-/
@[simps!]
def 
toEssImage: (F : C ⥤ D) → C ⥤ EssImageSubcategory F
toEssImage (
F: C ⥤ D
F : 
C: Type u₁
C ⥤ 
D: Type u₂
D) : 
C: Type u₁
C ⥤ 
F: C ⥤ D
F.
EssImageSubcategory: {C : Type ?u.3503} → {D : Type ?u.3502} → [inst : Category C] → [inst_1 : Category D] → C ⥤ D → Type ?u.3502
EssImageSubcategory :=
  
FullSubcategory.lift: {C : Type ?u.3557} →
  [inst : Category C] →
    {D : Type ?u.3556} →
      [inst_1 : Category D] → (P : D → Prop) → (F : C ⥤ D) → (∀ (X : C), P (F.obj X)) → C ⥤ FullSubcategory P
FullSubcategory.lift 
_: ?m.3562 → Prop
_ 
F: C ⥤ D
F (
obj_mem_essImage: ∀ {C : Type ?u.3612} {D : Type ?u.3611} [inst : Category C] [inst_1 : Category D] (F : D ⥤ C) (Y : D),
  F.obj Y ∈ essImage F
obj_mem_essImage 
_: ?m.3616 ⥤ ?m.3615
_)
#align category_theory.functor.to_ess_image 
CategoryTheory.Functor.toEssImage: {C : Type u₁} → {D : Type u₂} → [inst : Category C] → [inst_1 : Category D] → (F : C ⥤ D) → C ⥤ EssImageSubcategory F
CategoryTheory.Functor.toEssImage
#align category_theory.functor.to_ess_image_map 
CategoryTheory.Functor.toEssImage_map: ∀ {C : Type u₁} {D : Type u₂} [inst : Category C] [inst_1 : Category D] (F : C ⥤ D) {X Y : C} (f : X ⟶ Y),
  (toEssImage F).map f = F.map f
CategoryTheory.Functor.toEssImage_map
#align category_theory.functor.to_ess_image_obj_obj 
CategoryTheory.Functor.toEssImage_obj_obj: ∀ {C : Type u₁} {D : Type u₂} [inst : Category C] [inst_1 : Category D] (F : C ⥤ D) (X : C),
  ((toEssImage F).obj X).obj = F.obj X
CategoryTheory.Functor.toEssImage_obj_obj

/-- The functor `F` factorises through its essential image, where the first functor is essentially
surjective and the second is fully faithful.
-/
@[simps!]
def 
toEssImageCompEssentialImageInclusion: {C : Type u₁} →
  {D : Type u₂} → [inst : Category C] → [inst_1 : Category D] → (F : C ⥤ D) → toEssImage F ⋙ essImageInclusion F ≅ F
toEssImageCompEssentialImageInclusion (
F: C ⥤ D
F : 
C: Type u₁
C ⥤ 
D: Type u₂
D) : 
F: C ⥤ D
F.
toEssImage: {C : Type ?u.3974} →
  {D : Type ?u.3973} → [inst : Category C] → [inst_1 : Category D] → (F : C ⥤ D) → C ⥤ EssImageSubcategory F
toEssImage ⋙ 
F: C ⥤ D
F.
essImageInclusion: {C : Type ?u.4003} →
  {D : Type ?u.4002} → [inst : Category C] → [inst_1 : Category D] → (F : C ⥤ D) → EssImageSubcategory F ⥤ D
essImageInclusion ≅ 
F: C ⥤ D
F :=
  
FullSubcategory.lift_comp_inclusion: {C : Type ?u.4070} →
  [inst : Category C] →
    {D : Type ?u.4069} →
      [inst_1 : Category D] →
        (P : D → Prop) →
          (F : C ⥤ D) → (hF : ∀ (X : C), P (F.obj X)) → FullSubcategory.lift P F hF ⋙ fullSubcategoryInclusion P ≅ F
FullSubcategory.lift_comp_inclusion 
_: ?m.4075 → Prop
_ 
_: ?m.4073 ⥤ ?m.4075
_ 
_: ∀ (X : ?m.4073), ?m.4077 (?m.4078.obj X)
_
#align category_theory.functor.to_ess_image_comp_essential_image_inclusion 
CategoryTheory.Functor.toEssImageCompEssentialImageInclusion: {C : Type u₁} →
  {D : Type u₂} → [inst : Category C] → [inst_1 : Category D] → (F : C ⥤ D) → toEssImage F ⋙ essImageInclusion F ≅ F
CategoryTheory.Functor.toEssImageCompEssentialImageInclusion
#align category_theory.functor.to_ess_image_comp_essential_image_inclusion_hom_app 
CategoryTheory.Functor.toEssImageCompEssentialImageInclusion_hom_app: ∀ {C : Type u₁} {D : Type u₂} [inst : Category C] [inst_1 : Category D] (F : C ⥤ D) (X : C),
  (toEssImageCompEssentialImageInclusion F).hom.app X = 𝟙 (F.obj X)
CategoryTheory.Functor.toEssImageCompEssentialImageInclusion_hom_app
#align category_theory.functor.to_ess_image_comp_essential_image_inclusion_inv_app 
CategoryTheory.Functor.toEssImageCompEssentialImageInclusion_inv_app: ∀ {C : Type u₁} {D : Type u₂} [inst : Category C] [inst_1 : Category D] (F : C ⥤ D) (X : C),
  (toEssImageCompEssentialImageInclusion F).inv.app X = 𝟙 (F.obj X)
CategoryTheory.Functor.toEssImageCompEssentialImageInclusion_inv_app

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 .
-/
class 
EssSurj: {C : Type u₁} → {D : Type u₂} → [inst : Category C] → [inst_1 : Category D] → C ⥤ D → Prop
EssSurj (
F: C ⥤ D
F : 
C: Type u₁
C ⥤ 
D: Type u₂
D) : 
Prop: Type
Prop where
  /-- All the objects of the target category are in the essential image. -/
  
mem_essImage: ∀ {C : Type u₁} {D : Type u₂} [inst : Category C] [inst_1 : Category D] {F : C ⥤ D} [self : EssSurj F] (Y : D),
  Y ∈ Functor.essImage F
mem_essImage (
Y: D
Y : 
D: Type u₂
D) : 
Y: D
Y ∈ 
F: C ⥤ D
F.
essImage: {C : Type ?u.4873} → {D : Type ?u.4872} → [inst : Category C] → [inst_1 : Category D] → C ⥤ D → Set D
essImage
#align category_theory.ess_surj 
CategoryTheory.EssSurj: {C : Type u₁} → {D : Type u₂} → [inst : Category C] → [inst_1 : Category D] → C ⥤ D → Prop
CategoryTheory.EssSurj

instance: ∀ {C : Type u₁} {D : Type u₂} [inst : Category C] [inst_1 : Category D] {F : C ⥤ D}, EssSurj (Functor.toEssImage F)
instance :
    
EssSurj: {C : Type ?u.4965} → {D : Type ?u.4964} → [inst : Category C] → [inst_1 : Category D] → C ⥤ D → Prop
EssSurj
      
F: C ⥤ D
F.
toEssImage: {C : Type ?u.5009} →
  {D : Type ?u.5008} → [inst : Category C] → [inst_1 : Category D] → (F : C ⥤ D) → C ⥤ Functor.EssImageSubcategory F
toEssImage where mem_essImage := fun ⟨_, 
hY: Functor.essImage F obj✝
hY⟩ =>
    ⟨
_: ?m.5119
_, ⟨⟨
_: ?m.5144 ⟶ ?m.5145
_, 
_: ?m.5145 ⟶ ?m.5144
_, 
hY: Functor.essImage F obj✝
hY.
getIso: {C : Type ?u.5172} →
  {D : Type ?u.5171} →
    [inst : Category C] →
      [inst_1 : Category D] →
        {F : C ⥤ D} → {Y : D} → (h : Y ∈ Functor.essImage F) → F.obj (Functor.essImage.witness h) ≅ Y
getIso.
hom_inv_id: ∀ {C : Type ?u.5199} [inst : Category C] {X Y : C} (self : X ≅ Y), self.hom ≫ self.inv = 𝟙 X
hom_inv_id, 
hY: Functor.essImage F obj✝
hY.
getIso: {C : Type ?u.5234} →
  {D : Type ?u.5233} →
    [inst : Category C] →
      [inst_1 : Category D] →
        {F : C ⥤ D} → {Y : D} → (h : Y ∈ Functor.essImage F) → F.obj (Functor.essImage.witness h) ≅ Y
getIso.
inv_hom_id: ∀ {C : Type ?u.5250} [inst : Category C] {X Y : C} (self : X ≅ Y), self.inv ≫ self.hom = 𝟙 Y
inv_hom_id⟩⟩⟩

variable (
F: ?m.5407
F) [
EssSurj: {C : Type ?u.6180} → {D : Type ?u.6179} → [inst : Category C] → [inst_1 : Category D] → C ⥤ D → Prop
EssSurj 
F: ?m.5407
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.objPreimage: {C : Type u₁} → {D : Type u₂} → [inst : Category C] → [inst_1 : Category D] → (F : C ⥤ D) → [inst : EssSurj F] → D → C
Functor.objPreimage (
Y: D
Y : 
D: Type u₂
D) : 
C: Type u₁
C :=
  
essImage.witness: {C : Type ?u.5623} →
  {D : Type ?u.5622} → [inst : Category C] → [inst_1 : Category D] → {F : C ⥤ D} → {Y : D} → Y ∈ essImage F → C
essImage.witness (@
EssSurj.mem_essImage: ∀ {C : Type ?u.5669} {D : Type ?u.5668} [inst : Category C] [inst_1 : Category D] {F : C ⥤ D} [self : EssSurj F]
  (Y : D), Y ∈ essImage F
EssSurj.mem_essImage 
_: Type ?u.5669
_ 
_: Type ?u.5668
_ _ _ 
F: C ⥤ D
F _ 
Y: D
Y)
#align category_theory.functor.obj_preimage 
CategoryTheory.Functor.objPreimage: {C : Type u₁} → {D : Type u₂} → [inst : Category C] → [inst_1 : Category D] → (F : C ⥤ D) → [inst : EssSurj F] → D → C
CategoryTheory.Functor.objPreimage

/-- Applying an essentially surjective functor to a preimage of `Y` yields an object that is
    isomorphic to `Y`. -/
def 
Functor.objObjPreimageIso: (Y : D) → F.obj (objPreimage F Y) ≅ Y
Functor.objObjPreimageIso (
Y: D
Y : 
D: Type u₂
D) : 
F: C ⥤ D
F.
obj: {V : Type ?u.5944} → [inst : Quiver V] → {W : Type ?u.5943} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj (
F: C ⥤ D
F.
objPreimage: {C : Type ?u.5984} →
  {D : Type ?u.5983} → [inst : Category C] → [inst_1 : Category D] → (F : C ⥤ D) → [inst : EssSurj F] → D → C
objPreimage 
Y: D
Y) ≅ 
Y: D
Y :=
  
Functor.essImage.getIso: {C : Type ?u.6018} →
  {D : Type ?u.6017} →
    [inst : Category C] →
      [inst_1 : Category D] → {F : C ⥤ D} → {Y : D} → (h : Y ∈ essImage F) → F.obj (essImage.witness h) ≅ Y
Functor.essImage.getIso 
_: ?m.6026 ∈ essImage ?m.6025
_
#align category_theory.functor.obj_obj_preimage_iso 
CategoryTheory.Functor.objObjPreimageIso: {C : Type u₁} →
  {D : Type u₂} →
    [inst : Category C] →
      [inst_1 : Category D] → (F : C ⥤ D) → [inst_2 : EssSurj F] → (Y : D) → F.obj (Functor.objPreimage F Y) ≅ Y
CategoryTheory.Functor.objObjPreimageIso

/-- The induced functor of a faithful functor is faithful -/
instance 
Faithful.toEssImage: ∀ (F : C ⥤ D) [inst : Faithful F], Faithful (Functor.toEssImage F)
Faithful.toEssImage (
F: C ⥤ D
F : 
C: Type u₁
C ⥤ 
D: Type u₂
D) [
Faithful: {C : Type ?u.6256} → [inst : Category C] → {D : Type ?u.6255} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful 
F: C ⥤ D
F] : 
Faithful: {C : Type ?u.6316} → [inst : Category C] → {D : Type ?u.6315} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful 
F: C ⥤ D
F.
toEssImage: {C : Type ?u.6360} →
  {D : Type ?u.6359} → [inst : Category C] → [inst_1 : Category D] → (F : C ⥤ D) → C ⥤ Functor.EssImageSubcategory F
toEssImage :=
  
Faithful.of_comp_iso: ∀ {C : Type ?u.6410} [inst : Category C] {D : Type ?u.6409} [inst_1 : Category D] {E : Type ?u.6408}
  [inst_2 : Category E] {F : C ⥤ D} {G : D ⥤ E} {H : C ⥤ E} [inst_3 : Faithful H], (F ⋙ G ≅ H) → Faithful F
Faithful.of_comp_iso 
F: C ⥤ D
F.
toEssImageCompEssentialImageInclusion: {C : Type ?u.6515} →
  {D : Type ?u.6514} →
    [inst : Category C] → [inst_1 : Category D] → (F : C ⥤ D) → Functor.toEssImage F ⋙ Functor.essImageInclusion F ≅ F
toEssImageCompEssentialImageInclusion
#align category_theory.faithful.to_ess_image 
CategoryTheory.Faithful.toEssImage: ∀ {C : Type u₁} {D : Type u₂} [inst : Category C] [inst_1 : Category D] (F : C ⥤ D) [inst_2 : Faithful F],
  Faithful (Functor.toEssImage F)
CategoryTheory.Faithful.toEssImage

/-- The induced functor of a full functor is full -/
instance 
Full.toEssImage: (F : C ⥤ D) → [inst : Full F] → Full (Functor.toEssImage F)
Full.toEssImage (
F: C ⥤ D
F : 
C: Type u₁
C ⥤ 
D: Type u₂
D) [
Full: {C : Type ?u.6730} →
  [inst : Category C] → {D : Type ?u.6729} → [inst_1 : Category D] → C ⥤ D → Type (max(max?u.6730?u.6732)?u.6731)
Full 
F: C ⥤ D
F] : 
Full: {C : Type ?u.6790} →
  [inst : Category C] → {D : Type ?u.6789} → [inst_1 : Category D] → C ⥤ D → Type (max(max?u.6790?u.6792)?u.6791)
Full 
F: C ⥤ D
F.
toEssImage: {C : Type ?u.6834} →
  {D : Type ?u.6833} → [inst : Category C] → [inst_1 : Category D] → (F : C ⥤ D) → C ⥤ Functor.EssImageSubcategory F
toEssImage :=
  haveI := 
Full.ofIso: {C : Type ?u.6885} →
  [inst : Category C] →
    {D : Type ?u.6884} → [inst_1 : Category D] → {F F' : C ⥤ D} → [inst_2 : Full F] → (F ≅ F') → Full F'
Full.ofIso 
F: C ⥤ D
F.
toEssImageCompEssentialImageInclusion: {C : Type ?u.6961} →
  {D : Type ?u.6960} →
    [inst : Category C] → [inst_1 : Category D] → (F : C ⥤ D) → Functor.toEssImage F ⋙ Functor.essImageInclusion F ≅ F
toEssImageCompEssentialImageInclusion.
symm: {C : Type ?u.6972} → [inst : Category C] → {X Y : C} → (X ≅ Y) → (Y ≅ X)
symm
  
Full.ofCompFaithful: {C : Type ?u.7032} →
  [inst : Category C] →
    {D : Type ?u.7031} →
      [inst_1 : Category D] →
        {E : Type ?u.7030} →
          [inst_2 : Category E] → (F : C ⥤ D) → (G : D ⥤ E) → [inst_3 : Full (F ⋙ G)] → [inst_4 : Faithful G] → Full F
Full.ofCompFaithful 
F: C ⥤ D
F.
toEssImage: {C : Type ?u.7043} →
  {D : Type ?u.7042} → [inst : Category C] → [inst_1 : Category D] → (F : C ⥤ D) → C ⥤ Functor.EssImageSubcategory F
toEssImage 
F: C ⥤ D
F.
essImageInclusion: {C : Type ?u.7096} →
  {D : Type ?u.7095} → [inst : Category C] → [inst_1 : Category D] → (F : C ⥤ D) → Functor.EssImageSubcategory F ⥤ D
essImageInclusion
#align category_theory.full.to_ess_image 
CategoryTheory.Full.toEssImage: {C : Type u₁} →
  {D : Type u₂} →
    [inst : Category C] → [inst_1 : Category D] → (F : C ⥤ D) → [inst_2 : Full F] → Full (Functor.toEssImage F)
CategoryTheory.Full.toEssImage

end CategoryTheory