Commit 2025-12-16 10:54 35793aab

feat(CategoryTheory/Sites): add the Grothendieck topology generated by a precoverage (#32652) Add the file PrecoverageToGrothendieck.lean, in which the Grothendieck topology generated by a precoverage is defined as Precoverage.toGrothendieck. This replace the previous Precoverage.toGrothendieck, which was defined only in the case of a precoverage having pullbacks and being stable under base change. The equivalence between the two constructions is Precoverage.toGrothendieck_toCoverage. Prove Precoverage.isSheaf_toGrothendieck_iff: given a precoverage J, a type-valued presheaf is a sheaf for J.toGrothendieck if and only if it is a sheaf for all the pullback sieves of the presieves in J. The proof is based on the previous proof of isSheaf_coverage, which is now a consequence of Precoverage.isSheaf_toGrothendieck_iff.