claimroutineinferred_dep

Coarsened valuation nonnegative on R_F, positive on r

Shows coarsened valuation is ≥0\ge0 on RFR_F and positive on rr
gives the coarsened valuation a center containing r
Claim·§2.5 Odd valuations select a tested branch·inside lemOdd valuation selects a tested branch

Statement (paper)

The value vq(r~)v_q(\widetilde r) is positive, and the coarsened valuation w∗w_* of ∗F{}^*F obtained from an extension v∗v_* of vqv_q by passing to the ordered quotient ∗Z/J{}^*\Z/J satisfies w∗(x~)≥0w_*(\widetilde x)\ge0 for every x∈RFx\in R_F, while w∗(r~)>0w_*(\widetilde r)>0.

In plain English

The value vq(r~)v_q(\widetilde r) is positive. Passing from an extension v∗v_* of vqv_q to the coarsened valuation w∗w_* with values in ∗Z/J{}^*\Z/J gives w∗(x~)≥0w_*(\widetilde x)\ge 0 for all x∈RFx\in R_F and w∗(r~)>0w_*(\widetilde r)>0.

Why it's here

This shows that the coarsened valuation w∗w_* has a center on RFR_F that contains rr. The claim that follows uses it to identify that center as a prime ideal and then as one of the tested branch ideals p±\mathfrak p_\pm. The even-valuation claim for elements of RR inside JJ is what makes the coarsening to ∗Z/J{}^*\Z/J well behaved, so that negative values are absorbed into JJ and RFR_F is nonnegative.
Classified routine:
A direct step inside the proof of the red-coarsening lemma: it follows from the preceding even-valuation claim together with the standard construction of a coarsened valuation via the quotient of the value group by a convex subgroup.

Uses

claimRing valuations inside J are even

Used by

claimCenter of coarsened valuation is a branch ideal

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Coarsened valuation nonnegative on R_F, positive on r" rests on claim-red-coarsening-1