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.

source
def AddCommGroup.image {G H : AddCommGroup} (f : G ⟶ H) :
AddCommGroup

the image of a morphism in AddCommGroup is just the bundling of add_monoid_hom.range f

Equations
source
def AddCommGroup.image.ι {G H : AddCommGroup} (f : G ⟶ H) :
AddCommGroup.image f ⟶ H

the inclusion of image f into the target

Equations
Instances for AddCommGroup.image.ι
source
@[protected, instance]
def AddCommGroup.image.ι.category_theory.mono {G H : AddCommGroup} (f : G ⟶ H) :
category_theory.mono (AddCommGroup.image.ι f)
source
def AddCommGroup.factor_thru_image {G H : AddCommGroup} (f : G ⟶ H) :
G ⟶ AddCommGroup.image f

the corestriction map to the image

Equations
source
theorem AddCommGroup.image.fac {G H : AddCommGroup} (f : G ⟶ H) :
AddCommGroup.factor_thru_image f ≫ AddCommGroup.image.ι f = f
source
noncomputable def AddCommGroup.image.lift {G H : AddCommGroup} {f : G ⟶ H} (F' : category_theory.limits.mono_factorisation f) :
AddCommGroup.image f ⟶ F'.I

the universal property for the image factorisation

Equations
source
theorem AddCommGroup.image.lift_fac {G H : AddCommGroup} {f : G ⟶ H} (F' : category_theory.limits.mono_factorisation f) :
AddCommGroup.image.lift F' ≫ F'.m = AddCommGroup.image.ι f
source
def AddCommGroup.mono_factorisation {G H : AddCommGroup} (f : G ⟶ H) :
category_theory.limits.mono_factorisation f

the factorisation of any morphism in AddCommGroup through a mono.

Equations
source
noncomputable def AddCommGroup.is_image {G H : AddCommGroup} (f : G ⟶ H) :
category_theory.limits.is_image (AddCommGroup.mono_factorisation f)

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

Equations
source
noncomputable def AddCommGroup.image_iso_range {G H : AddCommGroup} (f : G ⟶ H) :
category_theory.limits.image f ≅ AddCommGroup.of ↥(add_monoid_hom.range f)

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

Equations