equal
deleted
inserted
replaced
37 lemma ring_hom_ringI: |
37 lemma ring_hom_ringI: |
38 fixes R (structure) and S (structure) |
38 fixes R (structure) and S (structure) |
39 assumes "ring R" "ring S" |
39 assumes "ring R" "ring S" |
40 assumes (* morphism: "h \<in> carrier R \<rightarrow> carrier S" *) |
40 assumes (* morphism: "h \<in> carrier R \<rightarrow> carrier S" *) |
41 hom_closed: "!!x. x \<in> carrier R ==> h x \<in> carrier S" |
41 hom_closed: "!!x. x \<in> carrier R ==> h x \<in> carrier S" |
42 and compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y" |
42 and compatible_mult: "\<And>x y. [| x \<in> carrier R; y \<in> carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y" |
43 and compatible_add: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y" |
43 and compatible_add: "\<And>x y. [| x \<in> carrier R; y \<in> carrier R |] ==> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y" |
44 and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>" |
44 and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>" |
45 shows "ring_hom_ring R S h" |
45 shows "ring_hom_ring R S h" |
46 proof - |
46 proof - |
47 interpret ring R by fact |
47 interpret ring R by fact |
48 interpret ring S by fact |
48 interpret ring S by fact |
70 qed |
70 qed |
71 |
71 |
72 lemma ring_hom_ringI3: |
72 lemma ring_hom_ringI3: |
73 fixes R (structure) and S (structure) |
73 fixes R (structure) and S (structure) |
74 assumes "abelian_group_hom R S h" "ring R" "ring S" |
74 assumes "abelian_group_hom R S h" "ring R" "ring S" |
75 assumes compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y" |
75 assumes compatible_mult: "\<And>x y. [| x \<in> carrier R; y \<in> carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y" |
76 and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>" |
76 and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>" |
77 shows "ring_hom_ring R S h" |
77 shows "ring_hom_ring R S h" |
78 proof - |
78 proof - |
79 interpret abelian_group_hom R S h by fact |
79 interpret abelian_group_hom R S h by fact |
80 interpret R: ring R by fact |
80 interpret R: ring R by fact |