Categorical images

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

Main definitions

A mono_factorisation is a factorisation f = e ≫ m, where m is a monomorphism
is_image F means that a given mono factorisation F has the universal property of the image.
has_image f means that we have chosen an image for the morphism f : X ⟶ Y.
- In this case, image f is the image object, image.ι f : image f ⟶ Y is the monomorphism m of the factorisation and factor_thru_image f : X ⟶ image f is the morphism e.
has_images C means that every morphism in C has an image.
Let f : X ⟶ Y and g : P ⟶ Q be morphisms in C, which we will represent as objects of the arrow category arrow C. Then sq : f ⟶ g is a commutative square in C. If f and g have images, then has_image_map sq represents the fact that there is a morphism i : image f ⟶ image g making the diagram

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

commute, where the top row is the image factorisation of f, the bottom row is the image factorisation of g, and the outer rectangle is the commutative square sq.
If a category has_images, then has_image_maps means that every commutative square admits an image map.
If a category has_images, then has_strong_epi_images means that the morphism to the image is always a strong epimorphism.

Main statements

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

Future work

TODO: coimages, and abelian categories.
TODO: connect this with existing working in the group theory and ring theory libraries.

source

structure category_theory.limits.mono_factorisation {C : Type u} [category_theory.category C] {X Y : C} :

(X ⟶ Y) → Type (max u v)

I : C
m : c.I ⟶ Y
m_mono : category_theory.mono c.m
e : X ⟶ c.I
fac' : c.e ≫ c.m = f . "obviously"

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

source

def category_theory.limits.mono_factorisation.self {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.mono f] :

category_theory.limits.mono_factorisation f

The obvious factorisation of a monomorphism through itself.

Equations

category_theory.limits.mono_factorisation.self f = {I := X, m := f, m_mono := _inst_2, e := 𝟙 X, fac' := _}

source

@[instance]

def category_theory.limits.mono_factorisation.inhabited {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.mono f] :

inhabited (category_theory.limits.mono_factorisation f)

Equations

category_theory.limits.mono_factorisation.inhabited f = {default := category_theory.limits.mono_factorisation.self f _inst_2}

source

@[ext]

theorem category_theory.limits.mono_factorisation.ext {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) {F F' : category_theory.limits.mono_factorisation f} (hI : F.I = F'.I) :

F.m = category_theory.eq_to_hom hI ≫ F'.m → F = F'

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

source

structure category_theory.limits.is_image {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} :

category_theory.limits.mono_factorisation f → Type (max u v)

lift : Π (F' : category_theory.limits.mono_factorisation f), F.I ⟶ F'.I
lift_fac' : (∀ (F' : category_theory.limits.mono_factorisation f), c.lift F' ≫ F'.m = F.m) . "obviously"

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

source

@[simp]

