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
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
