The inverse law of the chord group law #
FormalGroup/Add/Series.lean produces formalAdd, the series F(z₁, z₂) = ι(z₃(z₁, z₂)) of the
chord construction, and FormalGroup/Add/Unit.lean proves its two unit laws. This file proves the
inverse law F(z, ι(z)) = 0, where ι = formalInverse is the formal inverse.
This is not one of the axioms of FormalGroup, which asks only for the constant and linear
coefficients and for associativity; a formal group law has a unique inverse series regardless.
What the identity says is that the series produced from the curve's negation is that inverse, so
the geometric ι and the abstract one agree.
Geometrically the chord through a point P and its negative -P is the vertical line through
them, which meets the curve again at the point at infinity; so the third root z₃(z, ι(z))
vanishes, and F(z, ι(z)) = ι(z₃(z, ι(z))) = ι(0) = 0.
Main results #
WeierstrassCurve.subst_invPair_formalThirdRoot: the third root of the chord through a point and its formal inverse vanishes,z₃(z, ι(z)) = 0.WeierstrassCurve.subst_invPair_formalAdd: the inverse lawF(z, ι(z)) = 0.
Implementation notes #
Both results hold over an arbitrary commutative ring, but the chord argument does not prove them
there: it divides by ι - z, so it needs O to be a domain, and it reaches 2 = 0 in the branch
it has to rule out. Both hypotheses are met by ℤ[A₁, ⋯, A₆], so the argument runs over the
universal curve, and map_specialize then carries the conclusion to every W — the descent
DivisionPolynomial/Omega.lean also runs. The nondegeneracy ι ≠ z is not a further hypothesis:
it follows from 2 ≠ 0 by comparing linear coefficients.
The pair (z, ι(z)) enters as the substituted family Sum.elim X (fun _ ↦ formalInverse W),
written inline throughout, as Add/Unit.lean writes its own two families inline: naming it would
add a definition whose unfolding lemma every proof would carry. FormalGroup/PairEval.lean writes
the same family inline for the same reason when it transports subst_invPair_formalAdd through
evaluation, but takes hasSubst_invPair from here rather than rebuilding it — that witness is
exported for exactly this transport, because MvPowerSeries.aeval_subst needs a HasSubst for
the very family the two public subst_invPair_* results are stated about.
References #
Provenance #
Adapted from Michael Stoll's EllipticCurves project
(github.com/MichaelStollBayreuth/EllipticCurves, Apache-2.0, 66889eada51a),
EllipticCurves/WeierstrassFormalGroup/GroupLaw.lean lines 118-308, the section Domain, and
EllipticCurves/WeierstrassFormalGroup/ThirdPoint.lean lines 372-460, 501-577 and 630-653.
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 development.
FormalGroup/Add/PairSubst.lean proves the chord identities for an arbitrary pair (q₁, q₂) of
series with vanishing constant coefficient; this module specializes them to the pair (z, ι(z)),
which is the case the formal inverse law needs.
The source's subst_wSeries_ne_zero is subst_formalW_ne_zero in FormalGroup/Add/Assoc.lean;
its interceptSeries_ne_zero and X_pair_intercept_ne_zero have no counterpart in this
repository.
Substituting a point and its formal inverse #
Substituting z for the first parameter and ι(z) for the second is a legitimate
substitution: both series have vanishing constant coefficient.
The chord through a point and its formal inverse #
The formal inverse is not the identity #
The third point of the chord through a point and its formal inverse is the origin:
z₃(z, ι(z)) = 0.
The chord through (z, w(z)) and its negative is the vertical line through them, which meets the
curve again only at the point at infinity.
The chord argument needs a domain in which 2 ≠ 0; the identity itself needs neither, and is
obtained here by descent from the universal curve, whose base ℤ[A₁, ⋯, A₆] supplies both.
The inverse law of the chord group law: F(z, ι(z)) = 0.
The sum of a point and its formal inverse is the origin, so formalInverse is the inverse series
of formalAdd; with rename_swap_formalAdd it is a two-sided one.