# 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.VariableChange: a change of variables of Weierstrass curves.
• WeierstrassCurve.variableChange: the Weierstrass curve induced by a change of variables.
• 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.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 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
instance WeierstrassCurve.instInhabited {R : Type u} [] :
Equations
• WeierstrassCurve.instInhabited = { default := { a₁ := default, a₂ := default, a₃ := default, a₄ := default, a₆ := default } }

### Standard quantities #

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

The b₂ coefficient of a Weierstrass curve.

Equations
• W.b₂ = W.a₁ ^ 2 + 4 * W.a₂
Instances For
def WeierstrassCurve.b₄ {R : Type u} [] (W : ) :
R

The b₄ coefficient of a Weierstrass curve.

Equations
• W.b₄ = 2 * W.a₄ + W.a₁ * W.a₃
Instances For
def WeierstrassCurve.b₆ {R : Type u} [] (W : ) :
R

The b₆ coefficient of a Weierstrass curve.

Equations
• W.b₆ = W.a₃ ^ 2 + 4 * W.a₆
Instances For
def WeierstrassCurve.b₈ {R : Type u} [] (W : ) :
R

The b₈ coefficient of a Weierstrass curve.

Equations
• W.b₈ = W.a₁ ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2
Instances For
theorem WeierstrassCurve.b_relation {R : Type u} [] (W : ) :
4 * W.b₈ = W.b₂ * W.b₆ - W.b₄ ^ 2
def WeierstrassCurve.c₄ {R : Type u} [] (W : ) :
R

The c₄ coefficient of a Weierstrass curve.

Equations
• W.c₄ = W.b₂ ^ 2 - 24 * W.b₄
Instances For
def WeierstrassCurve.c₆ {R : Type u} [] (W : ) :
R

The c₆ coefficient of a Weierstrass curve.

Equations
• W.c₆ = -W.b₂ ^ 3 + 36 * W.b₂ * W.b₄ - 216 * W.b₆
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.

Equations
• W = -W.b₂ ^ 2 * W.b₈ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2 + 9 * W.b₂ * W.b₄ * W.b₆
Instances For
theorem WeierstrassCurve.c_relation {R : Type u} [] (W : ) :
1728 * W = W.c₄ ^ 3 - W.c₆ ^ 2

### Variable changes #

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
theorem WeierstrassCurve.VariableChange.ext {R : Type u} :
∀ {inst : } (x y : ), x.u = y.ux.r = y.rx.s = y.sx.t = y.tx = y
structure WeierstrassCurve.VariableChange (R : Type u) [] :

An admissible linear change of variables of Weierstrass curves defined over a ring R given by a tuple $(u, r, s, t)$ for some $u \in R^\times$ and some $r, s, t \in R$. As a matrix, it is $\begin{pmatrix} u^2 & 0 & r \cr u^2s & u^3 & t \cr 0 & 0 & 1 \end{pmatrix}$.

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

Instances For

The identity linear change of variables given by the identity matrix.

Equations
• WeierstrassCurve.VariableChange.id = { u := 1, r := 0, s := 0, t := 0 }
Instances For

The composition of two linear changes of variables given by matrix multiplication.

Equations
• C.comp C' = { u := C.u * C'.u, r := C.r * C'.u ^ 2 + C'.r, s := C'.u * C.s + C'.s, t := C.t * C'.u ^ 3 + C.r * C'.s * C'.u ^ 2 + C'.t }
Instances For

The inverse of a linear change of variables given by matrix inversion.

