Pullback of quasi-coherent module sheaves #

Pullback of module sheaves along any scheme morphism preserves quasi-coherence. The existing neutral presentation transport applies on inverse-image opens, which still cover the source scheme.

Main definitions #

This file introduces no new carrier, class, or instance.

Main results #

AlgebraicGeometry.Scheme.Modules.isQuasicoherent_pullback preserves quasi-coherence without a flatness, finiteness, or quasi-compactness premise.

Implementation notes #

The proof transports the chosen SheafOfModules.QuasicoherentData across each inverse-image open, then applies SheafOfModules.QuasicoherentData.isQuasicoherent.

References #

Pinned Mathlib's SheafOfModules.IsQuasicoherent supplies local presentation data, and AlgebraicGeometry.Scheme.Hom.coversTop_preimage supplies the cover.

Tags #

scheme modules, pullback, quasi-coherence

source

theorem AlgebraicGeometry.Scheme.Modules.isQuasicoherent_pullback {X Y : Scheme} (f : X ⟶ Y) (M : Y.Modules) (hM : SheafOfModules.IsQuasicoherent M) :

SheafOfModules.IsQuasicoherent ((pullback f).obj M)

Pullback of a quasi-coherent module sheaf is quasi-coherent along every scheme morphism. Presentations pull back on each member of the chosen open cover; no exactness of pullback is needed.