src/HOL/Algebra/Ideal.thy
author wenzelm
Mon Mar 16 18:24:30 2009 +0100 (2009-03-16)
changeset 30549 d2d7874648bd
parent 30363 9b8d9b6ef803
child 30729 461ee3e49ad3
permissions -rw-r--r--
simplified method setup;
     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 constdefs (structure R)
    51   genideal :: "('a, 'b) ring_scheme \<Rightarrow> 'a set \<Rightarrow> 'a set"  ("Idl\<index> _" [80] 79)
    52   "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 constdefs (structure R)
   455   cgenideal :: "('a, 'b) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a set"  ("PIdl\<index> _" [80] 79)
   456   "cgenideal R a \<equiv> { x \<otimes> 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