36.3 Derived category of… to 36.9 Koszul complexes

Section36.3 Derived category of quasi-coherent modules#

Section 36.3 of the Stacks Project, Tag 06YZ. 10 tags here are carried by 47 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06VT, an equation

Tag 06VT in the Stacks Project.

Stacks.AlgebraicGeometry.QuasicoherentDerived.derivedQuasicoherentComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/WeakSerre/DerivedComparison.lean, line 122. The attribute's comment: “comparison functor”.

Stacks 06VT. The canonical comparison functor D(QCoh(𝒪_X)) ⥤ D_QCoh(𝒪_X) from the derived category of quasi-coherent 𝒪_X-modules to the complexes of 𝒪_X-modules with quasi-coherent cohomology: the derived functor of the exact inclusion, factored through D_QCoh(𝒪_X).

def derivedQuasicoherentComparison :
    DerivedCategory (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory ⥤
      (DerivedCategoryB.derivedCategoryB
        (SheafOfModules.isQuasicoherent X.ringCatSheaf)).FullSubcategory

Stacks.AlgebraicGeometry.QuasicoherentDerived.derivedQuasicoherentComparisonCommShift, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/WeakSerre/DerivedComparison.lean, line 132. The attribute's comment: “shift compatibility”.

Stacks 06VT. The comparison functor is compatible with translation of complexes.

instance derivedQuasicoherentComparisonCommShift :
    (derivedQuasicoherentComparison.{w} X).CommShift ℤ

Stacks.AlgebraicGeometry.QuasicoherentDerived.derivedQuasicoherentComparisonIsTriangulated, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/WeakSerre/DerivedComparison.lean, line 141. The attribute's comment: “exactness”.

Stacks 06VT. The comparison functor preserves distinguished triangles, so it is an exact functor of triangulated categories.

instance derivedQuasicoherentComparisonIsTriangulated :
    (derivedQuasicoherentComparison.{w} X).IsTriangulated

Tag 08DT, a lemma

Tag 08DT in the Stacks Project.

AlgebraicGeometry.hasCoproducts_quasicoherentDerivedCategory, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/QuasiCoherentDerived/DirectSums.lean, line 121.

The derived category of 𝒪_X-modules with quasi-coherent cohomology has direct sums.

instance hasCoproducts_quasicoherentDerivedCategory (X : Scheme.{u}) :
    HasCoproducts.{u} (QuasicoherentDerivedCategory X)

Tag 0A0J, a lemma

Tag 0A0J in the Stacks Project.

AlgebraicGeometry.cohomology_isLimit_of_isDerivedLimit_of_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/Coherator/DerivedLimitQuasiCoherent.lean, line 166. The attribute's comment: “cohomology_limit”.

Stacks Project, Tag 0A0J. The degree-q cohomology sheaf of a derived inverse limit of a tower with quasi-coherent cohomology and surjective transition maps on cohomology is the ordinary inverse limit of the degree-q cohomology sheaves.

public theorem cohomology_isLimit_of_isDerivedLimit_of_epi
    (X : Scheme.{u})
    (K : ℕᵒᵖ ⥤ DerivedCategory.{u + 1} X.Modules)
    (L : DerivedCategory.{u + 1} X.Modules)
    [HasProduct fun n : ℕ ↦ K.obj ⟨n⟩]
    (p : L ⟶ ∏ᶜ fun n : ℕ ↦ K.obj ⟨n⟩)
    (hL : ∃ δ : (∏ᶜ fun n : ℕ ↦ K.obj ⟨n⟩) ⟶ L⟦(1 : ℤ)⟧,
      Triangle.mk p
        (Pi.lift fun n : ℕ ↦
          Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) n -
            Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) (n + 1) ≫
              K.map (homOfLE (Nat.le_succ n)).op) δ ∈
        distTriang (DerivedCategory X.Modules))
    (hqc : ∀ (n : ℕ) (q : ℤ),
      ((DerivedCategory.homologyFunctor X.Modules q).obj (K.obj ⟨n⟩)).IsQuasicoherent)
    (hsurj : ∀ (n : ℕ) (q : ℤ),
      Epi ((DerivedCategory.homologyFunctor X.Modules q).map
        (K.map (homOfLE (Nat.le_succ n)).op)))
    (q : ℤ) :
    ∃ τ : (Functor.const ℕᵒᵖ).obj
        ((DerivedCategory.homologyFunctor X.Modules q).obj L) ⟶
        K ⋙ DerivedCategory.homologyFunctor X.Modules q,
      (∀ n : ℕ, τ.app ⟨n⟩ =
        (DerivedCategory.homologyFunctor X.Modules q).map
          (p ≫ Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) n)) ∧
      Nonempty (IsLimit (Cone.mk _ τ))

AlgebraicGeometry.isDerivedLimit_single_limit_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/Coherator/DerivedLimitQuasiCoherent.lean, line 271. The attribute's comment: “derived_limit_sheaves”.

Stacks Project, Tag 0A0J. For a tower with quasi-coherent cohomology and surjective transition maps on cohomology, the ordinary inverse limit of each tower of cohomology sheaves, placed in degree zero, is its derived inverse limit.

public theorem isDerivedLimit_single_limit_homology
    (X : Scheme.{u})
    (K : ℕᵒᵖ ⥤ DerivedCategory.{u + 1} X.Modules)
    (hqc : ∀ (n : ℕ) (q : ℤ),
      ((DerivedCategory.homologyFunctor X.Modules q).obj (K.obj ⟨n⟩)).IsQuasicoherent)
    (hsurj : ∀ (n : ℕ) (q : ℤ),
      Epi ((DerivedCategory.homologyFunctor X.Modules q).map
        (K.map (homOfLE (Nat.le_succ n)).op)))
    (q : ℤ) :
    let F := K ⋙ DerivedCategory.homologyFunctor X.Modules q
    ∃ h : HasProduct (fun n : ℕ =>
        (F ⋙ DerivedCategory.singleFunctor X.Modules 0).obj ⟨n⟩),
      @IsDerivedLimit (DerivedCategory X.Modules) _ _ _ _ _ _
        (F ⋙ DerivedCategory.singleFunctor X.Modules 0) h
        ((DerivedCategory.singleFunctor X.Modules 0).obj (limit F))

AlgebraicGeometry.isZero_cohomology_limit_homology_of_isAffineOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/Coherator/DerivedLimitQuasiCoherent.lean, line 295. The attribute's comment: “affine_limit_acyclic”.

Stacks Project, Tag 0A0J. The inverse limit of a degreewise-surjective tower of quasi-coherent cohomology sheaves has no higher cohomology on an affine open.

public theorem isZero_cohomology_limit_homology_of_isAffineOpen
    (X : Scheme.{u})
    (K : ℕᵒᵖ ⥤ DerivedCategory.{u + 1} X.Modules)
    (hqc : ∀ (n : ℕ) (q : ℤ),
      ((DerivedCategory.homologyFunctor X.Modules q).obj (K.obj ⟨n⟩)).IsQuasicoherent)
    (hsurj : ∀ (n : ℕ) (q : ℤ),
      Epi ((DerivedCategory.homologyFunctor X.Modules q).map
        (K.map (homOfLE (Nat.le_succ n)).op)))
    (U : X.Opens) (hU : IsAffineOpen U) (q : ℤ) (p : ℕ) (hp : 0 < p) :
    let F : ℕᵒᵖ ⥤ X.Modules := K ⋙ DerivedCategory.homologyFunctor X.Modules q
    let h : HasLimit F := inferInstance
    IsZero (Hgroup X.ringCatSheaf U p (@limit _ _ _ _ F h))

Tag 08D3, a lemma

Tag 08D3 in the Stacks Project.

AlgebraicGeometry.isIso_to_isDerivedLimit_truncGETower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/SpaltensteinCriterion/QuasicoherentTruncationConvergence.lean, line 87.

Stacks 08D3. A complex of 𝒪_X-modules on a scheme whose cohomology sheaves are all quasi-coherent is canonically isomorphic to the derived inverse limit of the tower of its canonical lower truncations n ↦ τ_{≥ -n} E.

The derived limit is presented by a distinguished triangle whose second map is the canonical difference of the projections, and the map c is pinned down by the requirement that its composites with the projections are the canonical truncation maps; the conclusion is that this map is invertible.

theorem isIso_to_isDerivedLimit_truncGETower
    (E : DerivedCategory (SheafOfModules.{u} X.ringCatSheaf))
    (hE : ∀ i : ℤ, ((DerivedCategory.homologyFunctor
      (SheafOfModules.{u} X.ringCatSheaf) i).obj E).IsQuasicoherent)
    [HasProduct fun n : ℕ ↦
      (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} X.ringCatSheaf) E).obj ⟨n⟩]
    (L : DerivedCategory (SheafOfModules.{u} X.ringCatSheaf)) (c : E ⟶ L)
    (p : L ⟶ ∏ᶜ fun n : ℕ ↦
      (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} X.ringCatSheaf) E).obj ⟨n⟩)
    (δ : (∏ᶜ fun n : ℕ ↦
      (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} X.ringCatSheaf) E).obj ⟨n⟩) ⟶
      L⟦(1 : ℤ)⟧)
    (hL : Triangle.mk p (Pi.lift fun n : ℕ ↦
        Pi.π (fun n : ℕ ↦ (Stacks.DerivedLimit.truncGETower
          (SheafOfModules.{u} X.ringCatSheaf) E).obj ⟨n⟩) n -
          Pi.π (fun n : ℕ ↦ (Stacks.DerivedLimit.truncGETower
            (SheafOfModules.{u} X.ringCatSheaf) E).obj ⟨n⟩) (n + 1) ≫
            (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} X.ringCatSheaf) E).map
              (homOfLE (Nat.le_succ n)).op) δ ∈
      distTriang (DerivedCategory (SheafOfModules.{u} X.ringCatSheaf)))
    (hc : ∀ n : ℕ, c ≫ p ≫ Pi.π (fun n : ℕ ↦ (Stacks.DerivedLimit.truncGETower
        (SheafOfModules.{u} X.ringCatSheaf) E).obj ⟨n⟩) n =
      (DerivedCategory.TStructure.t.truncGEπ (-(n : ℤ))).app E) :
    IsIso c

AlgebraicGeometry.isIso_of_isDerivedLimit_truncGETower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TotalDirectImage/TruncationTower.lean, line 102.

Let X be a scheme and let E be an object of D(𝒪_X) whose cohomology sheaves are all quasi-coherent. Then the canonical map from E to a derived limit L of the tower n ↦ τ_{≥ -n} E of canonical truncations from below is an isomorphism.

The derived limit is presented by its structural morphism p to the product of the tower and the distinguished triangle hL characterising it; the map c out of E is the canonical one because its composites with the product projections are required to be the truncation maps.

theorem isIso_of_isDerivedLimit_truncGETower
    (E : DerivedCategory X.Modules)
    (hE : ∀ q : ℤ, ((DerivedCategory.homologyFunctor X.Modules q).obj E).IsQuasicoherent)
    [HasProduct fun n : ℕ ↦ (Stacks.DerivedLimit.truncGETower X.Modules E).obj ⟨n⟩]
    (L : DerivedCategory X.Modules) (c : E ⟶ L)
    (p : L ⟶ ∏ᶜ fun n : ℕ ↦ (Stacks.DerivedLimit.truncGETower X.Modules E).obj ⟨n⟩)
    (δ : (∏ᶜ fun n : ℕ ↦ (Stacks.DerivedLimit.truncGETower X.Modules E).obj ⟨n⟩) ⟶ L⟦(1 : ℤ)⟧)
    (hL : Triangle.mk p (Pi.lift fun n : ℕ ↦
      Pi.π (fun n : ℕ ↦ (Stacks.DerivedLimit.truncGETower X.Modules E).obj ⟨n⟩) n -
        Pi.π (fun n : ℕ ↦ (Stacks.DerivedLimit.truncGETower X.Modules E).obj ⟨n⟩) (n + 1) ≫
          (Stacks.DerivedLimit.truncGETower X.Modules E).map
            (homOfLE (Nat.le_succ n)).op) δ ∈ distTriang (DerivedCategory X.Modules))
    (hc : ∀ n : ℕ, c ≫ p ≫
      Pi.π (fun n : ℕ ↦ (Stacks.DerivedLimit.truncGETower X.Modules E).obj ⟨n⟩) n =
        (DerivedCategory.TStructure.t.truncGEπ (-(n : ℤ))).app E) :
    IsIso c

Tag 08D4, a lemma

Tag 08D4 in the Stacks Project.

Stacks.QuasicoherentAmplitude.isGE_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/QuasicoherentAmplitude.lean, line 481. The attribute's comment: “part (3), lower bound”.

[Stacks, Tag 08D4] part (3), lower bound. A total right derived functor preserves a lower cohomological bound on a complex with quasi-coherent cohomology.

No product hypothesis on F and no vanishing hypothesis are needed: the K-injective complexes compute any total right derived functor out of a Grothendieck abelian category, and a bounded below object is represented by a K-injective complex in the same range.

theorem isGE_obj {B : Type*} [Category* B] [Abelian B] [HasDerivedCategory B]
    (X : Scheme.{u})
    (F : X.Modules ⥤ B) [F.Additive]
    (RF : DerivedCategory X.Modules ⥤ DerivedCategory B)
    (alpha : F.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶
      DerivedCategory.Qh ⋙ RF)
    [RF.IsRightDerivedFunctor alpha
      (HomotopyCategory.quasiIso X.Modules (ComplexShape.up ℤ))]
    (E : DerivedCategory X.Modules)
    (hcoh : ∀ j : ℤ,
      ((DerivedCategory.homologyFunctor X.Modules j).obj E).IsQuasicoherent)
    (a : ℤ) (hE : E.IsGE a) : (RF.obj E).IsGE a

Stacks.QuasicoherentAmplitude.isLE_obj_of_isZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/QuasicoherentAmplitude.lean, line 504. The attribute's comment: “part (3), upper bound”.

[Stacks, Tag 08D4] part (3), upper bound. If the higher derived functors vanish from degree N onward on quasi-coherent modules, a total right derived functor shifts an upper cohomological bound by at most N - 1.

theorem isLE_obj_of_isZero {B : Type*} [Category* B] [Abelian B]
    [HasDerivedCategory B] [HasProductsOfShape ℕ B] [HasExactLimitsOfShape (Discrete ℕ) B]
    (X : Scheme.{u})
    (F : X.Modules ⥤ B) [F.Additive]
    [PreservesLimitsOfShape (Discrete ℕ) F]
    (RF : DerivedCategory X.Modules ⥤ DerivedCategory B)
    (alpha : F.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶
      DerivedCategory.Qh ⋙ RF)
    [RF.IsRightDerivedFunctor alpha
      (HomotopyCategory.quasiIso X.Modules (ComplexShape.up ℤ))]
    (N : ℕ)
    (hRF : ∀ (M : X.Modules), M.IsQuasicoherent → ∀ (p : ℤ), (N : ℤ) ≤ p →
      IsZero ((F.rightDerivedPlus p).obj M))
    (E : DerivedCategory X.Modules)
    (hcoh : ∀ j : ℤ,
      ((DerivedCategory.homologyFunctor X.Modules j).obj E).IsQuasicoherent)
    (b : ℤ) (hE : E.IsLE b) : (RF.obj E).IsLE (b + (N : ℤ) - 1)

Stacks.QuasicoherentAmplitude.isIso_homology_map_truncLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/QuasicoherentAmplitude.lean, line 530. The attribute's comment: “part (1)”.

[Stacks, Tag 08D4] part (1). A total right derived functor agrees in degrees at most a on a complex with quasi-coherent cohomology and its canonical truncation in degrees at most a.

The third vertex of the truncation triangle at a is ≥ a + 1, so by part (3) lower bound its image under RF has no cohomology in degrees i and i - 1 for i ≤ a, and the long exact sequence makes the comparison both mono and epi.

theorem isIso_homology_map_truncLE {B : Type*} [Category* B] [Abelian B]
    [HasDerivedCategory B]
    (X : Scheme.{u})
    (F : X.Modules ⥤ B) [F.Additive]
    (RF : DerivedCategory X.Modules ⥤ DerivedCategory B)
    (alpha : F.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶
      DerivedCategory.Qh ⋙ RF)
    [RF.IsRightDerivedFunctor alpha
      (HomotopyCategory.quasiIso X.Modules (ComplexShape.up ℤ))]
    (E : DerivedCategory X.Modules)
    (hE : ∀ j : ℤ,
      ((DerivedCategory.homologyFunctor X.Modules j).obj E).IsQuasicoherent)
    (a i : ℤ) (hi : i ≤ a) :
    IsIso ((DerivedCategory.homologyFunctor B i).map
      (RF.map ((DerivedCategory.TStructure.t.truncLEι a).app E)))

Stacks.QuasicoherentAmplitude.isIso_homology_map_truncGE_of_isZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/QuasicoherentAmplitude.lean, line 572. The attribute's comment: “part (2)”.

[Stacks, Tag 08D4] part (2). If the higher derived functors vanish from degree N onward on quasi-coherent modules, then in degrees at least b a total right derived functor agrees on a complex with quasi-coherent cohomology and its canonical truncation in degrees at least b - N + 1.

The first vertex of the truncation triangle at a = b - N + 1 is ≤ a - 1, so by part (3) upper bound its image under RF is ≤ a - 1 + N - 1 = b - 1, hence has no cohomology in degrees i and i + 1 for i ≥ b.

theorem isIso_homology_map_truncGE_of_isZero {B : Type*} [Category* B] [Abelian B]
    [HasDerivedCategory B] [HasProductsOfShape ℕ B] [HasExactLimitsOfShape (Discrete ℕ) B]
    (X : Scheme.{u})
    (F : X.Modules ⥤ B) [F.Additive]
    [PreservesLimitsOfShape (Discrete ℕ) F]
    (RF : DerivedCategory X.Modules ⥤ DerivedCategory B)
    (alpha : F.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶
      DerivedCategory.Qh ⋙ RF)
    [RF.IsRightDerivedFunctor alpha
      (HomotopyCategory.quasiIso X.Modules (ComplexShape.up ℤ))]
    (N : ℕ)
    (hRF : ∀ (M : X.Modules), M.IsQuasicoherent → ∀ (p : ℤ), (N : ℤ) ≤ p →
      IsZero ((F.rightDerivedPlus p).obj M))
    (E : DerivedCategory X.Modules)
    (hE : ∀ j : ℤ,
      ((DerivedCategory.homologyFunctor X.Modules j).obj E).IsQuasicoherent)
    (b i : ℤ) (hi : b ≤ i) :
    IsIso ((DerivedCategory.homologyFunctor B i).map
      (RF.map ((DerivedCategory.TStructure.t.truncGEπ (b - (N : ℤ) + 1)).app E)))

AlgebraicGeometry.isGE_rightDerivedFunctor_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/AffineVanishing/DerivedBounds.lean, line 102. The attribute's comment: “part (3), lower bound”.

A total right derived functor of an additive functor out of the 𝒪_X-modules of a scheme preserves the lower end of the range of degrees in which an object with quasi-coherent cohomology lives.

theorem isGE_rightDerivedFunctor_obj
    (E : DerivedCategory X.Modules)
    (hcoh : ∀ j : ℤ,
      ((DerivedCategory.homologyFunctor X.Modules j).obj E).IsQuasicoherent)
    (a : ℤ) (hE : E.IsGE a) : (RF.obj E).IsGE a

AlgebraicGeometry.isIso_homologyFunctor_map_rightDerivedFunctor_truncLEι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/AffineVanishing/DerivedBounds.lean, line 116. The attribute's comment: “part (1)”.

A total right derived functor of an additive functor out of the 𝒪_X-modules of a scheme agrees in degrees at most a on an object with quasi-coherent cohomology and on its canonical truncation in degrees at most a.

theorem isIso_homologyFunctor_map_rightDerivedFunctor_truncLEι
    (E : DerivedCategory X.Modules)
    (hE : ∀ j : ℤ,
      ((DerivedCategory.homologyFunctor X.Modules j).obj E).IsQuasicoherent)
    (a i : ℤ) (hi : i ≤ a) :
    IsIso ((DerivedCategory.homologyFunctor B i).map
      (RF.map ((DerivedCategory.TStructure.t.truncLEι a).app E)))

AlgebraicGeometry.isLE_rightDerivedFunctor_obj_of_isZero_rightDerivedPlus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/AffineVanishing/UpperBounds.lean, line 531. The attribute's comment: “part (3), upper bound”.

Stacks Project, Tag 08D4, part (3), the upper bound. Let X be a scheme, let F be an additive functor out of the 𝒪_X-modules which preserves countable products, and let RF be a total right derived functor of F on D(𝒪_X). Suppose the higher right derived functors R^pF vanish on every quasi-coherent module in every degree p ≥ N. If an object E of D(𝒪_X) has quasi-coherent cohomology sheaves and lives in degrees ≤ b, then RF(E) lives in degrees ≤ b + N - 1.

The canonical truncation triangle τ_{≤ b-1}E ⟶ E ⟶ τ_{≥ b}E reduces the claim to its third vertex, concentrated in degree b and so covered by the vanishing hypothesis, and to its first vertex, where the bound b - 1 + N — one worse, which is why the triangle is used — is supplied by the E = R\lim \tau_{\geq -n}E argument: E is the derived limit of its truncations from below ([Stacks, Tag 08D3]), RF carries that derived limit to a derived limit ([Stacks, Tag 08U1]), each RF(τ_{≥ -n}E) lives in degrees ≤ b + N - 1 because τ_{≥ -n}E is bounded, and a derived limit of such a tower lives in degrees ≤ b + N.

theorem isLE_rightDerivedFunctor_obj_of_isZero_rightDerivedPlus (N : ℕ)
    (hRF : ∀ M : SheafOfModules.{u} X.ringCatSheaf, M.IsQuasicoherent →
      ∀ p : ℤ, (N : ℤ) ≤ p → IsZero ((F.rightDerivedPlus p).obj M))
    (E : DerivedCategory (SheafOfModules.{u} X.ringCatSheaf))
    (hcoh : ∀ i : ℤ, ((DerivedCategory.homologyFunctor
      (SheafOfModules.{u} X.ringCatSheaf) i).obj E).IsQuasicoherent)
    (b : ℤ) (hE : E.IsLE b) : (RF.obj E).IsLE (b + (N : ℤ) - 1)

AlgebraicGeometry.isIso_homologyFunctor_map_rightDerivedFunctor_truncGEπ_of_isZero_rightDerivedPlus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/AffineVanishing/UpperBounds.lean, line 606. The attribute's comment: “part (2)”.

Stacks Project, Tag 08D4, part (2). In the situation of AlgebraicGeometry.isLE_rightDerivedFunctor_obj_of_isZero_rightDerivedPlus, the canonical comparison H^i(RF(E)) ⟶ H^i(RF(τ_{≥ b - N + 1}E)) is an isomorphism for every i ≥ b.

Write a = b - N + 1. The canonical truncation triangle τ_{≤ a-1}E ⟶ E ⟶ τ_{≥ a}E goes to a distinguished triangle under RF, which is exact; its first vertex has RF-image in degrees ≤ a - 1 + N - 1 = b - 1 by part (3), so H^i and H^{i+1} vanish there for i ≥ b, and the long exact homology sequence makes the second map invertible on H^i.

theorem isIso_homologyFunctor_map_rightDerivedFunctor_truncGEπ_of_isZero_rightDerivedPlus
    (N : ℕ)
    (hRF : ∀ M : SheafOfModules.{u} X.ringCatSheaf, M.IsQuasicoherent →
      ∀ p : ℤ, (N : ℤ) ≤ p → IsZero ((F.rightDerivedPlus p).obj M))
    (E : DerivedCategory (SheafOfModules.{u} X.ringCatSheaf))
    (hE : ∀ i : ℤ, ((DerivedCategory.homologyFunctor
      (SheafOfModules.{u} X.ringCatSheaf) i).obj E).IsQuasicoherent)
    (b i : ℤ) (hi : b ≤ i) :
    IsIso ((DerivedCategory.homologyFunctor B i).map
      (RF.map ((DerivedCategory.TStructure.t.truncGEπ (b - (N : ℤ) + 1)).app E)))

AlgebraicGeometry.isLE_rightDerivedFunctor_obj_addCommGrpCat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TotalDirectImage/DerivedUpperBound.lean, line 298. The attribute's comment: “part (3), upper bound”.

Stacks 08D4, part (3), the upper bound. Let X be a scheme, let F be an additive functor out of the 𝒪_X-modules commuting with countable products, and let (RF, alpha) be a total right derived functor of F on D(𝒪_X). If R ᵖ F vanishes on quasi-coherent modules for every p ≥ N, then RF carries an object with quasi-coherent cohomology lying in degrees ≤ b to one lying in degrees ≤ b + N - 1.

The object is split by the truncation triangle at b into a part concentrated in degree b and a part in degrees ≤ b - 1. The second is handled by the derived limit of its truncation tower: each stage is bounded, so the bounded statement applies with N - 1, [Stacks, Tag 08U1] carries the derived limit through RF, and the derived limit costs the one further degree.

theorem isLE_rightDerivedFunctor_obj_addCommGrpCat (E : DerivedCategory X.Modules)
    (hcoh : ∀ j : ℤ, ((DerivedCategory.homologyFunctor X.Modules j).obj E).IsQuasicoherent)
    (b : ℤ) (hE : E.IsLE b) : (RF.obj E).IsLE (b + (N : ℤ) - 1)

AlgebraicGeometry.isIso_homologyFunctor_map_rightDerivedFunctor_truncGEπ_addCommGrpCat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TotalDirectImage/DerivedUpperBound.lean, line 366. The attribute's comment: “part (2)”.

Stacks 08D4, part (2). With the hypotheses of the upper bound, in degrees at least b a total right derived functor agrees on an object with quasi-coherent cohomology and on its canonical truncation in degrees at least b - N + 1.

The truncation triangle at a = b - N + 1 has first vertex in degrees ≤ a - 1, so the upper bound puts its RF-image in degrees ≤ a - 1 + N - 1 = b - 1; the long exact homology sequence then makes the second map invertible on H^i for every i ≥ b.

theorem isIso_homologyFunctor_map_rightDerivedFunctor_truncGEπ_addCommGrpCat
    (E : DerivedCategory X.Modules)
    (hcoh : ∀ j : ℤ, ((DerivedCategory.homologyFunctor X.Modules j).obj E).IsQuasicoherent)
    (b i : ℤ) (hi : b ≤ i) :
    IsIso ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} i).map
      (RF.map ((DerivedCategory.TStructure.t.truncGEπ (b - (N : ℤ) + 1)).app E)))

Tag 06Z0, a lemma

Tag 06Z0 in the Stacks Project.

AlgebraicGeometry.isIso_derivedTildeGlobalSectionsAdjunction_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/AffineDerivedEquivalence.lean, line 130. The attribute's comment: “canonical unit isomorphism”.

The unit of the derived Spec–Γ adjunction is invertible. For every object M of D(R) the canonical map M ⟶ RΓ(Spec R, M^~) is an isomorphism.

This is AlgebraicGeometry.isIso_derivedTildeGlobalSectionsAdjunction_unit_app_of_quasiIso fed with unbounded affine vanishing for the complexes M̃^•, which is AlgebraicGeometry.quasiIso_globalSectionsOver_map_tilde.

theorem isIso_derivedTildeGlobalSectionsAdjunction_unit :
    IsIso (derivedTildeGlobalSectionsAdjunction R).val.unit

AlgebraicGeometry.derivedTilde_isEquivalence, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/AffineDerivedEquivalence.lean, line 233. The attribute's comment: “sheafification equivalence”.

Derived sheafification is an equivalence D(R) ≌ D_QCoh(𝒪_{Spec R}). This is the remaining content of [Stacks, Tag 06Z0] for the two edges ~ and (06VT) of its triangle.

Derived sheafification is exact and fully faithful, and its right adjoint, derived global sections, has zero kernel; by [Stacks, Tag 09J1] that is enough.

instance derivedTilde_isEquivalence : (derivedTilde R).IsEquivalence

AlgebraicGeometry.derivedGlobalSectionsQuasicoherent_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/AffineDerivedEquivalence.lean, line 242. The attribute's comment: “global sections equivalence”.

Unbounded derived global sections D_QCoh(𝒪_{Spec R}) ⥤ D(R) is an equivalence, being right adjoint to the equivalence AlgebraicGeometry.derivedTilde. This is the RΓ(X, -) edge of the triangle of [Stacks, Tag 06Z0].

theorem derivedGlobalSectionsQuasicoherent_isEquivalence :
    (derivedGlobalSectionsQuasicoherent R).IsEquivalence

AlgebraicGeometry.isIso_derivedTildeGlobalSectionsAdjunction_counit_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/AffineDerivedEquivalence.lean, line 258. The attribute's comment: “canonical counit isomorphism”.

The counit of the derived Spec–Γ adjunction is invertible on D_QCoh(𝒪_{Spec R}). For every object E of D(𝒪_{Spec R}) with quasi-coherent cohomology sheaves the canonical map RΓ(Spec R, E)^~ ⟶ E is an isomorphism.

The left adjoint derivedTilde R ⋙ ι is fully faithful, the unit being invertible, so its counit is invertible exactly on its essential image; and E is in that essential image because derived sheafification is essentially surjective onto D_QCoh(𝒪_{Spec R}). The restriction to objects with quasi-coherent cohomology cannot be dropped: RΓ(Spec R, E)^~ ⟶ E fails to be invertible as soon as some cohomology sheaf of E is not quasi-coherent, which is why the adjunction itself is not an equivalence.

theorem isIso_derivedTildeGlobalSectionsAdjunction_counit_app
    (E : (DerivedCategoryB.derivedCategoryB (A := (Spec R).Modules)
      (SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf)).FullSubcategory) :
    IsIso ((derivedTildeGlobalSectionsAdjunction R).val.counit.app
      ((DerivedCategoryB.derivedCategoryB (A := (Spec R).Modules)
        (SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf)).ι.obj E))

Stacks.DerivedQCoh.derivedQuasicoherentComparison_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/AffineDerivedEquivalence.lean, line 293. The attribute's comment: “comparison equivalence”.

The comparison functor of [Stacks, Tag 06VT] is an equivalence on an affine scheme. The canonical functor D(QCoh(𝒪_{Spec R})) ⥤ D_QCoh(𝒪_{Spec R}) is an equivalence of triangulated categories.

This is the first assertion of [Stacks, Tag 08D9] part (3). It is Stacks.DerivedQCoh.derivedTilde_isEquivalence_iff_comparison applied to AlgebraicGeometry.derivedTilde_isEquivalence: the ~ edge of [Stacks, Tag 06Z0] is an equivalence of abelian categories, so the comparison functor is an equivalence exactly when derived sheafification is.

