Models of elliptic curves with prescribed j-invariant

This file defines the Weierstrass equation over a field with prescribed j-invariant, proved that it is an elliptic curve, and that its j-invariant is equal to the given value. It is a modification of [silverman2009], Chapter III, Proposition 1.4 (c).

Main definitions

• WeierstrassCurve.ofJ0: an elliptic curve whose j-invariant is 0.
• WeierstrassCurve.ofJ1728: an elliptic curve whose j-invariant is 1728.
• WeierstrassCurve.ofJNe0Or1728: an elliptic curve whose j-invariant is neither 0 nor 1728.
• WeierstrassCurve.ofJ: an elliptic curve whose j-invariant equal to j.

Main statements

• WeierstrassCurve.ofJ_j: the j-invariant of WeierstrassCurve.ofJ is equal to j.

References

• [J Silverman, The Arithmetic of Elliptic Curves][silverman2009]

Tags

elliptic curve, weierstrass equation, j invariant

def WeierstrassCurve.ofJ0 (R : Type u_1) [CommRing R] : WeierstrassCurve R

The Weierstrass curve Y² + Y = X³. It is of j-invariant 0 if it is an elliptic curve.

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

theorem WeierstrassCurve.ofJ0_Δ (R : Type u_1) [CommRing R] : (ofJ0 R).Δ = -27

def WeierstrassCurve.ofJ1728 (R : Type u_1) [CommRing R] : WeierstrassCurve R

The Weierstrass curve Y² = X³ + X. It is of j-invariant 1728 if it is an elliptic curve.

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

theorem WeierstrassCurve.ofJ1728_Δ (R : Type u_1) [CommRing R] : (ofJ1728 R).Δ = -64

def WeierstrassCurve.ofJNe0Or1728 {R : Type u_1} [CommRing R] (j : R) : WeierstrassCurve R

The Weierstrass curve Y² + (j - 1728)XY = X³ - 36(j - 1728)³X - (j - 1728)⁵. It is a modification of the curve in [silverman2009], Chapter III, Proposition 1.4 (c) to avoid denominators. It is of j-invariant j if it is an elliptic curve.

theorem WeierstrassCurve.ofJNe0Or1728_c₄ {R : Type u_1} [CommRing R] (j : R) : (ofJNe0Or1728 j).c₄ = j * (j - 1728) ^ 3

theorem WeierstrassCurve.ofJNe0Or1728_Δ {R : Type u_1} [CommRing R] (j : R) : (ofJNe0Or1728 j).Δ = j ^ 2 * (j - 1728) ^ 9

instance WeierstrassCurve.instIsEllipticOfJ0OfFactIsUnitOfNat (R : Type u_1) [CommRing R] [hu : Fact (IsUnit 3)] : (ofJ0 R).IsElliptic

When 3 is a unit, Y² + Y = X³ is an elliptic curve. It is of j-invariant 0 (see WeierstrassCurve.ofJ0_j).

theorem WeierstrassCurve.ofJ0_j (R : Type u_1) [CommRing R] [Fact (IsUnit 3)] : (ofJ0 R).j = 0

instance WeierstrassCurve.instIsEllipticOfJ1728OfFactIsUnitOfNat (R : Type u_1) [CommRing R] [hu : Fact (IsUnit 2)] : (ofJ1728 R).IsElliptic

When 2 is a unit, Y² = X³ + X is an elliptic curve. It is of j-invariant 1728 (see WeierstrassCurve.ofJ1728_j).

theorem WeierstrassCurve.ofJ1728_j (R : Type u_1) [CommRing R] [Fact (IsUnit 2)] : (ofJ1728 R).j = 1728

instance WeierstrassCurve.instIsEllipticOfJNe0Or1728OfFactIsUnitHSubOfNat {R : Type u_1} [CommRing R] (j : R) [h1 : Fact (IsUnit j)] [h2 : Fact (IsUnit (j - 1728))] : (ofJNe0Or1728 j).IsElliptic

When j and j - 1728 are both units, Y² + (j - 1728)XY = X³ - 36(j - 1728)³X - (j - 1728)⁵ is an elliptic curve. It is of j-invariant j (see WeierstrassCurve.ofJNe0Or1728_j).

theorem WeierstrassCurve.ofJNe0Or1728_j {R : Type u_1} [CommRing R] (j : R) [Fact (IsUnit j)] [Fact (IsUnit (j - 1728))] : (ofJNe0Or1728 j).j = j

def WeierstrassCurve.ofJ {F : Type u_2} [Field F] (j : F) [DecidableEq F] : WeierstrassCurve F

For any element j of a field F, there exists an elliptic curve over F with j-invariant equal to j (see WeierstrassCurve.ofJ_j). Its coefficients are given explicitly (see WeierstrassCurve.ofJ0, WeierstrassCurve.ofJ1728 and WeierstrassCurve.ofJNe0Or1728).

theorem WeierstrassCurve.ofJ_0_of_three_ne_zero {F : Type u_2} [Field F] [DecidableEq F] (h3 : 3 ≠ 0) : ofJ 0 = ofJ0 F

theorem WeierstrassCurve.ofJ_0_of_three_eq_zero {F : Type u_2} [Field F] [DecidableEq F] (h3 : 3 = 0) : ofJ 0 = ofJ1728 F

theorem WeierstrassCurve.ofJ_0_of_two_eq_zero {F : Type u_2} [Field F] [DecidableEq F] (h2 : 2 = 0) : ofJ 0 = ofJ0 F

theorem WeierstrassCurve.ofJ_1728_of_three_eq_zero {F : Type u_2} [Field F] [DecidableEq F] (h3 : 3 = 0) : ofJ 1728 = ofJ1728 F

theorem WeierstrassCurve.ofJ_1728_of_two_ne_zero {F : Type u_2} [Field F] [DecidableEq F] (h2 : 2 ≠ 0) : ofJ 1728 = ofJ1728 F

theorem WeierstrassCurve.ofJ_1728_of_two_eq_zero {F : Type u_2} [Field F] [DecidableEq F] (h2 : 2 = 0) : ofJ 1728 = ofJ0 F

theorem WeierstrassCurve.ofJ_ne_0_ne_1728 {F : Type u_2} [Field F] (j : F) [DecidableEq F] (h0 : j ≠ 0) (h1728 : j ≠ 1728) : ofJ j = ofJNe0Or1728 j

instance WeierstrassCurve.instIsEllipticOfJ {F : Type u_2} [Field F] (j : F) [DecidableEq F] : (ofJ j).IsElliptic

theorem WeierstrassCurve.ofJ_j {F : Type u_2} [Field F] (j : F) [DecidableEq F] : (ofJ j).j = j

instance WeierstrassCurve.instInhabitedSubtypeIsElliptic {F : Type u_2} [Field F] [DecidableEq F] : Inhabited { W : WeierstrassCurve F // W.IsElliptic }