sheaves on a base, etc.

Stream: maths

[Jack J Garzella]

(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...

[Johan Commelin]

@Jack J Garzella Yes, this can be done

[Johan Commelin]

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.

[Johan Commelin]

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

[Jack J Garzella]

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

[Jack J Garzella]

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

[Johan Commelin]

I think I don't even have the code anymore

[Johan Commelin]

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

[Bhavik Mehta]

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

[Kevin Buzzard]

Are they in mathlib?

[Bhavik Mehta]

Not yet

[Jack J Garzella]

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?

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Bhavik Mehta]

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

[Kevin Buzzard]

I think the geology mistake was Ed's IIRC

[Bhavik Mehta]

That's not a mistake :P

[Kevin Buzzard]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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