Discrete valuation ring and fraction fields

Stream: mathlib4

[Christian Merten]

If my setup is the following: I have a DVR $R$ and its fraction field $K$ and for convenience I want to consider $R$ as a subring of $K$. What is the canonical lean setup? I think it could either be

• 1:

import Mathlib

variable {K : Type*} [Field K]
variable {R : Subring K} [DiscreteValuationRing R] [IsFractionRing R K]

with valuation ValuationRing.valuation R K.

• 2:

import Mathlib

variable {K : Type*} [Field K]
variable {R : ValuationSubring K} [DiscreteValuationRing R]

with valuation ValuationSubring.valuation. This setup comes with more api, e.g. docs#ValuationSubring.valuation_eq_one_iff exists.

• 3:

import Mathlib

variable {K : Type*} [Field K] {Γ : Type*} [LinearOrderedCommGroupWithZero Γ]
  (v : Valuation K Γ) [DiscreteValuationRing v.valuationSubring]

In this setup R is v.valuationSubring.

• Of course one could also imagine a more flexible and unbundled approach:

import Mathlib

variable {K : Type*} [Field K] {Γ : Type*} [LinearOrderedCommGroupWithZero Γ]
  (v : Valuation K Γ)
variable (R : Subring K) [DiscreteValuationRing R]

plus some compatibility condition on v and R. Probably

def IsValuationSubring : Prop := ∀ x : K, x ∈ R ↔ v x ≤ 1

And of course I can only have Algebra R K instead of having R as a Subring, but this seems to be annoying.

[Andrew Yang]

What do you plan to do? I think we prefer Algebra R K unless absolutely necessary.

[Christian Merten]

I am for example working with matrices in K which sometimes (or only partly) have coefficients in R. Here stating everything in terms of the image of algebraMap R K gets annoying, but maybe one can get around it by working with the v x ≤ 1 condition instead.

[Christian Merten]

With the Algebra R K approach, we would probably need something like IsValuationAlgebra R K similar to IsValuationSubring above.

[Andrew Yang]

Isn't IsValuationAlgebra R K <-> IsFractionRing R K and ValuationRing R? Do we need a separate class?

[Andrew Yang]

Or there is also docs#Valuation.Integers

[Christian Merten]

Andrew Yang said:

Or there is also docs#Valuation.Integers

Ah that is essentially what I had in mind with IsValuationAlgebra R K.

[Christian Merten]

I am afraid though that all of this algebraMap R K business complicates things unneccesarily? Although, since the trend seems to be to promote sub-things to types, maybe we are forced on the Algebra R K route anyway?

[Filippo A. E. Nuccio]

I think that much depends if you're rather focusing on K and you want to build up R out of it, or on R and want sometimes to look at its fraction field. In our paper with @María Inés de Frutos Fernández we opt for something in between 2 and 3

[Filippo A. E. Nuccio]

Point 1 has all the disadvantages of working with subrings, and no access to the valuation subring API.

[Filippo A. E. Nuccio]

For 3, you might want to benefit from our work (the PR's are in progress) where we define a Prop-valued IsDiscrete for a valuation, and we prove that under this assumption on the valuation, [DiscreteValuationRing v.valuationSubring] is automatic.

[Filippo A. E. Nuccio]

The repository is available here.

[Judith Ludwig]

Thank you for the comments.
@Christian Merten and I are working on formalizing the Bruhat-Tits tree, so I guess we are starting with K. But it is the interplay between R and K that makes the story interesting.

[Filippo A. E. Nuccio]

Yes, as usual :smile: At any rate, feel free to reach out to us so the we can align all design choices.

[Filippo A. E. Nuccio]

At any rate, I would urge you to take into account the class IsDiscrete for a valuation:
https://github.com/mariainesdff/LocalClassFieldTheory/blob/8258a25fa8c4b31bf85e49f04e6cb1a37f2f6547/LocalClassFieldTheory/DiscreteValuationRing/Basic.lean#L131
(which is nothing more than asking that the valuation is $\mathbb{Z}$-valued and is surjective), because most of the algebraic properties then follow from it.

[Filippo A. E. Nuccio]

"follow" in the sense that they have been formalized...

[Adam Topaz]

We also have docs#ValuationSubring but that’s mostly useful if you want to consider multiple valuations on the same field.

[Filippo A. E. Nuccio]

True, although we've used a good deal of your work on that file in our project to show that two valuations actually coincide :smile:

[Adam Topaz]

Concerning the original question (now that I read all of Christian's various options) I think going with either a valuation v (probably via the docs#Valued class) or with a valuation subring would be the smoothest.

[Christian Merten]

Adam Topaz said:

Concerning the original question (now that I read all of Christian's various options) I think going with either a valuation v (probably via the docs#Valued class) or with a valuation subring would be the smoothest.

So you are saying that going the Subring route is okay?

[Filippo A. E. Nuccio]

Well, ValuationSubring extends Subring, and has a reacher API, so I do not really see the advantage of forgetting this.

[Christian Merten]

Filippo A. E. Nuccio said:

Well, ValuationSubring extends Subring, and has a reacher API, so I do not really see the advantage of forgetting this.

Yes yes, sorry for being unclear. By going the Subring route I meant not working in the general Algebra R K setup.

[Filippo A. E. Nuccio]

Ah, I see. The main difference is that if you "start" with R, the way you produce elements in K is via the Algebra R K setup (that can sometimes be quite smooth, but it is always under the rug in one way or another). If you plan to start with K, then working with ValuationSubring (or Subring) is perfectly fine. Now, "starting with R" vs "starting with K" is not very well-defined mathematically, since we normally consider the whole gadget at the same time and move freely back and forth. So it is a bit a matter of realizing whether you expect that your "primary input" is K or R.

[Christian Merten]

Filippo A. E. Nuccio said:

At any rate, I would urge you to take into account the class IsDiscrete for a valuation:
https://github.com/mariainesdff/LocalClassFieldTheory/blob/8258a25fa8c4b31bf85e49f04e6cb1a37f2f6547/LocalClassFieldTheory/DiscreteValuationRing/Basic.lean#L131
(which is nothing more than asking that the valuation is $\mathbb{Z}$-valued and is surjective), because most of the algebraic properties then follow from it.

Thanks for the pointer! Is restricting to $\mathbb{Z}$-valued valuations necessary? I see that you define a structure Uniformizer, up to now I found working simply with an element ϖ : R with a Irreducible ϖ assumption convenient.

[Filippo A. E. Nuccio]

Well, the problem is that if you want to start relating the valuation of x to the power of the maximal ideal containing x and the valuation of varpi is not 1 you're in bad shape.

[Filippo A. E. Nuccio]

We address this in the paper, especially in section 2.3

[Filippo A. E. Nuccio]

We also provide some explanation about our choice of sticking with $\mathbb{Z}_{m0}$.

[Christian Merten]

Filippo A. E. Nuccio said:

We address this in the paper, especially in section 2.3

Thanks, I'll check that.

[Filippo A. E. Nuccio]

Don't hesitate to ask - and to suggest improvements, of course :smile: