🔍

Equations Inline Footnotes

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

open import Cat.Displayed.Univalence.Thin
open import Cat.Functor.Bifunctor
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 ∫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\text{,}$ however, we’re less interested in the functions $G\to H\text{,}$ and more interested in the homomorphisms $G\to H\text{.}$ 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 .fst x = f · x B.* g · x
  make-ab-on-hom .mul f g .snd .pres-⋆ x y =
    f · (x A.* y) B.* g · (x A.* y)          ≡⟨ ap₂ B._*_ (f .snd .pres-⋆ x y) (g .snd .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 .fst x = B._⁻¹ (f · x)
  make-ab-on-hom .inv f .snd .pres-⋆ x y =
    f · (x A.* y) B.⁻¹            ≡⟨ ap B._⁻¹ (f .snd .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 .fst x = B.1g
  make-ab-on-hom .1g .snd .pres-⋆ x y = B.introl refl

  make-ab-on-hom .idl x       = ext λ x → B.idl
  make-ab-on-hom .assoc x y z = ext λ _ → B.associative
  make-ab-on-hom .invl x      = ext λ x → B.inversel
  make-ab-on-hom .comm x y    = ext λ x → B.commutes

open Make-bifunctor

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}\text{.}$

Ab-hom-functor : ∀ {ℓ} → Bifunctor (Ab ℓ ^op) (Ab ℓ) (Ab ℓ)
Ab-hom-functor = make-bifunctor λ where
  .F₀ A B → Ab[ A , B ]
  .lmap f .fst → Ab._∘ f
  .lmap f .snd .pres-⋆ x y → ext λ z → refl
  .rmap f .fst → f Ab.∘_
  .rmap f .snd .pres-⋆ x y → ext λ z → f .snd .pres-⋆ _ _
  .lmap-id → ext λ _  _ → refl
  .rmap-id → ext λ _ _ → refl
  .lmap-∘ f g → ext λ _ _ → refl
  .rmap-∘ f g → ext λ _ _ → refl
  .lrmap  f g → ext λ _ _ → refl