# Documentation

Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

# 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, WeierstrassCurve.ofJ1728, WeierstrassCurve.ofJ: Weierstrass curves whose $j$-invariants are $0$, $1728$ and $j\neq 0,1728$, respectively.
• WeierstrassCurve.VariableChange: a change of variables of Weierstrass curves.
• WeierstrassCurve.variableChange: the Weierstrass curve induced by a change of variables.
• WeierstrassCurve.baseChange: the Weierstrass curve base changed over an algebra.
• WeierstrassCurve.twoTorsionPolynomial: the 2-torsion polynomial of a Weierstrass curve.
• WeierstrassCurve.polynomial: the polynomial associated to a Weierstrass curve.
• WeierstrassCurve.equation: the Weierstrass equation of a Weierstrass curve.
• WeierstrassCurve.nonsingular: the nonsingular condition at a point on a Weierstrass curve.
• WeierstrassCurve.CoordinateRing: the coordinate ring of a Weierstrass curve.
• WeierstrassCurve.FunctionField: the function field of a Weierstrass curve.
• WeierstrassCurve.CoordinateRing.basis: the power basis of the coordinate ring over R[X].
• EllipticCurve: an elliptic curve over a commutative ring.
• EllipticCurve.j: the j-invariant of an elliptic curve.
• EllipticCurve.ofJ0, EllipticCurve.ofJ1728, EllipticCurve.ofJ': elliptic curves whose $j$-invariants are $0$, $1728$ and $j\neq 0,1728$, respectively.
• EllipticCurve.ofJ: an elliptic curve over a field $F$, 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.
• WeierstrassCurve.nonsingular_of_Δ_ne_zero: a Weierstrass curve is nonsingular at every point if its discriminant is non-zero.
• WeierstrassCurve.CoordinateRing.instIsDomainCoordinateRing: the coordinate ring of a Weierstrass curve is an integral domain.
• WeierstrassCurve.CoordinateRing.degree_norm_smul_basis: the degree of the norm of an element in the coordinate ring in terms of the power basis.
• EllipticCurve.nonsingular: an elliptic curve is nonsingular at every point.
• EllipticCurve.variableChange_j: the j-invariant of an elliptic curve is invariant under an admissible linear change of variables.
• EllipticCurve.ofJ_j: the $j$-invariant of EllipticCurve.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][katz_mazur]
• [P Deligne, Courbes Elliptiques: Formulaire (d'après J. Tate)][deligne_formulaire]
• [J Silverman, The Arithmetic of Elliptic Curves][silverman2009]

## Tags #

elliptic curve, weierstrass equation, j invariant

## Weierstrass curves #

theorem WeierstrassCurve.ext {R : Type u} (x : ) (y : ) (a₁ : x.a₁ = y.a₁) (a₂ : x.a₂ = y.a₂) (a₃ : x.a₃ = y.a₃) (a₄ : x.a₄ = y.a₄) (a₆ : x.a₆ = y.a₆) :
x = y
theorem WeierstrassCurve.ext_iff {R : Type u} (x : ) (y : ) :
x = y x.a₁ = y.a₁ x.a₂ = y.a₂ x.a₃ = y.a₃ x.a₄ = y.a₄ x.a₆ = y.a₆
structure WeierstrassCurve (R : Type u) :
• 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.

A Weierstrass curve $Y^2 + a_1XY + a_3Y = X^3 + a_2X^2 + a_4X + a_6$ with parameters $a_i$.

Instances For

### Standard quantities #

def WeierstrassCurve.b₂ {R : Type u} [] (W : ) :
R

The b₂ coefficient of a Weierstrass curve.

Instances For
def WeierstrassCurve.b₄ {R : Type u} [] (W : ) :
R

The b₄ coefficient of a Weierstrass curve.

Instances For
def WeierstrassCurve.b₆ {R : Type u} [] (W : ) :
R

The b₆ coefficient of a Weierstrass curve.

Instances For
def WeierstrassCurve.b₈ {R : Type u} [] (W : ) :
R

The b₈ coefficient of a Weierstrass curve.

Instances For
theorem WeierstrassCurve.b_relation {R : Type u} [] (W : ) :
def WeierstrassCurve.c₄ {R : Type u} [] (W : ) :
R

The c₄ coefficient of a Weierstrass curve.

Instances For
def WeierstrassCurve.c₆ {R : Type u} [] (W : ) :
R

The c₆ coefficient of a Weierstrass curve.

Instances For
def WeierstrassCurve.Δ {R : Type u} [] (W : ) :
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.

Instances For
theorem WeierstrassCurve.c_relation {R : Type u} [] (W : ) :
1728 * =
def WeierstrassCurve.ofJ0 (R : Type u) [] :

The Weierstrass curve $Y^2 + Y = X^3$. It is of $j$-invariant $0$ if it is an elliptic curve.

Instances For

The Weierstrass curve $Y^2 = X^3 + X$. It is of $j$-invariant $1728$ if it is an elliptic curve.

Instances For
def WeierstrassCurve.ofJ {R : Type u} [] (j : R) :

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.

Instances For
theorem WeierstrassCurve.ofJ_c₄ {R : Type u} [] (j : R) :
= j * (j - 1728) ^ 3
theorem WeierstrassCurve.ofJ_Δ {R : Type u} [] (j : R) :
= j ^ 2 * (j - 1728) ^ 9

### Variable changes #

theorem WeierstrassCurve.VariableChange.ext {R : Type u} :
∀ {inst : } (x y : ), x.u = y.ux.r = y.rx.s = y.sx.t = y.tx = y
theorem WeierstrassCurve.VariableChange.ext_iff {R : Type u} :
∀ {inst : } (x y : ), x = y x.u = y.u x.r = y.r x.s = y.s x.t = y.t
structure WeierstrassCurve.VariableChange (R : Type u) [] :
• u : Rˣ

The u coefficient of an admissible linear change of variables, which must be a unit.

• r : R

The r coefficient of an admissible linear change of variables.

• s : R

The s coefficient of an admissible linear change of variables.

• t : R

The t coefficient of an admissible linear change of variables.

An admissible linear change of variables of Weierstrass curves defined over a ring R. It consists of a tuple $(u,r,s,t)$ of elements in $R$, with $u$ invertible. As a matrix, it is $\begin{pmatrix} u^2 & 0 & r \cr u^2s & u^3 & t \cr 0 & 0 & 1 \end{pmatrix}$.

Instances For

The identity linear change of variables. As a matrix, it is just identity matrix.

Instances For

The composition of two linear change of variables. As matrices, it is just matrix multiplcation.

Instances For

The inverse of a linear change of variables. As a matrix, it is just matrix inverse.

Instances For
theorem WeierstrassCurve.VariableChange.id_comp {R : Type u} [] :
WeierstrassCurve.VariableChange.comp WeierstrassCurve.VariableChange.id C = C
theorem WeierstrassCurve.VariableChange.comp_id {R : Type u} [] :
WeierstrassCurve.VariableChange.comp C WeierstrassCurve.VariableChange.id = C
theorem WeierstrassCurve.VariableChange.comp_left_inv {R : Type u} [] :
= WeierstrassCurve.VariableChange.id
theorem WeierstrassCurve.VariableChange.comp_assoc {R : Type u} [] (C' : ) (C'' : ) :
@[simp]
theorem WeierstrassCurve.variableChange_a₄ {R : Type u} [] (W : ) :
().a₄ = C.u⁻¹ ^ 4 * (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)
@[simp]
theorem WeierstrassCurve.variableChange_a₃ {R : Type u} [] (W : ) :
().a₃ = C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)
@[simp]
theorem WeierstrassCurve.variableChange_a₆ {R : Type u} [] (W : ) :
().a₆ = C.u⁻¹ ^ 6 * (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁)
@[simp]
theorem WeierstrassCurve.variableChange_a₁ {R : Type u} [] (W : ) :
().a₁ = C.u⁻¹ * (W.a₁ + 2 * C.s)
@[simp]
theorem WeierstrassCurve.variableChange_a₂ {R : Type u} [] (W : ) :
().a₂ = C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2)
def WeierstrassCurve.variableChange {R : Type u} [] (W : ) :

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

Instances For
theorem WeierstrassCurve.variableChange_id {R : Type u} [] (W : ) :
WeierstrassCurve.variableChange W WeierstrassCurve.VariableChange.id = W
theorem WeierstrassCurve.variableChange_comp {R : Type u} [] (C' : ) (W : ) :
@[simp]
theorem WeierstrassCurve.variableChange_b₂ {R : Type u} [] (W : ) :
= C.u⁻¹ ^ 2 * ( + 12 * C.r)
@[simp]
theorem WeierstrassCurve.variableChange_b₄ {R : Type u} [] (W : ) :
= C.u⁻¹ ^ 4 * ( + 6 * C.r ^ 2)
@[simp]
theorem WeierstrassCurve.variableChange_b₆ {R : Type u} [] (W : ) :
= C.u⁻¹ ^ 6 * ( + 2 * C.r * + C.r ^ 2 * + 4 * C.r ^ 3)
@[simp]
theorem WeierstrassCurve.variableChange_b₈ {R : Type u} [] (W : ) :
= C.u⁻¹ ^ 8 * ( + 3 * C.r * + 3 * C.r ^ 2 * + C.r ^ 3 * + 3 * C.r ^ 4)
@[simp]
theorem WeierstrassCurve.variableChange_c₄ {R : Type u} [] (W : ) :
@[simp]
theorem WeierstrassCurve.variableChange_c₆ {R : Type u} [] (W : ) :
@[simp]
theorem WeierstrassCurve.variableChange_Δ {R : Type u} [] (W : ) :
= C.u⁻¹ ^ 12 *

### Base changes #

@[simp]
theorem WeierstrassCurve.baseChange_a₄ {R : Type u} [] (W : ) (A : Type v) [] [Algebra R A] :
().a₄ = ↑() W.a₄
@[simp]
theorem WeierstrassCurve.baseChange_a₁ {R : Type u} [] (W : ) (A : Type v) [] [Algebra R A] :
().a₁ = ↑() W.a₁
@[simp]
theorem WeierstrassCurve.baseChange_a₆ {R : Type u} [] (W : ) (A : Type v) [] [Algebra R A] :
().a₆ = ↑() W.a₆
@[simp]
theorem WeierstrassCurve.baseChange_a₂ {R : Type u} [] (W : ) (A : Type v) [] [Algebra R A] :
().a₂ = ↑() W.a₂
@[simp]
theorem WeierstrassCurve.baseChange_a₃ {R : Type u} [] (W : ) (A : Type v) [] [Algebra R A] :
().a₃ = ↑() W.a₃
def WeierstrassCurve.baseChange {R : Type u} [] (W : ) (A : Type v) [] [Algebra R A] :

The Weierstrass curve over R base changed to A.

Instances For
@[simp]
theorem WeierstrassCurve.baseChange_b₂ {R : Type u} [] (W : ) (A : Type v) [] [Algebra R A] :
= ↑() ()
@[simp]
theorem WeierstrassCurve.baseChange_b₄ {R : Type u} [] (W : ) (A : Type v) [] [Algebra R A] :
= ↑() ()
@[simp]
theorem WeierstrassCurve.baseChange_b₆ {R : Type u} [] (W : ) (A : Type v) [] [Algebra R A] :
= ↑() ()
@[simp]
theorem WeierstrassCurve.baseChange_b₈ {R : Type u} [] (W : ) (A : Type v) [] [Algebra R A] :
= ↑() ()
@[simp]
theorem WeierstrassCurve.baseChange_c₄ {R : Type u} [] (W : ) (A : Type v) [] [Algebra R A] :
= ↑() ()
@[simp]
theorem WeierstrassCurve.baseChange_c₆ {R : Type u} [] (W : ) (A : Type v) [] [Algebra R A] :
= ↑() ()
@[simp]
theorem WeierstrassCurve.baseChange_Δ {R : Type u} [] (W : ) (A : Type v) [] [Algebra R A] :
= ↑() ()
theorem WeierstrassCurve.baseChange_self {R : Type u} [] (W : ) :
theorem WeierstrassCurve.baseChange_baseChange {R : Type u} [] (W : ) (A : Type v) [] [Algebra R A] (B : Type w) [] [Algebra R B] [Algebra A B] [] :
theorem WeierstrassCurve.baseChange_injective {R : Type u} [] (A : Type v) [] [Algebra R A] (h : Function.Injective ↑()) :
@[simp]
theorem WeierstrassCurve.VariableChange.baseChange_r {R : Type u} [] (A : Type v) [] [Algebra R A] :
= ↑() C.r
@[simp]
theorem WeierstrassCurve.VariableChange.baseChange_s {R : Type u} [] (A : Type v) [] [Algebra R A] :
= ↑() C.s
@[simp]
theorem WeierstrassCurve.VariableChange.baseChange_t {R : Type u} [] (A : Type v) [] [Algebra R A] :
= ↑() C.t
@[simp]
theorem WeierstrassCurve.VariableChange.baseChange_u {R : Type u} [] (A : Type v) [] [Algebra R A] :
= ↑(Units.map ↑()) C.u

The change of variables over R base changed to A.

Instances For
theorem WeierstrassCurve.VariableChange.baseChange_id {R : Type u} [] (A : Type v) [] [Algebra R A] :
WeierstrassCurve.VariableChange.baseChange A WeierstrassCurve.VariableChange.id = WeierstrassCurve.VariableChange.id
theorem WeierstrassCurve.VariableChange.baseChange_comp {R : Type u} [] (A : Type v) [] [Algebra R A] (C' : ) :

The base change of change of variables over R to A is a group homomorphism.

Instances For
theorem WeierstrassCurve.VariableChange.baseChange_baseChange {R : Type u} [] (A : Type v) [] [Algebra R A] (B : Type w) [] [Algebra R B] [Algebra A B] [] :
theorem WeierstrassCurve.baseChange_variableChange {R : Type u} [] (W : ) (A : Type v) [] [Algebra R 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.

Instances For
theorem WeierstrassCurve.twoTorsionPolynomial_disc_ne_zero {R : Type u} [] (W : ) [] [] (hΔ : ) :

The notation Y for X in the PolynomialPolynomial scope.

Instances For

The notation R[X][Y] for R[X][X] in the PolynomialPolynomial scope.

Instances For

### Weierstrass equations #

noncomputable def WeierstrassCurve.polynomial {R : Type u} [] (W : ) :

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 PolynomialPolynomial scope to represent the outer variable and the bivariate polynomial ring R[X][X] respectively.

Instances For
theorem WeierstrassCurve.polynomial_eq {R : Type u} [] (W : ) :
= Cubic.toPoly { a := 0, b := 1, c := Cubic.toPoly { a := 0, b := 0, c := W.a₁, d := W.a₃ }, d := Cubic.toPoly { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ } }
theorem WeierstrassCurve.polynomial_ne_zero {R : Type u} [] (W : ) [] :
@[simp]
theorem WeierstrassCurve.degree_polynomial {R : Type u} [] (W : ) [] :
@[simp]
theorem WeierstrassCurve.natDegree_polynomial {R : Type u} [] (W : ) [] :
theorem WeierstrassCurve.monic_polynomial {R : Type u} [] (W : ) :
theorem WeierstrassCurve.eval_polynomial {R : Type u} [] (W : ) (x : R) (y : R) :
Polynomial.eval x (Polynomial.eval (Polynomial.C y) ()) = y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆)
@[simp]
theorem WeierstrassCurve.eval_polynomial_zero {R : Type u} [] (W : ) :
= -W.a₆
def WeierstrassCurve.equation {R : Type u} [] (W : ) (x : R) (y : R) :

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

Instances For
theorem WeierstrassCurve.equation_iff' {R : Type u} [] (W : ) (x : R) (y : R) :
y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆) = 0
theorem WeierstrassCurve.equation_iff {R : Type u} [] (W : ) (x : R) (y : R) :
y ^ 2 + W.a₁ * x * y + W.a₃ * y = x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆
@[simp]
theorem WeierstrassCurve.equation_zero {R : Type u} [] (W : ) :
W.a₆ = 0
theorem WeierstrassCurve.equation_iff_variableChange {R : Type u} [] (W : ) (x : R) (y : R) :
WeierstrassCurve.equation (WeierstrassCurve.variableChange W { u := 1, r := x, s := 0, t := y }) 0 0
theorem WeierstrassCurve.equation_iff_baseChange {R : Type u} [] (W : ) (A : Type v) [] [Algebra R A] [] [] (x : R) (y : R) :
WeierstrassCurve.equation () (↑() x) (↑() y)
theorem WeierstrassCurve.equation_iff_baseChange_of_baseChange {R : Type u} [] (W : ) (A : Type v) [] [Algebra R A] (B : Type w) [] [Algebra R B] [Algebra A B] [] [] [] (x : A) (y : A) :
WeierstrassCurve.equation () (↑() x) (↑() y)

### Nonsingularity of Weierstrass curves #

noncomputable def WeierstrassCurve.polynomialX {R : Type u} [] (W : ) :

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

TODO: define this in terms of Polynomial.derivative.

Instances For
theorem WeierstrassCurve.eval_polynomialX {R : Type u} [] (W : ) (x : R) (y : R) :
Polynomial.eval x (Polynomial.eval (Polynomial.C y) ()) = W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)
@[simp]
theorem WeierstrassCurve.eval_polynomialX_zero {R : Type u} [] (W : ) :
= -W.a₄
noncomputable def WeierstrassCurve.polynomialY {R : Type u} [] (W : ) :

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

TODO: define this in terms of Polynomial.derivative.

Instances For
theorem WeierstrassCurve.eval_polynomialY {R : Type u} [] (W : ) (x : R) (y : R) :
Polynomial.eval x (Polynomial.eval (Polynomial.C y) ()) = 2 * y + W.a₁ * x + W.a₃
@[simp]
theorem WeierstrassCurve.eval_polynomialY_zero {R : Type u} [] (W : ) :
= W.a₃
def WeierstrassCurve.nonsingular {R : Type u} [] (W : ) (x : R) (y : R) :

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

Instances For
theorem WeierstrassCurve.nonsingular_iff' {R : Type u} [] (W : ) (x : R) (y : R) :
(W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄) 0 2 * y + W.a₁ * x + W.a₃ 0)
theorem WeierstrassCurve.nonsingular_iff {R : Type u} [] (W : ) (x : R) (y : R) :
(W.a₁ * y 3 * x ^ 2 + 2 * W.a₂ * x + W.a₄ y -y - W.a₁ * x - W.a₃)
@[simp]
theorem WeierstrassCurve.nonsingular_zero {R : Type u} [] (W : ) :
W.a₆ = 0 (W.a₃ 0 W.a₄ 0)
theorem WeierstrassCurve.nonsingular_iff_variableChange {R : Type u} [] (W : ) (x : R) (y : R) :
WeierstrassCurve.nonsingular (WeierstrassCurve.variableChange W { u := 1, r := x, s := 0, t := y }) 0 0
theorem WeierstrassCurve.nonsingular_iff_baseChange {R : Type u} [] (W : ) (A : Type v) [] [Algebra R A] [] [] (x : R) (y : R) :
WeierstrassCurve.nonsingular () (↑() x) (↑() y)
theorem WeierstrassCurve.nonsingular_iff_baseChange_of_baseChange {R : Type u} [] (W : ) (A : Type v) [] [Algebra R A] (B : Type w) [] [Algebra R B] [Algebra A B] [] [] [] (x : A) (y : A) :
WeierstrassCurve.nonsingular () (↑() x) (↑() y)
theorem WeierstrassCurve.nonsingular_zero_of_Δ_ne_zero {R : Type u} [] (W : ) (h : ) (hΔ : ) :
theorem WeierstrassCurve.nonsingular_of_Δ_ne_zero {R : Type u} [] (W : ) {x : R} {y : R} (h : ) (hΔ : ) :