theorem category_theory.limits.is_image.fac_lift {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} {F : category_theory.limits.mono_factorisation f} (hF : category_theory.limits.is_image F) (F' : category_theory.limits.mono_factorisation f) :

F.e ≫ hF.lift F' = F'.e

source

@[simp]

theorem category_theory.limits.is_image.fac_lift_assoc {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} {F : category_theory.limits.mono_factorisation f} (hF : category_theory.limits.is_image F) (F' : category_theory.limits.mono_factorisation f) {X' : C} (f' : F'.I ⟶ X') :

F.e ≫ hF.lift F' ≫ f' = F'.e ≫ f'

source

def category_theory.limits.is_image.self {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.mono f] :

category_theory.limits.is_image (category_theory.limits.mono_factorisation.self f)

The trivial factorisation of a monomorphism satisfies the universal property.

Equations

category_theory.limits.is_image.self f = {lift := λ (F' : category_theory.limits.mono_factorisation f), F'.e, lift_fac' := _}

source

@[simp]

theorem category_theory.limits.is_image.self_lift {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.mono f] (F' : category_theory.limits.mono_factorisation f) :

(category_theory.limits.is_image.self f).lift F' = F'.e

source

@[instance]

def category_theory.limits.is_image.inhabited {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.mono f] :

inhabited (category_theory.limits.is_image (category_theory.limits.mono_factorisation.self f))

Equations

category_theory.limits.is_image.inhabited f = {default := category_theory.limits.is_image.self f _inst_2}

source

def category_theory.limits.is_image.iso_ext {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} {F F' : category_theory.limits.mono_factorisation f} :

category_theory.limits.is_image F → category_theory.limits.is_image F' → (F.I ≅ F'.I)

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

Equations

hF.iso_ext hF' = {hom := hF.lift F', inv := hF'.lift F, hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

theorem category_theory.limits.is_image.iso_ext_inv {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} {F F' : category_theory.limits.mono_factorisation f} (hF : category_theory.limits.is_image F) (hF' : category_theory.limits.is_image F') :

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

source

@[simp]

theorem category_theory.limits.is_image.iso_ext_hom {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} {F F' : category_theory.limits.mono_factorisation f} (hF : category_theory.limits.is_image F) (hF' : category_theory.limits.is_image F') :

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

source

@[class]

structure category_theory.limits.has_image {C : Type u} [category_theory.category C] {X Y : C} :

(X ⟶ Y) → Type (max u v)

F : category_theory.limits.mono_factorisation f
is_image : category_theory.limits.is_image category_theory.limits.has_image.F

Data exhibiting that a morphism f has an image.

Instances

source

def category_theory.limits.image.mono_factorisation {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] :

category_theory.limits.mono_factorisation f

The chosen factorisation of f through a monomorphism.

Equations

category_theory.limits.image.mono_factorisation f = category_theory.limits.has_image.F

source

def category_theory.limits.image.is_image {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] :

category_theory.limits.is_image (category_theory.limits.image.mono_factorisation f)

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

Equations

category_theory.limits.image.is_image f = category_theory.limits.has_image.is_image

source

def category_theory.limits.image {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] :

The categorical image of a morphism.

Equations

category_theory.limits.image f = (category_theory.limits.image.mono_factorisation f).I

source

def category_theory.limits.image.ι {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] :

category_theory.limits.image f ⟶ Y

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

Equations

category_theory.limits.image.ι f = (category_theory.limits.image.mono_factorisation f).m

source

@[simp]

theorem category_theory.limits.image.as_ι {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] :

(category_theory.limits.image.mono_factorisation f).m = category_theory.limits.image.ι f

source

@[instance]

def category_theory.limits.category_theory.mono {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] :

category_theory.mono (category_theory.limits.image.ι f)

Equations

_ = _

source

def category_theory.limits.factor_thru_image {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] :

X ⟶ category_theory.limits.image f

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

Equations

category_theory.limits.factor_thru_image f = (category_theory.limits.image.mono_factorisation f).e

source

@[simp]

theorem category_theory.limits.as_factor_thru_image {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] :

(category_theory.limits.image.mono_factorisation f).e = category_theory.limits.factor_thru_image f

Rewrite in terms of the factor_thru_image interface.

source

@[simp]

theorem category_theory.limits.image.fac {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] :

category_theory.limits.factor_thru_image f ≫ category_theory.limits.image.ι f = f

source

@[simp]

theorem category_theory.limits.image.fac_assoc {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] {X' : C} (f' : Y ⟶ X') :

category_theory.limits.factor_thru_image f ≫ category_theory.limits.image.ι f ≫ f' = f ≫ f'

source

def category_theory.limits.image.lift {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} [category_theory.limits.has_image f] (F' : category_theory.limits.mono_factorisation f) :

category_theory.limits.image f ⟶ F'.I

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

Equations

category_theory.limits.image.lift F' = (category_theory.limits.image.is_image f).lift F'

source

@[simp]

theorem category_theory.limits.image.lift_fac_assoc {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} [category_theory.limits.has_image f] (F' : category_theory.limits.mono_factorisation f) {X' : C} (f' : Y ⟶ X') :

category_theory.limits.image.lift F' ≫ F'.m ≫ f' = category_theory.limits.image.ι f ≫ f'

source

@[simp]

theorem category_theory.limits.image.lift_fac {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} [category_theory.limits.has_image f] (F' : category_theory.limits.mono_factorisation f) :

category_theory.limits.image.lift F' ≫ F'.m = category_theory.limits.image.ι f

source

@[simp]

theorem category_theory.limits.image.fac_lift {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} [category_theory.limits.has_image f] (F' : category_theory.limits.mono_factorisation f) :

category_theory.limits.factor_thru_image f ≫ category_theory.limits.image.lift F' = F'.e

source

@[simp]

theorem category_theory.limits.image.fac_lift_assoc {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} [category_theory.limits.has_image f] (F' : category_theory.limits.mono_factorisation f) {X' : C} (f' : F'.I ⟶ X') :

category_theory.limits.factor_thru_image f ≫ category_theory.limits.image.lift F' ≫ f' = F'.e ≫ f'

source

@[instance]

def category_theory.limits.lift_mono {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} [category_theory.limits.has_image f] (F' : category_theory.limits.mono_factorisation f) :

category_theory.mono (category_theory.limits.image.lift F')

Equations

_ = _

source

theorem category_theory.limits.has_image.uniq {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} [category_theory.limits.has_image f] (F' : category_theory.limits.mono_factorisation f) (l : category_theory.limits.image f ⟶ F'.I) :

l ≫ F'.m = category_theory.limits.image.ι f → l = category_theory.limits.image.lift F'

source

@[class]

structure category_theory.limits.has_images (C : Type u) [category_theory.category C] :

Type (max u v)

has_image : Π {X Y : C} (f : X ⟶ Y), category_theory.limits.has_image f

has_images represents a choice of image for every morphism

Instances

source

def category_theory.limits.image_mono_iso_source {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] [category_theory.mono f] :

category_theory.limits.image f ≅ X

The image of a monomorphism is isomorphic to the source.

Equations

category_theory.limits.image_mono_iso_source f = (category_theory.limits.image.is_image f).iso_ext (category_theory.limits.is_image.self f)

source

@[simp]

theorem category_theory.limits.image_mono_iso_source_inv_ι_assoc {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] [category_theory.mono f] {X' : C} (f' : Y ⟶ X') :

(category_theory.limits.image_mono_iso_source f).inv ≫ category_theory.limits.image.ι f ≫ f' = f ≫ f'

source

@[simp]

theorem category_theory.limits.image_mono_iso_source_inv_ι {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] [category_theory.mono f] :

(category_theory.limits.image_mono_iso_source f).inv ≫ category_theory.limits.image.ι f = f

source

@[simp]

theorem category_theory.limits.image_mono_iso_source_hom_self {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] [category_theory.mono f] :

(category_theory.limits.image_mono_iso_source f).hom ≫ f = category_theory.limits.image.ι f

source

@[simp]

theorem category_theory.limits.image_mono_iso_source_hom_self_assoc {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] [category_theory.mono f] {X' : C} (f' : Y ⟶ X') :

(category_theory.limits.image_mono_iso_source f).hom ≫ f ≫ f' = category_theory.limits.image.ι f ≫ f'

source

@[ext]

theorem category_theory.limits.image.ext {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] {W : C} {g h : category_theory.limits.image f ⟶ W} [category_theory.limits.has_limit (category_theory.limits.parallel_pair g h)] :

category_theory.limits.factor_thru_image f ≫ g = category_theory.limits.factor_thru_image f ≫ h → g = h

source

@[instance]

def category_theory.limits.category_theory.epi {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] [Π {Z : C} (g h : category_theory.limits.image f ⟶ Z), category_theory.limits.has_limit (category_theory.limits.parallel_pair g h)] :

category_theory.epi (category_theory.limits.factor_thru_image f)

Equations

_ = _

source

theorem category_theory.limits.epi_image_of_epi {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] [E : category_theory.epi f] :

category_theory.epi (category_theory.limits.image.ι f)

source

theorem category_theory.limits.epi_of_epi_image {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] [category_theory.epi (category_theory.limits.image.ι f)] [category_theory.epi (category_theory.limits.factor_thru_image f)] :

category_theory.epi f

source

def category_theory.limits.image.eq_to_hom {C : Type u} [category_theory.category C] {X Y : C} {f f' : X ⟶ Y} [category_theory.limits.has_image f] [category_theory.limits.has_image f'] :

f = f' → (category_theory.limits.image f ⟶ category_theory.limits.image f')

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

Equations

category_theory.limits.image.eq_to_hom h = category_theory.limits.image.lift {I := category_theory.limits.image f' _inst_3, m := category_theory.limits.image.ι f' _inst_3, m_mono := _, e := category_theory.limits.factor_thru_image f' _inst_3, fac' := _}

source

@[instance]

def category_theory.limits.category_theory.is_iso {C : Type u} [category_theory.category C] {X Y : C} {f f' : X ⟶ Y} [category_theory.limits.has_image f] [category_theory.limits.has_image f'] (h : f = f') :

category_theory.is_iso (category_theory.limits.image.eq_to_hom h)

Equations

category_theory.limits.category_theory.is_iso h = {inv := category_theory.limits.image.eq_to_hom _, hom_inv_id' := _, inv_hom_id' := _}

source

def category_theory.limits.image.eq_to_iso {C : Type u} [category_theory.category C] {X Y : C} {f f' : X ⟶ Y} [category_theory.limits.has_image f] [category_theory.limits.has_image f'] :

f = f' → (category_theory.limits.image f ≅ category_theory.limits.image f')

An equation between morphisms gives an isomorphism between the images.

Equations

category_theory.limits.image.eq_to_iso h = category_theory.as_iso (category_theory.limits.image.eq_to_hom h)

source

theorem category_theory.limits.image.eq_fac {C : Type u} [category_theory.category C] {X Y : C} {f f' : X ⟶ Y} [category_theory.limits.has_image f] [category_theory.limits.has_image f'] [category_theory.limits.has_equalizers C] (h : f = f') :

category_theory.limits.image.ι f = (category_theory.limits.image.eq_to_iso h).hom ≫ category_theory.limits.image.ι f'

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

source

def category_theory.limits.image.pre_comp {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [category_theory.limits.has_image g] [category_theory.limits.has_image (f ≫ g)] :

category_theory.limits.image (f ≫ g) ⟶ category_theory.limits.image g

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

Equations

category_theory.limits.image.pre_comp f g = category_theory.limits.image.lift {I := category_theory.limits.image g _inst_2, m := category_theory.limits.image.ι g _inst_2, m_mono := _, e := f ≫ category_theory.limits.factor_thru_image g, fac' := _}

source

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

category_theory.limits.image.pre_comp f (g ≫ h) ≫ category_theory.limits.image.pre_comp g h = category_theory.limits.image.eq_to_hom _ ≫ category_theory.limits.image.pre_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]

def category_theory.limits.category_theory.limits.has_image {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] :

category_theory.limits.has_image (category_theory.arrow.mk f).hom

Equations

category_theory.limits.category_theory.limits.has_image f = show category_theory.limits.has_image f, from _inst_2

source

@[class]

structure category_theory.limits.has_image_map {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} [category_theory.limits.has_image f.hom] [category_theory.limits.has_image g.hom] :

(f ⟶ g) → Type v

map : category_theory.limits.image f.hom ⟶ category_theory.limits.image g.hom
map_ι' : category_theory.limits.has_image_map.map sq ≫ category_theory.limits.image.ι g.hom = category_theory.limits.image.ι f.hom ≫ sq.right . "obviously"

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

Instances

category_theory.limits.has_image_maps.has_image_map

source

@[simp]

theorem category_theory.limits.has_image_map.factor_map {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} [category_theory.limits.has_image f.hom] [category_theory.limits.has_image g.hom] (sq : f ⟶ g) [category_theory.limits.has_image_map sq] :

category_theory.limits.factor_thru_image f.hom ≫ category_theory.limits.has_image_map.map sq = sq.left ≫ category_theory.limits.factor_thru_image g.hom

source

@[simp]

theorem category_theory.limits.has_image_map.factor_map_assoc {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} [category_theory.limits.has_image f.hom] [category_theory.limits.has_image g.hom] (sq : f ⟶ g) [category_theory.limits.has_image_map sq] {X' : C} (f' : category_theory.limits.image g.hom ⟶ X') :

category_theory.limits.factor_thru_image f.hom ≫ category_theory.limits.has_image_map.map sq ≫ f' = sq.left ≫ category_theory.limits.factor_thru_image g.hom ≫ f'

source

@[instance]

def category_theory.limits.subsingleton {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} [category_theory.limits.has_image f.hom] [category_theory.limits.has_image g.hom] (sq : f ⟶ g) :

subsingleton (category_theory.limits.has_image_map sq)

Equations

_ = _

source

def category_theory.limits.image.map {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} [category_theory.limits.has_image f.hom] [category_theory.limits.has_image g.hom] (sq : f ⟶ g) [category_theory.limits.has_image_map sq] :

category_theory.limits.image f.hom ⟶ category_theory.limits.image g.hom

The map on images induced by a commutative square.

source

theorem category_theory.limits.image.factor_map {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} [category_theory.limits.has_image f.hom] [category_theory.limits.has_image g.hom] (sq : f ⟶ g) [category_theory.limits.has_image_map sq] :

category_theory.limits.factor_thru_image f.hom ≫ category_theory.limits.image.map sq = sq.left ≫ category_theory.limits.factor_thru_image g.hom

source

theorem category_theory.limits.image.map_ι {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} [category_theory.limits.has_image f.hom] [category_theory.limits.has_image g.hom] (sq : f ⟶ g) [category_theory.limits.has_image_map sq] :

category_theory.limits.image.map sq ≫ category_theory.limits.image.ι g.hom = category_theory.limits.image.ι f.hom ≫ sq.right

source

theorem category_theory.limits.image.map_hom_mk'_ι {C : Type u} [category_theory.category C] {X Y P Q : C} {k : X ⟶ Y} [category_theory.limits.has_image k] {l : P ⟶ Q} [category_theory.limits.has_image l] {m : X ⟶ P} {n : Y ⟶ Q} (w : m ≫ l = k ≫ n) [category_theory.limits.has_image_map (category_theory.arrow.hom_mk' w)] :

category_theory.limits.image.map (category_theory.arrow.hom_mk' w) ≫ category_theory.limits.image.ι l = category_theory.limits.image.ι k ≫ n

source

def category_theory.limits.has_image_map_comp {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} [category_theory.limits.has_image f.hom] [category_theory.limits.has_image g.hom] (sq : f ⟶ g) [category_theory.limits.has_image_map sq] {h : category_theory.arrow C} [category_theory.limits.has_image h.hom] (sq' : g ⟶ h) [category_theory.limits.has_image_map sq'] :

category_theory.limits.has_image_map (sq ≫ sq')

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

Equations

category_theory.limits.has_image_map_comp sq sq' = {map := category_theory.limits.image.map sq ≫ category_theory.limits.image.map sq', map_ι' := _}

source

@[simp]

theorem category_theory.limits.image.map_comp {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} [category_theory.limits.has_image f.hom] [category_theory.limits.has_image g.hom] (sq : f ⟶ g) [category_theory.limits.has_image_map sq] {h : category_theory.arrow C} [category_theory.limits.has_image h.hom] (sq' : g ⟶ h) [category_theory.limits.has_image_map sq'] [category_theory.limits.has_image_map (sq ≫ sq')] :

category_theory.limits.image.map (sq ≫ sq') = category_theory.limits.image.map sq ≫ category_theory.limits.image.map sq'

source

def category_theory.limits.has_image_map_id {C : Type u} [category_theory.category C] (f : category_theory.arrow C) [category_theory.limits.has_image f.hom] :

category_theory.limits.has_image_map (𝟙 f)

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

Equations

category_theory.limits.has_image_map_id f = {map := 𝟙 (category_theory.limits.image f.hom), map_ι' := _}

source

@[simp]

theorem category_theory.limits.image.map_id {C : Type u} [category_theory.category C] (f : category_theory.arrow C) [category_theory.limits.has_image f.hom] [category_theory.limits.has_image_map (𝟙 f)] :

category_theory.limits.image.map (𝟙 f) = 𝟙 (category_theory.limits.image f.hom)

source

@[class]

structure category_theory.limits.has_image_maps (C : Type u) [category_theory.category C] [category_theory.limits.has_images C] :

Type (max u v)

has_image_map : Π {f g : category_theory.arrow C} (st : f ⟶ g), category_theory.limits.has_image_map st

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

Instances

source

def category_theory.limits.im {C : Type u} [category_theory.category C] [category_theory.limits.has_images C] [category_theory.limits.has_image_maps C] :

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

category_theory.limits.im = {obj := λ (f : category_theory.arrow C), category_theory.limits.image f.hom, map := λ (_x _x_1 : category_theory.arrow C) (st : _x ⟶ _x_1), category_theory.limits.image.map st, map_id' := _, map_comp' := _}

source

@[simp]

theorem category_theory.limits.im_obj {C : Type u} [category_theory.category C] [category_theory.limits.has_images C] [category_theory.limits.has_image_maps C] (f : category_theory.arrow C) :

category_theory.limits.im.obj f = category_theory.limits.image f.hom

source

@[simp]

theorem category_theory.limits.im_map {C : Type u} [category_theory.category C] [category_theory.limits.has_images C] [category_theory.limits.has_image_maps C] (_x _x_1 : category_theory.arrow C) (st : _x ⟶ _x_1) :

category_theory.limits.im.map st = category_theory.limits.image.map st

source

structure category_theory.limits.strong_epi_mono_factorisation {C : Type u} [category_theory.category C] {X Y : C} :

(X ⟶ Y) → Type (max u v)

to_mono_factorisation : category_theory.limits.mono_factorisation f
e_strong_epi : category_theory.strong_epi c.to_mono_factorisation.e

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

source

@[instance]

def category_theory.limits.strong_epi_mono_factorisation_inhabited {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.strong_epi f] :

inhabited (category_theory.limits.strong_epi_mono_factorisation f)

Satisfying the inhabited linter

Equations

category_theory.limits.strong_epi_mono_factorisation_inhabited f = {default := {to_mono_factorisation := {I := Y, m := 𝟙 Y, m_mono := _, e := f, fac' := _}, e_strong_epi := _inst_2}}

source

def category_theory.limits.strong_epi_mono_factorisation.to_mono_is_image {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} (F : category_theory.limits.strong_epi_mono_factorisation f) :

category_theory.limits.is_image F.to_mono_factorisation

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

Equations

F.to_mono_is_image = {lift := λ (G : category_theory.limits.mono_factorisation f), category_theory.arrow.lift (category_theory.arrow.hom_mk' _), lift_fac' := _}

source

@[class]

structure category_theory.limits.has_strong_epi_mono_factorisations (C : Type u) [category_theory.category C] :

Type (max u v)

has_fac : Π {X Y : C} (f : X ⟶ Y), category_theory.limits.strong_epi_mono_factorisation f

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

Instances

category_theory.abelian.category_theory.limits.has_strong_epi_mono_factorisations

source

@[instance]

def category_theory.limits.has_images_of_has_strong_epi_mono_factorisations (C : Type u) [category_theory.category C] [category_theory.limits.has_strong_epi_mono_factorisations C] :

category_theory.limits.has_images C

Equations

category_theory.limits.has_images_of_has_strong_epi_mono_factorisations C = {has_image := λ (X Y : C) (f : X ⟶ Y), let F' : category_theory.limits.strong_epi_mono_factorisation f := category_theory.limits.has_strong_epi_mono_factorisations.has_fac f in {F := F'.to_mono_factorisation, is_image := F'.to_mono_is_image}}

source

@[class]

structure category_theory.limits.has_strong_epi_images (C : Type u) [category_theory.category C] [category_theory.limits.has_images C] :

Type (max u v)

strong_factor_thru_image : Π {X Y : C} (f : X ⟶ Y), category_theory.strong_epi (category_theory.limits.factor_thru_image f)

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

Instances

category_theory.limits.has_strong_epi_images_of_has_strong_epi_mono_factorisations

source

@[instance]

def category_theory.limits.has_strong_epi_images_of_has_strong_epi_mono_factorisations {C : Type u} [category_theory.category C] [category_theory.limits.has_strong_epi_mono_factorisations C] :

category_theory.limits.has_strong_epi_images C

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

Equations

category_theory.limits.has_strong_epi_images_of_has_strong_epi_mono_factorisations = {strong_factor_thru_image := λ (X Y : C) (f : X ⟶ Y), (category_theory.limits.has_strong_epi_mono_factorisations.has_fac f).e_strong_epi}

source

@[instance]

def category_theory.limits.has_image_maps_of_has_strong_epi_images {C : Type u} [category_theory.category C] [category_theory.limits.has_images C] [category_theory.limits.has_strong_epi_images C] :

category_theory.limits.has_image_maps C

A category with strong epi images has image maps. The construction is taken from Borceux, Handbook of Categorical Algebra 1, Proposition 4.4.5.

Equations

category_theory.limits.has_image_maps_of_has_strong_epi_images = {has_image_map := λ (f g : category_theory.arrow C) (st : f ⟶ g), let I : C := category_theory.limits.image (category_theory.limits.image.ι f.hom ≫ st.right), I' : C . "obviously" := category_theory.limits.image (st.left ≫ category_theory.limits.factor_thru_image g.hom), upper : category_theory.limits.strong_epi_mono_factorisation (f.hom ≫ st.right) := category_theory.limits.strong_epi_mono_factorisation.mk {I := I, m := category_theory.limits.image.ι (category_theory.limits.image.ι f.hom ≫ st.right) (category_theory.limits.has_images.has_image (category_theory.limits.image.ι f.hom ≫ st.right)), m_mono := _, e := category_theory.limits.factor_thru_image f.hom ≫ category_theory.limits.factor_thru_image (category_theory.limits.image.ι f.hom ≫ st.right), fac' := _}, lower : category_theory.limits.strong_epi_mono_factorisation (f.hom ≫ st.right) := category_theory.limits.strong_epi_mono_factorisation.mk {I := I', m := category_theory.limits.image.ι (st.left ≫ category_theory.limits.factor_thru_image g.hom) ≫ category_theory.limits.image.ι g.hom, m_mono := _, e := category_theory.limits.factor_thru_image (st.left ≫ category_theory.limits.factor_thru_image g.hom) (category_theory.limits.has_images.has_image (st.left ≫ category_theory.limits.factor_thru_image g.hom)), fac' := _}, s : I ⟶ I' := upper.to_mono_is_image.lift lower.to_mono_factorisation in {map := category_theory.limits.factor_thru_image (category_theory.limits.image.ι f.hom ≫ st.right) ≫ s ≫ category_theory.limits.image.ι (st.left ≫ category_theory.limits.factor_thru_image g.hom), map_ι' := _}}

source

def category_theory.limits.image.iso_strong_epi_mono {C : Type u} [category_theory.category C] [category_theory.limits.has_strong_epi_mono_factorisations C] {X Y : C} {f : X ⟶ Y} {I' : C} (e : X ⟶ I') (m : I' ⟶ Y) (comm : e ≫ m = f) [category_theory.strong_epi e] [category_theory.mono m] :

I' ≅ category_theory.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