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 AddCommGrpCat is an abelian category.

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

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

Equations

• AddCommGrpCat.image f = AddCommGrpCat.of ↥(AddCommGrpCat.Hom.hom f).range

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

the inclusion of image f into the target

Equations

• AddCommGrpCat.image.ι f = AddCommGrpCat.ofHom (AddCommGrpCat.Hom.hom f).range.subtype

instance AddCommGrpCat.instMonoι {G H : AddCommGrpCat} (f : G ⟶ H) : CategoryTheory.Mono (image.ι f)

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

the corestriction map to the image

Equations

• AddCommGrpCat.factorThruImage f = AddCommGrpCat.ofHom (AddCommGrpCat.Hom.hom f).rangeRestrict

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

noncomputable def AddCommGrpCat.image.lift {G H : AddCommGrpCat} {f : G ⟶ H} (F' : CategoryTheory.Limits.MonoFactorisation f) : 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 AddCommGrpCat.image.lift_fac {G H : AddCommGrpCat} {f : G ⟶ H} (F' : CategoryTheory.Limits.MonoFactorisation f) : CategoryTheory.CategoryStruct.comp (lift F') F'.m = ι f

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

the factorisation of any morphism in AddCommGrpCat through a mono.

Equations

• AddCommGrpCat.monoFactorisation f = { I := AddCommGrpCat.image f, m := AddCommGrpCat.image.ι f, m_mono := ⋯, e := AddCommGrpCat.factorThruImage f, fac := ⋯ }

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

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

Equations

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

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

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

Equations

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