44 and compatible_add: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y" |
44 and compatible_add: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y" |
45 and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>" |
45 and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>" |
46 shows "ring_hom_ring R S h" |
46 shows "ring_hom_ring R S h" |
47 apply unfold_locales |
47 apply unfold_locales |
48 apply (unfold ring_hom_def, safe) |
48 apply (unfold ring_hom_def, safe) |
49 apply (simp add: hom_closed Pi_def, assumption+) |
49 apply (simp add: hom_closed Pi_def) |
|
50 apply (erule (1) compatible_mult) |
|
51 apply (erule (1) compatible_add) |
|
52 apply (rule compatible_one) |
50 done |
53 done |
51 |
54 |
52 lemma ring_hom_ringI2: |
55 lemma ring_hom_ringI2: |
53 includes ring R + ring S |
56 includes ring R + ring S |
54 assumes h: "h \<in> ring_hom R S" |
57 assumes h: "h \<in> ring_hom R S" |
65 and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>" |
68 and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>" |
66 shows "ring_hom_ring R S h" |
69 shows "ring_hom_ring R S h" |
67 apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, assumption+) |
70 apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, assumption+) |
68 apply (insert group_hom.homh[OF a_group_hom]) |
71 apply (insert group_hom.homh[OF a_group_hom]) |
69 apply (unfold hom_def ring_hom_def, simp) |
72 apply (unfold hom_def ring_hom_def, simp) |
70 apply (safe, assumption+) |
73 apply safe |
|
74 apply (erule (1) compatible_mult) |
|
75 apply (rule compatible_one) |
71 done |
76 done |
72 |
77 |
73 lemma ring_hom_cringI: |
78 lemma ring_hom_cringI: |
74 includes ring_hom_ring R S h + cring R + cring S |
79 includes ring_hom_ring R S h + cring R + cring S |
75 shows "ring_hom_cring R S h" |
80 shows "ring_hom_cring R S h" |
76 by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro, assumption+, rule homh) |
81 by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro) |
|
82 (rule R.is_cring, rule S.is_cring, rule homh) |
77 |
83 |
78 |
84 |
79 subsection {* The kernel of a ring homomorphism *} |
85 subsection {* The kernel of a ring homomorphism *} |
80 |
86 |
81 --"the kernel of a ring homomorphism is an ideal" |
87 --"the kernel of a ring homomorphism is an ideal" |