Commit 2024-06-05 03:13 35b146f4

feat(CategoryTheory/Sites): characterization of sheaves using 1-hypercovers (#13004) In this PR, given a Grothendieck topology J on a category C, we define a type J.OneHypercoverFamily of families of 1-hypercovers. When H : J.OneHypercoverFamily, we define a predicate H.IsGenerating which means that any covering sieve contains the sieve generated by the underlying covering of one of the 1-hypercovers in the family. If this holds, we show in OneHypercoverFamily.isSheaf_iff that a presheaf P : Cᵒᵖ ⥤ A is a sheaf iff for any 1-hypercover E in the family, the multifork E.multifork P is limit.