Basic theory of heights

This is an attempt at formalizing some basic properties of height functions.

We aim at a level of generality that allows to apply the theory to algebraic number fields and to function fields (and possibly beyond).

The general set-up for heights is the following. Let K be a field.

• We have a Multiset of archimedean absolute values on K (with values in ℝ).
• We also have a Set of non-archimedean (i.e., |x+y| ≤ max |x| |y|) absolute values.
• For a given x ≠ 0 in K, |x|ᵥ = 1 for all but finitely many (non-archimedean) v.
• We have the product formula ∏ v : arch, |x|ᵥ * ∏ v : nonarch, |x|ᵥ = 1 for all x ≠ 0 in K, where the first product is over the multiset of archimedean absolute values.

We realize this implementation via the class Height.AdmissibleAbsValues K.

Main definitions

We define multiplicative heights and logarithmic heights (which are just defined to be the (real) logarithm of the corresponding multiplicative height). This leads to some duplication (in the definitions and statements; the proofs are reduced to those for the multiplicative height), which is justified, as both versions are frequently used.

We define the following variants.

• Height.mulHeight₁ x and Height.logHeight₁ x for x : K. This is the height of an element of K.
• Height.mulHeight x and Height.logHeight x for x : ι → K with ι finite. This is the height of a tuple of elements of K representing a point in projective space. When x = 0, we define the multiplicative height to be 1 (so the loarithmic height is 0). It is invariant under scaling by nonzero elements of K.
• Finsupp.mulHeight x and Finsupp.logHeight x for x : α →₀ K. This is the same as the height of x restricted to the support of x.
• (TODO) Projectivization.mulHeight and Projectivization.logHeight on Projectivization K (ι → K) (with a Fintype ι). This is the height of a point on projective space (with fixed basis).

TODO

• Add Height.AdmissibleAbsValues instances for

  • Fields of rational functions in n variables and
  • Finite extensions of fields with Height.AdmissibleAbsValues.

• Prove upper and lower bounds on the height of the image of a tuple under a tuple of homogeneous polynomial maps of the same degree.

Tags

Height, absolute value

Families of admissible absolute values

We define the class AdmissibleAbsValues K for a field K, which captures the notion of a family of absolute values on K satisfying a product formula.

class Height.AdmissibleAbsValues (K : Type u_1) [Field K] : Type u_1

A type class capturing an admissible family of absolute values.

• archAbsVal : Multiset (AbsoluteValue K ℝ)

  The archimedean absolute values as a multiset of ℝ-valued absolute values on K.

• nonarchAbsVal : Set (AbsoluteValue K ℝ)

  The nonarchimedean absolute values as a set of ℝ-valued absolute values on K.

• isNonarchimedean (v : AbsoluteValue K ℝ) : v ∈ nonarchAbsVal → IsNonarchimedean ⇑v

  The nonarchimedean absolute values are indeed nonarchimedean.

• mulSupport_finite {x : K} : x ≠ 0 → (Function.mulSupport fun (v : ↑nonarchAbsVal) => ↑v x).Finite

  Only finitely many (nonarchimedean) absolute values are ≠ 1 for any nonzero x : K.

