The category of presheaves of modules over a scheme

In this file, given a scheme X, we define the category of presheaves of modules over X. As categories of presheaves of modules are defined for presheaves of rings (and not presheaves of commutative rings), we also introduce a definition X.ringCatSheaf for the underlying sheaf of rings of X.

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.ringCatSheaf (X : AlgebraicGeometry.Scheme) : TopCat.Sheaf RingCat ↑X.toPresheafedSpace

The underlying sheaf of rings of a scheme.

Equations

• X.ringCatSheaf = (CategoryTheory.sheafCompose (Opens.grothendieckTopology ↑↑X.toPresheafedSpace) (CategoryTheory.forget₂ CommRingCat RingCat)).obj X.sheaf

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.PresheafOfModules (X : AlgebraicGeometry.Scheme) : Type (u + 1)

The category of presheaves of modules over a scheme.

Equations

• X.PresheafOfModules = PresheafOfModules X.ringCatSheaf.val