mathlib3 documentation

algebra.category.Group.images

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.

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