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

src/HOL/Algebra/Ideal.thy

author | haftmann |

Fri Apr 20 11:21:42 2007 +0200 (2007-04-20) | |

changeset 22744 | 5cbe966d67a2 |

parent 20318 | 0e0ea63fe768 |

child 23350 | 50c5b0912a0c |

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

Isar definitions are now added explicitly to code theorem table

1 (*

2 Title: HOL/Algebra/CIdeal.thy

3 Id: $Id$

4 Author: Stephan Hohe, TU Muenchen

5 *)

7 theory Ideal

8 imports Ring AbelCoset

9 begin

11 section {* Ideals *}

13 subsection {* General definition *}

15 locale ideal = additive_subgroup I R + ring R +

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 interpretation ideal \<subseteq> abelian_subgroup I R

20 apply (intro abelian_subgroupI3 abelian_group.intro)

21 apply (rule ideal.axioms, assumption)

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

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

24 done

26 lemma (in ideal) is_ideal:

27 "ideal I R"

28 by -

30 lemma idealI:

31 includes ring

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 by (intro ideal.intro ideal_axioms.intro additive_subgroupI, assumption+)

39 subsection {* Ideals Generated by a Subset of @{term [locale=ring] "carrier R"} *}

41 constdefs (structure R)

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

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

46 subsection {* Principal Ideals *}

48 locale principalideal = ideal +

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

51 lemma (in principalideal) is_principalideal:

52 shows "principalideal I R"

53 by -

55 lemma principalidealI:

56 includes ideal

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

58 shows "principalideal I R"

59 by (intro principalideal.intro principalideal_axioms.intro, assumption+)

62 subsection {* Maximal Ideals *}

64 locale maximalideal = ideal +

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

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

68 lemma (in maximalideal) is_maximalideal:

69 shows "maximalideal I R"

70 by -

72 lemma maximalidealI:

73 includes ideal

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

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

76 shows "maximalideal I R"

77 by (intro maximalideal.intro maximalideal_axioms.intro, assumption+)

80 subsection {* Prime Ideals *}

82 locale primeideal = ideal + cring +

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

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

86 lemma (in primeideal) is_primeideal:

87 shows "primeideal I R"

88 by -

90 lemma primeidealI:

91 includes ideal

92 includes cring

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

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

95 shows "primeideal I R"

96 by (intro primeideal.intro primeideal_axioms.intro, assumption+)

98 lemma primeidealI2:

99 includes additive_subgroup I R

100 includes cring

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

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

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

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

105 shows "primeideal I R"

106 apply (intro_locales)

107 apply (intro ideal_axioms.intro, assumption+)

108 apply (intro primeideal_axioms.intro, assumption+)

109 done

112 section {* Properties of Ideals *}

114 subsection {* Special Ideals *}

116 lemma (in ring) zeroideal:

117 shows "ideal {\<zero>} R"

118 apply (intro idealI subgroup.intro)

119 apply (rule is_ring)

120 apply simp+

121 apply (fold a_inv_def, simp)

122 apply simp+

123 done

125 lemma (in ring) oneideal:

126 shows "ideal (carrier R) R"

127 apply (intro idealI subgroup.intro)

128 apply (rule is_ring)

129 apply simp+

130 apply (fold a_inv_def, simp)

131 apply simp+

132 done

134 lemma (in "domain") zeroprimeideal:

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

136 apply (intro primeidealI)

137 apply (rule zeroideal)

138 apply (rule domain.axioms,assumption)

139 defer 1

140 apply (simp add: integral)

141 proof (rule ccontr, simp)

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

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

144 from this and one_not_zero

145 show "False" by simp

146 qed

149 subsection {* General Ideal Properies *}

151 lemma (in ideal) one_imp_carrier:

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

153 shows "I = carrier R"

154 apply (rule)

155 apply (rule)

156 apply (rule a_Hcarr, simp)

157 proof

158 fix x

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

160 from I_one_closed and this

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

162 from this and xcarr

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

164 qed

166 lemma (in ideal) Icarr:

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

168 shows "i \<in> carrier R"

169 by (rule a_Hcarr)

172 subsection {* Intersection of Ideals *}

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

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

176 lemma (in ring) i_intersect:

177 includes ideal I R

178 includes ideal J R

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

180 apply (intro idealI subgroup.intro)

181 apply (rule is_ring)

182 apply (force simp add: a_subset)

183 apply (simp add: a_inv_def[symmetric])

184 apply simp

185 apply (simp add: a_inv_def[symmetric])

186 apply (clarsimp, rule)

187 apply (fast intro: ideal.I_l_closed ideal.intro prems)+

188 apply (clarsimp, rule)

189 apply (fast intro: ideal.I_r_closed ideal.intro prems)+

190 done

193 subsubsection {* Intersection of a Set of Ideals *}

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

