I'm formalizing this paper in a proof assistant. On page 14, you can find a proof of a property called dichotomy. It is useful to stablish the group law for this curves. However, I'm not understanding the argument used:
Here if I assumed that $p \equiv 0 \mod S$ is equivalent to $p = 0$ it would be easy to deduce $(a_0,b_0) = \pm (b_1,a_1)$ since the first equality is saying $a_0 = \pm b_1, a_1 = \pm b_0$ and the last equality is saying that this two equalities have the same sign.
However, it is obvious that $p \equiv 0 \mod S$ is not equivalent to $p = 0$. I have several questions:
- Why does the author choose the ideal generated by $e_1,e_2,\delta',\ldots$. How does the reduction modulo $S$ justify the last equality?
- What is the role of $q$ in the polynomial $qx_0x_1y_0y_1 - 1$? It is not specified in the paper nor in the Mathematica computations.
Edit
Some progress:
Note that $e_1,e_2,\delta',\delta_{\pm}$ are zero. If the last one was zero also there should be no problem in establishing the property.
The coordinate ring of $E^\circ$ is the coordinate ring S of $E_{aff}$ with x and y inverted, which is S[q]/(q x y - 1), where q is a fresh variable. (In other words, q is the inverse of x*y.)
