---

Step * 1 of Lemma fmonalg_properties


1. g : AbMon
2. a : CRng
3. m : FMonAlg(g;a)
⊢ IsMonHom{g,m.alg↓rg↓xmn}(m.inj)
∧ (∀n:algebra{i:l}(a). ∀f:MonHom(g,n↓rg↓xmn).
     (m.umap n f) = !f':m.alg.car ⟶ n.car. (alg_hom_p(a; m.alg; n; f') ∧ ((f' o m.inj) = f ∈ (|g| ⟶ n.car))))
BY
{ D (-1) }

1
1. g : AbMon
2. a : CRng
3. m : fma_sig{i:l}(g;a)
4. [%1] : IsMonHom{g,m.alg↓rg↓xmn}(m.inj)
∧ (∀n:algebra{i:l}(a). ∀f:MonHom(g,n↓rg↓xmn).
     (m.umap n f) = !f':m.alg.car ⟶ n.car. (alg_hom_p(a; m.alg; n; f') ∧ ((f' o m.inj) = f ∈ (|g| ⟶ n.car))))
⊢ IsMonHom{g,m.alg↓rg↓xmn}(m.inj)
∧ (∀n:algebra{i:l}(a). ∀f:MonHom(g,n↓rg↓xmn).
     (m.umap n f) = !f':m.alg.car ⟶ n.car. (alg_hom_p(a; m.alg; n; f') ∧ ((f' o m.inj) = f ∈ (|g| ⟶ n.car))))

---

Latex:

---

Latex:

1.  g  :  AbMon
2.  a  :  CRng
3.  m  :  FMonAlg(g;a)
\mvdash{}  IsMonHom\{g,m.alg\mdownarrow{}rg\mdownarrow{}xmn\}(m.inj)
\mwedge{}  (\mforall{}n:algebra\{i:l\}(a).  \mforall{}f:MonHom(g,n\mdownarrow{}rg\mdownarrow{}xmn).
          (m.umap  n  f)  =  !f':m.alg.car  {}\mrightarrow{}  n.car.  (alg\_hom\_p(a;  m.alg;  n;  f')  \mwedge{}  ((f'  o  m.inj)  =  f)))


By

---

Latex:
D  (-1)

---

Home Index