# Zulip Chat Archive

## 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: Aug 03 2023 at 10:10 UTC