Evaluating the chord construction at a pair of parameters

The chord construction of FormalGroup/Chord.lean and the addition series of FormalGroup/Add/Series.lean are two-variable power series. This file evaluates them at a pair of parameters, as FormalGroup/Eval.lean evaluates the one-variable series at a single one, and carries the identities of series over to identities of values.

The pair is the family Sum.elim (fun _ ↦ t₁) fun _ ↦ t₂ on Unit ⊕ Unit, and it admits evaluation as soon as each parameter does — the decay condition is vacuous over finitely many variables, so MvPowerSeries.hasEval_of_finite_of_isTopologicallyNilpotent applies.

Main definitions

• WeierstrassCurve.formalSlopeEval : the slope λ(t₁, t₂) of the chord.
• WeierstrassCurve.formalInterceptEval : the intercept ν(t₁, t₂).
• WeierstrassCurve.formalThirdRootEval : the parameter t₃(t₁, t₂) of the third point.
• WeierstrassCurve.formalAddEval : the value F(t₁, t₂) of the addition series.

Main results

• WeierstrassCurve.formalSlopeEval_mul_sub : λ(t₁, t₂) * (t₂ - t₁) = w(t₂) - w(t₁).
• WeierstrassCurve.formalInterceptEval_eq : ν(t₁, t₂) = w(t₁) - λ(t₁, t₂) * t₁, and WeierstrassCurve.formalInterceptEval_eq_inr : ν(t₁, t₂) = w(t₂) - λ(t₁, t₂) * t₂, the same intercept read from either parameter.
• WeierstrassCurve.formalWEval_formalThirdRootEval : w(t₃(t₁, t₂)) = λ(t₁, t₂) * t₃(t₁, t₂) + ν(t₁, t₂), the w-expansion at the third root agreeing with the chord line there.
• WeierstrassCurve.formalSlopeEval_mem, WeierstrassCurve.formalThirdRootEval_mem : parameters in I ^ k keep the slope and the third root there.
• WeierstrassCurve.formalThirdRootEval_relation : Vieta's formula at a pair, cleared of the inverse of the cubic's leading coefficient.
• WeierstrassCurve.formalThirdRootEval_ne_zero : the third root is nonzero once t₁ * w(t₂) ≠ t₂ * w(t₁) — an inequality that forces both parameters nonzero, and over a field also makes their x-coordinates distinct.
• WeierstrassCurve.hasEval_formalThirdRootEval : the third root admits evaluation as soon as the two parameters do, the ideal-free counterpart of formalThirdRootEval_mem.
• WeierstrassCurve.formalAddEval_eq : F(t₁, t₂) = ι(t₃(t₁, t₂)).
• WeierstrassCurve.formalAddEval_formalInverseEval : F(t, ι(t)) = 0, the inverse law.
• WeierstrassCurve.formalAddEval_zero_right and WeierstrassCurve.formalAddEval_zero_left : the unit laws F(t, 0) = t and F(0, t) = t.
• WeierstrassCurve.formalAddEval_comm : commutativity F(t₁, t₂) = F(t₂, t₁).
• WeierstrassCurve.formalAddEval_assoc : F(F(t₁, t₂), t₃) = F(t₁, F(t₂, t₃)), the group law's associativity read at parameters.
• WeierstrassCurve.hasEval_formalAddEval : F(t₁, t₂) admits evaluation as soon as t₁ and t₂ do — the ideal-free closure law.
• WeierstrassCurve.formalAddEval_sub_add_mem : F(t₁, t₂) - (t₁ + t₂) ∈ I ^ (2 * k) for parameters in I ^ k, so the group law is t₁ + t₂ to first order, and WeierstrassCurve.formalAddEval_mem : each level I ^ k is therefore closed under the addition series.

Implementation notes

