Perfectoid spaces paper

Stream: general

[Patrick Massot]

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...

[Sebastien Gouezel]

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

[Sebastien Gouezel]

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?

[Mario Carneiro]

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)\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)

[Johan Commelin]

@Sebastien Gouezel @Mario Carneiro Thanks for the feedback!

[Patrick Massot]

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 $G$. The second one comes from the topological group structure built on $\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!

[Jesse Michael Han]

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

[Patrick Massot]

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