src/HOL/Algebra/Ideal.thy
author paulson <lp15@cam.ac.uk>
Sat Jun 30 15:44:04 2018 +0100 (12 months ago)
changeset 68551 b680e74eb6f2
parent 68464 3ead36cbe6b7
child 68604 57721285d4ef
permissions -rw-r--r--
More on Algebra by Paulo and Martin
     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 proof (intro abelian_subgroupI3 abelian_group.intro)
    21   show "additive_subgroup I R"
    22     by (simp add: is_additive_subgroup)
    23   show "abelian_monoid R"
    24     by (simp add: abelian_monoid_axioms)
    25   show "abelian_group_axioms R"
    26     using abelian_group_def is_abelian_group by blast
    27 qed
    28 
    29 lemma (in ideal) is_ideal: "ideal I R"
    30   by (rule ideal_axioms)
    31 
    32 lemma idealI:
    33   fixes R (structure)
    34   assumes "ring R"
    35   assumes a_subgroup: "subgroup I (add_monoid R)"
    36     and I_l_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
    37     and I_r_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
    38   shows "ideal I R"
    39 proof -
    40   interpret ring R by fact
    41   show ?thesis  
    42     by (auto simp: ideal.intro ideal_axioms.intro additive_subgroupI a_subgroup is_ring I_l_closed I_r_closed)
    43 qed
    44 
    45 
    46 subsubsection (in ring) \<open>Ideals Generated by a Subset of @{term "carrier R"}\<close>
    47 
    48 definition genideal :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set"  ("Idl\<index> _" [80] 79)
    49   where "genideal R S = \<Inter>{I. ideal I R \<and> S \<subseteq> I}"
    50 
    51 subsubsection \<open>Principal Ideals\<close>
    52 
    53 locale principalideal = ideal +
    54   assumes generate: "\<exists>i \<in> carrier R. I = Idl {i}"
    55 
    56 lemma (in principalideal) is_principalideal: "principalideal I R"
    57   by (rule principalideal_axioms)
    58 
    59 lemma principalidealI:
    60   fixes R (structure)
    61   assumes "ideal I R"
    62     and generate: "\<exists>i \<in> carrier R. I = Idl {i}"
    63   shows "principalideal I R"
    64 proof -
    65   interpret ideal I R by fact
    66   show ?thesis
    67     by (intro principalideal.intro principalideal_axioms.intro)
    68       (rule is_ideal, rule generate)
    69 qed
    70 
    71 
    72 subsubsection \<open>Maximal Ideals\<close>
    73 
    74 locale maximalideal = ideal +
    75   assumes I_notcarr: "carrier R \<noteq> I"
    76     and I_maximal: "\<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> (J = I) \<or> (J = carrier R)"
    77 
    78 lemma (in maximalideal) is_maximalideal: "maximalideal I R"
    79   by (rule maximalideal_axioms)
    80 
    81 lemma maximalidealI:
    82   fixes R
    83   assumes "ideal I R"
    84     and I_notcarr: "carrier R \<noteq> I"
    85     and I_maximal: "\<And>J. \<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> (J = I) \<or> (J = carrier R)"
    86   shows "maximalideal I R"
    87 proof -
    88   interpret ideal I R by fact
    89   show ?thesis
    90     by (intro maximalideal.intro maximalideal_axioms.intro)
    91       (rule is_ideal, rule I_notcarr, rule I_maximal)
    92 qed
    93 
    94 
    95 subsubsection \<open>Prime Ideals\<close>
    96 
    97 locale primeideal = ideal + cring +
    98   assumes I_notcarr: "carrier R \<noteq> I"
    99     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"
   100 
   101 lemma (in primeideal) primeideal: "primeideal I R"
   102   by (rule primeideal_axioms)
   103 
   104 lemma primeidealI:
   105   fixes R (structure)
   106   assumes "ideal I R"
   107     and "cring R"
   108     and I_notcarr: "carrier R \<noteq> I"
   109     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"
   110   shows "primeideal I R"
   111 proof -
   112   interpret ideal I R by fact
   113   interpret cring R by fact
   114   show ?thesis
   115     by (intro primeideal.intro primeideal_axioms.intro)
   116       (rule is_ideal, rule is_cring, rule I_notcarr, rule I_prime)
   117 qed
   118 
   119 lemma primeidealI2:
   120   fixes R (structure)
   121   assumes "additive_subgroup I R"
   122     and "cring R"
   123     and I_l_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
   124     and I_r_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
   125     and I_notcarr: "carrier R \<noteq> I"
   126     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"
   127   shows "primeideal I R"
   128 proof -
   129   interpret additive_subgroup I R by fact
   130   interpret cring R by fact
   131   show ?thesis apply intro_locales
   132     apply (intro ideal_axioms.intro)
   133     apply (erule (1) I_l_closed)
   134     apply (erule (1) I_r_closed)
   135     by (simp add: I_notcarr I_prime primeideal_axioms.intro)
   136 qed
   137 
   138 
   139 subsection \<open>Special Ideals\<close>
   140 
   141 lemma (in ring) zeroideal: "ideal {\<zero>} R"
   142   by (intro idealI subgroup.intro) (simp_all add: is_ring)
   143 
   144 lemma (in ring) oneideal: "ideal (carrier R) R"
   145   by (rule idealI) (auto intro: is_ring add.subgroupI)
   146 
   147 lemma (in "domain") zeroprimeideal: "primeideal {\<zero>} R"
   148 proof -
   149   have "carrier R \<noteq> {\<zero>}"
   150     by (simp add: carrier_one_not_zero)
   151   then show ?thesis
   152     by (metis (no_types, lifting) domain_axioms domain_def integral primeidealI singleton_iff zeroideal)
   153 qed
   154 
   155 
   156 subsection \<open>General Ideal Properies\<close>
   157 
   158 lemma (in ideal) one_imp_carrier:
   159   assumes I_one_closed: "\<one> \<in> I"
   160   shows "I = carrier R"
   161 proof
   162   show "carrier R \<subseteq> I"
   163     using I_r_closed assms by fastforce
   164   show "I \<subseteq> carrier R"
   165     by (rule a_subset)
   166 qed
   167 
   168 lemma (in ideal) Icarr:
   169   assumes iI: "i \<in> I"
   170   shows "i \<in> carrier R"
   171   using iI by (rule a_Hcarr)
   172 
   173 
   174 subsection \<open>Intersection of Ideals\<close>
   175 
   176 paragraph \<open>Intersection of two ideals\<close>
   177 text \<open>The intersection of any two ideals is again an ideal in @{term R}\<close>
   178 
   179 lemma (in ring) i_intersect:
   180   assumes "ideal I R"
   181   assumes "ideal J R"
   182   shows "ideal (I \<inter> J) R"
   183 proof -
   184   interpret ideal I R by fact
   185   interpret ideal J R by fact
   186   have IJ: "I \<inter> J \<subseteq> carrier R"
   187     by (force simp: a_subset)
   188   show ?thesis
   189     apply (intro idealI subgroup.intro)
   190     apply (simp_all add: IJ is_ring I_l_closed assms ideal.I_l_closed ideal.I_r_closed flip: a_inv_def)
   191     done
   192 qed
   193 
   194 text \<open>The intersection of any Number of Ideals is again an Ideal in @{term R}\<close>
   195 
   196 lemma (in ring) i_Intersect:
   197   assumes Sideals: "\<And>I. I \<in> S \<Longrightarrow> ideal I R" and notempty: "S \<noteq> {}"
   198   shows "ideal (\<Inter>S) R"
   199 proof -
   200   { fix x y J
   201     assume "\<forall>I\<in>S. x \<in> I" "\<forall>I\<in>S. y \<in> I" and JS: "J \<in> S"
   202     interpret ideal J R by (rule Sideals[OF JS])
   203     have "x \<oplus> y \<in> J"
   204       by (simp add: JS \<open>\<forall>I\<in>S. x \<in> I\<close> \<open>\<forall>I\<in>S. y \<in> I\<close>) }
   205   moreover
   206     have "\<zero> \<in> J" if "J \<in> S" for J
   207       by (simp add: that Sideals additive_subgroup.zero_closed ideal.axioms(1)) 
   208   moreover
   209   { fix x J
   210     assume "\<forall>I\<in>S. x \<in> I" and JS: "J \<in> S"
   211     interpret ideal J R by (rule Sideals[OF JS])
   212     have "\<ominus> x \<in> J"
   213       by (simp add: JS \<open>\<forall>I\<in>S. x \<in> I\<close>) }
   214   moreover
   215   { fix x y J
   216     assume "\<forall>I\<in>S. x \<in> I" and ycarr: "y \<in> carrier R" and JS: "J \<in> S"
   217     interpret ideal J R by (rule Sideals[OF JS])
   218     have "y \<otimes> x \<in> J" "x \<otimes> y \<in> J" 
   219       using I_l_closed I_r_closed JS \<open>\<forall>I\<in>S. x \<in> I\<close> ycarr by blast+ }
   220   moreover
   221   { fix x
   222     assume "\<forall>I\<in>S. x \<in> I"
   223     obtain I0 where I0S: "I0 \<in> S"
   224       using notempty by blast
   225     interpret ideal I0 R by (rule Sideals[OF I0S])
   226     have "x \<in> I0"
   227       by (simp add: I0S \<open>\<forall>I\<in>S. x \<in> I\<close>) 
   228     with a_subset have "x \<in> carrier R" by fast }
   229   ultimately show ?thesis
   230     by unfold_locales (auto simp: Inter_eq simp flip: a_inv_def)
   231 qed
   232 
   233 
   234 subsection \<open>Addition of Ideals\<close>
   235 
   236 lemma (in ring) add_ideals:
   237   assumes idealI: "ideal I R" and idealJ: "ideal J R"
   238   shows "ideal (I <+> J) R"
   239 proof (rule ideal.intro)
   240   show "additive_subgroup (I <+> J) R"
   241     by (intro ideal.axioms[OF idealI] ideal.axioms[OF idealJ] add_additive_subgroups)
   242   show "ring R"
   243     by (rule is_ring)
   244   show "ideal_axioms (I <+> J) R"
   245   proof -
   246     { fix x i j
   247       assume xcarr: "x \<in> carrier R" and iI: "i \<in> I" and jJ: "j \<in> J"
   248       from xcarr ideal.Icarr[OF idealI iI] ideal.Icarr[OF idealJ jJ]
   249       have "\<exists>h\<in>I. \<exists>k\<in>J. (i \<oplus> j) \<otimes> x = h \<oplus> k"
   250         by (meson iI ideal.I_r_closed idealJ jJ l_distr local.idealI) }
   251     moreover
   252     { fix x i j
   253       assume xcarr: "x \<in> carrier R" and iI: "i \<in> I" and jJ: "j \<in> J"
   254       from xcarr ideal.Icarr[OF idealI iI] ideal.Icarr[OF idealJ jJ]
   255       have "\<exists>h\<in>I. \<exists>k\<in>J. x \<otimes> (i \<oplus> j) = h \<oplus> k"
   256         by (meson iI ideal.I_l_closed idealJ jJ local.idealI r_distr) }
   257     ultimately show "ideal_axioms (I <+> J) R"
   258       by (intro ideal_axioms.intro) (auto simp: set_add_defs)
   259   qed
   260 qed
   261 
   262 subsection (in ring) \<open>Ideals generated by a subset of @{term "carrier R"}\<close>
   263 
   264 text \<open>@{term genideal} generates an ideal\<close>
   265 lemma (in ring) genideal_ideal:
   266   assumes Scarr: "S \<subseteq> carrier R"
   267   shows "ideal (Idl S) R"
   268 unfolding genideal_def
   269 proof (rule i_Intersect, fast, simp)
   270   from oneideal and Scarr
   271   show "\<exists>I. ideal I R \<and> S \<le> I" by fast
   272 qed
   273 
   274 lemma (in ring) genideal_self:
   275   assumes "S \<subseteq> carrier R"
   276   shows "S \<subseteq> Idl S"
   277   unfolding genideal_def by fast
   278 
   279 lemma (in ring) genideal_self':
   280   assumes carr: "i \<in> carrier R"
   281   shows "i \<in> Idl {i}"
   282   by (simp add: genideal_def)
   283 
   284 text \<open>@{term genideal} generates the minimal ideal\<close>
   285 lemma (in ring) genideal_minimal:
   286   assumes "ideal I R" "S \<subseteq> I"
   287   shows "Idl S \<subseteq> I"
   288   unfolding genideal_def by rule (elim InterD, simp add: assms)
   289 
   290 text \<open>Generated ideals and subsets\<close>
   291 lemma (in ring) Idl_subset_ideal:
   292   assumes Iideal: "ideal I R"
   293     and Hcarr: "H \<subseteq> carrier R"
   294   shows "(Idl H \<subseteq> I) = (H \<subseteq> I)"
   295 proof
   296   assume a: "Idl H \<subseteq> I"
   297   from Hcarr have "H \<subseteq> Idl H" by (rule genideal_self)
   298   with a show "H \<subseteq> I" by simp
   299 next
   300   fix x
   301   assume "H \<subseteq> I"
   302   with Iideal have "I \<in> {I. ideal I R \<and> H \<subseteq> I}" by fast
   303   then show "Idl H \<subseteq> I" unfolding genideal_def by fast
   304 qed
   305 
   306 lemma (in ring) subset_Idl_subset:
   307   assumes Icarr: "I \<subseteq> carrier R"
   308     and HI: "H \<subseteq> I"
   309   shows "Idl H \<subseteq> Idl I"
   310 proof -
   311   from Icarr have Iideal: "ideal (Idl I) R"
   312     by (rule genideal_ideal)
   313   from HI and Icarr have "H \<subseteq> carrier R"
   314     by fast
   315   with Iideal have "(H \<subseteq> Idl I) = (Idl H \<subseteq> Idl I)"
   316     by (rule Idl_subset_ideal[symmetric])
   317   then show "Idl H \<subseteq> Idl I"
   318     by (meson HI Icarr genideal_self order_trans)
   319 qed
   320 
   321 lemma (in ring) Idl_subset_ideal':
   322   assumes acarr: "a \<in> carrier R" and bcarr: "b \<in> carrier R"
   323   shows "Idl {a} \<subseteq> Idl {b} \<longleftrightarrow> a \<in> Idl {b}"
   324 proof -
   325   have "Idl {a} \<subseteq> Idl {b} \<longleftrightarrow> {a} \<subseteq> Idl {b}"
   326     by (simp add: Idl_subset_ideal acarr bcarr genideal_ideal)
   327   also have "\<dots> \<longleftrightarrow> a \<in> Idl {b}"
   328     by blast
   329   finally show ?thesis .
   330 qed
   331 
   332 lemma (in ring) genideal_zero: "Idl {\<zero>} = {\<zero>}"
   333 proof
   334   show "Idl {\<zero>} \<subseteq> {\<zero>}"
   335     by (simp add: genideal_minimal zeroideal)
   336   show "{\<zero>} \<subseteq> Idl {\<zero>}"
   337     by (simp add: genideal_self')
   338 qed
   339 
   340 lemma (in ring) genideal_one: "Idl {\<one>} = carrier R"
   341 proof -
   342   interpret ideal "Idl {\<one>}" "R" by (rule genideal_ideal) fast
   343   show "Idl {\<one>} = carrier R"
   344     using genideal_self' one_imp_carrier by blast
   345 qed
   346 
   347 
   348 text \<open>Generation of Principal Ideals in Commutative Rings\<close>
   349 
   350 definition cgenideal :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set"  ("PIdl\<index> _" [80] 79)
   351   where "cgenideal R a = {x \<otimes>\<^bsub>R\<^esub> a | x. x \<in> carrier R}"
   352 
   353 text \<open>genhideal (?) really generates an ideal\<close>
   354 lemma (in cring) cgenideal_ideal:
   355   assumes acarr: "a \<in> carrier R"
   356   shows "ideal (PIdl a) R"
   357   unfolding cgenideal_def
   358 proof (intro subgroup.intro idealI[OF is_ring], simp_all)
   359   show "{x \<otimes> a |x. x \<in> carrier R} \<subseteq> carrier R"
   360     by (blast intro: acarr)
   361   show "\<And>x y. \<lbrakk>\<exists>u. x = u \<otimes> a \<and> u \<in> carrier R; \<exists>x. y = x \<otimes> a \<and> x \<in> carrier R\<rbrakk>
   362               \<Longrightarrow> \<exists>v. x \<oplus> y = v \<otimes> a \<and> v \<in> carrier R"
   363     by (metis assms cring.cring_simprules(1) is_cring l_distr)
   364   show "\<exists>x. \<zero> = x \<otimes> a \<and> x \<in> carrier R"
   365     by (metis assms l_null zero_closed)
   366   show "\<And>x. \<exists>u. x = u \<otimes> a \<and> u \<in> carrier R 
   367             \<Longrightarrow> \<exists>v. inv\<^bsub>add_monoid R\<^esub> x = v \<otimes> a \<and> v \<in> carrier R"
   368     by (metis a_inv_def add.inv_closed assms l_minus)
   369   show "\<And>b x. \<lbrakk>\<exists>x. b = x \<otimes> a \<and> x \<in> carrier R; x \<in> carrier R\<rbrakk>
   370        \<Longrightarrow> \<exists>z. x \<otimes> b = z \<otimes> a \<and> z \<in> carrier R"
   371     by (metis assms m_assoc m_closed)
   372   show "\<And>b x. \<lbrakk>\<exists>x. b = x \<otimes> a \<and> x \<in> carrier R; x \<in> carrier R\<rbrakk>
   373        \<Longrightarrow> \<exists>z. b \<otimes> x = z \<otimes> a \<and> z \<in> carrier R"
   374     by (metis assms m_assoc m_comm m_closed)
   375 qed
   376 
   377 lemma (in ring) cgenideal_self:
   378   assumes icarr: "i \<in> carrier R"
   379   shows "i \<in> PIdl i"
   380   unfolding cgenideal_def
   381 proof simp
   382   from icarr have "i = \<one> \<otimes> i"
   383     by simp
   384   with icarr show "\<exists>x. i = x \<otimes> i \<and> x \<in> carrier R"
   385     by fast
   386 qed
   387 
   388 text \<open>@{const "cgenideal"} is minimal\<close>
   389 
   390 lemma (in ring) cgenideal_minimal:
   391   assumes "ideal J R"
   392   assumes aJ: "a \<in> J"
   393   shows "PIdl a \<subseteq> J"
   394 proof -
   395   interpret ideal J R by fact
   396   show ?thesis
   397     unfolding cgenideal_def
   398     using I_l_closed aJ by blast
   399 qed
   400 
   401 lemma (in cring) cgenideal_eq_genideal:
   402   assumes icarr: "i \<in> carrier R"
   403   shows "PIdl i = Idl {i}"
   404 proof
   405   show "PIdl i \<subseteq> Idl {i}"
   406     by (simp add: cgenideal_minimal genideal_ideal genideal_self' icarr)
   407   show "Idl {i} \<subseteq> PIdl i"
   408     by (simp add: cgenideal_ideal cgenideal_self genideal_minimal icarr)
   409 qed
   410 
   411 lemma (in cring) cgenideal_eq_rcos: "PIdl i = carrier R #> i"
   412   unfolding cgenideal_def r_coset_def by fast
   413 
   414 lemma (in cring) cgenideal_is_principalideal:
   415   assumes "i \<in> carrier R"
   416   shows "principalideal (PIdl i) R"
   417 proof -
   418   have "\<exists>i'\<in>carrier R. PIdl i = Idl {i'}"
   419     using cgenideal_eq_genideal assms by auto
   420   then show ?thesis
   421     by (simp add: cgenideal_ideal assms principalidealI)
   422 qed
   423 
   424 
   425 subsection \<open>Union of Ideals\<close>
   426 
   427 lemma (in ring) union_genideal:
   428   assumes idealI: "ideal I R" and idealJ: "ideal J R"
   429   shows "Idl (I \<union> J) = I <+> J"
   430 proof
   431   show "Idl (I \<union> J) \<subseteq> I <+> J"
   432   proof (rule ring.genideal_minimal [OF is_ring])
   433     show "ideal (I <+> J) R"
   434       by (rule add_ideals[OF idealI idealJ])
   435     have "\<And>x. x \<in> I \<Longrightarrow> \<exists>xa\<in>I. \<exists>xb\<in>J. x = xa \<oplus> xb"
   436       by (metis additive_subgroup.zero_closed ideal.Icarr idealJ ideal_def local.idealI r_zero)
   437     moreover have "\<And>x. x \<in> J \<Longrightarrow> \<exists>xa\<in>I. \<exists>xb\<in>J. x = xa \<oplus> xb"
   438       by (metis additive_subgroup.zero_closed ideal.Icarr idealJ ideal_def l_zero local.idealI)
   439     ultimately show "I \<union> J \<subseteq> I <+> J"
   440       by (auto simp: set_add_defs) 
   441   qed
   442 next
   443   show "I <+> J \<subseteq> Idl (I \<union> J)"
   444     by (auto simp: set_add_defs genideal_def additive_subgroup.a_closed ideal_def set_mp)
   445 qed
   446 
   447 subsection \<open>Properties of Principal Ideals\<close>
   448 
   449 text \<open>The zero ideal is a principal ideal\<close>
   450 corollary (in ring) zeropideal: "principalideal {\<zero>} R"
   451   using genideal_zero principalidealI zeroideal by blast
   452 
   453 text \<open>The unit ideal is a principal ideal\<close>
   454 corollary (in ring) onepideal: "principalideal (carrier R) R"
   455   using genideal_one oneideal principalidealI by blast
   456 
   457 text \<open>Every principal ideal is a right coset of the carrier\<close>
   458 lemma (in principalideal) rcos_generate:
   459   assumes "cring R"
   460   shows "\<exists>x\<in>I. I = carrier R #> x"
   461 proof -
   462   interpret cring R by fact
   463   from generate obtain i where icarr: "i \<in> carrier R" and I1: "I = Idl {i}"
   464     by fast+
   465   then have "I = PIdl i"
   466     by (simp add: cgenideal_eq_genideal)
   467   moreover have "i \<in> I"
   468     by (simp add: I1 genideal_self' icarr)
   469   moreover have "PIdl i = carrier R #> i"
   470     unfolding cgenideal_def r_coset_def by fast
   471   ultimately show "\<exists>x\<in>I. I = carrier R #> x"
   472     by fast
   473 qed
   474 
   475 
   476 (* Next lemma contributed by Paulo Emílio de Vilhena. *)
   477 
   478 text \<open>This next lemma would be trivial if placed in a theory that imports QuotRing,
   479       but it makes more sense to have it here (easier to find and coherent with the
   480       previous developments).\<close>
   481 
   482 lemma (in cring) cgenideal_prod:
   483   assumes "a \<in> carrier R" "b \<in> carrier R"
   484   shows "(PIdl a) <#> (PIdl b) = PIdl (a \<otimes> b)"
   485 proof -
   486   have "(carrier R #> a) <#> (carrier R #> b) = carrier R #> (a \<otimes> b)"
   487   proof
   488     show "(carrier R #> a) <#> (carrier R #> b) \<subseteq> carrier R #> a \<otimes> b"
   489     proof
   490       fix x assume "x \<in> (carrier R #> a) <#> (carrier R #> b)"
   491       then obtain r1 r2 where r1: "r1 \<in> carrier R" and r2: "r2 \<in> carrier R"
   492                           and "x = (r1 \<otimes> a) \<otimes> (r2 \<otimes> b)"
   493         unfolding set_mult_def r_coset_def by blast
   494       hence "x = (r1 \<otimes> r2) \<otimes> (a \<otimes> b)"
   495         by (simp add: assms local.ring_axioms m_lcomm ring.ring_simprules(11))
   496       thus "x \<in> carrier R #> a \<otimes> b"
   497         unfolding r_coset_def using r1 r2 assms by blast 
   498     qed
   499   next
   500     show "carrier R #> a \<otimes> b \<subseteq> (carrier R #> a) <#> (carrier R #> b)"
   501     proof
   502       fix x assume "x \<in> carrier R #> a \<otimes> b"
   503       then obtain r where r: "r \<in> carrier R" "x = r \<otimes> (a \<otimes> b)"
   504         unfolding r_coset_def by blast
   505       hence "x = (r \<otimes> a) \<otimes> (\<one> \<otimes> b)"
   506         using assms by (simp add: m_assoc)
   507       thus "x \<in> (carrier R #> a) <#> (carrier R #> b)"
   508         unfolding set_mult_def r_coset_def using assms r by blast
   509     qed
   510   qed
   511   thus ?thesis
   512     using cgenideal_eq_rcos[of a] cgenideal_eq_rcos[of b] cgenideal_eq_rcos[of "a \<otimes> b"] by simp
   513 qed
   514 
   515 
   516 subsection \<open>Prime Ideals\<close>
   517 
   518 lemma (in ideal) primeidealCD:
   519   assumes "cring R"
   520   assumes notprime: "\<not> primeideal I R"
   521   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)"
   522 proof (rule ccontr, clarsimp)
   523   interpret cring R by fact
   524   assume InR: "carrier R \<noteq> I"
   525     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)"
   526   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"
   527     by simp
   528   have "primeideal I R"
   529     by (simp add: I_prime InR is_cring is_ideal primeidealI)
   530   with notprime show False by simp
   531 qed
   532 
   533 lemma (in ideal) primeidealCE:
   534   assumes "cring R"
   535   assumes notprime: "\<not> primeideal I R"
   536   obtains "carrier R = I"
   537     | "\<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"
   538 proof -
   539   interpret R: cring R by fact
   540   assume "carrier R = I ==> thesis"
   541     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"
   542   then show thesis using primeidealCD [OF R.is_cring notprime] by blast
   543 qed
   544 
   545 text \<open>If \<open>{\<zero>}\<close> is a prime ideal of a commutative ring, the ring is a domain\<close>
   546 lemma (in cring) zeroprimeideal_domainI:
   547   assumes pi: "primeideal {\<zero>} R"
   548   shows "domain R"
   549 proof (intro domain.intro is_cring domain_axioms.intro)
   550   show "\<one> \<noteq> \<zero>"
   551     using genideal_one genideal_zero pi primeideal.I_notcarr by force
   552   show "a = \<zero> \<or> b = \<zero>" if ab: "a \<otimes> b = \<zero>" and carr: "a \<in> carrier R" "b \<in> carrier R" for a b
   553   proof -
   554     interpret primeideal "{\<zero>}" "R" by (rule pi)
   555     show "a = \<zero> \<or> b = \<zero>"
   556       using I_prime ab carr by blast
   557   qed
   558 qed
   559 
   560 corollary (in cring) domain_eq_zeroprimeideal: "domain R = primeideal {\<zero>} R"
   561   using domain.zeroprimeideal zeroprimeideal_domainI by blast
   562 
   563 
   564 subsection \<open>Maximal Ideals\<close>
   565 
   566 lemma (in ideal) helper_I_closed:
   567   assumes carr: "a \<in> carrier R" "x \<in> carrier R" "y \<in> carrier R"
   568     and axI: "a \<otimes> x \<in> I"
   569   shows "a \<otimes> (x \<otimes> y) \<in> I"
   570 proof -
   571   from axI and carr have "(a \<otimes> x) \<otimes> y \<in> I"
   572     by (simp add: I_r_closed)
   573   also from carr have "(a \<otimes> x) \<otimes> y = a \<otimes> (x \<otimes> y)"
   574     by (simp add: m_assoc)
   575   finally show "a \<otimes> (x \<otimes> y) \<in> I" .
   576 qed
   577 
   578 lemma (in ideal) helper_max_prime:
   579   assumes "cring R"
   580   assumes acarr: "a \<in> carrier R"
   581   shows "ideal {x\<in>carrier R. a \<otimes> x \<in> I} R"
   582 proof -
   583   interpret cring R by fact
   584   show ?thesis 
   585   proof (rule idealI, simp_all)
   586     show "ring R"
   587       by (simp add: local.ring_axioms)
   588     show "subgroup {x \<in> carrier R. a \<otimes> x \<in> I} (add_monoid R)"
   589       by (rule subgroup.intro) (auto simp: r_distr acarr r_minus simp flip: a_inv_def)
   590     show "\<And>b x. \<lbrakk>b \<in> carrier R \<and> a \<otimes> b \<in> I; x \<in> carrier R\<rbrakk>
   591                  \<Longrightarrow> a \<otimes> (x \<otimes> b) \<in> I"
   592       using acarr helper_I_closed m_comm by auto
   593     show "\<And>b x. \<lbrakk>b \<in> carrier R \<and> a \<otimes> b \<in> I; x \<in> carrier R\<rbrakk>
   594                 \<Longrightarrow> a \<otimes> (b \<otimes> x) \<in> I"
   595       by (simp add: acarr helper_I_closed)
   596   qed
   597 qed
   598 
   599 text \<open>In a cring every maximal ideal is prime\<close>
   600 lemma (in cring) maximalideal_prime:
   601   assumes "maximalideal I R"
   602   shows "primeideal I R"
   603 proof -
   604   interpret maximalideal I R by fact
   605   show ?thesis 
   606   proof (rule ccontr)
   607     assume neg: "\<not> primeideal I R"
   608     then obtain a b where acarr: "a \<in> carrier R" and bcarr: "b \<in> carrier R"
   609       and abI: "a \<otimes> b \<in> I" and anI: "a \<notin> I" and bnI: "b \<notin> I" 
   610       using primeidealCE [OF is_cring]
   611       by (metis I_notcarr)
   612     define J where "J = {x\<in>carrier R. a \<otimes> x \<in> I}"
   613     from is_cring and acarr have idealJ: "ideal J R"
   614       unfolding J_def by (rule helper_max_prime)
   615     have IsubJ: "I \<subseteq> J"
   616       using I_l_closed J_def a_Hcarr acarr by blast
   617     from abI and acarr bcarr have "b \<in> J"
   618       unfolding J_def by fast
   619     with bnI have JnI: "J \<noteq> I" by fast
   620     have "\<one> \<notin> J"
   621       unfolding J_def by (simp add: acarr anI)
   622     then have Jncarr: "J \<noteq> carrier R" by fast
   623     interpret ideal J R by (rule idealJ)    
   624     have "J = I \<or> J = carrier R"
   625       by (simp add: I_maximal IsubJ a_subset is_ideal)
   626     with JnI and Jncarr show False by simp
   627   qed
   628 qed
   629 
   630 
   631 subsection \<open>Derived Theorems\<close>
   632 
   633 text \<open>A non-zero cring that has only the two trivial ideals is a field\<close>
   634 lemma (in cring) trivialideals_fieldI:
   635   assumes carrnzero: "carrier R \<noteq> {\<zero>}"
   636     and haveideals: "{I. ideal I R} = {{\<zero>}, carrier R}"
   637   shows "field R"
   638 proof (intro cring_fieldI equalityI)
   639   show "Units R \<subseteq> carrier R - {\<zero>}"
   640     by (metis Diff_empty Units_closed Units_r_inv_ex carrnzero l_null one_zeroD subsetI subset_Diff_insert)
   641   show "carrier R - {\<zero>} \<subseteq> Units R"
   642   proof
   643     fix x
   644     assume xcarr': "x \<in> carrier R - {\<zero>}"
   645     then have xcarr: "x \<in> carrier R" and xnZ: "x \<noteq> \<zero>" by auto
   646     from xcarr have xIdl: "ideal (PIdl x) R"
   647       by (intro cgenideal_ideal) fast
   648     have "PIdl x \<noteq> {\<zero>}"
   649       using xcarr xnZ cgenideal_self by blast 
   650     with haveideals have "PIdl x = carrier R"
   651       by (blast intro!: xIdl)
   652     then have "\<one> \<in> PIdl x" by simp
   653     then have "\<exists>y. \<one> = y \<otimes> x \<and> y \<in> carrier R"
   654       unfolding cgenideal_def by blast
   655     then obtain y where ycarr: " y \<in> carrier R" and ylinv: "\<one> = y \<otimes> x"
   656       by fast    
   657     have "\<exists>y \<in> carrier R. y \<otimes> x = \<one> \<and> x \<otimes> y = \<one>"
   658       using m_comm xcarr ycarr ylinv by auto
   659     with xcarr show "x \<in> Units R"
   660       unfolding Units_def by fast
   661   qed
   662 qed
   663 
   664 lemma (in field) all_ideals: "{I. ideal I R} = {{\<zero>}, carrier R}"
   665 proof (intro equalityI subsetI)
   666   fix I
   667   assume a: "I \<in> {I. ideal I R}"
   668   then interpret ideal I R by simp
   669 
   670   show "I \<in> {{\<zero>}, carrier R}"
   671   proof (cases "\<exists>a. a \<in> I - {\<zero>}")
   672     case True
   673     then obtain a where aI: "a \<in> I" and anZ: "a \<noteq> \<zero>"
   674       by fast+
   675     have aUnit: "a \<in> Units R"
   676       by (simp add: aI anZ field_Units)
   677     then have a: "a \<otimes> inv a = \<one>" by (rule Units_r_inv)
   678     from aI and aUnit have "a \<otimes> inv a \<in> I"
   679       by (simp add: I_r_closed del: Units_r_inv)
   680     then have oneI: "\<one> \<in> I" by (simp add: a[symmetric])
   681     have "carrier R \<subseteq> I"
   682       using oneI one_imp_carrier by auto
   683     with a_subset have "I = carrier R" by fast
   684     then show "I \<in> {{\<zero>}, carrier R}" by fast
   685   next
   686     case False
   687     then have IZ: "\<And>a. a \<in> I \<Longrightarrow> a = \<zero>" by simp
   688     have a: "I \<subseteq> {\<zero>}"
   689       using False by auto
   690     have "\<zero> \<in> I" by simp
   691     with a have "I = {\<zero>}" by fast
   692     then show "I \<in> {{\<zero>}, carrier R}" by fast
   693   qed
   694 qed (auto simp: zeroideal oneideal)
   695 
   696 \<comment>\<open>"Jacobson Theorem 2.2"\<close>
   697 lemma (in cring) trivialideals_eq_field:
   698   assumes carrnzero: "carrier R \<noteq> {\<zero>}"
   699   shows "({I. ideal I R} = {{\<zero>}, carrier R}) = field R"
   700   by (fast intro!: trivialideals_fieldI[OF carrnzero] field.all_ideals)
   701 
   702 
   703 text \<open>Like zeroprimeideal for domains\<close>
   704 lemma (in field) zeromaximalideal: "maximalideal {\<zero>} R"
   705 proof (intro maximalidealI zeroideal)
   706   from one_not_zero have "\<one> \<notin> {\<zero>}" by simp
   707   with one_closed show "carrier R \<noteq> {\<zero>}" by fast
   708 next
   709   fix J
   710   assume Jideal: "ideal J R"
   711   then have "J \<in> {I. ideal I R}" by fast
   712   with all_ideals show "J = {\<zero>} \<or> J = carrier R"
   713     by simp
   714 qed
   715 
   716 lemma (in cring) zeromaximalideal_fieldI:
   717   assumes zeromax: "maximalideal {\<zero>} R"
   718   shows "field R"
   719 proof (intro trivialideals_fieldI maximalideal.I_notcarr[OF zeromax])
   720   have "J = carrier R" if Jn0: "J \<noteq> {\<zero>}" and idealJ: "ideal J R" for J
   721   proof -
   722     interpret ideal J R by (rule idealJ)
   723     have "{\<zero>} \<subseteq> J"
   724       by force
   725     from zeromax idealJ this a_subset
   726     have "J = {\<zero>} \<or> J = carrier R"
   727       by (rule maximalideal.I_maximal)
   728     with Jn0 show "J = carrier R"
   729       by simp
   730   qed
   731   then show "{I. ideal I R} = {{\<zero>}, carrier R}"
   732     by (auto simp: zeroideal oneideal)
   733 qed
   734 
   735 lemma (in cring) zeromaximalideal_eq_field: "maximalideal {\<zero>} R = field R"
   736   using field.zeromaximalideal zeromaximalideal_fieldI by blast
   737 
   738 end