The parametrisation carries the group law: the chord case

FormalGroup/Point/Basic.lean sends a parameter t of an adic ideal to a point of W⁄K, and FormalGroup/PairEval.lean gives the group law F(t₁, t₂) on parameters. This file joins them in the case where the chord through the two points is not vertical: the point of the parameter F(t₁, t₂) is the sum of the points of t₁ and t₂.

This is one case of the additivity of formalPoint, not the whole of it. The doubling case t₁ = t₂ and the inverse case t₂ = ι(t₁) — the two ways the points can share an x-coordinate — each need a different argument and are not treated here. A vanishing parameter is treated, by the unit laws. Only with the two remaining cases does formalPoint become a homomorphism, and only then are the parameters of an adic ideal a subgroup of the points of W⁄K rather than an indexed family of them.

The hypotheses

t₁ * w(t₂) ≠ t₂ * w(t₁) is the chord condition: over a field, where a nonzero parameter t carries the coordinates x = t / w(t) and y = -1 / w(t), it says the two points have distinct x-coordinates, so the line through them is not vertical. It is what excludes the doubling and inverse cases, which need a different argument and are not treated here.

Nothing further is asked of the parameters. w vanishes at 0, so the chord condition already excludes the zero parameter on either side; the sum is nonzero for the same reason, since formalAddEval_eq writes it as the formal inverse of the third root, formalThirdRootEval_ne_zero gives the third root's nonvanishing from the chord condition, and formalInverseEval_ne_zero carries it across; and formalAddEval_mem supplies the membership formalPoint needs of its argument, which is why the conclusion names that term rather than a hypothesis.

mul_formalWEval_eq_mul_formalWEval_iff in Point/Basic.lean characterises the cross-product: it holds exactly when a parameter vanishes, or the two are equal, or they are exchanged by ι. So for two nonzero parameters those two exclusions already give the chord condition. A vanishing parameter is the unit law F(0, t) = t or F(t, 0) = t. That is the second form of the theorem below, and the one a caller can discharge without computing w.

Main results

• WeierstrassCurve.add_eq_formalPoint_formalAddEval_of_X_ne: the point of F(t₁, t₂) is the sum of the points of t₁ and t₂, for parameters whose points have distinct x-coordinates.
• WeierstrassCurve.add_eq_formalPoint_formalAddEval_of_ne_of_ne_formalInverseEval: the same conclusion, asked of the parameters themselves — two nonzero parameters must be distinct and not exchanged by ι, while a vanishing parameter is asked nothing, being a unit law.

Provenance

Adapted from Michael Stoll's EllipticCurves project (github.com/MichaelStollBayreuth/EllipticCurves @ 66889eada51a, Apache-2.0), EllipticCurves/WeierstrassFormalGroup/Filtration.lean, declarations paramPoint_add (the chord case) and formalPoint_add_of_ne (the theorem below). The dichotomy the latter rests on is that source's eq_or_eq_negPoint_of_x_cond, ported as an iff alongside formalPoint in Point/Basic.lean.

The argument here is a transposition of this repository's own FormalGroup/Add/Assoc.lean, whose private thetaPoint_add runs the same chord computation one level up — over a fraction field of the power-series ring rather than at a parameter — for the associativity of formalAdd. The scalar inputs come from the Eval and PairEval layers instead of that file's substitution layer, and formalPoint replaces its thetaPoint.

The points

formalPoint needs the base-changed curve to be elliptic and the structure map to be injective. The group law on points needs decidable equality on K, which the two declarations that add points supply locally by classical reasoning rather than asking it of callers. The first below adds nothing, so it needs neither.

The argument runs in two steps: the chord construction identifies the sum with the third point of the line, and the formal inverse identifies that point's negation with the point of F(t₁, t₂).

@[simp]

theorem WeierstrassCurve.add_eq_formalPoint_formalAddEval_of_X_ne {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] (W : WeierstrassCurve O) {K : Type u_2} [Field K] [Algebra O K] [(W.baseChange K).IsElliptic] [FaithfulSMul O K] {I : Ideal O} (hI : IsAdic I) {t₁ t₂ : O} (h₁ : t₁ ∈ I) (h₂ : t₂ ∈ I) (hx : t₁ * W.formalWEval t₂ ≠ t₂ * W.formalWEval t₁) : W.formalPoint hI h₁ + W.formalPoint hI h₂ = W.formalPoint hI ⋯

The parametrisation carries the group law, for two nonzero parameters whose points have distinct x-coordinates: the point of F(t₁, t₂) is the sum of the points of t₁ and t₂.

The chord through the two points meets the curve again at the parameter t₃(t₁, t₂), and the addition series is the formal inverse of that third root, so the group law of W⁄K applied to the two points computes F(t₁, t₂).

@[simp]

theorem WeierstrassCurve.add_eq_formalPoint_formalAddEval_of_ne_of_ne_formalInverseEval {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] (W : WeierstrassCurve O) {K : Type u_2} [Field K] [Algebra O K] [(W.baseChange K).IsElliptic] [FaithfulSMul O K] {I : Ideal O} (hI : IsAdic I) {t₁ t₂ : O} (h₁ : t₁ ∈ I) (h₂ : t₂ ∈ I) (hne : t₁ ≠ 0 → t₂ ≠ 0 → t₂ ≠ t₁) (hnι : t₁ ≠ 0 → t₂ ≠ 0 → t₂ ≠ W.formalInverseEval t₁) : W.formalPoint hI h₁ + W.formalPoint hI h₂ = W.formalPoint hI ⋯

The parametrisation carries the group law, for two parameters that are not equal and not exchanged by the formal inverse — conditions asked only of a pair that is nowhere zero.

add_eq_formalPoint_formalAddEval_of_X_ne asks instead that the chord through the two points be non-vertical, a condition on the product t₁ * w(t₂). For two nonzero parameters the two requests agree, by mul_formalWEval_eq_mul_formalWEval_iff. The exclusions are guarded on both parameters being nonzero because a vanishing one is a unit law and needs no exclusion at all: t₁ = 0 and t₂ = 0 are both cases of this theorem, t₁ = t₂ = 0 among them.

Tagged @[simp] like the sibling, whose left-hand side it shares. Both carry side conditions simp cannot invent, so reaching either needs the hypotheses passed in, as simp [*] does; the gain here is that they are inequalities of parameters rather than of products of w-values.