Two of the series are built from one-variable ones through PowerSeries.toMvPowerSeries and MvPowerSeries.subst; evaluating those is PowerSeries.eval₂_id_toMvPowerSeries and MvPowerSeries.aeval_subst, neither of which requires the coefficient ring to be discrete — which matters here, because the ambient adic ring need not be.

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, whose full expansion is 66889eada51a74c2f5dfb7fb5909b0b5a0a2d96e), EllipticCurves/WeierstrassFormalGroup/Eval.lean — its pair-evaluation layer, declarations slopeEval, interceptEval, thirdRootEval, addEval, hasEval_pairElim, eval_pair_rename, eval_pair_subst_single, slopeEval_mul_sub, interceptEval_eq, slopeEval_mem, thirdRootEval_mem, thirdRootEval_relation, addEval_eq, addEval_sub_add_mem, addEval_iotaEval, wEval_thirdRootEval (here formalWEval_formalThirdRootEval), interceptEval_eq' (here formalInterceptEval_eq_inr) and thirdRootEval_ne_zero (here formalThirdRootEval_ne_zero, whose source carries an [IsDomain O] the argument does not use).

hasEval_formalThirdRootEval and hasEval_formalAddEval have no counterpart in the source, which reads evaluability off membership in IsLocalRing.maximalIdeal O; they are this repository's ideal-free replacements for that step.

The unit laws formalAddEval_zero_right and formalAddEval_zero_left, and the associativity formalAddEval_assoc, follow the same project's EllipticCurves/Mathlib/Chabauty/FormalGroupLaw/Points.lean, where they are the zero_add, add_zero and add_assoc fields of the AddCommMonoid instance on FormalGroupLaw.Points (def Points _Φ := ι → maximalIdeal O). Associativity's series-level input is that project's assoc_addSeries, which is FormalGroup/Add/Assoc.lean's formalAdd_assoc here. That generic formal-group scaffolding is not ported here: Mathlib's RingTheory/FormalGroup supersedes it, and its FormalGroup.Point is a different object — series carrying PowerSeries.HasSubst, not elements of an ideal — so the laws are stated as standalone lemmas about formalAddEval, ideal-free and taking PowerSeries.HasEval.

Four things are spelled differently here.

• The source's eval_pair_rename transports along MvPowerSeries.rename; this repository builds the one-variable series into two variables with PowerSeries.toMvPowerSeries instead, so the transport is PowerSeries.eval₂_id_toMvPowerSeries.
• The source states everything over IsLocalRing.maximalIdeal O at k = 1; the membership results here are over an arbitrary adic ideal and an arbitrary power of it, and the identities that use no ideal at all take PowerSeries.HasEval on each parameter, matching FormalGroup/Eval.lean.
• The source evaluates through its own ChabautyColeman.MvPSeries.eval, a wrapper for MvPowerSeries.eval₂ (RingHom.id _), which is not ported.
• The source writes the evaluated inverse series as iotaEval; here it is FormalGroup/Eval.lean's formalInverseEval, so its addEval_iotaEval is formalAddEval_formalInverseEval.

noncomputable def WeierstrassCurve.formalSlopeEval {O : Type u_1} [CommRing O] [UniformSpace O] (W : WeierstrassCurve O) (t₁ t₂ : O) : O

The value of the slope series at a pair of parameters.

Equations

• W.formalSlopeEval t₁ t₂ = MvPowerSeries.eval₂ (RingHom.id O) (Sum.elim (fun (x : Unit) => t₁) fun (x : Unit) => t₂) W.formalSlope

theorem WeierstrassCurve.formalSlopeEval_def {O : Type u_1} [CommRing O] [UniformSpace O] (W : WeierstrassCurve O) (t₁ t₂ : O) : W.formalSlopeEval t₁ t₂ = MvPowerSeries.eval₂ (RingHom.id O) (Sum.elim (fun (x : Unit) => t₁) fun (x : Unit) => t₂) W.formalSlope

formalSlopeEval is evaluation of formalSlope at the pair, through the identity ring hom.

noncomputable def WeierstrassCurve.formalInterceptEval {O : Type u_1} [CommRing O] [UniformSpace O] (W : WeierstrassCurve O) (t₁ t₂ : O) : O

The value of the intercept series at a pair of parameters.

Equations

• W.formalInterceptEval t₁ t₂ = MvPowerSeries.eval₂ (RingHom.id O) (Sum.elim (fun (x : Unit) => t₁) fun (x : Unit) => t₂) W.formalIntercept

