Zulip Chat Archive

Stream: maths

Topic: Taking the Stacks Project formalisation forward


view this post on Zulip Kevin Buzzard (Oct 09 2018 at 15:25):

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.

view this post on Zulip Patrick Massot (Oct 09 2018 at 15:27):

It should be going into mathlib

view this post on Zulip Patrick Massot (Oct 09 2018 at 15:27):

with mathlib quality

view this post on Zulip Kevin Buzzard (Oct 09 2018 at 15:34):

I thought you'd say that.

view this post on Zulip Patrick Massot (Oct 09 2018 at 15:37):

And we also need progress by @Scott Morrison on sheaves

view this post on Zulip Kevin Buzzard (Oct 09 2018 at 15:37):

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?

view this post on Zulip Kevin Buzzard (Oct 09 2018 at 15:38):

two minds with a single thought :-)

view this post on Zulip Patrick Massot (Oct 09 2018 at 15:39):

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

view this post on Zulip Johan Commelin (Oct 09 2018 at 16:18):

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.

view this post on Zulip Kevin Buzzard (Oct 09 2018 at 16:20):

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.

view this post on Zulip Kevin Buzzard (Oct 09 2018 at 16:20):

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?

view this post on Zulip Patrick Massot (Oct 09 2018 at 16:21):

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

view this post on Zulip Johan Commelin (Oct 09 2018 at 16:26):

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

view this post on Zulip Patrick Massot (Oct 09 2018 at 16:27):

Johan, I cannot allow you to bad mouth Bourbaki

view this post on Zulip Johan Commelin (Oct 09 2018 at 16:28):

What did I say wrong? :cold_sweat:

view this post on Zulip Patrick Massot (Oct 09 2018 at 16:28):

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

view this post on Zulip Johan Commelin (Oct 09 2018 at 16:29):

Bourbaki never wrote a volume on étale cohomology.

view this post on Zulip Patrick Massot (Oct 09 2018 at 16:30):

Oh, I just received an email from Bourbaki

view this post on Zulip Patrick Massot (Oct 09 2018 at 16:30):

But it's not about category theory

view this post on Zulip Johan Commelin (Oct 09 2018 at 16:31):

Oh, I just received an email from Bourbaki

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

view this post on Zulip Patrick Massot (Oct 09 2018 at 16:31):

He wants another seminar talk

view this post on Zulip Johan Commelin (Oct 09 2018 at 16:31):

He wants another seminar talk

Congratulations!

view this post on Zulip Patrick Massot (Oct 09 2018 at 16:31):

No, unfortunately it's another topic

view this post on Zulip Patrick Massot (Oct 09 2018 at 16:32):

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

view this post on Zulip Patrick Massot (Oct 09 2018 at 16:32):

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

view this post on Zulip Patrick Massot (Oct 09 2018 at 16:33):

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

view this post on Zulip Patrick Massot (Oct 09 2018 at 16:36):

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

view this post on Zulip Patrick Massot (Oct 09 2018 at 16:36):

Of course there is a risk he doesn't remember

view this post on Zulip Patrick Massot (Oct 09 2018 at 16:37):

he wrote that GT book in 1971

view this post on Zulip Johan Commelin (Oct 09 2018 at 16:40):

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

view this post on Zulip Kevin Buzzard (Oct 09 2018 at 16:55):

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

view this post on Zulip Kevin Buzzard (Oct 09 2018 at 16:55):

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

view this post on Zulip Kevin Buzzard (Oct 09 2018 at 16:56):

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

view this post on Zulip Kevin Buzzard (Oct 09 2018 at 16:57):

So it needs to be fixed up by then!

view this post on Zulip Johan Commelin (Oct 09 2018 at 17:06):

That's nice!

view this post on Zulip Johan Commelin (Oct 09 2018 at 17:06):

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

view this post on Zulip Johan Commelin (Oct 09 2018 at 17:07):

Alternatively, define smooth morphisms. Or something like that.

view this post on Zulip Kevin Buzzard (Oct 09 2018 at 17:15):

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

view this post on Zulip Kevin Buzzard (Oct 09 2018 at 17:15):

I never even did locally ringed spaces

view this post on Zulip Kevin Buzzard (Oct 09 2018 at 17:16):

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

view this post on Zulip Johan Commelin (Oct 09 2018 at 17:20):

