Subobjects in the category of
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
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.