Projective residue points determine unit charts and integral lifts in arbitrary dimension. Their reduced affine equations vanish at those lifts.

@[reducible, inline]

noncomputable abbrev CCDN.hypersurfaceResiduePivot {n p : ℕ} [Fact (Nat.Prime p)] (r : ProjectiveResidueSpace (n + 2) p) : Fin (n + 3)

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

Equations

• CCDN.hypersurfaceResiduePivot r = CCDN.projectiveResiduePivot r

theorem CCDN.hypersurfaceResiduePivot_ne_zero {n p : ℕ} [Fact (Nat.Prime p)] (r : ProjectiveResidueSpace (n + 2) p) : Projectivization.rep r (hypersurfaceResiduePivot r) ≠ 0

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

@[reducible, inline]

noncomputable abbrev CCDN.hypersurfaceResidueChartLift {n p : ℕ} [Fact (Nat.Prime p)] (r : ProjectiveResidueSpace (n + 2) p) : Fin (n + 2) → ℤ

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

Equations

• CCDN.hypersurfaceResidueChartLift r = CCDN.projectiveResidueChartLift r

theorem CCDN.cast_hypersurfaceResidueChartLift {n p : ℕ} [Fact (Nat.Prime p)] (r : ProjectiveResidueSpace (n + 2) p) (j : Fin (n + 2)) : ↑(hypersurfaceResidueChartLift r j) = Projectivization.rep r ((Equiv.swap 0 (hypersurfaceResiduePivot r)) j.succ) / Projectivization.rep r (hypersurfaceResiduePivot r)

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

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

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

theorem CCDN.hypersurfaceResidueChartLift_zero {n p d : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial (Fin (n + 3)) ℤ) (hf : f.IsHomogeneous d) (r : ProjectiveResidueSpace (n + 2) 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 + 2)) => ↑(hypersurfaceResidueChartLift r j)) (projectiveHypersurfaceChart (hypersurfaceResiduePivot r) f) = 0

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