Commit 2025-08-31 17:16 7717796b

refactor(CategoryTheory/Sites): make Coverage and Pretopology extend Precoverage (#29065) We add a new structure CategoryTheory.Precoverage which only contains a family of covering presieves with no stability conditions. The existing CategoryTheory.Pretopology and CategoryTheory.Coverage are changed to extend CategoryTheory.Precoverage. The main motivation for this refactor is to reduce the assumptions needed for using Coverage.ZeroHypercover (which is now Precoverage.ZeroHypercover): If P is a morphism property in a category C, the precoverage given by families satisfying P is only a coverage if C has pullbacks and P is stable under base change. In applications, this can either be not true or not known yet (For example the category of schemes has pullbacks and the relevant properties are stable under base change, but the cover API is used to deduce these results so we can't assume them a priori.) The second motivation is to unify the common parts of Coverage and Pretopology. The existing stability conditions Coverage.IsStableUnderComposition and Coverage.IsStableUnderBaseChange are defined for Precoverage instead. Main (breaking) API change: Coverage.covering is now Precoverage.coverings.