Zulip Chat Archive

Stream: maths

Topic: Perfectoid spaces


view this post on Zulip Kevin Buzzard (May 30 2018 at 13:22):

Ok so here is the perfectoid spaces thread. As many people here know, I've long been mulling over the idea of formalising the notion of a perfectoid space in Lean. To the CS people -- it's just some structure, like a group, just a few more axioms and things.

view this post on Zulip Kevin Buzzard (May 30 2018 at 13:22):

The problem is that I'm a mathematician and I'm not very good at building structures in Lean yet because I haven't practiced enough yet.

view this post on Zulip Kevin Buzzard (May 30 2018 at 13:23):

So here's the plan.

view this post on Zulip Kevin Buzzard (May 30 2018 at 13:23):

I'm going to make a public github repo called lean-perfectoid-spaces

view this post on Zulip Kevin Buzzard (May 30 2018 at 13:23):

and then we develop what we need in there.

view this post on Zulip Kevin Buzzard (May 30 2018 at 13:24):

What are the main ingredients? I'll explain these things in an issue.

view this post on Zulip Kevin Buzzard (May 30 2018 at 13:24):

But in short, we need adic spaces

view this post on Zulip Kevin Buzzard (May 30 2018 at 13:24):

so we need presheaves and sheaves of topological rings

view this post on Zulip Kevin Buzzard (May 30 2018 at 13:24):

and we need affinoid adic spaces

view this post on Zulip Kevin Buzzard (May 30 2018 at 13:24):

so we need the notion of a valuation on a ring

view this post on Zulip Kevin Buzzard (May 30 2018 at 13:25):

Now here's a dumb thing that everyone knew already but only dawned on me recently.

view this post on Zulip Kevin Buzzard (May 30 2018 at 13:26):

There are two ways to make a perfectoid space -- a "top down" way, where you define a perfectoid space to be an adic space with some property and define an adic space afterwards -- you sorry your way from the top and attempt to connect to the bottom.

view this post on Zulip Kevin Buzzard (May 30 2018 at 13:26):

Or there's a "bottom up" way, where you think "we'll definitely need adic spaces so we'll need affinoid adic spaces so we'll need valuations so we'll need a way of turning a totally ordered group into a totally ordered monoid by adding a bottom element and I think we have that, or we nearly have that anyway, so let's start with that and then build up"

view this post on Zulip Kevin Buzzard (May 30 2018 at 13:27):

With schemes I read the stacks project from front to back and I made the definition from the bottom up.

view this post on Zulip Kevin Buzzard (May 30 2018 at 13:27):

Are there advantages in working from the top down?

view this post on Zulip Kevin Buzzard (May 30 2018 at 13:28):

Next, who should be allowed to push? Is it sensible to start with just me and force other people to learn about PRs and so on?

view this post on Zulip Kevin Buzzard (May 30 2018 at 13:29):

As a git newbie I found it far easier to just give Kenny full access to the stacks project repo

view this post on Zulip Kevin Buzzard (May 30 2018 at 13:29):

but the result of this was that one day I realised there were a bunch of files in my project which I had no idea what they did

view this post on Zulip Kevin Buzzard (May 30 2018 at 13:29):

and then when Lean upgraded and they all broke and Kenny was revising for exams I was sort-of stuck.

view this post on Zulip Kevin Buzzard (May 30 2018 at 13:30):

Should I concentrate on making sure I understand every line of code in the project, or should this be something which I should be happy to delegate?

view this post on Zulip Kevin Buzzard (May 30 2018 at 13:30):

Those are my initial thoughts. I've been really busy recently with marking issues but now these things are over and I hope to find some time to put into this.

view this post on Zulip Assia Mahboubi (May 30 2018 at 13:39):

I think that you should be able to understand every line of code in the project, but it does not mean than you cannot delegate and grant push access to others. Just that you should be ready to revert commits, ask for freezing etc. This is how the Feit Thompson proof was written, with many people having commit rights (it was not even a git repo).

view this post on Zulip Assia Mahboubi (May 30 2018 at 13:46):

I have never seen anything serious being done top down. I have been working for some time with some axiomatic algebraic numbers, waiting form the completion of the closure construction, and even for such a simple thing, one of the axioms was wrong (I don't remember the details) . So I find it scary because it is usually hard to get definitions right at the first stab. And the one you're aiming at is a truly complex one. But may be you could try to build the bridge simultaneously from the two ends, and hope for the best. One really useful thing is to write down the complete roadmap somewhere, as precise as possible. But this is what will go in your issue right? Are there components that can be done in parallel?

view this post on Zulip Kevin Buzzard (May 30 2018 at 14:02):

I love this place.

view this post on Zulip Kevin Buzzard (May 30 2018 at 14:02):

Assia -- many thanks for your very quick and extremely helpful response.

view this post on Zulip Kevin Buzzard (May 30 2018 at 14:03):

I will begin, hopefully before the weekend, by creating a repo and writing an extended issue explaining as much as I know about what needs to be done.

view this post on Zulip Kevin Buzzard (May 30 2018 at 14:03):

There should be several things which can be done in parallel.

view this post on Zulip Kevin Buzzard (May 30 2018 at 14:04):

I remember now -- when I talked about making something else I wanted in mathlib, Mario suggested that I wrote as detailed an explanation as possible and made it an issue.

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:06):

I'm at the London Number Theory Seminar and it's being given by Matthew Morrow, co-author of several papers with Scholze and perfectoid expert! I just asked him what the definition of a perfectoid space was and I'm glad I did -- he said that he definition has gone through several iterations but he was now happy with it, and gave me a precise reference -- Scholze's paper "etale cohomology of diamonds".

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:06):

https://arxiv.org/abs/1709.07343

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:06):

That is the definition we will be formalizing.

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:07):

The paper is under 9 months old. To the CS people -- the reason that defining a random structure is interesting to mathematicians is that this is a cutting-edge structure.

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:09):

It is definition 3.19 on page 18 of (v1 of) the paper at the above link

view this post on Zulip Patrick Massot (May 30 2018 at 15:10):

It's funny Scholze refers to Fontaine's Bourbaki talk about Scholze

view this post on Zulip Patrick Massot (May 30 2018 at 15:10):

Maybe this theory is actually circular

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:15):

:-)

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:15):

Fontaine only defines perfectoid rings

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:16):

Technical interlude: in Scholze's original paper he only defined a perfectoid space over a field; Fontaine was the first person to make the definition live independently without being bound to an underlying field

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:16):

OK so here's a theorem in maths:

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:17):

Zpcycl[[T1/p]](p/T)1/p[1/T]\mathbb{Z}_p^{cycl}[[T^{1/p^\infty}]]\langle(p/T)^{1/p^\infty}\rangle[1/T] is a perfectoid ring

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:17):

You show that to any number theorist in the area and they'll know what that notation means

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:17):

Can we use it in Lean?

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:18):

We refer to the pointy brackets as "langle/rangle"

view this post on Zulip Patrick Massot (May 30 2018 at 15:18):

Definitely looks like the kind of sequences of symbols that show up in talks about perfectoid stuff

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:18):

because LaTeX

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:18):

Nobody is raising a prime number to the power infinity

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:19):

this is a limit of rings where the infinity is replaced by n

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:19):

and then n goes to infinity

view this post on Zulip Mario Carneiro (May 30 2018 at 15:19):

That's not the major concern. Of course all those things are schematic

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:19):

If this stuff were written out in full the definition would double in length and would involve two and possibly more limits

view this post on Zulip Mario Carneiro (May 30 2018 at 15:19):

How many ring construction mechanisms are nested there?

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:20):

I think three or four

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:20):

depending on whether it's a theorem that something commutes with something

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:20):

I don't think these things commute

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:20):

I think maybe four

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:20):

oh

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:20):

maybe far more

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:21):

it depends on what you mean

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:21):

Zpcycl\mathbb{Z}_p^{cycl}

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:21):

is a ring

view this post on Zulip Mario Carneiro (May 30 2018 at 15:21):

In lean syntax with constants, no notation, what would it look like roughly?

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:21):

So am I allowed to make the ring Z_p^cycl?

view this post on Zulip Mario Carneiro (May 30 2018 at 15:21):

yes

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:21):

I mean I can call it X?

view this post on Zulip Mario Carneiro (May 30 2018 at 15:21):

that's like Z_cycl p I guess

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:21):

no

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:22):

it's much worse

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:22):

maybe it's about as bad

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:22):

there is an issue with completions

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:22):

everything has to be complete at every stage

view this post on Zulip Mario Carneiro (May 30 2018 at 15:22):

so completion (Z_cycl p)?

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:22):

Let me define, for A an abelian group, P A to be the projective limit of A/pnAA/p^nA

view this post on Zulip Mario Carneiro (May 30 2018 at 15:23):

where's p?

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:23):

it's a constant

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:23):

we fix a prime p on line 1

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:23):

It never changes

view this post on Zulip Mario Carneiro (May 30 2018 at 15:23):

yeah okay, parameters

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:23):

there is no relation between the different p-adic theories for different primes p

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:24):

So Zpcycl\mathbf{Z}_p^{cycl} is:

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:24):

Zp\mathbf{Z}_p is the p-adic integers

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:24):

Zp[ζpn]\mathbf{Z}_p[\zeta_{p^n}] is the extension of that ring obtained by adjoining a primitive $$p^n$$th root of unity

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:25):

Zp[ζp]\mathbf{Z}_p[\zeta_{p^\infty}] is the direct limit of those things

view this post on Zulip Mario Carneiro (May 30 2018 at 15:25):

But Z_cycl_p is one thing after all that construction

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:25):

and Zpcycl\mathbf{Z}_p^{cycl} is P of that

view this post on Zulip Mario Carneiro (May 30 2018 at 15:25):

As in, the notation is not decomposable

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:25):

it depends only on p

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:26):

it's not p of Z^cycl or ^cycl of Z_p, really

view this post on Zulip Mario Carneiro (May 30 2018 at 15:26):

right

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:26):

We build from left to right

view this post on Zulip Mario Carneiro (May 30 2018 at 15:26):

So with that in mind, how many decomposable parts are there in the ring you mentioned at the top?

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:26):

If AA is a ring

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:27):

then A[[T1/pn]]A[[T^{1/p^n}]] is formal power series in T1/pnT^{1/p^n} with coefficients in AA

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:27):

and A[[T1/p]]A[[T^{1/p^\infty}]] is P of the direct limit of these things

view this post on Zulip Mario Carneiro (May 30 2018 at 15:27):

So that's just A[[X]] with some quotient?

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:27):

no quotient involved

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:27):

TT is a variable with no relations

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:28):

Each ring is isomorphic to A[[X]]

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:28):

the mentioning of the powers of p is just to show how to take the union

view this post on Zulip Mario Carneiro (May 30 2018 at 15:28):

what makes T1/pnT^{1/p^n} different from X

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:28):

the maps between the various rings

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:28):

$$T^{1/p^{n+1}}^p=T^{1/p^n}$$

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:29):

For fixed n all those rings are isomorphic

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:29):

but if you want to call them all X

view this post on Zulip Mario Carneiro (May 30 2018 at 15:29):

So the notation here is p_infty_completion A p

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:29):

then the maps all send X to X^p

view this post on Zulip Mario Carneiro (May 30 2018 at 15:29):

where there are only two arguments A and p

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:29):

yes

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:30):

that's what A[[T^{1/p^infty}]] means

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:30):

depends only on A and p

view this post on Zulip Mario Carneiro (May 30 2018 at 15:30):

This is my question

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:30):

Depends only on the ring A and the prime number p

view this post on Zulip Mario Carneiro (May 30 2018 at 15:30):

for each of those notations, what are the dependencies and atomic bits

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:30):

OK so I will say less about what you're not interested in for the pointy brackets

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:30):

I now understand the game we're playing

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:31):

If A is a topological ring

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:31):

and p is a prime number

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:31):

then I can build A(p/T)1/pA\langle(p/T)^{1/p^\infty}\rangle

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:32):

Remark: Zpcycl\mathbb{Z}_p^{cycl} has a topology

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:32):

and we need this topology to build a topology on Zpcycl[[T1/p]]\mathbf{Z}_p^{cycl}[[T^{1/p^\infty}]]

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:32):

Finally [1/T] is a localization

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:33):

if A is a ring and T is in A then A[1/T] is a localization of A

view this post on Zulip Mario Carneiro (May 30 2018 at 15:33):

I assume that the big expression is meant to be suggestive of the interpretation of the maps in the limit, but are there other expressions that could go there?

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:33):

It is "standard notation"

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:33):

this is really interesting

view this post on Zulip Mario Carneiro (May 30 2018 at 15:33):

like does A(pT)p2A\langle(pT)^{p^\infty-2}\rangle make any sense?

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:33):

no!

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:33):

Are you crazy?

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:34):

what kind of nonsense is that?

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:34):

So what is the question? :-/

view this post on Zulip Mario Carneiro (May 30 2018 at 15:35):

if there's only one thing that the expression can be, it seems like a waste of notation :P

view this post on Zulip Mario Carneiro (May 30 2018 at 15:35):

but sure, if you want that exact thing only then you can get a reasonable approximation in lean

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:35):

A[[X1/p]](p3/X)1/p[p/X]A[[X^{1/p^\infty}]]\langle (p^3/X)^{1/p^\infty}\rangle[p/X] makes sense

view this post on Zulip Mario Carneiro (May 30 2018 at 15:36):

I assume changing T for X does nothing?

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:36):

you got me

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:36):

I was just showing you how amazingly flexible our notation was

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:36):

T

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:36):

X

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:36):

any letter at all

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:36):

except most of them would be completely unsuitable

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:36):

I would stick with T

view this post on Zulip Mario Carneiro (May 30 2018 at 15:37):

From a CS standpoint those letters are kind of silly

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:37):

I can't quite work out who is laughing at who in this conversation :-)

view this post on Zulip Mario Carneiro (May 30 2018 at 15:37):

it's like a bound variable, but it isn't binding anything

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:37):

The ring contains an element called TT

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:37):

that's the trick

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:37):

k[T]k[T] and k[X]k[X] for polynomial rings

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:38):

they're defeq for you

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:38):

but for us, one has a T in and the other has an X in

view this post on Zulip Mario Carneiro (May 30 2018 at 15:38):

A simple idea that is surprisingly hard to formalize

view this post on Zulip Reid Barton (May 30 2018 at 15:38):

Tk[T]T \in k[T] just like Γ,xx\Gamma, x \vdash x

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:38):

A man who speaks both languages

view this post on Zulip Mario Carneiro (May 30 2018 at 15:38):

In that case x is in the context though

view this post on Zulip Mario Carneiro (May 30 2018 at 15:39):

k[T] isn't a context or a context like thing, it's a concrete ring

view this post on Zulip Mario Carneiro (May 30 2018 at 15:39):

(I guess k is in the context)

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:39):

Oh here is a question

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:39):

Is this question about notation

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:39):

completely independent of the question of formalizing the definition?

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:40):

i.e. the notation is something which can be thought about later

view this post on Zulip Mario Carneiro (May 30 2018 at 15:40):

not completely, but for the most part yes

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:40):

Those rings are not needed in the definition

view this post on Zulip Mario Carneiro (May 30 2018 at 15:40):

it affects what things get definitions

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:40):

that ring I posted is a famous example of a perfectoid ring

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:40):

nowhere in the definition of perfectoid space does that definition show up

view this post on Zulip Mario Carneiro (May 30 2018 at 15:41):

so for example since Zpcycl{\bf Z}^{cycl}_p is a notation you need a definition Z_cycl p

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:41):

however proving that that ring is a perfectoid ring is a theorem

view this post on Zulip Mario Carneiro (May 30 2018 at 15:42):

To answer your explicit question, yes you can (and probably should) defer all consideration of notation until late in the development

view this post on Zulip Mario Carneiro (May 30 2018 at 15:43):

It's basically easy to retrofit

view this post on Zulip Mario Carneiro (May 30 2018 at 15:44):

Probably in lean you wouldn't be able to have this X/T magic stuff, it would be just one fixed letter as part of the notation

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:52):

p151 : "choose a quasi-pro-etale surjection q from a strictly totally disconnected perfectoid space that can be written as an inverse limit of quasicompact separated etale maps q_i as in Proposition 11.24"

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:52):

This is going to be so much fun

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:52):

Lean is made for this sort of stuff

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:52):

Mario, this is what real maths looks like

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:53):

super-complex structures

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:53):

at least it's what some kinds of real maths looks like

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:53):

it is a million miles from anything that has ever been formalized

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:53):

and it will be easy to formalize

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:53):

that's why it's important

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:54):

and easy

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:54):

it's a huge gap in the market

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:55):

and I want to be part of a group which naturally fills this gap

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:55):

and has a great deal of fun and learns a bunch of stuff at the same time

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:56):

and there are huge gaps everywhere

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:56):

I'm sure Patrick can just reel off one in his area

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:56):

some complicated definition which turns out to be super-important in the kind of geometry he does

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:57):

Doing all this is one way of doing Tom Hales' fabstracts

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:57):

another way is: "scheme := sorry, now let's keep going"

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:57):

but this way is much more fun

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:57):

and you'll end up with types that typecheck

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:58):

Lean is a big puzzle game

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:58):

and we will be able to make some really cool levels for this game

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:58):

"construct a term of this type"

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:58):

that's the game

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:58):

the type is the level, the term is the solution

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:59):

All the old levels are boring

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:59):

"prove quadratic reciprocity"

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:59):

"prove the prime number theorem"

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:59):

kids want new levels

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:59):

they are bored with those old levels

view this post on Zulip Kevin Buzzard (May 30 2018 at 15:59):

and the computer scientists keep solving them again and again

view this post on Zulip Kevin Buzzard (May 30 2018 at 16:00):

all those websites

view this post on Zulip Kevin Buzzard (May 30 2018 at 16:00):

"100 classic levels in the formal proof verification game"

view this post on Zulip Kevin Buzzard (May 30 2018 at 16:00):

we want better levels with funkier graphics

view this post on Zulip Kevin Buzzard (May 30 2018 at 16:00):

I mean objects

view this post on Zulip Kevin Buzzard (May 30 2018 at 16:01):

it's like when I show my kids the old text-based adventure games which I used to love at their age

view this post on Zulip Kevin Buzzard (May 30 2018 at 16:01):

they are like "...dad, it's just a bunch of text"

view this post on Zulip Kevin Buzzard (May 30 2018 at 16:01):

"where are the perfectoid spaces?"

view this post on Zulip Kevin Buzzard (May 30 2018 at 16:02):

I mean graphics

view this post on Zulip Kevin Buzzard (May 30 2018 at 16:02):

the cool objects

view this post on Zulip Kevin Buzzard (May 30 2018 at 16:02):

things have moved on in maths

view this post on Zulip Kevin Buzzard (May 30 2018 at 16:07):

Should one put pdfs of papers in a github repo?

view this post on Zulip Kevin Buzzard (May 30 2018 at 16:08):

"Here are some foundational papers containing important definitions"

view this post on Zulip Kevin Buzzard (May 30 2018 at 16:08):

"which we are formalising"

view this post on Zulip Kevin Buzzard (May 30 2018 at 16:08):

Choice 1: offer a link

view this post on Zulip Kevin Buzzard (May 30 2018 at 16:08):

Choice 2: offer a pdf subdirectory

view this post on Zulip Kevin Buzzard (May 30 2018 at 16:08):

[Choice 3: both]

view this post on Zulip Patrick Massot (May 30 2018 at 16:10):

If arxiv version are up to date then a link is enough

view this post on Zulip Patrick Massot (May 30 2018 at 16:10):

But it's much more important to write a roadmap

view this post on Zulip Patrick Massot (May 30 2018 at 16:10):

unless you want to formalize everything in those papers...

view this post on Zulip Kevin Buzzard (May 30 2018 at 17:02):

This is very helpful.

view this post on Zulip Kevin Buzzard (May 30 2018 at 17:02):

It will take me some time to write a good roadmap

view this post on Zulip Kevin Buzzard (May 30 2018 at 17:02):

by which I mean a couple of days

view this post on Zulip Johan Commelin (May 30 2018 at 19:14):

Probably in lean you wouldn't be able to have this X/T magic stuff, it would be just one fixed letter as part of the notation

In Sage it is possible to choose your own symbol for the polynomial variable. I don't know what magic Python has to do this. But it is really nice!

view this post on Zulip Johan Commelin (May 31 2018 at 07:23):

Hmm, we probably also need some "almost mathematics". Or is that not needed for the definition, but only for using these guys? I don't remember...

view this post on Zulip Kevin Buzzard (May 31 2018 at 09:49):

That's only needed for the tilting correspondence I think

view this post on Zulip Kevin Buzzard (May 31 2018 at 09:49):

although we will surely need some facts about perfectoid rings

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 00:44):

What are the arguments for and against making Tate_ring into a typeclass?

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 00:44):

https://arxiv.org/pdf/1709.07343.pdf

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 00:44):

page 14 just before definition 3.1 for Tate ring. And then there is also the notion of perfectoid_ring in the definition itself.

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 00:45):

it's a condition on a pair consisting of a Tate ring and a prime number

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 00:46):

for example a certain subring of the ring (defined by the topology) has to be p-adically complete

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 00:47):

we will constantly be localizing Tate rings and getting other Tate rings

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 00:47):

it's some sort of p-adic version of usual ring localization

view this post on Zulip Kenny Lau (Jun 02 2018 at 00:50):

against: the pseudo-uniformiser is not canonical

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 00:50):

Kenny it's just the assertion that there exists pi with pi^p divides p

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 00:50):

you don't have to give it

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 00:50):

pi pseudouniformiser

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 00:51):

See Remark 3.2

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 00:51):

all you need is that one exists

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 00:51):

any choices are equivalent in some strong way

view this post on Zulip Mario Carneiro (Jun 02 2018 at 00:52):

I don't see why it wouldn't be a typeclass

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 00:52):

so no diamonds?

view this post on Zulip Mario Carneiro (Jun 02 2018 at 00:53):

with what?

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 00:53):

I have no idea how these things work

view this post on Zulip Mario Carneiro (Jun 02 2018 at 00:53):

where is p coming from though? Is it a component of any lower structures?

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 00:53):

it's a prime number

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 00:53):

best described as a parameter

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 00:53):

because you never change it

view this post on Zulip Mario Carneiro (Jun 02 2018 at 00:54):

The problem with parameters is they don't last long

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 00:54):

then it's just an input which is a prime number

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 00:54):

and which goes everywhere

view this post on Zulip Mario Carneiro (Jun 02 2018 at 00:54):

once you exit the section, the parameter becomes explicit and you can't make it a parameter again

view this post on Zulip Mario Carneiro (Jun 02 2018 at 00:55):

The question is: if lean is inferring Tate_ring ?p R, how can it infer p?

view this post on Zulip Mario Carneiro (Jun 02 2018 at 00:56):

I guess as long as all the theorems have p mentioned explicitly it may be solvable by unification, but I don't know how well this will work with notation and such that doesn't have a p explicitly in it

view this post on Zulip Kenny Lau (Jun 02 2018 at 00:57):

Tate_ring.p?

view this post on Zulip Mario Carneiro (Jun 02 2018 at 00:57):

that's also a possibility

view this post on Zulip Mario Carneiro (Jun 02 2018 at 00:59):

Let p be a fixed prime throughout. Recall that a topological ring R is Tate if it contains an open and bounded subring R0 ⊂ R and a topologically nilpotent unit omega∈R; such elements are called pseudo-uniformizers.

Where is p mentioned in that definition? Looks like Tate doesn't depend on p

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:00):

Right, I was confused earlier. You don't need p for Tate

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:01):

but you do need it for perfectoid

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:01):

so Tate_ring is I think fine, it's just a top ring plus some axioms

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:01):

and perfectoid_ring needs a Tate ring and a prime

view this post on Zulip Mario Carneiro (Jun 02 2018 at 01:02):

I suggest using a parameter (a two-argument typeclass) and see how it goes

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:03):

So my options are: (1) just make it a structure on a type alpha -- (a) it's a Tate ring (b) there's a prime (c) axioms

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:04):

or (2) demand both alpha and p as inputs and then it's a structure with (a) Tate ring and (b) axioms

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:04):

this is me building perfectoid ring

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:04):

I am building perfectoid space from the top down

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:04):

it's a long way up

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:04):

I'm taking tentative steps down

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:05):

and Mario is suggesting (2)

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:37):

Eew prime numbers

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:37):

how am I supposed to input a prime number?

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:37):

there's a function

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:37):

prime : nat -> Prop

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:38):

so it could be carrying round {p : nat} {p_prime : prime p}

view this post on Zulip Kenny Lau (Jun 02 2018 at 01:38):

just make a subtype

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:38):

I have an issue with the subtype solution

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:39):

then you have to spend your entire life writing p.1 instead of p

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:39):

and it is an absolutely fundamental part of the notation, it is on every line

view this post on Zulip Kenny Lau (Jun 02 2018 at 01:39):

then you have to spend your entire life writing p.1 instead of p

\u p

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:40):

and then you show it to people with the up-arrows off or something.

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:41):

like our dirty underwear

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:42):

Is the subtype already there?

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:44):

I can't see it explicitly defined. What is the subtype's name?

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:44):

prime is taken by the predicate

view this post on Zulip Reid Barton (Jun 02 2018 at 01:50):

I don't think there is one

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:51):

so I call it prime'?

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:59):

import data.nat.prime
open nat
definition prime' := subtype prime
-- unit test
definition two' : prime' := 2,prime_two

