English
Let α: R₀ → R be locally injective and locally surjective, and let P be a presheaf of modules with F a sheaf of modules. Then for any morphism f from the sheafification of P to F, the induced map on presheaf level agrees with the Hom-Equivalence coming from the sheafification adjunction.
Русский
Пусть α: R₀ → R является локально биективной по каждой точке, P — прешейф модулей, F — шейфикационному модулов. Тогда для любого отображения f: (sheafification α).obj P ⟶ F верно соответствие подлежащее гомоморфизмов через эквивалентность гомов в адъункции шейификации.
LaTeX
$$$ (toPresheaf\ R_0).map (sheafificationHomEquiv\ α\ f) = (sheafificationAdjunction\ J AddCommGrpCat).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F) ((SheafOfModules.toSheaf R).map f) $$$
Lean4
theorem toPresheaf_map_sheafificationHomEquiv {P : PresheafOfModules.{v} R₀} {F : SheafOfModules.{v} R}
(f : (sheafification α).obj P ⟶ F) :
(toPresheaf R₀).map (sheafificationHomEquiv α f) =
(sheafificationAdjunction J AddCommGrpCat).homEquiv P.presheaf ((SheafOfModules.toSheaf _).obj F)
((SheafOfModules.toSheaf _).map f) :=
by
rw [toPresheaf_map_sheafificationHomEquiv_def, Adjunction.homEquiv_unit]
dsimp
