leanprover-community / mathlib3

Lean 3's obsolete mathematical components library: please use mathlib4
https://leanprover-community.github.io/lean3
Apache License 2.0
1.67k stars 298 forks source link

Why are sheaves, sheaves? #1462

Open kim-em opened 5 years ago

kim-em commented 5 years ago

The reason why many sheaves satisfy the sheaf condition is that they consist of some collection of "functions to a target space" satisfying a further predicate which is "local", i.e. can be checked by checking it on some open neighbourhood of every point.

The simplest example of this is the sheaf of continuous functions into a fixed target space Y: clearly continuity of a map X -> Y is local in this sense.

However we'd like to build something quite a bit more general. As examples we'd like to show:

all give sheaves.

This note is an attempt to organise my thoughts on how to prove these statements uniformly and without repeating ourselves.

You'll see that I immediately start using category theoretic langauge. I don't think that the eventual API will need to expose any of this. (I know that people who think about holomorphic functions, for example, tend to be allergic to categories, and that's fine.) In the end to "do a particular example", you'll just need to check a locality property for your class of functions.


Let C be a category. (Think C = Type and C = CommRing as your examples. We'll be building sheaves of Cs.)

Let Q : OpenEmbeddingsᵒᵖ ⥤ Type be a functor, which we're thinking of associating the set of "Q-structures" to each topological space X, in a way that we can always pull back Q-structures along open embeddings.

Examples:

Recall Q.elements is the category of pairs (X, S), where X is a topological space, and S is a Q-structure, and morphisms (X, S) ⟶ (Y, T) are open embeddings of Y in X, such that T is the pullback of S along the open embedding.

Finally, let F : Q.elements ⥤ C be a functor. Except where specified below, C = Type, although many of the below can be generalised with other values of C.

Examples:

Given this data we get a presheaf on any topological space X equipped with a Q-structure E. Given an open set U in X, pull back E along the inclusion, to obtain E|U, and then the presheaf assigns F(U, E|U). We get functoriality "for free" from the fact that F was a functor out of Q.elements.

What more do we need to know to ensure that this is a sheaf?

I think all the examples fit into two classes:

I better explain what was going on there.

First, what are the components of b? For each (X, E) : Q.elements, we have a b.app (X, E), and this is a function from the type that F associates to (X, E) to the dependent functions on X with type a.app X E. You should think of this as a function forgetting that "smooth" sections are "smooth", for various values of "smooth"!

Second, here are the values of a and b in the examples:

Now we need to say what it means that "b is a local condition".

Given an (X : Top, E : Q X), and a dependent function f : a.app X E (which, behold, really is a dependent function type!), we want to know whether f is in the image of b. "Locality" means that it suffices to check that for every x : X, there is an open nbhd x ∈ U ⊆ X so that f restricted to U is in the image of b.

Finally, we need to explain why the locality of b lets us establish the sheaf condition. Suppose we have a collection of open sets, and some "sections" of the canonical presheaf over those open sets. (I'm assuming here that C is a concrete category; I haven't thought whether this matters.) We can turn all those sections into merely dependent functions on the open sets, and those we know how to glue. By locality, that glued together dependent function is in the image of b, so we take a preimage and have obtained a "glued together section". Now injectivity of b shows that this was the only possible "glued together section", because at the level of functions we have this uniqueness.

kim-em commented 5 years ago

@jcommelin, this is my promised note on checking the sheaf condition!

jcommelin commented 5 years ago

Thanks! This looks quite promising!

jcommelin commented 5 years ago

One question I have is whether we should try to be even more general, and replace OpenEmbeddings by covers on an arbitrary site... (and then specialize to the case you describe). All in all, I think this is a very nice approach to unifying all the variations of sheaves that we encounter.

kbuzzard commented 5 years ago

This is all a bit too topological for me. Can you explain an algebro-geometric example?

jcommelin commented 5 years ago

Most sheaves in algebraic geometry do not consist of "functions to a target space". We think of them like that, and it's a powerful intuition, but in the end an element of a non-reduced F_p-algebra is just not a function. On the other hand, sheaves of (smooth/holomorphic/continuous) functions all have sections that are really honest functions. Of course, even in the case of a non-reduced F_p-algebra, we could view a section as a dependent function to the Pi-type of all stalks... but I'm not sure if that is a useful thing to do. I think Scott is proposing a line of attack that would make it possible to move between "function" and "section of sheaf" without too much effort, in the cases where it makes sense, e.g., sheaves of (smooth/holomorphic/continuous) functions or sections of a vector bundle (in the analytic sense), etc.

kbuzzard commented 5 years ago

But we still wouldn't be able to glue sheaves of modules. Can I let Q(X) be the scheme structures on X though? This seems like it might work.

kbuzzard commented 5 years ago

I guess Scott is coming from a topological background though. It seems that if we want the etale site then this is a generalisation in a different direction, as you were pointing out earlier.