mathlib documentation

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 one). 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² + a₁xy + a₃y = x³ + a₂x² + 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 Pic R or, slightly more generally, when its 12-torsion 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. Prove associativity (hard).

@[simp]
def EllipticCurve.Δ_aux {R : Type u} [comm_ring R] (a₁ a₂ a₃ a₄ a₆ : R) :
R

The discriminant of an elliptic curve given by the long Weierstrass equation y² + a₁xy + a₃y = x³ + a₂x² + a₄x + a₆. If R is a field, then this polynomial vanishes iff the cubic curve cut out by this equation is singular. Sometimes only defined up to sign in the literature; we choose the sign used by the LMFDB. For more discussion, see the LMFDB page on discriminants.

Equations
  • EllipticCurve.Δ_aux a₁ a₂ a₃ a₄ a₆ = let b₂ : R := a₁ ^ 2 + 4 * a₂, b₄ : R := 2 * a₄ + a₁ * a₃, b₆ : R := a₃ ^ 2 + 4 * a₆, b₈ : R := a₁ ^ 2 * a₆ + 4 * a₂ * a₆ - a₁ * a₃ * a₄ + a₂ * a₃ ^ 2 - a₄ ^ 2 in -b₂ ^ 2 * b₈ - 8 * b₄ ^ 3 - 27 * b₆ ^ 2 + 9 * b₂ * b₄ * b₆
structure EllipticCurve (R : Type u) [comm_ring R] :
Type u

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

Instances for EllipticCurve
@[protected, instance]
Equations

Standard quantities #

@[simp]
def EllipticCurve.b₂ {R : Type u} [comm_ring R] (E : EllipticCurve R) :
R

The b₂ coefficient of an elliptic curve.

Equations
@[simp]
def EllipticCurve.b₄ {R : Type u} [comm_ring R] (E : EllipticCurve R) :
R

The b₄ coefficient of an elliptic curve.

Equations
@[simp]
def EllipticCurve.b₆ {R : Type u} [comm_ring R] (E : EllipticCurve R) :
R

The b₆ coefficient of an elliptic curve.

Equations
@[simp]
def EllipticCurve.b₈ {R : Type u} [comm_ring R] (E : EllipticCurve R) :
R

The b₈ coefficient of an elliptic curve.

Equations
theorem EllipticCurve.b_relation {R : Type u} [comm_ring R] (E : EllipticCurve R) :
4 * E.b₈ = E.b₂ * E.b₆ - E.b₄ ^ 2
@[simp]
def EllipticCurve.c₄ {R : Type u} [comm_ring R] (E : EllipticCurve R) :
R

The c₄ coefficient of an elliptic curve.

Equations
@[simp]
def EllipticCurve.c₆ {R : Type u} [comm_ring R] (E : EllipticCurve R) :
R

The c₆ coefficient of an elliptic curve.

Equations
@[simp]
theorem EllipticCurve.coe_Δ {R : Type u} [comm_ring R] (E : EllipticCurve R) :
(E.Δ) = -E.b₂ ^ 2 * E.b₈ - 8 * E.b₄ ^ 3 - 27 * E.b₆ ^ 2 + 9 * E.b₂ * E.b₄ * E.b₆
theorem EllipticCurve.c_relation {R : Type u} [comm_ring R] (E : EllipticCurve R) :
1728 * (E.Δ) = E.c₄ ^ 3 - E.c₆ ^ 2
@[simp]
def EllipticCurve.j {R : Type u} [comm_ring R] (E : EllipticCurve R) :
R

The j-invariant of an elliptic curve, which is invariant under isomorphisms over R.

Equations

2-torsion polynomials #

def EllipticCurve.two_torsion_polynomial {R : Type u} [comm_ring R] (E : EllipticCurve R) (A : Type v) [comm_ring A] [algebra R A] :

The polynomial whose roots over a splitting field of R are the 2-torsion points of the elliptic curve when R is a field of characteristic different from 2, and whose discriminant happens to be a multiple of the discriminant of the elliptic curve.

Equations
theorem EllipticCurve.two_torsion_polynomial.disc_eq {R : Type u} [comm_ring R] (E : EllipticCurve R) (A : Type v) [comm_ring A] [algebra R A] :

Changes of variables #

def EllipticCurve.change_of_variable {R : Type u} [comm_ring R] (E : EllipticCurve R) (u : Rˣ) (r s t : R) :

