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} [CategoryTheory.Category.{v, u} C] {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.

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

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

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

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

@[simp]

theorem CategoryTheory.Limits.MonoFactorisation.fac {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X ⟶ Y} (self : CategoryTheory.Limits.MonoFactorisation f) : CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X ⟶ Y} (self : CategoryTheory.Limits.MonoFactorisation f) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp self.e (CategoryTheory.CategoryStruct.comp self.m h) = CategoryTheory.CategoryStruct.comp f h

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

The obvious factorisation of a monomorphism through itself.

Equations

• CategoryTheory.Limits.MonoFactorisation.self f = CategoryTheory.Limits.MonoFactorisation.mk X f (CategoryTheory.CategoryStruct.id X) ⋯

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

Equations

• CategoryTheory.Limits.MonoFactorisation.instInhabitedOfMono f = { default := CategoryTheory.Limits.MonoFactorisation.self f }

theorem CategoryTheory.Limits.MonoFactorisation.ext {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X ⟶ Y} {F : CategoryTheory.Limits.MonoFactorisation f} {F' : CategoryTheory.Limits.MonoFactorisation f} (hI : F.I = F'.I) (hm : F.m = CategoryTheory.CategoryStruct.comp (CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X ⟶ Y} (F : CategoryTheory.Limits.MonoFactorisation f) {Y' : C} (g : Y ⟶ Y') [CategoryTheory.Mono g] : CategoryTheory.Limits.MonoFactorisation (CategoryTheory.CategoryStruct.comp f g)

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

Equations

• F.compMono g = CategoryTheory.Limits.MonoFactorisation.mk F.I (CategoryTheory.CategoryStruct.comp F.m g) F.e ⋯

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• F.ofCompIso = CategoryTheory.Limits.MonoFactorisation.mk F.I (CategoryTheory.CategoryStruct.comp F.m (CategoryTheory.inv g)) F.e ⋯

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• F.isoComp g = CategoryTheory.Limits.MonoFactorisation.mk F.I F.m (CategoryTheory.CategoryStruct.comp g F.e) ⋯

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.Limits.MonoFactorisation.ofIsoComp g F = CategoryTheory.Limits.MonoFactorisation.mk F.I F.m (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv g) F.e) ⋯

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• F.ofArrowIso sq = CategoryTheory.Limits.MonoFactorisation.mk F.I (CategoryTheory.CategoryStruct.comp F.m sq.right) (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv sq.left) F.e) ⋯

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

The trivial factorisation of a monomorphism satisfies the universal property.

Equations

• CategoryTheory.Limits.IsImage.self f = { lift := fun (F' : CategoryTheory.Limits.MonoFactorisation f) => F'.e, lift_fac := ⋯ }

@[simp]

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

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

Equations

• CategoryTheory.Limits.IsImage.instInhabitedSelf f = { default := CategoryTheory.Limits.IsImage.self f }

def CategoryTheory.Limits.IsImage.isoExt {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X ⟶ Y} {F : CategoryTheory.Limits.MonoFactorisation f} {F' : CategoryTheory.Limits.MonoFactorisation f} (hF : CategoryTheory.Limits.IsImage F) (hF' : CategoryTheory.Limits.IsImage F') : 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 := ⋯ }

@[simp]

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

@[simp]

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

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

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

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

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

def CategoryTheory.Limits.IsImage.ofArrowIso {C : Type u} [CategoryTheory.Category.{v, u} C] {f : CategoryTheory.Arrow C} {g : CategoryTheory.Arrow C} {F : CategoryTheory.Limits.MonoFactorisation f.hom} (hF : CategoryTheory.Limits.IsImage F) (sq : f ⟶ g) [CategoryTheory.IsIso sq] : CategoryTheory.Limits.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

Equations

• hF.ofArrowIso sq = { lift := fun (F' : CategoryTheory.Limits.MonoFactorisation g.hom) => hF.lift (F'.ofArrowIso (CategoryTheory.inv sq)), lift_fac := ⋯ }

@[simp]

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

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

Data exhibiting that a morphism f has an image.

• F : CategoryTheory.Limits.MonoFactorisation f

  Data exhibiting that a morphism f has an image.

• isImage : CategoryTheory.Limits.IsImage self.F

  Data exhibiting that a morphism f has an image.

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

Equations

• CategoryTheory.Limits.ImageFactorisation.instInhabitedOfMono f = { default := { F := CategoryTheory.Limits.MonoFactorisation.self f, isImage := CategoryTheory.Limits.IsImage.self f } }

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

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 }

@[simp]

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

@[simp]

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

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

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

• mk' :: (
• exists_image : Nonempty (CategoryTheory.Limits.ImageFactorisation f)

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

• )

