---

Step * 1 of Lemma free_abmon_unique


1. S : DSet
2. M : FAbMon(S)
3. N : FAbMon(S)
⊢ ∃f:MonHom(M.mon,N.mon). ∃g:MonHom(N.mon,M.mon). InvFuns(|M.mon|;|N.mon|;f;g)
BY
{ ((InstConcl  [M.umap N.mon N.inj;N.umap M.mon M.inj] 
THENM D 0) THENA Auto) }

1
1. S : DSet
2. M : FAbMon(S)
3. N : FAbMon(S)
⊢ ((N.umap M.mon M.inj) o (M.umap N.mon N.inj)) = Id{|M.mon|} ∈ (|M.mon| ⟶ |M.mon|)

2
1. S : DSet
2. M : FAbMon(S)
3. N : FAbMon(S)
⊢ ((M.umap N.mon N.inj) o (N.umap M.mon M.inj)) = Id{|N.mon|} ∈ (|N.mon| ⟶ |N.mon|)

---

Latex:

---

Latex:

1.  S  :  DSet
2.  M  :  FAbMon(S)
3.  N  :  FAbMon(S)
\mvdash{}  \mexists{}f:MonHom(M.mon,N.mon).  \mexists{}g:MonHom(N.mon,M.mon).  InvFuns(|M.mon|;|N.mon|;f;g)


By

---

Latex:
((InstConcl    [M.umap  N.mon  N.inj;N.umap  M.mon  M.inj] 
THENM  D  0)  THENA  Auto)

---

Home Index