Commit 2023-06-11 13:19 57f3c44f

View on Github →

feat: port CategoryTheory.Sites.Surjective (#4969)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Sites/Surjective.lean

added theorem CategoryTheory.IsLocallySurjective.comp

added def CategoryTheory.IsLocallySurjective

added def CategoryTheory.imageSieve

added theorem CategoryTheory.imageSieve_app

added theorem CategoryTheory.imageSieve_eq_sieveOfSection

added theorem CategoryTheory.imageSieve_whisker_forget

added theorem CategoryTheory.isLocallySurjective_iff_imagePresheaf_sheafify_eq_top'

added theorem CategoryTheory.isLocallySurjective_iff_imagePresheaf_sheafify_eq_top

added theorem CategoryTheory.isLocallySurjective_iff_isIso

added theorem CategoryTheory.isLocallySurjective_iff_whisker_forget

added theorem CategoryTheory.isLocallySurjective_of_iso

added theorem CategoryTheory.isLocallySurjective_of_surjective

added theorem CategoryTheory.toSheafify_isLocallySurjective