The chord construction along an arbitrary pair of parameters #
FormalGroup/Chord.lean builds the chord data — the slope λ, the intercept ν, the third
root z₃ and the addition series F — as two-variable series in MvPowerSeries (Unit ⊕ Unit) O,
and states their defining identities in the two variables themselves. This file substitutes an
arbitrary pair (q₁, q₂) of series with vanishing constant coefficient for those variables,
and carries each identity across.
FormalGroup/Add/Inverse.lean already does this for the one pair (z, ι(z)). Its versions are
this file's, specialized; see the Provenance note there.
Main results #
WeierstrassCurve.subst_pair_toMvPowerSeries_inl,WeierstrassCurve.subst_pair_toMvPowerSeries_inr: the one-variablew-expansion, embedded in either variable, becomesw(q₁)respectivelyw(q₂).WeierstrassCurve.subst_pair_formalSlope_mul:λ(q₁, q₂) * (q₂ - q₁) = w(q₂) - w(q₁).WeierstrassCurve.subst_pair_formalThirdRoot_formalW: thew-expansion at the third root is the chord line read there.WeierstrassCurve.subst_pair_thirdRootDenom_mul: Vieta's denominator stays a unit at the pair, andWeierstrassCurve.subst_pair_thirdRootDenom_ne_zero: in particular it is nonzero.WeierstrassCurve.subst_pair_formalThirdRoot_relation: the defining relation ofz₃at the pair, with that inverse cleared.WeierstrassCurve.constantCoeff_subst_pair_formalThirdRoot: the third root at the pair again vanishes at the origin, so it is itself a legitimate parameter.WeierstrassCurve.subst_pair_formalAdd: the addition series at the pair is the formal inverse read atz₃.WeierstrassCurve.subst_pair_formalW_formalAdd: thew-expansion at the addition series,w(F(q₁, q₂)) = -(w(z₃) * u(z₃)⁻¹).WeierstrassCurve.subst_pair_formalInverseDenom_mul,WeierstrassCurve.subst_pair_formalInverseDenom_eq: the denominator of the formal inverse, read atz₃, is a unit and equals1 - a₁ z₃ - a₃ w(z₃).WeierstrassCurve.subst_pair_formalAdd_eq: the addition series written out,F(q₁, q₂) = -(z₃ * u(z₃)⁻¹).WeierstrassCurve.subst_pair_formalIntercept_eq_inl,WeierstrassCurve.subst_pair_formalIntercept_eq_inr: the chord's intercept at the pair, read from either of the two points.WeierstrassCurve.subst_pair_formalIntercept_mul_sub: the cross combinationq₁ w(q₂) - q₂ w(q₁) = ν(q₁, q₂) * (q₁ - q₂), which is what the two readings buy.WeierstrassCurve.subst_pair_formalThirdRoot_ne_zero: a nonzero intercept forces a nonzero third root.
Implementation notes #
The pair is the family MvPowerSeries.pairSubstitution q₁ q₂ on Unit ⊕ Unit.
Add/Inverse.lean keeps its own spelling of the pair (z, ι(z)) and reaches these lemmas
through its private invPair_eq bridge.
Two of Stoll's helpers in this range are not ported, because this repository already has them in
a more general form. His subst_pair_rename, which pushes the substitution through the
one-variable-into-two-variable embedding, is Mathlib's PowerSeries.subst_toMvPowerSeries
composed with Sum.elim_inl/Sum.elim_inr — this repository builds the two-variable series with
PowerSeries.toMvPowerSeries where the source uses MvPowerSeries.rename. His
subst_wSeries_fix, that w composed with any parameter solves the w-equation, is
WeierstrassCurve.subst_formalW_wEquation in FormalGroup/WExpansion.lean, stated there over an
arbitrary algebra.
References #
Provenance #
Adapted from Michael Stoll's EllipticCurves project
(github.com/MichaelStollBayreuth/EllipticCurves, Apache-2.0) at commit
66889eada51a74c2f5dfb7fb5909b0b5a0a2d96e,
EllipticCurves/WeierstrassFormalGroup/ThirdPoint.lean, declarations hasSubst_pair,
pair_slope_identity, pair_A_mul and pair_T₃_relation, together with pair_online
from EllipticCurves/WeierstrassFormalGroup/GroupLaw.lean.
The source's slopeSeries, interceptSeries and wSeries are formalSlope, formalIntercept
and formalW here, continuing the renaming this repository applies to that development, so
pair_slope_identity and pair_online are subst_pair_formalSlope_mul and
subst_pair_formalThirdRoot_formalW.
Stoll's A for Vieta's denominator is formalThirdRootDenom here, so pair_A_mul and
pair_T₃_relation are subst_pair_thirdRootDenom_mul and
subst_pair_formalThirdRoot_relation.
Also from that file, pair_thirdRoot_constantCoeff is
constantCoeff_subst_pair_formalThirdRoot and pair_wF is subst_pair_formalW_formalAdd.
The source's pair_F_comp needs no counterpart of its own: it says the addition series at the
pair is the inverse series read at the third root, which here is formalAdd's definition
(Add/Series.lean) pushed through the substitution, and that is subst_pair_formalAdd.
A naming trap worth recording, since the rename map above invites the wrong reading. Stoll's
uSeries (Chord.lean:351, 1 - a₁ z - a₃ w) is formalInverseDenom here
(FormalGroup/Inverse.lean), not formalU. This repository's formalU is a different
series — the unit part of the w-expansion, w = z³ u. Anything ported from the source's u
lemmas must target formalInverseDenom.
The source's pair_intercept_identity₁ and pair_intercept_identity₂ are
subst_pair_formalIntercept_eq_inl and subst_pair_formalIntercept_eq_inr here.
The w-expansion in the first parameter becomes w(q₁).
The w-expansion in the second parameter becomes w(q₂).
The chord through the two parametrized points #
The defining property of the slope, read at the pair (q₁, q₂):
λ(q₁, q₂) * (q₂ - q₁) = w(q₂) - w(q₁).
The third point of the chord lies on the curve #
The on-line identity at the pair (q₁, q₂): reading the w-expansion at the third root
gives the chord line read there.
Vieta's denominator and the third-root relation #
Vieta's denominator, read at the pair (q₁, q₂), is still a unit: it times its invOfUnit
is 1.
Vieta's denominator at the pair is nonzero, because it has an explicit inverse. Over a
nontrivial base this is immediate from subst_pair_thirdRootDenom_mul; no coefficient
computation is needed.
The defining relation of the third root at the pair (q₁, q₂), with the inverse of Vieta's
denominator eliminated.
The third root as a parameter in its own right #
The third root, read at the pair (q₁, q₂), again has vanishing constant coefficient, so it
is itself a legitimate parameter to substitute into a one-variable series.
The addition series, read at the pair (q₁, q₂), again has vanishing constant coefficient, so
a bracketed sum is itself a legitimate parameter — which is what lets an associativity argument
feed one bracketed sum into another.
The addition series at the pair (q₁, q₂) is the formal inverse read at the third root
z₃(q₁, q₂).
This is formalAdd_def pushed through the pair substitution, and it is the bridge that turns any
one-variable identity about formalInverse into a statement about the group law at the pair.
The w-expansion at the addition series, read at the pair (q₁, q₂):
w(F(q₁, q₂)) = -(w(z₃) * u(z₃)⁻¹), where z₃ = z₃(q₁, q₂) is the third root and u is
formalInverseDenom, the denominator of the formal inverse.
This is the one-variable subst_formalInverse_formalW carried across by subst_pair_formalAdd,
so the group law's w at a pair is never recomputed. The third root is spelled as a Unit-family
substitution, matching subst_pair_formalThirdRoot_formalW, so the two rewrite against each
other.
The denominator of the formal inverse, read at the third root z₃(q₁, q₂), is still a unit:
it times its invOfUnit is 1.
The denominator of the formal inverse, read at the third root, written out:
u(z₃) = 1 - a₁ z₃ - a₃ w(z₃).
The addition series at the pair, written out: F(q₁, q₂) = -(z₃ * u(z₃)⁻¹).
The chord data at the pair, read from either point #
The intercept of the chord through the two parametrized points, read at the pair (q₁, q₂)
from the first point: ν(q₁, q₂) = w(q₁) - λ(q₁, q₂) * q₁.
subst_pair_formalIntercept_eq_inr is the same intercept read from the second point; the two
statements differ only in which parameter appears on the right, and rewriting with either one
clears the intercept but leaves the slope behind. Combining the two readings is what cancels the
slope, and that combination is already packaged as subst_pair_formalIntercept_mul_sub, so a
consumer that wants the slope gone should reach for it rather than for these two.
The same intercept read from the second point: ν(q₁, q₂) = w(q₂) - λ(q₁, q₂) * q₂. Together
with subst_pair_formalIntercept_eq_inl this is what expresses q₁ * w(q₂) - q₂ * w(q₁) through
the intercept alone.
The two readings differ only in which parameter appears on the right, and rewriting with either
one clears the intercept but leaves the slope behind; a consumer that wants the slope gone should
reach for subst_pair_formalIntercept_mul_sub, which packages the combination that cancels it.
The cross combination q₁ w(q₂) - q₂ w(q₁) is expressed through the intercept alone:
q₁ w(q₂) - q₂ w(q₁) = ν(q₁, q₂) * (q₁ - q₂).
Reading the intercept from both points is what makes the slope cancel, so this is the one
intercept identity with no λ in it: subst_pair_formalIntercept_eq_inl and
subst_pair_formalIntercept_eq_inr each clear the intercept but leave the slope behind. The
factored (q₁ - q₂) on the right is what the associativity assembly needs in order to know that
the chord's x-coordinates are distinct; reach for it there as a single rewrite rather than
recombining the two readings by hand.
A nonzero intercept forces a nonzero third root: at z₃ = 0 the on-line identity
w(z₃) = λ z₃ + ν collapses to 0 = ν, since w has no constant term.