mathlib documentation


The category of elliptic curves (over a field or a PID) #

We give a working definition of elliptic curves which is mathematically accurate in many cases, and also good for computation.

Mathematical background #

Let S be a scheme. The actual category of elliptic curves over S is a large category, whose objects are schemes E equipped with a map E → S, a section S → E, and some axioms (the map is smooth and proper and the fibres are geometrically connected group varieties of dimension 1). In the special case where S is Spec R for some commutative ring R whose Picard group is trivial (this includes all fields, all principal ideal domains, and many other commutative rings) then it can be shown (using rather a lot of algebro-geometric machinery) that every elliptic curve is, up to isomorphism, a projective plane cubic defined by the equation y^2+a₁xy+a₃y=x^3+a₂x^2+a₄x+a₆, with aᵢ : R, and such that the discriminant of the aᵢ is a unit in R.

Some more details of the construction can be found on pages 66-69 of N. Katz and B. Mazur, Arithmetic moduli of elliptic curves or pages 53-56 of P. Deligne, Courbes elliptiques: formulaire d'après J. Tate.

Warning #

The definition in this file makes sense for all commutative rings R, but it only gives a type which can be beefed up to a category which is equivalent to the category of elliptic curves over Spec R in the case that R has trivial Picard group or, slightly more generally, when the 12-torsion of Pic(R) is trivial. The issue is that for a general ring R, there might be elliptic curves over Spec(R) in the sense of algebraic geometry which are not globally defined by a cubic equation valid over the entire base.


Define the R-points (or even A-points if A is an R-algebra). Care will be needed at infinity if R is not a field. Define the group law on the R-points. (hard) prove associativity.

def EllipticCurve.disc_aux {R : Type u_1} [comm_ring R] (a1 a2 a3 a4 a6 : R) :

The discriminant of the plane cubic Y^2+a1*X*Y+a3*Y=X^3+a2*X^2+a4*X+a6. If R is a field then this polynomial vanishes iff the cubic curve cut out by this equation is singular.

structure EllipticCurve (R : Type u_1) [comm_ring R] :
Type u_1

The category of elliptic curves over R (note that this definition is only mathematically correct for certain rings, for example if R is a field or a PID).

Instances for EllipticCurve
@[protected, instance]
def EllipticCurve.disc {R : Type u_1} [comm_ring R] (E : EllipticCurve R) :

The discriminant of an elliptic curve. Sometimes only defined up to sign in the literature; we choose the sign used by the LMFDB. See the LMFDB page on discriminants for more discussion.

theorem EllipticCurve.disc_is_unit {R : Type u_1} [comm_ring R] (E : EllipticCurve R) :
def EllipticCurve.j {R : Type u_1} [comm_ring R] (E : EllipticCurve R) :

The j-invariant of an elliptic curve.