Stream: maths

Topic: Sheaf condition for type-valued sheaf

Justus Springer (Mar 26 2021 at 11:29):

So in topology/sheaves/sheaf_condition there are currently three equivalent formulations of the sheaf condition, all of which are stated for a sheaf valued in an arbitrary category. When working with type-valued sheaves, I find myself wanting a more explicit formulation, i.e. that for some family of open sets U : ι → opens X, every compatible family of sections s : Π i : ι, F.obj (op (U i)) admits a unique gluing t : F.obj (op (supr U)). In particular I want to conclude that if two sections s t : F.obj (op V) agree locally on an open cover, they must already be equal. Is there a straight-forward way to obtain this fact from the categorical definition of the sheaf condition? The most promising lemma I found in the library is unique_of_type_equalizer in category_theory/limits/shapes/types.lean, which gives an explicit construction of equalizers in the category of types. Would this be the way to go?

Follow-up question: Would an API for the sheaf condition of type-valued sheaves, which proves the facts from above, be desirable?

Johan Commelin (Mar 26 2021 at 11:31):

I think https://github.com/leanprover-community/mathlib/blob/master/src/topology/sheaves/local_predicate.lean was designed for working with "hands-on" sheaves

Johan Commelin (Mar 26 2021 at 11:32):

But I forgot to what extent we know that all the different sheaf conditions can be swapped in and out for eachother

Justus Springer (Mar 26 2021 at 11:33):

local_predicate.lean only talks about sheaves of functions, no?

Scott Morrison (Mar 26 2021 at 11:38):

Yes, I don't think local_predicate.lean is what you want.

Scott Morrison (Mar 26 2021 at 11:39):

The sheaf conditions in topology/sheaves/sheaf_condition are all proved equivalent. (We have yet more sheaf conditions for sheaves on a site, and I think they are still disconnected from the earlier development of sheaves on a space, however.)

Scott Morrison (Mar 26 2021 at 11:39):

I suspect that what you want, @Justus Springer, is not actually there yet. This part of the library is pretty new!

Scott Morrison (Mar 26 2021 at 11:46):

Oh, sorry, I think I misspoke about local_predicate.lean. Maybe Johan meant you should use it along with something in sheafify to reduce to the case of dependently typed functions.

Scott Morrison (Mar 26 2021 at 11:54):

Fix some type family Z : X \to Type*, and assume your sheaf F is any subsheaf of the sheaf of sections of this family. Then your statement is obviously true. Now, we construct sheafification of a presheaf F as follows. Let Z be the stalks of F. The sheafification of F is the sheaf of sections of Z which are locally germs. This ... means that the statement is true for any sheaf, because it is the same as its sheafification?

(I have no idea if that argument is even true, let alone if it is easy to formalise given what we have... 90% of my knowledge of sheaves came from writing those files...)

Scott Morrison (Mar 26 2021 at 11:59):

Okay, forget that argument for a bit.

I don't think you need anything about unique_of_type_equalizer. You are just using that equalizer.\iota is a mono, in the equalizer diagram for the sheaf condition.

Justus Springer (Mar 26 2021 at 12:17):

Thanks for the input! I'm going to keep experimenting and maybe PR something soon.

Justus Springer (Mar 26 2021 at 12:19):

Scott Morrison said:

You are just using that equalizer.\iota is a mono

Right, this would also be an option, however this only gives me uniqueness of a gluing, but not existence I think.

Scott Morrison (Mar 26 2021 at 12:20):

Ah, I was answering directly "In particular I want to conclude that if two sections s t : F.obj (op V) agree locally on an open cover, they must already be equal."

Scott Morrison (Mar 26 2021 at 12:20):

(This is done in the spoiler block above.)

Justus Springer (Mar 26 2021 at 12:20):

True, for that it would suffice

Justus Springer (Mar 26 2021 at 12:21):

Scott Morrison said:

(This is done in the spoiler block above.)

Oh thanks a lot!

Scott Morrison (Mar 26 2021 at 12:21):

I better sleep. Have fun, looking forward to the PRs!

Bhavik Mehta (Mar 26 2021 at 12:36):

I think this formulation is given by the definition of the sheaf condition in category_theory/sites/sheaf

Justus Springer (Mar 26 2021 at 13:13):

Bhavik Mehta said:

I think this formulation is given by the definition of the sheaf condition in category_theory/sites/sheaf

I don't know much about sheaves on sites/topoi unfortunately, so this seems like even more categorical overhead to me...

Justus Springer (Mar 26 2021 at 13:14):

Can sheaves on spaces be easily subsumed by this more general framework?

Kevin Buzzard (Mar 26 2021 at 13:20):

Right -- given a top space you can make a site, and a sheaf on the space is the same thing as a sheaf on the site.

Johan Commelin (Mar 26 2021 at 13:27):

On paper...
In Lean, they are different beasts, and so you will need to work your way through an equivalence of categories :grinning:

Bhavik Mehta (Mar 26 2021 at 14:45):

Right - it's on my todo list to make the passage between the two smoother

Scott Morrison (Mar 31 2021 at 10:44):

@Justus Springer, thanks for that pair of PRs. They look really nice, and much better than what we have at the moment.

Justus Springer (Mar 31 2021 at 11:15):

Thanks a lot!
I'm now learning more about sites, so I might be able to help building the bridges between sheaves on spaces and sheaves on sites in the future.

Justus Springer (Mar 31 2021 at 11:22):

By the way, is #5927 still being developed @Bhavik Mehta ?

Bhavik Mehta (Mar 31 2021 at 12:11):

I think the changes there were mostly just about names and docs which I just haven't got around to fixing yet!

Last updated: May 11 2021 at 16:22 UTC