open import Algebra.Group.Ab.Tensor
open import Algebra.Group.Ab
open import Algebra.Prelude
open import Algebra.Monoid
open import Algebra.Group

open import Cat.Diagram.Equaliser.Kernel

import Algebra.Group.Cat.Base as Grp
import Algebra.Group.Ab.Hom as Ab

module Cat.Abelian.Base where


# Abelian categoriesπ

This module defines the sequence of properties which βwork up toβ abelian categories: Ab-enriched categories, pre-additive categories, pre-abelian categories, and abelian categories. Each concept builds on the last by adding a new categorical property on top of a precategory.

## Ab-enriched categoriesπ

An $\mathbf{Ab}$-enriched category is one where each $\mathbf{Hom}$ set carries the structure of an Abelian group, such that the composition map is bilinear, hence extending to an Abelian group homomorphism

$\mathbf{Hom}(b, c) \otimes \mathbf{Hom}(a, b) \to \mathbf{Hom}(a, c)\text{,}$

where the term on the left is the tensor product of the corresponding $\mathbf{Hom}$-groups. As the name implies, every such category has a canonical $\mathbf{Ab}$-enrichment (made monoidal using $- \otimes -$), but we do not use the language of enriched category theory in our development of Abelian categories.

record Ab-category {o β} (C : Precategory o β) : Type (o β lsuc β) where
open Cat C public
field
Abelian-group-on-hom : β A B β Abelian-group-on (Hom A B)

_+_ : β {A B} (f g : Hom A B) β Hom A B
f + g = Abelian-group-on-hom _ _ .Abelian-group-on._*_ f g

0m : β {A B} β Hom A B
0m = Abelian-group-on-hom _ _ .Abelian-group-on.1g

Hom-grp : β A B β Abelian-group β
Hom-grp A B = (el (Hom A B) (Hom-set A B)) , Abelian-group-on-hom A B

field
-- Composition is multilinear:
β-linear-l
: β {A B C} (f g : Hom B C) (h : Hom A B)
β (f β h) + (g β h) β‘ (f + g) β h
β-linear-r
: β {A B C} (f : Hom B C) (g h : Hom A B)
β (f β g) + (f β h) β‘ f β (g + h)

βmap : β {A B C} β Ab.Hom (Hom-grp B C β Hom-grp A B) (Hom-grp A C)
βmap {A} {B} {C} =
from-bilinear-map (Hom-grp B C) (Hom-grp A B) (Hom-grp A C)
(record { map     = _β_
; pres-*l = Ξ» x y z β sym (β-linear-l x y z)
; pres-*r = Ξ» x y z β sym (β-linear-r x y z)
})

module Hom {A B} = Abelian-group-on (Abelian-group-on-hom A B) renaming (_β»ΒΉ to inverse)
open Hom
using (zero-diff)
renaming (_β_ to _-_)
public

Note that from multilinearity of composition, it follows that the addition of $\mathbf{Hom}$-groups and composition1 operations satisfy familiar algebraic identities, e.g.Β $0f = f0 = 0$, $-ab = (-a)b = a(-b)$, etc.
  β-zero-r : β {A B C} {f : Hom B C} β f β 0m {A} {B} β‘ 0m
β-zero-r {f = f} =
f β 0m                     β‘β¨ Hom.intror Hom.inverser β©β‘
f β 0m + (f β 0m - f β 0m) β‘β¨ Hom.associative β©β‘
(f β 0m + f β 0m) - f β 0m β‘β¨ ap (_- f β 0m) (β-linear-r _ _ _) β©β‘
(f β (0m + 0m)) - f β 0m   β‘β¨ ap ((_- f β 0m) β (f β_)) Hom.idl β©β‘
(f β 0m) - f β 0m          β‘β¨ Hom.inverser β©β‘
0m                         β

