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.

source
def Module.kernel_cone {R : Type u} [ring R] {M N : Module R} (f : M ⟶ N) :
category_theory.limits.kernel_fork f

The kernel cone induced by the concrete kernel.

Equations
source
def Module.kernel_is_limit {R : Type u} [ring R] {M N : Module R} (f : M ⟶ N) :
category_theory.limits.is_limit (Module.kernel_cone f)

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

Equations
source
def Module.cokernel_cocone {R : Type u} [ring R] {M N : Module R} (f : M ⟶ N) :
category_theory.limits.cokernel_cofork f

The cokernel cocone induced by the projection onto the quotient.

Equations
source
def Module.cokernel_is_colimit {R : Type u} [ring R] {M N : Module R} (f : M ⟶ N) :
category_theory.limits.is_colimit (Module.cokernel_cocone f)

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

Equations
source
theorem Module.has_kernels_Module {R : Type u} [ring R] :
category_theory.limits.has_kernels (Module R)

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

source
theorem Module.has_cokernels_Module {R : Type u} [ring R] :
category_theory.limits.has_cokernels (Module R)

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

source
noncomputable def Module.kernel_iso_ker {R : Type u} [ring R] {G H : Module R} (f : G ⟶ H) :
category_theory.limits.kernel f ≅ Module.of R ↥(linear_map.ker f)

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

Equations
source
@[simp]
theorem Module.kernel_iso_ker_inv_kernel_ι_apply {R : Type u} [ring R] {G H : Module R} (f : G ⟶ H) (x : ↥(Module.of R ↥(linear_map.ker f))) :
⇑(category_theory.limits.kernel.ι f) (⇑((Module.kernel_iso_ker f).inv) x) = ⇑((linear_map.ker f).subtype) x
source
@[simp]
theorem Module.kernel_iso_ker_inv_kernel_ι {R : Type u} [ring R] {G H : Module R} (f : G ⟶ H) :
(Module.kernel_iso_ker f).inv ≫ category_theory.limits.kernel.ι f = (linear_map.ker f).subtype
source
@[simp]
theorem Module.kernel_iso_ker_hom_ker_subtype {R : Type u} [ring R] {G H : Module R} (f : G ⟶ H) :
(Module.kernel_iso_ker f).hom ≫ (linear_map.ker f).subtype = category_theory.limits.kernel.ι f
source
@[simp]
theorem Module.kernel_iso_ker_hom_ker_subtype_apply {R : Type u} [ring R] {G H : Module R} (f : G ⟶ H) (x : ↥(category_theory.limits.kernel f)) :
⇑((linear_map.ker f).subtype) (⇑((Module.kernel_iso_ker f).hom) x) = ⇑(category_theory.limits.kernel.ι f) x
source
noncomputable def Module.cokernel_iso_range_quotient {R : Type u} [ring R] {G H : Module R} (f : G ⟶ H) :
category_theory.limits.cokernel f ≅ Module.of R (↥H ⧸ linear_map.range f)

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

Equations
source
@[simp]
theorem Module.cokernel_π_cokernel_iso_range_quotient_hom {R : Type u} [ring R] {G H : Module R} (f : G ⟶ H) :
category_theory.limits.cokernel.π f ≫ (Module.cokernel_iso_range_quotient f).hom = (linear_map.range f).mkq
source
@[simp]
theorem Module.cokernel_π_cokernel_iso_range_quotient_hom_apply {R : Type u} [ring R] {G H : Module R} (f : G ⟶ H) (x : ↥H) :
⇑((Module.cokernel_iso_range_quotient f).hom) (⇑(category_theory.limits.cokernel.π f) x) = ⇑((linear_map.range f).mkq) x
source
@[simp]
theorem Module.range_mkq_cokernel_iso_range_quotient_inv {R : Type u} [ring R] {G H : Module R} (f : G ⟶ H) :
Module.as_hom_left (linear_map.range f).mkq ≫ (Module.cokernel_iso_range_quotient f).inv = category_theory.limits.cokernel.π f
source
@[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) :
⇑((Module.cokernel_iso_range_quotient f).inv) (⇑(Module.as_hom_left (linear_map.range f).mkq) x) = ⇑(category_theory.limits.cokernel.π f) x
source
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) :
⇑(category_theory.limits.cokernel.π f) x = ⇑(category_theory.limits.cokernel.π f) y