module Cat.Abelian.Limits {o β„“} {C : Precategory o β„“} where


Recall that every pre-abelian category admits kernels and cokernels, and is also additive, so it additionally has products and coproducts1. It sounds like we’re missing some finite limits (dually, missing some finite colimits), but it turns out that this is enough: We can construct the equaliser of f,g:Aβ†’Bf, g : A \to B as ker⁑(fβˆ’g)\ker(f - g) β€” whence the name difference kernel!

The calculation is straightforward: To map out of ker⁑f\ker f, we must have (feβ€²βˆ’geβ€²)=0(fe' - ge') = 0, but this is immediate assuming that feβ€²=geβ€²fe' = ge' β€” an assumption we have to map out of eq(f,g)\id{eq}(f,g). Similarly, to show that fker⁑(fβˆ’g)=gker⁑(fβˆ’g)f\ker(f-g) = g\ker(f-g), we calculate

fker⁑(fβˆ’g)βˆ’gker⁑(fβˆ’g)=(fβˆ’g)ker⁑(fβˆ’g)=0. f\ker(f-g) - g\ker(f-g) = (f-g)\ker(f-g) = 0\text{.}

module _ (A : is-pre-abelian C) where
  open is-pre-abelian A
    : βˆ€ {A B} {f g : Hom A B}
    β†’ is-equaliser f g (Ker.kernel (f - g))
  difference-kernel {f = f} {g} = equ where
    open is-equaliser
    equ : is-equaliser f g (Ker.kernel (f - g))
    equ .equal = zero-diff $
      (f ∘ Ker.kernel (f - g)) - (g ∘ Ker.kernel (f - g)) β‰‘βŸ¨ ∘-minus-l f g (Ker.kernel (f - g)) βŸ©β‰‘
      (f - g) ∘ Ker.kernel (f - g)                        β‰‘βŸ¨ Ker.equal (f - g) βŸ©β‰‘
      βˆ….zeroβ†’ ∘ Ker.kernel (f - g)                        β‰‘βŸ¨ βˆ….zero-∘r _ βˆ™ 0m-unique βŸ©β‰‘
      0m                                                  ∎
    equ .limiting {eβ€² = eβ€²} p = Ker.limiting (f - g) {eβ€² = eβ€²} $
      (f - g) ∘ eβ€²         β‰‘Λ˜βŸ¨ ∘-minus-l _ _ _ βŸ©β‰‘Λ˜
      f ∘ eβ€² - g ∘ eβ€²      β‰‘βŸ¨ ap (f ∘ eβ€² -_) (sym p) βŸ©β‰‘
      f ∘ eβ€² - f ∘ eβ€²      β‰‘βŸ¨ Hom.inverser βŸ©β‰‘
      0m                   β‰‘Λ˜βŸ¨ βˆ….zero-∘r _ βˆ™ 0m-unique βŸ©β‰‘Λ˜
      Zero.zeroβ†’ βˆ… ∘ eβ€²    ∎
    equ .universal = Ker.universal _
    equ .unique = Ker.unique (f - g)

By a standard characterisation of finite limits in terms of finite products and binary equalisers, the construction of β€œdifference kernels” above implies that any pre-abelian category is finitely complete.

  finitely-complete : Finitely-complete C
  finitely-complete =
    with-equalisers C has-terminal has-prods Ξ» f g β†’
      record { has-is-eq = difference-kernel }

  1. actually, they’re the same thing!β†©οΈŽ