---

We construct the free group ⌜free-group(X)⌝ for any type X.
We use ⌜X + X⌝ for the generators and their inverses.
Because X may not have decidable equality, we can't reduce the
words of the free group to canonical form (removing adjacent x x^-1 pairs).

But we can still construct the free group using a quotient type.

The universal property of the free group is 
free-group-hom   
   -- which shows that every map X ⟶ |G| lifts to a homomorphism
and
free-group-generators
   -- which shows that the lifting is unique.⋅

---

Definition: inverse-letters
a = -b ==
  ∃x:X. (((a = (inl x) ∈ (X + X)) ∧ (b = (inr x ) ∈ (X + X))) ∨ ((a = (inr x ) ∈ (X + X)) ∧ (b = (inl x) ∈ (X + X))))

Lemma: inverse-letters_wf
∀[X:Type]. ∀[a,b:X + X].  (a = -b ∈ ℙ)

Lemma: inverse-inverse-letters
∀[X:Type]. ∀[a,b,c:X + X].  (a = -b ⇒ c = -a ⇒ (c = b ∈ (X + X)))

Definition: word-rel
This is the relation that says that word w2 is obtained from word w1 by 
deleting and adjacent pair of letters  x,y that are inverses.
This implies that the length of w2 is strictly less than the length of w1,
so it is a well-founded relation.

In word-rel-diamond we prove that is has the diamond property,
so its transitive closure is confluent, and we can get an equivalence
relation ⌜word-equiv(X;w1;w2)⌝.⋅

word-rel(X;w1;w2) ==
  ∃x,y:X + X. ∃a,b:(X + X) List. (x = -y ∧ (w1 = (a @ [x; y] @ b) ∈ ((X + X) List)) ∧ (w2 = (a @ b) ∈ ((X + X) List)))

Lemma: word-rel_wf
∀[X:Type]. ∀[w1,w2:(X + X) List].  (word-rel(X;w1;w2) ∈ ℙ)

Lemma: word-rel-length
∀[X:Type]. ∀[w1,w2:(X + X) List].  ||w2|| < ||w1|| supposing word-rel(X;w1;w2)

Lemma: word-rel-diamond
∀[X:Type]
  ∀x,y,z:(X + X) List.
    (word-rel(X;x;y)
    ⇒ word-rel(X;x;z)
    ⇒ ((y = z ∈ ((X + X) List)) ∨ (∃w:(X + X) List. (word-rel(X;y;w) ∧ word-rel(X;z;w)))))

Lemma: word-rel-confluent
∀[X:Type]
  ∀b,w1,w:(X + X) List.
    ((λx,y. word-rel(X;x;y)^* b w1)
    ⇒ (λx,y. word-rel(X;x;y)^* b w)
    ⇒ (∃z:(X + X) List. ((λx,y. word-rel(X;x;y)^* w1 z) ∧ (λx,y. word-rel(X;x;y)^* w z))))

Definition: word-equiv
word-equiv(X;w1;w2) ==  ∃w:(X + X) List. ((λx,y. word-rel(X;x;y)^* w1 w) ∧ (λx,y. word-rel(X;x;y)^* w2 w))

Lemma: word-equiv_wf
∀[X:Type]. ∀[w1,w2:(X + X) List].  (word-equiv(X;w1;w2) ∈ ℙ)

Lemma: word-equiv-equiv
∀[X:Type]. EquivRel((X + X) List;w1,w2.word-equiv(X;w1;w2))

Definition: free-word
free-word(X) ==  w1,w2:(X + X) List//word-equiv(X;w1;w2)

Lemma: free-word_wf
∀[X:Type]. (free-word(X) ∈ Type)

Lemma: word-rel-append1
∀X:Type. ∀w1,x,y:(X + X) List.  (word-rel(X;x;y) ⇒ word-rel(X;x @ w1;y @ w1))

Lemma: word-rel-append2
∀X:Type. ∀w1,x,y:(X + X) List.  (word-rel(X;x;y) ⇒ word-rel(X;w1 @ x;w1 @ y))

Definition: free-append
w + w' ==  w @ w'

