mathlib3 documentation

algebra.category.Module.images

The category of R-modules has images. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.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' : category_theory.limits.mono_factorisation f) :

The universal property for the image factorisation

Equations

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