## Stream: Is there code for X?

### Topic: sheafification of presheaf of ab groups

#### 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?

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

#### 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

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

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

#### 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?

#### Adam Topaz (Oct 17 2020 at 21:41):

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

#### Adam Topaz (Oct 17 2020 at 21:42):

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

#### Adam Topaz (Oct 17 2020 at 21:42):

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

#### Adam Topaz (Oct 17 2020 at 21:43):

That's listed under "future work"

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

#### Adam Topaz (Oct 17 2020 at 22:06):

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 (Oct 17 2020 at 22:08):

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

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

#### Kevin Buzzard (Oct 17 2020 at 22:08):

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

#### 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

#### 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 $\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 (Oct 17 2020 at 22:10):

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

#### Kevin Buzzard (Oct 17 2020 at 22:10):

so you can't prove anything is an adjoint

#### 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

#### Adam Topaz (Oct 17 2020 at 22:11):

Yeah, it's a lot :-/

#### 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 $\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 (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)

#### Adam Topaz (Oct 17 2020 at 22:21):

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

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

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

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

#### 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