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

def ModuleCat.kernelCone {R : Type u} [Ring R] {M N : ModuleCat R} (f : M ⟶ N) : CategoryTheory.Limits.KernelFork f

The kernel cone induced by the concrete kernel.

Equations

• ModuleCat.kernelCone f = CategoryTheory.Limits.KernelFork.ofι (ModuleCat.ofHom (ModuleCat.Hom.hom f).ker.subtype) ⋯

def ModuleCat.kernelIsLimit {R : Type u} [Ring R] {M N : ModuleCat R} (f : M ⟶ N) : CategoryTheory.Limits.IsLimit (kernelCone f)

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

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ModuleCat.isLimitKernelFork {R : Type u} [Ring R] {M N P : ModuleCat R} (f : M ⟶ N) (g : N ⟶ P) (H : Function.Exact ⇑(Hom.hom f) ⇑(Hom.hom g)) (H₂ : Function.Injective ⇑(Hom.hom f)) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι f ⋯)

Construct an IsLimit structure of kernels given Function.Exact.

Equations

• One or more equations did not get rendered due to their size.

def ModuleCat.cokernelCocone {R : Type u} [Ring R] {M N : ModuleCat R} (f : M ⟶ N) : CategoryTheory.Limits.CokernelCofork f

The cokernel cocone induced by the projection onto the quotient.

Equations

• ModuleCat.cokernelCocone f = CategoryTheory.Limits.CokernelCofork.ofπ (ModuleCat.ofHom (ModuleCat.Hom.hom f).range.mkQ) ⋯

def ModuleCat.cokernelIsColimit {R : Type u} [Ring R] {M N : ModuleCat R} (f : M ⟶ N) : CategoryTheory.Limits.IsColimit (cokernelCocone f)

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

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ModuleCat.isColimitCokernelCofork {R : Type u} [Ring R] {M N P : ModuleCat R} (f : M ⟶ N) (g : N ⟶ P) (H : Function.Exact ⇑(Hom.hom f) ⇑(Hom.hom g)) (H₂ : Function.Surjective ⇑(Hom.hom g)) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ g ⋯)

Construct an IsColimit structure of cokernels given Function.Exact.

Equations

• One or more equations did not get rendered due to their size.

theorem ModuleCat.hasKernels_moduleCat {R : Type u} [Ring R] : CategoryTheory.Limits.HasKernels (ModuleCat R)

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

theorem ModuleCat.hasCokernels_moduleCat {R : Type u} [Ring R] : CategoryTheory.Limits.HasCokernels (ModuleCat R)

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

noncomputable def ModuleCat.kernelIsoKer {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) : CategoryTheory.Limits.kernel f ≅ of R ↥(Hom.hom f).ker

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

Equations

• ModuleCat.kernelIsoKer f = CategoryTheory.Limits.limit.isoLimitCone { cone := ModuleCat.kernelCone f, isLimit := ModuleCat.kernelIsLimit f }

@[simp]

theorem ModuleCat.kernelIsoKer_inv_kernel_ι {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (kernelIsoKer f).inv (CategoryTheory.Limits.kernel.ι f) = ofHom (Hom.hom f).ker.subtype

theorem ModuleCat.kernelIsoKer_inv_kernel_ι_apply {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) (x : ↥(Hom.hom f).ker) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernel.ι f)) ((CategoryTheory.ConcreteCategory.hom (kernelIsoKer f).inv) x) = ↑x

@[simp]

theorem ModuleCat.kernelIsoKer_hom_ker_subtype {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (kernelIsoKer f).hom (ofHom (Hom.hom f).ker.subtype) = CategoryTheory.Limits.kernel.ι f

theorem ModuleCat.kernelIsoKer_hom_ker_subtype_apply {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) (x : ↑(CategoryTheory.Limits.kernel f)) : ↑((CategoryTheory.ConcreteCategory.hom (kernelIsoKer f).hom) x) = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernel.ι f)) x

noncomputable def ModuleCat.cokernelIsoRangeQuotient {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) : CategoryTheory.Limits.cokernel f ≅ of R (↑H ⧸ (Hom.hom f).range)

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

Equations

• ModuleCat.cokernelIsoRangeQuotient f = CategoryTheory.Limits.colimit.isoColimitCocone { cocone := ModuleCat.cokernelCocone f, isColimit := ModuleCat.cokernelIsColimit f }

@[simp]

theorem ModuleCat.cokernel_π_cokernelIsoRangeQuotient_hom {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f) (cokernelIsoRangeQuotient f).hom = ofHom (Hom.hom f).range.mkQ

theorem ModuleCat.cokernel_π_cokernelIsoRangeQuotient_hom_apply {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) (x : ↑H) : (CategoryTheory.ConcreteCategory.hom (cokernelIsoRangeQuotient f).hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.cokernel.π f)) x) = Submodule.Quotient.mk x

@[simp]

theorem ModuleCat.range_mkQ_cokernelIsoRangeQuotient_inv {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (ofHom (Hom.hom f).range.mkQ) (cokernelIsoRangeQuotient f).inv = CategoryTheory.Limits.cokernel.π f

theorem ModuleCat.range_mkQ_cokernelIsoRangeQuotient_inv_apply {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) (x : ↑H) : (CategoryTheory.ConcreteCategory.hom (cokernelIsoRangeQuotient f).inv) (Submodule.Quotient.mk x) = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.cokernel.π f)) x

theorem ModuleCat.cokernel_π_ext {R : Type u} [Ring R] {M N : ModuleCat R} (f : M ⟶ N) {x y : ↑N} (m : ↑M) (w : x = y + (CategoryTheory.ConcreteCategory.hom f) m) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.cokernel.π f)) x = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.cokernel.π f)) y