Ostrowski theorems formalized in Lean 3

Stream: general

[Ryan Lahfa]

I'm happy (shameless plug) to announce that two versions of Ostrowski (over $\mathbb{Q}$ and over $\mathbb{K}[X])$ theorems have been formalized completely (no sorry left!) in Lean 3 (https://github.com/RaitoBezarius/berkovich-spaces for the code). :-)

Thanks to everyone for the help over all these months, I will be trying to open PRs to commit back mathlib stuff and Ostrowski theorems themselves if I can!

[Eric Rodriguez]

(btw, for your setup instructions, you can just use leanproject get RaitoBezarius:berkovich-spaces and it should deal with it for you)

[Eric Wieser]

If you wanted you could add your project to https://github.com/leanprover-contrib/leanprover-contrib so that it's linked to from the mathlib website

[Patrick Massot]

I think the title of the README is pretty misleading. You could rewrite it as "Towards Berkovich space" or "The Berkovich spaces project".

[Ryan Lahfa]

Definitely, I wrote the README quickly to go for dinner, I will redo the README properly

[Ryan Lahfa]

Ryan Lahfa said:

Definitely, I wrote the README quickly to go for dinner, I will redo the README properly

Done

[Adam Topaz]

Good job! As far as I know, Ostrowski's theorem is somewhat orthogonal to the theory of Berkovich spaces (unless you start talking about the Berkovich space of global objects over $\mathbb{Z}$).

[Ryan Lahfa]

Adam Topaz said:

Good job! As far as I know, Ostrowski's theorem is somewhat orthogonal to the theory of Berkovich spaces (unless you start talking about the Berkovich space of global objects over $\mathbb{Z}$).

Before going too deep into the abstract theory, I thought it would be interesting to develop non-trivial examples and things around the Berkovich spectrum of $\mathbb{Z}$

[Adam Topaz]