theorem derivedQuasicoherentComparison_isEquivalence (R : CommRingCat.{u}) :
    (derivedQuasicoherentComparison.{u} (Spec R)).IsEquivalence

AlgebraicGeometry.AffineDerivedSections.full_derivedSectionsLeftAdjoint, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/AffineDerivedSectionsLeftAdjoint.lean, line 212. The attribute's comment: “the left adjoint of derived global sections is fully faithful on an affine scheme”.

The left adjoint of RΓ(S, -) is full on an affine scheme; see derivedSectionsLeftAdjointFullyFaithful.

instance full_derivedSectionsLeftAdjoint :
    (derivedBaseExtension S.toRingedSpace).Full

AlgebraicGeometry.AffineDerivedSections.faithful_derivedSectionsLeftAdjoint, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/AffineDerivedSectionsLeftAdjoint.lean, line 219. The attribute's comment: “the left adjoint of derived global sections is fully faithful on an affine scheme”.

The left adjoint of RΓ(S, -) is faithful on an affine scheme; see derivedSectionsLeftAdjointFullyFaithful.

instance faithful_derivedSectionsLeftAdjoint :
    (derivedBaseExtension S.toRingedSpace).Faithful

AlgebraicGeometry.AffineDerivedSections.essImage_derivedSectionsLeftAdjoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/AffineDerivedSectionsLeftAdjoint.lean, line 235. The attribute's comment: “the essential image of that left adjoint is the quasi-coherent part”.

Every complex of 𝒪_S-modules with quasi-coherent cohomology sheaves is in the essential image of the left adjoint of RΓ(S, -), S being affine. This is the predicate AlgebraicGeometry.IsQCohAll of the Künneth development, written out.

Pulling U back along S ≅ Spec Γ(S, 𝒪_S) keeps the cohomology sheaves quasi-coherent, by [Stacks, Tag 08DW] part (1); over Spec Γ(S, 𝒪_S) the result is a derived sheafification by [Stacks, Tag 06Z0], AlgebraicGeometry.StandardModel.exists_iso_mapDerivedCategory; and pushing that back through derivedSectionsLeftAdjointIso and the round trip of the derived pullbacks along the two directions of the isomorphism exhibits U itself.

theorem essImage_derivedSectionsLeftAdjoint
    (U : DerivedCategory (SheafOfModules.{u} (structureSheafRing S.toRingedSpace)))
    (hU : ∀ j : ℤ, ((DerivedCategory.homologyFunctor
      (SheafOfModules.{u} (structureSheafRing S.toRingedSpace)) j).obj U).IsQuasicoherent) :
    (derivedBaseExtension S.toRingedSpace).essImage U

Stacks.DerivedQCoh.derivedTildeEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/Basic.lean, line 164. The attribute's comment: “the tilde edge: D(A) ≌ D(QCoh(𝒪_X))”.

Stacks Project, Tag 06Z0 (the tilde edge). For X = Spec A the functor M ↦ M^~ is an equivalence of triangulated categories from D(A) to D(QCoh(𝒪_X)). This is the arrow labelled ~ in the triangle of Stacks 06Z0; the other two edges, the functor (06VT) and RΓ(X, -), are not treated here.

The underlying functor is AlgebraicGeometry.tildeEquiv.functor.mapDerivedCategory, by definition.

def derivedTildeEquiv : DerivedCategory (ModuleCat.{u} R) ≌
    DerivedCategory (SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf).FullSubcategory

Stacks.DerivedQCoh.derivedQuasicoherentComparison_isEquivalence_of_isAffine_atModel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/ComparisonAffine.lean, line 306. The attribute's comment: “comparison equivalence, any affine scheme at any model”.

[Stacks, Tag 06Z0]. For every affine scheme X the comparison functor i_X : D(QCoh(𝒪_X)) ⥤ D_QCoh(𝒪_X) of [Stacks, Tag 06VT] is an equivalence of triangulated categories, at every choice of the two derived categories.

Stacks.DerivedQCoh.derivedQuasicoherentComparison_isEquivalence is this statement for Spec R at the locally small model. An affine scheme is isomorphic to Spec Γ(X, ⊤) by AlgebraicGeometry.Scheme.isoSpec, and transporting along that isomorphism simultaneously changes the scheme and the model.

Stacks.DerivedQCoh.derivedQuasicoherentComparison_isEquivalence_of_isAffine is this statement at the locally small model alone, that is the case w = u.

theorem derivedQuasicoherentComparison_isEquivalence_of_isAffine_atModel (X : Scheme.{u})
    [IsAffine X]
    [HasDerivedCategory.{w} (SheafOfModules.{u} X.ringCatSheaf)]
    [HasDerivedCategory.{w} (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory] :
    (derivedQuasicoherentComparison.{w} X).IsEquivalence

AlgebraicGeometry.derivedGlobalSectionsHomologyZeroIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/DegreeZeroCohomology.lean, line 486. The attribute's comment: “degree-zero cohomology”.

Stacks 06Z0, degree-zero cohomology. On an affine scheme the degree-zero cohomology of derived global sections is the global sections of the degree-zero cohomology sheaf: H⁰(RΓ(Spec R, E)) ≅ Γ(Spec R, H⁰(E)) for E in D_QCoh(𝒪_{Spec R}), naturally in E.

This is AlgebraicGeometry.derivedGlobalSectionsQuasicoherentCompHomologyIso in degree zero. Its normalization on global cycles, which pins it down uniquely, is AlgebraicGeometry.globalSectionsCyclesToHomology_comp_derivedGlobalSectionsHomologyZeroIso.

def derivedGlobalSectionsHomologyZeroIso :
    derivedGlobalSectionsQuasicoherent R ⋙
        DerivedCategory.homologyFunctor (ModuleCat.{u} R) 0 ≅
      (DerivedCategoryB.derivedCategoryB (A := (Spec R).Modules)
        (SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf)).ι ⋙
        DerivedCategory.homologyFunctor (Spec R).Modules 0 ⋙
          globalSectionsOver (𝟙 (Spec R))

AlgebraicGeometry.globalSectionsCyclesToHomology_comp_derivedGlobalSectionsHomologyZeroIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/DegreeZeroCohomology.lean, line 747. The attribute's comment: “canonical degree-zero comparison”.

Stacks 06Z0, the canonical degree-zero comparison. The degree-zero identification H⁰(RΓ(Spec R, E)) ≅ Γ(Spec R, H⁰(E)) of AlgebraicGeometry.derivedGlobalSectionsHomologyZeroIso sends a global cycle of a complex K with quasi-coherent cohomology to its section of the degree-zero cohomology sheaf: the composite Γ(Spec R, Z⁰(K)) ⟶ H⁰(Γ(Spec R, K)) ⟶ H⁰(RΓ(Spec R, Q K)) ⟶ Γ(Spec R, H⁰(Q K)) ⟶ Γ(Spec R, H⁰(K)) is Γ(Spec R, -) applied to K.homologyπ 0.

Together with naturality this characterizes the isomorphism: AlgebraicGeometry.globalSectionsCyclesToHomology is an epimorphism, being the isomorphism Γ(Z⁰(K)) ≅ Z⁰(Γ(K)) followed by HomologicalComplex.homologyπ. The content is AlgebraicGeometry.globalSectionsHomologyComparison_eq.

theorem globalSectionsCyclesToHomology_comp_derivedGlobalSectionsHomologyZeroIso
    (K : CochainComplex (Spec R).Modules ℤ)
    (hK : (DerivedCategoryB.derivedCategoryB (A := (Spec R).Modules)
      (SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf)) (DerivedCategory.Q.obj K)) :
    globalSectionsCyclesToHomology (𝟙 (Spec R)) K 0 ≫
        (DerivedCategory.homologyFunctorFactors (ModuleCat.{u} R) 0).inv.app
          (((globalSectionsOver (𝟙 (Spec R))).mapHomologicalComplex
            (ComplexShape.up ℤ)).obj K) ≫
        (DerivedCategory.homologyFunctor (ModuleCat.{u} R) 0).map
          (globalSectionsComplexComparison (𝟙 (Spec R)) K) ≫
        (derivedGlobalSectionsHomologyZeroIso R).hom.app ⟨DerivedCategory.Q.obj K, hK⟩ ≫
        (globalSectionsOver (𝟙 (Spec R))).map
          ((DerivedCategory.homologyFunctorFactors (Spec R).Modules 0).hom.app K) =
      (globalSectionsOver (𝟙 (Spec R))).map (K.homologyπ 0)

AlgebraicGeometry.derivedTildeGlobalSectionsAdjunction_counit_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedTildeCounit.lean, line 285. The attribute's comment: “canonical counit isomorphism”.

Stacks 06Z0, the counit clause. On an affine scheme the counit of the canonical derived sheafification–sections adjunction is invertible at every object of D_QCoh(𝒪_{Spec R}): derived sheafification recovers a complex with quasi-coherent cohomology from its derived global sections.

theorem derivedTildeGlobalSectionsAdjunction_counit_isIso (R : CommRingCat.{u})
    [HasDerivedCategory.{w₂} (ModuleCat.{u} R)] :
    let _inst : HasDerivedCategory (Spec R).Modules := HasDerivedCategory.standard _
    ∀ E : (DerivedCategoryB.derivedCategoryB (A := (Spec R).Modules)
      (SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf)).FullSubcategory,
      IsIso ((derivedTildeGlobalSectionsAdjunction R).val.counit.app
        ((DerivedCategoryB.derivedCategoryB (A := (Spec R).Modules)
          (SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf)).ι.obj E))

Tag 08DV, a lemma

Tag 08DV in the Stacks Project.

AlgebraicGeometry.kFlat_tilde, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Modules/TildeKFlat.lean, line 330.

Stacks Project, Tag 08DV. If K is a K-flat complex of A-modules, then K̃ is a K-flat complex of 𝒪_{Spec A}-modules.

By the stalk criterion for K-flatness (Stacks 06YB) it suffices that the stalk complex of K̃ at every point x be K-flat over the stalk ring. That stalk complex is the extension of scalars of K along A → 𝒪_{Spec A, x} (tildeStalkComplexIso), and extension of scalars preserves K-flatness (Stacks 06Y1).

theorem kFlat_tilde (K : CochainComplex (ModuleCat.{u} A) ℤ)
    (hK : CochainComplex.KFlat.{u, u} K) :
    Stacks.SheafOfModules.IsKFlat (specCommRingSheaf A) (tildeComplexMod K)

Tag 0DJK, a lemma

Tag 0DJK in the Stacks Project.

AlgebraicGeometry.affineDerivedPushforward_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/Coherator/AffineDerivedTildePushforward.lean, line 88. The attribute's comment: “pushforward route”.

Stacks Project, Tag 0DJK. Derived direct image under a morphism of affine schemes preserves quasi-coherent cohomology.

public theorem affineDerivedPushforward_isQuasicoherent
    (R S : CommRingCat.{u}) (φ : R ⟶ S)
    (Rf : DerivedCategory (Spec S).Modules ⥤ DerivedCategory (Spec R).Modules)
    (α : (Scheme.Modules.pushforward (Spec.map φ)).mapHomologicalComplex (.up ℤ) ⋙
        DerivedCategory.Q ⟶ DerivedCategory.Q ⋙ Rf)
    [Rf.IsRightDerivedFunctor α
      (HomologicalComplex.quasiIso (Spec S).Modules (.up ℤ))]
    (K : QuasicoherentDerivedCategory (Spec S)) :
    DerivedCategoryB.derivedCategoryB
      (SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf)
      (Rf.obj K.obj)

AlgebraicGeometry.affineDerivedPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/Coherator/AffineDerivedTildePushforward.lean, line 122. The attribute's comment: “commutativity”.

Stacks Project, Tag 0DJK. The affine associated-sheaf/derived-pushforward square commutes naturally: derived direct image corresponds to restriction of scalars.

public noncomputable def affineDerivedPushforwardIso
    (R S : CommRingCat.{u}) (φ : R ⟶ S)
    (Rf : DerivedCategory (Spec S).Modules ⥤ DerivedCategory (Spec R).Modules)
    (α : (Scheme.Modules.pushforward (Spec.map φ)).mapHomologicalComplex (.up ℤ) ⋙
        DerivedCategory.Q ⟶ DerivedCategory.Q ⋙ Rf)
    [Rf.IsRightDerivedFunctor α
      (HomologicalComplex.quasiIso (Spec S).Modules (.up ℤ))] :
    affineTildeQuasicoherent S ⋙ affineDerivedPushforwardQuasicoherent R S φ Rf α ≅
      (ModuleCat.restrictScalars φ.hom).mapDerivedCategory ⋙ affineTildeQuasicoherent R

AlgebraicGeometry.derivedTildeCompDerivedQuasicoherentPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/Coherator/AffineDerivedPushforward.lean, line 424.

Stacks 0DJK. Let φ : R ⟶ S and let f = Spec φ : Spec S ⟶ Spec R. Then the square D(S) ⟶ D_QCoh(𝒪_{Spec S}) ⟶^{Rf_*} D_QCoh(𝒪_{Spec R}), D(S) ⟶^{restriction of scalars} D(R) ⟶ D_QCoh(𝒪_{Spec R}) commutes: derived direct image along a morphism of affine schemes corresponds, under derived sheafification, to derived restriction of scalars.

This is AlgebraicGeometry.derivedTildeCompIso_of_comparisonSquare with its hypothesis hsq discharged by AlgebraicGeometry.derivedQuasicoherentComparisonSquare, the commuting square of [Stacks, Tag 08D7]. It is also the first assertion of [Stacks, Tag 0A9F].

public def derivedTildeCompDerivedQuasicoherentPushforwardIso :
    derivedTilde S ⋙ derivedQuasicoherentPushforward (Spec.map φ) ≅
      (ModuleCat.restrictScalars φ.hom).mapDerivedCategory ⋙ derivedTilde R

Tag 08DW, a lemma

Tag 08DW in the Stacks Project.

AlgebraicGeometry.affineSchemePullbackComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedTilde/AffineSchemePullbackComparison.lean, line 92. The attribute's comment: “part (2) for a morphism of arbitrary affine schemes”.

[Stacks, Tag 08DW] part (2) for a morphism of arbitrary affine schemes. Let g : Y ⟶ X be a morphism of affine schemes, given by the ring map g.appTop : Γ(X, ⊤) ⟶ Γ(Y, ⊤). Then the square

D(Γ(X, ⊤)) ⟶ D(𝒪_X), D(Γ(Y, ⊤)) ⟶ D(𝒪_Y), - ⊗ᴸ Γ(Y, ⊤) on the left and Lg^* on the right,

commutes: Lg^* of the complex of sheaves associated to an object of D(Γ(X, ⊤)) is the complex of sheaves associated to its derived extension of scalars.

This is AlgebraicGeometry.affinePullbackComparison conjugated by the two canonical isomorphisms X ≅ Spec Γ(X, ⊤) and Y ≅ Spec Γ(Y, ⊤), the composition formula Stacks.Duality.derivedPullbackCompIso crossing the resulting two triangles.

def affineSchemePullbackComparison {X Y : Scheme.{u}} [IsAffine X] [IsAffine Y] (g : Y ⟶ X) :
    affineSchemeDerivedTilde X ⋙ Stacks.Duality.derivedPullback g ≅
      (CochainComplex.DerivedExtensionScalars.totalDerivedExtensionScalars.{u, u, u}
          (CommRingCat.Hom.hom g.appTop)).functor ⋙
        affineSchemeDerivedTilde Y

Stacks.Duality.isQuasicoherent_homology_derivedPullback', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedTilde/QuasiCoherentDerivedPullback.lean, line 422. The attribute's comment: “part (1): derived pullback preserves quasi-coherence of cohomology”.

[Stacks, Tag 08DW] part (1): Lf^* sends D_QCoh(𝒪_Y) into D_QCoh(𝒪_X). For an arbitrary morphism of schemes f : X ⟶ Y and a complex K of 𝒪_Y-modules all of whose cohomology sheaves are quasi-coherent, every cohomology sheaf of Lf^*K is quasi-coherent.

This is Stacks.Duality.isQuasicoherent_homology_derivedPullback, with hess found by instance search from AlgebraicGeometry.derivedTilde_isEquivalence.

theorem isQuasicoherent_homology_derivedPullback' {X Y : Scheme.{u}} (f : X ⟶ Y)
    (K : quasiCoherentDerivedCategory Y) (i : ℤ) :
    ((DerivedCategory.homologyFunctor X.Modules i).obj
      ((derivedPullback f).obj K.obj)).IsQuasicoherent

Stacks.Duality.quasiCoherentDerivedPullback', an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedTilde/QuasiCoherentDerivedPullback.lean, line 435. The attribute's comment: “part (1): the restriction D_QCoh(𝒪_Y) ⥤ D_QCoh(𝒪_X) of derived pullback”.

[Stacks, Tag 08DW] part (1), as a functor. Derived pullback along a morphism of schemes restricts to a functor D_QCoh(𝒪_Y) ⥤ D_QCoh(𝒪_X) between the derived categories of complexes with quasi-coherent cohomology.

This is Stacks.Duality.quasiCoherentDerivedPullback at Stacks.Duality.isQuasicoherent_homology_derivedPullback'.

abbrev quasiCoherentDerivedPullback' {X Y : Scheme.{u}} (f : X ⟶ Y) :
    quasiCoherentDerivedCategory Y ⥤ quasiCoherentDerivedCategory X

Stacks.Duality.isQuasicoherent_homology_derivedPullback_anyModel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedTilde/QuasiCoherentDerivedPullback.lean, line 479. The attribute's comment: “part (1) at an arbitrary model of the two derived categories”.

[Stacks, Tag 08DW] part (1) at an arbitrary model of the two derived categories: Lf^* sends D_QCoh(𝒪_Y) into D_QCoh(𝒪_X). For an arbitrary morphism of schemes f : X ⟶ Y and an object E of D(𝒪_Y) all of whose cohomology sheaves are quasi-coherent, every cohomology sheaf of Lf^*E is quasi-coherent.

The model of the two derived categories is a free [HasDerivedCategory.{w}] binder, so this serves the locally small model of Stacks.Duality.isQuasicoherent_homology_derivedPullback' and CategoryTheory.HasDerivedCategory.standard alike. By [Stacks, Tag 06YF] the object E is the class of a K-flat complex P, at that model Lf^*E is the class of f^*P by Stacks.Cohomology.derivedPullbackIsoPullbackOfKFlat, and the cohomology sheaves of f^*P are quasi-coherent by isQuasicoherent_homology_modulePullback_of_kFlat.

theorem isQuasicoherent_homology_derivedPullback_anyModel {X Y : Scheme.{u}} (f : X ⟶ Y)
    [HasDerivedCategory.{w₁} (SheafOfModules.{u} (structureSheafRing X.toRingedSpace))]
    [HasDerivedCategory.{w₂} (SheafOfModules.{u} (structureSheafRing Y.toRingedSpace))]
    (E : DerivedCategory (SheafOfModules.{u} (structureSheafRing Y.toRingedSpace)))
    (hE : ∀ j : ℤ, ((DerivedCategory.homologyFunctor
      (SheafOfModules.{u} (structureSheafRing Y.toRingedSpace)) j).obj E).IsQuasicoherent) (i : ℤ) :
    ((DerivedCategory.homologyFunctor (SheafOfModules.{u} (structureSheafRing X.toRingedSpace))
        i).obj
      ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
        f.toLRSHom.toShHom).obj E)).IsQuasicoherent

Declarations registered for the tag:

• AlgebraicGeometry.affinePullbackComparison, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Duality/DerivedTilde/QuasiCoherentDerivedPullback.lean, line 525 (StacksFrontier): “part (2): the affine comparison square Lf^*(M̃^•) ≅ (S ⊗ᴸ_R M^•)~”.
• AlgebraicGeometry.affinePullbackComparison_fac, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Duality/DerivedTilde/QuasiCoherentDerivedPullback.lean, line 528 (StacksFrontier): “part (2): the canonical normalisation of the affine comparison square”.

Tag 08DX, a lemma

Tag 08DX in the Stacks Project.

AlgebraicGeometry.affineTensorComplexIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedTilde/AffineDerivedTensor.lean, line 250. The attribute's comment: “part (2): the totalised ordinary comparison”.

The totalised affine tensor comparison. For complexes M^• and K^• of R-modules, the complex of 𝒪_{Spec R}-modules associated to the total tensor complex Tot(M^• ⊗_R K^•) is canonically the total tensor complex Tot(M̃^• ⊗_{𝒪_{Spec R}} K̃^•) of the associated complexes.

The isomorphism is returned together with the formula for its value on the summand of total degree n indexed by (i, j): there it is the degreewise comparison AlgebraicGeometry.tildeTensorIso of [Stacks, Tag 01I8] at M^i and K^j. That formula determines the isomorphism, since the source of total degree n is the direct sum of those summands, so it is carried in the type rather than stated separately.

public def affineTensorComplexIso (R : CommRingCat.{u})
    (M K : CochainComplex (ModuleCat.{u} R) ℤ) :
    { e : tildeComplexMod (A := R) (M ⊗ K) ≅
        ((tensorComplex.{u, u, u} (specCommRingSheaf R)).obj (tildeComplexMod (A := R) M)).obj
          (tildeComplexMod (A := R) K) //
      ∀ (i j n : ℤ) (h : i + j = n),
        (tilde.functor R).map (HomologicalComplex.ιMapBifunctor M K
            (curriedTensor (ModuleCat.{u} R)) (ComplexShape.up ℤ) i j n h) ≫ e.hom.f n =
          (tildeTensorIso R (M.X i) (K.X j)).hom ≫
            HomologicalComplex.ιMapBifunctor (tildeComplexMod (A := R) M)
              (tildeComplexMod (A := R) K)
              (sheafTensor.{u, u, u, u, u} (specCommRingSheaf R)) (ComplexShape.up ℤ) i j n h }

AlgebraicGeometry.affineDerivedTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedTilde/AffineDerivedTensor.lean, line 343. The attribute's comment: “part (2): the affine comparison”.

Stacks Project, Tag 08DX, part (2). On the spectrum of a commutative ring R, the derived tensor product of two associated complexes of sheaves of modules is the complex associated to their derived tensor product over R:

M̃^• ⊗_{𝒪_{Spec R}}^{L} K̃^• ≅ (M^• ⊗_R^{L} K^•)~.

Both arguments are replaced by K-flat representatives, where the two derived tensor products are computed by ordinary total tensor complexes and the comparison is the totalised ordinary comparison affineTensorComplexIso of [Stacks, Tag 01I8]; the representatives are supplied by the definite choices of kFlatRep.

public def affineDerivedTensorIso (R : CommRingCat.{u})
    (M K : CochainComplex.DerivedTensor.DObj (R : Type u)) :
    (((Stacks.Cohomology.TorAmplitude.derTensor.{u, u} (Spec R).toRingedSpace).tensor.obj
          ((tildeDS R).obj M)).obj ((tildeDS R).obj K)) ≅
      (tildeDS R).obj
        (((CochainComplex.DerivedTensor.canonicalDerivedTensorProduct
          (R : Type u)).tensor.obj M).obj K)

AlgebraicGeometry.affineDerivedTensorIsoStandard, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedTilde/AffineDualizingPair.lean, line 119. The attribute's comment: “part (2): the affine comparison, at the standard model”.

On the spectrum of a commutative ring R, the derived tensor product of the complexes of sheaves of modules associated to M and K is the complex associated to their derived tensor product over R, at the standard model:

M̃^• ⊗^L_{𝒪_{Spec R}} K̃^• ≅ (M^• ⊗^L_R K^•)~.

def affineDerivedTensorIsoStandard (M K : DerivedCategory (ModuleCat.{u} R)) :
    ((derivedTensorAsSiteDatum (Spec R).sheaf).tensor.obj
          ((Stacks.Duality.derivedTildeStructureSheafModules R).obj M)).obj
        ((Stacks.Duality.derivedTildeStructureSheafModules R).obj K) ≅
      (Stacks.Duality.derivedTildeStructureSheafModules R).obj
        (((canonicalDerivedTensorProduct (R : Type u)).tensor.obj M).obj K)

Stacks.Duality.isQuasicoherent_homology_derivedTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedTilde/QuasiCoherentDerivedTensor.lean, line 524. The attribute's comment: “part (1): D_QCoh is closed under derived tensor product”.

[Stacks, Tag 08DX] part (1): D_QCoh(𝒪_X) is closed under the derived tensor product. Let X be a scheme and let K and L be complexes of 𝒪_X-modules all of whose cohomology sheaves are quasi-coherent. Then every cohomology sheaf of K ⊗ᴸ_{𝒪_X} L is quasi-coherent.

This is isQuasicoherent_homology_derivedTensor_of_tensorTilde with its hypothesis discharged by exists_iso_derivedTilde_derivedTensor.

theorem isQuasicoherent_homology_derivedTensor (X : Scheme.{u})
    (K L : quasiCoherentDerivedCategory X) (i : ℤ) :
    ((DerivedCategory.homologyFunctor X.Modules i).obj
      (((derivedTensor X).obj K.obj).obj L.obj)).IsQuasicoherent

Stacks.Duality.quasiCoherentDerivedTensor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedTilde/QuasiCoherentDerivedTensor.lean, line 536. The attribute's comment: “part (1): the restriction D_QCoh ⥤ D_QCoh ⥤ D_QCoh of the derived tensor product”.

[Stacks, Tag 08DX] part (1), as structure: the derived tensor product restricts to D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_X). This is quasiCoherentDerivedTensor_of_tensorTilde with its hypothesis discharged by exists_iso_derivedTilde_derivedTensor.

abbrev quasiCoherentDerivedTensor (X : Scheme.{u}) :
    quasiCoherentDerivedCategory X ⥤ quasiCoherentDerivedCategory X ⥤
      quasiCoherentDerivedCategory X

Stacks.Duality.isQuasicoherent_homology_derivedTensor_anyModel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedTilde/QuasiCoherentDerivedTensorAnyModel.lean, line 113. The attribute's comment: “part (1) at an arbitrary model of the derived category”.

[Stacks, Tag 08DX] part (1) at an arbitrary model of D(𝒪_X): D_QCoh(𝒪_X) is closed under the derived tensor product. For a scheme X and objects E, A of D(𝒪_X) all of whose cohomology sheaves are quasi-coherent, every cohomology sheaf of E ⊗^𝐋_{𝒪_X} A is quasi-coherent.

The model of the derived category is a free [HasDerivedCategory.{w}] binder, so this serves the locally small model of Stacks.Duality.isQuasicoherent_homology_derivedTensor and CategoryTheory.HasDerivedCategory.standard alike. A is the class of a K-flat complex P by [Stacks, Tag 06YS], E is the class of some complex C, the K-flat comparison of [Stacks, Tag 06YU] identifies E ⊗^𝐋_{𝒪_X} A with the class of Tot(C ⊗_{𝒪_X} P), and the cohomology of that complex is quasi-coherent by isQuasicoherent_homology_tensorComplex.

theorem isQuasicoherent_homology_derivedTensor_anyModel (X : Scheme.{u})
    [HasDerivedCategory.{w} (Modules X.toRingedSpace.sheaf)]
    (E A : DerivedCategory (Modules X.toRingedSpace.sheaf))
    (hE : ∀ j : ℤ, ((DerivedCategory.homologyFunctor
      (Modules X.toRingedSpace.sheaf) j).obj E).IsQuasicoherent)
    (hA : ∀ j : ℤ, ((DerivedCategory.homologyFunctor
      (Modules X.toRingedSpace.sheaf) j).obj A).IsQuasicoherent) (i : ℤ) :
    ((DerivedCategory.homologyFunctor (Modules X.toRingedSpace.sheaf) i).obj
      (((derivedTensorProductFunctor X.toRingedSpace.sheaf).obj E).obj A)).IsQuasicoherent

Stacks.Thickenings.isQuasicoherent_homology_specDerivedTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/ThickeningQuasicoherent.lean, line 244. The attribute's comment: “part (1) on an affine scheme, at the standard model of the derived category”.

[Stacks, Tag 08DX] part (1) on an affine scheme, at the standard model. If every cohomology sheaf of A and of B is quasi-coherent, then so is every cohomology sheaf of A ⊗ᴸ_{𝒪_{Spec R}} B.

This is Stacks.Duality.isQuasicoherent_homology_derivedTensor_spec, whose only locally small-pinned input was essential surjectivity of derived sheafification, [Stacks, Tag 06Z0]; that is available at the standard model as AlgebraicGeometry.StandardModel.exists_iso_mapDerivedCategory, so the argument runs verbatim. A and B are derived sheafifications of complexes of R-modules, exists_iso_derivedTilde_derivedTensor_standard makes their derived tensor product one as well, and the cohomology sheaves of a derived sheafification are quasi-coherent by construction.

public theorem isQuasicoherent_homology_specDerivedTensor (R : CommRingCat.{u})
    (A B : DerivedCategory (Spec R).Modules)
    (hA : ∀ n : ℤ, ((DerivedCategory.homologyFunctor (Spec R).Modules n).obj A).IsQuasicoherent)
    (hB : ∀ n : ℤ, ((DerivedCategory.homologyFunctor (Spec R).Modules n).obj B).IsQuasicoherent)
    (i : ℤ) :
    ((DerivedCategory.homologyFunctor (Spec R).Modules i).obj
      (((specDerivedTensor R).obj A).obj B)).IsQuasicoherent

Sources

• Section 36.3, Tag 06YZ
• AxiomMath/Stacks at 5ed82d14

LeanStacks.AlgebraicGeometry.QuasicoherentDerived.derivedQuasicoherentComparison · Stacks.AlgebraicGeometry.QuasicoherentDerived.derivedQuasicoherentComparisonCommShift · Stacks.AlgebraicGeometry.QuasicoherentDerived.derivedQuasicoherentComparisonIsTriangulated · AlgebraicGeometry.hasCoproducts_quasicoherentDerivedCategory · AlgebraicGeometry.cohomology_isLimit_of_isDerivedLimit_of_epi · AlgebraicGeometry.isDerivedLimit_single_limit_homology · AlgebraicGeometry.isZero_cohomology_limit_homology_of_isAffineOpen · AlgebraicGeometry.isIso_to_isDerivedLimit_truncGETower

Section36.4 Total direct image#

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

Tag 08D5, a lemma

Tag 08D5 in the Stacks Project.

Stacks.Duality.exists_isLE_derivedPushforward_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedPushforward/UniformBound.lean, line 116. The attribute's comment: “part (2), in the duality spelling”.

[Stacks, Tag 08D5] part (2), in the duality spelling. Let f : X ⟶ Y be a quasi-compact and quasi-separated morphism of schemes with Y quasi-compact. There is an integer N, depending on f alone, such that Rf_*E lives in degrees ≤ b + N for every object E of D_QCoh(𝒪_X) living in degrees ≤ b.

