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² + a₁XY + a₃Y = X³ + a₂X² + a₄X + a₆ for some aᵢ 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.map: the Weierstrass curve mapped over a ring homomorphism.
• WeierstrassCurve.twoTorsionPolynomial: the 2-torsion polynomial of a Weierstrass curve.
• WeierstrassCurve.IsElliptic: typeclass asserting that a Weierstrass curve is an elliptic curve.
• WeierstrassCurve.j: the j-invariant of an elliptic curve.

Main statements

• WeierstrassCurve.twoTorsionPolynomial_disc: the discriminant of a Weierstrass curve is a constant factor of the cubic discriminant of its 2-torsion polynomial.

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 Spec(R) of R in the case that R has trivial Picard group 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 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
• P Deligne, Courbes Elliptiques: Formulaire (d'après J. Tate)
• J Silverman, The Arithmetic of Elliptic Curves

Tags

elliptic curve, weierstrass equation, j invariant

Weierstrass curves

structure WeierstrassCurve (R : Type u) : Type u

A Weierstrass curve Y² + a₁XY + a₃Y = X³ + a₂X² + a₄X + a₆ with parameters aᵢ.

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

theorem WeierstrassCurve.ext {R : Type u} {x 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

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

Equations

• WeierstrassCurve.instInhabited = { 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

theorem WeierstrassCurve.b₂_of_char_two {R : Type u} [CommRing R] (W : WeierstrassCurve R) [CharP R 2] : W.b₂ = W.a₁ ^ 2

theorem WeierstrassCurve.b₄_of_char_two {R : Type u} [CommRing R] (W : WeierstrassCurve R) [CharP R 2] : W.b₄ = W.a₁ * W.a₃

theorem WeierstrassCurve.b₆_of_char_two {R : Type u} [CommRing R] (W : WeierstrassCurve R) [CharP R 2] : W.b₆ = W.a₃ ^ 2

theorem WeierstrassCurve.b₈_of_char_two {R : Type u} [CommRing R] (W : WeierstrassCurve R) [CharP R 2] : W.b₈ = W.a₁ ^ 2 * W.a₆ + W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 + W.a₄ ^ 2

theorem WeierstrassCurve.c₄_of_char_two {R : Type u} [CommRing R] (W : WeierstrassCurve R) [CharP R 2] : W.c₄ = W.a₁ ^ 4

theorem WeierstrassCurve.c₆_of_char_two {R : Type u} [CommRing R] (W : WeierstrassCurve R) [CharP R 2] : W.c₆ = W.a₁ ^ 6

theorem WeierstrassCurve.Δ_of_char_two {R : Type u} [CommRing R] (W : WeierstrassCurve R) [CharP R 2] : W.Δ = W.a₁ ^ 4 * W.b₈ + W.a₃ ^ 4 + W.a₁ ^ 3 * W.a₃ ^ 3

theorem WeierstrassCurve.b_relation_of_char_two {R : Type u} [CommRing R] (W : WeierstrassCurve R) [CharP R 2] : W.b₂ * W.b₆ = W.b₄ ^ 2

theorem WeierstrassCurve.c_relation_of_char_two {R : Type u} [CommRing R] (W : WeierstrassCurve R) [CharP R 2] : W.c₄ ^ 3 = W.c₆ ^ 2

theorem WeierstrassCurve.b₂_of_char_three {R : Type u} [CommRing R] (W : WeierstrassCurve R) [CharP R 3] : W.b₂ = W.a₁ ^ 2 + W.a₂

theorem WeierstrassCurve.b₄_of_char_three {R : Type u} [CommRing R] (W : WeierstrassCurve R) [CharP R 3] : W.b₄ = -W.a₄ + W.a₁ * W.a₃

theorem WeierstrassCurve.b₆_of_char_three {R : Type u} [CommRing R] (W : WeierstrassCurve R) [CharP R 3] : W.b₆ = W.a₃ ^ 2 + W.a₆

theorem WeierstrassCurve.b₈_of_char_three {R : Type u} [CommRing R] (W : WeierstrassCurve R) [CharP R 3] : W.b₈ = W.a₁ ^ 2 * W.a₆ + W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2

theorem WeierstrassCurve.c₄_of_char_three {R : Type u} [CommRing R] (W : WeierstrassCurve R) [CharP R 3] : W.c₄ = W.b₂ ^ 2

theorem WeierstrassCurve.c₆_of_char_three {R : Type u} [CommRing R] (W : WeierstrassCurve R) [CharP R 3] : W.c₆ = -W.b₂ ^ 3

theorem WeierstrassCurve.Δ_of_char_three {R : Type u} [CommRing R] (W : WeierstrassCurve R) [CharP R 3] : W.Δ = -W.b₂ ^ 2 * W.b₈ - 8 * W.b₄ ^ 3

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

theorem WeierstrassCurve.c_relation_of_char_three {R : Type u} [CommRing R] (W : WeierstrassCurve R) [CharP R 3] : W.c₄ ^ 3 = W.c₆ ^ 2

Maps and base changes

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

The Weierstrass curve mapped over a ring homomorphism f : R →+* A.

Equations

• W.map f = { a₁ := f W.a₁, a₂ := f W.a₂, a₃ := f W.a₃, a₄ := f W.a₄, a₆ := f W.a₆ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem WeierstrassCurve.map_a₆ {R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (f : R →+* A) : (W.map f).a₆ = f 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] (f : R →+* A) : (W.map f).b₂ = f W.b₂

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem WeierstrassCurve.map_Δ {R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (f : R →+* A) : (W.map f).Δ = f 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] (f : R →+* A) {B : Type w} [CommRing B] (g : A →+* B) : (W.map f).map g = W.map (g.comp f)

@[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] (g : A →ₐ[S] B) : (W.baseChange A).map ↑g = W.baseChange B

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

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_of_char_two {R : Type u} [CommRing R] (W : WeierstrassCurve R) [CharP R 2] : W.twoTorsionPolynomial = { a := 0, b := W.b₂, c := 0, d := W.b₆ }

theorem WeierstrassCurve.twoTorsionPolynomial_disc_of_char_two {R : Type u} [CommRing R] (W : WeierstrassCurve R) [CharP R 2] : W.twoTorsionPolynomial.disc = 0

theorem WeierstrassCurve.twoTorsionPolynomial_of_char_three {R : Type u} [CommRing R] (W : WeierstrassCurve R) [CharP R 3] : W.twoTorsionPolynomial = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }

theorem WeierstrassCurve.twoTorsionPolynomial_disc_of_char_three {R : Type u} [CommRing R] (W : WeierstrassCurve R) [CharP R 3] : W.twoTorsionPolynomial.disc = W.Δ

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

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

Elliptic curves

class WeierstrassCurve.IsElliptic {R : Type u} [CommRing R] (W : WeierstrassCurve R) : Prop

WeierstrassCurve.IsElliptic is a typeclass which asserts that a Weierstrass curve is an elliptic curve: that its discriminant is a unit. 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.

• isUnit : IsUnit W.Δ

theorem WeierstrassCurve.isElliptic_iff {R : Type u} [CommRing R] (W : WeierstrassCurve R) : W.IsElliptic ↔ IsUnit W.Δ

theorem WeierstrassCurve.isUnit_Δ {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] : IsUnit W.Δ

noncomputable def WeierstrassCurve.Δ' {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] : Rˣ

The discriminant Δ' of an elliptic curve over R, which is given as a unit in R. Note that to prove two equal elliptic curves have the same Δ', you need to use simp_rw, as rw cannot transfer instance WeierstrassCurve.IsElliptic automatically.

Equations

• W.Δ' = ⋯.unit

@[simp]

theorem WeierstrassCurve.coe_Δ' {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] : ↑W.Δ' = W.Δ

The discriminant Δ' of an elliptic curve is equal to the discriminant Δ of it as a Weierstrass curve.

noncomputable def WeierstrassCurve.j {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] : R

The j-invariant j of an elliptic curve, which is invariant under isomorphisms over R. Note that to prove two equal elliptic curves have the same j, you need to use simp_rw, as rw cannot transfer instance WeierstrassCurve.IsElliptic automatically.

Equations

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

theorem WeierstrassCurve.j_eq_zero_iff' {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] : W.j = 0 ↔ W.c₄ ^ 3 = 0

A variant of WeierstrassCurve.j_eq_zero_iff without assuming a reduced ring.

theorem WeierstrassCurve.j_eq_zero {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] (h : W.c₄ = 0) : W.j = 0

theorem WeierstrassCurve.j_eq_zero_iff {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] [IsReduced R] : W.j = 0 ↔ W.c₄ = 0

theorem WeierstrassCurve.j_of_char_two {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] [CharP R 2] : W.j = ↑W.Δ'⁻¹ * W.a₁ ^ 12

theorem WeierstrassCurve.j_eq_zero_iff_of_char_two' {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] [CharP R 2] : W.j = 0 ↔ W.a₁ ^ 12 = 0

A variant of WeierstrassCurve.j_eq_zero_iff_of_char_two without assuming a reduced ring.

theorem WeierstrassCurve.j_eq_zero_of_char_two {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] [CharP R 2] (h : W.a₁ = 0) : W.j = 0

theorem WeierstrassCurve.j_eq_zero_iff_of_char_two {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] [CharP R 2] [IsReduced R] : W.j = 0 ↔ W.a₁ = 0

theorem WeierstrassCurve.j_of_char_three {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] [CharP R 3] : W.j = ↑W.Δ'⁻¹ * W.b₂ ^ 6

theorem WeierstrassCurve.j_eq_zero_iff_of_char_three' {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] [CharP R 3] : W.j = 0 ↔ W.b₂ ^ 6 = 0

A variant of WeierstrassCurve.j_eq_zero_iff_of_char_three without assuming a reduced ring.

theorem WeierstrassCurve.j_eq_zero_of_char_three {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] [CharP R 3] (h : W.b₂ = 0) : W.j = 0

theorem WeierstrassCurve.j_eq_zero_iff_of_char_three {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] [CharP R 3] [IsReduced R] : W.j = 0 ↔ W.b₂ = 0

theorem WeierstrassCurve.twoTorsionPolynomial_disc_ne_zero_of_isElliptic {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] [Nontrivial R] (hu : IsUnit 2) : W.twoTorsionPolynomial.disc ≠ 0

Maps and base changes

instance WeierstrassCurve.instIsEllipticMap {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {A : Type v} [CommRing A] (f : R →+* A) : (W.map f).IsElliptic

theorem WeierstrassCurve.coe_map_Δ' {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {A : Type v} [CommRing A] (f : R →+* A) : ↑(W.map f).Δ' = f ↑W.Δ'

@[simp]

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

theorem WeierstrassCurve.coe_inv_map_Δ' {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {A : Type v} [CommRing A] (f : R →+* A) : ↑(W.map f).Δ'⁻¹ = f ↑W.Δ'⁻¹

theorem WeierstrassCurve.inv_map_Δ' {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {A : Type v} [CommRing A] (f : R →+* A) : (W.map f).Δ'⁻¹ = (Units.map ↑f) W.Δ'⁻¹

@[simp]

theorem WeierstrassCurve.map_j {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {A : Type v} [CommRing A] (f : R →+* A) : (W.map f).j = f W.j