30.2 Čech cohomology of… to 30.16 Higher direct images…

Section30.2 Čech cohomology of quasi-coherent sheaves #

Section 30.2 of the Stacks Project, Tag 01X8. 6 tags here are carried by 14 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01X9, a lemma

Tag 01X9 in the Stacks Project.

Stacks.Cohomology.Cech.isZero_cechCohomology_of_isStandardOpenCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/Cech/StandardCoverVanishing.lean, line 424.

Positive-degree Čech cohomology of a quasi-coherent module vanishes on a finite standard open cover of an affine open. Here F is a quasi-coherent module on the ambient scheme X, the affine open U is covered by the ambient basic opens X.basicOpen (g i) attached to a finite family g of sections over U whose basic opens cover Spec Γ(X, U), and Čech cohomology is the homology of Mathlib's cechComplexFunctor applied to the underlying abelian sheaf of F.

theorem isZero_cechCohomology_of_isStandardOpenCover
    (X : Scheme.{u}) (F : X.Modules) [F.IsQuasicoherent]
    (U : X.Opens) (hU : IsAffineOpen U) {n : ℕ} (g : Fin n → Γ(X, U))
    (hg : PrimeSpectrum.IsStandardOpenCoverOfSpectrum g) (p : ℕ) (hp : 0 < p) :
    IsZero (((cechComplexFunctor fun i ↦ X.basicOpen (g i)).obj
      ((SheafOfModules.toSheaf X.ringCatSheaf).obj F).obj).homology p)

Tag 01XB, a lemma

Tag 01XB in the Stacks Project.

Stacks.Cohomology.Cech.isZero_hgroup_of_isAffineOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/Cech/AffineVanishing.lean, line 307. References: EGA III (1.3.1), “more general”; EGA I (5.1.9.2), “more general”; EGA II (5.2.4).

Serre vanishing on affine schemes. The positive-degree cohomology of a quasi-coherent module on an affine open of a scheme vanishes.

theorem isZero_hgroup_of_isAffineOpen (X : Scheme.{u}) (F : X.Modules)
    [F.IsQuasicoherent] (U : X.Opens) (hU : IsAffineOpen U) (p : ℕ) (hp : 0 < p) :
    IsZero (Hgroup X.ringCatSheaf U p F)

Stacks.Duality.Coherator.affineAmplitudeIn_zero_zero_single, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/Coherator/QuasiCoherentAffineAmplitude.lean, line 134. The attribute's comment: “the vanishing in positive degrees, together with left exactness in negative degrees, in the hypercohomology spelling of Coherator.AffineAmplitudeIn at the locally small model”.

A quasi-coherent module has affine amplitude in [0, 0]. Placed in degree zero, a quasi-coherent 𝒪_X-module has hypercohomology over every affine open of X concentrated in degree zero: this is the vanishing in negative degrees of Stacks.Duality.Coherator.isZero_homology_derivedSectionsLocallySmall_single_of_neg together with Serre vanishing ([Stacks, Tag 01XB]) in positive degrees.

It is the hypothesis of [Stacks, Tag 0CSA] at a = b = 0, which is what Example [Stacks, Tag 0CSB] feeds that tag.

theorem affineAmplitudeIn_zero_zero_single (M : X.Modules) [M.IsQuasicoherent] :
    AffineAmplitudeIn X 0 0 ((DerivedCategory.singleFunctor X.Modules 0).obj M)

Tag 01XC, a lemma

Tag 01XC in the Stacks Project.

Stacks.Cohomology.Affine.isZero_rightDerived_pushforward_of_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineCohomologyVanishing/Basic.lean, line 241.

[Stacks, Tag 01XC]. If f : X ⟶ S is an affine morphism of schemes and F is a quasi-coherent 𝒪_X-module, then Rⁱ f_* F vanishes for every i > 0.

theorem isZero_rightDerived_pushforward_of_isAffineHom {X S : Scheme.{u}} (f : X ⟶ S)
    (F : X.Modules) [IsAffineHom f] [F.IsQuasicoherent] (i : ℤ) (hi : 0 < i) :
    IsZero (((Scheme.Modules.pushforward f).rightDerivedPlus i).obj F)

Stacks.AffineHigherDirectImage.isZero_rightDerivedPlus_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineHigherDirectImage/Vanishing.lean, line 239.

[Stacks, Tag 01XC]. If f : X ⟶ S is an affine morphism of schemes and F is a quasi-coherent 𝒪_X-module, then R ⁱ f_* F = 0 for every i > 0.

theorem isZero_rightDerivedPlus_pushforward [IsAffineHom f] (F : X.Modules)
    [F.IsQuasicoherent] (i : ℤ) (hi : 0 < i) :
    IsZero (((Scheme.Modules.pushforward f).rightDerivedPlus i).obj F)

Tag 089W, a lemma

Tag 089W in the Stacks Project.

Stacks.Cohomology.AffineComparison.cohomologyIsoPushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineCohomologyComparison/Basic.lean, line 209.

[Stacks, Tag 089W]. For an affine morphism of schemes f : X ⟶ S and a quasi-coherent 𝒪_X-module F, the cohomology of F on X is the cohomology of its direct image on S, in every degree i ≥ 0, as modules over Γ(S, ⊤) after restriction of scalars along f^♯.

The higher direct images vanish ([Stacks, Tag 01XC]), so F is acyclic for f_*, and the direct image of an injective module has acyclic sections ([Stacks, Tag 01EX] part (2)), so the right derived functor of Γ(S, ⊤) ∘ f_* collapses onto H^i(S, f_* −); the other factor is Γ(X, ⊤) with its scalars restricted, by [Stacks, Tag 01EZ].

public def cohomologyIsoPushforward [AlgebraicGeometry.IsAffineHom f]
    (F : X.Modules) [F.IsQuasicoherent] (n : ℕ) :
    (ModuleCat.restrictScalars f.appTop.hom).obj
        (((moduleGlobalSections X).rightDerived n).obj F) ≅
      ((moduleGlobalSections S).rightDerived n).obj
        ((AlgebraicGeometry.Scheme.Modules.pushforward f).obj F)

Stacks.AffineCohomologyPushforward.cohomologyPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineHigherDirectImage/Natural.lean, line 266. The attribute's comment: “the natural isomorphism”. References: EGA II (5.2.3); EGA III (1.3.4), “g to a point”; EGA III (1.3.3).

[Stacks, Tag 089W]. For an affine morphism of schemes f : X ⟶ S, cohomology of a quasi-coherent module is canonically isomorphic to cohomology of its pushforward, naturally in the module: this is an isomorphism of functors on the category of quasi-coherent 𝒪_X-modules, not a choice of isomorphism for each one.

def cohomologyPushforwardIso [IsAffineHom f] (i : ℕ) :
    ObjectProperty.ι (SheafOfModules.isQuasicoherent (R := X.ringCatSheaf)) ⋙
        Hfunctor X.ringCatSheaf ⊤ i ≅
      ObjectProperty.ι (SheafOfModules.isQuasicoherent (R := X.ringCatSheaf)) ⋙
        Scheme.Modules.pushforward f ⋙ Hfunctor S.ringCatSheaf ⊤ i

Stacks.AffineCohomologyResolution.cohomologyPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineMorphismCohomology/Normalized.lean, line 110. The attribute's comment: “the natural isomorphism”. References: EGA II (5.2.3); EGA III (1.3.4), “g to a point”; EGA III (1.3.3).

[Stacks, Tag 089W]. For an affine morphism, cohomology of a quasi-coherent module is canonically isomorphic to cohomology of its pushforward. The isomorphism is a natural isomorphism on the category of quasi-coherent modules, rather than an unrelated choice of an isomorphism for each module.

public noncomputable def cohomologyPushforwardIso [IsAffineHom f] (i : ℕ) :
    ObjectProperty.ι (SheafOfModules.isQuasicoherent X.ringCatSheaf) ⋙
          Hfunctor X.ringCatSheaf ⊤ i ≅
      ObjectProperty.ι (SheafOfModules.isQuasicoherent X.ringCatSheaf) ⋙
          Scheme.Modules.pushforward f ⋙ Hfunctor S.ringCatSheaf ⊤ i

Stacks.AffineCohomologyResolution.cohomologyPushforwardIso_hom_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineMorphismCohomology/Normalized.lean, line 133. The attribute's comment: “comparison of resolutions”.

The affine cohomology isomorphism is computed by any map from the pushforward of an injective resolution to an injective resolution of the pushforward that preserves the augmentation. Global sections of the pushed-forward complex are definitionally global sections of the original complex.

public theorem cohomologyPushforwardIso_hom_eq [IsAffineHom f] (F : X.Modules)
    [F.IsQuasicoherent] (i : ℕ)
    (I : InjectiveResolution (C := SheafOfModules X.ringCatSheaf) F)
    (J : InjectiveResolution (C := SheafOfModules S.ringCatSheaf)
      ((Scheme.Modules.pushforward f).obj F))
    (φ : ((Scheme.Modules.pushforward f).mapHomologicalComplex (ComplexShape.up ℕ)).obj
      I.cocomplex ⟶ J.cocomplex)
    (hφ : (Scheme.Modules.pushforward f).map (I.ι.f 0) ≫ φ.f 0 = J.ι.f 0) :
    (cohomologyPushforwardIso f i).hom.app ⟨F, inferInstance⟩ =
      (I.isoRightDerivedObj (secF X.ringCatSheaf ⊤) i).hom ≫
        HomologicalComplex.homologyMap
          (((secF S.ringCatSheaf ⊤).mapHomologicalComplex (ComplexShape.up ℕ)).map φ) i ≫
        (J.isoRightDerivedObj (secF S.ringCatSheaf ⊤) i).inv

Stacks.AffineCohomologyResolution.cohomologyPushforwardIso_zero_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineMorphismCohomology/Normalized.lean, line 162. The attribute's comment: “degree-zero normalization”.

In degree zero, the affine cohomology isomorphism agrees with the ordinary identification of global sections through the canonical maps to zeroth right derived functors.

public theorem cohomologyPushforwardIso_zero_hom [IsAffineHom f] :
    Functor.whiskerLeft
          (ObjectProperty.ι (SheafOfModules.isQuasicoherent X.ringCatSheaf))
          (secF X.ringCatSheaf ⊤).toRightDerivedZero ≫
        (cohomologyPushforwardIso f 0).hom =
      Functor.whiskerLeft
          (ObjectProperty.ι (SheafOfModules.isQuasicoherent X.ringCatSheaf))
          (sectionsPushforwardIso f).hom ≫
        Functor.whiskerLeft
          (ObjectProperty.ι (SheafOfModules.isQuasicoherent X.ringCatSheaf) ⋙
            Scheme.Modules.pushforward f)
          (secF S.ringCatSheaf ⊤).toRightDerivedZero

Tag 0BDX, a lemma

Tag 0BDX in the Stacks Project.

AlgebraicGeometry.isAffineHom_diagonal_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/AffineDiagonal.lean, line 96. The attribute's comment: “equivalent conditions”.

Stacks Project, Tag 0BDX. For a scheme X, the following are equivalent: its diagonal is affine; intersections of two affine opens are affine; and it admits an affine open cover all of whose nonempty finite intersections are affine.

theorem isAffineHom_diagonal_tfae (X : Scheme.{u}) : List.TFAE [
    IsAffineHom (pullback.diagonal (terminal.from X)),
    ∀ (U V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (U ⊓ V),
    ∃ 𝒰 : Scheme.AffineOpenCover.{u} X,
      ∀ (p : ℕ) (i : Fin (p + 1) → 𝒰.I₀),
        IsAffineOpen (⨅ j, (𝒰.f (i j)).opensRange)]

Declarations registered for the tag:

AlgebraicGeometry.Scheme.IsSeparated.isSeparated_terminal_from registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/AffineDiagonal.lean, line 49 (StacksFrontier): “separated case: the structure morphism is separated”.
AlgebraicGeometry.IsSeparated.isClosedImmersion_diagonal registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/AffineDiagonal.lean, line 51 (StacksFrontier): “separated case: the diagonal is a closed immersion”.
AlgebraicGeometry.IsClosedImmersion.instIsAffineHom registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/AffineDiagonal.lean, line 53 (StacksFrontier): “separated case: closed immersions are affine”. References: EGA I (4.2.3), “more general”; EGA II (1.2.2); EGA II (1.6.2); SGA 3 VIB (2.9.1), “special case”; SGA 3 XXV (4.3), “partial”.

Tag 01XD, a lemma

Tag 01XD in the Stacks Project.

Stacks.Cohomology.Affine.isIso_cechCohomologyToCohomology_of_isAffineOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineCohomologyVanishing/CechAffineCover.lean, line 100. References: EGA III (1.4.1); EGA III (1.4.2), “more general”.

[Stacks, Tag 01XD]. A covering of an open subset of a scheme whose finite intersections are all affine opens computes the cohomology of a quasi-coherent module by its Čech complex: the canonical comparison of [Stacks, Tag 01EQ] from Čech cohomology to sheaf cohomology is an isomorphism of Γ(U, 𝒪_X)-modules in every degree.

public theorem isIso_cechCohomologyToCohomology_of_isAffineOpen
    (X : Scheme.{u}) {I : Type u} (U : X.Opens) (Ui : I → X.Opens) (hU : U = ⨆ i, Ui i)
    (haffine : ∀ (r : ℕ) (s : Fin (r + 1) → I), IsAffineOpen (⨅ k, Ui (s k)))
    (F : X.Modules) [F.IsQuasicoherent] (p : ℕ) :
    IsIso ((cechCohomologyToCohomology X.ringCatSheaf U Ui hU (p : ℤ)).app F)

Stacks.Cohomology.CechAffineCover.isIso_cechCohomologyToCohomology_app_of_isAffineOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineCover/Basic.lean, line 86. References: EGA III (1.4.1); EGA III (1.4.2), “more general”.

[Stacks, Tag 01XD]: a cover of a scheme whose finite intersections are affine computes the cohomology of a quasi-coherent module by its Čech complex. The canonical comparison Ȟᵖ(𝒰, F) ⟶ Hᵖ(U, F) of [Stacks, Tag 01EQ] is an isomorphism of Γ(U, 𝒪_X)-modules for every p.

theorem isIso_cechCohomologyToCohomology_app_of_isAffineOpen
    (haff : ∀ (r : ℕ) (s : Fin (r + 1) → I), IsAffineOpen (⨅ k, Ui (s k)))
    (F : X.Modules) [F.IsQuasicoherent] (p : ℕ) :
    IsIso ((cechCohomologyToCohomology X.ringCatSheaf U Ui hU (p : ℤ)).app F)

Stacks.Cohomology.Cech.isIso_cechCohomologyToCohomology_app_of_isAffineOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/Cech/AffineIntersectionComparison.lean, line 87. References: EGA III (1.4.1).

[Stacks, Tag 01XD]. Let X be a scheme and let U be an open covering of X such that every intersection U_{i₀} ⊓ … ⊓ U_{iₚ} is affine. For a quasi-coherent 𝒪_X-module ℱ the canonical comparison from the Čech cohomology of the covering to the cohomology of ℱ is an isomorphism of Γ(X, 𝒪_X)-modules in every degree.

public theorem isIso_cechCohomologyToCohomology_app_of_isAffineOpen (X : Scheme.{u})
    {I : Type u} (U : I → X.Opens) (hU : IsOpenCover U)
    (hUaffine : ∀ (p : ℕ) (i : Fin (p + 1) → I), IsAffineOpen (⨅ j, U (i j)))
    (F : X.Modules) [F.IsQuasicoherent] (p : ℕ) :
    IsIso ((Stacks.Cohomology.CechDerived.cechCohomologyToCohomology X.ringCatSheaf
      (⊤ : X.Opens) U hU.symm (p : ℤ)).app F)

Sources

LeanStacks.Cohomology.Cech.isZero_cechCohomology_of_isStandardOpenCover · Stacks.Cohomology.Cech.isZero_hgroup_of_isAffineOpen · Stacks.Duality.Coherator.affineAmplitudeIn_zero_zero_single · Stacks.Cohomology.Affine.isZero_rightDerived_pushforward_of_isAffineHom · Stacks.AffineHigherDirectImage.isZero_rightDerivedPlus_pushforward · Stacks.Cohomology.AffineComparison.cohomologyIsoPushforward · Stacks.AffineCohomologyPushforward.cohomologyPushforwardIso · Stacks.AffineCohomologyResolution.cohomologyPushforwardIso

Section30.3 Vanishing of cohomology #

Section 30.3 of the Stacks Project, Tag 01XE. 4 tags here are carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01XF, a lemma

Tag 01XF in the Stacks Project.

Stacks.SerreCriterion.isAffine_of_forall_isZero_H1_ideal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SerreAffinenessCriterion/VanishingCriterion.lean, line 59. References: EGA II (5.2.1), “(d')⇒(a)”; EGA IV (1.7.17), “(d') => affine”; EGA III (1.4.7), “(ii), special case”.

Serre's criterion for affineness. A quasi-compact scheme on which the first cohomology of every quasi-coherent sheaf of ideals vanishes is affine.

theorem isAffine_of_forall_isZero_H1_ideal (X : Scheme.{u}) [CompactSpace X]
    (hH₁ : ∀ I : Subobject (SheafOfModules.unit X.ringCatSheaf),
      (Subobject.underlying.obj I).IsQuasicoherent →
        IsZero (((SheafOfModules.evaluation X.ringCatSheaf (op ⊤)).rightDerived 1).obj
          (Subobject.underlying.obj I))) :
    IsAffine X

Tag 01XG, a lemma

Tag 01XG in the Stacks Project.

Stacks.SerreCriterion.isAffine_of_forall_isZero_H1_finiteType_ideal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SerreAffinenessCriterion/FiniteTypeIdeals.lean, line 92. References: EGA II (5.2.1), “(d')⇒(a), quasi-sep”; EGA III (1.4.7), “(ii), special case”.

Serre's criterion for affineness, finite type form. Vanishing of the first cohomology on the finite type quasi-coherent sheaves of ideals suffices for affineness of a quasi-compact, quasi-separated scheme.

theorem isAffine_of_forall_isZero_H1_finiteType_ideal (X : Scheme.{u}) [CompactSpace X]
    [QuasiSeparatedSpace X]
    (hH₁ : ∀ I : Subobject (SheafOfModules.unit X.ringCatSheaf),
      (Subobject.underlying.obj I).IsQuasicoherent →
        (Subobject.underlying.obj I).IsFiniteType →
          IsZero (((SheafOfModules.evaluation X.ringCatSheaf (op ⊤)).rightDerived 1).obj
            (Subobject.underlying.obj I))) :
    IsAffine X

Tag 0B5P, a lemma

Tag 0B5P in the Stacks Project.

AlgebraicGeometry.Scheme.Modules.isAmple_of_forall_isZero_h1_quasicoherentIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleDegreeCriterion/QuasicoherentIdeal.lean, line 204. References: EGA III (2.6.1), “c) => a), absolute”.

[Stacks, Tag 0B5P]. Let X be a quasi-compact scheme and 𝓛 an invertible 𝒪_X-module. If every quasi-coherent submodule 𝒥 ⊆ 𝒪_X admits an n ≥ 1 with H¹(X, 𝒥 ⊗ 𝓛^{⊗ n}) = 0, then 𝓛 is ample.

The hypothesis is clause (2) of the tag: a quasi-coherent sheaf of ideals is a quasi-coherent 𝒪_X-module with a monomorphism into 𝒪_X. It is specialised at the ideal sheaf of a closed immersion, which is such a submodule — quasi-coherent by Stacks.Conormal.isQuasicoherent_idealSheaf and included in 𝒪_X by kernel.ι — and the criterion isAmple_of_forall_exists_isZero_h1_idealSheaf then concludes.

public theorem isAmple_of_forall_isZero_h1_quasicoherentIdeal {X : Scheme.{u}} [CompactSpace X]
    (L : X.Modules)
    [hL : AlgebraicGeometry.SheafOfModules.IsInvertible X.toRingedSpace.presheaf
      (structureSheafRing X.toRingedSpace).property L]
    (hvan : ∀ (J : SheafOfModules.{u} (structureSheafRing X.toRingedSpace))
      (ι : J ⟶ SheafOfModules.unit (structureSheafRing X.toRingedSpace)), Mono ι →
      J.IsQuasicoherent → ∃ n : ℕ, 1 ≤ n ∧
        IsZero (((moduleGlobalSections X).rightDerived 1).obj
          ((((Stacks.SheafOfModules.Tensor.sheafTensor
              ⟨((X.toRingedSpace)).presheaf, ((X.toRingedSpace)).IsSheaf⟩).obj (J)).obj
            ((tensorPower X.toRingedSpace.presheaf
              (structureSheafRing X.toRingedSpace).property L (n : ℤ))))))) :
    IsAmple X L

Stacks.ProjectionFormula.isAmple_of_hasEventuallyVanishingH1, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectionFormulaInvertible/AmpleCriterion.lean, line 90. References: EGA III (2.6.1), “c) => a), absolute”.

Let X be a quasi-compact scheme and L an invertible 𝒪_X-module. If for every quasi-coherent sheaf of ideals I ⊆ 𝒪_X there is an n ≥ 1 with H¹(X, I ⊗ L^{⊗ n}) = 0, then L is ample.

Here CompactSpace X is "X is quasi-compact", Stacks.Ample.IsInvertibleModule X L is "L is an invertible 𝒪_X-module", and Stacks.AmpleCohomologicalCriterion.HasEventuallyVanishingH1 X L is the vanishing hypothesis.

theorem isAmple_of_hasEventuallyVanishingH1 (X : Scheme.{u}) [CompactSpace X] (L : X.Modules)
    [Stacks.Ample.IsInvertibleModule X L]
    (h : Stacks.AmpleCohomologicalCriterion.HasEventuallyVanishingH1 X L) :
    Stacks.Ample.IsAmple X L

Tag 0F83, a lemma

Tag 0F83 in the Stacks Project.

Stacks.AffineFromVanishing.isAffineHom_of_forall_isZero_rightDerived_ideal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/AffineFromVanishing.lean, line 165. References: EGA II (5.2.2), “c ⇒ a, c' ⇒ a”.

Stacks Project, Tag 0F83. A quasi-compact morphism between quasi-separated schemes is affine as soon as the first higher direct image of every quasi-coherent sheaf of ideals on the source vanishes.

theorem isAffineHom_of_forall_isZero_rightDerived_ideal
    {X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f]
    [QuasiSeparatedSpace X] [QuasiSeparatedSpace Y]
    (hR₁ : ∀ I : Subobject (SheafOfModules.unit X.ringCatSheaf),
      (Subobject.underlying.obj I).IsQuasicoherent →
        IsZero (((Scheme.Modules.pushforward f).rightDerived 1).obj
          (Subobject.underlying.obj I))) :
    IsAffineHom f

Sources

LeanStacks.SerreCriterion.isAffine_of_forall_isZero_H1_ideal · Stacks.SerreCriterion.isAffine_of_forall_isZero_H1_finiteType_ideal · AlgebraicGeometry.Scheme.Modules.isAmple_of_forall_isZero_h1_quasicoherentIdeal · Stacks.ProjectionFormula.isAmple_of_hasEventuallyVanishingH1 · Stacks.AffineFromVanishing.isAffineHom_of_forall_isZero_rightDerived_ideal

Section30.4 Quasi-coherence of higher direct images #

Section 30.4 of the Stacks Project, Tag 01XH. 6 tags here are carried by 23 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 08DR, a lemma

Tag 08DR in the Stacks Project.

AlgebraicGeometry.baseChangeOverAffineBase_of_affineOpens, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/GlobalBaseChange.lean, line 345. The attribute's comment: “the induction of Stacks 0DJ9 from the affine opens of X to X itself”.

The induction of Stacks 0DJ9 over the quasi-compact opens of X. Granted the affine case and the Mayer--Vietoris step, the conclusion holds for every cartesian square over an affine base: an affine base makes X quasi-compact and quasi-separated, so the induction principle of Stacks 08DR carries the property from the affine opens to all of X.

public theorem baseChangeOverAffineBase_of_affineOpens
    (haffine : BaseChangeAffineOpenCase.{u}) (hstep : BaseChangeMayerVietorisStep.{u}) :
    BaseChangeOverAffineBase.{u}

Stacks.AlgebraicGeometry.CompactOpenInduction.of_isCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CompactOpenInduction/Basic.lean, line 140. The attribute's comment: “induction on quasi-compact opens”.

[Stacks, Tag 08DR], the induction principle. Let X be a quasi-separated scheme and let P be a property of its open subsets such that P holds for every affine open, and such that P (U ⊔ V) holds whenever U is quasi-compact open, V is affine open and P U, P V, P (U ⊓ V) hold. Then P holds for every quasi-compact open of X.

Only the hypothesis P (U ⊓ V) has to be produced beyond what AlgebraicGeometry.compact_open_induction_on already supplies, and U ⊓ V is a quasi-compact open of the affine open V, so of_le_isAffineOpen produces it.

theorem of_isCompact [QuasiSeparatedSpace X] (S : X.Opens) (hS : IsCompact (S : Set X)) : P S

Stacks.AlgebraicGeometry.CompactOpenInduction.top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CompactOpenInduction/Basic.lean, line 153. The attribute's comment: “induction on quasi-compact opens”.

[Stacks, Tag 08DR], the conclusion at X itself. For a quasi-compact quasi-separated scheme, P ⊤ holds.

theorem top [QuasiSeparatedSpace X] [CompactSpace X] : P ⊤

Stacks.AlgebraicGeometry.InductionPrinciple.induction_isCompact_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/InductionPrinciple/Basic.lean, line 169.

[Stacks, Tag 08DR], the Induction Principle. Let X be a quasi-separated scheme and let P be a property of the opens of X which holds for every affine open and which, given a quasi-compact open U and an affine open V, passes from U, V and U ⊓ V to U ⊔ V. Then P holds for every quasi-compact open of X.

The source assumes in addition that X is quasi-compact; that hypothesis is not used for the conclusion about an arbitrary quasi-compact open, and induction_top records the clause of the source that does use it.

theorem induction_isCompact_open [QuasiSeparatedSpace X] (W : X.Opens)
    (hW : IsCompact (W : Set X)) : P W

Stacks.AlgebraicGeometry.InductionPrinciple.induction_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/InductionPrinciple/Basic.lean, line 202. The attribute's comment: “in particular for X”.

[Stacks, Tag 08DR], the clause "and in particular for X". On a quasi-compact quasi-separated scheme the induction principle applies to the whole space.

theorem induction_top [CompactSpace X] [QuasiSeparatedSpace X] : P ⊤

Tag 01XI, a lemma

Tag 01XI in the Stacks Project.

Stacks.Cohomology.AffineCover.isZero_cohomology_of_finite_affine_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/AffineCoverVanishing/Basic.lean, line 184. The attribute's comment: “finite-cover form”.

If X has affine diagonal and is covered by t affine opens, then the cohomology of a quasi-coherent 𝒪_X-module vanishes in every degree at least t.

theorem isZero_cohomology_of_finite_affine_cover (X : Scheme.{u})
    [IsAffineHom (pullback.diagonal (terminal.from X))]
    {t : ℕ} (U : Fin t → X.Opens) (hU : ∀ i, IsAffineOpen (U i))
    (hUcover : ⨆ i, U i = ⊤) (F : X.Modules) [F.IsQuasicoherent] (n : ℕ) (hn : t ≤ n) :
    IsZero (Hgroup X.ringCatSheaf (⊤ : X.Opens) n F)

Stacks.Cohomology.AffineCover.isZero_cohomologyPresheaf_of_affineCoveringNumber_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/AffineCoverVanishing/Basic.lean, line 197. The attribute's comment: “minimal-cover form”.

If X is quasi-compact with affine diagonal — for example if X is separated — then the cohomology of a quasi-coherent 𝒪_X-module vanishes in every degree at least the least number of affine opens needed to cover X.

theorem isZero_cohomologyPresheaf_of_affineCoveringNumber_le (X : Scheme.{u}) [CompactSpace X]
    [IsAffineHom (pullback.diagonal (terminal.from X))]
    [HasExt.{w} (Sheaf (Opens.grothendieckTopology X) AddCommGrpCat.{u})]
    (F : X.Modules) [F.IsQuasicoherent] (n : ℕ)
    (hn : minimalAffineCoverCardinality (⊤ : X.Opens) ≤ n) :
    IsZero ((((SheafOfModules.toSheaf X.ringCatSheaf).obj F).cohomologyPresheaf n).obj
      (op (⊤ : X.Opens)))

AlgebraicGeometry.isZero_cohomology_of_affineCoverNum_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/UniformVanishing/Basic.lean, line 220.

Stacks Project, Tag 01XI. Let X be a quasi-compact scheme with affine diagonal — for instance a separated scheme — and let t = t(X) be the minimal number of affine opens needed to cover X. Then H^p(X, F) = 0 for every p ≥ t and every quasi-coherent 𝒪_X-module F.

theorem isZero_cohomology_of_affineCoverNum_le (X : Scheme.{u}) [CompactSpace X]
    [IsAffineHom (pullback.diagonal (terminal.from X))] (F : X.Modules) [F.IsQuasicoherent]
    (p : ℕ) (hp : X.affineCoverNum ⊤ ≤ p) :
    IsZero (Hgroup X.ringCatSheaf ⊤ p F)

Stacks.Cohomology.FiniteCover.isZero_Hgroup_of_finite_affine_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EulerCharVanishing/Basic.lean, line 197. The attribute's comment: “finite-cover form”.

[Stacks, Tag 01XI], finite-cover form. On a scheme with affine diagonal covered by t affine opens, the cohomology of a quasi-coherent module vanishes in every degree at least t.

This is the library-spelling counterpart of isZero_H'_of_finite_affine_cover. The tag's own phrasing bounds the degree by the minimal number of affine opens needed to cover the scheme; that follows from this by applying it to a cover realizing the minimum, and is not stated here because the affine covering number has no name in the library yet.

theorem isZero_Hgroup_of_finite_affine_cover
    [IsAffineHom (pullback.diagonal (terminal.from X))] (F : X.Modules) [F.IsQuasicoherent]
    {t : ℕ} (U : Fin t → X.Opens) (hU : ∀ i, IsAffineOpen (U i)) (W : X.Opens)
    (hcover : ⨆ i, U i = W) (n : ℕ) (hn : t ≤ n) :
    IsZero (Hgroup X.ringCatSheaf W n F)

Declarations registered for the tag:

AlgebraicGeometry.minimalAffineCoverCardinality, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Cohomology/AffineCoverVanishing/CoveringNumber.lean, line 52 (StacksFrontier): “affine covering number”.

Tag 0BDY, a lemma

Tag 0BDY in the Stacks Project.

Stacks.Cohomology.QcohDelta.exists_mono_isZero_hfunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/QcohUniversalDeltaFunctor.lean, line 165. The attribute's comment: “part (1): the embedding with vanishing higher cohomology”.

Stacks 0BDY, part (1). On a quasi-compact scheme with affine diagonal every quasi-coherent 𝒪_X-module ℱ admits an embedding ℱ → ℱ' into a quasi-coherent module with Hᵖ(X, ℱ') = 0 for all p ≥ 1.

Take ℱ' = ∏ᵢ (ιᵢ)_*(ℱ|_{Uᵢ}) for a finite affine open cover X = ⋃ Uᵢ: each ιᵢ is affine because the diagonal of X is, so ℱ' is quasi-coherent and its cohomology is the product of the cohomologies of the ℱ|_{Uᵢ} on the affine schemes Uᵢ, which vanish in positive degrees.

