The concrete (co)kernels in the category of modules are (co)kernels in the categorical sense.
The kernel cone induced by the concrete kernel.
Equations
The kernel of a linear map is a kernel in the categorical sense.
Equations
- Module.kernel_is_limit f = category_theory.limits.fork.is_limit.mk (Module.kernel_cone f) (λ (s : category_theory.limits.fork f 0), linear_map.cod_restrict (linear_map.ker f) s.ι _) _ _
The cokernel cocone induced by the projection onto the quotient.
Equations
The projection onto the quotient is a cokernel in the categorical sense.
Equations
- Module.cokernel_is_colimit f = category_theory.limits.cofork.is_colimit.mk (Module.cokernel_cocone f) (λ (s : category_theory.limits.cofork f 0), (linear_map.range f).liftq s.π _) _ _
The category of R-modules has kernels, given by the inclusion of the kernel submodule.
Equations
- Module.has_kernels_Module = {has_limit := λ (X Y : Module R) (f : X ⟶ Y), {cone := Module.kernel_cone f, is_limit := Module.kernel_is_limit f}}
The category or R-modules has cokernels, given by the projection onto the quotient.
Equations
- Module.has_cokernels_Module = {has_colimit := λ (X Y : Module R) (f : X ⟶ Y), {cocone := Module.cokernel_cocone f, is_colimit := Module.cokernel_is_colimit f}}