open import Algebra.Group open import Cat.Functor.FullSubcategory open import Cat.Abelian.Base open import Cat.Diagram.Zero open import Cat.Prelude module Cat.Abelian.Functor where

# Ab-enriched Functorsπ

Since $\Ab$-categories are additionally equipped with the structure of abelian groups on their $\hom$-sets, itβs natural that we ask that functors between $\Ab$-categories preserve this structure. In particular, since every functor $F : \ca{C} \to \ca{D}$ has an action $F(-) : \hom(a,b) \to \hom(Fa,Fb)$ which is a map of sets, when $\ca{C}$ and $\ca{D}$ are considered to be abelian groups, we should require that the action $F(-)$ be a group homomorphism.

record Ab-functor : Type (o β oβ² β β β ββ²) where field functor : Functor C D open Functor functor public field F-+ : β {a b} (f g : A.Hom a b) β Fβ (f A.+ g) β‘ Fβ f B.+ Fβ g

In passing we note that, since the
$\hom$-abelian-groups
are *groups*, preservation of addition automatically implies
preservation of the zero morphism, preservation of inverses, and thus
preservation of subtraction.

F-hom : β {a b} β Group-hom (A.Group-on-hom a b) (B.Group-on-hom _ _) Fβ F-hom .Group-hom.pres-β = F-+ F-0m : β {a b} β Fβ {a} {b} A.0m β‘ B.0m F-0m = Group-hom.pres-id F-hom F-diff : β {a b} (f g : A.Hom a b) β Fβ (f A.- g) β‘ Fβ f B.- Fβ g F-diff _ _ = Group-hom.pres-diff F-hom F-inv : β {a b} (f : A.Hom a b) β Fβ (f A.Hom.β»ΒΉ) β‘ Fβ f B.Hom.β»ΒΉ F-inv _ = Group-hom.pres-inv F-hom

Since the zero object
$\emptyset$
in an
$\Ab$-category
is characterised as the unique object having
$\id{id}_\emptyset = 0$,
and
$\Ab$-functors
preserve both
$\id{id}$
and
$0$,
every
$\Ab$-functor
preserves zero objects. We say that the zero object, considered as a
colimit, is **absolute**, i.e., preserved by every
(relevant) functor.

Ab-functor-pres-β : β {o β oβ² ββ²} {C : Precategory o β} {D : Precategory oβ² ββ²} {A : Ab-category C} {B : Ab-category D} β (F : Ab-functor A B) (β A : Zero C) β is-zero D (Ab-functor.Fβ F (Zero.β β A)) Ab-functor-pres-β {A = A} {B = B} F β A = id-zeroβzero B $ B.id β‘Λβ¨ F.F-id β©β‘Λ F.β A.id β‘β¨ ap F.β (is-contrβis-prop (Zero.hasβ€ β A (Zero.β β A)) _ _) β©β‘ F.β A.0m β‘β¨ F.F-0m β©β‘ B.0m β where module A = Ab-category A module B = Ab-category B module F = Ab-functor F