The chord through two points of a Weierstrass curve near the origin

The w-expansion of WeierstrassCurve.formalW lives in the coordinates z = -x/y, w = -1/y obtained from the affine coordinates of W by x = z / w, y = -1 / w. In those coordinates the point at infinity is the origin, and the curve is parametrised near it by z ↦ (z, w(z)), where w(z) solves the transformed Weierstrass equation. The (z, w) here are therefore not the affine coordinates of W; everything below happens in the transformed chart.

The substitution turns an affine line of W into a relation w = λ z + ν, so the chord through the two parameters z₁ and z₂ is described by a slope and an intercept, as power series in R⟦z₁, z₂⟧ — variables indexed by Unit ⊕ Unit, as in Mathlib's formal-group-law conventions. Substituting w = λ z + ν into the transformed equation leaves a cubic in z, whose three roots are the parameters of the three points in which the chord meets the curve; the third of them is formalThirdRoot.

Together these are the data of the chord construction: the formal group law of W is obtained from formalThirdRoot by composing with the formal inverse, which is left to a later file.

Main definitions

• WeierstrassCurve.formalSlope: the slope λ(z₁, z₂) = (w(z₂) - w(z₁)) / (z₂ - z₁) of the chord, defined through its coefficients rather than as a quotient.
• WeierstrassCurve.formalIntercept: the intercept ν(z₁, z₂) = w(z₁) - λ(z₁, z₂) z₁.
• WeierstrassCurve.formalThirdRoot: the parameter z₃(z₁, z₂) of the third point in which the chord meets the curve, obtained from Vieta's formulas.

Main results

• WeierstrassCurve.coeff_formalSlope, WeierstrassCurve.formalIntercept_def and WeierstrassCurve.formalThirdRoot_def: the defining formulas, as named lemmas. Rewrite with these rather than unfolding the definitions.
• WeierstrassCurve.formalSlope_mul_X_add: the defining property λ z₂ + w(z₁) = λ z₁ + w(z₂) of the slope over a commutative semiring. Over a ring this becomes λ · (z₂ - z₁) = w(z₂) - w(z₁), which justifies calling it a divided difference.
• WeierstrassCurve.rename_swap_formalSlope, _formalIntercept, _formalThirdRoot: all three series are invariant under exchanging the two parameters, so the chord depends on the two points and not on their order. This is what makes the eventual group law commutative.
• WeierstrassCurve.formalIntercept_eq_inr: the intercept computed from the second point.
• WeierstrassCurve.constantCoeff_formalSlope, _formalIntercept, _formalThirdRoot: all three series vanish at the origin.
• WeierstrassCurve.subst_formalThirdRoot_formalW: the third point really lies on the chord — reading the w-expansion at formalThirdRoot returns the chord line read there. This is what makes the third root the parameter of an intersection point rather than merely a root of the cubic.

Implementation notes

formalSlope is defined by the coefficient formula rather than as a quotient of power series: z₂ - z₁ is not a unit in R⟦z₁, z₂⟧, so the divided difference has to be written down directly and formalSlope_mul_X_add recovers the property that names it.

The slope, its defining relation and the constant coefficient of the third-root denominator need no subtraction, so they are stated over a CommSemiring, matching formalW. The intercept and third-root constructions use subtraction and are stated over a CommRing.

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, revision 66889eada51a), EllipticCurves/WeierstrassFormalGroup/Chord.lean, its Chord section down to the third-root series together with the swap-invariance block — declarations slopeSeries, coeff_slopeSeries, slopeSeries_mul_sub, interceptSeries, interceptSeries_eq, constantCoeff_slopeSeries, constantCoeff_interceptSeries, thirdRootSeries, constantCoeff_thirdRootSeries, rename_swap_slopeSeries, rename_swap_interceptSeries and rename_swap_thirdRootSeries. The source's rename_swap_invOfUnit is not ported: it is the general MvPowerSeries.ringHom_invOfUnit specialised to rename Sum.swap, and is used as such.

The source's wSeries and vSeries are formalW and formalU, so neither is re-ported and everything here is stated over the existing w-expansion API. Where the source writes MvPowerSeries.rename (fun _ => i), this file uses the equal Mathlib map PowerSeries.toMvPowerSeries i.

The on-line section is adapted from the same project's EllipticCurves/WeierstrassFormalGroup/GroupLaw.lean, its Domain section — declarations line_at_thirdRoot and subst_thirdRootSeries_wSeries. Four of that section's steps are not ported. X_inl_ne_X_inr is not needed at all: the cancellation runs through MvPowerSeries.X_sub_X_mem_nonZeroDivisors, which never separates the two variables. The other three this repository already has — line_left and line_right are formalIntercept_def and formalIntercept_eq_inr with the terms moved across the equals sign, and wsAt_rename is subst_formalW_wEquation read through Mathlib's PowerSeries.toMvPowerSeries_eq_subst; all three are inlined at their single use site. The source's LowVanish hypotheses have no counterpart here at all, since eq_of_wEquation_mvPowerSeries takes vanishing constant coefficients directly.