theorem CategoryTheory.Limits.HasImage.exists_image {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} {X Y : C} {f : X ⟶ Y} [self : CategoryTheory.Limits.HasImage f], Nonempty (CategoryTheory.Limits.ImageFactorisation f)

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

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

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

@[instance 100]

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

Equations

• ⋯ = ⋯

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

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

Equations

• CategoryTheory.Limits.Image.monoFactorisation f = (Classical.choice ⋯).F

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

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

Equations

• CategoryTheory.Limits.Image.isImage f = (Classical.choice ⋯).isImage

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

The categorical image of a morphism.

Equations

• CategoryTheory.Limits.image f = (CategoryTheory.Limits.Image.monoFactorisation f).I

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

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

Equations

• CategoryTheory.Limits.image.ι f = (CategoryTheory.Limits.Image.monoFactorisation f).m

@[simp]

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

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

Equations

• ⋯ = ⋯

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

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

Equations

• CategoryTheory.Limits.factorThruImage f = (CategoryTheory.Limits.Image.monoFactorisation f).e

@[simp]

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

Rewrite in terms of the factorThruImage interface.

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.Limits.image.lift F' = (CategoryTheory.Limits.Image.isImage f).lift F'

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

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

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

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

Equations

• ⋯ = ⋯

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

HasImages asserts that every morphism has an image.

• has_image : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasImage f

  HasImages asserts that every morphism has an image.

theorem CategoryTheory.Limits.HasImages.has_image {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Limits.HasImages C] {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasImage f

HasImages asserts that every morphism has an image.

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

The image of a monomorphism is isomorphic to the source.

Equations

• CategoryTheory.Limits.imageMonoIsoSource f = (CategoryTheory.Limits.Image.isImage f).isoExt (CategoryTheory.Limits.IsImage.self f)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• ⋯ = ⋯

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

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

def CategoryTheory.Limits.image.eqToHom {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X ⟶ Y} {f' : X ⟶ Y} [CategoryTheory.Limits.HasImage f] [CategoryTheory.Limits.HasImage f'] (h : f = f') : CategoryTheory.Limits.image f ⟶ CategoryTheory.Limits.image 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.

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

Equations

• ⋯ = ⋯

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

An equation between morphisms gives an isomorphism between the images.

Equations

• CategoryTheory.Limits.image.eqToIso h = CategoryTheory.asIso (CategoryTheory.Limits.image.eqToHom h)

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

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

image.preComp f g is a monomorphism.

Equations

• ⋯ = ⋯

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

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} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [CategoryTheory.IsIso f] [CategoryTheory.Limits.HasImage g] : CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)

Equations

• ⋯ = ⋯

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

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} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [CategoryTheory.Limits.HasImage f] [CategoryTheory.IsIso g] : CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)

Equations

• ⋯ = ⋯

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

Postcomposing by an isomorphism induces an isomorphism on the image.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

