summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Algebra/Ideal.thy

author | wenzelm |

Mon Apr 09 21:29:47 2012 +0200 (2012-04-09) | |

changeset 47409 | c5be1120980d |

parent 44677 | 3fb27b19e058 |

child 61382 | efac889fccbc |

permissions | -rw-r--r-- |

tuned proofs;

1 (* Title: HOL/Algebra/Ideal.thy

2 Author: Stephan Hohe, TU Muenchen

3 *)

5 theory Ideal

6 imports Ring AbelCoset

7 begin

9 section {* Ideals *}

11 subsection {* Definitions *}

13 subsubsection {* General definition *}

15 locale ideal = additive_subgroup I R + ring R for I and R (structure) +

16 assumes I_l_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"

17 and I_r_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"

19 sublocale ideal \<subseteq> abelian_subgroup I R

20 apply (intro abelian_subgroupI3 abelian_group.intro)

21 apply (rule ideal.axioms, rule ideal_axioms)

22 apply (rule abelian_group.axioms, rule ring.axioms, rule ideal.axioms, rule ideal_axioms)

23 apply (rule abelian_group.axioms, rule ring.axioms, rule ideal.axioms, rule ideal_axioms)

24 done

26 lemma (in ideal) is_ideal: "ideal I R"

27 by (rule ideal_axioms)

29 lemma idealI:

30 fixes R (structure)

31 assumes "ring R"

32 assumes a_subgroup: "subgroup I \<lparr>carrier = carrier R, mult = add R, one = zero R\<rparr>"

33 and I_l_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"

34 and I_r_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"

35 shows "ideal I R"

36 proof -

37 interpret ring R by fact

38 show ?thesis apply (intro ideal.intro ideal_axioms.intro additive_subgroupI)

39 apply (rule a_subgroup)

40 apply (rule is_ring)

41 apply (erule (1) I_l_closed)

42 apply (erule (1) I_r_closed)

43 done

44 qed

47 subsubsection (in ring) {* Ideals Generated by a Subset of @{term "carrier R"} *}

49 definition genideal :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set" ("Idl\<index> _" [80] 79)

50 where "genideal R S = Inter {I. ideal I R \<and> S \<subseteq> I}"

52 subsubsection {* Principal Ideals *}

54 locale principalideal = ideal +

55 assumes generate: "\<exists>i \<in> carrier R. I = Idl {i}"

57 lemma (in principalideal) is_principalideal: "principalideal I R"

58 by (rule principalideal_axioms)

60 lemma principalidealI:

61 fixes R (structure)

62 assumes "ideal I R"

63 and generate: "\<exists>i \<in> carrier R. I = Idl {i}"

64 shows "principalideal I R"

65 proof -

66 interpret ideal I R by fact

67 show ?thesis

68 by (intro principalideal.intro principalideal_axioms.intro)

69 (rule is_ideal, rule generate)

70 qed

73 subsubsection {* Maximal Ideals *}

75 locale maximalideal = ideal +

76 assumes I_notcarr: "carrier R \<noteq> I"

77 and I_maximal: "\<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> J = I \<or> J = carrier R"

79 lemma (in maximalideal) is_maximalideal: "maximalideal I R"

80 by (rule maximalideal_axioms)

82 lemma maximalidealI:

83 fixes R

84 assumes "ideal I R"

85 and I_notcarr: "carrier R \<noteq> I"

86 and I_maximal: "\<And>J. \<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> J = I \<or> J = carrier R"

87 shows "maximalideal I R"

88 proof -

89 interpret ideal I R by fact

90 show ?thesis

91 by (intro maximalideal.intro maximalideal_axioms.intro)

92 (rule is_ideal, rule I_notcarr, rule I_maximal)

93 qed

96 subsubsection {* Prime Ideals *}

98 locale primeideal = ideal + cring +

99 assumes I_notcarr: "carrier R \<noteq> I"

100 and I_prime: "\<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I \<or> b \<in> I"

102 lemma (in primeideal) is_primeideal: "primeideal I R"

103 by (rule primeideal_axioms)

105 lemma primeidealI:

106 fixes R (structure)

107 assumes "ideal I R"

108 and "cring R"

109 and I_notcarr: "carrier R \<noteq> I"

110 and I_prime: "\<And>a b. \<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I \<or> b \<in> I"

111 shows "primeideal I R"

112 proof -

113 interpret ideal I R by fact

114 interpret cring R by fact

115 show ?thesis

116 by (intro primeideal.intro primeideal_axioms.intro)

117 (rule is_ideal, rule is_cring, rule I_notcarr, rule I_prime)

118 qed

120 lemma primeidealI2:

121 fixes R (structure)

122 assumes "additive_subgroup I R"

123 and "cring R"

124 and I_l_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"

125 and I_r_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"

126 and I_notcarr: "carrier R \<noteq> I"

127 and I_prime: "\<And>a b. \<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I \<or> b \<in> I"

128 shows "primeideal I R"

129 proof -

130 interpret additive_subgroup I R by fact

131 interpret cring R by fact

