src/HOL/Algebra/RingHom.thy
 author wenzelm Thu Nov 23 20:34:21 2006 +0100 (2006-11-23) changeset 21502 7f3ea2b3bab6 parent 20318 0e0ea63fe768 child 23350 50c5b0912a0c permissions -rw-r--r--
prefer antiquotations over LaTeX macros;
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
12 section {* Homomorphisms of Non-Commutative Rings *}
14 text {* Lifting existing lemmas in a @{text ring_hom_ring} locale *}
15 locale ring_hom_ring = ring R + ring S + var 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 interpretation ring_hom_cring \<subseteq> ring_hom_ring
21   by (unfold_locales, rule homh)
23 interpretation ring_hom_ring \<subseteq> 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   includes struct R + struct S
36   shows "ring_hom_ring R S h"
37 by -
39 lemma ring_hom_ringI:
40   includes 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 apply unfold_locales
48 apply (unfold ring_hom_def, safe)
49    apply (simp add: hom_closed Pi_def, assumption+)
50 done
52 lemma ring_hom_ringI2:
53   includes ring R + ring S
54   assumes "h \<in> ring_hom R S"
55   shows "ring_hom_ring R S h"
56 by (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
58 lemma ring_hom_ringI3:
59   includes abelian_group_hom R S + ring R + ring S
60   assumes compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
61       and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
62   shows "ring_hom_ring R S h"
63 apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, assumption+)
64 apply (insert group_hom.homh[OF a_group_hom])
65 apply (unfold hom_def ring_hom_def, simp)
66 apply (safe, assumption+)
67 done
69 lemma ring_hom_cringI:
70   includes ring_hom_ring R S h + cring R + cring S
71   shows "ring_hom_cring R S h"
72 by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro, assumption+, rule homh)
75 subsection {* The kernel of a ring homomorphism *}
77 --"the kernel of a ring homomorphism is an ideal"
78 lemma (in ring_hom_ring) kernel_is_ideal:
79   shows "ideal (a_kernel R S h) R"
80 apply (rule idealI)
81    apply (rule R.is_ring)
83  apply (unfold a_kernel_def', simp+)
84 done
86 text {* Elements of the kernel are mapped to zero *}
87 lemma (in abelian_group_hom) kernel_zero [simp]:
88   "i \<in> a_kernel R S h \<Longrightarrow> h i = \<zero>\<^bsub>S\<^esub>"
89 by (simp add: a_kernel_defs)
92 subsection {* Cosets *}
94 text {* Cosets of the kernel correspond to the elements of the image of the homomorphism *}
95 lemma (in ring_hom_ring) rcos_imp_homeq:
96   assumes acarr: "a \<in> carrier R"
97       and xrcos: "x \<in> a_kernel R S h +> a"
98   shows "h x = h a"
99 proof -
100   interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal)
102   from xrcos
103       have "\<exists>i \<in> a_kernel R S h. x = i \<oplus> a" by (simp add: a_r_coset_defs)
104   from this obtain i
105       where iker: "i \<in> a_kernel R S h"
106         and x: "x = i \<oplus> a"
107       by fast+
108   note carr = acarr iker[THEN a_Hcarr]
110   from x
111       have "h x = h (i \<oplus> a)" by simp
112   also from carr
113       have "\<dots> = h i \<oplus>\<^bsub>S\<^esub> h a" by simp
114   also from iker
115       have "\<dots> = \<zero>\<^bsub>S\<^esub> \<oplus>\<^bsub>S\<^esub> h a" by simp
116   also from carr
117       have "\<dots> = h a" by simp
118   finally
119       show "h x = h a" .
120 qed
122 lemma (in ring_hom_ring) homeq_imp_rcos:
123   assumes acarr: "a \<in> carrier R"
124       and xcarr: "x \<in> carrier R"
125       and hx: "h x = h a"
126   shows "x \<in> a_kernel R S h +> a"
127 proof -
128   interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal)
130   note carr = acarr xcarr
131   note hcarr = acarr[THEN hom_closed] xcarr[THEN hom_closed]
133   from hx and hcarr
134       have a: "h x \<oplus>\<^bsub>S\<^esub> \<ominus>\<^bsub>S\<^esub>h a = \<zero>\<^bsub>S\<^esub>" by algebra
135   from carr
136       have "h x \<oplus>\<^bsub>S\<^esub> \<ominus>\<^bsub>S\<^esub>h a = h (x \<oplus> \<ominus>a)" by simp
137   from a and this
138       have b: "h (x \<oplus> \<ominus>a) = \<zero>\<^bsub>S\<^esub>" by simp
140   from carr have "x \<oplus> \<ominus>a \<in> carrier R" by simp
141   from this and b
142       have "x \<oplus> \<ominus>a \<in> a_kernel R S h"
143       unfolding a_kernel_def'
144       by fast
146   from this and carr
147       show "x \<in> a_kernel R S h +> a" by (simp add: a_rcos_module_rev)
148 qed
150 corollary (in ring_hom_ring) rcos_eq_homeq:
151   assumes acarr: "a \<in> carrier R"
152   shows "(a_kernel R S h) +> a = {x \<in> carrier R. h x = h a}"
153 apply rule defer 1
154 apply clarsimp defer 1
155 proof
156   interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal)
158   fix x
159   assume xrcos: "x \<in> a_kernel R S h +> a"
160   from acarr and this
161       have xcarr: "x \<in> carrier R"
162       by (rule a_elemrcos_carrier)
164   from xrcos
165       have "h x = h a" by (rule rcos_imp_homeq[OF acarr])
166   from xcarr and this
167       show "x \<in> {x \<in> carrier R. h x = h a}" by fast
168 next
169   interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal)
171   fix x
172   assume xcarr: "x \<in> carrier R"
173      and hx: "h x = h a"
174   from acarr xcarr hx
175       show "x \<in> a_kernel R S h +> a" by (rule homeq_imp_rcos)
176 qed
178 end