# mathlibdocumentation

algebra.category.Module.images

# The category of R-modules 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 Module R is an abelian category.

def Module.image {R : Type u} [comm_ring R] {G H : Module R} (f : G H) :

The image of a morphism in Module R is just the bundling of linear_map.range f

Equations
def Module.image.ι {R : Type u} [comm_ring R] {G H : Module R} (f : G H) :

The inclusion of image f into the target

Equations
Instances for Module.image.ι
@[protected, instance]
def Module.image.ι.category_theory.mono {R : Type u} [comm_ring R] {G H : Module R} (f : G H) :
def Module.factor_thru_image {R : Type u} [comm_ring R] {G H : Module R} (f : G H) :

The corestriction map to the image

Equations
theorem Module.image.fac {R : Type u} [comm_ring R] {G H : Module R} (f : G H) :
noncomputable def Module.image.lift {R : Type u} [comm_ring R] {G H : Module R} {f : G H}  :
F'.I

The universal property for the image factorisation

Equations
theorem Module.image.lift_fac {R : Type u} [comm_ring R] {G H : Module R} {f : G H}  :
F'.m =
def Module.mono_factorisation {R : Type u} [comm_ring R] {G H : Module R} (f : G H) :

The factorisation of any morphism in Module R through a mono.

Equations
noncomputable def Module.is_image {R : Type u} [comm_ring R] {G H : Module R} (f : G H) :

The factorisation of any morphism in Module R through a mono has the universal property of the image.

Equations
noncomputable def Module.image_iso_range {R : Type u} [comm_ring R] {G H : Module R} (f : G H) :

The categorical image of a morphism in Module R agrees with the linear algebraic range.

Equations
@[simp]
theorem Module.image_iso_range_inv_image_ι {R : Type u} [comm_ring R] {G H : Module R} (f : G H) :
@[simp]
theorem Module.image_iso_range_inv_image_ι_apply {R : Type u} [comm_ring R] {G H : Module R} (f : G H) (x : (linear_map.range f))) :
(.inv) x) =
@[simp]
theorem Module.image_iso_range_inv_image_ι_assoc {R : Type u} [comm_ring R] {G H : Module R} (f : G H) {X' : Module R} (f' : H X') :
@[simp]
theorem Module.image_iso_range_hom_subtype {R : Type u} [comm_ring R] {G H : Module R} (f : G H) :
@[simp]
theorem Module.image_iso_range_hom_subtype_assoc {R : Type u} [comm_ring R] {G H : Module R} (f : G H) {X' : Module R} (f' : H X') :
@[simp]
theorem Module.image_iso_range_hom_subtype_apply {R : Type u} [comm_ring R] {G H : Module R} (f : G H) (x : ) :
(.hom) x) =