module Cat.Diagram.Equaliser.Kernel where


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→
      : βˆ€ {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 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 _ _))