mathlib documentation

algebra.category.Module.kernels

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

def Module.kernel_cone {R : Type u} [ring R] {M N : Module R} (f : M N) :

The kernel cone induced by the concrete kernel.

Equations

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

Equations
def Module.cokernel_cocone {R : Type u} [ring R] {M N : Module R} (f : M N) :

The cokernel cocone induced by the projection onto the quotient.

Equations

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

Equations

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

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

noncomputable def Module.kernel_iso_ker {R : Type u} [ring R] {G H : Module R} (f : G H) :

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

Equations
noncomputable def Module.cokernel_iso_range_quotient {R : Type u} [ring R] {G H : Module R} (f : G H) :

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

Equations