valuation associated to a prime ideal

Stream: Is there code for X?

[Kevin Buzzard]

If $R$ is a Dedekind domain with field of fractions $K$, then given a maximal ideal $P$ of $R$ there's a corresponding valuation subring of $K$ consisting of the elements of the form $a/b$ with $a,b\in R$ and $b\not\in P$. Is this ValuationSubring K in mathlib?

I ask because it seems that we have decomposition and inertia subgroups defined in terms of valuation subrings, but I want to talk about Frobenius elements associated to prime ideals so I need the bridge.

The difficulty I found when just trying to knock this off myself is proving mem_or_inv_mem, i.e. that if $k\in K$ can't be written as $a/b$ with $a,b\in R$ and $b\not\in P$, then $k^{-1}$ can be. This is specific to the 1-dimensional situation (e.g. it fails for $R=\mathbb{C}[X,Y]$, $P=(X,Y)$ and $k=X/Y$).

[Michael Stoll]

What is the paper proof?
You'll have to show that there are $c, d$ such that $ad = bc$ and $c \notin P$.

[Junyan Xu]

We do have docs#IsLocalization.AtPrime.discreteValuationRing_of_dedekind_domain

[Kevin Buzzard]

The paper proof is "it's in all the books, and I definitely knew it 20 years ago, but have forgotten it now".

[Kevin Buzzard]

Probably Junyan's observation reduces it to "if R is a DVR then it's a valuation subring of its field of fractions" which again is something that I remember seeing go past me and checking 20 years ago.

[Michael Stoll]

Well, every nonzero element in the field of fractions is a unit times an integral power of a uniformizer, so this should be easy (assuming the relevant facts are available, which I didn't check).

[Kevin Buzzard]

I think I put this statement in for natural powers and elements of the ring myself :-) So probably I can muddle home from here. Thanks! I'll come back if I'm still stuck.

[Junyan Xu]

There is a small amount of docs#Localization.subalgebra.ofField APIs developed by @Adam Topaz and it's imported by the file defining ValuationSubring, but they're apparently not used in the file. Maybe more stuff exists in his repo :)

[Adam Topaz]

I think we have somewhere that any valuation ring can be viewed as a valuation subring of some field which has an instance of being the fraction field... but I can't find it right now.

[Adam Topaz]

Oh we have docs#Valuation.valuationSubring and docs#ValuationRing.valuation

[Adam Topaz]

Kevin Buzzard said:

The paper proof is "it's in all the books, and I definitely knew it 20 years ago, but have forgotten it now".

The "conceptual" proof is that the localization of a normal ring is normal, and in codimension 1 being normal is the same as being regular, so the localization of a Dedekind domain at a nonzero prime is a regular local ring of dimension 1, and all such are DVRs. (I guess Noetherianity is required for all these assertions). Do we have all these ingredients in mathlib?

[Kevin Buzzard]

My instant response to that is "we have no concept of dimension in commutative algebra in mathlib as far as I know, but my PhD students Jujian and Fangming/John are working hard on it"