How much work is descent and twisting of sheaves and schemes

Stream: general

[Arnoud van der Leer]

Hi there,

For my master's thesis, my supervisor and I agreed that I will be formalizing "something" in a proof assistant. Yay!
We still have a couple of options for what "something" is exactly. There are very fundamental options, and there are more "high-level" options. One of the candidates is chapter 4 in https://math.mit.edu/~poonen/papers/Qpoints.pdf, the most important theorem for me being Theorem 4.5.2. However, for this we need a lot of theory on schemes and sheaves (glueing of sheaves, Galois coverings, base change by a Galois action on a field), so it is probably way too ambitious. Does anyone have an idea as to "how much" work there would be involved in formalizing all this? Are there any obvious pieces of foundation missing in mathlib, any obvious bottlenecks?

[Riccardo Brasca]

I think we don't have anything about sheaves of modules or base change for schemes so it's probably a lot of work. But of course one can formalize some of the missing prerequisites!

[Kevin Buzzard]

I thought we did have base change for schemes, but we don't have sheaves of modules; I made them as part of a course I gave last term but I didn't PR them, and making the API for them will take a long time.

[Arnoud van der Leer]

Section 4.1 is not about sheaves of modules, but about a general sheaf on a topological space. I don't know whether that is better or worse.

[Riccardo Brasca]

Ah yes, we have it!

[Kevin Buzzard]

We also don't have group cohomology, quasiprojective schemes or varieties. I have people working on these things but we're not ready for 4.5.2. I supervised a master's project which did group cohomology, if you want to get a more realistic idea about what is feasible.

[Arnoud van der Leer]

Right. Thank you for your help. Then I have an idea what my thesis will be about.

[Kevin Buzzard]

Part of what's going on here is that there is a difference between "I will write down a definition of group cohomology" and "I will formalise group cohomology and an API in a way which is acceptable to mathlib" which are two extremely different things. Amelia's group cohomology work now uses a lot of simplicial machinery, for example. It means that the entire process is very slow. On the other hand before lockdown I had an undergrad do their thesis on a basic definition of H^0 and H^1 and the first few terms of the long exact sequence, and that was simple and cool

[Kevin Buzzard]

The hold-up with projective varieties is that we needed to develop a theory of internal and external gradings on rings (and semirings, monoids etc) which ended up being a published paper.

[Arnoud van der Leer]

Whow, cool. But that sounds complicated indeed.

[Kevin Buzzard]

We now do have a definition of protective schemes but like group cohomology it's on a branch and not on master.

[Arnoud van der Leer]

So what is an "API" exactly, in this case? Is it the entirety of simple theorems that allows one to actually work with something without proving every little elementary detail?

[Arnoud van der Leer]

I didn't even consider that chapter 4 deals mostly with projective schemes. I just assume that a couple of properties will hold for most of the schemes I work with, but of course to work with them in Lean, one first needs to define them indeed.

[Riccardo Brasca]

One you make a definition in Lean you have to prove a lot of totally obvious lemma, for example if you define "finite modules" the first lemma you prove is the fact that a module is finite iff there is a finite set of generators.

[Riccardo Brasca]

This is of course completely obvious, it is the definition, but it's a good thing to have it explicitly.

[Riccardo Brasca]

Then you prove that it is the same has having a finset of generator (mathematically this is the same as above, but not for Lean). Then that the zero module is finite, that finite is stable under isomorphisms and so on.

[Kevin Buzzard]

Yes exactly, it's all the elementary little details which a user of the theory will want to have access to. Otherwise the development is unusable. For example if mathlib just offers you an opaque definition of H^1(G,A) and you say "great now I can state the theorem" then the first thing you'll say after that is "ok I now have a 1-cocycle, how do I get the cohomology class" and you don't want the answer "oh, we define group cohomology using some abstract derived functor nonsense, you're on your own if you have a cocycle". The API needs to give you a way of making cohomology classes from cocycles (so you don't just need group cohomology, you need a surjection from cocycles with kernel coboundaries).

[Riccardo Brasca]

You can have a look at a random file in mathlib to get an idea of what an API is.

[Arnoud van der Leer]

Hm, right. Yeah, that makes sense. Also to prevent people from reinventing that wheel in their own projects, I guess.

[Arnoud van der Leer]

Thank you

[Riccardo Brasca]

Note that often you develop the API while proving more interesting results (except from the very basic stuff). The first time you need that R is finite as an R module you prove the theorem and you put it in the API rather than proving it inside a bigger proof.

[Kevin Buzzard]

Conversely if you define cohomology as cocycles over coboundaries and then someone wants the Serre spectral sequence what are you going to do then? What you need from a good theory of group cohomology is enough extra functions and theorems so that everyone can do all the things they want to do with group cohomology despite the fact that we mathematicians all believe that everything is true "by definition" because we have 37 different definitions of group cohomology simultaneously in our head and are free to switch. That's not how formalising works. You have to choose one definition and then the API is there to make it look like it's all the definitions, eg you will need a surjection from n-cocycles to cohomology with kernel the n-coboundaries whether or not you defined it to be cocycles over coboundaries, you'll need the long exact sequence, you'll need Inf-Res etc etc. If you just make a definition and then don't check that your definition can be used to do all these things then your work isn't ready

[Arnoud van der Leer]

Hm, right. Got it. I will keep that in mind.

[Kevin Buzzard]

To give another example: section 4 uses fpqc morphisms, but right now we have no API for flatness at all, even for flat modules. This would be a very cool MSc project; to develop enough API for flatness in commutative algebra so that we can define and prove basic properties about flat morphisms of schemes. How much Lean experience do you have? Right now I have a PhD student who just proved that if I \tensor M -> M is injective for all ideals I of R then A tensor M -> B tensor M is injective for all injections of R-modules A -> B. Thus we are just beginning the journey towards a proof of "several definitions of flatness coincide". Once we have this we'll be able to start on stuff like "a free module is flat". My guess is that it will be at least a year before we can even state something like "the identity morphism from a scheme to itself is flat" because right now we don't have enough people working on this sort of thing. It's not hard, it just takes a while to do it right and we don't have the person-power.

[Arnoud van der Leer]

Currently, I have played a bit with Lean (mathlib) and coq (unimath). I was at the summer school in Cortona in july last year.

[Arnoud van der Leer]

But I am strongly considering to do my thesis on a more fundamental topic. Perhaps I will revisit this topic in my own time, as a hobby. Or see if I can get a PhD position where I can spend part of my time on stuff like this.

[Kevin Buzzard]

I am very much hoping that in a couple of years' time stuff like 4.5.2 will be very much a possibility for an MSc project. I am pushing algebraic number theory and arithmetic geometry amongst my own group. One thing it's important to remember is that despite the fact that theorems like 4.5.2 are as old as the hills (probably they go back to the 60s if not before), the formalisation community seems to have attached no importance to getting their systems ready to formalise this stuff until around 2018 when this community here decided to start making stuff like this their targets. As a consequence we are figuring out how to develop a lot of this stuff in a theorem prover for the first time -- this is "cutting edge research", rather bizarrely.

[Arnoud van der Leer]

Yeah. That is still hard for me to wrap my head around, that this "seemingly trivial" stuff apparently is sometimes worthy of publishing. But I probably will get more than acquainted with all the hardships involved in the next 6 months ^^