# 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
Instances for AddCommGroup.image.ι
@[protected, instance]

the corestriction map to the image

Equations
noncomputable def AddCommGroup.image.lift {G H : AddCommGroup} {f : G H}  :
F'.I

the universal property for the image factorisation

Equations

the factorisation of any morphism in AddCommGroup through a mono.

Equations
noncomputable def AddCommGroup.is_image {G H : AddCommGroup} (f : G H) :

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

Equations
noncomputable def AddCommGroup.image_iso_range {G H : AddCommGroup} (f : G H) :

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

Equations