# Zulip Chat Archive

## Stream: maths

### Topic: Perfectoid spaces

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

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

#### Kevin Buzzard (May 30 2018 at 13:23):

So here's the plan.

#### Kevin Buzzard (May 30 2018 at 13:23):

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

#### Kevin Buzzard (May 30 2018 at 13:23):

and then we develop what we need in there.

#### Kevin Buzzard (May 30 2018 at 13:24):

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

#### Kevin Buzzard (May 30 2018 at 13:24):

But in short, we need adic spaces

#### Kevin Buzzard (May 30 2018 at 13:24):

so we need presheaves and sheaves of topological rings

#### Kevin Buzzard (May 30 2018 at 13:24):

and we need affinoid adic spaces

#### Kevin Buzzard (May 30 2018 at 13:24):

so we need the notion of a valuation on a ring

#### Kevin Buzzard (May 30 2018 at 13:25):

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

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

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

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

#### Kevin Buzzard (May 30 2018 at 13:27):

Are there advantages in working from the top down?

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

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

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

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

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

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

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

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

#### Kevin Buzzard (May 30 2018 at 14:02):

I love this place.

#### Kevin Buzzard (May 30 2018 at 14:02):

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

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

#### Kevin Buzzard (May 30 2018 at 14:03):

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

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

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

#### Kevin Buzzard (May 30 2018 at 15:06):

https://arxiv.org/abs/1709.07343

#### Kevin Buzzard (May 30 2018 at 15:06):

That is the definition we will be formalizing.

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

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

#### Patrick Massot (May 30 2018 at 15:10):

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

#### Patrick Massot (May 30 2018 at 15:10):

Maybe this theory is actually circular

#### Kevin Buzzard (May 30 2018 at 15:15):

:-)

#### Kevin Buzzard (May 30 2018 at 15:15):

Fontaine only defines perfectoid rings

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

#### Kevin Buzzard (May 30 2018 at 15:16):

OK so here's a theorem in maths:

#### Kevin Buzzard (May 30 2018 at 15:17):

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

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

#### Kevin Buzzard (May 30 2018 at 15:17):

Can we use it in Lean?

#### Kevin Buzzard (May 30 2018 at 15:18):

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

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

#### Kevin Buzzard (May 30 2018 at 15:18):

because LaTeX

#### Kevin Buzzard (May 30 2018 at 15:18):

Nobody is raising a prime number to the power infinity

#### Kevin Buzzard (May 30 2018 at 15:19):

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

#### Kevin Buzzard (May 30 2018 at 15:19):

and then n goes to infinity

#### Mario Carneiro (May 30 2018 at 15:19):

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

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

#### Mario Carneiro (May 30 2018 at 15:19):

How many ring construction mechanisms are nested there?

#### Kevin Buzzard (May 30 2018 at 15:20):

I think three or four

#### Kevin Buzzard (May 30 2018 at 15:20):

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

#### Kevin Buzzard (May 30 2018 at 15:20):

I don't think these things commute

#### Kevin Buzzard (May 30 2018 at 15:20):

I think maybe four

#### Kevin Buzzard (May 30 2018 at 15:20):

oh

#### Kevin Buzzard (May 30 2018 at 15:20):

maybe far more

#### Kevin Buzzard (May 30 2018 at 15:21):

it depends on what you mean

#### Kevin Buzzard (May 30 2018 at 15:21):

$\mathbb{Z}_p^{cycl}$

#### Kevin Buzzard (May 30 2018 at 15:21):

is a ring

#### Mario Carneiro (May 30 2018 at 15:21):

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

#### Kevin Buzzard (May 30 2018 at 15:21):

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

#### Mario Carneiro (May 30 2018 at 15:21):

yes

#### Kevin Buzzard (May 30 2018 at 15:21):

I mean I can call it X?

#### Mario Carneiro (May 30 2018 at 15:21):

that's like `Z_cycl p`

I guess

#### Kevin Buzzard (May 30 2018 at 15:21):

no

#### Kevin Buzzard (May 30 2018 at 15:22):

it's much worse

#### Kevin Buzzard (May 30 2018 at 15:22):

maybe it's about as bad

#### Kevin Buzzard (May 30 2018 at 15:22):

there is an issue with completions

#### Kevin Buzzard (May 30 2018 at 15:22):

everything has to be complete at every stage

#### Mario Carneiro (May 30 2018 at 15:22):

so `completion (Z_cycl p)`

?

#### 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/p^nA$

#### Mario Carneiro (May 30 2018 at 15:23):

where's `p`

?

#### Kevin Buzzard (May 30 2018 at 15:23):

it's a constant

#### Kevin Buzzard (May 30 2018 at 15:23):

we fix a prime p on line 1

#### Kevin Buzzard (May 30 2018 at 15:23):

It never changes

#### Mario Carneiro (May 30 2018 at 15:23):

yeah okay, parameters

#### Kevin Buzzard (May 30 2018 at 15:23):

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

#### Kevin Buzzard (May 30 2018 at 15:24):

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

#### Kevin Buzzard (May 30 2018 at 15:24):

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

#### Kevin Buzzard (May 30 2018 at 15:24):

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

#### Kevin Buzzard (May 30 2018 at 15:25):

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

#### Mario Carneiro (May 30 2018 at 15:25):

But `Z_cycl_p`

is one thing after all that construction

#### Kevin Buzzard (May 30 2018 at 15:25):

and $\mathbf{Z}_p^{cycl}$ is `P`

of that

#### Mario Carneiro (May 30 2018 at 15:25):

As in, the notation is not decomposable

#### Kevin Buzzard (May 30 2018 at 15:25):

it depends only on p

#### Kevin Buzzard (May 30 2018 at 15:26):

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

#### Mario Carneiro (May 30 2018 at 15:26):

right

#### Kevin Buzzard (May 30 2018 at 15:26):

We build from left to right

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

#### Kevin Buzzard (May 30 2018 at 15:26):

If $A$ is a ring

#### Kevin Buzzard (May 30 2018 at 15:27):

then $A[[T^{1/p^n}]]$ is formal power series in $T^{1/p^n}$ with coefficients in $A$

#### Kevin Buzzard (May 30 2018 at 15:27):

and $A[[T^{1/p^\infty}]]$ is `P`

of the direct limit of these things

#### Mario Carneiro (May 30 2018 at 15:27):

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

#### Kevin Buzzard (May 30 2018 at 15:27):

no quotient involved

#### Kevin Buzzard (May 30 2018 at 15:27):

$T$ is a variable with no relations

#### Kevin Buzzard (May 30 2018 at 15:28):

Each ring is isomorphic to `A[[X]]`

#### Kevin Buzzard (May 30 2018 at 15:28):

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

#### Mario Carneiro (May 30 2018 at 15:28):

what makes $T^{1/p^n}$ different from X

#### Kevin Buzzard (May 30 2018 at 15:28):

the maps between the various rings

#### Kevin Buzzard (May 30 2018 at 15:28):

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

#### Kevin Buzzard (May 30 2018 at 15:29):

For fixed n all those rings are isomorphic

#### Kevin Buzzard (May 30 2018 at 15:29):

but if you want to call them all X

#### Mario Carneiro (May 30 2018 at 15:29):

So the notation here is `p_infty_completion A p`

#### Kevin Buzzard (May 30 2018 at 15:29):

then the maps all send X to X^p

#### Mario Carneiro (May 30 2018 at 15:29):

where there are only two arguments A and p

#### Kevin Buzzard (May 30 2018 at 15:29):

yes

#### Kevin Buzzard (May 30 2018 at 15:30):

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

#### Kevin Buzzard (May 30 2018 at 15:30):

depends only on A and p

#### Mario Carneiro (May 30 2018 at 15:30):

This is my question

#### Kevin Buzzard (May 30 2018 at 15:30):

Depends only on the ring A and the prime number p

#### Mario Carneiro (May 30 2018 at 15:30):

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

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

#### Kevin Buzzard (May 30 2018 at 15:30):

I now understand the game we're playing

#### Kevin Buzzard (May 30 2018 at 15:31):

If A is a topological ring

#### Kevin Buzzard (May 30 2018 at 15:31):

and p is a prime number

#### Kevin Buzzard (May 30 2018 at 15:31):

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

#### Kevin Buzzard (May 30 2018 at 15:32):

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

#### Kevin Buzzard (May 30 2018 at 15:32):

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

#### Kevin Buzzard (May 30 2018 at 15:32):

Finally [1/T] is a localization

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

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

#### Kevin Buzzard (May 30 2018 at 15:33):

It is "standard notation"

#### Kevin Buzzard (May 30 2018 at 15:33):

this is really interesting

#### Mario Carneiro (May 30 2018 at 15:33):

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

#### Kevin Buzzard (May 30 2018 at 15:33):

no!

#### Kevin Buzzard (May 30 2018 at 15:33):

Are you crazy?

#### Kevin Buzzard (May 30 2018 at 15:34):

what kind of nonsense is that?

#### Kevin Buzzard (May 30 2018 at 15:34):

So what is the question? :-/

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

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

#### Kevin Buzzard (May 30 2018 at 15:35):

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

#### Mario Carneiro (May 30 2018 at 15:36):

I assume changing `T`

for `X`

does nothing?

#### Kevin Buzzard (May 30 2018 at 15:36):

you got me

#### Kevin Buzzard (May 30 2018 at 15:36):

I was just showing you how amazingly flexible our notation was

#### Kevin Buzzard (May 30 2018 at 15:36):

T

#### Kevin Buzzard (May 30 2018 at 15:36):

X

#### Kevin Buzzard (May 30 2018 at 15:36):

any letter at all

#### Kevin Buzzard (May 30 2018 at 15:36):

except most of them would be completely unsuitable

#### Kevin Buzzard (May 30 2018 at 15:36):

I would stick with T

#### Mario Carneiro (May 30 2018 at 15:37):

From a CS standpoint those letters are kind of silly

#### Kevin Buzzard (May 30 2018 at 15:37):

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

#### Mario Carneiro (May 30 2018 at 15:37):

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

#### Kevin Buzzard (May 30 2018 at 15:37):

The ring contains an element called $T$

#### Kevin Buzzard (May 30 2018 at 15:37):

that's the trick

#### Kevin Buzzard (May 30 2018 at 15:37):

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

#### Kevin Buzzard (May 30 2018 at 15:38):

they're defeq for you

#### Kevin Buzzard (May 30 2018 at 15:38):

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

#### Mario Carneiro (May 30 2018 at 15:38):

A simple idea that is surprisingly hard to formalize

#### Reid Barton (May 30 2018 at 15:38):

$T \in k[T]$ just like $\Gamma, x \vdash x$

#### Kevin Buzzard (May 30 2018 at 15:38):

A man who speaks both languages

#### Mario Carneiro (May 30 2018 at 15:38):

In that case `x`

is in the context though

#### Mario Carneiro (May 30 2018 at 15:39):

`k[T]`

isn't a context or a context like thing, it's a concrete ring

#### Mario Carneiro (May 30 2018 at 15:39):

(I guess `k`

is in the context)

#### Kevin Buzzard (May 30 2018 at 15:39):

Oh here is a question

#### Kevin Buzzard (May 30 2018 at 15:39):

Is this question about notation

#### Kevin Buzzard (May 30 2018 at 15:39):

*completely independent* of the question of formalizing the definition?

#### Kevin Buzzard (May 30 2018 at 15:40):

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

#### Mario Carneiro (May 30 2018 at 15:40):

not completely, but for the most part yes

#### Kevin Buzzard (May 30 2018 at 15:40):

Those rings are not needed in the definition

#### Mario Carneiro (May 30 2018 at 15:40):

it affects what things get definitions

#### Kevin Buzzard (May 30 2018 at 15:40):

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

#### Kevin Buzzard (May 30 2018 at 15:40):

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

#### Mario Carneiro (May 30 2018 at 15:41):

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

#### Kevin Buzzard (May 30 2018 at 15:41):

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

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

#### Mario Carneiro (May 30 2018 at 15:43):

It's basically easy to retrofit

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

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

#### Kevin Buzzard (May 30 2018 at 15:52):

This is going to be so much fun

#### Kevin Buzzard (May 30 2018 at 15:52):

Lean is made for this sort of stuff

#### Kevin Buzzard (May 30 2018 at 15:52):

Mario, this is what real maths looks like

#### Kevin Buzzard (May 30 2018 at 15:53):

super-complex structures

#### Kevin Buzzard (May 30 2018 at 15:53):

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

#### Kevin Buzzard (May 30 2018 at 15:53):

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

#### Kevin Buzzard (May 30 2018 at 15:53):

and it will be easy to formalize

#### Kevin Buzzard (May 30 2018 at 15:53):

that's why it's important

#### Kevin Buzzard (May 30 2018 at 15:54):

and easy

#### Kevin Buzzard (May 30 2018 at 15:54):

it's a huge gap in the market

#### Kevin Buzzard (May 30 2018 at 15:55):

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

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

#### Kevin Buzzard (May 30 2018 at 15:56):

and there are huge gaps everywhere

#### Kevin Buzzard (May 30 2018 at 15:56):

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

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

#### Kevin Buzzard (May 30 2018 at 15:57):

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

#### Kevin Buzzard (May 30 2018 at 15:57):

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

#### Kevin Buzzard (May 30 2018 at 15:57):

but this way is much more fun

#### Kevin Buzzard (May 30 2018 at 15:57):

and you'll end up with types that typecheck

#### Kevin Buzzard (May 30 2018 at 15:58):

