Taking the Stacks Project formalisation forward

Stream: maths

[Kevin Buzzard]

I formalised the definition of a scheme -- in theory at least. I proved that an affine scheme was a scheme which gave me some sort of hope that I'd formalised the definition correctly. The files are a mess, some people were never happy with the names of the theorems or the names of the lean files, the whole thing needs a tidy. I have a Masters student who might be interested. What are the priorities here? He'd like to prove some more lemmas about schemes (and indeed we as a department would like to see some original material). But maybe I could use this as impetus to tidy the whole thing up. Does anyone have any ideas about what could be priorities here? @Patrick Massot and @Johan Commelin you probably both have clearer ideas than me about where this project should be going.

[Patrick Massot]

It should be going into mathlib

[Patrick Massot]

with mathlib quality

[Kevin Buzzard]

I thought you'd say that.

[Patrick Massot]

And we also need progress by @Scott Morrison on sheaves

[Kevin Buzzard]

A big question here is what to do with the sheaf theory. I defined a sheaf of rings and a presheaf of sets and a sheaf of sets on a basis of a topological space and blah blah blah; do we just sit and wait for more category theory stuff or use the fact that everything is a typeclass so the low-level approach is fine? How long will it be before mathlib contains all the machinery necessary to write "let F be a presheaf of rings on the topological space X" in a category-theory-like manner, so I don't have to also define morphisms of presheaves?

[Kevin Buzzard]

two minds with a single thought :-)

[Patrick Massot]

This is blocking for the perfectoid project as well (also blocked by ring completions, subring issue, etc...)

[Johan Commelin]

Right. I think those presheaves are pretty close. As soon as @Scott Morrison's coauthors stop being grumpy, we will get backwards_reasoning and then all sorts of limits. After that a bunch of stuff about sheaves will be within reach.

[Kevin Buzzard]

I managed just fine in the schemes project with no category theory. Part of me is scared that using the category theory stuff will actually make things more complicated! And unfortunately I must be completely honest and say that I have not been paying careful attention to exactly what is there and what is not there. I know that Scott's work seems to rely on a bunch of automation and I know that these things are very complicated to get right and that I know essentially nothing which would help. I would like to contribute to Scott's work by actually trying it out in some basic cases and then asking for advice when I can't get it to work.

Perhaps going back to the stacks project and doing it all again using the category-theoretic tools that we either have already or will have soon would be a good test case for this category theory stuff. I think that in particular getting the parts of category theory working which are used widely outside of pure category theory would be an important project.

[Kevin Buzzard]

Golly so we need backwards reasoning and then limits and _then_ sheaves? Because the sheaf axiom says that some map to a limit is an isomorphism?

[Patrick Massot]

Right, we need someone totally unrelated to GRU to visit Scott's collaborators towns for tourism

[Johan Commelin]

@Kevin Buzzard I think we should certainly try to take advantage of category theory. After all, we want étale cohomology next, and then you don't want to have live in a parallel universe where you have no category theory available...

[Patrick Massot]

Johan, I cannot allow you to bad mouth Bourbaki

[Johan Commelin]

What did I say wrong? :cold_sweat:

[Patrick Massot]

You don't like living in a parallel universe without category theory

[Johan Commelin]

Bourbaki never wrote a volume on étale cohomology.

[Patrick Massot]

Oh, I just received an email from Bourbaki

[Patrick Massot]

But it's not about category theory

[Johan Commelin]

Oh, I just received an email from Bourbaki

He invites you to give a seminar talk about interactive theorem proving?

[Patrick Massot]

He wants another seminar talk

[Johan Commelin]

He wants another seminar talk

Congratulations!

[Patrick Massot]

No, unfortunately it's another topic

[Patrick Massot]

Hales gave a Bourbaki seminar on proof assistants not so long ago

[Patrick Massot]

so I don't think they'll want another one before seeing real progress here

[Patrick Massot]

http://www.bourbaki.ens.fr/seminaires/2014/Prog_juin14.html

[Patrick Massot]

What's funny is I wanted to write Bourbaki an email asking whether he currently think he left a gap about that completion map thing or whether he claims this is only an ellipsis

[Patrick Massot]

Of course there is a risk he doesn't remember

[Patrick Massot]

he wrote that GT book in 1971

[Johan Commelin]

