Commit 2025-07-08 19:42 d045ff1c

feat(CategoryTheory/Sites): 0-hypercovers (#26888) We define the type of 0-hypercovers with respect to a coverage J on a category C as indexed families of morphisms such that the associated presieve is a covering sieve. The purpose of this definition is to unify workable notions of covers in categories of geometric objects, such as schemes or adic spaces. In particular, in a follow-up PR the notion AlgebraicGeometry.Scheme.Cover shall be an abbrev for a zero-hypercover for the associated coverage. We define this with respect to a coverage and not to a Grothendieck topology, because this yields more control over the components of the cover: For example, if J is the coverage given by jointly surjective families of open immersions of schemes, a ZeroHypercover J S is precisely an indexed, jointly surjective family of open immersions, but not only one that contains such a family.