---

Step * 1 of Lemma gcopower_properties


1. s : DSet@i'
2. g : AbGrp@i'
3. c : gcopower_sig{i:l}(s;g)@i'
4. [%2] : IsEqFun(|c.grp|;=b)
∧ grp_p(c.grp)
∧ Comm(|c.grp|;*)
∧ (∀j:|s|. IsMonHom{g,c.grp}(c.inj j))
∧ (∀h:AbGrp. ∀f:|s| ⟶ MonHom(g,h).
     (c.umap h f) = !v:|c.grp| ⟶ |h|. (IsMonHom{c.grp,h}(v) ∧ (∀j:|s|. ((f j) = (v o (c.inj j)) ∈ (|g| ⟶ |h|)))))@i'
5. IsEqFun(|c.grp|;=b)
⊢ SqStable(grp_p(c.grp))
BY
{ Unfold `grp_p` 0 THEN Auto⋅ }

---

Latex:

---

Latex:

1.  s  :  DSet@i'
2.  g  :  AbGrp@i'
3.  c  :  gcopower\_sig\{i:l\}(s;g)@i'
4.  [\%2]  :  IsEqFun(|c.grp|;=\msubb{})
\mwedge{}  grp\_p(c.grp)
\mwedge{}  Comm(|c.grp|;*)
\mwedge{}  (\mforall{}j:|s|.  IsMonHom\{g,c.grp\}(c.inj  j))
\mwedge{}  (\mforall{}h:AbGrp.  \mforall{}f:|s|  {}\mrightarrow{}  MonHom(g,h).
          (c.umap  h  f)  =  !v:|c.grp|  {}\mrightarrow{}  |h|
                                            (IsMonHom\{c.grp,h\}(v)  \mwedge{}  (\mforall{}j:|s|.  ((f  j)  =  (v  o  (c.inj  j))))))@i'
5.  IsEqFun(|c.grp|;=\msubb{})
\mvdash{}  SqStable(grp\_p(c.grp))


By

---

Latex:
Unfold  `grp\_p`  0  THEN  Auto\mcdot{}

---

Home Index