Discrete valuation

Stream: maths

[Andrew Yang]

Is the current definition of docs#ValuativeRel.IsDiscrete (which says that there exists a maximal element with valuation < 1) correct?
In particular, the map $v : R[X_i]_{i \in \mathbb{Q}_{>0}} \to \mathbb{Q} \cup\{\bot\}$, $f \mapsto \deg f$ (with $X_i$ having degree $i$) is a valuation that satisfies docs#ValuativeRel.IsDiscrete (because the only element with degree < 0 is 0) but it doesn't feel like a discrete valuation to me.

[Kenny Lau]

feels similar to #27990 :smile:

[Kenny Lau]

i guess the question to ask here is what do you want to gain from a definition of "discrete valuation" specifically in this case where you apply it to not-fields

[Filippo A. E. Nuccio]

Pinging @Antoine Chambert-Loir with whom we had similar discussions.

[Yakov Pechersky]

Would you rather it be that the value group is not densely ordered?

[Yakov Pechersky]

Which is stronger, and implies the current definition afaiu

[Yakov Pechersky]

The IsDiscrete currently is sufficient for the iff statement that says that a field F with IsDiscrete valuative relation will have an IsDVR valuation subring, again afaiu

[Adam Topaz]

Andrew Yang said:

Is the current definition of docs#ValuativeRel.IsDiscrete (which says that there exists a maximal element with valuation < 1) correct?
In particular, the map $v : R[X_i]_{i \in \mathbb{Q}_{>0}} \to \mathbb{Q} \cup\{\bot\}$, $f \mapsto \deg f$ (with $X_i$ having degree $i$) is a valuation that satisfies docs#ValuativeRel.IsDiscrete (because the only element with degree < 0 is 0) but it doesn't feel like a discrete valuation to me.

If the value group is $\mathbb{Q}$ then it won't be discrete.

[Adam Topaz]

The value group in the sense of ValuativeRel is actually the value group, not the image of the valuation. So even if you have a valuation taking values in $\mathbb{Q}$ whose image is the nonnegative rationals, the value group would still be the rationals.

[Adam Topaz]

It would be helpful if you could say explicitly what you expect the value group to be in your example, as a type satisfying LinearOrderedCommmGroupWithZero

[Adam Topaz]

Concerning the remark about "non fields". The way to think about this construction is as follows. If you have a valuation $v$ on a ring $R$, then it has a support which is a prime ideal $\mathfrak{p}$, and the valuation induces a valuation on the residue field $\kappa(\mathfrak{p})$ with the same value group. This construction can be reversed, and so any valuation in the sense of ValuativeRel arises from a valuation on a field.

[Adam Topaz]

In @Andrew Yang 's example, the support is the zero ideal, so this valuation should really arise from a valuation on the fraction field of the ring.

[Kenny Lau]

@Adam Topaz I'm not sure what you're referring to. You seem to be agreeing with Andrew's observation.

[Adam Topaz]

I’m saying that I don’t think his example satisfies IsDiscrete

[Andrew Yang]

No, Adam is correct that I overlooked the definition of IsDiscrete and that the current def seems fine to me now.

[Kenny Lau]

aha, I also overlooked it because it doesn't show the types in the docs :upside_down:

[Adam Topaz]

Yeah the notation in the docs can be confusing. It will take some time to get used to the fact that the relation on the ring is denoted $\le_v$ and that the value group is the one with a usual order.

[Yakov Pechersky]

Should we have IsDiscrete => not DenselyOrdered?

[Antoine Chambert-Loir]

Just to add an argument from authority: I was reviewing a Habilitation thesis a few weeks ago, on the topic of general valued fields, and I noted two points:

• Robinson's (Complete theories, 1956) quantifier elimination theorem for algebraically closed valued fields involves precisely docs#ValuativeRel

image.png

• The definition given by the applicant for a discrete valuation field was the existence of a largest element of value $<1$.

[Kenny Lau]

well, but this is for fields and our definition is for rings

[Adam Topaz]

Kenny Lau said:

well, but this is for fields and our definition is for rings

See #maths > Discrete valuation @ 💬