This is AlgebraicGeometry.exists_isZero_homology_derivedPushforward with Rf_* spelled Stacks.Duality.derivedPushforward and the conclusion packaged as DerivedCategory.IsLE; the degree drops by one in the repackaging because the source asserts vanishing at b + N.

theorem exists_isLE_derivedPushforward_obj [QuasiCompact f] [QuasiSeparated f]
    [CompactSpace Y] :
    ∃ N : ℤ, ∀ E : DerivedCategory X.Modules,
      (∀ j : ℤ, ((DerivedCategory.homologyFunctor X.Modules j).obj E).IsQuasicoherent) →
      ∀ b : ℤ, E.IsLE b → ((derivedPushforward f).obj E).IsLE (b + N)

Stacks.Duality.exists_isLE_derivedPushforward_obj_anyModel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedPushforward/UniformBoundAnyModel.lean, line 256. The attribute's comment: “part (2), at an arbitrary derived category”.

[Stacks, Tag 08D5] part (2), at an arbitrary chosen model of the derived categories, in the IsLE form. Let f : X ⟶ Y be a quasi-compact and quasi-separated morphism of schemes with Y quasi-compact. There is an integer N, depending on f alone, such that Rf_*E lives in degrees ≤ b + N for every object E of D(𝒪_X) with quasi-coherent cohomology living in degrees ≤ b.

This is Stacks.Duality.exists_isLE_derivedPushforward_obj with the choice of derived category a binder rather than a term; the degree drops by one in the repackaging because Stacks.Duality.exists_isZero_homology_derivedPushforward_anyModel asserts vanishing at b + N.

theorem exists_isLE_derivedPushforward_obj_anyModel
    [QuasiCompact f] [QuasiSeparated f] [CompactSpace Y] :
    ∃ N : ℤ, ∀ E : DerivedCategory X.Modules,
      (∀ j : ℤ, ((DerivedCategory.homologyFunctor X.Modules j).obj E).IsQuasicoherent) →
      ∀ b : ℤ, E.IsLE b → ((derivedPushforward.{w} f).obj E).IsLE (b + N)

AlgebraicGeometry.exists_uniform_isZero_homology_derivedPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TotalDirectImage/BaseChangeBound.lean, line 144. The attribute's comment: “uniform_bound_after_base_change”.

Stacks 08D5, part (3). Let f : X ⟶ S be a quasi-compact and quasi-separated morphism of schemes with S quasi-compact. There is an integer N, depending only on f, such that for every morphism g : S' ⟶ S the base change f' : X ×_S S' ⟶ S' satisfies H^q(Rf'_* E) = 0 for every q ≥ N and every object E of D(𝒪_{X ×_S S'}) with quasi-coherent cohomology sheaves and vanishing cohomology in positive degrees.

The covering data of f is extracted once, by AlgebraicGeometry.exists_affine_cover_data, and isZero_homology_derivedPushforward_of_commSq is applied to the cartesian square, whose affineness hypothesis is AlgebraicGeometry.isAffineOpen_inf_preimage. The degree N is read off the covering data alone, so it does not depend on g.

This is one of the three declarations carrying [Stacks, Tag 08D5]; the other two are AlgebraicGeometry.isQuasicoherent_derivedPushforward (part (1)) and AlgebraicGeometry.exists_isZero_homology_derivedPushforward_of_isLE_zero (part (2)).

theorem exists_uniform_isZero_homology_derivedPushforward {X S : Scheme.{u}} (f : X ⟶ S)
    [QuasiCompact f] [QuasiSeparated f] [CompactSpace S] :
    ∃ N : ℤ, ∀ (S' : Scheme.{u}) (g : S' ⟶ S)
      (E : DerivedCategory.{u + 1} (pullback f g).Modules),
      (∀ i : ℤ, ((DerivedCategory.homologyFunctor (pullback f g).Modules i).obj
        E).IsQuasicoherent) →
      E.IsLE 0 → ∀ q : ℤ, N ≤ q →
        IsZero ((DerivedCategory.homologyFunctor S'.Modules q).obj
          ((derivedPushforward (pullback.snd f g).toLRSHom.toShHom).obj E))

AlgebraicGeometry.exists_isZero_homology_derivedPushforward_of_isLE_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TotalDirectImage/BoundedCohomologicalDimension.lean, line 131. The attribute's comment: “bounded_cohomological_dimension”.

Let f : X ⟶ S be a quasi-compact and quasi-separated morphism of schemes with S quasi-compact. There is an integer N, depending only on f, such that every object E of D(𝒪_X) with quasi-coherent cohomology sheaves and vanishing cohomology in positive degrees has H^m(Rf_* E) = 0 for all m ≥ N.

theorem exists_isZero_homology_derivedPushforward_of_isLE_zero
    [QuasiCompact f] [QuasiSeparated f] [CompactSpace S] :
    ∃ N : ℤ, ∀ E : DerivedCategory.{u + 1} X.Modules,
      (∀ i : ℤ, ((DerivedCategory.homologyFunctor X.Modules i).obj E).IsQuasicoherent) →
      E.IsLE 0 → ∀ m : ℤ, N ≤ m →
        IsZero ((DerivedCategory.homologyFunctor S.Modules m).obj
          ((derivedPushforward f.toLRSHom.toShHom).obj E))

AlgebraicGeometry.isQuasicoherent_derivedPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TotalDirectImage/QuasiCoherentDirectImage.lean, line 374. The attribute's comment: “quasi_coherent_direct_image”.

Stacks 08D5, part (1). Let f : X ⟶ S be a quasi-compact and quasi-separated morphism of schemes. The unbounded derived direct image Rf_* carries D_QCoh(𝒪_X) into D_QCoh(𝒪_S): the cohomology sheaves of Rf_* E are quasi-coherent for every object E of D(𝒪_X) whose cohomology sheaves are.

Quasi-coherence is local on the target and Rf_* commutes with restriction to an open, which is AlgebraicGeometry.isQuasicoherent_derivedPushforward_of_compactTarget; the affine case is preservesQuasicoherentOnCompactTarget.

theorem isQuasicoherent_derivedPushforward [QuasiCompact f] [QuasiSeparated f]
    (E : QuasicoherentDerivedCategory X) :
    DerivedCategoryB.derivedCategoryB (SheafOfModules.isQuasicoherent S.ringCatSheaf)
      ((RingedSpace.derivedPushforward f.toLRSHom.toShHom).obj E.obj)

AlgebraicGeometry.isQuasicoherent_derivedPushforward_affineLocal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/UnboundedDerivedDirectImage/QuasiCoherence.lean, line 281. The attribute's comment: “part (1)”.

[Stacks, Tag 08D5], part (1). For a quasi-compact and quasi-separated morphism of schemes f : X ⟶ S the unbounded derived direct image Rf_* carries D_QCoh(𝒪_X) into D_QCoh(𝒪_S): the cohomology sheaves of Rf_*E are quasi-coherent whenever those of E are.

The question is local on S, and over an affine open of S it is the quasi-compact-target case AlgebraicGeometry.preservesQuasicoherentOnCompactTarget; the name records that affine-local route, the same statement being reached by the compact-target route in AlgebraicGeometry.isQuasicoherent_derivedPushforward.

theorem isQuasicoherent_derivedPushforward_affineLocal
    (E : QuasicoherentDerivedCategory X) :
    DerivedCategoryB.derivedCategoryB
      (SheafOfModules.isQuasicoherent S.ringCatSheaf)
      ((RingedSpace.derivedPushforward f.toLRSHom.toShHom).obj E.obj)

AlgebraicGeometry.exists_isZero_homology_derivedPushforward_of_isLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/UnboundedDerivedDirectImage/UniformBound.lean, line 424. The attribute's comment: “part (2)”.

[Stacks, Tag 08D5], part (2). Let f : X ⟶ S be a quasi-compact and quasi-separated morphism of schemes with S quasi-compact. There is an integer N, depending on X, S and f alone, such that every object E of D_QCoh(𝒪_X) with H^m(E) = 0 for m > 0 has H^m(Rf_*E) = 0 for m ≥ N.

This is AlgebraicGeometry.exists_isZero_homology_derivedPushforward at b = 0.

theorem exists_isZero_homology_derivedPushforward_of_isLE (f : X ⟶ S) [QuasiCompact f]
    [QuasiSeparated f] [CompactSpace S] :
    ∃ N : ℤ, ∀ E : QuasicoherentDerivedCategory X, E.obj.IsLE 0 → ∀ m : ℤ, N ≤ m →
      IsZero ((DerivedCategory.homologyFunctor S.Modules m).obj
        ((RingedSpace.derivedPushforward f.toLRSHom.toShHom).obj E.obj))

Tag 0G9N, a lemma

Tag 0G9N in the Stacks Project.

AlgebraicGeometry.isIso_to_rightDerived_of_termwise_acyclic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedAcyclic/Pushforward.lean, line 433.

Stacks Project, Tag 0G9N. Let f : X ⟶ S be a quasi-separated and quasi-compact morphism of schemes and let K be a complex of quasi-coherent 𝒪_X-modules each of which is right acyclic for f_*. Then f_* K represents Rf_* K in D(𝒪_S): the canonical comparison from the termwise direct image to any right derived direct image is an isomorphism at K.

theorem isIso_to_rightDerived_of_termwise_acyclic
    {X S : Scheme.{u}} (f : X ⟶ S) [QuasiCompact f] [QuasiSeparated f]
    (K : CochainComplex X.Modules ℤ)
    (hqc : ∀ n, (K.X n).IsQuasicoherent)
    (hacyclic : ∀ n, (Scheme.Modules.pushforward f).rightAcyclic (K.X n))
    (Rf : DerivedCategory X.Modules ⥤ DerivedCategory S.Modules)
    (α : (Scheme.Modules.pushforward f).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rf)
    [Rf.IsRightDerivedFunctor α
      (HomotopyCategory.quasiIso X.Modules (ComplexShape.up ℤ))] :
    IsIso (α.app ((HomotopyCategory.quotient _ _).obj K))

AlgebraicGeometry.isIso_pushforwardComparisonQ_of_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedAffineMorphism/AffinePushforwardComparisonQ.lean, line 83. The attribute's comment: “the comparison Q(f_C) ⟶ Rf_(QC) at the Q spelling: it is invertible for an affine morphism of schemes and a complex of quasi-coherent modules, with no boundedness hypothesis”.

Q(f_*C^•) ⟶ Rf_*(QC^•) is invertible along an affine morphism of schemes, for a cochain complex C^• of quasi-coherent 𝒪_X-modules and with no boundedness hypothesis.

The comparison is the unit of the derived direct image with the two comparisons between Q and Qh ∘ quotient inserted at either end. Those are isomorphisms for every morphism, and the unit is invertible at a complex of quasi-coherent modules along an affine morphism by [Stacks, Tag 0G9N], AlgebraicGeometry.AnyModel.isIso_derivedPushforwardUnit_app_of_isAffineHom.

This is the input that the source's proof of [Stacks, Tag 0B55] gets from [Stacks, Tag 08KS] for a closed embedding, and it is what the affine case of [Stacks, Tag 08I9] needs in its place.

theorem isIso_pushforwardComparisonQ_of_isAffineHom {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsAffineHom f]
    (C : CochainComplex
      (AlgebraicGeometry.RingedSpace.KFlatDerivedPullback.Modules X.toRingedSpace) ℤ)
    (hqc : ∀ n : ℤ, (C.X n : SheafOfModules.{u} X.ringCatSheaf).IsQuasicoherent) :
    IsIso (pushforwardComparisonQ f.toLRSHom.toShHom C)

Tag 0G9P, a lemma

Tag 0G9P in the Stacks Project.

AlgebraicGeometry.isIso_to_derivedGlobalSections_of_termwise_acyclic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedAcyclic/GlobalSections.lean, line 201.

Let X be a quasi-separated and quasi-compact scheme and let K be a complex of quasi-coherent 𝒪_X-modules each of which is right acyclic for Γ(X, -). Then Γ(X, K) represents RΓ(X, K) in D(Γ(X, 𝒪_X)): the canonical comparison from termwise global sections to any right derived global-sections functor is an isomorphism at K.

theorem isIso_to_derivedGlobalSections_of_termwise_acyclic (X : Scheme.{u})
    [CompactSpace X] [QuasiSeparatedSpace X]
    (K : CochainComplex X.Modules ℤ)
    (hqc : ∀ n, (K.X n).IsQuasicoherent)
    (hacyclic : ∀ n, (sectionsFunctor X ⊤).rightAcyclic (K.X n))
    (RΓ : DerivedCategory X.Modules ⥤ DerivedCategory (ModuleCat.{u} Γ(X, ⊤)))
    (α : (sectionsFunctor X ⊤).mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶
      DerivedCategory.Qh ⋙ RΓ)
    [RΓ.IsRightDerivedFunctor α
      (HomotopyCategory.quasiIso X.Modules (ComplexShape.up ℤ))] :
    IsIso (α.app ((HomotopyCategory.quotient _ _).obj K))

Tag 0G9Q, a lemma

Tag 0G9Q in the Stacks Project.

AlgebraicGeometry.hypercohomologySpectralSequence_isBounded, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/HypercohomologySpectralSequence/Convergence.lean, line 275. The attribute's comment: “boundedness”.

Stacks Project, Tag 0G9Q. The hypercohomology spectral sequence of an object of D_QCoh(𝒪_X) on a quasi-compact quasi-separated scheme is bounded: in each total degree only finitely many second-page terms are nonzero.

The second page in bidegree (i, j) is H^i(X, H^j(K)), and H^j(K) is quasi-coherent, so by the uniform vanishing of the cohomology of quasi-coherent modules the term is zero unless 0 ≤ i ≤ N - 1.

theorem hypercohomologySpectralSequence_isBounded (X : Scheme.{u}) [CompactSpace X]
    [QuasiSeparatedSpace X] (K : QuasicoherentDerivedCategory X) :
    IsBounded (hypercohomologySpectralSequence X.toRingedSpace K.obj).spectralSequence

AlgebraicGeometry.hypercohomologySpectralSequence_abutsTo, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/HypercohomologySpectralSequence/Convergence.lean, line 300. The attribute's comment: “convergence”.

Stacks Project, Tag 0G9Q. The hypercohomology spectral sequence of an object K of D_QCoh(𝒪_X) on a quasi-compact quasi-separated scheme converges to the hypercohomology of K: there is a finite decreasing filtration of each H^n(X, K) whose graded pieces are the terms of the infinity page.

The two hypotheses of the convergence statement of [Stacks, Tag 0BKK] are supplied by AlgebraicGeometry.exists_isZero_hypercohomology_filtration_obj and AlgebraicGeometry.exists_isIso_hypercohomologyMap_filtration_ι; what that statement delivers is the abutment of the unrenumbered spectral sequence to the hypercohomology of the underlying complex of the filtration, which is transported to K along the representative and then along the two renumberings.

theorem hypercohomologySpectralSequence_abutsTo (X : Scheme.{u}) [CompactSpace X]
    [QuasiSeparatedSpace X] (K : QuasicoherentDerivedCategory X) :
    (hypercohomologySpectralSequence X.toRingedSpace K.obj).spectralSequence.AbutsTo
      (fun n => (DerivedCategory.homologyFunctor
        (ModuleCat.{u} ((structureSheafRing X.toRingedSpace).obj.obj
          (op (⊤ : Opens X.carrier)))) n).obj
        ((hypercohomologySpectralSequence X.toRingedSpace K.obj).truncation.RΓ.obj K.obj))

Tag 08DZ, a lemma

Tag 08DZ in the Stacks Project.

Stacks.Duality.DerivedPushforward.preservesColimitsOfShape_discrete_qcqsQuasiCoherentDerivedPushforward_locallySmall, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedPushforward/QcohDirectSumsAnyModel.lean, line 599. The attribute's comment: “locally_small_model”.

[Stacks, Tag 08DZ]. Let f : X ⟶ S be a quasi-separated and quasi-compact morphism of schemes. Then Rf_* : D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_S) commutes with direct sums: for every index type α of the scheme universe it preserves α-indexed direct sums.

The index types are those of the scheme universe because those are the ones for which D_QCoh(𝒪_X) has direct sums at all ([Stacks, Tag 08DT], Stacks.Duality.DerivedPushforward.hasCoproducts_quasiCoherentDerivedCategory).

This is the tag at the locally small model of the derived categories, where that universe of index types is also the morphism universe; the companion registration preservesColimitsOfShape_discrete_qcqsQuasiCoherentDerivedPushforward is the tag at CategoryTheory.HasDerivedCategory.standard, where the two universes differ.

theorem preservesColimitsOfShape_discrete_qcqsQuasiCoherentDerivedPushforward_locallySmall
    (α : Type u) :
    PreservesColimitsOfShape (Discrete α)
      (qcqsQuasiCoherentDerivedPushforwardLocallySmall f)

Stacks.Duality.DerivedPushforward.preservesColimitsOfShape_discrete_qcqsQuasiCoherentDerivedPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedPushforward/QuasiCoherentDirectSums.lean, line 558.

[Stacks, Tag 08DZ]. Let f : X ⟶ S be a quasi-separated and quasi-compact morphism of schemes. Then Rf_* : D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_S) commutes with direct sums: for every index type α of the scheme universe it preserves α-indexed direct sums.

The index types are those of the scheme universe because those are the ones for which D_QCoh(𝒪_X) has direct sums at all ([Stacks, Tag 08DT], AlgebraicGeometry.hasCoproducts_quasicoherentDerivedCategory).

theorem preservesColimitsOfShape_discrete_qcqsQuasiCoherentDerivedPushforward (α : Type u) :
    PreservesColimitsOfShape (Discrete α) (qcqsQuasiCoherentDerivedPushforward f)

Stacks.Duality.DerivedPushforward.preservesColimitsOfShape_discrete_qcqsRestrictedDerivedPushforward, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedPushforward/QuasiCoherentDirectSumsLocallySmall.lean, line 415. The attribute's comment: “at the locally small model, which is the one Brown representability runs at”.

[Stacks, Tag 08DZ] at the locally small model, for the canonical restricted functor. Let f : X ⟶ Y be a quasi-compact and quasi-separated morphism of schemes with Y quasi-compact. Then Rf_* : D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_Y) commutes with direct sums indexed by any type of the scheme universe — which at this model is also the morphism universe of the category, so this is the hypothesis [Stacks, Tag 0A8G] asks for.

DerivedPushforward.preservesColimitsOfShape_discrete_qcqsQuasiCoherentDerivedPushforward is the same statement at CategoryTheory.HasDerivedCategory.standard, where HasCoproducts of the morphism universe is false and the statement therefore cannot be fed to Brown representability.

instance preservesColimitsOfShape_discrete_qcqsRestrictedDerivedPushforward (α : Type u) :
    PreservesColimitsOfShape (Discrete α) (qcqsRestrictedDerivedPushforward f)

Sources

• Section 36.4, Tag 08DY
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Duality.exists_isLE_derivedPushforward_obj · Stacks.Duality.exists_isLE_derivedPushforward_obj_anyModel · AlgebraicGeometry.exists_uniform_isZero_homology_derivedPushforward · AlgebraicGeometry.exists_isZero_homology_derivedPushforward_of_isLE_zero · AlgebraicGeometry.isQuasicoherent_derivedPushforward · AlgebraicGeometry.isQuasicoherent_derivedPushforward_affineLocal · AlgebraicGeometry.exists_isZero_homology_derivedPushforward_of_isLE · AlgebraicGeometry.isIso_to_rightDerived_of_termwise_acyclic

Section36.5 Affine morphisms#

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

Tag 0G9R, a lemma

Tag 0G9R in the Stacks Project.

AlgebraicGeometry.isIso_pushforwardToRightDerived_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedAcyclic/AffineMorphism.lean, line 76.

Stacks Project, Tag 0G9R. Let f : X ⟶ Y be an affine morphism of schemes and let K be a complex of quasi-coherent 𝒪_X-modules. Then f_* K = Rf_* K: the right derived direct image is defined at K and the canonical map from the termwise direct image to it is an isomorphism.

theorem isIso_pushforwardToRightDerived_of_isAffine
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsAffineHom f]
    [HasDerivedCategory Y.Modules]
    (K : HomologicalComplex X.Modules (ComplexShape.up ℤ))
    (hK : ∀ i, (K.X i).IsQuasicoherent) :
    ((Scheme.Modules.pushforward f).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh).ComputesRightDerived
        (HomotopyCategory.quasiIso X.Modules (ComplexShape.up ℤ))
        ((HomotopyCategory.quotient X.Modules (ComplexShape.up ℤ)).obj K)

Tag 08I8, a lemma

Tag 08I8 in the Stacks Project.

AlgebraicGeometry.reflectsIsomorphisms_derivedQuasicoherentPushforward_specMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedAffineMorphism/ReflectsIsomorphisms.lean, line 114. The attribute's comment: “a morphism Spec φ of affine schemes”.

[Stacks, Tag 08I8] for a morphism of affine schemes. Let φ : R ⟶ S and let f = Spec φ : Spec S ⟶ Spec R. Then Rf_* : D_QCoh(𝒪_{Spec S}) ⥤ D_QCoh(𝒪_{Spec R}) reflects isomorphisms: a map of complexes with quasi-coherent cohomology is invertible as soon as its derived pushforward is.

Derived sheafification is an equivalence D(S) ≌ D_QCoh(𝒪_{Spec S}) [Stacks, Tag 06Z0] carrying Rf_* to derived restriction of scalars along φ [Stacks, Tag 0DJK], and that functor reflects isomorphisms.

public theorem reflectsIsomorphisms_derivedQuasicoherentPushforward_specMap :
    (derivedQuasicoherentPushforward (Spec.map φ)).ReflectsIsomorphisms

AlgebraicGeometry.reflectsIsomorphisms_derivedQuasicoherentPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedAffineMorphism/ReflectsIsomorphismsAffineHom.lean, line 285.

[Stacks, Tag 08I8]. Let f : X ⟶ Y be an affine morphism of schemes, with Y an arbitrary scheme. Then Rf_* : D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_Y) reflects isomorphisms.

AlgebraicGeometry.derivedQuasicoherentPushforward is by construction the lift of D_QCoh(𝒪_X) ⥤ D(𝒪_X) ⥤ D(𝒪_Y) through the inclusion of D_QCoh(𝒪_Y), so a map of D_QCoh(𝒪_X) whose derived direct image is invertible in D_QCoh(𝒪_Y) has invertible derived direct image in D(𝒪_Y); AlgebraicGeometry.AnyModel.isIso_of_isIso_derivedPushforward_map_of_isAffineHom makes it invertible in D(𝒪_X), and the inclusion of D_QCoh(𝒪_X) is fully faithful, hence reflects isomorphisms.

public theorem reflectsIsomorphisms_derivedQuasicoherentPushforward [IsAffineHom f] :
    (derivedQuasicoherentPushforward f).ReflectsIsomorphisms

Stacks.AlgebraicGeometry.AffinePushforwardTExactness.isIso_of_isIso_derivedPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedAffineMorphism/ReflectsIsomorphismsQuasicoherent.lean, line 86.

[Stacks, Tag 08I8]. Let f : W ⟶ Y be an affine morphism of schemes and let α : E ⟶ F be a morphism of D(𝒪_W) between complexes whose cohomology sheaves are quasi-coherent. If the derived direct image Rf_*α is invertible in D(𝒪_Y), then α is invertible. This is the assertion that Rf_* : D_QCoh(𝒪_W) ⥤ D_QCoh(𝒪_Y) reflects isomorphisms.

theorem isIso_of_isIso_derivedPushforward (f : W ⟶ Y) [IsAffineHom f]
    {E F : DerivedCategory W.Modules}
    (hE : ∀ i : ℤ, ((DerivedCategory.homologyFunctor W.Modules i).obj E).IsQuasicoherent)
    (hF : ∀ i : ℤ, ((DerivedCategory.homologyFunctor W.Modules i).obj F).IsQuasicoherent)
    (α : E ⟶ F)
    (h : IsIso ((derivedPushforward f.toLRSHom.toShHom).map α)) : IsIso α

Tag 08I9, a lemma

Tag 08I9 in the Stacks Project.

AlgebraicGeometry.AffineProjectionFormula.isIso_pullbackPushforwardTensorMap_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedAffineMorphism/AffineProjectionFormulaGeneralBase.lean, line 160. The attribute's comment: “the canonical morphism Rf_O_X ⊗^L E ⟶ Rf_Lf^E is invertible for every affine morphism of schemes f : X ⟶ S and every object E of D_QCoh(O_S), with the genuine derived pullback Lf^ and the genuine derived tensor product ⊗^L, no boundedness, flatness or finiteness hypothesis on E and no hypothesis on S”.

Stacks, Tag 08I9. Let f : X ⟶ S be an affine morphism of schemes and let E be an object of D_QCoh(𝒪_S), that is, an object of D(𝒪_S) all of whose cohomology sheaves are quasi-coherent. Then the canonical morphism

Rf_*𝒪_X ⊗^𝐋_{𝒪_S} E ⟶ Rf_*Lf^*E

is an isomorphism. The derived pullback is the genuine Lf^* of [Stacks, Tag 06YJ], the tensor product is the genuine ⊗^𝐋, and there is no boundedness, flatness or finiteness hypothesis on E and no hypothesis on S.

The proof is the source's. The question is local on S, which is Stacks.Cohomology.DerivedProjectionFormula.isIso_pullbackPushforwardTensorMap_of_openCover over the cover of S by its affine opens; each restriction f|_U is an affine morphism over an affine scheme, and the restricted complex still has quasi-coherent cohomology by isQuasicoherent_homology_derivedPullback_of_isOpenImmersion, so isIso_pullbackPushforwardTensorMap_of_isAffine applies to it.

