[Merged by Bors] - feat(CategoryTheory/Sites): 1-hypercovers

[joelriou]

This PR defines a notion of 1-hypercovers in a category C equipped with a Grothendieck topology J. A covering of an object S : C consists of a family of maps f i : X i ⟶ S which generates a covering sieve. In the favourable case where the fibre products of X i and X j over S exist, the data of a 1-hypercover consists of the data of objects Y j which cover these fibre products. We formalize this notion without assuming that these fibre products actually exists. If F is a sheaf and E is a 1-hypercover of S, we show that F.val.obj (op S) is a multiequalizer of suitable maps F.val.obj (op (X i)) ⟶ F.val.obj (op (Y j)).

---

[adamtopaz]

I have no real objections about this, but I do wonder whether you considered going for arbitrary hypercovers (e.g. defining them using simplicial coskeleta). Do you have a particular use in mind for 1-hypercovers?

[adamtopaz]

thanks!

bors r+

[joelriou]

I have no real objections about this, but I do wonder whether you considered going for arbitrary hypercovers (e.g. defining them using simplicial coskeleta). Do you have a particular use in mind for 1-hypercovers?

I do not plan to PR an adhoc definition of 2-hypercovers! For general hypercovers, we could give a definition, but we would not be able to prove much about it until we make very significant progress on the formalization of the homotopy theory of simplicial sets.

Among the possible applications, 1-hypercovers are useful in order to describe elements in the sheafification of a presheaf. I have introduced a universe parameter w for the index types of 1-hypercovers, and I plan to use it in order to show that if X : Scheme.{u}, then even though the category of locally finite presentation etale schemes over X is a large.{u} category (not even essentially small), which should require considering sheaves with values in Type (u+1), any scheme over X is 1-hypercovered by objects in a suitable small category of affine schemes. Then, by using 1-hypercovers, the category of etale sheaves with values in Type u should be equivalent to a category of sheaves of Type u over a SmallCategory.{u}: then, we could deduce HasSheafify instance for categories of sheaves in algebraic geometry without a universe bump. (In a more remote future, etale cohomology groups could be defined in Type u.) Basically, I plan to generaliwe/refactor Sites.DenseSubsite with sharper universe bounds.

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style