The source guards line_at_thirdRoot with set_option maxRecDepth 4000 in. That is not ported: TauCeti's CI forbids set_option under TauCeti/, and the proof elaborates at the default depth here, so the guard was never load-bearing for this statement.

The slope of the chord

noncomputable def WeierstrassCurve.formalSlope {R : Type u_1} [CommSemiring R] (W : WeierstrassCurve R) : MvPowerSeries (Unit ⊕ Unit) R

The slope of the chord through the points with parameters z₁ and z₂, that is, the divided difference λ(z₁, z₂) = (w(z₂) - w(z₁)) / (z₂ - z₁).

It is defined through its coefficients: the coefficient of z₁ ^ i * z₂ ^ j is the coefficient of z ^ (i + j + 1) in w(z). See formalSlope_mul_X_add for the property this encodes.

Equations

• W.formalSlope d = (PowerSeries.coeff (d (Sum.inl ()) + d (Sum.inr ()) + 1)) W.formalW

@[simp]

theorem WeierstrassCurve.coeff_formalSlope {R : Type u_1} [CommSemiring R] (W : WeierstrassCurve R) (d : Unit ⊕ Unit →₀ ℕ) : (MvPowerSeries.coeff d) W.formalSlope = (PowerSeries.coeff (d (Sum.inl ()) + d (Sum.inr ()) + 1)) W.formalW

The defining formula for formalSlope: the coefficient of z₁ ^ i * z₂ ^ j in the slope is the coefficient of z ^ (i + j + 1) in w(z).

@[simp]

theorem WeierstrassCurve.constantCoeff_formalSlope {R : Type u_1} [CommSemiring R] (W : WeierstrassCurve R) : MvPowerSeries.constantCoeff W.formalSlope = 0

The slope of the chord vanishes at the origin.

theorem WeierstrassCurve.rename_swap_formalSlope {R : Type u_1} [CommSemiring R] (W : WeierstrassCurve R) : (MvPowerSeries.rename Sum.swap) W.formalSlope = W.formalSlope

The slope is unchanged by exchanging the two parameters: it depends on the pair of points and not on their order.

theorem WeierstrassCurve.formalSlope_mul_X_add {R : Type u_1} [CommSemiring R] (W : WeierstrassCurve R) : W.formalSlope * MvPowerSeries.X (Sum.inr ()) + (PowerSeries.toMvPowerSeries (Sum.inl ())) W.formalW = W.formalSlope * MvPowerSeries.X (Sum.inl ()) + (PowerSeries.toMvPowerSeries (Sum.inr ())) W.formalW

The defining property of the slope, without subtraction: λ(z₁, z₂) * z₂ + w(z₁) = λ(z₁, z₂) * z₁ + w(z₂).

Over a ring this is the divided-difference identity λ(z₁, z₂) * (z₂ - z₁) = w(z₂) - w(z₁).

@[simp]

theorem WeierstrassCurve.constantCoeff_formalThirdRootDenom {R : Type u_1} [CommSemiring R] (W : WeierstrassCurve R) : MvPowerSeries.constantCoeff (1 + MvPowerSeries.C W.a₂ * W.formalSlope + MvPowerSeries.C W.a₄ * W.formalSlope ^ 2 + MvPowerSeries.C W.a₆ * W.formalSlope ^ 3) = 1

The denominator 1 + a₂λ + a₄λ² + a₆λ³ of Vieta's formula for the third root is 1 at the origin. Over a commutative ring this makes it a unit, allowing formalThirdRoot to divide by it.

The intercept of the chord

