open import Cat.Prelude

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

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


# Kernels🔗

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

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→

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 $\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 $! : \ker\ker f \to \emptyset$ and $¡ : \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 $\ker\ker f \to \ker\ker f$, 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$, so we have

$\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)