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