Points of a Weierstrass curve from formal-group parameters

Over a complete ring O carrying the I-adic topology, a parameter t ∈ I gives a point of W over any field K whose structure map O → K is injective: the w-expansion converges at t, and the pair (t / w(t), -1 / w(t)) satisfies the Weierstrass equation because the w-equation is that equation read in the coordinates x = t / w, y = -1 / w. The parameter t = 0 gives the point at infinity.

equation_formalPoint needs nothing beyond that: the pair lies on the curve for any W. Turning it into a point does need the curve over K to be elliptic, so everything from formalPoint onwards assumes [(W.baseChange K).IsElliptic] — weaker than asking W itself to be elliptic over O, which would exclude an integral model whose discriminant is nonzero but not a unit.

The two coordinates are recorded in closed form as well. Since w(t) = t ^ 3 * u(t) with u(t) a unit, the x-coordinate is inverse to t ^ 2 * u(t) and the y-coordinate to -(t ^ 3 * u(t)). Both are stated as products in K, so no inverse of either factor has to be named; the powers 2 and 3 of t they exhibit are what a valuation on K would later turn into pole orders, but no order or valuation hypothesis is assumed here.

Main definitions

• WeierstrassCurve.formalPoint: the point of W⁄K attached to a parameter of an adic ideal.

Main results

• WeierstrassCurve.equation_formalPoint: the parametrized pair lies on the curve.
• WeierstrassCurve.formalPoint_eq_some: a point both of whose ratios -x / y and -1 / y come from the ideal is the parametrised point of the first, the surjectivity companion of WeierstrassCurve.formalPoint_injective.
• WeierstrassCurve.neg_xCoord_div_yCoord_formalPoint: the parameter read back off the point as -x / y, and with it WeierstrassCurve.formalPoint_eq_zero_iff and WeierstrassCurve.formalPoint_injective.
• WeierstrassCurve.formalPoint_of_param_eq_zero and WeierstrassCurve.formalPoint_of_param_ne_zero: the two branches of the definition.
• WeierstrassCurve.formalPoint_formalInverseEval: the parametrisation respects negation — the formal inverse on parameters becomes the group inverse on points, which on a generalised Weierstrass curve sends y to -y - a₁x - a₃ rather than to -y.
• WeierstrassCurve.xRep_formalPoint_eq_iff: two parameters have points with the same x-coordinate exactly when they are equal or exchanged by the formal inverse, with WeierstrassCurve.mul_formalWEval_eq_mul_formalWEval_iff its chord form.
• WeierstrassCurve.xCoord_formalPoint and WeierstrassCurve.yCoord_formalPoint: the point's coordinates, through which the closed forms WeierstrassCurve.xCoord_formalPoint_mul_eq_one and WeierstrassCurve.yCoord_formalPoint_mul_eq_neg_one are stated.

References

• J. Silverman, The Arithmetic of Elliptic Curves, IV.1, VII.2.

Provenance

The same parametrization is formalised in Michael Stoll's elliptic-curve development (github.com/MichaelStollBayreuth/EllipticCurves @ 66889eada51a, Apache-2.0), file EllipticCurves/WeierstrassFormalGroup/Filtration.lean, declarations formalPoint, formalPoint_of_param_eq_zero, formalPoint_of_param_ne_zero, formalPoint_nonsingular and formalPoint_negPoint. The first three keep their source names; the fourth is not restated, Affine.Point.mk carrying the equation-to-nonsingularity step itself.

formalPoint_formalInverseEval is that source's formalPoint_negPoint. It is what makes the parameters of an adic ideal closed under inverses as points, so that the chord case of additivity in Point/Add.lean can read the addition series as a negated third root. Its name takes this repository's vocabulary, formalInverseEval rather than the source's negPoint, since the object being applied is the evaluated formal inverse.

mul_formalWEval_eq_mul_formalWEval_iff is that source's eq_or_eq_negPoint_of_x_cond, private there and stated in one direction only; xRep_formalPoint_eq_iff is the form on xRep that it specialises.

