∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (M : CategoryTheory.Functor Cᵒᵖ Ab) [inst_1 : (X : Cᵒᵖ) → Module ↑(R.obj X) ↑(M.obj X)]
  (map_smul :
    ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r : ↑(R.obj X)) (m : ↑(M.obj X)),
      (CategoryTheory.ConcreteCategory.hom (M.map f)) (r • m) =
        (CategoryTheory.ConcreteCategory.hom (R.map f)) r • (CategoryTheory.ConcreteCategory.hom (M.map f)) m)
  (X : Cᵒᵖ), ↑((PresheafOfModules.ofPresheaf M map_smul).obj X) = ↑(M.obj X)