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 ${{\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 .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 $(\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 .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 $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.↩︎