Mathlib.CategoryTheory.Limits.Shapes.Images

CategoryTheory.Limits.MonoFactorisation structure

(f : X ⟶ Y)

Full source

/-- A factorisation of a morphism `f = e ≫ m`, with `m` monic. -/
structure MonoFactorisation (f : X ⟶ Y) where
  I : C -- Porting note: violates naming conventions but can't think a better replacement
  m : I ⟶ Y
  [m_mono : Mono m]
  e : X ⟶ I
  fac : e ≫ m = f := by aesop_cat

Monomorphism Factorization

Informal description

A `MonoFactorisation` of a morphism $f \colon X \to Y$ in a category is a factorization $f = e \circ m$ where $m$ is a monomorphism. Here $e \colon X \to I$ and $m \colon I \to Y$ are morphisms, with $I$ being some intermediate object.

CategoryTheory.Limits.MonoFactorisation.self definition

[Mono f] : MonoFactorisation f

Full source

/-- The obvious factorisation of a monomorphism through itself. -/
def self [Mono f] : MonoFactorisation f where
  I := X
  m := f
  e := 𝟙 X

-- I'm not sure we really need this, but the linter says that an inhabited instance
-- ought to exist...

Trivial monomorphism factorization

Informal description

Given a monomorphism $ f : X \to Y $ in a category, the trivial factorization of $ f $ is given by $ f = \text{id}_X \circ f $, where $\text{id}_X$ is the identity morphism on $ X $. This defines a monomorphism factorization where the intermediate object $ I $ is $ X $ itself, the monomorphism $ m $ is $ f $, and the morphism $ e $ is the identity morphism on $ X $.

CategoryTheory.Limits.MonoFactorisation.instInhabitedOfMono instance

[Mono f] : Inhabited (MonoFactorisation f)

Full source

instance [Mono f] : Inhabited (MonoFactorisation f) := ⟨self f⟩

Existence of Trivial Monomorphism Factorization

Informal description

For any monomorphism $f \colon X \to Y$ in a category, there exists a trivial monomorphism factorization of $f$ given by $f = \text{id}_X \circ f$, where $\text{id}_X$ is the identity morphism on $X$.

CategoryTheory.Limits.MonoFactorisation.ext theorem

