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, WeierstrassCurve.ofJ1728, WeierstrassCurve.ofJ: Weierstrass curves whose $j$-invariants are $0$, $1728$ and $j\neq 0,1728$, respectively.
• WeierstrassCurve.VariableChange: a change of variables of Weierstrass curves.
• WeierstrassCurve.variableChange: the Weierstrass curve induced by a change of variables.
• WeierstrassCurve.baseChange: the Weierstrass curve base changed over an algebra.
• WeierstrassCurve.twoTorsionPolynomial: the 2-torsion polynomial of a Weierstrass curve.
• WeierstrassCurve.polynomial: the polynomial associated to a Weierstrass curve.
• WeierstrassCurve.equation: the Weierstrass equation of a Weierstrass curve.
• WeierstrassCurve.nonsingular: the nonsingular condition at a point on a Weierstrass curve.
• WeierstrassCurve.CoordinateRing: the coordinate ring of a Weierstrass curve.
• WeierstrassCurve.FunctionField: the function field of a Weierstrass curve.
• WeierstrassCurve.CoordinateRing.basis: the power basis of the coordinate ring over R[X].
• EllipticCurve: an elliptic curve over a commutative ring.
• EllipticCurve.j: the j-invariant of an elliptic curve.
• EllipticCurve.ofJ0, EllipticCurve.ofJ1728, EllipticCurve.ofJ': elliptic curves whose $j$-invariants are $0$, $1728$ and $j\neq 0,1728$, respectively.
• EllipticCurve.ofJ: an elliptic curve over a field $F$, 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.
• WeierstrassCurve.nonsingular_of_Δ_ne_zero: a Weierstrass curve is nonsingular at every point if its discriminant is non-zero.
• WeierstrassCurve.CoordinateRing.instIsDomainCoordinateRing: the coordinate ring of a Weierstrass curve is an integral domain.
• WeierstrassCurve.CoordinateRing.degree_norm_smul_basis: the degree of the norm of an element in the coordinate ring in terms of the power basis.
• EllipticCurve.nonsingular: an elliptic curve is nonsingular at every point.
• EllipticCurve.variableChange_j: the j-invariant of an elliptic curve is invariant under an admissible linear change of variables.
• EllipticCurve.ofJ_j: the $j$-invariant of EllipticCurve.ofJ is equal to $j$.

Implementation notes

The definition of elliptic curves in this file makes sense for all commutative rings R, but it only gives a type which can be beefed up to a category which is equivalent to the category of elliptic curves over the spectrum $\mathrm{Spec}(R)$ of R in the case that R has trivial Picard group $\mathrm{Pic}(R)$ or, slightly more generally, when its 12-torsion is trivial. The issue is that for a general ring R, there might be elliptic curves over $\mathrm{Spec}(R)$ in the sense of algebraic geometry which are not globally defined by a cubic equation valid over the entire base.

References

