---

Step * 1 of Lemma free_abmon_umap_properties


1. S : DSet
2. M : FAbMon(S)
3. N : AbMon
4. p : |S| ⟶ |N|
⊢ (((M.umap N p) o M.inj) = p ∈ (|S| ⟶ |N|))
∧ (∀f:MonHom(M.mon,N). (((f o M.inj) = p ∈ (|S| ⟶ |N|)) ⇒ (f = (M.umap N p) ∈ (|M.mon| ⟶ |N|))))
BY
{ D 2 THEN D 3 
THEN AbReduce 0 }

1
1. S : DSet
2. mon : AbMon
3. inj : |S| ⟶ |mon|
4. M2 : mon':AbMon ⟶ f':(|S| ⟶ |mon'|) ⟶ {!g:MonHom(mon,mon') | (g o inj) = f' ∈ (|S| ⟶ |mon'|)}
5. N : AbMon
6. p : |S| ⟶ |N|
⊢ (((M2 N p) o inj) = p ∈ (|S| ⟶ |N|))
∧ (∀f:MonHom(mon,N). (((f o inj) = p ∈ (|S| ⟶ |N|)) ⇒ (f = (M2 N p) ∈ (|mon| ⟶ |N|))))

---

Latex:

---

Latex:

1.  S  :  DSet
2.  M  :  FAbMon(S)
3.  N  :  AbMon
4.  p  :  |S|  {}\mrightarrow{}  |N|
\mvdash{}  (((M.umap  N  p)  o  M.inj)  =  p)  \mwedge{}  (\mforall{}f:MonHom(M.mon,N).  (((f  o  M.inj)  =  p)  {}\mRightarrow{}  (f  =  (M.umap  N  p))))


By

---

Latex:
D  2  THEN  D  3 
THEN  AbReduce  0

---

Home Index