structure CategoryTheory.Limits.ImageMap {C : Type u} [CategoryTheory.Category.{v, u} C] {f : CategoryTheory.Arrow C} {g : CategoryTheory.Arrow C} [CategoryTheory.Limits.HasImage f.hom] [CategoryTheory.Limits.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 : CategoryTheory.Limits.image f.hom ⟶ CategoryTheory.Limits.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_ι : CategoryTheory.CategoryStruct.comp self.map (CategoryTheory.Limits.image.ι g.hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.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.

@[simp]

theorem CategoryTheory.Limits.ImageMap.map_ι {C : Type u} [CategoryTheory.Category.{v, u} C] {f : CategoryTheory.Arrow C} {g : CategoryTheory.Arrow C} [CategoryTheory.Limits.HasImage f.hom] [CategoryTheory.Limits.HasImage g.hom] {sq : f ⟶ g} (self : CategoryTheory.Limits.ImageMap sq) : CategoryTheory.CategoryStruct.comp self.map (CategoryTheory.Limits.image.ι g.hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {f : CategoryTheory.Arrow C} [CategoryTheory.Limits.HasImage f.hom] : Inhabited (CategoryTheory.Limits.ImageMap (CategoryTheory.CategoryStruct.id f))

Equations

• CategoryTheory.Limits.inhabitedImageMap = { default := { map := CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.image f.hom), map_ι := ⋯ } }

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.ImageMap.transport {C : Type u} [CategoryTheory.Category.{v, u} C] {f : CategoryTheory.Arrow C} {g : CategoryTheory.Arrow C} [CategoryTheory.Limits.HasImage f.hom] [CategoryTheory.Limits.HasImage g.hom] (sq : f ⟶ g) (F : CategoryTheory.Limits.MonoFactorisation f.hom) {F' : CategoryTheory.Limits.MonoFactorisation g.hom} (hF' : CategoryTheory.Limits.IsImage F') {map : F.I ⟶ F'.I} (map_ι : CategoryTheory.CategoryStruct.comp map F'.m = CategoryTheory.CategoryStruct.comp F.m sq.right) : CategoryTheory.Limits.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.

Equations

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

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

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

• mk' :: (
• has_image_map : Nonempty (CategoryTheory.Limits.ImageMap sq)

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

• )

theorem CategoryTheory.Limits.HasImageMap.has_image_map {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} {f g : CategoryTheory.Arrow C} {inst_1 : CategoryTheory.Limits.HasImage f.hom} {inst_2 : CategoryTheory.Limits.HasImage g.hom} {sq : f ⟶ g} [self : CategoryTheory.Limits.HasImageMap sq], Nonempty (CategoryTheory.Limits.ImageMap sq)

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

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

theorem CategoryTheory.Limits.HasImageMap.transport {C : Type u} [CategoryTheory.Category.{v, u} C] {f : CategoryTheory.Arrow C} {g : CategoryTheory.Arrow C} [CategoryTheory.Limits.HasImage f.hom] [CategoryTheory.Limits.HasImage g.hom] (sq : f ⟶ g) (F : CategoryTheory.Limits.MonoFactorisation f.hom) {F' : CategoryTheory.Limits.MonoFactorisation g.hom} (hF' : CategoryTheory.Limits.IsImage F') (map : F.I ⟶ F'.I) (map_ι : CategoryTheory.CategoryStruct.comp map F'.m = CategoryTheory.CategoryStruct.comp F.m sq.right) : CategoryTheory.Limits.HasImageMap sq

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

Obtain an ImageMap from a HasImageMap instance.

Equations

• CategoryTheory.Limits.HasImageMap.imageMap sq = Classical.choice ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

instance CategoryTheory.Limits.HasImageMap.comp {C : Type u} [CategoryTheory.Category.{v, u} C] {f : CategoryTheory.Arrow C} {g : CategoryTheory.Arrow C} {h : CategoryTheory.Arrow C} [CategoryTheory.Limits.HasImage f.hom] [CategoryTheory.Limits.HasImage g.hom] [CategoryTheory.Limits.HasImage h.hom] (sq1 : f ⟶ g) (sq2 : g ⟶ h) [CategoryTheory.Limits.HasImageMap sq1] [CategoryTheory.Limits.HasImageMap sq2] : CategoryTheory.Limits.HasImageMap (CategoryTheory.CategoryStruct.comp sq1 sq2)

Equations

• ⋯ = ⋯

theorem CategoryTheory.Limits.ImageMap.ext {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} {f g : CategoryTheory.Arrow C} {inst_1 : CategoryTheory.Limits.HasImage f.hom} {inst_2 : CategoryTheory.Limits.HasImage g.hom} {sq : f ⟶ g} {x y : CategoryTheory.Limits.ImageMap sq}, x.map = y.map → x = y

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

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

@[simp]

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

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

Equations

• ⋯ = ⋯

@[reducible, inline]

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

The map on images induced by a commutative square.

Equations

• CategoryTheory.Limits.image.map sq = (CategoryTheory.Limits.HasImageMap.imageMap sq).map

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

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

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

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

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

Equations

• CategoryTheory.Limits.imageMapComp sq sq' = { map := CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.map sq) (CategoryTheory.Limits.image.map sq'), map_ι := ⋯ }

@[simp]

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

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

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

Equations

• CategoryTheory.Limits.imageMapId f = { map := CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.image f.hom), map_ι := ⋯ }

