## Stream: general

### Topic: stacks project / schemes

#### Kevin Buzzard (Feb 28 2018 at 09:13):

Thought this was worth its own topic because we all know there are people here who are less interested in the maths side of things. Here's an update.

#### Kevin Buzzard (Feb 28 2018 at 09:14):

Kenny and I nearly have schemes. Not in a "just about ready for mathlib" sort of way -- far from it -- but in a "the mathematically correct definition" sort of way.

#### Kevin Buzzard (Feb 28 2018 at 09:16):

It will need a lot more work before it goes anywhere near mathlib, but I am not going to do that work quite yet because for deadline reasons it would be nice to get perfectoid spaces before 10th March, or at least to get some way towards them. After that we can think about tidying up and deciding which bits mathlib might want and in what form.

#### Kevin Buzzard (Feb 28 2018 at 09:18):

The reason I'm posting is because I need to make a call on categories. At the end of the day I currently need sheaves of commutative rings (for the _definition_ of a scheme), and to actually prove anything at all I need sheaves of modules for these rings. For perfectoid spaces I will need sheaves of topological rings on a site.

#### Kevin Buzzard (Feb 28 2018 at 09:18):

So do I go with sheaves taking values in categories or do I just muddle on?

#### Kevin Buzzard (Feb 28 2018 at 09:19):

If I go with sheaves taking values in categories then to put it bluntly it simply raises the bar even higher to getting anything in to mathlib.

#### Kevin Buzzard (Feb 28 2018 at 09:19):

Now Patrick has urged to me to get this into mathlib-ready form, and I'll start on this after the 11th.

#### Mario Carneiro (Feb 28 2018 at 09:19):

Here's a question: what is the least common denominator of all the things you need sheaves of?

#### Mario Carneiro (Feb 28 2018 at 09:20):

My hope is that it is at least a concrete category

#### Mario Carneiro (Feb 28 2018 at 09:21):

If you project needing 3+ different kinds of sheaves, that's sufficient for making a single generalization, but it's not immediate that this generalization should be over categories in the usual sense

#### Kevin Buzzard (Feb 28 2018 at 09:22):

But this has always been an independent experiment for me -- can we actually even define a scheme / perfectoid space in Lean? For me that is an interesting independent question. I don't think it is for Mario, because he looks at maths very differently and, not unreasonably, I don't think he can tell the difference between a perfectoid space and a topological space in some sense -- they're both structures with a bunch of axioms to him. And for some reason he seems very much focussed on theorems rather than definitions -- a theorem for him is proof that the definition works, whereas if I know as a mathematician that a definition is correct then for me that might be enough.

#### Kevin Buzzard (Feb 28 2018 at 09:23):

So there is certainly the possibility that my conclusion is "look, here's a definition" and Mario's response is "who cares?". And the definition might just then sit there for months just being something that mathematicians can look and go "oh look what they can do now, how fancy, that's a million miles from the odd order theorem isn't it".

#### Kevin Buzzard (Feb 28 2018 at 09:24):

The Least Common Denominator depends very much on how far you want to go.

#### Mario Carneiro (Feb 28 2018 at 09:24):

I think you are right in that assessment. It seems to me obvious that one can make a definition of scheme / perfectoid space in lean; that's obviously within Lean's capabilities. The question is only if one can make a good or useful definition

#### Kevin Buzzard (Feb 28 2018 at 09:24):

The Weil Conjectures are a famous theorem.

#### Kevin Buzzard (Feb 28 2018 at 09:25):

For them you ideally would have sheaves on a more general object than a topological space and then take the derived category.

#### Kevin Buzzard (Feb 28 2018 at 09:25):

My gut feeling is that by that point you want to be using categories.

by that point...

#### Mario Carneiro (Feb 28 2018 at 09:25):

I don't think you should be afraid of later revision

#### Mario Carneiro (Feb 28 2018 at 09:26):

have goals, and plan for them. If you want the Weil Conjectures, then go for it

#### Kevin Buzzard (Feb 28 2018 at 09:27):

