module Cat.Abelian.Functor where

Ab-enriched functorsπŸ”—

Since are additionally equipped with the structure of abelian groups on their it’s natural that we ask that functors between preserve this structure. In particular, since every functor has an action which is a map of sets, when and are considered to be abelian groups, we should require that the action 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 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 in an is characterised as the unique object having and preserve both and every 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