theorem isIso_pullbackPushforwardTensorMap_unconditional {X S : Scheme.{u}} (f : X ⟶ S)
    [IsAffineHom f] (E : DerivedCategory S.Modules)
    (hE : ∀ n : ℤ, ((DerivedCategory.homologyFunctor S.Modules n).obj E).IsQuasicoherent) :
    IsIso (pullbackPushforwardTensorMap' f.toLRSHom.toShHom E)

Stacks.AlgebraicGeometry.AffinePushforwardTExactness.derivedPushforwardDerivedPullbackTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedAffineMorphism/PullbackPushforwardDerivedTensor.lean, line 114.

For an affine morphism of schemes f : X ⟶ S and a complex E on S with quasi-coherent cohomology,

f_*𝒪_X ⊗^𝐋_{𝒪_S} E ≅ Rf_* Lf^* E,

with the derived tensor product and with no boundedness hypothesis on E.

def derivedPushforwardDerivedPullbackTensorIso (f : X ⟶ S) [IsAffineHom f]
    (E : DerivedCategory (SheafOfModules.{u} (structureSheafRing S.toRingedSpace)))
    (hE : ∀ j : ℤ, ((DerivedCategory.homologyFunctor
      (SheafOfModules.{u} (structureSheafRing S.toRingedSpace)) j).obj E).IsQuasicoherent) :
    ((derivedTensorProductFunctor S.toRingedSpace.sheaf).obj
        ((DerivedCategory.singleFunctor
          (SheafOfModules.{u} (structureSheafRing S.toRingedSpace)) 0).obj
          ((modulePushforward f.toLRSHom.toShHom).obj
            (SheafOfModules.unit (structureSheafRing X.toRingedSpace))))).obj E ≅
      (derivedPushforward f.toLRSHom.toShHom).obj
        ((derivedPullback f.toLRSHom.toShHom).obj E)

Stacks.AlgebraicGeometry.DerivedAffinePushforward.derivedPushforwardPullbackTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedAffineMorphism/PullbackPushforwardTensor.lean, line 198. The attribute's comment: “a SPECIAL CASE of the general statement, which is proved — the tag is closed by AlgebraicGeometry.AffineProjectionFormula.isIso_pullbackPushforwardTensorMap_unconditional. The degree-zero clause: Rf_((f^H)[0]) ≅ (f_𝒪_X ⊗_{𝒪_S} H)[0] for H a quasi-coherent 𝒪_S-module, with the underived f^ and ⊗ in place of the general statement's Lf^* and ⊗ᴸ and E restricted to a module in degree zero”.

[Stacks, Tag 08I9] for E a quasi-coherent module in degree zero, with the underived inverse image and tensor product: for an affine morphism of schemes f : X ⟶ S and a quasi-coherent 𝒪_S-module H,

Rf_*((f^*H)[0]) ≅ (f_*𝒪_X ⊗_{𝒪_S} H)[0]

in D(𝒪_S). Unconditional.

The source states Rf_*Lf^*E ≅ E ⊗^𝐋_{𝒪_S} f_*𝒪_X; here both derived functors on the right-hand side of that identity are replaced by their underived counterparts f^* and ⊗. See the module documentation for what that costs. The proof is pushforwardStructureSheafTensorIso followed by [Stacks, Tag 01XC] in the form derivedPushforwardSingleIso: f^*H is quasi-coherent and f is affine, so the ordinary direct image of f^*H in degree zero is already its derived direct image.

def derivedPushforwardPullbackTensorIso [IsAffineHom f] (H : S.Modules)
    (hH : H.IsQuasicoherent) :
    (Stacks.Duality.derivedPushforward f).obj
        ((DerivedCategory.singleFunctor X.Modules 0).obj ((Scheme.Modules.pullback f).obj H)) ≅
      (DerivedCategory.singleFunctor S.Modules 0).obj
        (((Functor.uncurry.obj (Stacks.SheafOfModules.Tensor.sheafTensor
            ⟨((S.toRingedSpace)).presheaf, ((S.toRingedSpace)).IsSheaf⟩))).obj
          ((Scheme.Modules.pushforward f).obj (SheafOfModules.unit X.ringCatSheaf : X.Modules),
            H))

Stacks.AlgebraicGeometry.DerivedAffinePushforward.derivedPushforwardDerivedPullbackTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedAffineMorphism/PullbackPushforwardTensor.lean, line 250. The attribute's comment: “a SPECIAL CASE of the general statement, which is proved — the tag is closed by AlgebraicGeometry.AffineProjectionFormula.isIso_pullbackPushforwardTensorMap_unconditional. E = H[0] for f affine and H a flat quasi-coherent 𝒪_S-module, with the genuine Lf^ and nothing carried: Rf_Lf^(H[0]) ≅ (f_𝒪_X ⊗_{𝒪_S} H)[0]; the right-hand tensor product is the underived ⊗, not ⊗ᴸ, and E is restricted to a module in degree zero”.

[Stacks, Tag 08I9] for E a flat quasi-coherent module in degree zero, with the genuine derived pullback: for an affine morphism of schemes f : X ⟶ S and a flat quasi-coherent 𝒪_S-module H,

Rf_*Lf^*(H[0]) ≅ (f_*𝒪_X ⊗_{𝒪_S} H)[0],

with nothing assumed beyond those restrictions on f and H. Flatness of H makes H[0] K-flat, so the degree-zero comparison Lf^*(H[0]) ≅ (f^*H)[0] is derivedPullbackSingleIsoOfFlat; the tensor product on the right-hand side is still the underived one.

def derivedPushforwardDerivedPullbackTensorIso [IsAffineHom f] (H : S.Modules)
    (hH : H.IsQuasicoherent)
    (hHflat : SheafOfModules.IsFlat.{u, u, u, u} (O := S.toRingedSpace.sheaf) H) :
    (Stacks.Duality.derivedPushforward f).obj
        ((Stacks.Duality.derivedPullback f).obj
          ((DerivedCategory.singleFunctor S.Modules 0).obj H)) ≅
      (DerivedCategory.singleFunctor S.Modules 0).obj
        (((Functor.uncurry.obj (Stacks.SheafOfModules.Tensor.sheafTensor
            ⟨((S.toRingedSpace)).presheaf, ((S.toRingedSpace)).IsSheaf⟩))).obj
          ((Scheme.Modules.pushforward f).obj (SheafOfModules.unit X.ringCatSheaf : X.Modules),
            H))

Stacks.AlgebraicGeometry.DerivedAffinePushforward.derivedPushforwardDerivedPullbackTensorIsoOfExact, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedAffineMorphism/PullbackPushforwardTensor.lean, line 299. The attribute's comment: “a SPECIAL CASE of the general statement, which is proved — the tag is closed by AlgebraicGeometry.AffineProjectionFormula.isIso_pullbackPushforwardTensorMap_unconditional. E = H[0] for f affine with f^ exact (f flat) and H quasi-coherent, with the genuine Rf_ and Lf^ and nothing carried: Rf_Lf^(H[0]) ≅ (f_𝒪_X ⊗_{𝒪_S} H)[0]; the right-hand tensor product is the underived ⊗, not ⊗ᴸ, and E is restricted to a module in degree zero”.

[Stacks, Tag 08I9] for a flat affine morphism and E a quasi-coherent module in degree zero: for f : X ⟶ S affine with f^* exact and H a quasi-coherent 𝒪_S-module,

Rf_*Lf^*(H[0]) ≅ (f_*𝒪_X ⊗_{𝒪_S} H)[0]

in D(𝒪_S), with no hypothesis carried. Flatness of f replaces the flatness of H asked by derivedPushforwardDerivedPullbackTensorIso: it supplies the degree-zero comparison Lf^*(H[0]) ≅ (f^*H)[0] through derivedPullbackSingleIsoOfExact instead.

Both sides are the source's, except that the tensor product on the right is the ordinary one rather than ⊗^𝐋; for f flat the two agree, but that identification is not proved here.

def derivedPushforwardDerivedPullbackTensorIsoOfExact [IsAffineHom f]
    [PreservesFiniteLimits (Scheme.Modules.pullback f)] (H : S.Modules)
    (hH : H.IsQuasicoherent) :
    (Stacks.Duality.derivedPushforward f).obj
        ((Stacks.Duality.derivedPullback f).obj
          ((DerivedCategory.singleFunctor S.Modules 0).obj H)) ≅
      (DerivedCategory.singleFunctor S.Modules 0).obj
        (((Functor.uncurry.obj (Stacks.SheafOfModules.Tensor.sheafTensor
            ⟨((S.toRingedSpace)).presheaf, ((S.toRingedSpace)).IsSheaf⟩))).obj
          ((Scheme.Modules.pushforward f).obj (SheafOfModules.unit X.ringCatSheaf : X.Modules),
            H))

Stacks.AlgebraicGeometry.AffinePullbackPushforwardTensor.derivedPushforwardDerivedPullbackTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedAffineMorphism/PullbackPushforwardTensorQCoh.lean, line 158. The attribute's comment: “the whole lemma: for an affine morphism of schemes f : X ⟶ S and every K in D_QCoh(𝒪_S), the canonical map f_𝒪_X ⊗ᴸ K ⟶ Rf_Lf^*K is invertible. The tensor factors are written in the opposite order from the source, the derived tensor product of a ringed space being symmetric”.

[Stacks, Tag 08I9]. Let f : X ⟶ S be an affine morphism of schemes. For every K in D_QCoh(𝒪_S),

f_*𝒪_X ⊗^𝐋_{𝒪_S} K ≅ Rf_*Lf^*K,

with the ordinary direct image of the structure sheaf placed in degree zero on the left and the derived tensor product. The left-hand factor is (f_*𝒪_X)[0] rather than Rf_*(𝒪_X[0]) by [Stacks, Tag 01XC] for an affine morphism, which is the first step of the source's proof.

def derivedPushforwardDerivedPullbackTensorIso (f : X ⟶ S) [IsAffineHom f]
    (K : DerivedCategory (_root_.SheafOfModules.{u} (structureSheafRing S.toRingedSpace)))
    (hK : Stacks.DerivedQCoh.IsDQCoh (R := structureSheafRing S.toRingedSpace) K) :
    ((derivedTensorProductFunctor S.toRingedSpace.sheaf).obj
        ((DerivedCategory.singleFunctor
            (_root_.SheafOfModules.{u} (structureSheafRing S.toRingedSpace)) 0).obj
          ((modulePushforward f.toLRSHom.toShHom).obj
            (_root_.SheafOfModules.unit
              (Stacks.SheafOfModules.Tensor.ringSheaf X.toRingedSpace.sheaf))))).obj K ≅
      (derivedPushforward f.toLRSHom.toShHom).obj
        ((derivedPullback f.toLRSHom.toShHom).obj K)

Tag 0AVW, a lemma

Tag 0AVW in the Stacks Project.

Stacks.AlgebraicGeometry.DerivedAffinePushforward.derivedPushforwardOverRingCompRestrictScalarsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedAffineMorphism/DerivedPushforwardOverPushforwardRing.lean, line 352. The attribute's comment: “the factorisation of Rf_ through D(f_𝒪_X); the equivalence clause is proved in isEquivalence_derivedQuasicoherentPushforwardOverRing (QuasicoherentEquivalenceOverPushforwardRing.lean), on the whole derived categories”.

The factorisation asserted by [Stacks, Tag 0AVW]: the derived direct image Rf_* is Φ followed by the functor D(f_* 𝒪_X) ⥤ D(𝒪_S) induced by restriction of scalars along 𝒪_S ⟶ f_* 𝒪_X. Both functors are right derived functors of degreewise direct image, so they agree by the uniqueness of right derived functors.

This is the second of the tag's two clauses, and the attribute carries a phrase naming it. The first clause — that Φ is an equivalence onto D_QCoh(f_* 𝒪_X) for f affine — is isEquivalence_derivedQuasicoherentPushforwardOverRing. The factorisation below holds for every morphism of schemes, with no affineness needed, and is read on the whole derived categories rather than on the quasi-coherent ones, so it is stronger than the source's clause on both counts.

def derivedPushforwardOverRingCompRestrictScalarsIso :
    AlgebraicGeometry.AnyModel.derivedPushforward.{w} f ≅
      derivedPushforwardOverRing.{w} f ⋙ (scalarRestriction f).mapDerivedCategory

Stacks.AlgebraicGeometry.DerivedAffinePushforward.isEquivalence_and_factorisation_derivedQuasicoherentPushforwardOverRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedAffineMorphism/QuasicoherentEquivalenceOverPushforwardRing.lean, line 709.

[Stacks, Tag 0AVW], the whole statement. Let f : X ⟶ S be an affine morphism of schemes. Then direct image induces an equivalence Φ : D_QCoh(𝒪_X) ⥤ D_QCoh(f_* 𝒪_X), and the composition of Φ with the functor D_QCoh(f_* 𝒪_X) ⥤ D_QCoh(𝒪_S) given by restriction of scalars along 𝒪_S ⟶ f_* 𝒪_X is Rf_*.

Both clauses are read on the quasi-coherent subcategories and under the source's condition that f be affine, which is where the tag's own statement puts them; the existing registration on derivedPushforwardOverRingCompRestrictScalarsIso carries the second clause alone, for every morphism of schemes and on the whole derived categories.

theorem isEquivalence_and_factorisation_derivedQuasicoherentPushforwardOverRing :
    (derivedQuasicoherentPushforwardOverRing f).IsEquivalence ∧
      Nonempty (derivedQuasicoherentPushforwardOverRing f ⋙
          derivedQuasicoherentScalarRestriction f ≅
        derivedQuasicoherentPushforwardAtModel f)

Sources

• Section 36.5, Tag 0AVV
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.isIso_pushforwardToRightDerived_of_isAffine · AlgebraicGeometry.reflectsIsomorphisms_derivedQuasicoherentPushforward_specMap · AlgebraicGeometry.reflectsIsomorphisms_derivedQuasicoherentPushforward · Stacks.AlgebraicGeometry.AffinePushforwardTExactness.isIso_of_isIso_derivedPushforward · AlgebraicGeometry.AffineProjectionFormula.isIso_pullbackPushforwardTensorMap_unconditional · Stacks.AlgebraicGeometry.AffinePushforwardTExactness.derivedPushforwardDerivedPullbackTensorIso · Stacks.AlgebraicGeometry.DerivedAffinePushforward.derivedPushforwardPullbackTensorIso · Stacks.AlgebraicGeometry.DerivedAffinePushforward.derivedPushforwardDerivedPullbackTensorIso

Section36.6 Cohomology with support in a closed subset#

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

Tag 08DA, a definition

Tag 08DA in the Stacks Project.

Declarations registered for the tag:

• AlgebraicGeometry.CohomologySupportedOn, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Perfect/SupportedCohomology.lean, line 59 (StacksFrontier).

Tag 0G7G, a lemma

Tag 0G7G in the Stacks Project.

Stacks.Perfect.SupportedQuasicoherent.quasiCoherentSupported_derivedSupportedPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/QuasicoherentSupportedComplexes.lean, line 508. The attribute's comment: “part (1)”.

Stacks 0G7G (1). Let X be a scheme, let T ⊆ X be a closed subset whose open complement X ∖ T is retrocompact, and let i : T → X be the inclusion. For E in D_QCoh(𝒪_X) the complex i_* R𝓗_T(E) lies in D_{QCoh, T}(𝒪_X): its cohomology sheaves are quasi-coherent and supported on T.

theorem quasiCoherentSupported_derivedSupportedPushforward (hTc : IsRetrocompact Tᶜ)
    (E : DerivedCategory (SheafOfModules.{u} (structureSheafRing X.toRingedSpace)))
    (hE : DerivedCategoryB.derivedCategoryB (SheafOfModules.isQuasicoherent X.ringCatSheaf) E) :
    Stacks.Duality.quasiCoherentSupported X T
      ((derivedSupportedPushforward X.toRingedSpace T hT).obj E)

Stacks.Perfect.SupportedQuasicoherent.quasiCoherentSupportedInclusionAdj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/QuasicoherentSupportedComplexes.lean, line 571. The attribute's comment: “part (2)”.

Stacks 0G7G (2). Let X be a scheme, let T ⊆ X be a closed subset whose open complement is retrocompact, and let i : T → X be the inclusion. The functor i_* ∘ R𝓗_T : D_QCoh(𝒪_X) ⥤ D_{QCoh,T}(𝒪_X) is right adjoint to the inclusion functor D_{QCoh,T}(𝒪_X) ⥤ D_QCoh(𝒪_X).

The adjunction is the restriction of the ambient adjunction i_* ⊣ R𝓗_T of Stacks 0A3B along the two fully faithful inclusions: on the left R𝓗_T identifies D_{QCoh,T}(𝒪_X) with a full subcategory of D(𝒪_X|_T), because the counit i_* R𝓗_T(A) ⟶ A is invertible there, and on the right D_QCoh(𝒪_X) is a full subcategory of D(𝒪_X).

def quasiCoherentSupportedInclusionAdj (hTc : IsRetrocompact Tᶜ) :
    quasiCoherentSupportedInclusion X T ⊣ quasiCoherentDerivedSupport X T hT hTc

Tag 0G7H, a lemma

Tag 0G7H in the Stacks Project.

Stacks.Cohomology.SupportedComplexes.preservesColimitsOfShape_discrete_derivedSupportedSectionsOnClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/SupportedSectionsDirectSums.lean, line 317. The attribute's comment: “for families indexed by a type of the scheme universe, the only index universe at which D_QCoh(𝒪_X) has direct sums”.

Let X be a scheme and let T ⊆ X be a closed subset such that X ∖ T is a retrocompact open of X. Then for a family Eᵢ, i ∈ I, of objects of D_QCoh(𝒪_X) we have R𝓗_T(⊕ Eᵢ) = ⊕ R𝓗_T(Eᵢ): the derived functor R𝓗_T of sections supported on T, restricted to D_QCoh(𝒪_X), preserves I-indexed direct sums.

theorem preservesColimitsOfShape_discrete_derivedSupportedSectionsOnClosed
    (hTc : IsRetrocompact (Tᶜ : Set X)) :
    PreservesColimitsOfShape (Discrete I)
      ((quasicoherentDerivedProperty X).ι ⋙
        derivedSupportedSectionsOnClosed X.toRingedSpace T hT)

Tag 0G7I, a remark

Tag 0G7I in the Stacks Project.

AlgebraicGeometry.ExtendedAlternatingCech.equationsClosedSubscheme, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/ExtendedAlternatingCech.lean, line 89. The attribute's comment: “closed subscheme cut out by the equations”.

The closed subscheme cut out by the given equations.

public def equationsClosedSubscheme : Scheme.{u}

AlgebraicGeometry.ExtendedAlternatingCech.equationsOpen, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/ExtendedAlternatingCech.lean, line 94. The attribute's comment: “principal-open intersections”.

The intersection of the principal opens belonging to an increasing tuple.

public def equationsOpen (p : ℕ) (s : CechCochains.OrdIndex (I := Fin c) p) : X.Opens

AlgebraicGeometry.ExtendedAlternatingCech.restrictedModule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/ExtendedAlternatingCech.lean, line 99. The attribute's comment: “direct images of restrictions”.

The direct image to X of a module restricted to a principal intersection.

public def restrictedModule (F : X.Modules) (p : ℕ)
    (s : CechCochains.OrdIndex (I := Fin c) p) : X.Modules

AlgebraicGeometry.ExtendedAlternatingCech.functor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/ExtendedAlternatingCech.lean, line 999. The attribute's comment: “extended alternating Čech complex and signed differentials”.

Stacks Project, Tag 0G7I. The extended alternating Čech complex of a module with respect to finitely many global equations, including its canonical augmentation, signed restriction differentials, and functoriality.

public def functor : FunctorData f

Stacks.Perfect.CechComparison.complexIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/ExtendedAlternatingCechComparison.lean, line 181. The attribute's comment: “the complex is determined by the data specifying it”.

Stacks Project, Tag 0G7I. The two constructions of the extended alternating Čech complex of a family of global equations and a coefficient module are isomorphic: in degree 0 by the two identifications with the coefficient module, and in degree p + 1 by the two identifications with the product of the direct images of its restrictions to the principal intersections.

def complexIso : (data f F).complex ≅ (extendedAlternatingCech f F).complex

Stacks.Perfect.ExtendedAlternatingCech.equationsClosedSubscheme, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/GlobalEquationsComplexData.lean, line 75. The attribute's comment: “closed subscheme cut out by the equations”.

The closed subscheme cut out by the given equations.

public def equationsClosedSubscheme : Scheme.{u}

Stacks.Perfect.ExtendedAlternatingCech.equationsOpen, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/GlobalEquationsComplexData.lean, line 80. The attribute's comment: “principal-open intersections”.

The intersection of the principal opens belonging to an increasing tuple.

public def equationsOpen (p : ℕ) (s : CechCochains.OrdIndex (I := Fin c) p) : X.Opens

Stacks.Perfect.ExtendedAlternatingCech.restrictedModule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/GlobalEquationsComplexData.lean, line 85. The attribute's comment: “direct images of restrictions”.

The direct image to X of a module restricted to a principal intersection.

public def restrictedModule (F : X.Modules) (p : ℕ)
    (s : CechCochains.OrdIndex (I := Fin c) p) : X.Modules

Stacks.Perfect.ExtendedAlternatingCech.extendedAlternatingCechFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/GlobalEquationsComplexData.lean, line 870. The attribute's comment: “extended alternating Čech complex and signed differentials”.

Stacks Project, Tag 0G7I. The extended alternating Čech complex of a module with respect to finitely many global equations, including its canonical augmentation, signed restriction differentials, and functoriality.

public def extendedAlternatingCechFunctor :
    ExtendedAlternatingCechFunctorData f

Tag 0G7K, a lemma

Tag 0G7K in the Stacks Project.

AlgebraicGeometry.ExtendedAlternatingCech.acyclic_on_equationsComplement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/Acyclicity.lean, line 243.

The extended alternating Čech complex is acyclic off the common zero locus of the global equations.

public theorem acyclic_on_equationsComplement
    {X : Scheme.{u}} {c : ℕ} (f : Fin c → Γ(X, ⊤)) (F : X.Modules) :
    (((Scheme.Modules.pullback (⨆ i, X.basicOpen (f i)).ι).mapHomologicalComplex
      (ComplexShape.up ℕ)).obj (data f F).complex).Acyclic

Stacks.Perfect.CechLocalCohomology.cohomologySupportedOn_extendedAlternatingCech, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/CechLocalCohomology.lean, line 162. The attribute's comment: “the cohomology sheaves are supported on the common zero locus”.

Stacks Project, Tag 0G7K, as a support statement. The cohomology sheaves of the extended alternating Čech complex of the equations f₁, …, f_c are supported on their common zero locus: the complex is acyclic on the complement, which is the union of the principal opens of the equations.

This is the hypothesis under which [Stacks, Tag 0AEF] part (2) applies to the complex.

theorem cohomologySupportedOn_extendedAlternatingCech :
    AlgebraicGeometry.CohomologySupportedOn (structureSheafRing X.toRingedSpace)
      (equationsClosedSet f)
      (DerivedCategory.Q.obj ((data f F).complex.extend ComplexShape.embeddingUpNat))

Stacks.Cech.extendedCechComplex_acyclic_restrict_basicOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/Cech/ExtendedAlternatingRingedSpace.lean, line 775.

Stacks 0G7K for an arbitrary ringed space. Let Y be a ringed space, let g 0, …, g (c-1) be global sections of its structure sheaf, let Z be their common zero locus and let F be a sheaf of 𝒪_Y-modules. Then the extended alternating Čech complex of F for the opens Y.basicOpen (g i) restricts to an acyclic complex over Y ∖ Z, which is the open ⨆ i, Y.basicOpen (g i) by Stacks.Cech.coe_iSup_basicOpen.

The proof is Stacks.Cech.sectionComplex_acyclic: over an open contained in one of the Y.basicOpen (g i) the complex of sections is the extended ordered Čech complex of a covering one of whose members is the whole open, hence is contractible by Stacks 0G6T; exactness of a complex of sheaves of modules is checked on stalks, and every point of Y ∖ Z has arbitrarily small neighbourhoods inside some Y.basicOpen (g i).

theorem extendedCechComplex_acyclic_restrict_basicOpen
    (F : OXMod.{u, u} Y) :
    (((restrictModules.{u, u, u} Y (⨆ i, Y.basicOpen (g i))).mapHomologicalComplex
      (ComplexShape.up ℕ)).obj
      (extendedCechComplex (fun i => Y.basicOpen (g i)) F)).Acyclic

Tag 0G7L, a remark

Tag 0G7L in the Stacks Project.

AlgebraicGeometry.ExtendedAlternatingCech.augmentation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/Augmentation.lean, line 59. The attribute's comment: “augmentation”.

The canonical map from the extended alternating Čech complex to its degree-zero module, in the unbounded derived category.

public def augmentation (F : X.Modules) :
    DerivedCategory.Q.obj
        ((data f F).complex.extend ComplexShape.embeddingUpNat) ⟶
      (DerivedCategory.singleFunctor X.Modules 0).obj F

AlgebraicGeometry.ExtendedAlternatingCech.augmentation_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/Augmentation.lean, line 70. The attribute's comment: “augmentation”.

The canonical augmentation is natural in the coefficient module.

public theorem augmentation_natural {F G : X.Modules} (φ : F ⟶ G) :
    DerivedCategory.Q.map
        (HomologicalComplex.extendMap ((functor f).map φ)
          ComplexShape.embeddingUpNat) ≫
      augmentation f G =
      augmentation f F ≫ (DerivedCategory.singleFunctor X.Modules 0).map φ

Stacks.Perfect.ExtendedAlternatingCech.Augmentation.augmentation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/AugmentationDerivedMap.lean, line 97. The attribute's comment: “augmentation”.

Stacks Project, Tag 0G7L. The canonical map from the extended alternating Čech complex to its coefficient module placed in degree 0, in the unbounded derived category.

public def augmentation (F : X.Modules) :
    DerivedCategory.Q.obj
        ((extendedAlternatingCech f F).complex.extend ComplexShape.embeddingUpNat) ⟶
      (DerivedCategory.singleFunctor X.Modules 0).obj F

Stacks.Perfect.ExtendedAlternatingCech.Augmentation.augmentation_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/AugmentationDerivedMap.lean, line 108. The attribute's comment: “augmentation”.

Stacks Project, Tag 0G7L. The canonical augmentation is natural in the coefficient module.

public theorem augmentation_natural {F G : X.Modules} (φ : F ⟶ G) :
    DerivedCategory.Q.map
        (HomologicalComplex.extendMap ((extendedAlternatingCechFunctor f).map φ)
          ComplexShape.embeddingUpNat) ≫
      augmentation f G =
    augmentation f F ≫ (DerivedCategory.singleFunctor X.Modules 0).map φ

Stacks.Perfect.SupportedFraction.cohomologySupportedOn_cech, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/DeterminantChangeOfEquations/Subfamily.lean, line 319. The attribute's comment: “the first assertion of the remark: the cohomology sheaves of 𝓕^• are supported on the common zero locus, hence 𝓕^• is an object of D_Z(𝒪_X). Deduced from Stacks 0G7K, stated at the derived-category spelling the remark's diagram uses, for an arbitrary 𝒪_X-module ℱ”.

The extended alternating Čech complex is supported on the common zero locus. Every cohomology sheaf of 𝓕^• has vanishing stalks outside the common zero locus of the equations, because 𝓕^• restricted to the union of the principal opens is acyclic (Stacks 0G7K).

This is the first assertion of Remark 0G7L, 𝓕^• ∈ D_Z(𝒪_X): CohomologySupportedOn is the property cutting out D_Z(𝒪_X) inside D(𝒪_X), so membership in the supported derived category is this statement, and it is what makes the adjunction of Stacks 0AEF applicable to 𝓕^• in the rest of the remark. The remark deduces it from Stacks 0G7K, whose own carrier is cohomologySupportedOn_extendedAlternatingCech; what is registered here is the deduction, at the derived-category spelling that the remark's diagram and the comparison cechToDerivedSupport below are stated at. No hypothesis beyond the remark's is carried: ℱ is an arbitrary 𝒪_X-module and the equations are arbitrary.

public theorem cohomologySupportedOn_cech :
    AlgebraicGeometry.CohomologySupportedOn (structureSheafRing X.toRingedSpace)
      (equationsClosedSet e)
      (DerivedCategory.Q.obj ((cplx e F).extend ComplexShape.embeddingUpNat))

Stacks.Perfect.SupportedFraction.cechToDerivedSupport, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/DeterminantChangeOfEquations/Subfamily.lean, line 400. The attribute's comment: “the canonical comparison 𝓕^• ⟶ i_*RℋT(ℱ), built from the counit of Stacks 0G72 and the augmentation, for an arbitrary 𝒪_X-module ℱ”.

The canonical comparison of Stacks 0G7L, 𝓕^• ⟶ i_* R𝓗_T(ℱ).

It is the inverse of the counit i_* R𝓗_T(𝓕^•) ⟶ 𝓕^•, invertible by isIso_derivedSupportedSectionsToId_cech, followed by i_* R𝓗_T applied to the augmentation 𝓕^• ⟶ ℱ[0] of Stacks 0G7L. This is the map whose degree-c cohomology sheaf Stacks 0G7Q uses to define c_{f₁,…,f_c}.

As in the source, ℱ is an arbitrary 𝒪_X-module: the counit is invertible at 𝓕^• because 𝓕^• is supported on the common zero locus of the equations, which is Stacks 0G7K and holds for every ℱ. Quasi-coherence enters only later, in Stacks 0G7M, where the other leg of the triangle — i_* R𝓗_T applied to the augmentation — is shown to be invertible.

public def cechToDerivedSupport (hTe : equationsClosedSet e ⊆ T) :
    DerivedCategory.Q.obj ((cplx e F).extend ComplexShape.embeddingUpNat) ⟶
      (supportPush hT).obj ((DerivedCategory.singleFunctor X.Modules 0).obj F)

Stacks.Perfect.SupportedFraction.cechToDerivedSupport_comp_derivedSupportedSectionsToId, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/DeterminantChangeOfEquations/Subfamily.lean, line 433. The attribute's comment: “the commuting triangle 𝓕^• ⟶ ℱ, 𝓕^• ⟶ i_RℋT(ℱ), i_RℋT(ℱ) ⟶ ℱ of the remark's diagram, for an arbitrary 𝒪_X-module ℱ”.

The commuting triangle of Stacks 0G7L, in the shape the remark displays:

𝓕^• ⟶ ℱ, 𝓕^• ⟶ i_* R𝓗_T(ℱ) and i_* R𝓗_T(ℱ) ⟶ ℱ

commute, the third edge being the counit of Stacks 0G72 at ℱ[0]. So the canonical map 𝓕^• ⟶ ℱ of the remark — the augmentation, coming from the equality 𝓕^0 = ℱ — factors through i_* R𝓗_T(ℱ), which is what the adjunction of Stacks 0A3B provides and what the remark asserts.

public theorem cechToDerivedSupport_comp_derivedSupportedSectionsToId
    (hTe : equationsClosedSet e ⊆ T) :
    cechToDerivedSupport e F hT hTe ≫
        (supportPushCounit hT).app ((DerivedCategory.singleFunctor X.Modules 0).obj F) =
      augmentation e F

Stacks.Perfect.CechComparison.augmentation_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/ExtendedAlternatingCechComparison.lean, line 238. The attribute's comment: “the augmentations of the two constructions agree”.

Stacks Project, Tag 0G7L. The augmentations of the two constructions of the extended alternating Čech complex correspond under the comparison isomorphism.

theorem augmentation_eq :
    AlgebraicGeometry.ExtendedAlternatingCech.augmentation f F =
      DerivedCategory.Q.map (extendBridge f F).hom ≫
        Stacks.Perfect.ExtendedAlternatingCech.Augmentation.augmentation f F

Stacks.Perfect.SupportedFraction.derivedSupportedSectionsToId_single_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/SupportedFractionNaturality.lean, line 154. The attribute's comment: “functoriality in the 𝒪_X-module ℱ, the edge i_*RℋT(ℱ) ⟶ ℱ of the diagram”.

The edge i_* R𝓗_T(ℱ) ⟶ ℱ of the diagram of Stacks 0G7L is natural in the coefficient module. It is the counit of Stacks 0G72 evaluated at ℱ[0], hence a component of a natural transformation, so its naturality square is NatTrans.naturality; it is stated here because the remark asserts its diagram functorial in ℱ, and that assertion is the naturality of all three edges.

public theorem derivedSupportedSectionsToId_single_naturality {T : Set X} (hT : IsClosed T)
    {F G : X.Modules} (φ : F ⟶ G) :
    (supportPush hT).map ((DerivedCategory.singleFunctor X.Modules 0).map φ) ≫
        (supportPushCounit hT).app ((DerivedCategory.singleFunctor X.Modules 0).obj G) =
      (supportPushCounit hT).app ((DerivedCategory.singleFunctor X.Modules 0).obj F) ≫
        (DerivedCategory.singleFunctor X.Modules 0).map φ

Stacks.Perfect.SupportedFraction.Q_map_extendMap_cplxMap_comp_cechToDerivedSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/SupportedFractionNaturality.lean, line 175. The attribute's comment: “functoriality in the 𝒪_X-module ℱ, the edge 𝓕^• ⟶ i_*RℋT(ℱ) of the diagram”.

The canonical comparison 𝓕^• ⟶ i_* R𝓗_T(ℱ) of Stacks 0G7L is natural in the coefficient module. Both sides become, after the invertible counit of Stacks 0G72, the functor i_* R𝓗_T applied to a naturality square for the augmentation.

This is the second of the three edges of the remark's diagram; with Q_map_extendMap_cplxMap_comp_augmentation for the edge 𝓕^• ⟶ ℱ and derivedSupportedSectionsToId_single_naturality for the edge i_* R𝓗_T(ℱ) ⟶ ℱ it is the remark's closing clause, that the diagram is "functorial in the 𝒪_X-module ℱ".

As in the source, φ is a morphism of arbitrary 𝒪_X-modules: quasi-coherence is nowhere used, the counit being invertible at the extended alternating Čech complex of any module by Stacks 0G7K.

public theorem Q_map_extendMap_cplxMap_comp_cechToDerivedSupport {m : ℕ} (e : Fin m → Γ(X, ⊤))
    {F G : X.Modules} (φ : F ⟶ G) {T : Set X}
    (hT : IsClosed T) (hTe : equationsClosedSet e ⊆ T) :
    DerivedCategory.Q.map (HomologicalComplex.extendMap (cplxMap e φ)
          ComplexShape.embeddingUpNat) ≫ cechToDerivedSupport e G hT hTe =
      cechToDerivedSupport e F hT hTe ≫
        (supportPush hT).map ((DerivedCategory.singleFunctor X.Modules 0).map φ)

Stacks.Cohomology.SupportedComplexes.derivedSupportedSectionsLift, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/SupportedSectionsCanonicalMaps.lean, line 498. The attribute's comment: “the canonical factorisation through derived supported sections”.

The canonical factorization of Stacks 0G7L. A map i_* L ⟶ K in D(𝒪_X) out of a complex pushed forward from Z has a canonical lift L ⟶ RH_Z(K), its adjoint transpose under derivedPushforwardAdjunction. Pushing the lift forward and composing with the counit i_* RH_Z(K) ⟶ K returns the original map, by modulePushforward_map_derivedSupportedSectionsLift_comp_counit: this is the commutative triangle of Stacks 0G7L, for the chosen adjunction.

noncomputable def derivedSupportedSectionsLift
    {L : DerivedCategory (_root_.SheafOfModules.{u}
      (structureSheafRing (closedSubsetRingedSpace X Z)))}
    {K : DerivedCategory (_root_.SheafOfModules.{u} (structureSheafRing X))}
    (u : letI := pushforward_preservesFiniteLimits X Z
      letI := pushforward_preservesFiniteColimits X Z hZ
      (modulePushforward (closedSubsetInclusion X Z)).mapDerivedCategory.obj L ⟶ K) :
    L ⟶ (derivedSupportedSectionsOnClosed X Z hZ).obj K

Stacks.Cohomology.SupportedComplexes.modulePushforward_map_derivedSupportedSectionsLift_comp_counit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/SupportedSectionsCanonicalMaps.lean, line 513. The attribute's comment: “the commuting triangle of the factorisation”.

The triangle of Stacks 0G7L commutes. The canonical lift of u : i_* L ⟶ K through i_* RH_Z(K), pushed forward and followed by the counit of the adjunction, is u again.

theorem modulePushforward_map_derivedSupportedSectionsLift_comp_counit
    {L : DerivedCategory (_root_.SheafOfModules.{u}
      (structureSheafRing (closedSubsetRingedSpace X Z)))}
    {K : DerivedCategory (_root_.SheafOfModules.{u} (structureSheafRing X))}
    (u : letI := pushforward_preservesFiniteLimits X Z
      letI := pushforward_preservesFiniteColimits X Z hZ
      (modulePushforward (closedSubsetInclusion X Z)).mapDerivedCategory.obj L ⟶ K) :
    letI := pushforward_preservesFiniteLimits X Z
    letI := pushforward_preservesFiniteColimits X Z hZ
    (modulePushforward (closedSubsetInclusion X Z)).mapDerivedCategory.map
          (derivedSupportedSectionsLift X Z hZ u) ≫
        (derivedPushforwardAdjunction X Z hZ).counit.app K = u

Tag 0G7M, a lemma

Tag 0G7M in the Stacks Project.

Stacks.Perfect.CechLocalCohomology.pushforwardLocalCohomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/CechLocalCohomology.lean, line 196. The attribute's comment: “the complex computes the local cohomology sheaves”.

The extended alternating Čech complex computes the local cohomology sheaves. For a quasi-coherent 𝒪_X-module F and the common zero locus Z of the equations, the direct image of the local cohomology sheaf 𝓗 ⁿ_Z(F) along the inclusion of Z is the degree-n cohomology sheaf of the extended alternating Čech complex of F.

In the top degree the right-hand side is the cokernel of the last Čech differential, the module in which the fraction class of [Stacks, Tag 0G7Q] takes its values.

def pushforwardLocalCohomologyIso [F.IsQuasicoherent] (n : ℕ) :
    letI := pushforward_preservesFiniteLimits X.toRingedSpace (equationsClosedSet f)
    letI := pushforward_preservesFiniteColimits X.toRingedSpace (equationsClosedSet f)
      (isClosed_equationsClosedSet f)
    (modulePushforward (closedSubsetInclusion X.toRingedSpace (equationsClosedSet f))).obj
        (localCohomologySheafOfComplex X.toRingedSpace (equationsClosedSet f)
          (isClosed_equationsClosedSet f) (n : ℤ)
          ((DerivedCategory.singleFunctor X.Modules 0).obj F)) ≅
      (data f F).complex.homology n

Stacks.Perfect.CechDerivedSupport.isIso_map_augmentation_of_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/DerivedSupportInvertsAugmentation.lean, line 357. The attribute's comment: “the derived sections with support invert the augmentation”.

Stacks Project, Tag 0G7M, the step of the proof that uses the quasi-coherence of the coefficient module. With X, f₁, …, f_c ∈ Γ(X, 𝒪_X) and F as in Stacks 0G7I, and F quasi-coherent, a derived functor R𝓗_Z of sections supported on the common zero locus Z of the equations inverts the augmentation 𝓕^• ⟶ F[0] of Stacks 0G7L.

The augmentation is the comparison between the extended alternating Čech complex and its coefficient module, so this says that the complex and the module have the same derived sections with support on Z.

public theorem isIso_map_augmentation_of_isQuasicoherent (F : X.Modules) [F.IsQuasicoherent]
    (RH : DerivedCategory X.Modules ⥤
      DerivedCategory (SheafOfModules.{u}
        (structureSheafRing (closedSubsetRingedSpace X.toRingedSpace (equationsClosedSet f)))))
    (αH : (schemeSupportedSectionsFunctor X (equationsClosedSet f)
        (isClosed_equationsClosedSet f)).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ RH)
    (hRH : RH.IsRightDerivedFunctor αH
      (HomotopyCategory.quasiIso X.Modules (ComplexShape.up ℤ))) :
    IsIso (RH.map (Stacks.Perfect.ExtendedAlternatingCech.Augmentation.augmentation f F))

Stacks.Perfect.CechDerivedSupport.nonempty_cechIso_derivedSupportedSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/DerivedSupportInvertsAugmentation.lean, line 407. The attribute's comment: “the extended alternating Čech complex represents i_*RℋZ(F)”.

Stacks Project, Tag 0G7M. With X, f₁, …, f_c ∈ Γ(X, 𝒪_X) and F as in Stacks 0G7I and F quasi-coherent, the extended alternating Čech complex 𝓕^• represents i_* R𝓗_Z(F), the comparison being the augmentation 𝓕^• ⟶ F[0] of Stacks 0G7L.

Two halves combine. The augmentation is inverted by R𝓗_Z, which is isIso_derivedSupportedSectionsOnClosed_map_augmentation and is where quasi-coherence is used; and 𝓕^• is its own derived sections with support, which is Stacks.Perfect.CechSupportRepresentation.nonempty_pushforwardDerivedSupportCechIso and is where the acyclicity of Stacks 0G7K is used. The K-injective resolution entering the second half is not canonical, so the conclusion is stated as the existence of the isomorphism, in the form the neighbouring existence statements of Stacks 0A3B take.

public theorem nonempty_cechIso_derivedSupportedSections (F : X.Modules) [F.IsQuasicoherent] :
    letI := pushforward_preservesFiniteLimits X.toRingedSpace (equationsClosedSet f)
    letI := pushforward_preservesFiniteColimits X.toRingedSpace (equationsClosedSet f)
      (isClosed_equationsClosedSet f)
    Nonempty
      (DerivedCategory.Q.obj
          ((Stacks.Perfect.ExtendedAlternatingCech.extendedAlternatingCech f F).complex.extend
            ComplexShape.embeddingUpNat) ≅
        (modulePushforward (closedSubsetInclusion X.toRingedSpace
            (equationsClosedSet f))).mapDerivedCategory.obj
          ((derivedSupportedSectionsOnClosed X.toRingedSpace (equationsClosedSet f)
              (isClosed_equationsClosedSet f)).obj
            ((DerivedCategory.singleFunctor X.Modules 0).obj F)))

Stacks.Perfect.SupportedFraction.isIso_derivedSupportedSectionsToId_cech, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/DeterminantChangeOfEquations/Subfamily.lean, line 381. The attribute's comment: “the canonical counit i_*RℋT(𝓕^•) ⟶ 𝓕^• of Stacks 0G72 is invertible at the extended alternating Čech complex, for every closed T containing the common zero locus of the equations. The theorem nonempty_pushforwardDerivedSupportCechIso asserts the same isomorphism without naming it, because it is produced on a chosen K-injective resolution; here only invertibility of the canonical map is asserted, and invertibility is a proposition, so nothing is chosen”.

Stacks 0G7M, the acyclicity half, with the comparison as a canonical term. The counit i_* R𝓗_T(𝓕^•) ⟶ 𝓕^• of Stacks 0G72 is invertible at the extended alternating Čech complex of a family of equations whose common zero locus is contained in T: the complex is supported there, so the third vertex Rj_*(𝓕^•|_U) of the triangle vanishes.

This is the content of nonempty_pushforwardDerivedSupportCechIso, with the isomorphism being the canonical map rather than one produced on a chosen K-injective resolution; only the invertibility is asserted, and invertibility is a proposition, so nothing is chosen.

public theorem isIso_derivedSupportedSectionsToId_cech (hTe : equationsClosedSet e ⊆ T) :
    IsIso ((supportPushCounit hT).app
      (DerivedCategory.Q.obj ((cplx e F).extend ComplexShape.embeddingUpNat)))

Stacks.Perfect.CechComparison.isIso_derivedSupportedSectionsOnClosed_map_augmentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/ExtendedAlternatingCechComparison.lean, line 261. The attribute's comment: “the derived sections with support invert the augmentation”.

Stacks Project, Tag 0G7M. With X a scheme, f₁, …, f_c ∈ Γ(X, 𝒪_X) global functions, Z their common zero locus and F a quasi-coherent 𝒪_X-module, the chosen derived functor of sections supported on Z inverts the augmentation of AlgebraicGeometry.ExtendedAlternatingCech.data.

This is Stacks.Perfect.CechDerivedSupport.isIso_derivedSupportedSectionsOnClosed_map_augmentation for the construction of the complex on which [Stacks, Tag 0G7K] and the well-definedness of the fraction class of [Stacks, Tag 0G7Q] are stated.

theorem isIso_derivedSupportedSectionsOnClosed_map_augmentation [F.IsQuasicoherent] :
    IsIso ((Stacks.Cohomology.SupportedComplexes.derivedSupportedSectionsOnClosed
      X.toRingedSpace (Stacks.Perfect.CechDerivedSupport.equationsClosedSet f)
      (Stacks.Perfect.CechDerivedSupport.isClosed_equationsClosedSet f)).map
        (AlgebraicGeometry.ExtendedAlternatingCech.augmentation f F))

Tag 0G7N, a lemma

Tag 0G7N in the Stacks Project.

Stacks.Perfect.LocalCohomologyDegrees.isZero_homology_derivedSupportedSections_of_locallyCutOut, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/LocalCohomologyVanishingDegrees.lean, line 119. The attribute's comment: “stated for the closed subset T; the source writes ℋ^i_Z for it, a slip”.

Stacks Project, Tag 0G7N. Let X be a scheme and let T ⊆ X be a closed subset which can locally be cut out by c elements of the structure sheaf. Then the local cohomology sheaves of a quasi-coherent 𝒪_X-module vanish above degree c:

ℋ ^i_T(ℱ) = 0 for i > c.

The hypothesis is that every point has an open neighbourhood U on which the part of T lying in U is the common zero locus of c functions on U.

public theorem isZero_homology_derivedSupportedSections_of_locallyCutOut {X : Scheme.{u}}
    (T : Set X) (hT : IsClosed T) (c : ℕ)
    (hcut : ∀ x : X, ∃ U : X.Opens, x ∈ U ∧ ∃ f : Fin c → Γ(U.toScheme, ⊤),
      U.ι ⁻¹' T = Stacks.Perfect.CechDerivedSupport.equationsClosedSet f)
    (F : X.Modules) [F.IsQuasicoherent] (i : ℤ) (hi : (c : ℤ) < i) :
    IsZero ((DerivedCategory.homologyFunctor
        (SheafOfModules.{u} (structureSheafRing (closedSubsetRingedSpace X.toRingedSpace T))) i).obj
      ((derivedSupportedSectionsOnClosed X.toRingedSpace T hT).obj
        ((DerivedCategory.singleFunctor X.Modules 0).obj F)))

Tag 0G7P, a lemma

Tag 0G7P in the Stacks Project.

Stacks.Perfect.LocalCohomologyDegrees.isZero_homology_derivedSupportedSections_of_locallyKoszulRegular_of_ne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/KoszulFlatVanishingLocal.lean, line 250. The attribute's comment: “the whole statement: for a closed subset locally cut out by a Koszul-regular sequence of c elements and a flat quasi-coherent module, the vanishing of the local cohomology sheaf in every degree other than c; exactly the source's conditions, with locally read over affine open neighbourhoods, which Stacks 063G shows is the same condition”.

Stacks Project, Tag 0G7P. Let X be a scheme. Let Z ⊆ X be a closed subset which can locally be cut out by a Koszul-regular sequence having c elements. Then

ℋ ^i_Z(ℱ) = 0 for i ≠ c

for every flat, quasi-coherent 𝒪_X-module ℱ.

Above degree c this is Stacks 0G7N, which needs neither the Koszul-regularity of the equations nor the flatness of ℱ (isZero_homology_derivedSupportedSections_of_locallyKoszulRegular); below degree c it needs both and is isZero_homology_derivedSupportedSections_of_locallyKoszulRegular_of_lt.

"Locally" is read with affine open neighbourhoods, which by Stacks 063G is the same condition as the source's; see the implementation notes of this file.

public theorem isZero_homology_derivedSupportedSections_of_locallyKoszulRegular_of_ne
    {X : Scheme.{u}} (Z : Set X) (hZ : IsClosed Z) (c : ℕ)
    (hcut : ∀ x : X, ∃ U : X.Opens, x ∈ U ∧ IsAffineOpen U ∧
      ∃ f : Fin c → Γ(U.toScheme, ⊤), Koszul.IsKoszulRegular f ∧
        U.ι ⁻¹' Z = equationsClosedSet f)
    (F : X.Modules) [F.IsQuasicoherent]
    (hflat : AlgebraicGeometry.SheafOfModules.IsFlat
      (C := TopologicalSpace.Opens X.toTopCat)
      (J := Opens.grothendieckTopology X.toTopCat) (O := X.sheaf) F)
    (i : ℤ) (hi : i ≠ (c : ℤ)) :
    IsZero ((DerivedCategory.homologyFunctor
        (SheafOfModules.{u} (structureSheafRing (closedSubsetRingedSpace X.toRingedSpace Z))) i).obj
      ((derivedSupportedSectionsOnClosed X.toRingedSpace Z hZ).obj
        ((DerivedCategory.singleFunctor X.Modules 0).obj F)))

Tag 0G7Q, a remark

Tag 0G7Q in the Stacks Project.

Stacks.Perfect.GysinLocalCohomology.fractionClassOnClosed, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/Gysin/GysinDifferentialCompatibility.lean, line 194. The attribute's comment: “the remark's conclusion: the canonical O_X|_Z-linear map c_{f₁,…,f_c} : i^ℱ ⟶ ℋ^c_Z(ℱ) on Z, together with its functoriality in the 𝒪_X-module ℱ, as a natural transformation of the two functors of ℱ into 𝒪_X|_Z-modules; obtained from the transformation on X by the remark's last step, the transposition along i^ ⊣ i_ that full faithfulness of i_ provides”.

With X a scheme, f₁, …, f_c ∈ Γ(X, 𝒪_X) and Z ⊆ X the closed subscheme they cut out, the canonical map c_{f₁, …, f_c} : i^*ℱ ⟶ ℋ^c_Z(ℱ) of 𝒪_X|_Z-modules on Z, as a natural transformation of functors of the 𝒪_X-module ℱ: from ℱ ↦ i^*(ℱ/(f₁, …, f_c)ℱ), the inverse image along the inclusion of Z of the cokernel of (f₁, …, f_c) : ℱ^{⊕c} ⟶ ℱ, to ℱ ↦ ℋ^c_Z(ℱ). Its component at ℱ is the transpose under i^* ⊣ i_* of the component of fractionClassPushTrans.

public def fractionClassOnClosed {d : ℕ} (f : Fin (d + 1) → Γ(X, ⊤)) :
    equationsQuotientFunctor f ⋙
        modulePullback (closedSubsetInclusion X.toRingedSpace (equationsClosedSet f)) ⟶
      DerivedCategory.singleFunctor X.Modules 0 ⋙
        derivedSupportedSectionsOnClosed X.toRingedSpace (equationsClosedSet f)
            (isClosed_equationsClosedSet f) ⋙
          DerivedCategory.homologyFunctor _ ((d + 1 : ℕ) : ℤ)

AlgebraicGeometry.ExtendedAlternatingCech.eq_of_eq_mod_equations_empty, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/FractionClass.lean, line 312. The attribute's comment: “fraction_class_well_defined”.

For no equations, the fraction is just the numerator itself, and the quotient by the zero ideal changes nothing.

public lemma eq_of_eq_mod_equations_empty
    {X : Scheme.{u}} (f : Fin 0 → Γ(X, ⊤)) (F : X.Modules) (V : X.Opens)
    (s t : Γ(F, V))
    (x y : Γ((data f F).complex.X 0, V))
    (hmod : s - t = ∑ i : Fin 0,
      (X.presheaf.map (homOfLE le_top : V ⟶ ⊤).op (f i)) •
        (0 : Γ(F, V)))
    (hx : ((data f F).zeroIso.hom).app V x = s)
    (hy : ((data f F).zeroIso.hom).app V y = t) :
    x = y

AlgebraicGeometry.ExtendedAlternatingCech.cokernel_π_app_eq_of_eq_mod_equations, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/FractionClass.lean, line 526. The attribute's comment: “fraction_class_well_defined”.

Fractions with congruent numerators have the same class in the final Čech cokernel.

public lemma cokernel_π_app_eq_of_eq_mod_equations
    {X : Scheme.{u}} {c : ℕ} {ι : Type*} (f : Fin (c + 1) → Γ(X, ⊤))
    (F : X.Modules) (V : X.Opens) (U : ι → X.Opens)
    (hU : ∀ i, U i ≤ V) (hcover : ⨆ i, U i = V)
    (s t : Γ(F, V))
    (x y : Γ((data f F).complex.X (c + 1), V))
    (a : ∀ j : ι, Fin (c + 1) → Γ(F, U j))
    (hmod : ∀ j,
      (Scheme.Modules.presheaf F).map (homOfLE (hU j)).op (s - t) =
        ∑ i, (X.presheaf.map (homOfLE le_top : U j ⟶ ⊤).op (f i)) • a j i)
    (hx : ∀ q : CechCochains.OrdIndex (I := Fin (c + 1)) c,
      (X.presheaf.map (homOfLE le_top :
        CechCochains.inter (fun i => V ⊓ X.basicOpen (f i)) q.1 ⟶ ⊤).op
        (∏ i, f i)) •
        ((data f F).sectionsIso c V x q) =
      (Scheme.Modules.presheaf F).map
        (homOfLE (show
          CechCochains.inter (fun i => V ⊓ X.basicOpen (f i)) q.1 ≤ V from
            (iInf_le _ (0 : Fin (c + 1))).trans inf_le_left)).op s)
    (hy : ∀ q : CechCochains.OrdIndex (I := Fin (c + 1)) c,
      (X.presheaf.map (homOfLE le_top :
        CechCochains.inter (fun i => V ⊓ X.basicOpen (f i)) q.1 ⟶ ⊤).op
        (∏ i, f i)) •
        ((data f F).sectionsIso c V y q) =
      (Scheme.Modules.presheaf F).map
        (homOfLE (show
          CechCochains.inter (fun i => V ⊓ X.basicOpen (f i)) q.1 ≤ V from
            (iInf_le _ (0 : Fin (c + 1))).trans inf_le_left)).op t) :
    (cokernel.π ((data f F).complex.d c (c + 1))).app V x =
      (cokernel.π ((data f F).complex.d c (c + 1))).app V y

Stacks.Perfect.FractionClass.classMapToPushforward_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/FractionClassAnyModule.lean, line 197. The attribute's comment: “functoriality in the 𝒪_X-module ℱ, with the direct image taken outside the cohomology sheaf, for an arbitrary 𝒪_X-module and any number of equations”.

Stacks Project, Tag 0G7Q, functoriality in ℱ, in the spelling of i_*ℋ ᶜ_T(ℱ) with the direct image outside: classMapToSupport_natural, with its carried numerator hypothesis discharged by fracTermTop_naturality, carried across the comparison of the two spellings, which is natural.

public theorem classMapToPushforward_natural {c : ℕ} (f : Fin c → Γ(X, ⊤)) {F G : X.Modules}
    (φ : F ⟶ G) {T : Set X} (hT : IsClosed T) (hTf : equationsClosedSet f ⊆ T) :
    φ ≫ classMapToPushforward f G hT hTf =
      classMapToPushforward f F hT hTf ≫ (localCohomologyPushforwardFunctor hT (c : ℤ)).map φ

Stacks.Perfect.FractionClass.quotientClassMapToPushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/FractionClassAnyModule.lean, line 274. The attribute's comment: “i_* of the remark's map c_{f₁,…,f_c}, between its two presentations, for an arbitrary 𝒪_X-module ℱ and any number of equations”.

Stacks Project, Tag 0G7Q, for an arbitrary 𝒪_X-module. The 𝒪_X-module map

i_*i^*ℱ = ℱ/(f₁, …, f_c)ℱ ⟶ i_*ℋ ᶜ_T(ℱ)

carrying the class of a local section s of ℱ to the class of the fraction s / (f₁ ⋯ f_c). The remark builds exactly this map and then descends it along the fully faithful i_*; here the descent is fractionClassAnyModule.

No quasi-coherence and no hypothesis on the number of equations: the class of the fraction lands in the degree-c cohomology sheaf of the extended alternating Čech complex, which the comparison of [Stacks, Tag 0G7L] carries into i_*ℋ ᶜ_T(ℱ) for every 𝒪_X-module ℱ.

public def quotientClassMapToPushforward {c : ℕ} (f : Fin c → Γ(X, ⊤)) (F : X.Modules)
    {T : Set X} (hT : IsClosed T) (hTf : equationsClosedSet f ⊆ T) :
    equationsQuotient f F ⟶ (localCohomologyPushforwardFunctor hT (c : ℤ)).obj F

Stacks.Perfect.FractionClass.cokernelπ_comp_quotientClassMapToPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/FractionClassAnyModule.lean, line 284. The attribute's comment: “the value on the class of a local section is the class of its fraction, for an arbitrary 𝒪_X-module ℱ”.

Stacks Project, Tag 0G7Q. The map out of the quotient sends the class of a local section s of ℱ to the class of the fraction s / (f₁ ⋯ f_c).

public theorem cokernelπ_comp_quotientClassMapToPushforward {c : ℕ} (f : Fin c → Γ(X, ⊤))
    (F : X.Modules) {T : Set X} (hT : IsClosed T) (hTf : equationsClosedSet f ⊆ T) :
    cokernel.π (equationsMap f F) ≫ quotientClassMapToPushforward f F hT hTf =
      classMapToPushforward f F hT hTf

Stacks.Perfect.FractionClass.quotientClassMapToPushforward_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/FractionClassAnyModule.lean, line 298. The attribute's comment: “functoriality in the 𝒪_X-module ℱ of i_* of the remark's map, for an arbitrary 𝒪_X-module ℱ and any number of equations”.

Stacks Project, Tag 0G7Q, functoriality in ℱ of the map out of the quotient. The square commutes for every morphism φ : ℱ ⟶ 𝒢 of 𝒪_X-modules, the left vertical arrow being i_*i^*φ in the presentation equationsQuotientMap.

The projection onto the quotient is an epimorphism, so this is classMapToPushforward_natural.

public theorem quotientClassMapToPushforward_natural {c : ℕ} (f : Fin c → Γ(X, ⊤))
    {F G : X.Modules} (φ : F ⟶ G) {T : Set X} (hT : IsClosed T)
    (hTf : equationsClosedSet f ⊆ T) :
    equationsQuotientMap f φ ≫ quotientClassMapToPushforward f G hT hTf =
      quotientClassMapToPushforward f F hT hTf ≫
        (localCohomologyPushforwardFunctor hT (c : ℤ)).map φ

Stacks.Perfect.FractionClass.fractionClassAnyModule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/FractionClassAnyModule.lean, line 332. The attribute's comment: “the canonical map c_{f_1, …, f_c}, for an arbitrary 𝒪_X-module ℱ and any number of equations”.

Stacks Project, Tag 0G7Q, for every 𝒪_X-module. The canonical 𝒪_X|_T-linear map

c_{f₁, …, f_c} : i^*(ℱ/(f₁, …, f_c)ℱ) ⟶ ℋ ᶜ_T(ℱ)

on a closed subset T containing the common zero locus of f₁, …, f_c, for an arbitrary 𝒪_X-module ℱ and an arbitrary number of equations. It is the transpose, under the adjunction i^* ⊣ i_* between inverse image and direct image along the inclusion of T, of the map quotientClassMapToPushforward carrying the class of a local section s of ℱ to the class of the fraction s / (f₁ ⋯ f_c).

This is the remark's own construction: the 𝒪_X-module map i_*i^*ℱ ⟶ i_*ℋ ᶜ_T(ℱ) followed by the descent along i_*. Only the comparison of [Stacks, Tag 0G7L] is used, and that holds for every 𝒪_X-module; Stacks.Perfect.FractionClass.fractionClass is this map on a quasi-coherent module, by fractionClassAnyModule_eq.

public def fractionClassAnyModule {c : ℕ} (f : Fin c → Γ(X, ⊤)) (F : X.Modules) {T : Set X}
    (hT : IsClosed T) (hTf : equationsClosedSet f ⊆ T) :
    (modulePullback (closedSubsetInclusion X.toRingedSpace T)).obj (equationsQuotient f F) ⟶
      localCohomologySheafOfComplex X.toRingedSpace T hT (c : ℤ)
        ((DerivedCategory.singleFunctor X.Modules 0).obj F)

Stacks.Perfect.FractionClass.homEquiv_fractionClassAnyModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/FractionClassAnyModule.lean, line 344. The attribute's comment: “c_{f_1, …, f_c} is the transpose of the map out of the quotient, for an arbitrary 𝒪_X-module ℱ”.

Stacks Project, Tag 0G7Q. The map c_{f₁, …, f_c} is the transpose of the map i_*i^*ℱ ⟶ i_*ℋ ᶜ_T(ℱ) out of the quotient by the equations.

public theorem homEquiv_fractionClassAnyModule {c : ℕ} (f : Fin c → Γ(X, ⊤)) (F : X.Modules)
    {T : Set X} (hT : IsClosed T) (hTf : equationsClosedSet f ⊆ T) :
    homEquiv (closedSubsetInclusion X.toRingedSpace T) _ (equationsQuotient f F)
        (fractionClassAnyModule f F hT hTf) =
      quotientClassMapToPushforward f F hT hTf

Stacks.Perfect.FractionClass.fractionClassAnyModule_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/FractionClassAnyModule.lean, line 364. The attribute's comment: “functoriality in the 𝒪_X-module ℱ of c_{f_1, …, f_c} itself, for an arbitrary 𝒪_X-module ℱ and any number of equations”.

Stacks Project, Tag 0G7Q, functoriality in ℱ of c_{f₁, …, f_c} itself. For every morphism φ : ℱ ⟶ 𝒢 of 𝒪_X-modules the square

i^*(ℱ/(f)ℱ) ⟶ ℋ ᶜ_T(ℱ), i^*(𝒢/(f)𝒢) ⟶ ℋ ᶜ_T(𝒢)

commutes, the vertical arrows being i^* of equationsQuotientMap and ℋ ᶜ_T(φ). This is the functoriality the remark asserts, read on c_{f₁, …, f_c} rather than on its direct image.

It is quotientClassMapToPushforward_natural transposed: both sides become maps out of ℱ/(f)ℱ under the bijection of the adjunction i^* ⊣ i_*, by its naturality in each variable, and there the square is the one already proved.

public theorem fractionClassAnyModule_natural {c : ℕ} (f : Fin c → Γ(X, ⊤)) {F G : X.Modules}
    (φ : F ⟶ G) {T : Set X} (hT : IsClosed T) (hTf : equationsClosedSet f ⊆ T) :
    (modulePullback (closedSubsetInclusion X.toRingedSpace T)).map (equationsQuotientMap f φ) ≫
        fractionClassAnyModule f G hT hTf =
      fractionClassAnyModule f F hT hTf ≫
        (localCohomologySheafOfComplexFunctor X.toRingedSpace T hT (c : ℤ)).map φ

Stacks.Perfect.FractionClass.fractionClassAnyModule_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/FractionClassAnyModule.lean, line 419. The attribute's comment: “the quasi-coherent construction of c_{f_1, …, f_c} is the arbitrary-module one specialised”.

Stacks Project, Tag 0G7Q: the quasi-coherent construction is this one specialised. On a quasi-coherent 𝒪_X-module the map c_{f₁, …, f_c} built here through [Stacks, Tag 0G7L] alone is Stacks.Perfect.FractionClass.fractionClass, which is built through [Stacks, Tag 0G7M]. Both are transposes along i^* ⊣ i_*, and their transposes agree by quotientClassMapToPushforward_eq.

public theorem fractionClassAnyModule_eq {c : ℕ} (f : Fin c → Γ(X, ⊤)) (F : X.Modules)
    [F.IsQuasicoherent] :
    fractionClassAnyModule f F (isClosed_equationsClosedSet f) subset_rfl = fractionClass f F

Stacks.Perfect.FractionClass.smulHom_comp_classMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/FractionClassMap.lean, line 526. The attribute's comment: “the class of the fraction depends only on the numerator modulo the equations”.

The fraction class only depends on the numerator modulo the equations. Multiplying the numerator by one of the equations kills the class of the fraction, because the result is the image of a cochain under the last Čech differential. An equation to multiply by is itself a witness that there is at least one, which is what the descent of the product needs.

public theorem smulHom_comp_classMap (j : Fin c) :
    smulHom (f j) F ≫ classMap f F = 0

Stacks.Perfect.FractionClass.cokernelπ_comp_quotientClassMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/FractionClassMap.lean, line 564. The attribute's comment: “the value on the class of a local section is the class of its fraction”.

The map out of the quotient sends the class of a section to the class of its fraction.

public theorem cokernelπ_comp_quotientClassMap :
    cokernel.π (equationsMap f F) ≫ quotientClassMap f F = classMap f F

Stacks.Perfect.FractionClass.fractionClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/FractionClassMap.lean, line 663. The attribute's comment: “the canonical map c_{f_1, …, f_c}”.

Stacks Project, Tag 0G7Q. The canonical map c_{f₁, …, f_c} : i^{-1}(ℱ/(f₁, …, f_c)ℱ) ⟶ 𝓗ᶜ_Z(ℱ) of 𝒪_X|_Z-modules on the common zero locus Z of f₁, …, f_c, for a quasi-coherent 𝒪_X-module ℱ: it is the transpose, under the adjunction between inverse image and direct image along the inclusion of Z, of the map carrying the class of a local section s of ℱ to the class of the fraction s / (f₁ ⋯ f_c) in the degree-c cohomology sheaf of the extended alternating Čech complex of the equations, which is the direct image of 𝓗ᶜ_Z(ℱ).

public def fractionClass [F.IsQuasicoherent] :
    (modulePullback (closedSubsetInclusion X.toRingedSpace (equationsClosedSet f))).obj
        (equationsQuotient f F) ⟶
      localCohomologySheafOfComplex X.toRingedSpace (equationsClosedSet f)
        (isClosed_equationsClosedSet f) (c : ℤ)
        ((DerivedCategory.singleFunctor X.Modules 0).obj F)

Stacks.Perfect.FractionClass.pushforwardFractionClass_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/FractionClassMap.lean, line 686. The attribute's comment: “the fraction class followed by the identifications”.

Stacks Project, Tag 0G7Q. The map to the direct image of the local cohomology sheaf is the fraction class followed by the two identifications: the comparison of the two constructions of the extended alternating Čech complex, and the identification of the degree-c cohomology sheaf of that complex with the direct image of 𝓗ᶜ_Z(ℱ).

public theorem pushforwardFractionClass_eq [F.IsQuasicoherent] :
    pushforwardFractionClass f F =
      (quotientClassMap f F ≫ HomologicalComplex.homologyMap
          (Stacks.Perfect.CechComparison.complexIso f F).inv c) ≫
        (Stacks.Perfect.CechLocalCohomology.pushforwardLocalCohomologyIso f F c).inv

Stacks.Perfect.FractionClass.homEquiv_fractionClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/FractionClassMap.lean, line 695. The attribute's comment: “c_{f_1, …, f_c} is the transpose of the fraction class”.

Stacks Project, Tag 0G7Q. The map c_{f₁, …, f_c} is the transpose of the map from the quotient ℱ/(f₁, …, f_c)ℱ to the direct image of the degree-c local cohomology sheaf.

public theorem homEquiv_fractionClass [F.IsQuasicoherent] :
    homEquiv (closedSubsetInclusion X.toRingedSpace (equationsClosedSet f)) _
        (equationsQuotient f F) (fractionClass f F) =
      pushforwardFractionClass f F

Stacks.Perfect.SupportedFraction.supportedFractionClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/SupportedFractionMap.lean, line 738. The attribute's comment: “i_* of the remark's map c_{f₁,…,f_c}, between its two presentations; no descent”.

Stacks Project, Tag 0G7Q, the class of the fraction s / (f₁ ⋯ f_c). With X, f₁, …, f_c ∈ Γ(X, 𝒪_X) and ℱ as in Tag 0G7I, this is the map

Coker((f₁, …, f_c) : ℱ^{⊕c} ⟶ ℱ) ⟶ Coker(⨁ᵢ ℱ_{1…î…c} ⟶ ℱ_{1…c})

carrying the class of a local section s of ℱ to the class of the fraction s / (f₁ ⋯ f_c), by supportedFractionClass_mk. It is the direct image along the closed immersion i : Z → X of the map c_{f₁,…,f_c} : i^*ℱ ⟶ ℋ^c_Z(ℱ) of the remark: its source is i_* i^*ℱ, presented as the cokernel of (f₁, …, f_c) as the remark does, and its target is i_* ℋ^c_Z(ℱ), presented as the cokernel of the last differential of the extended alternating Čech complex as the remark does, the two being identified by Tag 0G7M.

public def supportedFractionClass {d : ℕ} (f : Fin (d + 1) → Γ(X, ⊤)) (F : X.Modules) :
    cokernel (equationsMultiplication f F) ⟶ cokernel (lastDif f F)

Stacks.Perfect.SupportedFraction.supportedFractionClass_mk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/SupportedFractionMap.lean, line 748. The attribute's comment: “the value of the class map on the class of a section”.

Stacks Project, Tag 0G7Q. The class map sends the class of a local section s of ℱ to the class of the fraction s / (f₁ ⋯ f_c) in the cokernel of the last differential of the extended alternating Čech complex.

public theorem supportedFractionClass_mk {d : ℕ} (f : Fin (d + 1) → Γ(X, ⊤))
    (F : X.Modules) (V : X.Opens) (s : Γ(F, V)) :
    (supportedFractionClass f F).app V
        ((cokernel.π (equationsMultiplication f F)).app V s) =
      (cokernel.π (lastDif f F)).app V ((fractionHom f F d).app V s)

Stacks.Perfect.SupportedFraction.fractionClassTrans, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/SupportedFractionNaturality.lean, line 489. The attribute's comment: “the canonical map c_{f₁,…,f_c} : i^ℱ ⟶ ℋ^c_Z(ℱ) together with its functoriality in the 𝒪_X-module ℱ, as a natural transformation between the two functors of ℱ: from ℱ ↦ i_i^ℱ, the cokernel of (f₁,…,f_c) as the remark presents it, to ℱ ↦ i_ℋ^c_Z(ℱ); read on X along the fully faithful i_*, as the remark's last step and as Stacks 0G7T does for the twisted map”.

Stacks Project, Tag 0G7Q. With X a scheme, f₁, …, f_c ∈ Γ(X, 𝒪_X) global functions and Z ⊆ X the closed subscheme they cut out, there is a canonical map

c_{f₁, …, f_c} : i^*ℱ ⟶ ℋ^c_Z(ℱ)

of 𝒪_X|_Z-modules, functorial in the 𝒪_X-module ℱ. Here it is that functoriality: a natural transformation between the two functors of ℱ, from ℱ ↦ i_*i^*ℱ (equationsQuotientFunctor, the cokernel of (f₁, …, f_c) : ℱ^{⊕c} ⟶ ℱ, which is how the remark presents the source) to ℱ ↦ i_*ℋ^c_Z(ℱ) (supportCohomologySheafFunctor). Both functors are direct images along the inclusion of Z, which is fully faithful, so the transformation is the map of 𝒪_X|_Z-modules of the statement — this is the last step of the remark's construction and the form in which Stacks 0G7T states the analogous twisted map (Stacks.Perfect.ConormalClass.conormalTwistClass).

Its component at ℱ is the map supportedFractionClass of the remark, between the two presentations, followed by the canonical identification General.cokernelLastDifToSupport of its target with i_*ℋ^c_Z(ℱ); on the class of a local section s of ℱ it is the class of the fraction s / (f₁ ⋯ f_c), by cokernelπ_comp_fractionClassTrans_app. As in Remark 0G7I, which fixes the setting of this remark, ℱ is an arbitrary 𝒪_X-module and the morphisms of the naturality square are arbitrary morphisms of 𝒪_X-modules: quasi-coherence is used neither by the map nor by its functoriality, which is why the two factors and the naturality square are taken from the namespace General above, and the source adds it only in Stacks 0G7S and Stacks 0G7U.

The target is the spelling of i_*ℋ^c_Z(ℱ) in which Stacks 0G7Q and Stacks 0G7S are stated here, with the direct image taken before the cohomology sheaf. The other spelling, with the cohomology sheaf taken on Z first — the one Stacks.Perfect.FractionClass.fractionClass lands in — is identified with this one, naturally in ℱ and with no hypothesis on ℱ, by Stacks.Perfect.GysinLocalCohomology.supportCohomologySheafFunctorIso.

public def fractionClassTrans {d : ℕ} (f : Fin (d + 1) → Γ(X, ⊤)) :
    equationsQuotientFunctor f ⟶
      supportCohomologySheafFunctor (isClosed_equationsClosedSet f) ((d + 1 : ℕ) : ℤ)

Tag 0G7R, an example

Tag 0G7R in the Stacks Project.

Stacks.Perfect.AffineFractionClass.supportedFraction_eq_conj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/AffineFractionClassBijective.lean, line 673. The attribute's comment: “the description itself: Γ(Spec A, -) of Tag 0G7Q's map c_{f₁,…,f_c} for ℱ = M~, conjugated by the two canonical isomorphisms affineSourceEquiv and targetEquiv, IS the map Cech.supportedFraction of Tag 0G7R”.

Clause 3 of Tag 0G7R. Let A be a commutative ring, let f₁, …, f_c ∈ A be a finite nonempty family and let M be an A-module. The map c_{f₁,…,f_c} of Tag 0G7Q for X = Spec A and ℱ = M~, in the cokernel-to-cokernel presentation Coker((f₁,…,f_c) : ℱ^{⊕c} ⟶ ℱ) ⟶ Coker(lastDif) of Stacks.Perfect.SupportedFraction.supportedFractionClass, read on global sections through the two canonical isomorphisms

M/(f₁,…,f_c)M ≅ Γ(Spec A, Coker((f₁,…,f_c) : (M~)^{⊕c} ⟶ M~)) (affineSourceEquiv) and Coker(⨁ᵢ M_{f₁⋯f̂ᵢ⋯f_c} ⟶ M_{f₁⋯f_c}) ≅ Γ(Spec A, Coker(lastDif)) (targetEquiv),

is the map Cech.supportedFraction by which the example describes it. Both comparisons are isomorphisms (bijective_affineSourceComparison and bijective_targetComparison).

public theorem supportedFraction_eq_conj (f : Fin (d + 1) → R) (M : ModuleCat.{u} R) :
    Cech.supportedFraction f (M : Type u) =
      (targetEquiv f M).symm.toLinearMap ∘ₗ
        ((moduleSpecΓFunctor.map (supportedFractionClass (specFun f) (tilde M))).hom ∘ₗ
          (affineSourceEquiv f M).toLinearMap)

Stacks.Perfect.AffineFractionClass.targetEquiv_symm_Γ_supportedFractionClass_affineSourceEquiv_mk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/AffineFractionClassBijective.lean, line 715. The attribute's comment: “the example in one statement: for X = Spec A and ℱ = M~, Tag 0G7Q's map c_{f₁,…,f_c} on global sections, conjugated by the canonical isomorphisms affineSourceEquiv and targetEquiv, sends the class of s ∈ M to the class of the fraction s/(f₁⋯f_c) in Coker(⨁ᵢ M_{f₁⋯f̂ᵢ⋯f_c} ⟶ M_{f₁⋯f_c})”.

Tag 0G7R. Let A be a commutative ring, let f₁, …, f_c ∈ A and let M be an A-module. Take X = Spec A and ℱ = M~. Then the map c_{f₁,…,f_c} of Tag 0G7Q, read on global sections through the two canonical A-linear isomorphisms

M/(f₁,…,f_c)M ≅ Γ(Spec A, Coker((f₁,…,f_c) : ℱ^{⊕c} ⟶ ℱ)) (affineSourceEquiv) and Coker(⨁ᵢ M_{f₁⋯f̂ᵢ⋯f_c} ⟶ M_{f₁⋯f_c}) ≅ Γ(Spec A, Coker(lastDif)) (targetEquiv),

is the map M/(f₁,…,f_c)M ⟶ Coker(⨁ᵢ M_{f₁⋯f̂ᵢ⋯f_c} ⟶ M_{f₁⋯f_c}) carrying the class of s ∈ M to the class of the fraction s/(f₁⋯f_c).

This is the example's description, source and target modules, map and formula together, in one statement, for a nonempty family; the empty family is Stacks.Perfect.AffineFractionClassEmpty.targetIsoEmpty_inv_Γ_quotientClassMap_sourceIsoEmpty. The classes of sections exhaust M/(f₁,…,f_c)M, so the formula below determines the conjugated map; the map-level equality is supportedFraction_eq_conj and the formula alone is Cech.supportedFraction_mk.

The ring and the module are taken in a single universe, as tilde requires, whereas Cech.supportedFraction itself is stated for a ring and a module in independent universes. That is a restriction of spelling only: a ring and a module in independent universes are moved into a common universe by ULift.

public theorem targetEquiv_symm_Γ_supportedFractionClass_affineSourceEquiv_mk
    (f : Fin (d + 1) → R) (M : ModuleCat.{u} R) (s : M) :
    (targetEquiv f M).symm
        ((moduleSpecΓFunctor.map (supportedFractionClass (specFun f) (tilde M))).hom
          (affineSourceEquiv f M (Submodule.Quotient.mk s))) =
      Submodule.Quotient.mk
        (DirectSum.lof R {t : Finset (Fin (d + 1)) // t.card = d + 1}
          (fun t => Cech.cechMod f (M : Type u) t.1) ⟨Finset.univ, Finset.card_fin _⟩
          (LocalizedModule.mk s ⟨∏ i, f i, Submonoid.mem_powers _⟩))

Stacks.Perfect.AffineFractionClassEmpty.targetIsoEmpty_inv_Γ_quotientClassMap_sourceIsoEmpty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/AffineFractionClassEmpty.lean, line 145. The attribute's comment: “the case c = 0: for X = Spec A, ℱ = M~ and the empty family, Tag 0G7Q's map on global sections, conjugated by the canonical isomorphisms sourceIsoEmpty and targetIsoEmpty, sends the class of s ∈ M to s/(f₁⋯f_c) = s/1”.

For the empty family (c = 0), let A be a commutative ring, let M be an A-module and take X = Spec A, ℱ = M~ and the empty family of equations. Then the map c_{f₁, …, f_c} of Tag 0G7Q, read on global sections through the canonical isomorphisms M/(f₁, …, f_c)M ≅ Γ(Spec A, ℱ/(f₁, …, f_c)ℱ) (sourceIsoEmpty) and M_{f₁⋯f_c} ≅ Γ(Spec A, H⁰(ℱ^•)) (targetIsoEmpty), sends the class of s ∈ M to the fraction s/(f₁⋯f_c); here f₁⋯f_c = 1, the cokernel of the map out of the empty direct sum is M_{f₁⋯f_c} itself, and the map is s ↦ s/1.

theorem targetIsoEmpty_inv_Γ_quotientClassMap_sourceIsoEmpty (s : M) :
    (targetIsoEmpty f M).inv
        ((moduleSpecΓFunctor.map (quotientClassMap (specFunEmpty f) (tilde M))).hom
          ((sourceIsoEmpty f M).hom (Submodule.Quotient.mk s))) =
      LocalizedModule.mk s ⟨∏ i, f i, Submonoid.mem_powers _⟩

Tag 0G7S, a lemma

Tag 0G7S in the Stacks Project.

Stacks.Perfect.SupportedFraction.supportedFractionClass_eq_det_smul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/DeterminantChangeOfEquations/ClassTarget.lean, line 391. The attribute's comment: “the determinant identity c_{f₁,…,f_c} = det(a_{ji})·c_{g₁,…,g_c} as ONE equation of maps into the common target i_ℋ^c_Z(ℱ), together with the invertibility of the two identifications it is read through. The 0G7Q class maps of the f- and the g-complex are composed with cokernelLastDifToSupport -- cokernel of the last differential ≅ H^c of the complex ≅ i_ℋ^c_Z(ℱ), the last step by the canonical comparison of Stacks 0G7L and its invertibility, which is Stacks 0G7M -- and are read on the common source ℱ through the two canonical epimorphisms ℱ ↠ i_i^ℱ; those are epimorphisms, so this is equivalent to the equality of the class maps and needs no chosen isomorphism between the two presentations of i_i^ℱ. The hypothesis used in place of the source's 'g₁,…,g_c cut out Z scheme theoretically' is the weaker set-level equality of the two common zero loci, so this is a GENERALIZATION and not a weakening: it suffices because RℋT depends only on the closed set T, so no scheme structure on Z enters the identification of the two targets”.

Stacks Project, Tag 0G7S, the determinant identity as a single equation in a common target.

With X, f₁, …, f_c ∈ Γ(X, 𝒪_X) and ℱ as in Stacks 0G7I, let a_{ji} ∈ Γ(X, 𝒪_X) and g_j = ∑_i a_{ji} f_i, let ℱ be quasi-coherent and let g₁, …, g_c cut out the same closed subset Z as f₁, …, f_c. Then

c_{f₁,…,f_c} = det(a_{ji}) c_{g₁,…,g_c}

as maps into the single object i_*ℋ^c_Z(ℱ).

The two class maps supportedFractionClass f F and supportedFractionClass g F of Stacks 0G7Q land in the cokernels of the last differentials of the f- and the g-complex. Each of those cokernels is identified with i_*ℋ^c_Z(ℱ) by cokernelLastDifToSupport, the composite of cokernelLastDifIsoHomology (the cokernel of the last differential is the degree-c cohomology of the complex) with the degree-c cohomology of the canonical comparison cechToDerivedSupport of Stacks 0G7L; both identifications are isomorphisms, which is the first two conjuncts and is Stacks 0G7M. Both class maps are then read on the common source ℱ through the canonical epimorphisms cokernel.π (equationsMultiplication f F) and cokernel.π (equationsMultiplication g F) presenting i_* i^*ℱ in the two ways the remark does; since those are epimorphisms, the displayed equation is equivalent to the equality of the class maps themselves, and no choice of isomorphism between the two presentations of i_* i^*ℱ is needed.

The proof is the source's: both sides are the image of the single degree-c cohomology class of the mixed cocycle mixedFractionHom on the complex of the 2c equations f₁, …, f_c, g₁, …, g_c (subfamily_comp_cokernelπ_comp_cokernelLastDifToSupport applied to the two projections mixedFractionHom_subfamilyProd_castAdd and mixedFractionHom_subfamilyProd_natAdd).

The hypothesis hZ replaces the source's "g₁, …, g_c cut out Z scheme theoretically" by the equality of the two common zero loci as closed subsets. That is implied by the scheme-theoretic condition, so the statement is a generalisation of the source's and not a weakening of it. It suffices because R𝓗_T depends only on the closed subset T: no scheme structure on Z enters the identification of the two targets.

public theorem supportedFractionClass_eq_det_smul {d : ℕ} (f g : Fin (d + 1) → Γ(X, ⊤))
    (a : Matrix (Fin (d + 1)) (Fin (d + 1)) Γ(X, ⊤)) (F : X.Modules) [F.IsQuasicoherent]
    (hg : ∀ j, g j = ∑ i, a j i * f i)
    (hZ : equationsClosedSet g = equationsClosedSet f) :
    IsIso (cokernelLastDifToSupport f F (isClosed_equationsClosedSet f) subset_rfl) ∧
      IsIso (cokernelLastDifToSupport g F (isClosed_equationsClosedSet f) hZ.le) ∧
      cokernel.π (equationsMultiplication f F) ≫ supportedFractionClass f F ≫
          cokernelLastDifToSupport f F (isClosed_equationsClosedSet f) subset_rfl =
        globalSmul a.det F ≫ cokernel.π (equationsMultiplication g F) ≫
          supportedFractionClass g F ≫
            cokernelLastDifToSupport g F (isClosed_equationsClosedSet f) hZ.le

Stacks.Perfect.SupportedFraction.mixedFractionHom_projections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/DeterminantChangeOfEquations/Cocycle.lean, line 361. The attribute's comment: “the source's own construction: the explicit degree-c cocycle on the mixed extended alternating Čech complex of f₁,…,f_c,g₁,…,g_c is a cocycle, and projects to s/(f₁⋯f_c) and to det(a)·s/(g₁⋯g_c). Stated at the level of the complexes, i.e. before the identification of the degree-c cohomology of the three complexes with i_*ℋ^c_Z(ℱ); that identification is Stacks 0G7M, and composing it with this statement to obtain the single equation c_{f₁,…,f_c} = det(a_{ji})·c_{g₁,…,g_c} is carried out in this module, in supportedFractionClass_eq_det_smul”.

Stacks Project, Tag 0G7S, the determinant identity on the mixed extended alternating Čech complex.

With X, f₁, …, f_c ∈ Γ(X, 𝒪_X) and ℱ as in Stacks 0G7I, let a_{ji} ∈ Γ(X, 𝒪_X) and g_j = ∑_i a_{ji} f_i. Write 𝓕''^• for the extended alternating Čech complex of the mixed family f₁, …, f_c, g₁, …, g_c of 2c equations, which is the complex the source's proof introduces. Projecting away the components involving a g, respectively an f, gives the two morphisms of complexes 𝓕''^• ⟶ 𝓕^• and 𝓕''^• ⟶ (𝓕')^• of the source, both the identity in degree 0 (subfamilyCplxMap, whose degree-(c) component is subfamilyProd).

The content of the lemma is the explicit degree-c cocycle σ = mixedFractionHom of the source, whose component at an increasing c-tuple q of the 2c indices is det(minor of (a_{ji}) selected by q) · s / (product of the equations of q):

• σ is a cocycle;
• its projection to 𝓕^• is s / (f₁ ⋯ f_c), i.e. c_{f₁,…,f_c};
• its projection to (𝓕')^• is det(a_{ji}) s / (g₁ ⋯ g_c), i.e. det(a_{ji}) c_{g₁,…,g_c}.

What is not carried out here is the last step of the source's proof: passing from these two projections of σ to the single equation c_{f₁,…,f_c} = det(a_{ji}) c_{g₁,…,g_c} of sheaf maps i^*ℱ ⟶ ℋ^c_Z(ℱ). That step is the identification of the degree-c cohomology of each of the three complexes with i_*ℋ^c_Z(ℱ), which is Stacks 0G7M and is available in this library — Stacks.Perfect.CechDerivedSupport.isIso_map_augmentation_of_isQuasicoherent for the half that uses the quasi-coherence of ℱ, and isIso_derivedSupportedSectionsToId_cech above for the canonical form of the other half. What is missing is only the bookkeeping that composes the two statements below with those identifications: the comparison cechToDerivedSupport of Stacks 0G7L above, its degree-c cohomology sheaf, and the identification of H^c of each complex with the cokernel of its last differential. The hypothesis that g₁, …, g_c cut out Z scheme theoretically is likewise needed only for that step — it is what makes the two identifications land in the same i_*ℋ^c_Z(ℱ) — and so does not appear below.

public theorem mixedFractionHom_projections (hg : ∀ j, g j = ∑ i, a j i * f i) :
    mixedFractionHom (mixedEquations f g) a F ≫ difSucc (mixedEquations f g) F d = 0 ∧
      mixedFractionHom (mixedEquations f g) a F ≫
          subfamilyProd (mixedEquations f g) (Fin.castAddOrderEmb (d + 1) :
            Fin (d + 1) ↪o Fin ((d + 1) + (d + 1))) F d ≫
          prodTermCongr (mixedEquations_comp_castAdd f g) F d =
        fractionHom f F d ∧
      mixedFractionHom (mixedEquations f g) a F ≫
          subfamilyProd (mixedEquations f g) (Fin.natAddOrderEmb (d + 1) :
            Fin (d + 1) ↪o Fin ((d + 1) + (d + 1))) F d ≫
          prodTermCongr (mixedEquations_comp_natAdd f g) F d =
        globalSmul a.det F ≫ fractionHom g F d

Stacks.Perfect.SupportedFraction.mixedFractionHom_comp_cokernelπ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/DeterminantChangeOfEquations/Cocycle.lean, line 396. The attribute's comment: “the same identity read on the two class maps c_{f₁,…,f_c} and c_{g₁,…,g_c} of Stacks 0G7Q, with the two sides in the cokernels of the last differentials of the two complexes rather than in a common i_ℋ^c_Z(ℱ); the identification of those cokernels with i_ℋ^c_Z(ℱ) is Stacks 0G7M, and composing it with this statement to obtain the single equation is supportedFractionClass_eq_det_smul in this module”.

Stacks Project, Tag 0G7S, read on the classes of Stacks 0G7Q.

The class map c_{f₁,…,f_c} of Stacks 0G7Q is supportedFractionClass f F, carrying the class of a local section s to the class of s / (f₁ ⋯ f_c) in the cokernel of the last differential of the extended alternating Čech complex of f₁, …, f_c. Both c_{f₁,…,f_c} and det(a_{ji}) c_{g₁,…,g_c} are the image of the single degree-c class σ of the mixed complex under the two projections. This is the equality in the form the source proves it, with the two sides still living in the cokernels of the last differentials of the f- and the g-complex rather than in a common i_*ℋ^c_Z(ℱ); the identification of those two cokernels with i_*ℋ^c_Z(ℱ) is Stacks 0G7M, and composing it with this statement to obtain the single equation is supportedFractionClass_eq_det_smul below.

public theorem mixedFractionHom_comp_cokernelπ (hg : ∀ j, g j = ∑ i, a j i * f i) :
    mixedFractionHom (mixedEquations f g) a F ≫
          subfamilyProd (mixedEquations f g) (Fin.castAddOrderEmb (d + 1) :
            Fin (d + 1) ↪o Fin ((d + 1) + (d + 1))) F d ≫
          prodTermCongr (mixedEquations_comp_castAdd f g) F d ≫
          cokernel.π (lastDif f F) =
        cokernel.π (equationsMultiplication f F) ≫ supportedFractionClass f F ∧
      mixedFractionHom (mixedEquations f g) a F ≫
          subfamilyProd (mixedEquations f g) (Fin.natAddOrderEmb (d + 1) :
            Fin (d + 1) ↪o Fin ((d + 1) + (d + 1))) F d ≫
          prodTermCongr (mixedEquations_comp_natAdd f g) F d ≫
          cokernel.π (lastDif g F) =
        globalSmul a.det F ≫
          cokernel.π (equationsMultiplication g F) ≫ supportedFractionClass g F

Tag 0G7T, a lemma

Tag 0G7T in the Stacks Project.

Stacks.Perfect.ConormalClass.conormalTwistClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/ConormalClass/Main.lean, line 103. The attribute's comment: “the canonical map, as a natural transformation of functors of the module F; its value on a chart is conormalTwistClass_app_tmul”.

The canonical map ⋀^c(𝒞_{Z/X})^∨ ⊗_{𝒪_Z} i^*ℱ ⟶ ℋ^c_Z(ℱ), functorial in ℱ, for a closed immersion i : Z ⟶ X of finite presentation whose conormal sheaf 𝒞_{Z/X} is finite locally free of rank c. The source is i_* of the tensor product over 𝒪_Z (Stacks 01CA) of the dual SheafHom(⋀^c 𝒞_{Z/X}, 𝒪_Z) of the c-th exterior power of the conormal sheaf with i^*ℱ, and the target is ℋ^c_Z(ℱ) read on X; the direct image along i is fully faithful, so this is the map of 𝒪_X|_Z-modules of the statement. On a chart it is the map of conormalTwistClass_app_tmul.

def conormalTwistClass :
    twistFunctor i c ⟶ supportCohomologySheafFunctor (isClosed_zeroLocus i) (c : ℤ)

Stacks.Perfect.ConormalClass.conormalTwistClass_app_tmul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/ConormalClass/Main.lean, line 117. The attribute's comment: “canonicity: on every chart the map is the twisted fraction class of Stacks 0G7Q, λ ⊗ s ↦ c_{f₁, …, f_c}(λ(f₁ ∧ ⋯ ∧ f_c) s)”.

The value of conormalTwistClass on a chart. Let W ⊆ X be an open on which f₁, …, f_c generate the ideal sheaf of Z, let U ⊆ W be open, λ a local section of (⋀^c 𝒞_{Z/X})^∨ over Z ∩ U, s a local section of ℱ over U and r a function on U restricting on Z ∩ U to λ(f₁ ∧ ⋯ ∧ f_c). Then c(λ ⊗ s), read in ℋ^c_{T}(ℱ) for the closed subset T ⊇ Z of the chart (over W the change of support ℋ^c_Z ⟶ ℋ^c_T is an isomorphism), is the class c_{f₁, …, f_c}(r s) of the fraction r s / (f₁ ⋯ f_c) of Stacks 0G7Q. In particular the map does not depend on the chart.

theorem conormalTwistClass_app_tmul {W : X.Opens} {f : Fin c → Γ(X, W)}
    (hgen : IsGeneratedByOn X.toRingedSpace (definingIdealOfHom i) W f) (U : X.Opens) (hU : U ≤ W)
    (lam : (dualSheaf Z.toRingedSpace (line i c)).val.obj (op (i ⁻¹ᵁ U))) (s : Γ(F, U))
    (r : Γ(X, U))
    (hr : (i.app U).hom r = dualEval Z.toRingedSpace (line i c) lam
      ((line i c).presheaf.map (homOfLE (i.preimage_mono hU)).op
        (wedge i f (app_chart_eq_zero W f hgen)))) :
    (supportChangeH (isClosed_zeroLocus i) (isClosed_chartSupport W (chartEq W f))
        (zeroLocus_subset_chartSupport W f hgen) F (c : ℤ)).app U
        (((conormalTwistClass i c).app F).app U
          (tensorObjTmul Z.toRingedSpace (dualModule (line i c)) ((Scheme.Modules.pullback i).obj F)
            (op (i ⁻¹ᵁ U)) lam
            (((Scheme.Modules.pullbackPushforwardAdjunction i).unit.app F).app U s))) =
      (topClass W F (isClosed_chartSupport W (chartEq W f)) (chartEq W f) subset_rfl).app U
        (r • s)

Tag 0G7U, a remark

Tag 0G7U in the Stacks Project.

Stacks.Perfect.CechBaseChangeCounterexample.isEmpty_iso_cplx, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/CechBaseChangeCounterexample.lean, line 494. The attribute's comment: “refutes the note (F')^• = g^*F^• for a non-quasi-coherent F: for the diagonal A^1 → A^2, f_1 = x and F the extension by zero of O from D(y), the two complexes are not isomorphic at all; the quasi-coherent form is isIso_cplxBaseChange”.

No isomorphism at all between the extended alternating Čech complexes g^*(ℱ^•) and (g^*ℱ)^• of the counterexample: their degree-one terms are a single g^*(j_*(ℱ|_U)), resp. j'_*((g^*ℱ)|_{U'}), and these are not isomorphic (isEmpty_iso_restrictedModule). This refutes the note (ℱ')^• = g^*ℱ^• of [Stacks, Tag 0G7U] for non-quasi-coherent ℱ in its strongest reading, with no comparison map fixed in advance.

theorem isEmpty_iso_cplx :
    IsEmpty (((Scheme.Modules.pullback (diag k)).mapHomologicalComplex (ComplexShape.up ℕ)).obj
        (cplx (eqns k) (coeff k)) ≅
      cplx (fun j => (diag k).appTop (eqns k j)) ((Scheme.Modules.pullback (diag k)).obj
        (coeff k)))

Stacks.Perfect.CechBaseChangeCounterexample.not_isIso_cplxBaseChange_f_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/CechBaseChangeCounterexample.lean, line 511. The attribute's comment: “refutes the note (F')^• = g^*F^• for a non-quasi-coherent F: the comparison cplxBaseChange is not an isomorphism in degree 1 for the diagonal A^1 → A^2, f_1 = x and F the extension by zero of O from D(y); the quasi-coherent form is isIso_cplxBaseChange”.

The base-change comparison of complexes of [Stacks, Tag 0G7U] is not an isomorphism for the non-quasi-coherent module ℱ = coeff k, already in degree 1. Here k is any field, g : 𝔸¹_k ⟶ 𝔸²_k is the diagonal, the single equation is x, and ℱ is the sheaf of functions with vanishing germ at the generic point of the line y = 0 (the extension by zero of 𝒪 from D(y)). So the note (ℱ')^• = g^*ℱ^• of the remark, read through the comparison map cplxBaseChange, is false for an arbitrary 𝒪_X-module; for quasi-coherent ℱ it holds (Stacks.Perfect.CechBaseChange.isIso_cplxBaseChange).

theorem not_isIso_cplxBaseChange_f_one :
    ¬ IsIso ((cplxBaseChange (diag k) (eqns k) (coeff k)).f 1)

Stacks.Perfect.CechDegreeCBaseChange.supportedFractionSource_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/CechDegreeCBaseChange.lean, line 302. The attribute's comment: “the first diagram of the remark: the class map c_{f_1,...,f_c} of Tag 0G7Q commutes with base change, for quasi-coherent F, read on X in i_*H^c_Z(F) -- the spelling supportedFractionSource, which is the one Tag 0G7Q is itself registered at in SupportedFractionMap. Its top horizontal arrow IS the map of Cohomology Remark 0G78 on cohomology sheaves in degree c, which the remark's own sentence asserts: that identification is degreeCBaseChange_eq_homology_zeroG78 below, prefixed by the comparison the remark suppresses”.

The first diagram of [Stacks, Tag 0G7U]: the class map c_{f₁,…,f_c} of [Stacks, Tag 0G7Q], read on the coefficient module and in i_*ℋ^c_Z(ℱ), commutes with base change. The inverse image of the class map for f and ℱ, followed by the degree-c comparison degreeCBaseChange, is the class map for the pulled-back equations f' and the inverse-image module ℱ'.

Unfolding both class maps, the inverse of the identification of [Stacks, Tag 0G7M] sitting in degreeCBaseChange cancels against its occurrence in the class map, and what is left is the class of the fraction s / (f₁ ⋯ f_c): the characterizing property of the preserved-cokernel comparison turns the inverse image of the class of a top-degree cochain into the class of its inverse image, and the remaining identity is the compatibility of the fraction with base change, Stacks.Perfect.CechFractionBaseChange.cplxBaseChange_comp_fracTermTop.

public theorem supportedFractionSource_baseChange [F.IsQuasicoherent] :
    (Scheme.Modules.pullback g).map
          (supportedFractionSource f F (isClosed_equationsClosedSet f) le_rfl) ≫
        degreeCBaseChange g f F =
      supportedFractionSource (fun j => g.appTop (f j)) ((Scheme.Modules.pullback g).obj F)
        (isClosed_equationsClosedSet (fun j => g.appTop (f j))) le_rfl

Stacks.Perfect.CechDegreeCBaseChange.degreeCBaseChange_eq_homology_zeroG78, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/CechDegreeCBaseChange.lean, line 686. The attribute's comment: “the top horizontal arrow of the first diagram is the map of Cohomology Remark 0G78 on cohomology sheaves in degree c: the degree-c cohomology of the upper route of the derived diagram, preceded by the canonical comparison of H^c(Lg^(-)) with g^H^c(-) that the remark leaves implicit”.

The top arrow of the first diagram of [Stacks, Tag 0G7U] is the map of [Stacks, Tag 0G78] read on cohomology sheaves in degree c. This is what the remark asserts verbatim: the top horizontal arrow of its first diagram "is the map of Cohomology, Remark 0G78 on cohomology sheaves in degree c".

The arrow of [Stacks, Tag 0G78] is the upper route Stacks.Perfect.SupportedDerivedBaseChange.supportedPullbackRoute of the remark's derived diagram — its left-hand equal sign followed by its top horizontal arrow — followed by i'_* R𝓗_{Z'} of the down arrow Lg^*ℱ ⟶ ℱ'; it is the whole left-to-right passage of the derived diagram above the Čech complexes, and it is the composite that stands to the left of Lg^* of the comparison of [Stacks, Tag 0G7L] in Stacks.Perfect.CechDerivedBaseChange.derivedBaseChangeSquare_cech. Its degree-c cohomology starts at ℋ^c(Lg^* i_* R𝓗_Z(ℱ)), not at g^*ℋ^c_Z(ℱ) where degreeCBaseChange starts, so the canonical comparison derivedPullbackDegreeCComparison of the two is prefixed; and it ends at i'_*ℋ^c_{Z'}(ℱ') spelled at the preimage g^{-1}(Z), so the identification supportCohomologySheafPullbackIso of the two spellings of Z' is appended.

The proof is the source's own: take the degree-c cohomology of the derived diagram derivedBaseChangeSquare_cech, and cancel ℋ^c(Lg^*(ℱ^• ⟶ i_* R𝓗_Z(ℱ))), which is invertible because the comparison of [Stacks, Tag 0G7L] is ([Stacks, Tag 0G7M], as Stacks.Perfect.SupportedFraction.isIso_cechToSupport). What is left on the other side is ℋ^c of the lower horizontal arrow Lg^*(ℱ^•) ⟶ (ℱ')^• followed by ℋ^c of the comparison of [Stacks, Tag 0G7L] for f' and ℱ', and that is cokernelLastDifBaseChange followed by the identification of [Stacks, Tag 0G7M] — which is degreeCBaseChange — by homologyMap_extendBaseChange.

public theorem degreeCBaseChange_eq_homology_zeroG78 [F.IsQuasicoherent] :
    derivedPullbackDegreeCComparison g f F ≫ degreeCBaseChange g f F =
      (DerivedCategory.homologyFunctor X'.Modules ((d + 1 : ℕ) : ℤ)).map
          (supportedPullbackRoute g.toLRSHom.toShHom (equationsClosedSet f)
              (isClosed_equationsClosedSet f)
              ((DerivedCategory.singleFunctor X.Modules 0).obj F) ≫
            (supportPush (isClosed_equationsClosedSet_pullback g f)).map
              (derivedPullbackSingleObj g.toLRSHom.toShHom F)) ≫
        (supportCohomologySheafPullbackIso g f F).hom

Stacks.Perfect.CechDegreeCBaseChange.fractionClassTrans_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/CechDegreeCBaseChange.lean, line 922. The attribute's comment: “the first diagram of the remark with all four arrows, for quasi-coherent F: the components of the Tag 0G7Q transformation c_{f_1,...,f_c} at F and at F' = g^F on the quotients i_i^F = F/(f_1,...,f_c)F, the comparison of the two quotients as bottom arrow, and the degree-c comparison (the Tag 0G78 map in degree c) as top arrow; read on X' along the fully faithful i'_”.

The first diagram of [Stacks, Tag 0G7U], with all four of its arrows, read on X' along the fully faithful direct image i'_* along the inclusion of Z': for a quasi-coherent 𝒪_X-module ℱ the square

g^*(i_*ℋ^c_Z(ℱ))  --degreeCBaseChange-->  i'_*ℋ^c_{Z'}(ℱ')
      ^                                          ^
 g^*(c_{f₁,…,f_c})                         c_{f'₁,…,f'_c}
      |                                          |
g^*(i_*i^*ℱ)  --equationsQuotientBaseChange-->  i'_*(i')^*ℱ'

commutes, where the vertical arrows are the components at ℱ and at ℱ' = g^*ℱ of the natural transformation Stacks.Perfect.SupportedFraction.fractionClassTrans that [Stacks, Tag 0G7Q] is registered at — c_{f₁,…,f_c} read on X along the fully faithful i_*, with source the quotient ℱ/(f₁, …, f_c)ℱ = i_*i^*ℱ that the remark presents it on — the bottom arrow is the comparison of the two quotients, and the top arrow is the degree-c comparison, which is the map of Cohomology, Remark 0G78 on cohomology sheaves in degree c by degreeCBaseChange_eq_homology_zeroG78.

Why this is the remark's diagram. The remark's diagram lives on Z', with corners h^*i^*ℱ, (i')^*ℱ', (i')^{-1}𝒪_{X'} ⊗_{h^{-1}i^{-1}𝒪_X} h^{-1}ℋ^c_Z(ℱ) = h^*ℋ^c_Z(ℱ) and ℋ^c_{Z'}(ℱ'). Applying the fully faithful i'_* does not change whether it commutes, and i'_*h^* = g^*i_* for the cartesian square Z' = Z ×_X X' of the setting (AlgebraicGeometry.ExtendedAlternatingCech.isPullback_equationsClosedSubscheme) carries its left-hand corners to g^*(i_*i^*ℱ) and g^*(i_*ℋ^c_Z(ℱ)); this is the form in which the library states the class map of [Stacks, Tag 0G7Q] itself.

The proof cancels the epimorphism g^* of the projection ℱ ⟶ i_*i^*ℱ and is then supportedFractionSource_baseChange.

public theorem fractionClassTrans_baseChange [F.IsQuasicoherent] :
    (Scheme.Modules.pullback g).map ((fractionClassTrans f).app F) ≫
        degreeCBaseChange g f F =
      equationsQuotientBaseChange g f F ≫
        (fractionClassTrans (fun j => g.appTop (f j))).app
          ((Scheme.Modules.pullback g).obj F)

Stacks.Perfect.CechDegreeCBaseChangeOnClosed.fractionClassOnClosed_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/CechDegreeCBaseChangeOnClosed.lean, line 344. The attribute's comment: “the first diagram of the remark on the closed subscheme Z', for quasi-coherent F: h^c_{f_1,...,f_c} followed by the top arrow h^H^c_Z(F) -> H^c_{Z'}(F') equals the canonical h^i^F -> (i')^*F' followed by c_{f'_1,...,f'_c}, with c the Tag 0G7Q map on the closed subset”.

[Stacks, Tag 0G7U], the first diagram, on the closed subscheme Z'. Let g : X' ⟶ X be a morphism of schemes, f₁, …, f_c ∈ Γ(X, 𝒪_X), f'ⱼ = g^♯(fⱼ), Z ⊆ X and Z' ⊆ X' the closed subsets cut out by them, made into ringed spaces (Z, i^{-1}𝒪_X) and (Z', (i')^{-1}𝒪_{X'}), and h : Z' ⟶ Z the induced morphism (closedRestriction). For a quasi-coherent 𝒪_X-module ℱ, with ℱ' = g^*ℱ, the diagram

h^*ℋ^c_Z(ℱ)   --topArrow-->   ℋ^c_{Z'}(ℱ')
     ^                              ^
h^*c_{f₁,…,f_c}               c_{f'₁,…,f'_c}
     |                              |
h^*i^*ℱ      --bottomArrow-->   (i')^*ℱ'

commutes. Here c_{f₁,…,f_c} and c_{f'₁,…,f'_c} are the components at ℱ and at ℱ' of Stacks.Perfect.GysinLocalCohomology.fractionClassOnClosed, the map of [Stacks, Tag 0G7Q] on the closed subset, with source the remark's presentation i^*(ℱ/(f₁, …, f_c)ℱ) of i^*ℱ; the left-hand top corner is h^*ℋ^c_Z(ℱ) = (i')^{-1}𝒪_{X'} ⊗_{h^{-1}i^{-1}𝒪_X} h^{-1}ℋ^c_Z(ℱ), the inverse image of modules along the morphism of ringed spaces h; the bottom arrow is the canonical comparison h^*i^*ℱ ≅ (i')^*g^*ℱ = (i')^*ℱ'; and the top arrow is the one determined by the degree-c comparison degreeCBaseChange, which is the map of Cohomology, Remark 0G78 on cohomology sheaves in degree c (Stacks.Perfect.CechDegreeCBaseChange.degreeCBaseChange_eq_homology_zeroG78).

The proof is the remark's: the diagram read on X' is Stacks.Perfect.CechDegreeCBaseChange.fractionClassTrans_baseChange, and comp_transposeTop descends it to Z', the comparison of inverse images being conjugate to the comparison of direct images by Stacks.Cohomology.conjugateEquiv_pullbackCompSquare.

theorem fractionClassOnClosed_baseChange [F.IsQuasicoherent] :
    (modulePullback (closedRestriction g f)).map ((fractionClassOnClosed f).app F) ≫
        topArrow g f F =
      bottomArrow g f F ≫
        (fractionClassOnClosed (fun j => g.appTop (f j))).app
          ((Scheme.Modules.pullback g).obj F)

Stacks.Perfect.CechDerivedBaseChange.derivedBaseChangeSquare_cech, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/CechDerivedBaseChange.lean, line 375. The attribute's comment: “the derived diagram of the remark, with the remark's own lower horizontal arrow Lg^F^bullet -> g^F^bullet -> (F')^bullet and its own down arrow induced by Lg^F -> g^F = F', for an arbitrary O_X-module F”.

The derived diagram of [Stacks, Tag 0G7U] commutes, for the lower horizontal arrow and the down arrow the remark itself writes down. This is Stacks.Perfect.SupportedDerivedBaseChange.derivedBaseChangeSquare instantiated at cechDerivedBaseChange and AlgebraicGeometry.RingedSpaceThickening.derivedPullbackSingleObj, whose compatibility with the augmentations of [Stacks, Tag 0G7L] is cechDerivedBaseChange_comp_augmentation.

public theorem derivedBaseChangeSquare_cech :
    (derivedPullback g.toLRSHom.toShHom).map
          (cechToDerivedSupport f F (isClosed_equationsClosedSet f) le_rfl) ≫
        supportedPullbackRoute g.toLRSHom.toShHom (equationsClosedSet f)
            (isClosed_equationsClosedSet f)
            ((DerivedCategory.singleFunctor X.Modules 0).obj F) ≫
        (supportPush (isClosed_equationsClosedSet_pullback g f)).map
          (derivedPullbackSingleObj g.toLRSHom.toShHom F) =
      cechDerivedBaseChange g f F ≫
        cechToDerivedSupport (fun j => g.appTop (f j)) ((Scheme.Modules.pullback g).obj F)
          (isClosed_equationsClosedSet_pullback g f) (equationsClosedSet_pullback_subset g f)

AlgebraicGeometry.ExtendedAlternatingCech.isPullback_equationsClosedSubscheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/EquationsBaseChange.lean, line 276. The attribute's comment: “Z' = Z ×_X X' of the setting, as a pullback square of schemes”.

Stacks Project, Tag 0G7U, the assertion Z' = Z ×_X X' of the setting: the closed subscheme cut out by the pulled-back equations f'ᵢ = g^♯(fᵢ) is the base change along g of the closed subscheme cut out by f₁, …, f_c, the induced morphism of schemes being equationsClosedSubschemeBaseChange.

The set-theoretic form of the same assertion, which is the shape [Stacks, Tag 0G78] and hence the remark's diagrams are stated at, is Stacks.Perfect.SupportedDerivedBaseChange.equationsClosedSet_pullback.

public theorem isPullback_equationsClosedSubscheme :
    IsPullback (equationsClosedSubschemeι (fun j => g.appTop (f j)))
      (equationsClosedSubschemeBaseChange g f) g (equationsClosedSubschemeι f)

AlgebraicGeometry.ExtendedAlternatingCech.equationsClosedSubschemePullbackIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/EquationsBaseChange.lean, line 291. The attribute's comment: “the identification Z' ≅ Z ×_X X' of the setting”.

Stacks Project, Tag 0G7U, the identification Z' = Z ×_X X' of the setting, as an isomorphism of schemes.

public def equationsClosedSubschemePullbackIso :
    equationsClosedSubscheme (fun j => g.appTop (f j)) ≅
      pullback g (equationsClosedSubschemeι f)

Stacks.Perfect.CechBaseChange.isIso_cplxBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/OpenDirectImagePullback.lean, line 174. The attribute's comment: “the note (F')^• = g^*F^•, corrected to quasi-coherent F and read through the comparison map; for an arbitrary F it is false, see CechBaseChangeCounterexample.not_isIso_cplxBaseChange_f_one”.

The comparison of the two extended alternating Čech complexes is an isomorphism for quasi-coherent ℱ. This is the corrected form of the note (ℱ')^• = g^*ℱ^• of [Stacks, Tag 0G7U], as an isomorphism of complexes rather than only a morphism — which is what the remark's first diagram needs, and what lets its top arrow be identified with the [Stacks, Tag 0G78] map in degree c rather than with a Čech-level comparison.

The remark states the note for an arbitrary 𝒪_X-module ℱ, and in that generality it is false: Stacks.Perfect.CechBaseChangeCounterexample.not_isIso_cplxBaseChange_f_one takes k a field, g : 𝔸¹_k ⟶ 𝔸²_k the diagonal, the single equation x, and ℱ the extension by zero of 𝒪 from D(y), and shows that this comparison is not an isomorphism in degree 1 (Stacks.Perfect.CechBaseChangeCounterexample.isEmpty_iso_cplx: the two complexes are not isomorphic by any isomorphism). The quasi-coherence hypothesis is therefore needed here; it is the hypothesis under which the remark's first diagram is asserted.

A morphism of complexes is invertible as soon as every component is (HomologicalComplex.Hom.isIso_of_components); here the degree-0 component is the identity and the rest is isIso_prodTermBaseChange. No flatness on g.

public theorem isIso_cplxBaseChange (F : X.Modules) [F.IsQuasicoherent] :
    IsIso (cplxBaseChange g f F)

Sources

• Section 36.6, Tag 0G7F
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.CohomologySupportedOn · Stacks.Perfect.SupportedQuasicoherent.quasiCoherentSupported_derivedSupportedPushforward · Stacks.Perfect.SupportedQuasicoherent.quasiCoherentSupportedInclusionAdj · Stacks.Cohomology.SupportedComplexes.preservesColimitsOfShape_discrete_derivedSupportedSectionsOnClosed · AlgebraicGeometry.ExtendedAlternatingCech.equationsClosedSubscheme · AlgebraicGeometry.ExtendedAlternatingCech.equationsOpen · AlgebraicGeometry.ExtendedAlternatingCech.restrictedModule · AlgebraicGeometry.ExtendedAlternatingCech.functor

Section36.7 The coherator#

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

Tag 08D7, a lemma

Tag 08D7 in the Stacks Project.

AlgebraicGeometry.affineDerivedPushforward_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/Coherator/AffineDerivedPushforwardComparison.lean, line 61. The attribute's comment: “comparison square”.

Stacks Project, Tag 08D7. Comparison with an arbitrary right derived pushforward of all sheaves of modules. This is the commutative square of the source, up to the unique natural isomorphism whose inverse agrees with the derivation unit α on every homotopy complex of quasi-coherent modules, after the canonical termwise identifications.

public theorem affineDerivedPushforward_comparison {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsAffineHom f]
    (RF : DerivedCategory X.Modules ⥤ DerivedCategory Y.Modules)
    (α : (Scheme.Modules.pushforward f).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
        DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ RF)
    [RF.IsRightDerivedFunctor α
      (HomotopyCategory.quasiIso X.Modules (ComplexShape.up ℤ))] :
    let I : Scheme.QuasicoherentModules X ⥤ X.Modules :=
      (SheafOfModules.isQuasicoherent X.ringCatSheaf).ι
    let J : Scheme.QuasicoherentModules Y ⥤ Y.Modules :=
      (SheafOfModules.isQuasicoherent Y.ringCatSheaf).ι
    letI : I.Additive := CategoryTheory.Functor.fullSubcategoryInclusion_additive _
    letI : J.Additive := CategoryTheory.Functor.fullSubcategoryInclusion_additive _
    letI : PreservesFiniteLimits I :=
      Stacks.AlgebraicGeometry.QuasicoherentDerived.isQuasicoherent_ι_preservesFiniteLimits X
    letI : PreservesFiniteColimits I :=
      Stacks.AlgebraicGeometry.QuasicoherentDerived.isQuasicoherent_ι_preservesFiniteColimits X
    letI : PreservesFiniteLimits J :=
      Stacks.AlgebraicGeometry.QuasicoherentDerived.isQuasicoherent_ι_preservesFiniteLimits Y
    letI : PreservesFiniteColimits J :=
      Stacks.AlgebraicGeometry.QuasicoherentDerived.isQuasicoherent_ι_preservesFiniteColimits Y
    let F := quasicoherentPushforward f
    let G := Scheme.Modules.pushforward f
    ∃! e : (Stacks.AlgebraicGeometry.QuasicoherentDerived.derivedQuasicoherentComparison X ⋙
          affineRightDerivedPushforward f RF α) ≅
        (F.mapDerivedCategory ⋙
          Stacks.AlgebraicGeometry.QuasicoherentDerived.derivedQuasicoherentComparison Y),
      ∀ K : HomotopyCategory (Scheme.QuasicoherentModules X) (ComplexShape.up ℤ),
        (e.inv.app (DerivedCategory.Qh.obj K)).hom ≫
            RF.map (I.mapDerivedCategoryFactorsh.hom.app K) =
          J.mapDerivedCategory.map (F.mapDerivedCategoryFactorsh.hom.app K) ≫
            J.mapDerivedCategoryFactorsh.hom.app
              ((F.mapHomotopyCategory (ComplexShape.up ℤ)).obj K) ≫
            DerivedCategory.Qh.map
              ((Functor.mapHomotopyCategoryCompIso (Iso.refl (F ⋙ J))
                  (ComplexShape.up ℤ)).hom.app K ≫
                (Functor.mapHomotopyCategoryCompIso (Iso.refl (I ⋙ G))
                  (ComplexShape.up ℤ)).inv.app K) ≫
            α.app ((I.mapHomotopyCategory (ComplexShape.up ℤ)).obj K)

AlgebraicGeometry.affineRightDerivedPushforward_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/Coherator/AffineDerivedPushforwardQcoh.lean, line 52. The attribute's comment: “quasi-coherent cohomology of derived pushforward”.

Stacks Project, Tag 08D7. The derived direct image along an affine morphism of schemes takes a complex of 𝒪_X-modules with quasi-coherent cohomology to a complex of 𝒪_Y-modules with quasi-coherent cohomology.

public theorem affineRightDerivedPushforward_mem {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsAffineHom f]
    (RF : DerivedCategory X.Modules ⥤ DerivedCategory Y.Modules)
    (α : (Scheme.Modules.pushforward f).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
        DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ RF)
    [RF.IsRightDerivedFunctor α
      (HomotopyCategory.quasiIso X.Modules (ComplexShape.up ℤ))]
    (E : QuasicoherentDerivedCategory X) :
    (DerivedCategoryB.derivedCategoryB
      (SheafOfModules.isQuasicoherent Y.ringCatSheaf)) (RF.obj E.obj)

AlgebraicGeometry.affinePushforwardPreservesFiniteLimits, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/Coherator/AffinePushforwardExact.lean, line 62. The attribute's comment: “exactness, kernels”.

Stacks Project, Tag 08D7. Pushforward along an affine morphism preserves finite limits of quasi-coherent modules.

public instance affinePushforwardPreservesFiniteLimits {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsAffineHom f] : PreservesFiniteLimits (quasicoherentPushforward f)

AlgebraicGeometry.affinePushforwardPreservesFiniteColimits, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/Coherator/AffinePushforwardExact.lean, line 94. The attribute's comment: “exactness, cokernels”.

Stacks Project, Tag 08D7. Pushforward along an affine morphism preserves finite colimits of quasi-coherent modules.

public instance affinePushforwardPreservesFiniteColimits {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsAffineHom f] : PreservesFiniteColimits (quasicoherentPushforward f)

AlgebraicGeometry.isRightDerivedFunctor_quasicoherentPushforward_mapDerivedCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/Coherator/AffineDerivedPushforward.lean, line 203. The attribute's comment: “the derived functor”.

Pushforward along an affine morphism defines a derived functor D(QCoh(𝒪_X)) ⥤ D(QCoh(𝒪_Y)). This is the first assertion of [Stacks, Tag 08D7]: the functor induced on unbounded derived categories by the exact functor AlgebraicGeometry.quasicoherentPushforward, namely CategoryTheory.Functor.mapDerivedCategory, is a total right derived functor of it, so no resolutions are involved and the derived functor is computed by applying f_* to a representative complex.

The structure map is CategoryTheory.Functor.mapDerivedCategoryFactorsh.inv, which exhibits the induced functor as a lift through the localization DerivedCategory.Qh; a lift of a functor that inverts the quasi-isomorphisms is a right derived functor for the inverse of the lifting isomorphism.

public theorem isRightDerivedFunctor_quasicoherentPushforward_mapDerivedCategory
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsAffineHom f] :
    (quasicoherentPushforward f).mapDerivedCategory.IsRightDerivedFunctor
      (quasicoherentPushforward f).mapDerivedCategoryFactorsh.inv
      (HomotopyCategory.quasiIso (Scheme.QuasicoherentModules X) (ComplexShape.up ℤ))

AlgebraicGeometry.derivedQuasicoherentComparisonSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/Coherator/AffineDerivedPushforward.lean, line 316. The attribute's comment: “the commuting square”.

Stacks 08D7, the commuting square. For f : X ⟶ Y an affine morphism of schemes the square D(QCoh(𝒪_X)) ⟶ D_QCoh(𝒪_X) ⟶ D_QCoh(𝒪_Y), D(QCoh(𝒪_X)) ⟶ D(QCoh(𝒪_Y)) ⟶ D_QCoh(𝒪_Y) commutes: the comparison functor of [Stacks, Tag 06VT] carries the derived functor of direct image on quasi-coherent modules to the restriction of the unbounded derived direct image.

The two edges are compared after the fully faithful inclusion D_QCoh(𝒪_Y) ⥤ D(𝒪_Y), where the comparison functor becomes the derived inclusion (Stacks.AlgebraicGeometry.QuasicoherentDerived.derivedQuasicoherentComparisonCompι) and the square becomes AlgebraicGeometry.mapDerivedCategoryQuasicoherentPushforwardCompιIso, which is [Stacks, Tag 0G9N] for an affine morphism.

public def derivedQuasicoherentComparisonSquare {X Y : Scheme.{u}} (f : X ⟶ Y) [IsAffineHom f] :
    derivedQuasicoherentComparison.{u} X ⋙ derivedQuasicoherentPushforward f ≅
      (quasicoherentPushforward f).mapDerivedCategory ⋙ derivedQuasicoherentComparison.{u} Y

Tag 08D8, a lemma

Tag 08D8 in the Stacks Project.

AlgebraicGeometry.flatPushforwardCoheratorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/Coherator/FlatPushforward.lean, line 127.

Let f : X ⟶ Y be a quasi-compact, quasi-separated and flat morphism of schemes. Let Rf_* be a total right derived functor of pushforward of all modules, let RQ_X, RQ_Y be total right derived functors of the coherators, and let Φ be a total right derived functor of pushforward restricted to quasi-coherent modules. Then Rf_* ⋙ RQ_Y ≅ RQ_X ⋙ Φ.

public noncomputable def flatPushforwardCoheratorIso : Rf ⋙ RQY ≅ RQX ⋙ Φ

Tag 08D9, a lemma

Tag 08D9 in the Stacks Project.

Stacks.DerivedQCoh.coheratorSpecIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/AffineCoherator.lean, line 113. The attribute's comment: “part (1): the coherator on an affine scheme”.

[Stacks, Tag 08D9] part (1). On the affine scheme X = Spec R the coherator Q_X : Mod(𝒪_X) ⥤ QCoh(𝒪_X) sends a module F to the quasi-coherent module Γ(X, F)^~ attached to the R-module of global sections of F.

Both Q_X and Γ(X, -) ⋙ ~ are right adjoint to the inclusion of the quasi-coherent modules: for the second, compose the sheafification–sections adjunction ~ ⊣ Γ(X, -) with the equivalence Mod(R) ≌ QCoh(𝒪_X) of AlgebraicGeometry.tildeEquiv. A right adjoint is unique up to a unique natural isomorphism.

def coheratorSpecIso :
    coherator (Spec R) ≅ moduleSpecΓFunctor (R := R) ⋙ (tildeEquiv (R := R)).functor

Stacks.DerivedQCoh.derivedCoheratorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/AffineCoherator.lean, line 186. The attribute's comment: “part (2): the derived coherator”.

[Stacks, Tag 08D9] part (2). On the affine scheme X = Spec R the derived coherator RQ_X : D(𝒪_X) ⥤ D(QCoh(𝒪_X)) sends an object E to the complex of quasi-coherent modules attached to the object RΓ(X, E) of D(R).

Both sides are right derived functors of the two isomorphic functors of Stacks.DerivedQCoh.coheratorSpecIso: the right-hand side because derived sheafification D(R) ≌ D(QCoh(𝒪_X)) is an equivalence, hence a left adjoint, and postcomposing a right derived functor with a left adjoint again gives a right derived functor. A right derived functor is unique up to a unique natural isomorphism.

def derivedCoheratorIso :
    derivedCoherator R ≅
      derivedGlobalSectionsOver (𝟙 (Spec R)) ⋙ (derivedTildeEquiv R).functor

Stacks.DerivedQCoh.derivedCoheratorEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/AffineCoherator.lean, line 283. The attribute's comment: “part (3): quasi-inverse to the comparison functor”.

[Stacks, Tag 08D9] part (3). On the affine scheme X = Spec R the derived coherator, restricted to the complexes with quasi-coherent cohomology, is a quasi-inverse to the comparison functor D(QCoh(𝒪_X)) ⥤ D_QCoh(𝒪_X) of [Stacks, Tag 06VT]: the two are the two halves of an equivalence of categories.

The comparison functor is an equivalence by Stacks.DerivedQCoh.derivedQuasicoherentComparison_isEquivalence, and Stacks.DerivedQCoh.derivedCoheratorComparisonAdjunction exhibits the restricted derived coherator as its right adjoint; a right adjoint of an equivalence is its quasi-inverse.

def derivedCoheratorEquivalence :
    DerivedCategory (Scheme.QuasicoherentModules (Spec R)) ≌
      (DerivedCategoryB.derivedCategoryB (A := (Spec R).Modules)
        (SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf)).FullSubcategory

Tag 09T6, a lemma

Tag 09T6 in the Stacks Project.

Stacks.DerivedQCoh.derivedQuasicoherentComparison_isEquivalence_of_compatible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/AffineDiagonalEquivalence.lean, line 139. The attribute's comment: “equivalence clause”.

[Stacks, Tag 09T6], equivalence clause. Let X be a quasi-compact quasi-separated scheme satisfying Stacks.DerivedQCoh.AffineOpenPushforwardCompatible: for every affine open U ⊆ X the right derived functor Φ of j_* : QCoh(𝒪_U) ⥤ QCoh(𝒪_X) fits into the commutative square i_X ∘ Φ ≅ Rj_* ∘ i_U. Then the comparison functor i_X of [Stacks, Tag 06VT] is an equivalence.

The hypothesis names arbitrary models of the two derived functors; a total right derived functor is unique up to a unique natural isomorphism, so Stacks.DerivedQCoh.derivedPushforwardIsoOfCochainUnit and Stacks.DerivedQCoh.derivedQuasicoherentPushforwardIsoOfCochainUnit move the square to the chosen models, where Stacks.DerivedQCoh.derivedQuasicoherentComparison_isEquivalence_of_square runs the dévissage of the source on the derived coherator Stacks.DerivedQCoh.coheratorDerivedAdjunction.

theorem derivedQuasicoherentComparison_isEquivalence_of_compatible (X : Scheme.{u})
    [CompactSpace X] [QuasiSeparatedSpace X]
    (h : AffineOpenPushforwardCompatible.{u, u} X) :
    (derivedQuasicoherentComparison.{u} X).IsEquivalence

Stacks.DerivedQCoh.derivedQuasicoherentComparison_isEquivalence_of_affineOpenCompatible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/CoheratorEquivalence.lean, line 617. The attribute's comment: “equivalence”.

[Stacks, Tag 09T6], the equivalence. Let X be a quasi-compact quasi-separated scheme for which the right derived functor of direct image of quasi-coherent modules from every affine open fits into the commutative square of Stacks.DerivedQCoh.AffineOpenPushforwardCompatible. Then the comparison functor i_X : D(QCoh(𝒪_X)) ⥤ D_QCoh(𝒪_X) of [Stacks, Tag 06VT] is an equivalence.

The proof is the source's induction. The comparison functor is left adjoint to the derived coherator restricted to the complexes with quasi-coherent cohomology, and it is conservative, so it suffices to see that the counit of the adjunction ι_* ⊣ RQ_X is invertible at every complex with quasi-coherent cohomology. The counit is a natural transformation of exact functors of triangulated categories, hence invertible at the first vertex of a distinguished triangle as soon as it is invertible at the other two, and it is invertible at a zero object; so it suffices to produce, for a complex E with quasi-coherent cohomology supported on a closed set S and an affine open U, a distinguished triangle on E whose second vertex has invertible counit and whose third vertex again has quasi-coherent cohomology but is supported on S \ U. Finitely many affine opens cover X, so the support is exhausted. The triangle is the recollement triangle E ⟶ Rj_*(E|_U) ⟶ C: its second vertex has invertible counit by Stacks.DerivedQCoh.isIso_coheratorCounit_derivedPushforward, which is where the commutative square of the hypothesis and the equivalence on the affine open U are used, and its third vertex is supported on S \ U because E ⟶ Rj_*(E|_U) becomes invertible on U.

theorem derivedQuasicoherentComparison_isEquivalence_of_affineOpenCompatible
    (X : Scheme.{u}) [CompactSpace X] [QuasiSeparatedSpace X]
    (hcompat : AffineOpenPushforwardCompatible.{u + 1} X) :
    (derivedQuasicoherentComparison.{u + 1} X).IsEquivalence

Stacks.DerivedQCoh.derivedCoherator_isoInv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/CoheratorQuasiInverse.lean, line 361. The attribute's comment: “quasi-inverse clause, given the equivalence”.

[Stacks, Tag 09T6], quasi-inverse clause. Let X be a scheme whose comparison functor i_X : D(QCoh(𝒪_X)) ⥤ D_QCoh(𝒪_X) of [Stacks, Tag 06VT] is an equivalence, and let RQ_X be any total right derived functor of the coherator Q_X. Then the quasi-inverse of i_X is RQ_X restricted to the complexes with quasi-coherent cohomology.

Stacks.DerivedQCoh.comparisonDerivedCoheratorAdjunction exhibits that restriction as a right adjoint of i_X, the inverse of an equivalence is another, and a right adjoint is unique up to a unique natural isomorphism.

This is the second clause of the conclusion of [Stacks, Tag 09T6], deduced from the first clause rather than from the tag's affine-open hypothesis Stacks.DerivedQCoh.AffineOpenPushforwardCompatible; the first clause — that the comparison functor is an equivalence — is the source's induction on the number of affine opens covering the support, and is not proved here.

def derivedCoherator_isoInv [(derivedQuasicoherentComparison.{w} X).IsEquivalence] :
    (DerivedCategoryB.derivedCategoryB
        (SheafOfModules.isQuasicoherent X.ringCatSheaf)).ι ⋙ RQ ≅
      (derivedQuasicoherentComparison.{w} X).inv

Tag 08DB, a proposition

Tag 08DB in the Stacks Project.

Stacks.AmpleNonvanishing.exists_quasicoherentComplex_iso_of_isAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleNonvanishing/AmpleAffineDiagonal.lean, line 93. The attribute's comment: “on a scheme carrying an ample invertible module, which is the form Tag 0BQR consumes: quasi-compactness and the affine diagonal both come from ampleness”.

[Stacks, Tag 08DB] at the hypotheses of [Stacks, Tag 0BQR]. On a scheme carrying an ample invertible 𝒪_X-module every object K of D_QCoh(𝒪_X) is isomorphic in D(𝒪_X) to the class of a cochain complex G of quasi-coherent 𝒪_X-modules.

This is Stacks.AmpleNonvanishing.exists_quasicoherentComplex_iso with its two hypotheses — X quasi-compact and X of affine diagonal — supplied by ampleness, which is the first line of the proof of [Stacks, Tag 0BQR]. No hypothesis beyond the tag's is used.

theorem exists_quasicoherentComplex_iso_of_isAmple (X : Scheme.{u}) (L : X.Modules)
    [IsInvertibleModule X L] (hL : IsAmple X L)
    (K : (DerivedCategoryB.derivedCategoryB
      (SheafOfModules.isQuasicoherent X.ringCatSheaf)).FullSubcategory) :
    ∃ G : CochainComplex
        (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory ℤ,
      Nonempty (K.1 ≅ DerivedCategory.Q.obj
        (((SheafOfModules.isQuasicoherent X.ringCatSheaf).ι.mapHomologicalComplex
          (ComplexShape.up ℤ)).obj G))

Stacks.DerivedQCoh.derivedQuasicoherentComparison_isEquivalence_of_affineDiagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/AffineDiagonalEquivalence.lean, line 164. The attribute's comment: “equivalence”.

[Stacks, Tag 08DB]. Let X be a quasi-compact scheme with affine diagonal. Then the comparison functor i_X : D(QCoh(𝒪_X)) ⥤ D_QCoh(𝒪_X) of [Stacks, Tag 06VT] is an equivalence.

A scheme with affine diagonal is quasi-separated, and the inclusion of one of its affine opens is an affine morphism, so the square of [Stacks, Tag 09T6] is the square of [Stacks, Tag 08D7]; that is Stacks.DerivedQCoh.affineOpenPushforwardCompatible, which discharges the hypothesis of Stacks.DerivedQCoh.derivedQuasicoherentComparison_isEquivalence_of_compatible.

theorem derivedQuasicoherentComparison_isEquivalence_of_affineDiagonal (X : Scheme.{u})
    [CompactSpace X] [IsAffineHom (pullback.diagonal (terminal.from X))] :
    (derivedQuasicoherentComparison.{u} X).IsEquivalence

Stacks.DerivedQCoh.derivedCoherator_isoInv_of_affineDiagonal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/AffineDiagonalEquivalence.lean, line 181. The attribute's comment: “quasi-inverse”.

[Stacks, Tag 08DB], the quasi-inverse. On a quasi-compact scheme with affine diagonal the quasi-inverse of the comparison functor of [Stacks, Tag 06VT] is the derived coherator RQ_X, restricted to the complexes with quasi-coherent cohomology.

The comparison functor is an equivalence by Stacks.DerivedQCoh.derivedQuasicoherentComparison_isEquivalence_of_affineDiagonal, and Stacks.DerivedQCoh.derivedCoherator_isoInv — the quasi-inverse clause of [Stacks, Tag 09T6] — identifies the inverse of an equivalent comparison functor with any total right derived functor of the coherator, here Stacks.DerivedQCoh.derivedCoheratorOfScheme.

def derivedCoherator_isoInv_of_affineDiagonal (X : Scheme.{u})
    [CompactSpace X] [IsAffineHom (pullback.diagonal (terminal.from X))] :
    letI := derivedQuasicoherentComparison_isEquivalence_of_affineDiagonal X
    (DerivedCategoryB.derivedCategoryB
        (SheafOfModules.isQuasicoherent X.ringCatSheaf)).ι ⋙ derivedCoheratorOfScheme X ≅
      (derivedQuasicoherentComparison.{u} X).inv

Tag 0CRX, a lemma

Tag 0CRX in the Stacks Project.

AlgebraicGeometry.isIso_derivedPushforwardComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/Coherator/DirectImageCoherator.lean, line 335. The attribute's comment: “the canonical map Φ(K) ⟶ Rf_*(K) is an isomorphism for every K”.

The canonical map Φ(K) ⟶ Rf_*(K) is an isomorphism for every K. This is the content of [Stacks, Tag 0CRX]. Both functors are triangulated — Φ and Rf_* because they are right derived functors on Grothendieck abelian categories (Stacks.DerivedAcyclic.isTriangulated_of_isRightDerivedFunctor), and the derived inclusions because the inclusions are exact — so the dévissage Stacks.DerivedQCoh.isIso_natTrans_of_isIso_app_quasicoherentPushforward reduces the claim to complexes pushed forward from an affine open, where it is AlgebraicGeometry.isIso_derivedPushforwardComparison_app_quasicoherentPushforward.

theorem isIso_derivedPushforwardComparison : IsIso (derivedPushforwardComparison f Φ ηΦ)

AlgebraicGeometry.derivedQuasicoherentComparisonSquareOfAffineDiagonal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/Coherator/DirectImageCoherator.lean, line 378. The attribute's comment: “the commuting square, for any right derived functor (Φ, ηΦ) of f_*”.

The square for quasi-compact schemes with affine diagonal. Let f : X ⟶ Y be a morphism of schemes, with X and Y quasi-compact with affine diagonal, and let Φ, with derivation unit ηΦ, be a total right derived functor of f_* : QCoh(𝒪_X) ⥤ QCoh(𝒪_Y). Then the square

D(QCoh(𝒪_X)) --i_X--> D_QCoh(𝒪_X)
     | Φ                  | Rf_*
     v                     v
D(QCoh(𝒪_Y)) --i_Y--> D_QCoh(𝒪_Y)

commutes, the horizontal arrows being the comparison functors of [Stacks, Tag 06VT] and the right edge the restriction AlgebraicGeometry.affineDiagonalDerivedQuasicoherentPushforward of the unbounded derived direct image.

The isomorphism is the canonical one: after the fully faithful inclusion of D_QCoh(𝒪_Y) it is AlgebraicGeometry.derivedPushforwardComparison, the map Φ(K) ⟶ Rf_*(K) induced by f_* ⟶ Rf_*, which is invertible by AlgebraicGeometry.isIso_derivedPushforwardComparison.

def derivedQuasicoherentComparisonSquareOfAffineDiagonal :
    derivedQuasicoherentComparison.{u} X ⋙ affineDiagonalDerivedQuasicoherentPushforward f ≅
      Φ ⋙ derivedQuasicoherentComparison.{u} Y

Tag 0CRY, a remark

Tag 0CRY in the Stacks Project.

AlgebraicGeometry.exists_injective_quasicoherentSections_rightDerived_ne_cohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/Coherator/DirectImageCoheratorWarning.lean, line 57. The attribute's comment: “R^1_QCoh Γ(U, ℱ) = 0 while H^1(U, ℱ) ≠ 0, for ℱ injective in QCoh(𝒪_{Spec A})”.

On an affine scheme the comparison from derived sections computed inside QCoh(𝒪_X) to sheaf cohomology is not an isomorphism. There are a ring A, an injective object ℱ of QCoh(𝒪_{Spec A}) and a quasi-compact open U ⊆ Spec A with R^1_{QCoh}Γ(U, ℱ) = 0 and H^1(U, ℱ) ≠ 0; in particular no morphism from the first group to the second is an isomorphism, so the canonical t^1 is not one.

theorem exists_injective_quasicoherentSections_rightDerived_ne_cohomology :
    ∃ (A : CommRingCat.{u})
      (F : (SheafOfModules.isQuasicoherent (Spec A).ringCatSheaf).FullSubcategory)
      (U : (Spec A).Opens),
      Injective F ∧ IsCompact (U : Set (Spec A)) ∧
        IsZero (((quasicoherentSections (Spec A) U).rightDerived 1).obj F) ∧
        ¬ IsZero (Hgroup (Spec A).ringCatSheaf U 1
            ((SheafOfModules.isQuasicoherent (Spec A).ringCatSheaf).ι.obj F)) ∧
        ∀ t : ((quasicoherentSections (Spec A) U).rightDerived 1).obj F ⟶
            Hgroup (Spec A).ringCatSheaf U 1
              ((SheafOfModules.isQuasicoherent (Spec A).ringCatSheaf).ι.obj F),
          ¬ IsIso t

Sources

• Section 36.7, Tag 08D6
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.affineDerivedPushforward_comparison · AlgebraicGeometry.affineRightDerivedPushforward_mem · AlgebraicGeometry.affinePushforwardPreservesFiniteLimits · AlgebraicGeometry.affinePushforwardPreservesFiniteColimits · AlgebraicGeometry.isRightDerivedFunctor_quasicoherentPushforward_mapDerivedCategory · AlgebraicGeometry.derivedQuasicoherentComparisonSquare · AlgebraicGeometry.flatPushforwardCoheratorIso · Stacks.DerivedQCoh.coheratorSpecIso

Section36.8 The coherator for Noetherian schemes#

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

Tag 09T2, a lemma

Tag 09T2 in the Stacks Project.

AlgebraicGeometry.isFlasque_of_injective_quasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/InjectiveQcoh/SectionExtension.lean, line 373.

Let X be a Noetherian scheme and let 𝒥 be an injective object of the category of quasi-coherent 𝒪_X-modules. Then 𝒥 is a flasque sheaf of 𝒪_X-modules.

public theorem isFlasque_of_injective_quasicoherent (X : Scheme.{u}) [IsNoetherian X]
    (J : (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory) [Injective J] :
    TopCat.Sheaf.IsFlasque ((SheafOfModules.toSheaf X.ringCatSheaf).obj J.obj)

Tag 09T3, a lemma

Tag 09T3 in the Stacks Project.

AlgebraicGeometry.noetherianPushforwardExtension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/NoetherianExtension/Basic.lean, line 138.

The right derived extension Φ : D(QCoh(𝒪_X)) ⥤ D(QCoh(𝒪_Y)) of direct image on quasi-coherent modules, for a morphism of Noetherian schemes: the total right derived functor of termwise direct image.

This is the functor of [Stacks, Tag 09T3]; the compatibility with derived direct image that the source asserts of it is AlgebraicGeometry.noetherianPushforwardExtensionComparison.

def noetherianPushforwardExtension {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsNoetherian X] [IsNoetherian Y] :
    DerivedCategory (Scheme.QuasicoherentModules X) ⥤
      DerivedCategory (Scheme.QuasicoherentModules Y)

AlgebraicGeometry.noetherianPushforwardExtension_isRightDerivedFunctor, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/NoetherianExtension/Basic.lean, line 159.

AlgebraicGeometry.noetherianPushforwardExtension is a total right derived functor of direct image on quasi-coherent modules, with AlgebraicGeometry.noetherianPushforwardExtensionUnit as its derivation unit.

instance noetherianPushforwardExtension_isRightDerivedFunctor {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsNoetherian X] [IsNoetherian Y] :
    (noetherianPushforwardExtension f).IsRightDerivedFunctor
      (noetherianPushforwardExtensionUnit f)
      (HomotopyCategory.quasiIso (Scheme.QuasicoherentModules X) (ComplexShape.up ℤ))

AlgebraicGeometry.noetherianPushforwardExtensionComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/NoetherianExtension/Basic.lean, line 248.

The commuting square of [Stacks, Tag 09T3]. For a morphism of Noetherian schemes the derived extension of direct image on quasi-coherent modules agrees, under the comparison functors D(QCoh(𝒪_•)) ⥤ D_QCoh(𝒪_•), with any right derived direct image of all modules.

The isomorphism is the canonical one: both composites are right derived functors of the single functor K(QCoh(𝒪_X)) ⥤ D(𝒪_Y) given by termwise direct image followed by forgetting quasi-coherence, so they are identified by the uniqueness of right derived functors.

def noetherianPushforwardExtensionComparison :
    derivedQuasicoherentComparison X ⋙
        (DerivedCategoryB.derivedCategoryB
          (SheafOfModules.isQuasicoherent X.ringCatSheaf)).ι ⋙ RF ≅
      noetherianPushforwardExtension f ⋙ derivedQuasicoherentComparison Y ⋙
        (DerivedCategoryB.derivedCategoryB
          (SheafOfModules.isQuasicoherent Y.ringCatSheaf)).ι

Tag 09T4, a proposition

Tag 09T4 in the Stacks Project.

Stacks.DerivedQCoh.derivedQuasicoherentComparison_isEquivalence_of_isNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/NoetherianExtension/Equivalence.lean, line 124. The attribute's comment: “equivalence”.

On a Noetherian scheme the comparison functor i_X : D(QCoh(𝒪_X)) ⥤ D_QCoh(𝒪_X) of [Stacks, Tag 06VT] is an equivalence.

theorem derivedQuasicoherentComparison_isEquivalence_of_isNoetherian (X : Scheme.{u})
    [IsNoetherian X] : (derivedQuasicoherentComparison.{u + 1} X).IsEquivalence

Stacks.DerivedQCoh.derivedCoherator_isoInv_of_isNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/NoetherianExtension/Equivalence.lean, line 133. The attribute's comment: “identification of the quasi-inverse”.

On a Noetherian scheme the quasi-inverse of the comparison functor of [Stacks, Tag 06VT] is RQ_X: any total right derived functor of the coherator Q_X : Mod(𝒪_X) ⥤ QCoh(𝒪_X) of [Stacks, Tag 077P], restricted to the complexes with quasi-coherent cohomology.

theorem derivedCoherator_isoInv_of_isNoetherian (X : Scheme.{u}) [IsNoetherian X]
    (RQ : DerivedCategory (SheafOfModules.{u} X.ringCatSheaf) ⥤
      DerivedCategory (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory)
    (RQUnit : (modulesCoherator X).mapHomologicalComplex (ComplexShape.up ℤ) ⋙
        DerivedCategory.Q
          (C := (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory) ⟶
      DerivedCategory.Q (C := SheafOfModules.{u} X.ringCatSheaf) ⋙ RQ)
    [RQ.IsRightDerivedFunctor RQUnit
      (HomologicalComplex.quasiIso (SheafOfModules.{u} X.ringCatSheaf) (ComplexShape.up ℤ))] :
    letI := derivedQuasicoherentComparison_isEquivalence_of_isNoetherian X
    Nonempty ((DerivedCategoryB.derivedCategoryB
        (SheafOfModules.isQuasicoherent X.ringCatSheaf)).ι ⋙ RQ ≅
      (derivedQuasicoherentComparison.{u + 1} X).inv)

Stacks.DerivedQCoh.derivedCoherator_isoInv_of_isNoetherian', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/NoetherianExtension/Equivalence.lean, line 153. The attribute's comment: “identification of the quasi-inverse”.

On a Noetherian scheme the quasi-inverse of the comparison functor of [Stacks, Tag 06VT] is the restriction of the total right derived functor Stacks.DerivedQCoh.schemeDerivedCoherator of the coherator to the complexes with quasi-coherent cohomology.

theorem derivedCoherator_isoInv_of_isNoetherian' (X : Scheme.{u}) [IsNoetherian X] :
    letI := derivedQuasicoherentComparison_isEquivalence_of_isNoetherian X
    Nonempty ((DerivedCategoryB.derivedCategoryB
        (SheafOfModules.isQuasicoherent X.ringCatSheaf)).ι ⋙ schemeDerivedCoherator.{u + 1} X ≅
      (derivedQuasicoherentComparison.{u + 1} X).inv)

Sources

• Section 36.8, Tag 09T1
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.isFlasque_of_injective_quasicoherent · AlgebraicGeometry.noetherianPushforwardExtension · AlgebraicGeometry.noetherianPushforwardExtension_isRightDerivedFunctor · AlgebraicGeometry.noetherianPushforwardExtensionComparison · Stacks.DerivedQCoh.derivedQuasicoherentComparison_isEquivalence_of_isNoetherian · Stacks.DerivedQCoh.derivedCoherator_isoInv_of_isNoetherian · Stacks.DerivedQCoh.derivedCoherator_isoInv_of_isNoetherian'

Section36.9 Koszul complexes#

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

Tag 08CY, an equation

Tag 08CY in the Stacks Project.

Koszul.koszulIdealComplexSystem, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/Koszul.lean, line 91.

The canonical inverse system I^•(f) ← I^•(f²) ← I^•(f³) ← ⋯.

noncomputable def koszulIdealComplexSystem {r : ℕ} (f : Fin r → A) :
    KoszulIdealComplexSystem f

Tag 08CZ, a situation

Tag 08CZ in the Stacks Project.

Koszul.CechSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Koszul/Situation.lean, line 57.

Stacks Project, Tag 08CZ. The standing situation of the section on Koszul complexes: a commutative ring A and a finite sequence f₁, …, f_r of elements of A. The affine scheme X = Spec(A), the open U = D(f₁) ∪ ⋯ ∪ D(f_r) and the covering 𝒰 of U by the standard opens D(fᵢ) are derived from these data.

structure CechSituation

Tag 08D0, a lemma

Tag 08D0 in the Stacks Project.

Koszul.alternatingCechComplexIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Koszul/AlternatingCechColimit.lean, line 894. References: EGA III (2.1.2), “special case”.

Stacks Project, Tag 08D0. The canonical identification between the colimit of the contragredient Koszul complexes and the alternating Čech complex of M^~.

noncomputable def alternatingCechComplexIso {r : ℕ} (f : Fin r → A) (M : ModuleCat.{v} A) :
    colimit (koszulHomDiagram f M) ≅ moduleAlternatingCechComplex f M

Koszul.alternatingCechComplexIso_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Koszul/AlternatingCechColimit.lean, line 908.

Stacks Project, Tag 08D0. The identification is natural in the module.

theorem alternatingCechComplexIso_naturality {r : ℕ} (f : Fin r → A)
    (M N : ModuleCat.{v} A) (g : M ⟶ N) :
    (alternatingCechComplexIso f M).hom ≫ moduleAlternatingCechMap f g =
      koszulHomColimitMap f g ≫ (alternatingCechComplexIso f N).hom

Koszul.alternatingCechComplexIso_ι_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Koszul/AlternatingCechColimit.lean, line 924.

Stacks Project, Tag 08D0. On the stage-e linear form t the identification takes the value (-1)^p t([i₀, …, iₚ]) / ∏ⱼ f(iⱼ)^(e+1) at the tuple i.

theorem alternatingCechComplexIso_ι_apply {r : ℕ} (f : Fin r → A) (M : ModuleCat.{v} A)
    (e p : ℕ) (t : (koszulIdealComplexPower f e).X p →ₗ[A] M) (i : Fin (p + 1) → Fin r) :
    (((colimit.ι (koszulHomDiagram f M) e ≫
        (alternatingCechComplexIso f M).hom).f p) t).1 i =
      koszulCechFraction f M e p t i

Tag 08D1, a lemma

Tag 08D1 in the Stacks Project.

Koszul.koszulHomColimitIsoAlternatingCechTotal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Koszul/AlternatingCechTotal.lean, line 929.

Stacks Project, Tag 08D1. The filtered colimit of the Hom complexes from the powers of the truncated Koszul complex is canonically isomorphic to the total alternating Čech complex of the associated sheaf complex, naturally in the coefficient complex.

noncomputable def koszulHomColimitIsoAlternatingCechTotal
    {A : Type u} [CommRing A] {r : ℕ} (f : Fin r → A) :
    koszulHomColimitFunctor f ⋙
        (forget₂ (ModuleCat.{u} A) AddCommGrpCat.{u}).mapHomologicalComplex (up ℤ) ≅
      alternatingCechTotalFunctor f

Tag 08D2, a lemma

Tag 08D2 in the Stacks Project.

Koszul.CechSituation.isIso_linearAlternatingCechToDerivedComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Koszul/AlternatingCechComputesCohomology.lean, line 164. The attribute's comment: “the canonical map in D(A) is an isomorphism”.

Stacks Project, Tag 08D2. In the situation of [Stacks, Tag 08CZ], for a complex F^• of quasi-coherent 𝒪_U-modules the comparison map Tot(Č_alt^•(𝒰, F^•)) ⟶ RΓ(U, F^•) of [Stacks, Tag 08C1], taken in D(A), is an isomorphism.

theorem isIso_linearAlternatingCechToDerivedComparison (F : CochainComplex S.scheme.Modules ℤ)
    (hF : ∀ n, (F.X n).IsQuasicoherent) :
    IsIso ((Stacks.Cech.linearAlternatingCechToDerivedComparison (TopCat.of S.scheme)
      S.scheme.ringCatSheaf S.baseCenter S.coverUlift S.iSup_coverUlift).app F)

Koszul.CechSituation.alternatingCechTotalNatIsoDerivedSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Koszul/AlternatingCechComputesCohomology.lean, line 179. The attribute's comment: “the isomorphism in D(A), functorial in F^•”.

Stacks Project, Tag 08D2. In the situation of [Stacks, Tag 08CZ], the canonical isomorphism Tot(Č_alt^•(𝒰, F^•)) ≅ RΓ(U, F^•) in D(A), natural in the complex F^• of quasi-coherent 𝒪_U-modules: its components are the comparison maps of [Stacks, Tag 08C1].

def alternatingCechTotalNatIsoDerivedSections :
    S.QuasicoherentComplex.ι ⋙
        Stacks.Cech.linearAlternatingCechDerivedFunctor (TopCat.of S.scheme)
          S.scheme.ringCatSheaf S.baseCenter S.coverUlift ≅
      S.QuasicoherentComplex.ι ⋙
        Stacks.Cech.linearUnboundedDerivedGlobalSectionsFunctor (TopCat.of S.scheme)
          S.scheme.ringCatSheaf S.baseCenter

Koszul.DerivedSystem.isIso_alternatingCechToDerivedComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/KoszulCechComputesSections.lean, line 160. The attribute's comment: “the comparison map is an isomorphism, in D(Ab)”.

Stacks Project, Tag 08D2, in D(Ab). In Situation 08CZ, the comparison map Tot(Č_alt(𝒰, ℱ^•)) ⟶ RΓ(U, ℱ^•) of Tag 08C1 for the covering 𝒰 of U by the basic opens D(fᵢ) is an isomorphism in D(Ab) for every complex ℱ^• of quasi-coherent 𝒪_U-modules.

public theorem isIso_alternatingCechToDerivedComparison (f : Fin r → A)
    (K : CochainComplex (SheafOfModules.{u} (unionRingSheaf f)) ℤ)
    (hK : ∀ n : ℤ, (K.X n).IsQuasicoherent) :
    IsIso ((Stacks.Cech.alternatingCechToDerivedComparison (unionSpace f)
      (unionRingSheaf f) (unionSpaceCover f) (iSup_unionSpaceCover f)).app K)

Tag 08DC, an equation

Tag 08DC in the Stacks Project.

Koszul.DerivedSystem.cohomologyComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/KoszulCohomologyComparison.lean, line 358.

The comparison map of Stacks 08DC. For every object E of D(𝒪_X) the maps Iₑ → 𝒪_X, which become isomorphisms after restriction to U = D(f₁) ∪ ⋯ ∪ D(f_r), induce a canonical homomorphism

colimₑ Hom_{D(𝒪_X)}(Iₑ, E) ⟶ H⁰(U, E),

sending the class of α : Iₑ → E to the restriction of α to U precomposed with the inverse of the restriction of Iₑ → 𝒪_X, read as a degree-zero hypercohomology class over U.

public def cohomologyComparison (f : Fin r → A) (E : derivedCat A) :
    ↥(colimit (homGroupSystem f E)) →+ ↥((sectionsOnUnion f).obj E)

Tag 08DD, a proposition

Tag 08DD in the Stacks Project.

Koszul.DerivedSystem.cohomologyComparison_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/KoszulCohomologyComparisonBijective.lean, line 360.

Stacks 08DD. In the situation of [Stacks, Tag 08CZ] — A a commutative ring, f a finite sequence in A, X = Spec A and U = D(f₁) ∪ ⋯ ∪ D(f_r) — the comparison map of [Stacks, Tag 08DC]

colimₑ Hom_{D(𝒪_X)}(Iₑ, E) ⟶ H⁰(U, E)

is an isomorphism for every object E of D_QCoh(𝒪_X).

public theorem cohomologyComparison_bijective (E : derivedCat A)
    (hE : Stacks.DerivedQCoh.IsDQCoh (R := (Spec A).ringCatSheaf) E) :
    Function.Bijective (cohomologyComparison f E)

Tag 08E3, a lemma

Tag 08E3 in the Stacks Project.

AdicKoszul.exists_koszulPower_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/Coherator/KoszulPowerLift.lean, line 577.

A degree-zero class of a quasi-coherent complex on Spec A, supported on the closed complement of a union of r basic opens in the indicated range, comes from a Koszul complex on powers of the defining equations.

public theorem exists_koszulPower_lift {A : Type u} [CommRing A] {r : ℕ}
    (f : Fin r → A) (E : DerivedCategory (ModuleCat.{u} A))
    (hE : ∀ i : Fin r, ∀ n : ℤ, -(r : ℤ) + 1 ≤ n → n ≤ 0 →
      ∀ x : (DerivedCategory.homologyFunctor (ModuleCat.{u} A) n).obj E,
        ∃ k : ℕ, f i ^ k • x = 0)
    (s : DerivedCategory.Q.obj
      (((CochainComplex.singleFunctors (ModuleCat.{u} A)).functor 0).obj
        (ModuleCat.of A A)) ⟶ E) :
    ∃ e : ℕ, ∃ t : (AdicKoszul.canonicalKoszulPowerSystem f).obj ⟨e⟩ ⟶ E,
      s = DerivedCategory.Q.map (AdicKoszul.koszulPowerUnit f e) ≫ t

Stacks.Koszul.PowerLift.exists_koszulPower_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/PowerLift/KoszulPowerLift.lean, line 553.

[Stacks, Tag 08E3] over a ring, with the target read as a term of the canonical Koszul power system AdicKoszul.canonicalKoszulPowerSystem. That system is defined at CategoryTheory.HasDerivedCategory.standard, so this form of the statement is available only at that model; Stacks.Koszul.PowerLift.exists_koszulPower_lift_koszulCochain is the same result at an arbitrary one.

public theorem exists_koszulPower_lift {r : ℕ} (f : Fin r → A)
    (E : DerivedCategory (ModuleCat.{u} A))
    (hE : ∀ i : Fin r, ∀ n : ℤ, -(r : ℤ) + 1 ≤ n → n ≤ 0 →
      ∀ x : (DerivedCategory.homologyFunctor (ModuleCat.{u} A) n).obj E,
        ∃ k : ℕ, f i ^ k • x = 0)
    (s : DerivedCategory.Q.obj
      (((CochainComplex.singleFunctors (ModuleCat.{u} A)).functor 0).obj
        (ModuleCat.of A A)) ⟶ E) :
    ∃ e : ℕ, ∃ t : (AdicKoszul.canonicalKoszulPowerSystem f).obj ⟨e⟩ ⟶ E,
      s = DerivedCategory.Q.map (AdicKoszul.koszulPowerUnit f e) ≫ t

Sources

• Section 36.9, Tag 08CX
• AxiomMath/Stacks at 5ed82d14

LeanKoszul.koszulIdealComplexSystem · Koszul.CechSituation · Koszul.alternatingCechComplexIso · Koszul.alternatingCechComplexIso_naturality · Koszul.alternatingCechComplexIso_ι_apply · Koszul.koszulHomColimitIsoAlternatingCechTotal · Koszul.CechSituation.isIso_linearAlternatingCechToDerivedComparison · Koszul.CechSituation.alternatingCechTotalNatIsoDerivedSections

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.