universal property of sheafification (on topological spaces)

Stream: Is there code for X?

[Jujian Zhang]

In topology/sheaves/sheafify.lean, it is listed that there is no sheafification as a functor; and I would like to try that. Just to be safe, there is no universal property of sheafification right? I.e. $f : F \to G$ is a morphism from presheaf to sheaf (of Types), then it factors uniquely as F.to_sheafify and F.sheafify -> G .

[Andrew Yang]

I believe it is docs#category_theory.grothendieck_topology.sheafify_lift, though it is for sheaves on sites.

[Johan Commelin]

Can't we reuse all the sheafification API that Adam has built?

[Johan Commelin]

He really did a lot. It doesn't make much sense to redo all of that.

[Andrew Yang]

I think the culprit is that the docs of file#topology/sheaves/sheafify is not updated.

[Jujian Zhang]

Andrew Yang said:

I believe it is docs#category_theory.grothendieck_topology.sheafify_lift, though it is for sheaves on sites.

I am not sure, because it seems to me that sheafification of presheaves on sites and on topological spaces used very different approach, so it is not entirely trivial that the two approaches are isomorphic

[Jujian Zhang]

Johan Commelin said:

Can't we reuse all the sheafification API that Adam has built?

So, in order to translate stuff from presheaves on sites to presheaves on Top, it might be easier to show universal property of sheafification on Tops first

[Andrew Yang]

Probably showing that the stalks of grothendieck_topology.sheafify_lift F.to_sheafify _ is iso will do. I believe it wouldn't be that hard.
That said, is there a reason why you must use topology/sheaves/sheafify.lean? I would rather make that file deprecated.

[Andrew Yang]

There might still be value in keeping that file and proving the iso as a sanity check though. But I don't think that file should be used any further

[Jujian Zhang]

Andrew Yang said:

Probably showing that the stalks of grothendieck_topology.sheafify_lift F.to_sheafify _ is iso will do. I believe it wouldn't be that hard.
That said, is there a reason why you must use topology/sheaves/sheafify.lean? I would rather make that file deprecated.

Nothing in particular, I am trying to play with sheafification of presheaf of modules, that is the first file I looked at.

[Jujian Zhang]

Is there a quick way to see where topology/sheaves/sheafify.lean is used so that we can see how hard it is to deprecate this file?

[Yaël Dillies]

Look at what files import it: https://leanprover-community.github.io/mathlib_docs/topology/sheaves/sheafify.html

[Yaël Dillies]

The answer is :zero:

[Jujian Zhang]

@Andrew Yang so deprecating this file literally cost nothing

[Johan Commelin]

I think there is already an effort underway to redefine sheaves on a topological space via sheaves on a site.