Commit 2026-08-12 15:35 e2d86c68

View on Github →

feat(CategoryTheory/Sites): criteria for IsSheafFor for a presieve generated by a single morphism (#42568)

Estimated changes

Modified Mathlib/CategoryTheory/Sites/IsSheafFor.lean

added theorem CategoryTheory.Presieve.IsSeparatedFor.of_singleton_comp

added theorem CategoryTheory.Presieve.IsSheafFor.of_singleton

added theorem CategoryTheory.Presieve.IsSheafFor.of_singleton_comp

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

added theorem CategoryTheory.Presieve.singleton_le_iff