Integral points of a Weierstrass curve over a valued field #
Let F be a field, let v be a valuation on F, let O be the valuation subring of v, and
let W be a Weierstrass curve over F admitting a model over O. This file records the
valuation estimates that such a model forces, and the dichotomy they produce for the coordinates
of an affine point.
The dichotomy is the sharp one: v(x) is never exp 1. Either the point is integral,
v(x) ≤ 1 and v(y) ≤ 1, or it is a pole of order at least two in x, exp 2 ≤ v(x). There is
nothing in between: at a pole v(y)² = v(x)³, and exp 3 is not a square, which rules out the
one intermediate value. Only pole order one is excluded here — the general statement that every
pole order is even is not proved.
The two halves need different hypotheses, and are stated that way. The coefficient bounds — and
the estimates on the two sides of the Weierstrass equation — never look at the value group, so
they are stated for an arbitrary Γ₀. Only the dichotomy needs Γ₀ = ℤᵐ⁰, because the parity
argument that rules out v(x) = exp 1 is about the exponent being an integer.
The valuation is taken as an explicit argument rather than through Valued F Γ₀. Nothing here
uses a topology, and a fixed field carries many valuations at once — the intended consumers are
the IsDedekindDomain.HeightOneSpectrum.valuation of a varying prime, which cannot all be
Valued instances on F simultaneously.
Main results #
WeierstrassCurve.Affine.valuation_a₁_le_oneand itsa₂,a₃,a₄,a₆companions: the coefficients of a curve with an integral model are integral, over any value group.WeierstrassCurve.Affine.valuation_x_lt_valuation_y: at a pole ofx, they-coordinate strictly dominates.WeierstrassCurve.Affine.valuation_y_sq_eq_valuation_x_cube: at a pole ofx, the two coordinates have poles in ratio two to three, over any value group.WeierstrassCurve.Affine.valuation_y_le_one_of_valuation_x_le_one: an integralx-coordinate forces an integraly-coordinate, over any value group.WeierstrassCurve.Affine.valuation_x_le_one_and_valuation_y_le_one_of_valuation_x_lt_exp_two: an affine point whosex-coordinate has a pole of order less than two has both coordinates integral.
Implementation notes #
The hypothesis "W has a model over O" is Mathlib's WeierstrassCurve.IsIntegral O W, and the
model itself is WeierstrassCurve.integralModel O W; the coefficient bounds are then Mathlib's
WeierstrassCurve.integralModel_aᵢ_eq composed with membership in O.
The y-half of the dichotomy is not reproved by a valuation computation. Once x is known to be
integral, WeierstrassCurve.isIntegral_y_of_equation_of_isIntegral_x gives that y is
integral over O from the curve equation alone, over any algebra and with no valuation in sight;
O is a valuation subring, hence integrally closed in F, so integrality over it is membership.
That is how the main theorem discharges its y-half. Only the x-half — the parity argument that
rules out v(x) = exp 1 — is genuinely about the valuation, and it is the only half that needs
the estimates below.
The estimates distinguish integral points from points reducing to infinity. Over a complete discretely valued field, they connect the formal group at infinity to the kernel of reduction.
References #
- J. Silverman, The Arithmetic of Elliptic Curves, VII.2 — the characterisation
of
E₁(K)that this dichotomy underlies.
Provenance #
Adapted from the Stoll EllipticCurves development
(github.com/MichaelStollBayreuth/EllipticCurves, Apache-2.0, at 66889eada51a),
EllipticCurves/WeierstrassFormalGroup/Foundations.lean: valued_a₁–valued_a₄ (:125–:128),
valued_a₆ (:129), valued_lhs_eq_rhs (:72), valued_rhs_eq (:132), valued_lhs_eq (:164),
valued_lhs_le (:185), valued_ne_exp_one (:202) and integral_of_not_mem (:264), which is
valuation_x_le_one_and_valuation_y_le_one_of_valuation_x_lt_exp_two here.
The main departures are as follows. The source's private coe_a₁–coe_a₆ (:110–:122) are not
ported: they restate
the structure map for a model carried in the signature, whereas the model here is Mathlib's
integralModel, so the five coefficient bounds are integralModel_aᵢ_eq plus membership in O.
The setting is more general: the source works over v.adicCompletion K and
v.adicCompletionIntegers K, whereas no step uses completeness, the Dedekind hypothesis, or a
topology, so the results are stated for a bare (v : Valuation F Γ₀) and its valuation subring —
a weaker hypothesis set that still covers the source's case, adicCompletionIntegers being by
definition the valuation subring of Valued.v. valuation_a₆_le_one is public here although the
source's valued_a₆ (:129) is private: the five coefficient bounds are one API, and a consumer
holding an integral model needs all five. The hypothesis is stated positively as v x < exp 2
rather than the source's ¬ exp 2 ≤ v x. And the y-half is proved by reuse rather than by the
source's valuation computation: the source derives it from a valued_rhs_le bound (:151), whereas
here isIntegral_y_of_equation_of_isIntegral_x plus integral closedness of O gives it directly,
so that bound has no consumer and is not ported.
The coefficient bounds, over an arbitrary value group #
Nothing in this section looks at the value group: an integral model bounds the coefficients, and
the two sides of the Weierstrass equation are estimated, for any Γ₀. Only the dichotomy below
needs Γ₀ = ℤᵐ⁰.
Field F remains necessary for the coefficient bounds because Valuation.valuationSubring is
defined only for a field.
A curve over a trivially valued base has an integral model. Every coefficient of W⁄K is
the image of one of W's, and a valuation trivial on F puts all of those in its valuation
subring.
The a₁-coefficient of a curve with an integral model is integral.
The a₂-coefficient of a curve with an integral model is integral.
The a₃-coefficient of a curve with an integral model is integral.
The a₄-coefficient of a curve with an integral model is integral.
The a₆-coefficient of a curve with an integral model is integral.
At a pole of x, the y-coordinate strictly dominates.
A pole of x forces one of y, of three halves the order. On a point of the curve whose
x-coordinate is not integral, v(y)² = v(x)³: writing the valuations additively, x has a pole
of order 2e and y one of order 3e. Neither coordinate can dominate the other by any other
ratio, because the two sides of the Weierstrass equation must agree.
An integral x-coordinate forces an integral y-coordinate, over any value group.
The dichotomy, over a discretely valued field #
This is where Γ₀ = ℤᵐ⁰ is used: the parity argument that rules out v(x) = exp 1 needs the
value group to be ℤ. The bounds above are applied at Γ₀ := ℤᵐ⁰.
An affine point whose x-coordinate has pole order less than two is integral.
The x-coordinate of an affine point of W is either integral or has a pole of order at least
two, and in the former case the y-coordinate is integral too.