instance prime'_is_nat : has_coe prime'  := subtype.val

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:00):

Anyone any comments on style or anything that's missing?

view this post on Zulip Kenny Lau (Jun 02 2018 at 02:00):

make it an autoparam like pnat lol

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:00):

oh ha ha

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:00):

that is a really cool idea

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:00):

wait

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:00):

how does this work

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:01):

that open should be a namespace I think -- I'll edit

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:02):

I'll post a gist

view this post on Zulip Nicholas Scheel (Jun 02 2018 at 02:02):

what about a_prime? as in, “I have a prime number p : a_prime” (just my own way of doing it, I don’t think it’s common)

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:02):

https://gist.github.com/kbuzzard/327a9c466e3aaecf38fe93109ef8fde6

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:03):

I would like to maximise the chance that this stuff gets into mathlib

view this post on Zulip Nicholas Scheel (Jun 02 2018 at 02:03):

or rename the predicate to is_prime

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:03):

so I'd like to get it right as soon as possible

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:03):

It's very mathematical coding and the more I do it the better i'll get at it. I hope.

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:04):

for all I know there are standard rules of thumb concerning whether a name like prime should be used for the subtype or the predicate

view this post on Zulip Reid Barton (Jun 02 2018 at 02:05):

this is probably a bad idea but

instance predicate.has_coe_to_sort : has_coe_to_sort (  Prop) := (by apply_instance : has_coe_to_sort (set ))
variables {p : prime}

view this post on Zulip Kenny Lau (Jun 02 2018 at 02:05):

lmao

view this post on Zulip Kenny Lau (Jun 02 2018 at 02:05):

folly

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:05):

constant p

view this post on Zulip Kenny Lau (Jun 02 2018 at 02:05):

ensues

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:05):

I think that's the best place to start

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:05):

constant p : nat

view this post on Zulip Reid Barton (Jun 02 2018 at 02:06):

axiom hp : prime p

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:06):

I think that's consistent

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:07):

the guys doing LpL^p spaces will hit the roof

view this post on Zulip Kenny Lau (Jun 02 2018 at 02:07):

chaos

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:10):

Can I branch the mathlib in my perfectoid space repo

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:10):

and edit it

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:10):

and create a PR?

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:11):

and just make some note in a file: "this needs some stuff which isn't in mathlib yet -- when it's in mathlib then remove the import mathlib-foo-branch import"

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:11):

Is that a sane workflow or does it lead to madness?

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:12):

and get leanpkg to keep my branch up to date

view this post on Zulip Kenny Lau (Jun 02 2018 at 02:12):

it is sane

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:12):

What I am not clear on

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:13):

is whether I am supposed to say that my project has Mario's mathlib as a dependency

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:13):

or whether I am supposed to say that my project has some fork of mathlib, perhaps on my github website, as a dependency

view this post on Zulip Andrew Ashworth (Jun 02 2018 at 02:19):

If you have things you want to add to mathlib, I would have mathlib as its own project

view this post on Zulip Andrew Ashworth (Jun 02 2018 at 02:19):

and you work on it in that folder

view this post on Zulip Andrew Ashworth (Jun 02 2018 at 02:19):

editing _target is bad news

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:22):

I see. So you're saying that the perfectoid space repository could have as a dependency a perfectoid space mathlib

view this post on Zulip Andrew Ashworth (Jun 02 2018 at 02:22):

yes

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:22):

which is some fork of mathlib

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:23):

and we maybe have some directory like src/for_mathlib subdirectory

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:24):

and then when things are looking tidy

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:24):

we can just edit our mathlib, submit a PR, and press on

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:25):

Have I got all this straight?

view this post on Zulip Andrew Ashworth (Jun 02 2018 at 02:26):

yes

view this post on Zulip Andrew Ashworth (Jun 02 2018 at 02:26):

_target is not for things you plan on editing or working on

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:27):

I see

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:27):

you know what I sometimes creep in there in the middle of the night and run leanpkg build

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:27):

because I know my project won't

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:28):

Is adic_space a typeclass?

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:28):

Is scheme a typeclass?

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:28):

@Reid Barton what are your thoughts?

view this post on Zulip Andrew Ashworth (Jun 02 2018 at 02:28):

indeed package distribution in lean is a bit annoying right now since it's hard to distribute .oleans

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:28):

I just rebuild whenever I upgrade

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:29):

worth the initial wait

view this post on Zulip Andrew Ashworth (Jun 02 2018 at 02:29):

if mathlib really wants to contain all of mathematics, at some point people are not going to be able to run leanpkg build in a sane amount of time

view this post on Zulip Andrew Ashworth (Jun 02 2018 at 02:29):

unfortunately we are not quite near that point though

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:29):

https://github.com/kbuzzard/lean-stacks-project/blob/6617de7dd5f11af46f0c7e0d2223ee065d71b9f3/src/scheme.lean#L366

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:30):

if you have a sensible project that builds, then I think you can just build your project and it will only build the bits of mathlib that it needs

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:30):

this is one of my motivations for defining perfectoid spaces by the way -- to see performance.

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:30):

It's all very well proving things about finite groups

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:31):

the proof of the odd order theorem is just John Thompson and his friends writing down everything they know about finite groups and noticing that it happens to be enough

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:31):

but to write down even one thing about perfectoid spaces

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:31):

will force Lean to handle the notion of a perfectoid space

view this post on Zulip Andrew Ashworth (Jun 02 2018 at 02:31):

we also want oleans so we can search everything though (although there are ways to handle this differently)

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:33):

Oh -- does e.g. hover or ctrl-space not work in VS Code without the olean files? What exactly do you need them for?

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:33):

I have no idea what they are

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:33):

all I know is that if you type leanpkg build in _target/deps/mathlib then afterwards it goes quicker

view this post on Zulip Mario Carneiro (Jun 02 2018 at 02:37):

unfortunately we are not quite near that point though

Did you see https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/travis.20caching/near/127367872 ?

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:38):

dammit

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:38):

I want to get some headline definition of perfectoid space

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:38):

structure perfectoid_space (α : Type) extends adic_space α :=
(perfectoid_cover :  {γ : Type} (R : γ  Type) [ i : γ,  blah blah blah

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:39):

so I need adic_space

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:39):

but

view this post on Zulip Reid Barton (Jun 02 2018 at 02:39):

Using structure for schemes and so on seems reasonable. I don't see any practical advantages to using a type class.

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:39):

structure adic_space (α : Type) : Type := sorry doesn't work

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:39):

I mean the sorry doesn't work

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:39):

that's not an adequate structure

view this post on Zulip Mario Carneiro (Jun 02 2018 at 02:39):

you can write structure adic_space (α : Type) : Type.

view this post on Zulip Mario Carneiro (Jun 02 2018 at 02:40):

or def adic_space (α : Type) : Type := sorry

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:41):

the problem with the structure solution is that then it is far less obvious that something is missing

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:41):

the problem with the def solution is that I can't then extend the structure to a perfectoid space

view this post on Zulip Mario Carneiro (Jun 02 2018 at 02:41):

If you want to make sure to get the sorry warning with a structure you can do structure adic_space (α : Type) : Type := (unfinished : sorry)

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:42):

rofl

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:43):

Why are rings typeclasses? Why are they any different to schemes?

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:43):

Product of schemes is a scheme etc

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:44):

[wrong thread @Andrew Ashworth ] -- you can edit the post and just change the thread by editing it

view this post on Zulip Reid Barton (Jun 02 2018 at 02:48):

but the product of schemes isn't a "scheme structure" on the product of the underlying sets

view this post on Zulip Reid Barton (Jun 02 2018 at 02:48):

because that is sort of a weird way of thinking about it, but more importantly because its set of points is different

view this post on Zulip Reid Barton (Jun 02 2018 at 02:49):

Somehow the relationship between a ring and its underlying set is much more important than the relationship between a scheme and its underlying set

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:50):

o_O so it depends on the underlying type?

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:50):

I see

view this post on Zulip Reid Barton (Jun 02 2018 at 02:50):

Well, if you were going to write

class scheme (\a : Type) := ...

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:51):

what about if I just wrote class scheme := and then asked the user to provide the type?

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:51):

oh is that somehow the canonically bad thing to do

view this post on Zulip Reid Barton (Jun 02 2018 at 02:51):

then nobody would know which scheme you were talking about

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:52):

right

view this post on Zulip Reid Barton (Jun 02 2018 at 02:52):

Somehow, I feel that class group (\a : Type) := ... is related to the abuse of notation where we identify a group with its underlying set

view this post on Zulip Reid Barton (Jun 02 2018 at 02:53):

we feel that we can identify the group just by naming the set

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:53):

I do think it is rare that you find yourself putting two group structures on one set

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:53):

and even if it happened you could imagine that it was for some temporary calculation

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:53):

possibly which ultimately even proved they were equal

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:54):

on the other hand I'd say just the same thing about schemes

view this post on Zulip Reid Barton (Jun 02 2018 at 02:54):

but I guess, do you think of a scheme as a set equipped with "scheme structure"?

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:54):

Maybe it's a locally-ringed space with a scheme set-of-axioms

view this post on Zulip Reid Barton (Jun 02 2018 at 02:55):

Yes, that seems much better

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:55):

oh god that would make it a dreaded subtype

view this post on Zulip Reid Barton (Jun 02 2018 at 02:55):

Anyways, you wouldn't be able to write instance (scheme α) (scheme β) : scheme (α × β) to get α × β notation for product schemes because the underlying set is wrong

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:56):

As a mathematician I find it extremely hard to distinguish whether I "think about a scheme as a set equipped with the structures of a topological space, a sheaf of rings on the space and an axiom about the rings"

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:56):

or whether I "think about it as a locally ringed space equipped with an axiom"

view this post on Zulip Mario Carneiro (Jun 02 2018 at 02:57):

By the way re: your prime question, there is the naming convention of capitalizing p : Prime for bundled structures

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 02:57):

oh great! Thanks!

view this post on Zulip Reid Barton (Jun 02 2018 at 02:59):

Yeah, I think it's hard to pin anything down too precisely in this direction.
That's why I wrote "practical advantages" above :simple_smile:

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 03:00):

current v

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 03:00):

https://gist.github.com/kbuzzard/327a9c466e3aaecf38fe93109ef8fde6

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 03:00):

of Prime

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 03:01):

Yes, that seems much better

So a scheme should extend a locally ringed space by adding one axiom?

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 03:01):

Ha ha that would break my proof that affine schemes are schemes :-)

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 03:01):

the dirty truth coming out :-)

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 03:02):

I figured that I could define a scheme to be a topological space with a sheaf of rings which was locally an affine scheme

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 03:02):

because this would imply it was a locally ringed space

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 03:02):

I was cutting corners :-)

view this post on Zulip Mario Carneiro (Jun 02 2018 at 03:03):

and you wonder why I think it isn't ready for mathlib...

view this post on Zulip Reid Barton (Jun 02 2018 at 03:03):

Oh, I forgot "locally ringed" includes an extra condition

view this post on Zulip Johan Commelin (Jun 02 2018 at 03:21):

I do think it is rare that you find yourself putting two group structures on one set

I think the most famous example is Eckman-Hilton for homotopy groups.

view this post on Zulip Johan Commelin (Jun 02 2018 at 03:22):

And indeed, you prove that they are the same group structure.

view this post on Zulip Johan Commelin (Jun 02 2018 at 03:23):

Personally I definitely would love to be able to write X \times Y for the product of schemes.

view this post on Zulip Johan Commelin (Jun 02 2018 at 03:24):

The only way that I currently see to make this happen, is that we have some sort of has_cat_prod notation for categorical products. And then a proof that Schemes has products.

view this post on Zulip Johan Commelin (Jun 02 2018 at 03:25):

Pullbacks become a problem (notationwise) because we cannot but a subscript scheme under the \times.

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 03:28):

I've got two elements of a ring.

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 03:28):

Oh I know the bloody answer to what I was going to ask

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 03:28):

Mathematicians are great

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 03:28):

"use a subtype"

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 03:28):

"elements a and b in R, with a dividing b in the subring S"

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 03:28):

Having p as a subtype is awful

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 03:28):

x ^ p

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 03:28):

Lean : ?!

view this post on Zulip Mario Carneiro (Jun 02 2018 at 03:29):

yeah this is going to be difficult

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 03:29):

x is in a ring and p has a coercion to nat

view this post on Zulip Mario Carneiro (Jun 02 2018 at 03:29):

you can either coerce, or have a has_pow A Prime instance

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 03:29):

rofl

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 03:30):

I coerce with \u?

view this post on Zulip Mario Carneiro (Jun 02 2018 at 03:30):

lean can't coerce and do typeclass inference at the same time

view this post on Zulip Mario Carneiro (Jun 02 2018 at 03:30):

you would have to say it's a nat

view this post on Zulip Mario Carneiro (Jun 02 2018 at 03:30):

x ^ (p:nat)

view this post on Zulip Johan Commelin (Jun 02 2018 at 03:31):

lean can't coerce and do typeclass inference at the same time

Is this something that might change in Lean 4?

view this post on Zulip Mario Carneiro (Jun 02 2018 at 03:31):

I think that a prime typeclass might work better for you

view this post on Zulip Mario Carneiro (Jun 02 2018 at 03:31):

no, that's unlikely to change

view this post on Zulip Mario Carneiro (Jun 02 2018 at 03:31):

if you think about it that's a really large search space

view this post on Zulip Mario Carneiro (Jun 02 2018 at 03:32):

it's too underdetermined

view this post on Zulip Johan Commelin (Jun 02 2018 at 03:32):

Yes, I agree. Somehow humans are extremely good at navigating that search space.

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 03:32):

wait

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 03:32):

example (R : Type) [comm_ring R] : has_pow R ℕ := by apply_instance

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 03:32):

is that not a thing? Doesn't run for me

view this post on Zulip Mario Carneiro (Jun 02 2018 at 03:33):

you have algebra.group_power?

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 03:33):

I have one lying around somewhere

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 03:36):

How about adding p as a constant and the fact that it's prime as an axiom?

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 03:36):

Is that just a bridge too far?

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 03:37):

so if the predicate is called prime and the subtype Prime, what is the typeclass called?

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 03:37):

is_prime I guess?

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 05:01):

eew

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 05:01):

definition complete (R : Type) [topological_space R] [ring R] [topological_ring R] : Prop := sorry

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 05:02):

is that going away in Lean 4?

view this post on Zulip Mario Carneiro (Jun 02 2018 at 05:02):

Yes, we've decided that no one needs topology anymore

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 05:02):

you're going to use sites?

view this post on Zulip Mario Carneiro (Jun 02 2018 at 05:03):

nothing but pointless topology for us

view this post on Zulip Johan Commelin (Jun 02 2018 at 05:03):

No, infty-topoi.

view this post on Zulip Johan Commelin (Jun 02 2018 at 05:03):

nothing but pointless topology for us

definition complete (R : Type) [pointless_topological_space R] [ring R] [pointless_topological_ring R] : Prop := sorry

view this post on Zulip Mario Carneiro (Jun 02 2018 at 05:04):

much better

view this post on Zulip Johan Commelin (Jun 02 2018 at 05:06):

Kevin, so the problem is that topological_ring should imply ring and topological_space, right?

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 05:07):

I don't know why I had to say all three

view this post on Zulip Mario Carneiro (Jun 02 2018 at 05:07):

Maybe @Johannes Hölzl should field this one, I'm not sure why it's not a class extending those others

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 05:08):

I tried using type class inference

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 05:08):

class perfectoid_ring (R : Type) [Tate_ring R] (p : ℕ) [is_prime p] :=

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 05:09):

and then when I ask type class inference to prove the hypothesis that R is a perfectoid ring

view this post on Zulip Mario Carneiro (Jun 02 2018 at 05:09):

I mean I know why you had to write that, are you asking what is happening or why is it set up that way?

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 05:10):

I have typeclass woes

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 05:10):

I am writing my flagship definition

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 05:10):

so it has to look lovely

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 05:10):

and I write [∀ i, perfectoid_ring (R i) p]

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 05:10):

and curse the p

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 05:11):

and it complains that it can't see why R i is a Tate ring

view this post on Zulip Mario Carneiro (Jun 02 2018 at 05:11):

because perfectoid ring depends on Tate ring

view this post on Zulip Mario Carneiro (Jun 02 2018 at 05:12):

The way you declared it, you always have to write [Tate_ring R] [is_prime p] [perfectoid_ring R p]

view this post on Zulip Mario Carneiro (Jun 02 2018 at 05:13):

since perfectoid_ring takes the other two as parameters

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 05:15):

class perfectoid_ring (R : Type) [Tate_ring R] (p : ) [is_prime p] :=
(is_complete : complete R)
(is_uniform  : uniform R)
(ramified    :  ω : R ,
                 (is_pseudo_uniformizer ω)  (ω ^ p  p))
 (Frob       :  a : R ,
                  b c : R , a = b ^ p + p * c)

structure foo (p : ) [is_prime p] :=
(hello :  (R : Type) [perfectoid_ring R p], 1 + 1 = 2) -- failed to synthesize Tate_ring

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 05:16):

(hello : ∃ (R : Type) [Tate_ring R] [perfectoid_ring R p], 1 + 1 = 2)

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 05:16):

works but looks silly

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 05:16):

of course it's a Tate ring -- it's a perfectoid ring!

view this post on Zulip Mario Carneiro (Jun 02 2018 at 05:17):

It can't synthesize any of those classes

view this post on Zulip Mario Carneiro (Jun 02 2018 at 05:17):

it's right of the colon, so no typeclass inference for you

view this post on Zulip Johan Commelin (Jun 02 2018 at 05:17):

So, you should extend Tate_ring?

view this post on Zulip Mario Carneiro (Jun 02 2018 at 05:17):

use by exactI to workaround

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 05:17):

but I don't want by exactI everywhere

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 05:17):

it's an ugly hack

view this post on Zulip Mario Carneiro (Jun 02 2018 at 05:18):

Wait we're talking about different things again

view this post on Zulip Mario Carneiro (Jun 02 2018 at 05:18):

to make Tate_ring inferrable from perfectoid_ring, just make it extends the other

view this post on Zulip Mario Carneiro (Jun 02 2018 at 05:19):

instead of taking it as parameter

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 05:23):

I changed for a reason

view this post on Zulip Mario Carneiro (Jun 02 2018 at 05:25):

Why did you write out the divisibility condition instead of using the existing definition?

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 05:30):

I didn't know how to reduce mod p offhand

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 05:31):

so just wrote something mathematically equivalent

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 05:31):

reducing mod p would be fine

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 05:32):

I'd just need to look up how to make a principal ideal and then quotient out by an ideal, and then I would have had to verify that the p'th power map was well-defined on the quotient

view this post on Zulip Mario Carneiro (Jun 02 2018 at 05:32):

or you could write p | b ^ p - a

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 05:32):

try that with a subtype

view this post on Zulip Mario Carneiro (Jun 02 2018 at 05:33):

?

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 05:33):

just noting that a lot of coercion would be happening if we used subtypes

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 05:33):

for p

view this post on Zulip Mario Carneiro (Jun 02 2018 at 05:34):

I don't recommend it. You need it more often as a nat than a prime

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 05:35):

type mismatch at application
  pow b
term
  b
has type
  :Rᵒ
but is expected to have type
  ℕ

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 05:36):

b has type some strange smiley

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 05:37):

∃ b : R ᵒ, (p : R ᵒ) ∣ (b ^ p - a))

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 05:37):

looks less cool

view this post on Zulip Johan Commelin (Jun 02 2018 at 05:48):

Hmm, this doesn't score many readability points with me...

view this post on Zulip Mario Carneiro (Jun 02 2018 at 05:49):

why? that seems plenty readable

view this post on Zulip Mario Carneiro (Jun 02 2018 at 05:49):

you may also be able to get away with just \u p

view this post on Zulip Johan Commelin (Jun 02 2018 at 05:50):

Well, we are optimising this definition for maximal readability, because it will be the first Lean a lot of mathematicians will read this summer.

view this post on Zulip Johan Commelin (Jun 02 2018 at 05:50):

And then (p : R ᵒ) will already scare them away.

view this post on Zulip Johan Commelin (Jun 02 2018 at 05:50):

Why is it even there?

view this post on Zulip Mario Carneiro (Jun 02 2018 at 05:51):

because p is a nat but it is being mapped into the ring so it can be a divisor

view this post on Zulip Johan Commelin (Jun 02 2018 at 05:51):

Can't we tell somewhere else that this division happens in R ᵒ ?

view this post on Zulip Mario Carneiro (Jun 02 2018 at 05:51):

yes, that's why I suggested \u p

view this post on Zulip Johan Commelin (Jun 02 2018 at 05:53):

I think in the end, I would rather prefer something close to ∃ b : R ᵒ, a = b ^ p mod p

view this post on Zulip Johan Commelin (Jun 02 2018 at 05:53):

Even if it is just notation for what we had before.

view this post on Zulip Johan Commelin (Jun 02 2018 at 05:54):

@Kevin Buzzard something like that should be possible. And then you don't need quotient rings.

view this post on Zulip Johannes Hölzl (Jun 02 2018 at 08:16):

Maybe @Johannes Hölzl should field this one, I'm not sure why it's not a class extending those others

If topological_ring would contain the topology or the ring itself, then we would need to duplicate the algebraic and topological type class hierarchy. So we would need a topological_domain, a uniform_space_ring, a uniform_domain etc. by keeping it a relation this type class hierarchy duplication is avoided. Also topological_ring is a Prop now, so we can add arbitrary instances proving that something is a topological_ring without worrying that they are definitional equal.

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 21:29):

OK so a perfectoid space is an adic space with some properties, so we need to develop the theory of adic spaces

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 21:31):

and a basic constructor for adic spaces is the Spa function, which takes as input a so-called "Huber pair" and outputs an affinoid pre-adic space

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 21:31):

I am thinking about how to formalize that in Lean and I have a question regarding the input, that is, the Huber Pair.

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 21:32):

A Huber Pair is a topological ring RR satisfying some axioms, and a subring R+R^+ satisfying some more axioms related to both R+R^+ and how it sits in RR.

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 21:33):

So I can envisage several ways of setting this up

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 21:34):

and what of course I would really like to know is which one is the "best" way, where by "best" I mean "one for which the interface will be easiest to write".

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 21:34):

so how do I analyse this further?

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 21:34):

I definitely want easy access to RR

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 21:36):

and most of the time, when creating new pairs from old, you build the new RR from the old RR and then let the new R+R^+ be "the same construction but with R+R^+"

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 21:36):

e.g. new R+R^+ could be the image of the old R+R^+ or whatever

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 21:37):

and occasionally RR stays the same but R+R^+ changes

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 21:37):

one could think of changing R+R^+ as "changing RR infinitesimally"

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 21:37):

"so mostly you don't notice"

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 21:38):

and everything will be a topological ring

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 21:38):

and every map will be continuous

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 21:39):

and we'll be building things like "polynomial ring over a Huber Pair", sending (R,R+)(R,R^+) to (R[X],R+[X])(R[X],R^+[X])

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 21:39):

or "completion of a Huber Pair", sending (R,R+)(R,R^+) to (R^,R^+)(\hat{R},\hat{R}^+)

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 21:40):

where R^\hat{R} is a certain kind of completion of RR etc

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 21:41):

and R^+\hat{R}^+ is the topological closure of R+R^+

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:28):

I'm going to make a structure containing RR and R+R^+, and rely on has_coe_to_sort to enable me to treat it as R.

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:29):

Is there trouble ahead?

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:31):

There will be maps between different $$R$$s but in TPIL they sketch a method of how to use has_coe_to_fun which was designed for this purpose I guess.

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:50):

@Kenny Lau I am looking at the definition of f-adic ring in Wedhorn's notes (section 6.1) and he talks about a finitely-generated ideal of a ring. What's the best way of saying "there exists a finitely-generated ideal of R such that blah" in Lean, for a comm_ring?

view this post on Zulip Kenny Lau (Jun 03 2018 at 22:50):

we have all about that in linear_algebra/something I think

view this post on Zulip Kenny Lau (Jun 03 2018 at 22:51):

they proved that every vector space has a basis

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:51):

http://www2.math.uni-paderborn.de/fileadmin/Mathematik/People/wedhorn/Lehre/AdicSpaces.pdf

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:51):

it's the finiteness I am interested in

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:51):

I just want a smooth way of formalizing that definition

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:51):

p46 of the pdf

view this post on Zulip Kenny Lau (Jun 03 2018 at 22:51):

finiteness is just either fintype or set.finite

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:52):

OK I'll write something

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:52):

and then you can laugh at me :-)

view this post on Zulip Kenny Lau (Jun 03 2018 at 22:52):

/-- Linear span of a set of vectors -/
def span (s : set β) : set β := { x | (v : lc α β), (xs, v x = 0)  x = v.sum (λb a, a  b) }

view this post on Zulip Kenny Lau (Jun 03 2018 at 22:52):

https://github.com/leanprover/mathlib/blob/master/linear_algebra/basic.lean#L122

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:52):

Oh!

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:52):

I forgot -- see you on the R thread

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 23:45):

Does this already have a name in mathlib:

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 23:45):

definition is_cover {X γ : Type} (U : γ → set X) := ∀ x, ∃ i, x ∈ U i

view this post on Zulip Kenny Lau (Jun 03 2018 at 23:49):

