The place at infinity is the only place of F(W) where x has a pole

FunctionField/InfinityPlace/Basic.lean builds the valuation W.infinityPlace of the function field of an affine Weierstrass curve and computes v_∞ x = exp 2, so x has a pole there. This file proves the converse, and with it the uniqueness of that place: a valuation of F(W) which is trivial on F and gives x a value greater than 1 is equivalent to W.infinityPlace. Equivalence of valuations is the right conclusion — the hypothesis does not see the value group, and a valuation is only ever determined up to equivalence by its valuation ring.

The route has three steps, and none of them needs a Riemann–Roch theorem or a normalisation.

• On the rational functions the values are forced. Restricting v along F(x) → F(W) gives a valuation of F(x), trivial on F, with v x > 1; Mathlib's Ostrowski file evaluates such a valuation outright, v A = (v x) ^ A.intDegree (RatFunc.valuation_eq_valuation_X_zpow_intDegree_of_one_lt_valuation_X). So the pole order of a rational function is its degree, for v and for v_∞ alike.
• The Weierstrass equation fixes v y. Reading y (y + a₁x + a₃) = x³ + a₂x² + a₄x + a₆ through v, the cubic on the right has value (v x) ^ 3 by the previous step, while the left factor y + a₁x + a₃ has value max (v y) (v x); a value of y at most v x would make the left-hand side at most (v x) ^ 2. Hence v x < v y and (v y) ^ 2 = (v x) ^ 3. This is the familiar ord_∞ x = -2, ord_∞ y = -3 — but as a consequence of v x > 1, over any value group, so it is available before the place is known.
• Every function is A + B y and the two terms never cancel. F(W) is spanned by 1 and y over F(x), so a function is A + B y with A, B rational. Squaring, the two values are (v x) ^ (2 · deg A) and (v x) ^ (2 · deg B + 3), whose exponents differ in parity, so they are never equal and the valuation of the sum is the larger of the two. Hence v (A + B y) ≤ 1 holds exactly when deg A ≤ 0 and 2 · deg B + 3 ≤ 0 — a condition on two integers with no mention of v. Two valuations satisfying the hypothesis therefore have the same integers, so they are equivalent.

Main results

• WeierstrassCurve.Affine.isEquiv_infinityPlace_of_one_lt: the uniqueness theorem — a valuation of F(W) trivial on F at which x has a pole is equivalent to W.infinityPlace.
• WeierstrassCurve.Affine.val_algebraMap_eq_zpow_intDegree and WeierstrassCurve.Affine.val_algebraMap_eq_pow_natDegree: the value of a rational function, and of a polynomial, in x, as a power of v x; val_algebraMap_le_pow is the bound that also covers the zero polynomial.
• WeierstrassCurve.Affine.val_X_lt_val_mk_Y and WeierstrassCurve.Affine.val_mk_Y_sq: v x < v y and (v y) ^ 2 = (v x) ^ 3 — the pole orders 2 and 3, for any such v.
• WeierstrassCurve.Affine.val_add_mul_mk_Y_le_one_iff: the criterion the theorem is proved by, worth stating because it computes the valuation ring of every such v in closed form.
• WeierstrassCurve.Affine.exists_ratFunc_add_mul_mk_Y: every function is A + B y with A and B rational — the spanning half of the quadratic extension, in the form these arguments use.
• WeierstrassCurve.Affine.mk_Y_mul_add_eq: the Weierstrass equation, read in the function field.
• WeierstrassCurve.Affine.one_lt_infinityPlace_X: 1 < v_∞ x, the instance of the hypothesis that W.infinityPlace itself satisfies.

The hypotheses are exactly v.IsTrivialOn F and 1 < v x: no ellipticity, no nonsingularity, no perfect or algebraically closed base field, and no Dedekind hypothesis on the coordinate ring. The Weierstrass equation is the only geometry used, and it holds for singular cubics too.

What is deliberately not here

The affine-place classification. The complementary case v x ≤ 1 requires the coordinate ring, whereas this file uses only the Weierstrass equation. The downstream file Affine/FunctionField/PointPlace.lean proves that case with the generic affine-model place API, packages the infinity valuation as TauCeti.Place.infinity, and combines both cases into the point--place dictionary.

No divisor group. The downstream point--place file supplies a unified normalized place type and its degree. Building divisors as finite formal sums of all such places remains separate work.

Roadmap

