The unit laws and the linear part of the chord group law

FormalGroup/Add/Series.lean produces formalAdd, the series F(z₁, z₂) = ι(z₃(z₁, z₂)) of the chord construction. This file records what F does at the origin and in lowest degree: the two unit laws F(z, 0) = z and F(0, z) = z, and the fact that F(z₁, z₂) = z₁ + z₂ up to terms of total degree at least two.

Together with rename_swap_formalAdd, already in Add/Series.lean, the two unit laws are the formal-group-law axioms for formalAdd apart from associativity. constantCoeff_formalAdd is not one of those axioms: it supplies the HasSubst prerequisite that substituting F into a series requires in the first place.

Main results

• WeierstrassCurve.subst_unitR_formalThirdRoot: setting the second parameter to zero sends the third root of the chord to the formal inverse, z₃(z, 0) = ι(z). Geometrically the chord through P and O meets the curve again at -P.
• WeierstrassCurve.subst_unitR_formalAdd and WeierstrassCurve.subst_unitL_formalAdd: the two unit laws F(z, 0) = z and F(0, z) = z.
• WeierstrassCurve.coeff_single_inl_formalAdd and WeierstrassCurve.coeff_single_inr_formalAdd: both linear coefficients of F are 1.
• WeierstrassCurve.coeff_formalAdd_sub_eq_zero_of_degree_lt: below total degree two, F agrees with z₁ + z₂.

Implementation notes

The two specializations are substitutions of the families Sum.elim X (fun _ ↦ 0) and Sum.elim (fun _ ↦ 0) X, written inline throughout rather than named: they appear only in this file, and naming them would add a definition whose unfolding lemma every proof would then have to carry.

Only the right-hand unit law is proved directly. The left-hand one follows from it and the swap-invariance rename_swap_formalAdd, which is why this file needs no separate analysis of the chord in the second variable.

One-variable series are viewed in a single parameter of the pair through PowerSeries.toMvPowerSeries, the spelling Chord.lean and TauCeti/RingTheory/MvPowerSeries/ Equiv.lean already use, rather than through MvPowerSeries.rename (fun _ ↦ s). The two are definitionally equal (PowerSeries.toMvPowerSeries_apply), and the proofs below cross between them where the rename API is the more convenient of the two.

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 lines 576-870, the section AddZero — declarations hasSubst_unitR, subst_unitR_renameL, subst_unitR_renameR, X_mul_subst_unitR_slopeSeries, subst_unitR_interceptSeries, ringHom_invOfUnit, subst_unitR_thirdRootSeries, subst_unitR_addSeries, hasSubst_unitL, subst_unitL_addSeries, coeff_single_eq_one_of_subst_eq_X, coeff_single_inl_addSeries, coeff_single_inr_addSeries, degree_two_var and coeff_addSeries_sub_of_degree_lt.

The source's addSeries, thirdRootSeries, slopeSeries, interceptSeries, inverseSeries, uSeries and wSeries are formalAdd, formalThirdRoot, formalSlope, formalIntercept, formalInverse, formalInverseDenom and formalW here, continuing the renaming this repository applies to the rest of that file. The source's rename (fun _ ↦ s) spelling is replaced by PowerSeries.toMvPowerSeries s throughout, as elsewhere in FormalGroup/.

The source's private ringHom_invOfUnit is not ported. It carries no elliptic content, and the general statement now lives in a general file as MvPowerSeries.ringHom_invOfUnit, which this file uses directly.

Setting the second parameter to zero

The third point of a chord through the origin

@[simp]

theorem WeierstrassCurve.subst_unitR_formalThirdRoot {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : MvPowerSeries.subst (Sum.elim MvPowerSeries.X fun (x : Unit) => 0) W.formalThirdRoot = W.formalInverse

Specializing the third root at the origin gives the formal inverse: substituting z for the first parameter and 0 for the second sends formalThirdRoot to formalInverse, that is z₃(z, 0) = ι(z).

The identity is motivated by the chord through a point and the origin meeting the curve again at the negative of that point, but nothing about points of the curve is proved here — only the corresponding identity of power series.

The unit laws

@[simp]

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

The right unit law: F(z, 0) = z. Adding the origin does nothing.

@[simp]

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

The left unit law: F(0, z) = z, by the right unit law and commutativity.

The linear coefficients

@[simp]

theorem WeierstrassCurve.coeff_single_inl_formalAdd {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : (MvPowerSeries.coeff (Finsupp.single (Sum.inl ()) 1)) W.formalAdd = 1

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

@[simp]

theorem WeierstrassCurve.coeff_single_inr_formalAdd {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : (MvPowerSeries.coeff (Finsupp.single (Sum.inr ()) 1)) W.formalAdd = 1

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

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

Below total degree two the group law is addition: the coefficients of formalAdd W - X (Sum.inl ()) - X (Sum.inr ()) vanish on every exponent of total degree < 2.