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 open import Cat.Diagram.Product 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 -categories (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 = 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)