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.

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