Nuprl Definition : algebra_hom
algebra_hom(A; M; N) ==
{f:module_hom(A; M; N)| FunThru2op(M.car;N.car;M.times;N.times;f) ∧ ((f M.one) = N.one ∈ N.car)}
Definitions occuring in Statement :
module_hom: module_hom(A; M; N),
alg_one: a.one,
alg_times: a.times,
alg_car: a.car,
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
equal: s = t ∈ T,
fun_thru_2op: FunThru2op(A;B;opa;opb;f)
Definitions occuring in definition :
set: {x:A| B[x]} ,
module_hom: module_hom(A; M; N),
and: P ∧ Q,
fun_thru_2op: FunThru2op(A;B;opa;opb;f),
alg_times: a.times,
equal: s = t ∈ T,
alg_car: a.car,
apply: f a,
alg_one: a.one
Latex:
algebra\_hom(A; M; N) ==
\{f:module\_hom(A; M; N)| FunThru2op(M.car;N.car;M.times;N.times;f) \mwedge{} ((f M.one) = N.one)\}
Date html generated:
2016_05_16-AM-07_28_04
Last ObjectModification:
2015_09_23-AM-09_51_08
Theory : algebras_1
Home
Index