The category of commutative additive groups has images. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
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.