TauCetiRoadmap/EllipticCurves/README.md, Layer 0 (the function field, places, and divisors). Its §Places asks for "the places of W.FunctionField over K" with W.infinityPlace singled out as the one place beyond the affine ones; this is the statement that pins it down, and it is what turns a valuation produced by some construction — the restriction of v_∞ along an isogeny, in Isogeny/InfinityPlace.lean — into the place at infinity. The dual-isogeny milestone of Layer 1 names that step: "an unpointed induced-place map for finite function-field embeddings, with the named criterion MapsInfinity λ ↔ λ_*(O₂) = O₃".

Provenance

Not a port, and no code from an external formalisation is copied or adapted here. The one substantial input is Mathlib's RatFunc.valuation_eq_valuation_X_zpow_intDegree_of_one_lt_valuation_X (María Inés de Frutos-Fernández, Xavier Généreux, from the Ostrowski file for K(X)), which does the rational-function half; the rest is the Weierstrass equation and the quadratic extension.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, second edition, I.1–I.2.
• J. Silverman, The Arithmetic of Elliptic Curves, II.2.

theorem WeierstrassCurve.Affine.instIsTrivialOnRatFuncComapFunctionFieldAlgebraMap_tauCeti {F : Type u_1} [Field F] {Γ : Type u_2} [LinearOrderedCommGroupWithZero Γ] {W : Affine F} (v : Valuation W.FunctionField Γ) [Valuation.IsTrivialOn F v] : Valuation.IsTrivialOn F (Valuation.comap (algebraMap (RatFunc F) W.FunctionField) v)

theorem WeierstrassCurve.Affine.val_algebraMap_eq_zpow_intDegree {F : Type u_1} [Field F] {Γ : Type u_2} [LinearOrderedCommGroupWithZero Γ] {W : Affine F} (v : Valuation W.FunctionField Γ) [Valuation.IsTrivialOn F v] (hx : 1 < v ((algebraMap (Polynomial F) W.FunctionField) Polynomial.X)) {A : RatFunc F} (hA : A ≠ 0) : v ((algebraMap (RatFunc F) W.FunctionField) A) = v ((algebraMap (Polynomial F) W.FunctionField) Polynomial.X) ^ A.intDegree

A rational function in x is valued at its degree: v A = (v x) ^ deg A. This is Mathlib's evaluation of a valuation of F(x) with v X > 1, restricted along F(x) → F(W).

theorem WeierstrassCurve.Affine.val_algebraMap_eq_pow_natDegree {F : Type u_1} [Field F] {Γ : Type u_2} [LinearOrderedCommGroupWithZero Γ] {W : Affine F} (v : Valuation W.FunctionField Γ) [Valuation.IsTrivialOn F v] (hx : 1 < v ((algebraMap (Polynomial F) W.FunctionField) Polynomial.X)) {p : Polynomial F} (hp : p ≠ 0) : v ((algebraMap (Polynomial F) W.FunctionField) p) = v ((algebraMap (Polynomial F) W.FunctionField) Polynomial.X) ^ p.natDegree

A polynomial in x is valued at its degree: v p = (v x) ^ natDegree p.

theorem WeierstrassCurve.Affine.val_algebraMap_le_pow {F : Type u_1} [Field F] {Γ : Type u_2} [LinearOrderedCommGroupWithZero Γ] {W : Affine F} (v : Valuation W.FunctionField Γ) [Valuation.IsTrivialOn F v] (hx : 1 < v ((algebraMap (Polynomial F) W.FunctionField) Polynomial.X)) {p : Polynomial F} {n : ℕ} (hp : p.natDegree ≤ n) : v ((algebraMap (Polynomial F) W.FunctionField) p) ≤ v ((algebraMap (Polynomial F) W.FunctionField) Polynomial.X) ^ n

The degree bound form, which also covers p = 0: a polynomial of degree at most n in x has value at most (v x) ^ n.

theorem WeierstrassCurve.Affine.mk_Y_mul_add_eq {F : Type u_1} [Field F] (W : Affine F) : (algebraMap W.CoordinateRing W.FunctionField) ((CoordinateRing.mk W) Polynomial.X) * ((algebraMap W.CoordinateRing W.FunctionField) ((CoordinateRing.mk W) Polynomial.X) + (algebraMap (Polynomial F) W.FunctionField) (Polynomial.C W.a₁ * Polynomial.X + Polynomial.C W.a₃)) = (algebraMap (Polynomial F) W.FunctionField) (Polynomial.X ^ 3 + Polynomial.C W.a₂ * Polynomial.X ^ 2 + Polynomial.C W.a₄ * Polynomial.X + Polynomial.C W.a₆)

The Weierstrass equation, in the function field: y * (y + (a₁X + a₃)) = X³ + a₂X² + a₄X + a₆. Grouping the two left-hand terms as a product is what makes the valuation of the left-hand side a product of two values, which is how the pole orders of x and y are compared below.

