open import Algebra.Group.Cat.FinitelyComplete
open import Algebra.Group.Cat.Base
open import Algebra.Group.Ab
open import Algebra.Group

open import Cat.Diagram.Product
open import Cat.Prelude

module Algebra.Group.Ab.Sum where

module _ {ℓ} (G H : Abelian-group ℓ) where
  private
    module G = Abelian-group-on (G .snd)
    module H = Abelian-group-on (H .snd)

Direct sum of abelian groups🔗

Let $G,H:\mathbf{Ab}$ be two abelian groups; We construct their coproduct in the category of abelian groups by equipping the set $G_0\times H_0$ with the “pointwise” group structure. While this might seem like an odd way of constructing a coproduct — after all, $G_0\times H_0$ is literally a product — remember that in $\mathbf{Ab}\text{-categories}$ (like $\mathbf{Ab}$ itself, in this case), finite products and coproducts coincide.

So, despite the name “direct sum”, and despite the preceding paragraph, the structure we build is actually the product in $\mathbf{Ab}$ of $G$ and $H\text{.}$ However, we do not refer to this limit as a product — opting to use “direct sum” instead — because the more important notion of product in $\mathbf{Ab}$ is the tensor product of abelian groups.

  _⊕_ : Abelian-group ℓ
  _⊕_ = from-commutative-group
    (Direct-product (Ab↪Grp .Functor.F₀ G) (Ab↪Grp .Functor.F₀ H))
    λ x y → Σ-pathp G.commutes H.commutes

module _ {ℓ} {G H : Abelian-group ℓ} where
  private
    module G = Abelian-group-on (G .snd)
    module H = Abelian-group-on (H .snd)
  open is-group-hom

The construction of the projection homomorphisms and the “limiting” homomorphism is as in $\mathbf{Sets}\text{:}$ The existence of a left adjoint free abelian group functor $\mathbf{Sets}\to \mathbf{Ab}$ implies that limits in $\mathbf{Ab}$ are computed as in $\mathbf{Sets}$ (namely, because the forgetful functor $U:\mathbf{Ab}\to \mathbf{Sets}$ is a right adjoint, and right adjoints preserve limits).

  ⊕-proj₁ : Ab.Hom (G ⊕ H) G
  ⊕-proj₁ .hom = fst
  ⊕-proj₁ .preserves .pres-⋆ x y = refl

  ⊕-proj₂ : Ab.Hom (G ⊕ H) H
  ⊕-proj₂ .hom = snd
  ⊕-proj₂ .preserves .pres-⋆ x y = refl

  open is-product
  Direct-sum-is-product : is-product (Ab ℓ) {A = G} {H} {G ⊕ H} ⊕-proj₁ ⊕-proj₂
  Direct-sum-is-product .⟨_,_⟩ f g .hom x = f # x , g # x
  Direct-sum-is-product .⟨_,_⟩ f g .preserves .pres-⋆ x y =
    Σ-pathp (f .preserves .pres-⋆ x y) (g .preserves .pres-⋆ x y)

  Direct-sum-is-product .π₁∘⟨⟩ = trivial!
  Direct-sum-is-product .π₂∘⟨⟩ = trivial!
  Direct-sum-is-product .unique p q = ext λ x → p #ₚ x , q #ₚ x