mathlib3 documentation

algebra.category.Module.kernels

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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

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

Equations
theorem Module.cokernel_π_ext {R : Type u} [ring R] {M N : Module R} (f : M N) {x y : N} (m : M) (w : x = y + f m) :