Quasi-coherent module sheaves are closed under kernels and cokernels #

On an arbitrary scheme, an ambient kernel or cokernel of a morphism between quasi-coherent module sheaves is again quasi-coherent. This is the half of the weak Serre property that does not need extensions, and it is what makes the inclusion of quasi-coherent sheaves into all module sheaves exact.

Why this file exists at this layer #

The affine case was previously proved inside the moduli lane, in DerivedCategory/Dqc/AffineRealization.lean, where it was reachable only by that lane. Quasi-coherence closure is a general fact about schemes: the Serre lane wants it, and Dqc(X)'s triangulated structure wants it. So it lives here, under AlgebraicGeometry, and the moduli lane consumes it.

The shape of the argument #

Exactly the shape Abelian/Kernels.lean uses for coherence, with the Noetherian hypotheses deleted — quasi-coherence needs none.

Affine: a kernel is quasi-coherent because its basic-open restrictions are localizations (isLocalizedModule_basicOpenRestriction_kernel), which is the fromTildeΓ criterion. A cokernel is quasi-coherent because tilde is a left adjoint, so it preserves the cokernel, and both ends are already tildes.
General: restriction along an open immersion preserves finite limits and colimits, and quasi-coherence is affine-local, so the affine case transfers along X.affineOpenCover.

Main results #

Scheme.Hom.isQuasicoherent_over_iff_restrict;
Scheme.Modules.isQuasicoherent_iff_restrict_affineOpenCover;
Scheme.Modules.isQuasicoherent_kernel and isQuasicoherent_cokernel;
Scheme.quasicoherent_isClosedUnderKernels and Scheme.quasicoherent_isClosedUnderCokernels.

The open-immersion/slice bridge #

source

theorem AlgebraicGeometry.Scheme.Hom.isQuasicoherent_over_of_restrict {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (M : Y.Modules) (hM : SheafOfModules.IsQuasicoherent (M.restrict f)) :

(SheafOfModules.over M (opensRange f)).IsQuasicoherent

Quasi-coherence after scheme-level restriction along an open immersion implies quasi-coherence on the range slice — the converse of the restrictFunctor instance.

source

theorem AlgebraicGeometry.Scheme.Hom.isQuasicoherent_restrict {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (M : Y.Modules) (hM : (SheafOfModules.over M (opensRange f)).IsQuasicoherent) :

SheafOfModules.IsQuasicoherent (M.restrict f)

Quasi-coherence on the range slice implies quasi-coherence after scheme-level restriction.

source

theorem AlgebraicGeometry.Scheme.Hom.isQuasicoherent_over_iff_restrict {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (M : Y.Modules) :

(SheafOfModules.over M (opensRange f)).IsQuasicoherent ↔ SheafOfModules.IsQuasicoherent (M.restrict f)

Quasi-coherence is invariant under the open-immersion/slice equivalence.

The mirror of isFinitePresentation_over_iff_restrict, and it is cheaper: the two transport maps overQuasicoherentData and restrictQuasicoherentData already exist for the finite-presentation proof, and quasi-coherence is what is left of that statement once the finiteness fields are dropped.

The affine-local criterion #

source

theorem AlgebraicGeometry.Scheme.Modules.isQuasicoherent_of_affineOpenCover {X : Scheme} (M : X.Modules) (𝒰 : X.AffineOpenCover) (h : ∀ (i : 𝒰.I₀), (SheafOfModules.over M (Hom.opensRange (𝒰.f i))).IsQuasicoherent) :

SheafOfModules.IsQuasicoherent M

Quasi-coherence descends from the range slices of an affine open cover.

source

theorem AlgebraicGeometry.Scheme.Modules.isQuasicoherent_iff_restrict_affineOpenCover {X : Scheme} (M : X.Modules) (𝒰 : X.AffineOpenCover) :

SheafOfModules.IsQuasicoherent M ↔ ∀ (i : 𝒰.I₀), SheafOfModules.IsQuasicoherent (M.restrict (𝒰.f i))

The scheme-level affine-local criterion for quasi-coherence.

Stated against scheme-level restriction rather than the range slice, so that downstream arguments never have to mention Over or M.over.

The affine case #

source

theorem AlgebraicGeometry.Scheme.Modules.isQuasicoherent_kernel_affine {R : CommRingCat} {M N : (Spec R).Modules} (g : M ⟶ N) (hM : SheafOfModules.IsQuasicoherent M) (hN : SheafOfModules.IsQuasicoherent N) :

SheafOfModules.IsQuasicoherent (CategoryTheory.Limits.kernel g)

On an affine spectrum, an ambient kernel of a morphism between quasi-coherent module sheaves is quasi-coherent.

The criterion is fromTildeΓ: a module sheaf on Spec R is quasi-coherent exactly when its basic-open restrictions are the corresponding localizations, and isLocalizedModule_basicOpenRestriction_kernel says a kernel inherits that from its two ends. No Noetherian hypothesis appears, and none is needed.

source

theorem AlgebraicGeometry.Scheme.Modules.isQuasicoherent_cokernel_affine {R : CommRingCat} {M N : (Spec R).Modules} (g : M ⟶ N) (hM : SheafOfModules.IsQuasicoherent M) (hN : SheafOfModules.IsQuasicoherent N) :

SheafOfModules.IsQuasicoherent (CategoryTheory.Limits.cokernel g)

On an affine spectrum, an ambient cokernel of a morphism between quasi-coherent module sheaves is quasi-coherent.

Cheaper than the kernel: tilde is a left adjoint, so it already preserves the cokernel, and quasi-coherence of the two ends says they are tildes.

The general scheme #

source

theorem AlgebraicGeometry.Scheme.Modules.isQuasicoherent_kernel {X : Scheme} {M N : X.Modules} (g : M ⟶ N) (hM : SheafOfModules.IsQuasicoherent M) (hN : SheafOfModules.IsQuasicoherent N) :

SheafOfModules.IsQuasicoherent (CategoryTheory.Limits.kernel g)

Kernels of morphisms between quasi-coherent module sheaves are quasi-coherent, on an arbitrary scheme.

Restriction along an open immersion preserves finite limits, so the kernel restricts to a kernel; quasi-coherence is affine-local; and the affine case applies on each member of X.affineOpenCover.

source