Rational projective points with the multiplicative height used by CCDN. Bounded-height sets are finite, and primitive integral coordinates recover the paper's maximum-coordinate height.

@[reducible, inline]

abbrev CCDN.ProjectivePoint (n : ℕ) : Type

Rational points of projective n-space, as lines in ℚ^(n+1).

Equations

• CCDN.ProjectivePoint n = Projectivization ℚ (Fin (n + 1) → ℚ)

theorem CCDN.projective_rep_height {n : ℕ} (x : ProjectivePoint n) : Height.mulHeight (Projectivization.rep x) = Projectivization.mulHeight x

The multiplicative height of the chosen representative of a projective point equals the height of the point.

theorem CCDN.projective_height_finite (n : ℕ) (B : ℝ) : {x : ProjectivePoint n | Projectivization.mulHeight x ≤ B}.Finite

Northcott finiteness in rational projective space, proved using affine charts.

noncomputable def CCDN.projectivePoints {n : ℕ} (X : Set (ProjectivePoint n)) (B : ℝ) : Finset (ProjectivePoint n)

Projective points, counted once per rational line.

Equations

• CCDN.projectivePoints X B = {x ∈ ⋯.toFinset | x ∈ X}

noncomputable def CCDN.projectiveCount {n : ℕ} (X : Set (ProjectivePoint n)) (B : ℝ) : ℕ

The number of points of X of multiplicative height at most B.

Equations

• CCDN.projectiveCount X B = (CCDN.projectivePoints X B).card

theorem CCDN.mem_projectivePoints {n : ℕ} {X : Set (ProjectivePoint n)} {B : ℝ} {x : ProjectivePoint n} : x ∈ projectivePoints X B ↔ Projectivization.mulHeight x ≤ B ∧ x ∈ X

A projective point belongs to projectivePoints X B exactly when it lies in X and has height at most B.

theorem CCDN.projectiveCount_mono {n : ℕ} {X Y : Set (ProjectivePoint n)} {B C : ℝ} (hXY : X ⊆ Y) (hBC : B ≤ C) : projectiveCount X B ≤ projectiveCount Y C

The projective point count is monotone in both the set and the height bound.

theorem CCDN.rationalPoint_ne_zero {n : ℕ} {x : IntPoint n} (hx : x ≠ 0) : rationalPoint x ≠ 0

A nonzero integer point remains nonzero as a rational point.

theorem CCDN.projective_height_primitive {n : ℕ} (x : IntPoint (n + 1)) (hx : x ≠ 0) (hprimitive : Finset.univ.gcd x = 1) : (Projectivization.mk ℚ (rationalPoint x) ⋯).mulHeight = ↑(⨆ (i : Fin (n + 1)), |x i|)

The chosen projective height is exactly CCDN's height on primitive coordinates.