@Kevin Buzzard What does "original" mean for a masters project? Is computing an example enough? Or do we need a new lemma? Because that will be extremely hard to do in Lean.

[Kevin Buzzard]

Proving some basic lemmas about schemes and completely fixing up the schemes code is definitely enough.

[Kevin Buzzard]

Oh talking of schemes, you're not going to believe this: I've been asked to give a talk on them!

[Kevin Buzzard]

http://aitp-conference.org/2019/ :D

[Kevin Buzzard]

So it needs to be fixed up by then!

[Johan Commelin]

That's nice!

[Johan Commelin]

So I suggest that this master student turns it into a project to get schemes into mathlib. And then prove the Gamma_Spec adjunction.

[Johan Commelin]

Alternatively, define smooth morphisms. Or something like that.

[Kevin Buzzard]

I'd forgotten about gamma spec adjunction! That's an excellent project

[Kevin Buzzard]

I never even did locally ringed spaces

[Kevin Buzzard]

Because spec of a ring is automatically locally ringed and I never defined a morphism of schemes :-)

[Johan Commelin]

Right, so we need some category theory (-;

[Johan Commelin]

Another non-trivial but fundamental thing: fibre products of schemes.

[Reid Barton]

"let F be a presheaf of rings on the topological space X"

As it happens, we have this specific thing already. Not sure how far that will actually get you though.

import category_theory.opposites
import category_theory.examples.topological_spaces
import category_theory.examples.rings

open category_theory category_theory.examples

variables {X : Top} {F : (open_set X)ᵒᵖ ⥤ Ring}

[Patrick Massot]

But we can't look at its stalks, right?

[Reid Barton]

except it looks like open_set already has the order reversed for some reason

[Reid Barton]

Right, basically anything past this involves either limits or colimits of some kind.

[Scott Morrison]

I'm listening. :-) I've tried once or twice to just make my code on limits not need backwards_reasoning, but it felt pretty painful to me. backwards_reasoning \ back is actually quite close. Simon has ideas to make it efficient, but hopefully an inefficient PR can make it into mathlib if there's a promise we know how to make it fast, later.

[Scott Morrison]

@Reid Barton, Should I revert open_set to the usual definition? I guess I was just thinking "no one ever uses the forward direction, just the opposite category, lets just cut out the middleman".

[Scott Morrison]

(Perhaps the explicit opposites were causing some pain, but I don't think so.)

[Reid Barton]

@Scott Morrison, if the many different shapes of limit are causing some difficulty, I know that I would find it already very helpful to have just general (co)limits. Perhaps it would even be possible to do a version of these before back is merged (I might take another shot at this in a couple of days--I tried to set up a branch with all the limit types but it turned into too much work).

[Reid Barton]

Basically everything I want to formalize for locally presentable categories and model categories involves some kind of limits or colimits but a large fraction of it only needs general (co)limits (some other parts do need specific shapes like pushouts).

[Reid Barton]

I guess the situation for perfectoid spaces may be similar

[Scott Morrison]

Ok, I'll keep that in mind. There are a few missing sections on equalizers and pullbacks, but I was intending to leave those out at first anyway. Really the only thing to do for the PR is deal with the dependency on back.

[Scott Morrison]

getting closer. The new back works fine in my limits code, now it's just a matter of copying and pasting all the sequences of rewrites rewrite_search finds into the source code... :-(

[Scott Morrison]

It's not like rewrite_search is going to be merged anytime soon. :-)

[Johan Commelin]

@Scott Morrison This copy-pasting should/can be automated.

[Scott Morrison]

Meh... it should be made unnecessary. :-)

[Johan Commelin]

Anyway, I'm really glad to hear that back is converging to mathlib.

[Scott Morrison]

But okay, I agree.

[Johan Commelin]

I wrote a substitution script that takes coordinates and replacement text and patches up your file.

[Scott Morrison]

We need to learn how to have tactics talk directly to VS Code.

[Johan Commelin]

It is a sort of poor man's diff-patch.

[Scott Morrison]

command line scripts are too messy

[Scott Morrison]

I think Gabriel and Mario were talking about exactly this

[Mario Carneiro]

Could @Scott Morrison or someone explain why limits are difficult to formalize or require back? Seems like the basics are just more definitions, and everyone I have seen talking about (co)limits don't seem to expect more than that

[Johan Commelin]

I think it is mostly to make obviously do the right thing as auto_param.

[Johan Commelin]

But I'm only guessing.

[Scott Morrison]

Yeah, it is mostly me being lame, and not wanting to give up my automation. Sorry for making everyone wait. I made limits.lean itself mathlib ready last night, and as it turned out removing the dependency on rewrite_search was much more painful than removing back would have been.

[Kevin Buzzard]

I am doing a review of the stacks project code, because this is far more interesting than all the crappy reference letter requests I have piling up and I can now legitimately claim that is part of a work project, because I have an MSc student who is going to work on it and I am speaking about it at AITP 2019.

[Kevin Buzzard]

Are open immersions of topological spaces in mathlib?

[Kevin Buzzard]

Basic things such as composition of two open immersions is an open immersion, that sort of thing.

[Patrick Massot]

The closest that we almost have is https://github.com/leanprover-community/mathlib/blob/9d743bbb864234821c4ec881d4dc930ac3631838/analysis/topology/continuity.lean#L401

[Kevin Buzzard]

I want to define a locally ringed space in Lean (or rather get a student to define it). So this is a topological space plus a sheaf of rings plus an axiom about some direct limits (see stacks project for more info). I don't see that we have to wait for categories for this to happen. But when categories arrive, will this work somehow be wasted? I am assuming not. I didn't ever define a locally ringed space in the schemes repo, I dodged it, but I think I want to do things more properly this time.

[Reid Barton]

Well, what work is there? Certainly the bits to do with defining local rings and local ring maps will not be made redundant.

[Reid Barton]

We already have all the ingredients for presheaves of rings in mathlib.

[Reid Barton]

There is an oper PR which includes equalizers and products and another WIP one which constructs them for rings, so then you can define sheaves in that language. Johan seemed interested in defining sites for the perfectoid space project, and that seems like a reasonably small amount of effort to "future-proof" sheaves for the zariski topology

[Johan Commelin]

@Kevin Buzzard I think all the category theory will be there before your student has learned enough Lean to start working on this project.

[Reid Barton]

I think the remaining bit is to construct directed colimits of rings. Here you probably cannot avoid spending some effort which, eventually, could be superseded by some general machinery on finitary algebraic theories

[Kevin Buzzard]

My student is a 4th year joint maths and computing student that spent the summer working with Coq

[Kevin Buzzard]

The issue is that he has to learn some commutative algebra

[Kevin Buzzard]

We already have all the ingredients for presheaves of rings in mathlib.

So what does the definition of a locally ringed space look like now? It's going to be a structure consisting of a topological space, and then a presheaf of rings -- but I shouldn't define this by hand myself now? And then some lemma about a direct limit being local.

[Johan Commelin]

Well, stalks are also done by Scott. This should land within a couple of weeks (at most).

[Johan Commelin]

So you have to define a ring structure on the stalk. Local rings are already in mathlib.

[Kevin Buzzard]

Stalks for sheaves of sets I guess?

[Kevin Buzzard]

or types in this case

[Johan Commelin]

Yes, exactly. That's what I meant with "you have to define a ring structure on the stalk". I really think that this project should try to make schemes mathlib-ready. And as corollary, use all the machinery that is (almost) available.

[Reid Barton]

And the fact that you can define a ring structure on the stalk clearly has very little to do with the specific definition of a ring.

[Reid Barton]

So if you do it for rings in particular, then in the long run that particular effort is "wasted" (in some sense)

[Scott Morrison]

I have no idea what compiles here, but
https://github.com/semorrison/lean-category-theory/blob/working/src/category_theory/presheaves/locally_ringed.lean

[Scott Morrison]

Certainly filtered colimits of rings is not done yet, and should be. Your student, Kevin, should do this!

[Mario Carneiro]

@Kevin Buzzard I think that it would be best to do this with categories. Now that they are there, they should be put to some use! I recall you using this as an argument in favor of category theory last time this came up

[Kevin Buzzard]

I think that when I was trying to write the code last Feb I would just keep saying "look these things are a category" without ever really thinking about what advantage this would actually give me. Here's a concrete question. A locally ringed space is a topological space, a functor from the category of open sets to the category of rings, an axiom about this functor (a statement about the values of the functor on open covers of open sets -- some kernel equals some image) and another axiom about this functor (about direct limits of rings which are values of the functor being local rings). I can write all of that without ever mentioning categories, but the language (functors, direct limits) is everywhere. I am still unclear about what the modern way to define this structure is (independent of my usual confusion about what should be bundled).

[Johan Commelin]

Kevin, you saw that I could extend a presheaf from a basis in 10 lines. Otoh now I'm struggling with topological bases, and it's a real pain.

[Kevin Buzzard]

I am not reading these technical threads carefully right now, I am really snowed under. I write in the beginner threads because those are the only ones where I can understand what's going on easily and quickly. I do remember your post though. And you can do this because you defined a presheaf to be a functor?

[Johan Commelin]

I can do this because of all Scott's magic. The automation takes care of a lot of painful noise.

[Kevin Buzzard]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/subject/extend.20presheaf.20from.20basis/near/135546628 (for my own reference)

[Kevin Buzzard]

presheaf stuff

[Kevin Buzzard]

(deleted)

[Kevin Buzzard]

@Johan Commelin it's time that the people at Imperial College began to understand how presheaves work now. @Ramon Fernandez Mir is hopefully going to be formalising a locally ringed space soon.

[Ramon Fernandez Mir]

Hello, I'm Ramon. I'm doing my Master's project with Kevin and we'll be formalising more parts of the Stacks project. As he said, I'm currently trying to formalise a locally ringed space. I was wondering where I could find the

presheaf stuff

@Johan Commelin

[Johan Commelin]

@Ramon Fernandez Mir Hi, nice to meet you! I'm pretty busy until next week Wednesday (2 guests are visiting), but after that I hope to return to this stuff. In the mean time I'll keep an I on these threads.

[Kevin Buzzard]

So to do locally ringed spaces we need that stalks are local, so we need colimits in the category of commutative rings. If we were doing this in a category free way then I'd know what to do. How does this all work within the category theory framework? This would be a colimit over the set of all open sets containing a fixed point a in a topological space X.

[Reid Barton]

I assume you also want a specific explicit description of the stalk. So under the current/near future state of category theory in mathlib, I would suggest just doing the "category-free" construction, and then if it seems useful or interesting, also show that what you built is actually a colimit, i.e., fits in a cocone with the expected universal property.

[Reid Barton]

I guess proving that the stalk is a colimit should help you prove that a morphism of ringed spaces does induce maps on stalks, for example.

[Reid Barton]

But given the state of limits right now, "should" in that sentence is more of a design criterion for limits, not an assertion.

[Reid Barton]

Ah, but the input to the construction of a filtered (or directed) colimit of rings should already be in the category theory language.

[Reid Barton]

Let me check what is actually in mathlib so far...

[Reid Barton]

I suggest starting from here

import category_theory.functor
import category_theory.examples.rings

universe u

/- Copied from https://github.com/semorrison/lean-category-theory/blob/master/src/category_theory/filtered.lean -/
/- Name collides with mathlib `directed`... -/
class directed_preorder (α : Type u) [preorder α] :=
(bound (x₁ x₂ : α) : α)
(i₁ (x₁ x₂ : α) : x₁ ≤ bound x₁ x₂)
(i₂ (x₁ x₂ : α) : x₂ ≤ bound x₁ x₂)

open category_theory.examples

def directed_colimit_of_rings {J : Type u} [preorder J] [directed_preorder J]
  (F : J ⥤ Ring) : Ring :=
sorry

[Reid Barton]

and then also constructing morphisms in Ring from F j to directed_colimit_of_rings F, and checking that these are compatible with the diagram maps F j -> F k, and then also that directed_colimit_of_rings F has the universal property

[Reid Barton]

(and possibly you want to do filtered colimits instead, though directed ones would be enough for Zariski)

[Reid Barton]

Then, I would suggest building the indexing category for the colimit "opens containing x" by hand, or possibly using full_subcategory, and check that its opposite category is filtered, and then define stalk x F as the directed_colimit_of_rings of F composed with the inclusion of "opens containing x" in opens X

[Reid Barton]

Oh, I see that that directed_preorder is missing the inhabited constraint

[Reid Barton]

(I'm also not sure that directed_preorder should really contain data, rather than being a Prop or subsingleton)

[Kevin Buzzard]

Oh thanks a lot Reid! This is all for @Ramon Fernandez Mir who knows a bunch of Coq but is just starting with Lean.

[Kevin Buzzard]

Should it be H : scheme S or S : scheme? In CS language I think this is asking whether schemes should be bundled or unbundled.

Any seasoned algebraic geometer will tell you that whilst the set underlying a scheme is of key technical importance, it does not play a completely central role, unlike the set underlying a group. For example, the set underlying a scheme has a topology on it, but the topology is grotesque -- on an irreducible scheme every non-empty open set is dense, there are typically many non-closed points and so on. One essentially never uses standard useful results from topology on this topological space, a standard way to prove things about schemes is to reduce them to questions about commutative rings and then do some commutative ring theory.

To give another example -- the category of schemes has products, but the underlying set of $S\times T$ is essentially never the product of the underlying sets of $S$ and $T$. So the kind of typeclass inference instances one sees for products of groups (group G and group H to group (G x H) ) is not correct for schemes.

Is this evidence that schemes should be bundled? I hope I got this the right way round -- I mean put the underlying topological space as a carrier and just have a structure called scheme? Or is the bundle/unbundle issue about other things?

We don't have much bundled stuff in mathlib. My naive understanding of what Cyril and Assia were telling us in Amsterdam was that perhaps if we did then we would begin to understand the power of unification hints. I am still very unclear about the general arguments for and against bundling, my impression is that when I ask a question of this nature the answer is often "try both and see which works best". But if we are to move forward with categories we'd better get the hang of bundling, right?

[Reid Barton]

I would definitely recommend "bundled" (S : scheme)

[Reid Barton]

The underlying set of a scheme is basically never going to have any interesting kind of structure other than that which comes from being a scheme (this is related to the underlying set not commuting with products, so that the underlying set of a group scheme is not a group, etc.)

[Reid Barton]

You can give scheme a has_coe_to_sort instance and write an instance for (S : scheme) : topological_space S so that you can still write p : S, is_open U where U : set S, etc.

[Kevin Buzzard]

@Ramon Fernandez Mir the way I set it up in my schemes repo is perhaps a bad idea. Let's bundle!

[Ramon Fernandez Mir]

What do we think about:

structure scheme (X : Type u) [topological_space X] :=
(carrier    : locally_ringed_space X)
(Haffinecov :
  ∀ x, ∃ U : opens X,
      x ∈ U
    ∧ ∃ R [comm_ring R] (OSpecR : locally_ringed_space (Spec R)),
      (res U carrier) ≅ OSpecR)

Here res follows from what I was saying in https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Subspaces.20and.20opens and is the only bit missing. ≅ is an isomorphism of locally ringed spaces.

[Johan Commelin]

It's great to see this progressing!

[Johan Commelin]

I'm a bit confused by (OSpecR : locally_ringed_space (Spec R))

[Johan Commelin]

Anyway, congrats for getting this far! Are you planning to PR stuff to mathlib?

[Ramon Fernandez Mir]

Does this help?

structure locally_ringed_space (X : Type u) [topological_space X] :=
(OX      : sheaf_of_rings X)
(Hstalks : ∀ x, is_local_ring (stalk_of_rings OX.F x))

[Johan Commelin]

You are asking for the existence of a locally_ringed_space structure on Spec R. But you don't just want that something exists...

[Johan Commelin]

You want to use a carefully constructed one.

[Johan Commelin]

Somewhere you must have some definition

def blah (R : Type u) [comm_ring R] : locally_ringed_space (Spec R)

[Johan Commelin]

You want to use that definition here.

[Johan Commelin]

Did you already formalise isomorphisms of locally ringed spaces? (Maybe even morphisms??)

[Ramon Fernandez Mir]

That's what I initially thought and I'm working on that definition. I thought this definition was correct though? Or is it a usability problem? Maybe my mistake is that I was just thinking about proving that an affine scheme is a scheme, which I think I can do with this definition.

[Johan Commelin]

No, this definition is not correct

[Johan Commelin]

It is almost correct (-;

[Johan Commelin]

Also, I'm surprised Lean would be happy with \exists blabla, X \iso Y

[Johan Commelin]

Because X \iso Y is not a Prop.

[Johan Commelin]

So you will probably want to wrap that in a nonempty, or you save the isomorphism for later use, but then you can't use \exists.

[Ramon Fernandez Mir]

That is actually my own local notation for isomorphism of locally ringed spaces. Probably should be using a different symbol, or simply are_isomorphic.

[Johan Commelin]

The notation is fine. Just write nonempty ((res _ _) \iso (Spec R))

[Ramon Fernandez Mir]

I see I see, very useful advice. I'm glad I asked!

[Johan Commelin]

But the bigger problem is the one I mentioned at the start.

[Johan Commelin]

Because that one wouldn't be caught by the type checker.

[Johan Commelin]

Can you prove that affine schemes are schemes?

[Johan Commelin]

Where is your proof that Spec R is a locally ringed space?

[Ramon Fernandez Mir]

I am hoping to be able to prove it soon. I have been working on the machinery to do so. Of course I need the right definition of a scheme first.

[Ramon Fernandez Mir]

I mean that affine schemes are schemes.

[Johan Commelin]

Can you prove that Spec R is a locally ringed space?

[Ramon Fernandez Mir]

I have a couple of bits missing but I should be able to. Now I think I fully understand the issue with my definition, I tried to be smart and skip a step and instead I did something dumb. In fact, proving that Spec R is a locally ringed space has just moved to the top of my TODO list.

[Johan Commelin]

Great!

[Kevin Buzzard]

@Scott Morrison Perhaps this is the place for the discussion about using categories. I discouraged Ramon from using them because this is an MSc project with a hard deadline so we couldn't afford to be waiting for PRs or becoming involved in technical design implementation decisions -- we needed everything to be done by around now. However if we forget about this and start taking the longer view then in principle I think it's natural to want to use the category theory language going forward.

[Kevin Buzzard]

One reason I am beginning to think that this approach has its advantages is that as you know I've had questions over the last few days of the form "does Lean know that the category of topological rings has limits?" If there was a topological ring category then I could just check the predicate and see where it leads me

[Scott Morrison]

I think there's a lot of duplication that is happening because of not using the category theory library, as well as lots of missing generality.

[Scott Morrison]

There does not need to be a proliferation of equivs, and one can do (pre)sheaves of Xs for all Xs at once without any effort. Both are already problems in this definition of schemes.

[Scott Morrison]

I think the right way forward here is to start PRing all the zariski topology and localisation related stuff into mathlib, and as soon as general presheaves land in mathlib someone can start refactoring the (relatively small part) of the schemes code to use that style.

[Scott Morrison]

(I've actually just been looking through the for_mathlib directory of the perfectoid project... There's a lot to catch up on there!)

[Kevin Buzzard]

The reason there's a lot of stuff in there is there is that a lot of development happened recently when PRs were being slow so we made a decision to let it pile up there for now and get to the definition

[Scott Morrison]

Yes.

[Kevin Buzzard]

There's a lot of infrastructure work needs doing in the perfectoid project.Tthere is also a for_mathlib directory in Ramon's schemes project but it's much more manageable

[Scott Morrison]

I mean, everything in the schemes project should be in for_mathlib... :-)

[Kevin Buzzard]

Ha ha

[Scott Morrison]

No. I'm completely serious.

[Scott Morrison]

In the (not so) long run anything that doesn't make it to mathlib will rot.

[Kevin Buzzard]

Now it's been done in the correct generality I think there's a much more powerful argument for this .

[Scott Morrison]

I think for_mathlib directories should be used to mean "ready for mathlib" (I just need to find some time to cut some PRs).

[Kevin Buzzard]

We cut corners initially; starting again from scratch enabled me to ensure that things were constructed properly this time

[Scott Morrison]

And everything else is "not ready for mathlib" rather than "not intended for mathlib".

[Kevin Buzzard]

For example we have locally ringed spaces

[Kevin Buzzard]

The development is done in a much more mathlibby style

[Kevin Buzzard]

The correct objects are defined rather than corners being cut

[Kevin Buzzard]

In stark contrast to the perfectoid project :P

[Ramon Fernandez Mir]

Hi, sorry I didn't reply on the other thread. I won't be able to do much in the following month or so as I have exams. However, I agree with @Scott Morrison that in order to eventually have schemes in the mathlib we need to use #886 and related. Since there are still a few pieces missing and I have to submit everything in two months, I don't think it's a good idea for me to start refactoring sheaves but I quite like the idea of PRing everything else and making the schemes repository as small as possible.

[Johan Commelin]

That sounds like a reasonable plan.

[Kevin Buzzard]

OK so over the last day or two I had a good look at what Ramon has done. One reason I did this was that we need sheaves for the perfectoid project, and I really wanted to use categories, but I find it very hard to make them work because of (a) universe issues (b) the fact that much of the relevant stuff is not yet in mathlib (which breaks update-mathlib which breaks my workflow). Talking about this to Johan (who has had more experience using the category theory repo than me) he says that I'm trying to use it too quickly, and getting a solid API is even more crucial than when using non-category theory Lean.

I have come to the conclusion that I shouldn't be running before I can walk. So @Scott Morrison @Johan Commelin @Reid Barton @Mario Carneiro here is my current proposal. @Ramon Fernandez Mir has made what looks to me like a very solid repo

https://github.com/ramonfmir/lean-scheme

where he defines schemes and locally ringed spaces, and proves that an affine scheme is a scheme. He did not use category theory stuff at all. The code is an order of magnitude better than the code that Chris Kenny and I wrote when we were beginners. Most or all of my poor design decisions have been fixed. A crucial role is played by @Neil Strickland 's localisation predicate (which Ramon has now turned into a proper API, because he has had to use it extensively in the code).

The "next" results in the development of schemes are: to define a morphism of locally ringed spaces, and to prove that Spec: comm_ring -> locally ringed spaces and Gamma: locally ringed spaces -> comm_ring are adjoint functors. I am confident that Ramon's code will be good enough to make a non-category-theory proof of this. But the very statement of this is more naturally expressed in category theory language.

So it seems to me that a better test than the perfectoid repo, for seeing if categories are, or could be, made usable in Lean in the future (and I am optimistic that they can be), is to see if we can do some or all of the following things:

1) prove the Gamma-Spec adjunction within the language of category theory, in Lean.

2) replace Ramon's "hand-coded" sheaves of types and rings with category sheaves of types and rings

