Euclidean heights over number fields

This file defines the degree-normalized Euclidean height height2 of a finite tuple over a number field. At an infinite place it uses the Euclidean norm of the tuple, while at a finite place it uses the maximum norm. The relative Arakelov height arakelovMulHeight is its field-degree power, with the usual projective junk value one at the zero tuple.

The local formula and its normalization follow Evertse--Ferretti, where this Euclidean height is used for Plücker coordinates of subspaces. The elementary API here records the zero convention, reindexing, sign changes of coordinates, and the corresponding logarithmic and affine heights. Over ℚ, the Euclidean height of a tuple of coprime integers is its Euclidean norm (TauCeti.height2_intCast_eq_sqrt_of_gcd_eq_one), and for any tuple of integers it is the Euclidean norm divided by the greatest common divisor of the entries (TauCeti.gcd_mul_height2_intCast).

Main definitions

• TauCeti.height2: the absolute Euclidean height of a tuple over a number field.
• TauCeti.arakelovMulHeight: the relative Euclidean projective height.
• TauCeti.arakelovLogHeight: the logarithm of the relative Euclidean projective height.
• TauCeti.arakelovMulHeightAff: the relative affine Euclidean height of a finite tuple.
• TauCeti.arakelovLogHeightAff: its logarithm.

References

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

TauCeti.height2_intCast_eq_sqrt_of_gcd_eq_one is adapted from Ralf Stephan's NumberField.arakelovMulHeight_intCast_of_gcd_eq_one in ArithmeticHeights/RationalLattice.lean of rwst/Subspace-Theorems, commit 9894a1c4baf805296b249e95575f0e16e8e1afa3 (Apache 2.0), and TauCeti.gcd_mul_height2_intCast from his NumberField.gcd_mul_arakelovMulHeight_intCast in ArithmeticHeights/BombieriVaaler.lean of the same repository at commit 09835cb23557ae5ae0cf55a9c4ab9055f5d60338.

noncomputable def TauCeti.height2 {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] (y : ι → K) : ℝ

The degree-normalized Euclidean height of a finite tuple over a number field. It uses the Euclidean norm at infinite places and the maximum norm at finite places. In particular, its value at the zero tuple is zero.

theorem TauCeti.height2_eq {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] (y : ι → K) : height2 y = (∏ w : NumberField.InfinitePlace K, (∑ i : ι, ‖w.embedding (y i)‖ ^ 2) ^ (↑w.mult / (2 * ↑(Module.finrank ℚ K)))) * ∏ᶠ (v : NumberField.FinitePlace K), (⨆ (i : ι), v (y i)) ^ (1 / ↑(Module.finrank ℚ K))

The local formula defining the Euclidean height.

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

The Euclidean height is nonnegative.

@[simp]

theorem TauCeti.height2_zero {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] : height2 0 = 0

The Euclidean height of the zero tuple is zero.

@[simp]

theorem TauCeti.height2_comp_equiv {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} {ι' : Type u_3} [Finite ι] [Finite ι'] (e : ι ≃ ι') (y : ι' → K) : height2 (y ∘ ⇑e) = height2 y

The Euclidean height is unchanged by a bijective reindexing of the coordinates.

noncomputable def TauCeti.arakelovMulHeight {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] (y : ι → K) : ℝ

The relative Euclidean projective height. It is the field-degree power of height2 away from zero, and has the projective junk value one at the zero tuple.

noncomputable def TauCeti.arakelovLogHeight {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] (y : ι → K) : ℝ

The relative logarithmic Euclidean projective height.

noncomputable def TauCeti.arakelovMulHeightAff {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] (x : ι → K) : ℝ

The relative affine Euclidean height of a finite tuple, obtained by adjoining the coordinate one.

theorem TauCeti.arakelovMulHeightAff_def {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] (x : ι → K) : arakelovMulHeightAff x = arakelovMulHeight fun (o : Option ι) => o.elim 1 x

The affine height is the projective height of the tuple with the coordinate one adjoined.

noncomputable def TauCeti.arakelovLogHeightAff {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] (x : ι → K) : ℝ

The relative logarithmic affine Euclidean height of a finite tuple.

@[simp]

theorem TauCeti.arakelovMulHeight_zero {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] : arakelovMulHeight 0 = 1

