Stream: Is there code for X?

Topic: valuation rings

Adam Topaz (Dec 29 2019 at 20:51):

Is there code somewhere for valuation rings? A valuation ring (of a field $F$) is a subring $R$ of a field $F$ satisfying the following property: for all $x \in F$, one has $x \in R$ or $x^{-1} \in R$. I know valuations exists in the perfectoid repo, defined as a map to a totally ordered abelian group, but I couldn't find anything about valuation rings there.

I'm looking for something along the lines of:

class valuation_ring (R : Type*) extends integral_domain R :=
( val_cond : ∀ { x y : R }, ∃ z : R, x * z = y ∨ x = y * z )


Johan Commelin (Dec 30 2019 at 06:03):

@Adam Topaz We have the valuation ring of an arbitrary valuation. But not the definition that you have in mind. Of course every valuation ring à la your definition is provably also the valuation ring à la perfectoid repo. But this equivalence is not proven there.

Adam Topaz (Dec 30 2019 at 09:15):

Thanks! I see your definition now in the valuation/localization.lean file.

Last updated: May 16 2021 at 05:21 UTC