The w-expansion of a Weierstrass curve

Substituting x = z / w and y = -1 / w into the Weierstrass equation of W and clearing denominators turns it into

w = z ^ 3 + a₁ z w + a₂ z ^ 2 w + a₃ w ^ 2 + a₄ z w ^ 2 + a₆ w ^ 3,

which determines a unique power series w(z) ∈ R⟦z⟧ with no terms below z ^ 3. This file constructs that series, proves it satisfies the equation, and proves it is the only series with vanishing constant coefficient that does.

The equation is also recorded with its parameter left free, as WeierstrassCurve.wEquationRHS, and its solution shown unique at every parameter with vanishing constant coefficient: the formal group obtains the inverse and the group law by substitution, and a substituted series solves the equation at the substituted parameter rather than at z.

Main definitions

• WeierstrassCurve.formalWCoeff: the coefficients of w(z), by strong recursion.
• WeierstrassCurve.formalW: the series w(z) itself.
• WeierstrassCurve.formalUCoeff, WeierstrassCurve.formalU: the coefficients, and the series itself, of u(z) = w(z) / z ^ 3.
• WeierstrassCurve.wEquationRHS: the right-hand side of the displayed equation, with both the parameter and the unknown left free.

Main results

• WeierstrassCurve.formalW_wEquation: Silverman AEC IV.1.1(a), existence — w(z) satisfies the displayed equation, as an identity of power series.
• WeierstrassCurve.eq_formalW_of_wEquation: Silverman AEC IV.1.1(a), uniqueness — any power series with vanishing constant coefficient satisfying that equation equals w(z). The two together are the full statement, that w(z) is the such series.
• WeierstrassCurve.eq_of_wEquation: uniqueness at any parameter that itself has vanishing constant coefficient — two series with vanishing constant coefficient solving the equation at that parameter are equal.
• WeierstrassCurve.eq_of_wEquation_mvPowerSeries: that same uniqueness one index type up, for series in MvPowerSeries σ S over any R-algebra S — so it survives scalar extension. It is a sibling of eq_of_wEquation and not a generalisation of it: filtering by total degree needs subtraction, so this one asks for [CommRing S] on the coefficient algebra. The curve's base ring R is a CommSemiring for both.
• WeierstrassCurve.algebraMap_wEquationRHS: the equation's right-hand side commutes with an algebra map, so a solution over a ring is a solution over any algebra over it.
• WeierstrassCurve.wEquation_of_equation: the w-equation is the Weierstrass equation in the coordinates z = -x / y, w = -1 / y.
• WeierstrassCurve.subst_wEquationRHS and WeierstrassCurve.subst_formalW_wEquation: substituting a series q into the equation gives the equation at q, so w(q) solves it there. When moreover constantCoeff q = 0, eq_subst_formalW_of_wEquation combines this with eq_of_wEquation to identify w(q) as the only such solution.
• WeierstrassCurve.formalWCoeff_recurrence: the coefficientwise recurrence — each coefficient of w(z) above the leading one, from the strictly earlier ones. This is the form to compute with; the strong recursion behind formalWCoeff is an implementation detail.
• WeierstrassCurve.formalWCoeff_zero, _one, _two, _three and WeierstrassCurve.formalWCoeff_eq_zero_of_lt: the series begins w(z) = z ^ 3 + ⋯.
• WeierstrassCurve.formalW_eq_X_pow_mul_formalU: w(z) = z ^ 3 * u(z), where WeierstrassCurve.constantCoeff_formalU gives u(0) = 1. Over a CommRing that makes u(z) a unit; at the CommSemiring generality of that section it does not.

Scope

This is the w-expansion only, the foundation of the formal group of W; the group law F(z₁, z₂) is not here. Mathlib's FormalGroup (Mathlib/RingTheory/FormalGroup/Basic.lean) bundles an associativity proof, and associativity of the Weierstrass group law is a separate theorem of real depth, so a FormalGroup term cannot be produced from the w-expansion alone. The directory anticipates that later work.

