English
For a morphism g between P via the symmetrized hom-equivalence, the corresponding maps coincide under the adjunction isomorphism with the sheafified picture.
Русский
Для отображения g между P через симметрическую гомоморфизм-эквиваленцию соответствующие отображения совпадают через тождество адъункции с шейфицированной картинкой.
LaTeX
$$$ (SheafOfModules.toSheaf R).map ((sheafificationHomEquiv α).symm g) = \Big( (sheafificationAdjunction J AddCommGrpCat).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F) \Big).symm ((toPresheaf R_0).map g) $$$
Lean4
theorem toSheaf_map_sheafificationHomEquiv_symm {P : PresheafOfModules.{v} R₀} {F : SheafOfModules.{v} R}
(g : P ⟶ (restrictScalars α).obj ((SheafOfModules.forget _).obj F)) :
(SheafOfModules.toSheaf _).map ((sheafificationHomEquiv α).symm g) =
(((sheafificationAdjunction J AddCommGrpCat).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F)).symm
((toPresheaf R₀).map g)) :=
by
obtain ⟨f, rfl⟩ := (sheafificationHomEquiv α).surjective g
apply ((sheafificationAdjunction J AddCommGrpCat).homEquiv _ _).injective
rw [Equiv.apply_symm_apply, Adjunction.homEquiv_unit, Equiv.symm_apply_apply]
rfl
