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

src/HOL/Algebra/Ideal.thy

author | wenzelm |

Sun Mar 21 15:57:40 2010 +0100 (2010-03-21) | |

changeset 35847 | 19f1f7066917 |

parent 30729 | 461ee3e49ad3 |

child 35848 | 5443079512ea |

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

eliminated old constdefs;

1 (*

2 Title: HOL/Algebra/CIdeal.thy

3 Author: Stephan Hohe, TU Muenchen

4 *)

6 theory Ideal

7 imports Ring AbelCoset

8 begin

10 section {* Ideals *}

12 subsection {* Definitions *}

14 subsubsection {* General definition *}

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

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

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

20 sublocale ideal \<subseteq> abelian_subgroup I R

21 apply (intro abelian_subgroupI3 abelian_group.intro)

22 apply (rule ideal.axioms, rule ideal_axioms)

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

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

25 done

27 lemma (in ideal) is_ideal:

28 "ideal I R"

29 by (rule ideal_axioms)

31 lemma idealI:

32 fixes R (structure)

33 assumes "ring R"

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

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

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

37 shows "ideal I R"

38 proof -

39 interpret ring R by fact

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

41 apply (rule a_subgroup)

42 apply (rule is_ring)

43 apply (erule (1) I_l_closed)

44 apply (erule (1) I_r_closed)

45 done

46 qed

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

50 definition

51 genideal :: "('a, 'b) ring_scheme \<Rightarrow> 'a set \<Rightarrow> 'a set" ("Idl\<index> _" [80] 79)

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

55 subsubsection {* Principal Ideals *}

57 locale principalideal = ideal +

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

60 lemma (in principalideal) is_principalideal:

61 shows "principalideal I R"

62 by (rule principalideal_axioms)

64 lemma principalidealI:

65 fixes R (structure)

66 assumes "ideal I R"

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

68 shows "principalideal I R"

69 proof -

70 interpret ideal I R by fact

71 show ?thesis by (intro principalideal.intro principalideal_axioms.intro) (rule is_ideal, rule generate)

72 qed

74 subsubsection {* Maximal Ideals *}

76 locale maximalideal = ideal +

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

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

80 lemma (in maximalideal) is_maximalideal:

81 shows "maximalideal I R"

82 by (rule maximalideal_axioms)

84 lemma maximalidealI:

85 fixes R

86 assumes "ideal I R"

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

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

89 shows "maximalideal I R"

90 proof -

91 interpret ideal I R by fact

92 show ?thesis by (intro maximalideal.intro maximalideal_axioms.intro)

93 (rule is_ideal, rule I_notcarr, rule I_maximal)

94 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:

103 shows "primeideal I R"

104 by (rule primeideal_axioms)

106 lemma primeidealI:

107 fixes R (structure)

108 assumes "ideal I R"

109 assumes "cring R"

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

111 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"

112 shows "primeideal I R"

113 proof -

114 interpret ideal I R by fact

115 interpret cring R by fact

116 show ?thesis 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 assumes "cring R"

124 assumes 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

142 subsection {* Special Ideals *}

144 lemma (in ring) zeroideal:

145 shows "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:

154 shows "ideal (carrier R) R"

155 apply (intro idealI subgroup.intro)

156 apply (rule is_ring)

157 apply simp+

158 apply (fold a_inv_def, simp)

159 apply simp+

160 done

162 lemma (in "domain") zeroprimeideal:

163 shows "primeideal {\<zero>} R"

164 apply (intro primeidealI)

165 apply (rule zeroideal)

166 apply (rule domain.axioms, rule domain_axioms)

167 defer 1

168 apply (simp add: integral)

169 proof (rule ccontr, simp)

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

171 from this have "\<one> = \<zero>" by (rule one_zeroI)

172 from this and one_not_zero

173 show "False" by simp

174 qed

177 subsection {* General Ideal Properies *}

179 lemma (in ideal) one_imp_carrier:

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

181 shows "I = carrier R"

182 apply (rule)

183 apply (rule)

184 apply (rule a_Hcarr, simp)

185 proof

