Sheaves of modules on a ringed site

Extensions of Mathlib's SheafOfModules, at Mathlib's path Algebra/Category/ModuleCat/Sheaf/: Grothendieck's axioms AB4 and AB5 and exactness of the forgetful functor, restriction to over sites, generating sections from free epimorphisms, intrinsic invertibility and rank-one local trivializations, tensor descent, exterior powers, and finite presentation with its transport, locality, and closure properties. Every signature here uses only a sheaf of rings on an arbitrary site; scheme consumers live under AlgebraicGeometry/Modules/.