Commit 2025-12-26 18:30 5f557c4f

View on Github →

feat(CategoryTheory/Sites): more API for IsSheafFor (#33287) Some more API is added for (pre)sieves and we obtain a few results about how IsSheafFor behaves for presheaves on Over categories.

Estimated changes

Modified Mathlib/CategoryTheory/Sites/IsSheafFor.lean

added def CategoryTheory.Presieve.Arrows.toCompatible

added theorem CategoryTheory.Presieve.isSheafFor_iff_of_iso

added theorem CategoryTheory.Presieve.isSheafFor_ofArrows_iff_bijective_toCompabible

added theorem CategoryTheory.Presieve.isSheafFor_over_map_op_comp_iff

added theorem CategoryTheory.Presieve.isSheafFor_over_map_op_comp_ofArrows_iff

added theorem CategoryTheory.Presieve.isSheafFor_pullback_iff

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

added theorem CategoryTheory.Presieve.ofArrows_category

added theorem CategoryTheory.Sieve.exists_eq_ofArrows

added theorem CategoryTheory.Sieve.ofArrows_category'

added theorem CategoryTheory.Sieve.ofArrows_category

added theorem CategoryTheory.Sieve.pullback_ofArrows_of_iso