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

open import Cat.Diagram.Product

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}$-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$. 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}$: 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 .Οββfactor = Homomorphism-path Ξ» _ β refl
Direct-sum-is-product .Οββfactor = Homomorphism-path Ξ» _ β refl
Direct-sum-is-product .unique other p q = Homomorphism-path Ξ» x β
Ξ£-pathp (p #β x) (q #β x)