β-zero-l : β {A B C} {f : Hom A B} β 0m β f β‘ 0m {A} {C}
β-zero-l {f = f} =
0m β f                                   β‘β¨ Hom.introl Hom.inversel β©β‘
(Hom.inverse (0m β f) + 0m β f) + 0m β f β‘β¨ sym Hom.associative β©β‘
Hom.inverse (0m β f) + (0m β f + 0m β f) β‘β¨ ap (Hom.inverse (0m β f) +_) (β-linear-l _ _ _) β©β‘
Hom.inverse (0m β f) + ((0m + 0m) β f)   β‘β¨ ap ((Hom.inverse (0m β f) +_) β (_β f)) Hom.idl β©β‘
Hom.inverse (0m β f) + (0m β f)          β‘β¨ Hom.inversel β©β‘
0m                                       β

neg-β-l
: β {A B C} {g : Hom B C} {h : Hom A B}
β Hom.inverse (g β h) β‘ Hom.inverse g β h
neg-β-l {g = g} {h} = monoid-inverse-unique Hom.has-is-monoid (g β h) _ _
Hom.inversel
(β-linear-l _ _ _ β ap (_β h) Hom.inverser β β-zero-l)

neg-β-r
: β {A B C} {g : Hom B C} {h : Hom A B}
β Hom.inverse (g β h) β‘ g β Hom.inverse h
neg-β-r {g = g} {h} = monoid-inverse-unique Hom.has-is-monoid (g β h) _ _
Hom.inversel
(β-linear-r _ _ _ β ap (g β_) Hom.inverser β β-zero-r)

β-minus-l
: β {A B C} (f g : Hom B C) (h : Hom A B)
β (f β h) - (g β h) β‘ (f - g) β h
β-minus-l f g h =
f β h - g β h               β‘β¨ ap (f β h +_) neg-β-l β©β‘
f β h + (Hom.inverse g β h) β‘β¨ β-linear-l _ _ _ β©β‘
(f - g) β h                 β

β-minus-r
: β {A B C} (f : Hom B C) (g h : Hom A B)
β (f β g) - (f β h) β‘ f β (g - h)
β-minus-r f g h =
f β g - f β h               β‘β¨ ap (f β g +_) neg-β-r β©β‘
f β g + (f β Hom.inverse h) β‘β¨ β-linear-r _ _ _ β©β‘
f β (g - h)                 β


Before moving on, we note the following property of $\mathbf{Ab}$-categories: If $A$ is an object s.t. $\operatorname{id}_{A} = 0$, then $A$ is a zero object.

module _ {o β} {C : Precategory o β} (A : Ab-category C) where
private module A = Ab-category A

id-zeroβzero : β {A} β A.id {A} β‘ A.0m β A.is-zero A
id-zeroβzero idm .A.is-zero.has-is-initial B = contr A.0m Ξ» h β sym $h β‘β¨ A.intror refl β©β‘ h A.β A.id β‘β¨ A.reflβ©ββ¨ idm β©β‘ h A.β A.0m β‘β¨ A.β-zero-r β©β‘ A.0m β id-zeroβzero idm .A.is-zero.has-is-terminal x = contr A.0m Ξ» h β sym$
A.0m A.β h                     β‘β¨ A.β-zero-l β©β‘
A.0m                           β


Perhaps the simplest example of an $\mathbf{Ab}$-category is.. any ring! In the same way that a monoid is a category with one object, and a group is a groupoid with one object, a ring is a ringoid with one object; Ringoid being another word for $\mathbf{Ab}$-category, rather than a horizontal categorification of the drummer for the Beatles. The next simplest example is $\mathbf{Ab}$ itself:

module _ where
open Ab-category
Ab-ab-category : β {β} β Ab-category (Ab β)
Ab-ab-category .Abelian-group-on-hom A B = Ab.Abelian-group-on-hom A B
Ab-ab-category .β-linear-l f g h = Homomorphism-path (Ξ» _ β refl)
Ab-ab-category .β-linear-r f g h =
Homomorphism-path (Ξ» _ β sym (f .preserves .is-group-hom.pres-β _ _))


An $\mathbf{Ab}$-category is additive when its underlying category has a terminal object and finite products; By the yoga above, this implies that the terminal object is also a zero object, and the finite products coincide with finite coproducts.

record is-additive {o β} (C : Precategory o β) : Type (o β lsuc β) where
field has-ab : Ab-category C
open Ab-category has-ab public

field
has-terminal : Terminal
has-prods    : β A B β Product A B

