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