Evaluating the w-expansion and the formal inverse at a parameter

For a Weierstrass curve W over a complete linearly topologised ring O, the w-expansion of FormalGroup/WExpansion.lean and the formal inverse of FormalGroup/Inverse.lean can both be evaluated at a parameter t for which the evaluation converges. This file provides those evaluations, the identities they inherit from the series, and their membership, unit and non-vanishing properties.

Three hypotheses appear here, and they do different work. PowerSeries.HasEval t is what evaluation itself requires, and most results ask for it directly. Others ask instead for an ideal I whose adic topology is the ambient one, together with a membership t ∈ I that supplies the convergence: isUnit_formalUEval, formalWEval_ne_zero, algebraMap_formalWEval_ne_zero and hasEval_formalInverseEval. formalUEval_sub_one_mem is the one result asking for both. isUnit_thirdRootDenom asks for neither: it is a statement about the curve's coefficients and a topologically nilpotent element, so it takes IsTopologicallyNilpotent directly, and [NonarchimedeanRing O] in place of the ambient [IsTopologicalRing O]. formalWEval_zero asks for neither either, being an evaluation at a parameter that needs no convergence hypothesis.

Only two of the five values are confined to I ^ k: w(t) and ι(t). Of the four unit statements, only u(t)'s needs the ideal; the denominator d(t) = 1 - a₁ t - a₃ w(t) and its series inverse need nothing beyond evaluation, and the chord cubic's leading coefficient 1 + a₂l + a₄l² + a₆l³ needs only that l is topologically nilpotent. Each declaration's own docstring says where its conclusion comes from.

Main definitions

• WeierstrassCurve.formalWEval : the value w(t) of the w-expansion at t.
• WeierstrassCurve.formalUEval : the value u(t) of its unit part w(z) / z ^ 3.
• WeierstrassCurve.formalInverseDenomEval : the value of the denominator 1 - a₁ z - a₃ w(z).
• WeierstrassCurve.formalInverseDenomInvEval : the value of that denominator's series inverse.
• WeierstrassCurve.formalInverseEval : the value ι(t) of the formal inverse at t.

Main results

• WeierstrassCurve.formalWEval_eq_pow_mul_formalUEval : the factorisation w(t) = t ^ 3 * u(t).
• WeierstrassCurve.algebraMap_formalInverseEval_div_algebraMap_formalWEval_formalInverseEval and WeierstrassCurve.neg_one_div_algebraMap_formalWEval_formalInverseEval : the two division identities the inverse law rests on, over a field and with no nonvanishing hypothesis. Where w(t) ≠ 0 they say ι fixes the x-coordinate t / w(t) and sends -1 / w(t) to the curve's negY of it, y ↦ -y - a₁x - a₃.
• WeierstrassCurve.formalWEval_zero : w(0) = 0, an immediate consequence of that factorisation and the reason the zero parameter carries no affine coordinates.
• WeierstrassCurve.formalWEval_mem, WeierstrassCurve.formalInverseEval_mem : a parameter in I ^ k has w(t) and ι(t) in I ^ k.
• WeierstrassCurve.formalUEval_sub_one_mem : u(t) is congruent to 1 modulo I ^ k.
• WeierstrassCurve.isUnit_formalUEval, WeierstrassCurve.isUnit_formalInverseDenomEval, WeierstrassCurve.isUnit_formalInverseDenomInvEval : three of the four unit statements.
• WeierstrassCurve.isUnit_thirdRootDenom : the fourth — the leading coefficient 1 + a₂l + a₄l² + a₆l³ of the chord cubic, which Vieta's formula for the third root divides by, is a unit at any topologically nilpotent l.
• WeierstrassCurve.formalInverseDenomEval_eq, WeierstrassCurve.formalInverseEval_eq and WeierstrassCurve.formalInverseEval_mul_formalInverseDenomEval : the defining formulas for d(t) and ι(t), the last in the form ι(t) * d(t) = -t that avoids the series inverse.
• WeierstrassCurve.formalWEval_wEquation : the w-equation at a parameter.
• WeierstrassCurve.eq_formalWEval_of_wEquation : w(t) is the only solution of the w-equation lying in the ideal, the evaluated counterpart of WExpansion.lean's eq_of_wEquation.
• WeierstrassCurve.formalWEval_ne_zero, WeierstrassCurve.formalInverseEval_ne_zero : the two non-vanishing statements, and WeierstrassCurve.algebraMap_formalWEval_ne_zero for the image of w(t) in a nontrivial domain over O.
• WeierstrassCurve.formalInverseEval_formalInverseEval : the involution ι(ι(t)) = t, and WeierstrassCurve.formalWEval_formalInverseEval : w(ι(t)) = -(w(t) * d(t)⁻¹). Both ask only that t and ι(t) admit evaluation; WeierstrassCurve.hasEval_formalInverseEval supplies the second from an adic ideal when that is how a consumer holds it.