That development states them over v.adicCompletion K for a height-one prime of a Dedekind domain and builds nonsingularity from a chord lemma of its own. The declarations below are stated over an arbitrary complete adic ring mapping injectively to a field, and read the nonsingularity off Mathlib's equation_iff_nonsingular, which Affine.Point.mk also uses.

theorem WeierstrassCurve.equation_formalPoint {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] {K : Type u_2} [Field K] [Algebra O K] (W : WeierstrassCurve O) {t : O} (ht : PowerSeries.HasEval t) (hw : (algebraMap O K) (W.formalWEval t) ≠ 0) : (W.baseChange K).toAffine.Equation ((algebraMap O K) t / (algebraMap O K) (W.formalWEval t)) (-((algebraMap O K) (W.formalWEval t))⁻¹)

A formal-group parameter gives a point of the curve: the pair (t / w(t), -1 / w(t)) satisfies the Weierstrass equation over K. The hypothesis is w(t) ≠ 0 rather than t ≠ 0, because that is what the two denominators need; algebraMap_formalWEval_ne_zero supplies it from a nonzero image algebraMap O K t ≠ 0, which FaithfulSMul O K below derives from t ≠ 0.

noncomputable def WeierstrassCurve.formalPoint {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] {K : Type u_2} [Field K] [Algebra O K] (W : WeierstrassCurve O) [(W.baseChange K).IsElliptic] [FaithfulSMul O K] {I : Ideal O} (hI : IsAdic I) {t : O} (ht : t ∈ I) : (W.baseChange K).toAffine.Point

The point attached to a formal-group parameter: a nonzero t in an adic ideal gives the affine point (t / w(t), -1 / w(t)), and t = 0 gives the point at infinity.

Equations

• W.formalPoint hI ht = if h0 : t = 0 then 0 else have hT := ⋯; WeierstrassCurve.Affine.Point.mk ⋯

@[simp]

theorem WeierstrassCurve.formalPoint_of_param_eq_zero {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] {K : Type u_2} [Field K] [Algebra O K] (W : WeierstrassCurve O) [(W.baseChange K).IsElliptic] [FaithfulSMul O K] {I : Ideal O} (hI : IsAdic I) {t : O} (ht : t ∈ I) (h0 : t = 0) : W.formalPoint hI ht = 0

The parameter 0 gives the point at infinity.

theorem WeierstrassCurve.formalPoint_of_param_ne_zero {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] {K : Type u_2} [Field K] [Algebra O K] (W : WeierstrassCurve O) [(W.baseChange K).IsElliptic] [FaithfulSMul O K] {I : Ideal O} (hI : IsAdic I) {t : O} (ht : t ∈ I) (h0 : t ≠ 0) : W.formalPoint hI ht = Affine.Point.mk ⋯

A nonzero parameter gives the affine point, with its coordinates in the form equation_formalPoint states them.

@[simp]

theorem WeierstrassCurve.xCoord_formalPoint {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] {K : Type u_2} [Field K] [Algebra O K] (W : WeierstrassCurve O) [(W.baseChange K).IsElliptic] [FaithfulSMul O K] {I : Ideal O} (hI : IsAdic I) {t : O} (ht : t ∈ I) (h0 : t ≠ 0) : (W.formalPoint hI ht).xCoord = (algebraMap O K) t / (algebraMap O K) (W.formalWEval t)

The x-coordinate of the parametrized point is t / w(t).

@[simp]

theorem WeierstrassCurve.yCoord_formalPoint {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] {K : Type u_2} [Field K] [Algebra O K] (W : WeierstrassCurve O) [(W.baseChange K).IsElliptic] [FaithfulSMul O K] {I : Ideal O} (hI : IsAdic I) {t : O} (ht : t ∈ I) (h0 : t ≠ 0) : (W.formalPoint hI ht).yCoord = -((algebraMap O K) (W.formalWEval t))⁻¹

