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

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

The kernel cone induced by the concrete kernel.

Equations

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

def AddCommGrp.kernelIsLimit {G : AddCommGrp} {H : AddCommGrp} (f : G ⟶ H) : CategoryTheory.Limits.IsLimit (AddCommGrp.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 AddCommGrp.cokernelCocone {G : AddCommGrp} {H : AddCommGrp} (f : G ⟶ H) : CategoryTheory.Limits.CokernelCofork f

The cokernel cocone induced by the projection onto the quotient.

Equations

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

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