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