Valuations of a Weierstrass function field that are integral on the coordinate ring

For a valuation of F(W) trivial on F, having no pole at the coordinate x forces the valuation to be at most 1 on the whole coordinate ring: W.CoordinateRing is integral over F[x], and a valuation is at most 1 exactly on what is integral over its integers. This bounds those elements; it does not compute their values.

This is the affine-chart half of the classification of such valuations. The other half is WeierstrassCurve.Affine.isEquiv_infinityPlace_of_one_lt, which settles the case 1 < v x: there the valuation is the place at infinity. Neither half needs any Place packaging — no normalization, no surjectivity, no Dedekind hypothesis and no ellipticity — which is why they are stated for a bare valuation.

Main results

• Valuation.algebraMap_coordinateRing_le_one: a valuation trivial on F with v x ≤ 1 is at most 1 on the whole coordinate ring.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, I.1.

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

A valuation of the function field with no pole at x is integral on the coordinate ring. For v trivial on F with v x ≤ 1, every element of W.CoordinateRing has value at most 1 in F(W).