# mathlibdocumentation

algebraic_geometry.elliptic_curve.weierstrass

# Weierstrass equations of elliptic curves #

We give a working definition 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.basis: the power basis of the coordinate ring as an R[X]-algebra.
• 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.degree_norm_smul_basis: the degree of the norm of an element in the coordinate ring as an R[X]-algebra 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.

## Tags #

elliptic curve, weierstrass equation, j invariant

## Weierstrass curves #

theorem weierstrass_curve.ext_iff {R : Type u} (x y : weierstrass_curve R) :
x = y x.a₁ = y.a₁ x.a₂ = y.a₂ x.a₃ = y.a₃ x.a₄ = y.a₄ x.a₆ = y.a₆
@[ext]
structure weierstrass_curve (R : Type u) :
• 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
theorem weierstrass_curve.ext {R : Type u} (x y : weierstrass_curve R) (h : x.a₁ = y.a₁) (h_1 : x.a₂ = y.a₂) (h_2 : x.a₃ = y.a₃) (h_3 : x.a₄ = y.a₄) (h_4 : x.a₆ = y.a₆) :
x = y
@[protected, instance]
Equations

### Standard quantities #

@[simp]

The b₂ coefficient of a Weierstrass curve.

Equations
@[simp]

The b₄ coefficient of a Weierstrass curve.

Equations
@[simp]

The b₆ coefficient of a Weierstrass curve.

Equations
@[simp]

The b₈ coefficient of a Weierstrass curve.

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

The c₄ coefficient of a Weierstrass curve.

Equations
@[simp]

The c₆ coefficient of a Weierstrass curve.

Equations
@[simp]
def weierstrass_curve.Δ {R : Type u} [comm_ring R] (W : weierstrass_curve R) :
R

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.

Equations
theorem weierstrass_curve.c_relation {R : Type u} [comm_ring R] (W : weierstrass_curve R) :
1728 * W.Δ = W.c₄ ^ 3 - W.c₆ ^ 2

### Variable changes #

@[simp]
theorem weierstrass_curve.variable_change_a₃ {R : Type u} [comm_ring R] (W : weierstrass_curve R) (u : Rˣ) (r s t : R) :
(W.variable_change u r s t).a₃ = u⁻¹ ^ 3 * (W.a₃ + r * W.a₁ + 2 * t)
def weierstrass_curve.variable_change {R : Type u} [comm_ring R] (W : weierstrass_curve R) (u : Rˣ) (r s t : R) :

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
@[simp]
theorem weierstrass_curve.variable_change_a₆ {R : Type u} [comm_ring R] (W : weierstrass_curve R) (u : Rˣ) (r s t : R) :
(W.variable_change u r 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₁)
@[simp]
theorem weierstrass_curve.variable_change_a₄ {R : Type u} [comm_ring R] (W : weierstrass_curve R) (u : Rˣ) (r s t : R) :
(W.variable_change u r s t).a₄ = u⁻¹ ^ 4 * (W.a₄ - s * W.a₃ + 2 * r * W.a₂ - (t + r * s) * W.a₁ + 3 * r ^ 2 - 2 * s * t)
@[simp]
theorem weierstrass_curve.variable_change_a₂ {R : Type u} [comm_ring R] (W : weierstrass_curve R) (u : Rˣ) (r s t : R) :
(W.variable_change u r s t).a₂ = u⁻¹ ^ 2 * (W.a₂ - s * W.a₁ + 3 * r - s ^ 2)
@[simp]
theorem weierstrass_curve.variable_change_a₁ {R : Type u} [comm_ring R] (W : weierstrass_curve R) (u : Rˣ) (r s t : R) :
(W.variable_change u r s t).a₁ = u⁻¹ * (W.a₁ + 2 * s)
@[simp]
theorem weierstrass_curve.variable_change_b₂ {R : Type u} [comm_ring R] (W : weierstrass_curve R) (u : Rˣ) (r s t : R) :
(W.variable_change u r s t).b₂ = u⁻¹ ^ 2 * (W.b₂ + 12 * r)
@[simp]
theorem weierstrass_curve.variable_change_b₄ {R : Type u} [comm_ring R] (W : weierstrass_curve R) (u : Rˣ) (r s t : R) :
(W.variable_change u r s t).b₄ = u⁻¹ ^ 4 * (W.b₄ + r * W.b₂ + 6 * r ^ 2)
@[simp]
theorem weierstrass_curve.variable_change_b₆ {R : Type u} [comm_ring R] (W : weierstrass_curve R) (u : Rˣ) (r s t : R) :
(W.variable_change u r s t).b₆ = u⁻¹ ^ 6 * (W.b₆ + 2 * r * W.b₄ + r ^ 2 * W.b₂ + 4 * r ^ 3)
@[simp]
theorem weierstrass_curve.variable_change_b₈ {R : Type u} [comm_ring R] (W : weierstrass_curve R) (u : Rˣ) (r s t : R) :
(W.variable_change u r s t).b₈ = u⁻¹ ^ 8 * (W.b₈ + 3 * r * W.b₆ + 3 * r ^ 2 * W.b₄ + r ^ 3 * W.b₂ + 3 * r ^ 4)
@[simp]
theorem weierstrass_curve.variable_change_c₄ {R : Type u} [comm_ring R] (W : weierstrass_curve R) (u : Rˣ) (r s t : R) :
(W.variable_change u r s t).c₄ = u⁻¹ ^ 4 * W.c₄
@[simp]
theorem weierstrass_curve.variable_change_c₆ {R : Type u} [comm_ring R] (W : weierstrass_curve R) (u : Rˣ) (r s t : R) :
(W.variable_change u r s t).c₆ = u⁻¹ ^ 6 * W.c₆
@[simp]
theorem weierstrass_curve.variable_change_Δ {R : Type u} [comm_ring R] (W : weierstrass_curve R) (u : Rˣ) (r s t : R) :
(W.variable_change u r s t).Δ = u⁻¹ ^ 12 * W.Δ

