open import Algebra.Magma.Unital
open import Algebra.Group.Ab
open import Algebra.Prelude
open import Algebra.Monoid
open import Algebra.Group

open import Cat.Displayed.Univalence.Thin
open import Cat.Diagram.Equaliser.Kernel

import Algebra.Group.Cat.Base as Grp

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 $\Ab$-enriched category is one where each $\hom$ set carries the structure of an Abelian group, such that the composition map is bilinear, hence extending to an Abelian group homomorphism

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

where the term on the left is the tensor product of the corresponding $\hom$-groups. As the name implies, every such category has a canonical $\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
Group-on-hom :  A B  Group-on (Hom A B)

_+_ :  {A B} (f g : Hom A B)  Hom A B
f + g = Group-on-hom _ _ .Group-on._⋆_ f g

0m :  {A B}  Hom A B
0m = Group-on-hom _ _ .Group-on.unit

field
Hom-grp-ab :  A B (f g : Hom A B)  f + g  g + f

Hom-grp :  A B  AbGroup
Hom-grp A B = restrict (el! (Hom A B) , Group-on-hom A B) (Hom-grp-ab 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-multilinear-map {A = Hom-grp B C} {B = Hom-grp A B} {C = Hom-grp A C}
_∘_
f g h  sym (∘-linear-l _ _ _))
f g h  sym (∘-linear-r _ _ _))

module Hom {A B} = AbGrp (Hom-grp A B)
open Hom
using (zero-diff)
renaming (_—_ to _-_)
public
Note that from multilinearity of composition, it follows that the addition of $\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
f  0m + (f  0m - f  0m)
(f  0m + f  0m) - f  0m
(f  (0m + 0m)) - f  0m
(f  0m) - f  0m
0m

∘-zero-l :  {A B C} {f : Hom A B}  0m  f  0m {A} {C}
∘-zero-l {f = f} =
0m  f
(Hom.inverse (0m  f) + 0m  f) + 0m  f
Hom.inverse (0m  f) + (0m  f + 0m  f)
Hom.inverse (0m  f) + ((0m + 0m)  f)
Hom.inverse (0m  f) + (0m  f)
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
f  h + (Hom.inverse g  h)
(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
f  g + (f  Hom.inverse h)
f  (g - h)

Before moving on, we note the following property of $\Ab$-categories: If $A$ is an object s.t. $\id{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 h A.∘ A.id h A.∘ A.0m A.0m id-zero→zero idm .A.is-zero.has-is-terminal x = contr A.0m λ h sym$
h
A.id A.∘ h
A.0m A.∘ h
A.0m

Perhaps the simplest example of an $\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 $\Ab$-category, rather than a horizontal categorification of the drummer for the Beatles. The next simplest example is $\Ab$ itself:

module _ where
open Ab-category
Ab-ab-category :  {}  Ab-category (Ab )
Ab-ab-category .Group-on-hom A B = Hom-group A B .object .snd
Ab-ab-category .Hom-grp-ab A B = Hom-group A B .witness
Ab-ab-category .∘-linear-l f g h = Grp.Forget-is-faithful refl
Ab-ab-category .∘-linear-r f g h = Grp.Forget-is-faithful $funext λ x sym (f .preserves .Group-hom.pres-⋆ _ _) # Additive categories🔗 An $\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*} &(\id{id} \times 0) : A \to A \times B \\ &(0 \times \id{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)(\id{id}\times 0) \\ =& f\pi_1(\id{id}\times 0) + g\pi_2(\id{id}\times 0) \\ =& f\id{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.
coprod .in₁ = 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.
((inj0  Prod.π₁)  Prod. + _)
(inj0  Prod.π₁)  Prod.
inj0
coprod .has-is-coproduct .in₁∘factor {inj0 = inj0} {inj1} =
(inj0  Prod.π₁ + inj1  Prod.π₂)  Prod.
(_ + (inj1  Prod.π₂)  Prod.)
(inj1  Prod.π₂)  Prod.
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.π₂ (other Prod. Prod.π₁) + (other Prod. Prod.π₂) other (Prod. Prod.π₁ + Prod. Prod.π₂) other where lemma : Prod. Prod.π₁ + 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 has-additive : is-additive C open is-additive has-additive public 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 \xto{f} B$ in a preabelian category admits a canonical decomposition as $A \xepi{p} \coker (\ker f) \xto{f'} \ker (\coker f) \xmono{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.coequalise (Ker.kernel f) {e′ = f}$ sym path
map : Hom (Coker.coapex (Ker.kernel f)) (Ker.ker (Coker.coeq f))
map = Ker.limiting (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 \coker(f)$, and the map $i$ is the canonical subobject inclusion $\ker(f) \to B$. 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 \mono B$ is some monomorphism; We’ll show that it’s isomorphic to $\ker (\coker f)$ in the slice category $\ca{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 (\coker f)$ is obtained as the composite $A \xepi{p} \coker (\ker f) \cong \ker (\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 (\coker f) \to A$ is the composite $\ker (\coker f) \cong \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 \mono 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.coequalise (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 0m ≡˘ (∅.zero→ Ker.kernel f) ≡˘ f Ker.kernel f 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.universal _)
·· elimr refl
·· (decompose f .snd  assoc _ _ _)

path =
invertible→epic (coker-ker≃ker-coker _) _ _ $(f Coker.coequalise _ _ _) decompose f .fst ((f Coker.coequalise _ _) _) decompose f .fst f Coker.coequalise _ _ 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 $\ca{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.coequalise _ _  _
decompose f .fst  _
id
where
lemma = Coker.unique₂ _
{e′ = Coker.coeq (Ker.kernel f)}
{p = ∘-zero-r  sym (sym (Coker.coequal _)  ∘-zero-r)}
(sym (pullr (Coker.universal (Ker.kernel f))  elimr refl))
(introl refl)

kc→f→kc : kercoker→f m.∘ f→kercoker  m.id
kc→f→kc = /-Hom-path \$
(Coker.coequalise _ _  _)  decompose f .fst  Coker.coeq _
Coker.coequalise _ _  Coker.coeq _
id

1. “multiplication”↩︎