Restriction criteria for quasicoherent modules on schemes

Quasicoherence of a module restricted to an open subscheme implies quasicoherence of the corresponding module on the slice site. Consequently, quasicoherence can be checked on restrictions to any open cover, or to all affine opens.

The criteria live in TauCeti.AlgebraicGeometry and use ordinary function application. They transport quasicoherence with Mathlib's open-subscheme equivalence and descend it with SheafOfModules.IsQuasicoherent.of_coversTop.

theorem TauCeti.AlgebraicGeometry.isQuasicoherent_over_of_isQuasicoherent_restrict {X : AlgebraicGeometry.Scheme} (M : X.Modules) (U : X.Opens) [hM : SheafOfModules.IsQuasicoherent (M.restrict U.ι)] : (SheafOfModules.over M U).IsQuasicoherent

Quasicoherence on an open subscheme implies quasicoherence on its slice site.

theorem TauCeti.AlgebraicGeometry.isQuasicoherent_of_isQuasicoherent_restrict {X : AlgebraicGeometry.Scheme} {ι : Type u} (M : X.Modules) (U : ι → X.Opens) (hU : ⨆ (i : ι), U i = ⊤) (h : ∀ (i : ι), SheafOfModules.IsQuasicoherent (M.restrict (U i).ι)) : SheafOfModules.IsQuasicoherent M

Quasicoherence can be checked on restrictions to an open cover.

theorem TauCeti.AlgebraicGeometry.isQuasicoherent_of_isQuasicoherent_restrict_affineOpens {X : AlgebraicGeometry.Scheme} (M : X.Modules) (h : ∀ (U : ↑X.affineOpens), SheafOfModules.IsQuasicoherent (M.restrict (↑U).ι)) : SheafOfModules.IsQuasicoherent M

Quasicoherence can be checked on restrictions to all affine open subschemes.