Documentation

DerivedAlgGeo.AlgebraicGeometry.Modules.Coherent.Noetherian

Noetherian coherent sheaves #

Every coherent sheaf on a Noetherian scheme is a Noetherian object. The proof has three layers.

  1. A finite module over a Noetherian ring is a Noetherian object of FGModuleCat, hence the affine equivalence makes every object of Coh (Spec R) Noetherian.
  2. Restriction of coherent sheaves along an open immersion preserves monomorphisms. Restrictions to an open cover jointly reflect isomorphisms: this is checked on stalks using Scheme.Modules.restrictStalkNatIso.
  3. On a finite cover, take the maximum of the local stabilization indices. The categorical finite-family theorem then reflects the resulting local isomorphisms to a global one.

The quasi-compactness in IsNoetherian X is essential. Local Noetherianity alone would allow an infinite disjoint union, whose coherent sheaves need not satisfy a global ascending-chain condition.

This discharges the MuHNInput.noetherian obligation for proper varieties. It does not assert Grothendieck slope boundedness, which remains the other field of MuHNInput.

Main results #

source
noncomputable def AlgebraicGeometry.Coh.restrict {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] :
CategoryTheory.Functor (Coh Y) (Coh X)

Restriction of coherent sheaves along an open immersion.

Equations
Instances For
    source
    noncomputable def AlgebraicGeometry.Coh.restrictCompι {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] :
    (restrict f).comp (ι X) ≅ (ι Y).comp (Scheme.Modules.restrictFunctor f)

    Forgetting coherence after coherent restriction is module-sheaf restriction after forgetting coherence.

    Equations
    Instances For
      source
      instance AlgebraicGeometry.Coh.restrict_preservesMonomorphisms {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] [IsLocallyNoetherian Y] :
      (restrict f).PreservesMonomorphisms

      Restriction along an open immersion preserves monomorphisms of coherent sheaves when the ambient scheme is locally Noetherian.

      source
      theorem AlgebraicGeometry.Coh.restrict_jointlyReflectsIsomorphisms {X : Scheme} (Uc : X.OpenCover) [IsLocallyNoetherian X] {M N : Coh X} (f : M ⟶ N) (hf : ∀ (i : Uc.I₀), CategoryTheory.IsIso ((restrict (Uc.f i)).map f)) :
      CategoryTheory.IsIso f

      Restriction to the members of an open cover jointly reflects isomorphisms of coherent sheaves.

      At a point of X, choose a preimage in one cover member. Restriction commutes with the stalk at that preimage, so an isomorphism after restriction gives an isomorphism on the original stalk. The stalk criterion then gives an isomorphism of module sheaves, and the fully faithful coherent inclusion reflects it.

      source
      instance AlgebraicGeometry.Coh.isNoetherianObject_affine {R : CommRingCat} [IsNoetherianRing ↑R] (M : Coh (Spec R)) :
      CategoryTheory.IsNoetherianObject M

      Every coherent sheaf on an affine Noetherian scheme is a Noetherian object.

      source
      theorem AlgebraicGeometry.Coh.isNoetherianObject_of_finite_openCover {X : Scheme} (Uc : X.OpenCover) [Finite Uc.I₀] [IsLocallyNoetherian X] (M : Coh X) (hlocal : ∀ (i : Uc.I₀), CategoryTheory.IsNoetherianObject ((restrict (Uc.f i)).obj M)) :
      CategoryTheory.IsNoetherianObject M

      Finite-open-cover reduction for Noetherian coherent sheaves. If the restriction of M to every member of a finite open cover is Noetherian, then M is Noetherian.

      source
      instance AlgebraicGeometry.Coh.isNoetherianObject {X : Scheme} [IsNoetherian X] (M : Coh X) :
      CategoryTheory.IsNoetherianObject M

      Every coherent sheaf on a Noetherian scheme is a Noetherian object.