# mathlib3documentation

algebraic_geometry.elliptic_curve.weierstrass

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

## 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.Δ
theorem weierstrass_curve.base_change_base_change {R : Type u} [comm_ring R] (W : weierstrass_curve R) (A : Type v) [comm_ring A] [ A] (B : Type w) [comm_ring B] [ B] [ B] [ B] :

### 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 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$. 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
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]
theorem weierstrass_curve.equation_iff_base_change {R : Type u} [comm_ring R] (W : weierstrass_curve R) (A : Type v) [comm_ring A] [ A] [nontrivial A] (x y : R) :
W.equation x y (W.base_change A).equation ( A) x) ( A) y)
theorem weierstrass_curve.equation_iff_base_change_of_base_change {R : Type u} [comm_ring R] (W : weierstrass_curve R) (A : Type v) [comm_ring A] [ A] (B : Type w) [comm_ring B] [ B] [ B] [ B] [nontrivial B] (x y : A) :
(W.base_change A).equation x y (W.base_change B).equation ( B) x) ( B) y)

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

TODO: define this in terms of polynomial.derivative.

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

TODO: define this in terms of polynomial.derivative.

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.equation 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.equation x y (W.a₁ * y 3 * x ^ 2 + 2 * W.a₂ * x + W.a₄ y -y - W.a₁ * x - W.a₃)
@[simp]
theorem weierstrass_curve.nonsingular_iff_base_change {R : Type u} [comm_ring R] (W : weierstrass_curve R) (A : Type v) [comm_ring A] [ A] [nontrivial A] (x y : R) :
W.nonsingular x y (W.base_change A).nonsingular ( A) x) ( A) y)
theorem weierstrass_curve.nonsingular_iff_base_change_of_base_change {R : Type u} [comm_ring R] (W : weierstrass_curve R) (A : Type v) [comm_ring A] [ A] (B : Type w) [comm_ring B] [ B] [ B] [ B] [nontrivial B] (x y : A) :
(W.base_change A).nonsingular x y (W.base_change B).nonsingular ( B) x) ( B) y)
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.

@[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
@[simp]
noncomputable def weierstrass_curve.coordinate_ring.XY_ideal {R : Type u} [comm_ring R] (W : weierstrass_curve R) (x : R) (y : polynomial R) :

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

Equations

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

@[protected, instance]
Equations
@[protected, instance]
Equations
noncomputable def weierstrass_curve.coordinate_ring.quotient_XY_ideal_equiv {R : Type u} [comm_ring R] (W : weierstrass_curve R) {x : R} {y : polynomial R} (h : = 0) :

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
@[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