Commit 2026-06-22 16:23 8ade642d

View on Github →

feat(CategoryTheory/Sites): pushforward and pullback of presieves (#40527) We define analogues of Sieve.pushforward and Sieve.pullback for Presieves and show the Galois connection.

Estimated changes

Modified Mathlib/CategoryTheory/Sites/CoproductSheafCondition.lean

Modified Mathlib/CategoryTheory/Sites/Hypercover/Zero.lean

added def CategoryTheory.PreZeroHypercover.equivOfIso

added theorem CategoryTheory.PreZeroHypercover.mem_iff_of_iso

added theorem CategoryTheory.PreZeroHypercover.mem_of_iso

added theorem CategoryTheory.PreZeroHypercover.presieve₀_pushforward

added def CategoryTheory.PreZeroHypercover.pushforward

added def CategoryTheory.PreZeroHypercover.pushforwardIsoBind

added def CategoryTheory.Precoverage.ZeroHypercover.pushforward

Modified Mathlib/CategoryTheory/Sites/IsSheafFor.lean

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

added theorem CategoryTheory.Presieve.galoisConnection_pushforward_pullback

added theorem CategoryTheory.Presieve.le_pullback_pushforward

added theorem CategoryTheory.Presieve.monotone_pullback

added theorem CategoryTheory.Presieve.monotone_pushforward

added def CategoryTheory.Presieve.pullback

added theorem CategoryTheory.Presieve.pullback_comp

added theorem CategoryTheory.Presieve.pullback_id

added theorem CategoryTheory.Presieve.pullback_iff

added def CategoryTheory.Presieve.pushforward

added theorem CategoryTheory.Presieve.pushforward_apply_comp

added theorem CategoryTheory.Presieve.pushforward_comp

added theorem CategoryTheory.Presieve.pushforward_id

added theorem CategoryTheory.Presieve.pushforward_le_iff_le_pullback

added theorem CategoryTheory.Presieve.pushforward_ofArrows

added theorem CategoryTheory.Presieve.pushforward_pullback_le

added theorem CategoryTheory.Presieve.pushforward_singleton

added theorem CategoryTheory.Sieve.generate_pushforward

added theorem CategoryTheory.Sieve.pullback_arrows

added theorem CategoryTheory.Sieve.pushforward_arrows