Zulip Chat Archive

Stream: maths

Topic: Hensel's lemma


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 11 2018 at 17:42):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 11 2018 at 18:25):

It definitely is.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 11 2018 at 18:27):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 11 2018 at 18:28):

And usually the proofs are almost the same difficulty.

view this post on Zulip Johan Commelin (Sep 11 2018 at 18:28):

This is absolutely not meant as criticism.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Sep 12 2018 at 09:09):

@Rob Lewis Thanks for the documentation!


Last updated: May 09 2021 at 09:11 UTC