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

A Weierstrass curve $Y^2 + a_1XY + a_3Y = X^3 + a_2X^2 + a_4X + a_6$ with parameters $a_i$.

Instances For

    Standard quantities #

    The b₂ coefficient of a Weierstrass curve.

    Instances For

      The b₄ coefficient of a Weierstrass curve.

      Instances For

        The b₆ coefficient of a Weierstrass curve.

        Instances For

          The b₈ coefficient of a Weierstrass curve.

          Instances For

            The c₄ coefficient of a Weierstrass curve.

            Instances For

              The c₆ coefficient of a Weierstrass curve.

              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.

                Instances For

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

                  Instances For

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

                    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.

                      Instances For
                        theorem WeierstrassCurve.ofJ_Δ {R : Type u} [CommRing R] (j : R) :

                        Variable changes #

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

                        An admissible linear change of variables of Weierstrass curves defined over a ring R. It consists of a tuple $(u,r,s,t)$ of elements in $R$, with $u$ invertible. As a matrix, it is $\begin{pmatrix} u^2 & 0 & r \cr u^2s & u^3 & t \cr 0 & 0 & 1 \end{pmatrix}$.

                        Instances For

                          The identity linear change of variables. As a matrix, it is just identity matrix.

                          Instances For

                            The composition of two linear change of variables. As matrices, it is just matrix multiplcation.

                            Instances For

                              The inverse of a linear change of variables. As a matrix, it is just matrix inverse.

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

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

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

                                  Base changes #

                                  @[simp]
                                  theorem WeierstrassCurve.baseChange_a₄ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (A : Type v) [CommRing A] [Algebra R A] :
                                  (WeierstrassCurve.baseChange W A).a₄ = ↑(algebraMap R A) W.a₄
                                  @[simp]
                                  theorem WeierstrassCurve.baseChange_a₁ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (A : Type v) [CommRing A] [Algebra R A] :
                                  (WeierstrassCurve.baseChange W A).a₁ = ↑(algebraMap R A) W.a₁
                                  @[simp]
                                  theorem WeierstrassCurve.baseChange_a₆ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (A : Type v) [CommRing A] [Algebra R A] :
                                  (WeierstrassCurve.baseChange W A).a₆ = ↑(algebraMap R A) W.a₆
                                  @[simp]
                                  theorem WeierstrassCurve.baseChange_a₂ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (A : Type v) [CommRing A] [Algebra R A] :
                                  (WeierstrassCurve.baseChange W A).a₂ = ↑(algebraMap R A) W.a₂
                                  @[simp]
                                  theorem WeierstrassCurve.baseChange_a₃ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (A : Type v) [CommRing A] [Algebra R A] :
                                  (WeierstrassCurve.baseChange W A).a₃ = ↑(algebraMap R A) W.a₃

                                  The Weierstrass curve over R base changed to A.

                                  Instances For

                                    The change of variables over R base changed to A.

                                    Instances For
                                      theorem WeierstrassCurve.VariableChange.baseChange_id {R : Type u} [CommRing R] (A : Type v) [CommRing A] [Algebra R A] :
                                      WeierstrassCurve.VariableChange.baseChange A WeierstrassCurve.VariableChange.id = WeierstrassCurve.VariableChange.id

                                      The base change of change of variables over R to A is a group homomorphism.

                                      Instances For

                                        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.

                                        Instances For

                                          The notation Y for X in the PolynomialPolynomial scope.

                                          Instances For

                                            The notation R[X][Y] for R[X][X] in the PolynomialPolynomial scope.

                                            Instances For

                                              Weierstrass equations #

                                              The polynomial $W(X, Y) := Y^2 + a_1XY + a_3Y - (X^3 + a_2X^2 + a_4X + a_6)$ associated to a Weierstrass curve W over R. For ease of polynomial manipulation, this is represented as a term of type R[X][X], where the inner variable represents $X$ and the outer variable represents $Y$. For clarity, the alternative notations Y and R[X][Y] are provided in the PolynomialPolynomial scope to represent the outer variable and the bivariate polynomial ring R[X][X] respectively.

                                              Instances For
                                                theorem WeierstrassCurve.polynomial_eq {R : Type u} [CommRing R] (W : WeierstrassCurve R) :
                                                WeierstrassCurve.polynomial W = Cubic.toPoly { a := 0, b := 1, c := Cubic.toPoly { a := 0, b := 0, c := W.a₁, d := W.a₃ }, d := Cubic.toPoly { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ } }
                                                theorem WeierstrassCurve.eval_polynomial {R : Type u} [CommRing R] (W : WeierstrassCurve R) (x : R) (y : R) :
                                                Polynomial.eval x (Polynomial.eval (Polynomial.C y) (WeierstrassCurve.polynomial W)) = y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆)
                                                def WeierstrassCurve.equation {R : Type u} [CommRing R] (W : WeierstrassCurve R) (x : R) (y : R) :

                                                The proposition that an affine point $(x, y)$ lies in W. In other words, $W(x, y) = 0$.

                                                Instances For
                                                  theorem WeierstrassCurve.equation_iff' {R : Type u} [CommRing R] (W : WeierstrassCurve R) (x : R) (y : R) :
                                                  WeierstrassCurve.equation W x y y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆) = 0
                                                  theorem WeierstrassCurve.equation_iff {R : Type u} [CommRing R] (W : WeierstrassCurve R) (x : R) (y : R) :
                                                  WeierstrassCurve.equation W x y y ^ 2 + W.a₁ * x * y + W.a₃ * y = x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆

                                                  Nonsingularity of Weierstrass curves #

                                                  The partial derivative $W_X(X, Y)$ of $W(X, Y)$ with respect to $X$.

                                                  TODO: define this in terms of Polynomial.derivative.

                                                  Instances For
                                                    theorem WeierstrassCurve.eval_polynomialX {R : Type u} [CommRing R] (W : WeierstrassCurve R) (x : R) (y : R) :
                                                    Polynomial.eval x (Polynomial.eval (Polynomial.C y) (WeierstrassCurve.polynomialX W)) = W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)

                                                    The partial derivative $W_Y(X, Y)$ of $W(X, Y)$ with respect to $Y$.

                                                    TODO: define this in terms of Polynomial.derivative.

                                                    Instances For
                                                      theorem WeierstrassCurve.eval_polynomialY {R : Type u} [CommRing R] (W : WeierstrassCurve R) (x : R) (y : R) :
                                                      Polynomial.eval x (Polynomial.eval (Polynomial.C y) (WeierstrassCurve.polynomialY W)) = 2 * y + W.a₁ * x + W.a₃
                                                      def WeierstrassCurve.nonsingular {R : Type u} [CommRing R] (W : WeierstrassCurve R) (x : R) (y : R) :

                                                      The proposition that an affine point $(x, y)$ on W is nonsingular. In other words, either $W_X(x, y) \ne 0$ or $W_Y(x, y) \ne 0$.

                                                      Instances For
                                                        theorem WeierstrassCurve.nonsingular_iff' {R : Type u} [CommRing R] (W : WeierstrassCurve R) (x : R) (y : R) :
                                                        WeierstrassCurve.nonsingular W x y WeierstrassCurve.equation W x y (W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄) 0 2 * y + W.a₁ * x + W.a₃ 0)
                                                        theorem WeierstrassCurve.nonsingular_iff {R : Type u} [CommRing R] (W : WeierstrassCurve R) (x : R) (y : R) :
                                                        WeierstrassCurve.nonsingular W x y WeierstrassCurve.equation W x y (W.a₁ * y 3 * x ^ 2 + 2 * W.a₂ * x + W.a₄ y -y - W.a₁ * x - W.a₃)
                                                        @[simp]
                                                        theorem WeierstrassCurve.nonsingular_zero {R : Type u} [CommRing R] (W : WeierstrassCurve R) :
                                                        WeierstrassCurve.nonsingular W 0 0 W.a₆ = 0 (W.a₃ 0 W.a₄ 0)

                                                        A Weierstrass curve is nonsingular at every point if its discriminant is non-zero.

                                                        Ideals in the coordinate ring #

                                                        @[inline, reducible]

                                                        The coordinate ring $R[W] := R[X, Y] / \langle W(X, Y) \rangle$ of W.

                                                        Instances For
                                                          @[inline, reducible]

                                                          The function field $R(W) := \mathrm{Frac}(R[W])$ of W.

                                                          Instances For
                                                            @[inline, reducible]

                                                            An element of the coordinate ring R[W] of W over R.

                                                            Instances For

                                                              The class of the element $X - x$ in $R[W]$ for some $x \in R$.

                                                              Instances For

                                                                The class of the element $Y - y(X)$ in $R[W]$ for some $y(X) \in R[X]$.

                                                                Instances For

                                                                  The ideal $\langle X - x \rangle$ of $R[W]$ for some $x \in R$.

                                                                  Instances For

                                                                    The ideal $\langle Y - y(X) \rangle$ of $R[W]$ for some $y(X) \in R[X]$.

                                                                    Instances For

                                                                      The ideal $\langle X - x, Y - y(X) \rangle$ of $R[W]$ for some $x \in R$ and $y(X) \in R[X]$.

                                                                      Instances For

                                                                        The coordinate ring as an R[X]-algebra #

                                                                        noncomputable def WeierstrassCurve.CoordinateRing.quotientXYIdealEquiv' {R : Type u} [CommRing R] (W : WeierstrassCurve R) {x : R} {y : Polynomial R} (h : Polynomial.eval x (Polynomial.eval y (WeierstrassCurve.polynomial W)) = 0) :
                                                                        (WeierstrassCurve.CoordinateRing W WeierstrassCurve.CoordinateRing.XYIdeal W x y) ≃ₐ[R] Polynomial (Polynomial R) Ideal.span {Polynomial.C (Polynomial.X - Polynomial.C x), Polynomial.X - Polynomial.C y}

                                                                        The $R$-algebra isomorphism from $R[W] / \langle X - x, Y - y(X) \rangle$ to $R[X, Y] / \langle X - x, Y - y(X) \rangle$ provided that $W(x, y(x)) = 0$.

                                                                        Instances For

                                                                          The $R$-algebra isomorphism from $R[W] / \langle X - x, Y - y(X) \rangle$ to $R$ obtained by evaluation at $y(X)$ and at $x$ provided that $W(x, y(x)) = 0$.

                                                                          Instances For

                                                                            The basis ${1, Y}$ for the coordinate ring $R[W]$ over the polynomial ring $R[X]$.

                                                                            Instances For
                                                                              theorem WeierstrassCurve.CoordinateRing.smul_basis_eq_zero {R : Type u} [CommRing R] {W : WeierstrassCurve R} {p : Polynomial R} {q : Polynomial R} (hpq : p 1 + q ↑(WeierstrassCurve.CoordinateRing.mk W) Polynomial.X = 0) :
                                                                              p = 0 q = 0
                                                                              theorem WeierstrassCurve.CoordinateRing.smul_basis_mul_C {R : Type u} [CommRing R] (W : WeierstrassCurve R) (y : Polynomial R) (p : Polynomial R) (q : Polynomial R) :
                                                                              (p 1 + q ↑(WeierstrassCurve.CoordinateRing.mk W) Polynomial.X) * ↑(WeierstrassCurve.CoordinateRing.mk W) (Polynomial.C y) = (p * y) 1 + (q * y) ↑(WeierstrassCurve.CoordinateRing.mk W) Polynomial.X
                                                                              theorem WeierstrassCurve.CoordinateRing.smul_basis_mul_Y {R : Type u} [CommRing R] (W : WeierstrassCurve R) (p : Polynomial R) (q : Polynomial R) :
                                                                              (p 1 + q ↑(WeierstrassCurve.CoordinateRing.mk W) Polynomial.X) * ↑(WeierstrassCurve.CoordinateRing.mk W) Polynomial.X = (q * (Polynomial.X ^ 3 + Polynomial.C W.a₂ * Polynomial.X ^ 2 + Polynomial.C W.a₄ * Polynomial.X + Polynomial.C W.a₆)) 1 + (p - q * (Polynomial.C W.a₁ * Polynomial.X + Polynomial.C W.a₃)) ↑(WeierstrassCurve.CoordinateRing.mk W) Polynomial.X

                                                                              Norms on the coordinate ring #

                                                                              theorem WeierstrassCurve.CoordinateRing.norm_smul_basis {R : Type u} [CommRing R] (W : WeierstrassCurve R) (p : Polynomial R) (q : Polynomial R) :
                                                                              ↑(Algebra.norm (Polynomial R)) (p 1 + q ↑(WeierstrassCurve.CoordinateRing.mk W) Polynomial.X) = p ^ 2 - p * q * (Polynomial.C W.a₁ * Polynomial.X + Polynomial.C W.a₃) - q ^ 2 * (Polynomial.X ^ 3 + Polynomial.C W.a₂ * Polynomial.X ^ 2 + Polynomial.C W.a₄ * Polynomial.X + Polynomial.C W.a₆)
                                                                              theorem WeierstrassCurve.CoordinateRing.coe_norm_smul_basis {R : Type u} [CommRing R] (W : WeierstrassCurve R) (p : Polynomial R) (q : Polynomial R) :
                                                                              ↑(AdjoinRoot.of (WeierstrassCurve.polynomial W)) (↑(Algebra.norm (Polynomial R)) (p 1 + q ↑(WeierstrassCurve.CoordinateRing.mk W) Polynomial.X)) = ↑(WeierstrassCurve.CoordinateRing.mk W) ((Polynomial.C p + Polynomial.C q * Polynomial.X) * (Polynomial.C p + Polynomial.C q * (-Polynomial.X - Polynomial.C (Polynomial.C W.a₁ * Polynomial.X + Polynomial.C W.a₃))))

                                                                              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 :
                                                                              • 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_Δ' : s.Δ' = WeierstrassCurve.Δ s.toWeierstrassCurve

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

                                                                              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.

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

                                                                                Instances For
                                                                                  theorem EllipticCurve.nonsingular {R : Type u} [CommRing R] (E : EllipticCurve R) [Nontrivial R] {x : R} {y : R} (h : WeierstrassCurve.equation E.toWeierstrassCurve x y) :
                                                                                  WeierstrassCurve.nonsingular E.toWeierstrassCurve x y

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

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

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

                                                                                      Instances For
                                                                                        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').

                                                                                        Instances For
                                                                                          theorem EllipticCurve.ofJ_ne_0_ne_1728 {F : Type u} [Field F] (j : F) [DecidableEq F] (h0 : j 0) (h1728 : j 1728) :

                                                                                          Variable changes #

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

                                                                                          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.

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

                                                                                            Base changes #

                                                                                            @[simp]
                                                                                            theorem EllipticCurve.baseChange_a₃ {R : Type u} [CommRing R] (E : EllipticCurve R) (A : Type v) [CommRing A] [Algebra R A] :
                                                                                            (EllipticCurve.baseChange E A).toWeierstrassCurve.a₃ = ↑(algebraMap R A) E.a₃
                                                                                            @[simp]
                                                                                            theorem EllipticCurve.baseChange_toWeierstrassCurve {R : Type u} [CommRing R] (E : EllipticCurve R) (A : Type v) [CommRing A] [Algebra R A] :
                                                                                            (EllipticCurve.baseChange E A).toWeierstrassCurve = WeierstrassCurve.baseChange E.toWeierstrassCurve A
                                                                                            @[simp]
                                                                                            theorem EllipticCurve.baseChange_a₂ {R : Type u} [CommRing R] (E : EllipticCurve R) (A : Type v) [CommRing A] [Algebra R A] :
                                                                                            (EllipticCurve.baseChange E A).toWeierstrassCurve.a₂ = ↑(algebraMap R A) E.a₂
                                                                                            @[simp]
                                                                                            theorem EllipticCurve.baseChange_Δ' {R : Type u} [CommRing R] (E : EllipticCurve R) (A : Type v) [CommRing A] [Algebra R A] :
                                                                                            (EllipticCurve.baseChange E A).Δ' = ↑(Units.map ↑(algebraMap R A)) E.Δ'
                                                                                            @[simp]
                                                                                            theorem EllipticCurve.baseChange_a₄ {R : Type u} [CommRing R] (E : EllipticCurve R) (A : Type v) [CommRing A] [Algebra R A] :
                                                                                            (EllipticCurve.baseChange E A).toWeierstrassCurve.a₄ = ↑(algebraMap R A) E.a₄
                                                                                            @[simp]
                                                                                            theorem EllipticCurve.baseChange_a₆ {R : Type u} [CommRing R] (E : EllipticCurve R) (A : Type v) [CommRing A] [Algebra R A] :
                                                                                            (EllipticCurve.baseChange E A).toWeierstrassCurve.a₆ = ↑(algebraMap R A) E.a₆
                                                                                            @[simp]
                                                                                            theorem EllipticCurve.baseChange_a₁ {R : Type u} [CommRing R] (E : EllipticCurve R) (A : Type v) [CommRing A] [Algebra R A] :
                                                                                            (EllipticCurve.baseChange E A).toWeierstrassCurve.a₁ = ↑(algebraMap R A) E.a₁

                                                                                            The elliptic curve over R base changed to A.

                                                                                            Instances For
                                                                                              theorem EllipticCurve.coeBaseChange_Δ' {R : Type u} [CommRing R] (E : EllipticCurve R) (A : Type v) [CommRing A] [Algebra R A] :
                                                                                              (EllipticCurve.baseChange E A).Δ' = ↑(algebraMap R A) E.Δ'