The Deuring normal form of an elliptic curve

For a : R, the Weierstrass curve in Deuring normal form is

Y² + aXY + Y = X³,

that is, a₁ = a, a₃ = 1 and a₂ = a₄ = a₆ = 0 (WeierstrassCurve.deuringNormalForm). Its invariants are

c₄ = a (a³ - 24), c₆ = -a⁶ + 36a³ - 216, Δ = a³ - 27, j = a³ (a³ - 24)³ / (a³ - 27),

so it is elliptic exactly when a³ - 27 is a unit. The point (0, 0) lies on it, with horizontal tangent Y = 0 meeting the curve there to order three: (0, 0) is a flex, a point of order 3, and the 3-division polynomial Ψ₃ vanishes at 0.

Conversely, a point at which Ψ₃ vanishes can be moved to the origin in this shape (Silverman, AEC, Appendix A, Proposition 1.3). Let (x, y) be a point of W with Ψ₃(x) = 0, and suppose that ψ₂(x, y) = 2y + a₁x + a₃ is a cube u³ of a unit. The translation (r, t) = (x, y) moves the point to the origin (a₆ = 0), the shear s with s ψ₂(x, y) = a₄ + 2a₂x - a₁y + 3x² makes the tangent line there horizontal (a₄ = 0), and the scaling by u makes a₃ = 1. The coefficient a₂ then vanishes because a₂ ψ₂(x, y)² = Ψ₃(x) after the translation and shear (WeierstrassCurve.a₂_mul_ψ₂_sq_eq_eval_Ψ₃).

Away from characteristic 3 every elliptic curve takes this form after a finite separable extension of the base field: adjoin a root x of the separable polynomial Ψ₃, a matching y, and a cube root of ψ₂(x, y), which is nonzero because Ψ₃ and Ψ₂Sq have no common root. This holds in characteristic 2 too, where the Legendre form y² = x (x - 1) (x - λ) of TauCeti/AlgebraicGeometry/EllipticCurve/Legendre.lean is not available. Since j is an explicit rational function of a, the Deuring form ties the reduction of an elliptic curve to its j-invariant in residue characteristic 2, as the Legendre form does away from it: this is how the criterion WeierstrassCurve.hasPotentialGoodReduction_of_isInteger_j for potential good reduction is proved in residue characteristic 2.

Main definitions

• WeierstrassCurve.deuringNormalForm a: the curve Y² + aXY + Y = X³.

Main results

• WeierstrassCurve.deuringNormalForm_Δ and WeierstrassCurve.deuringNormalForm_j: its discriminant and j-invariant.
• WeierstrassCurve.exists_variableChange_smul_eq_deuringNormalForm: a curve with a point at which Ψ₃ vanishes and ψ₂ is a cube of a unit is a change of variables away from Deuring normal form.
• WeierstrassCurve.exists_variableChange_smul_baseChange_eq_deuringNormalForm: away from characteristic 3, an elliptic curve takes Deuring normal form over a finite separable extension.

References

• J. Silverman, The Arithmetic of Elliptic Curves, Appendix A, Proposition 1.3, and VII.5.5.

The Deuring normal form

def WeierstrassCurve.deuringNormalForm {R : Type u_1} [CommRing R] (a : R) : WeierstrassCurve R

The Weierstrass curve Y² + aXY + Y = X³ in Deuring normal form: a₁ = a, a₃ = 1 and a₂ = a₄ = a₆ = 0.

@[simp]

theorem WeierstrassCurve.deuringNormalForm_a₁ {R : Type u_1} [CommRing R] (a : R) : (deuringNormalForm a).a₁ = a

@[simp]

theorem WeierstrassCurve.deuringNormalForm_a₂ {R : Type u_1} [CommRing R] (a : R) : (deuringNormalForm a).a₂ = 0

@[simp]

theorem WeierstrassCurve.deuringNormalForm_a₃ {R : Type u_1} [CommRing R] (a : R) : (deuringNormalForm a).a₃ = 1

@[simp]

theorem WeierstrassCurve.deuringNormalForm_a₄ {R : Type u_1} [CommRing R] (a : R) : (deuringNormalForm a).a₄ = 0

@[simp]

theorem WeierstrassCurve.deuringNormalForm_a₆ {R : Type u_1} [CommRing R] (a : R) : (deuringNormalForm a).a₆ = 0

@[simp]

theorem WeierstrassCurve.deuringNormalForm_b₂ {R : Type u_1} [CommRing R] (a : R) : (deuringNormalForm a).b₂ = a ^ 2

@[simp]