@[simp]

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

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

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

• has_image_map : ∀ {f g : CategoryTheory.Arrow C} (st : f ⟶ g), CategoryTheory.Limits.HasImageMap st

theorem CategoryTheory.Limits.HasImageMaps.has_image_map {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasImages C} [self : CategoryTheory.Limits.HasImageMaps C] {f g : CategoryTheory.Arrow C} (st : f ⟶ g), CategoryTheory.Limits.HasImageMap st

def CategoryTheory.Limits.im {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasImageMaps C] : CategoryTheory.Functor (CategoryTheory.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.

Equations

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

@[simp]

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

@[simp]

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

structure CategoryTheory.Limits.StrongEpiMonoFactorisation {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ⟶ Y) extends CategoryTheory.Limits.MonoFactorisation : 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 : CategoryTheory.Mono self.m
• e : X ⟶ self.I
• fac : CategoryTheory.CategoryStruct.comp self.e self.m = f
• e_strong_epi : CategoryTheory.StrongEpi self.e

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

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

Satisfying the inhabited linter

Equations

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

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

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

Equations

• F.toMonoIsImage = { lift := fun (G : CategoryTheory.Limits.MonoFactorisation f) => ⋯.lift, lift_fac := ⋯ }

class CategoryTheory.Limits.HasStrongEpiMonoFactorisations (C : Type u) [CategoryTheory.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 (CategoryTheory.Limits.StrongEpiMonoFactorisation f)

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

• )

theorem CategoryTheory.Limits.HasStrongEpiMonoFactorisations.has_fac {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Limits.HasStrongEpiMonoFactorisations C] {X Y : C} (f : X ⟶ Y), Nonempty (CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] (d : {X Y : C} → (f : X ⟶ Y) → CategoryTheory.Limits.StrongEpiMonoFactorisation f) : CategoryTheory.Limits.HasStrongEpiMonoFactorisations C

@[instance 100]

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

Equations

• ⋯ = ⋯

class CategoryTheory.Limits.HasStrongEpiImages (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.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), CategoryTheory.StrongEpi (CategoryTheory.Limits.factorThruImage f)

theorem CategoryTheory.Limits.HasStrongEpiImages.strong_factorThruImage {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasImages C} [self : CategoryTheory.Limits.HasStrongEpiImages C] {X Y : C} (f : X ⟶ Y), CategoryTheory.StrongEpi (CategoryTheory.Limits.factorThruImage f)

theorem CategoryTheory.Limits.strongEpi_of_strongEpiMonoFactorisation {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X ⟶ Y} (F : CategoryTheory.Limits.StrongEpiMonoFactorisation f) {F' : CategoryTheory.Limits.MonoFactorisation f} (hF' : CategoryTheory.Limits.IsImage F') : CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X ⟶ Y} [CategoryTheory.Limits.HasImage f] (F : CategoryTheory.Limits.StrongEpiMonoFactorisation f) : CategoryTheory.StrongEpi (CategoryTheory.Limits.factorThruImage f)

@[instance 100]

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

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

Equations

• ⋯ = ⋯

@[instance 100]

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

A category with strong epi images has image maps.

Equations

• ⋯ = ⋯

@[instance 100]

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

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

Equations

• ⋯ = ⋯

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

Equations

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

@[simp]

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

@[simp]

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

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

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.

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