lemma compact_elim_finite_subcover {s : set α} {c : set (set α)}
  (hs : compact s) (hc₁ : tc, is_open t) (hc₂ : s  ⋃₀ c) : c'c, finite c'  s  ⋃₀ c' :=

view this post on Zulip Kenny Lau (Jun 03 2018 at 23:49):

https://github.com/leanprover/mathlib/blob/master/analysis/topology/topological_space.lean#L475

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 23:49):

structure Huber_Pair (R : Type) :=
[is_Hring : Huber_ring R]
(Rp : set R)
[intel : is_ring_of_integral_elements Rp]

structure Huber_Pair' (R : Type) [Huber_ring R] :=
(Rp : set R)
[intel : is_ring_of_integral_elements Rp]

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 23:50):

Is the first one just silly or does it ever have its uses?

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 23:50):

A Huber Pair is a Huber Ring plus a subring which is a ring of integral elements (i.e. satisfies a bunch of axioms)

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 23:51):

https://github.com/leanprover/mathlib/blob/master/analysis/topology/topological_space.lean#L475

is_cover is about as long as s ⊆ ⋃₀ c

view this post on Zulip Kenny Lau (Jun 03 2018 at 23:52):

lol

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 23:52):

it's all about the interface though

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 23:53):

(R⁺ : set R)

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 23:54):

what is this "unexpected token" error?

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 23:54):

can I PR it in somehow?

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 23:54):

hmm

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 23:54):

can I use it in notation?

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 23:56):

yes :-)

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 00:07):

Is the first one just silly or does it ever have its uses?

aargh the second one doesn't compile :-/

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 00:07):

because of type class inference woes

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 00:08):

definition is_ring_of_integral_elements {R : Type} [Huber_ring R] (Rplus : set R) : Prop := sorry

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 00:08):

needs huber ring

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 00:10):

boggle <goes back to type class woes thread>

view this post on Zulip Reid Barton (Jun 04 2018 at 00:11):

I don't understand why that would make the second one not compile

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 00:15):

no I am an idiot

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 00:15):

it works fine

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 00:16):

I am still very unsteady on my feet with typeclasses

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 00:16):

all I know is "it sometimes doesn't work" and it's something about where the colon is

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 00:22):

structure Huber_pair :=
(R : Type)
[RHuber : Huber_ring R]
(Rplus : set R)
[intel : is_ring_of_integral_elements Rplus]

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 00:22):

This is annoying

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 00:22):

I don't think I can use type class inference to get a Huber pair structure on R, because I want the freedom to change R+R^+

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 00:23):

postfix : 66 := λ R : Huber_pair _, R.Rplus

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 00:23):

and if I add it as a family of structures on R

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 00:23):

then I am forever having to make R and then the pair

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 00:23):

I can't just say "Let RR be a Huber Pair" like we'd say in maths

view this post on Zulip Scott Morrison (Jun 04 2018 at 00:25):

So, often a good solution when you want two different typeclasses on the same underlying type,

view this post on Zulip Scott Morrison (Jun 04 2018 at 00:25):

is to use the trick that Mario showed me, of making a "wrapper".

view this post on Zulip Scott Morrison (Jun 04 2018 at 00:25):

As an example, to define the opposite category, I use:

def op (C : Type u₁) : Type u₁ := C

notation C `ᵒᵖ` := op C

variable {C : Type u₁}
variable [𝒞 : category.{u₁ v₁} C]
include 𝒞

instance Opposite : category.{u₁ v₁} (Cᵒᵖ) := ...

view this post on Zulip Scott Morrison (Jun 04 2018 at 00:26):

Here the idea is that op C is of course just C, "thought of" as objects of the opposite category.

view this post on Zulip Scott Morrison (Jun 04 2018 at 00:27):

It's something mathematicians do all the time and are perfectly comfortable with, and maybe works for your Huber pairs setting, in particular when you want to change R+, but leave R alone.

view this post on Zulip Scott Morrison (Jun 04 2018 at 00:28):

On the other hand, I suspect that you never ever actually want to look at an element of the R of a Huber pair, so making a typeclass on R maybe doesn't have that much value.

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 00:30):

I think I will forever be playing around with pi's and p's in R I think

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 00:30):

as I explicitly evaluate my completions etc

view this post on Zulip Scott Morrison (Jun 04 2018 at 00:31):

Scratch that suggestion then!

view this post on Zulip Johan Commelin (Jun 04 2018 at 11:39):

I can't just say "Let RR be a Huber Pair" like we'd say in maths

I think it is important that we try to keep this "feature". But I don't see how to implement it in Lean, and also give you the freedom to change R⁺.

view this post on Zulip Johan Commelin (Jun 04 2018 at 11:42):

Unless we also have some postfix accessor notation for the ambient ring. So that a Huber pair R is (R^?,R⁺). But I don't have any cute ideas for what ? should actually be. And it is going to be annoying and offputing for mathematicians anyway.

view this post on Zulip Reid Barton (Jun 04 2018 at 11:48):

Could that notation for the ambient ring just be a coercion?

view this post on Zulip Reid Barton (Jun 04 2018 at 11:50):

structure Huber_pair :=
(R : Type)
[is_ring : ring R]
(Rp : set R)
(huber : true)

instance : has_coe_to_sort Huber_pair :=
{ S := Type, coe := Huber_pair.R }

instance Huber_pair.ring (R : Huber_pair) : ring R := R.is_ring

view this post on Zulip Johan Commelin (Jun 04 2018 at 11:51):

I think @Kevin Buzzard is currently the only one who knows enough about Huber pairs to see if this will give trouble down the road.

view this post on Zulip Reid Barton (Jun 04 2018 at 11:52):

notation R ``:99 := R.Rp
variables {R : Huber_pair} {x : R} {h : x  R}

view this post on Zulip Reid Barton (Jun 04 2018 at 11:52):

Yes, probably.

view this post on Zulip Johan Commelin (Jun 04 2018 at 11:56):

So far that looks promising, I would say.

view this post on Zulip Assia Mahboubi (Jun 04 2018 at 12:14):

I am trying to understand the maths a little bit more, to see if I can help. But I am a bit lost. In @Kevin Buzzard's first ref, p46 defines what an f-adic ring is, but there is no f right? Can I understand them as an I-adic ring? Then, for the question on Huber pairs. I do not understand this "pair" vocabulary yet. Can I think of RR as an ambiant (topological) ring, and R+R^+ as the actual interesting thing?

view this post on Zulip Johan Commelin (Jun 04 2018 at 12:15):

I think both rings in a Huber pair are interesting...

view this post on Zulip Johan Commelin (Jun 04 2018 at 12:16):

It is like ZQ\mathbb{Z} \subset \mathbb{Q} on steroids.

view this post on Zulip Johan Commelin (Jun 04 2018 at 12:17):

Also, I think the "f" in f-adic stands for finite: there is a finiteness condition in both items in the condition, first on the subset TT, and then on the ideal II in the second condition of the definition.

view this post on Zulip Johan Commelin (Jun 04 2018 at 12:19):

Disclaimer: I'm not an expert on this stuff. Only followed some seminars on this.

view this post on Zulip Assia Mahboubi (Jun 04 2018 at 12:42):

Sorry my sentence was misleading and in fact I think it was even nonsensical, as A+A^+ should be integrally closed in AA.

view this post on Zulip Johan Commelin (Jun 04 2018 at 12:47):

Don't you mean it the other way round?

view this post on Zulip Assia Mahboubi (Jun 04 2018 at 12:49):

Thanks.

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 13:09):

I am trying to understand the maths a little bit more, to see if I can help. But I am a bit lost. In @Kevin Buzzard's first ref, p46 defines what an f-adic ring is, but there is no f right? Can I understand them as an I-adic ring? Then, for the question on Huber pairs. I do not understand this "pair" vocabulary yet. Can I think of RR as an ambiant (topological) ring, and R+R^+ as the actual interesting thing?

Yes "f-adic ring" is a terrible name, there is no f, "f-adic ring" is just a ring with some structure and some axioms. In fact it's such a terrible name that Scholze proposed renaming it to "Huber ring" and that's what we're going to use in the project.

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 13:10):

The modern terminology is that RR is a Huber ring and (R,R+)(R,R^+) is a Huber pair. In the old terminology RR is an f-adic ring and R+R^+ is a ring of integral elements (I guess this definition will stay)

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 13:11):

So many of the proofs do not care about R+R^+, but I am beginning to see more about how this is going to work. I suspect often we will not make the Huber pair -- we will just have a ring RR and a subring R+R^+ and do calculations with them

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 20:19):

Should I have structure perfectoid_space := (X : Type) ... or structure perfectoid_space (X : Type) := ...?

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 20:19):

I was using the latter

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 20:19):

but here's something I ran into.

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 20:20):

A perfectoid space is a topological space equipped with a presheaf of rings and satisfying a bunch of axioms.

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 20:21):

A presheaf of rings on a topological space is the assignment, for every open subset U of the topological space, of a ring F(U)F(U), and a bit more data, and some axioms.

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 20:23):

Given a perfectoid space XX, and an open subset UU of the underlying topological space (which is also called XX), I can pull back all the structure and get a perfectoid space structure on UU (e.g. I need to associate a ring to an open subset of UU, but an open subset of UU is an open subset of XX so we use the presheaf of rings on XX to do this).

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 20:23):

So far so good.

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 20:23):

But I was kind of expecting perfectoid_space to be a typeclass

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 20:24):

and (finally the question!) I don't know how to get type class inference to get us from X to U

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 20:24):

because U is an open set in X so it's not even a type

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 20:25):

and if we use the associated subtype {x : X // x \in U}

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 20:25):

then I don't know how to say "...oh, and U needs to be open" to type class inference.

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 20:25):

In short -- if I have (X : Type) [perfectoid_space X]

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 20:26):

(perfectoid space extends topological space)

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 20:26):

and if (U : set X) is open

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 20:27):

then my instance wants to look like (X : Type) [perfectoid_space X] (U : set X) (HU : is_open U) : perfectoid_space {x : X // x \in U}

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 20:28):

"an open subset of a perfectoid space is a perfectoid space"

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 20:28):

but how is type class inference going to spot that U is open?

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 20:29):

I guess I could work with subtypes and make is_open a typeclass on them? Is this crazy? Would it even work?

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 20:33):

Or should I just give up on making perfectoid space a typeclass?

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 20:34):

Presumably typeclass inference only works on things which have been tagged as classes

view this post on Zulip Nicholas Scheel (Jun 04 2018 at 20:47):

I would say it makes sense to make them either both typeclasses or plain structures (you can still write a function to do what you want to do with typeclass inference there, I think); perhaps it wouldn’t hurt to start with all the structure explicit, and then determine what could be converted to use typeclass machinery ...

view this post on Zulip Nicholas Scheel (Jun 04 2018 at 20:49):

theorem perfectoid_space_on_open_set (X : Type) (U : set X) (HU : is_open U) : perfectoid_space X -> perfectoid_space {x : X // x \in U}

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 20:52):

So I can prove that theorem

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 20:52):

my question is whether I can persuade the type class inference system to use it

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 20:52):

if perfectoid_space is a class

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 20:52):

and what I can't get my head around

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 20:53):

is how type class inference can possibly guess that a subset is open

view this post on Zulip Nicholas Scheel (Jun 04 2018 at 20:53):

I agree, that’s why I think is_open would also have to be a typeclass

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 20:53):

but there is a technical problem there

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 20:53):

because U is not a type

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 20:53):

it's a term

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 20:54):

hmm

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 20:54):

I am just assuming that it's impossible to make this work

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 20:54):

Does it actually work?

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 20:55):

I somehow can't get it all to fit together but maybe it's possible

view this post on Zulip Nicholas Scheel (Jun 04 2018 at 20:56):

aren’t the (ring, group) homomorphisms classes? I don’t see how a set would be much different

view this post on Zulip Nicholas Scheel (Jun 04 2018 at 21:00):

class is_ring_hom

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 21:11):

That's true!

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 21:11):

Maybe it all just works?

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 21:14):

variables {X : Type} [topological_space X]

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 21:15):

class is_open (U : set X) : Prop :=
(is_open : is_open U)

or some such thing

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 21:16):

hmm maybe I need to think a bit about variable names...

view this post on Zulip Reid Barton (Jun 04 2018 at 21:31):

You can potentially also just make is_open into a class, with attribute [class] is_open (or local attribute)

view this post on Zulip Kevin Buzzard (Jun 04 2018 at 23:14):

I don't have time for this now but hopefully I'll be able to get to it tomorrow. Once I've resolved this I think I'm ready to go. I've been writing stuff from the top down, i.e. I have a definition of a perfectoid space but it depends on several other definitions, some of which I have and some of which I don't. Up here it feels very close to maths and looks very close to maths too.

view this post on Zulip Patrick Massot (Jun 05 2018 at 07:24):

Are doing all this privately in the end?

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 08:16):

No not at all -- but I wanted to get the definition of perfectoid space written (modulo lots of other definitions which are not written)

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 08:16):

before I "went public" as it were

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 08:16):

I am currently struggling with type class inference issues but I think I had the same ones before

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 08:16):

so I will look in the old thread

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 08:45):

Patrick here's the state of things:

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 08:45):

import adic_space

--notation
postfix `` : 66 := power_bounded_subring

/-- A perfectoid ring, following Fontaine Sem Bourb-/
class perfectoid_ring (R : Type) (p : ) [is_prime p] extends Tate_ring R :=
(is_complete : complete R)
(is_uniform  : uniform R)
(ramified    :  ω : R , (is_pseudo_uniformizer ω)  (ω ^ p  p))
(Frob        :  a : R ,  b : R , (p : R )  (b ^ p - a))

structure perfectoid_space (X : Type) (p : ) [is_prime p] extends adic_space X :=
(perfectoid_cover :
  -- gamma is our indexing set, U_i are the open cover for i in gamma
   {γ : Type} (U : γ  set X) [U_open :  i, is_open (U i)] (U_cover : is_cover U)
  -- U i is isomorphic to Spa(A_i,A_i^+) with A_i a perfectoid ring
  (A : γ  Huber_pair) (is_perfectoid :  i, perfectoid_ring (A i) p),
   i, is_preadic_space_equiv {x : X // x  (U i)} (Spa (A i))    )

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 08:45):

doesn't quite typecheck

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 08:46):

but once it does it's very readable if you already know pretty much what a perfectoid space is

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 08:46):

adic_space full of sorries

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 08:46):

I am in the middle of writing some long issues explaining exactly what needs to be done to finish the job, plus references

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 08:47):

is_preadic_space_equiv extends homeo -- did you get that into mathlib?

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 08:50):

The problem, by the way, is failed to synthesize ⊢ preadic_space {x // x ∈ U i}

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 08:50):

instance preadic_space_restriction {X : Type} [preadic_space X] {U : set X} [is_open U] : preadic_space {x : X // x ∈ U} := sorry

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 08:52):

so all the ingredients are there -- a proof that U i is open, an instance saying an open subspace of a preadic space is a preadic space, oh and adic_space extends preadic_space

view this post on Zulip Assia Mahboubi (Jun 05 2018 at 08:54):

The ∃ {γ : Type} looks very suspicious to me. Is it really what you want? And not a set of some type?

view this post on Zulip Scott Morrison (Jun 05 2018 at 08:58):

@Assia Mahboubi , could you explain why it looks suspicious? I've seen the same sentiment expressed about similar things, but never really understood how you decide between indexing by a type, and having a set of things. The one time I tried both approaches (defining a Grothendieck topology), it eventually became clear that the set approach was smoother, but I didn't really grok why that was the case.

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 08:58):

This is supposed to say "my topological space has a cover by nice topological subspaces"

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 08:58):

but the actual cover is not part of the structure

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 08:59):

it's just the fact that such a cover exists

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 08:59):

for each i : gamma I need an open set U_i and a ring A_i and an isomorphism Spa(A_i) = U_i

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 09:00):

Here's a MWE of my final problem

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 09:01):

import analysis.topology.topological_space

attribute [class] is_open

class preadic_space (X : Type) extends topological_space X

class adic_space (X : Type) extends preadic_space X

structure Huber_pair : Type

definition Spa (A : Huber_pair) : Type := sorry

instance Spa_topology (A : Huber_pair) : topological_space (Spa A) := sorry

structure preadic_space_equiv (X Y : Type) [AX : preadic_space X] [AY : preadic_space Y] extends equiv X Y

definition is_preadic_space_equiv (X Y : Type) [AX : preadic_space X] [AY : preadic_space Y] :=
  nonempty (preadic_space_equiv X Y)

structure not_perfectoid_space (X : Type) (p : ) extends adic_space X :=
(perfectoid_cover :
  -- gamma is our indexing set, U_i are the open cover for i in gamma
   {γ : Type} (U : γ  set X) [U_open :  i, is_open (U i)]
  (A : γ  Huber_pair),
   i, is_preadic_space_equiv {x : X // x  (U i)} (Spa (A i)))

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 09:01):

I might have just made a stupid mistake

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 09:03):

oh ignore all this I am sure I have made a stupid mistake -- my error is somewhere else now in the MWE. I just need to sort this out myself. I think I'm there but just being stupid

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 09:04):

import analysis.topology.topological_space

attribute [class] is_open

class preadic_space (X : Type) extends topological_space X

class adic_space (X : Type) extends preadic_space X

structure Huber_pair : Type

definition Spa (A : Huber_pair) : Type := sorry

instance Spa_topology (A : Huber_pair) : topological_space (Spa A) := sorry

instance (A : Huber_pair) : preadic_space (Spa A) := sorry

structure preadic_space_equiv (X Y : Type) [AX : preadic_space X] [AY : preadic_space Y] extends equiv X Y

definition is_preadic_space_equiv (X Y : Type) [AX : preadic_space X] [AY : preadic_space Y] :=
  nonempty (preadic_space_equiv X Y)

structure not_perfectoid_space (X : Type) (p : ) extends adic_space X :=
(perfectoid_cover :
  -- gamma is our indexing set, U_i are the open cover for i in gamma
   {γ : Type} (U : γ  set X) [U_open :  i, is_open (U i)]
  (A : γ  Huber_pair),
   i, is_preadic_space_equiv {x : X // x  (U i)} (Spa (A i)))

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 09:04):

failed to synthesize type class instance for ⊢ preadic_space {x // x ∈ U i}

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 09:04):

That's my problem

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 09:05):

I think maybe type class inference doesn't know U i is open

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 09:05):

but I thought that [U_open : ∀ i, is_open (U i)] would tell it this

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 09:06):

but it might all be happening too quickly for type class inference

view this post on Zulip Chris Hughes (Jun 05 2018 at 09:06):

Is it because you should be using a coercion to subtype instead of this {x // x ∈ U i}

view this post on Zulip Assia Mahboubi (Jun 05 2018 at 09:13):

@Scott Morrison : disclaimer: I do not know what Groethendick topology is. But it is much more difficult to "combine" things which have different types. For instance, if two families are indexed using two a priori distinct types, then in order to speak about the family obtained as the union of these two, you always first have to craft a new type for the indices of this union, which will be something like the sum type of the two previous index types (phew). As opposed to offering the option, when possible, to use the union set of two sets (indexed with the same nature of datas, ie. with sets of a same type).

view this post on Zulip Johan Commelin (Jun 05 2018 at 09:17):

This is supposed to say "my topological space has a cover by nice topological subspaces"

You could consider U\mathcal{U} a subset of the powerset of X, and then demand for every U : calU that it is open, and that calU is a cover.

view this post on Zulip Johan Commelin (Jun 05 2018 at 09:18):

I guess that is_cover is something you defined yourself. I didn't find it in mathlib.

view this post on Zulip Johan Commelin (Jun 05 2018 at 09:20):

@Assia Mahboubi But with indexing sets you usually don't want to take the union (in some ambient set) right? You would want to take the disjoint union. And the mathematician in me doesn't really see why disjoint unions or sum types differ in complexity. Please enlighten this DTT newbie (-;

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 09:28):

instance preadic_space_restriction {X : Type} [preadic_space X] {U : set X} [is_open U] :
  preadic_space {x : X // x  U} := sorry

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 09:31):

import analysis.topology.topological_space

attribute [class] is_open

class preadic_space (X : Type) extends topological_space X

class adic_space (X : Type) extends preadic_space X

structure Huber_pair : Type

definition Spa (A : Huber_pair) : Type := sorry

instance Spa_topology (A : Huber_pair) : topological_space (Spa A) := sorry

instance (A : Huber_pair) : preadic_space (Spa A) := sorry

structure preadic_space_equiv (X Y : Type) [AX : preadic_space X] [AY : preadic_space Y] extends equiv X Y

definition is_preadic_space_equiv (X Y : Type) [AX : preadic_space X] [AY : preadic_space Y] :=
  nonempty (preadic_space_equiv X Y)

instance preadic_space_restriction {X : Type} [preadic_space X] {U : set X} [is_open U] :
  preadic_space {x : X // x  U} := sorry

structure test (X : Type) extends adic_space X :=
(loc:  (U : set X) [U_open : is_open U] (A : Huber_pair),
  is_preadic_space_equiv {x : X // x  U} (Spa (A)))  -- fails ⊢ preadic_space {x // x ∈ U}

view this post on Zulip Johan Commelin (Jun 05 2018 at 09:31):

Kevin, isn't there some coercion that turns U into a (sub)type? Because {x : X // x ∈ U} is really weird to a mathematician. (I understand that you are having troubles here... but I think we should aim to get rid of that expression in the end.)

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 09:33):

We can't have everything

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 09:34):

import analysis.topology.topological_space

attribute [class] is_open

class preadic_space (X : Type) extends topological_space X

class adic_space (X : Type) extends preadic_space X

structure Huber_pair : Type

definition Spa (A : Huber_pair) : Type := sorry

instance Spa_topology (A : Huber_pair) : topological_space (Spa A) := sorry

instance (A : Huber_pair) : preadic_space (Spa A) := sorry

structure preadic_space_equiv (X Y : Type) [AX : preadic_space X] [AY : preadic_space Y] extends equiv X Y

definition is_preadic_space_equiv (X Y : Type) [AX : preadic_space X] [AY : preadic_space Y] :=
  nonempty (preadic_space_equiv X Y)

instance preadic_space_restriction {X : Type} [preadic_space X] {U : set X} [is_open U] :
  preadic_space U := sorry

structure test (X : Type) extends adic_space X :=
(loc:  (U : set X) [U_open : is_open U] (A : Huber_pair),
  is_preadic_space_equiv U (Spa (A)))  -- fails ⊢ preadic_space ↥U

view this post on Zulip Johan Commelin (Jun 05 2018 at 09:35):

Right, so the issue remains...

view this post on Zulip Johan Commelin (Jun 05 2018 at 09:35):

Which is really annoying.

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 09:37):

Now we have weird arrows

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 09:37):

I'm sure it can be fixed. The only reason I'm chatting about this at all is that Patrick wanted to know what was going on

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 09:37):

It would be a shame to have to start going on about letI or whatever

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 09:37):

My problem, i now realise, is that whilst Mario showed me how to overcome various typeclass inference issues in the schemes project

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 09:38):

I don't actually understand what is going on

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 09:38):

I don't understand what the "type class inference machine" has access to at any time

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 09:38):

For example I am not even sure if it knows X is an adic space

view this post on Zulip Johan Commelin (Jun 05 2018 at 09:41):

Kevin, the first lines of the error are:

failed to synthesize type class instance for
X : Type,
to_adic_space : adic_space X,
to_preadic_space : (λ {X : Type} (c : adic_space X), preadic_space X) to_adic_space := adic_space.to_preadic_space X,

That last line shows how to turn X into a preadic_space.

view this post on Zulip Johan Commelin (Jun 05 2018 at 09:41):

But it hasn't actually done it!

view this post on Zulip Johan Commelin (Jun 05 2018 at 09:42):

Maybe if that term was actually an instance, then the machine would do the rest for you.

view this post on Zulip Johan Commelin (Jun 05 2018 at 09:46):

Hmm, no. Because if I change the class of X to adic_space in preadic_space_restriction, then it still fails in test.

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 10:07):

It's very easy to get Lean to say things like "I know X : Y and type class inference is failing to find anything of type Y"

view this post on Zulip Johan Commelin (Jun 05 2018 at 10:49):

Do we know of any strategy for attacking this issue? Or should we wait 3 weeks till Mario and Johannes are back?

view this post on Zulip Johan Commelin (Jun 05 2018 at 11:05):

structure test (X : Type) extends adic_space X :=
(loc:  (U : set X) [U_open : is_open U] (A : Huber_pair),
  @is_preadic_space_equiv U (Spa (A)) (@preadic_space_restriction _ _ U U_open) _)

The trouble is with U_open. If I replace that with an _, then typeclass inference can't figure it out itself...

view this post on Zulip Johan Commelin (Jun 05 2018 at 11:10):

--failed to synthesize type class instance for
 _root_.is_open U

Is _root_ a pointer to the trouble?

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 11:26):

Maybe. Kenny pointed this out to me too. There's a long typeclass thread which might solve my problems.

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 11:27):

Kenny suggested making another typeclass for subtypes being open

view this post on Zulip Johan Commelin (Jun 05 2018 at 11:28):

I don't see why that would fix things...

view this post on Zulip Johan Commelin (Jun 05 2018 at 11:28):

The stupid system is looking in the root namespace for an instance of is_open U, but it should just look 2 lines up in the local context...

view this post on Zulip Johan Commelin (Jun 05 2018 at 11:29):

