Subobjects in the category of
We construct an explicit order isomorphism between the categorical subobjects of an
and its submodules. This immediately implies that the category of
R-modules is well-powered.
The categorical subobjects of a module
M are in one-to-one correspondence with its
Bundle an element
m : M such that
f m = 0 as a term of
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.