Nuprl Definition : fabgrp
FAbGrp(s) ==
{fg:fabgrp_sig{i:l}(s)|
∀g:AbGrp. ∀h:|s| ⟶ |g|.
(fg.umap g h) = !h':|fg.grp| ⟶ |g|. (IsMonHom{fg.grp,g}(h') ∧ ((h' o fg.inj) = h ∈ (|s| ⟶ |g|)))}
Definitions occuring in Statement :
fabgrp_umap: f.umap,
fabgrp_inj: f.inj,
fabgrp_grp: f.grp,
fabgrp_sig: fabgrp_sig{i:l}(s),
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_p: IsMonHom{M1,M2}(f),
abgrp: AbGrp,
grp_car: |g|,
set_car: |p|
Definitions occuring in definition :
set: {x:A| B[x]} ,
fabgrp_sig: fabgrp_sig{i:l}(s),
abgrp: AbGrp,
all: ∀x:A. B[x],
uni_sat: a = !x:T. Q[x],
apply: f a,
fabgrp_umap: f.umap,
and: P ∧ Q,
monoid_hom_p: IsMonHom{M1,M2}(f),
fabgrp_grp: f.grp,
equal: s = t ∈ T,
function: x:A ⟶ B[x],
set_car: |p|,
grp_car: |g|,
compose: f o g,
fabgrp_inj: f.inj
Latex:
FAbGrp(s) ==
\{fg:fabgrp\_sig\{i:l\}(s)|
\mforall{}g:AbGrp. \mforall{}h:|s| {}\mrightarrow{} |g|.
(fg.umap g h) = !h':|fg.grp| {}\mrightarrow{} |g|. (IsMonHom\{fg.grp,g\}(h') \mwedge{} ((h' o fg.inj) = h))\}
Date html generated:
2016_05_16-AM-08_13_33
Last ObjectModification:
2015_09_23-AM-09_52_32
Theory : polynom_1
Home
Index