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 $0\text{,}$ a kernel of a morphism $f:a\to b$ is an equaliser of $f$ and the zero morphism $0:a\to b\text{,}$ hence a subobject $\ker (f)\hookrightarrow a$ of the domain of $f\text{.}$

  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 $\mathcal{C}$ be a category with equalisers and a zero object. In $\mathcal{C}\text{,}$ 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 $!:\ker \ker f\to \varnothing$ and $¡:\varnothing \to \ker \ker f$ are inverses. In one direction the composite is in $\varnothing \to \varnothing \text{,}$ so it is trivially unique. In the other direction, we have maps $\ker \ker f\to \ker \ker f\text{,}$ which, since $\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 $\ker f\circ \ker \ker f=0$ (here we are talking about the inclusion maps, not the objects) — but recall that $\ker \ker f$ equalises $\ker f$ and $0\text{,}$ so we have

      p : ¡ ∘ ! ≡ id
      p = KKf.unique₂ (zero-comm _ _) (zero-∘l _)
            (Kf.unique₂ (extendl (zero-comm _ _))
                        (pulll KKf.equal ∙ idr _)
                        (zero-comm _ _))