132 show ?thesis apply (intro_locales)

133 apply (intro ideal_axioms.intro)

134 apply (erule (1) I_l_closed)

135 apply (erule (1) I_r_closed)

136 apply (intro primeideal_axioms.intro)

137 apply (rule I_notcarr)

138 apply (erule (2) I_prime)

139 done

140 qed

143 subsection {* Special Ideals *}

145 lemma (in ring) zeroideal: "ideal {\<zero>} R"

146 apply (intro idealI subgroup.intro)

147 apply (rule is_ring)

148 apply simp+

149 apply (fold a_inv_def, simp)

150 apply simp+

151 done

153 lemma (in ring) oneideal: "ideal (carrier R) R"

154 by (rule idealI) (auto intro: is_ring add.subgroupI)

156 lemma (in "domain") zeroprimeideal: "primeideal {\<zero>} R"

157 apply (intro primeidealI)

158 apply (rule zeroideal)

159 apply (rule domain.axioms, rule domain_axioms)

160 defer 1

161 apply (simp add: integral)

162 proof (rule ccontr, simp)

163 assume "carrier R = {\<zero>}"

164 then have "\<one> = \<zero>" by (rule one_zeroI)

165 with one_not_zero show False by simp

166 qed

169 subsection {* General Ideal Properies *}

171 lemma (in ideal) one_imp_carrier:

172 assumes I_one_closed: "\<one> \<in> I"

173 shows "I = carrier R"

174 apply (rule)

175 apply (rule)

176 apply (rule a_Hcarr, simp)

177 proof

178 fix x

179 assume xcarr: "x \<in> carrier R"

180 with I_one_closed have "x \<otimes> \<one> \<in> I" by (intro I_l_closed)

181 with xcarr show "x \<in> I" by simp

182 qed

184 lemma (in ideal) Icarr:

185 assumes iI: "i \<in> I"

186 shows "i \<in> carrier R"

187 using iI by (rule a_Hcarr)

190 subsection {* Intersection of Ideals *}

192 text {* \paragraph{Intersection of two ideals} The intersection of any

193 two ideals is again an ideal in @{term R} *}

194 lemma (in ring) i_intersect:

195 assumes "ideal I R"

196 assumes "ideal J R"

197 shows "ideal (I \<inter> J) R"

198 proof -

199 interpret ideal I R by fact

200 interpret ideal J R by fact

201 show ?thesis

202 apply (intro idealI subgroup.intro)

203 apply (rule is_ring)

204 apply (force simp add: a_subset)

205 apply (simp add: a_inv_def[symmetric])

206 apply simp

207 apply (simp add: a_inv_def[symmetric])

208 apply (clarsimp, rule)

209 apply (fast intro: ideal.I_l_closed ideal.intro assms)+

210 apply (clarsimp, rule)

211 apply (fast intro: ideal.I_r_closed ideal.intro assms)+

212 done

213 qed

215 text {* The intersection of any Number of Ideals is again

216 an Ideal in @{term R} *}

217 lemma (in ring) i_Intersect:

218 assumes Sideals: "\<And>I. I \<in> S \<Longrightarrow> ideal I R"

219 and notempty: "S \<noteq> {}"

220 shows "ideal (Inter S) R"

221 apply (unfold_locales)

222 apply (simp_all add: Inter_eq)

223 apply rule unfolding mem_Collect_eq defer 1

224 apply rule defer 1

225 apply rule defer 1

226 apply (fold a_inv_def, rule) defer 1

227 apply rule defer 1

228 apply rule defer 1

229 proof -

230 fix x y

231 assume "\<forall>I\<in>S. x \<in> I"

232 then have xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp

233 assume "\<forall>I\<in>S. y \<in> I"

234 then have yI: "\<And>I. I \<in> S \<Longrightarrow> y \<in> I" by simp

236 fix J

237 assume JS: "J \<in> S"

238 interpret ideal J R by (rule Sideals[OF JS])

239 from xI[OF JS] and yI[OF JS] show "x \<oplus> y \<in> J" by (rule a_closed)

240 next

241 fix J

242 assume JS: "J \<in> S"

243 interpret ideal J R by (rule Sideals[OF JS])

244 show "\<zero> \<in> J" by simp

245 next

246 fix x

247 assume "\<forall>I\<in>S. x \<in> I"

248 then have xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp

250 fix J

251 assume JS: "J \<in> S"

252 interpret ideal J R by (rule Sideals[OF JS])

254 from xI[OF JS] show "\<ominus> x \<in> J" by (rule a_inv_closed)

255 next

256 fix x y

257 assume "\<forall>I\<in>S. x \<in> I"

258 then have xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp

259 assume ycarr: "y \<in> carrier R"

261 fix J

262 assume JS: "J \<in> S"

263 interpret ideal J R by (rule Sideals[OF JS])

265 from xI[OF JS] and ycarr show "y \<otimes> x \<in> J" by (rule I_l_closed)

266 next

267 fix x y

268 assume "\<forall>I\<in>S. x \<in> I"

269 then have xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp

