Commit 2024-05-30 06:23 a5bd5640
View on Github →feat(CategoryTheory/Sites): more properties of locally surjective morphisms of presheaves (#13318)
IsLocallySurjective is made a type-class, and basic properties (similar to properties of injective/surjective maps) are obtained for locally injective/surjective morphisms of presheaves on a category equipped with a Grothendieck topology.
Estimated changes
added theorem CategoryTheory.Presheaf.isLocallyInjective_of_isLocallyInjective_of_isLocallySurjective
added theorem CategoryTheory.Presheaf.isLocallyInjective_of_isLocallyInjective_of_isLocallySurjective_fac
added theorem CategoryTheory.Presheaf.isLocallySurjective_of_isLocallySurjective_of_isLocallyInjective