I think you are right in that assessment. It seems to me obvious that one can make a definition of scheme / perfectoid space in lean; that's obviously within Lean's capabilities. The question is only if one can make a good or useful definition

No, that's just one question. Another question is how to get mathematicians talking about Lean. And we already have ample evidence that proving a theorem which is 400 pages of ingenious but relatively straightforward calculations in group theory and which was done by mathematicians before all of us were born, does not do it. But in the math community there is huge excitement about perfectoid spaces because they are new and they are demolishing bits of the Langlands Programme which people thought were hitherto inaccessible. They are fashionable.

#### Mario Carneiro (Feb 28 2018 at 09:27):

Is there positive evidence that writing down a definition will interest mathematicians?

#### Kevin Buzzard (Feb 28 2018 at 09:27):

This is the part that you (Mario) cannot see at all and this is unsurprising given where you are sitting and your background

#### Kevin Buzzard (Feb 28 2018 at 09:28):

There is positive evidence that not writing down a definition will not interest them.

#### Mario Carneiro (Feb 28 2018 at 09:28):

In a sense it seems much the same as proving an old theorem formally - whoop-de-doo you formalized a definition we all know

#### Kevin Buzzard (Feb 28 2018 at 09:28):

I am going to give a talk at an undergraduate conference on the 11th, a theoretical talk, an introduction to perfectoid spaces and what they can do

#### Kevin Buzzard (Feb 28 2018 at 09:29):

and I think it would be cool to unveil the definition there.

#### Kevin Buzzard (Feb 28 2018 at 09:29):

There is a difference which you can't see.

#### Kevin Buzzard (Feb 28 2018 at 09:29):

Proving an _old_ theorem formally -- you formalised a theorem that we all understand the statement of and which was proved before we were all born

#### Kevin Buzzard (Feb 28 2018 at 09:30):

Making a _new_ definition which is extremely complex and most mathematicians don't understand has much more of an air of mystery about it.

#### Kevin Buzzard (Feb 28 2018 at 09:30):

There is a subtlety.

#### Mario Carneiro (Feb 28 2018 at 09:31):

I assume that perfectoid spaces are not themselves the object of perfectoid theory, such as it is. Presumably they are being used in some way to get things done, some proof strategy that harnesses the power of the definition

#### Kevin Buzzard (Feb 28 2018 at 09:31):

Currently the word "perfectoid space" to most mathematicians means "abstract structure whose definition I have not read and would probably not understand if I did read, but I know that in the number theory community everyone is talking about them and I get the feeling that there is a general sense of excitement happening right now"

#### Kevin Buzzard (Feb 28 2018 at 09:31):

this is absolutely absolutely the opposite of everyone's feeling about the odd order theorem

#### Mario Carneiro (Feb 28 2018 at 09:32):

I'm obviously in the wrong place to make such pronouncements, but I won't be convinced you've done a thing with substance until you mimic such proofs

#### Kevin Buzzard (Feb 28 2018 at 09:32):

Well there is a basic "perfectoid theory" which was only worked out a few years ago

#### Kevin Buzzard (Feb 28 2018 at 09:32):

Mario I am not suggesting I have done anything of substance with perfectoid spaces even if I manage to define them.

#### Kevin Buzzard (Feb 28 2018 at 09:33):

But I am suggesting that they might be a selling point.

#### Kevin Buzzard (Feb 28 2018 at 09:33):

Because in contrast to the odd order theorem, which everyone understands and nobody cares about

#### Mario Carneiro (Feb 28 2018 at 09:33):

I freely admit I don't understand what makes a thing a selling point for mathematicians

#### Kevin Buzzard (Feb 28 2018 at 09:33):

perfectoid spaces have the property that nobody understands them and a lot of people care about them.

#### Kevin Buzzard (Feb 28 2018 at 09:33):

I freely admit I don't understand what makes a thing a selling point for mathematicians

#### Kevin Buzzard (Feb 28 2018 at 09:34):

Right, it's all just structures to you.

#### Kevin Buzzard (Feb 28 2018 at 09:34):

