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

src/HOL/Algebra/Ideal.thy

author | blanchet |

Tue Nov 07 15:16:42 2017 +0100 (21 months ago) | |

changeset 67022 | 49309fe530fd |

parent 63633 | 2accfb71e33b |

child 67443 | 3abf6a722518 |

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

more robust parsing for THF proofs (esp. polymorphic Leo-III 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 \<open>Ideals\<close>

11 subsection \<open>Definitions\<close>

13 subsubsection \<open>General definition\<close>

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) \<open>Ideals Generated by a Subset of @{term "carrier R"}\<close>

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 \<open>Principal Ideals\<close>

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 \<open>Maximal Ideals\<close>

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 \<open>Prime Ideals\<close>

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) 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 \<open>Special Ideals\<close>

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 \<open>General Ideal Properies\<close>

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 \<open>Intersection of Ideals\<close>

192 paragraph \<open>Intersection of two ideals\<close>

193 text \<open>The intersection of any two ideals is again an ideal in @{term R}\<close>

195 lemma (in ring) i_intersect:

196 assumes "ideal I R"

197 assumes "ideal J R"

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

199 proof -

200 interpret ideal I R by fact

201 interpret ideal J R by fact

202 show ?thesis

203 apply (intro idealI subgroup.intro)

204 apply (rule is_ring)

205 apply (force simp add: a_subset)

206 apply (simp add: a_inv_def[symmetric])

207 apply simp

208 apply (simp add: a_inv_def[symmetric])

209 apply (clarsimp, rule)

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

211 apply (clarsimp, rule)

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

213 done

214 qed

216 text \<open>The intersection of any Number of Ideals is again

217 an Ideal in @{term R}\<close>

218 lemma (in ring) i_Intersect:

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

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

221 shows "ideal (\<Inter>S) R"

222 apply (unfold_locales)

223 apply (simp_all add: Inter_eq)

224 apply rule unfolding mem_Collect_eq defer 1

225 apply rule defer 1

226 apply rule defer 1

227 apply (fold a_inv_def, rule) defer 1

228 apply rule defer 1

229 apply rule defer 1

230 proof -

231 fix x y

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

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

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

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

237 fix J

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

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

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

241 next

242 fix J

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

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

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

246 next

247 fix x

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

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

251 fix J

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

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

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

256 next

257 fix x y

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

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

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

262 fix J

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

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

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

267 next

268 fix x y

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

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

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

273 fix J

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

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

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

278 next

279 fix x

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

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

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

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

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

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

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

290 next

292 qed

295 subsection \<open>Addition of Ideals\<close>

297 lemma (in ring) add_ideals:

298 assumes idealI: "ideal I R"

299 and idealJ: "ideal J R"

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

301 apply (rule ideal.intro)

302 apply (rule add_additive_subgroups)

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

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

305 apply (rule is_ring)

306 apply (rule ideal_axioms.intro)

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

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

309 proof -

310 fix x i j

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

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

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

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

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

316 by algebra

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

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

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

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

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

322 by fast

323 next

324 fix x i j

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

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

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

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

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

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

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

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

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

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

335 by fast

336 qed

339 subsection (in ring) \<open>Ideals generated by a subset of @{term "carrier R"}\<close>

341 text \<open>@{term genideal} generates an ideal\<close>

342 lemma (in ring) genideal_ideal:

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

344 shows "ideal (Idl S) R"

345 unfolding genideal_def

346 proof (rule i_Intersect, fast, simp)

347 from oneideal and Scarr

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

349 qed

351 lemma (in ring) genideal_self:

352 assumes "S \<subseteq> carrier R"

353 shows "S \<subseteq> Idl S"

354 unfolding genideal_def by fast

356 lemma (in ring) genideal_self':

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

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

359 proof -

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

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

362 qed

364 text \<open>@{term genideal} generates the minimal ideal\<close>

365 lemma (in ring) genideal_minimal:

366 assumes a: "ideal I R"

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

368 shows "Idl S \<subseteq> I"

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

371 text \<open>Generated ideals and subsets\<close>

372 lemma (in ring) Idl_subset_ideal:

373 assumes Iideal: "ideal I R"

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

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

376 proof

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

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

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

380 next

381 fix x

382 assume "H \<subseteq> I"

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

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

385 qed

387 lemma (in ring) subset_Idl_subset:

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

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

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

391 proof -

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

393 by fast

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

396 by (rule genideal_ideal)

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

398 by fast

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

400 by (rule Idl_subset_ideal[symmetric])

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

403 qed

405 lemma (in ring) Idl_subset_ideal':

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

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

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

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

410 apply fast

411 done

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

414 apply rule

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

