src/HOL/Algebra/RingHom.thy
 author wenzelm Sun Mar 21 15:57:40 2010 +0100 (2010-03-21) changeset 35847 19f1f7066917 parent 30729 461ee3e49ad3 child 35849 b5522b51cb1e permissions -rw-r--r--
eliminated old constdefs;
1 (*
2   Title:     HOL/Algebra/RingHom.thy
3   Author:    Stephan Hohe, TU Muenchen
4 *)
6 theory RingHom
7 imports Ideal
8 begin
10 section {* Homomorphisms of Non-Commutative Rings *}
12 text {* Lifting existing lemmas in a @{text ring_hom_ring} locale *}
13 locale ring_hom_ring = R: ring R + S: ring S
14     for R (structure) and S (structure) +
15   fixes h
16   assumes homh: "h \<in> ring_hom R S"
17   notes hom_mult [simp] = ring_hom_mult [OF homh]
18     and hom_one [simp] = ring_hom_one [OF homh]
20 sublocale ring_hom_cring \<subseteq> ring: ring_hom_ring
21   proof qed (rule homh)
23 sublocale ring_hom_ring \<subseteq> abelian_group: abelian_group_hom R S
24 apply (rule abelian_group_homI)
25   apply (rule R.is_abelian_group)
26  apply (rule S.is_abelian_group)
27 apply (intro group_hom.intro group_hom_axioms.intro)
28   apply (rule R.a_group)
29  apply (rule S.a_group)
30 apply (insert homh, unfold hom_def ring_hom_def)
31 apply simp
32 done
34 lemma (in ring_hom_ring) is_ring_hom_ring:
35   "ring_hom_ring R S h"
36   by (rule ring_hom_ring_axioms)
38 lemma ring_hom_ringI:
39   fixes R (structure) and S (structure)
40   assumes "ring R" "ring S"
41   assumes (* morphism: "h \<in> carrier R \<rightarrow> carrier S" *)
42           hom_closed: "!!x. x \<in> carrier R ==> h x \<in> carrier S"
43       and compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^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>"
46   shows "ring_hom_ring R S h"
47 proof -
48   interpret ring R by fact
49   interpret ring S by fact
50   show ?thesis apply unfold_locales
51 apply (unfold ring_hom_def, safe)
52    apply (simp add: hom_closed Pi_def)
53   apply (erule (1) compatible_mult)
54  apply (erule (1) compatible_add)
55 apply (rule compatible_one)
56 done
57 qed
59 lemma ring_hom_ringI2:
60   assumes "ring R" "ring S"
61   assumes h: "h \<in> ring_hom R S"
62   shows "ring_hom_ring R S h"
63 proof -
64   interpret R: ring R by fact
65   interpret S: ring S by fact
66   show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
67     apply (rule R.is_ring)
68     apply (rule S.is_ring)
69     apply (rule h)
70     done
71 qed
73 lemma ring_hom_ringI3:
74   fixes R (structure) and S (structure)
75   assumes "abelian_group_hom R S h" "ring R" "ring S"
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>"
78   shows "ring_hom_ring R S h"
79 proof -
80   interpret abelian_group_hom R S h by fact
81   interpret R: ring R 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)
84     apply (insert group_hom.homh[OF a_group_hom])
85     apply (unfold hom_def ring_hom_def, simp)
86     apply safe
87     apply (erule (1) compatible_mult)
88     apply (rule compatible_one)
89     done
90 qed
92 lemma ring_hom_cringI:
93   assumes "ring_hom_ring R S h" "cring R" "cring S"
94   shows "ring_hom_cring R S h"
95 proof -
96   interpret ring_hom_ring R S h by fact
97   interpret R: cring R by fact
98   interpret S: cring S by fact
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)
101 qed
103 subsection {* The Kernel of a Ring Homomorphism *}
105 --"the kernel of a ring homomorphism is an ideal"
106 lemma (in ring_hom_ring) kernel_is_ideal:
107   shows "ideal (a_kernel R S h) R"
108 apply (rule idealI)
109    apply (rule R.is_ring)
111  apply (unfold a_kernel_def', simp+)
112 done
114 text {* Elements of the kernel are mapped to zero *}
115 lemma (in abelian_group_hom) kernel_zero [simp]:
116   "i \<in> a_kernel R S h \<Longrightarrow> h i = \<zero>\<^bsub>S\<^esub>"
117 by (simp add: a_kernel_defs)
120 subsection {* Cosets *}
122 text {* Cosets of the kernel correspond to the elements of the image of the homomorphism *}
123 lemma (in ring_hom_ring) rcos_imp_homeq:
124   assumes acarr: "a \<in> carrier R"
125       and xrcos: "x \<in> a_kernel R S h +> a"
126   shows "h x = h a"
127 proof -
128   interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
130   from xrcos
131       have "\<exists>i \<in> a_kernel R S h. x = i \<oplus> a" by (simp add: a_r_coset_defs)
132   from this obtain i
133       where iker: "i \<in> a_kernel R S h"
134         and x: "x = i \<oplus> a"
135       by fast+
136   note carr = acarr iker[THEN a_Hcarr]
138   from x
139       have "h x = h (i \<oplus> a)" by simp
140   also from carr
141       have "\<dots> = h i \<oplus>\<^bsub>S\<^esub> h a" by simp
142   also from iker
143       have "\<dots> = \<zero>\<^bsub>S\<^esub> \<oplus>\<^bsub>S\<^esub> h a" by simp
144   also from carr
145       have "\<dots> = h a" by simp
146   finally
147       show "h x = h a" .
148 qed
150 lemma (in ring_hom_ring) homeq_imp_rcos:
151   assumes acarr: "a \<in> carrier R"
152       and xcarr: "x \<in> carrier R"
153       and hx: "h x = h a"
154   shows "x \<in> a_kernel R S h +> a"
155 proof -
156   interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
158   note carr = acarr xcarr
159   note hcarr = acarr[THEN hom_closed] xcarr[THEN hom_closed]
161   from hx and hcarr
162       have a: "h x \<oplus>\<^bsub>S\<^esub> \<ominus>\<^bsub>S\<^esub>h a = \<zero>\<^bsub>S\<^esub>" by algebra
163   from carr
164       have "h x \<oplus>\<^bsub>S\<^esub> \<ominus>\<^bsub>S\<^esub>h a = h (x \<oplus> \<ominus>a)" by simp
165   from a and this
166       have b: "h (x \<oplus> \<ominus>a) = \<zero>\<^bsub>S\<^esub>" by simp
168   from carr have "x \<oplus> \<ominus>a \<in> carrier R" by simp
169   from this and b
170       have "x \<oplus> \<ominus>a \<in> a_kernel R S h"
171       unfolding a_kernel_def'
172       by fast
174   from this and carr
175       show "x \<in> a_kernel R S h +> a" by (simp add: a_rcos_module_rev)
176 qed
178 corollary (in ring_hom_ring) rcos_eq_homeq:
179   assumes acarr: "a \<in> carrier R"
180   shows "(a_kernel R S h) +> a = {x \<in> carrier R. h x = h a}"
181 apply rule defer 1
182 apply clarsimp defer 1
183 proof
184   interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
186   fix x
187   assume xrcos: "x \<in> a_kernel R S h +> a"
188   from acarr and this
189       have xcarr: "x \<in> carrier R"
190       by (rule a_elemrcos_carrier)
192   from xrcos
193       have "h x = h a" by (rule rcos_imp_homeq[OF acarr])
194   from xcarr and this
195       show "x \<in> {x \<in> carrier R. h x = h a}" by fast
196 next
197   interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
199   fix x
200   assume xcarr: "x \<in> carrier R"
201      and hx: "h x = h a"
202   from acarr xcarr hx
203       show "x \<in> a_kernel R S h +> a" by (rule homeq_imp_rcos)
204 qed
206 end