open import Algebra.Group.Ab
open import Algebra.Monoid
open import Algebra.Group

open import Cat.Abelian.Instances.Ab
open import Cat.Instances.Functor
open import Cat.Abelian.Functor
open import Cat.Abelian.Base
open import Cat.Prelude

module Cat.Abelian.Instances.Functor
  where

Ab-enriched functor categoriesπŸ”—

Recall that, for a pair of Ab{{\mathbf{Ab}}}-categories A\mathcal{A} and B\mathcal{B}, we define the Ab{{\mathbf{Ab}}}-functors between them to be the functors F:A→BF : \mathcal{A} \to \mathcal{B} which additionally preserve homwise addition1. We can, mimicking the construction of the ordinary functor category, construct a category [A,B]Ab[\mathcal{A}, \mathcal{B}]_{{{\mathbf{Ab}}}} consisting only of the Ab{{\mathbf{Ab}}}-functors, and prove that it is also an Ab{{\mathbf{Ab}}}-category.

  Ab-functors : Precategory _ _
  Ab-functors .Ob          = Ab-functor π’œ ℬ
  Ab-functors .Hom F G     = F .functor => G .functor
  Ab-functors .Hom-set _ _ = Nat-is-set
  Ab-functors .id    = Cat[ A , B ] .Precategory.id
  Ab-functors ._∘_   = Cat[ A , B ] .Precategory._∘_
  Ab-functors .idr   = Cat[ A , B ] .Precategory.idr
  Ab-functors .idl   = Cat[ A , B ] .Precategory.idl
  Ab-functors .assoc = Cat[ A , B ] .Precategory.assoc

We can calculate that the natural transformations F⇒GF {\Rightarrow}G between Ab{{\mathbf{Ab}}}-functors have a pointwise abelian group structure. The most important thing to verify is that the pointwise sum of natural transformations is natural, which follows from multilinearity of the composition operation.

  [_,_]Ab : Ab-category Ab-functors
  [_,_]Ab .Group-on-hom F G = to-group-on grp where
    open make-group
    open Group-on
    module F = Ab-functor F
    module G = Ab-functor G

    grp : make-group (F .functor => G .functor)
    grp .mul f g .Ξ· x = f .Ξ· x B.+ g .Ξ· x
    grp .mul f g .is-natural x y h =
      (f .Ξ· y B.+ g .Ξ· y) B.∘ F.₁ h             β‰‘Λ˜βŸ¨ B.∘-linear-l _ _ _ βŸ©β‰‘Λ˜
      (f .Ξ· y B.∘ F.₁ h) B.+ (g .Ξ· y B.∘ F.₁ h) β‰‘βŸ¨ apβ‚‚ B._+_ (f .is-natural x y h) (g .is-natural x y h) βŸ©β‰‘
      (G.₁ h B.∘ f .Ξ· x) B.+ (G.₁ h B.∘ g .Ξ· x) β‰‘βŸ¨ B.∘-linear-r _ _ _ βŸ©β‰‘
      G.₁ h B.∘ (f .Ξ· x B.+ g .Ξ· x)             ∎

Specifically, given (Ξ·x+Ξ΅x)F(h)(\eta_x + {\varepsilon}_x)F(h), we can distribute F(h)F(h) into the composite, apply naturality to both summands, and distribute G(h)G(h) out of the composite on the left. Similar computations establish that the pointwise inverse of natural transformations is natural.

    grp .unit .Ξ· x = B.0m
    grp .unit .is-natural x y f = B.∘-zero-l βˆ™ sym (B.∘-zero-r)

    grp .inv f .Ξ· x = B.Hom.inverse (f .Ξ· x)
    grp .inv f .is-natural x y g =
      B.Hom.inverse (f .Ξ· y) B.∘ F.₁ g   β‰‘Λ˜βŸ¨ B.neg-∘-l βŸ©β‰‘Λ˜
      B.Hom.inverse ⌜ f .Ξ· y B.∘ F.₁ g ⌝ β‰‘βŸ¨ ap! (f .is-natural x y g) βŸ©β‰‘
      B.Hom.inverse (G.₁ g B.∘ f .Ξ· x)   β‰‘βŸ¨ B.neg-∘-r βŸ©β‰‘
      G.₁ g B.∘ B.Hom.inverse (f .Ξ· x)   ∎

    grp .assoc _ _ _ = Nat-path Ξ» _ β†’ sym B.Hom.associative
    grp .idl _ = Nat-path Ξ» x β†’ B.Hom.idl
    grp .invl _ = Nat-path Ξ» x β†’ B.Hom.inversel
    grp .invr _ = Nat-path Ξ» x β†’ B.Hom.inverser
    grp .group-is-set = Nat-is-set

  [_,_]Ab .Hom-grp-ab F G f g = Nat-path Ξ» x β†’ B.Hom.commutative
  [_,_]Ab .∘-linear-l f g h = Nat-path Ξ» x β†’ B.∘-linear-l _ _ _
  [_,_]Ab .∘-linear-r f g h = Nat-path Ξ» x β†’ B.∘-linear-r _ _ _

  1. i.e.Β those functors FF for which, for all a,ba, b, the Hom{\mathbf{Hom}}-mapping Fa,b:A(a,b)β†’B(F(a),F(b))F_{a,b} : \mathcal{A}(a,b) \to \mathcal{B}(F(a),F(b)) extends to a group homomorphism.β†©οΈŽ