theorem WeierstrassCurve.formalInterceptEval_def {O : Type u_1} [CommRing O] [UniformSpace O] (W : WeierstrassCurve O) (t₁ t₂ : O) : W.formalInterceptEval t₁ t₂ = MvPowerSeries.eval₂ (RingHom.id O) (Sum.elim (fun (x : Unit) => t₁) fun (x : Unit) => t₂) W.formalIntercept

formalInterceptEval is evaluation of formalIntercept at the pair, through the identity ring hom.

noncomputable def WeierstrassCurve.formalThirdRootEval {O : Type u_1} [CommRing O] [UniformSpace O] (W : WeierstrassCurve O) (t₁ t₂ : O) : O

The value of the third-root series at a pair of parameters.

Equations

• W.formalThirdRootEval t₁ t₂ = MvPowerSeries.eval₂ (RingHom.id O) (Sum.elim (fun (x : Unit) => t₁) fun (x : Unit) => t₂) W.formalThirdRoot

theorem WeierstrassCurve.formalThirdRootEval_def {O : Type u_1} [CommRing O] [UniformSpace O] (W : WeierstrassCurve O) (t₁ t₂ : O) : W.formalThirdRootEval t₁ t₂ = MvPowerSeries.eval₂ (RingHom.id O) (Sum.elim (fun (x : Unit) => t₁) fun (x : Unit) => t₂) W.formalThirdRoot

formalThirdRootEval is evaluation of formalThirdRoot at the pair, through the identity ring hom.

noncomputable def WeierstrassCurve.formalAddEval {O : Type u_1} [CommRing O] [UniformSpace O] (W : WeierstrassCurve O) (t₁ t₂ : O) : O

The value of the addition series at a pair of parameters.

Equations

• W.formalAddEval t₁ t₂ = MvPowerSeries.eval₂ (RingHom.id O) (Sum.elim (fun (x : Unit) => t₁) fun (x : Unit) => t₂) W.formalAdd

theorem WeierstrassCurve.formalAddEval_def {O : Type u_1} [CommRing O] [UniformSpace O] (W : WeierstrassCurve O) (t₁ t₂ : O) : W.formalAddEval t₁ t₂ = MvPowerSeries.eval₂ (RingHom.id O) (Sum.elim (fun (x : Unit) => t₁) fun (x : Unit) => t₂) W.formalAdd

formalAddEval is evaluation of formalAdd at the pair, through the identity ring hom.

theorem WeierstrassCurve.hasEval_formalAddEval {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] (W : WeierstrassCurve O) {t₁ t₂ : O} (h₁ : PowerSeries.HasEval t₁) (h₂ : PowerSeries.HasEval t₂) : PowerSeries.HasEval (W.formalAddEval t₁ t₂)

The group law is closed on evaluable parameters: F(t₁, t₂) admits evaluation as soon as t₁ and t₂ do. This is the ideal-free counterpart of formalAddEval_mem, and it is what lets the associativity statement take only its three parameters.

theorem WeierstrassCurve.formalSlopeEval_mul_sub {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] (W : WeierstrassCurve O) {t₁ t₂ : O} (h₁ : PowerSeries.HasEval t₁) (h₂ : PowerSeries.HasEval t₂) : W.formalSlopeEval t₁ t₂ * (t₂ - t₁) = W.formalWEval t₂ - W.formalWEval t₁

The evaluated slope identity: λ(t₁, t₂) * (t₂ - t₁) = w(t₂) - w(t₁).

theorem WeierstrassCurve.formalInterceptEval_eq {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] (W : WeierstrassCurve O) {t₁ t₂ : O} (h₁ : PowerSeries.HasEval t₁) (h₂ : PowerSeries.HasEval t₂) : W.formalInterceptEval t₁ t₂ = W.formalWEval t₁ - W.formalSlopeEval t₁ t₂ * t₁

The evaluated intercept identity: ν(t₁, t₂) = w(t₁) - λ(t₁, t₂) * t₁.

theorem WeierstrassCurve.formalInterceptEval_eq_inr {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] (W : WeierstrassCurve O) {t₁ t₂ : O} (h₁ : PowerSeries.HasEval t₁) (h₂ : PowerSeries.HasEval t₂) : W.formalInterceptEval t₁ t₂ = W.formalWEval t₂ - W.formalSlopeEval t₁ t₂ * t₂

