mathlib3 documentation

category_theory.sites.compatible_sheafification

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

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

The isomorphism between the sheafification of P composed with F and the sheafification of P ⋙ F.

Use the lemmas whisker_right_to_sheafify_sheafify_comp_iso_hom, to_sheafify_comp_sheafify_comp_iso_inv and sheafify_comp_iso_inv_eq_sheafify_lift to reduce the components of this isomorphisms to a state that can be handled using the universal property of sheafification.

Equations

The isomorphism between the sheafification of P composed with F and the sheafification of P ⋙ F, functorially in F.

Equations

The isomorphism between the sheafification of P composed with F and the sheafification of P ⋙ F, functorially in P.

Equations