Implementation notes

The evaluation is Mathlib's PowerSeries.eval₂ at the identity ring hom. The adic hypothesis is carried as an explicit IsAdic I argument rather than through a WithIdeal instance, matching MvPowerSeries.eval₂_mem_pow, which these results call. WithIdeal would supply the topology itself at priority := 100, so on a ring that already carries one — ℤ_[p], whose topology comes from its metric — the adic topology is shadowed and the results become inapplicable. IsAdic is instead a proposition about the ambient topology, so it can be supplied for such a ring.

Names follow the series on this side rather than the source's: the evaluation of formalW is formalWEval, and so on. The source's names do not transfer, because the source-to-repository map is not order-preserving — the source's uSeries is this repository's formalInverseDenom, while formalU is the source's vSeries — and every series here has the same type, so a mismatched pairing would compile.

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 evaluation layer down to the formal inverse, declarations wEval, vEval, wEval_mem, wEval_eq, wEval_eq_cube_mul, vEval_sub_one_mem, isUnit_vEval, uEval, duEval, iotaEval, uEval_eq, uEval_mul_duEval, isUnit_uEval, isUnit_chordCoeff, iotaEval_eq, iotaEval_mem, wEval_iotaEval and iotaEval_iotaEval.

Four things are spelled differently here.

• The source evaluates through its own ChabautyColeman.MvPSeries.eval, which is by definition MvPowerSeries.eval₂ (RingHom.id _). That wrapper is not ported; the definitions use Mathlib's PowerSeries.eval₂ directly, as TauCeti/RingTheory/MvPowerSeries/Evaluation.lean already does for the membership estimates this file calls.
• The source's three eval_mem_maximalIdeal_pow lemmas are that same file's MvPowerSeries.eval₂_mem_pow, _mul and _add_mul, which are stated for an arbitrary adic ideal rather than the maximal one, so none of the three is re-ported.
• The source obtains unit-ness from IsLocalRing.isUnit_of_sub_one_mem_maximalIdeal. Here it comes instead from IsTopologicallyNilpotent.isUnit_one_add — Wedhorn 5.38, already in this repository — which the ambient completeness makes available and which needs no hypothesis relating I to the Jacobson radical. IsLocalRing is therefore not needed in this file at all.
• The source's wPoly is this repository's WeierstrassCurve.wEquationRHS, which is generic over an algebra, so evaluating it at O gives the element-level equation without a second definition.
• The source's private eval_subst_single is not ported. It is MvPSeries.eval_subst specialised, and this repository's PowerSeries.aeval_subst already states that fact without the DiscreteUniformity hypotheses Mathlib's MvPowerSeries.eval₂_subst carries — which a general adic ring does not supply, coefficients and values here being the same such ring. The two involution proofs call it directly.

The adic hypothesis is carried as an explicit IsAdic I argument for the reason given under implementation notes above.

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

The value of the w-expansion at a parameter.

Equations

• W.formalWEval t = PowerSeries.eval₂ (RingHom.id O) t W.formalW

theorem WeierstrassCurve.formalWEval_def {O : Type u_1} [CommRing O] [UniformSpace O] (W : WeierstrassCurve O) (t : O) : W.formalWEval t = PowerSeries.eval₂ (RingHom.id O) t W.formalW

formalWEval is evaluation of formalW through the identity ring hom.

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

The value of the unit part u(z) = w(z) / z ^ 3 at a parameter.

Equations

• W.formalUEval t = PowerSeries.eval₂ (RingHom.id O) t W.formalU

theorem WeierstrassCurve.formalUEval_def {O : Type u_1} [CommRing O] [UniformSpace O] (W : WeierstrassCurve O) (t : O) : W.formalUEval t = PowerSeries.eval₂ (RingHom.id O) t W.formalU

formalUEval is evaluation of formalU through the identity ring hom.