The evaluated intercept identity, read from the second point: ν(t₁, t₂) = w(t₂) - λ(t₁, t₂) * t₂. Together with formalInterceptEval_eq this says the chord meets the curve at both parameters, which is what makes the intercept symmetric in them.

theorem WeierstrassCurve.formalSlopeEval_mem {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] (W : WeierstrassCurve O) {I : Ideal O} (hI : IsAdic I) {k : ℕ} {t₁ t₂ : O} (hk₁ : t₁ ∈ I ^ k) (hk₂ : t₂ ∈ I ^ k) : W.formalSlopeEval t₁ t₂ ∈ I ^ k

The slope of the chord at parameters of I ^ k again lies in I ^ k: the slope series has vanishing constant coefficient.

theorem WeierstrassCurve.formalThirdRootEval_mem {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] (W : WeierstrassCurve O) {I : Ideal O} (hI : IsAdic I) {k : ℕ} {t₁ t₂ : O} (hk₁ : t₁ ∈ I ^ k) (hk₂ : t₂ ∈ I ^ k) : W.formalThirdRootEval t₁ t₂ ∈ I ^ k

The third point's parameter at parameters of I ^ k again lies in I ^ k.

theorem WeierstrassCurve.formalThirdRootEval_relation {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] (W : WeierstrassCurve O) {t₁ t₂ : O} (h₁ : PowerSeries.HasEval t₁) (h₂ : PowerSeries.HasEval t₂) : (1 + W.a₂ * W.formalSlopeEval t₁ t₂ + W.a₄ * W.formalSlopeEval t₁ t₂ ^ 2 + W.a₆ * W.formalSlopeEval t₁ t₂ ^ 3) * (W.formalThirdRootEval t₁ t₂ + t₁ + t₂) = -(W.a₁ * W.formalSlopeEval t₁ t₂ + W.a₂ * W.formalInterceptEval t₁ t₂ + W.a₃ * W.formalSlopeEval t₁ t₂ ^ 2 + 2 * W.a₄ * W.formalSlopeEval t₁ t₂ * W.formalInterceptEval t₁ t₂ + 3 * W.a₆ * W.formalSlopeEval t₁ t₂ ^ 2 * W.formalInterceptEval t₁ t₂)

Vieta's formula at a pair of parameters, cleared of the inverse of the cubic's leading coefficient: the third root satisfies (1 + a₂λ + a₄λ² + a₆λ³)(t₃ + t₁ + t₂) = -(a₁λ + a₂ν + a₃λ² + 2a₄λν + 3a₆λ²ν).

theorem WeierstrassCurve.hasEval_formalThirdRootEval {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] (W : WeierstrassCurve O) {t₁ t₂ : O} (h₁ : PowerSeries.HasEval t₁) (h₂ : PowerSeries.HasEval t₂) : PowerSeries.HasEval (W.formalThirdRootEval t₁ t₂)

The third root admits evaluation as soon as the two parameters do. Like hasEval_formalAddEval, this is the ideal-free counterpart of formalThirdRootEval_mem, and it is what lets the identities below take only their two parameters.

theorem WeierstrassCurve.formalWEval_formalThirdRootEval {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] (W : WeierstrassCurve O) {t₁ t₂ : O} (h₁ : PowerSeries.HasEval t₁) (h₂ : PowerSeries.HasEval t₂) : W.formalWEval (W.formalThirdRootEval t₁ t₂) = W.formalSlopeEval t₁ t₂ * W.formalThirdRootEval t₁ t₂ + W.formalInterceptEval t₁ t₂

The evaluated on-line identity: w(t₃(t₁, t₂)) = λ(t₁, t₂) * t₃(t₁, t₂) + ν(t₁, t₂), so the w-expansion read at the third root agrees with the chord line read there. Over a field, where the parameters carry the coordinates x = t / w and y = -1 / w, this is what says the third root parametrises a point on the chord and not merely a root of the chord cubic.

theorem WeierstrassCurve.formalThirdRootEval_ne_zero {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] (W : WeierstrassCurve O) {t₁ t₂ : O} (h₁ : PowerSeries.HasEval t₁) (h₂ : PowerSeries.HasEval t₂) (hx : t₁ * W.formalWEval t₂ ≠ t₂ * W.formalWEval t₁) : W.formalThirdRootEval t₁ t₂ ≠ 0

