Zulip Chat Archive

Stream: general

Topic: Perfectoid spaces paper


view this post on Zulip Patrick Massot (Oct 16 2019 at 08:10):

Kevin, Johan and I have written a paper on our perfectoid space formalization experiment: perfectoid-spaces.pdf
Comments are very welcome, especially if comments about the abstract come today and other comments come before October 22th...

view this post on Zulip Sebastien Gouezel (Oct 16 2019 at 09:10):

In Theorem 4.2, f should be a function on A.

view this post on Zulip Sebastien Gouezel (Oct 16 2019 at 09:24):

I am confused by the sentence we now have two different uniform structures onˆG. The first one comes from the completion functor composed with the forgetful functor from uniform spaces to topological spaces on Line 600. Do you mean two different topologies?

view this post on Zulip Mario Carneiro (Oct 16 2019 at 09:36):

In the introduction to the uniform space section, it might help to define briefly the uniformity corresponding to a metric space (that is, "U is generated by sets of the form {(x,y)d(x,y)<ϵ}\{(x,y)\mid d(x,y)<\epsilon\}") so that it is clearer what the connection is to make sense of "The other conditions are analogous to the symmetry and triangle inequality conditions" (EDIT: I see this is mentioned later, but it is useful in the motivation part)

view this post on Zulip Johan Commelin (Oct 16 2019 at 19:17):

@Sebastien Gouezel @Mario Carneiro Thanks for the feedback!

view this post on Zulip Patrick Massot (Oct 16 2019 at 19:55):

I am confused by the sentence we now have two different uniform structures onˆG. The first one comes from the completion functor composed with the forgetful functor from uniform spaces to topological spaces on Line 600. Do you mean two different topologies?

I know what I wanted to write here, but I have no idea why I wrote that. I wanted to say: "The first one comes from the completion functor applied to the uniform structure coming from the topological group structure on GG. The second one comes from the topological group structure built on G^\hat G". Probably I started trying to reformulate it in terms of functors, got interrupted, and finished the sentence without reading the beginning. Thanks anyway!

view this post on Zulip Jesse Michael Han (Oct 16 2019 at 20:15):

We feel that, since a proof assistant can handle the definition of a perfectoid space, then they should be able to handle a general modern mathematical definition

i would change this to, "...they should be able to handle general modern mathematical definitions", which is slightly less tautological than the singular

view this post on Zulip Patrick Massot (Oct 16 2019 at 20:18):

Good point. It help to have comments from logicians :wink:


Last updated: May 14 2021 at 22:15 UTC