186 fix x

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

188 from I_one_closed and this

189 have "x \<otimes> \<one> \<in> I" by (intro I_l_closed)

190 from this and xcarr

191 show "x \<in> I" by simp

192 qed

194 lemma (in ideal) Icarr:

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

196 shows "i \<in> carrier R"

197 using iI by (rule a_Hcarr)

200 subsection {* Intersection of Ideals *}

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

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

204 lemma (in ring) i_intersect:

205 assumes "ideal I R"

206 assumes "ideal J R"

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

208 proof -

209 interpret ideal I R by fact

210 interpret ideal J R by fact

211 show ?thesis

212 apply (intro idealI subgroup.intro)

213 apply (rule is_ring)

214 apply (force simp add: a_subset)

215 apply (simp add: a_inv_def[symmetric])

216 apply simp

217 apply (simp add: a_inv_def[symmetric])

218 apply (clarsimp, rule)

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

220 apply (clarsimp, rule)

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

222 done

223 qed

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

226 an Ideal in @{term R} *}

227 lemma (in ring) i_Intersect:

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

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

230 shows "ideal (Inter S) R"

231 apply (unfold_locales)

232 apply (simp_all add: Inter_def INTER_def)

233 apply (rule, simp) defer 1

234 apply rule defer 1

235 apply rule defer 1

236 apply (fold a_inv_def, rule) defer 1

237 apply rule defer 1

238 apply rule defer 1

239 proof -

240 fix x

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

242 hence xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp

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

245 from this obtain I0 where I0S: "I0 \<in> S" by auto

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

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

250 from this and a_subset show "x \<in> carrier R" by fast

251 next

252 fix x y

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

254 hence xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp

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

256 hence yI: "\<And>I. I \<in> S \<Longrightarrow> y \<in> I" by simp

258 fix J

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

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

261 from xI[OF JS] and yI[OF JS]

262 show "x \<oplus> y \<in> J" by (rule a_closed)

263 next

264 fix J

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

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

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

268 next

269 fix x

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

271 hence xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp

273 fix J

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

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

277 from xI[OF JS]

278 show "\<ominus> x \<in> J" by (rule a_inv_closed)

279 next

280 fix x y

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

282 hence xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp

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

285 fix J

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

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

289 from xI[OF JS] and ycarr

290 show "y \<otimes> x \<in> J" by (rule I_l_closed)

291 next

292 fix x y

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

294 hence xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp

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

297 fix J

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

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

301 from xI[OF JS] and ycarr

302 show "x \<otimes> y \<in> J" by (rule I_r_closed)

303 qed

306 subsection {* Addition of Ideals *}

308 lemma (in ring) add_ideals:

309 assumes idealI: "ideal I R"

310 and idealJ: "ideal J R"

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

312 apply (rule ideal.intro)

313 apply (rule add_additive_subgroups)

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

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

316 apply (rule is_ring)

317 apply (rule ideal_axioms.intro)

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

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

320 proof -

321 fix x i j

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

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

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

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

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

327 from xcarr and iI

328 have a: "i \<otimes> x \<in> I" by (simp add: ideal.I_r_closed[OF idealI])

329 from xcarr and jJ

330 have b: "j \<otimes> x \<in> J" by (simp add: ideal.I_r_closed[OF idealJ])

331 from a b c

332 show "\<exists>ha\<in>I. \<exists>ka\<in>J. (i \<oplus> j) \<otimes> x = ha \<oplus> ka" by fast

333 next

334 fix x i j

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

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

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

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

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

340 from xcarr and iI

341 have a: "x \<otimes> i \<in> I" by (simp add: ideal.I_l_closed[OF idealI])

342 from xcarr and jJ

343 have b: "x \<otimes> j \<in> J" by (simp add: ideal.I_l_closed[OF idealJ])

344 from a b c

345 show "\<exists>ha\<in>I. \<exists>ka\<in>J. x \<otimes> (i \<oplus> j) = ha \<oplus> ka" by fast

346 qed

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

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

352 lemma (in ring) genideal_ideal:

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

354 shows "ideal (Idl S) R"

