## Stream: general

### Topic: Perfectoid spaces paper

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

#### Sebastien Gouezel (Oct 16 2019 at 09:10):

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

#### 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?

#### 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)\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 (Oct 16 2019 at 19:17):

@Sebastien Gouezel @Mario Carneiro Thanks for the feedback!

#### 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 $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 (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

#### Patrick Massot (Oct 16 2019 at 20:18):

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

Last updated: Dec 20 2023 at 11:08 UTC