196 an Ideal in @{term R} *}

197 lemma (in ring) i_Intersect:

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

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

200 shows "ideal (Inter S) R"

201 apply (unfold_locales)

202 apply (simp_all add: Inter_def INTER_def)

203 apply (rule, simp) defer 1

204 apply rule defer 1

205 apply rule defer 1

206 apply (fold a_inv_def, rule) defer 1

207 apply rule defer 1

208 apply rule defer 1

209 proof -

210 fix x

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

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

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

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

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

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

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

221 next

222 fix x y

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

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

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

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

228 fix J

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

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

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

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

233 next

234 fix J

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

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

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

238 next

239 fix x

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

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

243 fix J

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

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

247 from xI[OF JS]

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

249 next

250 fix x y

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

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

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

255 fix J

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

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

259 from xI[OF JS] and ycarr

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

261 next

262 fix x y

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

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

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

267 fix J

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

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

271 from xI[OF JS] and ycarr

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

273 qed

276 subsection {* Addition of Ideals *}

278 lemma (in ring) add_ideals:

279 assumes idealI: "ideal I R"

280 and idealJ: "ideal J R"

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

282 apply (rule ideal.intro)

283 apply (rule add_additive_subgroups)

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

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

286 apply assumption

287 apply (rule ideal_axioms.intro)

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

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

290 proof -

291 fix x i j

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

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

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

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

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

297 from xcarr and iI

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

299 from xcarr and jJ

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

301 from a b c

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

303 next

304 fix x i j

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

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

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

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

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

310 from xcarr and iI

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

312 from xcarr and jJ

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

314 from a b c

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

316 qed

319 subsection {* Ideals generated by a subset of @{term [locale=ring]

320 "carrier R"} *}

322 subsubsection {* Generation of Ideals in General Rings *}

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

325 lemma (in ring) genideal_ideal:

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

327 shows "ideal (Idl S) R"

328 unfolding genideal_def

329 proof (rule i_Intersect, fast, simp)

330 from oneideal and Scarr

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

332 qed

334 lemma (in ring) genideal_self:

335 assumes "S \<subseteq> carrier R"

336 shows "S \<subseteq> Idl S"

337 unfolding genideal_def

338 by fast

340 lemma (in ring) genideal_self':

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

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

343 proof -

344 from carr

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

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

347 qed

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

350 lemma (in ring) genideal_minimal:

351 assumes a: "ideal I R"

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

353 shows "Idl S \<subseteq> I"

354 unfolding genideal_def

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

357 text {* Generated ideals and subsets *}

358 lemma (in ring) Idl_subset_ideal:

359 assumes Iideal: "ideal I R"

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

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

362 proof

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

364 have "H \<subseteq> Idl H" by (rule genideal_self)

365 from this and a

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

367 next

368 fix x

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

371 from Iideal and HI

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

373 from this

374 show "Idl H \<subseteq> I"

375 unfolding genideal_def

376 by fast

377 qed

379 lemma (in ring) subset_Idl_subset:

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

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

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

383 proof -

384 from HI and genideal_self[OF Icarr]

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

387 from Icarr

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

389 from HI and Icarr

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

391 from Iideal and this

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

393 by (rule Idl_subset_ideal[symmetric])

395 from HIdlI and this

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

397 qed

399 lemma (in ring) Idl_subset_ideal':

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

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

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

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

404 apply fast

405 done

407 lemma (in ring) genideal_zero:

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

409 apply rule

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