Provenance

Adapted from the AINTLIB HasseWeil project (github.com/CBirkbeck/AINTLIB, Apache-2.0, pinned by TauCetiRoadmap/EllipticCurves/README.md at dev/hasse-weil @ 513e83879e2f), HasseWeil/FormalGroup.lean, declarations formalW_step, formalW_coeff, formalW, formalU_coeff, the formalW_coeff_* lemmas and formalW_recurrence.

The statement of uniqueness at an arbitrary parameter is adapted from Michael Stoll's EllipticCurves project (github.com/MichaelStollBayreuth/EllipticCurves, Apache-2.0, pinned by TauCetiRoadmap/EllipticCurves/README.md at 66889eada51a), EllipticCurves/WeierstrassFormalGroup/Chord.lean, declarations wStepAt and eq_of_wStepAt_fixed. There the equation is a def used only internally; here it is the public wEquationRHS, so the existing statements in this file are phrased through it too. The univariate proof is not Stoll's: that argues by contraction for the z-adic filtration, which needs subtraction, whereas the coefficient induction used for eq_of_wEquation works at the CommSemiring generality of everything in this file except the substitution lemmas, which are CommRing only because Mathlib's PowerSeries.subst is.

The multivariate uniqueness statement eq_of_wEquation_mvPowerSeries does take Stoll's contraction route, adapted from the same project's EllipticCurves/WeierstrassFormalGroup/ThirdPoint.lean, declarations mvWStepAt and eq_of_mvWStepAt_fixed. Two things there are deliberately not ported. Stoll's mvWStepAt is a second copy of the equation; wEquationRHS is stated over an arbitrary R-algebra, so reading it in MvPowerSeries σ R already is that definition. And Stoll's filtration is carried by a private predicate LowVanish k f, "every coefficient of total degree below k vanishes" — that is Mathlib's MvPowerSeries.order, so the estimates here are stated as (k : ℕ∞) ≤ f.order and the predicate and its nine lemmas are not ported either.

Changes from the AINTLIB source. Its convolution helpers conv₂ and conv₃, and its coefficient and truncation lemmas for them, are stated only for formalW, although none of those proofs uses anything about that series. Generalised to an arbitrary series — and to a Semiring, which is all they need — they are not elliptic-curve material at all, and live in TauCeti.RingTheory.PowerSeries.SelfConvolution, which this file imports and which carries their attribution.

The AINTLIB source works over a commutative ring. Nothing there needs additive inverses — the equation, the recursion and both halves of IV.1.1(a) use only sums and products — so everything here is stated over a CommSemiring, with the single exception of the substitution lemmas, which need Mathlib's PowerSeries.subst and so a CommRing.

The AINTLIB source does not prove uniqueness: its closing note records that the factoring step is blocked by a PowerSeries typeclass gap (RightDistribClass and IsRightCancelAdd failing to synthesize), and names coefficient induction as the untried alternative. That is the route eq_formalW_of_wEquation takes here. Stoll's project does prove uniqueness, by the contraction route recorded above rather than by the coefficient induction used here for the univariate statement.

The AINTLIB source's own generic formal-group scaffolding (FormalGroupLaw, bmul, binv, bpow, bcomp) is deliberately not ported: it predates and duplicates Mathlib's Mathlib/RingTheory/FormalGroup/Basic.lean.

References

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

The series w(z)

noncomputable def WeierstrassCurve.formalWCoeff {R : Type u_1} [CommSemiring R] (W : WeierstrassCurve R) : ℕ → R

The coefficients of the w-expansion of W.

Equations

• W.formalWCoeff = WeierstrassCurve.formalWCoeff._proof_1✝.fix (WeierstrassCurve.formalWStep✝ W)

noncomputable def WeierstrassCurve.formalW {R : Type u_1} [CommSemiring R] (W : WeierstrassCurve R) : PowerSeries R

