Documentation

Mathlib.Topology.Algebra.Valued.NormedValued

Correspondence between nontrivial nonarchimedean norms and rank one valuations #

Nontrivial nonarchimedean norms correspond to rank one valuations.

Main Definitions #

Tags #

norm, nonarchimedean, nontrivial, valuation, rank one

source
def NormedField.valuation {K : Type u_1} [hK : NormedField K] [IsUltrametricDist K] :
Valuation K NNReal

The valuation on a nonarchimedean normed field K defined as nnnorm.

Equations
    Instances For
      source
      @[simp]
      theorem NormedField.valuation_apply {K : Type u_1} [hK : NormedField K] [IsUltrametricDist K] (x : K) :
      valuation x = ‖x‖₊
      source
      def NormedField.toValued {K : Type u_1} [hK : NormedField K] [IsUltrametricDist K] :
      Valued K NNReal

      The valued field structure on a nonarchimedean normed field K, determined by the norm.

      Equations
        Instances For
          source
          instance NormedField.instRankOneNNRealValuation {K : Type u_2} [NontriviallyNormedField K] [IsUltrametricDist K] :
          valuation.RankOne
          Equations
            source
            def Valued.norm {L : Type u_1} [Field L] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : v.RankOne] :
            L → ℝ

            The norm function determined by a rank one valuation on a field L.

            Equations
              Instances For
                source
                theorem Valued.norm_def {L : Type u_1} [Field L] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : v.RankOne] {x : L} :
                norm x = ↑((Valuation.RankOne.hom v) (v x))
                source
                theorem Valued.norm_nonneg {L : Type u_1} [Field L] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : v.RankOne] (x : L) :
                0 ≤ norm x
                source
                theorem Valued.norm_add_le {L : Type u_1} [Field L] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : v.RankOne] (x y : L) :
                norm (x + y) ≤ max (norm x) (norm y)
                source
                theorem Valued.norm_eq_zero {L : Type u_1} [Field L] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : v.RankOne] {x : L} (hx : norm x = 0) :
                x = 0
                source
                theorem Valued.norm_pos_iff_valuation_pos {L : Type u_1} [Field L] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : v.RankOne] {x : L} :
                0 < norm x ↔ 0 < v x
                source
                def Valued.toNormedField (L : Type u_1) [Field L] (Γ₀ : Type u_2) [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : v.RankOne] :
                NormedField L

                The normed field structure determined by a rank one valuation.

                Equations
                  Instances For
                    source
                    theorem Valued.isNonarchimedean_norm (L : Type u_1) [Field L] (Γ₀ : Type u_2) [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : v.RankOne] :
                    IsNonarchimedean fun (x : L) => ‖x‖
                    source
                    instance Valued.instIsUltrametricDist (L : Type u_1) [Field L] (Γ₀ : Type u_2) [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : v.RankOne] :
                    IsUltrametricDist L
                    source
                    theorem Valued.coe_valuation_eq_rankOne_hom_comp_valuation (L : Type u_1) [Field L] (Γ₀ : Type u_2) [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : v.RankOne] :
                    ⇑NormedField.valuation = ⇑(Valuation.RankOne.hom v) ∘ ⇑v
                    source
                    @[simp]
                    theorem Valued.toNormedField.norm_le_iff {L : Type u_1} [Field L] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : v.RankOne] {x x' : L} :
                    ‖x‖ ≤ ‖x'‖ ↔ v x ≤ v x'
                    source
                    @[simp]
                    theorem Valued.toNormedField.norm_lt_iff {L : Type u_1} [Field L] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : v.RankOne] {x x' : L} :
                    ‖x‖ < ‖x'‖ ↔ v x < v x'
                    source
                    @[simp]
                    theorem Valued.toNormedField.norm_le_one_iff {L : Type u_1} [Field L] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : v.RankOne] {x : L} :
                    ‖x‖ ≤ 1 ↔ v x ≤ 1
                    source
                    @[simp]
                    theorem Valued.toNormedField.norm_lt_one_iff {L : Type u_1} [Field L] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : v.RankOne] {x : L} :
                    ‖x‖ < 1 ↔ v x < 1
                    source
                    @[simp]
                    theorem Valued.toNormedField.one_le_norm_iff {L : Type u_1} [Field L] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : v.RankOne] {x : L} :
                    1 ≤ ‖x‖ ↔ 1 ≤ v x
                    source
                    @[simp]
                    theorem Valued.toNormedField.one_lt_norm_iff {L : Type u_1} [Field L] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : v.RankOne] {x : L} :
                    1 < ‖x‖ ↔ 1 < v x
                    source
                    theorem Valued.toNormedField.setOf_mem_integer_eq_closedBall {L : Type u_1} [Field L] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : v.RankOne] :
                    {x : L | x ∈ v.integer} = Metric.closedBall 0 1
                    source
                    def Valued.toNontriviallyNormedField {L : Type u_1} [Field L] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : v.RankOne] :
                    NontriviallyNormedField L

                    The nontrivially normed field structure determined by a rank one valuation.

                    Equations
                      Instances For