The concrete (co)kernels in the category of abelian groups are categorical (co)kernels.

def AddCommGrp.kernelCone {G H : AddCommGrp} (f : G ⟶ H) : CategoryTheory.Limits.KernelFork f

The kernel cone induced by the concrete kernel.

def AddCommGrp.kernelIsLimit {G H : AddCommGrp} (f : G ⟶ H) : CategoryTheory.Limits.IsLimit (kernelCone f)

The kernel of a group homomorphism is a kernel in the categorical sense.

def AddCommGrp.cokernelCocone {G H : AddCommGrp} (f : G ⟶ H) : CategoryTheory.Limits.CokernelCofork f

The cokernel cocone induced by the projection onto the quotient.

def AddCommGrp.cokernelIsColimit {G H : AddCommGrp} (f : G ⟶ H) : CategoryTheory.Limits.IsColimit (cokernelCocone f)

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