Lean is a big puzzle game

#### Kevin Buzzard (May 30 2018 at 15:58):

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

#### Kevin Buzzard (May 30 2018 at 15:58):

"construct a term of this type"

#### Kevin Buzzard (May 30 2018 at 15:58):

that's the game

#### Kevin Buzzard (May 30 2018 at 15:58):

the type is the level, the term is the solution

#### Kevin Buzzard (May 30 2018 at 15:59):

All the old levels are boring

#### Kevin Buzzard (May 30 2018 at 15:59):

"prove quadratic reciprocity"

#### Kevin Buzzard (May 30 2018 at 15:59):

"prove the prime number theorem"

#### Kevin Buzzard (May 30 2018 at 15:59):

kids want new levels

#### Kevin Buzzard (May 30 2018 at 15:59):

they are bored with those old levels

#### Kevin Buzzard (May 30 2018 at 15:59):

and the computer scientists keep solving them again and again

#### Kevin Buzzard (May 30 2018 at 16:00):

all those websites

#### Kevin Buzzard (May 30 2018 at 16:00):

"100 classic levels in the formal proof verification game"

#### Kevin Buzzard (May 30 2018 at 16:00):

we want better levels with funkier graphics

#### Kevin Buzzard (May 30 2018 at 16:00):

I mean objects

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

#### Kevin Buzzard (May 30 2018 at 16:01):

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

#### Kevin Buzzard (May 30 2018 at 16:01):

"where are the perfectoid spaces?"

#### Kevin Buzzard (May 30 2018 at 16:02):

I mean graphics

#### Kevin Buzzard (May 30 2018 at 16:02):

the cool objects

#### Kevin Buzzard (May 30 2018 at 16:02):

things have moved on in maths

#### Kevin Buzzard (May 30 2018 at 16:07):

Should one put pdfs of papers in a github repo?

#### Kevin Buzzard (May 30 2018 at 16:08):

"Here are some foundational papers containing important definitions"

#### Kevin Buzzard (May 30 2018 at 16:08):

"which we are formalising"

#### Kevin Buzzard (May 30 2018 at 16:08):

Choice 1: offer a link

#### Kevin Buzzard (May 30 2018 at 16:08):

Choice 2: offer a pdf subdirectory

#### Kevin Buzzard (May 30 2018 at 16:08):

[Choice 3: both]

#### Patrick Massot (May 30 2018 at 16:10):

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

#### Patrick Massot (May 30 2018 at 16:10):

But it's much more important to write a roadmap

#### Patrick Massot (May 30 2018 at 16:10):

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

#### Kevin Buzzard (May 30 2018 at 17:02):

This is very helpful.

#### Kevin Buzzard (May 30 2018 at 17:02):

It will take me some time to write a good roadmap

#### Kevin Buzzard (May 30 2018 at 17:02):

by which I mean a couple of days

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

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

#### Kevin Buzzard (May 31 2018 at 09:49):

That's only needed for the tilting correspondence I think

#### Kevin Buzzard (May 31 2018 at 09:49):

although we will surely need some facts about perfectoid rings

#### Kevin Buzzard (Jun 02 2018 at 00:44):

What are the arguments for and against making `Tate_ring`

into a typeclass?

#### Kevin Buzzard (Jun 02 2018 at 00:44):

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

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

#### Kevin Buzzard (Jun 02 2018 at 00:45):

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

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

#### Kevin Buzzard (Jun 02 2018 at 00:47):

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

#### Kevin Buzzard (Jun 02 2018 at 00:47):

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

#### Kenny Lau (Jun 02 2018 at 00:50):

against: the pseudo-uniformiser is not canonical

#### Kevin Buzzard (Jun 02 2018 at 00:50):

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

#### Kevin Buzzard (Jun 02 2018 at 00:50):

you don't have to give it

#### Kevin Buzzard (Jun 02 2018 at 00:50):

pi pseudouniformiser

#### Kevin Buzzard (Jun 02 2018 at 00:51):

See Remark 3.2

#### Kevin Buzzard (Jun 02 2018 at 00:51):

all you need is that one exists

#### Kevin Buzzard (Jun 02 2018 at 00:51):

any choices are equivalent in some strong way

#### Mario Carneiro (Jun 02 2018 at 00:52):

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

#### Kevin Buzzard (Jun 02 2018 at 00:52):

so no diamonds?

#### Mario Carneiro (Jun 02 2018 at 00:53):

with what?

#### Kevin Buzzard (Jun 02 2018 at 00:53):

I have no idea how these things work

#### Mario Carneiro (Jun 02 2018 at 00:53):

where is `p`

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

#### Kevin Buzzard (Jun 02 2018 at 00:53):

it's a prime number

#### Kevin Buzzard (Jun 02 2018 at 00:53):

best described as a parameter

#### Kevin Buzzard (Jun 02 2018 at 00:53):

because you never change it

#### Mario Carneiro (Jun 02 2018 at 00:54):

The problem with parameters is they don't last long

#### Kevin Buzzard (Jun 02 2018 at 00:54):

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

#### Kevin Buzzard (Jun 02 2018 at 00:54):

and which goes everywhere

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

#### Mario Carneiro (Jun 02 2018 at 00:55):

The question is: if lean is inferring `Tate_ring ?p R`

, how can it infer `p`

?

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

#### Kenny Lau (Jun 02 2018 at 00:57):

`Tate_ring.p`

?

#### Mario Carneiro (Jun 02 2018 at 00:57):

that's also a possibility

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

#### Kevin Buzzard (Jun 02 2018 at 01:00):

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

#### Kevin Buzzard (Jun 02 2018 at 01:01):

but you do need it for perfectoid

#### Kevin Buzzard (Jun 02 2018 at 01:01):

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

#### Kevin Buzzard (Jun 02 2018 at 01:01):

and perfectoid_ring needs a Tate ring and a prime

#### Mario Carneiro (Jun 02 2018 at 01:02):

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

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

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

#### Kevin Buzzard (Jun 02 2018 at 01:04):

this is me building perfectoid ring

#### Kevin Buzzard (Jun 02 2018 at 01:04):

I am building perfectoid space from the top down

#### Kevin Buzzard (Jun 02 2018 at 01:04):

it's a long way up

#### Kevin Buzzard (Jun 02 2018 at 01:04):

I'm taking tentative steps down

#### Kevin Buzzard (Jun 02 2018 at 01:05):

and Mario is suggesting (2)

#### Kevin Buzzard (Jun 02 2018 at 01:37):

Eew prime numbers

#### Kevin Buzzard (Jun 02 2018 at 01:37):

how am I supposed to input a prime number?

#### Kevin Buzzard (Jun 02 2018 at 01:37):

there's a function

#### Kevin Buzzard (Jun 02 2018 at 01:37):

prime : nat -> Prop

#### Kevin Buzzard (Jun 02 2018 at 01:38):

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

#### Kenny Lau (Jun 02 2018 at 01:38):

just make a subtype

#### Kevin Buzzard (Jun 02 2018 at 01:38):

I have an issue with the subtype solution

#### Kevin Buzzard (Jun 02 2018 at 01:39):

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

#### Kevin Buzzard (Jun 02 2018 at 01:39):

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

#### Kenny Lau (Jun 02 2018 at 01:39):

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

\u p

#### Kevin Buzzard (Jun 02 2018 at 01:40):

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

#### Kevin Buzzard (Jun 02 2018 at 01:41):

like our dirty underwear

#### Kevin Buzzard (Jun 02 2018 at 01:42):

Is the subtype already there?

#### Kevin Buzzard (Jun 02 2018 at 01:44):

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

#### Kevin Buzzard (Jun 02 2018 at 01:44):

`prime`

is taken by the predicate

#### Reid Barton (Jun 02 2018 at 01:50):

I don't think there is one

#### Kevin Buzzard (Jun 02 2018 at 01:51):

so I call it `prime'`

?

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

#### Kevin Buzzard (Jun 02 2018 at 02:00):

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

#### Kenny Lau (Jun 02 2018 at 02:00):

make it an autoparam like pnat lol

#### Kevin Buzzard (Jun 02 2018 at 02:00):

oh ha ha

#### Kevin Buzzard (Jun 02 2018 at 02:00):

that is a really cool idea

#### Kevin Buzzard (Jun 02 2018 at 02:00):

wait

#### Kevin Buzzard (Jun 02 2018 at 02:00):

how does this work

#### Kevin Buzzard (Jun 02 2018 at 02:01):

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

#### Kevin Buzzard (Jun 02 2018 at 02:02):

I'll post a gist

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

#### Kevin Buzzard (Jun 02 2018 at 02:02):

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

#### Kevin Buzzard (Jun 02 2018 at 02:03):

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

#### Nicholas Scheel (Jun 02 2018 at 02:03):

or rename the predicate to `is_prime`

#### Kevin Buzzard (Jun 02 2018 at 02:03):

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

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

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

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

#### Kenny Lau (Jun 02 2018 at 02:05):

lmao

#### Kenny Lau (Jun 02 2018 at 02:05):

folly

#### Kevin Buzzard (Jun 02 2018 at 02:05):

constant p

#### Kenny Lau (Jun 02 2018 at 02:05):

ensues

#### Kevin Buzzard (Jun 02 2018 at 02:05):

I think that's the best place to start

#### Kevin Buzzard (Jun 02 2018 at 02:05):

`constant p : nat`

#### Reid Barton (Jun 02 2018 at 02:06):

`axiom hp : prime p`

#### Kevin Buzzard (Jun 02 2018 at 02:06):

I think that's consistent

#### Kevin Buzzard (Jun 02 2018 at 02:07):

the guys doing $L^p$ spaces will hit the roof

#### Kenny Lau (Jun 02 2018 at 02:07):

chaos

#### Kevin Buzzard (Jun 02 2018 at 02:10):

Can I branch the mathlib in my perfectoid space repo

#### Kevin Buzzard (Jun 02 2018 at 02:10):

and edit it

#### Kevin Buzzard (Jun 02 2018 at 02:10):

and create a PR?

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

#### Kevin Buzzard (Jun 02 2018 at 02:11):

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

#### Kevin Buzzard (Jun 02 2018 at 02:12):

and get leanpkg to keep my branch up to date

#### Kenny Lau (Jun 02 2018 at 02:12):

it is sane

#### Kevin Buzzard (Jun 02 2018 at 02:12):

What I am not clear on

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

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

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

#### Andrew Ashworth (Jun 02 2018 at 02:19):

and you work on it in that folder

#### Andrew Ashworth (Jun 02 2018 at 02:19):

editing `_target`

is bad news

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

#### Andrew Ashworth (Jun 02 2018 at 02:22):

yes

#### Kevin Buzzard (Jun 02 2018 at 02:22):

which is some fork of mathlib

#### Kevin Buzzard (Jun 02 2018 at 02:23):

and we maybe have some directory like `src/for_mathlib`

subdirectory

#### Kevin Buzzard (Jun 02 2018 at 02:24):

and then when things are looking tidy

#### Kevin Buzzard (Jun 02 2018 at 02:24):

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

#### Kevin Buzzard (Jun 02 2018 at 02:25):

Have I got all this straight?

#### Andrew Ashworth (Jun 02 2018 at 02:26):

yes

#### Andrew Ashworth (Jun 02 2018 at 02:26):

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

#### Kevin Buzzard (Jun 02 2018 at 02:27):

I see

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

#### Kevin Buzzard (Jun 02 2018 at 02:27):

because I know my project won't

#### Kevin Buzzard (Jun 02 2018 at 02:28):

Is `adic_space`

a typeclass?

#### Kevin Buzzard (Jun 02 2018 at 02:28):

Is `scheme`

a typeclass?

#### Kevin Buzzard (Jun 02 2018 at 02:28):

@Reid Barton what are your thoughts?

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

#### Kevin Buzzard (Jun 02 2018 at 02:28):

I just rebuild whenever I upgrade

#### Kevin Buzzard (Jun 02 2018 at 02:29):

worth the initial wait

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

#### Andrew Ashworth (Jun 02 2018 at 02:29):

unfortunately we are not quite near that point though

#### Kevin Buzzard (Jun 02 2018 at 02:29):

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

#### Kevin Buzzard (Jun 02 2018 at 02:30):

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

#### Kevin Buzzard (Jun 02 2018 at 02:30):

It's all very well proving things about finite groups

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

#### Kevin Buzzard (Jun 02 2018 at 02:31):

but to write down even one thing about perfectoid spaces

#### Kevin Buzzard (Jun 02 2018 at 02:31):

will force Lean to handle the notion of a perfectoid space

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

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

#### Kevin Buzzard (Jun 02 2018 at 02:33):

I have no idea what they are

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

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

#### Kevin Buzzard (Jun 02 2018 at 02:38):

dammit

#### Kevin Buzzard (Jun 02 2018 at 02:38):

I want to get some headline definition of perfectoid space

#### Kevin Buzzard (Jun 02 2018 at 02:38):

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

#### Kevin Buzzard (Jun 02 2018 at 02:39):

so I need `adic_space`

#### Kevin Buzzard (Jun 02 2018 at 02:39):

but

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

#### Kevin Buzzard (Jun 02 2018 at 02:39):

`structure adic_space (α : Type) : Type := sorry`

doesn't work

#### Kevin Buzzard (Jun 02 2018 at 02:39):

I mean the sorry doesn't work

#### Kevin Buzzard (Jun 02 2018 at 02:39):

that's not an adequate structure

#### Mario Carneiro (Jun 02 2018 at 02:39):

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

