# mathlibdocumentation

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
def Module.kernel_is_limit {R : Type u} [ring R] {M N : Module R} (f : M N) :

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

Equations
• = (λ (s : , _) _ _
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
def Module.cokernel_is_colimit {R : Type u} [ring R] {M N : Module R} (f : M N) :

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

Equations
• = (λ (s : , s.π _) _ _
theorem Module.has_kernels_Module {R : Type u} [ring R] :

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

theorem Module.has_cokernels_Module {R : Type u} [ring R] :

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
@[simp]
theorem Module.kernel_iso_ker_inv_kernel_ι_apply {R : Type u} [ring R] {G H : Module R} (f : G H) (x : (linear_map.ker f))) :
@[simp]
theorem Module.kernel_iso_ker_inv_kernel_ι {R : Type u} [ring R] {G H : Module R} (f : G H) :
@[simp]
theorem Module.kernel_iso_ker_hom_ker_subtype {R : Type u} [ring R] {G H : Module R} (f : G H) :
@[simp]
theorem Module.kernel_iso_ker_hom_ker_subtype_apply {R : Type u} [ring R] {G H : Module R} (f : G H) (x : ) :
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
@[simp]
theorem Module.cokernel_π_cokernel_iso_range_quotient_hom {R : Type u} [ring R] {G H : Module R} (f : G H) :
@[simp]
theorem Module.cokernel_π_cokernel_iso_range_quotient_hom_apply {R : Type u} [ring R] {G H : Module R} (f : G H) (x : H) :
@[simp]
theorem Module.range_mkq_cokernel_iso_range_quotient_inv {R : Type u} [ring R] {G H : Module R} (f : G H) :
@[simp]
theorem Module.range_mkq_cokernel_iso_range_quotient_inv_apply {R : Type u} [ring R] {G H : Module R} (f : G H) (x : H) :
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) :