3) replace Ramon's "sheaf on a basis" with a category-theoretical approach

This to me looks like a substantial task. However what I am hoping is that actually rather than having to completely refactor the repo, we can actually incrementally build upon it, replacing definitions one by one. Doing this will show us actually whether things like total code length is going down or up when the category theory language is used.

I am wondering whether the fact that the code is already there in non-categorified form will somehow make experiments here easier than having to develop the theory from first principles. This is what my interpretation of Johan's API comment is. Johan -- if we have made all the definitions and proved all the theorems already, how easy will it be to make new definitions and prove new theorems using the category theory language? I think this will be a good test for the category theory stuff.

I am in no hurry to do this project, and Ramon now has to worry about other things such as passing his exams and writing up a pdf document about his project. But it seems to me to be a good practical application of all this category theory language and it might shed some light on things like design decisions. For example it occurred to me when trying to use categories within perfectoids that I really had lost all sight of the reason that I was trying to be maximally universe polymorphic. I had objects living in universe u and morphism sets Hom(X,Y) living in universe v. Why? I have no idea. All the other people using perfectoid spaces have objects living in Type and morphisms living in Type. Every example of a perfectoid space we will ever make, will live in Type, as far as I can see. At the very least Scott and I realised that perhaps we should have objects in Obj : Type u+1 and morphisms in Hom X Y : Type u (have I got this the right way round?). These "large categories" (if I've got it right) might make universes more manageable. The way I have started to think about them is like this: imagine I'm doing this stuff in ZFC (which was the way I always used to think about them). Where do the objects live there? Now call the ZFC universe u and see what happens. In particular I am suggesting that, just like the way Lean defines the reals to be a term of type Type rather than Type u, we define "concrete" categories such as the category of perfectoid spaces or the category of locally ringed spaces to only have one free universe variable rather than two. Even the category of sheaves of rings on a topological space -- I am now arguing that the rings should be in the same universe as the topological space, because that's how it actually works in maths and for the categories that come up in regular maths this doesn't seem to be an issue. I wish I knew more about e.g. Lurie's work on (infinity,1) categories to know whether this will be an issue. Reid do you have any comments on this?

[Kevin Buzzard]

@Scott Morrison @Ramon Fernandez Mir @Reid Barton @Kenny Lau @Chris Hughes I finally understand branches. Here is the challenge. Ramon has made a schemes repository which defines schemes and locally ringed spaces, and has proved that affine schemes are schemes. There are I think two interesting coding challenges with taking this project forward:

1) Prove that projective 1-space is a scheme. This would be our first non-affine scheme. Kenny -- this might be a neat project after exams.
2) Completely rip out Ramon's sheaves code and replace it with Scott's category theory code. Scott -- let's make your code work as well as we can, to solve real world problems in pure maths formalization.

