src/HOL/Algebra/Ideal.thy
 author wenzelm Sun Mar 21 15:57:40 2010 +0100 (2010-03-21) changeset 35847 19f1f7066917 parent 30729 461ee3e49ad3 child 35848 5443079512ea permissions -rw-r--r--
eliminated old constdefs;
```     1 (*
```
```     2   Title:     HOL/Algebra/CIdeal.thy
```
```     3   Author:    Stephan Hohe, TU Muenchen
```
```     4 *)
```
```     5
```
```     6 theory Ideal
```
```     7 imports Ring AbelCoset
```
```     8 begin
```
```     9
```
```    10 section {* Ideals *}
```
```    11
```
```    12 subsection {* Definitions *}
```
```    13
```
```    14 subsubsection {* General definition *}
```
```    15
```
```    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"
```
```    19
```
```    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
```
```    26
```
```    27 lemma (in ideal) is_ideal:
```
```    28   "ideal I R"
```
```    29 by (rule ideal_axioms)
```
```    30
```
```    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
```
```    47
```
```    48 subsubsection (in ring) {* Ideals Generated by a Subset of @{term "carrier R"} *}
```
```    49
```
```    50 definition
```
```    51   genideal :: "('a, 'b) ring_scheme \<Rightarrow> 'a set \<Rightarrow> 'a set"  ("Idl\<index> _"  79)
```
```    52   where "genideal R S \<equiv> Inter {I. ideal I R \<and> S \<subseteq> I}"
```
```    53
```
```    54
```
```    55 subsubsection {* Principal Ideals *}
```
```    56
```
```    57 locale principalideal = ideal +
```
```    58   assumes generate: "\<exists>i \<in> carrier R. I = Idl {i}"
```
```    59
```
```    60 lemma (in principalideal) is_principalideal:
```
```    61   shows "principalideal I R"
```
```    62 by (rule principalideal_axioms)
```
```    63
```
```    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
```
```    73
```
```    74 subsubsection {* Maximal Ideals *}
```
```    75
```
```    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"
```
```    79
```
```    80 lemma (in maximalideal) is_maximalideal:
```
```    81  shows "maximalideal I R"
```
```    82 by (rule maximalideal_axioms)
```
```    83
```
```    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
```
```    95
```
```    96 subsubsection {* Prime Ideals *}
```
```    97
```
```    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"
```
```   101
```
```   102 lemma (in primeideal) is_primeideal:
```
```   103  shows "primeideal I R"
```
```   104 by (rule primeideal_axioms)
```
```   105
```
```   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
```
```   119
```
```   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
```
```   141
```
```   142 subsection {* Special Ideals *}
```
```   143
```
```   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
```
```   152
```
```   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
```
```   161
```
```   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
```
```   175
```
```   176
```
```   177 subsection {* General Ideal Properies *}
```
```   178
```
```   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
```
```   193
```
```   194 lemma (in ideal) Icarr:
```
```   195   assumes iI: "i \<in> I"
```
```   196   shows "i \<in> carrier R"
```
```   197 using iI by (rule a_Hcarr)
```
```   198
```
```   199
```
```   200 subsection {* Intersection of Ideals *}
```
```   201
```
```   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
```
```   224
```
```   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
```
```   243
```
```   244   from notempty have "\<exists>I0. I0 \<in> S" by blast
```
```   245   from this obtain I0 where I0S: "I0 \<in> S" by auto
```
```   246
```
```   247   interpret ideal I0 R by (rule Sideals[OF I0S])
```
```   248
```
```   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
```
```   257
```
```   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
```
```   272
```
```   273   fix J
```
```   274   assume JS: "J \<in> S"
```
```   275   interpret ideal J R by (rule Sideals[OF JS])
```
```   276
```
```   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"
```
```   284
```
```   285   fix J
```
```   286   assume JS: "J \<in> S"
```
```   287   interpret ideal J R by (rule Sideals[OF JS])
```
```   288
```
```   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"
```
```   296
```
```   297   fix J
```
```   298   assume JS: "J \<in> S"
```
```   299   interpret ideal J R by (rule Sideals[OF JS])
```
```   300
```
```   301   from xI[OF JS] and ycarr
```
```   302       show "x \<otimes> y \<in> J" by (rule I_r_closed)
```
```   303 qed
```
```   304
```
```   305
```
```   306 subsection {* Addition of Ideals *}
```
```   307
```
```   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)
```
```   313   apply (rule add_additive_subgroups)
```
```   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
```
```   347
```
```   348
```
```   349 subsection (in ring) {* Ideals generated by a subset of @{term "carrier R"} *}
```
```   350
```
```   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
```
```   360
```
```   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
```
```   366
```
```   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
```
```   375
```
```   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)
```
```   383
```
```   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"
```
```   397
```
```   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
```
```   405
```
```   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
```
```   413
```
```   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])
```
```   421
```
```   422   from HIdlI and this
```
```   423       show "Idl H \<subseteq> Idl I" by simp
```
```   424 qed
```
```   425
```
```   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
```
```   433
```
```   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
```
```   440
```
```   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
```
```   450
```
```   451
```
```   452 text {* Generation of Principal Ideals in Commutative Rings *}
```
```   453
```
```   454 definition
```
```   455   cgenideal :: "('a, 'b) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a set"  ("PIdl\<index> _"  79)
```
```   456   where "cgenideal R a \<equiv> {x \<otimes>\<^bsub>R\<^esub> a | x. x \<in> carrier R}"
```
```   457
```
```   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
```
```   477
```
```   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
```
```   489
```
```   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
```
```   499
```
```   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
```
```   509
```
```   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
```
```   515
```
```   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
```
```   526
```
```   527 text {* @{const "cgenideal"} is minimal *}
```
```   528
```
```   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
```
```   542
```
```   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
```
```   554
```
```   555 lemma (in cring) cgenideal_eq_rcos:
```
```   556  "PIdl i = carrier R #> i"
```
```   557 unfolding cgenideal_def r_coset_def
```
```   558 by fast
```
```   559
```
```   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
```
```   571
```
```   572
```
```   573 subsection {* Union of Ideals *}
```
```   574
```
```   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
```
```   618
```
```   619
```
```   620 subsection {* Properties of Principal Ideals *}
```
```   621
```
```   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
```
```   629
```
```   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
```
```   637
```
```   638
```
```   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
```
```   646
```
```   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
```
```   654
```
```   655
```
```   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+
```
```   667
```
```   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)
```
```   671
```
```   672   from I1 icarr
```
```   673       have I2: "I = PIdl i" by (simp add: cgenideal_eq_genideal)
```
```   674
```
```   675   have "PIdl i = carrier R #> i"
```
```   676       unfolding cgenideal_def r_coset_def
```
```   677       by fast
```
```   678
```
```   679   from I2 and this
```
```   680       have "I = carrier R #> i" by simp
```
```   681
```
```   682   from iI and this
```
```   683       show "\<exists>x\<in>I. I = carrier R #> x" by fast
```
```   684 qed
```
```   685
```
```   686
```
```   687 subsection {* Prime Ideals *}
```
```   688
```
```   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
```
```   707
```
```   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
```
```   719
```
```   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
```
```   743
```
```   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
```
```   750
```
```   751
```
```   752 subsection {* Maximal Ideals *}
```
```   753
```
```   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
```
```   766
```
```   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
```
```   807
```
```   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}"
```
```   830
```
```   831     from is_cring and acarr
```
```   832     have idealJ: "ideal J R" unfolding J_def by (rule helper_max_prime)
```
```   833
```
```   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
```
```   843
```
```   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
```
```   855
```
```   856     interpret ideal J R by (rule idealJ)
```
```   857
```
```   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
```
```   864
```
```   865     from this and JnI and Jncarr
```
```   866     show "False" by simp
```
```   867   qed
```
```   868 qed
```
```   869
```
```   870 subsection {* Derived Theorems *}
```
```   871
```
```   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)
```
```   901
```
```   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
```
```   925
```
```   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
```
```   934
```
```   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])
```
```   949
```
```   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
```
```   965
```
```   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
```
```   973
```
```   974     have "\<zero> \<in> I" by simp
```
```   975     hence "{\<zero>} \<subseteq> I" by fast
```
```   976
```
```   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)
```
```   982
```
```   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)
```
```   988
```
```   989
```
```   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
```
```  1005
```
```  1006   from this and all_ideals
```
```  1007       show "J = {\<zero>} \<or> J = carrier R" by simp
```
```  1008 qed
```
```  1009
```
```  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
```
```  1027
```
```  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
```
```  1034
```
```  1035 end
```