The Northcott property on projective space

If a field has finitely many elements of bounded scalar height, its finite-dimensional projective spaces have finitely many points of bounded multiplicative or logarithmic height. The instances allow callers to use Northcott.finite_le and Northcott.exists_min_image. Over a number field the scalar hypothesis follows from Mathlib's number-field instance.

Normalizing a nonzero coordinate to 1 bounds the scalar height of every coordinate of the representative by the projective height. Such representatives form a finite product of finite scalar sublevel sets. The statement concerns projective points: tuple heights are invariant under nonzero scaling, so bounded-height tuples need not form a finite set.

References

The proof is adapted from Ralf Stephan's ArithmeticHeights/Northcott.lean in rwst/Subspace-Theorems, commit e443c2479e19f7665b31d8e94e2317c8ced1ca06 (Apache 2.0). The mathematical argument is Hindry–Silverman, Diophantine Geometry: An Introduction, Theorem B.2.3, for points over a fixed number field; see also Bombieri–Gubler, Heights in Diophantine Geometry, Theorem 2.4.9, specialized to projective space and degree 1.

instance Projectivization.instNorthcottMulHeight {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] [Northcott Height.mulHeight₁] : Northcott mulHeight

Projective multiplicative height has the Northcott property whenever scalar multiplicative height does. In particular, this applies to every number field.

instance Projectivization.instNorthcottLogHeight {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] [Northcott mulHeight] : Northcott logHeight

Projective logarithmic height has the Northcott property whenever projective multiplicative height does, and hence whenever scalar multiplicative height does.