module Algebra.Group.Ab.Free where

Free abelian groupsπŸ”—

We have already constructed the free group on a set and the free abelian group on a group; Composing these adjunctions, we obtain the free abelian group on a set.

Free-abelian : βˆ€ {β„“} β†’ Type β„“ β†’ Abelian-group β„“
Free-abelian T = Abelianise (Free-Group T)
    : βˆ€ {β„“} β†’ Free-abelian-functor {β„“} ⊣ Forget-structure (Group-structure β„“) F∘ Abβ†ͺGrp
  Free-abelian⊣Forget = LF⊣GR
    ( make-free-group)
    ( make-free-abelian)