Absolute values on fields

TheoremAbsolute values in positive characteristic are nonarchimedean#✓fully proved

Let \(K\) be a field of characteristic \(p > 0\). Then every real-valued absolute value \(v\) on \(K\) is nonarchimedean: \(v(x + y) \le \max(v(x), v(y))\) for all \(x, y \in K\).

public theorem isNonarchimedean_of_charP {p : ℕ} [CharP K p] [NeZero p]
    (v : AbsoluteValue K ℝ) : IsNonarchimedean v

TheoremAbsolute values on finite fields are trivial#✓fully proved

Let \(K\) be a finite field and \(v\) a real-valued absolute value on \(K\). Then \(v(x) = 1\) for every nonzero \(x \in K\).

public theorem eq_one_of_ne_zero_of_finite [Finite K] (v : AbsoluteValue K ℝ)
    {x : K} (hx : x ≠ 0) : v x = 1

DefinitionTopology induced by an absolute value#✓fully proved

Let \(K\) be a field and \(v\) a real-valued absolute value on \(K\). The topology induced by \(v\) on \(K\) is the topology pulled back along the identity map from \(K\) to \(K\) equipped with the norm \(v\); equivalently, it is the metric topology of the distance \(d(x, y) = v(x - y)\) on \(K\).

@[reducible]
public noncomputable def inducedTopology (v : AbsoluteValue K ℝ) : TopologicalSpace K :=
  letI : NormedRing (WithAbs v) := WithAbs.normedRing v
  TopologicalSpace.induced (WithAbs.toAbs v) inferInstance
Used by 1
Used byAbsolute values inducing the same topology are equivalent

TheoremAbsolute values inducing the same topology are equivalent#✓fully proved

Let \(K\) be a field and \(v\), \(w\) real-valued absolute values on \(K\). The topologies induced on \(K\) by \(v\) and by \(w\) are equal if and only if \(v\) and \(w\) are equivalent.

This is about equality of the induced topologies on \(K\), not about equality of the absolute values themselves: inequivalent absolute values may still agree on many elements while inducing different topologies.

public theorem inducedTopology_eq_iff_isEquiv (v w : AbsoluteValue K ℝ) :
    v.inducedTopology = w.inducedTopology ↔ v.IsEquiv w
Uses 1
Statement usesTopology induced by an absolute value

TheoremNonarchimedean criterion for absolute values#✓fully proved

Let \(K\) be a field and \(v\) a real-valued absolute value on \(K\). Then \(v\) is nonarchimedean, that is, \(v(x + y) \le \max(v(x), v(y))\) for all \(x, y \in K\), if and only if \(v(n) \le 1\) for every natural number \(n\), viewed as the element \(n \cdot 1\) of \(K\).

public theorem isNonarchimedean_iff_natCast_le_one (v : AbsoluteValue K ℝ) :
    IsNonarchimedean v ↔ ∀ n : ℕ, v (n : K) ≤ 1
Sources
  • ATLAS NumberTheoryI, Section 1.2, Lemma 1.4.
Used by 2
Used byNonarchimedean criterion using positive integers · Absolute values bounded by one on the natural numbers are nonarchimedean

TheoremAbsolute values bounded by one on the natural numbers are nonarchimedean#✓fully proved

Let \(K\) be a field and \(v\) a real-valued absolute value on \(K\). If \(v(n) \le 1\) for every natural number \(n\), viewed as the element \(n \cdot 1\) of \(K\), then \(v\) is nonarchimedean: \(v(x + y) \le \max(v(x), v(y))\) for all \(x, y \in K\).

public theorem isNonarchimedean_of_natCast_le_one (v : AbsoluteValue K ℝ)
    (hv : ∀ n : ℕ, v (n : K) ≤ 1) : IsNonarchimedean v
Sources
  • ATLAS NumberTheoryI, Section 1.2, backward direction of Lemma 1.4.
Uses 1
Proof usesNonarchimedean criterion for absolute values

TheoremNonarchimedean criterion using positive integers#✓fully proved

Let \(K\) be a field and \(v\) a real-valued absolute value on \(K\). Then \(v\) is nonarchimedean, that is, \(v(x + y) \le \max(v(x), v(y))\) for all \(x, y \in K\), if and only if \(v(n) \le 1\) for every positive integer \(n\), viewed as the element \(n \cdot 1\) of \(K\).

The case \(n = 0\) may be omitted because \(v(0) = 0 \le 1\).

public theorem isNonarchimedean_iff_natCast_le_one_of_pos
    (v : AbsoluteValue K ℝ) :
    IsNonarchimedean v ↔ ∀ n : ℕ, 0 < n → v (n : K) ≤ 1
Sources
  • ATLAS NumberTheoryI, Section 1.2, Lemma 1.4 (in the book's form).
Uses 1
Proof usesNonarchimedean criterion for absolute values

DefinitionPowers of an absolute value#✓fully proved

Let \(R\) be a semiring, \(v\) a real-valued absolute value on \(R\) and \(c\) a real number with \(0 < c \le 1\). The \(c\)-th power of \(v\) is the real-valued absolute value \(x \mapsto v(x)^c\) on \(R\).

AbsoluteValue.rpow · 16 lines 
noncomputable def rpow (v : AbsoluteValue R ℝ) (c : ℝ) (hc₀ : 0 < c) (hc₁ : c ≤ 1) :
    AbsoluteValue R ℝ where
  toFun x := (v x) ^ c
  map_mul' x y := by
    rw [AbsoluteValue.map_mul v x y,
      Real.mul_rpow (AbsoluteValue.nonneg v x) (AbsoluteValue.nonneg v y)]
  nonneg' x := Real.rpow_nonneg (AbsoluteValue.nonneg v x) c
  eq_zero' x := by
    rw [Real.rpow_eq_zero (AbsoluteValue.nonneg v x) hc₀.ne', AbsoluteValue.eq_zero v]
  add_le' x y := by
    calc
      v (x + y) ^ c ≤ (v x + v y) ^ c :=
        Real.rpow_le_rpow (AbsoluteValue.nonneg v (x + y)) (AbsoluteValue.add_le v x y) hc₀.le
      _ ≤ v x ^ c + v y ^ c :=
        Real.rpow_add_le_add_rpow (AbsoluteValue.nonneg v x) (AbsoluteValue.nonneg v y)
          hc₀.le hc₁
Used by 5
Used byDegree-normalized absolute value at a finite place · Degree-normalized absolute value at an infinite place · Value of the degree-normalized absolute value at a finite place · Value of the degree-normalized absolute value at an infinite place · Values of a power of an absolute value

TheoremValues of a power of an absolute value#✓fully proved

Let \(R\) be a semiring, \(v\) a real-valued absolute value on \(R\) and \(c\) a real number with \(0 < c \le 1\). The \(c\)-th power of \(v\) takes the value \(v(x)^c\) at every \(x \in R\).

@[simp]
theorem rpow_apply (v : AbsoluteValue R ℝ) (c : ℝ) (hc₀ : 0 < c) (hc₁ : c ≤ 1) (x : R) :
    v.rpow c hc₀ hc₁ x = v x ^ c
Uses 1 · Used by 2
Statement usesPowers of an absolute value
Used byValue of the degree-normalized absolute value at a finite place · Value of the degree-normalized absolute value at an infinite place
9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.