• [N Katz and B Mazur, Arithmetic Moduli of Elliptic Curves][katz_mazur]
• [P Deligne, Courbes Elliptiques: Formulaire (d'après J. Tate)][deligne_formulaire]
• [J Silverman, The Arithmetic of Elliptic Curves][silverman2009]

Tags

elliptic curve, weierstrass equation, j invariant

Weierstrass curves

theorem WeierstrassCurve.ext {R : Type u} (x : WeierstrassCurve R) (y : WeierstrassCurve R) (a₁ : x.a₁ = y.a₁) (a₂ : x.a₂ = y.a₂) (a₃ : x.a₃ = y.a₃) (a₄ : x.a₄ = y.a₄) (a₆ : x.a₆ = y.a₆) : x = y

theorem WeierstrassCurve.ext_iff {R : Type u} (x : WeierstrassCurve R) (y : WeierstrassCurve R) : x = y ↔ x.a₁ = y.a₁ ∧ x.a₂ = y.a₂ ∧ x.a₃ = y.a₃ ∧ x.a₄ = y.a₄ ∧ x.a₆ = y.a₆

structure WeierstrassCurve (R : Type u) : Type u

• a₁ : 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$.

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

Standard quantities

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

The b₂ coefficient of a Weierstrass curve.

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

The b₄ coefficient of a Weierstrass curve.

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

The b₆ coefficient of a Weierstrass curve.

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

The b₈ coefficient of a Weierstrass curve.

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

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

The c₄ coefficient of a Weierstrass curve.

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

The c₆ coefficient of a Weierstrass curve.

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.

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

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.

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

theorem WeierstrassCurve.ofJ0_Δ (R : Type u) [CommRing R] : WeierstrassCurve.Δ (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.

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

theorem WeierstrassCurve.ofJ1728_Δ (R : Type u) [CommRing R] : WeierstrassCurve.Δ (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.

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

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

Variable changes

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

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

structure WeierstrassCurve.VariableChange (R : Type u) [CommRing R] : Type u

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

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

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

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

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

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

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

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

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

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

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

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

@[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⁻¹ * (W.a₁ + 2 * C.s)

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

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

The Weierstrass curve over R induced by an admissible linear change of variables $(X, Y) \mapsto (u^2X + r, u^3Y + u^2sX + t)$ for some $u \in R^\times$ and some $r, s, t \in R$.

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The Weierstrass curve over R base changed to A.

@[simp]

theorem WeierstrassCurve.baseChange_b₂ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (A : Type v) [CommRing A] [Algebra R A] : WeierstrassCurve.b₂ (WeierstrassCurve.baseChange W A) = ↑(algebraMap R A) (WeierstrassCurve.b₂ W)

@[simp]

theorem WeierstrassCurve.baseChange_b₄ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (A : Type v) [CommRing A] [Algebra R A] : WeierstrassCurve.b₄ (WeierstrassCurve.baseChange W A) = ↑(algebraMap R A) (WeierstrassCurve.b₄ W)

@[simp]

theorem WeierstrassCurve.baseChange_b₆ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (A : Type v) [CommRing A] [Algebra R A] : WeierstrassCurve.b₆ (WeierstrassCurve.baseChange W A) = ↑(algebraMap R A) (WeierstrassCurve.b₆ W)

@[simp]

theorem WeierstrassCurve.baseChange_b₈ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (A : Type v) [CommRing A] [Algebra R A] : WeierstrassCurve.b₈ (WeierstrassCurve.baseChange W A) = ↑(algebraMap R A) (WeierstrassCurve.b₈ W)

@[simp]

theorem WeierstrassCurve.baseChange_c₄ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (A : Type v) [CommRing A] [Algebra R A] : WeierstrassCurve.c₄ (WeierstrassCurve.baseChange W A) = ↑(algebraMap R A) (WeierstrassCurve.c₄ W)

@[simp]

theorem WeierstrassCurve.baseChange_c₆ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (A : Type v) [CommRing A] [Algebra R A] : WeierstrassCurve.c₆ (WeierstrassCurve.baseChange W A) = ↑(algebraMap R A) (WeierstrassCurve.c₆ W)

@[simp]

theorem WeierstrassCurve.baseChange_Δ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (A : Type v) [CommRing A] [Algebra R A] : WeierstrassCurve.Δ (WeierstrassCurve.baseChange W A) = ↑(algebraMap R A) (WeierstrassCurve.Δ W)

theorem WeierstrassCurve.baseChange_self {R : Type u} [CommRing R] (W : WeierstrassCurve R) : WeierstrassCurve.baseChange W R = W

theorem WeierstrassCurve.baseChange_baseChange {R : Type u} [CommRing R] (W : WeierstrassCurve R) (A : Type v) [CommRing A] [Algebra R A] (B : Type w) [CommRing B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] : WeierstrassCurve.baseChange (WeierstrassCurve.baseChange W A) B = WeierstrassCurve.baseChange W B

theorem WeierstrassCurve.baseChange_injective {R : Type u} [CommRing R] (A : Type v) [CommRing A] [Algebra R A] (h : Function.Injective ↑(algebraMap R A)) : Function.Injective fun W => WeierstrassCurve.baseChange W A

@[simp]

theorem WeierstrassCurve.VariableChange.baseChange_r {R : Type u} [CommRing R] (A : Type v) [CommRing A] [Algebra R A] (C : WeierstrassCurve.VariableChange R) : (WeierstrassCurve.VariableChange.baseChange A C).r = ↑(algebraMap R A) C.r

@[simp]

theorem WeierstrassCurve.VariableChange.baseChange_s {R : Type u} [CommRing R] (A : Type v) [CommRing A] [Algebra R A] (C : WeierstrassCurve.VariableChange R) : (WeierstrassCurve.VariableChange.baseChange A C).s = ↑(algebraMap R A) C.s

@[simp]

theorem WeierstrassCurve.VariableChange.baseChange_t {R : Type u} [CommRing R] (A : Type v) [CommRing A] [Algebra R A] (C : WeierstrassCurve.VariableChange R) : (WeierstrassCurve.VariableChange.baseChange A C).t = ↑(algebraMap R A) C.t

@[simp]

theorem WeierstrassCurve.VariableChange.baseChange_u {R : Type u} [CommRing R] (A : Type v) [CommRing A] [Algebra R A] (C : WeierstrassCurve.VariableChange R) : (WeierstrassCurve.VariableChange.baseChange A C).u = ↑(Units.map ↑(algebraMap R A)) C.u

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

The change of variables over R base changed to A.

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

theorem WeierstrassCurve.VariableChange.baseChange_comp {R : Type u} [CommRing R] (A : Type v) [CommRing A] [Algebra R A] (C : WeierstrassCurve.VariableChange R) (C' : WeierstrassCurve.VariableChange R) : WeierstrassCurve.VariableChange.baseChange A (WeierstrassCurve.VariableChange.comp C C') = WeierstrassCurve.VariableChange.comp (WeierstrassCurve.VariableChange.baseChange A C) (WeierstrassCurve.VariableChange.baseChange A C')

def WeierstrassCurve.VariableChange.baseChangeMap {R : Type u} [CommRing R] (A : Type v) [CommRing A] [Algebra R A] : WeierstrassCurve.VariableChange R →* WeierstrassCurve.VariableChange A

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

theorem WeierstrassCurve.VariableChange.baseChange_self {R : Type u} [CommRing R] (C : WeierstrassCurve.VariableChange R) : WeierstrassCurve.VariableChange.baseChange R C = C

theorem WeierstrassCurve.VariableChange.baseChange_baseChange {R : Type u} [CommRing R] (A : Type v) [CommRing A] [Algebra R A] (B : Type w) [CommRing B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] (C : WeierstrassCurve.VariableChange R) : WeierstrassCurve.VariableChange.baseChange B (WeierstrassCurve.VariableChange.baseChange A C) = WeierstrassCurve.VariableChange.baseChange B C

theorem WeierstrassCurve.VariableChange.baseChange_injective {R : Type u} [CommRing R] (A : Type v) [CommRing A] [Algebra R A] (h : Function.Injective ↑(algebraMap R A)) : Function.Injective (WeierstrassCurve.VariableChange.baseChange A)

theorem WeierstrassCurve.baseChange_variableChange {R : Type u} [CommRing R] (W : WeierstrassCurve R) (A : Type v) [CommRing A] [Algebra R A] (C : WeierstrassCurve.VariableChange R) : WeierstrassCurve.variableChange (WeierstrassCurve.baseChange W A) (WeierstrassCurve.VariableChange.baseChange A C) = WeierstrassCurve.baseChange (WeierstrassCurve.variableChange W C) A

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.

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

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

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

def PolynomialPolynomial.termY : Lean.ParserDescr

The notation Y for X in the PolynomialPolynomial scope.

def PolynomialPolynomial.«term_[X][Y]» : Lean.TrailingParserDescr

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

Weierstrass equations

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

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.

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.polynomial_ne_zero {R : Type u} [CommRing R] (W : WeierstrassCurve R) [Nontrivial R] : WeierstrassCurve.polynomial W ≠ 0

@[simp]

theorem WeierstrassCurve.degree_polynomial {R : Type u} [CommRing R] (W : WeierstrassCurve R) [Nontrivial R] : Polynomial.degree (WeierstrassCurve.polynomial W) = 2

@[simp]

theorem WeierstrassCurve.natDegree_polynomial {R : Type u} [CommRing R] (W : WeierstrassCurve R) [Nontrivial R] : Polynomial.natDegree (WeierstrassCurve.polynomial W) = 2

theorem WeierstrassCurve.monic_polynomial {R : Type u} [CommRing R] (W : WeierstrassCurve R) : Polynomial.Monic (WeierstrassCurve.polynomial W)

theorem WeierstrassCurve.irreducible_polynomial {R : Type u} [CommRing R] (W : WeierstrassCurve R) [IsDomain R] : Irreducible (WeierstrassCurve.polynomial W)

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

@[simp]

theorem WeierstrassCurve.eval_polynomial_zero {R : Type u} [CommRing R] (W : WeierstrassCurve R) : Polynomial.eval 0 (Polynomial.eval 0 (WeierstrassCurve.polynomial W)) = -W.a₆

def WeierstrassCurve.equation {R : Type u} [CommRing R] (W : WeierstrassCurve R) (x : R) (y : R) : Prop

The proposition that an affine point $(x, y)$ lies in W. In other words, $W(x, y) = 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₆) = 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₆

@[simp]

theorem WeierstrassCurve.equation_zero {R : Type u} [CommRing R] (W : WeierstrassCurve R) : WeierstrassCurve.equation W 0 0 ↔ W.a₆ = 0

theorem WeierstrassCurve.equation_iff_variableChange {R : Type u} [CommRing R] (W : WeierstrassCurve R) (x : R) (y : R) : WeierstrassCurve.equation W x y ↔ WeierstrassCurve.equation (WeierstrassCurve.variableChange W { u := 1, r := x, s := 0, t := y }) 0 0

theorem WeierstrassCurve.equation_iff_baseChange {R : Type u} [CommRing R] (W : WeierstrassCurve R) (A : Type v) [CommRing A] [Algebra R A] [Nontrivial A] [NoZeroSMulDivisors R A] (x : R) (y : R) : WeierstrassCurve.equation W x y ↔ WeierstrassCurve.equation (WeierstrassCurve.baseChange W A) (↑(algebraMap R A) x) (↑(algebraMap R A) y)

theorem WeierstrassCurve.equation_iff_baseChange_of_baseChange {R : Type u} [CommRing R] (W : WeierstrassCurve R) (A : Type v) [CommRing A] [Algebra R A] (B : Type w) [CommRing B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] [Nontrivial B] [NoZeroSMulDivisors A B] (x : A) (y : A) : WeierstrassCurve.equation (WeierstrassCurve.baseChange W A) x y ↔ WeierstrassCurve.equation (WeierstrassCurve.baseChange W B) (↑(algebraMap A B) x) (↑(algebraMap A B) y)

Nonsingularity of Weierstrass curves

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

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

TODO: define this in terms of Polynomial.derivative.

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

@[simp]

theorem WeierstrassCurve.eval_polynomialX_zero {R : Type u} [CommRing R] (W : WeierstrassCurve R) : Polynomial.eval 0 (Polynomial.eval 0 (WeierstrassCurve.polynomialX W)) = -W.a₄

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

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

TODO: define this in terms of Polynomial.derivative.

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₃

@[simp]

theorem WeierstrassCurve.eval_polynomialY_zero {R : Type u} [CommRing R] (W : WeierstrassCurve R) : Polynomial.eval 0 (Polynomial.eval 0 (WeierstrassCurve.polynomialY W)) = W.a₃

def WeierstrassCurve.nonsingular {R : Type u} [CommRing R] (W : WeierstrassCurve R) (x : R) (y : R) : Prop

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

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)

theorem WeierstrassCurve.nonsingular_iff_variableChange {R : Type u} [CommRing R] (W : WeierstrassCurve R) (x : R) (y : R) : WeierstrassCurve.nonsingular W x y ↔ WeierstrassCurve.nonsingular (WeierstrassCurve.variableChange W { u := 1, r := x, s := 0, t := y }) 0 0

theorem WeierstrassCurve.nonsingular_iff_baseChange {R : Type u} [CommRing R] (W : WeierstrassCurve R) (A : Type v) [CommRing A] [Algebra R A] [Nontrivial A] [NoZeroSMulDivisors R A] (x : R) (y : R) : WeierstrassCurve.nonsingular W x y ↔ WeierstrassCurve.nonsingular (WeierstrassCurve.baseChange W A) (↑(algebraMap R A) x) (↑(algebraMap R A) y)

theorem WeierstrassCurve.nonsingular_iff_baseChange_of_baseChange {R : Type u} [CommRing R] (W : WeierstrassCurve R) (A : Type v) [CommRing A] [Algebra R A] (B : Type w) [CommRing B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] [Nontrivial B] [NoZeroSMulDivisors A B] (x : A) (y : A) : WeierstrassCurve.nonsingular (WeierstrassCurve.baseChange W A) x y ↔ WeierstrassCurve.nonsingular (WeierstrassCurve.baseChange W B) (↑(algebraMap A B) x) (↑(algebraMap A B) y)

theorem WeierstrassCurve.nonsingular_zero_of_Δ_ne_zero {R : Type u} [CommRing R] (W : WeierstrassCurve R) (h : WeierstrassCurve.equation W 0 0) (hΔ : WeierstrassCurve.Δ W ≠ 0) : WeierstrassCurve.nonsingular W 0 0

theorem WeierstrassCurve.nonsingular_of_Δ_ne_zero {R : Type u} [CommRing R] (W : WeierstrassCurve R) {x : R} {y : R} (h : WeierstrassCurve.equation W x y) (hΔ : WeierstrassCurve.Δ W ≠ 0) : WeierstrassCurve.nonsingular W x y

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

Ideals in the coordinate ring

@[inline, reducible]

abbrev WeierstrassCurve.CoordinateRing {R : Type u} [CommRing R] (W : WeierstrassCurve R) : Type u

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

@[inline, reducible]

abbrev WeierstrassCurve.FunctionField {R : Type u} [CommRing R] (W : WeierstrassCurve R) : Type u

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

@[inline, reducible]

noncomputable abbrev WeierstrassCurve.CoordinateRing.mk {R : Type u} [CommRing R] (W : WeierstrassCurve R) : Polynomial (Polynomial R) →+* WeierstrassCurve.CoordinateRing W

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

instance WeierstrassCurve.CoordinateRing.instIsDomainCoordinateRing {R : Type u} [CommRing R] (W : WeierstrassCurve R) [IsDomain R] [NormalizedGCDMonoid R] : IsDomain (WeierstrassCurve.CoordinateRing W)

instance WeierstrassCurve.CoordinateRing.instIsDomainCoordinateRing_of_Field {F : Type u} [Field F] (W : WeierstrassCurve F) : IsDomain (WeierstrassCurve.CoordinateRing W)

noncomputable def WeierstrassCurve.CoordinateRing.XClass {R : Type u} [CommRing R] (W : WeierstrassCurve R) (x : R) : WeierstrassCurve.CoordinateRing W

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

theorem WeierstrassCurve.CoordinateRing.XClass_ne_zero {R : Type u} [CommRing R] (W : WeierstrassCurve R) (x : R) [Nontrivial R] : WeierstrassCurve.CoordinateRing.XClass W x ≠ 0

noncomputable def WeierstrassCurve.CoordinateRing.YClass {R : Type u} [CommRing R] (W : WeierstrassCurve R) (y : Polynomial R) : WeierstrassCurve.CoordinateRing W

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

theorem WeierstrassCurve.CoordinateRing.YClass_ne_zero {R : Type u} [CommRing R] (W : WeierstrassCurve R) (y : Polynomial R) [Nontrivial R] : WeierstrassCurve.CoordinateRing.YClass W y ≠ 0

noncomputable def WeierstrassCurve.CoordinateRing.XIdeal {R : Type u} [CommRing R] (W : WeierstrassCurve R) (x : R) : Ideal (WeierstrassCurve.CoordinateRing W)

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

noncomputable def WeierstrassCurve.CoordinateRing.YIdeal {R : Type u} [CommRing R] (W : WeierstrassCurve R) (y : Polynomial R) : Ideal (WeierstrassCurve.CoordinateRing W)

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

noncomputable def WeierstrassCurve.CoordinateRing.XYIdeal {R : Type u} [CommRing R] (W : WeierstrassCurve R) (x : R) (y : Polynomial R) : Ideal (WeierstrassCurve.CoordinateRing W)

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

The coordinate ring as an R[X]-algebra

noncomputable instance WeierstrassCurve.CoordinateRing.instAlgebraCoordinateRing {R : Type u} [CommRing R] (W : WeierstrassCurve R) : Algebra (Polynomial R) (WeierstrassCurve.CoordinateRing W)

noncomputable instance WeierstrassCurve.CoordinateRing.instAlgebraCoordinateRing' {R : Type u} [CommRing R] (W : WeierstrassCurve R) : Algebra R (WeierstrassCurve.CoordinateRing W)

instance WeierstrassCurve.CoordinateRing.instIsScalarTowerCoordinateRing {R : Type u} [CommRing R] (W : WeierstrassCurve R) : IsScalarTower R (Polynomial R) (WeierstrassCurve.CoordinateRing W)

instance WeierstrassCurve.CoordinateRing.instSubsingletonCoordinateRing {R : Type u} [CommRing R] (W : WeierstrassCurve R) [Subsingleton R] : Subsingleton (WeierstrassCurve.CoordinateRing W)

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

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] R

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

noncomputable def WeierstrassCurve.CoordinateRing.basis {R : Type u} [CommRing R] (W : WeierstrassCurve R) : Basis (Fin 2) (Polynomial R) (WeierstrassCurve.CoordinateRing W)

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

theorem WeierstrassCurve.CoordinateRing.basis_apply {R : Type u} [CommRing R] (W : WeierstrassCurve R) (n : Fin 2) : ↑(WeierstrassCurve.CoordinateRing.basis W) n = (AdjoinRoot.powerBasis' (_ : Polynomial.Monic (WeierstrassCurve.polynomial W))).gen ^ ↑n

@[simp]

theorem WeierstrassCurve.CoordinateRing.basis_zero {R : Type u} [CommRing R] (W : WeierstrassCurve R) : ↑(WeierstrassCurve.CoordinateRing.basis W) 0 = 1

@[simp]

theorem WeierstrassCurve.CoordinateRing.basis_one {R : Type u} [CommRing R] (W : WeierstrassCurve R) : ↑(WeierstrassCurve.CoordinateRing.basis W) 1 = ↑(WeierstrassCurve.CoordinateRing.mk W) Polynomial.X

theorem WeierstrassCurve.CoordinateRing.coe_basis {R : Type u} [CommRing R] (W : WeierstrassCurve R) : ↑(WeierstrassCurve.CoordinateRing.basis W) = ![1, ↑(WeierstrassCurve.CoordinateRing.mk W) Polynomial.X]

theorem WeierstrassCurve.CoordinateRing.smul {R : Type u} [CommRing R] {W : WeierstrassCurve R} (x : Polynomial R) (y : WeierstrassCurve.CoordinateRing W) : x • y = ↑(WeierstrassCurve.CoordinateRing.mk W) (↑Polynomial.C x) * y

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.exists_smul_basis_eq {R : Type u} [CommRing R] {W : WeierstrassCurve R} (x : WeierstrassCurve.CoordinateRing W) : ∃ p q, p • 1 + q • ↑(WeierstrassCurve.CoordinateRing.mk W) Polynomial.X = x

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

theorem WeierstrassCurve.CoordinateRing.degree_norm_smul_basis {R : Type u} [CommRing R] (W : WeierstrassCurve R) [IsDomain R] (p : Polynomial R) (q : Polynomial R) : Polynomial.degree (↑(Algebra.norm (Polynomial R)) (p • 1 + q • ↑(WeierstrassCurve.CoordinateRing.mk W) Polynomial.X)) = max (2 • Polynomial.degree p) (2 • Polynomial.degree q + 3)

theorem WeierstrassCurve.CoordinateRing.degree_norm_ne_one {R : Type u} [CommRing R] {W : WeierstrassCurve R} [IsDomain R] (x : WeierstrassCurve.CoordinateRing W) : Polynomial.degree (↑(Algebra.norm (Polynomial R)) x) ≠ 1

theorem WeierstrassCurve.CoordinateRing.natDegree_norm_ne_one {R : Type u} [CommRing R] {W : WeierstrassCurve R} [IsDomain R] (x : WeierstrassCurve.CoordinateRing W) : Polynomial.natDegree (↑(Algebra.norm (Polynomial R)) x) ≠ 1

Elliptic curves

theorem EllipticCurve.ext_iff {R : Type u} : ∀ {inst : CommRing R} (x y : EllipticCurve R), x = y ↔ x.a₁ = y.a₁ ∧ x.a₂ = y.a₂ ∧ x.a₃ = y.a₃ ∧ x.a₄ = y.a₄ ∧ x.a₆ = y.a₆ ∧ x.Δ' = y.Δ'

theorem EllipticCurve.ext {R : Type u} : ∀ {inst : CommRing R} (x y : EllipticCurve R), x.a₁ = y.a₁ → x.a₂ = y.a₂ → x.a₃ = y.a₃ → x.a₄ = y.a₄ → x.a₆ = y.a₆ → x.Δ' = y.Δ' → x = y

structure EllipticCurve (R : Type u) [CommRing R] extends WeierstrassCurve : Type u

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

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.

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

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

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

theorem EllipticCurve.ofJ0_j (R : Type u) [CommRing R] [Invertible 3] : EllipticCurve.j (EllipticCurve.ofJ0 R) = 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).

theorem EllipticCurve.ofJ1728_j (R : Type u) [CommRing R] [Invertible 2] : EllipticCurve.j (EllipticCurve.ofJ1728 R) = 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).

theorem EllipticCurve.ofJ'_j {R : Type u} [CommRing R] (j : R) [Invertible j] [Invertible (j - 1728)] : EllipticCurve.j (EllipticCurve.ofJ' 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').

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.j (EllipticCurve.ofJ j) = j

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

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

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

@[simp]

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

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

The elliptic curve over R induced by an admissible linear change of variables $(X, Y) \mapsto (u^2X + r, u^3Y + u^2sX + t)$ for some $u \in R^\times$ and some $r, s, t \in R$. When R is a field, any two Weierstrass equations isomorphic to E are related by this.

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

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

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

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

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

@[simp]

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

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

The elliptic curve over R base changed to A.

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

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

@[simp]

theorem EllipticCurve.baseChange_j {R : Type u} [CommRing R] (E : EllipticCurve R) (A : Type v) [CommRing A] [Algebra R A] : EllipticCurve.j (EllipticCurve.baseChange E A) = ↑(algebraMap R A) (EllipticCurve.j E)

theorem EllipticCurve.baseChange_injective {R : Type u} [CommRing R] (A : Type v) [CommRing A] [Algebra R A] (h : Function.Injective ↑(algebraMap R A)) : Function.Injective fun E => EllipticCurve.baseChange E A