module Cat.Abelian.Functor where

Ab-enriched functorsπŸ”—

Since Ab\mathbf{Ab}-categories are additionally equipped with the structure of abelian groups on their Hom\mathbf{Hom}-sets, it’s natural that we ask that functors between Ab\mathbf{Ab}-categories preserve this structure. In particular, since every functor F:Cβ†’DF : \mathcal{C} \to \mathcal{D} has an action F(βˆ’):Hom(a,b)β†’Hom(Fa,Fb)F(-) : \mathbf{Hom}(a,b) \to \mathbf{Hom}(Fa,Fb) which is a map of sets, when C\mathcal{C} and D\mathcal{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\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-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 Ab\mathbf{Ab}-category is characterised as the unique object having idβ‘βˆ…=0\operatorname{id}_{\emptyset} = 0, and Ab\mathbf{Ab}-functors preserve both id⁑\operatorname{id}_{} and 00, every Ab\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.

  : βˆ€ {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