Commit 2025-09-19 18:56 b7a28221

View on Github →

chore(CategoryTheory/Sites): rename .ofGrothendieck to GrothendieckTopology.to{Coverage, Pretopology} (#29815) We rename {Coverage, Pretopology}.ofGrothendieck to GrothendieckTopology.to{Coverage, Pretopology}. This is friendlier to dot notation (anonymous dot notation needs extra parentheses and is harder to decipher). We also make the C argument in both the toGrothendieck as well as the to{Coverage, Pretopology} functions implicit.

Estimated changes

Modified Mathlib/AlgebraicGeometry/Sites/Small.lean

Modified Mathlib/CategoryTheory/Sites/Coherent/Basic.lean

Modified Mathlib/CategoryTheory/Sites/Coherent/Comparison.lean

Modified Mathlib/CategoryTheory/Sites/Coverage.lean

modified def CategoryTheory.Coverage.gi

deleted def CategoryTheory.Coverage.ofGrothendieck

deleted theorem CategoryTheory.Coverage.ofGrothendieck_iff

modified theorem CategoryTheory.Coverage.toGrothendieck_eq_sInf

added theorem CategoryTheory.GrothendieckTopology.mem_toCoverage_iff

added def CategoryTheory.GrothendieckTopology.toCoverage

Modified Mathlib/CategoryTheory/Sites/Pretopology.lean

added theorem CategoryTheory.GrothendieckTopology.mem_toPretopology

added def CategoryTheory.GrothendieckTopology.toPretopology

modified def CategoryTheory.Pretopology.gi

deleted theorem CategoryTheory.Pretopology.mem_ofGrothendieck

deleted def CategoryTheory.Pretopology.ofGrothendieck

modified theorem CategoryTheory.Pretopology.toGrothendieck_bot

Modified Mathlib/CategoryTheory/Sites/Sheaf.lean

Modified Mathlib/CategoryTheory/Sites/SheafOfTypes.lean

Modified Mathlib/CategoryTheory/Sites/Spaces.lean

deleted theorem Opens.pretopology_ofGrothendieck

added theorem Opens.toPretopology_grothendieckTopology