I guess my point is that Berkovich geometry over Z is not nearly as well developed as Berkovich geometry over a non archimedean field. The Berkovich spectrum of Z is a nice example (I assume here you're endowing Z with the Archimedean norm...), But a much more important example would be, for example, the Berkovich analytification of $\mathbb{A}^1$ over a nonarch. valued alg. closed field.

[Adam Topaz]

Anyway, please don't take my comment the wrong way. It's really great that you formalized Ostrowski's theorem, and it would be an excellent addition to mathlib. My main point is just that it's not necessarily a foundational result in the theory of Berkovich spaces.

In any case, it looks like there is a lot of number theory activity in lean recently, which is GREAT!

[Kevin Buzzard]

Do we have enough number theory to deduce from this result that the only valuations on a number field are the ones associated with embeddings into the complexes and primes of the ring of integers?

[Filippo A. E. Nuccio]

Related to this: at which stage are we about deciding what a valuation is?

[Patrick Massot]

mathlib already has a very general definition of a valuation

[Filippo A. E. Nuccio]

Are you speaking about this one?
https://leanprover-community.github.io/mathlib_docs/ring_theory/valuation/basic.html#valuation

[Filippo A. E. Nuccio]

Indeed, I agree it is very general and looks perfect (to me) for everything one could need for algebraic number theory. But I got the impression that @Kevin Buzzard was somewhat sceptical about the state of the art.

[Patrick Massot]

The open question is how to smoothly relate this very general notion to more elementary stuff

[Filippo A. E. Nuccio]

I see (somehow). You are working on adic valuations right now, isn't it?

[Kevin Buzzard]

I would like somebody to make a decision for me about how to put a valuation in the sense of mathlib on a discrete valuation ring in the sense of mathlib

[Kevin Buzzard]

I am not brave enough to decide whether the target monoid should be with_zero (multiplicative nat) or ...int and whether it needs to be defined as a new type or not

[Kevin Buzzard]

There was also an independent question about extending the topology on a topological ID to one on its field of fractions which was holding me up, but Maria has just solved this one

[Kevin Buzzard]

Now would be a good time to develop some of the theory of valuations in this setting. Patrick is working on the J-adic topology, Maria has solved the topology problems and we should be able to complete number fields at prime ideals and do everything we want with valuations

[Adam Topaz]

Kevin Buzzard said:

I would like somebody to make a decision for me about how to put a valuation in the sense of mathlib on a discrete valuation ring in the sense of mathlib

Just my opinion about this:

1. Define abstract valuation rings as a class, and show that discrete valuation rings are valuation rings.
2. Given any valuation ring $\mathcal{O}$, define "the canonical value group", a comm_monoid_with_zero, as $\Gamma_{\mathcal{O}} := \mathcal{O}/\mathcal{O}^\times$, and the corresponding valuation $v : \mathcal{O} \to \Gamma$ in the sense of mathlib.
3. For a discrete valuation ring, prove that $\Gamma_A$ is isomorphic to with_zero (multiplicative \N).

[Kevin Buzzard]

This looks great. And then one can develop a theory of topologies on valuation rings and maybe Tate algebras

[Adam Topaz]

I started with some code in branch#valuation_ring
I'm done for today, and I won't have much time tomorrow, but if anyone wants to build on this, please feel free.
(I'm not convinced the definition I chose for $\Gamma$ is the best option.)

[Johan Commelin]

That definition (assuming you are talking about (2) above) and the corresponding valuation $v \colon \mathcal O \to \Gamma$ are already in the perfectoid project. Not sure how much of this "canonical valuation" has made it to mathlib.

[Filippo A. E. Nuccio]

I only have one small comment: with @Adam Topaz ' definition, the valuation "group" of a DVR would not be defeq to with_zero (multuplicative \N), and I wonder if this is not a problem.

[Filippo A. E. Nuccio]

I was trying to play a bit with @Adam Topaz ' definition and I have a basic question about comm_group_with_zero: it seems to me that the "extended integers" $\mathbb{Z}\cup\{\infty\}$ are a comm_group_with_zero when declaring $\infty \cdot a=a\cdot \infty=\infty$ for every $a : \mathbb{Z}$. Then why can't we define the $p$-adic valuation as taking values here rather than in $\mathbb{Z}$ with the declaration $v(0)=0$ (as it is now in https://leanprover-community.github.io/mathlib_docs/number_theory/padics/padic_numbers.html#padic.valuation )?

[Adam Topaz]

That would break the fact that the units of the valuation are the elements with valuation zero (if you're using the additive notation for the value group).

[Yakov Pechersky]

It's not a comm_group_with_zero because what happens to 0? It doesn't have an inverse.

[Yakov Pechersky]

Unless you mean that 0 is the zero and the inverse of infty is infty

[Adam Topaz]

I think he means linear_ordered_add_comm_group_with_infinity

[Adam Topaz]

Which might not exist?

[Yakov Pechersky]

It's with_top

[Yakov Pechersky]

There's docs#linear_ordered_add_comm_monoid_with_top, docs#linear_ordered_add_comm_group_with_top

[Filippo A. E. Nuccio]

Yes, I mean a lin_ord_ab_group_with_inf, and I might have a look at that with_top instead.

[Filippo A. E. Nuccio]

Adam Topaz said:

That would break the fact that the units of the valuation are the elements with valuation zero (if you're using the additive notation for the value group).

I am sorry, but I don't understand why.

[Adam Topaz]

Because zero is not a unit?

[Adam Topaz]

Maybe I misunderstood the question?

[Filippo A. E. Nuccio]

Ok, I try to explain myself better: if we add to the additive group $\mathbb{Z}$ the element $\infty$ and we call it zero (so the one of the group is 0 : int and the zero of the group is $\infty$), don't we get a comm_group_with_zero when declaring that $\infty$ absorbs everything (additively)?

[Filippo A. E. Nuccio]

Now $\mathbb{Q}_p\rightarrow\bar{\mathbb{Z}}$ and I don't see problems with $0 : \mathbb{Q}_p$ which is the only guy sent to $\infty$.

[Adam Topaz]

Oh, but that's already what's been done... So what's the issue?

[Adam Topaz]

Just that it's not defeq to Z?

[Adam Topaz]

I'll move this thread to the maths stream where it belongs...

[Filippo A. E. Nuccio]

No, well, my "issue" is that here https://leanprover-community.github.io/mathlib_docs/number_theory/padics/padic_numbers.html#padic.valuation the p-adic valuations sends $0$ to $0$, not to $\infty$.

[Yakov Pechersky]

It's not a comm_group_with_zero because there are no multiplicative inverses. Do you mean add_comm_group...?

[Filippo A. E. Nuccio]

Ah, sure, thanks.

[Yakov Pechersky]

And there is no add_comm_group_with_* because add_comm_group already has zero, and no one has made the with_blah version for it.

[Filippo A. E. Nuccio]

Great, I see. I though the difference was just a matter of notation.