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.

source

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

source

@[simp]

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

source

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

source

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

source

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

source

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

source

@[simp]

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

source

@[simp]

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

(F.compMono g).I = F.I

source

@[simp]

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

(F.compMono g).e = F.e

source

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

source

@[simp]

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

source

@[simp]

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

source

@[simp]

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

source

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

source

@[simp]

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

(F.isoComp g).I = F.I

source

@[simp]

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

source

@[simp]

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

(F.isoComp g).m = F.m

source

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

source

@[simp]

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

source

@[simp]

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

source

@[simp]

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

source

def CategoryTheory.Limits.MonoFactorisation.ofArrowIso {C : Type u} [CategoryTheory.Category.{v, u} C] {f 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) ⋯

source

@[simp]

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

(F.ofArrowIso sq).I = F.I

source

@[simp]

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

source

@[simp]

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

source

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

source

@[simp]

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

source

@[simp]

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

source

@[simp]

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

source

def CategoryTheory.Limits.IsImage.self {C : Type u} [CategoryTheory.Category.{v, u} C] {X 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 := ⋯ }

source

@[simp]

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

(CategoryTheory.Limits.IsImage.self f).lift F' = F'.e

source

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

source

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

source

@[simp]

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

(hF.isoExt hF').inv = hF'.lift F

source

@[simp]

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

(hF.isoExt hF').hom = hF.lift F'

source

theorem CategoryTheory.Limits.IsImage.isoExt_hom_m {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {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

source

theorem CategoryTheory.Limits.IsImage.isoExt_inv_m {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {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

source

theorem CategoryTheory.Limits.IsImage.e_isoExt_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {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

source

theorem CategoryTheory.Limits.IsImage.e_isoExt_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {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

source

def CategoryTheory.Limits.IsImage.ofArrowIso {C : Type u} [CategoryTheory.Category.{v, u} C] {f 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 := ⋯ }

source

@[simp]

theorem CategoryTheory.Limits.IsImage.ofArrowIso_lift {C : Type u} [CategoryTheory.Category.{v, u} C] {f 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))

source

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

source

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

source

def CategoryTheory.Limits.ImageFactorisation.ofArrowIso {C : Type u} [CategoryTheory.Category.{v, u} C] {f 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 }

source

@[simp]

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

(F.ofArrowIso sq).F = F.F.ofArrowIso sq

source

@[simp]

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

(F.ofArrowIso sq).isImage = F.isImage.ofArrowIso sq

source

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

)

Instances

source

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

CategoryTheory.Limits.HasImage f

source

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

CategoryTheory.Limits.HasImage g.hom

source

@[instance 100]

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

CategoryTheory.Limits.HasImage f

Equations

⋯ = ⋯

source

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

source

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

source

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

The categorical image of a morphism.

Equations

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

source

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

source

@[simp]

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

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

source

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

CategoryTheory.Mono (CategoryTheory.Limits.image.ι f)

Equations

⋯ = ⋯

source

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

source

@[simp]

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

source

@[simp]

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

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage f) (CategoryTheory.Limits.image.ι f) = f

source

@[simp]

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

source

def CategoryTheory.Limits.image.lift {C : Type u} [CategoryTheory.Category.{v, u} C] {X 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'

source

@[simp]

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

source

@[simp]

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

source

@[simp]

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

source

@[simp]

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

source

@[simp]

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

source

@[simp]

theorem CategoryTheory.Limits.IsImage.lift_ι {C : Type u} [CategoryTheory.Category.{v, u} C] {X 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

source

@[simp]

theorem CategoryTheory.Limits.IsImage.lift_ι_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X 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

source

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

CategoryTheory.Mono (CategoryTheory.Limits.image.lift F')

Equations

⋯ = ⋯

source

theorem CategoryTheory.Limits.HasImage.uniq {C : Type u} [CategoryTheory.Category.{v, u} C] {X 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'

source

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

⋯ = ⋯

source

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.

Instances

source

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

source

@[simp]

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

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageMonoIsoSource f).inv (CategoryTheory.Limits.image.ι f) = f

source

@[simp]

theorem CategoryTheory.Limits.imageMonoIsoSource_inv_ι_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X 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

source

@[simp]

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

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageMonoIsoSource f).hom f = CategoryTheory.Limits.image.ι f

source

@[simp]

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

source

theorem CategoryTheory.Limits.image.ext {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] {W : C} {g 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

source

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

⋯ = ⋯

source

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

CategoryTheory.Epi (CategoryTheory.Limits.image.ι f)

source

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

CategoryTheory.Epi f

source

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

source

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

CategoryTheory.IsIso (CategoryTheory.Limits.image.eqToHom h)

Equations

⋯ = ⋯

source

def CategoryTheory.Limits.image.eqToIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f 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)

source

theorem CategoryTheory.Limits.image.eq_fac {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f 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.

source

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

source

@[simp]

theorem CategoryTheory.Limits.image.preComp_ι {C : Type u} [CategoryTheory.Category.{v, u} C] {X 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)

source

@[simp]

theorem CategoryTheory.Limits.image.preComp_ι_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X 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

source

@[simp]

theorem CategoryTheory.Limits.image.factorThruImage_preComp {C : Type u} [CategoryTheory.Category.{v, u} C] {X 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)

source

@[simp]

theorem CategoryTheory.Limits.image.factorThruImage_preComp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X 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)

source

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

⋯ = ⋯

source

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

source

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

⋯ = ⋯

source

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

⋯ = ⋯

source

instance CategoryTheory.Limits.image.isIso_precomp_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y 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

⋯ = ⋯

source

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

⋯ = ⋯

source

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

source

@[simp]

theorem CategoryTheory.Limits.image.compIso_hom_comp_image_ι {C : Type u} [CategoryTheory.Category.{v, u} C] {X 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

source

@[simp]

theorem CategoryTheory.Limits.image.compIso_hom_comp_image_ι_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X 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)

source

@[simp]

theorem CategoryTheory.Limits.image.compIso_inv_comp_image_ι {C : Type u} [CategoryTheory.Category.{v, u} C] {X 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)

source

@[simp]

theorem CategoryTheory.Limits.image.compIso_inv_comp_image_ι_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X 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)

source

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

CategoryTheory.Limits.HasImage (CategoryTheory.Arrow.mk f).hom

Equations

⋯ = ⋯

source

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

source

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_ι := ⋯ } }

source

@[simp]

theorem CategoryTheory.Limits.ImageMap.map_ι_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {f 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)

source

@[simp]

theorem CategoryTheory.Limits.ImageMap.factor_map {C : Type u} [CategoryTheory.Category.{v, u} C] {f 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)

source

@[simp]

theorem CategoryTheory.Limits.ImageMap.factor_map_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {f 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)

source

def CategoryTheory.Limits.ImageMap.transport {C : Type u} [CategoryTheory.Category.{v, u} C] {f 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.

source

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

)

Instances

source

theorem CategoryTheory.Limits.HasImageMap.mk {C : Type u} [CategoryTheory.Category.{v, u} C] {f 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

source

theorem CategoryTheory.Limits.HasImageMap.transport {C : Type u} [CategoryTheory.Category.{v, u} C] {f 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

source

def CategoryTheory.Limits.HasImageMap.imageMap {C : Type u} [CategoryTheory.Category.{v, u} C] {f 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 ⋯

source

@[instance 100]

instance CategoryTheory.Limits.hasImageMapOfIsIso {C : Type u} [CategoryTheory.Category.{v, u} C] {f 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

⋯ = ⋯

source

instance CategoryTheory.Limits.HasImageMap.comp {C : Type u} [CategoryTheory.Category.{v, u} C] {f g 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

⋯ = ⋯

source

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

x = y

source

map = map'

source

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

F.map = G.map

source

@[simp]

(map = map') = True

source

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

Subsingleton (CategoryTheory.Limits.ImageMap sq)

Equations

⋯ = ⋯

source

@[reducible, inline]

abbrev CategoryTheory.Limits.image.map {C : Type u} [CategoryTheory.Category.{v, u} C] {f 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

source

theorem CategoryTheory.Limits.image.factor_map {C : Type u} [CategoryTheory.Category.{v, u} C] {f 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)

source

theorem CategoryTheory.Limits.image.map_ι {C : Type u} [CategoryTheory.Category.{v, u} C] {f 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

source

theorem CategoryTheory.Limits.image.map_homMk'_ι {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y P 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

source

def CategoryTheory.Limits.imageMapComp {C : Type u} [CategoryTheory.Category.{v, u} C] {f 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_ι := ⋯ }

source

@[simp]

theorem CategoryTheory.Limits.image.map_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {f 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')

source

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_ι := ⋯ }

source

@[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)

source

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

Instances

source

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.

source

@[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

source

@[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

source

structure CategoryTheory.Limits.StrongEpiMonoFactorisation {C : Type u} [CategoryTheory.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 : 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.

source

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

source

def CategoryTheory.Limits.StrongEpiMonoFactorisation.toMonoIsImage {C : Type u} [CategoryTheory.Category.{v, u} C] {X 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 := ⋯ }

source

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.

)

Instances

source

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

source

@[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

⋯ = ⋯

source

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)

Instances

source

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

source

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

CategoryTheory.StrongEpi (CategoryTheory.Limits.factorThruImage f)

source

@[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

⋯ = ⋯

source

@[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

⋯ = ⋯

source

@[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

⋯ = ⋯

source

def CategoryTheory.Limits.image.isoStrongEpiMono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrongEpiMonoFactorisations C] {X 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