Translation by a point of order two, and the x-coordinate of a double

Let W be a Weierstrass curve over a field F, and let T = (e, t) be an affine point of order two, so that ψ₂(e, t) = 2t + a₁e + a₃ vanishes, and write c_T = -W_X(e, t) as in TauCeti.AlgebraicGeometry.EllipticCurve.Affine.Formula.TwoTorsion.

An affine point (x, y) has order two exactly when ψ₂(x, y) = 0, and the points S with 2S = O (the 2-torsion) are O, T and the points (e₀, t₀) with ψ₂(e₀, t₀) = 0 and e₀ ≠ e. This file records these facts and the formulas in which c_T appears, valid in every characteristic.

• Translation by T inverts x - e up to c_T: for an affine point P = (x, y) with x ≠ e, (x(P + T) - e)(x - e) = c_T, and ψ₂(P + T)(x - e) = -ψ₂(P)(x(P + T) - e).
• The x-coordinate of a double is e plus a square: for P = (x, y) with ψ₂(x, y) ≠ 0, (x(2P) - e) ψ₂(x, y)² = ((x - e)² - c_T)².

The second formula says that x - e, as a function on the curve, becomes a square after pulling back along multiplication by 2, with square root ((x - e)² - c_T) / ψ₂; the first says how that root transforms under translation by the points of order two. Together they compute the Kummer map of multiplication by 2 (Silverman X.1.4).

Main results

• WeierstrassCurve.Affine.Point.some_add_self_eq_zero_iff: (x, y) has order two exactly when ψ₂(x, y) = 0.
• WeierstrassCurve.Affine.Point.some_mem_torsionBy_two: such a point lies in E[2].
• WeierstrassCurve.Affine.Point.eq_zero_or_eq_or_exists_of_add_self_eq_zero: a point S with 2S = O is O, T, or a point of order two over another root.
• WeierstrassCurve.Affine.Point.xCoord_add_sub_mul_sub: (x(P + T) - e)(x - e) = c_T.
• WeierstrassCurve.Affine.Point.evalEval_polynomialY_add_mul_sub: ψ₂(P + T)(x - e) = -ψ₂(P)(x(P + T) - e).
• WeierstrassCurve.Affine.Point.xCoord_add_self_sub_mul_sq: (x(2P) - e) ψ₂(P)² = ((x - e)² - c_T)².
• WeierstrassCurve.Affine.Point.sq_xCoord_add_sub_add_evalEval_polynomialX_div: the square root ((x - e)² - c_T) / ψ₂ of x(2P) - e is fixed by translation by O and T, and changes sign under translation by the other two points of order two.
• WeierstrassCurve.Affine.Point.xCoord_add_sub: when (x - e)² = c_T, translation by a point of order two sends x - e to ±(x - e), with the same signs.

References

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

theorem WeierstrassCurve.Affine.Point.some_add_self_eq_zero_iff {F : Type u_1} [Field F] [DecidableEq F] {W : Affine F} {x y : F} (h : W.Nonsingular x y) : some x y h + some x y h = 0 ↔ Polynomial.evalEval x y W.polynomialY = 0

An affine point has order two exactly when ψ₂ vanishes there.

theorem WeierstrassCurve.Affine.Point.some_mem_torsionBy_two {F : Type u_1} [Field F] [DecidableEq F] {W : Affine F} {x y : F} (h : W.Nonsingular x y) (hy : Polynomial.evalEval x y W.polynomialY = 0) : some x y h ∈ AddSubgroup.torsionBy W.Point ↑2

An affine point at which ψ₂ vanishes is killed by two.

theorem WeierstrassCurve.Affine.Point.eq_zero_or_eq_or_exists_of_add_self_eq_zero {F : Type u_1} [Field F] [DecidableEq F] {W : Affine F} {e t : F} (hT : W.Nonsingular e t) {S : W.Point} (hS : S + S = 0) : S = 0 ∨ S = some e t hT ∨ ∃ (e₀ : F) (t₀ : F) (hT₀ : W.Nonsingular e₀ t₀), Polynomial.evalEval e₀ t₀ W.polynomialY = 0 ∧ e₀ ≠ e ∧ S = some e₀ t₀ hT₀

The points of order two, seen from any point: for a point T = (e, t), a point S with 2S = O is O, T, or a point (e₀, t₀) with ψ₂(e₀, t₀) = 0 and e₀ ≠ e.

theorem WeierstrassCurve.Affine.Point.xCoord_add_sub_mul_sub {F : Type u_1} [Field F] [DecidableEq F] {W : Affine F} {e t x y : F} (hT : W.Nonsingular e t) (hψ : Polynomial.evalEval e t W.polynomialY = 0) (h : W.Nonsingular x y) (hx : x ≠ e) : ((some x y h + some e t hT).xCoord - e) * (x - e) = -Polynomial.evalEval e t W.polynomialX

