Proof.
First we assume that is non-trivial.
Let us begin with the following:
Claim 4.1.1.
There are a positive integer and a finitely generated lattice of
such that
|
|
|
Proof.
First we assume that is discrete.
We choose a positive integer such that .
We set
.
Note that is a finitely generated lattice of
by Proposition 1.17.
As
by Proposition 1.17, we have
the assertion.
Next we assume that is not discrete.
By Proposition 1.18,
there is a lattice of such that .
By Proposition 1.19,
there is a finitely generated lattice of such that
and
, as desired.
∎
Let be the Zariski closure of in
(cf. §1.1.7) and
.
Moreover, let be a continuous metric of given by
|
|
|
Then, by Proposition 3.8 and Remark 3.9,
.
Therefore, by virtue of Theorem 3.2,
there are a positive integer and such that
and
| (5) |
|
|
|
As , we have
|
|
|
for all . Therefore, by Proposition 3.6,
| (6) |
|
|
|
for all . In particular, .
Therefore,
| (7) |
|
|
|
On the other hand, by using (6),
| (8) |
|
|
|
Thus the assertion follows from (5),
(7) and (8).
Next we assume that is trivial.
Clearly we may assume that .
Let be the field of formal Laurent power series over , that is,
the quotient field of the ring of formal power series over .
We set
|
|
|
As
is a finite set
by (1) in Lemma 1.12, we have
. Therefore, we can find .
Here we consider an absolute value of given by
|
|
|
We set
|
|
|
Note that .
Let be a continuous metric of given by the scalar extension of .
Then, by Lemma 3.7, is given by
|
|
|
where is the scalar extension of .
Moreover, for ,
for ,
where is the projection. Note that
is surjective. Therefore, for all .
By the previous observation,
there are a positive integer and such that
|
|
|
Note that, for a positive integer ,
|
|
|
Thus we may assume that is surjective.
Let be an orthogonal basis of with respect to
such that
forms a basis of
(cf. Proposition 1.3).
We set
|
|
|
for some .
As
and forms a basis of
, we have .
Note that
|
|
|
so that, by (2) in Lemma 1.12 and
Remark 1.13, forms an orthogonal
basis of with respect to .
Therefore, if we set ,
then , and
|
|
|
|
|
|
|
|
|
|
|
|
as required.
∎