The y-coordinate of the parametrized point is -1 / w(t).

theorem WeierstrassCurve.xCoord_formalPoint_mul_eq_one {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] {K : Type u_2} [Field K] [Algebra O K] (W : WeierstrassCurve O) [(W.baseChange K).IsElliptic] [FaithfulSMul O K] {I : Ideal O} (hI : IsAdic I) {t : O} (ht : t ∈ I) (ht0 : t ≠ 0) : (W.formalPoint hI ht).xCoord * (algebraMap O K) (t ^ 2 * W.formalUEval t) = 1

The x-coordinate in closed form: since w(t) = t ^ 3 * u(t) with u(t) a unit, the x-coordinate t / w(t) is the inverse of t ^ 2 * u(t). Stated as a product so that it needs no inverse; the exponent 2 is what a valuation would read as the pole order.

theorem WeierstrassCurve.yCoord_formalPoint_mul_eq_neg_one {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] {K : Type u_2} [Field K] [Algebra O K] (W : WeierstrassCurve O) [(W.baseChange K).IsElliptic] [FaithfulSMul O K] {I : Ideal O} (hI : IsAdic I) {t : O} (ht : t ∈ I) (ht0 : t ≠ 0) : (W.formalPoint hI ht).yCoord * (algebraMap O K) (t ^ 3 * W.formalUEval t) = -1

The y-coordinate in closed form: -1 / w(t) is minus the inverse of t ^ 3 * u(t), with exponent 3 where the x-coordinate has 2.

@[simp]

theorem WeierstrassCurve.neg_xCoord_div_yCoord_formalPoint {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] {K : Type u_2} [Field K] [Algebra O K] (W : WeierstrassCurve O) [(W.baseChange K).IsElliptic] [FaithfulSMul O K] {I : Ideal O} (hI : IsAdic I) {t : O} (ht : t ∈ I) : -(W.formalPoint hI ht).xCoord / (W.formalPoint hI ht).yCoord = (algebraMap O K) t

The parameter is recovered from the point as -x / y: the coordinates are t / w(t) and -1 / w(t), so their ratio cancels w(t). This is the identity that makes the parametrization injective, and hence the candidate injective side of Ê(𝔪) ≅ E₁(K). It covers the zero branch as well, where both coordinates and the parameter are 0.

@[simp]

theorem WeierstrassCurve.formalPoint_eq_zero_iff {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] {K : Type u_2} [Field K] [Algebra O K] (W : WeierstrassCurve O) [(W.baseChange K).IsElliptic] [FaithfulSMul O K] {I : Ideal O} (hI : IsAdic I) {t : O} (ht : t ∈ I) : W.formalPoint hI ht = 0 ↔ t = 0

The parametrization vanishes exactly at the zero parameter: the fibre over the point at infinity is exactly {0}. Calling that a kernel would be premature — no additive structure on the parameters is established here.

theorem WeierstrassCurve.formalPoint_injective {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] {K : Type u_2} [Field K] [Algebra O K] (W : WeierstrassCurve O) [(W.baseChange K).IsElliptic] [FaithfulSMul O K] {I : Ideal O} (hI : IsAdic I) : Function.Injective fun (t : ↥I) => W.formalPoint hI ⋯

The parametrization is injective on the parameters of I. Recovering the parameter as -x / y reduces this to injectivity of the structure map, and it is what would make the map the injective side of an identification with the kernel of reduction.

theorem WeierstrassCurve.formalPoint_eq_some {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] {K : Type u_2} [Field K] [Algebra O K] (W : WeierstrassCurve O) [(W.baseChange K).IsElliptic] [FaithfulSMul O K] {I : Ideal O} (hI : IsAdic I) {t s : O} (ht : t ∈ I) (hs : s ∈ I) {x y : K} (hns : (W.baseChange K).toAffine.Nonsingular x y) (hxt : (algebraMap O K) t * y = -x) (hys : (algebraMap O K) s * y = -1) : W.formalPoint hI ht = Affine.Point.some x y hns

