module Algebra.Group.Ab.Hom where

Maps between abelian groupsπŸ”—

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

It turns out that the answer is no: if you try to make Hom\mathbf{Hom} into a functor on Grp\mathbf{Grp}, equipping A→BA \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 Ab\mathbf{Ab}, this does work:

  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

It’s only a little more work to show that this extends to a functor AbopΓ—Abβ†’Ab\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