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) : CategoryTheory.Subobject M ≃o Submodule R ↑M

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.

instance ModuleCat.wellPowered_moduleCat {R : Type u} [Ring R] : CategoryTheory.WellPowered (ModuleCat R)

Equations

• ⋯ = ⋯

noncomputable def ModuleCat.toKernelSubobject {R : Type u} [Ring R] {M N : ModuleCat R} {f : M ⟶ N} : ↥(LinearMap.ker f) →ₗ[R] ↑(CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject f))

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

Equations

• ModuleCat.toKernelSubobject = (CategoryTheory.Limits.kernelSubobjectIso f ≪≫ ModuleCat.kernelIsoKer f).inv

@[simp]

theorem ModuleCat.toKernelSubobject_arrow {R : Type u} [Ring R] {M N : ModuleCat R} {f : M ⟶ N} (x : ↥(LinearMap.ker f)) : (CategoryTheory.Limits.kernelSubobject f).arrow (ModuleCat.toKernelSubobject x) = ↑x

theorem ModuleCat.cokernel_π_imageSubobject_ext {R : Type u} [Ring R] {L M N : ModuleCat R} (f : L ⟶ M) [CategoryTheory.Limits.HasImage f] (g : CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f) ⟶ N) [CategoryTheory.Limits.HasCokernel g] {x y : ↑N} (l : ↑L) (w : x = y + g ((CategoryTheory.Limits.factorThruImageSubobject f) l)) : (CategoryTheory.Limits.cokernel.π g) x = (CategoryTheory.Limits.cokernel.π g) 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.