270 assume ycarr: "y \<in> carrier R"

272 fix J

273 assume JS: "J \<in> S"

274 interpret ideal J R by (rule Sideals[OF JS])

276 from xI[OF JS] and ycarr show "x \<otimes> y \<in> J" by (rule I_r_closed)

277 next

278 fix x

279 assume "\<forall>I\<in>S. x \<in> I"

280 then have xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp

282 from notempty have "\<exists>I0. I0 \<in> S" by blast

283 then obtain I0 where I0S: "I0 \<in> S" by auto

285 interpret ideal I0 R by (rule Sideals[OF I0S])

287 from xI[OF I0S] have "x \<in> I0" .

288 with a_subset show "x \<in> carrier R" by fast

289 next

291 qed

294 subsection {* Addition of Ideals *}

296 lemma (in ring) add_ideals:

297 assumes idealI: "ideal I R"

298 and idealJ: "ideal J R"

299 shows "ideal (I <+> J) R"

300 apply (rule ideal.intro)

301 apply (rule add_additive_subgroups)

302 apply (intro ideal.axioms[OF idealI])

303 apply (intro ideal.axioms[OF idealJ])

304 apply (rule is_ring)

305 apply (rule ideal_axioms.intro)

306 apply (simp add: set_add_defs, clarsimp) defer 1

307 apply (simp add: set_add_defs, clarsimp) defer 1

308 proof -

309 fix x i j

310 assume xcarr: "x \<in> carrier R"

311 and iI: "i \<in> I"

312 and jJ: "j \<in> J"

313 from xcarr ideal.Icarr[OF idealI iI] ideal.Icarr[OF idealJ jJ]

314 have c: "(i \<oplus> j) \<otimes> x = (i \<otimes> x) \<oplus> (j \<otimes> x)"

315 by algebra

316 from xcarr and iI have a: "i \<otimes> x \<in> I"

317 by (simp add: ideal.I_r_closed[OF idealI])

318 from xcarr and jJ have b: "j \<otimes> x \<in> J"

319 by (simp add: ideal.I_r_closed[OF idealJ])

320 from a b c show "\<exists>ha\<in>I. \<exists>ka\<in>J. (i \<oplus> j) \<otimes> x = ha \<oplus> ka"

321 by fast

322 next

323 fix x i j

324 assume xcarr: "x \<in> carrier R"

325 and iI: "i \<in> I"

326 and jJ: "j \<in> J"

327 from xcarr ideal.Icarr[OF idealI iI] ideal.Icarr[OF idealJ jJ]

328 have c: "x \<otimes> (i \<oplus> j) = (x \<otimes> i) \<oplus> (x \<otimes> j)" by algebra

329 from xcarr and iI have a: "x \<otimes> i \<in> I"

330 by (simp add: ideal.I_l_closed[OF idealI])

331 from xcarr and jJ have b: "x \<otimes> j \<in> J"

332 by (simp add: ideal.I_l_closed[OF idealJ])

333 from a b c show "\<exists>ha\<in>I. \<exists>ka\<in>J. x \<otimes> (i \<oplus> j) = ha \<oplus> ka"

334 by fast

335 qed

338 subsection (in ring) {* Ideals generated by a subset of @{term "carrier R"} *}

340 text {* @{term genideal} generates an ideal *}

341 lemma (in ring) genideal_ideal:

342 assumes Scarr: "S \<subseteq> carrier R"

343 shows "ideal (Idl S) R"

344 unfolding genideal_def

345 proof (rule i_Intersect, fast, simp)

346 from oneideal and Scarr

347 show "\<exists>I. ideal I R \<and> S \<le> I" by fast

348 qed

350 lemma (in ring) genideal_self:

351 assumes "S \<subseteq> carrier R"

352 shows "S \<subseteq> Idl S"

353 unfolding genideal_def by fast

355 lemma (in ring) genideal_self':

356 assumes carr: "i \<in> carrier R"

357 shows "i \<in> Idl {i}"

358 proof -

359 from carr have "{i} \<subseteq> Idl {i}" by (fast intro!: genideal_self)

360 then show "i \<in> Idl {i}" by fast

361 qed

363 text {* @{term genideal} generates the minimal ideal *}

364 lemma (in ring) genideal_minimal:

365 assumes a: "ideal I R"

366 and b: "S \<subseteq> I"

367 shows "Idl S \<subseteq> I"

368 unfolding genideal_def by rule (elim InterD, simp add: a b)

370 text {* Generated ideals and subsets *}

371 lemma (in ring) Idl_subset_ideal:

372 assumes Iideal: "ideal I R"

373 and Hcarr: "H \<subseteq> carrier R"

374 shows "(Idl H \<subseteq> I) = (H \<subseteq> I)"

375 proof

376 assume a: "Idl H \<subseteq> I"

377 from Hcarr have "H \<subseteq> Idl H" by (rule genideal_self)

378 with a show "H \<subseteq> I" by simp

379 next

380 fix x

381 assume "H \<subseteq> I"

