Valuation estimates for the integral model of a Weierstrass curve

Source: MichaelStollBayreuth/EllipticCurves at commit 3f8c39c0fc4c0fd0a40e693aa2a9bbda08d9ee1f. Exact-pin changes are documented in PORTING.md.

This file specializes the formal-group evaluation layer to O = 𝒪_v (the valuation ring of an adic completion) and collects the technical estimates on which the geometric results rest: the valuation-integrality bookkeeping for the coordinates and coefficients of an integral model, the parameter-level vanishing of torsion in the kernel of reduction (points_eq_zero_of_nsmul_*, via the scaled formal logarithm), and the compactness and finite-quotient facts used downstream for the finite-index statements.

theorem WeierstrassCurve.Affine.valued_a₁ {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) : Valued.v W.a₁ ≤ 1

theorem WeierstrassCurve.Affine.valued_a₂ {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) : Valued.v W.a₂ ≤ 1

theorem WeierstrassCurve.Affine.valued_a₃ {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) : Valued.v W.a₃ ≤ 1

theorem WeierstrassCurve.Affine.valued_a₄ {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) : Valued.v W.a₄ ≤ 1

theorem WeierstrassCurve.Affine.integral_of_not_mem {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) {x y : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v} (hxy : W.Equation x y) (hx : ¬WithZero.exp 2 ≤ Valued.v x) : Valued.v x ≤ 1 ∧ Valued.v y ≤ 1

An affine point outside the kernel of reduction has integral coordinates: the only poles on a Weierstrass curve with integral coefficients have even order at x.

theorem WeierstrassCurve.Affine.valued_formalPoint_x {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} {t : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (ht : t ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (ht0 : t ≠ 0) : Valued.v (↑t / ↑(W₀.wEval t)) = (Valued.v ↑t)⁻¹ ^ 2

The valuation of the x-coordinate t/w(t) is v(t)⁻².