theorem Lemma24.pushforward_over_affineOpen_isQuasicoherent {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (F : X.Modules) [SheafOfModules.IsQuasicoherent F] (U : ↑Y.affineOpens) : (SheafOfModules.over ((AlgebraicGeometry.Scheme.Modules.pushforward f).obj F) ↑U).IsQuasicoherent

Lemma 24 (local case): on any affine open U ⊆ Y, the restriction of the pushforward f_*F of a quasicoherent sheaf F on X is quasicoherent.

theorem Lemma24.affineOpens_coversTop (Y : AlgebraicGeometry.Scheme) : (Opens.grothendieckTopology ↥Y).CoversTop fun (U : ↑Y.affineOpens) => ↑U

The collection of affine opens of Y covers the whole space in the Grothendieck topology of opens.

theorem Lemma24.pushforward_isQuasicoherent {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (F : X.Modules) [SheafOfModules.IsQuasicoherent F] : SheafOfModules.IsQuasicoherent ((AlgebraicGeometry.Scheme.Modules.pushforward f).obj F)

Lemma 24 (global): the pushforward f_*F along a morphism of schemes f : X → Y of a quasicoherent F on X is again quasicoherent. This is obtained by gluing the local case over the affine cover of Y.

instance Lemma24.pushforward_isQuasicoherent_inst {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (F : X.Modules) [SheafOfModules.IsQuasicoherent F] : SheafOfModules.IsQuasicoherent ((AlgebraicGeometry.Scheme.Modules.pushforward f).obj F)

Instance form of Lemma 24: pushforward preserves quasicoherence, so the typeclass search can pick it up automatically.

theorem Lemma24.pushforward_isQuasicoherent_affine {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y] (F : X.Modules) [SheafOfModules.IsQuasicoherent F] : SheafOfModules.IsQuasicoherent ((AlgebraicGeometry.Scheme.Modules.pushforward f).obj F)

Affine-to-affine specialisation: for f : X → Y between affine schemes, pushforward of a quasicoherent sheaf is quasicoherent.

theorem Lemma24.pushforward_isQuasicoherent_of_affineHom {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffineHom f] (F : X.Modules) [SheafOfModules.IsQuasicoherent F] : SheafOfModules.IsQuasicoherent ((AlgebraicGeometry.Scheme.Modules.pushforward f).obj F)

For an affine morphism f : X → Y, pushforward of a quasicoherent sheaf is quasicoherent.