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 : WeierstrassCurve R) (y : WeierstrassCurve R) (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 : WeierstrassCurve R) (y : WeierstrassCurve R) : 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) : 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.

instance WeierstrassCurve.instInhabitedWeierstrassCurve {R : Type u} [Inhabited R] : Inhabited (WeierstrassCurve R)

Equations

• WeierstrassCurve.instInhabitedWeierstrassCurve = { default := { a₁ := default, a₂ := default, a₃ := default, a₄ := default, a₆ := default } }

Standard quantities

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

The b₂ coefficient of a Weierstrass curve.

Equations

• W.b₂ = W.a₁ ^ 2 + 4 * W.a₂

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

The b₄ coefficient of a Weierstrass curve.

Equations

• W.b₄ = 2 * W.a₄ + W.a₁ * W.a₃

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

The b₆ coefficient of a Weierstrass curve.

Equations

• W.b₆ = W.a₃ ^ 2 + 4 * W.a₆

def WeierstrassCurve.b₈ {R : Type u} [CommRing R] (W : WeierstrassCurve R) : 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

theorem WeierstrassCurve.b_relation {R : Type u} [CommRing R] (W : WeierstrassCurve R) : 4 * W.b₈ = W.b₂ * W.b₆ - W.b₄ ^ 2

def WeierstrassCurve.c₄ {R : Type u} [CommRing R] (W : WeierstrassCurve R) : R

The c₄ coefficient of a Weierstrass curve.

Equations

• W.c₄ = W.b₂ ^ 2 - 24 * W.b₄

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

The c₆ coefficient of a Weierstrass curve.

Equations

• W.c₆ = -W.b₂ ^ 3 + 36 * W.b₂ * W.b₄ - 216 * W.b₆

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

• W.Δ = -W.b₂ ^ 2 * W.b₈ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2 + 9 * W.b₂ * W.b₄ * W.b₆

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

Variable changes

theorem WeierstrassCurve.VariableChange.ext {R : Type u} : ∀ {inst : CommRing R} (x y : WeierstrassCurve.VariableChange R), x.u = y.u → x.r = y.r → x.s = y.s → x.t = y.t → x = y

theorem WeierstrassCurve.VariableChange.ext_iff {R : Type u} : ∀ {inst : CommRing R} (x y : WeierstrassCurve.VariableChange R), x = y ↔ x.u = y.u ∧ x.r = y.r ∧ x.s = y.s ∧ x.t = y.t

structure WeierstrassCurve.VariableChange (R : Type u) [CommRing 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.

def WeierstrassCurve.VariableChange.id {R : Type u} [CommRing R] : WeierstrassCurve.VariableChange R

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

Equations

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

def WeierstrassCurve.VariableChange.comp {R : Type u} [CommRing R] (C : WeierstrassCurve.VariableChange R) (C' : WeierstrassCurve.VariableChange R) : WeierstrassCurve.VariableChange R

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 }

def WeierstrassCurve.VariableChange.inv {R : Type u} [CommRing R] (C : WeierstrassCurve.VariableChange R) : WeierstrassCurve.VariableChange R

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

Equations

• C.inv = { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }

theorem WeierstrassCurve.VariableChange.id_comp {R : Type u} [CommRing R] (C : WeierstrassCurve.VariableChange R) : WeierstrassCurve.VariableChange.id.comp C = C

theorem WeierstrassCurve.VariableChange.comp_id {R : Type u} [CommRing R] (C : WeierstrassCurve.VariableChange R) : C.comp WeierstrassCurve.VariableChange.id = C

theorem WeierstrassCurve.VariableChange.comp_left_inv {R : Type u} [CommRing R] (C : WeierstrassCurve.VariableChange R) : C.inv.comp C = WeierstrassCurve.VariableChange.id

theorem WeierstrassCurve.VariableChange.comp_assoc {R : Type u} [CommRing R] (C : WeierstrassCurve.VariableChange R) (C' : WeierstrassCurve.VariableChange R) (C'' : WeierstrassCurve.VariableChange R) : (C.comp C').comp C'' = C.comp (C'.comp C'')

instance WeierstrassCurve.VariableChange.instGroupVariableChange {R : Type u} [CommRing R] : Group (WeierstrassCurve.VariableChange R)

Equations

• WeierstrassCurve.VariableChange.instGroupVariableChange = Group.mk ⋯

@[simp]

theorem WeierstrassCurve.variableChange_a₄ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) : (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} [CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) : (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} [CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) : (W.variableChange C).a₃ = ↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)

