36.22 Cohomology and base… to 36.29 Limits and derived…

Section36.22 Cohomology and base change, IV #

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

Tag 08EU, a lemma

Tag 08EU in the Stacks Project.

Stacks.Cohomology.DerivedProjectionFormula.isIso_projectionFormulaMap_of_openCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/ProjectionFormulaOpenCoverDescent.lean, line 111. The attribute's comment: “the localization argument of the source's proof, closed over an open cover: for an arbitrary morphism of schemes and arbitrary complexes, invertibility of the projection-formula map for f|_U at the restricted complexes, for U running through an open cover of the base, implies invertibility of the map for f; the affine case of the tag is NOT proved here, so the tag is not closed”.

The projection-formula morphism of [Stacks, Tag 0B53] is invertible as soon as it is after restriction to the members of an open cover of the base.

For an arbitrary morphism of schemes f : X ⟶ Y, arbitrary E ∈ D(𝒪_X) and K ∈ D(𝒪_Y), and a family of opens U i covering Y: if the projection-formula map for the restricted morphism f|_{U_i} : f^{-1}U_i ⟶ U_i at the restricted complexes Lg_i'^*E and Lg_i^*K is invertible for every i, then the projection-formula map for f at E and K is invertible.

This is the localization argument of the proof of [Stacks, Tag 08EU], over an open cover of the base.

theorem isIso_projectionFormulaMap_of_openCover {ι : Type*} (U : ι → Y.Opens)
    (hU : ∀ y : Y, ∃ i, y ∈ U i)
    (E : DerivedCategory (SheafOfModules.{u} (structureSheafRing X.toRingedSpace)))
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing Y.toRingedSpace)))
    (h : ∀ i, IsIso (projectionFormulaMap (f ∣_ U i).toLRSHom.toShHom
      ((derivedPullback (f ⁻¹ᵁ U i).ι.toLRSHom.toShHom).obj E)
      ((derivedPullback (U i).ι.toLRSHom.toShHom).obj K))) :
    IsIso (projectionFormulaMap f.toLRSHom.toShHom E K)

Stacks.Cohomology.DerivedProjectionFormula.isIso_derivedPullback_map_projectionFormulaMap_of_isOpenImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/ProjectionFormulaOpenImmersionBaseChange.lean, line 262. The attribute's comment: “the localization step of the source's proof, for schemes: for a Cartesian square of schemes whose bottom arrow is an open immersion, invertibility of the projection-formula map for f' at the restricted complexes implies invertibility of the derived pullback along g of the map for f; unconditional in both complexes, but only one implication of the source's reduction — the affine case and the descent from an open cover back to the base are not proved”.

Invertibility of the derived projection-formula map of [Stacks, Tag 0B53] descends along an open immersion of the base, for schemes.

For a Cartesian square of schemes whose bottom arrow g is an open immersion, the derived pullback along g of the projection-formula map for f is invertible as soon as the map for f' at the restricted complexes is.

The other horizontal arrow g' is then an open immersion too, being a base change of g, and the square stays Cartesian in ringed spaces by Stacks.Cohomology.DerivedBaseChange.isPullback_toShHom_of_isOpenImmersion, so Stacks.Cohomology.ProjectionFormulaPerfect.isIso_derivedPullback_map_projectionFormulaMap applies. This is the form the source's localization argument is run in: it replaces the base Y by an open V ⊆ Y and X by its preimage.

theorem isIso_derivedPullback_map_projectionFormulaMap_of_isOpenImmersion
    [AlgebraicGeometry.IsOpenImmersion g] (sq : IsPullback g' f' f g)
    (E : DerivedCategory (SheafOfModules.{u} (structureSheafRing X.toRingedSpace)))
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing Y.toRingedSpace)))
    (h : IsIso (projectionFormulaMap f'.toLRSHom.toShHom
      ((derivedPullback g'.toLRSHom.toShHom).obj E)
      ((derivedPullback g.toLRSHom.toShHom).obj K))) :
    IsIso ((derivedPullback g.toLRSHom.toShHom).map
      (projectionFormulaMap f.toLRSHom.toShHom E K))

AlgebraicGeometry.projectionFormulaIsIsoOnQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedVarieties/FourierMukai/ProjectionFormulaDischarged.lean, line 46. The attribute's comment: “the whole tag, in the shape of the proposition AlgebraicGeometry.ProjectionFormulaIsIsoOnQuasicoherent, which this proves”.

[Stacks, Tag 08EU]. Let f : X ⟶ Y be a quasi-compact and quasi-separated morphism of schemes. For E in D_QCoh(𝒪_X) and K in D_QCoh(𝒪_Y) the projection-formula morphism of [Stacks, Tag 0B53]

R f_* E ⊗^𝐋_{𝒪_Y} K ⟶ R f_*(E ⊗^𝐋_{𝒪_X} L f^* K)

is an isomorphism; that is, AlgebraicGeometry.ProjectionFormulaIsIsoOnQuasicoherent holds.

theorem projectionFormulaIsIsoOnQuasicoherent :
    ProjectionFormulaIsIsoOnQuasicoherent.{u}

Stacks.Cohomology.ProjectionFormulaDevissage.isIso_projectionFormulaMap_twoOutOfThree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/ProjectionFormulaDevissage.lean, line 138. The attribute's comment: “the triangle step of the source's dévissage, with no hypothesis: for a distinguished triangle of D(𝒪_Y), invertibility of the Tag 0B53 map at all shifts of two of the three vertices gives it at all shifts of the third, in each of the three rotations. The source states this as two out of three of the functors being exact; the direct-sum step is isIso_projectionFormulaMap_coproduct and the affine reduction is isIso_projectionFormulaMap_of_derivedModuleFunctor, both of which carry a geometric input and so are not registered”.

Let Δ be a distinguished triangle of D(𝒪_Y). If the projection-formula morphism of [Stacks, Tag 0B53] is invertible at every shift of two of the three vertices of Δ, it is invertible at every shift of the third, in each of the three rotations.

theorem isIso_projectionFormulaMap_twoOutOfThree
    (Δ : Triangle (DerivedCategory (SheafOfModules.{u} (structureSheafRing Y))))
    (hΔ : Δ ∈ distTriang _) :
    ((∀ n : ℤ, IsIso (projectionFormulaMap f E (Δ.obj₁⟦n⟧))) →
        (∀ n : ℤ, IsIso (projectionFormulaMap f E (Δ.obj₂⟦n⟧))) →
        ∀ n : ℤ, IsIso (projectionFormulaMap f E (Δ.obj₃⟦n⟧))) ∧
      ((∀ n : ℤ, IsIso (projectionFormulaMap f E (Δ.obj₁⟦n⟧))) →
        (∀ n : ℤ, IsIso (projectionFormulaMap f E (Δ.obj₃⟦n⟧))) →
        ∀ n : ℤ, IsIso (projectionFormulaMap f E (Δ.obj₂⟦n⟧))) ∧
      ((∀ n : ℤ, IsIso (projectionFormulaMap f E (Δ.obj₂⟦n⟧))) →
        (∀ n : ℤ, IsIso (projectionFormulaMap f E (Δ.obj₃⟦n⟧))) →
        ∀ n : ℤ, IsIso (projectionFormulaMap f E (Δ.obj₁⟦n⟧)))

Stacks.Cohomology.ProjectionFormulaGeneralBase.isIso_projectionFormulaMap_of_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/ProjectionFormulaGeneralBase.lean, line 177. The attribute's comment: “the tag in full: for a quasi-compact quasi-separated morphism of schemes f : X ⟶ Y, an E in D_QCoh(𝒪_X) and a K in D_QCoh(𝒪_Y), the Tag 0B53 map Rf_E ⊗ᴸ K ⟶ Rf_(E ⊗ᴸ Lf^K) is invertible, with no hypothesis beyond those. The source's first step, that invertibility is a local question on Y, is carried out here: over an affine open V ⊆ Y the square of Tag 0B6B identifies L((V).ι)^ of the map with the map for the base change f ∣_ V, every other arrow of that square being invertible because (V).ι is an open immersion; the map for f ∣_ V is the affine case; and invertibility in D(𝒪_Y) is local on the affine opens of Y”.

[Stacks, Tag 08EU]. For a quasi-compact quasi-separated morphism of schemes f : X ⟶ Y, an E in D_QCoh(𝒪_X) and a K in D_QCoh(𝒪_Y), the projection-formula morphism Rf_*E ⊗^𝐋_{𝒪_Y} K ⟶ Rf_*(E ⊗^𝐋_{𝒪_X} Lf^*K) of [Stacks, Tag 0B53] is invertible.

theorem isIso_projectionFormulaMap_of_isQuasicoherent {X Y : Scheme.{u}} (f : X ⟶ Y)
    [AlgebraicGeometry.QuasiCompact f] [AlgebraicGeometry.QuasiSeparated f]
    (E : DerivedCategory (SheafOfModules.{u} (structureSheafRing X.toRingedSpace)))
    (hE : quasicoherentDerivedProperty X E)
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing Y.toRingedSpace)))
    (hK : quasicoherentDerivedProperty Y K) :
    IsIso (projectionFormulaMap f.toLRSHom.toShHom E K)

Stacks.Cohomology.ProjectionFormulaOverAffineBase.isIso_projectionFormulaMap_of_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/ProjectionFormulaOverAffineBase.lean, line 253. The attribute's comment: “the affine case, with no hypothesis beyond the tag's own: for a quasi-compact quasi-separated morphism of schemes g : X ⟶ Spec A, an E in D_QCoh(𝒪_X) and a K in D_QCoh(𝒪_{Spec A}), the Tag 0B53 map Rg_E ⊗ᴸ K ⟶ Rg_(E ⊗ᴸ Lg^*K) is invertible. This is the source's dévissage carried out — direct sums (Tag 08DZ), distinguished triangles, and the reduction to the shifts of the structure sheaf through the equivalence D(A) ≌ D_QCoh(𝒪_{Spec A}) of Tag 06Z0 and the remark of Tag 09PB. This is the tag over a base of the form Spec A; the source's first step, the reduction of a general base Y to an affine one, is carried out in Stacks.Cohomology.ProjectionFormulaGeneralBase, where the tag is registered in full”.

Let g : X ⟶ Spec A be a quasi-compact and quasi-separated morphism of schemes, let E be an object of D_QCoh(𝒪_X) and let K be an object of D_QCoh(𝒪_{Spec A}). Then the projection-formula morphism

Rg_*E ⊗^𝐋_{𝒪_{Spec A}} K ⟶ Rg_*(E ⊗^𝐋_{𝒪_X} Lg^*K)

is an isomorphism.

theorem isIso_projectionFormulaMap_of_isQuasicoherent
    [AlgebraicGeometry.QuasiCompact g] [AlgebraicGeometry.QuasiSeparated g]
    (E : DerivedCategory (_root_.SheafOfModules.{u} (structureSheafRing X.toRingedSpace)))
    (hE : quasicoherentDerivedProperty X E)
    (K : DerivedCategory (_root_.SheafOfModules.{u}
      (structureSheafRing (Spec A).toRingedSpace)))
    (hK : quasicoherentDerivedProperty (Spec A) K) :
    IsIso (projectionFormulaMap g.toLRSHom.toShHom E K)

Stacks.Cohomology.ProjectionFormulaPerfect.isIso_derivedPullback_map_projectionFormulaMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/ProjectionFormulaPerfect.lean, line 218. The attribute's comment: “the localization step of the source's proof: for a Cartesian square of ringed spaces whose horizontal arrows are open immersions, invertibility of the projection-formula map for f' at the restricted complexes implies invertibility of the derived pullback along g of the map for f; unconditional in both complexes, but only one implication of the source's reduction — the affine case and the passage from an open cover back to the base are not proved”.

The projection-formula morphism of [Stacks, Tag 0B53] is invertible after derived pullback along an open immersion of the base, as soon as it is invertible upstairs.

Let
          g'
   X' ----------→ X
   |              |
f' |              | f
   v      g       v
   Y' ----------→ Y
be a Cartesian square of ringed spaces whose horizontal arrows g and g' are open immersions, and let E ∈ D(𝒪_X), K ∈ D(𝒪_Y). If the projection-formula morphism for f' at L(g')^*E and Lg^*K is invertible, then Lg^* of the projection-formula morphism for f at E and K is invertible.

This is [Stacks, Tag 0B6B] read for invertibility. Of the six arrows of that square, five are invertible here — the two comparisons of [Stacks, Tag 079U] because they are components of Stacks.Cohomology.DerivedPullbackTensor.derivedPullbackTensorIso, the two derived base-change maps by Stacks.Cohomology.DerivedBaseChange.isIso_derivedBaseChangeMap_of_isOpenImmersions, and the projection-formula morphism for f' by hypothesis — so the sixth, Lg^* of the projection-formula morphism for f, is invertible too.

There is no boundedness, flatness, quasi-coherence or perfectness hypothesis on E or K.

theorem isIso_derivedPullback_map_projectionFormulaMap
    [SheafedSpace.IsOpenImmersion g'] [SheafedSpace.IsOpenImmersion g]
    (sq : IsPullback g' f' f g)
    (E : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing Y)))
    (h : IsIso (projectionFormulaMap f' ((derivedPullback g').obj E)
      ((derivedPullback g).obj K))) :
    IsIso ((derivedPullback g).map (projectionFormulaMap f E K))

Stacks.Cohomology.ProjectionFormulaQCoh.isIso_projectionFormulaMap_of_isDQCoh, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/ProjectionFormulaQCoh.lean, line 89. The attribute's comment: “the whole lemma: for a quasi-compact and quasi-separated morphism of schemes f : X ⟶ Y, E in D_QCoh(𝒪_X) and K in D_QCoh(𝒪_Y), the projection-formula morphism Rf_E ⊗ᴸ K ⟶ Rf_(E ⊗ᴸ Lf^*K) of Tag 0B53 is invertible. The proof is the source's dévissage: locality on Y, the affine equivalence D(A) ≌ D_QCoh(𝒪_Y) of Tag 06Z0 with the resolution of Tag 09PB, direct sums through Tag 08DZ, two-out-of-three on distinguished triangles, and the shifts of the structure sheaf as the base case”.

[Stacks, Tag 08EU]. For a quasi-compact and quasi-separated morphism of schemes f : X ⟶ Y, an E in D_QCoh(𝒪_X) and a K in D_QCoh(𝒪_Y), the projection-formula morphism of [Stacks, Tag 0B53]

Rf_*E ⊗^𝐋_{𝒪_Y} K ⟶ Rf_*(E ⊗^𝐋_{𝒪_X} Lf^*K)

is an isomorphism.

The hypotheses are the source's and no others: quasi-compactness and quasi-separatedness of f, and quasi-coherence of the cohomology sheaves of E and of K. No boundedness, no flatness, no perfectness, no affineness, no Noetherian or separatedness assumption, and no choice of model for either derived category beyond the one the whole file works in.

theorem isIso_projectionFormulaMap_of_isDQCoh {X Y : Scheme.{u}} (f : X ⟶ Y)
    [QuasiCompact f] [QuasiSeparated f]
    (E : DerivedCategory (SheafOfModules.{u} (structureSheafRing X.toRingedSpace)))
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing Y.toRingedSpace)))
    (hE : Stacks.DerivedQCoh.IsDQCoh (R := structureSheafRing X.toRingedSpace) E)
    (hK : Stacks.DerivedQCoh.IsDQCoh (R := structureSheafRing Y.toRingedSpace) K) :
    IsIso (projectionFormulaMap f.toLRSHom.toShHom E K)

Stacks.Cohomology.DerivedProjectionFormula.isIso_projectionFormulaMap_quasiCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/ProjectionFormulaQuasiCoherent.lean, line 183.

[Stacks, Tag 08EU]. Let f : X ⟶ Y be a quasi-compact and quasi-separated morphism of schemes. For E in D_QCoh(𝒪_X) and K in D_QCoh(𝒪_Y) the projection-formula morphism of [Stacks, Tag 0B53]

R f_* E ⊗^𝐋_{𝒪_Y} K ⟶ R f_*(E ⊗^𝐋_{𝒪_X} L f^* K)

is an isomorphism.

Invertibility is local on Y, the affine opens cover Y, and over an affine open the statement is isIso_projectionFormulaMap_of_isAffine.

theorem isIso_projectionFormulaMap_quasiCoherent
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing Y.toRingedSpace)))
    (hK : ∀ j : ℤ, ((DerivedCategory.homologyFunctor
      (SheafOfModules.{u} (structureSheafRing Y.toRingedSpace)) j).obj K).IsQuasicoherent) :
    IsIso (projectionFormulaMap f.toLRSHom.toShHom E K)

Stacks.Cohomology.DerivedProjectionFormula.isIso_projectionFormulaMap_unitObject_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/ProjectionFormulaUnitKFlat.lean, line 550. The attribute's comment: “the case K = 𝒪_Y[0]: for an arbitrary morphism of ringed spaces f and an arbitrary E in D(𝒪_X), the projection-formula morphism Rf_E ⊗ᴸ 𝒪_Y ⟶ Rf_(E ⊗ᴸ Lf^*𝒪_Y) is invertible; the right unitors are derivedTensorRightUnitorNatIso, the unit comparison is derivedPullbackUnitIso and the right-unitor coherence of Tag 079U is rightUnitorCoherence_unitObject”.

[Stacks, Tag 08EU] at K = 𝒪_Y[0]. For an arbitrary morphism of ringed spaces f : X ⟶ Y and an arbitrary E in D(𝒪_X), the derived projection-formula morphism

Rf_*E ⊗^𝐋_{𝒪_Y} 𝒪_Y ⟶ Rf_*(E ⊗^𝐋_{𝒪_X} Lf^*𝒪_Y)

is an isomorphism.

This is the base case of the source's dévissage for [Stacks, Tag 08EU]. The inputs of isIso_projectionFormulaMap_unitObject are: the two right unitors and the naturality of the one on X by Stacks.RingedSpace.derivedTensorRightUnitorNatIso, the unit comparison by derivedPullbackUnitIso, and the right-unitor coherence of [Stacks, Tag 079U] by rightUnitorCoherence_unitObject.

theorem isIso_projectionFormulaMap_unitObject_unconditional
    (E : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))) :
    IsIso (projectionFormulaMap f E (singleUnit Y))

Stacks.Cohomology.DerivedProjectionFormula.isIso_projectionFormulaMap_unitShift_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/ProjectionFormulaUnitShifts.lean, line 224. The attribute's comment: “the case K = 𝒪_Y[0]⟦m⟧, every shift of the structure sheaf: for an arbitrary morphism of ringed spaces and an arbitrary E in D(𝒪_X), Rf_E ⊗ᴸ 𝒪_Y[0]⟦m⟧ ⟶ Rf_(E ⊗ᴸ Lf^*(𝒪_Y[0]⟦m⟧)) is invertible for every integer m”.

[Stacks, Tag 08EU] at K = 𝒪_Y[0]⟦m⟧, for every integer m. For an arbitrary morphism of ringed spaces f : X ⟶ Y and an arbitrary E ∈ D(𝒪_X), the derived projection-formula morphism of [Stacks, Tag 0B53]

Rf_*E ⊗^𝐋_{𝒪_Y} 𝒪_Y[0]⟦m⟧ ⟶ Rf_*(E ⊗^𝐋_{𝒪_X} Lf^*(𝒪_Y[0]⟦m⟧))

is an isomorphism.

This is the case the source's proof calls clear — "the statement of the lemma is clear for shifts of the structure sheaf" — and it is the whole base case of the source's dévissage in K. At m = 0 it is the case K = 𝒪_Y[0] of [Stacks, Tag 08EU] up to the isomorphism Z⟦0⟧ ≅ Z.

The morphism f is an arbitrary morphism of ringed spaces and E is arbitrary.

theorem isIso_projectionFormulaMap_unitShift_unconditional
    (E : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))) (m : ℤ) :
    IsIso (projectionFormulaMap f E ((singleUnit Y)⟦m⟧))

Tag 08IA, a definition

Tag 08IA in the Stacks Project.

AlgebraicGeometry.TorIndependent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/TorIndependence.lean, line 101. References: SGA 6 III (1.5); SGA 5 III (6.2).

Two schemes over a common base are Tor independent if their local rings at every pair of points with the same image are Tor independent over the local ring of the base.

def TorIndependent {S X Y : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S) : Prop

Tag 0FXV, a lemma

Tag 0FXV in the Stacks Project.

AlgebraicGeometry.torIndependent_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/TorIndependence.lean, line 430. References: SGA 6 III (1.5), “affine/local criterion”.

Tor independence of two schemes over a base can be checked on every compatible triple of affine opens, or on affine open coverings of the base and of the two inverse images.

theorem torIndependent_tfae {S X Y : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S) :
    List.TFAE [
      TorIndependent f g,
      ∀ (U : X.Opens) (_ : IsAffineOpen U)
        (V : Y.Opens) (_ : IsAffineOpen V)
        (W : S.Opens) (_ : IsAffineOpen W)
        (hUW : U ≤ f ⁻¹ᵁ W) (hVW : V ≤ g ⁻¹ᵁ W),
        letI : Algebra Γ(S, W) Γ(X, U) := (f.appLE W U hUW).hom.toAlgebra
        letI : Algebra Γ(S, W) Γ(Y, V) := (g.appLE W V hVW).hom.toAlgebra
        Algebra.TorIndependent Γ(S, W) Γ(X, U) Γ(Y, V),
      ∃ (I : Type u) (W : I → S.Opens),
        ((⨆ i, W i) = ⊤) ∧
          ((∀ i, IsAffineOpen (W i)) ∧
            ∀ i, ∃ (J : Type u) (U : J → X.Opens)
              (hU : (⨆ j, U j) = f ⁻¹ᵁ W i),
              (∀ j, IsAffineOpen (U j)) ∧
                ∃ (K : Type u) (V : K → Y.Opens)
                  (hV : (⨆ k, V k) = g ⁻¹ᵁ W i),
                  (∀ k, IsAffineOpen (V k)) ∧
                    ∀ j k,
                      let hUW : U j ≤ f ⁻¹ᵁ W i := (le_iSup U j).trans hU.le
                      let hVW : V k ≤ g ⁻¹ᵁ W i := (le_iSup V k).trans hV.le
                      letI : Algebra Γ(S, W i) Γ(X, U j) :=
                        (f.appLE (W i) (U j) hUW).hom.toAlgebra
                      letI : Algebra Γ(S, W i) Γ(Y, V k) :=
                        (g.appLE (W i) (V k) hVW).hom.toAlgebra
                      Algebra.TorIndependent
                        Γ(S, W i) Γ(X, U j) Γ(Y, V k))]

Tag 0FXW, a lemma

Tag 0FXW in the Stacks Project.

AlgebraicGeometry.torIndependent_pullback_of_flat, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/BaseChangeFour/FlatBaseChange.lean, line 55.

Tor independence of two schemes over a common base is preserved by a flat base change.

lemma torIndependent_pullback_of_flat
    {S X Y S' : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S) (s : S' ⟶ S)
    [Flat s] (h : TorIndependent f g) :
    TorIndependent (pullback.snd f s) (pullback.snd g s)

Tag 08IB, a lemma

Tag 08IB in the Stacks Project.

AlgebraicGeometry.BaseChangeChart.isIso_derivedBaseChangeComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/AffineChartComparison.lean, line 194. The attribute's comment: “the Tor-independence input of the proof: on every Cartesian affine-open chart of the square the coordinate rings are Tor independent, so the ring-level derived base-change comparison of Stacks 065Z is invertible there. The global statement is isIso_derivedBaseChangeMap_of_torIndependent”.

Stacks 0661 on a Cartesian affine-open chart. If X and S' are Tor independent over S, then for every chart the canonical comparison

K ⊗ᴸ_R R' ⟶ K ⊗ᴸ_A A'

of Stacks 065Z is an isomorphism on the whole unbounded derived category of A-modules, for every choice of models of the two total derived extension-of-scalars functors.

The pushout hypothesis of Stacks 0661 is the chart's own square A' = A ⊗_R R', and the Tor independence hypothesis is AlgebraicGeometry.BaseChangeChart.torIndependent.

This is the Tor-independence input of Stacks 08IB, not its conclusion: it does not say that the derived base-change map Lg^*Rf_*K ⟶ Rf'_*L(g')^*K of Stacks 08HY is an isomorphism. Passing from the chartwise comparison to that map is Stacks 0DJ9.

