Mathlib.CategoryTheory.EssentialImage

CategoryTheory.Functor.essImage definition

(F : C ⥤ D) : ObjectProperty D

Full source

/-- 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 (F : C ⥤ D) : ObjectProperty D := fun Y => ∃ X : C, Nonempty (F.obj X ≅ Y)

Essential image of a functor

Informal description

The essential image of a functor $ F : \mathcal{C} \to \mathcal{D} $ consists of those objects $ Y $ in the target category $ \mathcal{D} $ for which there exists an object $ X $ in the source category $ \mathcal{C} $ such that $ F(X) $ is isomorphic to $ Y $. This provides a way to describe the image of a functor up to isomorphism, respecting the principle of equivalence in category theory.

CategoryTheory.Functor.essImage.witness definition

{Y : D} (h : F.essImage Y) : C

Full source

/-- Get the witnessing object that `Y` is in the subcategory given by `F`. -/
def essImage.witness {Y : D} (h : F.essImage Y) : C :=
  h.choose

Witnessing object for essential image

Informal description

Given an object $ Y $ in the essential image of a functor $ F : \mathcal{C} \to \mathcal{D} $, the function returns an object $ X $ in $ \mathcal{C} $ such that $ F(X) $ is isomorphic to $ Y $. This witnesses the fact that $ Y $ is in the essential image of $ F $.

CategoryTheory.Functor.essImage.getIso definition

{Y : D} (h : F.essImage Y) : F.obj h.witness ≅ Y

Full source

/-- Extract the isomorphism between `F.obj h.witness` and `Y` itself. -/
def essImage.getIso {Y : D} (h : F.essImage Y) : F.obj h.witness ≅ Y :=
  Classical.choice h.choose_spec

Isomorphism witnessing essential image membership

Informal description

Given an object $ Y $ in the essential image of a functor $ F : \mathcal{C} \to \mathcal{D} $, this function returns an isomorphism between $ F(X) $ and $ Y $, where $ X $ is the witnessing object in $ \mathcal{C} $ such that $ F(X) \cong Y $.

CategoryTheory.Functor.essImage.ofIso theorem

{Y Y' : D} (h : Y ≅ Y') (hY : essImage F Y) : essImage F Y'

Full source

/-- Being in the essential image is a "hygienic" property: it is preserved under isomorphism. -/
theorem essImage.ofIso {Y Y' : D} (h : Y ≅ Y') (hY : essImage F Y) : essImage F Y' :=
  hY.imp fun _ => Nonempty.map (· ≪≫ h)

Essential Image is Closed Under Isomorphism

Informal description

Let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor between categories. If an object $Y$ in $\mathcal{D}$ belongs to the essential image of $F$ and there exists an isomorphism $h \colon Y \cong Y'$ to another object $Y'$ in $\mathcal{D}$, then $Y'$ also belongs to the essential image of $F$.

CategoryTheory.Functor.instIsClosedUnderIsomorphismsEssImage instance

: F.essImage.IsClosedUnderIsomorphisms

Full source

instance : F.essImage.IsClosedUnderIsomorphisms where
  of_iso e h := essImage.ofIso e h

Essential Image is Closed Under Isomorphisms

Informal description

The essential image of a functor $ F \colon \mathcal{C} \to \mathcal{D} $ is closed under isomorphisms in the target category $\mathcal{D}$. That is, if an object $ Y $ in $\mathcal{D}$ belongs to the essential image of $ F $ and there exists an isomorphism $ Y \cong Y' $ for some object $ Y' $ in $\mathcal{D}$, then $ Y' $ also belongs to the essential image of $ F $.

CategoryTheory.Functor.essImage.ofNatIso theorem

{F' : C ⥤ D} (h : F ≅ F') {Y : D} (hY : essImage F Y) : essImage F' Y

Full source

/-- 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 {F' : C ⥤ D} (h : F ≅ F') {Y : D} (hY : essImage F Y) :
    essImage F' Y :=
  hY.imp fun X => Nonempty.map fun t => h.symm.app X ≪≫ t

Essential Image Invariance under Natural Isomorphism

Informal description

