The formal group law of a Weierstrass curve

The chord construction at the point at infinity gives an addition series formalAdd W. This file packages that series as Mathlib's one-dimensional FormalGroup: the two variables are reindexed from the named sum Unit ⊕ Unit to Fin 2, and the previously established constant, linear, and associativity identities supply the structure fields.

The resulting formal group is commutative because the chord addition series is symmetric. Thus Mathlib's FormalGroup.Point construction gives an additive commutative monoid of power-series-valued points whose constant coefficient is nilpotent.

Main definitions

• WeierstrassCurve.formalGroup: the one-dimensional formal group law attached to a Weierstrass curve.

Main results

• WeierstrassCurve.isComm_formalGroup: the elliptic formal group law is commutative.
• WeierstrassCurve.map_formalGroup: the construction commutes with base change.

References

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

Provenance

The addition series and its laws are adapted in the imported modules from Michael Stoll's EllipticCurves project (github.com/MichaelStollBayreuth/EllipticCurves, Apache-2.0) at commit 66889eada51a74c2f5dfb7fb5909b0b5a0a2d96e. The packaging here is original: that source uses its own formal-group-law structure, whereas this development refounds the construction on Mathlib's RingTheory/FormalGroup API.

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

The one-dimensional commutative formal group law of a Weierstrass curve, obtained by reindexing the chord addition series from Unit ⊕ Unit to Mathlib's Fin 2 convention.

Equations

• W.formalGroup = { toPowerSeries := (MvPowerSeries.rename ⇑unitSumUnitEquivFinTwo) W.formalAdd, zero_constantCoeff := ⋯, lin_coeff_X := ⋯, lin_coeff_Y := ⋯, assoc := ⋯ }

@[simp]

theorem WeierstrassCurve.formalGroup_toPowerSeries {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : W.formalGroup.toPowerSeries = (MvPowerSeries.rename ⇑unitSumUnitEquivFinTwo) W.formalAdd

The underlying Fin 2-indexed series of the formal group law is the reindexed chord addition series.

@[simp]

theorem WeierstrassCurve.map_formalGroup {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (W : WeierstrassCurve R) (φ : R →+* S) : (W.map φ).formalGroup = W.formalGroup.map φ

Base change of a Weierstrass curve commutes with passage to its formal group law.

instance WeierstrassCurve.isComm_formalGroup {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : W.formalGroup.IsComm

The formal group law of a Weierstrass curve is commutative. This makes its power-series-valued points whose constant coefficient is nilpotent an additive commutative monoid through Mathlib's standard instance.