36.10 Pseudo-coherent and… to 36.21 The coherator revisited

Section36.10 Pseudo-coherent and perfect complexes#

Section 36.10 of the Stacks Project, Tag 08E4. 9 tags here are carried by 38 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 08E5, a lemma

Tag 08E5 in the Stacks Project.

AlgebraicGeometry.isQuasicoherent_homology_of_isPseudoCoherentFrom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/QuasicoherentCohomology.lean, line 133. The attribute's comment: “cohomology above m”.

Let X be a scheme and let E be an m-pseudo-coherent object of D(𝒪_X). Then the cohomology sheaf H^i(E) is a quasi-coherent 𝒪_X-module for every i > m.

public theorem isQuasicoherent_homology_of_isPseudoCoherentFrom (X : Scheme.{u})
    [HasDerivedCategory.{d} (StrictlyPerfect.OXMod.{u, u, u} X.toRingedSpace)]
    (E : DerivedCategory (StrictlyPerfect.OXMod.{u, u, u} X.toRingedSpace)) (m i : ℤ)
    (hE : RingedSpace.IsPseudoCoherentFrom (X := X.toRingedSpace) E m) (hi : m < i) :
    ((DerivedCategory.homologyFunctor
      (StrictlyPerfect.OXMod.{u, u, u} X.toRingedSpace) i).obj E).IsQuasicoherent

AlgebraicGeometry.exists_local_epi_homology_of_isPseudoCoherentFrom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/QuasicoherentCohomology.lean, line 176. The attribute's comment: “cohomology in degree m, locally”.

Let X be a scheme and let E be an m-pseudo-coherent object of D(𝒪_X). Then every point of X has an open neighbourhood U on which H^m(E) is a quotient of a quasi-coherent 𝒪_U-module.

Stacks erratum. The source states this clause globally — that H^m(E) is a quotient of a quasi-coherent module on all of X — and that is false; the corrected clause is the local one stated here.

The counterexample is on X = Spec k[x, y]. With L = V(x), i : L → X and Q = i_* i^{-1}𝒪_X the pushforward of the ordinary inverse image of 𝒪_X, the function g = x - y(y-1) — the equation of the irreducible curve through p0 = (0, 0) and p1 = (0, 1) — is invertible on Q over U ∩ V, where U = X ∖ {p0} and V = X ∖ {p1}. Gluing Q|_U to Q|_V along a = g b gives an 𝒪_X-module F that is locally cyclic, so F[0] is 0-pseudo-coherent, yet every global section of F vanishes in the fibre at p1 by the valuation along g = 0; as X is affine, no quasi-coherent module surjects onto F. Quasi-compactness and quasi-separatedness would not have rescued the global form: Spec k[x, y] has both.

public theorem exists_local_epi_homology_of_isPseudoCoherentFrom (X : Scheme.{u})
    [HasDerivedCategory.{d} (StrictlyPerfect.OXMod.{u, u, u} X.toRingedSpace)]
    (E : DerivedCategory (StrictlyPerfect.OXMod.{u, u, u} X.toRingedSpace)) (m : ℤ)
    (hE : RingedSpace.IsPseudoCoherentFrom (X := X.toRingedSpace) E m) (x : X) :
    ∃ U : X.Opens, x ∈ U ∧ ∃ M : U.toScheme.Modules, M.IsQuasicoherent ∧
      ∃ f : M ⟶ (Scheme.Modules.restrictFunctor U.ι).obj
        ((DerivedCategory.homologyFunctor
          (StrictlyPerfect.OXMod.{u, u, u} X.toRingedSpace) m).obj E), Epi f

AlgebraicGeometry.isQuasicoherentDerived_of_isPseudoCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/QuasicoherentCohomology.lean, line 196. The attribute's comment: “pseudo-coherent objects”.

A pseudo-coherent object of D(𝒪_X) on a scheme has quasi-coherent cohomology in every degree, that is, it belongs to D_QCoh(𝒪_X).

public theorem isQuasicoherentDerived_of_isPseudoCoherent (X : Scheme.{u})
    [HasDerivedCategory.{d} (StrictlyPerfect.OXMod.{u, u, u} X.toRingedSpace)]
    (E : DerivedCategory (StrictlyPerfect.OXMod.{u, u, u} X.toRingedSpace))
    (hE : RingedSpace.IsPseudoCoherent (X := X.toRingedSpace) E) :
    DerivedCategoryB.derivedCategoryB
      (SheafOfModules.isQuasicoherent
        (StrictlyPerfect.structureSheafOfRings X.toRingedSpace)) E

Tag 08E7, a lemma

Tag 08E7 in the Stacks Project.

AlgebraicGeometry.RingedSpace.isPseudoCoherentFrom_tilde_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/PseudoCoherentFrom/Affine.lean, line 444. The attribute's comment: “m-pseudo-coherent”.

Tag 08E7 for m-pseudo-coherence. A complex of A-modules is m-pseudo-coherent exactly when the complex of 𝒪-modules it determines on Spec A is m-pseudo-coherent.

public theorem isPseudoCoherentFrom_tilde_iff {A : Type u} [CommRing A]
    (M : CochainComplex (ModuleCat.{u} A) ℤ) (m : ℤ) :
    IsPseudoCoherentFrom (X := (Spec (CommRingCat.of A)).toRingedSpace)
        (DerivedCategory.Q.obj
          (((tilde.functor (CommRingCat.of A) :
            ModuleCat.{u} A ⥤ OXMod.{u, u} (Spec (CommRingCat.of A)).toRingedSpace
            ).mapHomologicalComplex (ComplexShape.up ℤ)).obj M)) m ↔
      StacksDraft.PseudoCoherence.IsPseudoCoherentFrom (DerivedCategory.Q.obj M) m

AlgebraicGeometry.RingedSpace.isPseudoCoherent_tilde_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/PseudoCoherentFrom/Affine.lean, line 480. The attribute's comment: “pseudo-coherent”.

Tag 08E7 for pseudo-coherence. A complex of A-modules is pseudo-coherent exactly when the complex of 𝒪-modules it determines on Spec A is pseudo-coherent. Both sides are equivalent to the conjunction over all degrees of the fixed-degree condition: on the module side by Stacks 064W, on the sheaf side because Tag 08CC part (2) lets the one complex representing the object serve as the m-pseudo-coherent representative for every m.

public theorem isPseudoCoherent_tilde_iff {A : Type u} [CommRing A]
    (M : CochainComplex (ModuleCat.{u} A) ℤ) :
    IsPseudoCoherent (X := (Spec (CommRingCat.of A)).toRingedSpace)
        (DerivedCategory.Q.obj
          (((tilde.functor (CommRingCat.of A) :
            ModuleCat.{u} A ⥤ OXMod.{u, u} (Spec (CommRingCat.of A)).toRingedSpace
            ).mapHomologicalComplex (ComplexShape.up ℤ)).obj M)) ↔
      StacksDraft.PseudoCoherence.IsPseudoCoherent (DerivedCategory.Q.obj M)

AlgebraicGeometry.RingedSpace.isPseudoCoherentFrom_tilde_iff_locallySmall, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/PseudoCoherentFrom/AffineLocallySmall.lean, line 172. The attribute's comment: “m-pseudo-coherent, at the locally small derived category”.

Tag 08E7 for m-pseudo-coherence, at the locally small derived category. A complex of A-modules is m-pseudo-coherent exactly when the complex of 𝒪-modules it determines on Spec A is m-pseudo-coherent as an object of the derived category of 𝒪_{Spec A}-modules whose morphisms are in Type u. That is the derived category at which derived sheafification and the affine base-change comparison are stated.

public theorem isPseudoCoherentFrom_tilde_iff_locallySmall {A : Type u} [CommRing A]
    (M : CochainComplex (ModuleCat.{u} A) ℤ) (m : ℤ) :
    IsPseudoCoherentFrom (X := (Spec (CommRingCat.of A)).toRingedSpace)
        (DerivedCategory.Q.obj
          (((tilde.functor (CommRingCat.of A) :
            ModuleCat.{u} A ⥤ OXMod.{u, u} (Spec (CommRingCat.of A)).toRingedSpace
            ).mapHomologicalComplex (ComplexShape.up ℤ)).obj M)) m ↔
      StacksDraft.PseudoCoherence.IsPseudoCoherentFrom (DerivedCategory.Q.obj M) m

AlgebraicGeometry.RingedSpace.isPseudoCoherent_tilde_iff_locallySmall, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/PseudoCoherentFrom/AffineLocallySmall.lean, line 187. The attribute's comment: “pseudo-coherent, at the locally small derived category”.

Tag 08E7 for pseudo-coherence, at the locally small derived category. A complex of A-modules is pseudo-coherent exactly when the complex of 𝒪-modules it determines on Spec A is pseudo-coherent as an object of the derived category of 𝒪_{Spec A}-modules whose morphisms are in Type u.

public theorem isPseudoCoherent_tilde_iff_locallySmall {A : Type u} [CommRing A]
    (M : CochainComplex (ModuleCat.{u} A) ℤ) :
    IsPseudoCoherent (X := (Spec (CommRingCat.of A)).toRingedSpace)
        (DerivedCategory.Q.obj
          (((tilde.functor (CommRingCat.of A) :
            ModuleCat.{u} A ⥤ OXMod.{u, u} (Spec (CommRingCat.of A)).toRingedSpace
            ).mapHomologicalComplex (ComplexShape.up ℤ)).obj M)) ↔
      StacksDraft.PseudoCoherence.IsPseudoCoherent (DerivedCategory.Q.obj M)

Stacks.AffineTilde.isPseudoCoherentFrom_of_isPseudoCoherentFrom_tildeComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/PseudoCoherentRelative/TildeConverse.lean, line 215. The attribute's comment: “m-pseudo-coherent, the direction from sheaves to modules”.

Stacks 08E7, the direction from sheaves to modules. If the object of D(𝒪_{Spec R}) determined by a complex M^• of R-modules is m-pseudo-coherent (Stacks 08CB (3)), then M^• is m-pseudo-coherent as a complex of R-modules (Stacks 064Q (1)).

The standard opens over which the localization of M^• is m-pseudo-coherent generate the unit ideal, because every point of Spec R lies in one of them; a finite subfamily still does, and Stacks 066D descends m-pseudo-coherence along it.

theorem isPseudoCoherentFrom_of_isPseudoCoherentFrom_tildeComplex
    (h : AlgebraicGeometry.RingedSpace.IsPseudoCoherentFrom
      (X := (Spec R).toRingedSpace) (DerivedCategory.Q.obj (tildeComplex M)) m) :
    IsPseudoCoherentFrom (DerivedCategory.Q.obj M) m

Stacks.AffineTilde.isPseudoCoherent_of_isPseudoCoherent_tildeComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/PseudoCoherentRelative/TildeConverse.lean, line 241. The attribute's comment: “pseudo-coherent, the direction from sheaves to modules”.

Stacks 08E7, the direction from sheaves to modules, all degrees at once. If the object of D(𝒪_{Spec R}) determined by a complex M^• of R-modules is pseudo-coherent (Stacks 08CB (3)), then M^• is pseudo-coherent as a complex of R-modules (Stacks 064Q (2)).

Both notions are m-pseudo-coherence for every m — at the level of sheaves by definition, at the level of modules by Stacks 064U (StacksDraft.PseudoCoherence.pseudoCoherent_iff_all) — so this is the previous result applied degree by degree, with the representative the hypothesis supplies serving for all degrees.

theorem isPseudoCoherent_of_isPseudoCoherent_tildeComplex
    (h : AlgebraicGeometry.RingedSpace.IsPseudoCoherent
      (X := (Spec R).toRingedSpace) (DerivedCategory.Q.obj (tildeComplex M))) :
    IsPseudoCoherent (DerivedCategory.Q.obj M)

Stacks.AffineTilde.isPseudoCoherentFrom_tildeComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/PseudoCoherentRelative/TildePseudoCoherent.lean, line 142. The attribute's comment: “m-pseudo-coherent, the direction from modules to sheaves”.

Stacks 08E7, the direction from modules to sheaves. If a complex M^• of R-modules is m-pseudo-coherent (Stacks 064Q (1)), then the object of D(𝒪_{Spec R}) it determines is m-pseudo-coherent (Stacks 08CB (3)).

theorem isPseudoCoherentFrom_tildeComplex (M : CochainComplex (ModuleCat.{u} R) ℤ) (m : ℤ)
    (h : StacksDraft.PseudoCoherence.IsPseudoCoherentFrom (DerivedCategory.Q.obj M) m) :
    AlgebraicGeometry.RingedSpace.IsPseudoCoherentFrom
      (X := (Spec R).toRingedSpace) (DerivedCategory.Q.obj (tildeComplex M)) m

Stacks.AffineTilde.isPseudoCoherent_tildeComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/PseudoCoherentRelative/TildePseudoCoherent.lean, line 159. The attribute's comment: “pseudo-coherent, the direction from modules to sheaves”.

Stacks 08E7, the direction from modules to sheaves, all degrees at once. If a complex M^• of R-modules is pseudo-coherent (Stacks 064Q (2)), then the object of D(𝒪_{Spec R}) it determines is pseudo-coherent (Stacks 08CB (3)).

Both notions of pseudo-coherence are m-pseudo-coherence for every m — at the level of modules by Stacks 064U (StacksDraft.PseudoCoherence.pseudoCoherent_iff_all), at the level of sheaves by definition — so this follows from Stacks.AffineTilde.isPseudoCoherentComplexFrom_tildeComplex degree by degree, with the single representative \widetilde{M^•} serving for all degrees.

theorem isPseudoCoherent_tildeComplex (M : CochainComplex (ModuleCat.{u} R) ℤ)
    (h : StacksDraft.PseudoCoherence.IsPseudoCoherent (DerivedCategory.Q.obj M)) :
    AlgebraicGeometry.RingedSpace.IsPseudoCoherent
      (X := (Spec R).toRingedSpace) (DerivedCategory.Q.obj (tildeComplex M))

Tag 08E8, a lemma

Tag 08E8 in the Stacks Project.

AlgebraicGeometry.isPseudoCoherentFrom_iff_coherent_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/Noetherian/CoherentHomology.lean, line 137. The attribute's comment: “equivalence in degree m”. References: SGA 6 I (3.5), “b), Noetherian scheme”.

Stacks Project, Tag 08E8. Let X be a Noetherian scheme, let E be an object of D_QCoh(𝒪_X) and let m be an integer. Then E is m-pseudo-coherent if and only if Hⁱ(E) is coherent for every i ≥ m and vanishes for i ≫ 0.

public theorem isPseudoCoherentFrom_iff_coherent_homology (X : Scheme.{u}) [IsNoetherian X]
    (E : (DerivedCategoryB.derivedCategoryB
      (SheafOfModules.isQuasicoherent X.ringCatSheaf)).FullSubcategory)
    (m : ℤ) :
    RingedSpace.IsPseudoCoherentFrom (X := X.toRingedSpace) E.1 m ↔
      ((∀ i : ℤ, m ≤ i →
          ((DerivedCategory.homologyFunctor X.Modules i).obj E.1).IsCoherent) ∧
        DerivedCategoryB.IsBoundedAbove E.1)

AlgebraicGeometry.isPseudoCoherent_iff_boundedAbove_coherent_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/Noetherian/CoherentHomology.lean, line 158. The attribute's comment: “identification with D⁻_Coh”. References: SGA 6 I (3.5), “b) last claim, Noeth X”.

Stacks Project, Tag 08E8, the final statement. On a Noetherian scheme an object of D_QCoh(𝒪_X) is pseudo-coherent if and only if it is bounded above and all of its cohomology sheaves are coherent, that is, if and only if it is an object of D⁻_Coh(𝒪_X).

public theorem isPseudoCoherent_iff_boundedAbove_coherent_homology (X : Scheme.{u})
    [IsNoetherian X]
    (E : (DerivedCategoryB.derivedCategoryB
      (SheafOfModules.isQuasicoherent X.ringCatSheaf)).FullSubcategory) :
    RingedSpace.IsPseudoCoherent (X := X.toRingedSpace) E.1 ↔
      (DerivedCategoryB.IsBoundedAbove E.1 ∧
        ∀ i : ℤ,
          ((DerivedCategory.homologyFunctor X.Modules i).obj E.1).IsCoherent)

Tag 08E9, a lemma

Tag 08E9 in the Stacks Project.

AlgebraicGeometry.hasTorAmplitude_tilde_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedTildeTorAmplitude.lean, line 286. The attribute's comment: “part (1)”.

Stacks 08E9 (1). Let X = Spec R be an affine scheme and let M be an object of D(R). Then the associated object M̃ of D(𝒪_X) has Tor amplitude in [a, b] if and only if M has Tor amplitude in [a, b].

theorem hasTorAmplitude_tilde_iff (M : DerivedCategory (ModuleCat.{u} R)) (a b : ℤ) :
    Stacks.Cohomology.TorAmplitude.HasTorAmplitude (Spec R).toRingedSpace
        ((tilde.functor R).mapDerivedCategory.obj M) a b ↔
      StacksDraft.TorAmplitude.HasTorAmplitudeCanonical R M a b

AlgebraicGeometry.hasFiniteTorDimension_tilde_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedTildeTorAmplitude.lean, line 320. The attribute's comment: “part (2)”.

Stacks 08E9 (2). Let X = Spec R be an affine scheme and let M be an object of D(R). Then the associated object M̃ of D(𝒪_X) has finite Tor dimension if and only if M has finite Tor dimension.

theorem hasFiniteTorDimension_tilde_iff (M : DerivedCategory (ModuleCat.{u} R)) :
    Stacks.Cohomology.TorAmplitude.HasFiniteTorDimension (Spec R).toRingedSpace
        ((tilde.functor R).mapDerivedCategory.obj M) ↔
      StacksDraft.TorAmplitude.HasFiniteTorDimensionCanonical R M

Tag 0DHY, a lemma

Tag 0DHY in the Stacks Project.

AlgebraicGeometry.AffineRelativeTorAmplitude.hasTorAmplitude_relativeComplex_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeTorAmplitudeAffine.lean, line 1104. The attribute's comment: “part (1)”.

Stacks 0DHY, part (1). Let f : Spec A ⟶ Spec R be the morphism of affine schemes of a ring map R → A, let M^• be a complex of A-modules and let E be the complex of f^{-1}𝒪_{Spec R}-modules attached to it. Then E has Tor amplitude in [a, b] over f^{-1}𝒪_{Spec R} if and only if M^•, read as a complex of R-modules, has Tor amplitude in [a, b] over R.

Tor amplitude on the sheaf side is tested at the fibres of the topological points by hasTorAmplitude_iff_forall_pointFiber, where it becomes the Tor amplitude of the localisation of M^• at each prime of A over the corresponding localisation of R (hasTorAmplitudeCanonical_derivedModuleFiber_iff); that family of conditions is Tor amplitude over R by hasTorAmplitudeCanonical_restrictScalars_iff_forall_isPrime.

theorem hasTorAmplitude_relativeComplex_iff (M : CochainComplex (ModuleCat.{u} A) ℤ) (a b : ℤ) :
    Stacks.Cohomology.TorAmplitude.HasTorAmplitude (relativeRingedSpace R A)
        (DerivedCategory.Q.obj (relativeComplex R A M)) a b ↔
      HasTorAmplitudeCanonical R (DerivedCategory.Q.obj
        (((ModuleCat.restrictScalars (algebraMap R A)).mapHomologicalComplex
          (ComplexShape.up ℤ)).obj M)) a b

AlgebraicGeometry.AffineRelativeTorAmplitude.locallyHasFiniteTorDimension_relativeComplex_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeTorAmplitudeAffine.lean, line 1126. The attribute's comment: “part (2)”.

Stacks 0DHY, part (2). In the situation of part (1), the complex E of f^{-1}𝒪_{Spec R}-modules locally has finite Tor dimension if and only if M^•, read as a complex of R-modules, has finite Tor dimension over R.

The space Spec A is quasi-compact, so locally finite Tor dimension is Tor amplitude in a single interval (locallyHasFiniteTorDimension_iff_hasFiniteTorDimension), and part (1) translates each interval.

theorem locallyHasFiniteTorDimension_relativeComplex_iff
    (M : CochainComplex (ModuleCat.{u} A) ℤ) :
    LocallyHasFiniteTorDimension (relativeRingedSpace R A)
        (DerivedCategory.Q.obj (relativeComplex R A M)) ↔
      HasFiniteTorDimensionCanonical R (DerivedCategory.Q.obj
        (((ModuleCat.restrictScalars (algebraMap R A)).mapHomologicalComplex
          (ComplexShape.up ℤ)).obj M))

Tag 08EA, a lemma

Tag 08EA in the Stacks Project.

AlgebraicGeometry.hasTorAmplitude_iff_hasTorAmplitudeOnQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/TorAmplitudeQuasiCoherentTestsGlobal.lean, line 143.

Stacks 08EA. Let X be a quasi-separated scheme, E an object of D_QCoh(𝒪_X) and a ≤ b. The following are equivalent:

1. E has Tor amplitude in [a, b];
2. H^i(E ⊗^L_{𝒪_X} ℱ) = 0 for i ∉ [a, b] and every quasi-coherent 𝒪_X-module ℱ.

Neither direction uses a ≤ b.

theorem hasTorAmplitude_iff_hasTorAmplitudeOnQuasicoherent {X : Scheme.{u}}
    [QuasiSeparatedSpace X] (E : DerivedCategory (OXMod.{u, u} X.toRingedSpace)) (a b : ℤ)
    (hqc : ∀ n : ℤ, ((DerivedCategory.homologyFunctor X.Modules n).obj E).IsQuasicoherent) :
    Stacks.Cohomology.TorAmplitude.HasTorAmplitude X.toRingedSpace E a b ↔
      Stacks.Cohomology.TorAmplitude.HasTorAmplitudeOnQuasicoherent X.toRingedSpace E a b

Tag 08EB, a lemma

Tag 08EB in the Stacks Project.

AlgebraicGeometry.isPerfect_tilde_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedTildePerfect.lean, line 134.

Stacks 08EB. Let X = Spec R be an affine scheme and let M be an object of D(R). Then the associated object M̃ of D(𝒪_X) is a perfect object of D(𝒪_X) if and only if M is a perfect object of D(R).

theorem isPerfect_tilde_iff (M : DerivedCategory (ModuleCat.{u} R)) :
    Stacks.Cohomology.PerfectComplexes.IsPerfect
        ((tilde.functor R).mapDerivedCategory.obj M) ↔
      StacksDraft.Perfect.IsPerfect M

AlgebraicGeometry.isPerfect_tilde_iff_of_model, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedTildePerfect.lean, line 184.

Stacks 08EB at an arbitrary pair of chosen derived categories. Let X = Spec R be an affine scheme and let M be an object of D(R), for any chosen model of D(R) and any chosen model of D(𝒪_X), with the two morphism universes unrelated. Then the associated object M̃ of D(𝒪_X) is a perfect object of D(𝒪_X) if and only if M is a perfect object of D(R).

