feat(EllipticCurve): ZSMul formula in terms of division polynomials

[alreadydone]

The formula $[n]P = (\phi_n(x,y) : \omega_n(x,y) : \psi_n(x,y))$ in Jacobian coordinates for $P=(x,y)$ a nonsingular point on a Weierstrass/elliptic curve.

---

• depends on: [Merged by Bors] - feat(EllipticCurve): a coordinate ring over a domain is a domain #12883
• depends on: [Merged by Bors] - feat(AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic): add maps for division polynomials #13399
• depends on: feat(NumberTheory): characterize elliptic divisibility sequences #13057
• depends on: feat(NumberTheory/EllipticDivisibilitySequence): show elliptic relations follow from even-odd recursion #13155
• depends on: [Merged by Bors] - feat(EllipticCurve): affine formulas and bivariate polynomial lemmas #13845
• depends on: [Merged by Bors] - feat(EllipticCurve): lemmas in Jacobian coordinates #13846
• depends on: feat(EllipticCurve): the universal elliptic curve #13847

[Multramate]

Is suppress_compilation just the same as tagging noncomputable?

Anyways, I'm wondering if it's possible to extract a version of ω that very close to being a univariate polynomial, i.e. Ω for ω analogous to Ψ for ψ, where Ω is some univariate polynomial times a constant (2?) multiple of ψ. This way the ZSmul formula can be expressed in affine coordinates as n • (x, y) = (f(x), g(x) * h(x, y)) for some univariate rational functions f and g and some bivariate polynomial h, mirroring Sutherland's statement in Lemma 5.21. When a₁ and a₃ are zero, then there should be a way to define Ω so that h(x, y) is just y.

[alreadydone]

I'll see what I can do with ω.

Lean is sometimes slow to compile something computable or fails to compile due to incomplete support. Verifying computability seems to always be fast though, so there should never be a need to mark a computable def noncomputable. To deal with slow compilation people have invented suppress_compilation and that's what we should use instead.

[alreadydone]

I'm not yet sure what could be done for ω; the best idea I have is to take the expression
$$\omega_n=\frac{\psi_{n+1}\psi_n\psi_{n-1}}{\psi_3}(a_1 F_Y-F_X)-\frac{\psi_{n-2}\psi_{n+1}^2}{\psi_2}+(Y-F_Y)\psi_n^3$$
(first posted on Zulip, here I removed the multiple of polynomial) and try to analyze the even n and odd n cases separately. You can always write it as p(X)+Yq(X) in a unique way and maybe you will be able to compute the degrees of p(X) and q(X).

An inadvertent discovery: when I tried to derive negDblY from $$\omega_2$$, I arrived at the very simple expression ψ₃ polynomialX + Y polynomialY^3. Comparing this with what we have in mathlib we arrive at the identity ψ₃ + polynomialX^2 - a1 polynomialX polynomialY - (3x + a2) polynomialY^2 + (12 x + b2) polynomial = 0. In my notes I've explained that dblX can be taken to be X polynomialY^2 - ψh₃ where ψh₃ is the weighted homogenization of ψ₃. This new discovery shows that negDblY can be taken to be Y polynomialY^3 + ψh₃ polynomialX which is of a similar form. TODO: use this to simplify the expressions here.

[Multramate]

Thanks for the identities. I guess we'd have to either redefine ψh₃ recursively, or get the homogenisation API working and apply it to the existing ψ₃. It's probably not too urgent now but we should do it eventually.

The reason I'm asking for Ω is because I need Sutherland's argument for Theorem 5.8 to finish the computation for |E[n]| = n^2. We can translate that theorem into division polynomial language, and he essentially relates |E[n]| to the number of roots of ψ² (as a univariate polynomial), by showing that the fibers (x₀, y₀) of multiplication by n (after shifting 0 to a suitable point (a, b)) are uniquely determined by x₀, and we can show this easily if we have an expression for ω directly in terms of y. The same argument happens to also work to show that multiplication by n is surjective (the "standard" proof to this is a non-trivial fact about morphisms of curves).

[alreadydone]

I don't think there's a need to define the whole family ψh recursively (which I think is what you mean); in any case ψh₃ will be one of the base cases, so it either needs to be directly written down, or obtained from ψ₃ via homogenization API.
I'll read Sutherland to understand what is really needed.