English
If P_y Q_z^3 = Q_y P_z^3 and an auxiliary equality hy' holds, then addMap(P,Q) is the vector [1,1,0] scaled by the doubled U-map: W.addMap ⟦P⟧ ⟦Q⟧ = ⟦W.dblU P · [1,1,0]⟧.
Русский
Если P_y Q_z^3 = Q_y P_z^3 и выполняется дополнительное равенство hy', то addMap(P,Q) равен массиву, полученному умножением удвоения U: W.addMap ⟦P⟧ ⟦Q⟧ = ⟦W.dblU P · [1,1,0]⟧.
LaTeX
$$W'.addMap ⟦P⟧ ⟦Q⟧ = ⟦W'.dblU P · \begin{bmatrix}1 \\ 1 \\ 0\end{bmatrix}⟧$$
Lean4
theorem addMap_of_Y_eq {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Equation Q) (hPz : P z ≠ 0) (hQz : Q z ≠ 0)
(hx : P x * Q z ^ 2 = Q x * P z ^ 2) (hy' : P y * Q z ^ 3 = W.negY Q * P z ^ 3) : W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![1, 1, 0]⟧ :=
by
by_cases hy : P y * Q z ^ 3 = Q y * P z ^ 3
· rw [addMap_eq, add_of_Y_eq hPz hQz hx hy hy', smul_eq _ <| isUnit_dblU_of_Y_eq hP hPz hQz hx hy hy']
· rw [addMap_eq, add_of_Y_ne hP.left hQ hPz hQz hx hy, smul_eq _ <| isUnit_addU_of_Y_ne hPz hQz hy]
