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

LimitsπŸ”—

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)\mathrm{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
  difference-kernel
    : βˆ€ {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 .universal {eβ€² = eβ€²} p = Ker.universal (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 .factors = Ker.factors _
    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 }

Finite biproductsπŸ”—

An interesting property of Ab\mathbf{Ab}-enriched categories is the coincidence of finite products and finite coproducts: not only is there a map2 aβŠ”bβ†’aΓ—ba \sqcup b \to a \times b, defined from the universal properties, but it is also an isomorphism. This is, at least to the author, mildly unexpected, but it follows from the properties of zero morphisms.

More generally, suppose that F:[n]β†’AF : [n] \to \mathcal{A} is a finite family of objects in an Ab\mathbf{Ab}-category. If FF has both a coproduct ∐F\coprod F and a product ∏F\prod F in A\mathcal{A}, then we can define a map ∐Fβ†’βˆF\coprod F \to \prod F by giving a family of morphisms Fiβ†’βˆFF_i \to \prod F, which amounts to defining a family of morphisms Fiβ†’FjF_i \to F_j3. Since [n][n] is discrete, we can define this family to be id⁑:Fiβ†’Fi\operatorname{id}_{} : F_i \to F_i when i=ji = j and 0:Fiβ†’Fj0 : F_i \to F_j everywhere else!

What we actually prove in this module is a slight variation: we directly construct, given a product ∏F\prod F, the structure of a coproduct on ∏F\prod F. Uniqueness of coproducts then implies that, if some other ∐F\coprod F exists, then it must be isomorphic to ∐F\coprod F.

The first thing we’ll prove is a compatibility condition between tupling and sums: A sum of tuples is a tuple of sums. In the binary case, we’re showing that (a,b)+(c,d)(a, b) + (c, d) is (a+c,b+d)(a + c, b + d).

  tuple-sum : βˆ€ {j} {R} (f : Fin j β†’ βˆ€ i β†’ A.Hom R (F i))
        β†’ ip.tuple (Ξ» i β†’ βˆ‘β‚• j (Ξ» j β†’ f j i))
        ≑ βˆ‘β‚• j Ξ» j β†’ ip.tuple (f j)
  tuple-sum {j} f = sym $ ip.unique _ Ξ» i β†’
    ip.Ο€ i A.∘ βˆ‘β‚• j (Ξ» i β†’ ip.tuple (f i))   β‰‘βŸ¨ βˆ‘-∘-left {j = j} _ βŸ©β‰‘
    βˆ‘β‚• j (Ξ» j β†’ ip.Ο€ i A.∘ ip.tuple (f j))   β‰‘βŸ¨ βˆ‘-path {j} _ (Ξ» j β†’ ip.commute) βŸ©β‰‘
    βˆ‘β‚• j (Ξ» j β†’ f j i)                       ∎

We then define our function δi,j:Fi→Fj\delta_{i,j} : F_i \to F_j which is the identity on the diagonal.

  private
    Ξ΄β€² : (i j : Fin I) β†’ Dec (i ≑ᡒ j) β†’ A.Hom (F i) (F j)
    Ξ΄β€² i j (yes reflα΅’) = A.id
    Ξ΄β€² i j (no x) = A.0m

    Ξ΄ : βˆ€ i j β†’ A.Hom (F i) (F j)
    Ξ΄ i j = Ξ΄β€² i j (Discreteα΅’-Fin i j)

    Ξ΄α΅’α΅’ : βˆ€ i d β†’ Ξ΄β€² i i d ≑ A.id
    Ξ΄α΅’α΅’ i (yes x) = ap (Ξ΄β€² i i) $
      ap yes (is-set→is-setᡒ Fin-is-set i i x reflᡒ)
    Ξ΄α΅’α΅’ i (no Β¬x=x) = absurd (Β¬x=x reflα΅’)

    Ξ΄α΅’β±Ό : βˆ€ i j β†’ Β¬ i ≑ j β†’ (d : Dec (i ≑ᡒ j)) β†’ Ξ΄β€² i j d ≑ A.0m
    Ξ΄α΅’β±Ό i j iβ‰ j (yes i=j) = absurd (iβ‰ j (Id≃path.to i=j))
    δᡒⱼ i j i≠j (no _)    = refl

We can now define a factoring of the identity on ∏F\prod F through a β€” hypothetical β€” ∐F\coprod F. A β€œsplitting” map ∏Fβ†’βˆF\prod F \to \prod F, which works by summing (over jj) the tupling (over ii) of Ξ΄i,jΟ€j\delta_{i,j}\pi_j; and since tupling commutes with sums, we conclude that this is the tupling over ii of a bunch of tuples, zero on every component except for the one corresponding to their index in the sum. In the binary case, we’re showing that

(1,0)Ο€1+(0,1)Ο€2=(Ο€1,0)+(0,Ο€2)=(Ο€1,Ο€2)=id⁑. (1, 0)\pi_1 + (0,1)\pi_2 = (\pi_1, 0) + (0, \pi_2) = (\pi_1, \pi_2) = \operatorname{id}_{}\text{.}

  split = βˆ‘β‚• I Ξ» j β†’ ip.tuple Ξ» i β†’ Ξ΄ j i A.∘ ip.Ο€ j

  private
    split-remark : A.id ≑ split
    split-remark = ip.unique ip.Ο€ (Ξ» _ β†’ A.idr _) βˆ™ sym (ip.unique _ πΣδπ) where
      sum-Ξ΄-Ο€ : βˆ€ i β†’ βˆ‘ {I} _ (Ξ» j β†’ Ξ΄ j i A.∘ ip.Ο€ j) ≑ ip.Ο€ i
      sum-Ξ΄-Ο€ i = βˆ‘-diagonal-lemma (Abelianβ†’Group-on (A.Abelian-group-on-hom _ _)) {I} i _
        (A.eliml (Ξ΄α΅’α΅’ i (Discreteα΅’-Fin i i)))
        λ j i≠j →
            apβ‚‚ A._∘_ (Ξ΄α΅’β±Ό j i (Ξ» e β†’ iβ‰ j (sym e)) (Discreteα΅’-Fin j i))
                      refl
          βˆ™ A.∘-zero-l

      πΣδπ : βˆ€ i β†’ ip.Ο€ i A.∘ split ≑ ip.Ο€ i
      πΣδπ i =
        ip.Ο€ i A.∘ βˆ‘β‚• I (Ξ» i β†’ ip.tuple Ξ» j β†’ Ξ΄ i j A.∘ ip.Ο€ i) β‰‘βŸ¨ ap (ip.Ο€ i A.∘_) (sym (tuple-sum {I} _)) βŸ©β‰‘
        ip.Ο€ i A.∘ ip.tuple (Ξ» i β†’ βˆ‘β‚• I Ξ» j β†’ Ξ΄ j i A.∘ ip.Ο€ j) β‰‘βŸ¨ ip.commute βŸ©β‰‘
        βˆ‘β‚• I (Ξ» j β†’ Ξ΄ j i A.∘ ip.Ο€ j)                           β‰‘βŸ¨ sum-Ξ΄-Ο€ i βŸ©β‰‘
        ip.Ο€ i                                                  ∎

We can now use this split morphism to construct the coproduct structure on ∏F\prod F. First, the i-th coprojection ΞΉi:Fiβ†’βˆF\iota_i : F_i \to \prod F is a tuple where all but the ii-th coordinate are 00, and ii is one. That is: it’s the tuple over jj of Ξ΄i,j\delta_{i,j}!

  open Indexed-coproduct
  open is-indexed-coproduct
  coprod : Indexed-coproduct C F
  coprod .Ξ£F = ip.Ξ F
  coprod .ΞΉ i = ip.tuple (Ξ΄ i)

We now need to define the β€œmatch” function: Given a family f:Fiβ†’Yf : F_i \to Y, how do we extend this to a (unique) map mfm_f satisfying mfΞΉj=fjm_f \iota_j = f_j? Well, one potential approach is define mfm_f to be some kind of sum β€” let’s say it’s a sum over fiβ€²f'_i, where fiβ€²f'_i is something we’ll define later. We can still calculate

mfΞΉj=(βˆ‘ifiβ€²)ΞΉj=βˆ‘ifiβ€²ΞΉj m_f \iota_j = (\sum_i f'_i) \iota_{j} = \sum_i f'_i \iota_j

so we have to choose fiβ€²f'_i such that fiβ€²f'_i is ff when i=ji = j, and 00 otherwise, so only the ff term contributes to the above sum. And we know that, composed with ΞΉj\iota_j, the jj-th projection is the identity function, and all others are 00 β€” so if we define fiβ€²=fΟ€if'_i = f\pi_i, then we certainly have (βˆ‘ifiβ€²)ΞΉj(\sum_i f'_i) \iota_j = ff!

  coprod .has-is-ic = ico where
    m : βˆ€ {Y} β†’ (βˆ€ i β†’ A.Hom (F i) Y) β†’ A.Hom (ip .Indexed-product.Ξ F) Y
    m f = βˆ‘β‚• I Ξ» j β†’ f j A.∘ ip.Ο€ j

    ico : is-indexed-coproduct C F _
    ico .match f = m f
    ico .commute {i = i} {f = f} =
      m f A.∘ ip.tuple (Ξ΄ i)                           β‰‘βŸ¨ βˆ‘-∘-right {I} _ βŸ©β‰‘
      βˆ‘β‚• I (Ξ» j β†’ (f j A.∘ ip.Ο€ j) A.∘ ip.tuple (Ξ΄ i)) β‰‘βŸ¨ remark βŸ©β‰‘
      f i                                              ∎

And how do we show uniqueness? Using our remark about the split morphism defined above! It shows that any map mβ€²:∏Fβ†’Ym' : \prod F \to Y has to factor through something that looks a lot like our definition of mfm_f above, and if it also satisfies hΞΉj=fjh\iota_j = f_j, then a bit of massaging shows it is exactly mfm_f.

    ico .unique {h = h} f prf =
      h                                                    β‰‘βŸ¨ A.intror (sym split-remark) βŸ©β‰‘
      h A.∘ split                                          β‰‘βŸ¨ βˆ‘-∘-left {I} _ βŸ©β‰‘
      βˆ‘β‚• I (Ξ» i β†’ h A.∘ ip.tuple (Ξ» j β†’ Ξ΄ i j A.∘ ip.Ο€ i)) β‰‘βŸ¨ βˆ‘-path {I} _ (Ξ» i β†’ ap (h A.∘_) (sym (tuple∘ C F ip _))) βŸ©β‰‘
      βˆ‘β‚• I (Ξ» i β†’ h A.∘ ip.tuple (Ξ» j β†’ Ξ΄ i j) A.∘ ip.Ο€ i) β‰‘βŸ¨ βˆ‘-path {I} _ (Ξ» i β†’ A.pulll (prf i)) βŸ©β‰‘
      βˆ‘β‚• I (Ξ» i β†’ f i A.∘ ip.Ο€ i)                          β‰‘βŸ¨βŸ©
      m f                                                  ∎

  1. We’ll see in this very same module that they’re actually the same thing!β†©οΈŽ

  2. In the binary case.β†©οΈŽ

  3. Where i,ji, j both range over [n][n].β†©οΈŽ