# mathlibdocumentation

algebra.category.Group.images

# 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 image of a morphism in AddCommGroup is just the bundling of add_monoid_hom.range f

Equations

the inclusion of image f into the target

Equations
@[instance]

the corestriction map to the image

Equations
F'.I

the universal property for the image factorisation

Equations

the factorisation of any morphism in AddCommGroup through a mono.

Equations
The categorical image of a morphism in AddCommGroup agrees with the usual group-theoretical range.