36.39 Determinants of complexes to 36.41 Quasi-coherent objects in…

Section36.39 Determinants of complexes#

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

Tag 0FJX, a lemma

Tag 0FJX in the Stacks Project.

AlgebraicGeometry.DeterminantTwoTerm.specDet, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeterminantTwoTermAffine.lean, line 285. The attribute's comment: “the determinant functor, for an affine scheme”.

The determinant functor on Spec R, from the groupoid of perfect objects of D(𝒪_{Spec R}) of Tor amplitude in [-1, 0] and their isomorphisms to the groupoid of invertible 𝒪_{Spec R}-modules and their isomorphisms.

It is the determinant of More on Algebra, Section 0FJI, transported along the identification of the source groupoid with the ring-level one and along the associated-sheaf functor.

def specDet (R : CommRingCat.{u}) :
    Core (PerfectTwoTermAmplitude (Spec R)) ⥤ Core (InvertibleModuleCat (Spec R))

AlgebraicGeometry.DeterminantTwoTerm.specDelta, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeterminantTwoTermAffine.lean, line 315. The attribute's comment: “the canonical global section δ(L) of the determinant of a rank-zero object, for an affine scheme”.

The canonical global section δ(L) of the determinant of a rank-zero object of the source groupoid on Spec R: the canonical element of More on Algebra, Section 0FJI, read as a global section.

def specDelta (R : CommRingCat.{u}) (L : PerfectTwoTermAmplitude (Spec R))
    (hL : IsRankZeroSpec R L) : Γ(((specDet R).obj ⟨L⟩).of.obj, ⊤)

AlgebraicGeometry.DeterminantTwoTerm.specDet_map_specDelta, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeterminantTwoTermAffine.lean, line 323. The attribute's comment: “the compatibility det(a)(δ(L)) = δ(K) of the canonical global section with isomorphisms, for an affine scheme”.

For every isomorphism a : L ⟶ K of rank-zero objects of the source groupoid on Spec R, det(a)(δ(L)) = δ(K).

theorem specDet_map_specDelta (R : CommRingCat.{u}) {L K : PerfectTwoTermAmplitude (Spec R)}
    (a : (⟨L⟩ : Core (PerfectTwoTermAmplitude (Spec R))) ⟶ ⟨K⟩)
    (hL : IsRankZeroSpec R L) (hK : IsRankZeroSpec R K) :
    Scheme.Modules.Hom.app
        ((IsInvertibleProperty (Spec R)).ι.map ((specDet R).map a).iso.hom) ⊤
        (specDelta R L hL) = specDelta R K hK

AlgebraicGeometry.DeterminantTwoTerm.specDetPresentationIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeterminantTwoTermAffine.lean, line 337. The attribute's comment: “the construction is locally the one of More on Algebra, Section 0FJI: on an affine scheme the determinant is the determinant line of a two-term finite-projective presentation”.

The determinant on Spec R of an object of the source groupoid is the sheaf associated with the determinant line of More on Algebra, Section 0FJI of any two-term finite-projective presentation of the corresponding complex of R-modules. Such a presentation always exists, TwoTermDeterminant.presentation being one.

def specDetPresentationIso (R : CommRingCat.{u}) (L : PerfectTwoTermAmplitude (Spec R))
    (P : TwoTermPresentation (sourceComplex R L).obj) :
    letI := P.finite (-1)
    letI := P.projective (-1)
    letI := P.finite 0
    letI := P.projective 0
    ((specDet R).obj ⟨L⟩).of.obj ≅
      tilde (ModuleCat.of R
        (TwoTermComplex.determinantLine (P.complex.d (-1) 0).hom))

AlgebraicGeometry.DeterminantTwoTerm.specDetPresentationIso_specDelta, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeterminantTwoTermAffine.lean, line 354. The attribute's comment: “the canonical global section is locally the canonical element of More on Algebra, Section 0FJI: on an affine scheme it is the determinant of the differential of a two-term finite-projective presentation”.

Under the identification of the determinant with the determinant line of a rank-zero two-term finite-projective presentation, the canonical global section is the canonical element of More on Algebra, Section 0FJI of that presentation.

theorem specDetPresentationIso_specDelta (R : CommRingCat.{u})
    (L : PerfectTwoTermAmplitude (Spec R)) (P : TwoTermPresentation (sourceComplex R L).obj)
    (hP : P.IsRankZero) (hL : IsRankZeroSpec R L) :
    letI := P.finite (-1)
    letI := P.projective (-1)
    letI := P.finite 0
    letI := P.projective 0
    Scheme.Modules.Hom.app (specDetPresentationIso R L P).hom ⊤ (specDelta R L hL) =
      (tilde.toOpen (ModuleCat.of R
        (TwoTermComplex.determinantLine (P.complex.d (-1) 0).hom)) ⊤).hom
          (TwoTermComplex.delta (P.complex.d (-1) 0).hom hP)

AlgebraicGeometry.DeterminantTwoTerm.determinantFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeterminantTwoTermGlobal.lean, line 158. The attribute's comment: “part (1): the determinant functor, from the groupoid of perfect objects of Tor amplitude in [-1, 0] and their isomorphisms to the groupoid of invertible modules and their isomorphisms, on an arbitrary scheme”.

The determinant functor on an arbitrary scheme, from the groupoid of perfect objects of D(𝒪_X) of Tor-amplitude in [-1, 0] and their isomorphisms to the groupoid of invertible 𝒪_X-modules and their isomorphisms.

The value at L is the invertible module glued from the determinants of L on the affine opens of X, and the value at an isomorphism is glued from the determinants of its restrictions to the affine charts.

def determinantFunctor (X : Scheme.{u}) :
    Core (PerfectTwoTermAmplitude X) ⥤ Core (InvertibleModuleCat X)

AlgebraicGeometry.DeterminantTwoTerm.determinantSection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeterminantTwoTermGlobal.lean, line 200. The attribute's comment: “part (2): the canonical global section δ(L) of the determinant of a rank-zero object, on an arbitrary scheme”.

The canonical global section δ(L) of the determinant of a rank-zero perfect object of D(𝒪_X) of Tor-amplitude in [-1, 0] on an arbitrary scheme: the global section glued from the canonical elements of More on Algebra, Section 0FJI on the affine charts, which are matched by the chart comparisons.

def determinantSection {L : PerfectTwoTermAmplitude X} (hL : IsRankZeroOn L) :
    Γ(((determinantFunctor X).obj ⟨L⟩).of.obj, ⊤)

AlgebraicGeometry.DeterminantTwoTerm.determinantChartPresentationIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeterminantTwoTermGlobal.lean, line 229. The attribute's comment: “part (3): the construction is affine locally the one of More on Algebra, Section 0FJI — on an affine open of an arbitrary scheme the determinant is the determinant line of a two-term finite-projective presentation of the complex the object restricts to there”.

On an affine open V of an arbitrary scheme X the determinant of L is the sheaf associated with the determinant line of More on Algebra, Section 0FJI of any two-term finite-projective presentation P of the complex of Γ(X, V)-modules that L restricts to on the chart of V: the restriction of the determinant to V is the pullback along AlgebraicGeometry.IsAffineOpen.isoSpec of that associated sheaf.

The isomorphism is the glueing comparison AlgebraicGeometry.AffineOpensGlue.ChartComparison.chartIso of the datum, followed by AlgebraicGeometry.DeterminantTwoTerm.chartDetPresentationIso.

def determinantChartPresentationIso (L : PerfectTwoTermAmplitude X) (V : X.affineOpens)
    (P : TwoTermPresentation (chartComplex L V).obj) :
    letI := P.finite (-1)
    letI := P.projective (-1)
    letI := P.finite 0
    letI := P.projective 0
    Scheme.Modules.restrict ((determinantFunctor X).obj ⟨L⟩).of.obj
        (AffineOpensGlue.chart X V) ≅
      (Scheme.Modules.pullback V.2.isoSpec.hom).obj
        (tilde (ModuleCat.of Γ(X, (V.1 : X.Opens))
          (TwoTermComplex.determinantLine (P.complex.d (-1) 0).hom)))

