Zulip Chat Archive

Stream: maths

Topic: local fields / nonarchimedean fields


Johan Commelin (Dec 04 2019 at 09:47):

Is anyone in Amsterdam working on local fields? I would like to avoid duplicating efforts. Pinging @Rob Lewis @Casper Putz @Joey van Langen @Sander Dahmen

Johan Commelin (Dec 04 2019 at 09:48):

(If someone outside of Amsterdam is working on this kind of maths, then I would also like to know it :grinning:)

Rob Lewis (Dec 04 2019 at 09:48):

Not that I know of.

Casper Putz (Dec 04 2019 at 10:09):

Sander and me are started working on Henselian fields a while ago (did not work on it recently but we want to continue with it in January). We wanted to show extension of valuations for extensions of valued fields. There is some beginning (henselian.lean on the branch henselian_fields). We only did the minimum we needed on valuations. It's a subset of the stuff on valuations that is in the perfectoid project.

Johan Commelin (Dec 04 2019 at 10:13):

Ok, that's good to know

Casper Putz (Dec 04 2019 at 10:13):

I got a bit stuck myself when I needed field norms (specifically the constant coefficient of the minimal polynomial of an element is a power of the field norm). Got somewhere by defining characteristic polynomials but it got a bit messy. But we can maybe talk about that in January ;).

Casper Putz (Dec 04 2019 at 10:13):

What were you planning on doing on local fields?

Johan Commelin (Dec 04 2019 at 10:14):

Just basic stuff. A whole bunch of stuff done for the p-adics can be done more general. We have this file: https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/for_mathlib/padics.lean

Johan Commelin (Dec 04 2019 at 10:14):

That should mostly be generalized

Casper Putz (Dec 04 2019 at 10:15):

I agree that would be great to do more general!

Casper Putz (Dec 04 2019 at 10:17):

I would say it would be perfect if you were to port (some of) the stuff on valuations that is not in the perfectoid project to mathlib. We only did the bare minimum we needed and it can directly be replaced

Johan Commelin (Dec 04 2019 at 10:26):

Do you mean stuff that is in the perfectoid project?

Casper Putz (Dec 04 2019 at 10:34):

Yes that's what I meant, but I see that stuff is not in the for_mathlib folder. That is fine as well. You know now what we are working on so we are not doing the same stuff

Johan Commelin (Dec 04 2019 at 10:37):

I think it would be great to also PR some basic valuation stuff to mathlib

Johan Commelin (Dec 04 2019 at 10:37):

One of the big questions is whether we should also have additive valuations

Johan Commelin (Dec 04 2019 at 10:37):

Currently we only have multiplicative ones. But this means that discrete valuations with values in are not supported by our code

Kevin Buzzard (Dec 04 2019 at 22:49):

A PhD student at Imperial called Johannes Girsch is doing research into representations of p-adic groups and he and I were talking recently about formalising local fields. I was thinking of starting on the basics, and following Johan's advice of defining a discrete valuation as being a valuation-in-the-sense-of-Huber to the non-negative reals whose image is 0 plus the powers of some rho.


Last updated: Dec 20 2023 at 11:08 UTC