English
Let W be a Weierstrass curve and P,Q be nonsingular projective points on W. Then the affine image of their sum equals the sum of their affine images: toAffine(W, W.add P Q) = toAffine(W, P) + toAffine(W, Q).
Русский
Пусть W — кривая Вейерштрасса, P,Q — ненонсигуральные проектные точки на W. Тогда аффинное изображение их суммы равно сумме их аффинных изображений: toAffine(W, W.add P Q) = toAffine(W, P) + toAffine(W, Q).
LaTeX
$$$\\operatorname{toAffine}(W, W.add(P,Q)) = \\operatorname{toAffine}(W,P) + \\operatorname{toAffine}(W,Q)$$$
Lean4
theorem toAffine_add [DecidableEq F] {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q) :
toAffine W (W.add P Q) = toAffine W P + toAffine W Q :=
by
by_cases hPz : P z = 0
· rw [toAffine_of_Z_eq_zero hPz, zero_add]
by_cases hQz : Q z = 0
·
rw [add_of_Z_eq_zero hP hQ hPz hQz, toAffine_smul _ <| (isUnit_Y_of_Z_eq_zero hP hPz).pow 4, toAffine_zero,
toAffine_of_Z_eq_zero hQz]
·
rw [add_of_Z_eq_zero_left hP.left hPz hQz,
toAffine_smul _ <| ((isUnit_Y_of_Z_eq_zero hP hPz).pow 2).mul <| Ne.isUnit hQz]
· by_cases hQz : Q z = 0
·
rw [add_of_Z_eq_zero_right hQ.left hPz hQz,
toAffine_smul _ (((isUnit_Y_of_Z_eq_zero hQ hQz).pow 2).mul <| Ne.isUnit hPz).neg, toAffine_of_Z_eq_zero hQz,
add_zero]
· by_cases hxy : P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z
· rw [toAffine_of_Z_ne_zero hP hPz, toAffine_of_Z_ne_zero hQ hQz,
Affine.Point.add_of_Y_eq ((X_eq_iff hPz hQz).mp hxy.left) ((Y_eq_iff' hPz hQz).mp hxy.right)]
by_cases hy : P y * Q z = Q y * P z
·
rw [add_of_Y_eq hP.left hPz hQz hxy.left hy hxy.right,
toAffine_smul _ <| isUnit_dblU_of_Y_eq hP hPz hQz hxy.left hy hxy.right, toAffine_zero]
·
rw [add_of_Y_ne hP.left hQ.left hPz hQz hxy.left hy, toAffine_smul _ <| isUnit_addU_of_Y_ne hPz hQz hy,
toAffine_zero]
· have := toAffine_add_of_Z_ne_zero hP hQ hPz hQz hxy
by_cases hx : P x * Q z = Q x * P z
·
rwa [add_of_Y_ne' hP.left hQ.left hPz hQz hx <| not_and.mp hxy hx,
toAffine_smul _ <| isUnit_dblZ_of_Y_ne' hP.left hQ.left hPz hQz hx <| not_and.mp hxy hx]
· rwa [add_of_X_ne hP.left hQ.left hPz hQz hx, toAffine_smul _ <| isUnit_addZ_of_X_ne hP.left hQ.left hx]
