# mathlibdocumentation

category_theory.limits.shapes.images

# Categorical images #

We define the categorical image of `f` as a factorisation `f = e ≫ m` through a monomorphism `m`, so that `m` factors through the `m'` in any other such factorisation.

## Main definitions #

• A `mono_factorisation` is a factorisation `f = e ≫ m`, where `m` is a monomorphism

• `is_image F` means that a given mono factorisation `F` has the universal property of the image.

• `has_image f` means that there is some image factorization for the morphism `f : X ⟶ Y`.

• In this case, `image f` is some image object (selected with choice), `image.ι f : image f ⟶ Y` is the monomorphism `m` of the factorisation and `factor_thru_image f : X ⟶ image f` is the morphism `e`.
• `has_images C` means that every morphism in `C` has an image.

• Let `f : X ⟶ Y` and `g : P ⟶ Q` be morphisms in `C`, which we will represent as objects of the arrow category `arrow C`. Then `sq : f ⟶ g` is a commutative square in `C`. If `f` and `g` have images, then `has_image_map sq` represents the fact that there is a morphism `i : image f ⟶ image g` making the diagram

X ----→ image f ----→ Y | | | | | | ↓ ↓ ↓ P ----→ image g ----→ Q

commute, where the top row is the image factorisation of `f`, the bottom row is the image factorisation of `g`, and the outer rectangle is the commutative square `sq`.

• If a category `has_images`, then `has_image_maps` means that every commutative square admits an image map.

• If a category `has_images`, then `has_strong_epi_images` means that the morphism to the image is always a strong epimorphism.

## Main statements #

• When `C` has equalizers, the morphism `e` appearing in an image factorisation is an epimorphism.
• When `C` has strong epi images, then these images admit image maps.

## Future work #

• TODO: coimages, and abelian categories.
• TODO: connect this with existing working in the group theory and ring theory libraries.
structure category_theory.limits.mono_factorisation {C : Type u} {X Y : C} (f : X Y) :
Type (max u v)
• I : C
• m : self.I Y
• m_mono :
• e : X self.I
• fac' : self.e self.m = f . "obviously"

A factorisation of a morphism `f = e ≫ m`, with `m` monic.

