Let be such that , one needs to show that . Since the equalizer of exists, factorizes as with monic. But then is a factorization of with monomorphism. Hence by the universal property of the image there exists a unique arrow such that and since is monic . Furthermore, one has and by the monomorphism property of one obtains .
This means that and thus that equalizes , whence .
Second definition
In a category with all finite limits and colimits, the image is defined as the equalizer of the so-called cokernel pair, which is the cocartesian of a morphism with itself over its domain, which will result in a pair of morphisms , on which the equalizer is taken, i.e. the first of the following diagrams is cocartesian, and the second equalizing.[3]
Remarks:
Finite bicompleteness of the category ensures that pushouts and equalizers exist.
can be called regular image as is a regular monomorphism, i.e. the equalizer of a pair of morphisms. (Recall also that an equalizer is automatically a monomorphism).
In an abelian category, the cokernel pair property can be written and the equalizer condition . Moreover, all monomorphisms are regular.
Theorem — If always factorizes through regular monomorphisms, then the two definitions coincide.
Proof
First definition implies the second: Assume that (1) holds with regular monomorphism.
Equalization: one needs to show that . As the cokernel pair of and by previous proposition, since has all equalizers, the arrow in the factorization is an epimorphism, hence .
Universality: in a category with all colimits (or at least all pushouts) itself admits a cokernel pair
Moreover, as a regular monomorphism, is the equalizer of a pair of morphisms but we claim here that it is also the equalizer of .
Indeed, by construction thus the "cokernel pair" diagram for yields a unique morphism such that . Now, a map which equalizes also satisfies , hence by the equalizer diagram for , there exists a unique map such that .
Finally, use the cokernel pair diagram (of ) with : there exists a unique such that . Therefore, any map which equalizes also equalizes and thus uniquely factorizes as . This exactly means that is the equalizer of .
Second definition implies the first:
Factorization: taking in the equalizer diagram ( corresponds to ), one obtains the factorization .
Universality: let be a factorization with regular monomorphism, i.e. the equalizer of some pair .
Then so that by the "cokernel pair" diagram (of ), with , there exists a unique such that .
Now, from (m from the equalizer of (i1, i2) diagram), one obtains , hence by the universality in the (equalizer of (d1, d2) diagram, with f replaced by m), there exists a unique such that .
^Mitchell, Barry (1965), Theory of categories, Pure and applied mathematics, vol. 17, Academic Press, ISBN978-0-12-499250-4, MR0202787 Section I.10 p.12
^Mitchell, Barry (1965), Theory of categories, Pure and applied mathematics, vol. 17, Academic Press, ISBN978-0-12-499250-4, MR0202787 Proposition 10.1 p.12
^Kashiwara, Masaki; Schapira, Pierre (2006), "Categories and Sheaves", Grundlehren der Mathematischen Wissenschaften, vol. 332, Berlin Heidelberg: Springer, pp. 113–114 Definition 5.1.1