@[simp]

theorem WeierstrassCurve.variableChange_a₂ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) : (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} [CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) : (W.variableChange C).a₁ = ↑C.u⁻¹ * (W.a₁ + 2 * C.s)

def WeierstrassCurve.variableChange {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) : WeierstrassCurve 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

• One or more equations did not get rendered due to their size.

theorem WeierstrassCurve.variableChange_id {R : Type u} [CommRing R] (W : WeierstrassCurve R) : W.variableChange WeierstrassCurve.VariableChange.id = W

theorem WeierstrassCurve.variableChange_comp {R : Type u} [CommRing R] (C : WeierstrassCurve.VariableChange R) (C' : WeierstrassCurve.VariableChange R) (W : WeierstrassCurve R) : W.variableChange (C.comp C') = (W.variableChange C').variableChange C

instance WeierstrassCurve.instMulActionVariableChange {R : Type u} [CommRing R] : MulAction (WeierstrassCurve.VariableChange R) (WeierstrassCurve R)

Equations

• WeierstrassCurve.instMulActionVariableChange = MulAction.mk ⋯ ⋯

@[simp]

theorem WeierstrassCurve.variableChange_b₂ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) : (W.variableChange C).b₂ = ↑C.u⁻¹ ^ 2 * (W.b₂ + 12 * C.r)

@[simp]

theorem WeierstrassCurve.variableChange_b₄ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) : (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} [CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) : (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} [CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) : (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} [CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) : (W.variableChange C).c₄ = ↑C.u⁻¹ ^ 4 * W.c₄

@[simp]

theorem WeierstrassCurve.variableChange_c₆ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) : (W.variableChange C).c₆ = ↑C.u⁻¹ ^ 6 * W.c₆

@[simp]

theorem WeierstrassCurve.variableChange_Δ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) : (W.variableChange C).Δ = ↑C.u⁻¹ ^ 12 * W.Δ

Maps and base changes

@[simp]

