Zulip Chat Archive

Stream: maths

Topic: local fields


view this post on Zulip Kevin Buzzard (Nov 14 2019 at 19:16):

I'm staring at Serre's "Local Fields" and am wondering if I can persuade some MSc or PhD students here to formalise bits of it. But it would be nice to start them off with a definition. We have all of these facts about norms in the perfectoid project. But the key definition right at the start of Serre's book is v:KZ{}.v : K \to \mathbb{Z}\cup\{\infty\}. Do you think it's wise to bite the bullet and just formalise things like this? It's additive not multiplicative notation, and there's infinity. @Johan Commelin do you have an opinion?

view this post on Zulip Johan Commelin (Nov 14 2019 at 19:20):

Translating Serre to multiplicative notation on the fly should be trivial. A good mathematician wouldn't even see the difference. It would allow reusing 1500 lines of code from the perfectoid project (-;

view this post on Zulip Johan Commelin (Nov 14 2019 at 19:32):

Note that with #1687 we now have no excuse anymore to not work on local fields (-;

view this post on Zulip Kevin Buzzard (Nov 14 2019 at 19:41):

Hmm. But we don't have to_multiplicative :-/

view this post on Zulip Kevin Buzzard (Nov 14 2019 at 19:41):

Which monoid should I use?

view this post on Zulip Sebastien Gouezel (Nov 14 2019 at 19:45):

Note that with #1687 we now have no excuse anymore to not work on local fields (-;

Wait a second, this PR is only done aiming at partitions of unity on manifolds modelled on finite-dimensional real vector spaces. You don't have the right to use it for local fields! :)

view this post on Zulip Johan Commelin (Nov 14 2019 at 19:48):

@Sebastien Gouezel Too bad... you should have used a different license.

view this post on Zulip Johan Commelin (Nov 14 2019 at 19:49):

@Kevin Buzzard I guess the monoid with_zero (multiplicative int). But maybe just using nnreal is even better. And then add a is_discrete predicate on top of it.


Last updated: May 14 2021 at 19:21 UTC