Commit 2026-02-07 07:29 cce210ef

chore(CategoryTheory/Sites): rename Sheaf.isSheafFor_trans to Presieve.isSheafFor_trans and move to earlier file (#34924) We move the lemmas Sheaf.isSheafFor_trans and Sheaf.isSheafFor_bind from Mathlib/CategoryTheory/Sites/Canonical.lean to Mathlib/CategoryTheory/Sites/IsSheafFor.lean, because they are more generally useful. We also change the names to match their content:

• Sheaf.isSheafFor_trans -> Presieve.isSheafFor_trans
• Sheaf.isSheafFor_bind -> Presieve.isSheafFor_bind Finally, we generalize the universe of the codomain of the presheaf in both lemmas.