theorem WeierstrassCurve.map_a₄ {R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (φ : R →+* A) : (W.map φ).a₄ = φ W.a₄

@[simp]

theorem WeierstrassCurve.map_a₁ {R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (φ : R →+* A) : (W.map φ).a₁ = φ W.a₁

@[simp]

theorem WeierstrassCurve.map_a₆ {R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (φ : R →+* A) : (W.map φ).a₆ = φ W.a₆

@[simp]

theorem WeierstrassCurve.map_a₂ {R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (φ : R →+* A) : (W.map φ).a₂ = φ W.a₂

@[simp]

theorem WeierstrassCurve.map_a₃ {R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (φ : R →+* A) : (W.map φ).a₃ = φ W.a₃

def WeierstrassCurve.map {R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (φ : R →+* A) : WeierstrassCurve 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₆ }

@[reducible, inline]

abbrev WeierstrassCurve.baseChange {R : Type u} [CommRing R] (W : WeierstrassCurve R) (A : Type v) [CommRing A] [Algebra R A] : WeierstrassCurve A

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

Equations

• W.baseChange A = W.map (algebraMap R A)

@[simp]

theorem WeierstrassCurve.map_b₂ {R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (φ : R →+* A) : (W.map φ).b₂ = φ W.b₂

@[simp]

theorem WeierstrassCurve.map_b₄ {R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (φ : R →+* A) : (W.map φ).b₄ = φ W.b₄

@[simp]

theorem WeierstrassCurve.map_b₆ {R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (φ : R →+* A) : (W.map φ).b₆ = φ W.b₆

@[simp]

theorem WeierstrassCurve.map_b₈ {R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (φ : R →+* A) : (W.map φ).b₈ = φ W.b₈

@[simp]

theorem WeierstrassCurve.map_c₄ {R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (φ : R →+* A) : (W.map φ).c₄ = φ W.c₄

@[simp]

theorem WeierstrassCurve.map_c₆ {R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (φ : R →+* A) : (W.map φ).c₆ = φ W.c₆

@[simp]

theorem WeierstrassCurve.map_Δ {R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (φ : R →+* A) : (W.map φ).Δ = φ W.Δ

@[simp]

theorem WeierstrassCurve.map_id {R : Type u} [CommRing R] (W : WeierstrassCurve R) : W.map (RingHom.id R) = W

theorem WeierstrassCurve.map_map {R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (φ : R →+* A) {B : Type w} [CommRing B] (ψ : A →+* B) : (W.map φ).map ψ = W.map (ψ.comp φ)

@[simp]

theorem WeierstrassCurve.map_baseChange {R : Type u} [CommRing R] (W : WeierstrassCurve R) {S : Type s} [CommRing S] [Algebra R S] {A : Type v} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type w} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (ψ : A →ₐ[S] B) : (W.baseChange A).map ↑ψ = W.baseChange B

theorem WeierstrassCurve.map_injective {R : Type u} [CommRing R] {A : Type v} [CommRing A] {φ : R →+* A} (hφ : Function.Injective ⇑φ) : Function.Injective fun (W : WeierstrassCurve R) => W.map φ

@[simp]

theorem WeierstrassCurve.VariableChange.map_t {R : Type u} [CommRing R] {A : Type v} [CommRing A] (φ : R →+* A) (C : WeierstrassCurve.VariableChange R) : (φ.map C).t = φ C.t

@[simp]

theorem WeierstrassCurve.VariableChange.map_r {R : Type u} [CommRing R] {A : Type v} [CommRing A] (φ : R →+* A) (C : WeierstrassCurve.VariableChange R) : (φ.map C).r = φ C.r

@[simp]

theorem WeierstrassCurve.VariableChange.map_s {R : Type u} [CommRing R] {A : Type v} [CommRing A] (φ : R →+* A) (C : WeierstrassCurve.VariableChange R) : (φ.map C).s = φ C.s

@[simp]

theorem WeierstrassCurve.VariableChange.map_u {R : Type u} [CommRing R] {A : Type v} [CommRing A] (φ : R →+* A) (C : WeierstrassCurve.VariableChange R) : (φ.map C).u = (Units.map ↑φ) C.u

def WeierstrassCurve.VariableChange.map {R : Type u} [CommRing R] {A : Type v} [CommRing A] (φ : R →+* A) (C : WeierstrassCurve.VariableChange R) : WeierstrassCurve.VariableChange A

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

Equations

• φ.map C = { u := (Units.map ↑φ) C.u, r := φ C.r, s := φ C.s, t := φ C.t }

@[reducible, inline]

abbrev WeierstrassCurve.VariableChange.baseChange {R : Type u} [CommRing R] (A : Type v) [CommRing A] (C : WeierstrassCurve.VariableChange R) [Algebra R A] : WeierstrassCurve.VariableChange A

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

Equations

• A.baseChange C = (algebraMap R A).map C

@[simp]

theorem WeierstrassCurve.VariableChange.map_id {R : Type u} [CommRing R] (C : WeierstrassCurve.VariableChange R) : (RingHom.id R).map C = C

theorem WeierstrassCurve.VariableChange.map_map {R : Type u} [CommRing R] (C : WeierstrassCurve.VariableChange R) {A : Type v} [CommRing A] (φ : R →+* A) {B : Type w} [CommRing B] (ψ : A →+* B) : ψ.map (φ.map C) = (ψ.comp φ).map C

@[simp]

theorem WeierstrassCurve.VariableChange.map_baseChange {R : Type u} [CommRing R] (C : WeierstrassCurve.VariableChange R) {S : Type s} [CommRing S] [Algebra R S] {A : Type v} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type w} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (ψ : A →ₐ[S] B) : (↑ψ).map (A.baseChange C) = B.baseChange C

theorem WeierstrassCurve.VariableChange.map_injective {R : Type u} [CommRing R] {A : Type v} [CommRing A] {φ : R →+* A} (hφ : Function.Injective ⇑φ) : Function.Injective φ.map

def WeierstrassCurve.VariableChange.mapHom {R : Type u} [CommRing R] {A : Type v} [CommRing A] (φ : R →+* A) : WeierstrassCurve.VariableChange R →* WeierstrassCurve.VariableChange A

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

Equations

• WeierstrassCurve.VariableChange.mapHom φ = { toFun := φ.map, map_one' := ⋯, map_mul' := ⋯ }

theorem WeierstrassCurve.map_variableChange {R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (φ : R →+* A) (C : WeierstrassCurve.VariableChange R) : (W.map φ).variableChange (φ.map C) = (W.variableChange C).map φ

2-torsion polynomials

def WeierstrassCurve.twoTorsionPolynomial {R : Type u} [CommRing R] (W : WeierstrassCurve R) : Cubic R

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₆ }

theorem WeierstrassCurve.twoTorsionPolynomial_disc {R : Type u} [CommRing R] (W : WeierstrassCurve R) : W.twoTorsionPolynomial.disc = 16 * W.Δ

theorem WeierstrassCurve.twoTorsionPolynomial_disc_isUnit {R : Type u} [CommRing R] (W : WeierstrassCurve R) [Invertible 2] : IsUnit W.twoTorsionPolynomial.disc ↔ IsUnit W.Δ

theorem WeierstrassCurve.twoTorsionPolynomial_disc_ne_zero {R : Type u} [CommRing R] (W : WeierstrassCurve R) [Nontrivial R] [Invertible 2] (hΔ : IsUnit W.Δ) : W.twoTorsionPolynomial.disc ≠ 0

Models with prescribed j-invariant

def WeierstrassCurve.ofJ0 (R : Type u) [CommRing R] : WeierstrassCurve R

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

Equations

• WeierstrassCurve.ofJ0 R = { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }

theorem WeierstrassCurve.ofJ0_c₄ (R : Type u) [CommRing R] : (WeierstrassCurve.ofJ0 R).c₄ = 0

theorem WeierstrassCurve.ofJ0_Δ (R : Type u) [CommRing R] : (WeierstrassCurve.ofJ0 R).Δ = -27

def WeierstrassCurve.ofJ1728 (R : Type u) [CommRing R] : WeierstrassCurve R

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

Equations

• WeierstrassCurve.ofJ1728 R = { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }

theorem WeierstrassCurve.ofJ1728_c₄ (R : Type u) [CommRing R] : (WeierstrassCurve.ofJ1728 R).c₄ = -48

theorem WeierstrassCurve.ofJ1728_Δ (R : Type u) [CommRing R] : (WeierstrassCurve.ofJ1728 R).Δ = -64

def WeierstrassCurve.ofJ {R : Type u} [CommRing R] (j : R) : WeierstrassCurve 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

• WeierstrassCurve.ofJ j = { a₁ := j - 1728, a₂ := 0, a₃ := 0, a₄ := -36 * (j - 1728) ^ 3, a₆ := -(j - 1728) ^ 5 }

theorem WeierstrassCurve.ofJ_c₄ {R : Type u} [CommRing R] (j : R) : (WeierstrassCurve.ofJ j).c₄ = j * (j - 1728) ^ 3

theorem WeierstrassCurve.ofJ_Δ {R : Type u} [CommRing R] (j : R) : (WeierstrassCurve.ofJ j).Δ = j ^ 2 * (j - 1728) ^ 9

Elliptic curves

theorem EllipticCurve.ext_iff {R : Type u} : ∀ {inst : CommRing R} (x y : EllipticCurve R), 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 : CommRing R} (x y : EllipticCurve R), 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) [CommRing R] extends WeierstrassCurve : Type u

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.

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

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

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

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

Equations

• E.j = ↑E.Δ'⁻¹ * E.c₄ ^ 3

theorem EllipticCurve.twoTorsionPolynomial_disc_ne_zero {R : Type u} [CommRing R] (E : EllipticCurve R) [Nontrivial R] [Invertible 2] : E.twoTorsionPolynomial.disc ≠ 0

Variable changes

@[simp]

theorem EllipticCurve.variableChange_a₃ {R : Type u} [CommRing R] (E : EllipticCurve R) (C : WeierstrassCurve.VariableChange R) : (E.variableChange C).a₃ = ↑C.u⁻¹ ^ 3 * (E.a₃ + C.r * E.a₁ + 2 * C.t)

@[simp]

theorem EllipticCurve.variableChange_a₁ {R : Type u} [CommRing R] (E : EllipticCurve R) (C : WeierstrassCurve.VariableChange R) : (E.variableChange C).a₁ = ↑C.u⁻¹ * (E.a₁ + 2 * C.s)

@[simp]

theorem EllipticCurve.variableChange_toWeierstrassCurve {R : Type u} [CommRing R] (E : EllipticCurve R) (C : WeierstrassCurve.VariableChange R) : (E.variableChange C).toWeierstrassCurve = E.variableChange C

@[simp]

theorem EllipticCurve.variableChange_a₆ {R : Type u} [CommRing R] (E : EllipticCurve R) (C : WeierstrassCurve.VariableChange R) : (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_a₄ {R : Type u} [CommRing R] (E : EllipticCurve R) (C : WeierstrassCurve.VariableChange R) : (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} [CommRing R] (E : EllipticCurve R) (C : WeierstrassCurve.VariableChange R) : (E.variableChange C).a₂ = ↑C.u⁻¹ ^ 2 * (E.a₂ - C.s * E.a₁ + 3 * C.r - C.s ^ 2)

@[simp]

theorem EllipticCurve.variableChange_Δ' {R : Type u} [CommRing R] (E : EllipticCurve R) (C : WeierstrassCurve.VariableChange R) : (E.variableChange C).Δ' = C.u⁻¹ ^ 12 * E.Δ'

def EllipticCurve.variableChange {R : Type u} [CommRing R] (E : EllipticCurve R) (C : WeierstrassCurve.VariableChange R) : EllipticCurve 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

• E.variableChange C = { toWeierstrassCurve := E.variableChange C, Δ' := C.u⁻¹ ^ 12 * E.Δ', coe_Δ' := ⋯ }

theorem EllipticCurve.variableChange_id {R : Type u} [CommRing R] (E : EllipticCurve R) : E.variableChange WeierstrassCurve.VariableChange.id = E

theorem EllipticCurve.variableChange_comp {R : Type u} [CommRing R] (C : WeierstrassCurve.VariableChange R) (C' : WeierstrassCurve.VariableChange R) (E : EllipticCurve R) : E.variableChange (C.comp C') = (E.variableChange C').variableChange C

instance EllipticCurve.instMulActionVariableChange {R : Type u} [CommRing R] : MulAction (WeierstrassCurve.VariableChange R) (EllipticCurve R)

Equations

• EllipticCurve.instMulActionVariableChange = MulAction.mk ⋯ ⋯

theorem EllipticCurve.coe_variableChange_Δ' {R : Type u} [CommRing R] (E : EllipticCurve R) (C : WeierstrassCurve.VariableChange R) : (E.variableChange C).Δ' = C.u⁻¹ ^ 12 * E.Δ'

theorem EllipticCurve.coe_inv_variableChange_Δ' {R : Type u} [CommRing R] (E : EllipticCurve R) (C : WeierstrassCurve.VariableChange R) : (E.variableChange C).Δ'⁻¹ = C.u ^ 12 * E.Δ'⁻¹

@[simp]

theorem EllipticCurve.variableChange_j {R : Type u} [CommRing R] (E : EllipticCurve R) (C : WeierstrassCurve.VariableChange R) : (E.variableChange C).j = E.j

Maps and base changes

@[simp]

theorem EllipticCurve.map_toWeierstrassCurve {R : Type u} [CommRing R] (E : EllipticCurve R) {A : Type v} [CommRing A] (φ : R →+* A) : (E.map φ).toWeierstrassCurve = E.map φ

@[simp]

theorem EllipticCurve.map_a₄ {R : Type u} [CommRing R] (E : EllipticCurve R) {A : Type v} [CommRing A] (φ : R →+* A) : (E.map φ).a₄ = φ E.a₄

@[simp]

theorem EllipticCurve.map_a₁ {R : Type u} [CommRing R] (E : EllipticCurve R) {A : Type v} [CommRing A] (φ : R →+* A) : (E.map φ).a₁ = φ E.a₁

@[simp]

theorem EllipticCurve.map_a₃ {R : Type u} [CommRing R] (E : EllipticCurve R) {A : Type v} [CommRing A] (φ : R →+* A) : (E.map φ).a₃ = φ E.a₃

@[simp]

theorem EllipticCurve.map_a₂ {R : Type u} [CommRing R] (E : EllipticCurve R) {A : Type v} [CommRing A] (φ : R →+* A) : (E.map φ).a₂ = φ E.a₂

@[simp]

theorem EllipticCurve.map_Δ' {R : Type u} [CommRing R] (E : EllipticCurve R) {A : Type v} [CommRing A] (φ : R →+* A) : (E.map φ).Δ' = (Units.map ↑φ) E.Δ'

@[simp]

theorem EllipticCurve.map_a₆ {R : Type u} [CommRing R] (E : EllipticCurve R) {A : Type v} [CommRing A] (φ : R →+* A) : (E.map φ).a₆ = φ E.a₆

def EllipticCurve.map {R : Type u} [CommRing R] (E : EllipticCurve R) {A : Type v} [CommRing A] (φ : R →+* A) : EllipticCurve A

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

Equations

• E.map φ = { toWeierstrassCurve := E.map φ, Δ' := (Units.map ↑φ) E.Δ', coe_Δ' := ⋯ }

@[reducible, inline]

abbrev EllipticCurve.baseChange {R : Type u} [CommRing R] (E : EllipticCurve R) (A : Type v) [CommRing A] [Algebra R A] : EllipticCurve A

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

Equations

• E.baseChange A = E.map (algebraMap R A)

theorem EllipticCurve.coe_map_Δ' {R : Type u} [CommRing R] (E : EllipticCurve R) {A : Type v} [CommRing A] (φ : R →+* A) : ↑(E.map φ).Δ' = φ ↑E.Δ'

theorem EllipticCurve.coe_inv_map_Δ' {R : Type u} [CommRing R] (E : EllipticCurve R) {A : Type v} [CommRing A] (φ : R →+* A) : ↑(E.map φ).Δ'⁻¹ = φ ↑E.Δ'⁻¹

@[simp]

theorem EllipticCurve.map_j {R : Type u} [CommRing R] (E : EllipticCurve R) {A : Type v} [CommRing A] (φ : R →+* A) : (E.map φ).j = φ E.j

theorem EllipticCurve.map_injective {R : Type u} [CommRing R] {A : Type v} [CommRing A] {φ : R →+* A} (hφ : Function.Injective ⇑φ) : Function.Injective fun (E : EllipticCurve R) => E.map φ

Models with prescribed j-invariant

def EllipticCurve.ofJ0 (R : Type u) [CommRing R] [Invertible 3] : EllipticCurve R

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

Equations

• EllipticCurve.ofJ0 R = let_fun this := invertibleNeg (3 ^ 3); { toWeierstrassCurve := WeierstrassCurve.ofJ0 R, Δ' := unitOfInvertible (-3 ^ 3), coe_Δ' := ⋯ }

theorem EllipticCurve.ofJ0_j (R : Type u) [CommRing R] [Invertible 3] : (EllipticCurve.ofJ0 R).j = 0

def EllipticCurve.ofJ1728 (R : Type u) [CommRing R] [Invertible 2] : EllipticCurve R

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

Equations

• EllipticCurve.ofJ1728 R = let_fun this := invertibleNeg (2 ^ 6); { toWeierstrassCurve := WeierstrassCurve.ofJ1728 R, Δ' := unitOfInvertible (-2 ^ 6), coe_Δ' := ⋯ }

theorem EllipticCurve.ofJ1728_j (R : Type u) [CommRing R] [Invertible 2] : (EllipticCurve.ofJ1728 R).j = 1728

def EllipticCurve.ofJ' {R : Type u} [CommRing R] (j : R) [Invertible j] [Invertible (j - 1728)] : EllipticCurve R

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

• EllipticCurve.ofJ' j = let_fun this := invertibleMul (j ^ 2) ((j - 1728) ^ 9); { toWeierstrassCurve := WeierstrassCurve.ofJ j, Δ' := unitOfInvertible (j ^ 2 * (j - 1728) ^ 9), coe_Δ' := ⋯ }

theorem EllipticCurve.ofJ'_j {R : Type u} [CommRing R] (j : R) [Invertible j] [Invertible (j - 1728)] : (EllipticCurve.ofJ' j).j = j

def EllipticCurve.ofJ {F : Type u} [Field F] (j : F) [DecidableEq F] : EllipticCurve 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

• EllipticCurve.ofJ j = if h0 : j = 0 then if h3 : 3 = 0 then EllipticCurve.ofJ1728 F else EllipticCurve.ofJ0 F else if h1728 : j = 1728 then EllipticCurve.ofJ1728 F else EllipticCurve.ofJ' j

theorem EllipticCurve.ofJ_0_of_three_ne_zero {F : Type u} [Field F] [DecidableEq F] [h3 : NeZero 3] : EllipticCurve.ofJ 0 = EllipticCurve.ofJ0 F

theorem EllipticCurve.ofJ_0_of_three_eq_zero {F : Type u} [Field F] [DecidableEq F] (h3 : 3 = 0) : EllipticCurve.ofJ 0 = EllipticCurve.ofJ1728 F

theorem EllipticCurve.ofJ_0_of_two_eq_zero {F : Type u} [Field F] [DecidableEq F] (h2 : 2 = 0) : EllipticCurve.ofJ 0 = EllipticCurve.ofJ0 F

theorem EllipticCurve.ofJ_1728_of_three_eq_zero {F : Type u} [Field F] [DecidableEq F] (h3 : 3 = 0) : EllipticCurve.ofJ 1728 = EllipticCurve.ofJ1728 F

theorem EllipticCurve.ofJ_1728_of_two_ne_zero {F : Type u} [Field F] [DecidableEq F] [h2 : NeZero 2] : EllipticCurve.ofJ 1728 = EllipticCurve.ofJ1728 F

theorem EllipticCurve.ofJ_1728_of_two_eq_zero {F : Type u} [Field F] [DecidableEq F] (h2 : 2 = 0) : EllipticCurve.ofJ 1728 = EllipticCurve.ofJ0 F

theorem EllipticCurve.ofJ_ne_0_ne_1728 {F : Type u} [Field F] (j : F) [DecidableEq F] (h0 : j ≠ 0) (h1728 : j ≠ 1728) : EllipticCurve.ofJ j = EllipticCurve.ofJ' j

theorem EllipticCurve.ofJ_j {F : Type u} [Field F] (j : F) [DecidableEq F] : (EllipticCurve.ofJ j).j = j

instance EllipticCurve.instInhabitedEllipticCurve {F : Type u} [Field F] [DecidableEq F] : Inhabited (EllipticCurve F)

Equations

• EllipticCurve.instInhabitedEllipticCurve = { default := EllipticCurve.ofJ 37 }