The third root does not vanish once t₁ * w(t₂) ≠ t₂ * w(t₁). The inequality forces both parameters to be nonzero, w vanishing at 0; and over a field a nonzero parameter t carries the affine coordinates x = t / w(t), y = -1 / w(t), so it then also says the two x-coordinates differ. The conclusion is that the chord through the two points is not the vertical line.

theorem WeierstrassCurve.formalAddEval_eq {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] (W : WeierstrassCurve O) {t₁ t₂ : O} (h₁ : PowerSeries.HasEval t₁) (h₂ : PowerSeries.HasEval t₂) : W.formalAddEval t₁ t₂ = W.formalInverseEval (W.formalThirdRootEval t₁ t₂)

The addition series at a pair of parameters is the formal inverse of the third root: F(t₁, t₂) = ι(t₃(t₁, t₂)), the sum of two points being the negative of the third point of the chord through them.

@[simp]

theorem WeierstrassCurve.formalAddEval_formalInverseEval {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] (W : WeierstrassCurve O) {t : O} (ht : PowerSeries.HasEval t) (hι : PowerSeries.HasEval (W.formalInverseEval t)) : W.formalAddEval t (W.formalInverseEval t) = 0

The inverse law at parameters: F(t, ι(t)) = 0, so the value of the inverse series at t is the additive inverse of t under the group law read at parameters.

theorem WeierstrassCurve.formalAddEval_sub_add_mem {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] (W : WeierstrassCurve O) {I : Ideal O} (hI : IsAdic I) {k : ℕ} {t₁ t₂ : O} (hk₁ : t₁ ∈ I ^ k) (hk₂ : t₂ ∈ I ^ k) : W.formalAddEval t₁ t₂ - (t₁ + t₂) ∈ I ^ (2 * k)

The group law is t₁ + t₂ to first order: at parameters of I ^ k the addition series deviates from their sum by an element of I ^ (2 * k), because it agrees with z₁ + z₂ below total degree two.

theorem WeierstrassCurve.formalAddEval_mem {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] (W : WeierstrassCurve O) {I : Ideal O} (hI : IsAdic I) {k : ℕ} {t₁ t₂ : O} (hk₁ : t₁ ∈ I ^ k) (hk₂ : t₂ ∈ I ^ k) : W.formalAddEval t₁ t₂ ∈ I ^ k

The levels of the filtration are closed under the group law: the addition series carries a pair of parameters of I ^ k back into I ^ k, because it deviates from their sum by an element of I ^ (2 * k).

theorem WeierstrassCurve.formalAddEval_comm {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] (W : WeierstrassCurve O) {t₁ t₂ : O} (h₁ : PowerSeries.HasEval t₁) (h₂ : PowerSeries.HasEval t₂) : W.formalAddEval t₁ t₂ = W.formalAddEval t₂ t₁

Commutativity of the group law at parameters: F(t₁, t₂) = F(t₂, t₁).

theorem WeierstrassCurve.formalAddEval_assoc {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] (W : WeierstrassCurve O) {t₁ t₂ t₃ : O} (h₁ : PowerSeries.HasEval t₁) (h₂ : PowerSeries.HasEval t₂) (h₃ : PowerSeries.HasEval t₃) : W.formalAddEval (W.formalAddEval t₁ t₂) t₃ = W.formalAddEval t₁ (W.formalAddEval t₂ t₃)

Associativity of the group law at parameters: F(F(t₁, t₂), t₃) = F(t₁, F(t₂, t₃)).

@[simp]

theorem WeierstrassCurve.formalAddEval_zero_right {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] (W : WeierstrassCurve O) {t : O} (ht : PowerSeries.HasEval t) : W.formalAddEval t 0 = t

The right unit law at parameters: F(t, 0) = t, so the origin's parameter is neutral for the group law read at parameters.

@[simp]

theorem WeierstrassCurve.formalAddEval_zero_left {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] (W : WeierstrassCurve O) {t : O} (ht : PowerSeries.HasEval t) : W.formalAddEval 0 t = t

The left unit law at parameters: F(0, t) = t.