Commit 2024-02-27 06:22 3c1a8148

View on Github →

feat(CategoryTheory/Sites): coherent and regular topologies respect equivalences of categories (#10013) This PR transports the coherent and regular topologies along equivalences of categories, and provides API for checking the sheaf condition on one of the equivalent defining sites.

Estimated changes

Modified Mathlib.lean

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

added theorem CategoryTheory.Equivalence.precoherent

added theorem CategoryTheory.Equivalence.precoherent_eq

added theorem CategoryTheory.Equivalence.precoherent_isSheaf_iff

added theorem CategoryTheory.Equivalence.precoherent_isSheaf_iff_of_essentiallySmall

added theorem CategoryTheory.Equivalence.preregular

added theorem CategoryTheory.Equivalence.preregular_eq

added theorem CategoryTheory.Equivalence.preregular_isSheaf_iff

added theorem CategoryTheory.Equivalence.preregular_isSheaf_iff_of_essentiallySmall

added def CategoryTheory.Equivalence.sheafCongrPrecoherent

added def CategoryTheory.Equivalence.sheafCongrPreregular