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 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.

source

theorem valuation.inversion_estimate {K : Type u_1} [division_ring K] {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] (v : valuation K Γ₀) {x y : K} {γ : Γ₀ˣ} (y_ne : y ≠ 0) (h : ⇑v (x - y) < min ((↑γ) * (⇑v y) * ⇑v y) (⇑v y)) :

⇑v (x⁻¹ - y⁻¹) < ↑γ

source

@[protected, instance]

def valued.topological_division_ring {K : Type u_1} [division_ring K] {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [valued K Γ₀] :

topological_division_ring 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]

source

@[protected, instance]

def valued_ring.separated {K : Type u_1} [division_ring K] {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [valued K Γ₀] :

separated_space K

A valued division ring is separated.

source

theorem valued.continuous_valuation {K : Type u_1} [division_ring K] {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [valued K Γ₀] :

continuous ⇑valued.v

source

@[protected, instance]

def valued.completable {K : Type u_1} [field K] {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [hv : valued K Γ₀] :

completable_top_field K

A valued field is completable.

source

noncomputable def valued.extension {K : Type u_1} [field K] {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [hv : valued K Γ₀] :

uniform_space.completion K → Γ₀

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

source

theorem valued.continuous_extension {K : Type u_1} [field K] {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [hv : valued K Γ₀] :

continuous valued.extension

source

@[norm_cast]

theorem valued.extension_extends {K : Type u_1} [field K] {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [hv : valued K Γ₀] (x : K) :

valued.extension ↑x = ⇑valued.v x

source

noncomputable def valued.extension_valuation {K : Type u_1} [field K] {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [hv : valued K Γ₀] :

valuation (uniform_space.completion K) Γ₀

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' := _}