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, i.e. 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} [DivisionRing K] {Γ₀ : Type u_2} [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⁻¹) < ↑γ

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

@[instance 100]

instance Valued.isTopologicalDivisionRing {K : Type u_1} [DivisionRing K] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Valued K Γ₀] : IsTopologicalDivisionRing 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]

@[instance 100]

instance ValuedRing.separated {K : Type u_1} [DivisionRing K] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Valued K Γ₀] : T0Space K

A valued division ring is separated.

theorem Valued.continuous_valuation {K : Type u_1} [DivisionRing K] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Valued K Γ₀] : Continuous ⇑v

@[instance 100]

instance Valued.completable {K : Type u_1} [Field K] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] : CompletableTopField K

A valued field is completable.

theorem Valued.valuation_isClosedMap {K : Type u_1} [Field K] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] : IsClosedMap ⇑v

noncomputable def Valued.extension {K : Type u_1} [Field K] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] : UniformSpace.Completion K → Γ₀

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

Equations

• Valued.extension = ⋯.extend ⇑Valued.v

theorem Valued.continuous_extension {K : Type u_1} [Field K] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] : Continuous extension

@[simp]

theorem Valued.extension_extends {K : Type u_1} [Field K] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] (x : K) : extension ↑x = v x

noncomputable def Valued.extensionValuation {K : Type u_1} [Field K] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] : Valuation (UniformSpace.Completion K) Γ₀

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

Equations

• Valued.extensionValuation = { toFun := Valued.extension, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯, map_add_le_max' := ⋯ }

@[simp]

theorem Valued.extensionValuation_apply_coe {K : Type u_1} [Field K] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] (x : K) : extensionValuation ↑x = v x

@[simp]

theorem Valued.extension_eq_zero_iff {K : Type u_1} [Field K] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] {x : UniformSpace.Completion K} : extension x = 0 ↔ x = 0

theorem Valued.continuous_extensionValuation {K : Type u_1} [Field K] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] : Continuous ⇑extensionValuation

theorem Valued.exists_coe_eq_v {K : Type u_1} [Field K] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] (x : UniformSpace.Completion K) : ∃ (r : K), extensionValuation x = v r

theorem Valued.closure_coe_completion_v_lt {K : Type u_1} [Field K] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] {γ : Γ₀ˣ} : closure (UniformSpace.Completion.coe' '' {x : K | v x < ↑γ}) = {x : UniformSpace.Completion K | extensionValuation x < ↑γ}

theorem Valued.closure_coe_completion_v_mul_v_lt {K : Type u_1} [Field K] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued 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 | extensionValuation x * v r < v s}

noncomputable instance Valued.valuedCompletion {K : Type u_1} [Field K] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] : Valued (UniformSpace.Completion K) Γ₀

Equations

• Valued.valuedCompletion = { toUniformSpace := UniformSpace.Completion.uniformSpace K, toIsUniformAddGroup := ⋯, v := Valued.extensionValuation, is_topological_valuation := ⋯ }

@[simp]

theorem Valued.valuedCompletion_apply {K : Type u_1} [Field K] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] (x : K) : v ↑x = v x

theorem Valued.valuedCompletion_surjective_iff {K : Type u_1} [Field K] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] : Function.Surjective ⇑v ↔ Function.Surjective ⇑v

instance Valued.instFaithfulSMulCompletionOfUniformContinuousConstSMul {K : Type u_1} [Field K] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] {R : Type u_3} [CommSemiring R] [Algebra R K] [UniformContinuousConstSMul R K] [FaithfulSMul R K] : FaithfulSMul R (UniformSpace.Completion K)

@[reducible]

def Valued.integer (K : Type u_1) [Field K] {Γ₀ : outParam (Type u_2)} [LinearOrderedCommGroupWithZero Γ₀] [vK : Valued K Γ₀] : Subring K

A Valued version of Valuation.integer, enabling the notation 𝒪[K] for the valuation integers of a valued field K.

Equations

• Valued.integer K = Valued.v.integer

def Valued.«term𝒪[_]» : Lean.ParserDescr

A Valued version of Valuation.integer, enabling the notation 𝒪[K] for the valuation integers of a valued field K.

Equations

• One or more equations did not get rendered due to their size.

@[reducible]

def Valued.maximalIdeal (K : Type u_1) [Field K] {Γ₀ : outParam (Type u_2)} [LinearOrderedCommGroupWithZero Γ₀] [vK : Valued K Γ₀] : Ideal ↥(integer K)

An abbreviation for IsLocalRing.maximalIdeal 𝒪[K] of a valued field K, enabling the notation 𝓂[K] for the maximal ideal in 𝒪[K] of a valued field K.

Equations

• Valued.maximalIdeal K = IsLocalRing.maximalIdeal ↥(Valued.integer K)

def Valued.«term𝓂[_]» : Lean.ParserDescr

An abbreviation for IsLocalRing.maximalIdeal 𝒪[K] of a valued field K, enabling the notation 𝓂[K] for the maximal ideal in 𝒪[K] of a valued field K.

Equations

• One or more equations did not get rendered due to their size.

@[reducible]

def Valued.ResidueField (K : Type u_1) [Field K] {Γ₀ : outParam (Type u_2)} [LinearOrderedCommGroupWithZero Γ₀] [vK : Valued K Γ₀] : Type u_1

An abbreviation for IsLocalRing.ResidueField 𝒪[K] of a Valued instance, enabling the notation 𝓀[K] for the residue field of a valued field K.

Equations

• Valued.ResidueField K = IsLocalRing.ResidueField ↥(Valued.integer K)

def Valued.«term𝓀[_]» : Lean.ParserDescr

An abbreviation for IsLocalRing.ResidueField 𝒪[K] of a Valued instance, enabling the notation 𝓀[K] for the residue field of a valued field K.

Equations

• One or more equations did not get rendered due to their size.