Nonarchimedean absolute values

Three facts about nonarchimedean real absolute values, the first two of which Mathlib has only for norms or for valuations. They are what is needed to describe the absolute values of a finite extension of number fields lying over a finite place without passing to a completion: such an absolute value is bounded on ℤ, hence nonarchimedean and bounded by 1 on the ring of integers, and it is a real power, with exponent the inverse of a local degree, of the absolute value of a finite place of the extension.

• AbsoluteValue.isNonarchimedean_iff_forall_natCast_le_one: an absolute value on a field is nonarchimedean if and only if it is bounded by 1 on the natural numbers. Mathlib has the forward implication for every nonarchimedean function, IsNonarchimedean.apply_natCast_le_one, and the reverse one for the norm of a normed division ring, IsUltrametricDist.isUltrametricDist_of_forall_norm_natCast_le_one; here the latter is transferred to absolute values through WithAbs. Consequently an absolute value lying over a nonarchimedean one is nonarchimedean, AbsoluteValue.isNonarchimedean_of_liesOver.
• IsNonarchimedean.apply_le_one_of_isIntegral: a nonarchimedean absolute value on an R-algebra which is bounded by 1 on the image of R is bounded by 1 on every element integral over R. Over ℤ the hypothesis on R is automatic, IsNonarchimedean.apply_le_one_of_isIntegral_int. This is the absolute-value analogue of Mathlib's Valuation.Integers.isIntegral_iff_v_le_one, and the proof follows the same size argument on the equation of integrality.
• AbsoluteValue.nonarchRpow: for t > 0, the function x ↦ v x ^ t is again an absolute value when v is nonarchimedean, equivalent to v, nonarchimedean, and lying over the corresponding power of the restriction of v. For an archimedean absolute value only t ≤ 1 works in general; the example at the end of the file checks that |·| ^ 2 on ℚ is not an absolute value.

References

• E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Chapter 1.

theorem AbsoluteValue.LiesOver.apply_algebraMap {K : Type u_1} {L : Type u_2} {S : Type u_3} [CommSemiring K] [Semiring L] [Algebra K L] [FaithfulSMul K L] [PartialOrder S] [Semiring S] {w : AbsoluteValue L S} (v : AbsoluteValue K S) [w.LiesOver v] (x : K) : w ((algebraMap K L) x) = v x

An absolute value lying over v agrees with v on the base.

theorem AbsoluteValue.isNonarchimedean_of_forall_natCast_le_one {F : Type u_1} [Field F] {v : AbsoluteValue F ℝ} (h : ∀ (n : ℕ), v ↑n ≤ 1) : IsNonarchimedean ⇑v

An absolute value on a field which is bounded by 1 on the natural numbers is nonarchimedean.

theorem AbsoluteValue.isNonarchimedean_iff_forall_natCast_le_one {F : Type u_1} [Field F] {v : AbsoluteValue F ℝ} : IsNonarchimedean ⇑v ↔ ∀ (n : ℕ), v ↑n ≤ 1

An absolute value on a field is nonarchimedean if and only if it is bounded by 1 on the natural numbers.

theorem AbsoluteValue.isNonarchimedean_of_liesOver {F : Type u_1} [Field F] {v : AbsoluteValue F ℝ} {K : Type u_2} [CommSemiring K] [Algebra K F] [FaithfulSMul K F] {u : AbsoluteValue K ℝ} [v.LiesOver u] (hu : IsNonarchimedean ⇑u) : IsNonarchimedean ⇑v

An absolute value on a field lying over a nonarchimedean absolute value is nonarchimedean: it agrees with the latter on the natural numbers, where both are therefore bounded by 1.

theorem IsNonarchimedean.apply_le_one_of_isIntegral {R : Type u_1} {F : Type u_2} [CommRing R] [Ring F] [Algebra R F] {v : AbsoluteValue F ℝ} (hv : IsNonarchimedean ⇑v) (h : ∀ (r : R), v ((algebraMap R F) r) ≤ 1) {x : F} (hx : IsIntegral R x) : v x ≤ 1

A nonarchimedean absolute value on an R-algebra which is bounded by 1 on the image of R is bounded by 1 on every element integral over R.

This is the absolute-value analogue of the forward implication of Mathlib's Valuation.Integers.isIntegral_iff_v_le_one, and the proof follows it.

theorem IsNonarchimedean.apply_le_one_of_isIntegral_int {F : Type u_2} [Ring F] {v : AbsoluteValue F ℝ} (hv : IsNonarchimedean ⇑v) {x : F} (hx : IsIntegral ℤ x) : v x ≤ 1

A nonarchimedean absolute value is bounded by 1 on every element integral over ℤ.

noncomputable def AbsoluteValue.nonarchRpow {R : Type u_1} [Semiring R] (v : AbsoluteValue R ℝ) (hv : IsNonarchimedean ⇑v) {t : ℝ} (ht : 0 < t) : AbsoluteValue R ℝ

The t-th power x ↦ v x ^ t of a nonarchimedean absolute value v, for t > 0, as an absolute value. The strong triangle inequality is what makes it subadditive; for an archimedean v and t > 1 it is in general not an absolute value.

@[simp]

theorem AbsoluteValue.nonarchRpow_apply {R : Type u_1} [Semiring R] (v : AbsoluteValue R ℝ) (hv : IsNonarchimedean ⇑v) {t : ℝ} (ht : 0 < t) (x : R) : (v.nonarchRpow hv ht) x = v x ^ t

theorem AbsoluteValue.isNonarchimedean_nonarchRpow {R : Type u_1} [Semiring R] (v : AbsoluteValue R ℝ) (hv : IsNonarchimedean ⇑v) {t : ℝ} (ht : 0 < t) : IsNonarchimedean ⇑(v.nonarchRpow hv ht)

A real power of a nonarchimedean absolute value is nonarchimedean.

theorem AbsoluteValue.isEquiv_nonarchRpow {R : Type u_1} [Semiring R] (v : AbsoluteValue R ℝ) (hv : IsNonarchimedean ⇑v) {t : ℝ} (ht : 0 < t) : v.IsEquiv (v.nonarchRpow hv ht)

A nonarchimedean absolute value is equivalent to each of its positive real powers.

@[simp]

theorem AbsoluteValue.nonarchRpow_one {R : Type u_1} [Semiring R] (v : AbsoluteValue R ℝ) (hv : IsNonarchimedean ⇑v) : v.nonarchRpow hv ⋯ = v

@[simp]

theorem AbsoluteValue.nonarchRpow_nonarchRpow {R : Type u_1} [Semiring R] (v : AbsoluteValue R ℝ) (hv : IsNonarchimedean ⇑v) {t : ℝ} (ht : 0 < t) {s : ℝ} (hs : 0 < s) (hv' : IsNonarchimedean ⇑(v.nonarchRpow hv hs)) : (v.nonarchRpow hv hs).nonarchRpow hv' ht = v.nonarchRpow hv ⋯

theorem AbsoluteValue.liesOver_nonarchRpow {t : ℝ} (ht : 0 < t) {K : Type u_2} {L : Type u_3} [CommSemiring K] [Semiring L] [Algebra K L] [FaithfulSMul K L] {w : AbsoluteValue L ℝ} {u : AbsoluteValue K ℝ} [w.LiesOver u] (hw : IsNonarchimedean ⇑w) (hu : IsNonarchimedean ⇑u) : (w.nonarchRpow hw ht).LiesOver (u.nonarchRpow hu ht)

Real powers of nonarchimedean absolute values preserve lying over: if w lies over u, then w ^ t lies over u ^ t.