I finally understand now that we should be doing something like -- first figuring out how to host such a project, and then just running with our own branch of mathlib -- or fork, or whatever the terminology is.

@Assia Mahboubi @Cyril Cohen
Has anyone ever defined schemes in Coq? If so, did they use category theory or not? Do we have anything to learn from any Coq experiences in these areas?

PS Does it matter in which order one tries (1) and (2)?

[Kevin Buzzard]

The two developments could run in parallel and we could see which worked best.

[Kevin Buzzard]

The goal would be to define the category of locally ringed spaces in a way which looked presentable to a mathematician.

[Kevin Buzzard]

And I personally would be fine if its type were just Type or Type 3 or however high you have to go to make my life easy.

[Kevin Buzzard]

I don't care about universes

[Kevin Buzzard]

@Ramon Fernandez Mir can you get your objects and morphisms all defined within Type? I should just try it myself -- I'm compiling.

[Ramon Fernandez Mir]

Hey, I still need to clean up the repository a bit to make it properly usable but should be ready soon. I still haven't looked into the potential universe issues we talked about. My impression is that they should be manageable. Is everything within one universe what we want?

Also, my ideal is to PR a fair amount of it to the mathlib, mainly the localization predicate and basic facts about Spec(R) (where should these go btw?).

Regarding the projective line, I'd really like to have it there before my deadline. We currently have two examples: the empty scheme :-))) and affine schemes. But I feel like three is a much nicer number. How hard do we think it'll be? Hopefully reasonably easy, right? I'd be happy to do it with you Kenny if it's something you'd be interested in.

