The Legendre form of an elliptic curve

The Legendre form of an elliptic curve is y² = x (x - 1) (x - λ): the cubic on the right has its three roots at 0, 1 and λ. In Tau Ceti it is the curve TauCeti.freyCurve 1 B with B = -λ, whose invariants TauCeti.freyCurve_c₄, TauCeti.freyCurve_Δ and TauCeti.freyCurve_j specialise to

c₄ = 16 (B² + B + 1), Δ = 16 B² (B + 1)², j = 256 (B² + B + 1)³ / (B² (B + 1)²).

Away from characteristic 2 every elliptic curve takes this form after a finite separable extension of the base field (Silverman, AEC, III.1.7). Over a field F with 2 ≠ 0, suppose that the 2-division polynomial 4x³ + b₂x² + 2b₄x + b₆ of W factors as 4 (x - e₁) (x - e₂) (x - e₃) with e₁ ≠ e₂, and that e₂ - e₁ = u². Completing the square in y, moving e₁ to the origin and scaling by u is a change of variables taking W to the Legendre form with λ = (e₃ - e₁) / (e₂ - e₁). A splitting field of the 2-division polynomial, followed by a splitting field of X² - (e₂ - e₁), supplies the roots and the square root, and it is separable because the 2-division polynomial has nonzero discriminant 16 Δ.

Since j is an explicit rational function of λ, the Legendre form ties the reduction of an elliptic curve to its j-invariant: this is how the criterion WeierstrassCurve.hasPotentialGoodReduction_of_isInteger_j for potential good reduction is proved away from residue characteristic 2. In residue characteristic 2 the Deuring normal form of TauCeti/AlgebraicGeometry/EllipticCurve/DeuringNormalForm.lean takes its place.

Over an arbitrary commutative ring R the Legendre form is reached from two points of order two rather than from roots of the 2-division polynomial. Let (x₁, y₁) and (x₂, y₂) be points of W at which ψ₂ = 2y + a₁x + a₃ vanishes, and u a unit with x₂ - x₁ = u². If W is elliptic, this already forces 2 to be a unit (WeierstrassCurve.isUnit_two_of_evalEval_ψ₂_eq_zero). Exactly one change of variables with scaling u then carries W to a Legendre form, (x₁, y₁) to (0, 0) and (x₂, y₂) to (1, 0) (WeierstrassCurve.existsUnique_variableChange_legendre). It is WeierstrassCurve.toLegendre, with r = x₁, s = -a₁/2 and t = y₁. A change of variables with scaling u multiplies the invariant differential by u, so fixing u amounts to fixing the differential ω = u·ω_W. The ring ℤ[1/2][λ, 1/λ(λ - 1)] with the curve y² = x (x - 1) (x - λ) (WeierstrassCurve.UniversalLegendre.curve) classifies such data at the level of equations: an elliptic Weierstrass curve with two such points and such a unit u determines exactly one ring homomorphism out of it and one change of variables with scaling u to the base change of the universal curve carrying (x₁, y₁) to (0, 0) and (x₂, y₂) to (1, 0) (WeierstrassCurve.UniversalLegendre.existsUnique_legendre). The parameter λ depends on u only through u². This is not yet the representability of the Legendre structures of Katz and Mazur, an ordered basis of E[2] together with a nowhere-vanishing differential: it models them only once the two points are identified with a basis of the 2-torsion and ω with the corresponding differential, which needs the 2-torsion subgroup and invariant differential of an elliptic curve over a general base.

Main definitions

• WeierstrassCurve.toLegendre: the change of variables to Legendre form with scaling u, centred at a point of order two; it commutes with base change (WeierstrassCurve.toLegendre_map).
• WeierstrassCurve.UniversalLegendre.Ring, WeierstrassCurve.UniversalLegendre.curve: the ring ℤ[1/2][λ, 1/λ(λ - 1)] and the universal Legendre curve over it.
• WeierstrassCurve.UniversalLegendre.lift: the classifying homomorphism ℤ[1/2][λ, 1/λ(λ - 1)] →+* R of an element l with 2l(l - 1) a unit, along which the universal curve becomes y² = x (x - 1) (x - l) (WeierstrassCurve.UniversalLegendre.map_lift), naturally in R (WeierstrassCurve.UniversalLegendre.comp_lift).

Main results