It feels very much like a bug to me. (Wait. I'll first run this with pp.all set to true.)

view this post on Zulip Johan Commelin (Jun 05 2018 at 11:33):

Ok, so this is another (ugly) way to get it to work.

structure test (X : Type) extends adic_space X :=
(loc:  (U : set X) [U_open : @_root_.is_open.{0} X _ U] (A : Huber_pair),
  is_preadic_space_equiv U (Spa (A)))

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 11:34):

I doubt it's a bug.

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 11:34):

It's probably just how typeclass inference works

view this post on Zulip Johan Commelin (Jun 05 2018 at 11:34):

Yes, I also think that now.

view this post on Zulip Johan Commelin (Jun 05 2018 at 11:35):

So, what the heck is the difference between @_root_.is_open.{0} X _ U and is_open U?

view this post on Zulip Johan Commelin (Jun 05 2018 at 11:39):

One more golf (@Kevin Buzzard):

structure test (X : Type) extends adic_space X :=
(loc:  (U : set X) [U_open : _root_.is_open U] (A : Huber_pair),
  is_preadic_space_equiv U (Spa (A)))

view this post on Zulip Johan Commelin (Jun 05 2018 at 11:40):

So it really is about this _root_ thingy. But at least now it looks somewhat readable again.

view this post on Zulip Johan Commelin (Jun 05 2018 at 11:41):

Of course a mathematician (like me!) doesn't know at all what _root_ means, or what it is doing there. But hey! Cargo cult proofs for the win (-;

view this post on Zulip Gabriel Ebner (Jun 05 2018 at 11:45):

The problem is that is_open refers to two things here: the inherited field topological_space.is_open and the global definition _root_.is_open, which are different.

view this post on Zulip Johan Commelin (Jun 05 2018 at 11:46):

Aah, because of a long chain of extends, right?

view this post on Zulip Johan Commelin (Jun 05 2018 at 11:47):

Right, that makes a lot (a whole lot!) of sense

view this post on Zulip Johan Commelin (Jun 05 2018 at 11:47):

It has been staring us right in the face, all the time.

view this post on Zulip Johan Commelin (Jun 05 2018 at 11:47):

So it is just some stupid overloading, and preferably one of the two is_opens should have another name.

view this post on Zulip Johan Commelin (Jun 05 2018 at 11:56):

Anyway, @Gabriel Ebner thanks for enlightening me!

view this post on Zulip Johan Commelin (Jun 05 2018 at 11:57):

@Kevin Buzzard 'nother problem solved. Next!

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 11:58):

Definition currently looks like this:

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 11:58):

structure perfectoid_space (X : Type) (p : ) [is_prime p] extends adic_space X :=
(perfectoid_cover :
  -- gamma is our indexing set, U_i are the open cover for i in gamma
   {γ : Type} (U : γ  set X) [Uopen :  i, @_root_.is_open X _ (U i)] (U_cover : is_cover U)
  -- U i is isomorphic to Spa(A_i,A_i^+) with A_i a perfectoid ring
  (A : γ  Huber_pair) (is_perfectoid :  i, perfectoid_ring (A i) p),
   i, is_preadic_space_equiv {x : X // x  (U i)} (Spa (A i))    )

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 11:59):

Typechecks fine

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 11:59):

The is_open overloading is one thing

view this post on Zulip Johan Commelin (Jun 05 2018 at 11:59):

I guess you can remove the @ and the X _

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 11:59):

yes

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 12:00):

thanks

view this post on Zulip Johan Commelin (Jun 05 2018 at 12:00):

And just a (U i) on the last line? Instead of all the {x ... }

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 12:03):

structure perfectoid_space (X : Type) (p : ) [is_prime p] extends adic_space X :=
(perfectoid_cover :
  -- gamma is our indexing set, U_i are the open cover for i in gamma
   {γ : Type} (U : γ  set X) [Uopen :  i, _root_.is_open (U i)] (U_cover : is_cover U)
  -- U i is isomorphic to Spa(A_i,A_i^+) with A_i a perfectoid ring
  (A : γ  Huber_pair) (is_perfectoid :  i, perfectoid_ring (A i) p),
   i, is_preadic_space_equiv (U i) (Spa (A i))    )

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 12:03):

I'm not happy with that _root_ but everything else is great

view this post on Zulip Johan Commelin (Jun 05 2018 at 12:03):

Yes, completely agree.

view this post on Zulip Johan Commelin (Jun 05 2018 at 12:03):

We should just overhaul the definition in topological_space.lean

view this post on Zulip Johan Commelin (Jun 05 2018 at 12:04):

It's only a silly namespacing issue.

view this post on Zulip Johan Commelin (Jun 05 2018 at 12:04):

I it has a field open_subsets instead of is_open, then we're fine.

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 12:05):

can I fix this by writing my own open or is_open' or whatever?

view this post on Zulip Reid Barton (Jun 05 2018 at 12:06):

Probably even notation `is_open` := _root_.is_open would work

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 12:06):

Here's the full file

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 12:06):

import adic_space

--notation
postfix `` : 66 := power_bounded_subring

/-- A perfectoid ring, following Fontaine Sem Bourb-/
class perfectoid_ring (R : Type) (p : ) [is_prime p] extends Tate_ring R :=
(is_complete : complete R)
(is_uniform  : uniform R)
(ramified    :  ω : R , (is_pseudo_uniformizer ω)  (ω ^ p  p))
(Frob        :  a : R ,  b : R , (p : R )  (b ^ p - a))

structure perfectoid_space (X : Type) (p : ) [is_prime p] extends adic_space X :=
(perfectoid_cover :
  -- gamma is our indexing set, U_i are the open cover for i in gamma
   {γ : Type} (U : γ  set X) [Uopen :  i, _root_.is_open (U i)] (U_cover : is_cover U)
  -- U i is isomorphic to Spa(A_i,A_i^+) with A_i a perfectoid ring
  (A : γ  Huber_pair) (is_perfectoid :  i, perfectoid_ring (A i) p),
   i, is_preadic_space_equiv (U i) (Spa (A i))    )

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 12:07):

I am really happy with all of it apart from the _root_

view this post on Zulip Reid Barton (Jun 05 2018 at 12:07):

Some mathlib classes have the actual field name with a trailing ' to avoid this kind of collision

view this post on Zulip Reid Barton (Jun 05 2018 at 12:08):

except now I can't find any

view this post on Zulip Johan Commelin (Jun 05 2018 at 13:18):

can I fix this by writing my own open or is_open' or whatever?

Sure, but you would also need all the simp-lemmas etc. That's why I suggested we might as well overhaul topological_space.lean.

view this post on Zulip Johan Commelin (Jun 05 2018 at 13:20):

And we have 6 commits! The game is on!

view this post on Zulip Johan Commelin (Jun 05 2018 at 13:41):

@Kevin Buzzard What is your git workflow for this repo? fork -> feature branch -> push? Or just write access for everyone interested?

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 14:19):

Yeah, it should run. I have absolutely no idea about git workflows.

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 14:21):

I guess I do understand the question. For the stacks project I just let Kenny push anything -- I gave him write access. But for mathlib I have to do that fork feature push thing.

view this post on Zulip Johan Commelin (Jun 05 2018 at 15:11):

Ok, so this is your chance to level-up in git!

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 16:00):

Next job is the roadmap. I'll hopefully do this this evening (some issues explaining what needs to be done). Basically it's "type in a bunch of stuff from Wedhorn's paper"

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 16:00):

Kenny did chapter 1 but I'm sitting on it because it needs some non-mathlib imports

view this post on Zulip Johan Commelin (Jun 05 2018 at 16:56):

I like it that you moved the _root_ issue out of the perfectoid file

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:00):

I'm sorry I missed this early fight. I was busy with administration all day (including writing letter to Jean-Pierre Serre explaining how to come to our new math building next week).

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:01):

Is there a reason why perfectoid_spaces.lean is not inside the src directory?

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:02):

Yeah, it should run. I have absolutely no idea about git workflows.

Did you try using https://github.com/jlord/git-it-electron to learn? I never tried but it seems to be popular

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:16):

Why not using ϖ (\varpi)?

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:16):

Here it looks ugly but in my VScode it looks ok

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:18):

Why the space in R ᵒ? It works fine and looks better as Rᵒ

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:18):

I'm such an expert about perfectoid spaces now...

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:19):

Is instance subring_to_ring (R : Type) : has_coe (power_bounded_subring R) R := ⟨subtype.val⟩ meant to be useful right now? Deleting it changes nothing

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:27):

Is there any reason to use gamma instead of iota for the indexing type?

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 19:27):

no

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:27):

iota is the mathlib tradition, and consistent with using i as a variable name

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 19:27):

OK

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:27):

I guess the thing is never named in math papers

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 19:27):

I can change all these things. Thanks for the review!

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:28):

Now, serious question:

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 19:28):

Ri\coprod R_i

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 19:28):

who needs a name for the index set

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 19:28):

maybe I'll call it _

view this post on Zulip Mario Carneiro (Jun 05 2018 at 19:28):

You should not use existential quantification over Type in your definition

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 19:28):

eew

view this post on Zulip Mario Carneiro (Jun 05 2018 at 19:28):

for the index set

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 19:28):

Is this the thing Assia was also unhappy about?

view this post on Zulip Mario Carneiro (Jun 05 2018 at 19:28):

Yes

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:28):

What about this strange way of putting things before and after the existential comma?

view this post on Zulip Mario Carneiro (Jun 05 2018 at 19:29):

It will needlessly push up the universe level of the definition

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 19:29):

How do you do it then?

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:29):

And why naming instance implicit variables you don't use in the def?

view this post on Zulip Reid Barton (Jun 05 2018 at 19:29):

Even though it's inside an \ex?

view this post on Zulip Mario Carneiro (Jun 05 2018 at 19:29):

Instead you should quantify over all families that could possibly matter

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:29):

What about:

structure perfectoid_space (X : Type) (p : ) [is_prime p] extends adic_space X :=
(perfectoid_cover :
  -- gamma is our indexing set, U_i are the open cover for i in gamma
   (ι : Type) (U : ι  set X) [ i, is_open (U i)]
  -- U i is isomorphic to Spa(A_i,A_i^+) with A_i a perfectoid ring
  (A : ι  Huber_pair) [ i, perfectoid_ring (A i) p],
  (is_cover U)   i, is_preadic_space_equiv (U i) (Spa (A i)))

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:29):

Does it make any difference (what I wrote vs Kevin's version)?

view this post on Zulip Mario Carneiro (Jun 05 2018 at 19:30):

oh, actually reid you're right, impredicativity makes it okay

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:30):

Note that all data and instance implicit stuff is left of comma, and conditions are right of comma

view this post on Zulip Mario Carneiro (Jun 05 2018 at 19:30):

Still, I would prefer to quantify over subsets of set X

view this post on Zulip Gabriel Ebner (Jun 05 2018 at 19:30):

Maybe you should make ι a field of perfectoid_space (and the others as well).

view this post on Zulip Mario Carneiro (Jun 05 2018 at 19:31):

unless there is a reason that having many duplicates adds power?

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:31):

What Gabriel says was my next question

view this post on Zulip Reid Barton (Jun 05 2018 at 19:31):

There are a lot of equivalent ways one could write this definition, but this way matches the way we speak

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:32):

I agree it looks more mathematicial, I'm asking if this will bring pain

view this post on Zulip Mario Carneiro (Jun 05 2018 at 19:32):

alternatively, name the thing "perfectoid cover" or something and existentially quantify in the structure

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:32):

^ also sounds nice

view this post on Zulip Mario Carneiro (Jun 05 2018 at 19:32):

i.e. define what is a perfectoid cover and define a perfectoid space to be one which has a cover

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:33):

But again it would sound further away from math-speak

view this post on Zulip Johan Commelin (Jun 05 2018 at 19:33):

It think having the cover be a term of type set (set X) is not "un-mathematical". Except for the fact that we would call set X something like subset_of X.

view this post on Zulip Mario Carneiro (Jun 05 2018 at 19:33):

or "powerset"

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 19:34):

My definition is readable by mathematicians

view this post on Zulip Mario Carneiro (Jun 05 2018 at 19:34):

In fact, in math usually open covers are defined to be subsets of the collection of open sets

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 19:34):

and I don't understand what the problem with it is yet

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:34):

This thing with the indexing set makes it look like some kind of étale covering but it's actually a honest covering, right?

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 19:35):

I have an exotic construction "Spa" which basically takes a ring and spits out a "special" topological space

view this post on Zulip Reid Barton (Jun 05 2018 at 19:35):

The thing is that often one has some auxiliary data attached to each member of the cover, and then indexing the set with the set itself is awkward (what if the other data is not a function of the set)

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 19:35):

and the claim is that my perfectoid space has a covering by these "special" spaces

view this post on Zulip Mario Carneiro (Jun 05 2018 at 19:35):

that's the theorem

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:35):

What Reid wrote seems important to me

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 19:35):

@Patrick Massot yes it's just an honest covering of a topological space by open subsets

view this post on Zulip Mario Carneiro (Jun 05 2018 at 19:35):

It's good to know that you only "need" to talk about small things in the definition and prove that you can do it even for large families

view this post on Zulip Reid Barton (Jun 05 2018 at 19:36):

@Patrick Massot, did you ever write down a definition of manifold?
Even if it is just parameterized on a variable (i.e., not yet defined) notion of "smooth" maps of R^n, it might be an interesting exercise.

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 19:36):

Maybe you should make ι a field of perfectoid_space (and the others as well).

The covering and the set indexing the covering are not part of the data of a perfectoid space.

view this post on Zulip Mario Carneiro (Jun 05 2018 at 19:36):

Even if you quantify over type 0 in the definition, you might want a family in type 1 and then you have a theorem to prove anyway

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 19:36):

A perfectoid space is a space for which such a cover exists

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:37):

No I'm stuck in type class loops, out_param hell when I try to put a norm on R^n

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:37):

But indeed I could try to write the definition sorrying the definition of diffeomorphisms between open subsets of R^ n

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 19:37):

I understood everything Patrick said but I'm having trouble with these CS objections about iota. Can someone suggest something which you'd be happy with but which is the same idea and which is still readable by mathematicians?

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:38):

Note that my version of perfectoid_space quoted above is a variation in a direction orthogonal to this question of iota vs subsets

view this post on Zulip Mario Carneiro (Jun 05 2018 at 19:39):

just use U : set (opens X)

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 19:39):

i.e. define what is a perfectoid cover and define a perfectoid space to be one which has a cover

Aah I do understand this

view this post on Zulip Reid Barton (Jun 05 2018 at 19:40):

for more readability, it should probably be more like cover : set (opens X)

view this post on Zulip Reid Barton (Jun 05 2018 at 19:40):

Oh wait, you already have an example of the issue I was bringing up earlier here.

view this post on Zulip Reid Barton (Jun 05 2018 at 19:41):

We also have this (A : ι → Huber_pair) [∀ i, perfectoid_ring (A i) p] stuff

view this post on Zulip Mario Carneiro (Jun 05 2018 at 19:41):

BTW I think the p should come first

view this post on Zulip Mario Carneiro (Jun 05 2018 at 19:41):

because it's the parameter

view this post on Zulip Gabriel Ebner (Jun 05 2018 at 19:42):

The covering and the set indexing the covering are not part of the data of a perfectoid space.

Existentials are problematic since you'll have to use choice to access them, and in general you won't get the data back that you used to construct the perfectoid space in the first place. If you make them fields, then you can actually get back the Huber pair A that you used to construct the perfectoid space---just via definitional reduction.

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:43):

He doesn't want to get it back

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:43):

It's not part of the structure

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 19:51):

for more readability, it should probably be more like cover : set (opens X)

and now I need a Huber Pair for each element of the cover

view this post on Zulip Johan Commelin (Jun 05 2018 at 19:52):

What about Reid's concern? That we are not only indexing open subsets, but also other stuff with the same indexing set/type?

view this post on Zulip Reid Barton (Jun 05 2018 at 19:52):

I think in this case, you could write something like "there exists a set of open subsets which cover X and for each of these subsets, a Huber pair" such that ...". But there is a small subtlety here, in that the original definition allows you to choose the same open subset repeatedly with different Huber pairs. Here, there's no reason why you would want to do that, so it ends up not mattering.

view this post on Zulip Reid Barton (Jun 05 2018 at 19:52):

But if you try to define a smooth manifold, you cannot begin "there exists a set of open subsets which cover M and for each of these subsets, a continuous function to R^n such that ..."

view this post on Zulip Mario Carneiro (Jun 05 2018 at 19:52):

that's what makes the theorem not completely trivial

view this post on Zulip Johan Commelin (Jun 05 2018 at 19:53):

But if you try to define a smooth manifold, you cannot begin "there exists a set of open subsets which cover M and for each of these subsets, a continuous function to R^n such that ..."

Huh, why not?

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:53):

theorem claiming this doesn't matter?

view this post on Zulip Mario Carneiro (Jun 05 2018 at 19:53):

right

view this post on Zulip Reid Barton (Jun 05 2018 at 19:53):

Or, maybe you can?

view this post on Zulip Mario Carneiro (Jun 05 2018 at 19:54):

that given the definition using sets of opens you can recover the version with families indexed in an arbitrary type

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:54):

Huh, why not?

Because it wouldn't be correct

view this post on Zulip Reid Barton (Jun 05 2018 at 19:54):

but it's not the usual definition of an atlas, since there you can have multiple charts on the same open but with different coordinates

view this post on Zulip Mario Carneiro (Jun 05 2018 at 19:54):

but in general you should try to minimize your domain of quantification to something which is somehow bounded by the original input data

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:54):

You can build exotic spheres by gluing two open balls

view this post on Zulip Mario Carneiro (Jun 05 2018 at 19:55):

if you don't, this is when mathematicians have to write "chapter 4" or whatever on ZFC embedding subtleties

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:55):

All the exotictness is in the gluing map

view this post on Zulip Mario Carneiro (Jun 05 2018 at 19:55):

in the manifold case, I'm sure you can bound it by all the ways that maps can possibly fit together

view this post on Zulip Reid Barton (Jun 05 2018 at 19:56):

isn't it kind of a moot point anyways, since we are also asking for these Huber pairs, which also contain types?

view this post on Zulip Mario Carneiro (Jun 05 2018 at 19:57):

maybe the Huber pairs can't get that large either

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:57):

in the manifold case the atlas is a set of pairs (U_i, f_i) where U_i is an open set and f_i is a homeomorphism from U_i to some open set in R^n.

view this post on Zulip Reid Barton (Jun 05 2018 at 19:57):

I totally agree that if you find yourself with something that looks like a perfectoid space, but the indexing family is large, then it's a nontrivial theorem to show that you actually have a genuine perfectoid space

view this post on Zulip Patrick Massot (Jun 05 2018 at 19:58):

anyway, let's focus on the perfectoid case

view this post on Zulip Mario Carneiro (Jun 05 2018 at 19:58):

I'm sort of speculating here, but really if you need all that extra indexing power, then the definition is probably not correct anyway because then Type is probably not enough

view this post on Zulip Mario Carneiro (Jun 05 2018 at 19:59):

it's an arbitrary stopping point in the ZFC world

view this post on Zulip Patrick Massot (Jun 05 2018 at 20:00):

Kevin disappeared. Maybe he suddenly realized Scholze's perfectoid business makes no sense at all because of this issue

view this post on Zulip Johan Commelin (Jun 05 2018 at 20:02):

Ok, I don't know enough about manifolds. (They are weird, because they aren't defined as locally ringed spaces with some property.) But in the scheme case (and I think also in the perfectoid case) it should be fine to just work with a set of opens. Every point has an affine neighbourhood. That is what you need/want. Or am I messing up?

view this post on Zulip Johan Commelin (Jun 05 2018 at 20:04):

Nevertheless, if we use a set of opens, I don't know if that is a pretty thing to use as indexing set for the Huber pairs, and other data indexed on it. It might lead to ugly formalisation, it might lead to "un-mathematical" code. I really don't know.

view this post on Zulip Patrick Massot (Jun 05 2018 at 20:04):

You can define smooth manifolds as ringed space, see https://bookstore.ams.org/gsm-65

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 20:06):

I'm trying to do 10 things at once. I was hoping to get some work done tonight but my partner just got back from Canada and her sleeping patterns are in chaos; it might be bedtime.

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 20:07):

I am not sure that anyone has ever used a perfectoid space for which the index set is any bigger than countably infinite

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 20:07):

hmm

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 20:07):

maybe the size of the real numbers

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 20:08):

I can't imagine anything bigger. Mario's "chapter 4" reference is pertinent -- this is the same paper as the one I've taken the definition of perfectoid space from.

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 20:09):

maybe the Huber pairs can't get that large either

I am not sure there is a single object in this story that has size > 2^aleph_0

view this post on Zulip Johan Commelin (Jun 05 2018 at 20:16):

Which "chapter 4" are we referring to?

view this post on Zulip Patrick Massot (Jun 05 2018 at 20:16):

https://arxiv.org/abs/1709.07343

view this post on Zulip Johan Commelin (Jun 05 2018 at 20:17):

We should have a file/issue with references. Because now there is the diamonds paper, Fontaine's bourbaki notes, Wedhorn's notes...

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 20:17):

I have all these things as pdfs in my project directory but just didn't push them.

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 20:18):

Maybe some list of links on the README?

view this post on Zulip Johan Commelin (Jun 05 2018 at 20:19):

Yes, that should be fine.

view this post on Zulip Johan Commelin (Jun 05 2018 at 20:19):

I can PR the readme tomorrow

view this post on Zulip Reid Barton (Jun 05 2018 at 20:28):

Maybe make a separate repository with the pdfs, if you want to commit them somewhere. Then people don't have to download them if they don't want to

view this post on Zulip Patrick Massot (Jun 05 2018 at 20:40):

I don't see the point of hosting the pdf on github if they were taken from arXiv

view this post on Zulip Assia Mahboubi (Jun 05 2018 at 21:00):

It would also be great to have a "Getting it working" section in your README.

view this post on Zulip Reid Barton (Jun 05 2018 at 21:05):

I don't see the point of hosting the pdf on github if they were taken from arXiv

Agreed, I meant "better not to commit pdfs to the main repository, whether or not you host them elsewhere"

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 21:22):

It would also be great to have a "Getting it working" section in your README.

ha ha, I guess it currently doesn't work :-) (unless you allow sorrys). OK I'll write something about that in the README.

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 21:54):

It would also be great to have a "Getting it working" section in your README.

https://github.com/kbuzzard/lean-perfectoid-spaces/

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 21:55):

On my TODO list: (1) refactor definition of perfectoid space according to comments above, and move it into src (2) write a couple of issues explaining the details of what needs to be done to finish formalising the definition.

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 21:56):

Any comments / criticism / suggestions / anything -- I'd be happy to hear it. Once I've written the issues I will perhaps begin to circulate a link to the project amongst my mathematician chums

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 21:56):

And of course, many thanks to those who have already commented!

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 22:43):

boggle Every change I made bring new typeclass inference problems

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 22:44):

structure perfectoid_cover (p : ) [is_prime p] (X : Type) [adic_space X] :=
(𝓤 : set (set X))
[𝓤_open :  U  𝓤, is_open U]
(𝓤_cover :  x : X,  U  𝓤, x  U)
(𝓤_affinoid_perfectoid :  U  𝓤,
   (A : Huber_pair) (Aperf : perfectoid_ring p A), is_preadic_space_equiv U (Spa (A)))   )

view this post on Zulip Kenny Lau (Jun 05 2018 at 22:44):

𝓤

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 22:44):

and now I'm back with failing to synthesize ⊢ preadic_space ↥U

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 22:45):

𝓤

Collection of open sets

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 22:45):

except that Lean does not notice they're open

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 22:46):

instance preadic_space_restriction {X : Type} [preadic_space X] {U : set X} [@_root_.is_open X _ U] :
  preadic_space {x : X // x  U} := sorry

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 22:58):

I guess I really liked the idea of typeclass inference showing automatically that if X is some kind of nice top space (an adic space or perfectoid space) and U is an open subset then U inherits the niceness. I might just give up and spell it out.

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 23:04):

I've given up on typeclass inference because it's midnight.

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 23:05):

In the old version above, I had is_preadic_space_equiv (U i) (Spa (A i))

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 23:05):

and the preadic space structure on U i came from typeclass inference.

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 23:05):

I can't get it to work for U in some covering set

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 23:05):

but this works:

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 23:06):

-- definitions of adic_space, preadic_space, Huber_pair etc
import adic_space

--notation
postfix `` : 66 := power_bounded_subring

/-- A perfectoid ring, following Fontaine Sem Bourb-/
class perfectoid_ring (p : ) [is_prime p] (R : Type) extends Tate_ring R :=
(is_complete : complete R)
(is_uniform  : uniform R)
(ramified    :  ϖ : R, (is_pseudo_uniformizer ϖ)  (ϖ ^ p  p))
(Frob        :  a : R,  b : R, (p : R)  (b ^ p - a))

structure perfectoid_cover (p : ) [is_prime p] (X : Type) [adic_space X] :=
(𝓤 : set (set X))
[𝓤_open :  U  𝓤, is_open U]
(𝓤_cover :  x : X,  U  𝓤, x  U)
(𝓤_affinoid_perfectoid :  U  𝓤,  (A : Huber_pair) (Aperf : perfectoid_ring p A),
  is_preadic_space_equiv (preadic_space_pullback U) (Spa A)  )

class perfectoid_space (p : ) [is_prime p] (X : Type) extends adic_space X :=
(exists_perfectoid_cover : perfectoid_cover p X)

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 23:06):