### Base changes #

def weierstrass_curve.base_change {R : Type u} [comm_ring R] (W : weierstrass_curve R) (A : Type v) [comm_ring A] [ A] :

The Weierstrass curve over R base changed to A.

Equations
@[simp]
theorem weierstrass_curve.base_change_a₃ {R : Type u} [comm_ring R] (W : weierstrass_curve R) (A : Type v) [comm_ring A] [ A] :
@[simp]
theorem weierstrass_curve.base_change_a₁ {R : Type u} [comm_ring R] (W : weierstrass_curve R) (A : Type v) [comm_ring A] [ A] :
@[simp]
theorem weierstrass_curve.base_change_a₄ {R : Type u} [comm_ring R] (W : weierstrass_curve R) (A : Type v) [comm_ring A] [ A] :
@[simp]
theorem weierstrass_curve.base_change_a₂ {R : Type u} [comm_ring R] (W : weierstrass_curve R) (A : Type v) [comm_ring A] [ A] :
@[simp]
theorem weierstrass_curve.base_change_a₆ {R : Type u} [comm_ring R] (W : weierstrass_curve R) (A : Type v) [comm_ring A] [ A] :
@[simp]
theorem weierstrass_curve.base_change_b₂ {R : Type u} [comm_ring R] (W : weierstrass_curve R) (A : Type v) [comm_ring A] [ A] :
@[simp]
theorem weierstrass_curve.base_change_b₄ {R : Type u} [comm_ring R] (W : weierstrass_curve R) (A : Type v) [comm_ring A] [ A] :
@[simp]
theorem weierstrass_curve.base_change_b₆ {R : Type u} [comm_ring R] (W : weierstrass_curve R) (A : Type v) [comm_ring A] [ A] :
@[simp]
theorem weierstrass_curve.base_change_b₈ {R : Type u} [comm_ring R] (W : weierstrass_curve R) (A : Type v) [comm_ring A] [ A] :
@[simp]
theorem weierstrass_curve.base_change_c₄ {R : Type u} [comm_ring R] (W : weierstrass_curve R) (A : Type v) [comm_ring A] [ A] :
@[simp]
theorem weierstrass_curve.base_change_c₆ {R : Type u} [comm_ring R] (W : weierstrass_curve R) (A : Type v) [comm_ring A] [ A] :
@[simp, nolint]
theorem weierstrass_curve.base_change_Δ {R : Type u} [comm_ring R] (W : weierstrass_curve R) (A : Type v) [comm_ring A] [ A] :
(W.base_change A).Δ = A) W.Δ

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

