Commit 2025-10-02 13:49 ae4763b1
View on Github →refactor(AlgebraicGeometry/Sites): redefine pretopologies via precoverages (#29894)
We redefine the pretopology defined by a morphism property via Precoverage and make it independent of Scheme.Cover. This changes the definition of AlgebraicGeometry.Scheme.pretopology, because covering presieves are now allowed to be large. This does not matter, because the generated Grothendieck topology remains the same.
This allows us to redefine Scheme.Cover to be a ZeroHypercover with respect to this new precoverage, which will be done in the next PR.
Estimated changes
added theorem AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving.exists_preimage_snd_triplet_of_prop
deleted theorem AlgebraicGeometry.Scheme.jointlySurjectiveTopology_eq_toGrothendieck_jointlySurjectivePretopology