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

open import Cat.Diagram.Initial
open import Cat.Functor.Adjoint
open import Cat.Instances.Comma
open import Cat.Prelude

module Algebra.Group.Free where

Free GroupsπŸ”—

We give a direct, higher-inductive constructor of the free group F(A)F(A) on a type AA of generators. While we allow the parameter to be any type, these are best behaved in the case where AA is a set; In this case, FF 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-invr : βˆ€ x β†’ x β—† inv 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 .fst = Free-group A
Free-Group A .snd = make-group squash nil _β—†_ inv f-assoc f-invl f-invr 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 (bd x y (go x) (go y)) (go z))
      (bd x (y β—† z) (go x) (bd y z (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-invr x i) =
    is-prop→pathp (λ i → bp (f-invr x i)) (bd x (inv x) (go x) (binv 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 .fst) β†’ Groups.Hom (Free-Group A) G
fold-free-group {A = A} {G = G , ggrp} map = 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 GG, it’s GG’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-invr x i) = G.inverser {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 Group-hom

  go-hom : Group-hom _ _ go
  go-hom .pres-⋆ x y = refl

Now, given a set SS, we must come up with a group GG, with a map η:S→U(G)\eta : S \to U(G) (in Sets\sets, where UU is the underlying set functor), such that, for any other group HH, any map S→U(H)S \to U(H) can be factored uniquely as S→ηU(G)→U(H)S \xrightarrow{\eta} U(G) \to U(H). As hinted above, we pick G=Free(S)G = \id{Free}(S), the free group with SS as its set of generators, and the universal map η\eta is in fact inc.

Free-universal-maps : βˆ€ s β†’ Universal-morphism s (Forget {β„“})
Free-universal-maps S = um where
  it : ↓Obj _ Forget
  it .x   = tt
  it .y   = Free-Group ∣ S ∣
  it .map = inc

To prove that this map is unique, suppose we have a group HH together with a map g:S→U(H)g : S \to U(H). We can insert Free(S)\id{Free}(S) in the middle by breaking this map down as

S→incU(Free(S)→fold(g)H) S \xrightarrow{\id{inc}} U(\id{Free}(S) \xrightarrow{\id{fold}(g)} H) 

  um : Initial _
  um .bot        = it
  um .hasβŠ₯ other = contr factor unique where
    g : ∣ S ∣ β†’ other .y .fst
    g = other .map

    factor : ↓Hom _ _ it other
    factor .Ξ±  = tt
    factor .Ξ²  = fold-free-group g
    factor .sq = refl

To show that this factorisation is unique, suppose we had some other group homomorphism gβ€²:Free(S)β†’Hg' : \id{Free}(S) \to H, which also has the property that U(gβ€²)∘inc=gU(g') \circ \id{inc} = g; We must show that it is equal to fold(g)\id{fold}(g), which we can do pointwise, so assume we have a x:Free(S)x : \id{Free}(S).

By induction on xx, it suffices to consider the cases where xx is a generator, or one of the group operations (inverses, multiplication, or the identity). The case for generators is the most interesting: We have some y:Sy : S, and must show that g(y)=U(gβ€²)(inc(y))g(y) = U(g')(\id{inc}(y)); but this is immediate, by assumption. The other cases all follow from the induction hypotheses and gβ€²g' being a group homomorphism.

    unique : βˆ€ x β†’ factor ≑ x
    unique factoring = ↓Hom-path _ _ refl path where abstract
      path : factor .Ξ² ≑ factoring .Ξ²
      path = Ξ£-prop-path (Ξ» _ β†’ Group-hom-is-prop)
        (funext (Free-elim-prop _ (Ξ» _ β†’ y other .snd .has-is-set _ _)
          (Ξ» x β†’ happly (factoring .sq) _)
          (Ξ» _ _ p q β†’ apβ‚‚ (other .y .snd ._⋆_) p q
                     βˆ™ sym (factoring .Ξ² .snd .pres-⋆ _ _))
          (Ξ» _ p β†’ ap (other .y .snd .inverse) p
                 βˆ™ sym (pres-inv (factoring .Ξ² .snd)))
          (sym (pres-id (factoring .Ξ² .snd)))))