Sheaf theory for the working mathematician

Stream: mathlib4

[David Loeffler]

I was looking through the slides of @Adam Topaz 's very interesting seminar and it prompted the following question.

Suppose I have topological spaces X, Y, an open cover X = ⋃ i : ι, U i, and for each i, a continuous function f i : U i → Y, agreeing on overlaps. How do I get my hands on the unique continuous function F : X → Y whose restriction to each U i is f i?

The existence and uniqueness of this F, of course, exactly the statement that continuous functions form a sheaf. So is there a simple way of extracting this concrete statement from all the general machinery of sites and coverages etc?

I'm asking because I'm pretty sure I've proved several special instances of this by hand before in mathlib – e.g. in defining the Gamma function, you first give some formula that works for -n < re s for each n : ℕ, and then you patch them together (so you even have an increasing open cover). I'm curious whether there's now a "morally sound" way of doing this.

[Adam Topaz]

@David Loeffler you can certainly do this. One way is to deal concretely with docs#CategoryTheory.Presieve.IsSheafFor using the appropriate Grothendieck topology (in this case I suppose that docs#Opens.grothendieckTopology is the appropriate one). Note that the coverage I defined in my talk is unfortunately not how things are set up in mathlib.

[Adam Topaz]

unfortunately I also don't think mathlib yet knows that this Grothendieck topology on Opens is subcanonical, which is what your assertion would boil down to.

[Adam Topaz]

The closest I could find for gluing in the topological context is TopCat.GlueData.openCoverGlueHomeo

[David Loeffler]

I admit I'm not used to seeing the word "concretely" used together with ones like "presieve" or "subcanonical Grothendieck topology" :smile:

[Adam Topaz]

@Andrew Yang do we have the plain topological analogue of, say, docs#AlgebraicGeometry.Scheme.OpenCover.glueMorphisms ?

[David Loeffler]

Adam Topaz said:

Andrew Yang do we have the plain topological analogue of, say, docs#AlgebraicGeometry.Scheme.OpenCover.glueMorphisms ?

Indeed, it seems that what I'm after is exactly the topological analogue of that.

[Andrew Yang]

The relevent file is file#Mathlib/Topology/Gluing. We don't have glueMorphisms for topological spaces but one may mimic docs#AlgebraicGeometry.Scheme.OpenCover.gluedCover to get a glue data associated to a open cover.