theorem WeierstrassCurve.deuringNormalForm_b₄ {R : Type u_1} [CommRing R] (a : R) : (deuringNormalForm a).b₄ = a

@[simp]

theorem WeierstrassCurve.deuringNormalForm_b₆ {R : Type u_1} [CommRing R] (a : R) : (deuringNormalForm a).b₆ = 1

@[simp]

theorem WeierstrassCurve.deuringNormalForm_b₈ {R : Type u_1} [CommRing R] (a : R) : (deuringNormalForm a).b₈ = 0

@[simp]

theorem WeierstrassCurve.deuringNormalForm_c₄ {R : Type u_1} [CommRing R] (a : R) : (deuringNormalForm a).c₄ = a * (a ^ 3 - 24)

@[simp]

theorem WeierstrassCurve.deuringNormalForm_c₆ {R : Type u_1} [CommRing R] (a : R) : (deuringNormalForm a).c₆ = -a ^ 6 + 36 * a ^ 3 - 216

The c₆ of the Deuring normal form Y² + aXY + Y = X³ is -a⁶ + 36a³ - 216.

@[simp]

theorem WeierstrassCurve.deuringNormalForm_Δ {R : Type u_1} [CommRing R] (a : R) : (deuringNormalForm a).Δ = a ^ 3 - 27

The discriminant of the Deuring normal form Y² + aXY + Y = X³ is a³ - 27.

theorem WeierstrassCurve.isElliptic_deuringNormalForm_iff {R : Type u_1} [CommRing R] (a : R) : (deuringNormalForm a).IsElliptic ↔ IsUnit (a ^ 3 - 27)

The Deuring normal form Y² + aXY + Y = X³ is elliptic exactly when a³ - 27 is a unit.

@[simp]

theorem WeierstrassCurve.deuringNormalForm_j {F : Type u_2} [Field F] (a : F) [(deuringNormalForm a).IsElliptic] : (deuringNormalForm a).j = a ^ 3 * (a ^ 3 - 24) ^ 3 / (a ^ 3 - 27)

The j-invariant of the Deuring normal form Y² + aXY + Y = X³ is a³ (a³ - 24)³ / (a³ - 27).

theorem WeierstrassCurve.equation_deuringNormalForm_zero {R : Type u_1} [CommRing R] (a : R) : (deuringNormalForm a).toAffine.Equation 0 0

The point (0, 0) lies on the Deuring normal form.

@[simp]

theorem WeierstrassCurve.eval_Ψ₃_deuringNormalForm_zero {R : Type u_1} [CommRing R] (a : R) : Polynomial.eval 0 (deuringNormalForm a).Ψ₃ = 0

On the Deuring normal form, the 3-division polynomial Ψ₃ vanishes at 0: the origin is a point of order 3.

@[simp]

theorem WeierstrassCurve.map_deuringNormalForm {R : Type u_1} [CommRing R] (a : R) {A : Type u_2} [CommRing A] (φ : R →+* A) : (deuringNormalForm a).map φ = deuringNormalForm (φ a)

The Deuring normal form commutes with base change.

Changes of variables to Deuring normal form

theorem WeierstrassCurve.exists_variableChange_smul_eq_deuringNormalForm {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} (h : W.toAffine.Equation x y) (hΨ₃ : Polynomial.eval x W.Ψ₃ = 0) (u : Rˣ) (hu : ↑u ^ 3 = 2 * y + W.a₁ * x + W.a₃) : ∃ (C : VariableChange R) (a : R), C • W = deuringNormalForm a

Deuring normal form at a point of order 3. Let (x, y) be a point of W at which the 3-division polynomial Ψ₃ vanishes, and u a unit with u³ = ψ₂(x, y) = 2y + a₁x + a₃. Then a change of variables carries W to a curve Y² + aXY + Y = X³ in Deuring normal form.

theorem WeierstrassCurve.exists_variableChange_smul_baseChange_eq_deuringNormalForm {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (h3 : 3 ≠ 0) : ∃ (L : Type u) (x : Field L) (x_1 : Algebra K L) (_ : FiniteDimensional K L) (_ : Algebra.IsSeparable K L) (C : VariableChange L) (a : L), C • W.baseChange L = deuringNormalForm a

Deuring normal form over a finite separable extension. Away from characteristic 3, an elliptic curve over K becomes isomorphic to a curve Y² + aXY + Y = X³ over a finite separable extension L of K: one obtained by adjoining a root x of the 3-division polynomial Ψ₃, a point (x, y) of the curve above it, and a cube root of 2y + a₁x + a₃.