Definition of a scheme

[kbuzzard]

I am interested to know how Lean will cope with the sort of complex mathematical objects which many mathematicians use. My impression (which might be incorrect because of lack of experience) is that whilst there are nowadays some pretty complex proofs typed up in computer proof checkers, they are typically about objects which one could call "basic" in the sense that a first year undergraduate might know about them (finite groups, finite graphs spring to mind). My motivation for seeing complex mathematical objects in Lean is simply that the Formal Abstracts project is going to need definitions of many of the standard complex mathematical objects which mathematicians use, and whilst the project can of course just manage in the short term with axioms and constants, at some point the objects do need to be defined.

Here is an explanation (with coherent and complete URLs containing more details) of what a scheme is. Schemes are the fundamental objects of study in algebraic geometry. They were discovered (in their current form) by Grothendieck in the late 1950s and early 1960s and they revolutionised the theory of algebraic geometry. This issue is a roadmap for implementing the definition of schemes in Lean. For more details I will constantly refer to the stacks project, which is a gigantic (6000 pdf pages and counting, but available in far more friendly form on the web) piece of work overseen by Johan de Jong, which one can nowadays describe as an attempt to be "a readable Bourbaki for algebraic geometry". The work is extremely thorough, and the thoroughness of the work should be extremely helpful for anyone wishing to get involved in implementing algebro-geometric objects in Lean. The foundations of the work are in ZFC set theory, however my understanding is that this should be embeddable in Lean and hence cause no problems.

By "ring" throughout this issue I mean a commutative ring with a 1, and all morphisms of rings send 1 to 1.

Here are some definitions with links to the stacks project, and within the stacks project one should hopefully find all other mathematical definitions one needs. Note that the stacks project is not absolutely overloaded with hyperlinks like Wikipedia, however the search facility is good (in the sense that it seems to work for me, although admittedly I know the basics of the area already).

A sheaf of rings on a topological space is a functor from the category of open sets on the space to the category of rings, which satisfies the sheaf axiom (a glueing axiom). Here are definitions of a presheaf (of sets), a presheaf of rings, a sheaf (of sets) and a sheaf of rings.

A locally ringed space is a topological space equipped with a sheaf of rings, such that all the stalks are local rings (a local ring is a ring with a unique maximal ideal).

An affine scheme is a certain kind of locally ringed space which is built from a ring. It is a fundamental object in algebraic geometry. The points of the underlying topological space are the prime ideals of the ring, and the sheaf of rings is built via localizing the original ring.

A scheme is a locally ringed space which has a cover by affine schemes.

These four definitions above (a sheaf of rings, a locally ringed space, an affine scheme, a scheme) seem to me to be four natural steps which one takes when defining a scheme, given what we currently have in Lean (topological spaces, and commutative rings with 1). However there are lots of other intermediate definitions (local rings, sheaves of sets, stalks of a sheaf, prime ideals, the Zariski topology, localisation of a ring at a multiplicative set...) which will also be needed. But I see no obstruction to making these definitions. If anyone is unclear as to what any precise mathematical definitions are involved here, and they can't find answers in the stacks project, then I would be happy to try to help.

I should finish by saying that I am not posting this issue because I desperately need to see schemes in Lean. I am posting this issue as basically a challenge to see if Lean can handle such a complex definition. Note that there are many other definitions in geometry which have a similar flavour (e.g. a smooth manifold is something covered by open balls, a rigid space is something covered by affinoid rigid spaces, a perfectoid space is something covered by affinoid perfectoids, and so on and so on) and it seems to me that schemes are hence both a nice basic test case for other objects defined by "glueing", and also something whose definition is nowadays very well documented on the web.

[digama0]

Question: The way the stacks project develops it, a sheaf is defined over an arbitrary category, but for the purpose of developing schemes, it would appear to suffice to have only sheafs of rings, which need not make any direct category references. How reasonable would you say it would be to skip general sheafs entirely? Do other kinds of sheafs often come up in this theory?

[kbuzzard]

