-
Notifications
You must be signed in to change notification settings - Fork 0
/
Ideal_Product.thy
588 lines (541 loc) · 25.7 KB
/
Ideal_Product.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
(* Title: HOL/Algebra/Ideal_Product.thy
Author: Paulo Emílio de Vilhena
*)
theory Ideal_Product
imports Ideal
begin
section \<open>Product of Ideals\<close>
text \<open>In this section, we study the structure of the set of ideals of a given ring.\<close>
inductive_set
ideal_prod :: "[ ('a, 'b) ring_scheme, 'a set, 'a set ] \<Rightarrow> 'a set" (infixl "\<cdot>\<index>" 80)
for R and I and J (* both I and J are supposed ideals *) where
prod: "\<lbrakk> i \<in> I; j \<in> J \<rbrakk> \<Longrightarrow> i \<otimes>\<^bsub>R\<^esub> j \<in> ideal_prod R I J"
| sum: "\<lbrakk> s1 \<in> ideal_prod R I J; s2 \<in> ideal_prod R I J \<rbrakk> \<Longrightarrow> s1 \<oplus>\<^bsub>R\<^esub> s2 \<in> ideal_prod R I J"
definition ideals_set :: "('a, 'b) ring_scheme \<Rightarrow> ('a set) ring"
where "ideals_set R = \<lparr> carrier = { I. ideal I R },
mult = ideal_prod R,
one = carrier R,
zero = { \<zero>\<^bsub>R\<^esub> },
add = set_add R \<rparr>"
subsection \<open>Basic Properties\<close>
lemma (in ring) ideal_prod_in_carrier:
assumes "ideal I R" "ideal J R"
shows "I \<cdot> J \<subseteq> carrier R"
proof
fix s assume "s \<in> I \<cdot> J" thus "s \<in> carrier R"
by (induct s rule: ideal_prod.induct) (auto, meson assms ideal.I_l_closed ideal.Icarr)
qed
lemma (in ring) ideal_prod_inter:
assumes "ideal I R" "ideal J R"
shows "I \<cdot> J \<subseteq> I \<inter> J"
proof
fix s assume "s \<in> I \<cdot> J" thus "s \<in> I \<inter> J"
apply (induct s rule: ideal_prod.induct)
apply (auto, (meson assms ideal.I_r_closed ideal.I_l_closed ideal.Icarr)+)
apply (simp_all add: additive_subgroup.a_closed assms ideal.axioms(1))
done
qed
lemma (in ring) ideal_prod_is_ideal:
assumes "ideal I R" "ideal J R"
shows "ideal (I \<cdot> J) R"
proof (rule idealI)
show "ring R" using ring_axioms .
next
show "subgroup (I \<cdot> J) (add_monoid R)"
unfolding subgroup_def
proof (auto)
show "\<zero> \<in> I \<cdot> J" using ideal_prod.prod[of \<zero> I \<zero> J R]
by (simp add: additive_subgroup.zero_closed assms ideal.axioms(1))
next
fix s1 s2 assume s1: "s1 \<in> I \<cdot> J" and s2: "s2 \<in> I \<cdot> J"
show "s1 \<in> carrier R" using ideal_prod_in_carrier[OF assms] s1 by blast
show "s1 \<oplus> s2 \<in> I \<cdot> J" by (simp add: ideal_prod.sum[OF s1 s2])
show "inv\<^bsub>add_monoid R\<^esub> s1 \<in> I \<cdot> J" using s1
proof (induct s1 rule: ideal_prod.induct)
case (prod i j)
hence "inv\<^bsub>add_monoid R\<^esub> (i \<otimes> j) = (inv\<^bsub>add_monoid R\<^esub> i) \<otimes> j"
by (metis a_inv_def assms(1) assms(2) ideal.Icarr l_minus)
thus ?case using ideal_prod.prod[of "inv\<^bsub>add_monoid R\<^esub> i" I j J R] assms
by (simp add: additive_subgroup.a_subgroup ideal.axioms(1) prod.hyps subgroup.m_inv_closed)
next
case (sum s1 s2) thus ?case
by (smt a_inv_def add.inv_mult_group contra_subsetD
assms ideal_prod.sum ideal_prod_in_carrier)
qed
qed
next
fix s x assume s: "s \<in> I \<cdot> J" and x: "x \<in> carrier R"
show "x \<otimes> s \<in> I \<cdot> J" using s
proof (induct s rule: ideal_prod.induct)
case (prod i j) thus ?case using ideal_prod.prod[of "x \<otimes> i" I j J R] assms
by (simp add: x ideal.I_l_closed ideal.Icarr m_assoc)
next
case (sum s1 s2) thus ?case
by (smt assms contra_subsetD ideal_prod.sum ideal_prod_in_carrier r_distr x)
qed
show "s \<otimes> x \<in> I \<cdot> J" using s
proof (induct s rule: ideal_prod.induct)
case (prod i j) thus ?case using ideal_prod.prod[of i I "j \<otimes> x" J R] assms x
by (simp add: x ideal.I_r_closed ideal.Icarr m_assoc)
next
case (sum s1 s2) thus ?case
by (smt assms contra_subsetD ideal_prod.sum ideal_prod_in_carrier l_distr x)
qed
qed
lemma (in ring) ideal_prod_eq_genideal:
assumes "ideal I R" "ideal J R"
shows "I \<cdot> J = Idl (I <#> J)"
proof
have "I <#> J \<subseteq> I \<cdot> J"
proof
fix s assume "s \<in> I <#> J"
then obtain i j where "i \<in> I" "j \<in> J" "s = i \<otimes> j"
unfolding set_mult_def by blast
thus "s \<in> I \<cdot> J" using ideal_prod.prod by simp
qed
thus "Idl (I <#> J) \<subseteq> I \<cdot> J"
unfolding genideal_def using ideal_prod_is_ideal[OF assms] by blast
next
show "I \<cdot> J \<subseteq> Idl (I <#> J)"
proof
fix s assume "s \<in> I \<cdot> J" thus "s \<in> Idl (I <#> J)"
proof (induct s rule: ideal_prod.induct)
case (prod i j) hence "i \<otimes> j \<in> I <#> J" unfolding set_mult_def by blast
thus ?case unfolding genideal_def by blast
next
case (sum s1 s2) thus ?case
by (simp add: additive_subgroup.a_closed additive_subgroup.a_subset
assms genideal_ideal ideal.axioms(1) set_mult_closed)
qed
qed
qed
lemma (in ring) ideal_prod_simp:
assumes "ideal I R" "ideal J R" (* the second assumption could be suppressed *)
shows "I = I <+> (I \<cdot> J)"
proof
show "I \<subseteq> I <+> I \<cdot> J"
proof
fix i assume "i \<in> I" hence "i \<oplus> \<zero> \<in> I <+> I \<cdot> J"
using set_add_def'[of R I "I \<cdot> J"] ideal_prod_is_ideal[OF assms]
additive_subgroup.zero_closed[OF ideal.axioms(1), of "I \<cdot> J" R] by auto
thus "i \<in> I <+> I \<cdot> J"
using \<open>i \<in> I\<close> assms(1) ideal.Icarr by fastforce
qed
next
show "I <+> I \<cdot> J \<subseteq> I"
proof
fix s assume "s \<in> I <+> I \<cdot> J"
then obtain i ij where "i \<in> I" "ij \<in> I \<cdot> J" "s = i \<oplus> ij"
using set_add_def'[of R I "I \<cdot> J"] by auto
thus "s \<in> I"
using ideal_prod_inter[OF assms]
by (meson additive_subgroup.a_closed assms(1) ideal.axioms(1) inf_sup_ord(1) subsetCE)
qed
qed
lemma (in ring) ideal_prod_one:
assumes "ideal I R"
shows "I \<cdot> (carrier R) = I"
proof
show "I \<cdot> (carrier R) \<subseteq> I"
proof
fix s assume "s \<in> I \<cdot> (carrier R)" thus "s \<in> I"
by (induct s rule: ideal_prod.induct)
(simp_all add: assms ideal.I_r_closed additive_subgroup.a_closed ideal.axioms(1))
qed
next
show "I \<subseteq> I \<cdot> (carrier R)"
proof
fix i assume "i \<in> I" thus "i \<in> I \<cdot> (carrier R)"
by (metis assms ideal.Icarr ideal_prod.simps one_closed r_one)
qed
qed
lemma (in ring) ideal_prod_zero:
assumes "ideal I R"
shows "I \<cdot> { \<zero> } = { \<zero> }"
proof
show "I \<cdot> { \<zero> } \<subseteq> { \<zero> }"
proof
fix s assume "s \<in> I \<cdot> {\<zero>}" thus "s \<in> { \<zero> }"
using assms ideal.Icarr by (induct s rule: ideal_prod.induct) (fastforce, simp)
qed
next
show "{ \<zero> } \<subseteq> I \<cdot> { \<zero> }"
by (simp add: additive_subgroup.zero_closed assms
ideal.axioms(1) ideal_prod_is_ideal zeroideal)
qed
lemma (in ring) ideal_prod_assoc:
assumes "ideal I R" "ideal J R" "ideal K R"
shows "(I \<cdot> J) \<cdot> K = I \<cdot> (J \<cdot> K)"
proof
show "(I \<cdot> J) \<cdot> K \<subseteq> I \<cdot> (J \<cdot> K)"
proof
fix s assume "s \<in> (I \<cdot> J) \<cdot> K" thus "s \<in> I \<cdot> (J \<cdot> K)"
proof (induct s rule: ideal_prod.induct)
case (sum s1 s2) thus ?case
by (simp add: ideal_prod.sum)
next
case (prod i k) thus ?case
proof (induct i rule: ideal_prod.induct)
case (prod i j) thus ?case
using ideal_prod.prod[OF prod(1) ideal_prod.prod[OF prod(2-3),of R], of R]
by (metis assms ideal.Icarr m_assoc)
next
case (sum s1 s2) thus ?case
by (smt additive_subgroup.a_Hcarr contra_subsetD ideal.axioms(1)
assms ideal_prod.sum ideal_prod_in_carrier l_distr)
qed
qed
qed
next
show "I \<cdot> (J \<cdot> K) \<subseteq> (I \<cdot> J) \<cdot> K"
proof
fix s assume "s \<in> I \<cdot> (J \<cdot> K)" thus "s \<in> (I \<cdot> J) \<cdot> K"
proof (induct s rule: ideal_prod.induct)
case (sum s1 s2) thus ?case by (simp add: ideal_prod.sum)
next
case (prod i j) show ?case using prod(2) prod(1)
proof (induct j rule: ideal_prod.induct)
case (prod j k) thus ?case
using ideal_prod.prod[OF ideal_prod.prod[OF prod(3) prod(1), of R] prod (2), of R]
by (metis assms ideal.Icarr m_assoc)
next
case (sum s1 s2) thus ?case
by (smt additive_subgroup.a_Hcarr contra_subsetD ideal.axioms(1)
assms ideal_prod.sum ideal_prod_in_carrier r_distr)
qed
qed
qed
qed
lemma (in ring) ideal_prod_r_distr:
assumes "ideal I R" "ideal J R" "ideal K R"
shows "I \<cdot> (J <+> K) = (I \<cdot> J) <+> (I \<cdot> K)"
proof
show "I \<cdot> (J <+> K) \<subseteq> I \<cdot> J <+> I \<cdot> K"
proof
fix s assume "s \<in> I \<cdot> (J <+> K)" thus "s \<in> I \<cdot> J <+> I \<cdot> K"
proof(induct s rule: ideal_prod.induct)
case (prod i jk)
then obtain j k where j: "j \<in> J" and k: "k \<in> K" and jk: "jk = j \<oplus> k"
using set_add_def'[of R J K] by auto
hence "i \<otimes> j \<oplus> i \<otimes> k \<in> I \<cdot> J <+> I \<cdot> K"
using ideal_prod.prod[OF prod(1) j,of R]
ideal_prod.prod[OF prod(1) k,of R]
set_add_def'[of R "I \<cdot> J" "I \<cdot> K"] by auto
thus ?case
using assms ideal.Icarr r_distr jk j k prod(1) by metis
next
case (sum s1 s2) thus ?case
by (simp add: add_ideals additive_subgroup.a_closed assms ideal.axioms(1)
local.ring_axioms ring.ideal_prod_is_ideal)
qed
qed
next
{ fix s J K assume A: "ideal J R" "ideal K R" "s \<in> I \<cdot> J"
have "s \<in> I \<cdot> (J <+> K) \<and> s \<in> I \<cdot> (K <+> J)"
proof -
from \<open>s \<in> I \<cdot> J\<close> have "s \<in> I \<cdot> (J <+> K)"
proof (induct s rule: ideal_prod.induct)
case (prod i j)
hence "(j \<oplus> \<zero>) \<in> J <+> K"
using set_add_def'[of R J K]
additive_subgroup.zero_closed[OF ideal.axioms(1), of K R] A(2) by auto
thus ?case
by (metis A(1) additive_subgroup.a_Hcarr ideal.axioms(1) ideal_prod.prod prod r_zero)
next
case (sum s1 s2) thus ?case
by (simp add: ideal_prod.sum)
qed
thus ?thesis
by (metis A(1) A(2) ideal_def ring.union_genideal sup_commute)
qed } note aux_lemma = this
show "I \<cdot> J <+> I \<cdot> K \<subseteq> I \<cdot> (J <+> K)"
proof
fix s assume "s \<in> I \<cdot> J <+> I \<cdot> K"
then obtain s1 s2 where s1: "s1 \<in> I \<cdot> J" and s2: "s2 \<in> I \<cdot> K" and s: "s = s1 \<oplus> s2"
using set_add_def'[of R "I \<cdot> J" "I \<cdot> K"] by auto
thus "s \<in> I \<cdot> (J <+> K)"
using aux_lemma[OF assms(2) assms(3) s1]
aux_lemma[OF assms(3) assms(2) s2] by (simp add: ideal_prod.sum)
qed
qed
lemma (in cring) ideal_prod_commute:
assumes "ideal I R" "ideal J R"
shows "I \<cdot> J = J \<cdot> I"
proof -
{ fix I J assume A: "ideal I R" "ideal J R"
have "I \<cdot> J \<subseteq> J \<cdot> I"
proof
fix s assume "s \<in> I \<cdot> J" thus "s \<in> J \<cdot> I"
proof (induct s rule: ideal_prod.induct)
case (prod i j) thus ?case
using m_comm[OF ideal.Icarr[OF A(1) prod(1)] ideal.Icarr[OF A(2) prod(2)]]
by (simp add: ideal_prod.prod)
next
case (sum s1 s2) thus ?case by (simp add: ideal_prod.sum)
qed
qed }
thus ?thesis using assms by blast
qed
text \<open>The following result would also be true for locale ring\<close>
lemma (in cring) ideal_prod_distr:
assumes "ideal I R" "ideal J R" "ideal K R"
shows "I \<cdot> (J <+> K) = (I \<cdot> J) <+> (I \<cdot> K)"
and "(J <+> K) \<cdot> I = (J \<cdot> I) <+> (K \<cdot> I)"
by (simp_all add: assms ideal_prod_commute local.ring_axioms
ring.add_ideals ring.ideal_prod_r_distr)
lemma (in cring) ideal_prod_eq_inter:
assumes "ideal I R" "ideal J R"
and "I <+> J = carrier R"
shows "I \<cdot> J = I \<inter> J"
proof
show "I \<cdot> J \<subseteq> I \<inter> J"
using assms ideal_prod_inter by auto
next
show "I \<inter> J \<subseteq> I \<cdot> J"
proof
have "\<one> \<in> I <+> J" using assms(3) one_closed by simp
then obtain i j where ij: "i \<in> I" "j \<in> J" "\<one> = i \<oplus> j"
using set_add_def'[of R I J] by auto
fix s assume s: "s \<in> I \<inter> J"
hence "(i \<otimes> s \<in> I \<cdot> J) \<and> (s \<otimes> j \<in> I \<cdot> J)"
using ij(1-2) by (simp add: ideal_prod.prod)
moreover have "s = (i \<otimes> s) \<oplus> (s \<otimes> j)"
using ideal.Icarr[OF assms(1) ij(1)]
ideal.Icarr[OF assms(2) ij(2)]
ideal.Icarr[OF assms(1), of s]
by (metis ij(3) s m_comm[of s i] Int_iff r_distr r_one)
ultimately show "s \<in> I \<cdot> J"
using ideal_prod.sum by fastforce
qed
qed
subsection \<open>Structure of the Set of Ideals\<close>
text \<open>We focus on commutative rings for convenience.\<close>
lemma (in cring) ideals_set_is_semiring: "semiring (ideals_set R)"
proof -
have "abelian_monoid (ideals_set R)"
apply (rule abelian_monoidI) unfolding ideals_set_def
apply (simp_all add: add_ideals zeroideal)
apply (simp add: add.set_mult_assoc additive_subgroup.a_subset ideal.axioms(1) set_add_defs(1))
apply (metis Un_absorb1 additive_subgroup.a_subset additive_subgroup.zero_closed
cgenideal_minimal cgenideal_self empty_iff genideal_minimal ideal.axioms(1)
local.ring_axioms order_refl ring.genideal_self subset_antisym subset_singletonD
union_genideal zero_closed zeroideal)
by (metis sup_commute union_genideal)
moreover have "monoid (ideals_set R)"
apply (rule monoidI) unfolding ideals_set_def
apply (simp_all add: ideal_prod_is_ideal oneideal
ideal_prod_commute ideal_prod_one)
by (metis ideal_prod_assoc ideal_prod_commute)
ultimately show ?thesis
unfolding semiring_def semiring_axioms_def ideals_set_def
by (simp_all add: ideal_prod_distr ideal_prod_commute ideal_prod_zero zeroideal)
qed
lemma (in cring) ideals_set_is_comm_monoid: "comm_monoid (ideals_set R)"
proof -
have "monoid (ideals_set R)"
apply (rule monoidI) unfolding ideals_set_def
apply (simp_all add: ideal_prod_is_ideal oneideal
ideal_prod_commute ideal_prod_one)
by (metis ideal_prod_assoc ideal_prod_commute)
thus ?thesis
unfolding comm_monoid_def comm_monoid_axioms_def
by (simp add: ideal_prod_commute ideals_set_def)
qed
lemma (in cring) ideal_prod_eq_Inter_aux:
assumes "I: {..(Suc n)} \<rightarrow> { J. ideal J R }"
and "\<And>i j. \<lbrakk> i \<in> {..(Suc n)}; j \<in> {..(Suc n)} \<rbrakk> \<Longrightarrow>
i \<noteq> j \<Longrightarrow> (I i) <+> (I j) = carrier R"
shows "(\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..n}. I k) <+> (I (Suc n)) = carrier R" using assms
proof (induct n arbitrary: I)
case 0
hence "(\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..0}. I k) <+> I (Suc 0) = (I 0) <+> (I (Suc 0))"
using comm_monoid.finprod_0[OF ideals_set_is_comm_monoid, of I]
by (simp add: atMost_Suc ideals_set_def)
also have " ... = carrier R"
using 0(2)[of 0 "Suc 0"] by simp
finally show ?case .
next
interpret ISet: comm_monoid "ideals_set R"
by (simp add: ideals_set_is_comm_monoid)
case (Suc n)
let ?I' = "\<lambda>i. I (Suc i)"
have "?I': {..(Suc n)} \<rightarrow> { J. ideal J R }"
using Suc.prems(1) by auto
moreover have "\<And>i j. \<lbrakk> i \<in> {..(Suc n)}; j \<in> {..(Suc n)} \<rbrakk> \<Longrightarrow>
i \<noteq> j \<Longrightarrow> (?I' i) <+> (?I' j) = carrier R"
by (simp add: Suc.prems(2))
ultimately have "(\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..n}. ?I' k) <+> (?I' (Suc n)) = carrier R"
using Suc.hyps by metis
moreover have I_carr: "I: {..Suc (Suc n)} \<rightarrow> carrier (ideals_set R)"
unfolding ideals_set_def using Suc by simp
hence I'_carr: "I \<in> Suc ` {..n} \<rightarrow> carrier (ideals_set R)" by auto
ultimately have "(\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {(Suc 0)..Suc n}. I k) <+> (I (Suc (Suc n))) = carrier R"
using ISet.finprod_reindex[of I "\<lambda>i. Suc i" "{..n}"] by (simp add: atMost_atLeast0)
hence "(carrier R) \<cdot> (I 0) = ((\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {Suc 0..Suc n}. I k) <+> I (Suc (Suc n))) \<cdot> (I 0)"
by auto
moreover have fprod_cl1: "ideal (\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {Suc 0..Suc n}. I k) R"
by (metis I'_carr ISet.finprod_closed One_nat_def ideals_set_def image_Suc_atMost
mem_Collect_eq partial_object.select_convs(1))
ultimately
have "I 0 = (\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {Suc 0..Suc n}. I k) \<cdot> (I 0) <+> I (Suc (Suc n)) \<cdot> (I 0)"
by (metis PiE Suc.prems(1) atLeast0_atMost_Suc atLeast0_atMost_Suc_eq_insert_0
atMost_atLeast0 ideal_prod_commute ideal_prod_distr(2) ideal_prod_one insertI1
mem_Collect_eq oneideal)
also have " ... = (I 0) \<cdot> (\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {Suc 0..Suc n}. I k) <+> I (Suc (Suc n)) \<cdot> (I 0)"
using fprod_cl1 ideal_prod_commute Suc.prems(1)
by (simp add: atLeast0_atMost_Suc_eq_insert_0 atMost_atLeast0)
also have " ... = (I 0) \<otimes>\<^bsub>(ideals_set R)\<^esub> (\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {Suc 0..Suc n}. I k) <+>
I (Suc (Suc n)) \<cdot> (I 0)"
by (simp add: ideals_set_def)
finally have I0: "I 0 = (\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..Suc n}. I k) <+> I (Suc (Suc n)) \<cdot> (I 0)"
using ISet.finprod_insert[of "{Suc 0..Suc n}" 0 I]
I_carr I'_carr atMost_atLeast0 ISet.finprod_0' atMost_Suc by auto
have I_SucSuc_I0: "ideal (I (Suc (Suc n))) R \<and> ideal (I 0) R"
using Suc.prems(1) by auto
have fprod_cl2: "ideal (\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..Suc n}. I k) R"
by (smt ISet.finprod_closed I_carr Pi_split_insert_domain atMost_Suc ideals_set_def mem_Collect_eq partial_object.select_convs(1))
have "carrier R = I (Suc (Suc n)) <+> I 0"
by (simp add: Suc.prems(2))
also have " ... = I (Suc (Suc n)) <+>
((\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..Suc n}. I k) <+> I (Suc (Suc n)) \<cdot> (I 0))"
using I0 by auto
also have " ... = I (Suc (Suc n)) <+>
(I (Suc (Suc n)) \<cdot> (I 0) <+> (\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..Suc n}. I k))"
using fprod_cl2 I_SucSuc_I0 by (metis Un_commute ideal_prod_is_ideal union_genideal)
also have " ... = (I (Suc (Suc n)) <+> I (Suc (Suc n)) \<cdot> (I 0)) <+>
(\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..Suc n}. I k)"
using fprod_cl2 I_SucSuc_I0 by (metis add.set_mult_assoc ideal_def ideal_prod_in_carrier
oneideal ring.ideal_prod_one set_add_defs(1))
also have " ... = I (Suc (Suc n)) <+> (\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..Suc n}. I k)"
using ideal_prod_simp[of "I (Suc (Suc n))" "I 0"] I_SucSuc_I0 by simp
also have " ... = (\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..Suc n}. I k) <+> I (Suc (Suc n))"
using fprod_cl2 I_SucSuc_I0 by (metis Un_commute union_genideal)
finally show ?case by simp
qed
theorem (in cring) ideal_prod_eq_Inter:
assumes "I: {..n :: nat} \<rightarrow> { J. ideal J R }"
and "\<And>i j. \<lbrakk> i \<in> {..n}; j \<in> {..n} \<rbrakk> \<Longrightarrow> i \<noteq> j \<Longrightarrow> (I i) <+> (I j) = carrier R"
shows "(\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..n}. I k) = (\<Inter> k \<in> {..n}. I k)" using assms
proof (induct n)
case 0 thus ?case
using comm_monoid.finprod_0[OF ideals_set_is_comm_monoid] by (simp add: ideals_set_def)
next
interpret ISet: comm_monoid "ideals_set R"
by (simp add: ideals_set_is_comm_monoid)
case (Suc n)
hence IH: "(\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..n}. I k) = (\<Inter> k \<in> {..n}. I k)"
by (simp add: atMost_Suc)
hence "(\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..Suc n}. I k) = I (Suc n) \<otimes>\<^bsub>(ideals_set R)\<^esub> (\<Inter> k \<in> {..n}. I k)"
using ISet.finprod_insert[of "{Suc 0..Suc n}" 0 I] atMost_Suc_eq_insert_0[of n]
by (metis ISet.finprod_Suc Suc.prems(1) ideals_set_def partial_object.select_convs(1))
hence "(\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..Suc n}. I k) = I (Suc n) \<cdot> (\<Inter> k \<in> {..n}. I k)"
by (simp add: ideals_set_def)
moreover have "(\<Inter> k \<in> {..n}. I k) <+> I (Suc n) = carrier R"
using ideal_prod_eq_Inter_aux[of I n] by (simp add: Suc.prems IH)
moreover have "ideal (\<Inter> k \<in> {..n}. I k) R"
using ring.i_Intersect[of R "I ` {..n}"]
by (metis IH ISet.finprod_closed Pi_split_insert_domain Suc.prems(1) atMost_Suc
ideals_set_def mem_Collect_eq partial_object.select_convs(1))
ultimately
have "(\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..Suc n}. I k) = (\<Inter> k \<in> {..n}. I k) \<inter> I (Suc n)"
using ideal_prod_eq_inter[of "\<Inter> k \<in> {..n}. I k" "I (Suc n)"]
ideal_prod_commute[of "\<Inter> k \<in> {..n}. I k" "I (Suc n)"]
by (metis PiE Suc.prems(1) atMost_iff mem_Collect_eq order_refl)
thus ?case by (simp add: Int_commute atMost_Suc)
qed
corollary (in cring) inter_plus_ideal_eq_carrier:
assumes "\<And>i. i \<le> Suc n \<Longrightarrow> ideal (I i) R"
and "\<And>i j. \<lbrakk> i \<le> Suc n; j \<le> Suc n; i \<noteq> j \<rbrakk> \<Longrightarrow> I i <+> I j = carrier R"
shows "(\<Inter> i \<le> n. I i) <+> (I (Suc n)) = carrier R"
using ideal_prod_eq_Inter[of I n] ideal_prod_eq_Inter_aux[of I n] by (auto simp add: assms)
corollary (in cring) inter_plus_ideal_eq_carrier_arbitrary:
assumes "\<And>i. i \<le> Suc n \<Longrightarrow> ideal (I i) R"
and "\<And>i j. \<lbrakk> i \<le> Suc n; j \<le> Suc n; i \<noteq> j \<rbrakk> \<Longrightarrow> I i <+> I j = carrier R"
and "j \<le> Suc n"
shows "(\<Inter> i \<in> ({..(Suc n)} - { j }). I i) <+> (I j) = carrier R"
proof -
define I' where "I' = (\<lambda>i. if i = Suc n then (I j) else
if i = j then (I (Suc n))
else (I i))"
have "\<And>i. i \<le> Suc n \<Longrightarrow> ideal (I' i) R"
using I'_def assms(1) assms(3) by auto
moreover have "\<And>i j. \<lbrakk> i \<le> Suc n; j \<le> Suc n; i \<noteq> j \<rbrakk> \<Longrightarrow> I' i <+> I' j = carrier R"
using I'_def assms(2-3) by force
ultimately have "(\<Inter> i \<le> n. I' i) <+> (I' (Suc n)) = carrier R"
using inter_plus_ideal_eq_carrier by simp
moreover have "I' ` {..n} = I ` ({..(Suc n)} - { j })"
proof
show "I' ` {..n} \<subseteq> I ` ({..Suc n} - {j})"
proof
fix x assume "x \<in> I' ` {..n}"
then obtain i where i: "i \<in> {..n}" "I' i = x" by blast
thus "x \<in> I ` ({..Suc n} - {j})"
proof (cases)
assume "i = j" thus ?thesis using i I'_def by auto
next
assume "i \<noteq> j" thus ?thesis using I'_def i insert_iff by auto
qed
qed
next
show "I ` ({..Suc n} - {j}) \<subseteq> I' ` {..n}"
proof
fix x assume "x \<in> I ` ({..Suc n} - {j})"
then obtain i where i: "i \<in> {..Suc n}" "i \<noteq> j" "I i = x" by blast
thus "x \<in> I' ` {..n}"
proof (cases)
assume "i = Suc n" thus ?thesis using I'_def assms(3) i(2-3) by auto
next
assume "i \<noteq> Suc n" thus ?thesis using I'_def i by auto
qed
qed
qed
ultimately show ?thesis using I'_def by metis
qed
subsection \<open>Another Characterization of Prime Ideals\<close>
text \<open>With product of ideals being defined, we can give another definition of a prime ideal\<close>
lemma (in ring) primeideal_divides_ideal_prod:
assumes "primeideal P R" "ideal I R" "ideal J R"
and "I \<cdot> J \<subseteq> P"
shows "I \<subseteq> P \<or> J \<subseteq> P"
proof (cases)
assume "\<exists> i \<in> I. i \<notin> P"
then obtain i where i: "i \<in> I" "i \<notin> P" by blast
have "J \<subseteq> P"
proof
fix j assume j: "j \<in> J"
hence "i \<otimes> j \<in> P"
using ideal_prod.prod[OF i(1) j, of R] assms(4) by auto
thus "j \<in> P"
using primeideal.I_prime[OF assms(1), of i j] i j
by (meson assms(2-3) ideal.Icarr)
qed
thus ?thesis by blast
next
assume "\<not> (\<exists> i \<in> I. i \<notin> P)" thus ?thesis by blast
qed
lemma (in cring) divides_ideal_prod_imp_primeideal:
assumes "ideal P R"
and "P \<noteq> carrier R"
and "\<And>I J. \<lbrakk> ideal I R; ideal J R; I \<cdot> J \<subseteq> P \<rbrakk> \<Longrightarrow> I \<subseteq> P \<or> J \<subseteq> P"
shows "primeideal P R"
proof -
have "\<And>a b. \<lbrakk> a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> P \<rbrakk> \<Longrightarrow> a \<in> P \<or> b \<in> P"
proof -
fix a b assume A: "a \<in> carrier R" "b \<in> carrier R" "a \<otimes> b \<in> P"
have "(PIdl a) \<cdot> (PIdl b) = Idl (PIdl (a \<otimes> b))"
using ideal_prod_eq_genideal[of "Idl { a }" "Idl { b }"]
A(1-2) cgenideal_eq_genideal cgenideal_ideal cgenideal_prod by auto
hence "(PIdl a) \<cdot> (PIdl b) = PIdl (a \<otimes> b)"
by (simp add: A Idl_subset_ideal cgenideal_ideal cgenideal_minimal
genideal_self oneideal subset_antisym)
hence "(PIdl a) \<cdot> (PIdl b) \<subseteq> P"
by (simp add: A(3) assms(1) cgenideal_minimal)
hence "(PIdl a) \<subseteq> P \<or> (PIdl b) \<subseteq> P"
by (simp add: A assms(3) cgenideal_ideal)
thus "a \<in> P \<or> b \<in> P"
using A cgenideal_self by blast
qed
thus ?thesis
using assms is_cring by (simp add: primeidealI)
qed
end