The affine height of a tuple

Mathlib's Height.mulHeight is a height on projective space: it is invariant under scaling (Height.mulHeight_smul_eq_mulHeight), so it is a function of the line through a tuple rather than of the tuple. Quantities that are not homogeneous in the tuple, such as the value ∑ i, a i * x i of a linear form or the determinant of a matrix, scale with their arguments, so no bound on their height can be stated in terms of the projective heights of the arguments, which are scale-invariant. This file defines the affine height of a tuple x : ι → K, the projective height of the tuple with a coordinate 1 appended:

Height.mulHeightAff x = Height.mulHeight fun o : Option ι ↦ o.elim 1 x,

and its logarithm Height.logHeightAff. For a finite index type ι, the local factor at each place is max (⨆ i, v (x i)) 1 (Height.mulHeightAff_eq), so the affine height is the tuple analogue of Height.mulHeight₁ and agrees with it on a one-element tuple (Height.mulHeightAff_unique, Height.mulHeightAff_fin_one).

The affine height is deliberately not invariant under scaling (Height.exists_mulHeightAff_smul_ne). What it gains is domination: for finite index types, it bounds the projective height of the tuple and the height of every coordinate, and it can only drop under re-indexing. In the other direction, it is bounded above by the product of the scalar heights of the coordinates.

Main definitions

• Height.mulHeightAff: the multiplicative affine height of a tuple.
• Height.logHeightAff: its logarithm.

Main results

• Height.mulHeightAff_eq: for finite ι, the affine height as a product of the local factors max (⨆ i, v (x i)) 1; Height.prod_mulHeightAff_eq splits a finite product of affine heights into the products of these local factors place by place.
• Height.iSup_option_elim_eq_max, Height.iSup_option_elim_smul_le: the local factor max (⨆ i, v (x i)) 1 for any nonnegative multiplicative v, and its bound for a scalar multiple; Height.mul_log_iSup_option_elim_smul_le turns a logarithmic bound for v c and the local sup norm of x into one for the local factor of c • x.
• Height.hasFiniteMulSupport_max_iSup_nonarchAbsVal: the nonarchimedean local factors are 1 at all but finitely many places.
• Height.mulHeight_le_mulHeightAff, Height.mulHeight₁_le_mulHeightAff: for finite ι, the affine height dominates the projective height of the tuple and the height of each coordinate. The second fails for Height.mulHeight.
• Height.mulHeightAff_le_prod_mulHeight₁: for finite ι, the affine height is at most ∏ i, mulHeight₁ (x i); Height.logHeightAff_le_sum_logHeight₁ is its logarithmic form.
• Height.mulHeightAff_comp_le, Height.mulHeightAff_comp_equiv: monotonicity under re-indexing between finite index types, and equality for a bijection between arbitrary ones.
• Height.mulHeight_cons_one: for x : Fin n → K, prepending the coordinate 1 with Fin.cons instead of appending it gives the same height.
• Height.mulHeightAff_zero, Height.mulHeightAff_one: the zero tuple and the tuple of ones have affine height 1.
• Height.mulHeightAff_unique, Height.mulHeightAff_fin_one: on a one-element tuple the affine height is Height.mulHeight₁.
• Height.exists_mulHeightAff_smul_ne: the affine height is not invariant under scaling.

Implementation notes

The appended coordinate is indexed by none : Option ι. The type Option ι is finite when ι is, and re-indexing along f : ι → ι' becomes re-indexing along Option.map f.

The finiteness of the multiplicative support of the nonarchimedean local factors rests on Height.hasFiniteMulSupport_iSup_nonarchAbsVal, which is private in Mathlib/NumberTheory/Height/Basic.lean; it is reached by import all, as Mathlib's own Mathlib/NumberTheory/Height/MvPolynomial.lean does.

References

• E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press, 2006, §1.5.
• The statements and proofs follow ArithmeticHeights/Affine.lean of rwst/Subspace-Theorems (commit e443c24, Apache 2.0), restated against Mathlib's height API.

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

The affine height of a tuple x : ι → K: the projective height Height.mulHeight of the tuple with a coordinate 1 appended.

Unlike Height.mulHeight it is not invariant under scaling (Height.exists_mulHeightAff_smul_ne); for finite ι it dominates the projective height (Height.mulHeight_le_mulHeightAff) and the height of every coordinate (Height.mulHeight₁_le_mulHeightAff).

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

The affine logarithmic height of a tuple, the logarithm of Height.mulHeightAff.

theorem Height.mulHeightAff_def {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} (x : ι → K) : mulHeightAff x = mulHeight fun (o : Option ι) => o.elim 1 x