It would be like me saying "OK so you wrote a search engine and you wrote a space invaders game, they're all just computer programs at the end of the day though"

#### Kevin Buzzard (Feb 28 2018 at 09:34):

if I just couldn't tell the difference between them

#### Kevin Buzzard (Feb 28 2018 at 09:34):

because I never used either of them

#### Kevin Buzzard (Feb 28 2018 at 09:35):

I don't expect you to see any difference between the definition of a group and the definition of a perfectoid space

#### Kevin Buzzard (Feb 28 2018 at 09:35):

however I do think you should know that one is more fashionable than the other currently, in some circles.

#### Patrick Massot (Feb 28 2018 at 09:36):

Currently the word "perfectoid space" to most mathematicians means "abstract structure whose definition I have not read and would probably not understand if I did read, but I know that in the number theory community everyone is talking about them and I get the feeling that there is a general sense of excitement happening right now"

I can confirm this.

#### Mario Carneiro (Feb 28 2018 at 09:36):

Okay, by that analogy the proofs is where you "run the program" of the definition, that's where the differences become obvious

#### Mario Carneiro (Feb 28 2018 at 09:37):

Otherwise I'm just staring at a bunch of code for space invaders / google, and I don't understand what does what or why

Right

#### Kevin Buzzard (Feb 28 2018 at 09:39):

But on the other hand if you are in a community and there's a whole bunch of other people that you respect getting very excited by some computer program which you are not competent enough to use, then this might rub off.

#### Kevin Buzzard (Feb 28 2018 at 09:40):

And if you're then on some grant committee that is deciding where the money is going and you see a proposal which mentions this fancy new program which you know there are experts raving about then perhaps you are favourably inclined towards that proposal even though you can't actually understand it.

#### Mario Carneiro (Feb 28 2018 at 09:40):

I think you need to get famous number theorist X involved in your project then

#### Kevin Buzzard (Feb 28 2018 at 09:40):

I think I should write the definition first!

#### Patrick Massot (Feb 28 2018 at 09:41):

I think you need to get famous number theorist X involved in your project then

Yeah, who has Scholze's phone number?

#### Patrick Massot (Feb 28 2018 at 09:41):

That would have an impact

#### Kevin Buzzard (Feb 28 2018 at 09:41):

I exchange emails with him from time to time

#### Kevin Buzzard (Feb 28 2018 at 09:41):

but I've not mentioned this to him yet.

#### Patrick Massot (Feb 28 2018 at 09:41):

Imagine Peter Scholze in Rio explaining he is now using Lean as a day to day tool

#### Kevin Buzzard (Feb 28 2018 at 09:42):

That is not going to happen, but when I finish it I will certainly mention it to him.

#### Patrick Massot (Feb 28 2018 at 09:42):

[Note to non-mathematician: Rio is where Scholze will get his Fields medal this summer]

#### Kevin Buzzard (Feb 28 2018 at 09:42):

It would be interesting to hear his opinions.

#### Kevin Buzzard (Feb 28 2018 at 09:43):

The non-mathematicians have all muted this thread ;-)

Damn Zulip!

#### Kevin Buzzard (Feb 28 2018 at 09:44):

This is exactly the sort of chat that takes up 200 messages on gitter and all the poor CS guys just have to scroll through and hope that they see the CS question somewhere in the middle that we all ignore

#### Kevin Buzzard (Feb 28 2018 at 09:44):

I think that if we figure out how to make these topics work properly then it might be of benefit to everyone.

#### Kevin Buzzard (Feb 28 2018 at 09:45):

Anyway, Patrick and Mario I suspect you have different opinions on this issue. Let's imagine I triumphantly define a perfectoid space structure at 4am on the morning of 11th March and then decide to move on to something else for a month

#### Kevin Buzzard (Feb 28 2018 at 09:46):

and it's manifestly not mathlib-ready and I don't have the time to even prove Lemma 1 about perfectoid spaces

#### Kevin Buzzard (Feb 28 2018 at 09:46):

