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