preadic_space_pullback U is just U again :-) (actually it's {x : X // x \in U})

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 23:07):

but the instance can key on it

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 23:07):

I only half-know what those words mean

view this post on Zulip Kevin Buzzard (Jun 05 2018 at 23:07):

but type class inference works with this trick

view this post on Zulip Mario Carneiro (Jun 06 2018 at 01:25):

I said set (opens X) for a reason

view this post on Zulip Mario Carneiro (Jun 06 2018 at 01:26):

it's past time you had a opens X type of open subsets of X

view this post on Zulip Johan Commelin (Jun 06 2018 at 03:24):

I don't have Lean here, so there might be stupid typos. But how about something like this?

class perfectoid_space (p : ) [is_prime p] (X : Type) extends adic_space X :=
(perfectoid_cover :  x : X,  (U : opens X) (A : Huber_pair) (Aperf : perfectoid_ring p A),
  (x  U)  is_preadic_space_equiv U (Spa A))

view this post on Zulip Johan Commelin (Jun 06 2018 at 03:25):

That seems very readable to me. And I basically just squashed some lines together.

view this post on Zulip Johan Commelin (Jun 06 2018 at 06:45):

it's past time you had a opens X type of open subsets of X

@Mario Carneiro do you imagine something like this?

class opens (X : Type*) [topological_space X] :=
(U : set X)
(U_open : is_open U)

instance open_is_subset {X : Type*} [topological_space X] :
has_coe (opens X) (set X) := ⟨λU, U.U

view this post on Zulip Mario Carneiro (Jun 06 2018 at 07:10):

Yes. You will also want a has_mem A (opens A) instance

view this post on Zulip Mario Carneiro (Jun 06 2018 at 07:11):

You could also use subtype for the definition

view this post on Zulip Johan Commelin (Jun 06 2018 at 07:25):

Voila, another attempt.

section opens

variables (X : Type*) [t : topological_space X]
include X t

@[class] def opens := subtype (topological_space.is_open t)

instance : has_coe (opens X) (set X) := subtype.val

instance : has_mem X (opens X) := ⟨λx U, x  U.val

end opens

view this post on Zulip Mario Carneiro (Jun 06 2018 at 07:27):

It shouldn't make too much difference, but you should use is_open instead of topological_space.is_open

view this post on Zulip Johan Commelin (Jun 06 2018 at 07:32):

Done.

view this post on Zulip Johan Commelin (Jun 06 2018 at 07:33):

But I'm having type class inference issues with Kevin's latest code (that he posted above).

view this post on Zulip Johan Commelin (Jun 06 2018 at 07:33):

And it doesn't help if I change set (set X) to set (opens X).

view this post on Zulip Johan Commelin (Jun 06 2018 at 07:34):

Somehow Lean starts looking for an instance of has_coe_to_sort nat, and I have no idea why Lean would do that.

view this post on Zulip Johan Commelin (Jun 06 2018 at 07:42):

Never mind... error was between keyboard and chair.

view this post on Zulip Johan Commelin (Jun 06 2018 at 07:42):

-- definitions of adic_space, preadic_space, Huber_pair etc
import adic_space

--notation
postfix `` : 66 := power_bounded_subring

/-- A perfectoid ring, following Fontaine Sem Bourb-/
class perfectoid_ring (p : ) [is_prime p] (R : Type) extends Tate_ring R :=
(is_complete : complete R)
(is_uniform  : uniform R)
(ramified    :  ϖ : R, (is_pseudo_uniformizer ϖ)  (ϖ^p  p))
(Frob        :  a : R,  b : R, (p : R)  (b^p - a))

class perfectoid_space (p : ) [is_prime p] (X : Type) extends adic_space X :=
(perfectoid_cover :  x : X,  (U : opens X) (A : Huber_pair) [perfectoid_ring p A],
  (x  U)  is_preadic_space_equiv U (Spa A))

view this post on Zulip Johan Commelin (Jun 06 2018 at 07:43):

I think it would be really nice if we also made the [p : Prime] stuff work. I'll try to look into it.

view this post on Zulip Johan Commelin (Jun 06 2018 at 07:54):

Oh yes, I remember. That means that ϖ^p breaks. And we don't want up-arrows or p.val or the likes.

view this post on Zulip Mario Carneiro (Jun 06 2018 at 07:55):

Well, you can use [fixed_prime] plus fixed_prime.p to avoid the coercion stuff

view this post on Zulip Johan Commelin (Jun 06 2018 at 07:57):

Right, with your "hack" we get

-- definitions of adic_space, preadic_space, Huber_pair etc
import adic_space

--notation
postfix `` : 66 := power_bounded_subring

open nat.Prime
variable [nat.Prime] -- fix a prime p

/-- A perfectoid ring, following Fontaine Sem Bourb-/
class perfectoid_ring (R : Type) extends Tate_ring R :=
(is_complete : complete R)
(is_uniform  : uniform R)
(ramified    :  ϖ : R, (is_pseudo_uniformizer ϖ)  (ϖ^p  p))
(Frob        :  a : R,  b : R, (p : R)  (b^p - a))

class perfectoid_space (X : Type) extends adic_space X :=
(perfectoid_cover :  x : X,  (U : opens X) (A : Huber_pair) [perfectoid_ring A],
  (x  U)  is_preadic_space_equiv U (Spa A))

view this post on Zulip Johan Commelin (Jun 06 2018 at 07:57):

Look ma! No primes in our type signatures!

view this post on Zulip Johan Commelin (Jun 06 2018 at 07:58):

#check @perfectoid_space -- perfectoid_space : Π [_inst_1 : nat.Prime], Type → Type

view this post on Zulip Johan Commelin (Jun 06 2018 at 08:07):

@Kevin Buzzard Is there a reason why perfectoid_ring has hypothesis is_complete and is_uniform and also ramified. Why not is_ramified?

view this post on Zulip Kevin Buzzard (Jun 06 2018 at 08:08):

It's just random -- like in Lean. It's group but is_group_hom right?

view this post on Zulip Mario Carneiro (Jun 06 2018 at 08:08):

is_group_hom because that's a prop

view this post on Zulip Mario Carneiro (Jun 06 2018 at 08:09):

group is not

view this post on Zulip Kevin Buzzard (Jun 06 2018 at 08:09):

Aah!

view this post on Zulip Kevin Buzzard (Jun 06 2018 at 08:09):

So how about is_perfectoid_space

view this post on Zulip Kevin Buzzard (Jun 06 2018 at 08:09):

because it's an adic space plus some prop

view this post on Zulip Johan Commelin (Jun 06 2018 at 08:11):

I guess that makes sense. And similarly is_perfectoid_ring, and I guess is_ramified.

view this post on Zulip Johan Commelin (Jun 06 2018 at 08:12):

Hmmm, but group is also just a monoid with some props, right?

view this post on Zulip Kevin Buzzard (Jun 06 2018 at 08:15):

But maybe its type is not Prop

view this post on Zulip Kevin Buzzard (Jun 06 2018 at 08:15):

That's the distinction I think

view this post on Zulip Johan Commelin (Jun 06 2018 at 08:16):

Right, that makes sense. So then it is is_ramified, and the rest stays as it is.

view this post on Zulip Johan Commelin (Jun 06 2018 at 08:24):

@Kevin Buzzard Does it also make sense to call the last condition is_perfect instead of Frob?

view this post on Zulip Kevin Buzzard (Jun 06 2018 at 08:49):

If you search for "perfect ring" then you get ads for weddings

view this post on Zulip Kevin Buzzard (Jun 06 2018 at 08:50):

I thought Frobenius was bijective for a perfect ring, not surjective. What do you think?

view this post on Zulip Johan Commelin (Jun 06 2018 at 08:50):

Hmm, you are probably right

view this post on Zulip Johan Commelin (Jun 06 2018 at 08:51):

Bam! https://github.com/kbuzzard/lean-perfectoid-spaces/pull/1

view this post on Zulip Johan Commelin (Jun 06 2018 at 08:52):

@Kevin Buzzard Your first PR (-;

view this post on Zulip Kevin Buzzard (Jun 06 2018 at 08:52):

I've pushed Kenny's valuation stuff by the way (first chapter of Wedhorn)

view this post on Zulip Johan Commelin (Jun 06 2018 at 08:53):

And there is also https://github.com/jcommelin/lean-perfectoid-spaces/tree/opens

view this post on Zulip Kevin Buzzard (Jun 06 2018 at 08:53):

@Kevin Buzzard Your first PR (-;

One day when we have a gigantic maths brain that's taking over the universe, you'll be able to tell your children that you made the first PR.

view this post on Zulip Kevin Buzzard (Jun 06 2018 at 08:54):

if we decided to spare them

view this post on Zulip Johan Commelin (Jun 06 2018 at 08:54):

Which defines the opens class. And uses it in the perfectoid_space definition.

view this post on Zulip Johan Commelin (Jun 06 2018 at 08:56):

Kevin, should I also PR the opens stuff? Or do you not like that direction?

view this post on Zulip Kevin Buzzard (Jun 06 2018 at 08:56):

I said set (opens X) for a reason

I couldn't find opens in the topological space stuff so I left it and decided I should ask where it was later

view this post on Zulip Kevin Buzzard (Jun 06 2018 at 08:56):

it's past time you had a opens X type of open subsets of X

Ohh!

view this post on Zulip Johan Commelin (Jun 06 2018 at 09:01):

I see that @Kenny Lau made ker f a subset instead of a subtype. I really don't know when I should use which. Can someone clarify this for me?

view this post on Zulip Kenny Lau (Jun 06 2018 at 09:02):

you can coerce a subset to a subtype anytime

view this post on Zulip Kevin Buzzard (Jun 06 2018 at 09:02):

I can't. I'm constantly switching between them. I guess subsets are easier to work with

view this post on Zulip Kevin Buzzard (Jun 06 2018 at 09:02):

[I can't clarify, I can coerce]

view this post on Zulip Kevin Buzzard (Jun 06 2018 at 09:02):

Random screed by Hazewinkel claims perfect is bijective \lam x, x^p

view this post on Zulip Johan Commelin (Jun 06 2018 at 09:03):

Ok, so Frob it is. I already reverted it on my branch.

view this post on Zulip Patrick Massot (Jun 06 2018 at 10:39):

I don't understand https://github.com/kbuzzard/lean-perfectoid-spaces/blob/b1e6489145be504e64a009226c6811bfd84a5070/src/perfectoid_space.lean#L22 Why isn't there a here?

view this post on Zulip Patrick Massot (Jun 06 2018 at 10:40):

Do we have a roadmap saying which parts of Wedhorn are needed?

view this post on Zulip Johan Commelin (Jun 06 2018 at 10:58):

It is equivalent up to a choice, right?

view this post on Zulip Johan Commelin (Jun 06 2018 at 10:58):

And I think the roadmap is under construction.

view this post on Zulip Johan Commelin (Jun 06 2018 at 11:45):

Ooh, there is a tiny typo in subrel.lean. We need \alpha to be of type Type*. Without the * Kenny's code gets an error.

view this post on Zulip Kevin Buzzard (Jun 06 2018 at 12:13):

Do we have a roadmap saying which parts of Wedhorn are needed?

It's on the way

view this post on Zulip Kevin Buzzard (Jun 06 2018 at 12:13):

I keep trying to do everything

view this post on Zulip Kevin Buzzard (Jun 06 2018 at 12:13):

maybe I should post some basic info and then work on it more

view this post on Zulip Johan Commelin (Jun 06 2018 at 17:04):

Yes, some issues with basics would be totally fine.

view this post on Zulip Patrick Massot (Jun 06 2018 at 18:05):

I ran into Guy Henniart on the train this morning. I told him about schemes and perfectoid spaces in Lean, he was very interested. He told me proof assistants will probably be part of the future of mathematics and we should try to use this opportunity to tighten our links with the CS department, maybe hiring someone working on this.

view this post on Zulip Kenny Lau (Jun 06 2018 at 18:06):

@Kevin Buzzard

view this post on Zulip Kenny Lau (Jun 06 2018 at 18:06):

he proved local langland for GL(n) :o

view this post on Zulip Patrick Massot (Jun 06 2018 at 18:07):

Yes it's that level: stuff Scholze reproved when he was a 1st year undergrad

view this post on Zulip Patrick Massot (Jun 06 2018 at 18:07):

very impressive from Guy

view this post on Zulip Kenny Lau (Jun 06 2018 at 18:07):

"Une preuve simple des conjectures de Langlands pour GL(n) sur un corps p-adique"

view this post on Zulip Kenny Lau (Jun 06 2018 at 18:07):

"une preuve simple"

view this post on Zulip Kenny Lau (Jun 06 2018 at 18:08):

and one of my body parts is made of chicken

view this post on Zulip Reid Barton (Jun 06 2018 at 18:08):

maybe the proof has no nontrivial subproofs

view this post on Zulip Johan Commelin (Jun 06 2018 at 18:10):

Patrick, that's cool news! I really like it that people are enthusiastic about these formalisations. So far most people I encounter only shrug their shoulders...

view this post on Zulip Patrick Massot (Jun 06 2018 at 18:10):

It was also funny seeing him reacting when I said there would be riots if Scholze doesn't get his medal in Rio. He completely failed to picture how this could happen (Scholze not getting the medal).

view this post on Zulip Patrick Massot (Jun 06 2018 at 18:11):

Johan: yes, this is why I tell this story here. It was a pretty unusual reaction

view this post on Zulip Patrick Massot (Jun 06 2018 at 18:12):

Especially since Guy is from a generation that can barely use a computer to write an email

view this post on Zulip Patrick Massot (Jun 06 2018 at 18:12):

Next week I should try to ask Serre what he thinks about proof assistants

view this post on Zulip Johan Commelin (Jun 06 2018 at 18:12):

Trollolol

view this post on Zulip Kevin Buzzard (Jun 06 2018 at 18:18):

An algebraist in my department went to the Loeser conference last week and said that Hales had mentioned the schemes work in his talk. But I guess Hales is biased :-)

view this post on Zulip Johan Commelin (Jun 06 2018 at 18:20):

Ok, but this is only an encouragement that we really should get perfectoid spaces in Lean before Rio!

view this post on Zulip Patrick Massot (Jun 06 2018 at 18:21):

It looks like it's almost done

view this post on Zulip Johan Commelin (Jun 06 2018 at 18:21):

If Scholze showed some interest, and now Henniart...

view this post on Zulip Kenny Lau (Jun 06 2018 at 18:21):

who is Rio?

view this post on Zulip Johan Commelin (Jun 06 2018 at 18:31):

It looks like it's almost done

I guess you have to place quite a bit of emphasis on looks

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 19:41):

https://github.com/kbuzzard/lean-perfectoid-spaces/issues/3

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 19:42):

I had a good look through the maths last night and I don't see any major difficulties, but who knows.

view this post on Zulip Patrick Massot (Jun 07 2018 at 19:43):

"Page numbers are all for Huber's notes." I guess you meant Wedhorn?

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 19:43):

ooh thanks

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 19:43):

I do that a lot!

view this post on Zulip Patrick Massot (Jun 07 2018 at 19:44):

Lean 7 will tell you about such typos on Github

view this post on Zulip Patrick Massot (Jun 07 2018 at 19:48):

I'm not sure I understand the dependency graph

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 19:49):

I'm not surprised

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 19:49):

Should I explain it?

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 19:49):

In the issue, I mean?

view this post on Zulip Patrick Massot (Jun 07 2018 at 19:49):

It would help if you want help on this

view this post on Zulip Patrick Massot (Jun 07 2018 at 19:50):

Because currently it's not clear how the work could be divided

view this post on Zulip Patrick Massot (Jun 07 2018 at 19:51):

Is Spv(A) a typo or something different from Spa(A)?

view this post on Zulip Patrick Massot (Jun 07 2018 at 19:51):

Maybe v is valuation?

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 19:51):

something different

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 19:51):

I didn't make the notation

view this post on Zulip Patrick Massot (Jun 07 2018 at 19:51):

it appears only once in the issue

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 19:52):

It's an auxilary definition :-)

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 19:52):

I'll add some comments

view this post on Zulip Patrick Massot (Jun 07 2018 at 19:55):

Roughly, how many pages of Wedhorn are actually required for this definition of adic spaces?

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 20:05):

In retrospect I don't think that many.

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 20:06):

The hard work might be proving that an affinoid adic space is an adic space

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 20:06):

however

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 20:06):

that might be easier than proving that an affine scheme is a scheme

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 20:06):

because O_X is a sheaf on Spec(R)

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 20:06):

and the analogous fact for Spa(R) is not true

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 20:06):

so an affinoid adic space is Spa(R) for an R for which it is true

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 20:07):

Aah, I've got it

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 20:07):

The hard thing will be proving that an affinoid perfectoid space is a perfectoid space

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 20:07):

That will need far more stuff

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 20:10):

but we don't need to advertise that, right? ;-)

view this post on Zulip Patrick Massot (Jun 07 2018 at 20:11):

Is there any easier example of a perfectoid space?

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 20:12):

The empty space

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 20:12):

there is literally no simple example of a perfectoid space other than this

view this post on Zulip Patrick Massot (Jun 07 2018 at 20:12):

That's what I feared

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 20:12):

because the second simplest example is Spa(K,K^o) with K a perfectoid field

view this post on Zulip Patrick Massot (Jun 07 2018 at 20:12):

So we can't really escape that example

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 20:12):

well, at least it's a field

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 20:13):

Something like C_p, the completion of an algebraic closure of the p-adic numbers, is a relatively straightforward example of a perfectoid field

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 20:13):

don't worry, it's algebraically closed

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 20:13):

you don't have to go on forever

view this post on Zulip Patrick Massot (Jun 07 2018 at 20:13):

And if we want to prove any result about this definition, beyond having an example, is it super hard to prove that tilting thing?

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 20:13):

We number theorists tell people that C_p is our version of the complex numbers

view this post on Zulip Patrick Massot (Jun 07 2018 at 20:14):

Corollary 3.20 in the diamonds paper

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 20:14):

Oh yeah the tilting thing needs a whole bunch of commutative algebra

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 20:14):

almost etale extensions

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 20:14):

probably cotangent complex

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 20:14):

although actually maybe you could instead use my work with Verberkmoes

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 20:15):

a bunch of almost mathematics though

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 20:15):

derived categories

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 20:15):

yeah it would be a good challenge

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 20:15):

If you did that then serious people would get interested

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 20:16):

because that is like an odd order theorem but one that people are interested in

view this post on Zulip Patrick Massot (Jun 07 2018 at 20:17):

The proof is only two lines long in that diamonds paper: "The tilting process glues to give a functor X \maptos X^b . Theorem 3.13 globalizes to the following result." and the proof of Theorem 3.13 is "In [Sch12], these are only proved over a perfectoid field, but the proof works in general."

view this post on Zulip Patrick Massot (Jun 07 2018 at 20:18):

doesn't looks too bad

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 20:24):

Yes the work is tilting an affinoid perfectoid and...I guess writing down the definition of the tilt might not be so hard, come to think of it. It's proving that the space and its tilt have the same geometry that's hard

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 20:24):

A huge generalisation of Fontaine-Wintenberger and Faltings

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 20:30):

OK so I just looked at the paper (I'm travelling currently). The hard part is the equivalence, that is a lot of content. Maybe the definition of tilting might be possible.

view this post on Zulip Patrick Massot (Jun 07 2018 at 20:31):

Is there anything simpler but still significant that could be proved about those spaces?

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 22:07):

I guess one could prove that if A is perfectoid then Spa (A) is a perfectoid space. Scholze's original proof used tilting and a whole bunch of machinery. Verberkmoes and I found a much shorter direct proof. But doing basic stuff like defining perfectoids is the sort of thing we can do "in our spare time" -- formalising my paper would be a serious endeavour, although of course it's something I've considered. Most things in the area are impossibly hard or just very long. There are hundreds of pages by gabber and Romero that would be a joy to do but would take forever

view this post on Zulip Johan Commelin (Jun 08 2018 at 03:09):

I do think that it would be dissapointing if we have no examples at all... Defining tilting will be very nice PR I think. But it would be more 'honest' to first prove that Spa(A) is perfectoid (given that you have a proof without tilting).

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 06:47):

I think that most mathematicians will not really understand what is going on, and wouldn't know the difference between defining a perfectoid space and defining tilting. But I'd happily be proved wrong. There are two independent questions. The one I was interested in (and still am) is: "given that most of the non-trivial work doing maths on computers is of a Kepler conjecture / odd order theorem nature, i.e. hundreds of lemmas about relative simply things, are these programs even _capable_ of doing mathematics with non-trivial objects?"

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 06:47):

I now think they are. But there's a different question, which is much more complicated:

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 06:47):

how to get one non-trivial theorem about one non-trivial object into these systems?

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 06:47):

And that will cost time and money

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 06:48):

it's not just a "hobby project" like defining a perfectoid space

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 06:48):

I have 4.5 hours of meetings with the UK science funding council EPSRC today (it's one big reason that I couldn't go to Hanoi)

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 06:49):

and this will come up

view this post on Zulip Johan Commelin (Jun 08 2018 at 06:49):

Ok, good luck!

view this post on Zulip Johan Commelin (Jun 08 2018 at 06:49):

Sounds like today is an important day

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 06:49):

but if they're not interested then I don't quite know what happens next

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 06:49):

I guess I am more interested in hearing their thoughts about setting up something big

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 06:50):

and whether they'd encourage me to apply for funding

view this post on Zulip Johan Commelin (Jun 08 2018 at 06:58):

So, when does the meeting start? (Or rather, when will you be back to tell us about the good news :wink:?)

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 07:34):

I don't think any decisions will be made today!

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 07:34):

But there will be a chance to test the water.

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 07:52):

www.math.columbia.edu/~harris/otherarticles_files/perfectoid.pdf

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 07:52):

I hadn't been aware of this article until the other day

view this post on Zulip Johan Commelin (Jun 08 2018 at 07:55):

The introduction is really nice.

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 08:23):

[sorry, double post fail]

view this post on Zulip Johan Commelin (Jun 08 2018 at 10:30):

Kevin, do we even need the notion of Tate ring?

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 12:45):

Maybe not but it's pretty easy to formalise if you have everything else. A perfectoid ring is a Tate ring plus ...

view this post on Zulip Johan Commelin (Jun 08 2018 at 13:24):

If type class inference tries to turn an ideal into a module it starts looping to find a ring. Same issue that Patrick has I guess.

view this post on Zulip Patrick Massot (Jun 08 2018 at 13:28):

modules are very dangerous for type class resolution. I'm still waiting for Mario, Johannes and Sebastian to really solve this issue

view this post on Zulip Johan Commelin (Jun 08 2018 at 13:32):

Hmmz... we need finitely generated ideals. It would be very useful to have span from linear algebra. But then we need to treat an ideal as a module.

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 13:33):

If there are actual technical problem with modules being a typeclass then surely one solution is just to stop them being a typeclass?

view this post on Zulip Johan Commelin (Jun 08 2018 at 13:34):

And have all the code be utterly unreadable to mathematicians...

view this post on Zulip Johan Commelin (Jun 08 2018 at 13:34):

By the way, Kevin, are the meetings over yet? Were they receptive to your ideas/plans?

view this post on Zulip Johan Commelin (Jun 08 2018 at 13:38):

@Kevin Buzzard Is it ok to add https://github.com/johoelzl/mason-stother as dependency. Then we have univariate polynomials. And this is scheduled to go into mathlib anyway, so the dependecy would be temporary.

view this post on Zulip Johan Commelin (Jun 08 2018 at 14:14):

https://github.com/jcommelin/lean-perfectoid-spaces/tree/Huber_pair is a clumsy attempt to define Huber rings (up to the topological stuff).

view this post on Zulip Johan Commelin (Jun 08 2018 at 14:14):

But there is still a sorry to turn an ideal into a module.

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 19:12):

Money: I was encouraged to apply for it. Mason-Stothers -- is there a risk that we make this a dependency and then M-S gets PRed to mathlib and then stuff gets changed and then our code doesn't work? Or doesn't this matter?

view this post on Zulip Johan Commelin (Jun 08 2018 at 19:13):

Not so much... we really use very little of it. That part of the interface shouldn't change.

view this post on Zulip Johan Commelin (Jun 08 2018 at 19:14):

I can PR my subring branch into your repo if you want... it adds Mason-Stothers as dep.

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 19:14):

So then another question is: if we only use very little of it, is it best to just cut and paste a small part of it into our repo directly and then delete it later?

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 19:14):

I just have no idea how to run a project like this.

view this post on Zulip Johan Commelin (Jun 08 2018 at 19:15):

No, I would just go with the dependency.

view this post on Zulip Johan Commelin (Jun 08 2018 at 19:15):

And move on to interesting stuff (-;

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 19:15):

Ok then I'll add the dependency. Can it wait a day? Can you do it?

view this post on Zulip Johan Commelin (Jun 08 2018 at 19:15):

I did it.

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 19:15):

I have relatives here so I should go

view this post on Zulip Johan Commelin (Jun 08 2018 at 19:15):

Shall I PR?

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 19:15):

thanks

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 19:15):

yes please PR

view this post on Zulip Johan Commelin (Jun 08 2018 at 19:15):

Aaah, ok, see you later.

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 19:16):

I will look over it later. Assia suggested that I understand all the code I accept so I'd like to read through it before I accept it but I'm sure I will

view this post on Zulip Johan Commelin (Jun 08 2018 at 19:17):