The w-expansion w(z) of W, as a power series.

Equations

• W.formalW = PowerSeries.mk W.formalWCoeff

noncomputable def WeierstrassCurve.formalUCoeff {R : Type u_1} [CommSemiring R] (W : WeierstrassCurve R) : ℕ → R

The coefficients of the unit part u(z) = w(z) / z ^ 3 of the w-expansion.

Equations

• W.formalUCoeff n = W.formalWCoeff (n + 3)

noncomputable def WeierstrassCurve.formalU {R : Type u_1} [CommSemiring R] (W : WeierstrassCurve R) : PowerSeries R

The unit part u(z) = w(z) / z ^ 3 of the w-expansion, as a power series.

Equations

• W.formalU = PowerSeries.mk W.formalUCoeff

@[simp]

theorem WeierstrassCurve.formalWCoeff_zero {R : Type u_1} [CommSemiring R] (W : WeierstrassCurve R) : W.formalWCoeff 0 = 0

@[simp]

theorem WeierstrassCurve.formalWCoeff_one {R : Type u_1} [CommSemiring R] (W : WeierstrassCurve R) : W.formalWCoeff 1 = 0

@[simp]

theorem WeierstrassCurve.formalWCoeff_two {R : Type u_1} [CommSemiring R] (W : WeierstrassCurve R) : W.formalWCoeff 2 = 0

@[simp]

theorem WeierstrassCurve.formalWCoeff_three {R : Type u_1} [CommSemiring R] (W : WeierstrassCurve R) : W.formalWCoeff 3 = 1

theorem WeierstrassCurve.formalWCoeff_eq_zero_of_lt {R : Type u_1} [CommSemiring R] (W : WeierstrassCurve R) {n : ℕ} (hn : n < 3) : W.formalWCoeff n = 0

The w-expansion has no terms below degree 3.

theorem WeierstrassCurve.formalWCoeff_recurrence {R : Type u_1} [CommSemiring R] (W : WeierstrassCurve R) {n : ℕ} (hn : 3 < n) : W.formalWCoeff n = W.a₁ * W.formalWCoeff (n - 1) + W.a₂ * W.formalWCoeff (n - 2) + W.a₃ * PowerSeries.selfConvTwo W.formalWCoeff n + W.a₄ * PowerSeries.selfConvTwo W.formalWCoeff (n - 1) + W.a₆ * PowerSeries.selfConvThree W.formalWCoeff n

The recurrence characterising the coefficients of w(z) above the leading term: each is determined by the strictly earlier ones. This is the coefficientwise form of formalW_wEquation, and the intended way to compute with formalWCoeff.

@[simp]

theorem WeierstrassCurve.formalUCoeff_apply {R : Type u_1} [CommSemiring R] (W : WeierstrassCurve R) (n : ℕ) : W.formalUCoeff n = W.formalWCoeff (n + 3)

The unit-part coefficients are the coefficients of w(z) shifted down by three.

@[simp]

theorem WeierstrassCurve.coeff_formalW {R : Type u_1} [CommSemiring R] (W : WeierstrassCurve R) (n : ℕ) : (PowerSeries.coeff n) W.formalW = W.formalWCoeff n

@[simp]

theorem WeierstrassCurve.coeff_formalU {R : Type u_1} [CommSemiring R] (W : WeierstrassCurve R) (n : ℕ) : (PowerSeries.coeff n) W.formalU = W.formalUCoeff n

@[simp]

theorem WeierstrassCurve.constantCoeff_formalW {R : Type u_1} [CommSemiring R] (W : WeierstrassCurve R) : PowerSeries.constantCoeff W.formalW = 0

@[simp]

theorem WeierstrassCurve.constantCoeff_formalU {R : Type u_1} [CommSemiring R] (W : WeierstrassCurve R) : PowerSeries.constantCoeff W.formalU = 1

