We start with the elementary case of the
Chinese Remaindering Theorem
(Theorem 1).
Then we give a much more abstract version
(Theorem 2).
Then we state the Chinese Remaindering Theorem
and
the
Chinese Remaindering Algorithm
in the context of Euclidean domains.
Proof.
First observe that Relation (
46) implies
 |
(48) |
Now assume that

holds.
This implies
 |
(49) |
Thus Relations (
48) and (
49) lead to
 |
(50) |
Conversly
-
implies
that is
divides
and
-
implies
that is
divides
.
Since

and

are relatively prime it follows that

divides

.
(Gauss Lemma).
Proof.
The first statement is obvious.
Let us prove the second one.
Let

be in

.
We look for the pre-image of

.
Hence we look for

such that
 |
(53) |
that is
 |
(54) |
or
 |
(55) |
At this point of the proof we need the following lemma.
Proof.
The equation

means that the residue classe of

in

is equal
to the residue classe of

in

.
More formally we have
 |
(57) |
or equivalently
 |
(58) |
Since these sets are non empty this implies
 |
(59) |
Since

is an ideal we have

and thus
 |
(60) |
The lemma is proved.
CONTINUING THEOREM'S
Proof.
With the previous lemma
Relation (
55),
for all

such that

holds, leads to
 |
(61) |
or equivalently
 |
(62) |
Relation (
62) is a necessary condition
for the existence of a pre-image of

via the homomorphism

.
Therefore we proved the second statement of the theorem.
Let us prove the third one.
Let us ssume first that
is surjective.
Let
be such that
.
There exists
such that
 |
(63) |
Hence
 |
(64) |
which implies

.
Conversly, let us assume that the ideals

are pairwise coprime.
Let

be in the range

and consider
the product

of all ideals

except

.
It is a classical result that

and

are coprime.
Let

and

such that

.
Observe that for all

we have
 |
(65) |
Now consider

.
Then
 |
(66) |
satisfies
 |
(67) |
This concludes the proof of the theorem.
Proof.
The following ring isomorphism follows from Theorem
2
 |
(70) |
It is a well known fact that if the ideals

are pairwise coprime
(

for every

with

)
then their product is equal to their intersection [
van91].
Therefore, we have the ring isomorphism of the statement.
The group isomorphism follows from the previous ring isomorphism
and the fact that the element
 |
(71) |
is a unit iff every

is a unit of

.
From now on
denotes an Euclidean domain.
Proof.
Assume that the algorithm terminates without error,
that is the case if every

is
the gcd of

and

(which are assumed to be coprime).
Then, for

we have
 |
(74) |
Hence
 |
(75) |
and for

with

we have
 |
(76) |
The specification of Algorithm
4 follow
easily from Relation (
75) and (
76).
Proof.
Except for the complexity result (that can be found
in [
GG99] as Theorem 5.7) and the uniqueness, this theorem follows
from Algorithm
4.
The uniqueness follows from the constraint

.
Indeed, assume that there are two polynomials

and

solutions
of (
80).
Then we have
 |
(81) |
and thus
 |
(82) |
Hence

divides

although

holds.
Therefore

.
Proof.
Except for the complexity result (that can be found
in [
GG99] as Theorem 5.8) and the uniqueness,
this theorem follows
from Algorithm
4.
The proof of the uniqueness is quite easy to establish.
We reproduce below the ALDOR code for the Chinese Remaindering Algorithm.
More precisely, the operation interpolate satisfies exactly the
specification of Algorithm 4.
After the definition of the ChineseRemaindering domain
we prove that its operation combine satisifies the
specification of Algorithm 4
for the case of two moduli
and
.
The reader is left with the proof of the operation interpolate
which implements the general case (with
moduli).
ChineseRemaindering(E: EuclideanDomain): with {
combine: (E, E) -> (E, E) -> E;
interpolate: (List E, List E) -> E;
} == add {
combine(m1: E, m2: E): (E, E) -> E == {
local u1: E;
assert(m1 = unitCanonical m1);
assert(m2 = unitCanonical m2);
fn(r1: E, r2: E): E == {
r1__new := r1 rem m1;
r := (r2 - r1__new) rem m2 ;
r := (r * u1) rem m2 ;
r := r1__new + r * m1;
}
(u1, u2, g) := extendedEuclidean(m1, m2);
fn
}
interpolate(lm: List E, lr: List E): E == {
m := first lm;
r := first lr rem m;
for mi in rest lm for ri in rest lr repeat {
r := combine(m, mi)(r, ri);
m := m * mi;
}
return r;
}
}
Marc Moreno Maza
2008-01-07