Presheaves of modules

Extensions of Mathlib's PresheafOfModules, at Mathlib's path Algebra/Category/ModuleCat/Presheaf/: exactness of colimits, additivity of the pointwise tensor product, and objectwise exterior powers built from semilinear exterior powers of the restriction maps.