AlgebraicGeometry.DeterminantTwoTerm.determinantFunctor_map_determinantSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeterminantTwoTermGlobalDelta.lean, line 325. The attribute's comment: “part (2): the compatibility det(a)(δ(L)) = δ(K) of the canonical global section with isomorphisms, on an arbitrary scheme”.

For every isomorphism a : L ⟶ K of rank-zero perfect objects of D(𝒪_X) of Tor-amplitude in [-1, 0] on an arbitrary scheme X, the determinant of a carries the canonical global section of the determinant of L to that of K: det(a)(δ(L)) = δ(K).

theorem determinantFunctor_map_determinantSection {L K : PerfectTwoTermAmplitude X}
    (a : (⟨L⟩ : Core (PerfectTwoTermAmplitude X)) ⟶ ⟨K⟩)
    (hL : IsRankZeroOn L) (hK : IsRankZeroOn K) :
    Scheme.Modules.Hom.app
        ((IsInvertibleProperty X).ι.map ((determinantFunctor X).map a).iso.hom) ⊤
        (determinantSection hL) = determinantSection hK

AlgebraicGeometry.DeterminantTwoTerm.determinantChartPresentationIso_determinantSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeterminantTwoTermGlobalDelta.lean, line 462. The attribute's comment: “part (3): the canonical global section is affine locally the canonical element of More on Algebra, Section 0FJI — on an affine open of an arbitrary scheme it is the determinant of the differential of a two-term finite-projective presentation”.

Let X be a scheme, L a rank-zero perfect object of D(𝒪_X) of Tor-amplitude in [-1, 0], V an affine open of X and P a rank-zero two-term finite-projective presentation of the complex of Γ(X, V)-modules that L restricts to on the chart of V. Then the canonical global section δ(L) of the determinant of L, restricted to V and read on the chart of V through AlgebraicGeometry.DeterminantTwoTerm.chartDetRestrictPresentationIso, is the canonical element of More on Algebra, Section 0FJI of P — the determinant of the differential of P — read as a global section of the associated sheaf of the determinant line and restricted to the image open.

So the construction is affine locally the one of More on Algebra, Section 0FJI, canonical element included: δ(L) reads on an affine open as TwoTermComplex.delta of the differential of any two-term finite-projective presentation there.

theorem determinantChartPresentationIso_determinantSection {L : PerfectTwoTermAmplitude X}
    (hL : IsRankZeroOn L) (V : X.affineOpens)
    (P : TwoTermPresentation (chartComplex L V).obj) (hP : P.IsRankZero) :
    letI := P.finite (-1)
    letI := P.projective (-1)
    letI := P.finite 0
    letI := P.projective 0
    Scheme.Modules.Hom.app (chartDetRestrictPresentationIso L V P).hom
        ((V.1 : X.Opens).ι ⁻¹ᵁ (V.1 : X.Opens))
        ((chartComparison L).chartSec V (V.1 : X.Opens)
          ((chartComparison L).glued.val.map (homOfLE le_top).op (determinantSection hL))) =
      (tilde (ModuleCat.of Γ(X, (V.1 : X.Opens))
          (TwoTermComplex.determinantLine (P.complex.d (-1) 0).hom))).val.map
        (homOfLE (le_top :
          V.2.isoSpec.hom ''ᵁ ((V.1 : X.Opens).ι ⁻¹ᵁ (V.1 : X.Opens)) ≤ ⊤)).op
        ((tilde.toOpen (ModuleCat.of Γ(X, (V.1 : X.Opens))
          (TwoTermComplex.determinantLine (P.complex.d (-1) 0).hom)) ⊤).hom
          (TwoTermComplex.delta (P.complex.d (-1) 0).hom hP))
Tag 0FJY, a remark

Tag 0FJY in the Stacks Project.

AlgebraicGeometry.DeterminantTwoTerm.pullbackDetIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeterminantTwoTermGlobal/PullbackIso.lean, line 334. The attribute's comment: “(b) the canonical identification f^det(K) → det(Lf^K)”.

For a morphism of schemes f : X ⟶ Y and a perfect object K of D(𝒪_Y) of Tor amplitude in [-1, 0], the canonical identification f^* det(K) ≅ det(Lf^*K), adjoint to the glued maps of local determinants (detSectionsEquiv_pullbackDetIso_hom).

def pullbackDetIso :
    (Scheme.Modules.pullback f).obj (detModule K) ≅ detModule (pullbackObj f K)

AlgebraicGeometry.DeterminantTwoTerm.detSectionsEquiv_pullbackDetIso_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeterminantTwoTermGlobal/PullbackIso.lean, line 344. The attribute's comment: “(b) the identification f^det(K) → det(Lf^K) is, over affine opens W ⊆ f⁻¹V, the base change of the determinant of the local avatar of K over V”.

For affine opens V ⊆ Y and W ⊆ f⁻¹V, the identification f^* det(K) ≅ det(Lf^*K) sends the pullback of a section a of det(K) over V to the image of a under the base change det(M_V) → Γ(X, W) ⊗_{Γ(Y, V)} det(M_V) = det(M'_W) of the determinants of More on Algebra, Section 0FJI of the local avatars M_V of K and M'_W of Lf^*K.

theorem detSectionsEquiv_pullbackDetIso_hom (V : Y.affineOpens) (W : X.affineOpens)
    (h : (W : X.Opens) ≤ f ⁻¹ᵁ V) (a : Γ(detModule K, V)) :
    detSectionsEquiv (pullbackObj f K) W ((pullbackDetIso f K).hom.val.app (op W)
        (Scheme.Modules.pullbackSection f (detModule K) V W h a)) =
      pullbackDetMap f K V W h (detSectionsEquiv K V a)

AlgebraicGeometry.DeterminantTwoTerm.pullbackDetIso_hom_deltaSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeterminantTwoTermGlobal/PullbackIso.lean, line 367. The attribute's comment: “(c) if K has rank 0, δ(K) pulls back to δ(Lf^K) via f^det(K) → det(Lf^*K)”.

If K has rank zero, the identification f^* det(K) ≅ det(Lf^*K) carries the pullback of the canonical global section δ(K) to δ(Lf^*K).

theorem pullbackDetIso_hom_deltaSection (hK : IsRankZero K) :
    (pullbackDetIso f K).hom.val.app (op ⊤)
        (Scheme.Modules.pullbackSection f (detModule K) ⊤ ⊤ le_top (deltaSection K hK)) =
      deltaSection (pullbackObj f K) (isRankZero_pullbackObj f K hK)

AlgebraicGeometry.DeterminantTwoTerm.isPerfectTwoTermAmplitude_derivedPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeterminantTwoTermPerfect.lean, line 174. The attribute's comment: “the derived pullback lands in the source category”. References: SGA 6 I (4.19.2), “special case”.

The source category is preserved by derived pullback. For a morphism of schemes f : X ⟶ Y, the derived pullback Lf^*K of a perfect object K of D(𝒪_Y) of Tor amplitude in [-1, 0] is again perfect of Tor amplitude in [-1, 0].

theorem isPerfectTwoTermAmplitude_derivedPullback {X Y : Scheme.{u}} (f : X ⟶ Y)
    (K : DerivedCategory Y.Modules) (hK : IsPerfectTwoTermAmplitude Y K) :
    IsPerfectTwoTermAmplitude X
      ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
        f.toLRSHom.toShHom).obj K)
