[Merged by Bors] - refactor(CategoryTheory/Sites): continuous functors

[joelriou]

This PR introduces the typeclass Functor.IsContinuous which says that the precomposition with a functor preserves the sheaf condition for Grothendieck topologies. It slightly refactors the previous main theorem about CoverPreserving and CompatiblePreserving functors: it now states that such functors are continuous. The pushforward functor for a continuous functor is defined under the Functor.IsContinuous assumption rather than the combination of both CoverPreserving and CompatiblePreserving. The property CoverLifting is renamed IsCocontinuous and it is made a class. The property IsCoverDense is also made a class.

---

The current results are great, but I feel the terminology was very confusing: for example, the functor between categories of sheaves induced by a continuous functor was named pullback, even though it should be considered as a pushforward functor (for example, they induce the covariant functoriality of sheaves for sites or topological spaces). I have made some other similar renames.

[dagurtomas]

I think that if we're introducing the name Continuous for functors, we should go all the way and add Cocontinuous as well. The docstring of CoverLifting.lean says:

"This concept is also known as cocontinuous functors or
cover-reflecting functors, but we have chosen this name following [MM92] in order to avoid
potential naming collision or confusion with the general definition of cocontinuous functors
between categories as functors preserving small colimits."

This applies to the name continuous functor as well, but since we don't use that terminology for (co)limit preserving functors in mathlib, I think we can just remove that paragraph and claim both names for the sheaf-theoretic notion (and maybe add a warning that they don't mean "(co)limit-preserving".

[dagurtomas]

Could you also change line 44 in CoverPreserving.lean to * https://stacks.math.columbia.edu/tag/00WU to cite the whole section in Stacks and not just one particular lemma?

[joelriou]

Thanks for the suggestions @dagurtomas! Now, there is Functor.IsContinuous and Functor.IsCocontinuous.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Build failed:

• Build

[joelriou]

retrying

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style
• Check all files imported