382 with Iideal have "I \<in> {I. ideal I R \<and> H \<subseteq> I}" by fast

383 then show "Idl H \<subseteq> I" unfolding genideal_def by fast

384 qed

386 lemma (in ring) subset_Idl_subset:

387 assumes Icarr: "I \<subseteq> carrier R"

388 and HI: "H \<subseteq> I"

389 shows "Idl H \<subseteq> Idl I"

390 proof -

391 from HI and genideal_self[OF Icarr] have HIdlI: "H \<subseteq> Idl I"

392 by fast

394 from Icarr have Iideal: "ideal (Idl I) R"

395 by (rule genideal_ideal)

396 from HI and Icarr have "H \<subseteq> carrier R"

397 by fast

398 with Iideal have "(H \<subseteq> Idl I) = (Idl H \<subseteq> Idl I)"

399 by (rule Idl_subset_ideal[symmetric])

401 with HIdlI show "Idl H \<subseteq> Idl I" by simp

402 qed

404 lemma (in ring) Idl_subset_ideal':

405 assumes acarr: "a \<in> carrier R" and bcarr: "b \<in> carrier R"

406 shows "(Idl {a} \<subseteq> Idl {b}) = (a \<in> Idl {b})"

407 apply (subst Idl_subset_ideal[OF genideal_ideal[of "{b}"], of "{a}"])

408 apply (fast intro: bcarr, fast intro: acarr)

409 apply fast

410 done

412 lemma (in ring) genideal_zero: "Idl {\<zero>} = {\<zero>}"

413 apply rule

414 apply (rule genideal_minimal[OF zeroideal], simp)

