isomorphism between sheaf F and Sheaftify of `F.val`

Stream: maths

[Zhong TengXun]

Trying to do the tensor product of Sheaf of Modules in the obvious way. then when I need providing associator I belive I need the morphisms on the title to trasform associator of presheaves (M₁.val ⊗ M₂.val) ⊗ M₃.val ≅ M₁.val ⊗ (M₂.val ⊗ M₃.val) to (M₁⊗ M₂) ⊗ M₃ ≅ M₁ ⊗ (M₂⊗ M₃) after applying Sheaftification Functor.
I'll assume the results will be aquired from the adjoint relation PresheafOfModules.sheafificationAdjunction, but no idea on how to factor it yet. This (adjointion) form is not familiar to me.

[Zhong TengXun]

the sheaftification just use the identity 𝟙 _

[Joël Riou]

I am afraid there is no "obvious way" here. If you define M₁ ⊗ M₂ to be the sheafification of M₁.val ⊗ M₂.val, in order to proceed, you need to show that (M₁ ⊗ M₂) ⊗ M₃ is isomorphic to (M₁.val ⊗ M₂.val) ⊗ M₃.val (and something similar for M₁ ⊗ (M₂ ⊗ M₃). In order to do this, the critical lemma that is needed is that if f : M₁ ⟶ M₂ and g : N₁ ⟶ N₂ are morphisms of presheaves which become an isomorphism after sheafification, then it is also the case of f ⊗ g : M₁ ⊗ N₁ ⟶ M₂ ⊗ N₂, which I have obtained in PR #19915. When the PR #12728 will be merged (joint work with @Dagur Asgeirsson ), it will follow that the monoidal category structure on the category of presheaves localizes to give the monoidal category structure on the category of sheaves.

[Joël Riou]

(What I am saying above is for sheaves in a (closed) braided monoidal category, but the exact same strategy will apply to sheaves of modules.)

[Zhong TengXun]

Saw (part of) this difficulty few as I ask this, Thank for the answer. A very good example that how things supposed to obvious is actually not.