English
Let P be a nonsingular lift and Q be a nonsingular point with z-coordinate zero (the point at infinity) on the Weierstrass projective curve W. Then P + Q = P; i.e., adding the point at infinity leaves P unchanged.
Русский
Пусть P — ненулькачественный подстановок и Q — ненулевая точка на кривой Ваерештрасса с нулём в последней однородной координате (точка на бесконечности) на проективной кривой W. Тогда P + Q = P; то есть сумма с бесконечностью не изменяет P.
LaTeX
$$$ (W.NonsingularLift P) \land (W.Nonsingular Q) \land (Q_z = 0) \Rightarrow W.addMap P \langle Q \rangle = P $$$
Lean4
theorem addMap_of_Z_eq_zero_right {P : PointClass F} {Q : Fin 3 → F} (hP : W.NonsingularLift P) (hQ : W.Nonsingular Q)
(hQz : Q z = 0) : W.addMap P ⟦Q⟧ = P := by
revert hP
refine P.inductionOn (motive := fun P => _ → W.addMap P _ = P) fun P hP => ?_
by_cases hPz : P z = 0
· rw [addMap_eq, add_of_Z_eq_zero hP hQ hPz hQz, smul_eq _ <| (isUnit_Y_of_Z_eq_zero hP hPz).pow 4, Quotient.eq]
exact Setoid.symm <| equiv_zero_of_Z_eq_zero hP hPz
·
rw [addMap_eq, add_of_Z_eq_zero_right hQ.left hPz hQz,
smul_eq _ (((isUnit_Y_of_Z_eq_zero hQ hQz).pow 2).mul <| Ne.isUnit hPz).neg]
