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.
The kernel cone induced by the concrete kernel.
The kernel of a linear map is a kernel in the categorical sense.
The cokernel cocone induced by the projection onto the quotient.
The projection onto the quotient is a cokernel in the categorical sense.
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.
The categorical kernel of a morphism in
agrees with the usual module-theoretical kernel.
The categorical cokernel of a morphism in
agrees with the usual module-theoretical quotient.