Commit 2024-07-31 16:34 feb80cfa

View on Github →

feat(CategoryTheory): add some instances for essentially small sites (#13486) This PR proves that the properties PreservesSheafification and WEqualsLocallyBijective hold for an essentially small site if they hold for an equivalent small site.

Estimated changes

Modified Mathlib/CategoryTheory/Sites/Coherent/Equivalence.lean

Modified Mathlib/CategoryTheory/Sites/DenseSubsite.lean

added theorem CategoryTheory.Functor.functorPushforward_mem_iff

Modified Mathlib/CategoryTheory/Sites/Equivalence.lean

deleted theorem CategoryTheory.Equivalence.coverPreserving

added theorem CategoryTheory.Equivalence.eq_inducedTopology_of_isDenseSubsite

deleted theorem CategoryTheory.Equivalence.eq_inducedTopology_of_transports

added theorem CategoryTheory.GrothendieckTopology.PreservesSheafification.transport

Modified Mathlib/CategoryTheory/Sites/InducedTopology.lean

added theorem CategoryTheory.Functor.mem_inducedTopology_sieves_iff

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

added theorem CategoryTheory.Sieve.functorPushforward_equivalence_eq_pullback

added theorem CategoryTheory.Sieve.pullback_functorPushforward_equivalence_eq