A Weierstrass curve is nonsingular at every point if its discriminant is non-zero.

### Ideals in the coordinate ring #

@[inline, reducible]
abbrev WeierstrassCurve.CoordinateRing {R : Type u} [] (W : ) :

The coordinate ring $R[W] := R[X, Y] / \langle W(X, Y) \rangle$ of W.

Instances For
@[inline, reducible]
abbrev WeierstrassCurve.FunctionField {R : Type u} [] (W : ) :

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

Instances For
@[inline, reducible]
noncomputable abbrev WeierstrassCurve.CoordinateRing.mk {R : Type u} [] (W : ) :

An element of the coordinate ring R[W] of W over R.

Instances For
noncomputable def WeierstrassCurve.CoordinateRing.XClass {R : Type u} [] (W : ) (x : R) :

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

Instances For
theorem WeierstrassCurve.CoordinateRing.XClass_ne_zero {R : Type u} [] (W : ) (x : R) [] :
noncomputable def WeierstrassCurve.CoordinateRing.YClass {R : Type u} [] (W : ) (y : ) :

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

Instances For
theorem WeierstrassCurve.CoordinateRing.YClass_ne_zero {R : Type u} [] (W : ) (y : ) [] :
noncomputable def WeierstrassCurve.CoordinateRing.XIdeal {R : Type u} [] (W : ) (x : R) :

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

