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

  record Ab-functor : Type (o βŠ” oβ€² βŠ” β„“ βŠ” β„“β€²) where
      functor : Functor C D

    open Functor functor public

      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\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\Ab-category is characterised as the unique object having idβˆ…=0\id{id}_\emptyset = 0, and Ab\Ab-functors preserve both id\id{id} and 00, every Ab\Ab-functor preserves zero objects. We say that the zero object, considered as a colimit, is absolute, i.e., preserved by every (relevant) functor.

  : βˆ€ {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 $     β‰‘Λ˜βŸ¨ F.F-id βŸ©β‰‘Λ˜
    F.₁ β‰‘βŸ¨ ap F.₁ (is-contrβ†’is-prop (Zero.has⊀ βˆ…A (Zero.βˆ… βˆ…A)) _ _) βŸ©β‰‘
    F.₁ A.0m β‰‘βŸ¨ F.F-0m βŸ©β‰‘
    B.0m     ∎
    module A = Ab-category A
    module B = Ab-category B
    module F = Ab-functor F