Well, I'm a newbie... so maybe you want to improve little things...

view this post on Zulip Patrick Massot (Jun 08 2018 at 19:24):

Don't you think we should write a LaTeX file describing what has been formalized so far, and update it each time something is added? If we do this in real time it shouldn't be too painful. And I think it would be really useful. It could even include some comments about the formalization choices.

view this post on Zulip Patrick Massot (Jun 08 2018 at 19:25):

class normal_add_subgroup [add_group α] (s : set α) extends is_add_subgroup s : Prop := (normal : ∀ n ∈ s, ∀ g : α, g + n - g ∈ s) WTF?!

view this post on Zulip Johan Commelin (Jun 08 2018 at 19:26):

You can have tick boxes in Github issues, right?

view this post on Zulip Patrick Massot (Jun 08 2018 at 19:26):

Do perfectoid spaces include non commutative groups with additive notations?

view this post on Zulip Johan Commelin (Jun 08 2018 at 19:26):

That might be useful

view this post on Zulip Johan Commelin (Jun 08 2018 at 19:26):

I didn't write that file. I just copy-pasted it, and then find-replaced stuff to get additive versions.

view this post on Zulip Patrick Massot (Jun 08 2018 at 19:27):

But this bit is evil

view this post on Zulip Johan Commelin (Jun 08 2018 at 19:27):

I agree. I am just saying that I didn't actually read that part of the file.

view this post on Zulip Johan Commelin (Jun 08 2018 at 19:27):

I am still annoyed that I even had to do all that duplication.

view this post on Zulip Johan Commelin (Jun 08 2018 at 19:34):

Patrick, I think it might also be a good idea to have accompanying comments (like Kevin did in parts of the files).

view this post on Zulip Johan Commelin (Jun 08 2018 at 19:35):

That will help interested mathematicians to figure out what is going on.

view this post on Zulip Patrick Massot (Jun 08 2018 at 19:35):

Sure. Every documentation is good

view this post on Zulip Johan Commelin (Jun 08 2018 at 19:37):

Concerning the LaTeX-file, I think that's fine. But then maybe we shouldn't have issues as well. Otherwise we will have Zulip, issues, comments in the code, TeX-file,...

view this post on Zulip Johan Commelin (Jun 08 2018 at 19:37):

And then we get lost.

view this post on Zulip Patrick Massot (Jun 08 2018 at 19:37):

Issues are about things to do. LaTeX file would be about things that are done

view this post on Zulip Johan Commelin (Jun 08 2018 at 19:38):

Yes, and PR's form the boundary, and Zulip is the glue that keeps everything together.

view this post on Zulip Patrick Massot (Jun 09 2018 at 10:53):

Family request me, but see https://github.com/PatrickMassot/lean-perfectoid-spaces/commit/334581954ca07e38d16526a264ac85807ee221df to see what I'm working on (comments are already welcome)

view this post on Zulip Patrick Massot (Jun 09 2018 at 10:53):

@Kevin Buzzard

view this post on Zulip Patrick Massot (Jun 09 2018 at 10:54):

when I'll be done proving that uniform_space instance I will quickly be stuck waiting for Johan's PR merge

view this post on Zulip Johan Commelin (Jun 09 2018 at 11:16):

Cool!

view this post on Zulip Johan Commelin (Jun 09 2018 at 11:16):

In my Huber_pair branch I have a stupid definition of I-adic topology

view this post on Zulip Johan Commelin (Jun 09 2018 at 11:16):

But it doesn't give a uniform_space. So it is pretty useless.

view this post on Zulip Johan Commelin (Jun 09 2018 at 11:23):

This:

+-- Somehow we need R° both as a subset of R and a subtype.
+-- There is a coercion from the set to the subtype but relying naively on it seems to bring
+-- type class resolution issues
+definition power_bounded_subring := {r : R // is_power_bounded r}
+definition power_bounded_subring_set := {r : R | is_power_bounded r}

That is exactly the kind of trouble that I have also been having with subrings. I have them both as subset and subtype.

view this post on Zulip Chris Hughes (Jun 09 2018 at 12:09):

Have you tried sticking rigidly to the set notation, and always using coercions and never the subtype. If there's an instance about ↥{r : R | is_power_bounded r}, it won't apply it to {r : R // is_power_bounded r}

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

What is the advantage of working with subsets instead of subtypes?

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

Aah, @Chris Hughes , here's a problem: we have topological_space.induced which happily gives you a topology on a subtype. But not—I think—on a subset. So if you want a topological subring, you need the subring as a subtype.

view this post on Zulip Chris Hughes (Jun 09 2018 at 12:35):

The point is don't mix ↥{r : R | is_power_bounded r} and {r : R // is_power_bounded r} if you want type class inference to work.

view this post on Zulip Chris Hughes (Jun 09 2018 at 12:36):

And if some of your code requires sets, you have to stick to the former.

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

And if some of it requires subtypes? Then you stick with the latter...

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

But what is an example of "code [that] requirese sets"?

view this post on Zulip Chris Hughes (Jun 09 2018 at 12:37):

If it requires subtypes, then you use the coercion from a set and not //

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

I am new to all this type theory stuff, and so far I have been thinking of types as "sets for computer scientists", and I just treat them as sets. And then all of a sudden there are subsets and subtypes, and I don't see why we smuggle subsets in through the backdoor.

view this post on Zulip Chris Hughes (Jun 09 2018 at 12:38):

Unless you only ever need subtypes. In which case don't use sets.

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

If it requires subtypes, then you use the coercion from a set and not //

seems to conflict with

The point is don't mix ↥{r : R | is_power_bounded r} and {r : R // is_power_bounded r} if you want type class inference to work.

view this post on Zulip Chris Hughes (Jun 09 2018 at 12:39):

No it doesn't. Only use the first one.

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

I tried, and then it couldn't infer a topological space on it.

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

Because coercion and type inference don't work together.

view this post on Zulip Nicholas Scheel (Jun 09 2018 at 12:41):

types are not sets; the difference is that values are assigned exactly one type (typing judgments are rigid; although, of course, you can prove that two types are equal and use eq.mp(r) ...), whereas set membership in set theory says nothing about the type of object in the set, which is totally ridiculous imho

view this post on Zulip Chris Hughes (Jun 09 2018 at 12:41):

Use the coercion for your topological space instance as well?

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

I still haven't seen (here or in other threads where the topic came up) any reason to use subsets. I am just confused, and I would like to know why they are cool.

view this post on Zulip Chris Hughes (Jun 09 2018 at 12:42):

i.e. prove ↥{r : R | is_power_bounded r} is a topological space not {r : R // is_power_bounded r}

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

types are not sets; the difference is that values are assigned exactly one type (typing judgments are rigid; although, of course, you can prove that two types are equal and use eq.mp(r) ...), whereas set membership in set theory says nothing about the type of object in the set, which is totally ridiculous imho

@Nicholas Scheel Ok, great, so why do we smuggle set membership back in, if it is so ridiculous?

view this post on Zulip Nicholas Scheel (Jun 09 2018 at 12:42):

the model for a type-theoretic “set” is set a := a -> Prop which is precisely a “set” of elements (of a particular type) satisfying that predicate (conceptually)

view this post on Zulip Chris Hughes (Jun 09 2018 at 12:42):

Or always stick to subtypes. Subsets are good because they can intersect each other and be subsets of each other.

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

Ok, and subtypes find that hard?

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

We can define an intersection of subtypes right? Just take \and of their properties.

view this post on Zulip Nicholas Scheel (Jun 09 2018 at 12:43):

but set just a predicate, it doesn’t contain any elements of the type ... which is what a subtype is for: it contains an element and the proof that it is in the corresponding set, essentially

view this post on Zulip Chris Hughes (Jun 09 2018 at 12:43):

Because everything only has one type, there's no such thing really as the intersection of two subtypes.

view this post on Zulip Nicholas Scheel (Jun 09 2018 at 12:44):

the subtypes would need to have the same supertype, otherwise it doesn’t make sense

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

Right, I see.

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

But if I have two subtypes of X, say S and T, then I can do subtype (\lam x, S.property x \and T.property x).

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

But I understand that this is a clumsy way of doing intersections, and for subsets it is just a lot easier.

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

So we need subsets and subtypes.

view this post on Zulip Chris Hughes (Jun 09 2018 at 12:49):

And that would be hard to use if you had a proof that ∀ x : s, p x and you had x : subtype (\lam x, S.property x \and T.property x)

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

So, at some point in my code I prove that if the subset S is a subring, then we have an instance of ring S. And I think here S is silently coerced to a subtype, for otherwise ring S doesn't typecheck.

view this post on Zulip Chris Hughes (Jun 09 2018 at 12:49):

yes.

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

But then some other code couldn't infer an instance of ring (subtype S), and I got confused.

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

So I also proved explicitly that I had an instance of ring (subtype S) by copy-pasting the other proof verbatim.

view this post on Zulip Chris Hughes (Jun 09 2018 at 12:50):

Because it has to be the same expression for type class inference to work. definitional equality isn't good enough I think

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

And then it worked. But now I don't see the point of the silent coercion.

view this post on Zulip Chris Hughes (Jun 09 2018 at 12:51):

Which is why it's best to stick to coercions the whole time.

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

I tried, but it didn't work.

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

Maybe I didn't try hard enough (-;

view this post on Zulip Chris Hughes (Jun 09 2018 at 12:51):

What didn't work?

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

Sticking to coercions. (Or do you mean explicit coercions, instead of silent ones?)

view this post on Zulip Chris Hughes (Jun 09 2018 at 12:53):

There both the same. What in particular didn't work?

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

Let me try to find it.

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

I think it was these lines: https://github.com/jcommelin/lean-perfectoid-spaces/blob/Huber_pair/src/adic_space.lean#L36-L38

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

But I don't have Lean here, so I can't test it. Sorry.

view this post on Zulip Chris Hughes (Jun 09 2018 at 12:57):

I couldn't find for_mathlib.subring

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

Aah, that is in the subring branch

view this post on Zulip Chris Hughes (Jun 09 2018 at 12:58):

Found it.

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

I thought Huber_pair was a branch of subring

view this post on Zulip Patrick Massot (Jun 09 2018 at 12:58):

need to be in branch subring

view this post on Zulip Chris Hughes (Jun 09 2018 at 13:00):

Did the is_ideal I not work. Or something else?

view this post on Zulip Johan Commelin (Jun 09 2018 at 13:00):

No, I think it was with subrings and topological spaces

view this post on Zulip Johan Commelin (Jun 09 2018 at 13:00):

Ok, maybe it was both.

view this post on Zulip Johan Commelin (Jun 09 2018 at 13:01):

Because the is_ideal I needed to infer a ring structure ring (subtype S), and that (subtype S) was explicit because of the topological stuff in those lines.

view this post on Zulip Chris Hughes (Jun 09 2018 at 13:04):

I think this might be the issue instance subtype.comm_ring [comm_ring R] {S : set R} [is_subring S] : comm_ring (subtype S)
should be instance subtype.comm_ring [comm_ring R] {S : set R} [is_subring S] : comm_ring S

view this post on Zulip Chris Hughes (Jun 09 2018 at 13:06):

Worst case scenario if you can't get the coercion to work is to literally do @has_coe_to_sort.coe whatever instead of subtype S

view this post on Zulip Johan Commelin (Jun 09 2018 at 13:07):

Ok, thanks! I'll try it out when I get back to lean!

view this post on Zulip Patrick Massot (Jun 09 2018 at 14:16):

I need help with the following annoying lemma:

example (R : Type*) [comm_ring R] (V : set R) :
  prod.swap '' {p : R × R |  (x : R), x  V  -x = p.snd + -p.fst} = {p : R × R | p.snd + -p.fst  V} :=
sorry

view this post on Zulip Patrick Massot (Jun 09 2018 at 14:17):

part of the problem is I'm not able to use neg_eq_iff_neg_eq, even inside conv

view this post on Zulip Patrick Massot (Jun 09 2018 at 14:20):

I'm also stuck on

variables (R : Type) [comm_ring R] [topological_space R] [comm_ring R] [topological_ring R]
def nhd_zero := (nhds (0 : R)).sets

lemma nhd_zero_symmetric {V : set R} : V  nhd_zero R   (λ a, -a) '' V  nhd_zero R :=
begin
  intro H,
  dsimp [nhd_zero],
  have := continuous.tendsto (topological_add_group.continuous_neg R) 0,
  unfold filter.tendsto at this,
  simp at this,
  have almost:= this H,
  sorry
end

view this post on Zulip Patrick Massot (Jun 09 2018 at 14:20):

But this is one is nastier since it involves filters

view this post on Zulip Reid Barton (Jun 09 2018 at 14:30):

How about this

example (R : Type*) [comm_ring R] (V : set R) :
  prod.swap '' {p : R × R |  (x : R), x  V  -x = p.snd + -p.fst} = {p : R × R | p.snd + -p.fst  V} :=
begin
  rw set.image_swap_eq_preimage_swap, ext p, cases p with r1 r2,
  change ( x, x  V  -x = r1 - r2)  (r2 - r1  V),
  have :  x, -x = r1 - r2  x = r2 - r1,
    by intro x; rw [neg_eq_iff_neg_eq, eq_comm]; simp,
  simp only [this], simp
end

view this post on Zulip Reid Barton (Jun 09 2018 at 14:34):

For the second one, what you proved is (λ a, -a) ⁻¹' V ∈ nhd_zero R, so then show that (λ a, -a) ⁻¹' V = (λ a, -a) '' V somehow.

view this post on Zulip Patrick Massot (Jun 09 2018 at 15:37):

Thank you very much @Reid Barton. change was the key for the first one

view this post on Zulip Patrick Massot (Jun 09 2018 at 15:37):

For the second one I guess I only needed some encouragement ;-)

lemma nhd_zero_symmetric {V : set A} : V  nhd_zero A   (λ a, -a) '' V  nhd_zero A :=
begin
  intro H,
  have := continuous.tendsto (topological_add_group.continuous_neg A) 0,
  rw (show (λ (a : A), -a) 0 = 0, by simp) at this,
  have almost:= this H,
  have aux : { r : A | -r  V } = (λ a, -a) '' V, by simp[set.image, neg_eq_iff_neg_eq],
  simpa [filter.mem_map, aux] using almost
end

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 16:39):

But then some other code couldn't infer an instance of ring (subtype S), and I got confused.

Johan -- I think the point is that given a subset there are two ways to get a subtype, the explicit and the implicit way, because someone set up a coercion. Because the coercion is set up, you're never supposed to use the explicit constructor, you are completely handing the job over to the type class inference system. So when you use commands like subtype S explictly, instead of that funky up-arrow, this confuses the type class inference system.

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 16:40):

[nonsense deleted]

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 16:41):

A "subtype" really does not mean a subset of a type, a subtype is a completely new and different inductive type; if you want to get back to the original type you can use coercion but this is still applying a function, sending a term of the subtype to its value.

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 16:42):

subtypes are better than subsets because subtypes are types. It's easy to interact with them with the .1 and .2 notation and the \<_,_\> notation

view this post on Zulip Johan Commelin (Jun 09 2018 at 16:44):

Right, but I can imagine that at some point people want to take the intersection of two subrings, are maybe generate a subring, etc... And it seems that sutsets are useful in those cases.

view this post on Zulip Patrick Massot (Jun 09 2018 at 17:17):

Sometimes things come as subsets, for instance power bounded elements

view this post on Zulip Chris Hughes (Jun 09 2018 at 17:17):

I'm doing group_theory at the moment, and it is a little bit awkward proving things about a subgroup that's normal within another subgroup for example, or worse, quotienting by a subgroup within another subgroup. I've been copying the proofs os Sylow's theorem's over from coq, using this paper https://arxiv.org/pdf/cs/0611057.pdf, and most of the group theory in coq seems to be proved on subgroups rather than groups, i.e. they often talk about a subgroup H of a group G, without mentioning anything in G which is not in H.

view this post on Zulip Patrick Massot (Jun 09 2018 at 17:18):

This is the story Assia is always telling us

view this post on Zulip Johan Commelin (Jun 09 2018 at 17:19):

/me feels his inner mathematician shudder and cringe.

view this post on Zulip Johan Commelin (Jun 09 2018 at 17:20):

Somehow this shouldn't be necessary.

view this post on Zulip Patrick Massot (Jun 09 2018 at 17:25):

I agree

view this post on Zulip Chris Hughes (Jun 09 2018 at 17:27):

I'm not sure how much it would help, particularly with the quotienting issue. If you didn't quotient within the subtype, you wouldn't end up with a group, You'd have some type which had a subtype which is a group. It might help avoid notation like subtype.val '' S, which I seem to have to do rather a lot.

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 17:42):

@Kenny Lau Should is_valuation be a typeclass? It currently is

view this post on Zulip Kenny Lau (Jun 09 2018 at 17:43):

I don't know

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 17:47):

Me neither

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 17:47):

I'm writing brief LaTeX notes as Patrick suggested

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 18:05):

@Johan Commelin I don't understand github well enough to review your PR. I tried to add a comment and got the error Start commit oid is not part of the pull request

view this post on Zulip Johan Commelin (Jun 09 2018 at 18:07):

Hmm, I don't know how that happened...

view this post on Zulip Johan Commelin (Jun 09 2018 at 18:08):

I can't make sense of it... all commits in its "local context" are either already in your master branch, or in my PR...

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 18:08):

I can't seem to make comments on your PR.

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 18:08):

Or at least I can't say the following:

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 18:09):

So I was envisaging that stuff in for_mathlib was stuff which it was our responsibility to try and get into mathlib. But this code looks like it was written by other people -- is it even Ok to put it in our project? And then is our job to try and PR this to mathlib or will the authors take care of that?

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 18:09):

It's attached to the line Authors: Johannes Hölzl, Mitchell Rowett, Scott Morrison

view this post on Zulip Johan Commelin (Jun 09 2018 at 18:09):

Right... that's a good point

view this post on Zulip Johan Commelin (Jun 09 2018 at 18:10):

(I hate all those license things)

view this post on Zulip Johan Commelin (Jun 09 2018 at 18:10):

Anyway, all I did was take their code and translate from multiplicative notation to additive...

view this post on Zulip Johan Commelin (Jun 09 2018 at 18:10):

I don't know what is appropriate in this case

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 18:14):

@Mario Carneiro What do you think of this subring code?

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 18:14):

+/-- `S` is a subring: a set containing 1 and closed under multiplication, addition and and additive inverse. -/
+class is_subring  (S : set R) extends is_add_subgroup S, is_submonoid S : Prop.
+
+instance subset.ring {S : set R} [is_subring S] : ring S :=
+{ add_comm      := assume a,_⟩ b,_⟩, subtype.eq $ add_comm _ _,
+  left_distrib  := assume a,_⟩ b,_⟩ c,_⟩, subtype.eq $ left_distrib _ _ _,
+  right_distrib := assume a,_⟩ b,_⟩ c,_⟩, subtype.eq $ right_distrib _ _ _,
+  .. subtype.add_group,
+  .. subtype.monoid }
+
+instance subtype.ring {S : set R} [is_subring S] : ring (subtype S) :=
+{ add_comm      := assume a,_⟩ b,_⟩, subtype.eq $ add_comm _ _,
+  left_distrib  := assume a,_⟩ b,_⟩ c,_⟩, subtype.eq $ left_distrib _ _ _,
+  right_distrib := assume a,_⟩ b,_⟩ c,_⟩, subtype.eq $ right_distrib _ _ _,
+  .. subtype.add_group,
+  .. subtype.monoid }

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 18:15):

We will be playing with several subrings of a given Huber ring so we will surely need some way to formalise the idea of is_subring.

view this post on Zulip Chris Hughes (Jun 09 2018 at 18:16):

Why use both ring S and ring (subtype S) ?

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 18:16):

But should we just avoid subsets completely? Or is it hard to say without context?

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 18:17):

Chris I am just cutting and pasting what Johan wrote. I don't know what is best. My understanding is that you're saying ring (subtype S) is unnecessary

view this post on Zulip Chris Hughes (Jun 09 2018 at 18:17):

I think so.

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 18:17):

and we should use typeclass inference at all times

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 18:17):

but what I am unclear about is if we should be using sets at all

view this post on Zulip Chris Hughes (Jun 09 2018 at 18:18):

Whenever possible it's better to. I think you have to use sets. is_subring has to be defined on a predicate anyway. How would you define it on a subtype?

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 18:19):

I see your point!

view this post on Zulip Johan Commelin (Jun 09 2018 at 18:21):

The reason that both versions are there is simply that stuff doesn't typecheck without the (subtype S) version. Which is probably due to "mistakes" I made in other parts of the code.

view this post on Zulip Johan Commelin (Jun 09 2018 at 18:21):

I would love to get rid of it, because it looks "unmathematical"

view this post on Zulip Chris Hughes (Jun 09 2018 at 18:22):

and x \in S is more natural than S x so it may as well be a set. Going between sets and subtypes isn't the hard part, it's when you have to deal with subtypes of subtypes, and then the same set but as a subtype.

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 18:25):

So what exactly breaks when you remove the subtype version?

view this post on Zulip Johan Commelin (Jun 09 2018 at 18:27):

I think some code in my Huber_pair branch. The topology on S is the induced topology, via subtype.val. And this turns S into subtype S. But then you also want a ring structure on it...

view this post on Zulip Johan Commelin (Jun 09 2018 at 18:34):

Kevin, I will get back to the PR on monday morning I guess...

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 18:34):

Yeah, let's figure out how it all works

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 18:34):

this PR business

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 18:34):

there's no hurry

view this post on Zulip Johan Commelin (Jun 09 2018 at 18:41):

Ok, let's do that.

view this post on Zulip Johan Commelin (Jun 09 2018 at 18:42):

