Commit 2026-07-09 10:58 e469acc1

View on Github →

feat(CategoryTheory/Sites/Over): add Presieve.overEquiv (#41510) This PR adds Presieve.overEquiv, the presieve version of the existing Sieve.overEquiv. I also upgraded these equivs to order isomorphisms, and fixed some defeq abuse at the same time. Partial help from Claude on a couple of the proofs, all code was ultimately written and golfed by me.

Estimated changes

Modified Mathlib/AlgebraicGeometry/Sites/Small.lean

Modified Mathlib/CategoryTheory/Sites/Descent/DescentData.lean

Modified Mathlib/CategoryTheory/Sites/Descent/Precoverage.lean

Modified Mathlib/CategoryTheory/Sites/Over.lean

added theorem CategoryTheory.Presieve.functorPullback_map_overForget

modified theorem CategoryTheory.Presieve.map_functorPullback_overForget

added def CategoryTheory.Presieve.overEquiv

added theorem CategoryTheory.Sieve.functorPullback_functorPushforward_overForget

added theorem CategoryTheory.Sieve.functorPushforward_functorPullback_overForget

added theorem CategoryTheory.Sieve.functorPushforward_overForget_arrows

modified def CategoryTheory.Sieve.overEquiv

deleted theorem CategoryTheory.Sieve.overEquiv_bot

deleted theorem CategoryTheory.Sieve.overEquiv_le_overEquiv_iff

deleted theorem CategoryTheory.Sieve.overEquiv_symm_bot

deleted theorem CategoryTheory.Sieve.overEquiv_symm_top

deleted theorem CategoryTheory.Sieve.overEquiv_top

Modified Mathlib/CategoryTheory/Sites/Point/Over.lean

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

added theorem CategoryTheory.Presieve.map_le_functorPushforward

added theorem CategoryTheory.Sieve.arrows_mono

modified theorem CategoryTheory.Sieve.generate_mono