The chord group law over the fraction field of the series ring #

Associativity of the chord addition series, F(F(t₁, t₂), t₃) = F(t₁, F(t₂, t₃)), proved by transporting the honest group law of a Weierstrass curve. The parameters are power series, so the curve has to be read over a field containing them: this file base changes W along O → MvPowerSeries σ O → KK, records the w-equation there, and identifies a parameter with the point (q, w(q)) it names. Chord addition of those points is the addition series, so associativity of the curve's group law is associativity of the series.

That argument needs a domain, so it runs over the universal curve, whose base ℤ[A₁, ⋯, A₆] supplies one; map_specialize carries the conclusion to every W over every commutative ring.

Main statements #

WeierstrassCurve.formalAdd_assoc : the associativity of the addition series, for every Weierstrass curve over every commutative ring. It is this module's only exported result; the fraction-field base change, the parametrized point θ and the chord additions it satisfies are private implementation details of its proof.

Provenance #

Adapted from Michael Stoll's EllipticCurves project (github.com/MichaelStollBayreuth/EllipticCurves, Apache-2.0) at commit 66889eada51a74c2f5dfb7fb5909b0b5a0a2d96e, EllipticCurves/WeierstrassFormalGroup/GroupLaw.lean, sections Domain and Assembly, declarations subst_wSeries_ne_zero, fracCurve, rho_weierstrass, thetaPoint, thetaPoint_add, thetaPoint_neg, thetaPoint_inj and pair_intercept_ne_zero_of_ne, together with the single-parameter helpers single_u_mul, single_iota_eq, single_u_eq and single_wIota from EllipticCurves/WeierstrassFormalGroup/ThirdPoint.lean.

Two of those are proved differently here, because this repository already has the content in a more usable form. pair_intercept_ne_zero_of_ne collapses the cross combination with the single rewrite subst_pair_formalIntercept_mul_sub where the source combines its two intercept readings by hand; and Stoll's hA step inside thetaPoint_add argues through the constant coefficient, whereas subst_pair_thirdRootDenom_mul already exhibits an explicit inverse. The four single-parameter helpers are likewise transports of the FormalGroup/Inverse.lean identities along PowerSeries.subst q, not re-derivations of them.

The source's wSeries and vSeries are formalW and formalU here, continuing the renaming this repository applies to that development, so subst_wSeries_ne_zero is subst_formalW_ne_zero.

The Universal section of the same file (declarations universal_Δ_ne_zero and assoc_addSeries_universal) is fracCurve_universal_Δ_ne_zero and assoc_formalAdd_universal here. Four of that section's nine declarations are not ported, because this repository already has them: universal, exists_map_universal and universal_Δ_ne_zero are Universal.curve, map_specialize and Universal.curve_Δ_ne_zero, and the source's X_ne_X and X_ne_zero' are Mathlib's MvPowerSeries.X_inj and nonZeroDivisors.ne_zero MvPowerSeries.X_mem_nonzeroDivisors.

The source's interceptSeries_ne_zero and X_pair_intercept_ne_zero have no counterpart. The source needs them only because it supplies the nonvanishing intercept two different ways, an elementary one at a pair of distinct variables and pair_intercept_ne_zero_of_ne elsewhere; here pair_intercept_ne_zero_of_ne covers the variable pairs too, so thetaPoint_add_of_ne serves all four chord additions of the assembly.

The assembly also runs two specializations of the three parameters where the source runs one. The source separates the middle parameter from the third with X_ne_X, a syntactic argument; the corresponding hypothesis here is q₂ ≠ ι(q₃), which no syntactic argument reaches, so χ' sends the middle parameter to X and the other two to 0 exactly as χ does for the first.

The statement is adapted rather than transcribed, because this repository states the w-equation differently. Stoll carries a second copy of the equation as a private def mvWStepAt and phrases the fixed-point property as subst_wSeries_fix; here wEquationRHS is already stated over an arbitrary algebra, so reading it in KK is that definition, and subst_formalW_wEquation supplies the fixed-point property. Stoll's proof is congrArg followed by unfolding mvWStepAt; the corresponding step here has to move the coefficients across the base change instead, which is what fracCurve in the statement records.

The formal inverse at a parameter #

Reading a pair through a further substitution #

The parametrized point #

Associativity #

source

theorem WeierstrassCurve.formalAdd_assoc {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) :

Associativity of the chord addition series, for every Weierstrass curve over every commutative ring: F(F(t₁, t₂), t₃) = F(t₁, F(t₂, t₃)).

The chord construction proves this only where the curve has a group law to borrow, so the identity is proved for the universal curve — whose base ℤ[A₁, ⋯, A₆] is a domain, and whose series ring therefore has a fraction field — and map_specialize carries it to every W.

The three variables are indexed by Unit ⊕ Unit ⊕ Unit, with the two bracketings written as nested substitutions of formalAdd into itself.

Documentation