open import Algebra.Group.Ab.Tensor
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
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 Ab\mathbf{Ab}-enriched category is one where each Hom\mathbf{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)βŠ—Hom(a,b)β†’Hom(a,c), \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 Hom\mathbf{Hom}-groups. As the name implies, every such category has a canonical Ab\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 Hom\mathbf{Hom}-groups and composition1 operations satisfy familiar algebraic identities, e.g.Β 0f=f0=00f = f0 = 0, βˆ’ab=(βˆ’a)b=a(βˆ’b)-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\mathbf{Ab}-categories: If AA is an object s.t. idA=0\mathrm{id}_{A} = 0, then AA 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\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 Ab\mathbf{Ab}-category, rather than a horizontal categorification of the drummer for the Beatles. The next simplest example is Ab\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-⋆ _ _))

Additive categoriesπŸ”—

An Ab\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

(id×0):A→A×B(0×id):B→A×B, \begin{align*} &(\mathrm{id}_{} \times 0) : A \to A \times B \\ &(0 \times \mathrm{id}_{}) : B \to A \times B\text{,} \end{align*}

respectively, and the comultiplication of ff and gg is given by fΟ€1+gΟ€2f\pi_1 + g\pi_2. We can calculate, for the first coprojection followed by comultiplication,

(fΟ€1+gΟ€2)(idΓ—0)=fΟ€1(idΓ—0)+gΟ€2(idΓ—0)=fid+g0=f, \begin{align*} & (f\pi_1+g\pi_2)(\mathrm{id}_{}\times 0) \\ =& f\pi_1(\mathrm{id}_{}\times 0) + g\pi_2(\mathrm{id}_{}\times 0) \\ =& f\mathrm{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 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→fBA \xrightarrow{f} B in a preabelian category admits a canonical decomposition as

Aβ† pcoker⁑(ker⁑f)β†’fβ€²ker⁑(coker⁑f)β†ͺiB, A \xtwoheadrightarrow{p} \operatorname{coker}(\ker f) \xrightarrow{f'} \ker (\operatorname{coker}f) \xhookrightarrow{i} B\text{,}

where, as indicated, the map pp is an epimorphism (indeed a regular epimorphism, since it is a cokernel) and the map ii 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
      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β€²f', and indeed of the maps pp and ii, follow from the universal properties of kernels and cokernels. The map pp is the canonical quotient map Aβ†’coker⁑(f)A \to \operatorname{coker}(f), and the map ii is the canonical subobject inclusion ker⁑(f)β†’B\ker(f) \to B.

A pre-abelian category is abelian when the map fβ€²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β†ͺBf : A \hookrightarrow B is some monomorphism; We’ll show that it’s isomorphic to ker⁑(coker⁑f)\ker (\operatorname{coker}f) in the slice category A/B\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β†’ker⁑(coker⁑f)A \to \ker (\operatorname{coker}f) is obtained as the composite

Aβ† pcoker⁑(ker⁑f)β‰…ker⁑(coker⁑f), 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⁑(coker⁑f)β†’A\ker (\operatorname{coker}f) \to A is the composite

ker⁑(coker⁑f)β‰…coker⁑(ker⁑f)β†’A, \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β†ͺA\ker f \hookrightarrow A, since (using that ff is mono), we have 0=ker⁑f0 = \ker f from f0=fker⁑ff0 = 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 A\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                                                           ∎

  1. β€œmultiplicationβ€β†©οΈŽ