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

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.

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] (φ : 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₆ }

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

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

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

structure EllipticCurve (R : Type u) [CommRing R] extends WeierstrassCurve R : 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.toWeierstrassCurve_injective {R : Type u} [CommRing R] : Function.Injective EllipticCurve.toWeierstrassCurve

theorem EllipticCurve.ext {R : Type u} [CommRing R] {x y : EllipticCurve R} (h₁ : x.a₁ = y.a₁) (h₂ : x.a₂ = y.a₂) (h₃ : x.a₃ = y.a₃) (h₄ : x.a₄ = y.a₄) (h₆ : x.a₆ = y.a₆) : x = y

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.j_eq_zero_iff' {R : Type u} [CommRing R] (E : EllipticCurve R) : E.j = 0 ↔ E.c₄ ^ 3 = 0

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Maps and base changes

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_Δ' := ⋯ }

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

@[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 = { 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 = { 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 = { 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 }