English
There is a natural bijection between morphisms from the sheafification of a presheaf of modules to any sheaf F, and morphisms from the original presheaf to the restriction-scalars of the forgetful image of F.
Русский
Существует естественная биекция между гомоморфизмами от sheafify α φ к F и гомоморфизмами от исходного прешефа к ограниченному по скалярам образу F.
LaTeX
$$$\mathrm{Hom}(\mathrm{sheafify}(\alpha,\phi), F) \cong \mathrm{Hom}(M_0, (\mathrm{restrictScalars}\ \alpha).(\mathrm{forget}\, F)).$$$
Lean4
/-- The bijection
`(sheafify α φ ⟶ F) ≃ (M₀ ⟶ (restrictScalars α).obj ((SheafOfModules.forget _).obj F))`
which is part of the universal property of the sheafification of the presheaf of modules `M₀`,
for any sheaf of modules `F`, see `PresheafOfModules.sheafificationAdjunction` -/
noncomputable def sheafifyHomEquiv {F : SheafOfModules.{v} R} :
(sheafify α φ ⟶ F) ≃ (M₀ ⟶ (restrictScalars α).obj ((SheafOfModules.forget _).obj F)) :=
(SheafOfModules.fullyFaithfulForget R).homEquiv.trans (sheafifyHomEquiv' α φ F.isSheaf)
