@[reducible, inline]

abbrev AlgebraicGeometry.SheafOfOXModules {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) : Type (max (max (max u u₁) (v + 1)) v₁)

An O_X-module (Definition 25, Lecture 10): a sheaf of modules over a sheaf of rings R on a site, i.e. a sheafified version of a ring-action structure.