# 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 : ) :

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

Instances For
noncomputable def ModuleCat.toKernelSubobject {R : Type u} [Ring R] {M : } {N : } {f : M N} :
{ x // } →ₗ[R] ↑(CategoryTheory.Subobject.underlying.obj ())

Bundle an element m : M such that f m = 0 as a term of kernelSubobject f.

Instances For
@[simp]
theorem ModuleCat.toKernelSubobject_arrow {R : Type u} [Ring R] {M : } {N : } {f : M N} (x : { x // }) :
↑() (ModuleCat.toKernelSubobject x) = x
theorem ModuleCat.cokernel_π_imageSubobject_ext {R : Type u} [Ring R] {L : } {M : } {N : } (f : L M) (g : CategoryTheory.Subobject.underlying.obj () N) {x : N} {y : N} (l : L) (w : x = y + ) :

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.