Nuprl Definition : fmonalg
FMonAlg(g;a) ==
{m:fma_sig{i:l}(g;a)|
IsMonHom{g,m.alg↓rg↓xmn}(m.inj)
∧ (∀n:algebra{i:l}(a). ∀f:MonHom(g,n↓rg↓xmn).
(m.umap n f) = !f':m.alg.car ⟶ n.car. (alg_hom_p(a; m.alg; n; f') ∧ ((f' o m.inj) = f ∈ (|g| ⟶ n.car))))}
Definitions occuring in Statement :
fma_umap: f.umap,
fma_inj: f.inj,
fma_alg: f.alg,
fma_sig: fma_sig{i:l}(G;A),
alg_hom_p: alg_hom_p(a; m; n; f),
algebra: algebra{i:l}(A),
rng_of_alg: a↓rg,
alg_car: a.car,
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,
mul_mon_of_rng: r↓xmn,
monoid_hom: MonHom(M1,M2),
monoid_hom_p: IsMonHom{M1,M2}(f),
grp_car: |g|
Definitions occuring in definition :
set: {x:A| B[x]} ,
fma_sig: fma_sig{i:l}(G;A),
monoid_hom_p: IsMonHom{M1,M2}(f),
algebra: algebra{i:l}(A),
all: ∀x:A. B[x],
monoid_hom: MonHom(M1,M2),
mul_mon_of_rng: r↓xmn,
rng_of_alg: a↓rg,
uni_sat: a = !x:T. Q[x],
apply: f a,
fma_umap: f.umap,
and: P ∧ Q,
alg_hom_p: alg_hom_p(a; m; n; f),
fma_alg: f.alg,
equal: s = t ∈ T,
function: x:A ⟶ B[x],
grp_car: |g|,
alg_car: a.car,
compose: f o g,
fma_inj: f.inj
Latex:
FMonAlg(g;a) ==
\{m:fma\_sig\{i:l\}(g;a)|
IsMonHom\{g,m.alg\mdownarrow{}rg\mdownarrow{}xmn\}(m.inj)
\mwedge{} (\mforall{}n:algebra\{i:l\}(a). \mforall{}f:MonHom(g,n\mdownarrow{}rg\mdownarrow{}xmn).
(m.umap n f) = !f':m.alg.car {}\mrightarrow{} n.car. (alg\_hom\_p(a; m.alg; n; f') \mwedge{} ((f' o m.inj) = f)))\}
Date html generated:
2016_05_16-AM-08_14_23
Last ObjectModification:
2015_09_23-AM-09_52_41
Theory : polynom_1
Home
Index