Mario is then manifestly not interested in adding the definition to mathlib, and he has explained his reasons above.

#### Kevin Buzzard (Feb 28 2018 at 09:46):

Patrick would you be happy with it just sitting there in some random repo on my github?

#### Kevin Buzzard (Feb 28 2018 at 09:47):

a valid but potentially unusable definition?

#### Patrick Massot (Feb 28 2018 at 09:47):

I wouldn't be happy, but who cares?

#### Kevin Buzzard (Feb 28 2018 at 09:47):

My plan is to make the definition and then just tell a bunch of undergraduates about it

#### Kevin Buzzard (Feb 28 2018 at 09:47):

until I find one or two people who are interested in taking it further.

#### Kevin Buzzard (Feb 28 2018 at 09:48):

Probably people have seen MO questions of the form "I am an undergraduate but I have been reading Lurie's book and I have a question about infinity-categories"

#### Kevin Buzzard (Feb 28 2018 at 09:49):

and sometimes the questions are just plain stupid

#### Kevin Buzzard (Feb 28 2018 at 09:49):

but sometimes they are graduate student level

#### Kevin Buzzard (Feb 28 2018 at 09:49):

For me this is evidence of a big change in the way people are accessing and learning mathematics.

#### Kevin Buzzard (Feb 28 2018 at 09:49):

Undergraduates have access to so much information now because of the web, so they find random things and attempt to engage with them.

#### Patrick Massot (Feb 28 2018 at 09:49):

But this will happen one month after your talk. And by that time your lone repo won't be compiling against current Lean

I don't care

#### Kevin Buzzard (Feb 28 2018 at 09:50):

because I am going to fix this problem if necessary by fixing which version of Lean I am using

#### Kevin Buzzard (Feb 28 2018 at 09:50):

I would really really love for Leo to release 3.4.0. I would stick there like a shot.

#### Kevin Buzzard (Feb 28 2018 at 09:51):

I am going to make a bunch of teaching material which will all run on some fixed version of Lean and then actively urge the undergrads not to upgrade.

#### Kevin Buzzard (Feb 28 2018 at 09:51):

That's why I am excited about the project which is going to make old nightlies accessible.

#### Kevin Buzzard (Feb 28 2018 at 09:52):

I just think that for certain people, a formal definition of a perfectoid space will be a really interesting looking carrot.

#### Kevin Buzzard (Feb 28 2018 at 09:53):

Schemes was enough of a carrot for Kenny, for example.

#### Kevin Buzzard (Feb 28 2018 at 09:54):

But actually I came here to ask whether I should use @Scott Morrison 's category theory library or whether it's not yet ready. That's the call I have to make at the minute.

#### Kevin Buzzard (Feb 28 2018 at 09:54):

If all I want is schemes then all I need is sheaves of rings which I can do by hand.

#### Kevin Buzzard (Feb 28 2018 at 09:54):

But this doesn't scale.

#### Patrick Massot (Feb 28 2018 at 09:55):

People who care about schemes or perfectoid spaces will want the latest advances in Lean automatisation. They won't be happy with Lean 3.4.0

I see.

#### Patrick Massot (Feb 28 2018 at 10:42):

Proving an _old_ theorem formally -- you formalised a theorem that we all understand the statement of and which was proved before we were all born

Come on @Assia Mahboubi fight back!

#### Scott Morrison (Feb 28 2018 at 11:23):

@Kevin Buzzard, agreeing a bit with @Patrick Massot , I do think it's important that developments end up in mathlib (or otherwise in repositories with multiple contributors who may maintain things). In the current Lean ecosystem, bitrot happens incredibly quickly (in fact so much so that I think I actually agree with Leo --- possibly all of the current mathlib is doomed to need complete rewriting several times over in the next few years).

#### Scott Morrison (Feb 28 2018 at 11:27):

It leaves me genuinely uncertain about the best path. I think you're fundamentally right in wanting to make a dash towards an important and impressive part of modern mathematics. I agree with everything you say concerning the odd order theorem. (The initial human proof of the odd order theorem was in some ways a huge disappointment --- it was one of the first times humans encountered an interesting theorem whose shortest proof was really long. Saying that computers are helpful for doing tedious mathematics is not really a selling point.)