Instances For
noncomputable def WeierstrassCurve.CoordinateRing.YIdeal {R : Type u} [] (W : ) (y : ) :

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

Instances For
noncomputable def WeierstrassCurve.CoordinateRing.XYIdeal {R : Type u} [] (W : ) (x : R) (y : ) :

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

Instances For

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

noncomputable def WeierstrassCurve.CoordinateRing.quotientXYIdealEquiv' {R : Type u} [] (W : ) {x : R} {y : } (h : ) :
() ≃ₐ[R] Ideal.span {Polynomial.C (Polynomial.X - Polynomial.C x), Polynomial.X - Polynomial.C y}

The $R$-algebra isomorphism from $R[W] / \langle X - x, Y - y(X) \rangle$ to $R[X, Y] / \langle X - x, Y - y(X) \rangle$ provided that $W(x, y(x)) = 0$.

Instances For
noncomputable def WeierstrassCurve.CoordinateRing.quotientXYIdealEquiv {R : Type u} [] (W : ) {x : R} {y : } (h : ) :

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

Instances For
noncomputable def WeierstrassCurve.CoordinateRing.basis {R : Type u} [] (W : ) :
Basis (Fin 2) () ()

The basis ${1, Y}$ for the coordinate ring $R[W]$ over the polynomial ring $R[X]$.

