Pushforward of quasi-coherent modules along quasi-compact quasi-separated morphisms

Let f : X ⟶ Y be a quasi-compact quasi-separated morphism of schemes and let M be a quasi-coherent 𝒪_X-module. Then the pushforward f_* M is quasi-coherent. No Noetherian, finiteness or affineness hypothesis is needed.

Quasi-coherence of f_* M is checked on the affine opens V of Y: for g ∈ Γ(Y, V), the sections of f_* M over Y.basicOpen g must be the localization at g of its sections over V (AlgebraicGeometry.Scheme.Modules.isQuasicoherent_iff_isLocalizedModule). These are the sections of M over f ⁻¹ᵁ V and over f ⁻¹ᵁ Y.basicOpen g = X.basicOpen (f.app V g). The open f ⁻¹ᵁ V is quasi-compact and quasi-separated, so the qcqs lemma for quasi-coherent modules (AlgebraicGeometry.Scheme.Modules.isLocalizedModule_basicOpenRestrict_of_qcqs) applies.

Main declarations

• AlgebraicGeometry.Scheme.Modules.isLocalizedModule_basicOpenRestrict_pushforward: the localization property on Y.basicOpen g of a pushforward follows from that of M on X.basicOpen (f.app V g);
• AlgebraicGeometry.Scheme.Modules.isQuasicoherent_pushforward: pushforward along a quasi-compact quasi-separated morphism preserves quasi-coherence.

References

• R. Hartshorne, Algebraic Geometry, Proposition II.5.8(c).
• The Stacks Project, Lemma 26.24.1 (Tag 01LC).

theorem AlgebraicGeometry.Scheme.Modules.isLocalizedModule_basicOpenRestrict_pushforward {X Y : Scheme} (M : X.Modules) (f : X ⟶ Y) {V : Y.Opens} (g : ↑(Y.presheaf.obj (Opposite.op V))) [IsLocalizedModule.Away ((CategoryTheory.ConcreteCategory.hom (Scheme.Hom.app f V)) g) (M.basicOpenRestrict ((CategoryTheory.ConcreteCategory.hom (Scheme.Hom.app f V)) g))] : IsLocalizedModule.Away g (((pushforward f).obj M).basicOpenRestrict g)

Let f : X ⟶ Y, V an open of Y and g ∈ Γ(Y, V). If the sections of M over X.basicOpen (f.app V g) are the localization at f.app V g of its sections over f ⁻¹ᵁ V, then the sections of f_* M over Y.basicOpen g are the localization at g of its sections over V.

instance AlgebraicGeometry.Scheme.Modules.isQuasicoherent_pushforward {X Y : Scheme} (M : X.Modules) (f : X ⟶ Y) [SheafOfModules.IsQuasicoherent M] [QuasiCompact f] [QuasiSeparated f] : SheafOfModules.IsQuasicoherent ((pushforward f).obj M)

Pushforward along a quasi-compact quasi-separated morphism preserves quasi-coherence.