Global presentations of quasicoherent sheaves on affine schemes

A quasicoherent module on an affine scheme admits a global presentation by free sheaves, with arbitrary sets of generators and relations. This permits colimit arguments with quasicoherent modules on an affine scheme, even when no finite generation is assumed.

References

• R. Hartshorne, Algebraic Geometry, Proposition II.5.1.

noncomputable def AlgebraicGeometry.Scheme.Modules.presentationOfIsoSpec {X : Scheme} [IsAffine X] (M : X.Modules) (P : SheafOfModules.Presentation ((pullback X.isoSpec.inv).obj M)) : SheafOfModules.Presentation M

A presentation on the canonical spectrum of an affine scheme transports back to a presentation on the affine scheme.

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.Scheme.Modules.isFinite_presentationOfIsoSpec {X : Scheme} [IsAffine X] (M : X.Modules) (P : SheafOfModules.Presentation ((pullback X.isoSpec.inv).obj M)) [P.IsFinite] : (M.presentationOfIsoSpec P).IsFinite

Transporting a presentation from the canonical spectrum preserves finite generators and finite relations.

theorem AlgebraicGeometry.Scheme.Modules.nonempty_presentation_of_isAffine {X : Scheme} [IsAffine X] (M : X.Modules) [SheafOfModules.IsQuasicoherent M] : Nonempty (SheafOfModules.Presentation M)

A quasicoherent module on an affine scheme admits a global presentation by free sheaves. The generating and relation families need not be finite.