[Kevin Buzzard]

I know for sure that in the category of ZFC locally ringed spaces, the objects are all topological spaces equipped with some extra structure and hence the objects of the ZFC category form a proper class, which is the ZFC version of Obj : Type 1. However for any two objects X and Y of the category, Mor X Y has is a set, so \Pi (X Y : Obj),Mor X Y : Type. I would be perfectly happy to make the category of locally ringed spaces in these restricted universe situations using either Scott's or Ramon's development. I have still not seen a convincing argument for why I as a pure mathematician should care about universes so I would like to push this until I do.

[Johan Commelin]

I'm really excited about these developments. @Ramon Fernandez Mir I'm looking forward to a boatload of PRs from your side (-;
Concerning stress tests: I think the Gamma-Spec adjunction should be at the top of the list. Once we have that one under our belt, I think that constructing P^n (via charts, or maybe via Proj) is a good second step. After that we should prove that P^n is proper over the base scheme. Once we have those, I think it is safe to say that "we can start doing algebraic geometry".

[Kevin Buzzard]

Everything has gone really quiet here. @Ramon Fernandez Mir the last commit was 2 months ago. I'm sorry, I've been really busy. Did you see this https://twitter.com/AnthonyBordg/status/1168865159374393345?s=20 ? Affine schemes were done in Coq in 2003.

@XenaProject Dear Xena, sheaves and affine schemes were formalized using Coq in Laurent Chicli's PhD thesis defended in 2003. http://www-sop.inria.fr/lemme/Laurent.Chicli/index.html

- Anthony Bordg (@AnthonyBordg)

[Johan Commelin]

There seems to be quite a lot of stuff here: https://www-sop.inria.fr/lemme/personnel/Laurent.Chicli/FrCoq.html

[Kevin Buzzard]

@Patrick Massot at a glance, do they have anything we don't have?

[Johan Commelin]

They seem to have sheaves on sites...

[Johan Commelin]

It's annoying that the underlined thingies aren't actually hyperlinks

[Patrick Massot]

This page kind of suggest he formalized some Grothendieck topology (he mentions "cribles") although I don't see how that's relevant to the definition of Spec.

[Patrick Massot]

What is much clearer is has been abandoned software since 2002. The author left academia and his work is not even on https://coq.inria.fr/opam/www/

[Patrick Massot]

Actually I can't find those files anywhere on the internet. I think this is yet another example yelling at us: @Ramon Fernandez Mir should PR his work to mathlib!