The addition series presented over Fin 2 #
formalAdd is indexed by Unit ⊕ Unit, one variable per chord parameter, which is the shape every
series-level lemma about it is stated in. Mathlib's FormalGroup, by contrast, carries a power
series in MvPowerSeries (Fin 2) R. This file transports the two linear coefficients along the
reindexing unitSumUnitEquivFinTwo.
Those two are the lin_coeff_X and lin_coeff_Y fields of the FormalGroup structure built by
WeierstrassCurve.formalGroup. The constant coefficient is discharged directly by simp, while
associativity is transported at the construction site by the general
MvPowerSeries.rename_unitSumUnitEquivFinTwo_assoc theorem.
formalAdd over Unit ⊕ Unit stays the working object: nothing here re-founds it over Fin 2,
and the Fin 2 presentation is not a second public spelling of the addition series — it exists to
be the toPowerSeries field of that structure.
Main results #
WeierstrassCurve.coeff_single_zero_rename_unitSumUnitEquivFinTwo_formalAddandWeierstrassCurve.coeff_single_one_rename_unitSumUnitEquivFinTwo_formalAdd: the two linear coefficients.
Provenance #
No external source. Michael Stoll's development states the group law over Unit-indexed sums
throughout and bundles it into his own FormalGroupLaw structure, so the reindexing has no
counterpart there; it is the cost of refounding on Mathlib's FormalGroup, whose assoc field is
stated over Fin 2.
The linear coefficient of the reindexed addition series in the variable 0 is 1 — the
lin_coeff_X field.
The linear coefficient of the reindexed addition series in the variable 1 is 1 — the
lin_coeff_Y field.