Commit 2025-09-18 18:34 3dfd54e3

feat(CategoryTheory/Sites): generating precoverage for localized topology (#29737) We show that the Grothendieck topology on Over X, obtained from localizing the topology generated by the precoverage K, is generated by the preimage of K. The newly introduced Precoverage.toGrothendieck / GrothendieckTopology.toPrecoverage don't match the existing naming scheme for Pretopology and Coverage. The reason is that the name GrothendieckTopology.toPrecoverage is friendlier to dot notation (anonymous dot notation would need additional parenthesis). We will change the names for Pretopology and Coverage in a separate PR.