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.

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

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

Equations

• AddCommGroupCat.image f = AddCommGroupCat.of ↥(AddMonoidHom.range f)

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

the inclusion of image f into the target

Equations

• AddCommGroupCat.image.ι f = AddSubgroup.subtype (AddMonoidHom.range f)

instance AddCommGroupCat.instMonoAddCommGroupCatInstAddCommGroupCatLargeCategoryImageι {G : AddCommGroupCat} {H : AddCommGroupCat} (f : G ⟶ H) : CategoryTheory.Mono (AddCommGroupCat.image.ι f)

Equations

• ⋯ = ⋯

def AddCommGroupCat.factorThruImage {G : AddCommGroupCat} {H : AddCommGroupCat} (f : G ⟶ H) : G ⟶ AddCommGroupCat.image f

the corestriction map to the image

Equations

• AddCommGroupCat.factorThruImage f = AddMonoidHom.rangeRestrict f

theorem AddCommGroupCat.image.fac {G : AddCommGroupCat} {H : AddCommGroupCat} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (AddCommGroupCat.factorThruImage f) (AddCommGroupCat.image.ι f) = f

noncomputable def AddCommGroupCat.image.lift {G : AddCommGroupCat} {H : AddCommGroupCat} {f : G ⟶ H} (F' : CategoryTheory.Limits.MonoFactorisation f) : AddCommGroupCat.image f ⟶ F'.I

the universal property for the image factorisation

Equations

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

theorem AddCommGroupCat.image.lift_fac {G : AddCommGroupCat} {H : AddCommGroupCat} {f : G ⟶ H} (F' : CategoryTheory.Limits.MonoFactorisation f) : CategoryTheory.CategoryStruct.comp (AddCommGroupCat.image.lift F') F'.m = AddCommGroupCat.image.ι f

def AddCommGroupCat.monoFactorisation {G : AddCommGroupCat} {H : AddCommGroupCat} (f : G ⟶ H) : CategoryTheory.Limits.MonoFactorisation f

the factorisation of any morphism in AddCommGroupCat through a mono.

Equations

• AddCommGroupCat.monoFactorisation f = CategoryTheory.Limits.MonoFactorisation.mk (AddCommGroupCat.image f) (AddCommGroupCat.image.ι f) (AddCommGroupCat.factorThruImage f) ⋯

noncomputable def AddCommGroupCat.isImage {G : AddCommGroupCat} {H : AddCommGroupCat} (f : G ⟶ H) : CategoryTheory.Limits.IsImage (AddCommGroupCat.monoFactorisation f)

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

Equations

• AddCommGroupCat.isImage f = { lift := AddCommGroupCat.image.lift, lift_fac := ⋯ }

noncomputable def AddCommGroupCat.imageIsoRange {G : AddCommGroupCat} {H : AddCommGroupCat} (f : G ⟶ H) : CategoryTheory.Limits.image f ≅ AddCommGroupCat.of ↥(AddMonoidHom.range f)

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

Equations

• AddCommGroupCat.imageIsoRange f = CategoryTheory.Limits.IsImage.isoExt (CategoryTheory.Limits.Image.isImage f) (AddCommGroupCat.isImage f)