Projective reduction of primitive integer points, and the affine coordinate charts determined by their finite-field residue points.

@[reducible, inline]

abbrev CCDN.ProjectiveResidueSpace (n p : ℕ) [Fact (Nat.Prime p)] : Type

The projective space ℙⁿ(𝔽_p) over the prime field 𝔽_p.

Equations

• CCDN.ProjectiveResidueSpace n p = Projectivization (ZMod p) (Fin (n + 1) → ZMod p)

theorem CCDN.primitive_mod_ne_zero {n p : ℕ} [Fact (Nat.Prime p)] (z : IntPoint n) (hz : Finset.univ.gcd z = 1) : (fun (i : Fin n) => ↑(z i)) ≠ 0

A primitive integer vector has nonzero reduction modulo every prime.

def CCDN.primitiveProjectiveReduction {n p : ℕ} [Fact (Nat.Prime p)] (z : IntPoint (n + 1)) (hz : Finset.univ.gcd z = 1) : ProjectiveResidueSpace n p

The reduction modulo p of a primitive integer point, as a point of ℙⁿ(𝔽_p).

Equations

• CCDN.primitiveProjectiveReduction z hz = Projectivization.mk (ZMod p) (fun (i : Fin (n + 1)) => ↑(z i)) ⋯

noncomputable def CCDN.projectiveResiduePivot {n p : ℕ} [Fact (Nat.Prime p)] (r : ProjectiveResidueSpace n p) : Fin (n + 1)

A coordinate index at which the chosen representative of a point of ℙⁿ(𝔽_p) is nonzero.

Equations

• CCDN.projectiveResiduePivot r = Classical.choose ⋯

theorem CCDN.projectiveResiduePivot_ne_zero {n p : ℕ} [Fact (Nat.Prime p)] (r : ProjectiveResidueSpace n p) : Projectivization.rep r (projectiveResiduePivot r) ≠ 0

The representative of r is nonzero at the coordinate projectiveResiduePivot r.

noncomputable def CCDN.projectiveResidueChartLift {n p : ℕ} [Fact (Nat.Prime p)] (r : ProjectiveResidueSpace n p) : Fin n → ℤ

Integer lifts of the affine coordinates of a point r of ℙⁿ(𝔽_p) in the chart where its pivot coordinate projectiveResiduePivot r is moved to the front and set to 1.

Equations

• CCDN.projectiveResidueChartLift r j = ↑(Projectivization.rep r ((Equiv.swap 0 (CCDN.projectiveResiduePivot r)) j.succ) / Projectivization.rep r (CCDN.projectiveResiduePivot r)).val

theorem CCDN.cast_projectiveResidueChartLift {n p : ℕ} [Fact (Nat.Prime p)] (r : ProjectiveResidueSpace n p) (j : Fin n) : ↑(projectiveResidueChartLift r j) = Projectivization.rep r ((Equiv.swap 0 (projectiveResiduePivot r)) j.succ) / Projectivization.rep r (projectiveResiduePivot r)

Modulo p, projectiveResidueChartLift r gives the coordinates of r divided by its pivot coordinate, with the pivot coordinate swapped to the front.

theorem CCDN.projectiveResidueChart_normalized {n p : ℕ} [Fact (Nat.Prime p)] (r : ProjectiveResidueSpace n p) : (Fin.cons 1 fun (j : Fin n) => ↑(projectiveResidueChartLift r j)) ∘ ⇑(Equiv.swap 0 (projectiveResiduePivot r)) = (Projectivization.rep r (projectiveResiduePivot r))⁻¹ • Projectivization.rep r

The selected affine chart recovers the representative normalized by its pivot coordinate.

theorem CCDN.projectiveResidueChart_injective_of_pivot_eq {n p : ℕ} [Fact (Nat.Prime p)] {r t : ProjectiveResidueSpace n p} (hk : projectiveResiduePivot r = projectiveResiduePivot t) (ha : (fun (j : Fin n) => ↑(projectiveResidueChartLift r j)) = fun (j : Fin n) => ↑(projectiveResidueChartLift t j)) : r = t

Within a fixed pivot chart, affine residue coordinates determine the projective point.

theorem CCDN.primitiveProjectiveReduction_chart {n p : ℕ} [Fact (Nat.Prime p)] (z : IntPoint (n + 1)) (hz : Finset.univ.gcd z = 1) (r : ProjectiveResidueSpace n p) (he : primitiveProjectiveReduction z hz = r) : IsCoprime (↑p) (z (projectiveResiduePivot r)) ∧ ∀ (j : Fin n), ↑p ∣ z ((Equiv.swap 0 (projectiveResiduePivot r)) j.succ) - projectiveResidueChartLift r j * z (projectiveResiduePivot r)

Reduction determines both a unit coordinate and all affine congruences; these are derived from equality of projective residue points.

theorem CCDN.primitiveProjectiveReduction_zero {n p d : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial (Fin (n + 1)) ℤ) (hf : f.IsHomogeneous d) (z : IntPoint (n + 1)) (hz : Finset.univ.gcd z = 1) (hzf : (MvPolynomial.eval z) f = 0) : (MvPolynomial.eval (Projectivization.rep (primitiveProjectiveReduction z hz))) ((MvPolynomial.map (Int.castRingHom (ZMod p))) f) = 0

Homogeneous equations remain zero at the projective reduction.

theorem CCDN.projectiveResidueChartLift_zero {n p d : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial (Fin (n + 1)) ℤ) (hf : f.IsHomogeneous d) (r : ProjectiveResidueSpace n p) (hr : (MvPolynomial.eval (Projectivization.rep r)) ((MvPolynomial.map (Int.castRingHom (ZMod p))) f) = 0) : MvPolynomial.eval₂ (Int.castRingHom (ZMod p)) (fun (j : Fin n) => ↑(projectiveResidueChartLift r j)) ((affineChart n) ((MvPolynomial.rename ⇑(Equiv.swap 0 (projectiveResiduePivot r))) f)) = 0

The integer chart representative of a projective residue zero satisfies the reduced affine equation.