Valued fields and their completions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
valuation.basic).
We already know from valuation.topology that one can build a topology on K which
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
a completion hat K which is a topological field. We also prove that K is automatically
separated, so the map from K to hat K is injective.
Then we extend the valuation given on K to a valuation on hat K.
The topology coming from a valuation on a division ring makes it a topological division ring [BouAC, VI.5.1 middle of Proposition 1]
A valued division ring is separated.
A valued field is completable.
The extension of the valuation of a valued field to the completion of the field.
Equations
- valued.extension = valued.extension._proof_1.extend ⇑valued.v
the extension of a valuation on a division ring to its completion.
Equations
- valued.extension_valuation = {to_monoid_with_zero_hom := {to_fun := valued.extension hv, map_zero' := _, map_one' := _, map_mul' := _}, map_add_le_max' := _}