{F F' : MonoFactorisation f} (hI : F.I = F'.I) (hm : F.m = eqToHom hI ≫ F'.m) : F = F'

Full source

/-- The morphism `m` in a factorisation `f = e ≫ m` through a monomorphism is uniquely
determined. -/
@[ext (iff := false)]
theorem ext {F F' : MonoFactorisation f} (hI : F.I = F'.I)
    (hm : F.m = eqToHomeqToHom hI ≫ F'.m) : F = F' := by
  obtain ⟨_, Fm, _, Ffac⟩ := F; obtain ⟨_, Fm', _, Ffac'⟩ := F'
  cases hI
  simp? at hm says simp only [eqToHom_refl, Category.id_comp] at hm
  congr
  apply (cancel_mono Fm).1
  rw [Ffac, hm, Ffac']

Uniqueness of Monomorphism Factorization up to Intermediate Object Equality

Informal description

Given two monomorphism factorizations $F$ and $F'$ of a morphism $f \colon X \to Y$ in a category, if their intermediate objects are equal (i.e., $F.I = F'.I$) and their monomorphism parts satisfy $F.m = \text{eqToHom}(hI) \circ F'.m$, then the two factorizations are equal ($F = F'$).

CategoryTheory.Limits.MonoFactorisation.compMono definition

(F : MonoFactorisation f) {Y' : C} (g : Y ⟶ Y') [Mono g] : MonoFactorisation (f ≫ g)

Full source

/-- Any mono factorisation of `f` gives a mono factorisation of `f ≫ g` when `g` is a mono. -/
@[simps]
def compMono (F : MonoFactorisation f) {Y' : C} (g : Y ⟶ Y') [Mono g] :
    MonoFactorisation (f ≫ g) where
  I := F.I
  m := F.m ≫ g
  m_mono := mono_comp _ _
  e := F.e

Monomorphism factorization of a composition with a monomorphism

Informal description

Given a monomorphism factorization $F$ of a morphism $f \colon X \to Y$ in a category, and a monomorphism $g \colon Y \to Y'$, the composition $f \circ g$ has a monomorphism factorization with the same intermediate object $I$ as $F$, where the monomorphism part is $F.m \circ g$ and the epimorphism part remains $F.e$.

CategoryTheory.Limits.MonoFactorisation.ofCompIso definition

{Y' : C} {g : Y ⟶ Y'} [IsIso g] (F : MonoFactorisation (f ≫ g)) : MonoFactorisation f

Full source

/-- A mono factorisation of `f ≫ g`, where `g` is an isomorphism,
gives a mono factorisation of `f`. -/
@[simps]
def ofCompIso {Y' : C} {g : Y ⟶ Y'} [IsIso g] (F : MonoFactorisation (f ≫ g)) :
    MonoFactorisation f where
  I := F.I
  m := F.m ≫ inv g
  m_mono := mono_comp _ _
  e := F.e

Monomorphism factorization from composition with isomorphism

Informal description

Given a morphism $ g : Y \to Y' $ in a category $ C $ that is an isomorphism, and a monomorphism factorization $ F $ of the composition $ f \circ g $, this constructs a monomorphism factorization of $ f $ itself. The intermediate object $ I $ remains the same, the monomorphism part becomes $ F.m \circ g^{-1} $, and the epimorphism part remains $ F.e $.

CategoryTheory.Limits.MonoFactorisation.isoComp definition

(F : MonoFactorisation f) {X' : C} (g : X' ⟶ X) : MonoFactorisation (g ≫ f)

Full source

/-- Any mono factorisation of `f` gives a mono factorisation of `g ≫ f`. -/
@[simps]
def isoComp (F : MonoFactorisation f) {X' : C} (g : X' ⟶ X) : MonoFactorisation (g ≫ f) where
  I := F.I
  m := F.m
  e := g ≫ F.e

Monomorphism factorization of a composition with a morphism

Informal description

Given a monomorphism factorization $F$ of a morphism $f \colon X \to Y$ in a category, and a morphism $g \colon X' \to X$, the composition $g \circ f$ has a monomorphism factorization with the same intermediate object $I$ as $F$, where the monomorphism part is $F.m$ and the epimorphism part is the composition $g \circ F.e$.

CategoryTheory.Limits.MonoFactorisation.ofIsoComp definition

{X' : C} (g : X' ⟶ X) [IsIso g] (F : MonoFactorisation (g ≫ f)) : MonoFactorisation f

Full source

/-- A mono factorisation of `g ≫ f`, where `g` is an isomorphism,
gives a mono factorisation of `f`. -/
@[simps]
def ofIsoComp {X' : C} (g : X' ⟶ X) [IsIso g] (F : MonoFactorisation (g ≫ f)) :
    MonoFactorisation f where
  I := F.I
  m := F.m
  e := inv g ≫ F.e

Monomorphism factorization from composition with isomorphism

Informal description

Given an isomorphism $ g : X' \to X $ and a monomorphism factorization $ F $ of the composition $ g \circ f $, the function constructs a monomorphism factorization of $ f $ by setting the intermediate object to be $ F.I $, the monomorphism to be $ F.m $, and the morphism from $ X $ to $ F.I $ to be the composition of the inverse of $ g $ with $ F.e $.

CategoryTheory.Limits.MonoFactorisation.ofArrowIso definition

{f g : Arrow C} (F : MonoFactorisation f.hom) (sq : f ⟶ g) [IsIso sq] : MonoFactorisation g.hom

Full source

/-- If `f` and `g` are isomorphic arrows, then a mono factorisation of `f`
gives a mono factorisation of `g` -/
@[simps]
def ofArrowIso {f g : Arrow C} (F : MonoFactorisation f.hom) (sq : f ⟶ g) [IsIso sq] :
    MonoFactorisation g.hom where
  I := F.I
  m := F.m ≫ sq.right
  e := invinv sq.left ≫ F.e
  m_mono := mono_comp _ _
  fac := by simp only [fac_assoc, Arrow.w, IsIso.inv_comp_eq, Category.assoc]

Monomorphism factorization induced by an isomorphism in the arrow category

Informal description

Given two isomorphic morphisms $ f $ and $ g $ in the arrow category of $ C $, represented by a commutative square $ sq \colon f \to g $ that is an isomorphism, and given a monomorphism factorization $ F $ of $ f $, this constructs a monomorphism factorization of $ g $. Specifically, the factorization is given by: - The intermediate object $ I $ remains the same as in $ F $. - The monomorphism $ m $ is the composition of $ F.m $ with the right morphism of $ sq $. - The morphism $ e $ is the composition of the inverse of the left morphism of $ sq $ with $ F.e $.

CategoryTheory.Limits.IsImage structure

(F : MonoFactorisation f)

Full source

/-- Data exhibiting that a given factorisation through a mono is initial. -/
structure IsImage (F : MonoFactorisation f) where
  lift : ∀ F' : MonoFactorisation f, F.I ⟶ F'.I
  lift_fac : ∀ F' : MonoFactorisation f, lift F' ≫ F'.m = F.m := by aesop_cat

Universal property of a categorical image factorization

Informal description

A structure `IsImage F` asserts that a given monomorphism factorization `F` of a morphism `f : X ⟶ Y` in a category is the categorical image of `f`. This means that `F` provides a factorization `f = e ≫ m` through a monomorphism `m`, and that this factorization is universal in the sense that any other such factorization factors uniquely through `F`.

CategoryTheory.Limits.IsImage.fac_lift theorem

{F : MonoFactorisation f} (hF : IsImage F) (F' : MonoFactorisation f) : F.e ≫ hF.lift F' = F'.e

Full source

@[reassoc (attr := simp)]
theorem fac_lift {F : MonoFactorisation f} (hF : IsImage F) (F' : MonoFactorisation f) :
    F.e ≫ hF.lift F' = F'.e :=
  (cancel_mono F'.m).1 <| by simp

Factorization Property of Image Lifts

Informal description

Given a monomorphism factorization $F$ of a morphism $f \colon X \to Y$ in a category, if $F$ satisfies the universal property of being an image factorization (i.e., $hF \colon \text{IsImage} F$ holds), then for any other monomorphism factorization $F'$ of $f$, the composition of the morphism $F.e \colon X \to I$ (from $F$) with the unique lift morphism $hF.\text{lift} F' \colon I \to I'$ (from $F$ to $F'$) equals the morphism $F'.e \colon X \to I'$ from $F'$. In other words, the diagram \[ X \xrightarrow{F.e} I \xrightarrow{hF.\text{lift} F'} I' \] commutes and equals $X \xrightarrow{F'.e} I'$.

CategoryTheory.Limits.IsImage.self definition

[Mono f] : IsImage (MonoFactorisation.self f)

Full source

/-- The trivial factorisation of a monomorphism satisfies the universal property. -/
@[simps]
def self [Mono f] : IsImage (MonoFactorisation.self f) where lift F' := F'.e

Trivial image factorization of a monomorphism

Informal description

Given a monomorphism $ f : X \to Y $ in a category, the trivial factorization $ f = \text{id}_X \circ f $ satisfies the universal property of being a categorical image factorization. This means that any other factorization of $ f $ through a monomorphism factors uniquely through this trivial factorization.

CategoryTheory.Limits.IsImage.instInhabitedSelf instance

[Mono f] : Inhabited (IsImage (MonoFactorisation.self f))

Full source

instance [Mono f] : Inhabited (IsImage (MonoFactorisation.self f)) :=
  ⟨self f⟩

Trivial Image Factorization of a Monomorphism

Informal description

For any monomorphism $f : X \to Y$ in a category, the trivial factorization $f = \text{id}_X \circ f$ satisfies the universal property of being a categorical image factorization. In other words, there exists an instance witnessing that this factorization is indeed an image factorization.

CategoryTheory.Limits.IsImage.isoExt definition

{F F' : MonoFactorisation f} (hF : IsImage F) (hF' : IsImage F') : F.I ≅ F'.I

Full source

/-- Two factorisations through monomorphisms satisfying the universal property
must factor through isomorphic objects. -/
@[simps]
def isoExt {F F' : MonoFactorisation f} (hF : IsImage F) (hF' : IsImage F') :
    F.I ≅ F'.I where
  hom := hF.lift F'
  inv := hF'.lift F
  hom_inv_id := (cancel_mono F.m).1 (by simp)
  inv_hom_id := (cancel_mono F'.m).1 (by simp)

Isomorphism between image factorizations

Informal description

Given two monomorphism factorizations $F$ and $F'$ of a morphism $f \colon X \to Y$ in a category, both satisfying the universal property of being a categorical image, there exists an isomorphism $\varphi \colon F.I \cong F'.I$ between their intermediate objects. This isomorphism makes the diagram commute, meaning $\varphi \circ F'.m = F.m$ and $\varphi^{-1} \circ F.m = F'.m$.

CategoryTheory.Limits.IsImage.isoExt_hom_m theorem

: (isoExt hF hF').hom ≫ F'.m = F.m

Full source

theorem isoExt_hom_m : (isoExt hF hF').hom ≫ F'.m = F.m := by simp

Commutativity of isomorphism with monomorphisms in image factorization

Informal description

Given two monomorphism factorizations $F$ and $F'$ of a morphism $f \colon X \to Y$ in a category, both satisfying the universal property of being a categorical image, the isomorphism $\varphi \colon F.I \cong F'.I$ between their intermediate objects satisfies $\varphi \circ F'.m = F.m$.

CategoryTheory.Limits.IsImage.isoExt_inv_m theorem

: (isoExt hF hF').inv ≫ F.m = F'.m

Full source

theorem isoExt_inv_m : (isoExt hF hF').inv ≫ F.m = F'.m := by simp

Inverse isomorphism preserves factorization in categorical image

Informal description

Given two monomorphism factorizations $F$ and $F'$ of a morphism $f \colon X \to Y$ in a category, both satisfying the universal property of being a categorical image, the inverse of the isomorphism $\varphi \colon F.I \cong F'.I$ between their intermediate objects satisfies $\varphi^{-1} \circ F.m = F'.m$.

CategoryTheory.Limits.IsImage.e_isoExt_hom theorem

: F.e ≫ (isoExt hF hF').hom = F'.e

Full source

theorem e_isoExt_hom : F.e ≫ (isoExt hF hF').hom = F'.e := by simp

Commutativity of image factorization morphisms with isomorphism

Informal description

Given two monomorphism factorizations $F$ and $F'$ of a morphism $f \colon X \to Y$ in a category, both satisfying the universal property of being a categorical image, the composition of the morphism $F.e \colon X \to F.I$ with the isomorphism $\varphi \colon F.I \cong F'.I$ equals the morphism $F'.e \colon X \to F'.I$. In other words, the diagram \[ X \xrightarrow{F.e} F.I \xrightarrow{\varphi} F'.I \] commutes and equals $X \xrightarrow{F'.e} F'.I$.

CategoryTheory.Limits.IsImage.e_isoExt_inv theorem

: F'.e ≫ (isoExt hF hF').inv = F.e

Full source

theorem e_isoExt_inv : F'.e ≫ (isoExt hF hF').inv = F.e := by simp

Commutativity of inverse image isomorphism with factorization morphisms

Informal description

Given two monomorphism factorizations $F$ and $F'$ of a morphism $f \colon X \to Y$ in a category, both satisfying the universal property of being a categorical image, the composition of the morphism $F'.e \colon X \to I'$ with the inverse of the isomorphism $\varphi \colon F.I \cong F'.I$ equals the morphism $F.e \colon X \to I$. In other words, the diagram \[ X \xrightarrow{F'.e} I' \xrightarrow{\varphi^{-1}} I \] commutes and equals $X \xrightarrow{F.e} I$.

CategoryTheory.Limits.IsImage.ofArrowIso definition

{f g : Arrow C} {F : MonoFactorisation f.hom} (hF : IsImage F) (sq : f ⟶ g) [IsIso sq] : IsImage (F.ofArrowIso sq)

Full source

/-- If `f` and `g` are isomorphic arrows, then a mono factorisation of `f` that is an image
gives a mono factorisation of `g` that is an image -/
@[simps]
def ofArrowIso {f g : Arrow C} {F : MonoFactorisation f.hom} (hF : IsImage F) (sq : f ⟶ g)
    [IsIso sq] : IsImage (F.ofArrowIso sq) where
  lift F' := hF.lift (F'.ofArrowIso (inv sq))
  lift_fac F' := by
    simpa only [MonoFactorisation.ofArrowIso_m, Arrow.inv_right, ← Category.assoc,
      IsIso.comp_inv_eq] using hF.lift_fac (F'.ofArrowIso (inv sq))

Image factorization property preserved under isomorphism in the arrow category

Informal description

Given two isomorphic morphisms $ f $ and $ g $ in the arrow category of $ C $, represented by a commutative square $ sq \colon f \to g $ that is an isomorphism, and given a monomorphism factorization $ F $ of $ f $ that satisfies the universal property of an image factorization, the induced monomorphism factorization $ F.\text{ofArrowIso} \, sq $ of $ g $ also satisfies the universal property of an image factorization. Specifically, for any other monomorphism factorization $ F' $ of $ g $, there exists a unique morphism $ \text{lift} \, F' $ that makes the appropriate diagram commute, constructed using the universal property of $ F $ applied to the factorization $ F'.\text{ofArrowIso} \, (\text{inv} \, sq) $.

CategoryTheory.Limits.ImageFactorisation structure

(f : X ⟶ Y)

Full source

/-- Data exhibiting that a morphism `f` has an image. -/
structure ImageFactorisation (f : X ⟶ Y) where
  F : MonoFactorisation f -- Porting note: another violation of the naming convention
  isImage : IsImage F

Image factorisation of a morphism

Informal description

An image factorisation of a morphism $f \colon X \to Y$ in a category consists of a factorisation $f = e \circ m$ where $m$ is a monomorphism, with the universal property that any other such factorisation factors through it.

CategoryTheory.Limits.ImageFactorisation.instInhabitedOfMono instance

[Mono f] : Inhabited (ImageFactorisation f)

Full source

instance [Mono f] : Inhabited (ImageFactorisation f) :=
  ⟨⟨_, IsImage.self f⟩⟩

Trivial Image Factorisation for Monomorphisms

Informal description

For any monomorphism $f : X \to Y$ in a category, there exists a trivial image factorisation of $f$ given by $f = \text{id}_X \circ f$, where $\text{id}_X$ is the identity morphism on $X$.

CategoryTheory.Limits.ImageFactorisation.ofArrowIso definition

{f g : Arrow C} (F : ImageFactorisation f.hom) (sq : f ⟶ g) [IsIso sq] : ImageFactorisation g.hom

Full source

/-- If `f` and `g` are isomorphic arrows, then an image factorisation of `f`
gives an image factorisation of `g` -/
@[simps]
def ofArrowIso {f g : Arrow C} (F : ImageFactorisation f.hom) (sq : f ⟶ g) [IsIso sq] :
    ImageFactorisation g.hom where
  F := F.F.ofArrowIso sq
  isImage := F.isImage.ofArrowIso sq

Image factorization induced by an isomorphism in the arrow category

Informal description

Given two isomorphic morphisms $ f $ and $ g $ in the arrow category of $ C $, represented by a commutative square $ sq \colon f \to g $ that is an isomorphism, and given an image factorization $ F $ of $ f $, this constructs an image factorization of $ g $. Specifically, the factorization is obtained by applying the isomorphism $ sq $ to the monomorphism factorization $ F $, ensuring that the universal property of image factorizations is preserved.

CategoryTheory.Limits.HasImage structure

(f : X ⟶ Y)

Full source

/-- `HasImage f` means that there exists an image factorisation of `f`. -/
class HasImage (f : X ⟶ Y) : Prop where mk' ::
  exists_image : Nonempty (ImageFactorisation f)

Existence of Image Factorization for a Morphism

Informal description

The structure `HasImage f` asserts that a morphism $ f : X \to Y $ in a category can be factorized as $ f = e \circ m $, where $ m $ is a monomorphism. This factorization is called an image factorization of $ f $.

CategoryTheory.Limits.HasImage.mk theorem

{f : X ⟶ Y} (F : ImageFactorisation f) : HasImage f

Full source

theorem HasImage.mk {f : X ⟶ Y} (F : ImageFactorisation f) : HasImage f :=
  ⟨Nonempty.intro F⟩

Existence of Image Factorisation from Given Factorisation

Informal description

Given a morphism $f \colon X \to Y$ in a category $\mathcal{C}$ and an image factorisation $F$ of $f$ (i.e., a factorisation $f = e \circ m$ where $m$ is a monomorphism), there exists an image factorisation structure for $f$.

CategoryTheory.Limits.HasImage.of_arrow_iso theorem

{f g : Arrow C} [h : HasImage f.hom] (sq : f ⟶ g) [IsIso sq] : HasImage g.hom

Full source

theorem HasImage.of_arrow_iso {f g : Arrow C} [h : HasImage f.hom] (sq : f ⟶ g) [IsIso sq] :
    HasImage g.hom :=
  ⟨⟨h.exists_image.some.ofArrowIso sq⟩⟩

Preservation of Image Factorization under Isomorphism in Arrow Category

Informal description

Let $f$ and $g$ be morphisms in a category $C$, viewed as objects in the arrow category $\mathrm{Arrow}(C)$. If $f$ has an image factorization and there exists an isomorphism $sq : f \to g$ in $\mathrm{Arrow}(C)$, then $g$ also has an image factorization.

CategoryTheory.Limits.mono_hasImage instance

(f : X ⟶ Y) [Mono f] : HasImage f

Full source

instance (priority := 100) mono_hasImage (f : X ⟶ Y) [Mono f] : HasImage f :=
  HasImage.mk ⟨_, IsImage.self f⟩

Existence of Image Factorization for Monomorphisms

Informal description

For any monomorphism $f \colon X \to Y$ in a category, there exists an image factorization of $f$.

CategoryTheory.Limits.Image.monoFactorisation definition

: MonoFactorisation f

Full source

/-- Some factorisation of `f` through a monomorphism (selected with choice). -/
def Image.monoFactorisation : MonoFactorisation f :=
  (Classical.choice HasImage.exists_image).F

Monomorphism factorization of a morphism

Informal description

The monomorphism factorization of a morphism $ f : X \to Y $ in a category, which is a factorization $ f = e \circ m $ where $ m $ is a monomorphism. This factorization is chosen (via the axiom of choice) from all possible such factorizations that exist for $ f $.

CategoryTheory.Limits.Image.isImage definition

: IsImage (Image.monoFactorisation f)

Full source

/-- The witness of the universal property for the chosen factorisation of `f` through
a monomorphism. -/
def Image.isImage : IsImage (Image.monoFactorisation f) :=
  (Classical.choice HasImage.exists_image).isImage

Universal property of the categorical image factorization

Informal description

The structure `Image.isImage` asserts that the chosen monomorphism factorization of a morphism $ f : X \to Y $ satisfies the universal property of the categorical image. This means that the factorization $ f = e \circ m $ through the monomorphism $ m $ is universal among all such factorizations, in the sense that any other factorization of $ f $ through a monomorphism factors uniquely through this one.

CategoryTheory.Limits.image definition

: C

Full source

/-- The categorical image of a morphism. -/
def image : C :=
  (Image.monoFactorisation f).I

Image object of a morphism

Informal description

The object representing the image of a morphism $ f : X \to Y $ in a category, obtained from the monomorphism factorization $ f = e \circ m $ where $ m $ is a monomorphism. This object is chosen (via the axiom of choice) from all possible such factorizations that exist for $ f $.

CategoryTheory.Limits.image.ι definition

: image f ⟶ Y

Full source

/-- The inclusion of the image of a morphism into the target. -/
def image.ι : imageimage f ⟶ Y :=
  (Image.monoFactorisation f).m

Image inclusion morphism

Informal description

The monomorphism $ \iota : \text{image}(f) \to Y $ is the inclusion of the image object of a morphism $ f : X \to Y $ into its target object $ Y $, obtained from the monomorphism factorization $ f = e \circ \iota $.

CategoryTheory.Limits.image.as_ι theorem

: (Image.monoFactorisation f).m = image.ι f

Full source

@[simp]
theorem image.as_ι : (Image.monoFactorisation f).m = image.ι f := rfl

Image Factorization Monomorphism Equals Image Inclusion

Informal description

The monomorphism $m$ in the chosen monomorphism factorization of a morphism $f : X \to Y$ is equal to the image inclusion morphism $\iota : \text{image}(f) \to Y$.

CategoryTheory.Limits.instMonoι instance

: Mono (image.ι f)

Full source

instance : Mono (image.ι f) :=
  (Image.monoFactorisation f).m_mono

Monomorphism Property of Image Inclusion

Informal description

The inclusion morphism $\iota : \text{image}(f) \to Y$ of the image factorization of a morphism $f : X \to Y$ is a monomorphism.

CategoryTheory.Limits.factorThruImage definition

: X ⟶ image f

Full source

/-- The map from the source to the image of a morphism. -/
def factorThruImage : X ⟶ image f :=
  (Image.monoFactorisation f).e

Factorization through the image of a morphism

Informal description

The morphism from the source object $ X $ to the image object of a morphism $ f : X \to Y $ in a category, obtained as part of the monomorphism factorization $ f = e \circ m $, where $ m $ is a monomorphism. This morphism $ e $ is the first part of the factorization, satisfying $ e \circ m = f $.

CategoryTheory.Limits.as_factorThruImage theorem

: (Image.monoFactorisation f).e = factorThruImage f

Full source

/-- Rewrite in terms of the `factorThruImage` interface. -/
@[simp]
theorem as_factorThruImage : (Image.monoFactorisation f).e = factorThruImage f :=
  rfl

Equality of Factorization Morphisms in Image Factorization

Informal description

For a morphism $f \colon X \to Y$ in a category with image factorization, the morphism $e$ in the chosen monomorphism factorization $(e, m)$ of $f$ (where $m$ is a monomorphism) is equal to the canonical factorization morphism $\text{factorThruImage}\, f \colon X \to \text{image}\, f$.

CategoryTheory.Limits.image.fac theorem

: factorThruImage f ≫ image.ι f = f

Full source

@[reassoc (attr := simp)]
theorem image.fac : factorThruImagefactorThruImage f ≫ image.ι f = f :=
  (Image.monoFactorisation f).fac

Factorization Property of Image: $\text{factorThruImage}\, f \circ \iota = f$

Informal description

For a morphism $f \colon X \to Y$ in a category, the composition of the factorization morphism $\text{factorThruImage}\, f \colon X \to \text{image}(f)$ with the image inclusion morphism $\iota \colon \text{image}(f) \to Y$ equals $f$. That is, the diagram \[ X \xrightarrow{\text{factorThruImage}\, f} \text{image}(f) \xrightarrow{\iota} Y \] commutes and equals $f$.

CategoryTheory.Limits.image.lift definition

(F' : MonoFactorisation f) : image f ⟶ F'.I

Full source

/-- Any other factorisation of the morphism `f` through a monomorphism receives a map from the
image. -/
def image.lift (F' : MonoFactorisation f) : imageimage f ⟶ F'.I :=
  (Image.isImage f).lift F'

Universal lift from image factorization

Informal description

Given a monomorphism factorization $ F' $ of a morphism $ f \colon X \to Y $ in a category, the morphism $ \text{image.lift} \, F' $ from the image object of $ f $ to the intermediate object $ F'.I $ of $ F' $ is the unique morphism making the diagram commute, where the factorization through the image is universal among all such factorizations.

CategoryTheory.Limits.image.lift_fac theorem

(F' : MonoFactorisation f) : image.lift F' ≫ F'.m = image.ι f

Full source

@[reassoc (attr := simp)]
theorem image.lift_fac (F' : MonoFactorisation f) : image.liftimage.lift F' ≫ F'.m = image.ι f :=
  (Image.isImage f).lift_fac F'

Commutativity of the universal lift with the monomorphism in image factorization

Informal description

Given a monomorphism factorization $F'$ of a morphism $f \colon X \to Y$ in a category, the composition of the universal lift morphism $\text{image.lift}\, F' \colon \text{image}(f) \to F'.I$ with the monomorphism $F'.m \colon F'.I \to Y$ equals the image inclusion morphism $\iota \colon \text{image}(f) \to Y$. In other words, the diagram \[ \text{image}(f) \xrightarrow{\text{image.lift}\, F'} F'.I \xrightarrow{F'.m} Y \] commutes and equals $\iota$.

CategoryTheory.Limits.image.fac_lift theorem

(F' : MonoFactorisation f) : factorThruImage f ≫ image.lift F' = F'.e

Full source

@[reassoc (attr := simp)]
theorem image.fac_lift (F' : MonoFactorisation f) : factorThruImagefactorThruImage f ≫ image.lift F' = F'.e :=
  (Image.isImage f).fac_lift F'

Commutativity of Factorization and Lift in Image Construction

Informal description

Given a monomorphism factorization $F'$ of a morphism $f \colon X \to Y$ in a category, the composition of the factorization morphism $\text{factorThruImage}\, f \colon X \to \text{image}(f)$ with the universal lift morphism $\text{image.lift}\, F' \colon \text{image}(f) \to F'.I$ equals the morphism $F'.e \colon X \to F'.I$ from the factorization $F'$. In other words, the diagram \[ X \xrightarrow{\text{factorThruImage}\, f} \text{image}(f) \xrightarrow{\text{image.lift}\, F'} F'.I \] commutes and equals $X \xrightarrow{F'.e} F'.I$.

CategoryTheory.Limits.image.isImage_lift theorem

(F : MonoFactorisation f) : (Image.isImage f).lift F = image.lift F

Full source

@[simp]
theorem image.isImage_lift (F : MonoFactorisation f) : (Image.isImage f).lift F = image.lift F :=
  rfl

Universal Lift of Image Factorization Coincides with Image Lift

Informal description

For any monomorphism factorization $F$ of a morphism $f \colon X \to Y$ in a category, the universal lift morphism constructed via the image factorization property coincides with the image lift morphism, i.e., \[ (\text{Image.isImage}\, f).\text{lift}\, F = \text{image.lift}\, F. \]

CategoryTheory.Limits.IsImage.lift_ι theorem

{F : MonoFactorisation f} (hF : IsImage F) : hF.lift (Image.monoFactorisation f) ≫ image.ι f = F.m

Full source

@[reassoc (attr := simp)]
theorem IsImage.lift_ι {F : MonoFactorisation f} (hF : IsImage F) :
    hF.lift (Image.monoFactorisation f) ≫ image.ι f = F.m :=
  hF.lift_fac _

Commutativity of Image Factorization Lifting with Monomorphism

Informal description

Let $f : X \to Y$ be a morphism in a category, and let $F$ be a monomorphism factorization of $f$ (i.e., $f = e \circ m$ where $m$ is a monomorphism). If $F$ satisfies the universal property of being an image factorization (i.e., $hF : \text{IsImage} F$ holds), then the lifting morphism $hF.\text{lift}$ applied to the chosen image factorization of $f$ composed with the image inclusion $\iota_f$ equals the monomorphism $m$ from the factorization $F$. In symbols: $hF.\text{lift}(\text{Image.monoFactorisation} f) \circ \iota_f = F.m$

CategoryTheory.Limits.image.lift_mono instance

(F' : MonoFactorisation f) : Mono (image.lift F')

Full source

instance image.lift_mono (F' : MonoFactorisation f) : Mono (image.lift F') := by
  refine @mono_of_mono _ _ _ _ _ _ F'.m ?_
  simpa using MonoFactorisation.m_mono _

The Universal Lift from Image Factorization is a Monomorphism

Informal description

For any monomorphism factorization $F'$ of a morphism $f \colon X \to Y$ in a category, the universal lift morphism $\text{image.lift}\, F' \colon \text{image}(f) \to F'.I$ is a monomorphism.

CategoryTheory.Limits.HasImage.uniq theorem

(F' : MonoFactorisation f) (l : image f ⟶ F'.I) (w : l ≫ F'.m = image.ι f) : l = image.lift F'

Full source

theorem HasImage.uniq (F' : MonoFactorisation f) (l : imageimage f ⟶ F'.I) (w : l ≫ F'.m = image.ι f) :
    l = image.lift F' :=
  (cancel_mono F'.m).1 (by simp [w])

Uniqueness of the Universal Lift in Image Factorization

Informal description

Given a monomorphism factorization $F'$ of a morphism $f \colon X \to Y$ in a category, and a morphism $l \colon \text{image}(f) \to F'.I$ such that $l \circ F'.m = \iota_f$, where $\iota_f \colon \text{image}(f) \to Y$ is the image inclusion morphism, then $l$ must be equal to the universal lift morphism $\text{image.lift}\, F'$. In other words, the universal lift is the unique morphism making the following diagram commute: \[ \text{image}(f) \xrightarrow{l} F'.I \xrightarrow{F'.m} Y = \text{image}(f) \xrightarrow{\iota_f} Y \]

CategoryTheory.Limits.instHasImageCompOfIsIso instance

{X Y Z : C} (f : X ⟶ Y) [IsIso f] (g : Y ⟶ Z) [HasImage g] : HasImage (f ≫ g)

Full source

/-- If `has_image g`, then `has_image (f ≫ g)` when `f` is an isomorphism. -/
instance {X Y Z : C} (f : X ⟶ Y) [IsIso f] (g : Y ⟶ Z) [HasImage g] : HasImage (f ≫ g) where
  exists_image :=
    ⟨{  F :=
          { I := image g
            m := image.ι g
            e := f ≫ factorThruImage g }
        isImage :=
          { lift := fun F' => image.lift
                { I := F'.I
                  m := F'.m
                  e := inv f ≫ F'.e } } }⟩

Existence of Image Factorization for Compositions with Isomorphisms

Informal description

For any isomorphism $f \colon X \to Y$ in a category $\mathcal{C}$ and any morphism $g \colon Y \to Z$ that has an image factorization, the composition $f \circ g$ also has an image factorization.

CategoryTheory.Limits.HasImages structure

Full source

/-- `HasImages` asserts that every morphism has an image. -/
class HasImages : Prop where
  has_image : ∀ {X Y : C} (f : X ⟶ Y), HasImage f

Existence of images in a category

Informal description

A category `C` has images if every morphism `f : X ⟶ Y` in `C` can be factored as `f = e ≫ m`, where `m` is a monomorphism. This factorization is called the image factorization of `f`, and it satisfies the universal property that any other such factorization factors uniquely through it.

CategoryTheory.Limits.imageMonoIsoSource definition

[Mono f] : image f ≅ X

Full source

/-- The image of a monomorphism is isomorphic to the source. -/
def imageMonoIsoSource [Mono f] : imageimage f ≅ X :=
  IsImage.isoExt (Image.isImage f) (IsImage.self f)

Isomorphism between image and source for a monomorphism

Informal description

For any monomorphism $ f : X \to Y $ in a category, the image object $\text{image}\, f$ is isomorphic to the source object $ X $. This isomorphism is constructed by comparing the universal properties of the image factorization of $ f $ and the trivial factorization of $ f $ as a monomorphism.

CategoryTheory.Limits.imageMonoIsoSource_inv_ι theorem

[Mono f] : (imageMonoIsoSource f).inv ≫ image.ι f = f

Full source

@[reassoc (attr := simp)]
theorem imageMonoIsoSource_inv_ι [Mono f] : (imageMonoIsoSource f).inv ≫ image.ι f = f := by
  simp [imageMonoIsoSource]

Inverse Image Isomorphism Composed with Inclusion Equals Original Monomorphism

Informal description

For any monomorphism $f \colon X \to Y$ in a category, the composition of the inverse of the isomorphism $\text{image}(f) \cong X$ with the image inclusion morphism $\iota \colon \text{image}(f) \to Y$ equals $f$. That is, the diagram \[ X \xleftarrow{\text{imageMonoIsoSource}(f).\text{inv}} \text{image}(f) \xrightarrow{\iota} Y \] commutes and satisfies $(\text{imageMonoIsoSource}(f).\text{inv}) \circ \iota = f$.

CategoryTheory.Limits.imageMonoIsoSource_hom_self theorem

[Mono f] : (imageMonoIsoSource f).hom ≫ f = image.ι f

Full source

@[reassoc (attr := simp)]
theorem imageMonoIsoSource_hom_self [Mono f] : (imageMonoIsoSource f).hom ≫ f = image.ι f := by
  simp only [← imageMonoIsoSource_inv_ι f]
  rw [← Category.assoc, Iso.hom_inv_id, Category.id_comp]

Isomorphism from Image to Source Composed with Original Morphism Equals Image Inclusion

Informal description

For any monomorphism $f \colon X \to Y$ in a category, the composition of the isomorphism $\text{image}(f) \cong X$ with $f$ equals the image inclusion morphism $\iota \colon \text{image}(f) \to Y$. That is, the diagram \[ \text{image}(f) \xrightarrow{\text{imageMonoIsoSource}(f).\text{hom}} X \xrightarrow{f} Y \] commutes and satisfies $(\text{imageMonoIsoSource}(f).\text{hom}) \circ f = \iota$.

CategoryTheory.Limits.image.ext theorem

 [HasImage f] {W : C} {g h : image f ⟶ W} [HasLimit (parallelPair g h)]
  (w : factorThruImage f ≫ g = factorThruImage f ≫ h) : g = h

Full source

@[ext (iff := false)]
theorem image.ext [HasImage f] {W : C} {g h : imageimage f ⟶ W} [HasLimit (parallelPair g h)]
    (w : factorThruImagefactorThruImage f ≫ g = factorThruImagefactorThruImage f ≫ h) : g = h := by
  let q := equalizer.ι g h
  let e' := equalizer.lift _ w
  let F' : MonoFactorisation f :=
    { I := equalizer g h
      m := q ≫ image.ι f
      m_mono := mono_comp _ _
      e := e' }
  let v := image.lift F'
  have t₀ : v ≫ q ≫ image.ι f = image.ι f := image.lift_fac F'
  have t : v ≫ q = 𝟙 (image f) :=
    (cancel_mono_id (image.ι f)).1
      (by
        convert t₀ using 1
        rw [Category.assoc])
  -- The proof from wikipedia next proves `q ≫ v = 𝟙 _`,
  -- and concludes that `equalizer g h ≅ image f`,
  -- but this isn't necessary.
  calc
    g = 𝟙𝟙 (image f) ≫ g := by rw [Category.id_comp]
    _ = v ≫ q ≫ g := by rw [← t, Category.assoc]
    _ = v ≫ q ≫ h := by rw [equalizer.condition g h]
    _ = 𝟙𝟙 (image f) ≫ h := by rw [← Category.assoc, t]
    _ = h := by rw [Category.id_comp]

Uniqueness of Morphisms from Image via Factorization Condition

Informal description

Let $f \colon X \to Y$ be a morphism in a category with an image factorization. For any object $W$ and any pair of morphisms $g, h \colon \text{image}(f) \to W$ such that the equalizer of $g$ and $h$ exists, if the compositions $\text{factorThruImage}\, f \circ g$ and $\text{factorThruImage}\, f \circ h$ are equal, then $g = h$.

CategoryTheory.Limits.instEpiFactorThruImageOfHasLimitWalkingParallelPairParallelPair instance

[HasImage f] [∀ {Z : C} (g h : image f ⟶ Z), HasLimit (parallelPair g h)] : Epi (factorThruImage f)

Full source

instance [HasImage f] [∀ {Z : C} (g h : imageimage f ⟶ Z), HasLimit (parallelPair g h)] :
    Epi (factorThruImage f) :=
  ⟨fun _ _ w => image.ext f w⟩

Factorization Through Image is an Epimorphism When Equalizers Exist

Informal description

For any morphism $f \colon X \to Y$ in a category with image factorization, if the category has equalizers for all parallel pairs of morphisms out of the image object, then the factorization morphism $\text{factorThruImage}\, f \colon X \to \text{image}(f)$ is an epimorphism.

CategoryTheory.Limits.epi_image_of_epi theorem

{X Y : C} (f : X ⟶ Y) [HasImage f] [E : Epi f] : Epi (image.ι f)

Full source

theorem epi_image_of_epi {X Y : C} (f : X ⟶ Y) [HasImage f] [E : Epi f] : Epi (image.ι f) := by
  rw [← image.fac f] at E
  exact epi_of_epi (factorThruImage f) (image.ι f)

Image Inclusion of an Epimorphism is an Epimorphism

Informal description

For any epimorphism $f \colon X \to Y$ in a category $C$ that has an image factorization, the image inclusion morphism $\iota \colon \text{image}(f) \to Y$ is also an epimorphism.

CategoryTheory.Limits.epi_of_epi_image theorem

{X Y : C} (f : X ⟶ Y) [HasImage f] [Epi (image.ι f)] [Epi (factorThruImage f)] : Epi f

Full source

theorem epi_of_epi_image {X Y : C} (f : X ⟶ Y) [HasImage f] [Epi (image.ι f)]
    [Epi (factorThruImage f)] : Epi f := by
  rw [← image.fac f]
  apply epi_comp

Epimorphism Property via Image Factorization: If Image and Factorization Morphisms are Epimorphisms, then the Original Morphism is an Epimorphism

Informal description

Let $ f \colon X \to Y $ be a morphism in a category $ C $ that has an image factorization $ f = e \circ m $, where $ m \colon \text{image}(f) \to Y $ is the image inclusion morphism and $ e \colon X \to \text{image}(f) $ is the factorization morphism. If both $ m $ and $ e $ are epimorphisms, then $ f $ is also an epimorphism.

CategoryTheory.Limits.image.eqToHom definition

(h : f = f') : image f ⟶ image f'

Full source

/-- An equation between morphisms gives a comparison map between the images
(which momentarily we prove is an iso).
-/
def image.eqToHom (h : f = f') : imageimage f ⟶ image f' :=
  image.lift
    { I := image f'
      m := image.ι f'
      e := factorThruImage f'
      fac := by rw [h]; simp only [image.fac]}

Canonical comparison map between images of equal morphisms

Informal description

Given an equality $h : f = f'$ between two morphisms $f, f' : X \to Y$ in a category, the morphism $\text{image.eqToHom} \, h : \text{image}(f) \to \text{image}(f')$ is the canonical comparison map between their image objects, constructed using the universal property of the image factorization. This map makes the following diagram commute: X ----→ image(f) ----→ Y | | | | | | ↓ ↓ ↓ X ----→ image(f') ----→ Y where the vertical maps are identities and the horizontal maps are the respective image factorizations.

CategoryTheory.Limits.instIsIsoEqToHom instance

(h : f = f') : IsIso (image.eqToHom h)

Full source

instance (h : f = f') : IsIso (image.eqToHom h) :=
  ⟨⟨image.eqToHom h.symm,
      ⟨(cancel_mono (image.ι f)).1 (by
          -- Porting note: added let's for used to be a simp [image.eqToHom]
          let F : MonoFactorisation f' :=
            ⟨image f, image.ι f, factorThruImage f, (by aesop_cat)⟩
          dsimp [image.eqToHom]
          rw [Category.id_comp,Category.assoc,image.lift_fac F]
          let F' : MonoFactorisation f :=
            ⟨image f', image.ι f', factorThruImage f', (by aesop_cat)⟩
          rw [image.lift_fac F'] ),
        (cancel_mono (image.ι f')).1 (by
          -- Porting note: added let's for used to be a simp [image.eqToHom]
          let F' : MonoFactorisation f :=
            ⟨image f', image.ι f', factorThruImage f', (by aesop_cat)⟩
          dsimp [image.eqToHom]
          rw [Category.id_comp,Category.assoc,image.lift_fac F']
          let F : MonoFactorisation f' :=
            ⟨image f, image.ι f, factorThruImage f, (by aesop_cat)⟩
          rw [image.lift_fac F])⟩⟩⟩

The Canonical Comparison Between Images of Equal Morphisms is an Isomorphism

Informal description

For any equality $h : f = f'$ between morphisms $f, f' : X \to Y$ in a category, the canonical comparison map $\text{image.eqToHom}\, h : \text{image}(f) \to \text{image}(f')$ is an isomorphism.

CategoryTheory.Limits.image.eqToIso definition

(h : f = f') : image f ≅ image f'

Full source

/-- An equation between morphisms gives an isomorphism between the images. -/
def image.eqToIso (h : f = f') : imageimage f ≅ image f' :=
  asIso (image.eqToHom h)

Isomorphism between images of equal morphisms

Informal description

Given an equality $h : f = f'$ between two morphisms $f, f' : X \to Y$ in a category, the isomorphism $\text{image.eqToIso}\, h : \text{image}(f) \cong \text{image}(f')$ is constructed from the canonical comparison map $\text{image.eqToHom}\, h$ between their image objects. This isomorphism ensures that the images of equal morphisms are naturally isomorphic.

CategoryTheory.Limits.image.preComp definition

[HasImage g] [HasImage (f ≫ g)] : image (f ≫ g) ⟶ image g

Full source

/-- The comparison map `image (f ≫ g) ⟶ image g`. -/
def image.preComp [HasImage g] [HasImage (f ≫ g)] : imageimage (f ≫ g) ⟶ image g :=
  image.lift
    { I := image g
      m := image.ι g
      e := f ≫ factorThruImage g }

Comparison morphism from image of composition to image of second morphism

Informal description

The comparison morphism $\text{image}(f \circ g) \to \text{image}(g)$ is constructed using the universal property of the image factorization of $g$. It is the unique morphism that makes the following diagram commute: \[ \begin{array}{ccc} X & \xrightarrow{f \circ g} & Y \\ & \searrow & \uparrow \\ & & \text{image}(g) \end{array} \] where the vertical arrow is the monomorphism $\iota_g : \text{image}(g) \to Y$ and the diagonal arrow is the factorization of $f \circ g$ through $\text{image}(g)$.

CategoryTheory.Limits.image.preComp_ι theorem

[HasImage g] [HasImage (f ≫ g)] : image.preComp f g ≫ image.ι g = image.ι (f ≫ g)

Full source

@[reassoc (attr := simp)]
theorem image.preComp_ι [HasImage g] [HasImage (f ≫ g)] :
    image.preCompimage.preComp f g ≫ image.ι g = image.ι (f ≫ g) := by
      dsimp [image.preComp]
      rw [image.lift_fac]

Commutativity of Image Comparison with Inclusions: $\text{image.preComp}\, f\, g \circ \iota_g = \iota_{f \circ g}$

Informal description

Given morphisms $f \colon X \to Y$ and $g \colon Y \to Z$ in a category with image factorizations for both $g$ and $f \circ g$, the composition of the comparison morphism $\text{image.preComp}\, f\, g \colon \text{image}(f \circ g) \to \text{image}(g)$ with the image inclusion $\iota_g \colon \text{image}(g) \to Z$ equals the image inclusion $\iota_{f \circ g} \colon \text{image}(f \circ g) \to Z$. That is, the following diagram commutes: \[ \text{image}(f \circ g) \xrightarrow{\text{image.preComp}\, f\, g} \text{image}(g) \xrightarrow{\iota_g} Z \] and the composition equals $\iota_{f \circ g}$.

CategoryTheory.Limits.image.factorThruImage_preComp theorem

[HasImage g] [HasImage (f ≫ g)] : factorThruImage (f ≫ g) ≫ image.preComp f g = f ≫ factorThruImage g

Full source

@[reassoc (attr := simp)]
theorem image.factorThruImage_preComp [HasImage g] [HasImage (f ≫ g)] :
    factorThruImagefactorThruImage (f ≫ g) ≫ image.preComp f g = f ≫ factorThruImage g := by simp [image.preComp]

Factorization through image of composition equals composition of factorization

Informal description

Given morphisms $f \colon X \to Z$ and $g \colon Z \to Y$ in a category with image factorizations, the composition of the factorization morphism $\text{factorThruImage}(f \circ g) \colon X \to \text{image}(f \circ g)$ with the comparison morphism $\text{image.preComp}\, f\, g \colon \text{image}(f \circ g) \to \text{image}(g)$ equals the composition of $f$ with the factorization morphism $\text{factorThruImage}\, g \colon Z \to \text{image}(g)$. In other words, the following diagram commutes: \[ X \xrightarrow{\text{factorThruImage}(f \circ g)} \text{image}(f \circ g) \xrightarrow{\text{image.preComp}\, f\, g} \text{image}(g) = X \xrightarrow{f} Z \xrightarrow{\text{factorThruImage}\, g} \text{image}(g) \]

CategoryTheory.Limits.image.preComp_mono instance

[HasImage g] [HasImage (f ≫ g)] : Mono (image.preComp f g)

Full source

/-- `image.preComp f g` is a monomorphism.
-/
instance image.preComp_mono [HasImage g] [HasImage (f ≫ g)] : Mono (image.preComp f g) := by
  refine @mono_of_mono _ _ _ _ _ _ (image.ι g) ?_
  simp only [image.preComp_ι]
  infer_instance

Monomorphism Property of Image Comparison Map

Informal description

For any morphisms $f \colon X \to Y$ and $g \colon Y \to Z$ in a category with image factorizations for both $g$ and $f \circ g$, the comparison morphism $\text{image.preComp}\, f\, g \colon \text{image}(f \circ g) \to \text{image}(g)$ is a monomorphism.

CategoryTheory.Limits.image.preComp_comp theorem

 {W : C} (h : Z ⟶ W) [HasImage (g ≫ h)] [HasImage (f ≫ g ≫ h)] [HasImage h] [HasImage ((f ≫ g) ≫ h)] :
  image.preComp f (g ≫ h) ≫ image.preComp g h = image.eqToHom (Category.assoc f g h).symm ≫ image.preComp (f ≫ g) h

Full source

/-- The two step comparison map
  `image (f ≫ (g ≫ h)) ⟶ image (g ≫ h) ⟶ image h`
agrees with the one step comparison map
  `image (f ≫ (g ≫ h)) ≅ image ((f ≫ g) ≫ h) ⟶ image h`.
-/
theorem image.preComp_comp {W : C} (h : Z ⟶ W) [HasImage (g ≫ h)] [HasImage (f ≫ g ≫ h)]
    [HasImage h] [HasImage ((f ≫ g) ≫ h)] :
    image.preCompimage.preComp f (g ≫ h) ≫ image.preComp g h =
      image.eqToHomimage.eqToHom (Category.assoc f g h).symm ≫ image.preComp (f ≫ g) h := by
  apply (cancel_mono (image.ι h)).1
  dsimp [image.preComp, image.eqToHom]
  repeat (rw [Category.assoc,image.lift_fac])
  rw [image.lift_fac,image.lift_fac]

Compatibility of Image Comparison Maps with Composition and Associativity

Informal description

Let $f \colon X \to Y$, $g \colon Y \to Z$, and $h \colon Z \to W$ be morphisms in a category $C$, and assume that the images of $g \circ h$, $f \circ g \circ h$, $h$, and $(f \circ g) \circ h$ exist. Then the composition of the comparison maps \[ \text{image}(f \circ (g \circ h)) \xrightarrow{\text{image.preComp}\, f\, (g \circ h)} \text{image}(g \circ h) \xrightarrow{\text{image.preComp}\, g\, h} \text{image}(h) \] is equal to the composition \[ \text{image}(f \circ (g \circ h)) \xrightarrow{\text{image.eqToHom}\, (\text{assoc}\, f\, g\, h)^{-1}} \text{image}((f \circ g) \circ h) \xrightarrow{\text{image.preComp}\, (f \circ g)\, h} \text{image}(h), \] where $\text{assoc}\, f\, g\, h$ is the associativity isomorphism $(f \circ g) \circ h \cong f \circ (g \circ h)$.

CategoryTheory.Limits.image.preComp_epi_of_epi instance

[HasImage g] [HasImage (f ≫ g)] [Epi f] : Epi (image.preComp f g)

Full source

/-- `image.preComp f g` is an epimorphism when `f` is an epimorphism
(we need `C` to have equalizers to prove this).
-/
instance image.preComp_epi_of_epi [HasImage g] [HasImage (f ≫ g)] [Epi f] :
    Epi (image.preComp f g) := by
  apply @epi_of_epi_fac _ _ _ _ _ _ _ _ ?_ (image.factorThruImage_preComp _ _)
  exact epi_comp _ _

Epimorphism Property of Image Comparison Map for Epimorphic First Morphism

Informal description

For any morphisms $f \colon X \to Y$ and $g \colon Y \to Z$ in a category with image factorizations for both $g$ and $f \circ g$, if $f$ is an epimorphism, then the comparison morphism $\text{image}(f \circ g) \to \text{image}(g)$ is also an epimorphism.

CategoryTheory.Limits.hasImage_iso_comp instance

[IsIso f] [HasImage g] : HasImage (f ≫ g)

Full source

instance hasImage_iso_comp [IsIso f] [HasImage g] : HasImage (f ≫ g) :=
  HasImage.mk
    { F := (Image.monoFactorisation g).isoComp f
      isImage := { lift := fun F' => image.lift (F'.ofIsoComp f)
                   lift_fac := fun F' => by
                    dsimp
                    have : (MonoFactorisation.ofIsoComp f F').m = F'.m := rfl
                    rw [← this,image.lift_fac (MonoFactorisation.ofIsoComp f F')] } }

Existence of Image Factorization for Composition with Isomorphism

Informal description

For any isomorphism $f \colon X \to Y$ and morphism $g \colon Y \to Z$ in a category, if $g$ has an image factorization, then the composition $f \circ g$ also has an image factorization.

CategoryTheory.Limits.image.isIso_precomp_iso instance

(f : X ⟶ Y) [IsIso f] [HasImage g] : IsIso (image.preComp f g)

Full source

/-- `image.preComp f g` is an isomorphism when `f` is an isomorphism
(we need `C` to have equalizers to prove this).
-/
instance image.isIso_precomp_iso (f : X ⟶ Y) [IsIso f] [HasImage g] : IsIso (image.preComp f g) :=
  ⟨⟨image.lift
        { I := image (f ≫ g)
          m := image.ι (f ≫ g)
          e := inv f ≫ factorThruImage (f ≫ g) },
      ⟨by
        ext
        simp [image.preComp], by
        ext
        simp [image.preComp]⟩⟩⟩

Comparison Morphism for Image of Composition with Isomorphism is Isomorphic

Informal description

For any isomorphism $f \colon X \to Y$ in a category and any morphism $g \colon Y \to Z$ that has an image factorization, the comparison morphism $\text{image}(f \circ g) \to \text{image}(g)$ is an isomorphism.

CategoryTheory.Limits.hasImage_comp_iso instance

[HasImage f] [IsIso g] : HasImage (f ≫ g)

Full source

instance hasImage_comp_iso [HasImage f] [IsIso g] : HasImage (f ≫ g) :=
  HasImage.mk
    { F := (Image.monoFactorisation f).compMono g
      isImage :=
      { lift := fun F' => image.lift F'.ofCompIso
        lift_fac := fun F' => by
          rw [← Category.comp_id (image.liftimage.lift (MonoFactorisation.ofCompIso F') ≫ F'.m),
            ← IsIso.inv_hom_id g,← Category.assoc]
          refine congrArg (· ≫ g) ?_
          have : (image.lift (MonoFactorisation.ofCompIso F') ≫ F'.m) ≫ inv g =
            image.liftimage.lift (MonoFactorisation.ofCompIso F') ≫
            ((MonoFactorisation.ofCompIso F').m) := by
              simp only [MonoFactorisation.ofCompIso_I, Category.assoc,
                MonoFactorisation.ofCompIso_m]
          rw [this, image.lift_fac (MonoFactorisation.ofCompIso F'),image.as_ι] }}

Existence of Image Factorization for Composition with Isomorphism

Informal description

For any morphism $f \colon X \to Y$ in a category that has an image factorization, and any isomorphism $g \colon Y \to Z$, the composition $f \circ g$ also has an image factorization.

CategoryTheory.Limits.image.compIso definition

[HasImage f] [IsIso g] : image f ≅ image (f ≫ g)

Full source

/-- Postcomposing by an isomorphism induces an isomorphism on the image. -/
def image.compIso [HasImage f] [IsIso g] : imageimage f ≅ image (f ≫ g) where
  hom := image.lift (Image.monoFactorisation (f ≫ g)).ofCompIso
  inv := image.lift ((Image.monoFactorisation f).compMono g)

Isomorphism between images of a morphism and its composition with an isomorphism

Informal description

Given a morphism $ f : X \to Y $ in a category that has an image factorization, and an isomorphism $ g : Y \to Z $, there is an isomorphism between the image object of $ f $ and the image object of the composition $ f \circ g $. The isomorphism is constructed as follows: - The forward morphism is the universal lift from the image factorization of $ f $ to the monomorphism factorization of $ f \circ g $ obtained by composing with $ g^{-1} $. - The inverse morphism is the universal lift from the image factorization of $ f \circ g $ to the monomorphism factorization of $ f $ obtained by composing with $ g $. Moreover, these morphisms satisfy: 1. The composition of the forward isomorphism with the inclusion of the image of $ f \circ g $ equals the inclusion of the image of $ f $ composed with $ g $. 2. The composition of the inverse isomorphism with the inclusion of the image of $ f $ equals the inclusion of the image of $ f \circ g $ composed with $ g^{-1} $.

CategoryTheory.Limits.image.compIso_hom_comp_image_ι theorem

[HasImage f] [IsIso g] : (image.compIso f g).hom ≫ image.ι (f ≫ g) = image.ι f ≫ g

Full source

@[reassoc (attr := simp)]
theorem image.compIso_hom_comp_image_ι [HasImage f] [IsIso g] :
    (image.compIso f g).hom ≫ image.ι (f ≫ g) = image.ιimage.ι f ≫ g := by
  ext
  simp [image.compIso]

Commutativity of Image Isomorphism with Post-Composition by Isomorphism

Informal description

Let $f \colon X \to Y$ be a morphism in a category with an image factorization, and let $g \colon Y \to Z$ be an isomorphism. Then the composition of the isomorphism $\text{image}(f) \cong \text{image}(f \circ g)$ with the image inclusion $\iota_{f \circ g} \colon \text{image}(f \circ g) \to Z$ equals the composition of the image inclusion $\iota_f \colon \text{image}(f) \to Y$ with $g$. In other words, the following diagram commutes: \[ \text{image}(f) \xrightarrow{\text{compIso}(f,g).\text{hom}} \text{image}(f \circ g) \xrightarrow{\iota_{f \circ g}} Z \] equals \[ \text{image}(f) \xrightarrow{\iota_f} Y \xrightarrow{g} Z \]

CategoryTheory.Limits.image.compIso_inv_comp_image_ι theorem

[HasImage f] [IsIso g] : (image.compIso f g).inv ≫ image.ι f = image.ι (f ≫ g) ≫ inv g

Full source

@[reassoc (attr := simp)]
theorem image.compIso_inv_comp_image_ι [HasImage f] [IsIso g] :
    (image.compIso f g).inv ≫ image.ι f = image.ιimage.ι (f ≫ g) ≫ inv g := by
  ext
  simp [image.compIso]

Compatibility of Image Isomorphism Inverse with Image Inclusions

Informal description

For a morphism $f \colon X \to Y$ in a category with an image factorization, and an isomorphism $g \colon Y \to Z$, the inverse of the isomorphism $\text{image}(f) \cong \text{image}(f \circ g)$ satisfies: \[ (\text{image.compIso}\, f\, g)^{-1} \circ \iota_f = \iota_{f \circ g} \circ g^{-1} \] where $\iota_f \colon \text{image}(f) \to Y$ and $\iota_{f \circ g} \colon \text{image}(f \circ g) \to Z$ are the respective image inclusion morphisms.

CategoryTheory.Limits.instHasImageHomMk instance

{X Y : C} (f : X ⟶ Y) [HasImage f] : HasImage (Arrow.mk f).hom

Full source

instance {X Y : C} (f : X ⟶ Y) [HasImage f] : HasImage (Arrow.mk f).hom :=
  show HasImage f by infer_instance

Image Factorization in the Arrow Category

Informal description

For any morphism $f : X \to Y$ in a category $C$ that has an image factorization, the corresponding morphism in the arrow category of $C$ (constructed via `Arrow.mk f`) also has an image factorization.

CategoryTheory.Limits.ImageMap structure

{f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f ⟶ g)

Full source

/-- An image map is a morphism `image f → image g` fitting into a commutative square and satisfying
    the obvious commutativity conditions. -/
structure ImageMap {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f ⟶ g) where
  map : imageimage f.hom ⟶ image g.hom
  map_ι : map ≫ image.ι g.hom = image.ιimage.ι f.hom ≫ sq.right := by aesop

Image map for a commutative square

Informal description

Given a commutative square `sq` between two morphisms `f` and `g` in the arrow category of `C`, where both `f` and `g` have image factorizations, an `ImageMap` is a morphism between the images of `f` and `g` that makes the resulting diagram commute. Specifically, it consists of a morphism `map : image f → image g` such that the following diagram commutes: ``` X ----→ image f ----→ Y | | | | | | ↓ ↓ ↓ P ----→ image g ----→ Q ``` where the top and bottom rows are the image factorizations of `f` and `g` respectively, and the outer square is the original commutative square `sq`.

CategoryTheory.Limits.inhabitedImageMap instance

{f : Arrow C} [HasImage f.hom] : Inhabited (ImageMap (𝟙 f))

Full source

instance inhabitedImageMap {f : Arrow C} [HasImage f.hom] : Inhabited (ImageMap (𝟙 f)) :=
  ⟨⟨𝟙 _, by simp⟩⟩

Existence of Image Map for Identity Commutative Square

Informal description

For any morphism $f : X \to Y$ in a category $C$ that has an image factorization, the identity commutative square on $f$ in the arrow category of $C$ admits an image map.

CategoryTheory.Limits.ImageMap.factor_map theorem

 {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f ⟶ g) (m : ImageMap sq) :
  factorThruImage f.hom ≫ m.map = sq.left ≫ factorThruImage g.hom

Full source

@[reassoc (attr := simp)]
theorem ImageMap.factor_map {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f ⟶ g)
    (m : ImageMap sq) : factorThruImagefactorThruImage f.hom ≫ m.map = sq.left ≫ factorThruImage g.hom :=
  (cancel_mono (image.ι g.hom)).1 <| by simp

Commutativity of Image Map Factorization

Informal description

Given a commutative square `sq` between morphisms `f` and `g` in the arrow category of a category `C`, where both `f` and `g` have image factorizations, and given an image map `m` for this square, the following diagram commutes: \[ \text{factorThruImage}\, f \circ m.\text{map} = \text{sq.left} \circ \text{factorThruImage}\, g \] Here, `factorThruImage f` and `factorThruImage g` are the factorization morphisms for `f` and `g` respectively, and `sq.left` is the left morphism in the commutative square `sq`.

CategoryTheory.Limits.ImageMap.transport definition

 {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f ⟶ g) (F : MonoFactorisation f.hom)
  {F' : MonoFactorisation g.hom} (hF' : IsImage F') {map : F.I ⟶ F'.I} (map_ι : map ≫ F'.m = F.m ≫ sq.right) :
  ImageMap sq

Full source

/-- To give an image map for a commutative square with `f` at the top and `g` at the bottom, it
    suffices to give a map between any mono factorisation of `f` and any image factorisation of
    `g`. -/
def ImageMap.transport {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f ⟶ g)
    (F : MonoFactorisation f.hom) {F' : MonoFactorisation g.hom} (hF' : IsImage F')
    {map : F.I ⟶ F'.I} (map_ι : map ≫ F'.m = F.m ≫ sq.right) : ImageMap sq where
  map := image.liftimage.lift F ≫ map ≫ hF'.lift (Image.monoFactorisation g.hom)
  map_ι := by simp [map_ι]

Construction of Image Map via Transport through Given Factorizations

Informal description

Given a commutative square `sq` between morphisms `f` and `g` in the arrow category of `C`, where both `f` and `g` have image factorizations, and given a monomorphism factorization `F` of `f` and a monomorphism factorization `F'` of `g` that satisfies the universal property of an image, along with a morphism `map : F.I → F'.I` making the square involving `F.m` and `F'.m` commute, there exists an image map for `sq` constructed by composing the universal lifts from the image factorizations with `map`.

CategoryTheory.Limits.HasImageMap structure

{f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f ⟶ g)

Full source

/-- `HasImageMap sq` means that there is an `ImageMap` for the square `sq`. -/
class HasImageMap {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f ⟶ g) : Prop where
mk' ::
  has_image_map : Nonempty (ImageMap sq)

Existence of Image Map for a Commutative Square

Informal description

The structure `HasImageMap sq` asserts that for a commutative square `sq` between morphisms `f` and `g` in the arrow category of `C`, there exists a morphism between their image factorizations making the resulting diagram commute. Specifically, if `f` and `g` have image factorizations `f = e ≫ m` and `g = e' ≫ m'` with monomorphisms `m` and `m'`, then there exists a morphism `i` from the image of `f` to the image of `g` such that the following diagram commutes: ``` X ----→ image f ----→ Y | | | | | | ↓ ↓ ↓ P ----→ image g ----→ Q ``` where the top and bottom rows are the image factorizations of `f` and `g` respectively, and the outer rectangle is the commutative square `sq`.

CategoryTheory.Limits.HasImageMap.mk theorem

{f g : Arrow C} [HasImage f.hom] [HasImage g.hom] {sq : f ⟶ g} (m : ImageMap sq) : HasImageMap sq

Full source

theorem HasImageMap.mk {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] {sq : f ⟶ g}
    (m : ImageMap sq) : HasImageMap sq :=
  ⟨Nonempty.intro m⟩

Existence of Image Map from Given Image Map Data

Informal description

Given a commutative square `sq` between morphisms `f` and `g` in the arrow category of `C`, where both `f` and `g` have image factorizations, and given an image map `m` for `sq`, there exists an instance of `HasImageMap sq` witnessing that `sq` admits an image map.

CategoryTheory.Limits.HasImageMap.transport theorem

 {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f ⟶ g) (F : MonoFactorisation f.hom)
  {F' : MonoFactorisation g.hom} (hF' : IsImage F') (map : F.I ⟶ F'.I) (map_ι : map ≫ F'.m = F.m ≫ sq.right) :
  HasImageMap sq

Full source

theorem HasImageMap.transport {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f ⟶ g)
    (F : MonoFactorisation f.hom) {F' : MonoFactorisation g.hom} (hF' : IsImage F')
    (map : F.I ⟶ F'.I) (map_ι : map ≫ F'.m = F.m ≫ sq.right) : HasImageMap sq :=
  HasImageMap.mk <| ImageMap.transport sq F hF' map_ι

Construction of Image Map via Transport through Given Factorizations

Informal description

Given a commutative square $sq$ between morphisms $f \colon X \to Y$ and $g \colon P \to Q$ in a category $C$, where both $f$ and $g$ have image factorizations, suppose we have: 1. A monomorphism factorization $F$ of $f$ as $f = e \circ m$ with $m \colon F.I \to Y$, 2. A monomorphism factorization $F'$ of $g$ that satisfies the universal property of an image (i.e., $F'$ is an image factorization), 3. A morphism $map \colon F.I \to F'.I$ such that the diagram \[ \begin{array}{ccc} F.I & \xrightarrow{map} & F'.I \\ \downarrow m & & \downarrow m' \\ Y & \xrightarrow{sq.right} & Q \end{array} \] commutes (i.e., $map \circ m' = m \circ sq.right$). Then there exists an image map for the square $sq$, meaning the image factorizations of $f$ and $g$ can be connected via $map$ to make the entire diagram commute.

CategoryTheory.Limits.HasImageMap.imageMap definition

{f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f ⟶ g) [HasImageMap sq] : ImageMap sq

Full source

/-- Obtain an `ImageMap` from a `HasImageMap` instance. -/
def HasImageMap.imageMap {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f ⟶ g)
    [HasImageMap sq] : ImageMap sq :=
  Classical.choice <| @HasImageMap.has_image_map _ _ _ _ _ _ sq _

Selected image map for a commutative square

Informal description

Given a commutative square `sq` between two morphisms `f` and `g` in the arrow category of `C`, where both `f` and `g` have image factorizations and `sq` has an image map, this definition selects a specific image map for `sq` using the axiom of choice. The image map consists of a morphism between the images of `f` and `g` that makes the resulting diagram commute.

CategoryTheory.Limits.hasImageMapOfIsIso instance

{f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f ⟶ g) [IsIso sq] : HasImageMap sq

Full source

instance (priority := 100) hasImageMapOfIsIso {f g : Arrow C} [HasImage f.hom] [HasImage g.hom]
    (sq : f ⟶ g) [IsIso sq] : HasImageMap sq :=
  HasImageMap.mk
    { map := image.lift ((Image.monoFactorisation g.hom).ofArrowIso (inv sq))
      map_ι := by
        erw [← cancel_mono (inv sq).right, Category.assoc, ← MonoFactorisation.ofArrowIso_m,
          image.lift_fac, Category.assoc, ← Comma.comp_right, IsIso.hom_inv_id, Comma.id_right,
          Category.comp_id] }

Existence of Image Map for Isomorphic Commutative Squares

Informal description

For any commutative square $sq$ between morphisms $f$ and $g$ in the arrow category of a category $C$, if $sq$ is an isomorphism and both $f$ and $g$ have image factorizations, then there exists an image map for $sq$.

CategoryTheory.Limits.HasImageMap.comp instance

 {f g h : Arrow C} [HasImage f.hom] [HasImage g.hom] [HasImage h.hom] (sq1 : f ⟶ g) (sq2 : g ⟶ h) [HasImageMap sq1]
  [HasImageMap sq2] : HasImageMap (sq1 ≫ sq2)

Full source

instance HasImageMap.comp {f g h : Arrow C} [HasImage f.hom] [HasImage g.hom] [HasImage h.hom]
    (sq1 : f ⟶ g) (sq2 : g ⟶ h) [HasImageMap sq1] [HasImageMap sq2] : HasImageMap (sq1 ≫ sq2) :=
  HasImageMap.mk
    { map := (HasImageMap.imageMap sq1).map ≫ (HasImageMap.imageMap sq2).map
      map_ι := by
        rw [Category.assoc,ImageMap.map_ι, ImageMap.map_ι_assoc, Comma.comp_right] }

Composition of Image Maps for Commutative Squares

Informal description

For any commutative squares $sq_1 \colon f \to g$ and $sq_2 \colon g \to h$ in the arrow category of a category $C$, where $f$, $g$, and $h$ have image factorizations and $sq_1$ and $sq_2$ admit image maps, the composition $sq_1 \circ sq_2$ also admits an image map.

CategoryTheory.Limits.ImageMap.map_uniq theorem

{f g : Arrow C} [HasImage f.hom] [HasImage g.hom] {sq : f ⟶ g} (F G : ImageMap sq) : F.map = G.map

Full source

theorem ImageMap.map_uniq {f g : Arrow C} [HasImage f.hom] [HasImage g.hom]
    {sq : f ⟶ g} (F G : ImageMap sq) : F.map = G.map := by
  apply ImageMap.map_uniq_aux _ F.map_ι _ G.map_ι

Uniqueness of Image Map for Commutative Squares

Informal description

For any commutative square $sq$ between morphisms $f$ and $g$ in the arrow category of a category $C$, where both $f$ and $g$ have image factorizations, any two image maps $F$ and $G$ for $sq$ must have identical induced maps between the images, i.e., $F.\text{map} = G.\text{map}$.

CategoryTheory.Limits.instSubsingletonImageMap instance

: Subsingleton (ImageMap sq)

Full source

instance : Subsingleton (ImageMap sq) :=
  Subsingleton.intro fun a b =>
    ImageMap.ext <| ImageMap.map_uniq a b

Uniqueness of Image Maps for Commutative Squares

Informal description

For any commutative square `sq` between morphisms `f` and `g` in the arrow category of a category `C`, where both `f` and `g` have image factorizations, the type of image maps for `sq` is a subsingleton. This means that any two image maps for `sq` are equal, i.e., the induced map between the images is unique.

CategoryTheory.Limits.image.map abbrev

: image f.hom ⟶ image g.hom

Full source

/-- The map on images induced by a commutative square. -/
abbrev image.map : imageimage f.hom ⟶ image g.hom :=
  (HasImageMap.imageMap sq).map

Induced map between images of morphisms in a commutative square

Informal description

Given a commutative square between morphisms $f$ and $g$ in the arrow category of $C$, where both $f$ and $g$ have image factorizations, the morphism $\text{image}(f) \to \text{image}(g)$ induced by the square is the unique map making the following diagram commute: \[ \begin{array}{ccc} X & \longrightarrow & \text{image}(f) & \longrightarrow & Y \\ \downarrow & & \downarrow & & \downarrow \\ P & \longrightarrow & \text{image}(g) & \longrightarrow & Q \end{array} \] Here the top and bottom rows are the image factorizations of $f$ and $g$ respectively, and the outer rectangle commutes by the given square.

CategoryTheory.Limits.image.factor_map theorem

: factorThruImage f.hom ≫ image.map sq = sq.left ≫ factorThruImage g.hom

Full source

theorem image.factor_map :
    factorThruImagefactorThruImage f.hom ≫ image.map sq = sq.left ≫ factorThruImage g.hom := by simp

Commutativity of the Image Factorization Diagram for a Square

Informal description

Given a commutative square `sq` between morphisms $f \colon X \to Y$ and $g \colon P \to Q$ in a category, where both $f$ and $g$ have image factorizations, the following diagram commutes: \[ \text{factorThruImage}(f) \circ \text{image.map}(sq) = \text{sq.left} \circ \text{factorThruImage}(g) \] Here, $\text{factorThruImage}(f) \colon X \to \text{image}(f)$ and $\text{factorThruImage}(g) \colon P \to \text{image}(g)$ are the factorization morphisms, and $\text{sq.left} \colon X \to P$ is the left morphism in the commutative square `sq`.

CategoryTheory.Limits.image.map_ι theorem

: image.map sq ≫ image.ι g.hom = image.ι f.hom ≫ sq.right

Full source

theorem image.map_ι : image.mapimage.map sq ≫ image.ι g.hom = image.ιimage.ι f.hom ≫ sq.right := by simp

Commutativity of Image Map with Image Inclusions in a Square

Informal description

Given a commutative square between morphisms $f \colon X \to Y$ and $g \colon P \to Q$ in a category $C$, where both $f$ and $g$ have image factorizations, the following diagram commutes: \[ \text{image}(f) \xrightarrow{\text{image.map } sq} \text{image}(g) \xrightarrow{\iota_g} Q = \text{image}(f) \xrightarrow{\iota_f} Y \xrightarrow{sq.\text{right}} Q \] Here $\iota_f \colon \text{image}(f) \to Y$ and $\iota_g \colon \text{image}(g) \to Q$ are the monomorphisms in the image factorizations of $f$ and $g$ respectively, and $sq.\text{right} \colon Y \to Q$ is the right vertical morphism in the commutative square $sq$.

CategoryTheory.Limits.image.map_homMk'_ι theorem

 {X Y P Q : C} {k : X ⟶ Y} [HasImage k] {l : P ⟶ Q} [HasImage l] {m : X ⟶ P} {n : Y ⟶ Q} (w : m ≫ l = k ≫ n)
  [HasImageMap (Arrow.homMk' _ _ w)] : image.map (Arrow.homMk' _ _ w) ≫ image.ι l = image.ι k ≫ n

Full source

theorem image.map_homMk'_ι {X Y P Q : C} {k : X ⟶ Y} [HasImage k] {l : P ⟶ Q} [HasImage l]
    {m : X ⟶ P} {n : Y ⟶ Q} (w : m ≫ l = k ≫ n) [HasImageMap (Arrow.homMk' _ _ w)] :
    image.mapimage.map (Arrow.homMk' _ _ w) ≫ image.ι l = image.ιimage.ι k ≫ n :=
  image.map_ι _

Commutativity of Image Map with Image Inclusions for a Constructed Square

Informal description

Given objects $X, Y, P, Q$ in a category $C$ and morphisms $k : X \to Y$ and $l : P \to Q$ with image factorizations, along with morphisms $m : X \to P$ and $n : Y \to Q$ satisfying the commutative condition $m \circ l = k \circ n$, the following diagram commutes: \[ \text{image}(k) \xrightarrow{\text{image.map}(w)} \text{image}(l) \xrightarrow{\iota_l} Q = \text{image}(k) \xrightarrow{\iota_k} Y \xrightarrow{n} Q \] where $\iota_k : \text{image}(k) \to Y$ and $\iota_l : \text{image}(l) \to Q$ are the monomorphisms in the image factorizations of $k$ and $l$ respectively, and $w$ is the commutative square formed by $m$ and $n$.

CategoryTheory.Limits.imageMapComp definition

: ImageMap (sq ≫ sq')

Full source

/-- Image maps for composable commutative squares induce an image map in the composite square. -/
def imageMapComp : ImageMap (sq ≫ sq') where map := image.mapimage.map sq ≫ image.map sq'

Composition of image maps for composable commutative squares

Informal description

Given two composable commutative squares `sq` and `sq'` between morphisms in a category, the image map for the composite square `sq ≫ sq'` is the composition of the image maps for `sq` and `sq'`. Specifically, if `image.map sq` and `image.map sq'` are the image maps for `sq` and `sq'` respectively, then the image map for `sq ≫ sq'` is given by the composition `image.map sq ≫ image.map sq'`.

CategoryTheory.Limits.image.map_comp theorem

[HasImageMap (sq ≫ sq')] : image.map (sq ≫ sq') = image.map sq ≫ image.map sq'

Full source

@[simp]
theorem image.map_comp [HasImageMap (sq ≫ sq')] :
    image.map (sq ≫ sq') = image.mapimage.map sq ≫ image.map sq' :=
  show (HasImageMap.imageMap (sq ≫ sq')).map = (imageMapComp sq sq').map by
    congr; simp only [eq_iff_true_of_subsingleton]

Composition of Image Maps for Composable Squares

Informal description

Given two composable commutative squares `sq` and `sq'` between morphisms in a category, where both squares have image maps, the image map of the composite square `sq ≫ sq'` is equal to the composition of the image maps of `sq` and `sq'`. That is, $\text{image.map}(sq \circ sq') = \text{image.map}(sq) \circ \text{image.map}(sq')$.

CategoryTheory.Limits.imageMapId definition

: ImageMap (𝟙 f)

Full source

/-- The identity `image f ⟶ image f` fits into the commutative square represented by the identity
    morphism `𝟙 f` in the arrow category. -/
def imageMapId : ImageMap (𝟙 f) where map := 𝟙 (image f.hom)

Identity image map for the identity commutative square

Informal description

The identity morphism on the image object of a morphism $ f $ in a category serves as the image map for the identity commutative square (represented by the identity morphism $ \mathbf{1} f $ in the arrow category). This means that when considering the image factorization of $ f $, the identity morphism on the image object makes the diagram commute where all vertical and horizontal morphisms are identities.

CategoryTheory.Limits.image.map_id theorem

[HasImageMap (𝟙 f)] : image.map (𝟙 f) = 𝟙 (image f.hom)

Full source

@[simp]
theorem image.map_id [HasImageMap (𝟙 f)] : image.map (𝟙 f) = 𝟙 (image f.hom) :=
  show (HasImageMap.imageMap (𝟙 f)).map = (imageMapId f).map by
    congr; simp only [eq_iff_true_of_subsingleton]

Identity Image Map Induces Identity Morphism

Informal description

For any morphism $f$ in a category with image factorizations, the induced map between the images of $f$ under the identity commutative square is the identity morphism on the image object of $f$, i.e., $\mathrm{image.map}(\mathbf{1}_f) = \mathbf{1}_{\mathrm{image}(f)}$.

CategoryTheory.Limits.HasImageMaps structure

Full source

/-- If a category `has_image_maps`, then all commutative squares induce morphisms on images. -/
class HasImageMaps : Prop where
  has_image_map : ∀ {f g : Arrow C} (st : f ⟶ g), HasImageMap st

Existence of image maps in a category

Informal description

A category has image maps if for every commutative square formed by morphisms $f \colon X \to Y$ and $g \colon P \to Q$ (viewed as objects in the arrow category), there exists a morphism between their image factorizations making the resulting diagram commute. This means that given image factorizations $f = e_f \circ m_f$ and $g = e_g \circ m_g$ (where $m_f$ and $m_g$ are monomorphisms), there exists a morphism $i \colon \text{image}(f) \to \text{image}(g)$ such that the diagram formed by these factorizations and the original square commutes.

CategoryTheory.Limits.im definition

: Arrow C ⥤ C

Full source

/-- The functor from the arrow category of `C` to `C` itself that maps a morphism to its image
    and a commutative square to the induced morphism on images. -/
@[simps]
def im : ArrowArrow C ⥤ C where
  obj f := image f.hom
  map st := image.map st

Image functor for the arrow category

Informal description

The functor $\mathrm{im} \colon \mathrm{Arrow}(C) \to C$ maps: - Each morphism $f \colon X \to Y$ in $C$ (viewed as an object of $\mathrm{Arrow}(C)$) to its image object $\mathrm{image}(f)$ in $C$. - Each commutative square (viewed as a morphism in $\mathrm{Arrow}(C)$) to the induced morphism between the corresponding image objects in $C$. This functor is defined when the category $C$ has images for all its morphisms and image maps for all commutative squares.

CategoryTheory.Limits.StrongEpiMonoFactorisation structure

{X Y : C} (f : X ⟶ Y) extends MonoFactorisation f

Full source

/-- A strong epi-mono factorisation is a decomposition `f = e ≫ m` with `e` a strong epimorphism
    and `m` a monomorphism. -/
structure StrongEpiMonoFactorisation {X Y : C} (f : X ⟶ Y) extends MonoFactorisation f where
  [e_strong_epi : StrongEpi e]

Strong epi-mono factorization

Informal description

A strong epi-mono factorization of a morphism $ f : X \to Y $ in a category $ C $ is a decomposition $ f = e \circ m $, where $ e : X \to I $ is a strong epimorphism and $ m : I \to Y $ is a monomorphism. This structure extends the basic mono factorization by additionally requiring $ e $ to be a strong epimorphism.

CategoryTheory.Limits.strongEpiMonoFactorisationInhabited instance

{X Y : C} (f : X ⟶ Y) [StrongEpi f] : Inhabited (StrongEpiMonoFactorisation f)

Full source

/-- Satisfying the inhabited linter -/
instance strongEpiMonoFactorisationInhabited {X Y : C} (f : X ⟶ Y) [StrongEpi f] :
    Inhabited (StrongEpiMonoFactorisation f) :=
  ⟨⟨⟨Y, 𝟙 Y, f, by simp⟩⟩⟩

Existence of Strong Epi-Mono Factorizations for Strong Epimorphisms

Informal description

For any morphism $f \colon X \to Y$ in a category $\mathcal{C}$, if $f$ is a strong epimorphism, then there exists a strong epi-mono factorization of $f$, i.e., a decomposition $f = e \circ m$ where $e$ is a strong epimorphism and $m$ is a monomorphism.

CategoryTheory.Limits.StrongEpiMonoFactorisation.toMonoIsImage definition

{X Y : C} {f : X ⟶ Y} (F : StrongEpiMonoFactorisation f) : IsImage F.toMonoFactorisation

Full source

/-- A mono factorisation coming from a strong epi-mono factorisation always has the universal
    property of the image. -/
def StrongEpiMonoFactorisation.toMonoIsImage {X Y : C} {f : X ⟶ Y}
    (F : StrongEpiMonoFactorisation f) : IsImage F.toMonoFactorisation where
  lift G :=
    (CommSq.mk (show G.e ≫ G.m = F.e ≫ F.m by rw [F.toMonoFactorisation.fac, G.fac])).lift

Universal property of the image factorization via strong epi-mono factorization

Informal description

Given a strong epi-mono factorization $ F $ of a morphism $ f \colon X \to Y $ in a category $ C $, the underlying mono factorization $ F.\text{toMonoFactorisation} $ satisfies the universal property of the categorical image. That is, any other factorization of $ f $ through a monomorphism factors uniquely through $ F.\text{toMonoFactorisation} $.

CategoryTheory.Limits.HasStrongEpiMonoFactorisations structure

Full source

/-- A category has strong epi-mono factorisations if every morphism admits a strong epi-mono
    factorisation. -/
class HasStrongEpiMonoFactorisations : Prop where mk' ::
  has_fac : ∀ {X Y : C} (f : X ⟶ Y), Nonempty (StrongEpiMonoFactorisation f)

Strong epi-mono factorisations in a category

Informal description

A category has strong epi-mono factorisations if every morphism $f : X \to Y$ can be factored as $f = e \circ m$, where $e$ is a strong epimorphism and $m$ is a monomorphism.

CategoryTheory.Limits.HasStrongEpiMonoFactorisations.mk theorem

(d : ∀ {X Y : C} (f : X ⟶ Y), StrongEpiMonoFactorisation f) : HasStrongEpiMonoFactorisations C

Full source

theorem HasStrongEpiMonoFactorisations.mk
    (d : ∀ {X Y : C} (f : X ⟶ Y), StrongEpiMonoFactorisation f) :
    HasStrongEpiMonoFactorisations C :=
  ⟨fun f => Nonempty.intro <| d f⟩

Existence of Strong Epi-Mono Factorizations in a Category

Informal description

Given a category $C$, if for every morphism $f \colon X \to Y$ in $C$ there exists a strong epi-mono factorization $f = e \circ m$ (where $e$ is a strong epimorphism and $m$ is a monomorphism), then $C$ has strong epi-mono factorizations.

CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations instance

[HasStrongEpiMonoFactorisations C] : HasImages C

Full source

instance (priority := 100) hasImages_of_hasStrongEpiMonoFactorisations
    [HasStrongEpiMonoFactorisations C] : HasImages C where
  has_image f :=
    let F' := Classical.choice (HasStrongEpiMonoFactorisations.has_fac f)
    HasImage.mk
      { F := F'.toMonoFactorisation
        isImage := F'.toMonoIsImage }

Existence of Images from Strong Epi-Mono Factorisations

Informal description

Every category $C$ that has strong epi-mono factorisations also has images. That is, if every morphism in $C$ can be factored as a strong epimorphism followed by a monomorphism, then $C$ has image factorisations for all morphisms.

CategoryTheory.Limits.HasStrongEpiImages structure

Full source

/-- A category has strong epi images if it has all images and `factorThruImage f` is a strong
    epimorphism for all `f`. -/
class HasStrongEpiImages : Prop where
  strong_factorThruImage : ∀ {X Y : C} (f : X ⟶ Y), StrongEpi (factorThruImage f)

Strong epi images in a category

Informal description

A category has strong epi images if it has all images and for every morphism $f$, the morphism to its image is a strong epimorphism.

CategoryTheory.Limits.strongEpi_of_strongEpiMonoFactorisation theorem

 {X Y : C} {f : X ⟶ Y} (F : StrongEpiMonoFactorisation f) {F' : MonoFactorisation f} (hF' : IsImage F') : StrongEpi F'.e

Full source

/-- If there is a single strong epi-mono factorisation of `f`, then every image factorisation is a
    strong epi-mono factorisation. -/
theorem strongEpi_of_strongEpiMonoFactorisation {X Y : C} {f : X ⟶ Y}
    (F : StrongEpiMonoFactorisation f) {F' : MonoFactorisation f} (hF' : IsImage F') :
    StrongEpi F'.e := by
  rw [← IsImage.e_isoExt_hom F.toMonoIsImage hF']
  apply strongEpi_comp

Strong Epimorphism Property of Image Factorizations via Strong Epi-Mono Factorization

Informal description

Let $f \colon X \to Y$ be a morphism in a category $C$, and let $F$ be a strong epi-mono factorization of $f$. For any monomorphism factorization $F'$ of $f$ that satisfies the universal property of being a categorical image, the morphism $F'.e \colon X \to F'.I$ is a strong epimorphism.

CategoryTheory.Limits.strongEpi_factorThruImage_of_strongEpiMonoFactorisation theorem

{X Y : C} {f : X ⟶ Y} [HasImage f] (F : StrongEpiMonoFactorisation f) : StrongEpi (factorThruImage f)

Full source

theorem strongEpi_factorThruImage_of_strongEpiMonoFactorisation {X Y : C} {f : X ⟶ Y} [HasImage f]
    (F : StrongEpiMonoFactorisation f) : StrongEpi (factorThruImage f) :=
  strongEpi_of_strongEpiMonoFactorisation F <| Image.isImage f

Strong Epimorphism Property of the Factorization Through Image via Strong Epi-Mono Factorization

Informal description

Let $C$ be a category, and let $f \colon X \to Y$ be a morphism in $C$ that has an image factorization. Given a strong epi-mono factorization $F$ of $f$, the morphism $\text{factorThruImage}(f) \colon X \to \text{image}(f)$ is a strong epimorphism.

CategoryTheory.Limits.hasStrongEpiImages_of_hasStrongEpiMonoFactorisations instance

[HasStrongEpiMonoFactorisations C] : HasStrongEpiImages C

Full source

/-- If we constructed our images from strong epi-mono factorisations, then these images are
    strong epi images. -/
instance (priority := 100) hasStrongEpiImages_of_hasStrongEpiMonoFactorisations
    [HasStrongEpiMonoFactorisations C] : HasStrongEpiImages C where
  strong_factorThruImage f :=
    strongEpi_factorThruImage_of_strongEpiMonoFactorisation <|
      Classical.choice <| HasStrongEpiMonoFactorisations.has_fac f

Strong Epi Images from Strong Epi-Mono Factorisations

Informal description

Every category $C$ that has strong epi-mono factorisations also has strong epi images. That is, if every morphism in $C$ can be factored as a strong epimorphism followed by a monomorphism, then for every morphism $f$ in $C$, the morphism to its image is a strong epimorphism.

CategoryTheory.Limits.hasImageMapsOfHasStrongEpiImages instance

[HasStrongEpiImages C] : HasImageMaps C

Full source

/-- A category with strong epi images has image maps. -/
instance (priority := 100) hasImageMapsOfHasStrongEpiImages [HasStrongEpiImages C] :
    HasImageMaps C where
  has_image_map {f} {g} st :=
    HasImageMap.mk
      { map :=
          (CommSq.mk
              (show
                (st.left ≫ factorThruImage g.hom) ≫ image.ι g.hom =
                  factorThruImagefactorThruImage f.hom ≫ image.ι f.hom ≫ st.right
                by simp)).lift }

Existence of Image Maps in Categories with Strong Epi Images

Informal description

In a category with strong epi images, every commutative square between morphisms admits an image map. That is, if the category has images where the morphism to the image is a strong epimorphism, then for any commutative square formed by morphisms $f \colon X \to Y$ and $g \colon P \to Q$, there exists a morphism between their image factorizations making the resulting diagram commute.

CategoryTheory.Limits.hasStrongEpiImages_of_hasPullbacks_of_hasEqualizers instance

[HasPullbacks C] [HasEqualizers C] : HasStrongEpiImages C

Full source

/-- If a category has images, equalizers and pullbacks, then images are automatically strong epi
    images. -/
instance (priority := 100) hasStrongEpiImages_of_hasPullbacks_of_hasEqualizers [HasPullbacks C]
    [HasEqualizers C] : HasStrongEpiImages C where
  strong_factorThruImage f :=
    StrongEpi.mk' fun {A} {B} h h_mono x y sq =>
      CommSq.HasLift.mk'
        { l :=
            image.liftimage.lift
                { I := pullback h y
                  m := pullback.snd h y ≫ image.ι f
                  m_mono := mono_comp _ _
                  e := pullback.lift _ _ sq.w } ≫
              pullback.fst h y
          fac_left := by simp only [image.fac_lift_assoc, pullback.lift_fst]
          fac_right := by
            apply image.ext
            simp only [sq.w, Category.assoc, image.fac_lift_assoc, pullback.lift_fst_assoc] }

Strong Epi Images from Pullbacks and Equalizers

Informal description

In any category $\mathcal{C}$ that has pullbacks and equalizers, every morphism has a strong epi image factorization. That is, for any morphism $f \colon X \to Y$ in $\mathcal{C}$, there exists a factorization $f = e \circ m$ where $e$ is a strong epimorphism and $m$ is a monomorphism, and this factorization is universal among all such factorizations.

CategoryTheory.Limits.image.isoStrongEpiMono definition

{I' : C} (e : X ⟶ I') (m : I' ⟶ Y) (comm : e ≫ m = f) [StrongEpi e] [Mono m] : I' ≅ image f

Full source

/--
If `C` has strong epi mono factorisations, then the image is unique up to isomorphism, in that if
`f` factors as a strong epi followed by a mono, this factorisation is essentially the image
factorisation.
-/
def image.isoStrongEpiMono {I' : C} (e : X ⟶ I') (m : I' ⟶ Y) (comm : e ≫ m = f) [StrongEpi e]
    [Mono m] : I' ≅ image f :=
  let F : StrongEpiMonoFactorisation f := { I := I', m := m, e := e}
  IsImage.isoExt F.toMonoIsImage <| Image.isImage f

Isomorphism between strong epi-mono factorization and image factorization

Informal description

Given a morphism $ f : X \to Y $ in a category $ C $, and a factorization $ f = e \circ m $ where $ e : X \to I' $ is a strong epimorphism and $ m : I' \to Y $ is a monomorphism, there exists an isomorphism $ I' \cong \text{image } f $ between the intermediate object $ I' $ and the image object of $ f $. This isomorphism makes the diagram commute, meaning it identifies the given factorization with the canonical image factorization of $ f $.

CategoryTheory.Limits.image.isoStrongEpiMono_hom_comp_ι theorem

 {I' : C} (e : X ⟶ I') (m : I' ⟶ Y) (comm : e ≫ m = f) [StrongEpi e] [Mono m] :
  (image.isoStrongEpiMono e m comm).hom ≫ image.ι f = m

Full source

@[simp]
theorem image.isoStrongEpiMono_hom_comp_ι {I' : C} (e : X ⟶ I') (m : I' ⟶ Y) (comm : e ≫ m = f)
    [StrongEpi e] [Mono m] : (image.isoStrongEpiMono e m comm).hom ≫ image.ι f = m := by
  dsimp [isoStrongEpiMono]
  apply IsImage.lift_fac

Compatibility of Image Isomorphism with Factorization Morphisms

Informal description

Given a morphism $f \colon X \to Y$ in a category $C$ with a strong epi-mono factorization $f = e \circ m$, where $e \colon X \to I'$ is a strong epimorphism and $m \colon I' \to Y$ is a monomorphism, the composition of the isomorphism $\text{image}(f) \cong I'$ (induced by the universal property of the image) with the image inclusion $\iota \colon \text{image}(f) \to Y$ equals $m$. That is, the following diagram commutes: \[ \text{image}(f) \xrightarrow{\cong} I' \xrightarrow{m} Y = \text{image}(f) \xrightarrow{\iota} Y. \]

CategoryTheory.Limits.image.isoStrongEpiMono_inv_comp_mono theorem

 {I' : C} (e : X ⟶ I') (m : I' ⟶ Y) (comm : e ≫ m = f) [StrongEpi e] [Mono m] :
  (image.isoStrongEpiMono e m comm).inv ≫ m = image.ι f

Full source

@[simp]
theorem image.isoStrongEpiMono_inv_comp_mono {I' : C} (e : X ⟶ I') (m : I' ⟶ Y) (comm : e ≫ m = f)
    [StrongEpi e] [Mono m] : (image.isoStrongEpiMono e m comm).inv ≫ m = image.ι f :=
  image.lift_fac _

Inverse Isomorphism Composes to Image Inclusion in Strong Epi-Mono Factorization

Informal description

Given a morphism $f \colon X \to Y$ in a category $C$, and a factorization $f = e \circ m$ where $e \colon X \to I'$ is a strong epimorphism and $m \colon I' \to Y$ is a monomorphism, the composition of the inverse of the isomorphism $\text{image.isoStrongEpiMono}\, e\, m\, \text{comm} \colon I' \cong \text{image}(f)$ with $m$ equals the image inclusion morphism $\iota \colon \text{image}(f) \to Y$. In other words, the diagram \[ \text{image}(f) \xrightarrow{\text{image.isoStrongEpiMono}\, e\, m\, \text{comm}^{-1}} I' \xrightarrow{m} Y \] commutes and equals $\iota$.

CategoryTheory.Limits.functorialEpiMonoFactorizationData definition

: FunctorialFactorizationData (epimorphisms C) (monomorphisms C)

Full source

/-- A category with strong epi mono factorisations admits functorial epi/mono factorizations. -/
noncomputable def functorialEpiMonoFactorizationData :
    FunctorialFactorizationData (epimorphisms C) (monomorphisms C) where
  Z := im
  i := { app := fun f => factorThruImage f.hom }
  p := { app := fun f => image.ι f.hom }
  hi _ := epimorphisms.infer_property _
  hp _ := monomorphisms.infer_property _

Functorial epi-mono factorization data

Informal description

The functorial factorization data for a category $ C $ with strong epi-mono factorisations, which provides a functorial way to factor any morphism $ f $ in $ C $ as $ f = e \circ m $, where $ e $ is an epimorphism and $ m $ is a monomorphism. Specifically: - The functor $ Z $ maps each morphism $ f $ to its image object $ \text{image}(f) $. - The natural transformation $ i $ maps each morphism $ f $ to the factorization morphism $ \text{factorThruImage}(f) $, which is an epimorphism. - The natural transformation $ p $ maps each morphism $ f $ to the image inclusion morphism $ \text{image.ι}(f) $, which is a monomorphism.

CategoryTheory.Functor.hasStrongEpiMonoFactorisations_imp_of_isEquivalence theorem

(F : C ⥤ D) [IsEquivalence F] [h : HasStrongEpiMonoFactorisations C] : HasStrongEpiMonoFactorisations D

Full source

theorem hasStrongEpiMonoFactorisations_imp_of_isEquivalence (F : C ⥤ D) [IsEquivalence F]
    [h : HasStrongEpiMonoFactorisations C] : HasStrongEpiMonoFactorisations D :=
  ⟨fun {X} {Y} f => by
    let em : StrongEpiMonoFactorisation (F.inv.map f) :=
      (HasStrongEpiMonoFactorisations.has_fac (F.inv.map f)).some
    haveI : Mono (F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y) := mono_comp _ _
    haveI : StrongEpi (F.asEquivalence.counitIso.inv.app X ≫ F.map em.e) := strongEpi_comp _ _
    exact
      Nonempty.intro
        { I := F.obj em.I
          e := F.asEquivalence.counitIso.inv.app X ≫ F.map em.e
          m := F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y
          fac := by
            simp only [asEquivalence_functor, Category.assoc, ← F.map_comp_assoc,
              MonoFactorisation.fac, fun_inv_map, id_obj, Iso.inv_hom_id_app, Category.comp_id,
              Iso.inv_hom_id_app_assoc] }⟩

Equivalences preserve strong epi-mono factorisations

Informal description

Let $F \colon C \to D$ be an equivalence of categories. If $C$ has strong epi-mono factorisations, then $D$ also has strong epi-mono factorisations. That is, every morphism in $D$ can be factored as a strong epimorphism followed by a monomorphism.

Mathlib.CategoryTheory.Limits.Shapes.Images

Main definitions

Main statements

Future work