module Algebra.Group.Ab.Hom where

Maps between abelian groups🔗

As groups are an algebraic theory, if is a group, we can equip the set of functions with the pointwise group structure. When considering a pair of groups however, we’re less interested in the functions and more interested in the homomorphisms Can these be equipped with a group structure?

It turns out that the answer is no: if you try to make into a functor on , equipping 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 , this does work:

  make-ab-on-hom .mul f g .hom x = f · x B.* g · x
  make-ab-on-hom .mul f g .preserves .pres-⋆ x y =
    f · (x A.* y) B.* g · (x A.* y)          ≡⟨ ap₂ B._*_ (f .preserves .pres-⋆ x y) (g .preserves .pres-⋆ x y) 
    (f · x B.* f · y) B.* (g · x B.* g · y)  ≡⟨ B.pullr (B.pulll refl)  
    f · x B.* (f · y B.* g · x) B.* g · y    ≡⟨  i  f · x B.* B.commutes {x = f · y} {y = g · x} i B.* (g · y)) 
    f · x B.* (g · x B.* f · y) B.* g · y    ≡⟨ B.pushr (B.pushl refl) 
    (f · x B.* g · x) B.* (f · y B.* g · y)  

  make-ab-on-hom .inv f .hom x = B._⁻¹ (f · x)
  make-ab-on-hom .inv f .preserves .pres-⋆ x y =
    f · (x A.* y) B.⁻¹            ≡⟨ ap B._⁻¹ (f .preserves .pres-⋆ x y) 
    (f · x B.* f · y) B.⁻¹        ≡⟨ B.inv-comm 
    (f · y B.⁻¹) B.* (f · x B.⁻¹) ≡⟨ B.commutes 
    (f · x B.⁻¹) B.* (f · y B.⁻¹) 

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

It’s only a little more work to show that this extends to a functor

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 = ext λ z 
  g .preserves .pres-⋆ _ _
Ab-hom-functor .F-id    = trivial!
Ab-hom-functor .F-∘ f g = trivial!