Instances For
theorem WeierstrassCurve.CoordinateRing.basis_apply {R : Type u} [] (W : ) (n : Fin 2) :
= ().gen ^ n
@[simp]
@[simp]
theorem WeierstrassCurve.CoordinateRing.basis_one {R : Type u} [] (W : ) :
= ↑() Polynomial.X
theorem WeierstrassCurve.CoordinateRing.coe_basis {R : Type u} [] (W : ) :
= ![1, ↑() Polynomial.X]
theorem WeierstrassCurve.CoordinateRing.smul {R : Type u} [] {W : } (x : ) :
x y = ↑() (Polynomial.C x) * y
theorem WeierstrassCurve.CoordinateRing.smul_basis_eq_zero {R : Type u} [] {W : } {p : } {q : } (hpq : p 1 + q ↑() Polynomial.X = 0) :
p = 0 q = 0
theorem WeierstrassCurve.CoordinateRing.exists_smul_basis_eq {R : Type u} [] {W : } :
p q, p 1 + q ↑() Polynomial.X = x
theorem WeierstrassCurve.CoordinateRing.smul_basis_mul_C {R : Type u} [] (W : ) (y : ) (p : ) (q : ) :
(p 1 + q ↑() Polynomial.X) * ↑() (Polynomial.C y) = (p * y) 1 + (q * y) ↑() Polynomial.X
theorem WeierstrassCurve.CoordinateRing.smul_basis_mul_Y {R : Type u} [] (W : ) (p : ) (q : ) :
(p 1 + q ↑() Polynomial.X) * ↑() Polynomial.X = (q * (Polynomial.X ^ 3 + Polynomial.C W.a₂ * Polynomial.X ^ 2 + Polynomial.C W.a₄ * Polynomial.X + Polynomial.C W.a₆)) 1 + (p - q * (Polynomial.C W.a₁ * Polynomial.X + Polynomial.C W.a₃)) ↑() Polynomial.X

