open import 1Lab.Reflection.Induction

open import Algebra.Group.Cat.FinitelyComplete
open import Algebra.Group.Cat.Base
open import Algebra.Group

open import Cat.Diagram.Colimit.Finite
open import Cat.Diagram.Coproduct
open import Cat.Diagram.Pushout
open import Cat.Diagram.Zero
open import Cat.Prelude

open Finitely-cocomplete
open is-group-hom
open is-pushout
open Coproduct
open Pushout

module Algebra.Group.Free.Product {β} where


# Free products of groupsπ

Given two groups and their free product is the coproduct in the category of groups (not to be confused with the direct product which is the categorical product).

As the name suggests, we can describe the free product as the free group equipped with inclusions and In fact, we define a more general construction: the amalgamated free product of a span of groups which realises the pushout of this span.

module _ {A B C : Group β} (f : Groups.Hom C A) (g : Groups.Hom C B) where
private
module A = Group-on (A .snd)
module B = Group-on (B .snd)


We start by freely adding the group operations and enforcing the group axioms, just like for free groupsβ¦

  data Amalgamated : Type β where
_β_ : Amalgamated β Amalgamated β Amalgamated
inv : Amalgamated β Amalgamated
nil : Amalgamated

f-assoc : β x y z β x β (y β z) β‘ (x β y) β z
f-invl  : β x β inv x β x β‘ nil
f-idl   : β x β nil β x β‘ x


β¦we then throw in the inclusions of and which are required to be group homomorphisms and to make the pushout square commuteβ¦

    inl : β A β β Amalgamated
inl-hom : β a a' β inl (a A.β a') β‘ inl a β inl a'

inr : β B β β Amalgamated
inr-hom : β b b' β inr (b B.β b') β‘ inr b β inr b'

glue : (c : β C β) β inl (f # c) β‘ inr (g # c)


β¦finally, we truncate the resulting type to a set.

    squash : is-set Amalgamated

  unquoteDecl Amalgamated-elim-prop = make-elim-n 1
Amalgamated-elim-prop (quote Amalgamated)


As expected, this data perfectly assembles into a group together with homomorphisms and fitting into a square with and

  Amalgamated-free-product : Group β
inlα΄³ : Groups.Hom A Amalgamated-free-product
inrα΄³ : Groups.Hom B Amalgamated-free-product
glueα΄³ : inlα΄³ Groups.β f β‘ inrα΄³ Groups.β g

  Amalgamated-free-product = to-group fp where
fp : make-group Amalgamated
fp .make-group.group-is-set = squash
fp .make-group.unit = nil
fp .make-group.mul = _β_
fp .make-group.inv = inv
fp .make-group.assoc = f-assoc
fp .make-group.invl = f-invl
fp .make-group.idl = f-idl

inlα΄³ .hom = inl
inlα΄³ .preserves .pres-β = inl-hom

inrα΄³ .hom = inr
inrα΄³ .preserves .pres-β = inr-hom

glueα΄³ = ext glue


The universal property of the pushout is easy to verify.

  Groups-pushout : is-pushout (Groups β) f inlα΄³ g inrα΄³
Groups-pushout .square = glueα΄³
Groups-pushout .universal {Q} {p} {q} comm .hom = go where
module Q = Group-on (Q .snd)
go : Amalgamated β β Q β
go (x β y) = go x Q.β go y
go (inv x) = go x Q.β»ΒΉ
go nil = Q.unit
go (f-assoc x y z i) = Q.associative {go x} {go y} {go z} i
go (f-invl x i) = Q.inversel {go x} i
go (f-idl x i) = Q.idl {go x} i
go (inl a) = p # a
go (inl-hom a a' i) = p .preserves .pres-β a a' i
go (inr b) = q # b
go (inr-hom b b' i) = q .preserves .pres-β b b' i
go (glue c i) = unext comm c i
go (squash x y Ξ± Ξ² i j) =
Q.has-is-set (go x) (go y) (Ξ» i β go (Ξ± i)) (Ξ» i β go (Ξ² i)) i j
Groups-pushout .universal comm .preserves .pres-β _ _ = refl
Groups-pushout .universalβiβ = trivial!
Groups-pushout .universalβiβ = trivial!
Groups-pushout .unique {Q = Q} {colim' = u} commβ commβ = ext \$
Amalgamated-elim-prop (Ξ» _ β hlevel 1)
(Ξ» x p y q β u .preserves .pres-β x y β apβ Q._β_ p q)
(Ξ» x p β pres-inv (u .preserves) β ap Q._β»ΒΉ p)
(pres-id (u .preserves))
(unext commβ) (unext commβ)
where module Q = Group-on (Q .snd)

Groups-Pushout : Pushout (Groups β) f g
Groups-Pushout .coapex = Amalgamated-free-product
Groups-Pushout .iβ = inlα΄³
Groups-Pushout .iβ = inrα΄³
Groups-Pushout .has-is-po = Groups-pushout


Since the zero group is also an initial object, this shows that the category of groups is finitely cocomplete.

Groups-finitely-cocomplete : Finitely-cocomplete (Groups β)
Groups-finitely-cocomplete = with-pushouts (Groups _)
(Zero.initial βα΄³) Groups-Pushout


We thus get the free product of and by abstract nonsense, as the pushout of the span

Free-product : Group β β Group β β Group β
Free-product A B = Groups-finitely-cocomplete .coproducts A B .coapex