Elliptic curve as group scheme: a blueprint

Stream: maths

[Junyan Xu]

Let R be a commutative ring and let W be a WeierstrassCurve over R. Let F denote the associated homogeneous Weierstrass polynomial, so $W=\operatorname{Proj} R[X,Y,Z]/\langle F\rangle$. Let W⁰ denote the R-smooth locus in W, i.e. W⁰ is the union of the three basic opens associated to the three partial derivatives $F_X, F_Y$ and $F_Z$. We aim to show that there is a group R-scheme structure on W⁰ that gives rise to the familiar group law WeierstrassCurve.Projective.Point.add on W⁰(K) when K is an R-algebra that is a field. Moreover, there is a group scheme action of W⁰ on W that "fixes the singular point (if exists)". This is basically a generalization of Theorem IV.5.3c in Silverman's 2nd volume as discussed before. To construct the addition/AddAction morphism, the proof given there splits the domain $W^0\times W$ into 2x2=4 affine charts and the codomain $W$ into 2, which is quite cumbersome, especially to show agreement on intersections to glue up the 4x2=8 morphisms. (We consider W⁰ and W as objects in the category of schemes over R, so $W^0\times W$ denotes the fibered product over R.)

More recent discussions on Zulip led to a paper [BL] of Bosma--Lenstra giving two addition formulas in projective coordinates that are complete, and I've since realized that they are all that are needed to construct the morphism. Briefly, [BL] gives six polynomials $X^{(1)},Y^{(1)},Z^{(1)},X^{(2)},Y^{(2)},Z^{(2)}$ (subscript 3 omitted here) in six variables $X_1,Y_1,Z_1,X_2,Y_2,Z_2$ that are bi-homogeneous of bi-degree (2,2) which can be verified to satisfy the cross identity $X^{(1)}Y^{(2)}=X^{(2)}Y^{(1)}$ modulo $F(X_1,Y_1,Z_1)$ and $F(X_2,Y_2,Z_2)$, and similarly for $XZ$ and $YZ$. In mathlib, we already verified that WeierstrassCurve.Projective.addXYZ, which is exactly $(X^{(1)},Y^{(1)},Z^{(1)})$, defines the familiar group law, so by the identities so does $(X^{(2)},Y^{(2)},Z^{(2)})$.

