# Zulip Chat Archive

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

Comments are very welcome, especially if comments about the abstract come today and other comments come before October 22th...

#### 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: Aug 03 2023 at 10:10 UTC