module Algebra.Group.Ab.Sum where

Direct sum of abelian groupsπŸ”—

Let G,H:AbG, H : \mathbf{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\mathbf{Ab}-categories (like Ab\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 Ab\mathbf{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\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

The construction of the projection homomorphisms and the β€œlimiting” homomorphism is as in Sets\mathbf{Sets}: The existence of a left adjoint free abelian group functor Setsβ†’Ab\mathbf{Sets} \to \mathbf{Ab} implies that limits in Ab\mathbf{Ab} are computed as in Sets\mathbf{Sets} (namely, because the forgetful functor U:Abβ†’SetsU : \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)