355 unfolding genideal_def

356 proof (rule i_Intersect, fast, simp)

357 from oneideal and Scarr

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

359 qed

361 lemma (in ring) genideal_self:

362 assumes "S \<subseteq> carrier R"

363 shows "S \<subseteq> Idl S"

364 unfolding genideal_def

365 by fast

367 lemma (in ring) genideal_self':

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

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

370 proof -

371 from carr

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

373 thus "i \<in> Idl {i}" by fast

374 qed

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

377 lemma (in ring) genideal_minimal:

378 assumes a: "ideal I R"

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

380 shows "Idl S \<subseteq> I"

381 unfolding genideal_def

382 by (rule, elim InterD, simp add: a b)

384 text {* Generated ideals and subsets *}

385 lemma (in ring) Idl_subset_ideal:

386 assumes Iideal: "ideal I R"

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

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

389 proof

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

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

392 from this and a

393 show "H \<subseteq> I" by simp

394 next

395 fix x

396 assume HI: "H \<subseteq> I"

398 from Iideal and HI

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

400 from this

401 show "Idl H \<subseteq> I"

402 unfolding genideal_def

403 by fast

404 qed

406 lemma (in ring) subset_Idl_subset:

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

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

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

410 proof -

411 from HI and genideal_self[OF Icarr]

412 have HIdlI: "H \<subseteq> Idl I" by fast

414 from Icarr

415 have Iideal: "ideal (Idl I) R" by (rule genideal_ideal)

416 from HI and Icarr

417 have "H \<subseteq> carrier R" by fast

418 from Iideal and this

419 have "(H \<subseteq> Idl I) = (Idl H \<subseteq> Idl I)"

420 by (rule Idl_subset_ideal[symmetric])

422 from HIdlI and this

423 show "Idl H \<subseteq> Idl I" by simp

424 qed

426 lemma (in ring) Idl_subset_ideal':

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

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

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

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

431 apply fast

432 done

434 lemma (in ring) genideal_zero:

435 "Idl {\<zero>} = {\<zero>}"

436 apply rule

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

