The category of commutative additive groups has images.
the image of a morphism in AddCommGroup is just the bundling of add_monoid_hom.range f
Equations
the inclusion of image f into the target
Equations
@[instance]
Equations
- _ = _
the corestriction map to the image
Equations
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
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
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' := _}
@[instance]
Equations
- AddCommGroup.category_theory.limits.has_image f = {F := AddCommGroup.mono_factorisation f, is_image := {lift := AddCommGroup.image.lift f, lift_fac' := _}}
@[instance]
Equations
- AddCommGroup.category_theory.limits.has_images = {has_image := infer_instance (λ {X Y : AddCommGroup} (f : X ⟶ Y), AddCommGroup.category_theory.limits.has_image f)}
@[instance]
Equations
- AddCommGroup.category_theory.limits.has_image_maps = {has_image_map := λ (f g : category_theory.arrow AddCommGroup) (st : f ⟶ g), {map := {to_fun := category_theory.limits.image.map ((category_theory.forget AddCommGroup).map_arrow.map st) (category_theory.limits.has_image_maps.has_image_map ((category_theory.forget AddCommGroup).map_arrow.map st)), map_zero' := _, map_add' := _}, map_ι' := _}}
@[simp]
theorem
AddCommGroup.image_map
{f g : category_theory.arrow AddCommGroup}
(st : f ⟶ g)
(x : ↥(AddCommGroup.image f.hom)) :
The categorical image of a morphism in AddCommGroup
agrees with the usual group-theoretical range.