## Stream: maths

### Topic: sheaves on a base, etc.

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

#### Johan Commelin (Jul 30 2020 at 18:57):

@Jack J Garzella Yes, this can be done

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

#### Johan Commelin (Jul 30 2020 at 19:00):

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

#### Jack J Garzella (Jul 30 2020 at 22:43):

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

#### 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

#### Johan Commelin (Jul 31 2020 at 04:32):

I think I don't even have the code anymore

#### Johan Commelin (Jul 31 2020 at 04:32):

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

#### Bhavik Mehta (Jul 31 2020 at 12:51):

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

#### Kevin Buzzard (Jul 31 2020 at 14:16):

Are they in mathlib?

Not yet

#### 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?

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

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

#### 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

#### Kevin Buzzard (Jul 31 2020 at 17:42):

I think the geology mistake was Ed's IIRC

#### Bhavik Mehta (Jul 31 2020 at 17:43):

That's not a mistake :P

#### Kevin Buzzard (Jul 31 2020 at 17:43):

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

#### 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

#### 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