Translating by a point of order two inverts x - e up to c_T: if T = (e, t) has ψ₂(e, t) = 0 and P = (x, y) has x ≠ e, then (x(P + T) - e)(x - e) = -W_X(e, t).

theorem WeierstrassCurve.Affine.Point.evalEval_polynomialY_add_mul_sub {F : Type u_1} [Field F] [DecidableEq F] {W : Affine F} {e t x y : F} (hT : W.Nonsingular e t) (hψ : Polynomial.evalEval e t W.polynomialY = 0) (h : W.Nonsingular x y) : Polynomial.evalEval (some x y h + some e t hT).xCoord (some x y h + some e t hT).yCoord W.polynomialY * (x - e) = -Polynomial.evalEval x y W.polynomialY * ((some x y h + some e t hT).xCoord - e)

ψ₂ under translation by a point of order two: if T = (e, t) has ψ₂(e, t) = 0 and P = (x, y) is any affine point, then ψ₂(P + T)(x - e) = -ψ₂(P)(x(P + T) - e).

theorem WeierstrassCurve.Affine.Point.xCoord_add_self_sub_mul_sq {F : Type u_1} [Field F] [DecidableEq F] {W : Affine F} {e t x y : F} (hT : W.Equation e t) (hψ : Polynomial.evalEval e t W.polynomialY = 0) (h : W.Nonsingular x y) (hy : Polynomial.evalEval x y W.polynomialY ≠ 0) : ((some x y h + some x y h).xCoord - e) * Polynomial.evalEval x y W.polynomialY ^ 2 = ((x - e) ^ 2 + Polynomial.evalEval e t W.polynomialX) ^ 2

The x-coordinate of a double is e plus a square: if T = (e, t) has ψ₂(e, t) = 0 and P = (x, y) has ψ₂(x, y) ≠ 0, then (x(2P) - e) ψ₂(x, y)² = ((x - e)² + W_X(e, t))².

theorem WeierstrassCurve.Affine.Point.evalEval_polynomialY_add_ne_zero {F : Type u_1} [Field F] [DecidableEq F] {W : Affine F} {x y : F} (h : W.Nonsingular x y) (hy : Polynomial.evalEval x y W.polynomialY ≠ 0) {S : W.Point} (hS : S + S = 0) : Polynomial.evalEval (some x y h + S).xCoord (some x y h + S).yCoord W.polynomialY ≠ 0

Translating a point with ψ₂ ≠ 0 by a point of order two keeps ψ₂ ≠ 0.

theorem WeierstrassCurve.Affine.Point.sq_xCoord_add_sub_add_evalEval_polynomialX_div {F : Type u_1} [Field F] [DecidableEq F] {W : Affine F} {e t x y : F} (hT : W.Nonsingular e t) (hψ : Polynomial.evalEval e t W.polynomialY = 0) (h : W.Nonsingular x y) (hy : Polynomial.evalEval x y W.polynomialY ≠ 0) {S : W.Point} (hS : S + S = 0) : (((some x y h + S).xCoord - e) ^ 2 + Polynomial.evalEval e t W.polynomialX) / Polynomial.evalEval (some x y h + S).xCoord (some x y h + S).yCoord W.polynomialY = (if S = 0 ∨ S = some e t hT then 1 else -1) * (((x - e) ^ 2 + Polynomial.evalEval e t W.polynomialX) / Polynomial.evalEval x y W.polynomialY)

The square root of x(2P) - e under translation by E[2]: if T = (e, t) has ψ₂(e, t) = 0, P = (x, y) has ψ₂(x, y) ≠ 0 and 2S = O, then r(P + S) = ±r(P) for r = ((x - e)² + W_X(e, t)) / ψ₂, with the sign + exactly when S ∈ {O, T}.

theorem WeierstrassCurve.Affine.Point.xCoord_add_sub {F : Type u_1} [Field F] [DecidableEq F] {W : Affine F} {e t x y : F} (hT : W.Nonsingular e t) (hψ : Polynomial.evalEval e t W.polynomialY = 0) (h : W.Nonsingular x y) (hx2 : (x - e) ^ 2 + Polynomial.evalEval e t W.polynomialX = 0) {S : W.Point} (hS : S + S = 0) : (some x y h + S).xCoord - e = (if S = 0 ∨ S = some e t hT then 1 else -1) * (x - e)

The square root of c_T under translation by E[2]: if T = (e, t) has ψ₂(e, t) = 0, P = (x, y) satisfies (x - e)² = c_T, as when 2P = T, and 2S = O, then x(P + S) - e = ±(x - e), with the sign + exactly when S ∈ {O, T}.