Sources
LeanAlgebraicGeometry.DeterminantTwoTerm.specDet · AlgebraicGeometry.DeterminantTwoTerm.specDelta · AlgebraicGeometry.DeterminantTwoTerm.specDet_map_specDelta · AlgebraicGeometry.DeterminantTwoTerm.specDetPresentationIso · AlgebraicGeometry.DeterminantTwoTerm.specDetPresentationIso_specDelta · AlgebraicGeometry.DeterminantTwoTerm.determinantFunctor · AlgebraicGeometry.DeterminantTwoTerm.determinantSection · AlgebraicGeometry.DeterminantTwoTerm.determinantChartPresentationIso

Section36.40 Detecting Boundedness#

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

Tag 0GEJ, a lemma

Tag 0GEJ in the Stacks Project.

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

[Stacks, Tag 0GEJ], the implication "Koszul orthogonality implies truncated restriction". Let f₁, …, f_r ∈ A, let U = ⋃ᵢ D(f_i) ⊆ Spec A, let j : U ⟶ Spec A be the inclusion and let K be the sheafified Koszul complex of the sequence. Let E be an object of D_QCoh(𝒪_{Spec A}). If every morphism K⟦-n⟧ ⟶ E vanishes for n ≥ a, then the canonical map E ⟶ Rj_*(E|_U) becomes invertible after truncation in degrees ≥ a.

This is condition (2) of the source implying condition (1), at the source's own index: the premise is at a and the conclusion at a.

The cone N of the unit restricts to zero on U, receives no morphism from K⟦-n⟧ for n ≥ a - 1, and has quasi-coherent cohomology sheaves — the last because E does and Rj_* preserves quasi-coherent cohomology along a quasi-compact open immersion ([Stacks, Tag 08D5]). The graded detection statement Stacks.Koszul.Truncation.isZero_homology_of_forall_hom_koszulObject_eq_zero then kills the homology of N in degrees ≥ a - 1, which is what makes the truncated map invertible. That is where the commutative algebra of the source sits: the Koszul power triangles of [Stacks, Tag 062C], the lifting lemma of [Stacks, Tag 08E3] and the affine comparison D(A) ≌ D_QCoh(𝒪_{Spec A}) of [Stacks, Tag 06Z0]. The two other inputs of the source are proved too: the Koszul object restricts to zero on U by Stacks.Koszul.OpenComplement.isZero_derivedRestrict_koszulObject, and Rj_* is fully faithful by the instance Stacks.Duality.OpenImmersion.isIso_derivedRestrictPushforwardAdjunction_counit_app.

theorem truncGE_restriction_of_hom_koszul_eq_zero
    (E : DerivedCategory (Spec (CommRingCat.of A)).Modules) (hE : qcohSpec A E) (a : ℤ)
    (h : ∀ n : ℤ, a ≤ n → Subsingleton ((koszulObject f)⟦-n⟧ ⟶ E)) :
    IsIso ((DerivedCategory.TStructure.t.truncGE a).map
      ((derivedRestrictPushforwardAdjunction (openComplement f).ι).unit.app E))

Stacks.Koszul.Truncation.hom_koszul_eq_zero_of_truncGE_restriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/KoszulHighDegreeOrthogonality.lean, line 495. The attribute's comment: “(1) implies (2) with a replaced by a + r, not the published a + 1, which is false for r ≥ 2 — see the module docstring for the counterexample over k[x,y]”.

[Stacks, Tag 0GEJ], the implication "truncated restriction implies Koszul orthogonality r degrees up". In the situation above, if the canonical map E ⟶ Rj_*(E|_U) is invertible after truncation in degrees ≥ a, then every morphism K⟦-n⟧ ⟶ E vanishes for n ≥ a + r.

The argument spends the window Stacks.Koszul.Truncation.subsingleton_hom_koszulObject_shift_of_isLE, which is the perfectness of K: K is a bounded complex of finite free modules in degrees -r, …, 0, so Hom(K⟦-m⟧, M) sees only the homology of M in the r + 1 degrees m - r, …, m. It is applied to τ_{≤a-1}E and to τ_{≤a-1}(Rj_*(E|_U)), both of which have quasi-coherent cohomology sheaves — and quasi-coherence is not a convenience here, the window being false without it.

The index is a + r, and the a + 1 of the published statement of the tag is false for r ≥ 2. This is an approved erratum of the Stacks Project, recorded against the tag; the Stacks source text is left as published. The module documentation gives the counterexample over k[x, y], where a + r is sharp.

theorem hom_koszul_eq_zero_of_truncGE_restriction
    (E : DerivedCategory (Spec (CommRingCat.of A)).Modules) (hE : qcohSpec A E) (a : ℤ)
    (h : IsIso ((DerivedCategory.TStructure.t.truncGE a).map
      ((derivedRestrictPushforwardAdjunction (openComplement f).ι).unit.app E))) :
    ∀ n : ℤ, a + (r : ℤ) ≤ n → Subsingleton ((koszulObject f)⟦-n⟧ ⟶ E)
Tag 0GEK, a lemma

Tag 0GEK in the Stacks Project.

Stacks.Koszul.Truncation.truncLE_restriction_of_hom_koszul_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/KoszulTruncatedOrthogonality.lean, line 277. The attribute's comment: “(2) at a+1 implies (1) at a, for E in D_QCoh. This is the corrected reverse implication; the published '(2) at a implies (1) at a' is false: for A = k[x], f = (x), E = 𝒪_X and a = 0 condition (2) holds and (1) fails, see the module documentation”.

Let f₁, …, f_r ∈ A, let U = ⋃ᵢ D(f_i) ⊆ X = Spec A, let j : U ⟶ X be the inclusion and let K be the sheafified Koszul complex of the sequence. Let E be an object of D_QCoh(𝒪_X), that is one whose cohomology sheaves are quasi-coherent. If every morphism K⟦-n⟧ ⟶ E vanishes for n ≤ a + 1, then the canonical map E ⟶ Rj_*(E|_U) is invertible after truncation in degrees ≤ a.

theorem truncLE_restriction_of_hom_koszul_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)
    (a : ℤ)
    (h : ∀ n : ℤ, n ≤ a + 1 → Subsingleton ((koszulObject f)⟦-n⟧ ⟶ E)) :
    IsIso ((DerivedCategory.TStructure.t.truncLE a).map
      ((derivedRestrictPushforwardAdjunction (openComplement f).ι).unit.app E))

Stacks.Koszul.Truncation.hom_koszul_eq_zero_of_truncLE_restriction_sub_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/KoszulTruncatedOrthogonality.lean, line 307. The attribute's comment: “(1) implies (2) with a replaced by a-1, at the source's own index, for E in D_QCoh”.

Let f₁, …, f_r ∈ A, let U = ⋃ᵢ D(f_i) ⊆ X = Spec A, let j : U ⟶ X be the inclusion and let K be the sheafified Koszul complex of the sequence. Let E be an object of D_QCoh(𝒪_X), that is one whose cohomology sheaves are quasi-coherent. If the canonical map E ⟶ Rj_*(E|_U) is invertible after truncation in degrees ≤ a, then every morphism K⟦-n⟧ ⟶ E vanishes for n ≤ a - 1.

theorem hom_koszul_eq_zero_of_truncLE_restriction_sub_one
    (E : DerivedCategory (Spec (CommRingCat.of A)).Modules)
    (_hE : DerivedCategoryB.derivedCategoryB (A := (Spec (CommRingCat.of A)).Modules)
      (SheafOfModules.isQuasicoherent (Spec (CommRingCat.of A)).ringCatSheaf) E)
    (a : ℤ)
    (h : IsIso ((DerivedCategory.TStructure.t.truncLE a).map
      ((derivedRestrictPushforwardAdjunction (openComplement f).ι).unit.app E))) :
    ∀ n : ℤ, n ≤ a - 1 → Subsingleton ((koszulObject f)⟦-n⟧ ⟶ E)
