Zulip Chat Archive

Stream: general

Topic: Schemes in Arend?


Horatiu Cheval (Jun 04 2021 at 19:25):

I'll start this off by stating that I know nothing about algebraic geometry or what schemes are. I only understand that they are sophisticated constructions and that it was a big achievement having them in Lean. I also watched the "Is HoTT the way to do mathematics" given by Kevin Buzzard and one of the points I took from it was that it would be interesting to see what would happen if one would try to do these kind of things in a HoTT-based systems.

Recently, I started playing with Arend, a proof assistant based on cubical type theory. While looking through its standard library, I noticed a Scheme.ard file. Now, I can't really tell how far that goes in terms of a formalization of schemes (hence the question mark in the title), but in any case, I just wonder what do people here who actually know something about these things think of this?

Johan Commelin (Jun 04 2021 at 19:28):

It looks like a pretty good start. They are importing some stuff about sheaves, but they don't seem to define any sheaves yet.

Johan Commelin (Jun 04 2021 at 19:29):

So there is still a bit of work left before they are done. I don't know Arend, but it seems to me that with 1 or 2 more weeks they could be done.

Johan Commelin (Jun 04 2021 at 19:30):

It's great to see them pushing in this direction

Kevin Buzzard (Jun 04 2021 at 21:46):

So then I have to hold off with my comments about schemes in Arend. Maybe Shadman can just ask again in the right stream.

So first we have schemes in Isabelle and now this. I was wondering whether "do schemes" is not the best test for systems and one should prove a theorem or two about them to actually see if the systems can manipulate the objects. For example, Gamma Spec adjunction for schemes, existence of categorical products, construction of projective n-space over a field and proof that global sections of it are just the constants -- these were things that came to mind

Andrew Ashworth (Jun 05 2021 at 06:30):

I am unsure why doing math in Arend the HoTT system is thought to be difficult. It's still type theory in end. The library writers are interested in constructive math, so it is a little unfamiliar to most, but isn't the hard part the actual math bits since they're using locales instead of "normal" topological spaces?

Kevin Buzzard (Jun 05 2021 at 08:11):

Several people have said this to me. The answer is simply that Voevodsky proved lots of theorems about schemes on paper and then switched to unimath and 15 years later there were still no schemes in unimath. In contrast it took three complete lean amateurs a few months to make them, and this was back in 2017 when mathlib was tiny. Because of this I suspected something was up.

Patrick Massot (Jun 05 2021 at 08:17):

Kevin Buzzard said:

So first we have schemes in Isabelle and now this. I was wondering whether "do schemes" is not the best test for systems and one should prove a theorem or two about them to actually see if the systems can manipulate the objects. For example, Gamma Spec adjunction for schemes, existence of categorical products, construction of projective n-space over a field and proof that global sections of it are just the constants -- these were things that came to mind

I think the first reaction should be celebrating that something should be moving towards doing formalized math in more systems, not saying we should change the criterion! Then we should try to figure out whether these are indeed schemes as honest topological spaces endowed with a sheaf of rings or some alternative reality where topological spaces don't exist. And then then ask whether HoTT helped in any way or whether we are simply celebrating that HoTT annoyance had been worked around.

Kevin Buzzard (Jun 05 2021 at 08:25):

I think those are very interesting questions!

Kevin Buzzard (Jun 05 2021 at 08:27):

But let's say that it turns out that the Arend definition is just some "corepresentable localic ind-sheaf on the infinity category of rings" nonsense definition, far from the topological space plus sheaf of rings concrete model which we have. Then this will exactly be shown up by being a definition it's impossible to work with.

Patrick Massot (Jun 05 2021 at 08:29):

The question of whether it's possible to work with schemes is of course the next step. But here all proof assistants are at the same point, right? We don't have anything either if I understand correctly.

Kevin Buzzard (Jun 05 2021 at 09:18):

Yes that's absolutely true, which is why I thought it was an interesting question. We still don't know if we can define projective n-space, for example, in practice. I am in the middle of preparing a PR on internally graded rings.


Last updated: Dec 20 2023 at 11:08 UTC