β : Zero
β .Zero.β = has-terminal .Terminal.top
β .Zero.has-is-zero = id-zeroβzero has-ab is-contrβis-prop (has-terminal .Terminal.hasβ€ _) _ _ module β = Zero β 0m-unique : β {A B} β β .zeroβ {A} {B} β‘ 0m 0m-unique = apβ _β_ (β .hasβ₯ _ .paths _) refl β β-zero-l  Coincidence of finite products and finite coproducts leads to an object commonly called a (finite) biproduct. The coproduct coprojections are given by the pair of maps \begin{align*} &(\operatorname{id}_{} \times 0) : A \to A \times B \\ &(0 \times \operatorname{id}_{}) : B \to A \times B\text{,} \end{align*} respectively, and the comultiplication of $f$ and $g$ is given by $f\pi_1 + g\pi_2$. We can calculate, for the first coprojection followed by comultiplication, \begin{align*} & (f\pi_1+g\pi_2)(\operatorname{id}_{}\times 0) \\ =& f\pi_1(\operatorname{id}_{}\times 0) + g\pi_2(\operatorname{id}_{}\times 0) \\ =& f\operatorname{id}_{} + g0 \\ =& f\text{,} \end{align*} and analogously for the second coprojection followed by comultiplication.  has-coprods : β A B β Coproduct A B has-coprods A B = coprod where open Coproduct open is-coproduct module Prod = Product (has-prods A B) coprod : Coproduct A B coprod .coapex = Prod.apex coprod .inβ = Prod.β¨ id , 0m β©Prod. coprod .inβ = Prod.β¨ 0m , id β©Prod. coprod .has-is-coproduct .[_,_] f g = f β Prod.Οβ + g β Prod.Οβ coprod .has-is-coproduct .inββfactor {inj0 = inj0} {inj1} = (inj0 β Prod.Οβ + inj1 β Prod.Οβ) β Prod.β¨ id , 0m β©Prod. β‘β¨ sym (β-linear-l _ _ _) β©β‘ ((inj0 β Prod.Οβ) β Prod.β¨ id , 0m β©Prod. + _) β‘β¨ Hom.elimr (pullr Prod.Οββfactor β β-zero-r) β©β‘ (inj0 β Prod.Οβ) β Prod.β¨ id , 0m β©Prod. β‘β¨ cancelr Prod.Οββfactor β©β‘ inj0 β coprod .has-is-coproduct .inββfactor {inj0 = inj0} {inj1} = (inj0 β Prod.Οβ + inj1 β Prod.Οβ) β Prod.β¨ 0m , id β©Prod. β‘β¨ sym (β-linear-l _ _ _) β©β‘ (_ + (inj1 β Prod.Οβ) β Prod.β¨ 0m , id β©Prod.) β‘β¨ Hom.eliml (pullr Prod.Οββfactor β β-zero-r) β©β‘ (inj1 β Prod.Οβ) β Prod.β¨ 0m , id β©Prod. β‘β¨ cancelr Prod.Οββfactor β©β‘ inj1 β  For uniqueness, we use distributivity of composition over addition of morphisms and the universal property of the product to establish the desired equation. Check it out:  coprod .has-is-coproduct .unique {inj0 = inj0} {inj1} other p q = sym
inj0 β Prod.Οβ + inj1 β Prod.Οβ                                             β‘β¨ apβ _+_ (pushl (sym p)) (pushl (sym q)) β©β‘
(other β Prod.β¨ id , 0m β©Prod. β Prod.Οβ) + (other β Prod.β¨ 0m , id β©Prod. β Prod.Οβ) β‘β¨ β-linear-r _ _ _ β©β‘
other β (Prod.β¨ id , 0m β©Prod. β Prod.Οβ + Prod.β¨ 0m , id β©Prod. β Prod.Οβ)           β‘β¨ elimr lemma β©β‘
other                                                                       β
where
lemma : Prod.β¨ id , 0m β©Prod. β Prod.Οβ + Prod.β¨ 0m , id β©Prod. β Prod.Οβ
β‘ id
lemma = Prod.uniqueβ {pr1 = Prod.Οβ} {pr2 = Prod.Οβ}
(sym (β-linear-r _ _ _) β apβ _+_ (cancell Prod.Οββfactor) (pulll Prod.Οββfactor β β-zero-l) β Hom.elimr refl)
(sym (β-linear-r _ _ _) β apβ _+_ (pulll Prod.Οββfactor β β-zero-l) (cancell Prod.Οββfactor) β Hom.eliml refl)
(elimr refl)
(elimr refl)


