mathlib3 documentation

category_theory.sites.compatible_plus

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file, we prove that the plus functor is compatible with functors which preserve the correct limits and colimits.

See category_theory/sites/compatible_sheafification for the compatibility of sheafification, which follows easily from the content in this file.