Any such three polynomials give rise to a morphism from the union of the corresponding three basic opens in $W\times W$ to $W$. However, mathlib doesn't currently have a mechanism to define morphisms between (subschemes of fiber products of) Proj schemes like Hartshorne Exercise II.2.14. Further complicating the matter is that $W\times W$ is a multi-graded Proj scheme (formalized by Arnaud Mayeux and Jujian Zhang but isn't in mathlib), and the polynomials define a graded homomorphism of rings graded by different monoids (the "functoriality of Proj" stated in their paper doesn't treat this generality).

Last week, it came to my realization that the viewpoint of functors of points can serve as a general way of constructing such morphisms. In previous discussions with @David Ang, we considered generalizing the current definition of (projective) A-points of W, to $W_{\text{pre}}(A)=\{(x,y,z)\in A^3 \mid F(x,y,z)=0, \langle x,y,z\rangle = A\}/A^\times$ (where Aˣ acts by coordinate-wise multiplication), and take $W^0_{\text{pre}}(A)$ to be the subset of Rˣ-orbits satisfying $\langle F_X(x,y,z), F_Y(x,y,z), F_Z(x,y,z) \rangle=A$. These definitions don't actually capture all A-points of W or W⁰ if Pic(A) is nontrivial, but they still define a functor from the category of commutative R-algebras A to Type, and can be extended to a presheaf on the big Zariski site of R-schemes by composing with the global sections functor. The sheafification of these presheaves are exactly the functors of points (over R), because they agree on stalks, since local rings do have trivial Picard group.

To define the morphism $W^0\times W\to W$, it would suffice to define a natural transformation $W^0_{\text{pre}}(A)\times W_{\text{pre}}(A)\to W_{\text{pre}}(A)$ for R-algebras A, which induces a sheaf morphism between the sheafifications $(W^0\times W)(X)\to W(X)$ for R-schemes X, and the desired morphism is obtained by fullness of Yoneda embedding. Unfortunately this doesn't quite work; what is true is that there are natural transformations $W^{(i)}(A)\to W_{\text{pre}}(A)$ for $i=1,2$ that agree on their intersection, where $W^{(i)}(A)=\{(P_1, P_2)\in A^3\times A^3 \mid \langle X^{(i)}(P_1,P_2), Y^{(i)}(P_1,P_2), Z^{(i)}(P_1,P_2)\rangle = A \}$, and an inclusion $W^0_{\text{pre}}(A)\times W_{\text{pre}}(A)\subseteq W^{(1)}(A)\cup W^{(2)}(A)$ for A local, which induces $W^0\times W\to (W^{(1)}\cup W^{(2)})^+$ between the sheafifications.

[Junyan Xu]

Now let me go into some details and list some subgoals; I'll probably start working on these in March. If anyone is interested in collaboration please let me know.

I. Elementary facts about commutative (semi)rings

1. If $x_1,y_1,x_2,y_2\in R$ satisfies $\langle x_i,y_i\rangle=R$ for $i=1,2$, then $(x_1,y_1)$ and $(x_2,y_2)$ are in the same Rˣ-orbit iff $x_1 y_2=x_2 y_1$. Specifically if $ax_1+by_1=1$ we have $(x_2,y_2)=(ax_2+by_2)(x_1,y_1)$, and then since $x_2$ and $y_2$ generate the unit ideal, $ax_2+by_2$ must be a unit. This easily extends from $R^2$ to arbitrary $R^n$ (corresponding to $\mathbb{P}^{n-1}$).
2. As a corallary, $W_{\text{pre}}$ is a separated presheaf: if $(x_1,y_1,z_1)$ and $(x_2,y_2,z_2)$ are in the same Rᵢˣ-orbit for each i, such that the Rᵢ form a Zariski cover of R, then $x_1 y_2=x_2 y_1, x_1 z_2=x_2 z_1$ and $y_1 z_2=y_2 z_1$ in every Rᵢ, implying the same are true in R, which in turn implies that the two triples are in the same Rˣ-orbit.

II. Functor of points of subschemes of projective spaces

1. Define the presheaf $W_{\text{pre}}$ and its subpresheaf $W^0_{\text{pre}}$, first for R-algebras and then for all R-schemes; one may also consider defining both as subpresheaves of some $\mathbb{P}^3_{\text{pre}}$.
   We probably want to rename the current (Affine/Projective/Jacobian).Point (which is currently W⁰) to NonsingularPoint or Pointₙₛ and give the original name to W. Equation should probably be unbunbled from Nonsingular(Lift).

2. Show that functors of points, in particular $W$ and $W^0$, are sheaves on the big Zariski site: this is basically saying one can glue scheme morphisms, which is already in mathlib.

3. Construct the natural transformation $W_{\text{pre}}\to W$, which involves constructing morphisms $X\to\mathbb{P}^n_R$ from a tuple $(f_1,\dots,f_{n+1})$ that generates the unit ideal in $\Gamma(\mathcal{O}_X)$. This can be achieved by glueing $D(f_i)\to\mathbb{A}_R^n$ corresponding to $(f_1/f_i,\dots,\widehat{f_i/f_i},\dots,f_{n+1}/f_i)$.
4. Show $W_{\text{pre}}$ preserves directed colimits, so its stalks are just evaluations at local rings.
5. Show $W_{\text{pre}}(A)\to W(A)$ is bijective for A local (use AlgebraicGeometry.SpecToEquivOfLocalRing), and deduce that $W_{\text{pre}}\to W$ is sheafification. Consequently, $W_{\text{pre}}(X)\to W(X)$ is injective for all X by I.2.

III. Projective formulas (@David Ang and me are most familiar with this part):

1. Define the three polynomials $X^{(2)},Y^{(2)},Z^{(2)}$ not yet in mathlib. Notice that one of the terms in each of $X^{(2)}$ and $Y^{(2)}$ in [BL] are wrong. Show the the cross identities $X^{(1)}Y^{(2)}=X^{(2)}Y^{(1)}$ etc. module F (for which I've obtained explicit coefficients).
2. Define the natural transformation $W^{(1)}\cup W^{(2)}\to W$: we should probably generalize WeierstrassCurve.Projective.add for this. Instead of splitting byP ≈ Q and using dblXYZ, we should use addXYZ whenever $X^{(1)},Y^{(1)},Z^{(1)}$ generate the unit ideal and $X^{(2)},Y^{(2)},Z^{(2)}$ otherwise. When both triples generate the unit ideal, the results agree by I.1.

3. The condition that $X^{(1)},Y^{(1)},Z^{(1)}$ evaluated at $P_1=(x_1,y_1,z_1)$ and $P_2=(x_2,y_2,z_2)$ generate the unit ideal is equivalent to that $x_1 y_2-x_2 y_1, x_1 z_2-x_2 z_1, y_1 z_2-y_2 z_1$ generate the unit ideal, so geometrically $W^{(1)}$ is exactly the complement of the diagonal in $W\times W$. One direction is easy since one can check directly that $X^{(1)},Y^{(1)},Z^{(1)}$ are linear combinations of $X_1 Y_2-X_2 Y_1$ etc.: in fact $[-1](X^{(1)},Y^{(1)},Z^{(1)})=\nabla_{P_2}F(P_1)P_2-\nabla_{P_1}F(P_2)P_1$ which is obviously antisymmetric in $P_1$ and $P_2$. (This formula actually work for any cubic hypersurface, while $X^{(2)}$ etc. are more specific to plane cubic in Weierstrass form.)
   It suffices to show the other direction in a field K, since if an ideal is not the unit ideal then it is contained in some maximal ideal, and in the residue field the ideal becomes zero (not the unit ideal) so all generators become zero. $\nabla_{P_2}F(P_1)P_2=\nabla_{P_1}F(P_2)P_1$ implies that either $P_1$ and $P_2$ are proportional (therefore $x_1 y_2=x_2 y_1$ etc.), or they are not and $\nabla_{P_1}(P_2)=\nabla_{P_2}(P_1)=0$. But that implies $F(sP_1+tP_2)=s^3 F(P_1)+s^2 t \nabla_{P_2}F(P_1) + st^2 \nabla_{P_1}F(P_2) + t^3 F(P_2)=0$ for arbitrary s,t, so F vanishes on some two dimensional subspace of $K^3$, and therefore has the equation of this subspace as a linear factor, contradicting its irreducibility. It's necessary to take s,t in the algebraic closure to make this argument work. Or we may divide F by the linear factor $(y_1 z_2-y_2 z_1)X+(z_1 x_2-z_2 x_1)Y+(x_1 y_2-x_2 y_1)X$ to find the other factor. We need to deduce irreducibility of F from WeierstrassCurve.Affine.irreducible_polynomial (Lemma 2 in #maths > thoughts on elliptic curves @ 💬 ).

4. We still need to show $W^0(A)\times W(A)\subseteq W^{(1)}(A)\cup W^{(2)}(A)$ for A local. In a local ring, a set generates the unit ideal iff at least one element of it is a unit, or equivalently, is nonzero in the residue field. So we may again assume A is a field. For $(P,Q)\in W^0(A)\times W(A)$, if P≠Q we already showed $(P,Q)\in W^{(1)}(A)$. Otherwise, $P=Q\in W^0(A)$, and we can check that $XYZ^{(2)}$ reduces to WeierstrassCurve.Projective.dblXYZ modulo F(P), and from the proof of WeierstrassCurve.Projective.nonsingular_add we should be able to extract the fact that $XYZ^{(2)}$ don't all vanish.

IV. Group scheme axioms
We need to show the addition/AddAction morphism $W^0\times W\to W$ together with the negation $W\to W$ and identity $\operatorname{Spec}R\to W$ satisfy the commutative diagrams in group scheme axioms. The hardest one is of course associativity, which amounts to showing two morphisms $W^0\times W^0\times W \to W$ agree. By faithfulness of Yoneda we just need to check the induced natural transformation between functors of points agree, which can be checked on the level of stalks (local rings), but we only have associativity for field-valued points in mathlib. My current idea is to prove 2x2x3=12 universal cross identities of polynomials in 9 variables $x_i,y_i,z_i$ for i=1,2,3 over the polynomial ring $U=\mathbb{Z}[a_1,a_2,a_3,a_4,a_6]$ by considering the field of fractions of U, which can then be specialized to an arbitrary ring. (In fact to show the image of $W^0\times W\to\mathbb{P}^2$ is contained in $W$ we probably already need some universal identities.)

V. Reduction homomorphisms
If R is a valuation ring, denote by K its field of fractions and k its residue field. Applying the functor $W^0\times W\to W$ to the quotient map $R\to k$, we obtain a group homomorphism $W^0(R)\to W^0(k)$. Since R is a domain, $W^0(R)\to W^0(K)$ is injective and we may regard $W^0(R)$ as a subgroup of $W^0(K)$. Since W is proper we always have $W(R)=W(K)$, and if W has nonzero discriminant then $W(K)=W^0(K)$, so we get a reduction homomorphism from a subgroup of $W(K)$ to $W^0(k)$; if moreover W has good reduction (discriminant is a unit), then $W=W^0$ and we get a homomorphism $W(K)\to W(k)$.
This has been a major motivation for constructing the group scheme, but with the current approach it can be obtained from just a few ingredients towards the full construction (I.1, II.1 and III.1-2): since every ring involved is local, we may as well replace W by $W_{\text{pre}}$, and the claims can be verified elementarily without mentioning schemes or sheafification. In fact $W_{\text{pre}}(R)=W_{\text{pre}}(K)$ can be easily verified for Bézout domains R, but if R is not local then two formulas are not enough to define addition and you also need linear combinations of them, so for convenience we should consider only local Bézout domains, which are exactly valuation rings (stacks#090Q).

[Andrew Yang]

Might be stupid suggestion: Can you just define it on one chart and extend by valuative criterion + properness of Proj?

Edit: no the domain is $W \times W$ which is not a curve so the stalks aren't necessarily DVRs.

[Junyan Xu]

Yeah, in general if you have a rational map from a smooth curve over a field to a proper scheme it can be extended to a morphism, but in higher dimension the domain of definition can be a proper open subset. Here R also adds more dimension, and W is not smooth everywhere. If R is a field it's easy to see the domain of definition is exactly $W^0\times W \cup W \times W^0$, but I don't know an abstract argument to derive the result for arbitrary R from this.

[Andrew Yang]

But how bad is gluing actually? Gluing 8 morphisms is just checking 8 rational function identities right? And to check the group axioms you only need to check on one affine cover (by separated-ness)

[Ravi Vakil]

You can do an abstract argument, but cheapest (not the most elegant) is just to define it chart by chart, and as @Andrew Yang says, check by gluing. And if you can invoke separatedness to save time, but since I suspect you are working over an arbitrary base, I might suspect that it will be easier to just do it on all charts. Define the morphisms; then check that they have the properties of a group scheme over the base.

[Junyan Xu]

But how bad is gluing actually?

As discussed before, there are a total of 7 cases; 2 are just swapping factors, and 1 case is in mathlib, so we count 5. Each case has two coordinates, so we need to introduce 10 new formulas; for each case we also need to verify certain elements in certain tensor product of localizations generate the unit ideal. In contrast the new approach only introduce 3 new formulas $X^{(2)},Y^{(2)},Z^{(2)}$, and in fact $Z^{(2)}$ is just $Y^{(1)}$ up to negation. Working with polynomials directly should be more pleasant than working with tensor products of localizations of quotients of polynomial rings.

Gluing 8 morphisms is just checking 8 rational function identities right? And to check the group axioms you only need to check on one affine cover (by separated-ness)

That's correct (except for the count): in the universal case ($R=\mathbb{Z}[a_i]$) it's shouldn't be hard to prove the scheme is integral, since we have WeierstrassCurve.Affine.CoordinateRing.instIsDomain and we can similarly prove the coordinate ring at infinity is also a domain. I remarked before that we need 7-1=6 intersections to form a tree connecting all the cases, and each case requires 2 identities, for a total of 12. They can be reduced to checking polynomial identities modulo Weierstrass polynomial, but these identities are dissimilar to each other and you need to treat them case by case. In the new approach we need 2x2x3=12 identities to check associativity but they can be treated uniformly, and requires no computation. We just show associativity in the universal case implies certain cross products of compositions of polynomials are equal, and specialize it to deduce associativity for R-points.

You can do an abstract argument, but cheapest (not the most elegant) is just to define it chart by chart, and as @Andrew Yang says, check by gluing.

I do think the the new approach is the shortest path; I'm not really concerned with elegance, but I'm in favor of using abstract mechanisms to get rid of a lot formulas that are not useful for other purposes. It's also nice that the new approach produces reduction homomorphisms as an intermediate result.

[Scott Carnahan]

I haven’t looked at the Neron Models (Bosch Lutkebohmert Raynaud? sorry on a phone) book in a while, but I think they had written down some theory of rationally defined group laws and actions that may be useful here.

[Junyan Xu]

The Theorem IV.5.3c I'm proving with this new approach is exactly from Silverman's chapter on Néron model, and he does cite BLR, so he must be well aware if simplifications are possible using materials in BLR. Yet the only alternative approach to 5.3c (in the case of good reduction) he gave uses the full force of existence of existence of Néron models ($\mathcal{E}/R$ is a group scheme by definition of Néron models):
image.png
image.png

But the existence of Néron models for Dedekind domains actually depends on 5.3 (it's crucial that "these group laws are given by the same equations, so they fit together"); isn't this circular? ("bad reduction" should be "good reduction" here)
image.png
image.png

Fortunately no, since Silverman's 5.3 is only stated for DVRs, and for DVRs the existence reduces to the case of strict Henselian rings, known from 6.7 and 6.10 which do not use 5.3 (notice that 6.10 proves the group law extends for strict Henselian DVRs):
image.png
image.png

To give an proof of 5.3c using this, one still needs to show that the Weierstrass equation defines a minimal proper regular model. This is the case in the good reduction case and a few other cases; for other Weierstrass equations you need to run Tate's algorithm and blow up the singular point to get the minimal model, so you no longer stay in $\mathbb{P}^2_R$.
image.png

I think the argument in the good reduction case is that the special fiber is an elliptic curve, so contains no exceptional divisor (which is rational), so by Remark 7.5.1 it's minimal (7.5 is Castelnuovo's criterion):
image.png

So overall this alternative argument is fairly complicated, requiring a lot of prerequisites, and only proves something less general. I think Silverman is proposing it as an alternative only because he consider the approach of glueing morphisms on affine charts to be also fairly complicated (notice that 3 of 4 cases are relegated to Exercise 4.22), which reaffirms the advantage of my new approach presented above.

[David Ang]

What are we planning to do with the "tuples/triples quotient by action" API? I have an old PR that changes Fin 3 -> R to R x R x R for better definitional equality based on my experiments; what are we going to do about this?

We probably want to rename the current (Affine/Projective/Jacobian).Point (which is currently W⁰) to NonsingularPoint or Pointₙₛ and give the original name to W. Equation should probably be unbunbled from Nonsingular(Lift).

Good idea, I will change Point to NonsingularPoint and keep the original name free for now. The predicates should really be something like OnCurve (SatisfiesEquation?) and IsNonsingular, according to naming conventions?

1. Define the three polynomials $X^{(2)},Y^{(2)},Z^{(2)}$ not yet in mathlib. Notice that one of the terms in each of $X^{(2)}$ and $Y^{(2)}$ in [BL] are wrong. Show the the cross identities $X^{(1)}Y^{(2)}=X^{(2)}Y^{(1)}$ etc. module F (for which I've obtained explicit coefficients).

Do you have the corrected versions of $X_3^{(2)}$ etc somewhere? I can also change the $X_3^{(1)}$ (addX) etc to follow [BL] and then cite their paper (because currently it looks like I conjured the formulae out of thin air), or alternatively we could use the bilinear form description you have in the division polynomials paper (which still isn't public)? I guess we don't care about $X_3^{(3)}$ etc from their paper.

1. Define the natural transformation $W^{(1)}\cup W^{(2)}\to W$: we should probably generalize WeierstrassCurve.Projective.add for this. Instead of splitting byP ≈ Q and using dblXYZ, we should use addXYZ whenever $X^{(1)},Y^{(1)},Z^{(1)}$ generate the unit ideal and $X^{(2)},Y^{(2)},Z^{(2)}$ otherwise. When both triples generate the unit ideal, the results agree by I.1.

I can do this. Does this mean that the doubling formulae (dblX) etc should be removed?

[Junyan Xu]

What are we planning to do with the "tuples/triples quotient by action" API? I have an old PR that changes Fin 3 -> R to R x R x R for better definitional equality based on my experiments; what are we going to do about this?

I think I'd stick with Fin 3 -> R because it's easier to connect to MvPolynomial. Also note that WeierstrassCurve.Projective.PointClass can be changed to $\mathbb{P}^2_{\text{pre}}$, generalized to $\mathbb{P}^n_{\text{pre}}$, and move to another file about (points of) projective spaces.

Good idea, I will change Point to NonsingularPoint and keep the original name free for now. The predicates should really be something like OnCurve (SatisfiesEquation?) and IsNonsingular, according to naming conventions?

Thanks! I think W.polynomial.eval P = 0 is already short enough to write, so maybe we deprecate the Equation predicate if we can't think of a better name? I'm also fine with keeping it. On the other hand Nonsingular is an adjective and I heard that Is isn't required in this case?

Do you have the corrected versions of $X_3^{(2)}$ etc somewhere? I can also change the $X_3^{(1)}$ (addX) etc to follow [BL] and then cite their paper (because currently it looks like I conjured the formulae out of thin air), or alternatively we could use the bilinear form description you have in the division polynomials

We have $Z^{(2)}(P_1,P_2)=-Y^{(1)}([-1]P_1,P_2)$ and $X^{(2)},Y^{(2)}$ are in XY2.txt. The errors in [BL] are: $a_3 a_4(X_1 Z_2-2X_2 Z_1)X_2 Z_1$ in $X^{(2)}$ should be $-a_3 a_4(2X_1 Z_2+X_2 Z_1)X_2 Z_1$, and $-(3a_2 a_6-a_4^2)(X_1 Z_2+X_2 Z_1)(X_1 Z_2-X_2 Z_1)$ in $Y^{(2)}$ should be $(3 a_2 a_6 - a_4^2) (2 X_1 Z_2 + X_2 Z_1) X_2 Z_1$. I've obtained a more compact formula for $X^{(2)}([-1]P_1,P_2)$, given by

y1  y2 (x2  y1 - x1  y2) +
 a1 (x2^2 y1^2 - x1^2 y2^2) + (b2 - 3 a2) x1 x2 (x2 y1 - x1 y2) +
 a3 (x2 y1^2 z2 - x1 y2^2 z1) + (b4 - a4) (x2^2 y1 z1 - x1^2 y2 z2 +
    2 x1 x2 (y1 z2 - y2 z1)) + (b6 - a6) (x1 y1 z2^2 - x2 y2 z1^2 +
    2 z1 z2 (x2 y1 - x1 y2)) + b8 z1 z2 (y1 z2 - y2  z1)

I hope I can figure out a more conceptual formula for $XYZ^{(2)}$, or at least make $Y^{(2)}$ as compact as this.
For $XYZ^{(1)}$ I think I prefer the expression $\nabla_Q F(P)\cdot Q-\nabla_P F(Q)\cdot P$, where $\nabla_Q F(P)$ is Q x * W.polynomialX.eval P + Q y * W.polynomialY.eval P + Q z * W.polynomialZ.eval P and similarly for $\nabla_P F(Q)$. This formula allows you to define addXYZ directly and then addX/Y/Z as its coordinates.

I can do this. Does this mean that the doubling formulae (dblX) etc should be removed?

Thanks! I think dblX/Y/Z are still useful to connect to the affine formula, and we do want to focus on the diagonal after we showed the rational map is defined off diagonal by addXYZ. Though it's reasonable to redefine them as specializations of $XYZ^{(2)}$ to the case P=Q (whatever is convenient, I don't care a lot).

[Junyan Xu]

I opened draft PR #35151 to supply more details of the construction of the group scheme. I now think that the definition of PointClass needn't be changed, and I just renamed it to AlgebraicGeometry.ProjectiveSpace.PointClass, and defined two more predicates SpanEqTop and EquationLift on it; together with the existing NonsingularLift, they define subpresheaves (CategoryTheory.Subfunctor) whose sheafifications are functors of points (Yoneda) of $\mathbb{P}^2$, $W$ and $W^0$. I also defined point and nonsingularPoint as sets in PointClass, and I think the structure Point should no longer be needed.

[David Ang]

Seems like we'd have to call it W.NonsingularPoint even if W.IsElliptic? Maybe W.Pointₙₛ might be a little less invasive (but still there)