# 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 MonoFactorisation is a factorisation f = e ≫ m, where m is a monomorphism

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

• HasImage 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 factorThruImage f : X ⟶ image f is the morphism e.
• HasImages 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 HasImageMap 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 HasImages, then HasImageMaps means that every commutative square admits an image map.

• If a category HasImages, then HasStrongEpiImages 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 CategoryTheory.Limits.MonoFactorisation {C : Type u} {X : C} {Y : C} (f : X Y) :
Type (max u v)

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

• I : C

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

• m : self.I Y

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

• m_mono : CategoryTheory.Mono self.m

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

• e : X self.I

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

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

Instances For
theorem CategoryTheory.Limits.MonoFactorisation.m_mono {C : Type u} {X : C} {Y : C} {f : X Y} (self : ) :

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

@[simp]
theorem CategoryTheory.Limits.MonoFactorisation.fac {C : Type u} {X : C} {Y : C} {f : X Y} (self : ) :

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

@[simp]
theorem CategoryTheory.Limits.MonoFactorisation.fac_assoc {C : Type u} {X : C} {Y : C} {f : X Y} (self : ) {Z : C} (h : Y Z) :
def CategoryTheory.Limits.MonoFactorisation.self {C : Type u} {X : C} {Y : C} (f : X Y) :

The obvious factorisation of a monomorphism through itself.

