Documentation

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

theorem Subtype.ext_val_iff {α : Sort u_1} {p : αProp} {a1 : { x : α // p x }} {a2 : { x : α // p x }} :
a1 = a2 a1 = a2

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

Equations
Instances For

    the inclusion of image f into the target

    Equations
    Instances For

      the corestriction map to the image

      Equations
      Instances For

        the universal property for the image factorisation

        Equations
        Instances For

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

          Equations
          Instances For

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

            Equations
            Instances For