claimroutineinferred_dep

Power-series valuation of order one

Claim·§8.4 A separate odd valuation for each radicand·inside lemPrivate odd valuation for each radicand

Statement (paper)

There is an embedding K0(V1)↪K0((T))K_0(V_1)\hookrightarrow K_0((T)) sending zz to a+Ta+T, obtained by solving f(a+T,b+c1T+c2T2+⋯ )=0f(a+T,b+c_1T+c_2T^2+\cdots)=0 recursively in K0[[T]]K_0[[T]], under which Lℓ=T(b−wrℓ+O(T))L_\ell=T\bigl(b-w_{r_\ell}+O(T)\bigr) has order one, while Lℓ−4L_\ell-4 and all Lm(Lm−4)L_m(L_m-4), m≠ℓm\ne\ell, have nonzero constant terms. Hence the order in TT is a valuation over K0K_0 with the required properties.

In plain English

The function field K0(V1)K_0(V_1) embeds into K0((T))K_0((T)) with z↦a+Tz\mapsto a+T, by solving f(a+T,b+c1T+c2T2+⋯ )=0f(a+T,b+c_1T+c_2T^2+\cdots)=0 recursively. Under this embedding LℓL_\ell has TT-order exactly one, while Lℓ−4L_\ell-4 and every Lm(Lm−4)L_m(L_m-4) with m≠ℓm\ne\ell have nonzero constant term, so the TT-order is a valuation over K0K_0 with the required properties.

Why it's here

Since fw(a,b)≠0f_w(a,b)\ne0 at the point sℓ=(a,b)s_\ell=(a,b), Hensel-style recursion gives a unique power-series branch, and b≠wrℓb\ne w_{r_\ell} makes the leading coefficient b−wrℓb-w_{r_\ell} of LℓL_\ell nonzero, so LℓL_\ell has order one. The previous claim shows the other radicands are nonzero and not 44 at sℓs_\ell, so they have order zero. This yields the odd valuation vℓv_\ell with vℓ(Dℓ)=1v_\ell(D_\ell)=1 and vℓ(Dm)=0v_\ell(D_m)=0 for m≠ℓm\ne\ell.
Classified routine:
Standard construction of a discrete valuation at a smooth point of a plane curve via its Hensel/implicit-function power-series branch (local parametrization at a nonsingular point), combined with the earlier claims on the chosen point s_ell.

Uses

claimSimple point on curve away from anchorclaimOther radicands avoid 0 and 4 at s_ell

Used by

claimSubset products of radicands are non-squares

Sources

PaperOpen
Section
§8.4 A separate odd valuation for each radicand
Page
—
Label
—
Line
sections/07-algebra.tex:510
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Power-series embedding gives order-one valuation" rests on claim-alg-private-valuations-2
  • info
    inferred_dep
    outline: "Power-series embedding gives order-one valuation" rests on claim-alg-private-valuations-3