#### Mario Carneiro (Jun 02 2018 at 02:40):

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

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

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

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

#### Kevin Buzzard (Jun 02 2018 at 02:42):

rofl

#### Kevin Buzzard (Jun 02 2018 at 02:43):

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

#### Kevin Buzzard (Jun 02 2018 at 02:43):

Product of schemes is a scheme etc

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

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

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

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

#### Kevin Buzzard (Jun 02 2018 at 02:50):

o_O so it depends on the underlying type?

#### Kevin Buzzard (Jun 02 2018 at 02:50):

I see

#### Reid Barton (Jun 02 2018 at 02:50):

Well, if you were going to write

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

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

#### Kevin Buzzard (Jun 02 2018 at 02:51):

oh is that somehow the canonically bad thing to do

#### Reid Barton (Jun 02 2018 at 02:51):

then nobody would know which scheme you were talking about

#### Kevin Buzzard (Jun 02 2018 at 02:52):

right

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

#### Reid Barton (Jun 02 2018 at 02:53):

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

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

#### Kevin Buzzard (Jun 02 2018 at 02:53):

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

#### Kevin Buzzard (Jun 02 2018 at 02:53):

possibly which ultimately even proved they were equal

#### Kevin Buzzard (Jun 02 2018 at 02:54):

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

#### Reid Barton (Jun 02 2018 at 02:54):

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

#### Kevin Buzzard (Jun 02 2018 at 02:54):

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

#### Reid Barton (Jun 02 2018 at 02:55):

Yes, that seems much better

#### Kevin Buzzard (Jun 02 2018 at 02:55):

oh god that would make it a dreaded subtype

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

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

#### Kevin Buzzard (Jun 02 2018 at 02:56):

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

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

#### Kevin Buzzard (Jun 02 2018 at 02:57):

oh great! Thanks!

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

#### Kevin Buzzard (Jun 02 2018 at 03:00):

current v

#### Kevin Buzzard (Jun 02 2018 at 03:00):

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

#### Kevin Buzzard (Jun 02 2018 at 03:00):

of Prime

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

#### Kevin Buzzard (Jun 02 2018 at 03:01):

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

#### Kevin Buzzard (Jun 02 2018 at 03:01):

the dirty truth coming out :-)

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

#### Kevin Buzzard (Jun 02 2018 at 03:02):

because this would imply it was a locally ringed space

#### Kevin Buzzard (Jun 02 2018 at 03:02):

I was cutting corners :-)

#### Mario Carneiro (Jun 02 2018 at 03:03):

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

#### Reid Barton (Jun 02 2018 at 03:03):

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

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

#### Johan Commelin (Jun 02 2018 at 03:22):

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

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

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

#### Johan Commelin (Jun 02 2018 at 03:25):

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

.

#### Kevin Buzzard (Jun 02 2018 at 03:28):

I've got two elements of a ring.

#### Kevin Buzzard (Jun 02 2018 at 03:28):

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

#### Kevin Buzzard (Jun 02 2018 at 03:28):

Mathematicians are great

#### Kevin Buzzard (Jun 02 2018 at 03:28):

"use a subtype"

#### Kevin Buzzard (Jun 02 2018 at 03:28):

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

#### Kevin Buzzard (Jun 02 2018 at 03:28):

Having p as a subtype is awful

#### Kevin Buzzard (Jun 02 2018 at 03:28):

`x ^ p`

#### Kevin Buzzard (Jun 02 2018 at 03:28):

Lean : ?!

#### Mario Carneiro (Jun 02 2018 at 03:29):

yeah this is going to be difficult

#### Kevin Buzzard (Jun 02 2018 at 03:29):

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

#### Mario Carneiro (Jun 02 2018 at 03:29):

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

instance

#### Kevin Buzzard (Jun 02 2018 at 03:29):

rofl

#### Kevin Buzzard (Jun 02 2018 at 03:30):

I coerce with \u?

#### Mario Carneiro (Jun 02 2018 at 03:30):

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

#### Mario Carneiro (Jun 02 2018 at 03:30):

you would have to say it's a nat

#### Mario Carneiro (Jun 02 2018 at 03:30):

`x ^ (p:nat)`

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

#### Mario Carneiro (Jun 02 2018 at 03:31):

I think that a prime typeclass might work better for you

#### Mario Carneiro (Jun 02 2018 at 03:31):

no, that's unlikely to change

#### Mario Carneiro (Jun 02 2018 at 03:31):

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

#### Mario Carneiro (Jun 02 2018 at 03:32):

it's too underdetermined

#### Johan Commelin (Jun 02 2018 at 03:32):

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

#### Kevin Buzzard (Jun 02 2018 at 03:32):

wait

#### Kevin Buzzard (Jun 02 2018 at 03:32):

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

#### Kevin Buzzard (Jun 02 2018 at 03:32):

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

#### Mario Carneiro (Jun 02 2018 at 03:33):

you have `algebra.group_power`

?

#### Kevin Buzzard (Jun 02 2018 at 03:33):

I have one lying around somewhere

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

#### Kevin Buzzard (Jun 02 2018 at 03:36):

Is that just a bridge too far?

#### Kevin Buzzard (Jun 02 2018 at 03:37):

so if the predicate is called `prime`

and the subtype `Prime`

, what is the typeclass called?

#### Kevin Buzzard (Jun 02 2018 at 03:37):

`is_prime`

I guess?

#### Kevin Buzzard (Jun 02 2018 at 05:01):

eew

#### Kevin Buzzard (Jun 02 2018 at 05:01):

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

#### Kevin Buzzard (Jun 02 2018 at 05:02):

is that going away in Lean 4?

#### Mario Carneiro (Jun 02 2018 at 05:02):

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

#### Kevin Buzzard (Jun 02 2018 at 05:02):

you're going to use sites?

#### Mario Carneiro (Jun 02 2018 at 05:03):

nothing but pointless topology for us

#### Johan Commelin (Jun 02 2018 at 05:03):

No, infty-topoi.

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

#### Mario Carneiro (Jun 02 2018 at 05:04):

much better

#### Johan Commelin (Jun 02 2018 at 05:06):

Kevin, so the problem is that `topological_ring`

should imply `ring`

and `topological_space`

, right?

#### Kevin Buzzard (Jun 02 2018 at 05:07):

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

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

#### Kevin Buzzard (Jun 02 2018 at 05:08):

I tried using type class inference

#### Kevin Buzzard (Jun 02 2018 at 05:08):

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

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

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

#### Kevin Buzzard (Jun 02 2018 at 05:10):

I have typeclass woes

#### Kevin Buzzard (Jun 02 2018 at 05:10):

I am writing my flagship definition

#### Kevin Buzzard (Jun 02 2018 at 05:10):

so it has to look lovely

#### Kevin Buzzard (Jun 02 2018 at 05:10):

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

#### Kevin Buzzard (Jun 02 2018 at 05:10):

and curse the `p`

#### Kevin Buzzard (Jun 02 2018 at 05:11):

and it complains that it can't see why `R i`

is a Tate ring

#### Mario Carneiro (Jun 02 2018 at 05:11):

because perfectoid ring depends on Tate ring

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

#### Mario Carneiro (Jun 02 2018 at 05:13):

since `perfectoid_ring `

takes the other two as parameters

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

#### Kevin Buzzard (Jun 02 2018 at 05:16):

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

#### Kevin Buzzard (Jun 02 2018 at 05:16):

works but looks silly

#### Kevin Buzzard (Jun 02 2018 at 05:16):

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

#### Mario Carneiro (Jun 02 2018 at 05:17):

It can't synthesize any of those classes

#### Mario Carneiro (Jun 02 2018 at 05:17):

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

#### Johan Commelin (Jun 02 2018 at 05:17):

So, you should extend Tate_ring?

#### Mario Carneiro (Jun 02 2018 at 05:17):

use `by exactI`

to workaround

#### Kevin Buzzard (Jun 02 2018 at 05:17):

but I don't want by exactI everywhere

#### Kevin Buzzard (Jun 02 2018 at 05:17):

it's an ugly hack

#### Mario Carneiro (Jun 02 2018 at 05:18):

Wait we're talking about different things again

#### Mario Carneiro (Jun 02 2018 at 05:18):

to make Tate_ring inferrable from perfectoid_ring, just make it `extends`

the other

#### Mario Carneiro (Jun 02 2018 at 05:19):

instead of taking it as parameter

#### Kevin Buzzard (Jun 02 2018 at 05:23):

I changed for a reason

#### Mario Carneiro (Jun 02 2018 at 05:25):

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

#### Kevin Buzzard (Jun 02 2018 at 05:30):

I didn't know how to reduce mod p offhand

#### Kevin Buzzard (Jun 02 2018 at 05:31):

so just wrote something mathematically equivalent

#### Kevin Buzzard (Jun 02 2018 at 05:31):

reducing mod p would be fine

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

#### Mario Carneiro (Jun 02 2018 at 05:32):

or you could write `p | b ^ p - a`

#### Kevin Buzzard (Jun 02 2018 at 05:32):

try that with a subtype

#### Mario Carneiro (Jun 02 2018 at 05:33):

?

#### Kevin Buzzard (Jun 02 2018 at 05:33):

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

#### Kevin Buzzard (Jun 02 2018 at 05:33):

for p

#### Mario Carneiro (Jun 02 2018 at 05:34):

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

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

#### Kevin Buzzard (Jun 02 2018 at 05:36):

b has type some strange smiley

#### Kevin Buzzard (Jun 02 2018 at 05:37):

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

#### Kevin Buzzard (Jun 02 2018 at 05:37):

looks less cool

#### Johan Commelin (Jun 02 2018 at 05:48):

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

#### Mario Carneiro (Jun 02 2018 at 05:49):

why? that seems plenty readable

#### Mario Carneiro (Jun 02 2018 at 05:49):

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

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

#### Johan Commelin (Jun 02 2018 at 05:50):

And then `(p : R ᵒ)`

will already scare them away.

#### Johan Commelin (Jun 02 2018 at 05:50):

Why is it even there?

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

#### Johan Commelin (Jun 02 2018 at 05:51):

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

?

#### Mario Carneiro (Jun 02 2018 at 05:51):

yes, that's why I suggested `\u p`

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

#### Johan Commelin (Jun 02 2018 at 05:53):

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

#### Johan Commelin (Jun 02 2018 at 05:54):

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

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

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

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

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

#### Kevin Buzzard (Jun 03 2018 at 21:32):

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

#### Kevin Buzzard (Jun 03 2018 at 21:33):

So I can envisage several ways of setting this up

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

#### Kevin Buzzard (Jun 03 2018 at 21:34):

so how do I analyse this further?

#### Kevin Buzzard (Jun 03 2018 at 21:34):

I definitely want easy access to $R$

#### Kevin Buzzard (Jun 03 2018 at 21:36):

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

#### Kevin Buzzard (Jun 03 2018 at 21:36):

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

#### Kevin Buzzard (Jun 03 2018 at 21:37):

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

#### Kevin Buzzard (Jun 03 2018 at 21:37):

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

#### Kevin Buzzard (Jun 03 2018 at 21:37):

"so mostly you don't notice"

#### Kevin Buzzard (Jun 03 2018 at 21:38):

and everything will be a topological ring

#### Kevin Buzzard (Jun 03 2018 at 21:38):

and every map will be continuous

#### Kevin Buzzard (Jun 03 2018 at 21:39):

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

#### Kevin Buzzard (Jun 03 2018 at 21:39):

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

#### Kevin Buzzard (Jun 03 2018 at 21:40):

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

#### Kevin Buzzard (Jun 03 2018 at 21:41):

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

#### Kevin Buzzard (Jun 03 2018 at 22:28):

I'm going to make a structure containing $R$ and $R^+$, and rely on `has_coe_to_sort`

to enable me to treat it as `R`

.

#### Kevin Buzzard (Jun 03 2018 at 22:29):

Is there trouble ahead?

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

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

?

#### Kenny Lau (Jun 03 2018 at 22:50):

we have all about that in `linear_algebra/something`

I think

#### Kenny Lau (Jun 03 2018 at 22:51):

they proved that every vector space has a basis

#### Kevin Buzzard (Jun 03 2018 at 22:51):

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

#### Kevin Buzzard (Jun 03 2018 at 22:51):

it's the finiteness I am interested in

#### Kevin Buzzard (Jun 03 2018 at 22:51):

I just want a smooth way of formalizing that definition

#### Kevin Buzzard (Jun 03 2018 at 22:51):

p46 of the pdf

#### Kenny Lau (Jun 03 2018 at 22:51):

finiteness is just either `fintype`

or `set.finite`

#### Kevin Buzzard (Jun 03 2018 at 22:52):

OK I'll write something

#### Kevin Buzzard (Jun 03 2018 at 22:52):

and then you can laugh at me :-)

#### Kenny Lau (Jun 03 2018 at 22:52):

/-- Linear span of a set of vectors -/ def span (s : set β) : set β := { x | ∃(v : lc α β), (∀x∉s, v x = 0) ∧ x = v.sum (λb a, a • b) }

#### Kenny Lau (Jun 03 2018 at 22:52):

https://github.com/leanprover/mathlib/blob/master/linear_algebra/basic.lean#L122

#### Kevin Buzzard (Jun 03 2018 at 22:52):

Oh!

#### Kevin Buzzard (Jun 03 2018 at 22:52):

I forgot -- see you on the R thread

#### Kevin Buzzard (Jun 03 2018 at 23:45):

Does this already have a name in mathlib:

