mathlib documentation


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.


The isomorphism between P⁺ ⋙ F and (P ⋙ F)⁺, functorially in F.