Zulip Chat Archive

Stream: Is there code for X?

Topic: sheafification of presheaf of ab groups


view this post on Zulip Kevin Buzzard (Oct 17 2020 at 18:54):

I need to catch up after some time only paying very superficial attention to what's been going on. I am supposed to be giving a graduate algebraic geometry Lean course in January. The first exercise in Hartshorne Chapter 2 involves sheafification of a presheaf of abelian groups. I can find sheafification of sheaves of types -- what do we need to sheafify abelian group-valued presheaves? Is the problem something I can understand -- or is it already there?

view this post on Zulip Adam Topaz (Oct 17 2020 at 19:02):

I think the main thing that's needed is the fact that the forgetful functor from abelian groups to types preserves filtered colimits.

view this post on Zulip Adam Topaz (Oct 17 2020 at 19:03):

There may be a hack to get around this by using the low-level docs#Top.prelocal_predicate.sheafify

view this post on Zulip Adam Topaz (Oct 17 2020 at 19:03):

And adding abelian group instances to the types involved, as well as subgroup structures to the predicates appearing there.

view this post on Zulip Adam Topaz (Oct 17 2020 at 19:40):

Unfortunately, the sheafification of a type valued presheaf is defined in terms of this Top.prelocal_predicate.sheafify, and not in the "usual" way as a colimit over all open covers, so I don't know if the fact that the fact about filtered colimits I mentioned above would even be useful :-/

view this post on Zulip Kevin Buzzard (Oct 17 2020 at 21:41):

This is just like localisation isn't it -- the sheafification is defined up to unique isomorphism and it ultimately hopefully won't matter which model is used. So I guess there should be a predicate on morphisms from presheaves to sheaves saying "I am a sheafification". Do we have that?

view this post on Zulip Adam Topaz (Oct 17 2020 at 21:41):

I don't think mathlib has the fact that the sheafification is left adjoint...

view this post on Zulip Adam Topaz (Oct 17 2020 at 21:42):

If it did, then sure, you can use that as the defining property :)

view this post on Zulip Adam Topaz (Oct 17 2020 at 21:42):

https://github.com/leanprover-community/mathlib/blob/b145c36fdce63f4a4772da3e9a9a3c32f41bc434/src/topology/sheaves/sheafify.lean#L26

view this post on Zulip Adam Topaz (Oct 17 2020 at 21:43):

That's listed under "future work"

view this post on Zulip Kevin Buzzard (Oct 17 2020 at 22:05):

I think I'm asking something different. If I have a presheaf F and a sheaf G and a map of presheaves from F to G, then there's a predicate which says "G is the sheafification of F", which is just some universal property about maps from presheaves to sheaves. I see -- I'm just asking about the universal property of sheafification of a fixed presheaf.

view this post on Zulip Adam Topaz (Oct 17 2020 at 22:06):

Right, the sheafification of F\mathscr{F} is the initial sheaf F\mathscr{F}^\dagger with a morphism of presheaves FF\mathscr{F} \to \mathscr{F}^\dagger, but if you unravel this, the condition is equivalent to saying that sheafification is left adjoint to the forgetful functor.
Anyway, neither description seems to be in mathlib at this point.

view this post on Zulip Adam Topaz (Oct 17 2020 at 22:08):

Oh, I guess F\mathscr{F}^\sharp is the usual notation?

view this post on Zulip Kevin Buzzard (Oct 17 2020 at 22:08):

What I'm confused about is that the statement "sheafification is adjoint to the forgetful functor" is a statement about the functor which can sheafifiy any presheaf, whereas the sheafification of one fixed presheaf also has a universal property.

view this post on Zulip Kevin Buzzard (Oct 17 2020 at 22:08):

I think there are several notations -- there is also this "double plus" notation

view this post on Zulip Kevin Buzzard (Oct 17 2020 at 22:08):

where you apply a functor twice. This is what made me realise that there isn't "the sheafification" -- one just needs some random construction and then one should talk about all the sheafifications i.e. everything satisfying the universal property

view this post on Zulip Adam Topaz (Oct 17 2020 at 22:09):

But the functorial properties follow from the universal property. For example if you have a morphism of presheaves FG\mathscr{F} \to \mathscr{G}, then the universal property of the sheafification tells you that you can lift the composition FGG\mathscr{F} \to \mathscr{G} \to \mathscr{G}^\sharp to a morphism of sheaves FG\mathscr{F}^\sharp \to \mathscr{G}^\sharp.

view this post on Zulip Kevin Buzzard (Oct 17 2020 at 22:10):

Right. But I am imagining a situation where there is no functor involved.

view this post on Zulip Kevin Buzzard (Oct 17 2020 at 22:10):

so you can't prove anything is an adjoint

view this post on Zulip Kevin Buzzard (Oct 17 2020 at 22:11):

I am talking about the characterisation of the morphism from F to F+, not the characterisation of + itself. But it's OK, I don't have any more questions, i can see there is a lot to do

view this post on Zulip Adam Topaz (Oct 17 2020 at 22:11):

Yeah, it's a lot :-/

view this post on Zulip Adam Topaz (Oct 17 2020 at 22:13):

I guess the first thing to do would be to prove that a moprhism from a presheaf F\mathscr{F} to a sheaf G\mathscr{G} can be lifted to a morphism of sheaves FG\mathscr{F}^\sharp \to \mathscr{G}. Even this I don't think is in mathlib yet.

view this post on Zulip Kevin Buzzard (Oct 17 2020 at 22:19):

Should all this be done for sheaves of types, and then some magic descends it all to sheaves of "algebraic objects" or whatever they're called? (i.e. not topological rings but pretty much all the other things which show up in basic alg geom)

view this post on Zulip Adam Topaz (Oct 17 2020 at 22:21):

I don't know. Maybe @Scott Morrison is the right person to ask?

view this post on Zulip Adam Topaz (Oct 17 2020 at 22:39):

I mean... if we had a description of the sections of the sheafification of a presheaf valued in types in terms of some colimit of some equalizers or something like this, then I can imagine some abstract nonsense argument giving sheafification in algebraic categories since their forgetful functors to types preserve the correct (co)limits. But I don't know if there is a way to see this just from the universal property of the sheafification without this explicit description of its sections.

view this post on Zulip Scott Morrison (Oct 18 2020 at 03:35):

Yeah, I forget how this goes. I dimly remember that the treatment in Stacks explained why sheaves of algebraic things was easy after you'd done the forget/sheafification adjunction for sheaves of types.

view this post on Zulip Scott Morrison (Oct 18 2020 at 03:35):

I've been meaning to get back to doing that adjunction, but haven't spent so much time with Lean the last few weeks.

view this post on Zulip Adam Topaz (Oct 18 2020 at 04:07):

I think the argument in the following link should work with what's currently in mathlib:

https://stacks.math.columbia.edu/tag/0083


Last updated: May 19 2021 at 02:10 UTC