More Definitions and Theorems of Valuations

Stream: maths

[Jiang Jiedong]

Recently I'm trying to add some valuation theory into mathlib. A short plan is doing some ramification theory of valuations, such as defining and discussing higher ramification groups.

A first step is to add more concrete definitions of valuations into mathlib. For example , I want to define the predicate describing a valuation being trivial or being discrete. I find that currently there is already some theorems talking about IsEquiv of valuations. So is it better to define these properties modulo IsEquiv or to do it in another way? From my perspective, if I want to do some number theory in the future, I will encounter concrete calculations of valuations happening in NNReal or NNRat, so I may need to use IsEquiv to convert an arbitrary value group to NNReal.

Another issue rising naturally is about using add version or mul version (v(0) = \infty or v(0) = 0) of valuation. From the aspect of linking the theory of valuations with prime ideals, an add version is more easy to use. Is it reasonable to do both mul and add theory of valuations, or is it better to just stick to mul version?

[Kevin Buzzard]

Right now we seem to have decomposition and inertia subgroups for a very general class of valuations. What's the correct generality for higher ramification groups? My guess is that the "lower numbering" could also be defined in some big generality, indexed by elements a of the valuation subring A and defined by "induces the identity on A/a".

But all of this seems to be set up with valuation subrings rather than valuations so there's another design decision to be made. For a finite extension of the p-adic numbers, for example, what would one like to be using?

To get to NNReal we probably need a general theory of rank one valuations but I don't know at what point this kicks in.

I would stick to the mul version for now. Why do we need the add version? Making the prime ideal is easy and surely is already done?

[Jiang Jiedong]

Kevin Buzzard said:

Right now we seem to have decomposition and inertia subgroups for a very general class of valuations. What's the correct generality for higher ramification groups? My guess is that the "lower numbering" could also be defined in some big generality, indexed by elements a of the valuation subring A and defined by "induces the identity on A/a".

But all of this seems to be set up with valuation subrings rather than valuations so there's another design decision to be made. For a finite extension of the p-adic numbers, for example, what would one like to be using?

A useful property concerning higher ramification group of finite extension of p-adic numbers is that lower numbering works compatibly with subgroups of the Galois group, and upper numbering works compatibly with quotients of the Galois group. The way to link upper and lower numbering of ramification group is through the piecewise-linear Herbrand function. My first impression is that it would be easier to work with if we use concrete valuations and use some real number indexed "lower numbering" and "upper numbering", at least for the Herbrand function.

[Jiang Jiedong]

Kevin Buzzard said:

Right now we seem to have decomposition and inertia subgroups for a very general class of valuations.

Currently, the decomposition and inertia subgroups is defined using only valuation subrings instead of of concrete valuations?

[Jiang Jiedong]

Maybe I am wrong, but I think most textbooks in p-adic number theory do use the language of valuations heavily due to calculation reasons. For example, concrete calculations of the valuation of differences and discriminants.

[Jiang Jiedong]

I totally agree with that there is no need to do add version of valuations. There is no real advantage in doing this. :face_with_hand_over_mouth:

[Kevin Buzzard]

Right -- decomposition and inertia subgroups are defined using valuation subrings of fields, but for a field, equivalence classes of valuations are the same thing as valuation subrings.

[Kevin Buzzard]

In other words, for a field, the preorder associated to an equiv class of valuations is determined by the things which are <= 1.

[Kevin Buzzard]

@María Inés de Frutos Fernández what do you work with when extending valuations to finite extensions? You have the issue that the value group might go up if the extension is ramified.

[Jiang Jiedong]