Tag 0GEL, a lemma

Tag 0GEL in the Stacks Project.

Stacks.DerivedQCoh.eventually_subsingleton_hom_iff_truncGE_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DetectingBoundednessOfAPerfectComplex.lean, line 222.

[Stacks, Tag 0GEL]. Let X be a quasi-compact and quasi-separated scheme, let P be a perfect object of D(𝒪_X), let E be an object of D_QCoh(𝒪_X) and let a be an integer. Then

  1. Hom_{D(𝒪_X)}(P⟦-i⟧, E) = 0 for i ≫ 0

if and only if

  1. Hom_{D(𝒪_X)}(P⟦-i⟧, τ_{≥a}E) = 0 for i ≫ 0,

where τ_{≥a} is the canonical truncation of D(𝒪_X) and vanishing of a Hom-group is subsingletonness of the morphism type, the derived category being additive.

Both implications are the truncation triangle τ_{≤a-1}E ⟶ E ⟶ τ_{≥a}E ⟶ (τ_{≤a-1}E)⟦1⟧: a morphism P⟦-i⟧ ⟶ E which dies in τ_{≥a}E factors through τ_{≤a-1}E, and a morphism P⟦-i⟧ ⟶ τ_{≥a}E which dies in (τ_{≤a-1}E)⟦1⟧ factors through E. So each direction needs only that τ_{≤a-1}E and (τ_{≤a-1}E)⟦1⟧ receive no nonzero morphism from P⟦-i⟧ for i large; both of them lie in D_QCoh(𝒪_X) and are bounded above, by a - 1 and a - 2, and Stacks.DerivedQCoh.exists_threshold_subsingleton_hom_negShift_of_isPerfect kills both from i ≥ a - 1 + c on, with c the threshold that perfectness of P supplies through [Stacks, Tag 09M4].

theorem eventually_subsingleton_hom_iff_truncGE_of_isPerfect
    (P E : DerivedCategory X.Modules)
    (hP : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace) P)
    (hE : ∀ j : ℤ, ((DerivedCategory.homologyFunctor X.Modules j).obj E).IsQuasicoherent)
    (a : ℤ) :
    (∃ N : ℤ, ∀ i : ℤ, N ≤ i → Subsingleton (P⟦-i⟧ ⟶ E)) ↔
      ∃ N : ℤ, ∀ i : ℤ, N ≤ i →
        Subsingleton (P⟦-i⟧ ⟶ (DerivedCategory.TStructure.t.truncGE a).obj E)
Tag 0GEM, a lemma

Tag 0GEM in the Stacks Project.

Stacks.Perfect.eventually_subsingleton_hom_iff_truncLE_of_isLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DetectingBoundedness.lean, line 264.

[Stacks, Tag 0GEM]. Let X be a scheme, let P and E be objects of D(𝒪_X) with P bounded above by nP, and let a be an integer. Then Hom(P⟦-i⟧, E) = 0 for i ≪ 0 if and only if Hom(P⟦-i⟧, τ_{≤a}E) = 0 for i ≪ 0.

The source states this for P perfect on a quasi-compact quasi-separated scheme and E in D_QCoh(𝒪_X); the argument consumes only boundedness above of P, which those hypotheses imply, so the statement here is strictly more general and a consumer holding the source's hypotheses may restrict. The vanishing that makes the truncation triangle harmless is pure t-structure orthogonality: P⟦-i⟧ is ≤ nP + i, while τ_{>a}E is ≥ a + 1, and nP + i < a + 1 for i ≪ 0.

theorem eventually_subsingleton_hom_iff_truncLE_of_isLE
    (P E : DerivedCategory X.Modules) (nP : ℤ) (hP : P.IsLE nP) (a : ℤ) :
    (∃ N : ℤ, ∀ i : ℤ, i ≤ N → Subsingleton (P⟦-i⟧ ⟶ E)) ↔
      ∃ N : ℤ, ∀ i : ℤ, i ≤ N →
        Subsingleton (P⟦-i⟧ ⟶ (DerivedCategory.TStructure.t.truncLE a).obj E)
Tag 0GEN, a proposition

Tag 0GEN in the Stacks Project.

Stacks.SheafOfModules.tfae_minus_of_isPerfect_generator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/DetectingBoundednessGenerator.lean, line 331.

Let X be a quasi-compact and quasi-separated scheme, let G be a perfect object of D(𝒪_X) which generates D_QCoh(𝒪_X), and let E ∈ D_QCoh(𝒪_X). The following are equivalent:

  1. E ∈ D^-_QCoh(𝒪_X);
  2. Hom_{D(𝒪_X)}(G[-i], E) = 0 for i ≫ 0;
  3. Ext^i_X(G, E) = 0 for i ≫ 0;
  4. RHom_X(G, E) is in D^-(ℤ);
  5. H^i(X, G^∨ ⊗^L E) = 0 for i ≫ 0;
  6. RΓ(X, G^∨ ⊗^L E) is in D^-(ℤ);
  7. for every perfect object P of D(𝒪_X): (a) the assertions (2), (3), (4) hold with G replaced by P, (b) H^i(X, P ⊗^L E) = 0 for i ≫ 0, and (c) RΓ(X, P ⊗^L E) is in D^-(ℤ).

Generation of D_QCoh(𝒪_X) by G is the hypothesis that an object of D(𝒪_X) with quasi-coherent cohomology receiving only zero morphisms from the shifts of G is zero, and E ∈ D_QCoh(𝒪_X) is quasi-coherence of the cohomology sheaves of E. RHom_X(G, E) is the global derived hom, read in D(ℤ); D^-(ℤ) is the property minus of the canonical t-structure on D(AddCommGrpCat).

theorem tfae_minus_of_isPerfect_generator
    (hqc : CompactSpace X) (hqs : QuasiSeparatedSpace X)
    (G E : DerivedCategory (StructureSheafModules X.sheaf))
    (hG : (ringedSite X.sheaf).IsPerfect G)
    (hgen : ∀ K : DerivedCategory (StructureSheafModules X.sheaf),
      (∀ i : ℤ, ((DerivedCategory.homologyFunctor
          (StructureSheafModules X.sheaf) i).obj K).IsQuasicoherent) →
        (∀ (n : ℤ) (f : G⟦n⟧ ⟶ K), f = 0) → IsZero K)
    (hE : ∀ i : ℤ, ((DerivedCategory.homologyFunctor
      (StructureSheafModules X.sheaf) i).obj E).IsQuasicoherent) :
    List.TFAE
      [(DerivedCategory.TStructure.t (C := StructureSheafModules X.sheaf)).minus E,
        ∃ N : ℤ, ∀ i, N ≤ i → Subsingleton (G⟦-i⟧ ⟶ E),
        ∃ N : ℤ, ∀ i, N ≤ i → Subsingleton (DerivedCategory.Ext G E i),
        (DerivedCategory.TStructure.t (C := AddCommGrpCat.{u})).minus
          ((RingedSite.underlyingDerivedGroup (ringedSite X.sheaf)).obj
            (((globalDerivedHom X.sheaf).obj (op G)).obj E)),
        ∃ N : ℤ, ∀ i, N ≤ i → IsZero ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} i).obj
          ((derivedModuleGlobalSections (ringedSite X.sheaf)).obj
            (((derivedTensor X.sheaf).obj (derivedDual X.sheaf G)).obj E))),
        (DerivedCategory.TStructure.t (C := AddCommGrpCat.{u})).minus
          ((derivedModuleGlobalSections (ringedSite X.sheaf)).obj
            (((derivedTensor X.sheaf).obj (derivedDual X.sheaf G)).obj E)),
        ∀ P : DerivedCategory (StructureSheafModules X.sheaf), (ringedSite X.sheaf).IsPerfect P →
          ((∃ N : ℤ, ∀ i, N ≤ i → Subsingleton (P⟦-i⟧ ⟶ E)) ∧
            (∃ N : ℤ, ∀ i, N ≤ i → Subsingleton (DerivedCategory.Ext P E i)) ∧
            (DerivedCategory.TStructure.t (C := AddCommGrpCat.{u})).minus
              ((RingedSite.underlyingDerivedGroup (ringedSite X.sheaf)).obj
                (((globalDerivedHom X.sheaf).obj (op P)).obj E))) ∧
          (∃ N : ℤ, ∀ i, N ≤ i → IsZero ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} i).obj
            ((derivedModuleGlobalSections (ringedSite X.sheaf)).obj
              (((derivedTensor X.sheaf).obj P).obj E)))) ∧
          (DerivedCategory.TStructure.t (C := AddCommGrpCat.{u})).minus
            ((derivedModuleGlobalSections (ringedSite X.sheaf)).obj
              (((derivedTensor X.sheaf).obj P).obj E))]
