open import Cat.Diagram.Equaliser
open import Cat.Diagram.Zero
open import Cat.Prelude

import Cat.Reasoning

module Cat.Diagram.Equaliser.Kernel where

module _ {o β} (C : Precategory o β) where
open Cat.Reasoning C


Kernelsπ

In a category with equalisers and a zero object a kernel of a morphism is an equaliser of and the zero morphism hence a subobject of the domain of

  module _ (β : Zero C) where
open Zero β

is-kernel : β {a b ker} (f : Hom a b) (k : Hom ker a) β Type _
is-kernel f = is-equaliser C f zeroβ

kernels-are-subobjects
: β {a b ker} {f : Hom a b} (k : Hom ker a)
β is-kernel f k β is-monic k
kernels-are-subobjects = is-equaliserβis-monic

record Kernel {a b} (f : Hom a b) : Type (o β β) where
field
{ker} : Ob
kernel : Hom ker a
has-is-kernel : is-kernel f kernel
open is-equaliser has-is-kernel public


Lemma: Let be a category with equalisers and a zero object. In the kernel of a kernel is zero. First, note that if a category has a choice of zero object and a choice of equaliser for any pair of morphisms, then it has canonically-defined choices of kernels:

  module Canonical-kernels
(zero : Zero C) (eqs : β {a b} (f g : Hom a b) β Equaliser C f g) where
open Zero zero
open Kernel

Ker : β {a b} (f : Hom a b) β Kernel zero f
Ker f .ker           = _
Ker f .kernel        = eqs f zeroβ .Equaliser.equ
Ker f .has-is-kernel = eqs _ _ .Equaliser.has-is-eq


We now show that the maps and are inverses. In one direction the composite is in so it is trivially unique. In the other direction, we have maps which, since is a limit, are uniquely determined if they are cone homomorphisms.

    Ker-of-kerββ : β {a b} (f : Hom a b) β Ker (Ker f .kernel) .ker β β
Ker-of-kerββ f = make-iso ! Β‘ (!-uniqueβ _ _) p where
module Kf = Kernel (Ker f)
module KKf = Kernel (Ker (Ker f .kernel))


The calculation is straightforward enough: The hardest part is showing that (here we are talking about the inclusion maps, not the objects) β but recall that equalises and so we have

      p : Β‘ β ! β‘ id
p = KKf.uniqueβ (zero-comm _ _) (zero-βl _)
(Kf.uniqueβ (extendl (zero-comm _ _))
(pulll KKf.equal β idr _)
(zero-comm _ _))