The category of commutative additive groups has images. #
Note that we don't need to register any of the constructions here as instances, because we get them
from the fact that
AddCommGroup is an abelian category.
the inclusion of
image f into the target
the corestriction map to the image
the universal property for the image factorisation
the factorisation of any morphism in AddCommGroup through a mono.
the factorisation of any morphism in AddCommGroup through a mono has the universal property of
The categorical image of a morphism in
agrees with the usual group-theoretical range.