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

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

The kernel cone induced by the concrete kernel.

Equations

• AddCommGroupCat.kernelCone f = CategoryTheory.Limits.KernelFork.ofι (AddMonoidHom.ker f).subtype ⋯

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

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

Equations

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

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

The cokernel cocone induced by the projection onto the quotient.

Equations

• AddCommGroupCat.cokernelCocone f = CategoryTheory.Limits.CokernelCofork.ofπ (QuotientAddGroup.mk' (AddMonoidHom.range f)) ⋯

def AddCommGroupCat.cokernelIsColimit {G : AddCommGroupCat} {H : AddCommGroupCat} (f : G ⟶ H) : CategoryTheory.Limits.IsColimit (AddCommGroupCat.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.