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.
Instances For
The isomorphism between the sheafification of P
composed with F
and
the sheafification of P ⋙ F
, functorially in F
.
Instances For
The isomorphism between the sheafification of P
composed with F
and
the sheafification of P ⋙ F
, functorially in P
.