Definition of a scheme about mathlib HOT 10 CLOSED

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?

from mathlib.

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.

from mathlib.

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.

from mathlib.

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.

from mathlib.

@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(U_i) 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?

from mathlib.

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.

from mathlib.

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

from mathlib.

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.

from mathlib.

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.

from mathlib.

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

from mathlib.