Affine locality of coherent sheaves

This file proves the scheme-level affine-local criterion for coherent sheaves. Preservation and descent of finite presentation on an arbitrary ringed site are supplied by Algebra.Category.ModuleCat.Sheaf.Presentation.Locality.

The site-local arguments below are expressed using M.over U, the canonical restriction to the slice site over an open U. The scheme-level restriction results use the equivalence with the restriction functor along an open immersion constructed in AlgebraicGeometry.Modules.Restriction.OpenImmersion.

theorem AlgebraicGeometry.Scheme.Modules.IsCoherent.restrict_of_isOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (N : Y.Modules) (hN : IsCoherent Y N) : SheafOfModules.IsFinitePresentation (N.restrict f)

A coherent module restricts to a finitely presented module along an open immersion.

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

Coherence descends from finite presentation on the range slices of an affine open cover.

theorem AlgebraicGeometry.Scheme.Modules.isCoherent_iff_of_affineOpenCover {X : Scheme} (M : X.Modules) (𝒰 : X.AffineOpenCover) : IsCoherent X M ↔ ∀ (i : 𝒰.I₀), (SheafOfModules.over M (Hom.opensRange (𝒰.f i))).IsFinitePresentation

A sheaf of modules is coherent if and only if it is of finite presentation on the range slice of every member of an affine open cover.

theorem AlgebraicGeometry.Scheme.Modules.IsCoherent.restrict_affineOpenCover {X : Scheme} (M : X.Modules) (𝒰 : X.AffineOpenCover) (hM : IsCoherent X M) (i : 𝒰.I₀) : SheafOfModules.IsFinitePresentation (M.restrict (𝒰.f i))

A coherent module restricts to a finitely presented module along each scheme-level open immersion in an affine open cover.

theorem AlgebraicGeometry.Scheme.Modules.isCoherent_iff_restrict_affineOpenCover {X : Scheme} (M : X.Modules) (𝒰 : X.AffineOpenCover) : IsCoherent X M ↔ ∀ (i : 𝒰.I₀), SheafOfModules.IsFinitePresentation (M.restrict (𝒰.f i))

The scheme-level affine-local criterion for coherence.

A sheaf of modules is coherent exactly when it is of finite presentation after scheme-level restriction along each member of an affine open cover.

This is isCoherent_iff_of_affineOpenCover carried across the open-immersion/slice equivalence by Scheme.Hom.isFinitePresentation_over_iff_restrict, whose reverse half is what makes the ↔ available rather than just the forward implication. The slice-level statement remains the engine and is not reproved here; the point of this one is that downstream arguments never have to mention Over or M.over.