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