The formal inverse of a Weierstrass curve #

In the (z, w)-chart of WeierstrassCurve.formalW, where x = z / w and y = -1 / w, the negative of the point with parameter z has parameter ι(z) = -z / (1 - a₁ z - a₃ w(z)). This file constructs that series and proves it is an involution.

The denominator is formalInverseDenom; its constant coefficient is 1, so it is a unit, which is what makes formalInverse a power series at all.

Main definitions #

WeierstrassCurve.formalInverseDenom: the series 1 - a₁ z - a₃ w(z) inverted in ι.
WeierstrassCurve.formalInverse: the parameter ι(z) of the negative point.

Main results #

WeierstrassCurve.subst_formalInverse_self: ι(ι(z)) = z, the formal inverse is an involution. This is the formal-series form of -(-P) = P.
WeierstrassCurve.subst_formalInverse_formalW and WeierstrassCurve.subst_formalInverse_formalInverseDenom: the two substitution identities the involution is assembled from, giving the w-coordinate and the denominator at the negative point.
WeierstrassCurve.isUnit_formalInverseDenom: the denominator is a unit.
WeierstrassCurve.constantCoeff_formalInverse: ι(0) = 0, so ι may itself be substituted into a power series — WeierstrassCurve.hasSubst_formalInverse.

Implementation notes #

The substitution identities are proved through the uniqueness of the solution of the w-equation (WeierstrassCurve.eq_subst_formalW_of_wEquation) rather than by comparing coefficients: w ∘ ι and the candidate -w · u⁻¹ both solve that equation at the parameter ι, and a solution with vanishing constant coefficient is unique.

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/Chord.lean — declarations uSeries, constantCoeff_uSeries, mul_invOfUnit_uSeries, isUnit_uSeries, inverseSeries, constantCoeff_inverseSeries, hasSubst_inverseSeries, subst_inverseSeries_invOfUnit, subst_inverseSeries_wSeries, subst_inverseSeries_uSeries and subst_inverseSeries_self.

The source's uSeries is renamed formalInverseDenom here. It must not be called formalU: that name is already taken, in FormalGroup/WExpansion.lean, by the unit part w(z) / z ^ 3, which is a different series (it is the source's vSeries). The source proves the substitution identities through its own private wStep recursion; this file uses the w-equation API of FormalGroup/WExpansion.lean instead, so the source's wStepAt lemmas are not ported.

The denominator of the formal inverse #

source

noncomputable def WeierstrassCurve.formalInverseDenom {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) :

PowerSeries R

The denominator 1 - a₁ z - a₃ w(z) of the formal inverse.

Up to sign and a factor of w, this is the y-coordinate of the negative of the point with parameter z, in the coordinates x = z / w, y = -1 / w.

Equations

W.formalInverseDenom = 1 - PowerSeries.C W.a₁ * PowerSeries.X - PowerSeries.C W.a₃ * W.formalW

Instances For

source

theorem WeierstrassCurve.formalInverseDenom_def {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) :

W.formalInverseDenom = 1 - PowerSeries.C W.a₁ * PowerSeries.X - PowerSeries.C W.a₃ * W.formalW

The defining formula for formalInverseDenom.

source

@[simp]

theorem WeierstrassCurve.constantCoeff_formalInverseDenom {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) :

PowerSeries.constantCoeff W.formalInverseDenom = 1

The denominator of the formal inverse is 1 at the origin, which is what makes it a unit.

source

theorem WeierstrassCurve.mul_invOfUnit_formalInverseDenom {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) :

W.formalInverseDenom * W.formalInverseDenom.invOfUnit 1 = 1

The denominator times its invOfUnit is 1.

source

theorem WeierstrassCurve.isUnit_formalInverseDenom {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) :

IsUnit W.formalInverseDenom

The denominator of the formal inverse is a unit.

The formal inverse #

source

noncomputable def WeierstrassCurve.formalInverse {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) :

PowerSeries R

The parameter ι(z) = -z / (1 - a₁ z - a₃ w(z)) of the negative of the point with parameter z on the curve (z, w(z)).

Equations

W.formalInverse = -(PowerSeries.X * W.formalInverseDenom.invOfUnit 1)

Instances For

source

theorem WeierstrassCurve.formalInverse_def {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) :

W.formalInverse = -(PowerSeries.X * W.formalInverseDenom.invOfUnit 1)

The defining formula for formalInverse.

source

@[simp]

theorem WeierstrassCurve.constantCoeff_formalInverse {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) :

PowerSeries.constantCoeff W.formalInverse = 0

The formal inverse vanishes at the origin: the negative of O is O.

source

theorem WeierstrassCurve.hasSubst_formalInverse {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) :

PowerSeries.HasSubst W.formalInverse

The formal inverse may be substituted into a power series.

Substituting the formal inverse #

source

theorem WeierstrassCurve.subst_formalInverse_formalW {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) :

PowerSeries.subst W.formalInverse W.formalW = -(W.formalW * W.formalInverseDenom.invOfUnit 1)

Composing the w-expansion with the formal inverse gives -w / (1 - a₁ z - a₃ w), the w-coordinate of the negative point.

Both sides solve the w-equation at the parameter ι and have vanishing constant coefficient, so they agree by eq_subst_formalW_of_wEquation. Clearing the denominator u ^ 3, the identity to check is -w u ^ 2 = -z ^ 3 + a₁ z w u - a₂ z ^ 2 w + a₃ w ^ 2 u - a₄ z w ^ 2 - a₆ w ^ 3, which is the w-equation itself after a₁ z w + a₃ w ^ 2 = w (1 - u).

source