416 apply (simp add: genideal_self')

417 done

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

420 proof -

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

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

423 apply (rule, rule a_subset)

424 apply (simp add: one_imp_carrier genideal_self')

425 done

426 qed

429 text \<open>Generation of Principal Ideals in Commutative Rings\<close>

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

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

434 text \<open>genhideal (?) really generates an ideal\<close>

435 lemma (in cring) cgenideal_ideal:

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

437 shows "ideal (PIdl a) R"

438 apply (unfold cgenideal_def)

439 apply (rule idealI[OF is_ring])

440 apply (rule subgroup.intro)

441 apply simp_all

442 apply (blast intro: acarr)

443 apply clarsimp defer 1

444 defer 1

445 apply (fold a_inv_def, clarsimp) defer 1

446 apply clarsimp defer 1

447 apply clarsimp defer 1

448 proof -

449 fix x y

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

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

452 note carr = acarr xcarr ycarr

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

455 by (simp add: l_distr)

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

457 by fast

458 next

459 from l_null[OF acarr, symmetric] and zero_closed

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

461 next

462 fix x

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

464 note carr = acarr xcarr

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

467 by (simp add: l_minus)

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

469 by fast

470 next

471 fix x y

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

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

474 note carr = acarr xcarr ycarr

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

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

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

479 by fast

480 next

481 fix x y

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

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

484 note carr = acarr xcarr ycarr

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

487 by (simp add: m_assoc)

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

489 by fast

490 qed

492 lemma (in ring) cgenideal_self:

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

494 shows "i \<in> PIdl i"

495 unfolding cgenideal_def

496 proof simp

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

498 by simp

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

500 by fast

501 qed

503 text \<open>@{const "cgenideal"} is minimal\<close>

505 lemma (in ring) cgenideal_minimal:

506 assumes "ideal J R"

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

508 shows "PIdl a \<subseteq> J"

509 proof -

510 interpret ideal J R by fact

511 show ?thesis

512 unfolding cgenideal_def

513 apply rule

514 apply clarify

515 using aJ

516 apply (erule I_l_closed)

517 done

518 qed

520 lemma (in cring) cgenideal_eq_genideal:

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

522 shows "PIdl i = Idl {i}"

523 apply rule

524 apply (intro cgenideal_minimal)

525 apply (rule genideal_ideal, fast intro: icarr)

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

527 apply (intro genideal_minimal)

528 apply (rule cgenideal_ideal [OF icarr])

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

530 done

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

533 unfolding cgenideal_def r_coset_def by fast

535 lemma (in cring) cgenideal_is_principalideal:

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

537 shows "principalideal (PIdl i) R"

538 apply (rule principalidealI)

539 apply (rule cgenideal_ideal [OF icarr])

540 proof -

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

542 by (rule cgenideal_eq_genideal)

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

544 by fast

545 qed

548 subsection \<open>Union of Ideals\<close>

550 lemma (in ring) union_genideal:

551 assumes idealI: "ideal I R"

552 and idealJ: "ideal J R"

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

554 apply rule

555 apply (rule ring.genideal_minimal)

556 apply (rule is_ring)

557 apply (rule add_ideals[OF idealI idealJ])

558 apply (rule)

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

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

561 proof -

562 fix x

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

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

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

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

567 by algebra

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

569 by fast

570 next

571 fix x

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

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

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

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

576 by algebra

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

578 by fast

579 next

580 fix i j K

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

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

583 and idealK: "ideal K R"

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

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

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

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

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

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

590 qed

593 subsection \<open>Properties of Principal Ideals\<close>

595 text \<open>\<open>\<zero>\<close> generates the zero ideal\<close>

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

597 apply rule

598 apply (simp add: genideal_minimal zeroideal)

599 apply (fast intro!: genideal_self)

600 done

602 text \<open>\<open>\<one>\<close> generates the unit ideal\<close>

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

604 proof -

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

606 by (simp add: genideal_self')

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

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

609 qed

612 text \<open>The zero ideal is a principal ideal\<close>

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

614 apply (rule principalidealI)

615 apply (rule zeroideal)

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

617 done

619 text \<open>The unit ideal is a principal ideal\<close>

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

621 apply (rule principalidealI)

622 apply (rule oneideal)

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

624 done

627 text \<open>Every principal ideal is a right coset of the carrier\<close>

628 lemma (in principalideal) rcos_generate:

629 assumes "cring R"

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

631 proof -

632 interpret cring R by fact

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

634 by fast+

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

637 by fast

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

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

641 by (simp add: cgenideal_eq_genideal)

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

644 unfolding cgenideal_def r_coset_def by fast

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

647 by simp

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

650 by fast

651 qed

654 subsection \<open>Prime Ideals\<close>

656 lemma (in ideal) primeidealCD:

657 assumes "cring R"

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

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

660 proof (rule ccontr, clarsimp)

661 interpret cring R by fact

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

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

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

665 by simp

666 have "primeideal I R"

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

668 apply (rule primeideal_axioms.intro)

669 apply (rule InR)

670 apply (erule (2) I_prime)

671 done

672 with notprime show False by simp

673 qed

675 lemma (in ideal) primeidealCE:

676 assumes "cring R"

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

678 obtains "carrier R = I"

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

680 proof -

681 interpret R: cring R by fact

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

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

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

685 qed

687 text \<open>If \<open>{\<zero>}\<close> is a prime ideal of a commutative ring, the ring is a domain\<close>

688 lemma (in cring) zeroprimeideal_domainI:

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

690 shows "domain R"

691 apply (rule domain.intro, rule is_cring)

692 apply (rule domain_axioms.intro)

693 proof (rule ccontr, simp)

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

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

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

697 from this[symmetric] and I_notcarr show False

698 by simp

699 next

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

701 fix a b

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

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

704 by fast

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

706 by (rule I_prime)

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

708 qed

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

711 apply rule

712 apply (erule domain.zeroprimeideal)

713 apply (erule zeroprimeideal_domainI)

714 done

717 subsection \<open>Maximal Ideals\<close>

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 have "(a \<otimes> x) \<otimes> y \<in> I"

725 by (simp add: I_r_closed)

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

727 by (simp add: m_assoc)

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

729 qed

731 lemma (in ideal) helper_max_prime:

732 assumes "cring R"

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

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

735 proof -

736 interpret cring R by fact

737 show ?thesis apply (rule idealI)

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

739 apply (rule subgroup.intro)

740 apply (simp, fast)

741 apply clarsimp apply (simp add: r_distr acarr)

742 apply (simp add: acarr)

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

744 apply clarsimp defer 1

745 apply (fast intro!: helper_I_closed acarr)

746 proof -

747 fix x

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

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

750 from ax and acarr xcarr

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

752 also from acarr xcarr

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

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

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

756 next

757 fix x y

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

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

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

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

762 by (simp add: helper_I_closed)

763 moreover

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

765 by (simp add: m_comm)

766 ultimately

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

768 qed

769 qed

771 text \<open>In a cring every maximal ideal is prime\<close>

772 lemma (in cring) maximalideal_prime:

773 assumes "maximalideal I R"

774 shows "primeideal I R"

775 proof -

776 interpret maximalideal I R by fact

777 show ?thesis apply (rule ccontr)

778 apply (rule primeidealCE)

779 apply (rule is_cring)

780 apply assumption

781 apply (simp add: I_notcarr)

782 proof -

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

784 then obtain a b where

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

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

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

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

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

790 define J where "J = {x\<in>carrier R. a \<otimes> x \<in> I}"

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

793 unfolding J_def by (rule helper_max_prime)

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

796 proof

797 fix x

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

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

800 by (intro I_l_closed)

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

802 unfolding J_def by fast

803 qed

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

806 unfolding J_def by fast

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

808 from acarr

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

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

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

812 unfolding J_def by fast

813 then have 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 with JnI and Jncarr show False by simp

825 qed

826 qed

829 subsection \<open>Derived Theorems\<close>

831 \<comment>"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 then have a: "\<zero> \<otimes> inv \<zero> = \<one>" by (rule Units_r_inv)

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

846 by (intro l_null) (rule Units_inv_closed)

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

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

849 with carrnzero show False by simp

850 next

851 fix x

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

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

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

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

856 by (intro cgenideal_ideal) fast

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

859 by (intro cgenideal_self) fast

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

861 with haveideals have "PIdl x = carrier R"

862 by (blast intro!: xIdl)

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

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

865 unfolding cgenideal_def by blast

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

867 by fast+

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

869 by (simp add: m_comm)

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

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

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

873 unfolding Units_def by fast

874 qed

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

877 apply (rule, rule)

878 proof -

879 fix I

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

881 then interpret ideal I R by simp

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

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

885 case True

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

887 by fast+

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

889 by (simp add: field_Units)

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

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

892 by (simp add: I_r_closed del: Units_r_inv)

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

895 have "carrier R \<subseteq> I"

896 proof

897 fix x

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

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

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

901 qed

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

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

904 next

905 case False

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

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

909 proof

910 fix x

911 assume "x \<in> I"

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

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

914 qed

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

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

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

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

921 qed

922 qed (simp add: zeroideal oneideal)

924 \<comment>"Jacobson Theorem 2.2"

925 lemma (in cring) trivialideals_eq_field:

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

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

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

931 text \<open>Like zeroprimeideal for domains\<close>

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

933 apply (rule maximalidealI)

934 apply (rule zeroideal)

935 proof-

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

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

938 next

939 fix J

940 assume Jideal: "ideal J R"

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

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

943 by simp

944 qed

946 lemma (in cring) zeromaximalideal_fieldI:

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

948 shows "field R"

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

950 apply rule apply clarsimp defer 1

951 apply (simp add: zeroideal oneideal)

952 proof -

953 fix J

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

955 and idealJ: "ideal J R"

956 interpret ideal J R by (rule idealJ)

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

958 from zeromax and idealJ and this and a_subset

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

960 by (rule maximalideal.I_maximal)

961 with Jn0 show "J = carrier R"

962 by simp

963 qed

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

966 apply rule

967 apply (erule zeromaximalideal_fieldI)

968 apply (erule field.zeromaximalideal)

969 done

971 end