Equations
Instances For
instance CategoryTheory.Limits.MonoFactorisation.instInhabitedOfMono {C : Type u} {X : C} {Y : C} (f : X Y) :
Equations
theorem CategoryTheory.Limits.MonoFactorisation.ext {C : Type u} {X : C} {Y : C} {f : X Y} (hI : F.I = F'.I) (hm : ) :
F = F'

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

@[simp]
theorem CategoryTheory.Limits.MonoFactorisation.compMono_m {C : Type u} {X : C} {Y : C} {f : X Y} {Y' : C} (g : Y Y') :
(F.compMono g).m =
@[simp]
theorem CategoryTheory.Limits.MonoFactorisation.compMono_I {C : Type u} {X : C} {Y : C} {f : X Y} {Y' : C} (g : Y Y') :
(F.compMono g).I = F.I
@[simp]
theorem CategoryTheory.Limits.MonoFactorisation.compMono_e {C : Type u} {X : C} {Y : C} {f : X Y} {Y' : C} (g : Y Y') :
(F.compMono g).e = F.e
def CategoryTheory.Limits.MonoFactorisation.compMono {C : Type u} {X : C} {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
• F.compMono g =
Instances For
@[simp]
theorem CategoryTheory.Limits.MonoFactorisation.ofCompIso_e {C : Type u} {X : C} {Y : C} {f : X Y} {Y' : C} {g : Y Y'} :
F.ofCompIso.e = F.e
@[simp]
theorem CategoryTheory.Limits.MonoFactorisation.ofCompIso_I {C : Type u} {X : C} {Y : C} {f : X Y} {Y' : C} {g : Y Y'} :
F.ofCompIso.I = F.I
@[simp]
theorem CategoryTheory.Limits.MonoFactorisation.ofCompIso_m {C : Type u} {X : C} {Y : C} {f : X Y} {Y' : C} {g : Y Y'} :
F.ofCompIso.m =
def CategoryTheory.Limits.MonoFactorisation.ofCompIso {C : Type u} {X : C} {Y : C} {f : X Y} {Y' : C} {g : Y Y'} :

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

Equations
• F.ofCompIso =
Instances For
@[simp]
theorem CategoryTheory.Limits.MonoFactorisation.isoComp_e {C : Type u} {X : C} {Y : C} {f : X Y} {X' : C} (g : X' X) :
(F.isoComp g).e =
@[simp]
theorem CategoryTheory.Limits.MonoFactorisation.isoComp_I {C : Type u} {X : C} {Y : C} {f : X Y} {X' : C} (g : X' X) :
(F.isoComp g).I = F.I
@[simp]
theorem CategoryTheory.Limits.MonoFactorisation.isoComp_m {C : Type u} {X : C} {Y : C} {f : X Y} {X' : C} (g : X' X) :
(F.isoComp g).m = F.m
def CategoryTheory.Limits.MonoFactorisation.isoComp {C : Type u} {X : C} {Y : C} {f : X Y} {X' : C} (g : X' X) :

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

Equations
• F.isoComp g =
Instances For
@[simp]
theorem CategoryTheory.Limits.MonoFactorisation.ofIsoComp_e {C : Type u} {X : C} {Y : C} {f : X Y} {X' : C} (g : X' X) :
@[simp]
theorem CategoryTheory.Limits.MonoFactorisation.ofIsoComp_m {C : Type u} {X : C} {Y : C} {f : X Y} {X' : C} (g : X' X) :
@[simp]
theorem CategoryTheory.Limits.MonoFactorisation.ofIsoComp_I {C : Type u} {X : C} {Y : C} {f : X Y} {X' : C} (g : X' X) :
def CategoryTheory.Limits.MonoFactorisation.ofIsoComp {C : Type u} {X : C} {Y : C} {f : X Y} {X' : C} (g : X' X) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.MonoFactorisation.ofArrowIso_I {C : Type u} {f : } {g : } (F : ) (sq : f g) [] :
(F.ofArrowIso sq).I = F.I
@[simp]
theorem CategoryTheory.Limits.MonoFactorisation.ofArrowIso_e {C : Type u} {f : } {g : } (F : ) (sq : f g) [] :
(F.ofArrowIso sq).e = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv sq.left) F.e
@[simp]
theorem CategoryTheory.Limits.MonoFactorisation.ofArrowIso_m {C : Type u} {f : } {g : } (F : ) (sq : f g) [] :
(F.ofArrowIso sq).m = CategoryTheory.CategoryStruct.comp F.m sq.right
def CategoryTheory.Limits.MonoFactorisation.ofArrowIso {C : Type u} {f : } {g : } (F : ) (sq : f g) [] :

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

Equations
Instances For
structure CategoryTheory.Limits.IsImage {C : Type u} {X : C} {Y : C} {f : X Y} :
Type (max u v)

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

• lift : (F' : ) → F.I F'.I

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

• lift_fac : ∀ (F' : ), CategoryTheory.CategoryStruct.comp (self.lift F') F'.m = F.m

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

Instances For
@[simp]
theorem CategoryTheory.Limits.IsImage.lift_fac {C : Type u} {X : C} {Y : C} {f : X Y} (self : ) :
CategoryTheory.CategoryStruct.comp (self.lift F') F'.m = F.m

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

@[simp]
theorem CategoryTheory.Limits.IsImage.lift_fac_assoc {C : Type u} {X : C} {Y : C} {f : X Y} (self : ) {Z : C} (h : Y Z) :
@[simp]
theorem CategoryTheory.Limits.IsImage.fac_lift_assoc {C : Type u} {X : C} {Y : C} {f : X Y} (hF : ) {Z : C} (h : F'.I Z) :
@[simp]
theorem CategoryTheory.Limits.IsImage.fac_lift {C : Type u} {X : C} {Y : C} {f : X Y} (hF : ) :
@[simp]
theorem CategoryTheory.Limits.IsImage.self_lift {C : Type u} {X : C} {Y : C} (f : X Y) :
.lift F' = F'.e
def CategoryTheory.Limits.IsImage.self {C : Type u} {X : C} {Y : C} (f : X Y) :

The trivial factorisation of a monomorphism satisfies the universal property.

Equations
• = { lift := fun (F' : ) => F'.e, lift_fac := }
Instances For
instance CategoryTheory.Limits.IsImage.instInhabitedSelf {C : Type u} {X : C} {Y : C} (f : X Y) :
Equations
@[simp]
theorem CategoryTheory.Limits.IsImage.isoExt_inv {C : Type u} {X : C} {Y : C} {f : X Y} (hF : ) (hF' : ) :
(hF.isoExt hF').inv = hF'.lift F
@[simp]
theorem CategoryTheory.Limits.IsImage.isoExt_hom {C : Type u} {X : C} {Y : C} {f : X Y} (hF : ) (hF' : ) :
(hF.isoExt hF').hom = hF.lift F'
def CategoryTheory.Limits.IsImage.isoExt {C : Type u} {X : C} {Y : C} {f : X Y} (hF : ) (hF' : ) :
F.I F'.I

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

Equations
• hF.isoExt hF' = { hom := hF.lift F', inv := hF'.lift F, hom_inv_id := , inv_hom_id := }
Instances For
theorem CategoryTheory.Limits.IsImage.isoExt_hom_m {C : Type u} {X : C} {Y : C} {f : X Y} (hF : ) (hF' : ) :
CategoryTheory.CategoryStruct.comp (hF.isoExt hF').hom F'.m = F.m
theorem CategoryTheory.Limits.IsImage.isoExt_inv_m {C : Type u} {X : C} {Y : C} {f : X Y} (hF : ) (hF' : ) :
CategoryTheory.CategoryStruct.comp (hF.isoExt hF').inv F.m = F'.m
theorem CategoryTheory.Limits.IsImage.e_isoExt_hom {C : Type u} {X : C} {Y : C} {f : X Y} (hF : ) (hF' : ) :
CategoryTheory.CategoryStruct.comp F.e (hF.isoExt hF').hom = F'.e
theorem CategoryTheory.Limits.IsImage.e_isoExt_inv {C : Type u} {X : C} {Y : C} {f : X Y} (hF : ) (hF' : ) :
CategoryTheory.CategoryStruct.comp F'.e (hF.isoExt hF').inv = F.e
@[simp]
theorem CategoryTheory.Limits.IsImage.ofArrowIso_lift {C : Type u} {f : } {g : } {F : } (hF : ) (sq : f g) [] (F' : ) :
(hF.ofArrowIso sq).lift F' = hF.lift (F'.ofArrowIso )
def CategoryTheory.Limits.IsImage.ofArrowIso {C : Type u} {f : } {g : } {F : } (hF : ) (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
• hF.ofArrowIso sq = { lift := fun (F' : ) => hF.lift (F'.ofArrowIso ), lift_fac := }
Instances For
structure CategoryTheory.Limits.ImageFactorisation {C : Type u} {X : C} {Y : C} (f : X Y) :
Type (max u v)

Data exhibiting that a morphism f has an image.

• Data exhibiting that a morphism f has an image.

• isImage :

Data exhibiting that a morphism f has an image.

Instances For
instance CategoryTheory.Limits.ImageFactorisation.instInhabitedOfMono {C : Type u} {X : C} {Y : C} (f : X Y) :
Equations
• = { default := }
@[simp]
theorem CategoryTheory.Limits.ImageFactorisation.ofArrowIso_isImage {C : Type u} {f : } {g : } (F : ) (sq : f g) [] :
(F.ofArrowIso sq).isImage = F.isImage.ofArrowIso sq
@[simp]
theorem CategoryTheory.Limits.ImageFactorisation.ofArrowIso_F {C : Type u} {f : } {g : } (F : ) (sq : f g) [] :
(F.ofArrowIso sq).F = F.F.ofArrowIso sq
def CategoryTheory.Limits.ImageFactorisation.ofArrowIso {C : Type u} {f : } {g : } (F : ) (sq : f g) [] :

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

Equations
• F.ofArrowIso sq = { F := F.F.ofArrowIso sq, isImage := F.isImage.ofArrowIso sq }
Instances For
class CategoryTheory.Limits.HasImage {C : Type u} {X : C} {Y : C} (f : X Y) :

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

• mk' :: (
• exists_image :

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

• )
Instances
theorem CategoryTheory.Limits.HasImage.exists_image {C : Type u} {X : C} {Y : C} {f : X Y} [self : ] :

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

theorem CategoryTheory.Limits.HasImage.mk {C : Type u} {X : C} {Y : C} {f : X Y} :
theorem CategoryTheory.Limits.HasImage.of_arrow_iso {C : Type u} {f : } {g : } [h : ] (sq : f g) [] :
@[instance 100]
instance CategoryTheory.Limits.mono_hasImage {C : Type u} {X : C} {Y : C} (f : X Y) :
Equations
• =
def CategoryTheory.Limits.Image.monoFactorisation {C : Type u} {X : C} {Y : C} (f : X Y) :

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

Equations
Instances For
def CategoryTheory.Limits.Image.isImage {C : Type u} {X : C} {Y : C} (f : X Y) :

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

Equations
• = .isImage
Instances For
def CategoryTheory.Limits.image {C : Type u} {X : C} {Y : C} (f : X Y) :
C

The categorical image of a morphism.

Equations
Instances For
def CategoryTheory.Limits.image.ι {C : Type u} {X : C} {Y : C} (f : X Y) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.image.as_ι {C : Type u} {X : C} {Y : C} (f : X Y) :
instance CategoryTheory.Limits.instMonoι {C : Type u} {X : C} {Y : C} (f : X Y) :
Equations
• =
def CategoryTheory.Limits.factorThruImage {C : Type u} {X : C} {Y : C} (f : X Y) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.as_factorThruImage {C : Type u} {X : C} {Y : C} (f : X Y) :

Rewrite in terms of the factorThruImage interface.

@[simp]
theorem CategoryTheory.Limits.image.fac_assoc {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (h : Y Z) :
@[simp]
theorem CategoryTheory.Limits.image.fac {C : Type u} {X : C} {Y : C} (f : X Y) :
def CategoryTheory.Limits.image.lift {C : Type u} {X : C} {Y : C} {f : X Y} :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.image.lift_fac_assoc {C : Type u} {X : C} {Y : C} {f : X Y} {Z : C} (h : Y Z) :
@[simp]
theorem CategoryTheory.Limits.image.lift_fac {C : Type u} {X : C} {Y : C} {f : X Y} :
@[simp]
theorem CategoryTheory.Limits.image.fac_lift_assoc {C : Type u} {X : C} {Y : C} {f : X Y} {Z : C} (h : F'.I Z) :
@[simp]
theorem CategoryTheory.Limits.image.fac_lift {C : Type u} {X : C} {Y : C} {f : X Y} :
@[simp]
theorem CategoryTheory.Limits.image.isImage_lift {C : Type u} {X : C} {Y : C} {f : X Y} :
@[simp]
theorem CategoryTheory.Limits.IsImage.lift_ι_assoc {C : Type u} {X : C} {Y : C} {f : X Y} (hF : ) {Z : C} (h : Y Z) :
@[simp]
theorem CategoryTheory.Limits.IsImage.lift_ι {C : Type u} {X : C} {Y : C} {f : X Y} (hF : ) :
instance CategoryTheory.Limits.image.lift_mono {C : Type u} {X : C} {Y : C} {f : X Y} :
Equations
• =
theorem CategoryTheory.Limits.HasImage.uniq {C : Type u} {X : C} {Y : C} {f : X Y} (l : ) (w : ) :
instance CategoryTheory.Limits.instHasImageCompOfIsIso {C : Type u} {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) :

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

Equations
• =

HasImages asserts that every morphism has an image.

• has_image : ∀ {X Y : C} (f : X Y),

HasImages asserts that every morphism has an image.

Instances
theorem CategoryTheory.Limits.HasImages.has_image {C : Type u} [self : ] {X : C} {Y : C} (f : X Y) :

HasImages asserts that every morphism has an image.

def CategoryTheory.Limits.imageMonoIsoSource {C : Type u} {X : C} {Y : C} (f : X Y) :

The image of a monomorphism is isomorphic to the source.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.imageMonoIsoSource_inv_ι_assoc {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (h : Y Z) :
@[simp]
theorem CategoryTheory.Limits.imageMonoIsoSource_inv_ι {C : Type u} {X : C} {Y : C} (f : X Y) :
@[simp]
theorem CategoryTheory.Limits.imageMonoIsoSource_hom_self_assoc {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (h : Y Z) :
@[simp]
theorem CategoryTheory.Limits.imageMonoIsoSource_hom_self {C : Type u} {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.Limits.image.ext {C : Type u} {X : C} {Y : C} (f : X Y) {W : C} {g : } {h : } :
g = h
instance CategoryTheory.Limits.instEpiFactorThruImageOfHasLimitWalkingParallelPairParallelPair {C : Type u} {X : C} {Y : C} (f : X Y) [∀ {Z : C} (g h : ), ] :
Equations
• =
theorem CategoryTheory.Limits.epi_image_of_epi {C : Type u} {X : C} {Y : C} (f : X Y) [E : ] :
theorem CategoryTheory.Limits.epi_of_epi_image {C : Type u} {X : C} {Y : C} (f : X Y) :
def CategoryTheory.Limits.image.eqToHom {C : Type u} {X : C} {Y : C} {f : X Y} {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
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.Limits.instIsIsoEqToHom {C : Type u} {X : C} {Y : C} {f : X Y} {f' : X Y} (h : f = f') :
Equations
• =
def CategoryTheory.Limits.image.eqToIso {C : Type u} {X : C} {Y : C} {f : X Y} {f' : X Y} (h : f = f') :

An equation between morphisms gives an isomorphism between the images.

Equations
Instances For
theorem CategoryTheory.Limits.image.eq_fac {C : Type u} {X : C} {Y : C} {f : X Y} {f' : X Y} (h : f = f') :

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

def CategoryTheory.Limits.image.preComp {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (g : Y Z) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.image.preComp_ι_assoc {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (g : Y Z✝) {Z : C} (h : Z✝ Z) :
@[simp]
theorem CategoryTheory.Limits.image.preComp_ι {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (g : Y Z) :
@[simp]
theorem CategoryTheory.Limits.image.factorThruImage_preComp_assoc {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (g : Y Z✝) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.Limits.image.factorThruImage_preComp {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (g : Y Z) :
instance CategoryTheory.Limits.image.preComp_mono {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (g : Y Z) :

image.preComp f g is a monomorphism.

Equations
• =
theorem CategoryTheory.Limits.image.preComp_comp {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (g : Y Z) {W : C} (h : Z W) :

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.

instance CategoryTheory.Limits.image.preComp_epi_of_epi {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (g : Y Z) :

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

Equations
• =
instance CategoryTheory.Limits.hasImage_iso_comp {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (g : Y Z) :
Equations
• =
instance CategoryTheory.Limits.image.isIso_precomp_iso {C : Type u} {X : C} {Y : C} {Z : C} (g : Y Z) (f : X Y) :

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

Equations
• =
instance CategoryTheory.Limits.hasImage_comp_iso {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (g : Y Z) :
Equations
• =
def CategoryTheory.Limits.image.compIso {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (g : Y Z) :

Postcomposing by an isomorphism induces an isomorphism on the image.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.image.compIso_hom_comp_image_ι_assoc {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (g : Y Z✝) {Z : C} (h : Z✝ Z) :
@[simp]
theorem CategoryTheory.Limits.image.compIso_hom_comp_image_ι {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (g : Y Z) :
@[simp]
theorem CategoryTheory.Limits.image.compIso_inv_comp_image_ι_assoc {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (g : Y Z✝) {Z : C} (h : Y Z) :
@[simp]
theorem CategoryTheory.Limits.image.compIso_inv_comp_image_ι {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (g : Y Z) :
instance CategoryTheory.Limits.instHasImageHomMk {C : Type u} {X : C} {Y : C} (f : X Y) :
Equations
• =
structure CategoryTheory.Limits.ImageMap {C : Type u} {f : } {g : } [] [] (sq : f g) :

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

• map :

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

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

Instances For
@[simp]
theorem CategoryTheory.Limits.ImageMap.map_ι {C : Type u} {f : } {g : } [] [] {sq : f g} (self : ) :

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

Equations
• CategoryTheory.Limits.inhabitedImageMap = { default := { map := , map_ι := } }
@[simp]
theorem CategoryTheory.Limits.ImageMap.map_ι_assoc {C : Type u} {f : } {g : } [] [] {sq : f g} (self : ) {Z : C} (h : g.right Z) :
=
@[simp]
theorem CategoryTheory.Limits.ImageMap.factor_map_assoc {C : Type u} {f : } {g : } [] [] (sq : f g) (m : ) {Z : C} (h : Z) :
@[simp]
theorem CategoryTheory.Limits.ImageMap.factor_map {C : Type u} {f : } {g : } [] [] (sq : f g) (m : ) :
def CategoryTheory.Limits.ImageMap.transport {C : Type u} {f : } {g : } [] [] (sq : f g) (F : ) {F' : } (hF' : ) {map : F.I F'.I} (map_ι : = CategoryTheory.CategoryStruct.comp 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
• One or more equations did not get rendered due to their size.
Instances For
class CategoryTheory.Limits.HasImageMap {C : Type u} {f : } {g : } [] [] (sq : f g) :

HasImageMap sq means that there is an ImageMap for the square sq.

• mk' :: (
• has_image_map :

HasImageMap sq means that there is an ImageMap for the square sq.

• )
Instances
theorem CategoryTheory.Limits.HasImageMap.has_image_map {C : Type u} {f : } {g : } [] [] {sq : f g} [self : ] :

HasImageMap sq means that there is an ImageMap for the square sq.

theorem CategoryTheory.Limits.HasImageMap.mk {C : Type u} {f : } {g : } [] [] {sq : f g} (m : ) :
theorem CategoryTheory.Limits.HasImageMap.transport {C : Type u} {f : } {g : } [] [] (sq : f g) (F : ) {F' : } (hF' : ) (map : F.I F'.I) (map_ι : = CategoryTheory.CategoryStruct.comp F.m sq.right) :
def CategoryTheory.Limits.HasImageMap.imageMap {C : Type u} {f : } {g : } [] [] (sq : f g) :

Obtain an ImageMap from a HasImageMap instance.

Equations
Instances For
@[instance 100]
instance CategoryTheory.Limits.hasImageMapOfIsIso {C : Type u} {f : } {g : } [] [] (sq : f g) [] :
Equations
• =
instance CategoryTheory.Limits.HasImageMap.comp {C : Type u} {f : } {g : } {h : } [] [] [] (sq1 : f g) (sq2 : g h) :
Equations
• =
theorem CategoryTheory.Limits.ImageMap.ext_iff {C : Type u} :
∀ {inst : } {f g : } {inst_1 : } {inst_2 : } {sq : f g} {x y : }, x = y x.map = y.map
theorem CategoryTheory.Limits.ImageMap.ext {C : Type u} :
∀ {inst : } {f g : } {inst_1 : } {inst_2 : } {sq : f g} {x y : }, x.map = y.mapx = y
theorem CategoryTheory.Limits.ImageMap.map_uniq_aux {C : Type u} {f : } {g : } [] [] {sq : f g} (map : ) (map_ι : autoParam ( = CategoryTheory.CategoryStruct.comp sq.right) _auto✝) (map' : ) (map_ι' : = CategoryTheory.CategoryStruct.comp sq.right) :
map = map'
theorem CategoryTheory.Limits.ImageMap.map_uniq {C : Type u} {f : } {g : } [] [] {sq : f g} (F : ) (G : ) :
F.map = G.map
@[simp]
theorem CategoryTheory.Limits.ImageMap.mk.injEq' {C : Type u} {f : } {g : } [] [] {sq : f g} (map : ) (map_ι : autoParam ( = CategoryTheory.CategoryStruct.comp sq.right) _auto✝) (map' : ) (map_ι' : = CategoryTheory.CategoryStruct.comp sq.right) :
(map = map') = True
instance CategoryTheory.Limits.instSubsingletonImageMap {C : Type u} {f : } {g : } [] [] (sq : f g) :
Equations
• =
@[reducible, inline]
abbrev CategoryTheory.Limits.image.map {C : Type u} {f : } {g : } [] [] (sq : f g) :

The map on images induced by a commutative square.

Equations
Instances For
theorem CategoryTheory.Limits.image.factor_map {C : Type u} {f : } {g : } [] [] (sq : f g) :
theorem CategoryTheory.Limits.image.map_ι {C : Type u} {f : } {g : } [] [] (sq : f g) :
theorem CategoryTheory.Limits.image.map_homMk'_ι {C : Type u} {X : C} {Y : C} {P : C} {Q : C} {k : X Y} {l : P Q} {m : X P} {n : Y Q} :
def CategoryTheory.Limits.imageMapComp {C : Type u} {f : } {g : } [] [] (sq : f g) {h : } [] (sq' : g h) :

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

Equations
• = { map := , map_ι := }
Instances For
@[simp]
theorem CategoryTheory.Limits.image.map_comp {C : Type u} {f : } {g : } [] [] (sq : f g) {h : } [] (sq' : g h) :

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

Equations
• = { map := , map_ι := }
Instances For
@[simp]

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

• has_image_map : ∀ {f g : } (st : f g),
Instances
theorem CategoryTheory.Limits.HasImageMaps.has_image_map {C : Type u} [self : ] {f : } {g : } (st : f g) :
@[simp]
theorem CategoryTheory.Limits.im_obj {C : Type u} (f : ) :
CategoryTheory.Limits.im.obj f =
@[simp]
theorem CategoryTheory.Limits.im_map {C : Type u} :
∀ {X Y : } (st : X Y), CategoryTheory.Limits.im.map st =

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
• One or more equations did not get rendered due to their size.
Instances For
structure CategoryTheory.Limits.StrongEpiMonoFactorisation {C : Type u} {X : C} {Y : C} (f : X Y) extends :
Type (max u v)

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

Instances For

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

instance CategoryTheory.Limits.strongEpiMonoFactorisationInhabited {C : Type u} {X : C} {Y : C} (f : X Y) :

Satisfying the inhabited linter

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

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

Equations
• F.toMonoIsImage = { lift := fun (G : ) => .lift, lift_fac := }
Instances For

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

• mk' :: (
• 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
theorem CategoryTheory.Limits.HasStrongEpiMonoFactorisations.has_fac {C : Type u} {X : C} {Y : C} (f : X Y) :

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

@[instance 100]
Equations
• =

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

• strong_factorThruImage : ∀ {X Y : C} (f : X Y),
Instances
theorem CategoryTheory.Limits.HasStrongEpiImages.strong_factorThruImage {C : Type u} [self : ] {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.Limits.strongEpi_of_strongEpiMonoFactorisation {C : Type u} {X : C} {Y : C} {f : X Y} (hF' : ) :

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

@[instance 100]

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

Equations
• =
@[instance 100]

A category with strong epi images has image maps.

Equations
• =
@[instance 100]

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

Equations
• =
def CategoryTheory.Limits.image.isoStrongEpiMono {C : Type u} {X : C} {Y : C} {f : X Y} {I' : C} (e : X I') (m : I' Y) (comm : ) :

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
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.image.isoStrongEpiMono_hom_comp_ι {C : Type u} {X : C} {Y : C} {f : X Y} {I' : C} (e : X I') (m : I' Y) (comm : ) :
@[simp]
theorem CategoryTheory.Limits.image.isoStrongEpiMono_inv_comp_mono {C : Type u} {X : C} {Y : C} {f : X Y} {I' : C} (e : X I') (m : I' Y) (comm : ) :
noncomputable def CategoryTheory.Limits.functorialEpiMonoFactorizationData (C : Type u) :
.FunctorialFactorizationData

A category with strong epi mono factorisations admits functorial epi/mono factorizations.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Functor.hasStrongEpiMonoFactorisations_imp_of_isEquivalence {C : Type u_1} {D : Type u_2} [] [] (F : ) [F.IsEquivalence] :