Lemma: free-append_wf
∀[X:Type]. ∀[w,w':free-word(X)].  (w + w' ∈ free-word(X))

Lemma: free-append-assoc
∀[X:Type]. ∀[x,y,z:free-word(X)].  (x + y + z = x + y + z ∈ free-word(X))

Definition: free-0
0 ==  []

Lemma: free-0_wf
∀[X:Type]. (0 ∈ free-word(X))

Lemma: free-append-0
∀[X:Type]. ∀[w:free-word(X)].  (w + 0 = w ∈ free-word(X))

Lemma: free-0-append
∀[X:Type]. ∀[w:free-word(X)].  (0 + w = w ∈ free-word(X))

Definition: free-word-inv
free-word-inv(w) ==  map(λx.case x of inl(a) => inr a  | inr(a) => inl a;rev(w))

Lemma: free-word-inv-append
∀[x:Top List]. ∀[y:Top].  (free-word-inv(x @ y) ~ free-word-inv(y) @ free-word-inv(x))

Lemma: free-word-inv_wf
∀[X:Type]. ∀[w:free-word(X)].  (free-word-inv(w) ∈ free-word(X))

Lemma: free-word-inv-append1
∀[X:Type]. ∀[x:free-word(X)].  (free-word-inv(x) + x = 0 ∈ free-word(X))

Lemma: free-word-inv-append2
∀[X:Type]. ∀[x:free-word(X)].  (x + free-word-inv(x) = 0 ∈ free-word(X))

Definition: free-group
free-group(X) ==  <free-word(X), λw,w'. tt, λw,w'. tt, λw,w'. w + w', 0, λw.free-word-inv(w)>

Lemma: free-group_wf
∀[X:Type]. (free-group(X) ∈ Group{i})

Definition: free-letter
free-letter(x) ==  [inl x]

Lemma: free-letter_wf
∀[X:Type]. ∀[x:X].  (free-letter(x) ∈ free-word(X))

Lemma: free-group-generators
∀[X:Type]
  ∀G:Group{i}
    ∀[f,g:MonHom(free-group(X),G)].
      f = g ∈ MonHom(free-group(X),G) supposing ∀x:X. ((f free-letter(x)) = (g free-letter(x)) ∈ |G|)

Definition: fg-hom
fg-hom(G;f;w) ==
  accumulate (with value x and list item u):
   x * case u of inl(a) => f a | inr(b) => ~ (f b)
  over list:
    w
  with starting value:
   e)

Lemma: fg-hom-append
∀[X:Type]. ∀[G:Group{i}]. ∀[f:X ⟶ |G|]. ∀[a,b:(X + X) List].
  (fg-hom(G;f;a @ b) = (fg-hom(G;f;a) * fg-hom(G;f;b)) ∈ |G|)

Lemma: fg-hom_wf
∀[X:Type]. ∀[G:Group{i}]. ∀[f:X ⟶ |G|]. ∀[w:free-word(X)].  (fg-hom(G;f;w) ∈ |G|)

Definition: fg-lift
fg-lift(G;f) ==  λw.fg-hom(G;f;w)

Lemma: fg-lift_wf
∀[X:Type]
  ∀G:Group{i}. ∀f:X ⟶ |G|.  (fg-lift(G;f) ∈ {F:MonHom(free-group(X),G)| ∀x:X. ((F free-letter(x)) = (f x) ∈ |G|)} )

Lemma: free-group-hom
∀[X:Type]. ∀G:Group{i}. ∀f:X ⟶ |G|.  ∃F:MonHom(free-group(X),G). ∀x:X. ((F free-letter(x)) = (f x) ∈ |G|)

Definition: free-group-functor
FreeGp ==  functor(ob(X) = free-group(X);arrow(X,Y,f) = fg-lift(free-group(Y);λx.free-letter(f x)))

Lemma: free-group-functor_wf
FreeGp ∈ Functor(TypeCat;Group)

Definition: forget-group
ForgetGroup ==  functor(ob(G) = |G|;arrow(G,H,f) = f)

Lemma: forget-group_wf
ForgetGroup ∈ Functor(Group;TypeCat)

Lemma: free-group-adjunction
FreeGp -| ForgetGroup



Home Index