The kind of sheaves that come up in basic algebraic geometry initially are sheaves of abelian groups or commutative rings on a topological space. Strictly speaking such a gadget is a functor from the category of open sets on the space to the category of abelian groups or commutative rings, but the category of open sets on a topological space is a particularly simple category because there is at most one morphism ("inclusion") between any two objects. One needs only the notion of a sheaf of rings on a topological space to define a scheme. When the stacks project people talk about a presheaf or sheaf with values in a category they are just setting up the general theory; in practice this category (in my experience at least), is almost always the category of abelian groups or the category of rings (or occasionally of sets) -- or one more slightly complex notion, which I'll outline in the next paragraph. But note that all of these examples (and the more complex one) do satisfy the hypotheses of this technical lemma and in particular there are no surprises regarding exactly what it means to be a sheaf.

Early on in the theory (not for the definition of scheme, but shortly afterwards) one needs a slightly more subtle notion, which is a sheaf of modules. This is slightly more delicate because the modules are over different rings: one starts with a sheaf of rings, and then one can define a sheaf of modules over this sheaf of rings, with the module associated to an open set U being a module for the ring associated to the open set U. But really this is something like a sheaf of abelian groups with an action by a sheaf of rings.

When defining various cohomology theories attached to schemes one considers more general kinds of schemes, but typically what gets generalised is not the target (the rings or groups or modules) but the source category: instead of considering just open sets one might consider more general source categories whose objects are certain nice maps to the scheme slightly more general than open immersions (for example etale morphisms, of which open immersions are an example but not the only example, are used to define the etale site and hence the etale topos and etale cohomology). But whilst these objects are very much in common usage in algebraic geometry research, we don't need to worry about them at this point. And my point is that when things start getting more general, this is where the generalisation occurs; one does not very often see sheaves of more exotic objects, but sheaves of rings play a fundamental role and it's the category associated to the topological space which might change later on.

I guess looking nearer to the future, when defining formal schemes or adic spaces one might want to consider sheaves of topological rings on a topological space. But in summary, sticking to sheaves of sets, abelian groups and rings on a topological space would be absolutely fine at this point.

[PatrickMassot]

This is not the first time I see @digama0's reluctance to use categories. Is there any deep reason for this? Here for instance, it really helps to define presheaves quickly to use the language of categories.

[johoelzl]

I don't know about @digama0 but for me the problem is not category theory itself, we surely want to have some form of category theory in mathlib. But we do not want to state average theorems in (topology, analysis, linear algebra, group theory etc..) in terms of category theory. The reason is simple: category theory requires us to bundle everything up into one type. Where bundle means that we need to pack all data into one object, for example the type and the corresponding topological structure.

For example topologies: the objects in the category of topological spaces are Top.{u} := Σ α : Type u, topological_space α, and the morphisms are Hom.{u} (T S : Top) := λ⟨α, hα⟩ ⟨β, hβ⟩, { f : α -> β // @continuous α hα β hβ f }. These objects are quite far away from the concrete types and functions we want to reason about, also note that the topologies and morphisms need to live in the same type universe u. Now when we work internally in topology, which means we proof that a concrete function is a continuous functions, or talking about points in a concrete topology all the baggage required for category theory is unnecessary.

Also for many proofs category does not help. It gives often nice name :-)

If there is a theorem in category with a large proof / development behind it, we still have the possibility to set up our categories and get the necessary statement.

[kbuzzard]

@johoelzl Thanks for this explanation of why carrying around a fully-fledged category is a pain in practice.

Let's start with the basics then. A presheaf F of abelian groups on a topological space X is two things.

1) A way of assigning an abelian group F(U) to every open subset U of X.

2) A way of assigning a homomorphism of abelian groups F(U)->F(V) to every pair (U,V) of open subsets of X such that V is a subset of U.

3) "All the diagrams commute", i.e. if W is in V is in U, then the map F(U)->F(W) is the same as the composition F(U)->F(V)->F(W), and the map F(U)->F(U) is the identity map.

A mathematician might describe this definition as follows. Given a topological space X one can consider the category whose objects are open sets in X and whose morphisms are inclusions (in particular, given any two objects in X there is at most one morphism between them). A presheaf of abelian groups on X is a contravariant functor from X to the category of abelian groups..

One way of thinking about it set-theoretically is that F(U) could be the (set-theoretic) functions f from U to some big ambient abelian group A, with the group law on F(U) being addition of functions : (f+g)(u)=f(u)+g(u) for u in U and f,g : U -> A. The homomorphisms F(U)->F(V) are simply restrictions of the functions on U to the subset V.

Examples of things one wants to do with F later on in the theory are:

