mathlib

mathlib copied to clipboard

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:

• C^k functions,
• holomorphic functions,
• (flat?) sections of a vector bundle

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:

• Q X = punit, "no extra structure"
• Q X = Fibr X, "all fibrations with base space X"
• Q X = Bun X, "all topological fibre bundles on X" (related: all vector bundles, all line bundles, all principal G-bundles)
• Q X = Mfld G X, "all manifolds with structure group G, with underlying topological space X"

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:

• Q X = punit, and F (X, ()) = arbitrary functions from X to Y
• Q X = punit, and F (X, ()) = continuous maps X to Y, for some fixed topological space Y
• Q X = punit, C = CommRing, and F(X, ()) = the ring of continuous maps X to Y for some fixed Y
• Q X = (X → Type) (ignoring topology), and F (X, E) = Π x : X, E x, i.e. the type of set-theoretic sections of E.
• Q X = Fibr X, and F (X, E) = continuous sections of the fibration E
• Q X = Bun X, and F (X, E) = continuous sections of the bundle E
• Q X = Mfld G X, and F (X, E) = smooth functions to X to Y, for some fixed G-structured manifold Y (notice this example includes holomorphic functions)

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:

• ("the base case"), Q0 X = (X → Type), F0 (X, E) = sections of E, which ignores entirely the topology on X, and the sheaf condition is just that dependent functions on subsets can be uniquely glued together
• ("the reduction") I think "all the interesting examples" above have a natural transformation a : Q ⟶ Q0, which induces a functor A : Q.elements ⥤ Q0.elements, and another natural transformation b : F ⟶ (A ⋙ F0), whose components are injective, and whether a function is in the image of b "can be checked locally", and this implies the sheaf condition.

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:

• if Q X = punit, and F (X, ()) = arbitrary functions from X to Y, then a sends punit.star to the constant function with value Y, and b is the identity (sending functions X to Y to themselves).
• if Q X = punit, and F (X, ()) = continuous maps X to Y, for some fixed topological space Y, then again a sends punit.star to the constant function with value Y, and b is the inclusion of continuous functions into all functions X to Y.
• if Q X = punit, C = CommRing, and F(X, ()) = the ring of continuous maps X to Y for some fixed Y then a and b are the same, but we note that the components of b are ring homomorphisms, as required.
• if Q X = (X → Type) (ignoring topology), and F (X, E) = Π x : X, E x, i.e. the type of set-theoretic sections of E we're exactly in the base case, so a and b are the identity.
• if Q X = Fibr X, and F (X, E) = continuous sections of the fibration E, a is the natural transformation sending a fibration to the function describing the type of the fibre over each point (i.e. forgetting the topology of the fibration), and b includes the continuous sections amongst all sections.
• if Q X = Bun X, and F (X, E) = continuous sections of the bundle E, a is the natural transformation sending an bundle to the constant function whose value is the type of the fibre, and again b includes continuous sections amongst all sections.
• if Q X = Mfld G X, and F (X, E) = smooth functions to X to Y, for some fixed G-structured manifold Y, then a sends a manifold structure to the constant function with value the underlying type of Y, and b includes the smooth function amongst arbitrary sections.

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.