The relative Euclidean projective height assigns its junk value one to the zero tuple.

theorem TauCeti.arakelovMulHeight_of_ne_zero {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] {y : ι → K} (hy : y ≠ 0) : arakelovMulHeight y = height2 y ^ Module.finrank ℚ K

Away from zero, the relative height is the field-degree power of height2.

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

The relative Euclidean projective height is nonnegative.

theorem TauCeti.arakelovMulHeight_eq {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] {y : ι → K} (hy : y ≠ 0) : arakelovMulHeight y = (∏ w : NumberField.InfinitePlace K, (∑ i : ι, ‖w.embedding (y i)‖ ^ 2) ^ (↑w.mult / 2)) * ∏ᶠ (v : NumberField.FinitePlace K), ⨆ (i : ι), v (y i)

The local formula for the relative Euclidean projective height of a nonzero tuple. The degree power removes the normalizing field-degree roots from height2.

theorem TauCeti.arakelovMulHeight_mul_absNorm_span_range {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] {y : ι → NumberField.RingOfIntegers K} (hy : y ≠ 0) : (arakelovMulHeight fun (i : ι) => ↑(y i)) * ↑(Ideal.absNorm (Ideal.span (Set.range y))) = ∏ w : NumberField.InfinitePlace K, (∑ i : ι, ‖w.embedding ↑(y i)‖ ^ 2) ^ (↑w.mult / 2)

For a nonzero integral tuple, multiplying its relative Euclidean height by the norm of its coordinate ideal leaves precisely the archimedean Euclidean factors.

@[simp]

theorem TauCeti.arakelovMulHeight_smul {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] (y : ι → K) {c : K} (hc : c ≠ 0) : arakelovMulHeight (c • y) = arakelovMulHeight y

Multiplication by a nonzero number-field scalar preserves the relative Euclidean projective height.

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

The relative Euclidean projective height is at least one.

theorem TauCeti.arakelovMulHeight_pos {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] (y : ι → K) : 0 < arakelovMulHeight y

The relative Euclidean projective height is positive.

theorem TauCeti.arakelovMulHeight_ne_zero {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] (y : ι → K) : arakelovMulHeight y ≠ 0

The relative Euclidean projective height is nonzero.

theorem TauCeti.arakelovMulHeight_eq_height2 {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] (y : ι → K) : arakelovMulHeight y ^ (1 / ↑(Module.finrank ℚ K)) = if y = 0 then 1 else height2 y

Taking the field-degree root recovers height2 away from zero and preserves the projective junk value at zero.

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

A nonzero tuple has Euclidean height at least one.

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

The Euclidean height of a nonzero tuple is positive.

@[simp]

theorem TauCeti.height2_eq_zero_iff {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] {y : ι → K} : height2 y = 0 ↔ y = 0

The Euclidean height vanishes exactly on the zero tuple.

@[simp]

theorem TauCeti.height2_smul {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] (y : ι → K) {c : K} (hc : c ≠ 0) : height2 (c • y) = height2 y

Multiplication by a nonzero number-field scalar preserves the degree-normalized Euclidean height.

@[simp]

theorem TauCeti.arakelovMulHeight_comp_equiv {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} {ι' : Type u_3} [Finite ι] [Finite ι'] (e : ι ≃ ι') (y : ι' → K) : arakelovMulHeight (y ∘ ⇑e) = arakelovMulHeight y

The relative Euclidean projective height is unchanged by a bijective reindexing of the coordinates.

theorem TauCeti.height2_eq_of_forall_eq_or_eq_neg {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] {x y : ι → K} (h : ∀ (i : ι), y i = x i ∨ y i = -x i) : height2 y = height2 x

The Euclidean height is unchanged by changing the signs of some coordinates.

theorem TauCeti.arakelovMulHeight_eq_of_forall_eq_or_eq_neg {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] {x y : ι → K} (h : ∀ (i : ι), y i = x i ∨ y i = -x i) : arakelovMulHeight y = arakelovMulHeight x

The relative Euclidean projective height is unchanged by changing the signs of some coordinates.

@[simp]

theorem TauCeti.arakelovLogHeight_zero {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] : arakelovLogHeight 0 = 0

