Sheaves of modules on over categories #
Elementary API for restricting a sheaf of modules on an arbitrary ringed site to an over category. No geometric realization of the site is required.
@[simp]
theorem
SheafOfModules.overFunctor_obj
{C : Type u}
[CategoryTheory.Category.{u, u} C]
{J : CategoryTheory.GrothendieckTopology C}
(R : CategoryTheory.Sheaf J RingCat)
(U : C)
(M : SheafOfModules R)
: