open import Algebra.Group.Ab.Abelianisation
open import Algebra.Group.Cat.Base
open import Algebra.Group.Free
open import Algebra.Group.Ab
open import Algebra.Group

open import Cat.Functor.Adjoint.Compose
open import Cat.Functor.Adjoint
open import Cat.Prelude

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)

mutual
  Free-abelian-functor : βˆ€ {β„“} β†’ Functor (Sets β„“) (Ab β„“)
  Free-abelian-functor = _

  Free-abelian⊣Forget
    : βˆ€ {β„“} β†’ Free-abelian-functor {β„“} ⊣ Forget-structure (Group-structure β„“) F∘ Abβ†ͺGrp
  Free-abelian⊣Forget = LF⊣GR
    (Ml.to-left-adjoint make-free-group)
    (Ml.to-left-adjoint make-free-abelian)

open is-group-hom

module _ {β„“} (T : Type β„“) (t-set : is-set T) where
  functionβ†’free-ab-hom : (G : Abelian-group β„“) β†’ (T β†’ ⌞ G ⌟) β†’ Ab.Hom (Free-abelian T) G
  function→free-ab-hom G fn = morp where
    private module G = Abelian-group-on (G .snd)
    goβ‚€ : Free-group T β†’ ⌞ G ⌟
    go₀ = fold-free-group {G = G .fst , G.Abelian→Group-on} fn .hom

    go : ⌞ Free-abelian T ⌟ β†’ ⌞ G ⌟
    go (inc x)              = goβ‚€ x
    go (glue (a , b , c) i) = goβ‚€ a G.* G.commutes {goβ‚€ b} {goβ‚€ c} i
    go (squash x y p q i j) =
      G.has-is-set (go x) (go y) (Ξ» i β†’ go (p i)) (Ξ» i β†’ go (q i)) i j

    morp : Ab.Hom (Free-abelian T) G
    morp .hom = go
    morp .preserves .pres-⋆ = Coeq-elim-propβ‚‚ (Ξ» x y β†’ G.has-is-set _ _) Ξ» x y β†’ refl