gluing presheaves

Stream: maths

[Scott Morrison]

Sorry I haven't been participating in the great sheaf-hunt. I had a think while walking the dog this morning about the "high-brow" way to do gluing of (pre)sheaves, and came up with the following. (IANAAG, so this may all be nonsense...)

Instead of thinking about the special case of gluing (pre)sheaves on a pair of open sets, I'd be more general, and try to construct colimits in the category of (pre)sheaved spaces. (This should avoid all the mucking about with open sets in open sets in open sets ...)

Given a diagram F : J \func (PresheafedSpace C), you can compose with the forgetful functor to Top and get a diagram of topological spaces. Take the colimit of this, and call the resulting space X. You can now pushforward the presheaves (F.obj j).𝒪 to get presheaves on X, and indeed you ... get a diagram F' : J \func (X.presheaf C). As long as C has limits, X.presheaf C automatically has limits, so we just take the limit of F' to define our final presheaf O on X.

There's a cocone on F with tip (X, O). Its j component is just the pair consisting of the inclusion of (F.obj j).to_Top into X, and the component of the limit cone for F'.

Presumably this cocone is actually universal, but I didn't think about it!

Finally, we better check that if we glue presheaves which are actually sheaves, we end up with a sheaf. The sheaf condition on G : (opens X)^op \func C says that G preserves certain limits. (In particular, limits of the "pairwise intersections" diagrams for a cover, but I think you can also get away with saying it preserves limits over arbitrary filtered (not cofiltered!) diagrams in (opens X)^op; doesn't matter either way.) Now there's just a general fact that if you have a diagram of functors, which all preserve limits of a certain shape, then the limit of that diagram of functors also preserves limits of that shape (this part is not in mathlib yet, but should be pretty easy; first prove the Fubini theorem for limits?), and this gives the result.

[Johan Commelin]

I didn't manage to get a workable version of "sheaves are presheaves that preserve limits of a certain shape". That was causing me lots of pain last november/december... however, it clearly seems like a good theorem/def to have if we want to do sheaves on sites.

[Scott Morrison]

My last paragraph was inddeed wrong; while being a sheaf is about preserving certain limits, it's not about preserves limits of a certain shape. So while I think my sketch of gluing presheaves is fine (indeed, the construction, including all the data but missing some proofs, is at https://github.com/leanprover-community/mathlib/blob/sheaves/src/algebraic_geometry/presheafed_space/colimits.lean), it's still slightly more work to glue sheaves.

[Scott Morrison]

I suspect the best way to do that is to do sheafification first, which shows sheaves are a reflective subcategory of presheaves. Then a little more work would show sheafed-spaces are a reflective subcategory of presheafed-spaces, and then the general nonsense I proved recently about reflective subcategories would give you filtered colimits (in particular, pushouts) of sheafed-spaces.

[Scott Morrison]

@Johan Commelin, I did a little more work on sheaves this afternoon. I haven't got to the interesting things (sheafification and gluing sheaves), but it seems to be going fairly smoothly so far. The only thing I've actually proved so far is that the pushforward of a sheaf is a sheaf.

[Scott Morrison]

See https://github.com/leanprover-community/mathlib/blob/sheaves/src/topology/Top/sheaf.lean

[Scott Morrison]

The highlights are:

def sheaf_condition := Π (c : cover.{v} X), preserves_limit c.diagram F

/--
A sheaf is a presheaf satisfying the sheaf condition.
-/
structure sheaf : Type (max (v+1) u) :=
(F : X.presheaf C)
(condition : F.sheaf_condition)

/--
Morphisms of sheaves are just morphisms of the underlying presheaves, so we
transfer the category structure using `induced_category.category`.
-/
instance category_sheaf (X : Top.{v}) : category (sheaf.{v} C X) :=
induced_category.category sheaf.F

/--
The pushforward of a sheaf is still a sheaf.
-/
def pushforward {X Y : Top.{v}} (f : X ⟶ Y) (ℱ : sheaf.{v} C X) : sheaf.{v} C Y :=
{ F := f _* ℱ.F,
  condition := λ c, by { dsimp [presheaf.pushforward], apply_instance } }

[Scott Morrison]

There are still a few underlying sorries in other files, but they are boring general things about preserving limits.

[Kevin Buzzard]

It's great to hear it's going well so far!

Ramon broke down the sheaf condition into two parts -- "locality" and "gluing", which for rings and groups boiled down to the assertion that to say a map was bijective was the same as saying it was injective and surjective. In general category-theoretic terms one probably cannot do this though.

[David Michael Roberts]

Reminds me of the Grothendieck +-construction on presheaves that first constructs a separated presheaf from a presheaf, then a sheaf from a separated presheaf.

[Kevin Buzzard]

Yes exactly; this is why I mentioned it. For Grothendieck the distinction was important in the construction of sheafification of a presheaf. On the other hand because a general isomorphism is more than a monomorphism which is an epimorphism I am slightly confused about what one should do in this generality.

[Johan Commelin]

@Scott Morrison Thanks for working on this! Any updates so far? I'm still hoping for some sort of synthesis with all the work done by @Kenny Lau.
Kenny, do you plan on PRing your espace etale stuff?

[Scott Morrison]

No recent news, I haven’t had a lot of space for mathlib in the last two weeks. I made a fair bit of progress on the + construction, but haven’t returned to gluing. I don’t yet see an obstacle to doing gluing “properly”, i.e. with presheaves defined as functors (open X)^\op \func C and sheaves defined by the preserves_limit condition that is now fully defined in the sheaves branch.

[Scott Morrison]

It will just take some more work. :-)

[Scott Morrison]

I’d be happy, @JohanCommelin, if you’d have a look at the sheaf condition as written in that branch as see if you’re happy with it.

[Johan Commelin]

@Scott Morrison I think it looks fine... can you prove that yoneda Top lands in sheaves? Or is that hard? There is almost no maths content in that statement.

[Scott Morrison]

You don't literally mean yoneda Top, I think. You mean something like X.toTop.op ⋙ (yoneda Top), I think -- you want to start at (opens X)^\op, and end at Type. [ED: this is in mathlib as presheaf_to_Top X T, the presheaf of continuous functions on X with values in T.]

[Scott Morrison]

I think there should be exactly the real mathematical work of that statement: if you have a bunch of continuous functions on opens sets of X, that agree on the overlaps, then there exists a unique continuous function on the union that agrees with each of them.

[Scott Morrison]

I'm actually not sure if that's in mathlib. I'll look later, and if so hook it up to prove the sheaf condition for presheaf_to_Top X T.

[Scott Morrison]

If it's not in mathlib, I won't do it right away. :-)

[Johan Commelin]

Ok, I think @Calle Sönne did the gluing of continuous functions at some point. I don't know if it ended up in mathlib.

[Scott Morrison]

@Calle Sönne, do you have this code somewhere? It doesn't seem to have made it to mathlib: https://github.com/leanprover-community/mathlib/commits?author=callesonne

[Calle Sönne]

I dont recall working on that, maybe @Jean Lo was working on it?

[Jean Lo]

yeah, I think that was me. I went on to be consumed by some other stuff, and did not put together a PR.

[Jean Lo]

unfortunately I'm currently away from home without my work computer, but here's a link to the discussion about gluing continuous functions: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/gluing.20functions