Equations

### Weierstrass polynomials and equations #

@[protected]
noncomputable def weierstrass_curve.polynomial {R : Type u} [comm_ring R] (W : weierstrass_curve R) :

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

Equations
theorem weierstrass_curve.polynomial_eq {R : Type u} [comm_ring R] (W : weierstrass_curve R) :
W.polynomial = {a := 0, b := 1, c := {a := 0, b := 0, c := W.a₁, d := W.a₃}.to_poly, d := {a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆}.to_poly}.to_poly
@[simp]
theorem weierstrass_curve.eval_polynomial {R : Type u} [comm_ring R] (W : weierstrass_curve R) (x y : R) :
= y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆)
def weierstrass_curve.equation {R : Type u} [comm_ring R] (W : weierstrass_curve R) (x y : R) :
Prop

The proposition that an affine point $(x, y)$ lies in W. In other words, $W(x, y) = 0$.

Equations
theorem weierstrass_curve.equation_iff' {R : Type u} [comm_ring R] (W : weierstrass_curve R) (x y : R) :
W.equation x y y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆) = 0
@[simp]
theorem weierstrass_curve.equation_iff {R : Type u} [comm_ring R] (W : weierstrass_curve R) (x y : R) :
W.equation x y y ^ 2 + W.a₁ * x * y + W.a₃ * y = x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆
@[simp]

### Nonsingularity of Weierstrass curves #

noncomputable def weierstrass_curve.polynomial_X {R : Type u} [comm_ring R] (W : weierstrass_curve R) :

The partial derivative $W_X(X, Y)$ of $W(X, Y)$ with respect to $X$.

Equations
@[simp]
theorem weierstrass_curve.eval_polynomial_X {R : Type u} [comm_ring R] (W : weierstrass_curve R) (x y : R) :
= W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)
noncomputable def weierstrass_curve.polynomial_Y {R : Type u} [comm_ring R] (W : weierstrass_curve R) :

The partial derivative $W_Y(X, Y)$ of $W(X, Y)$ with respect to $Y$.