438 apply (simp add: genideal_self')

439 done

441 lemma (in ring) genideal_one:

442 "Idl {\<one>} = carrier R"

443 proof -

444 interpret ideal "Idl {\<one>}" "R" by (rule genideal_ideal, fast intro: one_closed)

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

446 apply (rule, rule a_subset)

447 apply (simp add: one_imp_carrier genideal_self')

448 done

449 qed

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

454 definition

455 cgenideal :: "('a, 'b) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a set" ("PIdl\<index> _" [80] 79)

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

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

459 lemma (in cring) cgenideal_ideal:

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

461 shows "ideal (PIdl a) R"

462 apply (unfold cgenideal_def)

463 apply (rule idealI[OF is_ring])

464 apply (rule subgroup.intro)

465 apply (simp_all add: monoid_record_simps)

466 apply (blast intro: acarr m_closed)

467 apply clarsimp defer 1

468 defer 1

469 apply (fold a_inv_def, clarsimp) defer 1

470 apply clarsimp defer 1

471 apply clarsimp defer 1

472 proof -

473 fix x y

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

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

476 note carr = acarr xcarr ycarr

478 from carr

479 have "x \<otimes> a \<oplus> y \<otimes> a = (x \<oplus> y) \<otimes> a" by (simp add: l_distr)

480 from this and carr

481 show "\<exists>z. x \<otimes> a \<oplus> y \<otimes> a = z \<otimes> a \<and> z \<in> carrier R" by fast

482 next

483 from l_null[OF acarr, symmetric] and zero_closed

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

485 next

486 fix x

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

488 note carr = acarr xcarr

490 from carr

491 have "\<ominus> (x \<otimes> a) = (\<ominus> x) \<otimes> a" by (simp add: l_minus)

492 from this and carr

493 show "\<exists>z. \<ominus> (x \<otimes> a) = z \<otimes> a \<and> z \<in> carrier R" by fast

494 next

495 fix x y

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

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

498 note carr = acarr xcarr ycarr

500 from carr

501 have "y \<otimes> a \<otimes> x = (y \<otimes> x) \<otimes> a" by (simp add: m_assoc, simp add: m_comm)

502 from this and carr

503 show "\<exists>z. y \<otimes> a \<otimes> x = z \<otimes> a \<and> z \<in> carrier R" by fast

504 next

505 fix x y

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

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

508 note carr = acarr xcarr ycarr

510 from carr

511 have "x \<otimes> (y \<otimes> a) = (x \<otimes> y) \<otimes> a" by (simp add: m_assoc)

512 from this and carr

513 show "\<exists>z. x \<otimes> (y \<otimes> a) = z \<otimes> a \<and> z \<in> carrier R" by fast

514 qed

516 lemma (in ring) cgenideal_self:

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

518 shows "i \<in> PIdl i"

519 unfolding cgenideal_def

520 proof simp

521 from icarr

522 have "i = \<one> \<otimes> i" by simp

523 from this and icarr

524 show "\<exists>x. i = x \<otimes> i \<and> x \<in> carrier R" by fast

525 qed

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

529 lemma (in ring) cgenideal_minimal:

530 assumes "ideal J R"

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

532 shows "PIdl a \<subseteq> J"

533 proof -

534 interpret ideal J R by fact

535 show ?thesis unfolding cgenideal_def

536 apply rule

537 apply clarify

538 using aJ

539 apply (erule I_l_closed)

540 done

541 qed

543 lemma (in cring) cgenideal_eq_genideal:

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

545 shows "PIdl i = Idl {i}"

546 apply rule

547 apply (intro cgenideal_minimal)

548 apply (rule genideal_ideal, fast intro: icarr)

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

550 apply (intro genideal_minimal)

551 apply (rule cgenideal_ideal [OF icarr])

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

553 done

555 lemma (in cring) cgenideal_eq_rcos:

556 "PIdl i = carrier R #> i"

557 unfolding cgenideal_def r_coset_def

558 by fast

560 lemma (in cring) cgenideal_is_principalideal:

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

562 shows "principalideal (PIdl i) R"

563 apply (rule principalidealI)

564 apply (rule cgenideal_ideal [OF icarr])

565 proof -

566 from icarr

567 have "PIdl i = Idl {i}" by (rule cgenideal_eq_genideal)

568 from icarr and this

569 show "\<exists>i'\<in>carrier R. PIdl i = Idl {i'}" by fast

570 qed

573 subsection {* Union of Ideals *}

575 lemma (in ring) union_genideal:

576 assumes idealI: "ideal I R"

577 and idealJ: "ideal J R"

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

579 apply rule

580 apply (rule ring.genideal_minimal)

581 apply (rule is_ring)

582 apply (rule add_ideals[OF idealI idealJ])

583 apply (rule)

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

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

586 proof -

587 fix x

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

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

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

591 from ideal.Icarr[OF idealI xI]

592 have "x = x \<oplus> \<zero>" by algebra

593 from xI and ZJ and this

594 show "\<exists>h\<in>I. \<exists>k\<in>J. x = h \<oplus> k" by fast

595 next

596 fix x

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

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

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

600 from ideal.Icarr[OF idealJ xJ]

601 have "x = \<zero> \<oplus> x" by algebra

602 from ZI and xJ and this

603 show "\<exists>h\<in>I. \<exists>k\<in>J. x = h \<oplus> k" by fast

604 next

605 fix i j K

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

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

608 and idealK: "ideal K R"

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

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

611 from iI and IK

612 have iK: "i \<in> K" by fast

613 from jJ and JK

614 have jK: "j \<in> K" by fast

615 from iK and jK

616 show "i \<oplus> j \<in> K" by (intro additive_subgroup.a_closed) (rule ideal.axioms[OF idealK])

617 qed

620 subsection {* Properties of Principal Ideals *}

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

623 lemma (in ring) zero_genideal:

624 shows "Idl {\<zero>} = {\<zero>}"

625 apply rule

626 apply (simp add: genideal_minimal zeroideal)

627 apply (fast intro!: genideal_self)

628 done

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

631 lemma (in ring) one_genideal:

632 shows "Idl {\<one>} = carrier R"

633 proof -

634 have "\<one> \<in> Idl {\<one>}" by (simp add: genideal_self')

635 thus "Idl {\<one>} = carrier R" by (intro ideal.one_imp_carrier, fast intro: genideal_ideal)

636 qed

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

640 corollary (in ring) zeropideal:

641 shows "principalideal {\<zero>} R"

642 apply (rule principalidealI)

643 apply (rule zeroideal)

644 apply (blast intro!: zero_closed zero_genideal[symmetric])

645 done

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

648 corollary (in ring) onepideal:

649 shows "principalideal (carrier R) R"

650 apply (rule principalidealI)

651 apply (rule oneideal)

652 apply (blast intro!: one_closed one_genideal[symmetric])

653 done

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

657 lemma (in principalideal) rcos_generate:

658 assumes "cring R"

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

660 proof -

661 interpret cring R by fact

662 from generate

663 obtain i

664 where icarr: "i \<in> carrier R"

665 and I1: "I = Idl {i}"

666 by fast+

668 from icarr and genideal_self[of "{i}"]

669 have "i \<in> Idl {i}" by fast

670 hence iI: "i \<in> I" by (simp add: I1)

672 from I1 icarr

673 have I2: "I = PIdl i" by (simp add: cgenideal_eq_genideal)

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

676 unfolding cgenideal_def r_coset_def

677 by fast

679 from I2 and this

680 have "I = carrier R #> i" by simp

682 from iI and this

683 show "\<exists>x\<in>I. I = carrier R #> x" by fast

684 qed

687 subsection {* Prime Ideals *}

689 lemma (in ideal) primeidealCD:

690 assumes "cring R"

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

692 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)"

693 proof (rule ccontr, clarsimp)

694 interpret cring R by fact

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

696 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)"

697 hence 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" by simp

698 have "primeideal I R"

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

700 apply (rule primeideal_axioms.intro)

701 apply (rule InR)

702 apply (erule (2) I_prime)

703 done

704 from this and notprime

705 show "False" by simp

706 qed

708 lemma (in ideal) primeidealCE:

709 assumes "cring R"

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

711 obtains "carrier R = I"

712 | "\<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"

713 proof -

714 interpret R: cring R by fact

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

716 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"

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

718 qed

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

721 lemma (in cring) zeroprimeideal_domainI:

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

723 shows "domain R"

724 apply (rule domain.intro, rule is_cring)

725 apply (rule domain_axioms.intro)

726 proof (rule ccontr, simp)

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

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

729 hence "carrier R = {\<zero>}" by (rule one_zeroD)

730 from this[symmetric] and I_notcarr

731 show "False" by simp

732 next

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

734 fix a b

735 assume ab: "a \<otimes> b = \<zero>"

736 and carr: "a \<in> carrier R" "b \<in> carrier R"

737 from ab

738 have abI: "a \<otimes> b \<in> {\<zero>}" by fast

739 from carr and this

740 have "a \<in> {\<zero>} \<or> b \<in> {\<zero>}" by (rule I_prime)

741 thus "a = \<zero> \<or> b = \<zero>" by simp

742 qed

744 corollary (in cring) domain_eq_zeroprimeideal:

745 shows "domain R = primeideal {\<zero>} R"

746 apply rule

747 apply (erule domain.zeroprimeideal)

748 apply (erule zeroprimeideal_domainI)

749 done

752 subsection {* Maximal Ideals *}

754 lemma (in ideal) helper_I_closed:

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

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

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

758 proof -

759 from axI and carr

760 have "(a \<otimes> x) \<otimes> y \<in> I" by (simp add: I_r_closed)

761 also from carr

762 have "(a \<otimes> x) \<otimes> y = a \<otimes> (x \<otimes> y)" by (simp add: m_assoc)

763 finally

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

765 qed

767 lemma (in ideal) helper_max_prime:

768 assumes "cring R"

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

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

771 proof -

772 interpret cring R by fact

773 show ?thesis apply (rule idealI)

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

775 apply (rule subgroup.intro)

776 apply (simp, fast)

777 apply clarsimp apply (simp add: r_distr acarr)

778 apply (simp add: acarr)

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

780 apply clarsimp defer 1

781 apply (fast intro!: helper_I_closed acarr)

782 proof -

783 fix x

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

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

786 from ax and acarr xcarr

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

788 also from acarr xcarr

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

790 finally

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

792 from acarr

793 have "a \<otimes> \<zero> = \<zero>" by simp

794 next

795 fix x y

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

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

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

799 from ayI and acarr xcarr ycarr

800 have "a \<otimes> (y \<otimes> x) \<in> I" by (simp add: helper_I_closed)

801 moreover from xcarr ycarr

802 have "y \<otimes> x = x \<otimes> y" by (simp add: m_comm)

803 ultimately

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

805 qed

806 qed

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

809 lemma (in cring) maximalideal_is_prime:

810 assumes "maximalideal I R"

811 shows "primeideal I R"

812 proof -

813 interpret maximalideal I R by fact

814 show ?thesis apply (rule ccontr)

815 apply (rule primeidealCE)

816 apply (rule is_cring)

817 apply assumption

818 apply (simp add: I_notcarr)

819 proof -

820 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"

821 from this

822 obtain a b

823 where acarr: "a \<in> carrier R"

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

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

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

827 and bnI: "b \<notin> I"

828 by fast

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

831 from is_cring and acarr

832 have idealJ: "ideal J R" unfolding J_def by (rule helper_max_prime)

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

835 proof

836 fix x

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

838 from this and acarr

839 have "a \<otimes> x \<in> I" by (intro I_l_closed)

840 from xI[THEN a_Hcarr] this

841 show "x \<in> J" unfolding J_def by fast

842 qed

844 from abI and acarr bcarr

845 have "b \<in> J" unfolding J_def by fast

846 from bnI and this

847 have JnI: "J \<noteq> I" by fast

848 from acarr

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

850 from this and anI

851 have "a \<otimes> \<one> \<notin> I" by simp

852 from one_closed and this

853 have "\<one> \<notin> J" unfolding J_def by fast

854 hence Jncarr: "J \<noteq> carrier R" by fast

856 interpret ideal J R by (rule idealJ)

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

859 apply (intro I_maximal)

860 apply (rule idealJ)

861 apply (rule IsubJ)

862 apply (rule a_subset)

863 done

865 from this and JnI and Jncarr

866 show "False" by simp

867 qed

868 qed

870 subsection {* Derived Theorems *}

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

873 lemma (in cring) trivialideals_fieldI:

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

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

876 shows "field R"

877 apply (rule cring_fieldI)

878 apply (rule, rule, rule)

879 apply (erule Units_closed)

880 defer 1

881 apply rule

882 defer 1

883 proof (rule ccontr, simp)

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

885 hence a: "\<zero> \<otimes> inv \<zero> = \<one>" by (rule Units_r_inv)

886 from zUnit

887 have "\<zero> \<otimes> inv \<zero> = \<zero>" by (intro l_null, rule Units_inv_closed)

888 from a[symmetric] and this

889 have "\<one> = \<zero>" by simp

890 hence "carrier R = {\<zero>}" by (rule one_zeroD)

891 from this and carrnzero

892 show "False" by simp

893 next

894 fix x

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

896 hence xcarr: "x \<in> carrier R" by fast

897 from xcarr'

898 have xnZ: "x \<noteq> \<zero>" by fast

899 from xcarr

900 have xIdl: "ideal (PIdl x) R" by (intro cgenideal_ideal, fast)

902 from xcarr

903 have "x \<in> PIdl x" by (intro cgenideal_self, fast)

904 from this and xnZ

905 have "PIdl x \<noteq> {\<zero>}" by fast

906 from haveideals and this

907 have "PIdl x = carrier R"

908 by (blast intro!: xIdl)

909 hence "\<one> \<in> PIdl x" by simp

910 hence "\<exists>y. \<one> = y \<otimes> x \<and> y \<in> carrier R" unfolding cgenideal_def by blast

911 from this

912 obtain y

913 where ycarr: " y \<in> carrier R"

914 and ylinv: "\<one> = y \<otimes> x"

915 by fast+

916 from ylinv and xcarr ycarr

917 have yrinv: "\<one> = x \<otimes> y" by (simp add: m_comm)

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

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

920 from this and xcarr

921 show "x \<in> Units R"

922 unfolding Units_def

923 by fast

924 qed

926 lemma (in field) all_ideals:

927 shows "{I. ideal I R} = {{\<zero>}, carrier R}"

928 apply (rule, rule)

929 proof -

930 fix I

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

932 with this

933 interpret ideal I R by simp

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

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

937 assume "\<exists>a. a \<in> I - {\<zero>}"

938 from this

939 obtain a

940 where aI: "a \<in> I"

941 and anZ: "a \<noteq> \<zero>"

942 by fast+

943 from aI[THEN a_Hcarr] anZ

944 have aUnit: "a \<in> Units R" by (simp add: field_Units)

945 hence a: "a \<otimes> inv a = \<one>" by (rule Units_r_inv)

946 from aI and aUnit

947 have "a \<otimes> inv a \<in> I" by (simp add: I_r_closed del: Units_r_inv)

948 hence oneI: "\<one> \<in> I" by (simp add: a[symmetric])

950 have "carrier R \<subseteq> I"

951 proof

952 fix x

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

954 from oneI and this

955 have "\<one> \<otimes> x \<in> I" by (rule I_r_closed)

956 from this and xcarr

957 show "x \<in> I" by simp

958 qed

959 from this and a_subset

960 have "I = carrier R" by fast

961 thus "I \<in> {{\<zero>}, carrier R}" by fast

962 next

963 assume "\<not> (\<exists>a. a \<in> I - {\<zero>})"

964 hence IZ: "\<And>a. a \<in> I \<Longrightarrow> a = \<zero>" by simp

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

967 proof

968 fix x

969 assume "x \<in> I"

970 hence "x = \<zero>" by (rule IZ)

971 thus "x \<in> {\<zero>}" by fast

972 qed

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

975 hence "{\<zero>} \<subseteq> I" by fast

977 from this and a

978 have "I = {\<zero>}" by fast

979 thus "I \<in> {{\<zero>}, carrier R}" by fast

980 qed

981 qed (simp add: zeroideal oneideal)

983 --"Jacobson Theorem 2.2"

984 lemma (in cring) trivialideals_eq_field:

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

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

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

990 text {* Like zeroprimeideal for domains *}

991 lemma (in field) zeromaximalideal:

992 "maximalideal {\<zero>} R"

993 apply (rule maximalidealI)

994 apply (rule zeroideal)

995 proof-

996 from one_not_zero

997 have "\<one> \<notin> {\<zero>}" by simp

998 from this and one_closed

999 show "carrier R \<noteq> {\<zero>}" by fast

1000 next

1001 fix J

1002 assume Jideal: "ideal J R"

1003 hence "J \<in> {I. ideal I R}"

1004 by fast

1006 from this and all_ideals

1007 show "J = {\<zero>} \<or> J = carrier R" by simp

1008 qed

1010 lemma (in cring) zeromaximalideal_fieldI:

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

1012 shows "field R"

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

1014 apply rule apply clarsimp defer 1

1015 apply (simp add: zeroideal oneideal)

1016 proof -

1017 fix J

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

1019 and idealJ: "ideal J R"

1020 interpret ideal J R by (rule idealJ)

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

1022 from zeromax and idealJ and this and a_subset

1023 have "J = {\<zero>} \<or> J = carrier R" by (rule maximalideal.I_maximal)

1024 from this and Jn0

1025 show "J = carrier R" by simp

1026 qed

1028 lemma (in cring) zeromaximalideal_eq_field:

1029 "maximalideal {\<zero>} R = field R"

1030 apply rule

1031 apply (erule zeromaximalideal_fieldI)

1032 apply (erule field.zeromaximalideal)

1033 done

1035 end