Commit 2022-02-01 20:41 343cbd98

feat(sites/sheaf): simple sheaf condition in terms of limit (#11692)

• Given a presheaf on a site, construct a simple cone for each sieve. The sheaf condition is equivalent to all these cones being limit cones for all covering sieves of the Grothendieck topology. This is made possible by a series of work that mostly removed universe restrictions on limits.
• Given a sieve over X : C, the diagram of its associated cone is a functor from the full subcategory of the over category C/X consisting of the arrows in the sieve, constructed from the canonical cocone over forget : over X ⥤ C with cone point X, which is only now added to mathlib. This cone is simpler than the multifork cone in is_sheaf_iff_multifork. The underlying type of this full subcategory is equivalent to grothendieck_topology.cover.arrow.
• This limit sheaf condition might be more convenient to use to do sheafification, which has been done by @adamtopaz using the multifork cone before universes are sufficiently generalized for limits, though I haven't thought about it in detail. It may not be worth refactoring sheafification in terms of this sheaf condition, but we might consider using this if we ever want to do sheafification for more general (e.g. non-concrete) value categories. #11706 is another application. This is based on a Zulip discussion with @adamtopaz.