Sheaf condition for type-valued sheaf

Stream: maths

[Justus Springer]

So in topology/sheaves/sheaf_condition there are currently three equivalent formulations of the sheaf condition, all of which are stated for a sheaf valued in an arbitrary category. When working with type-valued sheaves, I find myself wanting a more explicit formulation, i.e. that for some family of open sets U : ι → opens X, every compatible family of sections s : Π i : ι, F.obj (op (U i)) admits a unique gluing t : F.obj (op (supr U)). In particular I want to conclude that if two sections s t : F.obj (op V) agree locally on an open cover, they must already be equal. Is there a straight-forward way to obtain this fact from the categorical definition of the sheaf condition? The most promising lemma I found in the library is unique_of_type_equalizer in category_theory/limits/shapes/types.lean, which gives an explicit construction of equalizers in the category of types. Would this be the way to go?

Follow-up question: Would an API for the sheaf condition of type-valued sheaves, which proves the facts from above, be desirable?

[Johan Commelin]

I think https://github.com/leanprover-community/mathlib/blob/master/src/topology/sheaves/local_predicate.lean was designed for working with "hands-on" sheaves

[Johan Commelin]

But I forgot to what extent we know that all the different sheaf conditions can be swapped in and out for eachother

[Justus Springer]

local_predicate.lean only talks about sheaves of functions, no?

[Scott Morrison]

Yes, I don't think local_predicate.lean is what you want.

[Scott Morrison]

The sheaf conditions in topology/sheaves/sheaf_condition are all proved equivalent. (We have yet more sheaf conditions for sheaves on a site, and I think they are still disconnected from the earlier development of sheaves on a space, however.)

[Scott Morrison]

I suspect that what you want, @Justus Springer, is not actually there yet. This part of the library is pretty new!

[Scott Morrison]

Oh, sorry, I think I misspoke about local_predicate.lean. Maybe Johan meant you should use it along with something in sheafify to reduce to the case of dependently typed functions.

[Scott Morrison]

Fix some type family Z : X \to Type*, and assume your sheaf F is any subsheaf of the sheaf of sections of this family. Then your statement is obviously true. Now, we construct sheafification of a presheaf F as follows. Let Z be the stalks of F. The sheafification of F is the sheaf of sections of Z which are locally germs. This ... means that the statement is true for any sheaf, because it is the same as its sheafification?

(I have no idea if that argument is even true, let alone if it is easy to formalise given what we have... 90% of my knowledge of sheaves came from writing those files...)

[Scott Morrison]

Okay, forget that argument for a bit.

I don't think you need anything about unique_of_type_equalizer. You are just using that equalizer.\iota is a mono, in the equalizer diagram for the sheaf condition.

[Justus Springer]

Thanks for the input! I'm going to keep experimenting and maybe PR something soon.

[Scott Morrison]

import topology.sheaves.sheaf
import category_theory.limits.types

open Top
open topological_space
open opposite
open category_theory
open category_theory.limits

universes u

variables (X : Top.{u})
variables (F : sheaf (Type u) X)
variables {ι : Type u} (U : ι → opens X)

lemma ext {f g : F.presheaf.obj (op (supr U))}
(w : ∀ i, F.presheaf.map (opens.le_supr U i).op f = F.presheaf.map (opens.le_supr U i).op g ) :
f = g :=
begin
have := mono_of_is_limit_parallel_pair (F.sheaf_condition U),
have := (mono_iff_injective _).mp this,
apply this,
ext,
dsimp [presheaf.sheaf_condition_equalizer_products.res],
simp,
apply w,
end

[Justus Springer]

Scott Morrison said:

You are just using that equalizer.\iota is a mono

Right, this would also be an option, however this only gives me uniqueness of a gluing, but not existence I think.

[Scott Morrison]

Ah, I was answering directly "In particular I want to conclude that if two sections s t : F.obj (op V) agree locally on an open cover, they must already be equal."

[Scott Morrison]

(This is done in the spoiler block above.)

[Justus Springer]

True, for that it would suffice

[Justus Springer]

Scott Morrison said:

(This is done in the spoiler block above.)

Oh thanks a lot!

[Scott Morrison]

I better sleep. Have fun, looking forward to the PRs!

[Bhavik Mehta]

I think this formulation is given by the definition of the sheaf condition in category_theory/sites/sheaf

[Justus Springer]

Bhavik Mehta said:

I think this formulation is given by the definition of the sheaf condition in category_theory/sites/sheaf

I don't know much about sheaves on sites/topoi unfortunately, so this seems like even more categorical overhead to me...

[Justus Springer]

Can sheaves on spaces be easily subsumed by this more general framework?

[Kevin Buzzard]

Right -- given a top space you can make a site, and a sheaf on the space is the same thing as a sheaf on the site.

[Johan Commelin]

On paper...
In Lean, they are different beasts, and so you will need to work your way through an equivalence of categories :grinning:

[Bhavik Mehta]

Right - it's on my todo list to make the passage between the two smoother

[Scott Morrison]

@Justus Springer, thanks for that pair of PRs. They look really nice, and much better than what we have at the moment.

[Justus Springer]

Thanks a lot!
I'm now learning more about sites, so I might be able to help building the bridges between sheaves on spaces and sheaves on sites in the future.

[Justus Springer]

By the way, is #5927 still being developed @Bhavik Mehta ?

[Bhavik Mehta]

I think the changes there were mostly just about names and docs which I just haven't got around to fixing yet!