Commit 2024-07-24 04:05 dea5c169

View on Github →

feat(CategoryTheory/Sites): Sieves under equivalences. (#15063)

Estimated changes

Modified Mathlib/CategoryTheory/Sites/Equivalence.lean

Modified Mathlib/CategoryTheory/Sites/Grothendieck.lean

added theorem CategoryTheory.GrothendieckTopology.pullback_mem_iff_of_isIso

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

added theorem CategoryTheory.Sieve.comp_mem_iff

added theorem CategoryTheory.Sieve.functorPushforward_functor

added theorem CategoryTheory.Sieve.functorPushforward_inverse

added theorem CategoryTheory.Sieve.mem_functorPushforward_functor

added theorem CategoryTheory.Sieve.mem_functorPushforward_inverse