[Merged by Bors] - feat(category_theory/sites): Sheaves of structures

[b-mehta]

Define sheaves on a site taking values in an arbitrary category.

Joint with @kbuzzard. cc: @jcommelin, this is a step towards condensed abelian groups.

I don't love the names here, design advice (particularly from those who'll use this) more than appreciated.

The main points are:

• An A-valued presheaf P : C^op => A is defined to be a sheaf (for the topology J) iff for every X : A, the type-valued presheaves of sets given by sending U : C^op to Hom_{A}(X, P U) are all sheaves of sets.
• When A = Type, this recovers the basic definition of sheaves of sets.
• An alternate definition when C is small, has pullbacks and A has products is given by an equalizer condition is_sheaf'.
• This is equivalent to the earlier definition.
• When A = Type, this is definitionally equal to the equalizer condition for presieves in sheaf_of_types.lean
• When A has limits and there is a functor s : A => Type which is faithful, reflects isomorphisms and preserves limits, then P : C^op => A is a sheaf iff the underlying presheaf of types P >>> s : C^op => Type is a sheaf. (cf https://stacks.math.columbia.edu/tag/0073, which is a weaker version of this statement (it's only over spaces, not sites) and https://stacks.math.columbia.edu/tag/00YR (a), which additionally assumes filtered colimits).

A couple of questions for reviewers:

• We've now got a ton of equivalent ways of showing something's a sheaf, and it's not the easiest to navigate between them. Is there a nice way around this? I think it's still valuable to have all the ways, since each can be helpful in different contexts but it makes the API a bit opaque. There's also a bit of inconsistency - there's a definition yoneda_sheaf_condition which is the same as is_sheaf_for but the equalizer conditions at the bottom of sheaf_of_types aren't named, they're just some nonempty (is_limit (fork.of_ι _ (w P R))) even though they're also equivalent.
• The name presieve.is_sheaf is stupid, I think I was just lazy with namespaces. I think presieve.family_of_elements and presieve.is_sheaf_for are still sensible, since they are relative to a presieve, but is_sheaf doesn't have any reference to presieves in its type.
• The equalizer condition of sheaves of types is definitionally the same as the equalizer condition for sheaves of structures, so is there any point in having the former version in the library - the latter is just more general (the same doesn't apply to the actual def of sheaves of structures since that's defined in terms of sheaves of types). The main downside I can see is that it might make the proofs of equalizer_sheaf_condition a bit trickier, but that's about it

[jcommelin]

Thank you so much for working on this!

A couple of questions for reviewers:

• We've now got a ton of equivalent ways of showing something's a sheaf, and it's not the easiest to navigate between them. Is there a nice way around this? I think it's still valuable to have all the ways, since each can be helpful in different contexts but it makes the API a bit opaque. There's also a bit of inconsistency - there's a definition yoneda_sheaf_condition which is the same as is_sheaf_for but the equalizer conditions at the bottom of sheaf_of_types aren't named, they're just some nonempty (is_limit (fork.of_ι _ (w P R))) even though they're also equivalent.

I think we will probably want to keep all the versions, at least for now. And gradually flesh out the API.

• The name presieve.is_sheaf is stupid, I think I was just lazy with namespaces. I think presieve.family_of_elements and presieve.is_sheaf_for are still sensible, since they are relative to a presieve, but is_sheaf doesn't have any reference to presieves in its type.

This sounds like something that can be fixed.

• The equalizer condition of sheaves of types is definitionally the same as the equalizer condition for sheaves of structures, so is there any point in having the former version in the library - the latter is just more general (the same doesn't apply to the actual def of sheaves of structures since that's defined in terms of sheaves of types). The main downside I can see is that it might make the proofs of equalizer_sheaf_condition a bit trickier, but that's about it

Let's keep it for now. If we find that it's rarely useful, and leads to duplication, then we can remove it later. I think the proofs in this area are already hard enough... so anything that makes it easier is welcome (-;

[jcommelin]

• An A-valued presheaf P : C^op => A is defined to be a sheaf (for the topology J) iff for every X : A, the type-valued presheaves of sets given by sending U : C^op to Hom_{A}(X, P U) are all sheaves of sets.
• When A = Type, this recovers the basic definition of sheaves of sets.
• An alternate definition when C is small, has pullbacks and A has products is given by an equalizer condition is_sheaf'.
• This is equivalent to the earlier definition.
• When A = Type, this is definitionally equal to the equalizer condition for presieves in sheaf_of_types.lean
• When A has limits and there is a functor s : A => Type which is faithful, reflects isomorphisms and preserves limits, then P : C^op => A is a sheaf iff the underlying presheaf of types P >>> s : C^op => Type is a sheaf. (cf https://stacks.math.columbia.edu/tag/0073, which is a weaker version of this statement (it's only over spaces, not sites) and https://stacks.math.columbia.edu/tag/00YR (a), which additionally assumes filtered colimits).

These comments are useful! Please copy them to the module docstring.

[jcommelin]

The code looks good. But some names might need to be tweaked a bit... like sheaf_cond3.

[kbuzzard]

This looks excellent. My comments are all superficial. This will enable us to do sheaves of rings in a non-ad-hoc way.

[jcommelin]

LGTM. But I wonder if @justus-springer has some comments, since he's been working with sheaves in mathlib lately.

[justus-springer]

Just a question about the sheaf condition. Otherwise no further comments other than that I really like this!

[jcommelin]

Thanks 🎉

bors merge

[bors]

Build failed (retrying...):

• Lint mathlib

[eric-wieser]

bors r-

The linter fails even before bors ran.

[bors]

Canceled.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests