Nuprl Definition : mcopower
MCopower(s;g) ==
{c:mcopower_sig{i:l}(s;g)|
(∀j:|s|. IsMonHom{g,c.mon}(c.inj j))
∧ (∀h:AbMon. ∀f:|s| ⟶ MonHom(g,h).
(c.umap h f) = !v:|c.mon| ⟶ |h|. (IsMonHom{c.mon,h}(v) ∧ (∀j:|s|. ((f j) = (v o (c.inj j)) ∈ (|g| ⟶ |h|)))))}
Definitions occuring in Statement :
mcopower_umap: m.umap,
mcopower_inj: m.inj,
mcopower_mon: m.mon,
mcopower_sig: mcopower_sig{i:l}(s;g),
compose: f o g,
uni_sat: a = !x:T. Q[x],
all: ∀x:A. B[x],
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
equal: s = t ∈ T,
monoid_hom: MonHom(M1,M2),
monoid_hom_p: IsMonHom{M1,M2}(f),
abmonoid: AbMon,
grp_car: |g|,
set_car: |p|
Definitions occuring in definition :
set: {x:A| B[x]} ,
mcopower_sig: mcopower_sig{i:l}(s;g),
abmonoid: AbMon,
monoid_hom: MonHom(M1,M2),
uni_sat: a = !x:T. Q[x],
mcopower_umap: m.umap,
and: P ∧ Q,
monoid_hom_p: IsMonHom{M1,M2}(f),
mcopower_mon: m.mon,
all: ∀x:A. B[x],
set_car: |p|,
equal: s = t ∈ T,
function: x:A ⟶ B[x],
grp_car: |g|,
compose: f o g,
apply: f a,
mcopower_inj: m.inj
Latex:
MCopower(s;g) ==
\{c:mcopower\_sig\{i:l\}(s;g)|
(\mforall{}j:|s|. IsMonHom\{g,c.mon\}(c.inj j))
\mwedge{} (\mforall{}h:AbMon. \mforall{}f:|s| {}\mrightarrow{} MonHom(g,h).
(c.umap h f) = !v:|c.mon| {}\mrightarrow{} |h|
(IsMonHom\{c.mon,h\}(v) \mwedge{} (\mforall{}j:|s|. ((f j) = (v o (c.inj j))))))\}
Date html generated:
2016_05_16-AM-08_12_59
Last ObjectModification:
2015_09_23-AM-09_52_29
Theory : polynom_1
Home
Index