Commit 2023-05-10 21:21 ec7fb745

View on Github →

feat: port CategoryTheory.Sites.CoverPreserving (#3884) Straightforward.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Sites/CoverPreserving.lean

added theorem CategoryTheory.CompatiblePreserving.apply_map

added structure CategoryTheory.CompatiblePreserving

added theorem CategoryTheory.CoverPreserving.comp

added structure CategoryTheory.CoverPreserving

added theorem CategoryTheory.Presieve.FamilyOfElements.Compatible.functorPushforward

added def CategoryTheory.Sites.pullback

added theorem CategoryTheory.compatiblePreservingOfDownwardsClosed

added theorem CategoryTheory.compatiblePreservingOfFlat

added theorem CategoryTheory.idCoverPreserving

added def CategoryTheory.pullbackSheaf

added theorem CategoryTheory.pullback_isSheaf_of_coverPreserving