Completion of valuations #

This file defines the extension of a valuation on a field K to its uniform completion Completion K, assuming the valuation is compatible with the topology on K.

Main definitions #

Valuation.extension : extends a valuation on a field K to Completion K, provided the valuation is compatible with the topology on K.
UniformSpace.Completion.valuativeRel : the valuative relation on Completion K, extending the one on K that is compatible (in the sense of Valuation.Compatible) with the topology.

Main statements #

Valuation.hasBasis_nhds_coe_zero : the neighbourhoods of 0 in the completion of K have a basis given by the open balls of v.extension.restrict.
UniformSpace.Completion.isValuativeTopology : the extended valuative relation on Completion K is compatible with the topology.
Valuation.compatible_extension : if v is compatible with the valuative relation on K, then v.extension is compatible with the valuative relation on Completion K.
Valuation.isEquiv_extension : if v and v' are two valuations compatible with the valuative relation on K, then v.extension and v'.extension are equivalent to each other.

TODO #

The current approach relies on the field structure of K, it can be generalized to arbitrary commutative rings.

Generalize WithZeroTopology.topologicalSpace to LinearOrderedCommMonoidWithZero and upgrade it to WithZeroTopology.uniformSpace.
Generalize Valuation.extension from fields to arbitrary commutative rings by first showing that the original valuation is uniformly continuous.
Split this file into two parts: one about valuation extension in general, and another about the theory specific to valued fields (the DivisionRing and Field sections).

source

theorem IsValuativeTopology.continuousAt_valuation_of_ne_zero {R : Type u_1} {Γ₀ : Type u_3} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] [v.Compatible] [TopologicalSpace Γ₀] {x : R} (h : v x ≠ 0) :

ContinuousAt (⇑v) x

A compatible valuation is continuous, at every point where it does not vanish, for any topology on Γ₀.

source

theorem IsValuativeTopology.eventually_lt_nhds_zero {R : Type u_1} {Γ₀ : Type u_3} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] [v.Compatible] {y : R} (hy : v y ≠ 0) :

∀ᶠ (x : R) in nhds 0, v x < v y

For y : K with v y ≠ 0, the open ball {x | v x < v y} is a neighbourhood of 0.

source

theorem Valuation.inversion_estimate {K : Type u_2} {Γ₀ : Type u_3} [DivisionRing K] [LinearOrderedCommGroupWithZero Γ₀] (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

theorem Valuation.inversion_estimate' {K : Type u_2} {Γ₀ : Type u_3} [DivisionRing K] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) {x y r s : K} (y_ne : y ≠ 0) (hr : r ≠ 0) (hs : s ≠ 0) (h : v (x - y) < min (v s / v r * (v y * v y)) (v y)) :

v (x⁻¹ - y⁻¹) * v r < v s

A variant of Valuation.inversion_estimate specialized to the case γ = v s / v r.

source

@[instance 100]

instance IsValuativeTopology.instIsTopologicalDivisionRing {K : Type u_2} [DivisionRing K] [ValuativeRel K] [TopologicalSpace K] [IsValuativeTopology K] :

IsTopologicalDivisionRing K

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

source

@[instance 100]

instance IsValuativeTopology.instT2Space {K : Type u_2} [DivisionRing K] [ValuativeRel K] [TopologicalSpace K] [IsValuativeTopology K] :

T2Space K

A division ring with topology coming from a valuation is a Hausdorff space.

source

theorem IsValuativeTopology.continuous_valuation_of_surjective {K : Type u_2} {Γ₀ : Type u_3} [DivisionRing K] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) [ValuativeRel K] [TopologicalSpace K] [IsValuativeTopology K] [v.Compatible] (hsurj : Function.Surjective ⇑v) :

Continuous ⇑v

source

theorem IsValuativeTopology.continuous_restrict {K : Type u_2} {Γ₀ : Type u_3} [DivisionRing K] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) [ValuativeRel K] [TopologicalSpace K] [IsValuativeTopology K] [v.Compatible] :

Continuous ⇑v.restrict

Restricting the codomain of a valuation to ValueGroup₀ (equipped with WithZeroTopology) makes it continuous. Without this restriction, it is not continuous in general.

source

theorem IsValuativeTopology.isClosedMap_restrict {K : Type u_2} {Γ₀ : Type u_3} [DivisionRing K] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) [ValuativeRel K] [TopologicalSpace K] [IsValuativeTopology K] [v.Compatible] :

IsClosedMap ⇑v.restrict

source

@[instance 100]

instance IsValuativeTopology.instCompletableTopFieldOfIsUniformAddGroup {K : Type u_2} [Field K] [ValuativeRel K] [UniformSpace K] [IsValuativeTopology K] [IsUniformAddGroup K] :

CompletableTopField K

A valued field is completable.

source

