Weierstrass equations of elliptic curves #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 #
weierstrass_curve: a Weierstrass curve over a commutative ring.weierstrass_curve.Δ: the discriminant of a Weierstrass curve.weierstrass_curve.variable_change: the Weierstrass curve induced by a change of variables.weierstrass_curve.base_change: the Weierstrass curve base changed over an algebra.weierstrass_curve.two_torsion_polynomial: the 2-torsion polynomial of a Weierstrass curve.weierstrass_curve.polynomial: the polynomial associated to a Weierstrass curve.weierstrass_curve.equation: the Weirstrass equation of a Weierstrass curve.weierstrass_curve.nonsingular: the nonsingular condition at a point on a Weierstrass curve.weierstrass_curve.coordinate_ring: the coordinate ring of a Weierstrass curve.weierstrass_curve.function_field: the function field of a Weierstrass curve.weierstrass_curve.coordinate_ring.basis: the power basis of the coordinate ring overR[X].elliptic_curve: an elliptic curve over a commutative ring.elliptic_curve.j: the j-invariant of an elliptic curve.
Main statements #
weierstrass_curve.two_torsion_polynomial_disc: the discriminant of a Weierstrass curve is a constant factor of the cubic discriminant of its 2-torsion polynomial.weierstrass_curve.nonsingular_of_Δ_ne_zero: a Weierstrass curve is nonsingular at every point if its discriminant is non-zero.weierstrass_curve.coordinate_ring.is_domain: the coordinate ring of a Weierstrass curve is an integral domain.weierstrass_curve.coordinate_ring.degree_norm_smul_basis: the degree of the norm of an element in the coordinate ring in terms of the power basis.elliptic_curve.nonsingular: an elliptic curve is nonsingular at every point.elliptic_curve.variable_change_j: the j-invariant of an elliptic curve is invariant under an admissible linear change of variables.
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₁ : R
- a₂ : R
- a₃ : R
- a₄ : R
- a₆ : R
A Weierstrass curve $Y^2 + a_1XY + a_3Y = X^3 + a_2X^2 + a_4X + a_6$ with parameters $a_i$.
Instances for weierstrass_curve
- weierstrass_curve.has_sizeof_inst
- weierstrass_curve.inhabited
Equations
- weierstrass_curve.inhabited = {default := {a₁ := inhabited.default _inst_1, a₂ := inhabited.default _inst_1, a₃ := inhabited.default _inst_1, a₄ := inhabited.default _inst_1, a₆ := inhabited.default _inst_1}}
Standard quantities #
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.
Variable changes #
The Weierstrass curve over R induced by an admissible linear change of variables
$(X, Y) \mapsto (u^2X + r, u^3Y + u^2sX + t)$ for some $u \in R^\times$ and some $r, s, t \in R$.
Equations
- W.variable_change u r s t = {a₁ := ↑u⁻¹ * (W.a₁ + 2 * s), a₂ := ↑u⁻¹ ^ 2 * (W.a₂ - s * W.a₁ + 3 * r - s ^ 2), a₃ := ↑u⁻¹ ^ 3 * (W.a₃ + r * W.a₁ + 2 * t), a₄ := ↑u⁻¹ ^ 4 * (W.a₄ - s * W.a₃ + 2 * r * W.a₂ - (t + r * s) * W.a₁ + 3 * r ^ 2 - 2 * s * t), a₆ := ↑u⁻¹ ^ 6 * (W.a₆ + r * W.a₄ + r ^ 2 * W.a₂ + r ^ 3 - t * W.a₃ - t ^ 2 - r * t * W.a₁)}
Base changes #
The Weierstrass curve over R base changed to A.
Equations
- W.base_change A = {a₁ := ⇑(algebra_map R A) W.a₁, a₂ := ⇑(algebra_map R A) W.a₂, a₃ := ⇑(algebra_map R A) W.a₃, a₄ := ⇑(algebra_map R A) W.a₄, a₆ := ⇑(algebra_map R A) W.a₆}
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.
Weierstrass equations #
The polynomial $W(X, Y) := Y^2 + a_1XY + a_3Y - (X^3 + a_2X^2 + a_4X + a_6)$ associated to a
Weierstrass curve W over R. For ease of polynomial manipulation, this is represented as a term
of type R[X][X], where the inner variable represents $X$ and the outer variable represents $Y$.
For clarity, the alternative notations Y and R[X][Y] are provided in the polynomial_polynomial
locale to represent the outer variable and the bivariate polynomial ring R[X][X] respectively.
Equations
- W.polynomial = polynomial.X ^ 2 + ⇑polynomial.C (⇑polynomial.C W.a₁ * polynomial.X + ⇑polynomial.C W.a₃) * polynomial.X - ⇑polynomial.C (polynomial.X ^ 3 + ⇑polynomial.C W.a₂ * polynomial.X ^ 2 + ⇑polynomial.C W.a₄ * polynomial.X + ⇑polynomial.C W.a₆)
The proposition that an affine point $(x, y)$ lies in W. In other words, $W(x, y) = 0$.
Equations
- W.equation x y = (polynomial.eval x (polynomial.eval (⇑polynomial.C y) W.polynomial) = 0)
Nonsingularity of Weierstrass curves #
The partial derivative $W_X(X, Y)$ of $W(X, Y)$ with respect to $X$.
TODO: define this in terms of polynomial.derivative.
Equations
- W.polynomial_X = ⇑polynomial.C (⇑polynomial.C W.a₁) * polynomial.X - ⇑polynomial.C (⇑polynomial.C 3 * polynomial.X ^ 2 + ⇑polynomial.C (2 * W.a₂) * polynomial.X + ⇑polynomial.C W.a₄)
The partial derivative $W_Y(X, Y)$ of $W(X, Y)$ with respect to $Y$.
TODO: define this in terms of polynomial.derivative.
Equations
The proposition that an affine point $(x, y)$ on W is nonsingular.
In other words, either $W_X(x, y) \ne 0$ or $W_Y(x, y) \ne 0$.
Equations
- W.nonsingular x y = (W.equation x y ∧ (polynomial.eval x (polynomial.eval (⇑polynomial.C y) W.polynomial_X) ≠ 0 ∨ polynomial.eval x (polynomial.eval (⇑polynomial.C y) W.polynomial_Y) ≠ 0))
A Weierstrass curve is nonsingular at every point if its discriminant is non-zero.
Ideals in the coordinate ring #
The coordinate ring $R[W] := R[X, Y] / \langle W(X, Y) \rangle$ of W.
Note that derive comm_ring generates a reducible instance of comm_ring for coordinate_ring.
In certain circumstances this might be extremely slow, because all instances in its definition are
unified exponentially many times. In this case, one solution is to manually add the local attribute
local attribute [irreducible] coordinate_ring.comm_ring to block this type-level unification.
TODO Lean 4: verify if the new def-eq cache (lean4#1102) fixed this issue.
See Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/.E2.9C.94.20class_group.2Emk
Equations
Instances for weierstrass_curve.coordinate_ring
- weierstrass_curve.coordinate_ring.inhabited
- weierstrass_curve.coordinate_ring.comm_ring
- weierstrass_curve.coordinate_ring.is_domain
- weierstrass_curve.coordinate_ring.is_domain_of_field
- weierstrass_curve.coordinate_ring.algebra
- weierstrass_curve.coordinate_ring.algebra'
- weierstrass_curve.coordinate_ring.is_scalar_tower
- weierstrass_curve.coordinate_ring.subsingleton
The function field $R(W) := \mathrm{Frac}(R[W])$ of W.
The class of the element $X - x$ in $R[W]$ for some $x \in R$.
Equations
The class of the element $Y - y(X)$ in $R[W]$ for some $y(X) \in R[X]$.
Equations
The ideal $\langle X - x \rangle$ of $R[W]$ for some $x \in R$.
The ideal $\langle Y - y(X) \rangle$ of $R[W]$ for some $y(X) \in R[X]$.
The ideal $\langle X - x, Y - y(X) \rangle$ of $R[W]$ for some $x \in R$ and $y(X) \in R[X]$.
The coordinate ring as an R[X]-algebra #
Equations
The $R$-algebra isomorphism from $R[W] / \langle X - x, Y - y(X) \rangle$ to $R$ obtained by evaluation at $y(X)$ and at $x$ provided that $W(x, y(x)) = 0$.
Equations
- weierstrass_curve.coordinate_ring.quotient_XY_ideal_equiv W h = (ideal.quotient_equiv_alg_of_eq R _).trans ((double_quot.quot_quot_equiv_quot_of_leₐ R _).trans ((alg_equiv.restrict_scalars R (polynomial.quotient_span_C_X_sub_C_alg_equiv (polynomial.X - ⇑polynomial.C x) y)).trans (polynomial.quotient_span_X_sub_C_alg_equiv x)))
The basis $\{1, Y\}$ for the coordinate ring $R[W]$ over the polynomial ring $R[X]$.
Given a Weierstrass curve W, write W^.coordinate_ring.basis for this basis.
Equations
- weierstrass_curve.coordinate_ring.basis W = _.by_cases (λ (_x : subsingleton R), inhabited.default) (λ (_x : nontrivial R), (adjoin_root.power_basis' _).basis.reindex (fin_congr _))
Norms on the coordinate ring #
Elliptic curves #
- to_weierstrass_curve : weierstrass_curve R
- Δ' : Rˣ
- coe_Δ' : ↑(self.Δ') = self.to_weierstrass_curve.Δ
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.
Instances for elliptic_curve
- elliptic_curve.has_sizeof_inst
- elliptic_curve.inhabited
The j-invariant j of an elliptic curve, which is invariant under isomorphisms over R.
Variable changes #
The elliptic curve over R induced by an admissible linear change of variables
$(X, Y) \mapsto (u^2X + r, u^3Y + u^2sX + t)$ for some $u \in R^\times$ and some $r, s, t \in R$.
When R is a field, any two Weierstrass equations isomorphic to E are related by this.
Equations
- E.variable_change u r s t = {to_weierstrass_curve := E.to_weierstrass_curve.variable_change u r s t, Δ' := u⁻¹ ^ 12 * E.Δ', coe_Δ' := _}
Base changes #
The elliptic curve over R base changed to A.
Equations
- E.base_change A = {to_weierstrass_curve := E.to_weierstrass_curve.base_change A _inst_3, Δ' := ⇑(units.map ↑(algebra_map R A)) E.Δ', coe_Δ' := _}