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⊣Forget : ∀ {ℓ} → Free-abelian-functor {ℓ} ⊣ Ab↪Sets Free-abelian⊣Forget = LF⊣GR (free-objects→left-adjoint make-free-group) (free-objects→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 module G = Abelian-group-on (G .snd) go₀ : Free-group T → ⌞ G ⌟ go₀ = fold-free-group {G = G .fst , G.Abelian→Group-on} fn .fst 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 .fst = go morp .snd .pres-⋆ = elim! λ x y → refl