module Algebra.Group.Free where

private variable β : Level A : Type β open is-group-hom open Group-on open Initial open βObj open βHom

# Free groupsπ

We give a direct, higher-inductive constructor of the **free
group
$F(A)$
on a type
$A$
of generators**. While we allow the parameter to be any type,
these are best behaved in the case where
$A$
is a set; In this case,
$F$
satisfies the expected universal property.

data Free-group (A : Type β) : Type β where inc : A β Free-group A

The higher-inductive presentation of free algebraic structures is very direct: There is no need to describe a set of words and then quotient by an appropriate (complicated) equivalence relation: we can define point constructors corresponding to the operations of a group, then add in the path constructors that make this into a group.

_β_ : Free-group A β Free-group A β Free-group A inv : Free-group A β Free-group A nil : Free-group A

We postulate precisely the data that is needed by `make-group`

. This is potentially
more data than is needed, but constructing maps out of `Free-group`

is most conveniently
done using the universal property, and there, this redundancy doesnβt
matter.

f-assoc : β x y z β x β (y β z) β‘ (x β y) β z f-invl : β x β inv x β x β‘ nil f-idl : β x β nil β x β‘ x squash : is-set (Free-group A)

We can package these constructors together to give a group with
underlying set `Free-group`

. See what was meant
by βprecisely the data needed by `make-group`

β?

Free-Group : Type β β Group β Free-Group A = to-group fg where fg : make-group (Free-group A) fg .make-group.group-is-set = squash fg .make-group.unit = nil fg .make-group.mul = _β_ fg .make-group.inv = inv fg .make-group.assoc = f-assoc fg .make-group.invl = f-invl fg .make-group.idl = f-idl

This lemma will be very useful later. It says that whenever you want
to prove a proposition by induction on `Free-group`

, it suffices to
address the value constructors. This is because propositions
automatically respect (higher) path constructors.

Free-elim-prop : β {β} (B : Free-group A β Type β) β (β x β is-prop (B x)) β (β x β B (inc x)) β (β x β B x β β y β B y β B (x β y)) β (β x β B x β B (inv x)) β B nil β β x β B x

The proof of it is a direct (by which I mean repetitive) case analysis, so we let our reflection machinery handle it for us.

unquoteDef Free-elim-prop = make-elim-with (default-elim-visible into 1) Free-elim-prop (quote Free-group)

## Universal propertyπ

We now prove the universal property of `Free-group`

, or, more
specifically, of the map `inc`

: It gives a universal way of
mapping from the category of sets to an object in the category of
groups, in that any map from a set to (the underlying set of) a group
factors uniquely through `inc`

. To establish
this result, we first implement a helper function, `fold-free-group`

, which, given
the data of where to send the generators of a free group, determines a
group homomorphism.

fold-free-group : {A : Type β} {G : Group β} β (A β β G β) β Groups.Hom (Free-Group A) G fold-free-group {A = A} {G = G , ggrp} map = total-hom go go-hom where module G = Group-on ggrp

While it might seem that there are many cases to consider when
defining the function `go`

, for most of them, our hand
is forced: For example, we must take multiplication in the free group
(the `_β_`

constructor) to multiplication in the codomain.

go : Free-group A β β£ G β£ go (inc x) = map x go (x β y) = go x G.β go y go (inv x) = go x G.β»ΒΉ go nil = G.unit

Since `_β_`

is
interpreted as multiplication in
$G,$
itβs
$Gβs$
associativity, identity and inverse laws that provide the cases for
`Free-group`

βs higher
constructors.

go (f-assoc x y z i) = G.associative {x = go x} {y = go y} {z = go z} i go (f-invl x i) = G.inversel {x = go x} i go (f-idl x i) = G.idl {x = go x} 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 open is-group-hom go-hom : is-group-hom _ _ go go-hom .pres-β x y = refl

Now, given a set
$S,$
we must come up with a group
$G,$
with a map
$Ξ·:SβU(G)$
(in
$Sets,$
where
$U$
is the underlying set
functor), such that, for any other group
$H,$
any map
$SβU(H)$
can be factored uniquely as
$SΞ·βU(G)βU(H).$
As hinted above, we pick
$G=Free(S),$
the free group with
$S$
as its set of generators, and the universal map
$Ξ·$
is in fact `inc`

.

make-free-group : make-left-adjoint (Forget {β}) make-free-group .Ml.free S = Free-Group β£ S β£ make-free-group .Ml.unit _ = inc make-free-group .Ml.universal f = fold-free-group f make-free-group .Ml.commutes f = refl make-free-group .Ml.unique {y = y} {g = g} p = ext $ Free-elim-prop _ (Ξ» _ β hlevel!) (p $β_) (Ξ» a p b q β apβ y._β_ p q β sym (g .preserves .is-group-hom.pres-β _ _)) (Ξ» a p β ap y.inverse p β sym (is-group-hom.pres-inv (g .preserves))) (sym (is-group-hom.pres-id (g .preserves))) where module y = Group-on (y .snd) module Free-groups {β} = make-left-adjoint (make-free-group {β = β})