The absolute projective height of a tuple

Mathlib's multiplicative height Height.mulHeight x of a finite tuple x over a number field K is relative to K, and NumberField.absMulHeight₁ turns the scalar height into an absolute quantity by computing it in ℚ(x) and taking the [ℚ(x) : ℚ]-th root. This file does the same for tuples: for a finite tuple x in a field F of characteristic zero whose coordinates are algebraic, absoluteProjectiveTupleHeight x is the relative height of x in the number field ℚ(x) generated by the coordinates, raised to the power 1 / [ℚ(x) : ℚ]. A tuple with a transcendental coordinate gets the junk value 1. The zero tuple has value 1, following the projective convention of Height.mulHeight_zero.

The absolute height is the field-independent height of a point of projective space over an algebraic closure of ℚ: it may be computed in any number field containing the coordinates, it is invariant under homomorphisms of fields of characteristic zero, and it is unchanged by nonzero algebraic scalars. The absolute height of an element x is that of the pair (x, 1).

Prepending the coordinate 1 gives the absolute affine logarithmic height TauCeti.absoluteLogHeightAff x = log H(1, x) of a tuple x : Fin n → F, the absolute counterpart of the relative affine height Height.logHeightAff. It is not invariant under scaling, and is the height that measures perturbations in quantitative forms of the subspace theorem.

Main definitions

• TauCeti.absoluteProjectiveTupleHeight: the absolute multiplicative height of a finite tuple.
• TauCeti.absoluteLogHeightAff: the absolute affine logarithmic height of a tuple.

Main results

• TauCeti.absoluteProjectiveTupleHeight_eq: for a tuple x in a number field K, the absolute height is H_K(x) ^ (1 / [K : ℚ]).
• TauCeti.absoluteProjectiveTupleHeight_le_of_forall_le: a nonzero tuple of algebraic integers whose coordinates are at most c at every infinite place has absolute height at most c.
• TauCeti.absoluteProjectiveTupleHeight_comp: invariance under homomorphisms of fields of characteristic zero.
• TauCeti.absoluteProjectiveTupleHeight_smul: invariance under nonzero algebraic scalars.
• TauCeti.absoluteProjectiveTupleHeight_pow: H(x ^ n) = H(x) ^ n, coordinatewise.
• TauCeti.absMulHeight₁_eq_absoluteProjectiveTupleHeight: H(x) = H(x, 1).
• TauCeti.absoluteLogHeightAff_eq: over a number field K, h_aff(x) = Height.logHeight (Fin.cons 1 x) / [K : ℚ].
• TauCeti.absoluteLogHeightAff_eq_logHeightAff_div: over a number field K, h_aff(x) = Height.logHeightAff x / [K : ℚ].
• TauCeti.absoluteLogHeightAff_fin_one: h_aff(x) = h(x) for a one-element tuple.

References

• X. Wu, Diophantine geometry, week 08: arithmetic heights (2023), §2, Lemma 2.5 and Definition 2.7.
• J.-H. Evertse, H. P. Schlickewei and W. M. Schmidt, Linear equations in variables which lie in a multiplicative group, Ann. of Math. 155 (2002), §2, for the affine height of a tuple.

noncomputable def TauCeti.absoluteProjectiveTupleHeight {F : Type u_1} [Field F] [CharZero F] {ι : Type u_3} [Finite ι] (x : ι → F) : ℝ

The absolute multiplicative height of a finite tuple x in a field of characteristic zero. If every coordinate is algebraic, it is the relative height of x in the number field ℚ(x) generated by the coordinates, raised to the power 1 / [ℚ(x) : ℚ]; otherwise it is the junk value 1. The zero tuple has value 1.

theorem TauCeti.absoluteProjectiveTupleHeight_of_not_isIntegral {F : Type u_1} [Field F] [CharZero F] {ι : Type u_3} [Finite ι] {x : ι → F} {i : ι} (hi : ¬IsIntegral ℚ (x i)) : absoluteProjectiveTupleHeight x = 1

A tuple with a transcendental coordinate has the junk absolute height 1.

theorem TauCeti.absoluteProjectiveTupleHeight_eq {ι : Type u_3} [Finite ι] {K : Type u_4} [Field K] [NumberField K] (x : ι → K) : absoluteProjectiveTupleHeight x = Height.mulHeight x ^ (↑(Module.finrank ℚ K))⁻¹

Computation in a number field. For a tuple x in a number field K, the absolute height of x is its height relative to K raised to the power 1 / [K : ℚ].

