English
There exists a canonical natural isomorphism between the sheafification of P composed with F and the sheafification of P composed with F, i.e. J.sheafify P ∘ F ≅ J.sheafify (P ∘ F).
Русский
Существует каноническое естественное изоморфизм между шейфификацией P после F и шейфификацией P после F, то есть J.sheafify P ∘ F ≅ J.sheafify (P ∘ F).
LaTeX
$$$J\text{.sheafify} (P) \circ F \cong J\text{.sheafify} (P \circ F)$$$
Lean4
/-- 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. -/
noncomputable def sheafifyCompIso : J.sheafify P ⋙ F ≅ J.sheafify (P ⋙ F) :=
J.plusCompIso _ _ ≪≫ (J.plusFunctor _).mapIso (J.plusCompIso _ _)
