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

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

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

Equations

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

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

the inclusion of image f into the target

Equations

• AddCommGrp.image.ι f = (AddMonoidHom.range f).subtype

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

Equations

• ⋯ = ⋯

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

the corestriction map to the image

Equations

• AddCommGrp.factorThruImage f = AddMonoidHom.rangeRestrict f

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

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

the universal property for the image factorisation

Equations

• AddCommGrp.image.lift F' = { toFun := fun (x : ↑(AddCommGrp.image f)) => F'.e ↑(Classical.indefiniteDescription (fun (x_1 : ↑G) => f x_1 = ↑x) ⋯), map_zero' := ⋯, map_add' := ⋯ }

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

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

the factorisation of any morphism in AddCommGrp through a mono.

Equations

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

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

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

Equations

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

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

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

Equations

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