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