open import Algebra.Group.Ab
open import Algebra.Group

open import Cat.Displayed.Univalence.Thin
open import Cat.Instances.Product
open import Cat.Displayed.Total
open import Cat.Prelude

module Algebra.Group.Ab.Hom where


# Maps between abelian groupsπ

open is-group-hom
open Total-hom


As groups are an algebraic theory, if $G$ is a group, we can equip the set of functions $X \to G$ with the pointwise group structure. When considering a pair of groups $G, H$, however, weβre less interested in the functions $G \to H$, and more interested in the homomorphisms $G \to H$. Can these be equipped with a group structure?

It turns out that the answer is no: if you try to make $\mathbf{Hom}$ into a functor on $\mathbf{Grp}$, equipping $A \to B$ the pointwise group structure, you find out that the sum of group homomorphisms can not be shown to be a homomorphism. But when considering abelian groups, i.e.Β the category $\mathbf{Ab}$, this does work:

Abelian-group-on-hom
: β {β} (A B : Abelian-group β)
β Abelian-group-on (Ab.Hom A B)
Abelian-group-on-hom A B = to-abelian-group-on make-ab-on-hom module Hom-ab where
open make-abelian-group
private
module B = Abelian-group-on (B .snd)
module A = Abelian-group-on (A .snd)

make-ab-on-hom : make-abelian-group (Ab.Hom A B)
make-ab-on-hom .ab-is-set = Ab.Hom-set _ _

  make-ab-on-hom .mul f g .hom x = f .hom x B.* g .hom x
make-ab-on-hom .mul f g .preserves .pres-β x y =
f .hom (x A.* y) B.* g .hom (x A.* y)                β‘β¨ apβ B._*_ (f .preserves .pres-β x y) (g .preserves .pres-β x y) β©β‘
(f .hom x B.* f .hom y) B.* (g .hom x B.* g .hom y)  β‘β¨ B.pullr (B.pulll refl)  β©β‘
f .hom x B.* (f .hom y B.* g .hom x) B.* g .hom y    β‘β¨ (Ξ» i β f .hom x B.* B.commutes {x = f .hom y} {y = g .hom x} i B.* (g .hom y)) β©β‘
f .hom x B.* (g .hom x B.* f .hom y) B.* g .hom y    β‘β¨ B.pushr (B.pushl refl) β©β‘
(f .hom x B.* g .hom x) B.* (f .hom y B.* g .hom y)  β

make-ab-on-hom .inv f .hom x = B._β»ΒΉ (f .hom x)
make-ab-on-hom .inv f .preserves .pres-β x y =
f .hom (x A.* y) B.β»ΒΉ               β‘β¨ ap B._β»ΒΉ (f .preserves .pres-β x y) β©β‘
(f .hom x B.* f .hom y) B.β»ΒΉ        β‘β¨ B.inv-comm β©β‘
(f .hom y B.β»ΒΉ) B.* (f .hom x B.β»ΒΉ) β‘β¨ B.commutes β©β‘
(f .hom x B.β»ΒΉ) B.* (f .hom y B.β»ΒΉ) β

make-ab-on-hom .1g .hom x = B.1g
make-ab-on-hom .1g .preserves .pres-β x y = B.introl refl

  make-ab-on-hom .idl x       = Homomorphism-path Ξ» x β B.idl
make-ab-on-hom .assoc x y z = Homomorphism-path Ξ» _ β B.associative
make-ab-on-hom .invl x      = Homomorphism-path Ξ» x β B.inversel
make-ab-on-hom .comm x y    = Homomorphism-path Ξ» x β B.commutes

open Functor

Ab[_,_] : β {β} β Abelian-group β β Ab.Ob β Ab.Ob
β£ Ab[ A , B ] .fst β£ = _
Ab[ A , B ] .fst .is-tr = Ab.Hom-set A B
Ab[ A , B ] .snd = Abelian-group-on-hom A B


Itβs only a little more work to show that this extends to a functor $\mathbf{Ab}^{\mathrm{op}} \times \mathbf{Ab} \to \mathbf{Ab}$.

Ab-hom-functor : β {β} β Functor (Ab β ^op ΓαΆ Ab β) (Ab β)
Ab-hom-functor .Fβ (A , B) = Ab[ A , B ]
Ab-hom-functor .Fβ (f , g) .hom h = g Ab.β h Ab.β f
Ab-hom-functor .Fβ (f , g) .preserves .pres-β x y = Homomorphism-path Ξ» z β
g .preserves .pres-β _ _
Ab-hom-functor .F-id    = Homomorphism-path Ξ» _ β Homomorphism-path Ξ» x β refl
Ab-hom-functor .F-β f g = Homomorphism-path Ξ» _ β Homomorphism-path Ξ» x β refl