Equations
Instances For
theorem WeierstrassCurve.VariableChange.id_comp {R : Type u} [] :
WeierstrassCurve.VariableChange.id.comp C = C
theorem WeierstrassCurve.VariableChange.comp_id {R : Type u} [] :
C.comp WeierstrassCurve.VariableChange.id = C
theorem WeierstrassCurve.VariableChange.comp_left_inv {R : Type u} [] :
C.inv.comp C = WeierstrassCurve.VariableChange.id
theorem WeierstrassCurve.VariableChange.comp_assoc {R : Type u} [] (C' : ) (C'' : ) :
(C.comp C').comp C'' = C.comp (C'.comp C'')
Equations
• WeierstrassCurve.VariableChange.instGroup =
@[simp]
theorem WeierstrassCurve.variableChange_a₄ {R : Type u} [] (W : ) :
(W.variableChange C).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 : ) :
(W.variableChange C).a₁ = C.u⁻¹ * (W.a₁ + 2 * C.s)
@[simp]
theorem WeierstrassCurve.variableChange_a₆ {R : Type u} [] (W : ) :
(W.variableChange C).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 : ) :
(W.variableChange C).a₂ = C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2)
@[simp]
theorem WeierstrassCurve.variableChange_a₃ {R : Type u} [] (W : ) :
(W.variableChange C).a₃ = C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)
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$.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem WeierstrassCurve.variableChange_id {R : Type u} [] (W : ) :
W.variableChange WeierstrassCurve.VariableChange.id = W
theorem WeierstrassCurve.variableChange_comp {R : Type u} [] (C' : ) (W : ) :
W.variableChange (C.comp C') = (W.variableChange C').variableChange C
Equations
• WeierstrassCurve.instMulActionVariableChange =
@[simp]
theorem WeierstrassCurve.variableChange_b₂ {R : Type u} [] (W : ) :
(W.variableChange C).b₂ = C.u⁻¹ ^ 2 * (W.b₂ + 12 * C.r)
@[simp]
theorem WeierstrassCurve.variableChange_b₄ {R : Type u} [] (W : ) :
(W.variableChange C).b₄ = C.u⁻¹ ^ 4 * (W.b₄ + C.r * W.b₂ + 6 * C.r ^ 2)
@[simp]
theorem WeierstrassCurve.variableChange_b₆ {R : Type u} [] (W : ) :
(W.variableChange C).b₆ = C.u⁻¹ ^ 6 * (W.b₆ + 2 * C.r * W.b₄ + C.r ^ 2 * W.b₂ + 4 * C.r ^ 3)
@[simp]
theorem WeierstrassCurve.variableChange_b₈ {R : Type u} [] (W : ) :
(W.variableChange C).b₈ = C.u⁻¹ ^ 8 * (W.b₈ + 3 * C.r * W.b₆ + 3 * C.r ^ 2 * W.b₄ + C.r ^ 3 * W.b₂ + 3 * C.r ^ 4)
@[simp]
theorem WeierstrassCurve.variableChange_c₄ {R : Type u} [] (W : ) :
(W.variableChange C).c₄ = C.u⁻¹ ^ 4 * W.c₄
@[simp]
theorem WeierstrassCurve.variableChange_c₆ {R : Type u} [] (W : ) :
(W.variableChange C).c₆ = C.u⁻¹ ^ 6 * W.c₆
@[simp]
theorem WeierstrassCurve.variableChange_Δ {R : Type u} [] (W : ) :
(W.variableChange C) = C.u⁻¹ ^ 12 * W

### Maps and base changes #

@[simp]
theorem WeierstrassCurve.map_a₃ {R : Type u} [] (W : ) {A : Type v} [] (φ : R →+* A) :
(W.map φ).a₃ = φ W.a₃
@[simp]
theorem WeierstrassCurve.map_a₂ {R : Type u} [] (W : ) {A : Type v} [] (φ : R →+* A) :
(W.map φ).a₂ = φ W.a₂
@[simp]
theorem WeierstrassCurve.map_a₄ {R : Type u} [] (W : ) {A : Type v} [] (φ : R →+* A) :
(W.map φ).a₄ = φ W.a₄
@[simp]
theorem WeierstrassCurve.map_a₁ {R : Type u} [] (W : ) {A : Type v} [] (φ : R →+* A) :
(W.map φ).a₁ = φ W.a₁
@[simp]
theorem WeierstrassCurve.map_a₆ {R : Type u} [] (W : ) {A : Type v} [] (φ : R →+* A) :
(W.map φ).a₆ = φ W.a₆
def WeierstrassCurve.map {R : Type u} [] (W : ) {A : Type v} [] (φ : R →+* A) :

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
@[reducible, inline]
abbrev WeierstrassCurve.baseChange {R : Type u} [] (W : ) (A : Type v) [] [Algebra R A] :

The Weierstrass curve base changed to an algebra A over R.

Equations
• W.baseChange A = W.map ()
Instances For
@[simp]
theorem WeierstrassCurve.map_b₂ {R : Type u} [] (W : ) {A : Type v} [] (φ : R →+* A) :
(W.map φ).b₂ = φ W.b₂
@[simp]
theorem WeierstrassCurve.map_b₄ {R : Type u} [] (W : ) {A : Type v} [] (φ : R →+* A) :
(W.map φ).b₄ = φ W.b₄
@[simp]
theorem WeierstrassCurve.map_b₆ {R : Type u} [] (W : ) {A : Type v} [] (φ : R →+* A) :
(W.map φ).b₆ = φ W.b₆
@[simp]
theorem WeierstrassCurve.map_b₈ {R : Type u} [] (W : ) {A : Type v} [] (φ : R →+* A) :
(W.map φ).b₈ = φ W.b₈
@[simp]
theorem WeierstrassCurve.map_c₄ {R : Type u} [] (W : ) {A : Type v} [] (φ : R →+* A) :
(W.map φ).c₄ = φ W.c₄
@[simp]
theorem WeierstrassCurve.map_c₆ {R : Type u} [] (W : ) {A : Type v} [] (φ : R →+* A) :
(W.map φ).c₆ = φ W.c₆
@[simp]
theorem WeierstrassCurve.map_Δ {R : Type u} [] (W : ) {A : Type v} [] (φ : R →+* A) :
(W.map φ) = φ W
@[simp]
theorem WeierstrassCurve.map_id {R : Type u} [] (W : ) :
W.map () = W
theorem WeierstrassCurve.map_map {R : Type u} [] (W : ) {A : Type v} [] (φ : R →+* A) {B : Type w} [] (ψ : A →+* B) :
(W.map φ).map ψ = W.map (ψ.comp φ)
@[simp]
theorem WeierstrassCurve.map_baseChange {R : Type u} [] (W : ) {S : Type s} [] [Algebra R S] {A : Type v} [] [Algebra R A] [Algebra S A] [] {B : Type w} [] [Algebra R B] [Algebra S B] [] (ψ : A →ₐ[S] B) :
(W.baseChange A).map ψ = W.baseChange B
theorem WeierstrassCurve.map_injective {R : Type u} [] {A : Type v} [] {φ : R →+* A} (hφ : ) :
Function.Injective fun (W : ) => W.map φ
@[simp]
theorem WeierstrassCurve.VariableChange.map_r {R : Type u} [] {A : Type v} [] (φ : R →+* A) :
= φ C.r
@[simp]
theorem WeierstrassCurve.VariableChange.map_s {R : Type u} [] {A : Type v} [] (φ : R →+* A) :
= φ C.s
@[simp]
theorem WeierstrassCurve.VariableChange.map_u {R : Type u} [] {A : Type v} [] (φ : R →+* A) :
= () C.u
@[simp]
theorem WeierstrassCurve.VariableChange.map_t {R : Type u} [] {A : Type v} [] (φ : R →+* A) :
= φ C.t
def WeierstrassCurve.VariableChange.map {R : Type u} [] {A : Type v} [] (φ : R →+* A) :

The change of variables mapped over a ring homomorphism φ : R →+* A.

Equations
• = { u := () C.u, r := φ C.r, s := φ C.s, t := φ C.t }
Instances For
@[reducible, inline]
abbrev WeierstrassCurve.VariableChange.baseChange {R : Type u} [] (A : Type v) [] [Algebra R A] :

The change of variables base changed to an algebra A over R.

Equations
Instances For
theorem WeierstrassCurve.VariableChange.map_map {R : Type u} [] {A : Type v} [] (φ : R →+* A) {B : Type w} [] (ψ : A →+* B) :
@[simp]
theorem WeierstrassCurve.VariableChange.map_baseChange {R : Type u} [] {S : Type s} [] [Algebra R S] {A : Type v} [] [Algebra R A] [Algebra S A] [] {B : Type w} [] [Algebra R B] [Algebra S B] [] (ψ : A →ₐ[S] B) :
theorem WeierstrassCurve.VariableChange.map_injective {R : Type u} [] {A : Type v} [] {φ : R →+* A} (hφ : ) :
def WeierstrassCurve.VariableChange.mapHom {R : Type u} [] {A : Type v} [] (φ : R →+* A) :

The map over a ring homomorphism of a change of variables is a group homomorphism.

Equations
• = { toFun := , map_one' := , map_mul' := }
Instances For
theorem WeierstrassCurve.map_variableChange {R : Type u} [] (W : ) {A : Type v} [] (φ : R →+* A) :
(W.map φ).variableChange = (W.variableChange C).map φ

### 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
• W.twoTorsionPolynomial = { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ }
Instances For
theorem WeierstrassCurve.twoTorsionPolynomial_disc {R : Type u} [] (W : ) :
W.twoTorsionPolynomial.disc = 16 * W
theorem WeierstrassCurve.twoTorsionPolynomial_disc_isUnit {R : Type u} [] (W : ) [] :
IsUnit W.twoTorsionPolynomial.disc IsUnit W
theorem WeierstrassCurve.twoTorsionPolynomial_disc_ne_zero {R : Type u} [] (W : ) [] [] (hΔ : IsUnit W) :
W.twoTorsionPolynomial.disc 0

### Models with prescribed j-invariant #

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.

Equations
• = { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }
Instances For
theorem WeierstrassCurve.ofJ0_c₄ (R : Type u) [] :
.c₄ = 0
theorem WeierstrassCurve.ofJ0_Δ (R : Type u) [] :
= -27

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

Equations
• = { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }
Instances For
theorem WeierstrassCurve.ofJ1728_c₄ (R : Type u) [] :
.c₄ = -48
theorem WeierstrassCurve.ofJ1728_Δ (R : Type u) [] :
= -64
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.

Equations
• = { a₁ := j - 1728, a₂ := 0, a₃ := 0, a₄ := -36 * (j - 1728) ^ 3, a₆ := -(j - 1728) ^ 5 }
Instances For
theorem WeierstrassCurve.ofJ_c₄ {R : Type u} [] (j : R) :
.c₄ = j * (j - 1728) ^ 3
theorem WeierstrassCurve.ofJ_Δ {R : Type u} [] (j : R) :
= j ^ 2 * (j - 1728) ^ 9

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

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 over R, which is given as a unit in R.

• coe_Δ' : self.Δ' = self

The discriminant of E is equal to the discriminant of E as a Weierstrass curve.

Instances For
theorem EllipticCurve.coe_Δ' {R : Type u} [] (self : ) :
self.Δ' = self

The discriminant of E is equal to the discriminant of E as a Weierstrass curve.

def EllipticCurve.j {R : Type u} [] (E : ) :
R

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

Equations
Instances For
theorem EllipticCurve.twoTorsionPolynomial_disc_ne_zero {R : Type u} [] (E : ) [] [] :
E.twoTorsionPolynomial.disc 0

### Variable changes #

@[simp]
theorem EllipticCurve.variableChange_a₄ {R : Type u} [] (E : ) :
(E.variableChange C).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 : ) :
(E.variableChange C).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 : ) :
(E.variableChange C).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 : ) :
(E.variableChange C).toWeierstrassCurve = E.variableChange C
@[simp]
theorem EllipticCurve.variableChange_a₃ {R : Type u} [] (E : ) :
(E.variableChange C).a₃ = C.u⁻¹ ^ 3 * (E.a₃ + C.r * E.a₁ + 2 * C.t)
@[simp]
theorem EllipticCurve.variableChange_Δ' {R : Type u} [] (E : ) :
(E.variableChange C).Δ' = C.u⁻¹ ^ 12 * E.Δ'
@[simp]
theorem EllipticCurve.variableChange_a₁ {R : Type u} [] (E : ) :
(E.variableChange C).a₁ = C.u⁻¹ * (E.a₁ + 2 * C.s)
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.

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