• WeierstrassCurve.exists_variableChange_smul_eq_freyCurve_one: a curve whose 2-division polynomial splits, with e₂ - e₁ a square, is a change of variables away from Legendre form.
• WeierstrassCurve.exists_variableChange_smul_baseChange_eq_freyCurve_one: away from characteristic 2, an elliptic curve takes Legendre form over a finite separable extension.
• TauCeti.isElliptic_freyCurve_one_neg_iff: y² = x (x - 1) (x - l) is elliptic exactly when 2l(l - 1) is a unit.
• WeierstrassCurve.toLegendre_smul: over a ring, toLegendre carries W to Legendre form, with an explicit parameter.
• WeierstrassCurve.eq_toLegendre: it is the only change of variables with scaling u doing so that sends (x₁, y₁) to (0, 0).
• WeierstrassCurve.existsUnique_variableChange_legendre and WeierstrassCurve.exists_variableChange_legendre_iff: existence and uniqueness together, and, for elliptic W, the converse.
• WeierstrassCurve.UniversalLegendre.existsUnique_legendre: the equation-level universal property of the universal Legendre curve.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.1.7 and VII.5.5.
• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, Annals of Mathematics Studies 108, Princeton University Press, 1985, 2.2.9 and 4.6.2, for the Legendre structures.

Provenance

The WeierstrassCurve.UniversalLegendre namespace is adapted from Tau Ceti's own WeierstrassCurve.UniversalTate in TauCeti.AlgebraicGeometry.EllipticCurve.TateNormalForm: the ring as a localisation of a polynomial ring over ℤ, and Ring.ringHom_ext, lift, lift_comp_algebraMap, lift_algebraMap, map_lift, comp_lift and eq_lift, follow the declarations of the same names there.

theorem TauCeti.isElliptic_freyCurve_one_neg_iff {R : Type u_1} [CommRing R] {l : R} : (freyCurve 1 (-l)).IsElliptic ↔ IsUnit (2 * l * (l - 1))

The Legendre form y² = x (x - 1) (x - l) is elliptic exactly when 2l(l - 1) is a unit.

Legendre form over a ring

