---

Step * 1 2 2 of Lemma oal_omcp_wf


1. s : LOSet@i'
2. g : OGrp@i'
3. ∀j:|s|. IsMonHom{g↓hgrp,<oal_hgp(s;g), λk,v. inj(k,v), λh,f. umap(h,f)>.mon}(<oal_hgp(s;g), λk,v. inj(k,v), λh,f. uma\000Cp(h,f)>.inj j)
4. h : AbMon@i'
5. f : |s| ⟶ MonHom(g↓hgrp,h)@i
⊢ (<oal_hgp(s;g), λk,v. inj(k,v), λh,f. umap(h,f)>.umap h f) = !v:|<oal_hgp(s;g), λk,v. inj(k,v), λh,f. umap(h,f)>.mon| \000C⟶ |h|
                                                         (IsMonHom{<oal_hgp(s;g), λk,v. inj(k,v), λh,f. umap(h,f)>.mon,h\000C}(v)
                                                         ∧ (∀j:|s|
                                                              ((f j)
                                                              = (v o (<oal_hgp(s;g), λk,v. inj(k,v), λh,f. umap(h,f)>.in\000Cj j))
                                                              ∈ (|(g↓hgrp)| ⟶ |h|))))
BY
{ Force `6` (Reduce 0)⋅ }

1
1. s : LOSet@i'
2. g : OGrp@i'
3. ∀j:|s|. IsMonHom{g↓hgrp,<oal_hgp(s;g), λk,v. inj(k,v), λh,f. umap(h,f)>.mon}(<oal_hgp(s;g), λk,v. inj(k,v), λh,f. uma\000Cp(h,f)>.inj j)
4. h : AbMon@i'
5. f : |s| ⟶ MonHom(g↓hgrp,h)@i
⊢ umap(h,f) = !v:|oal(s;g↓hgrp)| ⟶ |h|
                (IsMonHom{oal_hgp(s;g),h}(v) ∧ (∀j:|s|. ((f j) = (v o (λv.inj(j,v))) ∈ (|g|+ ⟶ |h|))))

---

Latex:

---

Latex:

1.  s  :  LOSet@i'
2.  g  :  OGrp@i'
3.  \mforall{}j:|s|.  IsMonHom\{g\mdownarrow{}hgrp,<oal\_hgp(s;g),  \mlambda{}k,v.  inj(k,v),  \mlambda{}h,f.  umap(h,f)>.mon\}(<oal\_hgp(s;g),  \mlambda{}k,v.\000C  inj(k,v),  \mlambda{}h,f.  umap(h,f)>.inj  j)
4.  h  :  AbMon@i'
5.  f  :  |s|  {}\mrightarrow{}  MonHom(g\mdownarrow{}hgrp,h)@i
\mvdash{}  (<oal\_hgp(s;g),  \mlambda{}k,v.  inj(k,v),  \mlambda{}h,f.  umap(h,f)>.umap  h  f)  =  !v:|<oal\_hgp(s;g)
                                                                                                                      ,  \mlambda{}k,v.  inj(k,v)
                                                                                                                      ,  \mlambda{}h,f.  umap(h,f)>.mon|  {}\mrightarrow{}  |h|
                                                                                                                  (IsMonHom\{<oal\_hgp(s;g)
                                                                                                                                      ,  \mlambda{}k,v.  inj(k,v)
                                                                                                                                      ,  \mlambda{}h,f.  umap(h,f)>.mon,h\}(v)
                                                                                                                  \mwedge{}  (\mforall{}j:|s|
                                                                                                                            ((f  j)
                                                                                                                            =  (v  o  (<oal\_hgp(s;g)
                                                                                                                                            ,  \mlambda{}k,v.  inj(k,v)
                                                                                                                                            ,  \mlambda{}h,f.  umap(h,f)>.inj 
                                                                                                                                            j)))))


By

---

Latex:
Force  `6`  (Reduce  0)\mcdot{}

---

Home Index