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