Weierstrass equations of elliptic curves #
This file defines the structure of an elliptic curve as a nonsingular Weierstrass curve given by a Weierstrass equation, which is mathematically accurate in many cases but 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 one-dimensional group varieties). In
the special case where S
is the spectrum of some commutative ring R
whose Picard group is zero
(this includes all fields, all PIDs, and many other commutative rings) it can be shown (using a lot
of algebro-geometric machinery) that every elliptic curve E
is a projective plane cubic isomorphic
to a Weierstrass curve given by the equation $Y^2 + a_1XY + a_3Y = X^3 + a_2X^2 + a_4X + a_6$ for
some $a_i$ in R
, and such that a certain quantity called the discriminant of E
is a unit in R
.
If R
is a field, this quantity divides the discriminant of a cubic polynomial whose roots over a
splitting field of R
are precisely the $X$-coordinates of the non-zero 2-torsion points of E
.
Main definitions #
WeierstrassCurve
: a Weierstrass curve over a commutative ring.WeierstrassCurve.Δ
: the discriminant of a Weierstrass curve.WeierstrassCurve.ofJ0
: a Weierstrass curve whose j-invariant is 0.WeierstrassCurve.ofJ1728
: a Weierstrass curve whose j-invariant is 1728.WeierstrassCurve.ofJ
: a Weierstrass curve whose j-invariant is neither 0 nor 1728.WeierstrassCurve.map
: the Weierstrass curve mapped over a ring homomorphism.WeierstrassCurve.twoTorsionPolynomial
: the 2-torsion polynomial of a Weierstrass curve.EllipticCurve
: an elliptic curve over a commutative ring.EllipticCurve.j
: the j-invariant of an elliptic curve.EllipticCurve.ofJ0
: an elliptic curve whose j-invariant is 0.EllipticCurve.ofJ1728
: an elliptic curve whose j-invariant is 1728.EllipticCurve.ofJ'
: an elliptic curve whose j-invariant is neither 0 nor 1728.EllipticCurve.ofJ
: an elliptic curve whose j-invariant equal to j.
Main statements #
WeierstrassCurve.twoTorsionPolynomial_disc
: the discriminant of a Weierstrass curve is a constant factor of the cubic discriminant of its 2-torsion polynomial.EllipticCurve.ofJ_j
: the j-invariant ofEllipticCurve.ofJ
is equal to j.
Implementation notes #
The definition of elliptic curves 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 the spectrum $\mathrm{Spec}(R)$ of R
in the case that R
has trivial Picard
group $\mathrm{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 $\mathrm{Spec}(R)$ in the sense of
algebraic geometry which are not globally defined by a cubic equation valid over the entire base.
References #
- N Katz and B Mazur, Arithmetic Moduli of Elliptic Curves
- P Deligne, Courbes Elliptiques: Formulaire (d'après J. Tate)
- J Silverman, The Arithmetic of Elliptic Curves
Tags #
elliptic curve, weierstrass equation, j invariant
Weierstrass curves #
A Weierstrass curve $Y^2 + a_1XY + a_3Y = X^3 + a_2X^2 + a_4X + a_6$ with parameters $a_i$.
- a₁ : R
The
a₁
coefficient of a Weierstrass curve. - a₂ : R
The
a₂
coefficient of a Weierstrass curve. - a₃ : R
The
a₃
coefficient of a Weierstrass curve. - a₄ : R
The
a₄
coefficient of a Weierstrass curve. - a₆ : R
The
a₆
coefficient of a Weierstrass curve.
Instances For
Equations
- WeierstrassCurve.instInhabited = { default := { a₁ := default, a₂ := default, a₃ := default, a₄ := default, a₆ := default } }
Standard quantities #
The b₂
coefficient of a Weierstrass curve.
Instances For
The b₄
coefficient of a Weierstrass curve.
Instances For
The b₆
coefficient of a Weierstrass curve.
Instances For
The c₄
coefficient of a Weierstrass curve.
Instances For
The discriminant Δ
of a Weierstrass curve. If R
is a field, then this polynomial vanishes
if and only if 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.
Instances For
Maps and base changes #
The Weierstrass curve mapped over a ring homomorphism φ : R →+* A
.
Equations
- W.map φ = { a₁ := φ W.a₁, a₂ := φ W.a₂, a₃ := φ W.a₃, a₄ := φ W.a₄, a₆ := φ W.a₆ }
Instances For
The Weierstrass curve base changed to an algebra A
over R
.
Equations
- W.baseChange A = W.map (algebraMap R A)
Instances For
2-torsion polynomials #
A cubic polynomial whose discriminant is a multiple of the Weierstrass curve discriminant. If
W
is an elliptic curve over a field R
of characteristic different from 2, then its roots over a
splitting field of R
are precisely the $X$-coordinates of the non-zero 2-torsion points of W
.
Instances For
Models with prescribed j-invariant #
The Weierstrass curve $Y^2 + Y = X^3$. It is of j-invariant 0 if it is an elliptic curve.
Equations
- WeierstrassCurve.ofJ0 R = { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }
Instances For
The Weierstrass curve $Y^2 = X^3 + X$. It is of j-invariant 1728 if it is an elliptic curve.
Equations
- WeierstrassCurve.ofJ1728 R = { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }
Instances For
The Weierstrass curve $Y^2 + (j - 1728)XY = X^3 - 36(j - 1728)^3X - (j - 1728)^5$. It is of j-invariant j if it is an elliptic curve.
Equations
Instances For
Elliptic curves #
An elliptic curve over a commutative ring. Note that this definition is only mathematically accurate for certain rings whose Picard group has trivial 12-torsion, such as a field or a PID.
- a₁ : R
- a₂ : R
- a₃ : R
- a₄ : R
- a₆ : R
- Δ' : Rˣ
The discriminant
Δ'
of an elliptic curve overR
, which is given as a unit inR
. - coe_Δ' : ↑self.Δ' = self.Δ
The discriminant of
E
is equal to the discriminant ofE
as a Weierstrass curve.
Instances For
The discriminant of E
is equal to the discriminant of E
as a Weierstrass curve.
The j-invariant j
of an elliptic curve, which is invariant under isomorphisms over R
.
Instances For
A variant of EllipticCurve.j_eq_zero_iff
without assuming a reduced ring.
A variant of EllipticCurve.j_eq_zero_iff_of_char_two
without assuming a reduced ring.
A variant of EllipticCurve.j_eq_zero_iff_of_char_three
without assuming a reduced ring.
Maps and base changes #
The elliptic curve mapped over a ring homomorphism φ : R →+* A
.
Instances For
The elliptic curve base changed to an algebra A
over R
.
Equations
- E.baseChange A = E.map (algebraMap R A)
Instances For
Models with prescribed j-invariant #
When 3 is invertible, $Y^2 + Y = X^3$ is an elliptic curve.
It is of j-invariant 0 (see EllipticCurve.ofJ0_j
).
Equations
- EllipticCurve.ofJ0 R = { toWeierstrassCurve := WeierstrassCurve.ofJ0 R, Δ' := unitOfInvertible (-3 ^ 3), coe_Δ' := ⋯ }
Instances For
When 2 is invertible, $Y^2 = X^3 + X$ is an elliptic curve.
It is of j-invariant 1728 (see EllipticCurve.ofJ1728_j
).
Equations
- EllipticCurve.ofJ1728 R = { toWeierstrassCurve := WeierstrassCurve.ofJ1728 R, Δ' := unitOfInvertible (-2 ^ 6), coe_Δ' := ⋯ }
Instances For
When j and j - 1728 are both invertible,
$Y^2 + (j - 1728)XY = X^3 - 36(j - 1728)^3X - (j - 1728)^5$ is an elliptic curve.
It is of j-invariant j (see EllipticCurve.ofJ'_j
).
Equations
- EllipticCurve.ofJ' j = { toWeierstrassCurve := WeierstrassCurve.ofJ j, Δ' := unitOfInvertible (j ^ 2 * (j - 1728) ^ 9), coe_Δ' := ⋯ }
Instances For
For any element j of a field $F$, there exists an elliptic curve over $F$
with j-invariant equal to j (see EllipticCurve.ofJ_j
).
Its coefficients are given explicitly (see EllipticCurve.ofJ0
, EllipticCurve.ofJ1728
and EllipticCurve.ofJ'
).
Equations
- EllipticCurve.ofJ j = if h0 : j = 0 then if h3 : 3 = 0 then EllipticCurve.ofJ1728 F else EllipticCurve.ofJ0 F else if h1728 : j = 1728 then EllipticCurve.ofJ1728 F else EllipticCurve.ofJ' j
Instances For
Equations
- EllipticCurve.instInhabitedEllipticCurve = { default := EllipticCurve.ofJ 37 }