#### Scott Morrison (Feb 28 2018 at 11:28):

But I'm also pretty sceptical that the March 11 dash you have in mind is going to have much effect. It's too likely that the code will fall apart quickly afterwards, or otherwise be unusable because it was written hurriedly.

#### Scott Morrison (Feb 28 2018 at 11:32):

I would like it to have an effect --- what we should dream about is a "mathoverflow effect", whereby one day a new thing appeared in the world that everyone realised they'd always wanted. I think there are potentially a huge number of students out there who would be interested in contributing to Lean libraries. However in combination with any "publicity", we would also need to have better strategy in place for teaching them how to work in Lean, and to productively organise their work. The current Lean community is realistically not yet ready for either of those.

#### Scott Morrison (Feb 28 2018 at 11:33):

It's great that documentation is coming along. TPIL is a great resource, and it's fantastic to see the mathlib documentation growing.

#### Scott Morrison (Feb 28 2018 at 11:34):

Unfortunately writing good Lean code is really hard (I still write lots of crappy code, after 18 months of learning Lean), and so any influx of new people could potentially just overwhelm those people in the community who can actually review PRs.

#### Scott Morrison (Feb 28 2018 at 11:35):

Finally, to try to answer your question, @Kevin Buzzard, I am trying to get the category theory library ready to PR into mathlib. But collaborators and postdocs and students are starting (ha!) to notice that I'm not getting much maths done...

#### Scott Morrison (Feb 28 2018 at 11:38):

Hearing you wanting it of course motivates me, for better or worse. I think building good foundations (e.g. using category theory to avoid proving everything 5 times over when setting up algebraic geometry) will be really helpful.

Also, I'm still a little proud of how few proofs I have in my library (i.e. how many are proved by obviously with little or no human intervention). :-)

#### Scott Morrison (Feb 28 2018 at 11:39):

Oh -- and in some interesting news -- two mathematicians here at ANU, after coming to my undergraduate students' talks (on implementing Euclidean domains, and the first iso theorem for groups), said they were going home to install Lean over the weekend. There's hope. :-)

#### Kevin Buzzard (Feb 28 2018 at 11:56):

I would like it to have an effect --- what we should dream about is a "mathoverflow effect", whereby one day a new thing appeared in the world that everyone realised they'd always wanted. I think there are potentially a huge number of students out there who would be interested in contributing to Lean libraries. However in combination with any "publicity", we would also need to have better strategy in place for teaching them how to work in Lean, and to productively organise their work. The current Lean community is realistically not yet ready for either of those.

I am going to dedicate a lot of time over the summer to writing documentation for undergraduate mathematicians introducing them to how to use Lean via my introduction to proof course.

#### Kevin Buzzard (Feb 28 2018 at 11:58):

Proving an _old_ theorem formally -- you formalised a theorem that we all understand the statement of and which was proved before we were all born

Come on @Assia Mahboubi fight back!

Ha ha! I was of course taking a very extreme viewpoint which I do not 100% believe in myself. I just wanted to highlight some of the obvious differences between defining a perfectoid space and proving the odd order theorem, even though "they're both computer programs".

#### Assia Mahboubi (Feb 28 2018 at 13:34):

Hi @Patrick Massot ! Thanks for having pointed me to this new forum and thread!

#### Assia Mahboubi (Feb 28 2018 at 13:37):

Hi @Kevin Buzzard ! Thanks for this thread, it's extremely interesting. And no worries about the assessment of the odd order theorem: in fact,
I agree with many of the points you make.

#### Assia Mahboubi (Feb 28 2018 at 13:39):

Fortunately, I was told what a perfectoid space is 2 weeks ago, otherwise I wouldn't have dared joining the discussion :-).

#### Assia Mahboubi (Feb 28 2018 at 13:48):