The defining formula of Height.mulHeightAff, to unfold it into Height.mulHeight.

theorem Height.logHeightAff_eq_log_mulHeightAff {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} (x : ι → K) : logHeightAff x = Real.log (mulHeightAff x)

The defining formula of Height.logHeightAff as the logarithm of Height.mulHeightAff.

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

The affine height does not change under a bijective re-indexing.

@[simp]

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

The tuple of ones has affine height 1: appending a coordinate 1 gives the tuple of ones on Option ι.

@[simp]

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

The tuple of ones has affine logarithmic height 0.

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

The logarithmic form of Height.mulHeightAff_comp_equiv.

@[simp]

theorem Height.mulHeight_cons_one {K : Type u_1} [Field K] [AdmissibleAbsValues K] {n : ℕ} (x : Fin n → K) : mulHeight (Fin.cons 1 x) = mulHeightAff x

The affine height may equally be computed by prepending the coordinate 1 to a tuple indexed by Fin n: the projective height of Fin.cons 1 x is Height.mulHeightAff x.

@[simp]

theorem Height.logHeight_cons_one {K : Type u_1} [Field K] [AdmissibleAbsValues K] {n : ℕ} (x : Fin n → K) : logHeight (Fin.cons 1 x) = logHeightAff x

The logarithmic form of Height.mulHeight_cons_one.

@[simp]

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

The zero tuple has affine height 1, with no finiteness assumption on its index type.

@[simp]

theorem Height.logHeightAff_zero {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} : logHeightAff 0 = 0

The zero tuple has affine logarithmic height 0.

theorem Height.iSup_apply_pos {K : Type u_1} [Field K] {ι : Type u_2} [Finite ι] {F : Type u_4} [FunLike F K ℝ] [MonoidWithZeroHomClass F K ℝ] [NonnegHomClass F K ℝ] (v : F) {x : ι → K} (hx : x ≠ 0) : 0 < ⨆ (i : ι), v (x i)

The local sup norm ⨆ i, v (x i) of a nonzero finite tuple is positive.

theorem Height.one_le_iSup_option_elim {K : Type u_1} [Field K] {ι : Type u_2} [Finite ι] {F : Type u_4} [FunLike F K ℝ] [MonoidWithZeroHomClass F K ℝ] (v : F) (x : ι → K) : 1 ≤ ⨆ (o : Option ι), v (o.elim 1 x)

The local sup norm of a tuple with a coordinate 1 appended is at least 1.

theorem Height.iSup_option_elim_eq_max {K : Type u_1} [Field K] {ι : Type u_2} [Finite ι] {F : Type u_4} [FunLike F K ℝ] [MonoidWithZeroHomClass F K ℝ] (v : F) (x : ι → K) : ⨆ (o : Option ι), v (o.elim 1 x) = max (⨆ (i : ι), v (x i)) 1

The local factor of the affine height: the local sup norm of a tuple with a coordinate 1 appended is max (⨆ i, v (x i)) 1.

theorem Height.iSup_option_elim_smul_le {K : Type u_1} [Field K] {ι : Type u_2} {F : Type u_4} [FunLike F K ℝ] [MonoidWithZeroHomClass F K ℝ] [NonnegHomClass F K ℝ] (v : F) (c : K) (x : ι → K) : ⨆ (o : Option ι), v (o.elim 1 (c • x)) ≤ max (v c * ⨆ (i : ι), v (x i)) 1

The local factor of the affine height of a scalar multiple c • x is at most max (v c * ⨆ i, v (x i)) 1.

theorem Height.mul_log_iSup_option_elim_smul_le {K : Type u_1} [Field K] {ι : Type u_2} [Finite ι] {F : Type u_4} [FunLike F K ℝ] [MonoidWithZeroHomClass F K ℝ] [NonnegHomClass F K ℝ] (v : F) {x : ι → K} (hx : x ≠ 0) {c : K} (hc : c ≠ 0) {m B : ℝ} (hm : 0 ≤ m) (hB : 0 ≤ B) (h : m * Real.log (v c) + m * Real.log (⨆ (i : ι), v (x i)) ≤ B) : m * Real.log (⨆ (o : Option ι), v (o.elim 1 (c • x))) ≤ B

A logarithmic bound m * log (v c) + m * log (⨆ i, v (x i)) ≤ B with 0 ≤ m and 0 ≤ B bounds m times the logarithm of the local factor of the affine height of c • x.

