stuck proving sheafify is a functor

Stream: general

[Alexandra Foster]

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]

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]

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]

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]

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

[Johan Commelin]

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

[Alexandra Foster]

yeah, being a category with products, probably

[Alexandra Foster]

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

[Justus Springer]

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]

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.