Commit 2025-08-30 20:46 c1faf313

refactor(CategoryTheory/Sites/Sieves): avoid HasPullbacks C in Presieve.pullbackArrows (#29085) We introduce a new typeclass Presieve.HasPullbacks R f which says that the pullbacks of the component maps of R along f exist. This is used instead of HasPullbacks C in Presieve.pullbackArrows. The motivation for this is to be able to use Presieve.pullbackArrows in situations where either not all pullbacks exist or it is not yet known that all pullbacks exist. An example is the category of schemes, where existence of pullbacks along open immersions is shown as a step towards the proof of existence of all pullbacks. The already existing Presieve.hasPullbacks is renamed to Presieve.HasPairwisePullbacks to make the distinction clear. This refactor also opens up the possibility to weaken the HasPullbacks C assumption from Pretopology.