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 , a kernel of a morphism is an equaliser of and the zero morphism , hence a subobject of the domain of .
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 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 and are inverses. In one direction the composite is in , so it is trivally 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₂ {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)