[Merged by Bors] - feat(CategoryTheory): local epimorphisms wrt. an object property

[chrisflav]

Let P be an object property on a category C. We say that f : X ⟶ Y is a local epimorphism wrt. P if f cancels on the left for morphisms with codomain in P.

The motivating example is C the category of presheafs on some category with Grothendieck topology J and P the
property of being a sheaf for J. Then being a local epimorphism wrt. P is being an epimorphism after sheafification.

---

[github-actions]

PR summary bad1f8058c

Import changes exceeding 2%

%	File
+2.41%	Mathlib.CategoryTheory.EssentialImage

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.EssentialImage	291	298	+7 (+2.41%)

Import changes for all files

Files	Import difference
57 files Mathlib.AlgebraicTopology.DoldKan.Compatibility Mathlib.CategoryTheory.Bicategory.End Mathlib.CategoryTheory.Bicategory.EqToHom Mathlib.CategoryTheory.Bicategory.Functor.Prelax Mathlib.CategoryTheory.Bicategory.LocallyDiscrete Mathlib.CategoryTheory.Bicategory.Opposites Mathlib.CategoryTheory.Bicategory.Strict.Basic Mathlib.CategoryTheory.CatCommSq Mathlib.CategoryTheory.Category.ULift Mathlib.CategoryTheory.CommSq Mathlib.CategoryTheory.Comma.Arrow Mathlib.CategoryTheory.Comma.Basic Mathlib.CategoryTheory.Comma.CatCommSq Mathlib.CategoryTheory.DinatTrans Mathlib.CategoryTheory.Discrete.Basic Mathlib.CategoryTheory.Discrete.SumsProducts Mathlib.CategoryTheory.EqToHom Mathlib.CategoryTheory.Equivalence Mathlib.CategoryTheory.EssentialImage Mathlib.CategoryTheory.FiberedCategory.BasedCategory Mathlib.CategoryTheory.FiberedCategory.Cartesian Mathlib.CategoryTheory.FiberedCategory.Cocartesian Mathlib.CategoryTheory.FiberedCategory.Fiber Mathlib.CategoryTheory.FiberedCategory.Fibered Mathlib.CategoryTheory.FiberedCategory.HasFibers Mathlib.CategoryTheory.FiberedCategory.HomLift Mathlib.CategoryTheory.Functor.Const Mathlib.CategoryTheory.Functor.CurryingThree Mathlib.CategoryTheory.Functor.Currying Mathlib.CategoryTheory.Functor.TwoSquare Mathlib.CategoryTheory.Join.Basic Mathlib.CategoryTheory.Join.Opposites Mathlib.CategoryTheory.Join.Sum Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform Mathlib.CategoryTheory.Monoidal.Action.Basic Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor Mathlib.CategoryTheory.Monoidal.Category Mathlib.CategoryTheory.Monoidal.CoherenceLemmas Mathlib.CategoryTheory.Opposites Mathlib.CategoryTheory.PEmpty Mathlib.CategoryTheory.PUnit Mathlib.CategoryTheory.Pi.Basic Mathlib.CategoryTheory.Products.Associator Mathlib.CategoryTheory.Products.Basic Mathlib.CategoryTheory.Products.Bifunctor Mathlib.CategoryTheory.Products.Unitor Mathlib.CategoryTheory.Square Mathlib.CategoryTheory.Sums.Associator Mathlib.CategoryTheory.Sums.Basic Mathlib.CategoryTheory.Sums.Products Mathlib.Tactic.CategoryTheory.Monoidal.Basic Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes Mathlib.Tactic.CategoryTheory.Monoidal.Normalize Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence Mathlib.Tactic.CategoryTheory.MonoidalComp Mathlib.Tactic.Widget.StringDiagram	7
Mathlib.CategoryTheory.MorphismProperty.LocalEpi (new file)	675

---

Declarations diff

+ instance (W : MorphismProperty C) : P.localEpi.HasOfPrecompProperty W
+ instance : P.localEpi.HasOfPostcompProperty P.isLocal
+ instance : P.localEpi.IsMultiplicative
+ instance : P.localEpi.IsStableUnderCobaseChange := by
+ instance : P.localEpi.Respects P.isLocal
+ instance : P.localEpi.RespectsIso
+ isLocal_le_localEpi
+ isoClosure_eq_essImage
+ localEpi
+ localEpi.of_epi
+ localEpi_antitone
+ localEpi_essImage
+ localEpi_isoClosure
+ localEpi_mem_range_eq_inverseImage_epimorphisms
+ localEpi_mem_range_iff_epi
+ localEpi_top_apply_iff
+ localEpi_top_eq_epimorphisms

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[joelriou]

For "local epimorphisms", we already have Presheaf.IsLocallySurjective and under suitable assumptions, this is the same as being an epimorphism after sheafification, so that I am wondering whether this new API is really needed?

[chrisflav]

Presheaf.IsLocallySurjective only works for concrete-category-valued presheafs, which is a bit unsatisfactory. The definition I give here is the one from SGA, where they calls these morphisms "morphisme couvrant" (see SGA4, II, Définition 5.2). The terminology is taken from Kashiwara-Shapira, see Definition 16.1.3, although they give a definition in terms of sieves. (I did not put these references in the file, because I thought they should be in the PR about the special case of presheaves).
I would like to develop (part of) the content of SGA4, II, Section 5, we will for example need 5.3 for Robin's and my proposed definition of hypercovers.

I was planning to make the link of this definition to Presheaf.IsLocallySurjective in the PR defining "local epimorphisms of presheaves" (they are at least equivalent if the site has sheafification).

[robin-carlier]

Since the terminology is from Kashiwara-Schapira, maybe that can be mentioned in the doc-module? I think this reference is already in the references.bib

[robin-carlier]

Thanks!

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by robin-carlier.

[joelriou]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-CI job
• ci (staging) / Post-Build Step
• ci (staging) / Build
• ci (staging) / Lint style