Valued fields and their completions #
In this file we study the topology of a field
K endowed with a valuation (in our application
to adic spaces,
K will be the valuation field associated to some valuation on a ring, defined in
We already know from valuation.topology that one can build a topology on
makes it a topological ring.
The first goal is to show
K is a topological field, ie inversion is continuous
at every non-zero element.
The next goal is to prove
K is a completable topological field. This gives us
hat K which is a topological field. We also prove that
K is automatically
separated, so the map from
hat K is injective.
Then we extend the valuation given on
K to a valuation on