theorem WeierstrassCurve.formalW_eq_X_pow_mul_formalU {R : Type u_1} [CommSemiring R] (W : WeierstrassCurve R) : W.formalW = PowerSeries.X ^ 3 * W.formalU

The w-expansion factors through its unit part: w(z) = z ^ 3 * u(z), where constantCoeff_formalU gives u(0) = 1.

The w-equation

noncomputable def WeierstrassCurve.wEquationRHS {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommSemiring A] [Algebra R A] (W : WeierstrassCurve R) (q v : A) : A

The right-hand side of the w-equation, with the parameter series q in place of z and the unknown v in place of w:

q ^ 3 + a₁ q v + a₂ q ^ 2 v + a₃ v ^ 2 + a₄ q v ^ 2 + a₆ v ^ 3.

The w-expansion is the solution at the parameter q = z, but the formal group needs solutions at other parameters — substituting a series into w(z) solves the equation at that series — so the parameter is left free. Every occurrence of the unknown is multiplied by q or sits in a square or a cube, which is what makes the solution unique (eq_of_wEquation).

Rewrite with wEquationRHS_def rather than unfolding this definition.

Equations

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

theorem WeierstrassCurve.wEquationRHS_def {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommSemiring A] [Algebra R A] (W : WeierstrassCurve R) (q v : A) : W.wEquationRHS q v = q ^ 3 + (algebraMap R A) W.a₁ * q * v + (algebraMap R A) W.a₂ * q ^ 2 * v + (algebraMap R A) W.a₃ * v ^ 2 + (algebraMap R A) W.a₄ * q * v ^ 2 + (algebraMap R A) W.a₆ * v ^ 3

The defining formula for wEquationRHS.

@[simp]

theorem WeierstrassCurve.algebraMap_wEquationRHS {R : Type u_1} [CommSemiring R] (W : WeierstrassCurve R) {A : Type u_2} {B : Type u_3} [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B] (q v : A) : (algebraMap A B) (W.wEquationRHS q v) = W.wEquationRHS ((algebraMap A B) q) ((algebraMap A B) v)

The right-hand side of the w-equation commutes with an algebra map, both the parameter and the unknown being carried along. This is the element-level companion of map_wEquationRHS, which transports series along a ring homomorphism; here the coefficients stay put and only the two arguments move up the tower.

theorem WeierstrassCurve.wEquation_of_equation {O : Type u_2} [CommRing O] {K : Type u_3} [Field K] [Algebra O K] (W : WeierstrassCurve O) {x y : K} (hxy : (W.baseChange K).toAffine.Equation x y) (hy : y ≠ 0) : -y⁻¹ = W.wEquationRHS (-(x / y)) (-y⁻¹)

The w-equation is the Weierstrass equation read in the coordinates z = -x / y, w = -1 / y. Clearing the denominators of y ^ 2 + a₁ x y + a₃ y = x ^ 3 + a₂ x ^ 2 + a₄ x + a₆ at x = z / w, y = -1 / w is what produces that equation in the first place; this is the converse reading, from a point of the curve to a solution of the equation.

The hypothesis is Equation, not Nonsingular: nothing here needs the point to be smooth.

theorem WeierstrassCurve.wEquationRHS_powerSeries {R : Type u_1} [CommSemiring R] (W : WeierstrassCurve R) (q v : PowerSeries R) : W.wEquationRHS q v = q ^ 3 + PowerSeries.C W.a₁ * q * v + PowerSeries.C W.a₂ * q ^ 2 * v + PowerSeries.C W.a₃ * v ^ 2 + PowerSeries.C W.a₄ * q * v ^ 2 + PowerSeries.C W.a₆ * v ^ 3

The w-equation in R⟦z⟧ itself, where the structure map is PowerSeries.C. This is the spelling the coefficient lemmas below match against.

theorem WeierstrassCurve.formalW_wEquation {R : Type u_1} [CommSemiring R] (W : WeierstrassCurve R) : W.formalW = W.wEquationRHS PowerSeries.X W.formalW

