The valuation at infinity on the function field of a Weierstrass curve #

The function field F(W) of an affine Weierstrass curve is a quadratic extension of the rational function field F(x) (WeierstrassCurve.Affine.finrank_functionField), so every function has an algebra norm there. Composing that norm with Mathlib's place at infinity of F(x) gives the place at infinity of the curve: ord_∞ f = -deg N f, the place where x and y have their poles.

Main definitions #

WeierstrassCurve.Affine.infinityPlace: the valuation at infinity, Valuation W.FunctionField (WithZero (Multiplicative ℤ)), as RatFunc.inftyValuation composed with Algebra.norm.

Main results #

The valuation's map_add_le_max' rests on an ultrametric inequality in degree form, proved here; the other three axioms are the norm's multiplicativity and Mathlib's place at infinity.

WeierstrassCurve.Affine.infinityPlace.X, WeierstrassCurve.Affine.infinityPlace.mk_Y: v_∞ x = exp 2 and v_∞ y = exp 3 — the double and triple poles at infinity, ord_∞ x = -2 and ord_∞ y = -3, which is what Layer 0 asks for by name. They read this file's two natDegree_norm_* helpers through Algebra.norm_localization and Mathlib's polynomial valuation.
WeierstrassCurve.Affine.infinityPlace.algebraMap_eq_sq: restricting along RatFunc F → W.FunctionField squares RatFunc.inftyValuation, so the place at infinity is ramified of index two over the infinite place of F(x).
WeierstrassCurve.Affine.infinityPlace.C: the valuation is trivial on the base field — a nonzero constant has value 1, the constant case of the previous result. The Valuation.IsTrivialOn F and Valuation.IsNontrivial instances follow, so the place is usable through Mathlib's standard valuation API.
WeierstrassCurve.Affine.infinityPlace.X_div_mk_Y and WeierstrassCurve.Affine.infinityPlace.isUniformizer_X_div_mk_Y: x / y is a uniformiser at infinity. Its value is exp (-1), and it is a uniformiser in Mathlib's Valuation.IsUniformizer sense. That the place is discrete of rank one needs no proof here — its value group is a nontrivial subgroup of the cyclic ℤᵐ⁰ˣ, so Mathlib's IsRankOneDiscrete instance fires by itself — but the generator does: discreteness alone permits exp (-n) with n ≥ 1, and the proper subgroup 2ℤ genuinely occurs, being the value group of the restriction of v_∞ to F(x). One element of value exp (-1) settles it, which is what the value above is.
WeierstrassCurve.Affine.infinityPlace_ne_heightOneSpectrum_valuation: the place at infinity is distinct from the valuation of every height-one prime of the coordinate ring — the affine places. With CoordinateRing.pointPlace_eq_iff that makes the whole point-to-place assignment injective, the point at infinity included.

The two coordinate-function values each come in a second @[simp] form, stated in the shape simp actually normalises them to (the note above infinityPlace.X explains why the coordinate forms cannot carry the tag themselves). The quotient value gets no restatement of its own: map_div₀ is a simp lemma, so simp decomposes the quotient through the two atomic restatements. The machinery that builds the ultrametric inequality is private, and the norm-degree theory it rests on lives in FunctionField/Norm.lean.

Roadmap #

TauCetiRoadmap/EllipticCurves/README.md, Layer 0 (the function field, places, and divisors), whose §Places asks for the one further place W.infinityPlace beyond the affine ones, sitting "where x and y have their poles", with ord_∞ x = -2, ord_∞ y = -3. This file supplies the valuation, those two degrees, and the uniformiser x / y — §Places lists "ord_v, uniformisers, residue fields, the degree deg v" as the API the later layers consume. Suggested.lean seeds no declaration it competes with, recording that the function-field layer's "types are new API and are built there, not pinned here".

Provenance #

The route is that of the AINTLIB HasseWeil project (github.com/CBirkbeck/AINTLIB, Apache-2.0, dev/hasse-weil at a582951fe96b), HasseWeil/Curves/Infinity.lean: normAsRatFunc, ordAtInfty, ordAtInfty_mul, ordAtInfty_add_ge_min (tagged T-ORD-ARITH-12) and ordAtInfty_coordX/ordAtInfty_coordY.

The ramification statement corresponds to that project's Curves/OrdAtInftyRamification.lean and Curves/RamificationAtInfinity.lean; there it is an order identity for a WithTop ℤ-valued ordAtInfty over the SmoothPlaneCurve wrapper, where here it is an equality of Mathlib Valuations and follows from Algebra.norm_algebraMap with finrank_functionField.

Changes from the source. There ordAtInfty is a definition of its own, valued in WithTop ℤ, built over a SmoothPlaneCurve structure wrapping WeierstrassCurve.Affine, with multiplicativity, vanishing and the ultrametric bound all proved by hand. Here the norm is Mathlib's Algebra.norm and the target is Mathlib's ℤᵐ⁰, so the result is a genuine Valuation uniform with RatFunc.inftyValuation and IsDedekindDomain.HeightOneSpectrum.valuation; multiplicativity and vanishing are map_mul and Algebra.norm_zero, and only the ultrametric inequality is reproved.

The uniformiser corresponds to that project's projects/HasseWeil/HasseWeil/Foundation/LocalExpansion.lean at main 1c1c7466, localParam — the local parameter t = -x/y at O (Silverman IV.1) — whose uniformising property is recorded there through a Laurent-series embedding (localExpand_localParam), over a SmoothPlaneCurve and that development's own WithTop ℤ-valued ordAtInfty. None of that apparatus is needed here: the value of x / y is two rewrites from the two pole orders, and Mathlib's Valuation.IsRankOneDiscrete.generator_eq_exp_neg_one_of_mem_range turns that single value into the generator, so the conclusion is Mathlib's Valuation.IsUniformizer directly. The sign is dropped, x / y and -x / y having the same valuation.