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