The category of sheaves of modules over a scheme

In this file, we define the abelian category of sheaves of modules X.Modules over a scheme X.

@[reducible, inline]

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

The category of sheaves of modules over a scheme.

Equations

• X.Modules = SheafOfModules X.ringCatSheaf

noncomputable instance AlgebraicGeometry.Scheme.instAbelianModules (X : Scheme) : CategoryTheory.Abelian X.Modules

Equations

• X.instAbelianModules = inferInstance