Sheaf of modules on a scheme

Stream: mathlib4

[Raphael Douglas Giles]

We have a couple of questions about sheaves of modules in mathlib.

Q1: Mathlib has support for sheaves of modules over an arbitrary sheaf of rings, but now if X is a scheme and I want a sheaf of O_X modules, then the best I can come up with is:

(F : SheafOfModules ((sheafCompose (Opens.grothendieckTopology ↥X)  (forget₂ CommRingCat RingCat)).obj X.sheaf))

Is there a better way with current mathlib or do we need a new definition?

Q2: Suppose X is a scheme over an affine base Spec R. Is there already a slick way to turn a sheaf of O_X modules F into a sheaf of R modules? I started writing this snippet but it looks like it 's going to be a pretty long definition because the second component of the structure morphism $f$ is a morphism of sheaves $\mathcal{O}_R \to f_* \mathcal{O}_X$

def foo {X : Scheme} (R : CommRingCat) [X.CanonicallyOver (Spec R)]
    (F : SheafOfModules ((sheafCompose (Opens.grothendieckTopology ↥X)
    (forget₂ CommRingCat RingCat)).obj X.sheaf)) :
  X.Opensᵒᵖ ⥤ ModuleCat R where
    obj U := by
      let f := X ↘ Spec R
      sorry
    map := sorry
    map_id := sorry
    map_comp := sorry

[Joël Riou]

Q1 -> We have https://leanprover-community.github.io/mathlib4_docs/Mathlib/AlgebraicGeometry/Modules/Sheaf.html

[Joël Riou]

Q2 -> I would think that what we need is an equivalence of categories between the category of presheaves of R-modules on a category and the category of presheaves of modules over the constant presheaf with values R. Up to the verification that the presheaves we construct are sheaves (which shall be easy here), we are reduced to the "basic" functoriality of presheaves corresponding to the "restriction of scalars" for a morphism from the constant presheaf of rings R to the structure (pre)sheaf $\mathcal O_X$ https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Category/ModuleCat/Presheaf/Pushforward.html