### Norms on the coordinate ring #

theorem WeierstrassCurve.CoordinateRing.norm_smul_basis {R : Type u} [] (W : ) (p : ) (q : ) :
↑() (p 1 + q ↑() Polynomial.X) = p ^ 2 - p * q * (Polynomial.C W.a₁ * Polynomial.X + Polynomial.C W.a₃) - q ^ 2 * (Polynomial.X ^ 3 + Polynomial.C W.a₂ * Polynomial.X ^ 2 + Polynomial.C W.a₄ * Polynomial.X + Polynomial.C W.a₆)
theorem WeierstrassCurve.CoordinateRing.coe_norm_smul_basis {R : Type u} [] (W : ) (p : ) (q : ) :
↑() (↑() (p 1 + q ↑() Polynomial.X)) = ↑() ((Polynomial.C p + Polynomial.C q * Polynomial.X) * (Polynomial.C p + Polynomial.C q * (-Polynomial.X - Polynomial.C (Polynomial.C W.a₁ * Polynomial.X + Polynomial.C W.a₃))))
theorem WeierstrassCurve.CoordinateRing.degree_norm_smul_basis {R : Type u} [] (W : ) [] (p : ) (q : ) :
Polynomial.degree (↑() (p 1 + q ↑() Polynomial.X)) = max () ( + 3)

