Sheafification?

Stream: maths

[Brendan Seamas Murphy]

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]

@Brendan Seamas Murphy Welcome!

[Johan Commelin]

I'm not aware of sheafification being defined.

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Brendan Seamas Murphy]

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]

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

[Johan Commelin]

Nice!

[Johan Commelin]

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

[Johan Commelin]

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

[Brendan Seamas Murphy]

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]

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

[Johan Commelin]

Aha, I see.

[Brendan Seamas Murphy]

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

[Johan Commelin]

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

[Brendan Seamas Murphy]

Yeah lol

[Johan Commelin]

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

[Johan Commelin]

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

[Scott Morrison]

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

[Johan Commelin]

Sure, but we also want a hands on description.

[Johan Commelin]

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

[Kevin Buzzard]

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