## Stream: maths

### Topic: gluing presheaves

#### Scott Morrison (Jul 24 2019 at 00:59):

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 (Jul 24 2019 at 04:31):

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 (Jul 27 2019 at 00:16):

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 (Jul 27 2019 at 00:18):

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 (Aug 11 2019 at 11:21):

@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 (Aug 11 2019 at 11:22):

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 (Aug 11 2019 at 11:23):

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

#### Kevin Buzzard (Aug 11 2019 at 11:26):

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 (Aug 11 2019 at 11:45):

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 (Aug 11 2019 at 11:46):

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 (Aug 24 2019 at 14:57):

@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 (Aug 27 2019 at 00:14):

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 (Aug 27 2019 at 00:14):

It will just take some more work. :-)

#### Scott Morrison (Aug 27 2019 at 00:15):

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 (Aug 27 2019 at 10:23):

@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 (Aug 28 2019 at 04:48):

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 (Aug 28 2019 at 04:49):

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 (Aug 28 2019 at 04:50):

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 (Aug 28 2019 at 04:50):

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

#### Johan Commelin (Aug 28 2019 at 04:53):

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 (Aug 29 2019 at 00:00):

@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 (Sep 03 2019 at 11:26):

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

#### Jean Lo (Sep 03 2019 at 11:30):

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 (Sep 03 2019 at 11:36):

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

Last updated: May 11 2021 at 16:22 UTC