Equations
@[simp]
theorem weierstrass_curve.eval_polynomial_Y {R : Type u} [comm_ring R] (W : weierstrass_curve R) (x y : R) :
= 2 * y + W.a₁ * x + W.a₃
def weierstrass_curve.nonsingular {R : Type u} [comm_ring R] (W : weierstrass_curve R) (x y : R) :
Prop

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
theorem weierstrass_curve.nonsingular_iff' {R : Type u} [comm_ring R] (W : weierstrass_curve R) (x y : R) :
W.nonsingular x y W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄) 0 2 * y + W.a₁ * x + W.a₃ 0
@[simp]
theorem weierstrass_curve.nonsingular_iff {R : Type u} [comm_ring R] (W : weierstrass_curve R) (x y : R) :
W.nonsingular x y W.a₁ * y 3 * x ^ 2 + 2 * W.a₂ * x + W.a₄ y -y - W.a₁ * x - W.a₃
theorem weierstrass_curve.nonsingular_of_Δ_ne_zero {R : Type u} [comm_ring R] (W : weierstrass_curve R) {x y : R} (h : W.equation x y) (hΔ : W.Δ 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.

Equations
Instances for weierstrass_curve.coordinate_ring
@[protected, instance]
@[protected, instance]
@[reducible]

The function field $R(W) := \mathrm{Frac}(R[W])$ of W.

Equations
@[protected, instance]
@[protected, instance]
@[simp]
noncomputable def weierstrass_curve.coordinate_ring.X_class {R : Type u} [comm_ring R] (W : weierstrass_curve R) (x : R) :

The class of the element $X - x$ in $R[W]$ for some $x \in R$.

Equations
@[simp]
noncomputable def weierstrass_curve.coordinate_ring.Y_class {R : Type u} [comm_ring R] (W : weierstrass_curve R) (y : polynomial R) :

The class of the element $Y - y(X)$ in $R[W]$ for some $y(X) \in R[X]$.

Equations
@[simp]
noncomputable def weierstrass_curve.coordinate_ring.X_ideal {R : Type u} [comm_ring R] (W : weierstrass_curve R) (x : R) :

The ideal $\langle X - x \rangle$ of $R[W]$ for some $x \in R$.

Equations
@[simp]
noncomputable def weierstrass_curve.coordinate_ring.Y_ideal {R : Type u} [comm_ring R] (W : weierstrass_curve R) (y : polynomial R) :

The ideal $\langle Y - y(X) \rangle$ of $R[W]$ for some $y(X) \in R[X]$.

Equations

### The coordinate ring as an R[X]-algebra #

@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected]

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
theorem weierstrass_curve.coordinate_ring.smul_basis_eq_zero {R : Type u} [comm_ring R] {W : weierstrass_curve R} {p q : polynomial R} (hpq : p 1 + = 0) :
p = 0 q = 0
theorem weierstrass_curve.coordinate_ring.smul_basis_mul_C {R : Type u} [comm_ring R] (W : weierstrass_curve R) (y p q : polynomial R) :
(p 1 + * = (p * y) 1 + (q * y)

## Elliptic curves #

theorem elliptic_curve.ext_iff {R : Type u} {_inst_1 : comm_ring R} (x y : elliptic_curve R) :
x = y x.Δ' = y.Δ'
@[ext]
structure elliptic_curve (R : Type u) [comm_ring R] :

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
theorem elliptic_curve.ext {R : Type u} {_inst_1 : comm_ring R} (x y : elliptic_curve R) (h_1 : x.Δ' = y.Δ') :
x = y
@[protected, instance]
Equations
@[simp]
def elliptic_curve.j {R : Type u} [comm_ring R] (E : elliptic_curve R) :
R

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

Equations
theorem elliptic_curve.nonsingular {R : Type u} [comm_ring R] (E : elliptic_curve R) [nontrivial R] {x y : R} (h : y) :

### Variable changes #

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

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
@[simp]
@[simp]
theorem elliptic_curve.variable_change_Δ' {R : Type u} [comm_ring R] (E : elliptic_curve R) (u : Rˣ) (r s t : R) :
(E.variable_change u r s t).Δ' = u⁻¹ ^ 12 * E.Δ'
theorem elliptic_curve.coe_variable_change_Δ' {R : Type u} [comm_ring R] (E : elliptic_curve R) (u : Rˣ) (r s t : R) :
((E.variable_change u r s t).Δ') = u⁻¹ ^ 12 * (E.Δ')
theorem elliptic_curve.coe_inv_variable_change_Δ' {R : Type u} [comm_ring R] (E : elliptic_curve R) (u : Rˣ) (r s t : R) :
@[simp]
theorem elliptic_curve.variable_change_j {R : Type u} [comm_ring R] (E : elliptic_curve R) (u : Rˣ) (r s t : R) :
(E.variable_change u r s t).j = E.j

### Base changes #

@[simp]
@[simp]
theorem elliptic_curve.base_change_Δ' {R : Type u} [comm_ring R] (E : elliptic_curve R) (A : Type v) [comm_ring A] [ A] :
def elliptic_curve.base_change {R : Type u} [comm_ring R] (E : elliptic_curve R) (A : Type v) [comm_ring A] [ A] :

The elliptic curve over R base changed to A.

Equations
theorem elliptic_curve.coe_base_change_Δ' {R : Type u} [comm_ring R] (E : elliptic_curve R) (A : Type v) [comm_ring A] [ A] :
((E.base_change A).Δ') = A) (E.Δ')
@[simp]
theorem elliptic_curve.base_change_j {R : Type u} [comm_ring R] (E : elliptic_curve R) (A : Type v) [comm_ring A] [ A] :
(E.base_change A).j = A) E.j