open import Cat.Prelude

import Cat.Diagram.Equaliser
import Cat.Diagram.Zero

module Cat.Diagram.Equaliser.Kernel {o } (C : Precategory o ) where


In a category with equalisers and a zero object 00, a kernel of a morphism f:abf : a \to b is an equaliser of ff and the zero morphism 0:ab0 : a \to b, hence a subobject ker(f)a\mathrm{ker}(f) \mono a of the domain of ff.

module _ ( : Zero) where
  open Zero 

  is-kernel :  {a b ker} (f : Hom a b) (k : Hom ker a)  Type _
  is-kernel f = is-equaliser f zero→

    :  {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
      {ker} : Ob
      kernel : Hom ker a
      has-is-kernel : is-kernel f kernel
    open is-equaliser has-is-kernel public

Lemma: Let C\ca{C} 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) (eqs :  {a b} (f g : Hom a b)  Equaliser 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 !:kerkerf! : \ker\ker f \to \emptyset and ¡:kerkerf¡ : \emptyset \to \ker\ker f are inverses. In one direction the composite is in \emptyset \to \emptyset, so it is trivally unique. In the other direction, we have maps kerkerfkerkerf\ker\ker f \to \ker\ker f, which, since ker\ker 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 kerfkerkerf=0\ker f \circ \ker \ker f = 0 (here we are talking about the inclusion maps, not the objects) — but recall that kerkerf\ker \ker f equalises kerf\ker f and 00, so we have

kerfkerkerf=0kerkerf=0 \ker f \circ \ker \ker f = 0 \circ \ker \ker f = 0

    p : ¡  !  id
    p = KKf.unique₂ {p = zero-∘l _  sym (zero-∘r _)} (sym (zero-∘l _))
      ( Kf.unique₂  {p = zero-∘l _  sym (zero-∘r _)} (sym (zero-∘l _))
          (sym (KKf.equal  zero-∘r _))  intror refl)