---

Step * 3 2 of Lemma free-group-adjunction


1. b1 : Group{i}
2. b2 : Group{i}
3. g : MonHom(b1,b2)
4. x : |b1|
⊢ ((g o fg-lift(b1;λg.g)) free-letter(x))
= ((fg-lift(b2;λg.g) o fg-lift(free-group(|b2|);λx.free-letter(g x))) free-letter(x))
∈ |b2|
BY
{ RepUR ``free-letter fg-lift fg-hom free-0 free-append`` 0 }

1
1. b1 : Group{i}
2. b2 : Group{i}
3. g : MonHom(b1,b2)
4. x : |b1|
⊢ (g (e * x)) = (e * (g x)) ∈ |b2|

---

Latex:

---

Latex:

1.  b1  :  Group\{i\}
2.  b2  :  Group\{i\}
3.  g  :  MonHom(b1,b2)
4.  x  :  |b1|
\mvdash{}  ((g  o  fg-lift(b1;\mlambda{}g.g))  free-letter(x))
=  ((fg-lift(b2;\mlambda{}g.g)  o  fg-lift(free-group(|b2|);\mlambda{}x.free-letter(g  x)))  free-letter(x))


By

---

Latex:
RepUR  ``free-letter  fg-lift  fg-hom  free-0  free-append``  0

---

Home Index