The range of the formal parametrisation

Point/AdicCompletion.lean maps the formal-group parameters of the maximal ideal of 𝒪_v injectively into the points of the curve over the completion K_v. This file computes the image of that map: a point is parametrised exactly when it is the point at infinity, or its x-coordinate has a pole. Together with the injectivity already proved, this is the content of Silverman AEC VII.2.2 — the identification of the formal group Ê(𝔪) with the kernel of reduction E₁(K_v).

The image is described by the valuation of the x-coordinate, which is the condition that cuts out that kernel: a point of E(K_v) reduces to the point at infinity exactly when its x-coordinate has a pole. Neither reduction nor E₁ is named below, no reduction map on points entering the statements.

Main results

• WeierstrassCurve.one_lt_valuation_xCoord_formalPoint and WeierstrassCurve.exists_formalPoint_eq_of_one_lt_valuation_xCoord: the two inclusions over an adic completion.
• WeierstrassCurve.range_formalPointHomAdicCompletion: the range itself. Since the left-hand side is the range of an additive homomorphism, this exhibits the set of points on the right as a subgroup.
• WeierstrassCurve.valuation_xCoord_le_one_and_valuation_yCoord_le_one_of_notMem_range: outside the range both coordinates are integral.

References

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

Provenance

The parametrisation whose image is computed here, and its injectivity, come from the Stoll development pinned in Point/Basic.lean's provenance.

theorem WeierstrassCurve.instIsLinearTopologySubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers_tauCeti_1 {A : Type u_1} [CommRing A] [IsDedekindDomain A] {F : Type u_2} [Field F] [Algebra A F] [IsFractionRing A F] (u : IsDedekindDomain.HeightOneSpectrum A) : IsLinearTopology ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F u) ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F u)

theorem WeierstrassCurve.instFactIsAdicSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegersMaximalIdeal_tauCeti_1 {A : Type u_1} [CommRing A] [IsDedekindDomain A] {F : Type u_2} [Field F] [Algebra A F] [IsFractionRing A F] (u : IsDedekindDomain.HeightOneSpectrum A) : Fact (IsAdic (IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F u)))

theorem WeierstrassCurve.one_lt_valuation_xCoord_formalPoint {A : Type u_1} [CommRing A] [IsDedekindDomain A] {F : Type u_2} [Field F] [Algebra A F] [IsFractionRing A F] (u : IsDedekindDomain.HeightOneSpectrum A) (C : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F u)) [(C.baseChange (IsDedekindDomain.HeightOneSpectrum.adicCompletion F u)).IsElliptic] {t : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F u)} (ht : t ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F u)) (ht0 : t ≠ 0) : 1 < Valued.v (C.formalPoint ⋯ ht).xCoord

A nonzero parameter has a pole in the x-coordinate of its point. The closed form x * (t ^ 2 u(t)) = 1 of xCoord_formalPoint_mul_eq_one makes x inverse to an element of the maximal ideal, t lying there and u(t) being integral.

theorem WeierstrassCurve.exists_formalPoint_eq_of_one_lt_valuation_xCoord {A : Type u_1} [CommRing A] [IsDedekindDomain A] {F : Type u_2} [Field F] [Algebra A F] [IsFractionRing A F] (u : IsDedekindDomain.HeightOneSpectrum A) (C : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F u)) [(C.baseChange (IsDedekindDomain.HeightOneSpectrum.adicCompletion F u)).IsElliptic] {P : (C.baseChange (IsDedekindDomain.HeightOneSpectrum.adicCompletion F u)).toAffine.Point} (hP : 1 < Valued.v P.xCoord) : ∃ (t : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F u)) (ht : t ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F u)), C.formalPoint ⋯ ht = P

A point with a pole in its x-coordinate is parametrised, by the parameter -x / y. This is the converse of one_lt_valuation_xCoord_formalPoint, and the substantial half of Silverman AEC VII.2.2.

The pole of x is what puts both -x / y and -1 / y in the maximal ideal: v x < v y at such a point, so v (x / y) < 1, and 1 < v y gives v (1 / y) < 1.

@[simp]

theorem WeierstrassCurve.range_formalPointHomAdicCompletion {A : Type u_1} [CommRing A] [IsDedekindDomain A] {F : Type u_2} [Field F] [Algebra A F] [IsFractionRing A F] (u : IsDedekindDomain.HeightOneSpectrum A) (C : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F u)) [(C.baseChange (IsDedekindDomain.HeightOneSpectrum.adicCompletion F u)).IsElliptic] : Set.range ⇑(formalPointHomAdicCompletion u C) = {P : (C.baseChange (IsDedekindDomain.HeightOneSpectrum.adicCompletion F u)).toAffine.Point | P = 0 ∨ 1 < Valued.v P.xCoord}

The range of the formal parametrisation of an adic completion: the point at infinity together with the points whose x-coordinate has a pole. Since the left-hand side is the range of an additive homomorphism, this exhibits that set of points as a subgroup; classically it is the kernel of reduction E₁(K_v).

theorem WeierstrassCurve.valuation_xCoord_le_one_and_valuation_yCoord_le_one_of_notMem_range {A : Type u_1} [CommRing A] [IsDedekindDomain A] {F : Type u_2} [Field F] [Algebra A F] [IsFractionRing A F] (u : IsDedekindDomain.HeightOneSpectrum A) (C : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F u)) [(C.baseChange (IsDedekindDomain.HeightOneSpectrum.adicCompletion F u)).IsElliptic] {P : (C.baseChange (IsDedekindDomain.HeightOneSpectrum.adicCompletion F u)).toAffine.Point} (hP : P ∉ (formalPointHomAdicCompletion u C).range) : Valued.v P.xCoord ≤ 1 ∧ Valued.v P.yCoord ≤ 1

A point outside the range has integral coordinates. The parametrised points are exactly those with a pole, so a point of the complement has v x ≤ 1, and then the Weierstrass equation forces v y ≤ 1 as well. This is the other half of the dichotomy of Affine/ValuationIntegrality.lean, read against the range.