local fields / nonarchimedean fields

Stream: maths

[Johan Commelin]

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]

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

[Rob Lewis]

Not that I know of.

[Casper Putz]

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]

Ok, that's good to know

[Casper Putz]

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]

What were you planning on doing on local fields?

[Johan Commelin]

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]

That should mostly be generalized

[Casper Putz]

I agree that would be great to do more general!

[Casper Putz]

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]

Do you mean stuff that is in the perfectoid project?

[Casper Putz]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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.