A point of the curve is the parametrised point of -x / y as soon as -x / y and -1 / y both come from the ideal I. This is surjectivity of the parametrisation in its valuation-free form: which points satisfy the hypothesis is a separate question, answered over an adic completion in Point/Range.lean by exists_formalPoint_eq_of_one_lt_valuation_xCoord.

The two ratios are asked for as products, t * y = -x and s * y = -1, so that no division is needed to state the hypothesis and y ≠ 0 follows from the second rather than being assumed. The parameter s does not appear in the conclusion: it is there only to witness that -1 / y is a value of the ideal, and the proof identifies it as w(t), which is what pins the point down.

@[simp]

theorem WeierstrassCurve.formalPoint_formalInverseEval {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] {K : Type u_2} [Field K] [Algebra O K] (W : WeierstrassCurve O) [(W.baseChange K).IsElliptic] [FaithfulSMul O K] {I : Ideal O} (hI : IsAdic I) {t : O} (ht : t ∈ I) : W.formalPoint hI ⋯ = -W.formalPoint hI ht

The parametrisation respects negation. The formal inverse ι on parameters becomes the group inverse on points — on a generalised Weierstrass curve the negY transformation y ↦ -y - a₁x - a₃, not plain negation — so formalPoint carries the inverse law across.

Tagged @[simp] in the reducing orientation, towards point negation. Note that simp reaches it only where the parameter is syntactically formalInverseEval t: the parameter sits in the membership proof's type, so matching it otherwise would need higher-order unification.

@[simp]

theorem WeierstrassCurve.xRep_formalPoint_eq_iff {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_3) [Field K] [Algebra O K] [(W.baseChange K).IsElliptic] [FaithfulSMul O K] {I : Ideal O} (hI : IsAdic I) {t₁ t₂ : O} (h₁ : t₁ ∈ I) (h₂ : t₂ ∈ I) : (W.formalPoint hI h₂).xRep = (W.formalPoint hI h₁).xRep ↔ t₂ = t₁ ∨ t₂ = W.formalInverseEval t₁

Two parameters have points with the same x-coordinate exactly when they are equal or exchanged by the formal inverse. Over a field the x-coordinate determines a point up to negation, and the parametrisation respects negation, so t₁ and ι(t₁) are the only candidates.

Stated at equality of xRep, Mathlib's projective x-coordinate, which asks nothing of either parameter: the point at infinity has xRep = ![1, 0] and an affine point ![x, 1], so the left-hand side already forces the two parameters to vanish together. The right-hand side is about the parameters alone, so the field the coordinates are read in is an explicit argument.

theorem WeierstrassCurve.mul_formalWEval_eq_mul_formalWEval_iff {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_3) [Field K] [Algebra O K] [(W.baseChange K).IsElliptic] [FaithfulSMul O K] {I : Ideal O} (hI : IsAdic I) {t₁ t₂ : O} (h₁ : t₁ ∈ I) (h₂ : t₂ ∈ I) : t₁ * W.formalWEval t₂ = t₂ * W.formalWEval t₁ ↔ t₁ = 0 ∨ t₂ = 0 ∨ t₂ = t₁ ∨ t₂ = W.formalInverseEval t₁

The chord form of xRep_formalPoint_eq_iff: when the cross-product of parameters against w-values agrees.

w vanishes at 0, so a vanishing parameter satisfies the cross-product whatever the other one is; those two cases are therefore disjuncts of the conclusion rather than hypotheses. With both parameters nonzero the remaining two disjuncts are the dichotomy of xRep_formalPoint_eq_iff.

Not a simp lemma, unlike xRep_formalPoint_eq_iff: neither side names the field, so K and its instances would be left as metavariables that simp cannot solve. Rewrite with it explicitly.