Commit 2026-02-07 07:45 fbfd573c

View on Github →

feat(CategoryTheory/Sites): various API additions for #34917 (#34921)

Estimated changes

Modified Mathlib/CategoryTheory/Sites/Coverage.lean

added theorem CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange

added theorem CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange_of_small

Modified Mathlib/CategoryTheory/Sites/Grothendieck.lean

Modified Mathlib/CategoryTheory/Sites/Hypercover/Zero.lean

added theorem CategoryTheory.PreZeroHypercover.Hom.sieve₀_le_sieve₀

added theorem CategoryTheory.PreZeroHypercover.presieve₀_restrictIndex_le

added def CategoryTheory.PreZeroHypercover.restrictIndexHom

added theorem CategoryTheory.PreZeroHypercover.sieve₀_eq_of_iso

Modified Mathlib/CategoryTheory/Sites/MorphismProperty.lean

added theorem CategoryTheory.MorphismProperty.bot_mem_precoverage

Modified Mathlib/CategoryTheory/Sites/PrecoverageToGrothendieck.lean

added theorem CategoryTheory.PreZeroHypercover.isSheafFor_iff_of_iso

added theorem CategoryTheory.Precoverage.toGrothendieck_mono

added theorem CategoryTheory.Presieve.isSheafFor_ofArrows_comp_iff

added theorem CategoryTheory.Presieve.isSheafFor_singleton_iff_of_iso

Modified Mathlib/CategoryTheory/Sites/Pretopology.lean

added theorem CategoryTheory.Pretopology.toGrothendieck_mono

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

added theorem CategoryTheory.Presieve.ofArrows_of_unique

added theorem CategoryTheory.Sieve.generate_bot