Silverman AEC IV.1.1(a), existence. The w-expansion satisfies the equation obtained from the Weierstrass equation of W by the substitution x = z / w, y = -1 / w.

Uniqueness at a parameter with vanishing constant coefficient

The formal group needs uniqueness not only at the parameter z but at any parameter series with vanishing constant coefficient, because the inverse and the group law are obtained by substituting one series into another, and such a substitution solves the equation at the substituted parameter rather than at z. Vanishing of the constant coefficient is exactly what makes the equation determine its solution: it is what forces the n-th coefficient of the right-hand side to depend only on the earlier coefficients of the unknown.

theorem WeierstrassCurve.eq_of_wEquation {R : Type u_1} [CommSemiring R] (W : WeierstrassCurve R) {q v v' : PowerSeries R} (hq : PowerSeries.constantCoeff q = 0) (hv : PowerSeries.constantCoeff v = 0) (hv' : PowerSeries.constantCoeff v' = 0) (h : v = W.wEquationRHS q v) (h' : v' = W.wEquationRHS q v') : v = v'

Uniqueness of the solution of the w-equation. Two power series with vanishing constant coefficient that satisfy the w-equation at the same parameter series q are equal, provided q too has vanishing constant coefficient.

The hypothesis on q is what drives the induction: it is exactly what makes the n-th coefficient of the right-hand side depend only on the coefficients of the unknown strictly below n, so that the equation determines its solution one coefficient at a time.

eq_formalW_of_wEquation is the case q = z, where the solution is moreover identified as formalW W.

theorem WeierstrassCurve.eq_formalW_of_wEquation {R : Type u_1} [CommSemiring R] (W : WeierstrassCurve R) (w : PowerSeries R) (h0 : PowerSeries.constantCoeff w = 0) (hw : w = W.wEquationRHS PowerSeries.X w) : w = W.formalW

Silverman AEC IV.1.1(a), uniqueness. A power series with vanishing constant coefficient that satisfies the w-equation is formalW W. Together with formalW_wEquation this is the full statement of Silverman AEC IV.1.1(a): formalW W is the such series.

Only constantCoeff w = 0 is assumed: the equation at degrees 1 and 2 then forces those two coefficients to vanish as well, because every occurrence of w on its right-hand side is multiplied by X or sits in a square or a cube.

Uniqueness over a multivariate power series ring

eq_of_wEquation argues by strong induction on the coefficient index, which needs that index to be linearly ordered. Over MvPowerSeries σ S no such order is available, so the induction runs on the total degree instead: MvPowerSeries.order is exactly the filtration by total degree, and the right-hand side of the w-equation is a contraction for it. That argument needs additive inverses in the coefficient algebra S, and only there, which is why [CommRing S] appears below while the curve's base ring R stays a CommSemiring; the two uniqueness statements are siblings and neither subsumes the other.

theorem WeierstrassCurve.eq_of_wEquation_mvPowerSeries {R : Type u_1} [CommSemiring R] (W : WeierstrassCurve R) {σ : Type u_2} {S : Type u_3} [CommRing S] [Algebra R S] {q v v' : MvPowerSeries σ S} (hq : MvPowerSeries.constantCoeff q = 0) (hv : MvPowerSeries.constantCoeff v = 0) (hv' : MvPowerSeries.constantCoeff v' = 0) (h : v = W.wEquationRHS q v) (h' : v' = W.wEquationRHS q v') : v = v'

Uniqueness of the solution of the w-equation over a multivariate power series ring. Two series with vanishing constant coefficient that satisfy the w-equation at the same parameter q are equal, provided q too has vanishing constant coefficient.

The coefficients are taken in an arbitrary R-algebra S, matching wEquationRHS itself and the substitution lemmas, so the statement survives scalar extension of the curve's base ring.

This is eq_of_wEquation one index type up. It is not a generalisation of it: the argument here subtracts, so it needs [CommRing S] on the coefficient algebra, whereas the univariate statement needs no inverses at all. The base ring R is a CommSemiring in both.