theorem isPerfect_tilde_iff_of_model [HasDerivedCategory.{w} (ModuleCat.{u} R)]
    [hS : HasDerivedCategory.{w'} (Spec R).Modules] (M : DerivedCategory (ModuleCat.{u} R)) :
    @Stacks.Cohomology.PerfectComplexes.IsPerfect (Spec R).toRingedSpace hS
        ((tilde.functor R).mapDerivedCategory.obj M) ↔
      StacksDraft.Perfect.IsPerfect M

Tag 0A6H, a lemma

Tag 0A6H in the Stacks Project.

AlgebraicGeometry.affineDerivedTildeHomComparison_perfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedTilde/AffineDerivedHom/Comparison.lean, line 624. The attribute's comment: “(3)(b) K perfect and L arbitrary: the canonical comparison is the inverse of the isomorphism”.

The canonical comparison agrees with clause (3)(b). For K perfect it is the inverse of the isomorphism affinePerfectDerivedSheafHomIso, hence invertible. This is what identifies the comparison as the morphism whose invertibility clause (3)(b) asserts, rather than as some morphism between the right two objects: the two are equal because they agree on bounded finite-projective sources with K-injective targets, where both are the five-fold model composite, and because both are natural.

public theorem affineDerivedTildeHomComparison_perfect (R : CommRingCat.{u})
    (K L : DerivedCategory (ModuleCat.{u} R))
    (hK : StacksDraft.Perfect.IsPerfect K) :
    affineDerivedTildeHomComparison R K L =
      (affinePerfectDerivedSheafHomIso R K L hK).inv

AlgebraicGeometry.affinePerfectDerivedSheafHomIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedTilde/AffineDerivedHom/PerfectSource.lean, line 607. The attribute's comment: “(3)(b) K perfect and L arbitrary”.

Stacks 0A6H, clause (3), case (b). Let R be a commutative ring, X = Spec R, and let K, L be objects of D(R) with K perfect. Then the derived internal Hom of the derived sheafifications is the derived sheafification of the derived Hom over R:

R𝓗om_{𝒪_X}(K̃, L̃) ≅ (R Hom_R(K, L))~.

The object L is arbitrary. The isomorphism is not an arbitrary one: it is pinned down on bounded finite-projective representatives by affinePerfectDerivedSheafHomIso_model, and it is natural in both arguments by affinePerfectDerivedSheafHomIso_natural_left and _natural_right.

public def affinePerfectDerivedSheafHomIso (R : CommRingCat.{u})
    (K L : DerivedCategory (ModuleCat.{u} R))
    (hK : StacksDraft.Perfect.IsPerfect K) :
    ((Stacks.SheafOfModules.derivedSheafHom (Spec R).sheaf).obj
        (op ((tildeDer R).obj K))).obj ((tildeDer R).obj L) ≅
      (tildeDer R).obj
        ((StacksDraft.DerivedHom.derivedHomAdjunction (R := R)).hom.obj (op K, L))

AlgebraicGeometry.affinePerfectDerivedSheafHomIso_model, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedTilde/AffineDerivedHom/PerfectSource.lean, line 622. The attribute's comment: “(3)(b) K perfect and L arbitrary”.

The normalization of clause (3)(b). On a bounded complex P of finite projective modules the comparison is the sheafification of the ordinary Hom-complex comparison affineHomComplexTildeIso, read through the [Stacks, Tag 08JH] comparison on the sheaf side and the [Stacks, Tag 0A66] comparison on the module side. This identifies the isomorphism, not just its source and target.

public theorem affinePerfectDerivedSheafHomIso_model (R : CommRingCat.{u})
    (P L : CochainComplex (ModuleCat.{u} R) ℤ) (b : ℤ)
    [P.IsStrictlyLE b] [∀ i, Projective (P.X i)] [∀ i, Module.Finite R (P.X i)]
    (hP : {i : ℤ | ¬ IsZero (P.X i)}.Finite)
    (hK : StacksDraft.Perfect.IsPerfect (DerivedCategory.Q.obj P)) :
    strictlyPerfectHomComparison (specSite R) (specRHom R)
          ((tildeCx R).obj P) ((tildeCx R).obj L) ≫
        ((specRHom R).hom.map ((tilde.functor R).mapDerivedCategoryFactors.hom.app P).op).app
          (DerivedCategory.Q.obj ((tildeCx R).obj L)) ≫
        ((specRHom R).hom.obj (op ((tildeDer R).obj (DerivedCategory.Q.obj P)))).map
          ((tilde.functor R).mapDerivedCategoryFactors.inv.app L) ≫
        (affinePerfectDerivedSheafHomIso R (DerivedCategory.Q.obj P)
          (DerivedCategory.Q.obj L) hK).hom ≫
        (tildeDer R).map (StacksDraft.DerivedHom.projectiveHomComparison.iso P L b).hom ≫
        (tilde.functor R).mapDerivedCategoryFactors.hom.app
          (CochainComplex.HomComplexR R P L) =
      (DerivedCategory.Q.mapIso (affineHomComplexTildeIso R P L hP)).hom

AlgebraicGeometry.affinePerfectDerivedSheafHomIso_natural_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedTilde/AffineDerivedHom/PerfectSource.lean, line 652. The attribute's comment: “(3)(b) K perfect and L arbitrary”.

Clause (3)(b) is natural in the target.

public theorem affinePerfectDerivedSheafHomIso_natural_right (R : CommRingCat.{u})
    (K : DerivedCategory (ModuleCat.{u} R))
    (hK : StacksDraft.Perfect.IsPerfect K)
    {L L' : DerivedCategory (ModuleCat.{u} R)} (g : L ⟶ L') :
    ((Stacks.SheafOfModules.derivedSheafHom (Spec R).sheaf).obj
          (op ((tildeDer R).obj K))).map ((tildeDer R).map g) ≫
        (affinePerfectDerivedSheafHomIso R K L' hK).hom =
      (affinePerfectDerivedSheafHomIso R K L hK).hom ≫
        (tildeDer R).map
          ((StacksDraft.DerivedHom.derivedHomAdjunction (R := R)).hom.map (𝟙 (op K), g))

AlgebraicGeometry.affinePerfectDerivedSheafHomIso_natural_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedTilde/AffineDerivedHom/PerfectSource.lean, line 677. The attribute's comment: “(3)(b) K perfect and L arbitrary”.

Clause (3)(b) is contravariantly natural in the perfect source.

public theorem affinePerfectDerivedSheafHomIso_natural_left (R : CommRingCat.{u})
    {K K' : DerivedCategory (ModuleCat.{u} R)} (f : K' ⟶ K)
    (hK : StacksDraft.Perfect.IsPerfect K)
    (hK' : StacksDraft.Perfect.IsPerfect K')
    (L : DerivedCategory (ModuleCat.{u} R)) :
    ((Stacks.SheafOfModules.derivedSheafHom (Spec R).sheaf).map
          ((tildeDer R).map f).op).app ((tildeDer R).obj L) ≫
        (affinePerfectDerivedSheafHomIso R K' L hK').hom =
      (affinePerfectDerivedSheafHomIso R K L hK).hom ≫
        (tildeDer R).map
          ((StacksDraft.DerivedHom.derivedHomAdjunction (R := R)).hom.map (f.op, 𝟙 L))

AlgebraicGeometry.AffineExt.cohomologySheaf_isSheafification_extPresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedTilde/AffineExtCohomologySheaf.lean, line 71. The attribute's comment: “(4) the n-th cohomology sheaf of RHom(K~, L~) on Spec A is the sheaf of modules associated to the presheaf D(f) ↦ Ext^n_{A_f}(K ⊗ A_f, L ⊗ A_f), through the canonical A_f-linear comparison maps”.

Let A be a commutative ring, let K, L be objects of D(A) and let n be an integer. The n-th cohomology sheaf of R𝓗om(K̃, L̃) on Spec A is the sheaf of 𝒪_{Spec A}-modules associated to the presheaf D(f) ↦ Ext^n_{A_f}(K ⊗_A A_f, L ⊗_A A_f) on the principal opens of Spec A: the canonical maps Ext^n_{A_f}(K ⊗_A A_f, L ⊗_A A_f) ⟶ Γ(D(f), Hⁿ(R𝓗om(K̃, L̃))), one for every f : A, which are A_f-linear (AlgebraicGeometry.AffineExt.extToCohomologySheafLinear), * commute with restriction, the restriction of Ext classes from D(f) to D(g) ⊆ D(f) being derived base change along A_f ⟶ A_g; * are locally surjective: every section of Hⁿ(R𝓗om(K̃, L̃)) over D(f) is, around every point of D(f), the restriction of the image of an Ext class over a smaller principal open; * are locally injective: an Ext class over D(f) with zero image restricts to zero over a principal open around every point of D(f).

Here A_f = Γ(Spec A, D(f)) is the localization of A away from f, which is also the ring of sections of 𝒪_{Spec A} over D(f). The objects K and L are arbitrary.

theorem cohomologySheaf_isSheafification_extPresheaf (R : CommRingCat.{u})
    (K L : DerivedCategory (ModuleCat.{u} R)) (n : ℤ) :
    (∀ (f g : R) (h : basicOpen R g ≤ basicOpen R f) (α : localizedExt R K L f n),
        (cohomologySheaf R K L n).presheaf.map (homOfLE h).op
            (extToCohomologySheafLinear R K L n f α) =
          extToCohomologySheafLinear R K L n g (localizedExtRestrict R K L h n α)) ∧
      (∀ (f : R) (s : Γ(cohomologySheaf R K L n, basicOpen R f)) (x : Spec R),
        x ∈ basicOpen R f → ∃ (g : R) (h : basicOpen R g ≤ basicOpen R f),
          x ∈ basicOpen R g ∧ ∃ α, extToCohomologySheafLinear R K L n g α =
            (cohomologySheaf R K L n).presheaf.map (homOfLE h).op s) ∧
      (∀ (f : R) (α : localizedExt R K L f n), extToCohomologySheafLinear R K L n f α = 0 →
        ∀ x : Spec R, x ∈ basicOpen R f → ∃ (g : R) (h : basicOpen R g ≤ basicOpen R f),
          x ∈ basicOpen R g ∧ localizedExtRestrict R K L h n α = 0)

AlgebraicGeometry.affinePseudoCoherentDerivedSheafHomIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedTilde/AffinePseudoCoherentDerivedHom.lean, line 761. The attribute's comment: “(3)(a) K pseudo-coherent and L bounded below”.

[Stacks, Tag 0A6H] (3)(a). Let R be a commutative ring, X = Spec R, and let K, L be objects of D(R) with K pseudo-coherent and L bounded below. Then the derived internal Hom of the derived sheafifications of K and L is the derived sheafification of the derived Hom RHom_R(K, L):

RSheafHom_{𝒪_X}(K̃, L̃) ≅ (RHom_R(K, L))~.

The comparison is not an arbitrary isomorphism. K is replaced by a bounded-above representative with finite free terms and L by a bounded-below K-injective representative; there the sheaf side is computed by the ordinary internal Hom complex (Stacks 08I5) and the module side by the ordinary Hom complex (Stacks 0A66), and the comparison is the one pinned degreewise by the affine internal-Hom isomorphism of [Stacks, Tag 01I8]. The representatives are definite choices, so the construction is a function of its arguments, and it is natural in both of them (affinePseudoCoherentDerivedSheafHomIso_natural_left and affinePseudoCoherentDerivedSheafHomIso_natural_right). The canonical comparison AlgebraicGeometry.affineDerivedTildeHomComparison in the other direction is an isomorphism under the same hypotheses, isIso_affineDerivedTildeHomComparison_of_isPseudoCoherent.

noncomputable def affinePseudoCoherentDerivedSheafHomIso (R : CommRingCat.{u})
    (K L : DerivedCategory (ModuleCat.{u} R))
    (hK : StacksDraft.PseudoCoherence.IsPseudoCoherent K)
    (hL : (DerivedCategory.TStructure.t).plus L) :
    ((Stacks.SheafOfModules.derivedSheafHom (Spec R).sheaf).obj
        (op ((tilde.functor R).mapDerivedCategory.obj K))).obj
          ((tilde.functor R).mapDerivedCategory.obj L) ≅
      (tilde.functor R).mapDerivedCategory.obj
        ((StacksDraft.DerivedHom.derivedHomAdjunction (R := R)).hom.obj (op K, L))

AlgebraicGeometry.affinePseudoCoherentDerivedSheafHomIso_natural_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedTilde/AffinePseudoCoherentDerivedHom.lean, line 889. The attribute's comment: “(3)(a) K pseudo-coherent and L bounded below”.

[Stacks, Tag 0A6H] (3)(a). The affine comparison is contravariantly natural in the pseudo-coherent argument.

theorem affinePseudoCoherentDerivedSheafHomIso_natural_left (R : CommRingCat.{u})
    {K K' L : DerivedCategory (ModuleCat.{u} R)}
    (hK : StacksDraft.PseudoCoherence.IsPseudoCoherent K)
    (hK' : StacksDraft.PseudoCoherence.IsPseudoCoherent K')
    (hL : (DerivedCategory.TStructure.t).plus L) (f : K' ⟶ K) :
    ((Stacks.SheafOfModules.derivedSheafHom (Spec R).sheaf).map
        ((tilde.functor R).mapDerivedCategory.map f).op).app
          ((tilde.functor R).mapDerivedCategory.obj L) ≫
      (affinePseudoCoherentDerivedSheafHomIso R K' L hK' hL).hom =
    (affinePseudoCoherentDerivedSheafHomIso R K L hK hL).hom ≫
      (tilde.functor R).mapDerivedCategory.map
        ((StacksDraft.DerivedHom.derivedHomAdjunction (R := R)).hom.map
          (f.op, 𝟙 L))

AlgebraicGeometry.affinePseudoCoherentDerivedSheafHomIso_natural_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedTilde/AffinePseudoCoherentDerivedHom.lean, line 914. The attribute's comment: “(3)(a) K pseudo-coherent and L bounded below”.

[Stacks, Tag 0A6H] (3)(a). The affine comparison is covariantly natural in the bounded-below argument.

theorem affinePseudoCoherentDerivedSheafHomIso_natural_right (R : CommRingCat.{u})
    {K L L' : DerivedCategory (ModuleCat.{u} R)}
    (hK : StacksDraft.PseudoCoherence.IsPseudoCoherent K)
    (hL : (DerivedCategory.TStructure.t).plus L)
    (hL' : (DerivedCategory.TStructure.t).plus L') (g : L ⟶ L') :
    ((Stacks.SheafOfModules.derivedSheafHom (Spec R).sheaf).obj
        (op ((tilde.functor R).mapDerivedCategory.obj K))).map
          ((tilde.functor R).mapDerivedCategory.map g) ≫
      (affinePseudoCoherentDerivedSheafHomIso R K L' hK hL').hom =
    (affinePseudoCoherentDerivedSheafHomIso R K L hK hL).hom ≫
      (tilde.functor R).mapDerivedCategory.map
        ((StacksDraft.DerivedHom.derivedHomAdjunction (R := R)).hom.map
          (𝟙 (op K), g))

AlgebraicGeometry.isIso_affineDerivedTildeHomComparison_of_isPseudoCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedTilde/AffinePseudoCoherentDerivedHom.lean, line 995. The attribute's comment: “(3)(a) K pseudo-coherent and L bounded below: the canonical comparison is an isomorphism”.

[Stacks, Tag 0A6H] (3)(a), for the canonical comparison. Let R be a commutative ring, X = Spec R, and let K, L be objects of D(R) with K pseudo-coherent and L bounded below. Then the canonical comparison

(RHom_R(K, L))~ ⟶ R𝓗om_{𝒪_X}(K̃, L̃)

of AlgebraicGeometry.affineDerivedTildeHomComparison is an isomorphism.

theorem isIso_affineDerivedTildeHomComparison_of_isPseudoCoherent (R : CommRingCat.{u})
    (K L : DerivedCategory (ModuleCat.{u} R))
    (hK : StacksDraft.PseudoCoherence.IsPseudoCoherent K)
    (hL : (DerivedCategory.TStructure.t).plus L) :
    IsIso (affineDerivedTildeHomComparison R K L)

AlgebraicGeometry.derivedCategoryB_derivedSheafHom_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedTilde/SchemeSheafPerfectHomQuasicoherent.lean, line 125. The attribute's comment: “part (2) on an arbitrary scheme: the derived internal Hom out of a perfect object into an object of D_QCoh has quasi-coherent cohomology sheaves”.

Stacks Project, Tag 0A6H, part (2). Let Y be a scheme, let E be a perfect object of D(𝒪_Y) and let F be an object of D_QCoh(𝒪_Y). Then the derived internal Hom R𝓗om_{𝒪_Y}(E, F) lies in D_QCoh(𝒪_Y): all of its cohomology sheaves are quasi-coherent.

The affine opens of Y cover it, so by the locality of quasi-coherence it is enough to see that each cohomology sheaf restricts to a quasi-coherent module on every affine open U. Restriction along U.ι commutes with the derived internal Hom by [Stacks, Tag 08DL], keeps E perfect by [Stacks, Tag 09UA] and keeps F in D_QCoh, so the restriction is the derived internal Hom of the restrictions on the affine scheme U, where derivedCategoryB_derivedSheafHom_of_isPerfect_of_isAffine applies.

theorem derivedCategoryB_derivedSheafHom_of_isPerfect (Y : Scheme.{u})
    (E F : DerivedCategory (StructureSheafModules Y.sheaf))
    (hE : RingedSpace.IsPerfect (X := Y.toRingedSpace) E)
    (hF : DerivedCategoryB.derivedCategoryB
      (SheafOfModules.isQuasicoherent Y.ringCatSheaf) F) :
    DerivedCategoryB.derivedCategoryB (SheafOfModules.isQuasicoherent Y.ringCatSheaf)
      (((Stacks.SheafOfModules.derivedSheafHom Y.sheaf).obj (op E)).obj F)

AlgebraicGeometry.isLocallyBoundedBelow_derivedSheafHom_of_isPseudoCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedTilde/SchemeSheafPseudoCoherentHomLocallyBounded.lean, line 95. The attribute's comment: “part (1) on an arbitrary scheme: the derived internal Hom out of a pseudo-coherent object into an object of D⁺_QCoh is locally bounded below”.

Let Y be a scheme, let E be a pseudo-coherent object of D(𝒪_Y) and let F be an object of D⁺_QCoh(𝒪_Y). Then R𝓗om_{𝒪_Y}(E, F) is locally bounded below: every point of Y has an open neighbourhood over which the cohomology sheaves vanish in all sufficiently negative degrees.

theorem isLocallyBoundedBelow_derivedSheafHom_of_isPseudoCoherent (Y : Scheme.{u})
    (E F : DerivedCategory (StructureSheafModules Y.sheaf))
    (hE : RingedSpace.IsPseudoCoherent (X := Y.toRingedSpace) E)
    (hF : DerivedCategoryB.derivedCategoryBPlus
      (SheafOfModules.isQuasicoherent Y.ringCatSheaf) F) :
    RingedSpace.IsLocallyBoundedBelow Y.toRingedSpace
      (((Stacks.SheafOfModules.derivedSheafHom Y.sheaf).obj (op E)).obj F)

AlgebraicGeometry.derivedCategoryB_derivedSheafHom_of_isPseudoCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedTilde/SchemeSheafPseudoCoherentHomQuasicoherent.lean, line 168. The attribute's comment: “part (1) on an arbitrary scheme: the derived internal Hom out of a pseudo-coherent object into an object of D⁺_QCoh has quasi-coherent cohomology sheaves”.

Stacks Project, Tag 0A6H, part (1). Let Y be a scheme, let E be a pseudo-coherent object of D(𝒪_Y) and let F be an object of D⁺_QCoh(𝒪_Y). Then the derived internal Hom R𝓗om_{𝒪_Y}(E, F) lies in D_QCoh(𝒪_Y): all of its cohomology sheaves are quasi-coherent.

The affine opens of Y cover it, so by the locality of quasi-coherence it is enough to see that each cohomology sheaf restricts to a quasi-coherent module on every affine open U. Restriction along U.ι commutes with the derived internal Hom by [Stacks, Tag 08DL], keeps E pseudo-coherent by [Stacks, Tag 08CC] and keeps F in D⁺_QCoh, so the restriction is the derived internal Hom of the restrictions on the affine scheme U, where derivedCategoryB_derivedSheafHom_of_isPseudoCoherent_of_isAffine applies.

theorem derivedCategoryB_derivedSheafHom_of_isPseudoCoherent (Y : Scheme.{u})
    (E F : DerivedCategory (StructureSheafModules Y.sheaf))
    (hE : RingedSpace.IsPseudoCoherent (X := Y.toRingedSpace) E)
    (hF : DerivedCategoryB.derivedCategoryBPlus
      (SheafOfModules.isQuasicoherent Y.ringCatSheaf) F) :
    DerivedCategoryB.derivedCategoryB (SheafOfModules.isQuasicoherent Y.ringCatSheaf)
      (((Stacks.SheafOfModules.derivedSheafHom Y.sheaf).obj (op E)).obj F)

AlgebraicGeometry.derivedCategoryBPlus_derivedSheafHom_of_isPseudoCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/FinitePushforwardDerivedSheafHom.lean, line 75. The attribute's comment: “part (1) with the lower bound, on an arbitrary scheme, for a cohomologically bounded-above pseudo-coherent first argument”.

Let Z be a scheme, let E be an object of D(𝒪_Z) which is pseudo-coherent and cohomologically bounded above, and let F lie in D⁺_QCoh(𝒪_Z). Then R𝓗om_{𝒪_Z}(E, F) lies in D⁺_QCoh(𝒪_Z).

theorem derivedCategoryBPlus_derivedSheafHom_of_isPseudoCoherent (Z : Scheme.{u})
    (E F : DerivedCategory (StructureSheafModules Z.sheaf))
    (hE : RingedSpace.IsPseudoCoherent (X := Z.toRingedSpace) E)
    (hE' : DerivedCategoryB.IsBoundedAbove E)
    (hF : DerivedCategoryB.derivedCategoryBPlus
      (SheafOfModules.isQuasicoherent Z.ringCatSheaf) F) :
    DerivedCategoryB.derivedCategoryBPlus (SheafOfModules.isQuasicoherent Z.ringCatSheaf)
      (((Stacks.SheafOfModules.derivedSheafHom Z.sheaf).obj (op E)).obj F)

Tag 0ATN, a lemma

Tag 0ATN in the Stacks Project.

AlgebraicGeometry.RingedSite.isIso_derivedTensorHomDiagonal_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedTensorHomDiagonalPerfect.lean, line 333. The attribute's comment: “part (1)”.

Stacks 0ATN part (1): the diagonal of Stacks 0BYS is an isomorphism at a perfect source. For objects K, L, M of D(O) with M perfect,

K ⊗^L_O RSheafHom(M, L) ⟶ RSheafHom(M, K ⊗^L_O L)

is an isomorphism.

The only hypothesis is X.IsPerfect M, the site-level notion of Stacks 08G5: there is a complex N representing M and a covering of the site on each member of which the restriction of N receives a quasi-isomorphism from a strictly perfect complex. Nothing is assumed of K or L.

The instances in the ambient variable block are setup, not hypotheses on the lemma: a ringed site whose slices admit sheafification and on which the tensor product of sheaves of modules is additive and totalisable is what it takes for the objects in the statement — the derived tensor product, the derived internal Hom, and their restrictions to the slices appearing in the definition of perfection — to exist at all. A class needed only by the proof would have been an extra hypothesis, and there is none.

theorem isIso_derivedTensorHomDiagonal_of_isPerfect
    (K L M : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (hM : X.IsPerfect M) :
    IsIso (derivedTensorHomDiagonal X K L M)

AlgebraicGeometry.RingedSite.isIso_derivedTensorHomDiagonal_of_isPerfect_tensorFactor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedTensorHomDiagonalPerfectTensorFactor.lean, line 227. The attribute's comment: “part (2)”.

Stacks 0ATN part (2): the diagonal of Stacks 0BYS is an isomorphism at a perfect tensor factor. For objects K, L, M of D(O) with K perfect,

K ⊗^L_O RSheafHom(M, L) ⟶ RSheafHom(M, K ⊗^L_O L)

is an isomorphism.

The only hypothesis is X.IsPerfect K, the site-level notion of Stacks 08G5: there is a complex A₀ representing K and a covering of the site on each member of which the restriction of A₀ receives a quasi-isomorphism from a strictly perfect complex. Nothing is assumed of L or M. This is the same notion, with the same slack, that part (1) assumes of M.

The instances in the ambient variable block are setup, not hypotheses on the lemma, exactly as for part (1): a ringed site whose slices admit sheafification and on which the tensor product of sheaves of modules is additive and totalisable is what it takes for the objects named in the statement to exist. A class needed only by the proof would have been an extra hypothesis, and there is none.

The K-flat resolution is taken of A₀ itself rather than of the chosen K-flat model of K, so that the comparison between the criterion's model and the complex the covering resolves is a quasi-isomorphism of complexes and the slice-level input can be assembled from chain maps.

theorem isIso_derivedTensorHomDiagonal_of_isPerfect_tensorFactor
    (K L M : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (hK : X.IsPerfect K) :
    IsIso (derivedTensorHomDiagonal X K L M)

AlgebraicGeometry.RingedSite.isIso_derivedTensorHomDiagonal_of_isPseudoCoherent_of_hasTorAmplitudeGE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedTensorHomDiagonalPseudoCoherent.lean, line 396. The attribute's comment: “part (3), with the tensor factor of Tor amplitude in [a, ∞) rather than of finite Tor dimension”.

The diagonal of Stacks 0BYS is an isomorphism at a pseudo-coherent source, a cohomologically bounded-below target and a tensor factor of Tor amplitude in [a, ∞). For objects K, L, M of D(O) with M pseudo-coherent, the cohomology of L vanishing in degrees ≪ 0 and K of Tor amplitude in [a, ∞),

K ⊗^L_O RSheafHom(M, L) ⟶ RSheafHom(M, K ⊗^L_O L)

is an isomorphism.

Pseudo-coherence is AlgebraicGeometry.RingedSite.IsPseudoCoherent, Tor amplitude in [a, ∞) is Stacks.SheafOfModules.DerivedTensorProduct.HasTorAmplitudeGE for the canonical derived tensor product, and boundedness below is vanishing of the cohomology sheaves in degrees ≪ 0.

public theorem isIso_derivedTensorHomDiagonal_of_isPseudoCoherent_of_hasTorAmplitudeGE
    (K L M : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (a : ℤ)
    (hM : X.IsPseudoCoherent M)
    (hL : DerivedCategoryB.IsBoundedBelow L)
    (hK : Stacks.SheafOfModules.DerivedTensorProduct.HasTorAmplitudeGE
      (Stacks.SheafOfModules.canonicalDerivedTensorProduct X) K a) :
    IsIso (derivedTensorHomDiagonal X K L M)

AlgebraicGeometry.RingedSite.isIso_derivedTensorHomDiagonal_of_isPseudoCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedTensorHomDiagonalPseudoCoherent.lean, line 468. The attribute's comment: “part (3)”.

Stacks 0ATN part (3): the diagonal of Stacks 0BYS is an isomorphism at a pseudo-coherent source, a cohomologically bounded-below target and a tensor factor of finite Tor dimension. For objects K, L, M of D(O) with M pseudo-coherent, the cohomology of L vanishing in degrees ≪ 0 and K of finite Tor dimension,

K ⊗^L_O RSheafHom(M, L) ⟶ RSheafHom(M, K ⊗^L_O L)

is an isomorphism.

The three hypotheses are the site-level notions: pseudo-coherence is AlgebraicGeometry.RingedSite.IsPseudoCoherent of Stacks 08FT, finite Tor dimension is Stacks.SheafOfModules.DerivedTensorProduct.HasFiniteTorDimension of Stacks 08FZ for the canonical derived tensor product, and boundedness below is vanishing of the cohomology sheaves in degrees ≪ 0.

public theorem isIso_derivedTensorHomDiagonal_of_isPseudoCoherent
    (K L M : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (hM : X.IsPseudoCoherent M)
    (hL : DerivedCategoryB.IsBoundedBelow L)
    (hK : Stacks.SheafOfModules.DerivedTensorProduct.HasFiniteTorDimension
      (Stacks.SheafOfModules.canonicalDerivedTensorProduct X) K) :
    IsIso (derivedTensorHomDiagonal X K L M)

Sources

• Section 36.10, Tag 08E4
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.isQuasicoherent_homology_of_isPseudoCoherentFrom · AlgebraicGeometry.exists_local_epi_homology_of_isPseudoCoherentFrom · AlgebraicGeometry.isQuasicoherentDerived_of_isPseudoCoherent · AlgebraicGeometry.RingedSpace.isPseudoCoherentFrom_tilde_iff · AlgebraicGeometry.RingedSpace.isPseudoCoherent_tilde_iff · AlgebraicGeometry.RingedSpace.isPseudoCoherentFrom_tilde_iff_locallySmall · AlgebraicGeometry.RingedSpace.isPseudoCoherent_tilde_iff_locallySmall · Stacks.AffineTilde.isPseudoCoherentFrom_of_isPseudoCoherentFrom_tildeComplex

Section36.11 Derived category of coherent modules#

Section 36.11 of the Stacks Project, Tag 08E0. 9 tags here are carried by 23 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 08E1, an equation

Tag 08E1 in the Stacks Project.

Stacks.SheafOfModules.coherentDerivedComparison_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/CoherentDerivedCategory.lean, line 78. The attribute's comment: “well-definedness”.

Stacks Project, Tag 08E1. The derived inclusion of coherent modules has coherent cohomology in every degree.

theorem coherentDerivedComparison_mem
    {X : Type u} [TopologicalSpace X]
    (R : Sheaf (Opens.grothendieckTopology X) RingCat.{u}) :
    let P : ObjectProperty (_root_.SheafOfModules.{u} R) := fun M => IsCoherent M
    letI : Preadditive P.FullSubcategory := Abelian.toPreadditive
    letI : Preadditive (_root_.SheafOfModules.{u} R) := Abelian.toPreadditive
    let I : P.FullSubcategory ⥤ _root_.SheafOfModules.{u} R := P.ι
    letI : PreservesFiniteLimits I :=
      ObjectProperty.preservesFiniteLimits_ι_of_isWeakSerreClass P
    letI : PreservesFiniteColimits I :=
      ObjectProperty.preservesFiniteColimits_ι_of_isWeakSerreClass P
    letI : I.Additive := I.additive_of_preserves_binary_products
    ∀ K : DerivedCategory (CoherentModules R),
      (DerivedCategoryB.derivedCategoryB P) (I.mapDerivedCategory.obj K)

Stacks.SheafOfModules.coherentDerivedComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/CoherentDerivedCategory.lean, line 111. The attribute's comment: “comparison functor”.

Stacks Project, Tag 08E1. The canonical functor from the derived category of coherent modules to the subcategory of the derived category with coherent cohomology.

noncomputable def coherentDerivedComparison
    {X : Type u} [TopologicalSpace X]
    (R : Sheaf (Opens.grothendieckTopology X) RingCat.{u}) :
    DerivedCategory (CoherentModules R) ⥤
      (DerivedCategoryB.derivedCategoryB
        (fun M : _root_.SheafOfModules.{u} R => IsCoherent M)).FullSubcategory

Stacks.SheafOfModules.coherentDerivedComparison_comp_inclusion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/CoherentDerivedCategory.lean, line 132. The attribute's comment: “canonical comparison”.

Stacks Project, Tag 08E1. Forgetting the coherence condition after comparison gives the derived functor of the inclusion of coherent modules.

noncomputable def coherentDerivedComparison_comp_inclusion
    {X : Type u} [TopologicalSpace X]
    (R : Sheaf (Opens.grothendieckTopology X) RingCat.{u}) :
    let P : ObjectProperty (_root_.SheafOfModules.{u} R) := fun M => IsCoherent M
    letI : Preadditive P.FullSubcategory := Abelian.toPreadditive
    letI : Preadditive (_root_.SheafOfModules.{u} R) := Abelian.toPreadditive
    let I : P.FullSubcategory ⥤ _root_.SheafOfModules.{u} R := P.ι
    letI : PreservesFiniteLimits I :=
      ObjectProperty.preservesFiniteLimits_ι_of_isWeakSerreClass P
    letI : PreservesFiniteColimits I :=
      ObjectProperty.preservesFiniteColimits_ι_of_isWeakSerreClass P
    letI : I.Additive := I.additive_of_preserves_binary_products
    coherentDerivedComparison R ⋙ (DerivedCategoryB.derivedCategoryB P).ι ≅
      I.mapDerivedCategory

Tag 0FDA, a lemma

Tag 0FDA in the Stacks Project.

AlgebraicGeometry.coherentToQuasicoherentDerivedMinus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedCoherent/Basic.lean, line 249.

Stacks Project, Tag 0FDA. The canonical functor D⁻(Coh(𝒪_X)) ⥤ D⁻_Coh(QCoh(𝒪_X)) on a Noetherian scheme: the derived functor of the inclusion Coh(𝒪_X) ⥤ QCoh(𝒪_X), restricted to the bounded above complexes and corestricted to the bounded above complexes with coherent cohomology, where it lands.

def coherentToQuasicoherentDerivedMinus [IsNoetherian X] :
    DerivedCategory.Minus (SheafOfModules.CoherentModules X.ringCatSheaf) ⥤
      (DerivedCategoryB.derivedCategoryBMinus (coherentInQuasicoherent X)).FullSubcategory

AlgebraicGeometry.coherentToQuasicoherentDerivedMinus_isEquivalence, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedCoherent/Basic.lean, line 293. References: SGA 6 II (2.2.2).

Stacks Project, Tag 0FDA. On a Noetherian scheme the canonical functor D⁻(Coh(𝒪_X)) ⥤ D⁻_Coh(QCoh(𝒪_X)) is an equivalence: the bounded above derived category of coherent modules is the full subcategory of the bounded above derived category of quasi-coherent modules whose objects have coherent cohomology.

instance coherentToQuasicoherentDerivedMinus_isEquivalence [IsNoetherian X] :
    (coherentToQuasicoherentDerivedMinus X).IsEquivalence

Tag 0FDB, a proposition

Tag 0FDB in the Stacks Project.

AlgebraicGeometry.coherentToModulesDerivedMinus_isEquivalence, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedCoherent/Modules.lean, line 306. The attribute's comment: “bounded above”. References: SGA 6 II (2.2.2.1), “more general”.

Stacks Project, Tag 0FDB. On a Noetherian scheme the canonical functor D⁻(Coh(𝒪_X)) ⥤ D⁻_Coh(𝒪_X) is an equivalence: the bounded above derived category of the coherent 𝒪_X-modules is the full subcategory of D(𝒪_X) of the complexes which are cohomologically bounded above with coherent cohomology sheaves.

instance coherentToModulesDerivedMinus_isEquivalence [IsNoetherian X] :
    (coherentToModulesDerivedMinus X).IsEquivalence

AlgebraicGeometry.coherentToModulesDerivedBounded_isEquivalence, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedCoherent/Modules.lean, line 418. The attribute's comment: “bounded”. References: SGA 6 II (2.2.2.1).

Stacks Project, Tag 0FDB. On a Noetherian scheme the canonical functor D^b(Coh(𝒪_X)) ⥤ D^b_Coh(𝒪_X) is an equivalence: the bounded derived category of the coherent 𝒪_X-modules is the full subcategory of D(𝒪_X) of the complexes which are cohomologically bounded with coherent cohomology sheaves.

instance coherentToModulesDerivedBounded_isEquivalence [IsNoetherian X] :
    (coherentToModulesDerivedBounded X).IsEquivalence

Tag 08E2, a lemma

Tag 08E2 in the Stacks Project.

Stacks.AlgebraicGeometry.ProperSupportCoherent.derivedCategoryBBounded_derivedPushforward_of_isProperOver_supp_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProperSupportCoherent/DerivedDirectImageSupplement.lean, line 80. References: EGA II (7.3.12), “special case”; EGA III (6.2.5), “special case”; SGA 6 III (2.2.1), “special case”; SGA 6 XIV (2.3), “special case”.

[Stacks, Tag 08E2]. Let S be a Noetherian scheme, f : X ⟶ S locally of finite type and E a bounded object of D(𝒪_X) whose cohomology sheaves are coherent with support proper over S. Then Rf_*E is an object of D^b_Coh(𝒪_S).

The dévissage is applied to the window [a, b] of E; at each cohomology sheaf of E its hypothesis is hasCoherentBoundedDirectImages_of_isProperOver_supp_unconditional, this library's form of [Stacks, Tag 08DS] together with the uniform vanishing of [Stacks, Tag 01XJ].

theorem derivedCategoryBBounded_derivedPushforward_of_isProperOver_supp_unconditional
    [IsNoetherian S] [LocallyOfFiniteType f] (E : DerivedCategory X.Modules)
    (hcoh : ∀ j : ℤ, ((DerivedCategory.homologyFunctor X.Modules j).obj E).IsCoherent)
    (hsupp : ∀ j : ℤ, IsProperOver f
      ⟨SheafOfModules.supp ((DerivedCategory.homologyFunctor X.Modules j).obj E),
        @SheafOfModules.isClosed_supp _ _ _ (hcoh j).isFiniteType⟩)
    (a b : ℤ) (hGE : E.IsGE a) (hLE : E.IsLE b) :
    DerivedCategoryB.derivedCategoryBBounded (fun N : S.Modules => N.IsCoherent)
      ((derivedPushforwardModules f).obj E)

Stacks.AlgebraicGeometry.ProperSupportCoherent.derivedCategoryBBounded_derivedPushforward_of_properSupp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProperSupportCoherent/DerivedDirectImageUnconditional.lean, line 76. References: EGA III (3.2.1), “Noetherian target”; EGA III (3.2.4), “special case”; EGA III (4.1.10), “more general”; SGA 6 0 (3.1), “partial”; SGA 6 III (2.2.1), “special case”.

[Stacks, Tag 08E2]. Let S be a Noetherian scheme, let f : X ⟶ S be locally of finite type and let E be a bounded object of D(𝒪_X) whose cohomology sheaves are coherent with support proper over S. Then Rf_*E is an object of D^b_Coh(𝒪_S).

The dévissage derivedCategoryBBounded_derivedPushforward_of_isProperOver_supp asks for [Stacks, Tag 02O5] in the affine-base form AlgebraicGeometry.ProperCoherentImage.HigherDirectImageIsCoherentOverAffineBase, which AlgebraicGeometry.ProperCoherenceWitness.higherDirectImageIsCoherentOverAffineBase supplies.

theorem derivedCategoryBBounded_derivedPushforward_of_properSupp {X S : Scheme.{u}} (f : X ⟶ S)
    [IsNoetherian S] [LocallyOfFiniteType f] (E : DerivedCategory X.Modules)
    (hcoh : ∀ j : ℤ, ((DerivedCategory.homologyFunctor X.Modules j).obj E).IsCoherent)
    (hsupp : ∀ j : ℤ, IsProperOver f
      ⟨SheafOfModules.supp ((DerivedCategory.homologyFunctor X.Modules j).obj E),
        @SheafOfModules.isClosed_supp _ _ _ (hcoh j).isFiniteType⟩)
    (a b : ℤ) (hGE : E.IsGE a) (hLE : E.IsLE b) :
    DerivedCategoryB.derivedCategoryBBounded (fun N : S.Modules => N.IsCoherent)
      ((derivedPushforwardModules f).obj E)

Stacks.AlgebraicGeometry.ProperSupportCoherent.derivedCategoryBBounded_derivedPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProperSupportCoherent/UnconditionalBounded.lean, line 39.

[Stacks, Tag 08E2]. Let S be a Noetherian scheme, f : X ⟶ S locally of finite type and E an object of D^b_Coh(𝒪_X) such that the support of H^i(E) is proper over S for all i. Then Rf_*E is an object of D^b_Coh(𝒪_S).

theorem derivedCategoryBBounded_derivedPushforward [IsNoetherian S]
    (E : DerivedCategory X.Modules)
    (hcoh : ∀ j : ℤ, ((DerivedCategory.homologyFunctor X.Modules j).obj E).IsCoherent)
    (hsupp : ∀ j : ℤ, IsProperOver f
      ⟨SheafOfModules.supp ((DerivedCategory.homologyFunctor X.Modules j).obj E),
        @SheafOfModules.isClosed_supp _ _ _ (hcoh j).isFiniteType⟩)
    (a b : ℤ) (hGE : E.IsGE a) (hLE : E.IsLE b) :
    DerivedCategoryB.derivedCategoryBBounded (fun N : S.Modules => N.IsCoherent)
      ((derivedPushforwardModules f).obj E)

Tag 0D0B, a lemma

Tag 0D0B in the Stacks Project.

Stacks.AlgebraicGeometry.ProperSupportCoherent.derivedCategoryBPlus_derivedPushforward_of_properSupp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProperSupportCoherent/BoundedBelowUnconditional.lean, line 96. References: EGA III (3.2.1), “Noetherian target”; EGA III (3.2.4), “special case”; EGA III (4.1.10), “more general”.

[Stacks, Tag 0D0B]. Let S be a Noetherian scheme, let f : X ⟶ S be a morphism of schemes which is locally of finite type and let E be an object of D^+_Coh(𝒪_X) such that the support of H^i(E) is proper over S for all i. Then Rf_*E is an object of D^+_Coh(𝒪_S).

This is derivedCategoryBPlus_derivedPushforward_of_isProperOver_supp with its appeal to [Stacks, Tag 02O5] supplied by AlgebraicGeometry.ProperCoherenceWitness.higherDirectImageIsCoherentOverAffineBase, a theorem.

theorem derivedCategoryBPlus_derivedPushforward_of_properSupp [IsNoetherian S]
    [LocallyOfFiniteType f] (E : DerivedCategory X.Modules)
    (hE : DerivedCategoryB.derivedCategoryBPlus (fun M : X.Modules => M.IsCoherent) E)
    (hsupp : ∀ j : ℤ, IsProperOver f
      ⟨SheafOfModules.supp ((DerivedCategory.homologyFunctor X.Modules j).obj E),
        @SheafOfModules.isClosed_supp _ _ _ (hE.2 j).isFiniteType⟩) :
    DerivedCategoryB.derivedCategoryBPlus (fun N : S.Modules => N.IsCoherent)
      ((derivedPushforwardModules f).obj E)

Tag 0D0C, a lemma

Tag 0D0C in the Stacks Project.

AlgebraicGeometry.derivedCategoryBPlus_coherent_affineDerivedSheafHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedTilde/AffineCoherentDerivedHom.lean, line 240. The attribute's comment: “the coherence clause on Spec R, for sheafified D⁻_Coh and D⁺_Coh arguments”.

The coherence clause of [Stacks, Tag 0D0C] on an affine scheme. Let R be a Noetherian ring, let K be an object of D⁻_Coh(R) and L an object of D⁺_Coh(R). Then R𝓗om_{𝒪_{Spec R}}(K̃, L̃) lies in D⁺_Coh(𝒪_{Spec R}): it is cohomologically bounded below and all of its cohomology sheaves are coherent.

Boundedness below is Stacks.SheafOfModules.isBoundedBelow_derivedSheafHom, the clause of the tag the library already carries, applied after transporting the bounds of K and L to their sheafifications. Coherence is isCoherent_homology_affineDerivedSheafHom.

The hypotheses are on the module-level objects K and L; the source states the tag for objects of D⁻_Coh(𝒪_X) and D⁺_Coh(𝒪_X) on an arbitrary locally Noetherian X, and neither the reduction to an affine open nor the identification of a sheaf-level coherent complex with a sheafification ([Stacks, Tag 06Z0]) is carried out here; see the module documentation.

theorem derivedCategoryBPlus_coherent_affineDerivedSheafHom [IsNoetherianRing R]
    (K L : DerivedCategory (ModuleCat.{u} R))
    (hK : DerivedCategoryB.derivedCategoryBMinus
      (fun M : ModuleCat.{u} R => Module.Finite R M) K)
    (hL : DerivedCategoryB.derivedCategoryBPlus
      (fun M : ModuleCat.{u} R => Module.Finite R M) L) :
    DerivedCategoryB.derivedCategoryBPlus (A := (Spec R).Modules)
      (Stacks.SheafOfModules.coherentModules (Spec R).ringCatSheaf)
      (((Stacks.SheafOfModules.derivedSheafHom (Spec R).sheaf).obj
          (op ((tilde.functor R).mapDerivedCategory.obj K))).obj
            ((tilde.functor R).mapDerivedCategory.obj L))

AlgebraicGeometry.derivedCategoryBPlus_isCoherent_derivedSheafHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedTilde/SchemeCoherentDerivedHom.lean, line 336.

Stacks Project, Tag 0D0C. Let X be a locally Noetherian scheme, K an object of D⁻_Coh(𝒪_X) and L an object of D⁺_Coh(𝒪_X). Then R𝓗om_{𝒪_X}(K, L) lies in D⁺_Coh(𝒪_X).

Boundedness below is Stacks.SheafOfModules.isBoundedBelow_derivedSheafHom, which needs only the two cohomological bounds; coherence of the cohomology sheaves is isCoherent_homology_derivedSheafHom.

theorem derivedCategoryBPlus_isCoherent_derivedSheafHom (Y : Scheme.{u})
    [IsLocallyNoetherian Y] (E F : DerivedCategory Y.Modules)
    (hE : DerivedCategoryB.derivedCategoryBMinus
      (Stacks.SheafOfModules.coherentModules Y.ringCatSheaf) E)
    (hF : DerivedCategoryB.derivedCategoryBPlus
      (Stacks.SheafOfModules.coherentModules Y.ringCatSheaf) F) :
    DerivedCategoryB.derivedCategoryBPlus
      (Stacks.SheafOfModules.coherentModules Y.ringCatSheaf)
      (((Stacks.SheafOfModules.derivedSheafHom Y.sheaf).obj (op E)).obj F)

Stacks.SheafOfModules.isBoundedBelow_derivedSheafHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedBoundedBelow.lean, line 120. The attribute's comment: “the boundedness clause, on an arbitrary ringed space and with no coherence or Noetherian hypothesis; the coherence clause is not carried”.

The derived internal Hom of a bounded-above complex into a bounded-below complex is cohomologically bounded below. If K is bounded above and L is bounded below, then RSheafHom(K, L) is bounded below, on an arbitrary ringed space.

public theorem isBoundedBelow_derivedSheafHom
    (K L : DerivedCategory (StructureSheafModules Rc))
    (hK : DerivedCategoryB.IsBoundedAbove K) (hL : DerivedCategoryB.IsBoundedBelow L) :
    DerivedCategoryB.IsBoundedBelow (((derivedSheafHom Rc).obj (op K)).obj L)

Tag 0FXU, a lemma

Tag 0FXU in the Stacks Project.

Stacks.AlgebraicGeometry.PerfectCohomology.isBoundedCoherent_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/PseudoCoherentComplex/PerfectBoundedCoherent.lean, line 47. The attribute's comment: “perfect_bounded_coherent”.

A perfect derived object on a Noetherian scheme has bounded coherent cohomology.

theorem isBoundedCoherent_of_isPerfect
    (X : Scheme.{u}) [IsNoetherian X]
    [HasDerivedCategory.{d} (StrictlyPerfect.OXMod.{u, u} X.toRingedSpace)]
    (K : DerivedCategory (StrictlyPerfect.OXMod.{u, u} X.toRingedSpace))
    (hK : RingedSpace.IsPerfect (X := X.toRingedSpace) K) :
    DerivedCategoryB.derivedCategoryBBounded
      (fun M : StrictlyPerfect.OXMod.{u, u} X.toRingedSpace => M.IsCoherent) K

Stacks.AlgebraicGeometry.PerfectCohomology.derivedCategoryB_coherent_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/PseudoCoherentComplex/PerfectTensorInternalHom.lean, line 337. The attribute's comment: “part (2): for L in D_Coh(𝒪_X) both E ⊗^𝐋 L and R𝓗om(E, L) are in D_Coh(𝒪_X)”.

[Stacks, Tag 0FXU], part (2). Let X be a Noetherian scheme and let E in D(𝒪_X) be perfect. If L is in D_Coh(𝒪_X) then E ⊗^𝐋_{𝒪_X} L and R𝓗om_{𝒪_X}(E, L) are in D_Coh(𝒪_X).

theorem derivedCategoryB_coherent_of_isPerfect [IsNoetherian X]
    (E L : DerivedCategory (StrictlyPerfect.OXMod.{u, u} X.toRingedSpace))
    (hE : RingedSpace.IsPerfect (X := X.toRingedSpace) E)
    (hL : DerivedCategoryB.derivedCategoryB
      (fun M : StrictlyPerfect.OXMod.{u, u} X.toRingedSpace => M.IsCoherent) L) :
    DerivedCategoryB.derivedCategoryB
        (fun M : StrictlyPerfect.OXMod.{u, u} X.toRingedSpace => M.IsCoherent)
        (derivedTensorObj X E L) ∧
      DerivedCategoryB.derivedCategoryB
        (fun M : StrictlyPerfect.OXMod.{u, u} X.toRingedSpace => M.IsCoherent)
        (derivedSheafHomObj X E L)

Stacks.AlgebraicGeometry.PerfectCohomology.derivedCategoryBBounded_coherent_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/PseudoCoherentComplex/PerfectTensorInternalHom.lean, line 356. The attribute's comment: “part (3): for L in D^b_Coh(𝒪_X) both E ⊗^𝐋 L and R𝓗om(E, L) are in D^b_Coh(𝒪_X)”.

[Stacks, Tag 0FXU], part (3). Let X be a Noetherian scheme and let E in D(𝒪_X) be perfect. If L is in D^b_Coh(𝒪_X) then E ⊗^𝐋_{𝒪_X} L and R𝓗om_{𝒪_X}(E, L) are in D^b_Coh(𝒪_X).

theorem derivedCategoryBBounded_coherent_of_isPerfect [IsNoetherian X]
    (E L : DerivedCategory (StrictlyPerfect.OXMod.{u, u} X.toRingedSpace))
    (hE : RingedSpace.IsPerfect (X := X.toRingedSpace) E)
    (hL : DerivedCategoryB.derivedCategoryBBounded
      (fun M : StrictlyPerfect.OXMod.{u, u} X.toRingedSpace => M.IsCoherent) L) :
    DerivedCategoryB.derivedCategoryBBounded
        (fun M : StrictlyPerfect.OXMod.{u, u} X.toRingedSpace => M.IsCoherent)
        (derivedTensorObj X E L) ∧
      DerivedCategoryB.derivedCategoryBBounded
        (fun M : StrictlyPerfect.OXMod.{u, u} X.toRingedSpace => M.IsCoherent)
        (derivedSheafHomObj X E L)

Stacks.AlgebraicGeometry.PerfectCohomology.derivedCategoryBPlus_coherent_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/PseudoCoherentComplex/PerfectTensorInternalHom.lean, line 379. The attribute's comment: “part (4): for L in D^+_Coh(𝒪_X) both E ⊗^𝐋 L and R𝓗om(E, L) are in D^+_Coh(𝒪_X)”.

[Stacks, Tag 0FXU], part (4). Let X be a Noetherian scheme and let E in D(𝒪_X) be perfect. If L is in D^+_Coh(𝒪_X) then E ⊗^𝐋_{𝒪_X} L and R𝓗om_{𝒪_X}(E, L) are in D^+_Coh(𝒪_X).

theorem derivedCategoryBPlus_coherent_of_isPerfect [IsNoetherian X]
    (E L : DerivedCategory (StrictlyPerfect.OXMod.{u, u} X.toRingedSpace))
    (hE : RingedSpace.IsPerfect (X := X.toRingedSpace) E)
    (hL : DerivedCategoryB.derivedCategoryBPlus
      (fun M : StrictlyPerfect.OXMod.{u, u} X.toRingedSpace => M.IsCoherent) L) :
    DerivedCategoryB.derivedCategoryBPlus
        (fun M : StrictlyPerfect.OXMod.{u, u} X.toRingedSpace => M.IsCoherent)
        (derivedTensorObj X E L) ∧
      DerivedCategoryB.derivedCategoryBPlus
        (fun M : StrictlyPerfect.OXMod.{u, u} X.toRingedSpace => M.IsCoherent)
        (derivedSheafHomObj X E L)

Stacks.AlgebraicGeometry.PerfectCohomology.derivedCategoryBMinus_coherent_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/PseudoCoherentComplex/PerfectTensorInternalHom.lean, line 400. The attribute's comment: “part (5): for L in D^-_Coh(𝒪_X) both E ⊗^𝐋 L and R𝓗om(E, L) are in D^-_Coh(𝒪_X)”.

[Stacks, Tag 0FXU], part (5). Let X be a Noetherian scheme and let E in D(𝒪_X) be perfect. If L is in D^-_Coh(𝒪_X) then E ⊗^𝐋_{𝒪_X} L and R𝓗om_{𝒪_X}(E, L) are in D^-_Coh(𝒪_X).

theorem derivedCategoryBMinus_coherent_of_isPerfect [IsNoetherian X]
    (E L : DerivedCategory (StrictlyPerfect.OXMod.{u, u} X.toRingedSpace))
    (hE : RingedSpace.IsPerfect (X := X.toRingedSpace) E)
    (hL : DerivedCategoryB.derivedCategoryBMinus
      (fun M : StrictlyPerfect.OXMod.{u, u} X.toRingedSpace => M.IsCoherent) L) :
    DerivedCategoryB.derivedCategoryBMinus
        (fun M : StrictlyPerfect.OXMod.{u, u} X.toRingedSpace => M.IsCoherent)
        (derivedTensorObj X E L) ∧
      DerivedCategoryB.derivedCategoryBMinus
        (fun M : StrictlyPerfect.OXMod.{u, u} X.toRingedSpace => M.IsCoherent)
        (derivedSheafHomObj X E L)

Tag 0D0D, a lemma

Tag 0D0D in the Stacks Project.

Stacks.AlgebraicGeometry.ProperSupportCoherent.moduleFinite_ext_of_proper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProperSupportCoherent/ExtFinitenessUnconditional.lean, line 259.

Stacks Project, Tag 0D0D. Let A be a Noetherian ring, let X be a scheme proper over A, let K be an object of D^-_Coh(𝒪_X) and let L be an object of D^+_Coh(𝒪_X). Then the A-module Ext^n_{𝒪_X}(K, L) is finite, for every n, the A-action being the canonical one induced by the structure morphism X ⟶ Spec A.

Ext^n_{𝒪_X}(K, L) is Hom_{D(𝒪_X)}(K, L⟦n⟧), which is the degree-zero cohomology of RΓ(X, R𝓗om(K, L⟦n⟧)) as an A-module by extLinearEquiv, that is by [Stacks, Tag 08DK]; R𝓗om(K, L⟦n⟧) is an object of D^+_Coh(𝒪_X) by [Stacks, Tag 0D0C], the shift of L being one by derivedCategoryBPlus_isCoherent_shift; and moduleFinite_homologyZero_derivedGlobalSections_of_proper makes the degree-zero hypercohomology of such an object a finite A-module.

theorem moduleFinite_ext_of_proper {A : Type u} [CommRing A] [IsNoetherianRing A]
    (X : Over (Spec (CommRingCat.of A))) [IsProper X.hom]
    (K L : DerivedCategory X.left.Modules)
    (hK : DerivedCategoryB.derivedCategoryBMinus
      (fun M : X.left.Modules => M.IsCoherent) K)
    (hL : DerivedCategoryB.derivedCategoryBPlus
      (fun M : X.left.Modules => M.IsCoherent) L)
    (n : ℤ) :
    letI : Linear A X.left.Modules := modulesLinear A X
    Module.Finite A (DerivedCategory.Ext K L n)

Tag 0FDC, a lemma

Tag 0FDC in the Stacks Project.

Stacks.AlgebraicGeometry.PerfectCohomology.isBoundedCoherent_of_isPerfect_of_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/PseudoCoherentComplex/RegularPerfect.lean, line 79. The attribute's comment: “converse direction only: a perfect object on a quasi-compact regular scheme is bounded with coherent cohomology”.

The converse half of [Stacks, Tag 0FDC]. Let X be a regular scheme which is quasi-compact — equivalently, Noetherian and regular. Then every perfect object of the derived category of 𝒪_X-modules lies in D^b_{Coh}(𝒪_X): it is bounded and all of its cohomology sheaves are coherent.

Regularity enters only through local Noetherianity, so this is Stacks.AlgebraicGeometry.PerfectCohomology.isBoundedCoherent_of_isPerfect ([Stacks, Tag 0FXU]) read at the hypotheses of [Stacks, Tag 0FDC].

theorem isBoundedCoherent_of_isPerfect_of_isRegular
    (X : Scheme.{u}) (hX : IsRegular X) [CompactSpace X]
    [HasDerivedCategory.{d} (StrictlyPerfect.OXMod.{u, u} X.toRingedSpace)]
    (K : DerivedCategory (StrictlyPerfect.OXMod.{u, u} X.toRingedSpace))
    (hK : RingedSpace.IsPerfect (X := X.toRingedSpace) K) :
    DerivedCategoryB.derivedCategoryBBounded
      (fun M : StrictlyPerfect.OXMod.{u, u} X.toRingedSpace => M.IsCoherent) K

Stacks.AlgebraicGeometry.PerfectCohomology.isPerfect_of_isBoundedCoherent_of_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RegularBoundedCoherentPerfect.lean, line 241. The attribute's comment: “forward direction: a bounded object with coherent cohomology on a regular scheme is perfect”.

The forward half of [Stacks, Tag 0FDC]. Let X be a regular scheme. Then every object of D^b_{Coh}(𝒪_X) — every object of the derived category of 𝒪_X-modules which is bounded and all of whose cohomology sheaves are coherent — is perfect.

Quasi-compactness of X is not assumed. The proof is an induction on the length of the interval carrying the cohomology of the object, with AlgebraicGeometry.isPerfect_single_of_isCoherent_of_isRegular as its base case; that statement needs no quasi-compactness either.

theorem isPerfect_of_isBoundedCoherent_of_isRegular {X : Scheme.{u}} (hX : IsRegular X)
    [HasDerivedCategory.{d} (StrictlyPerfect.OXMod.{u, u} X.toRingedSpace)]
    (K : DerivedCategory (StrictlyPerfect.OXMod.{u, u} X.toRingedSpace))
    (hK : DerivedCategoryB.derivedCategoryBBounded
      (fun M : StrictlyPerfect.OXMod.{u, u} X.toRingedSpace => M.IsCoherent) K) :
    RingedSpace.IsPerfect (X := X.toRingedSpace) K

Stacks.AlgebraicGeometry.PerfectCohomology.isPerfect_iff_isBoundedCoherent_of_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RegularBoundedCoherentPerfect.lean, line 262. The attribute's comment: “the equivalence, on a quasi-compact regular scheme”.

[Stacks, Tag 0FDC]. Let X be a quasi-compact regular scheme — equivalently, a Noetherian regular scheme. Then the perfect objects of the derived category of 𝒪_X-modules are exactly the objects of D^b_{Coh}(𝒪_X).

The forward implication is Stacks.AlgebraicGeometry.PerfectCohomology.isPerfect_of_isBoundedCoherent_of_isRegular, which does not use quasi-compactness; the converse is Stacks.AlgebraicGeometry.PerfectCohomology.isBoundedCoherent_of_isPerfect_of_isRegular, which does.

theorem isPerfect_iff_isBoundedCoherent_of_isRegular {X : Scheme.{u}} (hX : IsRegular X)
    [CompactSpace X]
    [HasDerivedCategory.{d} (StrictlyPerfect.OXMod.{u, u} X.toRingedSpace)]
    (K : DerivedCategory (StrictlyPerfect.OXMod.{u, u} X.toRingedSpace)) :
    RingedSpace.IsPerfect (X := X.toRingedSpace) K ↔
      DerivedCategoryB.derivedCategoryBBounded
        (fun M : StrictlyPerfect.OXMod.{u, u} X.toRingedSpace => M.IsCoherent) K

Sources

• Section 36.11, Tag 08E0
• AxiomMath/Stacks at 5ed82d14

LeanStacks.SheafOfModules.coherentDerivedComparison_mem · Stacks.SheafOfModules.coherentDerivedComparison · Stacks.SheafOfModules.coherentDerivedComparison_comp_inclusion · AlgebraicGeometry.coherentToQuasicoherentDerivedMinus · AlgebraicGeometry.coherentToQuasicoherentDerivedMinus_isEquivalence · AlgebraicGeometry.coherentToModulesDerivedMinus_isEquivalence · AlgebraicGeometry.coherentToModulesDerivedBounded_isEquivalence · Stacks.AlgebraicGeometry.ProperSupportCoherent.derivedCategoryBBounded_derivedPushforward_of_isProperOver_supp_unconditional

Section36.12 Descent finiteness properties of complexes#

Section 36.12 of the Stacks Project, Tag 09UC. 6 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 09UD, a lemma

Tag 09UD in the Stacks Project.

Stacks.Cohomology.TorAmplitude.FlatDescent.hasTorAmplitude_derivedPullback_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/TorAmplitude/FlatSurjectiveDescent.lean, line 229.

Let f : X ⟶ Y be a surjective flat morphism of locally ringed spaces, let E be an object of D(𝒪_Y) and let a, b be integers. Then E has Tor amplitude in [a, b] if and only if Lf^*E has Tor amplitude in [a, b].

theorem hasTorAmplitude_derivedPullback_iff {X Y : LocallyRingedSpace.{u}} (f : X ⟶ Y)
    (hsurj : Function.Surjective f.base) (hflat : AlgebraicGeometry.IsFlat f.toShHom)
    (E : DerivedCategory (OXMod.{u, u} Y.toRingedSpace)) (a b : ℤ) :
    HasTorAmplitude Y.toRingedSpace E a b ↔
      HasTorAmplitude X.toRingedSpace
        ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback f.toShHom).obj E)
        a b

Tag 09UE, a lemma

Tag 09UE in the Stacks Project.

Stacks.Cohomology.PseudoCoherence.FpqcDescent.isPseudoCoherentFrom_iff_forall_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/FpqcDescent.lean, line 595.

Stacks 09UE.

public theorem isPseudoCoherentFrom_iff_forall_fpqc {X : Scheme.{u}} {I : Type v}
    (Y : I → Scheme.{u}) (f : ∀ i, Y i ⟶ X)
    (hf : Presieve.ofArrows Y f ∈ Scheme.fpqcPrecoverage X)
    (E : Stacks.Duality.quasiCoherentDerivedCategory X) (m : ℤ) :
    IsPseudoCoherentFrom E.obj m ↔
      ∀ i : I, IsPseudoCoherentFrom
        ((Stacks.Duality.quasiCoherentDerivedPullback' (f i)).obj E).obj m

Tag 09UF, a lemma

Tag 09UF in the Stacks Project.

Stacks.Cohomology.PseudoCoherence.FlatDescent.isPseudoCoherentFrom_iff_forall_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/FppfDescent.lean, line 441.

Let {f_i : X_i ⟶ X} be an fppf covering of schemes, let E be an object of D(𝒪_X) and let m be an integer. Then E is m-pseudo-coherent if and only if each Lf_i^*E is m-pseudo-coherent.

public theorem isPseudoCoherentFrom_iff_forall_fppf {X : Scheme.{u}} {I : Type v}
    (Y : I → Scheme.{u}) (f : ∀ i, Y i ⟶ X)
    (hf : Presieve.ofArrows Y f ∈ Scheme.fppfPrecoverage X)
    (E : DerivedCategory (OXMod.{u, u} X.toRingedSpace)) (m : ℤ) :
    IsPseudoCoherentFrom E m ↔
      ∀ i : I, IsPseudoCoherentFrom
        ((derivedPullback (f i).toLRSHom.toShHom).obj E) m

Tag 09UG, a lemma

Tag 09UG in the Stacks Project.

Stacks.Cohomology.PerfectComplexes.FpqcDescent.isPerfect_iff_forall_isPerfect_derivedPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/FpqcDescent.lean, line 157.

Stacks 09UG. Let {f_i : Y_i ⟶ X} be an fpqc covering of schemes and let E ∈ D(𝒪_X). Then E is perfect if and only if each derived pullback Lf_i^*E is perfect.

public theorem isPerfect_iff_forall_isPerfect_derivedPullback {X : Scheme.{u}} {I : Type v}
    (Y : I → Scheme.{u}) (f : ∀ i, Y i ⟶ X)
    (hf : Presieve.ofArrows Y f ∈ Scheme.fpqcPrecoverage X)
    (E : DerivedCategory (OXMod.{u, u} X.toRingedSpace)) :
    IsPerfect (X := X.toRingedSpace) E ↔
      ∀ i, IsPerfect (X := (Y i).toRingedSpace)
        ((derivedPullback (f i).toLRSHom.toShHom).obj E)

Tag 09VA, a lemma

Tag 09VA in the Stacks Project.

AlgebraicGeometry.RingedSpace.isPseudoCoherentFrom_derivedPushforwardOXMod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/DerivedPushforwardPseudoCoherent.lean, line 116. The attribute's comment: “E m-pseudo-coherent implies Ri_E m-pseudo-coherent”. References: SGA 6 III (1.1.1), “necessity: E ⇒ Ri_E”.

The forward half of Stacks 09VA. Let i : Z ⟶ X be a morphism of ringed spaces whose underlying continuous map is a closed immersion and such that i_*𝒪_Z is pseudo-coherent as an 𝒪_X-module. If E ∈ D(𝒪_Z) is m-pseudo-coherent then so is Ri_*E.

Pseudo-coherence is local on X. Away from the image of i the restriction of Ri_*E vanishes. Around a point i(z) of the image, a strictly perfect approximation 𝒫 ⟶ 𝒦|_{i⁻¹U} of a complex 𝒦 representing E is pushed forward degreewise along i|_{i⁻¹U}; exactness of pushforward preserves the two cohomological conditions, (i|_{i⁻¹U})_*𝒫 is m-pseudo-coherent because its terms are direct summands of powers of (i|_{i⁻¹U})_*𝒪 and it is bounded, and the target is (Ri_*E)|_U. Stacks 08CC part (1) in the form AlgebraicGeometry.RingedSpace.isPseudoCoherentFrom_of_approximation finishes.

public theorem isPseudoCoherentFrom_derivedPushforwardOXMod
    (hi : Topology.IsClosedEmbedding i.hom.base)
    (hO : IsPseudoCoherent ((DerivedCategory.singleFunctor (OXMod.{u, u} X) 0).obj
      (pushforwardStructureModule i)))
    (m : ℤ) (E : DerivedCategory (OXMod.{u, u} Z)) (hE : IsPseudoCoherentFrom E m) :
    IsPseudoCoherentFrom ((derivedPushforwardOXMod i hi).obj E) m

AlgebraicGeometry.RingedSpace.isPseudoCoherentFrom_of_derivedPushforwardOXMod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/PushforwardReflectPseudoCoherent.lean, line 372. The attribute's comment: “Ri_E m-pseudo-coherent implies E m-pseudo-coherent”. References: SGA 6 III (1.1.1), “sufficiency: Ri_E ⇒ E”.

The converse half of Stacks 09VA. Let i : Z ⟶ X be a morphism of ringed spaces whose underlying continuous map is a closed embedding and such that i_*𝒪_Z is pseudo-coherent as an 𝒪_X-module. If Ri_*E is m-pseudo-coherent for E ∈ D(𝒪_Z) then so is E.

Pseudo-coherence is local on Z, and the opens i⁻¹W for W open in X are a fundamental system of neighbourhoods of a point of Z, so it is enough to produce, for each z, an open W of X containing i(z) on which E becomes m-pseudo-coherent. Take for W an open on which the cohomology of Ri_*E is bounded above (AlgebraicGeometry.RingedSpace.exists_isZero_homology_gt_derivedRestrict); then the cohomology of E|_{i⁻¹W} is bounded above as well, because i_* reflects zero objects (AlgebraicGeometry.RingedSpace.isZero_homology_of_isZero_homology_derivedPushforward), and AlgebraicGeometry.RingedSpace.isPseudoCoherentFrom_Q_of_derivedPushforwardOXMod_of_bounded' applies to i|_{i⁻¹W} : Z|_{i⁻¹W} ⟶ X|_W.

public theorem isPseudoCoherentFrom_of_derivedPushforwardOXMod {Z X : RingedSpace.{u, u}}
    [HasDerivedCategory.{d} (StrictlyPerfect.OXMod.{u, u} Z)]
    [HasDerivedCategory.{d} (StrictlyPerfect.OXMod.{u, u} X)]
    [∀ V : Opens X.carrier,
      HasDerivedCategory.{w} (StrictlyPerfect.OXMod.{u, u} (X.restrict V.isOpenEmbedding))]
    [∀ V : Opens Z.carrier,
      HasDerivedCategory.{w} (StrictlyPerfect.OXMod.{u, u} (Z.restrict V.isOpenEmbedding))]
    (i : Z ⟶ X) (hi : Topology.IsClosedEmbedding i.hom.base)
    (hO : IsPseudoCoherent ((DerivedCategory.singleFunctor (StrictlyPerfect.OXMod.{u, u} X) 0).obj
      (pushforwardStructureModule i)))
    (m : ℤ) (E : DerivedCategory (StrictlyPerfect.OXMod.{u, u} Z))
    (hE : IsPseudoCoherentFrom ((derivedPushforwardOXMod i hi).obj E) m) :
    IsPseudoCoherentFrom E m

Tag 09VB, a lemma

Tag 09VB in the Stacks Project.

AlgebraicGeometry.isPseudoCoherentFrom_iff_derivedPushforward_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/FinitePushforwardDescent.lean, line 74.

Let f : X ⟶ Y be a finite morphism of schemes such that f_*𝒪_X is pseudo-coherent as an 𝒪_Y-module, that is, such that the object of D(𝒪_Y) it determines in degree zero is pseudo-coherent in the sense of Stacks 08CB. Let E be an object of D_{QCoh}(𝒪_X). Then E is m-pseudo-coherent if and only if Rf_*E is m-pseudo-coherent.

theorem isPseudoCoherentFrom_iff_derivedPushforward_of_isFinite {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsFinite f]
    (hf : RingedSpace.IsPseudoCoherent (X := Y.toRingedSpace)
      ((DerivedCategory.singleFunctor Y.Modules 0).obj
        ((Scheme.Modules.pushforward f).obj (SheafOfModules.unit X.ringCatSheaf))))
    (E : DerivedCategory X.Modules)
    (hE : ∀ i : ℤ, ((DerivedCategory.homologyFunctor X.Modules i).obj E).IsQuasicoherent)
    (m : ℤ) :
    RingedSpace.IsPseudoCoherentFrom (X := X.toRingedSpace) E m ↔
      RingedSpace.IsPseudoCoherentFrom (X := Y.toRingedSpace)
        ((RingedSpace.derivedPushforward f.toLRSHom.toShHom).obj E) m

Sources

• Section 36.12, Tag 09UC
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Cohomology.TorAmplitude.FlatDescent.hasTorAmplitude_derivedPullback_iff · Stacks.Cohomology.PseudoCoherence.FpqcDescent.isPseudoCoherentFrom_iff_forall_fpqc · Stacks.Cohomology.PseudoCoherence.FlatDescent.isPseudoCoherentFrom_iff_forall_fppf · Stacks.Cohomology.PerfectComplexes.FpqcDescent.isPerfect_iff_forall_isPerfect_derivedPullback · AlgebraicGeometry.RingedSpace.isPseudoCoherentFrom_derivedPushforwardOXMod · AlgebraicGeometry.RingedSpace.isPseudoCoherentFrom_of_derivedPushforwardOXMod · AlgebraicGeometry.isPseudoCoherentFrom_iff_derivedPushforward_of_isFinite

Section36.13 Lifting complexes#

Section 36.13 of the Stacks Project, Tag 08EC. 12 tags here are carried by 19 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 08ED, a lemma

Tag 08ED in the Stacks Project.

AlgebraicGeometry.exists_quasicoherentDerived_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/OpenLift/EssentialSurjectivity.lean, line 129. The attribute's comment: “unbounded derived category”.

Stacks Project, Tag 08ED. Every quasi-coherent derived object on a quasi-compact open subscheme extends to a quasi-coherent derived object on the ambient scheme: the functor D_QCoh(𝒪_X) ⟶ D_QCoh(𝒪_U) given by restriction is essentially surjective.

theorem exists_quasicoherentDerived_lift (E : QuasicoherentDerivedCategory U) :
    ∃ F : QuasicoherentDerivedCategory X,
      Nonempty ((derivedPullback j.toLRSHom.toShHom).obj F.obj ≅ E.obj)

AlgebraicGeometry.exists_quasicoherentDerived_plus_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/OpenLift/EssentialSurjectivity.lean, line 141. The attribute's comment: “bounded-below derived category”.

Stacks Project, Tag 08ED. A bounded-below quasi-coherent derived object on a quasi-compact open subscheme has a bounded-below quasi-coherent lift: the functor D⁺_QCoh(𝒪_X) ⟶ D⁺_QCoh(𝒪_U) given by restriction is essentially surjective.

No quasi-compactness of the ambient scheme is needed, the derived direct image preserving a lower cohomological bound for an arbitrary morphism of schemes.

theorem exists_quasicoherentDerived_plus_lift (E : QuasicoherentDerivedCategory U)
    (hE : DerivedCategory.TStructure.t.plus E.obj) :
    ∃ F : QuasicoherentDerivedCategory X,
      DerivedCategory.TStructure.t.plus F.obj ∧
      Nonempty ((derivedPullback j.toLRSHom.toShHom).obj F.obj ≅ E.obj)

AlgebraicGeometry.exists_quasicoherentDerived_minus_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/OpenLift/EssentialSurjectivity.lean, line 159. The attribute's comment: “bounded-above derived category”.

Stacks Project, Tag 08ED. A bounded-above quasi-coherent derived object on a quasi-compact open subscheme of a quasi-compact scheme has a bounded-above quasi-coherent lift: the functor D⁻_QCoh(𝒪_X) ⟶ D⁻_QCoh(𝒪_U) given by restriction is essentially surjective.

Quasi-compactness of the ambient scheme is what bounds the cohomological dimension of j, and so bounds the shift by which the derived direct image can raise an upper bound.

theorem exists_quasicoherentDerived_minus_lift [CompactSpace X]
    (E : QuasicoherentDerivedCategory U) (hE : DerivedCategory.TStructure.t.minus E.obj) :
    ∃ F : QuasicoherentDerivedCategory X,
      DerivedCategory.TStructure.t.minus F.obj ∧
      Nonempty ((derivedPullback j.toLRSHom.toShHom).obj F.obj ≅ E.obj)

AlgebraicGeometry.exists_quasicoherentDerived_bounded_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/OpenLift/EssentialSurjectivity.lean, line 177. The attribute's comment: “bounded derived category”.

Stacks Project, Tag 08ED. A bounded quasi-coherent derived object on a quasi-compact open subscheme of a quasi-compact scheme has a bounded quasi-coherent lift: the functor D^b_QCoh(𝒪_X) ⟶ D^b_QCoh(𝒪_U) given by restriction is essentially surjective.

theorem exists_quasicoherentDerived_bounded_lift [CompactSpace X]
    (E : QuasicoherentDerivedCategory U) (hE : DerivedCategory.TStructure.t.bounded E.obj) :
    ∃ F : QuasicoherentDerivedCategory X,
      DerivedCategory.TStructure.t.bounded F.obj ∧
      Nonempty ((derivedPullback j.toLRSHom.toShHom).obj F.obj ≅ E.obj)

Tag 0G48, a lemma

Tag 0G48 in the Stacks Project.

AlgebraicGeometry.essSurj_coherentDerivedBoundedRestrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedCoherent/EssSurjRestrictOpen.lean, line 88.

[Stacks, Tag 0G48]. On a Noetherian scheme, restriction to an open subscheme is essentially surjective as a functor D^b_Coh(𝒪_X) ⥤ D^b_Coh(𝒪_U): every bounded complex of 𝒪_U-modules with coherent cohomology is the restriction of one on X.

theorem essSurj_coherentDerivedBoundedRestrict {X : Scheme.{u}} [IsNoetherian X] (U : X.Opens) :
    (coherentDerivedBoundedRestrict U).EssSurj

Tag 08EE, a lemma

Tag 08EE in the Stacks Project.

AlgebraicGeometry.exists_boundedAbove_finiteFree_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/OpenLift/FiniteFreeComplex.lean, line 1188.

A pseudo-coherent derived object on a quasi-compact open of an affine scheme is the restriction of a bounded-above complex of finite free modules.

theorem exists_boundedAbove_finiteFree_lift
    (X : Scheme.{u}) [IsAffine X] (U : X.Opens)
    (hU : IsCompact (U : Set X))
    [HasDerivedCategory.{d} (OXMod.{u} (X.toRingedSpace.restrict U.isOpenEmbedding))]
    (E : DerivedCategory (OXMod.{u} (X.toRingedSpace.restrict U.isOpenEmbedding)))
    (hE : AlgebraicGeometry.RingedSpace.IsPseudoCoherent
      (X := X.toRingedSpace.restrict U.isOpenEmbedding) E) :
    ∃ P : CochainComplex (OXMod.{u} X.toRingedSpace) ℤ,
      (∃ b : ℤ, ∀ i : ℤ, b < i → CategoryTheory.Limits.IsZero (P.X i)) ∧
      (∀ i : ℤ, ∃ I : Type u, Finite I ∧ Nonempty
        (P.X i ≅ SheafOfModules.free (R := structureSheafOfRings X.toRingedSpace) I)) ∧
      Nonempty (DerivedCategory.Q.obj
        (((RingedSpace.restrictModules X.toRingedSpace U).mapHomologicalComplex
          (ComplexShape.up ℤ)).obj P) ≅ E)

Tag 08EF, a lemma

Tag 08EF in the Stacks Project.

Stacks.DerivedQCoh.exists_pos_subsingleton_hom_singleFunctor_of_isFiniteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/EventualExtVanishing.lean, line 589.

Stacks Project, Tag 08EF. Let X be a quasi-compact and quasi-separated scheme and let E ∈ D^b_{QCoh}(𝒪_X). There exists an integer n₀ > 0 such that Ext^n_{D(𝒪_X)}(ℰ, E) = 0 for every finite locally free 𝒪_X-module ℰ and every n ≥ n₀.

The Ext group is the group of morphisms ℰ ⟶ E⟦n⟧ in D(𝒪_X), with ℰ placed in cohomological degree zero, and its vanishing is subsingletonness of that group.

theorem exists_pos_subsingleton_hom_singleFunctor_of_isFiniteLocallyFree
    (X : Scheme.{u}) [CompactSpace X] [QuasiSeparatedSpace X]
    (E : DerivedCategory X.Modules)
    (hE : DerivedCategoryB.derivedCategoryBBounded
      (SheafOfModules.isQuasicoherent X.ringCatSheaf) E) :
    ∃ n₀ : ℤ, 0 < n₀ ∧
      ∀ ℰ : X.Modules, AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} ℰ →
        ∀ n : ℤ, n₀ ≤ n →
          Subsingleton ((DerivedCategory.singleFunctor X.Modules 0).obj ℰ ⟶ E⟦n⟧)

Tag 09M4, a lemma

Tag 09M4 in the Stacks Project.

Stacks.DerivedQCoh.exists_window_subsingleton_hom_of_isPerfect_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DetectingBoundednessOfAPerfectComplex.lean, line 147. The attribute's comment: “part (1)”.

[Stacks, Tag 09M4], part (1). Let X be a quasi-compact and quasi-separated scheme and let K be a perfect object of D(𝒪_X). Then there are integers a ≤ b such that every L ∈ D_QCoh(𝒪_X) whose cohomology sheaves vanish in the degrees a, …, b admits no nonzero morphism K ⟶ L.

This is Stacks.DerivedQCoh.exists_window_subsingleton_hom_of_isPerfect_general at the derived global sections Stacks.DerivedQCoh.schemeDerivedSections X, which exist for every scheme; the statement mentions no derived global sections functor and carries no hypothesis beyond the source's.

theorem exists_window_subsingleton_hom_of_isPerfect_qcqs (K : DerivedCategory X.Modules)
    (hK : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace) K) :
    ∃ a b : ℤ, a ≤ b ∧
      ∀ L : DerivedCategory X.Modules,
        (∀ i : ℤ, ((DerivedCategory.homologyFunctor X.Modules i).obj L).IsQuasicoherent) →
        (∀ i : ℤ, a ≤ i → i ≤ b → IsZero ((DerivedCategory.homologyFunctor X.Modules i).obj L)) →
        Subsingleton (K ⟶ L)

Stacks.DerivedQCoh.finite_setOf_not_subsingleton_hom_shift_of_isPerfect_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DetectingBoundednessOfAPerfectComplex.lean, line 164. The attribute's comment: “part (2)”.

[Stacks, Tag 09M4], part (2). Let X be a quasi-compact and quasi-separated scheme, let K be a perfect object of D(𝒪_X) and let L be a bounded object of D_QCoh(𝒪_X). Then Ext^n_{D(𝒪_X)}(K, L) = Hom_{D(𝒪_X)}(K, L⟦n⟧) vanishes for all but finitely many n.

This is Stacks.DerivedQCoh.finite_setOf_not_subsingleton_hom_shift_of_isPerfect_general at the derived global sections Stacks.DerivedQCoh.schemeDerivedSections X.

theorem finite_setOf_not_subsingleton_hom_shift_of_isPerfect_qcqs (K : DerivedCategory X.Modules)
    (hK : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace) K)
    (L : DerivedCategory X.Modules)
    (hLqc : ∀ i : ℤ, ((DerivedCategory.homologyFunctor X.Modules i).obj L).IsQuasicoherent)
    (c d : ℤ) (hLGE : L.IsGE c) (hLLE : L.IsLE d) :
    {n : ℤ | ¬ Subsingleton (K ⟶ L⟦n⟧)}.Finite

Tag 08EG, a lemma

Tag 08EG in the Stacks Project.

Stacks.DerivedQCoh.OpenLift.exists_finiteLocallyFree_biprod_iso_restrict_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/OpenLift/ShiftedBundleSummand.lean, line 428.

[Stacks, Tag 08EG]. Let X be an affine scheme and U ⊆ X a quasi-compact open. For every perfect object E of D(𝒪_U) there are an integer r, a finite locally free 𝒪_U-module ℱ and a perfect complex P of 𝒪_X-modules with ℱ[-r] ⊕ E ≅ P|_U, where ℱ[-r] is ℱ placed in cohomological degree r.

theorem exists_finiteLocallyFree_biprod_iso_restrict_of_isPerfect
    (X : Scheme.{u}) [IsAffine X] (U : X.Opens) (hU : IsCompact (U : Set X))
    (E : DerivedCategory U.toScheme.Modules)
    (hE : IsPerfect (X := U.toScheme.toRingedSpace) E) :
    ∃ (r : ℤ) (F : U.toScheme.Modules) (P : CochainComplex (OXMod.{u, u, u} X.toRingedSpace) ℤ),
      AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} F ∧
      IsPerfectComplex P ∧
      Nonempty (((DerivedCategory.singleFunctor U.toScheme.Modules r).obj F ⊞ E) ≅
        DerivedCategory.Q.obj
          (((AlgebraicGeometry.RingedSpace.restrictModules.{u, u} X.toRingedSpace
            U).mapHomologicalComplex (ComplexShape.up ℤ)).obj P))

Tag 08EH, a lemma

Tag 08EH in the Stacks Project.

Stacks.DerivedQCoh.OpenLift.exists_isPerfect_derivedTensor_lift_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/OpenLift/AffineLift.lean, line 245.

Let X be an affine scheme and U ⊆ X a quasi-compact open. Let E, E' be objects of D_QCoh(𝒪_X) with E perfect. For every morphism α : E|_U ⟶ E'|_U there are a perfect object I of D(𝒪_X), a morphism b : I ⟶ 𝒪_X whose restriction to U is an isomorphism, and a morphism γ : E ⊗^L I ⟶ E', such that, writing β : E ⊗^L I ⟶ E ⊗^L 𝒪_X ≅ E for the morphism induced by b, the object E₁ = E ⊗^L I is perfect, β|_U is an isomorphism and α = γ|_U ∘ (β|_U)⁻¹.

theorem exists_isPerfect_derivedTensor_lift_of_isAffine (X : Scheme.{u}) [IsAffine X]
    (U : X.Opens) (hU : IsCompact (U : Set X))
    (E E' : DerivedCategory (SheafOfModules X.ringCatSheaf))
    (hE : Stacks.Cohomology.PerfectComplexes.IsPerfect.{u, u, u + 1} (X := X.toRingedSpace) E)
    (hE' : ∀ i : ℤ, ((DerivedCategory.homologyFunctor X.Modules i).obj E').IsQuasicoherent)
    (α : (derivedRestrict U.ι).obj E ⟶ (derivedRestrict U.ι).obj E') :
    letI := derivedMonoidalStructure X.sheaf
    ∃ (I : DerivedCategory (SheafOfModules X.ringCatSheaf))
      (b : I ⟶ 𝟙_ (DerivedCategory (SheafOfModules X.ringCatSheaf))) (γ : E ⊗ I ⟶ E'),
      Stacks.Cohomology.PerfectComplexes.IsPerfect.{u, u, u + 1} (X := X.toRingedSpace) I ∧
      IsIso ((derivedRestrict U.ι).map b) ∧
      Stacks.Cohomology.PerfectComplexes.IsPerfect.{u, u, u + 1} (X := X.toRingedSpace)
        (E ⊗ I : DerivedCategory (SheafOfModules X.ringCatSheaf)) ∧
      IsIso ((derivedRestrict U.ι).map (E ◁ b ≫ (ρ_ E).hom)) ∧
      (derivedRestrict U.ι).map (E ◁ b ≫ (ρ_ E).hom) ≫ α = (derivedRestrict U.ι).map γ

Tag 08EI, a lemma

Tag 08EI in the Stacks Project.

Stacks.DerivedQCoh.OpenLift.exists_isPerfectComplex_restrict_iso_biprod_shift_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/OpenLift/AffineLift.lean, line 361.

Let X be an affine scheme and U ⊆ X a quasi-compact open. For every perfect object F of D(𝒪_U) the object F ⊕ F[1] is the restriction of a perfect object of D(𝒪_X): there is a perfect complex P of 𝒪_X-modules whose degreewise restriction to U represents F ⊕ F[1].

theorem exists_isPerfectComplex_restrict_iso_biprod_shift_of_isAffine (X : Scheme.{u})
    [IsAffine X] (U : X.Opens) (hU : IsCompact (U : Set X))
    (F : DerivedCategory U.toScheme.Modules)
    (hF : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := U.toScheme.toRingedSpace) F) :
    ∃ P : CochainComplex (StrictlyPerfect.OXMod.{u, u, u} X.toRingedSpace) ℤ,
      Stacks.Cohomology.PerfectComplexes.IsPerfectComplex P ∧
      Nonempty ((F ⊞ F⟦(1 : ℤ)⟧) ≅ DerivedCategory.Q.obj
        (((AlgebraicGeometry.RingedSpace.restrictModules.{u, u} X.toRingedSpace
          U).mapHomologicalComplex (ComplexShape.up ℤ)).obj P))

Tag 08EJ, a lemma

Tag 08EJ in the Stacks Project.

Stacks.PowerTorsion.exists_pow_smul_eq_zero_of_isPerfect_of_cohomologySupportedOn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/AffinePowerTorsion.lean, line 152. The attribute's comment: “on an affine scheme, in D(𝒪_X); the base case of the induction over the quasi-compact opens that gives the quasi-compact quasi-separated case”.

[Stacks, Tag 08EJ] on an affine scheme. Let R be a commutative ring, let f : R and let X = Spec R. Let α : E ⟶ E' be a morphism of D_QCoh(𝒪_X) such that E is perfect and E' is supported on the closed subset T = V(f), that is, the cohomology sheaves of E' have vanishing stalks at every point off V(f). Then f ^ n • α = 0 for some n ≥ 0.

Both objects are Ñ for an object N of D(R) by [Stacks, Tag 06Z0], perfectness of E becomes perfectness of its preimage M by [Stacks, Tag 08EB], and the support condition on E' becomes f-power torsion of the cohomology modules of the preimage N. The statement in D(R) is StacksDraft.Perfect.homPowerTorsion_of_isPerfect; derived sheafification carries its conclusion back, being R-linear and fully faithful.

This is the base case of the induction over the quasi-compact opens that proves the statement for a quasi-compact quasi-separated scheme, Stacks.PowerTorsion.exists_pow_smul_eq_zero_of_isPerfect_of_cohomologySupportedOn_qcqs.

theorem exists_pow_smul_eq_zero_of_isPerfect_of_cohomologySupportedOn (f : R)
    {E E' : DerivedCategory (Spec (CommRingCat.of R)).Modules}
    (hE : Stacks.Cohomology.PerfectComplexes.IsPerfect
      (X := (Spec (CommRingCat.of R)).toRingedSpace) E)
    (hEq : ∀ n : ℤ, ((DerivedCategory.homologyFunctor
      (Spec (CommRingCat.of R)).Modules n).obj E).IsQuasicoherent)
    (hE'q : ∀ n : ℤ, ((DerivedCategory.homologyFunctor
      (Spec (CommRingCat.of R)).Modules n).obj E').IsQuasicoherent)
    (hsupp : CohomologySupportedOn (Spec (CommRingCat.of R)).ringCatSheaf
      (PrimeSpectrum.zeroLocus {f}) E')
    (α : E ⟶ E') :
    letI : Linear R (Spec (CommRingCat.of R)).Modules := modulesLinear R (specBase R)
    ∃ k : ℕ, f ^ k • α = 0

Stacks.DerivedQCoh.exists_pow_smul_eq_zero_of_isPerfect_of_cohomologySupportedOn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/PowerTorsionAffineOpen.lean, line 215. The attribute's comment: “on a quasi-compact quasi-separated scheme, the statement in full”.

Let X be a quasi-compact quasi-separated scheme and let f ∈ Γ(X, 𝒪_X). Let E and E' be objects of D_QCoh(𝒪_X) with E perfect and E' cohomologically supported on T = V(f). Then for every α : E ⟶ E' there is an n ≥ 0 with f ^ n · α = 0.

public theorem exists_pow_smul_eq_zero_of_isPerfect_of_cohomologySupportedOn {X : Scheme.{u}}
    [CompactSpace X] [QuasiSeparatedSpace X] (f : Γ(X, ⊤))
    (E F : DerivedCategory X.Modules)
    (hFqc : ∀ i : ℤ, ((DerivedCategory.homologyFunctor X.Modules i).obj F).IsQuasicoherent)
    (hE : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace) E)
    (hF : AlgebraicGeometry.CohomologySupportedOn X.ringCatSheaf (X.zeroLocus {f}) F)
    (α : E ⟶ F) :
    ∃ n : ℕ, globalScalar X.ringCatSheaf f ^ n • α = 0

Stacks.PowerTorsion.exists_pow_smul_eq_zero_of_isPerfect_of_cohomologySupportedOn_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/QcqsPowerTorsion.lean, line 412.

[Stacks, Tag 08EJ]. Let X be a quasi-compact quasi-separated scheme and let f ∈ Γ(X, 𝒪_X). Let α : E ⟶ E' be a morphism of D_QCoh(𝒪_X) such that E is perfect and E' is supported on the closed subset T = V(f), that is, the cohomology sheaves of E' have vanishing stalks at every point where f does not vanish. Then f ^ n • α = 0 for some n ≥ 0.

The scalar acts through the Γ(X, 𝒪_X)-linear structure AlgebraicGeometry.Scheme.linearOfRingHom of the identity ring map, which is a definition and not an instance -- a scheme does not determine a base ring -- and so appears as a letI in the statement.

This is Stacks.PowerTorsion.powerTorsionProperty_top at the degree 0, the shift being undone by the unitor of the shift.

theorem exists_pow_smul_eq_zero_of_isPerfect_of_cohomologySupportedOn_qcqs {X : Scheme.{u}}
    [CompactSpace X] [QuasiSeparatedSpace X] (f : Γ(X, ⊤)) (E E' : DerivedCategory X.Modules)
    (hE : IsPerfect (X := ringedSpace X) E)
    (hEq : ∀ n : ℤ, ((DerivedCategory.homologyFunctor X.Modules n).obj E).IsQuasicoherent)
    (hE'q : ∀ n : ℤ, ((DerivedCategory.homologyFunctor X.Modules n).obj E').IsQuasicoherent)
    (hsupp : CohomologySupportedOn X.ringCatSheaf ((X.basicOpen f : Set X)ᶜ) E')
    (α : E ⟶ E') :
    letI : Linear Γ(X, ⊤) X.Modules := Scheme.linearOfRingHom X Γ(X, ⊤) (RingHom.id Γ(X, ⊤))
    ∃ k : ℕ, f ^ k • α = 0

StacksDraft.Perfect.exists_pow_smul_eq_zero_of_isPerfect_of_support_subset_zeroLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Perfect/PowerTorsionTarget.lean, line 182. The attribute's comment: “affine case, in D(A); the geometric form on an affine scheme, and the quasi-compact quasi-separated case, are in the AlgebraicGeometry directory”.

Let A be a commutative ring and let f : A. Let α : E ⟶ E' be a morphism in D(A) such that E is perfect and E' is supported on T = V(f), that is, every cohomology module of E' has support contained in the zero locus of f. Then there is an n ≥ 0 with f ^ n • α = 0.

public theorem exists_pow_smul_eq_zero_of_isPerfect_of_support_subset_zeroLocus (f : A)
    {E E' : DerivedCategory (ModuleCat.{u} A)} (hE : IsPerfect E)
    (hE' : ∀ p : ℤ, Module.support A
      ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) p).obj E' : Type u) ⊆
      PrimeSpectrum.zeroLocus {f})
    (α : E ⟶ E') : ∃ n : ℕ, f ^ n • α = 0

Tag 08EK, a lemma

Tag 08EK in the Stacks Project.

Stacks.DerivedQCoh.OpenLift.exists_isPerfectComplex_supported_restrict_iso_biprod_shift_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/OpenLift/AffineSupportedLift.lean, line 44.

Let X be an affine scheme, T ⊆ X a closed subset with X ∖ T quasi-compact and U ⊆ X a quasi-compact open. For every perfect object F of D(𝒪_U) whose cohomology is supported on T ∩ U, the object F ⊕ F[1] is the restriction of a perfect object of D(𝒪_X) with cohomology supported on T: there is a perfect complex P of 𝒪_X-modules, with cohomology supported on T, whose degreewise restriction to U represents F ⊕ F[1].

theorem exists_isPerfectComplex_supported_restrict_iso_biprod_shift_of_isAffine
    (X : Scheme.{u}) [IsAffine X]
    (T : Set X) (hT : IsClosed T) (hTc : IsCompact Tᶜ)
    (U : X.Opens) (hU : IsCompact (U : Set X))
    (F : DerivedCategory U.toScheme.Modules)
    (hF : IsPerfect (X := U.toScheme.toRingedSpace) F)
    (hFT : CohomologySupportedOn U.toScheme.ringCatSheaf (Subtype.val ⁻¹' T) F) :
    ∃ P : CochainComplex (StrictlyPerfect.OXMod.{u, u, u} X.toRingedSpace) ℤ,
      IsPerfectComplex P ∧
      CohomologySupportedOn X.ringCatSheaf T (DerivedCategory.Q.obj P) ∧
      Nonempty ((F ⊞ F⟦(1 : ℤ)⟧) ≅ DerivedCategory.Q.obj
        (((AlgebraicGeometry.RingedSpace.restrictModules.{u, u} X.toRingedSpace
          U).mapHomologicalComplex (ComplexShape.up ℤ)).obj P))

Tag 09IM, a lemma

Tag 09IM in the Stacks Project.

Stacks.Perfect.LiftingComplexes.exists_isPerfect_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/LiftingComplexes/General.lean, line 341.

[Stacks, Tag 09IM]. Let X be a quasi-compact quasi-separated scheme, U ⊆ X a quasi-compact open, T ⊆ X a closed subset whose complement is retrocompact in X, and E an object of D_QCoh(𝒪_X). Every map α : P ⟶ E|_U out of a perfect object P of D(𝒪_U) whose cohomology is supported on T ∩ U comes from a map β : R ⟶ E out of a perfect object R of D(𝒪_X) whose cohomology is supported on T, with P a direct summand of R|_U by an inclusion i satisfying i ≫ β|_U = α.

Quasi-compactness of X gives a finite cover of X by affine opens; the statement then follows from Stacks.Perfect.LiftingComplexes.exists_isPerfect_lift_of_list by the induction over that cover, whose single step glues the object already built over a smaller open to the one the affine case produces over the next affine.

theorem exists_isPerfect_lift {X : Scheme.{u}} [CompactSpace X] [QuasiSeparatedSpace X]
    (U : X.Opens) (hU : IsCompact (U : Set X)) (T : Set X) (hT : IsClosed T)
    (hTc : ∀ W : X.Opens, IsCompact (W : Set X) → IsCompact ((W : Set X) ∩ Tᶜ))
    (E : DerivedCategory X.Modules)
    (hE : Stacks.DerivedQCoh.IsDQCoh (R := X.ringCatSheaf) E)
    (P : DerivedCategory U.toScheme.Modules) (hP : IsPerfect (X := ringedSpace U.toScheme) P)
    (hPT : CohomologySupportedOn U.toScheme.ringCatSheaf (⇑U.ι.base ⁻¹' T) P)
    (α : P ⟶ (derivedRestrict U.ι).obj E) :
    ∃ (R : DerivedCategory X.Modules) (β : R ⟶ E),
      IsPerfect (X := ringedSpace X) R ∧
      CohomologySupportedOn X.ringCatSheaf T R ∧
      ∃ (i : P ⟶ (derivedRestrict U.ι).obj R) (p : (derivedRestrict U.ι).obj R ⟶ P),
        i ≫ p = 𝟙 P ∧ i ≫ (derivedRestrict U.ι).map β = α

Tag 09IN, a remark

Tag 09IN in the Stacks Project.

Stacks.Perfect.SupportedLiftDegree.exists_isPerfect_supported_hom_biprod_sumShifts_isZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportedLiftDegree.lean, line 204. The attribute's comment: “The complement of P in R|_U is a finite biproduct of positive shifts of P, and for every degree n the construction can be iterated so that the complement has vanishing cohomology in all degrees ≥ n, which is the agreement of the cohomology sheaves of R|_U and of P above n.”.

[Stacks, Tag 09IN]. Let X be a quasi-compact quasi-separated scheme, U ⊆ X a quasi-compact open, T ⊆ X closed with X ∖ T retrocompact, and E an object of D(𝒪_X) with quasi-coherent cohomology. Let P be a perfect object of D(𝒪_U) supported on T ∩ U and α : P ⟶ E|_U. Then for every degree n there are a perfect object R of D(𝒪_X) supported on T, a map β : R ⟶ E, an object Q of D(𝒪_U) and an isomorphism R|_U ≅ P ⊞ Q through which β|_U is the projection onto P followed by α, with Q a finite biproduct of positive shifts of P and Hⁱ(Q) = 0 for every i ≥ n.

The two clauses are the remark's two sentences: the shape R|_U = P ⊕ P^{⊕n_1}[1] ⊕ ⋯ ⊕ P^{⊕n_m}[m], recorded as Stacks.SumOfPositiveShifts.IsSumOfPositiveShifts, and the agreement of the cohomology sheaves of R|_U and of P above the given degree, which for a splitting is the vanishing of the complement there. The degree is fixed first: the other reading, one R serving every n, is false, because a perfect object is bounded, so agreement in every degree would make P ⟶ R|_U an isomorphism and extend P to a perfect object of D(𝒪_X).

The statement proved here is stronger than the remark in one further respect, and that strengthening is what makes the iteration possible: β|_U is the projection R|_U ⟶ P followed by α, not merely a map restricting to α on the summand.

Where the formalisation departs from the source's recipe. The remark says to repeat the construction "for the map P^{⊕n_1}[1] ⊕ ⋯ ⊕ P^{⊕n_m}[m] ⟶ R|_U", that is, with ambient object R and then to take cones. A map out of cone(ρ) extends a map out of R only when its composite with ρ vanishes, and with ambient object R nothing makes ρ ≫ β vanish, so that route loses the map to E at the first cone. The route taken instead carries, at each stage k, the fibre F_k of β_k : R_k ⟶ E — the first vertex of a distinguished triangle F_k ⟶ R_k ⟶ E ⟶ F_k⟦1⟧ — and applies [Stacks, Tag 09IM] with ambient object F_k; the cone is then formed on ρ := β'' ≫ u with u : F_k ⟶ R_k, and ρ ≫ β_k = β'' ≫ (u ≫ β_k) = 0 because u and β_k are consecutive maps of a distinguished triangle. The octahedral axiom returns both the new map to E and the new fibre at once. The device is Stacks.SplitLiftTower.exists_biprod_iso_lift_of_fibre_octahedron and the iteration is DerivedCategory.exists_hom_biprod_iso_of_fibreOracle.

[Stacks, Tag 09IM] itself is registered on another declaration and is used here through Stacks.Perfect.SupportedLiftGeneral.exists_isPerfect_supported_hom_biprod_sumShifts.

theorem exists_isPerfect_supported_hom_biprod_sumShifts_isZero (X : Scheme.{u}) [CompactSpace X]
    [QuasiSeparatedSpace X] (U : X.Opens) (hU : IsCompact ((U : X.Opens) : Set X))
    (T : Set X) (hT : IsClosed T) (hTc : IsRetrocompact (Tᶜ : Set X))
    (E : DerivedModules X.toRingedSpace) (hE : HasQuasicoherentHomology X E)
    (P : DerivedModules (X.toRingedSpace.restrict U.isOpenEmbedding))
    (hP : IsPerfect.{u, u, u + 1} (X := X.toRingedSpace.restrict U.isOpenEmbedding) P)
    (hPT : AlgebraicGeometry.CohomologySupportedOn
      (structureSheafRing (X.toRingedSpace.restrict U.isOpenEmbedding))
      (Subtype.val ⁻¹' T) P)
    (α : P ⟶ (derivedRestrict (openInclusion X U)).obj E) :
    ∀ n : ℤ, ∃ (R : DerivedModules X.toRingedSpace) (β : R ⟶ E),
      (IsPerfect.{u, u, u + 1} (X := X.toRingedSpace) R ∧
          AlgebraicGeometry.CohomologySupportedOn (structureSheafRing X.toRingedSpace) T R) ∧
        ∃ (Q : DerivedModules (X.toRingedSpace.restrict U.isOpenEmbedding))
          (e : (derivedRestrict (openInclusion X U)).obj R ≅ P ⊞ Q),
          IsSumOfPositiveShifts P Q ∧
            (∀ i : ℤ, n ≤ i → IsZero ((DerivedCategory.homologyFunctor (SheafOfModules.{u}
              (structureSheafRing (X.toRingedSpace.restrict U.isOpenEmbedding))) i).obj Q)) ∧
              e.inv ≫ (derivedRestrict (openInclusion X U)).map β = biprod.fst ≫ α

Sources

• Section 36.13, Tag 08EC
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.exists_quasicoherentDerived_lift · AlgebraicGeometry.exists_quasicoherentDerived_plus_lift · AlgebraicGeometry.exists_quasicoherentDerived_minus_lift · AlgebraicGeometry.exists_quasicoherentDerived_bounded_lift · AlgebraicGeometry.essSurj_coherentDerivedBoundedRestrict · AlgebraicGeometry.exists_boundedAbove_finiteFree_lift · Stacks.DerivedQCoh.exists_pos_subsingleton_hom_singleFunctor_of_isFiniteLocallyFree · Stacks.DerivedQCoh.exists_window_subsingleton_hom_of_isPerfect_qcqs

Section36.14 Approximation by perfect complexes#

Section 36.14 of the Stacks Project, Tag 08EL. 6 tags here are carried by 11 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 08EM, a definition

Tag 08EM in the Stacks Project.

AlgebraicGeometry.HasPerfectApproximation, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/PerfectApproximation/Defs.lean, line 65.

Approximation holds for the triple (T, E, m): there is a perfect object of the derived category of 𝒪_X-modules, cohomologically supported on T, mapping to E by a map which is an isomorphism on cohomology in every degree above m and an epimorphism on cohomology in degree m.

abbrev HasPerfectApproximation (X : Scheme.{u}) (T : Set X)
    (E : DerivedCategory.{u + 1} X.Modules) (m : ℤ) : Prop

Tag 08EN, a definition

Tag 08EN in the Stacks Project.

AlgebraicGeometry.HasApproximationByPerfectComplexes, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/PerfectApproximation/Defs.lean, line 79.

The scheme X satisfies approximation by perfect complexes: for every closed subset T with retrocompact complement there is an integer r such that every sufficiently pseudo-coherent derived object with quasi-coherent cohomology supported on T in high degrees admits a perfect approximation.

abbrev HasApproximationByPerfectComplexes (X : Scheme.{u}) : Prop

Tag 08EP, a lemma

Tag 08EP in the Stacks Project.

AlgebraicGeometry.hasPerfectApproximation_of_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/Approximation/OpenSubscheme.lean, line 276.

Stacks Project, Tag 08EP. Let T be a closed subset of a scheme X contained in an open subscheme U, and let E be an object of the derived category of 𝒪_X-modules whose cohomology vanishes off T in every degree at least m. If approximation by a perfect complex holds for the restriction of E to U, relative to the preimage of T and the same degree m, then it holds for E.

The perfect object is the extension by zero j_! P of an approximation P over U: it is perfect because the derived pushforward of a perfect object with closed support is perfect (Stacks 08DP) and agrees there with extension by zero (Stacks 08DF), and its cohomology is supported on T because extension by zero preserves the support. The map to E is the extension by zero of the approximation, followed by the derived counit of j_! ⊣ j^*; the support hypothesis on E makes the underived counit invertible on each cohomology sheaf in degree at least m, and hence the derived counit invertible on cohomology there.

theorem hasPerfectApproximation_of_open
    (X : Scheme.{u}) (U : X.Opens) (T : Set X) (hT : IsClosed T) (hTU : T ⊆ (U : Set X))
    (E : DerivedCategory.{u + 1} X.Modules) (m : ℤ)
    (hApprox : HasPerfectApproximation (U : Scheme.{u})
      ((fun x : U ↦ (x.1 : X)) ⁻¹' T)
      ((RingedSpace.restrictModules X.toRingedSpace U).mapDerivedCategory.obj E) m)
    (hSupport : ∀ i : ℤ, m ≤ i → ∀ x : X, x ∉ T →
      IsZero (TopCat.Presheaf.stalk (X := X)
        (((DerivedCategory.homologyFunctor X.Modules i).obj E).val.presheaf) x)) :
    HasPerfectApproximation X T E m

Tag 08EQ, a lemma

Tag 08EQ in the Stacks Project.

AlgebraicGeometry.PerfectApproximation.approximationHolds_of_affineCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/PerfectApproximation/AffineCover.lean, line 386. The attribute's comment: “first assertion: approximation for triples on an affine scheme”.

Let X be an affine scheme. Approximation holds for every triple (T, E, m) with E an object of D_QCoh(𝒪_X) for which there is an integer r ≥ 0 such that

1. E is m-pseudo-coherent,
2. Hⁱ(E) is supported on T for i ≥ m - r + 1,
3. X ∖ T is the union of r affine opens U₁, …, U_r.

theorem approximationHolds_of_affineCover (X : Scheme.{u}) [IsAffine X] (T : Set X)
    {r : ℕ} (U : Fin r → X.Opens) (hU : ∀ k, IsAffineOpen (U k))
    (hcover : ((⨆ k, U k : X.Opens) : Set X) = Tᶜ)
    (E : DerivedCategory.{u + 1} X.Modules) (m : ℤ)
    (hqc : ∀ i : ℤ, ((DerivedCategory.homologyFunctor X.Modules i).obj E).IsQuasicoherent)
    (hpc : RingedSpace.IsPseudoCoherentFrom (X := X.toRingedSpace) E m)
    (hsupp : ∀ i : ℤ, m - (r : ℤ) + 1 ≤ i → ∀ x : X, x ∉ T →
      IsZero (TopCat.Presheaf.stalk (X := X)
        (((DerivedCategory.homologyFunctor X.Modules i).obj E).val.presheaf) x)) :
    ApproximationHolds X T E m

AlgebraicGeometry.PerfectApproximation.approximationByPerfectComplexes_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/PerfectApproximation/AffineScheme.lean, line 256. The attribute's comment: “second assertion: approximation by perfect complexes on an affine scheme”.

Approximation by perfect complexes holds on an affine scheme. This is the second assertion of [Stacks, Tag 08EQ]: the case of Spec R, AlgebraicGeometry.PerfectApproximation.approximationByPerfectComplexes_spec, transported along AlgebraicGeometry.Scheme.isoSpec.

theorem approximationByPerfectComplexes_of_isAffine (X : Scheme.{u}) [IsAffine X] :
    ApproximationByPerfectComplexes X

AlgebraicGeometry.PerfectApproximation.hasApproximationByPerfectComplexes_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/PerfectApproximation/AffineScheme.lean, line 264. The attribute's comment: “second assertion: approximation by perfect complexes on an affine scheme”.

Approximation by perfect complexes holds on an affine scheme, in the encoding of AlgebraicGeometry.HasApproximationByPerfectComplexes.

theorem hasApproximationByPerfectComplexes_of_isAffine (X : Scheme.{u}) [IsAffine X] :
    HasApproximationByPerfectComplexes X

Tag 08ER, a lemma

Tag 08ER in the Stacks Project.

AlgebraicGeometry.PerfectApproximation.hasApproximationByPerfectComplexes_of_sup_affine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/PerfectApproximation/QuasiCompactQuasiSeparated.lean, line 356.

Let X = U ∪ V be an open cover with U quasi-compact, V affine and U ∩ V quasi-compact. If approximation by perfect complexes holds on U, then it holds on X.

theorem hasApproximationByPerfectComplexes_of_sup_affine {X : Scheme.{u}} (U V : X.Opens)
    (hUV : U ⊔ V = ⊤) (hU : IsCompact (U : Set X)) (hV : IsAffineOpen V)
    (hUVc : IsCompact ((U : Set X) ∩ V)) (h : HasApproximationByPerfectComplexes U.toScheme) :
    HasApproximationByPerfectComplexes X

AlgebraicGeometry.PerfectApproximation.approximationByPerfectComplexes_sup_affine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/PerfectApproximation/UnionAffine.lean, line 124. The attribute's comment: “approximation by perfect complexes passes from a quasi-compact open to its union with an affine open meeting it in a quasi-compact open; nothing is carried, and the statement is at the standard derived category of the sheaves of modules of the scheme, the model the whole chapter is written at”.

[Stacks, Tag 08ER]. Let X be a scheme, let X = U ∪ V be an open covering with U quasi-compact, V affine and U ∩ V quasi-compact. If approximation by perfect complexes holds on U, then it holds on X.

The integer attached to a closed subset T with retrocompact complement is a + b, where a is the integer attached on U to T ∩ U and b the integer attached on V to T ∖ U, both taken nonnegative. Given a triple (T, E, m) satisfying the hypotheses for that integer, the approximation is built by induction on the largest degree in which the cohomology of E survives on U: below m - b the cohomology of E is supported on T ∖ U ⊆ V in all relevant degrees and [Stacks, Tag 08EQ] on V together with [Stacks, Tag 08EP] finishes, while above it the glueing step of [Stacks, Tag 09IM] turns an approximation on U in that degree into a perfect object on X surjective there, and the cone of the resulting map survives on U in one degree fewer.

theorem approximationByPerfectComplexes_sup_affine (X : Scheme.{u}) (U V : X.Opens)
    (hVaff : IsAffineOpen V) (hcover : U ⊔ V = ⊤)
    (hUc : IsCompact (U : Set X)) (hUVc : IsCompact ((U ⊓ V : X.Opens) : Set X))
    (hUapp : ApproximationByPerfectComplexes (U : Scheme.{u})) :
    ApproximationByPerfectComplexes X

AlgebraicGeometry.PerfectApproximation.hasApproximationByPerfectComplexes_sup_affine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/PerfectApproximation/UnionAffine.lean, line 287. The attribute's comment: “the same statement in the second encoding of the property of Tag 08EN; nothing is carried, and the derived category is the standard model, as in the first encoding”.

[Stacks, Tag 08ER], in the encoding of AlgebraicGeometry.HasApproximationByPerfectComplexes.

theorem hasApproximationByPerfectComplexes_sup_affine (X : Scheme.{u}) (U V : X.Opens)
    (hVaff : IsAffineOpen V) (hcover : U ⊔ V = ⊤)
    (hUc : IsCompact (U : Set X)) (hUVc : IsCompact ((U ⊓ V : X.Opens) : Set X))
    (hUapp : HasApproximationByPerfectComplexes (U : Scheme.{u})) :
    HasApproximationByPerfectComplexes X

Tag 08ES, a theorem

Tag 08ES in the Stacks Project.

AlgebraicGeometry.PerfectApproximation.approximationByPerfectComplexes_of_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/PerfectApproximation/Qcqs.lean, line 65. The attribute's comment: “approximation by perfect complexes on a quasi-compact quasi-separated scheme; nothing is carried, and the statement is at the standard derived category of the sheaves of modules of the scheme, the model the whole chapter is written at”.

[Stacks, Tag 08ES]. Approximation by perfect complexes holds on every quasi-compact and quasi-separated scheme.

The induction principle of [Stacks, Tag 08DR] applied to the property that approximation holds on an open subscheme: the affine case is [Stacks, Tag 08EQ] and the union step is [Stacks, Tag 08ER].

theorem approximationByPerfectComplexes_of_qcqs (X : Scheme.{u}) [CompactSpace X]
    [QuasiSeparatedSpace X] : ApproximationByPerfectComplexes X

AlgebraicGeometry.PerfectApproximation.hasApproximationByPerfectComplexes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/PerfectApproximation/QuasiCompactQuasiSeparated.lean, line 485.

Approximation by perfect complexes holds on every quasi-compact and quasi-separated scheme.

theorem hasApproximationByPerfectComplexes (X : Scheme.{u}) [CompactSpace X]
    [QuasiSeparatedSpace X] : HasApproximationByPerfectComplexes X

Sources

• Section 36.14, Tag 08EL
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.HasPerfectApproximation · AlgebraicGeometry.HasApproximationByPerfectComplexes · AlgebraicGeometry.hasPerfectApproximation_of_open · AlgebraicGeometry.PerfectApproximation.approximationHolds_of_affineCover · AlgebraicGeometry.PerfectApproximation.approximationByPerfectComplexes_of_isAffine · AlgebraicGeometry.PerfectApproximation.hasApproximationByPerfectComplexes_of_isAffine · AlgebraicGeometry.PerfectApproximation.hasApproximationByPerfectComplexes_of_sup_affine · AlgebraicGeometry.PerfectApproximation.approximationByPerfectComplexes_sup_affine

Section36.15 Generating derived categories#

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

Tag 09IQ, a lemma

Tag 09IQ in the Stacks Project.

Stacks.DerivedQCoh.AnyModel.exists_isPerfect_retract_derivedRestrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/AnyModel/PerfectSummandOfRestriction.lean, line 79.

[Stacks, Tag 09IQ]. Let X be a quasi-compact quasi-separated scheme and U ⊆ X a quasi-compact open. Every perfect object P of D(𝒪_U) is a direct summand -- a retract -- of the restriction to U of a perfect object of D(𝒪_X).

This is [Stacks, Tag 09IM] with T the whole space and the zero object, transported from the model that tag is proved at to the locally small one.

theorem exists_isPerfect_retract_derivedRestrict {X : Scheme.{u}} [CompactSpace X]
    [QuasiSeparatedSpace X] (U : X.Opens) (hU : IsCompact (U : Set X))
    (P : DerivedCategory U.toScheme.Modules)
    (hP : IsPerfect (X := ringedSpace U.toScheme) P) :
    ∃ R : DerivedCategory X.Modules, IsPerfect (X := ringedSpace X) R ∧
      ∃ (i : P ⟶ (Stacks.Duality.OpenImmersion.derivedRestrict U.ι).obj R)
        (p : (Stacks.Duality.OpenImmersion.derivedRestrict U.ι).obj R ⟶ P), i ≫ p = 𝟙 P

Stacks.DerivedQCoh.OpenLift.exists_isPerfectComplex_retract_of_isPerfect_of_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/OpenLift/QcqsSummandOfRestriction.lean, line 459. The attribute's comment: “the perfect object on X exhibited by a perfect complex; any model of D(O_U)”.

[Stacks, Tag 09IQ]. Let X be a quasi-compact and quasi-separated scheme and U ⊆ X a quasi-compact open. Every perfect object P of D(𝒪_U) is a direct summand -- a retract -- of the restriction to U of a perfect object of D(𝒪_X), here exhibited by a perfect complex M of 𝒪_X-modules: P is a retract of the class of M|_U.

The derived category of 𝒪_U is an arbitrary model, and none is needed on X.

theorem exists_isPerfectComplex_retract_of_isPerfect_of_qcqs (X : Scheme.{u}) [CompactSpace X]
    [QuasiSeparatedSpace X] (U : X.Opens) (hU : IsCompact (U : Set X))
    [hd : HasDerivedCategory.{d₁} U.toScheme.Modules] (P : DerivedCategory U.toScheme.Modules)
    (hP : @IsPerfect U.toScheme.toRingedSpace hd P) :
    ∃ M : CochainComplex X.Modules ℤ, IsPerfectComplex (X := X.toRingedSpace) M ∧
      Nonempty (Retract P (DerivedCategory.Q.obj
        (((Scheme.Modules.restrictFunctor U.ι).mapHomologicalComplex (ComplexShape.up ℤ)).obj
          M)))

Stacks.DerivedQCoh.OpenLift.exists_isPerfect_retract_derivedRestrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/OpenLift/QcqsSummandOfRestriction.lean, line 484. The attribute's comment: “in D(O_X), at any models of the two derived categories”.

[Stacks, Tag 09IQ], in D(𝒪_X). Let X be a quasi-compact and quasi-separated scheme and U ⊆ X a quasi-compact open. Every perfect object P of D(𝒪_U) is a retract of the restriction to U of a perfect object R of D(𝒪_X), at any models of the two derived categories, in independent universes; restriction is j^* for the open immersion j : U ⟶ X, which Stacks.Duality.OpenImmersion.derivedRestrict names when the two universes agree.

theorem exists_isPerfect_retract_derivedRestrict (X : Scheme.{u}) [CompactSpace X]
    [QuasiSeparatedSpace X] (U : X.Opens) (hU : IsCompact (U : Set X))
    [hU' : HasDerivedCategory.{d₁} U.toScheme.Modules] [hX : HasDerivedCategory.{d₂} X.Modules]
    (P : DerivedCategory U.toScheme.Modules) (hP : @IsPerfect U.toScheme.toRingedSpace hU' P) :
    ∃ R : DerivedCategory X.Modules, @IsPerfect X.toRingedSpace hX R ∧
      Nonempty (Retract P ((Scheme.Modules.restrictFunctor U.ι).mapDerivedCategory.obj R))

Stacks.DerivedQCoh.OpenLift.exists_isPerfectComplex_retract_restrict_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/OpenLift/SummandOfRestriction.lean, line 76. The attribute's comment: “for X affine; the quasi-compact quasi-separated case is deduced in the source from 09IM, whose induction over an affine cover needs 08EK and 08EH, neither of which this library has”.

[Stacks, Tag 09IQ] for X affine. Let X be an affine scheme and U ⊆ X a quasi-compact open. Every perfect object P of D(𝒪_U) is a direct summand -- a retract -- of the restriction to U of a perfect complex of 𝒪_X-modules.

theorem exists_isPerfectComplex_retract_restrict_of_isPerfect
    (X : Scheme.{u}) [IsAffine X] (U : X.Opens) (hU : IsCompact (U : Set X))
    (P : DerivedCategory U.toScheme.Modules)
    (hP : IsPerfect (X := U.toScheme.toRingedSpace) P) :
    ∃ M : CochainComplex (OXMod.{u, u, u} X.toRingedSpace) ℤ,
      IsPerfectComplex M ∧
      Nonempty (Retract P (DerivedCategory.Q.obj
        (((AlgebraicGeometry.RingedSpace.restrictModules.{u, u} X.toRingedSpace
          U).mapHomologicalComplex (ComplexShape.up ℤ)).obj M)))

Stacks.Duality.OpenImmersion.exists_isPerfect_retract_derivedRestrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/PerfectApproximation/SummandOfRestriction.lean, line 61.

[Stacks, Tag 09IQ]. Let X be a quasi-compact quasi-separated scheme and U ⊆ X a quasi-compact open. Every perfect object P of D(𝒪_U) is a direct summand -- a retract -- of the restriction to U of a perfect object R of D(𝒪_X).

theorem exists_isPerfect_retract_derivedRestrict (X : Scheme.{u}) [CompactSpace X]
    [QuasiSeparatedSpace X] (U : X.Opens) (hU : IsCompact (U : Set X))
    (P : DerivedCategory U.toScheme.Modules)
    (hP : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := U.toScheme.toRingedSpace) P) :
    ∃ R : DerivedCategory X.Modules,
      Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace) R ∧
        Nonempty (Retract P ((derivedRestrict U.ι).obj R))

Tag 09IR, a lemma

Tag 09IR in the Stacks Project.

Stacks.Koszul.Truncation.hom_koszulObject_eq_zero_of_isIso_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/KoszulOrthogonality/AffineSituation.lean, line 186. The attribute's comment: “(1) implies (2)”.

[Stacks, Tag 09IR], the implication "(1) implies (2)". In Situation [Stacks, Tag 08CZ], if the canonical map E ⟶ Rj_*(E|_U) is invertible then Hom_{D(𝒪_X)}(K[n], E) = 0 for every n ∈ ℤ, where K is the sheafified Koszul complex on f₁, …, f_r.

There is nothing to assume. The Koszul object restricts to zero on U = ⋃ᵢ D(f_i) by Stacks.Koszul.OpenComplement.isZero_derivedRestrict_koszulObject, so a morphism K⟦n⟧ ⟶ Rj_* Z is adjoint to a morphism out of (j^* K)⟦n⟧ = 0 and hence zero; and E is isomorphic to Rj_*(E|_U) through the unit, while the condition is closed under isomorphism.

theorem hom_koszulObject_eq_zero_of_isIso_unit
    (E : DerivedCategory (Spec (CommRingCat.of A)).Modules)
    (h : IsIso ((derivedRestrictPushforwardAdjunction (openComplement f).ι).unit.app E)) :
    ∀ (n : ℤ) (g : (koszulObject f)⟦n⟧ ⟶ E), g = 0

Stacks.Koszul.Truncation.isIso_unit_of_hom_koszulObject_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/KoszulOrthogonality/AffineSituation.lean, line 261. The attribute's comment: “(2) implies (1)”.

[Stacks, Tag 09IR], the implication "(2) implies (1)". In Situation [Stacks, Tag 08CZ], let E be an object of D_QCoh(𝒪_X), that is one whose cohomology sheaves are quasi-coherent. If Hom_{D(𝒪_X)}(K[n], E) = 0 for every n ∈ ℤ then the canonical map E ⟶ Rj_*(E|_U) is invertible.

Take a distinguished triangle E ⟶ Rj_*(E|_U) ⟶ M ⟶ E⟦1⟧; the claim is that M = 0. Three things are known about M.

• M|_U = 0, because j^* of the unit at E is a section of the counit at E|_U, which is invertible — Rj_* is fully faithful along an open immersion.
• Hom(K⟦n⟧, M) = 0 for every n, because right orthogonality to the shifts of K is a triangulated subcategory and both E and Rj_*(E|_U) lie in it, the latter for the formal reason that j^* K = 0.
• The cohomology sheaves of M are quasi-coherent, because those of E are and Rj_* preserves quasi-coherent cohomology along a quasi-compact open immersion ([Stacks, Tag 08D5]).

Those three force M = 0 by Stacks.Koszul.Truncation.isZero_of_forall_hom_koszulObject_eq_zero, which is the source's argument: pass to D(A) along the affine comparison of [Stacks, Tag 06Z0] and apply the Koszul detection statement over the ring. A distinguished triangle whose third vertex vanishes has invertible first morphism.

theorem isIso_unit_of_hom_koszulObject_eq_zero
    (E : DerivedCategory (Spec (CommRingCat.of A)).Modules)
    (hE : DerivedCategoryB.derivedCategoryB (A := (Spec (CommRingCat.of A)).Modules)
      (SheafOfModules.isQuasicoherent (Spec (CommRingCat.of A)).ringCatSheaf) E)
    (h : ∀ (n : ℤ) (g : (koszulObject f)⟦n⟧ ⟶ E), g = 0) :
    IsIso ((derivedRestrictPushforwardAdjunction (openComplement f).ι).unit.app E)

Tag 09IS, a theorem

Tag 09IS in the Stacks Project.

Stacks.DerivedQCoh.AnyModel.hasPerfectGenerator_of_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/PerfectGeneratorInduction.lean, line 415. The attribute's comment: “the generator, in the ObjectProperty.IsWeakTriangulatedGenerator spelling”.

[Stacks, Tag 09IS], the theorem of Bondal and Van den Bergh, in the form that D_QCoh(𝒪_X) is weakly generated by a single perfect object: on a quasi-compact quasi-separated scheme the property Stacks.DerivedQCoh.AnyModel.HasPerfectGenerator holds.

This is the induction principle [Stacks, Tag 08DR] — in the clause induction_top for the whole space — applied to Stacks.DerivedQCoh.AnyModel.HasPerfectGeneratorOn, whose two clauses are Stacks.DerivedQCoh.AnyModel.hasPerfectGeneratorOn_of_isAffineOpen and Stacks.DerivedQCoh.AnyModel.hasPerfectGeneratorOn_sup; the conclusion is read at the identity of X, an open immersion whose image is all of X.

theorem hasPerfectGenerator_of_qcqs (X : Scheme.{u}) [CompactSpace X] [QuasiSeparatedSpace X] :
    HasPerfectGenerator X

Stacks.DerivedQCoh.AnyModel.exists_isPerfect_isZero_iff_forall_hom_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/PerfectGeneratorInduction.lean, line 431.

[Stacks, Tag 09IS], the theorem of Bondal and Van den Bergh, in the source's own words. Let X be a quasi-compact quasi-separated scheme. There is a perfect object P of D(𝒪_X) such that for every object E of D_QCoh(𝒪_X) the following are equivalent: E = 0, and Hom_{D(𝒪_X)}(P⟦n⟧, E) = 0 for all n : ℤ.

This is Stacks.DerivedQCoh.AnyModel.hasPerfectGenerator_of_qcqs read in the ambient derived category by CategoryTheory.ObjectProperty.isWeakTriangulatedGenerator_singleton_iff; the converse implication holds for any object, a morphism into a zero object being zero.

theorem exists_isPerfect_isZero_iff_forall_hom_eq_zero (X : Scheme.{u}) [CompactSpace X]
    [QuasiSeparatedSpace X] :
    ∃ P : DerivedCategory X.Modules, IsPerfect (X := X.toRingedSpace) P ∧
      ∀ E : DerivedCategory X.Modules, DerivedCategoryB.derivedCategoryB (A := X.Modules)
        (SheafOfModules.isQuasicoherent X.ringCatSheaf) E →
          (IsZero E ↔ ∀ (n : ℤ) (g : P⟦n⟧ ⟶ E), g = 0)

Stacks.Duality.AffineGeneration.exists_isCompactObject_isWeakTriangulatedGenerator_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactGeneration/AffineQuasiCoherent.lean, line 370. The attribute's comment: “FOR AN AFFINE SCHEME ONLY, and with the generator exhibited as a COMPACT rather than a perfect object. The source's induction over the quasi-compact opens, Tag 08DR, is available and so is its generation step, but two of its inputs are not: Tag 09IQ at a quasi-compact quasi-separated scheme (the library has only the affine case, Stacks.DerivedQCoh.OpenLift.exists_isPerfectComplex_retract_restrict_of_isPerfect; the source deduces the rest from Tag 09IM, needing Tags 08EK and 08EH, none of the three being present), and the implication perfect implies compact of Tag 09M1, which the source draws from the Hom formula of Tag 08DQ, absent. The generator here is the image of the regular module in degree zero under the comparison of Tag 06Z0, that is the structure sheaf in degree zero, which is the source's generator for an affine scheme; that it is perfect as well as compact is Tag 07LT carried across Tag 06Z0, which is not done here because the library's statement of the affine case of Tag 09M1, AlgebraicGeometry.isCompactObject_iff_isPerfect_spec, is pinned to CategoryTheory.HasDerivedCategory.standard and so speaks of a different derived category. Compactness is what the consumers of the tag ask for”.

[Stacks, Tag 09IS] for an affine scheme. D_QCoh(𝒪_X) is generated by a single compact object: there is an object P of D_QCoh(𝒪_X) which is compact and such that an object of D_QCoh(𝒪_X) receiving only zero morphisms from the shifts of P is zero.

The object produced is the image under Stacks.Duality.AffineGeneration.affineComparison of the regular module in degree zero, which is the structure sheaf in degree zero — the source's own generator for an affine scheme. See the implementation notes for why it is exhibited as compact rather than as perfect, and for what separates this from the tag's quasi-compact quasi-separated statement.

theorem exists_isCompactObject_isWeakTriangulatedGenerator_of_isAffine (X : Scheme.{u})
    [IsAffine X] :
    ∃ P : (DerivedCategoryB.derivedCategoryB
        (SheafOfModules.isQuasicoherent X.ringCatSheaf)).FullSubcategory,
      IsCompactObject.{u} P ∧ (ObjectProperty.singleton P).IsWeakTriangulatedGenerator

Stacks.Duality.AffineGeneration.isCompactlyGenerated_derivedQuasiCoherent_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactGeneration/AffineQuasiCoherent.lean, line 397. The attribute's comment: “FOR AN AFFINE SCHEME ONLY, in the IsCompactlyGenerated form of Tag 09SQ and with the generator exhibited as compact rather than perfect; see Stacks.Duality.AffineGeneration.exists_isCompactObject_isWeakTriangulatedGenerator_of_isAffine for the full caveat”.

[Stacks, Tag 09IS] for an affine scheme, in the form [Stacks, Tag 09SQ] defines and Brown representability consumes. D_QCoh(𝒪_X) is compactly generated: the one-element family consisting of the generator of Stacks.Duality.AffineGeneration.exists_isCompactObject_isWeakTriangulatedGenerator_of_isAffine is a family of compact objects which jointly generate.

The category is spelled over AlgebraicGeometry.SheafOfModules X.ringCatSheaf, which is the spelling the hypothesis of [Stacks, Tag 0CR0] uses.

theorem isCompactlyGenerated_derivedQuasiCoherent_of_isAffine (X : Scheme.{u}) [IsAffine X] :
    IsCompactlyGenerated.{u}
      (DerivedCategoryB.derivedCategoryB
        (SheafOfModules.isQuasicoherent X.ringCatSheaf)).FullSubcategory

Stacks.Duality.AffineGeneration.isCompactlyGenerated_quasiCoherentDerivedCategory_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactGeneration/AffineQuasiCoherent.lean, line 413. The attribute's comment: “FOR AN AFFINE SCHEME ONLY, in the IsCompactlyGenerated form of Tag 09SQ at the Scheme.Modules spelling of the category, which is the one Tag 0A9E's statement uses; see Stacks.Duality.AffineGeneration.exists_isCompactObject_isWeakTriangulatedGenerator_of_isAffine for the full caveat”.

[Stacks, Tag 09IS] for an affine scheme, at the spelling of D_QCoh(𝒪_X) over AlgebraicGeometry.Scheme.Modules X — the one the statement of [Stacks, Tag 0A9E] uses. The two spellings are the same type with separately declared HasDerivedCategory instances; see the implementation notes.

theorem isCompactlyGenerated_quasiCoherentDerivedCategory_of_isAffine (X : Scheme.{u})
    [IsAffine X] :
    IsCompactlyGenerated.{u} (Stacks.Duality.quasiCoherentDerivedCategory X)

Stacks.Duality.QuasiAffineGeneration.exists_isCompactObject_isWeakTriangulatedGenerator_of_isQuasiAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactGeneration/QuasiAffineQuasiCoherent.lean, line 334. The attribute's comment: “FOR A QUASI-AFFINE SCHEME, and with the generator exhibited as a COMPACT rather than a perfect object. This weakens the affine hypothesis of Stacks.Duality.AffineGeneration.exists_isCompactObject_isWeakTriangulatedGenerator_of_isAffine but does NOT reach the tag's quasi-compact quasi-separated statement. The route is the reverse of the source's: compact generation passes DOWN from a scheme to a quasi-compact open of it, by Stacks.Duality.OpenImmersion.isCompactlyGenerated_quasiCoherentDerivedCategory_of_isOpenImmersion, so from the affine case it reaches exactly the schemes with a quasi-compact open immersion into an affine scheme, the quasi-affine ones. The source's own induction over the quasi-compact opens, Tag 08DR, goes the other way and still needs Tag 09IQ at a quasi-compact quasi-separated scheme and the implication perfect implies compact of Tag 09M1, neither of which is in the library; see the implementation notes of StacksFrontier/AlgebraicGeometry/Duality/CompactGeneration/AffineQuasiCoherent.lean. Nothing here needs either: the generator is compact by construction and compactness is what the consumers of the tag ask for”.

[Stacks, Tag 09IS] for a quasi-affine scheme. D_QCoh(𝒪_X) is generated by a single compact object.

A quasi-affine scheme is quasi-compact and X ⟶ Spec Γ(X, ⊤) is an open immersion ([Stacks, Tag 01P6], Mathlib's AlgebraicGeometry.Scheme.IsQuasiAffine), so this is the affine case AffineGeneration.exists_isCompactObject_isWeakTriangulatedGenerator_of_isAffine restricted along that immersion by OpenImmersion.exists_isCompactObject_isWeakTriangulatedGenerator_of_isOpenImmersion. The generator is therefore the restriction to X of the structure sheaf of Spec Γ(X, ⊤) in degree zero, which is 𝒪_X in degree zero — the source's own generator.

theorem exists_isCompactObject_isWeakTriangulatedGenerator_of_isQuasiAffine (X : Scheme.{u})
    [X.IsQuasiAffine] :
    ∃ P : Stacks.Duality.quasiCoherentDerivedCategory X,
      IsCompactObject.{u} P ∧ (ObjectProperty.singleton P).IsWeakTriangulatedGenerator

Stacks.Duality.QuasiAffineGeneration.isCompactlyGenerated_quasiCoherentDerivedCategory_of_isQuasiAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactGeneration/QuasiAffineQuasiCoherent.lean, line 350. The attribute's comment: “FOR A QUASI-AFFINE SCHEME, in the IsCompactlyGenerated form of Tag 09SQ at the Scheme.Modules spelling of the category, which is the one Tag 0A9E's statement uses; see Stacks.Duality.QuasiAffineGeneration.exists_isCompactObject_isWeakTriangulatedGenerator_of_isQuasiAffine for the full caveat”.

[Stacks, Tag 09IS] for a quasi-affine scheme, in the form [Stacks, Tag 09SQ] defines and Brown representability consumes, at the spelling of D_QCoh(𝒪_X) over AlgebraicGeometry.Scheme.Modules X — the one the statement of [Stacks, Tag 0A9E] uses.

theorem isCompactlyGenerated_quasiCoherentDerivedCategory_of_isQuasiAffine (X : Scheme.{u})
    [X.IsQuasiAffine] :
    IsCompactlyGenerated.{u} (Stacks.Duality.quasiCoherentDerivedCategory X)

Stacks.Duality.QuasiAffineGeneration.isCompactlyGenerated_derivedQuasiCoherent_of_isQuasiAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactGeneration/QuasiAffineQuasiCoherent.lean, line 366. The attribute's comment: “FOR A QUASI-AFFINE SCHEME, in the IsCompactlyGenerated form of Tag 09SQ at the SheafOfModules spelling of the category, which is the one Tag 0CR0's hypothesis uses; see Stacks.Duality.QuasiAffineGeneration.exists_isCompactObject_isWeakTriangulatedGenerator_of_isQuasiAffine for the full caveat”.

[Stacks, Tag 09IS] for a quasi-affine scheme, at the spelling of D_QCoh(𝒪_X) over AlgebraicGeometry.SheafOfModules X.ringCatSheaf — the one the hypothesis of [Stacks, Tag 0CR0] uses. The two spellings are the same type with separately declared HasDerivedCategory instances.

theorem isCompactlyGenerated_derivedQuasiCoherent_of_isQuasiAffine (X : Scheme.{u})
    [X.IsQuasiAffine] :
    IsCompactlyGenerated.{u}
      (DerivedCategoryB.derivedCategoryB
        (SheafOfModules.isQuasicoherent X.ringCatSheaf)).FullSubcategory

Stacks.SheafOfModules.exists_isPerfect_generator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/QcqsPerfectGenerator.lean, line 292.

[Stacks, Tag 09IS]. Let X be a quasi-compact and quasi-separated scheme. Then D_QCoh(𝒪_X) has a perfect generator: there is a perfect object G of D(𝒪_X) such that every object K of D(𝒪_X) with quasi-coherent cohomology sheaves which receives no nonzero morphism from any shift G⟦n⟧ is zero.

This is Stacks.SheafOfModules.exists_isPerfect_generator_modules read in the spelling StructureSheafModules X.sheaf with perfectness for the ringed site of opens, the spelling of the generator hypotheses of Stacks 0GEN in DetectingBoundedAboveGenerator; the two notions of perfectness agree by Stacks.Cohomology.PerfectComplexes.isPerfect_ringedSite_of_isPerfect.

The proof is the source's: induction over a finite affine cover produces finitely many compact generators of D_QCoh(𝒪_X) (Stacks.Duality.QcqsGeneration.exists_finite_compact_generators), compact objects of D_QCoh(𝒪_X) are perfect (Stacks.Duality.QcqsPerfect.isPerfect_of_isCompactObject_of_qcqs), and their direct sum is a single perfect generator.

theorem exists_isPerfect_generator {X : Scheme.{u}}
    [HasSheafify (Opens.grothendieckTopology X.toPresheafedSpace.carrier) AddCommGrpCat.{u}]
    [(Opens.grothendieckTopology X.toPresheafedSpace.carrier).WEqualsLocallyBijective
      AddCommGrpCat.{u}]
    (hqc : CompactSpace X) (hqs : QuasiSeparatedSpace X) :
    ∃ G : DerivedCategory (StructureSheafModules X.sheaf), (ringedSite X.sheaf).IsPerfect G ∧
      ∀ K : DerivedCategory (StructureSheafModules X.sheaf),
        (∀ i : ℤ, ((DerivedCategory.homologyFunctor (StructureSheafModules X.sheaf) i).obj
          K).IsQuasicoherent) →
        (∀ (n : ℤ) (f : G⟦n⟧ ⟶ K), f = 0) → IsZero K

Tag 0A9A, a lemma

Tag 0A9A in the Stacks Project.

Stacks.Duality.SupportedGeneration.exists_isPerfect_quasiCoherentSupported_isWeakGenerator_of_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactGeneration/QcqsPerfectGenerator.lean, line 282.

[Stacks, Tag 0A9A] (Rouquier, Theorem 6.8). Let X be a quasi-compact and quasi-separated scheme and let T ⊆ X be a closed subset such that X ∖ T is quasi-compact. Then D_{QCoh,T}(𝒪_X) is generated by a single perfect object: there is a perfect object P of D(𝒪_X) lying in D_{QCoh,T}(𝒪_X) such that every object E of D_{QCoh,T}(𝒪_X) with Hom(P[n], E) = 0 for all n ∈ ℤ is zero.

Generation is [Stacks, Tag 09SJ] for D_{QCoh,T}(𝒪_X), written out; morphisms of the full subcategory are morphisms of D(𝒪_X). The generator is the compact one of Stacks.Duality.SupportedGeneration.hasCompactSupportedGenerators, built by the induction of the source, and it is perfect by Stacks.Duality.SupportedGeneration.isPerfect_of_isCompactObject.

theorem exists_isPerfect_quasiCoherentSupported_isWeakGenerator_of_qcqs (X : Scheme.{u})
    [CompactSpace X] [QuasiSeparatedSpace X] (T : Set X) (hT : IsClosed T) (hTc : IsCompact Tᶜ) :
    ∃ P : DerivedCategory X.Modules,
      AlgebraicGeometry.RingedSpace.IsPerfect (X := X.toRingedSpace) P ∧
        quasiCoherentSupported X T P ∧
        ∀ E : DerivedCategory X.Modules, quasiCoherentSupported X T E →
          (∀ (n : ℤ) (g : P⟦n⟧ ⟶ E), g = 0) → IsZero E

Stacks.Rouquier.exists_isPerfect_isWeakTriangulatedGenerator_supported, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Rouquier/SupportedGeneratorQcqs.lean, line 128. The attribute's comment: “the generator, in the ObjectProperty.IsWeakTriangulatedGenerator spelling”.

The theorem of Rouquier. Let X be a quasi-compact quasi-separated scheme and let T ⊆ X be closed with quasi-compact complement. Then D_{QCoh,T}(𝒪_X) has a weak triangulated generator which is perfect as an object of D(𝒪_X).

theorem exists_isPerfect_isWeakTriangulatedGenerator_supported (X : Scheme.{u}) [CompactSpace X]
    [QuasiSeparatedSpace X] (T : Set X) (hT : IsClosed T) (hTc : IsCompact Tᶜ) :
    ∃ G : Stacks.Duality.QuasiCoherentSupportedDerivedCategory X T,
      IsPerfect (X := X.toRingedSpace) G.obj ∧
        (ObjectProperty.singleton G).IsWeakTriangulatedGenerator

Stacks.Rouquier.exists_isPerfect_isZero_iff_forall_hom_eq_zero_supported, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Rouquier/SupportedGeneratorQcqs.lean, line 145.

The theorem of Rouquier, with the generator condition spelled out. Let X be a quasi-compact quasi-separated scheme and let T ⊆ X be closed with quasi-compact complement. There is a perfect object P of D(𝒪_X) such that for every object E of D_{QCoh,T}(𝒪_X) the following are equivalent: E = 0, and Hom_{D(𝒪_X)}(P⟦n⟧, E) = 0 for all n : ℤ.

theorem exists_isPerfect_isZero_iff_forall_hom_eq_zero_supported (X : Scheme.{u}) [CompactSpace X]
    [QuasiSeparatedSpace X] (T : Set X) (hT : IsClosed T) (hTc : IsCompact Tᶜ) :
    ∃ P : DerivedCategory X.Modules, IsPerfect (X := X.toRingedSpace) P ∧
      ∀ E : DerivedCategory X.Modules, Stacks.Duality.quasiCoherentSupported X T E →
        (IsZero E ↔ ∀ (n : ℤ) (g : P⟦n⟧ ⟶ E), g = 0)

Sources

• Section 36.15, Tag 09IP
• AxiomMath/Stacks at 5ed82d14

LeanStacks.DerivedQCoh.AnyModel.exists_isPerfect_retract_derivedRestrict · Stacks.DerivedQCoh.OpenLift.exists_isPerfectComplex_retract_of_isPerfect_of_qcqs · Stacks.DerivedQCoh.OpenLift.exists_isPerfect_retract_derivedRestrict · Stacks.DerivedQCoh.OpenLift.exists_isPerfectComplex_retract_restrict_of_isPerfect · Stacks.Duality.OpenImmersion.exists_isPerfect_retract_derivedRestrict · Stacks.Koszul.Truncation.hom_koszulObject_eq_zero_of_isIso_unit · Stacks.Koszul.Truncation.isIso_unit_of_hom_koszulObject_eq_zero · Stacks.DerivedQCoh.AnyModel.hasPerfectGenerator_of_qcqs

Section36.16 An example generator#

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

Tag 0BQR, a lemma

Tag 0BQR in the Stacks Project.

Stacks.AmpleNonvanishing.exists_nonzero_hypercohomology_tensorPower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleNonvanishing/Derived.lean, line 223. The attribute's comment: “the general derived statement: K is an arbitrary nonzero object of D_QCoh(O_X), the tensor product is the derived one of Tag 06YH with a tensor power of L in degree zero, and the cohomology is the derived hypercohomology of Tag 08JA in degree p. The hypothesis is stated at the locally small model of D(O_X), the only model Tag 08DB is available at, and the conclusion at the standard model, the only model Tag 08JA is available at; the object in the conclusion is K itself, Stacks.Injectives.grothendieckModelEquiv being the identity on objects. The degree-zero module case, which this does not subsume because it carries an explicit witness, is the separate carrier Stacks.AmpleNonvanishingChart.exists_twistedSection_restrict_eq_tensorSection”.

[Stacks, Tag 0BQR]. Let X be a scheme, L an ample invertible 𝒪_X-module and K a nonzero object of D_QCoh(𝒪_X). Then there are an exponent n and a degree p with

H^p(X, K ⊗^𝐋_{𝒪_X} L^{⊗ n}[0]) ≠ 0.

The tensor product is the derived tensor product of [Stacks, Tag 06YH] with the n-th tensor power of L placed in degree zero, and the cohomology is the derived hypercohomology, the degree-p homology of unbounded derived global sections. The object the conclusion is about is K itself, read in the standard model of the derived category; see the implementation notes on the two models.

theorem exists_nonzero_hypercohomology_tensorPower (X : Scheme.{u}) (L : X.Modules)
    [IsInvertibleModule X L] (hL : IsAmple X L)
    (K : (@DerivedCategoryB.derivedCategoryB X.Modules _ _
      (AlgebraicGeometry.Scheme.Modules.hasDerivedCategory X)
      (SheafOfModules.isQuasicoherent X.ringCatSheaf)).FullSubcategory)
    (hK : ¬ IsZero K) :
    ∃ (n : ℕ) (p : ℤ),
      ¬ IsZero ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} p).obj
        ((derivedModuleGlobalSections
            (Stacks.SheafOfModules.ringedSite X.toRingedSpace.sheaf)).obj
          (((Stacks.Cohomology.TorAmplitude.derTensor X.toRingedSpace).tensor.obj
              ((Stacks.Injectives.grothendieckModelEquiv X.Modules).inverse.obj K.1)).obj
            (DerivedCategory.Q.obj
              ((HomologicalComplex.single (Stacks.DerivedTensor.RingedSite.Modules X.sheaf)
                (ComplexShape.up ℤ) 0).obj (tensorPowModule X L (n : ℤ)))))))

Stacks.AmpleNonvanishingChart.exists_twistedSection_restrict_eq_tensorSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleNonvanishing/TwistedSectionChart.lean, line 141. The attribute's comment: “run at a quasi-coherent module rather than at an object of D_QCoh(O_X) in a degree: Gamma(X, F tensor L^p) is nonzero, witnessed by an explicit tau. The derived-category form is a separate assertion; see the module docstring”.

[Stacks, Tag 0BQR] for a quasi-coherent module. For L an ample invertible 𝒪_X-module and F a nonzero quasi-coherent 𝒪_X-module there are an exponent p, a global section σ of L ^⊗ p with affine nonvanishing open U = X_σ, a nonzero section t of F over U, and a nonzero global section τ of F ⊗ L ^⊗ p with τ|_U = t ⊗ σ|_U.

These are the five steps of the source argument run on a module instead of on a complex: the point with nonzero stalk, the affine chart of ampleness, the nonzero section on it, the surjectivity half of [Stacks, Tag 01PW], and — for τ ≠ 0 — the whiskered clause 2 of [Stacks, Tag 01CY] in the form Stacks.SectionProduct.eq_zero_of_tensorSection_eq_zero: over an open inside X_σ the product with σ kills no section of F, so τ|_U = t ⊗ σ|_U with t ≠ 0 forces τ ≠ 0.

theorem exists_twistedSection_restrict_eq_tensorSection {X : Scheme.{u}} (L : X.Modules)
    [IsInvertibleModule X L] (hL : IsAmple X L) (F : X.Modules) [F.IsQuasicoherent]
    (hF : ¬ IsZero F) :
    ∃ (p : ℕ) (σ : Γ(tensorPowModule X L (p : ℤ), ⊤)) (U : X.Opens)
      (τ : Γ(F ⊗ tensorPowModule X L (p : ℤ), ⊤)) (t : Γ(F, U)),
      U = Stacks.AmpleTheory.powNonvanishingOpen X L p σ ∧ IsAffineOpen U ∧ t ≠ 0 ∧ τ ≠ 0 ∧
        resTop U τ = tensorSection F (tensorPowModule X L (p : ℤ)) t (resTop U σ)

Tag 0BQS, a lemma

Tag 0BQS in the Stacks Project.

Stacks.AlgebraicGeometry.ProjKoszulComplex.acyclic_koszulComplex_and_locallyFree_koszulTerm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjKoszulComplex/LocallyFree.lean, line 152.

Stacks 0BQS. Let A be a ring and X = P^n_A = Proj A[X₀, …, Xₙ]. For every integer a there is an exact complex of vector bundles

0 ⟶ 𝒪_X(a) ⟶ … ⟶ 𝒪_X(a+j)^{⊕ binom(n+1, j)} ⟶ … ⟶ 𝒪_X(a+n+1) ⟶ 0

on X, namely the Koszul complex Stacks.AlgebraicGeometry.ProjKoszulComplex.koszulComplex of the coordinates X₀, …, Xₙ, graded so that the generators of the j-th exterior power sit in degree j and twisted by a. Its j-th term is the direct sum of copies of 𝒪_X(a+j) indexed by the j-element subsets of the coordinates, of which there are binom(n+1, j), and each term is free on that index set over every standard open of a degree-one element, those opens covering X; the complex is acyclic, so it is exact in every degree, and it is concentrated in degrees 0, …, n+1 because outside that range the index set is empty.

theorem acyclic_koszulComplex_and_locallyFree_koszulTerm (j : ℕ) :
    (koszulComplex A n a).Acyclic ∧
      (koszulComplex A n a).X (j : ℤ) =
        (⨁ fun _ : koszulIndex (n + 1) (j : ℤ) =>
          twistingSheaf (polyGrading A n) (a + (j : ℤ))) ∧
      Fintype.card (koszulIndex (n + 1) (j : ℤ)) = (n + 1).choose j ∧
      ∃ (I : Type u) (U : I → Opens (ProjectiveSpectrum.top (polyGrading A n))),
        (Opens.grothendieckTopology (ProjectiveSpectrum.top (polyGrading A n))).CoversTop U ∧
          ∀ f : I, Nonempty (SheafOfModules.free.{u} (ULift.{u} (koszulIndex (n + 1) (j : ℤ))) ≅
            (koszulTerm A n a (j : ℤ)).over (U f))

Tag 0A9V, a lemma

Tag 0A9V in the Stacks Project.

Stacks.AlgebraicGeometry.ExampleGenerator.twist_mem_gen_of_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/ExampleGenerator/Koszul.lean, line 116. The attribute's comment: “each of the twists O, O(-1), …, O(-n) lies in the subcategory generated by E”.

Each of the n + 1 displayed twists is a direct summand of E, hence lies in ⟨E⟩.

theorem twist_mem_gen_of_le (i : Fin (n + 1)) :
    twist A n (-(i : ℤ)) ∈ gen (twistSum A n)

Stacks.AlgebraicGeometry.ExampleGenerator.twist_neg_mem_gen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/ExampleGenerator/Koszul.lean, line 227. The attribute's comment: “the subcategory generated by E contains every twist O(-m), m ≥ 0”.

Every twist 𝒪_X(-m), m ≥ 0, lies in ⟨E⟩. For X = P^n_A and E = 𝒪_X ⊕ 𝒪_X(-1) ⊕ ⋯ ⊕ 𝒪_X(-n), every twist 𝒪_X(-m) with m ≥ 0 lies in the subcategory ⟨E⟩ of [Stacks, Tag 09SI] generated by E.

Strong induction on m. For m ≤ n the twist is a direct summand of E. For m ≥ n + 1 the one-step descent twist_mem_gen_of_shift_mem_gen at a = -m reduces the claim to the twists 𝒪_X(-m+p) for 1 ≤ p ≤ n + 1, and -m + p = -(m - p) with m - p < m.

theorem twist_neg_mem_gen (m : ℕ) : twist A n (-(m : ℤ)) ∈ gen (twistSum A n)

Stacks.AlgebraicGeometry.ExampleGenerator.isWeakTriangulatedGenerator_twistSumDerivedQCoh, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/ExampleGenerator/KoszulQuasiCoherent.lean, line 151.

Let A be a ring and X = P^n_A. Then E = 𝒪_X ⊕ 𝒪_X(-1) ⊕ ⋯ ⊕ 𝒪_X(-n) is a generator of D_QCoh(𝒪_X) in the sense of [Stacks, Tag 09SJ]: every object of D_QCoh(𝒪_X) receiving only zero maps from the shifts of E is zero.

theorem isWeakTriangulatedGenerator_twistSumDerivedQCoh :
    (ObjectProperty.singleton (twistSumDerivedQCoh A n)).IsWeakTriangulatedGenerator

Stacks.AlgebraicGeometry.ExampleGenerator.isWeakTriangulatedGenerator_twistSumQCoh, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/ExampleGenerator/QuasiCoherentGenerator.lean, line 278. The attribute's comment: “the generator conclusion of Definition 09SJ(3) for D_QCoh(O_X), with no hypothesis beyond the tag's. The generation step on the whole of D(O_X) is Stacks.AlgebraicGeometry.ExampleGenerator.twist_neg_mem_gen”.

[Stacks, Tag 0A9V] on D_QCoh(𝒪_X). For X = P^n_A the object E = 𝒪_X ⊕ 𝒪_X(-1) ⊕ ⋯ ⊕ 𝒪_X(-n) in degree zero is a weak generator of D_QCoh(𝒪_X).

An object K of D_QCoh(𝒪_X) receiving only zero morphisms from the shifts of E receives only zero morphisms from every object of ⟨E⟩ ([Stacks, Tag 09SK]), hence from every 𝒪_X(-m)[-p] with m ≥ 0 — that is the generation step Stacks.AlgebraicGeometry.ExampleGenerator.twist_neg_mem_gen. Those twists are enough to force K = 0 by Stacks.AmpleNonvanishing.isZero_of_hom_single_eq_zero, whose presentation hypothesis is exists_epi_coproduct_twist_nonpos.

theorem isWeakTriangulatedGenerator_twistSumQCoh :
    (ObjectProperty.singleton (twistSumQCoh A n)).IsWeakTriangulatedGenerator

Tag 0BQT, a remark

Tag 0BQT in the Stacks Project.

Stacks.Duality.DerivedPushforward.conditions_of_multiplicativeClosure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedPushforward/GeneratorClauses.lean, line 365. The attribute's comment: “the clause that the three conditions hold when f is affine, when f is an open immersion, and when f is a composition of such”.

[Stacks, Tag 0BQT]: the three conditions hold when f is affine, when f is an open immersion, and when f is a composition of such. Let f : X ⟶ Y be a finite composite of affine morphisms and open immersions between quasi-compact and quasi-separated schemes, and let E be a weak generator of D_QCoh(𝒪_Y). Then

1. every object K of D_QCoh(𝒪_X) with Rf_*K zero is itself zero;
2. Rf_* : D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_Y) reflects isomorphisms;
3. Lf^*E is a weak generator of D_QCoh(𝒪_X).

Condition (3) is isWeakTriangulatedGenerator_quasiCoherentDerivedPullback_of_openFactorization, applied to the trivial factorization f = f ≫ 𝟙 Y; (1) and (2) follow from it by tfae_isZero_quasiCoherentDerivedPushforward, the equivalence of the three conditions.

theorem conditions_of_multiplicativeClosure {X Y : Scheme.{u}} [CompactSpace X]
    [QuasiSeparatedSpace X] [CompactSpace Y] [QuasiSeparatedSpace Y] {f : X ⟶ Y}
    (hf : ((@IsAffineHom) ⊔ (@IsOpenImmersion) :
      MorphismProperty (Scheme.{u})).multiplicativeClosure f)
    (E : Stacks.Duality.quasiCoherentDerivedCategory Y)
    (hE : (ObjectProperty.singleton E).IsWeakTriangulatedGenerator) :
    (∀ K : Stacks.Duality.quasiCoherentDerivedCategory X,
        IsZero ((qcqsRestrictedDerivedPushforward f).obj K) → IsZero K) ∧
      (qcqsRestrictedDerivedPushforward f).ReflectsIsomorphisms ∧
      (ObjectProperty.singleton
        ((Stacks.Duality.quasiCoherentDerivedPullback' f).obj E)
        ).IsWeakTriangulatedGenerator

Stacks.Duality.DerivedPushforward.isWeakTriangulatedGenerator_restrictedTwistSum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedPushforward/ProjectiveImmersionGenerator.lean, line 167. The attribute's comment: “the second consequence drawn from the remark: for X a quasi-compact locally closed subscheme of P^n_A, the object O_X ⊕ O_X(-1) ⊕ … ⊕ O_X(-n) is a generator for D_QCoh(O_X)”.

For i : W ⟶ P^n_A an immersion with W quasi-compact, the object 𝒪_W ⊕ 𝒪_W(-1) ⊕ ⋯ ⊕ 𝒪_W(-n), placed in degree zero, generates D_QCoh(𝒪_W).

theorem isWeakTriangulatedGenerator_restrictedTwistSum [IsImmersion i] [CompactSpace W] :
    (ObjectProperty.singleton (restrictedTwistSum i)).IsWeakTriangulatedGenerator

Stacks.Duality.DerivedPushforward.tfae_isZero_quasiCoherentDerivedPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedPushforward/PullbackGenerator.lean, line 197.

[Stacks, Tag 0BQT]. Let f : X ⟶ Y be a quasi-compact and quasi-separated morphism of schemes with Y quasi-compact, and let E be a weak generator of D_QCoh(𝒪_Y) — the object [Stacks, Tag 09IS] provides, and the one hypothesis the source's remark carries. Then the following are equivalent:

1. every object K of D_QCoh(𝒪_X) with Rf_*K zero is itself zero;
2. Rf_* : D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_Y) reflects isomorphisms;
3. Lf^*E is a weak generator of D_QCoh(𝒪_X).

(1) ⇒ (2): complete a morphism α whose image is invertible to a distinguished triangle; Rf_* is exact, so it carries that triangle to a distinguished triangle whose first morphism is Rf_*α, whence its third vertex Rf_*(cone α) is zero, whence cone α is zero by (1), whence α is invertible. (2) ⇒ (1): if Rf_*K is zero then the zero endomorphism of Rf_*K is its identity, so the zero endomorphism of K is invertible by (2) and 𝟙 K = 0.

(1) ⇔ (3): K is right orthogonal to the shifts of Lf^*E exactly when Rf_*K is right orthogonal to the shifts of E, by rightOrthogonal_shiftClosure_singleton_quasiCoherentDerivedPullback_iff, and the latter says exactly that Rf_*K is zero because E generates.

theorem tfae_isZero_quasiCoherentDerivedPushforward
    (E : Stacks.Duality.quasiCoherentDerivedCategory Y)
    (hE : (ObjectProperty.singleton E).IsWeakTriangulatedGenerator) :
    [∀ K : Stacks.Duality.quasiCoherentDerivedCategory X,
        IsZero ((qcqsRestrictedDerivedPushforward f).obj K) → IsZero K,
      (qcqsRestrictedDerivedPushforward f).ReflectsIsomorphisms,
      (ObjectProperty.singleton
        ((Stacks.Duality.quasiCoherentDerivedPullback' f).obj E)
        ).IsWeakTriangulatedGenerator].TFAE

Stacks.Duality.DerivedPushforward.isWeakTriangulatedGenerator_quasiCoherentDerivedPullback_specMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedPushforward/PullbackGenerator.lean, line 257. The attribute's comment: “the conditions hold for an affine morphism: the case of a morphism Spec φ of affine schemes, where Lf^* carries a generator to a generator”.

[Stacks, Tag 0BQT] for a morphism of affine schemes: L(Spec φ)^* carries a generator to a generator. Let φ : R ⟶ S be a map of commutative rings and let E be a weak generator of D_QCoh(𝒪_{Spec R}). Then L(Spec φ)^*E is a weak generator of D_QCoh(𝒪_{Spec S}).

This is the implication (2) ⇒ (3) of tfae_isZero_quasiCoherentDerivedPushforward, whose condition (2) holds for Spec φ by [Stacks, Tag 08I8]; it is the source's clause that the three conditions of the remark hold when f is affine, in the case of a morphism of affine schemes.

theorem isWeakTriangulatedGenerator_quasiCoherentDerivedPullback_specMap
    (E : Stacks.Duality.quasiCoherentDerivedCategory (Spec R))
    (hE : (ObjectProperty.singleton E).IsWeakTriangulatedGenerator) :
    (ObjectProperty.singleton
        ((Stacks.Duality.quasiCoherentDerivedPullback' (Spec.map φ)).obj E)
      ).IsWeakTriangulatedGenerator

Stacks.Duality.DerivedPushforward.isWeakTriangulatedGenerator_derivedStructureSheaf_of_isQuasiAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedPushforward/QuasiAffineGenerator.lean, line 165. The attribute's comment: “the first consequence drawn from the remark: if X is a quasi-affine scheme then the structure sheaf O_X is a generator for D_QCoh(O_X)”.

[Stacks, Tag 0BQT]: if X is a quasi-affine scheme then 𝒪_X generates D_QCoh(𝒪_X). This is the first consequence the source draws from its remark.

A quasi-affine scheme is quasi-compact, quasi-separated, and its canonical morphism j : X ⟶ Spec Γ(X, 𝒪_X) is an open immersion; the target is affine, hence quasi-compact and quasi-separated. The remark's clause for an open immersion therefore applies to j, and 𝒪 is a generator on the affine target by isWeakTriangulatedGenerator_derivedStructureSheaf_spec, so Lj^*𝒪 is a generator — and Lj^*𝒪 is 𝒪_X.

theorem isWeakTriangulatedGenerator_derivedStructureSheaf_of_isQuasiAffine (X : Scheme.{u})
    [X.IsQuasiAffine] :
    (ObjectProperty.singleton (derivedStructureSheaf X)).IsWeakTriangulatedGenerator

Sources

• Section 36.16, Tag 0BQQ
• AxiomMath/Stacks at 5ed82d14

LeanStacks.AmpleNonvanishing.exists_nonzero_hypercohomology_tensorPower · Stacks.AmpleNonvanishingChart.exists_twistedSection_restrict_eq_tensorSection · Stacks.AlgebraicGeometry.ProjKoszulComplex.acyclic_koszulComplex_and_locallyFree_koszulTerm · Stacks.AlgebraicGeometry.ExampleGenerator.twist_mem_gen_of_le · Stacks.AlgebraicGeometry.ExampleGenerator.twist_neg_mem_gen · Stacks.AlgebraicGeometry.ExampleGenerator.isWeakTriangulatedGenerator_twistSumDerivedQCoh · Stacks.AlgebraicGeometry.ExampleGenerator.isWeakTriangulatedGenerator_twistSumQCoh · Stacks.Duality.DerivedPushforward.conditions_of_multiplicativeClosure

Section36.17 Compact and perfect objects#

Section 36.17 of the Stacks Project, Tag 09M0. 5 tags here are carried by 13 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 09M1, a proposition

Tag 09M1 in the Stacks Project.

Stacks.Duality.isCompactObject_iff_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactGeneration/CompactPerfect.lean, line 661.

[Stacks, Tag 09M1]. On a quasi-compact quasi-separated scheme X, an object of D_QCoh(𝒪_X) is compact if and only if it is a perfect object of D(𝒪_X), in any model of D(𝒪_X).

theorem _root_.Stacks.Duality.isCompactObject_iff_isPerfect {X : Scheme.{u}} [CompactSpace X]
    [QuasiSeparatedSpace X] [h : HasDerivedCategory.{w} X.Modules]
    (K : Stacks.Duality.quasiCoherentDerivedCategory X) :
    IsCompactObject.{u} K ↔ @Stacks.Cohomology.PerfectComplexes.IsPerfect X.toRingedSpace h K.obj

Stacks.Duality.isCompactObject_eq_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactGeneration/CompactPerfectTag.lean, line 48.

[Stacks, Tag 09M1]. Let X be a quasi-compact and quasi-separated scheme. An object of D_QCoh(𝒪_X) is compact if and only if it is perfect: the compact objects of D_QCoh(𝒪_X) are exactly those whose underlying object of D(𝒪_X) is perfect, in any model of D(𝒪_X).

theorem isCompactObject_eq_isPerfect (X : Scheme.{u}) [CompactSpace X] [QuasiSeparatedSpace X]
    [h : HasDerivedCategory.{w} X.Modules] :
    (IsCompactObject.{u} : ObjectProperty (quasiCoherentDerivedCategory X)) =
      fun K => @Stacks.Cohomology.PerfectComplexes.IsPerfect X.toRingedSpace h K.obj

Stacks.Duality.PerfectCompact.isCompactObject_iff_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactGeneration/PerfectIsCompactCover.lean, line 311.

Let X be a quasi-compact and quasi-separated scheme. An object of D_QCoh(𝒪_X) is compact if and only if it is perfect.

theorem isCompactObject_iff_isPerfect (X : Scheme.{u}) [CompactSpace X] [QuasiSeparatedSpace X]
    (K : Stacks.Duality.quasiCoherentDerivedCategory X) :
    IsCompactObject.{u} K ↔ RingedSpace.IsPerfect (X := X.toRingedSpace) K.obj

AlgebraicGeometry.isCompactObject_iff_isPerfect_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/QuasiCoherentDerived/CompactAndPerfect.lean, line 124. The attribute's comment: “the affine case, both directions”.

Stacks 09M1 on an affine scheme. Let R be a ring and let L be an object of D_QCoh(𝒪_{Spec R}). Then L is a compact object of D_QCoh(𝒪_{Spec R}) if and only if it is a perfect object of D(𝒪_{Spec R}).

Writing L = M̃ for an object M of D(R), compactness of L is compactness of M because M ↦ M̃ is an equivalence ([Stacks, Tag 06Z0], here AlgebraicGeometry.affineTildeQuasicoherent_isEquivalence), compactness of M is perfectness of M by [Stacks, Tag 07LT], and perfectness of M is perfectness of M̃ by [Stacks, Tag 08EB].

theorem isCompactObject_iff_isPerfect_spec (R : CommRingCat.{u})
    (L : QuasicoherentDerivedCategory (Spec R)) :
    IsCompactObject.{u} L ↔
      Stacks.Cohomology.PerfectComplexes.IsPerfect (X := (Spec R).toRingedSpace) L.obj

AlgebraicGeometry.isPerfect_of_isCompactObject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/QuasiCoherentDerived/CompactAndPerfect.lean, line 161. The attribute's comment: “compact implies perfect; the affine-local datum, which the source draws from Tag 08DZ (derived direct image along a quasi-compact quasi-separated morphism commutes with direct sums) together with Tag 06Z0, is a hypothesis: that deduction is not carried out here. Tag 08DZ is proved in this repository, as Stacks.Duality.DerivedPushforward.preservesColimitsOfShape_discrete_qcqsQuasiCoherentDerivedPushforward, but only at HasDerivedCategory.standard”.

Stacks 09M1, the implication from compactness to perfectness. Let X be a scheme and let K be an object of D_QCoh(𝒪_X). Suppose every point of X has an open neighbourhood U on which K is the image, under a functor preserving perfectness, of a compact object of D_QCoh(𝒪_{Spec R}) for some ring R. Then K is a perfect object of D(𝒪_X).

Compactness of K itself enters only through the local models: on a quasi-compact quasi-separated scheme the restriction of a compact object of D_QCoh(𝒪_X) to an affine open is compact there, by [Stacks, Tag 08DZ] and adjunction. The affine case makes the local models perfect, and perfectness is local on the space by [Stacks, Tag 08CN].

theorem isPerfect_of_isCompactObject (X : Scheme.{u}) (K : QuasicoherentDerivedCategory X)
    (hloc : ∀ x : X.toRingedSpace.carrier,
      ∃ (U : Opens X.toRingedSpace.carrier) (_ : x ∈ U) (R : CommRingCat.{u})
        (Φ : DerivedCategory (SheafOfModules.{u} (Spec R).ringCatSheaf) ⥤
          DerivedCategory (StrictlyPerfect.OXMod.{u, u, u}
            (X.toRingedSpace.restrict U.isOpenEmbedding)))
        (L : QuasicoherentDerivedCategory (Spec R)),
        IsCompactObject.{u} L ∧
          (∀ N, Stacks.Cohomology.PerfectComplexes.IsPerfect
              (X := (Spec R).toRingedSpace) N →
            Stacks.Cohomology.PerfectComplexes.IsPerfect
              (X := X.toRingedSpace.restrict U.isOpenEmbedding) (Φ.obj N)) ∧
          Nonempty (Φ.obj L.obj ≅
            (RingedSpace.restrictModules X.toRingedSpace U).mapDerivedCategory.obj K.obj)) :
    Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace) K.obj

AlgebraicGeometry.isCompactObject_iff_isPerfect_spec_of_model, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/QuasiCoherentDerived/CompactAndPerfectLocallySmall.lean, line 104. The attribute's comment: “the affine case, both directions, at an arbitrary chosen derived category -- in particular at the locally small AlgebraicGeometry.Scheme.Modules.hasDerivedCategory, at which the companion AlgebraicGeometry.isCompactObject_iff_isPerfect_spec says nothing. The global case is not covered here”.

The affine case of [Stacks, Tag 09M1], at an arbitrary chosen derived category. Let R be a ring and let K be an object of D_QCoh(𝒪_{Spec R}), for any chosen model of D(R) and any chosen model of D(𝒪_{Spec R}). Then K is a compact object of D_QCoh(𝒪_{Spec R}), with the direct sums tested over index types in Type u, if and only if K is a perfect object of D(𝒪_{Spec R}).

Writing K = M̃ for an object M of D(R), which is possible because M ↦ M̃ is an equivalence ([Stacks, Tag 06Z0]), compactness of K is compactness of M because compactness at a fixed index universe crosses an additive equivalence, compactness of M is perfectness of M by [Stacks, Tag 07LT], and perfectness of M is perfectness of M̃ by [Stacks, Tag 08EB].

This is AlgebraicGeometry.isCompactObject_iff_isPerfect_spec with the pin on the standard model removed; see the implementation notes for why it cannot be added beside it.

theorem isCompactObject_iff_isPerfect_spec_of_model
    (K : Stacks.Duality.quasiCoherentDerivedCategory (Spec R)) :
    IsCompactObject.{u} K ↔
      @Stacks.Cohomology.PerfectComplexes.IsPerfect (Spec R).toRingedSpace hS K.obj

Stacks.Duality.QcqsPerfect.isCompactObject_iff_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/QuasiCoherentDerived/QcqsCompactIsPerfect.lean, line 93. The attribute's comment: “both directions, on a quasi-compact quasi-separated scheme, at the locally small AlgebraicGeometry.Scheme.Modules.hasDerivedCategory”.

[Stacks, Tag 09M1]. On a quasi-compact quasi-separated scheme X, an object of D_QCoh(𝒪_X) is compact if and only if it is perfect, at the locally small derived category.

theorem isCompactObject_iff_isPerfect (X : Scheme.{u}) [CompactSpace X] [QuasiSeparatedSpace X]
    (K : Stacks.Duality.quasiCoherentDerivedCategory X) :
    IsCompactObject.{u} K ↔
      Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace) K.obj

Stacks.Duality.QcqsPerfect.isCompactObject_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/QuasiCoherentDerived/QcqsPerfectIsCompact.lean, line 289. The attribute's comment: “perfect implies compact, on a quasi-compact quasi-separated scheme, at the locally small AlgebraicGeometry.Scheme.Modules.hasDerivedCategory. The opposite implication is not covered here; for it on a general scheme see AlgebraicGeometry.isPerfect_of_isCompactObject, and for both on an affine scheme see AlgebraicGeometry.isCompactObject_iff_isPerfect_spec_of_model”.

Let X be a quasi-compact quasi-separated scheme and let K be an object of D_QCoh(𝒪_X) which is perfect as an object of D(𝒪_X). Then K is a compact object of D_QCoh(𝒪_X), with the direct sums tested over index types in the universe of X, at the locally small derived category AlgebraicGeometry.Scheme.Modules.hasDerivedCategory.

theorem isCompactObject_of_isPerfect (X : Scheme.{u}) [CompactSpace X] [QuasiSeparatedSpace X]
    (K : Stacks.Duality.quasiCoherentDerivedCategory X)
    (hK : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace) K.obj) :
    IsCompactObject.{u} K

Tag 0GEF, a remark

Tag 0GEF in the Stacks Project.

Stacks.Duality.PerfectClassicalGenerator.triangEnvelope_eq_perfectObjects_of_isWeakTriangulatedGenerator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ClassicalGeneratorOfPerfectComplexes.lean, line 253. The attribute's comment: “for X quasi-compact and quasi-separated and G a perfect object generating D_QCoh(O_X), G is a classical generator of D_perf(O_X): the triangulated envelope of G is exactly the perfect objects”.

Stacks 0GEF. Let X be a quasi-compact and quasi-separated scheme and let G be a perfect object of D(𝒪_X) lying in D_QCoh(𝒪_X) and generating it, in the sense that an object of D_QCoh(𝒪_X) receiving only zero morphisms from the shifts of G is zero. Then G is a classical generator of D_perf(𝒪_X): the smallest strictly full triangulated subcategory of D_QCoh(𝒪_X) closed under direct summands and containing G is exactly the subcategory of perfect objects.

theorem triangEnvelope_eq_perfectObjects_of_isWeakTriangulatedGenerator
    (X : Scheme.{u}) [CompactSpace X] [QuasiSeparatedSpace X]
    (G : Stacks.Duality.quasiCoherentDerivedCategory X)
    (hG : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace) G.obj)
    (hgen : (ObjectProperty.singleton G).IsWeakTriangulatedGenerator) :
    (ObjectProperty.singleton G).triangEnvelope = perfectObjects X

Tag 0A9B, a lemma

Tag 0A9B in the Stacks Project.

Stacks.Duality.Supported.isCompactObject_iff_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactGeneration/SupportedCompactObject.lean, line 218. The attribute's comment: “compactness in D_{QCoh,T}(𝒪_X) is perfectness in D(𝒪_X), with nothing carried. Both results the source cites are proved in this library and discharged in the proof: Tag 09M1, that a perfect object of D_QCoh(𝒪_X) is a compact object of it, as AlgebraicGeometry.isCompactObject_of_isPerfect, and Tag 0A9A, that D_{QCoh,T}(𝒪_X) is generated by a perfect object, as Stacks.Rouquier.exists_isPerfect_isWeakTriangulatedGenerator_supported. They are discharged at the cost of the source's own hypotheses that X be quasi-compact and quasi-separated and that T be closed with quasi-compact complement, which are Tag 0A9B's hypotheses too and are used for nothing else. The source's step (d), that a direct summand of a perfect object is perfect, is Tag 08CS and is proved in this library, so it is not a hypothesis. The derived category is the locally small model rather than a binder, Tag 0A9A being available at no other; the two directions at an arbitrary model are Stacks.Duality.Supported.isCompactObject_of_isPerfect and, with the generator given, Stacks.Duality.Supported.isPerfect_of_isCompactObject”.

An object of D_{QCoh,T}(𝒪_X) is compact if and only if it is perfect as an object of D(𝒪_X), for X quasi-compact and quasi-separated and T closed with quasi-compact complement. The derived category is taken at the locally small model.

theorem isCompactObject_iff_isPerfect [CompactSpace X] [QuasiSeparatedSpace X]
    (hT : IsClosed T) (hTc : IsCompact Tᶜ)
    (K : QuasiCoherentSupportedDerivedCategory X T) :
    IsCompactObject.{u} K ↔ IsPerfect (X := X.toRingedSpace) K.obj

Stacks.Duality.Supported.isCompactObject_iff_isPerfect_of_isClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactGeneration/SupportedCompactPerfect.lean, line 296.

[Stacks, Tag 0A9B]. Let X be a quasi-compact and quasi-separated scheme and let T ⊆ X be a closed subset such that X ∖ T is quasi-compact. An object of D_{QCoh,T}(𝒪_X) is compact (in D_{QCoh,T}(𝒪_X)) if and only if it is perfect as an object of D(𝒪_X).

Perfect objects are compact in D_QCoh(𝒪_X) by [Stacks, Tag 09M1] (Stacks.Duality.PerfectCompact.isCompactObject_of_isPerfect), hence in the full subcategory D_{QCoh,T}(𝒪_X), which is closed under direct sums (Stacks.Duality.Supported.isCompactObject_of_isCompactObject_obj). Conversely D_{QCoh,T}(𝒪_X) has a compact perfect generator ([Stacks, Tag 0A9A], Stacks.Duality.Supported.exists_isCompactObject_isPerfect_isWeakTriangulatedGenerator), so every compact object is built from it by shifts, cones, finite direct sums and summands ([Stacks, Tag 09SR]), and is perfect (Stacks.Duality.Supported.isPerfect_of_isCompactObject_of_generator).

theorem isCompactObject_iff_isPerfect_of_isClosed (hT : IsClosed T) (hTc : IsCompact Tᶜ)
    (K : Stacks.Duality.QuasiCoherentSupportedDerivedCategory X T) :
    IsCompactObject.{u} K ↔
      AlgebraicGeometry.RingedSpace.IsPerfect (X := X.toRingedSpace) K.obj

Tag 0GEG, a remark

Tag 0GEG in the Stacks Project.

Stacks.Duality.SupportedClassicalGenerator.hasCoproducts_and_exists_perfect_generator_and_triangEnvelope_eq_perfectSupported, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportedClassicalGenerator.lean, line 386.

[Stacks, Remark 0GEG]. Let X be a quasi-compact and quasi-separated scheme and let T ⊆ X be a closed subset such that X ∖ T is quasi-compact. Then

1. D_{QCoh,T}(𝒪_X) has direct sums;
2. there is a perfect object G of D_{QCoh,T}(𝒪_X) which is a generator for D_{QCoh,T}(𝒪_X) (by [Stacks, Tag 0A9A]);
3. every such G is a classical generator for D_{perf,T}(𝒪_X): the smallest strictly full, saturated, triangulated subcategory of D_{QCoh,T}(𝒪_X) containing G is the subcategory perfectSupported X T of objects perfect in D(𝒪_X).

Generators are weak generators in the sense of [Stacks, Tag 09SJ](3) and the classical generation is equality with CategoryTheory.ObjectProperty.triangEnvelope. Everything is stated at an arbitrary model of the derived category. The direct sums are indexed by the universe of 𝒪_X-modules; the source's argument uses them, with [Stacks, Tag 0A9B] and [Stacks, Tag 09SR], at the locally small model, where the morphisms of D(𝒪_X) lie in that universe too.

theorem hasCoproducts_and_exists_perfect_generator_and_triangEnvelope_eq_perfectSupported
    (hT : IsClosed T) (hTc : IsCompact (Tᶜ : Set X)) :
    HasCoproducts.{u} (QuasiCoherentSupportedDerivedCategory X T) ∧
      (∃ G : QuasiCoherentSupportedDerivedCategory X T,
        perfectSupported X T G ∧ (ObjectProperty.singleton G).IsWeakTriangulatedGenerator) ∧
      ∀ G : QuasiCoherentSupportedDerivedCategory X T, perfectSupported X T G →
        (ObjectProperty.singleton G).IsWeakTriangulatedGenerator →
          (ObjectProperty.singleton G).triangEnvelope = perfectSupported X T

Tag 0A9C, a lemma

Tag 0A9C in the Stacks Project.

Stacks.Duality.exists_isPerfect_whiskerRight_comp_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactGeneration/PerfectAnnihilator.lean, line 149.

[Stacks, Tag 0A9C]. Let X be quasi-compact and quasi-separated, U ⊆ X a quasi-compact open and α : P ⟶ E a morphism of D_QCoh(𝒪_X) with E supported on X \ U, where either P is perfect, or P is pseudo-coherent and E is bounded below. Then there is a perfect complex I and a map u : I ⟶ 𝒪_X invertible on U such that I ⊗ᴸ P ⟶ P ⟶ E is zero.

theorem exists_isPerfect_whiskerRight_comp_eq_zero {X U : Scheme.{u}} [CompactSpace X]
    [QuasiSeparatedSpace X] (j : U ⟶ X) [IsOpenImmersion j] [AlgebraicGeometry.QuasiCompact j]
    {P E : quasiCoherentDerivedCategory X} (α : P ⟶ E)
    (hE : IsZero ((derivedRestrict j).obj E.obj))
    (hP : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace) P.obj ∨
      (AlgebraicGeometry.RingedSpace.IsPseudoCoherent (X := X.toRingedSpace) P.obj ∧
        DerivedCategoryB.IsBoundedBelow E.obj)) :
    ∃ (I : quasiCoherentDerivedCategory X) (u : I ⟶ 𝟙_ (quasiCoherentDerivedCategory X)),
      Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace) I.obj ∧
        IsIso ((derivedRestrict j).map ((ObjectProperty.ι _).map u)) ∧
          (u ▷ P) ≫ (λ_ P).hom ≫ α = 0

Sources

• Section 36.17, Tag 09M0
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Duality.isCompactObject_iff_isPerfect · Stacks.Duality.isCompactObject_eq_isPerfect · Stacks.Duality.PerfectCompact.isCompactObject_iff_isPerfect · AlgebraicGeometry.isCompactObject_iff_isPerfect_spec · AlgebraicGeometry.isPerfect_of_isCompactObject · AlgebraicGeometry.isCompactObject_iff_isPerfect_spec_of_model · Stacks.Duality.QcqsPerfect.isCompactObject_iff_isPerfect · Stacks.Duality.QcqsPerfect.isCompactObject_of_isPerfect

Section36.18 Derived categories as module categories#

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

Tag 09M3, a lemma

Tag 09M3 in the Stacks Project.

AlgebraicGeometry.RingedSite.derivedCategoryB_tensorWithComplexDerived_obj_scheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/TensorWithComplexQuasicoherentAdjoint.lean, line 262. The attribute's comment: “for the site of opens of the scheme”.

Stacks 09M3. "Let X be a scheme, K a complex of O_X-modules with quasi-coherent cohomology sheaves, (E, d) = Hom(K, K). Then - ⊗_E^𝐋 K : D(E, d) ⟶ D(O_X) of Tag 09LX has image contained in D_QCoh(O_X)." The scheme is read as the ringed site of its opens.

theorem derivedCategoryB_tensorWithComplexDerived_obj_scheme (Y : Scheme.{u})
    (K : CochainComplex (ModO.{u, u, u, u}
      (Stacks.AlgebraicGeometry.ReflexiveModules.schemeRingedSite Y)) ℤ)
    (hK : tensorModOQuasicoherentDerived.{u, u, u, u, u}
      (Stacks.AlgebraicGeometry.ReflexiveModules.schemeRingedSite Y)
      (DerivedCategory.Q.obj (liftComplex.{u, u, u, u, u}
        (Stacks.AlgebraicGeometry.ReflexiveModules.schemeRingedSite Y) K)))
    (M : DifferentialGradedModule.derivedCategory.{0, u, u}
      (Rep.{u, u, u, u, u, 0}
        (Stacks.AlgebraicGeometry.ReflexiveModules.schemeRingedSite Y) ℤ K).algebra) :
    tensorModOQuasicoherentDerived.{u, u, u, u, u}
      (Stacks.AlgebraicGeometry.ReflexiveModules.schemeRingedSite Y)
      ((tensorWithComplexDerived.{u, u, u, u, u, 0}
        (Stacks.AlgebraicGeometry.ReflexiveModules.schemeRingedSite Y) ℤ K).obj M)

AlgebraicGeometry.RingedSite.derivedCategoryB_isQuasicoherent_tensorWithComplexDerived_obj_scheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/TensorWithComplexQuasicoherentAdjoint.lean, line 284.

Stacks 09M3. Every cohomology sheaf of M ⊗_E^𝐋 K is a quasi-coherent O_Y-module, for Y a scheme and K a complex of O_Y-modules with quasi-coherent cohomology sheaves.

theorem derivedCategoryB_isQuasicoherent_tensorWithComplexDerived_obj_scheme (Y : Scheme.{u})
    (K : CochainComplex (ModO.{u, u, u, u}
      (Stacks.AlgebraicGeometry.ReflexiveModules.schemeRingedSite Y)) ℤ)
    (hK : tensorModOQuasicoherentDerived.{u, u, u, u, u}
      (Stacks.AlgebraicGeometry.ReflexiveModules.schemeRingedSite Y)
      (DerivedCategory.Q.obj (liftComplex.{u, u, u, u, u}
        (Stacks.AlgebraicGeometry.ReflexiveModules.schemeRingedSite Y) K)))
    (M : DifferentialGradedModule.derivedCategory.{0, u, u}
      (Rep.{u, u, u, u, u, 0}
        (Stacks.AlgebraicGeometry.ReflexiveModules.schemeRingedSite Y) ℤ K).algebra) :
    DerivedCategoryB.derivedCategoryB
        (A := TensorModO.{u, u, u, u, u}
          (Stacks.AlgebraicGeometry.ReflexiveModules.schemeRingedSite Y))
        (SheafOfModules.isQuasicoherent Y.ringCatSheaf)
      ((tensorWithComplexDerived.{u, u, u, u, u, 0}
        (Stacks.AlgebraicGeometry.ReflexiveModules.schemeRingedSite Y) ℤ K).obj M)

Tag 09M5, a theorem

Tag 09M5 in the Stacks Project.

AlgebraicGeometry.exists_differentialGradedAlgebra_quasiCoherentDerivedCategory_equivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/QuasiCoherentDerived/DGAModel.lean, line 250.

Stacks 09M5 (Bondal–van den Bergh). Let X be a quasi-compact and quasi-separated scheme. Then there exist a differential graded algebra (E, d) with only a finite number of nonzero cohomology groups H^i(E) such that D_QCoh(O_X) is equivalent to D(E, d).

D_QCoh(O_X) is the full subcategory of the derived category of O_X-modules — at an arbitrary chosen model — of the objects all of whose cohomology sheaves are quasi-coherent, and D(E, d) is the derived category of differential graded E-modules. The algebra is an algebra over ℤ, the endomorphism algebra Hom_{Comp^dg(O_X)}(K^•, K^•) of a K-injective perfect generator K^• of D_QCoh(O_X); the equivalence is the derived tensor product - ⊗_E^𝐋 K^• of Tag 09LX, see AlgebraicGeometry.exists_isKInjective_tensorWithComplexDerived_lift_isEquivalence, followed by the comparison of the standard model with the chosen one.

theorem exists_differentialGradedAlgebra_quasiCoherentDerivedCategory_equivalence
    (X : Scheme.{u}) [CompactSpace X] [QuasiSeparatedSpace X] [HasDerivedCategory X.Modules] :
    ∃ E : DifferentialGradedAlgebra.{0, u} ℤ,
      {i : ℤ | Nontrivial (E.Cohomology i)}.Finite ∧
        Nonempty ((DerivedCategoryB.derivedCategoryB (A := X.Modules)
          (SheafOfModules.isQuasicoherent X.ringCatSheaf)).FullSubcategory ≌
            DifferentialGradedModule.derivedCategory.{0, u, u} E)

Tag 0DJL, a remark

Tag 0DJL in the Stacks Project.

Stacks.Duality.SupportedGeneration.exists_dga_equivalence_quasiCoherentSupported, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactGeneration/SupportedDGAModel.lean, line 235.

[Stacks, Tag 0DJL]. "Let X be a quasi-compact and quasi-separated scheme. Let T ⊂ X be a closed subset such that X ∖ T is quasi-compact. The analogue of Theorem 09M5 holds for D_{QCoh,T}(𝒪_X)." That is: there is a differential graded algebra (E, d) with only a finite number of nonzero cohomology groups H^i(E) such that D_{QCoh,T}(𝒪_X) is equivalent to D(E, d). The derived category of 𝒪_X-modules is taken at an arbitrary model h.

theorem exists_dga_equivalence_quasiCoherentSupported (hT : IsClosed T)
    (hTc : IsCompact (Tᶜ : Set X))
    [h : HasDerivedCategory.{w} (SheafOfModules.{u} X.ringCatSheaf)] :
    ∃ E : DifferentialGradedAlgebra.{0, u} ℤ, {i : ℤ | Nontrivial (E.Cohomology i)}.Finite ∧
      Nonempty (@Stacks.Duality.QuasiCoherentSupportedDerivedCategory X T h ≌
        DifferentialGradedModule.derivedCategory.{0, u, u} E)

Tag 09SU, a remark

Tag 09SU in the Stacks Project.

AlgebraicGeometry.exists_dga_quasiCoherentDerived_linearEquivalence_and_derivedTensor_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/QuasiCoherentDerived/DGAUniqueness/Remark.lean, line 142.

Stacks 09SU (uniqueness of the differential graded algebra). Let X be a quasi-compact and quasi-separated scheme over a ring R. By the construction of the proof of Tag 09M5 there exists a differential graded algebra (A, d) over R such that D_QCoh(X) is R-linearly equivalent to D(A, d) as a triangulated category. If (B, d) is a second such pair, then (A, d) = Hom_{Comp^dg(𝒪_X)}(K, K) and (B, d) = Hom_{Comp^dg(𝒪_X)}(L, L) for K-injective complexes K, L of 𝒪_X-modules corresponding to perfect generators of D_QCoh(𝒪_X); with Ω = Hom(K, L) and Ω' = Hom(L, K), Ω is a differential graded B^{opp} ⊗_R A-module and Ω' a differential graded A^{opp} ⊗_R B-module, and the equivalence D(A, d) → D_QCoh(𝒪_X) → D(B, d) is given by - ⊗_A^𝐋 Ω', and similarly its quasi-inverse by - ⊗_B^𝐋 Ω.

The scheme is over R through f : X ⟶ Spec R, which makes 𝒪_X-modules R-linear (AlgebraicGeometry.overRingLinear). D_QCoh(X) is taken at an arbitrary model h of the derived category of 𝒪_X-modules. The pairs of the construction are indexed by the complexes K with IsPerfectGeneratorRepresentative X K (K-injective, perfect, generating D_QCoh(𝒪_X)): the algebra is A = Hom_{Comp^dg(𝒪_X)}(K, K) (RingedSite.Rep … K's algebra, a differential graded R-algebra) and the equivalence is AlgebraicGeometry.dgaModelEquivalenceAt, the quasi-inverse of - ⊗_A^𝐋 K.

1. Such a K exists, and the equivalence D_QCoh(X) ≌ D(A, d) is R-linear and exact.
2. For two of them K, L, Ω' = Hom(L, K) is the differential graded (A, B)-bimodule RingedSite.homBimodule … K L — its right B-module is the Hom complex of Tag 09LE, and a ∈ A acts by postcomposition — and, through Tag 0FQJ, comes from a differential graded A^{opp} ⊗_R B-module; symmetrically for Ω = Hom(K, L), a (B, A)-bimodule coming from a B^{opp} ⊗_R A-module.
3. The composite equivalence D(A, d) ≌ D_QCoh(X) ≌ D(B, d) has functor isomorphic to - ⊗_A^𝐋 Ω' and quasi-inverse isomorphic to - ⊗_B^𝐋 Ω.

theorem exists_dga_quasiCoherentDerived_linearEquivalence_and_derivedTensor_iso
    (X : Scheme.{u}) [CompactSpace X] [QuasiSeparatedSpace X] {R : CommRingCat.{u}}
    (f : X ⟶ Spec R) [h : HasDerivedCategory.{w} X.Modules] :
    letI := overRingLinear f
    letI := overRingScalarSections f
    (∃ K : CochainComplex (RingedSite.ModO.{u, u, u, u} (𝒮 X)) ℤ,
      ∃ hK : IsPerfectGeneratorRepresentative X K,
        (dgaModelEquivalenceAt R hK h).functor.Linear R ∧
          ∃ _ : (dgaModelEquivalenceAt R hK h).functor.CommShift ℤ,
            (dgaModelEquivalenceAt R hK h).functor.IsTriangulated) ∧
    ∀ (K L : CochainComplex (RingedSite.ModO.{u, u, u, u} (𝒮 X)) ℤ)
      (hK : IsPerfectGeneratorRepresentative X K) (hL : IsPerfectGeneratorRepresentative X L),
      -- `Ω' = Hom(L, K)`: an `(A, B)`-bimodule, by pre- and postcomposition
      (RingedSite.homBimodule (𝒮 X) R K L).rightModule =
          (RingedSite.Rep.{u, u, u, u, u, u} (𝒮 X) R L).functor.obj
            (RingedSite.liftComplex.{u, u, u, u, u} (𝒮 X) K) ∧
        (∀ (n : ℤ) (a : (RingedSite.Rep.{u, u, u, u, u, u} (𝒮 X) R K).algebra.grading n),
          (RingedSite.homBimodule (𝒮 X) R K L).leftAction.1.action n a =
            DifferentialGradedModule.homogeneousMapToCochain _
              ((RingedSite.Rep.{u, u, u, u, u, u} (𝒮 X) R L).functor.map
                ((RingedSite.Rep.{u, u, u, u, u, u} (𝒮 X) R K).algebraHom n a))) ∧
        -- `Ω' = Hom(L, K)`: a differential graded `A^{opp} ⊗_R B`-module (Tag 0FQJ)
        (∃ N : DifferentialGradedModule.{u, u, u} (DifferentialGraded.Bimodule.tensorAlgebra
            (RingedSite.Rep.{u, u, u, u, u, u} (𝒮 X) R K).algebra
            (RingedSite.Rep.{u, u, u, u, u, u} (𝒮 X) R L).algebra),
          Nonempty ((DifferentialGraded.Bimodule.tensorEquivalence _ _).equivalence.inverse.obj N ≅
            RingedSite.homBimodule (𝒮 X) R K L)) ∧
        -- `Ω = Hom(K, L)`: a `(B, A)`-bimodule, by pre- and postcomposition
        (RingedSite.homBimodule (𝒮 X) R L K).rightModule =
          (RingedSite.Rep.{u, u, u, u, u, u} (𝒮 X) R K).functor.obj
            (RingedSite.liftComplex.{u, u, u, u, u} (𝒮 X) L) ∧
        (∀ (n : ℤ) (b : (RingedSite.Rep.{u, u, u, u, u, u} (𝒮 X) R L).algebra.grading n),
          (RingedSite.homBimodule (𝒮 X) R L K).leftAction.1.action n b =
            DifferentialGradedModule.homogeneousMapToCochain _
              ((RingedSite.Rep.{u, u, u, u, u, u} (𝒮 X) R K).functor.map
                ((RingedSite.Rep.{u, u, u, u, u, u} (𝒮 X) R L).algebraHom n b))) ∧
        -- `Ω = Hom(K, L)`: a differential graded `B^{opp} ⊗_R A`-module (Tag 0FQJ)
        (∃ N : DifferentialGradedModule.{u, u, u} (DifferentialGraded.Bimodule.tensorAlgebra
            (RingedSite.Rep.{u, u, u, u, u, u} (𝒮 X) R L).algebra
            (RingedSite.Rep.{u, u, u, u, u, u} (𝒮 X) R K).algebra),
          Nonempty ((DifferentialGraded.Bimodule.tensorEquivalence _ _).equivalence.inverse.obj N ≅
            RingedSite.homBimodule (𝒮 X) R L K)) ∧
        -- the composite `D(A, d) ≌ D_QCoh(X) ≌ D(B, d)` is `- ⊗_A^𝐋 Ω'`, with quasi-inverse
        -- `- ⊗_B^𝐋 Ω`
        Nonempty (((dgaModelEquivalenceAt R hK h).symm.trans
            (dgaModelEquivalenceAt R hL h)).functor ≅
          RingedSite.derivedTensorHom (𝒮 X) R K L) ∧
        Nonempty (((dgaModelEquivalenceAt R hK h).symm.trans
            (dgaModelEquivalenceAt R hL h)).inverse ≅
          RingedSite.derivedTensorHom (𝒮 X) R L K)

Sources

• Section 36.18, Tag 09M2
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.RingedSite.derivedCategoryB_tensorWithComplexDerived_obj_scheme · AlgebraicGeometry.RingedSite.derivedCategoryB_isQuasicoherent_tensorWithComplexDerived_obj_scheme · AlgebraicGeometry.exists_differentialGradedAlgebra_quasiCoherentDerivedCategory_equivalence · Stacks.Duality.SupportedGeneration.exists_dga_equivalence_quasiCoherentSupported · AlgebraicGeometry.exists_dga_quasiCoherentDerived_linearEquivalence_and_derivedTensor_iso

Section36.19 Characterizing pseudo-coherent complexes, I#

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

Tag 0DJN, a lemma

Tag 0DJN in the Stacks Project.

Stacks.PseudoCoherentHocolim.isPseudoCoherent_iff_exists_perfect_hocolim, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/PseudoCoherentHocolim.lean, line 672.

[Stacks, Tag 0DJN]. Let X be a quasi-compact and quasi-separated scheme and let K be an object of D(𝒪_X). The following are equivalent: 1. K is pseudo-coherent; 2. K = hocolim Kₙ where each Kₙ is perfect and τ_{≥ -n} Kₙ ⟶ τ_{≥ -n} K is an isomorphism for all n.

Here K = hocolim Kₙ is CategoryTheory.Pretriangulated.IsHomotopyColimitWith F K c (Definition 090Z, recording the coprojections cₙ : Kₙ ⟶ K), the map τ_{≥ -n} Kₙ ⟶ τ_{≥ -n} K is the truncation of the coprojection cₙ, and the derived category is an arbitrary model of D(𝒪_X). The system is indexed by n = 0, 1, 2, …, as in Definition 090Z; a system K₁ ⟶ K₂ ⟶ ⋯ indexed from 1 as in the source's proof is the case Kₙ ↦ Kₙ₊₁, which satisfies the condition at n because it does at n + 1.

theorem isPseudoCoherent_iff_exists_perfect_hocolim [CompactSpace X] [QuasiSeparatedSpace X]
    (K : DerivedCategory X.Modules) :
    @RingedSpace.IsPseudoCoherent X.toRingedSpace h K ↔
      ∃ (F : ℕ ⥤ DerivedCategory X.Modules) (_ : HasCoproduct F.obj) (c : ∀ n, F.obj n ⟶ K),
        (∀ n, @Stacks.Cohomology.PerfectComplexes.IsPerfect X.toRingedSpace h (F.obj n)) ∧
        IsHomotopyColimitWith F K c ∧
        ∀ n : ℕ, IsIso ((DerivedCategory.TStructure.t.truncGE (-(n : ℤ))).map (c n))

Tag 0DJP, a lemma

Tag 0DJP in the Stacks Project.

Stacks.PseudoCoherentHocolim.isPseudoCoherent_iff_exists_supported_perfect_hocolim, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/PseudoCoherentHocolimSupported.lean, line 55.

[Stacks, Tag 0DJP]. Let X be a quasi-compact and quasi-separated scheme, let T ⊆ X be a closed subset with X \ T quasi-compact and let K ∈ D(𝒪_X) be supported on T. Then K is pseudo-coherent if and only if K = hocolim Kₙ for a system F of perfect objects Kₙ, each supported on T, such that τ_{≥ -n} Kₙ ⟶ τ_{≥ -n} K is an isomorphism for every n; here c n : Kₙ ⟶ K are the coprojections of the homotopy colimit. The derived category is an arbitrary model of D(𝒪_X).

theorem isPseudoCoherent_iff_exists_supported_perfect_hocolim (X : Scheme.{u})
    [CompactSpace X] [QuasiSeparatedSpace X] [h : HasDerivedCategory.{w} X.Modules]
    (T : Set X) (hT : IsClosed T) (hTc : IsCompact Tᶜ) (K : DerivedCategory X.Modules)
    (hK : @Stacks.Cohomology.PushforwardRestriction.CohomologySupportedOn _ X.ringCatSheaf h T K) :
    @RingedSpace.IsPseudoCoherent X.toRingedSpace h K ↔
      ∃ (F : ℕ ⥤ DerivedCategory X.Modules) (_ : HasCoproduct F.obj) (c : ∀ n, F.obj n ⟶ K),
        (∀ n, @Stacks.Cohomology.PerfectComplexes.IsPerfect X.toRingedSpace h (F.obj n)) ∧
        (∀ n, @Stacks.Cohomology.PushforwardRestriction.CohomologySupportedOn _ X.ringCatSheaf h
          T (F.obj n)) ∧
        IsHomotopyColimitWith F K c ∧
        ∀ n : ℕ, IsIso ((DerivedCategory.TStructure.t.truncGE (-(n : ℤ))).map (c n))

Sources

• Section 36.19, Tag 0DJM
• AxiomMath/Stacks at 5ed82d14

LeanStacks.PseudoCoherentHocolim.isPseudoCoherent_iff_exists_perfect_hocolim · Stacks.PseudoCoherentHocolim.isPseudoCoherent_iff_exists_supported_perfect_hocolim

Section36.20 An example equivalence#

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

Tag 0CS8, an equation

Tag 0CS8 in the Stacks Project.

Stacks.AlgebraicGeometry.ProjectiveGenerator.twistSum, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ProjectiveGeneratorAlgebra.lean, line 136.

The direct sum 𝒪_X ⊕ 𝒪_X(-1) ⊕ ⋯ ⊕ 𝒪_X(-n) of the n + 1 nonpositive twists of the structure sheaf of X = ℙⁿ_A.

public def twistSum : (projectiveSpaceOverRing n (.of A)).Modules

Tag 0CS9, an equation

Tag 0CS9 in the Stacks Project.

Stacks.AlgebraicGeometry.ProjectiveGenerator.matrixRingEquivEnd, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ProjectiveGeneratorHomGroups.lean, line 683.

[Stacks, Tag 0CS9]: R = Hom_{𝒪_X}(P, P). On X = ℙⁿ_A = Proj A[X₀, …, Xₙ], the ring of upper triangular (n + 1) × (n + 1) matrices whose (i, j) entry is homogeneous of degree j - i — S₀ on the diagonal, S₁ above it, and so on — is the endomorphism ring of P = 𝒪_X ⊕ 𝒪_X(-1) ⊕ ⋯ ⊕ 𝒪_X(-n), the (i, j) entry acting as the component 𝒪_X(-j) ⟶ 𝒪_X(-i) by multiplication.

public def matrixRingEquivEnd : endomorphismMatrices A n ≃+* End (projTwistSum A n)

Tag 0BQU, a lemma

Tag 0BQU in the Stacks Project.

Stacks.AlgebraicGeometry.ProjectiveGenerator.twistSum_tensorDerived_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ProjectiveSpaceExampleEquivalence.lean, line 399. The attribute's comment: “RESTRICTED. UNCONDITIONAL HERE is the assembly of Beilinson's argument at X = ℙⁿ_A with P the twist sum of Tag 0CS8 placed in degree zero: the adjunction - ⊗_E^𝐋 P ⊣ RHom(P, -) of Tag 09LY, supplied by its carrier AlgebraicGeometry.RingedSite.tensorWithComplexDerived_adj_derivedHomWithComplex, together with the commutation of RHom(P, -) with the translation that the adjunction induces (derivedHomWithComplexCommShift); the dévissage of Tag 0FQE, supplied by its carrier DifferentialGradedModule.General.property_of_coproducts_of_two_out_of_three_of_shifts; the direct sums of D(E), supplied by DifferentialGradedModule.General.hasCoproducts_derivedCategory; the weak generation of D(E) by the regular module, proved here as isWeakTriangulatedGenerator_q_regularModule, the independent-universe cone-triangle form of DifferentialGradedModule.isWeakTriangulatedGenerator_q_regularModule; full faithfulness by Tag 09LZ; the conversion of the weak-generator property of P into the kernel condition hker of Tag 09J1 (isZero_of_isZero_derivedHom); and the conclusion by Tag 09J1 that the functor - ⊗_E^𝐋 P of Tag 09LX is an equivalence of categories and is exact. The clause 'sending R to P' is twistSumTensorDerivedObjRegularIso. NOT PROVED: the identification of E = Hom^dg(P, P) with the upper triangular matrix algebra R of Tag 0CS9, so the source category is D(E) and not D(R); and A-linearity, the library supplying no A-linear structure on D(E), the ground ring of the differential graded category of complexes on a ringed site being ℤ by Tag 09L9. CARRIED HYPOTHESES. (i) hKgen, that P weakly generates D(O_X). This is exactly the conclusion of Tag 0A9V, which this library has as Stacks.AlgebraicGeometry.ExampleGenerator.isWeakTriangulatedGenerator_twistSum_of_twists and which is itself conditional: it carries hvanish, the vanishing criterion the source obtains from Tag 0BQR applied to the ample invertible sheaf O_X(1) of Tag 01Q2. Tag 0BQR has no carrier in this library, so it is carried as a declared hypothesis here and is neither proved nor duplicated. Tag 0A9V is moreover stated for the locally small model of the derived category of SheafOfModules (projRingSheaf (polyGrading A n)) and for the whole of D(O_X), whereas the functor of Tag 09LX is formed in the standard derived category of the ambient module category of the ringed site and the source's statement is about D_QCoh(O_X), which is also the scope on which hvanish is available from Tag 0BQR; neither identification is made here, so no transport of Tag 0A9V is claimed and hKgen is taken in the model in which the functor lives. (ii) The three inputs of Tag 09LZ this library does not discharge. The exactness of RHom(P, -): Mathlib's CategoryTheory.Adjunction.isTriangulated_rightAdjoint would give it from the exactness of - ⊗_E^𝐋 P, but that is the second conjunct of the conclusion here, and the independent route AlgebraicGeometry.RingedSite.tensorWithComplexDerived_isTriangulated needs the exactness of - ⊗_E P on K(Mod_E), which Tag 09LW supplies only against the pretriangulated structure whose distinguished triangles come from admissible short exact sequences, whereas D(E) and the dévissage of Tag 0FQE are read in the structure whose distinguished triangles are the cone triangles, the two classes agreeing by Tag 09KH, which this library does not formalize. The commutation of RHom(P, -) with direct sums, which is the only use the source's proof makes of its hypothesis (1) that P represents a compact object of D(O_X). And hExt, hypothesis (2) of Tag 09LZ that E computes the ext groups of P”.

Stacks 0BQU, with the matrix description of the endomorphism algebra and A-linearity omitted and the inputs of Tag 09LZ and Tag 0A9V carried. "Let A be a ring. Let X = ℙⁿ_A = Proj(S) where S = A[X₀, …, Xₙ]. With P as in Tag 0CS8 and R as in Tag 0CS9 the functor - ⊗_R^𝐋 P : D(R) ⟶ D_QCoh(𝒪_X) is an A-linear equivalence of triangulated categories sending R to P."

What is proved: for P the twist sum of Tag 0CS8 on ℙⁿ_A, placed in degree zero, and E = Hom^{dg}(P, P) its endomorphism differential graded algebra, the functor - ⊗_E^𝐋 P of Tag 09LX is an equivalence of categories and is exact. The image of the regular module is P, which is Stacks.AlgebraicGeometry.ProjectiveGenerator.twistSumTensorDerivedObjRegularIso.

What is not: the identification E = R with the upper triangular matrix algebra of Tag 0CS9, which this library does not have, so the source category is D(E) rather than D(R); and A-linearity, for which the library supplies no A-linear structure on D(E). The carried hypotheses are the three inputs of Tag 09LZ this library does not discharge — the exactness of RHom(P, -), its commutation with direct sums and hExt — together with hKgen, the weak generation of D(𝒪_X) by P, which is the conclusion of Tag 0A9V; see the module's implementation notes for why Tag 0A9V is carried rather than applied. The adjunction of Tag 09LY, the dévissage of Tag 0FQE, the direct sums of D(E) and the weak generation of D(E) by the regular module are not carried: each is supplied by a carrier of this library.

theorem twistSum_tensorDerived_isEquivalence
    [(derivedHomWithComplex.{u, u, u, u, u} (projectiveSpaceSite A n)
      (twistSumComplex A n)).IsTriangulated]
    [∀ ι : Type u, PreservesColimitsOfShape (Discrete ι)
      (derivedHomWithComplex.{u, u, u, u, u} (projectiveSpaceSite A n)
        (twistSumComplex A n))]
    (hExt : ∀ m : ℤ, Function.Bijective
      (fun f : repRegularDerived.{u, u, u, u, u} (projectiveSpaceSite A n)
            (twistSumComplex A n) ⟶
          (repRegularDerived.{u, u, u, u, u} (projectiveSpaceSite A n)
            (twistSumComplex A n))⟦m⟧ =>
        (tensorWithComplexDerived.{u, u, u, u, u, 0} (projectiveSpaceSite A n) ℤ
          (twistSumComplex A n)).map f))
    (hKgen : (ObjectProperty.singleton (DerivedCategory.Q.obj
      (liftComplex.{u, u, u, u, u} (projectiveSpaceSite A n)
        (twistSumComplex A n)))).IsWeakTriangulatedGenerator) :
    (tensorWithComplexDerived.{u, u, u, u, u, 0} (projectiveSpaceSite A n) ℤ
        (twistSumComplex A n)).IsEquivalence ∧
      (tensorWithComplexDerived.{u, u, u, u, u, 0} (projectiveSpaceSite A n) ℤ
        (twistSumComplex A n)).IsTriangulated

Stacks.AlgebraicGeometry.ProjectiveGenerator.twistSumTensorDerivedObjRegularIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ProjectiveSpaceExampleEquivalence.lean, line 432. The attribute's comment: “the clause 'sending R to P', with the regular module read over E = Hom^dg(P, P) rather than over the upper triangular matrix algebra R of Tag 0CS9, the identification E = R not being available in this library”.

Stacks 0BQU, the clause "sending R to P": the derived tensor product with the twist sum sends the regular module of its endomorphism differential graded algebra to the twist sum itself.

This is AlgebraicGeometry.RingedSite.tensorWithComplexDerivedObjRegularIso at X = ℙⁿ_A and K = P. The source writes the regular module as R, which this library does not identify with the matrix algebra of Tag 0CS9; it is here the regular module over E = Hom^{dg}(P, P).

def twistSumTensorDerivedObjRegularIso :
    (tensorWithComplexDerived.{u, u, u, u, u, 0} (projectiveSpaceSite A n) ℤ
        (twistSumComplex A n)).obj
        ((quasiIsomorphisms (RingedSite.Rep.{u, u, u, u, u, 0} (projectiveSpaceSite A n) ℤ
            (twistSumComplex A n)).algebra).Q.obj
          ((toHomotopyCategory (RingedSite.Rep.{u, u, u, u, u, 0} (projectiveSpaceSite A n) ℤ
              (twistSumComplex A n)).algebra).obj
            ((RingedSite.Rep.{u, u, u, u, u, 0} (projectiveSpaceSite A n) ℤ
                (twistSumComplex A n)).functor.obj
              (liftComplex.{u, u, u, u, u} (projectiveSpaceSite A n)
                (twistSumComplex A n))))) ≅
      DerivedCategory.Q.obj (liftComplex.{u, u, u, u, u} (projectiveSpaceSite A n)
        (twistSumComplex A n))

Stacks.AlgebraicGeometry.Beilinson.beilinson_equivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/ExampleGenerator/BeilinsonEquivalenceLinear.lean, line 320.

[Stacks, Tag 0BQU] (Beilinson). Let A be a ring, X = P^n_A = Proj A[T₀, …, Tₙ], P = 𝒪_X ⊕ 𝒪_X(-1) ⊕ ⋯ ⊕ 𝒪_X(-n) and R = Hom_{𝒪_X}(P, P), read as in the source as the differential graded algebra Hom_{Comp^dg(𝒪_X)}(P, P) with zero differential. Then - ⊗_R^𝐋 P : D(R) ⥤ D_QCoh(𝒪_X) is an A-linear equivalence of triangulated categories sending R to P.

theorem beilinson_equivalence :
    (tensorWithGenerator A n).IsEquivalence ∧ (tensorWithGenerator A n).IsTriangulated ∧
      Nonempty ((tensorWithGenerator A n).obj (regular A n) ≅ twistSumQCoh A n) ∧
      letI := derivedCategoryRLinear A n
      letI := quasiCoherentDerivedCategoryLinear A n
      (tensorWithGenerator A n).Linear A

Sources

• Section 36.20, Tag 0CS7
• AxiomMath/Stacks at 5ed82d14

LeanStacks.AlgebraicGeometry.ProjectiveGenerator.twistSum · Stacks.AlgebraicGeometry.ProjectiveGenerator.matrixRingEquivEnd · Stacks.AlgebraicGeometry.ProjectiveGenerator.twistSum_tensorDerived_isEquivalence · Stacks.AlgebraicGeometry.ProjectiveGenerator.twistSumTensorDerivedObjRegularIso · Stacks.AlgebraicGeometry.Beilinson.beilinson_equivalence

Section36.21 The coherator revisited#

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

Tag 0CR0, a lemma

Tag 0CR0 in the Stacks Project.

Stacks.Duality.Coherator.isLeftAdjoint_quasiCoherentι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactGeneration/QcqsCoherator.lean, line 183.

Let X be a quasi-compact and quasi-separated scheme. The inclusion functor D_QCoh(𝒪_X) ⥤ D(𝒪_X) has a right adjoint DQ_X.

theorem isLeftAdjoint_quasiCoherentι : (quasiCoherentι X).IsLeftAdjoint

Stacks.Duality.Coherator.exists_isTriangulated_rightAdjoint_quasiCoherentι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactGeneration/QcqsCoherator.lean, line 190. The attribute's comment: “the coherator is exact”.

For a quasi-compact quasi-separated scheme X the inclusion D_QCoh(𝒪_X) ⥤ D(𝒪_X) has a right adjoint DQ_X together with a Functor.CommShift ℤ structure making the adjunction triangulated.

theorem exists_isTriangulated_rightAdjoint_quasiCoherentι :
    ∃ (DQ : DerivedCategory X.Modules ⥤ quasiCoherentDerivedCategory X)
      (adj : quasiCoherentι X ⊣ DQ) (_ : DQ.CommShift ℤ), adj.IsTriangulated

Tag 0CR1, a lemma

Tag 0CR1 in the Stacks Project.

Stacks.Duality.coheratorDerivedPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/Coherator/DerivedPushforwardCommutation.lean, line 132.

Derived direct image commutes with the coherator. Let f : X ⟶ Y be a morphism of schemes along which Rf_* preserves quasi-coherence of cohomology — as it does whenever f is quasi-compact and quasi-separated, by [Stacks, Tag 08D5] part (1) — and suppose the inclusions D_QCoh ⥤ D admit right adjoints DQ_X and DQ_Y on X and on Y. Then the two functors D(𝒪_X) ⥤ D_QCoh(𝒪_Y) given by Rf_* ∘ DQ_X and by DQ_Y ∘ Rf_* are canonically isomorphic.

Both are right adjoint to Lf^* : D_QCoh(𝒪_Y) ⥤ D(𝒪_X), which lands in D_QCoh(𝒪_X) by [Stacks, Tag 08DW] part (1), so they are identified by uniqueness of right adjoints.

def coheratorDerivedPushforwardIso :
    DQX ⋙ quasiCoherentDerivedPushforward f hpush ≅ derivedPushforward f ⋙ DQY

Stacks.Duality.coheratorDerivedPushforwardIsoOfQcqs, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/Coherator/DerivedPushforwardCommutationQcqs.lean, line 63.

Derived direct image commutes with the coherator. Let f : X ⟶ Y be a quasi-compact and quasi-separated morphism of schemes and suppose the inclusions D_QCoh ⥤ D admit right adjoints DQ_X and DQ_Y on X and on Y. Then

Rf_* ∘ DQ_X ≅ DQ_Y ∘ Rf_*

as functors D(𝒪_X) ⥤ D_QCoh(𝒪_Y).

This is Stacks.Duality.coheratorDerivedPushforwardIso with its preservation hypothesis discharged: for a quasi-compact and quasi-separated morphism Rf_* sends D_QCoh(𝒪_X) into D_QCoh(𝒪_Y), which is part (1) of [Stacks, Tag 08D5] in the form Stacks.Duality.isQuasicoherent_homology_derivedPushforward.

def coheratorDerivedPushforwardIsoOfQcqs :
    DQX ⋙ quasiCoherentDerivedPushforward f (isQuasicoherent_homology_derivedPushforward f) ≅
      derivedPushforward f ⋙ DQY

Tag 0CR2, a remark

Tag 0CR2 in the Stacks Project.

Stacks.Duality.Coherator.mayerVietorisTriangle, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/Coherator/MayerVietorisTriangle.lean, line 186. The attribute's comment: “the canonical triangle, as data”.

The canonical triangle

DQ_X(K) ⟶ Rj_{U,*}DQ_U(K|_U) ⊕ Rj_{V,*}DQ_V(K|_V) ⟶ Rj_{U ∩ V,*}DQ_{U ∩ V}(K|_{U ∩ V}) ⟶

attached to a scheme X, two opens U, V of X, coherators DQ_X, DQ_U, DQ_V, DQ_{U ∩ V} with DQ_X commuting with the shift, an object K of D(𝒪_X), and the last two maps mor₂, mor₃ of the Mayer--Vietoris triangle of [Stacks, Tag 08BV] for the cover X = U ∪ V.

It is the image under DQ_X of that Mayer--Vietoris triangle, conjugated by Stacks.Duality.Coherator.mayerVietorisMiddleIso and Stacks.Duality.Coherator.mayerVietorisThirdIso: the first map is DQ_X of the canonical biprod.lift of the two units of j_W^* ⊣ Rj_{W,*} followed by the middle identification, the second is DQ_X(mor₂) read through both identifications, and the third is DQ_X(mor₃) read through the third identification and the commutation of DQ_X with the shift.

def mayerVietorisTriangle [DQX.CommShift ℤ]
    (mor₂ : restrictPushforward U K ⊞ restrictPushforward V K ⟶ restrictPushforward (U ⊓ V) K)
    (mor₃ : restrictPushforward (U ⊓ V) K ⟶ K⟦(1 : ℤ)⟧) :
    Triangle (quasiCoherentDerivedCategory X)

Stacks.Duality.Coherator.mayerVietorisTriangle_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/Coherator/MayerVietorisTriangle.lean, line 242. The attribute's comment: “the distinguished triangle of the tag, over arbitrary coherators”.

Let X be a quasi-compact and quasi-separated scheme, let X = U ∪ V with U and V quasi-compact open, and let DQ_X, DQ_U, DQ_V, DQ_{U ∩ V} be coherators — right adjoints of the inclusions D_QCoh ⥤ D. Then for every object K of D(𝒪_X) there is a distinguished triangle

DQ_X(K) ⟶ Rj_{U,*}DQ_U(K|_U) ⊕ Rj_{V,*}DQ_V(K|_V) ⟶ Rj_{U ∩ V,*}DQ_{U ∩ V}(K|_{U ∩ V}) ⟶

in D_QCoh(𝒪_X).

theorem mayerVietorisTriangle_distinguished (hUV : U ⊔ V = ⊤) :
    ∃ (f : DQX.obj K ⟶
          coheratorPushforwardOpens U DQU K ⊞ coheratorPushforwardOpens V DQV K)
      (g : coheratorPushforwardOpens U DQU K ⊞ coheratorPushforwardOpens V DQV K ⟶
          coheratorPushforwardOpens (U ⊓ V) DQUV K)
      (h : coheratorPushforwardOpens (U ⊓ V) DQUV K ⟶ (DQX.obj K)⟦(1 : ℤ)⟧),
      Triangle.mk f g h ∈ distTriang (quasiCoherentDerivedCategory X)

Stacks.Duality.Coherator.exists_distTriang_rightAdjoint_quasiCoherentι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/Coherator/QcqsMayerVietorisTriangle.lean, line 118. The attribute's comment: “the distinguished triangle at the coherators of X, U, V and U ∩ V supplied by Tag 0CR0”.

[Stacks, Tag 0CR2]. Let X be a quasi-compact and quasi-separated scheme covered by two quasi-compact opens, X = U ∪ V, and write DQ_Z for the coherator of Z, the right adjoint of the inclusion D_QCoh(𝒪_Z) ⥤ D(𝒪_Z) whose existence for Z quasi-compact and quasi-separated is [Stacks, Tag 0CR0] (Stacks.Duality.Coherator.isLeftAdjoint_quasiCoherentι). Then for every object K of D(𝒪_X) there is a distinguished triangle

DQ_X(K) ⟶ Rj_{U,*}DQ_U(K|_U) ⊕ Rj_{V,*}DQ_V(K|_V) ⟶ Rj_{U ∩ V,*}DQ_{U ∩ V}(K|_{U ∩ V}) ⟶

in D_QCoh(𝒪_X).

The four coherators are the ones [Stacks, Tag 0CR0] produces at X, U, V and U ∩ V: the three opens are quasi-compact — U ∩ V because X is quasi-separated — and quasi-separated, being opens of a quasi-separated scheme. The triangle is then Stacks.Duality.Coherator.mayerVietorisTriangle_distinguished at those coherators.

theorem exists_distTriang_rightAdjoint_quasiCoherentι (hUV : U ⊔ V = ⊤)
    (K : DerivedCategory X.Modules) :
    letI := isLeftAdjoint_quasiCoherentι X
    letI := isLeftAdjoint_quasiCoherentι U.toScheme
    letI := isLeftAdjoint_quasiCoherentι V.toScheme
    letI := isLeftAdjoint_quasiCoherentι (U ⊓ V).toScheme
    ∃ (f : (quasiCoherentι X).rightAdjoint.obj K ⟶
          coheratorPushforwardOpens U (quasiCoherentι U.toScheme).rightAdjoint K ⊞
            coheratorPushforwardOpens V (quasiCoherentι V.toScheme).rightAdjoint K)
      (g : coheratorPushforwardOpens U (quasiCoherentι U.toScheme).rightAdjoint K ⊞
            coheratorPushforwardOpens V (quasiCoherentι V.toScheme).rightAdjoint K ⟶
          coheratorPushforwardOpens (U ⊓ V) (quasiCoherentι (U ⊓ V).toScheme).rightAdjoint K)
      (h : coheratorPushforwardOpens (U ⊓ V) (quasiCoherentι (U ⊓ V).toScheme).rightAdjoint K ⟶
          ((quasiCoherentι X).rightAdjoint.obj K)⟦(1 : ℤ)⟧),
      Triangle.mk f g h ∈ distTriang (quasiCoherentDerivedCategory X)

Stacks.Duality.Coherator.exists_coherator_distTriang, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/Coherator/QcqsMayerVietorisTriangle.lean, line 156. The attribute's comment: “coherators of the four schemes exist and the triangle of the tag is distinguished for them”.

[Stacks, Tag 0CR2], in existential form. For a quasi-compact quasi-separated scheme X covered by two quasi-compact opens, X = U ∪ V, there are coherators DQ_X, DQ_U, DQ_V, DQ_{U ∩ V} of X, U, V and U ∩ V — right adjoints of the inclusions D_QCoh(𝒪_Z) ⥤ D(𝒪_Z), [Stacks, Tag 0CR0] — such that every object K of D(𝒪_X) sits in a distinguished triangle

DQ_X(K) ⟶ Rj_{U,*}DQ_U(K|_U) ⊕ Rj_{V,*}DQ_V(K|_V) ⟶ Rj_{U ∩ V,*}DQ_{U ∩ V}(K|_{U ∩ V}) ⟶

in D_QCoh(𝒪_X). A coherator is unique up to a canonical isomorphism, so this is the same assertion as Stacks.Duality.Coherator.exists_distTriang_rightAdjoint_quasiCoherentι, read without naming the right adjoints.

theorem exists_coherator_distTriang (hUV : U ⊔ V = ⊤) :
    ∃ (DQX : DerivedCategory X.Modules ⥤ quasiCoherentDerivedCategory X)
      (DQU : DerivedCategory U.toScheme.Modules ⥤ quasiCoherentDerivedCategory U.toScheme)
      (DQV : DerivedCategory V.toScheme.Modules ⥤ quasiCoherentDerivedCategory V.toScheme)
      (DQUV : DerivedCategory (U ⊓ V).toScheme.Modules ⥤
        quasiCoherentDerivedCategory (U ⊓ V).toScheme)
      (_ : quasiCoherentι X ⊣ DQX) (_ : quasiCoherentι U.toScheme ⊣ DQU)
      (_ : quasiCoherentι V.toScheme ⊣ DQV) (_ : quasiCoherentι (U ⊓ V).toScheme ⊣ DQUV),
      ∀ K : DerivedCategory X.Modules,
        ∃ (f : DQX.obj K ⟶
              coheratorPushforwardOpens U DQU K ⊞ coheratorPushforwardOpens V DQV K)
          (g : coheratorPushforwardOpens U DQU K ⊞ coheratorPushforwardOpens V DQV K ⟶
              coheratorPushforwardOpens (U ⊓ V) DQUV K)
          (h : coheratorPushforwardOpens (U ⊓ V) DQUV K ⟶ (DQX.obj K)⟦(1 : ℤ)⟧),
          Triangle.mk f g h ∈ distTriang (quasiCoherentDerivedCategory X)

Tag 0CSA, a lemma

Tag 0CSA in the Stacks Project.

Stacks.Duality.Coherator.exists_isGE_isLE_coherator_obj_of_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/Coherator/UnconditionalBoundedness.lean, line 401.

[Stacks, Tag 0CSA]. Let X be a quasi-compact and quasi-separated scheme and let DQ_X : D(𝒪_X) ⥤ D_QCoh(𝒪_X) be a coherator of X, i.e. a right adjoint of the inclusion ι : D_QCoh(𝒪_X) ⥤ D(𝒪_X) with the adjunction triangulated — the exact functor DQ_X of [Stacks, Tag 0CR0]. Then there is an integer N, depending only on X and on DQ_X and in particular not on K, a or b, such that for every object K of D(𝒪_X) and all integers a, b, if H^i(U, K) = 0 for every affine open U ⊆ X and every i ∉ [a, b], then the cohomology sheaves H^i(DQ_X(K)) vanish for i ∉ [a, b + N].

This is Stacks.Duality.Coherator.exists_isGE_isLE_coherator_obj, the source's induction over the quasi-compact opens of X ([Stacks, Tag 08DR]), with its three inputs supplied: the two Mayer–Vietoris triangles of [Stacks, Tag 08BV] are Stacks.Duality.Coherator.isMayerVietorisApex_restrictPushforward_sup and Stacks.Duality.Coherator.isMayerVietorisApex_self, and the affine base case is Stacks.Duality.Coherator.hasCoheratorBoundAt_of_isAffineOpen.

theorem exists_isGE_isLE_coherator_obj_of_qcqs (X : Scheme.{u}) [CompactSpace X]
    [QuasiSeparatedSpace X]
    (DQ : DerivedCategory X.Modules ⥤ quasiCoherentDerivedCategory X)
    (adj : quasiCoherentι X ⊣ DQ) [DQ.CommShift ℤ] [adj.IsTriangulated] :
    ∃ N : ℤ, ∀ (a b : ℤ) (K : DerivedCategory X.Modules), AffineAmplitudeIn X a b K →
      ((quasiCoherentι X).obj (DQ.obj K)).IsGE a ∧
        ((quasiCoherentι X).obj (DQ.obj K)).IsLE (b + N)

Tag 0CSB, an example

Tag 0CSB in the Stacks Project.

AlgebraicGeometry.isZero_cohomology_of_isDerivedLimit_single_of_isAffineOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/Coherator/InverseLimitAffineCohomology.lean, line 110. The attribute's comment: “the cohomology computation on an affine open: H^i(U, R lim 𝓕ₙ) = 0 for i outside [0, 1]”.

[Stacks, Tag 0CSB]. Let X be a scheme, let (𝓕ₙ) be an inverse system of quasi-coherent 𝒪_X-modules and let L be a derived limit in D(𝒪_X) of the system (𝓕ₙ) placed in degree zero. Then H^i(U, L) = 0 for every affine open U ⊆ X and every i outside [0, 1].

Sections over U commute with derived limits, so RΓ(U, L) = R lim RΓ(U, 𝓕ₙ), and each RΓ(U, 𝓕ₙ) is concentrated in degree zero because 𝓕ₙ is quasi-coherent and U is affine. In the Milnor short exact sequence 0 → lim¹ H^{i-1}(U, 𝓕ₙ) → H^i(U, L) → lim H^i(U, 𝓕ₙ) → 0 both outer terms then vanish as soon as i ≠ 0 and i ≠ 1.

theorem isZero_cohomology_of_isDerivedLimit_single_of_isAffineOpen (X : Scheme.{u})
    (𝓕 : ℕᵒᵖ ⥤ X.Modules) (hqc : ∀ n : ℕ, (𝓕.obj ⟨n⟩).IsQuasicoherent)
    [HasProduct fun n : ℕ ↦ (𝓕 ⋙ DerivedCategory.singleFunctor X.Modules 0).obj ⟨n⟩]
    (L : DerivedCategory.{u + 1} X.Modules)
    (hL : IsDerivedLimit (𝓕 ⋙ DerivedCategory.singleFunctor X.Modules 0) L)
    (U : X.Opens) (hU : IsAffineOpen U) (i : ℤ) (hi0 : i ≠ 0) (hi1 : i ≠ 1) :
    IsZero ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} i).obj
      ((derivedSectionsOverObject (schemeOpensRingedSite X) U).obj L))

Stacks.Duality.Coherator.exists_isGE_isLE_coherator_obj_of_isDerivedLimit_single, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/Coherator/InverseLimitBounded.lean, line 185. The attribute's comment: “the conclusion that the R lim in D_QCoh(𝒪_X), i.e. DQ_X(R lim 𝓕ₙ), lies in D^b_QCoh(𝒪_X), for every coherator DQ of X”.

[Stacks, Tag 0CSB]. Let X be a quasi-compact and quasi-separated scheme, let DQ be a coherator of X and let L be a derived limit in D(𝒪_X) of an inverse system (𝓕ₙ) of quasi-coherent 𝒪_X-modules placed in degree zero. Then DQ L lies in D^b_QCoh(𝒪_X): its cohomology sheaves vanish below degree 0 and above degree 1 + N for some N depending only on X and DQ.

The affine amplitude of L is [0, 1], so this is the boundedness property of the coherator, [Stacks, Tag 0CSA] in the form Stacks.Duality.Coherator.exists_isGE_isLE_coherator_obj_of_qcqs, applied with a = 0 and b = 1.

theorem exists_isGE_isLE_coherator_obj_of_isDerivedLimit_single (X : Scheme.{u})
    [CompactSpace X] [QuasiSeparatedSpace X]
    (DQ : DerivedCategory X.Modules ⥤ quasiCoherentDerivedCategory X)
    (adj : quasiCoherentι X ⊣ DQ) [DQ.CommShift ℤ] [adj.IsTriangulated]
    (𝓕 : ℕᵒᵖ ⥤ X.Modules) (hqc : ∀ n : ℕ, (𝓕.obj ⟨n⟩).IsQuasicoherent)
    [HasProduct fun n : ℕ ↦ (𝓕 ⋙ DerivedCategory.singleFunctor X.Modules 0).obj ⟨n⟩]
    (L : DerivedCategory X.Modules)
    (hL : IsDerivedLimit (𝓕 ⋙ DerivedCategory.singleFunctor X.Modules 0) L) :
    ∃ N : ℤ, ((quasiCoherentι X).obj (DQ.obj L)).IsGE 0 ∧
      ((quasiCoherentι X).obj (DQ.obj L)).IsLE (1 + N)

Stacks.Duality.Coherator.isDerivedLimit_coherator_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/Coherator/InverseLimitQuasiCoherent.lean, line 147. The attribute's comment: “the identification DQ_X(R lim 𝓕ₙ) = (R lim in D_QCoh(𝒪_X))(𝓕ₙ), for every coherator DQ of X, i.e. every exact right adjoint of the inclusion; one exists on any quasi-compact quasi-separated scheme by Stacks 0CR0, Stacks.Duality.Coherator.exists_isTriangulated_rightAdjoint_quasiCoherentι”.

[Stacks, Tag 0CSB]. Let X be a scheme and let DQ be a right adjoint of the inclusion D_QCoh(𝒪_X) ⥤ D(𝒪_X) which makes the adjunction triangulated. If L is a derived limit in D(𝒪_X) of an inverse system F of objects of D_QCoh(𝒪_X), then DQ L is a derived limit of F in D_QCoh(𝒪_X).

Right adjoints preserve products, so DQ preserves the product of the system; it is exact, so it carries the triangle witnessing the derived limit to one of the same shape. The inclusion is fully faithful, so the unit of the adjunction identifies F ⋙ ι ⋙ DQ with F.

theorem isDerivedLimit_coherator_obj
    (DQ : DerivedCategory (SheafOfModules.{u} X.ringCatSheaf) ⥤
      (derivedQuasiCoherent X).FullSubcategory)
    (adj : (derivedQuasiCoherent X).ι ⊣ DQ) [DQ.CommShift ℤ] [adj.IsTriangulated]
    (F : ℕᵒᵖ ⥤ (derivedQuasiCoherent X).FullSubcategory)
    [HasProduct fun n : ℕ ↦ (F ⋙ (derivedQuasiCoherent X).ι).obj (op n)]
    (L : DerivedCategory (SheafOfModules.{u} X.ringCatSheaf))
    (hL : IsDerivedLimit (F ⋙ (derivedQuasiCoherent X).ι) L) :
    ∃ h : HasProduct fun n : ℕ ↦ F.obj (op n),
      letI := h
      IsDerivedLimit F (DQ.obj L)

Sources

• Section 36.21, Tag 0CQZ
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Duality.Coherator.isLeftAdjoint_quasiCoherentι · Stacks.Duality.Coherator.exists_isTriangulated_rightAdjoint_quasiCoherentι · Stacks.Duality.coheratorDerivedPushforwardIso · Stacks.Duality.coheratorDerivedPushforwardIsoOfQcqs · Stacks.Duality.Coherator.mayerVietorisTriangle · Stacks.Duality.Coherator.mayerVietorisTriangle_distinguished · Stacks.Duality.Coherator.exists_distTriang_rightAdjoint_quasiCoherentι · Stacks.Duality.Coherator.exists_coherator_distTriang

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.