theorem Valuation.exists_eventually_map_eq {K : Type u_2} {Γ₀ : Type u_3} [Field K] [ValuativeRel K] [UniformSpace K] [IsValuativeTopology K] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) [v.Compatible] [IsUniformAddGroup K] {x₀ : UniformSpace.Completion K} (hx₀ : x₀ ≠ 0) :

∃ (z₀ : K), z₀ ≠ 0 ∧ ∀ᶠ (x : K) in Filter.comap UniformSpace.Completion.coe' (nhds x₀), v x = v z₀

For a nonzero element x₀ of the completion of K, the valuation v is constant on the elements of K close to x₀, with value v z₀ for any z₀ : K close enough to x₀.

source

noncomputable def Valuation.extension {K : Type u_2} {Γ₀ : Type u_3} [Field K] [ValuativeRel K] [UniformSpace K] [IsValuativeTopology K] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) [v.Compatible] [IsUniformAddGroup K] :

Valuation (UniformSpace.Completion K) Γ₀

The extension of a valuation on a field to its completion.

Equations

v.extension = { toFun := ⇑MonoidWithZeroHom.ValueGroup₀.embedding ∘ Valuation.extensionFun✝ v, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯, map_add_le_max' := ⋯ }

Instances For

source

@[simp]

theorem Valuation.extension_apply_coe {K : Type u_2} {Γ₀ : Type u_3} [Field K] [ValuativeRel K] [UniformSpace K] [IsValuativeTopology K] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) [v.Compatible] [IsUniformAddGroup K] (x : K) :

v.extension ↑x = v x

source

theorem Valuation.extension_locally_const {K : Type u_2} {Γ₀ : Type u_3} [Field K] [ValuativeRel K] [UniformSpace K] [IsValuativeTopology K] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) [v.Compatible] [IsUniformAddGroup K] {x : UniformSpace.Completion K} (h : x ≠ 0) :

{y : UniformSpace.Completion K | v.extension y = v.extension x} ∈ nhds x

The extension of v to the completion of K is locally constant away from 0.

source

theorem Valuation.exists_coe_mem_extension_eq {K : Type u_2} {Γ₀ : Type u_3} [Field K] [ValuativeRel K] [UniformSpace K] [IsValuativeTopology K] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) [v.Compatible] [IsUniformAddGroup K] {x : UniformSpace.Completion K} {U : Set (UniformSpace.Completion K)} (hU : U ∈ nhds x) :

∃ (r : K), ↑r ∈ U ∧ v.extension x = v r

Every neighbourhood of x in the completion of K contains an element r of K with v r = v.extension x.

source

theorem Valuation.exists_coe_mem_extension_eq₂ {K : Type u_2} {Γ₀ : Type u_3} [Field K] [ValuativeRel K] [UniformSpace K] [IsValuativeTopology K] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) [v.Compatible] [IsUniformAddGroup K] {x y : UniformSpace.Completion K} {U : Set (UniformSpace.Completion K × UniformSpace.Completion K)} (hU : U ∈ nhds (x, y)) :

∃ (r : K) (s : K), (↑r, ↑s) ∈ U ∧ v.extension x = v r ∧ v.extension y = v s

Every neighbourhood of (x, y) in Completion K × Completion K contains a pair (r, s) of elements of K with v r = v.extension x and v s = v.extension y.

source

theorem Valuation.exists_extension_eq_map {K : Type u_2} {Γ₀ : Type u_3} [Field K] [ValuativeRel K] [UniformSpace K] [IsValuativeTopology K] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) [v.Compatible] [IsUniformAddGroup K] (x : UniformSpace.Completion K) :

∃ (r : K), v.extension x = v r

source

theorem Valuation.closure_image_coe_le {K : Type u_2} {Γ₀ : Type u_3} [Field K] [ValuativeRel K] [UniformSpace K] [IsValuativeTopology K] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) [v.Compatible] [IsUniformAddGroup K] :

closure (Prod.map UniformSpace.Completion.coe' UniformSpace.Completion.coe' '' {(x, y) : K × K | v x ≤ v y}) = {(x, y) : UniformSpace.Completion K × UniformSpace.Completion K | v.extension x ≤ v.extension y}

source

theorem Valuation.closure_image_coe_ofPred_map_lt {K : Type u_2} {Γ₀ : Type u_3} [Field K] [ValuativeRel K] [UniformSpace K] [IsValuativeTopology K] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) [v.Compatible] [IsUniformAddGroup K] {r : Γ₀} (hr : r ≠ 0) :

closure (UniformSpace.Completion.coe' '' {x : K | v x < r}) = {x : UniformSpace.Completion K | v.extension x < r}

[Bou89] VI §5 no.3 Proposition 5 (d)

source

theorem Valuation.closure_image_coe_ofPred_map_mul_map_lt_map {K : Type u_2} {Γ₀ : Type u_3} [Field K] [ValuativeRel K] [UniformSpace K] [IsValuativeTopology K] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) [v.Compatible] [IsUniformAddGroup K] {r s : K} (hr : r ≠ 0) (hs : s ≠ 0) :

