Zulip Chat Archive

Stream: maths

Topic: sheaves on a base, etc.


view this post on Zulip Jack J Garzella (Jul 30 2020 at 14:41):

(pre)Sheaves on a base have a very similar definitions, proofs, etc. to "regular" sheaves. Maybe I'm getting too greedy, but is there a way we could unify the definitions? Instead of a contravariant functor from opens X to a category, could we replace opens X with an "open-sets-like" category that might work with a topoligical base?

Also this might be nice when we do sites...

view this post on Zulip Johan Commelin (Jul 30 2020 at 18:57):

@Jack J Garzella Yes, this can be done

view this post on Zulip Johan Commelin (Jul 30 2020 at 18:58):

In fact, I did it in lean about 1.5 years ago. But that approach to sheaves didn't really work, for reasons that I didn't really understand.

view this post on Zulip Johan Commelin (Jul 30 2020 at 19:00):

See https://ncatlab.org/nlab/show/coverage#Examples for the informal explanations

view this post on Zulip Jack J Garzella (Jul 30 2020 at 22:43):

@Johan Commelin Do you have that code in a repo somewhere?

view this post on Zulip Jack J Garzella (Jul 30 2020 at 22:43):

Probably in the meantime I'll just make a new definition for sheaves on a base

view this post on Zulip Johan Commelin (Jul 31 2020 at 04:32):

I think I don't even have the code anymore

view this post on Zulip Johan Commelin (Jul 31 2020 at 04:32):

But I think @Bhavik Mehta has sites and sheaves in his topos repo

view this post on Zulip Bhavik Mehta (Jul 31 2020 at 12:51):

Yup, I've got a definition of sites, and sheaves on a site

view this post on Zulip Kevin Buzzard (Jul 31 2020 at 14:16):

Are they in mathlib?

view this post on Zulip Bhavik Mehta (Jul 31 2020 at 14:19):

Not yet

view this post on Zulip Jack J Garzella (Jul 31 2020 at 17:30):

I guess my point was that right now the plain is to separately define sheaves on a topological space, site, topological basis, and not use coverages for now, right?

view this post on Zulip Kevin Buzzard (Jul 31 2020 at 17:36):

It's not so clear that there is a plan. When I wanted to define schemes, category theory was not really ready, so I just made sheaves of types on a space, sheaves of types on a basis, sheaves of rings etc all by hand and all differently. It's pretty painless that way, but involves a bunch of repetition. Now of course the general story would be to define sites and then sheaves of X on a site, where X are objects in some category which has enough structure the concept of a sheaf to make sense (e.g. commutative rings, abelian groups...). Now all of a sudden things are going to take a lot longer because Bhavik didn't PR his work because he's a PhD student with a thesis to worry about, and Scott didn't do sheaves in the category theory library yet because he can't figure out a nice API and has 100 other things to worry about, so all of a sudden things start proceeding more slowly. This is the nature of the area. There is no plan. The plan is whatever someone can find the time to do.

view this post on Zulip Kevin Buzzard (Jul 31 2020 at 17:37):

Behold, many files which can be unified: https://github.com/ramonfmir/lean-scheme/tree/master/src/sheaves but Ramon Mir needed to graduate so he did everything separately.

view this post on Zulip Bhavik Mehta (Jul 31 2020 at 17:41):

A definition of a sheaf (for a site) is here: https://github.com/b-mehta/topos/blob/master/src/grothendieck.lean (any of the good bits are due to Ed, all the mistakes are mine), and the definition of the obvious site for a space is in opens.lean

view this post on Zulip Kevin Buzzard (Jul 31 2020 at 17:42):

I think the geology mistake was Ed's IIRC

view this post on Zulip Bhavik Mehta (Jul 31 2020 at 17:43):

That's not a mistake :P

view this post on Zulip Kevin Buzzard (Jul 31 2020 at 17:43):

It's definitely a good bit :-) How far is this from being PR'able?

view this post on Zulip Bhavik Mehta (Jul 31 2020 at 17:44):

To be honest I don't see anything immediate that needs to be changed there (from my perspective at least), the main reason I haven't made the PR myself for that bit is just time

view this post on Zulip Bhavik Mehta (Jul 31 2020 at 17:45):

There's obviously no actual sheaf api but that's something that should be left to people who aren't me anyway


Last updated: May 11 2021 at 17:39 UTC