Tag 0GEP, an equation

Tag 0GEP in the Stacks Project.

Stacks.Cohomology.ExtensionByZeroClosedSupport.isPerfect_jShriek_of_closedSupport_and_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PerfectComplexes/ExtensionByZeroClosedSupport.lean, line 121.

Stacks 0GEP. Let j : U → X be an open subspace of a ringed space and let T ⊆ U be closed in X. For a perfect object E of the derived category of 𝒪_U-modules whose cohomology sheaves are supported on T, the object K' = j_! E satisfies

  • j_! E = Rj_* E: the canonical map j_! E ⟶ Rj_* E is an isomorphism ([Stacks, Tag 08DF]);
  • K' is a perfect object of D(𝒪_X) ([Stacks, Tag 08DP]);
  • K' is supported on the closed set T;
  • K' restricts to E on U.

These are the assertions made of the complex K' = R(V → X)_* K = R(V → X)_! K in the proof of [Stacks, Tag 0GEN], where K is the Koszul complex on functions cutting out T = X \ U' inside the affine open V.

theorem isPerfect_jShriek_of_closedSupport_and_restrict
    (X : RingedSpace.{u, u}) (U : Opens X) (T : Set X) (hT : IsClosed T) (hTU : T ⊆ (U : Set X))
    (Rj : DerivedCategory (SheafOfModules.{u} (resRing U (structureSheafRing X))) ⥤
      DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (αj : (jPush U (structureSheafRing X)).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rj)
    (hRj : Rj.IsRightDerivedFunctor αj
      (HomotopyCategory.quasiIso (SheafOfModules.{u} (resRing U (structureSheafRing X)))
        (ComplexShape.up ℤ)))
    (E : DerivedCategory (SheafOfModules.{u} (resRing U (structureSheafRing X))))
    (hE : RingedSpace.IsPerfect (X := X.restrict U.isOpenEmbedding) E)
    (hET : AlgebraicGeometry.CohomologySupportedOn (resRing U (structureSheafRing X))
      ((fun x : Usp U ↦ x.1) ⁻¹' T) E) :
    IsIso ((extensionByZeroToDerivedPushforward (structureSheafRing X) U Rj αj).app E) ∧
      RingedSpace.IsPerfect (X := X)
        ((jShriek U (structureSheafRing X)).mapDerivedCategory.obj E) ∧
      AlgebraicGeometry.CohomologySupportedOn (structureSheafRing X) T
        ((jShriek U (structureSheafRing X)).mapDerivedCategory.obj E) ∧
      Nonempty ((jStar U (structureSheafRing X)).mapDerivedCategory.obj
        ((jShriek U (structureSheafRing X)).mapDerivedCategory.obj E) ≅ E)
Tag 0GEQ, a proposition

Tag 0GEQ in the Stacks Project.

Stacks.SheafOfModules.eventually_subsingleton_shiftedHom_iff_ext, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/DetectingBoundedBelowGenerator.lean, line 94. The attribute's comment: “conditions (2) and (3): eventual vanishing of Hom(G[-i], E) and of Ext^i(G, E)”.

Stacks 0GEQ, conditions (2) and (3). For a perfect generator G of D_QCoh(𝒪_X) on a quasi-compact, quasi-separated scheme and an object E of D_QCoh(𝒪_X), the groups Hom_{D(𝒪_X)}(G⟦-i⟧, E) vanish for i ≪ 0 exactly when the groups Ext^i_X(G, E) do.

The two conditions hold of the same i, because ⟦-i⟧ is left adjoint to ⟦i⟧.

theorem eventually_subsingleton_shiftedHom_iff_ext
    (_hqc : CompactSpace X) (_hqs : QuasiSeparatedSpace X)
    (G E : DerivedCategory (StructureSheafModules X.sheaf))
    (_hG : (ringedSite X.sheaf).IsPerfect G)
    (_hgen : ∀ K : DerivedCategory (StructureSheafModules X.sheaf),
      (∀ i : ℤ, ((DerivedCategory.homologyFunctor
          (StructureSheafModules X.sheaf) i).obj K).IsQuasicoherent) →
        (∀ (n : ℤ) (f : G⟦n⟧ ⟶ K), f = 0) → IsZero K)
    (_hE : ∀ i : ℤ, ((DerivedCategory.homologyFunctor
      (StructureSheafModules X.sheaf) i).obj E).IsQuasicoherent) :
    (∃ N : ℤ, ∀ i ≤ N, Subsingleton (G⟦-i⟧ ⟶ E)) ↔
      ∃ N : ℤ, ∀ i ≤ N, Subsingleton (DerivedCategory.Ext G E i)

Stacks.SheafOfModules.plus_derivedGlobalSections_derivedTensor_derivedDual_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/DetectingBoundedBelowGenerator.lean, line 127. The attribute's comment: “conditions (5) and (6): eventual vanishing of H^i(X, G^vee ⊗ E) and membership of RGamma(X, G^vee ⊗ E) in D^+(Z)”.

Stacks 0GEQ, conditions (5) and (6). For a perfect generator G of D_QCoh(𝒪_X) on a quasi-compact, quasi-separated scheme and an object E of D_QCoh(𝒪_X), the cohomology groups H^i(X, G^∨ ⊗^L_{𝒪_X} E) vanish for i ≪ 0 exactly when RΓ(X, G^∨ ⊗^L_{𝒪_X} E) lies in D⁺(ℤ).

This is the description of the bounded-below derived category by its cohomology, applied to the single object RΓ(X, G^∨ ⊗^L_{𝒪_X} E) of D(AddCommGrpCat).

theorem plus_derivedGlobalSections_derivedTensor_derivedDual_iff
    (_hqc : CompactSpace X) (_hqs : QuasiSeparatedSpace X)
    (G E : DerivedCategory (StructureSheafModules X.sheaf))
    (_hG : (ringedSite X.sheaf).IsPerfect G)
    (_hgen : ∀ K : DerivedCategory (StructureSheafModules X.sheaf),
      (∀ i : ℤ, ((DerivedCategory.homologyFunctor
          (StructureSheafModules X.sheaf) i).obj K).IsQuasicoherent) →
        (∀ (n : ℤ) (f : G⟦n⟧ ⟶ K), f = 0) → IsZero K)
    (_hE : ∀ i : ℤ, ((DerivedCategory.homologyFunctor
      (StructureSheafModules X.sheaf) i).obj E).IsQuasicoherent) :
    (DerivedCategory.TStructure.t (C := AddCommGrpCat.{u})).plus
        ((derivedModuleGlobalSections (ringedSite X.sheaf)).obj
          (((derivedTensor X.sheaf).obj E).obj (derivedDual X.sheaf G))) ↔
      ∃ N : ℤ, ∀ n ≤ N, IsZero ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} n).obj
        ((derivedModuleGlobalSections (ringedSite X.sheaf)).obj
          (((derivedTensor X.sheaf).obj E).obj (derivedDual X.sheaf G))))

