The formal group law of a Weierstrass curve

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

Over the fraction field of a domain, the addition series realizes the group law of the curve (t, w(t)) (the Domain and Assembly sections); the universal curve over ℤ[A₁, …, A₆]⟦…⟧ then yields associativity (Universal). Assembling all the axioms gives WeierstrassCurve.formalGroupLaw, the one-dimensional ChabautyColeman.FormalGroupLaw of the curve, together with the inverse property subst_inverseSeries_addSeries.

theorem WeierstrassCurve.subst_thirdRootSeries_wSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) [IsDomain O] : MvPowerSeries.subst (fun (x : Unit) => W.thirdRootSeries) W.wSeries = W.slopeSeries * W.thirdRootSeries + W.interceptSeries

The third intersection point lies on the chord: w(t₃(t₁, t₂)) = λ(t₁, t₂)·t₃(t₁, t₂) + ν(t₁, t₂).

Assembly: the addition series realizes the group law over the fraction field

noncomputable def WeierstrassCurve.universal : WeierstrassCurve (MvPolynomial (Fin 5) ℤ)

The universal Weierstrass curve, over ℤ[A₁, A₂, A₃, A₄, A₆].

Equations

• WeierstrassCurve.universal = { a₁ := MvPolynomial.X 0, a₂ := MvPolynomial.X 1, a₃ := MvPolynomial.X 2, a₄ := MvPolynomial.X 3, a₆ := MvPolynomial.X 4 }

theorem WeierstrassCurve.exists_map_universal {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : ∃ (φ : MvPolynomial (Fin 5) ℤ →+* O), universal.map φ = W

Every Weierstrass curve is a base change of the universal one.

theorem WeierstrassCurve.assoc_addSeries_universal : MvPowerSeries.subst (ChabautyColeman.assocLeftFam fun (x : Unit) => universal.addSeries) universal.addSeries = MvPowerSeries.subst (ChabautyColeman.assocRightFam fun (x : Unit) => universal.addSeries) universal.addSeries

theorem WeierstrassCurve.assoc_addSeries {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : MvPowerSeries.subst (ChabautyColeman.assocLeftFam fun (x : Unit) => W.addSeries) W.addSeries = MvPowerSeries.subst (ChabautyColeman.assocRightFam fun (x : Unit) => W.addSeries) W.addSeries

Associativity of the addition series, for any Weierstrass curve, by reduction to the universal one.

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

The formal inverse property F(t, ι(t)) = 0: the addition series vanishes along the pair (t, ι(t)), for any Weierstrass curve — proved for the universal curve via the chord geometry (the chord through a point and its inverse has intercept 0, so its third root is 0 by Vieta) and transported by naturality.

noncomputable def WeierstrassCurve.formalGroupLaw {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) : ChabautyColeman.FormalGroupLaw O Unit

The formal group law of a Weierstrass curve: the power series F(t₁, t₂) giving the t-coordinate of the sum of the points with parameters t₁, t₂ on the curve (t, w(t)), via the chord construction (Silverman, IV.1.1). One-dimensional, so the index type is Unit. Associativity is proved via the group law of the universal curve over the fraction field of ℤ[A₁, …, A₆]⟦t₁, t₂, t₃⟧.

Equations

• W.formalGroupLaw = { F := fun (x : Unit) => W.addSeries, zero_constantCoeff := ⋯, add_zero' := ⋯, zero_add' := ⋯, comm' := ⋯, assoc' := ⋯ }