# mathlibdocumentation

algebraic_geometry.EllipticCurve

# 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.

## TODO #

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) :
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.

Equations
• a3 a4 a6 = (-432) * a6 ^ 2 + ((288 * a2 + 72 * a1 ^ 2) * a4 + ((-216) * a3 ^ 2 + ((144 * a1) * a2 + 36 * a1 ^ 3) * a3 + ((-64) * a2 ^ 3 - (48 * a1 ^ 2) * a2 ^ 2 - (12 * a1 ^ 4) * a2 - a1 ^ 6))) * a6 + ((-64) * a4 ^ 3 + (((-96) * a1) * a3 + (16 * a2 ^ 2 + (8 * a1 ^ 2) * a2 + a1 ^ 4)) * a4 ^ 2 + ((72 * a2 - 30 * a1 ^ 2) * a3 ^ 2 + ((16 * a1) * a2 ^ 2 + (8 * a1 ^ 3) * a2 + a1 ^ 5) * a3) * a4 + ((-27) * a3 ^ 4 + ((36 * a1) * a2 + a1 ^ 3) * a3 ^ 3 + ((-16) * a2 ^ 3 - (8 * a1 ^ 2) * a2 ^ 2 - (a1 ^ 4) * a2) * a3 ^ 2))
structure EllipticCurve (R : Type u_1) [comm_ring R] :
Type u_1
• a1 : R
• a2 : R
• a3 : R
• a4 : R
• a6 : R
• disc_unit :
• disc_unit_eq : (self.disc_unit) = self.a2 self.a3 self.a4 self.a6

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).

@[instance]
Equations
def EllipticCurve.disc {R : Type u_1} [comm_ring R] (E : EllipticCurve R) :
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.

Equations
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) :
R

The j-invariant of an elliptic curve.

Equations