• product_formula {x : K} : x ≠ 0 → (Multiset.map (fun (x_1 : AbsoluteValue K ℝ) => x_1 x) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ↑v x = 1

  The product formula. The archimedean absolute values are taken with their multiplicity.

def Height.totalWeight (K : Type u_1) [Field K] [AdmissibleAbsValues K] : ℕ

The totalWeight of a field with AdmissibleAbsValues is the sum of the multiplicities of the archimedean places.

Heights of field elements

We use the subscipt ₁ to denote multiplicative and logarithmic heights of field elements (this is because we are in the one-dimensional case of (affine) heights).

def Height.mulHeight₁ {K : Type u_1} [Field K] [AdmissibleAbsValues K] (x : K) : ℝ

The multiplicative height of an element of K.

theorem Height.mulHeight₁_eq {K : Type u_1} [Field K] [AdmissibleAbsValues K] (x : K) : mulHeight₁ x = (Multiset.map (fun (v : AbsoluteValue K ℝ) => max (v x) 1) AdmissibleAbsValues.archAbsVal).prod * ∏ᶠ (v : ↑AdmissibleAbsValues.nonarchAbsVal), max (↑v x) 1

@[simp]

theorem Height.mulHeight₁_zero {K : Type u_1} [Field K] [AdmissibleAbsValues K] : mulHeight₁ 0 = 1

@[simp]

theorem Height.mulHeight₁_one {K : Type u_1} [Field K] [AdmissibleAbsValues K] : mulHeight₁ 1 = 1

theorem Height.one_le_mulHeight₁ {K : Type u_1} [Field K] [AdmissibleAbsValues K] (x : K) : 1 ≤ mulHeight₁ x

The mutliplicative height of a field element is always at least 1.

theorem Height.mulHeight₁_pos {K : Type u_1} [Field K] [AdmissibleAbsValues K] (x : K) : 0 < mulHeight₁ x

theorem Height.mulHeight₁_ne_zero {K : Type u_1} [Field K] [AdmissibleAbsValues K] (x : K) : mulHeight₁ x ≠ 0

theorem Height.mulHeight₁_nonneg {K : Type u_1} [Field K] [AdmissibleAbsValues K] (x : K) : 0 ≤ mulHeight₁ x

def Height.logHeight₁ {K : Type u_1} [Field K] [AdmissibleAbsValues K] (x : K) : ℝ

The logarithmic height of an element of K.

theorem Height.logHeight₁_eq_log_mulHeight₁ {K : Type u_1} [Field K] [AdmissibleAbsValues K] (x : K) : logHeight₁ x = Real.log (mulHeight₁ x)

@[simp]

theorem Height.logHeight₁_zero {K : Type u_1} [Field K] [AdmissibleAbsValues K] : logHeight₁ 0 = 0

@[simp]

theorem Height.logHeight₁_one {K : Type u_1} [Field K] [AdmissibleAbsValues K] : logHeight₁ 1 = 0

theorem Height.zero_le_logHeight₁ {K : Type u_1} [Field K] [AdmissibleAbsValues K] (x : K) : 0 ≤ logHeight₁ x

Positivity extension for mulHeight₁, logHeight₁

def Mathlib.Meta.Positivity.evalMulHeight₁ : PositivityExt

Extension for the positivity tactic: Height.mulHeight₁ is always positive.

def Mathlib.Meta.Positivity.evalLogHeight₁ : PositivityExt

Extension for the positivity tactic: Height.logHeight₁ is always nonnegative.

Heights of tuples and finitely supported maps

We define the multiplicative height of a nonzero tuple x : ι → K as the product of the maxima of v on x, as v runs through the relevant absolute values of K. As usual, the logarithmic height is the logarithm of the multiplicative height. When x = 0, we define the multiplicative height to be 1; this is a convenient "junk value", which allows to avoid the condition x ≠ 0 in most of the results.

For a finitely supported function x : ι →₀ K, we define the height as the height of x restricted to its support.

def Height.mulHeight {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} (x : ι → K) : ℝ

The multiplicative height of a tuple of elements of K. For the zero tuple we take the junk value 1.

theorem Height.mulHeight_eq {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} {x : ι → K} (hx : x ≠ 0) : mulHeight x = (Multiset.map (fun (v : AbsoluteValue K ℝ) => ⨆ (i : ι), v (x i)) AdmissibleAbsValues.archAbsVal).prod * ∏ᶠ (v : ↑AdmissibleAbsValues.nonarchAbsVal), ⨆ (i : ι), ↑v (x i)

@[simp]

theorem Height.mulHeight_zero {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} : mulHeight 0 = 1

@[simp]

theorem Height.fun_mulHeight_zero {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} : (mulHeight fun (x : ι) => 0) = 1

Eta-expanded form of Height.mulHeight_zero

@[simp]

theorem Height.mulHeight_one {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} : mulHeight 1 = 1

@[simp]

theorem Height.fun_mulHeight_one {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} : (mulHeight fun (x : ι) => 1) = 1

Eta-expanded form of Height.mulHeight_one

theorem Height.mulHeight_comp_equiv {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} {ι' : Type u_3} (e : ι ≃ ι') (x : ι' → K) : mulHeight (x ∘ ⇑e) = mulHeight x

The multiplicative height does not change under re-indexing.

theorem Height.mulHeight_swap {K : Type u_1} [Field K] [AdmissibleAbsValues K] (x y : K) : mulHeight ![x, y] = mulHeight ![y, x]

def Height.logHeight {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} (x : ι → K) : ℝ

The logarithmic height of a tuple of elements of K.

theorem Height.logHeight_eq_log_mulHeight {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} (x : ι → K) : logHeight x = Real.log (mulHeight x)

@[simp]

theorem Height.logHeight_zero {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_3} : logHeight 0 = 0

@[simp]

theorem Height.fun_logHeight_zero {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_3} : (logHeight fun (x : ι) => 0) = 0

Eta-expanded form of Height.logHeight_zero

@[simp]

theorem Height.logHeight_one {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_3} : logHeight 1 = 0

@[simp]

theorem Height.fun_logHeight_one {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_3} : (logHeight fun (x : ι) => 1) = 0

Eta-expanded form of Height.logHeight_one

def Finsupp.mulHeight {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] {α : Type u_3} (x : α →₀ K) : ℝ

The multiplicative height of a finitely supported function.

def Finsupp.logHeight {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] {α : Type u_3} (x : α →₀ K) : ℝ

The logarithmic height of a finitely supported function.

theorem Finsupp.logHeight_eq_log_mulHeight {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] {α : Type u_3} (x : α →₀ K) : Height.logHeight ⇑x = Real.log (Height.mulHeight ⇑x)

First properties of heights

theorem Height.mulHeight_smul_eq_mulHeight {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x : ι → K) {c : K} (hc : c ≠ 0) : mulHeight (c • x) = mulHeight x

The multiplicative height of a tuple does not change under scaling.

theorem Height.one_le_mulHeight {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x : ι → K) : 1 ≤ mulHeight x

theorem Height.mulHeight_pos {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x : ι → K) : 0 < mulHeight x

theorem Height.mulHeight_ne_zero {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x : ι → K) : mulHeight x ≠ 0

theorem Height.logHeight_nonneg {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x : ι → K) : 0 ≤ logHeight x

Positivity extension for mulHeight, logHeight

def Mathlib.Meta.Positivity.evalMulHeight : PositivityExt

Extension for the positivity tactic: Height.mulHeight is always positive.

def Mathlib.Meta.Positivity.evalLogHeight : PositivityExt

Extension for the positivity tactic: Height.logHeight is always nonnegative.

Further properties of heights

theorem Height.logHeight_smul_eq_logHeight {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x : ι → K) {c : K} (hc : c ≠ 0) : logHeight (c • x) = logHeight x

The logarithmic height of a tuple does not change under scaling.

theorem Height.mulHeight₁_eq_mulHeight {K : Type u_1} [Field K] [AdmissibleAbsValues K] (x : K) : mulHeight₁ x = mulHeight ![x, 1]

theorem Height.logHeight₁_eq_logHeight {K : Type u_1} [Field K] [AdmissibleAbsValues K] (x : K) : logHeight₁ x = logHeight ![x, 1]

theorem Height.mulHeight₁_div_eq_mulHeight {K : Type u_1} [Field K] [AdmissibleAbsValues K] (x y : K) : mulHeight₁ (x / y) = mulHeight ![x, y]

theorem Height.logHeight₁_div_eq_logHeight {K : Type u_1} [Field K] [AdmissibleAbsValues K] (x y : K) : logHeight₁ (x / y) = logHeight ![x, y]

theorem Height.mulHeight_pow {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x : ι → K) (n : ℕ) : mulHeight (x ^ n) = mulHeight x ^ n

The multiplicative height of the coordinate-wise nth power of a tuple is the nth power of its multiplicative height.

theorem Height.logHeight_pow {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x : ι → K) (n : ℕ) : logHeight (x ^ n) = ↑n * logHeight x

The logarithmic height of the coordinate-wise nth power of a tuple is n times its logarithmic height.

theorem Height.mulHeight₁_inv {K : Type u_1} [Field K] [AdmissibleAbsValues K] (x : K) : mulHeight₁ x⁻¹ = mulHeight₁ x

The multiplicative height of the inverse of a field element x is the same as the multiplicative height of x.

theorem Height.logHeight₁_inv {K : Type u_1} [Field K] [AdmissibleAbsValues K] (x : K) : logHeight₁ x⁻¹ = logHeight₁ x

The logarithmic height of the inverse of a field element x is the same as the logarithmic height of x.

theorem Height.mulHeight₁_pow {K : Type u_1} [Field K] [AdmissibleAbsValues K] (x : K) (n : ℕ) : mulHeight₁ (x ^ n) = mulHeight₁ x ^ n

The multiplicative height of the nth power of a field element x (with n : ℕ) is the nth power of the multiplicative height of x.

theorem Height.logHeight₁_pow {K : Type u_1} [Field K] [AdmissibleAbsValues K] (x : K) (n : ℕ) : logHeight₁ (x ^ n) = ↑n * logHeight₁ x

The logarithmic height of the nth power of a field element x (with n : ℕ) is n times the logaritmic height of x.

theorem Height.mulHeight₁_zpow {K : Type u_1} [Field K] [AdmissibleAbsValues K] (x : K) (n : ℤ) : mulHeight₁ (x ^ n) = mulHeight₁ x ^ n.natAbs

The multiplicative height of the nth power of a field element x (with n : ℤ) is the |n|th power of the multiplicative height of x.

theorem Height.logHeight₁_zpow {K : Type u_1} [Field K] [AdmissibleAbsValues K] (x : K) (n : ℤ) : logHeight₁ (x ^ n) = ↑n.natAbs * logHeight₁ x

The logarithmic height of the nth power of a field element x (with n : ℤ) is |n| times the logarithmic height of x.

Bounds for the height of sums of field elements

We prove the general case (finite sums of arbitrary length) first and deduce the result for sums of two elements from it.

theorem Finset.max_abv_sum_one_le {R : Type u_1} {S : Type u_2} [Semiring R] [CommSemiring S] [LinearOrder S] [IsOrderedRing S] [CharZero S] (v : AbsoluteValue R S) {ι : Type u_3} {s : Finset ι} (hs : s.Nonempty) (x : ι → R) : max (v (∑ i ∈ s, x i)) 1 ≤ ↑s.card * ∏ i ∈ s, max (v (x i)) 1

The "local" version of the height bound for arbitrary sums for general (possibly archimedean) absolute values.

theorem Finset.max_abv_sum_one_le_of_isNonarchimedean {R : Type u_1} {S : Type u_2} [Semiring R] [CommSemiring S] [LinearOrder S] [IsOrderedRing S] {v : AbsoluteValue R S} (hv : IsNonarchimedean ⇑v) {ι : Type u_3} (s : Finset ι) (x : ι → R) : max (v (∑ i ∈ s, x i)) 1 ≤ ∏ i ∈ s, max (v (x i)) 1

The "local" version of the height bound for arbitrary sums for nonarchimedean absolute values.

theorem Height.mulHeight₁_sum_le {K : Type u_1} [Field K] [AdmissibleAbsValues K] {α : Type u_2} {s : Finset α} (hs : s.Nonempty) (x : α → K) : mulHeight₁ (∑ a ∈ s, x a) ≤ ↑s.card ^ totalWeight K * ∏ a ∈ s, mulHeight₁ (x a)

The multiplicative height of a nonempty finite sum of field elements is at most n ^ (totalWeight K) times the product of the individual multiplicative heights, where n is the number of terms.

theorem Height.logHeight₁_sum_le {K : Type u_1} [Field K] [AdmissibleAbsValues K] {α : Type u_2} (s : Finset α) (x : α → K) : logHeight₁ (∑ a ∈ s, x a) ≤ ↑(totalWeight K) * Real.log ↑s.card + ∑ a ∈ s, logHeight₁ (x a)

The logarithmic height of a finite sum of field elements is at most totalWeight K * log n plus the sum of the individual logarithmic heights, where n is the number of terms.

(Note that here we do not need to assume that s is nonempty, due to the convenient junk value log 0 = 0.)

@[simp]

theorem Height.mulHeight₁_neg {K : Type u_1} [Field K] [AdmissibleAbsValues K] (x : K) : mulHeight₁ (-x) = mulHeight₁ x

The multiplicative height of -x is the same as that of x.

@[simp]

theorem Height.logHeight₁_neg {K : Type u_1} [Field K] [AdmissibleAbsValues K] (x : K) : logHeight₁ (-x) = logHeight₁ x

The logarithmic height of -x is the same as that of x.

theorem Height.mulHeight₁_add_le {K : Type u_1} [Field K] [AdmissibleAbsValues K] (x y : K) : mulHeight₁ (x + y) ≤ 2 ^ totalWeight K * mulHeight₁ x * mulHeight₁ y

The multiplicative height of x + y is at most 2 ^ totalWeight K times the product of the multiplicative heights of x and y.

theorem Height.logHeight₁_add_le {K : Type u_1} [Field K] [AdmissibleAbsValues K] (x y : K) : logHeight₁ (x + y) ≤ ↑(totalWeight K) * Real.log 2 + logHeight₁ x + logHeight₁ y

The logarithmic height of x + y is at most totalWeight K * log 2 plus the sum of the logarithmic heights of x and y.

theorem Height.mulHeight₁_sub_le {K : Type u_1} [Field K] [AdmissibleAbsValues K] (x y : K) : mulHeight₁ (x - y) ≤ 2 ^ totalWeight K * mulHeight₁ x * mulHeight₁ y

The multiplicative height of x - y is at most 2 ^ totalWeight K times the product of the multiplicative heights of x and y.

theorem Height.logHeight₁_sub_le {K : Type u_1} [Field K] [AdmissibleAbsValues K] (x y : K) : logHeight₁ (x - y) ≤ ↑(totalWeight K) * Real.log 2 + logHeight₁ x + logHeight₁ y

The logarithmic height of x - y is at most totalWeight K * log 2 plus the sum of the logarithmic heights of x and y.