module Cat.Abelian.Instances.Functor
  where

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.β†©οΈŽ