I've been reading Bosch's book "Lectures on Formal and Rigid Geometry". In the proof of Theorem 6 on page 26, which I will show below, he claimed that there is a subspace $V'$ of a complete normed $K$-vector space $V$ with $(y_{\mu})_{\mu \in M}$ as its orthonormal basis. However, I wonder how to construct this subspace explicitly.
Theorem 6. Let $K$ be a field with a complete valuation, and $V$ a complete normed $K$-vector space with an orthonormal basis $(x_{\nu})_{\nu \in N}$. Write $R$ for the valuation ring of $K$, and consider a system of elements $$y_{\mu}=\sum_{\mu \in M}c_{\mu\nu}x_{\nu} \in V^{o}, \mu \in M$$ where the smallest subring of $R$ containing all coefficients $c_{\mu\nu}$ is bald. Then, if the residue classes $\tilde{y}_\mu \in \tilde{V}$ form a $k$-basis of $\tilde{V}$, the elements $y_\mu$ form an orthonormal basis of $V$.
Proof:
The systems $(x_{\nu})_{\nu \in N}$ and$y_{\mu}=\sum_{\mu \in M}$ form a $k$-basis of $\tilde{V}$. So $M$ and $N$ have the same cardinality, and $M$ is at most countable. In particular, $y_{\mu}=\sum_{\mu \in M}$ is an orthonormal basis of a subspace $V' \subset V$. ...
Also perhaps I should give the definition of $\tilde{V}$, which is $$\tilde{V}=\{x\in V:|x|\leq 1\}/ \{x\in V:|x| < 1\}$$ And the definition of an orthonormal basis: Let $V$ be a $K$-vector space. A system $(x_{\nu})_{\nu \in N}$ of elements in $V$, where $N$ is finite or at most countable, is called a (topological) orthonormal basis of $V$ if the following hold:
- $|x_\mu|=1$ for all $\mu \in N$.
- Each $x\in V$ can be written as convergent series $x=\sum_{\mu \in N}c_{\mu}x_{\mu}$ with coefficients $c_{\mu} \in K$.
- For each equation $x=\sum_{\mu \in N}c_{\mu}x_{\mu}$ as in (2) we have $|x|=$max$_{\mu \in N}|c_{\mu}|$. In particular, the coefficients $c_{\mu}$ in (2) are unique.
Thanks for reminding me. I should add the definition of "bald" as well:
A ring $R$ with a multiplicative ring norm $|\cdot|$ such that $|a|\leq 1$
for all $a\in R$ is called bald if
$$\text{sup}\{|a|:a\in R, |a|<1\}<1$$
A ring norm on R is a map $|\cdot|:R\rightarrow \mathbb{R}_{\geq0}$ satisfying:
- $|a|=0 \Leftrightarrow a=0$
- $|ab|\leq |a||b|$
- $|1|\leq 1$
- $|a+b|\leq \text{max}\{|a|,|b|\}$
(and the norm is called multiplicative if instead of (2) we have $|ab|=|a||b|$)