Commit 2024-02-14 17:45 765353a8

View on Github →

feat(CategoryTheory/Sites): add a left version of sheafCongr (#10423)

Estimated changes

Modified Mathlib/CategoryTheory/Sites/Equivalence.lean

modified theorem CategoryTheory.Equivalence.coverPreserving

added theorem CategoryTheory.Equivalence.eq_inducedTopology_of_transports

modified def CategoryTheory.Equivalence.sheafCongr.counitIso

modified def CategoryTheory.Equivalence.sheafCongr.functor

modified def CategoryTheory.Equivalence.sheafCongr.inverse

modified def CategoryTheory.Equivalence.sheafCongr.unitIso

modified def CategoryTheory.Equivalence.sheafCongr

modified def CategoryTheory.Equivalence.transportIsoSheafToPresheaf

modified def CategoryTheory.Equivalence.transportSheafificationAdjunction

modified def CategoryTheory.smallSheafify