# mathlibdocumentation

algebra.category.Module.subobject

# Subobjects in the category of R-modules #

We construct an explicit order isomorphism between the categorical subobjects of an R-module M and its submodules. This immediately implies that the category of R-modules is well-powered.

noncomputable def Module.subobject_Module {R : Type u} [ring R] (M : Module R) :

The categorical subobjects of a module M are in one-to-one correspondence with its submodules.

Equations
@[protected, instance]
def Module.well_powered_Module {R : Type u} [ring R] :
noncomputable def Module.to_kernel_subobject {R : Type u} [ring R] {M N : Module R} {f : M N} :

Bundle an element m : M such that f m = 0 as a term of kernel_subobject f.

Equations
@[simp]
theorem Module.to_kernel_subobject_arrow {R : Type u} [ring R] {M N : Module R} {f : M N} (x : ) :
@[ext]
theorem Module.cokernel_π_image_subobject_ext {R : Type u} [ring R] {L M N : Module R} (f : L M) (g : N) {x y : N} (l : L) (w : x = ) :

An extensionality lemma showing that two elements of a cokernel by an image are equal if they differ by an element of the image.

The application is for homology: two elements in homology are equal if they differ by a boundary.