# Pre-abelian & abelian categoriesπ

An additive category is pre-abelian when it additionally has kernels and cokernels, hence binary equalisers and coequalisers where one of the maps is zero.

record is-pre-abelian {o β} (C : Precategory o β) : Type (o β lsuc β) where
field
kernel   : β {A B} (f : Hom A B) β Kernel C β f
cokernel : β {A B} (f : Hom A B) β Coequaliser 0m f

module Ker {A B} (f : Hom A B) = Kernel (kernel f)
module Coker {A B} (f : Hom A B) = Coequaliser (cokernel f)


Every morphism $A \xrightarrow{f} B$ in a preabelian category admits a canonical decomposition as

$A \xtwoheadrightarrow{p} \operatorname{coker}(\ker f) \xrightarrow{f'} \ker (\operatorname{coker}f) \xhookrightarrow{i} B\text{,}$

where, as indicated, the map $p$ is an epimorphism (indeed a regular epimorphism, since it is a cokernel) and the map $i$ is a regular monomorphism.

  decompose
: β {A B} (f : Hom A B)
β Ξ£[ fβ² β Hom (Coker.coapex (Ker.kernel f)) (Ker.ker (Coker.coeq f)) ]
(f β‘ Ker.kernel (Coker.coeq f) β fβ² β Coker.coeq (Ker.kernel f))
decompose {A} {B} f = map , sym path
where
projβ² : Hom (Coker.coapex (Ker.kernel f)) B
projβ² = Coker.universal (Ker.kernel f) {eβ² = f} $sym path   where abstract path : f β kernel f .Kernel.kernel β‘ f β 0m path = Ker.equal f Β·Β· β .zero-βr _ Β·Β· apβ _β_ (β .hasβ₯ _ .paths 0m) refl Β·Β· β-zero-l Β·Β· sym β-zero-r   map : Hom (Coker.coapex (Ker.kernel f)) (Ker.ker (Coker.coeq f)) map = Ker.universal (Coker.coeq f) {eβ² = projβ²}$ sym path


The existence of the map $f'$, and indeed of the maps $p$ and $i$, follow from the universal properties of kernels and cokernels. The map $p$ is the canonical quotient map $A \to \operatorname{coker}(f)$, and the map $i$ is the canonical subobject inclusion $\ker(f) \to B$.

        where abstract
path : β.zeroβ β projβ² β‘ Coker.coeq f β projβ²
path = Coker.uniqueβ (Ker.kernel f)
{eβ² = 0m} (β-zero-r β sym β-zero-l)
(pushl (β.zero-βr _) β pulll ( apβ _β_ refl (β.hasβ€ _ .paths 0m)
β β-zero-r)
β β-zero-l)
(pullr (Coker.factors (Ker.kernel f)) β sym (Coker.coequal _)
β β-zero-r)

path =
Ker.kernel (Coker.coeq f) β map β Coker.coeq (Ker.kernel f) β‘β¨ pulll (Ker.factors _) β©β‘
projβ² β Coker.coeq (Ker.kernel f)                           β‘β¨ Coker.factors _ β©β‘
f                                                           β


A pre-abelian category is abelian when the map $f'$ in the above decomposition is an isomorphism.

record is-abelian {o β} (C : Precategory o β) : Type (o β lsuc β) where
field has-is-preab : is-pre-abelian C
open is-pre-abelian has-is-preab public
field
coker-kerβker-coker
: β {A B} (f : Hom A B) β is-invertible (decompose f .fst)


This implies in particular that any monomorphism is a kernel, and every epimorphism is a cokernel. Letβs investigate the case for βevery mono is a kernelβ first: Suppose that $f : A \hookrightarrow B$ is some monomorphism; Weβll show that itβs isomorphic to $\ker (\operatorname{coker}f)$ in the slice category $\mathcal{A}/B$.

  module _ {A B} (f : Hom A B) (monic : is-monic f) where
private
module m = Cat (Slice C B)


The map $A \to \ker (\operatorname{coker}f)$ is obtained as the composite

$A \xtwoheadrightarrow{p} \operatorname{coker}(\ker f) \cong \ker (\operatorname{coker}f)\text{,}$

where the isomorphism is our canonical map from before.

      fβkercoker : m.Hom (cut f) (cut (Ker.kernel (Coker.coeq f)))
fβkercoker ./-Hom.map = decompose f .fst β Coker.coeq (Ker.kernel f)
fβkercoker ./-Hom.commutes = sym (decompose f .snd)


Conversely, map $\ker (\operatorname{coker}f) \to A$ is the composite

$\ker (\operatorname{coker}f) \cong \operatorname{coker}(\ker f) \to A\text{,}$

where the second map arises from the universal property of the cokernel: We can map out of it with the map $\ker f \hookrightarrow A$, since (using that $f$ is mono), we have $0 = \ker f$ from $f0 = f\ker f$.

      kercokerβf : m.Hom (cut (Ker.kernel (Coker.coeq f))) (cut f)
kercokerβf ./-Hom.map =
Coker.universal (Ker.kernel f) {eβ² = id} (monic _ _ path) β
coker-kerβker-coker f .is-invertible.inv
where abstract
path : f β id β 0m β‘ f β id β Ker.kernel f
path =
f β id β 0m              β‘β¨ ap (f β_) (eliml refl) β β-zero-r β©β‘
0m                       β‘Λβ¨ β.zero-βr _ β 0m-unique β©β‘Λ
(β.zeroβ β Ker.kernel f) β‘Λβ¨ Ker.equal f β©β‘Λ
f β Ker.kernel f         β‘β¨ ap (f β_) (introl refl) β©β‘
f β id β Ker.kernel f    β


This is indeed a map in the slice using that both isomorphisms and coequalisers are epic to make progress.

      kercokerβf ./-Hom.commutes = path where
lemma =
is-coequaliserβis-epic (Coker.coeq _) (Coker.has-is-coeq _) _ _ $pullr (Coker.factors _) Β·Β· elimr refl Β·Β· (decompose f .snd β assoc _ _ _) path = invertibleβepic (coker-kerβker-coker _) _ _$
(f β Coker.universal _ _ β _) β decompose f .fst   β‘β¨ apβ _β_ (assoc _ _ _) refl β©β‘
((f β Coker.universal _ _) β _) β decompose f .fst β‘β¨ cancelr (coker-kerβker-coker _ .is-invertible.invr) β©β‘
f β Coker.universal _ _                            β‘β¨ lemma β©β‘
Ker.kernel _ β decompose f .fst                     β


Using the universal property of the cokernel (both uniqueness and universality), we establish that the maps defined above are inverses in $\mathcal{A}$, thus assemble into an isomorphism in the slice.

    monoβkernel : cut f m.β cut (Ker.kernel (Coker.coeq f))
monoβkernel = m.make-iso fβkercoker kercokerβf fβkcβf kcβfβkc where
fβkcβf : fβkercoker m.β kercokerβf β‘ m.id
fβkcβf = /-Hom-path $(decompose f .fst β Coker.coeq _) β Coker.universal _ _ β _ β‘β¨ cancel-inner lemma β©β‘ decompose f .fst β _ β‘β¨ coker-kerβker-coker f .is-invertible.invl β©β‘ id β where lemma = Coker.uniqueβ _ {eβ² = Coker.coeq (Ker.kernel f)} (β-zero-r β sym (sym (Coker.coequal _) β β-zero-r)) (pullr (Coker.factors (Ker.kernel f)) β elimr refl) (eliml refl) kcβfβkc : kercokerβf m.β fβkercoker β‘ m.id kcβfβkc = /-Hom-path$
(Coker.universal _ _ β _) β decompose f .fst β Coker.coeq _ β‘β¨ cancel-inner (coker-kerβker-coker f .is-invertible.invr) β©β‘
Coker.universal _ _ β Coker.coeq _                          β‘β¨ Coker.factors _ β©β‘
id                                                           β