theorem TauCeti.absoluteProjectiveTupleHeight_le_of_forall_le {ι : Type u_3} [Finite ι] {K : Type u_4} [Field K] [NumberField K] {y : ι → NumberField.RingOfIntegers K} (hy : y ≠ 0) {c : ℝ} (hc : ∀ (i : ι) (w : NumberField.InfinitePlace K), w ↑(y i) ≤ c) : (absoluteProjectiveTupleHeight fun (i : ι) => ↑(y i)) ≤ c

A nonzero tuple of algebraic integers whose coordinates have absolute value at most c at every infinite place has absolute height at most c.

@[simp]

theorem TauCeti.absoluteProjectiveTupleHeight_comp {F : Type u_1} {F' : Type u_2} [Field F] [CharZero F] [Field F'] [CharZero F'] {ι : Type u_3} [Finite ι] (f : F →+* F') (x : ι → F) : absoluteProjectiveTupleHeight (⇑f ∘ x) = absoluteProjectiveTupleHeight x

The absolute height is invariant under homomorphisms of fields of characteristic zero.

@[simp]

theorem TauCeti.absoluteProjectiveTupleHeight_zero {F : Type u_1} [Field F] [CharZero F] {ι : Type u_3} [Finite ι] : absoluteProjectiveTupleHeight 0 = 1

The zero tuple has absolute height 1.

theorem TauCeti.one_le_absoluteProjectiveTupleHeight {F : Type u_1} [Field F] [CharZero F] {ι : Type u_3} [Finite ι] (x : ι → F) : 1 ≤ absoluteProjectiveTupleHeight x

The absolute height of a tuple is at least 1.

theorem TauCeti.absoluteProjectiveTupleHeight_pos {F : Type u_1} [Field F] [CharZero F] {ι : Type u_3} [Finite ι] (x : ι → F) : 0 < absoluteProjectiveTupleHeight x

The absolute height of a tuple is positive.

@[simp]

theorem TauCeti.absoluteProjectiveTupleHeight_eq_one_of_subsingleton {F : Type u_1} [Field F] [CharZero F] {ι : Type u_3} [Subsingleton ι] (x : ι → F) : absoluteProjectiveTupleHeight x = 1

A tuple with at most one coordinate has absolute projective height one, including the empty tuple and the transcendental junk branch.

@[simp]

theorem TauCeti.absoluteProjectiveTupleHeight_comp_equiv {F : Type u_1} [Field F] [CharZero F] {ι : Type u_3} [Finite ι] {ι' : Type u_4} [Finite ι'] (e : ι ≃ ι') (x : ι' → F) : absoluteProjectiveTupleHeight (x ∘ ⇑e) = absoluteProjectiveTupleHeight x

The absolute height is invariant under reordering the coordinates.

@[simp]

theorem TauCeti.absoluteProjectiveTupleHeight_one {F : Type u_1} [Field F] [CharZero F] {ι : Type u_3} [Finite ι] : absoluteProjectiveTupleHeight 1 = 1

The constant tuple 1 has absolute height 1.

