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).

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.

Equations

• Height.totalWeight K = Height.AdmissibleAbsValues.archAbsVal.card

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.

Equations

• Height.mulHeight₁ x = (Multiset.map (fun (v : AbsoluteValue K ℝ) => max (v x) 1) Height.AdmissibleAbsValues.archAbsVal).prod * ∏ᶠ (v : ↑Height.AdmissibleAbsValues.nonarchAbsVal), max (↑v x) 1

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.zero_le_mulHeight₁ {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.

Equations

• Height.logHeight₁ x = Real.log (Height.mulHeight₁ x)

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

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.

Equations

• One or more equations did not get rendered due to their size.

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.mulHeight_one {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} : mulHeight 1 = 1

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.

Equations

• Height.logHeight x = Real.log (Height.mulHeight x)

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)

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.

Equations

• x.mulHeight = Height.mulHeight fun (i : ↥x.support) => x ↑i

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.

Equations

• x.logHeight = Real.log (Height.mulHeight ⇑x)

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)

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.zero_le_logHeight {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] {x : ι → K} : 0 ≤ logHeight x

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.