Commit 2026-03-03 14:05 a98da297

View on Github →

chore(Mathlib/CategoryTheory/Sites): more API for Presieve.map (#35949) This PR was automatically created from PR #35948 by @chrisflav via a review comment by @chrisflav.

Estimated changes

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

added theorem CategoryTheory.Presieve.functorPullback_arrows

added theorem CategoryTheory.Presieve.functorPullback_map_functorPullback

added theorem CategoryTheory.Presieve.functorPullback_monotone

added theorem CategoryTheory.Presieve.functorPushforward_monotone

added theorem CategoryTheory.Presieve.galoisConnection_map_functorPullback

added theorem CategoryTheory.Presieve.le_functorPullback_map

added theorem CategoryTheory.Presieve.map_functorPullback_map

added theorem CategoryTheory.Presieve.map_iff

added theorem CategoryTheory.Presieve.map_le_iff_le_functorPullback

modified theorem CategoryTheory.Presieve.map_monotone

added theorem CategoryTheory.Sieve.functorPullback_functorPushforward_eq