### Maps and base changes #

@[simp]
theorem EllipticCurve.map_a₁ {R : Type u} [] (E : ) {A : Type v} [] (φ : R →+* A) :
(E.map φ).a₁ = φ E.a₁
@[simp]
theorem EllipticCurve.map_a₃ {R : Type u} [] (E : ) {A : Type v} [] (φ : R →+* A) :
(E.map φ).a₃ = φ E.a₃
@[simp]
theorem EllipticCurve.map_a₂ {R : Type u} [] (E : ) {A : Type v} [] (φ : R →+* A) :
(E.map φ).a₂ = φ E.a₂
@[simp]
theorem EllipticCurve.map_a₆ {R : Type u} [] (E : ) {A : Type v} [] (φ : R →+* A) :
(E.map φ).a₆ = φ E.a₆
@[simp]
theorem EllipticCurve.map_toWeierstrassCurve {R : Type u} [] (E : ) {A : Type v} [] (φ : R →+* A) :
(E.map φ).toWeierstrassCurve = E.map φ
@[simp]
theorem EllipticCurve.map_a₄ {R : Type u} [] (E : ) {A : Type v} [] (φ : R →+* A) :
(E.map φ).a₄ = φ E.a₄
@[simp]
theorem EllipticCurve.map_Δ' {R : Type u} [] (E : ) {A : Type v} [] (φ : R →+* A) :
(E.map φ).Δ' = () E.Δ'
def EllipticCurve.map {R : Type u} [] (E : ) {A : Type v} [] (φ : R →+* A) :