#### Kevin Buzzard (Jun 03 2018 at 23:45):

`definition is_cover {X γ : Type} (U : γ → set X) := ∀ x, ∃ i, x ∈ U i`

#### Kenny Lau (Jun 03 2018 at 23:49):

lemma compact_elim_finite_subcover {s : set α} {c : set (set α)} (hs : compact s) (hc₁ : ∀t∈c, is_open t) (hc₂ : s ⊆ ⋃₀ c) : ∃c'⊆c, finite c' ∧ s ⊆ ⋃₀ c' :=

#### Kenny Lau (Jun 03 2018 at 23:49):

https://github.com/leanprover/mathlib/blob/master/analysis/topology/topological_space.lean#L475

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

#### Kevin Buzzard (Jun 03 2018 at 23:50):

Is the first one just silly or does it ever have its uses?

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

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

#### Kenny Lau (Jun 03 2018 at 23:52):

lol

#### Kevin Buzzard (Jun 03 2018 at 23:52):

it's all about the interface though

#### Kevin Buzzard (Jun 03 2018 at 23:53):

`(R⁺ : set R)`

#### Kevin Buzzard (Jun 03 2018 at 23:54):

what is this "unexpected token" error?

#### Kevin Buzzard (Jun 03 2018 at 23:54):

can I PR it in somehow?

#### Kevin Buzzard (Jun 03 2018 at 23:54):

hmm

#### Kevin Buzzard (Jun 03 2018 at 23:54):

can I use it in notation?

#### Kevin Buzzard (Jun 03 2018 at 23:56):

yes :-)

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

#### Kevin Buzzard (Jun 04 2018 at 00:07):

because of type class inference woes

#### Kevin Buzzard (Jun 04 2018 at 00:08):

`definition is_ring_of_integral_elements {R : Type} [Huber_ring R] (Rplus : set R) : Prop := sorry`

#### Kevin Buzzard (Jun 04 2018 at 00:08):

needs huber ring

#### Kevin Buzzard (Jun 04 2018 at 00:10):

*boggle* <goes back to type class woes thread>

#### Reid Barton (Jun 04 2018 at 00:11):

I don't understand why that would make the second one not compile

#### Kevin Buzzard (Jun 04 2018 at 00:15):

no I am an idiot

#### Kevin Buzzard (Jun 04 2018 at 00:15):

it works fine

#### Kevin Buzzard (Jun 04 2018 at 00:16):

I am still very unsteady on my feet with typeclasses

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

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

#### Kevin Buzzard (Jun 04 2018 at 00:22):

This is annoying

#### 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^+$

#### Kevin Buzzard (Jun 04 2018 at 00:23):

`postfix `

⁺` : 66 := λ R : Huber_pair _, R.Rplus `

#### Kevin Buzzard (Jun 04 2018 at 00:23):

and if I add it as a family of structures on R

#### Kevin Buzzard (Jun 04 2018 at 00:23):

then I am forever having to make R and then the pair

#### Kevin Buzzard (Jun 04 2018 at 00:23):

I can't just say "Let $R$ be a Huber Pair" like we'd say in maths

#### Scott Morrison (Jun 04 2018 at 00:25):

So, often a good solution when you want two different typeclasses on the same underlying type,

#### Scott Morrison (Jun 04 2018 at 00:25):

is to use the trick that Mario showed me, of making a "wrapper".

#### 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ᵒᵖ) := ...

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

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

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

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

#### Kevin Buzzard (Jun 04 2018 at 00:30):

as I explicitly evaluate my completions etc

#### Scott Morrison (Jun 04 2018 at 00:31):

Scratch that suggestion then!

#### Johan Commelin (Jun 04 2018 at 11:39):

I can't just say "Let $R$ 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⁺`

.

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

#### Reid Barton (Jun 04 2018 at 11:48):

Could that notation for the ambient ring just be a coercion?

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

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

#### Reid Barton (Jun 04 2018 at 11:52):

notation R `⁺`:99 := R.Rp variables {R : Huber_pair} {x : R} {h : x ∈ R⁺}

#### Reid Barton (Jun 04 2018 at 11:52):

Yes, probably.

#### Johan Commelin (Jun 04 2018 at 11:56):

So far that looks promising, I would say.

#### 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 $R$ as an ambiant (topological) ring, and $R^+$ as the actual interesting thing?

#### Johan Commelin (Jun 04 2018 at 12:15):

I think both rings in a Huber pair are interesting...

#### Johan Commelin (Jun 04 2018 at 12:16):

It is like $\mathbb{Z} \subset \mathbb{Q}$ on steroids.

#### 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 $T$, and then on the ideal $I$ in the second condition of the definition.

#### Johan Commelin (Jun 04 2018 at 12:19):

Disclaimer: I'm not an expert on this stuff. Only followed some seminars on this.

#### Assia Mahboubi (Jun 04 2018 at 12:42):

Sorry my sentence was misleading and in fact I think it was even nonsensical, as $A^+$ should be integrally closed in $A$.

#### Johan Commelin (Jun 04 2018 at 12:47):

~~Don't you mean it the other way round?~~

#### Assia Mahboubi (Jun 04 2018 at 12:49):

Thanks.

#### 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 $R$ as an ambiant (topological) ring, and $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.

#### Kevin Buzzard (Jun 04 2018 at 13:10):

The modern terminology is that $R$ is a Huber ring and $(R,R^+)$ is a Huber pair. In the old terminology $R$ is an f-adic ring and $R^+$ is a ring of integral elements (I guess this definition will stay)

#### Kevin Buzzard (Jun 04 2018 at 13:11):

So many of the proofs do not care about $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 $R$ and a subring $R^+$ and do calculations with them

#### Kevin Buzzard (Jun 04 2018 at 20:19):

Should I have `structure perfectoid_space := (X : Type) ...`

or `structure perfectoid_space (X : Type) := ...`

?

#### Kevin Buzzard (Jun 04 2018 at 20:19):

I was using the latter

#### Kevin Buzzard (Jun 04 2018 at 20:19):

but here's something I ran into.

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

#### 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)$, and a bit more data, and some axioms.

#### Kevin Buzzard (Jun 04 2018 at 20:23):

Given a perfectoid space $X$, and an open subset $U$ of the underlying topological space (which is also called $X$), I can pull back all the structure and get a perfectoid space structure on $U$ (e.g. I need to associate a ring to an open subset of $U$, but an open subset of $U$ is an open subset of $X$ so we use the presheaf of rings on $X$ to do this).

#### Kevin Buzzard (Jun 04 2018 at 20:23):

So far so good.

#### Kevin Buzzard (Jun 04 2018 at 20:23):

But I was kind of expecting `perfectoid_space`

to be a typeclass

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

#### Kevin Buzzard (Jun 04 2018 at 20:24):

because U is an open set in X so it's not even a type

#### Kevin Buzzard (Jun 04 2018 at 20:25):

and if we use the associated subtype `{x : X // x \in U}`

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

#### Kevin Buzzard (Jun 04 2018 at 20:25):

In short -- if I have `(X : Type) [perfectoid_space X]`

#### Kevin Buzzard (Jun 04 2018 at 20:26):

(perfectoid space extends topological space)

#### Kevin Buzzard (Jun 04 2018 at 20:26):

and if `(U : set X)`

is open

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

#### Kevin Buzzard (Jun 04 2018 at 20:28):

"an open subset of a perfectoid space is a perfectoid space"

#### Kevin Buzzard (Jun 04 2018 at 20:28):

but how is type class inference going to spot that U is open?

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

#### Kevin Buzzard (Jun 04 2018 at 20:33):

Or should I just give up on making perfectoid space a typeclass?

#### Kevin Buzzard (Jun 04 2018 at 20:34):

Presumably typeclass inference only works on things which have been tagged as classes

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

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

#### Kevin Buzzard (Jun 04 2018 at 20:52):

So I can prove that theorem

#### Kevin Buzzard (Jun 04 2018 at 20:52):

my question is whether I can persuade the type class inference system to use it

#### Kevin Buzzard (Jun 04 2018 at 20:52):

if `perfectoid_space`

is a class

#### Kevin Buzzard (Jun 04 2018 at 20:52):

and what I can't get my head around

#### Kevin Buzzard (Jun 04 2018 at 20:53):

is how type class inference can possibly guess that a subset is open

#### Nicholas Scheel (Jun 04 2018 at 20:53):

I agree, that’s why I think `is_open`

would also have to be a typeclass

#### Kevin Buzzard (Jun 04 2018 at 20:53):

but there is a technical problem there

#### Kevin Buzzard (Jun 04 2018 at 20:53):

because U is not a type

#### Kevin Buzzard (Jun 04 2018 at 20:53):

it's a term

#### Kevin Buzzard (Jun 04 2018 at 20:54):

hmm

#### Kevin Buzzard (Jun 04 2018 at 20:54):

I am just assuming that it's impossible to make this work

#### Kevin Buzzard (Jun 04 2018 at 20:54):

Does it actually work?

#### Kevin Buzzard (Jun 04 2018 at 20:55):

I somehow can't get it all to fit together but maybe it's possible

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

#### Nicholas Scheel (Jun 04 2018 at 21:00):

`class is_ring_hom`

#### Kevin Buzzard (Jun 04 2018 at 21:11):

That's true!

#### Kevin Buzzard (Jun 04 2018 at 21:11):

Maybe it all just works?

#### Kevin Buzzard (Jun 04 2018 at 21:14):

`variables {X : Type} [topological_space X]`

#### Kevin Buzzard (Jun 04 2018 at 21:15):

class is_open (U : set X) : Prop := (is_open : is_open U)

or some such thing

#### Kevin Buzzard (Jun 04 2018 at 21:16):

hmm maybe I need to think a bit about variable names...

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

)

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

#### Patrick Massot (Jun 05 2018 at 07:24):

Are doing all this privately in the end?

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

#### Kevin Buzzard (Jun 05 2018 at 08:16):

before I "went public" as it were

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

#### Kevin Buzzard (Jun 05 2018 at 08:16):

so I will look in the old thread

#### Kevin Buzzard (Jun 05 2018 at 08:45):

Patrick here's the state of things:

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

#### Kevin Buzzard (Jun 05 2018 at 08:45):

doesn't quite typecheck

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

#### Kevin Buzzard (Jun 05 2018 at 08:46):

`adic_space`

full of sorries

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

#### Kevin Buzzard (Jun 05 2018 at 08:47):

`is_preadic_space_equiv`

extends `homeo`

-- did you get that into mathlib?

#### Kevin Buzzard (Jun 05 2018 at 08:50):

The problem, by the way, is `failed to synthesize ⊢ preadic_space {x // x ∈ U i}`

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

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

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

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

#### Kevin Buzzard (Jun 05 2018 at 08:58):

This is supposed to say "my topological space has a cover by nice topological subspaces"

#### Kevin Buzzard (Jun 05 2018 at 08:58):

but the actual cover is not part of the structure

#### Kevin Buzzard (Jun 05 2018 at 08:59):

it's just the fact that such a cover exists

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

#### Kevin Buzzard (Jun 05 2018 at 09:00):

Here's a MWE of my final problem

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

#### Kevin Buzzard (Jun 05 2018 at 09:01):

I might have just made a stupid mistake

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

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

#### Kevin Buzzard (Jun 05 2018 at 09:04):

`failed to synthesize type class instance for ⊢ preadic_space {x // x ∈ U i}`

#### Kevin Buzzard (Jun 05 2018 at 09:04):

That's my problem

#### Kevin Buzzard (Jun 05 2018 at 09:05):

I think maybe type class inference doesn't know `U i`

is open

#### Kevin Buzzard (Jun 05 2018 at 09:05):

but I thought that `[U_open : ∀ i, is_open (U i)]`

would tell it this

#### Kevin Buzzard (Jun 05 2018 at 09:06):

but it might all be happening too quickly for type class inference

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

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

#### 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 $\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.

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

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

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

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

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

#### Kevin Buzzard (Jun 05 2018 at 09:33):

We can't have everything

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

#### Johan Commelin (Jun 05 2018 at 09:35):

Right, so the issue remains...

#### Johan Commelin (Jun 05 2018 at 09:35):

Which is really annoying.

#### Kevin Buzzard (Jun 05 2018 at 09:37):

Now we have weird arrows

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

#### Kevin Buzzard (Jun 05 2018 at 09:37):

It would be a shame to have to start going on about letI or whatever

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

#### Kevin Buzzard (Jun 05 2018 at 09:38):

I don't actually understand what is going on

#### Kevin Buzzard (Jun 05 2018 at 09:38):

I don't understand what the "type class inference machine" has access to at any time

#### Kevin Buzzard (Jun 05 2018 at 09:38):

For example I am not even sure if it knows X is an adic space

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

.

#### Johan Commelin (Jun 05 2018 at 09:41):

But it hasn't actually done it!

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

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

.

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

"

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

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

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

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

#### Kevin Buzzard (Jun 05 2018 at 11:27):

Kenny suggested making another typeclass for subtypes being open

#### Johan Commelin (Jun 05 2018 at 11:28):

I don't see why that would fix things...

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

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

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

#### Kevin Buzzard (Jun 05 2018 at 11:34):

I doubt it's a bug.

#### Kevin Buzzard (Jun 05 2018 at 11:34):

It's probably just how typeclass inference works

#### Johan Commelin (Jun 05 2018 at 11:34):

Yes, I also think that now.

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

?

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

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

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

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

#### Johan Commelin (Jun 05 2018 at 11:46):

Aah, because of a long chain of `extends`

, right?

