open import Algebra.Group.NAry
open import Algebra.Group.Ab

open import Cat.Diagram.Coproduct.Indexed
open import Cat.Diagram.Product.Indexed
open import Cat.Diagram.Limit.Finite
open import Cat.Diagram.Equaliser
open import Cat.Abelian.Base
open import Cat.Diagram.Zero
open import Cat.Prelude hiding (_-_ ; _+_)

open import Data.Id.Base
open import Data.Dec
open import Data.Fin

import Cat.Abelian.NAry

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 as β whence the name difference kernel!

The calculation is straightforward: To map out of we must have but this is immediate assuming that β an assumption we have to map out of Similarly, to show that we calculate

module _ (A : is-pre-abelian C) where
open is-pre-abelian A
difference-kernel
: β {A B} {f g : Hom A B}
β is-equaliser C f g (Ker.kernel (f - g))
difference-kernel {f = f} {g} = equ where
open is-equaliser
equ : is-equaliser C 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 categories is the coincidence of finite products and finite coproducts: not only is there a map2 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 is a finite family of objects in an If has both a coproduct and a product in then we can define a map by giving a family of morphisms which amounts to defining a family of morphisms 3. Since is discrete, we can define this family to be when and everywhere else!

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

module _ (A : Ab-category C) {I : Nat} (F : Fin I β C .Precategory.Ob)
(ip : Indexed-product C F) where
private
module A = Ab-category A
module ip = Indexed-product ip
open Cat.Abelian.NAry A


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 is

  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 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 (i β‘α΅’? j)

Ξ΄α΅’β±Ό : β 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 through a β hypothetical β A βsplittingβ map which works by summing (over the tupling (over of and since tupling commutes with sums, we conclude that this is the tupling over 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

  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 refl) Ξ» j iβ j β
apβ A._β_ (Ξ΄α΅’β±Ό j i (Ξ» e β iβ j (sym e)) (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 First, the i-th coprojection is a tuple where all but the coordinate are and is one. That is: itβs the tuple over of

  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 how do we extend this to a (unique) map satisfying Well, one potential approach is define to be some kind of sum β letβs say itβs a sum over where is something weβll define later. We can still calculate

so we have to choose such that is when and otherwise, so only the term contributes to the above sum. And we know that, composed with the projection is the identity function, and all others are β so if we define then we certainly have =

  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                                              β

      where
remark = β-diagonal-lemma (AbelianβGroup-on (A.Abelian-group-on-hom _ _)) {I} i
(Ξ» j β (f j A.β ip.Ο j) A.β ip.tuple (Ξ» v β Ξ΄ i v))
(A.cancelr ip.commute)
Ξ» j iβ j β A.pullr (ip.commute β Ξ΄α΅’β±Ό i j iβ j (i β‘α΅’? j))
β A.β-zero-r


And how do we show uniqueness? Using our remark about the split morphism defined above! It shows that any map has to factor through something that looks a lot like our definition of above, and if it also satisfies then a bit of massaging shows it is exactly

    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!β©οΈ