theorem TauCeti.absoluteProjectiveTupleHeight_comp_le {F : Type u_1} [Field F] [CharZero F] {ι : Type u_3} [Finite ι] {ι' : Type u_4} [Finite ι'] {x : ι → F} (hx : ∀ (i : ι), IsAlgebraic ℚ (x i)) (f : ι' → ι) : absoluteProjectiveTupleHeight (x ∘ f) ≤ absoluteProjectiveTupleHeight x

Restricting or repeating the coordinates of a tuple with algebraic coordinates along any map does not increase its absolute height. The algebraicity hypothesis is needed because a tuple with a transcendental coordinate has the junk height 1.

theorem TauCeti.absoluteProjectiveTupleHeight_pow {F : Type u_1} [Field F] [CharZero F] {ι : Type u_3} [Finite ι] (x : ι → F) (n : ℕ) : absoluteProjectiveTupleHeight (x ^ n) = absoluteProjectiveTupleHeight x ^ n

The absolute height of the coordinatewise n-th power of a tuple is the n-th power of its absolute height.

theorem TauCeti.absoluteProjectiveTupleHeight_smul {F : Type u_1} [Field F] [CharZero F] {ι : Type u_3} [Finite ι] (x : ι → F) {c : F} (hc : c ≠ 0) (hcalg : IsAlgebraic ℚ c) : absoluteProjectiveTupleHeight (c • x) = absoluteProjectiveTupleHeight x

A nonzero algebraic scalar does not change the absolute height of a tuple.

theorem TauCeti.absMulHeight₁_eq_absoluteProjectiveTupleHeight {F : Type u_1} [Field F] [CharZero F] (x : F) : NumberField.absMulHeight₁ x = absoluteProjectiveTupleHeight ![x, 1]

The absolute height of an element x is the absolute height of the pair (x, 1).

The absolute affine logarithmic height

noncomputable def TauCeti.absoluteLogHeightAff {F : Type u_1} [Field F] [CharZero F] {n : ℕ} (x : Fin n → F) : ℝ

The absolute affine logarithmic height h_aff(x) of a tuple x : Fin n → F in a field of characteristic zero: the logarithm of the absolute height of the tuple (1, x) obtained by prepending the coordinate 1. Over a number field K containing the coordinates it is Height.logHeight (Fin.cons 1 x) / [K : ℚ] (TauCeti.absoluteLogHeightAff_eq).

Unlike the absolute height of x, it is not invariant under scaling: (1/3, 1/3) has absolute projective height 1 but absolute affine logarithmic height log 3. A tuple with a transcendental coordinate has the junk value 0.

theorem TauCeti.absoluteLogHeightAff_def {F : Type u_1} [Field F] [CharZero F] {n : ℕ} (x : Fin n → F) : absoluteLogHeightAff x = Real.log (absoluteProjectiveTupleHeight (Fin.cons 1 x))

The defining formula of TauCeti.absoluteLogHeightAff.

theorem TauCeti.absoluteLogHeightAff_nonneg {F : Type u_1} [Field F] [CharZero F] {n : ℕ} (x : Fin n → F) : 0 ≤ absoluteLogHeightAff x

The absolute affine logarithmic height is nonnegative.

@[simp]

theorem TauCeti.absoluteLogHeightAff_comp {F : Type u_1} {F' : Type u_2} [Field F] [CharZero F] [Field F'] [CharZero F'] {n : ℕ} (f : F →+* F') (x : Fin n → F) : absoluteLogHeightAff (⇑f ∘ x) = absoluteLogHeightAff x

The absolute affine logarithmic height is invariant under homomorphisms of fields of characteristic zero.

theorem TauCeti.absoluteLogHeightAff_eq {n : ℕ} {K : Type u_4} [Field K] [NumberField K] (x : Fin n → K) : absoluteLogHeightAff x = Height.logHeight (Fin.cons 1 x) / ↑(Module.finrank ℚ K)

Computation in a number field. For a tuple x in a number field K, the absolute affine logarithmic height is the logarithmic height of (1, x) relative to K divided by [K : ℚ]. With TauCeti.absoluteLogHeightAff_comp this computes absoluteLogHeightAff (f ∘ x) for every embedding f of K into a field of characteristic zero.

theorem TauCeti.absoluteLogHeightAff_eq_logHeightAff_div {n : ℕ} {K : Type u_4} [Field K] [NumberField K] (x : Fin n → K) : absoluteLogHeightAff x = Height.logHeightAff x / ↑(Module.finrank ℚ K)

For a tuple x in a number field K, the absolute affine logarithmic height is the affine logarithmic height Height.logHeightAff x relative to K divided by [K : ℚ]. The two differ only in where the coordinate 1 is placed, so this is a re-indexing. With TauCeti.absoluteLogHeightAff_comp it computes absoluteLogHeightAff (f ∘ x) for every embedding f of K into a field of characteristic zero, such as an algebraic closure of ℚ.

@[simp]

theorem TauCeti.absoluteLogHeightAff_zero {F : Type u_1} [Field F] [CharZero F] {n : ℕ} : absoluteLogHeightAff 0 = 0

The zero tuple has absolute affine logarithmic height 0.

@[simp]

theorem TauCeti.absoluteLogHeightAff_one {F : Type u_1} [Field F] [CharZero F] {n : ℕ} : absoluteLogHeightAff 1 = 0

The tuple of ones has absolute affine logarithmic height 0.

@[simp]

theorem TauCeti.absoluteLogHeightAff_fin_one {F : Type u_1} [Field F] [CharZero F] (x : F) : absoluteLogHeightAff ![x] = NumberField.absLogHeight₁ x

The absolute affine logarithmic height of ![x] is the absolute logarithmic height of x: with the coordinate 1 prepended, the height of a one-element tuple recovers the height of its entry.