## Elliptic curves #

theorem EllipticCurve.ext_iff {R : Type u} :
∀ {inst : } (x y : ), x = y x.a₁ = y.a₁ x.a₂ = y.a₂ x.a₃ = y.a₃ x.a₄ = y.a₄ x.a₆ = y.a₆ x.Δ' = y.Δ'
theorem EllipticCurve.ext {R : Type u} :
∀ {inst : } (x y : ), x.a₁ = y.a₁x.a₂ = y.a₂x.a₃ = y.a₃x.a₄ = y.a₄x.a₆ = y.a₆x.Δ' = y.Δ'x = y
structure EllipticCurve (R : Type u) [] extends :
• a₁ : R
• a₂ : R
• a₃ : R
• a₄ : R
• a₆ : R
• Δ' : Rˣ

The discriminant Δ' of an elliptic curve over R, which is given as a unit in R.

• coe_Δ' : s.Δ' = WeierstrassCurve.Δ s.toWeierstrassCurve

The discriminant of E is equal to the discriminant of E as a 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
def EllipticCurve.j {R : Type u} [] (E : ) :
R

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

Instances For
theorem EllipticCurve.nonsingular {R : Type u} [] (E : ) [] {x : R} {y : R} (h : WeierstrassCurve.equation E.toWeierstrassCurve x y) :
WeierstrassCurve.nonsingular E.toWeierstrassCurve x y
def EllipticCurve.ofJ0 (R : Type u) [] [] :