(Oh and by the way, you can git rm *.aux etc in the LaTeX folder, to get rid of those files that you don't actually want to track.)

view this post on Zulip Patrick Massot (Jun 09 2018 at 20:13):

And put them in .gitignore file: at root of project, a file containing lines like *.aux, *.dvi (dvi?!)

view this post on Zulip Patrick Massot (Jun 09 2018 at 22:11):

I'm the king of filters! https://github.com/kbuzzard/lean-perfectoid-spaces/pull/5

view this post on Zulip Mario Carneiro (Jun 10 2018 at 08:54):

What do you think of this subring code?

It's fine, except that the two instances are defeq so you need not prove it twice

view this post on Zulip Kevin Buzzard (Jun 10 2018 at 10:28):

(Oh and by the way, you can git rm *.aux etc in the LaTeX folder, to get rid of those files that you don't actually want to track.)

Sure, but every time the file is updated they come back, right?

view this post on Zulip Kevin Buzzard (Jun 10 2018 at 10:32):

What do you think of this subring code?

It's fine, except that the two instances are defeq so you need not prove it twice

Johan -- defeq is not the same as equal (for example rw won't make some random change from a thing to a defeq thing before rewriting), so Mario is not saying "your code is bound to still work if you remove the second instance", but my impression is that we should kill that last instance and then try and understand how to correctly work around the problems that this causes. The type class inference system is not something you can just add to -- my understanding is that careful thought needs to go into it. The moment there is more than one route from A to B, or a non-trivial way of getting from A to A, there's a risk that there will be problems down the line (time-outs, obscure errors).

view this post on Zulip Mario Carneiro (Jun 10 2018 at 10:41):

That's not quite what I'm saying. You should have both instances, but you can prove one by just referencing the other

view this post on Zulip Kevin Buzzard (Jun 10 2018 at 10:47):

This whole type class inference thing is still a mystery to me in places.

view this post on Zulip Patrick Massot (Jun 10 2018 at 12:01):

(Oh and by the way, you can git rm *.aux etc in the LaTeX folder, to get rid of those files that you don't actually want to track.)

Sure, but every time the file is updated they come back, right?

git will never track a file without being explicitly instructed to do so. You could issue this instruction by mistake, using a careless git add *. This is where .gitignore comes in. In a file matches a pattern listed in .gitignore you need a git add -f file_name to add it. This way you can safely add *.pdf in .gitignore but still put, say Wedhorn's lecture notes, in the repository if you want to. Adding compiled versions of the TeX files present in the repository is pointless.

view this post on Zulip Johan Commelin (Jun 11 2018 at 06:57):

@Patrick Massot Does

instance toplogical_ring.to_uniform_space : uniform_space R

use the ring structure?

view this post on Zulip Johan Commelin (Jun 11 2018 at 07:04):

Cool PR by the way! I added some comments.

view this post on Zulip Patrick Massot (Jun 11 2018 at 07:05):

No, it should be about topological groups. I PR'ed this quickly to make sure no work is duplicated (we should maybe declare somewhere on what part we intend to work), but really it should go to the for_mathlib directory, and be stated for topological groups (maybe even non abelian). @Johannes Hölzl did you intend to build this instance (canonical uniform structure on commutative topological groups) at some point?

view this post on Zulip Johan Commelin (Jun 11 2018 at 07:13):

Yes, it would be nice to know who is working on what.

view this post on Zulip Johan Commelin (Jun 11 2018 at 07:13):

But I think we have done most low-hanging fruit

view this post on Zulip Patrick Massot (Jun 11 2018 at 07:17):

Sure

view this post on Zulip Kevin Buzzard (Jun 11 2018 at 15:18):

Isn't it all low-hanging fruit? ;-)

view this post on Zulip Kevin Buzzard (Jun 11 2018 at 15:18):

I guess someone needs to think about completions at some point. Perhaps we need some more issues, perhaps of a smaller nature.

view this post on Zulip Johan Commelin (Jun 11 2018 at 17:02):

Isn't it all low-hanging fruit? ;-)

Well, I think that Spa will be non-trivial (Leanwise).

view this post on Zulip Johan Commelin (Jun 11 2018 at 17:10):

@Mario Carneiro Will stuff like the following line mess up the type class system?

instance toplogical_ring.to_uniform_space : uniform_space R := stuff_goes_here

view this post on Zulip Mario Carneiro (Jun 11 2018 at 17:10):

I don't see any obvious reason for this to cause a problem

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

Ok, I thought you would get a non-trivial route topological_ring → uniform_space → topological_space.

view this post on Zulip Mario Carneiro (Jun 11 2018 at 17:12):

oh, well that's true, I suppose you need to make sure that this is defeq to the other path to topological space

view this post on Zulip Mario Carneiro (Jun 11 2018 at 17:13):

A uniform space extends a topological space, so you just need to let the topological component be the one inherited from topological_ring

view this post on Zulip Mario Carneiro (Jun 11 2018 at 17:13):

that means that you can't use the default proof of is_open_uniformity

view this post on Zulip Johan Commelin (Jun 11 2018 at 17:23):

This might create some trouble...

view this post on Zulip Johan Commelin (Jun 11 2018 at 17:24):

@Mario Carneiro Does this suggest that in fact topological_ring should extend ring and uniform_space. And have constructor from ring + top_space ?

view this post on Zulip Johan Commelin (Jun 11 2018 at 17:25):

(In fact, this is more about topological groups... the ring structure is not relevant.)

view this post on Zulip Patrick Massot (Jun 11 2018 at 19:01):

@Mario Carneiro we are talking about https://github.com/PatrickMassot/lean-perfectoid-spaces/blob/top_rings/src/adic_space.lean#L60 It uses uniform_space.of_core I'm not sure about things that should be defeq are defeq

view this post on Zulip Patrick Massot (Jun 11 2018 at 19:02):

I'll try to ask Lean

view this post on Zulip Patrick Massot (Jun 11 2018 at 19:28):

It doesn't want to answer, which is probably not good. I tries

example : (@toplogical_ring.to_uniform_space R _ _ _ _).to_topological_space  = (by apply_instance : topological_space R) := rfl

but Lean says tactic failed, type mismatch on the opening parenthesis on RHS. Checking the type of LHS and RHS looks good, even with pp.all

view this post on Zulip Mario Carneiro (Jun 12 2018 at 01:52):

Ah yes, you shouldn't use uniform_space.of_core, that generates the uniformity topology but you want to pick up the default topology on a topological ring

view this post on Zulip Johannes Hölzl (Jun 12 2018 at 02:51):

No, it should be about topological groups. I PR'ed this quickly to make sure no work is duplicated (we should maybe declare somewhere on what part we intend to work), but really it should go to the for_mathlib directory, and be stated for topological groups (maybe even non abelian). @Johannes Hölzl did you intend to build this instance (canonical uniform structure on commutative topological groups) at some point?

Yes, I would like to see uniform spaces derived from topological groups.

view this post on Zulip Johan Commelin (Jun 12 2018 at 07:10):

Right, but picking up the existing topology is going to be pretty hard, I guess.

view this post on Zulip Johan Commelin (Jun 12 2018 at 07:13):

Noob question: if we have a situation like this in the type class system, or more generally... to paths $$f$ and gg to go from AA to BB, and they are not defeq, but there is a proof that they are equal. Would parametricity help out? Or is it an idle hope to envision some synergy between this lambda-Prolog unification and parametricity?

view this post on Zulip Johan Commelin (Jun 12 2018 at 07:14):

(I still don't know if parametricity is the promising silver bullet that I want it to be. If it is, then I think I ought to spend most of my time in bringing it to Lean... but I fear that it doesn't actually help that much in doing maths.)

view this post on Zulip Andrew Ashworth (Jun 12 2018 at 07:19):

well, that would require a lot more brains on the part of the type class inference system

view this post on Zulip Johan Commelin (Jun 12 2018 at 07:20):

/me loves type class inference systems with brains :graduation_cap:

view this post on Zulip Andrew Ashworth (Jun 12 2018 at 07:20):

while I personally haven't encountered it, Leo is already worried about the performance of the type class inference system

view this post on Zulip Andrew Ashworth (Jun 12 2018 at 07:21):

so I don't think it's a practical thing to hope for in the future

view this post on Zulip Andrew Ashworth (Jun 12 2018 at 07:21):

the more you ask a tactic to do, the slower it runs...

view this post on Zulip Andrew Ashworth (Jun 12 2018 at 07:22):

i wonder if anyone here is interested in old-style chess engines

view this post on Zulip Johan Commelin (Jun 12 2018 at 07:23):

Hmmm too bad. And Kudos to human brains...

view this post on Zulip Andrew Ashworth (Jun 12 2018 at 07:23):

type class inference works like that, it searches all the possible ways to get from A to B

view this post on Zulip Andrew Ashworth (Jun 12 2018 at 07:23):

the number of possible paths grows exponentially

view this post on Zulip Andrew Ashworth (Jun 12 2018 at 07:23):

with each step

view this post on Zulip Johan Commelin (Jun 12 2018 at 07:23):

Yes, how would the old-style Chess engines help? (I never studied them.)

view this post on Zulip Andrew Ashworth (Jun 12 2018 at 07:24):

they don't help, it's a comment on how hard the problem is

view this post on Zulip Andrew Ashworth (Jun 12 2018 at 07:25):

type class inference is something that must be done in a sane amount of time, or users of Lean will get really frustrated when their proof takes ages to type-check

view this post on Zulip Johan Commelin (Jun 12 2018 at 07:26):

Would new-style chess engines help? I wonder if we are willing to give up "determinism" to win a lot of speed.

view this post on Zulip Andrew Ashworth (Jun 12 2018 at 07:27):

no, because if lean manages to synthesize a proof at 2 pm and then doesn't at 4pm, you've got a problem

view this post on Zulip Andrew Ashworth (Jun 12 2018 at 07:28):

I mean, maybe you can find some way to cache the proof, but.... this is very out there

view this post on Zulip Johan Commelin (Jun 12 2018 at 07:28):

Right. I would think that maybe Lean could output some hints that will help it to verify the proof deterministically and fast the next time round.

view this post on Zulip Scott Morrison (Jun 12 2018 at 07:29):

There's also no need to give up determinism merely because you have good heuristics for searching the "interesting" parts of the tree first.

view this post on Zulip Johan Commelin (Jun 12 2018 at 07:29):

Hmm, true

view this post on Zulip Johan Commelin (Jun 12 2018 at 07:29):

But, do you know of good heuristics?

view this post on Zulip Scott Morrison (Jun 12 2018 at 07:30):

I really need to explore uses of my rewrite_search tactic outside of category theory. It attempts to prove A = B by exploring the graph of all possible rewrites by a given set of lemmas, but targets the search by exploring the parts of the graph with least "edit distance" between the LHS and the RHS, for various interpretations of "edit distance".

view this post on Zulip Johan Commelin (Jun 12 2018 at 07:32):

Sounds promising.

view this post on Zulip Johan Commelin (Jun 12 2018 at 07:33):

Can't wait to have such stuff available at my fingertips (-;

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 07:39):

@Johan Commelin Do you understand the consequences of all this for the perfectoid project?

view this post on Zulip Johan Commelin (Jun 12 2018 at 07:43):

@Kevin Buzzard What do you mean? The consequences of Scott's tactics, or the consequences of this topological diamond?

view this post on Zulip Johan Commelin (Jun 12 2018 at 07:44):

Now that I think of it, we can probably remove the diamond by just not making it an instance. That means we can write nice stuff like is_complete R but we can still write is_complete (to_uniform R).

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 07:44):

I just mean whether you now know the answer to the question "will stuff like [instance top_ring_to_uniform_space] mess up the type class system?"

view this post on Zulip Johan Commelin (Jun 12 2018 at 07:44):

And then, when those with more Lean-fu then the mortal mathematicians have some time, they can fix the diamond issue, and we can write nice code again.

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 07:45):

I mean that I have not really been following the details of this typeclass discussion and am wondering if you now know enough to tell me how to set up the perfectoid project.

view this post on Zulip Johan Commelin (Jun 12 2018 at 07:46):

Maybe @Patrick Massot can join in. But my suggestion would be to have an explicit map from top_rings to uniform_spaces, and just use it explicitly when needed. (Because I think we don't need it that often.)

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 07:48):

I should note that when I started writing schemes I didn't use type class inference for anything (I had lots of rings and didn't use it for them). You don't have to use it. It's just supposed to make things easier. If it doesn't make them easier then we can probably avoid it. If we convince ourselves that it's not robust enough then we can avoid it. Is there some sort of underlying unfixable problem with modules?

view this post on Zulip Johan Commelin (Jun 12 2018 at 07:50):

We don't need modules for this project, right?

view this post on Zulip Johan Commelin (Jun 12 2018 at 07:51):

Modules seem to be rather easy to agitate in Lean. I think we could write module' that avoids the type class system, but it would duplicate a lot of effort; and ultimately it is not the path we want to take.

view this post on Zulip Johan Commelin (Jun 12 2018 at 07:52):

But in the current situation it seems to me that modules are almost unusable.

view this post on Zulip Johan Commelin (Jun 12 2018 at 07:55):

In that Gitter link, Mario said that the ring shouldn't be a field in the module structure. But I don't really understand why not. I think it would solve a lot of problems, and I don't really see what kind of problems it creates.

view this post on Zulip Johan Commelin (Jun 12 2018 at 07:58):

@Mario Carneiro If you have time, could you say a few words about why the ring shouldn't be a field of the module structure?

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 08:07):

noncomputable def poly.map {S : Type} [ring S] (f : S  R) [is_ring_hom f] : polynomial S  polynomial R :=
finsupp.map_range f (is_ring_hom.map_zero f)

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 08:08):

@Johannes Hölzl Should this map be noncomputable, or should we try to make it computable by making extra assumptions on R and/or S and then over-riding them later?

view this post on Zulip Johan Commelin (Jun 12 2018 at 08:08):

I think it is fine to have this in for_mathlib, but it should go into the mason_stothers lib at some point.

view this post on Zulip Scott Morrison (Jun 12 2018 at 08:09):

err... it should go in mathlib!

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

Yes, by transitivity

view this post on Zulip Johan Commelin (Jun 12 2018 at 08:10):

And then in mason_stothers they can make it as computable as they want :wink:

view this post on Zulip Mario Carneiro (Jun 12 2018 at 09:20):

Right, but picking up the existing topology is going to be pretty hard, I guess.

It is not difficult to set this up with the current setup. You should just not use uniform_space.to_core, just construct the uniform space using the constructor

view this post on Zulip Johannes Hölzl (Jun 12 2018 at 09:20):

@Johannes Hölzl Should this map be noncomputable, or should we try to make it computable by making extra assumptions on R and/or S and then over-riding them later?

this should be computable now, in the recent mathlib versions, finsupp.map_range is computable

view this post on Zulip Mario Carneiro (Jun 12 2018 at 09:23):

If you have time, could you say a few words about why the ring shouldn't be a field of the module structure?

At least with the current setup, it is generally not a good idea to have types as fields in the structure. If you did this with the scalar ring of module, you wouldn't be able to talk about ℝ-modules without imposing an equality condition, which would cause cast headaches

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

Hmm, do you mean that all of a sudden you have 1 type for all modules? So, if you would have fields (R : Type) (hR : ring R) in the structure, then you want to define is_linear_map [module M] [module N] (M -> N) : Prop, but now they might be modules over different rings!

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

Or do you mean something more subtle?

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 09:59):

If you have rings A and B and a ring map A -> B, and an A-module M and a B-module N then mathematicians would quite happily talk about A-module homomorphisms M -> N

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 09:59):

because N inherits an A-module structure from the map A->B

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 10:00):

but as Johan points out, this discussion is, at least at this point, in the wrong thread, this is Patrick's type class woes

view this post on Zulip Johan Commelin (Jun 12 2018 at 10:26):

Right, so returning to perfectoid spaces... what is the next step?

view this post on Zulip Johan Commelin (Jun 12 2018 at 10:26):

Should we pull stuff on presheaves in from your schemes-repo?

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 12:45):

The next step is for me to accept these PRs and then have a look at what is left.

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 12:45):

I think I want to do presheaves because I did them before

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 12:45):

I think the next step is the topological space Spa(A)

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 12:45):

for A a Huber pair

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 12:45):

and that goes via Spv(R)

view this post on Zulip Patrick Massot (Jun 13 2018 at 21:26):

It is not difficult to set this up with the current setup. You should just not use uniform_space.to_core, just construct the uniform space using the constructor

What do you call "the constructor"? I'm not worried at all, I'm pretty sure I have the mathematical content right, and I used the filter library so we will have all lemmas we need. But I'm not quite sure what I should do (And I had no time at all since Saturday, because of a conference and invited people).

view this post on Zulip Mario Carneiro (Jun 13 2018 at 22:58):

I mean the default, built in constructor for a structure, the thing that you get with { x := ... } notation

view this post on Zulip Mario Carneiro (Jun 13 2018 at 22:59):

I guess the constant is called uniform_space.mk

view this post on Zulip Mario Carneiro (Jun 13 2018 at 23:03):

If you just delete the of_core function application in the instance, and just use that structure directly as the instance, it will more or less work, except there will be a new proof obligation for the part of the proof that of_core was doing

view this post on Zulip Kevin Buzzard (Jun 20 2018 at 20:50):

I've spent the last few days doing non-Lean stuff but I would like to accept these PRs soon; I read through them all properly today. One thing that occurred to me about this uniform space business is that Patrick's construction of a uniform space on a topological ring should (a) probably work for a topological group and (b) might already be in mathlib (if the docstring for uniform_space is anything to go by). @Johannes Hölzl you wrote "A topological group also has a natural uniformity, even when it is not metrizable" in the docstring for uniform space -- is this theorem somewhere in mathlib?

view this post on Zulip Mario Carneiro (Jun 20 2018 at 20:55):

This is in the pipeline last I checked. it should appear soonish

view this post on Zulip Mario Carneiro (Jun 20 2018 at 20:55):

I think Johannes is working on merging Patrick's normed space stuff

view this post on Zulip Kevin Buzzard (Jun 20 2018 at 21:02):

Thanks. I've not been at all Lean-active for the last week or so, and today I tried to catch up with perfectoid spaces but there's a whole bunch of stuff which should be in mathlib but isn't; I could open about 8 small PRs but I didn't want to add to the pile because I can happily store them in my project. However stuff like polynomials in 1 variable, which is lengthy, presents more of a problem because mason-stother doesn't compile at the minute. Patrick has explicitly proved that a topological ring has a uniform space structure and it wouldn't surprise me if his proof worked for topological groups. So we have something if you or Johannes want it. For the schemes project I just kept bundling everything in my repo but this time I'd rather do it more sensibly.

view this post on Zulip Mario Carneiro (Jun 20 2018 at 21:04):

I'm not sure how useful this will be given that Johannes is working on this stuff at the moment - it may just be additional merging overhead. You should coordinate with him

view this post on Zulip Kevin Buzzard (Jun 20 2018 at 21:05):

OK thanks for the tips.

view this post on Zulip Patrick Massot (Jun 20 2018 at 21:44):

I'm sorry I haven't talk at all since last saturday. I'm attending a conference and have extremely bad internet access in my hotel (only my phone is able to use the wifi, at very slow speed). I have completely rewritten my uniform structure stuff, and I hope to PR it tomorrow from the lecture hall. It now provides a uniform structure on commutative topological groups which gives back a topology defeq to the original one. I'm very grateful for Johannes work but it seems both over-engineered and nit enough. I have no idea what kind of generalization he has in mind.

view this post on Zulip Scott Morrison (Jun 20 2018 at 21:48):

Polynomials in 1 variable I'd really like to see in mathlib; so even if Kevin can "happily store them in my project", let's try to accumulate as little as possible in the perfectoid repository.

view this post on Zulip Kevin Buzzard (Jun 20 2018 at 22:36):

Polynomials in 1 variable I'd really like to see in mathlib; so even if Kevin can "happily store them in my project", let's try to accumulate as little as possible in the perfectoid repository.

Currently we're unhappy when it comes to polynomials. We tried using Johannes' mason-stother but not all of it compiles. Currently we're sorrying stuff.

view this post on Zulip Kenny Lau (Jun 20 2018 at 22:36):

I proved its UMP :P although Chris did much more than me

view this post on Zulip Kenny Lau (Jun 20 2018 at 22:37):

def polynomial.UMP (A : Type v) [comm_ring A] [algebra R A] :
  A  alg_hom (polynomial R) A :=
(ℕ.UMP A).trans (monoid_ring.UMP _ _ _)

view this post on Zulip Kenny Lau (Jun 20 2018 at 22:37):

https://github.com/kckennylau/local-langlands-abelian/blob/master/src/polynomial.lean#L37

view this post on Zulip Kevin Buzzard (Jun 20 2018 at 22:39):

o_O there is group cohomology, Galois theory, and local class field theory in that repo too!

view this post on Zulip Kevin Buzzard (Jun 20 2018 at 22:39):

You have been busy.

view this post on Zulip Kenny Lau (Jun 20 2018 at 22:40):

well I can’t talk too much ‘bout it now :p

view this post on Zulip Kenny Lau (Jun 20 2018 at 22:41):

we both know the reason

view this post on Zulip Kevin Buzzard (Jun 20 2018 at 22:41):

I shall be grilling you on it in about 36 hours.

view this post on Zulip Patrick Massot (Jun 21 2018 at 10:51):

@Kevin Buzzard the situation with uniform structures is now as follows. Contrary to what the docstrings you mentioned suggests, mathlib currently doesn't know that a commutative topological group has a canonical uniform structure. What @Johannes Hölzl did recently was to write https://gist.github.com/johoelzl/ca90562c46b49a1bbb1be36272ec3b1a At the same time I decided to use my flight to learn a bit about filters instead of complaining I'm not used to them. Then I wrote https://github.com/PatrickMassot/lean-perfectoid-spaces/blob/top_rings/src/for_mathlib/topological_structures.lean. What are the differences then? The obvious one is that Johannes' code is shorter and most probably cleaner. But it also doesn't address the main question. He defines a class group_with_nhds_zero which seems to be a generalization of topological groups, remembering just enough about properties of neighborhoods of zero in a topological group to define the uniform structure. He doesn't prove topological groups give instances of this new class but this should be easy (one would need to be careful with the topology induced by the uniform structure to be defeq to the original one, which is what I messed up in my first attempt). My concern is over-engineering: I see no use of this new class beyond topological group. AFAIK this only adds a layer of complexity. Actually I was already completely puzzled by this section. I have no idea how this could be useful beyond the obvious case where the uniform structure is the canonical one.

view this post on Zulip Kevin Buzzard (Jun 21 2018 at 18:26):

I don't think these CS people worry about over-engineering. I guess as we just saw from the filter stuff, it's actually sometimes convenient to have these things around. I've written a paper about adic spaces and I don't understand filters, but that's only because for actual adic spaces you only basically deal with rings whose topology is generated by a finitely-generated ideal, when sanity is restored. [by "generated by" I mean that powers of the ideal form a basis of neighbourhoods of zero]

view this post on Zulip Kevin Buzzard (Jun 21 2018 at 20:13):

Oh wow I have universe issues!

