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 on a type of generators. While we allow the parameter to be any type, these are best behaved in the case where is a set; In this case, 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 y β B x β 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 Iβve put it in a <details>
tag.
Free-elim-prop B bp bi bd binv bnil = go where go : β x β B x go (inc x) = bi x go (x β y) = bd x y (go x) (go y) go (inv x) = binv x (go x) go nil = bnil go (f-assoc x y z i) = is-propβpathp (Ξ» i β bp (f-assoc x y z i)) (bd x (y β z) (go x) (bd y z (go y) (go z))) (bd (x β y) z (bd x y (go x) (go y)) (go z)) i go (f-invl x i) = is-propβpathp (Ξ» i β bp (f-invl x i)) (bd (inv x) x (binv x (go x)) (go x)) bnil i go (f-idl x i) = is-propβpathp (Ξ» i β bp (f-idl x i)) (bd nil x bnil (go x)) (go x) i go (squash x y p q i j) = is-propβsquarep (Ξ» i j β bp (squash x y p q i j)) (Ξ» i β go x) (Ξ» i β go (p i)) (Ξ» i β go (q i)) (Ξ» i β go y) i j
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 , itβs β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 , we must come up with a group , with a map (in , where is the underlying set functor), such that, for any other group , any map can be factored uniquely as . As hinted above, we pick , the free group with 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 = Homomorphism-path $ Free-elim-prop _ (Ξ» _ β hlevel!) (p $β_) (Ξ» a b p 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 {β = β})