module Algebra.Group.Ab.Sum where

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

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