When $3$ is invertible, $Y^2 + Y = X^3$ is an elliptic curve. It is of $j$-invariant $0$ (see EllipticCurve.ofJ0_j).

Instances For
theorem EllipticCurve.ofJ0_j (R : Type u) [] [] :
def EllipticCurve.ofJ1728 (R : Type u) [] [] :

When $2$ is invertible, $Y^2 = X^3 + X$ is an elliptic curve. It is of $j$-invariant $1728$ (see EllipticCurve.ofJ1728_j).

Instances For
theorem EllipticCurve.ofJ1728_j (R : Type u) [] [] :
def EllipticCurve.ofJ' {R : Type u} [] (j : R) [] [Invertible (j - 1728)] :

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

Instances For
theorem EllipticCurve.ofJ'_j {R : Type u} [] (j : R) [] [Invertible (j - 1728)] :
def EllipticCurve.ofJ {F : Type u} [] (j : F) [] :

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').

Instances For
theorem EllipticCurve.ofJ_0_of_three_ne_zero {F : Type u} [] [] [h3 : ] :
theorem EllipticCurve.ofJ_0_of_three_eq_zero {F : Type u} [] [] (h3 : 3 = 0) :
theorem EllipticCurve.ofJ_0_of_two_eq_zero {F : Type u} [] [] (h2 : 2 = 0) :
theorem EllipticCurve.ofJ_1728_of_three_eq_zero {F : Type u} [] [] (h3 : 3 = 0) :
theorem EllipticCurve.ofJ_1728_of_two_ne_zero {F : Type u} [] [] [h2 : ] :
theorem EllipticCurve.ofJ_1728_of_two_eq_zero {F : Type u} [] [] (h2 : 2 = 0) :
theorem EllipticCurve.ofJ_ne_0_ne_1728 {F : Type u} [] (j : F) [] (h0 : j 0) (h1728 : j 1728) :
theorem EllipticCurve.ofJ_j {F : Type u} [] (j : F) [] :

### Variable changes #

