open import Algebra.Group.Ab
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 $\mathbf{Ab}$-categories are additionally equipped with the structure of abelian groups on their $\mathbf{Hom}$-sets, itβs natural that we ask that functors between $\mathbf{Ab}$-categories preserve this structure. In particular, since every functor $F : \mathcal{C} \to \mathcal{D}$ has an action $F(-) : \mathbf{Hom}(a,b) \to \mathbf{Hom}(Fa,Fb)$ which is a map of sets, when $\mathcal{C}$ and $\mathcal{D}$ are considered to be abelian groups, we should require that the action $F(-)$ be a group homomorphism.

module
_ {o β o' β'} {C : Precategory o β} {D : Precategory o' β'}
(A : Ab-category C) (B : Ab-category D)
where
private
module A = Ab-category A
module B = Ab-category B

  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 $\mathbf{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} β is-group-hom
(AbelianβGroup-on (A.Abelian-group-on-hom a b))
(AbelianβGroup-on (B.Abelian-group-on-hom _ _))
Fβ
F-hom .is-group-hom.pres-β = F-+

F-0m : β {a b} β Fβ {a} {b} A.0m β‘ B.0m
F-0m = is-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 _ _ = is-group-hom.pres-diff F-hom

F-inv : β {a b} (f : A.Hom a b) β Fβ (A.Hom.inverse f) β‘ B.Hom.inverse (Fβ f)
F-inv _ = is-group-hom.pres-inv F-hom


Since the zero object $\emptyset$ in an $\mathbf{Ab}$-category is characterised as the unique object having $\operatorname{id}_{\emptyset} = 0$, and $\mathbf{Ab}$-functors preserve both $\operatorname{id}_{}$ and $0$, every $\mathbf{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 \$