The bounded integral affine projection lifts to a projective plane map on the standard chart, with the same polynomial height factor.

theorem CCDN.affineProjectivePoint_eq_integer {n : ℕ} (z : IntPoint (n + 1)) (hz0 : z 0 ≠ 0) : (affineProjectivePoint fun (j : Fin n) => ↑(z j.succ) / ↑(z 0)) = Projectivization.mk ℚ (rationalPoint z) ⋯

For an integer vector z with z 0 ≠ 0, the projective point [1 : z 1 / z 0 : …] is the point with homogeneous coordinates z.

noncomputable def CCDN.projectivePlaneChartProjection {n : ℕ} (k₀ k₁ : ℕ) (x : ProjectivePoint n) : ProjectivePoint 2

The map from ℙⁿ to the projective plane on the chart X₀ ≠ 0, sending a point with affine coordinates x to [1 : m₀(x) : m₁(x)], where m₀, m₁ are the moment coordinates with parameters k₀ and k₁.

Equations

• One or more equations did not get rendered due to their size.

theorem CCDN.projectivePlaneChartProjection_height {n d k₀ k₁ : ℕ} (hk₀ : k₀ ≤ n ^ 2 * d) (hk₁ : k₁ ≤ n * d ^ 2) (x : ProjectivePoint n) (hx : Projectivization.rep x 0 ≠ 0) {B : ℝ} (hB : 1 ≤ B) (hxB : Projectivization.mulHeight x ≤ B) : Projectivization.mulHeight (projectivePlaneChartProjection k₀ k₁ x) ≤ projectionBoxFactor n d * B

For parameters k₀ ≤ n ^ 2 * d and k₁ ≤ n * d ^ 2, the plane chart projection of a point on the chart X₀ ≠ 0 of height at most B ≥ 1 has height at most projectionBoxFactor n d * B.

theorem CCDN.projectivePlaneChartProjection_zero {n d k₀ k₁ : ℕ} (I : Ideal (MvPolynomial (Fin (n + 1)) ℚ)) [I.IsPrime] (hX : MvPolynomial.X 0 ∉ I) (f : MvPolynomial (Fin 2) ℚ) (hfd : f.totalDegree = d) (hfI : (MvPolynomial.aeval ![momentCoordinate ℚ n k₀, momentCoordinate ℚ n k₁]) f ∈ projectiveChartIdeal I) (x : ProjectivePoint n) (hx : x ∈ projectiveIdealZeroLocus I) (hx0 : Projectivization.rep x 0 ≠ 0) : projectivePlaneChartProjection k₀ k₁ x ∈ projectiveZeroLocus (scaledHomogenize d 1 f)

If the moment coordinates satisfy the plane relation f of degree d on the affine chart of the prime I (with X 0 ∉ I), then the plane chart projection maps the points of the projective variety of I on the chart X₀ ≠ 0 into the projective plane curve defined by the homogenization of f.