I agree that the fact that it was possible to write down a formal proof of the odd order theorem only demonstrates that proof assistants can be used to represent good old undergraduate level algebra. Not that proof assistants are useful tools for research in mathematics.

#### Assia Mahboubi (Feb 28 2018 at 13:51):

Even if in fact parts of the proofs involve slightly more advanced representation/character theory, etc.

#### Patrick Massot (Feb 28 2018 at 13:56):

Fortunately, I was told what a perfectoid space is 2 weeks ago, otherwise I wouldn't have dared joining the discussion :-).

Hi Assia! That's the point: Kevin wants to formalize stuff that mathematicians think are cool and intimidating

#### Assia Mahboubi (Feb 28 2018 at 13:58):

My hope is that one day proof assistants will be useful to discover new stuff, because the computer can in principle help you play with the definitions, discover abstractions and test them. So yes, I agree, it would be really cool to have the definition of a perfectoid formalized, because then one could play with it interactively instead of staring at a paper definition like a fish out of water.

#### Assia Mahboubi (Feb 28 2018 at 14:01):

But then I am not sure that the main problem is to come up with a definition which is not usable. I would say that the problem would be to formalize what a cat is and then to call it a perfectoid. Specially if not many people both know what a perfectoid is and how to speak/read Lean.
Lean checks proofs but only human readers check the definitions. So a collection of theorems, and of convincing examples, helps this assessment.

#### Assia Mahboubi (Feb 28 2018 at 14:11):

As a regular reviewer of papers about formalized mathematics, I often read papers which claim to formalize the theory of mystuffoids, it is very interesting and the authors prove a litany of lemmas, culminating with the Fundamental Theorem of Mystuffoids. But the authors never provide a (formalized) instance of mystuffoid. So as a reviewer, I try to verify that all the elementary examples of mystuffoids I know of can indeed by equipped with the structure provided by the authors. And that a few things that are not stuffoids for a good reason will not be instances. I had myself issues with my own tentative formal definitions at several occasions, and rejected several papers because this protocole made explicit flaws in the definitions.

#### Patrick Massot (Feb 28 2018 at 14:28):

I'm afraid there is no "elementary example" of a perfectoid space :wink: And my daughter woke up, I need to rush to ski

Enjoy!

#### Kevin Buzzard (Feb 28 2018 at 20:37):

But I'm also pretty sceptical that the March 11 dash you have in mind is going to have much effect. It's too likely that the code will fall apart quickly afterwards, or otherwise be unusable because it was written hurriedly.

#### Kevin Buzzard (Feb 28 2018 at 20:43):

As a regular reviewer of papers about formalized mathematics, I often read papers which claim to formalize the theory of mystuffoids, it is very interesting and the authors prove a litany of lemmas, culminating with the Fundamental Theorem of Mystuffoids. But the authors never provide a (formalized) instance of mystuffoid. So as a reviewer, I try to verify that all the elementary examples of mystuffoids I know of can indeed by equipped with the structure provided by the authors. And that a few things that are not stuffoids for a good reason will not be instances. I had myself issues with my own tentative formal definitions at several occasions, and rejected several papers because this protocole made explicit flaws in the definitions.

Oh this is a _great_ comment! Because basically it is pointing out that until I prove some lemmas, people can just say "how do you know you have the right definition?". I am not sure that undergraduates have the guts to say that ;-) but still this comment sticks in my head. So in fact I have to prove some lemmas just to check.

#### Kevin Buzzard (Feb 28 2018 at 20:45):

I'm afraid there is no "elementary example" of a perfectoid space :wink: And my daughter woke up, I need to rush to ski

I think the empty space is perfectoid. I'm not sure that it highlights the key features though.

#### Sean Leather (Mar 01 2018 at 06:28):

Oh this is a _great_ comment! Because basically it is pointing out that until I prove some lemmas, people can just say "how do you know you have the right definition?". I am not sure that undergraduates have the guts to say that ;-) but still this comment sticks in my head. So in fact I have to prove some lemmas just to check.

