ballarin@20318
|
1 |
(*
|
ballarin@20318
|
2 |
Title: HOL/Algebra/CIdeal.thy
|
ballarin@20318
|
3 |
Id: $Id$
|
ballarin@20318
|
4 |
Author: Stephan Hohe, TU Muenchen
|
ballarin@20318
|
5 |
*)
|
ballarin@20318
|
6 |
|
ballarin@20318
|
7 |
theory Ideal
|
ballarin@20318
|
8 |
imports Ring AbelCoset
|
ballarin@20318
|
9 |
begin
|
ballarin@20318
|
10 |
|
ballarin@20318
|
11 |
section {* Ideals *}
|
ballarin@20318
|
12 |
|
ballarin@20318
|
13 |
subsection {* General definition *}
|
ballarin@20318
|
14 |
|
ballarin@20318
|
15 |
locale ideal = additive_subgroup I R + ring R +
|
ballarin@20318
|
16 |
assumes I_l_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
|
ballarin@20318
|
17 |
and I_r_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
|
ballarin@20318
|
18 |
|
ballarin@20318
|
19 |
interpretation ideal \<subseteq> abelian_subgroup I R
|
ballarin@20318
|
20 |
apply (intro abelian_subgroupI3 abelian_group.intro)
|
wenzelm@23463
|
21 |
apply (rule ideal.axioms, rule ideal_axioms)
|
wenzelm@23463
|
22 |
apply (rule abelian_group.axioms, rule ring.axioms, rule ideal.axioms, rule ideal_axioms)
|
wenzelm@23463
|
23 |
apply (rule abelian_group.axioms, rule ring.axioms, rule ideal.axioms, rule ideal_axioms)
|
ballarin@20318
|
24 |
done
|
ballarin@20318
|
25 |
|
ballarin@20318
|
26 |
lemma (in ideal) is_ideal:
|
ballarin@20318
|
27 |
"ideal I R"
|
wenzelm@26203
|
28 |
by (rule ideal_axioms)
|
ballarin@20318
|
29 |
|
ballarin@20318
|
30 |
lemma idealI:
|
ballarin@27611
|
31 |
fixes R (structure)
|
ballarin@27611
|
32 |
assumes "ring R"
|
ballarin@20318
|
33 |
assumes a_subgroup: "subgroup I \<lparr>carrier = carrier R, mult = add R, one = zero R\<rparr>"
|
ballarin@20318
|
34 |
and I_l_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
|
ballarin@20318
|
35 |
and I_r_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
|
ballarin@20318
|
36 |
shows "ideal I R"
|
ballarin@27611
|
37 |
proof -
|
ballarin@27611
|
38 |
interpret ring [R] by fact
|
ballarin@27611
|
39 |
show ?thesis apply (intro ideal.intro ideal_axioms.intro additive_subgroupI)
|
wenzelm@23463
|
40 |
apply (rule a_subgroup)
|
wenzelm@23463
|
41 |
apply (rule is_ring)
|
wenzelm@23463
|
42 |
apply (erule (1) I_l_closed)
|
wenzelm@23463
|
43 |
apply (erule (1) I_r_closed)
|
wenzelm@23463
|
44 |
done
|
ballarin@27611
|
45 |
qed
|
ballarin@20318
|
46 |
|
ballarin@20318
|
47 |
subsection {* Ideals Generated by a Subset of @{term [locale=ring] "carrier R"} *}
|
ballarin@20318
|
48 |
|
ballarin@20318
|
49 |
constdefs (structure R)
|
ballarin@20318
|
50 |
genideal :: "('a, 'b) ring_scheme \<Rightarrow> 'a set \<Rightarrow> 'a set" ("Idl\<index> _" [80] 79)
|
ballarin@20318
|
51 |
"genideal R S \<equiv> Inter {I. ideal I R \<and> S \<subseteq> I}"
|
ballarin@20318
|
52 |
|
ballarin@20318
|
53 |
|
ballarin@20318
|
54 |
subsection {* Principal Ideals *}
|
ballarin@20318
|
55 |
|
ballarin@20318
|
56 |
locale principalideal = ideal +
|
ballarin@20318
|
57 |
assumes generate: "\<exists>i \<in> carrier R. I = Idl {i}"
|
ballarin@20318
|
58 |
|
ballarin@20318
|
59 |
lemma (in principalideal) is_principalideal:
|
ballarin@20318
|
60 |
shows "principalideal I R"
|
wenzelm@26203
|
61 |
by (rule principalideal_axioms)
|
ballarin@20318
|
62 |
|
ballarin@20318
|
63 |
lemma principalidealI:
|
ballarin@27611
|
64 |
fixes R (structure)
|
ballarin@27611
|
65 |
assumes "ideal I R"
|
ballarin@20318
|
66 |
assumes generate: "\<exists>i \<in> carrier R. I = Idl {i}"
|
ballarin@20318
|
67 |
shows "principalideal I R"
|
ballarin@27611
|
68 |
proof -
|
ballarin@27611
|
69 |
interpret ideal [I R] by fact
|
ballarin@27611
|
70 |
show ?thesis by (intro principalideal.intro principalideal_axioms.intro) (rule is_ideal, rule generate)
|
ballarin@27611
|
71 |
qed
|
ballarin@20318
|
72 |
|
ballarin@20318
|
73 |
subsection {* Maximal Ideals *}
|
ballarin@20318
|
74 |
|
ballarin@20318
|
75 |
locale maximalideal = ideal +
|
ballarin@20318
|
76 |
assumes I_notcarr: "carrier R \<noteq> I"
|
ballarin@20318
|
77 |
and I_maximal: "\<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> J = I \<or> J = carrier R"
|
ballarin@20318
|
78 |
|
ballarin@20318
|
79 |
lemma (in maximalideal) is_maximalideal:
|
ballarin@20318
|
80 |
shows "maximalideal I R"
|
wenzelm@26203
|
81 |
by (rule maximalideal_axioms)
|
ballarin@20318
|
82 |
|
ballarin@20318
|
83 |
lemma maximalidealI:
|
ballarin@27611
|
84 |
fixes R
|
ballarin@27611
|
85 |
assumes "ideal I R"
|
ballarin@20318
|
86 |
assumes I_notcarr: "carrier R \<noteq> I"
|
ballarin@20318
|
87 |
and I_maximal: "\<And>J. \<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> J = I \<or> J = carrier R"
|
ballarin@20318
|
88 |
shows "maximalideal I R"
|
ballarin@27611
|
89 |
proof -
|
ballarin@27611
|
90 |
interpret ideal [I R] by fact
|
ballarin@27611
|
91 |
show ?thesis by (intro maximalideal.intro maximalideal_axioms.intro)
|
wenzelm@23463
|
92 |
(rule is_ideal, rule I_notcarr, rule I_maximal)
|
ballarin@27611
|
93 |
qed
|
ballarin@20318
|
94 |
|
ballarin@20318
|
95 |
subsection {* Prime Ideals *}
|
ballarin@20318
|
96 |
|
ballarin@20318
|
97 |
locale primeideal = ideal + cring +
|
ballarin@20318
|
98 |
assumes I_notcarr: "carrier R \<noteq> I"
|
ballarin@20318
|
99 |
and I_prime: "\<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I \<or> b \<in> I"
|
ballarin@20318
|
100 |
|
ballarin@20318
|
101 |
lemma (in primeideal) is_primeideal:
|
ballarin@20318
|
102 |
shows "primeideal I R"
|
wenzelm@26203
|
103 |
by (rule primeideal_axioms)
|
ballarin@20318
|
104 |
|
ballarin@20318
|
105 |
lemma primeidealI:
|
ballarin@27611
|
106 |
fixes R (structure)
|
ballarin@27611
|
107 |
assumes "ideal I R"
|
ballarin@27611
|
108 |
assumes "cring R"
|
ballarin@20318
|
109 |
assumes I_notcarr: "carrier R \<noteq> I"
|
ballarin@20318
|
110 |
and I_prime: "\<And>a b. \<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I \<or> b \<in> I"
|
ballarin@20318
|
111 |
shows "primeideal I R"
|
ballarin@27611
|
112 |
proof -
|
ballarin@27611
|
113 |
interpret ideal [I R] by fact
|
ballarin@27611
|
114 |
interpret cring [R] by fact
|
ballarin@27611
|
115 |
show ?thesis by (intro primeideal.intro primeideal_axioms.intro)
|
wenzelm@23463
|
116 |
(rule is_ideal, rule is_cring, rule I_notcarr, rule I_prime)
|
ballarin@27611
|
117 |
qed
|
ballarin@20318
|
118 |
|
ballarin@20318
|
119 |
lemma primeidealI2:
|
ballarin@27611
|
120 |
fixes R (structure)
|
ballarin@27611
|
121 |
assumes "additive_subgroup I R"
|
ballarin@27611
|
122 |
assumes "cring R"
|
ballarin@20318
|
123 |
assumes I_l_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
|
ballarin@20318
|
124 |
and I_r_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
|
ballarin@20318
|
125 |
and I_notcarr: "carrier R \<noteq> I"
|
ballarin@20318
|
126 |
and I_prime: "\<And>a b. \<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I \<or> b \<in> I"
|
ballarin@20318
|
127 |
shows "primeideal I R"
|
ballarin@27611
|
128 |
proof -
|
ballarin@27611
|
129 |
interpret additive_subgroup [I R] by fact
|
ballarin@27611
|
130 |
interpret cring [R] by fact
|
ballarin@27611
|
131 |
show ?thesis apply (intro_locales)
|
ballarin@27611
|
132 |
apply (intro ideal_axioms.intro)
|
ballarin@27611
|
133 |
apply (erule (1) I_l_closed)
|
ballarin@27611
|
134 |
apply (erule (1) I_r_closed)
|
ballarin@27611
|
135 |
apply (intro primeideal_axioms.intro)
|
ballarin@27611
|
136 |
apply (rule I_notcarr)
|
ballarin@27611
|
137 |
apply (erule (2) I_prime)
|
ballarin@27611
|
138 |
done
|
ballarin@27611
|
139 |
qed
|
ballarin@20318
|
140 |
|
ballarin@20318
|
141 |
section {* Properties of Ideals *}
|
ballarin@20318
|
142 |
|
ballarin@20318
|
143 |
subsection {* Special Ideals *}
|
ballarin@20318
|
144 |
|
ballarin@20318
|
145 |
lemma (in ring) zeroideal:
|
ballarin@20318
|
146 |
shows "ideal {\<zero>} R"
|
ballarin@20318
|
147 |
apply (intro idealI subgroup.intro)
|
ballarin@20318
|
148 |
apply (rule is_ring)
|
ballarin@20318
|
149 |
apply simp+
|
ballarin@20318
|
150 |
apply (fold a_inv_def, simp)
|
ballarin@20318
|
151 |
apply simp+
|
ballarin@20318
|
152 |
done
|
ballarin@20318
|
153 |
|
ballarin@20318
|
154 |
lemma (in ring) oneideal:
|
ballarin@20318
|
155 |
shows "ideal (carrier R) R"
|
ballarin@20318
|
156 |
apply (intro idealI subgroup.intro)
|
ballarin@20318
|
157 |
apply (rule is_ring)
|
ballarin@20318
|
158 |
apply simp+
|
ballarin@20318
|
159 |
apply (fold a_inv_def, simp)
|
ballarin@20318
|
160 |
apply simp+
|
ballarin@20318
|
161 |
done
|
ballarin@20318
|
162 |
|
ballarin@20318
|
163 |
lemma (in "domain") zeroprimeideal:
|
ballarin@20318
|
164 |
shows "primeideal {\<zero>} R"
|
ballarin@20318
|
165 |
apply (intro primeidealI)
|
ballarin@20318
|
166 |
apply (rule zeroideal)
|
wenzelm@23463
|
167 |
apply (rule domain.axioms, rule domain_axioms)
|
ballarin@20318
|
168 |
defer 1
|
ballarin@20318
|
169 |
apply (simp add: integral)
|
ballarin@20318
|
170 |
proof (rule ccontr, simp)
|
ballarin@20318
|
171 |
assume "carrier R = {\<zero>}"
|
ballarin@20318
|
172 |
from this have "\<one> = \<zero>" by (rule one_zeroI)
|
ballarin@20318
|
173 |
from this and one_not_zero
|
ballarin@20318
|
174 |
show "False" by simp
|
ballarin@20318
|
175 |
qed
|
ballarin@20318
|
176 |
|
ballarin@20318
|
177 |
|
ballarin@20318
|
178 |
subsection {* General Ideal Properies *}
|
ballarin@20318
|
179 |
|
ballarin@20318
|
180 |
lemma (in ideal) one_imp_carrier:
|
ballarin@20318
|
181 |
assumes I_one_closed: "\<one> \<in> I"
|
ballarin@20318
|
182 |
shows "I = carrier R"
|
ballarin@20318
|
183 |
apply (rule)
|
ballarin@20318
|
184 |
apply (rule)
|
ballarin@20318
|
185 |
apply (rule a_Hcarr, simp)
|
ballarin@20318
|
186 |
proof
|
ballarin@20318
|
187 |
fix x
|
ballarin@20318
|
188 |
assume xcarr: "x \<in> carrier R"
|
ballarin@20318
|
189 |
from I_one_closed and this
|
ballarin@20318
|
190 |
have "x \<otimes> \<one> \<in> I" by (intro I_l_closed)
|
ballarin@20318
|
191 |
from this and xcarr
|
ballarin@20318
|
192 |
show "x \<in> I" by simp
|
ballarin@20318
|
193 |
qed
|
ballarin@20318
|
194 |
|
ballarin@20318
|
195 |
lemma (in ideal) Icarr:
|
ballarin@20318
|
196 |
assumes iI: "i \<in> I"
|
ballarin@20318
|
197 |
shows "i \<in> carrier R"
|
wenzelm@23350
|
198 |
using iI by (rule a_Hcarr)
|
ballarin@20318
|
199 |
|
ballarin@20318
|
200 |
|
ballarin@20318
|
201 |
subsection {* Intersection of Ideals *}
|
ballarin@20318
|
202 |
|
ballarin@20318
|
203 |
text {* \paragraph{Intersection of two ideals} The intersection of any
|
ballarin@20318
|
204 |
two ideals is again an ideal in @{term R} *}
|
ballarin@20318
|
205 |
lemma (in ring) i_intersect:
|
ballarin@27611
|
206 |
assumes "ideal I R"
|
ballarin@27611
|
207 |
assumes "ideal J R"
|
ballarin@20318
|
208 |
shows "ideal (I \<inter> J) R"
|
ballarin@27611
|
209 |
proof -
|
ballarin@27611
|
210 |
interpret ideal [I R] by fact
|
ballarin@27611
|
211 |
interpret ideal [J R] by fact
|
ballarin@27611
|
212 |
show ?thesis
|
ballarin@20318
|
213 |
apply (intro idealI subgroup.intro)
|
ballarin@20318
|
214 |
apply (rule is_ring)
|
ballarin@20318
|
215 |
apply (force simp add: a_subset)
|
ballarin@20318
|
216 |
apply (simp add: a_inv_def[symmetric])
|
ballarin@20318
|
217 |
apply simp
|
ballarin@20318
|
218 |
apply (simp add: a_inv_def[symmetric])
|
ballarin@20318
|
219 |
apply (clarsimp, rule)
|
ballarin@20318
|
220 |
apply (fast intro: ideal.I_l_closed ideal.intro prems)+
|
ballarin@20318
|
221 |
apply (clarsimp, rule)
|
ballarin@20318
|
222 |
apply (fast intro: ideal.I_r_closed ideal.intro prems)+
|
ballarin@20318
|
223 |
done
|
ballarin@27611
|
224 |
qed
|
ballarin@20318
|
225 |
|
ballarin@20318
|
226 |
subsubsection {* Intersection of a Set of Ideals *}
|
ballarin@20318
|
227 |
|
ballarin@20318
|
228 |
text {* The intersection of any Number of Ideals is again
|
ballarin@20318
|
229 |
an Ideal in @{term R} *}
|
ballarin@20318
|
230 |
lemma (in ring) i_Intersect:
|
ballarin@20318
|
231 |
assumes Sideals: "\<And>I. I \<in> S \<Longrightarrow> ideal I R"
|
ballarin@20318
|
232 |
and notempty: "S \<noteq> {}"
|
ballarin@20318
|
233 |
shows "ideal (Inter S) R"
|
ballarin@20318
|
234 |
apply (unfold_locales)
|
ballarin@20318
|
235 |
apply (simp_all add: Inter_def INTER_def)
|
ballarin@20318
|
236 |
apply (rule, simp) defer 1
|
ballarin@20318
|
237 |
apply rule defer 1
|
ballarin@20318
|
238 |
apply rule defer 1
|
ballarin@20318
|
239 |
apply (fold a_inv_def, rule) defer 1
|
ballarin@20318
|
240 |
apply rule defer 1
|
ballarin@20318
|
241 |
apply rule defer 1
|
ballarin@20318
|
242 |
proof -
|
ballarin@20318
|
243 |
fix x
|
ballarin@20318
|
244 |
assume "\<forall>I\<in>S. x \<in> I"
|
ballarin@20318
|
245 |
hence xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp
|
ballarin@20318
|
246 |
|
ballarin@20318
|
247 |
from notempty have "\<exists>I0. I0 \<in> S" by blast
|
ballarin@20318
|
248 |
from this obtain I0 where I0S: "I0 \<in> S" by auto
|
ballarin@20318
|
249 |
|
ballarin@20318
|
250 |
interpret ideal ["I0" "R"] by (rule Sideals[OF I0S])
|
ballarin@20318
|
251 |
|
ballarin@20318
|
252 |
from xI[OF I0S] have "x \<in> I0" .
|
ballarin@20318
|
253 |
from this and a_subset show "x \<in> carrier R" by fast
|
ballarin@20318
|
254 |
next
|
ballarin@20318
|
255 |
fix x y
|
ballarin@20318
|
256 |
assume "\<forall>I\<in>S. x \<in> I"
|
ballarin@20318
|
257 |
hence xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp
|
ballarin@20318
|
258 |
assume "\<forall>I\<in>S. y \<in> I"
|
ballarin@20318
|
259 |
hence yI: "\<And>I. I \<in> S \<Longrightarrow> y \<in> I" by simp
|
ballarin@20318
|
260 |
|
ballarin@20318
|
261 |
fix J
|
ballarin@20318
|
262 |
assume JS: "J \<in> S"
|
ballarin@20318
|
263 |
interpret ideal ["J" "R"] by (rule Sideals[OF JS])
|
ballarin@20318
|
264 |
from xI[OF JS] and yI[OF JS]
|
ballarin@20318
|
265 |
show "x \<oplus> y \<in> J" by (rule a_closed)
|
ballarin@20318
|
266 |
next
|
ballarin@20318
|
267 |
fix J
|
ballarin@20318
|
268 |
assume JS: "J \<in> S"
|
ballarin@20318
|
269 |
interpret ideal ["J" "R"] by (rule Sideals[OF JS])
|
ballarin@20318
|
270 |
show "\<zero> \<in> J" by simp
|
ballarin@20318
|
271 |
next
|
ballarin@20318
|
272 |
fix x
|
ballarin@20318
|
273 |
assume "\<forall>I\<in>S. x \<in> I"
|
ballarin@20318
|
274 |
hence xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp
|
ballarin@20318
|
275 |
|
ballarin@20318
|
276 |
fix J
|
ballarin@20318
|
277 |
assume JS: "J \<in> S"
|
ballarin@20318
|
278 |
interpret ideal ["J" "R"] by (rule Sideals[OF JS])
|
ballarin@20318
|
279 |
|
ballarin@20318
|
280 |
from xI[OF JS]
|
ballarin@20318
|
281 |
show "\<ominus> x \<in> J" by (rule a_inv_closed)
|
ballarin@20318
|
282 |
next
|
ballarin@20318
|
283 |
fix x y
|
ballarin@20318
|
284 |
assume "\<forall>I\<in>S. x \<in> I"
|
ballarin@20318
|
285 |
hence xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp
|
ballarin@20318
|
286 |
assume ycarr: "y \<in> carrier R"
|
ballarin@20318
|
287 |
|
ballarin@20318
|
288 |
fix J
|
ballarin@20318
|
289 |
assume JS: "J \<in> S"
|
ballarin@20318
|
290 |
interpret ideal ["J" "R"] by (rule Sideals[OF JS])
|
ballarin@20318
|
291 |
|
ballarin@20318
|
292 |
from xI[OF JS] and ycarr
|
ballarin@20318
|
293 |
show "y \<otimes> x \<in> J" by (rule I_l_closed)
|
ballarin@20318
|
294 |
next
|
ballarin@20318
|
295 |
fix x y
|
ballarin@20318
|
296 |
assume "\<forall>I\<in>S. x \<in> I"
|
ballarin@20318
|
297 |
hence xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp
|
ballarin@20318
|
298 |
assume ycarr: "y \<in> carrier R"
|
ballarin@20318
|
299 |
|
ballarin@20318
|
300 |
fix J
|
ballarin@20318
|
301 |
assume JS: "J \<in> S"
|
ballarin@20318
|
302 |
interpret ideal ["J" "R"] by (rule Sideals[OF JS])
|
ballarin@20318
|
303 |
|
ballarin@20318
|
304 |
from xI[OF JS] and ycarr
|
ballarin@20318
|
305 |
show "x \<otimes> y \<in> J" by (rule I_r_closed)
|
ballarin@20318
|
306 |
qed
|
ballarin@20318
|
307 |
|
ballarin@20318
|
308 |
|
ballarin@20318
|
309 |
subsection {* Addition of Ideals *}
|
ballarin@20318
|
310 |
|
ballarin@20318
|
311 |
lemma (in ring) add_ideals:
|
ballarin@20318
|
312 |
assumes idealI: "ideal I R"
|
ballarin@20318
|
313 |
and idealJ: "ideal J R"
|
ballarin@20318
|
314 |
shows "ideal (I <+> J) R"
|
ballarin@20318
|
315 |
apply (rule ideal.intro)
|
ballarin@20318
|
316 |
apply (rule add_additive_subgroups)
|
ballarin@20318
|
317 |
apply (intro ideal.axioms[OF idealI])
|
ballarin@20318
|
318 |
apply (intro ideal.axioms[OF idealJ])
|
wenzelm@23463
|
319 |
apply (rule is_ring)
|
ballarin@20318
|
320 |
apply (rule ideal_axioms.intro)
|
ballarin@20318
|
321 |
apply (simp add: set_add_defs, clarsimp) defer 1
|
ballarin@20318
|
322 |
apply (simp add: set_add_defs, clarsimp) defer 1
|
ballarin@20318
|
323 |
proof -
|
ballarin@20318
|
324 |
fix x i j
|
ballarin@20318
|
325 |
assume xcarr: "x \<in> carrier R"
|
ballarin@20318
|
326 |
and iI: "i \<in> I"
|
ballarin@20318
|
327 |
and jJ: "j \<in> J"
|
ballarin@20318
|
328 |
from xcarr ideal.Icarr[OF idealI iI] ideal.Icarr[OF idealJ jJ]
|
ballarin@20318
|
329 |
have c: "(i \<oplus> j) \<otimes> x = (i \<otimes> x) \<oplus> (j \<otimes> x)" by algebra
|
ballarin@20318
|
330 |
from xcarr and iI
|
ballarin@20318
|
331 |
have a: "i \<otimes> x \<in> I" by (simp add: ideal.I_r_closed[OF idealI])
|
ballarin@20318
|
332 |
from xcarr and jJ
|
ballarin@20318
|
333 |
have b: "j \<otimes> x \<in> J" by (simp add: ideal.I_r_closed[OF idealJ])
|
ballarin@20318
|
334 |
from a b c
|
ballarin@20318
|
335 |
show "\<exists>ha\<in>I. \<exists>ka\<in>J. (i \<oplus> j) \<otimes> x = ha \<oplus> ka" by fast
|
ballarin@20318
|
336 |
next
|
ballarin@20318
|
337 |
fix x i j
|
ballarin@20318
|
338 |
assume xcarr: "x \<in> carrier R"
|
ballarin@20318
|
339 |
and iI: "i \<in> I"
|
ballarin@20318
|
340 |
and jJ: "j \<in> J"
|
ballarin@20318
|
341 |
from xcarr ideal.Icarr[OF idealI iI] ideal.Icarr[OF idealJ jJ]
|
ballarin@20318
|
342 |
have c: "x \<otimes> (i \<oplus> j) = (x \<otimes> i) \<oplus> (x \<otimes> j)" by algebra
|
ballarin@20318
|
343 |
from xcarr and iI
|
ballarin@20318
|
344 |
have a: "x \<otimes> i \<in> I" by (simp add: ideal.I_l_closed[OF idealI])
|
ballarin@20318
|
345 |
from xcarr and jJ
|
ballarin@20318
|
346 |
have b: "x \<otimes> j \<in> J" by (simp add: ideal.I_l_closed[OF idealJ])
|
ballarin@20318
|
347 |
from a b c
|
ballarin@20318
|
348 |
show "\<exists>ha\<in>I. \<exists>ka\<in>J. x \<otimes> (i \<oplus> j) = ha \<oplus> ka" by fast
|
ballarin@20318
|
349 |
qed
|
ballarin@20318
|
350 |
|
ballarin@20318
|
351 |
|
ballarin@20318
|
352 |
subsection {* Ideals generated by a subset of @{term [locale=ring]
|
ballarin@20318
|
353 |
"carrier R"} *}
|
ballarin@20318
|
354 |
|
ballarin@20318
|
355 |
subsubsection {* Generation of Ideals in General Rings *}
|
ballarin@20318
|
356 |
|
ballarin@20318
|
357 |
text {* @{term genideal} generates an ideal *}
|
ballarin@20318
|
358 |
lemma (in ring) genideal_ideal:
|
ballarin@20318
|
359 |
assumes Scarr: "S \<subseteq> carrier R"
|
ballarin@20318
|
360 |
shows "ideal (Idl S) R"
|
ballarin@20318
|
361 |
unfolding genideal_def
|
ballarin@20318
|
362 |
proof (rule i_Intersect, fast, simp)
|
ballarin@20318
|
363 |
from oneideal and Scarr
|
ballarin@20318
|
364 |
show "\<exists>I. ideal I R \<and> S \<le> I" by fast
|
ballarin@20318
|
365 |
qed
|
ballarin@20318
|
366 |
|
ballarin@20318
|
367 |
lemma (in ring) genideal_self:
|
ballarin@20318
|
368 |
assumes "S \<subseteq> carrier R"
|
ballarin@20318
|
369 |
shows "S \<subseteq> Idl S"
|
ballarin@20318
|
370 |
unfolding genideal_def
|
ballarin@20318
|
371 |
by fast
|
ballarin@20318
|
372 |
|
ballarin@20318
|
373 |
lemma (in ring) genideal_self':
|
ballarin@20318
|
374 |
assumes carr: "i \<in> carrier R"
|
ballarin@20318
|
375 |
shows "i \<in> Idl {i}"
|
ballarin@20318
|
376 |
proof -
|
ballarin@20318
|
377 |
from carr
|
ballarin@20318
|
378 |
have "{i} \<subseteq> Idl {i}" by (fast intro!: genideal_self)
|
ballarin@20318
|
379 |
thus "i \<in> Idl {i}" by fast
|
ballarin@20318
|
380 |
qed
|
ballarin@20318
|
381 |
|
ballarin@20318
|
382 |
text {* @{term genideal} generates the minimal ideal *}
|
ballarin@20318
|
383 |
lemma (in ring) genideal_minimal:
|
ballarin@20318
|
384 |
assumes a: "ideal I R"
|
ballarin@20318
|
385 |
and b: "S \<subseteq> I"
|
ballarin@20318
|
386 |
shows "Idl S \<subseteq> I"
|
ballarin@20318
|
387 |
unfolding genideal_def
|
ballarin@20318
|
388 |
by (rule, elim InterD, simp add: a b)
|
ballarin@20318
|
389 |
|
ballarin@20318
|
390 |
text {* Generated ideals and subsets *}
|
ballarin@20318
|
391 |
lemma (in ring) Idl_subset_ideal:
|
ballarin@20318
|
392 |
assumes Iideal: "ideal I R"
|
ballarin@20318
|
393 |
and Hcarr: "H \<subseteq> carrier R"
|
ballarin@20318
|
394 |
shows "(Idl H \<subseteq> I) = (H \<subseteq> I)"
|
ballarin@20318
|
395 |
proof
|
ballarin@20318
|
396 |
assume a: "Idl H \<subseteq> I"
|
wenzelm@23350
|
397 |
from Hcarr have "H \<subseteq> Idl H" by (rule genideal_self)
|
ballarin@20318
|
398 |
from this and a
|
ballarin@20318
|
399 |
show "H \<subseteq> I" by simp
|
ballarin@20318
|
400 |
next
|
ballarin@20318
|
401 |
fix x
|
ballarin@20318
|
402 |
assume HI: "H \<subseteq> I"
|
ballarin@20318
|
403 |
|
ballarin@20318
|
404 |
from Iideal and HI
|
ballarin@20318
|
405 |
have "I \<in> {I. ideal I R \<and> H \<subseteq> I}" by fast
|
ballarin@20318
|
406 |
from this
|
ballarin@20318
|
407 |
show "Idl H \<subseteq> I"
|
ballarin@20318
|
408 |
unfolding genideal_def
|
ballarin@20318
|
409 |
by fast
|
ballarin@20318
|
410 |
qed
|
ballarin@20318
|
411 |
|
ballarin@20318
|
412 |
lemma (in ring) subset_Idl_subset:
|
ballarin@20318
|
413 |
assumes Icarr: "I \<subseteq> carrier R"
|
ballarin@20318
|
414 |
and HI: "H \<subseteq> I"
|
ballarin@20318
|
415 |
shows "Idl H \<subseteq> Idl I"
|
ballarin@20318
|
416 |
proof -
|
ballarin@20318
|
417 |
from HI and genideal_self[OF Icarr]
|
ballarin@20318
|
418 |
have HIdlI: "H \<subseteq> Idl I" by fast
|
ballarin@20318
|
419 |
|
ballarin@20318
|
420 |
from Icarr
|
ballarin@20318
|
421 |
have Iideal: "ideal (Idl I) R" by (rule genideal_ideal)
|
ballarin@20318
|
422 |
from HI and Icarr
|
ballarin@20318
|
423 |
have "H \<subseteq> carrier R" by fast
|
ballarin@20318
|
424 |
from Iideal and this
|
ballarin@20318
|
425 |
have "(H \<subseteq> Idl I) = (Idl H \<subseteq> Idl I)"
|
ballarin@20318
|
426 |
by (rule Idl_subset_ideal[symmetric])
|
ballarin@20318
|
427 |
|
ballarin@20318
|
428 |
from HIdlI and this
|
ballarin@20318
|
429 |
show "Idl H \<subseteq> Idl I" by simp
|
ballarin@20318
|
430 |
qed
|
ballarin@20318
|
431 |
|
ballarin@20318
|
432 |
lemma (in ring) Idl_subset_ideal':
|
ballarin@20318
|
433 |
assumes acarr: "a \<in> carrier R" and bcarr: "b \<in> carrier R"
|
ballarin@20318
|
434 |
shows "(Idl {a} \<subseteq> Idl {b}) = (a \<in> Idl {b})"
|
ballarin@20318
|
435 |
apply (subst Idl_subset_ideal[OF genideal_ideal[of "{b}"], of "{a}"])
|
ballarin@20318
|
436 |
apply (fast intro: bcarr, fast intro: acarr)
|
ballarin@20318
|
437 |
apply fast
|
ballarin@20318
|
438 |
done
|
ballarin@20318
|
439 |
|
ballarin@20318
|
440 |
lemma (in ring) genideal_zero:
|
ballarin@20318
|
441 |
"Idl {\<zero>} = {\<zero>}"
|
ballarin@20318
|
442 |
apply rule
|
ballarin@20318
|
443 |
apply (rule genideal_minimal[OF zeroideal], simp)
|
ballarin@20318
|
444 |
apply (simp add: genideal_self')
|
ballarin@20318
|
445 |
done
|
ballarin@20318
|
446 |
|
ballarin@20318
|
447 |
lemma (in ring) genideal_one:
|
ballarin@20318
|
448 |
"Idl {\<one>} = carrier R"
|
ballarin@20318
|
449 |
proof -
|
ballarin@20318
|
450 |
interpret ideal ["Idl {\<one>}" "R"] by (rule genideal_ideal, fast intro: one_closed)
|
ballarin@20318
|
451 |
show "Idl {\<one>} = carrier R"
|
ballarin@20318
|
452 |
apply (rule, rule a_subset)
|
ballarin@20318
|
453 |
apply (simp add: one_imp_carrier genideal_self')
|
ballarin@20318
|
454 |
done
|
ballarin@20318
|
455 |
qed
|
ballarin@20318
|
456 |
|
ballarin@20318
|
457 |
|
ballarin@20318
|
458 |
subsubsection {* Generation of Principal Ideals in Commutative Rings *}
|
ballarin@20318
|
459 |
|
ballarin@20318
|
460 |
constdefs (structure R)
|
ballarin@20318
|
461 |
cgenideal :: "('a, 'b) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a set" ("PIdl\<index> _" [80] 79)
|
ballarin@20318
|
462 |
"cgenideal R a \<equiv> { x \<otimes> a | x. x \<in> carrier R }"
|
ballarin@20318
|
463 |
|
ballarin@20318
|
464 |
text {* genhideal (?) really generates an ideal *}
|
ballarin@20318
|
465 |
lemma (in cring) cgenideal_ideal:
|
ballarin@20318
|
466 |
assumes acarr: "a \<in> carrier R"
|
ballarin@20318
|
467 |
shows "ideal (PIdl a) R"
|
ballarin@20318
|
468 |
apply (unfold cgenideal_def)
|
ballarin@20318
|
469 |
apply (rule idealI[OF is_ring])
|
ballarin@20318
|
470 |
apply (rule subgroup.intro)
|
ballarin@20318
|
471 |
apply (simp_all add: monoid_record_simps)
|
ballarin@20318
|
472 |
apply (blast intro: acarr m_closed)
|
ballarin@20318
|
473 |
apply clarsimp defer 1
|
ballarin@20318
|
474 |
defer 1
|
ballarin@20318
|
475 |
apply (fold a_inv_def, clarsimp) defer 1
|
ballarin@20318
|
476 |
apply clarsimp defer 1
|
ballarin@20318
|
477 |
apply clarsimp defer 1
|
ballarin@20318
|
478 |
proof -
|
ballarin@20318
|
479 |
fix x y
|
ballarin@20318
|
480 |
assume xcarr: "x \<in> carrier R"
|
ballarin@20318
|
481 |
and ycarr: "y \<in> carrier R"
|
ballarin@20318
|
482 |
note carr = acarr xcarr ycarr
|
ballarin@20318
|
483 |
|
ballarin@20318
|
484 |
from carr
|
ballarin@20318
|
485 |
have "x \<otimes> a \<oplus> y \<otimes> a = (x \<oplus> y) \<otimes> a" by (simp add: l_distr)
|
ballarin@20318
|
486 |
from this and carr
|
ballarin@20318
|
487 |
show "\<exists>z. x \<otimes> a \<oplus> y \<otimes> a = z \<otimes> a \<and> z \<in> carrier R" by fast
|
ballarin@20318
|
488 |
next
|
ballarin@20318
|
489 |
from l_null[OF acarr, symmetric] and zero_closed
|
ballarin@20318
|
490 |
show "\<exists>x. \<zero> = x \<otimes> a \<and> x \<in> carrier R" by fast
|
ballarin@20318
|
491 |
next
|
ballarin@20318
|
492 |
fix x
|
ballarin@20318
|
493 |
assume xcarr: "x \<in> carrier R"
|
ballarin@20318
|
494 |
note carr = acarr xcarr
|
ballarin@20318
|
495 |
|
ballarin@20318
|
496 |
from carr
|
ballarin@20318
|
497 |
have "\<ominus> (x \<otimes> a) = (\<ominus> x) \<otimes> a" by (simp add: l_minus)
|
ballarin@20318
|
498 |
from this and carr
|
ballarin@20318
|
499 |
show "\<exists>z. \<ominus> (x \<otimes> a) = z \<otimes> a \<and> z \<in> carrier R" by fast
|
ballarin@20318
|
500 |
next
|
ballarin@20318
|
501 |
fix x y
|
ballarin@20318
|
502 |
assume xcarr: "x \<in> carrier R"
|
ballarin@20318
|
503 |
and ycarr: "y \<in> carrier R"
|
ballarin@20318
|
504 |
note carr = acarr xcarr ycarr
|
ballarin@20318
|
505 |
|
ballarin@20318
|
506 |
from carr
|
ballarin@20318
|
507 |
have "y \<otimes> a \<otimes> x = (y \<otimes> x) \<otimes> a" by (simp add: m_assoc, simp add: m_comm)
|
ballarin@20318
|
508 |
from this and carr
|
ballarin@20318
|
509 |
show "\<exists>z. y \<otimes> a \<otimes> x = z \<otimes> a \<and> z \<in> carrier R" by fast
|
ballarin@20318
|
510 |
next
|
ballarin@20318
|
511 |
fix x y
|
ballarin@20318
|
512 |
assume xcarr: "x \<in> carrier R"
|
ballarin@20318
|
513 |
and ycarr: "y \<in> carrier R"
|
ballarin@20318
|
514 |
note carr = acarr xcarr ycarr
|
ballarin@20318
|
515 |
|
ballarin@20318
|
516 |
from carr
|
ballarin@20318
|
517 |
have "x \<otimes> (y \<otimes> a) = (x \<otimes> y) \<otimes> a" by (simp add: m_assoc)
|
ballarin@20318
|
518 |
from this and carr
|
ballarin@20318
|
519 |
show "\<exists>z. x \<otimes> (y \<otimes> a) = z \<otimes> a \<and> z \<in> carrier R" by fast
|
ballarin@20318
|
520 |
qed
|
ballarin@20318
|
521 |
|
ballarin@20318
|
522 |
lemma (in ring) cgenideal_self:
|
ballarin@20318
|
523 |
assumes icarr: "i \<in> carrier R"
|
ballarin@20318
|
524 |
shows "i \<in> PIdl i"
|
ballarin@20318
|
525 |
unfolding cgenideal_def
|
ballarin@20318
|
526 |
proof simp
|
ballarin@20318
|
527 |
from icarr
|
ballarin@20318
|
528 |
have "i = \<one> \<otimes> i" by simp
|
ballarin@20318
|
529 |
from this and icarr
|
ballarin@20318
|
530 |
show "\<exists>x. i = x \<otimes> i \<and> x \<in> carrier R" by fast
|
ballarin@20318
|
531 |
qed
|
ballarin@20318
|
532 |
|
ballarin@20318
|
533 |
text {* @{const "cgenideal"} is minimal *}
|
ballarin@20318
|
534 |
|
ballarin@20318
|
535 |
lemma (in ring) cgenideal_minimal:
|
ballarin@27611
|
536 |
assumes "ideal J R"
|
ballarin@20318
|
537 |
assumes aJ: "a \<in> J"
|
ballarin@20318
|
538 |
shows "PIdl a \<subseteq> J"
|
ballarin@27611
|
539 |
proof -
|
ballarin@27611
|
540 |
interpret ideal [J R] by fact
|
ballarin@27611
|
541 |
show ?thesis unfolding cgenideal_def
|
ballarin@27611
|
542 |
apply rule
|
ballarin@27611
|
543 |
apply clarify
|
ballarin@27611
|
544 |
using aJ
|
ballarin@27611
|
545 |
apply (erule I_l_closed)
|
ballarin@27611
|
546 |
done
|
ballarin@27611
|
547 |
qed
|
ballarin@20318
|
548 |
|
ballarin@20318
|
549 |
lemma (in cring) cgenideal_eq_genideal:
|
ballarin@20318
|
550 |
assumes icarr: "i \<in> carrier R"
|
ballarin@20318
|
551 |
shows "PIdl i = Idl {i}"
|
ballarin@20318
|
552 |
apply rule
|
ballarin@20318
|
553 |
apply (intro cgenideal_minimal)
|
ballarin@20318
|
554 |
apply (rule genideal_ideal, fast intro: icarr)
|
ballarin@20318
|
555 |
apply (rule genideal_self', fast intro: icarr)
|
ballarin@20318
|
556 |
apply (intro genideal_minimal)
|
wenzelm@23463
|
557 |
apply (rule cgenideal_ideal [OF icarr])
|
wenzelm@23463
|
558 |
apply (simp, rule cgenideal_self [OF icarr])
|
ballarin@20318
|
559 |
done
|
ballarin@20318
|
560 |
|
ballarin@20318
|
561 |
lemma (in cring) cgenideal_eq_rcos:
|
ballarin@20318
|
562 |
"PIdl i = carrier R #> i"
|
ballarin@20318
|
563 |
unfolding cgenideal_def r_coset_def
|
ballarin@20318
|
564 |
by fast
|
ballarin@20318
|
565 |
|
ballarin@20318
|
566 |
lemma (in cring) cgenideal_is_principalideal:
|
ballarin@20318
|
567 |
assumes icarr: "i \<in> carrier R"
|
ballarin@20318
|
568 |
shows "principalideal (PIdl i) R"
|
ballarin@20318
|
569 |
apply (rule principalidealI)
|
wenzelm@23464
|
570 |
apply (rule cgenideal_ideal [OF icarr])
|
ballarin@20318
|
571 |
proof -
|
ballarin@20318
|
572 |
from icarr
|
ballarin@20318
|
573 |
have "PIdl i = Idl {i}" by (rule cgenideal_eq_genideal)
|
ballarin@20318
|
574 |
from icarr and this
|
ballarin@20318
|
575 |
show "\<exists>i'\<in>carrier R. PIdl i = Idl {i'}" by fast
|
ballarin@20318
|
576 |
qed
|
ballarin@20318
|
577 |
|
ballarin@20318
|
578 |
|
ballarin@20318
|
579 |
subsection {* Union of Ideals *}
|
ballarin@20318
|
580 |
|
ballarin@20318
|
581 |
lemma (in ring) union_genideal:
|
ballarin@20318
|
582 |
assumes idealI: "ideal I R"
|
ballarin@20318
|
583 |
and idealJ: "ideal J R"
|
ballarin@20318
|
584 |
shows "Idl (I \<union> J) = I <+> J"
|
ballarin@20318
|
585 |
apply rule
|
ballarin@20318
|
586 |
apply (rule ring.genideal_minimal)
|
wenzelm@23464
|
587 |
apply (rule R.is_ring)
|
ballarin@20318
|
588 |
apply (rule add_ideals[OF idealI idealJ])
|
ballarin@20318
|
589 |
apply (rule)
|
ballarin@20318
|
590 |
apply (simp add: set_add_defs) apply (elim disjE) defer 1 defer 1
|
ballarin@20318
|
591 |
apply (rule) apply (simp add: set_add_defs genideal_def) apply clarsimp defer 1
|
ballarin@20318
|
592 |
proof -
|
ballarin@20318
|
593 |
fix x
|
ballarin@20318
|
594 |
assume xI: "x \<in> I"
|
ballarin@20318
|
595 |
have ZJ: "\<zero> \<in> J"
|
ballarin@20318
|
596 |
by (intro additive_subgroup.zero_closed, rule ideal.axioms[OF idealJ])
|
ballarin@20318
|
597 |
from ideal.Icarr[OF idealI xI]
|
ballarin@20318
|
598 |
have "x = x \<oplus> \<zero>" by algebra
|
ballarin@20318
|
599 |
from xI and ZJ and this
|
ballarin@20318
|
600 |
show "\<exists>h\<in>I. \<exists>k\<in>J. x = h \<oplus> k" by fast
|
ballarin@20318
|
601 |
next
|
ballarin@20318
|
602 |
fix x
|
ballarin@20318
|
603 |
assume xJ: "x \<in> J"
|
ballarin@20318
|
604 |
have ZI: "\<zero> \<in> I"
|
ballarin@20318
|
605 |
by (intro additive_subgroup.zero_closed, rule ideal.axioms[OF idealI])
|
ballarin@20318
|
606 |
from ideal.Icarr[OF idealJ xJ]
|
ballarin@20318
|
607 |
have "x = \<zero> \<oplus> x" by algebra
|
ballarin@20318
|
608 |
from ZI and xJ and this
|
ballarin@20318
|
609 |
show "\<exists>h\<in>I. \<exists>k\<in>J. x = h \<oplus> k" by fast
|
ballarin@20318
|
610 |
next
|
ballarin@20318
|
611 |
fix i j K
|
ballarin@20318
|
612 |
assume iI: "i \<in> I"
|
ballarin@20318
|
613 |
and jJ: "j \<in> J"
|
ballarin@20318
|
614 |
and idealK: "ideal K R"
|
ballarin@20318
|
615 |
and IK: "I \<subseteq> K"
|
ballarin@20318
|
616 |
and JK: "J \<subseteq> K"
|
ballarin@20318
|
617 |
from iI and IK
|
ballarin@20318
|
618 |
have iK: "i \<in> K" by fast
|
ballarin@20318
|
619 |
from jJ and JK
|
ballarin@20318
|
620 |
have jK: "j \<in> K" by fast
|
ballarin@20318
|
621 |
from iK and jK
|
ballarin@20318
|
622 |
show "i \<oplus> j \<in> K" by (intro additive_subgroup.a_closed) (rule ideal.axioms[OF idealK])
|
ballarin@20318
|
623 |
qed
|
ballarin@20318
|
624 |
|
ballarin@20318
|
625 |
|
ballarin@20318
|
626 |
subsection {* Properties of Principal Ideals *}
|
ballarin@20318
|
627 |
|
ballarin@20318
|
628 |
text {* @{text "\<zero>"} generates the zero ideal *}
|
ballarin@20318
|
629 |
lemma (in ring) zero_genideal:
|
ballarin@20318
|
630 |
shows "Idl {\<zero>} = {\<zero>}"
|
ballarin@20318
|
631 |
apply rule
|
ballarin@20318
|
632 |
apply (simp add: genideal_minimal zeroideal)
|
ballarin@20318
|
633 |
apply (fast intro!: genideal_self)
|
ballarin@20318
|
634 |
done
|
ballarin@20318
|
635 |
|
ballarin@20318
|
636 |
text {* @{text "\<one>"} generates the unit ideal *}
|
ballarin@20318
|
637 |
lemma (in ring) one_genideal:
|
ballarin@20318
|
638 |
shows "Idl {\<one>} = carrier R"
|
ballarin@20318
|
639 |
proof -
|
ballarin@20318
|
640 |
have "\<one> \<in> Idl {\<one>}" by (simp add: genideal_self')
|
ballarin@20318
|
641 |
thus "Idl {\<one>} = carrier R" by (intro ideal.one_imp_carrier, fast intro: genideal_ideal)
|
ballarin@20318
|
642 |
qed
|
ballarin@20318
|
643 |
|
ballarin@20318
|
644 |
|
ballarin@20318
|
645 |
text {* The zero ideal is a principal ideal *}
|
ballarin@20318
|
646 |
corollary (in ring) zeropideal:
|
ballarin@20318
|
647 |
shows "principalideal {\<zero>} R"
|
ballarin@20318
|
648 |
apply (rule principalidealI)
|
ballarin@20318
|
649 |
apply (rule zeroideal)
|
ballarin@20318
|
650 |
apply (blast intro!: zero_closed zero_genideal[symmetric])
|
ballarin@20318
|
651 |
done
|
ballarin@20318
|
652 |
|
ballarin@20318
|
653 |
text {* The unit ideal is a principal ideal *}
|
ballarin@20318
|
654 |
corollary (in ring) onepideal:
|
ballarin@20318
|
655 |
shows "principalideal (carrier R) R"
|
ballarin@20318
|
656 |
apply (rule principalidealI)
|
ballarin@20318
|
657 |
apply (rule oneideal)
|
ballarin@20318
|
658 |
apply (blast intro!: one_closed one_genideal[symmetric])
|
ballarin@20318
|
659 |
done
|
ballarin@20318
|
660 |
|
ballarin@20318
|
661 |
|
ballarin@20318
|
662 |
text {* Every principal ideal is a right coset of the carrier *}
|
ballarin@20318
|
663 |
lemma (in principalideal) rcos_generate:
|
ballarin@27611
|
664 |
assumes "cring R"
|
ballarin@20318
|
665 |
shows "\<exists>x\<in>I. I = carrier R #> x"
|
ballarin@20318
|
666 |
proof -
|
ballarin@27611
|
667 |
interpret cring [R] by fact
|
ballarin@20318
|
668 |
from generate
|
ballarin@20318
|
669 |
obtain i
|
ballarin@20318
|
670 |
where icarr: "i \<in> carrier R"
|
ballarin@20318
|
671 |
and I1: "I = Idl {i}"
|
ballarin@20318
|
672 |
by fast+
|
ballarin@20318
|
673 |
|
ballarin@20318
|
674 |
from icarr and genideal_self[of "{i}"]
|
ballarin@20318
|
675 |
have "i \<in> Idl {i}" by fast
|
ballarin@20318
|
676 |
hence iI: "i \<in> I" by (simp add: I1)
|
ballarin@20318
|
677 |
|
ballarin@20318
|
678 |
from I1 icarr
|
ballarin@20318
|
679 |
have I2: "I = PIdl i" by (simp add: cgenideal_eq_genideal)
|
ballarin@20318
|
680 |
|
ballarin@20318
|
681 |
have "PIdl i = carrier R #> i"
|
ballarin@20318
|
682 |
unfolding cgenideal_def r_coset_def
|
ballarin@20318
|
683 |
by fast
|
ballarin@20318
|
684 |
|
ballarin@20318
|
685 |
from I2 and this
|
ballarin@20318
|
686 |
have "I = carrier R #> i" by simp
|
ballarin@20318
|
687 |
|
ballarin@20318
|
688 |
from iI and this
|
ballarin@20318
|
689 |
show "\<exists>x\<in>I. I = carrier R #> x" by fast
|
ballarin@20318
|
690 |
qed
|
ballarin@20318
|
691 |
|
ballarin@20318
|
692 |
|
ballarin@20318
|
693 |
subsection {* Prime Ideals *}
|
ballarin@20318
|
694 |
|
ballarin@20318
|
695 |
lemma (in ideal) primeidealCD:
|
ballarin@27611
|
696 |
assumes "cring R"
|
ballarin@20318
|
697 |
assumes notprime: "\<not> primeideal I R"
|
ballarin@20318
|
698 |
shows "carrier R = I \<or> (\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I)"
|
ballarin@20318
|
699 |
proof (rule ccontr, clarsimp)
|
ballarin@27611
|
700 |
interpret cring [R] by fact
|
ballarin@20318
|
701 |
assume InR: "carrier R \<noteq> I"
|
ballarin@20318
|
702 |
and "\<forall>a. a \<in> carrier R \<longrightarrow> (\<forall>b. a \<otimes> b \<in> I \<longrightarrow> b \<in> carrier R \<longrightarrow> a \<in> I \<or> b \<in> I)"
|
ballarin@20318
|
703 |
hence I_prime: "\<And> a b. \<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I \<or> b \<in> I" by simp
|
ballarin@20318
|
704 |
have "primeideal I R"
|
wenzelm@23464
|
705 |
apply (rule primeideal.intro [OF is_ideal is_cring])
|
wenzelm@23464
|
706 |
apply (rule primeideal_axioms.intro)
|
wenzelm@23464
|
707 |
apply (rule InR)
|
wenzelm@23464
|
708 |
apply (erule (2) I_prime)
|
wenzelm@23464
|
709 |
done
|
ballarin@20318
|
710 |
from this and notprime
|
ballarin@20318
|
711 |
show "False" by simp
|
ballarin@20318
|
712 |
qed
|
ballarin@20318
|
713 |
|
ballarin@20318
|
714 |
lemma (in ideal) primeidealCE:
|
ballarin@27611
|
715 |
assumes "cring R"
|
ballarin@20318
|
716 |
assumes notprime: "\<not> primeideal I R"
|
wenzelm@23383
|
717 |
obtains "carrier R = I"
|
wenzelm@23383
|
718 |
| "\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I"
|
ballarin@27611
|
719 |
proof -
|
ballarin@27611
|
720 |
interpret R: cring [R] by fact
|
ballarin@27611
|
721 |
assume "carrier R = I ==> thesis"
|
ballarin@27611
|
722 |
and "\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I \<Longrightarrow> thesis"
|
ballarin@27611
|
723 |
then show thesis using primeidealCD [OF R.is_cring notprime] by blast
|
ballarin@27611
|
724 |
qed
|
ballarin@20318
|
725 |
|
ballarin@20318
|
726 |
text {* If @{text "{\<zero>}"} is a prime ideal of a commutative ring, the ring is a domain *}
|
ballarin@20318
|
727 |
lemma (in cring) zeroprimeideal_domainI:
|
ballarin@20318
|
728 |
assumes pi: "primeideal {\<zero>} R"
|
ballarin@20318
|
729 |
shows "domain R"
|
wenzelm@23464
|
730 |
apply (rule domain.intro, rule is_cring)
|
ballarin@20318
|
731 |
apply (rule domain_axioms.intro)
|
ballarin@20318
|
732 |
proof (rule ccontr, simp)
|
ballarin@20318
|
733 |
interpret primeideal ["{\<zero>}" "R"] by (rule pi)
|
ballarin@20318
|
734 |
assume "\<one> = \<zero>"
|
ballarin@20318
|
735 |
hence "carrier R = {\<zero>}" by (rule one_zeroD)
|
ballarin@20318
|
736 |
from this[symmetric] and I_notcarr
|
ballarin@20318
|
737 |
show "False" by simp
|
ballarin@20318
|
738 |
next
|
ballarin@20318
|
739 |
interpret primeideal ["{\<zero>}" "R"] by (rule pi)
|
ballarin@20318
|
740 |
fix a b
|
ballarin@20318
|
741 |
assume ab: "a \<otimes> b = \<zero>"
|
ballarin@20318
|
742 |
and carr: "a \<in> carrier R" "b \<in> carrier R"
|
ballarin@20318
|
743 |
from ab
|
ballarin@20318
|
744 |
have abI: "a \<otimes> b \<in> {\<zero>}" by fast
|
ballarin@20318
|
745 |
from carr and this
|
ballarin@20318
|
746 |
have "a \<in> {\<zero>} \<or> b \<in> {\<zero>}" by (rule I_prime)
|
ballarin@20318
|
747 |
thus "a = \<zero> \<or> b = \<zero>" by simp
|
ballarin@20318
|
748 |
qed
|
ballarin@20318
|
749 |
|
ballarin@20318
|
750 |
corollary (in cring) domain_eq_zeroprimeideal:
|
ballarin@20318
|
751 |
shows "domain R = primeideal {\<zero>} R"
|
ballarin@20318
|
752 |
apply rule
|
ballarin@20318
|
753 |
apply (erule domain.zeroprimeideal)
|
ballarin@20318
|
754 |
apply (erule zeroprimeideal_domainI)
|
ballarin@20318
|
755 |
done
|
ballarin@20318
|
756 |
|
ballarin@20318
|
757 |
|
ballarin@20318
|
758 |
subsection {* Maximal Ideals *}
|
ballarin@20318
|
759 |
|
ballarin@20318
|
760 |
lemma (in ideal) helper_I_closed:
|
ballarin@20318
|
761 |
assumes carr: "a \<in> carrier R" "x \<in> carrier R" "y \<in> carrier R"
|
ballarin@20318
|
762 |
and axI: "a \<otimes> x \<in> I"
|
ballarin@20318
|
763 |
shows "a \<otimes> (x \<otimes> y) \<in> I"
|
ballarin@20318
|
764 |
proof -
|
ballarin@20318
|
765 |
from axI and carr
|
ballarin@20318
|
766 |
have "(a \<otimes> x) \<otimes> y \<in> I" by (simp add: I_r_closed)
|
ballarin@20318
|
767 |
also from carr
|
ballarin@20318
|
768 |
have "(a \<otimes> x) \<otimes> y = a \<otimes> (x \<otimes> y)" by (simp add: m_assoc)
|
ballarin@20318
|
769 |
finally
|
ballarin@20318
|
770 |
show "a \<otimes> (x \<otimes> y) \<in> I" .
|
ballarin@20318
|
771 |
qed
|
ballarin@20318
|
772 |
|
ballarin@20318
|
773 |
lemma (in ideal) helper_max_prime:
|
ballarin@27611
|
774 |
assumes "cring R"
|
ballarin@20318
|
775 |
assumes acarr: "a \<in> carrier R"
|
ballarin@20318
|
776 |
shows "ideal {x\<in>carrier R. a \<otimes> x \<in> I} R"
|
ballarin@27611
|
777 |
proof -
|
ballarin@27611
|
778 |
interpret cring [R] by fact
|
ballarin@27611
|
779 |
show ?thesis apply (rule idealI)
|
ballarin@27611
|
780 |
apply (rule cring.axioms[OF is_cring])
|
ballarin@27611
|
781 |
apply (rule subgroup.intro)
|
ballarin@27611
|
782 |
apply (simp, fast)
|
ballarin@20318
|
783 |
apply clarsimp apply (simp add: r_distr acarr)
|
ballarin@27611
|
784 |
apply (simp add: acarr)
|
ballarin@27611
|
785 |
apply (simp add: a_inv_def[symmetric], clarify) defer 1
|
ballarin@27611
|
786 |
apply clarsimp defer 1
|
ballarin@27611
|
787 |
apply (fast intro!: helper_I_closed acarr)
|
ballarin@27611
|
788 |
proof -
|
ballarin@27611
|
789 |
fix x
|
ballarin@27611
|
790 |
assume xcarr: "x \<in> carrier R"
|
ballarin@27611
|
791 |
and ax: "a \<otimes> x \<in> I"
|
ballarin@27611
|
792 |
from ax and acarr xcarr
|
ballarin@27611
|
793 |
have "\<ominus>(a \<otimes> x) \<in> I" by simp
|
ballarin@27611
|
794 |
also from acarr xcarr
|
ballarin@27611
|
795 |
have "\<ominus>(a \<otimes> x) = a \<otimes> (\<ominus>x)" by algebra
|
ballarin@27611
|
796 |
finally
|
ballarin@27611
|
797 |
show "a \<otimes> (\<ominus>x) \<in> I" .
|
ballarin@27611
|
798 |
from acarr
|
ballarin@27611
|
799 |
have "a \<otimes> \<zero> = \<zero>" by simp
|
ballarin@27611
|
800 |
next
|
ballarin@27611
|
801 |
fix x y
|
ballarin@27611
|
802 |
assume xcarr: "x \<in> carrier R"
|
ballarin@27611
|
803 |
and ycarr: "y \<in> carrier R"
|
ballarin@27611
|
804 |
and ayI: "a \<otimes> y \<in> I"
|
ballarin@27611
|
805 |
from ayI and acarr xcarr ycarr
|
ballarin@27611
|
806 |
have "a \<otimes> (y \<otimes> x) \<in> I" by (simp add: helper_I_closed)
|
ballarin@27611
|
807 |
moreover from xcarr ycarr
|
ballarin@27611
|
808 |
have "y \<otimes> x = x \<otimes> y" by (simp add: m_comm)
|
ballarin@27611
|
809 |
ultimately
|
ballarin@27611
|
810 |
show "a \<otimes> (x \<otimes> y) \<in> I" by simp
|
ballarin@27611
|
811 |
qed
|
ballarin@20318
|
812 |
qed
|
ballarin@20318
|
813 |
|
ballarin@20318
|
814 |
text {* In a cring every maximal ideal is prime *}
|
ballarin@20318
|
815 |
lemma (in cring) maximalideal_is_prime:
|
ballarin@27611
|
816 |
assumes "maximalideal I R"
|
ballarin@20318
|
817 |
shows "primeideal I R"
|
ballarin@20318
|
818 |
proof -
|
ballarin@27611
|
819 |
interpret maximalideal [I R] by fact
|
ballarin@27611
|
820 |
show ?thesis apply (rule ccontr)
|
ballarin@27611
|
821 |
apply (rule primeidealCE)
|
ballarin@27611
|
822 |
apply (rule is_cring)
|
ballarin@27611
|
823 |
apply assumption
|
ballarin@27611
|
824 |
apply (simp add: I_notcarr)
|
ballarin@27611
|
825 |
proof -
|
ballarin@27611
|
826 |
assume "\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I"
|
ballarin@27611
|
827 |
from this
|
ballarin@27611
|
828 |
obtain a b
|
ballarin@27611
|
829 |
where acarr: "a \<in> carrier R"
|
ballarin@27611
|
830 |
and bcarr: "b \<in> carrier R"
|
ballarin@27611
|
831 |
and abI: "a \<otimes> b \<in> I"
|
ballarin@27611
|
832 |
and anI: "a \<notin> I"
|
ballarin@27611
|
833 |
and bnI: "b \<notin> I"
|
ballarin@20318
|
834 |
by fast
|
ballarin@27611
|
835 |
def J \<equiv> "{x\<in>carrier R. a \<otimes> x \<in> I}"
|
ballarin@27611
|
836 |
|
ballarin@27611
|
837 |
from R.is_cring and acarr
|
ballarin@27611
|
838 |
have idealJ: "ideal J R" unfolding J_def by (rule helper_max_prime)
|
ballarin@27611
|
839 |
|
ballarin@27611
|
840 |
have IsubJ: "I \<subseteq> J"
|
ballarin@27611
|
841 |
proof
|
ballarin@27611
|
842 |
fix x
|
ballarin@27611
|
843 |
assume xI: "x \<in> I"
|
ballarin@27611
|
844 |
from this and acarr
|
ballarin@27611
|
845 |
have "a \<otimes> x \<in> I" by (intro I_l_closed)
|
ballarin@27611
|
846 |
from xI[THEN a_Hcarr] this
|
ballarin@27611
|
847 |
show "x \<in> J" unfolding J_def by fast
|
ballarin@27611
|
848 |
qed
|
ballarin@27611
|
849 |
|
ballarin@27611
|
850 |
from abI and acarr bcarr
|
ballarin@27611
|
851 |
have "b \<in> J" unfolding J_def by fast
|
ballarin@27611
|
852 |
from bnI and this
|
ballarin@27611
|
853 |
have JnI: "J \<noteq> I" by fast
|
ballarin@27611
|
854 |
from acarr
|
ballarin@27611
|
855 |
have "a = a \<otimes> \<one>" by algebra
|
ballarin@27611
|
856 |
from this and anI
|
ballarin@27611
|
857 |
have "a \<otimes> \<one> \<notin> I" by simp
|
ballarin@27611
|
858 |
from one_closed and this
|
ballarin@27611
|
859 |
have "\<one> \<notin> J" unfolding J_def by fast
|
ballarin@27611
|
860 |
hence Jncarr: "J \<noteq> carrier R" by fast
|
ballarin@27611
|
861 |
|
ballarin@27611
|
862 |
interpret ideal ["J" "R"] by (rule idealJ)
|
ballarin@27611
|
863 |
|
ballarin@27611
|
864 |
have "J = I \<or> J = carrier R"
|
ballarin@27611
|
865 |
apply (intro I_maximal)
|
ballarin@27611
|
866 |
apply (rule idealJ)
|
ballarin@27611
|
867 |
apply (rule IsubJ)
|
ballarin@27611
|
868 |
apply (rule a_subset)
|
ballarin@27611
|
869 |
done
|
ballarin@27611
|
870 |
|
ballarin@27611
|
871 |
from this and JnI and Jncarr
|
ballarin@27611
|
872 |
show "False" by simp
|
ballarin@20318
|
873 |
qed
|
ballarin@20318
|
874 |
qed
|
ballarin@20318
|
875 |
|
ballarin@20318
|
876 |
subsection {* Derived Theorems Involving Ideals *}
|
ballarin@20318
|
877 |
|
ballarin@20318
|
878 |
--"A non-zero cring that has only the two trivial ideals is a field"
|
ballarin@20318
|
879 |
lemma (in cring) trivialideals_fieldI:
|
ballarin@20318
|
880 |
assumes carrnzero: "carrier R \<noteq> {\<zero>}"
|
ballarin@20318
|
881 |
and haveideals: "{I. ideal I R} = {{\<zero>}, carrier R}"
|
ballarin@20318
|
882 |
shows "field R"
|
ballarin@20318
|
883 |
apply (rule cring_fieldI)
|
ballarin@20318
|
884 |
apply (rule, rule, rule)
|
ballarin@20318
|
885 |
apply (erule Units_closed)
|
ballarin@20318
|
886 |
defer 1
|
ballarin@20318
|
887 |
apply rule
|
ballarin@20318
|
888 |
defer 1
|
ballarin@20318
|
889 |
proof (rule ccontr, simp)
|
ballarin@20318
|
890 |
assume zUnit: "\<zero> \<in> Units R"
|
ballarin@20318
|
891 |
hence a: "\<zero> \<otimes> inv \<zero> = \<one>" by (rule Units_r_inv)
|
ballarin@20318
|
892 |
from zUnit
|
ballarin@20318
|
893 |
have "\<zero> \<otimes> inv \<zero> = \<zero>" by (intro l_null, rule Units_inv_closed)
|
ballarin@20318
|
894 |
from a[symmetric] and this
|
ballarin@20318
|
895 |
have "\<one> = \<zero>" by simp
|
ballarin@20318
|
896 |
hence "carrier R = {\<zero>}" by (rule one_zeroD)
|
ballarin@20318
|
897 |
from this and carrnzero
|
ballarin@20318
|
898 |
show "False" by simp
|
ballarin@20318
|
899 |
next
|
ballarin@20318
|
900 |
fix x
|
ballarin@20318
|
901 |
assume xcarr': "x \<in> carrier R - {\<zero>}"
|
ballarin@20318
|
902 |
hence xcarr: "x \<in> carrier R" by fast
|
ballarin@20318
|
903 |
from xcarr'
|
ballarin@20318
|
904 |
have xnZ: "x \<noteq> \<zero>" by fast
|
ballarin@20318
|
905 |
from xcarr
|
ballarin@20318
|
906 |
have xIdl: "ideal (PIdl x) R" by (intro cgenideal_ideal, fast)
|
ballarin@20318
|
907 |
|
ballarin@20318
|
908 |
from xcarr
|
ballarin@20318
|
909 |
have "x \<in> PIdl x" by (intro cgenideal_self, fast)
|
ballarin@20318
|
910 |
from this and xnZ
|
ballarin@20318
|
911 |
have "PIdl x \<noteq> {\<zero>}" by fast
|
ballarin@20318
|
912 |
from haveideals and this
|
ballarin@20318
|
913 |
have "PIdl x = carrier R"
|
ballarin@20318
|
914 |
by (blast intro!: xIdl)
|
ballarin@20318
|
915 |
hence "\<one> \<in> PIdl x" by simp
|
ballarin@20318
|
916 |
hence "\<exists>y. \<one> = y \<otimes> x \<and> y \<in> carrier R" unfolding cgenideal_def by blast
|
ballarin@20318
|
917 |
from this
|
ballarin@20318
|
918 |
obtain y
|
ballarin@20318
|
919 |
where ycarr: " y \<in> carrier R"
|
ballarin@20318
|
920 |
and ylinv: "\<one> = y \<otimes> x"
|
ballarin@20318
|
921 |
by fast+
|
ballarin@20318
|
922 |
from ylinv and xcarr ycarr
|
ballarin@20318
|
923 |
have yrinv: "\<one> = x \<otimes> y" by (simp add: m_comm)
|
ballarin@20318
|
924 |
from ycarr and ylinv[symmetric] and yrinv[symmetric]
|
ballarin@20318
|
925 |
have "\<exists>y \<in> carrier R. y \<otimes> x = \<one> \<and> x \<otimes> y = \<one>" by fast
|
ballarin@20318
|
926 |
from this and xcarr
|
ballarin@20318
|
927 |
show "x \<in> Units R"
|
ballarin@20318
|
928 |
unfolding Units_def
|
ballarin@20318
|
929 |
by fast
|
ballarin@20318
|
930 |
qed
|
ballarin@20318
|
931 |
|
ballarin@20318
|
932 |
lemma (in field) all_ideals:
|
ballarin@20318
|
933 |
shows "{I. ideal I R} = {{\<zero>}, carrier R}"
|
ballarin@20318
|
934 |
apply (rule, rule)
|
ballarin@20318
|
935 |
proof -
|
ballarin@20318
|
936 |
fix I
|
ballarin@20318
|
937 |
assume a: "I \<in> {I. ideal I R}"
|
ballarin@20318
|
938 |
with this
|
ballarin@20318
|
939 |
interpret ideal ["I" "R"] by simp
|
ballarin@20318
|
940 |
|
ballarin@20318
|
941 |
show "I \<in> {{\<zero>}, carrier R}"
|
ballarin@20318
|
942 |
proof (cases "\<exists>a. a \<in> I - {\<zero>}")
|
ballarin@20318
|
943 |
assume "\<exists>a. a \<in> I - {\<zero>}"
|
ballarin@20318
|
944 |
from this
|
ballarin@20318
|
945 |
obtain a
|
ballarin@20318
|
946 |
where aI: "a \<in> I"
|
ballarin@20318
|
947 |
and anZ: "a \<noteq> \<zero>"
|
ballarin@20318
|
948 |
by fast+
|
ballarin@20318
|
949 |
from aI[THEN a_Hcarr] anZ
|
ballarin@20318
|
950 |
have aUnit: "a \<in> Units R" by (simp add: field_Units)
|
ballarin@20318
|
951 |
hence a: "a \<otimes> inv a = \<one>" by (rule Units_r_inv)
|
ballarin@20318
|
952 |
from aI and aUnit
|
ballarin@27698
|
953 |
have "a \<otimes> inv a \<in> I" by (simp add: I_r_closed del: Units_r_inv)
|
ballarin@20318
|
954 |
hence oneI: "\<one> \<in> I" by (simp add: a[symmetric])
|
ballarin@20318
|
955 |
|
ballarin@20318
|
956 |
have "carrier R \<subseteq> I"
|
ballarin@20318
|
957 |
proof
|
ballarin@20318
|
958 |
fix x
|
ballarin@20318
|
959 |
assume xcarr: "x \<in> carrier R"
|
ballarin@20318
|
960 |
from oneI and this
|
ballarin@20318
|
961 |
have "\<one> \<otimes> x \<in> I" by (rule I_r_closed)
|
ballarin@20318
|
962 |
from this and xcarr
|
ballarin@20318
|
963 |
show "x \<in> I" by simp
|
ballarin@20318
|
964 |
qed
|
ballarin@20318
|
965 |
from this and a_subset
|
ballarin@20318
|
966 |
have "I = carrier R" by fast
|
ballarin@20318
|
967 |
thus "I \<in> {{\<zero>}, carrier R}" by fast
|
ballarin@20318
|
968 |
next
|
ballarin@20318
|
969 |
assume "\<not> (\<exists>a. a \<in> I - {\<zero>})"
|
ballarin@20318
|
970 |
hence IZ: "\<And>a. a \<in> I \<Longrightarrow> a = \<zero>" by simp
|
ballarin@20318
|
971 |
|
ballarin@20318
|
972 |
have a: "I \<subseteq> {\<zero>}"
|
ballarin@20318
|
973 |
proof
|
ballarin@20318
|
974 |
fix x
|
ballarin@20318
|
975 |
assume "x \<in> I"
|
ballarin@20318
|
976 |
hence "x = \<zero>" by (rule IZ)
|
ballarin@20318
|
977 |
thus "x \<in> {\<zero>}" by fast
|
ballarin@20318
|
978 |
qed
|
ballarin@20318
|
979 |
|
ballarin@20318
|
980 |
have "\<zero> \<in> I" by simp
|
ballarin@20318
|
981 |
hence "{\<zero>} \<subseteq> I" by fast
|
ballarin@20318
|
982 |
|
ballarin@20318
|
983 |
from this and a
|
ballarin@20318
|
984 |
have "I = {\<zero>}" by fast
|
ballarin@20318
|
985 |
thus "I \<in> {{\<zero>}, carrier R}" by fast
|
ballarin@20318
|
986 |
qed
|
ballarin@20318
|
987 |
qed (simp add: zeroideal oneideal)
|
ballarin@20318
|
988 |
|
ballarin@20318
|
989 |
--"Jacobson Theorem 2.2"
|
ballarin@20318
|
990 |
lemma (in cring) trivialideals_eq_field:
|
ballarin@20318
|
991 |
assumes carrnzero: "carrier R \<noteq> {\<zero>}"
|
ballarin@20318
|
992 |
shows "({I. ideal I R} = {{\<zero>}, carrier R}) = field R"
|
ballarin@20318
|
993 |
by (fast intro!: trivialideals_fieldI[OF carrnzero] field.all_ideals)
|
ballarin@20318
|
994 |
|
ballarin@20318
|
995 |
|
ballarin@20318
|
996 |
text {* Like zeroprimeideal for domains *}
|
ballarin@20318
|
997 |
lemma (in field) zeromaximalideal:
|
ballarin@20318
|
998 |
"maximalideal {\<zero>} R"
|
ballarin@20318
|
999 |
apply (rule maximalidealI)
|
ballarin@20318
|
1000 |
apply (rule zeroideal)
|
ballarin@20318
|
1001 |
proof-
|
ballarin@20318
|
1002 |
from one_not_zero
|
ballarin@20318
|
1003 |
have "\<one> \<notin> {\<zero>}" by simp
|
ballarin@20318
|
1004 |
from this and one_closed
|
ballarin@20318
|
1005 |
show "carrier R \<noteq> {\<zero>}" by fast
|
ballarin@20318
|
1006 |
next
|
ballarin@20318
|
1007 |
fix J
|
ballarin@20318
|
1008 |
assume Jideal: "ideal J R"
|
ballarin@20318
|
1009 |
hence "J \<in> {I. ideal I R}"
|
ballarin@20318
|
1010 |
by fast
|
ballarin@20318
|
1011 |
|
ballarin@20318
|
1012 |
from this and all_ideals
|
ballarin@20318
|
1013 |
show "J = {\<zero>} \<or> J = carrier R" by simp
|
ballarin@20318
|
1014 |
qed
|
ballarin@20318
|
1015 |
|
ballarin@20318
|
1016 |
lemma (in cring) zeromaximalideal_fieldI:
|
ballarin@20318
|
1017 |
assumes zeromax: "maximalideal {\<zero>} R"
|
ballarin@20318
|
1018 |
shows "field R"
|
ballarin@20318
|
1019 |
apply (rule trivialideals_fieldI, rule maximalideal.I_notcarr[OF zeromax])
|
ballarin@20318
|
1020 |
apply rule apply clarsimp defer 1
|
ballarin@20318
|
1021 |
apply (simp add: zeroideal oneideal)
|
ballarin@20318
|
1022 |
proof -
|
ballarin@20318
|
1023 |
fix J
|
ballarin@20318
|
1024 |
assume Jn0: "J \<noteq> {\<zero>}"
|
ballarin@20318
|
1025 |
and idealJ: "ideal J R"
|
ballarin@20318
|
1026 |
interpret ideal ["J" "R"] by (rule idealJ)
|
ballarin@20318
|
1027 |
have "{\<zero>} \<subseteq> J" by (rule ccontr, simp)
|
ballarin@20318
|
1028 |
from zeromax and idealJ and this and a_subset
|
ballarin@20318
|
1029 |
have "J = {\<zero>} \<or> J = carrier R" by (rule maximalideal.I_maximal)
|
ballarin@20318
|
1030 |
from this and Jn0
|
ballarin@20318
|
1031 |
show "J = carrier R" by simp
|
ballarin@20318
|
1032 |
qed
|
ballarin@20318
|
1033 |
|
ballarin@20318
|
1034 |
lemma (in cring) zeromaximalideal_eq_field:
|
ballarin@20318
|
1035 |
"maximalideal {\<zero>} R = field R"
|
ballarin@20318
|
1036 |
apply rule
|
ballarin@20318
|
1037 |
apply (erule zeromaximalideal_fieldI)
|
ballarin@20318
|
1038 |
apply (erule field.zeromaximalideal)
|
ballarin@20318
|
1039 |
done
|
ballarin@20318
|
1040 |
|
ballarin@20318
|
1041 |
end
|