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.
• (TODO) 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. It is invariant under scaling by nonzero elements of K (for x ≠ 0).
• (TODO) 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