To discuss images in a category , we must first fix a notion of subobject or embedding in . (Sometimes we want these to be the monomorphisms, but sometimes we want the regular monomorphisms instead.) Then the image of a morphism in is a universal factorization of into a composite such that is a subobject, of the specified sort.
Note that in this generality, a given morphism may or may not have an image, although if it does, it is unique up to isomorphism by universality. In many cases, images can be constructed out of limits and colimits in the ambient category. In particular, in a regular category, images (relative to all monomorphisms) can be constructed as the quotient object of a kernel pair.
Let be a category, let be a subclass of the monomorphisms in , and let be a morphism in . The image of is the smallest -subobject through which factors (if it exists). The factorizing morphism is sometimes called the corestriction of (or coastriction, see mathoverflow):
In other words, it is a factorization of (i.e. ) such that , and given any other factorization with , we have as subobjects of (i.e. factors through , for some ). Such a factorization is unique up to unique isomorphism, if it exists.
This can be phrased equivalently as follows. Let be the slice category of over , and let be its full subcategory whose objects are -morphisms into . If all images exist in , then taking the image of a map provides a left adjoint
to the inclusion . More generally, an image of a single morphism is a universal arrow from to this inclusion.
In algebraic categories such as Grp, for monomorphisms, this also reproduces the ordinary notions of image.
In Top, for subspace inclusions, the -image is the set-theoretic image topologized as a subspace of the codomain. On the other hand, for injective continuous maps, the -image is the set-theoretic image topologized as a quotient space of the domain. For more basic details see at Introduction to Topology -- 1 here.
A regular category can be defined as a finitely complete category in which all images exist for monomorphisms, and such images are moreover stable under pullback. In particular, this includes any topos.
In Cat (considered as a 1-category), the image of a functor is the smallest subcategory of which contains images through of all morphisms in . Note that some of the morphisms in the image may not be images of any morphism in ; all morphisms in the image of are compositions in of -composable sequences of images of morphisms in , but these themselves do not necessarily form -composable sequences of morphisms in .
Suppose that is closed under composition, and that is an image factorization relative to . Then has the property that if for some , then is an isomorphism — for then we would have and so by universality of images, would factor through . In particular, if is the class of all monomorphisms and has equalizers, then is an extremal epimorphism.
is a commutative square with , then the pullback is an -morphism through which factors. Hence must be an isomorphism, and so the square admits a diagonal filler, which is unique since is monic. It follows that if all -images exist in , then is the right class of an orthogonal factorization system, and -images are precisely the factorizations in this OFS.
Conversely, it is easy to see that if is an OFS on a category , then all -images exist and are given by the factorizations of the OFS. Therefore, to give a notion of image is more or less equivalent to giving an orthogonal factorization system.
Note that the notion of factorization system is self-dual. Therefore, if is a factorization system and is an -factorization of , then not only is the -image of (the least -subobject through which factors), but dually is also the -coimage of , i.e. the greatest -quotient through which factors.
However, see below for additional remarks on the usage of the terms “image” and “coimage.”
where denotes the pushout
In other words, the regular image is the equalizer of the cokernel pair. To see that this is in fact the -image, we first note that it is of course a regular monomorphism by definition, and then invoke the fact that in a category with finite limits and colimits, a monomorphism is regular if and only if it is the equalizer of its cokernel pair.
Dually, the regular coimage of a morphism is the coequalizer of its kernel pair. In Set (and more generally in any topos) these two constructions coincide, but in general they are distinct. For example, in Top the regular image is the set-theoretic image topologized as a subspace of the codomain, while the regular coimage is the set-theoretic image topologized as a quotient space of the domain.
Note that some authors drop the “regular” and simply call these constructions the image and coimage respectively. This can be confusing, however, since in many cases (such as in any regular category) the regular coimage coincides with the -image for the class of all monomorphisms, which it is also natural to simply call the image.
Suppose that and are two classes with . If has both an -image and an -image , then by universality, the latter must factor through the former. The correspondence between images and factorization systems also extends to pairs; see ternary factorization system.
As a special case of this, we have:
If has finite limits and colimits, then there is a unique map
from its regular coimage to its image such that
Because coequalizes , a morphism in
Because is epi it follows that equalizes and hence in the diagram
If this map is an isomorphism, then is sometimes called a strict morphism. In particular, if has finite limits and colimits and every morphism is a strict morphism, then the regular image and regular coimage factorizations coincide and give an epi-mono factorization system.
In higher category theory there are generalizations of the notion of image, such as these:
However, it is not clear that either serves as the proper categorification of the notion described above.
There are several properties we might want a ‘higher image’ to have. For example, in an -category, we might want isomorphic 1-cells to have equivalent images. In Cat, we might want the image of a functor between discrete categories to be its image as a function. One fruitful direction is to study a factorization system in a 2-category.
this reduces to the above equalizer definition in the case that the ambient -category is just an ordinary category;
For more see n-image.