-
Notifications
You must be signed in to change notification settings - Fork 0
/
Chinese_Remainder.thy
509 lines (429 loc) · 25 KB
/
Chinese_Remainder.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
(* Title: HOL/Algebra/Chinese_Remainder.thy
Author: Paulo Emílio de Vilhena
*)
theory Chinese_Remainder
imports Weak_Morphisms Ideal_Product
begin
section \<open>Direct Product of Rings\<close>
subsection \<open>Definitions\<close>
definition RDirProd :: "('a, 'n) ring_scheme \<Rightarrow> ('b, 'm) ring_scheme \<Rightarrow> ('a \<times> 'b) ring"
where "RDirProd R S = monoid.extend (R \<times>\<times> S)
\<lparr> zero = one ((add_monoid R) \<times>\<times> (add_monoid S)),
add = mult ((add_monoid R) \<times>\<times> (add_monoid S)) \<rparr> "
abbreviation nil_ring :: "('a list) ring"
where "nil_ring \<equiv> monoid.extend nil_monoid \<lparr> zero = [], add = (\<lambda>a b. []) \<rparr>"
definition RDirProd_list :: "(('a, 'n) ring_scheme) list \<Rightarrow> ('a list) ring"
where "RDirProd_list Rs = foldr (\<lambda>R S. image_ring (\<lambda>(a, as). a # as) (RDirProd R S)) Rs nil_ring"
subsection \<open>Basic Properties\<close>
lemma RDirProd_carrier: "carrier (RDirProd R S) = carrier R \<times> carrier S"
unfolding RDirProd_def DirProd_def by (simp add: monoid.defs)
lemma RDirProd_add_monoid [simp]: "add_monoid (RDirProd R S) = (add_monoid R) \<times>\<times> (add_monoid S)"
by (simp add: RDirProd_def monoid.defs)
lemma RDirProd_ring:
assumes "ring R" and "ring S" shows "ring (RDirProd R S)"
proof -
have "monoid (RDirProd R S)"
using DirProd_monoid[OF assms[THEN ring.axioms(2)]] unfolding monoid_def
by (auto simp add: DirProd_def RDirProd_def monoid.defs)
then interpret Prod: group "add_monoid (RDirProd R S)" + monoid "RDirProd R S"
using DirProd_group[OF assms[THEN abelian_group.a_group[OF ring.is_abelian_group]]]
unfolding RDirProd_add_monoid by auto
show ?thesis
by (unfold_locales, auto simp add: RDirProd_def DirProd_def monoid.defs assms ring.ring_simprules)
qed
lemma RDirProd_iso1:
"(\<lambda>(x, y). (y, x)) \<in> ring_iso (RDirProd R S) (RDirProd S R)"
unfolding ring_iso_def ring_hom_def bij_betw_def inj_on_def
by (auto simp add: RDirProd_def DirProd_def monoid.defs)
lemma RDirProd_iso2:
"(\<lambda>(x, (y, z)). ((x, y), z)) \<in> ring_iso (RDirProd R (RDirProd S T)) (RDirProd (RDirProd R S) T)"
unfolding ring_iso_def ring_hom_def bij_betw_def inj_on_def
by (auto simp add: image_iff RDirProd_def DirProd_def monoid.defs)
lemma RDirProd_iso3:
"(\<lambda>((x, y), z). (x, (y, z))) \<in> ring_iso (RDirProd (RDirProd R S) T) (RDirProd R (RDirProd S T))"
unfolding ring_iso_def ring_hom_def bij_betw_def inj_on_def
by (auto simp add: image_iff RDirProd_def DirProd_def monoid.defs)
lemma RDirProd_iso4:
assumes "f \<in> ring_iso R S" shows "(\<lambda>(r, t). (f r, t)) \<in> ring_iso (RDirProd R T) (RDirProd S T)"
using assms unfolding ring_iso_def ring_hom_def bij_betw_def inj_on_def
by (auto simp add: image_iff RDirProd_def DirProd_def monoid.defs)+
lemma RDirProd_iso5:
assumes "f \<in> ring_iso S T" shows "(\<lambda>(r, s). (r, f s)) \<in> ring_iso (RDirProd R S) (RDirProd R T)"
using ring_iso_set_trans[OF ring_iso_set_trans[OF RDirProd_iso1 RDirProd_iso4[OF assms]] RDirProd_iso1]
by (simp add: case_prod_unfold comp_def)
lemma RDirProd_iso6:
assumes "f \<in> ring_iso R R'" and "g \<in> ring_iso S S'"
shows "(\<lambda>(r, s). (f r, g s)) \<in> ring_iso (RDirProd R S) (RDirProd R' S')"
using ring_iso_set_trans[OF RDirProd_iso4[OF assms(1)] RDirProd_iso5[OF assms(2)]]
by (simp add: case_prod_beta' comp_def)
lemma RDirProd_iso7:
shows "(\<lambda>a. (a, [])) \<in> ring_iso R (RDirProd R nil_ring)"
unfolding ring_iso_def ring_hom_def bij_betw_def inj_on_def
by (auto simp add: RDirProd_def DirProd_def monoid.defs)
lemma RDirProd_hom1:
shows "(\<lambda>a. (a, a)) \<in> ring_hom R (RDirProd R R)"
by (auto simp add: ring_hom_def RDirProd_def DirProd_def monoid.defs)
lemma RDirProd_hom2:
assumes "f \<in> ring_hom S T"
shows "(\<lambda>(x, y). (x, f y)) \<in> ring_hom (RDirProd R S) (RDirProd R T)"
and "(\<lambda>(x, y). (f x, y)) \<in> ring_hom (RDirProd S R) (RDirProd T R)"
using assms by (auto simp add: ring_hom_def RDirProd_def DirProd_def monoid.defs)
lemma RDirProd_hom3:
assumes "f \<in> ring_hom R R'" and "g \<in> ring_hom S S'"
shows "(\<lambda>(r, s). (f r, g s)) \<in> ring_hom (RDirProd R S) (RDirProd R' S')"
using ring_hom_trans[OF RDirProd_hom2(2)[OF assms(1)] RDirProd_hom2(1)[OF assms(2)]]
by (simp add: case_prod_beta' comp_def)
subsection \<open>Direct Product of a List of Rings\<close>
lemma RDirProd_list_nil [simp]: "RDirProd_list [] = nil_ring"
unfolding RDirProd_list_def by simp
lemma nil_ring_simprules [simp]:
"carrier nil_ring = { [] }" and "one nil_ring = []" and "zero nil_ring = []"
by (auto simp add: monoid.defs)
lemma RDirProd_list_truncate:
shows "monoid.truncate (RDirProd_list Rs) = DirProd_list Rs"
proof (induct Rs, simp add: RDirProd_list_def DirProd_list_def monoid.defs)
case (Cons R Rs)
have "monoid.truncate (RDirProd_list (R # Rs)) =
monoid.truncate (image_ring (\<lambda>(a, as). a # as) (RDirProd R (RDirProd_list Rs)))"
unfolding RDirProd_list_def by simp
also have " ... = image_group (\<lambda>(a, as). a # as) (monoid.truncate (RDirProd R (RDirProd_list Rs)))"
by (simp add: image_ring_def image_group_def monoid.defs)
also have " ... = image_group (\<lambda>(a, as). a # as) (R \<times>\<times> (monoid.truncate (RDirProd_list Rs)))"
by (simp add: RDirProd_def DirProd_def monoid.defs)
also have " ... = DirProd_list (R # Rs)"
unfolding Cons DirProd_list_def by simp
finally show ?case .
qed
lemma RDirProd_list_carrier_def':
shows "carrier (RDirProd_list Rs) = carrier (DirProd_list Rs)"
proof -
have "carrier (RDirProd_list Rs) = carrier (monoid.truncate (RDirProd_list Rs))"
by (simp add: monoid.defs)
thus ?thesis
unfolding RDirProd_list_truncate .
qed
lemma RDirProd_list_carrier:
shows "carrier (RDirProd_list (G # Gs)) = (\<lambda>(x, xs). x # xs) ` (carrier G \<times> carrier (RDirProd_list Gs))"
unfolding RDirProd_list_carrier_def' using DirProd_list_carrier .
lemma RDirProd_list_one:
shows "one (RDirProd_list Rs) = foldr (\<lambda>R tl. (one R) # tl) Rs []"
unfolding RDirProd_list_def RDirProd_def image_ring_def image_group_def
by (induct Rs) (auto simp add: monoid.defs)
lemma RDirProd_list_zero:
shows "zero (RDirProd_list Rs) = foldr (\<lambda>R tl. (zero R) # tl) Rs []"
unfolding RDirProd_list_def RDirProd_def image_ring_def
by (induct Rs) (auto simp add: monoid.defs)
lemma RDirProd_list_zero':
shows "zero (RDirProd_list (R # Rs)) = (zero R) # (zero (RDirProd_list Rs))"
unfolding RDirProd_list_zero by simp
lemma RDirProd_list_carrier_mem:
assumes "as \<in> carrier (RDirProd_list Rs)"
shows "length as = length Rs" and "\<And>i. i < length Rs \<Longrightarrow> (as ! i) \<in> carrier (Rs ! i)"
using assms DirProd_list_carrier_mem unfolding RDirProd_list_carrier_def' by auto
lemma RDirProd_list_carrier_memI:
assumes "length as = length Rs" and "\<And>i. i < length Rs \<Longrightarrow> (as ! i) \<in> carrier (Rs ! i)"
shows "as \<in> carrier (RDirProd_list Rs)"
using assms DirProd_list_carrier_memI unfolding RDirProd_list_carrier_def' by auto
lemma inj_on_RDirProd_carrier:
shows "inj_on (\<lambda>(a, as). a # as) (carrier (RDirProd R (RDirProd_list Rs)))"
unfolding RDirProd_def DirProd_def inj_on_def by auto
lemma RDirProd_list_is_ring:
assumes "\<And>i. i < length Rs \<Longrightarrow> ring (Rs ! i)" shows "ring (RDirProd_list Rs)"
using assms
proof (induct Rs)
case Nil thus ?case
unfolding RDirProd_list_def by (unfold_locales, auto simp add: monoid.defs Units_def)
next
case (Cons R Rs)
hence is_ring: "ring (RDirProd R (RDirProd_list Rs))"
using RDirProd_ring[of R "RDirProd_list Rs"] by force
show ?case
using ring.inj_imp_image_ring_is_ring[OF is_ring inj_on_RDirProd_carrier]
unfolding RDirProd_list_def by auto
qed
lemma RDirProd_list_iso1:
"(\<lambda>(a, as). a # as) \<in> ring_iso (RDirProd R (RDirProd_list Rs)) (RDirProd_list (R # Rs))"
using inj_imp_image_ring_iso[OF inj_on_RDirProd_carrier] unfolding RDirProd_list_def by auto
lemma RDirProd_list_iso2:
"Hilbert_Choice.inv (\<lambda>(a, as). a # as) \<in> ring_iso (RDirProd_list (R # Rs)) (RDirProd R (RDirProd_list Rs))"
unfolding RDirProd_list_def by (auto intro: inj_imp_image_ring_inv_iso simp add: inj_def)
lemma RDirProd_list_iso3:
"(\<lambda>a. [ a ]) \<in> ring_iso R (RDirProd_list [ R ])"
proof -
have [simp]: "(\<lambda>a. [ a ]) = (\<lambda>(a, as). a # as) \<circ> (\<lambda>a. (a, []))" by auto
show ?thesis
using ring_iso_set_trans[OF RDirProd_iso7] RDirProd_list_iso1[of R "[]"]
unfolding RDirProd_list_def by simp
qed
lemma RDirProd_list_hom1:
"(\<lambda>(a, as). a # as) \<in> ring_hom (RDirProd R (RDirProd_list Rs)) (RDirProd_list (R # Rs))"
using RDirProd_list_iso1 unfolding ring_iso_def by auto
lemma RDirProd_list_hom2:
assumes "f \<in> ring_hom R S" shows "(\<lambda>a. [ f a ]) \<in> ring_hom R (RDirProd_list [ S ])"
proof -
have hom1: "(\<lambda>a. (a, [])) \<in> ring_hom R (RDirProd R nil_ring)"
using RDirProd_iso7 unfolding ring_iso_def by auto
have hom2: "(\<lambda>(a, as). a # as) \<in> ring_hom (RDirProd S nil_ring) (RDirProd_list [ S ])"
using RDirProd_list_hom1[of _ "[]"] unfolding RDirProd_list_def by auto
have [simp]: "(\<lambda>(a, as). a # as) \<circ> ((\<lambda>(x, y). (f x, y)) \<circ> (\<lambda>a. (a, []))) = (\<lambda>a. [ f a ])" by auto
show ?thesis
using ring_hom_trans[OF ring_hom_trans[OF hom1 RDirProd_hom2(2)[OF assms]] hom2] by simp
qed
section \<open>Chinese Remainder Theorem\<close>
subsection \<open>Definitions\<close>
abbreviation (in ring) canonical_proj :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'a set \<times> 'a set"
where "canonical_proj I J \<equiv> (\<lambda>a. (I +> a, J +> a))"
definition (in ring) canonical_proj_ext :: "(nat \<Rightarrow> 'a set) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> ('a set) list"
where "canonical_proj_ext I n = (\<lambda>a. map (\<lambda>i. (I i) +> a) [0..< Suc n])"
subsection \<open>Chinese Remainder Simple\<close>
lemma (in ring) canonical_proj_is_surj:
assumes "ideal I R" "ideal J R" and "I <+> J = carrier R"
shows "(canonical_proj I J) ` carrier R = carrier (RDirProd (R Quot I) (R Quot J))"
unfolding RDirProd_def DirProd_def FactRing_def A_RCOSETS_def'
proof (auto simp add: monoid.defs)
{ fix I i assume "ideal I R" "i \<in> I" hence "I +> i = \<zero>\<^bsub>R Quot I\<^esub>"
using a_rcos_zero by (simp add: FactRing_def)
} note aux_lemma1 = this
{ fix I i j assume A: "ideal I R" "i \<in> I" "j \<in> carrier R" "i \<oplus> j = \<one>"
have "(I +> i) \<oplus>\<^bsub>R Quot I\<^esub> (I +> j) = I +> \<one>"
using ring_hom_memE(3)[OF ideal.rcos_ring_hom ideal.Icarr[OF _ A(2)] A(3)] A(1,4) by simp
moreover have "I +> i = I"
using abelian_subgroupI3[OF ideal.axioms(1) is_abelian_group]
by (simp add: A(1-2) abelian_subgroup.a_rcos_const)
moreover have "I +> j \<in> carrier (R Quot I)" and "I = \<zero>\<^bsub>R Quot I\<^esub>" and "I +> \<one> = \<one>\<^bsub>R Quot I\<^esub>"
by (auto simp add: FactRing_def A_RCOSETS_def' A(3))
ultimately have "I +> j = \<one>\<^bsub>R Quot I\<^esub>"
using ring.ring_simprules(8)[OF ideal.quotient_is_ring[OF A(1)]] by simp
} note aux_lemma2 = this
interpret I: ring "R Quot I" + J: ring "R Quot J"
using assms(1-2)[THEN ideal.quotient_is_ring] by auto
fix a b assume a: "a \<in> carrier R" and b: "b \<in> carrier R"
have "\<one> \<in> I <+> J"
using assms(3) by blast
then obtain i j where i: "i \<in> carrier R" "i \<in> I" and j: "j \<in> carrier R" "j \<in> J" and ij: "i \<oplus> j = \<one>"
using assms(1-2)[THEN ideal.Icarr] unfolding set_add_def' by auto
hence rcos_j: "I +> j = \<one>\<^bsub>R Quot I\<^esub>" and rcos_i: "J +> i = \<one>\<^bsub>R Quot J\<^esub>"
using assms(1-2)[THEN aux_lemma2] a_comm by simp+
define s where "s = (a \<otimes> j) \<oplus> (b \<otimes> i)"
hence "s \<in> carrier R"
using a b i j by simp
have "I +> s = ((I +> a) \<otimes>\<^bsub>R Quot I\<^esub> (I +> j)) \<oplus>\<^bsub>R Quot I\<^esub> (I +> (b \<otimes> i))"
using ring_hom_memE(2-3)[OF ideal.rcos_ring_hom[OF assms(1)]]
by (simp add: a b i(1) j(1) s_def)
moreover have "I +> a \<in> carrier (R Quot I)"
by (auto simp add: FactRing_def A_RCOSETS_def' a)
ultimately have "I +> s = I +> a"
unfolding rcos_j aux_lemma1[OF assms(1) ideal.I_l_closed[OF assms(1) i(2) b]] by simp
have "J +> s = (J +> (a \<otimes> j)) \<oplus>\<^bsub>R Quot J\<^esub> ((J +> b) \<otimes>\<^bsub>R Quot J\<^esub> (J +> i))"
using ring_hom_memE(2-3)[OF ideal.rcos_ring_hom[OF assms(2)]]
by (simp add: a b i(1) j(1) s_def)
moreover have "J +> b \<in> carrier (R Quot J)"
by (auto simp add: FactRing_def A_RCOSETS_def' b)
ultimately have "J +> s = J +> b"
unfolding rcos_i aux_lemma1[OF assms(2) ideal.I_l_closed[OF assms(2) j(2) a]] by simp
from \<open>I +> s = I +> a\<close> and \<open>J +> s = J +> b\<close> and \<open>s \<in> carrier R\<close>
show "(I +> a, J +> b) \<in> (canonical_proj I J) ` carrier R" by blast
qed
lemma (in ring) canonical_proj_ker:
assumes "ideal I R" and "ideal J R"
shows "a_kernel R (RDirProd (R Quot I) (R Quot J)) (canonical_proj I J) = I \<inter> J"
proof
show "a_kernel R (RDirProd (R Quot I) (R Quot J)) (canonical_proj I J) \<subseteq> I \<inter> J"
unfolding FactRing_def RDirProd_def DirProd_def a_kernel_def'
by (auto simp add: assms[THEN ideal.rcos_const_imp_mem] monoid.defs)
next
show "I \<inter> J \<subseteq> a_kernel R (RDirProd (R Quot I) (R Quot J)) (canonical_proj I J)"
proof
fix s assume s: "s \<in> I \<inter> J" then have "I +> s = I" and "J +> s = J"
using abelian_subgroupI3[OF ideal.axioms(1) is_abelian_group]
by (simp add: abelian_subgroup.a_rcos_const assms)+
thus "s \<in> a_kernel R (RDirProd (R Quot I) (R Quot J)) (canonical_proj I J)"
unfolding FactRing_def RDirProd_def DirProd_def a_kernel_def'
using ideal.Icarr[OF assms(1)] s by (simp add: monoid.defs)
qed
qed
lemma (in ring) canonical_proj_is_hom:
assumes "ideal I R" and "ideal J R"
shows "(canonical_proj I J) \<in> ring_hom R (RDirProd (R Quot I) (R Quot J))"
unfolding RDirProd_def DirProd_def FactRing_def A_RCOSETS_def'
by (auto intro!: ring_hom_memI
simp add: assms[THEN ideal.rcoset_mult_add]
assms[THEN ideal.a_rcos_sum] monoid.defs)
lemma (in ring) canonical_proj_ring_hom:
assumes "ideal I R" and "ideal J R"
shows "ring_hom_ring R (RDirProd (R Quot I) (R Quot J)) (canonical_proj I J)"
using ring_hom_ring.intro[OF ring_axioms RDirProd_ring[OF assms[THEN ideal.quotient_is_ring]]]
by (simp add: ring_hom_ring_axioms_def canonical_proj_is_hom[OF assms])
theorem (in ring) chinese_remainder_simple:
assumes "ideal I R" "ideal J R" and "I <+> J = carrier R"
shows "R Quot (I \<inter> J) \<simeq> RDirProd (R Quot I) (R Quot J)"
using ring_hom_ring.FactRing_iso[OF canonical_proj_ring_hom canonical_proj_is_surj]
by (simp add: canonical_proj_ker assms)
subsection \<open>Chinese Remainder Generalized\<close>
lemma (in ring) canonical_proj_ext_zero [simp]: "(canonical_proj_ext I 0) = (\<lambda>a. [ (I 0) +> a ])"
unfolding canonical_proj_ext_def by simp
lemma (in ring) canonical_proj_ext_tl:
"(\<lambda>a. canonical_proj_ext I (Suc n) a) = (\<lambda>a. ((I 0) +> a) # (canonical_proj_ext (\<lambda>i. I (Suc i)) n a))"
unfolding canonical_proj_ext_def by (induct n) (auto, metis (lifting) append.assoc append_Cons append_Nil)
lemma (in ring) canonical_proj_ext_is_hom:
assumes "\<And>i. i \<le> n \<Longrightarrow> ideal (I i) R"
shows "(canonical_proj_ext I n) \<in> ring_hom R (RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n]))"
using assms
proof (induct n arbitrary: I)
case 0 thus ?case
using RDirProd_list_hom2[OF ideal.rcos_ring_hom[of _ R]] by (simp add: canonical_proj_ext_def)
next
let ?DirProd = "\<lambda>I n. RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..<Suc n])"
let ?proj = "\<lambda>I n. canonical_proj_ext I n"
case (Suc n)
hence I: "ideal (I 0) R" by simp
have hom: "(?proj (\<lambda>i. I (Suc i)) n) \<in> ring_hom R (?DirProd (\<lambda>i. I (Suc i)) n)"
using Suc(1)[of "\<lambda>i. I (Suc i)"] Suc(2) by simp
have [simp]:
"(\<lambda>(a, as). a # as) \<circ> ((\<lambda>(r, s). (I 0 +> r, ?proj (\<lambda>i. I (Suc i)) n s)) \<circ> (\<lambda>a. (a, a))) = ?proj I (Suc n)"
unfolding canonical_proj_ext_tl by auto
moreover have
"(R Quot I 0) # (map (\<lambda>i. R Quot I (Suc i)) [0..< Suc n]) = map (\<lambda>i. R Quot (I i)) [0..< Suc (Suc n)]"
by (induct n) (auto)
moreover show ?case
using ring_hom_trans[OF ring_hom_trans[OF RDirProd_hom1
RDirProd_hom3[OF ideal.rcos_ring_hom[OF I] hom]] RDirProd_list_hom1]
unfolding calculation(2) by simp
qed
lemma (in ring) RDirProd_Quot_list_is_ring:
assumes "\<And>i. i \<le> n \<Longrightarrow> ideal (I i) R" shows "ring (RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n]))"
proof -
have ring_list: "\<And>i. i < Suc n \<Longrightarrow> ring ((map (\<lambda>i. R Quot I i) [0..< Suc n]) ! i)"
using ideal.quotient_is_ring[OF assms]
by (metis add.left_neutral diff_zero le_simps(2) nth_map_upt)
show ?thesis
using RDirProd_list_is_ring[OF ring_list] by simp
qed
lemma (in ring) canonical_proj_ext_ring_hom:
assumes "\<And>i. i \<le> n \<Longrightarrow> ideal (I i) R"
shows "ring_hom_ring R (RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n])) (canonical_proj_ext I n)"
proof -
have ring: "ring (RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n]))"
using RDirProd_Quot_list_is_ring[OF assms] by simp
show ?thesis
using canonical_proj_ext_is_hom assms ring_hom_ring.intro[OF ring_axioms ring]
unfolding ring_hom_ring_axioms_def by blast
qed
lemma (in ring) canonical_proj_ext_ker:
assumes "\<And>i. i \<le> (n :: nat) \<Longrightarrow> ideal (I i) R"
shows "a_kernel R (RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n])) (canonical_proj_ext I n) = (\<Inter>i \<le> n. I i)"
proof -
let ?map_Quot = "\<lambda>I n. map (\<lambda>i. R Quot (I i)) [0..< Suc n]"
let ?ker = "\<lambda>I n. a_kernel R (RDirProd_list (?map_Quot I n)) (canonical_proj_ext I n)"
from assms show ?thesis
proof (induct n arbitrary: I)
case 0 then have I: "ideal (I 0) R" by simp
show ?case
unfolding a_kernel_def' RDirProd_list_zero canonical_proj_ext_def FactRing_def
using ideal.rcos_const_imp_mem a_rcos_zero ideal.Icarr I by auto
next
case (Suc n)
hence I: "ideal (I 0) R" by simp
have map_simp: "?map_Quot I (Suc n) = (R Quot I 0) # (?map_Quot (\<lambda>i. I (Suc i)) n)"
by (induct n) (auto)
have ker_I0: "I 0 = a_kernel R (R Quot (I 0)) (\<lambda>a. (I 0) +> a)"
using ideal.rcos_const_imp_mem[OF I] a_rcos_zero[OF I] ideal.Icarr[OF I]
unfolding a_kernel_def' FactRing_def by auto
hence "?ker I (Suc n) = (?ker (\<lambda>i. I (Suc i)) n) \<inter> (I 0)"
unfolding a_kernel_def' map_simp RDirProd_list_zero' canonical_proj_ext_tl by auto
moreover have "?ker (\<lambda>i. I (Suc i)) n = (\<Inter>i \<le> n. I (Suc i))"
using Suc(1)[of "\<lambda>i. I (Suc i)"] Suc(2) by auto
ultimately show ?case
by (auto simp add: INT_extend_simps(10) atMost_atLeast0)
(metis atLeastAtMost_iff le_zero_eq not_less_eq_eq)
qed
qed
lemma (in cring) canonical_proj_ext_is_surj:
assumes "\<And>i. i \<le> n \<Longrightarrow> ideal (I i) R" and "\<And>i j. \<lbrakk> i \<le> n; j \<le> n \<rbrakk> \<Longrightarrow> i \<noteq> j \<Longrightarrow> I i <+> I j = carrier R"
shows "(canonical_proj_ext I n) ` carrier R = carrier (RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n]))"
using assms
proof (induct n arbitrary: I)
case 0 show ?case
by (auto simp add: RDirProd_list_carrier FactRing_def A_RCOSETS_def')
next
{ fix S :: "'c ring" and T :: "'d ring" and f g
assume A: "ring T" "f \<in> ring_hom R S" "g \<in> ring_hom R T" "f ` carrier R \<subseteq> f ` (a_kernel R T g)"
have "(\<lambda>a. (f a, g a)) ` carrier R = (f ` carrier R) \<times> (g ` carrier R)"
proof
show "(\<lambda>a. (f a, g a)) ` carrier R \<subseteq> (f ` carrier R) \<times> (g ` carrier R)"
by blast
next
show "(f ` carrier R) \<times> (g ` carrier R) \<subseteq> (\<lambda>a. (f a, g a)) ` carrier R"
proof
fix t assume "t \<in> (f ` carrier R) \<times> (g ` carrier R)"
then obtain a b where a: "a \<in> carrier R" "f a = fst t" and b: "b \<in> carrier R" "g b = snd t"
by auto
obtain c where c: "c \<in> a_kernel R T g" "f c = f (a \<ominus> b)"
using A(4) minus_closed[OF a(1) b (1)] by auto
have "f (c \<oplus> b) = f (a \<ominus> b) \<oplus>\<^bsub>S\<^esub> f b"
using ring_hom_memE(3)[OF A(2)] b c unfolding a_kernel_def' by auto
hence "f (c \<oplus> b) = f a"
using ring_hom_memE(3)[OF A(2) minus_closed[of a b], of b] a b by algebra
moreover have "g (c \<oplus> b) = g b"
using ring_hom_memE(1,3)[OF A(3)] b(1) c ring.ring_simprules(8)[OF A(1)]
unfolding a_kernel_def' by auto
ultimately have "(\<lambda>a. (f a, g a)) (c \<oplus> b) = t" and "c \<oplus> b \<in> carrier R"
using a b c unfolding a_kernel_def' by auto
thus "t \<in> (\<lambda>a. (f a, g a)) ` carrier R"
by blast
qed
qed } note aux_lemma = this
let ?map_Quot = "\<lambda>I n. map (\<lambda>i. R Quot (I i)) [0..< Suc n]"
let ?DirProd = "\<lambda>I n. RDirProd_list (?map_Quot I n)"
let ?proj = "\<lambda>I n. canonical_proj_ext I n"
case (Suc n)
interpret I: ideal "I 0" R + Inter: ideal "\<Inter>i \<le> n. I (Suc i)" R
using i_Intersect[of "(\<lambda>i. I (Suc i)) ` {..n}"] Suc(2) by auto
have map_simp: "?map_Quot I (Suc n) = (R Quot I 0) # (?map_Quot (\<lambda>i. I (Suc i)) n)"
by (induct n) (auto)
have IH: "(?proj (\<lambda>i. I (Suc i)) n) ` carrier R = carrier (?DirProd (\<lambda>i. I (Suc i)) n)"
and ring: "ring (?DirProd (\<lambda>i. I (Suc i)) n)"
and hom: "?proj (\<lambda>i. I (Suc i)) n \<in> ring_hom R (?DirProd (\<lambda>i. I (Suc i)) n)"
using RDirProd_Quot_list_is_ring[of n "\<lambda>i. I (Suc i)"] Suc(1)[of "\<lambda>i. I (Suc i)"]
canonical_proj_ext_is_hom[of n "\<lambda>i. I (Suc i)"] Suc(2-3) by auto
have ker: "a_kernel R (?DirProd (\<lambda>i. I (Suc i)) n) (?proj (\<lambda>i. I (Suc i)) n) = (\<Inter>i \<le> n. I (Suc i))"
using canonical_proj_ext_ker[of n "\<lambda>i. I (Suc i)"] Suc(2) by auto
have carrier_Quot: "carrier (R Quot (I 0)) = (\<lambda>a. (I 0) +> a) ` carrier R"
by (auto simp add: RDirProd_list_carrier FactRing_def A_RCOSETS_def')
have ring: "ring (?DirProd (\<lambda>i. I (Suc i)) n)"
and hom: "?proj (\<lambda>i. I (Suc i)) n \<in> ring_hom R (?DirProd (\<lambda>i. I (Suc i)) n)"
using RDirProd_Quot_list_is_ring[of n "\<lambda>i. I (Suc i)"]
canonical_proj_ext_is_hom[of n "\<lambda>i. I (Suc i)"] Suc(2) by auto
have "carrier (R Quot (I 0)) \<subseteq> (\<lambda>a. (I 0) +> a) ` (\<Inter>i \<le> n. I (Suc i))"
proof
have "(\<Inter>i \<in> {Suc 0.. Suc n}. I i) <+> (I 0) = carrier R"
using inter_plus_ideal_eq_carrier_arbitrary[of n I 0]
by (simp add: Suc(2-3) atLeast1_atMost_eq_remove0)
hence eq_carrier: "(I 0) <+> (\<Inter>i \<le> n. I (Suc i)) = carrier R"
using set_add_comm[OF I.a_subset Inter.a_subset]
by (metis INT_extend_simps(10) atMost_atLeast0 image_Suc_atLeastAtMost)
fix b assume "b \<in> carrier (R Quot (I 0))"
hence "(b, (\<Inter>i \<le> n. I (Suc i))) \<in> carrier (R Quot I 0) \<times> carrier (R Quot (\<Inter>i\<le>n. I (Suc i)))"
using ring.ring_simprules(2)[OF Inter.quotient_is_ring] by (simp add: FactRing_def)
then obtain s
where "s \<in> carrier R" "(canonical_proj (I 0) (\<Inter>i \<le> n. I (Suc i))) s = (b, (\<Inter>i \<le> n. I (Suc i)))"
using canonical_proj_is_surj[OF I.is_ideal Inter.is_ideal eq_carrier]
unfolding RDirProd_carrier by (metis (no_types, lifting) imageE)
hence "s \<in> (\<Inter>i \<le> n. I (Suc i))" and "(\<lambda>a. (I 0) +> a) s = b"
using Inter.rcos_const_imp_mem by auto
thus "b \<in> (\<lambda>a. (I 0) +> a) ` (\<Inter>i \<le> n. I (Suc i))"
by auto
qed
hence "(\<lambda>a. ((I 0) +> a, ?proj (\<lambda>i. I (Suc i)) n a)) ` carrier R =
carrier (R Quot (I 0)) \<times> carrier (?DirProd (\<lambda>i. I (Suc i)) n)"
using aux_lemma[OF ring I.rcos_ring_hom hom] unfolding carrier_Quot ker IH by simp
moreover show ?case
unfolding map_simp RDirProd_list_carrier sym[OF calculation(1)] canonical_proj_ext_tl by auto
qed
theorem (in cring) chinese_remainder:
assumes "\<And>i. i \<le> n \<Longrightarrow> ideal (I i) R" and "\<And>i j. \<lbrakk> i \<le> n; j \<le> n \<rbrakk> \<Longrightarrow> i \<noteq> j \<Longrightarrow> I i <+> I j = carrier R"
shows "R Quot (\<Inter>i \<le> n. I i) \<simeq> RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n])"
using ring_hom_ring.FactRing_iso[OF canonical_proj_ext_ring_hom, of n I]
canonical_proj_ext_is_surj[of n I] canonical_proj_ext_ker[of n I] assms
by auto
end