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 work in the group theory and ring theory libraries.

structure CategoryTheory.Limits.MonoFactorisation {C : Type u} [Category.{v, u} C] {X 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 : 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.

• fac : CategoryStruct.comp self.e self.m = f

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

@[simp]

theorem CategoryTheory.Limits.MonoFactorisation.fac_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (self : MonoFactorisation f) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp self.e (CategoryStruct.comp self.m h) = CategoryStruct.comp f h

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

def CategoryTheory.Limits.MonoFactorisation.self {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Mono f] : MonoFactorisation f

The obvious factorisation of a monomorphism through itself.

instance CategoryTheory.Limits.MonoFactorisation.instInhabitedOfMono {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Mono f] : Inhabited (MonoFactorisation f)

theorem CategoryTheory.Limits.MonoFactorisation.ext {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F F' : MonoFactorisation f} (hI : F.I = F'.I) (hm : F.m = CategoryStruct.comp (eqToHom hI) F'.m) : F = F'

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

def CategoryTheory.Limits.MonoFactorisation.compMono {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : MonoFactorisation f) {Y' : C} (g : Y ⟶ Y') [Mono g] : MonoFactorisation (CategoryStruct.comp f g)

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

@[simp]

theorem CategoryTheory.Limits.MonoFactorisation.compMono_e {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : MonoFactorisation f) {Y' : C} (g : Y ⟶ Y') [Mono g] : (F.compMono g).e = F.e

@[simp]

theorem CategoryTheory.Limits.MonoFactorisation.compMono_m {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : MonoFactorisation f) {Y' : C} (g : Y ⟶ Y') [Mono g] : (F.compMono g).m = CategoryStruct.comp F.m g

@[simp]

theorem CategoryTheory.Limits.MonoFactorisation.compMono_I {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : MonoFactorisation f) {Y' : C} (g : Y ⟶ Y') [Mono g] : (F.compMono g).I = F.I

def CategoryTheory.Limits.MonoFactorisation.ofCompIso {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {Y' : C} {g : Y ⟶ Y'} [IsIso g] (F : MonoFactorisation (CategoryStruct.comp f g)) : MonoFactorisation f

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

@[simp]

theorem CategoryTheory.Limits.MonoFactorisation.ofCompIso_m {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {Y' : C} {g : Y ⟶ Y'} [IsIso g] (F : MonoFactorisation (CategoryStruct.comp f g)) : F.ofCompIso.m = CategoryStruct.comp F.m (inv g)

@[simp]

theorem CategoryTheory.Limits.MonoFactorisation.ofCompIso_I {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {Y' : C} {g : Y ⟶ Y'} [IsIso g] (F : MonoFactorisation (CategoryStruct.comp f g)) : F.ofCompIso.I = F.I

@[simp]

theorem CategoryTheory.Limits.MonoFactorisation.ofCompIso_e {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {Y' : C} {g : Y ⟶ Y'} [IsIso g] (F : MonoFactorisation (CategoryStruct.comp f g)) : F.ofCompIso.e = F.e

def CategoryTheory.Limits.MonoFactorisation.isoComp {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : MonoFactorisation f) {X' : C} (g : X' ⟶ X) : MonoFactorisation (CategoryStruct.comp g f)

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

@[simp]

theorem CategoryTheory.Limits.MonoFactorisation.isoComp_I {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : MonoFactorisation f) {X' : C} (g : X' ⟶ X) : (F.isoComp g).I = F.I

@[simp]

theorem CategoryTheory.Limits.MonoFactorisation.isoComp_m {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : MonoFactorisation f) {X' : C} (g : X' ⟶ X) : (F.isoComp g).m = F.m

@[simp]

theorem CategoryTheory.Limits.MonoFactorisation.isoComp_e {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : MonoFactorisation f) {X' : C} (g : X' ⟶ X) : (F.isoComp g).e = CategoryStruct.comp g F.e

def CategoryTheory.Limits.MonoFactorisation.ofIsoComp {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {X' : C} (g : X' ⟶ X) [IsIso g] (F : MonoFactorisation (CategoryStruct.comp g f)) : MonoFactorisation f

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

@[simp]

theorem CategoryTheory.Limits.MonoFactorisation.ofIsoComp_m {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {X' : C} (g : X' ⟶ X) [IsIso g] (F : MonoFactorisation (CategoryStruct.comp g f)) : (ofIsoComp g F).m = F.m

@[simp]

theorem CategoryTheory.Limits.MonoFactorisation.ofIsoComp_I {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {X' : C} (g : X' ⟶ X) [IsIso g] (F : MonoFactorisation (CategoryStruct.comp g f)) : (ofIsoComp g F).I = F.I

@[simp]

theorem CategoryTheory.Limits.MonoFactorisation.ofIsoComp_e {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {X' : C} (g : X' ⟶ X) [IsIso g] (F : MonoFactorisation (CategoryStruct.comp g f)) : (ofIsoComp g F).e = CategoryStruct.comp (inv g) F.e

def CategoryTheory.Limits.MonoFactorisation.ofArrowIso {C : Type u} [Category.{v, u} C] {f g : Arrow C} (F : MonoFactorisation f.hom) (sq : f ⟶ g) [IsIso sq] : MonoFactorisation g.hom

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

@[simp]

theorem CategoryTheory.Limits.MonoFactorisation.ofArrowIso_m {C : Type u} [Category.{v, u} C] {f g : Arrow C} (F : MonoFactorisation f.hom) (sq : f ⟶ g) [IsIso sq] : (F.ofArrowIso sq).m = CategoryStruct.comp F.m sq.right

@[simp]

theorem CategoryTheory.Limits.MonoFactorisation.ofArrowIso_e {C : Type u} [Category.{v, u} C] {f g : Arrow C} (F : MonoFactorisation f.hom) (sq : f ⟶ g) [IsIso sq] : (F.ofArrowIso sq).e = CategoryStruct.comp (inv sq.left) F.e

@[simp]

theorem CategoryTheory.Limits.MonoFactorisation.ofArrowIso_I {C : Type u} [Category.{v, u} C] {f g : Arrow C} (F : MonoFactorisation f.hom) (sq : f ⟶ g) [IsIso sq] : (F.ofArrowIso sq).I = F.I

def CategoryTheory.Limits.MonoFactorisation.ofIsoI {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : MonoFactorisation f) {I' : C} (e : F.I ≅ I') : MonoFactorisation f

Given a mono factorisation X ⟶ I ⟶ Y of an arrow f, an isomorphism I ≅ I' gives a new mono factorisation X ⟶ I' ⟶ Y of f.

@[simp]

theorem CategoryTheory.Limits.MonoFactorisation.ofIsoI_I {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : MonoFactorisation f) {I' : C} (e : F.I ≅ I') : (F.ofIsoI e).I = I'

@[simp]

theorem CategoryTheory.Limits.MonoFactorisation.ofIsoI_e {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : MonoFactorisation f) {I' : C} (e : F.I ≅ I') : (F.ofIsoI e).e = CategoryStruct.comp F.e e.hom

@[simp]

theorem CategoryTheory.Limits.MonoFactorisation.ofIsoI_m {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : MonoFactorisation f) {I' : C} (e : F.I ≅ I') : (F.ofIsoI e).m = CategoryStruct.comp e.inv F.m

def CategoryTheory.Limits.MonoFactorisation.copy {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : MonoFactorisation f) (m : F.I ⟶ Y) (e : X ⟶ F.I) (hm : m = F.m := by cat_disch) (he : e = F.e := by cat_disch) : MonoFactorisation f

Copying a mono factorisation to another mono factorisation with propositionally equal m and e fields.

@[simp]

theorem CategoryTheory.Limits.MonoFactorisation.copy_e {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : MonoFactorisation f) (m : F.I ⟶ Y) (e : X ⟶ F.I) (hm : m = F.m := by cat_disch) (he : e = F.e := by cat_disch) : (F.copy m e hm he).e = e

@[simp]

theorem CategoryTheory.Limits.MonoFactorisation.copy_m {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : MonoFactorisation f) (m : F.I ⟶ Y) (e : X ⟶ F.I) (hm : m = F.m := by cat_disch) (he : e = F.e := by cat_disch) : (F.copy m e hm he).m = m

@[simp]

theorem CategoryTheory.Limits.MonoFactorisation.copy_I {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : MonoFactorisation f) (m : F.I ⟶ Y) (e : X ⟶ F.I) (hm : m = F.m := by cat_disch) (he : e = F.e := by cat_disch) : (F.copy m e hm he).I = F.I

@[simp]

theorem CategoryTheory.Limits.MonoFactorisation.fac_apply {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} {f : F ⟶ G} {X : C} (H : MonoFactorisation f) (x : F.obj X) : H.m.app X (H.e.app X x) = f.app X x

structure CategoryTheory.Limits.IsImage {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : MonoFactorisation f) : Type (max u v)

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

• lift (F' : MonoFactorisation f) : F.I ⟶ F'.I

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

• lift_fac (F' : MonoFactorisation f) : 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} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F : MonoFactorisation f} (self : IsImage F) (F' : MonoFactorisation f) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (self.lift F') (CategoryStruct.comp F'.m h) = CategoryStruct.comp F.m h

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

@[simp]

theorem CategoryTheory.Limits.IsImage.fac_lift {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F : MonoFactorisation f} (hF : IsImage F) (F' : MonoFactorisation f) : CategoryStruct.comp F.e (hF.lift F') = F'.e

@[simp]

theorem CategoryTheory.Limits.IsImage.fac_lift_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F : MonoFactorisation f} (hF : IsImage F) (F' : MonoFactorisation f) {Z : C} (h : F'.I ⟶ Z) : CategoryStruct.comp F.e (CategoryStruct.comp (hF.lift F') h) = CategoryStruct.comp F'.e h

def CategoryTheory.Limits.IsImage.self {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Mono f] : IsImage (MonoFactorisation.self f)

The trivial factorisation of a monomorphism satisfies the universal property.

@[simp]

theorem CategoryTheory.Limits.IsImage.self_lift {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Mono f] (F' : MonoFactorisation f) : (self f).lift F' = F'.e

instance CategoryTheory.Limits.IsImage.instInhabitedSelf {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Mono f] : Inhabited (IsImage (MonoFactorisation.self f))

def CategoryTheory.Limits.IsImage.isoExt {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F F' : MonoFactorisation f} (hF : IsImage F) (hF' : IsImage F') : F.I ≅ F'.I

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

@[simp]

theorem CategoryTheory.Limits.IsImage.isoExt_inv {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F F' : MonoFactorisation f} (hF : IsImage F) (hF' : IsImage F') : (hF.isoExt hF').inv = hF'.lift F

@[simp]

theorem CategoryTheory.Limits.IsImage.isoExt_hom {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F F' : MonoFactorisation f} (hF : IsImage F) (hF' : IsImage F') : (hF.isoExt hF').hom = hF.lift F'

theorem CategoryTheory.Limits.IsImage.isoExt_hom_m {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F F' : MonoFactorisation f} (hF : IsImage F) (hF' : IsImage F') : CategoryStruct.comp (hF.isoExt hF').hom F'.m = F.m

theorem CategoryTheory.Limits.IsImage.isoExt_inv_m {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F F' : MonoFactorisation f} (hF : IsImage F) (hF' : IsImage F') : CategoryStruct.comp (hF.isoExt hF').inv F.m = F'.m

theorem CategoryTheory.Limits.IsImage.e_isoExt_hom {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F F' : MonoFactorisation f} (hF : IsImage F) (hF' : IsImage F') : CategoryStruct.comp F.e (hF.isoExt hF').hom = F'.e

theorem CategoryTheory.Limits.IsImage.e_isoExt_inv {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F F' : MonoFactorisation f} (hF : IsImage F) (hF' : IsImage F') : CategoryStruct.comp F'.e (hF.isoExt hF').inv = F.e

def CategoryTheory.Limits.IsImage.ofArrowIso {C : Type u} [Category.{v, u} C] {f g : Arrow C} {F : MonoFactorisation f.hom} (hF : IsImage F) (sq : f ⟶ g) [IsIso sq] : IsImage (F.ofArrowIso sq)

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

@[simp]

theorem CategoryTheory.Limits.IsImage.ofArrowIso_lift {C : Type u} [Category.{v, u} C] {f g : Arrow C} {F : MonoFactorisation f.hom} (hF : IsImage F) (sq : f ⟶ g) [IsIso sq] (F' : MonoFactorisation g.hom) : (hF.ofArrowIso sq).lift F' = hF.lift (F'.ofArrowIso (inv sq))

def CategoryTheory.Limits.IsImage.ofIsoI {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F : MonoFactorisation f} (hF : IsImage F) {I' : C} (e : F.I ≅ I') : IsImage (F.ofIsoI e)

Given a mono factorisation X ⟶ I ⟶ Y of an arrow f that is an image and an isomorphism I ≅ I', the induced mono factorisation by the isomorphism is also an image.

@[simp]

theorem CategoryTheory.Limits.IsImage.ofIsoI_lift {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F : MonoFactorisation f} (hF : IsImage F) {I' : C} (e : F.I ≅ I') (F' : MonoFactorisation f) : (hF.ofIsoI e).lift F' = CategoryStruct.comp e.inv (hF.lift F')

def CategoryTheory.Limits.IsImage.copy {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F : MonoFactorisation f} (hF : IsImage F) (m : F.I ⟶ Y) (e : X ⟶ F.I) (hm : m = F.m := by cat_disch) (he : e = F.e := by cat_disch) : IsImage (F.copy m e ⋯ ⋯)

Copying a mono factorisation to another mono factorisation with propositionally equal fields preserves the property of being an image. This is useful when one needs precise control of the m and e fields.

@[simp]

theorem CategoryTheory.Limits.IsImage.copy_lift {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F : MonoFactorisation f} (hF : IsImage F) (m : F.I ⟶ Y) (e : X ⟶ F.I) (hm : m = F.m := by cat_disch) (he : e = F.e := by cat_disch) (F' : MonoFactorisation f) : (hF.copy m e hm he).lift F' = hF.lift F'

structure CategoryTheory.Limits.ImageFactorisation {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : Type (max u v)

Data exhibiting that a morphism f has an image.

• F : MonoFactorisation f

  Data exhibiting that a morphism f has an image.

• isImage : IsImage self.F

  Data exhibiting that a morphism f has an image.

instance CategoryTheory.Limits.ImageFactorisation.instInhabitedOfMono {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Mono f] : Inhabited (ImageFactorisation f)

def CategoryTheory.Limits.ImageFactorisation.ofArrowIso {C : Type u} [Category.{v, u} C] {f g : Arrow C} (F : ImageFactorisation f.hom) (sq : f ⟶ g) [IsIso sq] : ImageFactorisation g.hom

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

@[simp]

theorem CategoryTheory.Limits.ImageFactorisation.ofArrowIso_F {C : Type u} [Category.{v, u} C] {f g : Arrow C} (F : ImageFactorisation f.hom) (sq : f ⟶ g) [IsIso sq] : (F.ofArrowIso sq).F = F.F.ofArrowIso sq

@[simp]

theorem CategoryTheory.Limits.ImageFactorisation.ofArrowIso_isImage {C : Type u} [Category.{v, u} C] {f g : Arrow C} (F : ImageFactorisation f.hom) (sq : f ⟶ g) [IsIso sq] : (F.ofArrowIso sq).isImage = F.isImage.ofArrowIso sq

def CategoryTheory.Limits.ImageFactorisation.ofIsoI {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : ImageFactorisation f) {I' : C} (e : F.F.I ≅ I') : ImageFactorisation f

Given an image factorisation X ⟶ I ⟶ Y of an arrow f, an isomorphism I ≅ I' induces a new image factorisation X ⟶ I' ⟶ Y of f.

@[simp]

theorem CategoryTheory.Limits.ImageFactorisation.ofIsoI_isImage {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : ImageFactorisation f) {I' : C} (e : F.F.I ≅ I') : (F.ofIsoI e).isImage = F.isImage.ofIsoI e

@[simp]

theorem CategoryTheory.Limits.ImageFactorisation.ofIsoI_F {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : ImageFactorisation f) {I' : C} (e : F.F.I ≅ I') : (F.ofIsoI e).F = F.F.ofIsoI e

def CategoryTheory.Limits.ImageFactorisation.copy {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : ImageFactorisation f) (m : F.F.I ⟶ Y) (e : X ⟶ F.F.I) (hm : m = F.F.m := by cat_disch) (he : e = F.F.e := by cat_disch) : ImageFactorisation f

Copying an image factorisation to another image factorisation with propositionally equal m and e fields.

@[simp]

theorem CategoryTheory.Limits.ImageFactorisation.copy_isImage {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : ImageFactorisation f) (m : F.F.I ⟶ Y) (e : X ⟶ F.F.I) (hm : m = F.F.m := by cat_disch) (he : e = F.F.e := by cat_disch) : (F.copy m e hm he).isImage = F.isImage.copy m e ⋯ ⋯

@[simp]

theorem CategoryTheory.Limits.ImageFactorisation.copy_F {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : ImageFactorisation f) (m : F.F.I ⟶ Y) (e : X ⟶ F.F.I) (hm : m = F.F.m := by cat_disch) (he : e = F.F.e := by cat_disch) : (F.copy m e hm he).F = F.F.copy m e ⋯ ⋯

class CategoryTheory.Limits.HasImage {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : Prop

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

• mk' :: (
• exists_image : Nonempty (ImageFactorisation f)

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

• )

theorem CategoryTheory.Limits.HasImage.mk {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : ImageFactorisation f) : HasImage f

theorem CategoryTheory.Limits.HasImage.of_arrow_iso {C : Type u} [Category.{v, u} C] {f g : Arrow C} [h : HasImage f.hom] (sq : f ⟶ g) [IsIso sq] : HasImage g.hom

@[instance 100]

instance CategoryTheory.Limits.mono_hasImage {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Mono f] : HasImage f

def CategoryTheory.Limits.Image.imageFactorisation {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] : ImageFactorisation f

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

def CategoryTheory.Limits.Image.monoFactorisation {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] : MonoFactorisation f

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

def CategoryTheory.Limits.Image.isImage {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] : IsImage (monoFactorisation f)

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

def CategoryTheory.Limits.image {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] : C

The categorical image of a morphism.

def CategoryTheory.Limits.image.ι {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] : image f ⟶ Y

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

@[simp]

theorem CategoryTheory.Limits.image.as_ι {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] : (Image.monoFactorisation f).m = ι f

instance CategoryTheory.Limits.instMonoι {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] : Mono (image.ι f)

def CategoryTheory.Limits.factorThruImage {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] : X ⟶ image f

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

@[simp]

theorem CategoryTheory.Limits.as_factorThruImage {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] : (Image.monoFactorisation f).e = factorThruImage f

Rewrite in terms of the factorThruImage interface.

@[simp]

theorem CategoryTheory.Limits.image.fac {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] : CategoryStruct.comp (factorThruImage f) (ι f) = f

@[simp]

theorem CategoryTheory.Limits.image.fac_assoc {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (factorThruImage f) (CategoryStruct.comp (ι f) h) = CategoryStruct.comp f h

def CategoryTheory.Limits.image.lift {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [HasImage f] (F' : MonoFactorisation f) : image f ⟶ F'.I

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

@[simp]

theorem CategoryTheory.Limits.image.lift_fac {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [HasImage f] (F' : MonoFactorisation f) : CategoryStruct.comp (lift F') F'.m = ι f

@[simp]

theorem CategoryTheory.Limits.image.lift_fac_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [HasImage f] (F' : MonoFactorisation f) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (lift F') (CategoryStruct.comp F'.m h) = CategoryStruct.comp (ι f) h

@[simp]

theorem CategoryTheory.Limits.image.fac_lift {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [HasImage f] (F' : MonoFactorisation f) : CategoryStruct.comp (factorThruImage f) (lift F') = F'.e

@[simp]

theorem CategoryTheory.Limits.image.fac_lift_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [HasImage f] (F' : MonoFactorisation f) {Z : C} (h : F'.I ⟶ Z) : CategoryStruct.comp (factorThruImage f) (CategoryStruct.comp (lift F') h) = CategoryStruct.comp F'.e h

@[simp]

theorem CategoryTheory.Limits.image.isImage_lift {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [HasImage f] (F : MonoFactorisation f) : (Image.isImage f).lift F = lift F

@[simp]

theorem CategoryTheory.Limits.IsImage.lift_ι {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [HasImage f] {F : MonoFactorisation f} (hF : IsImage F) : CategoryStruct.comp (hF.lift (Image.monoFactorisation f)) (image.ι f) = F.m

@[simp]

theorem CategoryTheory.Limits.IsImage.lift_ι_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [HasImage f] {F : MonoFactorisation f} (hF : IsImage F) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (hF.lift (Image.monoFactorisation f)) (CategoryStruct.comp (image.ι f) h) = CategoryStruct.comp F.m h

@[simp]

theorem CategoryTheory.Limits.image.lift_mk_factorThruImage {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [HasImage f] : CategoryStruct.comp (lift { I := image f, m := ι f, m_mono := ⋯, e := factorThruImage f, fac := ⋯ }) (ι f) = ι f

@[simp]

theorem CategoryTheory.Limits.image.lift_mk_factorThruImage_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [HasImage f] {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (lift { I := image f, m := ι f, m_mono := ⋯, e := factorThruImage f, fac := ⋯ }) (CategoryStruct.comp (ι f) h) = CategoryStruct.comp (ι f) h

@[simp]

theorem CategoryTheory.Limits.image.lift_mk_comp {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasImage g] [HasImage (CategoryStruct.comp f g)] (h : Y ⟶ image g) (H : CategoryStruct.comp (CategoryStruct.comp f h) (ι g) = CategoryStruct.comp f g) : CategoryStruct.comp (lift { I := image g, m := ι g, m_mono := ⋯, e := CategoryStruct.comp f h, fac := ⋯ }) (ι g) = ι (CategoryStruct.comp f g)

@[simp]

theorem CategoryTheory.Limits.image.lift_mk_comp_assoc {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasImage g] [HasImage (CategoryStruct.comp f g)] (h : Y ⟶ image g) (H : CategoryStruct.comp (CategoryStruct.comp f h) (ι g) = CategoryStruct.comp f g) {Z✝ : C} (h✝ : Z ⟶ Z✝) : CategoryStruct.comp (lift { I := image g, m := ι g, m_mono := ⋯, e := CategoryStruct.comp f h, fac := ⋯ }) (CategoryStruct.comp (ι g) h✝) = CategoryStruct.comp (ι (CategoryStruct.comp f g)) h✝

instance CategoryTheory.Limits.image.lift_mono {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [HasImage f] (F' : MonoFactorisation f) : Mono (lift F')

theorem CategoryTheory.Limits.HasImage.uniq {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [HasImage f] (F' : MonoFactorisation f) (l : image f ⟶ F'.I) (w : CategoryStruct.comp l F'.m = image.ι f) : l = image.lift F'

instance CategoryTheory.Limits.instHasImageCompOfIsIso {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) [IsIso f] (g : Y ⟶ Z) [HasImage g] : HasImage (CategoryStruct.comp f g)

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

class CategoryTheory.Limits.HasImages (C : Type u) [Category.{v, u} C] : Prop

HasImages asserts that every morphism has an image.

• has_image {X Y : C} (f : X ⟶ Y) : HasImage f

  HasImages asserts that every morphism has an image.

def CategoryTheory.Limits.imageMonoIsoSource {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Mono f] : image f ≅ X

The image of a monomorphism is isomorphic to the source.

@[simp]

theorem CategoryTheory.Limits.imageMonoIsoSource_inv_ι {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Mono f] : CategoryStruct.comp (imageMonoIsoSource f).inv (image.ι f) = f

@[simp]

theorem CategoryTheory.Limits.imageMonoIsoSource_inv_ι_assoc {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Mono f] {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (imageMonoIsoSource f).inv (CategoryStruct.comp (image.ι f) h) = CategoryStruct.comp f h

@[simp]

theorem CategoryTheory.Limits.imageMonoIsoSource_hom_self {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Mono f] : CategoryStruct.comp (imageMonoIsoSource f).hom f = image.ι f

@[simp]

theorem CategoryTheory.Limits.imageMonoIsoSource_hom_self_assoc {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Mono f] {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (imageMonoIsoSource f).hom (CategoryStruct.comp f h) = CategoryStruct.comp (image.ι f) h

theorem CategoryTheory.Limits.image.ext {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] {W : C} {g h : image f ⟶ W} [HasLimit (parallelPair g h)] (w : CategoryStruct.comp (factorThruImage f) g = CategoryStruct.comp (factorThruImage f) h) : g = h

instance CategoryTheory.Limits.instEpiFactorThruImageOfHasLimitWalkingParallelPairParallelPair {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] [∀ {Z : C} (g h : image f ⟶ Z), HasLimit (parallelPair g h)] : Epi (factorThruImage f)

theorem CategoryTheory.Limits.epi_image_of_epi {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] [E : Epi f] : Epi (image.ι f)

theorem CategoryTheory.Limits.epi_of_epi_image {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] [Epi (image.ι f)] [Epi (factorThruImage f)] : Epi f

def CategoryTheory.Limits.image.eqToHom {C : Type u} [Category.{v, u} C] {X Y : C} {f f' : X ⟶ Y} [HasImage f] [HasImage f'] (h : f = f') : image f ⟶ image f'

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

instance CategoryTheory.Limits.instIsIsoEqToHom {C : Type u} [Category.{v, u} C] {X Y : C} {f f' : X ⟶ Y} [HasImage f] [HasImage f'] (h : f = f') : IsIso (image.eqToHom h)

def CategoryTheory.Limits.image.eqToIso {C : Type u} [Category.{v, u} C] {X Y : C} {f f' : X ⟶ Y} [HasImage f] [HasImage f'] (h : f = f') : image f ≅ image f'

An equation between morphisms gives an isomorphism between the images.

theorem CategoryTheory.Limits.image.eq_fac {C : Type u} [Category.{v, u} C] {X Y : C} {f f' : X ⟶ Y} [HasImage f] [HasImage f'] [HasEqualizers C] (h : f = f') : ι f = CategoryStruct.comp (eqToIso h).hom (ι f')

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

def CategoryTheory.Limits.image.preComp {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [HasImage g] [HasImage (CategoryStruct.comp f g)] : image (CategoryStruct.comp f g) ⟶ image g

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

@[simp]

theorem CategoryTheory.Limits.image.preComp_ι {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [HasImage g] [HasImage (CategoryStruct.comp f g)] : CategoryStruct.comp (preComp f g) (ι g) = ι (CategoryStruct.comp f g)

@[simp]

theorem CategoryTheory.Limits.image.preComp_ι_assoc {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [HasImage g] [HasImage (CategoryStruct.comp f g)] {Z✝ : C} (h : Z ⟶ Z✝) : CategoryStruct.comp (preComp f g) (CategoryStruct.comp (ι g) h) = CategoryStruct.comp (ι (CategoryStruct.comp f g)) h

@[simp]

theorem CategoryTheory.Limits.image.factorThruImage_preComp {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [HasImage g] [HasImage (CategoryStruct.comp f g)] : CategoryStruct.comp (factorThruImage (CategoryStruct.comp f g)) (preComp f g) = CategoryStruct.comp f (factorThruImage g)

@[simp]

theorem CategoryTheory.Limits.image.factorThruImage_preComp_assoc {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [HasImage g] [HasImage (CategoryStruct.comp f g)] {Z✝ : C} (h : image g ⟶ Z✝) : CategoryStruct.comp (factorThruImage (CategoryStruct.comp f g)) (CategoryStruct.comp (preComp f g) h) = CategoryStruct.comp f (CategoryStruct.comp (factorThruImage g) h)

instance CategoryTheory.Limits.image.preComp_mono {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [HasImage g] [HasImage (CategoryStruct.comp f g)] : Mono (preComp f g)

image.preComp f g is a monomorphism.

theorem CategoryTheory.Limits.image.preComp_comp {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) {W : C} (h : Z ⟶ W) [HasImage (CategoryStruct.comp g h)] [HasImage (CategoryStruct.comp f (CategoryStruct.comp g h))] [HasImage h] [HasImage (CategoryStruct.comp (CategoryStruct.comp f g) h)] : CategoryStruct.comp (preComp f (CategoryStruct.comp g h)) (preComp g h) = CategoryStruct.comp (eqToHom ⋯) (preComp (CategoryStruct.comp 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.

instance CategoryTheory.Limits.image.preComp_epi_of_epi {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [HasEqualizers C] [HasImage g] [HasImage (CategoryStruct.comp f g)] [Epi f] : Epi (preComp f g)

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

instance CategoryTheory.Limits.hasImage_iso_comp {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [IsIso f] [HasImage g] : HasImage (CategoryStruct.comp f g)

instance CategoryTheory.Limits.image.isIso_precomp_iso {C : Type u} [Category.{v, u} C] {X Y Z : C} (g : Y ⟶ Z) [HasEqualizers C] (f : X ⟶ Y) [IsIso f] [HasImage g] : IsIso (preComp f g)

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

instance CategoryTheory.Limits.hasImage_comp_iso {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [HasImage f] [IsIso g] : HasImage (CategoryStruct.comp f g)

def CategoryTheory.Limits.image.compIso {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [HasEqualizers C] [HasImage f] [IsIso g] : image f ≅ image (CategoryStruct.comp f g)

Postcomposing by an isomorphism induces an isomorphism on the image.

@[simp]

theorem CategoryTheory.Limits.image.compIso_hom_comp_image_ι {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [HasEqualizers C] [HasImage f] [IsIso g] : CategoryStruct.comp (compIso f g).hom (ι (CategoryStruct.comp f g)) = CategoryStruct.comp (ι f) g

@[simp]

theorem CategoryTheory.Limits.image.compIso_hom_comp_image_ι_assoc {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [HasEqualizers C] [HasImage f] [IsIso g] {Z✝ : C} (h : Z ⟶ Z✝) : CategoryStruct.comp (compIso f g).hom (CategoryStruct.comp (ι (CategoryStruct.comp f g)) h) = CategoryStruct.comp (ι f) (CategoryStruct.comp g h)

@[simp]

theorem CategoryTheory.Limits.image.compIso_inv_comp_image_ι {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [HasEqualizers C] [HasImage f] [IsIso g] : CategoryStruct.comp (compIso f g).inv (ι f) = CategoryStruct.comp (ι (CategoryStruct.comp f g)) (inv g)

@[simp]

theorem CategoryTheory.Limits.image.compIso_inv_comp_image_ι_assoc {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [HasEqualizers C] [HasImage f] [IsIso g] {Z✝ : C} (h : Y ⟶ Z✝) : CategoryStruct.comp (compIso f g).inv (CategoryStruct.comp (ι f) h) = CategoryStruct.comp (ι (CategoryStruct.comp f g)) (CategoryStruct.comp (inv g) h)

instance CategoryTheory.Limits.instHasImageHomMk {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] : HasImage (Arrow.mk f).hom

structure CategoryTheory.Limits.ImageMap {C : Type u} [Category.{v, u} C] {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f ⟶ g) : Type v

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

• map : image f.hom ⟶ image g.hom

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

• map_ι : CategoryStruct.comp self.map (image.ι g.hom) = CategoryStruct.comp (image.ι f.hom) sq.right

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

instance CategoryTheory.Limits.inhabitedImageMap {C : Type u} [Category.{v, u} C] {f : Arrow C} [HasImage f.hom] : Inhabited (ImageMap (CategoryStruct.id f))

@[simp]

theorem CategoryTheory.Limits.ImageMap.map_ι_assoc {C : Type u} [Category.{v, u} C] {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] {sq : f ⟶ g} (self : ImageMap sq) {Z : C} (h : g.right ⟶ Z) : CategoryStruct.comp self.map (CategoryStruct.comp (image.ι g.hom) h) = CategoryStruct.comp (image.ι f.hom) (CategoryStruct.comp sq.right h)

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

@[simp]

theorem CategoryTheory.Limits.ImageMap.factor_map {C : Type u} [Category.{v, u} C] {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f ⟶ g) (m : ImageMap sq) : CategoryStruct.comp (factorThruImage f.hom) m.map = CategoryStruct.comp sq.left (factorThruImage g.hom)

@[simp]

theorem CategoryTheory.Limits.ImageMap.factor_map_assoc {C : Type u} [Category.{v, u} C] {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f ⟶ g) (m : ImageMap sq) {Z : C} (h : image g.hom ⟶ Z) : CategoryStruct.comp (factorThruImage f.hom) (CategoryStruct.comp m.map h) = CategoryStruct.comp sq.left (CategoryStruct.comp (factorThruImage g.hom) h)

def CategoryTheory.Limits.ImageMap.transport {C : Type u} [Category.{v, u} C] {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_ι : CategoryStruct.comp map F'.m = CategoryStruct.comp F.m sq.right) : ImageMap sq

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.

class CategoryTheory.Limits.HasImageMap {C : Type u} [Category.{v, u} C] {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f ⟶ g) : Prop

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

• mk' :: (
• has_image_map : Nonempty (ImageMap sq)

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

• )

theorem CategoryTheory.Limits.HasImageMap.mk {C : Type u} [Category.{v, u} C] {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] {sq : f ⟶ g} (m : ImageMap sq) : HasImageMap sq

theorem CategoryTheory.Limits.HasImageMap.transport {C : Type u} [Category.{v, u} C] {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_ι : CategoryStruct.comp map F'.m = CategoryStruct.comp F.m sq.right) : HasImageMap sq

def CategoryTheory.Limits.HasImageMap.imageMap {C : Type u} [Category.{v, u} C] {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f ⟶ g) [HasImageMap sq] : ImageMap sq

Obtain an ImageMap from a HasImageMap instance.

@[instance 100]

instance CategoryTheory.Limits.hasImageMapOfIsIso {C : Type u} [Category.{v, u} C] {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f ⟶ g) [IsIso sq] : HasImageMap sq

instance CategoryTheory.Limits.HasImageMap.comp {C : Type u} [Category.{v, u} C] {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 (CategoryStruct.comp sq1 sq2)

theorem CategoryTheory.Limits.ImageMap.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {f g : Arrow C} {inst✝¹ : HasImage f.hom} {inst✝² : HasImage g.hom} {sq : f ⟶ g} {x y : ImageMap sq} : x = y ↔ x.map = y.map

theorem CategoryTheory.Limits.ImageMap.ext {C : Type u} {inst✝ : Category.{v, u} C} {f g : Arrow C} {inst✝¹ : HasImage f.hom} {inst✝² : HasImage g.hom} {sq : f ⟶ g} {x y : ImageMap sq} (map : x.map = y.map) : x = y

theorem CategoryTheory.Limits.ImageMap.map_uniq_aux {C : Type u} [Category.{v, u} C] {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] {sq : f ⟶ g} (map : image f.hom ⟶ image g.hom) (map_ι : CategoryStruct.comp map (image.ι g.hom) = CategoryStruct.comp (image.ι f.hom) sq.right := by cat_disch) (map' : image f.hom ⟶ image g.hom) (map_ι' : CategoryStruct.comp map' (image.ι g.hom) = CategoryStruct.comp (image.ι f.hom) sq.right) : map = map'

theorem CategoryTheory.Limits.ImageMap.map_uniq {C : Type u} [Category.{v, u} C] {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] {sq : f ⟶ g} (F G : ImageMap sq) : F.map = G.map

@[simp]

theorem CategoryTheory.Limits.ImageMap.mk.injEq' {C : Type u} [Category.{v, u} C] {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] {sq : f ⟶ g} (map : image f.hom ⟶ image g.hom) (map_ι : CategoryStruct.comp map (image.ι g.hom) = CategoryStruct.comp (image.ι f.hom) sq.right := by cat_disch) (map' : image f.hom ⟶ image g.hom) (map_ι' : CategoryStruct.comp map' (image.ι g.hom) = CategoryStruct.comp (image.ι f.hom) sq.right) : (map = map') = True

@[simp]-normal form of ImageMap.mk.injEq.

instance CategoryTheory.Limits.instSubsingletonImageMap {C : Type u} [Category.{v, u} C] {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f ⟶ g) : Subsingleton (ImageMap sq)

@[reducible, inline]

abbrev CategoryTheory.Limits.image.map {C : Type u} [Category.{v, u} C] {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f ⟶ g) [HasImageMap sq] : image f.hom ⟶ image g.hom

The map on images induced by a commutative square.

theorem CategoryTheory.Limits.image.factor_map {C : Type u} [Category.{v, u} C] {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f ⟶ g) [HasImageMap sq] : CategoryStruct.comp (factorThruImage f.hom) (map sq) = CategoryStruct.comp sq.left (factorThruImage g.hom)

theorem CategoryTheory.Limits.image.map_ι {C : Type u} [Category.{v, u} C] {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f ⟶ g) [HasImageMap sq] : CategoryStruct.comp (map sq) (ι g.hom) = CategoryStruct.comp (ι f.hom) sq.right

theorem CategoryTheory.Limits.image.map_homMk'_ι {C : Type u} [Category.{v, u} C] {X Y P Q : C} {k : X ⟶ Y} [HasImage k] {l : P ⟶ Q} [HasImage l] {m : X ⟶ P} {n : Y ⟶ Q} (w : CategoryStruct.comp m l = CategoryStruct.comp k n) [HasImageMap (Arrow.homMk' m n w)] : CategoryStruct.comp (map (Arrow.homMk' m n w)) (ι l) = CategoryStruct.comp (ι k) n

def CategoryTheory.Limits.imageMapComp {C : Type u} [Category.{v, u} C] {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f ⟶ g) [HasImageMap sq] {h : Arrow C} [HasImage h.hom] (sq' : g ⟶ h) [HasImageMap sq'] : ImageMap (CategoryStruct.comp sq sq')

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

@[simp]

theorem CategoryTheory.Limits.image.map_comp {C : Type u} [Category.{v, u} C] {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f ⟶ g) [HasImageMap sq] {h : Arrow C} [HasImage h.hom] (sq' : g ⟶ h) [HasImageMap sq'] [HasImageMap (CategoryStruct.comp sq sq')] : map (CategoryStruct.comp sq sq') = CategoryStruct.comp (map sq) (map sq')

def CategoryTheory.Limits.imageMapId {C : Type u} [Category.{v, u} C] (f : Arrow C) [HasImage f.hom] : ImageMap (CategoryStruct.id f)

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

@[simp]

theorem CategoryTheory.Limits.image.map_id {C : Type u} [Category.{v, u} C] (f : Arrow C) [HasImage f.hom] [HasImageMap (CategoryStruct.id f)] : map (CategoryStruct.id f) = CategoryStruct.id (image f.hom)

class CategoryTheory.Limits.HasImageMaps (C : Type u) [Category.{v, u} C] [HasImages C] : Prop

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

• has_image_map {f g : Arrow C} (st : f ⟶ g) : HasImageMap st

def CategoryTheory.Limits.im {C : Type u} [Category.{v, u} C] [HasImages C] [HasImageMaps C] : Functor (Arrow C) C

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.

@[simp]

theorem CategoryTheory.Limits.im_map {C : Type u} [Category.{v, u} C] [HasImages C] [HasImageMaps C] {X✝ Y✝ : Arrow C} (st : X✝ ⟶ Y✝) : im.map st = image.map st

@[simp]

theorem CategoryTheory.Limits.im_obj {C : Type u} [Category.{v, u} C] [HasImages C] [HasImageMaps C] (f : Arrow C) : im.obj f = image f.hom

structure CategoryTheory.Limits.StrongEpiMonoFactorisation {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) extends CategoryTheory.Limits.MonoFactorisation f : Type (max u v)

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

• I : C
• m : self.I ⟶ Y
• m_mono : Mono self.m
• e : X ⟶ self.I
• fac : CategoryStruct.comp self.e self.m = f
• e_strong_epi : StrongEpi self.e

  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} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [StrongEpi f] : Inhabited (StrongEpiMonoFactorisation f)

Satisfying the inhabited linter

def CategoryTheory.Limits.StrongEpiMonoFactorisation.toMonoIsImage {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : StrongEpiMonoFactorisation f) : IsImage F.toMonoFactorisation

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

class CategoryTheory.Limits.HasStrongEpiMonoFactorisations (C : Type u) [Category.{v, u} C] : Prop

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) : Nonempty (StrongEpiMonoFactorisation f)

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

• )

theorem CategoryTheory.Limits.HasStrongEpiMonoFactorisations.mk {C : Type u} [Category.{v, u} C] (d : {X Y : C} → (f : X ⟶ Y) → StrongEpiMonoFactorisation f) : HasStrongEpiMonoFactorisations C

@[instance 100]

instance CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations {C : Type u} [Category.{v, u} C] [HasStrongEpiMonoFactorisations C] : HasImages C

class CategoryTheory.Limits.HasStrongEpiImages (C : Type u) [Category.{v, u} C] [HasImages C] : Prop

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) : StrongEpi (factorThruImage f)

theorem CategoryTheory.Limits.strongEpi_of_strongEpiMonoFactorisation {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : StrongEpiMonoFactorisation f) {F' : MonoFactorisation f} (hF' : IsImage F') : StrongEpi F'.e

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

theorem CategoryTheory.Limits.strongEpi_factorThruImage_of_strongEpiMonoFactorisation {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [HasImage f] (F : StrongEpiMonoFactorisation f) : StrongEpi (factorThruImage f)

@[instance 100]

instance CategoryTheory.Limits.hasStrongEpiImages_of_hasStrongEpiMonoFactorisations {C : Type u} [Category.{v, u} C] [HasStrongEpiMonoFactorisations C] : HasStrongEpiImages C

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

@[instance 100]

instance CategoryTheory.Limits.hasImageMapsOfHasStrongEpiImages {C : Type u} [Category.{v, u} C] [HasImages C] [HasStrongEpiImages C] : HasImageMaps C

A category with strong epi images has image maps.

@[instance 100]

instance CategoryTheory.Limits.hasStrongEpiImages_of_hasPullbacks_of_hasEqualizers {C : Type u} [Category.{v, u} C] [HasImages C] [HasPullbacks C] [HasEqualizers C] : HasStrongEpiImages C

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

def CategoryTheory.Limits.image.isoStrongEpiMono {C : Type u} [Category.{v, u} C] [HasStrongEpiMonoFactorisations C] {X Y : C} {f : X ⟶ Y} {I' : C} (e : X ⟶ I') (m : I' ⟶ Y) (comm : CategoryStruct.comp e m = f) [StrongEpi e] [Mono m] : I' ≅ image 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.

@[simp]

theorem CategoryTheory.Limits.image.isoStrongEpiMono_hom_comp_ι {C : Type u} [Category.{v, u} C] [HasStrongEpiMonoFactorisations C] {X Y : C} {f : X ⟶ Y} {I' : C} (e : X ⟶ I') (m : I' ⟶ Y) (comm : CategoryStruct.comp e m = f) [StrongEpi e] [Mono m] : CategoryStruct.comp (isoStrongEpiMono e m comm).hom (ι f) = m

@[simp]

theorem CategoryTheory.Limits.image.isoStrongEpiMono_inv_comp_mono {C : Type u} [Category.{v, u} C] [HasStrongEpiMonoFactorisations C] {X Y : C} {f : X ⟶ Y} {I' : C} (e : X ⟶ I') (m : I' ⟶ Y) (comm : CategoryStruct.comp e m = f) [StrongEpi e] [Mono m] : CategoryStruct.comp (isoStrongEpiMono e m comm).inv m = ι f

noncomputable def CategoryTheory.Limits.functorialEpiMonoFactorizationData (C : Type u) [Category.{v, u} C] [HasStrongEpiMonoFactorisations C] : (MorphismProperty.epimorphisms C).FunctorialFactorizationData (MorphismProperty.monomorphisms C)

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

theorem CategoryTheory.Functor.hasStrongEpiMonoFactorisations_imp_of_isEquivalence {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [F.IsEquivalence] [h : Limits.HasStrongEpiMonoFactorisations C] : Limits.HasStrongEpiMonoFactorisations D