mathlib documentation

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.

def AddCommGroup.image {G H : AddCommGroup} :
(G H)AddCommGroup

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

the corestriction map to the image

Equations

the universal property for the image factorisation

Equations

the factorisation of any morphism in AddCommGroup through a mono.

Equations

the factorisation of any morphism in AddCommGroup through a mono has the universal property of the image.

Equations

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

Equations