Right, so we need some category theory (-;

view this post on Zulip Johan Commelin (Oct 09 2018 at 17:20):

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

view this post on Zulip Reid Barton (Oct 09 2018 at 18:33):

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

view this post on Zulip Patrick Massot (Oct 09 2018 at 18:34):

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

view this post on Zulip Reid Barton (Oct 09 2018 at 18:34):

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

view this post on Zulip Reid Barton (Oct 09 2018 at 18:35):

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

view this post on Zulip Scott Morrison (Oct 09 2018 at 21:27):

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.

view this post on Zulip Scott Morrison (Oct 09 2018 at 21:28):

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

view this post on Zulip Scott Morrison (Oct 09 2018 at 21:29):

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

view this post on Zulip Reid Barton (Oct 09 2018 at 21:53):

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

view this post on Zulip Reid Barton (Oct 09 2018 at 21:54):

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

view this post on Zulip Reid Barton (Oct 09 2018 at 21:54):

I guess the situation for perfectoid spaces may be similar

view this post on Zulip Scott Morrison (Oct 09 2018 at 22:10):

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.

view this post on Zulip Scott Morrison (Oct 10 2018 at 11:21):

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... :-(

view this post on Zulip Scott Morrison (Oct 10 2018 at 11:21):

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

view this post on Zulip Johan Commelin (Oct 10 2018 at 11:28):

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

view this post on Zulip Scott Morrison (Oct 10 2018 at 11:28):

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

view this post on Zulip Johan Commelin (Oct 10 2018 at 11:28):

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

view this post on Zulip Scott Morrison (Oct 10 2018 at 11:28):

But okay, I agree.

view this post on Zulip Johan Commelin (Oct 10 2018 at 11:29):

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

view this post on Zulip Scott Morrison (Oct 10 2018 at 11:29):

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

view this post on Zulip Johan Commelin (Oct 10 2018 at 11:29):

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

view this post on Zulip Scott Morrison (Oct 10 2018 at 11:29):

command line scripts are too messy

view this post on Zulip Scott Morrison (Oct 10 2018 at 11:29):

I think Gabriel and Mario were talking about exactly this

view this post on Zulip Mario Carneiro (Oct 10 2018 at 18:43):

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

view this post on Zulip Johan Commelin (Oct 10 2018 at 18:44):

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

view this post on Zulip Johan Commelin (Oct 10 2018 at 18:45):

But I'm only guessing.

view this post on Zulip Scott Morrison (Oct 10 2018 at 22:13):

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.

view this post on Zulip Kevin Buzzard (Oct 13 2018 at 10:34):

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.

view this post on Zulip Kevin Buzzard (Oct 13 2018 at 10:34):

Are open immersions of topological spaces in mathlib?

view this post on Zulip Kevin Buzzard (Oct 13 2018 at 10:35):

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

view this post on Zulip Patrick Massot (Oct 13 2018 at 10:43):

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

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 15:17):

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.

view this post on Zulip Reid Barton (Oct 16 2018 at 16:10):

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

view this post on Zulip Reid Barton (Oct 16 2018 at 16:10):

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

view this post on Zulip Reid Barton (Oct 16 2018 at 16:13):

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

view this post on Zulip Johan Commelin (Oct 16 2018 at 16:15):

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

view this post on Zulip Reid Barton (Oct 16 2018 at 16:15):

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

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

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

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 16:16):

The issue is that he has to learn some commutative algebra

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 16:17):

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.

view this post on Zulip Johan Commelin (Oct 16 2018 at 16:18):

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

view this post on Zulip Johan Commelin (Oct 16 2018 at 16:18):

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

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 16:20):

Stalks for sheaves of sets I guess?

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 16:20):

or types in this case

view this post on Zulip Johan Commelin (Oct 16 2018 at 16:27):

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.

view this post on Zulip Reid Barton (Oct 16 2018 at 16:49):

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.

view this post on Zulip Reid Barton (Oct 16 2018 at 16:49):

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

view this post on Zulip Scott Morrison (Oct 17 2018 at 02:28):

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

view this post on Zulip Scott Morrison (Oct 17 2018 at 02:38):

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

view this post on Zulip Mario Carneiro (Oct 17 2018 at 04:12):

@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

view this post on Zulip Kevin Buzzard (Oct 17 2018 at 07:06):

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

