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.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 = (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 composition¹ 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 $\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                                ≡⟨ 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 $
    h                              ≡⟨ A.introl refl ⟩≡
    A.id A.∘ h                     ≡⟨ idm A.⟩∘⟨refl ⟩≡
    A.0m A.∘ h                     ≡⟨ A.∘-zero-l ⟩≡
    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 .snd .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\times{,} \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 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              ≡⟨ 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.universal _)
            ·· elimr refl
            ·· (decompose f .snd ∙ assoc _ _ _)

        path =
          invertible→epic (coker-ker≃ker-coker _) _ _ $
            (f ∘ Coker.coequalise _ _ ∘ _) ∘ decompose f .fst   ≡⟨ ap₂ _∘_ (assoc _ _ _) refl ⟩≡
            ((f ∘ Coker.coequalise _ _) ∘ _) ∘ decompose f .fst ≡⟨ cancelr (coker-ker≃ker-coker _ .is-invertible.invr) ⟩≡
            f ∘ Coker.coequalise _ _                            ≡⟨ 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 $\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 _ _ ∘ _ ≡⟨ 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)}
            {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 _ ≡⟨ cancel-inner (coker-ker≃ker-coker f .is-invertible.invr) ⟩≡
        Coker.coequalise _ _ ∘ Coker.coeq _                          ≡⟨ Coker.universal _ ⟩≡
        id                                                           ∎

“multiplication”↩︎