The elliptic curve mapped over a ring homomorphism φ : R →+* A.

Equations
• E.map φ = { toWeierstrassCurve := E.map φ, Δ' := () E.Δ', coe_Δ' := }
Instances For
@[reducible, inline]
abbrev EllipticCurve.baseChange {R : Type u} [] (E : ) (A : Type v) [] [Algebra R A] :

The elliptic curve base changed to an algebra A over R.

Equations
• E.baseChange A = E.map ()
Instances For
theorem EllipticCurve.coe_map_Δ' {R : Type u} [] (E : ) {A : Type v} [] (φ : R →+* A) :
(E.map φ).Δ' = φ E.Δ'
theorem EllipticCurve.coe_inv_map_Δ' {R : Type u} [] (E : ) {A : Type v} [] (φ : R →+* A) :
(E.map φ).Δ'⁻¹ = φ E.Δ'⁻¹
@[simp]
theorem EllipticCurve.map_j {R : Type u} [] (E : ) {A : Type v} [] (φ : R →+* A) :
(E.map φ).j = φ E.j
theorem EllipticCurve.map_injective {R : Type u} [] {A : Type v} [] {φ : R →+* A} (hφ : ) :
Function.Injective fun (E : ) => E.map φ

### Models with prescribed j-invariant #

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

Equations
Instances For
theorem EllipticCurve.ofJ0_j (R : Type u) [] [] :
.j = 0
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).

Equations
Instances For
theorem EllipticCurve.ofJ1728_j (R : Type u) [] [] :
.j = 1728
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).

Equations
Instances For
theorem EllipticCurve.ofJ'_j {R : Type u} [] (j : R) [] [Invertible (j - 1728)] :
.j = j
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').

Equations
• = if h0 : j = 0 then if h3 : 3 = 0 then else else if h1728 : j = 1728 then else
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) [] :
.j = j
Equations
• EllipticCurve.instInhabitedEllipticCurve = { default := }