#### Johan Commelin (Jun 05 2018 at 11:47):

Right, that makes a lot (*a whole lot*!) of sense

#### Johan Commelin (Jun 05 2018 at 11:47):

It has been staring us right in the face, all the time.

#### Johan Commelin (Jun 05 2018 at 11:47):

So it is just some stupid overloading, and preferably one of the two `is_open`

s should have another name.

#### Johan Commelin (Jun 05 2018 at 11:56):

Anyway, @Gabriel Ebner thanks for enlightening me!

#### Johan Commelin (Jun 05 2018 at 11:57):

@Kevin Buzzard 'nother problem solved. Next!

#### Kevin Buzzard (Jun 05 2018 at 11:58):

Definition currently looks like this:

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

#### Kevin Buzzard (Jun 05 2018 at 11:59):

Typechecks fine

#### Kevin Buzzard (Jun 05 2018 at 11:59):

The `is_open`

overloading is one thing

#### Johan Commelin (Jun 05 2018 at 11:59):

I guess you can remove the `@`

and the `X _ `

#### Kevin Buzzard (Jun 05 2018 at 11:59):

yes

#### Kevin Buzzard (Jun 05 2018 at 12:00):

thanks

#### Johan Commelin (Jun 05 2018 at 12:00):

And just a `(U i)`

on the last line? Instead of all the `{x ... }`

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

#### Kevin Buzzard (Jun 05 2018 at 12:03):

I'm not happy with that `_root_`

but everything else is great

#### Johan Commelin (Jun 05 2018 at 12:03):

Yes, completely agree.

#### Johan Commelin (Jun 05 2018 at 12:03):

We should just overhaul the definition in `topological_space.lean`

#### Johan Commelin (Jun 05 2018 at 12:04):

It's only a silly namespacing issue.

#### Johan Commelin (Jun 05 2018 at 12:04):

I it has a field `open_subsets`

instead of `is_open`

, then we're fine.

#### Kevin Buzzard (Jun 05 2018 at 12:05):

can I fix this by writing my own `open`

or `is_open'`

or whatever?

#### Reid Barton (Jun 05 2018 at 12:06):

Probably even `notation `is_open` := _root_.is_open`

would work

#### Kevin Buzzard (Jun 05 2018 at 12:06):

Here's the full file

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

#### Kevin Buzzard (Jun 05 2018 at 12:07):

I am really happy with all of it apart from the `_root_`

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

#### Reid Barton (Jun 05 2018 at 12:08):

except now I can't find any

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

.

#### Johan Commelin (Jun 05 2018 at 13:20):

And we have 6 commits! The game is on!

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

#### Kevin Buzzard (Jun 05 2018 at 14:19):

Yeah, it should run. I have absolutely no idea about git workflows.

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

#### Johan Commelin (Jun 05 2018 at 15:11):

Ok, so this is your chance to level-up in git!

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

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

#### Johan Commelin (Jun 05 2018 at 16:56):

I like it that you moved the `_root_`

issue out of the perfectoid file

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

#### Patrick Massot (Jun 05 2018 at 19:01):

Is there a reason why `perfectoid_spaces.lean`

is not inside the `src`

directory?

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

#### Patrick Massot (Jun 05 2018 at 19:16):

Why not using ϖ (\varpi)?

#### Patrick Massot (Jun 05 2018 at 19:16):

Here it looks ugly but in my VScode it looks ok

#### Patrick Massot (Jun 05 2018 at 19:18):

Why the space in `R ᵒ`

? It works fine and looks better as `Rᵒ`

#### Patrick Massot (Jun 05 2018 at 19:18):

I'm such an expert about perfectoid spaces now...

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

#### Patrick Massot (Jun 05 2018 at 19:27):

Is there any reason to use gamma instead of iota for the indexing type?

#### Kevin Buzzard (Jun 05 2018 at 19:27):

no

#### Patrick Massot (Jun 05 2018 at 19:27):

iota is the mathlib tradition, and consistent with using `i`

as a variable name

#### Kevin Buzzard (Jun 05 2018 at 19:27):

OK

#### Patrick Massot (Jun 05 2018 at 19:27):

I guess the thing is never named in math papers

#### Kevin Buzzard (Jun 05 2018 at 19:27):

I can change all these things. Thanks for the review!

#### Patrick Massot (Jun 05 2018 at 19:28):

Now, serious question:

#### Kevin Buzzard (Jun 05 2018 at 19:28):

$\coprod R_i$

#### Kevin Buzzard (Jun 05 2018 at 19:28):

who needs a name for the index set

#### Kevin Buzzard (Jun 05 2018 at 19:28):

maybe I'll call it `_`

#### Mario Carneiro (Jun 05 2018 at 19:28):

You should not use existential quantification over `Type`

in your definition

#### Kevin Buzzard (Jun 05 2018 at 19:28):

eew

#### Mario Carneiro (Jun 05 2018 at 19:28):

for the index set

#### Kevin Buzzard (Jun 05 2018 at 19:28):

Is this the thing Assia was also unhappy about?

#### Mario Carneiro (Jun 05 2018 at 19:28):

Yes

#### Patrick Massot (Jun 05 2018 at 19:28):

What about this strange way of putting things before and after the existential comma?

#### Mario Carneiro (Jun 05 2018 at 19:29):

It will needlessly push up the universe level of the definition

#### Kevin Buzzard (Jun 05 2018 at 19:29):

How do you do it then?

#### Patrick Massot (Jun 05 2018 at 19:29):

And why naming instance implicit variables you don't use in the def?

#### Reid Barton (Jun 05 2018 at 19:29):

Even though it's inside an `\ex`

?

#### Mario Carneiro (Jun 05 2018 at 19:29):

Instead you should quantify over all families that could possibly matter

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

#### Patrick Massot (Jun 05 2018 at 19:29):

