Commit 2021-04-30 10:14 4a94b28f

feat(category_theory/sites): Sheaves of structures (#5927) 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