Points of order two on the Weierstrass equation

Let W be a Weierstrass curve over a field F, and let T = (e, t) be a solution of the Weierstrass equation at which ψ₂(e, t) = 2t + a₁e + a₃ vanishes, so that T is its own negative. Write

c_T = -W_X(e, t) = 3e² + 2a₂e + a₄ - a₁t

for the value at T of minus the partial derivative of the Weierstrass polynomial in X. It is nonzero when T is nonsingular, since the other partial derivative ψ₂(e, t) vanishes; when the equation is y² = (x - e)(x - e')(x - e''), it is (e - e')(e - e'').

This file records the facts about such solutions that do not involve the group law, valid in every characteristic: (e, t) is the only solution over e, and two of them T = (e, t) and T₀ = (e₀, t₀) with e₀ ≠ e have c_T + c_{T₀} = (e - e₀)². The characterization of ψ₂ = 0 holds over any commutative ring, uniqueness over e holds over any reduced commutative ring, and the identity for c_T + c_{T₀} holds over any commutative ring without zero divisors. The formulas for translation by a point of order two are in TauCeti.AlgebraicGeometry.EllipticCurve.Affine.Point.TwoTorsion.

Main results

• WeierstrassCurve.Affine.evalEval_polynomialY_eq_zero_iff: ψ₂(x, y) = 0 exactly when y = negY x y.
• WeierstrassCurve.Affine.Y_eq_of_evalEval_polynomialY_eq_zero: if ψ₂(e, t) = 0, the only solution over e is (e, t).
• WeierstrassCurve.Affine.evalEval_polynomialX_add_evalEval_polynomialX: for two distinct points of order two, c_T + c_{T₀} = (e - e₀)².

References

• J. Silverman, The Arithmetic of Elliptic Curves, X.1.4.

theorem WeierstrassCurve.Affine.evalEval_polynomialY_eq_zero_iff {R : Type u_1} [CommRing R] {W : Affine R} {x y : R} : Polynomial.evalEval x y W.polynomialY = 0 ↔ y = W.negY x y

ψ₂ vanishes exactly at the points that are their own negatives: ψ₂(x, y) = 0 ↔ y = negY x y.

theorem WeierstrassCurve.Affine.Y_eq_of_evalEval_polynomialY_eq_zero {R : Type u_1} [CommRing R] {W : Affine R} {e t : R} [IsReduced R] (hT : W.Equation e t) (hψ : Polynomial.evalEval e t W.polynomialY = 0) {t₀ : R} (hT₀ : W.Equation e t₀) : t₀ = t

The only point over a point of order two is itself: if ψ₂(e, t) = 0 and (e, t₀) lies on the curve, then t₀ = t.

theorem WeierstrassCurve.Affine.X_ne_of_evalEval_polynomialY_ne_zero {R : Type u_1} [CommRing R] {W : Affine R} {e t x y : R} [IsReduced R] (hT : W.Equation e t) (hψ : Polynomial.evalEval e t W.polynomialY = 0) (h : W.Equation x y) (hy : Polynomial.evalEval x y W.polynomialY ≠ 0) : x ≠ e

A point with ψ₂ ≠ 0 does not lie over a point of order two: if ψ₂(e, t) = 0 and ψ₂(x, y) ≠ 0, then x ≠ e, since the only point over e is (e, t).

theorem WeierstrassCurve.Affine.evalEval_polynomialX_add_evalEval_polynomialX {R : Type u_1} [CommRing R] {W : Affine R} {e t : R} [NoZeroDivisors R] {e₀ t₀ : R} (hT : W.Equation e t) (hψ : Polynomial.evalEval e t W.polynomialY = 0) (hT₀ : W.Equation e₀ t₀) (hψ₀ : Polynomial.evalEval e₀ t₀ W.polynomialY = 0) (he : e₀ ≠ e) : Polynomial.evalEval e t W.polynomialX + Polynomial.evalEval e₀ t₀ W.polynomialX = -(e - e₀) ^ 2

Two distinct points of order two: if (e, t) and (e₀, t₀) both have ψ₂ = 0 and e₀ ≠ e, then W_X(e, t) + W_X(e₀, t₀) = -(e - e₀)², that is c_T + c_{T₀} = (e - e₀)². When the equation is y² = (x - e)(x - e₀)(x - e''), this is (e - e₀)(e - e'') + (e₀ - e)(e₀ - e'') = (e - e₀)².