Stacks.SheafOfModules.eventually_subsingleton_ext_iff_isZero_homology_derivedTensorDual, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/DetectingBoundedBelowGenerator.lean, line 187. The attribute's comment: “conditions (3) and (5): eventual vanishing of Ext^i(G, E) and of H^i(X, G^vee ⊗ E), granted the 08I1 map E[i] ⊗ G^vee ⟶ RSheafHom(G, E[i]) invertible for all i”.

Stacks 0GEQ, conditions (3) and (5). For a perfect generator G of D_QCoh(𝒪_X) on a quasi-compact, quasi-separated scheme and an object E of D_QCoh(𝒪_X), the groups Ext^i_X(G, E) vanish for i ≪ 0 exactly when the cohomology groups H^i(X, G^∨ ⊗^L_{𝒪_X} E) do, granted that the canonical map E⟦i⟧ ⊗^L_{𝒪_X} G^∨ ⟶ RSheafHom(G, E⟦i⟧) of Stacks 08I1 is invertible for every i.

The two conditions hold of the same i, because Ext^i_X(G, E) and H^i(X, G^∨ ⊗^L_{𝒪_X} E) are the same group: Stacks 08DQ identifies H⁰(X, M ⊗^L_{𝒪_X} G^∨) with Hom(G, M), and at M = E⟦i⟧ the left side becomes H^i(X, G^∨ ⊗^L_{𝒪_X} E) because tensoring with G^∨ and RΓ(X, -) are triangulated, hence commute with the shift, and H⁰ of an i-fold shift is H^i.

theorem eventually_subsingleton_ext_iff_isZero_homology_derivedTensorDual
    (_hqc : CompactSpace X) (_hqs : QuasiSeparatedSpace X)
    (G E : DerivedCategory (StructureSheafModules X.sheaf))
    (_hG : (ringedSite X.sheaf).IsPerfect G)
    (_hgen : ∀ K : DerivedCategory (StructureSheafModules X.sheaf),
      (∀ i : ℤ, ((DerivedCategory.homologyFunctor
          (StructureSheafModules X.sheaf) i).obj K).IsQuasicoherent) →
        (∀ (n : ℤ) (f : G⟦n⟧ ⟶ K), f = 0) → IsZero K)
    (_hE : ∀ i : ℤ, ((DerivedCategory.homologyFunctor
      (StructureSheafModules X.sheaf) i).obj E).IsQuasicoherent)
    (h08I1 : ∀ i : ℤ, IsIso (derivedTensorDualToSheafHom X.sheaf G (E⟦i⟧))) :
    (∃ N : ℤ, ∀ i ≤ N, Subsingleton (DerivedCategory.Ext G E i)) ↔
      ∃ N : ℤ, ∀ n ≤ N, IsZero ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} n).obj
        ((derivedModuleGlobalSections (ringedSite X.sheaf)).obj
          (((derivedTensor X.sheaf).obj E).obj (derivedDual X.sheaf G))))

Stacks.SheafOfModules.tfae_plus_of_isPerfect_generator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/DetectingBoundednessGenerator.lean, line 405.

Let X be a quasi-compact and quasi-separated scheme, let G be a perfect object of D(𝒪_X) which generates D_QCoh(𝒪_X), and let E ∈ D_QCoh(𝒪_X). The following are equivalent:

  1. E ∈ D^+_QCoh(𝒪_X);
  2. Hom_{D(𝒪_X)}(G[-i], E) = 0 for i ≪ 0;
  3. Ext^i_X(G, E) = 0 for i ≪ 0;
  4. RHom_X(G, E) is in D^+(ℤ);
  5. H^i(X, G^∨ ⊗^L E) = 0 for i ≪ 0;
  6. RΓ(X, G^∨ ⊗^L E) is in D^+(ℤ);
  7. for every perfect object P of D(𝒪_X): (a) the assertions (2), (3), (4) hold with G replaced by P, (b) H^i(X, P ⊗^L E) = 0 for i ≪ 0, and (c) RΓ(X, P ⊗^L E) is in D^+(ℤ).

Generation of D_QCoh(𝒪_X) by G is the hypothesis that an object of D(𝒪_X) with quasi-coherent cohomology receiving only zero morphisms from the shifts of G is zero, and E ∈ D_QCoh(𝒪_X) is quasi-coherence of the cohomology sheaves of E. RHom_X(G, E) is the global derived hom, read in D(ℤ); D^+(ℤ) is the property plus of the canonical t-structure on D(AddCommGrpCat).

theorem tfae_plus_of_isPerfect_generator
    (hqc : CompactSpace X) (hqs : QuasiSeparatedSpace X)
    (G E : DerivedCategory (StructureSheafModules X.sheaf))
    (hG : (ringedSite X.sheaf).IsPerfect G)
    (hgen : ∀ K : DerivedCategory (StructureSheafModules X.sheaf),
      (∀ i : ℤ, ((DerivedCategory.homologyFunctor
          (StructureSheafModules X.sheaf) i).obj K).IsQuasicoherent) →
        (∀ (n : ℤ) (f : G⟦n⟧ ⟶ K), f = 0) → IsZero K)
    (hE : ∀ i : ℤ, ((DerivedCategory.homologyFunctor
      (StructureSheafModules X.sheaf) i).obj E).IsQuasicoherent) :
    List.TFAE
      [(DerivedCategory.TStructure.t (C := StructureSheafModules X.sheaf)).plus E,
        ∃ N : ℤ, ∀ i ≤ N, Subsingleton (G⟦-i⟧ ⟶ E),
        ∃ N : ℤ, ∀ i ≤ N, Subsingleton (DerivedCategory.Ext G E i),
        (DerivedCategory.TStructure.t (C := AddCommGrpCat.{u})).plus
          ((RingedSite.underlyingDerivedGroup (ringedSite X.sheaf)).obj
            (((globalDerivedHom X.sheaf).obj (op G)).obj E)),
        ∃ N : ℤ, ∀ i ≤ N, IsZero ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} i).obj
          ((derivedModuleGlobalSections (ringedSite X.sheaf)).obj
            (((derivedTensor X.sheaf).obj (derivedDual X.sheaf G)).obj E))),
        (DerivedCategory.TStructure.t (C := AddCommGrpCat.{u})).plus
          ((derivedModuleGlobalSections (ringedSite X.sheaf)).obj
            (((derivedTensor X.sheaf).obj (derivedDual X.sheaf G)).obj E)),
        ∀ P : DerivedCategory (StructureSheafModules X.sheaf), (ringedSite X.sheaf).IsPerfect P →
          ((∃ N : ℤ, ∀ i ≤ N, Subsingleton (P⟦-i⟧ ⟶ E)) ∧
            (∃ N : ℤ, ∀ i ≤ N, Subsingleton (DerivedCategory.Ext P E i)) ∧
            (DerivedCategory.TStructure.t (C := AddCommGrpCat.{u})).plus
              ((RingedSite.underlyingDerivedGroup (ringedSite X.sheaf)).obj
                (((globalDerivedHom X.sheaf).obj (op P)).obj E))) ∧
          (∃ N : ℤ, ∀ i ≤ N, IsZero ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} i).obj
            ((derivedModuleGlobalSections (ringedSite X.sheaf)).obj
              (((derivedTensor X.sheaf).obj P).obj E)))) ∧
          (DerivedCategory.TStructure.t (C := AddCommGrpCat.{u})).plus
            ((derivedModuleGlobalSections (ringedSite X.sheaf)).obj
              (((derivedTensor X.sheaf).obj P).obj E))]