theorem exists_mono_isZero_hfunctor (X : Scheme.{u}) [CompactSpace X]
    [IsAffineHom (pullback.diagonal (terminal.from X))]
    (F : (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory) :
    ∃ (G : (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory) (φ : F ⟶ G),
      Mono ((ObjectProperty.ι (SheafOfModules.isQuasicoherent X.ringCatSheaf)).map φ) ∧
        ∀ p : ℕ, 0 < p → IsZero ((Hfunctor X.ringCatSheaf ⊤ p).obj G.obj)

Stacks.Cohomology.QcohDelta.cohomologyDeltaFunctor_isUniversal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/QcohUniversalDeltaFunctor.lean, line 235. The attribute's comment: “part (2): universality of the delta-functor”.

Stacks 0BDY, part (2). On a quasi-compact scheme with affine diagonal the cohomology functors {Hⁿ(X, -)}_{n ≥ 0} form a universal δ-functor from QCoh(𝒪_X) to Ab.

Part (1) effaces every positive-degree component, and an effaceable δ-functor is universal.

theorem cohomologyDeltaFunctor_isUniversal [CompactSpace X]
    [IsAffineHom (pullback.diagonal (terminal.from X))] :
    (cohomologyDeltaFunctor X).IsUniversal

Tag 071L, a lemma

Tag 071L in the Stacks Project.

Stacks.Cohomology.AffineCover.isZero_cohomology_of_degree_ge_separatedCoverBound, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/AffineCoverVanishing/SeparatedCover.lean, line 271.

Let X be a quasi-compact quasi-separated scheme and let X = U₁ ∪ … ∪ Uₙ be an open covering by quasi-compact separated opens — for example affine ones. If d = max_{I} (|I| + t(⋂_{i ∈ I} Uᵢ) - 1), where t is the affine covering number, then the cohomology of every quasi-coherent 𝒪_X-module vanishes in every degree at least d.

theorem isZero_cohomology_of_degree_ge_separatedCoverBound {X : Scheme.{u}} [CompactSpace X]
    [QuasiSeparatedSpace X]
    [HasExt.{w} (Sheaf (Opens.grothendieckTopology X) AddCommGrpCat.{u})]
    {n d : ℕ} (U : Fin n → X.Opens) (hU : ⨆ i, U i = ⊤)
    (hU_compact : ∀ i, IsCompact (U i : Set X))
    (hU_separated : ∀ i, Scheme.IsSeparated (U i : Scheme))
    (hd : d = Finset.univ.sup fun I : Finset (Fin n) ↦
      I.card + minimalAffineCoverCardinality (⨅ i ∈ I, U i) - 1)
    (F : X.Modules) [F.IsQuasicoherent] (p : ℕ) (hp : d ≤ p) :
    IsZero ((((SheafOfModules.toSheaf X.ringCatSheaf).obj F).cohomologyPresheaf p).obj
      (op (⊤ : X.Opens)))

AlgebraicGeometry.isZero_cohomology_of_coverDegreeBound_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/UniformVanishing/Basic.lean, line 290.

Stacks Project, Tag 071L. Let X be a quasi-compact quasi-separated scheme and let X = U 1 ∪ … ∪ U n be an open covering with each U i quasi-compact and with affine diagonal — for instance separated, or affine. Set

d = max { |I| + t(⋂_{i ∈ I} U i) - 1 : ∅ ≠ I ⊆ {1, …, n} },

the AlgebraicGeometry.Scheme.coverDegreeBound of the covering, where t(U) is the minimal number of affine opens needed to cover U. Then H^p(X, F) = 0 for all p ≥ d and every quasi-coherent 𝒪_X-module F.

theorem isZero_cohomology_of_coverDegreeBound_le [CompactSpace X] [QuasiSeparatedSpace X]
    (F : X.Modules) [F.IsQuasicoherent] {n : ℕ} (U : Fin n → X.Opens) (hcov : ⨆ i, U i = ⊤)
    (hUc : ∀ i, IsCompact (U i : Set X))
    (hUinf : ∀ (i : Fin n) (A B : X.Opens), A ≤ U i → B ≤ U i → IsAffineOpen A →
      IsAffineOpen B → IsAffineOpen (A ⊓ B))
    (p : ℕ) (hp : X.coverDegreeBound U ≤ p) :
    IsZero (Hgroup X.ringCatSheaf ⊤ p F)

AlgebraicGeometry.isZero_cohomology_of_coverDegreeBound_le_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/UniformVanishing/Basic.lean, line 303.

Stacks Project, Tag 071L, with the covering hypothesis in the source's form: each U i is quasi-compact and separated.

theorem isZero_cohomology_of_coverDegreeBound_le_of_isSeparated [CompactSpace X]
    [QuasiSeparatedSpace X] (F : X.Modules) [F.IsQuasicoherent] {n : ℕ} (U : Fin n → X.Opens)
    (hcov : ⨆ i, U i = ⊤) (hUc : ∀ i, IsCompact (U i : Set X))
    (hUsep : ∀ i, (U i).toScheme.IsSeparated)
    (p : ℕ) (hp : X.coverDegreeBound U ≤ p) :
    IsZero (Hgroup X.ringCatSheaf ⊤ p F)

Tag 01XJ, a lemma

Tag 01XJ in the Stacks Project.

Stacks.AlgebraicGeometry.HigherDirectImageQcoh.isQuasicoherent_higherDirectImage, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/HigherDirectImageQcqs/Qcqs.lean, line 485. The attribute's comment: “quasicoherence”. References: EGA III (1.4.10), “more general”.

Stacks Project, Tag 01XJ (quasicoherence). The higher direct images of a quasi-coherent module under a quasi-compact and quasi-separated morphism of schemes are quasi-coherent.

instance isQuasicoherent_higherDirectImage {X S : Scheme.{u}} (f : X ⟶ S)
    [QuasiCompact f] [QuasiSeparated f] (F : X.Modules) [F.IsQuasicoherent] (p : ℤ) :
    (((Scheme.Modules.pushforward f).rightDerivedPlus p).obj F).IsQuasicoherent

Stacks.AlgebraicGeometry.HigherDirectImageQcoh.exists_isZero_rightDerived_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/HigherDirectImageQcqs/UniformVanishing.lean, line 439. The attribute's comment: “uniform_vanishing”.

For a quasi-compact and quasi-separated morphism of schemes whose target is quasi-compact there is an integer, depending on the morphism alone, above which every higher direct image of every quasi-coherent module vanishes.

theorem exists_isZero_rightDerived_pushforward {X S : Scheme.{u}} (f : X ⟶ S)
    [QuasiCompact f] [QuasiSeparated f] [CompactSpace S] :
    ∃ n : ℤ, ∀ p : ℤ, n ≤ p → ∀ (F : X.Modules) [F.IsQuasicoherent],
      IsZero (((Scheme.Modules.pushforward f).rightDerivedPlus p).obj F)

Stacks.AlgebraicGeometry.HigherDirectImageQcoh.exists_isZero_rightDerivedNat_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/HigherDirectImageQcqs/UniformVanishing.lean, line 562. The attribute's comment: “uniform_vanishing”. References: EGA IV (1.7.21), “vanishing bound”; EGA III (1.4.12), “existence of r”.

For a quasi-compact and quasi-separated morphism of schemes whose target is quasi-compact there is a natural number, depending on the morphism alone, above which (Rⁿ f_*) F vanishes for every quasi-coherent module F, where Rⁿ f_* is Mathlib's ℕ-indexed CategoryTheory.Functor.rightDerived (Scheme.Modules.pushforward f) n.

theorem exists_isZero_rightDerivedNat_pushforward {X S : Scheme.{u}} (f : X ⟶ S)
    [QuasiCompact f] [QuasiSeparated f] [CompactSpace S] :
    ∃ N : ℕ, ∀ F : X.Modules, F.IsQuasicoherent → ∀ n : ℕ, N ≤ n →
      IsZero (((Scheme.Modules.pushforward f).rightDerived n).obj F)

Stacks.AlgebraicGeometry.HigherDirectImageQcoh.exists_isZero_rightDerivedPlus_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/HigherDirectImageQcqs/UniformVanishing.lean, line 586. The attribute's comment: “uniform_vanishing”.

For a quasi-compact and quasi-separated morphism of schemes whose target is quasi-compact there is an integer, depending on the morphism alone, above which every higher direct image of every quasi-coherent module vanishes, for the ℤ-indexed right derived functors at an arbitrary model of the bounded below derived category.

theorem exists_isZero_rightDerivedPlus_pushforward {X S : Scheme.{u}} (f : X ⟶ S)
    [QuasiCompact f] [QuasiSeparated f] [CompactSpace S]
    [HasDerivedCategory.{w} X.Modules] [HasDerivedCategory.{w'} S.Modules] :
    ∃ N : ℤ, ∀ p : ℤ, N ≤ p → ∀ F : X.Modules, F.IsQuasicoherent →
      IsZero (((Scheme.Modules.pushforward f).rightDerivedPlus p).obj F)

Stacks.AlgebraicGeometry.Tag01XJQcohInduction.higherDirectImage_isQuasicoherent, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QcohInduction/Basic.lean, line 332. The attribute's comment: “quasicoherence”. References: EGA III (6.2.3), “special case”.

Stacks Project, Tag 01XJ (quasicoherence). The higher direct images of a quasi-coherent module under a quasi-compact and quasi-separated morphism of schemes are quasi-coherent.

Quasi-coherence is local on the base (Stacks.AlgebraicGeometry.HigherDirectImageQcoh.isQuasicoherent_rightDerivedPlus_of_affineOpens, which is [Stacks, Tag 01E5] for schemes), and f ∣_ V is again quasi-compact and quasi-separated with affine target, so the statement reduces to isQuasicoherent_rightDerivedPlus_of_isAffine.

instance higherDirectImage_isQuasicoherent (f : X ⟶ S) [QuasiCompact f] [QuasiSeparated f]
    (F : X.Modules) [F.IsQuasicoherent] (p : ℤ) :
    (((Scheme.Modules.pushforward f).rightDerivedPlus p).obj F).IsQuasicoherent

Stacks.AlgebraicGeometry.Tag01XJUniformVanishing.exists_isZero_rightDerived_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/UniformVanishing/Basic.lean, line 383. The attribute's comment: “uniform_vanishing”. References: EGA IV (1.7.21), “vanishing bound”; EGA III (1.4.12), “existence of r”.

Stacks Project, Tag 01XJ (uniform_vanishing). Let f : X ⟶ S be a quasi-compact and quasi-separated morphism of schemes with S quasi-compact. Then there is an integer n, depending only on f, such that R ᵖ f_* F = 0 for every p ≥ n and every quasi-coherent 𝒪_X-module F.

S is covered by finitely many affine opens B j (exists_fin_affineOpen_cover), each f ∣_ B j is again quasi-compact and quasi-separated with affine target, so exists_isZero_rightDerived_pushforward_of_isAffine supplies a bound n j; the bound is ⨆ j, (n j).toNat. Above it every restriction of R ᵖ f_* F to a B j vanishes — by [Stacks, Tag 01E5] for schemes, higherDirectImageRestrictObjIso — and vanishing is local, isZero_of_isZero_restrict.

theorem exists_isZero_rightDerived_pushforward (f : X ⟶ S) [QuasiCompact f] [QuasiSeparated f]
    [CompactSpace S] :
    ∃ n : ℤ, ∀ (p : ℤ), n ≤ p → ∀ (F : X.Modules) [F.IsQuasicoherent],
      IsZero (((Scheme.Modules.pushforward f).rightDerivedPlus p).obj F)

AlgebraicGeometry.exists_uniform_isZero_rightDerived_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/UniformVanishingDirectImage/Basic.lean, line 243. The attribute's comment: “base_change_uniform_vanishing”. References: EGA IV (1.7.21), “base change vanishing”; EGA III (1.4.12), “existence of r”.

Stacks Project, Tag 01XJ (3). Let f : X ⟶ S be a quasi-compact and quasi-separated morphism of schemes with S quasi-compact. There is an integer n = n(X, S, f) such that for every morphism g : S' ⟶ S the base change f' : X' = X ×_S S' ⟶ S' satisfies R ᵖ f'_* F' = 0 for every p ≥ n and every quasi-coherent module F' on X'.

theorem exists_uniform_isZero_rightDerived_pushforward {X S : Scheme.{u}} (f : X ⟶ S)
    [QuasiCompact f] [QuasiSeparated f] [CompactSpace S] :
    ∃ n : ℤ, ∀ (S' : Scheme.{u}) (g : S' ⟶ S) (F : (pullback f g).Modules) [F.IsQuasicoherent],
      ∀ p : ℤ, n ≤ p →
        IsZero (((Scheme.Modules.pushforward (pullback.snd f g)).rightDerivedPlus p).obj F)

Tag 01XK, a lemma

Tag 01XK in the Stacks Project.

Stacks.Cohomology.AffineBase.cohomologyIsoGlobalSectionsRightDerivedPushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineCohomologyVanishing/AffineBase.lean, line 262. References: EGA III (1.4.14), “affine base, Z=point”.

[Stacks, Tag 01XK]. For a quasi-compact and quasi-separated morphism f : X ⟶ S with affine target, the cohomology of a quasi-coherent module on X is naturally isomorphic, as a module over Γ(S, ⊤), to the global sections of its higher direct image.

public noncomputable def cohomologyIsoGlobalSectionsRightDerivedPushforward (q : ℤ) :
    (SheafOfModules.isQuasicoherent X.ringCatSheaf).ι ⋙
        (moduleGlobalSections X).rightDerivedPlus q ⋙
        ModuleCat.restrictScalars f.appTop.hom ≅
      (SheafOfModules.isQuasicoherent X.ringCatSheaf).ι ⋙
        (AlgebraicGeometry.Scheme.Modules.pushforward f).rightDerivedPlus q ⋙
        moduleGlobalSections S

Stacks.Cohomology.AffineBase.cohomologyIsoSectionsRightDerivedPushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/AffineBase.lean, line 149. References: EGA III (1.4.14), “affine base, Z=point”.

Let f : X ⟶ S be a quasi-compact and quasi-separated morphism of schemes with S affine. For every q : ℤ the cohomology H^q(X, F) of a quasi-coherent 𝒪_X-module F, regarded as a Γ(S, 𝒪_S)-module by restriction of scalars along f^\# : Γ(S, 𝒪_S) ⟶ Γ(X, 𝒪_X), is the module of global sections of the higher direct image R^qf_*F, naturally in F.

def cohomologyIsoSectionsRightDerivedPushforward (q : ℤ) :
    quasicoherentInclusion X ⋙
        (sectionsFunctor X ⊤).rightDerivedPlus q ⋙ ModuleCat.restrictScalars f.appTop.hom ≅
      quasicoherentInclusion X ⋙
        (Scheme.Modules.pushforward f).rightDerivedPlus q ⋙ sectionsFunctor S ⊤

Sources

LeanAlgebraicGeometry.baseChangeOverAffineBase_of_affineOpens · Stacks.AlgebraicGeometry.CompactOpenInduction.of_isCompact · Stacks.AlgebraicGeometry.CompactOpenInduction.top · Stacks.AlgebraicGeometry.InductionPrinciple.induction_isCompact_open · Stacks.AlgebraicGeometry.InductionPrinciple.induction_top · Stacks.Cohomology.AffineCover.isZero_cohomology_of_finite_affine_cover · Stacks.Cohomology.AffineCover.isZero_cohomologyPresheaf_of_affineCoveringNumber_le · AlgebraicGeometry.isZero_cohomology_of_affineCoverNum_le

Section30.5 Cohomology and base change, I #

Section 30.5 of the Stacks Project, Tag 02KE. 4 tags here are carried by 12 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02KF, an equation

Tag 02KF in the Stacks Project.

AlgebraicGeometry.BaseChangeDiagram, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/EulerChar/BaseChange.lean, line 54. The attribute's comment: “the cartesian square and quasi-coherent module”.

Stacks Project, Tag 02KF. The base-change diagram: a cartesian square of schemes, together with the quasi-coherent module 𝓕 on X.

structure BaseChangeDiagram

AlgebraicGeometry.BaseChangeDiagram.pulledBack, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/EulerChar/BaseChange.lean, line 71. The attribute's comment: “the pulled-back module”.

The module 𝓕' = (g')^*𝓕 in the base-change diagram.

noncomputable abbrev pulledBack (d : BaseChangeDiagram) : d.X'.Modules

AlgebraicGeometry.BaseChangeDiagram.derivedPushforward, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/EulerChar/BaseChange.lean, line 76. The attribute's comment: “the lower-right derived direct image”.

The total derived direct image Rf_*𝓕 in the base-change diagram.

noncomputable abbrev derivedPushforward (d : BaseChangeDiagram) :
    DerivedCategory.Plus d.S.Modules

AlgebraicGeometry.BaseChangeDiagram.derivedPushforward', an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/EulerChar/BaseChange.lean, line 83. The attribute's comment: “the lower-left derived direct image”.

The total derived direct image Rf'_*𝓕' in the base-change diagram.

noncomputable abbrev derivedPushforward' (d : BaseChangeDiagram) :
    DerivedCategory.Plus d.S'.Modules

Tag 02KG, a lemma

Tag 02KG in the Stacks Project.

Stacks.AlgebraicGeometry.AffineBaseChangeIso.isIso_baseChangeNatTrans_of_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineBaseChangeIso/Reduction.lean, line 176. The attribute's comment: “affine base change”.

The base-change assertion of Stacks Tag 02KG. The base-change morphism of a cartesian square of schemes whose right-hand morphism is affine is invertible at every quasi-coherent module.

theorem isIso_baseChangeNatTrans_of_isAffineHom (hw : IsPullback g' f' f g) [IsAffineHom f]
    (F : X.Modules) [F.IsQuasicoherent] :
    IsIso ((AffinePushforward.baseChangeNatTrans hw.w).app F)

Stacks.AlgebraicGeometry.AffinePushforward.pushforward_isQuasicoherent_of_isAffineHom, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffinePushforward/Basic.lean, line 251. The attribute's comment: “quasi-coherence of the direct image”.

Stacks Project, Tag 02KG. The direct image of a quasi-coherent module along an affine morphism is quasi-coherent.

instance pushforward_isQuasicoherent_of_isAffineHom {X S : Scheme.{u}} (f : X ⟶ S)
    (F : X.Modules) [IsAffineHom f] [F.IsQuasicoherent] :
    ((Scheme.Modules.pushforward f).obj F).IsQuasicoherent

Stacks.Tag02KGDerivedComparison.isIso_rightDerivedFunctorPlusUnit_app_of_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedComparison/Basic.lean, line 83. The attribute's comment: “comparison with the derived direct image”. References: EGA III (1.3.2).

[Stacks, Tag 02KG], comparison with the derived direct image. For an affine morphism f : X ⟶ S of schemes and a quasi-coherent 𝒪_X-module F, the canonical map from the ordinary direct image f_* F, placed in degree zero, to the total derived direct image R f_*(F[0]) is an isomorphism. Equivalently: a quasi-coherent module has no higher direct images along an affine morphism, so the unit of R f_* is already invertible on degree-zero complexes.

This is Stacks.AffineHigherDirectImage.rightAcyclic_pushforward, [Stacks, Tag 01XC], read at the unfolding of CategoryTheory.Functor.rightAcyclic.

theorem isIso_rightDerivedFunctorPlusUnit_app_of_isAffineHom
    {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) [IsAffineHom f] [F.IsQuasicoherent] :
    IsIso ((Scheme.Modules.pushforward f).rightDerivedFunctorPlusUnith.app
      ((HomotopyCategory.Plus.singleFunctor X.Modules 0).obj F))

Tag 02KH, a lemma

Tag 02KH in the Stacks Project.

Stacks.AlgebraicGeometry.FlatBaseChangeDerived.isIso_baseChangeMap_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FlatBaseChangeCohomology/Derived/FlatBaseChange.lean, line 76. The attribute's comment: “part (1): the base change map of Tag 02N7 is an isomorphism in D⁺(𝒪_{S'}), hence in every degree i”.

Flat base change in the derived category ([Stacks, Tag 02KH], part (1)). For a cartesian square of schemes with g flat and f quasi-compact and quasi-separated, and a quasi-coherent 𝒪_X-module ℱ, the base change map g^* Rf_* ℱ ⟶ Rf'_* (g')^* ℱ of [Stacks, Tag 02N7] is an isomorphism in D⁺(𝒪_{S'}). Taking cohomology sheaves, the base change maps g^* R^i f_* ℱ ⟶ R^i f'_* (g')^* ℱ are isomorphisms for every i (isIso_higherBaseChangeMap).

theorem isIso_baseChangeMap_of_flat (H : IsPullback g' f' f g) [Flat g] [QuasiCompact f]
    [QuasiSeparated f] (F : X.Modules) [F.IsQuasicoherent] :
    IsIso ((Stacks.Cohomology.FlatBaseChange.baseChangeMap f.toLRSHom.toShHom
      f'.toLRSHom.toShHom g.toLRSHom.toShHom g'.toLRSHom.toShHom
      (congrArg (fun h => h.toLRSHom.toShHom) H.w) (isFlat_toShHom g)
      (isFlat_toShHom_of_isPullback H)).app ((DerivedCategory.Plus.singleFunctor _ 0).obj F))

Stacks.AlgebraicGeometry.FlatBaseChangeDerived.isIso_higherBaseChangeMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FlatBaseChangeCohomology/Derived/FlatBaseChange.lean, line 118. The attribute's comment: “part (1), in each degree i”.

[Stacks, Tag 02KH], part (1). For a cartesian square of schemes with g flat and f quasi-compact and quasi-separated, and a quasi-coherent 𝒪_X-module ℱ, the base change map g^* R^i f_* ℱ ⟶ R^i f'_* (g')^* ℱ is an isomorphism for every i.

theorem isIso_higherBaseChangeMap (H : IsPullback g' f' f g) [Flat g] [QuasiCompact f]
    [QuasiSeparated f] (F : X.Modules) [F.IsQuasicoherent] (i : ℤ) :
    IsIso (higherBaseChangeMap H F i)

Stacks.AlgebraicGeometry.FlatBaseChangeDerived.cohomologyBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FlatBaseChangeCohomology/Derived/FlatBaseChange.lean, line 169. The attribute's comment: “part (2)”.

[Stacks, Tag 02KH], part (2). For a cartesian square of schemes with S and S' affine, g flat and f quasi-compact and quasi-separated, and a quasi-coherent 𝒪_X-module ℱ,

H^i(X, ℱ) ⊗_{Γ(S, 𝒪_S)} Γ(S', 𝒪_{S'}) ≅ H^i(X', (g')^* ℱ)

