English
There is a canonical isomorphism between the sheafification of a presheaf F and the sheafification of the presheaf obtained from the range of J.toSheafify F; namely, J.sheafify F ≅ (Subpresheaf.range (J.toSheafify F)).sheafify J).toPresheaf.
Русский
Существует каноническое изоморфизм между шейфайфикацией прешафаза F и шейфайфикацией прешафаза, полученного как образ диапазона J.toSheafify F; то есть, J.sheafify F ≅ (Subpresheaf.range (J.toSheafify F)).sheafify J).toPresheaf.
LaTeX
$$$J.\mathrm{sheafify} F \cong \bigl( \mathrm{Subpresheaf.range}(J.toSheafify F) \bigr).\mathrm{sheafify} J . \mathrm{toPresheaf}$$$
Lean4
/-- The image of `F` in `J.sheafify F` is isomorphic to the sheafification. -/
noncomputable def sheafificationIsoImagePresheaf (F : Cᵒᵖ ⥤ Type max u v) :
J.sheafify F ≅ ((Subpresheaf.range (J.toSheafify F)).sheafify J).toPresheaf
where
hom :=
J.sheafifyLift (Subpresheaf.toRangeSheafify J _)
((isSheaf_iff_isSheaf_of_type J _).mpr <|
Subpresheaf.sheafify_isSheaf _ <|
(isSheaf_iff_isSheaf_of_type J _).mp <| GrothendieckTopology.sheafify_isSheaf J _)
inv := Subpresheaf.ι _
hom_inv_id := J.sheafify_hom_ext _ _ (J.sheafify_isSheaf _) (by simp [Subpresheaf.toRangeSheafify])
inv_hom_id := by
rw [← cancel_mono (Subpresheaf.ι _), Category.id_comp, Category.assoc]
refine Eq.trans ?_ (Category.comp_id _)
congr 1
exact J.sheafify_hom_ext _ _ (J.sheafify_isSheaf _) (by simp [Subpresheaf.toRangeSheafify])