noncomputable def WeierstrassCurve.toLegendre {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (h2 : IsUnit 2) (u : Rˣ) (x₁ y₁ : R) : VariableChange R

The change of variables to Legendre form with scaling u and centre (x₁, y₁), defined when 2 is a unit: u, r = x₁, s = -a₁/2 and t = y₁. When (x₁, y₁) and (x₂, y₂) are points of order two on W with x₂ - x₁ = u², it carries W to Legendre form, (x₁, y₁) to (0, 0) and (x₂, y₂) to (1, 0) (toLegendre_smul), and it is the only change of variables with scaling u doing so (eq_toLegendre).

@[simp]

theorem WeierstrassCurve.toLegendre_u {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {x₁ y₁ : R} (h2 : IsUnit 2) (u : Rˣ) : (W.toLegendre h2 u x₁ y₁).u = u

@[simp]

theorem WeierstrassCurve.toLegendre_r {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {x₁ y₁ : R} (h2 : IsUnit 2) (u : Rˣ) : (W.toLegendre h2 u x₁ y₁).r = x₁

@[simp]

theorem WeierstrassCurve.toLegendre_s {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {x₁ y₁ : R} (h2 : IsUnit 2) (u : Rˣ) : (W.toLegendre h2 u x₁ y₁).s = -W.a₁ * ↑h2.unit⁻¹

@[simp]

theorem WeierstrassCurve.toLegendre_t {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {x₁ y₁ : R} (h2 : IsUnit 2) (u : Rˣ) : (W.toLegendre h2 u x₁ y₁).t = y₁

theorem WeierstrassCurve.toLegendre_map {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {x₁ y₁ : R} (h2 : IsUnit 2) (u : Rˣ) {A : Type u_2} [CommRing A] (φ : R →+* A) : (W.toLegendre h2 u x₁ y₁).map φ = (W.map φ).toLegendre ⋯ ((Units.map ↑φ) u) (φ x₁) (φ y₁)

Legendre form commutes with base change. The image of toLegendre under a ring homomorphism φ is the change of variables to Legendre form of W.map φ with scaling φ u and centre (φ x₁, φ y₁), where 2 is again a unit since it is the image of 2 under φ.

theorem WeierstrassCurve.toLegendre_smul {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x₁ y₁ x₂ y₂ : R} (h2 : IsUnit 2) (u : Rˣ) (h₁ : W.toAffine.Equation x₁ y₁) (h₂ : W.toAffine.Equation x₂ y₂) (hψ₁ : Polynomial.evalEval x₁ y₁ W.ψ₂ = 0) (hψ₂ : Polynomial.evalEval x₂ y₂ W.ψ₂ = 0) (hu : x₂ - x₁ = ↑u ^ 2) : W.toLegendre h2 u x₁ y₁ • W = TauCeti.freyCurve 1 ((W.b₂ * ↑h2.unit⁻¹ ^ 2 + 2 * x₁ + x₂) * ↑u⁻¹ ^ 2)

Existence of Legendre form. Let (x₁, y₁) and (x₂, y₂) be points of W at which ψ₂ vanishes, with x₂ - x₁ = u². Then toLegendre carries W to the Legendre form y² = x (x - 1) (x - λ), that is freyCurve 1 (-λ), with λ = -(b₂/4 + 2x₁ + x₂)/u². Thus u² λ = x₃ - x₁ where x₃ = -b₂/4 - x₁ - x₂ is the x-coordinate of the third point of order two.

theorem WeierstrassCurve.toLegendre_one_zero {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x₁ y₁ x₂ y₂ : R} (h2 : IsUnit 2) (u : Rˣ) (hψ₁ : Polynomial.evalEval x₁ y₁ W.ψ₂ = 0) (hψ₂ : Polynomial.evalEval x₂ y₂ W.ψ₂ = 0) (hu : x₂ - x₁ = ↑u ^ 2) : ↑(W.toLegendre h2 u x₁ y₁).u ^ 2 + (W.toLegendre h2 u x₁ y₁).r = x₂ ∧ ↑(W.toLegendre h2 u x₁ y₁).u ^ 2 * (W.toLegendre h2 u x₁ y₁).s + (W.toLegendre h2 u x₁ y₁).t = y₂

If ψ₂ vanishes at the coordinate pairs (x₁, y₁) and (x₂, y₂) and x₂ - x₁ = u², the change of variables toLegendre with centre (x₁, y₁) carries (x₂, y₂) to (1, 0): u² · 1 + r = x₂ and u³ · 0 + u² s · 1 + t = y₂. Neither pair need lie on W.

theorem WeierstrassCurve.eq_toLegendre {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x₁ y₁ : R} (h2 : IsUnit 2) (u : Rˣ) {C : VariableChange R} (hu : C.u = u) (hr : C.r = x₁) (ht : C.t = y₁) {B : R} (hC : C • W = TauCeti.freyCurve 1 B) : C = W.toLegendre h2 u x₁ y₁

Uniqueness of Legendre form. A change of variables with scaling u carrying W to a curve freyCurve 1 B and (x₁, y₁) to (0, 0) (that is, with r = x₁ and t = y₁) is toLegendre.

theorem WeierstrassCurve.existsUnique_variableChange_legendre {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x₁ y₁ x₂ y₂ : R} (h2 : IsUnit 2) (u : Rˣ) (h₁ : W.toAffine.Equation x₁ y₁) (h₂ : W.toAffine.Equation x₂ y₂) (hψ₁ : Polynomial.evalEval x₁ y₁ W.ψ₂ = 0) (hψ₂ : Polynomial.evalEval x₂ y₂ W.ψ₂ = 0) (hu : x₂ - x₁ = ↑u ^ 2) : ∃! C : VariableChange R, C.u = u ∧ C.r = x₁ ∧ C.t = y₁ ∧ ↑C.u ^ 2 + C.r = x₂ ∧ ↑C.u ^ 2 * C.s + C.t = y₂ ∧ ∃ (B : R), C • W = TauCeti.freyCurve 1 B

Legendre form. Let (x₁, y₁) and (x₂, y₂) be points of W at which the 2-division polynomial ψ₂ vanishes, with x₂ - x₁ = u² for a unit u, over a ring in which 2 is a unit. Then exactly one change of variables with scaling u carries W to a Legendre form y² = x (x - 1) (x - λ) (a curve freyCurve 1 B, with B = -λ), (x₁, y₁) to (0, 0) and (x₂, y₂) to (1, 0). A change of variables with scaling u multiplies the invariant differential by u, so this is the Legendre normalisation of the triple ((x₁, y₁), (x₂, y₂), ω), for the differential ω that is u times the invariant differential of W.

theorem WeierstrassCurve.exists_variableChange_legendre_iff {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x₁ y₁ x₂ y₂ : R} (u : Rˣ) [W.IsElliptic] : (∃ (C : VariableChange R), C.u = u ∧ C.r = x₁ ∧ C.t = y₁ ∧ ↑C.u ^ 2 + C.r = x₂ ∧ ↑C.u ^ 2 * C.s + C.t = y₂ ∧ ∃ (B : R), C • W = TauCeti.freyCurve 1 B) ↔ W.toAffine.Equation x₁ y₁ ∧ W.toAffine.Equation x₂ y₂ ∧ Polynomial.evalEval x₁ y₁ W.ψ₂ = 0 ∧ Polynomial.evalEval x₂ y₂ W.ψ₂ = 0 ∧ x₂ - x₁ = ↑u ^ 2

For an elliptic W, a change of variables with scaling u carrying W to a Legendre form, (x₁, y₁) to (0, 0) and (x₂, y₂) to (1, 0) exists exactly when these are points of W at which ψ₂ vanishes and x₂ - x₁ = u². The ring is then automatically one in which 2 is a unit (isUnit_two_of_evalEval_ψ₂_eq_zero).

Legendre form over a field

theorem WeierstrassCurve.exists_variableChange_smul_eq_freyCurve_one {F : Type u_1} [Field F] {W : WeierstrassCurve F} (h2 : 2 ≠ 0) {e₁ e₂ e₃ u : F} (h : W.twoTorsionPolynomial.toPoly = Polynomial.C 4 * (Polynomial.X - Polynomial.C e₁) * (Polynomial.X - Polynomial.C e₂) * (Polynomial.X - Polynomial.C e₃)) (he : e₂ ≠ e₁) (hu : u ^ 2 = e₂ - e₁) : ∃ (C : VariableChange F), C • W = TauCeti.freyCurve 1 ((e₁ - e₃) / (e₂ - e₁))

Legendre form. If 2 ≠ 0, the 2-division polynomial of W factors as 4 (X - e₁) (X - e₂) (X - e₃) with e₁ ≠ e₂, and e₂ - e₁ = u², then a change of variables takes W to the Legendre form y² = x (x - 1) (x - λ) with λ = (e₃ - e₁) / (e₂ - e₁), that is to freyCurve 1 (-λ). It completes the square in y, moves e₁ to the origin and scales x by u²: it is toLegendre centred at the point (e₁, -(a₁e₁ + a₃)/2) of order two.

theorem WeierstrassCurve.exists_variableChange_smul_baseChange_eq_freyCurve_one {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (h2 : 2 ≠ 0) : ∃ (L : Type u) (x : Field L) (x_1 : Algebra K L) (_ : FiniteDimensional K L) (_ : Algebra.IsSeparable K L) (C : VariableChange L) (B : L), C • W.baseChange L = TauCeti.freyCurve 1 B

Legendre form over a finite separable extension. Away from characteristic 2, an elliptic curve over K becomes isomorphic to a curve y² = x (x - 1) (x + B) over a finite separable extension L of K: one obtained by adjoining the roots e₁, e₂, e₃ of its 2-division polynomial and a square root of e₂ - e₁.

The universal Legendre curve over ℤ[1/2][λ, 1/λ(λ - 1)]

@[reducible, inline]

abbrev WeierstrassCurve.UniversalLegendre.Ring : Type

The ring ℤ[1/2][λ, 1/λ(λ - 1)]: the polynomial ring ℤ[λ] localised away from 2λ(λ - 1).

@[reducible, inline]

noncomputable abbrev WeierstrassCurve.UniversalLegendre.param : Ring

The parameter λ of ℤ[1/2][λ, 1/λ(λ - 1)].

noncomputable def WeierstrassCurve.UniversalLegendre.curve : WeierstrassCurve Ring

The universal Legendre curve y² = x (x - 1) (x - λ), over ℤ[1/2][λ, 1/λ(λ - 1)], with its points (0, 0) and (1, 0) of order two. Let W be an elliptic Weierstrass curve with points (x₁, y₁) and (x₂, y₂) of order two, and u a unit with x₂ - x₁ = u². Then there is exactly one pair of a ring homomorphism and a change of variables with scaling u carrying W to the base change of this curve along it, (x₁, y₁) to (0, 0) and (x₂, y₂) to (1, 0) (existsUnique_legendre).

theorem WeierstrassCurve.UniversalLegendre.curve_def : curve = TauCeti.freyCurve 1 (-param)

The universal Legendre curve is the Legendre form y² = x (x - 1) (x - λ) with parameter λ. Not @[simp], so that map_lift stays the simp normal form of its base changes.

instance WeierstrassCurve.UniversalLegendre.instIsEllipticRingCurve : curve.IsElliptic

The universal Legendre curve is an elliptic curve.

theorem WeierstrassCurve.UniversalLegendre.Ring.ringHom_ext {S : Type u_2} [Semiring S] {f g : Ring →+* S} (h : f param = g param) : f = g

Two ring homomorphisms out of ℤ[1/2][λ, 1/λ(λ - 1)] are equal as soon as they agree on the parameter λ.

theorem WeierstrassCurve.UniversalLegendre.Ring.ringHom_ext_iff {S : Type u_2} [Semiring S] {f g : Ring →+* S} : f = g ↔ f param = g param

noncomputable def WeierstrassCurve.UniversalLegendre.lift {R : Type u_1} [CommRing R] {l : R} (h : IsUnit (2 * l * (l - 1))) : Ring →+* R

The classifying homomorphism ℤ[1/2][λ, 1/λ(λ - 1)] →+* R of an element l of R with 2l(l - 1) a unit, sending λ to l.

theorem WeierstrassCurve.UniversalLegendre.lift_comp_algebraMap {R : Type u_1} [CommRing R] {l : R} (h : IsUnit (2 * l * (l - 1))) : (lift h).comp (algebraMap (Polynomial ℤ) Ring) = Polynomial.eval₂RingHom (Int.castRingHom R) l

Restricted to the polynomial ring ℤ[λ], the classifying homomorphism substitutes l for λ. Use this shape when composing ring maps and lift_algebraMap when rewriting underneath an application.

theorem WeierstrassCurve.UniversalLegendre.lift_algebraMap {R : Type u_1} [CommRing R] {l : R} (h : IsUnit (2 * l * (l - 1))) (p : Polynomial ℤ) : (lift h) ((algebraMap (Polynomial ℤ) Ring) p) = (Polynomial.eval₂RingHom (Int.castRingHom R) l) p

The pointwise form of lift_comp_algebraMap.

@[simp]

theorem WeierstrassCurve.UniversalLegendre.lift_param {R : Type u_1} [CommRing R] {l : R} (h : IsUnit (2 * l * (l - 1))) : (lift h) param = l

theorem WeierstrassCurve.UniversalLegendre.comp_lift {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (φ : R →+* S) {l : R} (h : IsUnit (2 * l * (l - 1))) : φ.comp (lift h) = lift ⋯

The classifying homomorphism is natural in the base ring: followed by a ring homomorphism φ : R →+* S, the classifying homomorphism of l is that of φ l.

theorem WeierstrassCurve.UniversalLegendre.eq_lift {R : Type u_1} [CommRing R] {l : R} (h : IsUnit (2 * l * (l - 1))) {f : Ring →+* R} (hf : f param = l) : f = lift h

The classifying homomorphism is unique: a ring homomorphism out of ℤ[1/2][λ, 1/λ(λ - 1)] sending λ to l is lift.

@[simp]

theorem WeierstrassCurve.UniversalLegendre.map_lift {R : Type u_1} [CommRing R] {l : R} (h : IsUnit (2 * l * (l - 1))) : curve.map (lift h) = TauCeti.freyCurve 1 (-l)

Every Legendre form y² = x (x - 1) (x - l) with 2l(l - 1) a unit is the base change of the universal Legendre curve along its classifying homomorphism.

theorem WeierstrassCurve.UniversalLegendre.existsUnique_legendre {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x₁ y₁ x₂ y₂ : R} (u : Rˣ) [W.IsElliptic] (h₁ : W.toAffine.Equation x₁ y₁) (h₂ : W.toAffine.Equation x₂ y₂) (hψ₁ : Polynomial.evalEval x₁ y₁ W.ψ₂ = 0) (hψ₂ : Polynomial.evalEval x₂ y₂ W.ψ₂ = 0) (hu : x₂ - x₁ = ↑u ^ 2) : ∃! p : (Ring →+* R) × VariableChange R, p.2.u = u ∧ p.2.r = x₁ ∧ p.2.t = y₁ ∧ ↑p.2.u ^ 2 + p.2.r = x₂ ∧ ↑p.2.u ^ 2 * p.2.s + p.2.t = y₂ ∧ p.2 • W = curve.map p.1

The universal Legendre curve classifies Legendre normalisations. Let W be an elliptic Weierstrass curve, (x₁, y₁) and (x₂, y₂) points of W at which ψ₂ vanishes, and u a unit with x₂ - x₁ = u². Then there is exactly one pair of a ring homomorphism f : ℤ[1/2][λ, 1/λ(λ - 1)] →+* R and a change of variables C with scaling u such that C carries W to the base change of the universal Legendre curve along f, (x₁, y₁) to (0, 0) and (x₂, y₂) to (1, 0). This is an equation-level statement: it models the Legendre structures of Katz and Mazur only after identifying the two points with a basis of E[2] and u with the differential u times the invariant differential of W.