theorem WeierstrassCurve.formalWEval_eq_pow_mul_formalUEval {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.formalWEval t = t ^ 3 * W.formalUEval t

The factorisation w(t) = t ^ 3 * u(t) at a parameter, from the corresponding factorisation formalW_eq_X_pow_mul_formalU of the series.

@[simp]

theorem WeierstrassCurve.formalWEval_zero {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] (W : WeierstrassCurve O) : W.formalWEval 0 = 0

The w-expansion vanishes at the zero parameter, w being a multiple of z ^ 3. This is why the zero parameter is the point at infinity: the coordinates t / w(t) and -1 / w(t) have no value there.

theorem WeierstrassCurve.formalWEval_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} {k : ℕ} {t : O} (ht : PowerSeries.HasEval t) (htk : t ∈ I ^ k) : W.formalWEval t ∈ I ^ k

The value of the w-expansion at a parameter of I ^ k again lies in I ^ k: it is t ^ 3 times the value of the unit part.

theorem WeierstrassCurve.formalUEval_sub_one_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 : O} (ht : PowerSeries.HasEval t) (htk : t ∈ I ^ k) : W.formalUEval t - 1 ∈ I ^ k

The value of the unit part differs from 1 by an element of I ^ k when the parameter lies there: its constant coefficient is 1, and every other monomial carries a factor of the parameter.

theorem WeierstrassCurve.isUnit_formalUEval {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) {t : O} (ht : t ∈ I) : IsUnit (W.formalUEval t)

The value of the unit part at a parameter of I is a unit: it differs from 1 by an element of I, which is topologically nilpotent, so Wedhorn 5.38 applies.

theorem WeierstrassCurve.isUnit_thirdRootDenom {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsLinearTopology O O] (W : WeierstrassCurve O) [NonarchimedeanRing O] {l : O} (hl : IsTopologicallyNilpotent l) : IsUnit (1 + W.a₂ * l + W.a₄ * l ^ 2 + W.a₆ * l ^ 3)

The leading coefficient of the chord cubic is a unit at any topologically nilpotent element. Substituting w = λz + ν into the Weierstrass equation produces a cubic in z whose leading coefficient is 1 + a₂λ + a₄λ² + a₆λ³; Vieta's formula for its third root divides by that coefficient, so dividing is legitimate exactly when this holds.

Stated for an arbitrary topologically nilpotent element rather than for the evaluated slope, since that is all the statement needs; IsAdic.isTopologicallyNilpotent_of_mem supplies it from membership in an adic ideal when that is how a consumer holds it. [NonarchimedeanRing O] stands in for the ambient [IsTopologicalRing O], which it implies.

Not the same fact as Add/PairSubst.lean's subst_pair_thirdRootDenom_ne_zero, which says the corresponding multivariate power series is nonzero over a nontrivial base. That one lives in the series world and concludes nonvanishing; this one concludes invertibility, which is what dividing by it requires.

The inverse-side evaluations

Note which series these evaluate. The source's uSeries is this repository's formalInverseDenom, not formalU; formalU is the source's vSeries, evaluated above as formalUEval. Both are PowerSeries O, so pairing an evaluation with the wrong one would compile.

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

The value of the formal inverse's denominator 1 - a₁ z - a₃ w(z) at a parameter.

Equations

• W.formalInverseDenomEval t = PowerSeries.eval₂ (RingHom.id O) t W.formalInverseDenom

theorem WeierstrassCurve.formalInverseDenomEval_def {O : Type u_1} [CommRing O] [UniformSpace O] (W : WeierstrassCurve O) (t : O) : W.formalInverseDenomEval t = PowerSeries.eval₂ (RingHom.id O) t W.formalInverseDenom

formalInverseDenomEval is evaluation of formalInverseDenom through the identity ring hom.

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

The value at a parameter of the power-series inverse of formalInverseDenom.

Equations

• W.formalInverseDenomInvEval t = PowerSeries.eval₂ (RingHom.id O) t (W.formalInverseDenom.invOfUnit 1)

theorem WeierstrassCurve.formalInverseDenomInvEval_def {O : Type u_1} [CommRing O] [UniformSpace O] (W : WeierstrassCurve O) (t : O) : W.formalInverseDenomInvEval t = PowerSeries.eval₂ (RingHom.id O) t (W.formalInverseDenom.invOfUnit 1)

formalInverseDenomInvEval is evaluation of the series inverse of formalInverseDenom through the identity ring hom.

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

