English
There exists an addition-preserving equivalence between points of the Jacobian and affine points that is compatible with addition.
Русский
Существует эквиваленция между точками Якобиана и аффинными точками, сохраняющая сложение и совместимая с операцией сложения.
LaTeX
$$$W.Point \\cong_{+} W.toAffine.Point$$$
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_X_of_Z_eq_zero hP hPz).pow 2, toAffine_zero,
toAffine_of_Z_eq_zero hQz]
· rw [add_of_Z_eq_zero_left hP.left hPz hQz, toAffine_smul _ <| (isUnit_X_of_Z_eq_zero hP hPz).mul <| Ne.isUnit hQz]
· by_cases hQz : Q z = 0
·
rw [add_of_Z_eq_zero_right hQ.left hPz hQz,
toAffine_smul _ ((isUnit_X_of_Z_eq_zero hQ hQz).mul <| Ne.isUnit hPz).neg, toAffine_of_Z_eq_zero hQz, add_zero]
· by_cases hxy : P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3
· 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 ^ 3 = Q y * P z ^ 3
·
rw [add_of_Y_eq 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 ^ 2 = Q x * P z ^ 2
·
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 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 hx]