A valuation on a ring RR is a map from RR to a totally ordered commutative monoid satisfying some axioms. Two valuations vv and ww are equivalent if v(r)v(s)w(r)w(s)v(r)\leq v(s) \iff w(r)\leq w(s). The valuation spectrum Spv(R)Spv(R) of RR is the set of equivalence classes of valuations. As a ZFC-ist I did a little calculation here -- I checked that every valuation (which could take values in a monoid which gigantic cardinality, far far bigger than that of R) was equivalent to a valuation taking values in basically the monoid generated by the image of R (I'm being a bit sloppy -- one has to check that there is no issue here with the axioms for a valuation). But at the end of the day I have a set.

In Lean I have

structure valuations (R : Type) [comm_ring R] :=
{α : Type}
[ : linear_ordered_comm_group α]
(f : R  option α)
(Hf : is_valuation f)

and I can define two valuations to be equivalent

instance valuations.setoid (R : Type) [comm_ring R] : setoid (valuations R) :=
{ r := λ f g,  r s : R, f r  f s  g r  g s,
  iseqv := ...

but the associated quotient has type Type 1, so in theory I have left the world of ZFC. As I just outlined above, in ZFC I know how to claw my way back [I can put an upper bound on the cardinality of alpha and hence build a set containing at least one instance of every equivalence class]. Can I do this in Lean somehow?


view this post on Zulip Mario Carneiro (Jun 21 2018 at 20:41):

If you don't care about computational content (I hear you Kenny, keep it down), you can notice that a valuation equivalence class is determined by the relation S : R -> R -> Prop defined by S r s <-> v r <= v s. That is, two valuations are equivalent if and only if they have equal induced relations on R. Thus you can define the spectrum to be the collection of all relations that arise from some valuation (from a commutative monoid in the same universe as R).

view this post on Zulip Reid Barton (Jun 21 2018 at 21:10):

This is a good example of the kind of situation I was asking about here -- https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/type.20resizing/near/127424550

view this post on Zulip Mario Carneiro (Jun 21 2018 at 21:33):

The answer is ad hoc. Essentially you figure out the "reason" why your set is small, which will take the form of some small set that enumerates your large objects, and use that as the index instead

view this post on Zulip Kevin Buzzard (Jun 21 2018 at 23:21):

The "reason" for me was a standard ZFC-ish one: one can "shrink" the target until it's generated by the image of R, and hence has the same cardinality of R (or aleph_null if R is finite). So we get a bound on the cardinality of the target and this suffices because the set of isomorphism classes is now a set. The relation argument is alien to me, although obviously I believe it. I am torn about whether I should care about this -- should I write my own "section 4" or just forget it? Interestingly, I notice that the foundational paper https://arxiv.org/abs/math/0409584 (section 1 page 7) which is strongly related to the foundations of what Scholze is doing, assumes that every set is contained in a universe. This paper would be really nice to formalise! Although those that look at it will quickly see what the issue is...

view this post on Zulip Mario Carneiro (Jun 22 2018 at 01:13):

There is nothing wrong with your argument, and indeed you can also use it to get a bound as well. The relation argument just seemed easier since it literally defines the equivalence relation, making the quotient trivial. Actually you would probably want to run that argument anyway to prove that given a valuation in any universe you get a relation, since this amounts to constructing an equivalent valuation in the same universe as the ring.

view this post on Zulip Kevin Buzzard (Jun 24 2018 at 09:54):

So I finally followed up on this. Here's what the code looks like (I removed the actual definition of valuation to simplify things):

view this post on Zulip Kevin Buzzard (Jun 24 2018 at 09:55):

import data.equiv

def is_valuation {R : Type} [comm_ring R] {α : Type} [linear_order α] (f : R  α) : Prop := sorry

structure valuations (R : Type) [comm_ring R] :=
(α : Type) [ : linear_order α] (f : R  α) (Hf : is_valuation f)

instance to_make_next_line_work (R : Type) [comm_ring R] (v : valuations R) : linear_order v.α := v.

instance valuations.setoid (R : Type) [comm_ring R] : setoid (valuations R) := {
  r := λ v w,  r s : R, valuations.f v r  v.f s  w.f r  w.f s,
  iseqv := ⟨λ v r s,iff.rfl,λ v w H r s,(H r s).symm,λ v w x H1 H2 r s,iff.trans (H1 r s) (H2 r s)
}

def Spv1 (R : Type) [comm_ring R] := quotient (valuations.setoid R)

def Spv2 (R : Type) [comm_ring R] :=
  {ineq : R  R  Prop //  v : valuations R,  r s : R, ineq r s  v.f r  v.f s}

#check Spv1 _ -- Type 1
#check Spv2 _ -- Type

view this post on Zulip Kevin Buzzard (Jun 24 2018 at 09:58):

Spv1 is the equivalance classes of valuations, and Spv2 is the associated vague notions of order (it's not antisymmetric because f might not be injective -- maybe it's a preorder?) on R. The constructions live in different type universes. But are they equiv?

view this post on Zulip Kenny Lau (Jun 24 2018 at 09:58):

equiv can take different universes

view this post on Zulip Kevin Buzzard (Jun 24 2018 at 09:58):

In other words, should I expect to be able to prove noncomputable definition they_are_the_same (R : Type) [comm_ring R] : equiv (Spv1 R) (Spv2 R) := sorry?

view this post on Zulip Kevin Buzzard (Jun 24 2018 at 09:58):

Yes Kenny, I noticed this -- so at least my question typechecks.

view this post on Zulip Kevin Buzzard (Jun 24 2018 at 09:59):

Here are perhaps the functions:

def to_fun (R : Type) [comm_ring R] : Spv1 R  Spv2 R :=
quotient.lift (λ v,(⟨λ r s, valuations.f v r  v.f s,v,λ r s,iff.rfl⟩⟩ : Spv2 R))
  (λ v w H,begin dsimp,congr,funext,exact propext (H r s) end)

noncomputable def inv_fun (R : Type) [comm_ring R] : Spv2 R  Spv1 R :=
λ ineq,H,classical.some H

view this post on Zulip Kevin Buzzard (Jun 24 2018 at 10:00):

I don't know if that's going to give me trouble because I used tactics in a definition -- but it was for a proof.

view this post on Zulip Kevin Buzzard (Jun 24 2018 at 10:16):

To prove either direction I need to show something about a map constructed using quotient.lift (assuming this is the way to define to_fun). For example right_inv boils down to

R : Type,
_inst_1 : comm_ring R,
rel : R  R  Prop,
Hrel :  (v : valuations R),  (r s : R), rel r s  v.f r  v.f s,
r s : R
 (to_fun R classical.some Hrel).val r s = rel r s

view this post on Zulip Kevin Buzzard (Jun 24 2018 at 10:21):

Is this quotient.something?

view this post on Zulip Kevin Buzzard (Jun 24 2018 at 10:22):

and left_inv looks like

R : Type,
_inst_1 : comm_ring R,
vs : Spv1 R
 inv_fun R (to_fun R vs) = vs

view this post on Zulip Kenny Lau (Jun 24 2018 at 10:22):

just unfold everything

view this post on Zulip Kevin Buzzard (Jun 24 2018 at 10:22):

I don't need this equiv, but I'm trying to get a feeling for the relative merits of either definition

view this post on Zulip Kevin Buzzard (Jun 24 2018 at 10:23):

If you unfold everything you end up with classical.somes which don't behave

view this post on Zulip Kevin Buzzard (Jun 24 2018 at 10:23):

or at least I did

view this post on Zulip Kevin Buzzard (Jun 24 2018 at 10:24):

you end up with a goal of the form classical.some _ a <= classical.some _ b iff classical.some _ a <= classical.some _ b or something, and iff.refl doesn't work because the _s are slightly different -- or at least they were for me (with the definition of valuation filled in)

view this post on Zulip Kenny Lau (Jun 24 2018 at 10:24):

what is the property of each some

view this post on Zulip Kevin Buzzard (Jun 24 2018 at 10:24):

Kenny it must be more than an unfold -- the left_inv goal has vs in it and we know nothing about vs other than its type --

view this post on Zulip Kevin Buzzard (Jun 24 2018 at 10:25):

I don't know if I'm making a wrong turn, but I tried quotient.exists_rep

view this post on Zulip Kevin Buzzard (Jun 24 2018 at 10:30):

Here's an example of the sort of mess I get into:

  left_inv := λ vs,begin
    cases (quotient.exists_rep vs) with v Hv,
    rw Hv,
    apply quotient.sound,
    intros r s,
    have H := classical.some_spec (to_fun R vs).property,
    rw (H r s).symm, -- fails
    /-
    rewrite tactic failed, did not find instance of the pattern in the target expression
  (classical.some _).f r ≤ (classical.some _).f s
state:
R : Type,
_inst_1 : comm_ring R,
vs : Spv1 R,
v : valuations R,
Hv : ⟦v⟧ = vs,
r s : R,
H : ∀ (r s : R), (to_fun R vs).val r s ↔ (classical.some _).f r ≤ (classical.some _).f s
⊢ (classical.some _).f r ≤ (classical.some _).f s ↔ v.f r ≤ v.f s
    -/

view this post on Zulip Kevin Buzzard (Jun 24 2018 at 10:31):

I wondered if I'd made a wrong turn

view this post on Zulip Kevin Buzzard (Jun 24 2018 at 10:54):

https://gist.github.com/kbuzzard/e0b36acade48f955212e8ea5142cb7b1 is where I'm at. Somehow I was expecting this to be easier. Various failures deleted.

view this post on Zulip Kevin Buzzard (Jun 24 2018 at 11:02):

Perhaps I should outline the reason I'm even thinking about this. Part of me still wants to work in ZFC so everything should live in Type. But the natural definition of Spv R lives in Type 1. I just wanted to weigh up the pros and cons of the two approaches. If I can prove they're equiv then many of the assertions I'll be making about one type will be true for the other one by some general "canonical isomorphism" principle. I figured that if I kept track of both then I could see to what extent my code was affected by the choice I'll ultimately make. But if I can't prove the equiv then I am less sure that the two approaches are "the same". Probably the equiv is fine and it's just my general incompetence with quotient types. Maybe I should instead be proving that to_fun is a bijection?

view this post on Zulip Chris Hughes (Jun 24 2018 at 11:10):

I wish there was an option to display the type of proofs in the pp.

view this post on Zulip Chris Hughes (Jun 24 2018 at 11:16):

Proved left_inv

noncomputable definition they_are_the_same (R : Type) [comm_ring R] : equiv (Spv1 R) (Spv2 R) :=
{ to_fun := to_fun R,
  inv_fun := inv_fun R,
  left_inv := λ vs, quotient.induction_on vs begin
    assume vs,
    apply quotient.sound,
    intros r s,
    have := (to_fun R vs).property,
    have H := classical.some_spec (to_fun R vs).property r s,
    refine H.symm.trans _,
    refl,
  end,
  right_inv := λ s2,begin
    cases s2 with rel Hrel,
    apply subtype.eq,
    dsimp,
    unfold inv_fun,
    funext r s,
    sorry
  end
}

view this post on Zulip Chris Hughes (Jun 24 2018 at 11:17):

Often when the inverse function is classical.some, it's much easier to use equiv.of_bijective

view this post on Zulip Chris Hughes (Jun 24 2018 at 11:29):

Done

open function
noncomputable definition they_are_the_same (R : Type) [comm_ring R] : equiv (Spv1 R) (Spv2 R) :=
equiv.of_bijective (show bijective (to_fun R),
from ⟨λ x y, quotient.induction_on₂ x y (λ x y h,
  quotient.sound (λ r s, iff_of_eq (congr_fun (congr_fun (subtype.mk.inj h) r) s))),
  λ x, v, hv⟩⟩, v, subtype.eq $ funext (λ r, funext (λ s, propext (hv r s).symm))⟩⟩)

view this post on Zulip Kevin Buzzard (Jun 24 2018 at 12:33):

Thanks!

view this post on Zulip Mario Carneiro (Jun 24 2018 at 12:56):

I wish there was an option to display the type of proofs in the pp.

set_option pp.proofs true

view this post on Zulip Chris Hughes (Jun 24 2018 at 14:14):

That displays the proofs, not their type.

view this post on Zulip Patrick Massot (Jun 24 2018 at 19:44):

I think Johannes is working on merging Patrick's normed space stuff

@Mario Carneiro @Johannes Hölzl What do you mean? Is he extracting stuff from https://github.com/PatrickMassot/lean-differential-topology/blob/master/src/norms.lean? This effort is completely stopped because of type class resolution issues in the very last declaration of that file that seems to be related again to the modules and rings issue. I would really love to be able to move forward. Especially since I should have quite a lot of time for Lean in the coming weeks.

view this post on Zulip Johannes Hölzl (Jun 25 2018 at 05:19):

Yes, I want to work on normed spaces. I won't have time this week (we have two workshops in Amsterdam) but the following week.

view this post on Zulip Patrick Massot (Jun 25 2018 at 05:33):

Do you intend to fix my stuff or restart from scratch?

view this post on Zulip Patrick Massot (Jun 25 2018 at 05:34):

Also, did you see my new version of uniform structures on topological groups (that I discussed in this thread four days ago)?

view this post on Zulip Patrick Massot (Jun 25 2018 at 14:17):

I wanted to start working on completions of abelian topological groups and noticed I forgot to prove the uniform group instance. This is now done in https://github.com/PatrickMassot/lean-perfectoid-spaces/commit/adb5140ecc46a577325cda46dcf6626424f5ef02

view this post on Zulip Patrick Massot (Jun 25 2018 at 14:18):

sub_eq_add_neg being a simp rule is really a nuisance. I can't imagine any situation where I would want to replace a - b with a + -b

view this post on Zulip Kevin Buzzard (Jun 25 2018 at 16:41):

The idea that neg is a "simpler" function than sub I guess. Computer scientists seem to have some crazy ordering of things which is very counterintuitive to mathematicians. Concepts which we regard as having equal weight often don't have equal weight in Lean. I guess Lean is trying to put something into some kind of canonical form with simp, and clearly this canonical form isn't supposed to have any subs in.

view this post on Zulip Chris Hughes (Jun 25 2018 at 16:50):

I guess some simp lemmas deal with add and neg, but not sub. It's not that weird, everyone writes ab1a b^{-1} in a group, but never a/ba / b

view this post on Zulip Kevin Buzzard (Jun 25 2018 at 16:53):

Conversely no schoolkid writes 5 + (-3), they all write 5 - 3

view this post on Zulip Mario Carneiro (Jun 26 2018 at 02:04):

I just discovered the [norm] simp set thanks to Simon:

Add [norm] simp set. It contains all lemmas tagged with [simp] plus any lemma tagged with [norm]. These rules are used to produce normal forms and/or reduce the number of constants used in a goal. For example, we plan to add the lemma f <$> x = x >>= pure ∘ f to [norm].

I agree that the sub elimination theorem is a horrible simp lemma, and it's a candidate for [norm] if anything is.

view this post on Zulip Johan Commelin (Jun 27 2018 at 07:48):

I think we can improve readability of the code that uses valuations by using slightly longer names in https://github.com/kbuzzard/lean-perfectoid-spaces/blob/cc415fe8834b4886a5305feb89ac566d7b04ba94/src/valuations.lean#L338
I suggest that the field f be called fun and Hf be called is_val.

view this post on Zulip Johan Commelin (Jun 28 2018 at 07:38):

Hmm, I see that there was a coercion that would coerce v to v.f. @Kevin Buzzard Why was that removed? I think it greatly improves readability...

view this post on Zulip Johan Commelin (Jun 28 2018 at 07:39):

And it hides the .f so then I don't care so much how that field is called (-;

view this post on Zulip Kevin Buzzard (Jun 28 2018 at 07:46):

It didn't work sometimes

view this post on Zulip Kevin Buzzard (Jun 28 2018 at 07:48):

But I was too lazy to debug. I was sitting next to Chris when I wrote it and he said "oh yeah, has coe to fun is a bit rubbish and doesn't always work" and although I interpreted this as "we need to ask Mario why it is failing" I just wanted the code to work so I removed it. Put it back, see what breaks, and ask for help!

view this post on Zulip Scott Morrison (Jun 28 2018 at 07:49):

Yeah, my experience of coercions is that the pain of them mysteriously not working (usually it's not so mysterious, just Lean isn't quite as clever as you are guessing what you really meant to say) far outweighs the smoothness when they do work. But I like writing verbose code, anyway. :-)

view this post on Zulip Johan Commelin (Jun 28 2018 at 07:52):

Ok, will do (-; So far nothing is breaking...

view this post on Zulip Johan Commelin (Jun 28 2018 at 07:54):

Scott, yes I understand that. But in this case I think there are some crucial parts of the code that should be as readible as possible.

view this post on Zulip Kevin Buzzard (Jun 28 2018 at 11:58):

I removed the coercion for all the wrong reasons. It was Thursday night at Xena, I was low on battery, I had nearly finished a file, it was time to go home, I asked Chris why my code didn't work and he said he'd had trouble with has_coe_to_fun and I thought "sod it I'll just remove it". I commented it out specifically to remind future me to come back to it.

view this post on Zulip Kevin Buzzard (Jun 28 2018 at 12:04):

In other news, I discovered a subtlety in the definition of continuous. Two valuations v : R -> option alpha and v' : R -> option beta are equivalent if v(r)v(s)v(r)v(s)v(r)\leq v(s)\iff v'(r)\leq v'(s) for all r,sr,s. There are other equivalent ways of writing the equivalence, and it's a lemma that they all coincide. Unsurprisingly, at some point I found I needed the lemma, but surprisingly it was in the definition of continuous. My slightly superficial (as it turns out) understanding of the definition of a continuous valuation was that vv was continuous iff the pre-image of a : option alpha // a < b was open for all b in alpha -- but this is not always constant on an equivalence class! The problem is that alpha might be embedded as some infinitesimally small subgroup of beta, and then beta contains elements smaller than everything in the image other than 0 (the none option) which have no analogue in alpha. One has to restrict to b's which are in the group generated by the image of v. I'd never noticed this before.

So we need to prove 1.25 and 1.27 in Wedhorn -- but then it turns out that we don't even have quotient rings and the fact that the quotient of a comm ring by a prime ideal is an integral domain. These are not hard -- but it's funny to see how holey everything still is. I am about to ask Kenny to fill in my sorries :-) [I just committed some stuff]

view this post on Zulip Johan Commelin (Jul 02 2018 at 10:13):

That actually sounds pretty technical! I would have glossed over this for sure...

view this post on Zulip Patrick Massot (Jul 02 2018 at 10:28):

Working on the definition of manifolds in Lean also taught me that the well known fact that the relation of equivalence of atlases is an equivalence relation has slightly more content that I was aware of. I don't think there is any book proving this fact. Most of them simply use the word "equivalence class" without writing "equivalence relation" anywhere (this includes my own lecture notes on differential topology). Some write "is easily seen to be an equivalence relation". I haven't seen any proof anywhere except on my scratchpad.

view this post on Zulip Johan Commelin (Jul 03 2018 at 07:50):

@Kevin Buzzard I'm confused: why are you changing is_valuation to valuation? I thought that it should be is_* because the type is Prop.

view this post on Zulip Johan Commelin (Jul 03 2018 at 07:50):

Is there a good explanation of these naming conventions somewhere?

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 07:50):

We can have is_ if you like.

view this post on Zulip Johan Commelin (Jul 03 2018 at 07:51):

Well... you're the boss :rolling_on_the_floor_laughing:

view this post on Zulip Johan Commelin (Jul 03 2018 at 07:51):

It is just that I got a bit confused... but I'm not sure if there even is a solid convention.

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 07:52):

Boss -- not really. And I don't understand the rules properly. I think Kenny had a namespace is_valuation which I thought was going a bit far.

view this post on Zulip Mario Carneiro (Jul 03 2018 at 07:52):

What is the convention in question? (I think I am the MC - Master of Conventions)

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 07:53):

So a function f from a ring R to some totally ordered monoid M is a _valuation_ if it satisfies some axioms.

view this post on Zulip Mario Carneiro (Jul 03 2018 at 07:53):

Is it a property of the function, or an augmented function?

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 07:53):

class valuation {α : Type} [linear_ordered_comm_group α]
  {R : Type} [comm_ring R] (f : R  option α) : Prop :=
(map_zero : f 0 = 0)
(map_one  : f 1 = 1)
(map_mul  :  x y, f (x * y) = f x * f y)
(map_add  :  x y, f (x + y)  f x  f (x + y)  f y)

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 07:53):

That used to say class is_valuation

view this post on Zulip Mario Carneiro (Jul 03 2018 at 07:54):

I think it should be is_valuation then

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 07:54):

The next line in the code is namespace valuation

view this post on Zulip Johan Commelin (Jul 03 2018 at 07:54):

Kevin, you see Prop stands for property :wink:

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 07:54):

and did it used to say namespace is_valuation?

view this post on Zulip Mario Carneiro (Jul 03 2018 at 07:55):

namespace valuation will be annoying since it's not accessed by projection

view this post on Zulip Mario Carneiro (Jul 03 2018 at 07:55):

since it's a typeclass

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 07:55):

I don't understand that. I've never understood projection properly.

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 07:56):

I just muddle through with projections. I write G.mul_assoc and if it doesn't work I write group.mul_assoc G

view this post on Zulip Mario Carneiro (Jul 03 2018 at 07:56):

To use projection you have to be projecting on an expression whose type has the same name as the namespace

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 07:56):

and I never have a clue which one I'm supposed to use or which one will work

view this post on Zulip Mario Carneiro (Jul 03 2018 at 07:56):

If you use typeclass inference, then the operative name is in a hidden parameter, so it doesn't work

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 07:56):

These words are too hard for me

view this post on Zulip Mario Carneiro (Jul 03 2018 at 07:57):

i.e. you can't write f.map_zero when you know is_valuation f because lean looks at the type of f, which is pi, and then checks the pi namespace only

view this post on Zulip Mario Carneiro (Jul 03 2018 at 07:57):

(actually that doesn't really work, pi isn't a namespace)

view this post on Zulip Mario Carneiro (Jul 03 2018 at 07:58):

but for inductive types like nat which are also namespaces, it works well

view this post on Zulip Johan Commelin (Jul 03 2018 at 07:58):

Kevin, you can write H.bla for [H: is_valuation f], but not f.bla. But then, we want H to be implicit (type class inference, etc...) so in practice you won't be able to type H.bla because there is no explicit H.

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 07:58):

What I do not understand (at all) is whether I should have _something_ called valuation. We have group G, right? Why can't I have valuation f?

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 07:58):

I don't see the difference

view this post on Zulip Mario Carneiro (Jul 03 2018 at 07:58):

I think lean might complain if H turns out to be implicit in is_valuation.bla though

view this post on Zulip Johan Commelin (Jul 03 2018 at 07:58):

Because group has extra structure.

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 07:59):

Why do I want to use type class inference for valuations?

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 07:59):

I do not understand what we want here

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 07:59):

I was just sick of writing is_

view this post on Zulip Mario Carneiro (Jul 03 2018 at 07:59):

If you use the augmented function approach you can use the name valuation and call functions by projection

view this post on Zulip Johan Commelin (Jul 03 2018 at 07:59):

So, if you have a monoid or something like that, you could have a is_group G : Prop, but group G is not a Prop.

view this post on Zulip Mario Carneiro (Jul 03 2018 at 08:00):

You can also just ignore conventions if you think valuation will never be defined

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 08:00):

What's worse is that "valuation" in the literature actually means "equivalence class of valuations"

view this post on Zulip Mario Carneiro (Jul 03 2018 at 08:00):

You didn't like my valuation = relation suggestion?

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 08:00):

I don't know about that either. I implemented both

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 08:00):

I have zfc.valuation too

view this post on Zulip Mario Carneiro (Jul 03 2018 at 08:00):

ooh, mysterious

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 08:01):

just means "I only use Type"

view this post on Zulip Mario Carneiro (Jul 03 2018 at 08:01):

why would you do that? You can just restrict the universe variables of polymorphic functions

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 08:02):

I've just realised I don't even know what is being suggested. (1) I change class valuation ... : Prop back to class is_valuation. Then what? Is namespace valuation changing back to namespace is_valuation?

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 08:02):

"I only use Type" is just a maths thing

view this post on Zulip Mario Carneiro (Jul 03 2018 at 08:03):

You can put it in a namespace if you want, or use valuation_* pseudo-namespacing, or put the theorems in the parent namespace

view this post on Zulip Johan Commelin (Jul 03 2018 at 08:03):

Kevin, I think Mario would want

structure valuations (R : Type) [comm_ring R] :=
{α : Type}
[ : linear_ordered_comm_group α]
(f : R  option α)
(Hf : is_valuation f)

to be called valuation

view this post on Zulip Johan Commelin (Jul 03 2018 at 08:03):

But I am not sure about that...

view this post on Zulip Mario Carneiro (Jul 03 2018 at 08:03):

Only the f and hf should be in the structure

view this post on Zulip Johan Commelin (Jul 03 2018 at 08:03):

No...

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 08:04):

Two valuations are equivalent if they "only differ by the alpha"

view this post on Zulip Mario Carneiro (Jul 03 2018 at 08:04):

you can still state that with the alpha as parameter

view this post on Zulip Johan Commelin (Jul 03 2018 at 08:04):

But then valuations depends on alpha, that becomes horrible right?

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 08:04):

I have valuations defined to be something else

view this post on Zulip Mario Carneiro (Jul 03 2018 at 08:04):

no, that becomes tractable

view this post on Zulip Mario Carneiro (Jul 03 2018 at 08:05):

(I would drop the s though)

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 08:05):

no I don't, I have valuations to be defined exactly like that

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 08:05):

then

instance valuations.setoid (R : Type) [comm_ring R] : setoid (valuations R) :=
{ r := λ v w, ∀ r s : R, v.f r ≤ v.f s ↔ w.f r ≤ w.f s,...

view this post on Zulip Johan Commelin (Jul 03 2018 at 08:05):

Mario, then you have defined "valuation on R with value group alpha" (why not Gamma?)

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 08:06):

alpha not Gamma because Kenny wrote it

view this post on Zulip Mario Carneiro (Jul 03 2018 at 08:06):

Note that valuations as Johan quotes lives in Type 1, so if it's aiming for zfc land it's not doing so great

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 08:06):

I don't know whether I should be worrying about ZFC or not. It seems futile really because I use so much other stuff with universes in

view this post on Zulip Johan Commelin (Jul 03 2018 at 08:06):

Yes, and I am completely fine with that (-;

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 08:07):

Maybe I'm just making sure that one day I can write my own section 4

view this post on Zulip Mario Carneiro (Jul 03 2018 at 08:07):

Mario, then you have defined "valuation on R with value group alpha" (why not Gamma?)

Yes, that's the point. The equivalence relation can span two value groups

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 08:08):

Only the f and hf should be in the structure

I don't understand how to make the setoid if alpha is not where Johan put it

view this post on Zulip Mario Carneiro (Jul 03 2018 at 08:09):

Kevin, someday I will write a treatise on lean in ZFC and there will be an automated analysis to find out if your theorem uses universes in an essential way. Until then, just write things that are intuitively not using universes essentially and don't otherwise worry about it

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 08:09):

There is a "minimal" alpha associated with every valuation, which is unique up to unique isomorphism -- it's just the group generated by the image of teh valuation

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 08:09):

Mario -- that's great news about ZFC. I'm sure there will be mathematicians out there who genuinely care (those who read the section 4's in this world)

view this post on Zulip Mario Carneiro (Jul 03 2018 at 08:10):

I care

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 08:10):

There was a lot of fuss after FLT was proved, on the foundations of maths mailing list, because Wiles had used categories

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 08:10):

so a rumour started that the proof didn't fit into ZFC

view this post on Zulip Mario Carneiro (Jul 03 2018 at 08:10):

but the analysis is not quite as easy as "just stick to Type", even if it is morally just that

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 08:11):

Isn't the analysis just "just stick to Type, and demand that all your libraries do the same"?

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 08:11):

Or is even that not enough?

view this post on Zulip Mario Carneiro (Jul 03 2018 at 08:11):

The problem is that almost everything you write is trivially not just in Type

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 08:11):

?!

view this post on Zulip Mario Carneiro (Jul 03 2018 at 08:11):

for example, any function Type -> Type is not in Type

view this post on Zulip Mario Carneiro (Jul 03 2018 at 08:12):

i.e. huber_ring or whatever

view this post on Zulip Mario Carneiro (Jul 03 2018 at 08:12):

these are justifiable in ZFC as class functions

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 08:12):

Ok I give in

view this post on Zulip Johan Commelin (Jul 03 2018 at 08:13):

As far as I am concerned, universes are just the axiom of infinity on steroids. Which means I am not concerned...

view this post on Zulip Mario Carneiro (Jul 03 2018 at 08:13):

But my point is that this analysis, when it eventually arrives, will handle universe polymorphic functions, so you shouldn't avoid polymorphism for the sake of "chapter 4"

view this post on Zulip Johan Commelin (Jul 03 2018 at 08:14):

Mario, so how do we write an alpha-agnostic setoid with your version of valuation?

view this post on Zulip Mario Carneiro (Jul 03 2018 at 08:14):

You shouldn't literally write a setoid

view this post on Zulip Mario Carneiro (Jul 03 2018 at 08:14):

it's too big

view this post on Zulip Mario Carneiro (Jul 03 2018 at 08:15):

instead you just use the equivalence relation

view this post on Zulip Mario Carneiro (Jul 03 2018 at 08:15):

and use the relation as a small representative when you need one

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 08:15):

But we need the actual valuation functions all the time

view this post on Zulip Johan Commelin (Jul 03 2018 at 08:16):

Mario, so what is morally wrong with the current version that I quoted?

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 08:16):

Line 1 of valuation_spectrum.lean is

definition Spv (A : Type) [comm_ring A] : Type 1 := quotient (valuation.valuations.setoid A)

namespace Spv

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 08:16):

and this is a fundamental object

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 08:16):

Spv is almost an adic space

view this post on Zulip Johan Commelin (Jul 03 2018 at 08:16):

Right, and Spv is the basic building block of all this theory. It is all over the place.

view this post on Zulip Mario Carneiro (Jul 03 2018 at 08:16):

You can define the setoid, but it is one of the things that "essentially uses universes"

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 08:16):

and we're constantly choosing points

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 08:17):

The fundamental topological space which we use all the time is the space of equivalence classes of valuations

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 08:17):

so we have to get this right

view this post on Zulip Johan Commelin (Jul 03 2018 at 08:17):

You can define the setoid, but it is one of the things that "essentially uses universes"

Is that its only moral failure?

view this post on Zulip Mario Carneiro (Jul 03 2018 at 08:17):

What's wrong, again, with defining Spv as the collection of all valuation relations?

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 08:17):

All proofs need an actual valuation

view this post on Zulip Mario Carneiro (Jul 03 2018 at 08:18):

You can define your own version of quot.lift and quot.mk that take valuations

view this post on Zulip Mario Carneiro (Jul 03 2018 at 08:18):

valuation functions that is

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 08:18):

Aah

view this post on Zulip Mario Carneiro (Jul 03 2018 at 08:19):

You only use the relations as inhabitants of the type so that the universe isn't pushed up, but all the work uses functions

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 08:19):

So we hide all the noncomputable stuff in some functions like this, and prove everything we need about them. Is this going to cause problems later?

view this post on Zulip Kevin Buzzard (Jul 03 2018 at 08:20):

We define Spv as t