Grothendieck's axioms for module sheaves on a scheme

X.Modules satisfies AB4 and AB5: colimits of every shape along which colimits in Ab are exact are exact, in particular coproducts indexed by a type in the universe of the scheme and filtered colimits. Mathlib defines X.Modules as a copy of SheafOfModules X.ringCatSheaf with its own category instance, so the instance on sheaves of modules is transported by inferInstanceAs, as Mathlib does for limits and colimits.

Main results

• AlgebraicGeometry.Scheme.Modules.hasExactColimitsOfShape: the per-shape instance.
• AlgebraicGeometry.Scheme.Modules.ab4, AlgebraicGeometry.Scheme.Modules.ab5.
• AlgebraicGeometry.Scheme.Modules.isGrothendieckAbelian: X.Modules is Grothendieck abelian, hence has enough injectives and small Ext groups.

instance AlgebraicGeometry.Scheme.Modules.hasExactColimitsOfShape (X : Scheme) (K : Type u) [CategoryTheory.Category.{u, u} K] [CategoryTheory.HasExactColimitsOfShape K AddCommGrpCat] : CategoryTheory.HasExactColimitsOfShape K X.Modules

Colimits in X.Modules of every shape along which colimits in Ab are exact are exact. X.Modules is a copy of SheafOfModules X.ringCatSheaf with its own category instance, so the instance on sheaves of modules is not found by search and is transported by inferInstanceAs, as Mathlib transports Abelian, HasLimits and HasColimits.

instance AlgebraicGeometry.Scheme.Modules.ab4 (X : Scheme) : CategoryTheory.AB4 X.Modules

X.Modules satisfies AB4: coproducts indexed by a type in the universe of X are exact.

instance AlgebraicGeometry.Scheme.Modules.ab5 (X : Scheme) : CategoryTheory.AB5 X.Modules

X.Modules satisfies AB5: filtered colimits are exact.

instance AlgebraicGeometry.Scheme.Modules.isGrothendieckAbelian (X : Scheme) : CategoryTheory.IsGrothendieckAbelian.{u, u, u + 1} X.Modules

X.Modules is Grothendieck abelian: AB5 as above and the separator of SheafOfModules.isGrothendieckAbelian. Mathlib then supplies EnoughInjectives X.Modules and HasExt.{u} X.Modules.