Let $F, F' \colon \mathcal{C} \to \mathcal{D}$ be functors with a natural isomorphism $\alpha \colon F \cong F'$. If an object $Y$ in $\mathcal{D}$ belongs to the essential image of $F$, then it also belongs to the essential image of $F'$.

CategoryTheory.Functor.essImage_eq_of_natIso theorem

{F' : C ⥤ D} (h : F ≅ F') : essImage F = essImage F'

Full source

/-- Isomorphic functors have equal essential images. -/
theorem essImage_eq_of_natIso {F' : C ⥤ D} (h : F ≅ F') : essImage F = essImage F' :=
  funext fun _ => propext ⟨essImage.ofNatIso h, essImage.ofNatIso h.symm⟩

Essential Image Equality under Natural Isomorphism

Informal description

Given two functors $F, F' \colon \mathcal{C} \to \mathcal{D}$ and a natural isomorphism $h \colon F \cong F'$, the essential images of $F$ and $F'$ are equal, i.e., $\mathrm{essImage}(F) = \mathrm{essImage}(F')$.

CategoryTheory.Functor.obj_mem_essImage theorem

(F : D ⥤ C) (Y : D) : essImage F (F.obj Y)

Full source

/-- An object in the image is in the essential image. -/
theorem obj_mem_essImage (F : D ⥤ C) (Y : D) : essImage F (F.obj Y) :=
  ⟨Y, ⟨Iso.refl _⟩⟩

Objects in the image are in the essential image

Informal description

For any functor $F \colon \mathcal{D} \to \mathcal{C}$ and any object $Y$ in $\mathcal{D}$, the object $F(Y)$ in $\mathcal{C}$ belongs to the essential image of $F$. That is, there exists an object $X$ in $\mathcal{D}$ (namely $X = Y$) such that $F(X) \cong F(Y)$ via the identity isomorphism.

CategoryTheory.Functor.EssImageSubcategory abbrev

(F : C ⥤ D)

Full source

/-- The essential image of a functor, interpreted as a full subcategory of the target category. -/
abbrev EssImageSubcategory (F : C ⥤ D) := F.essImage.FullSubcategory

Essential Image Subcategory of a Functor

Informal description

Given a functor $F \colon \mathcal{C} \to \mathcal{D}$, the essential image subcategory $\mathrm{EssImageSubcategory}(F)$ is the full subcategory of $\mathcal{D}$ whose objects are those $Y \in \mathcal{D}$ for which there exists an object $X \in \mathcal{C}$ with $F(X) \cong Y$.

CategoryTheory.Functor.essImageInclusion definition

(F : C ⥤ D) : F.EssImageSubcategory ⥤ D

Full source

/-- The essential image as a subcategory has a fully faithful inclusion into the target category. -/
@[deprecated "use F.essImage.ι" (since := "2025-03-04")]
def essImageInclusion (F : C ⥤ D) : F.EssImageSubcategory ⥤ D :=
  F.essImage.ι

Inclusion functor of the essential image

Informal description

The inclusion functor from the essential image subcategory of a functor $ F \colon \mathcal{C} \to \mathcal{D} $ back into the target category $\mathcal{D}$. This functor is fully faithful, meaning it preserves all morphism structures between objects in the essential image.

CategoryTheory.Functor.essImage_ext theorem

(F : C ⥤ D) {X Y : F.EssImageSubcategory} (f g : X ⟶ Y) (h : F.essImage.ι.map f = F.essImage.ι.map g) : f = g

Full source

lemma essImage_ext (F : C ⥤ D) {X Y : F.EssImageSubcategory} (f g : X ⟶ Y)
    (h : F.essImage.ι.map f = F.essImage.ι.map g) : f = g :=
  F.essImage.ι.map_injective h

Faithfulness of Essential Image Inclusion

Informal description

Let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor, and let $X, Y$ be objects in the essential image subcategory of $F$. For any two morphisms $f, g \colon X \to Y$ in this subcategory, if the images of $f$ and $g$ under the inclusion functor $\iota$ of the essential image into $\mathcal{D}$ are equal (i.e., $\iota(f) = \iota(g)$), then $f = g$.

CategoryTheory.Functor.toEssImage definition

(F : C ⥤ D) : C ⥤ F.EssImageSubcategory

