### 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