sheafification of presheaf of ab groups

Stream: Is there code for X?

[Kevin Buzzard]

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?

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

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 :-/

[Kevin Buzzard]

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?

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

That's listed under "future work"

[Kevin Buzzard]

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.

[Adam Topaz]

Right, the sheafification of $\mathscr{F}$ is the initial sheaf $\mathscr{F}^\dagger$ with a morphism of presheaves $\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.

[Adam Topaz]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Adam Topaz]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

so you can't prove anything is an adjoint

[Kevin Buzzard]

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

[Adam Topaz]

Yeah, it's a lot :-/

[Adam Topaz]

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

[Kevin Buzzard]

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)

[Adam Topaz]

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

[Adam Topaz]

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.

[Scott Morrison]

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.

[Scott Morrison]

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

[Adam Topaz]

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

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