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.

Instances For
    noncomputable def ModuleCat.toKernelSubobject {R : Type u} [Ring R] {M : ModuleCat R} {N : ModuleCat R} {f : M N} :
    { x // x 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.

    Instances For
      @[simp]
      theorem ModuleCat.toKernelSubobject_arrow {R : Type u} [Ring R] {M : ModuleCat R} {N : ModuleCat R} {f : M N} (x : { x // 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.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.