Commit 2026-01-23 18:54 81e378d0

View on Github →

feat(CategoryTheory/Sites): add Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition (#34272) We also add various API lemmas for Precoverages and Sieves. In particular, the simp lemma Sieve.arrows_top, which changes some simp normal forms. From Proetale.

Estimated changes

Modified Mathlib/CategoryTheory/Sites/Canonical.lean

Modified Mathlib/CategoryTheory/Sites/IsSheafFor.lean

added theorem CategoryTheory.Presieve.isSheafFor_top

deleted theorem CategoryTheory.Presieve.isSheafFor_top_sieve

Modified Mathlib/CategoryTheory/Sites/MorphismProperty.lean

added theorem CategoryTheory.MorphismProperty.comap_precoverage

Modified Mathlib/CategoryTheory/Sites/Precoverage.lean

added theorem CategoryTheory.Precoverage.comap_comp

Modified Mathlib/CategoryTheory/Sites/PrecoverageToGrothendieck.lean

added theorem CategoryTheory.Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition

added theorem CategoryTheory.Precoverage.toGrothendieck_toPretopology_eq_toGrothendieck

Modified Mathlib/CategoryTheory/Sites/SheafOfTypes.lean

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

added theorem CategoryTheory.Presieve.ofArrows_le_iff

added theorem CategoryTheory.Sieve.arrows_eq_top_iff

added theorem CategoryTheory.Sieve.arrows_top

added theorem CategoryTheory.Sieve.functorPushforward_le_iff_le_functorPullback

added theorem CategoryTheory.Sieve.functorPushforward_pullback_le

added theorem CategoryTheory.top_apply

Modified Mathlib/Topology/Sheaves/PUnit.lean