415 apply (simp add: genideal_self')

416 done

418 lemma (in ring) genideal_one: "Idl {\<one>} = carrier R"

419 proof -

420 interpret ideal "Idl {\<one>}" "R" by (rule genideal_ideal) fast

421 show "Idl {\<one>} = carrier R"

422 apply (rule, rule a_subset)

423 apply (simp add: one_imp_carrier genideal_self')

424 done

425 qed

428 text {* Generation of Principal Ideals in Commutative Rings *}

430 definition cgenideal :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set" ("PIdl\<index> _" [80] 79)

431 where "cgenideal R a = {x \<otimes>\<^bsub>R\<^esub> a | x. x \<in> carrier R}"

433 text {* genhideal (?) really generates an ideal *}

434 lemma (in cring) cgenideal_ideal:

435 assumes acarr: "a \<in> carrier R"

436 shows "ideal (PIdl a) R"

437 apply (unfold cgenideal_def)

438 apply (rule idealI[OF is_ring])

439 apply (rule subgroup.intro)

440 apply simp_all

441 apply (blast intro: acarr)

442 apply clarsimp defer 1

443 defer 1

444 apply (fold a_inv_def, clarsimp) defer 1

445 apply clarsimp defer 1

446 apply clarsimp defer 1

447 proof -

448 fix x y

449 assume xcarr: "x \<in> carrier R"

450 and ycarr: "y \<in> carrier R"

451 note carr = acarr xcarr ycarr

453 from carr have "x \<otimes> a \<oplus> y \<otimes> a = (x \<oplus> y) \<otimes> a"

454 by (simp add: l_distr)

455 with carr show "\<exists>z. x \<otimes> a \<oplus> y \<otimes> a = z \<otimes> a \<and> z \<in> carrier R"

456 by fast

457 next

458 from l_null[OF acarr, symmetric] and zero_closed

459 show "\<exists>x. \<zero> = x \<otimes> a \<and> x \<in> carrier R" by fast

460 next

461 fix x

462 assume xcarr: "x \<in> carrier R"

463 note carr = acarr xcarr

465 from carr have "\<ominus> (x \<otimes> a) = (\<ominus> x) \<otimes> a"

466 by (simp add: l_minus)

467 with carr show "\<exists>z. \<ominus> (x \<otimes> a) = z \<otimes> a \<and> z \<in> carrier R"

468 by fast

469 next

470 fix x y

471 assume xcarr: "x \<in> carrier R"

472 and ycarr: "y \<in> carrier R"

473 note carr = acarr xcarr ycarr

475 from carr have "y \<otimes> a \<otimes> x = (y \<otimes> x) \<otimes> a"

476 by (simp add: m_assoc) (simp add: m_comm)

477 with carr show "\<exists>z. y \<otimes> a \<otimes> x = z \<otimes> a \<and> z \<in> carrier R"

478 by fast

479 next

480 fix x y

481 assume xcarr: "x \<in> carrier R"

482 and ycarr: "y \<in> carrier R"

483 note carr = acarr xcarr ycarr

485 from carr have "x \<otimes> (y \<otimes> a) = (x \<otimes> y) \<otimes> a"

486 by (simp add: m_assoc)

487 with carr show "\<exists>z. x \<otimes> (y \<otimes> a) = z \<otimes> a \<and> z \<in> carrier R"

488 by fast

489 qed

491 lemma (in ring) cgenideal_self:

492 assumes icarr: "i \<in> carrier R"

493 shows "i \<in> PIdl i"

494 unfolding cgenideal_def

495 proof simp

496 from icarr have "i = \<one> \<otimes> i"

497 by simp

498 with icarr show "\<exists>x. i = x \<otimes> i \<and> x \<in> carrier R"

499 by fast

500 qed

502 text {* @{const "cgenideal"} is minimal *}

504 lemma (in ring) cgenideal_minimal:

505 assumes "ideal J R"

506 assumes aJ: "a \<in> J"

507 shows "PIdl a \<subseteq> J"

508 proof -

509 interpret ideal J R by fact

510 show ?thesis

511 unfolding cgenideal_def

512 apply rule

513 apply clarify

514 using aJ

515 apply (erule I_l_closed)

516 done

517 qed

519 lemma (in cring) cgenideal_eq_genideal:

520 assumes icarr: "i \<in> carrier R"

521 shows "PIdl i = Idl {i}"

522 apply rule

523 apply (intro cgenideal_minimal)

524 apply (rule genideal_ideal, fast intro: icarr)

525 apply (rule genideal_self', fast intro: icarr)

526 apply (intro genideal_minimal)

527 apply (rule cgenideal_ideal [OF icarr])

528 apply (simp, rule cgenideal_self [OF icarr])

529 done

531 lemma (in cring) cgenideal_eq_rcos: "PIdl i = carrier R #> i"

532 unfolding cgenideal_def r_coset_def by fast

534 lemma (in cring) cgenideal_is_principalideal:

535 assumes icarr: "i \<in> carrier R"

536 shows "principalideal (PIdl i) R"

537 apply (rule principalidealI)

538 apply (rule cgenideal_ideal [OF icarr])

539 proof -

540 from icarr have "PIdl i = Idl {i}"

541 by (rule cgenideal_eq_genideal)

542 with icarr show "\<exists>i'\<in>carrier R. PIdl i = Idl {i'}"

543 by fast

544 qed

547 subsection {* Union of Ideals *}

549 lemma (in ring) union_genideal:

550 assumes idealI: "ideal I R"

551 and idealJ: "ideal J R"

552 shows "Idl (I \<union> J) = I <+> J"

553 apply rule

554 apply (rule ring.genideal_minimal)

555 apply (rule is_ring)

556 apply (rule add_ideals[OF idealI idealJ])

557 apply (rule)

558 apply (simp add: set_add_defs) apply (elim disjE) defer 1 defer 1

559 apply (rule) apply (simp add: set_add_defs genideal_def) apply clarsimp defer 1

560 proof -

561 fix x

562 assume xI: "x \<in> I"

563 have ZJ: "\<zero> \<in> J"

564 by (intro additive_subgroup.zero_closed) (rule ideal.axioms[OF idealJ])

565 from ideal.Icarr[OF idealI xI] have "x = x \<oplus> \<zero>"

566 by algebra

567 with xI and ZJ show "\<exists>h\<in>I. \<exists>k\<in>J. x = h \<oplus> k"

568 by fast

569 next

570 fix x

571 assume xJ: "x \<in> J"

572 have ZI: "\<zero> \<in> I"

573 by (intro additive_subgroup.zero_closed, rule ideal.axioms[OF idealI])

574 from ideal.Icarr[OF idealJ xJ] have "x = \<zero> \<oplus> x"

575 by algebra

576 with ZI and xJ show "\<exists>h\<in>I. \<exists>k\<in>J. x = h \<oplus> k"

577 by fast

578 next

579 fix i j K

580 assume iI: "i \<in> I"

581 and jJ: "j \<in> J"

582 and idealK: "ideal K R"

583 and IK: "I \<subseteq> K"

584 and JK: "J \<subseteq> K"

585 from iI and IK have iK: "i \<in> K" by fast

586 from jJ and JK have jK: "j \<in> K" by fast

587 from iK and jK show "i \<oplus> j \<in> K"

588 by (intro additive_subgroup.a_closed) (rule ideal.axioms[OF idealK])

589 qed

592 subsection {* Properties of Principal Ideals *}

594 text {* @{text "\<zero>"} generates the zero ideal *}

595 lemma (in ring) zero_genideal: "Idl {\<zero>} = {\<zero>}"

596 apply rule

597 apply (simp add: genideal_minimal zeroideal)

598 apply (fast intro!: genideal_self)

599 done

601 text {* @{text "\<one>"} generates the unit ideal *}

602 lemma (in ring) one_genideal: "Idl {\<one>} = carrier R"

603 proof -

604 have "\<one> \<in> Idl {\<one>}"

605 by (simp add: genideal_self')

606 then show "Idl {\<one>} = carrier R"

607 by (intro ideal.one_imp_carrier) (fast intro: genideal_ideal)

608 qed

611 text {* The zero ideal is a principal ideal *}

612 corollary (in ring) zeropideal: "principalideal {\<zero>} R"

613 apply (rule principalidealI)

614 apply (rule zeroideal)

615 apply (blast intro!: zero_genideal[symmetric])

616 done

618 text {* The unit ideal is a principal ideal *}

619 corollary (in ring) onepideal: "principalideal (carrier R) R"

620 apply (rule principalidealI)

621 apply (rule oneideal)

622 apply (blast intro!: one_genideal[symmetric])

623 done

626 text {* Every principal ideal is a right coset of the carrier *}

627 lemma (in principalideal) rcos_generate:

628 assumes "cring R"

629 shows "\<exists>x\<in>I. I = carrier R #> x"

630 proof -

631 interpret cring R by fact

632 from generate obtain i where icarr: "i \<in> carrier R" and I1: "I = Idl {i}"

633 by fast+

635 from icarr and genideal_self[of "{i}"] have "i \<in> Idl {i}"

636 by fast

637 then have iI: "i \<in> I" by (simp add: I1)

639 from I1 icarr have I2: "I = PIdl i"

640 by (simp add: cgenideal_eq_genideal)

642 have "PIdl i = carrier R #> i"

643 unfolding cgenideal_def r_coset_def by fast

645 with I2 have "I = carrier R #> i"

646 by simp

648 with iI show "\<exists>x\<in>I. I = carrier R #> x"

649 by fast

650 qed

653 subsection {* Prime Ideals *}

655 lemma (in ideal) primeidealCD:

656 assumes "cring R"

657 assumes notprime: "\<not> primeideal I R"

658 shows "carrier R = I \<or> (\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I)"

659 proof (rule ccontr, clarsimp)

660 interpret cring R by fact

661 assume InR: "carrier R \<noteq> I"

662 and "\<forall>a. a \<in> carrier R \<longrightarrow> (\<forall>b. a \<otimes> b \<in> I \<longrightarrow> b \<in> carrier R \<longrightarrow> a \<in> I \<or> b \<in> I)"

663 then have I_prime: "\<And> a b. \<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I \<or> b \<in> I"

664 by simp

665 have "primeideal I R"

666 apply (rule primeideal.intro [OF is_ideal is_cring])

667 apply (rule primeideal_axioms.intro)

668 apply (rule InR)

669 apply (erule (2) I_prime)

670 done

671 with notprime show False by simp

672 qed

674 lemma (in ideal) primeidealCE:

675 assumes "cring R"

676 assumes notprime: "\<not> primeideal I R"

677 obtains "carrier R = I"

678 | "\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I"

679 proof -

680 interpret R: cring R by fact

681 assume "carrier R = I ==> thesis"

682 and "\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I \<Longrightarrow> thesis"

683 then show thesis using primeidealCD [OF R.is_cring notprime] by blast

684 qed

686 text {* If @{text "{\<zero>}"} is a prime ideal of a commutative ring, the ring is a domain *}

687 lemma (in cring) zeroprimeideal_domainI:

688 assumes pi: "primeideal {\<zero>} R"

689 shows "domain R"

690 apply (rule domain.intro, rule is_cring)

691 apply (rule domain_axioms.intro)

692 proof (rule ccontr, simp)

693 interpret primeideal "{\<zero>}" "R" by (rule pi)

694 assume "\<one> = \<zero>"

695 then have "carrier R = {\<zero>}" by (rule one_zeroD)

696 from this[symmetric] and I_notcarr show False

697 by simp

698 next

699 interpret primeideal "{\<zero>}" "R" by (rule pi)

700 fix a b

701 assume ab: "a \<otimes> b = \<zero>" and carr: "a \<in> carrier R" "b \<in> carrier R"

702 from ab have abI: "a \<otimes> b \<in> {\<zero>}"

703 by fast

704 with carr have "a \<in> {\<zero>} \<or> b \<in> {\<zero>}"

705 by (rule I_prime)

706 then show "a = \<zero> \<or> b = \<zero>" by simp

707 qed

709 corollary (in cring) domain_eq_zeroprimeideal: "domain R = primeideal {\<zero>} R"

710 apply rule

711 apply (erule domain.zeroprimeideal)

712 apply (erule zeroprimeideal_domainI)

713 done

716 subsection {* Maximal Ideals *}

718 lemma (in ideal) helper_I_closed:

719 assumes carr: "a \<in> carrier R" "x \<in> carrier R" "y \<in> carrier R"

720 and axI: "a \<otimes> x \<in> I"

721 shows "a \<otimes> (x \<otimes> y) \<in> I"

722 proof -

723 from axI and carr have "(a \<otimes> x) \<otimes> y \<in> I"

724 by (simp add: I_r_closed)

725 also from carr have "(a \<otimes> x) \<otimes> y = a \<otimes> (x \<otimes> y)"

726 by (simp add: m_assoc)

727 finally show "a \<otimes> (x \<otimes> y) \<in> I" .

728 qed

730 lemma (in ideal) helper_max_prime:

731 assumes "cring R"

732 assumes acarr: "a \<in> carrier R"

733 shows "ideal {x\<in>carrier R. a \<otimes> x \<in> I} R"

734 proof -

735 interpret cring R by fact

736 show ?thesis apply (rule idealI)

737 apply (rule cring.axioms[OF is_cring])

738 apply (rule subgroup.intro)

739 apply (simp, fast)

740 apply clarsimp apply (simp add: r_distr acarr)

741 apply (simp add: acarr)

742 apply (simp add: a_inv_def[symmetric], clarify) defer 1

743 apply clarsimp defer 1

744 apply (fast intro!: helper_I_closed acarr)

745 proof -

746 fix x

747 assume xcarr: "x \<in> carrier R"

748 and ax: "a \<otimes> x \<in> I"

749 from ax and acarr xcarr

750 have "\<ominus>(a \<otimes> x) \<in> I" by simp

751 also from acarr xcarr

752 have "\<ominus>(a \<otimes> x) = a \<otimes> (\<ominus>x)" by algebra

753 finally show "a \<otimes> (\<ominus>x) \<in> I" .

754 from acarr have "a \<otimes> \<zero> = \<zero>" by simp

755 next

756 fix x y

757 assume xcarr: "x \<in> carrier R"

758 and ycarr: "y \<in> carrier R"

759 and ayI: "a \<otimes> y \<in> I"

760 from ayI and acarr xcarr ycarr have "a \<otimes> (y \<otimes> x) \<in> I"

761 by (simp add: helper_I_closed)

762 moreover

763 from xcarr ycarr have "y \<otimes> x = x \<otimes> y"

764 by (simp add: m_comm)

765 ultimately

766 show "a \<otimes> (x \<otimes> y) \<in> I" by simp

767 qed

768 qed

770 text {* In a cring every maximal ideal is prime *}

771 lemma (in cring) maximalideal_is_prime:

772 assumes "maximalideal I R"

773 shows "primeideal I R"

774 proof -

775 interpret maximalideal I R by fact

776 show ?thesis apply (rule ccontr)

777 apply (rule primeidealCE)

778 apply (rule is_cring)

779 apply assumption

780 apply (simp add: I_notcarr)

781 proof -

782 assume "\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I"

783 then obtain a b where

784 acarr: "a \<in> carrier R" and

785 bcarr: "b \<in> carrier R" and

786 abI: "a \<otimes> b \<in> I" and

787 anI: "a \<notin> I" and

788 bnI: "b \<notin> I" by fast

789 def J \<equiv> "{x\<in>carrier R. a \<otimes> x \<in> I}"

791 from is_cring and acarr have idealJ: "ideal J R"

792 unfolding J_def by (rule helper_max_prime)

794 have IsubJ: "I \<subseteq> J"

795 proof

796 fix x

797 assume xI: "x \<in> I"

798 with acarr have "a \<otimes> x \<in> I"

799 by (intro I_l_closed)

800 with xI[THEN a_Hcarr] show "x \<in> J"

801 unfolding J_def by fast

802 qed

804 from abI and acarr bcarr have "b \<in> J"

805 unfolding J_def by fast

806 with bnI have JnI: "J \<noteq> I" by fast

807 from acarr

808 have "a = a \<otimes> \<one>" by algebra

809 with anI have "a \<otimes> \<one> \<notin> I" by simp

810 with one_closed have "\<one> \<notin> J"

811 unfolding J_def by fast

812 then have Jncarr: "J \<noteq> carrier R" by fast

814 interpret ideal J R by (rule idealJ)

816 have "J = I \<or> J = carrier R"

817 apply (intro I_maximal)

818 apply (rule idealJ)

819 apply (rule IsubJ)

820 apply (rule a_subset)

821 done

823 with JnI and Jncarr show False by simp

824 qed

825 qed

828 subsection {* Derived Theorems *}

830 --"A non-zero cring that has only the two trivial ideals is a field"

831 lemma (in cring) trivialideals_fieldI:

832 assumes carrnzero: "carrier R \<noteq> {\<zero>}"

833 and haveideals: "{I. ideal I R} = {{\<zero>}, carrier R}"

834 shows "field R"

835 apply (rule cring_fieldI)

836 apply (rule, rule, rule)

837 apply (erule Units_closed)

838 defer 1

839 apply rule

840 defer 1

841 proof (rule ccontr, simp)

842 assume zUnit: "\<zero> \<in> Units R"

843 then have a: "\<zero> \<otimes> inv \<zero> = \<one>" by (rule Units_r_inv)

844 from zUnit have "\<zero> \<otimes> inv \<zero> = \<zero>"

845 by (intro l_null) (rule Units_inv_closed)

846 with a[symmetric] have "\<one> = \<zero>" by simp

847 then have "carrier R = {\<zero>}" by (rule one_zeroD)

848 with carrnzero show False by simp

849 next

850 fix x

851 assume xcarr': "x \<in> carrier R - {\<zero>}"

852 then have xcarr: "x \<in> carrier R" by fast

853 from xcarr' have xnZ: "x \<noteq> \<zero>" by fast

854 from xcarr have xIdl: "ideal (PIdl x) R"

855 by (intro cgenideal_ideal) fast

857 from xcarr have "x \<in> PIdl x"

858 by (intro cgenideal_self) fast

859 with xnZ have "PIdl x \<noteq> {\<zero>}" by fast

860 with haveideals have "PIdl x = carrier R"

861 by (blast intro!: xIdl)

862 then have "\<one> \<in> PIdl x" by simp

863 then have "\<exists>y. \<one> = y \<otimes> x \<and> y \<in> carrier R"

864 unfolding cgenideal_def by blast

865 then obtain y where ycarr: " y \<in> carrier R" and ylinv: "\<one> = y \<otimes> x"

866 by fast+

867 from ylinv and xcarr ycarr have yrinv: "\<one> = x \<otimes> y"

868 by (simp add: m_comm)

869 from ycarr and ylinv[symmetric] and yrinv[symmetric]

870 have "\<exists>y \<in> carrier R. y \<otimes> x = \<one> \<and> x \<otimes> y = \<one>" by fast

871 with xcarr show "x \<in> Units R"

872 unfolding Units_def by fast

873 qed

875 lemma (in field) all_ideals: "{I. ideal I R} = {{\<zero>}, carrier R}"

876 apply (rule, rule)

877 proof -

878 fix I

879 assume a: "I \<in> {I. ideal I R}"

880 then interpret ideal I R by simp

882 show "I \<in> {{\<zero>}, carrier R}"

883 proof (cases "\<exists>a. a \<in> I - {\<zero>}")

884 case True

885 then obtain a where aI: "a \<in> I" and anZ: "a \<noteq> \<zero>"

886 by fast+

887 from aI[THEN a_Hcarr] anZ have aUnit: "a \<in> Units R"

888 by (simp add: field_Units)

889 then have a: "a \<otimes> inv a = \<one>" by (rule Units_r_inv)

890 from aI and aUnit have "a \<otimes> inv a \<in> I"

891 by (simp add: I_r_closed del: Units_r_inv)

892 then have oneI: "\<one> \<in> I" by (simp add: a[symmetric])

894 have "carrier R \<subseteq> I"

895 proof

896 fix x

897 assume xcarr: "x \<in> carrier R"

898 with oneI have "\<one> \<otimes> x \<in> I" by (rule I_r_closed)

899 with xcarr show "x \<in> I" by simp

900 qed

901 with a_subset have "I = carrier R" by fast

902 then show "I \<in> {{\<zero>}, carrier R}" by fast

903 next

904 case False

905 then have IZ: "\<And>a. a \<in> I \<Longrightarrow> a = \<zero>" by simp

907 have a: "I \<subseteq> {\<zero>}"

908 proof

909 fix x

910 assume "x \<in> I"

911 then have "x = \<zero>" by (rule IZ)

912 then show "x \<in> {\<zero>}" by fast

913 qed

915 have "\<zero> \<in> I" by simp

916 then have "{\<zero>} \<subseteq> I" by fast

918 with a have "I = {\<zero>}" by fast

919 then show "I \<in> {{\<zero>}, carrier R}" by fast

920 qed

921 qed (simp add: zeroideal oneideal)

923 --"Jacobson Theorem 2.2"

924 lemma (in cring) trivialideals_eq_field:

925 assumes carrnzero: "carrier R \<noteq> {\<zero>}"

926 shows "({I. ideal I R} = {{\<zero>}, carrier R}) = field R"

927 by (fast intro!: trivialideals_fieldI[OF carrnzero] field.all_ideals)

930 text {* Like zeroprimeideal for domains *}

931 lemma (in field) zeromaximalideal: "maximalideal {\<zero>} R"

932 apply (rule maximalidealI)

933 apply (rule zeroideal)

934 proof-

935 from one_not_zero have "\<one> \<notin> {\<zero>}" by simp

936 with one_closed show "carrier R \<noteq> {\<zero>}" by fast

937 next

938 fix J

939 assume Jideal: "ideal J R"

940 then have "J \<in> {I. ideal I R}" by fast

941 with all_ideals show "J = {\<zero>} \<or> J = carrier R"

942 by simp

943 qed

945 lemma (in cring) zeromaximalideal_fieldI:

946 assumes zeromax: "maximalideal {\<zero>} R"

947 shows "field R"

948 apply (rule trivialideals_fieldI, rule maximalideal.I_notcarr[OF zeromax])

949 apply rule apply clarsimp defer 1

950 apply (simp add: zeroideal oneideal)

951 proof -

952 fix J

953 assume Jn0: "J \<noteq> {\<zero>}"

954 and idealJ: "ideal J R"

955 interpret ideal J R by (rule idealJ)

956 have "{\<zero>} \<subseteq> J" by (rule ccontr) simp

957 from zeromax and idealJ and this and a_subset

958 have "J = {\<zero>} \<or> J = carrier R"

959 by (rule maximalideal.I_maximal)

960 with Jn0 show "J = carrier R"

961 by simp

962 qed

964 lemma (in cring) zeromaximalideal_eq_field: "maximalideal {\<zero>} R = field R"

965 apply rule

966 apply (erule zeromaximalideal_fieldI)

967 apply (erule field.zeromaximalideal)

968 done

970 end