1 (* Title: HOL/GroupTheory/Ring |
|
2 ID: $Id$ |
|
3 Author: Florian Kammueller, with new proofs by L C Paulson |
|
4 |
|
5 *) |
|
6 |
|
7 header{*Ring Theory*} |
|
8 |
|
9 theory Ring = Bij + Coset: |
|
10 |
|
11 |
|
12 subsection{*Definition of a Ring*} |
|
13 |
|
14 record 'a ring = "'a group" + |
|
15 prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<cdot>\<index>" 70) |
|
16 |
|
17 record 'a unit_ring = "'a ring" + |
|
18 one :: 'a ("\<one>\<index>") |
|
19 |
|
20 |
|
21 text{*Abbrevations for the left and right distributive laws*} |
|
22 constdefs |
|
23 distrib_l :: "['a set, ['a, 'a] => 'a, ['a, 'a] => 'a] => bool" |
|
24 "distrib_l A f g == |
|
25 (\<forall>x \<in> A. \<forall>y \<in> A. \<forall>z \<in> A. (f x (g y z) = g (f x y) (f x z)))" |
|
26 |
|
27 distrib_r :: "['a set, ['a, 'a] => 'a, ['a, 'a] => 'a] => bool" |
|
28 "distrib_r A f g == |
|
29 (\<forall>x \<in> A. \<forall>y \<in> A. \<forall>z \<in> A. (f (g y z) x = g (f y x) (f z x)))" |
|
30 |
|
31 |
|
32 locale ring = abelian_group R + |
|
33 assumes prod_funcset: "prod R \<in> carrier R \<rightarrow> carrier R \<rightarrow> carrier R" |
|
34 and prod_assoc: |
|
35 "[|x \<in> carrier R; y \<in> carrier R; z \<in> carrier R|] |
|
36 ==> (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)" |
|
37 and left: "distrib_l (carrier R) (prod R) (sum R)" |
|
38 and right: "distrib_r (carrier R) (prod R) (sum R)" |
|
39 |
|
40 constdefs |
|
41 Ring :: "('a,'b) ring_scheme set" |
|
42 "Ring == Collect ring" |
|
43 |
|
44 |
|
45 lemma ring_is_abelian_group: "ring(R) ==> abelian_group(R)" |
|
46 by (simp add: ring_def abelian_group_def) |
|
47 |
|
48 text{*Construction of a ring from a semigroup and an Abelian group*} |
|
49 lemma ringI: |
|
50 "[|abelian_group R; |
|
51 semigroup(|carrier = carrier R, sum = prod R|); |
|
52 distrib_l (carrier R) (prod R) (sum R); |
|
53 distrib_r (carrier R) (prod R) (sum R)|] ==> ring R" |
|
54 by (simp add: abelian_group_def ring_def ring_axioms_def semigroup_def) |
|
55 |
|
56 lemma (in ring) prod_closed [simp]: |
|
57 "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<cdot> y \<in> carrier R" |
|
58 apply (insert prod_funcset) |
|
59 apply (blast dest: funcset_mem) |
|
60 done |
|
61 |
|
62 declare ring.prod_closed [simp] |
|
63 |
|
64 lemma (in ring) sum_closed: |
|
65 "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<oplus> y \<in> carrier R" |
|
66 by simp |
|
67 |
|
68 declare ring.sum_closed [simp] |
|
69 |
|
70 lemma (in ring) distrib_left: |
|
71 "[|x \<in> carrier R; y \<in> carrier R; z \<in> carrier R|] |
|
72 ==> x \<cdot> (y \<oplus> z) = (x \<cdot> y) \<oplus> (x \<cdot> z)" |
|
73 apply (insert left) |
|
74 apply (simp add: distrib_l_def) |
|
75 done |
|
76 |
|
77 lemma (in ring) distrib_right: |
|
78 "[|x \<in> carrier R; y \<in> carrier R; z \<in> carrier R|] |
|
79 ==> (y \<oplus> z) \<cdot> x = (y \<cdot> x) \<oplus> (z \<cdot> x)" |
|
80 apply (insert right) |
|
81 apply (simp add: distrib_r_def) |
|
82 done |
|
83 |
|
84 lemma (in ring) prod_zero_left: "x \<in> carrier R ==> \<zero> \<cdot> x = \<zero>" |
|
85 by (simp add: idempotent_imp_zero distrib_right [symmetric]) |
|
86 |
|
87 lemma (in ring) prod_zero_right: "x \<in> carrier R ==> x \<cdot> \<zero> = \<zero>" |
|
88 by (simp add: idempotent_imp_zero distrib_left [symmetric]) |
|
89 |
|
90 lemma (in ring) prod_minus_left: |
|
91 "[|x \<in> carrier R; y \<in> carrier R|] |
|
92 ==> (\<ominus>x) \<cdot> y = \<ominus> (x \<cdot> y)" |
|
93 by (simp add: minus_unique prod_zero_left distrib_right [symmetric]) |
|
94 |
|
95 lemma (in ring) prod_minus_right: |
|
96 "[|x \<in> carrier R; y \<in> carrier R|] |
|
97 ==> x \<cdot> (\<ominus>y) = \<ominus> (x \<cdot> y)" |
|
98 by (simp add: minus_unique prod_zero_right distrib_left [symmetric]) |
|
99 |
|
100 |
|
101 subsection {*Example: The Ring of Integers*} |
|
102 |
|
103 constdefs |
|
104 integers :: "int ring" |
|
105 "integers == (|carrier = UNIV, |
|
106 sum = op +, |
|
107 gminus = (%x. -x), |
|
108 zero = 0::int, |
|
109 prod = op *|)" |
|
110 |
|
111 theorem ring_integers: "ring (integers)" |
|
112 by (simp add: integers_def ring_def ring_axioms_def |
|
113 distrib_l_def distrib_r_def |
|
114 zadd_zmult_distrib zadd_zmult_distrib2 |
|
115 abelian_group_axioms_def group_axioms_def semigroup_def) |
|
116 |
|
117 |
|
118 subsection {*Ring Homomorphisms*} |
|
119 |
|
120 constdefs |
|
121 ring_hom :: "[('a,'c)ring_scheme, ('b,'d)ring_scheme] => ('a => 'b)set" |
|
122 "ring_hom R R' == |
|
123 {h. h \<in> carrier R -> carrier R' & |
|
124 (\<forall>x \<in> carrier R. \<forall>y \<in> carrier R. h(sum R x y) = sum R' (h x) (h y)) & |
|
125 (\<forall>x \<in> carrier R. \<forall>y \<in> carrier R. h(prod R x y) = prod R' (h x) (h y))}" |
|
126 |
|
127 ring_auto :: "('a,'b)ring_scheme => ('a => 'a)set" |
|
128 "ring_auto R == ring_hom R R \<inter> Bij(carrier R)" |
|
129 |
|
130 RingAutoGroup :: "[('a,'c) ring_scheme] => ('a=>'a) group" |
|
131 "RingAutoGroup R == BijGroup (carrier R) (|carrier := ring_auto R |)" |
|
132 |
|
133 |
|
134 lemma ring_hom_subset_hom: "ring_hom R R' <= hom R R'" |
|
135 by (force simp add: ring_hom_def hom_def) |
|
136 |
|
137 subsection{*The Ring Automorphisms From a Group*} |
|
138 |
|
139 lemma id_in_ring_auto: "ring R ==> (%x: carrier R. x) \<in> ring_auto R" |
|
140 by (simp add: ring_auto_def ring_hom_def restrictI ring.axioms id_Bij) |
|
141 |
|
142 lemma restrict_Inv_ring_hom: |
|
143 "[|ring R; h \<in> ring_hom R R; h \<in> Bij (carrier R)|] |
|
144 ==> restrict (Inv (carrier R) h) (carrier R) \<in> ring_hom R R" |
|
145 by (simp add: ring.axioms group.axioms |
|
146 ring_hom_def Bij_Inv_mem restrictI |
|
147 semigroup.sum_funcset ring.prod_funcset Bij_Inv_lemma) |
|
148 |
|
149 text{*Ring automorphisms are a subgroup of the group of bijections over the |
|
150 ring's carrier, and thus a group*} |
|
151 lemma subgroup_ring_auto: |
|
152 "ring R ==> subgroup (ring_auto R) (BijGroup (carrier R))" |
|
153 apply (rule group.subgroupI) |
|
154 apply (rule group_BijGroup) |
|
155 apply (force simp add: ring_auto_def BijGroup_def) |
|
156 apply (blast dest: id_in_ring_auto) |
|
157 apply (simp add: ring_auto_def BijGroup_def restrict_Inv_Bij |
|
158 restrict_Inv_ring_hom) |
|
159 apply (simp add: ring_auto_def BijGroup_def compose_Bij) |
|
160 apply (simp add: ring_hom_def compose_def Pi_def) |
|
161 done |
|
162 |
|
163 lemma ring_auto: "ring R ==> group (RingAutoGroup R)" |
|
164 apply (drule subgroup_ring_auto) |
|
165 apply (simp add: subgroup_def RingAutoGroup_def) |
|
166 done |
|
167 |
|
168 |
|
169 subsection{*A Locale for a Pair of Rings and a Homomorphism*} |
|
170 |
|
171 locale ring_homomorphism = ring R + ring R' + |
|
172 fixes h |
|
173 assumes homh: "h \<in> ring_hom R R'" |
|
174 |
|
175 lemma ring_hom_sum: |
|
176 "[|h \<in> ring_hom R R'; x \<in> carrier R; y \<in> carrier R|] |
|
177 ==> h(sum R x y) = sum R' (h x) (h y)" |
|
178 by (simp add: ring_hom_def) |
|
179 |
|
180 lemma ring_hom_prod: |
|
181 "[|h \<in> ring_hom R R'; x \<in> carrier R; y \<in> carrier R|] |
|
182 ==> h(prod R x y) = prod R' (h x) (h y)" |
|
183 by (simp add: ring_hom_def) |
|
184 |
|
185 lemma ring_hom_closed: |
|
186 "[|h \<in> ring_hom G G'; x \<in> carrier G|] ==> h x \<in> carrier G'" |
|
187 by (auto simp add: ring_hom_def funcset_mem) |
|
188 |
|
189 lemma (in ring_homomorphism) ring_hom_sum [simp]: |
|
190 "[|x \<in> carrier R; y \<in> carrier R|] ==> h (x \<oplus>\<^sub>1 y) = (h x) \<oplus>\<^sub>2 (h y)" |
|
191 by (simp add: ring_hom_sum [OF homh]) |
|
192 |
|
193 lemma (in ring_homomorphism) ring_hom_prod [simp]: |
|
194 "[|x \<in> carrier R; y \<in> carrier R|] ==> h (x \<cdot>\<^sub>1 y) = (h x) \<cdot>\<^sub>2 (h y)" |
|
195 by (simp add: ring_hom_prod [OF homh]) |
|
196 |
|
197 lemma (in ring_homomorphism) group_homomorphism: "group_homomorphism R R' h" |
|
198 by (simp add: group_homomorphism_def group_homomorphism_axioms_def |
|
199 prems homh ring_hom_subset_hom [THEN subsetD]) |
|
200 |
|
201 lemma (in ring_homomorphism) hom_zero_closed [simp]: "h \<zero>\<^sub>1 \<in> carrier R'" |
|
202 by (simp add: ring_hom_closed [OF homh]) |
|
203 |
|
204 lemma (in ring_homomorphism) hom_zero [simp]: "h \<zero>\<^sub>1 = \<zero>\<^sub>2" |
|
205 by (rule group_homomorphism.hom_zero [OF group_homomorphism]) |
|
206 |
|
207 lemma (in ring_homomorphism) hom_minus_closed [simp]: |
|
208 "x \<in> carrier R ==> h (\<ominus>x) \<in> carrier R'" |
|
209 by (rule group_homomorphism.hom_minus_closed [OF group_homomorphism]) |
|
210 |
|
211 lemma (in ring_homomorphism) hom_minus [simp]: |
|
212 "x \<in> carrier R ==> h (\<ominus>\<^sub>1 x) = \<ominus>\<^sub>2 (h x)" |
|
213 by (rule group_homomorphism.hom_minus [OF group_homomorphism]) |
|
214 |
|
215 |
|
216 text{*Needed because the standard theorem @{text "ring_homomorphism.intro"} |
|
217 is unnatural.*} |
|
218 lemma ring_homomorphismI: |
|
219 "[|ring R; ring R'; h \<in> ring_hom R R'|] ==> ring_homomorphism R R' h" |
|
220 by (simp add: ring_def ring_homomorphism_def ring_homomorphism_axioms_def) |
|
221 |
|
222 end |
|