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.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 _ _ _ = 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.β©οΈ