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