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
module _
  {o o' β„“ β„“'} {A : Precategory o β„“}   (π’œ : Ab-category A)
              {B : Precategory o' β„“'} (ℬ : Ab-category B)
  where
  private
    module A = Ab-category π’œ
    module B = Ab-category ℬ
  open Precategory
  open Ab-category
  open Ab-functor
  open _=>_

Ab-enriched functor categoriesπŸ”—

Recall that, for a pair of and we define the between them to be the functors which additionally preserve homwise addition1. We can, mimicking the construction of the ordinary functor category, construct a category consisting only of the and prove that it is also an 

  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 between 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 .Abelian-group-on-hom F G = to-abelian-group-on grp where
    open make-abelian-group
    open Group-on
    module F = Ab-functor F
    module G = Ab-functor G

    grp : make-abelian-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 we can distribute into the composite, apply naturality to both summands, and distribute out of the composite on the left. Similar computations establish that the pointwise inverse of natural transformations is natural.

    grp .1g .Ξ· x = B.0m
    grp .1g .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.∘-negatel ⟩
      B.Hom.inverse ⌜ f .Ξ· y B.∘ F.₁ g ⌝ β‰‘βŸ¨ ap! (f .is-natural x y g) ⟩
      B.Hom.inverse (G.₁ g B.∘ f .Ξ· x)   β‰‘βŸ¨ B.∘-negater ⟩
      G.₁ g B.∘ B.Hom.inverse (f .Ξ· x)   ∎

    grp .assoc _ _ _ = ext Ξ» _ β†’ B.Hom.associative
    grp .idl _       = ext Ξ» x β†’ B.Hom.idl
    grp .invl _      = ext Ξ» x β†’ B.Hom.inversel
    grp .comm _ _    = ext Ξ» x β†’ B.Hom.commutes
    grp .ab-is-set   = Nat-is-set

  [_,_]Ab .∘-linear-l f g h = ext Ξ» x β†’ B.∘-linear-l _ _ _
  [_,_]Ab .∘-linear-r f g h = ext Ξ» x β†’ B.∘-linear-r _ _ _

  1. i.e.Β those functors for which, for all the extends to a group homomorphism.β†©οΈŽ