mathlib3 documentation

category_theory.essential_image

Essential image of a functor #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
def category_theory.functor.ess_image {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (F : C ⥤ D) :
set 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
source
noncomputable def category_theory.functor.ess_image.witness {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {F : C ⥤ D} {Y : D} (h : Y ∈ F.ess_image) :
C

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

Equations
source
noncomputable def category_theory.functor.ess_image.get_iso {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {F : C ⥤ D} {Y : D} (h : Y ∈ F.ess_image) :
F.obj (category_theory.functor.ess_image.witness h) ≅ Y

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

Equations
source
theorem category_theory.functor.ess_image.of_iso {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {F : C ⥤ D} {Y Y' : D} (h : Y ≅ Y') (hY : Y ∈ F.ess_image) :
Y' ∈ F.ess_image

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

source
theorem category_theory.functor.ess_image.of_nat_iso {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {F F' : C ⥤ D} (h : F ≅ F') {Y : D} (hY : Y ∈ F.ess_image) :
Y ∈ F'.ess_image

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 category_theory.functor.ess_image_eq_of_nat_iso {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {F F' : C ⥤ D} (h : F ≅ F') :
F.ess_image = F'.ess_image

Isomorphic functors have equal essential images.

source
theorem category_theory.functor.obj_mem_ess_image {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (F : D ⥤ C) (Y : D) :
F.obj Y ∈ F.ess_image

An object in the image is in the essential image.

source
@[protected, instance]
def category_theory.functor.ess_image_subcategory.category {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (F : C ⥤ D) :
category_theory.category F.ess_image_subcategory
source
@[nolint]
def category_theory.functor.ess_image_subcategory {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (F : C ⥤ D) :
Type u₂

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

Equations
Instances for category_theory.functor.ess_image_subcategory
source
@[protected, instance]
def category_theory.functor.ess_image_inclusion.full {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (F : C ⥤ D) :
category_theory.full F.ess_image_inclusion
source
def category_theory.functor.ess_image_inclusion {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (F : C ⥤ D) :
F.ess_image_subcategory ⥤ D

The essential image as a subcategory has a fully faithful inclusion into the target category.

Equations
Instances for category_theory.functor.ess_image_inclusion
source
@[protected, instance]
def category_theory.functor.ess_image_inclusion.faithful {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (F : C ⥤ D) :
category_theory.faithful F.ess_image_inclusion
source
@[simp]
theorem category_theory.functor.ess_image_inclusion_obj {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (F : C ⥤ D) (self : category_theory.full_subcategory F.ess_image) :
F.ess_image_inclusion.obj self = self.obj
source
@[simp]
theorem category_theory.functor.ess_image_inclusion_map {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (F : C ⥤ D) (x y : category_theory.induced_category D category_theory.full_subcategory.obj) (f : x ⟶ y) :
F.ess_image_inclusion.map f = f
source
@[simp]
theorem category_theory.functor.to_ess_image_map {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (F : C ⥤ D) (X Y : C) (f : X ⟶ Y) :
F.to_ess_image.map f = F.map f
source
def category_theory.functor.to_ess_image {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (F : C ⥤ D) :
C ⥤ F.ess_image_subcategory

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

Equations
Instances for category_theory.functor.to_ess_image
source
@[simp]
theorem category_theory.functor.to_ess_image_obj_obj {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (F : C ⥤ D) (X : C) :
(F.to_ess_image.obj X).obj = F.obj X
source
@[simp]
theorem category_theory.functor.to_ess_image_comp_essential_image_inclusion_hom_app {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (F : C ⥤ D) (X : C) :
F.to_ess_image_comp_essential_image_inclusion.hom.app X = 𝟙 (F.obj X)
source
@[simp]
theorem category_theory.functor.to_ess_image_comp_essential_image_inclusion_inv_app {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (F : C ⥤ D) (X : C) :
F.to_ess_image_comp_essential_image_inclusion.inv.app X = 𝟙 (F.obj X)
source
def category_theory.functor.to_ess_image_comp_essential_image_inclusion {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (F : C ⥤ D) :
F.to_ess_image ⋙ F.ess_image_inclusion ≅ F

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

Equations
source
@[class]
structure category_theory.ess_surj {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (F : 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.

See https://stacks.math.columbia.edu/tag/001C.

Instances of this typeclass
source
@[protected, instance]
def category_theory.functor.to_ess_image.ess_surj {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {F : C ⥤ D} :
category_theory.ess_surj F.to_ess_image
source
noncomputable def category_theory.functor.obj_preimage {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (F : C ⥤ D) [category_theory.ess_surj F] (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
source
noncomputable def category_theory.functor.obj_obj_preimage_iso {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (F : C ⥤ D) [category_theory.ess_surj F] (Y : D) :
F.obj (F.obj_preimage Y) ≅ Y

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

Equations
source
@[protected, instance]
def category_theory.faithful.to_ess_image {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (F : C ⥤ D) [category_theory.faithful F] :
category_theory.faithful F.to_ess_image

The induced functor of a faithful functor is faithful

source
@[protected, instance]
def category_theory.full.to_ess_image {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (F : C ⥤ D) [category_theory.full F] :
category_theory.full F.to_ess_image

The induced functor of a full functor is full

Equations