claimroutineinferred_dep

Localization membership transfers to valuation bounds

Shows membership in rl(RF)pr^l(R_F)_{\mathfrak p} gives v∗(D~′)≥lv_*(\widetilde D')\ge l
transfers localization membership to valuation bounds
Claim·§2.5 Odd valuations select a tested branch·inside lemOdd valuation selects a tested branch

Statement (paper)

If D′=rlX/YD'=r^lX/Y with X∈RFX\in R_F and Y∈RF∖pY\in R_F\setminus\mathfrak p, so that D′∈rl(RF)pD'\in r^l(R_F)_{\mathfrak p}, then w∗(D~′)≥l w∗(r~)w_*(\widetilde D')\ge l\,w_*(\widetilde r). Consequently, for every ordinary integer l≥1l\ge1 and every D′∈FRD'\in F_R, D′∈rl(RF)pD'\in r^l(R_F)_{\mathfrak p} implies v∗(D~′)≥lv_*(\widetilde D')\ge l. Moreover, every tested finite formal point xx satisfies 1/x∈r(RF)p1/x\in r(R_F)_{\mathfrak p}, so its actual xx-valuation is negative, and hence it reduces to OO for v∗v_* at the good integral model; the identity point reduces to OO as well.

In plain English

If D′=rlX/YD'=r^lX/Y with X∈RFX\in R_F and Y∈RF∖pY\in R_F\setminus\mathfrak p, then w∗(D~′)≥l w∗(r~)w_*(\widetilde D')\ge l\,w_*(\widetilde r). Hence D′∈rl(RF)pD'\in r^l(R_F)_{\mathfrak p} implies v∗(D~′)≥lv_*(\widetilde D')\ge l, and every tested finite formal point xx has 1/x∈r(RF)p1/x\in r(R_F)_{\mathfrak p}, negative xx-valuation, and reduces to OO for v∗v_*, as does the identity point.

Why it's here

This finishes the proof of the coarsening lemma. By the previous claim, the center of w∗w_* is the branch ideal p\mathfrak p, so elements outside p\mathfrak p have w∗w_*-value zero and the denominator YY costs nothing, which gives the valuation bound. The bound then gives the displayed transfer implication and forces tested formal points to reduce to OO at v∗v_*.
Classified routine:
Direct consequence of the previous claim that the center of w∗w_* is p\mathfrak p: units outside p\mathfrak p have w∗w_*-value zero, so the bound follows from the multiplicativity of valuations, and reduction to OO follows from the negative xx-valuation as in standard reduction of elliptic curve points.

Uses

claimCenter of coarsened valuation is a branch ideal

Used by

Nothing in the paper

Sources

PaperOpen
Section
§2.5 Odd valuations select a tested branch
Page
—
Label
—
Line
sections/02-reduction.tex:700
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Localization membership transfers to ambient valuation bounds" rests on claim-red-coarsening-3