src/HOL/Algebra/RingHom.thy
 author haftmann Mon Nov 17 17:00:55 2008 +0100 (2008-11-17) changeset 28823 dcbef866c9e2 parent 27717 21bbd410ba04 child 29237 e90d9d51106b permissions -rw-r--r--
tuned unfold_locales invocation
1 (*
2   Title:     HOL/Algebra/RingHom.thy
3   Id:        \$Id\$
4   Author:    Stephan Hohe, TU Muenchen
5 *)
7 theory RingHom
8 imports Ideal
9 begin
11 section {* Homomorphisms of Non-Commutative Rings *}
13 text {* Lifting existing lemmas in a @{text ring_hom_ring} locale *}
14 locale ring_hom_ring = ring R + ring S + var h +
15   assumes homh: "h \<in> ring_hom R S"
16   notes hom_mult [simp] = ring_hom_mult [OF homh]
17     and hom_one [simp] = ring_hom_one [OF homh]
19 interpretation ring_hom_cring \<subseteq> ring_hom_ring
20   proof qed (rule homh)
22 interpretation ring_hom_ring \<subseteq> abelian_group_hom R S
23 apply (rule abelian_group_homI)
24   apply (rule R.is_abelian_group)
25  apply (rule S.is_abelian_group)
26 apply (intro group_hom.intro group_hom_axioms.intro)
27   apply (rule R.a_group)
28  apply (rule S.a_group)
29 apply (insert homh, unfold hom_def ring_hom_def)
30 apply simp
31 done
33 lemma (in ring_hom_ring) is_ring_hom_ring:
34   "ring_hom_ring R S h"
35   by (rule ring_hom_ring_axioms)
37 lemma ring_hom_ringI:
38   fixes R (structure) and S (structure)
39   assumes "ring R" "ring S"
40   assumes (* morphism: "h \<in> carrier R \<rightarrow> 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"
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>"
45   shows "ring_hom_ring R S h"
46 proof -
47   interpret ring [R] by fact
48   interpret ring [S] by fact
49   show ?thesis apply unfold_locales
50 apply (unfold ring_hom_def, safe)
51    apply (simp add: hom_closed Pi_def)
52   apply (erule (1) compatible_mult)
53  apply (erule (1) compatible_add)
54 apply (rule compatible_one)
55 done
56 qed
58 lemma ring_hom_ringI2:
59   assumes "ring R" "ring S"
60   assumes h: "h \<in> ring_hom R S"
61   shows "ring_hom_ring R S h"
62 proof -
63   interpret R: ring [R] by fact
64   interpret S: ring [S] by fact
65   show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
66     apply (rule R.is_ring)
67     apply (rule S.is_ring)
68     apply (rule h)
69     done
70 qed
72 lemma ring_hom_ringI3:
73   fixes R (structure) and S (structure)
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"
76       and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
77   shows "ring_hom_ring R S h"
78 proof -
79   interpret abelian_group_hom [R S h] by fact
80   interpret R: ring [R] by fact
81   interpret S: ring [S] by fact
82   show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring)
83     apply (insert group_hom.homh[OF a_group_hom])
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
91 lemma ring_hom_cringI:
92   assumes "ring_hom_ring R S h" "cring R" "cring S"
93   shows "ring_hom_cring R S h"
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)
99     (rule R.is_cring, rule S.is_cring, rule homh)
100 qed
102 subsection {* The Kernel of a Ring Homomorphism *}
104 --"the kernel of a ring homomorphism is an ideal"
105 lemma (in ring_hom_ring) kernel_is_ideal:
106   shows "ideal (a_kernel R S h) R"
107 apply (rule idealI)
108    apply (rule R.is_ring)
110  apply (unfold a_kernel_def', simp+)
111 done
113 text {* Elements of the kernel are mapped to zero *}
114 lemma (in abelian_group_hom) kernel_zero [simp]:
115   "i \<in> a_kernel R S h \<Longrightarrow> h i = \<zero>\<^bsub>S\<^esub>"
116 by (simp add: a_kernel_defs)
119 subsection {* Cosets *}
121 text {* Cosets of the kernel correspond to the elements of the image of the homomorphism *}
122 lemma (in ring_hom_ring) rcos_imp_homeq:
123   assumes acarr: "a \<in> carrier R"
124       and xrcos: "x \<in> a_kernel R S h +> a"
125   shows "h x = h a"
126 proof -
127   interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal)
129   from xrcos
130       have "\<exists>i \<in> a_kernel R S h. x = i \<oplus> a" by (simp add: a_r_coset_defs)
131   from this obtain i
132       where iker: "i \<in> a_kernel R S h"
133         and x: "x = i \<oplus> a"
134       by fast+
135   note carr = acarr iker[THEN a_Hcarr]
137   from x
138       have "h x = h (i \<oplus> a)" by simp
139   also from carr
140       have "\<dots> = h i \<oplus>\<^bsub>S\<^esub> h a" by simp
141   also from iker
142       have "\<dots> = \<zero>\<^bsub>S\<^esub> \<oplus>\<^bsub>S\<^esub> h a" by simp
143   also from carr
144       have "\<dots> = h a" by simp
145   finally
146       show "h x = h a" .
147 qed
149 lemma (in ring_hom_ring) homeq_imp_rcos:
150   assumes acarr: "a \<in> carrier R"
151       and xcarr: "x \<in> carrier R"
152       and hx: "h x = h a"
153   shows "x \<in> a_kernel R S h +> a"
154 proof -
155   interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal)
157   note carr = acarr xcarr
158   note hcarr = acarr[THEN hom_closed] xcarr[THEN hom_closed]
160   from hx and hcarr
161       have a: "h x \<oplus>\<^bsub>S\<^esub> \<ominus>\<^bsub>S\<^esub>h a = \<zero>\<^bsub>S\<^esub>" by algebra
162   from carr
163       have "h x \<oplus>\<^bsub>S\<^esub> \<ominus>\<^bsub>S\<^esub>h a = h (x \<oplus> \<ominus>a)" by simp
164   from a and this
165       have b: "h (x \<oplus> \<ominus>a) = \<zero>\<^bsub>S\<^esub>" by simp
167   from carr have "x \<oplus> \<ominus>a \<in> carrier R" by simp
168   from this and b
169       have "x \<oplus> \<ominus>a \<in> a_kernel R S h"
170       unfolding a_kernel_def'
171       by fast
173   from this and carr
174       show "x \<in> a_kernel R S h +> a" by (simp add: a_rcos_module_rev)
175 qed
177 corollary (in ring_hom_ring) rcos_eq_homeq:
178   assumes acarr: "a \<in> carrier R"
179   shows "(a_kernel R S h) +> a = {x \<in> carrier R. h x = h a}"
180 apply rule defer 1
181 apply clarsimp defer 1
182 proof
183   interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal)
185   fix x
186   assume xrcos: "x \<in> a_kernel R S h +> a"
187   from acarr and this
188       have xcarr: "x \<in> carrier R"
189       by (rule a_elemrcos_carrier)
191   from xrcos
192       have "h x = h a" by (rule rcos_imp_homeq[OF acarr])
193   from xcarr and this
194       show "x \<in> {x \<in> carrier R. h x = h a}" by fast
195 next
196   interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal)
198   fix x
199   assume xcarr: "x \<in> carrier R"
200      and hx: "h x = h a"
201   from acarr xcarr hx
202       show "x \<in> a_kernel R S h +> a" by (rule homeq_imp_rcos)
203 qed
205 end