The Weierstrass fixed-point series and the chord data

Source: MichaelStollBayreuth/EllipticCurves at commit 3f8c39c0fc4c0fd0a40e693aa2a9bbda08d9ee1f. Exact-pin changes are documented in PORTING.md.

For a Weierstrass curve W over a commutative ring O, this file builds the fixed-point series w(t) ∈ O⟦t⟧ (solution of w = t³ + a₁tw + a₂t²w + a₃w² + a₄tw² + a₆w³) and the two-variable chord data of the curve (t, w(t)): slopeSeries, interceptSeries, thirdRootSeries, addSeries, and the inverse inverseSeries, with their basic identities, the swap-invariance giving commutativity, the t₂ = 0 specialization, and naturality under coefficient-ring maps.

noncomputable def WeierstrassCurve.wStepAt {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) (q v : PowerSeries O) : PowerSeries O

The right-hand side of the Weierstrass equation in the coordinates (t, w), with the parameter series q in place of t and the unknown v in place of w.

Equations

• W.wStepAt 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

noncomputable def WeierstrassCurve.wStep {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) (w : PowerSeries O) : PowerSeries O

One step of the fixed-point iteration defining wSeries: the right-hand side of the Weierstrass equation in the coordinates (t, w).

Equations

• W.wStep w = W.wStepAt PowerSeries.X w

noncomputable def WeierstrassCurve.wSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : PowerSeries O

The power series w(t) ∈ O⟦t⟧ describing a Weierstrass curve near the origin in the coordinates t = -x/y, w = -1/y: the unique solution with w ≡ t³ mod t⁴ of the fixed-point equation wSeries_eq (Silverman, IV.1.1), obtained as the t-adic limit of the iteration of the right-hand side starting at 0.

Equations

• W.wSeries = PowerSeries.mk fun (n : ℕ) => (PowerSeries.coeff n) (W.wStep^[n + 1] 0)

theorem WeierstrassCurve.X_pow_three_dvd_wSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : PowerSeries.X ^ 3 ∣ W.wSeries

@[simp]

theorem WeierstrassCurve.constantCoeff_wSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : PowerSeries.constantCoeff W.wSeries = 0

theorem WeierstrassCurve.coeff_wSeries_of_lt {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) {k : ℕ} (hk : k < 3) : (PowerSeries.coeff k) W.wSeries = 0

@[simp]

