mathlib documentation

topology.algebra.valued_field

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.

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) < linear_order.min (γ * (v y * v y)) (v y)) :
v (x⁻¹ - y⁻¹) < γ
@[protected, instance]

The topology coming from a valuation on a division ring makes it a topological division ring [BouAC, VI.5.1 middle of Proposition 1]

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

A valued division ring is separated.

theorem valued.continuous_valuation {K : Type u_1} [division_ring K] {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [valued K Γ₀] :
@[protected, instance]
def valued.completable {K : Type u_1} [field K] {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [hv : valued K Γ₀] :

A valued field is completable.

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

The extension of the valuation of a valued field to the completion of the field.

Equations
theorem valued.continuous_extension {K : Type u_1} [field K] {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [hv : valued K Γ₀] :
@[simp, 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) :
noncomputable def valued.extension_valuation {K : Type u_1} [field K] {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [hv : valued K Γ₀] :

the extension of a valuation on a division ring to its completion.

Equations
theorem valued.closure_coe_completion_v_lt {K : Type u_1} [field K] {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [hv : valued K Γ₀] {γ : Γ₀ˣ} :