Full source

/--
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 ⥤ F.EssImageSubcategory :=
  F.essImage.lift F (obj_mem_essImage _)

Functor to the essential image

Informal description

Given a functor $ F \colon \mathcal{C} \to \mathcal{D} $, the functor $ \mathrm{toEssImage}(F) $ maps objects and morphisms from the source category $ \mathcal{C} $ to the essential image subcategory of $ F $ in $ \mathcal{D} $. This functor is essentially surjective by construction, as every object in the essential image is isomorphic to some $ F(X) $ for $ X $ in $ \mathcal{C} $.

CategoryTheory.Functor.toEssImageCompι definition

(F : C ⥤ D) : F.toEssImage ⋙ F.essImage.ι ≅ F

Full source

/-- The functor `F` factorises through its essential image, where the first functor is essentially
surjective and the second is fully faithful.
-/
@[simps!]
def toEssImageCompι (F : C ⥤ D) : F.toEssImage ⋙ F.essImage.ιF.toEssImage ⋙ F.essImage.ι ≅ F :=
  ObjectProperty.liftCompιIso _ _ _

Natural isomorphism between essential image factorization and original functor

Informal description

The natural isomorphism between the composition of the functor `F.toEssImage` (which maps objects and morphisms from the source category $\mathcal{C}$ to the essential image subcategory of $F$ in $\mathcal{D}$) followed by the inclusion functor `F.essImage.ι` (which embeds the essential image subcategory back into $\mathcal{D}$) and the original functor $F \colon \mathcal{C} \to \mathcal{D}$. This isomorphism witnesses the fact that the essential image factorization of $F$ is naturally isomorphic to $F$ itself.

CategoryTheory.Functor.EssSurj structure

(F : C ⥤ D)

Full source