Does it make any difference (what I wrote vs Kevin's version)?

#### Mario Carneiro (Jun 05 2018 at 19:30):

oh, actually reid you're right, impredicativity makes it okay

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

#### Mario Carneiro (Jun 05 2018 at 19:30):

Still, I would prefer to quantify over subsets of set X

#### Gabriel Ebner (Jun 05 2018 at 19:30):

Maybe you should make `ι`

a field of `perfectoid_space`

(and the others as well).

#### Mario Carneiro (Jun 05 2018 at 19:31):

unless there is a reason that having many duplicates adds power?

#### Patrick Massot (Jun 05 2018 at 19:31):

What Gabriel says was my next question

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

#### Patrick Massot (Jun 05 2018 at 19:32):

I agree it looks more mathematicial, I'm asking if this will bring pain

#### Mario Carneiro (Jun 05 2018 at 19:32):

alternatively, name the thing "perfectoid cover" or something and existentially quantify in the structure

#### Patrick Massot (Jun 05 2018 at 19:32):

^ also sounds nice

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

#### Patrick Massot (Jun 05 2018 at 19:33):

But again it would sound further away from math-speak

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

.

#### Mario Carneiro (Jun 05 2018 at 19:33):

or "powerset"

#### Kevin Buzzard (Jun 05 2018 at 19:34):

My definition is readable by mathematicians

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

#### Kevin Buzzard (Jun 05 2018 at 19:34):

and I don't understand what the problem with it is yet

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

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

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

#### Kevin Buzzard (Jun 05 2018 at 19:35):

and the claim is that my perfectoid space has a covering by these "special" spaces

#### Mario Carneiro (Jun 05 2018 at 19:35):

that's the theorem

#### Patrick Massot (Jun 05 2018 at 19:35):

What Reid wrote seems important to me

#### Kevin Buzzard (Jun 05 2018 at 19:35):

@Patrick Massot yes it's just an honest covering of a topological space by open subsets

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

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

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

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

#### Kevin Buzzard (Jun 05 2018 at 19:36):

A perfectoid space is a space for which such a cover exists

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

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

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

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

#### Mario Carneiro (Jun 05 2018 at 19:39):

just use `U : set (opens X)`

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

#### Reid Barton (Jun 05 2018 at 19:40):

for more readability, it should probably be more like `cover : set (opens X)`

#### Reid Barton (Jun 05 2018 at 19:40):

Oh wait, you already have an example of the issue I was bringing up earlier here.

#### Reid Barton (Jun 05 2018 at 19:41):

We also have this `(A : ι → Huber_pair) [∀ i, perfectoid_ring (A i) p]`

stuff

#### Mario Carneiro (Jun 05 2018 at 19:41):

BTW I think the `p`

should come first

#### Mario Carneiro (Jun 05 2018 at 19:41):

because it's the parameter

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

#### Patrick Massot (Jun 05 2018 at 19:43):

He doesn't want to get it back

#### Patrick Massot (Jun 05 2018 at 19:43):

It's not part of the structure

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

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

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

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

#### Mario Carneiro (Jun 05 2018 at 19:52):

that's what makes the theorem not completely trivial

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

#### Patrick Massot (Jun 05 2018 at 19:53):

theorem claiming this doesn't matter?

#### Mario Carneiro (Jun 05 2018 at 19:53):

right

#### Reid Barton (Jun 05 2018 at 19:53):

Or, maybe you can?

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

#### Patrick Massot (Jun 05 2018 at 19:54):

Huh, why not?

Because it wouldn't be correct

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

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

#### Patrick Massot (Jun 05 2018 at 19:54):

You can build exotic spheres by gluing two open balls

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

#### Patrick Massot (Jun 05 2018 at 19:55):

All the exotictness is in the gluing map

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

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

#### Mario Carneiro (Jun 05 2018 at 19:57):

maybe the Huber pairs can't get that large either

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

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

#### Patrick Massot (Jun 05 2018 at 19:58):

anyway, let's focus on the perfectoid case

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

#### Mario Carneiro (Jun 05 2018 at 19:59):

it's an arbitrary stopping point in the ZFC world

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

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

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

#### Patrick Massot (Jun 05 2018 at 20:04):

You can define smooth manifolds as ringed space, see https://bookstore.ams.org/gsm-65

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

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

#### Kevin Buzzard (Jun 05 2018 at 20:07):

hmm

#### Kevin Buzzard (Jun 05 2018 at 20:07):

maybe the size of the real numbers

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

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

#### Johan Commelin (Jun 05 2018 at 20:16):

Which "chapter 4" are we referring to?

#### Patrick Massot (Jun 05 2018 at 20:16):

https://arxiv.org/abs/1709.07343

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

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

#### Kevin Buzzard (Jun 05 2018 at 20:18):

Maybe some list of links on the README?

#### Johan Commelin (Jun 05 2018 at 20:19):

Yes, that should be fine.

#### Johan Commelin (Jun 05 2018 at 20:19):

I can PR the readme tomorrow

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

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

#### Assia Mahboubi (Jun 05 2018 at 21:00):

It would also be great to have a "Getting it working" section in your README.

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

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

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

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

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

#### Kevin Buzzard (Jun 05 2018 at 21:56):

And of course, many thanks to those who have already commented!

#### Kevin Buzzard (Jun 05 2018 at 22:43):

*boggle* Every change I made bring new typeclass inference problems

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

#### Kenny Lau (Jun 05 2018 at 22:44):

𝓤

#### Kevin Buzzard (Jun 05 2018 at 22:44):

and now I'm back with failing to synthesize `⊢ preadic_space ↥U`

#### Kevin Buzzard (Jun 05 2018 at 22:45):

𝓤

Collection of open sets

#### Kevin Buzzard (Jun 05 2018 at 22:45):

except that Lean does not notice they're open

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

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

#### Kevin Buzzard (Jun 05 2018 at 23:04):

I've given up on typeclass inference because it's midnight.

#### Kevin Buzzard (Jun 05 2018 at 23:05):

In the old version above, I had `is_preadic_space_equiv (U i) (Spa (A i))`

#### Kevin Buzzard (Jun 05 2018 at 23:05):

and the preadic space structure on `U i`

came from typeclass inference.

#### Kevin Buzzard (Jun 05 2018 at 23:05):

I can't get it to work for U in some covering set

#### Kevin Buzzard (Jun 05 2018 at 23:05):

but this works:

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

#### Kevin Buzzard (Jun 05 2018 at 23:06):

`preadic_space_pullback U`

is just `U`

again :-) (actually it's {x : X // x \in U})

#### Kevin Buzzard (Jun 05 2018 at 23:07):

but the instance can key on it

#### Kevin Buzzard (Jun 05 2018 at 23:07):

I only half-know what those words mean

#### Kevin Buzzard (Jun 05 2018 at 23:07):

but type class inference works with this trick

#### Mario Carneiro (Jun 06 2018 at 01:25):

I said `set (opens X)`

for a reason

#### Mario Carneiro (Jun 06 2018 at 01:26):

it's past time you had a `opens X`

type of open subsets of X

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

#### Johan Commelin (Jun 06 2018 at 03:25):

That seems very readable to me. And I basically just squashed some lines together.

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

#### Mario Carneiro (Jun 06 2018 at 07:10):

Yes. You will also want a `has_mem A (opens A)`

instance

#### Mario Carneiro (Jun 06 2018 at 07:11):

You could also use `subtype`

for the definition

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

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

#### Johan Commelin (Jun 06 2018 at 07:32):

Done.

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

#### Johan Commelin (Jun 06 2018 at 07:33):

And it doesn't help if I change `set (set X)`

to `set (opens X)`

.

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

#### Johan Commelin (Jun 06 2018 at 07:42):

Never mind... error was between keyboard and chair.

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

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

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

#### Mario Carneiro (Jun 06 2018 at 07:55):

Well, you can use `[fixed_prime]`

plus `fixed_prime.p`

to avoid the coercion stuff

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

#### Johan Commelin (Jun 06 2018 at 07:57):

Look ma! No primes in our type signatures!

#### Johan Commelin (Jun 06 2018 at 07:58):

#check @perfectoid_space -- perfectoid_space : Π [_inst_1 : nat.Prime], Type → Type

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

?

#### Kevin Buzzard (Jun 06 2018 at 08:08):

It's just random -- like in Lean. It's `group`

but `is_group_hom`

right?

#### Mario Carneiro (Jun 06 2018 at 08:08):

`is_group_hom`

because that's a prop

#### Mario Carneiro (Jun 06 2018 at 08:09):

`group`

is not

#### Kevin Buzzard (Jun 06 2018 at 08:09):

Aah!

#### Kevin Buzzard (Jun 06 2018 at 08:09):

So how about `is_perfectoid_space`

#### Kevin Buzzard (Jun 06 2018 at 08:09):

because it's an adic space plus some prop

#### Johan Commelin (Jun 06 2018 at 08:11):

I guess that makes sense. And similarly `is_perfectoid_ring`

, and I guess `is_ramified`

.

#### Johan Commelin (Jun 06 2018 at 08:12):

Hmmm, but `group`

is also just a `monoid`

with some props, right?

#### Kevin Buzzard (Jun 06 2018 at 08:15):

But maybe its type is not Prop

#### Kevin Buzzard (Jun 06 2018 at 08:15):

That's the distinction I think

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

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

?

#### Kevin Buzzard (Jun 06 2018 at 08:49):

If you search for "perfect ring" then you get ads for weddings

#### Kevin Buzzard (Jun 06 2018 at 08:50):

I thought Frobenius was bijective for a perfect ring, not surjective. What do you think?

#### Johan Commelin (Jun 06 2018 at 08:50):

Hmm, you are probably right

#### Johan Commelin (Jun 06 2018 at 08:51):

Bam! https://github.com/kbuzzard/lean-perfectoid-spaces/pull/1

#### Johan Commelin (Jun 06 2018 at 08:52):

@Kevin Buzzard Your first PR (-;

#### Kevin Buzzard (Jun 06 2018 at 08:52):

I've pushed Kenny's valuation stuff by the way (first chapter of Wedhorn)

#### Johan Commelin (Jun 06 2018 at 08:53):

And there is also https://github.com/jcommelin/lean-perfectoid-spaces/tree/opens

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

#### Kevin Buzzard (Jun 06 2018 at 08:54):

if we decided to spare them

#### Johan Commelin (Jun 06 2018 at 08:54):

Which defines the `opens`

class. And uses it in the `perfectoid_space`

definition.

#### Johan Commelin (Jun 06 2018 at 08:56):

Kevin, should I also PR the `opens`

stuff? Or do you not like that direction?

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

#### Kevin Buzzard (Jun 06 2018 at 08:56):

it's past time you had a

`opens X`

type of open subsets of X

Ohh!

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

#### Kenny Lau (Jun 06 2018 at 09:02):

you can coerce a subset to a subtype anytime

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

#### Kevin Buzzard (Jun 06 2018 at 09:02):

[I can't clarify, I can coerce]

#### Kevin Buzzard (Jun 06 2018 at 09:02):

Random screed by Hazewinkel claims perfect is bijective \lam x, x^p

#### Johan Commelin (Jun 06 2018 at 09:03):

Ok, so `Frob`

it is. I already reverted it on my branch.

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

#### Patrick Massot (Jun 06 2018 at 10:40):

Do we have a roadmap saying which parts of Wedhorn are needed?

#### Johan Commelin (Jun 06 2018 at 10:58):

It is equivalent up to a choice, right?

#### Johan Commelin (Jun 06 2018 at 10:58):

And I think the roadmap is under construction.

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

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

#### Kevin Buzzard (Jun 06 2018 at 12:13):

I keep trying to do everything

#### Kevin Buzzard (Jun 06 2018 at 12:13):

maybe I should post some basic info and then work on it more

#### Johan Commelin (Jun 06 2018 at 17:04):

Yes, some issues with basics would be totally fine.

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

#### Kenny Lau (Jun 06 2018 at 18:06):

@Kevin Buzzard

#### Kenny Lau (Jun 06 2018 at 18:06):

he proved local langland for GL(n) :o

#### Patrick Massot (Jun 06 2018 at 18:07):

Yes it's that level: stuff Scholze reproved when he was a 1st year undergrad

#### Patrick Massot (Jun 06 2018 at 18:07):

very impressive from Guy

#### Kenny Lau (Jun 06 2018 at 18:07):

"Une preuve simple des conjectures de Langlands pour GL(n) sur un corps p-adique"

#### Kenny Lau (Jun 06 2018 at 18:07):

"une preuve simple"

#### Kenny Lau (Jun 06 2018 at 18:08):

and one of my body parts is made of chicken

#### Reid Barton (Jun 06 2018 at 18:08):

maybe the proof has no nontrivial subproofs

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

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

#### Patrick Massot (Jun 06 2018 at 18:11):

Johan: yes, this is why I tell this story here. It was a pretty unusual reaction

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

#### Patrick Massot (Jun 06 2018 at 18:12):

Next week I should try to ask Serre what he thinks about proof assistants

#### Johan Commelin (Jun 06 2018 at 18:12):

Trollolol

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

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

#### Patrick Massot (Jun 06 2018 at 18:21):

It looks like it's almost done

#### Johan Commelin (Jun 06 2018 at 18:21):

If Scholze showed some interest, and now Henniart...

#### Kenny Lau (Jun 06 2018 at 18:21):

who is Rio?

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

#### Kevin Buzzard (Jun 07 2018 at 19:41):

https://github.com/kbuzzard/lean-perfectoid-spaces/issues/3

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

#### Patrick Massot (Jun 07 2018 at 19:43):

"Page numbers are all for Huber's notes." I guess you meant Wedhorn?

#### Kevin Buzzard (Jun 07 2018 at 19:43):

ooh thanks

#### Kevin Buzzard (Jun 07 2018 at 19:43):

I do that a lot!

#### Patrick Massot (Jun 07 2018 at 19:44):

Lean 7 will tell you about such typos on Github

#### Patrick Massot (Jun 07 2018 at 19:48):

I'm not sure I understand the dependency graph

#### Kevin Buzzard (Jun 07 2018 at 19:49):

I'm not surprised

#### Kevin Buzzard (Jun 07 2018 at 19:49):

Should I explain it?

#### Kevin Buzzard (Jun 07 2018 at 19:49):

In the issue, I mean?

#### Patrick Massot (Jun 07 2018 at 19:49):

It would help if you want help on this

#### Patrick Massot (Jun 07 2018 at 19:50):

Because currently it's not clear how the work could be divided

#### Patrick Massot (Jun 07 2018 at 19:51):

Is Spv(A) a typo or something different from Spa(A)?

#### Patrick Massot (Jun 07 2018 at 19:51):

Maybe v is valuation?

#### Kevin Buzzard (Jun 07 2018 at 19:51):

something different

#### Kevin Buzzard (Jun 07 2018 at 19:51):

I didn't make the notation

#### Patrick Massot (Jun 07 2018 at 19:51):

it appears only once in the issue

#### Kevin Buzzard (Jun 07 2018 at 19:52):

It's an auxilary definition :-)

#### Kevin Buzzard (Jun 07 2018 at 19:52):

I'll add some comments

#### Patrick Massot (Jun 07 2018 at 19:55):

Roughly, how many pages of Wedhorn are actually required for this definition of adic spaces?

#### Kevin Buzzard (Jun 07 2018 at 20:05):

In retrospect I don't think that many.

#### Kevin Buzzard (Jun 07 2018 at 20:06):

The hard work might be proving that an affinoid adic space is an adic space

#### Kevin Buzzard (Jun 07 2018 at 20:06):

however

#### Kevin Buzzard (Jun 07 2018 at 20:06):

that might be easier than proving that an affine scheme is a scheme

#### Kevin Buzzard (Jun 07 2018 at 20:06):

because O_X is a sheaf on Spec(R)

#### Kevin Buzzard (Jun 07 2018 at 20:06):

and the analogous fact for Spa(R) is not true

#### Kevin Buzzard (Jun 07 2018 at 20:06):

so an affinoid adic space is Spa(R) for an R for which it is true

#### Kevin Buzzard (Jun 07 2018 at 20:07):

Aah, I've got it

#### Kevin Buzzard (Jun 07 2018 at 20:07):

The hard thing will be proving that an affinoid perfectoid space is a perfectoid space

#### Kevin Buzzard (Jun 07 2018 at 20:07):

That will need far more stuff

#### Kevin Buzzard (Jun 07 2018 at 20:10):

but we don't need to advertise that, right? ;-)

#### Patrick Massot (Jun 07 2018 at 20:11):

Is there any easier example of a perfectoid space?

#### Kevin Buzzard (Jun 07 2018 at 20:12):

The empty space

#### Kevin Buzzard (Jun 07 2018 at 20:12):

there is literally no simple example of a perfectoid space other than this

#### Patrick Massot (Jun 07 2018 at 20:12):

That's what I feared

#### Kevin Buzzard (Jun 07 2018 at 20:12):

because the second simplest example is Spa(K,K^o) with K a perfectoid field

#### Patrick Massot (Jun 07 2018 at 20:12):

So we can't really escape that example

#### Kevin Buzzard (Jun 07 2018 at 20:12):

well, at least it's a field

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

#### Kevin Buzzard (Jun 07 2018 at 20:13):

don't worry, it's algebraically closed

#### Kevin Buzzard (Jun 07 2018 at 20:13):

you don't have to go on forever

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

#### Kevin Buzzard (Jun 07 2018 at 20:13):

We number theorists tell people that C_p is our version of the complex numbers

#### Patrick Massot (Jun 07 2018 at 20:14):

Corollary 3.20 in the diamonds paper

#### Kevin Buzzard (Jun 07 2018 at 20:14):

Oh yeah the tilting thing needs a whole bunch of commutative algebra

#### Kevin Buzzard (Jun 07 2018 at 20:14):

almost etale extensions

#### Kevin Buzzard (Jun 07 2018 at 20:14):

probably cotangent complex

#### Kevin Buzzard (Jun 07 2018 at 20:14):

although actually maybe you could instead use my work with Verberkmoes

#### Kevin Buzzard (Jun 07 2018 at 20:15):

a bunch of almost mathematics though

#### Kevin Buzzard (Jun 07 2018 at 20:15):

derived categories

#### Kevin Buzzard (Jun 07 2018 at 20:15):

yeah it would be a good challenge

#### Kevin Buzzard (Jun 07 2018 at 20:15):

If you did that then serious people would get interested

#### Kevin Buzzard (Jun 07 2018 at 20:16):

because that is like an odd order theorem but one that people are interested in

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

#### Patrick Massot (Jun 07 2018 at 20:18):

doesn't looks too bad

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

#### Kevin Buzzard (Jun 07 2018 at 20:24):

A huge generalisation of Fontaine-Wintenberger and Faltings

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

#### Patrick Massot (Jun 07 2018 at 20:31):

Is there anything simpler but still significant that could be proved about those spaces?

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

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

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

#### Kevin Buzzard (Jun 08 2018 at 06:47):

I now think they are. But there's a different question, which is much more complicated:

#### Kevin Buzzard (Jun 08 2018 at 06:47):

how to get one non-trivial theorem about one non-trivial object into these systems?

#### Kevin Buzzard (Jun 08 2018 at 06:47):

And that will cost time and money

#### Kevin Buzzard (Jun 08 2018 at 06:48):

it's not just a "hobby project" like defining a perfectoid space

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

#### Kevin Buzzard (Jun 08 2018 at 06:49):

and this will come up

#### Johan Commelin (Jun 08 2018 at 06:49):

Ok, good luck!

#### Johan Commelin (Jun 08 2018 at 06:49):

Sounds like today is an important day

#### Kevin Buzzard (Jun 08 2018 at 06:49):

but if they're not interested then I don't quite know what happens next

#### Kevin Buzzard (Jun 08 2018 at 06:49):

I guess I am more interested in hearing their thoughts about setting up something big

#### Kevin Buzzard (Jun 08 2018 at 06:50):

and whether they'd encourage me to apply for funding

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

#### Kevin Buzzard (Jun 08 2018 at 07:34):

I don't think any decisions will be made today!

#### Kevin Buzzard (Jun 08 2018 at 07:34):

But there will be a chance to test the water.

#### Kevin Buzzard (Jun 08 2018 at 07:52):

www.math.columbia.edu/~harris/otherarticles_files/perfectoid.pdf

#### Kevin Buzzard (Jun 08 2018 at 07:52):

I hadn't been aware of this article until the other day

#### Johan Commelin (Jun 08 2018 at 07:55):

The introduction is really nice.

#### Kevin Buzzard (Jun 08 2018 at 08:23):

[sorry, double post fail]

#### Johan Commelin (Jun 08 2018 at 10:30):

Kevin, do we even need the notion of Tate ring?

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

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

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

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

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

#### Johan Commelin (Jun 08 2018 at 13:34):

And have all the code be utterly unreadable to mathematicians...

#### Johan Commelin (Jun 08 2018 at 13:34):

By the way, Kevin, are the meetings over yet? Were they receptive to your ideas/plans?

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

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

#### Johan Commelin (Jun 08 2018 at 14:14):

But there is still a sorry to turn an ideal into a module.

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

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

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

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

#### Kevin Buzzard (Jun 08 2018 at 19:14):

I just have no idea how to run a project like this.

#### Johan Commelin (Jun 08 2018 at 19:15):

No, I would just go with the dependency.

#### Johan Commelin (Jun 08 2018 at 19:15):

And move on to interesting stuff (-;

#### Kevin Buzzard (Jun 08 2018 at 19:15):

Ok then I'll add the dependency. Can it wait a day? Can you do it?

#### Johan Commelin (Jun 08 2018 at 19:15):

I did it.

#### Kevin Buzzard (Jun 08 2018 at 19:15):

I have relatives here so I should go

#### Johan Commelin (Jun 08 2018 at 19:15):

Shall I PR?

#### Kevin Buzzard (Jun 08 2018 at 19:15):

thanks

#### Kevin Buzzard (Jun 08 2018 at 19:15):

yes please PR

#### Johan Commelin (Jun 08 2018 at 19:15):

Aaah, ok, see you later.

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

#### Johan Commelin (Jun 08 2018 at 19:17):

Well, I'm a newbie... so maybe you want to improve little things...

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

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

#### Johan Commelin (Jun 08 2018 at 19:26):

You can have tick boxes in Github issues, right?

#### Patrick Massot (Jun 08 2018 at 19:26):

Do perfectoid spaces include non commutative groups with additive notations?

#### Johan Commelin (Jun 08 2018 at 19:26):

That might be useful

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

#### Patrick Massot (Jun 08 2018 at 19:27):

But this bit is evil

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

#### Johan Commelin (Jun 08 2018 at 19:27):

I am still annoyed that I even had to do all that duplication.

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

#### Johan Commelin (Jun 08 2018 at 19:35):

That will help interested mathematicians to figure out what is going on.

#### Patrick Massot (Jun 08 2018 at 19:35):

Sure. Every documentation is good

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

#### Johan Commelin (Jun 08 2018 at 19:37):

And then we get lost.

#### Patrick Massot (Jun 08 2018 at 19:37):

Issues are about things to do. LaTeX file would be about things that are done

#### Johan Commelin (Jun 08 2018 at 19:38):

Yes, and PR's form the boundary, and Zulip is the glue that keeps everything together.

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

#### Patrick Massot (Jun 09 2018 at 10:53):

@Kevin Buzzard

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

#### Johan Commelin (Jun 09 2018 at 11:16):

Cool!

#### Johan Commelin (Jun 09 2018 at 11:16):

In my `Huber_pair`

branch I have a stupid definition of `I`

-adic topology

#### Johan Commelin (Jun 09 2018 at 11:16):

But it doesn't give a uniform_space. So it is pretty useless.

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

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

#### Johan Commelin (Jun 09 2018 at 12:31):

What is the advantage of working with subsets instead of subtypes?

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

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

#### Chris Hughes (Jun 09 2018 at 12:36):

And if some of your code requires sets, you have to stick to the former.

#### Johan Commelin (Jun 09 2018 at 12:37):

And if some of it requires subtypes? Then you stick with the latter...

#### Johan Commelin (Jun 09 2018 at 12:37):

But what is an example of "code [that] requirese sets"?

#### Chris Hughes (Jun 09 2018 at 12:37):

If it requires subtypes, then you use the coercion from a set and not `//`

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

#### Chris Hughes (Jun 09 2018 at 12:38):

Unless you only ever need subtypes. In which case don't use sets.

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

#### Chris Hughes (Jun 09 2018 at 12:39):

No it doesn't. Only use the first one.

#### Johan Commelin (Jun 09 2018 at 12:40):

I tried, and then it couldn't infer a topological space on it.

#### Johan Commelin (Jun 09 2018 at 12:40):

Because coercion and type inference don't work together.

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

#### Chris Hughes (Jun 09 2018 at 12:41):

Use the coercion for your topological space instance as well?

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

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

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

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

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

#### Johan Commelin (Jun 09 2018 at 12:43):

Ok, and subtypes find that hard?

#### Johan Commelin (Jun 09 2018 at 12:43):

We can define an intersection of subtypes right? Just take `\and`

of their properties.

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

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

#### Nicholas Scheel (Jun 09 2018 at 12:44):

the subtypes would need to have the same supertype, otherwise it doesn’t make sense

#### Johan Commelin (Jun 09 2018 at 12:45):

Right, I see.

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

.

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

#### Johan Commelin (Jun 09 2018 at 12:48):

So we need subsets and subtypes.

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

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

#### Chris Hughes (Jun 09 2018 at 12:49):

yes.

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

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

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

#### Johan Commelin (Jun 09 2018 at 12:50):

And then it worked. But now I don't see the point of the silent coercion.

#### Chris Hughes (Jun 09 2018 at 12:51):

Which is why it's best to stick to coercions the whole time.

#### Johan Commelin (Jun 09 2018 at 12:51):

I tried, but it didn't work.

#### Johan Commelin (Jun 09 2018 at 12:51):

Maybe I didn't try hard enough (-;

#### Chris Hughes (Jun 09 2018 at 12:51):

What didn't work?

#### Johan Commelin (Jun 09 2018 at 12:52):

Sticking to coercions. (Or do you mean explicit coercions, instead of silent ones?)

#### Chris Hughes (Jun 09 2018 at 12:53):

There both the same. What in particular didn't work?

#### Johan Commelin (Jun 09 2018 at 12:54):

Let me try to find it.

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

#### Johan Commelin (Jun 09 2018 at 12:55):

But I don't have Lean here, so I can't test it. Sorry.

#### Chris Hughes (Jun 09 2018 at 12:57):

I couldn't find `for_mathlib.subring`

#### Johan Commelin (Jun 09 2018 at 12:57):

Aah, that is in the `subring`

branch

#### Chris Hughes (Jun 09 2018 at 12:58):

Found it.

#### Johan Commelin (Jun 09 2018 at 12:58):

I thought `Huber_pair`

was a branch of `subring`

#### Patrick Massot (Jun 09 2018 at 12:58):

need to be in branch `subring`

#### Chris Hughes (Jun 09 2018 at 13:00):

Did the `is_ideal I`

not work. Or something else?

#### Johan Commelin (Jun 09 2018 at 13:00):

No, I think it was with subrings and topological spaces

#### Johan Commelin (Jun 09 2018 at 13:00):

Ok, maybe it was both.

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

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

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

#### Johan Commelin (Jun 09 2018 at 13:07):

Ok, thanks! I'll try it out when I get back to lean!

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

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

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

#### Patrick Massot (Jun 09 2018 at 14:20):

But this is one is nastier since it involves filters

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

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

#### Patrick Massot (Jun 09 2018 at 15:37):

Thank you very much @Reid Barton. `change`

was the key for the first one

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

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

#### Kevin Buzzard (Jun 09 2018 at 16:40):

[nonsense deleted]

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

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

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

#### Patrick Massot (Jun 09 2018 at 17:17):

Sometimes things come as subsets, for instance power bounded elements

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

#### Patrick Massot (Jun 09 2018 at 17:18):

This is the story Assia is always telling us

#### Johan Commelin (Jun 09 2018 at 17:19):

/me feels his inner mathematician shudder and cringe.

#### Johan Commelin (Jun 09 2018 at 17:20):

Somehow this *shouldn't* be necessary.

#### Patrick Massot (Jun 09 2018 at 17:25):

I agree

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

#### Kevin Buzzard (Jun 09 2018 at 17:42):

@Kenny Lau Should `is_valuation`

be a typeclass? It currently is

#### Kenny Lau (Jun 09 2018 at 17:43):

I don't know

#### Kevin Buzzard (Jun 09 2018 at 17:47):

Me neither

#### Kevin Buzzard (Jun 09 2018 at 17:47):

I'm writing brief LaTeX notes as Patrick suggested

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

#### Johan Commelin (Jun 09 2018 at 18:07):

Hmm, I don't know how that happened...

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

#### Kevin Buzzard (Jun 09 2018 at 18:08):

I can't seem to make comments on your PR.

#### Kevin Buzzard (Jun 09 2018 at 18:08):

Or at least I can't say the following:

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

#### Kevin Buzzard (Jun 09 2018 at 18:09):

It's attached to the line `Authors: Johannes Hölzl, Mitchell Rowett, Scott Morrison`

#### Johan Commelin (Jun 09 2018 at 18:09):

Right... that's a good point

#### Johan Commelin (Jun 09 2018 at 18:10):

(I hate all those license things)

#### Johan Commelin (Jun 09 2018 at 18:10):

Anyway, all I did was take their code and translate from multiplicative notation to additive...

#### Johan Commelin (Jun 09 2018 at 18:10):

I don't know what is appropriate in this case

#### Kevin Buzzard (Jun 09 2018 at 18:14):

@Mario Carneiro What do you think of this subring code?

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

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

.

#### Chris Hughes (Jun 09 2018 at 18:16):

Why use both `ring S`

and `ring (subtype S)`

?

#### Kevin Buzzard (Jun 09 2018 at 18:16):

But should we just avoid subsets completely? Or is it hard to say without context?

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

#### Chris Hughes (Jun 09 2018 at 18:17):

I think so.

#### Kevin Buzzard (Jun 09 2018 at 18:17):

and we should use typeclass inference at all times

#### Kevin Buzzard (Jun 09 2018 at 18:17):

but what I am unclear about is if we should be using sets at all

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

#### Kevin Buzzard (Jun 09 2018 at 18:19):

I see your point!

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

#### Johan Commelin (Jun 09 2018 at 18:21):

I would love to get rid of it, because it looks "unmathematical"

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

#### Kevin Buzzard (Jun 09 2018 at 18:25):

So what exactly breaks when you remove the subtype version?

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

#### Johan Commelin (Jun 09 2018 at 18:34):

Kevin, I will get back to the PR on monday morning I guess...

#### Kevin Buzzard (Jun 09 2018 at 18:34):

Yeah, let's figure out how it all works

#### Kevin Buzzard (Jun 09 2018 at 18:34):

this PR business

#### Kevin Buzzard (Jun 09 2018 at 18:34):

there's no hurry

#### Johan Commelin (Jun 09 2018 at 18:41):

Ok, let's do that.

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

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

#### Patrick Massot (Jun 09 2018 at 22:11):

I'm the king of filters! https://github.com/kbuzzard/lean-perfectoid-spaces/pull/5

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

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

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

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

#### Kevin Buzzard (Jun 10 2018 at 10:47):

This whole type class inference thing is still a mystery to me in places.

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

#### Johan Commelin (Jun 11 2018 at 06:57):

@Patrick Massot Does

instance toplogical_ring.to_uniform_space : uniform_space R

use the ring structure?

#### Johan Commelin (Jun 11 2018 at 07:04):

Cool PR by the way! I added some comments.

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

#### Johan Commelin (Jun 11 2018 at 07:13):

Yes, it would be nice to know who is working on what.

#### Johan Commelin (Jun 11 2018 at 07:13):

But I think we have done most low-hanging fruit

#### Patrick Massot (Jun 11 2018 at 07:17):

Sure

#### Kevin Buzzard (Jun 11 2018 at 15:18):

Isn't it all low-hanging fruit? ;-)

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

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

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

#### Mario Carneiro (Jun 11 2018 at 17:10):

I don't see any obvious reason for this to cause a problem

#### Johan Commelin (Jun 11 2018 at 17:11):

Ok, I thought you would get a non-trivial route `topological_ring → uniform_space → topological_space`

.

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

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

#### Mario Carneiro (Jun 11 2018 at 17:13):

that means that you can't use the default proof of `is_open_uniformity`

#### Johan Commelin (Jun 11 2018 at 17:23):

This might create some trouble...

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

#### Johan Commelin (Jun 11 2018 at 17:25):

(In fact, this is more about topological groups... the ring structure is not relevant.)

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

#### Patrick Massot (Jun 11 2018 at 19:02):

I'll try to ask Lean

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

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

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

#### Johan Commelin (Jun 12 2018 at 07:10):

Right, but picking up the existing topology is going to be pretty hard, I guess.

#### 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 $g$ to go from $A$ to $B$, 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?

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

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

#### Johan Commelin (Jun 12 2018 at 07:20):

/me loves type class inference systems with brains :graduation_cap:

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

#### Andrew Ashworth (Jun 12 2018 at 07:21):

so I don't think it's a practical thing to hope for in the future

#### Andrew Ashworth (Jun 12 2018 at 07:21):

the more you ask a tactic to do, the slower it runs...

#### Andrew Ashworth (Jun 12 2018 at 07:22):

i wonder if anyone here is interested in old-style chess engines

#### Johan Commelin (Jun 12 2018 at 07:23):

Hmmm too bad. And Kudos to human brains...

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

#### Andrew Ashworth (Jun 12 2018 at 07:23):

the number of possible paths grows exponentially

#### Andrew Ashworth (Jun 12 2018 at 07:23):

with each step

#### Johan Commelin (Jun 12 2018 at 07:23):

Yes, how would the old-style Chess engines help? (I never studied them.)

#### Andrew Ashworth (Jun 12 2018 at 07:24):

they don't help, it's a comment on how hard the problem is

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

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

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

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

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

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

#### Johan Commelin (Jun 12 2018 at 07:29):

Hmm, true

#### Johan Commelin (Jun 12 2018 at 07:29):

But, do you know of good heuristics?

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

#### Johan Commelin (Jun 12 2018 at 07:32):

Sounds promising.

#### Johan Commelin (Jun 12 2018 at 07:33):

Can't wait to have such stuff available at my fingertips (-;

#### Kevin Buzzard (Jun 12 2018 at 07:39):

@Johan Commelin Do you understand the consequences of all this for the perfectoid project?

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

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

.

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

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

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

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

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

#### Johan Commelin (Jun 12 2018 at 07:50):

We don't need modules for this project, right?

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

#### Johan Commelin (Jun 12 2018 at 07:52):

But in the current situation it seems to me that modules are almost unusable.

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

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

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

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

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

#### Scott Morrison (Jun 12 2018 at 08:09):

err... it should go in mathlib!

#### Johan Commelin (Jun 12 2018 at 08:09):

Yes, by transitivity

#### Johan Commelin (Jun 12 2018 at 08:10):

And then in mason_stothers they can make it as computable as they want :wink:

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

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

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

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

#### Johan Commelin (Jun 12 2018 at 09:27):

Or do you mean something more subtle?

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

#### Kevin Buzzard (Jun 12 2018 at 09:59):

because `N`

inherits an `A`

-module structure from the map `A->B`

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

#### Johan Commelin (Jun 12 2018 at 10:26):

Right, so returning to perfectoid spaces... what is the next step?

#### Johan Commelin (Jun 12 2018 at 10:26):

Should we pull stuff on presheaves in from your schemes-repo?

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

#### Kevin Buzzard (Jun 12 2018 at 12:45):

I think I want to do presheaves because I did them before

#### Kevin Buzzard (Jun 12 2018 at 12:45):

I think the next step is the topological space Spa(A)

#### Kevin Buzzard (Jun 12 2018 at 12:45):

for A a Huber pair

#### Kevin Buzzard (Jun 12 2018 at 12:45):

and that goes via Spv(R)

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

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

#### Mario Carneiro (Jun 13 2018 at 22:59):

I guess the constant is called `uniform_space.mk`

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

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

#### Mario Carneiro (Jun 20 2018 at 20:55):

This is in the pipeline last I checked. it should appear soonish

#### Mario Carneiro (Jun 20 2018 at 20:55):

I think Johannes is working on merging Patrick's normed space stuff

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

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

#### Kevin Buzzard (Jun 20 2018 at 21:05):

OK thanks for the tips.

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

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

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

#### Kenny Lau (Jun 20 2018 at 22:36):

I proved its UMP :P although Chris did much more than me

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

#### Kenny Lau (Jun 20 2018 at 22:37):

https://github.com/kckennylau/local-langlands-abelian/blob/master/src/polynomial.lean#L37

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

#### Kevin Buzzard (Jun 20 2018 at 22:39):

You have been busy.

#### Kenny Lau (Jun 20 2018 at 22:40):

well I can’t talk too much ‘bout it now :p

#### Kenny Lau (Jun 20 2018 at 22:41):

we both know the reason

#### Kevin Buzzard (Jun 20 2018 at 22:41):

I shall be grilling you on it in about 36 hours.

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

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

#### Kevin Buzzard (Jun 21 2018 at 20:13):

Oh wow I have universe issues!

A valuation on a ring $R$ is a map from $R$ to a totally ordered commutative monoid satisfying some axioms. Two valuations $v$ and $w$ are *equivalent* if $v(r)\leq v(s) \iff w(r)\leq w(s)$. The *valuation spectrum* $Spv(R)$ of $R$ 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} [Hα : 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?

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

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

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

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

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

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

#### 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) [Hα : 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.Hα 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

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

#### Kenny Lau (Jun 24 2018 at 09:58):

equiv can take different universes

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

?

#### Kevin Buzzard (Jun 24 2018 at 09:58):

Yes Kenny, I noticed this -- so at least my question typechecks.

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

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

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

#### Kevin Buzzard (Jun 24 2018 at 10:21):

Is this quotient.something?

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

#### Kenny Lau (Jun 24 2018 at 10:22):

just `unfold`

everything

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

#### Kevin Buzzard (Jun 24 2018 at 10:23):

If you unfold everything you end up with classical.somes which don't behave

#### Kevin Buzzard (Jun 24 2018 at 10:23):

or at least I did

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

#### Kenny Lau (Jun 24 2018 at 10:24):

what is the property of each some

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

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

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

#### Kevin Buzzard (Jun 24 2018 at 10:31):

I wondered if I'd made a wrong turn

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

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

#### Chris Hughes (Jun 24 2018 at 11:10):

I wish there was an option to display the type of proofs in the pp.

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

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

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

#### Kevin Buzzard (Jun 24 2018 at 12:33):

Thanks!

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

#### Chris Hughes (Jun 24 2018 at 14:14):

That displays the proofs, not their type.

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

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

#### Patrick Massot (Jun 25 2018 at 05:33):

Do you intend to fix my stuff or restart from scratch?

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

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

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

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

#### 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 $a b^{-1}$ in a group, but never $a / b$

#### Kevin Buzzard (Jun 25 2018 at 16:53):

Conversely no schoolkid writes 5 + (-3), they all write 5 - 3

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

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

.

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

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

#### Kevin Buzzard (Jun 28 2018 at 07:46):

It didn't work sometimes

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

#### 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. :-)

#### Johan Commelin (Jun 28 2018 at 07:52):

Ok, will do (-; So far nothing is breaking...

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

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

#### 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)\leq v(s)\iff v'(r)\leq v'(s)$ for all $r,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 $v$ 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]

#### Johan Commelin (Jul 02 2018 at 10:13):

That actually sounds pretty technical! I would have glossed over this for sure...

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

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

.

#### Johan Commelin (Jul 03 2018 at 07:50):

Is there a good explanation of these naming conventions somewhere?

#### Kevin Buzzard (Jul 03 2018 at 07:50):

We can have `is_`

if you like.

#### Johan Commelin (Jul 03 2018 at 07:51):

Well... you're the boss :rolling_on_the_floor_laughing:

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

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

#### Mario Carneiro (Jul 03 2018 at 07:52):

What is the convention in question? (I think I am the MC - Master of Conventions)

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

#### Mario Carneiro (Jul 03 2018 at 07:53):

Is it a property of the function, or an augmented function?

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

#### Kevin Buzzard (Jul 03 2018 at 07:53):

That used to say `class is_valuation`

#### Mario Carneiro (Jul 03 2018 at 07:54):

I think it should be `is_valuation`

then

#### Kevin Buzzard (Jul 03 2018 at 07:54):

The next line in the code is `namespace valuation`

#### Johan Commelin (Jul 03 2018 at 07:54):

Kevin, you see `Prop`

stands for *property* :wink:

#### Kevin Buzzard (Jul 03 2018 at 07:54):

and did it used to say `namespace is_valuation`

?

#### Mario Carneiro (Jul 03 2018 at 07:55):

`namespace valuation`

will be annoying since it's not accessed by projection

#### Mario Carneiro (Jul 03 2018 at 07:55):

since it's a typeclass

#### Kevin Buzzard (Jul 03 2018 at 07:55):

I don't understand that. I've never understood projection properly.

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

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

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

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

#### Kevin Buzzard (Jul 03 2018 at 07:56):

These words are too hard for me

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

#### Mario Carneiro (Jul 03 2018 at 07:57):

(actually that doesn't really work, `pi`

isn't a namespace)

#### Mario Carneiro (Jul 03 2018 at 07:58):

but for inductive types like `nat`

which are also namespaces, it works well

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

.

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

?

#### Kevin Buzzard (Jul 03 2018 at 07:58):

I don't see the difference

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

#### Johan Commelin (Jul 03 2018 at 07:58):

Because `group`

has extra structure.

#### Kevin Buzzard (Jul 03 2018 at 07:59):

Why do I want to use type class inference for valuations?

#### Kevin Buzzard (Jul 03 2018 at 07:59):

I do not understand what we want here

#### Kevin Buzzard (Jul 03 2018 at 07:59):

I was just sick of writing is_

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

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

.

#### Mario Carneiro (Jul 03 2018 at 08:00):

You can also just ignore conventions if you think `valuation`

will never be defined

#### Kevin Buzzard (Jul 03 2018 at 08:00):

What's worse is that "valuation" in the literature actually means "equivalence class of valuations"

#### Mario Carneiro (Jul 03 2018 at 08:00):

You didn't like my valuation = relation suggestion?

#### Kevin Buzzard (Jul 03 2018 at 08:00):

I don't know about that either. I implemented both

#### Kevin Buzzard (Jul 03 2018 at 08:00):

I have `zfc.valuation`

too

#### Mario Carneiro (Jul 03 2018 at 08:00):

ooh, mysterious

#### Kevin Buzzard (Jul 03 2018 at 08:01):

just means "I only use Type"

#### Mario Carneiro (Jul 03 2018 at 08:01):

why would you do that? You can just restrict the universe variables of polymorphic functions

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

?

#### Kevin Buzzard (Jul 03 2018 at 08:02):

"I only use Type" is just a maths thing

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

#### Johan Commelin (Jul 03 2018 at 08:03):

Kevin, I think Mario would want

structure valuations (R : Type) [comm_ring R] := {α : Type} [Hα : linear_ordered_comm_group α] (f : R → option α) (Hf : is_valuation f)

to be called `valuation`

#### Johan Commelin (Jul 03 2018 at 08:03):

But I am not sure about that...

#### Mario Carneiro (Jul 03 2018 at 08:03):

Only the `f`

and `hf`

should be in the structure

#### Johan Commelin (Jul 03 2018 at 08:03):

No...

#### Kevin Buzzard (Jul 03 2018 at 08:04):

Two valuations are equivalent if they "only differ by the alpha"

#### Mario Carneiro (Jul 03 2018 at 08:04):

you can still state that with the alpha as parameter

#### Johan Commelin (Jul 03 2018 at 08:04):

But then `valuations`

depends on `alpha`

, that becomes horrible right?

#### Kevin Buzzard (Jul 03 2018 at 08:04):

I have valuations defined to be something else

#### Mario Carneiro (Jul 03 2018 at 08:04):

no, that becomes tractable

#### Mario Carneiro (Jul 03 2018 at 08:05):

(I would drop the `s`

though)

#### Kevin Buzzard (Jul 03 2018 at 08:05):

no I don't, I have valuations to be defined exactly like that

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

#### Johan Commelin (Jul 03 2018 at 08:05):

Mario, then you have defined "valuation on R with value group alpha" (why not `Gamma`

?)

#### Kevin Buzzard (Jul 03 2018 at 08:06):

alpha not Gamma because Kenny wrote it

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

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

#### Johan Commelin (Jul 03 2018 at 08:06):

Yes, and *I* am completely fine with that (-;

#### Kevin Buzzard (Jul 03 2018 at 08:07):

Maybe I'm just making sure that one day I can write my own section 4

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

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

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

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

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

#### Mario Carneiro (Jul 03 2018 at 08:10):

*I* care

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

#### Kevin Buzzard (Jul 03 2018 at 08:10):

so a rumour started that the proof didn't fit into ZFC

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

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

#### Kevin Buzzard (Jul 03 2018 at 08:11):

Or is even that not enough?

#### Mario Carneiro (Jul 03 2018 at 08:11):

The problem is that almost everything you write is trivially not just in Type

#### Kevin Buzzard (Jul 03 2018 at 08:11):

?!

#### Mario Carneiro (Jul 03 2018 at 08:11):

for example, any function Type -> Type is not in Type

#### Mario Carneiro (Jul 03 2018 at 08:12):

i.e. `huber_ring`

or whatever

#### Mario Carneiro (Jul 03 2018 at 08:12):

these are justifiable in ZFC as class functions

#### Kevin Buzzard (Jul 03 2018 at 08:12):

Ok I give in

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

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

#### Johan Commelin (Jul 03 2018 at 08:14):

Mario, so how do we write an alpha-agnostic setoid with your version of `valuation`

?

#### Mario Carneiro (Jul 03 2018 at 08:14):

You shouldn't literally write a setoid

#### Mario Carneiro (Jul 03 2018 at 08:14):

it's too big

#### Mario Carneiro (Jul 03 2018 at 08:15):

instead you just use the equivalence relation

#### Mario Carneiro (Jul 03 2018 at 08:15):

and use the relation as a small representative when you need one

#### Kevin Buzzard (Jul 03 2018 at 08:15):

But we need the actual valuation functions all the time

#### Johan Commelin (Jul 03 2018 at 08:16):

Mario, so what is morally wrong with the current version that I quoted?

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

#### Kevin Buzzard (Jul 03 2018 at 08:16):

and this is a fundamental object

#### Kevin Buzzard (Jul 03 2018 at 08:16):

Spv is almost an adic space

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

#### Mario Carneiro (Jul 03 2018 at 08:16):

You can define the setoid, but it is one of the things that "essentially uses universes"

#### Kevin Buzzard (Jul 03 2018 at 08:16):

and we're constantly choosing points

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

#### Kevin Buzzard (Jul 03 2018 at 08:17):

so we have to get this right

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

#### Mario Carneiro (Jul 03 2018 at 08:17):

What's wrong, again, with defining `Spv`

as the collection of all valuation relations?

#### Kevin Buzzard (Jul 03 2018 at 08:17):

All proofs need an actual valuation

#### Mario Carneiro (Jul 03 2018 at 08:18):

You can define your own version of `quot.lift`

and `quot.mk`

that take valuations

#### Mario Carneiro (Jul 03 2018 at 08:18):

valuation functions that is

#### Kevin Buzzard (Jul 03 2018 at 08:18):

Aah

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

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

#### Kevin Buzzard (Jul 03 2018 at 08:20):

We define Spv as t