closure (UniformSpace.Completion.coe' '' {x : K | v x * v r < v s}) = {x : UniformSpace.Completion K | v.extension x * v r < v s}

source

noncomputable def Valuation.valueGroup₀ExtensionHom {K : Type u_2} {Γ₀ : Type u_3} [Field K] [ValuativeRel K] [UniformSpace K] [IsValuativeTopology K] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) [v.Compatible] [IsUniformAddGroup K] :

(↑v).ValueGroup₀ →*₀ (↑v.extension).ValueGroup₀

The zero-preserving monoid homomorphism from the ValueGroup₀ of the valuation on K to that of the extension to its completion. It will be upgraded to an MulEquiv later, see valueGroup₀ExtensionEquiv.

Equations

v.valueGroup₀ExtensionHom = { toFun := Valuation.valueGroup₀ExtensionHomFun✝ v, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source

@[simp]

theorem Valuation.embedding_valueGroup₀ExtensionHom {K : Type u_2} {Γ₀ : Type u_3} [Field K] [ValuativeRel K] [UniformSpace K] [IsValuativeTopology K] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) [v.Compatible] [IsUniformAddGroup K] (a : (↑v).ValueGroup₀) :

MonoidWithZeroHom.ValueGroup₀.embedding (v.valueGroup₀ExtensionHom a) = MonoidWithZeroHom.ValueGroup₀.embedding a

source

@[simp]

theorem Valuation.valueGroup₀ExtensionHom_restrict {K : Type u_2} {Γ₀ : Type u_3} [Field K] [ValuativeRel K] [UniformSpace K] [IsValuativeTopology K] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) [v.Compatible] [IsUniformAddGroup K] (x : K) :

v.valueGroup₀ExtensionHom (v.restrict x) = v.extension.restrict ↑x

source

noncomputable def Valuation.valueGroup₀ExtensionEquiv {K : Type u_2} {Γ₀ : Type u_3} [Field K] [ValuativeRel K] [UniformSpace K] [IsValuativeTopology K] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) [v.Compatible] [IsUniformAddGroup K] :

(↑v).ValueGroup₀ ≃* (↑v.extension).ValueGroup₀

The isomorphism from the ValueGroup₀ of the valuation on K to that of the extension to its completion.

Equations

v.valueGroup₀ExtensionEquiv = MulEquiv.ofBijective v.valueGroup₀ExtensionHom ⋯

Instances For

source

@[simp]

theorem Valuation.embedding_valueGroup₀ExtensionEquiv {K : Type u_2} {Γ₀ : Type u_3} [Field K] [ValuativeRel K] [UniformSpace K] [IsValuativeTopology K] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) [v.Compatible] [IsUniformAddGroup K] (a : (↑v).ValueGroup₀) :

MonoidWithZeroHom.ValueGroup₀.embedding (v.valueGroup₀ExtensionEquiv a) = MonoidWithZeroHom.ValueGroup₀.embedding a

source

@[simp]

theorem Valuation.embedding_valueGroup₀ExtensionEquiv_symm {K : Type u_2} {Γ₀ : Type u_3} [Field K] [ValuativeRel K] [UniformSpace K] [IsValuativeTopology K] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) [v.Compatible] [IsUniformAddGroup K] (a : (↑v.extension).ValueGroup₀) :

MonoidWithZeroHom.ValueGroup₀.embedding (v.valueGroup₀ExtensionEquiv.symm a) = MonoidWithZeroHom.ValueGroup₀.embedding a

source

theorem Valuation.closure_image_coe_ofPred_restrict_lt {K : Type u_2} {Γ₀ : Type u_3} [Field K] [ValuativeRel K] [UniformSpace K] [IsValuativeTopology K] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) [v.Compatible] [IsUniformAddGroup K] (γ : (↑v).ValueGroup₀ˣ) :

closure (UniformSpace.Completion.coe' '' {x : K | v.restrict x < ↑γ}) = {x : UniformSpace.Completion K | v.extension x < MonoidWithZeroHom.ValueGroup₀.embedding ↑γ}

Valuation.closure_image_coe_ofPred_map_lt, stated for the open balls of v.restrict.

source

theorem Valuation.hasBasis_nhds_coe_zero {K : Type u_2} {Γ₀ : Type u_3} [Field K] [ValuativeRel K] [UniformSpace K] [IsValuativeTopology K] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) [v.Compatible] [IsUniformAddGroup K] :

(nhds 0).HasBasis (fun (x : (↑v.extension).ValueGroup₀ˣ) => True) fun (γ : (↑v.extension).ValueGroup₀ˣ) => {x : UniformSpace.Completion K | v.extension.restrict x < ↑γ}

The neighbourhoods of 0 in the completion of K have a basis given by the open balls of v.extension.restrict. This is Valuation.hasBasis_nhds_zero for v.extension, proved before the instance IsValuativeTopology (Completion K) is available.

source

@[instance_reducible]