/-- 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`. -/
@[stacks 001C]
class EssSurj (F : C ⥤ D) : Prop where
  /-- All the objects of the target category are in the essential image. -/
  mem_essImage (Y : D) : F.essImage Y

Essentially surjective functor

Informal description

A functor $F \colon C \to D$ is *essentially surjective* if for every object $Y$ in $D$, there exists an object $X$ in $C$ such that $F(X)$ is isomorphic to $Y$ in $D$. This means that every object in the target category $D$ is isomorphic to an object coming from the source category $C$ via $F$.

CategoryTheory.Functor.EssSurj.toEssImage instance

: EssSurj F.toEssImage

Full source

instance EssSurj.toEssImage : EssSurj F.toEssImage where
  mem_essImage := fun ⟨_, hY⟩ =>
    ⟨_, ⟨⟨_, _, hY.getIso.hom_inv_id, hY.getIso.inv_hom_id⟩⟩⟩

Essential Surjectivity of the Functor to the Essential Image

Informal description

The functor $F \colon \mathcal{C} \to \mathrm{EssImageSubcategory}(F)$ is essentially surjective. That is, for every object $Y$ in the essential image subcategory of $F$, there exists an object $X$ in $\mathcal{C}$ such that $F(X)$ is isomorphic to $Y$.

CategoryTheory.Functor.essSurj_of_surj theorem

(h : Function.Surjective F.obj) : EssSurj F

Full source

theorem essSurj_of_surj (h : Function.Surjective F.obj) : EssSurj F where
  mem_essImage Y := by
    obtain ⟨X, rfl⟩ := h Y
    apply obj_mem_essImage

Surjective Object Function Implies Essentially Surjective Functor

Informal description

If a functor $F \colon \mathcal{C} \to \mathcal{D}$ has a surjective object function (i.e., for every object $Y$ in $\mathcal{D}$, there exists an object $X$ in $\mathcal{C}$ such that $F(X) = Y$), then $F$ is essentially surjective.

CategoryTheory.Functor.objPreimage definition

(Y : D) : C

Full source

/-- 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 objPreimage (Y : D) : C :=
  essImage.witness (@EssSurj.mem_essImage _ _ _ _ F _ Y)

Preimage of an object under an essentially surjective functor

Informal description

Given an essentially surjective functor $ F \colon \mathcal{C} \to \mathcal{D} $ and an object $ Y $ in $ \mathcal{D} $, the function returns an object $ X $ in $ \mathcal{C} $ such that $ F(X) $ is isomorphic to $ Y $. This object $ X $ is called a *preimage* of $ Y $ under $ F $.

CategoryTheory.Functor.objObjPreimageIso definition

(Y : D) : F.obj (F.objPreimage Y) ≅ Y

Full source

/-- Applying an essentially surjective functor to a preimage of `Y` yields an object that is
    isomorphic to `Y`. -/
def objObjPreimageIso (Y : D) : F.obj (F.objPreimage Y) ≅ Y :=
  Functor.essImage.getIso _

Isomorphism between image of preimage and target object

Informal description

For an essentially surjective functor $ F \colon \mathcal{C} \to \mathcal{D} $ and an object $ Y $ in $ \mathcal{D} $, there exists an isomorphism between $ F(X) $ and $ Y $, where $ X $ is a preimage of $ Y $ under $ F $. This isomorphism witnesses that $ Y $ is in the essential image of $ F $.

CategoryTheory.Functor.Faithful.toEssImage instance

(F : C ⥤ D) [Faithful F] : Faithful F.toEssImage

Full source

/-- The induced functor of a faithful functor is faithful. -/
instance Faithful.toEssImage (F : C ⥤ D) [Faithful F] : Faithful F.toEssImage := by
  dsimp only [Functor.toEssImage]
  infer_instance

Faithfulness of the Induced Functor to the Essential Image

Informal description

For any faithful functor $ F \colon \mathcal{C} \to \mathcal{D} $, the induced functor $ F.\mathrm{toEssImage} \colon \mathcal{C} \to F.\mathrm{EssImageSubcategory} $ is also faithful. This means that $ F.\mathrm{toEssImage} $ reflects the injectivity of morphisms, i.e., if $ F.\mathrm{toEssImage}(f) = F.\mathrm{toEssImage}(g) $ for two morphisms $ f, g $ in $ \mathcal{C} $, then $ f = g $.

CategoryTheory.Functor.Full.toEssImage instance

(F : C ⥤ D) [Full F] : Full F.toEssImage

Full source

/-- The induced functor of a full functor is full. -/
instance Full.toEssImage (F : C ⥤ D) [Full F] : Full F.toEssImage := by
  dsimp only [Functor.toEssImage]
  infer_instance

Fullness of the Induced Functor to the Essential Image

Informal description

For any full functor $ F \colon \mathcal{C} \to \mathcal{D} $, the induced functor $ F.\mathrm{toEssImage} \colon \mathcal{C} \to F.\mathrm{EssImageSubcategory} $ is also full. This means that for any two objects $ X, Y $ in $ \mathcal{C} $, the map $ \mathrm{Hom}(X, Y) \to \mathrm{Hom}(F(X), F(Y)) $ is surjective, where the codomain is restricted to morphisms in the essential image subcategory.

CategoryTheory.Functor.instEssSurjId instance

: EssSurj (𝟭 C)

Full source

instance instEssSurjId : EssSurj (𝟭 C) where
  mem_essImage Y := ⟨Y, ⟨Iso.refl _⟩⟩

Essential Surjectivity of the Identity Functor

Informal description

The identity functor $\text{id}_C \colon C \to C$ is essentially surjective. That is, for every object $X$ in $C$, there exists an object $Y$ in $C$ (namely $X$ itself) such that $\text{id}_C(Y) \cong X$.

CategoryTheory.Functor.essSurj_of_iso theorem

{F G : C ⥤ D} [EssSurj F] (α : F ≅ G) : EssSurj G

Full source

lemma essSurj_of_iso {F G : C ⥤ D} [EssSurj F] (α : F ≅ G) : EssSurj G where
  mem_essImage Y := Functor.essImage.ofNatIso α (EssSurj.mem_essImage Y)

Essential Surjectivity is Preserved by Natural Isomorphism

Informal description

Let $F, G \colon \mathcal{C} \to \mathcal{D}$ be functors with a natural isomorphism $\alpha \colon F \cong G$. If $F$ is essentially surjective, then $G$ is also essentially surjective.

CategoryTheory.Functor.essSurj_comp instance

(F : C ⥤ D) (G : D ⥤ E) [F.EssSurj] [G.EssSurj] : (F ⋙ G).EssSurj

Full source

instance essSurj_comp (F : C ⥤ D) (G : D ⥤ E) [F.EssSurj] [G.EssSurj] :
    (F ⋙ G).EssSurj where
  mem_essImage Z := ⟨_, ⟨G.mapIso (F.objObjPreimageIso _) ≪≫ G.objObjPreimageIso Z⟩⟩

Composition of Essentially Surjective Functors is Essentially Surjective

Informal description

For any essentially surjective functor $F \colon \mathcal{C} \to \mathcal{D}$ and any essentially surjective functor $G \colon \mathcal{D} \to \mathcal{E}$, the composition $F \circ G \colon \mathcal{C} \to \mathcal{E}$ is also essentially surjective. This means that for every object $Z$ in $\mathcal{E}$, there exists an object $X$ in $\mathcal{C}$ such that $(F \circ G)(X)$ is isomorphic to $Z$.

CategoryTheory.Functor.essSurj_of_comp_fully_faithful theorem

(F : C ⥤ D) (G : D ⥤ E) [(F ⋙ G).EssSurj] [G.Faithful] [G.Full] : F.EssSurj

Full source

lemma essSurj_of_comp_fully_faithful (F : C ⥤ D) (G : D ⥤ E) [(F ⋙ G).EssSurj]
    [G.Faithful] [G.Full] : F.EssSurj where
  mem_essImage X := ⟨_, ⟨G.preimageIso ((F ⋙ G).objObjPreimageIso (G.obj X))⟩⟩

Essential Surjectivity Inherited from Composition with Fully Faithful Functor

Informal description

Let $F \colon \mathcal{C} \to \mathcal{D}$ and $G \colon \mathcal{D} \to \mathcal{E}$ be functors such that the composition $F \circ G$ is essentially surjective, and $G$ is fully faithful. Then $F$ is essentially surjective.

CategoryTheory.Functor.essImage_comp_apply_of_essSurj theorem

: (F ⋙ G).essImage X ↔ G.essImage X

Full source

/-- Pre-composing by an essentially surjective functor doesn't change the essential image. -/
lemma essImage_comp_apply_of_essSurj : (F ⋙ G).essImage X ↔ G.essImage X where
  mp := fun ⟨Y, ⟨e⟩⟩ ↦ ⟨F.obj Y, ⟨e⟩⟩
  mpr := fun ⟨Y, ⟨e⟩⟩ ↦
    let ⟨Z, ⟨e'⟩⟩ := Functor.EssSurj.mem_essImage Y; ⟨Z, ⟨(G.mapIso e').trans e⟩⟩

Essential Image Preservation under Essentially Surjective Functor Composition: $(F \circ G).\text{essImage}(X) \leftrightarrow G.\text{essImage}(X)$

Informal description

For any object $X$ in the target category, $X$ belongs to the essential image of the composition $F \circ G$ if and only if $X$ belongs to the essential image of $G$, provided that $F$ is essentially surjective.

CategoryTheory.Functor.essImage_comp_of_essSurj theorem

: (F ⋙ G).essImage = G.essImage

Full source

/-- Pre-composing by an essentially surjective functor doesn't change the essential image. -/
@[simp] lemma essImage_comp_of_essSurj : (F ⋙ G).essImage = G.essImage :=
  funext fun _X ↦ propext essImage_comp_apply_of_essSurj

Essential Image Equality under Composition with Essentially Surjective Functor: $(F \circ G).\text{essImage} = G.\text{essImage}$

Informal description

For functors $F \colon \mathcal{C} \to \mathcal{D}$ and $G \colon \mathcal{D} \to \mathcal{E}$, if $F$ is essentially surjective, then the essential image of the composition $F \circ G$ is equal to the essential image of $G$. That is, $(F \circ G).\text{essImage} = G.\text{essImage}$.

CategoryTheory.Functor.essImage.liftFunctor definition

: J ⥤ C

Full source

/-- Lift a functor `G : J ⥤ D` to the essential image of a fully functor `F : C ⥤ D` to a functor
`G' : J ⥤ C` such that `G' ⋙ F ≅ G`. See `essImage.liftFunctorCompIso`. -/
@[simps] def essImage.liftFunctor : J ⥤ C where
  obj j := F.toEssImage.objPreimage ⟨G.obj j, hG j⟩
  -- TODO: `map` isn't type-correct:
  -- It conflates `⟨G.obj i, hG i⟩ ⟶ ⟨G.obj j, hG j⟩` and `G.obj i ⟶ G.obj j`.
  map {i j} f := F.preimage <|
    (F.toEssImage.objObjPreimageIso ⟨G.obj i, hG i⟩).hom ≫ G.map f ≫
      (F.toEssImage.objObjPreimageIso ⟨G.obj j, hG j⟩).inv
  map_id i := F.map_injective <| by
    simpa [-Iso.hom_inv_id] using (F.toEssImage.objObjPreimageIso ⟨G.obj i, hG i⟩).hom_inv_id
  map_comp {i j k} f g := F.map_injective <| by
    simp only [Functor.map_comp, Category.assoc, Functor.map_preimage]
    congr 2
    symm
    convert (F.toEssImage.objObjPreimageIso ⟨G.obj j, hG j⟩).inv_hom_id_assoc (G.map g ≫
      (F.toEssImage.objObjPreimageIso ⟨G.obj k, hG k⟩).inv)

Lift of a functor to the essential image

Informal description

Given a fully faithful functor $ F : \mathcal{C} \to \mathcal{D} $ and a functor $ G : \mathcal{J} \to \mathcal{D} $ whose image lies in the essential image of $ F $, the functor `essImage.liftFunctor` constructs a lift $ G' : \mathcal{J} \to \mathcal{C} $ such that the composition $ G' \circ F $ is naturally isomorphic to $ G $. On objects, $ G' $ maps $ j \in \mathcal{J} $ to a preimage $ X \in \mathcal{C} $ such that $ F(X) $ is isomorphic to $ G(j) $. On morphisms, $ G' $ maps $ f : i \to j $ to the unique morphism in $ \mathcal{C} $ (guaranteed by full faithfulness of $ F $) that corresponds to the composition of the isomorphism $ F(X_i) \cong G(i) $, the morphism $ G(f) $, and the inverse of the isomorphism $ F(X_j) \cong G(j) $.

CategoryTheory.Functor.essImage.liftFunctorCompIso definition

: essImage.liftFunctor G F hG ⋙ F ≅ G

Full source

/-- A functor `G : J ⥤ D` to the essential image of a fully functor `F : C ⥤ D` does factor through
`essImage.liftFunctor G F hG`. -/
@[simps!] def essImage.liftFunctorCompIso : essImage.liftFunctoressImage.liftFunctor G F hG ⋙ FessImage.liftFunctor G F hG ⋙ F ≅ G :=
  NatIso.ofComponents
    (fun i ↦ F.essImage.ι.mapIso (F.toEssImage.objObjPreimageIso ⟨G.obj i, hG _⟩))
      fun {i j} f ↦ by
    simp only [Functor.comp_obj, liftFunctor_obj, Functor.comp_map, liftFunctor_map,
      Functor.map_preimage, Functor.mapIso_hom, ObjectProperty.ι_map, Category.assoc]
    congr 1
    convert Category.comp_id _
    exact (F.toEssImage.objObjPreimageIso ⟨G.obj j, hG j⟩).inv_hom_id

Natural isomorphism between lift composition and original functor

Informal description

Given a fully faithful functor $ F : \mathcal{C} \to \mathcal{D} $ and a functor $ G : \mathcal{J} \to \mathcal{D} $ whose image lies in the essential image of $ F $, there exists a natural isomorphism between the composition of the lifted functor $ \mathrm{essImage.liftFunctor}\,G\,F\,hG $ with $ F $ and $ G $. Concretely, for each object $ i $ in $ \mathcal{J} $, the isomorphism is given by the image under $ F $ of the isomorphism between $ F(X_i) $ and $ G(i) $, where $ X_i $ is a preimage of $ G(i) $ under $ F $. The naturality condition ensures that these isomorphisms commute with the morphisms in $ \mathcal{J} $.