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:AbG, H : \Ab be two abelian groups; We construct their coproduct in the category of abelian groups by equipping the set G0Γ—H0G_0 \times H_0 with the β€œpointwise” group structure. While this might seem like an odd way of constructing a coproduct β€” after all, G0Γ—H0G_0 \times H_0 is literally a product β€” remember that in Ab\Ab-categories (like Ab\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\Ab of GG and HH. 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\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\sets: The existence of a left adjoint free abelian group functor Setsβ†’Ab\sets \to \Ab implies that limits in Ab\Ab are computed as in Sets\sets (namely, because the forgetful functor U:Abβ†’SetsU : \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)