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

AddCommGroup.image f = AddCommGroup.of ↥(add_monoid_hom.range f)

source

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

AddCommGroup.image f ⟶ H

the inclusion of image f into the target

Equations

AddCommGroup.image.ι f = (add_monoid_hom.range f).subtype

source

@[instance]

def AddCommGroup.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

AddCommGroup.factor_thru_image f = add_monoid_hom.to_range f

source

theorem AddCommGroup.image.fac {G H : AddCommGroup} (f : G ⟶ H) :

AddCommGroup.factor_thru_image f ≫ AddCommGroup.image.ι f = f

source

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

AddCommGroup.image.lift F' = {to_fun := λ (x : ↥(AddCommGroup.image f)), ⇑(F'.e) (classical.indefinite_description (λ (y : ↥G), ⇑f y = x.val) _).val, map_zero' := _, map_add' := _}

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

AddCommGroup.mono_factorisation f = {I := AddCommGroup.image f, m := AddCommGroup.image.ι f, m_mono := _, e := AddCommGroup.factor_thru_image f, fac' := _}

source

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

AddCommGroup.is_image f = {lift := AddCommGroup.image.lift f, lift_fac' := _}

source

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

AddCommGroup.image_iso_range f = (category_theory.limits.image.is_image f).iso_ext (AddCommGroup.is_image f)