theorem WeierstrassCurve.coeff_wSeries_three {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : (PowerSeries.coeff 3) W.wSeries = 1

theorem WeierstrassCurve.wSeries_eq {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : W.wSeries = PowerSeries.X ^ 3 + PowerSeries.C W.a₁ * PowerSeries.X * W.wSeries + PowerSeries.C W.a₂ * PowerSeries.X ^ 2 * W.wSeries + PowerSeries.C W.a₃ * W.wSeries ^ 2 + PowerSeries.C W.a₄ * PowerSeries.X * W.wSeries ^ 2 + PowerSeries.C W.a₆ * W.wSeries ^ 3

The defining fixed-point equation of wSeries, i.e. the Weierstrass equation in the coordinates (t, w).

noncomputable def WeierstrassCurve.vSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : PowerSeries O

The unit part of wSeries: w = t³·v with v(0) = 1.

Equations

• W.vSeries = Exists.choose ⋯

theorem WeierstrassCurve.wSeries_eq_X_pow_three_mul {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : W.wSeries = PowerSeries.X ^ 3 * W.vSeries

@[simp]

theorem WeierstrassCurve.constantCoeff_vSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : PowerSeries.constantCoeff W.vSeries = 1

The chord construction

The slope and intercept of the chord through the points with parameters t₁, t₂ on the curve (t, w(t)), as power series in O⟦t₁, t₂⟧ (variables indexed by Unit ⊕ Unit, as in the formal-group-law kit).

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

The slope (divided difference) series λ(t₁, t₂) = (w(t₂) - w(t₁))/(t₂ - t₁), defined directly by its coefficients: the coefficient of t₁ⁱt₂ʲ is the coefficient of t^(i+j+1) in wSeries.

Equations

• W.slopeSeries d = (PowerSeries.coeff (d (Sum.inl ()) + d (Sum.inr ()) + 1)) W.wSeries

theorem WeierstrassCurve.coeff_slopeSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) (d : Unit ⊕ Unit →₀ ℕ) : (MvPowerSeries.coeff d) W.slopeSeries = (PowerSeries.coeff (d (Sum.inl ()) + d (Sum.inr ()) + 1)) W.wSeries

theorem WeierstrassCurve.slopeSeries_mul_sub {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : W.slopeSeries * (MvPowerSeries.X (Sum.inr ()) - MvPowerSeries.X (Sum.inl ())) = (MvPowerSeries.rename fun (x : Unit) => Sum.inr ()) W.wSeries - (MvPowerSeries.rename fun (x : Unit) => Sum.inl ()) W.wSeries

The defining property of the slope series: λ(t₁, t₂) · (t₂ - t₁) = w(t₂) - w(t₁).

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

The intercept series ν(t₁, t₂) = w(t₁) - λ(t₁, t₂)·t₁ of the chord through the points with parameters t₁, t₂ on the curve (t, w(t)).

Equations

• W.interceptSeries = (MvPowerSeries.rename fun (x : Unit) => Sum.inl ()) W.wSeries - W.slopeSeries * MvPowerSeries.X (Sum.inl ())

theorem WeierstrassCurve.interceptSeries_eq {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : W.interceptSeries = (MvPowerSeries.rename fun (x : Unit) => Sum.inr ()) W.wSeries - W.slopeSeries * MvPowerSeries.X (Sum.inr ())

The intercept series is symmetric in the two parameters.

@[simp]

theorem WeierstrassCurve.constantCoeff_slopeSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : MvPowerSeries.constantCoeff W.slopeSeries = 0

theorem WeierstrassCurve.constantCoeff_wSeries_mv {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : MvPowerSeries.constantCoeff W.wSeries = 0

@[simp]

theorem WeierstrassCurve.constantCoeff_interceptSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : MvPowerSeries.constantCoeff W.interceptSeries = 0

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

The third-root series: the parameter t₃(t₁, t₂) of the third intersection point of the chord through the points with parameters t₁, t₂ with the curve (t, w(t)). By Vieta applied to the cubic in t obtained by substituting w = λt + ν into the Weierstrass equation, t₃ = -t₁ - t₂ - (a₁λ + a₂ν + a₃λ² + 2a₄λν + 3a₆λ²ν)/(1 + a₂λ + a₄λ² + a₆λ³).

Equations

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

@[simp]

theorem WeierstrassCurve.constantCoeff_thirdRootSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : MvPowerSeries.constantCoeff W.thirdRootSeries = 0

noncomputable def WeierstrassCurve.uSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : PowerSeries O

The series u(t) = 1 - a₁t - a₃w(t): minus the denominator y of the coordinates x = t/w, y = -1/w of the negative of the point with parameter t, rescaled by w.

Equations

• W.uSeries = 1 - PowerSeries.C W.a₁ * PowerSeries.X - PowerSeries.C W.a₃ * W.wSeries

@[simp]

theorem WeierstrassCurve.constantCoeff_uSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : PowerSeries.constantCoeff W.uSeries = 1

theorem WeierstrassCurve.mul_invOfUnit_uSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : W.uSeries * W.uSeries.invOfUnit 1 = 1

theorem WeierstrassCurve.isUnit_uSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : IsUnit W.uSeries

noncomputable def WeierstrassCurve.inverseSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : PowerSeries O

The formal inverse parameter series: the parameter ι(t) = -t/(1 - a₁t - a₃w(t)) of the negative of the point with parameter t on the curve (t, w(t)).

Equations

• W.inverseSeries = -(PowerSeries.X * W.uSeries.invOfUnit 1)

@[simp]

theorem WeierstrassCurve.constantCoeff_inverseSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : PowerSeries.constantCoeff W.inverseSeries = 0

theorem WeierstrassCurve.hasSubst_inverseSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : PowerSeries.HasSubst W.inverseSeries

theorem WeierstrassCurve.subst_inverseSeries_wSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : PowerSeries.subst W.inverseSeries W.wSeries = -(W.wSeries * W.uSeries.invOfUnit 1)

Composition with the formal inverse maps w to -w/u (the w-coordinate of the negative of a point).

theorem WeierstrassCurve.subst_inverseSeries_uSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : PowerSeries.subst W.inverseSeries W.uSeries = W.uSeries.invOfUnit 1

Composition with the formal inverse maps u to its inverse.

theorem WeierstrassCurve.subst_inverseSeries_self {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : PowerSeries.subst W.inverseSeries W.inverseSeries = PowerSeries.X

The formal inverse is an involution.

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

The addition series of the chord construction: F(t₁, t₂) = ι(t₃(t₁, t₂)), the parameter of the sum of the points with parameters t₁, t₂.

Equations

• W.addSeries = MvPowerSeries.subst (fun (x : Unit) => W.thirdRootSeries) W.inverseSeries

theorem WeierstrassCurve.hasSubst_thirdRootSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : MvPowerSeries.HasSubst fun (x : Unit) => W.thirdRootSeries

@[simp]

theorem WeierstrassCurve.constantCoeff_addSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : MvPowerSeries.constantCoeff W.addSeries = 0

Swap-invariance of the chord data, giving commutativity of the formal group law.

theorem WeierstrassCurve.rename_swap_slopeSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : (MvPowerSeries.rename Sum.swap) W.slopeSeries = W.slopeSeries

theorem WeierstrassCurve.rename_swap_interceptSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : (MvPowerSeries.rename Sum.swap) W.interceptSeries = W.interceptSeries

theorem WeierstrassCurve.rename_swap_thirdRootSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : (MvPowerSeries.rename Sum.swap) W.thirdRootSeries = W.thirdRootSeries

theorem WeierstrassCurve.rename_swap_addSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : (MvPowerSeries.rename Sum.swap) W.addSeries = W.addSeries

Specialization of the chord data at t₂ = 0: the slope becomes w(t)/t, the intercept vanishes, and the third root becomes the formal inverse ι(t).

theorem WeierstrassCurve.subst_zero_of_constantCoeff_zero_compat {O : Type u_1} [CommRing O] {σ : Type u_2} {τ : Type u_3} (f : MvPowerSeries σ O) (hf : MvPowerSeries.constantCoeff f = 0) : MvPowerSeries.subst 0 f = 0

theorem WeierstrassCurve.subst_unitR_thirdRootSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : MvPowerSeries.subst (Sum.elim MvPowerSeries.X fun (x : Unit) => 0) W.thirdRootSeries = W.inverseSeries

Specializing the third-root series at t₂ = 0 gives the formal inverse.

theorem WeierstrassCurve.subst_unitR_addSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : MvPowerSeries.subst (Sum.elim MvPowerSeries.X fun (x : Unit) => 0) W.addSeries = PowerSeries.X

Adding the zero point does nothing: specialization of the addition series at t₂ = 0 is the identity.

theorem WeierstrassCurve.subst_unitL_addSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : MvPowerSeries.subst (Sum.elim (fun (x : Unit) => 0) MvPowerSeries.X) W.addSeries = PowerSeries.X

Adding the zero point on the left does nothing either, by commutativity.

theorem WeierstrassCurve.coeff_single_inl_addSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : (MvPowerSeries.coeff fun₀ | Sum.inl () => 1) W.addSeries = 1

The linear coefficient of the addition series in the first variable is 1.

theorem WeierstrassCurve.coeff_single_inr_addSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : (MvPowerSeries.coeff fun₀ | Sum.inr () => 1) W.addSeries = 1

The linear coefficient of the addition series in the second variable is 1.

theorem WeierstrassCurve.coeff_addSeries_sub_of_degree_lt {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) {d : Unit ⊕ Unit →₀ ℕ} (hd : Finsupp.degree d < 2) : (MvPowerSeries.coeff d) (W.addSeries - MvPowerSeries.X (Sum.inl ()) - MvPowerSeries.X (Sum.inr ())) = 0

Below total degree 2, the addition series agrees with t₁ + t₂: the formal group law is F(t₁, t₂) = t₁ + t₂ + (higher order).

Naturality of the chord construction under coefficient ring maps

Every ingredient of the chord construction commutes with base change along a ring homomorphism φ : O →+* O'. This is the reduction engine for associativity: it transports identities from the universal Weierstrass curve over ℤ[A₁, …, A₆] to any curve.

theorem WeierstrassCurve.map_wSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) {O' : Type u_2} [CommRing O'] (φ : O →+* O') : (PowerSeries.map φ) W.wSeries = (W.map φ).wSeries

theorem WeierstrassCurve.map_slopeSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) {O' : Type u_2} [CommRing O'] (φ : O →+* O') : (MvPowerSeries.map φ) W.slopeSeries = (W.map φ).slopeSeries

theorem WeierstrassCurve.map_interceptSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) {O' : Type u_2} [CommRing O'] (φ : O →+* O') : (MvPowerSeries.map φ) W.interceptSeries = (W.map φ).interceptSeries

theorem WeierstrassCurve.map_uSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) {O' : Type u_2} [CommRing O'] (φ : O →+* O') : (PowerSeries.map φ) W.uSeries = (W.map φ).uSeries

theorem WeierstrassCurve.map_thirdRootSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) {O' : Type u_2} [CommRing O'] (φ : O →+* O') : (MvPowerSeries.map φ) W.thirdRootSeries = (W.map φ).thirdRootSeries

theorem WeierstrassCurve.map_inverseSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) {O' : Type u_2} [CommRing O'] (φ : O →+* O') : (PowerSeries.map φ) W.inverseSeries = (W.map φ).inverseSeries

theorem WeierstrassCurve.map_addSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) {O' : Type u_2} [CommRing O'] (φ : O →+* O') : (MvPowerSeries.map φ) W.addSeries = (W.map φ).addSeries