The affine height of a tuple

Mathlib's Height.mulHeight is a height on projective space: it is invariant under scaling, and so is a function of the line through a tuple rather than of the tuple. That is the right object for a point of ℙⁿ and the wrong one for anything not homogeneous — the value ∑ i, a i * x i of a linear form, or the determinant of a matrix, both of which scale with the tuple. This file adds the affine height, the projective height of the tuple with a coordinate 1 appended:

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

It is the tuple analogue of Mathlib's Height.mulHeight₁ x = mulHeight ![x, 1], and agrees with it on a one-element tuple (Height.mulHeightAff_fin_one). Being a normalization and not a theorem, it is stated here in Layer 0 rather than at its first use.

mulHeightAff is deliberately not scaling-invariant, and Height.exists_mulHeightAff_smul_ne records that as a theorem: over ℚ the tuples ![1] and ![2] have affine heights 1 and 2. That failure is the content of the definition, not a defect of it. What survives is one-sided: the affine height dominates the projective height and the height of every single coordinate, and is monotone under re-indexing.

Main definitions

• Height.mulHeightAff x for x : ι → K, and Height.logHeightAff x its logarithm.

Main results

• Height.mulHeight_le_mulHeightAff and Height.mulHeight₁_le_mulHeightAff: the affine height dominates the projective height of the tuple and the height of each coordinate. The second is false for Height.mulHeight.
• Height.mulHeightAff_comp_le and Height.mulHeightAff_comp_equiv: monotonicity under re-indexing, and invariance under a bijective one.
• 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 scaling-invariant.

Implementation notes

The appended coordinate is indexed by none : Option ι rather than by Sum.inl of a Unit or by Fin.succ: Option ι needs no Fintype bookkeeping, inherits Finite ι by instance resolution, and makes re-indexing along f : ι → ι' literally Option.map f.

No Arakelov analogue is defined here. Layer 0.1 already has the one-variable NumberField.arakelovMulHeight₁, and no bound in the roadmap needs an affine Arakelov height of a tuple; the Arakelov bounds that would want one carry the constant 1 and need no affine height at all.

References

E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006), §1.5, where the affine and projective heights of a point are distinguished throughout.

This is Layer 0.5 of the ArithmeticHeights roadmap.

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

The affine height of a tuple: the projective height of the tuple with a coordinate 1 appended.

Unlike Height.mulHeight this is not invariant under scaling (Height.exists_mulHeightAff_smul_ne), and that is exactly what a bound on a non-homogeneous quantity needs: the value ∑ i, a i * x i of a linear form is not a function on projective space, so no scaling-invariant quantity can bound its height. The affine height dominates the projective height (Height.mulHeight_le_mulHeightAff) and the height of every single coordinate (Height.mulHeight₁_le_mulHeightAff), neither of which mulHeight does.

Equations

• Height.mulHeightAff x = Height.mulHeight fun (o : Option ι) => o.elim 1 x

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

The affine logarithmic height of a tuple. As everywhere in this development, the logarithmic height is defined as the logarithm of the multiplicative one.

Equations

• Height.logHeightAff x = Real.log (Height.mulHeightAff x)

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)

theorem Height.optionElim_one_ne_zero {K : Type u_1} [Field K] {ι : Type u_2} (x : ι → K) : (fun (o : Option ι) => o.elim 1 x) ≠ 0

The tuple whose height is Height.mulHeightAff x is never zero: its coordinate at none is 1. This is what makes the affine height positive with no hypothesis on x, and it is the nondegeneracy that consumers of the Segre relation need.

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

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

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

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

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.mulHeight₁_le_mulHeightAff {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x : ι → K) (i : ι) : mulHeight₁ (x i) ≤ mulHeightAff x

The affine height of a tuple dominates the affine height of each of its coordinates. This is false for Height.mulHeight, which 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_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 is monotone under re-indexing: the appended coordinate 1 is common to both tuples, so re-indexing along f is re-indexing along Option.map 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_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.

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.mulHeightAff_zero {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] : mulHeightAff 0 = 1

The affine height of the zero tuple is 1 — not by a junk-value convention but because the tuple whose height is taken is (1, 0, …, 0).

@[simp]

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

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

The affine height extends Mathlib's Height.mulHeight₁: on a one-element tuple the two agree. This is the check that the appended coordinate is the right one; a definition that appended a different constant, or that normalized by the degree, would fail it.

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.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] doubles its affine height. This is the whole point of the definition: a bound on a quantity that scales with its argument — the value of a linear form, the determinant of a matrix — cannot have a scaling-invariant right-hand side, so Height.mulHeight cannot appear there and Height.mulHeightAff must.

Examples

The acceptance criterion the roadmap states for this milestone: the affine and projective heights of one and the same tuple differ, so the appended coordinate is doing something.