Sources
LeanStacks.Koszul.Truncation.truncGE_restriction_of_hom_koszul_eq_zero · Stacks.Koszul.Truncation.hom_koszul_eq_zero_of_truncGE_restriction · Stacks.Koszul.Truncation.truncLE_restriction_of_hom_koszul_eq_zero · Stacks.Koszul.Truncation.hom_koszul_eq_zero_of_truncLE_restriction_sub_one · Stacks.DerivedQCoh.eventually_subsingleton_hom_iff_truncGE_of_isPerfect · Stacks.Perfect.eventually_subsingleton_hom_iff_truncLE_of_isLE · Stacks.SheafOfModules.tfae_minus_of_isPerfect_generator · Stacks.Cohomology.ExtensionByZeroClosedSupport.isPerfect_jShriek_of_closedSupport_and_restrict

Section36.41 Quasi-coherent objects in the derived category#

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

Tag 0GZZ, a lemma

Tag 0GZZ in the Stacks Project.

AlgebraicGeometry.smallAffineChaoticDerivedQuasiCoherentEquivQC, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/AffineSiteQuasiCoherentObjects.lean, line 238. The attribute's comment: “the equivalence (4) ≃ (5)”.

Stacks 0GZZ, the equivalence of (4) and (5). For a scheme S, the derived category of modules on the small affine site S_affine with quasi-coherent cohomology sheaves is canonically equivalent to the category QC(S_affine, 𝒪) of quasi-coherent objects of the derived category.

The equivalence is realized inside D(S_affine, 𝒪), by smallAffineChaoticDerivedQuasiCoherentEquivQC_functor_comp_ι; the two subcategories are in fact equal, by smallAffineChaotic_isQC_eq_hasQuasicoherentCohomology.

For a scheme in Scheme.{0} both sides are triangulated subcategories of D(S_affine, 𝒪), by smallAffineChaotic_qcohCohomologyProperty_isTriangulated, so the comparison is then an exact equivalence of triangulated categories. None of the other four comparisons of Stacks 0GZZ is proved; see the coverage note of this file.

def smallAffineChaoticDerivedQuasiCoherentEquivQC
    (bc : BaseChangeData.{w}
      (Stacks.SheafOfModules.Tensor.ringSheaf (smallAffineChaoticRingedSite B S hS).O).obj) :
    (qcohCohomologyProperty.{w} (smallAffineChaoticRingedSite B S hS)).FullSubcategory ≌
      QC.{w} bc

AlgebraicGeometry.smallAffineChaoticDerivedQuasiCoherentEquivQC_functor_comp_ι, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/AffineSiteQuasiCoherentObjects.lean, line 262. The attribute's comment: “the equivalence (4) ≃ (5) is the canonical one”.

Stacks 0GZZ, the equivalence of (4) and (5), as a commuting triangle. The comparison D_QCoh(S_affine, 𝒪) ≌ QC(S_affine, 𝒪) is the canonical one: it commutes with the inclusions of both sides into D(S_affine, 𝒪).

def smallAffineChaoticDerivedQuasiCoherentEquivQC_functor_comp_ι
    (bc : BaseChangeData.{w}
      (Stacks.SheafOfModules.Tensor.ringSheaf (smallAffineChaoticRingedSite B S hS).O).obj) :
    (smallAffineChaoticDerivedQuasiCoherentEquivQC.{w} B S hS bc).functor ⋙ QCι.{w} bc ≅
      (qcohCohomologyProperty.{w} (smallAffineChaoticRingedSite B S hS)).ι

AlgebraicGeometry.smallAffineChaotic_qcohCohomologyProperty_isTriangulated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/AffineSiteQuasiCoherentObjects.lean, line 319. The attribute's comment: “(4) and (5) are triangulated, for a scheme in Scheme.{0}”.

Stacks 0GZZ, triangulatedness of (4) and (5). For a scheme in Scheme.{0}, D_QCoh(S_affine, 𝒪) is a triangulated subcategory of D(S_affine, 𝒪): it is the same subcategory as QC(S_affine, 𝒪), which is triangulated by Stacks 0GYW.

Together with smallAffineChaoticDerivedQuasiCoherentEquivQC and smallAffineChaoticDerivedQuasiCoherentEquivQC_functor_comp_ι this makes the comparison of (4) and (5) an exact equivalence of triangulated categories, both sides being triangulated subcategories of D(S_affine, 𝒪) and the comparison commuting with the two inclusions.

The restriction to Scheme.{0} comes from the input: the library constructs derived base change only over a structure sheaf with values in RingCat.{0}; see smallAffineChaoticBaseChangeData.

theorem smallAffineChaotic_qcohCohomologyProperty_isTriangulated :
    ObjectProperty.IsTriangulated
      (qcohCohomologyProperty.{0} (smallAffineChaoticRingedSite B₀ S₀ hS₀))

AlgebraicGeometry.smallAffineChaotic_qcohCohomologyProperty_isTriangulated_univ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/AffineSiteQuasiCoherentObjectsSupplement.lean, line 82. The attribute's comment: “(4) and (5) are triangulated”.

Stacks 0GZZ, triangulatedness of (4) and (5). For an arbitrary scheme S, D_QCoh(S_affine, 𝒪) is a triangulated subcategory of D(S_affine, 𝒪): it is the same subcategory as QC(S_affine, 𝒪), which is triangulated by Stacks 0GYW.

Together with smallAffineChaoticDerivedQuasiCoherentEquivQC and smallAffineChaoticDerivedQuasiCoherentEquivQC_functor_comp_ι this makes the comparison of (4) and (5) an exact equivalence of triangulated categories, both sides being triangulated subcategories of D(S_affine, 𝒪) and the comparison commuting with the two inclusions.

theorem smallAffineChaotic_qcohCohomologyProperty_isTriangulated_univ :
    ObjectProperty.IsTriangulated
      (qcohCohomologyProperty.{w} (smallAffineChaoticRingedSite B S hS))

AlgebraicGeometry.Scheme.nonempty_quasicoherentDerived_linearTriangulatedEquivalences, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/QuasiCoherentObjectsExactEquivalences.lean, line 597.

Stacks 0GZZ. Let X be a scheme, and let Sch_Zar be a big Zariski site containing it. There are canonical exact equivalences between the following triangulated categories:

  1. D_QCoh(𝒪_X), the complexes of 𝒪_X-modules on the ringed space (X, 𝒪_X) with quasi-coherent cohomology sheaves;
  2. D_QCoh(X_Zar, 𝒪), the same on the small Zariski site X_Zar of Topologies, Definition 020T (the open immersions U → X of Sch_Zar), with its structure sheaf U ↦ Γ(U, 𝒪_U) and quasi-coherence in the sense of Modules on Sites, Definition 03DL;
  3. D_QCoh(X_{affine, Zar}, 𝒪), the same on the category of affine opens of X with the Zariski topology;
  4. D_QCoh(X_affine, 𝒪), the same on the category of affine opens of X with the chaotic topology, where modules are presheaves of modules;
  5. QC(X_affine, 𝒪), the full subcategory of D(X_affine, 𝒪) of Cohomology on Sites, Definition 0GYV: the objects K for which RΓ(V, K) ⊗^L_{𝒪(V)} 𝒪(U) ⟶ RΓ(U, K) is an isomorphism for all U ⟶ V, formed with the derived base change of AlgebraicGeometry.affineChaoticBaseChangeData.

