Documentation

Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Weierstrass equations of elliptic curves #

This file defines the structure of an elliptic curve as a nonsingular Weierstrass curve given by a Weierstrass equation, which is mathematically accurate in many cases but also good for computation.

Mathematical background #

Let S be a scheme. The actual category of elliptic curves over S is a large category, whose objects are schemes E equipped with a map E → S, a section S → E, and some axioms (the map is smooth and proper and the fibres are geometrically-connected one-dimensional group varieties). In the special case where S is the spectrum of some commutative ring R whose Picard group is zero (this includes all fields, all PIDs, and many other commutative rings) it can be shown (using a lot of algebro-geometric machinery) that every elliptic curve E is a projective plane cubic isomorphic to a Weierstrass curve given by the equation $Y^2 + a_1XY + a_3Y = X^3 + a_2X^2 + a_4X + a_6$ for some $a_i$ in R, and such that a certain quantity called the discriminant of E is a unit in R. If R is a field, this quantity divides the discriminant of a cubic polynomial whose roots over a splitting field of R are precisely the $X$-coordinates of the non-zero 2-torsion points of E.

Main definitions #

Main statements #

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 #

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

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
    Equations
    • WeierstrassCurve.instInhabited = { default := { a₁ := default, a₂ := default, a₃ := default, a₄ := default, a₆ := default } }

    Standard quantities #

    The b₂ coefficient of a Weierstrass curve.

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

      The b₄ coefficient of a Weierstrass curve.

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

        The b₆ coefficient of a Weierstrass curve.

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

          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} [CommRing R] (W : WeierstrassCurve R) :
            4 * W.b₈ = W.b₂ * W.b₆ - W.b₄ ^ 2

            The c₄ coefficient of a Weierstrass curve.

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

              The c₆ coefficient of a Weierstrass curve.

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

                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} [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 #

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

                  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]

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

                    Equations
                    Instances For
                      @[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 #

                      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} [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 #

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

                        Equations
                        Instances For

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

                          Equations
                          Instances For

                            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
                            Instances For
                              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 :

                              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} [CommRing R] (self : EllipticCurve R) :
                                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_iff {R : Type u} [CommRing R] {x : EllipticCurve R} {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₆
                                theorem EllipticCurve.ext {R : Type u} [CommRing R] {x : EllipticCurve R} {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
                                Instances For
                                  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 #

                                  @[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_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_Δ' {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) :

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

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

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

                                    Equations
                                    Instances For
                                      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 #

                                      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

                                        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
                                          def EllipticCurve.ofJ' {R : Type u} [CommRing R] (j : R) [Invertible j] [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} [CommRing R] (j : R) [Invertible j] [Invertible (j - 1728)] :
                                            def EllipticCurve.ofJ {F : Type u} [Field F] (j : F) [DecidableEq 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
                                            Instances For
                                              theorem EllipticCurve.ofJ_ne_0_ne_1728 {F : Type u} [Field F] (j : F) [DecidableEq F] (h0 : j 0) (h1728 : j 1728) :
                                              theorem EllipticCurve.ofJ_j {F : Type u} [Field F] (j : F) [DecidableEq F] :
                                              Equations