src/HOL/Algebra/Ideal.thy
 author wenzelm Thu Oct 22 23:01:49 2015 +0200 (2015-10-22) changeset 61506 436b7fe89cdc parent 61382 efac889fccbc child 61952 546958347e05 permissions -rw-r--r--
tuned;
1 (*  Title:      HOL/Algebra/Ideal.thy
2     Author:     Stephan Hohe, TU Muenchen
3 *)
5 theory Ideal
6 imports Ring AbelCoset
7 begin
9 section \<open>Ideals\<close>
11 subsection \<open>Definitions\<close>
13 subsubsection \<open>General definition\<close>
15 locale ideal = additive_subgroup I R + ring R for I and R (structure) +
16   assumes I_l_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
17     and I_r_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
19 sublocale ideal \<subseteq> abelian_subgroup I R
20   apply (intro abelian_subgroupI3 abelian_group.intro)
21     apply (rule ideal.axioms, rule ideal_axioms)
22    apply (rule abelian_group.axioms, rule ring.axioms, rule ideal.axioms, rule ideal_axioms)
23   apply (rule abelian_group.axioms, rule ring.axioms, rule ideal.axioms, rule ideal_axioms)
24   done
26 lemma (in ideal) is_ideal: "ideal I R"
27   by (rule ideal_axioms)
29 lemma idealI:
30   fixes R (structure)
31   assumes "ring R"
32   assumes a_subgroup: "subgroup I \<lparr>carrier = carrier R, mult = add R, one = zero R\<rparr>"
33     and I_l_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
34     and I_r_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
35   shows "ideal I R"
36 proof -
37   interpret ring R by fact
38   show ?thesis  apply (intro ideal.intro ideal_axioms.intro additive_subgroupI)
39      apply (rule a_subgroup)
40     apply (rule is_ring)
41    apply (erule (1) I_l_closed)
42   apply (erule (1) I_r_closed)
43   done
44 qed
47 subsubsection (in ring) \<open>Ideals Generated by a Subset of @{term "carrier R"}\<close>
49 definition genideal :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set"  ("Idl\<index> _"  79)
50   where "genideal R S = Inter {I. ideal I R \<and> S \<subseteq> I}"
52 subsubsection \<open>Principal Ideals\<close>
54 locale principalideal = ideal +
55   assumes generate: "\<exists>i \<in> carrier R. I = Idl {i}"
57 lemma (in principalideal) is_principalideal: "principalideal I R"
58   by (rule principalideal_axioms)
60 lemma principalidealI:
61   fixes R (structure)
62   assumes "ideal I R"
63     and generate: "\<exists>i \<in> carrier R. I = Idl {i}"
64   shows "principalideal I R"
65 proof -
66   interpret ideal I R by fact
67   show ?thesis
68     by (intro principalideal.intro principalideal_axioms.intro)
69       (rule is_ideal, rule generate)
70 qed
73 subsubsection \<open>Maximal Ideals\<close>
75 locale maximalideal = ideal +
76   assumes I_notcarr: "carrier R \<noteq> I"
77     and I_maximal: "\<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> J = I \<or> J = carrier R"
79 lemma (in maximalideal) is_maximalideal: "maximalideal I R"
80   by (rule maximalideal_axioms)
82 lemma maximalidealI:
83   fixes R
84   assumes "ideal I R"
85     and I_notcarr: "carrier R \<noteq> I"
86     and I_maximal: "\<And>J. \<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> J = I \<or> J = carrier R"
87   shows "maximalideal I R"
88 proof -
89   interpret ideal I R by fact
90   show ?thesis
91     by (intro maximalideal.intro maximalideal_axioms.intro)
92       (rule is_ideal, rule I_notcarr, rule I_maximal)
93 qed
96 subsubsection \<open>Prime Ideals\<close>
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: "primeideal I R"
103   by (rule primeideal_axioms)
105 lemma primeidealI:
106   fixes R (structure)
107   assumes "ideal I R"
108     and "cring R"
109     and I_notcarr: "carrier R \<noteq> I"
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"
111   shows "primeideal I R"
112 proof -
113   interpret ideal I R by fact
114   interpret cring R by fact
115   show ?thesis
116     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     and "cring R"
124     and 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
143 subsection \<open>Special Ideals\<close>
145 lemma (in ring) zeroideal: "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: "ideal (carrier R) R"
154   by (rule idealI) (auto intro: is_ring add.subgroupI)
156 lemma (in "domain") zeroprimeideal: "primeideal {\<zero>} R"
157   apply (intro primeidealI)
158      apply (rule zeroideal)
159     apply (rule domain.axioms, rule domain_axioms)
160    defer 1
161    apply (simp add: integral)
162 proof (rule ccontr, simp)
163   assume "carrier R = {\<zero>}"
164   then have "\<one> = \<zero>" by (rule one_zeroI)
165   with one_not_zero show False by simp
166 qed
169 subsection \<open>General Ideal Properies\<close>
171 lemma (in ideal) one_imp_carrier:
172   assumes I_one_closed: "\<one> \<in> I"
173   shows "I = carrier R"
174   apply (rule)
175   apply (rule)
176   apply (rule a_Hcarr, simp)
177 proof
178   fix x
179   assume xcarr: "x \<in> carrier R"
180   with I_one_closed have "x \<otimes> \<one> \<in> I" by (intro I_l_closed)
181   with xcarr show "x \<in> I" by simp
182 qed
184 lemma (in ideal) Icarr:
185   assumes iI: "i \<in> I"
186   shows "i \<in> carrier R"
187   using iI by (rule a_Hcarr)
190 subsection \<open>Intersection of Ideals\<close>
192 paragraph \<open>Intersection of two ideals\<close>
193 text \<open>The intersection of any two ideals is again an ideal in @{term R}\<close>
195 lemma (in ring) i_intersect:
196   assumes "ideal I R"
197   assumes "ideal J R"
198   shows "ideal (I \<inter> J) R"
199 proof -
200   interpret ideal I R by fact
201   interpret ideal J R by fact
202   show ?thesis
203     apply (intro idealI subgroup.intro)
204           apply (rule is_ring)
205          apply (force simp add: a_subset)
206         apply (simp add: a_inv_def[symmetric])
207        apply simp
208       apply (simp add: a_inv_def[symmetric])
209      apply (clarsimp, rule)
210       apply (fast intro: ideal.I_l_closed ideal.intro assms)+
211     apply (clarsimp, rule)
212      apply (fast intro: ideal.I_r_closed ideal.intro assms)+
213     done
214 qed
216 text \<open>The intersection of any Number of Ideals is again
217         an Ideal in @{term R}\<close>
218 lemma (in ring) i_Intersect:
219   assumes Sideals: "\<And>I. I \<in> S \<Longrightarrow> ideal I R"
220     and notempty: "S \<noteq> {}"
221   shows "ideal (Inter S) R"
222   apply (unfold_locales)
223   apply (simp_all add: Inter_eq)
224         apply rule unfolding mem_Collect_eq defer 1
225         apply rule defer 1
226         apply rule defer 1
227         apply (fold a_inv_def, rule) defer 1
228         apply rule defer 1
229         apply rule defer 1
230 proof -
231   fix x y
232   assume "\<forall>I\<in>S. x \<in> I"
233   then have xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp
234   assume "\<forall>I\<in>S. y \<in> I"
235   then have yI: "\<And>I. I \<in> S \<Longrightarrow> y \<in> I" by simp
237   fix J
238   assume JS: "J \<in> S"
239   interpret ideal J R by (rule Sideals[OF JS])
240   from xI[OF JS] and yI[OF JS] show "x \<oplus> y \<in> J" by (rule a_closed)
241 next
242   fix J
243   assume JS: "J \<in> S"
244   interpret ideal J R by (rule Sideals[OF JS])
245   show "\<zero> \<in> J" by simp
246 next
247   fix x
248   assume "\<forall>I\<in>S. x \<in> I"
249   then have xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp
251   fix J
252   assume JS: "J \<in> S"
253   interpret ideal J R by (rule Sideals[OF JS])
255   from xI[OF JS] show "\<ominus> x \<in> J" by (rule a_inv_closed)
256 next
257   fix x y
258   assume "\<forall>I\<in>S. x \<in> I"
259   then have xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp
260   assume ycarr: "y \<in> carrier R"
262   fix J
263   assume JS: "J \<in> S"
264   interpret ideal J R by (rule Sideals[OF JS])
266   from xI[OF JS] and ycarr show "y \<otimes> x \<in> J" by (rule I_l_closed)
267 next
268   fix x y
269   assume "\<forall>I\<in>S. x \<in> I"
270   then have xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp
271   assume ycarr: "y \<in> carrier R"
273   fix J
274   assume JS: "J \<in> S"
275   interpret ideal J R by (rule Sideals[OF JS])
277   from xI[OF JS] and ycarr show "x \<otimes> y \<in> J" by (rule I_r_closed)
278 next
279   fix x
280   assume "\<forall>I\<in>S. x \<in> I"
281   then have xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp
283   from notempty have "\<exists>I0. I0 \<in> S" by blast
284   then obtain I0 where I0S: "I0 \<in> S" by auto
286   interpret ideal I0 R by (rule Sideals[OF I0S])
288   from xI[OF I0S] have "x \<in> I0" .
289   with a_subset show "x \<in> carrier R" by fast
290 next
292 qed
295 subsection \<open>Addition of Ideals\<close>
297 lemma (in ring) add_ideals:
298   assumes idealI: "ideal I R"
299       and idealJ: "ideal J R"
300   shows "ideal (I <+> J) R"
301   apply (rule ideal.intro)
303      apply (intro ideal.axioms[OF idealI])
304     apply (intro ideal.axioms[OF idealJ])
305    apply (rule is_ring)
306   apply (rule ideal_axioms.intro)
307    apply (simp add: set_add_defs, clarsimp) defer 1
308    apply (simp add: set_add_defs, clarsimp) defer 1
309 proof -
310   fix x i j
311   assume xcarr: "x \<in> carrier R"
312     and iI: "i \<in> I"
313     and jJ: "j \<in> J"
314   from xcarr ideal.Icarr[OF idealI iI] ideal.Icarr[OF idealJ jJ]
315   have c: "(i \<oplus> j) \<otimes> x = (i \<otimes> x) \<oplus> (j \<otimes> x)"
316     by algebra
317   from xcarr and iI have a: "i \<otimes> x \<in> I"
318     by (simp add: ideal.I_r_closed[OF idealI])
319   from xcarr and jJ have b: "j \<otimes> x \<in> J"
320     by (simp add: ideal.I_r_closed[OF idealJ])
321   from a b c show "\<exists>ha\<in>I. \<exists>ka\<in>J. (i \<oplus> j) \<otimes> x = ha \<oplus> ka"
322     by fast
323 next
324   fix x i j
325   assume xcarr: "x \<in> carrier R"
326     and iI: "i \<in> I"
327     and jJ: "j \<in> J"
328   from xcarr ideal.Icarr[OF idealI iI] ideal.Icarr[OF idealJ jJ]
329   have c: "x \<otimes> (i \<oplus> j) = (x \<otimes> i) \<oplus> (x \<otimes> j)" by algebra
330   from xcarr and iI have a: "x \<otimes> i \<in> I"
331     by (simp add: ideal.I_l_closed[OF idealI])
332   from xcarr and jJ have b: "x \<otimes> j \<in> J"
333     by (simp add: ideal.I_l_closed[OF idealJ])
334   from a b c show "\<exists>ha\<in>I. \<exists>ka\<in>J. x \<otimes> (i \<oplus> j) = ha \<oplus> ka"
335     by fast
336 qed
339 subsection (in ring) \<open>Ideals generated by a subset of @{term "carrier R"}\<close>
341 text \<open>@{term genideal} generates an ideal\<close>
342 lemma (in ring) genideal_ideal:
343   assumes Scarr: "S \<subseteq> carrier R"
344   shows "ideal (Idl S) R"
345 unfolding genideal_def
346 proof (rule i_Intersect, fast, simp)
347   from oneideal and Scarr
348   show "\<exists>I. ideal I R \<and> S \<le> I" by fast
349 qed
351 lemma (in ring) genideal_self:
352   assumes "S \<subseteq> carrier R"
353   shows "S \<subseteq> Idl S"
354   unfolding genideal_def by fast
356 lemma (in ring) genideal_self':
357   assumes carr: "i \<in> carrier R"
358   shows "i \<in> Idl {i}"
359 proof -
360   from carr have "{i} \<subseteq> Idl {i}" by (fast intro!: genideal_self)
361   then show "i \<in> Idl {i}" by fast
362 qed
364 text \<open>@{term genideal} generates the minimal ideal\<close>
365 lemma (in ring) genideal_minimal:
366   assumes a: "ideal I R"
367     and b: "S \<subseteq> I"
368   shows "Idl S \<subseteq> I"
369   unfolding genideal_def by rule (elim InterD, simp add: a b)
371 text \<open>Generated ideals and subsets\<close>
372 lemma (in ring) Idl_subset_ideal:
373   assumes Iideal: "ideal I R"
374     and Hcarr: "H \<subseteq> carrier R"
375   shows "(Idl H \<subseteq> I) = (H \<subseteq> I)"
376 proof
377   assume a: "Idl H \<subseteq> I"
378   from Hcarr have "H \<subseteq> Idl H" by (rule genideal_self)
379   with a show "H \<subseteq> I" by simp
380 next
381   fix x
382   assume "H \<subseteq> I"
383   with Iideal have "I \<in> {I. ideal I R \<and> H \<subseteq> I}" by fast
384   then show "Idl H \<subseteq> I" unfolding genideal_def by fast
385 qed
387 lemma (in ring) subset_Idl_subset:
388   assumes Icarr: "I \<subseteq> carrier R"
389     and HI: "H \<subseteq> I"
390   shows "Idl H \<subseteq> Idl I"
391 proof -
392   from HI and genideal_self[OF Icarr] have HIdlI: "H \<subseteq> Idl I"
393     by fast
395   from Icarr have Iideal: "ideal (Idl I) R"
396     by (rule genideal_ideal)
397   from HI and Icarr have "H \<subseteq> carrier R"
398     by fast
399   with Iideal have "(H \<subseteq> Idl I) = (Idl H \<subseteq> Idl I)"
400     by (rule Idl_subset_ideal[symmetric])
402   with HIdlI show "Idl H \<subseteq> Idl I" by simp
403 qed
405 lemma (in ring) Idl_subset_ideal':
406   assumes acarr: "a \<in> carrier R" and bcarr: "b \<in> carrier R"
407   shows "(Idl {a} \<subseteq> Idl {b}) = (a \<in> Idl {b})"
408   apply (subst Idl_subset_ideal[OF genideal_ideal[of "{b}"], of "{a}"])
409     apply (fast intro: bcarr, fast intro: acarr)
410   apply fast
411   done
413 lemma (in ring) genideal_zero: "Idl {\<zero>} = {\<zero>}"
414   apply rule
415    apply (rule genideal_minimal[OF zeroideal], simp)
416   apply (simp add: genideal_self')
417   done
419 lemma (in ring) genideal_one: "Idl {\<one>} = carrier R"
420 proof -
421   interpret ideal "Idl {\<one>}" "R" by (rule genideal_ideal) fast
422   show "Idl {\<one>} = carrier R"
423   apply (rule, rule a_subset)
424   apply (simp add: one_imp_carrier genideal_self')
425   done
426 qed
429 text \<open>Generation of Principal Ideals in Commutative Rings\<close>
431 definition cgenideal :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set"  ("PIdl\<index> _"  79)
432   where "cgenideal R a = {x \<otimes>\<^bsub>R\<^esub> a | x. x \<in> carrier R}"
434 text \<open>genhideal (?) really generates an ideal\<close>
435 lemma (in cring) cgenideal_ideal:
436   assumes acarr: "a \<in> carrier R"
437   shows "ideal (PIdl a) R"
438   apply (unfold cgenideal_def)
439   apply (rule idealI[OF is_ring])
440      apply (rule subgroup.intro)
441         apply simp_all
442         apply (blast intro: acarr)
443         apply clarsimp defer 1
444         defer 1
445         apply (fold a_inv_def, clarsimp) defer 1
446         apply clarsimp defer 1
447         apply clarsimp defer 1
448 proof -
449   fix x y
450   assume xcarr: "x \<in> carrier R"
451     and ycarr: "y \<in> carrier R"
452   note carr = acarr xcarr ycarr
454   from carr have "x \<otimes> a \<oplus> y \<otimes> a = (x \<oplus> y) \<otimes> a"
455     by (simp add: l_distr)
456   with carr show "\<exists>z. x \<otimes> a \<oplus> y \<otimes> a = z \<otimes> a \<and> z \<in> carrier R"
457     by fast
458 next
459   from l_null[OF acarr, symmetric] and zero_closed
460   show "\<exists>x. \<zero> = x \<otimes> a \<and> x \<in> carrier R" by fast
461 next
462   fix x
463   assume xcarr: "x \<in> carrier R"
464   note carr = acarr xcarr
466   from carr have "\<ominus> (x \<otimes> a) = (\<ominus> x) \<otimes> a"
467     by (simp add: l_minus)
468   with carr show "\<exists>z. \<ominus> (x \<otimes> a) = z \<otimes> a \<and> z \<in> carrier R"
469     by fast
470 next
471   fix x y
472   assume xcarr: "x \<in> carrier R"
473      and ycarr: "y \<in> carrier R"
474   note carr = acarr xcarr ycarr
476   from carr have "y \<otimes> a \<otimes> x = (y \<otimes> x) \<otimes> a"
477     by (simp add: m_assoc) (simp add: m_comm)
478   with carr show "\<exists>z. y \<otimes> a \<otimes> x = z \<otimes> a \<and> z \<in> carrier R"
479     by fast
480 next
481   fix x y
482   assume xcarr: "x \<in> carrier R"
483      and ycarr: "y \<in> carrier R"
484   note carr = acarr xcarr ycarr
486   from carr have "x \<otimes> (y \<otimes> a) = (x \<otimes> y) \<otimes> a"
487     by (simp add: m_assoc)
488   with carr show "\<exists>z. x \<otimes> (y \<otimes> a) = z \<otimes> a \<and> z \<in> carrier R"
489     by fast
490 qed
492 lemma (in ring) cgenideal_self:
493   assumes icarr: "i \<in> carrier R"
494   shows "i \<in> PIdl i"
495   unfolding cgenideal_def
496 proof simp
497   from icarr have "i = \<one> \<otimes> i"
498     by simp
499   with icarr show "\<exists>x. i = x \<otimes> i \<and> x \<in> carrier R"
500     by fast
501 qed
503 text \<open>@{const "cgenideal"} is minimal\<close>
505 lemma (in ring) cgenideal_minimal:
506   assumes "ideal J R"
507   assumes aJ: "a \<in> J"
508   shows "PIdl a \<subseteq> J"
509 proof -
510   interpret ideal J R by fact
511   show ?thesis
512     unfolding cgenideal_def
513     apply rule
514     apply clarify
515     using aJ
516     apply (erule I_l_closed)
517     done
518 qed
520 lemma (in cring) cgenideal_eq_genideal:
521   assumes icarr: "i \<in> carrier R"
522   shows "PIdl i = Idl {i}"
523   apply rule
524    apply (intro cgenideal_minimal)
525     apply (rule genideal_ideal, fast intro: icarr)
526    apply (rule genideal_self', fast intro: icarr)
527   apply (intro genideal_minimal)
528    apply (rule cgenideal_ideal [OF icarr])
529   apply (simp, rule cgenideal_self [OF icarr])
530   done
532 lemma (in cring) cgenideal_eq_rcos: "PIdl i = carrier R #> i"
533   unfolding cgenideal_def r_coset_def by fast
535 lemma (in cring) cgenideal_is_principalideal:
536   assumes icarr: "i \<in> carrier R"
537   shows "principalideal (PIdl i) R"
538   apply (rule principalidealI)
539   apply (rule cgenideal_ideal [OF icarr])
540 proof -
541   from icarr have "PIdl i = Idl {i}"
542     by (rule cgenideal_eq_genideal)
543   with icarr show "\<exists>i'\<in>carrier R. PIdl i = Idl {i'}"
544     by fast
545 qed
548 subsection \<open>Union of Ideals\<close>
550 lemma (in ring) union_genideal:
551   assumes idealI: "ideal I R"
552     and idealJ: "ideal J R"
553   shows "Idl (I \<union> J) = I <+> J"
554   apply rule
555    apply (rule ring.genideal_minimal)
556      apply (rule is_ring)
557     apply (rule add_ideals[OF idealI idealJ])
558    apply (rule)
559    apply (simp add: set_add_defs) apply (elim disjE) defer 1 defer 1
560    apply (rule) apply (simp add: set_add_defs genideal_def) apply clarsimp defer 1
561 proof -
562   fix x
563   assume xI: "x \<in> I"
564   have ZJ: "\<zero> \<in> J"
565     by (intro additive_subgroup.zero_closed) (rule ideal.axioms[OF idealJ])
566   from ideal.Icarr[OF idealI xI] have "x = x \<oplus> \<zero>"
567     by algebra
568   with xI and ZJ show "\<exists>h\<in>I. \<exists>k\<in>J. x = h \<oplus> k"
569     by fast
570 next
571   fix x
572   assume xJ: "x \<in> J"
573   have ZI: "\<zero> \<in> I"
574     by (intro additive_subgroup.zero_closed, rule ideal.axioms[OF idealI])
575   from ideal.Icarr[OF idealJ xJ] have "x = \<zero> \<oplus> x"
576     by algebra
577   with ZI and xJ show "\<exists>h\<in>I. \<exists>k\<in>J. x = h \<oplus> k"
578     by fast
579 next
580   fix i j K
581   assume iI: "i \<in> I"
582     and jJ: "j \<in> J"
583     and idealK: "ideal K R"
584     and IK: "I \<subseteq> K"
585     and JK: "J \<subseteq> K"
586   from iI and IK have iK: "i \<in> K" by fast
587   from jJ and JK have jK: "j \<in> K" by fast
588   from iK and jK show "i \<oplus> j \<in> K"
589     by (intro additive_subgroup.a_closed) (rule ideal.axioms[OF idealK])
590 qed
593 subsection \<open>Properties of Principal Ideals\<close>
595 text \<open>@{text "\<zero>"} generates the zero ideal\<close>
596 lemma (in ring) zero_genideal: "Idl {\<zero>} = {\<zero>}"
597   apply rule
598   apply (simp add: genideal_minimal zeroideal)
599   apply (fast intro!: genideal_self)
600   done
602 text \<open>@{text "\<one>"} generates the unit ideal\<close>
603 lemma (in ring) one_genideal: "Idl {\<one>} = carrier R"
604 proof -
605   have "\<one> \<in> Idl {\<one>}"
606     by (simp add: genideal_self')
607   then show "Idl {\<one>} = carrier R"
608     by (intro ideal.one_imp_carrier) (fast intro: genideal_ideal)
609 qed
612 text \<open>The zero ideal is a principal ideal\<close>
613 corollary (in ring) zeropideal: "principalideal {\<zero>} R"
614   apply (rule principalidealI)
615    apply (rule zeroideal)
616   apply (blast intro!: zero_genideal[symmetric])
617   done
619 text \<open>The unit ideal is a principal ideal\<close>
620 corollary (in ring) onepideal: "principalideal (carrier R) R"
621   apply (rule principalidealI)
622    apply (rule oneideal)
623   apply (blast intro!: one_genideal[symmetric])
624   done
627 text \<open>Every principal ideal is a right coset of the carrier\<close>
628 lemma (in principalideal) rcos_generate:
629   assumes "cring R"
630   shows "\<exists>x\<in>I. I = carrier R #> x"
631 proof -
632   interpret cring R by fact
633   from generate obtain i where icarr: "i \<in> carrier R" and I1: "I = Idl {i}"
634     by fast+
636   from icarr and genideal_self[of "{i}"] have "i \<in> Idl {i}"
637     by fast
638   then have iI: "i \<in> I" by (simp add: I1)
640   from I1 icarr have I2: "I = PIdl i"
641     by (simp add: cgenideal_eq_genideal)
643   have "PIdl i = carrier R #> i"
644     unfolding cgenideal_def r_coset_def by fast
646   with I2 have "I = carrier R #> i"
647     by simp
649   with iI show "\<exists>x\<in>I. I = carrier R #> x"
650     by fast
651 qed
654 subsection \<open>Prime Ideals\<close>
656 lemma (in ideal) primeidealCD:
657   assumes "cring R"
658   assumes notprime: "\<not> primeideal I R"
659   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)"
660 proof (rule ccontr, clarsimp)
661   interpret cring R by fact
662   assume InR: "carrier R \<noteq> I"
663     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)"
664   then have 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"
665     by simp
666   have "primeideal I R"
667     apply (rule primeideal.intro [OF is_ideal is_cring])
668     apply (rule primeideal_axioms.intro)
669      apply (rule InR)
670     apply (erule (2) I_prime)
671     done
672   with notprime show False by simp
673 qed
675 lemma (in ideal) primeidealCE:
676   assumes "cring R"
677   assumes notprime: "\<not> primeideal I R"
678   obtains "carrier R = I"
679     | "\<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"
680 proof -
681   interpret R: cring R by fact
682   assume "carrier R = I ==> thesis"
683     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"
684   then show thesis using primeidealCD [OF R.is_cring notprime] by blast
685 qed
687 text \<open>If @{text "{\<zero>}"} is a prime ideal of a commutative ring, the ring is a domain\<close>
688 lemma (in cring) zeroprimeideal_domainI:
689   assumes pi: "primeideal {\<zero>} R"
690   shows "domain R"
691   apply (rule domain.intro, rule is_cring)
692   apply (rule domain_axioms.intro)
693 proof (rule ccontr, simp)
694   interpret primeideal "{\<zero>}" "R" by (rule pi)
695   assume "\<one> = \<zero>"
696   then have "carrier R = {\<zero>}" by (rule one_zeroD)
697   from this[symmetric] and I_notcarr show False
698     by simp
699 next
700   interpret primeideal "{\<zero>}" "R" by (rule pi)
701   fix a b
702   assume ab: "a \<otimes> b = \<zero>" and carr: "a \<in> carrier R" "b \<in> carrier R"
703   from ab have abI: "a \<otimes> b \<in> {\<zero>}"
704     by fast
705   with carr have "a \<in> {\<zero>} \<or> b \<in> {\<zero>}"
706     by (rule I_prime)
707   then show "a = \<zero> \<or> b = \<zero>" by simp
708 qed
710 corollary (in cring) domain_eq_zeroprimeideal: "domain R = primeideal {\<zero>} R"
711   apply rule
712    apply (erule domain.zeroprimeideal)
713   apply (erule zeroprimeideal_domainI)
714   done
717 subsection \<open>Maximal Ideals\<close>
719 lemma (in ideal) helper_I_closed:
720   assumes carr: "a \<in> carrier R" "x \<in> carrier R" "y \<in> carrier R"
721     and axI: "a \<otimes> x \<in> I"
722   shows "a \<otimes> (x \<otimes> y) \<in> I"
723 proof -
724   from axI and carr have "(a \<otimes> x) \<otimes> y \<in> I"
725     by (simp add: I_r_closed)
726   also from carr have "(a \<otimes> x) \<otimes> y = a \<otimes> (x \<otimes> y)"
727     by (simp add: m_assoc)
728   finally show "a \<otimes> (x \<otimes> y) \<in> I" .
729 qed
731 lemma (in ideal) helper_max_prime:
732   assumes "cring R"
733   assumes acarr: "a \<in> carrier R"
734   shows "ideal {x\<in>carrier R. a \<otimes> x \<in> I} R"
735 proof -
736   interpret cring R by fact
737   show ?thesis apply (rule idealI)
738     apply (rule cring.axioms[OF is_cring])
739     apply (rule subgroup.intro)
740     apply (simp, fast)
741     apply clarsimp apply (simp add: r_distr acarr)
742     apply (simp add: acarr)
743     apply (simp add: a_inv_def[symmetric], clarify) defer 1
744     apply clarsimp defer 1
745     apply (fast intro!: helper_I_closed acarr)
746   proof -
747     fix x
748     assume xcarr: "x \<in> carrier R"
749       and ax: "a \<otimes> x \<in> I"
750     from ax and acarr xcarr
751     have "\<ominus>(a \<otimes> x) \<in> I" by simp
752     also from acarr xcarr
753     have "\<ominus>(a \<otimes> x) = a \<otimes> (\<ominus>x)" by algebra
754     finally show "a \<otimes> (\<ominus>x) \<in> I" .
755     from acarr have "a \<otimes> \<zero> = \<zero>" by simp
756   next
757     fix x y
758     assume xcarr: "x \<in> carrier R"
759       and ycarr: "y \<in> carrier R"
760       and ayI: "a \<otimes> y \<in> I"
761     from ayI and acarr xcarr ycarr have "a \<otimes> (y \<otimes> x) \<in> I"
762       by (simp add: helper_I_closed)
763     moreover
764     from xcarr ycarr have "y \<otimes> x = x \<otimes> y"
765       by (simp add: m_comm)
766     ultimately
767     show "a \<otimes> (x \<otimes> y) \<in> I" by simp
768   qed
769 qed
771 text \<open>In a cring every maximal ideal is prime\<close>
772 lemma (in cring) maximalideal_is_prime:
773   assumes "maximalideal I R"
774   shows "primeideal I R"
775 proof -
776   interpret maximalideal I R by fact
777   show ?thesis apply (rule ccontr)
778     apply (rule primeidealCE)
779     apply (rule is_cring)
780     apply assumption
781     apply (simp add: I_notcarr)
782   proof -
783     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"
784     then obtain a b where
785       acarr: "a \<in> carrier R" and
786       bcarr: "b \<in> carrier R" and
787       abI: "a \<otimes> b \<in> I" and
788       anI: "a \<notin> I" and
789       bnI: "b \<notin> I" by fast
790     def J \<equiv> "{x\<in>carrier R. a \<otimes> x \<in> I}"
792     from is_cring and acarr have idealJ: "ideal J R"
793       unfolding J_def by (rule helper_max_prime)
795     have IsubJ: "I \<subseteq> J"
796     proof
797       fix x
798       assume xI: "x \<in> I"
799       with acarr have "a \<otimes> x \<in> I"
800         by (intro I_l_closed)
801       with xI[THEN a_Hcarr] show "x \<in> J"
802         unfolding J_def by fast
803     qed
805     from abI and acarr bcarr have "b \<in> J"
806       unfolding J_def by fast
807     with bnI have JnI: "J \<noteq> I" by fast
808     from acarr
809     have "a = a \<otimes> \<one>" by algebra
810     with anI have "a \<otimes> \<one> \<notin> I" by simp
811     with one_closed have "\<one> \<notin> J"
812       unfolding J_def by fast
813     then have Jncarr: "J \<noteq> carrier R" by fast
815     interpret ideal J R by (rule idealJ)
817     have "J = I \<or> J = carrier R"
818       apply (intro I_maximal)
819       apply (rule idealJ)
820       apply (rule IsubJ)
821       apply (rule a_subset)
822       done
824     with JnI and Jncarr show False by simp
825   qed
826 qed
829 subsection \<open>Derived Theorems\<close>
831 --"A non-zero cring that has only the two trivial ideals is a field"
832 lemma (in cring) trivialideals_fieldI:
833   assumes carrnzero: "carrier R \<noteq> {\<zero>}"
834     and haveideals: "{I. ideal I R} = {{\<zero>}, carrier R}"
835   shows "field R"
836   apply (rule cring_fieldI)
837   apply (rule, rule, rule)
838    apply (erule Units_closed)
839   defer 1
840     apply rule
841   defer 1
842 proof (rule ccontr, simp)
843   assume zUnit: "\<zero> \<in> Units R"
844   then have a: "\<zero> \<otimes> inv \<zero> = \<one>" by (rule Units_r_inv)
845   from zUnit have "\<zero> \<otimes> inv \<zero> = \<zero>"
846     by (intro l_null) (rule Units_inv_closed)
847   with a[symmetric] have "\<one> = \<zero>" by simp
848   then have "carrier R = {\<zero>}" by (rule one_zeroD)
849   with carrnzero show False by simp
850 next
851   fix x
852   assume xcarr': "x \<in> carrier R - {\<zero>}"
853   then have xcarr: "x \<in> carrier R" by fast
854   from xcarr' have xnZ: "x \<noteq> \<zero>" by fast
855   from xcarr have xIdl: "ideal (PIdl x) R"
856     by (intro cgenideal_ideal) fast
858   from xcarr have "x \<in> PIdl x"
859     by (intro cgenideal_self) fast
860   with xnZ have "PIdl x \<noteq> {\<zero>}" by fast
861   with haveideals have "PIdl x = carrier R"
862     by (blast intro!: xIdl)
863   then have "\<one> \<in> PIdl x" by simp
864   then have "\<exists>y. \<one> = y \<otimes> x \<and> y \<in> carrier R"
865     unfolding cgenideal_def by blast
866   then obtain y where ycarr: " y \<in> carrier R" and ylinv: "\<one> = y \<otimes> x"
867     by fast+
868   from ylinv and xcarr ycarr have yrinv: "\<one> = x \<otimes> y"
869     by (simp add: m_comm)
870   from ycarr and ylinv[symmetric] and yrinv[symmetric]
871   have "\<exists>y \<in> carrier R. y \<otimes> x = \<one> \<and> x \<otimes> y = \<one>" by fast
872   with xcarr show "x \<in> Units R"
873     unfolding Units_def by fast
874 qed
876 lemma (in field) all_ideals: "{I. ideal I R} = {{\<zero>}, carrier R}"
877   apply (rule, rule)
878 proof -
879   fix I
880   assume a: "I \<in> {I. ideal I R}"
881   then interpret ideal I R by simp
883   show "I \<in> {{\<zero>}, carrier R}"
884   proof (cases "\<exists>a. a \<in> I - {\<zero>}")
885     case True
886     then obtain a where aI: "a \<in> I" and anZ: "a \<noteq> \<zero>"
887       by fast+
888     from aI[THEN a_Hcarr] anZ have aUnit: "a \<in> Units R"
889       by (simp add: field_Units)
890     then have a: "a \<otimes> inv a = \<one>" by (rule Units_r_inv)
891     from aI and aUnit have "a \<otimes> inv a \<in> I"
892       by (simp add: I_r_closed del: Units_r_inv)
893     then have oneI: "\<one> \<in> I" by (simp add: a[symmetric])
895     have "carrier R \<subseteq> I"
896     proof
897       fix x
898       assume xcarr: "x \<in> carrier R"
899       with oneI have "\<one> \<otimes> x \<in> I" by (rule I_r_closed)
900       with xcarr show "x \<in> I" by simp
901     qed
902     with a_subset have "I = carrier R" by fast
903     then show "I \<in> {{\<zero>}, carrier R}" by fast
904   next
905     case False
906     then have IZ: "\<And>a. a \<in> I \<Longrightarrow> a = \<zero>" by simp
908     have a: "I \<subseteq> {\<zero>}"
909     proof
910       fix x
911       assume "x \<in> I"
912       then have "x = \<zero>" by (rule IZ)
913       then show "x \<in> {\<zero>}" by fast
914     qed
916     have "\<zero> \<in> I" by simp
917     then have "{\<zero>} \<subseteq> I" by fast
919     with a have "I = {\<zero>}" by fast
920     then show "I \<in> {{\<zero>}, carrier R}" by fast
921   qed
922 qed (simp add: zeroideal oneideal)
924 --"Jacobson Theorem 2.2"
925 lemma (in cring) trivialideals_eq_field:
926   assumes carrnzero: "carrier R \<noteq> {\<zero>}"
927   shows "({I. ideal I R} = {{\<zero>}, carrier R}) = field R"
928   by (fast intro!: trivialideals_fieldI[OF carrnzero] field.all_ideals)
931 text \<open>Like zeroprimeideal for domains\<close>
932 lemma (in field) zeromaximalideal: "maximalideal {\<zero>} R"
933   apply (rule maximalidealI)
934     apply (rule zeroideal)
935 proof-
936   from one_not_zero have "\<one> \<notin> {\<zero>}" by simp
937   with one_closed show "carrier R \<noteq> {\<zero>}" by fast
938 next
939   fix J
940   assume Jideal: "ideal J R"
941   then have "J \<in> {I. ideal I R}" by fast
942   with all_ideals show "J = {\<zero>} \<or> J = carrier R"
943     by simp
944 qed
946 lemma (in cring) zeromaximalideal_fieldI:
947   assumes zeromax: "maximalideal {\<zero>} R"
948   shows "field R"
949   apply (rule trivialideals_fieldI, rule maximalideal.I_notcarr[OF zeromax])
950   apply rule apply clarsimp defer 1
951    apply (simp add: zeroideal oneideal)
952 proof -
953   fix J
954   assume Jn0: "J \<noteq> {\<zero>}"
955     and idealJ: "ideal J R"
956   interpret ideal J R by (rule idealJ)
957   have "{\<zero>} \<subseteq> J" by (rule ccontr) simp
958   from zeromax and idealJ and this and a_subset
959   have "J = {\<zero>} \<or> J = carrier R"
960     by (rule maximalideal.I_maximal)
961   with Jn0 show "J = carrier R"
962     by simp
963 qed
965 lemma (in cring) zeromaximalideal_eq_field: "maximalideal {\<zero>} R = field R"
966   apply rule
967    apply (erule zeromaximalideal_fieldI)
968   apply (erule field.zeromaximalideal)
969   done
971 end