public theorem isIso_derivedBaseChangeComparison (hTor : TorIndependent f g)
    (ch : BaseChangeChart f g f' g')
    (L_g : DerivedCategory (ModuleCat.{u} ch.R) ⥤ DerivedCategory (ModuleCat.{u} ch.R'))
    (L_h : DerivedCategory (ModuleCat.{u} ch.A) ⥤ DerivedCategory (ModuleCat.{u} ch.A'))
    (alpha_g : DerivedCategory.Q ⋙ L_g ⟶
      (ModuleCat.extendScalars.{u, u, u} ch.b.hom).mapHomologicalComplex (ComplexShape.up ℤ) ⋙
        DerivedCategory.Q)
    (alpha_h : DerivedCategory.Q ⋙ L_h ⟶
      (ModuleCat.extendScalars.{u, u, u} ch.c.hom).mapHomologicalComplex (ComplexShape.up ℤ) ⋙
        DerivedCategory.Q)
    [L_g.IsLeftDerivedFunctor alpha_g
      (HomologicalComplex.quasiIso (ModuleCat.{u} ch.R) (ComplexShape.up ℤ))]
    [L_h.IsLeftDerivedFunctor alpha_h
      (HomologicalComplex.quasiIso (ModuleCat.{u} ch.A) (ComplexShape.up ℤ))] :
    IsIso (RingTheory.TorIndependence.derivedBaseChangeComparison.{u, u, u, u, u}
      ch.a.hom ch.b.hom ch.c.hom ch.d.hom ch.isPushout_hom L_g L_h alpha_g alpha_h).2.1

AlgebraicGeometry.derivedBaseChangeIsIsoOnQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/BaseChangeUnitSingle.lean, line 285. References: SGA 6 IV (3.1.0), “more general”.

[Stacks, Tag 08IB]. Let
X' --g'--> X
|          |
f'         f
v          v
S' --g---> S
be a Cartesian square of schemes with f quasi-compact and quasi-separated and X and S' Tor independent over S, and let K be an object of D(𝒪_X) with quasi-coherent cohomology sheaves. Then the derived base-change map

Lg^*(Rf_*K) ⟶ Rf'_*(L(g')^*K)

of [Stacks, Tag 08HY] is an isomorphism.

AlgebraicGeometry.derivedBaseChangeIsIsoOnQuasicoherent_of_overAffineBase — the source's reduction to an affine base — at derivedBaseChangeIsIsoOverAffineBase.

theorem derivedBaseChangeIsIsoOnQuasicoherent : DerivedBaseChangeIsIsoOnQuasicoherent.{u}

AlgebraicGeometry.isIso_derivedBaseChangeMap_of_torIndependent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/TorIndependentBaseChange.lean, line 55.

Let g : S' ⟶ S be a morphism of schemes, f : X ⟶ S quasi-compact and quasi-separated, and X' = X ×_S S' with projections g' : X' ⟶ X and f' : X' ⟶ S'. If X and S' are Tor independent over S, then for every E ∈ D_QCoh(𝒪_X) the canonical arrow Lg^*Rf_*E ⟶ Rf'_*L(g')^*E is an isomorphism.

theorem isIso_derivedBaseChangeMap_of_torIndependent (sq : IsPullback g' f' f g) [QuasiCompact f]
    [QuasiSeparated f] (hTor : TorIndependent f g)
    (E : DerivedCategory (SheafOfModules.{u} (structureSheafRing X.toSheafedSpace)))
    (hE : ∀ n : ℤ, ((DerivedCategory.homologyFunctor
      (SheafOfModules.{u} (structureSheafRing X.toRingedSpace)) n).obj E).IsQuasicoherent) :
    IsIso (derivedBaseChangeMap g'.toLRSHom.toShHom f'.toLRSHom.toShHom f.toLRSHom.toShHom
      g.toLRSHom.toShHom (comp_toShHom_of_comm sq.w) E)

Stacks.Duality.OpenImmersion.isIso_quasiCoherentDerivedBaseChangeSquare_of_isOpenImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/OpenImmersion/TwistedInverseImageRestrictionBaseChange.lean, line 401. The attribute's comment: “for base change along an OPEN IMMERSION of the base, hence flat, hence Tor independent of f: invertibility of Stacks.Duality.quasiCoherentDerivedBaseChangeSquare, the derived base change map of Stacks 08HY on the quasi-coherent derived categories at the locally small model. The general Tor-independent case is not proved in this repository; see Stacks.Duality.OpenImmersion.isIso_twistedInverseImagePushforwardBaseChange_of_isOpenImmersion”.

[Stacks, Tag 08IB] for base change along an open immersion of the base, on the quasi-coherent derived categories at the locally small model: the derived base change map β : Rf_* ⋙ Lj^* ⟶ L(j')^* ⋙ Rf'_* of [Stacks, Tag 08HY] is invertible.

This is the companion of isIso_twistedInverseImagePushforwardBaseChange_of_isOpenImmersion under Stacks.Duality.isIso_twistedInverseImagePushforwardBaseChange_iff, and it is the localization step of [Stacks, Tag 0DJ9] at this model — β here is the mate of Stacks.Duality.quasiCoherentDerivedPushforwardSquareIso, not the comparison of Stacks.Duality.OpenImmersion.quasiCoherentDerivedRestrictBaseChangeSquare, so nothing identifies derived pullback with the exact restriction along the way.

theorem isIso_quasiCoherentDerivedBaseChangeSquare_of_isOpenImmersion
    [(Stacks.Duality.quasiCoherentDerivedPushforward f hpushf).IsLeftAdjoint]
    [(Stacks.Duality.quasiCoherentDerivedPushforward f' hpushf').IsLeftAdjoint]
    (sq : IsPullback j' f' f j) :
    IsIso (Stacks.Duality.quasiCoherentDerivedBaseChangeSquare j' f' f j hpushj' hpushf hpushf'
      hpushj (Stacks.Duality.isQuasicoherent_homology_derivedPullback' j)
      (Stacks.Duality.isQuasicoherent_homology_derivedPullback' j') sq.w)

Tag 0AA7, a lemma

Tag 0AA7 in the Stacks Project.

AlgebraicGeometry.GlobalHomBaseChange.isIso_globalHomBaseChangeMap_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/GlobalHomBaseChangeIso.lean, line 505. The attribute's comment: “case (1): M perfect and K in D_QCoh(O_X)”.

Stacks 0AA7, case (1). Let X' --g'--> X, f : X ⟶ Spec R, f' : X' ⟶ Spec R' be a cartesian square over Spec φ : Spec R' ⟶ Spec R, with f quasi-compact and quasi-separated and X, Spec R' Tor independent over Spec R. For M perfect and K ∈ D_QCoh(𝒪_X) the canonical map R Hom_X(M, K) ⊗^𝐋_R R' ⟶ R Hom_{X'}(L(g')^*M, L(g')^*K) of D(R') is an isomorphism.

theorem isIso_globalHomBaseChangeMap_of_isPerfect (hsq : IsPullback g' f' f (Spec.map φ))
    [QuasiCompact f] [QuasiSeparated f] (hTor : TorIndependent f (Spec.map φ))
    (M K : DerivedCategory X.Modules)
    (hM : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace) M)
    (hK : ∀ n : ℤ, ((DerivedCategory.homologyFunctor X.Modules n).obj K).IsQuasicoherent) :
    IsIso (globalHomBaseChangeMap φ f f' g' hsq.w M K)

AlgebraicGeometry.GlobalHomBaseChange.isIso_globalHomBaseChangeMap_of_isPseudoCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/GlobalHomBaseChangeIso.lean, line 521. The attribute's comment: “case (2): M pseudo-coherent, K in D^+_QCoh(O_X), R' of finite tor dimension over R”.

Stacks 0AA7, case (2). Let X' --g'--> X, f : X ⟶ Spec R, f' : X' ⟶ Spec R' be a cartesian square over Spec φ : Spec R' ⟶ Spec R, with f quasi-compact and quasi-separated and X, Spec R' Tor independent over Spec R. If M is pseudo-coherent, K ∈ D^+_QCoh(𝒪_X) and R' has finite Tor dimension over R, the canonical map R Hom_X(M, K) ⊗^𝐋_R R' ⟶ R Hom_{X'}(L(g')^*M, L(g')^*K) of D(R') is an isomorphism.

theorem isIso_globalHomBaseChangeMap_of_isPseudoCoherent (hsq : IsPullback g' f' f (Spec.map φ))
    [QuasiCompact f] [QuasiSeparated f] (hTor : TorIndependent f (Spec.map φ))
    (M K : DerivedCategory X.Modules)
    (hM : RingedSpace.IsPseudoCoherent (X := X.toRingedSpace) M)
    (hK : DerivedCategoryB.derivedCategoryBPlus (SheafOfModules.isQuasicoherent X.ringCatSheaf) K)
    (hR' : StacksDraft.TorAmplitude.HasFiniteTorDimensionCanonical R (algebraComplex R R' φ)) :
    IsIso (globalHomBaseChangeMap φ f f' g' hsq.w M K)

Tag 0BZA, a remark

Tag 0BZA in the Stacks Project.

AlgebraicGeometry.GlobalHomBaseChange.isIso_globalHomAdjunctionMap_and_globalHomBaseChangeMap_comp_counit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/GlobalHomBaseChangeIso.lean, line 639.

Stacks 0BZA. With notation as in Stacks 0AA7, the square
R Hom_X(M, Rg'_*L) ⊗^𝐋_R R' ----> R Hom_{X'}(L(g')^*M, L(g')^*Rg'_*L)
        |  μ                                   |  a
        v                                      v
R Hom_X(M, Rg'_*L)  ===========  R Hom_{X'}(L(g')^*M, L)
commutes, and its bottom map is the canonical identification. The bottom map R Hom_X(M, Rg'_*L) ⟶ R Hom_{X'}(L(g')^*M, L) of D(R) (globalHomAdjunctionMap) is an isomorphism: it is RΓ(X, -) of the derived adjunction isomorphism R𝓗om(M, Rg'_*L) ≅ Rg'_*R𝓗om(L(g')^*M, L) followed by RΓ(X, Rg'_* -) = RΓ(X', -). The square says that the map of Stacks 0AA7 at K = Rg'_*L followed by the map a induced by the counit L(g')^*Rg'_*L ⟶ L is the multiplication map μ, the counit K' ⊗^𝐋_R R' ⟶ K' of the adjunction between - ⊗^𝐋_R R' and restriction of scalars at K' = R Hom_{X'}(L(g')^*M, L), read through that identification. Both hold for every commutative square over Spec R' ⟶ Spec R.

theorem isIso_globalHomAdjunctionMap_and_globalHomBaseChangeMap_comp_counit
    (M : DerivedCategory X.Modules) (L : DerivedCategory X'.Modules) :
    IsIso (globalHomAdjunctionMap φ f f' g' w M L) ∧
      globalHomBaseChangeMap φ f f' g' w M ((derivedPushforward g'.toLRSHom.toShHom).obj L) ≫
          (linearSections f').map
            (((Stacks.SheafOfModules.derivedSheafHom X'.toRingedSpace.sheaf).obj
              (op ((derivedPullback g'.toLRSHom.toShHom).obj M))).map
              ((derivedAdjunction g'.toLRSHom.toShHom).counit.app L)) =
        (derivedExtendScalars φ).map (globalHomAdjunctionMap φ f f' g' w M L) ≫
          (derivedExtendScalarsAdjunction φ).counit.app
            (globalHom f' ((derivedPullback g'.toLRSHom.toShHom).obj M) L)

Tag 0C0V, a lemma

Tag 0C0V in the Stacks Project.

AlgebraicGeometry.derivedPullback_hasTorAmplitudeOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativeTorAmplitudeBaseChange.lean, line 223. The attribute's comment: “preservation of Tor amplitude over the base”. References: SGA 6 III (3.5.2); SGA 6 III (4.7.2), “amplitude inclusion”.

Stacks 0C0V (1). For a cartesian square of schemes whose two morphisms to the base are Tor independent, derived pullback preserves Tor amplitude over the base.

public theorem derivedPullback_hasTorAmplitudeOver
    {X' X S' S : Scheme.{u}} (g' : X' ⟶ X) (f' : X' ⟶ S')
    (f : X ⟶ S) (g : S' ⟶ S) (hpb : IsPullback g' f' f g)
    (htor : TorIndependent f g) (E : DerivedCategory X.Modules) (a b : ℤ)
    (hE : HasTorAmplitudeOver f E a b) :
    HasTorAmplitudeOver f'
      ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
        g'.toLRSHom.toShHom).obj E) a b

AlgebraicGeometry.derivedPullbackComparison_isIso_of_isFlatOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativeTorAmplitudeBaseChange.lean, line 408. The attribute's comment: “derived pullback of a module flat over the base is the ordinary pullback”.

Stacks 0C0V (2). For a Tor-independent cartesian square of schemes and an 𝒪_X-module G flat over S, the canonical comparison from the derived pullback of G along g' to its ordinary pullback is an isomorphism.

public theorem derivedPullbackComparison_isIso_of_isFlatOver
    {X' X S' S : Scheme.{u}} (g' : X' ⟶ X) (f' : X' ⟶ S')
    (f : X ⟶ S) (g : S' ⟶ S) (hpb : IsPullback g' f' f g)
    (htor : TorIndependent f g) (G : X.Modules) (hG : IsFlatOver f.toLRSHom.toShHom G) :
    IsIso ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullbackComparison
      g'.toLRSHom.toShHom).app
      ((HomotopyCategory.quotient _ (ComplexShape.up ℤ)).obj
        ((CochainComplex.singleFunctor X.Modules 0).obj G)))

Tag 0E23, a lemma

Tag 0E23 in the Stacks Project.

Stacks.Cohomology.ClosedImmersionBaseChange.isIso_derivedBaseChangeSquare_of_torIndependent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/ClosedImmersionBaseChangeMergeCoherence.lean, line 275. The attribute's comment: “the canonical base change map Lf^ ∘ Ri_ ⟶ Ri'_ ∘ Lg^ is invertible”.

In a cartesian square of schemes with i a closed immersion and Z, X' Tor independent over X, the canonical morphism of functors Ri_* ⋙ Lf^* ⟶ Lg^* ⋙ Ri'_* of Stacks 08HY is an isomorphism.

theorem isIso_derivedBaseChangeSquare_of_torIndependent (sq : IsPullback i' g f i)
    [AlgebraicGeometry.IsClosedImmersion i] (htor : AlgebraicGeometry.TorIndependent i f) :
    IsIso (derivedBaseChangeSquare g.toLRSHom.toShHom i'.toLRSHom.toShHom i.toLRSHom.toShHom
      f.toLRSHom.toShHom (comp_toShHom_of_isPullback sq))

Stacks.Cohomology.ClosedImmersionBaseChange.derivedBaseChangeSquareIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/ClosedImmersionBaseChangeMergeCoherence.lean, line 300.

Tor-independent base change along a closed immersion. For a cartesian square with i a closed immersion and Z, X' Tor independent over X, the functors Lf^* ∘ Ri_* and Ri'_* ∘ Lg^* from D(𝒪_Z) to D(𝒪_{X'}) are isomorphic, by the canonical derived base change map of Stacks 08HY.

def derivedBaseChangeSquareIso (sq : IsPullback i' g f i)
    [AlgebraicGeometry.IsClosedImmersion i] (htor : AlgebraicGeometry.TorIndependent i f) :
    Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward i.toLRSHom.toShHom ⋙
        Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback f.toLRSHom.toShHom ≅
      Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback g.toLRSHom.toShHom ⋙
        Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward
          i'.toLRSHom.toShHom

Stacks.Cohomology.ClosedImmersionBaseChange.derivedBaseChangeSquareAsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/ClosedImmersionBaseChangeTorIndependent.lean, line 406. The attribute's comment: “Lf^ ∘ Ri_ ≅ Ri'_ ∘ Lg^ on D(𝒪_Z), by the canonical base change map”.

Tor-independent base change along a closed immersion. For a cartesian square of schemes with i a closed immersion and Z, X' Tor independent over X, the functors Lf^* ∘ Ri_* and Ri'_* ∘ Lg^* from D(𝒪_Z) to D(𝒪_{X'}) are isomorphic, by the canonical derived base change map of Stacks 08HY.

def derivedBaseChangeSquareAsIso (sq : IsPullback i' g f i)
    [AlgebraicGeometry.IsClosedImmersion i] (htor : AlgebraicGeometry.TorIndependent i f) :
    derivedPushforward i.toLRSHom.toShHom ⋙ derivedPullback f.toLRSHom.toShHom ≅
      derivedPullback g.toLRSHom.toShHom ⋙ derivedPushforward i'.toLRSHom.toShHom

Sources

LeanStacks.Cohomology.DerivedProjectionFormula.isIso_projectionFormulaMap_of_openCover · Stacks.Cohomology.DerivedProjectionFormula.isIso_derivedPullback_map_projectionFormulaMap_of_isOpenImmersion · AlgebraicGeometry.projectionFormulaIsIsoOnQuasicoherent · Stacks.Cohomology.ProjectionFormulaDevissage.isIso_projectionFormulaMap_twoOutOfThree · Stacks.Cohomology.ProjectionFormulaGeneralBase.isIso_projectionFormulaMap_of_isQuasicoherent · Stacks.Cohomology.ProjectionFormulaOverAffineBase.isIso_projectionFormulaMap_of_isQuasicoherent · Stacks.Cohomology.ProjectionFormulaPerfect.isIso_derivedPullback_map_projectionFormulaMap · Stacks.Cohomology.ProjectionFormulaQCoh.isIso_projectionFormulaMap_of_isDQCoh

Section36.23 Künneth formula, II #

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

Tag 0FLP, an equation

Tag 0FLP in the Stacks Project.

Stacks.Cohomology.DerivedKunneth.kunnethMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/KunnethMap.lean, line 199.

The relative Künneth morphism Ra_*K ⊗^L_{𝒪_S} Rb_*M ⟶ Rf_*(Lp^*K ⊗^L_{𝒪_W} Lq^*M), Equation 36.23.0.1: the adjoint transpose of the monoidality isomorphism of Stacks 079U for Lf^* followed by the tensor product of the two counit legs. It is defined for arbitrary K ∈ D(𝒪_X) and M ∈ D(𝒪_Y).

def kunnethMap
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (M : DerivedCategory (SheafOfModules.{u} (structureSheafRing Y))) :
    ((Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor S.sheaf).obj
          ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward a).obj K)).obj
        ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward b).obj M) ⟶
      (Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f).obj
        (((Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor W.sheaf).obj
            ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback p).obj K)).obj
          ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback q).obj M))

Stacks.Cohomology.DerivedKunneth.kunnethMap_natural_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/KunnethMap.lean, line 237. The attribute's comment: “naturality in the complex on the first factor”.

The relative Künneth morphism is natural in the derived module on X.

theorem kunnethMap_natural_left
    {K K' : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))}
    (k : K ⟶ K')
    (M : DerivedCategory (SheafOfModules.{u} (structureSheafRing Y))) :
    ((Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor S.sheaf).map
          ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward a).map k)).app
        ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward b).obj M) ≫
        kunnethMap a b p q f hp hq K' M =
      kunnethMap a b p q f hp hq K M ≫
        (Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f).map
          (((Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor W.sheaf).map
              ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback p).map k)).app
            ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback q).obj M))

Stacks.Cohomology.DerivedKunneth.kunnethMap_natural_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/KunnethMap.lean, line 259. The attribute's comment: “naturality in the complex on the second factor”.

The relative Künneth morphism is natural in the derived module on Y.

theorem kunnethMap_natural_right
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    {M M' : DerivedCategory (SheafOfModules.{u} (structureSheafRing Y))}
    (m : M ⟶ M') :
    ((Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor S.sheaf).obj
          ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward a).obj K)).map
        ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward b).map m) ≫
        kunnethMap a b p q f hp hq K M' =
      kunnethMap a b p q f hp hq K M ≫
        (Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f).map
          (((Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor W.sheaf).obj
              ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback p).obj K)).map
            ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback q).map m))

Tag 0G7V, an equation

Tag 0G7V in the Stacks Project.

Stacks.Cohomology.GlobalKunneth.kunnethGlobalMapCanonical, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/GlobalKunnethMapCanonical.lean, line 154. The attribute's comment: “the map, for arbitrary K ∈ D(𝒪_X) and M ∈ D(𝒪_Y) over an arbitrary base”.

The global Künneth map of Tag 0G7V, with no parameter.

RΓ(X, K) ⊗^𝐋_A RΓ(Y, M) ⟶ RΓ(W, Lp^*K ⊗^𝐋_{𝒪_W} Lq^*M)

in D(A) for A = Γ(S, 𝒪_S), where p ≫ a = f = q ≫ b; the source takes W = X ×_S Y with its two projections. It is defined for arbitrary K ∈ D(𝒪_X) and M ∈ D(𝒪_Y), over an arbitrary base, and it is built from the canonical global cup product of Section 0FKU on the base together with the relative Künneth map of Tag 0FLP and the Leray isomorphism of Tag 0D5W.

def kunnethGlobalMapCanonical (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (M : DerivedCategory (SheafOfModules.{u} (structureSheafRing Y))) :
    ((tensorBase S).obj ((sectionsOverBase a).obj K)).obj ((sectionsOverBase b).obj M) ⟶
      (sectionsOverBase f).obj
        (((derivedTensorProductFunctor W.sheaf).obj ((derivedPullback p).obj K)).obj
          ((derivedPullback q).obj M))

Stacks.Cohomology.GlobalKunneth.kunnethGlobalMapCanonical_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/GlobalKunnethMapCanonical.lean, line 173. The attribute's comment: “naturality in both complexes, with no parameter”.

The global Künneth map with no parameter is natural in both complexes jointly.

theorem kunnethGlobalMapCanonical_naturality
    {K K' : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))}
    {M M' : DerivedCategory (SheafOfModules.{u} (structureSheafRing Y))} (k : K ⟶ K') (m : M ⟶ M') :
    (Functor.uncurry.obj (tensorBase S)).map
          ((sectionsOverBase a).map k ×ₘ (sectionsOverBase b).map m) ≫
        kunnethGlobalMapCanonical a b p q f hp hq K' M' =
      kunnethGlobalMapCanonical a b p q f hp hq K M ≫
        (sectionsOverBase f).map
          ((Functor.uncurry.obj (derivedTensorProductFunctor W.sheaf)).map
            ((derivedPullback p).map k ×ₘ (derivedPullback q).map m))

Stacks.Cohomology.GlobalKunneth.kunnethGlobalMapSchemeCanonical, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/GlobalKunnethMapCanonical.lean, line 205. The attribute's comment: “the map at X ×_S Y, for arbitrary K and M over an arbitrary base scheme”.

The global Künneth map of Tag 0G7V at the fibre product of two schemes, with no parameter. For schemes a : X ⟶ S and b : Y ⟶ S over a base and A = Γ(S, 𝒪_S), the canonical map

RΓ(X, K) ⊗^𝐋_A RΓ(Y, M) ⟶ RΓ(X ×_S Y, Lp^*K ⊗^𝐋_{𝒪_{X ×_S Y}} Lq^*M)

in D(A), where p and q are the two projections of X ×_S Y. The base scheme is arbitrary and K, M are arbitrary; quasi-compactness, quasi-separatedness, quasi-coherence and Tor-independence enter only in Tag 0FLQ, which asserts that this map is an isomorphism.

def kunnethGlobalMapSchemeCanonical (K : DerivedCategory X.Modules)
    (M : DerivedCategory Y.Modules) :
    ((tensorBase S.toRingedSpace).obj ((sectionsOverBase a.toLRSHom.toShHom).obj K)).obj
        ((sectionsOverBase b.toLRSHom.toShHom).obj M) ⟶
      (sectionsOverBase (pullback.fst a b ≫ a).toLRSHom.toShHom).obj
        (((derivedTensorProductFunctor (pullback a b).toRingedSpace.sheaf).obj
            ((derivedPullback (pullback.fst a b).toLRSHom.toShHom).obj K)).obj
          ((derivedPullback (pullback.snd a b).toLRSHom.toShHom).obj M))

Stacks.Cohomology.GlobalKunneth.kunnethGlobalMapSchemeCanonical_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/GlobalKunnethMapCanonical.lean, line 226. The attribute's comment: “naturality at the fibre product of two schemes, with no parameter”.

The global Künneth map at the fibre product of two schemes, with no parameter, is natural in both complexes.

theorem kunnethGlobalMapSchemeCanonical_naturality {K K' : DerivedCategory X.Modules}
    {M M' : DerivedCategory Y.Modules} (k : K ⟶ K') (m : M ⟶ M') :
    (Functor.uncurry.obj (tensorBase S.toRingedSpace)).map
          ((sectionsOverBase a.toLRSHom.toShHom).map k ×ₘ
            (sectionsOverBase b.toLRSHom.toShHom).map m) ≫
        kunnethGlobalMapSchemeCanonical a b K' M' =
      kunnethGlobalMapSchemeCanonical a b K M ≫
        (sectionsOverBase (pullback.fst a b ≫ a).toLRSHom.toShHom).map
          ((Functor.uncurry.obj
              (derivedTensorProductFunctor (pullback a b).toRingedSpace.sheaf)).map
            ((derivedPullback (pullback.fst a b).toLRSHom.toShHom).map k ×ₘ
              (derivedPullback (pullback.snd a b).toLRSHom.toShHom).map m))

Tag 0FLQ, a lemma

Tag 0FLQ in the Stacks Project.

Stacks.Cohomology.DerivedKunneth.isIso_kunnethMapScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/KunnethDischarged.lean, line 85. The attribute's comment: “the relative conclusion, at the fibre product of two schemes, with no hypothesis beyond the tag's own”.

[Stacks, Tag 0FLQ], the relative conclusion, with no hypothesis beyond the tag's own. Let a : X ⟶ S and b : Y ⟶ S be quasi-compact and quasi-separated morphisms of schemes with X and Y Tor independent over S, let W = X ×_S Y with projections p and q, and let K ∈ D_QCoh(𝒪_X) and M ∈ D_QCoh(𝒪_Y). Then the relative Künneth morphism of [Stacks, Tag 0FLP]

Ra_*K ⊗^𝐋_{𝒪_S} Rb_*M ⟶ R(p ≫ a)_*(Lp^*K ⊗^𝐋_{𝒪_W} Lq^*M)

is an isomorphism.

This is isIso_kunnethMap_pullback_of_torIndependent_of_baseChange with its one remaining carried proposition discharged against the proved [Stacks, Tag 08IB]. All three comparisons the source's proof chains together are now proved in this library: hproj₁ and hproj₂ from [Stacks, Tag 08EU], with the interchanged-order conjugation supplied by the proved braiding compatibility of [Stacks, Tag 079U], and hbase from [Stacks, Tag 08IB].

theorem isIso_kunnethMapScheme
    [QuasiCompact a] [QuasiSeparated a] [QuasiCompact b] [QuasiSeparated b]
    (hTor : TorIndependent a b)
    (K : DerivedCategory X.Modules) (M : DerivedCategory Y.Modules)
    (hK : IsQCohAll K) (hM : IsQCohAll M) :
    IsIso (kunnethMap a.toLRSHom.toShHom b.toLRSHom.toShHom
      (pullback.fst a b).toLRSHom.toShHom (pullback.snd a b).toLRSHom.toShHom
      (pullback.fst a b ≫ a).toLRSHom.toShHom rfl
      (Stacks.Cohomology.GlobalKunneth.toShHom_pullback_condition a b) K M)

Stacks.Cohomology.DerivedKunneth.isIso_kunnethGlobalMapScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/KunnethGlobalCupProduct.lean, line 130. The attribute's comment: “the global conclusion, over an affine base, at the fibre product of two schemes, for the canonical global cup product of Section 0FKU and with no hypothesis beyond the tag's own”.

[Stacks, Tag 0FLQ], the global conclusion over an affine base, with no hypothesis beyond the tag's own.

Let a : X ⟶ S and b : Y ⟶ S be quasi-compact and quasi-separated morphisms of schemes with S affine and X and Y Tor independent over S, let W = X ×_S Y with projections p and q, and let K ∈ D_QCoh(𝒪_X) and M ∈ D_QCoh(𝒪_Y). Then the global Künneth morphism of [Stacks, Tag 0G7V]

RΓ(X, K) ⊗^𝐋_A RΓ(Y, M) ⟶ RΓ(W, Lp^*K ⊗^𝐋_{𝒪_W} Lq^*M)

for the global cup product of Cohomology, Section 0FKU is an isomorphism.

The cup product is the canonical one, not a parameter: it is Stacks.Cohomology.DerivedGlobalCupProduct.globalCupProduct of the one-point comparison Stacks.Cohomology.DerivedSectionsLeftAdjoint.onePointComparisonOnARingedSpace, which is the relative cup product of [Stacks, Tag 0B68] for the structure morphism π : S ⟶ ({*}, A) of [Stacks, Tag 01BH] read through the identification of modules on the point with A-modules, exactly as the source defines μ.

The three inputs of isIso_kunnethGlobalMapScheme_of_onePointComparison are discharged: the tensor comparison of that one-point comparison is invertible because it is the hom of an isomorphism of bifunctors, and affineness of the base supplies the invertibility of the unit and of the counit on the quasi-coherent part, which is the Spec–Γ equivalence of [Stacks, Tag 06Z0].

theorem isIso_kunnethGlobalMapScheme
    [IsAffine S] [QuasiCompact a] [QuasiSeparated a] [QuasiCompact b] [QuasiSeparated b]
    (hTor : TorIndependent a b)
    (K : DerivedCategory X.Modules) (M : DerivedCategory Y.Modules)
    (hK : IsQCohAll K) (hM : IsQCohAll M) :
    IsIso (Stacks.Cohomology.GlobalKunneth.kunnethGlobalMapScheme a b
      (globalCupProduct
        (Stacks.Cohomology.DerivedSectionsLeftAdjoint.onePointComparisonOnARingedSpace
          S.toRingedSpace)) K M)

Stacks.Cohomology.DerivedKunneth.isIso_kunnethMap_of_projectionFormulas_of_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/KunnethIsomorphism.lean, line 277. The attribute's comment: “the relative isomorphism, granted the projection formula of Tag 08EU for a and for p and the base-change comparison of Tag 08IB for the square, carried as the explicit hypotheses hproj₁, hproj₂ and hbase, together with the Stacks 079U/0D5S monoidality coherence hcoh; what is proved is that the Künneth map of Tag 0FLP is the composite of those three, the verification the source omits”.

The first conclusion of Tag 0FLQ, granted its three cited inputs.

For a : X ⟶ S, b : Y ⟶ S, p : W ⟶ X and q : W ⟶ Y with q ≫ b = p ≫ a, the relative Künneth morphism of Tag 0FLP at f = p ≫ a,

Ra_*K ⊗^𝐋_{𝒪_S} Rb_*M ⟶ Rf_*(Lp^*K ⊗^𝐋_{𝒪_W} Lq^*M),

is an isomorphism as soon as the three comparisons the source's first proof chains together are. In order they are: the projection formula of Tag 08EU for a at (K, Rb_*M); the base-change comparison La^*Rb_*M ⟶ Rp_*Lq^*M of Tag 08IB for the square; and the projection formula of Tag 08EU for p at (K, Lq^*M), read with the two tensor factors interchanged. What the proof supplies is the identification of the composite of those three with the Künneth map, which the source states and omits.

theorem isIso_kunnethMap_of_projectionFormulas_of_baseChange
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (M : DerivedCategory (SheafOfModules.{u} (structureSheafRing Y)))
    (hcoh : PullbackTensorComparisonComp a p
      ((derivedPushforward a).obj K) ((derivedPushforward b).obj M))
    (hproj₁ : IsIso (projectionFormulaMap a K ((derivedPushforward b).obj M)))
    (hbase : IsIso (kunnethBaseChangeLeg a b p q hq M))
    (hproj₂ : IsIso (adjunctionTensorMapRight (derivedAdjunction p)
      (Functor.uncurry.obj (derivedTensorProductFunctor X.sheaf))
      (Functor.uncurry.obj (derivedTensorProductFunctor W.sheaf))
      (pullbackTensorComparison p) K ((derivedPullback q).obj M))) :
    IsIso (kunnethMap a b p q (p ≫ a) rfl hq K M)

Stacks.Cohomology.DerivedKunneth.isIso_kunnethGlobalMap_of_projectionFormulas_of_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/KunnethIsomorphism.lean, line 314. The attribute's comment: “the global isomorphism over an affine base, granted the same three inputs as the relative one together with the invertibility of the A-linear global cup product on the base, carried as the explicit hypotheses hproj₁, hproj₂, hbase and hκ”.

The second conclusion of Tag 0FLQ, granted the same three inputs. Over a base whose A-linear global cup product is invertible at (Ra_*K, Rb_*M), which is what affineness of the base supplies, the global Künneth morphism of Tag 0G7V

RΓ(X, K) ⊗^𝐋_A RΓ(Y, M) ⟶ RΓ(W, Lp^*K ⊗^𝐋_{𝒪_W} Lq^*M)

is an isomorphism. The source deduces this from the relative statement by applying RΓ(S, -) to its source and target.

theorem isIso_kunnethGlobalMap_of_projectionFormulas_of_baseChange
    (κ : Stacks.Cohomology.GlobalKunneth.GlobalCupProduct S)
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (M : DerivedCategory (SheafOfModules.{u} (structureSheafRing Y)))
    (hκ : IsIso (κ.app ((derivedPushforward a).obj K, (derivedPushforward b).obj M)))
    (hcoh : PullbackTensorComparisonComp a p
      ((derivedPushforward a).obj K) ((derivedPushforward b).obj M))
    (hproj₁ : IsIso (projectionFormulaMap a K ((derivedPushforward b).obj M)))
    (hbase : IsIso (kunnethBaseChangeLeg a b p q hq M))
    (hproj₂ : IsIso (adjunctionTensorMapRight (derivedAdjunction p)
      (Functor.uncurry.obj (derivedTensorProductFunctor X.sheaf))
      (Functor.uncurry.obj (derivedTensorProductFunctor W.sheaf))
      (pullbackTensorComparison p) K ((derivedPullback q).obj M))) :
    IsIso (Stacks.Cohomology.GlobalKunneth.kunnethGlobalMap a b p q (p ≫ a) rfl hq κ K M)

Tag 0FML, a lemma

Tag 0FML in the Stacks Project.

Stacks.RelativeComplexPushforward.isIso_projectionFormulaMap_relativeComplex_of_isLocallyBounded_of_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativeComplexProjectionFormula.lean, line 880. The attribute's comment: “conclusion (5), with no hypothesis beyond the tag's own: for a quasi-compact quasi-separated morphism of schemes a : X ⟶ S, a LOCALLY BOUNDED complex F^• of a^{-1}O_S-modules each of whose terms carries a compatible quasi-coherent O_X-module structure, and K in D_QCoh(O_S), the Tag 0B53 map Ra_F^• ⊗ᴸ_{O_S} K ⟶ Ra_(F^• ⊗ᴸ_{a^{-1}O_S} L(a')^*K) is invertible. One difference from the source's phrasing, not a weakening: flatness of the terms, which the source assumes, is not needed for this conclusion and is not assumed. The two tensor factors are in the order the Tag 0B53 map produces them, which is the opposite of the source's”.

Stacks Project, Tag 0FML, conclusion (5), with no hypothesis beyond the tag's own. For f : X ⟶ S quasi-compact and quasi-separated, K an object of D_QCoh(𝒪_S) and F a locally bounded complex of f^{-1}𝒪_S-modules, the term in degree i being the restriction of scalars of a quasi-coherent 𝒪_X-module M i, the projection-formula morphism of [Stacks, Tag 0B53] at (X, f^{-1}𝒪_S) ⟶ (S, 𝒪_S) is an isomorphism.

isIso_projectionFormulaMap_relativeComplex_of_isLocallyBounded above with its hypothesis discharged by isIso_projectionFormulaMap_single_relativeBase.

theorem isIso_projectionFormulaMap_relativeComplex_of_isLocallyBounded_of_isQuasicoherent
    [QuasiCompact f] [QuasiSeparated f] (K : DerivedCategory (Modules S.toRingedSpace))
    (hK : DerivedCategoryB.derivedCategoryB
      (_root_.SheafOfModules.isQuasicoherent S.ringCatSheaf) K)
    (F : CochainComplex (Modules (inverseImageBase f)) ℤ)
    (hF : Stacks.SheafOfModules.OnSpace.IsLocallyBounded (inverseImageBase f) F)
    (M : ℤ → X.Modules) (hM : ∀ i, (M i).IsQuasicoherent)
    (hFM : ∀ i, F.X i ≅ (pushforward (toInverseImageBase f)).obj (M i)) :
    IsIso (projectionFormulaMap (inverseImageBaseProjection f)
      (DerivedCategory.Q.obj F) K)

Stacks.RelativeComplexPushforward.relativeComplexProjectionFormulaIsoOfIsLocallyBoundedOfIsQuasicoherent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativeComplexProjectionFormula.lean, line 904. The attribute's comment: “conclusion (5) read as an isomorphism, with no hypothesis beyond the tag's own: Ra_F^• ⊗ᴸ_{O_S} K is Ra_(F^• ⊗ᴸ_{a^{-1}O_S} a^{-1}K) for K in D_QCoh(O_S) and F^• LOCALLY BOUNDED. The same single difference from the source's phrasing as in the invertibility form, not a weakening: flatness of the terms is not needed for this conclusion and is not assumed”.

Stacks Project, Tag 0FML, conclusion (5) read as an isomorphism and with no hypothesis beyond the tag's own,

Rf_*F^• ⊗^𝐋_{𝒪_S} K ≅ Rf_*(F^• ⊗^𝐋_{f^{-1}𝒪_S} f^{-1}K)

for K in D_QCoh(𝒪_S) and F locally bounded, the two tensor products being written in the order the morphism of [Stacks, Tag 0B53] produces them.

def relativeComplexProjectionFormulaIsoOfIsLocallyBoundedOfIsQuasicoherent [QuasiCompact f]
    [QuasiSeparated f] (K : DerivedCategory (Modules S.toRingedSpace))
    (hK : DerivedCategoryB.derivedCategoryB
      (_root_.SheafOfModules.isQuasicoherent S.ringCatSheaf) K)
    (F : CochainComplex (Modules (inverseImageBase f)) ℤ)
    (hF : Stacks.SheafOfModules.OnSpace.IsLocallyBounded (inverseImageBase f) F)
    (M : ℤ → X.Modules) (hM : ∀ i, (M i).IsQuasicoherent)
    (hFM : ∀ i, F.X i ≅ (pushforward (toInverseImageBase f)).obj (M i)) :
    ((derivedTensorProductFunctor S.toRingedSpace.sheaf).obj
        ((derivedPushforward (inverseImageBaseProjection f)).obj
          (DerivedCategory.Q.obj F))).obj K ≅
      (derivedPushforward (inverseImageBaseProjection f)).obj
        (((derivedTensorProductFunctor (inverseImageBase f).sheaf).obj
            (DerivedCategory.Q.obj F)).obj
          ((derivedPullback (inverseImageBaseProjection f)).obj K))

Stacks.RelativeComplexPushforward.relativeComplexOrdinaryProjectionFormulaIsoOfIsLocallyBoundedOfIsQuasicoherent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativeComplexProjectionFormula.lean, line 1108. The attribute's comment: “conclusion (4), with no hypothesis beyond the tag's own: for a quasi-compact quasi-separated morphism of schemes a : X ⟶ S, a LOCALLY BOUNDED complex F^• of a^{-1}O_S-modules each of whose terms is flat over a^{-1}O_S and carries a compatible quasi-coherent O_X-module structure, and an ORDINARY quasi-coherent O_S-module G, Ra_F^• ⊗ᴸ_{O_S} G is Ra_(F^• ⊗_{a^{-1}O_S} a^{-1}G) with the ORDINARY tensor product on the right. The two tensor factors are in the order the Tag 0B53 map produces them, which is the opposite of the source's”.

Stacks Project, Tag 0FML, conclusion (4), with no hypothesis beyond the tag's own. For f : X ⟶ S quasi-compact and quasi-separated, G a quasi-coherent 𝒪_S-module and F a locally bounded complex of f^{-1}𝒪_S-modules, each term flat over f^{-1}𝒪_S and the restriction of scalars of a quasi-coherent 𝒪_X-module,

Rf_*F^• ⊗^𝐋_{𝒪_S} G ≅ Rf_*(F^• ⊗_{f^{-1}𝒪_S} f^{-1}G),

the tensor product on the right being the ordinary one.

relativeComplexOrdinaryProjectionFormulaIsoOfIsLocallyBounded above with its hypothesis discharged by isIso_projectionFormulaMap_single_relativeBase at K = G[0], which lies in D_QCoh(𝒪_S) by derivedCategoryB_isQuasicoherent_single.

def relativeComplexOrdinaryProjectionFormulaIsoOfIsLocallyBoundedOfIsQuasicoherent
    [QuasiCompact f] [QuasiSeparated f] (G : Modules S.toRingedSpace) (hG : G.IsQuasicoherent)
    (F : CochainComplex (Modules (inverseImageBase f)) ℤ)
    (hF : Stacks.SheafOfModules.OnSpace.IsLocallyBounded (inverseImageBase f) F)
    (hflat : ∀ i : ℤ, AlgebraicGeometry.SheafOfModules.IsFlat.{u, u, u, u}
      (O := (inverseImageBase f).sheaf) (F.X i))
    (M : ℤ → X.Modules) (hM : ∀ i, (M i).IsQuasicoherent)
    (hFM : ∀ i, F.X i ≅ (pushforward (toInverseImageBase f)).obj (M i)) :
    ((derivedTensorProductFunctor S.toRingedSpace.sheaf).obj
        ((derivedPushforward (inverseImageBaseProjection f)).obj
          (DerivedCategory.Q.obj F))).obj
      ((DerivedCategory.singleFunctor (Modules S.toRingedSpace) 0).obj G) ≅
      (derivedPushforward (inverseImageBaseProjection f)).obj
        (DerivedCategory.Q.obj
          (((Stacks.SheafOfModules.Tensor.tensorComplex (inverseImageBase f).sheaf).obj F).obj
            ((CochainComplex.singleFunctor (Modules (inverseImageBase f)) 0).obj
              ((RingedSpaceModuleAdjunction.modulePullback
                (inverseImageBaseProjection f)).obj G))))

Stacks.RelativeComplexPushforward.relativeDerivedPushforward_locallyBounded_qcoh_torDimension_projectionFormula, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativeComplexPushforwardLocal.lean, line 595. The attribute's comment: “all five conclusions, under exactly the source's hypotheses: a : X ⟶ S quasi-compact and quasi-separated, F^• a LOCALLY BOUNDED complex of a^{-1}O_S-modules with flat terms each carrying a compatible quasi-coherent O_X-module structure (differentials not O_X-linear); Ra_ is the unbounded derived pushforward along (X, a^{-1}O_S) ⟶ (S, O_S). (1) every point of S has an open neighbourhood U with (Ra_F^•)|_U cohomologically bounded; (2) Ra_F^• in D_QCoh(O_S); (3) LocallyHasFiniteTorDimension at the derived tensor product of Tag 06YU; (4) an isomorphism Ra_F^• ⊗ᴸ G ≅ Ra_*(F^• ⊗ a^{-1}G) for G quasi-coherent; (5) invertibility of the Tag 0B53 map for K in D_QCoh(O_S). Tensor factors in (4), (5) are in the order the Tag 0B53 map produces them, the opposite of the source's”.

Stacks Project, Tag 0FML. Let a : X ⟶ S be a quasi-compact and quasi-separated morphism of schemes and F^• a locally bounded complex of a⁻¹𝒪_S-modules, each term F^n a flat a⁻¹𝒪_S-module carrying the structure of a quasi-coherent 𝒪_X-module M n compatible with its a⁻¹𝒪_S-module structure (F^n ≅ b_*(M n) for b : (X, 𝒪_X) ⟶ (X, a⁻¹𝒪_S); the differentials of F^• need not be 𝒪_X-linear). Write Ra_*F^• for the derived pushforward along the morphism of ringed spaces (X, a⁻¹𝒪_S) ⟶ (S, 𝒪_S). Then

Ra_*F^• is locally bounded: every point of S has an open neighbourhood U on which (Ra_*F^•)|_U has only finitely many nonzero cohomology sheaves;

Ra_*F^• lies in D_QCoh(𝒪_S);

Ra_*F^• locally has finite Tor dimension;

Ra_*F^• ⊗^𝐋_{𝒪_S} 𝒢 ≅ Ra_*(F^• ⊗_{a⁻¹𝒪_S} a⁻¹𝒢) for every quasi-coherent 𝒢;

the map of [Stacks, Tag 0B53] Ra_*F^• ⊗^𝐋_{𝒪_S} K ⟶ Ra_*(F^• ⊗^𝐋_{a⁻¹𝒪_S} a⁻¹K) is an isomorphism for every K in D_QCoh(𝒪_S).

The tensor products in (4) and (5) are written in the order the map of [Stacks, Tag 0B53] produces them, the opposite of the source's; the two orders agree by symmetry. Conclusions (4) and (5) are relativeComplexOrdinaryProjectionFormulaIsoOfIsLocallyBoundedOfIsQuasicoherent and isIso_projectionFormulaMap_relativeComplex_of_isLocallyBounded_of_isQuasicoherent. Conclusions (1)–(3) are local on S; over an affine open V the complex is bounded on the quasi-compact a⁻¹V, and prop_restrict_derivedPushforward_relativeComplex reduces each of them to a single quasi-coherent M n, where (1) is [Stacks, Tag 01XJ], (2) is the quasi-coherence of the higher direct images and (3) is the Mayer–Vietoris bound on Tor amplitude of a derived direct image of a module flat over the base.

theorem relativeDerivedPushforward_locallyBounded_qcoh_torDimension_projectionFormula
    [QuasiCompact f] [QuasiSeparated f]
    (F : CochainComplex (Modules (inverseImageBase f)) ℤ)
    (hF : Stacks.SheafOfModules.OnSpace.IsLocallyBounded (inverseImageBase f) F)
    (hflat : ∀ i : ℤ, AlgebraicGeometry.SheafOfModules.IsFlat.{u, u, u, u}
      (O := (inverseImageBase f).sheaf) (F.X i))
    (M : ℤ → X.Modules) (hM : ∀ i, (M i).IsQuasicoherent)
    (hFM : ∀ i, F.X i ≅ (pushforward (toInverseImageBase f)).obj (M i)) :
    (∀ s : S, ∃ U : S.Opens, s ∈ U ∧ DerivedCategoryB.IsBounded
      ((Scheme.Modules.restrictFunctor U.ι).mapDerivedCategory.obj
        ((derivedPushforward (inverseImageBaseProjection f)).obj
          (DerivedCategory.Q.obj F)))) ∧
    (DerivedCategoryB.derivedCategoryB (_root_.SheafOfModules.isQuasicoherent S.ringCatSheaf) :
      ObjectProperty (DerivedCategory (Modules S.toRingedSpace)))
      ((derivedPushforward (inverseImageBaseProjection f)).obj (DerivedCategory.Q.obj F)) ∧
    LocallyHasFiniteTorDimension S.toRingedSpace
      ((derivedPushforward (inverseImageBaseProjection f)).obj (DerivedCategory.Q.obj F)) ∧
    (∀ G : Modules S.toRingedSpace, G.IsQuasicoherent →
      Nonempty (((derivedTensorProductFunctor S.toRingedSpace.sheaf).obj
          ((derivedPushforward (inverseImageBaseProjection f)).obj
            (DerivedCategory.Q.obj F))).obj
        ((DerivedCategory.singleFunctor (Modules S.toRingedSpace) 0).obj G) ≅
        (derivedPushforward (inverseImageBaseProjection f)).obj
          (DerivedCategory.Q.obj
            (((Stacks.SheafOfModules.Tensor.tensorComplex (inverseImageBase f).sheaf).obj F).obj
              ((CochainComplex.singleFunctor (Modules (inverseImageBase f)) 0).obj
                ((RingedSpaceModuleAdjunction.modulePullback
                  (inverseImageBaseProjection f)).obj G)))))) ∧
    (∀ K : DerivedCategory (Modules S.toRingedSpace),
      DerivedCategoryB.derivedCategoryB
        (_root_.SheafOfModules.isQuasicoherent S.ringCatSheaf) K →
      IsIso (Stacks.Cohomology.DerivedProjectionFormula.projectionFormulaMap
        (inverseImageBaseProjection f) (DerivedCategory.Q.obj F) K))

Stacks.RelativeComplexPushforward.isQuasicoherent_homology_relativeDerivedPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativeComplexPushforwardQcoh.lean, line 89. The attribute's comment: “conclusion (2), that Ra_* of the complex lies in D_QCoh, degreewise, for a complex bounded below with an explicit bound rather than merely locally bounded”.

Stacks Project, Tag 0FML, conclusion (2). Let f : X ⟶ S be quasi-compact and quasi-separated and let K be a complex of f^{-1}𝒪_S-modules, strictly bounded below, whose term in degree i is the restriction of scalars of a quasi-coherent 𝒪_X-module M i. Then every cohomology sheaf of Rf_*K is quasi-coherent.

theorem isQuasicoherent_homology_relativeDerivedPushforward [QuasiCompact f] [QuasiSeparated f]
    (n : ℤ) (K : CochainComplex (Modules (inverseImageBase f)) ℤ)
    [CochainComplex.IsStrictlyGE K n] (M : ℤ → X.Modules) (hM : ∀ i, (M i).IsQuasicoherent)
    (hK : ∀ i, K.X i ≅ (pushforward (toInverseImageBase f)).obj (M i)) (i : ℤ) :
    ((DerivedCategory.Plus.homologyFunctor S.Modules i).obj
      (relativeDerivedPushforward f n K)).IsQuasicoherent

Stacks.RelativeComplexPushforward.derivedCategoryB_relativeDerivedPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativeComplexPushforwardQcoh.lean, line 127. The attribute's comment: “conclusion (2), that Ra_* of the complex lies in D_QCoh, as a membership, for a complex bounded below with an explicit bound rather than merely locally bounded”.

Stacks Project, Tag 0FML, conclusion (2), in the membership form: the object property on D(𝒪_S) cutting out the complexes with quasi-coherent cohomology holds of Rf_*K. The complex being bounded below, Rf_*K is read in D⁺(𝒪_S) and compared with D(𝒪_S) along the inclusion, under which the cohomology functors agree.

theorem derivedCategoryB_relativeDerivedPushforward [QuasiCompact f] [QuasiSeparated f]
    (n : ℤ) (K : CochainComplex (Modules (inverseImageBase f)) ℤ)
    [CochainComplex.IsStrictlyGE K n] (M : ℤ → X.Modules) (hM : ∀ i, (M i).IsQuasicoherent)
    (hK : ∀ i, K.X i ≅ (pushforward (toInverseImageBase f)).obj (M i)) :
    DerivedCategoryB.derivedCategoryB (_root_.SheafOfModules.isQuasicoherent S.ringCatSheaf)
      (DerivedCategory.Plus.ι.obj (relativeDerivedPushforward f n K))

Tag 0FMQ, a lemma

Tag 0FMQ in the Stacks Project.

AlgebraicGeometry.kFlat_totalCechComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/Coherator/KunnethTotalCech.lean, line 1082.

Stacks 0FMQ. Let f : X ⟶ S be a morphism of schemes with S affine and A = Γ(S, 𝒪_S), and let U : I → X.Opens be a finite family of opens all of whose finite intersections are affine. Let K be a bounded complex of presheaves of A-modules on X whose degree-n term is the presheaf of sections of a quasi-coherent 𝒪_X-module F n that is flat over S. Then Tot(Č^•(𝒰, K)) is K-flat as a complex of A-modules.

public theorem kFlat_totalCechComplex {X S : Scheme.{u}} [IsAffine S] (f : X ⟶ S)
    {I : Type u} [Finite I] (U : I → X.Opens)
    (haffine : ∀ (p : ℕ) (s : Fin (p + 1) → I), IsAffineOpen (⨅ k, U (s k)))
    (K : CochainComplex ((X.Opens)ᵒᵖ ⥤ ModuleCat.{u} ↑Γ(S, ⊤)) ℤ) (a b : ℤ)
    [CochainComplex.IsStrictlyGE K a] [CochainComplex.IsStrictlyLE K b]
    (F : ℤ → X.Modules) (hqc : ∀ n, (F n).IsQuasicoherent)
    (hflat : ∀ n, IsFlatOver f.toLRSHom.toShHom (F n))
    (hterm : ∀ n, K.X n ≅ sectionsPresheaf f (F n)) :
    CochainComplex.KFlat.{u, u} ((totalCechComplex U).obj K)

Tag 0G49, an equation

Tag 0G49 in the Stacks Project.

Stacks.Cohomology.GlobalKunneth.kunnethMapOfSheavesCanonical, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/GlobalCupProductCanonicalInstances.lean, line 192. The attribute's comment: “the map, at the A-linear global cup product globalCupProductCanonical of Section 0FKU on the base”.

The global Künneth map for two module sheaves at the canonical global cup product.

RΓ(X, ℱ) ⊗^𝐋_A RΓ(Y, 𝒢) ⟶ RΓ(W, p^*ℱ ⊗_{𝒪_W} q^*𝒢)

in D(A) for A = Γ(S, 𝒪_S), where p ≫ a = f = q ≫ b; the source takes W = X ×_S Y with its two projections. It is Stacks.Cohomology.GlobalKunneth.kunnethMapOfSheaves at the canonical global cup product of Section 0FKU.

def kunnethMapOfSheavesCanonical (F : Modules X.sheaf) (G : Modules Y.sheaf) :
    ((tensorBase S).obj ((sectionsOverBase a).obj (singleD F))).obj
        ((sectionsOverBase b).obj (singleD G)) ⟶
      (sectionsOverBase f).obj
        (singleD (sheafTensorObj ((modulePullback p).obj F) ((modulePullback q).obj G)))

Stacks.Cohomology.GlobalKunneth.kunnethMapOfSheavesCanonical_eq_kunnethGlobalMapCanonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/GlobalCupProductCanonicalInstances.lean, line 220. The attribute's comment: “the map is the derived map at the sheaves in degree zero: both sides are at the canonical global cup product, the right-hand side being kunnethGlobalMapCanonical of Tag 0G7V”.

The Künneth map for two module sheaves at the canonical global cup product is the derived Künneth map kunnethGlobalMapCanonical at the two sheaves placed in degree zero, followed by derived global sections of the canonical comparison from the derived tensor product of the derived pullbacks to the ordinary tensor product of the ordinary pullbacks.

theorem kunnethMapOfSheavesCanonical_eq_kunnethGlobalMapCanonical (F : Modules X.sheaf)
    (G : Modules Y.sheaf) :
    kunnethMapOfSheavesCanonical a b p q f hp hq F G =
      kunnethGlobalMapCanonical a b p q f hp hq (singleD F) (singleD G) ≫
        (sectionsOverBase f).map (externalTensorComparison p q F G)

Stacks.Cohomology.GlobalKunneth.kunnethMapOfSheavesCanonical_naturality_derived, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/GlobalCupProductCanonicalInstances.lean, line 230. The attribute's comment: “naturality inherited from the derived map, at the canonical global cup product”.

The derived Künneth map kunnethGlobalMapCanonical at sheaves placed in degree zero, the first factor of kunnethMapOfSheavesCanonical, is natural in the two sheaves ℱ and 𝒢.

theorem kunnethMapOfSheavesCanonical_naturality_derived
    {F F' : Modules X.sheaf} {G G' : Modules Y.sheaf} (φ : F ⟶ F') (ψ : G ⟶ G') :
    (Functor.uncurry.obj (tensorBase S)).map
          ((sectionsOverBase a).map (DerivedCategory.Q.map
              ((CochainComplex.singleFunctor (Modules X.sheaf) 0).map φ)) ×ₘ
            (sectionsOverBase b).map (DerivedCategory.Q.map
              ((CochainComplex.singleFunctor (Modules Y.sheaf) 0).map ψ))) ≫
        kunnethGlobalMapCanonical a b p q f hp hq (singleD F') (singleD G') =
      kunnethGlobalMapCanonical a b p q f hp hq (singleD F) (singleD G) ≫
        (sectionsOverBase f).map
          ((Functor.uncurry.obj (derivedTensorProductFunctor W.sheaf)).map
            ((derivedPullback p).map (DerivedCategory.Q.map
                ((CochainComplex.singleFunctor (Modules X.sheaf) 0).map φ)) ×ₘ
              (derivedPullback q).map (DerivedCategory.Q.map
                ((CochainComplex.singleFunctor (Modules Y.sheaf) 0).map ψ))))

Stacks.Cohomology.GlobalKunneth.kunnethMapOfSheavesSchemeCanonical, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/GlobalCupProductCanonicalInstances.lean, line 265. The attribute's comment: “the map at X ×_S Y, at the global cup product globalCupProductCanonical on the base”.

The global Künneth map at the fibre product of two schemes, at the canonical global cup product. For schemes a : X ⟶ S and b : Y ⟶ S over a base, A = Γ(S, 𝒪_S), an 𝒪_X-module ℱ and an 𝒪_Y-module 𝒢, the canonical map

RΓ(X, ℱ) ⊗^𝐋_A RΓ(Y, 𝒢) ⟶ RΓ(X ×_S Y, p^*ℱ ⊗_{𝒪_{X ×_S Y}} q^*𝒢)

in D(A), where p and q are the two projections of X ×_S Y and the target is the external tensor product of Tag 0G46 placed in degree zero.

def kunnethMapOfSheavesSchemeCanonical (F : X.Modules) (G : Y.Modules) :
    ((tensorBase S.toRingedSpace).obj
          ((sectionsOverBase a.toLRSHom.toShHom).obj (singleD F))).obj
        ((sectionsOverBase b.toLRSHom.toShHom).obj (singleD G)) ⟶
      (sectionsOverBase (pullback.fst a b ≫ a).toLRSHom.toShHom).obj
        (singleD (externalTensorProduct a b F G))

Stacks.Cohomology.GlobalKunneth.kunnethMapOfSheavesSchemeCanonical_eq_kunnethGlobalMapSchemeCanonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/GlobalCupProductCanonicalInstances.lean, line 286. The attribute's comment: “the map at the fibre product is the derived map at the sheaves in degree zero: both sides are at the canonical global cup product, the right-hand side being kunnethGlobalMapSchemeCanonical of Tag 0G7V”.

At the fibre product of two schemes, the Künneth map for two module sheaves at the canonical global cup product is the derived Künneth map kunnethGlobalMapSchemeCanonical at the two sheaves placed in degree zero, followed by derived global sections of externalTensorComparison.

theorem kunnethMapOfSheavesSchemeCanonical_eq_kunnethGlobalMapSchemeCanonical
    (F : X.Modules) (G : Y.Modules) :
    kunnethMapOfSheavesSchemeCanonical a b F G =
      kunnethGlobalMapSchemeCanonical a b (singleD F) (singleD G) ≫
        (sectionsOverBase (pullback.fst a b ≫ a).toLRSHom.toShHom).map
          (externalTensorComparison (pullback.fst a b).toLRSHom.toShHom
            (pullback.snd a b).toLRSHom.toShHom F G)

Tag 0FU4, a lemma

Tag 0FU4 in the Stacks Project.

AlgebraicGeometry.FlatKunneth.isIso_kunnethMapOfSheavesSchemeCanonical_of_affineDiagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/FlatKunneth/KunnethFlatSheaves.lean, line 257.

[Stacks, Tag 0FU4]. Let a : X ⟶ S and b : Y ⟶ S be morphisms of schemes with S affine, let A = Γ(S, 𝒪_S), and let p, q be the projections of X ×_S Y. If ℱ on X and 𝒢 on Y are S-flat and quasi-coherent and X and Y are quasi-compact with affine diagonal, then the Künneth map of [Stacks, Tag 0G49]

RΓ(X, ℱ) ⊗^𝐋_A RΓ(Y, 𝒢) ⟶ RΓ(X ×_S Y, p^*ℱ ⊗_{𝒪_{X ×_S Y}} q^*𝒢)

is an isomorphism in D(A). The map is Stacks.Cohomology.GlobalKunneth.kunnethMapOfSheavesSchemeCanonical, built from the global cup product of Cohomology, Section 0FKU with no parameter.

Nothing is carried. Quasi-compactness and affineness of the diagonals give the quasi-compactness and quasi-separatedness of a and b; affineness of S, flatness of 𝒢 and quasi-coherence of ℱ and 𝒢 are consumed by isIso_kunnethMapOfSheavesSchemeCanonical_of_isFlatOver, which this specializes. Flatness of ℱ is the tag's hypothesis but the proof does not need it: one flat factor suffices, by the Tor vanishing of [Stacks, Tag 0GMU].

theorem isIso_kunnethMapOfSheavesSchemeCanonical_of_affineDiagonal [IsAffine S] [CompactSpace X]
    [CompactSpace Y] [IsAffineHom (pullback.diagonal (terminal.from X))]
    [IsAffineHom (pullback.diagonal (terminal.from Y))]
    (F : X.Modules) (G : Y.Modules) [F.IsQuasicoherent] [G.IsQuasicoherent]
    (_hF : IsFlatOver a.toLRSHom.toShHom F) (hG : IsFlatOver b.toLRSHom.toShHom G) :
    IsIso (kunnethMapOfSheavesSchemeCanonical a b F G)

Stacks.Cohomology.GlobalKunneth.isIso_kunnethMapOfSheavesScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/KunnethIsomorphismOfSheaves.lean, line 239. The attribute's comment: “the isomorphism at X ×_S Y; three inputs are carried, so the geometric hypotheses are not consumed: hκ, invertibility of the global cup product on the affine base, which no bare GlobalCupProduct has; hrel, Tag 0FLQ at the sheaves in degree zero; hext, the 06YU comparison, which the tag's relative S-flatness cannot discharge in this library”.

[Stacks, Tag 0FU4]. Let a : X ⟶ S and b : Y ⟶ S be morphisms of schemes with S affine, let A = Γ(S, 𝒪_S) and let p, q be the projections of W = X ×_S Y. If X and Y are quasi-compact with affine diagonal and ℱ on X, 𝒢 on Y are quasi-coherent and flat over S, then the Künneth map of [Stacks, Tag 0G49]

RΓ(X, ℱ) ⊗^𝐋_A RΓ(Y, 𝒢) ⟶ RΓ(X ×_S Y, ℱ ⊠ 𝒢)

is an isomorphism in D(A).

The three inputs of the proof are carried as the hypotheses hκ, hrel and hext, and the geometric hypotheses are therefore not consumed; the implementation notes of this file say what each of the three is and why none is available in the library. hκ is the invertibility of the A-linear global cup product on the affine base, hrel is [Stacks, Tag 0FLQ] at the two sheaves placed in degree zero, and hext is the invertibility of the derived-to-ordinary comparison in which the source consumes the flatness of ℱ and 𝒢. What is proved here is that the three suffice.

theorem isIso_kunnethMapOfSheavesScheme [IsAffine S] [CompactSpace X] [CompactSpace Y]
    [IsAffineHom (pullback.diagonal (terminal.from X))]
    [IsAffineHom (pullback.diagonal (terminal.from Y))]
    (κ : GlobalCupProduct S.toRingedSpace) (F : X.Modules) (G : Y.Modules)
    [F.IsQuasicoherent] [G.IsQuasicoherent]
    (_hF : IsFlatOver a.toLRSHom.toShHom F) (_hG : IsFlatOver b.toLRSHom.toShHom G)
    (hκ : IsIso (κ.app ((derivedPushforward a.toLRSHom.toShHom).obj (singleD F),
      (derivedPushforward b.toLRSHom.toShHom).obj (singleD G))))
    (hrel : IsIso (Stacks.Cohomology.DerivedKunneth.kunnethMap a.toLRSHom.toShHom
      b.toLRSHom.toShHom (pullback.fst a b).toLRSHom.toShHom
      (pullback.snd a b).toLRSHom.toShHom (pullback.fst a b ≫ a).toLRSHom.toShHom rfl
      (toShHom_pullback_condition a b) (singleD F) (singleD G)))
    (hext : IsIso (externalTensorComparison (pullback.fst a b).toLRSHom.toShHom
      (pullback.snd a b).toLRSHom.toShHom F G)) :
    IsIso (kunnethMapOfSheavesScheme a b κ F G)

Tag 0G7W, a remark

Tag 0G7W in the Stacks Project.

Stacks.Cohomology.KunnethCupWithClass.kunnethGlobalMapSchemeCanonical_cupWithClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/GlobalKunnethCupWithClassCanonical.lean, line 481.

Remark 0G7W. Let a : X ⟶ S and b : Y ⟶ S be morphisms of schemes, let p : X ×_S Y ⟶ X and q : X ×_S Y ⟶ Y be the projections, and set A = Γ(S, 𝒪_S). Let 𝒢, ℱ ∈ D(𝒪_X) and ℰ ∈ D(𝒪_Y) — for instance quasi-coherent modules placed in degree zero — and let ξ ∈ Hⁱ(X, 𝒢), with pullback p^*ξ ∈ Hⁱ(X ×_S Y, Lp^*𝒢), represented by the morphism A[-i] ⟶ RΓ(X, 𝒢) representing ξ followed by the pullback map p^* : RΓ(X, 𝒢) ⟶ RΓ(X ×_S Y, Lp^*𝒢) (that this represents the class Hⁱ(p^*)(ξ) is Stacks.Cohomology.KunnethCupWithClass.classOverBase_comp_homology). Then the square
RΓ(X, ℱ)[-i] ⊗^𝐋_A RΓ(Y, ℰ) --ξ ⊗ 1--> RΓ(X, 𝒢 ⊗ ℱ) ⊗^𝐋_A RΓ(Y, ℰ)
           |                                            |
           v                                            v
RΓ(X ×_S Y, Lp^*ℱ ⊗ Lq^*ℰ)[-i] --p^*ξ--> RΓ(X ×_S Y, Lp^*(𝒢 ⊗ ℱ) ⊗ Lq^*ℰ)
commutes in D(A). The horizontal arrows are cup product with a class, Remark 0G6W, for the A-linear global cup products of Section 0FKU on X and on X ×_S Y; the vertical arrows are the global Künneth map of Equation 36.23.0.2, kunnethGlobalMapSchemeCanonical (Tag 0G7V), shifted by [-i] through the source's identification M[-i] = A[-i] ⊗^𝐋_A M. Nothing is a parameter: the cup products, the pullback map, the associativity constraint baseAssociator of ⊗^𝐋_A (that of D({*}, A) read through D(A) = D({*}, A), as in Section 0FKU) and that of ⊗^𝐋_{𝒪} (Tag 0FPB) are all canonical. The two identifications the source makes silently in the bottom-right corner, Lp^*(𝒢 ⊗ ℱ) = Lp^*𝒢 ⊗ Lp^*ℱ (Tag 079U) and the rebracketing, are the last two arrows of the right-hand route. No quasi-coherence, affineness or finiteness hypothesis is needed.

theorem kunnethGlobalMapSchemeCanonical_cupWithClass
    (𝒢 ℱ : DerivedCategory X.Modules) (ℰ : DerivedCategory Y.Modules) (i : ℤ)
    (ξ : ModuleCat.of (baseRing S.toRingedSpace) (baseRing S.toRingedSpace) ⟶
      cohomologyModuleOverBase a.toLRSHom.toShHom 𝒢 i) :
    ((tensorBase S.toRingedSpace).map
          (cupWithClassOverBase (sectionsOverBaseComparison a.toLRSHom.toShHom) 𝒢 ℱ i
            (classOverBase a.toLRSHom.toShHom 𝒢 i ξ))).app
          ((sectionsOverBase b.toLRSHom.toShHom).obj ℰ) ≫
        kunnethGlobalMapSchemeCanonical a b
            (((derivedTensorProductFunctor X.toRingedSpace.sheaf).obj 𝒢).obj ℱ) ℰ ≫
          (sectionsOverBase (pullback.fst a b ≫ a).toLRSHom.toShHom).map
              ((Functor.uncurry.obj
                  (derivedTensorProductFunctor (pullback a b).toRingedSpace.sheaf)).map
                (pullbackTensorComparisonApp (pullback.fst a b).toLRSHom.toShHom 𝒢 ℱ ×ₘ
                  𝟙 ((derivedPullback (pullback.snd a b).toLRSHom.toShHom).obj ℰ))) ≫
            (sectionsOverBase (pullback.fst a b ≫ a).toLRSHom.toShHom).map
              (derivedAssociator (pullback a b).toRingedSpace
                ((derivedPullback (pullback.fst a b).toLRSHom.toShHom).obj 𝒢)
                ((derivedPullback (pullback.fst a b).toLRSHom.toShHom).obj ℱ)
                ((derivedPullback (pullback.snd a b).toLRSHom.toShHom).obj ℰ)) =
      (Functor.uncurry.obj (tensorBase S.toRingedSpace)).map
          ((baseShiftTensorIso S.toRingedSpace i
              ((sectionsOverBase a.toLRSHom.toShHom).obj ℱ)).inv ×ₘ
            𝟙 ((sectionsOverBase b.toLRSHom.toShHom).obj ℰ)) ≫
        baseAssociator S.toRingedSpace (baseShift S.toRingedSpace i)
            ((sectionsOverBase a.toLRSHom.toShHom).obj ℱ)
            ((sectionsOverBase b.toLRSHom.toShHom).obj ℰ) ≫
          ((tensorBase S.toRingedSpace).obj (baseShift S.toRingedSpace i)).map
              (kunnethGlobalMapSchemeCanonical a b ℱ ℰ) ≫
            (baseShiftTensorIso S.toRingedSpace i
              ((sectionsOverBase (pullback.fst a b ≫ a).toLRSHom.toShHom).obj
                (((derivedTensorProductFunctor (pullback a b).toRingedSpace.sheaf).obj
                  ((derivedPullback (pullback.fst a b).toLRSHom.toShHom).obj ℱ)).obj
                    ((derivedPullback (pullback.snd a b).toLRSHom.toShHom).obj ℰ)))).hom ≫
              cupWithClassOverBase
                (sectionsOverBaseComparison (pullback.fst a b ≫ a).toLRSHom.toShHom)
                ((derivedPullback (pullback.fst a b).toLRSHom.toShHom).obj 𝒢)
                (((derivedTensorProductFunctor (pullback a b).toRingedSpace.sheaf).obj
                    ((derivedPullback (pullback.fst a b).toLRSHom.toShHom).obj ℱ)).obj
                  ((derivedPullback (pullback.snd a b).toLRSHom.toShHom).obj ℰ)) i
                (classOverBase a.toLRSHom.toShHom 𝒢 i ξ ≫
                  pullbackSections a.toLRSHom.toShHom (pullback.fst a b).toLRSHom.toShHom
                    (pullback.fst a b ≫ a).toLRSHom.toShHom rfl 𝒢)

Stacks.Cohomology.DerivedGlobalCupProduct.kunnethOverBase_cupWithClassOverBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/GlobalKunnethMapAndCupProduct.lean, line 562. The attribute's comment: “the commutativity of the square, for A-linear cup products built from a one-point comparison on X and on W (the parameters κX, κW, as for Section 0FKU in this development), for the pullback map π on derived global sections with its compatibility hπ with the two cup products (Cohomology, Lemma 0FP6, which this development cannot transport onto them), and for associativity constraints aA, aB with their naturality haA, haB and the compatibility hα of the comparison with them, all universally quantified; the source's suppressed identifications p^(G ⊗ F) = p^G ⊗ p^*F of Tag 079U and the rebracketing are the last two arrows of the right-hand route”.

Remark 0G7W. Let a : X ⟶ S and b : Y ⟶ S be spaces over a base, let p : W ⟶ X, q : W ⟶ Y and f : W ⟶ S with p ≫ a = f = q ≫ b, and set A = Γ(S, 𝒪_S). For 𝒢, ℱ ∈ D(𝒪_X), ℰ ∈ D(𝒪_Y) and a class ξ ∈ Hⁱ(X, 𝒢) represented by a morphism A[-i] ⟶ RΓ(X, 𝒢), the square
RΓ(X, ℱ)[-i] ⊗^𝐋_A RΓ(Y, ℰ) --ξ ⊗ 1--> RΓ(X, 𝒢 ⊗^𝐋 ℱ) ⊗^𝐋_A RΓ(Y, ℰ)
           |                                            |
           v                                            v
RΓ(W, Lp^*ℱ ⊗^𝐋 Lq^*ℰ)[-i] --p^*ξ--> RΓ(W, Lp^*(𝒢 ⊗^𝐋 ℱ) ⊗^𝐋 Lq^*ℰ)
commutes in D(A), the horizontals being cup product with a class as in Remark 0G6W and the verticals the global Künneth map of Equation 36.23.0.2. The right-hand route is continued by the pullback–tensor comparison of Tag 079U and the associativity constraint, the two identifications the source makes silently in its bottom-right corner.

theorem kunnethOverBase_cupWithClassOverBase
    (aA : ∀ P Q Z : DerivedCategory (ModuleCat.{u} (baseRing S)),
      ((tensorBase S).obj (((tensorBase S).obj P).obj Q)).obj Z ⟶
        ((tensorBase S).obj P).obj (((tensorBase S).obj Q).obj Z))
    (aB : ∀ U V Z : DerivedCategory (SheafOfModules.{u} (structureSheafRing W)),
      ((derivedTensorProductFunctor W.sheaf).obj
          (((derivedTensorProductFunctor W.sheaf).obj U).obj V)).obj Z ⟶
        ((derivedTensorProductFunctor W.sheaf).obj U).obj
          (((derivedTensorProductFunctor W.sheaf).obj V).obj Z))
    (haA : ∀ {P P' Q Q' Z Z' : DerivedCategory (ModuleCat.{u} (baseRing S))} (k : P ⟶ P')
        (l : Q ⟶ Q') (m : Z ⟶ Z'),
      (Functor.uncurry.obj (tensorBase S)).map
            ((Functor.uncurry.obj (tensorBase S)).map (k ×ₘ l) ×ₘ m) ≫ aA P' Q' Z' =
        aA P Q Z ≫
          (Functor.uncurry.obj (tensorBase S)).map
            (k ×ₘ (Functor.uncurry.obj (tensorBase S)).map (l ×ₘ m)))
    (haB : ∀ {U U' V V' Z Z' : DerivedCategory (SheafOfModules.{u} (structureSheafRing W))}
        (k : U ⟶ U') (l : V ⟶ V') (m : Z ⟶ Z'),
      (Functor.uncurry.obj (derivedTensorProductFunctor W.sheaf)).map
            ((Functor.uncurry.obj (derivedTensorProductFunctor W.sheaf)).map (k ×ₘ l) ×ₘ m) ≫
          aB U' V' Z' =
        aB U V Z ≫
          (Functor.uncurry.obj (derivedTensorProductFunctor W.sheaf)).map
            (k ×ₘ (Functor.uncurry.obj (derivedTensorProductFunctor W.sheaf)).map (l ×ₘ m)))
    (hα : ∀ P Q Z : DerivedCategory (ModuleCat.{u} (baseRing S)),
      κW.tensorComparison.app ((Functor.uncurry.obj (tensorBase S)).obj (P, Q), Z) ≫
          (Functor.uncurry.obj (derivedTensorProductFunctor W.sheaf)).map
              (κW.tensorComparison.app (P, Q) ×ₘ 𝟙 (κW.pullback.obj Z)) ≫
            aB (κW.pullback.obj P) (κW.pullback.obj Q) (κW.pullback.obj Z) =
        κW.pullback.map (aA P Q Z) ≫
          κW.tensorComparison.app (P, (Functor.uncurry.obj (tensorBase S)).obj (Q, Z)) ≫
            (Functor.uncurry.obj (derivedTensorProductFunctor W.sheaf)).map
              (𝟙 (κW.pullback.obj P) ×ₘ κW.tensorComparison.app (Q, Z)))
    (hπ : CupProductPullbackCompatible κX κW π)
    (ξ : baseShift S i ⟶ (sectionsOverBase a).obj 𝒢) :
    ((tensorBase S).map (cupWithClassOverBase κX 𝒢 ℱ i ξ)).app
            ((sectionsOverBase b).obj ℰ) ≫
        kunnethOverBase κW π ρ (((derivedTensorProductFunctor X.sheaf).obj 𝒢).obj ℱ) ℰ ≫
          (sectionsOverBase f).map
              ((Functor.uncurry.obj (derivedTensorProductFunctor W.sheaf)).map
                (pullbackTensorComparisonApp p 𝒢 ℱ ×ₘ 𝟙 ((derivedPullback q).obj ℰ))) ≫
            (sectionsOverBase f).map
              (aB ((derivedPullback p).obj 𝒢) ((derivedPullback p).obj ℱ)
                ((derivedPullback q).obj ℰ)) =
      (Functor.uncurry.obj (tensorBase S)).map
          ((baseShiftTensorIso S i ((sectionsOverBase a).obj ℱ)).inv ×ₘ
            𝟙 ((sectionsOverBase b).obj ℰ)) ≫
        aA (baseShift S i) ((sectionsOverBase a).obj ℱ) ((sectionsOverBase b).obj ℰ) ≫
          ((tensorBase S).obj (baseShift S i)).map (kunnethOverBase κW π ρ ℱ ℰ) ≫
            (baseShiftTensorIso S i
              ((sectionsOverBase f).obj
                (((derivedTensorProductFunctor W.sheaf).obj
                  ((derivedPullback p).obj ℱ)).obj ((derivedPullback q).obj ℰ)))).hom ≫
              cupWithClassOverBase κW ((derivedPullback p).obj 𝒢)
                (((derivedTensorProductFunctor W.sheaf).obj ((derivedPullback p).obj ℱ)).obj
                  ((derivedPullback q).obj ℰ)) i (ξ ≫ π 𝒢)

Sources

LeanStacks.Cohomology.DerivedKunneth.kunnethMap · Stacks.Cohomology.DerivedKunneth.kunnethMap_natural_left · Stacks.Cohomology.DerivedKunneth.kunnethMap_natural_right · Stacks.Cohomology.GlobalKunneth.kunnethGlobalMapCanonical · Stacks.Cohomology.GlobalKunneth.kunnethGlobalMapCanonical_naturality · Stacks.Cohomology.GlobalKunneth.kunnethGlobalMapSchemeCanonical · Stacks.Cohomology.GlobalKunneth.kunnethGlobalMapSchemeCanonical_naturality · Stacks.Cohomology.DerivedKunneth.isIso_kunnethMapScheme

Section36.24 Künneth formula, III #

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

Tag 0G4A, the section

Tag 0G4A in the Stacks Project.

Stacks.Cohomology.BoxKunneth.boxProductObj_module, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/BoxTotalSection.lean, line 135. The attribute's comment: “the display F ⊠ G = p^*F ⊗_{O_{X ×_S Y}} q^*G that opens the section, including that the tensor product is the nonderived one; the bifunctoriality of ⊠ is Tag 0G46, AlgebraicGeometry.FiniteOrderDifferentialOperatorCategory.boxProductFunctor”.

𝓕 ⊠ 𝓖 = p^*𝓕 ⊗_{𝒪_{X ×_S Y}} q^*𝓖, the definition [Stacks, Section 0G4A] opens with: the tensor product, on X ×_S Y, of the two pullbacks along the projections. The tensor product is the nonderived one, Stacks.SheafOfModules.TensorStalkRingedSpace.tensorSheaf; the section says explicitly that, contrary to a later section, the nonderived product is meant.

theorem boxProductObj_module (F : FiniteOrderDifferentialOperatorCategory a)
    (G : FiniteOrderDifferentialOperatorCategory b) :
    (boxProductObj F G).module =
      (((Stacks.SheafOfModules.Tensor.sheafTensor
          ⟨(((pullback a b).toRingedSpace)).presheaf, (((pullback a b).toRingedSpace)).IsSheaf⟩).obj
            (((Scheme.Modules.pullback (pullback.fst a b)).obj F.module))).obj
        (((Scheme.Modules.pullback (pullback.snd a b)).obj G.module)))

Stacks.Cohomology.BoxKunneth.boxDoubleComplex, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/BoxTotalSection.lean, line 160. The attribute's comment: “the double complex displayed in the section: the bicomplex (i, j) ↦ F^i ⊠ G^j of finite-order differential operators on X ×_S Y / S. No boundedness is needed for the double complex itself; its total complex, Stacks.Cohomology.BoxKunneth.boxTotal, needs both factors strictly bounded below”.

The double complex 𝓕^i ⊠ 𝓖^j of [Stacks, Section 0G4A]: the bicomplex obtained by applying the box product of [Stacks, Tag 0G46] to two ℤ-indexed complexes of quasi-coherent modules with finite-order differential operators as differentials, by the construction of [Stacks, Tag 0A5J]. Its horizontal differential is d_1 = d_𝓕 ⊠ 1 and its vertical one is d_2 = 1 ⊠ d_𝓖; both are morphisms of the category of finite-order differential operators on X ×_S Y / S, which is the section's assertion that the maps of the diagram are differential operators of finite order there.

abbrev boxDoubleComplex :
    HomologicalComplex₂ (FiniteOrderDifferentialOperatorCategory (pullback.fst a b ≫ a))
      (ComplexShape.up ℤ) (ComplexShape.up ℤ)

Stacks.Cohomology.BoxKunneth.boxDoubleComplex_X_X, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/BoxTotalSection.lean, line 168. The attribute's comment: “the entries of the displayed double complex”.

The term of the double complex in degree (i, j) is 𝓕^i ⊠ 𝓖^j.

theorem boxDoubleComplex_X_X (i j : ℤ) :
    ((boxDoubleComplex a b K L).X i).X j = boxProductObj (K.X i) (L.X j)

Stacks.Cohomology.BoxKunneth.boxDoubleComplex_d_f, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/BoxTotalSection.lean, line 178. The attribute's comment: “the display d_1^{i, j} = d^i_F ⊠ 1, the horizontal differential of the double complex”.

The horizontal differential of the double complex is d_1^{i, j} = d^i_𝓕 ⊠ 1, the first of the two formulas written out in [Stacks, Section 0G4A]. There is no sign: the signs of [Stacks, Tag 012Z] enter only in the total complex, where Stacks.Cohomology.BoxKunneth.boxTotal_d records them.

theorem boxDoubleComplex_d_f (i i' j : ℤ) :
    ((boxDoubleComplex a b K L).d i i').f j = boxHom (K.d i i') (𝟙 (L.X j))

Stacks.Cohomology.BoxKunneth.boxDoubleComplex_X_d, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/BoxTotalSection.lean, line 186. The attribute's comment: “the display d_2^{i, j} = 1 ⊠ d^j_G, the vertical differential of the double complex”.

The vertical differential of the double complex is d_2^{i, j} = 1 ⊠ d^j_𝓖, the second of the two formulas written out in [Stacks, Section 0G4A], again with no sign.

theorem boxDoubleComplex_X_d (i j j' : ℤ) :
    ((boxDoubleComplex a b K L).X i).d j j' = boxHom (𝟙 (K.X i)) (L.d j j')

Stacks.Cohomology.BoxKunneth.boxDoubleComplex_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/BoxTotalSection.lean, line 195. The attribute's comment: “commutativity of the squares of the displayed diagram, i.e. that (i, j) ↦ F^i ⊠ G^j with those two differentials really is a double complex”.

The squares of the diagram displayed in [Stacks, Section 0G4A] commute: boxing with the identity in one variable is natural in the other, so (1 ⊠ d_𝓖) ∘ (d_𝓕 ⊠ 1) and (d_𝓕 ⊠ 1) ∘ (1 ⊠ d_𝓖) agree as operators 𝓕^i ⊠ 𝓖^j ⟶ 𝓕^{i'} ⊠ 𝓖^{j'}.

theorem boxDoubleComplex_comm (i i' j j' : ℤ) :
    boxHom (K.d i i') (𝟙 (L.X j)) ≫ boxHom (𝟙 (K.X i')) (L.d j j') =
      boxHom (𝟙 (K.X i)) (L.d j j') ≫ boxHom (K.d i i') (𝟙 (L.X j'))

Stacks.Cohomology.BoxKunneth.boxTotal_eq_total, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/BoxTotalSection.lean, line 211. The attribute's comment: “the sentence fixing the notation Tot(F^• ⊠ G^•) as the total complex of the displayed double complex; the sign convention of that total complex is Tag 012Z, recorded by Stacks.Cohomology.BoxKunneth.boxTotal_d”.

Tot(𝓕^• ⊠ 𝓖^•) is the total complex of the double complex 𝓕^i ⊠ 𝓖^j, which is what the notation means in [Stacks, Section 0G4A]. Stacks.Cohomology.BoxKunneth.boxTotal is formed as HomologicalComplex.mapBifunctor, the total complex of the bicomplex obtained by applying the box product; this identifies the two.

theorem boxTotal_eq_total
    [HomologicalComplex.HasMapBifunctor K L (boxProductCurried a b) (ComplexShape.up ℤ)] :
    boxTotal a b K L n₁ n₂ = (boxDoubleComplex a b K L).total (ComplexShape.up ℤ)

Stacks.Cohomology.BoxKunneth.isQuasicoherent_boxTotal_X, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/BoxTotalSection.lean, line 222. The attribute's comment: “the assertion that Tot(F^• ⊠ G^•) has quasi-coherent terms”.

The terms of Tot(𝓕^• ⊠ 𝓖^•) are quasi-coherent 𝒪_{X ×_S Y}-modules, the first of the two closing assertions of the paragraph of [Stacks, Section 0G4A] that fixes the notation. In degree n the term is a finite biproduct of the 𝓕^i ⊠ 𝓖^j with i + j = n, and the external tensor product of two quasi-coherent modules is quasi-coherent (AlgebraicGeometry.isQuasicoherent_externalTensorProduct).

theorem isQuasicoherent_boxTotal_X (n : ℤ) :
    ((boxTotal a b K L n₁ n₂).X n).module.IsQuasicoherent

Stacks.Cohomology.BoxKunneth.exists_isGlobalDiffOpOfOrder_boxTotal_d, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/BoxTotalSection.lean, line 233. The attribute's comment: “the assertion that the differentials of Tot(F^• ⊠ G^•) are differential operators of finite order on X ×_S Y / S”.

The differentials of Tot(𝓕^• ⊠ 𝓖^•) are differential operators of finite order on X ×_S Y / S, the second of the two closing assertions of the paragraph of [Stacks, Section 0G4A] that fixes the notation: for each pair of degrees there is a k for which the differential is a global differential operator of order ≤ k relative to the structure map of X ×_S Y / S.

theorem exists_isGlobalDiffOpOfOrder_boxTotal_d (n m : ℤ) :
    ∃ k, DiffOp.IsGlobalDiffOpOfOrder (pullback.fst a b ≫ a).relativeStructureSheafMap k
      ((boxTotal a b K L n₁ n₂).d n m).1

Tag 0G4B, an equation

Tag 0G4B in the Stacks Project.

Stacks.Cohomology.BoxKunneth.relativeBoxKunnethMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/BoxTotalKunnethMap.lean, line 123. The attribute's comment: “the map, corrected: Tot(F ⊠ G) is formed under strict boundedness below of both complexes, without which it does not exist in the category of finite-order differential operators; and steps (1) to (3) are taken with the derived inverse image Lp^*, the canonical comparison Lp^*F ⟶ p^{-1}F being inserted into step (4); the step-(5) comparison Tot(p^{-1}F ⊗ q^{-1}G) ⟶ Tot(F ⊠ G) is Stacks.Cohomology.BoxKunneth.boxTotalComparison”.

The relative Künneth map of the box product

Ra_*(𝓕^•) ⊗^𝐋_{𝒪_S} Rb_*(𝓖^•) ⟶ Rf_*(Tot(𝓕^• ⊠ 𝓖^•)),

for 𝓕^• on X/S and 𝓖^• on Y/S complexes of quasi-coherent modules with differentials differential operators of finite order, both strictly bounded below, and f the structure morphism of X ×_S Y. It is the Künneth map of [Stacks, Tag 0FLP] for the inverse-image ringed spaces, followed by Rf_* of steps (4) and (5).

def relativeBoxKunnethMap :
    ((derivedTensorProductFunctor.{u, u + 1} (SheafedSpace.sheaf S.toRingedSpace)).obj
          ((derivedPushforward.{u, u + 1, u + 1} (inverseImageBaseProjection a)).obj
            (DerivedCategory.Q.obj (leftComplex a K)))).obj
        ((derivedPushforward.{u, u + 1, u + 1} (inverseImageBaseProjection b)).obj
          (DerivedCategory.Q.obj (rightComplex b L))) ⟶
      (derivedPushforward.{u, u + 1, u + 1}
          (inverseImageBaseProjection (pullback.fst a b ≫ a))).obj
        (DerivedCategory.Q.obj (boxTotalModules a b K L n₁ n₂))

Stacks.Cohomology.BoxKunneth.relativeBoxKunnethMap_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/BoxTotalKunnethMap.lean, line 146. The attribute's comment: “the map is the Künneth map of Tag 0FLP for the inverse-image ringed spaces, which is steps (1) to (3) with Lp^* for p^{-1}, followed by Rf_* of steps (4) and (5)”.

The relative map is the three-step map of [Stacks, Tag 0FLP] followed by the last two steps. Steps (1) to (3), the two pullback maps and the relative cup product, are the Künneth map of [Stacks, Tag 0FLP] for the projections of (W, f^{-1}𝒪_S) to (X, a^{-1}𝒪_S) and (Y, b^{-1}𝒪_S); steps (4) and (5) are boxTotalDerivedComparison.

theorem relativeBoxKunnethMap_eq :
    relativeBoxKunnethMap a b K L n₁ n₂ =
      Stacks.Cohomology.DerivedKunneth.kunnethMap (inverseImageBaseProjection a)
          (inverseImageBaseProjection b) (fstProjection a b) (sndProjection a b)
          (inverseImageBaseProjection (pullback.fst a b ≫ a))
          (fstProjection_comp a b) (sndProjection_comp a b)
          (DerivedCategory.Q.obj (leftComplex a K)) (DerivedCategory.Q.obj (rightComplex b L)) ≫
        (derivedPushforward (inverseImageBaseProjection (pullback.fst a b ≫ a))).map
          (boxTotalDerivedComparison a b K L n₁ n₂ (boxTotalComparison a b K L n₁ n₂))

Tag 0FLR, an equation

Tag 0FLR in the Stacks Project.

Stacks.Cohomology.BoxKunneth.globalBoxCupProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/BoxTotalKunnethMapUnbounded.lean, line 249. The attribute's comment: “the map, as the composite of the five maps of the source: steps (1) to (3) are the global Künneth map of Tag 0G7V at the global cup product globalCupProductCanonical of Section 0FKU, the pullbacks being Lp^*, which computes p^{-1} along (X ×_S Y, f^{-1}𝒪_S) ⟶ (X, a^{-1}𝒪_S); steps (4) and (5) are boxTotalComplexDerivedComparison”.

The global cup product of [Stacks, Tag 0FLR]

RΓ(X, 𝓕^•) ⊗^𝐋_A RΓ(Y, 𝓖^•) ⟶ RΓ(X ×_S Y, Tot(𝓕^• ⊠ 𝓖^•))

in D(A) for A = Γ(S, 𝒪_S), for 𝓕^• on X/S and 𝓖^• on Y/S arbitrary ℤ-indexed complexes of quasi-coherent modules whose differentials are differential operators of finite order. It is the composite of the two pullback maps on derived global sections, the global cup product of [Stacks, Section 0FKU] (together these are the global Künneth map Stacks.Cohomology.GlobalKunneth.kunnethGlobalMapCanonical of [Stacks, Tag 0G7V] for the inverse-image ringed spaces), and derived global sections of steps (4) and (5).

def globalBoxCupProduct :
    ((tensorBase S.toRingedSpace).obj
          ((sectionsOverBase (inverseImageBaseProjection a)).obj
            (DerivedCategory.Q.obj (leftComplex a K)))).obj
        ((sectionsOverBase (inverseImageBaseProjection b)).obj
          (DerivedCategory.Q.obj (rightComplex b L))) ⟶
      (sectionsOverBase (inverseImageBaseProjection (pullback.fst a b ≫ a))).obj
        (DerivedCategory.Q.obj
          (HomologicalComplex.mapBifunctor K L (boxProductRelativeCurried a b)
            (ComplexShape.up ℤ)))

Stacks.Cohomology.BoxKunneth.globalBoxCupProduct_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/BoxTotalKunnethMapUnbounded.lean, line 272. The attribute's comment: “the map is the composite of steps (1) to (3), the global Künneth map of Tag 0G7V at the global cup product of Section 0FKU, with derived global sections of steps (4) and (5)”.

The map is the five-step composite: the global Künneth map of [Stacks, Tag 0G7V] at the global cup product of [Stacks, Section 0FKU], followed by derived global sections of steps (4) and (5).

theorem globalBoxCupProduct_eq :
    globalBoxCupProduct a b K L =
      kunnethGlobalMap (inverseImageBaseProjection a) (inverseImageBaseProjection b)
          (fstProjection a b) (sndProjection a b)
          (inverseImageBaseProjection (pullback.fst a b ≫ a))
          (fstProjection_comp a b) (sndProjection_comp a b)
          (globalCupProductCanonical S.toRingedSpace)
          (DerivedCategory.Q.obj (leftComplex a K)) (DerivedCategory.Q.obj (rightComplex b L)) ≫
        (sectionsOverBase (inverseImageBaseProjection (pullback.fst a b ≫ a))).map
          (boxTotalComplexDerivedComparison a b K L)

Tag 0FLT, a lemma

Tag 0FLT in the Stacks Project.

Stacks.Cohomology.BoxKunnethFlat.isIso_globalBoxCupProduct_of_isFlatOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/BoxKunnethFlat/Isomorphism.lean, line 131. The attribute's comment: “the whole statement under exactly the source's hypotheses: S affine; X, Y quasi-compact with affine diagonal; F^• bounded (terms vanish outside some [m₁, m₂]); G^• bounded below (terms vanish below some n); every term of F^• and of G^• flat over S. The cup product is the parameter-free map of Tag 0FLR built from the canonical global cup product; nothing the source proves is assumed”.

Stacks Project, Tag 0FLT. Let a : X ⟶ S and b : Y ⟶ S be morphisms of schemes and let 𝓕^• and 𝓖^• be complexes of quasi-coherent 𝒪_X-, respectively 𝒪_Y-modules whose differentials are differential operators of finite order on X/S and on Y/S. The cup product RΓ(X, 𝓕^•) ⊗^𝐋_A RΓ(Y, 𝓖^•) ⟶ RΓ(X ×_S Y, Tot(𝓕^• ⊠ 𝓖^•)) of [Stacks, Tag 0FLR] is an isomorphism in D(A) if

S = Spec(A) is affine,

X and Y are quasi-compact with affine diagonal,

𝓕^• is bounded,

𝓖^• is bounded below,

every 𝓕^n is S-flat, and

every 𝓖^m is S-flat.

Here the cup product is Stacks.Cohomology.BoxKunneth.globalBoxCupProduct, built from the canonical global cup product, with A the ring of global sections of S.

theorem isIso_globalBoxCupProduct_of_isFlatOver [IsAffine S] [CompactSpace X] [CompactSpace Y]
    [IsAffineHom (pullback.diagonal (terminal.from X))]
    [IsAffineHom (pullback.diagonal (terminal.from Y))]
    (K : CochainComplex (FiniteOrderDifferentialOperatorCategory a) ℤ)
    (L : CochainComplex (FiniteOrderDifferentialOperatorCategory b) ℤ)
    (hK : ∃ m₁ m₂ : ℤ, K.IsStrictlyGE m₁ ∧ K.IsStrictlyLE m₂)
    (hL : ∃ n : ℤ, L.IsStrictlyGE n)
    (hKflat : ∀ n, IsFlatOver a.toLRSHom.toShHom (K.X n).module)
    (hLflat : ∀ n, IsFlatOver b.toLRSHom.toShHom (L.X n).module) :
    IsIso (globalBoxCupProduct a b K L)

Stacks.Cohomology.BoxKunneth.isIso_globalBoxKunnethMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/BoxTotalKunnethIsomorphism.lean, line 194. The attribute's comment: “the isomorphism; three inputs are carried, so the geometric hypotheses are not consumed: hκ, invertibility of the global cup product on the affine base, which no bare GlobalCupProduct has; hrel, Tag 0FLQ at the two inverse-image complexes; hstep, steps (4) and (5), which the tag's termwise relative S-flatness cannot discharge in this library”.

[Stacks, Tag 0FLT]. Let a : X ⟶ S and b : Y ⟶ S be morphisms of schemes with S affine, let A = Γ(S, 𝒪_S), and let 𝓕^• on X/S and 𝓖^• on Y/S be complexes of quasi-coherent modules with differentials differential operators of finite order. If X and Y are quasi-compact with affine diagonal, 𝓕^• is bounded, 𝓖^• is bounded below, and every term of 𝓕^• and of 𝓖^• is flat over S, then the cup product of [Stacks, Tag 0FLR]

RΓ(X, 𝓕^•) ⊗^𝐋_A RΓ(Y, 𝓖^•) ⟶ RΓ(X ×_S Y, Tot(𝓕^• ⊠ 𝓖^•))

is an isomorphism in D(A).

The three inputs of the proof are carried as the hypotheses hκ, hrel and hstep, and the geometric hypotheses are therefore not consumed; the implementation notes of this file say what each of the three is and what the source's own dévissage would need in addition. hκ is the invertibility of the A-linear global cup product on the affine base, hrel is [Stacks, Tag 0FLQ] at the two inverse-image complexes, and hstep is the invertibility of steps (4) and (5), in which the source consumes the flatness of the terms. What is proved here is that the three suffice.

theorem isIso_globalBoxKunnethMap [IsAffine S] [CompactSpace X] [CompactSpace Y]
    [IsAffineHom (pullback.diagonal (terminal.from X))]
    [IsAffineHom (pullback.diagonal (terminal.from Y))]
    (_hK : ∀ n, IsFlatOver a.toLRSHom.toShHom (K.X n).module)
    (_hL : ∀ n, IsFlatOver b.toLRSHom.toShHom (L.X n).module)
    (κ : GlobalCupProduct S.toRingedSpace)
    (hκ : IsIso (κ.app
      ((derivedPushforward (inverseImageBaseProjection a)).obj
          (DerivedCategory.Q.obj (leftComplex a K)),
        (derivedPushforward (inverseImageBaseProjection b)).obj
          (DerivedCategory.Q.obj (rightComplex b L)))))
    (hrel : IsIso (Stacks.Cohomology.DerivedKunneth.kunnethMap (inverseImageBaseProjection a)
      (inverseImageBaseProjection b) (fstProjection a b) (sndProjection a b)
      (inverseImageBaseProjection (pullback.fst a b ≫ a)) (fstProjection_comp a b)
      (sndProjection_comp a b) (DerivedCategory.Q.obj (leftComplex a K))
      (DerivedCategory.Q.obj (rightComplex b L))))
    (hstep : IsIso (boxTotalDerivedComparison a b K L n₁ n₂
      (boxTotalComparison a b K L n₁ n₂))) :
    IsIso (globalBoxKunnethMap a b K L n₁ n₂ κ)

Sources

LeanStacks.Cohomology.BoxKunneth.boxProductObj_module · Stacks.Cohomology.BoxKunneth.boxDoubleComplex · Stacks.Cohomology.BoxKunneth.boxDoubleComplex_X_X · Stacks.Cohomology.BoxKunneth.boxDoubleComplex_d_f · Stacks.Cohomology.BoxKunneth.boxDoubleComplex_X_d · Stacks.Cohomology.BoxKunneth.boxDoubleComplex_comm · Stacks.Cohomology.BoxKunneth.boxTotal_eq_total · Stacks.Cohomology.BoxKunneth.isQuasicoherent_boxTotal_X

Section36.25 Künneth formula for Ext #

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

Tag 0FXY, an equation

Tag 0FXY in the Stacks Project.

Stacks.Cohomology.DerivedKunnethExt.kunnethExtMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/KunnethMapForExt.lean, line 255.

The Künneth morphism for Ext Ra_*R SheafHom(K, K') ⊗^L_{𝒪_S} Rb_*R SheafHom(M, M') ⟶ Rf_*(R SheafHom(K ⊠ M, K' ⊠ M')), Equation 36.25.0.1: the relative Künneth morphism of Stacks 0FLP at the two derived internal homs, followed by the pushforward of Stacks.Cohomology.DerivedKunnethExt.boxSheafHomMap. It is defined for arbitrary K, K' ∈ D(𝒪_X) and M, M' ∈ D(𝒪_Y).

def kunnethExtMap (K K' : DerivedCategory (Mod X.sheaf))
    (M M' : DerivedCategory (Mod Y.sheaf)) :
    tensorObj S ((derivedPushforwardFunctor a).obj (sheafHomObj X K K'))
        ((derivedPushforwardFunctor b).obj (sheafHomObj Y M M')) ⟶
      (derivedPushforwardFunctor f).obj
        (sheafHomObj W (boxProd p q K M) (boxProd p q K' M'))

Tag 0FXZ, a lemma

Tag 0FXZ in the Stacks Project.

Stacks.Cohomology.DerivedKunnethExt.isIso_kunnethExtMap_fibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/KunnethExtFibreProduct.lean, line 61.

Let a : X ⟶ S and b : Y ⟶ S be quasi-compact and quasi-separated morphisms of schemes, and let X and Y be Tor independent over S. Let W = X ×_S Y with its two projections p and q and f = p ≫ a. If K ∈ D(𝒪_X) is perfect, K' ∈ D_QCoh(𝒪_X), M ∈ D(𝒪_Y) is perfect and M' ∈ D_QCoh(𝒪_Y), then the Künneth morphism for Ext (Equation 36.25.0.1)

Ra_*R𝓗om(K, K') ⊗^𝐋_{𝒪_S} Rb_*R𝓗om(M, M') ⟶ Rf_*(R𝓗om(K ⊠ M, K' ⊠ M'))

is an isomorphism.

theorem isIso_kunnethExtMap_fibreProduct
    [QuasiCompact a] [QuasiSeparated a] [QuasiCompact b] [QuasiSeparated b]
    (hTor : AlgebraicGeometry.TorIndependent a b)
    (K K' : DerivedCategory X.Modules) (M M' : DerivedCategory Y.Modules)
    (hK : RingedSpace.IsPerfect (X := X.toRingedSpace) K)
    (hK' : IsDQCoh (R := X.ringCatSheaf) K')
    (hM : RingedSpace.IsPerfect (X := Y.toRingedSpace) M)
    (hM' : IsDQCoh (R := Y.ringCatSheaf) M') :
    IsIso (kunnethExtMap a.toLRSHom.toShHom b.toLRSHom.toShHom
      (pullback.fst a b).toLRSHom.toShHom (pullback.snd a b).toLRSHom.toShHom
      (pullback.fst a b ≫ a).toLRSHom.toShHom rfl
      (Stacks.Cohomology.GlobalKunneth.toShHom_pullback_condition a b) K K' M M')

Stacks.Cohomology.DerivedKunnethExt.isIso_kunnethExtMap_cartesian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/KunnethExtIsomorphism.lean, line 279. The attribute's comment: “for a and b quasi-compact and quasi-separated, X and Y Tor independent over S, K and M perfect and K', M' in D_QCoh, the Künneth morphism for Ext of Tag 0FXY at a cartesian square of schemes is invertible. Both steps of the source's two-step proof are carried as explicit hypotheses and the source's geometric hypotheses are consequently not consumed: hkunneth is the invertibility of the relative Künneth morphism of Tag 0FLP at the pair (RSheafHom(K,K'), RSheafHom(M,M')), which is Tag 0FLQ. That tag is carried, for this same kunnethMap, by isIso_kunnethMap_of_projectionFormulas_of_baseChange, but itself only conditionally, on four named inputs: the projection formula of Tag 08EU for a and for p, the Tor-independent base-change comparison of Tag 08IB for the square, and the Tag 079U/0D5S monoidality coherence. So hkunneth is exactly that carrier's conclusion and is obtainable from it once those four are supplied; it is carried here as one hypothesis rather than four. Perfectness of K and M does not discharge them, because 0FLQ is applied to RSheafHom(K,K') and RSheafHom(M,M'), which for K' and M' merely in D_QCoh are quasi-coherent and not perfect. And hbox is the invertibility of the canonical comparison Lp^RSheafHom(K,K') (x)^L Lq^RSheafHom(M,M') -> RSheafHom(K [x] M, K' [x] M'), which is where the source uses perfectness, through the identification RSheafHom(K,K') = K' (x)^L K^dual of Cohomology Tag 08DQ, of which the repository carries only the statement that the dual of a perfect object is perfect, and which also absorbs the parenthetical verification the source omits that the identifications give the same map. What is proved here is that the two steps suffice, which in the source is the word hence”.

Stacks 0FXZ. Let a : X ⟶ S and b : Y ⟶ S be morphisms of schemes which are quasi-compact and quasi-separated, let X and Y be Tor independent over S, and let W = X ×_S Y with its two projections p and q. If K ∈ D(𝒪_X) is perfect, K' ∈ D_{QCoh}(𝒪_X), M ∈ D(𝒪_Y) is perfect and M' ∈ D_{QCoh}(𝒪_Y), then the Künneth morphism for Ext of Stacks 0FXY,

Ra_*R SheafHom(K, K') ⊗^𝐋_{𝒪_S} Rb_*R SheafHom(M, M') ⟶ Rf_*(R SheafHom(K ⊠ M, K' ⊠ M')),

is an isomorphism.

The two steps of the source's proof are carried as the hypotheses hkunneth and hbox, and the geometric hypotheses are therefore not consumed; the implementation notes of this file say what each of the two steps is, why neither is available in the library, and where the verification the source omits sits. hkunneth is Stacks 0FLQ at the pair of derived internal homs and hbox is the identification of Cohomology, Stacks 08DQ together with that verification.

theorem isIso_kunnethExtMap_cartesian (hW : IsPullback p q a b)
    [QuasiCompact a] [QuasiSeparated a] [QuasiCompact b] [QuasiSeparated b]
    (_htor : AlgebraicGeometry.TorIndependent a b)
    (K K' : DerivedCategory X.Modules) (M M' : DerivedCategory Y.Modules)
    (_hK : RingedSpace.IsPerfect (X := X.toRingedSpace) K)
    (_hK' : IsDQCoh (R := X.ringCatSheaf) K')
    (_hM : RingedSpace.IsPerfect (X := Y.toRingedSpace) M)
    (_hM' : IsDQCoh (R := Y.ringCatSheaf) M')
    (hkunneth : IsIso (Stacks.Cohomology.DerivedKunneth.kunnethMap a.toLRSHom.toShHom
      b.toLRSHom.toShHom p.toLRSHom.toShHom q.toLRSHom.toShHom (p ≫ a).toLRSHom.toShHom rfl
      (toShHom_isPullback_w a b p q hW)
      (sheafHomObj X.toRingedSpace K K') (sheafHomObj Y.toRingedSpace M M')))
    (hbox : IsIso (boxSheafHomMap p.toLRSHom.toShHom q.toLRSHom.toShHom K K' M M')) :
    IsIso (kunnethExtMap a.toLRSHom.toShHom b.toLRSHom.toShHom p.toLRSHom.toShHom
      q.toLRSHom.toShHom (p ≫ a).toLRSHom.toShHom rfl (toShHom_isPullback_w a b p q hW)
      K K' M M')

Sources

LeanStacks.Cohomology.DerivedKunnethExt.kunnethExtMap · Stacks.Cohomology.DerivedKunnethExt.isIso_kunnethExtMap_fibreProduct · Stacks.Cohomology.DerivedKunnethExt.isIso_kunnethExtMap_cartesian

Section36.26 Cohomology and base change, V #

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

Tag 0DJ7, an equation

Tag 0DJ7 in the Stacks Project.

AlgebraicGeometry.baseChangeCohomologyMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/StalkCohomologyMap.lean, line 106.

Stacks 0DJ7. The canonical pointwise base-change map on stalkwise cohomology induced by a morphism φ : L(g')^* K ⟶ K' over a commutative square of schemes. No flatness, cartesianness or Tor independence is required.

def baseChangeCohomologyMap {X X' S S' : Scheme.{u}} (f : X ⟶ S) (g : S' ⟶ S)
    (f' : X' ⟶ S') (g' : X' ⟶ X) (w : g' ≫ f = f' ≫ g)
    [HasDerivedCategory.{w'} X.Modules] [HasDerivedCategory.{w'} X'.Modules]
    (K : DerivedCategory X.Modules) (K' : DerivedCategory X'.Modules)
    (φ : (Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
      g'.toLRSHom.toShHom).obj K ⟶ K')
    (x' : X')
    [HasDerivedCategory.{w'} (ModuleCat.{u} (S.presheaf.stalk (f (g' x'))))]
    [HasDerivedCategory.{w'} (ModuleCat.{u} (X.presheaf.stalk (g' x')))]
    [HasDerivedCategory.{w'} (ModuleCat.{u} (S'.presheaf.stalk (f' x')))]
    [HasDerivedCategory.{w'} (ModuleCat.{u} (X'.presheaf.stalk x'))]
    (n : ℤ)

Tag 0DJ8, a lemma

Tag 0DJ8 in the Stacks Project.

AlgebraicGeometry.BaseChangeChart, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/AffineChart.lean, line 80. The attribute's comment: “the Cartesian affine-open chart quantified over in (2) and (3)”.

A Cartesian affine-open chart for a base-change square of schemes. This is the quadruple U, V, V', U' of Stacks 0DJ8 (2): affine opens U ⊆ X and V' ⊆ S' both mapping into an affine open V ⊆ S, together with U' = V' ×_V U, the last expressed by the pushout square of coordinate rings.

public structure BaseChangeChart {X X' S S' : Scheme.{u}} (f : X ⟶ S) (g : S' ⟶ S)
    (f' : X' ⟶ S') (g' : X' ⟶ X)

AlgebraicGeometry.BaseChangeChart.isOpenImmersion_incU', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/AffineChart.lean, line 146. The attribute's comment: “the U' of a chart is an open of X'”.

U' is an open of X'. The structure imposes no open-immersion hypothesis on Spec 𝒪_{X'}(U') ⟶ X': once the outer square is cartesian the chart data determine that morphism uniquely, and it is then automatically an open immersion, being the base change of U ⊆ X and V' ⊆ S' over V ⊆ S.

public theorem isOpenImmersion_incU' (sq : IsPullback g' f' f g)
    (ch : BaseChangeChart f g f' g') : IsOpenImmersion ch.incU'

AlgebraicGeometry.BaseChangeChart.ofAffineOpens, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/AffineChart.lean, line 177. The attribute's comment: “the chart on a triple of affine opens”.

The chart on given affine opens. For affine opens U ⊆ X, V ⊆ S, V' ⊆ S' with f(U) ⊆ V and g(V') ⊆ V, the coordinate rings and the tensor product 𝒪_X(U) ⊗_{𝒪_S(V)} 𝒪_{S'}(V') form a chart, its U' being the canonical open V' ×_V U of X'.

public def ofAffineOpens (sq : IsPullback g' f' f g)
    (U : X.Opens) (V : S.Opens) (V' : S'.Opens)
    (hU : IsAffineOpen U) (hV : IsAffineOpen V) (hV' : IsAffineOpen V')
    (hUV : U ≤ f ⁻¹ᵁ V) (hV'V : V' ≤ g ⁻¹ᵁ V) : BaseChangeChart f g f' g'

AlgebraicGeometry.exists_baseChangeChart_covering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/AffineChart.lean, line 239. The attribute's comment: “every point of X' lies in the U' of a chart, the covering input to (2) ⟹ (3)”.

Every point of X' lies in the U' of a chart. Choose an affine open V ⊆ S around f(g' x'), then an affine open U ⊆ X around g' x' inside f⁻¹V, then an affine open V' ⊆ S' around f' x' inside g⁻¹V; the resulting chart's U' = V' ×_V U contains x', because x' corresponds to a point of U ×_V V' under the cartesian square.

This is the covering input to the step (2) ⟹ (3) of Stacks 0DJ8.

public theorem exists_baseChangeChart_covering {X X' S S' : Scheme.{u}} {f : X ⟶ S}
    {g : S' ⟶ S} {f' : X' ⟶ S'} {g' : X' ⟶ X} (sq : IsPullback g' f' f g) (x' : X') :
    ∃ ch : BaseChangeChart f g f' g', ∃ y : Spec ch.A', ch.incU' y = x'

AlgebraicGeometry.exists_coveringFamily_of_forall_baseChangeChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/AffineChart.lean, line 328. The attribute's comment: “(2) ⟹ (3), for an arbitrary property of charts”.

The step (2) ⟹ (3) of Stacks 0DJ8. If a property of charts holds for every chart then there is a family of charts on which it holds whose opens U' cover X': take the family of all charts and apply exists_baseChangeChart_covering.

The property is left abstract because this step uses nothing about it. Reading P ch as "the comparison map of ch is an isomorphism" turns this into the implication (2) ⟹ (3) of the source, which is the only use intended.

public theorem exists_coveringFamily_of_forall_baseChangeChart {X X' S S' : Scheme.{u}}
    {f : X ⟶ S} {g : S' ⟶ S} {f' : X' ⟶ S'} {g' : X' ⟶ X} (sq : IsPullback g' f' f g)
    (P : BaseChangeChart f g f' g' → Prop) (h : ∀ ch : BaseChangeChart f g f' g', P ch) :
    ∃ 𝒞 : Set (BaseChangeChart f g f' g'), (∀ ch ∈ 𝒞, P ch) ∧
      ∀ x' : X', ∃ ch ∈ 𝒞, ∃ y : Spec ch.A', ch.incU' y = x'

AlgebraicGeometry.BaseChangeChart.cohomologyComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/AffineChartCohomologyComparison.lean, line 248. The attribute's comment: “the comparison map of (2) on a Cartesian affine-open chart, in degree n: the A'-linear map of Tag 0DJ7's ring form for the chart's pushout square of rings”.

The chart comparison in degree n: on a chart with coordinate rings R, A, R', A', the A'-linear map

A' ⊗_{A ⊗_R R'} H^n(RΓ(U,K) ⊗ᴸ_R R') ⟶ H^n(RΓ(U',K'))

given by ringCohomologyComparison for the chart's pushout square of rings.

public def cohomologyComparison (ch : BaseChangeChart f g f' g')
    (K : DerivedCategory X.Modules) (K' : DerivedCategory X'.Modules)
    (φ : (Stacks.Duality.derivedPullback g').obj K ⟶ K') (n : ℤ)

AlgebraicGeometry.BaseChangeChart.cohomologyComparison_tmul_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/AffineChartCohomologyComparison.lean, line 286. The attribute's comment: “the degree-n map of a chart is H^n of the comparison map of (2)”.

The degree-n map of a chart is H^n of the chart comparison: its value on 1 ⊗ m is H^n(comparison) of m, read through the identification of the cohomology of a complex of A'-modules with the cohomology of its restriction to R'.

public theorem cohomologyComparison_tmul_one (ch : BaseChangeChart f g f' g')
    (K : DerivedCategory X.Modules) (K' : DerivedCategory X'.Modules)
    (φ : (Stacks.Duality.derivedPullback g').obj K ⟶ K') (n : ℤ) :
    letI : Algebra ch.R ch.A := ch.a.hom.toAlgebra
    letI : Algebra ch.R ch.R' := ch.b.hom.toAlgebra
    letI : Algebra ch.R ch.A' := (ch.c.hom.comp ch.a.hom).toAlgebra
    letI : Algebra ch.A ch.A' := ch.c.hom.toAlgebra
    letI : Algebra ch.R' ch.A' := ch.d.hom.toAlgebra
    letI : IsScalarTower ch.R ch.A ch.A' := IsScalarTower.of_algebraMap_eq' rfl
    letI : IsScalarTower ch.R ch.R' ch.A' := IsScalarTower.of_algebraMap_eq' ch.isPushout_hom
    ∀ m : baseChangeCohomology (R := ch.R) (R' := ch.R')
      ((affineDerivedSections ch.incU).obj K) n,
      let B := ch.A ⊗[ch.R] ch.R'
      let k : B →+* ch.A' :=
        (Algebra.TensorProduct.lift (IsScalarTower.toAlgHom ch.R ch.A ch.A')
          (IsScalarTower.toAlgHom ch.R ch.R' ch.A') (fun _ _ => Commute.all _ _)).toRingHom
      (ch.cohomologyComparison K K' φ n).hom ((1 : ch.A') ⊗ₜ[B, k] m) =
        (((ModuleCat.restrictScalars ch.d.hom).mapDerivedCategoryHomologyIso n).app
            ((affineDerivedSections ch.incU').obj K')).hom.hom
          (((DerivedCategory.homologyFunctor (ModuleCat.{u} ch.R') n).map
            (ch.comparison K K' φ)).hom m)

AlgebraicGeometry.BaseChangeChart.isIso_comparison_iff_forall_isIso_cohomologyComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/AffineChartCohomologyComparison.lean, line 332. The attribute's comment: “condition (2) at a Cartesian affine-open chart, read degree by degree: the chart comparison is invertible exactly when the A'-linear base-change maps on cohomology of the chart's pushout square of rings are invertible in every degree”.

The chart comparison

RΓ(U,K) ⊗ᴸ_{𝒪_S(V)} 𝒪_{S'}(V') ⟶ RΓ(U',K')

is an isomorphism exactly when, in every degree n, the A'-linear map

A' ⊗_{A ⊗_R R'} H^n(RΓ(U,K) ⊗ᴸ_R R') ⟶ H^n(RΓ(U',K'))

of the chart's pushout square of rings is.

public theorem isIso_comparison_iff_forall_isIso_cohomologyComparison
    (ch : BaseChangeChart f g f' g') (K : DerivedCategory X.Modules)
    (K' : DerivedCategory X'.Modules)
    (φ : (Stacks.Duality.derivedPullback g').obj K ⟶ K') :
    IsIso (ch.comparison K K' φ) ↔
      ∀ n : ℤ, IsIso (ch.cohomologyComparison K K' φ n)

AlgebraicGeometry.BaseChangeChart.isIso_comparison_iff_forall_localized, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/AffineChartCohomologyComparison.lean, line 356. The attribute's comment: “condition (2) at a Cartesian affine-open chart is a pointwise condition on the points of U': invertibility of the localization at each prime of A' of each degree-n map”.

The chart comparison is an isomorphism exactly when, at every prime y of A' = 𝒪_{X'}(U') (that is, at every point of U') and in every degree n, the localization at y of the degree-n map of the chart is an isomorphism.

public theorem isIso_comparison_iff_forall_localized (ch : BaseChangeChart f g f' g')
    (K : DerivedCategory X.Modules) (K' : DerivedCategory X'.Modules)
    (φ : (Stacks.Duality.derivedPullback g').obj K ⟶ K') :
    IsIso (ch.comparison K K' φ) ↔
      ∀ (y : PrimeSpectrum ch.A') (n : ℤ),
        IsIso ((ModuleCat.localizedModuleFunctor.{u} y.asIdeal.primeCompl).map
          (ch.cohomologyComparison K K' φ n))

AlgebraicGeometry.BaseChangeChart.sectionsBaseChangeMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/AffineChartComparisonMap.lean, line 103. The attribute's comment: “the second arrow of the composition in (2): the identification RΓ(U,K) ⊗ᴸ_{𝒪_X(U)} 𝒪_{X'}(U') = RΓ(U', L(g')^*K)”.

The identification in condition (2). On a chart, derived sections of K over U base changed along 𝒪_X(U) ⟶ 𝒪_{X'}(U') compare with derived sections over U' of the derived pullback of K: RΓ(U, K) ⊗ᴸ_{𝒪_X(U)} 𝒪_{X'}(U') ⟶ RΓ(U', L(g')^*K).

public def sectionsBaseChangeMap (ch : BaseChangeChart f g f' g')
    (K : DerivedCategory X.Modules) :
    (CochainComplex.DerivedExtensionScalars.totalDerivedExtensionScalars.{u, u, u}
        ch.c.hom).functor.obj ((affineDerivedSections ch.incU).obj K) ⟶
      (affineDerivedSections ch.incU').obj ((Stacks.Duality.derivedPullback g').obj K)

AlgebraicGeometry.BaseChangeChart.isIso_sectionsBaseChangeMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/AffineChartComparisonMap.lean, line 132. The attribute's comment: “the second arrow of the composition in (2) is an isomorphism for K with quasi-coherent cohomology, so (2) tests the composition the source displays”.

The identification sectionsBaseChangeMap is an isomorphism when every cohomology sheaf of K is quasi-coherent.

public theorem isIso_sectionsBaseChangeMap (ch : BaseChangeChart f g f' g')
    (K : DerivedCategory X.Modules)
    (hK : ∀ n : ℤ, ((DerivedCategory.homologyFunctor X.Modules n).obj K).IsQuasicoherent) :
    IsIso (ch.sectionsBaseChangeMap K)

AlgebraicGeometry.BaseChangeChart.comparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/AffineChartComparisonMap.lean, line 191. The attribute's comment: “the comparison map on a Cartesian affine-open chart: the morphism whose invertibility is condition (2), and, asked only of a family of charts whose opens U' cover X', condition (3)”.

The chart comparison map. On a chart, the composition

RΓ(U,K) ⊗ᴸ_{𝒪_S(V)} 𝒪_{S'}(V') ⟶ RΓ(U,K) ⊗ᴸ_{𝒪_X(U)} 𝒪_{X'}(U') ⟶ RΓ(U',K')

in D(𝒪_{S'}(V')): pullbackComparison followed by RΓ(U', -) applied to the given morphism φ : L(g')^*K ⟶ K'.

public def comparison (ch : BaseChangeChart f g f' g')
    (K : DerivedCategory X.Modules) (K' : DerivedCategory X'.Modules)
    (φ : (Stacks.Duality.derivedPullback g').obj K ⟶ K') :
    (CochainComplex.DerivedExtensionScalars.totalDerivedExtensionScalars.{u, u, u}
        ch.b.hom).functor.obj
        ((ModuleCat.restrictScalars ch.a.hom).mapDerivedCategory.obj
          ((affineDerivedSections ch.incU).obj K)) ⟶
      (ModuleCat.restrictScalars ch.d.hom).mapDerivedCategory.obj
        ((affineDerivedSections ch.incU').obj K')

AlgebraicGeometry.exists_coveringFamily_isIso_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/AffineChartComparisonMap.lean, line 251. The attribute's comment: “(2) ⟹ (3) for the comparison map itself, which is the step of the three-way equivalence that needs no affine reduction: take the family of all charts”.

The step (2) ⟹ (3). If the comparison map of every Cartesian affine-open chart is an isomorphism, then there is a family of charts on which it is, whose opens U' cover X'.

public theorem exists_coveringFamily_isIso_comparison {X X' S S' : Scheme.{u}}
    {f : X ⟶ S} {g : S' ⟶ S} {f' : X' ⟶ S'} {g' : X' ⟶ X} (sq : IsPullback g' f' f g)
    (K : DerivedCategory X.Modules) (K' : DerivedCategory X'.Modules)
    (φ : (Stacks.Duality.derivedPullback g').obj K ⟶ K')
    (h : ∀ ch : BaseChangeChart f g f' g', IsIso (ch.comparison K K' φ)) :
    ∃ 𝒞 : Set (BaseChangeChart f g f' g'), (∀ ch ∈ 𝒞, IsIso (ch.comparison K K' φ)) ∧
      ∀ x' : X', ∃ ch ∈ 𝒞, ∃ y : Spec ch.A', ch.incU' y = x'

AlgebraicGeometry.BaseChangeChart.comparison_eq_ringComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/AffineChartPrimeCriterion.lean, line 242. The attribute's comment: “the comparison map of (2) is the ring-level comparison of the chart's square”.

The comparison map of a chart is the ring-level comparison of the chart's square of coordinate rings, applied to the morphism RΓ(U,K) ⊗ᴸ_{𝒪_X(U)} 𝒪_{X'}(U') ⟶ RΓ(U',K') assembled from the identification sectionsBaseChangeMap and RΓ(U', φ).

theorem comparison_eq_ringComparison (ch : BaseChangeChart f g f' g')
    (K : DerivedCategory X.Modules) (K' : DerivedCategory X'.Modules)
    (φ : (Stacks.Duality.derivedPullback g').obj K ⟶ K') :
    letI := ch.a.hom.toAlgebra
    letI := ch.b.hom.toAlgebra
    letI := ch.c.hom.toAlgebra
    letI := ch.d.hom.toAlgebra
    letI := (ch.c.hom.comp ch.a.hom).toAlgebra
    haveI : IsScalarTower ch.R ch.A ch.A' := IsScalarTower.of_algebraMap_eq fun _ => rfl
    haveI : IsScalarTower ch.R ch.R' ch.A' :=
      IsScalarTower.of_algebraMap_eq fun r => DFunLike.congr_fun ch.isPushout_hom r
    ch.comparison K K' φ =
      RingTheory.TorIndependence.ringComparison
        (R := ch.R) (R' := ch.R')
        ((affineDerivedSections ch.incU).obj K)
        ((affineDerivedSections ch.incU').obj K')
        (ch.sectionsBaseChangeMap K ≫ (affineDerivedSections ch.incU').map φ)

AlgebraicGeometry.BaseChangeChart.isIso_comparison_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/AffineChartPrimeCriterion.lean, line 267. The attribute's comment: “(2) at one chart, reduced to the primes of the chart's coordinate ring”.

The comparison map of a Cartesian affine-open chart is an isomorphism exactly when, in every degree, the induced map on cohomology is bijective after localizing at every prime of 𝒪_X(U) ⊗_{𝒪_S(V)} 𝒪_{S'}(V').

theorem isIso_comparison_iff (ch : BaseChangeChart f g f' g')
    (K : DerivedCategory X.Modules) (K' : DerivedCategory X'.Modules)
    (φ : (Stacks.Duality.derivedPullback g').obj K ⟶ K') :
    letI := ch.a.hom.toAlgebra
    letI := ch.b.hom.toAlgebra
    letI := ch.c.hom.toAlgebra
    letI := ch.d.hom.toAlgebra
    letI := (ch.c.hom.comp ch.a.hom).toAlgebra
    haveI : IsScalarTower ch.R ch.A ch.A' := IsScalarTower.of_algebraMap_eq fun _ => rfl
    haveI : IsScalarTower ch.R ch.R' ch.A' :=
      IsScalarTower.of_algebraMap_eq fun r => DFunLike.congr_fun ch.isPushout_hom r
    (IsIso (ch.comparison K K' φ) ↔
      ∀ (n : ℤ) (q : Ideal (ch.A ⊗[ch.R] ch.R')) (_ : q.IsPrime),
        Function.Bijective (LocalizedModule.map q.primeCompl
          (RingTheory.TorIndependence.cohomologyComparisonLinearMapGeneral
            (R := ch.R) (R' := ch.R')
            ((affineDerivedSections ch.incU).obj K)
            ((affineDerivedSections ch.incU').obj K')
            (ch.sectionsBaseChangeMap K ≫ (affineDerivedSections ch.incU').map φ) n).hom))

AlgebraicGeometry.BaseChangeChart.isIso_comparison_iff_forall_isIso_ringBaseChangeCohomologyMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/AffineChartPrimeCriterion.lean, line 294. The attribute's comment: “(2) at one chart is the invertibility, in every degree, of the ring-level map of Stacks 0DJ7 for the chart's rings: the affine reduction of the source proof”.

The comparison map of a Cartesian affine-open chart is an isomorphism exactly when the ring-level map RingTheory.TorIndependence.ringBaseChangeCohomologyMapGeneral of Stacks 0DJ7 for the chart's square of coordinate rings is invertible in every degree.

theorem isIso_comparison_iff_forall_isIso_ringBaseChangeCohomologyMap
    (ch : BaseChangeChart f g f' g')
    (K : DerivedCategory X.Modules) (K' : DerivedCategory X'.Modules)
    (φ : (Stacks.Duality.derivedPullback g').obj K ⟶ K') :
    letI := ch.a.hom.toAlgebra
    letI := ch.b.hom.toAlgebra
    letI := ch.c.hom.toAlgebra
    letI := ch.d.hom.toAlgebra
    letI := (ch.c.hom.comp ch.a.hom).toAlgebra
    haveI : IsScalarTower ch.R ch.A ch.A' := IsScalarTower.of_algebraMap_eq fun _ => rfl
    haveI : IsScalarTower ch.R ch.R' ch.A' :=
      IsScalarTower.of_algebraMap_eq fun r => DFunLike.congr_fun ch.isPushout_hom r
    (IsIso (ch.comparison K K' φ) ↔
      ∀ n : ℤ, IsIso (RingTheory.TorIndependence.ringBaseChangeCohomologyMapGeneral
        (R := ch.R) (R' := ch.R')
        ((affineDerivedSections ch.incU).obj K)
        ((affineDerivedSections ch.incU').obj K')
        (ch.sectionsBaseChangeMap K ≫ (affineDerivedSections ch.incU').map φ) n))

AlgebraicGeometry.baseChange_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/BaseChangeTFAEFinal.lean, line 500.

Stacks 0DJ8. Let

X' ⟶ X, X' ⟶ S', X ⟶ S, S' ⟶ S

be a Cartesian square of schemes, K an object of D(𝒪_X) with quasi-coherent cohomology sheaves, K' an object of D(𝒪_{X'}') with quasi-coherent cohomology sheaves, and φ : L(g')^*K ⟶ K'. Then the following are equivalent.

The pointwise map of Stacks 0DJ7 is an isomorphism at every point of X' and in every degree.

The comparison map of every Cartesian affine-open chart is an isomorphism.

The comparison map of every chart in some family whose opens U' cover X' is an isomorphism.

The implications are read off the source bridge AlgebraicGeometry.baseChange_tfae_of_sourceBridge: at a chart, a point y of Spec 𝒪_{X'}(U') and a degree, AlgebraicGeometry.BaseChangeChart.sourceBridgeMap is a bijection of the two maps' sources — AlgebraicGeometry.BaseChangeChart.bijective_sourceBridgeMap — commuting with them through the identification of their targets, by AlgebraicGeometry.BaseChangeChart.baseChangeCohomologyMap_sourceBridgeMap.

public theorem baseChange_tfae {X X' S S' : Scheme.{u}}
    (f : X ⟶ S) (g : S' ⟶ S) (f' : X' ⟶ S') (g' : X' ⟶ X) (sq : IsPullback g' f' f g)
    (K : DerivedCategory X.Modules) (K' : DerivedCategory X'.Modules)
    (hK : ∀ n : ℤ, ((DerivedCategory.homologyFunctor X.Modules n).obj K).IsQuasicoherent)
    (hK' : ∀ n : ℤ, ((DerivedCategory.homologyFunctor X'.Modules n).obj K').IsQuasicoherent)
    (φ : (Stacks.Duality.derivedPullback g').obj K ⟶ K') :
    List.TFAE
      [∀ (x' : X') (i : ℤ), IsIso (baseChangeCohomologyMap f g f' g' sq.w K K' φ x' i),
       ∀ ch : BaseChangeChart f g f' g', IsIso (ch.comparison K K' φ),
       ∃ 𝒞 : Set (BaseChangeChart f g f' g'),
         (∀ ch ∈ 𝒞, IsIso (ch.comparison K K' φ)) ∧
           ∀ x' : X', ∃ ch ∈ 𝒞, ∃ y : Spec ch.A', ch.incU' y = x']

AlgebraicGeometry.isIso_baseChangeCohomologyMap_derivedPullbackNatTrans_of_isFlatOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/TensorBaseChange/FlatOverModel.lean, line 494. The attribute's comment: “condition (1), at every point and in every degree, for the derived-to-ordinary comparison L(g')^G ⟶ (g')^G of a bounded-above complex G whose terms are flat over S, over a cartesian square: the stalk check the proof of Tag 0A1D performs”.

The stalk check of Stacks 0DJ8 for a complex flat over the base, at one point. For a cartesian square of schemes and a bounded-above complex 𝒢^• of 𝒪_X-modules whose terms are flat over S, the map of Stacks 0DJ7 at the derived-to-ordinary comparison L(g')^*𝒢^• ⟶ (g')^*𝒢^• is an isomorphism at x' in degree n.

theorem isIso_baseChangeCohomologyMap_derivedPullbackNatTrans_of_isFlatOver
    (hpb : IsPullback g' f' f g) (w : g' ≫ f = f' ≫ g) (G : CochainComplex X.Modules ℤ)
    (hG : CochainComplex.minus X.Modules G)
    (hflat : ∀ n : ℤ, IsFlatOver f.toLRSHom.toShHom (G.X n)) (x' : X') (n : ℤ) :
    IsIso (baseChangeCohomologyMap f g f' g' w (DerivedCategory.Q.obj G)
      (DerivedCategory.Q.obj ((pullbackComplex g'.toLRSHom.toShHom).obj G))
      ((derivedPullbackNatTrans g'.toLRSHom.toShHom).app G) x' n)

AlgebraicGeometry.derivedStalkAffineSectionsIsoToStalk, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/AffineDerivedStalk.lean, line 321. The attribute's comment: “the first of the two inputs still needed to turn condition (1) into condition (2): the derived stalk of K at a point of an affine open, identified with the derived localization of RGamma(U,K) there. This is that identification only; the compatibility of the base-change comparison of Tag 065Z with localization, which is the second input, is not proved anywhere, so condition (1) implies condition (2) is NOT formalized”.

The derived stalk at a point of an affine open is the derived localization of the sections over that open. Let i : Spec R ⟶ X be a morphism of schemes out of an affine scheme, y a point of Spec R, and K ∈ D(𝒪_X) an object with quasi-coherent cohomology sheaves. Then

RΓ(U, K) ⊗ᴸ_R 𝒪_{Spec R, y} ≅ (K_{i y}) ⊗ᴸ_{𝒪_{X, i y}} 𝒪_{Spec R, y},

where RΓ(U, K) is AlgebraicGeometry.affineDerivedSections i applied to K. When i is an open immersion with image U the extension of scalars on the right is along the germ isomorphism 𝒪_{X, i y} ≅ 𝒪_{Spec R, y}, so the right-hand side is the derived stalk of K at the point i y of U, and the two sides are the two readings of that derived stalk; the statement itself asks nothing of i.

The left-hand side is the derived localization at y of the derived global sections of the derived pullback of K to Spec R, which has quasi-coherent cohomology by Stacks 08DW, so affineDerivedStalkSectionsIso identifies it with the derived stalk at y of that pullback; AlgebraicGeometry.derivedPullbackStalkIso then moves the stalk from Spec R to X.

public def derivedStalkAffineSectionsIsoToStalk {X : Scheme.{u}} {A : CommRingCat.{u}}
    (i : Spec A ⟶ X) (y : Spec A) (K : DerivedCategory X.Modules)
    (hK : ∀ n : ℤ, ((DerivedCategory.homologyFunctor X.Modules n).obj K).IsQuasicoherent) :
    (totalDerivedExtensionScalars.{u, u, u}
        (A := ((Spec A).presheaf.stalk y : Type u))
        (StructureSheaf.toStalk A y).hom).functor.obj
        ((affineDerivedSections i).obj K) ≅
      (totalDerivedExtensionScalars.{u, u, u} (i.stalkMap y).hom).functor.obj
        ((derivedStalkFunctor (i y)).obj K)

AlgebraicGeometry.localizedHomologyAffineSectionsStalkIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/AffineDerivedStalkHomology.lean, line 119. The attribute's comment: “the degreewise reading of the first of the two inputs needed to turn condition (1) into condition (2): the localization at a prime of the degree-n cohomology of RGamma(U,K) is the degree-n cohomology of the derived stalk there. The identification of this localized module with the localization of the degree-n chart map of condition (2), which needs the compatibility of the base-change comparison of Tag 065Z with localizing ALL FOUR rings of the chart's square and not only its right-hand column, is not proved anywhere, so condition (1) implies condition (2) is NOT formalized”.

The derived stalk at a point of an affine open, read degree by degree. For i : Spec A ⟶ X, a point y of Spec A and K ∈ D(𝒪_X) with quasi-coherent cohomology sheaves, the localization at y of the degree-n cohomology of RΓ(U,K) is the degree-n cohomology of the derived stalk of K at i y, base changed to 𝒪_{Spec A,y}:

(Hⁿ RΓ(U,K))_y ≅ Hⁿ(K_{i y} ⊗ᴸ_{𝒪_{X, i y}} 𝒪_{Spec A,y}).

When i is an open immersion 𝒪_{X, i y} ⟶ 𝒪_{Spec A,y} is invertible and the right-hand side is the degree-n cohomology of the derived stalk itself; the statement asks nothing of i.

This is AlgebraicGeometry.derivedStalkAffineSectionsIsoToStalk with Hⁿ applied, the left-hand side being recognized as a localization because the germ map is one.

public def localizedHomologyAffineSectionsStalkIso {X : Scheme.{u}} {A : CommRingCat.{u}}
    (i : Spec A ⟶ X) (y : Spec A) (K : DerivedCategory X.Modules)
    (hK : ∀ n : ℤ, ((DerivedCategory.homologyFunctor X.Modules n).obj K).IsQuasicoherent)
    (n : ℤ) :
    (CochainComplex.DerivedTensor.localizedModuleFunctor.{u, u}
        (show PrimeSpectrum (A : Type u) from y).asIdeal.primeCompl).obj
        ((DerivedCategory.homologyFunctor (ModuleCat.{u} (A : Type u)) n).obj
          ((affineDerivedSections i).obj K)) ≅
      (ModuleCat.restrictScalars.{u, u, u} (StructureSheaf.toStalk A y).hom).obj
        ((DerivedCategory.homologyFunctor
            (ModuleCat.{u} ((Spec A).presheaf.stalk y : Type u)) n).obj
          ((totalDerivedExtensionScalars.{u, u, u} (i.stalkMap y).hom).functor.obj
            ((derivedStalkFunctor (i y)).obj K)))

Tag 0DJ9, a lemma

Tag 0DJ9 in the Stacks Project.

AlgebraicGeometry.globalBaseChangeIsIsoOfPointwise, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TensorFlatPushforwardBaseChangeCartesian.lean, line 67. The attribute's comment: “the conclusion over every cartesian square at once, in the spelling of GlobalBaseChangeIsIsoOfPointwise, with the conditions of Tag 0DJ8 read in form (1)”.

GlobalBaseChangeIsIsoOfPointwise holds: it is Stacks 0DJ9, AlgebraicGeometry.isIso_derivedBaseChangeComp_of_pointwiseBaseChange, quantified over all cartesian squares.

theorem globalBaseChangeIsIsoOfPointwise : GlobalBaseChangeIsIsoOfPointwise.{u}

AlgebraicGeometry.isIso_derivedBaseChangeComp_of_pointwiseBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/PointwiseBaseChangeIso.lean, line 58.

Stacks 0DJ9. For a cartesian square of schemes with f quasi-compact and quasi-separated, an object K of D_QCoh(𝒪_X) and a morphism φ : L(g')^*K ⟶ K' to an object of D_QCoh(𝒪_{X'}) whose pointwise maps of Stacks 0DJ7 are invertible at every point of X' and in every degree, the composition Lg^*Rf_*K ⟶ Rf'_*L(g')^*K ⟶ Rf'_*K' is an isomorphism.

theorem isIso_derivedBaseChangeComp_of_pointwiseBaseChange (sq : IsPullback g' f' f g)
    [QuasiCompact f] [QuasiSeparated f] (K : DerivedCategory X.Modules)
    (K' : DerivedCategory X'.Modules) (φ : (derivedPullback g'.toLRSHom.toShHom).obj K ⟶ K')
    (hK : ∀ n : ℤ, ((DerivedCategory.homologyFunctor X.Modules n).obj K).IsQuasicoherent)
    (hK' : ∀ n : ℤ, ((DerivedCategory.homologyFunctor X'.Modules n).obj K').IsQuasicoherent)
    (hp : PointwiseBaseChange f g f' g' sq.w K K' φ) :
    IsIso (derivedBaseChangeComp f g f' g' sq.w K K' φ)

Tag 0DJA, a lemma

Tag 0DJA in the Stacks Project.

AlgebraicGeometry.pointwiseBaseChangeTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TensorFlatPushforwardBaseChangeCartesian.lean, line 88. The attribute's comment: “(1), over every cartesian square at once, with the conditions of Tag 0DJ8 read in form (1)”.

PointwiseBaseChangeTensor holds: it is Stacks 0DJA (1), AlgebraicGeometry.isIso_baseChangeCohomologyMap_baseChangeTensorComparison_of_isPullback.

Cartesianness of the square is needed: for X = S = S' = Spec ℤ/4, X' = Spec ℤ/2, f = g = 𝟙, g' = f' the quotient map, K = 𝒪_X, K' = 𝒪_{X'} and φ the canonical isomorphism, the map of Stacks 0DJ7 is ℤ/2 ⟶ ℤ/2, while for E = (ℤ/2)~ it is 0 ⟶ Tor_1^{ℤ/4}(ℤ/2, ℤ/2) = ℤ/2 in degree -1.

theorem pointwiseBaseChangeTensor : PointwiseBaseChangeTensor.{u}

AlgebraicGeometry.baseChangeCohomologyMap_baseChangeTensorComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/TensorAndSheafHomBaseChange.lean, line 99. The attribute's comment: “the factorization the proof of conclusion (1) computes with, and not that conclusion: the map of Stacks 0DJ7 at the comparison L(g')^*(E ⊗^L K) ⟶ L(g')^*E ⊗^L K' is the map of Stacks 0DJ7 at the monoidality isomorphism of Tag 079U, followed by the stalkwise cohomology of the map induced by φ. Conclusion (1) itself is isIso_baseChangeCohomologyMap_baseChangeTensorComparison_of_isPullback”.

The base-change map on the comparison for a derived tensor product. The map of Stacks 0DJ7 at L(g')^*(E ⊗^L_{𝒪_X} K) ⟶ L(g')^*E ⊗^L_{𝒪_{X'}} K' is the map of Stacks 0DJ7 at the monoidality isomorphism of Tag 079U, followed by the stalkwise cohomology of L(g')^*E ⊗^L_{𝒪_{X'}} φ.

theorem baseChangeCohomologyMap_baseChangeTensorComparison (x' : X') (n : ℤ) :
    baseChangeCohomologyMap f g f' g' w
        (((derivedTensorProductFunctor X.sheaf).obj E).obj K)
        (((derivedTensorProductFunctor X'.sheaf).obj
          ((derivedPullback g'.toLRSHom.toShHom).obj E)).obj K')
        (baseChangeTensorComparison g'.toLRSHom.toShHom E K K' φ) x' n =
      baseChangeCohomologyMap f g f' g' w
          (((derivedTensorProductFunctor X.sheaf).obj E).obj K)
          (((derivedTensorProductFunctor X'.sheaf).obj
            ((derivedPullback g'.toLRSHom.toShHom).obj E)).obj
            ((derivedPullback g'.toLRSHom.toShHom).obj K))
          ((derivedPullbackTensorIso g'.toLRSHom.toShHom).hom.app (E, K)) x' n ≫
        (DerivedCategory.homologyFunctor (ModuleCat.{u} (X'.presheaf.stalk x')) n).map
          ((derivedStalkFunctor x').map
            (((derivedTensorProductFunctor X'.sheaf).obj
              ((derivedPullback g'.toLRSHom.toShHom).obj E)).map φ))

AlgebraicGeometry.baseChangeCohomologyMap_baseChangeSheafHomComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/TensorAndSheafHomBaseChange.lean, line 127. The attribute's comment: “the factorization through R𝓗om(L(g')^*E, L(g')^*K) that the proof of conclusions (2) and (3) performs, and not either conclusion: the map of Stacks 0DJ7 at the comparison L(g')^*R𝓗om(E, K) ⟶ R𝓗om(L(g')^*E, K') is the map of Stacks 0DJ7 at the map of Tag 08I3, followed by the stalkwise cohomology of the map induced by φ. Conclusion (2) itself is isIso_baseChangeCohomologyMap_baseChangeSheafHomComparison_of_isPerfect”.

The base-change map on the comparison for a derived internal hom. The map of Stacks 0DJ7 at L(g')^*R𝓗om_{𝒪_X}(E, K) ⟶ R𝓗om_{𝒪_{X'}}(L(g')^*E, K') is the map of Stacks 0DJ7 at the map of Tag 08I3, followed by the stalkwise cohomology of R𝓗om_{𝒪_{X'}}(L(g')^*E, φ).

theorem baseChangeCohomologyMap_baseChangeSheafHomComparison (x' : X') (n : ℤ) :
    baseChangeCohomologyMap f g f' g' w
        (((derivedSheafHom X.sheaf).obj (op E)).obj K)
        (((derivedSheafHom X'.sheaf).obj
          (op ((derivedPullback g'.toLRSHom.toShHom).obj E))).obj K')
        (baseChangeSheafHomComparison g'.toLRSHom.toShHom E K K' φ) x' n =
      baseChangeCohomologyMap f g f' g' w
          (((derivedSheafHom X.sheaf).obj (op E)).obj K)
          (((derivedSheafHom X'.sheaf).obj
            (op ((derivedPullback g'.toLRSHom.toShHom).obj E))).obj
            ((derivedPullback g'.toLRSHom.toShHom).obj K))
          (derivedPullbackSheafHomMap g'.toLRSHom.toShHom E K) x' n ≫
        (DerivedCategory.homologyFunctor (ModuleCat.{u} (X'.presheaf.stalk x')) n).map
          ((derivedStalkFunctor x').map
            (((derivedSheafHom X'.sheaf).obj
              (op ((derivedPullback g'.toLRSHom.toShHom).obj E))).map φ))

AlgebraicGeometry.isIso_baseChangeCohomologyMap_baseChangeSheafHomComparison_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/TensorBaseChange/DerivedSheafHom.lean, line 68. The attribute's comment: “(2)”.

Stacks 0DJA (2). For a cartesian square of schemes, if the map of Stacks 0DJ7 at (K, K', φ) is an isomorphism at every point of X' and in every degree, then so is the one at the comparison L(g')^*R𝓗om(E, K) ⟶ R𝓗om(L(g')^*E, K'), for every perfect E in D(𝒪_X).

theorem isIso_baseChangeCohomologyMap_baseChangeSheafHomComparison_of_isPerfect
    (hpb : IsPullback g' f' f g) (E K : DerivedCategory X.Modules)
    (hE : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace) E)
    (K' : DerivedCategory X'.Modules) (φ : (derivedPullback g'.toLRSHom.toShHom).obj K ⟶ K')
    (h : ∀ (x' : X') (n : ℤ), IsIso (baseChangeCohomologyMap f g f' g' hpb.w K K' φ x' n))
    (x' : X') (n : ℤ) :
    IsIso (baseChangeCohomologyMap f g f' g' hpb.w
      (((Stacks.SheafOfModules.derivedSheafHom X.sheaf).obj (op E)).obj K)
      (((Stacks.SheafOfModules.derivedSheafHom X'.sheaf).obj
        (op ((derivedPullback g'.toLRSHom.toShHom).obj E))).obj K')
      (Stacks.Cohomology.DerivedBaseChangeComparison.baseChangeSheafHomComparison
        g'.toLRSHom.toShHom E K K' φ) x' n)

AlgebraicGeometry.isIso_baseChangeCohomologyMap_baseChangeSheafHomComparison_of_isPseudoCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/TensorBaseChange/DerivedSheafHomPseudoCoherent.lean, line 63. The attribute's comment: “(3), for a flat morphism g : S' → S; without flatness of g part (3) fails, by the counterexample over ℤ/4 AlgebraicGeometry.not_pointwiseBaseChangeSheafHomOfPseudoCoherent”.

Stacks 0DJA (3), for a flat g. For a cartesian square of schemes with g flat, if the map of Stacks 0DJ7 at (K, K', φ) is an isomorphism at every point of X' and in every degree and K is bounded below, then so is the one at the comparison L(g')^*R𝓗om(E, K) ⟶ R𝓗om(L(g')^*E, K'), for every pseudo-coherent E in D(𝒪_X).

theorem isIso_baseChangeCohomologyMap_baseChangeSheafHomComparison_of_isPseudoCoherent
    (hpb : IsPullback g' f' f g) [Flat g] (E K : DerivedCategory X.Modules)
    (hE : AlgebraicGeometry.RingedSpace.PseudoCoherence.IsPseudoCoherent (X := X.toRingedSpace) E)
    (hK : DerivedCategoryB.IsBoundedBelow K)
    (K' : DerivedCategory X'.Modules) (φ : (derivedPullback g'.toLRSHom.toShHom).obj K ⟶ K')
    (h : ∀ (x' : X') (n : ℤ), IsIso (baseChangeCohomologyMap f g f' g' hpb.w K K' φ x' n))
    (x' : X') (n : ℤ) :
    IsIso (baseChangeCohomologyMap f g f' g' hpb.w
      (((Stacks.SheafOfModules.derivedSheafHom X.sheaf).obj (op E)).obj K)
      (((Stacks.SheafOfModules.derivedSheafHom X'.sheaf).obj
        (op ((derivedPullback g'.toLRSHom.toShHom).obj E))).obj K')
      (Stacks.Cohomology.DerivedBaseChangeComparison.baseChangeSheafHomComparison
        g'.toLRSHom.toShHom E K K' φ) x' n)

AlgebraicGeometry.not_pointwiseBaseChangeSheafHomOfPseudoCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/TensorBaseChange/DerivedSheafHomPseudoCoherentCounterexample.lean, line 304. The attribute's comment: “(3) as written is false: the statement of part (3) without flatness of g fails, by a counterexample over ℤ/4 with g : Spec ℤ/2 ⟶ Spec ℤ/4, K the structure sheaf and E the periodic resolution of ℤ/2”.

The statement of part (3) of Stacks 0DJA, with the equivalent conditions of Stacks 0DJ8 read in form (1) and g an arbitrary morphism, fails: for A = ℤ/4, the cartesian square with g : Spec ℤ/2 ⟶ Spec ℤ/4 the closed immersion and identities as vertical arrows, K = 𝒪_{Spec ℤ/4}, K' = L g^* K, φ = id, and E the pseudo-coherent object attached to the resolution ⋯ --2--> ℤ/4 --2--> ℤ/4 of ℤ/2, condition (1) of Stacks 0DJ8 holds for φ but fails for L g^* R𝓗om(E, K) ⟶ R𝓗om(L g^* E, K'), whose source has cohomology Tor_1^{ℤ/4}(ℤ/2, ℤ/2) ≠ 0 in degree -1 while its target lies in degrees ≥ 0.

theorem not_pointwiseBaseChangeSheafHomOfPseudoCoherent :
    ¬ (∀ {X X' S S' : Scheme.{u}} (f : X ⟶ S) (g : S' ⟶ S) (f' : X' ⟶ S') (g' : X' ⟶ X),
      IsPullback g' f' f g →
      ∀ (w : g' ≫ f = f' ≫ g) (E K : DerivedCategory X.Modules)
        (K' : DerivedCategory X'.Modules)
        (φ : (derivedPullback g'.toLRSHom.toShHom).obj K ⟶ K'),
        RingedSpace.IsPseudoCoherent (X := X.toRingedSpace) E →
        (∃ (L : CochainComplex X.Modules ℤ) (a : ℤ), L.IsStrictlyGE a ∧
          Nonempty (DerivedCategory.Q.obj L ≅ K)) →
        (∀ n : ℤ, ((DerivedCategory.homologyFunctor X.Modules n).obj K).IsQuasicoherent) →
        (∀ n : ℤ, ((DerivedCategory.homologyFunctor X'.Modules n).obj K').IsQuasicoherent) →
        PointwiseBaseChangeIsIso f g f' g' w K K' φ →
        PointwiseBaseChangeIsIso f g f' g' w
          (((derivedSheafHom X.sheaf).obj (op E)).obj K)
          (((derivedSheafHom X'.sheaf).obj
            (op ((derivedPullback g'.toLRSHom.toShHom).obj E))).obj K')
          (baseChangeSheafHomComparison g'.toLRSHom.toShHom E K K' φ))

AlgebraicGeometry.isIso_baseChangeCohomologyMap_baseChangeTensorComparison_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TorIndependence/TensorBaseChange/DerivedTensor.lean, line 130. The attribute's comment: “(1)”.

Stacks 0DJA (1). For a cartesian square of schemes, if the map of Stacks 0DJ7 at (K, K', φ) is an isomorphism at every point of X' and in every degree, then so is the one at the comparison L(g')^*(E ⊗^L K) ⟶ L(g')^*E ⊗^L K', for every E in D(𝒪_X).

theorem isIso_baseChangeCohomologyMap_baseChangeTensorComparison_of_isPullback
    (hpb : IsPullback g' f' f g) (E K : DerivedCategory X.Modules)
    (K' : DerivedCategory X'.Modules) (φ : (derivedPullback g'.toLRSHom.toShHom).obj K ⟶ K')
    (h : ∀ (x' : X') (n : ℤ), IsIso (baseChangeCohomologyMap f g f' g' hpb.w K K' φ x' n))
    (x' : X') (n : ℤ) :
    IsIso (baseChangeCohomologyMap f g f' g' hpb.w
      (((derivedTensorProductFunctor X.sheaf).obj E).obj K)
      (((derivedTensorProductFunctor X'.sheaf).obj
        ((derivedPullback g'.toLRSHom.toShHom).obj E)).obj K')
      (Stacks.Cohomology.DerivedBaseChangeComparison.baseChangeTensorComparison
        g'.toLRSHom.toShHom E K K' φ) x' n)

Tag 0A1D, a lemma

Tag 0A1D in the Stacks Project.

AlgebraicGeometry.isIso_tensorFlatBaseChangeMap_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/FlatOverBase/TensorFlat.lean, line 62.

Stacks 0A1D. Let f : X ⟶ S be a quasi-compact and quasi-separated morphism of schemes, E an object of D_QCoh(𝒪_X) and 𝒢^• a bounded above complex of quasi-coherent 𝒪_X-modules flat over S. For every cartesian square the canonical map

Lg^*Rf_*(E ⊗^L_{𝒪_X} 𝒢^•) ⟶ Rf'_*(L(g')^*E ⊗^L_{𝒪_{X'}} (g')^*𝒢^•)

of tensorFlatBaseChangeMap, with the ordinary pullback of 𝒢^• on the right, is an isomorphism.

theorem isIso_tensorFlatBaseChangeMap_of_isPullback {X X' S S' : Scheme.{u}} (f : X ⟶ S)
    (g : S' ⟶ S) (f' : X' ⟶ S') (g' : X' ⟶ X) (hsq : IsPullback g' f' f g)
    (hqc : QuasiCompact f) (hqs : QuasiSeparated f)
    (sq : g'.toLRSHom.toShHom ≫ f.toLRSHom.toShHom =
      f'.toLRSHom.toShHom ≫ g.toLRSHom.toShHom)
    (E : DerivedCategory X.Modules)
    (hE : ∀ n : ℤ, ((DerivedCategory.homologyFunctor X.Modules n).obj E).IsQuasicoherent)
    (G : CochainComplex X.Modules ℤ)
    (hGminus : CochainComplex.minus X.Modules G)
    (hGqcoh : ∀ n : ℤ, (G.X n).IsQuasicoherent)
    (hGflat : ∀ n : ℤ, IsFlatOver f.toLRSHom.toShHom (G.X n)) :
    IsIso (tensorFlatBaseChangeMap f g f' g' sq E G)

AlgebraicGeometry.tensorFlatBaseChangeMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/TensorFlatPushforwardBaseChange.lean, line 137. The attribute's comment: “the canonical map whose invertibility is the tag's conclusion, as the precise statement in the proof displays it: the derived base-change map of Stacks 08HY at E ⊗^L 𝒢^•, followed by Rf'_ of the base-change comparison of Stacks 0DJA taken at the derived-to-ordinary comparison L(g')^𝒢^• ⟶ (g')^𝒢^•. The target uses the ORDINARY pullback (g')^𝒢^•, which the source sets in bold, and the derived-to-ordinary comparison is not assumed invertible”.

The canonical map of Stacks 0A1D, as the precise statement in the source's proof displays it:

Lg^*Rf_*(E ⊗^L_{𝒪_X} 𝒢^•) ⟶ Rf'_*(L(g')^*E ⊗^L_{𝒪_{X'}} (g')^*𝒢^•).

It is the derived base-change map of Stacks 08HY at E ⊗^L_{𝒪_X} 𝒢^•, followed by Rf'_* of the base-change comparison for a derived tensor product of Stacks 0DJA, taken at the derived-to-ordinary comparison L(g')^*𝒢^• ⟶ (g')^*𝒢^•.

On the right-hand side the complex 𝒢^• is pulled back by the ordinary functor (g')^*, which is what the source's boldface insists on; the derived-to-ordinary comparison that makes this possible is the φ of the second factor, and it is never assumed invertible.

public def tensorFlatBaseChangeMap {X X' S S' : Scheme.{u}} (f : X ⟶ S) (g : S' ⟶ S)
    (f' : X' ⟶ S') (g' : X' ⟶ X)
    (sq : g'.toLRSHom.toShHom ≫ f.toLRSHom.toShHom =
      f'.toLRSHom.toShHom ≫ g.toLRSHom.toShHom)
    (E : DerivedCategory X.Modules) (G : CochainComplex X.Modules ℤ) :
    (derivedPullback g.toLRSHom.toShHom).obj
        ((derivedPushforward f.toLRSHom.toShHom).obj
          (((derivedTensorProductFunctor X.sheaf).obj E).obj (DerivedCategory.Q.obj G))) ⟶
      (derivedPushforward f'.toLRSHom.toShHom).obj
        (((derivedTensorProductFunctor X'.sheaf).obj
            ((derivedPullback g'.toLRSHom.toShHom).obj E)).obj
          (DerivedCategory.Q.obj ((pullbackComplex g'.toLRSHom.toShHom).obj G)))

Tag 08IE, a lemma

Tag 08IE in the Stacks Project.

AlgebraicGeometry.sheafHomFlatBaseChangeMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/SheafHomFlatPushforwardBaseChange.lean, line 132. The attribute's comment: “the canonical map whose invertibility is the tag's conclusion: the derived base-change map of Stacks 08HY at R𝓗om(E, 𝒢^•), followed by Rf'_ of the base-change comparison of Stacks 0DJA taken at the derived-to-ordinary comparison L(g')^𝒢^• ⟶ (g')^𝒢^•. The target uses the ORDINARY pullback (g')^𝒢^•, which the source sets in bold, and the derived-to-ordinary comparison is not assumed invertible”.

The canonical map of Stacks 08IE:

Lg^*Rf_*R𝓗om_{𝒪_X}(E, 𝒢^•) ⟶ Rf'_*R𝓗om_{𝒪_{X'}}(L(g')^*E, (g')^*𝒢^•).

It is the derived base-change map of Stacks 08HY at R𝓗om_{𝒪_X}(E, 𝒢^•), followed by Rf'_* of the base-change comparison for a derived internal hom of Stacks 0DJA, taken at the derived-to-ordinary comparison L(g')^*𝒢^• ⟶ (g')^*𝒢^•.

On the right-hand side the complex 𝒢^• is pulled back by the ordinary functor (g')^*, which is what the source's boldface insists on; the derived-to-ordinary comparison that makes this possible is the φ of the second factor, and it is never assumed invertible.

public def sheafHomFlatBaseChangeMap {X X' S S' : Scheme.{u}} (f : X ⟶ S) (g : S' ⟶ S)
    (f' : X' ⟶ S') (g' : X' ⟶ X)
    (sq : g'.toLRSHom.toShHom ≫ f.toLRSHom.toShHom =
      f'.toLRSHom.toShHom ≫ g.toLRSHom.toShHom)
    (E : DerivedCategory X.Modules) (G : CochainComplex X.Modules ℤ) :
    (derivedPullback g.toLRSHom.toShHom).obj
        ((derivedPushforward f.toLRSHom.toShHom).obj
          (((derivedSheafHom X.sheaf).obj (op E)).obj (DerivedCategory.Q.obj G))) ⟶
      (derivedPushforward f'.toLRSHom.toShHom).obj
        (((derivedSheafHom X'.sheaf).obj
            (op ((derivedPullback g'.toLRSHom.toShHom).obj E))).obj
          (DerivedCategory.Q.obj ((pullbackComplex g'.toLRSHom.toShHom).obj G)))

AlgebraicGeometry.isIso_sheafHomFlatBaseChangeMap_of_perfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/SheafHomFlatPushforwardBaseChange.lean, line 242. The attribute's comment: “case (1) of the tag -- E perfect, 𝒢^• bounded above, each 𝒢^n flat over S -- for the canonical map sheafHomFlatBaseChangeMap, with the ORDINARY pullback (g')^𝒢^• on the right as the source's boldface demands, the derived-to-ordinary comparison L(g')^𝒢^• ⟶ (g')^𝒢^• never being assumed invertible. The three steps the source cites are all proved in this library and none of them is assumed: the conclusion of Stacks 0DJ9, in the spelling globalBaseChangeIsIsoOfPointwise (reused verbatim from the Stacks 0A1D module, where it serves the same purpose); conclusion (2) of Stacks 0DJA, isIso_baseChangeCohomologyMap_baseChangeSheafHomComparison_of_isPerfect, at the cartesian square; and the stalk check performed inside the proof of Stacks 0A1D, pointwiseBaseChangeOfFlatOver, that flatness of the terms of 𝒢^• over S gives the condition of Stacks 0DJ8 for L(g')^𝒢^• ⟶ (g')^*𝒢^•. With those three, the qcqs hypothesis on f and the cartesian square, the displayed map is an isomorphism. The equivalent conditions of Stacks 0DJ8 are used only in form (1), the pointwise condition: forms (2) and (3) are carried in this library at the locally small model of D(𝒪_X) rather than at the standard model the map of Stacks 08HY lives at, and no implication between them is available. The two D_QCoh memberships Stacks 0DJ9 asks of the two derived internal homs are the statement's own conditions hK and hK', at a spelling of the derived internal hom that does not line up with the one the comparison map is written at”.

Stacks 08IE, case (1). Let f : X ⟶ S be a quasi-compact and quasi-separated morphism of schemes, let E be a perfect object of D(𝒪_X) and let 𝒢^• be a bounded-above complex of quasi-coherent 𝒪_X-modules flat over S. For every cartesian base-change square the canonical map

Lg^*Rf_*R𝓗om_{𝒪_X}(E, 𝒢^•) ⟶ Rf'_*R𝓗om_{𝒪_{X'}}(L(g')^*E, (g')^*𝒢^•)

of sheafHomFlatBaseChangeMap is an isomorphism — note the ordinary pullback of 𝒢^• on the right.

The proof is the source's: the flatness of the terms of 𝒢^• over S gives the condition of Stacks 0DJ8 for L(g')^*𝒢^• ⟶ (g')^*𝒢^• (AlgebraicGeometry.pointwiseBaseChangeOfFlatOver), Stacks 0DJA (2) (AlgebraicGeometry.isIso_baseChangeCohomologyMap_baseChangeSheafHomComparison_of_isPerfect) propagates it to the comparison for R𝓗om_{𝒪_X}(E, 𝒢^•), and Stacks 0DJ9 (AlgebraicGeometry.globalBaseChangeIsIsoOfPointwise) turns it into the invertibility of the displayed map.

public theorem isIso_sheafHomFlatBaseChangeMap_of_perfect
    {X X' S S' : Scheme.{u}} (f : X ⟶ S) (g : S' ⟶ S) (f' : X' ⟶ S') (g' : X' ⟶ X)
    (hsq : IsPullback g' f' f g) (hqc : QuasiCompact f) (hqs : QuasiSeparated f)
    (w : g' ≫ f = f' ≫ g)
    (sq : g'.toLRSHom.toShHom ≫ f.toLRSHom.toShHom =
      f'.toLRSHom.toShHom ≫ g.toLRSHom.toShHom)
    (E : DerivedCategory X.Modules)
    (hEperfect : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace) E)
    (G : CochainComplex X.Modules ℤ)
    (hGminus : CochainComplex.minus X.Modules G)
    (hGqcoh : ∀ n : ℤ, (G.X n).IsQuasicoherent)
    (hGflat : ∀ n : ℤ, IsFlatOver f.toLRSHom.toShHom (G.X n))
    (hK : ∀ n : ℤ, ((DerivedCategory.homologyFunctor X.Modules n).obj
      (((derivedSheafHom X.sheaf).obj (op E)).obj
        (DerivedCategory.Q.obj G))).IsQuasicoherent)
    (hK' : ∀ n : ℤ, ((DerivedCategory.homologyFunctor X'.Modules n).obj
      (((derivedSheafHom X'.sheaf).obj
          (op ((derivedPullback g'.toLRSHom.toShHom).obj E))).obj
        (DerivedCategory.Q.obj
          ((pullbackComplex g'.toLRSHom.toShHom).obj G)))).IsQuasicoherent) :
    IsIso (sheafHomFlatBaseChangeMap f g f' g' sq E G)

AlgebraicGeometry.isIso_sheafHomFlatBaseChangeMap_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/SheafHomPerfectFlatPushforwardBaseChange.lean, line 117. The attribute's comment: “case (1): E perfect, 𝒢^• bounded above with terms quasi-coherent and flat over S, f quasi-compact and quasi-separated, an arbitrary cartesian square; the canonical map of the source's proof, with the ORDINARY pullback (g')^*𝒢^• on the right, is an isomorphism. Case (2) is false as stated (see the module documentation); its corrected form is isIso_sheafHomFlatBaseChangeMap_of_isPseudoCoherent_of_flat”.

Stacks 08IE, case (1). Let f : X ⟶ S be a quasi-compact and quasi-separated morphism of schemes, let E be a perfect object of D(𝒪_X) and let 𝒢^• be a bounded above complex of quasi-coherent 𝒪_X-modules whose terms are flat over S. For every cartesian square
X' --g'--> X
|          |
f'         f
v          v
S' --g---> S
the canonical map

Lg^*Rf_*R𝓗om(E, 𝒢^•) ⟶ Rf'_*R𝓗om(L(g')^*E, (g')^*𝒢^•)

of AlgebraicGeometry.sheafHomFlatBaseChangeMap, with the ordinary pullback (g')^*𝒢^• on the right as the source insists, is an isomorphism: the formation of Rf_*R𝓗om(E, 𝒢^•) commutes with arbitrary base change.

public theorem isIso_sheafHomFlatBaseChangeMap_of_isPerfect
    {X X' S S' : Scheme.{u}} (f : X ⟶ S) (g : S' ⟶ S) (f' : X' ⟶ S') (g' : X' ⟶ X)
    (hsq : IsPullback g' f' f g) (hqc : QuasiCompact f) (hqs : QuasiSeparated f)
    (sq : g'.toLRSHom.toShHom ≫ f.toLRSHom.toShHom =
      f'.toLRSHom.toShHom ≫ g.toLRSHom.toShHom)
    (E : DerivedCategory X.Modules)
    (hE : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace) E)
    (G : CochainComplex X.Modules ℤ)
    (hGminus : CochainComplex.minus X.Modules G)
    (hGqcoh : ∀ n : ℤ, (G.X n).IsQuasicoherent)
    (hGflat : ∀ n : ℤ, IsFlatOver f.toLRSHom.toShHom (G.X n)) :
    IsIso (sheafHomFlatBaseChangeMap f g f' g' sq E G)

AlgebraicGeometry.isIso_sheafHomFlatBaseChangeMap_of_isPseudoCoherent_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/SheafHomPseudoCoherentFlatPushforwardBaseChange.lean, line 109. The attribute's comment: “case (2), CORRECTED: as stated (E pseudo-coherent, 𝒢^• bounded with terms flat over S, arbitrary base change) it is false -- for S = X = Spec ℤ/4, f = id, E = (ℤ/2)~, 𝒢^• = 𝒪_X and g : Spec ℤ/2 ⟶ Spec ℤ/4 the source has H^{-1} = Tor_1^{ℤ/4}(ℤ/2, ℤ/2) ≠ 0 while the target lies in D^{≥0}; the gap is in the proof of Tag 0DJA (3). Proved here for base change along a FLAT g, with E pseudo-coherent and 𝒢^• any complex of quasi-coherent modules bounded below (so in particular for 𝒢^• bounded with terms flat over S)”.

Stacks 08IE, case (2), corrected to base change along a flat morphism. Let f : X ⟶ S be a quasi-compact and quasi-separated morphism of schemes, let E be a pseudo-coherent object of D(𝒪_X) and let 𝒢^• be a complex of quasi-coherent 𝒪_X-modules vanishing in degrees below some a. For every cartesian square
X' --g'--> X
|          |
f'         f
v          v
S' --g---> S
with g flat, the canonical map

Lg^*Rf_*R𝓗om(E, 𝒢^•) ⟶ Rf'_*R𝓗om(L(g')^*E, (g')^*𝒢^•)

of AlgebraicGeometry.sheafHomFlatBaseChangeMap is an isomorphism. The source's case (2), for a bounded 𝒢^• with terms flat over S and an arbitrary g, is false: see the module documentation.

public theorem isIso_sheafHomFlatBaseChangeMap_of_isPseudoCoherent_of_flat
    {X X' S S' : Scheme.{u}} (f : X ⟶ S) (g : S' ⟶ S) (f' : X' ⟶ S') (g' : X' ⟶ X)
    (hsq : IsPullback g' f' f g) (hqc : QuasiCompact f) (hqs : QuasiSeparated f) [Flat g]
    (sq : g'.toLRSHom.toShHom ≫ f.toLRSHom.toShHom =
      f'.toLRSHom.toShHom ≫ g.toLRSHom.toShHom)
    (E : DerivedCategory X.Modules)
    (hE : RingedSpace.IsPseudoCoherent (X := X.toRingedSpace) E)
    (G : CochainComplex X.Modules ℤ) (a : ℤ) (hGge : G.IsStrictlyGE a)
    (hGqcoh : ∀ n : ℤ, (G.X n).IsQuasicoherent) :
    IsIso (sheafHomFlatBaseChangeMap f g f' g' sq E G)

Stacks.Examples.SheafHomCounterexample.not_forall_isIso_sheafHomFlatBaseChangeMap_of_isPseudoCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/BaseChange/SheafHomPseudoCoherentCounterexample.lean, line 297. The attribute's comment: “the erratum's counterexample: case (2) for an ARBITRARY base change is false; it fails for S = X = Spec ℤ/4, f = id, E = (ℤ/2)~, 𝒢^• = 𝒪_X and g : Spec ℤ/2 ⟶ Spec ℤ/4”.

It is not true that for every quasi-compact and quasi-separated f : X ⟶ S, every pseudo-coherent E ∈ D(𝒪_X), every bounded complex 𝒢^• of quasi-coherent 𝒪_X-modules flat over S and every cartesian square, the canonical map Lg^*Rf_*R𝓗om(E, 𝒢^•) ⟶ Rf'_*R𝓗om(L(g')^*E, (g')^*𝒢^•) of AlgebraicGeometry.sheafHomFlatBaseChangeMap is an isomorphism.

theorem not_forall_isIso_sheafHomFlatBaseChangeMap_of_isPseudoCoherent :
    ¬ ∀ {X X' S S' : Scheme.{0}} (f : X ⟶ S) (g : S' ⟶ S) (f' : X' ⟶ S') (g' : X' ⟶ X)
      (_ : IsPullback g' f' f g) (_ : QuasiCompact f) (_ : QuasiSeparated f)
      (sq : g'.toLRSHom.toShHom ≫ f.toLRSHom.toShHom =
        f'.toLRSHom.toShHom ≫ g.toLRSHom.toShHom)
      (E : DerivedCategory X.Modules) (_ : RingedSpace.IsPseudoCoherent (X := X.toRingedSpace) E)
      (G : CochainComplex X.Modules ℤ) (a b : ℤ) (_ : G.IsStrictlyGE a) (_ : G.IsStrictlyLE b)
      (_ : ∀ n : ℤ, (G.X n).IsQuasicoherent)
      (_ : ∀ n : ℤ, IsFlatOver f.toLRSHom.toShHom (G.X n)),
      IsIso (sheafHomFlatBaseChangeMap f g f' g' sq E G)

Sources

LeanAlgebraicGeometry.baseChangeCohomologyMap · AlgebraicGeometry.BaseChangeChart · AlgebraicGeometry.BaseChangeChart.isOpenImmersion_incU' · AlgebraicGeometry.BaseChangeChart.ofAffineOpens · AlgebraicGeometry.exists_baseChangeChart_covering · AlgebraicGeometry.exists_coveringFamily_of_forall_baseChangeChart · AlgebraicGeometry.BaseChangeChart.cohomologyComparison · AlgebraicGeometry.BaseChangeChart.cohomologyComparison_tmul_one

Section36.27 Producing perfect complexes #

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

Tag 08EV, a lemma

Tag 08EV in the Stacks Project.

Stacks.Cohomology.ProperSupportPerfection.isPerfect_derivedPushforward_of_properSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ProperSupportPerfection.lean, line 314. The attribute's comment: “the direct image is the derived pushforward, not an arbitrary functor; carried are Tag 08E2 for the object and the source's closing Tor-dimension estimate, both named hypotheses about that functor; this theorem is what Tag 0DJQ and Tag 0B6F consume, so neither of those assumes this tag any longer”.

[Stacks, Tag 08EV]. Let S be a locally Noetherian scheme and f : X ⟶ S a morphism locally of finite type. Let K be an object of D(𝒪_X) which

is bounded with coherent cohomology sheaves, that is, lies in D^b_{Coh}(𝒪_X);

has the support of each of its cohomology sheaves inside a closed subset proper over S; and

has finite Tor dimension as an object of D(f⁻¹𝒪_S).

Then Rf_*K is a perfect object of D(𝒪_S), with Rf_* the derived direct image Stacks.Cohomology.ProperSupportPerfection.derivedPushforwardOX — the total right derived functor of degreewise pushforward — and not an arbitrary functor.

Two hypotheses beyond those are carried, and they are the two statements of the source's proof that this repository does not have; each is a statement about that same Rf_*, and see the implementation notes of this file for why each is unavoidable here. hpushforwardCoherence is [Stacks, Tag 08E2] for K, read through [Stacks, Tag 08E8]: granted a closed subset proper over S carrying the cohomological support, and granted coherence of the cohomology sheaves, Rf_*K is pseudo-coherent. hpushforwardTorDimension is the closing step of the source's proof for K: granted the same closed subset and clause (3), Rf_*K has finite Tor dimension over 𝒪_S. Neither mentions perfectness; what is proved here is the production of the closed subset — the source's "let T ⊂ X be the union of the supports of the H^i(E)" — and the passage from the two residues to perfectness through [Stacks, Tag 08CQ].

theorem isPerfect_derivedPushforward_of_properSupport [IsLocallyNoetherian S]
    (hbounded : ∃ a b : ℤ, ∀ i : ℤ, i ∉ Set.Icc a b →
      Limits.IsZero ((DerivedCategory.homologyFunctor (OXMod.{u, u} X.toRingedSpace) i).obj K))
    (hcoherent : ∀ i : ℤ,
      ((DerivedCategory.homologyFunctor (OXMod.{u, u} X.toRingedSpace) i).obj K).IsCoherent)
    (hproperSupport : ∀ i : ℤ, ∃ Z : Closeds X, IsProperOver f Z ∧
      SheafOfModules.supp
          ((DerivedCategory.homologyFunctor (OXMod.{u, u} X.toRingedSpace) i).obj K) ⊆
        (Z : Set X))
    (hTor : D.HasFiniteTorDimension ((Scheme.Hom.derivedScalarRestriction f).obj K))
    (hpushforwardCoherence : ∀ T : Closeds X, IsProperOver f T → SuppHomologySubset K T →
      (∀ i : ℤ,
        ((DerivedCategory.homologyFunctor (OXMod.{u, u} X.toRingedSpace) i).obj K).IsCoherent) →
      RingedSpace.IsPseudoCoherent (X := S.toRingedSpace)
        ((derivedPushforwardOX f).obj K))
    (hpushforwardTorDimension : ∀ T : Closeds X, IsProperOver f T → SuppHomologySubset K T →
      D.HasFiniteTorDimension ((Scheme.Hom.derivedScalarRestriction f).obj K) →
      Stacks.Cohomology.TorAmplitude.HasFiniteTorDimension S.toRingedSpace
        ((derivedPushforwardOX f).obj K)) :
    RingedSpace.IsPerfect (X := S.toRingedSpace) ((derivedPushforwardOX f).obj K)

Stacks.AlgebraicGeometry.ProperSupportCoherent.isPseudoCoherent_derivedPushforward_of_isProperOver_supp_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProperSupportCoherent/PerfectDirectImageSupplement.lean, line 48. The attribute's comment: “the pseudo-coherence half of the conclusion only: Rf_E is a pseudo-coherent object of D(𝒪_S). Perfectness is pseudo-coherence together with locally finite Tor dimension by Tag 08CQ, and the Tor-dimension half is not proved here: it needs the clause (2) implies (1) of Tag 08EA and the projection formula of Tag 08EU at a general target complex, neither of which is in the tree. Rf_E is nowhere asserted here to be of locally finite Tor dimension, nor to be perfect”. References: SGA 6 IV (2.11.1), “partial”; SGA 6 XIV (2.2), “special case”.

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

By [Stacks, Tag 08CQ] perfectness is pseudo-coherence together with locally finite Tor dimension; this is the first of the two, obtained from [Stacks, Tag 08E2] and [Stacks, Tag 08E8].

theorem isPseudoCoherent_derivedPushforward_of_isProperOver_supp_unconditional [IsNoetherian S]
    [LocallyOfFiniteType f] (E : DerivedCategory X.Modules)
    (hcoh : ∀ j : ℤ, ((DerivedCategory.homologyFunctor X.Modules j).obj E).IsCoherent)
    (hsupp : ∀ j : ℤ, IsProperOver f
      ⟨SheafOfModules.supp ((DerivedCategory.homologyFunctor X.Modules j).obj E),
        @SheafOfModules.isClosed_supp _ _ _ (hcoh j).isFiniteType⟩)
    (a b : ℤ) (hGE : E.IsGE a) (hLE : E.IsLE b) :
    AlgebraicGeometry.RingedSpace.IsPseudoCoherent (X := S.toRingedSpace)
      ((derivedPushforwardModules f).obj E)

Stacks.AlgebraicGeometry.ProperSupportCoherent.isPerfect_derivedPushforward_of_isProperOver_supp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProperSupportCoherent/TorDimensionDirectImage.lean, line 345. References: SGA 6 0 (3.1), “more general”; SGA 6 0 (4.1), “more general”; SGA 6 XIV (2.2), “special case”.

Let S be a Noetherian scheme, f : X ⟶ S a morphism locally of finite type and E an object of D(𝒪_X) such that

E is in D^b_{Coh}(𝒪_X): it is bounded, E ∈ D^{≥ a} ∩ D^{≤ b}, and its cohomology sheaves are coherent;

the support of H^i(E) is proper over S for every i;

E has finite Tor dimension as an object of D(f⁻¹𝒪_S).

Then Rf_*E is a perfect object of D(𝒪_S).

theorem isPerfect_derivedPushforward_of_isProperOver_supp {X S : Scheme.{u}} (f : X ⟶ S)
    [IsNoetherian S] [LocallyOfFiniteType f] (E : DerivedCategory X.Modules)
    (a b : ℤ) (hGE : E.IsGE a) (hLE : E.IsLE b)
    (hcoh : ∀ j : ℤ, ((DerivedCategory.homologyFunctor X.Modules j).obj E).IsCoherent)
    (hsupp : ∀ j : ℤ, IsProperOver f
      ⟨SheafOfModules.supp ((DerivedCategory.homologyFunctor X.Modules j).obj E),
        @SheafOfModules.isClosed_supp _ _ _ (hcoh j).isFiniteType⟩)
    (htor : Stacks.Cohomology.TorAmplitude.HasFiniteTorDimension
      (RingedSpace.inverseImage S.toRingedSpace f.base)
      ((Scheme.Hom.derivedScalarRestriction f).obj E)) :
    Stacks.Cohomology.PerfectComplexes.IsPerfect (X := S.toRingedSpace)
      ((derivedPushforwardModules f).obj E)

Tag 0DJQ, a lemma

Tag 0DJQ in the Stacks Project.

Stacks.Cohomology.PerfectPushforward.isPerfect_derivedPushforward_derivedTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/PerfectPushforward.lean, line 1543. The attribute's comment: “the direct image is the derived pushforward, not an arbitrary functor; Tag 08EV is proved in ProperSupportPerfection and applied here, so what stands in its place are its own two residues about that same functor, Tag 08E2 for it and the source's closing Tor-dimension estimate; of Tag 08EV's four clauses for the derived tensor product three are proved here and the fourth, finiteness of the Tor dimension over the inverse image of the structure sheaf of the base, is carried, with the geometric step it runs on proved as exists_local_tensorComplex_models”.

[Stacks, Tag 0DJQ]. Let S be a Noetherian scheme, f : X ⟶ S a morphism locally of finite type, E a perfect object of D(𝒪_X) and 𝒢 a bounded complex of coherent 𝒪_X-modules, flat over S, whose support is proper over S. Then Rf_*(E ⊗^L_{𝒪_X} 𝒢) is a perfect object of D(𝒪_S), with Rf_* the derived direct image Stacks.Cohomology.ProperSupportPerfection.derivedPushforwardOX f — the total right derived functor of degreewise pushforward — and not a functor left unspecified.

[Stacks, Tag 08EV] itself is not a hypothesis: it is proved in StacksFrontier/AlgebraicGeometry/Perfect/ProperSupportPerfection.lean, and Stacks.Cohomology.PerfectPushforward.pushforwardPerfectionCriterion_of_residues turns it into the criterion this proof consumes. What is carried in its place are that theorem's own two residues, hcoh and htor — [Stacks, Tag 08E2] for Rf_* and the source's closing Tor-dimension estimate, both statements about that same functor — each of which is strictly smaller than the conclusion, with its obstruction identified in its own docstring.

One of the four clauses of [Stacks, Tag 08EV]'s hypothesis for E ⊗^L_{𝒪_X} 𝒢 is still carried, as the hasFiniteTorDimension field of h. The support clause is proved: see Stacks.Cohomology.PerfectPushforward.supp_homology_derivedTensor_subset and Stacks.Cohomology.PerfectPushforward.TensorPushforwardData.input. So is the boundedness clause: see Stacks.Cohomology.PerfectPushforward.exists_isZero_homology_derivedTensor and Stacks.Cohomology.PerfectPushforward.TensorPushforwardData.bounded. So is coherence: see Stacks.Cohomology.PerfectPushforward.isCoherent_homology_derivedTensor and Stacks.Cohomology.PerfectPushforward.TensorPushforwardData.isCoherent. The geometric step the remaining clause runs on — that E ⊗^L_{𝒪_X} 𝒢 is, locally on a covering of X, the total tensor complex of a strictly perfect complex with the restriction of 𝒢 — is proved above, as Stacks.Cohomology.PerfectPushforward.exists_local_tensorComplex_models; what reading it off that still needs is listed in the implementation notes of this file.

theorem isPerfect_derivedPushforward_derivedTensor [IsNoetherian S] [LocallyOfFiniteType f]
    (D : RingedSpace.CertifiedDerivedSheafTensoring
      (RingedSpace.inverseImage S.toRingedSpace f.base))
    (T : Stacks.DerivedTensor.RingedSite.DerivedTensorProduct X.toRingedSpace.sheaf)
    [(Stacks.SheafOfModules.Tensor.sheafTensor.{_, _, u, u, u} X.toRingedSpace.sheaf).Additive]
    [∀ M, ((Stacks.SheafOfModules.Tensor.sheafTensor.{_, _, u, u, u} X.toRingedSpace.sheaf).obj M).Additive]
    [∀ K L : CochainComplex (Stacks.DerivedTensor.RingedSite.Modules X.toRingedSpace.sheaf) ℤ,
      HomologicalComplex.HasMapBifunctor K L
        (Stacks.SheafOfModules.Tensor.sheafTensor.{_, _, u, u, u} X.toRingedSpace.sheaf) (ComplexShape.up ℤ)]
    (hcoh : PushforwardCoherenceResidue f (derivedPushforwardOX f))
    (htor : PushforwardTorDimensionResidue f D (derivedPushforwardOX f))
    (E : DerivedCategory (OXMod.{u, u} X.toRingedSpace))
    (G : CochainComplex (OXMod.{u, u} X.toRingedSpace) ℤ)
    (h : TensorPushforwardData f D T E G) :
    RingedSpace.IsPerfect (X := S.toRingedSpace)
      ((derivedPushforwardOX f).obj ((T.tensor.obj E).obj (DerivedCategory.Q.obj G)))

Stacks.Cohomology.PerfectPushforward.isPerfect_derivedPushforward_derivedTensorProductFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/PerfectPushforwardCanonicalTensor.lean, line 70.

[Stacks, Tag 0DJQ]. Let S be a Noetherian scheme and f : X ⟶ S a morphism of schemes which is locally of finite type. Let E be a perfect object of D(𝒪_X) and let 𝒢 be a bounded complex of coherent 𝒪_X-modules, flat over S, with support proper over S (Stacks.Cohomology.PerfectPushforward.FlatProperSupportComplex). Then Rf_*(E ⊗^L_{𝒪_X} 𝒢) is a perfect object of D(𝒪_S).

theorem isPerfect_derivedPushforward_derivedTensorProductFunctor [IsNoetherian S]
    [LocallyOfFiniteType f] (G : CochainComplex (OXMod.{u, u} X.toRingedSpace) ℤ)
    (hG : FlatProperSupportComplex f G) :
    letI := HasDerivedCategory.standard (OXMod.{u, u} X.toRingedSpace)
    letI := HasDerivedCategory.standard
      (Stacks.DerivedTensor.RingedSite.Modules X.toRingedSpace.sheaf)
    letI := HasDerivedCategory.standard (OXMod.{u, u} S.toRingedSpace)
    ∀ E : DerivedCategory (OXMod.{u, u} X.toRingedSpace),
      RingedSpace.IsPerfect (X := X.toRingedSpace) E →
        RingedSpace.IsPerfect (X := S.toRingedSpace)
          ((derivedPushforwardOX f).obj
            (((derivedTensorProductFunctor X.toRingedSpace.sheaf).obj E).obj
              (DerivedCategory.Q.obj G)))

Tag 0DJR, a lemma

Tag 0DJR in the Stacks Project.

Stacks.Cohomology.PerfectInternalHomPushforward.isPerfect_derivedPushforward_derivedSheafHom_of_flatProperSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/PerfectInternalHomPushforwardUnconditional.lean, line 96.

[Stacks, Tag 0DJR]. Let S be a Noetherian scheme, f : X ⟶ S a morphism locally of finite type, E a perfect object of D(𝒪_X) and 𝒢 a bounded complex of coherent 𝒪_X-modules, flat over S, with support proper over S. Then Rf_*RSheafHom(E, 𝒢) is a perfect object of D(𝒪_S), with Rf_* the derived direct image Stacks.Cohomology.ProperSupportPerfection.derivedPushforwardOX f.

The source's proof: E^∨ is perfect and RSheafHom(E, 𝒢) ≅ E^∨ ⊗^L 𝒢 by [Stacks, Tag 08DQ] (derivedSheafHomObjIsoDualTensor), and [Stacks, Tag 0DJQ] applies to (E^∨, 𝒢).

theorem isPerfect_derivedPushforward_derivedSheafHom_of_flatProperSupport [IsNoetherian S]
    [LocallyOfFiniteType f]
    (E : DerivedCategory (OXMod.{u, u} X.toRingedSpace))
    (G : CochainComplex (OXMod.{u, u} X.toRingedSpace) ℤ)
    (hE : RingedSpace.IsPerfect (X := X.toRingedSpace) E) (hG : FlatProperSupportComplex f G) :
    RingedSpace.IsPerfect (X := S.toRingedSpace)
      ((derivedPushforwardOX f).obj (derivedSheafHomObj (X := X) E G))

Tag 0B6F, a lemma

Tag 0B6F in the Stacks Project.

Stacks.Cohomology.PerfectPushforward.isPerfect_derivedPushforward_of_flat_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/PerfectPushforwardCanonicalTensor.lean, line 92.

[Stacks, Tag 0B6F]. Let S be a Noetherian scheme and f : X ⟶ S a flat proper morphism of schemes. Let E be a perfect object of D(𝒪_X). Then Rf_*E is a perfect object of D(𝒪_S).

theorem isPerfect_derivedPushforward_of_flat_of_isProper [IsNoetherian S] [Flat f] [IsProper f] :
    letI := HasDerivedCategory.standard (OXMod.{u, u} X.toRingedSpace)
    letI := HasDerivedCategory.standard (OXMod.{u, u} S.toRingedSpace)
    ∀ E : DerivedCategory (OXMod.{u, u} X.toRingedSpace),
      RingedSpace.IsPerfect (X := X.toRingedSpace) E →
        RingedSpace.IsPerfect (X := S.toRingedSpace) ((derivedPushforwardOX f).obj E)

Sources

LeanStacks.Cohomology.ProperSupportPerfection.isPerfect_derivedPushforward_of_properSupport · Stacks.AlgebraicGeometry.ProperSupportCoherent.isPseudoCoherent_derivedPushforward_of_isProperOver_supp_unconditional · Stacks.AlgebraicGeometry.ProperSupportCoherent.isPerfect_derivedPushforward_of_isProperOver_supp · Stacks.Cohomology.PerfectPushforward.isPerfect_derivedPushforward_derivedTensor · Stacks.Cohomology.PerfectPushforward.isPerfect_derivedPushforward_derivedTensorProductFunctor · Stacks.Cohomology.PerfectInternalHomPushforward.isPerfect_derivedPushforward_derivedSheafHom_of_flatProperSupport · Stacks.Cohomology.PerfectPushforward.isPerfect_derivedPushforward_of_flat_of_isProper

Section36.28 A projection formula for Ext #

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

Tag 0A1F, a lemma

Tag 0A1F in the Stacks Project.

Stacks.Cohomology.ExtProjectionFormula.extCohomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ExtProjectionFormula.lean, line 292. The attribute's comment: “the functorial isomorphisms for every i, as a natural isomorphism in ℱ ranging over all 𝒪_S-modules rather than only the quasi-coherent ones, and Γ(S, 𝒪_S)-linear; two steps of the source's proof are carried as explicit named hypotheses, the fields projectionFormula and mixedFlatTensor of ExtProjectionInput — invertibility of the projection-formula map of Tag 0B53 at ℱ, which is Tag 08EU and which this library proves only at ℱ = 𝒪_S, and the identification of 𝒢 ⊗ᴸ Lf^ℱ with 𝒢 ⊗ f^ℱ, which is Tag 08DE together with flatness of the terms of 𝒢 over S; the remaining two steps, associativity of the derived tensor product and Leray, are proved, the latter in the unbounded form of Tag 0D5W; the compatibility with boundary maps is NOT carried”.

In the situation of [Stacks, Tag 0DJQ] there are isomorphisms

H^i(S, K ⊗^L_{𝒪_S} ℱ) ≅ H^i(X, E ⊗^L_{𝒪_X} (𝒢 ⊗_{𝒪_X} f^*ℱ)),

functorial in the 𝒪_S-module ℱ — the statement is a natural isomorphism of functors on 𝒪_S-modules, so functoriality is part of its type — and Γ(S, 𝒪_S)-linear. Quasi-coherence of ℱ is not assumed.

Two steps of the source's proof are carried, as the projectionFormula and mixedFlatTensor fields of h: [Stacks, Tag 08EU] at ℱ, which this library proves only at ℱ = 𝒪_S, and the identification 𝒢 ⊗^L_{𝒪_X} Lf^*ℱ ≅ 𝒢 ⊗_{𝒪_X} f^*ℱ, which is [Stacks, Tag 08DE] together with flatness of the 𝒢^n over S. The other two steps are proved: associativity of the derived tensor product, and Leray in the unbounded form [Stacks, Tag 0D5W], which holds with no hypothesis on f and which the bounded-below [Stacks, Tag 01EZ] that the source cites does not cover here.

The compatibility with boundary maps is not part of this statement; see the module docstring for what it asks and why naturality does not give it.

def extCohomologyIso (h : ExtProjectionInput f E G) (i : ℤ) :
    baseTensorFunctor f E G ⋙ cohomologyOnBase S i ≅
      pullbackTensorFunctor f E G ⋙ cohomologyOnSource f i

Stacks.Cohomology.ExtProjectionFormulaBoundary.extCohomologyIso_qcoh_boundary, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ExtProjectionFormulaBoundary.lean, line 182. The attribute's comment: “the functorial isomorphisms on quasi-coherent F for every i, and their compatibility with the boundary maps of every short exact sequence of quasi-coherent modules; H^i(S, -) = H^i of unbounded RΓ(S, -), H^i(X, -) as a Γ(S, O_S)-module along f^♯, boundary maps the connecting morphisms of H^0 at the image under RΓ(S, -) of K ⊗^L (triangle of the sequence) and at the image under RΓ(X, E ⊗^L -) of the triangle of 0 → G ⊗ f^F₁ → G ⊗ f^F₂ → G ⊗ f^*F₃ → 0; no hypothesis beyond those of Tag 0DJQ”.

[Stacks, Tag 0A1F]. Let S be a Noetherian scheme, f : X ⟶ S a morphism locally of finite type, E ∈ D(𝒪_X) perfect and 𝒢 a bounded complex of coherent 𝒪_X-modules, flat over S, whose support is contained in a closed subset proper over S (the assumptions of [Stacks, Tag 0DJQ]), and let K = Rf_*(E ⊗^𝐋_{𝒪_X} 𝒢). Then there are isomorphisms

H^i(S, K ⊗^𝐋_{𝒪_S} ℱ) ≅ H^i(X, E ⊗^𝐋_{𝒪_X} (𝒢 ⊗_{𝒪_X} f^*ℱ)),

functorial in the quasi-coherent 𝒪_S-module ℱ (a natural isomorphism of functors on the full subcategory of quasi-coherent modules, for every i), and compatible with boundary maps: for a short exact sequence 0 → ℱ₁ → ℱ₂ → ℱ₃ → 0 of quasi-coherent 𝒪_S-modules the square formed with the connecting morphisms commutes, where on the left the connecting morphism is that of H^*(S, -) at the distinguished triangle K ⊗^𝐋 ℱ₁ → K ⊗^𝐋 ℱ₂ → K ⊗^𝐋 ℱ₃ → (K ⊗^𝐋 ℱ₁)[1], and on the right that of H^*(X, E ⊗^𝐋 -) at the distinguished triangle of the short exact sequence of complexes 0 → 𝒢 ⊗ f^*ℱ₁ → 𝒢 ⊗ f^*ℱ₂ → 𝒢 ⊗ f^*ℱ₃ → 0.

Here H^i(S, -) is the i-th cohomology of unbounded derived global sections, valued in Γ(S, 𝒪_S)-modules, H^i(X, -) is read as a Γ(S, 𝒪_S)-module by restriction along f^♯, the connecting morphisms are CategoryTheory.Functor.homologySequenceδ of the homological functor H^0 at the image triangles, and 𝒢 ⊗ f^*ℱ is the complex with terms 𝒢^p ⊗ f^*ℱ (Stacks.Cohomology.ExtProjectionFormula.tensorModuleComplex); its short exactness is shortExact_Ψ, proved from flatness of the 𝒢^p over S.

Every step of the source's proof is proved: the projection formula ([Stacks, Tag 08EU]) through a quasi-compact open neighbourhood of the support (f need not be quasi-compact), associativity, Leray ([Stacks, Tag 0D5W]) and the flat identification 𝒢 ⊗^𝐋 Lf^*ℱ ≅ 𝒢 ⊗ f^*ℱ ([Stacks, Tag 08DE] with flatness over S); the isomorphisms in degree i are obtained from a degree-zero comparison evaluated at ℱ[i], which is what makes them compatible with the connecting morphisms.

theorem extCohomologyIso_qcoh_boundary [IsNoetherian S] [LocallyOfFiniteType f]
    (hE : RingedSpace.IsPerfect (X := X.toRingedSpace) E)
    (hG : PerfectPushforward.FlatProperSupportComplex f G) :
    ∃ Φ : ∀ i : ℤ, (qcModules S).ι ⋙ DerivedCategory.singleFunctor (ModS S) 0 ⋙
          (Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor S.toRingedSpace.sheaf).obj
            (Kobj f E G) ⋙
          Stacks.Cohomology.DerivedSectionsLeray.derivedSectionsOverOpen S.toRingedSpace ⊤ ⋙
          DerivedCategory.homologyFunctor _ i ≅
        (qcModules S).ι ⋙ Ψ f G ⋙ DerivedCategory.Q ⋙
          (Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor X.toRingedSpace.sheaf).obj
            E ⋙
          Stacks.Cohomology.DerivedSectionsLeray.derivedPreimageSections f.toLRSHom.toShHom ⊤ ⋙
          DerivedCategory.homologyFunctor _ i,
      ∀ (T : ShortComplex (ModS S)) (hT : T.ShortExact) (h₁ : qcModules S T.X₁)
        (h₃ : qcModules S T.X₃) (i : ℤ),
        (Φ i).hom.app ⟨T.X₃, h₃⟩ ≫
          (H0 (S := S)).homologySequenceδ
            ((sourceSections f E).mapTriangle.obj
              (DerivedCategory.triangleOfSES (shortExact_Ψ f G hG T hT))) i (i + 1) rfl =
        (H0 (S := S)).homologySequenceδ
            ((sectionsS (S := S)).mapTriangle.obj
              ((tensorK f E G).mapTriangle.obj hT.singleTriangle)) i (i + 1) rfl ≫
          (Φ (i + 1)).hom.app ⟨T.X₁, h₁⟩

Tag 08ID, a lemma

Tag 08ID in the Stacks Project.

Stacks.Cohomology.ExtPerfectProjection.extIso_qcoh_boundary, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ExtPerfectProjectionBoundary.lean, line 206. The attribute's comment: “the functorial isomorphisms for every i, Ext^i read as Hom_{D(O_X)}(E, -[i]), and their compatibility with the boundary maps of every short exact sequence of quasi-coherent modules (ℱ₂ need not be assumed quasi-coherent): the class of a boundary is the Yoneda composite with the connecting morphism of the triangle of 0 → G ⊗ f^F₁ → G ⊗ f^F₂ → G ⊗ f^*F₃ → 0; H^i(S, -) is H^i of unbounded RΓ(S, -) with its Γ(S, O_S)-module structure forgotten”.

[Stacks, Tag 08ID]. Let S be a Noetherian scheme, f : X ⟶ S locally of finite type, E a perfect object of D(𝒪_X) and 𝒢 a bounded complex of coherent 𝒪_X-modules, flat over S, with support proper over S, and let K = Rf_* RSheafHom(E, 𝒢) as in [Stacks, Tag 0DJR]. Then there are isomorphisms

Φᵢ : H^i(S, K ⊗^L_{𝒪_S} ℱ) ⟶ Ext^i_{𝒪_X}(E, 𝒢 ⊗_{𝒪_X} f^*ℱ) = Hom_{D(𝒪_X)}(E, (𝒢 ⊗ f^*ℱ)[i]),

functorial in the quasi-coherent 𝒪_S-module ℱ (a natural isomorphism of functors on quasi-coherent modules for every i), compatible with boundary maps: for a short exact sequence 0 → ℱ₁ → ℱ₂ → ℱ₃ → 0 of 𝒪_S-modules with ℱ₁, ℱ₃ quasi-coherent and every class y in H^i(S, K ⊗^L ℱ₃),

Φᵢ₊₁(∂ y) = Φᵢ(y) ∘ δ,

where ∂ : H^i(S, K ⊗^L ℱ₃) ⟶ H^{i+1}(S, K ⊗^L ℱ₁) is the connecting morphism of the distinguished triangle K ⊗^L ℱ₁ → K ⊗^L ℱ₂ → K ⊗^L ℱ₃ → (K ⊗^L ℱ₁)[1] (the image under K ⊗^L - of the triangle of the sequence) and δ : 𝒢 ⊗ f^*ℱ₃ ⟶ (𝒢 ⊗ f^*ℱ₁)[1] is the connecting morphism of the distinguished triangle of the short exact sequence of complexes 0 → 𝒢 ⊗ f^*ℱ₁ → 𝒢 ⊗ f^*ℱ₂ → 𝒢 ⊗ f^*ℱ₃ → 0, composed as an element of Ext¹.

H^i(S, -) is the i-th cohomology of the unbounded derived global sections; it is a group of Γ(S, 𝒪_S)-modules, read as an abelian group and lifted to the universe of the morphism groups of D(𝒪_X). f^* is the pullback of modules and 𝒢 ⊗ f^*ℱ the complex with terms 𝒢^p ⊗ f^*ℱ.

theorem extIso_qcoh_boundary [IsNoetherian S] [LocallyOfFiniteType f]
    (hE : RingedSpace.IsPerfect (X := X.toRingedSpace) E)
    (hG : PerfectPushforward.FlatProperSupportComplex f G) :
    ∃ Φ : ∀ i : ℤ, (qcModules S).ι ⋙ DerivedCategory.singleFunctor (ModS S) 0 ⋙
          tensorSheafHomK f E G ⋙ sectionsS (S := S) ⋙ DerivedCategory.homologyFunctor _ i ⋙
          forgetLift (Y := S.toRingedSpace) ≅
        (qcModules S).ι ⋙ Ψ f G ⋙ DerivedCategory.Q ⋙ shiftFunctor _ i ⋙
          preadditiveCoyoneda.obj (op E),
      ∀ (T : ShortComplex (ModS S)) (hT : T.ShortExact) (h₁ : qcModules S T.X₁)
        (h₃ : qcModules S T.X₃) (i : ℤ)
        (y : ((qcModules S).ι ⋙ DerivedCategory.singleFunctor (ModS S) 0 ⋙
          tensorSheafHomK f E G ⋙ sectionsS (S := S) ⋙ DerivedCategory.homologyFunctor _ i ⋙
          forgetLift (Y := S.toRingedSpace)).obj ⟨T.X₃, h₃⟩),
        (Φ (i + 1)).hom.app ⟨T.X₁, h₁⟩
            ((forgetLift (Y := S.toRingedSpace)).map ((H0 (S := S)).homologySequenceδ
              ((sectionsS (S := S)).mapTriangle.obj
                ((tensorSheafHomK f E G).mapTriangle.obj hT.singleTriangle)) i (i + 1) rfl) y) =
          ((Φ i).hom.app ⟨T.X₃, h₃⟩ y : E ⟶ _) ≫
            (DerivedCategory.triangleOfSESδ
              (Stacks.Cohomology.ExtProjectionFormulaBoundary.shortExact_Ψ f G hG T hT))⟦i⟧' ≫
            (shiftFunctorAdd' _ 1 i (i + 1) (by omega)).inv.app _

Stacks.Cohomology.ExtProjectionFormulaQuasiCoherent.extCohomologyIsoSheafHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ExtProjectionFormulaQuasiCoherent.lean, line 225. The attribute's comment: “the functorial isomorphisms for every i, as a natural isomorphism in ℱ ranging over all 𝒪_S-modules rather than only the quasi-coherent ones (the restriction to the quasi-coherent ones is extCohomologyIsoQuasicoherent), and Γ(S, 𝒪_S)-linear, with Ext^i_{𝒪_X}(E, -) read as the i-th hypercohomology on X of the derived internal Hom out of E, which is Tag 08DK; the source's reduction to Tag 0A1F is carried out, that tag being applied here and not assumed, so the only thing granted beyond its own input bundle is Tag 08DQ for E, as hdual: a dual E-dual with a natural isomorphism from its derived tensor product to the derived internal Hom out of E, which this tree lacks at this spelling, exactly as PerfectInternalHomPushforward records for Tag 0DJR; S is not assumed Noetherian, that assumption serving in Tag 0DJR only to make K perfect, which is not used; the compatibility with boundary maps is NOT carried -- the source omits that verification and naturality in ℱ gives only the squares on the first two legs of the two distinguished triangles”.

[Stacks, Tag 08ID]. In the situation of [Stacks, Tag 0DJR], with K = Rf_*RSheafHom_{𝒪_X}(E, 𝒢), there are isomorphisms

H^i(S, K ⊗^L_{𝒪_S} ℱ) ≅ Ext^i_{𝒪_X}(E, 𝒢 ⊗_{𝒪_X} f^*ℱ),

functorial in the 𝒪_S-module ℱ — the statement is a natural isomorphism of functors on 𝒪_S-modules, so functoriality is part of its type — and Γ(S, 𝒪_S)-linear. The right-hand side is the i-th hypercohomology of RSheafHom_{𝒪_X}(E, 𝒢 ⊗_{𝒪_X} f^*ℱ) on X, which is Ext^i_{𝒪_X}(E, 𝒢 ⊗_{𝒪_X} f^*ℱ) by [Stacks, Tag 08DK]. Quasi-coherence of ℱ is not assumed; see extCohomologyIsoQuasicoherent for the restriction to quasi-coherent modules that the source states.

This is the source's proof. hdual, which is [Stacks, Tag 08DQ] for E, turns perfectness of E into a dual E^∨ with E^∨ ⊗^L_{𝒪_X} - ≅ RSheafHom_{𝒪_X}(E, -). Applying that at 𝒢 and pushing forward identifies K with the K of [Stacks, Tag 0DJQ] for (E^∨, 𝒢), applying it at 𝒢 ⊗_{𝒪_X} f^*ℱ identifies the right-hand side with H^i(X, E^∨ ⊗^L_{𝒪_X} (𝒢 ⊗ f^*ℱ)), and in between the assertion is [Stacks, Tag 0A1F] at E^∨.

Beyond hdual nothing is carried here: h is the input bundle of [Stacks, Tag 0A1F] at E^∨, whose two carried fields are the projection formula [Stacks, Tag 08EU] at ℱ and the flat identification [Stacks, Tag 08DE], and whose other two fields are the source's assumptions on E^∨ and 𝒢. The compatibility with boundary maps is not part of this statement; see the module docstring for what it asks and why naturality does not give it.

def extCohomologyIsoSheafHom (hE : RingedSpace.IsPerfect (X := X.toRingedSpace) E)
    (hdual : RingedSpace.IsPerfect (X := X.toRingedSpace) E → DualSheafHomData E)
    (h : ExtProjectionInput f (hdual hE).dual G) (i : ℤ) :
    baseTensorSheafHomFunctor f E G ⋙ cohomologyOnBase S i ≅
      extFunctor f E G ⋙ cohomologyOnSource f i

Tag 08IF, a lemma

Tag 08IF in the Stacks Project.

Stacks.Cohomology.RelativeExt.exists_perfect_relativeExt_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativeExt/PartA.lean, line 51. The attribute's comment: “(A)”.

Let S be a Noetherian scheme, f : X ⟶ S a morphism locally of finite type, E ∈ D^-_{Coh}(𝒪_X) and 𝒢 a bounded complex of coherent 𝒪_X-modules, flat over S, with support proper over S. For every m there are a perfect object K of D(𝒪_S) and maps

α^i_ℱ : Ext^i_{𝒪_X}(E, 𝒢 ⊗_{𝒪_X} f^*ℱ) ⟶ H^i(S, K ⊗^L_{𝒪_S} ℱ)

for quasi-coherent ℱ (with H^i(S, -) = Ext^i_{𝒪_S}(𝒪_S, -)), which are additive, functorial in ℱ, compatible with the boundary maps of short exact sequences 0 ⟶ ℱ₁ ⟶ ℱ₂ ⟶ ℱ₃ ⟶ 0 of quasi-coherent modules (on the left, the connecting morphism of 0 ⟶ 𝒢 ⊗ f^*ℱ₁ ⟶ 𝒢 ⊗ f^*ℱ₂ ⟶ 𝒢 ⊗ f^*ℱ₃ ⟶ 0, exact because 𝒢 is flat over S; on the right, that of the distinguished triangle K ⊗^L ℱ₁ ⟶ K ⊗^L ℱ₂ ⟶ K ⊗^L ℱ₃ ⟶), and bijective for i ≤ m.

theorem exists_perfect_relativeExt_comparison (E : DStd X) (hE : IsBoundedAboveCoherent E)
    (G : CochainComplex (TModules X.toRingedSpace) ℤ)
    (hG : Stacks.Cohomology.PerfectPushforward.FlatProperSupportComplex f G) (m : ℤ) :
    ∃ K : DStd S, IsPerfectObject K ∧
      ∃ α : ∀ (i : ℤ) (F : SheafOfModules.{u} (structureSheafRing S.toRingedSpace)),
          F.IsQuasicoherent → (relativeExtGroup f G E F i →+ baseTensorGroup K F i),
        (∀ (i : ℤ) (F F' : SheafOfModules.{u} (structureSheafRing S.toRingedSpace))
            (hF : F.IsQuasicoherent) (hF' : F'.IsQuasicoherent) (v : F ⟶ F')
            (y : relativeExtGroup f G E F i),
          α i F' hF' (relativeExtMap f G E i v y) = baseTensorMap i K v (α i F hF y)) ∧
        (∀ (A : ShortComplex (SheafOfModules.{u} (structureSheafRing S.toRingedSpace)))
            (hA : A.ShortExact) (h₁ : A.X₁.IsQuasicoherent) (h₃ : A.X₃.IsQuasicoherent)
            (n m' : ℤ) (h : 1 + n = m') (y : relativeExtGroup f G E A.X₃ n),
          α m' A.X₁ h₁ (relativeExtBoundaryMap E
              (isBoundedFlatOver_of_flatProperSupportComplex hG) hA n m' h y) =
            baseTensorBoundaryMap K hA n m' h (α n A.X₃ h₃ y)) ∧
        (∀ (i : ℤ), i ≤ m → ∀ (F : SheafOfModules.{u} (structureSheafRing S.toRingedSpace))
            (hF : F.IsQuasicoherent), Function.Bijective (α i F hF))

Stacks.Cohomology.RelativeExt.exists_pseudoCoherent_relativeExt_representative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativeExt/PartB.lean, line 369. The attribute's comment: “(B)”.

[Stacks, Tag 08IF] (B). Let S be a Noetherian scheme, f : X ⟶ S a morphism locally of finite type, E ∈ D^-_{Coh}(𝒪_X) and 𝒢 a bounded complex of coherent 𝒪_X-modules, flat over S, with support proper over S. There is a pseudo-coherent object L of D(𝒪_S) and isomorphisms

Ext^i_{𝒪_S}(L, ℱ) ≅ Ext^i_{𝒪_X}(E, 𝒢 ⊗_{𝒪_X} f^*ℱ)

for all i and all quasi-coherent ℱ, functorial in ℱ and compatible with the boundary maps of short exact sequences 0 ⟶ ℱ₁ ⟶ ℱ₂ ⟶ ℱ₃ ⟶ 0 of quasi-coherent modules (on the left, composition with the connecting morphism ℱ₃ ⟶ ℱ₁[1]; on the right, with that of 0 ⟶ 𝒢 ⊗ f^*ℱ₁ ⟶ 𝒢 ⊗ f^*ℱ₂ ⟶ 𝒢 ⊗ f^*ℱ₃ ⟶ 0, exact because 𝒢 is flat over S).

theorem exists_pseudoCoherent_relativeExt_representative (E : DStd X)
    (hE : IsBoundedAboveCoherent E) (G : CochainComplex (TModules X.toRingedSpace) ℤ)
    (hG : Stacks.Cohomology.PerfectPushforward.FlatProperSupportComplex f G) :
    ∃ L : DStd S, IsPseudoCoherentObject L ∧
      ∃ β : ∀ (i : ℤ) (F : SheafOfModules.{u} (structureSheafRing S.toRingedSpace)),
          F.IsQuasicoherent → (baseExtGroup L F i ≃+ relativeExtGroup f G E F i),
        (∀ (i : ℤ) (F F' : SheafOfModules.{u} (structureSheafRing S.toRingedSpace))
            (hF : F.IsQuasicoherent) (hF' : F'.IsQuasicoherent) (v : F ⟶ F')
            (z : baseExtGroup L F i),
          β i F' hF' (baseExtMap L i v z) = relativeExtMap f G E i v (β i F hF z)) ∧
        (∀ (A : ShortComplex (SheafOfModules.{u} (structureSheafRing S.toRingedSpace)))
            (hA : A.ShortExact) (h₁ : A.X₁.IsQuasicoherent) (h₃ : A.X₃.IsQuasicoherent)
            (n m : ℤ) (h : 1 + n = m) (z : baseExtGroup L A.X₃ n),
          β m A.X₁ h₁ (baseExtBoundaryMap L hA n m h z) =
            relativeExtBoundaryMap E (isBoundedFlatOver_of_flatProperSupportComplex hG) hA n m
              h (β n A.X₃ h₃ z))

Tag 0DJS, a remark

Tag 0DJS in the Stacks Project.

Stacks.Cohomology.RelativeExtCanonical.exists_baseChange_relativeExt_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativeExtCanonical/BaseChangeExt.lean, line 102. The attribute's comment: “base change”.

[Stacks, Tag 0DJS]: formation of the complex L of [Stacks, Tag 08IF] (B) is compatible with base change. Let S be Noetherian, f : X ⟶ S locally of finite type, E ∈ D^-_{Coh}(𝒪_X) and 𝒢 a bounded complex of coherent 𝒪_X-modules, flat over S, with support proper over S, and let L be the pseudo-coherent complex of (B). For every cartesian square of schemes with g' : X' ⟶ X, f' : X' ⟶ S', g : S' ⟶ S there are isomorphisms

Ext^i_{𝒪_{S'}}(Lg^*L, ℱ') ≅ Ext^i_{𝒪_{X'}}(L(g')^*E, (g')^*𝒢 ⊗_{𝒪_{X'}} (f')^*ℱ')

for quasi-coherent ℱ' on S', with (g')^*𝒢 the ordinary termwise pullback of 𝒢, which are functorial in ℱ' and compatible with the boundary maps of short exact sequences. They are canonical: they are the ones induced by an identification Hom(Lg^*L, N) ≃ Hom(L(g')^*E, L(f')^*N ⊗^L (g')^*𝒢) natural in N ∈ D^+_{QCoh}(𝒪_{S'}).

theorem exists_baseChange_relativeExt_iso :
    ∃ β : ∀ (i : ℤ) (F' : SheafOfModules.{u} (structureSheafRing S'.toRingedSpace)),
        F'.IsQuasicoherent →
        (baseExtGroup (baseChangedRepresentative f E hE G hG g) F' i ≃+
          relativeExtGroup f'
            ((Stacks.Cohomology.DerivedPullbackTensor.pullbackComplex g'.toLRSHom.toShHom).obj G)
            (baseChangedSource E g') F' i),
      (∀ (i : ℤ) (F F' : SheafOfModules.{u} (structureSheafRing S'.toRingedSpace))
          (hF : F.IsQuasicoherent) (hF' : F'.IsQuasicoherent) (v : F ⟶ F')
          (z : baseExtGroup (baseChangedRepresentative f E hE G hG g) F i),
        β i F' hF' (baseExtMap _ i v z) =
          relativeExtMap f'
            ((Stacks.Cohomology.DerivedPullbackTensor.pullbackComplex g'.toLRSHom.toShHom).obj G)
            (baseChangedSource E g') i v (β i F hF z)) ∧
      (∀ (A : ShortComplex (SheafOfModules.{u} (structureSheafRing S'.toRingedSpace)))
          (hA : A.ShortExact) (h₁ : A.X₁.IsQuasicoherent) (h₃ : A.X₃.IsQuasicoherent)
          (n m : ℤ) (h : 1 + n = m)
          (z : baseExtGroup (baseChangedRepresentative f E hE G hG g) A.X₃ n),
        β m A.X₁ h₁ (baseExtBoundaryMap _ hA n m h z) =
          relativeExtBoundaryMap (baseChangedSource E g')
            (isBoundedFlatOver_total_pullback hsq hG) hA n m h (β n A.X₃ h₃ z)) ∧
      ∃ θ : ShiftedHom.NaturalHomEquiv (𝟭 (DStd S'))
          (pullbackTensorDerivedFunctor (isBoundedFlatOver_total_pullback hsq hG))
          (baseChangedRepresentative f E hE G hG g)
          (baseChangedSource E g') (plusQCohDerived S'),
        ∀ (i : ℤ) (F' : SheafOfModules.{u} (structureSheafRing S'.toRingedSpace))
          (hF' : F'.IsQuasicoherent),
          β i F' hF' = extIsoOfIdentification (isBoundedFlatOver_total_pullback hsq hG)
            (θ.toIdentification (plusQCohDerived_biprod S')) i F' hF'

Stacks.Cohomology.RelativeExtCanonical.exists_iso_pseudoCoherentRepresentative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativeExtCanonical/Canonicity.lean, line 63. The attribute's comment: “canonical”.

The pseudo-coherent complex L representing relative Ext is canonical. Let S be Noetherian, f : X ⟶ S locally of finite type, E ∈ D^-_{Coh}(𝒪_X) and 𝒢 a bounded complex of coherent 𝒪_X-modules, flat over S, with support proper over S; let L be the pseudo-coherent complex pseudoCoherentRepresentative f E hE G hG, with its identification θ_N : Hom(L, N) ≃ Hom(E, Lf^*N ⊗^L 𝒢), natural in N ∈ D^+_{QCoh}(𝒪_S), and the isomorphisms Ext^i_{𝒪_S}(L, ℱ) ≅ Ext^i_{𝒪_X}(E, 𝒢 ⊗ f^*ℱ) it induces. Then these are functorial in quasi-coherent ℱ and compatible with boundary maps, and for every L' with quasi-coherent cohomology and every identification θ'_N : Hom(L', N) ≃ Hom(E, Lf^*N ⊗^L 𝒢) natural in N ∈ D^+_{QCoh}(𝒪_S) there is an isomorphism φ : L' ≅ L with θ'(φ ∘ x) = θ(x) for all such N and x : L ⟶ N; in particular φ carries the Ext-isomorphisms induced by θ' to those of L.

theorem exists_iso_pseudoCoherentRepresentative (E : DStd X) (hE : IsBoundedAboveCoherent E)
    (G : CochainComplex (TModules X.toRingedSpace) ℤ)
    (hG : Stacks.Cohomology.PerfectPushforward.FlatProperSupportComplex f G) :
    IsPseudoCoherentObject (pseudoCoherentRepresentative f E hE G hG) ∧
    (∀ (i : ℤ) (F F' : SheafOfModules.{u} (structureSheafRing S.toRingedSpace))
        (hF : F.IsQuasicoherent) (hF' : F'.IsQuasicoherent) (v : F ⟶ F')
        (z : baseExtGroup (pseudoCoherentRepresentative f E hE G hG) F i),
      extIsoOfIdentification (isBoundedFlatOver_of_flatProperSupportComplex hG)
          ((pseudoCoherentRepresentativeHomEquiv f E hE G hG).toIdentification
            (plusQCohDerived_biprod S)) i F' hF'
          (baseExtMap (pseudoCoherentRepresentative f E hE G hG) i v z) =
        relativeExtMap f G E i v
          (extIsoOfIdentification (isBoundedFlatOver_of_flatProperSupportComplex hG)
            ((pseudoCoherentRepresentativeHomEquiv f E hE G hG).toIdentification
              (plusQCohDerived_biprod S)) i F hF z)) ∧
    (∀ (A : ShortComplex (SheafOfModules.{u} (structureSheafRing S.toRingedSpace)))
        (hA : A.ShortExact) (h₁ : A.X₁.IsQuasicoherent) (h₃ : A.X₃.IsQuasicoherent)
        (n m : ℤ) (h : 1 + n = m)
        (z : baseExtGroup (pseudoCoherentRepresentative f E hE G hG) A.X₃ n),
      extIsoOfIdentification (isBoundedFlatOver_of_flatProperSupportComplex hG)
          ((pseudoCoherentRepresentativeHomEquiv f E hE G hG).toIdentification
            (plusQCohDerived_biprod S)) m A.X₁ h₁
          (baseExtBoundaryMap (pseudoCoherentRepresentative f E hE G hG) hA n m h z) =
        relativeExtBoundaryMap E (isBoundedFlatOver_of_flatProperSupportComplex hG) hA n m h
          (extIsoOfIdentification (isBoundedFlatOver_of_flatProperSupportComplex hG)
            ((pseudoCoherentRepresentativeHomEquiv f E hE G hG).toIdentification
              (plusQCohDerived_biprod S)) n A.X₃ h₃ z)) ∧
    ∀ (L' : DStd S) (_ : qcohDerived S L')
      (θ' : ShiftedHom.NaturalHomEquiv (𝟭 (DStd S))
        (pullbackTensorDerivedFunctor (isBoundedFlatOver_of_flatProperSupportComplex hG)) L' E
        (plusQCohDerived S)),
      ∃ φ : L' ≅ pseudoCoherentRepresentative f E hE G hG,
        (∀ (N : DStd S) (hN : plusQCohDerived S N)
            (x : pseudoCoherentRepresentative f E hE G hG ⟶ N),
          θ'.equiv N hN (φ.hom ≫ x) =
            (pseudoCoherentRepresentativeHomEquiv f E hE G hG).equiv N hN x) ∧
        ∀ (i : ℤ) (F : SheafOfModules.{u} (structureSheafRing S.toRingedSpace))
          (hF : F.IsQuasicoherent)
          (z : baseExtGroup (pseudoCoherentRepresentative f E hE G hG) F i),
          extIsoOfIdentification (isBoundedFlatOver_of_flatProperSupportComplex hG)
              (θ'.toIdentification (plusQCohDerived_biprod S)) i F hF (φ.hom ≫ z) =
            extIsoOfIdentification (isBoundedFlatOver_of_flatProperSupportComplex hG)
              ((pseudoCoherentRepresentativeHomEquiv f E hE G hG).toIdentification
                (plusQCohDerived_biprod S)) i F hF z

Sources

LeanStacks.Cohomology.ExtProjectionFormula.extCohomologyIso · Stacks.Cohomology.ExtProjectionFormulaBoundary.extCohomologyIso_qcoh_boundary · Stacks.Cohomology.ExtPerfectProjection.extIso_qcoh_boundary · Stacks.Cohomology.ExtProjectionFormulaQuasiCoherent.extCohomologyIsoSheafHom · Stacks.Cohomology.RelativeExt.exists_perfect_relativeExt_comparison · Stacks.Cohomology.RelativeExt.exists_pseudoCoherent_relativeExt_representative · Stacks.Cohomology.RelativeExtCanonical.exists_baseChange_relativeExt_iso · Stacks.Cohomology.RelativeExtCanonical.exists_iso_pseudoCoherentRepresentative

Section36.29 Limits and derived categories #

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

Tag 09RD, a situation

Tag 09RD in the Stacks Project.

AlgebraicGeometry.DescentSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/Limits.lean, line 36. References: SGA 6 IV (3.2).

A directed inverse system of quasi-compact and quasi-separated schemes whose transition morphisms are affine, equipped with a chosen limit cone and a chosen index.

structure AlgebraicGeometry.DescentSituation (I : Type v) [Preorder I]
    [IsDirected I (· ≤ ·)]

Tag 09RE, a lemma

Tag 09RE in the Stacks Project.

AlgebraicGeometry.DescentSituation.homProjection_homTransition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/LimitHomDescent.lean, line 206. The attribute's comment: “the maps to Hom(E, K) are compatible with the transition maps of the directed system, for all E_0 and K_0”.

The cocone clause of the conclusion of Stacks 09RE. Pushing a homomorphism from the stage i to the stage j and then to the limit gives the same homomorphism E ⟶ K as pushing it to the limit directly.

This holds for all E₀ and K₀: it is the coherence of the two comparison isomorphisms of derived pullback along the factorisations f_{ji} ≫ f_{i0} = f_{j0} and f_j ≫ f_{ji} = f_i, together with the naturality of the second.

theorem homProjection_homTransition (i j : D.Stages) (h : i ≤ j)
    (g : stageObj E₀ i ⟶ stageObj K₀ i) :
    homProjection E₀ K₀ j (homTransition E₀ K₀ i j h g) = homProjection E₀ K₀ i g

AlgebraicGeometry.DescentSituation.homTransition_homTransition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/LimitHomDescent.lean, line 225. The attribute's comment: “the directed system whose colimit the tag takes: its transition maps compose, for all E_0 and K_0”.

The maps of the directed system of Stacks 09RE compose. For i ≤ j ≤ k among the stages, pushing a homomorphism from the stage i to the stage j and then to the stage k gives the same homomorphism E_k ⟶ K_k as pushing it to the stage k directly. Together with AlgebraicGeometry.DescentSituation.homProjection_homTransition this says that i ↦ Hom_{D(𝒪_{S_i})}(E_i, K_i) is a system over the stages and that the maps to Hom_{D(𝒪_S)}(E, K) form a cocone on it, which is what makes the colimit the tag speaks of well-posed.

Like the cocone clause, this holds for all E₀ and K₀; it is the cocycle identity of the comparisons Lf_{i0}^* ⋙ Lf_{ji}^* ≅ Lf_{j0}^*.

theorem homTransition_homTransition (i j k : D.Stages) (h : i ≤ j) (h' : j ≤ k)
    (g : stageObj E₀ i ⟶ stageObj K₀ i) :
    homTransition E₀ K₀ j k h' (homTransition E₀ K₀ i j h g) =
      homTransition E₀ K₀ i k (h.trans h') g

AlgebraicGeometry.DescentSituation.isHomColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/LimitHomDescent.lean, line 301.

Stacks 09RE. In Situation 09RD, let E₀ and K₀ be objects of D(𝒪_{S₀}), put E_i = Lf_{i0}^*E₀, K_i = Lf_{i0}^*K₀ for i ≥ 0 and E = Lf_0^*E₀, K = Lf_0^*K₀. If either E₀ is perfect and K₀ lies in D_QCoh(𝒪_{S₀}), or E₀ is pseudo-coherent and K₀ lies in D_QCoh(𝒪_{S₀}) and has finite Tor dimension, then

colim_{i ≥ 0} Hom_{D(𝒪_{S_i})}(E_i, K_i) ⟶ Hom_{D(𝒪_S)}(E, K)

is an isomorphism.

The index set lies in the universe of the schemes; over a larger index set the statement fails, see AlgebraicGeometry.DescentSituation.exists_not_isHomColimit.

theorem isHomColimit
    (hcase :
      (Stacks.Cohomology.PerfectComplexes.IsPerfect
            (X := (D.stage D.base).toRingedSpace) E₀ ∧
          ∀ n : ℤ, SheafOfModules.isQuasicoherent (D.stage D.base).ringCatSheaf
            ((DerivedCategory.homologyFunctor (D.stage D.base).Modules n).obj K₀)) ∨
        (AlgebraicGeometry.RingedSpace.PseudoCoherence.IsPseudoCoherent
            (X := (D.stage D.base).toRingedSpace) E₀ ∧
          (∀ n : ℤ, SheafOfModules.isQuasicoherent (D.stage D.base).ringCatSheaf
            ((DerivedCategory.homologyFunctor (D.stage D.base).Modules n).obj K₀)) ∧
          Stacks.Cohomology.TorAmplitude.HasFiniteTorDimension
            (D.stage D.base).toRingedSpace K₀)) :
    IsHomColimit E₀ K₀

Tag 09RF, a lemma

Tag 09RF in the Stacks Project.

AlgebraicGeometry.DescentSituation.perfect_isColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/LimitPerfectCategoryColimit.lean, line 201.

[Stacks, Tag 09RF]. In the situation of [Stacks, Tag 09RD], the category of perfect objects of D(𝒪_S) is the colimit of the categories of perfect objects of D(𝒪_{S_i}): the comparison functor out of the colimit, induced by derived pullback along the projections, is

essentially surjective — every perfect object of D(𝒪_S) is isomorphic to the derived pullback of a perfect object of D(𝒪_{S_i}) for some i; and

fully faithful — for perfect E and K on a stage S_i, the group Hom_{D(𝒪_S)}(Lf_i^*E, Lf_i^*K) is the filtered colimit over j ≥ i of the groups Hom_{D(𝒪_{S_j})}(Lf_{ji}^*E, Lf_{ji}^*K).

A morphism of the colimit category between objects living at two stages is a morphism after pullback to a common later stage, so the second clause, stated for two objects of one stage, is the whole of full faithfulness.

theorem perfect_isColimit :
    (∀ (E : DerivedCategory D.limitScheme.Modules),
      IsPerfect (X := D.limitScheme.toRingedSpace) E →
      ∃ (i : I) (_ : D.base ≤ i) (Eᵢ : DerivedCategory (D.stage i).Modules),
        IsPerfect (X := (D.stage i).toRingedSpace) Eᵢ ∧
          Nonempty ((derivedPullback (D.projection i).toLRSHom.toShHom).obj Eᵢ ≅ E)) ∧
    (∀ (i : I) (E K : DerivedCategory (D.stage i).Modules),
      IsPerfect (X := (D.stage i).toRingedSpace) E →
      IsPerfect (X := (D.stage i).toRingedSpace) K → IsHomColimit (D := D.atStage i) E K)

AlgebraicGeometry.DescentSituation.isPerfect_transition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/LimitPerfectObjects.lean, line 135. The attribute's comment: “derived pullback along the transition morphisms of the situation sends perfect objects to perfect objects, so the transition functors of the colimit statement are defined; the colimit property itself is not included”.

Derived pullback along a transition morphism of the situation preserves perfectness. This is Stacks 09UA at f_{ji}, and it is what makes the transition functor on the categories of perfect objects defined.

theorem isPerfect_transition {i j : I} (h : i ≤ j)
    (E : DerivedCategory (D.stage i).Modules) (hE : IsPerfect (X := (D.stage i).toRingedSpace) E) :
    IsPerfect (X := (D.stage j).toRingedSpace)
      ((derivedPullback (D.transition h).toLRSHom.toShHom).obj E)

AlgebraicGeometry.DescentSituation.isPerfect_projection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/LimitPerfectObjects.lean, line 147. The attribute's comment: “derived pullback along the projections of the situation sends perfect objects to perfect objects, so the comparison functors of the colimit statement are defined; the colimit property itself is not included”.

Derived pullback along a projection of the situation preserves perfectness. This is Stacks 09UA at f_i, and it is what makes the comparison functor from the stage i to the limit defined.

theorem isPerfect_projection (i : I)
    (E : DerivedCategory (D.stage i).Modules) (hE : IsPerfect (X := (D.stage i).toRingedSpace) E) :
    IsPerfect (X := D.limitScheme.toRingedSpace)
      ((derivedPullback (D.projection i).toLRSHom.toShHom).obj E)

AlgebraicGeometry.DescentSituation.perfectComparison_coherence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/LimitPerfectObjects.lean, line 240. The attribute's comment: “the canonical cocone of the colimit statement: the functors between the categories of perfect objects induced by derived pullback along the projections, and their coherence with the transition functors. Neither full faithfulness nor essential surjectivity of the comparison out of the colimit is included”.

The cocone coherence on the categories of perfect objects. For i ≤ j ≤ k, comparing through the stage j and comparing after composing the two transitions give the same isomorphism from the functor out of D_perf(𝒪_{S_i}) through the stage k to the functor out of D_perf(𝒪_{S_i}) directly. Together with AlgebraicGeometry.DescentSituation.perfectTransitionComp_coherence this is the statement that the functors AlgebraicGeometry.DescentSituation.perfectProjection form a coherent cocone over the system of categories of perfect objects.

theorem perfectComparison_coherence {i j k : I} (h : i ≤ j) (h' : j ≤ k)
    (E : PerfectDerivedCategory (D.stage i)) :
    ((D.perfectComparison h').app ((D.perfectTransition h).obj E)).hom ≫
        ((D.perfectComparison h).app E).hom =
      (D.perfectProjection k).map ((D.perfectTransitionComp h h').app E).hom ≫
        ((D.perfectComparison (h.trans h')).app E).hom

AlgebraicGeometry.DescentSituation.perfectTransitionComp_coherence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/LimitPerfectObjects.lean, line 280. The attribute's comment: “the system of categories of perfect objects along the transition morphisms: the transition functors, their composition isomorphisms and the cocycle identity those satisfy. Neither full faithfulness nor essential surjectivity of the comparison out of the colimit is included”.

The system of transition functors on the categories of perfect objects is coherent. For i ≤ j ≤ k ≤ l, the two ways of composing the comparison isomorphisms of the three transitions agree.

theorem perfectTransitionComp_coherence {i j k l : I} (h : i ≤ j) (h' : j ≤ k) (h'' : k ≤ l)
    (E : PerfectDerivedCategory (D.stage i)) :
    ((D.perfectTransitionComp h' h'').app ((D.perfectTransition h).obj E)).hom ≫
        ((D.perfectTransitionComp h (h'.trans h'')).app E).hom =
      (D.perfectTransition h'').map ((D.perfectTransitionComp h h').app E).hom ≫
        ((D.perfectTransitionComp (h.trans h') h'').app E).hom

AlgebraicGeometry.AffinePerfectLimit.exists_isPerfect_stage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/LimitPerfectObjectsSupplement.lean, line 53. The attribute's comment: “essential surjectivity of the comparison out of the colimit, in the affine base case of the source's induction: for a filtered system of rings with colimit R, every perfect object of D(𝒪_{Spec R}) is derived pullback of a perfect object at a stage. The induction over the quasi-compact opens of S_0 that globalises it is not included, and neither is full faithfulness”.

Stacks 09RF, the affine base case of essential surjectivity. Let i ↦ R_i be a filtered diagram of commutative rings whose colimit is computed on underlying sets, with colimit cocone c, and write R = c.pt, so that Spec R is the limit of the affine schemes Spec R_i. Then every perfect object E of D(𝒪_{Spec R}) is, for some stage i, the derived pullback along Spec R ⟶ Spec R_i of a perfect object of D(𝒪_{Spec R_i}).

theorem exists_isPerfect_stage {J : Type u} [Category.{u} J] [IsFiltered J]
    (A : J ⥤ CommRingCat.{u}) [PreservesColimit A (forget CommRingCat.{u})]
    (c : Cocone A) (hc : IsColimit c) (E : DerivedCategory (Spec c.pt).Modules)
    (hE : IsPerfect (X := (Spec c.pt).toRingedSpace) E) :
    ∃ (j : J) (Ej : DerivedCategory (Spec (A.obj j)).Modules),
      IsPerfect (X := (Spec (A.obj j)).toRingedSpace) Ej ∧
        Nonempty ((derivedPullback (Spec.map (c.ι.app j)).toLRSHom.toShHom).obj Ej ≅ E)

Sources

LeanAlgebraicGeometry.DescentSituation · AlgebraicGeometry.DescentSituation.homProjection_homTransition · AlgebraicGeometry.DescentSituation.homTransition_homTransition · AlgebraicGeometry.DescentSituation.isHomColimit · AlgebraicGeometry.DescentSituation.perfect_isColimit · AlgebraicGeometry.DescentSituation.isPerfect_transition · AlgebraicGeometry.DescentSituation.isPerfect_projection · AlgebraicGeometry.DescentSituation.perfectComparison_coherence

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

36.22 Cohomology and base… to 36.29 Limits and derived…

Section36.22 Cohomology and base change, IV#

Tag 08EU, a lemma

Tag 08IA, a definition

Tag 0FXV, a lemma

Tag 0FXW, a lemma

Tag 08IB, a lemma

Tag 0AA7, a lemma

Tag 0BZA, a remark

Tag 0C0V, a lemma

Tag 0E23, a lemma

Sources

Section36.23 Künneth formula, II#

Tag 0FLP, an equation

Tag 0G7V, an equation

Tag 0FLQ, a lemma

Tag 0FML, a lemma

Tag 0FMQ, a lemma

Tag 0G49, an equation

Tag 0FU4, a lemma

Tag 0G7W, a remark

Sources

Section36.24 Künneth formula, III#

Tag 0G4A, the section

Tag 0G4B, an equation

Tag 0FLR, an equation

Tag 0FLT, a lemma

Sources

Section36.25 Künneth formula for Ext#

Tag 0FXY, an equation

Tag 0FXZ, a lemma

Sources

Section36.26 Cohomology and base change, V#

Tag 0DJ7, an equation

Tag 0DJ8, a lemma

Tag 0DJ9, a lemma

Tag 0DJA, a lemma

Tag 0A1D, a lemma

Tag 08IE, a lemma

Sources

Section36.27 Producing perfect complexes#

Tag 08EV, a lemma

Tag 0DJQ, a lemma

Tag 0DJR, a lemma

Tag 0B6F, a lemma

Sources

Section36.28 A projection formula for Ext#

Tag 0A1F, a lemma

Tag 08ID, a lemma

Tag 08IF, a lemma

Tag 0DJS, a remark

Sources

Section36.29 Limits and derived categories#

Tag 09RD, a situation

Tag 09RE, a lemma

Tag 09RF, a lemma

Sources

Section36.22 Cohomology and base change, IV #

Section36.23 Künneth formula, II #

Section36.24 Künneth formula, III #

Section36.25 Künneth formula for Ext #

Section36.26 Cohomology and base change, V #

Section36.27 Producing perfect complexes #

Section36.28 A projection formula for Ext #

Section36.29 Limits and derived categories #