Zulip Chat Archive

Stream: maths

Topic: Hensel's lemma

Johan Commelin (Sep 11 2018 at 17:40):

@Rob Lewis has PR'd Hensel's lemma for the p-adics! :tada: :octopus: :muscle:
https://github.com/leanprover/mathlib/pull/337/files?w=1

Johan Commelin (Sep 11 2018 at 17:41):

Rob, would you mind sharing a bit of your long term plans? It seems like you project and the perfectoid project could strengthen each other.

Johan Commelin (Sep 11 2018 at 17:42):

I'm really excited to see all this stuff materialising.

Kevin Buzzard (Sep 11 2018 at 17:44):

In terms of what is needed to do modern mathematics I guess one has to plough through Serre's book on local fields

Rob Lewis (Sep 11 2018 at 18:25):

There's not so much of a long term plan right now. I've just been talking to Sander Dahmen about what we'll need to start formalizing his work, like we promised in the Lean Forward project. This seemed like a good place to start.

Johan Commelin (Sep 11 2018 at 18:25):

It definitely is.

Rob Lewis (Sep 11 2018 at 18:26):

Short term, I want to see what I can do about cleaning up some of the annoying inequality proofs in that PR.

Johan Commelin (Sep 11 2018 at 18:26):

I am not intimately familiar with Sanders work, but I do worry a tiny little bit that in the near future you might need to do a lot of this again for completions of number fields.

Rob Lewis (Sep 11 2018 at 18:26):

I'm sure there's plenty of overlap between Lean Forward and the perfectoid project, maybe we could get everyone together and chat sometime.

Johan Commelin (Sep 11 2018 at 18:27):

I think starting from a slightly more general perspective might pay off in the long run.

Johan Commelin (Sep 11 2018 at 18:27):

Let me put it like this: I would be very surprised if the only local rings in Sanders work are p-adics. I would expect to also find finite extensions of those.

Johan Commelin (Sep 11 2018 at 18:28):

And usually the proofs are almost the same difficulty.

Johan Commelin (Sep 11 2018 at 18:28):

This is absolutely not meant as criticism.

Patrick Massot (Sep 11 2018 at 20:12):

Short term, I want to see what I can do about cleaning up some of the annoying inequality proofs in that PR.

Did you have a look at Simon's mono tactic? It's not yet merged but it's in the nursery

Patrick Massot (Sep 11 2018 at 20:16):

@Rob Lewis would you mind documenting your p-adic work somewhere in https://github.com/leanprover/mathlib/tree/master/docs/theories?

Johan Commelin (Sep 12 2018 at 09:09):

@Rob Lewis Thanks for the documentation!

Last updated: Dec 20 2023 at 11:08 UTC