(Co)kernels in functor categories #
noncomputable def
CategoryTheory.Limits.kerIsKernel
(C : Type u_1)
[Category.{u, u_1} C]
[HasZeroMorphisms C]
[HasKernels C]
:
IsLimit (KernelFork.ofι (ker.ι C) ⋯)
The kernel inclusion is itself a kernel in the functor category.
Equations
Instances For
noncomputable def
CategoryTheory.Limits.cokerIsCokernel
(C : Type u_1)
[Category.{u, u_1} C]
[HasZeroMorphisms C]
[HasCokernels C]
:
IsColimit (CokernelCofork.ofπ (coker.π C) ⋯)
The cokernel projection is itself a cokernel in the functor category.