Yes, mathematically the valuation subring of a field is in one-to-one correspondence to its valuation equivalence class. Although I have written some codes using valuations (mostly about Ostrowski's theorem and higher ramification groups), but I think it is not hard to convert them into the language of valuation rings once this design decision is settled.

[María Inés de Frutos Fernández]

Jiang Jiedong said:

A first step is to add more concrete definitions of valuations into mathlib. For example , I want to define the predicate describing a valuation being trivial or being discrete.

@Filippo A. E. Nuccio and I have formalized a definition of discrete valuation and several results about discretely valued fields, discrete valuation rings, and relations between these; you can see what we did here (so that you don't duplicate existing work).

[María Inés de Frutos Fernández]

Kevin Buzzard said:

María Inés de Frutos Fernández what do you work with when extending valuations to finite extensions? You have the issue that the value group might go up if the extension is ramified.

In the discrete valuation case, we chose to always work with normalized valuations taking values in with_zero (multiplicative Z). So to extend a discrete valuation on a field K to a field extension L, first we compute the extension of a real-valued nonarchimedean norm corresponding to the valuation on K (using my previous work for constructing C_p), and then normalize this extension to obtain a with_zero (multiplicative Z)-valued valuation on L. Of course, we needed to be careful with types; the details of how we did this are also covered in our paper.

[Adam Topaz]

Concerning higher ramification groups: given a valuation v taking values in a LinearOrderedCommGroupWithZero $\Gamma$, we could introduce the type of "min-closed" subsets of $\Gamma$, and given such a subset S, consider the subgroup of elements $\sigma$ in the decomposition group where $v(x - \sigma(x)) \in S$ for any $x$ in the valuation ring.

[Adam Topaz]

That's the naive generalization of the higher ramification groups (in the lower numbering, as Kevin said) in the discrete case. I don't know how naive that actually is though.

[Kevin Buzzard]

I have never had any conceptual understanding of the upper numbering; I assume there is no analogue in this generality?

[Adam Topaz]

Isn't there some work of Saito about this?

[Jiang Jiedong]

I was thinking about how to formalize the upper numbering $G^u$ and linking of upper and lower numbering through Herbrand's function $\eta$.

Let $K$ be an algebraic extension of $\mathbb{Q}_p$, let $\mathcal{O}_K$ be the ring of integers. Using valuations (across the relation IsEquiv) to define the lower numbering ramification group $G_v$, for any $v$ in the value group gives us the flexibility of talking about $G_v$ when $v$ is not a valuation of any element of the ring $\mathcal{O}_K$. This is often the case when we try to define $G^u = G_{\eta (u)}$, where possibly no elements of $\mathcal{O}_K$ has valuation $\eta(u)$.

Maybe it is also possible to define a very general lower number without using concrete valuations, and deal with this problem in another way if we come up with some good idea.

[Jiang Jiedong]

Adam Topaz said:

Isn't there some work of Saito about this?

Is there any reference on this? Thank you!

[Kevin Buzzard]

Perhaps Takeshi's ICM talk https://www.ms.u-tokyo.ac.jp/~t-saito/talk/ICM.pdf is the place to start?

@Jiang Jiedong I think that before we start on this we need to wait for @María Inés de Frutos Fernández 's work on extensions of valuations to be ported to mathlib4. The base field should not be $\mathbb{Q}_p$ but should at the very least be a nonarchimedean local field, and in fact probably a complete discretely-valued field with (at some point) perfect residue field. I agree that there is a huge amount to be done here, and the questions which have come up here (whether to use valuation subrings, or NNReal-valued valuations, or valuations taking values in WithZero (multiplicative Int) ) are perhaps some of the first questions one should be asking.

My gut feeling is: don't use additive valuations unless we really have to (morally because 0 is better-behaved than $\infty$) but that perhaps it's time to set up a theory of rank 1 valuations (i.e. valuations with target NNReal), because these are also needed in the theory of Berkovich spaces. Valuations are used for so many different things but my attitude has always been that the way to make progress is just to make some decisions and push on, because otherwise nothing gets done. But definitely don't start with base field $\mathbb{Q}_p$ :-) Follow Serre's local fields book perhaps?

[Filippo A. E. Nuccio]

Following Serre's book is indeed what we are planning to do with @María Inés de Frutos Fernández in our work. In particular, we are suggesting a different definition of $\mathbb{Q}_p$ and we are proposing a general notion of local field (be it of equal or mixed characteristic) and this seems already to be a better setting for defining upper/lower ramification numbers. We hope this will be ported to mathlib reasonably soon...

[Jiang Jiedong]

Kevin Buzzard said:

Valuations are used for so many different things but my attitude has always been that the way to make progress is just to make some decisions and push on, because otherwise nothing gets done. But definitely don't start with base field $\mathbb{Q}_p$ :-) Follow Serre's local fields book perhaps?

Thank you! Then perhaps I shall do some more basic things first, and move on step by step. Such as the Ostrowski's theorem, stated as any nontrivial (non-Archimedean) valuation on $\mathbb{Q}$ is equivalent to one of the p-adic valuations? However, I need to ask this question first, should the Ostrowski's theorem be stated and proved in a more general version or it is ok for the mathlib (at least for now)?

[Jiang Jiedong]

And yes, I agree with that we need to wait for @Filippo A. E. Nuccio and @María Inés de Frutos Fernández porting their great work on Serre's local fields to Mathlib4 before we can do this higher ramification group. And I'll do some more serious investigation of their lean3 code, so that I'll be ready when the porting is done :)

[Yaël Dillies]

Ostrowski was already proved by @Billy Miao, although I'm not sure what the status is

[Filippo A. E. Nuccio]

But has Ostrowski made it into mathlib? And is it only for $\mathbb{Q}$?

[Johan Commelin]

There is also https://github.com/RaitoBezarius/berkovich-spaces, which contains Ostrowski over Q, but it needs quite some cleanup before it could enter mathlib.

[Antoine Chambert-Loir]

Kevin Buzzard said:

I have never had any conceptual understanding of the upper numbering; I assume there is no analogue in this generality?

Iirc the upper numbering is good for quotients, the lower one for subgroups. 8n any case, they differ by an increasing bijection on the reals.

[Kevin Buzzard]

Right, but why should there be any numbering which is good for quotients and why is it defined in such an ad hoc way?

[Kevin Buzzard]

The lower numbering generalises to valuations taking values in an arbitrary totally ordered monoid with zero. Does the upper numbering? Or is the rank 1 assumption essential for "behaves well for quotients"?

[Filippo A. E. Nuccio]

Kevin Buzzard said:

Right, but why should there be any numbering which is good for quotients and why is it defined in such an ad hoc way?

I am not sure to understand what you mean exactly by "why should there be any numbering which..." but one striking evidence for me that the "upper numbering" is not just a fortuitous invention that happens to work for quotients, is that in an abelian extension the reciprocity map sends $(\mathcal{O}_K^\times)^n$ (the units that are $1$ modulo $\varpi^n$) to $G^n$ (and not to $G_n$). This is Théorème 2, Chap XV, §3 in Serre's Corps Locaux. But I know nothing about rank $\geq 2$.

[Kevin Buzzard]

Right, but the reciprocity map only works for nonarch local fields so DVRs and in particular rank 1. If K is any field with a valuation taking values in some abstract monoid with 0 then the lower numbering makes sense and plays well with respect to subgroups. Is there anything which plays well with respect to quotients?

[Filippo A. E. Nuccio]

Well, unfortunately I do not have the slightest clue, I know very little about rank $\geq 2$... :sad:

[Adam Topaz]

Even if you take a 2 dimensional local field, the reciprocity map has Milnor K2 as the source, not the multiplicative group. So the analogue of the statement above for the reciprocity map must be changed in some nontrivial way.

[Adam Topaz]

IIRC it’s still possible in such cases, and was done by Kato, I think?

[Adam Topaz]

(Such cases should be any higher dimensional local field)

[Filippo A. E. Nuccio]

What I tried was Saito's Class Field theory for two-dimensional local rings (Adv Studies Pure Math 12), but it seems to me that he does not discuss the relation between reciprocity map and units vs ramification.

[Kevin Buzzard]

Reciprocity is only a thing for abelian extensions, the upper numbering works for an arbitrary Galois extension of local fields

[Filippo A. E. Nuccio]

Good point.

[Kevin Buzzard]

And another thing. Whyever does the lower numbering start at -1?? (screenshot from Wikipedia page on ramification groups)

Screenshot_20240121-151238.png

No $i$ in sight, all $i+1$.

[Adam Topaz]

Isn’t that just a reindexing so the Herbrand function has a nice definition?

[Adam Topaz]

Kevin Buzzard said:

Reciprocity is only a thing for abelian extensions, the upper numbering works for an arbitrary Galois extension of local fields

Yes, of course, but there's also an internal sort of consistency that must be satisfied in the following sense. Suppose that $L|K$ is any finite extension of (1-dimensional) local fields and $G_L^{ab} \to G_K^{ab}$ is the map induced by the inclusion $G_L \to G_K$ then on the one hand that map has to be compatible with the lower numbering (since that's the one compatible with restrictions) and on the other hand the upper numbering corresponds to the filtration on the units. So again the Herbrand function comes into play. Is it not the case that this is the unique function which is compatible in this sense?

[Kevin Buzzard]

Lower numbering doesn't make sense for infinite extensions, right? Are these absolute Galois groups? Oh but do you just want to replace with some sufficiently large finite extension or something?

[Filippo A. E. Nuccio]

Kevin Buzzard said:

And another thing. Whyever does the lower numbering start at -1?? (screenshot from Wikipedia page on ramification groups)

Screenshot_20240121-151238.png

No $i$ in sight, all $i+1$.

I have always interpreted this as a way to cope with the existence of tame inertia, so that the $G_i$'s for $i \geq 1$ account for wild inertia (that is where the juice is) and you do not want to start off at $2$.

[Adam Topaz]

Kevin Buzzard said:

Lower numbering doesn't make sense for infinite extensions, right? Are these absolute Galois groups? Oh but do you just want to replace with some sufficiently large finite extension or something?

Yes that's what I meant by "compatible with the lower numbering". to make it precise you can take any finite extension $L'|L$ which is Galois over $K$, and the map $Gal(L'|L) \to Gal(L'|K)$ is compatible with lower numbering while if $K'|K$ is the maximal subextension of $L'|K$ which is abelian over $K$ then $Gal(L'|K) \to Gal(K'|K)$ has to be compatible with the upper numbering.

[Adam Topaz]

But also as we discussed above the lower numbering should make sense even for non-finite Galois extensions because there is no longer a restriction on the valuation being discrete!

[Adam Topaz]

Filippo A. E. Nuccio said:

Kevin Buzzard said:

And another thing. Whyever does the lower numbering start at -1?? (screenshot from Wikipedia page on ramification groups)

Screenshot_20240121-151238.png

No $i$ in sight, all $i+1$.

I have always interpreted this as a way to cope with the existence of tame inertia, so that the $G_i$'s for $i \geq 1$ account for wild inertia (that is where the juice is) and you do not want to start off at $2$.

It’s also nice that in the abelian case G^i corresponds to 1+m^i

[Kevin Buzzard]

It's the normalisation of the lower numbering I'm complaining about, I agree that the upper numbering might be sensible!

[Jiang Jiedong]

Is it OK for me to add the following instances into mathlib?

1. A valuation ring is valued in a canonical way. More specifically,

import Mathlib.RingTheory.Valuation.ValuationRing
import Mathlib.RingTheory.DiscreteValuationRing.Basic
import Mathlib.Topology.Algebra.Valuation

variable [CommRing R] [IsDomain R] [ValuationRing R]
instance : Valued R (ValuationRing.ValueGroup R (FractionRing R)) := sorry

2. A preorder relation of divisibility on any valuation ring

instance : Preorder R where
 le a b := ∃ c, a * c = b
 le_refl _ := ⟨1, mul_one _⟩
 le_trans _ _ _ := fun ⟨u, h⟩ ⟨v, g⟩ => ⟨u * v, by rw [← g, ← h]; ring⟩

[Jiang Jiedong]

And an OrderTopology instance after these two instances.

[Filippo A. E. Nuccio]

The problem I see with the first point is that I am not sure that definining the "canonical" valuation to take values in the ValueGroup is the best choice. For instance, most of the library concerning Adic Valuations considers $\mathbb{Z}_{m0}$-valued ones.

[Filippo A. E. Nuccio]

One even major issue is that every field (like $\mathbb{Q}$) is a valuation ring and you may want to put different valued structures on it (like all the $p$-adic ones).

[Filippo A. E. Nuccio]

The same problem shows up in the Preorderpoint, for basically the same reason.

[Jiang Jiedong]

Filippo A. E. Nuccio said:

One even major issue is that every field (like $\mathbb{Q}$) is a valuation ring and you may want to put different valued structures on it (like all the $p$-adic ones).

Sadly, any instance for valuation ring will automatically apply to fields. Is scoped instance good enough in this case? Or should I just write definitions instead of instances.

[Filippo A. E. Nuccio]

Well, I think that the point is precisely that we do not want to declare such an instance. The idea behind the valued class is that it should really reflect a somewhat "unique" valuation (and uniformity that goes with it), whereas there are many rings with several useful valuations.

[Filippo A. E. Nuccio]

Indeed, using def is much more appropriate in this setting.