The elliptic curve over R induced by an admissible linear change of variables (x, y) ↦ (u²x + r, u³y + u²sx + t) for some u ∈ Rˣ and some r, s, t ∈ R. When R is a field, any two isomorphic long Weierstrass equations are related by this.

Equations
@[simp]
theorem EllipticCurve.change_of_variable.a₁_eq {R : Type u} [comm_ring R] (E : EllipticCurve R) (u : Rˣ) (r s t : R) :
(E.change_of_variable u r s t).a₁ = u⁻¹ * (E.a₁ + 2 * s)
@[simp]
theorem EllipticCurve.change_of_variable.a₂_eq {R : Type u} [comm_ring R] (E : EllipticCurve R) (u : Rˣ) (r s t : R) :
(E.change_of_variable u r s t).a₂ = u⁻¹ ^ 2 * (E.a₂ - s * E.a₁ + 3 * r - s ^ 2)
@[simp]
theorem EllipticCurve.change_of_variable.a₃_eq {R : Type u} [comm_ring R] (E : EllipticCurve R) (u : Rˣ) (r s t : R) :
(E.change_of_variable u r s t).a₃ = u⁻¹ ^ 3 * (E.a₃ + r * E.a₁ + 2 * t)
@[simp]
theorem EllipticCurve.change_of_variable.a₄_eq {R : Type u} [comm_ring R] (E : EllipticCurve R) (u : Rˣ) (r s t : R) :
(E.change_of_variable u r s t).a₄ = u⁻¹ ^ 4 * (E.a₄ - s * E.a₃ + 2 * r * E.a₂ - (t + r * s) * E.a₁ + 3 * r ^ 2 - 2 * s * t)
@[simp]
theorem EllipticCurve.change_of_variable.a₆_eq {R : Type u} [comm_ring R] (E : EllipticCurve R) (u : Rˣ) (r s t : R) :
(E.change_of_variable u r s t).a₆ = u⁻¹ ^ 6 * (E.a₆ + r * E.a₄ + r ^ 2 * E.a₂ + r ^ 3 - t * E.a₃ - t ^ 2 - r * t * E.a₁)
@[simp]
theorem EllipticCurve.change_of_variable.b₂_eq {R : Type u} [comm_ring R] (E : EllipticCurve R) (u : Rˣ) (r s t : R) :
(E.change_of_variable u r s t).b₂ = u⁻¹ ^ 2 * (E.b₂ + 12 * r)
@[simp]
theorem EllipticCurve.change_of_variable.b₄_eq {R : Type u} [comm_ring R] (E : EllipticCurve R) (u : Rˣ) (r s t : R) :
(E.change_of_variable u r s t).b₄ = u⁻¹ ^ 4 * (E.b₄ + r * E.b₂ + 6 * r ^ 2)
@[simp]
theorem EllipticCurve.change_of_variable.b₆_eq {R : Type u} [comm_ring R] (E : EllipticCurve R) (u : Rˣ) (r s t : R) :
(E.change_of_variable u r s t).b₆ = u⁻¹ ^ 6 * (E.b₆ + 2 * r * E.b₄ + r ^ 2 * E.b₂ + 4 * r ^ 3)
@[simp]
theorem EllipticCurve.change_of_variable.b₈_eq {R : Type u} [comm_ring R] (E : EllipticCurve R) (u : Rˣ) (r s t : R) :
(E.change_of_variable u r s t).b₈ = u⁻¹ ^ 8 * (E.b₈ + 3 * r * E.b₆ + 3 * r ^ 2 * E.b₄ + r ^ 3 * E.b₂ + 3 * r ^ 4)
@[simp]
theorem EllipticCurve.change_of_variable.c₄_eq {R : Type u} [comm_ring R] (E : EllipticCurve R) (u : Rˣ) (r s t : R) :
@[simp]
theorem EllipticCurve.change_of_variable.c₆_eq {R : Type u} [comm_ring R] (E : EllipticCurve R) (u : Rˣ) (r s t : R) :
@[simp]
theorem EllipticCurve.change_of_variable.Δ_eq {R : Type u} [comm_ring R] (E : EllipticCurve R) (u : Rˣ) (r s t : R) :
(E.change_of_variable u r s t).Δ = u⁻¹ ^ 12 * E.Δ
@[simp]
theorem EllipticCurve.change_of_variable.j_eq {R : Type u} [comm_ring R] (E : EllipticCurve R) (u : Rˣ) (r s t : R) :
(E.change_of_variable u r s t).j = E.j