Primitive integral representatives of rational projective points.

theorem CCDN.exists_primitive_projective_rep {n : ℕ} (x : ProjectivePoint n) : ∃ (z : IntPoint (n + 1)) (hz : z ≠ 0), Finset.univ.gcd z = 1 ∧ Projectivization.mk ℚ (rationalPoint z) ⋯ = x

Every rational projective point is spanned by a nonzero integer vector whose coordinates have gcd 1.

noncomputable def CCDN.primitiveProjectiveRep {n : ℕ} (x : ProjectivePoint n) : IntPoint (n + 1)

A chosen primitive integer representative of the projective point x: a nonzero integer vector with coprime coordinates spanning x.

Equations

• CCDN.primitiveProjectiveRep x = ⋯.choose

theorem CCDN.primitiveProjectiveRep_ne_zero {n : ℕ} (x : ProjectivePoint n) : primitiveProjectiveRep x ≠ 0

The primitive integer representative of a projective point is nonzero.

theorem CCDN.primitiveProjectiveRep_gcd {n : ℕ} (x : ProjectivePoint n) : Finset.univ.gcd (primitiveProjectiveRep x) = 1

The coordinates of the primitive integer representative of a projective point have gcd 1.

theorem CCDN.primitiveProjectiveRep_mk {n : ℕ} (x : ProjectivePoint n) : Projectivization.mk ℚ (rationalPoint (primitiveProjectiveRep x)) ⋯ = x

The primitive integer representative of x spans x.

theorem CCDN.primitiveProjectiveRep_injective {n : ℕ} : Function.Injective primitiveProjectiveRep

Distinct projective points have distinct primitive integer representatives.

theorem CCDN.primitiveProjectiveRep_bound {n : ℕ} (x : ProjectivePoint n) (i : Fin (n + 1)) : |↑(primitiveProjectiveRep x i)| ≤ Projectivization.mulHeight x

Every coordinate of the primitive integer representative of x has absolute value at most the multiplicative height of x.