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:Ab$ be two abelian groups; We construct their coproduct in the category of abelian groups by equipping the set $G_{0}ΓH_{0}$ with the βpointwiseβ group structure. While this might seem like an odd way of constructing a coproduct β after all, $G_{0}ΓH_{0}$ is literally a product β remember that in $Ab-categories$ (like $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
$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
$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
$Sets:$
The existence of a left
adjoint free abelian group functor
$SetsβAb$
implies that limits in
$Ab$
are computed as in
$Sets$
(namely, because the *forgetful* functor
$U:Abβ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