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.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

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