equal
deleted
inserted
replaced
59 lemma ring_hom_ringI2: |
59 lemma ring_hom_ringI2: |
60 assumes "ring R" "ring S" |
60 assumes "ring R" "ring S" |
61 assumes h: "h \<in> ring_hom R S" |
61 assumes h: "h \<in> ring_hom R S" |
62 shows "ring_hom_ring R S h" |
62 shows "ring_hom_ring R S h" |
63 proof - |
63 proof - |
64 interpret R!: ring R by fact |
64 interpret R: ring R by fact |
65 interpret S!: ring S by fact |
65 interpret S: ring S by fact |
66 show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro) |
66 show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro) |
67 apply (rule R.is_ring) |
67 apply (rule R.is_ring) |
68 apply (rule S.is_ring) |
68 apply (rule S.is_ring) |
69 apply (rule h) |
69 apply (rule h) |
70 done |
70 done |
76 assumes compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y" |
76 assumes compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y" |
77 and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>" |
77 and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>" |
78 shows "ring_hom_ring R S h" |
78 shows "ring_hom_ring R S h" |
79 proof - |
79 proof - |
80 interpret abelian_group_hom R S h by fact |
80 interpret abelian_group_hom R S h by fact |
81 interpret R!: ring R by fact |
81 interpret R: ring R by fact |
82 interpret S!: ring S by fact |
82 interpret S: ring S by fact |
83 show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring) |
83 show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring) |
84 apply (insert group_hom.homh[OF a_group_hom]) |
84 apply (insert group_hom.homh[OF a_group_hom]) |
85 apply (unfold hom_def ring_hom_def, simp) |
85 apply (unfold hom_def ring_hom_def, simp) |
86 apply safe |
86 apply safe |
87 apply (erule (1) compatible_mult) |
87 apply (erule (1) compatible_mult) |
92 lemma ring_hom_cringI: |
92 lemma ring_hom_cringI: |
93 assumes "ring_hom_ring R S h" "cring R" "cring S" |
93 assumes "ring_hom_ring R S h" "cring R" "cring S" |
94 shows "ring_hom_cring R S h" |
94 shows "ring_hom_cring R S h" |
95 proof - |
95 proof - |
96 interpret ring_hom_ring R S h by fact |
96 interpret ring_hom_ring R S h by fact |
97 interpret R!: cring R by fact |
97 interpret R: cring R by fact |
98 interpret S!: cring S by fact |
98 interpret S: cring S by fact |
99 show ?thesis by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro) |
99 show ?thesis by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro) |
100 (rule R.is_cring, rule S.is_cring, rule homh) |
100 (rule R.is_cring, rule S.is_cring, rule homh) |
101 qed |
101 qed |
102 |
102 |
103 subsection {* The Kernel of a Ring Homomorphism *} |
103 subsection {* The Kernel of a Ring Homomorphism *} |