@Kevin Buzzard: I interpreted the comment not as saying “prove some lemmas,” but as saying “give examples.” In other words, don't just give a definition and lemmas, but show that there are things that instantiate your definition. Otherwise, your lemmas might be wonderful but never be of any actual use.

#### Kevin Buzzard (Mar 01 2018 at 07:28):

In fact for the definition I'm going to give, it will be really hard to give any examples, because we're going to cut corners and possibly come back later.

#### Patrick Massot (Mar 01 2018 at 08:46):

@Kevin Buzzard: I interpreted the comment not as saying “prove some lemmas,” but as saying “give examples.” In other words, don't just give a definition and lemmas, but show that there are things that instantiate your definition. Otherwise, your lemmas might be wonderful but never be of any actual use.

@Sean Leather I hope you realize you are being really rude here. We are talking about Algebraic Geometry and Langlands Program here, giving an example would be a disgrace. If needed, google "Grothendieck prime number 57".

#### Sean Leather (Mar 01 2018 at 08:56):

I hope you realize you are being really rude here. We are talking about Algebraic Geometry and Langlands Program here, giving an example would be a disgrace. If needed, google "Grothendieck prime number 57".

@Patrick Massot: You're right. I'm so accustomed to using the programs I write that I forget about mathematicians not needing to use the theorems they prove. :sweat_smile: I'm completely out of my depth here, and I apologize for any unintended insolence. :innocent:

#### Kevin Buzzard (Mar 01 2018 at 09:37):

@Sean Leather I thought about your comment a bit more and it's more complicated than I first imagined. Somehow examples and lemmas all get mixed together in this game, and definitions too. It's a bit strange. I said to Mario earlier "for you there is no difference between a perfectoid space and a group, they're both just structures" but somehow this isn't right. A group really is just a structure defined by some axioms. For these more complex objects there are theorems that you need to prove before things even make sense. For example you sometimes want to say "and my structure has an X, and if we choose a generator f of X then f also has property Y" or maybe even "and for all generators f of X, f also has property Y" but then if you actually want to get anywhere you need some lemma to say that all X's have generators, or maybe even that one generator of X has property Y iff they all do. Either you prove these lemmas or you don't. If you don't (and there are going to be a couple of times with schemes where I propose not proving the lemmas just yet) then it really would be impossible to give any examples at all because the lemmas are somehow part of the infrastructure. So perhaps I interpreted @Assia Mahboubi 's comments in a similar way to you but then went on and thought more about the consequences of constructing an example in the situation I had in mind, and realised that I was some genuine lemmas in algebraic geometry away from being able to give any example at all.

#### Sean Leather (Mar 01 2018 at 09:40):

Makes sense. I was thinking in the first order, whereas you were at a higher order. Good thing you're the mathematician. :wink:

#### Kevin Buzzard (Mar 07 2018 at 20:47):

Kenny and I just finished the definition of a scheme.

#### Kevin Buzzard (Mar 07 2018 at 20:49):

https://github.com/kbuzzard/lean-stacks-project/blob/ed8a255cef466794d4d836ffa6ffc1093532fa4b/src/scheme.lean#L430

#### Kevin Buzzard (Mar 07 2018 at 20:49):

It passes no basic tests whatsoever, other than "compiles" and "is mathematically correct".

#### Kevin Buzzard (Mar 07 2018 at 20:52):

In particular, for any commutative ring R we can build an affine scheme Spec(R), but we have not yet proved that this object is a scheme.

#### Kevin Buzzard (Mar 07 2018 at 20:52):

We are a couple of theorems away from this.

#### Kevin Buzzard (Mar 07 2018 at 20:56):

[the issue is that a scheme is a space with a sheaf, locally isomorphic to an affine scheme, but this isomorphism is an isomorphism of spaces with presheaves of rings (a morphism of sheaves is by definition a morphism of the underlying presheaves) so we do not logically need to check that the presheaf of rings that we have defined on Spec(R) is a sheaf]

#### Kevin Buzzard (Mar 07 2018 at 21:15):

Now for perfectoid spaces ;-)

Last updated: May 12 2021 at 04:19 UTC