29 apply (insert homh, unfold hom_def ring_hom_def) |
29 apply (insert homh, unfold hom_def ring_hom_def) |
30 apply simp |
30 apply simp |
31 done |
31 done |
32 |
32 |
33 lemma (in ring_hom_ring) is_ring_hom_ring: |
33 lemma (in ring_hom_ring) is_ring_hom_ring: |
34 includes struct R + struct S |
34 "ring_hom_ring R S h" |
35 shows "ring_hom_ring R S h" |
35 by (rule ring_hom_ring_axioms) |
36 by (rule ring_hom_ring_axioms) |
|
37 |
36 |
38 lemma ring_hom_ringI: |
37 lemma ring_hom_ringI: |
39 includes ring R + ring S |
38 fixes R (structure) and S (structure) |
|
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: "!!x y. [| x : carrier R; y : 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: "!!x y. [| x : carrier R; y : 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 apply unfold_locales |
46 proof - |
|
47 interpret ring [R] by fact |
|
48 interpret ring [S] by fact |
|
49 show ?thesis apply unfold_locales |
47 apply (unfold ring_hom_def, safe) |
50 apply (unfold ring_hom_def, safe) |
48 apply (simp add: hom_closed Pi_def) |
51 apply (simp add: hom_closed Pi_def) |
49 apply (erule (1) compatible_mult) |
52 apply (erule (1) compatible_mult) |
50 apply (erule (1) compatible_add) |
53 apply (erule (1) compatible_add) |
51 apply (rule compatible_one) |
54 apply (rule compatible_one) |
52 done |
55 done |
|
56 qed |
53 |
57 |
54 lemma ring_hom_ringI2: |
58 lemma ring_hom_ringI2: |
55 includes ring R + ring S |
59 assumes "ring R" "ring S" |
56 assumes h: "h \<in> ring_hom R S" |
60 assumes h: "h \<in> ring_hom R S" |
57 shows "ring_hom_ring R S h" |
61 shows "ring_hom_ring R S h" |
58 apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro) |
62 proof - |
59 apply (rule R.is_ring) |
63 interpret R: ring [R] by fact |
60 apply (rule S.is_ring) |
64 interpret S: ring [S] by fact |
61 apply (rule h) |
65 show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro) |
62 done |
66 apply (rule R.is_ring) |
|
67 apply (rule S.is_ring) |
|
68 apply (rule h) |
|
69 done |
|
70 qed |
63 |
71 |
64 lemma ring_hom_ringI3: |
72 lemma ring_hom_ringI3: |
65 includes abelian_group_hom R S + ring R + ring S |
73 fixes R (structure) and S (structure) |
|
74 assumes "abelian_group_hom R S h" "ring R" "ring S" |
66 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: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y" |
67 and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>" |
76 and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>" |
68 shows "ring_hom_ring R S h" |
77 shows "ring_hom_ring R S h" |
69 apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring) |
78 proof - |
70 apply (insert group_hom.homh[OF a_group_hom]) |
79 interpret abelian_group_hom [R S h] by fact |
71 apply (unfold hom_def ring_hom_def, simp) |
80 interpret R: ring [R] by fact |
72 apply safe |
81 interpret S: ring [S] by fact |
73 apply (erule (1) compatible_mult) |
82 show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring) |
74 apply (rule compatible_one) |
83 apply (insert group_hom.homh[OF a_group_hom]) |
75 done |
84 apply (unfold hom_def ring_hom_def, simp) |
|
85 apply safe |
|
86 apply (erule (1) compatible_mult) |
|
87 apply (rule compatible_one) |
|
88 done |
|
89 qed |
76 |
90 |
77 lemma ring_hom_cringI: |
91 lemma ring_hom_cringI: |
78 includes ring_hom_ring R S h + cring R + cring S |
92 assumes "ring_hom_ring R S h" "cring R" "cring S" |
79 shows "ring_hom_cring R S h" |
93 shows "ring_hom_cring R S h" |
80 by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro) |
94 proof - |
|
95 interpret ring_hom_ring [R S h] by fact |
|
96 interpret R: cring [R] by fact |
|
97 interpret S: cring [S] by fact |
|
98 show ?thesis by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro) |
81 (rule R.is_cring, rule S.is_cring, rule homh) |
99 (rule R.is_cring, rule S.is_cring, rule homh) |
82 |
100 qed |
83 |
101 |
84 subsection {* The kernel of a ring homomorphism *} |
102 subsection {* The kernel of a ring homomorphism *} |
85 |
103 |
86 --"the kernel of a ring homomorphism is an ideal" |
104 --"the kernel of a ring homomorphism is an ideal" |
87 lemma (in ring_hom_ring) kernel_is_ideal: |
105 lemma (in ring_hom_ring) kernel_is_ideal: |