Comparison of Euclidean and sup heights

The relative Euclidean height arakelovMulHeight and the projective height Height.mulHeight of a tuple over a number field K have the same local factors at the finite places. At an infinite place one uses the Euclidean norm of the embedded tuple and the other its maximum norm, and for a tuple indexed by ι these satisfy max ≤ ℓ² ≤ √#ι · max. Taking the product over the places gives H_K(x) ≤ arakelovMulHeight x ≤ √#ι ^ [K : ℚ] · H_K(x) for the relative heights. For a nonzero tuple the absolute Euclidean height height2 is the [K : ℚ]-th root of arakelovMulHeight, so H(x) ≤ height2 x ≤ √#ι · H(x), where H is absoluteProjectiveTupleHeight.

These comparisons transfer bounds between the two normalizations. For instance, a bound for the sup height of the Plücker coordinates of a subspace bounds its Euclidean height, at the cost of a power of the number of coordinates.

For a tuple of algebraic integers the finite places contribute at most one, so a bound c on the Euclidean norm of the embedded tuple at every infinite place gives height2 x ≤ c.

Main results

• TauCeti.mulHeight_le_arakelovMulHeight: the sup height is at most the Arakelov height.
• TauCeti.arakelovMulHeight_le_sqrt_natCard_pow_mul_mulHeight: the Arakelov height is at most √#ι ^ [K : ℚ] times the sup height.
• TauCeti.absoluteProjectiveTupleHeight_le_height2 and TauCeti.height2_le_sqrt_natCard_mul_absoluteProjectiveTupleHeight: the absolute forms.
• TauCeti.arakelovMulHeight_le_pow_finrank_of_forall_le and TauCeti.height2_le_of_forall_le: Euclidean bounds at the infinite places bound the Euclidean height of a tuple of algebraic integers.
• TauCeti.logHeight_le_arakelovLogHeight and TauCeti.arakelovLogHeight_le_mul_log_natCard_add_logHeight: the logarithmic forms.

References

• J.-H. Evertse and R. G. Ferretti, A further improvement of the quantitative Subspace Theorem, Ann. of Math. 177 (2013), §6.1, (6.1)–(6.4).

theorem TauCeti.mulHeight_le_arakelovMulHeight {K : Type u_1} [Field K] {ι : Type u_2} [Finite ι] [NumberField K] (y : ι → K) : Height.mulHeight y ≤ arakelovMulHeight y

The projective sup height of a tuple over a number field is at most its relative Euclidean projective height. At the zero tuple both heights are one.

theorem TauCeti.arakelovMulHeight_le_sqrt_natCard_pow_mul_mulHeight {K : Type u_1} [Field K] {ι : Type u_2} [Finite ι] [NumberField K] [Nonempty ι] (y : ι → K) : arakelovMulHeight y ≤ √↑(Nat.card ι) ^ Module.finrank ℚ K * Height.mulHeight y

The relative Euclidean projective height of a tuple over a number field K indexed by a nonempty type ι is at most √#ι ^ [K : ℚ] times its projective sup height. The nonemptiness is only needed at the zero tuple, where both heights are one.

theorem TauCeti.absoluteProjectiveTupleHeight_le_height2 {K : Type u_1} [Field K] {ι : Type u_2} [Finite ι] [NumberField K] {y : ι → K} (hy : y ≠ 0) : absoluteProjectiveTupleHeight y ≤ height2 y

The absolute sup height of a nonzero tuple over a number field is at most its absolute Euclidean height. The zero tuple is excluded, since there height2 is zero.

theorem TauCeti.height2_le_sqrt_natCard_mul_absoluteProjectiveTupleHeight {K : Type u_1} [Field K] {ι : Type u_2} [Finite ι] [NumberField K] (y : ι → K) : height2 y ≤ √↑(Nat.card ι) * absoluteProjectiveTupleHeight y

The absolute Euclidean height of a tuple over a number field indexed by ι is at most √#ι times its absolute sup height.

theorem TauCeti.arakelovMulHeight_le_pow_finrank_of_forall_le {K : Type u_1} [Field K] {ι : Type u_2} [Finite ι] [NumberField K] [Fintype ι] {y : ι → NumberField.RingOfIntegers K} (hy : y ≠ 0) {c : ℝ} (hc : ∀ (w : NumberField.InfinitePlace K), √(∑ i : ι, ‖w.embedding ↑(y i)‖ ^ 2) ≤ c) : (arakelovMulHeight fun (i : ι) => ↑(y i)) ≤ c ^ Module.finrank ℚ K

A nonzero tuple of algebraic integers whose embedding at every infinite place has Euclidean norm at most c has relative Euclidean projective height at most c ^ [K : ℚ].

theorem TauCeti.height2_le_of_forall_le {K : Type u_1} [Field K] {ι : Type u_2} [Finite ι] [NumberField K] [Fintype ι] {y : ι → NumberField.RingOfIntegers K} {c : ℝ} (hc : ∀ (w : NumberField.InfinitePlace K), √(∑ i : ι, ‖w.embedding ↑(y i)‖ ^ 2) ≤ c) : (height2 fun (i : ι) => ↑(y i)) ≤ c

A tuple of algebraic integers whose embedding at every infinite place has Euclidean norm at most c has absolute Euclidean height at most c.

theorem TauCeti.logHeight_le_arakelovLogHeight {K : Type u_1} [Field K] {ι : Type u_2} [Finite ι] [NumberField K] (y : ι → K) : Height.logHeight y ≤ arakelovLogHeight y

The logarithmic form of mulHeight_le_arakelovMulHeight.

theorem TauCeti.arakelovLogHeight_le_mul_log_natCard_add_logHeight {K : Type u_1} [Field K] {ι : Type u_2} [Finite ι] [NumberField K] (y : ι → K) : arakelovLogHeight y ≤ ↑(Module.finrank ℚ K) / 2 * Real.log ↑(Nat.card ι) + Height.logHeight y

The logarithmic form of arakelovMulHeight_le_sqrt_natCard_pow_mul_mulHeight: the relative logarithmic Euclidean height exceeds the logarithmic sup height by at most [K : ℚ] / 2 · log #ι.