as Γ(S', 𝒪_{S'})-modules, for every i. The isomorphism is the one given by the base change map of [Stacks, Tag 02N7]: it is the global sections over S' of the isomorphism g^* R^i f_* ℱ ≅ R^i f'_* (g')^* ℱ of part (1), read through the identifications H^i(X, ℱ) = Γ(S, R^i f_* ℱ) of [Stacks, Tag 01XK] (for f and for f') and Γ(S', g^* 𝒢) = Γ(S, 𝒢) ⊗_{Γ(S, 𝒪_S)} Γ(S', 𝒪_{S'}) for the quasi-coherent 𝒢 = R^i f_* ℱ ([Stacks, Tag 01XJ]).

def cohomologyBaseChangeIso (H : IsPullback g' f' f g) [IsAffine S] [IsAffine S'] [Flat g]
    [QuasiCompact f] [QuasiSeparated f] (F : X.Modules) [F.IsQuasicoherent] (i : ℤ) :
    (ModuleCat.extendScalars g.appTop.hom).obj (cohomologyOver f F i) ≅
      cohomologyOver f' ((Scheme.Modules.pullback g').obj F) i

Tag 0CKW, a lemma

Tag 0CKW in the Stacks Project.

Stacks.Tag0CKW.isIso_cohomologyBaseChangeMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FlatBaseChangeCohomology/FiniteLocallyFreeCanonical.lean, line 861.

Finite locally free base change. For a cartesian square of schemes
Y --p--> X
|        |
k        iX
v        v
T --q--> S
with S = Spec A and T = Spec B affine and q finite locally free, and for every quasi-coherent 𝒪_X-module F and every n, the canonical map Hⁿ(X, F) ⊗_A B ⟶ Hⁿ(Y, p^* F), x ⊗ b ↦ b • p^* x, is an isomorphism of B-modules, for an arbitrary scheme X.

The map is cohomologyBaseChangeMap, the B-linear extension of the pullback map cohomologyPullback.

theorem isIso_cohomologyBaseChangeMap [Stacks.Morphisms.IsFiniteLocallyFree q]
    (F : X.Modules) [F.IsQuasicoherent] (n : ℕ) :
    IsIso (cohomologyBaseChangeMap H F n)

Stacks.Tag0CKW.isIso_cohomologyBaseChangeMap_of_isFiniteLocallyFree_module, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FlatBaseChangeCohomology/FiniteLocallyFreeCanonical.lean, line 883. The attribute's comment: “as stated: B a finite locally free A-module”.

Finite locally free base change. Let φ : A ⟶ B be a ring map making B a finite locally free A-module, and consider a cartesian square of schemes
Y ------p-----> X
|               |
k               iX
v               v
Spec B --> Spec A
with bottom arrow Spec φ. For every quasi-coherent 𝒪_X-module F and every n, the canonical map Hⁿ(X, F) ⊗_A B ⟶ Hⁿ(Y, p^* F), x ⊗ b ↦ b • p^* x, is an isomorphism of B-modules; here A and B act through Γ(Spec A, 𝒪) and Γ(Spec B, 𝒪), and X is an arbitrary scheme.

theorem isIso_cohomologyBaseChangeMap_of_isFiniteLocallyFree_module {A B : CommRingCat.{u}}
    (φ : A ⟶ B) {X Y : Scheme.{u}} {iX : X ⟶ Spec A} {p : Y ⟶ X} {k : Y ⟶ Spec B}
    (H : IsPullback p k iX (Spec.map φ))
    (hB : letI := φ.hom.toAlgebra; Module.IsFiniteLocallyFree A B)
    (F : X.Modules) [F.IsQuasicoherent] (n : ℕ) :
    IsIso (cohomologyBaseChangeMap H F n)

Sources

LeanAlgebraicGeometry.BaseChangeDiagram · AlgebraicGeometry.BaseChangeDiagram.pulledBack · AlgebraicGeometry.BaseChangeDiagram.derivedPushforward · AlgebraicGeometry.BaseChangeDiagram.derivedPushforward' · Stacks.AlgebraicGeometry.AffineBaseChangeIso.isIso_baseChangeNatTrans_of_isAffineHom · Stacks.AlgebraicGeometry.AffinePushforward.pushforward_isQuasicoherent_of_isAffineHom · Stacks.Tag02KGDerivedComparison.isIso_rightDerivedFunctorPlusUnit_app_of_isAffineHom · Stacks.AlgebraicGeometry.FlatBaseChangeDerived.isIso_baseChangeMap_of_flat

Section30.6 Colimits and higher direct images #

Section 30.6 of the Stacks Project, Tag 07TA. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07TB, a lemma

Tag 07TB in the Stacks Project.

Stacks.Cohomology.SchemeColimits.higherDirectImage_preservesFilteredColimits, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/ColimitsHigherDirect/HigherDirectImage.lean, line 399.

For a quasi-compact and quasi-separated morphism of schemes, its p-th higher direct image functor on sheaves of abelian groups preserves all filtered colimits.

instance higherDirectImage_preservesFilteredColimits
    {X S : AlgebraicGeometry.Scheme.{u}} (f : X ⟶ S)
    [AlgebraicGeometry.QuasiCompact f] [AlgebraicGeometry.QuasiSeparated f] (p : ℕ) :
    PreservesFilteredColimits
      ((TopCat.Sheaf.pushforward AddCommGrpCat.{u} f.base).rightDerived p)

Sources

LeanStacks.Cohomology.SchemeColimits.higherDirectImage_preservesFilteredColimits

Section30.7 Cohomology and base change, II #

Section 30.7 of the Stacks Project, Tag 071M. 4 tags here are carried by 17 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01XL, a lemma

Tag 01XL in the Stacks Project.

Stacks.AlgebraicGeometry.Tag01XLDerivedIso.relativeCechIsoDerivedPushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedIso/Leray.lean, line 275. The attribute's comment: “the derived isomorphism”.

The relative Čech complex of [Stacks, Tag 01XL] computes Rf_*ℱ. In D⁺(S),

Č ⁼(𝒰, f, ℱ) ≅ Rf_*ℱ,

functorially in the quasi-coherent 𝒪_X-module ℱ. The hypotheses are those of [Stacks, Tag 01XL]: T a finite affine open cover of X — so X is quasi-compact and covered by finitely many affine opens — and X, S of affine diagonal. Nothing is assumed about f.

This is relativeCechComputesDerivedPushforward composed with the resolution ℱ[0] ≅ 𝔠 ⁼(𝒰, ℱ) of [Stacks, Tag 02FU].

noncomputable def relativeCechIsoDerivedPushforward (f : X ⟶ S) (T : X.AffineOpenCover.{u, u})
    [Fintype T.I₀]
    [IsAffineHom (pullback.diagonal (terminal.from X))]
    [IsAffineHom (pullback.diagonal (terminal.from S))] :
    relativeCechComplex f T ⋙ HomotopyCategory.Plus.quotient S.Modules ⋙
        DerivedCategory.Plus.Qh ≅
      ObjectProperty.ι (SheafOfModules.isQuasicoherent X.ringCatSheaf) ⋙
        DerivedCategory.Plus.singleFunctor X.Modules 0 ⋙
          (Scheme.Modules.pushforward f).rightDerivedFunctorPlus

Stacks.AlgebraicGeometry.RelativeCech.relativeCechPresheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeCech/Basic.lean, line 329. The attribute's comment: “the coefficient presheaf”.

The coefficient presheaf of the relative Čech complex of Tag 01XL: the functor sending a quasi-coherent 𝒪_X-module F to the presheaf on Over X whose value at A, with structure morphism a, is (a ≫ f)_* a^* F, with the canonical restriction maps.

public noncomputable def relativeCechPresheaf (f : X ⟶ S) :
    (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory ⥤
      ((Over X)ᵒᵖ ⥤ S.Modules)

Stacks.AlgebraicGeometry.RelativeCechComplex.relativeCechComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeCechComplex/Basic.lean, line 72. The attribute's comment: “the complex”.

The bounded-below relative Čech complex of a finite affine open cover (Stacks 01XL). The alternating Čech complex, for the family Over.mk (T.f i) in Over X, of the coefficient presheaf of f, extended from ℕ-indexing to ℤ-indexing and regarded as a bounded-below complex.

public noncomputable def relativeCechComplex (f : X ⟶ S) (T : X.AffineOpenCover)
    [Fintype T.I₀] :
    (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory ⥤
      CochainComplex.Plus S.Modules

Stacks.AlgebraicGeometry.RelativeCechComplex.relativeCechComplex_obj_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeCechComplex/Quasicoherent.lean, line 113. The attribute's comment: “quasi-coherence of the terms”. References: EGA III (1.4.9), “affine diagonal”.

Stacks Project, Tag 01XL: every term of the relative Čech complex of a finite affine open cover is a quasi-coherent 𝒪_S-module.

public theorem relativeCechComplex_obj_isQuasicoherent (f : X ⟶ S) (T : X.AffineOpenCover)
    [Fintype T.I₀]
    [IsAffineHom (pullback.diagonal (terminal.from X))]
    [IsAffineHom (pullback.diagonal (terminal.from S))]
    (F : (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory) (p : ℤ) :
    (((relativeCechComplex f T).obj F).obj.X p).IsQuasicoherent

Tag 01XM, a lemma

Tag 01XM in the Stacks Project.

Stacks.AlgebraicGeometry.RelativeCechBaseChange.baseChangeRelativeCechIsoDerivedPushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeCechComplex/BaseChangeDerived.lean, line 308. The attribute's comment: “the canonical isomorphism”.

[Stacks, Tag 01XM], the canonical isomorphism. For a cartesian square
X' --g'--> X
|f'        |f
S' --g-->  S
with X and S of affine diagonal, a finite affine open cover 𝒰 of X and a quasi-coherent 𝒪_X-module ℱ, there is a canonical isomorphism

g^* Č ⁼(𝒰, f, ℱ) ≅ Rf'_* (g')^*ℱ

in D⁺(S'): the termwise inverse image of the relative Čech complex is the relative Čech complex of the cover X' = ⋃ Uᵢ ×_X X' (the base change map of [Stacks, Tag 02KG] on each finite intersection), whose finite intersections are affine over X' and over S', so that it computes Rf'_* as in [Stacks, Tag 01XL].

noncomputable def baseChangeRelativeCechIsoDerivedPushforward :
    DerivedCategory.Plus.Qh.obj ((HomotopyCategory.Plus.quotient S'.Modules).obj
        ((Scheme.Modules.pullback g).mapCochainComplexPlus.obj
          ((relativeCechComplex f T).obj F))) ≅
      (Scheme.Modules.pushforward f').rightDerivedFunctorPlus.obj
        ((DerivedCategory.Plus.singleFunctor X'.Modules 0).obj
          ((Scheme.Modules.pullback g').obj F.obj))

Stacks.AlgebraicGeometry.RelativeCechBaseChange.baseChangeRelativeCechComplexIsoOfIsAffineHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeCechComplex/BaseChangeDerived.lean, line 358. The attribute's comment: “the affine case”.

[Stacks, Tag 01XM], the affine case. For a cartesian square as in baseChangeRelativeCechIsoDerivedPushforward with g : S' ⟶ S affine, the members U'ᵢ = (g')^{-1}(Uᵢ) = Uᵢ ×_X X' of the inverse-image cover 𝒰' are affine, and the termwise inverse image of the relative Čech complex is the relative Čech complex of this affine open cover:

g^* Č ⁼(𝒰, f, ℱ) ≅ Č ⁼(𝒰', f', (g')^*ℱ)

as bounded below complexes of 𝒪_{S'}-modules.

noncomputable def baseChangeRelativeCechComplexIsoOfIsAffineHom [IsAffineHom g] :
    letI : IsAffineHom g' := MorphismProperty.of_isPullback hw.flip inferInstance
    (Scheme.Modules.pullback g).mapCochainComplexPlus.obj ((relativeCechComplex f T).obj F) ≅
      (relativeCechComplex f' (inverseImageAffineOpenCover g' T)).obj (pullbackQcohObj g' F)

Tag 01XN, a lemma

Tag 01XN in the Stacks Project.

Stacks.AlgebraicGeometry.UniversalPushforward.universalPushforwardComplexOfQuasiSeparated, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeCechComplex/HypercoveringDerivedPushforward.lean, line 373.

Stacks Project, Tag 01XN. Let f : X ⟶ S be a quasi-compact and quasi-separated morphism of schemes with S quasi-compact and separated, and let 𝓕 be a quasi-coherent 𝒪_X-module. There is a bounded below complex 𝓚⁼ of quasi-coherent 𝒪_S-modules such that for every morphism g : S' ⟶ S the complex g^*𝓚⁼ represents Rf'_*𝓕' in D⁺(S'), with the notation of the cartesian square of [Stacks, Tag 02KF].

The complex is 𝓚⁼(K, f, 𝓕) = ( ∏_{i ∈ I₀} f_{i,*}𝓕|_{U_i} ⟶ ∏_{i ∈ I₁} f_{i,*}𝓕|_{U_i} ⟶ ⋯ ) for a hypercovering K = (I, {U_i}) of X finite in every degree by affine opens (exists_finite_affine_hypercovering_isAffineHom, [Stacks, Tag 01H7]); its terms are quasi-coherent because each f_i : U_i ⟶ S is affine, S being separated, and the base-change isomorphisms are nonempty_baseChangeIso.

def universalPushforwardComplexOfQuasiSeparated (f : X ⟶ S) [QuasiCompact f]
    [QuasiSeparated f] [CompactSpace S] [S.IsSeparated]
    (F : (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory) :
    UniversalPushforwardComplex f F

Stacks.AlgebraicGeometry.UniversalPushforward.universalPushforwardComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeCechComplex/UniversalPushforward.lean, line 488. The attribute's comment: “for an affine morphism”.

Stacks Project, Tag 01XN, for an affine morphism. Let f : X ⟶ S be an affine morphism of schemes and 𝓕 a quasi-coherent 𝒪_X-module. Then f_*𝓕 placed in degree zero is a bounded below complex of quasi-coherent 𝒪_S-modules whose ordinary inverse image along every g : S' ⟶ S represents Rf'_*𝓕' in D⁺(S'), with the notation of the cartesian square of [Stacks, Tag 02KF].

The three fields are discharged separately. The complex is the single complex, so its terms are f_*𝓕 in degree zero — quasi-coherent because f is affine ([Stacks, Tag 01XD]) — and zero objects elsewhere. The base-change isomorphism for every g is affineBaseChangeSingleIso: affineness is stable under base change, so no hypothesis on S' is needed and the universal quantification over g is genuine.

noncomputable def universalPushforwardComplex (f : X ⟶ S) [IsAffineHom f]
    (F : (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory) :
    UniversalPushforwardComplex f F

Stacks.AlgebraicGeometry.UniversalPushforward.nonempty_universalPushforwardComplex_of_isAffineHom_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeCechComplex/UniversalPushforwardAffineDiagonal.lean, line 96. The attribute's comment: “for a source of affine diagonal”.

Let f : X ⟶ S be a quasi-compact, quasi-separated morphism of schemes, let S be quasi-compact and separated and let 𝓕 be a quasi-coherent 𝒪_X-module. If X has affine diagonal then there is a bounded below complex 𝓚⁼ of quasi-coherent 𝒪_S-modules such that for every g : S' ⟶ S the ordinary inverse image g^*𝓚⁼ represents Rf'_*𝓕' in D⁺(S').

theorem nonempty_universalPushforwardComplex_of_isAffineHom_diagonal (f : X ⟶ S)
    [QuasiCompact f] [QuasiSeparated f] [CompactSpace S] [S.IsSeparated]
    [IsAffineHom (pullback.diagonal (terminal.from X))]
    (F : (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory) :
    Nonempty (UniversalPushforwardComplex f F)

Stacks.AlgebraicGeometry.UniversalPushforward.nonempty_universalPushforwardComplex_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeCechComplex/UniversalPushforwardAffineDiagonal.lean, line 109. The attribute's comment: “for a separated morphism”.

Let f : X ⟶ S be a quasi-compact, separated morphism of schemes, let S be quasi-compact and separated and let 𝓕 be a quasi-coherent 𝒪_X-module. Then there is a bounded below complex 𝓚⁼ of quasi-coherent 𝒪_S-modules such that for every g : S' ⟶ S the ordinary inverse image g^*𝓚⁼ represents Rf'_*𝓕' in D⁺(S').

theorem nonempty_universalPushforwardComplex_of_isSeparated (f : X ⟶ S)
    [QuasiCompact f] [IsSeparated f] [CompactSpace S] [S.IsSeparated]
    (F : (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory) :
    Nonempty (UniversalPushforwardComplex f F)

Tag 0GN5, a lemma

Tag 0GN5 in the Stacks Project.

Stacks.AlgebraicGeometry.ModuleBaseChange.isIso_degreewiseComparison_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FlatModuleCohomologyBaseChange/QuasiSeparated.lean, line 381.

[Stacks, Tag 0GN5]. Let
X' --g'--> X
|          |
f'         f
v          v
S' --g---> S
be a cartesian square of schemes with f quasi-compact and quasi-separated, let G be a quasi-coherent 𝒪_{S'}-module flat over S and let F be a quasi-coherent 𝒪_X-module. Then the degreewise comparison

Φ(R ⁱ f_* F) ⟶ R ⁱ f'_*(Ψ F)

of the two coefficient functors Φ : M ↦ g^*M ⊗ G and Ψ : F ↦ (g')^*F ⊗ (f')^*G is an isomorphism in every degree i.

theorem isIso_degreewiseComparison_app (H : IsPullback g' f' f g)
    [QuasiCompact f] [QuasiSeparated f]
    (G : SheafOfModules.{u} (structureSheafRing S'.toRingedSpace)) [G.IsQuasicoherent]
    (hG : AlgebraicGeometry.IsFlatOver g.toLRSHom.toShHom G)
    (F : SheafOfModules.{u} (structureSheafRing X.toRingedSpace)) [F.IsQuasicoherent]
    (i : ℕ) :
    IsIso ((degreewiseComparison H G hG i).app F)

Stacks.Cohomology.DerivedTensorBaseChange.tensorBaseChangeMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/TensorBaseChangeMap.lean, line 181. The attribute's comment: “the canonical map from left to right, in the derived category”.

The left-to-right map of [Stacks, Tag 0GN5] attached to a commutative square of ringed spaces:

G ⊗^L_{𝒪_{S'}} Lg^*Rf_*F ⟶ Rf'_*(L(f')^*G ⊗^L_{𝒪_{X'}} L(g')^*F).

It is the adjunction unit G ⟶ Rf'_*L(f')^*G of Stacks 079W in the first tensor factor and the derived base change map of Stacks 08HY in the second, followed by the relative cup product of Stacks 0B68 for f'.

def tensorBaseChangeMap (G : DerivedCategory (SheafOfModules.{u} (structureSheafRing S')))
    (F : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))) :
    ((derivedTensorProductFunctor S'.sheaf).obj G).obj
        ((derivedPullback g).obj ((derivedPushforward f).obj F)) ⟶
      (derivedPushforward f').obj
        (((derivedTensorProductFunctor X'.sheaf).obj ((derivedPullback f').obj G)).obj
          ((derivedPullback g').obj F))

Stacks.Cohomology.DerivedTensorBaseChange.tensorBaseChangeMap_naturality_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/TensorBaseChangeMap.lean, line 207. The attribute's comment: “naturality of the canonical map in the module on the base”.

The map of [Stacks, Tag 0GN5] is natural in the derived module on the base S'.

theorem tensorBaseChangeMap_naturality_left
    {G G' : DerivedCategory (SheafOfModules.{u} (structureSheafRing S'))} (w : G ⟶ G')
    (F : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))) :
    ((derivedTensorProductFunctor S'.sheaf).map w).app
          ((derivedPullback g).obj ((derivedPushforward f).obj F)) ≫
        tensorBaseChangeMap g' f' f g sq G' F =
      tensorBaseChangeMap g' f' f g sq G F ≫
        (derivedPushforward f').map
          (((derivedTensorProductFunctor X'.sheaf).map ((derivedPullback f').map w)).app
            ((derivedPullback g').obj F))

Stacks.Cohomology.DerivedTensorBaseChange.tensorBaseChangeMap_naturality_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/TensorBaseChangeMap.lean, line 224. The attribute's comment: “naturality of the canonical map in the module upstairs”.

The map of [Stacks, Tag 0GN5] is natural in the derived module on X.

theorem tensorBaseChangeMap_naturality_right
    (G : DerivedCategory (SheafOfModules.{u} (structureSheafRing S')))
    {F F' : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))} (u : F ⟶ F') :
    ((derivedTensorProductFunctor S'.sheaf).obj G).map
          ((derivedPullback g).map ((derivedPushforward f).map u)) ≫
        tensorBaseChangeMap g' f' f g sq G F' =
      tensorBaseChangeMap g' f' f g sq G F ≫
        (derivedPushforward f').map
          (((derivedTensorProductFunctor X'.sheaf).obj ((derivedPullback f').obj G)).map
            ((derivedPullback g').map u))

Stacks.Cohomology.DerivedTensorBaseChange.schemeTensorBaseChangeMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/TensorBaseChangeMap.lean, line 259. The attribute's comment: “the canonical map from left to right, for a cartesian square of schemes”.

The left-to-right map of [Stacks, Tag 0GN5] for the cartesian square of schemes of [Stacks, Tag 02KF]:

G ⊗^L_{𝒪_{S'}} Lg^*Rf_*F ⟶ Rf'_*(L(f')^*G ⊗^L_{𝒪_{X'}} L(g')^*F).

It is the map above at the underlying ringed spaces.

def schemeTensorBaseChangeMap (H : IsPullback g' f' f g) (G : DerivedCategory S'.Modules)
    (F : DerivedCategory X.Modules) :
    ((derivedTensorProductFunctor S'.toRingedSpace.sheaf).obj G).obj
        ((derivedPullback g.toLRSHom.toShHom).obj
          ((derivedPushforward f.toLRSHom.toShHom).obj F)) ⟶
      (derivedPushforward f'.toLRSHom.toShHom).obj
        (((derivedTensorProductFunctor X'.toRingedSpace.sheaf).obj
            ((derivedPullback f'.toLRSHom.toShHom).obj G)).obj
          ((derivedPullback g'.toLRSHom.toShHom).obj F))

Stacks.Cohomology.DerivedTensorBaseChange.schemeTensorBaseChangeMap_naturality_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/TensorBaseChangeMap.lean, line 278. The attribute's comment: “naturality for a cartesian square of schemes, in the module on the base”.

The map of [Stacks, Tag 0GN5] for a cartesian square of schemes is natural in the derived module on the base S'.

theorem schemeTensorBaseChangeMap_naturality_left (H : IsPullback g' f' f g)
    {G G' : DerivedCategory S'.Modules} (w : G ⟶ G') (F : DerivedCategory X.Modules) :
    ((derivedTensorProductFunctor S'.toRingedSpace.sheaf).map w).app
          ((derivedPullback g.toLRSHom.toShHom).obj
            ((derivedPushforward f.toLRSHom.toShHom).obj F)) ≫
        schemeTensorBaseChangeMap H G' F =
      schemeTensorBaseChangeMap H G F ≫
        (derivedPushforward f'.toLRSHom.toShHom).map
          (((derivedTensorProductFunctor X'.toRingedSpace.sheaf).map
            ((derivedPullback f'.toLRSHom.toShHom).map w)).app
              ((derivedPullback g'.toLRSHom.toShHom).obj F))

Stacks.Cohomology.DerivedTensorBaseChange.schemeTensorBaseChangeMap_naturality_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/TensorBaseChangeMap.lean, line 294. The attribute's comment: “naturality for a cartesian square of schemes, in the module upstairs”.

The map of [Stacks, Tag 0GN5] for a cartesian square of schemes is natural in the derived module on X.

theorem schemeTensorBaseChangeMap_naturality_right (H : IsPullback g' f' f g)
    (G : DerivedCategory S'.Modules) {F F' : DerivedCategory X.Modules} (u : F ⟶ F') :
    ((derivedTensorProductFunctor S'.toRingedSpace.sheaf).obj G).map
          ((derivedPullback g.toLRSHom.toShHom).map
            ((derivedPushforward f.toLRSHom.toShHom).map u)) ≫
        schemeTensorBaseChangeMap H G F' =
      schemeTensorBaseChangeMap H G F ≫
        (derivedPushforward f'.toLRSHom.toShHom).map
          (((derivedTensorProductFunctor X'.toRingedSpace.sheaf).obj
            ((derivedPullback f'.toLRSHom.toShHom).obj G)).map
              ((derivedPullback g'.toLRSHom.toShHom).map u))

Sources

LeanStacks.AlgebraicGeometry.Tag01XLDerivedIso.relativeCechIsoDerivedPushforward · Stacks.AlgebraicGeometry.RelativeCech.relativeCechPresheaf · Stacks.AlgebraicGeometry.RelativeCechComplex.relativeCechComplex · Stacks.AlgebraicGeometry.RelativeCechComplex.relativeCechComplex_obj_isQuasicoherent · Stacks.AlgebraicGeometry.RelativeCechBaseChange.baseChangeRelativeCechIsoDerivedPushforward · Stacks.AlgebraicGeometry.RelativeCechBaseChange.baseChangeRelativeCechComplexIsoOfIsAffineHom · Stacks.AlgebraicGeometry.UniversalPushforward.universalPushforwardComplexOfQuasiSeparated · Stacks.AlgebraicGeometry.UniversalPushforward.universalPushforwardComplex

Section30.8 Cohomology of projective space #

Section 30.8 of the Stacks Project, Tag 01XS. 5 tags here are carried by 29 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01XT, a lemma

Tag 01XT in the Stacks Project.

Stacks.ProjectiveSpace.Cohomology.twistCohomologyIsoHomogeneous, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/Cohomology/TwistCohomologyMonomial.lean, line 232. The attribute's comment: “degree zero, nonnegative twist”.

[Stacks, Tag 01XT], the degree-zero row. For d ≥ 0 the module H⁰(ℙⁿ_R, 𝒪(d)) is the module of degree-d homogeneous polynomials in T₀, …, Tₙ, for every n ≥ 0.

def twistCohomologyIsoHomogeneous (R : Type u) [CommRing R] (n : ℕ) (d : ℤ) (hd : 0 ≤ d) :
    twistCohomology R n d 0 ≅
      ModuleCat.of R (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R d.toNat)

Stacks.ProjectiveSpace.Cohomology.twistCohomologyIsoNegative, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/Cohomology/TwistCohomologyMonomial.lean, line 246. The attribute's comment: “top degree, negative twist”.

[Stacks, Tag 01XT], the top-degree row. For d < 0 the module Hⁿ(ℙⁿ_R, 𝒪(d)) is the degree-d part of (T₀ ⋯ Tₙ)⁻¹ R[T₀⁻¹, …, Tₙ⁻¹], the free R-module on the degree-d Laurent monomials with every exponent negative, for every n ≥ 0.

def twistCohomologyIsoNegative (R : Type u) [CommRing R] (n : ℕ) (d : ℤ) (hd : d < 0) :
    twistCohomology R n d n ≅ ModuleCat.of R (negativeTwistPart R n d)

Stacks.ProjectiveSpace.Cohomology.isZero_twistCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/Cohomology/TwistCohomologyMonomial.lean, line 257. The attribute's comment: “all other cases”.

[Stacks, Tag 01XT], the vanishing row. Outside the two cases q = 0, d ≥ 0 and q = n, d < 0 the module H^q(ℙⁿ_R, 𝒪(d)) is zero, for every n ≥ 0.

theorem isZero_twistCohomology (R : Type u) [CommRing R] (n : ℕ) (d : ℤ) (q : ℕ)
    (hq : ¬ ((q = 0 ∧ 0 ≤ d) ∨ (q = n ∧ d < 0))) :
    IsZero (twistCohomology R n d q)

Stacks.ProjectiveSpace.Cohomology.twistCohomologyMonomial, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/Cohomology/TwistCohomologyMonomial.lean, line 309. References: EGA III (2.1.13), “more general”; EGA III (2.1.14), “more general”; SGA 7 XIX (1.2), “special case”.

The cohomology of the twists of the structure sheaf on projective space. For every commutative ring R, every n ≥ 0 and every integer d, H^q(ℙⁿ_R, 𝒪(d)) is the degree-d part of R[T₀, …, Tₙ] when q = 0 and d ≥ 0, is the degree-d part of (T₀ ⋯ Tₙ)⁻¹ R[T₀⁻¹, …, Tₙ⁻¹] when q = n and d < 0, and is zero otherwise, as R-modules.

def twistCohomologyMonomial (R : Type u) [CommRing R] (n : ℕ) (d : ℤ) :
    TwistCohomologyMonomial R n d

Stacks.ProjectiveSpace.Cohomology.bijective_degreeSection_line, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/Cohomology/TwistSectionsBijective.lean, line 87. The attribute's comment: “degree zero, nonnegative twist, for the projective line over a field: the canonical map of Equation 01MP from the degree-d binary forms to the sections of O(d) is bijective”. References: EGA II (8.14.11), “Case Y = Spec k”.

Γ(𝐏¹_k, 𝒪(d)) is the module of binary forms of degree d, through the canonical map of Equation [Stacks, Tag 01MP].

For k a field and every d ≥ 0, the degree-d section map (k[T₀, T₁])_d ⟶ Γ(𝐏¹_k, 𝒪(d)) is bijective. This is the n = 1 case of Stacks.ProjectiveSpace.Cohomology.bijective_degreeSection, which is injective because k[T₀, …, Tₙ] is a domain and surjective because Stacks.ProjectiveSpace.Cohomology.homogeneousIsoTwistSections makes the two sides k-vector spaces of the same finite dimension.

Together with the multiplicativity across degrees of Stacks.AlgebraicGeometry.ProjTwistSectionRing.mul_degreeSection this is the identification of the graded ring ⨁_d Γ(𝐏¹_k, 𝒪(d)) with k[T₀, T₁].

theorem bijective_degreeSection_line (k : Type u) [Field k] (d : ℕ) :
    Function.Bijective (degreeSection (polyGrading k 1) d)

Tag 01XU, an equation

Tag 01XU in the Stacks Project.

Stacks.ProjectiveSpace.Cohomology.serreTwistCohomology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/Cohomology/SerreComputation.lean, line 285. References: EGA III (2.1.13), “more general”; SGA 7 XIX (1.2), “special case”.

Serre's computation of the cohomology of the twists of the structure sheaf on projective space. For a commutative ring R, n = m + 1 ≥ 1 and every integer d, H^q(ℙⁿ_R, 𝒪(d)) is the degree-d part of R[T₀, …, Tₙ] for q = 0, is zero for q ≠ 0, n, and is Hom_R((R[T₀, …, Tₙ])_{-n-1-d}, R) for q = n, as R-modules.

def serreTwistCohomology (R : Type u) [CommRing R] (m : ℕ) (d : ℤ) :
    SerreTwistCohomology R m d

Tag 01XV, a lemma

Tag 01XV in the Stacks Project.

Stacks.ProjectiveSpace.Cohomology.serreTwistCohomology_degreeZero_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/Cohomology/SerreSheafBaseChange/TwistBaseChange.lean, line 584. The attribute's comment: “base change along R → S on H^0, through Equation 01XU”.

[Stacks, Tag 01XV], base change on H⁰. For a ring map φ : R → S, the base-change map H⁰(ℙⁿ_R, 𝒪(d)) ⟶ H⁰(ℙⁿ_S, 𝒪(d)) — the map on cohomology attached to the pullback along ℙⁿ_S ⟶ ℙⁿ_R and the identification of the pullback of 𝒪(d) with 𝒪(d) — is, through the identifications of [Stacks, Equation 01XU] of H⁰(ℙⁿ_R, 𝒪(d)) with (R[T₀, …, Tₙ])_d and of H⁰(ℙⁿ_S, 𝒪(d)) with (S[T₀, …, Tₙ])_d, the coefficientwise base change (R[T₀, …, Tₙ])_d ⟶ (S[T₀, …, Tₙ])_d. Here n = N + 1 and d is any integer.

theorem serreTwistCohomology_degreeZero_baseChange (N : ℕ) (d : ℤ)
    (x : twistCohomology R (N + 1) d 0) :
    ConcreteCategory.hom (serreTwistCohomology S N d).degreeZero.hom
        (ConcreteCategory.hom (Stacks.Cohomology.CechIso.fMapCohomology (projModelMap (N + 1) φ)
          (ProjectiveSpectrum.Proj.twistingSheaf (polyGrading S (N + 1)) d)
          (ProjectiveSpectrum.Proj.twistingSheaf (polyGrading R (N + 1)) d)
          (twistBaseChangeFMap φ (N + 1) d) 0) x) =
      baseChangeChart φ (N + 1) d ∅
        (ConcreteCategory.hom (serreTwistCohomology R N d).degreeZero.hom x)

Stacks.ProjectiveSpace.Cohomology.serreTwistCohomology_degreeTop_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/Cohomology/SerreSheafBaseChange/TwistBaseChange.lean, line 614. The attribute's comment: “base change along R → S on H^n, through Equation 01XU”.

[Stacks, Tag 01XV], base change on Hⁿ. For a ring map φ : R → S, the base-change map Hⁿ(ℙⁿ_R, 𝒪(d)) ⟶ Hⁿ(ℙⁿ_S, 𝒪(d)) is, through the identifications of [Stacks, Equation 01XU] of Hⁿ with Hom((R[T₀, …, Tₙ])_{-n-1-d}, R) and with Hom((S[T₀, …, Tₙ])_{-n-1-d}, S), the base change of functionals: the functional attached to the base change of a class takes the value φ (λ h) on the base change of h, where λ is the functional attached to the class. Since the base changes of the monomials span (S[T₀, …, Tₙ])_{-n-1-d}, this determines it. Here n = N + 1 and d is any integer.

theorem serreTwistCohomology_degreeTop_baseChange (N : ℕ) (d : ℤ)
    (x : twistCohomology R (N + 1) d (N + 1))
    (h : twistChart R (N + 1) (-d - (((N + 1 : ℕ) : ℤ) + 1)) (∅ : Set (Fin (N + 1 + 1)))) :
    ConcreteCategory.hom (serreTwistCohomology S N d).degreeTop.hom
        (ConcreteCategory.hom (Stacks.Cohomology.CechIso.fMapCohomology (projModelMap (N + 1) φ)
          (ProjectiveSpectrum.Proj.twistingSheaf (polyGrading S (N + 1)) d)
          (ProjectiveSpectrum.Proj.twistingSheaf (polyGrading R (N + 1)) d)
          (twistBaseChangeFMap φ (N + 1) d) (N + 1)) x)
        (baseChangeChart φ (N + 1) (-d - (((N + 1 : ℕ) : ℤ) + 1)) ∅ h) =
      φ (ConcreteCategory.hom (serreTwistCohomology R N d).degreeTop.hom x h)

Stacks.ProjectiveSpace.Cohomology.zeroDim_degreeZero_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/Cohomology/SerreSheafBaseChange/ZeroDim.lean, line 175. The attribute's comment: “n = 0: multiplication by a homogeneous f on H^0, d ≥ 0, through Tag 01XT”.

[Stacks, Tag 01XV] for n = 0, multiplication on H⁰, corrected. On ℙ⁰_R the two rows of [Stacks, Equation 01XU] both concern H⁰ and hold only under the side conditions of [Stacks, Tag 01XT]. For d ≥ 0, through the identification of H⁰(ℙ⁰_R, 𝒪(d)) with (R[T₀])_d, the map induced by multiplication by f, homogeneous of degree m, is multiplication by f.

theorem zeroDim_degreeZero_mul {m : ℕ} {d e : ℤ} (f : MvPolynomial (Fin (0 + 1)) R)
    (hf : f.IsHomogeneous m) (hde : d + m = e) (hd : 0 ≤ d) (x : twistCohomology R 0 d 0) :
    LinearEquiv.ofEq _ _ (twistChart_univ_eq_empty_zeroDim R (show 0 ≤ e by omega))
        (ConcreteCategory.hom (twistCohomologyIsoChartUnivZeroDim R e).hom
          (ConcreteCategory.hom ((ModuleCat.restrictScalars.{u} (coeffScalar R 0)).map
          (((Stacks.Cohomology.sectionsFunctor (AlgebraicGeometry.Proj (polyGrading R 0))
            ⊤).rightDerived 0).map (twistScalarSheafMap (polyGrading R 0) m d e
              (by omega) ⟨f, (MvPolynomial.mem_homogeneousSubmodule m f).2 hf⟩))) x)) =
      chartMul (chartOfHomogeneous R 0 f hf) hde ∅
        (LinearEquiv.ofEq _ _ (twistChart_univ_eq_empty_zeroDim R hd)
          (ConcreteCategory.hom (twistCohomologyIsoChartUnivZeroDim R d).hom x))

Stacks.ProjectiveSpace.Cohomology.zeroDim_degreeTop_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/Cohomology/SerreSheafBaseChange/ZeroDim.lean, line 194. The attribute's comment: “n = 0: multiplication on H^n is the contragredient, d + m < 0, through Tag 01XT”.

[Stacks, Tag 01XV] for n = 0, multiplication on Hⁿ, corrected. For d + m < 0, through the identification of H⁰(ℙ⁰_R, 𝒪(d)) with Hom_R((R[T₀])_{-1-d}, R) by the residue pairing, the map induced by multiplication by f, homogeneous of degree m, is the contragredient of multiplication by f, (R[T₀])_{-1-(d+m)} ⟶ (R[T₀])_{-1-d}.

theorem zeroDim_degreeTop_mul {m : ℕ} {d e : ℤ} (f : MvPolynomial (Fin (0 + 1)) R)
    (hf : f.IsHomogeneous m) (hde : d + m = e) (he : e < 0) (x : twistCohomology R 0 d 0)
    (h : twistChart R 0 (-e - (((0 : ℕ) : ℤ) + 1)) (∅ : Set (Fin (0 + 1)))) :
    topDualEquiv R 0 e (LinearEquiv.ofEq _ _ (twistChart_univ_eq_negativeTwistPart_zeroDim R he)
        (ConcreteCategory.hom (twistCohomologyIsoChartUnivZeroDim R e).hom
          (ConcreteCategory.hom ((ModuleCat.restrictScalars.{u} (coeffScalar R 0)).map
          (((Stacks.Cohomology.sectionsFunctor (AlgebraicGeometry.Proj (polyGrading R 0))
            ⊤).rightDerived 0).map (twistScalarSheafMap (polyGrading R 0) m d e
              (by omega) ⟨f, (MvPolynomial.mem_homogeneousSubmodule m f).2 hf⟩))) x))) h =
      topDualEquiv R 0 d (LinearEquiv.ofEq _ _
          (twistChart_univ_eq_negativeTwistPart_zeroDim R (show d < 0 by omega))
          (ConcreteCategory.hom (twistCohomologyIsoChartUnivZeroDim R d).hom x))
        (chartMul (chartOfHomogeneous R 0 f hf) (show -e - (((0 : ℕ) : ℤ) + 1) + m =
          -d - (((0 : ℕ) : ℤ) + 1) by omega) ∅ h)

Stacks.ProjectiveSpace.Cohomology.zeroDim_degreeZero_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/Cohomology/SerreSheafBaseChange/ZeroDim.lean, line 217. The attribute's comment: “n = 0: base change along R → S on H^0, d ≥ 0, through Tag 01XT”.

[Stacks, Tag 01XV] for n = 0, base change on H⁰, corrected. For d ≥ 0, through the identifications of H⁰(ℙ⁰, 𝒪(d)) with (R[T₀])_d and (S[T₀])_d, the base-change map is the coefficientwise base change.

theorem zeroDim_degreeZero_baseChange (d : ℤ) (hd : 0 ≤ d) (x : twistCohomology R 0 d 0) :
    LinearEquiv.ofEq _ _ (twistChart_univ_eq_empty_zeroDim S hd)
        (ConcreteCategory.hom (twistCohomologyIsoChartUnivZeroDim S d).hom
          (ConcreteCategory.hom (Stacks.Cohomology.CechIso.fMapCohomology (projModelMap 0 φ)
          (ProjectiveSpectrum.Proj.twistingSheaf (polyGrading S 0) d)
          (ProjectiveSpectrum.Proj.twistingSheaf (polyGrading R 0) d)
          (twistBaseChangeFMap φ 0 d) 0) x)) =
      baseChangeChart φ 0 d ∅ (LinearEquiv.ofEq _ _ (twistChart_univ_eq_empty_zeroDim R hd)
        (ConcreteCategory.hom (twistCohomologyIsoChartUnivZeroDim R d).hom x))

Stacks.ProjectiveSpace.Cohomology.zeroDim_degreeTop_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/Cohomology/SerreSheafBaseChange/ZeroDim.lean, line 234. The attribute's comment: “n = 0: base change along R → S on H^n, d < 0, through Tag 01XT”.

[Stacks, Tag 01XV] for n = 0, base change on Hⁿ, corrected. For d < 0, through the identifications of H⁰(ℙ⁰, 𝒪(d)) with Hom_R((R[T₀])_{-1-d}, R) and with Hom_S((S[T₀])_{-1-d}, S) by the residue pairing, the functional attached to the base change of a class takes the value φ (λ h) on the base change of h.

theorem zeroDim_degreeTop_baseChange (d : ℤ) (hd : d < 0) (x : twistCohomology R 0 d 0)
    (h : twistChart R 0 (-d - (((0 : ℕ) : ℤ) + 1)) (∅ : Set (Fin (0 + 1)))) :
    topDualEquiv S 0 d (LinearEquiv.ofEq _ _ (twistChart_univ_eq_negativeTwistPart_zeroDim S hd)
        (ConcreteCategory.hom (twistCohomologyIsoChartUnivZeroDim S d).hom
          (ConcreteCategory.hom (Stacks.Cohomology.CechIso.fMapCohomology (projModelMap 0 φ)
          (ProjectiveSpectrum.Proj.twistingSheaf (polyGrading S 0) d)
          (ProjectiveSpectrum.Proj.twistingSheaf (polyGrading R 0) d)
          (twistBaseChangeFMap φ 0 d) 0) x)))
        (baseChangeChart φ 0 (-d - (((0 : ℕ) : ℤ) + 1)) ∅ h) =
      φ (topDualEquiv R 0 d (LinearEquiv.ofEq _ _
        (twistChart_univ_eq_negativeTwistPart_zeroDim R hd)
          (ConcreteCategory.hom (twistCohomologyIsoChartUnivZeroDim R d).hom x)) h)

Stacks.ProjectiveSpace.Cohomology.serreTwistCohomology_degreeZero_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/Cohomology/SerreSheafFunctoriality.lean, line 339. The attribute's comment: “multiplication by a homogeneous f on H^0, through Equation 01XU”.

[Stacks, Tag 01XV], multiplication on H⁰. For f ∈ R[T₀, …, Tₙ] homogeneous of degree m, the map H⁰(ℙⁿ_R, 𝒪(d)) ⟶ H⁰(ℙⁿ_R, 𝒪(d + m)) induced by the morphism of sheaves 𝒪(d) ⟶ 𝒪(d + m) given by multiplication by f is, through the identification of [Stacks, Equation 01XU] of H⁰(ℙⁿ_R, 𝒪(d)) with (R[T₀, …, Tₙ])_d, multiplication by f (R[T₀, …, Tₙ])_d ⟶ (R[T₀, …, Tₙ])_{d+m}. Here n = N + 1 and d is any integer.

theorem serreTwistCohomology_degreeZero_mul (N : ℕ) {m : ℕ} {d e : ℤ}
    (f : MvPolynomial (Fin (N + 1 + 1)) R) (hf : f.IsHomogeneous m) (hde : d + m = e) :
    (ModuleCat.restrictScalars.{u} (coeffScalar R (N + 1))).map
          (((Stacks.Cohomology.sectionsFunctor (AlgebraicGeometry.Proj (polyGrading R (N + 1)))
            ⊤).rightDerived 0).map (twistScalarSheafMap (polyGrading R (N + 1)) m d e
              (by omega) ⟨f, (MvPolynomial.mem_homogeneousSubmodule m f).2 hf⟩)) ≫
        (serreTwistCohomology R N e).degreeZero.hom =
      (serreTwistCohomology R N d).degreeZero.hom ≫
        ModuleCat.ofHom (chartMul (chartOfHomogeneous R (N + 1) f hf) hde ∅)

Stacks.ProjectiveSpace.Cohomology.serreTwistCohomology_degreeTop_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/Cohomology/SerreSheafFunctoriality.lean, line 361. The attribute's comment: “multiplication by a homogeneous f on H^n is the contragredient, through Equation 01XU”.

[Stacks, Tag 01XV], multiplication on Hⁿ. For f ∈ R[T₀, …, Tₙ] homogeneous of degree m, the map Hⁿ(ℙⁿ_R, 𝒪(d)) ⟶ Hⁿ(ℙⁿ_R, 𝒪(d + m)) induced by the morphism of sheaves 𝒪(d) ⟶ 𝒪(d + m) given by multiplication by f is, through the identifications of [Stacks, Equation 01XU] of Hⁿ(ℙⁿ_R, 𝒪(d)) with Hom_R((R[T₀, …, Tₙ])_{-n-1-d}, R), the contragredient of multiplication by f (R[T₀, …, Tₙ])_{-n-1-(d+m)} ⟶ (R[T₀, …, Tₙ])_{-n-1-d}. Here n = N + 1 and d is any integer.

theorem serreTwistCohomology_degreeTop_mul (N : ℕ) {m : ℕ} {d e : ℤ}
    (f : MvPolynomial (Fin (N + 1 + 1)) R) (hf : f.IsHomogeneous m) (hde : d + m = e) :
    (ModuleCat.restrictScalars.{u} (coeffScalar R (N + 1))).map
          (((Stacks.Cohomology.sectionsFunctor (AlgebraicGeometry.Proj (polyGrading R (N + 1)))
            ⊤).rightDerived (N + 1)).map (twistScalarSheafMap (polyGrading R (N + 1)) m d e
              (by omega) ⟨f, (MvPolynomial.mem_homogeneousSubmodule m f).2 hf⟩)) ≫
        (serreTwistCohomology R N e).degreeTop.hom =
      (serreTwistCohomology R N d).degreeTop.hom ≫
        ModuleCat.ofHom
          (chartMul (chartOfHomogeneous R (N + 1) f hf)
            (dualDegree_add_of_add N hde) ∅).dualMap

Tag 01XW, a lemma

Tag 01XW in the Stacks Project.

Stacks.AlgebraicGeometry.ProjectiveSpaceHigherDirectImage.isIso_app_structureMorphism_projectiveSpaceOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpaceHigherDirectImage/DegreeZero.lean, line 158. The attribute's comment: “the degree-zero clause at the zeroth twist, sectionwise and for the underived direct image: the structure morphism of ℙⁿ_S induces an isomorphism Γ(S, V) ≅ Γ(ℙⁿ_S, f⁻¹V) for every affine open V of the base, which is f_ 𝒪 = 𝒪_S on a basis of opens. The degree-zero row at every twist, assembled as an isomorphism of module sheaves on S and in the R⁰ f_ spelling, is ProjectiveSpaceHigherDirectImage.baseDegreeSheafIsoPushforwardTwistOver and ...baseDegreeSheafIsoRightDerivedPushforwardTwistOver in ...DegreeZeroRow; the whole display, its three rows in one statement at n >= 1, is ...rightDerivedPlusPushforwardTwistOverDisplay in ...Display”.

The degree-zero identification f_* 𝒪_{ℙⁿ_S} = 𝒪_S. For the structure morphism f : ℙⁿ_S ⟶ S over an arbitrary scheme S and an arbitrary n, the canonical map 𝒪_S ⟶ f_* 𝒪_{ℙⁿ_S} is an isomorphism on the sections over every affine open V of the base: f induces an isomorphism Γ(S, V) ≅ Γ(ℙⁿ_S, f⁻¹V).

Since the affine opens form a basis of S and a morphism of sheaves that is invertible on a basis is invertible, this is the full assertion that the direct image of the structure sheaf of ℙⁿ_S is the structure sheaf of S.

theorem isIso_app_structureMorphism_projectiveSpaceOver (n : ℕ) (S : Scheme.{u}) {V : S.Opens}
    (hV : IsAffineOpen V) : IsIso ((projectiveSpaceOver n S ↘ S).app V)

Stacks.AlgebraicGeometry.ProjectiveSpaceHigherDirectImage.rightDerivedPlusPushforwardTwistOverDisplay, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpaceHigherDirectImage/Display.lean, line 110. The attribute's comment: “the display whole, at n = m + 1 >= 1, for every scheme S and every integer twist d: R^0 f_ O(d) = (O_S[T_0, ..., T_n])_d, R^q f_ O(d) = 0 for every q /= 0, n, and R^n f_* O(d) = Hom_{O_S}((O_S[T_0, ..., T_n])_{-n-1-d}, O_S). At n = 0 the display's first and third rows speak about the same degree and disagree, so n >= 1 is the range in which it is a consistent assertion”.

The display of [Stacks, Tag 01XW]. For the structure morphism f : ℙⁿ_S ⟶ S of projective n-space over an arbitrary scheme S, with n = m + 1 ≥ 1, and for every integer twist d:

R⁰ f_* 𝒪(d) ≅ (𝒪_S[T₀, …, Tₙ])_d, the degree-d part of the polynomial algebra on the base;

Rᵠ f_* 𝒪(d) = 0 for every integer q with q ≠ 0 and q ≠ n;

Rⁿ f_* 𝒪(d) ≅ Hom_{𝒪_S}((𝒪_S[T₀, …, Tₙ])_{-n-1-d}, 𝒪_S).

The three components are baseDegreeSheafIsoRightDerivedPushforwardTwistOver, whose hypothesis 0 ≤ d ∨ 0 < n is discharged by n = m + 1 ≥ 1, then MiddleVanishing.isZero_rightDerivedPlus_pushforward_twistOver_of_ne, then rightDerivedPlusTopIsoDualBaseDegreeSheaf.

The source's display is inconsistent at n = 0, where its first and third rows apply to the same degree and disagree, so n ≥ 1 is the range in which it asserts something; see the module docstring.

def rightDerivedPlusPushforwardTwistOverDisplay (m : ℕ) (S : Scheme.{u}) (d : ℤ) :
    PProd (baseDegreeSheaf (m + 1) S d ≅
        ((Scheme.Modules.pushforward (projectiveSpaceOver (m + 1) S ↘ S)).rightDerivedPlus 0).obj
          (twistOver (m + 1) S d))
      (PProd (∀ q : ℤ, q ≠ 0 → q ≠ ((m + 1 : ℕ) : ℤ) →
            IsZero (((Scheme.Modules.pushforward
              (projectiveSpaceOver (m + 1) S ↘ S)).rightDerivedPlus q).obj
                (twistOver (m + 1) S d)))
        (((Scheme.Modules.pushforward (projectiveSpaceOver (m + 1) S ↘ S)).rightDerivedPlus
              ((m + 1 : ℕ) : ℤ)).obj (twistOver (m + 1) S d) ≅
          dualSheaf (baseDegreeSheaf (m + 1) S (-((m + 1 : ℕ) : ℤ) - 1 - d))))

Stacks.AlgebraicGeometry.ProjectiveSpaceHigherDirectImage.MiddleVanishing.isZero_rightDerivedPlus_pushforward_twistOver_of_ne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpaceHigherDirectImage/MiddleVanishing.lean, line 238. The attribute's comment: “the vanishing row, whole: R^q f_* 𝒪(d) = 0 for every q ≠ 0, n, every scheme S, every n and every integer d. The q = 0 row is ProjectiveSpaceHigherDirectImage.baseDegreeSheafIsoRightDerivedPushforwardTwistOver in ...DegreeZeroRow; the q = n row is ...rightDerivedPlusTopIsoDualBaseDegreeSheaf in ...TopDegreeRowGeneral, for every twist d over an arbitrary base. The whole display, its three rows in one statement at n >= 1, is ...rightDerivedPlusPushforwardTwistOverDisplay in ...Display”.

The vanishing row of [Stacks, Tag 01XW]. For the structure morphism f : ℙⁿ_S ⟶ S over an arbitrary scheme S, an arbitrary n and an arbitrary integer d, the higher direct image Rᵠ f_* 𝒪(d) is zero in every degree q with q ≠ 0 and q ≠ n.

theorem isZero_rightDerivedPlus_pushforward_twistOver_of_ne (n : ℕ) (S : Scheme.{u}) (d : ℤ)
    (q : ℤ) (hq0 : q ≠ 0) (hqn : q ≠ (n : ℤ)) :
    IsZero (((Scheme.Modules.pushforward (projectiveSpaceOver n S ↘ S)).rightDerivedPlus q).obj
      (twistOver n S d))

Tag 01XX, a lemma

Tag 01XX in the Stacks Project.

Stacks.AlgebraicGeometry.ProjectiveBundleCohomology.higherDirectImageZeroIso_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveBundleCohomology/BaseChangeCompatibility.lean, line 118. The attribute's comment: “compatibility with base change, the q = 0 row: for g : S' → S and E' ≅ g^E, the base change map g^ R^0 π_ O(d) → R^0 π'_ O(d) followed by R^0 π'_ O(d) ≅ Sym^d(E') is g^(R^0 π_ O(d) ≅ Sym^d(E)) followed by g^ Sym^d(E) ≅ Sym^d(E'), for every d ≥ 0 and n ≥ 1”.

[Stacks, Tag 01XX], compatibility with base change, the row q = 0: for a morphism of schemes g : S' ⟶ S, E finite locally free of constant rank n + 1 with n ≥ 1, E' ≅ g^*E and every d ≥ 0, the base change map g^* R⁰π_* 𝒪_{𝐏(E)}(d) ⟶ R⁰π'_* 𝒪_{𝐏(E')}(d) corresponds, under the identifications R⁰π_* 𝒪(d) ≅ Sym^d(E) and R⁰π'_* 𝒪(d) ≅ Sym^d(E'), to g^* Sym^d(E) ≅ Sym^d(E').

public theorem higherDirectImageZeroIso_baseChange (hn : 1 ≤ n) (d : ℕ) :
    bundleTwistBaseChange g E hfree E' hE D D' 0 (d : ℤ) ≫
        (higherDirectImageZeroIso E' (isFiniteLocallyFreeOfRank_of_iso_pullback g E hfree E' hE)
          D' hn d).hom =
      (Scheme.Modules.pullback g).map (higherDirectImageZeroIso E hfree D hn d).hom ≫
        bundleSymBaseChange g E hfree E' hE (d : ℤ)

Stacks.AlgebraicGeometry.ProjectiveBundleCohomology.higherDirectImageTopIso_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveBundleCohomology/BaseChangeCompatibility.lean, line 161. The attribute's comment: “compatibility with base change, the q = n row: for g : S' → S and E' ≅ g^E, the base change map g^ R^n π_ O(d) → R^n π'_ O(d) followed by R^n π'_ O(d) ≅ SheafHom(Sym^(-n-1-d)(E') ⊗ ∧^(n+1) E', O_S') is g^(R^n π_ O(d) ≅ SheafHom(Sym^(-n-1-d)(E) ⊗ ∧^(n+1) E, O_S)) followed by the canonical map g^ SheafHom(M, O_S) → SheafHom(g^ M, O_S') and g^(Sym^(-n-1-d)(E) ⊗ ∧^(n+1) E) ≅ Sym^(-n-1-d)(E') ⊗ ∧^(n+1) E', for every integer d and n ≥ 1”.

[Stacks, Tag 01XX], compatibility with base change, the row q = n: for a morphism of schemes g : S' ⟶ S, E finite locally free of constant rank n + 1 with n ≥ 1, E' ≅ g^*E and every integer d, the base change map g^* Rⁿ π_* 𝒪_{𝐏(E)}(d) ⟶ Rⁿ π'_* 𝒪_{𝐏(E')}(d) corresponds, under the identifications Rⁿ π_* 𝒪(d) ≅ SheafHom(Sym^{-n-1-d}(E) ⊗ ⋀ⁿ⁺¹ E, 𝒪_S) and Rⁿ π'_* 𝒪(d) ≅ SheafHom(Sym^{-n-1-d}(E') ⊗ ⋀ⁿ⁺¹ E', 𝒪_{S'}), to the canonical map g^* SheafHom(Sym^{-n-1-d}(E) ⊗ ⋀ⁿ⁺¹ E, 𝒪_S) ⟶ SheafHom(Sym^{-n-1-d}(E') ⊗ ⋀ⁿ⁺¹ E', 𝒪_{S'}).

public theorem higherDirectImageTopIso_baseChange (hn : 1 ≤ n) (d : ℤ) :
    bundleTwistBaseChange g E hfree E' hE D D' n d ≫
        (higherDirectImageTopIso E' (isFiniteLocallyFreeOfRank_of_iso_pullback g E hfree E' hE)
          D' hn d).hom =
      (Scheme.Modules.pullback g).map (higherDirectImageTopIso E hfree D hn d).hom ≫
        bundleTopTargetBaseChange g E hfree E' hE d

Stacks.AlgebraicGeometry.ProjectiveBundleCohomology.isIso_bundleTwistBaseChange_of_ne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveBundleCohomology/BaseChangeCompatibility.lean, line 179. The attribute's comment: “compatibility with base change, the vanishing rows: for g : S' → S, E' ≅ g^E and q ≠ 0, n the base change map g^ R^q π_ O(d) → R^q π'_ O(d) is an isomorphism between zero modules, for every integer d”.

[Stacks, Tag 01XX], compatibility with base change, the vanishing rows: for q ≠ 0, n the base change map g^* R^q π_* 𝒪_{𝐏(E)}(d) ⟶ R^q π'_* 𝒪_{𝐏(E')}(d) is an isomorphism of zero modules, for every integer d.

public theorem isIso_bundleTwistBaseChange_of_ne (q : ℕ) (d : ℤ) (hq0 : q ≠ 0) (hqn : q ≠ n) :
    IsIso (bundleTwistBaseChange g E hfree E' hE D D' q d)

Stacks.AlgebraicGeometry.ProjectiveBundleCohomology.isIso_bundleTwistBaseChange_zero_of_neg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveBundleCohomology/BaseChangeCompatibility.lean, line 194. The attribute's comment: “compatibility with base change, the q = 0 row for d < 0: for g : S' → S and E' ≅ g^E the base change map g^ R^0 π_ O(d) → R^0 π'_ O(d) is an isomorphism between zero modules, for n ≥ 1”.

[Stacks, Tag 01XX], compatibility with base change, the row q = 0 for d < 0: the base change map g^* R⁰π_* 𝒪_{𝐏(E)}(d) ⟶ R⁰π'_* 𝒪_{𝐏(E')}(d) is an isomorphism of zero modules.

public theorem isIso_bundleTwistBaseChange_zero_of_neg (hn : 1 ≤ n) {d : ℤ} (hd : d < 0) :
    IsIso (bundleTwistBaseChange g E hfree E' hE D D' 0 d)

Stacks.AlgebraicGeometry.ProjectiveBundleCohomology.higherDirectImage_iso_compatible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveBundleCohomology/IsoTopRowIso.lean, line 744. The attribute's comment: “compatibility with isomorphisms between locally free sheaves, every row: for an isomorphism e : E ≅ E' of finite locally free modules of constant rank n + 1, n ≥ 1, over an arbitrary scheme S, the maps R^q π_ O(d) → R^q π'_ O(d) induced by e and P(E') ≅ P(E) carry the identification R^0 π_ O(d) ≅ Sym^d(E) to R^0 π'_ O(d) ≅ Sym^d(E') under Sym^d(e) for d ≥ 0, are zero for q = 0, d < 0 and for q ≠ 0, n, and carry R^n π_* O(d) ≅ SheafHom(Sym^(-n-1-d)(E) ⊗ ∧^(n+1) E, O_S) to the same identification for E' under the dual of Sym^(-n-1-d)(e⁻¹) ⊗ ∧^(n+1)(e⁻¹), for every integer d”.

[Stacks, Tag 01XX]: the identifications of the higher direct images of the twists on a projective bundle are compatible with isomorphisms between locally free sheaves. Let e : E ≅ E' be an isomorphism of finite locally free 𝒪_S-modules of constant rank n + 1, n ≥ 1, inducing 𝐏(E') ≅ 𝐏(E) over S and the maps R^q π_* 𝒪_{𝐏(E)}(d) ⟶ R^q π'_* 𝒪_{𝐏(E')}(d) (higherDirectImageIsoMap). For every pair (q, d) of integers: * q = 0, d ≥ 0: the identifications R⁰π_* 𝒪(d) ≅ Sym^d correspond under Sym^d(e); * q = 0, d < 0, and q ≠ 0, n: the induced map is zero, between modules that vanish; * q = n: the identifications Rⁿ π_* 𝒪(d) ≅ SheafHom(Sym^{-n-1-d}(E) ⊗ ⋀ⁿ⁺¹ E, 𝒪_S) correspond under the dual of Sym^{-n-1-d}(e⁻¹) ⊗ ⋀ⁿ⁺¹(e⁻¹).

public theorem higherDirectImage_iso_compatible :
    (∀ d : ℕ, higherDirectImageIsoMap hfree hfree' e D D' 0 d ≫
        (higherDirectImageZeroIso E' hfree' D' hn d).hom =
      (higherDirectImageZeroIso E hfree D hn d).hom ≫ (symHom hfree hfree' e.hom).app (d : ℤ)) ∧
    (∀ d : ℤ, d < 0 → higherDirectImageIsoMap hfree hfree' e D D' 0 d = 0) ∧
    (∀ q d : ℤ, q ≠ 0 → q ≠ n → higherDirectImageIsoMap hfree hfree' e D D' q d = 0) ∧
    (∀ d : ℤ,
      haveI := isQuasicoherent_of_isFiniteLocallyFreeOfRank E hfree
      haveI := isQuasicoherent_of_isFiniteLocallyFreeOfRank E' hfree'
      higherDirectImageIsoMap hfree hfree' e D D' (n : ℤ) d ≫
          (higherDirectImageTopIso E' hfree' D' hn d).hom =
        (higherDirectImageTopIso E hfree D hn d).hom ≫ topRowTargetMap hfree hfree' e d)

Stacks.AlgebraicGeometry.ProjectiveBundleCohomology.isZero_higherDirectImage_twist, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveBundleCohomology/Statement.lean, line 81. The attribute's comment: “the vanishing row: R^q π_* O(d) = 0 for q ≠ 0, n, every integer d and every integer q, for E finite locally free of constant rank n + 1 over an arbitrary scheme S”. References: EGA III (2.1.15), “partial”.

For E finite locally free of constant rank n + 1 with projective bundle π : 𝐏(E) ⟶ S, R^q π_* 𝒪_{𝐏(E)}(d) = 0 for every integer d and every integer q with q ≠ 0 and q ≠ n.

public theorem isZero_higherDirectImage_twist (d q : ℤ) (hq0 : q ≠ 0) (hqn : q ≠ n) :
    IsZero (((Scheme.Modules.pushforward
        (relativeProj (bundleAlgebra E hfree)).toBase).rightDerivedPlus
      q).obj (D.algebra.piece d))

Stacks.AlgebraicGeometry.ProjectiveBundleCohomology.isIso_symToPushforwardTwist, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveBundleCohomology/Statement.lean, line 92. The attribute's comment: “the q = 0 row in degrees d ≥ 0, in the canonical form: the map Sym^d(E) → π_* O(d) of Tag 01NR is an isomorphism, for n ≥ 1”.

The canonical map Sym^d(E) ⟶ π_* 𝒪_{𝐏(E)}(d) is an isomorphism, for n ≥ 1 and d ≥ 0.

public theorem isIso_symToPushforwardTwist (hn : 1 ≤ n) (d : ℕ) : IsIso (D.ψ d)

Stacks.AlgebraicGeometry.ProjectiveBundleCohomology.higherDirectImageZeroIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveBundleCohomology/Statement.lean, line 99. The attribute's comment: “the q = 0 row, d ≥ 0: R^0 π_* O(d) ≅ Sym^d(E), for n ≥ 1”.

R^0 π_* 𝒪_{𝐏(E)}(d) ≅ Sym^d(E) for d ≥ 0: the comparison R^0π_* = π_* of [Stacks, Tag 05TD] followed by the inverse of the canonical map of Tag 01NR.

public def higherDirectImageZeroIso (hn : 1 ≤ n) (d : ℕ) :
    ((Scheme.Modules.pushforward (relativeProj (bundleAlgebra E hfree)).toBase).rightDerivedPlus
      0).obj (D.algebra.piece (d : ℤ)) ≅ (bundleAlgebra E hfree).piece (d : ℤ)

Stacks.AlgebraicGeometry.ProjectiveBundleCohomology.isZero_higherDirectImage_zero_of_neg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveBundleCohomology/Statement.lean, line 107. The attribute's comment: “the q = 0 row, d < 0: R^0 π_* O(d) = 0 = Sym^d(E), for n ≥ 1”.

For d < 0, both R^0 π_* 𝒪_{𝐏(E)}(d) and Sym^d(E) vanish.

public theorem isZero_higherDirectImage_zero_of_neg (hn : 1 ≤ n) {d : ℤ} (hd : d < 0) :
    IsZero (((Scheme.Modules.pushforward
        (relativeProj (bundleAlgebra E hfree)).toBase).rightDerivedPlus
      0).obj (D.algebra.piece d)) ∧ IsZero ((bundleAlgebra E hfree).piece d)

Stacks.AlgebraicGeometry.ProjectiveBundleCohomology.higherDirectImageTopIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveBundleCohomology/Statement.lean, line 122. The attribute's comment: “the q = n row, every integer d: R^n π_* O(d) ≅ SheafHom(Sym^(-n-1-d)(E) ⊗ ∧^(n+1) E, O_S), for E finite locally free of constant rank n + 1 over an arbitrary scheme S, n ≥ 1”. References: EGA III (2.1.16), “(ii)”.

For n ≥ 1 and every integer d, Rⁿ π_* 𝒪_{𝐏(E)}(d) ≅ SheafHom(Sym^{-n-1-d}(E) ⊗ ⋀ⁿ⁺¹ E, 𝒪_S). For d ≤ -n - 1 it is induced by the multiplication pairing 𝒪(d) ⊗ π^* Sym^{-n-1-d}(E) ⟶ 𝒪(-n-1) and the trace Rⁿ π_* 𝒪(-n-1) ≅ (⋀ⁿ⁺¹ E)^∨; for d ≥ -n both sides vanish.

public def higherDirectImageTopIso (hn : 1 ≤ n) (d : ℤ) :
    ((Scheme.Modules.pushforward (relativeProj (bundleAlgebra E hfree)).toBase).rightDerivedPlus
      (n : ℤ)).obj (D.algebra.piece d) ≅
      Stacks.AlgebraicGeometry.ReflexiveModules.dualSheaf
        ((Stacks.ProjectionFormula.tensorRightInvertible S
          (Scheme.Modules.exteriorPower E ((n + 1 : ℕ) : ℤ))).obj
          ((bundleAlgebra E hfree).piece (-(n : ℤ) - 1 - d)))

Stacks.AlgebraicGeometry.ProjectiveBundleVanishing.isZero_rightDerivedPlus_pushforward_twist, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpaceHigherDirectImage/BundleTwistVanishing.lean, line 391. The attribute's comment: “the vanishing clause in the degrees above the relative dimension and below zero”. References: EGA III (2.1.15), “partial”.

The higher direct images of the twists on a projective bundle vanish outside the relative dimension. Let E be an 𝒪_S-module which is finite locally free of constant rank n + 1, let π : 𝐏(E) = Proj_S(Sym(E)) ⟶ S be the structure morphism of its projective bundle and let 𝒪_{𝐏(E)}(d) be the degree-d homogeneous piece of a family of twists on it. Then R^q π_* 𝒪_{𝐏(E)}(d) is zero whenever q < 0 or q > n.

Below degree zero this is the vanishing of any right derived functor in negative degrees. Above degree n the affine opens over which E is free form a basis of S, over such an open the section ring of Sym(E) is generated by n + 1 degree-one elements, and Stacks.AlgebraicGeometry.ProjectiveBundleVanishing.isZero_rightDerivedPlus_pushforward_piece turns that into the vanishing. The vanishing in every degree q ≠ 0, n is Stacks.AlgebraicGeometry.ProjectiveBundleCohomology.isZero_higherDirectImage_twist.

public theorem isZero_rightDerivedPlus_pushforward_twist (n : ℕ)
    (hqc : Stacks.SymGraded.IsQuasicoherentPieces E)
    (hfree : Scheme.Modules.IsFiniteLocallyFreeOfRank E (n + 1))
    (D : TwistData (Stacks.SymGraded.schemeSheafGradedAlgebra E hqc)) (d : ℤ) (q : ℤ)
    (hq : q < 0 ∨ (n : ℤ) < q) :
    IsZero (((Scheme.Modules.pushforward
        (relativeProj (Stacks.SymGraded.schemeSheafGradedAlgebra E hqc)).toBase).rightDerivedPlus
      q).obj (D.algebra.piece d))

Stacks.AlgebraicGeometry.ProjectiveBundleVanishing.TopDegree.topCohomologyTwistIsoSymTensorDet, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpaceHigherDirectImage/TopDegreeTwistIdentification.lean, line 100. The attribute's comment: “the q = n identification for an affine base S = Spec R and a free module E = R^(n+1), n ≥ 1, on the cohomology module H^n(P(E), O(d))”.

The top cohomology of the twists on projective space: for a commutative ring R, for n = m + 1 ≥ 1, an integer d and a natural number k with k = -n - 1 - d,

H^n(𝐏(E), 𝒪(d)) ≅ Hom_R(Sym^k(E) ⊗_R ⋀^{n+1}E, R), E = R^{⊕ n+1},

as R-modules.

public def topCohomologyTwistIsoSymTensorDet (R : Type u) [CommRing R] (m : ℕ) (d : ℤ) (k : ℕ)
    (hk : (k : ℤ) = -((m + 1 : ℕ) : ℤ) - 1 - d) :
    Stacks.ProjectiveSpace.Cohomology.twistCohomology R (m + 1) d (m + 1) ≅
      ModuleCat.of R
        (TensorProduct R (SymPow.symmetricPower k R (Fin (m + 1 + 1) → R))
            (⋀[R]^(m + 1 + 1) (Fin (m + 1 + 1) → R)) →ₗ[R] R)

Sources

Section30.9 Coherent sheaves on locally Noetherian schemes #

Section 30.9 of the Stacks Project, Tag 01XY. 11 tags here are carried by 43 declarations of the repository (all in StacksFrontier) and 7 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01XZ, a lemma

Tag 01XZ in the Stacks Project.

Stacks.AlgebraicGeometry.CoherenceCriteria.coherent_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CoherenceCriteria/Basic.lean, line 168. The attribute's comment: “five equivalent conditions”. References: EGA I (1.5.1), “(a) <=> (b)”.

[Stacks, Tag 01XZ]. On a locally Noetherian scheme the following are equivalent for a module F: it is coherent; it is quasi-coherent and of finite type; it is of finite presentation; on every affine open it is the sheaf associated with a finite module; on the members of some affine open covering it is the sheaf associated with a finite module.

theorem coherent_tfae (X : Scheme.{u}) [IsLocallyNoetherian X] (F : X.Modules) :
    List.TFAE [
      F.IsCoherent,
      F.IsQuasicoherent ∧ F.IsFiniteType,
      F.IsFinitePresentation,
      ∀ (U : X.Opens) (hU : IsAffineOpen U), IsFiniteTildeOn F U hU,
      ∃ (ι : Type u) (U : ι → X.Opens),
        IsOpenCover U ∧ ∀ i, ∃ hU : IsAffineOpen (U i), IsFiniteTildeOn F (U i) hU]

Stacks.AlgebraicGeometry.CoherenceCriteria.structureSheaf_isCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CoherenceCriteria/Basic.lean, line 229. The attribute's comment: “the structure sheaf is coherent”.

[Stacks, Tag 01XZ]. The structure sheaf of a locally Noetherian scheme is coherent.

theorem structureSheaf_isCoherent (X : Scheme.{u}) [IsLocallyNoetherian X] :
    (SheafOfModules.unit X.ringCatSheaf).IsCoherent

Stacks.AlgebraicGeometry.CoherenceCriteria.isCoherent_of_isFiniteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CoherenceCriteria/Basic.lean, line 259. The attribute's comment: “finite locally free modules are coherent”.

[Stacks, Tag 01XZ]. A finite locally free module on a locally Noetherian scheme is coherent.

theorem isCoherent_of_isFiniteLocallyFree (X : Scheme.{u}) [IsLocallyNoetherian X]
    (F : X.Modules) [_root_.AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree
      (C := Opens ↥X) (J := Opens.grothendieckTopology ↥X) F] : F.IsCoherent

Stacks.AlgebraicGeometry.CoherenceCriteria.isCoherent_of_isInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CoherenceCriteria/Basic.lean, line 325. The attribute's comment: “invertible modules are coherent”.

[Stacks, Tag 01XZ]. An invertible module on a locally Noetherian scheme is coherent.

By [Stacks, Tag 0B8N] (b) an invertible module is, on a covering of the whole scheme, a direct summand of a finite free module, hence the kernel of 1 - e for the associated split idempotent; and the structure sheaf is coherent, so Stacks.SheafOfModules.isCoherent_of_locallyKernelFiniteCoproduct applies.

theorem isCoherent_of_isInvertible (X : Scheme.{u}) [IsLocallyNoetherian X] (F : X.Modules)
    [Stacks.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property F] :
    F.IsCoherent

Stacks.AlgebraicGeometry.CoherentKernel.coherent_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CoherentKernel/Basic.lean, line 617. The attribute's comment: “five equivalent conditions”.

The five equivalent conditions of [Stacks, Tag 01XZ] for a module on a locally Noetherian scheme: coherence, quasi-coherence together with finite type, finite presentation, and the two forms — at every affine open and on some affine open covering — of being the sheaf associated to a finite module.

Every implication but the two into (1) was available beforehand; the new one is isCoherent_of_isQuasicoherent_isFiniteType.

theorem coherent_tfae (F : X.Modules) :
    List.TFAE [
      F.IsCoherent,
      F.IsQuasicoherent ∧ F.IsFiniteType,
      F.IsFinitePresentation,
      ∀ (U : X.Opens) (hU : IsAffineOpen U), IsFiniteTildeOn F U hU,
      ∃ (ι : Type u) (U : ι → X.Opens),
        IsOpenCover U ∧ ∀ i, ∃ hU : IsAffineOpen (U i), IsFiniteTildeOn F (U i) hU
    ]

Stacks.AlgebraicGeometry.CoherentKernel.structureSheaf_isCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CoherentKernel/Basic.lean, line 639. The attribute's comment: “the structure sheaf is coherent”.

On a locally Noetherian scheme the structure sheaf is coherent.

theorem structureSheaf_isCoherent : (SheafOfModules.unit X.ringCatSheaf).IsCoherent

Stacks.AlgebraicGeometry.CoherentKernel.isCoherent_of_isFiniteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CoherentKernel/Basic.lean, line 652. The attribute's comment: “finite locally free modules are coherent”.

A finite locally free module on a locally Noetherian scheme is coherent.

theorem isCoherent_of_isFiniteLocallyFree (F : X.Modules)
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree (R := X.ringCatSheaf) F] :
    F.IsCoherent

Stacks.AlgebraicGeometry.CoherentKernel.isCoherent_of_isInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CoherentKernel/Basic.lean, line 662. The attribute's comment: “invertible modules are coherent”.

An invertible module on a locally Noetherian scheme is coherent. An invertible module on a scheme is finite locally free of rank one, by Stacks.SheafRankOne.isFiniteLocallyFreeOfRank_one_of_isInvertible_scheme.

theorem isCoherent_of_isInvertible (F : X.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 F] :
    F.IsCoherent

Stacks.AlgebraicGeometry.CoherentTFAE.tfae_isCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/NoetherianCoherent.lean, line 373.

[Stacks, Tag 01XZ]. For a module on a locally Noetherian scheme the following are equivalent:

it is coherent;

it is quasi-coherent and of finite type;

it is of finite presentation;

on every affine open U it is the tilde of a finite Γ(X, U)-module;

the same on the members of some affine open covering.

The implications not using the Noetherian hypothesis are the ones already proved in StacksFrontier/AlgebraicGeometry/CoherentTFAE/ and StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/FiniteTilde.lean; the one that uses it is (2) ⇒ (1).

theorem tfae_isCoherent (F : X.Modules) :
    List.TFAE
      [_root_.SheafOfModules.IsCoherent F,
        F.IsQuasicoherent ∧ SheafOfModules.IsFiniteType.{u, u, u} F,
        F.IsFinitePresentation,
        ∀ (U : X.Opens) (hU : IsAffineOpen U), IsFiniteTildeOn F U hU,
        ∃ (ι : Type u) (U : ι → X.Opens),
          IsOpenCover U ∧ ∀ i, ∃ hU : IsAffineOpen (U i), IsFiniteTildeOn F (U i) hU]

Stacks.AlgebraicGeometry.CoherentTFAE.coherent_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/LocallyNoetherian/Coherent.lean, line 57. The attribute's comment: “five equivalent conditions”.

Stacks Project, Tag 01XZ. The five characterizations of a coherent module on a locally Noetherian scheme.

theorem coherent_tfae (X : Scheme.{u}) [IsLocallyNoetherian X]
    (F : X.Modules) :
    List.TFAE [
      F.IsCoherent,
      F.IsQuasicoherent ∧ F.IsFiniteType,
      F.IsFinitePresentation,
      ∀ (U : X.Opens) (hU : IsAffineOpen U), IsFiniteTildeOn F U hU,
      ∃ (ι : Type u) (U : ι → X.Opens),
        IsOpenCover U ∧ ∀ i, ∃ hU : IsAffineOpen (U i), IsFiniteTildeOn F (U i) hU
    ]

Stacks.AlgebraicGeometry.CoherentTFAE.structureSheaf_isCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/LocallyNoetherian/Coherent.lean, line 83. The attribute's comment: “the structure sheaf is coherent”.

Stacks Project, Tag 01XZ. On a locally Noetherian scheme the structure sheaf is coherent.

theorem structureSheaf_isCoherent (X : Scheme.{u}) [IsLocallyNoetherian X] :
    (SheafOfModules.unit X.ringCatSheaf).IsCoherent

Stacks.AlgebraicGeometry.CoherentTFAE.isCoherent_of_isFiniteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/LocallyNoetherian/Coherent.lean, line 89. The attribute's comment: “finite locally free modules are coherent”.

Stacks Project, Tag 01XZ. A finite locally free module on a locally Noetherian scheme is coherent.

theorem isCoherent_of_isFiniteLocallyFree (X : Scheme.{u}) [IsLocallyNoetherian X]
    (F : X.Modules) [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree
      (C := Opens X) (J := Opens.grothendieckTopology X) F] :
    F.IsCoherent

Tag 01Y0, a lemma

Tag 01Y0 in the Stacks Project.

AlgebraicGeometry.isCoherent_kernel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CoherentSubquotients/Abelian.lean, line 71. The attribute's comment: “kernel”.

[Stacks, Tag 01Y0]. The kernel of a map of coherent modules on a locally Noetherian scheme is coherent.

theorem isCoherent_kernel {X : Scheme.{u}} [IsLocallyNoetherian X] {F G : X.Modules}
    [F.IsCoherent] [G.IsCoherent] (φ : F ⟶ G) : (kernel φ).IsCoherent

AlgebraicGeometry.isCoherent_cokernel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CoherentSubquotients/Abelian.lean, line 78. The attribute's comment: “cokernel”.

[Stacks, Tag 01Y0]. The cokernel of a map of coherent modules on a locally Noetherian scheme is coherent.

theorem isCoherent_cokernel {X : Scheme.{u}} [IsLocallyNoetherian X] {F G : X.Modules}
    [F.IsCoherent] [G.IsCoherent] (φ : F ⟶ G) : (cokernel φ).IsCoherent

AlgebraicGeometry.isCoherent_X₂_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CoherentSubquotients/Abelian.lean, line 86. The attribute's comment: “extensions”.

[Stacks, Tag 01Y0]. An extension of coherent modules on a locally Noetherian scheme is coherent: the middle term of a short exact sequence of 𝒪_X-modules whose outer terms are coherent is coherent.

theorem isCoherent_X₂_of_shortExact {X : Scheme.{u}} [IsLocallyNoetherian X]
    {S : ShortComplex X.Modules} (hS : S.ShortExact)
    (h₁ : S.X₁.IsCoherent) (h₃ : S.X₃.IsCoherent) : S.X₂.IsCoherent

AlgebraicGeometry.nonempty_abelian_coherentModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CoherentSubquotients/Abelian.lean, line 96. The attribute's comment: “abelian category”.

[Stacks, Tag 01Y0]. The category of coherent 𝒪_X-modules on a locally Noetherian scheme is abelian. The abelian structure is the one a weak Serre subcategory of an abelian category carries, by [Stacks, Tag 0754].

theorem nonempty_abelian_coherentModules (X : Scheme.{u}) [IsLocallyNoetherian X] :
    Nonempty (Abelian (ObjectProperty.FullSubcategory (fun F : X.Modules => F.IsCoherent)))

Declarations registered for the tag:

Stacks.SheafOfModules.coherentModulesAbelian, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/AbelianCategory.lean, line 43 (StacksFrontier): “abelian category”.
Stacks.SheafOfModules.isCoherent_kernel, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/AbelianCategory.lean, line 44 (StacksFrontier): “kernel”.
Stacks.SheafOfModules.coherentModules_isClosedUnderCokernels, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/AbelianCategory.lean, line 45 (StacksFrontier): “cokernel”.
Stacks.SheafOfModules.isCoherent_X₂_of_shortExact, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/AbelianCategory.lean, line 46 (StacksFrontier): “extensions”.

Tag 01Y1, a lemma

Tag 01Y1 in the Stacks Project.

Stacks.AlgebraicGeometry.CoherentOfFiniteType.isCoherent_of_mono_of_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CoherentOfFiniteType.lean, line 195. The attribute's comment: “quasi_coherent_submodule”. References: EGA I (9.6.4), “submodule, B = O_X”.

Stacks 01Y1, submodules. A quasi-coherent submodule of a coherent module on a locally Noetherian scheme is coherent.

This carries the tag, and with the quotient statement below 01Y1's covering set is complete. The source (coherent.tex:2364) states exactly two assertions — "Any quasi-coherent submodule of F is coherent. Any quasi-coherent quotient module of F is coherent." — and one declaration is tagged for each. Both are proved here, so the attribute is not an over-claim.

theorem isCoherent_of_mono_of_isQuasicoherent {G F : X.Modules} [G.IsQuasicoherent]
    (hF : _root_.SheafOfModules.IsCoherent F) (ι : G ⟶ F) [Mono ι] :
    _root_.SheafOfModules.IsCoherent G

Stacks.AlgebraicGeometry.CoherentOfFiniteType.isCoherent_of_epi_of_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CoherentOfFiniteType.lean, line 206. The attribute's comment: “quasi_coherent_quotient”. References: EGA I (9.6.4), “quotient, B = O_X”.

Stacks 01Y1, quotients. A quasi-coherent quotient of a coherent module on a locally Noetherian scheme is coherent. This is the second of 01Y1's two assertions; see the submodule statement above for why the tag is complete here.

theorem isCoherent_of_epi_of_isQuasicoherent {F Q : X.Modules} [Q.IsQuasicoherent]
    (hF : _root_.SheafOfModules.IsCoherent F) (p : F ⟶ Q) [Epi p] :
    _root_.SheafOfModules.IsCoherent Q

Stacks.AlgebraicGeometry.CoherentSubquotients.isCoherent_of_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CoherentSubquotients/Basic.lean, line 66. The attribute's comment: “quasi_coherent_quotient”. References: EGA I (9.6.4), “quotient, B = O_X”.

[Stacks, Tag 01Y1]. A quasi-coherent quotient of a coherent sheaf of modules on a locally Noetherian scheme is coherent.

theorem isCoherent_of_epi {X : Scheme.{u}} [IsLocallyNoetherian X]
    {F G : X.Modules} [hF : F.IsCoherent] [G.IsQuasicoherent]
    (f : F ⟶ G) [Epi f] : G.IsCoherent

Stacks.AlgebraicGeometry.CoherentSubquotients.isCoherent_of_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CoherentSubquotients/Basic.lean, line 191. The attribute's comment: “quasi_coherent_submodule”.

[Stacks, Tag 01Y1]. A quasi-coherent submodule of a coherent sheaf of modules on a locally Noetherian scheme is coherent.

theorem isCoherent_of_mono {X : Scheme.{u}} [IsLocallyNoetherian X]
    {F G : X.Modules} [F.IsCoherent] [G.IsQuasicoherent]
    (f : G ⟶ F) [Mono f] : G.IsCoherent

Stacks.AlgebraicGeometry.CoherentTFAE.isCoherent_of_epi_of_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/LocallyNoetherian/SubQuotient.lean, line 56. The attribute's comment: “quasi_coherent_quotient”.

Stacks Project, Tag 01Y1. A quasi-coherent quotient of a coherent module on a locally Noetherian scheme is coherent.

theorem isCoherent_of_epi_of_isQuasicoherent [IsLocallyNoetherian X]
    {F G : X.Modules} [F.IsCoherent] [G.IsQuasicoherent]
    (f : F ⟶ G) [Epi f] : G.IsCoherent

Stacks.AlgebraicGeometry.CoherentTFAE.isCoherent_of_mono_of_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/LocallyNoetherian/SubQuotient.lean, line 75. The attribute's comment: “quasi_coherent_submodule”.

Stacks Project, Tag 01Y1. A quasi-coherent submodule of a coherent module on a locally Noetherian scheme is coherent.

theorem isCoherent_of_mono_of_isQuasicoherent [IsLocallyNoetherian X]
    {F G : X.Modules} [F.IsCoherent] [G.IsQuasicoherent]
    (f : G ⟶ F) [Mono f] : G.IsCoherent

Tag 01Y2, a lemma

Tag 01Y2 in the Stacks Project.

AlgebraicGeometry.SheafOfModules.tensorSheaf_isCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TensorCoherence/Basic.lean, line 556. The attribute's comment: “tensor product”. References: EGA 0 (5.3.5), “tensor product”; EGA I (9.1.1), “coherent tensor”.

The tensor product of two coherent sheaves of modules is coherent.

theorem tensorSheaf_isCoherent (X : AlgebraicGeometry.RingedSpace.{u, u})
    (F G : _root_.SheafOfModules.{u}
      (structureSheafRing X))
    [_root_.SheafOfModules.IsCoherent F] [_root_.SheafOfModules.IsCoherent G] :
    _root_.SheafOfModules.IsCoherent ((((Stacks.SheafOfModules.Tensor.sheafTensor ⟨((X)).presheaf,
        ((X)).IsSheaf⟩).obj (F)).obj (G)))

Stacks.AlgebraicGeometry.TensorHomCoherent.isCoherent_sheafInternalHom_of_isCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TensorHomCoherent/Basic.lean, line 104. The attribute's comment: “sheaf-hom”. References: EGA I (9.1.1), “more general”.

The sheaf-hom clause of [Stacks, Tag 01Y2]. On a ringed space, the sheaf-hom SheafHom(ℱ, 𝒢) between two coherent modules is coherent.

A coherent module is of finite presentation ([Stacks, Tag 01BW] (1)), and the sheaf-hom from a module of finite presentation into a coherent module is coherent ([Stacks, Tag 01CQ] (2)). The source states this for a locally Noetherian scheme; see isCoherent_sheafHom below for that statement.

theorem isCoherent_sheafInternalHom_of_isCoherent {Y : Type u} [TopologicalSpace Y]
    (O : Sheaf (Opens.grothendieckTopology Y) CommRingCat.{u})
    (F G : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf (spaceRingedSite O).O))
    [_root_.SheafOfModules.IsCoherent F] [_root_.SheafOfModules.IsCoherent G] :
    _root_.SheafOfModules.IsCoherent (sheafInternalHom (spaceRingedSite O) F G)

Stacks.AlgebraicGeometry.TensorHomCoherent.isCoherent_sheafHom, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TensorHomCoherent/Basic.lean, line 137. The attribute's comment: “sheaf-hom, as the source states it: locally Noetherian scheme”.

[Stacks, Tag 01Y2], the sheaf-hom clause. Let X be a locally Noetherian scheme and let ℱ, 𝒢 be coherent 𝒪_X-modules. Then SheafHom_{𝒪_X}(ℱ, 𝒢) is coherent.

This is isCoherent_sheafInternalHom_of_isCoherent at the site of opens of X with its structure sheaf; the Noetherian condition is the source's and is not used.

instance isCoherent_sheafHom (X : Scheme.{u}) [IsLocallyNoetherian X] (F G : X.Modules)
    [hF : _root_.SheafOfModules.IsCoherent F] [hG : _root_.SheafOfModules.IsCoherent G] :
    _root_.SheafOfModules.IsCoherent (sheafInternalHom (spaceRingedSite X.sheaf) F G)

Stacks.AlgebraicGeometry.TensorHomCoherent.isCoherent_tensorObj, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TensorHomCoherent/Basic.lean, line 149. The attribute's comment: “tensor product, as the source states it: locally Noetherian scheme”.

[Stacks, Tag 01Y2], the tensor-product clause. Let X be a locally Noetherian scheme and let ℱ, 𝒢 be coherent 𝒪_X-modules. Then ℱ ⊗_{𝒪_X} 𝒢 is coherent.

This is AlgebraicGeometry.SheafOfModules.tensorSheaf_isCoherent, which carries the tag, read at the AlgebraicGeometry.Scheme.Modules.tensorObj spelling of the tensor product; the Noetherian condition is the source's and is not used.

instance isCoherent_tensorObj (X : Scheme.{u}) [IsLocallyNoetherian X] (F G : X.Modules)
    [hF : _root_.SheafOfModules.IsCoherent F] [hG : _root_.SheafOfModules.IsCoherent G] :
    _root_.SheafOfModules.IsCoherent (Scheme.Modules.tensorObj F G)

Tag 01Y3, a lemma

Tag 01Y3 in the Stacks Project.

AlgebraicGeometry.exists_epi_over_of_stalk_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/LocalSurjectivity.lean, line 114. The attribute's comment: “part (3)”.

Stacks Project, Tag 01Y3. A morphism with finite-type target which is surjective on one stalk is an epimorphism after restriction to a neighbourhood of that point.

public theorem exists_epi_over_of_stalk_surjective {F G : SheafOfModules.{u} R}
    [F.IsFiniteType] (φ : G ⟶ F) (x : X)
    (hx : Function.Surjective
      (ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor AddCommGrpCat.{u} x).map
        ((PresheafOfModules.toPresheaf R.obj).map φ.val)))) :
    ∃ U : Opens X, x ∈ U ∧ Epi (φ.over U)

AlgebraicGeometry.exists_isZero_over_of_stalk_isZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/LocalSurjectivity.lean, line 126. The attribute's comment: “part (1)”. References: EGA 0 (5.2.2), “support closed”.

Stacks Project, Tag 01Y3. A finite-type sheaf whose stalk vanishes at a point vanishes on a neighbourhood of that point.

public theorem exists_isZero_over_of_stalk_isZero (F : SheafOfModules.{u} R)
    [F.IsFiniteType] (x : X)
    (hx : IsZero (TopCat.Presheaf.stalk (C := Ab.{u}) F.val.presheaf x)) :
    ∃ U : Opens X, x ∈ U ∧ IsZero (F.over U)

AlgebraicGeometry.exists_isIso_over_of_stalk_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/LocalSurjectivity.lean, line 159. The attribute's comment: “part (4)”.

Stacks Project, Tag 01Y3. A morphism from a module of finite type to a coherent module which is bijective on the stalk at a point is an isomorphism after restriction to a neighbourhood of that point.

public theorem exists_isIso_over_of_stalk_isIso {F G : SheafOfModules.{u} R}
    [F.IsCoherent] [G.IsFiniteType] (φ : G ⟶ F) (x : X)
    (hx : IsIso ((TopCat.Presheaf.stalkFunctor AddCommGrpCat.{u} x).map
      ((PresheafOfModules.toPresheaf R.obj).map φ.val))) :
    ∃ U : Opens X, x ∈ U ∧ IsIso (φ.over U)

Stacks.AlgebraicGeometry.Tag01Y3LocalIso.exists_isIso_over_of_stalk_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalIso/Basic.lean, line 293. The attribute's comment: “part (4)”.

Part (4) of [Stacks, Tag 01Y3]. A map from a finite-type module sheaf to a coherent module sheaf which is an isomorphism on one stalk is an isomorphism after restriction to a neighbourhood of that point.

theorem exists_isIso_over_of_stalk_isIso {F G : SheafOfModules.{u} R}
    [F.IsCoherent] [G.IsFiniteType] (φ : G ⟶ F) (x : X)
    (hx : IsIso ((TopCat.Presheaf.stalkFunctor AddCommGrpCat.{u} x).map
      ((PresheafOfModules.toPresheaf R.obj).map φ.val))) :
    ∃ U : Opens X, x ∈ U ∧ IsIso (φ.over U)

Declarations registered for the tag:

AlgebraicGeometry.exists_isMono_over_of_stalk_injective, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/LocalIsomorphism.lean, line 156 (StacksFrontier): “part (2)”.
Stacks.AlgebraicGeometry.Tag01Y3LocalIso.exists_isMono_over_of_stalk_injective, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/LocalIso/Basic.lean, line 286 (StacksFrontier): “part (2)”.

Tag 01Y4, a lemma

Tag 01Y4 in the Stacks Project.

Stacks.SheafOfModules.SheafHomStalk.exists_localHom_of_stalkLinearMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/LocalHom.lean, line 86.

Stacks Project, Tag 01Y4. A linear map out of the stalk of a finitely presented sheaf of modules on a ringed space is represented by a homomorphism on some open neighbourhood.

theorem exists_localHom_of_stalkLinearMap (X : TopCat.{u})
    (Rc : TopCat.Sheaf CommRingCat.{u} X)
    (G F : SheafOfModules.{u} (structureSheaf Rc))
    [G.IsFinitePresentation] (x : X)
    (ψ : TopCat.Presheaf.stalk (C := Ab.{u})
        (commVal G).presheaf x →ₗ[TopCat.Presheaf.stalk
          (C := CommRingCat.{u}) Rc.obj x]
      TopCat.Presheaf.stalk (C := Ab.{u}) (commVal F).presheaf x) :
    ∃ (U : Opens X) (_hxU : x ∈ U) (φ : G.over U ⟶ F.over U),
      ∀ (V : Opens X) (hVU : V ≤ U) (hxV : x ∈ V) (m : G.val.obj (op V)),
        TopCat.Presheaf.germ (C := Ab.{u}) F.val.presheaf V x hxV
            ((φ.val.app (op (Over.mk (homOfLE hVU)))) m) =
          ψ (TopCat.Presheaf.germ (C := Ab.{u}) G.val.presheaf V x hxV m)

Tag 01Y5, a lemma

Tag 01Y5 in the Stacks Project.

AlgebraicGeometry.Scheme.Modules.exists_coherent_module_on_schemeTheoreticSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Support/SchemeTheoreticCoherent.lean, line 72. The attribute's comment: “descent to a coherent module on the scheme-theoretic support”.

[Stacks, Tag 01Y5]. A coherent module on a locally Noetherian scheme is the direct image of a coherent module on its scheme-theoretic support.

theorem exists_coherent_module_on_schemeTheoreticSupport :
    ∃ G : (schemeTheoreticSupport F).subscheme.Modules,
      G.IsCoherent ∧
        Nonempty ((Scheme.Modules.pushforward
          (schemeTheoreticSupport F).subschemeι).obj G ≅ F)

Declarations registered for the tag:

SheafOfModules.isClosed_supp, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/Support/SchemeTheoreticCoherent.lean, line 50 (StacksFrontier): “closedness of the support”.

Tag 087T, a lemma

Tag 087T in the Stacks Project.

Stacks.ClosedImmersion.pushforwardCoh, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ClosedPushforward/Coherent.lean, line 170. The attribute's comment: “the induced functor”.

[Stacks, Tag 087T], the induced functor. Direct image along a closed immersion of locally Noetherian schemes carries a coherent 𝒪_Z-module to a coherent 𝒪_X-module annihilated by the ideal sheaf cutting out Z, hence induces a functor Coh(𝒪_Z) ⥤ {ℱ ∈ Coh(𝒪_X) | ℐℱ = 0}.

def pushforwardCoh :
    _root_.AlgebraicGeometry.SheafOfModules.CoherentModules Z.ringCatSheaf ⥤
      (coherentAnnihilatedByKer i).FullSubcategory

Stacks.ClosedImmersion.pushforwardCohEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ClosedPushforward/Coherent.lean, line 230. The attribute's comment: “the equivalence”.

[Stacks, Tag 087T]. Let i : Z ⟶ X be a closed immersion of locally Noetherian schemes and let ℐ ⊆ 𝒪_X be the quasi-coherent sheaf of ideals cutting out Z. Direct image along i is an equivalence from the category of coherent 𝒪_Z-modules to the category of coherent 𝒪_X-modules annihilated by ℐ.

The functor of this equivalence is Stacks.ClosedImmersion.pushforwardCoh, which composed with the inclusion of the full subcategory is AlgebraicGeometry.Scheme.Modules.pushforward i, by pushforwardCoh_comp_ι.

def pushforwardCohEquivalence :
    _root_.AlgebraicGeometry.SheafOfModules.CoherentModules Z.ringCatSheaf ≌
      (coherentAnnihilatedByKer i).FullSubcategory

AlgebraicGeometry.isCoherent_pushforward_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ClosedPushforward/Coherent.lean, line 268. The attribute's comment: “coherence of the direct image”.

[Stacks, Tag 087T], coherence of the direct image. The direct image of a coherent module along a closed immersion into a locally Noetherian scheme is coherent.

Local Noetherianity of the source is not assumed: it follows from that of the target by isLocallyNoetherian_of_isClosedImmersion.

theorem isCoherent_pushforward_of_isClosedImmersion
    [IsClosedImmersion i] [IsLocallyNoetherian X] (G : Z.Modules) [G.IsCoherent] :
    ((Scheme.Modules.pushforward i).obj G).IsCoherent

AlgebraicGeometry.exists_isCoherent_pushforward_iso_of_smul_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ClosedPushforward/Coherent.lean, line 283. The attribute's comment: “essential surjectivity onto coherent modules”.

[Stacks, Tag 087T], essential surjectivity. A coherent module on X annihilated, section by section, by the kernel of the comorphism of a closed immersion i : Z ⟶ X is the direct image along i of a coherent module on Z.

The module on Z is i^* M: it is coherent because Z is locally Noetherian and the pullback of a coherent module is coherent, and the unit M ⟶ i_* i^* M is an isomorphism by Stacks.ClosedImmersion.isIso_unit_app_of_smul_eq_zero.

theorem exists_isCoherent_pushforward_iso_of_smul_eq_zero
    [IsClosedImmersion i] [IsLocallyNoetherian X] (M : X.Modules) [M.IsCoherent]
    (h : ∀ (U : X.Opens) (a : Γ(X, U)), (i.app U).hom a = 0 → ∀ m : Γ(M, U), a • m = 0) :
    ∃ G : Z.Modules, G.IsCoherent ∧
      Nonempty ((Scheme.Modules.pushforward i).obj G ≅ M)

AlgebraicGeometry.exists_isCoherent_pushforward_iso_iff_smul_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ClosedPushforward/Coherent.lean, line 303. The attribute's comment: “the essential image on coherent modules”.

[Stacks, Tag 087T], the essential image on coherent modules. A coherent module on X is the direct image of a coherent module on Z exactly when the kernel of the comorphism of the closed immersion annihilates it section by section.

This is the characterisation of the essential image of i_* restricted to coherent modules: the forward implication is the general essential-image criterion Stacks.ClosedImmersion.pushforward_essImage_iff, which needs no coherence at all, and the reverse one is exists_isCoherent_pushforward_iso_of_smul_eq_zero.

theorem exists_isCoherent_pushforward_iso_iff_smul_eq_zero
    [IsClosedImmersion i] [IsLocallyNoetherian X] (M : X.Modules) [M.IsCoherent] :
    (∃ G : Z.Modules, G.IsCoherent ∧
        Nonempty ((Scheme.Modules.pushforward i).obj G ≅ M)) ↔
      ∀ (U : X.Opens) (a : Γ(X, U)), (i.app U).hom a = 0 → ∀ m : Γ(M, U), a • m = 0

Stacks.AlgebraicGeometry.Tag087TCoherentImage.coherentPushforwardEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CoherentImage/Basic.lean, line 236.

[Stacks, Tag 087T]. Direct image along a closed immersion of locally Noetherian schemes is an equivalence from the coherent modules on the source onto the coherent modules on the target annihilated by the defining ideal, and the equivalence is the one induced by direct image.

The second component of the pair is ObjectProperty.liftCompιIso, which is Iso.refl: the functor was built as the lift of ι ⋙ i_*, so no identification is needed.

def coherentPushforwardEquivalence :
    Σ e : CoherentModulesOn Z ≌ CoherentAnnihilatedModules i,
      e.functor ⋙ ObjectProperty.ι
          (fun M : X.Modules => M.IsCoherent ∧ AnnihilatedByKer i M) ≅
        ObjectProperty.ι (fun M : Z.Modules => M.IsCoherent) ⋙ Scheme.Modules.pushforward i

Tag 01Y6, a lemma

Tag 01Y6 in the Stacks Project.

Stacks.AlgebraicGeometry.FiniteDirectImageCoherent.isCoherent_pushforward_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FiniteDirectImageCoherent/Basic.lean, line 166. The attribute's comment: “the direct image is coherent”. References: EGA III (3.2.2), “finite case”; EGA III (4.8.6), “scheme case”.

The direct image of a coherent module along a finite morphism to a locally Noetherian scheme is coherent.

It is quasi-coherent because a finite morphism is affine, and on every affine open of the target its sections form a finite module, which is condition (5) of [Stacks, Tag 01XZ].

theorem isCoherent_pushforward_of_isFinite {X S : Scheme.{u}} (f : X ⟶ S) [IsFinite f]
    [IsLocallyNoetherian S] (F : X.Modules) [F.IsCoherent] :
    ((Scheme.Modules.pushforward f).obj F).IsCoherent

Stacks.AlgebraicGeometry.FiniteDirectImageCoherent.isZero_higherDirectImage_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FiniteDirectImageCoherent/Basic.lean, line 178. The attribute's comment: “the higher direct images vanish”.

The higher direct images of a quasi-coherent module along a finite morphism vanish in positive degrees, a finite morphism being affine; this is [Stacks, Tag 01XC]. No hypothesis on the target is used.

theorem isZero_higherDirectImage_of_isFinite {X S : Scheme.{u}} (f : X ⟶ S) [IsFinite f]
    (F : X.Modules) [F.IsQuasicoherent] (p : ℤ) (hp : 0 < p) :
    IsZero (((Scheme.Modules.pushforward f).rightDerivedPlus p).obj F)

Tag 0B3J, a lemma

Tag 0B3J in the Stacks Project.

AlgebraicGeometry.nonempty_generatingSections_of_support_dim_le_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/GlobalGeneration/ZeroDimensionalSupport.lean, line 270. The attribute's comment: “global_generation”.

A coherent sheaf with support of dimension at most zero on a locally Noetherian scheme is generated by global sections.

This is also clause (1) of Stacks 0AYT, in a form more general than that clause states it: Stacks 0AYT takes X proper over a field k, which gives IsLocallyNoetherian X through LocallyOfFiniteType.isLocallyNoetherian, so the condition here is strictly weaker than the clause's and the clause follows by instantiation.

public theorem nonempty_generatingSections_of_support_dim_le_zero
    {X : Scheme.{u}} [IsLocallyNoetherian X] (F : X.Modules) [F.IsCoherent]
    (hF : topologicalKrullDim (SheafOfModules.supp F) ≤ 0) :
    Nonempty F.GeneratingSections

AlgebraicGeometry.isZero_hgroup_top_of_support_dim_le_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/ZeroDimensionalSupport/HigherVanishing.lean, line 80. The attribute's comment: “vanishing”.

[Stacks, Tag 0B3J], the vanishing clause. For X a locally Noetherian scheme and ℱ a coherent 𝒪_X-module whose support has dimension at most zero, Hⁱ(X, ℱ) = 0 for every i > 0.

The global generation clause of the same tag is AlgebraicGeometry.nonempty_generatingSections_of_support_dim_le_zero.

theorem isZero_hgroup_top_of_support_dim_le_zero
    {X : Scheme.{u}} [IsLocallyNoetherian X] (F : X.Modules) [F.IsCoherent]
    (hF : topologicalKrullDim (SheafOfModules.supp F) ≤ 0)
    (i : ℕ) (hi : 0 < i) :
    IsZero (Hgroup X.ringCatSheaf ⊤ i F)

Tag 0CYJ, a lemma

Tag 0CYJ in the Stacks Project.

Stacks.AlgebraicGeometry.CoherentPushforward.isCoherent_pushforward_of_supp_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/LocallyNoetherian/PushforwardSupport.lean, line 350.

A coherent sheaf on an open subscheme, supported on a closed subset contained in that open, has coherent direct image.

theorem isCoherent_pushforward_of_supp_subset {X : Scheme.{u}} (U : X.Opens) (T : Set X)
    (hT : IsClosed T) (hTU : T ⊆ U)
    (F : (U : Scheme.{u}).Modules) [F.IsCoherent]
    (hF : U.ι.base '' SheafOfModules.supp F ⊆ T) :
    ((Scheme.Modules.pushforward U.ι).obj F).IsCoherent

Sources

LeanStacks.AlgebraicGeometry.CoherenceCriteria.coherent_tfae · Stacks.AlgebraicGeometry.CoherenceCriteria.structureSheaf_isCoherent · Stacks.AlgebraicGeometry.CoherenceCriteria.isCoherent_of_isFiniteLocallyFree · Stacks.AlgebraicGeometry.CoherenceCriteria.isCoherent_of_isInvertible · Stacks.AlgebraicGeometry.CoherentKernel.coherent_tfae · Stacks.AlgebraicGeometry.CoherentKernel.structureSheaf_isCoherent · Stacks.AlgebraicGeometry.CoherentKernel.isCoherent_of_isFiniteLocallyFree · Stacks.AlgebraicGeometry.CoherentKernel.isCoherent_of_isInvertible

Section30.10 Coherent sheaves on Noetherian schemes #

Section 30.10 of the Stacks Project, Tag 01Y7. 6 tags here are carried by 9 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01Y8, a lemma

Tag 01Y8 in the Stacks Project.

AlgebraicGeometry.exists_eventually_constant_quasicoherentSubobjects, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/AscendingChain.lean, line 270.

Stacks Project, Tag 01Y8. An ascending chain of quasi-coherent submodules of a coherent sheaf on a Noetherian scheme eventually stabilizes.

public theorem exists_eventually_constant_quasicoherentSubobjects
    (X : Scheme.{u}) [IsNoetherian X] (F : X.Modules) [F.IsCoherent]
    (G : ℕ → Subobject F) (hG : ∀ n, (G n : X.Modules).IsQuasicoherent)
    (hmono : Monotone G) :
    ∃ n, ∀ m, n ≤ m → G m = G n

Tag 01Y9, a lemma

Tag 01Y9 in the Stacks Project.

AlgebraicGeometry.exists_idealPowerMultiple_eq_bot_iff_supp_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/IdealPowerAnnihilation.lean, line 159. References: EGA I (9.3.4).

Stacks Project, Tag 01Y9. Let ℱ be a coherent module on a Noetherian scheme X and let ℐ ⊆ 𝒪_X be a quasi-coherent sheaf of ideals, cutting out the closed subscheme Z ⊆ X. Then some power of ℐ annihilates ℱ if and only if the support of ℱ is contained in Z.

theorem exists_idealPowerMultiple_eq_bot_iff_supp_subset {X : Scheme.{u}} [IsNoetherian X]
    (F : X.Modules) [F.IsCoherent] (I : X.IdealSheafData) :
    (∃ n : ℕ, idealPowerMultiple I n F = ⊥) ↔
      SheafOfModules.supp F ⊆ (I.support : Set X)

Stacks.IdealPowerSupport.exists_idealPowerMultiple_eq_bot_iff_supp_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/IdealPowerSupport.lean, line 230. References: EGA I (9.3.4).

Stacks Project, Tag 01Y9. Let X be a Noetherian scheme, I a quasi-coherent sheaf of ideals and F a coherent 𝒪_X-module — here a quasi-coherent module of finite type, which on a locally Noetherian scheme is the same thing by Tag 01XZ. Then some power of I annihilates F if and only if the support of F is contained in the closed set cut out by I.

Both directions are affine-local, with the algebraic content supplied by Tag 00L6 over the Noetherian ring of sections on an affine open: a power of an ideal kills a finite module exactly when the support of the module lies in the zero locus of the ideal. For the forward direction one affine open containing the point suffices. For the converse the exponent must be chosen uniformly, and that is where quasi-compactness enters: finitely many affine opens cover X, the largest of their exponents works on each of them, and smul_pow_eq_bot_of_le carries the vanishing from a member of the cover to any affine open inside it, which is enough to conclude by sheaf separation.

public theorem exists_idealPowerMultiple_eq_bot_iff_supp_subset {X : Scheme.{u}}
    [IsNoetherian X] (F : X.Modules) [_root_.SheafOfModules.IsCoherent F]
    (I : X.IdealSheafData) :
    (∃ n : ℕ, idealPowerMultiple I n F = ⊥) ↔
      SheafOfModules.supp F ⊆ (I.support : Set X)

Tag 01YA, a lemma

Tag 01YA in the Stacks Project.

AlgebraicGeometry.exists_ideal_pow_smul_inf_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/ArtinRees.lean, line 301. References: EGA 0 (7.3.2.1).

Stacks Project, Tag 01YA. Artin-Rees for a coherent sheaf and a quasi-coherent subsheaf on a Noetherian scheme: the equality holds on every affine open with a single constant.

theorem exists_ideal_pow_smul_inf_eq {X : Scheme.{u}} [IsNoetherian X]
    (F : X.Modules) [F.IsCoherent]
    (G : F.Submodule) [G.toSheafOfModules.IsQuasicoherent]
    (I : (SheafOfModules.unit X.ringCatSheaf).Submodule)
    [I.toSheafOfModules.IsQuasicoherent] :
    ∃ c : ℕ, ∀ n : ℕ, c ≤ n → ∀ U : X.affineOpens,
      (show Ideal Γ(X, U.1) from I.toSubmodule.obj (op U.1)) ^ (n - c) •
          (((show Ideal Γ(X, U.1) from I.toSubmodule.obj (op U.1)) ^ c •
            (⊤ : Submodule Γ(X, U.1) Γ(F, U.1))) ⊓
            G.toSubmodule.obj (op U.1)) =
        ((show Ideal Γ(X, U.1) from I.toSubmodule.obj (op U.1)) ^ n •
          (⊤ : Submodule Γ(X, U.1) Γ(F, U.1))) ⊓
          G.toSubmodule.obj (op U.1)

Tag 0GN6, a lemma

Tag 0GN6 in the Stacks Project.

AlgebraicGeometry.coherentSubobject_isFiltered, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/FilteredColimit.lean, line 121. The attribute's comment: “directedness”. References: EGA I (1.5.4), “filtered system”.

Stacks Project, Tag 0GN6 (directedness). The coherent submodules of a quasi-coherent module on a Noetherian scheme form a filtered category.

instance coherentSubobject_isFiltered {X : Scheme.{u}} (F : X.Modules)
    [IsNoetherian X] [F.IsQuasicoherent] : IsFiltered (CoherentSubobject F)

AlgebraicGeometry.isColimit_coherentSubobjectCocone, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/FilteredColimit.lean, line 128. The attribute's comment: “colimit”. References: EGA I (1.5.4), “colimit”; EGA I (9.4.9), “Noetherian scheme”.

Stacks Project, Tag 0GN6 (colimit). A quasi-coherent module on a Noetherian scheme is the filtered colimit of its coherent submodules.

noncomputable def isColimit_coherentSubobjectCocone {X : Scheme.{u}} (F : X.Modules)
    [IsNoetherian X] [F.IsQuasicoherent] :
    IsColimit (coherentSubobjectCocone F)

Tag 01YB, a lemma

Tag 01YB in the Stacks Project.

Stacks.AlgebraicGeometry.IdealPowerColimit.canonicalMapToHomRestrict_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Coherent/HomColimit/FirstDisplaySurjectivity.lean, line 295. The attribute's comment: “first display”. References: SGA 2 II (Theorem6), “b)”.

For a Noetherian scheme X, a quasi-coherent sheaf of ideals I with complement U = X \ V(I), a coherent 𝒪_X-module G and a quasi-coherent 𝒪_X-module F, the canonical map

colim_n Hom_{𝒪_X}(Iⁿ G, F) ⟶ Hom_{𝒪_U}(G|_U, F|_U)

is bijective.

public theorem canonicalMapToHomRestrict_bijective [AlgebraicGeometry.IsNoetherian X]
    (I : X.IdealSheafData) (G F : X.Modules) [G.IsCoherent] [F.IsQuasicoherent] :
    Function.Bijective (canonicalMapToHomRestrict I G F)

Stacks.AlgebraicGeometry.IdealPowerColimit.canonicalMapToSections_bijective_of_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Coherent/HomColimit/GlobalSections.lean, line 496. The attribute's comment: “global sections”. References: SGA 2 II (Theorem6), “b)”.

The global-sections clause of [Stacks, Tag 01YB]. For a Noetherian scheme X, a quasi-coherent sheaf of ideals I and a quasi-coherent 𝒪_X-module F, the canonical map

colim_n Hom_{𝒪_X}(Iⁿ, F) ⟶ Γ(X \\ V(I), F)

is a bijection. Injectivity is canonicalMapToSections_injective, the first assertion of [Stacks, Tag 01PQ]; surjectivity is exists_hom_idealPow_app_oneSection_eq_of_isQuasicoherent.

This is the second of the two displays of Tag 01YB. The tag's first display, colim_n Hom(Iⁿ G, F) ≅ Hom(G|_U, F|_U) for a coherent G, is not proved here; its G = 𝒪_X case is, so the clause label records the global-sections half only. The first display is what [Stacks, Tag 0BJZ] consumes: there G is the coherent module itself, never 𝒪_X. Its arrow is canonicalMapToHomRestrict and its bijectivity is canonicalMapToHomRestrict_bijective, whose surjectivity half applies this clause to SheafHom(G, F) and then transports the resulting morphism Iⁿ ⟶ SheafHom(G, F) across the surjection Iⁿ ⊗ G ⟶ Iⁿ G, using the vanishing Iⁿ ker(Iⁿ ⊗ G ⟶ Iⁿ G) = 0 and a second Artin-Rees step.

theorem canonicalMapToSections_bijective_of_isQuasicoherent
    [AlgebraicGeometry.IsNoetherian X] (I : X.IdealSheafData) (F : X.Modules)
    [F.IsQuasicoherent] :
    Function.Bijective (canonicalMapToSections I F)

Tag 0FD0, a lemma

Tag 0FD0 in the Stacks Project.

AlgebraicGeometry.exists_coherent_submodule_extension_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/CoherentExtension/LocallyNoetherian.lean, line 350.

Stacks Project, Tag 0FD0. Let F and G be coherent modules on a locally Noetherian scheme X, and let φ : F|_U ⟶ G|_U be a morphism over an open subscheme U. Then there is a coherent submodule F' ⟶ F agreeing with F over U and a morphism φ' : F' ⟶ G whose restriction to U is φ under that agreement.

The submodule is presented as a monomorphism i : F' ⟶ F whose restriction to U is an isomorphism e; the two equations say that e is that restriction and that φ is the restriction of φ' read through e.

theorem exists_coherent_submodule_extension_of_isLocallyNoetherian [IsLocallyNoetherian X]
    (F G : X.Modules) [F.IsCoherent] [G.IsCoherent] (U : X.Opens)
    (φ : F.restrict U.ι ⟶ G.restrict U.ι) :
    ∃ (F' : X.Modules) (_ : F'.IsCoherent) (i : F' ⟶ F) (_ : Mono i)
      (φ' : F' ⟶ G) (e : F'.restrict U.ι ≅ F.restrict U.ι),
      (Scheme.Modules.restrictFunctor U.ι).map i = e.hom ∧
        e.hom ≫ φ = (Scheme.Modules.restrictFunctor U.ι).map φ'

Sources

LeanAlgebraicGeometry.exists_eventually_constant_quasicoherentSubobjects · AlgebraicGeometry.exists_idealPowerMultiple_eq_bot_iff_supp_subset · Stacks.IdealPowerSupport.exists_idealPowerMultiple_eq_bot_iff_supp_subset · AlgebraicGeometry.exists_ideal_pow_smul_inf_eq · AlgebraicGeometry.coherentSubobject_isFiltered · AlgebraicGeometry.isColimit_coherentSubobjectCocone · Stacks.AlgebraicGeometry.IdealPowerColimit.canonicalMapToHomRestrict_bijective · Stacks.AlgebraicGeometry.IdealPowerColimit.canonicalMapToSections_bijective_of_isQuasicoherent

Section30.11 Depth #

Section 30.11 of the Stacks Project, Tag 0340. 5 tags here are carried by 9 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0341, a definition

Tag 0341 in the Stacks Project.

AlgebraicGeometry.SheafHasDepthAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/Depth.lean, line 54. The attribute's comment: “part (1)”.

Stacks Project, Tag 0341. A sheaf of modules has depth k at x when its stalk has depth k over the local ring at x.

abbrev SheafHasDepthAt (X : Scheme.{u})
    (F : SheafOfModules.{u} (structureSheafRing
      X.toRingedSpace)) (x : X)
    (k : ℕ) : Prop

AlgebraicGeometry.SchemeHasDepthAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/Depth.lean, line 64. The attribute's comment: “part (2)”.

Stacks Project, Tag 0341. A scheme has depth k at x when its local ring at x has depth k over itself.

abbrev SchemeHasDepthAt (X : Scheme.{u}) (x : X) (k : ℕ) : Prop

AlgebraicGeometry.SheafHasPropertySk, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/Depth.lean, line 72. The attribute's comment: “part (3)”. References: EGA IV (5.7.2), “more general”.

Stacks Project, Tag 0341. Serre's condition (Sₖ) for a sheaf of modules: at every point its depth is at least the minimum of k and the dimension of the support of its stalk.

abbrev SheafHasPropertySk (X : Scheme.{u})
    (F : SheafOfModules.{u} (structureSheafRing
      X.toRingedSpace))
    (k : ℕ) : Prop

Declarations registered for the tag:

AlgebraicGeometry.HasPropertySk, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/Depth.lean, line 83 (StacksFrontier): “part (4)”.

Tag 0EBC, a lemma

Tag 0EBC in the Stacks Project.

AlgebraicGeometry.one_le_depth_stalk_internalHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/InternalHomDepth.lean, line 157. The attribute's comment: “part (1)”.

[Stacks, Tag 0EBC], part (1). For coherent modules on a locally Noetherian scheme, the stalk of SheafHom(F, G) at x has depth at least one as soon as G_x does.

public theorem one_le_depth_stalk_internalHom [IsLocallyNoetherian X] (F G : X.Modules)
    [_root_.SheafOfModules.IsCoherent F] [_root_.SheafOfModules.IsCoherent G]
    (H : SheafHom X.sheaf F G) (x : X)
    (hx : (1 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
      (IsLocalRing.maximalIdeal (X.presheaf.stalk x)) (G.presheaf.stalk x)) :
    (1 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
      (IsLocalRing.maximalIdeal (X.presheaf.stalk x))
      ((internalHomOf H).presheaf.stalk x)

AlgebraicGeometry.two_le_depth_stalk_internalHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/InternalHomDepth.lean, line 170. The attribute's comment: “part (2)”.

[Stacks, Tag 0EBC], part (2). For coherent modules on a locally Noetherian scheme, the stalk of SheafHom(F, G) at x has depth at least two as soon as G_x does.

public theorem two_le_depth_stalk_internalHom [IsLocallyNoetherian X] (F G : X.Modules)
    [_root_.SheafOfModules.IsCoherent F] [_root_.SheafOfModules.IsCoherent G]
    (H : SheafHom X.sheaf F G) (x : X)
    (hx : (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
      (IsLocalRing.maximalIdeal (X.presheaf.stalk x)) (G.presheaf.stalk x)) :
    (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
      (IsLocalRing.maximalIdeal (X.presheaf.stalk x))
      ((internalHomOf H).presheaf.stalk x)

Tag 0AXQ, a lemma

Tag 0AXQ in the Stacks Project.

AlgebraicGeometry.sheafHasPropertySk_one_internalHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/InternalHomDepth.lean, line 204. The attribute's comment: “hom_into_s1”.

[Stacks, Tag 0AXQ], part (1). On a locally Noetherian scheme the internal hom of coherent modules into a module satisfying Serre's condition (S₁) satisfies (S₁).

public theorem sheafHasPropertySk_one_internalHom [IsLocallyNoetherian X] (F G : X.Modules)
    [_root_.SheafOfModules.IsCoherent F] [_root_.SheafOfModules.IsCoherent G]
    (H : SheafHom X.sheaf F G) (hG : SheafHasPropertySk X G 1) :
    SheafHasPropertySk X (internalHomOf H) 1

AlgebraicGeometry.sheafHasPropertySk_two_internalHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/InternalHomDepth.lean, line 216. The attribute's comment: “hom_into_s2”.

[Stacks, Tag 0AXQ], part (2). On a locally Noetherian scheme the internal hom of coherent modules into a module satisfying Serre's condition (S₂) satisfies (S₂).

public theorem sheafHasPropertySk_two_internalHom [IsLocallyNoetherian X] (F G : X.Modules)
    [_root_.SheafOfModules.IsCoherent F] [_root_.SheafOfModules.IsCoherent G]
    (H : SheafHom X.sheaf F G) (hG : SheafHasPropertySk X G 2) :
    SheafHasPropertySk X (internalHomOf H) 2

Tag 0343, a definition

Tag 0343 in the Stacks Project.

AlgebraicGeometry.SheafIsCohenMacaulay, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/Depth.lean, line 88. References: EGA IV (5.7.1).

Stacks Project, Tag 0343. A sheaf of modules is Cohen–Macaulay when it satisfies Serre's condition (Sₖ) for every k.

abbrev SheafIsCohenMacaulay (X : Scheme.{u})
    (F : SheafOfModules.{u} (structureSheafRing
      X.toRingedSpace)) : Prop

Tag 0B3K, a lemma

Tag 0B3K in the Stacks Project.

AlgebraicGeometry.sheafIsCohenMacaulay_and_supp_eq_univ_iff_isFiniteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/CohenMacaulayRegular.lean, line 220. References: EGA 0 (17.3.5), “(i)”.

Stacks Project, Tag 0B3K. Let X be a regular scheme and F a coherent 𝒪_X-module. Then F is Cohen–Macaulay with support all of X if and only if it is finite locally free of positive rank at every point.

public theorem sheafIsCohenMacaulay_and_supp_eq_univ_iff_isFiniteLocallyFree
    (hX : IsRegular X) (F : X.Modules) [_root_.SheafOfModules.IsCoherent F] :
    (SheafIsCohenMacaulay X F ∧ _root_.SheafOfModules.supp F = Set.univ) ↔
      SheafOfModules.IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf) F ∧
        ∀ x : X, 0 < Scheme.Modules.fiberRank F x

Sources

LeanAlgebraicGeometry.SheafHasDepthAt · AlgebraicGeometry.SchemeHasDepthAt · AlgebraicGeometry.SheafHasPropertySk · AlgebraicGeometry.HasPropertySk · AlgebraicGeometry.one_le_depth_stalk_internalHom · AlgebraicGeometry.two_le_depth_stalk_internalHom · AlgebraicGeometry.sheafHasPropertySk_one_internalHom · AlgebraicGeometry.sheafHasPropertySk_two_internalHom

Section30.12 Devissage of coherent sheaves #

Section 30.12 of the Stacks Project, Tag 01YC. 8 tags here are carried by 11 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01YD, a lemma

Tag 01YD in the Stacks Project.

Stacks.AlgebraicGeometry.HigherDirectImageCoherent.exists_shortExact_coherent_of_supp_eq_union, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CoherentDevissage/SupportSeparation.lean, line 241.

[Stacks, Tag 01YD]. A coherent module whose support is a union of two closed sets is an extension of coherent modules supported on those sets: there is a short exact sequence 0 ⟶ G' ⟶ F ⟶ G ⟶ 0 of coherent modules with Supp G' ⊆ Z' and Supp G ⊆ Z, and F is literally its middle term.

public theorem exists_shortExact_coherent_of_supp_eq_union
    (X : Scheme.{u}) [IsNoetherian X] (F : X.Modules) [_root_.SheafOfModules.IsCoherent F]
    (Z Z' : Set X) (hZ : IsClosed Z) (hZ' : IsClosed Z')
    (hF : SheafOfModules.supp F = Z ∪ Z') :
    ∃ (G' G : X.Modules) (f : G' ⟶ F) (g : F ⟶ G) (w : f ≫ g = 0),
      (ShortComplex.mk f g w).ShortExact ∧
        _root_.SheafOfModules.IsCoherent G' ∧ _root_.SheafOfModules.IsCoherent G ∧
        SheafOfModules.supp G' ⊆ Z' ∧ SheafOfModules.supp G ⊆ Z

Stacks.AlgebraicGeometry.IdealPowerSmul.hasSupportSplitting, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/IdealPowerSmul/Splitting.lean, line 78.

[Stacks, Tag 01YD]. A coherent module on a Noetherian scheme whose support is the union of two closed sets sits in a short exact sequence of coherent modules whose sub is supported in the first and whose quotient is supported in the second.

theorem hasSupportSplitting (X : Scheme.{u}) [IsNoetherian X] :
    DevissageNoetherian.HasSupportSplitting X

Tag 01YE, a lemma

Tag 01YE in the Stacks Project.

Stacks.ClosedImmersion.exists_idealCoproduct_pushforward_mono_isIso_near_genericPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/IrreducibleDevissage/GenericIdealPushforward.lean, line 226.

[Stacks, Tag 01YE]. Let X be a Noetherian scheme, let i : Z ⟶ X be an integral closed subscheme with generic point ξ, and let ℱ be a coherent 𝒪_X-module whose stalk at i ξ is annihilated by the maximal ideal of the local ring there. Then there are an integer r ≥ 0, a coherent sheaf of ideals ℐ ⊆ 𝒪_Z and an injective map of coherent sheaves i_*(ℐ^{⊕ r}) ⟶ ℱ which is an isomorphism on a neighbourhood of i ξ.

The subsheaf of sections of ℱ annihilated by the ideal sheaf of Z has the same stalk at i ξ as ℱ does, because that ideal generates the maximal ideal there, so it agrees with ℱ on a neighbourhood of i ξ; being killed by the ideal it is i_* 𝒢 for a coherent 𝒢 on Z by [Stacks, Tag 087T]; and the case Z = X, applied to 𝒢, supplies the sheaf of ideals and the monomorphism.

theorem exists_idealCoproduct_pushforward_mono_isIso_near_genericPoint
    [AlgebraicGeometry.IsNoetherian X] (i : Z ⟶ X)
    [AlgebraicGeometry.IsClosedImmersion i] [AlgebraicGeometry.IsIntegral Z]
    (ξ : Z) (hξ : IsGenericPoint ξ (Set.univ : Set Z))
    (F : X.Modules) [F.IsCoherent] (hF : StalkKilledByMaximalIdeal F (i ξ)) :
    ∃ (r : ℕ) (I : (SheafOfModules.unit Z.ringCatSheaf).Submodule),
      I.toSheafOfModules.IsCoherent ∧
      ((Scheme.Modules.pushforward i).obj
        (∐ fun _ : Fin r => I.toSheafOfModules)).IsCoherent ∧
      ∃ φ : (Scheme.Modules.pushforward i).obj
          (∐ fun _ : Fin r => I.toSheafOfModules) ⟶ F,
        Mono φ ∧ ∃ U : X.Opens, i ξ ∈ U ∧
          IsIso ((Scheme.Modules.restrictFunctor U.ι).map φ)

Tag 01YF, a lemma

Tag 01YF in the Stacks Project.

Stacks.AlgebraicGeometry.CoherentDevissage.exists_filtration_by_integral_ideal_pushforwards, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CoherentDevissage/IdealFiltration/NoetherianInduction.lean, line 638.

[Stacks, Tag 01YF]. A coherent module on a Noetherian scheme has a finite filtration by coherent submodules, starting at ⊥ and ending at ⊤, whose successive quotients are direct images of nonzero coherent sheaves of ideals on integral closed subschemes.

public theorem exists_filtration_by_integral_ideal_pushforwards
    (X : Scheme.{u}) [IsNoetherian X] (F : X.Modules) [F.IsCoherent] :
    ∃ (n : ℕ) (G : Fin (n + 1) → Subobject F) (hG : Monotone G),
      G 0 = ⊥ ∧ G (Fin.last n) = ⊤ ∧
      (∀ j : Fin (n + 1), (G j : X.Modules).IsCoherent) ∧
      ∀ j : Fin n,
        ∃ (Z : Scheme.{u}) (i : Z ⟶ X) (_ : IsClosedImmersion i) (_ : IsIntegral Z)
          (I : (SheafOfModules.unit Z.ringCatSheaf).Submodule),
          I.toSheafOfModules.IsCoherent ∧ ¬ IsZero I.toSheafOfModules ∧
          Nonempty (cokernel (Subobject.ofLE (G j.castSucc) (G j.succ)
            (hG j.castSucc_le_succ)) ≅
            (Scheme.Modules.pushforward i).obj I.toSheafOfModules)

Tag 01YG, a lemma

Tag 01YG in the Stacks Project.

Stacks.AlgebraicGeometry.CoherentDevissage.property_of_isCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CoherentDevissage/IdealPushforwardCriterion.lean, line 73.

Let X be a Noetherian scheme and let P be a property of coherent 𝒪_X-modules which holds on the zero module, is stable under extensions of coherent modules, and holds on the direct image i_* I of every quasi-coherent ideal I ⊆ 𝒪_Z along the closed immersion of every integral closed subscheme i : Z ⟶ X. Then P holds on every coherent 𝒪_X-module.

Every coherent module is filtered by such direct images ([Stacks, Tag 01YF]), and extension stability propagates P along the filtration.

public theorem property_of_isCoherent (X : Scheme.{u}) [IsNoetherian X]
    (P : X.Modules → Prop) (hzero : P (⊤_ X.Modules))
    (hext : ∀ S : ShortComplex X.Modules, S.ShortExact →
      _root_.SheafOfModules.IsCoherent S.X₁ → _root_.SheafOfModules.IsCoherent S.X₂ →
      _root_.SheafOfModules.IsCoherent S.X₃ → P S.X₁ → P S.X₃ → P S.X₂)
    (hideal : ∀ {Z : Scheme.{u}} (i : Z ⟶ X) [IsClosedImmersion i] [IsIntegral Z]
      (I : (SheafOfModules.unit Z.ringCatSheaf).Submodule),
      I.toSheafOfModules.IsQuasicoherent →
      P ((Scheme.Modules.pushforward i).obj I.toSheafOfModules)) :
    ∀ F : X.Modules, _root_.SheafOfModules.IsCoherent F → P F

Tag 01YH, a lemma

Tag 01YH in the Stacks Project.

Stacks.AlgebraicGeometry.IrreducibleSupportDevissage.property_of_irreducible_support, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CoherentDevissage/IrreducibleSupportCriterion.lean, line 706.

A two-out-of-three property of coherent sheaves holds for every sheaf supported on the given irreducible closed subset if it holds on proper integral closed subschemes and on one generically simple sheaf of full support.

public theorem property_of_irreducible_support
    (X : Scheme.{u}) [IsNoetherian X]
    (Z₀ : Set X) (hZ₀ : IsClosed Z₀) (_hZ₀irr : IsIrreducible Z₀)
    (ξ : X) (hξ : IsGenericPoint ξ Z₀)
    (P : X.Modules → Prop)
    (hexact : ∀ (S : ShortComplex X.Modules), S.ShortExact →
      S.X₁.IsCoherent → S.X₂.IsCoherent → S.X₃.IsCoherent →
      ((P S.X₁ ∧ P S.X₂ → P S.X₃) ∧
        (P S.X₁ ∧ P S.X₃ → P S.X₂) ∧
        (P S.X₂ ∧ P S.X₃ → P S.X₁)))
    (hproper : ∀ (Z : Scheme.{u}) (i : Z ⟶ X) [IsClosedImmersion i]
      [IsIntegral Z], Set.range i.base ⊂ Z₀ →
      ∀ (I : (SheafOfModules.unit Z.ringCatSheaf).Submodule)
        [I.toSheafOfModules.IsQuasicoherent],
        P ((Scheme.Modules.pushforward i).obj I.toSheafOfModules))
    (hgeneric : ∃ G : X.Modules,
      G.IsCoherent ∧ SheafOfModules.supp G = Z₀ ∧
      Stacks.ClosedImmersion.StalkKilledByMaximalIdeal G ξ ∧
      (letI : Module (X.presheaf.stalk ξ) (G.presheaf.stalk ξ) :=
        PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
          (R := X.presheaf) G.val ξ
       Module.length (X.presheaf.stalk ξ) (G.presheaf.stalk ξ) = 1) ∧
      P G) :
    ∀ F : X.Modules, F.IsCoherent → SheafOfModules.supp F ⊆ Z₀ → P F

Tag 01YI, a lemma

Tag 01YI in the Stacks Project.

Stacks.AlgebraicGeometry.CoherentDevissage.property_of_isCoherent_of_generic_stalk_of_nonempty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CoherentDevissage/GenericStalkCriterion.lean, line 166.

[Stacks, Tag 01YI]. Let X be a nonempty Noetherian scheme and let P be a property of coherent 𝒪_X-modules such that

for a short exact sequence of coherent modules, if two out of three have P then so does the third, and

every integral closed subscheme i : Z ⟶ X with generic point ξ carries some coherent module 𝒢 with Supp 𝒢 the range of i, with 𝒢_ξ annihilated by 𝔪_ξ and of length one over 𝒪_{X,ξ}, and with P 𝒢.

Then P holds on every coherent 𝒪_X-module.

Nonemptiness cannot be dropped: on the empty Noetherian scheme hypotheses (1) and (2) hold for P := fun _ => False, while the zero module is coherent.

public theorem property_of_isCoherent_of_generic_stalk_of_nonempty
    (X : Scheme.{u}) [IsNoetherian X] (hX : Nonempty X) (P : X.Modules → Prop)
    (hexact : ∀ S : ShortComplex X.Modules, S.ShortExact →
      _root_.SheafOfModules.IsCoherent S.X₁ → _root_.SheafOfModules.IsCoherent S.X₂ →
      _root_.SheafOfModules.IsCoherent S.X₃ →
      ((P S.X₁ ∧ P S.X₂ → P S.X₃) ∧
        (P S.X₁ ∧ P S.X₃ → P S.X₂) ∧
        (P S.X₂ ∧ P S.X₃ → P S.X₁)))
    (hgeneric : ∀ (Z : Scheme.{u}) (i : Z ⟶ X), IsClosedImmersion i → IsIntegral Z →
      ∀ ξ : X, IsGenericPoint ξ (Set.range i.base) →
      ∃ G : X.Modules, _root_.SheafOfModules.IsCoherent G ∧
        SheafOfModules.supp G = Set.range i.base ∧
        Stacks.ClosedImmersion.StalkKilledByMaximalIdeal G ξ ∧
        (letI : Module (X.presheaf.stalk ξ) (G.presheaf.stalk ξ) :=
          PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
            (R := X.presheaf) G.val ξ
         Module.length (X.presheaf.stalk ξ) (G.presheaf.stalk ξ) = 1) ∧
        P G) :
    ∀ F : X.Modules, _root_.SheafOfModules.IsCoherent F → P F

Stacks.AlgebraicGeometry.GenericRankOneDevissage.property_of_genericRankOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GenericRankOneDevissage/Basic.lean, line 217. The attribute's comment: “corrected: the source statement is false on the empty scheme, where condition (2) is vacuous and the identically false property satisfies both hypotheses, so P on the zero module is added”.

The dévissage criterion of [Stacks, Tag 01YI], with the zero module added to its hypotheses. On a Noetherian scheme X, a property P of coherent modules which holds for the zero module, propagates along a short exact sequence of coherent modules from any two of its terms to the third, and holds for one coherent module supported exactly on each integral closed subscheme with generic stalk killed by the maximal ideal there and of length one over it, holds for every coherent module.

The criterion of [Stacks, Tag 01YG] reduces this to the direct images of quasi-coherent ideals on integral closed subschemes, which is pushforward_ideal_property_of_genericRankOne. The hypothesis on the zero module cannot be dropped: on the empty scheme, which is Noetherian and has no integral closed subscheme, the identically false property satisfies the other two hypotheses.

theorem property_of_genericRankOne (X : Scheme.{u}) [IsNoetherian X]
    (P : X.Modules → Prop) (hzero : P (⊤_ X.Modules))
    (hexact : ∀ S : ShortComplex X.Modules, S.ShortExact →
      S.X₁.IsCoherent → S.X₂.IsCoherent → S.X₃.IsCoherent →
      ((P S.X₁ ∧ P S.X₂ → P S.X₃) ∧
        (P S.X₁ ∧ P S.X₃ → P S.X₂) ∧
        (P S.X₂ ∧ P S.X₃ → P S.X₁)))
    (hgeneric : ∀ (Z : Scheme.{u}) (i : Z ⟶ X) [IsClosedImmersion i] [IsIntegral Z]
      (ξ : X), IsGenericPoint ξ (Set.range i.base) →
      ∃ G : X.Modules, G.IsCoherent ∧
        SheafOfModules.supp G = Set.range i.base ∧
        Stacks.ClosedImmersion.StalkKilledByMaximalIdeal G ξ ∧
        (letI : Module (X.presheaf.stalk ξ) (G.presheaf.stalk ξ) :=
          PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
            (R := X.presheaf) G.val ξ
         Module.length (X.presheaf.stalk ξ) (G.presheaf.stalk ξ) = 1) ∧
        P G) :
    ∀ F : X.Modules, F.IsCoherent → P F

Stacks.AlgebraicGeometry.GenericRankOneDevissage.property_of_genericRankOne_of_exists_isIntegral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GenericRankOneDevissage/Basic.lean, line 253. The attribute's comment: “corrected: the source statement is false on the empty scheme, where condition (2) is vacuous and the identically false property satisfies both hypotheses, so the existence of one integral closed subscheme is added”.

The dévissage criterion of [Stacks, Tag 01YI], with one integral closed subscheme added to its hypotheses. On a Noetherian scheme carrying at least one integral closed subscheme, a property P of coherent modules satisfying conditions (1) and (2) of [Stacks, Tag 01YI] holds for every coherent module.

Condition (2) at that one subscheme produces a coherent module for which P holds, and condition (1) then carries P to the zero module, so the hypothesis of property_of_genericRankOne is met. The added hypothesis is implied by Nonempty X and implies it, and it cannot be dropped: on the empty scheme the identically false property satisfies conditions (1) and (2) and fails for the coherent zero module.

theorem property_of_genericRankOne_of_exists_isIntegral (X : Scheme.{u}) [IsNoetherian X]
    (hne : ∃ (Z : Scheme.{u}) (i : Z ⟶ X), IsClosedImmersion i ∧ IsIntegral Z)
    (P : X.Modules → Prop)
    (hexact : ∀ S : ShortComplex X.Modules, S.ShortExact →
      S.X₁.IsCoherent → S.X₂.IsCoherent → S.X₃.IsCoherent →
      ((P S.X₁ ∧ P S.X₂ → P S.X₃) ∧
        (P S.X₁ ∧ P S.X₃ → P S.X₂) ∧
        (P S.X₂ ∧ P S.X₃ → P S.X₁)))
    (hgeneric : ∀ (Z : Scheme.{u}) (i : Z ⟶ X) [IsClosedImmersion i] [IsIntegral Z]
      (ξ : X), IsGenericPoint ξ (Set.range i.base) →
      ∃ G : X.Modules, G.IsCoherent ∧
        SheafOfModules.supp G = Set.range i.base ∧
        Stacks.ClosedImmersion.StalkKilledByMaximalIdeal G ξ ∧
        (letI : Module (X.presheaf.stalk ξ) (G.presheaf.stalk ξ) :=
          PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
            (R := X.presheaf) G.val ξ
         Module.length (X.presheaf.stalk ξ) (G.presheaf.stalk ξ) = 1) ∧
        P G) :
    ∀ F : X.Modules, F.IsCoherent → P F

Tag 01YL, a lemma

Tag 01YL in the Stacks Project.

Stacks.AlgebraicGeometry.HigherRankIrreducibleDevissage.property_irreducible_higher_rank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CoherentDevissage/HigherRankIrreducibleCriterion.lean, line 1080.

[Stacks, Tag 01YL], in the corrected form. Let X be a Noetherian scheme, Z₀ an irreducible closed subset with generic point ξ, and P a property of coherent modules which holds for the zero module, is stable under extensions of coherent modules, descends from a nonempty finite direct sum, holds for the direct image of every quasi-coherent sheaf of ideals on every integral closed subscheme strictly inside Z₀, and admits one coherent G of support exactly Z₀ whose stalk at ξ is annihilated by the maximal ideal there and which has, inside every ideal multiple J·G with J_ξ the whole local ring, a quasi-coherent subsheaf agreeing with G at ξ for which P holds. Then P holds for every coherent module whose support is contained in Z₀.

The correction is the hypothesis hzero: the source's four conditions do not list P for the zero module and do not imply it, and without it the statement is false. See this file's implementation notes for the counterexample.

public theorem property_irreducible_higher_rank
    (X : Scheme.{u}) [IsNoetherian X]
    (Z₀ : Set X) (hZ₀ : IsClosed Z₀)
    (ξ : X) (hξ : IsGenericPoint ξ Z₀)
    (P : X.Modules → Prop)
    (hzero : P (⊤_ X.Modules))
    (hext : ∀ (S : ShortComplex X.Modules), S.ShortExact →
      S.X₁.IsCoherent → S.X₂.IsCoherent → S.X₃.IsCoherent →
      P S.X₁ → P S.X₃ → P S.X₂)
    (hsum : ∀ (F : X.Modules), F.IsCoherent →
      (∃ n : ℕ, P (∏ᶜ (fun _ : Fin (n + 1) => F))) → P F)
    (hproper : ∀ (I : X.IdealSheafData) [IsIntegral I.subscheme],
      (I.support : Set X) ⊆ Z₀ → (I.support : Set X) ≠ Z₀ →
      ∀ (H : (SheafOfModules.unit I.subscheme.ringCatSheaf).Submodule)
        [H.toSheafOfModules.IsQuasicoherent],
        P ((Scheme.Modules.pushforward I.subschemeι).obj H.toSheafOfModules))
    (hgeneric : ∃ (G : X.Modules), G.IsCoherent ∧
      (∀ x : X, x ∈ Z₀ ↔ Nontrivial (G.presheaf.stalk x)) ∧
      Tag01YEStalkBridge.IsMaximalIdealAnnihilated G ξ ∧
      (∀ (J : X.IdealSheafData), ξ ∉ J.support →
        ∃ (G' : G.Submodule),
          G'.toSheafOfModules.IsQuasicoherent ∧
          (∀ (U : X.affineOpens) (s : Γ(G'.toSheafOfModules, U.1)),
            (Scheme.Modules.Hom.app G'.ι U.1 s : Γ(G, U.1)) ∈
              J.ideal U • (⊤ : Submodule Γ(X, U.1) Γ(G, U.1))) ∧
          Function.Surjective
            (((TopCat.Presheaf.stalkFunctor Ab ξ).map
              (Scheme.Modules.Hom.mapPresheaf G'.ι)).hom) ∧
          P G'.toSheafOfModules)) :
    ∀ (F : X.Modules), F.IsCoherent →
      (∀ x : X, Nontrivial (F.presheaf.stalk x) → x ∈ Z₀) → P F

Tag 01YM, a lemma

Tag 01YM in the Stacks Project.

Stacks.AlgebraicGeometry.NoetherianDevissage.property_higher_rank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CoherentDevissage/NoetherianDevissage.lean, line 82. The attribute's comment: “plus P on the zero sheaf, which conditions (1) and (2) do not give”.

The dévissage of coherent sheaves on a Noetherian scheme. A property closed under extensions, descending from a nonempty finite direct sum, and holding for a suitable coherent module at every integral closed subscheme, holds for every coherent module.

theorem property_higher_rank [IsNoetherian X] (P : X.Modules → Prop)
    (hzero : P (⊤_ X.Modules))
    (hext : ∀ S : ShortComplex X.Modules, S.ShortExact →
      S.X₁.IsCoherent → S.X₂.IsCoherent → S.X₃.IsCoherent → P S.X₁ → P S.X₃ → P S.X₂)
    (hsum : ∀ F : X.Modules, F.IsCoherent →
      (∃ n : ℕ, P (∏ᶜ fun _ : Fin (n + 1) => F)) → P F)
    (hgeneric : ∀ (I : X.IdealSheafData) [IsIntegral I.subscheme],
      ∃ G : X.Modules, G.IsCoherent ∧
        (∀ x : X, x ∈ I.support ↔ Nontrivial (G.presheaf.stalk x)) ∧
        Tag01YEStalkBridge.IsMaximalIdealAnnihilated G
          (I.subschemeι (genericPoint I.subscheme)) ∧
        (∀ J : X.IdealSheafData,
          I.subschemeι (genericPoint I.subscheme) ∉ J.support →
          ∃ G' : G.Submodule,
            G'.toSheafOfModules.IsCoherent ∧
            (∀ (U : X.affineOpens) (s : Γ(G'.toSheafOfModules, U.1)),
              (Scheme.Modules.Hom.app G'.ι U.1 s : Γ(G, U.1)) ∈
                J.ideal U • (⊤ : Submodule Γ(X, U.1) Γ(G, U.1))) ∧
            Function.Surjective
              (((TopCat.Presheaf.stalkFunctor Ab
                (I.subschemeι (genericPoint I.subscheme))).map
                  (Scheme.Modules.Hom.mapPresheaf G'.ι)).hom) ∧
            P G'.toSheafOfModules)) :
    ∀ F : X.Modules, F.IsCoherent → P F

Sources

LeanStacks.AlgebraicGeometry.HigherDirectImageCoherent.exists_shortExact_coherent_of_supp_eq_union · Stacks.AlgebraicGeometry.IdealPowerSmul.hasSupportSplitting · Stacks.ClosedImmersion.exists_idealCoproduct_pushforward_mono_isIso_near_genericPoint · Stacks.AlgebraicGeometry.CoherentDevissage.exists_filtration_by_integral_ideal_pushforwards · Stacks.AlgebraicGeometry.CoherentDevissage.property_of_isCoherent · Stacks.AlgebraicGeometry.IrreducibleSupportDevissage.property_of_irreducible_support · Stacks.AlgebraicGeometry.CoherentDevissage.property_of_isCoherent_of_generic_stalk_of_nonempty · Stacks.AlgebraicGeometry.GenericRankOneDevissage.property_of_genericRankOne

Section30.13 Finite morphisms and affines #

Section 30.13 of the Stacks Project, Tag 01YN. 3 tags here are carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01YO, a lemma

Tag 01YO in the Stacks Project.

Stacks.AlgebraicGeometry.FiniteSurjectiveCoherentSupport.exists_isCoherent_supp_pushforward_eq_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FiniteSurjectiveCoherentSupport/Basic.lean, line 341.

[Stacks, Tag 01YO]. Let f : Y ⟶ X be finite and surjective with X locally Noetherian and let i : Z ⟶ X be an integral closed subscheme with generic point ξ. Then there is a coherent module ℱ on Y whose direct image f_* ℱ has support exactly Z and whose stalk at ξ is annihilated by the maximal ideal of 𝒪_{X,ξ}.

theorem exists_isCoherent_supp_pushforward_eq_range
    {X Y Z : Scheme.{u}} (f : Y ⟶ X) [IsFinite f] [Surjective f]
    [IsLocallyNoetherian X] (i : Z ⟶ X) [IsClosedImmersion i] [IsIntegral Z] :
    ∃ F : Y.Modules, F.IsCoherent ∧
      SheafOfModules.supp ((Scheme.Modules.pushforward f).obj F) = Set.range i ∧
      (let G := (Scheme.Modules.pushforward f).obj F
       let x := i (genericPoint Z)
       letI : Module (X.presheaf.stalk x)
           (TopCat.Presheaf.stalk (C := Ab.{u}) G.val.presheaf x) :=
         PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
           (R := X.presheaf) G.val x
       ∀ a : X.presheaf.stalk x,
         a ∈ IsLocalRing.maximalIdeal (X.presheaf.stalk x) →
         ∀ s : TopCat.Presheaf.stalk (C := Ab.{u}) G.val.presheaf x, a • s = 0)

Tag 01YP, a lemma

Tag 01YP in the Stacks Project.

Stacks.AlgebraicGeometry.AffineIdealPushforward.ideal_smul_pushforward_sections_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/IdealPushforwardAffine.lean, line 145.

Stacks Project, Tag 01YP. If f : Y ⟶ X is affine, F is a quasi-coherent 𝒪_Y-module, and I is a quasi-coherent ideal sheaf on X, then I · f₊ F = f₊((f⁻¹ I) · F).

The equality is stated on every affine open, using the affine-open presentation of quasi-coherent ideal sheaves.

theorem ideal_smul_pushforward_sections_eq (f : Y ⟶ X) [IsAffineHom f]
    (I : X.IdealSheafData) (F : Y.Modules) [F.IsQuasicoherent]
    (U : X.affineOpens) :
    pushforwardIdealMultipleSections f I F U =
      pullbackIdealMultiplePushforwardSections f I F U

Tag 01YQ, a lemma

Tag 01YQ in the Stacks Project.

Stacks.AlgebraicGeometry.Tag01YQClauseThree.isAffine_of_isFinite_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ClauseThree/GenericStalkInput.lean, line 61.

A Noetherian scheme admitting a finite surjective morphism from an affine scheme is affine.

theorem isAffine_of_isFinite_surjective {X Y : Scheme.{u}} (f : Y ⟶ X)
    [IsFinite f] [Surjective f] [IsAffine Y] [IsNoetherian X] :
    IsAffine X

Sources

LeanStacks.AlgebraicGeometry.FiniteSurjectiveCoherentSupport.exists_isCoherent_supp_pushforward_eq_range · Stacks.AlgebraicGeometry.AffineIdealPushforward.ideal_smul_pushforward_sections_eq · Stacks.AlgebraicGeometry.Tag01YQClauseThree.isAffine_of_isFinite_surjective

Section30.14 Coherent sheaves on Proj, I #

Section 30.14 of the Stacks Project, Tag 01YR. 4 tags here are carried by 13 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01YS, a lemma

Tag 01YS in the Stacks Project.

Stacks.ProjectiveCohomology.isZero_Hgroup_of_lt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveCohomology/Basic.lean, line 256. The attribute's comment: “clause (2), vanishing above the dimension”. References: EGA III (2.2.2), “(ii), P^n case”.

[Stacks, Tag 01YS], clause (2). The cohomology of a quasi-coherent module on projective n-space over a ring vanishes in every degree above n.

Projective space is covered by its n + 1 standard charts, all affine, and it is separated, hence has affine diagonal; [Stacks, Tag 01XI] then bounds the cohomological degree by n + 1. As the source observes, no Noetherian hypothesis is needed, and the conclusion holds for every quasi-coherent module, not only coherent ones. The source's remaining range i < 0 is vacuous in this spelling, where cohomology is indexed by ℕ.

theorem isZero_Hgroup_of_lt (F : (projectiveSpaceOverRing n R).Modules) [F.IsQuasicoherent]
    (q : ℕ) (hq : n < q) :
    IsZero (Hgroup (projectiveSpaceOverRing n R).ringCatSheaf ⊤ q F)

Stacks.ProjectiveSpace.exists_epi_biproduct_tensorPowModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/CoherentQuotientOfTwists.lean, line 88. The attribute's comment: “assertion (1)”.

Assertion (1) of [Stacks, Tag 01YS]. A quasi-coherent module of finite type on projective n-space over an affine base is a quotient of a finite direct sum of twists 𝒪(d₁), …, 𝒪(d_r) of the structure sheaf, and the degrees may be taken below any prescribed integer.

The source assumes the base ring Noetherian and the module coherent; neither is needed, and Stacks.ProjectiveSpace.exists_epi_biproduct_of_isCoherent is the source's reading.

The proof is the source's: 𝒪(1) is ample on ℙⁿ_S (Stacks.ProjectiveSpace.isAmple_projectiveSpaceTwistingSheaf), and clause (8) of [Stacks, Tag 01Q3] (Stacks.AmpleLocalGeneration.isQuotientOfNegativeTwists_of_isAmple) presents a finite-type quasi-coherent module as a quotient of a finite direct sum of negative tensor powers of an ample invertible module.

theorem exists_epi_biproduct_tensorPowModule (n : ℕ) (S : Scheme.{u}) [IsAffine S] (k : ℤ)
    (F : (projectiveSpaceOver n S).Modules) (hFqc : F.IsQuasicoherent)
    (hFft : SheafOfModules.IsFiniteType.{u, u, u} F) :
    ∃ (r : ℕ) (d : Fin r → ℤ)
      (b : Bicone fun j : Fin r => tensorPowModule (projectiveSpaceOver n S)
        (projectiveSpaceTwistingSheaf n S) (d j))
      (_ : b.IsBilimit) (p : b.pt ⟶ F), Epi p ∧ ∀ j, d j ≤ k

Stacks.ProjectiveSpace.SerreVanishing.moduleFinite_cohomology_of_isCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/Cohomology/CoherentSerreVanishing.lean, line 217. The attribute's comment: “(3) finiteness of the cohomology modules”. References: EGA III (2.2.2), “clause (i), special case”.

[Stacks, Tag 01YS] clause (3). Let R be a Noetherian ring, n ≥ 0 and ℱ a coherent sheaf on ℙⁿ_R = Proj R[T₀, …, Tₙ]. For every i the cohomology H^i(ℙⁿ_R, ℱ) is a finite R-module.

The proof is the source's descending induction on i: it holds above degree n because the cohomology vanishes there (clause (2)), the twists 𝒪(d) have finite cohomology ([Stacks, Tag 01XT]), and ℱ is a quotient of a finite direct sum of twists (clause (1) of the same tag), so the long exact sequence of the kernel sequence places H^i(ℙⁿ_R, ℱ) between two finite modules over the Noetherian ring R.

theorem moduleFinite_cohomology_of_isCoherent [IsNoetherianRing R]
    (F : (AlgebraicGeometry.Proj (polyGrading R n)).Modules)
    (hF : _root_.SheafOfModules.IsCoherent F) (q : ℕ) :
    Module.Finite R
      ((ModuleCat.restrictScalars ((Scheme.ΓSpecIso (CommRingCat.of R)).inv ≫
          (Stacks.AlgebraicGeometry.ProjPolyChart.projToSpecCoeff R n).appTop).hom).obj
        (((Stacks.Cohomology.AffineBase.moduleGlobalSections
          (AlgebraicGeometry.Proj (polyGrading R n))).rightDerived q).obj F))

Stacks.ProjectiveSpace.SerreVanishing.exists_isZero_Hgroup_twist_of_isCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/Cohomology/CoherentSerreVanishing.lean, line 243. The attribute's comment: “(4) eventual vanishing of the higher cohomology of the twists”.

[Stacks, Tag 01YS] clause (4). Let R be a Noetherian ring, n ≥ 0 and ℱ a coherent sheaf on ℙⁿ_R = Proj R[T₀, …, Tₙ]. For every i > 0 the cohomology H^i(ℙⁿ_R, ℱ(d)) vanishes for all d large enough.

The proof is the source's: ℱ is a quotient of a finite direct sum of twists (hasTwistQuotients_polyGrading, clause (1) of the same tag), the twists are eventually acyclic (hasEventuallyAcyclicTwists_polyGrading, from the computation of H^i(ℙⁿ_R, 𝒪(d)) of [Stacks, Tag 01XT]), and the dévissage descends on the cohomological degree from the degree above which everything vanishes.

theorem exists_isZero_Hgroup_twist_of_isCoherent [IsNoetherianRing R] (i : ℕ) (hi : 0 < i)
    (F : (AlgebraicGeometry.Proj (polyGrading R n)).Modules)
    (hF : _root_.SheafOfModules.IsCoherent F) :
    ∃ d₀ : ℤ, ∀ d : ℤ, d₀ ≤ d →
      IsZero (Hgroup (projRingSheaf (polyGrading R n)) ⊤ i
        (twistSheafOfModules (polyGrading R n) F d))

Stacks.ProjectiveSpace.Cohomology.isZero_cohomology_of_lt_zero_or_dim_lt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/Cohomology/CohomologicalDimension.lean, line 64. The attribute's comment: “assertion (2)”. References: EGA III (2.2.2), “(ii), P^n case”.

The cohomological dimension of projective space: the cohomology of a quasi-coherent module on projective n-space over an affine base vanishes in every degree outside 0, …, n.

theorem isZero_cohomology_of_lt_zero_or_dim_lt (n : ℕ) (S : Scheme.{u}) [IsAffine S]
    (F : (projectiveSpaceOver n S).Modules) [F.IsQuasicoherent] (i : ℤ)
    (hi : i < 0 ∨ (n : ℤ) < i) :
    IsZero (((sectionsFunctor (projectiveSpaceOver n S) ⊤).rightDerivedPlus i).obj F)

Stacks.ProjectiveSpace.Cohomology.moduleFinite_truncation_of_isCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/Cohomology/TwistSectionsDegreeOne.lean, line 291. The attribute's comment: “(5) finiteness of the graded module of twisted global sections”. References: SGA 2 XII (5.3), “clause (a), case i = 0”.

[Stacks, Tag 01YS] clause (5). Let R be a Noetherian ring, n ≥ 0 and ℱ a coherent sheaf on ℙⁿ_R = Proj R[T₀, …, Tₙ]. For every k ∈ ℤ the graded R[T₀, …, Tₙ]-module ⨁_{d ≥ k} H⁰(ℙⁿ_R, ℱ(d)) is a finite R[T₀, …, Tₙ]-module.

The proof is the source's sandwich, now with both halves available: each homogeneous piece Γ(ℙⁿ_R, ℱ(d)) is a finite R-module by clause (3) at i = 0, and above some degree every piece lies in the span of the piece one degree below (exists_forall_subset_span_twistedGlobalSectionsGrading), so finitely many pieces generate.

theorem moduleFinite_truncation_of_isCoherent [IsNoetherianRing R]
    (F : SheafOfModules.{u} (projRingSheaf R n))
    (hF : _root_.SheafOfModules.IsCoherent F)
    (D : TwistedGlobalSectionsModule (polyGrading R n) F) (k : ℤ) :
    letI := D.moduleInst
    Module.Finite (MvPolynomial (Fin (n + 1)) R)
      (TwistedGlobalSectionsModule.truncation (polyGrading R n) F D k)

Tag 0AG6, a lemma

Tag 0AG6 in the Stacks Project.

Stacks.ProjCoherentDegreeOne.proj_isNoetherian_and_forall_isCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjCoherentDegreeOne/Main.lean, line 110. References: EGA III (2.2.2).

[Stacks, Tag 0AG6]. Let A be a graded ring such that A₀ is Noetherian and A is generated by finitely many elements of A₁ over A₀. Set X = Proj A. Then X is a Noetherian scheme, and for every coherent 𝒪_X-module ℱ:

there exist an r ≥ 0, integers d₁, …, d_r and a surjection ⨁_{j = 1, …, r} 𝒪_X(d_j) ⟶ ℱ;

for every p the cohomology group H^p(X, ℱ) is a finite A₀-module;

if p > 0 then H^p(X, ℱ(d)) = 0 for all d large enough;

for every k ∈ ℤ the graded A-module ⨁_{d ≥ k} H⁰(X, ℱ(d)) is a finite A-module.

theorem proj_isNoetherian_and_forall_isCoherent :
    AlgebraicGeometry.IsNoetherian (AlgebraicGeometry.Proj 𝒜) ∧
      ∀ F : SheafOfModules.{u} (projRingSheaf 𝒜), _root_.SheafOfModules.IsCoherent F →
        (∃ (r : ℕ) (d : Fin r → ℤ),
            ∃ φ : (∐ fun j : Fin r => twistingSheaf 𝒜 (d j)) ⟶ F, Epi φ) ∧
          (∀ p : ℕ, Module.Finite (𝒜 0)
            ((ModuleCat.restrictScalars ((Scheme.ΓSpecIso (.of (𝒜 0))).inv ≫
                (AlgebraicGeometry.Proj.toSpecZero 𝒜).appTop).hom).obj
              (((moduleGlobalSections (AlgebraicGeometry.Proj 𝒜)).rightDerived p).obj F))) ∧
          (∀ p : ℕ, 0 < p → ∃ d₀ : ℤ, ∀ d : ℤ, d₀ ≤ d →
            IsZero (Hgroup (projRingSheaf 𝒜) ⊤ p (twistSheafOfModules 𝒜 F d))) ∧
          (∀ k : ℤ,
            letI := (twistedGlobalSectionsModule 𝒜 F).moduleInst
            Module.Finite A (TwistedGlobalSectionsModule.truncation 𝒜 F
              (twistedGlobalSectionsModule 𝒜 F) k))

Declarations registered for the tag:

Stacks.AlgebraicGeometry.Proj.isNoetherian_proj, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/ProjNoetherian.lean, line 29 (StacksFrontier): “proj_noetherian”.

Tag 0AG7, a lemma

Tag 0AG7 in the Stacks Project.

Stacks.AlgebraicGeometry.ProjLargeDegreeSections.exists_bijective_degreeNToGlobalSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjLargeDegreeSections/Basic.lean, line 114. The attribute's comment: “bijectivity in all large degrees, from homogeneous generators of the kernel and of the cokernel annihilated, respectively carried into the image, by a power of the irrelevant ideal”.

The comparison maps are bijective in all large degrees, with the finiteness input of the source replaced by homogeneous generating data for the kernel and the cokernel of the comparison.

In every degree n the canonical map 𝒨 n ⟶ Γ(Proj 𝒮, M(n)~) of Equation 01MR is degreeNToGlobalSections. Assume S is generated in degree one over 𝒮 0 and:

the kernel is generated degreewise by x : Fin ck → M placed in degrees dx, and a power of the irrelevant ideal annihilates every x j;

the cokernel is generated degreewise by sections y k of M(dy k)~, and a power of the irrelevant ideal carries every y k into the image of the comparison.

Then the comparison is bijective in every sufficiently large degree. The statement does not assume that 𝒨 is a decomposition of M.

theorem exists_bijective_degreeNToGlobalSections
    (hgen : Algebra.adjoin (𝒮 0) (𝒮 1 : Set S) = ⊤)
    {ck : ℕ} (x : Fin ck → M) (dx : Fin ck → ℤ) (Nx : Fin ck → ℕ)
    (hxtors : ∀ j, ∀ a ∈ (HomogeneousIdeal.irrelevant 𝒮).toIdeal ^ Nx j, a • x j = 0)
    (hxgen : ∀ n : ℤ, (∀ j, dx j ≤ n) → ∀ m : 𝒨 n,
      degreeNToGlobalSections 𝒮 𝒨 n m = 0 →
        ∃ a : (j : Fin ck) → 𝒮 (n - dx j).toNat, (m : M) = ∑ j, (a j : S) • x j)
    {cq : ℕ} (dy : Fin cq → ℤ) (Ny : Fin cq → ℕ)
    (y : (k : Fin cq) → shiftedSectionsComponent 𝒮 𝒨 (dy k))
    (hytors : ∀ (k : Fin cq) (i : ℕ) (a : 𝒮 i),
      (a : S) ∈ (HomogeneousIdeal.irrelevant 𝒮).toIdeal ^ Ny k →
        ∃ m : 𝒨 ((i : ℤ) + dy k),
          homogeneousScalarGlobalSections 𝒮 𝒨 i (dy k) a (y k)
            = degreeNToGlobalSections 𝒮 𝒨 ((i : ℤ) + dy k) m)
    (hygen : ∀ (n : ℤ) (hn : ∀ k, dy k ≤ n) (s : shiftedSectionsComponent 𝒮 𝒨 n),
      ∃ (m : 𝒨 n) (a : (k : Fin cq) → 𝒮 (n - dy k).toNat),
        s = degreeNToGlobalSections 𝒮 𝒨 n m +
          ∑ k, ofDegreeEq 𝒮 𝒨 (show (((n - dy k).toNat : ℤ) + dy k) = n by
              have := hn k; omega)
            (homogeneousScalarGlobalSections 𝒮 𝒨 ((n - dy k).toNat) (dy k) (a k) (y k))) :
    ∃ n₀ : ℤ, ∀ n : ℤ, n₀ ≤ n → Function.Bijective (degreeNToGlobalSections 𝒮 𝒨 n)

Stacks.AlgebraicGeometry.ProjLargeDegreeSections.exists_bijective_degreeNToGlobalSections_of_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjLargeDegreeSections/Noetherian.lean, line 322. The attribute's comment: “the maps M_n to Gamma(Proj A, M(n)~) of Equation 01MR are isomorphisms in all sufficiently large degrees, for A_0 Noetherian, A generated over A_0 by finitely many elements of A_1, and M a finite graded A-module”.

Let S = ⨁_{d ≥ 0} 𝒮 d be a graded ring whose degree-zero part is Noetherian and which is generated over that part by finitely many elements fam 0, … of 𝒮 1, let M = ⨁_{n ∈ ℤ} 𝒨 n be a finite graded S-module and X = Proj 𝒮. The canonical maps

𝒨 n ⟶ Γ(X, M(n)~)

of Equation 01MR are isomorphisms for all sufficiently large n.

theorem exists_bijective_degreeNToGlobalSections_of_finite [IsNoetherianRing ↥(𝒮 0)]
    [Module.Finite S M] {r : ℕ} (fam : Fin r → S) (hfam : ∀ i, fam i ∈ 𝒮 1)
    (hgen : Algebra.adjoin ↥(𝒮 0) (Set.range fam) = ⊤) :
    ∃ n₀ : ℤ, ∀ n : ℤ, n₀ ≤ n → Function.Bijective (degreeNToGlobalSections 𝒮 𝒨 n)

Tag 0BXD, a proposition

Tag 0BXD in the Stacks Project.

Stacks.AlgebraicGeometry.ProjSerreCorrespondence.equivalence_coherentQuotientFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjSerreCorrespondence/Equivalence.lean, line 458. The attribute's comment: “the equivalence Mod^fg_A / Mod^fg_{A,torsion} ⟶ Coh(O_X) induced by M ↦ M~, with quasi-inverse F ↦ ⨁_{n ≥ 0} Γ(X, F(n)), at the source's hypotheses: A_0 Noetherian and A generated by finitely many elements of A_1 over A_0. The torsion subcategory is the irrelevant finitely generated graded modules in generation degree one, which for a Noetherian A generated in degree one is the source's Mod^fg_{A,torsion}. The Noetherianity of A, its finite type over A_0 and the quasi-compactness of Proj A are derived from those hypotheses rather than assumed, which is why the statement opens with haveI. The equality clauses pin the functor to M ↦ M~ and the inverse to F ↦ ⨁_{n ≥ 0} Γ(X, F(n)) on the nose, and the last clause says the functor is induced by M ↦ M~”. References: EGA III (2.3.3), “(F), special case”.

Let A be a graded ring such that A₀ is Noetherian and A is generated by finitely many elements of A₁ over A₀, and set X = Proj A. Then M ↦ M̃ induces an equivalence

Mod^fg_A / Mod^fg_{A, torsion} ⟶ Coh(𝒪_X)

whose quasi-inverse is ℱ ↦ ⨁_{n ≥ 0} Γ(X, ℱ(n)).

The third clause is what says the equivalence is induced by M ↦ M̃: composed with the quotient functor and read in all sheaves of 𝒪_X-modules, its functor is the associated-sheaf functor on Mod^fg_A.

theorem equivalence_coherentQuotientFunctor :
    haveI := isNoetherianRing_of_adjoin_range 𝒜 x hx hgen
    haveI := finiteType_of_adjoin_range 𝒜 x hx hgen
    haveI : CompactSpace (AlgebraicGeometry.Proj 𝒜) :=
      QuasiCompact.compactSpace_of_compactSpace (AlgebraicGeometry.Proj.toSpecZero 𝒜)
    ∃ e : IrrelevantQuotient.{u, u, u} 𝒜 (d := 1) Nat.one_pos ≌
            Stacks.SheafOfModules.CoherentModules (projRingSheaf 𝒜),
      e.functor = coherentQuotientFunctor.{u, u} 𝒜 ∧
      e.inverse = nonnegTwistedSectionsQuotientFunctor 𝒜 x hx hgen ∧
      Nonempty (toIrrelevantQuotient.{u, u, u} 𝒜 Nat.one_pos ⋙ e.functor ⋙
        (Stacks.SheafOfModules.coherentModules (projRingSheaf 𝒜)).ι ≅
          finiteAssociatedSheafFunctor.{u, u} 𝒜)

Stacks.AlgebraicGeometry.ProjSerreCorrespondence.isZero_associatedModuleSheaf_of_isIPowerTorsion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjSerreCorrespondence/TorsionVanishing.lean, line 84. The attribute's comment: “the functor M ↦ M~ kills the torsion modules, the step that lets it be defined on the quotient category; stated for 𝒜₊-power torsion modules, with no finiteness, Noetherian or degree-one generation hypothesis”. References: EGA II (2.5.6), “sufficiency clause”.

The associated sheaf M̃ of an 𝒜₊-power torsion graded module M is a zero object.

theorem isZero_associatedModuleSheaf_of_isIPowerTorsion
    (htor : IsIPowerTorsion S M (HomogeneousIdeal.irrelevant 𝒜).toIdeal) :
    Limits.IsZero (associatedModuleSheaf 𝒜 𝒨)

Stacks.AlgebraicGeometry.ProjSerreCorrespondence.isZero_associatedModuleSheaf_of_eventually_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjSerreCorrespondence/TorsionVanishing.lean, line 140. The attribute's comment: “the functor M ↦ M~ kills the torsion subcategory, with torsion in the form the source defines the subcategory Mod^fg_{A,torsion}: the homogeneous components vanish in all large degrees; no finiteness hypothesis is used”. References: EGA II (2.5.6), “sufficiency clause”; EGA II (2.7.2), “If M satisfies (TN)”; EGA II (2.7.3), “(ii)”; EGA II (3.4.2), “special case”.

A graded module whose homogeneous components vanish in all sufficiently large degrees has zero associated sheaf.

theorem isZero_associatedModuleSheaf_of_eventually_eq_zero [DirectSum.Decomposition 𝒨] {N : ℤ}
    (hN : ∀ n : ℤ, N ≤ n → ∀ m : M, m ∈ 𝒨 n → m = 0) :
    Limits.IsZero (associatedModuleSheaf 𝒜 𝒨)

Stacks.AlgebraicGeometry.ProjSerreCorrespondence.isZero_associatedModuleSheafFunctor_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjSerreCorrespondence/TorsionVanishing.lean, line 151. The attribute's comment: “the bundled functor M ↦ M~ sends torsion graded modules to zero objects, the step that lets it be defined on the quotient category”.

The associated-sheaf functor M ↦ M̃ sends an 𝒜₊-power torsion graded module to a zero object.

theorem isZero_associatedModuleSheafFunctor_obj (X : GradedModuleCat.{u, v, w} 𝒜)
    (htor : IsIPowerTorsion S X.carrier (HomogeneousIdeal.irrelevant 𝒜).toIdeal) :
    Limits.IsZero ((associatedModuleSheafFunctor 𝒜).obj X)

Sources

LeanStacks.ProjectiveCohomology.isZero_Hgroup_of_lt · Stacks.ProjectiveSpace.exists_epi_biproduct_tensorPowModule · Stacks.ProjectiveSpace.SerreVanishing.moduleFinite_cohomology_of_isCoherent · Stacks.ProjectiveSpace.SerreVanishing.exists_isZero_Hgroup_twist_of_isCoherent · Stacks.ProjectiveSpace.Cohomology.isZero_cohomology_of_lt_zero_or_dim_lt · Stacks.ProjectiveSpace.Cohomology.moduleFinite_truncation_of_isCoherent · Stacks.ProjCoherentDegreeOne.proj_isNoetherian_and_forall_isCoherent · Stacks.AlgebraicGeometry.Proj.isNoetherian_proj

Section30.15 Coherent sheaves on Proj, II #

Section 30.15 of the Stacks Project, Tag 0BXE. 3 tags here are carried by 11 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0B5Q, a lemma

Tag 0B5Q in the Stacks Project.

Stacks.AlgebraicGeometry.ProjCoherentII.moduleFinite_truncation_of_isCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjCoherentII/TwistedFiniteness.lean, line 350. The attribute's comment: “clause (4)”. References: SGA 2 XII (5.3), “clause (a), special case”.

Clause (4) of [Stacks, Tag 0B5Q], equivalently part (2) of [Stacks, Tag 0B5R]. For S a Noetherian graded ring, X = Proj S, ℱ a coherent 𝒪_X-module and k ∈ ℤ, the graded S-module ⨁_{n ≥ k} Γ(X, ℱ(n)) is a finite S-module.

No generation hypothesis on S is assumed. The proof is the source's Veronese reduction: a degree d is chosen by Stacks.AlgebraicGeometry.ProjCoherentII.exists_reductionDegree, the degrees are split into the d residue classes, each class is compared with the twisted global sections of a coherent sheaf on X' = Proj S⁽ᵈ⁾ where [Stacks, Tag 0AG6] (4) applies, and the d resulting finite families are assembled over S by Stacks.AlgebraicGeometry.ProjTwistedSections.moduleFinite_gradedActionTruncation_of_residues.

public theorem moduleFinite_truncation_of_isCoherent [IsNoetherianRing S]
    (F : (AlgebraicGeometry.Proj 𝒮).Modules) (hF : _root_.SheafOfModules.IsCoherent F) (k : ℤ) :
    letI := (twistedGlobalSectionsModule 𝒮 F).moduleInst
    Module.Finite S ((twistedGlobalSectionsModule 𝒮 F).truncation 𝒮 F k)

Stacks.AlgebraicGeometry.Proj.isNoetherian_proj, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjNoetherian/Basic.lean, line 135. The attribute's comment: “proj_noetherian”. References: EGA II (2.7.1), “(i)”.

Stacks Project, Tag 0B5Q. The projective spectrum of a Noetherian graded ring is a Noetherian scheme.

public instance isNoetherian_proj
    {A : Type u} {σ : Type v} [CommRing A] [IsNoetherianRing A]
    [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] :
    IsNoetherian (Proj 𝒜)

Stacks.AlgebraicGeometry.ProjNoetherian.proj_isNoetherian_and_coherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjNoetherian/CoherentSheaves.lean, line 51.

Stacks Project, Tag 0B5Q. Let A be a Noetherian graded ring and X = Proj A. Then X is a Noetherian scheme, and every coherent 𝒪_X-module ℱ satisfies the four assertions of the lemma: ℱ is a quotient of a finite direct sum of twisting sheaves, each Hᵖ(X, ℱ) is a finite A₀-module, the higher cohomology of the high twists vanishes, and each graded tail ⨁_{n ≥ k} H⁰(X, ℱ(n)) is a finite A-module.

theorem proj_isNoetherian_and_coherent :
    AlgebraicGeometry.IsNoetherian (AlgebraicGeometry.Proj 𝒜) ∧
      ∀ F : SheafOfModules.{u} (projRingSheaf 𝒜), _root_.SheafOfModules.IsCoherent F →
        (∃ (r : ℕ) (dj : Fin r → ℤ)
            (b : Bicone fun j : Fin r => twistingSheaf 𝒜 (dj j)) (_ : b.IsBilimit)
            (φ : b.pt ⟶ F), Epi φ) ∧
          (∀ p : ℕ, Module.Finite (𝒜 0)
            ((ModuleCat.restrictScalars
              (Stacks.AlgebraicGeometry.GradedProperCohomology.specAlgebraRingHom (𝒜 0)
                (AlgebraicGeometry.Proj.toSpecZero 𝒜))).obj
              (Stacks.AlgebraicGeometry.GradedProperCohomology.cohomologyOf
                (AlgebraicGeometry.Proj 𝒜) p F))) ∧
          (∀ p : ℕ, 0 < p → ∃ e₀ : ℤ, ∀ e : ℤ, e₀ ≤ e →
            IsZero (Hgroup (projRingSheaf 𝒜) ⊤ p (twistSheafOfModules 𝒜 F e))) ∧
          (∀ k : ℤ,
            letI := (ProjTwistedSections.twistedGlobalSectionsModule 𝒜 F).moduleInst
            Module.Finite A
              (TwistedGlobalSectionsModule.truncation 𝒜 F
                (ProjTwistedSections.twistedGlobalSectionsModule 𝒜 F) k))

Tag 0B5R, a lemma

Tag 0B5R in the Stacks Project.

Stacks.AlgebraicGeometry.ProjCoherentII.truncatedTwistedToShifted, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjCoherentII/Basic.lean, line 227. The attribute's comment: “part (3), the canonical map N → N'”.

Tag 0B5R (3): the canonical map N → N'. The comparison assembled from the global sections of Tag 01MQ's maps carries the degrees ≥ k part of ⨁_n H⁰(X, M̃(n)) into the degrees ≥ k part of ⨁_n H⁰(X, M(n)~), because it is degreewise.

def truncatedTwistedToShifted (k : ℤ) :
    twistedSectionsTruncation 𝒮 𝒨 k →+ shiftedSectionsTruncation 𝒮 𝒨 k

Stacks.AlgebraicGeometry.ProjCoherentII.moduleToTruncatedShiftedSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjCoherentII/Basic.lean, line 284. The attribute's comment: “part (4), the canonical map M → N'”.

Tag 0B5R (4): for k small enough there is a canonical map M → N'. The map is Tag 01MR's M → ⨁_{n ∈ ℤ} H⁰(X, M(n)~), and "k small enough" is the hypothesis hlow : ∀ n < k, ∀ x ∈ 𝒨 n, x = 0 that M vanishes below degree k, which is what generators of M in degrees ≥ k give.

def moduleToTruncatedShiftedSections (k : ℤ)
    (hlow : ∀ n : ℤ, n < k → ∀ x ∈ 𝒨 n, x = (0 : M)) :
    M →+ shiftedSectionsTruncation 𝒮 𝒨 k

Stacks.AlgebraicGeometry.ProjCoherentII.exists_pos_forall_bijective_twistedToShiftedComponent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjCoherentII/Basic.lean, line 342. The attribute's comment: “part (6), N_n ≅ N'_n for d | n”.

Tag 0B5R (6). For a Noetherian graded ring A and a graded A-module M there is a positive d such that N_n = H⁰(X, M̃(n)) → H⁰(X, M(n)~) = N'_n is bijective for every n divisible by d. The d is the common degree of a finite standard-open cover of Proj(A), which is the property the source's d = lcm(deg f_i) is used for.

theorem exists_pos_forall_bijective_twistedToShiftedComponent [IsNoetherianRing S] :
    ∃ d : ℕ, 0 < d ∧ ∀ n : ℤ, (d : ℤ) ∣ n →
      Function.Bijective (twistedToShiftedComponent 𝒮 𝒨 n)

Stacks.AlgebraicGeometry.ProjCoherentII.truncatedSections_finite_and_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjCoherentII/FiniteGradedModuleSections.lean, line 163. The attribute's comment: “all six parts: (1) N' is a finite A-module; (2) N is a finite A-module; (3) the canonical map N → N'; (4) the canonical map M → N' for k small enough, i.e. for every k at most some k₀; (5) M_n → N'_n is an isomorphism in all sufficiently large degrees; (6) N_n → N'_n is an isomorphism for d | n, with d the lcm of the degrees of homogeneous generators of A over A_0; (1), (2), (3), (5) and (6) for every k ∈ ℤ”.

Let A be a Noetherian graded ring, f_1, …, f_r homogeneous generators of A over A_0 of positive degrees deg_1, …, deg_r, and d = lcm(deg_i). Let M be a finite graded A-module, X = Proj(A), M̃ the associated quasi-coherent 𝒪_X-module and k ∈ ℤ arbitrary, and set

N' = ⨁_{n ≥ k} H⁰(X, M(n)~) and N = ⨁_{n ≥ k} H⁰(X, M̃(n)).

Then, in order:

N' is a finite A-module;

N is a finite A-module;

the comparison map ⨁_n H⁰(X, M̃(n)) → ⨁_n H⁰(X, M(n)~) carries N into N', giving the canonical map N → N';

for k small enough the canonical map M → ⨁_n H⁰(X, M(n)~) carries M into N': there is k₀ such that for every k' ≤ k₀ it lands in ⨁_{n ≥ k'} H⁰(X, M(n)~);

M_n → N'_n is an isomorphism for all sufficiently large n;

N_n → N'_n is an isomorphism whenever d divides n.

public theorem truncatedSections_finite_and_comparison [IsNoetherianRing S] [Module.Finite S M]
    {r : ℕ} (f : Fin r → S) (deg : Fin r → ℕ) (hdeg : ∀ i, 0 < deg i)
    (hf : ∀ i, f i ∈ 𝒮 (deg i))
    (hgen : Algebra.adjoin (Stacks.Veronese.gradeZero 𝒮) (Set.range f) = ⊤)
    (k : ℤ) :
    letI := (globalSectionsModuleMap 𝒮 𝒨).moduleInst
    letI := (twistedGlobalSectionsModule 𝒮 (associatedModuleSheaf 𝒮 𝒨)).moduleInst
    Module.Finite S ((globalSectionsModuleMap 𝒮 𝒨).truncation 𝒮 𝒨 k) ∧
      Module.Finite S ((twistedGlobalSectionsModule 𝒮
        (associatedModuleSheaf 𝒮 𝒨)).truncation 𝒮 (associatedModuleSheaf 𝒮 𝒨) k) ∧
      (∀ x ∈ twistedSectionsTruncation 𝒮 𝒨 k,
        twistedToShiftedSections 𝒮 𝒨 x ∈ shiftedSectionsTruncation 𝒮 𝒨 k) ∧
      (∃ k₀ : ℤ, ∀ k' ≤ k₀, ∀ m : M,
        (globalSectionsModuleMap 𝒮 𝒨).hom m ∈ shiftedSectionsTruncation 𝒮 𝒨 k') ∧
      (∃ n₀ : ℤ, ∀ n : ℤ, n₀ ≤ n → Function.Bijective (degreeNToGlobalSections 𝒮 𝒨 n)) ∧
      (∀ n : ℤ, ((Finset.univ.lcm deg : ℕ) : ℤ) ∣ n →
        Function.Bijective (twistedToShiftedComponent 𝒮 𝒨 n))

Tag 0BXF, a proposition

Tag 0BXF in the Stacks Project.

Stacks.AlgebraicGeometry.ProjSerreCorrespondence.exists_coherentIrrelevantQuotientEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjSerreCorrespondence/CoherentEquivalence.lean, line 344. The attribute's comment: “the proposition: for A a Noetherian graded ring and X = Proj(A), the functor M ↦ M~ induces an equivalence Mod^fg_A / Mod^fg_{A, irrelevant} ⟶ Coh(O_X) whose quasi-inverse is F ↦ ⨁_{n ≥ 0} Γ(X, F(n)). The degree d of Tag 0BXE, the lcm of the degrees of a finite homogeneous generating set of A over A_0, is produced here as the source produces it; the same statement for an arbitrary d divisible by those degrees is coherentIrrelevantQuotientEquivalence”. References: EGA II (2.7.7), “Coherent noetherian case”.

[Stacks, Tag 0BXF]. Let A be a Noetherian graded ring and X = Proj(A). There is a degree d of the kind [Stacks, Tag 0BXE] asks for — the least common multiple of the degrees of a finite homogeneous generating set of A over A₀ — and for it the functor M ↦ M̃ induces an equivalence

Mod^fg_A / Mod^fg_{A, irrelevant} ⟶ Coh(𝒪_X)

whose quasi-inverse is ℱ ↦ ⨁_{n ≥ 0} Γ(X, ℱ(n)).

The two equations say that the equivalence is the proposition's two functors: its functor is coherentIrrelevantQuotientFunctor, the arrow induced by M ↦ M̃ on the quotient category, and its inverse is coherentTruncatedTwistedSectionsFunctor 𝒮 0 followed by the quotient functor, which is ℱ ↦ ⨁_{n ≥ 0} Γ(X, ℱ(n)).

The degree cannot be quantified away: for A = k[x] with deg x = 2 the module A(1) has vanishing associated sheaf and is not irrelevant at d = 1, so the subcategory of [Stacks, Tag 0BXE], and with it the quotient category, genuinely depends on d being a multiple of the generators' degrees. coherentIrrelevantQuotientEquivalence is the same statement for every such d.

public theorem exists_coherentIrrelevantQuotientEquivalence :
    ∃ (d : ℕ) (hd : 0 < d) (e : IrrelevantQuotient 𝒮 hd ≌
        _root_.AlgebraicGeometry.SheafOfModules.CoherentModules (projRingSheaf 𝒮)),
      e.functor = coherentIrrelevantQuotientFunctor.{u, u} 𝒮 hd ∧
        e.inverse = coherentTruncatedTwistedSectionsFunctor.{u} 𝒮 0 ⋙
          toIrrelevantQuotient.{u, u, u} 𝒮 hd

Stacks.AlgebraicGeometry.ProjSerreCorrespondence.irrelevantModules_prop_of_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjSerreCorrespondence/IrrelevantModules.lean, line 384. The attribute's comment: “only the step that the irrelevant finite graded modules satisfy the Serre-subcategory condition of Tag 02MO, which is what makes the quotient category in the statement exist; the equivalence with Coh(O_X) and its twisted-section quasi-inverse are not formalized, and exactness is spelled elementwise because this library's category of graded modules has no abelian structure yet”.

The irrelevant finitely generated graded modules satisfy the Serre-subcategory condition of Stacks 02MO inside Mod^{fg}_A: they contain every zero module, and they contain the middle term of every exact sequence whose outer terms belong to them.

public theorem irrelevantModules_prop_of_exact {d : ℕ} (hd : 0 < d)
    (M₀ : FiniteGradedModules.{u, v, w} 𝒮) (h₀ : Subsingleton M₀.obj.carrier) :
    irrelevantModules 𝒮 d M₀ ∧
      ∀ (L N P : FiniteGradedModules.{u, v, w} 𝒮) (f : L ⟶ N) (g : N ⟶ P),
        (∀ y : N.obj.carrier, g.hom.toLinearMap y = 0 →
          ∃ x : L.obj.carrier, f.hom.toLinearMap x = y) →
        irrelevantModules 𝒮 d L → irrelevantModules 𝒮 d P → irrelevantModules 𝒮 d N

Stacks.AlgebraicGeometry.ProjSerreCorrespondence.irrelevantQuotientFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjSerreCorrespondence/IrrelevantQuotientFunctor.lean, line 134. The attribute's comment: “the arrow of the proposition: the functor out of the quotient category Mod^fg_A / Mod^fg_{A, irrelevant} induced by M ↦ M~, obtained by factoring that functor's restriction to the finitely generated graded modules through the localization at the isomorphisms modulo the irrelevant ones. Its target is written as all sheaves of O_X-modules; its corestriction to the proposition's own target Coh(O_X) is coherentIrrelevantQuotientFunctor. Of the proposition's assertion that this functor is an equivalence, faithfulness is proved (faithful_irrelevantQuotientFunctor), for the corestriction too (faithful_coherentIrrelevantQuotientFunctor); the whole proposition is now proved, as exists_coherentIrrelevantQuotientEquivalence of CoherentEquivalence.lean. The quasi-inverse F ↦ ⨁_{n ≥ 0} Γ(X, F(n)) is identified on objects, by truncatedTwistedSectionsIsoOfNoetherian, and assembled into a functor to all graded modules, truncatedTwistedSectionsFunctor”.

The functor Mod^fg_A / Mod^fg_{A, irrelevant} ⟶ Mod(𝒪_X) induced by M ↦ M̃. This is the functor of which Stacks 0BXF asserts that it is an equivalence onto Coh(𝒪_X).

public def irrelevantQuotientFunctor (hd : 0 < d) :
    IrrelevantQuotient 𝒮 hd ⥤ SheafOfModules.{u}
      ((sheafCompose (Opens.grothendieckTopology (ProjectiveSpectrum.top 𝒮))
        (forget₂ CommRingCat.{u} RingCat.{u})).obj
          (ProjectiveSpectrum.Proj.structureSheaf 𝒮))

Stacks.AlgebraicGeometry.ProjSerreCorrespondence.isSerreClass_irrelevantModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjSerreCorrespondence/SerreClass.lean, line 213. The attribute's comment: “the Serre-subcategory step of the proposition: the irrelevant finitely generated graded modules are a Serre class in Mod^fg_A, which is what makes the quotient category on the left of the arrow exist, and which this file turns into that quotient category. The equivalence with Coh(O_X) and the identification of its quasi-inverse with F ↦ ⨁_{n ≥ 0} Γ(X, F(n)) are exists_coherentIrrelevantQuotientEquivalence of CoherentEquivalence.lean”.

The irrelevant finitely generated graded modules (Tag 0BXE) are a Serre class in Mod^fg_A: the subcategory contains a zero object and is closed under subobjects, quotients and extensions.

public theorem isSerreClass_irrelevantModules (hd : 0 < d) :
    ObjectProperty.IsSerreClass (irrelevantModules.{u, v, w} 𝒮 d)

Sources

Section30.16 Higher direct images along projective morphisms #

Section 30.16 of the Stacks Project, Tag 0B5S. 3 tags here are carried by 6 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0B5T, a lemma

Tag 0B5T in the Stacks Project.

Stacks.AlgebraicGeometry.ProperAmpleCohomology.exists_epi_biproduct_tensorPowModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProperAmpleCohomology/Basic.lean, line 67. The attribute's comment: “clause (2), the surjection from a finite direct sum of tensor powers; clauses (1), (3), (4) and (5) are not covered”.

Let f : X ⟶ S be proper with S Noetherian, let ℒ be an ample invertible 𝒪_X-module and let ℱ be a coherent 𝒪_X-module. Then there are a finite index type ι, exponents d : ι → ℤ and a surjection ⨁_{j ∈ ι} ℒ ^⊗ dⱼ ↠ ℱ.

theorem exists_epi_biproduct_tensorPowModule {X S : Scheme.{u}} (f : X ⟶ S)
    [AlgebraicGeometry.IsNoetherian S] [IsProper f] (F L : X.Modules)
    [_root_.SheafOfModules.IsCoherent F]
    [IsInvertibleModule X L] (hL : IsAmple X L) :
    ∃ (ι : Type u) (_ : Finite ι) (d : ι → ℤ)
      (b : Bicone fun j : ι => tensorPowModule X L (d j)) (_ : b.IsBilimit)
      (p : b.pt ⟶ F), Epi p

Stacks.AlgebraicGeometry.ProperAmpleCohomology.exists_isZero_Hgroup_tensorPowTwist, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProperAmpleCohomology/Basic.lean, line 84. The attribute's comment: “clause (4), the eventual vanishing of the higher cohomology of the high twists of a coherent module, with one exponent serving every positive degree”.

Let R be a Noetherian ring, let f : X ⟶ Spec R be proper, let ℒ be an ample invertible 𝒪_X-module and let ℱ be a coherent 𝒪_X-module. Then there is a d₀ with

H ᵖ(X, ℱ ⊗ ℒ ^⊗ d) = 0 for every d ≥ d₀ and every p > 0.

theorem exists_isZero_Hgroup_tensorPowTwist {X : Scheme.{u}} {R : Type u}
    [CommRing R] [IsNoetherianRing R] (f : X ⟶ Spec (CommRingCat.of R)) [IsProper f]
    (F L : X.Modules) [_root_.SheafOfModules.IsCoherent F] [IsInvertibleModule X L]
    (hL : IsAmple X L) :
    ∃ d₀ : ℕ, ∀ d p : ℕ, d₀ ≤ d → 0 < p →
      IsZero (Hgroup X.ringCatSheaf ⊤ p
        (Stacks.RelativeVeryAmple.tensorModules X F (tensorPowModule X L (d : ℤ))))

Stacks.AlgebraicGeometry.ProperAmpleCohomology.coherent_proper_ample, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProperAmpleCohomology/CoherentProperAmple.lean, line 112. The attribute's comment: “all five clauses: the section ring is a finitely generated R-algebra, a finite direct sum of tensor powers of L surjects onto F, the cohomology of F is a finite R-module in every degree, the higher cohomology of the high twists of F vanishes, and the graded module of twisted sections in degrees at least k is a finite module over the section ring”.

[Stacks, Tag 0B5T]. Let R be a Noetherian ring, let f : X ⟶ Spec R be proper, let ℒ be an ample invertible 𝒪_X-module and let ℱ be a coherent 𝒪_X-module. Then all five of the tag's assertions hold:

the graded ring A = ⨁_{d ≥ 0} H⁰(X, ℒ ^⊗ d) is a finitely generated R-algebra;

there are a finite index type ι, exponents d : ι → ℤ and a surjection ⨁_{j ∈ ι} ℒ ^⊗ dⱼ ↠ ℱ;

H ᵖ(X, ℱ) is a finite R-module for every p;

there is a d₀ with H ᵖ(X, ℱ ⊗ ℒ ^⊗ d) = 0 for every d ≥ d₀ and every p > 0;

for every k ∈ ℤ the graded A-module ⨁_{d ≥ k} H⁰(X, ℱ ⊗ ℒ ^⊗ d) is a finite A-module.

See the module documentation for the spelling of each clause. The five components are ringHomFiniteType_sectionRing, exists_epi_biproduct_tensorPowModule_of_isAmple, moduleFinite_cohomology_of_isProper, exists_isZero_Hgroup_tensorPowTwist and moduleFinite_twistModule.

theorem coherent_proper_ample {X : Scheme.{u}} {R : Type u} [CommRing R] [IsNoetherianRing R]
    (f : X ⟶ Spec (CommRingCat.of R)) [IsProper f] (F L : X.Modules)
    [_root_.SheafOfModules.IsCoherent F] [Stacks.Ample.IsInvertibleModule X L]
    (hL : Stacks.Ample.IsAmple X L) :
    RingHom.FiniteType
        ((sectionRingZeroHom X L).comp (specAlgebraRingHom R f)) ∧
      (∃ (ι : Type u) (_ : Finite ι) (d : ι → ℤ)
        (b : Bicone fun j : ι => Stacks.Ample.tensorPowModule X L (d j)) (_ : b.IsBilimit)
        (p : b.pt ⟶ F), Epi p) ∧
      (∀ p : ℕ, Module.Finite R
        ((ModuleCat.restrictScalars (specAlgebraRingHom R f)).obj (cohomologyOf X p F))) ∧
      (∃ d₀ : ℕ, ∀ d p : ℕ, d₀ ≤ d → 0 < p →
        IsZero (Hgroup X.ringCatSheaf ⊤ p
          (Stacks.RelativeVeryAmple.tensorModules X F
            (Stacks.Ample.tensorPowModule X L (d : ℤ))))) ∧
      (∀ k : ℤ, Module.Finite (sectionRing L)
        (twistModule (F ⊗ Stacks.Ample.tensorPowModule X L k) L))

Stacks.AlgebraicGeometry.ProperAmpleCohomology.moduleFinite_cohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProperAmpleCohomology/CohomologyFinite.lean, line 95. The attribute's comment: “clause (3), the finiteness of the cohomology of a coherent module over the Noetherian base ring”.

Clause (3) of [Stacks, Tag 0B5T]. Let R be a Noetherian ring, let f : X ⟶ Spec R be proper, let ℒ be an ample invertible 𝒪_X-module and let ℱ be a coherent 𝒪_X-module. Then Hᵖ(X, ℱ) is a finite R-module for every p.

This is moduleFinite_cohomology_of_isProper with the tag's remaining hypotheses bound; the ample invertible module is not used, and the more general statement is the one to apply. The tag's clause (3) is recorded here so that it sits on a declaration stating the clause in the tag's own setting.

theorem moduleFinite_cohomology {X : Scheme.{u}} {R : Type u} [CommRing R] [IsNoetherianRing R]
    (f : X ⟶ Spec (CommRingCat.of R)) [IsProper f] (F L : X.Modules)
    [_root_.SheafOfModules.IsCoherent F] [IsInvertibleModule X L] (_hL : IsAmple X L) (p : ℕ) :
    Module.Finite R ((ModuleCat.restrictScalars (specAlgebraRingHom R f)).obj
      (cohomologyOf X p F))

Tag 02O1, a lemma

Tag 02O1 in the Stacks Project.

Stacks.AlgebraicGeometry.AmpleTwistAcyclicity.exists_isZero_rightDerivedPlus_pushforward_tensorPowModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleTwistAcyclicity/Basic.lean, line 350.

[Stacks, Tag 02O1], with no hypothesis. Let f : X ⟶ S be a proper morphism of schemes with S Noetherian, let ℱ be a coherent 𝒪_X-module and let ℒ be an invertible 𝒪_X-module ample relative to f. Then there is an n₀ such that for all n ≥ n₀,

R ᵖ f_* (ℱ ⊗ ℒ ^⊗ n) = 0 for every p > 0,

with the one bound n₀ serving every positive degree.

This is Stacks.AlgebraicGeometry.RelativeAmpleTwistVanishing .exists_isZero_rightDerivedPlus_pushforward_tensorPowModule with its hypothesis haffine discharged by vanishingOverAffineBase.

theorem exists_isZero_rightDerivedPlus_pushforward_tensorPowModule {X S : Scheme.{u}} (f : X ⟶ S)
    [AlgebraicGeometry.IsNoetherian S] [IsProper f] (F L : X.Modules) [F.IsCoherent]
    [IsInvertibleModule X L] (hL : Stacks.RelativeAmple.IsRelativelyAmple f L) :
    ∃ n₀ : ℕ, ∀ n p : ℕ, n₀ ≤ n → 0 < p →
      IsZero (((Scheme.Modules.pushforward f).rightDerivedPlus (p : ℤ)).obj
        (tensorModules X F (tensorPowModule X L (n : ℤ))))

Tag 02O4, a lemma

Tag 02O4 in the Stacks Project.

AlgebraicGeometry.LocallyProjectiveCoherentImage.isCoherent_rightDerived_of_isLocallyProjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocallyProjectiveCoherentImage/Basic.lean, line 155.

[Stacks, Tag 02O4]. For S locally Noetherian, f : X ⟶ S locally H-projective and ℱ a coherent 𝒪_X-module, the higher direct image R^i f_* ℱ is coherent for every i ≥ 0.

Local H-projectivity supplies an open cover of S over whose members f is H-projective — the definition states this for pullback.snd f (𝒰.f i), which is isomorphic as an arrow to f ∣_ (𝒰.f i).opensRange — and coherence of a higher direct image is local on the base.

theorem isCoherent_rightDerived_of_isLocallyProjective {X S : Scheme.{u}} (f : X ⟶ S)
    [IsLocallyNoetherian S] (hf : IsLocallyProjectiveMorphism f) (F : X.Modules)
    (hF : F.IsCoherent) (i : ℕ) :
    (((Scheme.Modules.pushforward f).rightDerived i).obj F).IsCoherent

Sources

LeanStacks.AlgebraicGeometry.ProperAmpleCohomology.exists_epi_biproduct_tensorPowModule · Stacks.AlgebraicGeometry.ProperAmpleCohomology.exists_isZero_Hgroup_tensorPowTwist · Stacks.AlgebraicGeometry.ProperAmpleCohomology.coherent_proper_ample · Stacks.AlgebraicGeometry.ProperAmpleCohomology.moduleFinite_cohomology · Stacks.AlgebraicGeometry.AmpleTwistAcyclicity.exists_isZero_rightDerivedPlus_pushforward_tensorPowModule · AlgebraicGeometry.LocallyProjectiveCoherentImage.isCoherent_rightDerived_of_isLocallyProjective

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

30.2 Čech cohomology of… to 30.16 Higher direct images…

Section30.2 Čech cohomology of quasi-coherent sheaves#

Tag 01X9, a lemma

Tag 01XB, a lemma

Tag 01XC, a lemma

Tag 089W, a lemma

Tag 0BDX, a lemma

Tag 01XD, a lemma

Sources

Section30.3 Vanishing of cohomology#

Tag 01XF, a lemma

Tag 01XG, a lemma

Tag 0B5P, a lemma

Tag 0F83, a lemma

Sources

Section30.4 Quasi-coherence of higher direct images#

Tag 08DR, a lemma

Tag 01XI, a lemma

Tag 0BDY, a lemma

Tag 071L, a lemma

Tag 01XJ, a lemma

Tag 01XK, a lemma

Sources

Section30.5 Cohomology and base change, I#

Tag 02KF, an equation

Tag 02KG, a lemma

Tag 02KH, a lemma

Tag 0CKW, a lemma

Sources

Section30.6 Colimits and higher direct images#

Tag 07TB, a lemma

Sources

Section30.7 Cohomology and base change, II#

Tag 01XL, a lemma

Tag 01XM, a lemma

Tag 01XN, a lemma

Tag 0GN5, a lemma

Sources

Section30.8 Cohomology of projective space#

Tag 01XT, a lemma

Tag 01XU, an equation

Tag 01XV, a lemma

Tag 01XW, a lemma

Tag 01XX, a lemma

Sources

Section30.9 Coherent sheaves on locally Noetherian schemes#

Tag 01XZ, a lemma

Tag 01Y0, a lemma

Tag 01Y1, a lemma

Tag 01Y2, a lemma

Tag 01Y3, a lemma

Tag 01Y4, a lemma

Tag 01Y5, a lemma

Tag 087T, a lemma

Tag 01Y6, a lemma

Tag 0B3J, a lemma

Tag 0CYJ, a lemma

Sources

Section30.10 Coherent sheaves on Noetherian schemes#

Tag 01Y8, a lemma

Tag 01Y9, a lemma

Tag 01YA, a lemma

Tag 0GN6, a lemma

Tag 01YB, a lemma

Tag 0FD0, a lemma

Sources

Section30.11 Depth#

Tag 0341, a definition

Tag 0EBC, a lemma

Tag 0AXQ, a lemma

Tag 0343, a definition

Tag 0B3K, a lemma

Sources

Section30.12 Devissage of coherent sheaves#

Tag 01YD, a lemma

Tag 01YE, a lemma

Tag 01YF, a lemma

Tag 01YG, a lemma

Tag 01YH, a lemma

Tag 01YI, a lemma

Section30.2 Čech cohomology of quasi-coherent sheaves #

Section30.3 Vanishing of cohomology #

Section30.4 Quasi-coherence of higher direct images #

Section30.5 Cohomology and base change, I #

Section30.6 Colimits and higher direct images #

Section30.7 Cohomology and base change, II #

Section30.8 Cohomology of projective space #

Section30.9 Coherent sheaves on locally Noetherian schemes #

Section30.10 Coherent sheaves on Noetherian schemes #

Section30.11 Depth #

Section30.12 Devissage of coherent sheaves #

Section30.13 Finite morphisms and affines #

Section30.14 Coherent sheaves on Proj, I #

Section30.15 Coherent sheaves on Proj, II #

Section30.16 Higher direct images along projective morphisms #