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} (f : G H) :

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
Instances for AddCommGroup.image.ι

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