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 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 -enriched 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 -category. 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 (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 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 (Ξ΄α΅’α΅’ 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
.
First, the i-th coprojection
is a tuple where all but the
-th
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 -th 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 _ (A.cancelr (ip.commute β Ξ΄α΅’α΅’ i (Discreteα΅’-Fin i i))) Ξ» j iβ j β A.pullr (ip.commute β Ξ΄α΅’β±Ό i j iβ j (Discreteα΅’-Fin 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 β