theorem WeierstrassCurve.Affine.exists_ratFunc_add_mul_mk_Y {F : Type u_1} [Field F] (W : Affine F) (z : W.FunctionField) : ∃ (A : RatFunc F) (B : RatFunc F), (algebraMap (RatFunc F) W.FunctionField) A + (algebraMap (RatFunc F) W.FunctionField) B * (algebraMap W.CoordinateRing W.FunctionField) ((CoordinateRing.mk W) Polynomial.X) = z

Every function is A + B y with A and B rational functions of x. Clearing a polynomial denominator reduces to the coordinate ring, where Mathlib's basis {1, Y} supplies the decomposition.

theorem WeierstrassCurve.Affine.val_X_lt_val_mk_Y {F : Type u_1} [Field F] {Γ : Type u_2} [LinearOrderedCommGroupWithZero Γ] {W : Affine F} (v : Valuation W.FunctionField Γ) [Valuation.IsTrivialOn F v] (hx : 1 < v ((algebraMap (Polynomial F) W.FunctionField) Polynomial.X)) : v ((algebraMap (Polynomial F) W.FunctionField) Polynomial.X) < v ((algebraMap W.CoordinateRing W.FunctionField) ((CoordinateRing.mk W) Polynomial.X))

y has a higher pole than x.

theorem WeierstrassCurve.Affine.val_mk_Y_sq {F : Type u_1} [Field F] {Γ : Type u_2} [LinearOrderedCommGroupWithZero Γ] {W : Affine F} (v : Valuation W.FunctionField Γ) [Valuation.IsTrivialOn F v] (hx : 1 < v ((algebraMap (Polynomial F) W.FunctionField) Polynomial.X)) : v ((algebraMap W.CoordinateRing W.FunctionField) ((CoordinateRing.mk W) Polynomial.X)) ^ 2 = v ((algebraMap (Polynomial F) W.FunctionField) Polynomial.X) ^ 3

The pole orders of x and y are in the ratio 2 : 3: (v y) ^ 2 = (v x) ^ 3. Once v x < v y is known, the second factor of the Weierstrass equation has value v y.

theorem WeierstrassCurve.Affine.val_add_mul_mk_Y_le_one_iff {F : Type u_1} [Field F] {Γ : Type u_2} [LinearOrderedCommGroupWithZero Γ] {W : Affine F} (v : Valuation W.FunctionField Γ) [Valuation.IsTrivialOn F v] (hx : 1 < v ((algebraMap (Polynomial F) W.FunctionField) Polynomial.X)) (A B : RatFunc F) : v ((algebraMap (RatFunc F) W.FunctionField) A + (algebraMap (RatFunc F) W.FunctionField) B * (algebraMap W.CoordinateRing W.FunctionField) ((CoordinateRing.mk W) Polynomial.X)) ≤ 1 ↔ (A = 0 ∨ A.intDegree ≤ 0) ∧ (B = 0 ∨ 2 * B.intDegree + 3 ≤ 0)

The valuation ring of v, in closed form: A + B y lies in it exactly when deg A ≤ 0 and 2 deg B + 3 ≤ 0. The two summands never have the same value — after squaring, their exponents have opposite parities — so the valuation of the sum is the larger of the two, and the resulting condition mentions v nowhere.

theorem WeierstrassCurve.Affine.one_lt_infinityPlace_X {F : Type u_1} [Field F] (W : Affine F) : 1 < W.infinityPlace ((algebraMap (Polynomial F) W.FunctionField) Polynomial.X)

x has a pole at the place at infinity: 1 < v_∞ x, since v_∞ x = exp 2. This is the instance of the uniqueness theorem's hypothesis satisfied by W.infinityPlace itself.

theorem WeierstrassCurve.Affine.isEquiv_infinityPlace_of_one_lt {F : Type u_1} [Field F] {Γ : Type u_2} [LinearOrderedCommGroupWithZero Γ] {W : Affine F} (v : Valuation W.FunctionField Γ) [Valuation.IsTrivialOn F v] (hx : 1 < v ((algebraMap (Polynomial F) W.FunctionField) Polynomial.X)) : v.IsEquiv W.infinityPlace

The place at infinity is the only place of F(W) at which x has a pole: a valuation of the function field which is trivial on the base field and satisfies 1 < v x is equivalent to W.infinityPlace. Both valuations satisfy val_add_mul_mk_Y_le_one_iff, whose right-hand side is a condition on two integers, so their valuation rings agree.