@[simp]
theorem EllipticCurve.variableChange_a₄ {R : Type u} [] (E : ) :
().toWeierstrassCurve.a₄ = C.u⁻¹ ^ 4 * (E.a₄ - C.s * E.a₃ + 2 * C.r * E.a₂ - (C.t + C.r * C.s) * E.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)
@[simp]
theorem EllipticCurve.variableChange_a₆ {R : Type u} [] (E : ) :
().toWeierstrassCurve.a₆ = C.u⁻¹ ^ 6 * (E.a₆ + C.r * E.a₄ + C.r ^ 2 * E.a₂ + C.r ^ 3 - C.t * E.a₃ - C.t ^ 2 - C.r * C.t * E.a₁)
@[simp]
theorem EllipticCurve.variableChange_toWeierstrassCurve {R : Type u} [] (E : ) :
().toWeierstrassCurve = WeierstrassCurve.variableChange E.toWeierstrassCurve C
@[simp]
theorem EllipticCurve.variableChange_a₁ {R : Type u} [] (E : ) :
().toWeierstrassCurve.a₁ = C.u⁻¹ * (E.a₁ + 2 * C.s)
@[simp]
theorem EllipticCurve.variableChange_a₂ {R : Type u} [] (E : ) :
().toWeierstrassCurve.a₂ = C.u⁻¹ ^ 2 * (E.a₂ - C.s * E.a₁ + 3 * C.r - C.s ^ 2)
@[simp]
theorem EllipticCurve.variableChange_a₃ {R : Type u} [] (E : ) :
().toWeierstrassCurve.a₃ = C.u⁻¹ ^ 3 * (E.a₃ + C.r * E.a₁ + 2 * C.t)
@[simp]
theorem EllipticCurve.variableChange_Δ' {R : Type u} [] (E : ) :
().Δ' = C.u⁻¹ ^ 12 * E.Δ'
def EllipticCurve.variableChange {R : Type u} [] (E : ) :

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.

Instances For
theorem EllipticCurve.variableChange_id {R : Type u} [] (E : ) :
EllipticCurve.variableChange E WeierstrassCurve.VariableChange.id = E
theorem EllipticCurve.variableChange_comp {R : Type u} [] (C' : ) (E : ) :
theorem EllipticCurve.coe_variableChange_Δ' {R : Type u} [] (E : ) :
().Δ' = C.u⁻¹ ^ 12 * E.Δ'
theorem EllipticCurve.coe_inv_variableChange_Δ' {R : Type u} [] (E : ) :
().Δ'⁻¹ = C.u ^ 12 * E.Δ'⁻¹
@[simp]
theorem EllipticCurve.variableChange_j {R : Type u} [] (E : ) :

### Base changes #

@[simp]
theorem EllipticCurve.baseChange_a₃ {R : Type u} [] (E : ) (A : Type v) [] [Algebra R A] :
().toWeierstrassCurve.a₃ = ↑() E.a₃
@[simp]
theorem EllipticCurve.baseChange_toWeierstrassCurve {R : Type u} [] (E : ) (A : Type v) [] [Algebra R A] :
().toWeierstrassCurve = WeierstrassCurve.baseChange E.toWeierstrassCurve A
@[simp]
theorem EllipticCurve.baseChange_a₂ {R : Type u} [] (E : ) (A : Type v) [] [Algebra R A] :
().toWeierstrassCurve.a₂ = ↑() E.a₂
@[simp]
theorem EllipticCurve.baseChange_Δ' {R : Type u} [] (E : ) (A : Type v) [] [Algebra R A] :
().Δ' = ↑(Units.map ↑()) E.Δ'
@[simp]
theorem EllipticCurve.baseChange_a₄ {R : Type u} [] (E : ) (A : Type v) [] [Algebra R A] :
().toWeierstrassCurve.a₄ = ↑() E.a₄
@[simp]
theorem EllipticCurve.baseChange_a₆ {R : Type u} [] (E : ) (A : Type v) [] [Algebra R A] :
().toWeierstrassCurve.a₆ = ↑() E.a₆
@[simp]
theorem EllipticCurve.baseChange_a₁ {R : Type u} [] (E : ) (A : Type v) [] [Algebra R A] :
().toWeierstrassCurve.a₁ = ↑() E.a₁
def EllipticCurve.baseChange {R : Type u} [] (E : ) (A : Type v) [] [Algebra R A] :

The elliptic curve over R base changed to A.

Instances For
theorem EllipticCurve.coeBaseChange_Δ' {R : Type u} [] (E : ) (A : Type v) [] [Algebra R A] :
().Δ' = ↑() E.Δ'
theorem EllipticCurve.coe_inv_baseChange_Δ' {R : Type u} [] (E : ) (A : Type v) [] [Algebra R A] :
().Δ'⁻¹ = ↑() E.Δ'⁻¹
@[simp]
theorem EllipticCurve.baseChange_j {R : Type u} [] (E : ) (A : Type v) [] [Algebra R A] :
= ↑() ()
theorem EllipticCurve.baseChange_injective {R : Type u} [] (A : Type v) [] [Algebra R A] (h : Function.Injective ↑()) :