mathlib3 documentation

category_theory.limits.shapes.images

Categorical images #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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} (f : X Y) :
Type (max u v)

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

Instances for category_theory.limits.mono_factorisation
@[simp]
theorem category_theory.limits.mono_factorisation.fac_assoc {C : Type u} [category_theory.category C] {X Y : C} {f : X Y} (self : category_theory.limits.mono_factorisation f) {X' : C} (f' : Y X') :
self.e self.m f' = f f'

The obvious factorisation of a monomorphism through itself.

Equations
@[ext]

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

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

Equations

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

Equations
@[simp]
@[simp]

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

Equations
@[simp]

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

Equations

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

Equations

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

Instances for category_theory.limits.is_image

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

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

Data exhibiting that a morphism f has an image.

Instances for category_theory.limits.image_factorisation

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

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

The categorical image of a morphism.

Equations

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

Equations
Instances for category_theory.limits.image.ι

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

Equations
Instances for category_theory.limits.image.lift
@[protected, instance]

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

@[class]

has_images asserts that every morphism has an image.

Instances of this typeclass

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

Equations
Instances for category_theory.limits.image.eq_to_hom

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

@[protected, instance]

image.pre_comp f g is a monomorphism.

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.

@[protected, instance]

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

@[protected, instance]

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

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

Instances for category_theory.limits.image_map

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

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 of this typeclass
Instances of other typeclasses for category_theory.limits.has_image_maps
  • category_theory.limits.has_image_maps.has_sizeof_inst

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} (f : 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.

Instances for category_theory.limits.strong_epi_mono_factorisation

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

Equations
@[class]

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

@[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 of this typeclass

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

@[protected, instance]

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

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