# 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 an essentially surjective functor and a fully faithful functor. (TODO: show that this decomposition forms an orthogonal factorisation system).

source
def CategoryTheory.Functor.essImage {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) :
ObjectProperty D

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.

Equations

- F.essImage Y = ∃ (X : C), Nonempty (F.obj X ≅ Y)

Instances For

source
def CategoryTheory.Functor.essImage.witness {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {F : Functor C D} {Y : D} (h : F.essImage Y) :
C

Get the witnessing object that `Y` is in the subcategory given by `F`.

Equations

- h.witness = Exists.choose h

Instances For

source
def CategoryTheory.Functor.essImage.getIso {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {F : Functor C D} {Y : D} (h : F.essImage Y) :
F.obj h.witness ≅ Y

Extract the isomorphism between `F.obj h.witness` and `Y` itself.

Equations

- h.getIso = Classical.choice ⋯

Instances For

source
theorem CategoryTheory.Functor.essImage.ofIso {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {F : Functor C D} {Y Y' : D} (h : Y ≅ Y') (hY : F.essImage Y) :
F.essImage Y'

Being in the essential image is a "hygienic" property: it is preserved under isomorphism.

source
instance CategoryTheory.Functor.instIsClosedUnderIsomorphismsEssImage {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {F : Functor C D} :
F.essImage.IsClosedUnderIsomorphisms
source
theorem CategoryTheory.Functor.essImage.ofNatIso {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {F F' : Functor C D} (h : F ≅ F') {Y : D} (hY : F.essImage Y) :
F'.essImage Y

If `Y` is in the essential image of `F` then it is in the essential image of `F'` as long as `F ≅ F'`.

source
theorem CategoryTheory.Functor.essImage_eq_of_natIso {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {F F' : Functor C D} (h : F ≅ F') :
F.essImage = F'.essImage

Isomorphic functors have equal essential images.

source
theorem CategoryTheory.Functor.obj_mem_essImage {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor D C) (Y : D) :
F.essImage (F.obj Y)

An object in the image is in the essential image.

source
@[reducible, inline]
abbrev CategoryTheory.Functor.EssImageSubcategory {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) :
Type u₂

The essential image of a functor, interpreted as a full subcategory of the target category.

Equations

- F.EssImageSubcategory = F.essImage.FullSubcategory

Instances For

source
theorem CategoryTheory.Functor.essImage_ext {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) {X Y : F.EssImageSubcategory} (f g : X ⟶ Y) (h : F.essImage.ι.map f = F.essImage.ι.map g) :
f = g
source
def CategoryTheory.Functor.toEssImage {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) :
Functor C F.EssImageSubcategory

Given a functor `F : C ⥤ D`, we have an (essentially surjective) functor from `C` to the essential image of `F`.

Equations

- F.toEssImage = F.essImage.lift F ⋯

Instances For

source
@[simp]
theorem CategoryTheory.Functor.toEssImage_obj_obj {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) (X : C) :
(F.toEssImage.obj X).obj = F.obj X
source
@[simp]
theorem CategoryTheory.Functor.toEssImage_map {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) :
F.toEssImage.map f = F.map f
source
def CategoryTheory.Functor.toEssImageCompι {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) :
F.toEssImage.comp F.essImage.ι ≅ F

The functor `F` factorises through its essential image, where the first functor is essentially surjective and the second is fully faithful.

Equations

- F.toEssImageCompι = F.essImage.liftCompιIso F ⋯

Instances For

source
@[simp]
theorem CategoryTheory.Functor.toEssImageCompι_hom_app {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) (X : C) :
F.toEssImageCompι.hom.app X = CategoryStruct.id (F.obj X)
source
@[simp]
theorem CategoryTheory.Functor.toEssImageCompι_inv_app {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) (X : C) :
F.toEssImageCompι.inv.app X = CategoryStruct.id (F.obj X)
source
class CategoryTheory.Functor.EssSurj {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) :
Prop

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`.

- mem_essImage (Y : D) : F.essImage Y

  All the objects of the target category are in the essential image.

Instances

source
instance CategoryTheory.Functor.EssSurj.toEssImage {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {F : Functor C D} :
F.toEssImage.EssSurj
source
theorem CategoryTheory.Functor.essSurj_of_surj {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {F : Functor C D} (h : Function.Surjective F.obj) :
F.EssSurj
source
def CategoryTheory.Functor.objPreimage {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) [F.EssSurj] (Y : D) :
C

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`.

Equations

- F.objPreimage Y = ⋯.witness

Instances For

source
def CategoryTheory.Functor.objObjPreimageIso {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) [F.EssSurj] (Y : D) :
F.obj (F.objPreimage Y) ≅ Y

Applying an essentially surjective functor to a preimage of `Y` yields an object that is isomorphic to `Y`.

Equations

- F.objObjPreimageIso Y = ⋯.getIso

Instances For

source
instance CategoryTheory.Functor.Faithful.toEssImage {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) [F.Faithful] :
F.toEssImage.Faithful

The induced functor of a faithful functor is faithful.

source
instance CategoryTheory.Functor.Full.toEssImage {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) [F.Full] :
F.toEssImage.Full

The induced functor of a full functor is full.

source
instance CategoryTheory.Functor.instEssSurjId {C : Type u₁} [Category.{v₁, u₁} C] :
(Functor.id C).EssSurj
source
theorem CategoryTheory.Functor.essSurj_of_iso {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {F G : Functor C D} [F.EssSurj] (α : F ≅ G) :
G.EssSurj
source
instance CategoryTheory.Functor.essSurj_comp {C : Type u₁} {D : Type u₂} {E : Type u₃} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [F.EssSurj] [G.EssSurj] :
(F.comp G).EssSurj
source
theorem CategoryTheory.Functor.essSurj_of_comp_fully_faithful {C : Type u₁} {D : Type u₂} {E : Type u₃} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [(F.comp G).EssSurj] [G.Faithful] [G.Full] :
F.EssSurj
source
theorem CategoryTheory.Functor.essImage_comp_apply_of_essSurj {C : Type u₁} {D : Type u₂} {E : Type u₃} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Category.{v₃, u₃} E] {F : Functor C D} {G : Functor D E} [F.EssSurj] {X : E} :
(F.comp G).essImage X ↔ G.essImage X

Pre-composing by an essentially surjective functor doesn't change the essential image.

source
@[simp]
theorem CategoryTheory.Functor.essImage_comp_of_essSurj {C : Type u₁} {D : Type u₂} {E : Type u₃} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Category.{v₃, u₃} E] {F : Functor C D} {G : Functor D E} [F.EssSurj] :
(F.comp G).essImage = G.essImage

Pre-composing by an essentially surjective functor doesn't change the essential image.

source
def CategoryTheory.Functor.essImage.liftFunctor {J : Type u_1} {C : Type u_2} {D : Type u_3} [Category.{u_4, u_1} J] [Category.{u_5, u_2} C] [Category.{u_6, u_3} D] (G : Functor J D) (F : Functor C D) [F.Full] [F.Faithful] (hG : ∀ (j : J), F.essImage (G.obj j)) :
Functor J C

Lift a functor `G : J ⥤ D` to the essential image of a fully faithful functor `F : C ⥤ D` to a functor `G' : J ⥤ C` such that `G' ⋙ F ≅ G`. See `essImage.liftFunctorCompIso`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem CategoryTheory.Functor.essImage.liftFunctor_obj {J : Type u_1} {C : Type u_2} {D : Type u_3} [Category.{u_4, u_1} J] [Category.{u_5, u_2} C] [Category.{u_6, u_3} D] (G : Functor J D) (F : Functor C D) [F.Full] [F.Faithful] (hG : ∀ (j : J), F.essImage (G.obj j)) (j : J) :
(liftFunctor G F hG).obj j = F.toEssImage.objPreimage { obj := G.obj j, property := ⋯ }
source
@[simp]
theorem CategoryTheory.Functor.essImage.liftFunctor_map {J : Type u_1} {C : Type u_2} {D : Type u_3} [Category.{u_4, u_1} J] [Category.{u_5, u_2} C] [Category.{u_6, u_3} D] (G : Functor J D) (F : Functor C D) [F.Full] [F.Faithful] (hG : ∀ (j : J), F.essImage (G.obj j)) {i j : J} (f : i ⟶ j) :
(liftFunctor G F hG).map f = F.preimage (CategoryStruct.comp (F.toEssImage.objObjPreimageIso { obj := G.obj i, property := ⋯ }).hom (CategoryStruct.comp (G.map f) (F.toEssImage.objObjPreimageIso { obj := G.obj j, property := ⋯ }).inv))
source
def CategoryTheory.Functor.essImage.liftFunctorCompIso {J : Type u_1} {C : Type u_2} {D : Type u_3} [Category.{u_4, u_1} J] [Category.{u_5, u_2} C] [Category.{u_6, u_3} D] (G : Functor J D) (F : Functor C D) [F.Full] [F.Faithful] (hG : ∀ (j : J), F.essImage (G.obj j)) :
(liftFunctor G F hG).comp F ≅ G

A functor `G : J ⥤ D` to the essential image of a fully faithful functor `F : C ⥤ D` does factor through `essImage.liftFunctor G F hG`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem CategoryTheory.Functor.essImage.liftFunctorCompIso_hom_app {J : Type u_1} {C : Type u_2} {D : Type u_3} [Category.{u_4, u_1} J] [Category.{u_5, u_2} C] [Category.{u_6, u_3} D] (G : Functor J D) (F : Functor C D) [F.Full] [F.Faithful] (hG : ∀ (j : J), F.essImage (G.obj j)) (X : J) :
(liftFunctorCompIso G F hG).hom.app X = (F.toEssImage.objObjPreimageIso { obj := G.obj X, property := ⋯ }).hom
source
@[simp]
theorem CategoryTheory.Functor.essImage.liftFunctorCompIso_inv_app {J : Type u_1} {C : Type u_2} {D : Type u_3} [Category.{u_4, u_1} J] [Category.{u_5, u_2} C] [Category.{u_6, u_3} D] (G : Functor J D) (F : Functor C D) [F.Full] [F.Faithful] (hG : ∀ (j : J), F.essImage (G.obj j)) (X : J) :
(liftFunctorCompIso G F hG).inv.app X = (F.toEssImage.objObjPreimageIso { obj := G.obj X, property := ⋯ }).inv