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.

[Raphael Douglas Giles]

@Joël Riou What's the status on tensor products of sheaves of modules now that this stuff has been merged? It seems like just writing M \otimes N for some sheaves of modules M and N doesn't currently work, is there more work to be done or is this just not the correct way to work with the definitions?

[Joël Riou]

For sheaves with values in a monoidal category, we have a monoidal category structure docs#CategoryTheory.Sheaf.monoidalCategory thanks to the work by @Dagur Asgeirsson and myself. A similar strategy would apply for sheaves of modules: construct the internal hom of presheaves, show it is a sheaf when the target presheaf is a sheaf, etc. I do not think anybody is currently working on this now, so anybody is welcome to implement it.