---

Step * 3 of Lemma free-group-adjunction


1. b1 : Group{i}
2. b2 : Group{i}
3. g : MonHom(b1,b2)
⊢ (g o fg-lift(b1;λg.g))
= (fg-lift(b2;λg.g) o fg-lift(free-group(|b2|);λx.free-letter(g x)))
∈ MonHom(free-group(|b1|),b2)
BY
{ (BLemma `free-group-generators` THEN Auto) }

1
1. b1 : Group{i}
2. b2 : Group{i}
3. g : MonHom(b1,b2)
⊢ fg-lift(free-group(|b2|);λx.free-letter(g x)) ∈ MonHom(free-group(|b1|),free-group(|b2|))

2
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|

---

Latex:

---

Latex:

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


By

---

Latex:
(BLemma  `free-group-generators`  THEN  Auto)

---

Home Index