The value of the formal inverse ι(z) at a parameter.

Equations

• W.formalInverseEval t = PowerSeries.eval₂ (RingHom.id O) t W.formalInverse

theorem WeierstrassCurve.formalInverseEval_def {O : Type u_1} [CommRing O] [UniformSpace O] (W : WeierstrassCurve O) (t : O) : W.formalInverseEval t = PowerSeries.eval₂ (RingHom.id O) t W.formalInverse

formalInverseEval is evaluation of formalInverse through the identity ring hom.

theorem WeierstrassCurve.formalInverseDenomEval_mul_inv {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.formalInverseDenomEval t * W.formalInverseDenomInvEval t = 1

The denominator's value and the value of its series inverse multiply to 1.

theorem WeierstrassCurve.isUnit_formalInverseDenomEval {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) : IsUnit (W.formalInverseDenomEval t)

The denominator's value at a parameter is a unit.

theorem WeierstrassCurve.isUnit_formalInverseDenomInvEval {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) : IsUnit (W.formalInverseDenomInvEval t)

The value of the series inverse of the denominator is a unit.

theorem WeierstrassCurve.formalInverseDenomEval_eq {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.formalInverseDenomEval t = 1 - W.a₁ * t - W.a₃ * W.formalWEval t

The defining formula for the denominator's value: 1 - a₁ t - a₃ w(t).

theorem WeierstrassCurve.formalInverseEval_eq {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.formalInverseEval t = -(t * W.formalInverseDenomInvEval t)

The defining formula for the formal inverse's value: ι(t) = -t / (1 - a₁ t - a₃ w(t)), written through the series inverse of the denominator.

theorem WeierstrassCurve.formalInverseEval_mul_formalInverseDenomEval {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.formalInverseEval t * W.formalInverseDenomEval t = -t

The defining formula for ι(t) cleared of the series inverse: ι(t) times the concrete denominator 1 - a₁ t - a₃ w(t) is -t.

theorem WeierstrassCurve.formalInverseEval_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} {k : ℕ} {t : O} (ht : PowerSeries.HasEval t) (htk : t ∈ I ^ k) : W.formalInverseEval t ∈ I ^ k

The formal inverse maps a parameter of I ^ k back into I ^ k: it is -t times a value.

theorem WeierstrassCurve.formalWEval_wEquation {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.formalWEval t = W.wEquationRHS t (W.formalWEval t)

The w-equation at a parameter. Evaluating formalW_wEquation at t shows w(t) is a fixed point of v ↦ wEquationRHS W t v, which is the Weierstrass equation in the coordinates x = z / w, y = -1 / w.

theorem WeierstrassCurve.eq_formalWEval_of_wEquation {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) {t s : O} (ht : t ∈ I) (hs : s ∈ I) (h : s = W.wEquationRHS t s) : s = W.formalWEval t

Uniqueness of the solution of the w-equation at a parameter. For a parameter t of an adic ideal I, the value w(t) is the only element of I solving the w-equation at t. Both membership hypotheses are used: t ∈ I is what makes w converge at t, and s ∈ I is what confines the competing solution.

This is the evaluated counterpart of WExpansion.lean's eq_of_wEquation. It is what recognises a point of the curve as a parametrised one: the coordinates of such a point supply some solution of the w-equation, and this is what identifies that solution as w(t).

theorem WeierstrassCurve.formalWEval_ne_zero {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) {t : O} (ht : t ∈ I) (ht0 : t ^ 3 ≠ 0) : W.formalWEval t ≠ 0

w does not vanish at a parameter of I whose cube is nonzero: the factorisation w(t) = t ^ 3 * u(t) has a unit second factor. Over a domain the hypothesis is t ≠ 0.

theorem WeierstrassCurve.algebraMap_formalWEval_ne_zero {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] (W : WeierstrassCurve O) {S : Type u_2} [CommRing S] [Nontrivial S] [NoZeroDivisors S] [Algebra O S] {I : Ideal O} (hI : IsAdic I) {t : O} (ht : t ∈ I) (ht0 : (algebraMap O S) t ≠ 0) : (algebraMap O S) (W.formalWEval t) ≠ 0

w(t) has nonzero image in any nontrivial domain over O once the image of t does: the expansion factors as t ^ 3 * u(t) with u(t) a unit, and both factors have nonzero image — the cube because there are no zero divisors, the unit because units map to units. Unlike formalWEval_ne_zero this needs no hypothesis on t ^ 3, because the cube is checked in the codomain.

theorem WeierstrassCurve.formalInverseEval_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 : O} (ht : PowerSeries.HasEval t) (ht0 : t ≠ 0) : W.formalInverseEval t ≠ 0

The formal inverse does not vanish at a nonzero parameter: ι(t) is -t times a unit, and multiplying by a unit cannot create a zero. No hypothesis on t ^ 3 is needed — unlike formalWEval_ne_zero, whose factor t ^ 3 can vanish at a nonzero nilpotent t.

The involution

ι is an involution on the series (subst_formalInverse_self), and evaluating that identity at a parameter needs evaluation of a substitution. Mathlib's MvPowerSeries.eval₂_subst is not applicable at this generality: it carries [DiscreteUniformity R] [DiscreteUniformity S], and a general adic ring supplies no such instance. These two therefore go through PowerSeries.aeval_subst, which is the same statement with an arbitrary uniform structure on the coefficients.

theorem WeierstrassCurve.hasEval_formalInverseEval {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) {t : O} (ht : t ∈ I) : PowerSeries.HasEval (W.formalInverseEval t)

ι(t) admits evaluation when t is drawn from an ideal carrying the ambient topology: formalInverseEval_mem puts it in the same ideal. This is the adic route to the second hypothesis of the two identities below, which do not themselves need an ideal.

theorem WeierstrassCurve.formalWEval_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} (hE : PowerSeries.HasEval t) (hV : PowerSeries.HasEval (W.formalInverseEval t)) : W.formalWEval (W.formalInverseEval t) = -(W.formalWEval t * W.formalInverseDenomInvEval t)

The w-expansion at an inverted parameter: w(ι(t)) = -(w(t) * d(t)⁻¹), the evaluation of the series identity subst_formalInverse_formalW.

theorem WeierstrassCurve.algebraMap_formalInverseEval_div_algebraMap_formalWEval_formalInverseEval {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] (W : WeierstrassCurve O) {K : Type u_2} [Field K] [Algebra O K] {t : O} (hE : PowerSeries.HasEval t) (hEV : PowerSeries.HasEval (W.formalInverseEval t)) : (algebraMap O K) (W.formalInverseEval t) / (algebraMap O K) (W.formalWEval (W.formalInverseEval t)) = (algebraMap O K) t / (algebraMap O K) (W.formalWEval t)

The formal inverse fixes the x-coordinate. ι(t) = -(t · d(t)⁻¹) and w(ι t) = -(w(t) · d(t)⁻¹) share the unit d(t)⁻¹ = formalInverseDenomInvEval t, so the sign and that unit cancel in the ratio. No nonvanishing is needed: if w(t) = 0 then w(ι t) = 0 too and both sides are zero.

theorem WeierstrassCurve.neg_one_div_algebraMap_formalWEval_formalInverseEval {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] (W : WeierstrassCurve O) {K : Type u_2} [Field K] [Algebra O K] {t : O} (hE : PowerSeries.HasEval t) (hEV : PowerSeries.HasEval (W.formalInverseEval t)) : -1 / (algebraMap O K) (W.formalWEval (W.formalInverseEval t)) = (1 - (W.baseChange K).a₁ * (algebraMap O K) t - (W.baseChange K).a₃ * (algebraMap O K) (W.formalWEval t)) / (algebraMap O K) (W.formalWEval t)

The formal inverse's y-value in closed form: d(t)⁻¹ inverts d(t) = 1 - a₁t - a₃w(t), which is what turns -1 / w(ι t) into the displayed ratio. The identity holds with no nonvanishing hypothesis, both sides being zero when w(t) = 0.

When w(t) ≠ 0 the right-hand side is the curve's negY at the coordinates t / w(t) and -1 / w(t), so the formal inverse applies y ↦ -y - a₁x - a₃ rather than plain negation. That reading needs the hypothesis: at w(t) = 0 both ratios are zero by field division, while negY 0 0 = -a₃.

theorem WeierstrassCurve.formalInverseEval_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} (hE : PowerSeries.HasEval t) (hV : PowerSeries.HasEval (W.formalInverseEval t)) : W.formalInverseEval (W.formalInverseEval t) = t

The formal inverse is an involution at a parameter: ι(ι(t)) = t. This is -(-P) = P for the group law near the origin, evaluated at t.