Formally: the five subcategories are triangulated subcategories of their ambient derived categories, and there are equivalences of triangulated categories (an equivalence whose functor commutes with the shifts and preserves distinguished triangles) (2) ≌ (1), (1) ≌ (3), (4) ≌ (3) and (4) ≌ (5), which are the canonical ones: each lies, through the inclusions of the subcategories, over the canonical functor of the source, namely derived restriction along the identification of modules of Descent, Remark 03FG; derived restriction to the affine opens; the identification of presheaves with sheaves for the chaotic topology followed by Lε^* for the morphism of ringed sites ε : (X_{affine, Zar}, 𝒪) ⟶ (X_affine, 𝒪) of Cohomology on Sites, Lemma 07A8; and the identity of D(X_affine, 𝒪).

The derived categories of sheaves of modules are taken at the standard model HasDerivedCategory.standard, the one the change of topology of Stacks 07A8 is constructed at; those of presheaves of modules at the model of Stacks.ModulesOnACategory.QuasiCoherentEquivalence.DMod.

theorem Scheme.nonempty_quasicoherentDerived_linearTriangulatedEquivalences :
    letI := SmallZariski.abelianModules B X hX
    letI := SmallZariski.derivedCategoryModel B X hX
    haveI := Scheme.isWeakSerreClass_isQuasicoherent_ringCatSheaf X
    haveI := SmallZariski.isWeakSerreClass_isQuasicoherentOnSite B X hX
    haveI := SmallZariski.additive_restrictModuleEquivalence B X hX
    -- the five subcategories are triangulated
    (DerivedCategoryB.derivedCategoryB
        (SheafOfModules.isQuasicoherent X.ringCatSheaf)).IsTriangulated ∧
    (DerivedCategoryB.derivedCategoryB (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
        (SmallZariski.structureSheaf B X hX))).IsTriangulated ∧
    (DerivedCategoryB.derivedCategoryB (SheafOfModules.isQuasicoherentOnSite.{u, u, u, u}
        (Stacks.SheafOfModules.Tensor.ringSheaf X.affineZariskiRingedSite.O))).IsTriangulated ∧
    (qcohCohomologyProperty.{u} X.affineChaoticRingedSite).IsTriangulated ∧
    (isQCProperty.{u} (affineChaoticBaseChangeData.{u} X)).IsTriangulated ∧
    -- `(2) ≃ (1)`, over derived restriction along Descent, Remark 03FG
    (∃ e : LinearTriangulatedEquivalence ℤ
        (DerivedCategoryB.derivedCategoryB (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
          (SmallZariski.structureSheaf B X hX))).FullSubcategory
        (DerivedCategoryB.derivedCategoryB
          (SheafOfModules.isQuasicoherent X.ringCatSheaf)).FullSubcategory,
      Nonempty (e.equivalence.functor ⋙
          (DerivedCategoryB.derivedCategoryB (SheafOfModules.isQuasicoherent X.ringCatSheaf)).ι ≅
        (DerivedCategoryB.derivedCategoryB (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
          (SmallZariski.structureSheaf B X hX))).ι ⋙
          (SmallZariski.restrictModuleEquivalence B X hX).functor.mapDerivedCategory)) ∧
    -- `(1) ≃ (3)`, over derived restriction to the affine opens
    (∃ e : LinearTriangulatedEquivalence ℤ
        (DerivedCategoryB.derivedCategoryB
          (SheafOfModules.isQuasicoherent X.ringCatSheaf)).FullSubcategory
        X.affineOpensQuasicoherentDerivedCategory,
      Nonempty (e.equivalence.functor ⋙
          (DerivedCategoryB.derivedCategoryB (SheafOfModules.isQuasicoherentOnSite.{u, u, u, u}
            (Stacks.SheafOfModules.Tensor.ringSheaf X.affineZariskiRingedSite.O))).ι ≅
        (DerivedCategoryB.derivedCategoryB (SheafOfModules.isQuasicoherent X.ringCatSheaf)).ι ⋙
          X.affineOpensModuleRestrictionEquivalence.functor.mapDerivedCategory)) ∧
    -- `(4) ≃ (3)`, over sheafification for the chaotic topology followed by `Lε^*`
    (∃ e : LinearTriangulatedEquivalence ℤ
        (qcohCohomologyProperty.{u} X.affineChaoticRingedSite).FullSubcategory
        X.affineOpensQuasicoherentDerivedCategory,
      Nonempty (e.equivalence.functor ⋙
          (DerivedCategoryB.derivedCategoryB (SheafOfModules.isQuasicoherentOnSite.{u, u, u, u}
            (Stacks.SheafOfModules.Tensor.ringSheaf X.affineZariskiRingedSite.O))).ι ≅
        (qcohCohomologyProperty.{u} X.affineChaoticRingedSite).ι ⋙
          X.affineChaoticSheafPresheafEquivalence.inverse.mapDerivedCategory ⋙
            X.affineCoarseningDerivedPullback)) ∧
    -- `(4) ≃ (5)`, over the identity of `D(X_affine, 𝒪)`
    (∃ e : LinearTriangulatedEquivalence ℤ
        (qcohCohomologyProperty.{u} X.affineChaoticRingedSite).FullSubcategory
        (QC.{u} (affineChaoticBaseChangeData.{u} X)),
      Nonempty (e.equivalence.functor ⋙ QCι.{u} (affineChaoticBaseChangeData.{u} X) ≅
        (qcohCohomologyProperty.{u} X.affineChaoticRingedSite).ι))
Tag 0H00, a remark

Tag 0H00 in the Stacks Project.

AlgebraicGeometry.Stack.affineBigSiteQuasiCoherentDerivedEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/SchemeQC/AffineBigSiteEquivalence.lean, line 92.

Stacks 0H00. Let S be a scheme in a big fppf site B. Then QC((Aff/S), O) — the triangulated category of quasi-coherent objects (Stacks 0GYV) of the derived category of O-modules on the category (Aff/S) of affine schemes over S with the chaotic topology and its sheaf of rings of global functions, that is QC((Sch/S)_{fppf}) of Stacks 0H0H for the identity of (Sch/S)_{fppf} — is canonically equivalent to D_QCoh(O_S), the full subcategory of the derived category of O_S-modules (in any model) of the objects with quasi-coherent cohomology sheaves; the modules have their sections in max (u + 1) t.

The equivalence is the composite of the three equivalences of the proof of Stacks 0H0K, for the Zariski topology: ε^* from QC((Aff/S), O) onto the objects K of D((Aff/S)_{Zar}↑) with Rε_*K cartesian (Stacks 0H0J, 0GZS); the direct image along the morphism of ringed sites given by the affine opens of S, inverse to the derived pullback on the 0GZS subcategories (the argument of Stacks 09J1); and the identification of the 0GZS subcategory of the lifted small affine Zariski site of S with D_QCoh(O_S) (Descent 03FG, Stacks 0F1B, 0H04).

def affineBigSiteQuasiCoherentDerivedEquivalence
    [HasDerivedCategory (SheafOfModules.{max (u + 1) t} S.ringCatSheaf)] :
    quasiCoherentDerived.{u, u + 1, u, t} B S hS (𝟭 (BigFppfOver B S hS)) ≌
      (DerivedCategoryB.derivedCategoryB (SheafOfModules.isQuasicoherentOnSite S.ringCatSheaf :
        ObjectProperty (SheafOfModules.{max (u + 1) t} S.ringCatSheaf))).FullSubcategory
Sources
LeanAlgebraicGeometry.smallAffineChaoticDerivedQuasiCoherentEquivQC · AlgebraicGeometry.smallAffineChaoticDerivedQuasiCoherentEquivQC_functor_comp_ι · AlgebraicGeometry.smallAffineChaotic_qcohCohomologyProperty_isTriangulated · AlgebraicGeometry.smallAffineChaotic_qcohCohomologyProperty_isTriangulated_univ · AlgebraicGeometry.Scheme.nonempty_quasicoherentDerived_linearTriangulatedEquivalences · AlgebraicGeometry.Stack.affineBigSiteQuasiCoherentDerivedEquivalence

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.