## Stream: maths

### Topic: Sheafification?

#### Brendan Seamas Murphy (Jul 20 2019 at 03:20):

Is sheafification defined in https://github.com/ramonfmir/lean-scheme? I might have just missed it or there's a good reason for it not being added. I would be happy to work on a pull request if there's interest

#### Johan Commelin (Jul 20 2019 at 04:03):

@Brendan Seamas Murphy Welcome!

#### Johan Commelin (Jul 20 2019 at 04:03):

I'm not aware of sheafification being defined.

#### Johan Commelin (Jul 20 2019 at 04:04):

There has been lots of debate about how to implement sheafs correctly.

#### Johan Commelin (Jul 20 2019 at 04:04):

The implementation in the lean-scheme repo will most likely change substantially when being added to mathlib.

#### Johan Commelin (Jul 20 2019 at 04:04):

So I'm not sure if it is wise to make a PR to the lean-scheme repository.

#### Johan Commelin (Jul 20 2019 at 04:05):

It's very unfortunate that we aren't moving faster )-;

#### Brendan Seamas Murphy (Jul 20 2019 at 04:22):

Well I'd be happy to help, but I'm just learning this stuff for the first time so I certainly don't know the right way to implement this stuff

#### Brendan Seamas Murphy (Jul 20 2019 at 04:22):

I'm just trying to formalize a solution to a problem in hartshorne

Nice!

#### Johan Commelin (Jul 20 2019 at 04:44):

@Brendan Seamas Murphy That seems like a very nice way to dive in (-;

#### Johan Commelin (Jul 20 2019 at 04:44):

Sheaves have been quite stubborn. Which problem were you thinking of formalizing?

#### Brendan Seamas Murphy (Jul 20 2019 at 04:47):

Problem 2.1.2a, that the stalk of the the sheaf kernel/image gives you the kernel/image of the induced map on the stalks

#### Brendan Seamas Murphy (Jul 20 2019 at 04:47):

I was finding it hard to understand how the image embeds into the codomain (see problem 2.1.4) and I thought lean might be able to keep me straight

Aha, I see.

#### Brendan Seamas Murphy (Jul 20 2019 at 04:48):

To state the problem though I need (pre)sheaves of abelian groups and the sheaf image/sheafification

#### Johan Commelin (Jul 20 2019 at 04:48):

Without sheafification you won't get far with that exercise (-;

Yeah lol

#### Johan Commelin (Jul 20 2019 at 04:50):

Maybe we can kick some action into the sheaf development again.

#### Johan Commelin (Jul 20 2019 at 04:51):

@Kenny Lau @Kevin Buzzard Are there any updates since the discussions from 2 or 3 weeks ago?

#### Scott Morrison (Jul 20 2019 at 04:53):

sheafification will also be a nice test drive of my PR of reflective subcategories!

#### Johan Commelin (Jul 20 2019 at 04:54):

Sure, but we also want a hands on description.

#### Johan Commelin (Jul 20 2019 at 04:54):

And before anything like that... we first need a definition of sheaves.

#### Kevin Buzzard (Jul 20 2019 at 09:55):

@Brendan Seamas Murphy you are talking about the schemes project. If something is in mathlib then with high probability it is in some sort of shape which the experts are happy with. The schemes project is an MSc project which is "mathematically right" (in fact it's not even quite right at the minute -- the definition of scheme is wrong, it depends on the cover by affines) but which is not yet in mathlib so there are risks involved if you are thinking of doing something which will ultimately become a PR into mathlib. The issue with sheaves is that mathematically these things are completely unambiguous, but the CS people are actually making machines which model these ideas, and there is still a debate amongst the community as to which machine is best. This is a tedious implementation issue and it really should not affect any proofs, which should just use the "mathematician's interface to sheaves", but it does; indeed I think this is part of the point: if a different implementation makes proofs easier, then they want to change to that implementation.

We don't have sheafification and one can think about how one might make it. There are two approaches. One is to fix upon a concrete idea of "sheaves of X on Y" e.g. (sheaves of abelian groups on a top space) and then make it by hand. This is what @Ramon Fernandez Mir did with schemes, following me, who did it when I was learning and didn't know any other way. At the other extreme there is a glorious theory of sheaves of objects of a nice category on a site, and it would not surprise me if you could then slap down a few axioms on the objects and the site and get a general theory of sheafification. Which one do we do? Do we plough through sheaves of types on a top space, then sheaves of ab groups, sheaves of rings etc? The community is not actually sure. Glueing sheaves of types on a top space was surprisingly interesting. Glueing sheaves of objects on a site will be a lot more interesting by which I think I mean difficult.

@Scott Morrison Kenny managed to glue sheaves of types on a top space and prove the universal property, using a low-level approach and an extremely dodgy definition of sheaves on a subspace of a top space, which relied on rejecting the concept type theory's inductive equality (it was broken anyway). I think glueing is a key test for the category approach. Do you want to glue sheaves on subspaces by categorifying Kenny's work, or do it again from scratch?

Ultimately we have two ways of doing sheaves and the community has not yet understood the advantages and disadvantages of the two approaches.

Last updated: May 18 2021 at 08:14 UTC