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 module Algebra.Group.Ab.Sum where

# 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 \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 $\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.

_β_ : AbGroup β _β_ = restrict (Direct-product (G .object) (H .object)) ab where ab : is-abelian-group (Direct-product (G .object) (H .object) .snd) ab x y = Ξ£-pathp G.commutative H.commutative

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 \to \Ab$
implies that limits in
$\Ab$
are computed as in
$\sets$
(namely, because the *forgetful* functor
$U : \Ab \to \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 Ab.is-product Direct-sum-is-product : Ab.is-product {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 = Forget-is-faithful refl Direct-sum-is-product .Οββfactor = Forget-is-faithful refl Direct-sum-is-product .unique other p q = Forget-is-faithful $ funext Ξ» x β Ξ£-pathp (p #β x) (q #β x)