noncomputable def WeierstrassCurve.formalIntercept {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : MvPowerSeries (Unit ⊕ Unit) R

The intercept ν(z₁, z₂) = w(z₁) - λ(z₁, z₂) z₁ of the chord through the points with parameters z₁ and z₂.

Equations

• W.formalIntercept = (PowerSeries.toMvPowerSeries (Sum.inl ())) W.formalW - W.formalSlope * MvPowerSeries.X (Sum.inl ())

theorem WeierstrassCurve.formalIntercept_def {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : W.formalIntercept = (PowerSeries.toMvPowerSeries (Sum.inl ())) W.formalW - W.formalSlope * MvPowerSeries.X (Sum.inl ())

The defining formula for formalIntercept, in terms of the first point.

theorem WeierstrassCurve.formalIntercept_eq_inr {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : W.formalIntercept = (PowerSeries.toMvPowerSeries (Sum.inr ())) W.formalW - W.formalSlope * MvPowerSeries.X (Sum.inr ())

The intercept computed from the second point is the same series.

@[simp]

theorem WeierstrassCurve.constantCoeff_formalIntercept {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : MvPowerSeries.constantCoeff W.formalIntercept = 0

The intercept of the chord vanishes at the origin.

theorem WeierstrassCurve.rename_swap_formalIntercept {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : (MvPowerSeries.rename Sum.swap) W.formalIntercept = W.formalIntercept

The intercept is unchanged by exchanging the two parameters.

The third point of the chord

noncomputable def WeierstrassCurve.formalThirdRoot {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : MvPowerSeries (Unit ⊕ Unit) R

The parameter z₃(z₁, z₂) of the third point in which the chord through the points with parameters z₁ and z₂ meets the curve.

Substituting w = λ z + ν into the transformed Weierstrass equation gives a cubic in z whose roots are the three parameters, so by Vieta's formulas z₃ = -z₁ - z₂ - (a₁λ + a₂ν + a₃λ² + 2a₄λν + 3a₆λ²ν) / (1 + a₂λ + a₄λ² + a₆λ³), the denominator being a unit because λ has vanishing constant coefficient.

Equations

• One or more equations did not get rendered due to their size.

theorem WeierstrassCurve.formalThirdRoot_def {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : W.formalThirdRoot = -MvPowerSeries.X (Sum.inl ()) - MvPowerSeries.X (Sum.inr ()) - (MvPowerSeries.C W.a₁ * W.formalSlope + MvPowerSeries.C W.a₂ * W.formalIntercept + MvPowerSeries.C W.a₃ * W.formalSlope ^ 2 + 2 * MvPowerSeries.C W.a₄ * W.formalSlope * W.formalIntercept + 3 * MvPowerSeries.C W.a₆ * W.formalSlope ^ 2 * W.formalIntercept) * (1 + MvPowerSeries.C W.a₂ * W.formalSlope + MvPowerSeries.C W.a₄ * W.formalSlope ^ 2 + MvPowerSeries.C W.a₆ * W.formalSlope ^ 3).invOfUnit 1

The defining formula for formalThirdRoot, as read off Vieta's formulas.

@[simp]

theorem WeierstrassCurve.constantCoeff_formalThirdRoot {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : MvPowerSeries.constantCoeff W.formalThirdRoot = 0

The parameter of the third point of the chord vanishes at the origin.

theorem WeierstrassCurve.rename_swap_formalThirdRoot {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : (MvPowerSeries.rename Sum.swap) W.formalThirdRoot = W.formalThirdRoot

The third point of the chord is unchanged by exchanging the two parameters. This is what makes the formal group law commutative.

theorem WeierstrassCurve.hasSubst_formalThirdRoot {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : MvPowerSeries.HasSubst fun (x : Unit) => W.formalThirdRoot

The two-variable family that substitutes formalThirdRoot for the single variable of a one-variable series. Stated here, beside formalThirdRoot itself, because the substitution it witnesses is used from this file onwards.

The third point lies on the chord

Vieta's formulas produce formalThirdRoot from the coefficients of the chord cubic, which by itself says nothing about where the curve meets that chord: it is an identity between series, not a statement that the point with parameter z₃ lies on the line w = λ z + ν. It does, and the argument is the classical one — the cubic already has z₁ and z₂ among its roots, so cancelling z₁ - z₂ from the difference of the two identities pins the third.

That cancellation needs no hypothesis on R. The difference of two distinct variables is a non-zero-divisor of MvPowerSeries (Unit ⊕ Unit) R over an arbitrary commutative ring (MvPowerSeries.X_sub_X_mem_nonZeroDivisors), because the coefficient recursion behind it never cancels anything in R.

@[simp]

theorem WeierstrassCurve.subst_formalThirdRoot_formalW {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : MvPowerSeries.subst (fun (x : Unit) => W.formalThirdRoot) W.formalW = W.formalSlope * W.formalThirdRoot + W.formalIntercept

The third intersection point lies on the chord. Reading the w-expansion at the third root gives the chord line read there: w(z₃(z₁, z₂)) = λ(z₁, z₂) · z₃(z₁, z₂) + ν(z₁, z₂).

This is what makes formalThirdRoot the parameter of an actual third intersection point rather than merely the third root of a cubic, and it is the identity the addition series is built on.

Base change

The chord data is built from formalW and the coefficients by ring operations, so it commutes with base change; WExpansion.lean has the corresponding statement for the w-expansion itself.

@[simp]

theorem WeierstrassCurve.map_formalSlope {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {S : Type u_2} [CommRing S] (φ : R →+* S) : (W.map φ).formalSlope = (MvPowerSeries.map φ) W.formalSlope

The slope of the chord commutes with base change.

@[simp]

theorem WeierstrassCurve.map_formalIntercept {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {S : Type u_2} [CommRing S] (φ : R →+* S) : (W.map φ).formalIntercept = (MvPowerSeries.map φ) W.formalIntercept

The intercept of the chord commutes with base change.

@[simp]

theorem WeierstrassCurve.map_formalThirdRoot {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {S : Type u_2} [CommRing S] (φ : R →+* S) : (W.map φ).formalThirdRoot = (MvPowerSeries.map φ) W.formalThirdRoot

The parameter of the third point of the chord commutes with base change.