Zulip Chat Archive

Stream: maths

Topic: Sheaf condition for type-valued sheaf


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Justus Springer (Mar 26 2021 at 11:33):

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

view this post on Zulip Scott Morrison (Mar 26 2021 at 11:38):

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

view this post on Zulip 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.)

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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...)

view this post on Zulip 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.

view this post on Zulip Justus Springer (Mar 26 2021 at 12:17):

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

view this post on Zulip Scott Morrison (Mar 26 2021 at 12:19):

view this post on Zulip 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.

view this post on Zulip 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."

view this post on Zulip Scott Morrison (Mar 26 2021 at 12:20):

(This is done in the spoiler block above.)

view this post on Zulip Justus Springer (Mar 26 2021 at 12:20):

True, for that it would suffice

view this post on Zulip Justus Springer (Mar 26 2021 at 12:21):

Scott Morrison said:

(This is done in the spoiler block above.)

Oh thanks a lot!

view this post on Zulip Scott Morrison (Mar 26 2021 at 12:21):

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

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Justus Springer (Mar 26 2021 at 13:14):

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

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip Bhavik Mehta (Mar 26 2021 at 14:45):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Justus Springer (Mar 31 2021 at 11:22):

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

view this post on Zulip 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