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
The topology coming from a valuation on a division ring makes it a topological division ring [BouAC, VI.5.1 middle of Proposition 1]
The extension of the valuation of a valued field to the completion of the field.
the extension of a valuation on a division ring to its completion.