Valuation rings

Stream: maths

[Adam Topaz]

Hi all,

I just opened a WIP/RFC PR with the definition of a valuation ring and the construction of the associated valuation.
Comments are very welcome! There is much more to add, but this PR is already a little long...
I'm sure there is overlap with the perfectoid project, so let me ping @Johan Commelin @Kevin Buzzard and @Patrick Massot

[Adam Topaz]

#12719

[Kevin Buzzard]

Maria and I seem to want rank 1 valuations. Do you have an opinion about how they should fit into things?

[Adam Topaz]

Perhaps via Krull dimension?

[Adam Topaz]

the rank of a valuation ring (in the sense of the rank of the value group) is the Krull dimension -- I should prove that at some point...

[Eric Rodriguez]

I don't think we have Krull dimension yet

[Adam Topaz]

Oh my.... we have so much to do!

[Ruben Van de Velde]

So much fun still to be had!

[Yaël Dillies]

How does this fit into my idea of formalizing (part of) this book about spectrai spaces?

[Adam Topaz]

I don't know, @Yaël Dillies .... what do you have in mind?

[Yaël Dillies]

Hochster's result, chapter 12

[Adam Topaz]

Yeah, but what do you have in mind in connection with valuation rings?

[Yaël Dillies]

No idea! Probably my question was misguided.

[Adam Topaz]

I mean... valuation rings play an important role in algebraic geometry in various ways and the topological properties is one of them (for example by mapping spectra of valuation rings to a scheme it is possible to reconstruct the underlying topology of a scheme, see e.g. section 3 of https://arxiv.org/pdf/1906.00921.pdf ), but I don't have a clear enough picture of what you're planning to do @Yaël Dillies to say whether anything about valuation rings will be useful...

[Adam Topaz]

@Kevin Buzzard for now I added:

variables (A : Type*) [comm_ring A] [is_domain A] [discrete_valuation_ring A]

instance of_discrete_valuation_ring : valuation_ring A := ...

[Eric Wieser]

Is it me, or is your value_group almost identical to docs#projectivization?

[Kevin Buzzard]

It shouldn't be

[Eric Wieser]

At a glance both are just the quotient by (mul_action.orbit_rel Kˣ V) with various extra typeclass assumptions on K and V

[Eric Wieser]

Maybe the nonzero requirement is worth more than I'm giving it

[Kevin Buzzard]

No, you do make a fair point

[Kevin Buzzard]

I'm quite surprised Adam left the zero in the value group. I think in adic space valuation theory it's usually not there (and this is what I was thinking about; I hadn't looked at the PR), and in the adic space theory the quotient is more complex than the things of valuation 1, and it's only a monoid so you have to take the associated group.

[Adam Topaz]

Note that a valuation in the sense of mathlib takes values in a linearly_ordered_comm_monoid_with_zero.

[Adam Topaz]

So not removing the zero is necessary!

[Kevin Buzzard]

Right. But Wedhorn uses the word "value group" of v : R -> {0} union G to be the smallest subgroup H of G such that v takes values in {0} union H. It seems you're using the phrase differently (which was why I was so quick to tell Eric that they weren't the same before I looked at your code, and so quick to back down once I did )

[Adam Topaz]

I could rename the thing in my PR to value_group_with_zero if folks prefer that.

[Kevin Buzzard]

I don't know the standard language for valuation rings

[Eric Wieser]

I only ask because I wonder if this is one of these "group rings and magma algebras are the same thing"- or "semimodules and vectors spaces are the same thing"- type cases, where the construction is the same, and we're just using different words to refer to them when extra ambient typeclasses are available.

[Adam Topaz]

The terminology is all off anyway... Usually (as far as I know) a valuation on a field is a map from the units of the field to some totally ordered abelian group, and the and the ultrametric condition is v (x+y) \geq min .... We flip things around and include the zero in mathlib. I think having a zero in the value group is not the end of the world.

[Kevin Buzzard]

Oh golly, a valuation on a field isn't defined at 0?? And a valuation on a ring is :-) Eric's going to like that :-)

[Johan Commelin]

I think we did something similar in the perfectoid project: https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/valuation/canonical.lean#L85L111
I'm glad to see that all this can now be golfed into 1 line with current mathlib.

[Antoine Chambert-Loir]

It's a good thing to authorize 0 in the “value group”, it simplifies the definition, — and, while you're here, you could define “semivaluations on a ring” which may take 0 on something else than 0. Berkovich spaces are defined by spaces of seminorms and semivaluations are more flexible, a semivaluation passes to the quotient by the prime ideal on which it vanishes, etc.

[Antoine Chambert-Loir]

In fact, “general” valuations could take their value in any “ordered monoid with bot“.

[Antoine Chambert-Loir]

There is also the (convention) issue of the ordering: if $a | b$, is $v(a) \leq v(b)$ or $v(b)\leq v(a)$$.
The traditional convention is the former, but people (like Huber) use the first one, which makes a valuation more like the $p$-adic norm.

[Kevin Buzzard]

docs#valuation

[Kevin Buzzard]

Antoine we have the multiplicative version, taking values in an ordered commutative monoid with 0 (and which may take 0 on inputs other than 0) (and we use Huber's convention)

[Adam Topaz]

Johan Commelin said:

I think we did something similar in the perfectoid project: https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/valuation/canonical.lean#L85L111
I'm glad to see that all this can now be golfed into 1 line with current mathlib.

Yes, this setoid is essentially the same.

Maybe I should explain what's happening in my PR a little better:

First, suppose that $A$ is an integral domain.
We say that $A$ is a valuation ring provided that for all $a,b \in A$, there exists some $c \in A$ such that $c \cdot a = b$ or $c \cdot b = a$. This is equivalent to saying that when we consider $A$ as a subring of its fraction field, say $K$, that for every element $x \in K$, either $x \in A$ or $x^{-1} \in A$. In other words, this agrees with the usual notion of a valuation ring, except there is no need to refer to "the" fraction field.

Now comes some lean/mathlib technicalities. Given a valuation ring $A$, an $A$-algebra $K$ which happens to be a field, and an instance of is_fraction_ring A K (so K is a fraction field of A), this PR constructs value_group A K as the quotient of K by the multiplicative action of the units of A (this is essentially the same setoid from the perfectoid project that Johan linked above). In this PR, I do not assume that there is some valuation given ahead of time (unlike what's done in the perfectoid project), so we need to define a linear_ordered_comm_group_with_zero structure on value_group A K using only the axioms of A and K. This takes up the most work in the PR. The quotient map from K to value_group A K then becomes a valuation in the sense of docs#valuation whose ring of integers ( docs#valuation.integer ) agrees with the original A.

[Adam Topaz]

In a followup PR, I will define valuation_subring K, the type of valuation subrings of a field K. These are subrings $\mathcal{O}$ satisfying the condition that for all $x \in K$, either $x \in \mathcal{O}$ or $x^{-1} \in \mathcal{O}$. Of course, these are all valuation rings in the above sense, and the argument above shows that any valuation ring comes from a valuation on the field $K$. Even better, two valuations on a field $K$ are equivalent if and only if their associated valuation rings are equal in valuation_subring K. For a general ring $A$, two valuations are equivalent if their support (a prime ideal) is the same, and the induced valuation subring of the residue field of the prime is the same.

[Adam Topaz]

Here is a start to that followup PR: #12741