theorem Height.mulHeightAff_eq {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x : ι → K) : mulHeightAff x = (Multiset.map (fun (v : AbsoluteValue K ℝ) => max (⨆ (i : ι), v (x i)) 1) AdmissibleAbsValues.archAbsVal).prod * ∏ᶠ (v : ↑AdmissibleAbsValues.nonarchAbsVal), max (⨆ (i : ι), ↑v (x i)) 1

The affine height as a product of local factors: at each place v the factor is max (⨆ i, v (x i)) 1, the tuple analogue of the local factor max (v x) 1 of Height.mulHeight₁.

theorem Height.hasFiniteMulSupport_max_iSup_nonarchAbsVal {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x : ι → K) : Function.HasFiniteMulSupport fun (v : ↑AdmissibleAbsValues.nonarchAbsVal) => max (⨆ (i : ι), ↑v (x i)) 1

The nonarchimedean local factor max (⨆ i, v (x i)) 1 of the affine height is 1 at all but finitely many places.

theorem Height.prod_mulHeightAff_eq {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] {κ : Type u_4} [Fintype κ] (y : κ → ι → K) : ∏ k : κ, mulHeightAff (y k) = (Multiset.map (fun (v : AbsoluteValue K ℝ) => ∏ k : κ, max (⨆ (i : ι), v (y k i)) 1) AdmissibleAbsValues.archAbsVal).prod * ∏ᶠ (v : ↑AdmissibleAbsValues.nonarchAbsVal), ∏ k : κ, max (⨆ (i : ι), ↑v (y k i)) 1

A finite product of affine heights, split place by place: the local factor at v is the product ∏ k, max (⨆ i, v (y k i)) 1 of the local factors of the tuples y k.

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

The affine height of a tuple is at least 1.

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

The affine height of a tuple is positive.

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

The affine height of a tuple is nonzero.

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

The affine logarithmic height of a tuple is nonnegative.

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

The projective height of a tuple is at most its affine height.

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

The logarithmic form of Height.mulHeight_le_mulHeightAff.

theorem Height.mulHeightAff_comp_le {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} {ι' : Type u_3} [Finite ι] [Finite ι'] (f : ι → ι') (x : ι' → K) : mulHeightAff (x ∘ f) ≤ mulHeightAff x

The affine height of x ∘ f is at most that of x, for any re-indexing f.

theorem Height.logHeightAff_comp_le {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} {ι' : Type u_3} [Finite ι] [Finite ι'] (f : ι → ι') (x : ι' → K) : logHeightAff (x ∘ f) ≤ logHeightAff x

The logarithmic form of Height.mulHeightAff_comp_le.

theorem Height.mulHeightAff_unique {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} [Unique ι] (x : ι → K) : mulHeightAff x = mulHeight₁ (x default)

On a one-element tuple the affine height is the height Height.mulHeight₁ of the unique coordinate.

theorem Height.logHeightAff_unique {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} [Unique ι] (x : ι → K) : logHeightAff x = logHeight₁ (x default)

The logarithmic form of Height.mulHeightAff_unique.

@[simp]

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

The affine height of ![x] is Height.mulHeight₁ x: with the appended coordinate 1, the affine height of a one-element tuple recovers the height of its entry.

@[simp]

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

The logarithmic form of Height.mulHeightAff_fin_one.

theorem Height.mulHeight₁_le_mulHeightAff {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x : ι → K) (i : ι) : mulHeight₁ (x i) ≤ mulHeightAff x

The height of each coordinate is at most the affine height of the tuple. The analogous bound for Height.mulHeight is false, since the projective height is invariant under scaling.

theorem Height.logHeight₁_le_logHeightAff {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x : ι → K) (i : ι) : logHeight₁ (x i) ≤ logHeightAff x

The logarithmic form of Height.mulHeight₁_le_mulHeightAff.

theorem Height.mulHeightAff_le_prod_mulHeight₁ {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} [Fintype ι] (x : ι → K) : mulHeightAff x ≤ ∏ i : ι, mulHeight₁ (x i)

The affine height is at most the product of the scalar heights of its coordinates.

theorem Height.logHeightAff_le_sum_logHeight₁ {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} [Fintype ι] (x : ι → K) : logHeightAff x ≤ ∑ i : ι, logHeight₁ (x i)

The affine logarithmic height is at most the sum of the scalar logarithmic heights.

theorem Height.exists_mulHeightAff_smul_ne : ∃ (c : ℚ) (x : Fin 1 → ℚ), c ≠ 0 ∧ mulHeightAff (c • x) ≠ mulHeightAff x

The affine height is not invariant under scaling. Over ℚ, doubling the tuple ![1] changes its affine height from 1 to 2, while the projective height of every tuple is unchanged by scaling (Height.mulHeight_smul_eq_mulHeight).

Examples