A) The restriction of F to an open subset U of X is a presheaf on U. This is the first of many ways of building a presheaf on a new space Y from a presheaf on X, given some relation between Y and X (in this case, Y=U is an open subset of X).

B) If U_i are all open subsets of X (i running through some arbitrary index set) with union U then one would be interested in the product of the restriction maps, which is a group homomorphism from F(U) to prod_i F(U_i). This comes up in the definition of a sheaf.

C) If U_i are as above, then one would be interested in the map from prod_i F(Ui) to prod{i,j} F(U_i intersect U_j) which on the (i,j) component is defined as "restriction of the element of F(U_i) minus restriction of the element of F(U_j)". This comes up in the definition of a sheaf.

D) If x is a point in X then one is sometimes interested in the direct limit of F(U_i) as U_i run through all the open sets containing x. This is called the stalk of F at x and is a fundamental invariant.

E) If F and G are two such presheaves then one would also be interested in maps h : F->G, which are defined to be maps h_U: F(U)->G(U) for all U, such that the two induced maps F(U)->G(U)->G(V) and F(U)->F(V)->G(V) are equal. These are the morphisms in the category of presheaves on a fixed topological space X.

The notion of a presheaf is a basic notion in geometry and is used well beyond algebraic geometry; it's used in topology and differential geometry as well. This might be a good place to start with this issue. How might one package a presheaf F up in Lean? Are there multiple ways to do it and each has its advantages?

[PatrickMassot]

I'm not fully convinced by @johoelzl comment. I agree there is a certain amount of overhead in using categories. But I hope this amount of overhead is something that could be handled transparently using the type class and coercion mechanisms. Otherwise I'm not very optimistic about this scheme issue. Any mathematical object at least as complicated as a scheme will need a lot of help from Lean to be manageable.

[kbuzzard]

I've formalised the first of the four notions that I mentioned above -- a sheaf of rings on a topological space. I don't really see any obstruction to formalising a scheme. What I am somehow dreading is actually having to prove anything at all about schemes. This makes me think a little. One could imagine making some "front end" for schemes, where the end user who knows nothing about the nuts and bolts of the formalisation can just work, and in theory I suppose the whole logic of the formalisation can just be ripped up and replaced with some different implementation. Is this some standard idea? I realise now that my primary goal of "make anything as long as it is mathematically valid, however difficult it is to use" might not be quite the right goal. There will also be the issue of maintaining the code I guess, but I am hoping that code I write nowadays is becoming more and more maintainable...

[kim-em]

I just defined a sheaf (just of sets, but any category with a product is probably not much harder) in my category theory library, at https://github.com/semorrison/lean-category-theory/blob/94427dbac71374f9660f60a218f4f36f7d578874/src/categories/examples/sheaves.lean#L65. The definition of Sheaf itself looks like:

structure Sheaf { α } ( X : topological_space α ) :=
  ( presheaf        : Presheaf X )
  ( sheaf_condition : Π ( U : OpenCovering X ) ( s : CompatibleSections U presheaf ), Gluing s )

and after that you have to descend the rabbit hole of Presheaf, OpenCovering, CompatibleSection, and Gluing.

I'm curious @kbuzzard, to hear what you think about this sort of approach.

[kbuzzard]

Ok so @kckennylau and I just finished the definition of a scheme (for some value of "finished"). It barely works, but it compiles and I believe is a mathematically correct definition. It turned out that the vast majority of the work was the many constructions needed in commutative algebra to make affine schemes work, for example localization plus all the lemmas that go with it. We only had to really engage with presheaves and sheaves over the last few days and I really felt that our approach stank. We defined presheaves of types, and presheaves of rings as some way of putting a ring structure on each of the types such that all the maps were ring maps etc. We had trouble with type class inference, perhaps because we're not experts, but ultimately we ended up steering clear. I do wonder whether using categories would have made this last bit cleaner. @semorrison We did import your library as a dependency, it was disconcerting running lean build on our project and seeing assertion violations coming from your library files :-) We didn't use it yet, but if we do adic spaces next then we might need sheaves of topological rings and for these I am currently unclear about whether the category approach would be better or worse. We can close this issue now I guess. I will try and write up a perfectoid space issue later on when I have more of a roadmap in my head.

[kim-em]

Sorry about the assertion violations. I think the latest version of my library, and the latest version of Lean, should be free of them.