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

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
@[instance]
def Module.well_powered_Module {R : Type u} [ring R] :