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 be two abelian groups; We construct their coproduct in the category of abelian groups by equipping the set with the βpointwiseβ group structure. While this might seem like an odd way of constructing a coproduct β after all, is literally a product β remember that in (like 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 of and 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 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 The existence of a left adjoint free abelian group functor implies that limits in are computed as in (namely, because the forgetful functor 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 = trivial!
Direct-sum-is-product .Οββfactor = trivial!
Direct-sum-is-product .unique other p q = ext Ξ» x β p #β x , q #β x