# The concrete (co)kernels in the category of modules are (co)kernels in the categorical sense. #

def ModuleCat.kernelCone {R : Type u} [Ring R] {M : } {N : } (f : M N) :

The kernel cone induced by the concrete kernel.

Equations
Instances For
def ModuleCat.kernelIsLimit {R : Type u} [Ring R] {M : } {N : } (f : M N) :

The kernel of a linear map is a kernel in the categorical sense.

Equations
Instances For
def ModuleCat.cokernelCocone {R : Type u} [Ring R] {M : } {N : } (f : M N) :

The cokernel cocone induced by the projection onto the quotient.

Equations
Instances For
def ModuleCat.cokernelIsColimit {R : Type u} [Ring R] {M : } {N : } (f : M N) :

The projection onto the quotient is a cokernel in the categorical sense.

Equations
Instances For

The category of R-modules has kernels, given by the inclusion of the kernel submodule.

The category of R-modules has cokernels, given by the projection onto the quotient.

noncomputable def ModuleCat.kernelIsoKer {R : Type u} [Ring R] {G : } {H : } (f : G H) :

The categorical kernel of a morphism in ModuleCat agrees with the usual module-theoretical kernel.

Equations
Instances For
theorem ModuleCat.kernelIsoKer_inv_kernel_ι_apply {R : Type u} [Ring R] {G : } {H : } (f : G H) (x : .obj ()) :
(.inv x) = ().subtype x
@[simp]
theorem ModuleCat.kernelIsoKer_inv_kernel_ι {R : Type u} [Ring R] {G : } {H : } (f : G H) :
= ().subtype
theorem ModuleCat.kernelIsoKer_hom_ker_subtype_apply {R : Type u} [Ring R] {G : } {H : } (f : G H) (x : .obj ) :
().subtype (.hom x) =
@[simp]
theorem ModuleCat.kernelIsoKer_hom_ker_subtype {R : Type u} [Ring R] {G : } {H : } (f : G H) :
noncomputable def ModuleCat.cokernelIsoRangeQuotient {R : Type u} [Ring R] {G : } {H : } (f : G H) :

The categorical cokernel of a morphism in ModuleCat agrees with the usual module-theoretical quotient.

Equations
Instances For
theorem ModuleCat.cokernel_π_cokernelIsoRangeQuotient_hom_apply {R : Type u} [Ring R] {G : } {H : } (f : G H) (x : .obj H) :
= ().mkQ x
@[simp]
theorem ModuleCat.cokernel_π_cokernelIsoRangeQuotient_hom {R : Type u} [Ring R] {G : } {H : } (f : G H) :
theorem ModuleCat.range_mkQ_cokernelIsoRangeQuotient_inv_apply {R : Type u} [Ring R] {G : } {H : } (f : G H) (x : .obj H) :
(() x) =
@[simp]
theorem ModuleCat.range_mkQ_cokernelIsoRangeQuotient_inv {R : Type u} [Ring R] {G : } {H : } (f : G H) :
theorem ModuleCat.cokernel_π_ext {R : Type u} [Ring R] {M : } {N : } (f : M N) {x : N} {y : N} (m : M) (w : x = y + f m) :