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