Sheaves on a site

Generic sheaf theory on an arbitrary site: constant pullback, cohomology pushforward, short exact sequences, and coverwise detection of local equivalences. Sheaves of modules on a ringed site extend Mathlib's SheafOfModules and live at its path, Algebra/Category/ModuleCat/Sheaf/.