Documentation

Mathlib.Topology.Algebra.Valued.ValuedField

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} [DivisionRing K] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) {x : K} {y : K} {γ : Γ₀ˣ} (y_ne : y 0) (h : v (x - y) < min (γ * (v y * v y)) (v y)) :
v (x⁻¹ - y⁻¹) < γ
@[instance 100]

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

Equations
  • =
@[instance 100]
instance ValuedRing.separated {K : Type u_1} [DivisionRing K] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Valued K Γ₀] :

A valued division ring is separated.

Equations
  • =
theorem Valued.continuous_valuation {K : Type u_1} [DivisionRing K] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [Valued K Γ₀] :
Continuous Valued.v
@[instance 100]
instance Valued.completable {K : Type u_1} [Field K] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] :

A valued field is completable.

Equations
  • =
noncomputable def Valued.extension {K : Type u_1} [Field K] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] :

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

Equations
  • Valued.extension = .extend Valued.v
Instances For
    theorem Valued.continuous_extension {K : Type u_1} [Field K] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] :
    Continuous Valued.extension
    @[simp]
    theorem Valued.extension_extends {K : Type u_1} [Field K] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] (x : K) :
    Valued.extension (K x) = Valued.v x
    noncomputable def Valued.extensionValuation {K : Type u_1} [Field K] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued 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' := }
    Instances For
      theorem Valued.closure_coe_completion_v_lt {K : Type u_1} [Field K] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] {γ : Γ₀ˣ} :
      closure (K '' {x : K | Valued.v x < γ}) = {x : UniformSpace.Completion K | Valued.extensionValuation x < γ}
      noncomputable instance Valued.valuedCompletion {K : Type u_1} [Field K] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] :
      Equations
      • Valued.valuedCompletion = Valued.mk Valued.extensionValuation
      @[simp]
      theorem Valued.valuedCompletion_apply {K : Type u_1} [Field K] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] (x : K) :
      Valued.v (K x) = Valued.v x
      @[reducible]
      def Valued.integer (K : Type u_1) [Field K] {Γ₀ : outParam (Type u_2)} [LinearOrderedCommGroupWithZero Γ₀] [vK : Valued K Γ₀] :

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

      Equations
      Instances For

        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.
        Instances For
          @[reducible]
          def Valued.maximalIdeal (K : Type u_1) [Field K] {Γ₀ : outParam (Type u_2)} [LinearOrderedCommGroupWithZero Γ₀] [vK : Valued K Γ₀] :

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

          Equations
          Instances For

            An abbrevation for LocalRing.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.
            Instances For
              @[reducible]
              def Valued.ResidueField (K : Type u_1) [Field K] {Γ₀ : outParam (Type u_2)} [LinearOrderedCommGroupWithZero Γ₀] [vK : Valued K Γ₀] :
              Type u_1

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

              Equations
              Instances For

                An abbrevation for LocalRing.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.
                Instances For