view this post on Zulip Johan Commelin (Oct 17 2018 at 07:09):

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.

view this post on Zulip Kevin Buzzard (Oct 17 2018 at 07:11):

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?

view this post on Zulip Johan Commelin (Oct 17 2018 at 07:19):

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

view this post on Zulip Kevin Buzzard (Oct 17 2018 at 07:32):

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

view this post on Zulip Kevin Buzzard (Oct 22 2018 at 15:20):

presheaf stuff

view this post on Zulip Kevin Buzzard (Oct 22 2018 at 15:21):

(deleted)

view this post on Zulip Kevin Buzzard (Oct 22 2018 at 15:23):

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

view this post on Zulip Ramon Fernandez Mir (Oct 22 2018 at 15:30):

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

view this post on Zulip Johan Commelin (Oct 22 2018 at 16:46):

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

view this post on Zulip Kevin Buzzard (Oct 23 2018 at 15:14):

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.

view this post on Zulip Reid Barton (Oct 23 2018 at 15:20):

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.

view this post on Zulip Reid Barton (Oct 23 2018 at 15:23):

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.

view this post on Zulip Reid Barton (Oct 23 2018 at 15:25):

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

view this post on Zulip Reid Barton (Oct 23 2018 at 15:40):

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

view this post on Zulip Reid Barton (Oct 23 2018 at 15:44):

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

view this post on Zulip Reid Barton (Oct 23 2018 at 15:49):

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

view this post on Zulip Reid Barton (Oct 23 2018 at 15:51):

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

view this post on Zulip Reid Barton (Oct 23 2018 at 15:52):

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

view this post on Zulip Reid Barton (Oct 23 2018 at 16:00):

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

view this post on Zulip Reid Barton (Oct 23 2018 at 16:02):

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

view this post on Zulip Reid Barton (Oct 23 2018 at 16:04):

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

view this post on Zulip Kevin Buzzard (Oct 23 2018 at 16:22):

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

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 14:42):

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×TS\times T is essentially never the product of the underlying sets of SS and TT. 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?

view this post on Zulip Reid Barton (Jan 26 2019 at 14:59):

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

view this post on Zulip Reid Barton (Jan 26 2019 at 15:04):

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

view this post on Zulip Reid Barton (Jan 26 2019 at 15:06):

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.

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 15:13):

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

view this post on Zulip Ramon Fernandez Mir (Mar 08 2019 at 17:32):

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.

view this post on Zulip Johan Commelin (Mar 08 2019 at 17:35):

It's great to see this progressing!

view this post on Zulip Johan Commelin (Mar 08 2019 at 17:35):

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

view this post on Zulip Johan Commelin (Mar 08 2019 at 17:37):

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

view this post on Zulip Ramon Fernandez Mir (Mar 08 2019 at 17:37):

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

view this post on Zulip Johan Commelin (Mar 08 2019 at 17:39):

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

view this post on Zulip Johan Commelin (Mar 08 2019 at 17:39):

You want to use a carefully constructed one.

view this post on Zulip Johan Commelin (Mar 08 2019 at 17:40):

Somewhere you must have some definition

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

view this post on Zulip Johan Commelin (Mar 08 2019 at 17:41):

You want to use that definition here.

view this post on Zulip Johan Commelin (Mar 08 2019 at 17:45):

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

view this post on Zulip Ramon Fernandez Mir (Mar 08 2019 at 17:45):

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.

view this post on Zulip Johan Commelin (Mar 08 2019 at 17:46):

No, this definition is not correct

view this post on Zulip Johan Commelin (Mar 08 2019 at 17:46):

