mathlib documentation

category_theory.limits.shapes.images

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

Main statements

Future work

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

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

The obvious factorisation of a monomorphism through itself.

Equations
@[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'.mF = F'

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

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

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

The trivial factorisation of a monomorphism satisfies the universal property.

Equations

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

Equations
structure category_theory.limits.image_factorisation {C : Type u} [category_theory.category C] {X Y : C} :
(X Y)Type (max u v)

Data exhibiting that a morphism f has an image.

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

Equations

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

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

has_images represents a choice of image for every morphism

Instances

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

Equations

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

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.

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

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

has_image_map sq means that there is an image_map for the square sq.

Instances

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

Equations
@[class]

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

Instances

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
structure category_theory.limits.strong_epi_mono_factorisation {C : Type u} [category_theory.category C] {X Y : C} :
(X Y)Type (max u v)

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

@[class]

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

Instances
@[class]

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

Instances

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

@[instance]

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

@[instance]

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

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