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 $\mathbf{Ab}$-categories $\mathcal{A}$ and $\mathcal{B}$, we define the $\mathbf{Ab}$-functors between them to be the functors $F : \mathcal{A} \to \mathcal{B}$ which additionally preserve homwise addition1. We can, mimicking the construction of the ordinary functor category, construct a category $[\mathcal{A}, \mathcal{B}]_{\mathbf{Ab}}$ consisting only of the $\mathbf{Ab}$-functors, and prove that it is also an $\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 \Rightarrow G$ between $\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 .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 $(\eta_x + \varepsilon_x)F(h)$, we can distribute $F(h)$ into the composite, apply naturality to both summands, and distribute $G(h)$ 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 _ _ _ = Nat-path Ξ» _ β B.Hom.associative
grp .idl _       = Nat-path Ξ» x β B.Hom.idl
grp .invl _      = Nat-path Ξ» x β B.Hom.inversel
grp .comm _ _    = Nat-path Ξ» x β B.Hom.commutes
grp .ab-is-set   = Nat-is-set

[_,_]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 $F$ for which, for all $a, b$, the $\mathbf{Hom}$-mapping $F_{a,b} : \mathcal{A}(a,b) \to \mathcal{B}(F(a),F(b))$ extends to a group homomorphism.β©οΈ