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.
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.