## Stream: general

### Topic: stuck proving sheafify is a functor

#### Alexandra Foster (Jul 03 2021 at 20:27):

So, I am trying to prove that sheafify is a functor, but the context I need it in is specialized to sheaves of abelian groups over a space. I attempted to specialize the definition of sheafify in mathlib:

import algebra.category.Group.basic
import algebra.category.Group.limits
import topology.sheaves.sheaf
import topology.sheaves.presheaf
import topology.sheaves.sheafify
import category_theory.limits.has_limits
import category_theory.limits.shapes.products
import category_theory.functor
import topology.category.Top.basic

variable X : Top

def Ab.has_products
: category_theory.limits.has_products Ab
:=
begin
have h : category_theory.limits.has_limits Ab := AddCommGroup.has_limits,
intro J,
refine {has_limit := id
(λ (F : category_theory.discrete J ⥤ Ab), category_theory.limits.has_limit_of_has_limits_of_shape F)},
end

-- sheafify is a functor
def sheafify_functor : Top.presheaf Ab X ⥤ Top.sheaf Ab X
:=
begin
have sh : Top.presheaf Ab X → Top.sheaf Ab X := Top.presheaf.sheafify,
end


But Lean complained that it could not do it:

invalid type ascription, term has type
Top.presheaf (Type ?) ?m_1 → Top.sheaf (Type ?) ?m_1 : Type (?+1)
but is expected to have type
Top.presheaf Ab X → Top.sheaf Ab X : Type (u_1+1)
state:
X : Top
⊢ Top.presheaf Ab X ⥤ Top.sheaf Ab X


Is there some kind of magic with dependent quantifiers or universes that I'm not taking into account when I write this? Alternately: is the result I'm trying to prove already in mathlib, hidden from my eyes?

#### Markus Himmel (Jul 04 2021 at 07:47):

I believe that you get the error because Top.presheaf.sheafify currently only works for Type-valued presheaves and you are trying to sheafify Ab-valued presheaves.

#### Markus Himmel (Jul 04 2021 at 07:54):

I'm don't know what the current plans regarding sheafification of Ab-valued presheaves are. Perhaps @Scott Morrison or @Bhavik Mehta know whether there has been any work on this?

#### Alexandra Foster (Jul 06 2021 at 17:43):

I am indeed starting to think the problem is with Top.presheaf.sheafify -- Top.presheaf and Top.sheaf both have a variable C : Type u with [category.{v} C] and then work with Top.presheaf C X or Top.sheaf C X, which is no problem and lets me consider (pre)sheaves valued in Ab or whatever category with products I want, but then Top.sheafify works on Top.presheaf (Type u) X, rather than on some C : Type u. Although I can... imagine some kind of abstract justification of why this kind of makes sense, I suspect it doesn't give me any way of getting Top.sheafify for sheaves defined in any specific category that I have, Ab or otherwise. Changing it to use a C : Type u seems like a fairly easy fix, so I'll give it a shot.

#### Alexandra Foster (Jul 06 2021 at 17:52):

... hm. maybe not so easy after all. I'll chip away at it anyway

#### Johan Commelin (Jul 06 2021 at 17:55):

You'll need a bunch of assumptions on C, right?

#### Alexandra Foster (Jul 06 2021 at 17:56):

yeah, being a category with products, probably

#### Alexandra Foster (Jul 06 2021 at 17:58):

and it seems like all the local_predicate stuff also is defined only on Type-valued (pre)sheaves also

#### Justus Springer (Jul 06 2021 at 19:15):

A lot of stuff is only defined for Type-valued sheaves unfortunately. I have also wished before that the sheaves library would be more general in this regard and it might be a nice project. I don't know what class of categories would be best suited for this. It probably should have pi instances so all the stuff from sheaf_of_functions makes sense. Maybe someone who knows more about sheaves than me can comment.

#### Justus Springer (Jul 06 2021 at 19:22):

For now, a different approach might be to sheafify the underlying Type-valued sheaf by composing with the forgetful functor Ab ⥤ Type. Then you could show that the sections s : Π x : X, F.stalk x being locally germs form a subgroup of all sections and use that to define the add_comm_group structure on the sheafified Type-valued sheaf, turning it into a proper Ab-valued sheaf. I'm not completely sure this would work but it might be worth a try. You might want to look at algebraic_geometry/structure_sheaf where something similar is done to define a CommRing-valued sheaf.

Last updated: Dec 20 2023 at 11:08 UTC