Instances for `category_theory.limits.mono_factorisation`
@[simp]
theorem category_theory.limits.mono_factorisation.fac {C : Type u} {X Y : C} {f : X Y}  :
self.e self.m = f
@[simp]
theorem category_theory.limits.mono_factorisation.fac_assoc {C : Type u} {X Y : C} {f : X Y} {X' : C} (f' : Y X') :
self.e self.m f' = f f'
def category_theory.limits.mono_factorisation.self {C : Type u} {X Y : C} (f : X Y)  :

The obvious factorisation of a monomorphism through itself.

Equations
@[protected, instance]
def category_theory.limits.mono_factorisation.inhabited {C : Type u} {X Y : C} (f : X Y)  :
Equations
@[ext]
theorem category_theory.limits.mono_factorisation.ext {C : Type u} {X Y : C} {f : X Y} (hI : F.I = F'.I) (hm : F.m = ) :
F = F'

The morphism `m` in a factorisation `f = e ≫ m` through a monomorphism is uniquely determined.

@[simp]
theorem category_theory.limits.mono_factorisation.comp_mono_I {C : Type u} {X Y : C} {f : X Y} {Y' : C} (g : Y Y')  :
(F.comp_mono g).I = F.I
def category_theory.limits.mono_factorisation.comp_mono {C : Type u} {X Y : C} {f : X Y} {Y' : C} (g : Y Y')  :

Any mono factorisation of `f` gives a mono factorisation of `f ≫ g` when `g` is a mono.

Equations
@[simp]
theorem category_theory.limits.mono_factorisation.comp_mono_e {C : Type u} {X Y : C} {f : X Y} {Y' : C} (g : Y Y')  :
(F.comp_mono g).e = F.e
@[simp]
theorem category_theory.limits.mono_factorisation.comp_mono_m {C : Type u} {X Y : C} {f : X Y} {Y' : C} (g : Y Y')  :
(F.comp_mono g).m = F.m g
@[simp]
theorem category_theory.limits.mono_factorisation.of_comp_iso_e {C : Type u} {X Y : C} {f : X Y} {Y' : C} {g : Y Y'} (F : category_theory.limits.mono_factorisation (f g)) :
noncomputable def category_theory.limits.mono_factorisation.of_comp_iso {C : Type u} {X Y : C} {f : X Y} {Y' : C} {g : Y Y'} (F : category_theory.limits.mono_factorisation (f g)) :

A mono factorisation of `f ≫ g`, where `g` is an isomorphism, gives a mono factorisation of `f`.

Equations
@[simp]
theorem category_theory.limits.mono_factorisation.of_comp_iso_m {C : Type u} {X Y : C} {f : X Y} {Y' : C} {g : Y Y'} (F : category_theory.limits.mono_factorisation (f g)) :
@[simp]
theorem category_theory.limits.mono_factorisation.of_comp_iso_I {C : Type u} {X Y : C} {f : X Y} {Y' : C} {g : Y Y'} (F : category_theory.limits.mono_factorisation (f g)) :
@[simp]
theorem category_theory.limits.mono_factorisation.iso_comp_I {C : Type u} {X Y : C} {f : X Y} {X' : C} (g : X' X) :
(F.iso_comp g).I = F.I
@[simp]
theorem category_theory.limits.mono_factorisation.iso_comp_m {C : Type u} {X Y : C} {f : X Y} {X' : C} (g : X' X) :
(F.iso_comp g).m = F.m
def category_theory.limits.mono_factorisation.iso_comp {C : Type u} {X Y : C} {f : X Y} {X' : C} (g : X' X) :

Any mono factorisation of `f` gives a mono factorisation of `g ≫ f`.

Equations
@[simp]
theorem category_theory.limits.mono_factorisation.iso_comp_e {C : Type u} {X Y : C} {f : X Y} {X' : C} (g : X' X) :
(F.iso_comp g).e = g F.e
@[simp]
theorem category_theory.limits.mono_factorisation.of_iso_comp_m {C : Type u} {X Y : C} {f : X Y} {X' : C} (g : X' X) (F : category_theory.limits.mono_factorisation (g f)) :
noncomputable def category_theory.limits.mono_factorisation.of_iso_comp {C : Type u} {X Y : C} {f : X Y} {X' : C} (g : X' X) (F : category_theory.limits.mono_factorisation (g f)) :

A mono factorisation of `g ≫ f`, where `g` is an isomorphism, gives a mono factorisation of `f`.

Equations
@[simp]
theorem category_theory.limits.mono_factorisation.of_iso_comp_I {C : Type u} {X Y : C} {f : X Y} {X' : C} (g : X' X) (F : category_theory.limits.mono_factorisation (g f)) :
@[simp]
theorem category_theory.limits.mono_factorisation.of_iso_comp_e {C : Type u} {X Y : C} {f : X Y} {X' : C} (g : X' X) (F : category_theory.limits.mono_factorisation (g f)) :
@[simp]
noncomputable def category_theory.limits.mono_factorisation.of_arrow_iso {C : Type u} {f g : category_theory.arrow C} (sq : f g)  :

If `f` and `g` are isomorphic arrows, then a mono factorisation of `f` gives a mono factorisation of `g`

Equations
@[simp]
@[simp]
structure category_theory.limits.is_image {C : Type u} {X Y : C} {f : X Y}  :
Type (max u v)
• lift : Π (F' : , F.I F'.I
• lift_fac' : (∀ (F' : , self.lift F' F'.m = F.m) . "obviously"

Data exhibiting that a given factorisation through a mono is initial.

Instances for `category_theory.limits.is_image`
@[simp]
theorem category_theory.limits.is_image.lift_fac {C : Type u} {X Y : C} {f : X Y} (self : category_theory.limits.is_image F)  :
self.lift F' F'.m = F.m
@[simp]
theorem category_theory.limits.is_image.lift_fac_assoc {C : Type u} {X Y : C} {f : X Y} (self : category_theory.limits.is_image F) {X' : C} (f' : Y X') :
self.lift F' F'.m f' = F.m f'
@[simp]
theorem category_theory.limits.is_image.fac_lift {C : Type u} {X Y : C} {f : X Y}  :
F.e hF.lift F' = F'.e
@[simp]
theorem category_theory.limits.is_image.fac_lift_assoc {C : Type u} {X Y : C} {f : X Y} {X' : C} (f' : F'.I X') :
F.e hF.lift F' f' = F'.e f'
@[simp]
theorem category_theory.limits.is_image.self_lift {C : Type u} {X Y : C} (f : X Y)  :
= F'.e
def category_theory.limits.is_image.self {C : Type u} {X Y : C} (f : X Y)  :

The trivial factorisation of a monomorphism satisfies the universal property.

Equations
@[protected, instance]
def category_theory.limits.is_image.inhabited {C : Type u} {X Y : C} (f : X Y)  :
Equations
def category_theory.limits.is_image.iso_ext {C : Type u} {X Y : C} {f : X Y} (hF' : category_theory.limits.is_image F') :
F.I F'.I

Two factorisations through monomorphisms satisfying the universal property must factor through isomorphic objects.

Equations
@[simp]
theorem category_theory.limits.is_image.iso_ext_hom {C : Type u} {X Y : C} {f : X Y} (hF' : category_theory.limits.is_image F') :
(hF.iso_ext hF').hom = hF.lift F'
@[simp]
theorem category_theory.limits.is_image.iso_ext_inv {C : Type u} {X Y : C} {f : X Y} (hF' : category_theory.limits.is_image F') :
(hF.iso_ext hF').inv = hF'.lift F
theorem category_theory.limits.is_image.iso_ext_hom_m {C : Type u} {X Y : C} {f : X Y} (hF' : category_theory.limits.is_image F') :
(hF.iso_ext hF').hom F'.m = F.m
theorem category_theory.limits.is_image.iso_ext_inv_m {C : Type u} {X Y : C} {f : X Y} (hF' : category_theory.limits.is_image F') :
(hF.iso_ext hF').inv F.m = F'.m
theorem category_theory.limits.is_image.e_iso_ext_hom {C : Type u} {X Y : C} {f : X Y} (hF' : category_theory.limits.is_image F') :
F.e (hF.iso_ext hF').hom = F'.e
theorem category_theory.limits.is_image.e_iso_ext_inv {C : Type u} {X Y : C} {f : X Y} (hF' : category_theory.limits.is_image F') :
F'.e (hF.iso_ext hF').inv = F.e
@[simp]
noncomputable def category_theory.limits.is_image.of_arrow_iso {C : Type u} {f g : category_theory.arrow C} (sq : f g)  :

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

Equations
structure category_theory.limits.image_factorisation {C : Type u} {X Y : C} (f : X Y) :
Type (max u v)
• F :
• is_image :

Data exhibiting that a morphism `f` has an image.

Instances for `category_theory.limits.image_factorisation`
@[protected, instance]
def category_theory.limits.image_factorisation.inhabited {C : Type u} {X Y : C} (f : X Y)  :
Equations
noncomputable def category_theory.limits.image_factorisation.of_arrow_iso {C : Type u} {f g : category_theory.arrow C} (sq : f g)  :

If `f` and `g` are isomorphic arrows, then an image factorisation of `f` gives an image factorisation of `g`

Equations
@[simp]
@[class]
structure category_theory.limits.has_image {C : Type u} {X Y : C} (f : X Y) :
Prop
• exists_image :

`has_image f` means that there exists an image factorisation of `f`.

Instances of this typeclass
theorem category_theory.limits.has_image.mk {C : Type u} {X Y : C} {f : X Y}  :
theorem category_theory.limits.has_image.of_arrow_iso {C : Type u} {f g : category_theory.arrow C} (sq : f g)  :
@[protected, instance]
def category_theory.limits.mono_has_image {C : Type u} {X Y : C} (f : X Y)  :
noncomputable def category_theory.limits.image.mono_factorisation {C : Type u} {X Y : C} (f : X Y)  :

Some factorisation of `f` through a monomorphism (selected with choice).

Equations
noncomputable def category_theory.limits.image.is_image {C : Type u} {X Y : C} (f : X Y)  :

The witness of the universal property for the chosen factorisation of `f` through a monomorphism.

Equations
noncomputable def category_theory.limits.image {C : Type u} {X Y : C} (f : X Y)  :
C

The categorical image of a morphism.

Equations
noncomputable def category_theory.limits.image.ι {C : Type u} {X Y : C} (f : X Y)  :

The inclusion of the image of a morphism into the target.

Equations
Instances for `category_theory.limits.image.ι`
@[simp]
theorem category_theory.limits.image.as_ι {C : Type u} {X Y : C} (f : X Y)  :
@[protected, instance]
def category_theory.limits.image.ι.category_theory.mono {C : Type u} {X Y : C} (f : X Y)  :
noncomputable def category_theory.limits.factor_thru_image {C : Type u} {X Y : C} (f : X Y)  :

The map from the source to the image of a morphism.

Equations
Instances for `category_theory.limits.factor_thru_image`
@[simp]
theorem category_theory.limits.as_factor_thru_image {C : Type u} {X Y : C} (f : X Y)  :

Rewrite in terms of the `factor_thru_image` interface.

@[simp]
theorem category_theory.limits.image.fac {C : Type u} {X Y : C} (f : X Y)  :
@[simp]
theorem category_theory.limits.image.fac_assoc {C : Type u} {X Y : C} (f : X Y) {X' : C} (f' : Y X') :
noncomputable def category_theory.limits.image.lift {C : Type u} {X Y : C} {f : X Y}  :

Any other factorisation of the morphism `f` through a monomorphism receives a map from the image.

Equations
Instances for `category_theory.limits.image.lift`
@[simp]
theorem category_theory.limits.image.lift_fac_assoc {C : Type u} {X Y : C} {f : X Y} {X' : C} (f' : Y X') :
F'.m f' =
@[simp]
theorem category_theory.limits.image.lift_fac {C : Type u} {X Y : C} {f : X Y}  :
@[simp]
theorem category_theory.limits.image.fac_lift_assoc {C : Type u} {X Y : C} {f : X Y} {X' : C} (f' : F'.I X') :
@[simp]
theorem category_theory.limits.image.fac_lift {C : Type u} {X Y : C} {f : X Y}  :
@[simp]
theorem category_theory.limits.image.is_image_lift {C : Type u} {X Y : C} {f : X Y}  :
@[simp]
theorem category_theory.limits.is_image.lift_ι {C : Type u} {X Y : C} {f : X Y}  :
@[simp]
theorem category_theory.limits.is_image.lift_ι_assoc {C : Type u} {X Y : C} {f : X Y} {X' : C} (f' : Y X') :
= F.m f'
@[protected, instance]
def category_theory.limits.image.lift_mono {C : Type u} {X Y : C} {f : X Y}  :
theorem category_theory.limits.has_image.uniq {C : Type u} {X Y : C} {f : X Y} (l : F'.I) (w : l F'.m = ) :
@[protected, instance]
def category_theory.limits.category_theory.category_struct.comp.has_image {C : Type u} {X Y Z : C} (f : X Y) (g : Y Z)  :

If `has_image g`, then `has_image (f ≫ g)` when `f` is an isomorphism.

@[class]
structure category_theory.limits.has_images (C : Type u)  :
Prop
• has_image : ∀ {X Y : C} (f : X Y),

`has_images` asserts that every morphism has an image.

Instances of this typeclass
noncomputable def category_theory.limits.image_mono_iso_source {C : Type u} {X Y : C} (f : X Y)  :

The image of a monomorphism is isomorphic to the source.

Equations
@[simp]
theorem category_theory.limits.image_mono_iso_source_inv_ι_assoc {C : Type u} {X Y : C} (f : X Y) {X' : C} (f' : Y X') :
@[simp]
theorem category_theory.limits.image_mono_iso_source_inv_ι {C : Type u} {X Y : C} (f : X Y)  :
@[simp]
theorem category_theory.limits.image_mono_iso_source_hom_self {C : Type u} {X Y : C} (f : X Y)  :
@[simp]
theorem category_theory.limits.image_mono_iso_source_hom_self_assoc {C : Type u} {X Y : C} (f : X Y) {X' : C} (f' : Y X') :
@[ext]
theorem category_theory.limits.image.ext {C : Type u} {X Y : C} (f : X Y) {W : C} {g h : W}  :
g = h
@[protected, instance]
def category_theory.limits.factor_thru_image.category_theory.epi {C : Type u} {X Y : C} (f : X Y) [∀ {Z : C} (g h : , ] :
theorem category_theory.limits.epi_image_of_epi {C : Type u} {X Y : C} (f : X Y) [E : category_theory.epi f] :
theorem category_theory.limits.epi_of_epi_image {C : Type u} {X Y : C} (f : X Y)  :
noncomputable def category_theory.limits.image.eq_to_hom {C : Type u} {X Y : C} {f f' : X Y} (h : f = f') :

An equation between morphisms gives a comparison map between the images (which momentarily we prove is an iso).

Equations
Instances for `category_theory.limits.image.eq_to_hom`
@[protected, instance]
def category_theory.limits.image.eq_to_hom.category_theory.is_iso {C : Type u} {X Y : C} {f f' : X Y} (h : f = f') :
noncomputable def category_theory.limits.image.eq_to_iso {C : Type u} {X Y : C} {f f' : X Y} (h : f = f') :

An equation between morphisms gives an isomorphism between the images.

Equations
theorem category_theory.limits.image.eq_fac {C : Type u} {X Y : C} {f f' : X Y} (h : f = f') :

As long as the category has equalizers, the image inclusion maps commute with `image.eq_to_iso`.

noncomputable def category_theory.limits.image.pre_comp {C : Type u} {X Y : C} (f : X Y) {Z : C} (g : Y Z)  :

The comparison map `image (f ≫ g) ⟶ image g`.

Equations
Instances for `category_theory.limits.image.pre_comp`
@[simp]
theorem category_theory.limits.image.pre_comp_ι {C : Type u} {X Y : C} (f : X Y) {Z : C} (g : Y Z)  :
@[simp]
theorem category_theory.limits.image.pre_comp_ι_assoc {C : Type u} {X Y : C} (f : X Y) {Z : C} (g : Y Z) {X' : C} (f' : Z X') :
@[simp]
theorem category_theory.limits.image.factor_thru_image_pre_comp_assoc {C : Type u} {X Y : C} (f : X Y) {Z : C} (g : Y Z) {X' : C} (f' : X') :
@[simp]
theorem category_theory.limits.image.factor_thru_image_pre_comp {C : Type u} {X Y : C} (f : X Y) {Z : C} (g : Y Z)  :
@[protected, instance]
def category_theory.limits.image.pre_comp_mono {C : Type u} {X Y : C} (f : X Y) {Z : C} (g : Y Z)  :

`image.pre_comp f g` is a monomorphism.

theorem category_theory.limits.image.pre_comp_comp {C : Type u} {X Y : C} (f : X Y) {Z : C} (g : Y Z) {W : C} (h : Z W) [category_theory.limits.has_image (f g h)] [category_theory.limits.has_image ((f g) h)] :

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

@[protected, instance]
def category_theory.limits.image.pre_comp_epi_of_epi {C : Type u} {X Y : C} (f : X Y) {Z : C} (g : Y Z)  :

`image.pre_comp f g` is an epimorphism when `f` is an epimorphism (we need `C` to have equalizers to prove this).

@[protected, instance]
def category_theory.limits.has_image_iso_comp {C : Type u} {X Y : C} (f : X Y) {Z : C} (g : Y Z)  :
@[protected, instance]
def category_theory.limits.image.is_iso_precomp_iso {C : Type u} {X Y Z : C} (g : Y Z) (f : X Y)  :

`image.pre_comp f g` is an isomorphism when `f` is an isomorphism (we need `C` to have equalizers to prove this).

@[protected, instance]
def category_theory.limits.has_image_comp_iso {C : Type u} {X Y : C} (f : X Y) {Z : C} (g : Y Z)  :
noncomputable def category_theory.limits.image.comp_iso {C : Type u} {X Y : C} (f : X Y) {Z : C} (g : Y Z)  :

Postcomposing by an isomorphism induces an isomorphism on the image.

Equations
@[simp]
theorem category_theory.limits.image.comp_iso_hom_comp_image_ι {C : Type u} {X Y : C} (f : X Y) {Z : C} (g : Y Z)  :
@[simp]
theorem category_theory.limits.image.comp_iso_hom_comp_image_ι_assoc {C : Type u} {X Y : C} (f : X Y) {Z : C} (g : Y Z) {X' : C} (f' : Z X') :
=
@[simp]
theorem category_theory.limits.image.comp_iso_inv_comp_image_ι_assoc {C : Type u} {X Y : C} (f : X Y) {Z : C} (g : Y Z) {X' : C} (f' : Y X') :
@[simp]
theorem category_theory.limits.image.comp_iso_inv_comp_image_ι {C : Type u} {X Y : C} (f : X Y) {Z : C} (g : Y Z)  :
@[protected, instance]
def category_theory.limits.hom.has_image {C : Type u} {X Y : C} (f : X Y)  :
structure category_theory.limits.image_map {C : Type u} {f g : category_theory.arrow C} (sq : f g) :
Type v
• map :
• map_ι' : . "obviously"

An image map is a morphism `image f → image g` fitting into a commutative square and satisfying the obvious commutativity conditions.

Instances for `category_theory.limits.image_map`
@[protected, instance]
noncomputable def category_theory.limits.inhabited_image_map {C : Type u} {f : category_theory.arrow C}  :
Equations
@[simp]
@[simp]
theorem category_theory.limits.image_map.map_ι_assoc {C : Type u} {f g : category_theory.arrow C} {sq : f g} (self : category_theory.limits.image_map sq) {X' : C} (f' : g.right X') :
self.map = sq.right f'
@[simp]
theorem category_theory.limits.image_map.factor_map_assoc {C : Type u} {f g : category_theory.arrow C} (sq : f g) {X' : C} (f' : X') :
@[simp]
theorem category_theory.limits.image_map.factor_map {C : Type u} {f g : category_theory.arrow C} (sq : f g)  :
noncomputable def category_theory.limits.image_map.transport {C : Type u} {f g : category_theory.arrow C} (sq : f g) (hF' : category_theory.limits.is_image F') {map : F.I F'.I} (map_ι : map F'.m = F.m sq.right) :

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

Equations
@[class]
structure category_theory.limits.has_image_map {C : Type u} {f g : category_theory.arrow C} (sq : f g) :
Prop
• has_image_map :

`has_image_map sq` means that there is an `image_map` for the square `sq`.

Instances of this typeclass
theorem category_theory.limits.has_image_map.mk {C : Type u} {f g : category_theory.arrow C} {sq : f g}  :
theorem category_theory.limits.has_image_map.transport {C : Type u} {f g : category_theory.arrow C} (sq : f g) (hF' : category_theory.limits.is_image F') (map : F.I F'.I) (map_ι : map F'.m = F.m sq.right) :
noncomputable def category_theory.limits.has_image_map.image_map {C : Type u} {f g : category_theory.arrow C} (sq : f g)  :

Obtain an `image_map` from a `has_image_map` instance.

Equations
@[protected, instance]
@[protected, instance]
def category_theory.limits.has_image_map.comp {C : Type u} {f g h : category_theory.arrow C} (sq1 : f g) (sq2 : g h)  :
@[protected, instance]
@[reducible]
noncomputable def category_theory.limits.image.map {C : Type u} {f g : category_theory.arrow C} (sq : f g)  :

The map on images induced by a commutative square.

theorem category_theory.limits.image.map_ι {C : Type u} {f g : category_theory.arrow C} (sq : f g)  :
theorem category_theory.limits.image.map_hom_mk'_ι {C : Type u} {X Y P Q : C} {k : X Y} {l : P Q} {m : X P} {n : Y Q} (w : m l = k n)  :
noncomputable def category_theory.limits.image_map_comp {C : Type u} {f g : category_theory.arrow C} (sq : f g) {h : category_theory.arrow C} (sq' : g h)  :

Image maps for composable commutative squares induce an image map in the composite square.

Equations
@[simp]
theorem category_theory.limits.image.map_comp {C : Type u} {f g : category_theory.arrow C} (sq : f g) {h : category_theory.arrow C} (sq' : g h) [category_theory.limits.has_image_map (sq sq')] :
noncomputable def category_theory.limits.image_map_id {C : Type u} (f : category_theory.arrow C)  :

The identity `image f ⟶ image f` fits into the commutative square represented by the identity morphism `𝟙 f` in the arrow category.

Equations
@[simp]
@[class]
structure category_theory.limits.has_image_maps (C : Type u)  :
Type
• has_image_map : ∀ {f g : (st : f g),

If a category `has_image_maps`, then all commutative squares induce morphisms on images.

Instances of this typeclass
Instances of other typeclasses for `category_theory.limits.has_image_maps`
• category_theory.limits.has_image_maps.has_sizeof_inst
noncomputable def category_theory.limits.im {C : Type u}  :

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.

Equations
@[simp]
theorem category_theory.limits.im_map {C : Type u} (_x _x_1 : category_theory.arrow C) (st : _x _x_1) :
@[simp]
structure category_theory.limits.strong_epi_mono_factorisation {C : Type u} {X Y : C} (f : X Y) :
Type (max u v)
• to_mono_factorisation :
• e_strong_epi :

A strong epi-mono factorisation is a decomposition `f = e ≫ m` with `e` a strong epimorphism and `m` a monomorphism.

Instances for `category_theory.limits.strong_epi_mono_factorisation`
@[protected, instance]
def category_theory.limits.strong_epi_mono_factorisation_inhabited {C : Type u} {X Y : C} (f : X Y)  :

Satisfying the inhabited linter

Equations
noncomputable def category_theory.limits.strong_epi_mono_factorisation.to_mono_is_image {C : Type u} {X Y : C} {f : X Y}  :

A mono factorisation coming from a strong epi-mono factorisation always has the universal property of the image.

Equations
@[class]
• has_fac : ∀ {X Y : C} (f : X Y),

A category has strong epi-mono factorisations if every morphism admits a strong epi-mono factorisation.

Instances of this typeclass
theorem category_theory.limits.has_strong_epi_mono_factorisations.mk {C : Type u} (d : Π {X Y : C} (f : X Y), ) :
@[protected, instance]
@[class]
structure category_theory.limits.has_strong_epi_images (C : Type u)  :
Prop
• strong_factor_thru_image : ∀ {X Y : C} (f : X Y),

A category has strong epi images if it has all images and `factor_thru_image f` is a strong epimorphism for all `f`.

Instances of this typeclass

If there is a single strong epi-mono factorisation of `f`, then every image factorisation is a strong epi-mono factorisation.

@[protected, instance]

If we constructed our images from strong epi-mono factorisations, then these images are strong epi images.

@[protected, instance]

A category with strong epi images has image maps.

Equations
@[protected, instance]

If a category has images, equalizers and pullbacks, then images are automatically strong epi images.

noncomputable def category_theory.limits.image.iso_strong_epi_mono {C : Type u} {X Y : C} {f : X Y} {I' : C} (e : X I') (m : I' Y) (comm : e m = f)  :

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.

Equations
@[simp]
theorem category_theory.limits.image.iso_strong_epi_mono_hom_comp_ι {C : Type u} {X Y : C} {f : X Y} {I' : C} (e : X I') (m : I' Y) (comm : e m = f)  :
@[simp]
theorem category_theory.limits.image.iso_strong_epi_mono_inv_comp_mono {C : Type u} {X Y : C} {f : X Y} {I' : C} (e : X I') (m : I' Y) (comm : e m = f)  :