# Zulip Chat Archive

## Stream: maths

### Topic: Taking the Stacks Project formalisation forward

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

#### Patrick Massot (Oct 09 2018 at 15:27):

It should be going into mathlib

#### Patrick Massot (Oct 09 2018 at 15:27):

with mathlib quality

#### Kevin Buzzard (Oct 09 2018 at 15:34):

I thought you'd say that.

#### Patrick Massot (Oct 09 2018 at 15:37):

And we also need progress by @Scott Morrison on sheaves

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

#### Kevin Buzzard (Oct 09 2018 at 15:38):

two minds with a single thought :-)

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

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

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

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

#### Patrick Massot (Oct 09 2018 at 16:21):

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

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

#### Patrick Massot (Oct 09 2018 at 16:27):

Johan, I cannot allow you to bad mouth Bourbaki

#### Johan Commelin (Oct 09 2018 at 16:28):

What did I say wrong? :cold_sweat:

#### Patrick Massot (Oct 09 2018 at 16:28):

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

#### Johan Commelin (Oct 09 2018 at 16:29):

Bourbaki never wrote a volume on étale cohomology.

#### Patrick Massot (Oct 09 2018 at 16:30):

Oh, I just received an email from Bourbaki

#### Patrick Massot (Oct 09 2018 at 16:30):

But it's not about category theory

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

#### Patrick Massot (Oct 09 2018 at 16:31):

He wants another seminar talk

#### Johan Commelin (Oct 09 2018 at 16:31):

He wants another seminar talk

Congratulations!

#### Patrick Massot (Oct 09 2018 at 16:31):

No, unfortunately it's another topic

#### Patrick Massot (Oct 09 2018 at 16:32):

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

#### Patrick Massot (Oct 09 2018 at 16:32):

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

#### Patrick Massot (Oct 09 2018 at 16:33):

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

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

#### Patrick Massot (Oct 09 2018 at 16:36):

Of course there is a risk he doesn't remember

#### Patrick Massot (Oct 09 2018 at 16:37):

he wrote that GT book in 1971

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

#### Kevin Buzzard (Oct 09 2018 at 16:55):

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

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

#### Kevin Buzzard (Oct 09 2018 at 16:56):

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

#### Kevin Buzzard (Oct 09 2018 at 16:57):

So it needs to be fixed up by then!

#### Johan Commelin (Oct 09 2018 at 17:06):

That's nice!

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

#### Johan Commelin (Oct 09 2018 at 17:07):

Alternatively, define smooth morphisms. Or something like that.

#### Kevin Buzzard (Oct 09 2018 at 17:15):

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

#### Kevin Buzzard (Oct 09 2018 at 17:15):

I never even did locally ringed spaces

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

#### Johan Commelin (Oct 09 2018 at 17:20):

Right, so we need some category theory (-;

#### Johan Commelin (Oct 09 2018 at 17:20):

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

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

#### Patrick Massot (Oct 09 2018 at 18:34):

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

#### Reid Barton (Oct 09 2018 at 18:34):

except it looks like `open_set`

already has the order reversed for some reason

#### Reid Barton (Oct 09 2018 at 18:35):

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

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

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

#### Scott Morrison (Oct 09 2018 at 21:29):

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

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

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

#### Reid Barton (Oct 09 2018 at 21:54):

I guess the situation for perfectoid spaces may be similar

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

.

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

#### Scott Morrison (Oct 10 2018 at 11:21):

It's not like `rewrite_search`

is going to be merged anytime soon. :-)

#### Johan Commelin (Oct 10 2018 at 11:28):

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

#### Scott Morrison (Oct 10 2018 at 11:28):

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

#### Johan Commelin (Oct 10 2018 at 11:28):

Anyway, I'm really glad to hear that `back`

is converging to mathlib.

#### Scott Morrison (Oct 10 2018 at 11:28):

But okay, I agree.

#### Johan Commelin (Oct 10 2018 at 11:29):

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

#### Scott Morrison (Oct 10 2018 at 11:29):

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

#### Johan Commelin (Oct 10 2018 at 11:29):

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

#### Scott Morrison (Oct 10 2018 at 11:29):

command line scripts are too messy

#### Scott Morrison (Oct 10 2018 at 11:29):

I think Gabriel and Mario were talking about exactly this

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

#### Johan Commelin (Oct 10 2018 at 18:44):

I think it is mostly to make `obviously`

do the right thing as auto_param.

#### Johan Commelin (Oct 10 2018 at 18:45):

But I'm only guessing.

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

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

#### Kevin Buzzard (Oct 13 2018 at 10:34):