411 apply (simp add: genideal_self')

412 done

414 lemma (in ring) genideal_one:

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

416 proof -

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

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

419 apply (rule, rule a_subset)

420 apply (simp add: one_imp_carrier genideal_self')

421 done

422 qed

425 subsubsection {* Generation of Principal Ideals in Commutative Rings *}

427 constdefs (structure R)

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

429 "cgenideal R a \<equiv> { x \<otimes> a | x. x \<in> carrier R }"

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

432 lemma (in cring) cgenideal_ideal:

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

434 shows "ideal (PIdl a) R"

435 apply (unfold cgenideal_def)

436 apply (rule idealI[OF is_ring])

437 apply (rule subgroup.intro)

438 apply (simp_all add: monoid_record_simps)

439 apply (blast intro: acarr m_closed)

440 apply clarsimp defer 1

441 defer 1

442 apply (fold a_inv_def, clarsimp) defer 1

443 apply clarsimp defer 1

444 apply clarsimp defer 1

445 proof -

446 fix x y

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

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

449 note carr = acarr xcarr ycarr

451 from carr

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

453 from this and carr

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

455 next

456 from l_null[OF acarr, symmetric] and zero_closed

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

458 next

459 fix x

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

461 note carr = acarr xcarr

463 from carr

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

465 from this and carr

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

467 next

468 fix x y

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

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

471 note carr = acarr xcarr ycarr

473 from carr

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

475 from this and carr

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

477 next

478 fix x y

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

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

481 note carr = acarr xcarr ycarr

483 from carr

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

485 from this and carr

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

487 qed

489 lemma (in ring) cgenideal_self:

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

491 shows "i \<in> PIdl i"

492 unfolding cgenideal_def

493 proof simp

494 from icarr

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

496 from this and icarr

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

498 qed

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

502 lemma (in ring) cgenideal_minimal:

503 includes ideal J R

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

505 shows "PIdl a \<subseteq> J"

506 unfolding cgenideal_def

507 by (rule, clarify, rule I_l_closed)

510 lemma (in cring) cgenideal_eq_genideal:

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

512 shows "PIdl i = Idl {i}"

513 apply rule

514 apply (intro cgenideal_minimal)

515 apply (rule genideal_ideal, fast intro: icarr)

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

517 apply (intro genideal_minimal)

518 apply (rule cgenideal_ideal, assumption)

519 apply (simp, rule cgenideal_self, assumption)

520 done

522 lemma (in cring) cgenideal_eq_rcos:

523 "PIdl i = carrier R #> i"

524 unfolding cgenideal_def r_coset_def

525 by fast

527 lemma (in cring) cgenideal_is_principalideal:

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

529 shows "principalideal (PIdl i) R"

530 apply (rule principalidealI)

531 apply (rule cgenideal_ideal, assumption)

532 proof -

533 from icarr

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

535 from icarr and this

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

537 qed

540 subsection {* Union of Ideals *}

542 lemma (in ring) union_genideal:

543 assumes idealI: "ideal I R"

544 and idealJ: "ideal J R"

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

546 apply rule

547 apply (rule ring.genideal_minimal)

548 apply assumption

549 apply (rule add_ideals[OF idealI idealJ])

550 apply (rule)

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

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

553 proof -

554 fix x

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

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

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

558 from ideal.Icarr[OF idealI xI]

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

560 from xI and ZJ and this

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

562 next

563 fix x

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

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

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

567 from ideal.Icarr[OF idealJ xJ]

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

569 from ZI and xJ and this

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

571 next

572 fix i j K

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

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

575 and idealK: "ideal K R"

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

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

578 from iI and IK

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

580 from jJ and JK

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

582 from iK and jK

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

584 qed

587 subsection {* Properties of Principal Ideals *}

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

590 lemma (in ring) zero_genideal:

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

592 apply rule

593 apply (simp add: genideal_minimal zeroideal)

594 apply (fast intro!: genideal_self)

595 done

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

598 lemma (in ring) one_genideal:

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

600 proof -

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

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

603 qed

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

607 corollary (in ring) zeropideal:

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

609 apply (rule principalidealI)

610 apply (rule zeroideal)

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

612 done

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

615 corollary (in ring) onepideal:

616 shows "principalideal (carrier R) R"

617 apply (rule principalidealI)

618 apply (rule oneideal)

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

620 done

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

624 lemma (in principalideal) rcos_generate:

625 includes cring

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

627 proof -

628 from generate

629 obtain i

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

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

632 by fast+

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

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

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

638 from I1 icarr

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

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

642 unfolding cgenideal_def r_coset_def

643 by fast

645 from I2 and this

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

648 from iI and this

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

650 qed

653 subsection {* Prime Ideals *}

655 lemma (in ideal) primeidealCD:

656 includes cring

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 assume InR: "carrier R \<noteq> I"

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

662 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

663 have "primeideal I R"

664 apply (rule primeideal.intro, assumption+)

665 by (rule primeideal_axioms.intro, rule InR, erule I_prime)

666 from this and notprime

667 show "False" by simp

668 qed

670 lemma (in ideal) primeidealCE:

671 includes cring

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

673 and elim1: "carrier R = I \<Longrightarrow> P"

674 and elim2: "(\<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> P"

675 shows "P"

676 proof -

677 from notprime

678 have "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)"

679 by (intro primeidealCD)

680 thus "P"

681 apply (rule disjE)

682 by (erule elim1, erule elim2)

683 qed

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

686 lemma (in cring) zeroprimeideal_domainI:

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

688 shows "domain R"

689 apply (rule domain.intro, assumption+)

690 apply (rule domain_axioms.intro)

691 proof (rule ccontr, simp)

692 interpret primeideal ["{\<zero>}" "R"] by (rule pi)

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

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

695 from this[symmetric] and I_notcarr

696 show "False" by simp

697 next

698 interpret primeideal ["{\<zero>}" "R"] by (rule pi)

699 fix a b

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

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

702 from ab

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

704 from carr and this

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

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

707 qed

709 corollary (in cring) domain_eq_zeroprimeideal:

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

711 apply rule

712 apply (erule domain.zeroprimeideal)

713 apply (erule zeroprimeideal_domainI)

714 done

717 subsection {* Maximal Ideals *}

719 lemma (in ideal) helper_I_closed:

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

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

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

723 proof -

724 from axI and carr

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

726 also from carr

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

728 finally

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

730 qed

732 lemma (in ideal) helper_max_prime:

733 includes cring

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

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

736 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

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

755 from acarr

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

757 next

758 fix x y

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

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

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

762 from ayI and acarr xcarr ycarr

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

764 moreover from xcarr ycarr

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

766 ultimately

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

768 qed

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

771 lemma (in cring) maximalideal_is_prime:

772 includes maximalideal

773 shows "primeideal I R"

774 apply (rule ccontr)

775 apply (rule primeidealCE)

776 apply assumption+

777 apply (simp add: I_notcarr)

778 proof -

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

780 from this

781 obtain a b

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

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

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

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

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

787 by fast

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

790 from acarr

791 have idealJ: "ideal J R" by (unfold J_def, intro helper_max_prime)

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

794 proof

795 fix x

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

797 from this and acarr

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

799 from xI[THEN a_Hcarr] this

800 show "x \<in> J" by (unfold J_def, fast)

801 qed

803 from abI and acarr bcarr

804 have "b \<in> J" by (unfold J_def, fast)

805 from bnI and this

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

807 from acarr

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

809 from this and anI

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

811 from one_closed and this

812 have "\<one> \<notin> J" by (unfold J_def, fast)

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

815 interpret ideal ["J" "R"] by (rule idealJ)

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

818 apply (intro I_maximal)

819 apply (rule idealJ)

820 apply (rule IsubJ)

821 apply (rule a_subset)

822 done

824 from this and JnI and Jncarr

825 show "False" by simp

826 qed

829 subsection {* Derived Theorems Involving Ideals *}

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

832 lemma (in cring) trivialideals_fieldI:

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

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

835 shows "field R"

836 apply (rule cring_fieldI)

837 apply (rule, rule, rule)

838 apply (erule Units_closed)

839 defer 1

840 apply rule

841 defer 1

842 proof (rule ccontr, simp)

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

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

845 from zUnit

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

847 from a[symmetric] and this

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

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

850 from this and carrnzero

851 show "False" by simp

852 next

853 fix x

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

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

856 from xcarr'

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

858 from xcarr

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

861 from xcarr

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

863 from this and xnZ

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

865 from haveideals and this

866 have "PIdl x = carrier R"

867 by (blast intro!: xIdl)

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

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

870 from this

871 obtain y

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

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

874 by fast+

875 from ylinv and xcarr ycarr

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

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

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

879 from this and xcarr

880 show "x \<in> Units R"

881 unfolding Units_def

882 by fast

883 qed

885 lemma (in field) all_ideals:

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

887 apply (rule, rule)

888 proof -

889 fix I

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

891 with this

892 interpret ideal ["I" "R"] by simp

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

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

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

897 from this

898 obtain a

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

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

901 by fast+

902 from aI[THEN a_Hcarr] anZ

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

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

905 from aI and aUnit

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

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

909 have "carrier R \<subseteq> I"

910 proof

911 fix x

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

913 from oneI and this

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

915 from this and xcarr

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

917 qed

918 from this and a_subset

919 have "I = carrier R" by fast

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

921 next

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

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

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

926 proof

927 fix x

928 assume "x \<in> I"

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

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

931 qed

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

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

936 from this and a

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

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

939 qed

940 qed (simp add: zeroideal oneideal)

942 --"Jacobson Theorem 2.2"

943 lemma (in cring) trivialideals_eq_field:

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

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

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

949 text {* Like zeroprimeideal for domains *}

950 lemma (in field) zeromaximalideal:

951 "maximalideal {\<zero>} R"

952 apply (rule maximalidealI)

953 apply (rule zeroideal)

954 proof-

955 from one_not_zero

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

957 from this and one_closed

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

959 next

960 fix J

961 assume Jideal: "ideal J R"

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

963 by fast

965 from this and all_ideals

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

967 qed

969 lemma (in cring) zeromaximalideal_fieldI:

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

971 shows "field R"

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

973 apply rule apply clarsimp defer 1

974 apply (simp add: zeroideal oneideal)

975 proof -

976 fix J

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

978 and idealJ: "ideal J R"

979 interpret ideal ["J" "R"] by (rule idealJ)

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

981 from zeromax and idealJ and this and a_subset

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

983 from this and Jn0

984 show "J = carrier R" by simp

985 qed

987 lemma (in cring) zeromaximalideal_eq_field:

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

989 apply rule

990 apply (erule zeromaximalideal_fieldI)

991 apply (erule field.zeromaximalideal)

992 done

994 end