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
- ModuleCat.kernelCone f = CategoryTheory.Limits.KernelFork.ofι (ModuleCat.ofHom (LinearMap.ker f.hom).subtype) ⋯
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.
The cokernel cocone induced by the projection onto the quotient.
Equations
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.
The category of R-modules has kernels, given by the inclusion of the kernel submodule.
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 ↥(LinearMap.ker f.hom)
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 (LinearMap.ker f.hom).subtype
theorem
ModuleCat.kernelIsoKer_inv_kernel_ι_apply
{R : Type u}
[Ring R]
{G H : ModuleCat R}
(f : G ⟶ H)
(x : (CategoryTheory.forget (ModuleCat R)).obj (of R ↥(LinearMap.ker f.hom)))
:
(CategoryTheory.Limits.kernel.ι f) ((kernelIsoKer f).inv x) = (ofHom (LinearMap.ker f.hom).subtype) 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 (LinearMap.ker f.hom).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.forget (ModuleCat R)).obj (CategoryTheory.Limits.kernel f))
:
(ofHom (LinearMap.ker f.hom).subtype) ((kernelIsoKer f).hom x) = (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 ⧸ LinearMap.range f.hom)
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 (LinearMap.range f.hom).mkQ
theorem
ModuleCat.cokernel_π_cokernelIsoRangeQuotient_hom_apply
{R : Type u}
[Ring R]
{G H : ModuleCat R}
(f : G ⟶ H)
(x : (CategoryTheory.forget (ModuleCat R)).obj H)
:
(cokernelIsoRangeQuotient f).hom ((CategoryTheory.Limits.cokernel.π f) x) = (ofHom (LinearMap.range f.hom).mkQ) x
@[simp]
theorem
ModuleCat.range_mkQ_cokernelIsoRangeQuotient_inv
{R : Type u}
[Ring R]
{G H : ModuleCat R}
(f : G ⟶ H)
:
CategoryTheory.CategoryStruct.comp (ofHom (LinearMap.range f.hom).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 : (CategoryTheory.forget (ModuleCat R)).obj (of R ↑H))
:
(cokernelIsoRangeQuotient f).inv ((ofHom (LinearMap.range f.hom).mkQ) x) = (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 + f.hom m)
:
(CategoryTheory.Limits.cokernel.π f).hom x = (CategoryTheory.Limits.cokernel.π f).hom y