Documentation

Mathlib.Algebra.Category.GroupCat.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 AddCommGroupCat is an abelian category.

the image of a morphism in AddCommGroupCat is just the bundling of AddMonoidHom.range f

Equations
Instances For

    the inclusion of image f into the target

    Equations
    Instances For

      the universal property for the image factorisation

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

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

        Equations
        Instances For

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

          Equations
          Instances For