The chord construction computes the group law

Over a field, a point of a Weierstrass curve W away from the origin can be written in the (z, w)-chart of WeierstrassCurve.formalW as (z / w, -1 / w), coming from the substitution x = z / w, y = -1 / w. This file proves that such a point is nonsingular, and that the chord construction in that chart computes the group law: the third intersection point of the chord through two of them is, after negation, their sum in WeierstrassCurve.Affine.Point.

Everything here is an identity between field elements. The parameters Λ, N and z₃ of the chord enter as hypotheses saying they satisfy the defining relations — the same relations that formalSlope, formalIntercept and formalThirdRoot satisfy as power series — so that this file is independent of the power-series development and can be applied to it later.

Main results

• WeierstrassCurve.chord_point_nonsingular: a point of the (z, w)-chart is nonsingular.
• WeierstrassCurve.chord_point_add: the third point of the chord computes the group law.

References

• J. Silverman, The Arithmetic of Elliptic Curves, IV.1.

Provenance

Adapted from Michael Stoll's EllipticCurves project (github.com/MichaelStollBayreuth/EllipticCurves, Apache-2.0, pinned by TauCetiRoadmap/EllipticCurves/README.md at 66889eada51a), EllipticCurves/WeierstrassFormalGroup/ThirdPoint.lean, its FieldChord section — declarations chord_x_ne, chord_point_nonsingular, chord_addX_addY and chord_point_add.

theorem WeierstrassCurve.chord_point_nonsingular {F : Type u_1} [Field F] (W : WeierstrassCurve F) {q w : F} (hw : w = q ^ 3 + W.a₁ * q * w + W.a₂ * q ^ 2 * w + W.a₃ * w ^ 2 + W.a₄ * q * w ^ 2 + W.a₆ * w ^ 3) (hw0 : w ≠ 0) (hΔ : W.Δ ≠ 0) : W.toAffine.Nonsingular (q / w) (-1 / w)

The parametrized point (q/w, -1/w) is nonsingular whenever (q, w) satisfies the Weierstrass equation in the (z, w)-chart and the discriminant does not vanish.

theorem WeierstrassCurve.chord_point_add {F : Type u_1} [Field F] (W : WeierstrassCurve F) [DecidableEq F] {q₁ q₂ w₁ w₂ Λ N T₃ wT : F} (hw₁ : w₁ = q₁ ^ 3 + W.a₁ * q₁ * w₁ + W.a₂ * q₁ ^ 2 * w₁ + W.a₃ * w₁ ^ 2 + W.a₄ * q₁ * w₁ ^ 2 + W.a₆ * w₁ ^ 3) (hw₂ : w₂ = q₂ ^ 3 + W.a₁ * q₂ * w₂ + W.a₂ * q₂ ^ 2 * w₂ + W.a₃ * w₂ ^ 2 + W.a₄ * q₂ * w₂ ^ 2 + W.a₆ * w₂ ^ 3) (hslope : Λ * (q₂ - q₁) = w₂ - w₁) (hN : N = w₁ - Λ * q₁) (hT₃ : (1 + W.a₂ * Λ + W.a₄ * Λ ^ 2 + W.a₆ * Λ ^ 3) * (T₃ + q₁ + q₂) = -(W.a₁ * Λ + W.a₂ * N + W.a₃ * Λ ^ 2 + 2 * W.a₄ * Λ * N + 3 * W.a₆ * Λ ^ 2 * N)) (hwT : wT = Λ * T₃ + N) (hA : 1 + W.a₂ * Λ + W.a₄ * Λ ^ 2 + W.a₆ * Λ ^ 3 ≠ 0) (hw₁0 : w₁ ≠ 0) (hw₂0 : w₂ ≠ 0) (hwT0 : wT ≠ 0) (hx : q₁ * w₂ - q₂ * w₁ ≠ 0) (h₁ : W.toAffine.Nonsingular (q₁ / w₁) (-1 / w₁)) (h₂ : W.toAffine.Nonsingular (q₂ / w₂) (-1 / w₂)) : ∃ (h₃ : W.toAffine.Nonsingular (T₃ / wT) ((1 - W.a₁ * T₃ - W.a₃ * wT) / wT)), Affine.Point.some (q₁ / w₁) (-1 / w₁) h₁ + Affine.Point.some (q₂ / w₂) (-1 / w₂) h₂ = Affine.Point.some (T₃ / wT) ((1 - W.a₁ * T₃ - W.a₃ * wT) / wT) h₃

The chord construction computes the group law, at the level of nonsingular points.