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 -enriched category is one where each set carries the structure of an Abelian group, such that the composition map is bilinear, hence extending to an Abelian group homomorphism
where the term on the left is the tensor product of the corresponding -groups. As the name implies, every such category has a canonical -enrichment (made monoidal using ), 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 -groups and composition1 operations satisfy familiar algebraic identities, e.g.Β , , 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 -categories: If is an object s.t. , then 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 -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 -category, rather than a horizontal categorification of the drummer for the Beatles. The next simplest example is 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 -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
respectively, and the comultiplication of and is given by . We can calculate, for the first coprojection followed by comultiplication,
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 in a preabelian category admits a canonical decomposition as
where, as indicated, the map is an epimorphism (indeed a regular epimorphism, since it is a cokernel) and the map 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 , and indeed of the maps and , follow from the universal properties of kernels and cokernels. The map is the canonical quotient map , and the map is the canonical subobject inclusion .
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 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 is some monomorphism; Weβll show that itβs isomorphic to in the slice category .
module _ {A B} (f : Hom A B) (monic : is-monic f) where private module m = Cat (Slice C B)
The map is obtained as the composite
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 is the composite
where the second map arises from the universal property of the cokernel: We can map out of it with the map , since (using that is mono), we have from .
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 , 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 β
βmultiplicationββ©οΈ