The logarithmic projective height of the zero tuple is zero.

theorem TauCeti.arakelovLogHeight_eq_log_arakelovMulHeight {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] (y : ι → K) : arakelovLogHeight y = Real.log (arakelovMulHeight y)

The multiplicative and logarithmic relative Euclidean heights agree by definition.

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

The relative logarithmic Euclidean height is nonnegative.

@[simp]

theorem TauCeti.arakelovLogHeight_smul {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] (y : ι → K) {c : K} (hc : c ≠ 0) : arakelovLogHeight (c • y) = arakelovLogHeight y

The relative logarithmic Euclidean height is invariant under nonzero scalar multiplication.

@[simp]

theorem TauCeti.arakelovLogHeight_comp_equiv {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} {ι' : Type u_3} [Finite ι] [Finite ι'] (e : ι ≃ ι') (y : ι' → K) : arakelovLogHeight (y ∘ ⇑e) = arakelovLogHeight y

The relative logarithmic height is unchanged by a bijective reindexing.

theorem TauCeti.arakelovLogHeight_eq_of_forall_eq_or_eq_neg {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] {x y : ι → K} (h : ∀ (i : ι), y i = x i ∨ y i = -x i) : arakelovLogHeight y = arakelovLogHeight x

The logarithmic projective height is unchanged by changing the signs of some coordinates.

theorem TauCeti.arakelovLogHeightAff_eq_log_arakelovMulHeightAff {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] (x : ι → K) : arakelovLogHeightAff x = Real.log (arakelovMulHeightAff x)

The affine multiplicative and logarithmic heights agree by definition.

theorem TauCeti.one_le_arakelovMulHeightAff {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] (x : ι → K) : 1 ≤ arakelovMulHeightAff x

The relative affine Euclidean height is at least one.

theorem TauCeti.arakelovLogHeightAff_nonneg {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] (x : ι → K) : 0 ≤ arakelovLogHeightAff x

The relative logarithmic affine Euclidean height is nonnegative.

@[simp]

theorem TauCeti.arakelovMulHeightAff_comp_equiv {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} {ι' : Type u_3} [Finite ι] [Finite ι'] (e : ι ≃ ι') (x : ι' → K) : arakelovMulHeightAff (x ∘ ⇑e) = arakelovMulHeightAff x

The relative affine Euclidean height is unchanged by a bijective reindexing.

@[simp]

theorem TauCeti.arakelovLogHeightAff_comp_equiv {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} {ι' : Type u_3} [Finite ι] [Finite ι'] (e : ι ≃ ι') (x : ι' → K) : arakelovLogHeightAff (x ∘ ⇑e) = arakelovLogHeightAff x

The relative logarithmic affine Euclidean height is unchanged by a bijective reindexing.

@[simp]

theorem TauCeti.arakelovMulHeightAff_zero {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] : arakelovMulHeightAff 0 = 1

The affine height of the zero tuple is one because the adjoined coordinate is one.

@[simp]

theorem TauCeti.arakelovLogHeightAff_zero {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] : arakelovLogHeightAff 0 = 0

The logarithmic affine height of the zero tuple is zero.

theorem TauCeti.height2_intCast_eq_sqrt_of_gcd_eq_one {ι : Type u_2} [Fintype ι] {x : ι → ℤ} (hx : Finset.univ.gcd x = 1) : height2 (Int.cast ∘ x) = √(∑ i : ι, ↑(x i) ^ 2)

Over ℚ, the Euclidean height of a tuple of coprime integers is its Euclidean norm: the finite places do not contribute. This is the Euclidean analogue of Mathlib's Rat.mulHeight_eq_max_abs_of_gcd_eq_one.

theorem TauCeti.gcd_mul_height2_intCast {ι : Type u_2} [Fintype ι] (x : ι → ℤ) : ↑(Finset.univ.gcd x) * height2 (Int.cast ∘ x) = √(∑ i : ι, ↑(x i) ^ 2)

Over ℚ, the Euclidean height of a tuple of integers, multiplied by the greatest common divisor of its entries, is its Euclidean norm. Both sides vanish for the zero tuple. This is the Euclidean analogue of the sup-norm statement that the height of an integer tuple is its largest absolute value divided by the greatest common divisor of its entries.