It is almost correct (-;

view this post on Zulip Johan Commelin (Mar 08 2019 at 17:46):

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

view this post on Zulip Johan Commelin (Mar 08 2019 at 17:47):

Because X \iso Y is not a Prop.

view this post on Zulip Johan Commelin (Mar 08 2019 at 17:48):

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.

view this post on Zulip Ramon Fernandez Mir (Mar 08 2019 at 17:48):

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

view this post on Zulip Johan Commelin (Mar 08 2019 at 17:49):

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

view this post on Zulip Ramon Fernandez Mir (Mar 08 2019 at 17:53):

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

view this post on Zulip Johan Commelin (Mar 08 2019 at 17:56):

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

view this post on Zulip Johan Commelin (Mar 08 2019 at 17:56):

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

view this post on Zulip Johan Commelin (Mar 08 2019 at 17:56):

Can you prove that affine schemes are schemes?

view this post on Zulip Johan Commelin (Mar 08 2019 at 17:57):

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

view this post on Zulip Ramon Fernandez Mir (Mar 08 2019 at 18:01):

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.

view this post on Zulip Ramon Fernandez Mir (Mar 08 2019 at 18:02):

I mean that affine schemes are schemes.

view this post on Zulip Johan Commelin (Mar 08 2019 at 18:06):

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

view this post on Zulip Ramon Fernandez Mir (Mar 08 2019 at 18:09):

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.

view this post on Zulip Johan Commelin (Mar 08 2019 at 18:15):

Great!

view this post on Zulip Kevin Buzzard (Apr 11 2019 at 03:28):

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

view this post on Zulip Kevin Buzzard (Apr 11 2019 at 03:31):

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

view this post on Zulip Scott Morrison (Apr 11 2019 at 04:05):

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.

view this post on Zulip Scott Morrison (Apr 11 2019 at 04:06):

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.

view this post on Zulip Scott Morrison (Apr 11 2019 at 04:07):

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.

view this post on Zulip Scott Morrison (Apr 11 2019 at 04:08):

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

view this post on Zulip Kevin Buzzard (Apr 11 2019 at 04:21):

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

view this post on Zulip Scott Morrison (Apr 11 2019 at 04:22):

Yes.

view this post on Zulip Kevin Buzzard (Apr 11 2019 at 04:23):

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

view this post on Zulip Scott Morrison (Apr 11 2019 at 04:23):

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

view this post on Zulip Kevin Buzzard (Apr 11 2019 at 04:23):

Ha ha

view this post on Zulip Scott Morrison (Apr 11 2019 at 04:24):

No. I'm completely serious.

view this post on Zulip Scott Morrison (Apr 11 2019 at 04:24):

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

view this post on Zulip Kevin Buzzard (Apr 11 2019 at 04:24):

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

view this post on Zulip Scott Morrison (Apr 11 2019 at 04:25):

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

view this post on Zulip Kevin Buzzard (Apr 11 2019 at 04:25):

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

view this post on Zulip Scott Morrison (Apr 11 2019 at 04:25):

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

view this post on Zulip Kevin Buzzard (Apr 11 2019 at 04:26):

For example we have locally ringed spaces

view this post on Zulip Kevin Buzzard (Apr 11 2019 at 04:26):

The development is done in a much more mathlibby style

view this post on Zulip Kevin Buzzard (Apr 11 2019 at 04:27):

The correct objects are defined rather than corners being cut

view this post on Zulip Kevin Buzzard (Apr 11 2019 at 04:27):

In stark contrast to the perfectoid project :P

view this post on Zulip Ramon Fernandez Mir (Apr 12 2019 at 15:24):

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.

view this post on Zulip Johan Commelin (Apr 12 2019 at 16:00):

That sounds like a reasonable plan.

view this post on Zulip Kevin Buzzard (Apr 17 2019 at 17:00):

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?

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 23:27):

@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)?

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 23:34):

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

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 23:35):

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

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 23:36):

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.

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 23:36):

I don't care about universes

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 23:49):

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

view this post on Zulip Ramon Fernandez Mir (Apr 21 2019 at 00:30):

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.

view this post on Zulip Kevin Buzzard (Apr 21 2019 at 00:34):

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.

view this post on Zulip Johan Commelin (Apr 23 2019 at 06:12):

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

view this post on Zulip Kevin Buzzard (Sep 04 2019 at 04:47):

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.

view this post on Zulip Johan Commelin (Sep 04 2019 at 06:04):

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

view this post on Zulip Kevin Buzzard (Sep 04 2019 at 06:04):

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

view this post on Zulip Johan Commelin (Sep 04 2019 at 06:05):

They seem to have sheaves on sites...

view this post on Zulip Johan Commelin (Sep 04 2019 at 06:06):

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

view this post on Zulip Patrick Massot (Sep 04 2019 at 07:52):

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.

view this post on Zulip Patrick Massot (Sep 04 2019 at 07:53):

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/

view this post on Zulip Patrick Massot (Sep 04 2019 at 07:55):

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!


Last updated: May 09 2021 at 11:09 UTC