Substituting into the equation

Substituting a series into the w-equation gives the equation at the substituted parameters. The w-equation makes sense in any commutative R-algebra, and substitution is an R-algebra map, so this is just the statement that wEquationRHS is built from +, *, ^ and the structure map.

With constantCoeff q = 0 — strictly stronger than PowerSeries.HasSubst q, which asks only that the constant coefficient be nilpotent — this combines with eq_of_wEquation to identify the substituted solution, which is eq_subst_formalW_of_wEquation.

Mathlib's PowerSeries.subst is defined only over a CommRing, so this section is stated there; everything above needs no such hypothesis and keeps the CommSemiring of the rest of this file.

theorem WeierstrassCurve.subst_wEquationRHS {R : Type u_2} [CommRing R] (W : WeierstrassCurve R) {τ : Type u_3} {S : Type u_4} [CommRing S] [Algebra R S] {a : MvPowerSeries τ S} (ha : PowerSeries.HasSubst a) (q v : PowerSeries R) : PowerSeries.subst a (W.wEquationRHS q v) = W.wEquationRHS (PowerSeries.subst a q) (PowerSeries.subst a v)

Substitution passes through the w-equation, carrying both the parameter and the unknown with it. Both sides are read in the target algebra, which is why wEquationRHS is stated for an arbitrary R-algebra: substituting a one-variable series into it lands in MvPowerSeries τ S.

theorem WeierstrassCurve.subst_formalW_wEquation {R : Type u_2} [CommRing R] (W : WeierstrassCurve R) {τ : Type u_3} {S : Type u_4} [CommRing S] [Algebra R S] {a : MvPowerSeries τ S} (ha : PowerSeries.HasSubst a) : PowerSeries.subst a W.formalW = W.wEquationRHS a (PowerSeries.subst a W.formalW)

The w-expansion composed with a substitutable series a solves the w-equation at a.

theorem WeierstrassCurve.eq_subst_formalW_of_wEquation {R : Type u_2} [CommRing R] (W : WeierstrassCurve R) {q v : PowerSeries R} (hq : PowerSeries.constantCoeff q = 0) (hv : PowerSeries.constantCoeff v = 0) (h : v = W.wEquationRHS q v) : v = PowerSeries.subst q W.formalW

The substituted w-expansion is the unique solution at the substituted parameter. For a parameter q with vanishing constant coefficient, any series with vanishing constant coefficient solving the w-equation at q is w(q).

This is the composite the formal group consumes: subst_formalW_wEquation supplies a solution and eq_of_wEquation says there is only one. Note the hypothesis is constantCoeff q = 0 rather than PowerSeries.HasSubst q; the latter asks only for a nilpotent constant coefficient, which is not enough for uniqueness.

Base change

Every coefficient of the w-expansion is a polynomial in a₁, …, a₆, so it commutes with base change along a ring homomorphism. This is what lets an identity between w-expansions be proved once over the universal Weierstrass curve and specialised to any curve.

@[simp]

theorem WeierstrassCurve.map_wEquationRHS {R : Type u_2} [CommRing R] (W : WeierstrassCurve R) {S : Type u_3} [CommRing S] (φ : R →+* S) (q v : PowerSeries R) : (W.map φ).wEquationRHS ((PowerSeries.map φ) q) ((PowerSeries.map φ) v) = (PowerSeries.map φ) (W.wEquationRHS q v)

Base change passes through the right-hand side of the w-equation, carrying the parameter and the unknown with it.

@[simp]

theorem WeierstrassCurve.map_formalW {R : Type u_2} [CommRing R] (W : WeierstrassCurve R) {S : Type u_3} [CommRing S] (φ : R →+* S) : (W.map φ).formalW = (PowerSeries.map φ) W.formalW

The w-expansion commutes with base change. Both sides have vanishing constant coefficient and solve the w-equation of W.map φ, and that solution is unique.