Schemes in Arend?

Stream: general

[Horatiu Cheval]

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]

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]

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]

It's great to see them pushing in this direction

[Kevin Buzzard]

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]

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]

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]

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]

I think those are very interesting questions!

[Kevin Buzzard]

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]

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]

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.