The concrete (co)kernels in the category of modules are (co)kernels in the categorical sense. #
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.
theorem
ModuleCat.kernelIsoKer_inv_kernel_ι_apply
{R : Type u}
[Ring R]
{G H : ModuleCat R}
(f : G ⟶ H)
(x : CategoryTheory.ToType (of R ↥(LinearMap.ker (Hom.hom f))))
:
theorem
ModuleCat.kernelIsoKer_hom_ker_subtype_apply
{R : Type u}
[Ring R]
{G H : ModuleCat R}
(f : G ⟶ H)
(x : CategoryTheory.ToType (CategoryTheory.Limits.kernel f))
:
theorem
ModuleCat.cokernel_π_cokernelIsoRangeQuotient_hom_apply
{R : Type u}
[Ring R]
{G H : ModuleCat R}
(f : G ⟶ H)
(x : CategoryTheory.ToType H)
:
theorem
ModuleCat.range_mkQ_cokernelIsoRangeQuotient_inv_apply
{R : Type u}
[Ring R]
{G H : ModuleCat R}
(f : G ⟶ H)
(x : CategoryTheory.ToType (of R ↑H))
: