Documentation

TauCeti.Analysis.AbsoluteValue.Equivalence

Weak approximation for absolute values restricting to standard ones on ℚ #

Mathlib's AbsoluteValue.denseRange_algebraMap_pi approximates finitely many targets for a family of nontrivial, pairwise inequivalent absolute values. This file states it for a finite set of absolute values in which equivalent ones are equal, and supplies that hypothesis for absolute values on a field which agree on natural-number casts with the real or a q-adic absolute value on ℚ: two such that are equivalent are equal.

Main definitions #

Main results #

source
theorem TauCeti.exists_forall_apply_sub_lt {F : Type u_1} [Field F] (S : Finset (AbsoluteValue F ℝ)) (hS : ∀ v ∈ S, v.IsNontrivial) (hS' : ∀ v ∈ S, ∀ w ∈ S, v.IsEquiv w → v = w) (t : AbsoluteValue F ℝ → F) {ε : ℝ} (hε : 0 < ε) :
∃ (x : F), ∀ v ∈ S, v (x - t v) < ε

Weak approximation for a finite set of absolute values. For a finite set S of nontrivial absolute values on a field, any two of which are equal as soon as they are equivalent, every family of targets is approximated simultaneously by one element of the field.

source
theorem AbsoluteValue.IsEquiv.eq_of_apply_eq {F : Type u_1} [Field F] {v w : AbsoluteValue F ℝ} (h : v.IsEquiv w) {x : F} (hx : x ≠ 0) (hv : v x ≠ 1) (hvw : v x = w x) :
v = w

Two equivalent absolute values on a field are equal as soon as they agree at a nonzero element at which they do not take the value 1.

source
def Rat.AbsoluteValue.IsStandard (a : AbsoluteValue ℚ ℝ) :
Prop

The standard absolute values on ℚ: the real one and the q-adic ones.

Instances For
    source
    theorem Rat.AbsoluteValue.IsStandard.real :
    IsStandard AbsoluteValue.real

    The real absolute value on ℚ is standard.

    source
    theorem Rat.AbsoluteValue.IsStandard.padic (q : ℕ) [Fact (Nat.Prime q)] :
    IsStandard (AbsoluteValue.padic q)

    The q-adic absolute value on ℚ is standard.

    source
    theorem Rat.AbsoluteValue.IsStandard.eq_of_isEquiv {a b : AbsoluteValue ℚ ℝ} (ha : IsStandard a) (hb : IsStandard b) (h : a.IsEquiv b) :
    a = b

    Two equivalent standard absolute values on ℚ are equal.

    source
    theorem Rat.AbsoluteValue.IsStandard.isNontrivial {a : AbsoluteValue ℚ ℝ} (ha : IsStandard a) :
    a.IsNontrivial

    A standard absolute value on ℚ is nontrivial.

    source
    theorem AbsoluteValue.IsNontrivial.exists_nat_ne_one {a : AbsoluteValue ℚ ℝ} (ha : a.IsNontrivial) :
    ∃ (n : ℕ), n ≠ 0 ∧ a ↑n ≠ 1

    A nontrivial absolute value on ℚ takes a value other than 1 at a nonzero natural number.

    source
    theorem AbsoluteValue.IsEquiv.eq_of_isStandard {F : Type u_1} [Field F] {v w : AbsoluteValue F ℝ} (h : v.IsEquiv w) {a b : AbsoluteValue ℚ ℝ} (ha : Rat.AbsoluteValue.IsStandard a) (hb : Rat.AbsoluteValue.IsStandard b) (hva : ∀ (n : ℕ), v ↑n = a ↑n) (hwb : ∀ (n : ℕ), w ↑n = b ↑n) :
    v = w

    Equivalent absolute values agreeing on natural-number casts with standard absolute values on ℚ are equal.

    source
    theorem AbsoluteValue.isNontrivial_of_forall_natCast_eq {F : Type u_1} [Semiring F] {v : AbsoluteValue F ℝ} {a : AbsoluteValue ℚ ℝ} (ha : a.IsNontrivial) (hva : ∀ (n : ℕ), v ↑n = a ↑n) :
    v.IsNontrivial

    An absolute value agreeing on natural-number casts with a nontrivial absolute value on ℚ is nontrivial.