English
Let W' be a projective Weierstrass curve over a field F and let P = (P x, P y, P z) be a projective point represented in homogeneous coordinates with P z ≠ 0. Then evaluating the homogeneous polynomial W at P and dividing by P z^3 gives exactly the affine Weierstrass polynomial evaluated at the affine coordinates (P x / P z, P y / P z). In other words, the projective equation reduces to the affine equation on the chart Z ≠ 0.
Русский
Пусть W' — проективная кривая Вейерштрасса над полем F и пусть P = (P x, P y, P z) задаёт точку в однородных координатах с P z ≠ 0. Тогда значение однородного многочлена W в точке P, делённое на P z^3, совпадает с аффинным многочленом W, оцениваемым в аффинных координатах (P x / P z, P y / P z). Другими словами, уравнение в проективных координатах сводится к аффинному уравнению на область Z ≠ 0.
LaTeX
$$$\\dfrac{\\mathrm{eval} \\, P \\, W'.polynomial}{P z^{3}} = W'.toAffine.polynomial.evalEval \\left( \\dfrac{P x}{P z}, \\dfrac{P y}{P z} \\right)$$$
Lean4
theorem eval_polynomial_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) :
eval P W.polynomial / P z ^ 3 = W.toAffine.polynomial.evalEval (P x / P z) (P y / P z) := by
linear_combination (norm := (rw [eval_polynomial, Affine.evalEval_polynomial]; ring1))
P y ^ 2 / P z ^ 2 * div_self hPz + W.a₁ * P x * P y / P z ^ 2 * div_self hPz +
W.a₃ * P y / P z * div_self (pow_ne_zero 2 hPz) -
W.a₂ * P x ^ 2 / P z ^ 2 * div_self hPz -
W.a₄ * P x / P z * div_self (pow_ne_zero 2 hPz) -
W.a₆ * div_self (pow_ne_zero 3 hPz)
