Documentation

Mathlib.Algebra.Category.ModuleCat.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 ModuleCat.subobjectModule {R : Type u} [Ring R] (M : ModuleCat R) :

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    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.