Are open immersions of topological spaces in mathlib?

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

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

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

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

#### Reid Barton (Oct 16 2018 at 16:10):

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

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

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

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

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

#### Kevin Buzzard (Oct 16 2018 at 16:16):

The issue is that he has to learn some commutative algebra

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

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

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

#### Kevin Buzzard (Oct 16 2018 at 16:20):

Stalks for sheaves of sets I guess?

#### Kevin Buzzard (Oct 16 2018 at 16:20):

or types in this case

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

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

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

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

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

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

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

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

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

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

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

#### Kevin Buzzard (Oct 22 2018 at 15:20):

#### Kevin Buzzard (Oct 22 2018 at 15:21):

(deleted)

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

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

@Johan Commelin

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

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

.

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

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

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

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

#### Reid Barton (Oct 23 2018 at 15:44):

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

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

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

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

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

#### Reid Barton (Oct 23 2018 at 16:02):

Oh, I see that that `directed_preorder`

is missing the `inhabited`

constraint

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

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

#### 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\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 (Jan 26 2019 at 14:59):

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

)

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

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

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

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

#### Johan Commelin (Mar 08 2019 at 17:35):

It's great to see this progressing!

#### Johan Commelin (Mar 08 2019 at 17:35):

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

#### Johan Commelin (Mar 08 2019 at 17:37):

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

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

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

#### Johan Commelin (Mar 08 2019 at 17:39):

You want to use a carefully constructed one.

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

#### Johan Commelin (Mar 08 2019 at 17:41):

You want to use that definition here.

#### Johan Commelin (Mar 08 2019 at 17:45):

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

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

#### Johan Commelin (Mar 08 2019 at 17:46):

No, this definition is not correct

#### Johan Commelin (Mar 08 2019 at 17:46):

It is almost correct (-;

#### Johan Commelin (Mar 08 2019 at 17:46):

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

#### Johan Commelin (Mar 08 2019 at 17:47):

Because `X \iso Y`

is not a `Prop`

.

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

.

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

.

#### Johan Commelin (Mar 08 2019 at 17:49):

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

#### Ramon Fernandez Mir (Mar 08 2019 at 17:53):

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

#### Johan Commelin (Mar 08 2019 at 17:56):

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

#### Johan Commelin (Mar 08 2019 at 17:56):

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

#### Johan Commelin (Mar 08 2019 at 17:56):

Can you prove that affine schemes are schemes?

#### Johan Commelin (Mar 08 2019 at 17:57):

Where is your proof that `Spec R`

is a locally ringed space?

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

#### Ramon Fernandez Mir (Mar 08 2019 at 18:02):

I mean that affine schemes are schemes.

#### Johan Commelin (Mar 08 2019 at 18:06):

Can you prove that `Spec R`

is a locally ringed space?

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

#### Johan Commelin (Mar 08 2019 at 18:15):

Great!

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

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

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

#### Scott Morrison (Apr 11 2019 at 04:06):

There does not need to be a proliferation of `equiv`

s, 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 (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.

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

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

#### Scott Morrison (Apr 11 2019 at 04:22):

Yes.

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

#### Scott Morrison (Apr 11 2019 at 04:23):

I mean, everything in the schemes project should be in `for_mathlib`

... :-)

#### Kevin Buzzard (Apr 11 2019 at 04:23):

Ha ha

#### Scott Morrison (Apr 11 2019 at 04:24):

No. I'm completely serious.

#### Scott Morrison (Apr 11 2019 at 04:24):

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

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

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

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

#### Scott Morrison (Apr 11 2019 at 04:25):

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

#### Kevin Buzzard (Apr 11 2019 at 04:26):

For example we have locally ringed spaces

#### Kevin Buzzard (Apr 11 2019 at 04:26):

The development is done in a much more mathlibby style

#### Kevin Buzzard (Apr 11 2019 at 04:27):

The correct objects are defined rather than corners being cut

#### Kevin Buzzard (Apr 11 2019 at 04:27):

In stark contrast to the perfectoid project :P

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

#### Johan Commelin (Apr 12 2019 at 16:00):

That sounds like a reasonable plan.

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

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

#### Kevin Buzzard (Apr 20 2019 at 23:34):

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

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

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

#### Kevin Buzzard (Apr 20 2019 at 23:36):

I don't care about universes

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

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

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

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

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

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

#### Kevin Buzzard (Sep 04 2019 at 06:04):

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

#### Johan Commelin (Sep 04 2019 at 06:05):

They seem to have sheaves on sites...

#### Johan Commelin (Sep 04 2019 at 06:06):

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

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

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

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