Documentation

Mathlib.Algebra.Category.GroupCat.Kernels

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

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

The kernel cone induced by the concrete kernel.

Instances For
    source
    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.

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

      The cokernel cocone induced by the projection onto the quotient.

      Instances For
        source
        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.

        Instances For