Nuprl Definition : gcopower
gcopower{i}(s;g) ==
{c:gcopower_sig{i:l}(s;g)|
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|)))))}
Definitions occuring in Statement :
grp_p: grp_p(g),
gcopower_umap: g1.umap,
gcopower_inj: g1.inj,
gcopower_grp: g1.grp,
gcopower_sig: gcopower_sig{i:l}(s;g),
eqfun_p: IsEqFun(T;eq),
comm: Comm(T;op),
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),
abgrp: AbGrp,
grp_op: *,
grp_eq: =b,
grp_car: |g|,
set_car: |p|
Definitions occuring in definition :
set: {x:A| B[x]} ,
gcopower_sig: gcopower_sig{i:l}(s;g),
eqfun_p: IsEqFun(T;eq),
grp_eq: =b,
grp_p: grp_p(g),
comm: Comm(T;op),
grp_op: *,
abgrp: AbGrp,
monoid_hom: MonHom(M1,M2),
uni_sat: a = !x:T. Q[x],
gcopower_umap: g1.umap,
and: P ∧ Q,
monoid_hom_p: IsMonHom{M1,M2}(f),
gcopower_grp: g1.grp,
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,
gcopower_inj: g1.inj
Latex:
gcopower\{i\}(s;g) ==
\{c:gcopower\_sig\{i:l\}(s;g)|
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))))))\}
Date html generated:
2016_05_16-AM-08_14_01
Last ObjectModification:
2015_09_23-AM-09_52_37
Theory : polynom_1
Home
Index