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.
Instances For
Equations
- (_ : CategoryTheory.WellPowered (ModuleCat R)) = (_ : CategoryTheory.WellPowered (ModuleCat R))
noncomputable def
ModuleCat.toKernelSubobject
{R : Type u}
[Ring R]
{M : ModuleCat R}
{N : ModuleCat R}
{f : M ⟶ N}
:
↥(LinearMap.ker f) →ₗ[R] ↑(CategoryTheory.Subobject.underlying.toPrefunctor.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
Instances For
@[simp]
theorem
ModuleCat.toKernelSubobject_arrow
{R : Type u}
[Ring R]
{M : ModuleCat R}
{N : ModuleCat R}
{f : M ⟶ N}
(x : ↥(LinearMap.ker f))
:
(CategoryTheory.Subobject.arrow (CategoryTheory.Limits.kernelSubobject f)) (ModuleCat.toKernelSubobject x) = ↑x
theorem
ModuleCat.cokernel_π_imageSubobject_ext
{R : Type u}
[Ring R]
{L : ModuleCat R}
{M : ModuleCat R}
{N : ModuleCat R}
(f : L ⟶ M)
[CategoryTheory.Limits.HasImage f]
(g : CategoryTheory.Subobject.underlying.toPrefunctor.obj (CategoryTheory.Limits.imageSubobject f) ⟶ N)
[CategoryTheory.Limits.HasCokernel g]
{x : ↑N}
{y : ↑N}
(l : ↑L)
(w : x = y + g ((CategoryTheory.Limits.factorThruImageSubobject f) l))
:
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.