20.45 Glueing complexes to 20.54 Projection formula

Section20.45 Glueing complexes#

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

Tag 08DG, a lemma

Tag 08DG in the Stacks Project.

Stacks.Cohomology.GlueingComplexes.exists_glueing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/GlueingComplexes/TwoOpens.lean, line 1051. The attribute's comment: “existence of a glueing”.

Stacks Project, Tag 08DG. Let X be a ringed space, let jU : U ⟶ X and jV : V ⟶ X be open immersions and let W be their intersection. An object A of D(𝒪_U), an object B of D(𝒪_V) and an isomorphism c : A|_W ≅ B|_W come from an object of D(𝒪_X).

No hypothesis that U and V cover X is needed for the glued object to exist; a cover is what makes it unique.

theorem exists_glueing {X U V W : RingedSpace.{u, u}} (jU : U ⟶ X) (jV : V ⟶ X) (iU : W ⟶ U)
    (iV : W ⟶ V) [SheafedSpace.IsOpenImmersion jU] [SheafedSpace.IsOpenImmersion jV]
    (h : IsPullback iU iV jU jV) (A : DerivedModules U) (B : DerivedModules V)
    (c : (derivedRestrict iU).obj A ≅ (derivedRestrict iV).obj B) :
    Nonempty (Glueing jU jV iU iV h.w A B c)

Stacks.Cohomology.GlueingComplexes.exists_hom_of_compatible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/GlueingComplexes/TwoOpens.lean, line 1441. The attribute's comment: “a compatible pair of maps comes from the glued object”.

Stacks Project, Tag 08DG. Let X be a ringed space covered by the images of two open immersions jU : U ⟶ X and jV : V ⟶ X, let W be their intersection, and let F be a glueing of the glueing data (A, B, c), with identifications f : F|_U ≅ A and g : F|_V ≅ B. Let E be an object of D(𝒪_X) and let a : A ⟶ E|_U and b : B ⟶ E|_V agree on W through c. Then there is a morphism F ⟶ E restricting to a ∘ f on U and to b ∘ g on V.

Unlike the existence of the glued object, this needs U and V to cover X: it is Mayer--Vietoris for Hom, and the covering hypothesis enters only through isIso_of_restrict_isIso.

theorem exists_hom_of_compatible {X U V W : RingedSpace.{u, u}} (jU : U ⟶ X) (jV : V ⟶ X)
    (iU : W ⟶ U) (iV : W ⟶ V) [SheafedSpace.IsOpenImmersion jU]
    [SheafedSpace.IsOpenImmersion jV] (h : IsPullback iU iV jU jV)
    (cover : Set.range jU.hom.base ∪ Set.range jV.hom.base = Set.univ)
    {A : DerivedModules U} {B : DerivedModules V}
    {c : (derivedRestrict iU).obj A ≅ (derivedRestrict iV).obj B}
    (G : Glueing jU jV iU iV h.w A B c) (E : DerivedModules X)
    (a : A ⟶ (derivedRestrict jU).obj E) (b : B ⟶ (derivedRestrict jV).obj E)
    (hab : (derivedRestrict iU).map a ≫ (overlapIso jU jV iU iV h.w).hom.app E =
      c.hom ≫ (derivedRestrict iV).map b) :
    ∃ φ : G.F ⟶ E, (derivedRestrict jU).map φ = G.f.hom ≫ a ∧
      (derivedRestrict jV).map φ = G.g.hom ≫ b

Tag 0D66, a lemma

Tag 0D66 in the Stacks Project.

Stacks.Cohomology.UnboundedHigherDirectImage.isZero_homologyDerivedPushforward_of_isBasis, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/ConnectivityOnABasis.lean, line 105. The attribute's comment: “negative_sheaves”.

Vanishing of the cohomology sheaves of Rf_* K. If the degree-i hypercohomology H^i(f⁻¹ V, K) vanishes for every V in a basis of the topology of Y, then the degree-i cohomology sheaf of Rf_* K vanishes.

theorem isZero_homologyDerivedPushforward_of_isBasis (i : ℤ)
    (hK : ∀ V ∈ B, IsZero ((DerivedCategory.homologyFunctor
      (ModuleCat.{u} ((structureSheafRing Y).obj.obj (op V))) i).obj
        ((derivedPreimageSections f V).obj K))) :
    IsZero ((DerivedCategory.homologyFunctor (SheafOfModules.{u} (structureSheafRing Y)) i).obj
      ((derivedPushforward f).obj K))

Stacks.Cohomology.UnboundedHigherDirectImage.isZero_homologyDerivedPreimageSections_of_isBasis, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/ConnectivityOnABasis.lean, line 120. The attribute's comment: “negative_hypercohomology”.

Negative hypercohomology over every inverse image. If H^i(f⁻¹ V, K) = 0 for i < 0 and every V in a basis of the topology of Y, then H^i(f⁻¹ V, K) = 0 for i < 0 and every open V ⊆ Y.

theorem isZero_homologyDerivedPreimageSections_of_isBasis
    (hK : ∀ V ∈ B, ∀ i : ℤ, i < 0 → IsZero ((DerivedCategory.homologyFunctor
      (ModuleCat.{u} ((structureSheafRing Y).obj.obj (op V))) i).obj
        ((derivedPreimageSections f V).obj K)))
    (V : Opens Y.carrier) (i : ℤ) (hi : i < 0) :
    IsZero ((DerivedCategory.homologyFunctor
      (ModuleCat.{u} ((structureSheafRing Y).obj.obj (op V))) i).obj
        ((derivedPreimageSections f V).obj K))

Stacks.Cohomology.UnboundedHigherDirectImage.isSheaf_zerothDerivedPreimageCohomologyPresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/ConnectivityOnABasis.lean, line 139. The attribute's comment: “zeroth_sheaf”.

The rule V ↦ H^0(f⁻¹ V, K) is a sheaf. If H^i(f⁻¹ V, K) = 0 for i < 0 and every V in a basis of the topology of Y, then the presheaf of 𝒪_Y-modules V ↦ H^0(f⁻¹ V, K) — that is derivedPreimageCohomologyPresheaf f K 0, whose values are identified with H^0(f⁻¹ V, K) by preimageCohomologyEvaluationIso — satisfies the sheaf condition.

theorem isSheaf_zerothDerivedPreimageCohomologyPresheaf
    (hK : ∀ V ∈ B, ∀ i : ℤ, i < 0 → IsZero ((DerivedCategory.homologyFunctor
      (ModuleCat.{u} ((structureSheafRing Y).obj.obj (op V))) i).obj
        ((derivedPreimageSections f V).obj K))) :
    Presheaf.IsSheaf (Opens.grothendieckTopology Y.carrier)
      (derivedPreimageCohomologyPresheaf f K 0).presheaf

Stacks.Cohomology.UnboundedHigherDirectImage.subsingleton_shiftedHom_preimageRestrict_of_isBasis, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/ConnectivityOnABasis.lean, line 268. The attribute's comment: “hom_negative_ext”.

Negative Ext over every inverse image. If Ext^i(K|_{f⁻¹ V}, L|_{f⁻¹ V}) = 0 for i < 0 and every V in a basis of the topology of Y, then the same vanishing holds for i < 0 and every open V ⊆ Y.

theorem subsingleton_shiftedHom_preimageRestrict_of_isBasis
    (hExt : ∀ V ∈ B, ∀ i : ℤ, i < 0 →
      Subsingleton (ShiftedHom ((preimageRestrict f V).obj K)
        ((preimageRestrict f V).obj L) i))
    (V : Opens Y.carrier) (i : ℤ) (hi : i < 0) :
    Subsingleton (ShiftedHom ((preimageRestrict f V).obj K)
      ((preimageRestrict f V).obj L) i)

Stacks.Cohomology.UnboundedHigherDirectImage.isSheaf_derivedPreimageHomPresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/ConnectivityOnABasis.lean, line 289. The attribute's comment: “hom_sheaf”.

The rule V ↦ Hom(K|_{f⁻¹ V}, L|_{f⁻¹ V}) is a sheaf. If Ext^i(K|_{f⁻¹ V}, L|_{f⁻¹ V}) = 0 for i < 0 and every V in a basis of the topology of Y, then the presheaf of 𝒪_Y-modules V ↦ Hom(K|_{f⁻¹ V}, L|_{f⁻¹ V}) satisfies the sheaf condition. Here the presheaf is derivedPreimageCohomologyPresheaf f (RSheafHom(K, L)) 0, whose value on V is identified with Hom(K|_{f⁻¹ V}, L|_{f⁻¹ V}) by derivedPreimageHomPresheafValueEquiv.

theorem isSheaf_derivedPreimageHomPresheaf
    (hExt : ∀ V ∈ B, ∀ i : ℤ, i < 0 →
      Subsingleton (ShiftedHom ((preimageRestrict f V).obj K)
        ((preimageRestrict f V).obj L) i)) :
    Presheaf.IsSheaf (Opens.grothendieckTopology Y.carrier)
      (derivedPreimageCohomologyPresheaf f (homSheafObject X.sheaf K L) 0).presheaf

Tag 0D67, a situation

Tag 0D67 in the Stacks Project.

Stacks.DerivedGlueing.LocallyGiven, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedCategory/LocallyGivenObjects.lean, line 120.

A system of locally given derived objects on a ringed space.

The restrictionComp field is the canonical identification between direct restriction and restriction in two steps. With this identification inserted, cocycle says exactly ρ W U = ρ W V ∘ (ρ V U)|_W.

structure LocallyGiven (X : RingedSpace.{u})

Tag 0D68, a lemma

Tag 0D68 in the Stacks Project.

Stacks.DerivedGlueing.subsingleton_shiftedHom_self_of_covers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedCategory/SelfExtOnACollectionOfOpens.lean, line 494. The attribute's comment: “the vanishing of negative self-Ext, for an arbitrary object K of D(𝒪_X) and an arbitrary collection of opens covering X with intersections covered by members, such that K|_U has no negative self-Ext for every member U”.

Stacks 0D68, the vanishing of negative self-Ext. Let (X, 𝒪_X) be a ringed space and let ℬ be a collection of open subsets covering X such that the intersection of two members of ℬ is the union of the members of ℬ contained in it. If K is an object of D(𝒪_X) with Ext^i(K|_U, K|_U) = 0 for i < 0 and every U ∈ ℬ, then Ext^i(K, K) = 0 for i < 0.

The members of ℬ need not form a basis; by Tag 0D5Q there is a continuous f : X → Y whose images of the members of ℬ do form a basis of Y and satisfy f⁻¹(f(U)) = U, and Tag 0D66 part (2) applied to f with 𝒪_Y = f_* 𝒪_X gives the vanishing over every open of Y, including ⊤.

Here K is an arbitrary object of D(𝒪_X) and ℬ an arbitrary collection; Stacks.DerivedGlueing.Solution.subsingleton_shiftedHom_self is this statement applied to the global object of a Stacks.DerivedGlueing.Solution of a system of locally given objects.

theorem subsingleton_shiftedHom_self_of_covers {X : RingedSpace.{u, u}}
    (ℬ : Set (Opens X.carrier)) (hcover : sSup ℬ = ⊤)
    (hinter : ∀ U ∈ ℬ, ∀ V ∈ ℬ, U ⊓ V = sSup {W | W ∈ ℬ ∧ W ≤ U ⊓ V})
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (hExt : ∀ U ∈ ℬ, ∀ i : ℤ, i < 0 → Subsingleton (ShiftedHom
      ((SheafOfModules.overFunctor.{u} (structureSheafRing X) U).mapDerivedCategory.obj K)
      ((SheafOfModules.overFunctor.{u} (structureSheafRing X) U).mapDerivedCategory.obj K) i))
    (i : ℤ) (hi : i < 0) :
    Subsingleton (ShiftedHom K K i)

Stacks.DerivedGlueing.Solution.subsingleton_shiftedHom_self, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedCategory/SelfExtOnACollectionOfOpens.lean, line 652. The attribute's comment: “the vanishing of negative self-Ext of the global object of a solution”.

Stacks 0D68, the vanishing of negative self-Ext. In Situation 0D67, suppose that the displayed opens cover X and that the intersection of two of them is the union of the members of the collection it contains, and that the prescribed local objects have no negative self-Ext. Then the global object of a solution has no negative self-Ext either.

The restrictions of the global object are the prescribed local objects, by Stacks.DerivedGlueing.Solution.restrictionIso, so this is Stacks.DerivedGlueing.subsingleton_shiftedHom_self_of_covers read through the equivalences comparing the models of restriction of modules to an open.

theorem Solution.subsingleton_shiftedHom_self {S : LocallyGiven X} (A : Solution S)
    (hcover : sSup S.opens = ⊤)
    (hinter : ∀ U ∈ S.opens, ∀ V ∈ S.opens, U ⊓ V = sSup {W | W ∈ S.opens ∧ W ≤ U ⊓ V})
    (hExt : ∀ (U : Opens X.carrier) (hU : U ∈ S.opens), ∀ i : ℤ, i < 0 →
      Subsingleton (ShiftedHom (S.obj U hU) (S.obj U hU) i))
    (i : ℤ) (hi : i < 0) :
    Subsingleton (ShiftedHom A.obj A.obj i)

Stacks.DerivedGlueing.exists_unique_solutionIso_of_covers_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedCategory/UniquenessOfASolutionUnconditional.lean, line 146. The attribute's comment: “the uniqueness of a solution up to unique isomorphism, under the tag's conditions (1) and (2); the vanishing of negative self-Ext is subsingleton_shiftedHom_self_of_covers and Solution.subsingleton_shiftedHom_self”.

The uniqueness clause of [Stacks, Tag 0D68]: in Situation 0D67, if the displayed opens cover X, if the intersection of two of them is the union of the members of the collection it contains, and if the prescribed local objects have no negative self-Ext, then any two solutions are identified by exactly one isomorphism of solutions.

The three conditions are (1) and (2) of the tag, as in Stacks.DerivedGlueing.Solution.subsingleton_shiftedHom_self, the tag's other clause. The proof applies Stacks.DerivedGlueing.exists_unique_solutionIso_of_covers_of_coherence, its coherence input being Stacks.DerivedGlueing.restrictHomBelow_eq_restrictDerivedHom.

The conclusion Stacks.DerivedGlueing.Solution.IsCompatibleHom A B ψ.hom is by definition ∀ (U : Opens X.carrier) (hU : U ∈ S.opens), (S.restriction U ⊤ le\_top).map ψ.hom ≫ (B.rho U hU).hom = (A.rho U hU).hom, which is the clause as the source states it.

theorem exists_unique_solutionIso_of_covers_unconditional (S : LocallyGiven X)
    (hcover : sSup S.opens = ⊤)
    (hinter : ∀ U ∈ S.opens, ∀ V ∈ S.opens, U ⊓ V = sSup {W | W ∈ S.opens ∧ W ≤ U ⊓ V})
    (hExt : ∀ (U : Opens X.carrier) (hU : U ∈ S.opens), ∀ i : ℤ, i < 0 →
      Subsingleton (ShiftedHom (S.obj U hU) (S.obj U hU) i))
    (A B : Solution S) :
    ∃! ψ : A.obj ≅ B.obj, A.IsCompatibleHom B ψ.hom

Tag 0D69, a remark

Tag 0D69 in the Stacks Project.

Stacks.DerivedGlueing.exists_unique_overlapIso_of_covers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedCategory/HomVanishingOverASubcollection.lean, line 457. The attribute's comment: “the comparison isomorphism over an overlap: for U, V ∈ ℬ a unique isomorphism K_U|_{U ⊓ V} ≅ K_V|_{U ⊓ V} compatible with the prescribed transitions on the members of ℬ contained in U ⊓ V, for a collection satisfying hinter (condition (1) of 0D68) and hExt (condition (2) of 0D68)”.

The comparison isomorphism over an overlap. For members U and V of the collection there is a unique isomorphism ρ_{U,V} : K_U|_{U ∩ V} ≅ K_V|_{U ∩ V} compatible with the prescribed transitions on the members contained in U ∩ V. Here hinter is hypothesis (1) of [Stacks, Tag 0D68] and hExt is its hypothesis (2); the collection need not cover X.

theorem exists_unique_overlapIso_of_covers (S : LocallyGiven X)
    (hinter : ∀ U ∈ S.opens, ∀ V ∈ S.opens, U ⊓ V = sSup {W | W ∈ S.opens ∧ W ≤ U ⊓ V})
    (hExt : ∀ (U : Opens X.carrier) (hU : U ∈ S.opens), ∀ i : ℤ, i < 0 →
      Subsingleton (ShiftedHom (S.obj U hU) (S.obj U hU) i))
    (U V : Opens X.carrier) (hU : U ∈ S.opens) (hV : V ∈ S.opens) :
    ∃! φ : (S.restriction (U ⊓ V) U inf_le_left).obj (S.obj U hU) ≅
        (S.restriction (U ⊓ V) V inf_le_right).obj (S.obj V hV),
      IsOverlapHom S hU hV inf_le_left inf_le_right φ.hom

Stacks.DerivedGlueing.restrictOverlapHom_cocycle_of_covers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedCategory/HomVanishingOverASubcollection.lean, line 477. The attribute's comment: “the cocycle condition ρ_{U,W} = ρ_{V,W} ∘ ρ_{U,V} over a triple intersection, for any three compatible isomorphisms over the three overlaps -- which by exists_unique_overlapIso_of_covers are the source's own ρ_{U,V}, ρ_{V,W} and ρ_{U,W}, being the unique compatible ones -- for a collection satisfying hinter (condition (1) of 0D68) and hExt (condition (2) of 0D68)”.

The cocycle condition over a triple intersection. For members U, V and W and compatible isomorphisms over the three overlaps, ρ_{U,W} = ρ_{V,W} ∘ ρ_{U,V} over U ∩ V ∩ W. By Stacks.DerivedGlueing.exists_unique_overlapIso_of_covers the compatible isomorphisms over the overlaps are unique.

theorem restrictOverlapHom_cocycle_of_covers (S : LocallyGiven X)
    (hinter : ∀ U ∈ S.opens, ∀ V ∈ S.opens, U ⊓ V = sSup {W | W ∈ S.opens ∧ W ≤ U ⊓ V})
    (hExt : ∀ (U : Opens X.carrier) (hU : U ∈ S.opens), ∀ i : ℤ, i < 0 →
      Subsingleton (ShiftedHom (S.obj U hU) (S.obj U hU) i))
    (U V W : Opens X.carrier) (hU : U ∈ S.opens) (hV : V ∈ S.opens) (hW : W ∈ S.opens)
    (φUV : (S.restriction (U ⊓ V) U inf_le_left).obj (S.obj U hU) ≅
      (S.restriction (U ⊓ V) V inf_le_right).obj (S.obj V hV))
    (hφUV : IsOverlapHom S hU hV inf_le_left inf_le_right φUV.hom)
    (φVW : (S.restriction (V ⊓ W) V inf_le_left).obj (S.obj V hV) ≅
      (S.restriction (V ⊓ W) W inf_le_right).obj (S.obj W hW))
    (hφVW : IsOverlapHom S hV hW inf_le_left inf_le_right φVW.hom)
    (φUW : (S.restriction (U ⊓ W) U inf_le_left).obj (S.obj U hU) ≅
      (S.restriction (U ⊓ W) W inf_le_right).obj (S.obj W hW))
    (hφUW : IsOverlapHom S hU hW inf_le_left inf_le_right φUW.hom) :
    restrictOverlapHom S hU hW inf_le_left inf_le_right
        (le_inf (inf_le_left.trans inf_le_left) inf_le_right : U ⊓ V ⊓ W ≤ U ⊓ W) φUW.hom =
      restrictOverlapHom S hU hV inf_le_left inf_le_right
          (inf_le_left : U ⊓ V ⊓ W ≤ U ⊓ V) φUV.hom ≫
        restrictOverlapHom S hV hW inf_le_left inf_le_right
          (le_inf (inf_le_left.trans inf_le_right) inf_le_right : U ⊓ V ⊓ W ≤ V ⊓ W) φVW.hom

Stacks.DerivedGlueing.restrictedSystemOverInf_covers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedCategory/OverlapRestrictedSystem.lean, line 99. The attribute's comment: “the restricted system covers the overlap: condition (1) of 0D68 for the subsystem on the members contained in U ⊓ V, from the condition that the intersection of two members is the union of the members contained in it”.

[Stacks, Tag 0D69], the restricted system covers the overlap. The overlap of two members is the union of the members of the restricted collection contained in it — which is condition (1) of [Stacks, Tag 0D68] for the restricted system, read at U ⊓ V. It is the condition that intersections of members are unions of members, read at the pair U, V.

theorem restrictedSystemOverInf_covers (S : LocallyGiven X)
    (hinter : ∀ U ∈ S.opens, ∀ V ∈ S.opens, U ⊓ V = sSup {W | W ∈ S.opens ∧ W ≤ U ⊓ V})
    (U V : Opens X.carrier) (hU : U ∈ S.opens) (hV : V ∈ S.opens) :
    U ⊓ V = sSup {W | W ∈ (restrictedSystemOverInf S U V).opens ∧ W ≤ U ⊓ V}

Stacks.DerivedGlueing.restrictedSystemOverInf_intersections_covered, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedCategory/OverlapRestrictedSystem.lean, line 114. The attribute's comment: “the restricted system's intersection condition: condition (1) of 0D68 for the subsystem on the members contained in U ⊓ V, at an arbitrary pair of its members”.

[Stacks, Tag 0D69], the restricted system's intersection condition. The intersection of two members of the restricted collection is the union of the members of the restricted collection contained in it — condition (1) of [Stacks, Tag 0D68] for the restricted system, at an arbitrary pair of its members.

The members of the restricted collection contained in A ⊓ B are exactly the members of the whole collection contained in it, because A ⊓ B ≤ A ≤ U ⊓ V.

theorem restrictedSystemOverInf_intersections_covered (S : LocallyGiven X)
    (hinter : ∀ U ∈ S.opens, ∀ V ∈ S.opens, U ⊓ V = sSup {W | W ∈ S.opens ∧ W ≤ U ⊓ V})
    (U V : Opens X.carrier) :
    ∀ A ∈ (restrictedSystemOverInf S U V).opens, ∀ B ∈ (restrictedSystemOverInf S U V).opens,
      A ⊓ B = sSup {W | W ∈ (restrictedSystemOverInf S U V).opens ∧ W ≤ A ⊓ B}

Stacks.DerivedGlueing.restrictedSystemOverInf_ext, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedCategory/OverlapRestrictedSystem.lean, line 129. The attribute's comment: “the restricted system's Ext condition: condition (2) of 0D68 for the subsystem on the members contained in U ⊓ V, from the vanishing of negative self-Ext of the prescribed objects”.

[Stacks, Tag 0D69], the restricted system's Ext condition. The prescribed objects of the restricted system have no negative self-Ext, since they are prescribed objects of the whole system — condition (2) of [Stacks, Tag 0D68] for the restricted system.

theorem restrictedSystemOverInf_ext (S : LocallyGiven X)
    (hExt : ∀ (W : Opens X.carrier) (hW : W ∈ S.opens), ∀ i : ℤ, i < 0 →
      Subsingleton (ShiftedHom (S.obj W hW) (S.obj W hW) i))
    (U V : Opens X.carrier) :
    ∀ (W : Opens X.carrier) (hW : W ∈ (restrictedSystemOverInf S U V).opens), ∀ i : ℤ, i < 0 →
      Subsingleton (ShiftedHom ((restrictedSystemOverInf S U V).obj W hW)
        ((restrictedSystemOverInf S U V).obj W hW) i)

Stacks.DerivedGlueing.exists_solutionOver_inf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedCategory/OverlapRestrictedSystem.lean, line 149. The attribute's comment: “the two restricted objects are solutions over the overlap: K_U|_{U ∩ V} and K_V|_{U ∩ V} are each a solution for the system over U ∩ V, for every U, V ∈ ℬ”.

[Stacks, Tag 0D69], both restrictions are solutions over the overlap. The prescribed object on a member is a solution over that member, Stacks.DerivedGlueing.selfSolutionOver, and a solution over an open restricts to a solution over a smaller one, Stacks.DerivedGlueing.SolutionOver.restrictOpen. So K_U|_{U ∩ V} and K_V|_{U ∩ V} are each a solution for the system over U ∩ V, and these are the two solutions the source feeds to the uniqueness clause of [Stacks, Tag 0D68]. This holds for all U, V ∈ ℬ.

theorem exists_solutionOver_inf (S : LocallyGiven X) (U V : Opens X.carrier)
    (hU : U ∈ S.opens) (hV : V ∈ S.opens) :
    (∃ A : SolutionOver S (U ⊓ V),
        A.obj = (S.restriction (U ⊓ V) U inf_le_left).obj (S.obj U hU)) ∧
      ∃ B : SolutionOver S (U ⊓ V),
        B.obj = (S.restriction (U ⊓ V) V inf_le_right).obj (S.obj V hV)

Tag 0D6A, a lemma

Tag 0D6A in the Stacks Project.

Stacks.DerivedGlueing.exists_solution_of_finite_cover_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedCategory/GlueingForHomsWithoutCovering.lean, line 113. The attribute's comment: “existence: for X = U_1 ∪ … ∪ U_n with U_i in the collection, intersections of members covered by members, and no negative self-Ext of the prescribed objects, the system has a solution”.

[Stacks, Tag 0D6A], existence. In Situation 0D67, suppose that X = U_1 ∪ … ∪ U_n with the U_i in the displayed collection, that the intersection of two members of the collection is the union of the members contained in it, and that the prescribed objects have no negative self-Ext. Then the system has a solution.

The proof applies Stacks.DerivedGlueing.exists_solution_of_finite_cover_of_homs; the sheaf condition of [Stacks, Tag 0D66] part (2) for every subsystem is Stacks.DerivedGlueing.hasGluingForHomsOver_of_covers, a theorem with no binder beyond the system. The nonemptiness hs of the cover is used here: the induction of Stacks.DerivedGlueing.exists_solutionOver_finsetSup runs on Finset.Nonempty.cons_induction and starts from a single member.

theorem exists_solution_of_finite_cover_unconditional (S : LocallyGiven X)
    (s : Finset (Opens X.carrier)) (hs : s.Nonempty) (hmem : ∀ U ∈ s, U ∈ S.opens)
    (hcover : s.sup id = ⊤)
    (hinter : ∀ U ∈ S.opens, ∀ V ∈ S.opens, U ⊓ V = sSup {W | W ∈ S.opens ∧ W ≤ U ⊓ V})
    (hExt : ∀ (U : Opens X.carrier) (hU : U ∈ S.opens), ∀ i : ℤ, i < 0 →
      Subsingleton (ShiftedHom (S.obj U hU) (S.obj U hU) i)) :
    Nonempty (Solution S)

Stacks.DerivedGlueing.exists_solution_and_unique_solutionIso_of_finite_cover_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedCategory/GlueingForHomsWithoutCovering.lean, line 137. The attribute's comment: “the whole tag: for X = U_1 ∪ … ∪ U_n with U_i in the collection, intersections of members covered by members, and no negative self-Ext of the prescribed objects, a solution exists and is unique up to unique isomorphism”.

[Stacks, Tag 0D6A] in full: under the conditions (1), (2) and (3) of the tag the system has a solution, and any two solutions are identified by exactly one isomorphism of solutions.

Both clauses of the tag in one statement, the existence clause above together with the uniqueness clause of [Stacks, Tag 0D68] over the finite cover. The conclusion Stacks.DerivedGlueing.Solution.IsCompatibleHom A B ψ.hom is by definition ∀ (U : Opens X.carrier) (hU : U ∈ S.opens), (S.restriction U ⊤ le\_top).map ψ.hom ≫ (B.rho U hU).hom = (A.rho U hU).hom, which is "compatible with the ρ\_U" as the source means it.

theorem exists_solution_and_unique_solutionIso_of_finite_cover_unconditional (S : LocallyGiven X)
    (s : Finset (Opens X.carrier)) (hs : s.Nonempty) (hmem : ∀ U ∈ s, U ∈ S.opens)
    (hcover : s.sup id = ⊤)
    (hinter : ∀ U ∈ S.opens, ∀ V ∈ S.opens, U ⊓ V = sSup {W | W ∈ S.opens ∧ W ≤ U ⊓ V})
    (hExt : ∀ (U : Opens X.carrier) (hU : U ∈ S.opens), ∀ i : ℤ, i < 0 →
      Subsingleton (ShiftedHom (S.obj U hU) (S.obj U hU) i)) :
    Nonempty (Solution S) ∧
      ∀ A B : Solution S, ∃! ψ : A.obj ≅ B.obj, A.IsCompatibleHom B ψ.hom

Stacks.DerivedGlueing.exists_solution_of_top_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedCategory/GlueingOverAFiniteCover.lean, line 290. The attribute's comment: “existence when a single member of the collection is all of X”.

[Stacks, Tag 0D6A] when the cover has a single member. If the whole of X belongs to the collection, then the system has a solution: the prescribed object on ⊤ is one.

This is the case n = 1 of the tag.

theorem exists_solution_of_top_mem (S : LocallyGiven X) (htop : ⊤ ∈ S.opens) :
    Nonempty (Solution S)

Stacks.DerivedGlueing.exists_unique_solutionIso_of_top_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedCategory/UniquenessOverACover.lean, line 172. The attribute's comment: “uniqueness up to unique isomorphism when a single member of the collection is all of X, the case n = 1”.

[Stacks, Tag 0D6A] when the cover has a single member: uniqueness up to unique isomorphism. If the whole of X belongs to the collection, then any two solutions are identified by exactly one isomorphism of solutions.

This is the case n = 1 of the tag: restriction from ⊤ to ⊤ is the identity functor, by Stacks.DerivedGlueing.restrictionSelfIso, so the identifications over ⊤ of the two solutions compose to the required isomorphism and determine it; and compatibility over ⊤ forces compatibility over every member, by Stacks.DerivedGlueing.Solution.isCompatibleHom_of_top.

Together with Stacks.DerivedGlueing.exists_solution_of_top_mem this is the whole of Tag 0D6A for n = 1.

theorem exists_unique_solutionIso_of_top_mem (S : LocallyGiven X) (htop : ⊤ ∈ S.opens)
    (A B : Solution S) :
    ∃! φ : A.obj ≅ B.obj, A.IsCompatibleHom B φ.hom

Tag 0D6B, a lemma

Tag 0D6B in the Stacks Project.

Stacks.DerivedGlueing.exists_glueing_of_wellOrderedCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedCategory/WellOrderedCoverRecursion.lean, line 1180. The attribute's comment: “the glued object G over ⊤ with identifications sigma α of its restrictions with the K α, compatible with the prescribed ρ^α_β for every β < α, for a well ordered covering with hsucc (W_α ⊆ W_{α+1}), hlimit (continuity at the stages that are not successors), hcover, hExt (no negative self-Ext) and the cocycle condition hcocycle”.

[Stacks, Tag 0D6B]. Let X be a ringed space, let E be a well ordered set and let X = ⋃_{α ∈ E} W_α be an open covering with W_α ⊆ W_{α+1} and W_α = ⋃_{β < α} W_β when α is not a successor. Let K_α be an object of D(𝒪_{W_α}) with Ext^i(K_α, K_α) = 0 for i < 0, and let ρ^α_β : K_α|_{W_β} ≅ K_β for β < α satisfy ρ^α_γ = ρ^β_γ ∘ ρ^α_β|_{W_γ} for γ < β < α. Then there is an object K of D(𝒪_X) and isomorphisms K|_{W_α} ≅ K_α compatible with the ρ^α_β.

"β is the immediate predecessor of α" is rendered as "β < α and every γ < α satisfies γ ≤ β", so hsucc is the inclusion W_α ⊆ W_{α+1} and hlimit the continuity at the stages that are not successors; Stacks.DerivedGlueing.le_of_succ_of_limit derives from them the inclusion W_β ⊆ W_α for every β < α along which the transitions are stated.

The system S : Stacks.DerivedGlueing.LocallyGiven X (the structure of StacksFrontier/Topology/Sheaves/Cohomology/DerivedCategory/LocallyGivenObjects.lean, not RingedSite.LocallyGiven) is exactly Situation 0D67 and carries no further data: its restriction functors S.restriction V U are the canonical derived restrictions j^* along the inclusions V ⊆ U, since the field restrictionFactors identifies each with the derived functor of the restriction of complexes openModuleRestriction through the localization, and its comparisons S.restrictionComp are the canonical ones, by the field restrictionCompFactors.

theorem exists_glueing_of_wellOrderedCover (S : Stacks.DerivedGlueing.LocallyGiven X)
    (E : Type v) [LinearOrder E] [WellFoundedLT E]
    (W : E → Opens X.carrier)
    (hsucc : ∀ β α : E, β < α → (∀ γ : E, γ < α → γ ≤ β) → W β ≤ W α)
    (hlimit : ∀ α : E, (¬ ∃ β : E, β < α ∧ ∀ γ : E, γ < α → γ ≤ β) →
      W α = ⨆ (β : E) (_ : β < α), W β)
    (hcover : (⨆ α : E, W α) = ⊤) (K : ∀ α : E, OpenDerivedCategory X (W α))
    (hExt : ∀ (α : E) (i : ℤ), i < 0 → Subsingleton (ShiftedHom (K α) (K α) i))
    (rho : ∀ (β α : E) (h : β < α),
      (S.restriction (W β) (W α) (le_of_succ_of_limit W hsucc hlimit β α h)).obj (K α) ≅ K β)
    (hcocycle : ∀ (γ β α : E) (hγβ : γ < β) (hβα : β < α),
      (rho γ α (hγβ.trans hβα)).hom =
        (S.restrictionComp (W γ) (W β) (W α) (le_of_succ_of_limit W hsucc hlimit γ β hγβ)
            (le_of_succ_of_limit W hsucc hlimit β α hβα)).hom.app (K α) ≫
          (S.restriction (W γ) (W β)
            (le_of_succ_of_limit W hsucc hlimit γ β hγβ)).map (rho β α hβα).hom ≫
            (rho γ β hγβ).hom) :
    ∃ (G : OpenDerivedCategory X ⊤)
      (sigma : ∀ α : E, (S.restriction (W α) ⊤ le_top).obj G ≅ K α),
      ∀ (β α : E) (h : β < α),
        (S.restrictionComp (W β) (W α) ⊤
              (le_of_succ_of_limit W hsucc hlimit β α h) le_top).hom.app G ≫
            (S.restriction (W β) (W α)
              (le_of_succ_of_limit W hsucc hlimit β α h)).map (sigma α).hom ≫ (rho β α h).hom =
          (sigma β).hom

Tag 0D6C, a theorem

Tag 0D6C in the Stacks Project.

Stacks.DerivedGlueing.exists_solution_and_unique_solutionIso_of_covers_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedCategory/BBDGlueing.lean, line 433. The attribute's comment: “existence of a solution (K, ρ_U) and its uniqueness up to unique isomorphism, for a collection satisfying (1) hcover, (2) hinter and (3) hExt”.

[Stacks, Tag 0D6C] (BBD gluing lemma). In Situation 0D67 suppose that the members of the collection cover X, that for two members U, V the intersection U ∩ V is the union of the members contained in it, and that Ext^i(K_U, K_U) = 0 for i < 0 and every member U. Then the system has a solution, and any two solutions are identified by exactly one isomorphism of solutions.

A solution is a Stacks.DerivedGlueing.Solution: an object K of D(𝒪_X) with isomorphisms ρ_U : K|_U ≅ K_U satisfying ρ^U_V ∘ ρ_U|_V = ρ_V. The conclusion Stacks.DerivedGlueing.Solution.IsCompatibleHom A B ψ.hom says that ψ is compatible with the ρ_U of the two solutions.

theorem exists_solution_and_unique_solutionIso_of_covers_unconditional (S : LocallyGiven X)
    (hcover : sSup S.opens = ⊤)
    (hinter : ∀ U ∈ S.opens, ∀ V ∈ S.opens, U ⊓ V = sSup {W | W ∈ S.opens ∧ W ≤ U ⊓ V})
    (hExt : ∀ (U : Opens X.carrier) (hU : U ∈ S.opens), ∀ i : ℤ, i < 0 →
      Subsingleton (ShiftedHom (S.obj U hU) (S.obj U hU) i)) :
    Nonempty (Solution S) ∧
      ∀ A B : Solution S, ∃! ψ : A.obj ≅ B.obj, A.IsCompatibleHom B ψ.hom

Sources

• Section 20.45, Tag 0D65
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Cohomology.GlueingComplexes.exists_glueing · Stacks.Cohomology.GlueingComplexes.exists_hom_of_compatible · Stacks.Cohomology.UnboundedHigherDirectImage.isZero_homologyDerivedPushforward_of_isBasis · Stacks.Cohomology.UnboundedHigherDirectImage.isZero_homologyDerivedPreimageSections_of_isBasis · Stacks.Cohomology.UnboundedHigherDirectImage.isSheaf_zerothDerivedPreimageCohomologyPresheaf · Stacks.Cohomology.UnboundedHigherDirectImage.subsingleton_shiftedHom_preimageRestrict_of_isBasis · Stacks.Cohomology.UnboundedHigherDirectImage.isSheaf_derivedPreimageHomPresheaf · Stacks.DerivedGlueing.LocallyGiven

Section20.46 Strictly perfect complexes#

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

Tag 08C4, a definition

Tag 08C4 in the Stacks Project.

Declarations registered for the tag:

• StrictlyPerfect.IsStrictlyPerfect, declared in the repository, registered with add_to_stacks in StacksFrontier/Topology/Sheaves/Cohomology/StrictlyPerfect/Defs.lean, line 42 (StacksFrontier).

Tag 08C5, a lemma

Tag 08C5 in the Stacks Project.

StrictlyPerfect.isStrictlyPerfect_mappingCone, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/StrictlyPerfect/FiniteFreeSummands.lean, line 311.

The cone on a morphism of strictly perfect complexes is strictly perfect.

The cone C(f) is CochainComplex.mappingCone f, whose n-th term is L^n ⊕ K^{n+1}. The hypothesis HasHomotopyCofiber f is the (automatically satisfied, since the category has binary biproducts) condition ensuring the mapping cone exists.

theorem isStrictlyPerfect_mappingCone {K L : CochainComplex (OXMod.{u, w} X) ℤ}
    (f : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber f]
    (hK : IsStrictlyPerfect K) (hL : IsStrictlyPerfect L) :
    IsStrictlyPerfect (CochainComplex.mappingCone f)

Tag 09J2, a lemma

Tag 09J2 in the Stacks Project.

strictlyPerfect_tensorObj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/StrictlyPerfect/TensorOfFiniteFreeSummands.lean, line 250.

Stacks Tag 09J2 (Lemma 20.46.3). If E and F are strictly perfect complexes, then the total complex HomologicalComplex.tensorObj E F of their tensor product, whose degree n term is ⨁_{p+q=n} E^p ⊗ F^q with the Koszul-sign differential, is strictly perfect.

The hypothesis [E.HasTensor F] asserts that the total complex exists; for bounded complexes (such as strictly perfect ones) it is automatically satisfied since each total degree only involves finitely many summands.

theorem strictlyPerfect_tensorObj
    (E F : CochainComplex C ℤ) [E.HasTensor F]
    (hE : StrictlyPerfect E) (hF : StrictlyPerfect F) :
    StrictlyPerfect (HomologicalComplex.tensorObj E F)

Tag 09U6, a lemma

Tag 09U6 in the Stacks Project.

Stacks.Cohomology.StrictlyPerfectPullback.pullback_isStrictlyPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/StrictlyPerfectRestriction/PullbackOverASite.lean, line 142.

Stacks Tag 09U6, Lemma 20.46.4. Let f : (X, O_X) → (Y, O_Y) be a morphism of ringed spaces, with pullback functor f^* : Mod(O_Y) ⥤ Mod(O_X). If F^• is a strictly perfect complex of O_Y-modules, then f^* F^• (the termwise pullback of F^•) is a strictly perfect complex of O_X-modules.

theorem pullback_isStrictlyPerfect {X Y : AlgebraicGeometry.RingedSpace.{0, 0}} (f : X ⟶ Y)
    (F : HomologicalComplex (Modules Y) (ComplexShape.up ℤ))
    (hF : IsStrictlyPerfect F) :
    IsStrictlyPerfect
      (((_root_.pullback f).mapHomologicalComplex (ComplexShape.up ℤ)).obj F)

Tag 08C6, a lemma

Tag 08C6 in the Stacks Project.

StrictlyPerfect.exists_over_lift_of_isDirectSummandOfFiniteFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/StrictlyPerfectLiftModuleUniverse.lean, line 265. The attribute's comment: “at an arbitrary module universe”.

Stacks 08C6. Let X be a ringed space, p : 𝒢 ⟶ ℱ an epimorphism of 𝒪_X-modules and f : ℰ ⟶ ℱ a morphism out of a direct summand of a finite free 𝒪_X-module. Then every point of X has an open neighbourhood U and a morphism l : ℰ|_U ⟶ 𝒢|_U with l ≫ p|_U = f|_U.

The ring universe, the space universe and the module universe are independent; the price is the two sheafification hypotheses, which are what make Mod(𝒪_X) abelian and are Stacks' standing convention. See the module docstring for how the module universe is freed and for the two other carriers of this tag.

theorem exists_over_lift_of_isDirectSummandOfFiniteFree {E F G : OXMod.{u, w} X} (f : E ⟶ F)
    (p : G ⟶ F) [Epi p] (hE : IsDirectSummandOfFiniteFree E) :
    ∀ x : X.carrier, ∃ U : Opens X.carrier, x ∈ U ∧
      ∃ l : E.over U ⟶ G.over U, l ≫ p.over U = f.over U

StrictlyPerfect.exists_local_lift_of_isDirectSummandOfFiniteFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/StrictlyPerfectRestriction.lean, line 269. The attribute's comment: “module universe = ring universe, space universe free, stated through restrictModules. Strictly more general than the collapsed form in StacksFrontier/AlgebraicGeometry/PseudoCoherent/StrictlyPerfectLift.lean, strictly less than the arbitrary-module-universe form in StrictlyPerfectLiftModuleUniverse.lean.”.

Given α : E ⟶ F and an epimorphism p : G ⟶ F of O_X-modules with E a direct summand of a finite free O_X-module, a factorisation of α through p exists locally on X: every point has an open neighbourhood U and a morphism β : E|_U ⟶ G|_U with β ≫ p|_U = α|_U.

theorem exists_local_lift_of_isDirectSummandOfFiniteFree {E F G : OXMod.{r, r} X}
    (hE : IsDirectSummandOfFiniteFree E) (α : E ⟶ F) (p : G ⟶ F) [Epi p] (x : X.carrier) :
    ∃ U : Opens X.carrier, x ∈ U ∧
      ∃ β : (restrictModules X U).obj E ⟶ (restrictModules X U).obj G,
        β ≫ (restrictModules X U).map p = (restrictModules X U).map α

AlgebraicGeometry.RingedSpace.exists_local_lift_of_isDirectSummandOfFiniteFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/StrictlyPerfectLift.lean, line 216. The attribute's comment: “all three universes collapsed (space = ring = module), stated through restrictModules. The module-universe-free form is in StacksFrontier/Algebra/Homology/StrictlyPerfectLiftModuleUniverse.lean; neither subsumes the other.”.

Stacks 08C6. Let X be a ringed space, let p : 𝒢 ⟶ ℱ be an epimorphism of 𝒪_X-modules and let f : ℰ ⟶ ℱ be a map out of a direct summand of a finite free 𝒪_X-module. Then every point of X has an open neighbourhood over which f factors through p.

Writing ℰ as a retract (i, r) of 𝒪_X^{⊕ n}, it is enough to lift r ≫ f and compose the lift with i, since i ≫ r = 𝟙.

theorem exists_local_lift_of_isDirectSummandOfFiniteFree
    {E F G : StrictlyPerfect.OXMod.{u, u, u} X} (f : E ⟶ F) (p : G ⟶ F) [Epi p]
    (hE : StrictlyPerfect.IsDirectSummandOfFiniteFree E) :
    ∀ x : X.carrier, ∃ U : Opens X.carrier, x ∈ U ∧
      ∃ l : (restrictModules X U).obj E ⟶ (restrictModules X U).obj G,
        l ≫ (restrictModules X U).map p = (restrictModules X U).map f

StrictlyPerfect.LocalLifting.exists_local_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/StrictlyPerfect/LocalLiftingOfMaps.lean, line 141.

A map from a direct summand of a finite free module lifts locally through any epimorphism of sheaves of modules.

theorem exists_local_lift [Epi p] (hE : IsDirectSummandOfFiniteFree E) :
    ∀ x : X.carrier, ∃ U : Opens X.carrier, x ∈ U ∧
      ∃ l : E.over U ⟶ G.over U, l ≫ p.over U = f.over U

Tag 08C7, a lemma

Tag 08C7 in the Stacks Project.

AlgebraicGeometry.RingedSpace.exists_local_homotopy_zero_of_isZero_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/StrictlyPerfectRestriction/LocalNullHomotopyOverSlices.lean, line 82. The attribute's comment: “part (2)”. References: SGA 6 I (4.1), “ringed space”.

A map from a strictly perfect complex concentrated in degrees at least a is locally null-homotopic if the target's cohomology vanishes in those degrees.

This is the ringed-space-facing name for Stacks.Cohomology.LocalNullHomotopy.exists_local_homotopy_zero_of_isZero_homology, which carries the proof.

theorem exists_local_homotopy_zero_of_isZero_homology (a : ℤ)
    (hE : StrictlyPerfect.IsStrictlyPerfect E) (hE₀ : ∀ i : ℤ, i < a → IsZero (E.X i))
    (hF : ∀ i : ℤ, a ≤ i → IsZero (F.homology i)) :
    ∀ x : X.carrier, ∃ U : Opens X.carrier, x ∈ U ∧
      Nonempty (Homotopy
        (((SheafOfModules.overFunctor (structureSheafOfRings X) U).mapHomologicalComplex
          (ComplexShape.up ℤ)).map α) 0)

AlgebraicGeometry.RingedSpace.exists_local_homotopy_zero_of_acyclic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/StrictlyPerfectRestriction/LocalNullHomotopyOverSlices.lean, line 99. The attribute's comment: “part (1)”. References: SGA 6 I (4.1), “ringed space”.

A map from a strictly perfect complex to an acyclic complex is locally null-homotopic.

This is the ringed-space-facing name for Stacks.Cohomology.LocalNullHomotopy.exists_local_homotopy_zero_of_acyclic, which carries the proof.

theorem exists_local_homotopy_zero_of_acyclic
    (hE : StrictlyPerfect.IsStrictlyPerfect E) (hF : F.Acyclic) :
    ∀ x : X.carrier, ∃ U : Opens X.carrier, x ∈ U ∧
      Nonempty (Homotopy
        (((SheafOfModules.overFunctor (structureSheafOfRings X) U).mapHomologicalComplex
          (ComplexShape.up ℤ)).map α) 0)

Tag 08C8, a lemma

Tag 08C8 in the Stacks Project.

AlgebraicGeometry.RingedSpace.exists_local_lift_homotopy, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/StrictlyPerfectCone.lean, line 150. References: SGA 6 I (4.2), “ringed space case”.

Stacks 08C8. Let X be a ringed space, let α : ℰ ⟶ ℱ be a morphism of complexes of 𝒪_X-modules with ℰ strictly perfect and ℰ^j = 0 for j < a, and let f : 𝒢 ⟶ ℱ be a morphism of complexes of 𝒪_X-modules which is an isomorphism on cohomology in every degree above a and an epimorphism on cohomology in degree a. Then every point of X has an open neighbourhood U carrying a morphism β : ℰ|_U ⟶ 𝒢|_U with β ≫ f|_U homotopic to α|_U.

The mapping cone C(f) has vanishing cohomology in degrees at least a (AlgebraicGeometry.RingedSpace.isZero_homology_mappingCone), so Stacks 08C7 makes the composite α ≫ inr f null-homotopic over some open neighbourhood U of the given point. Hence α|_U composed with the second map of the distinguished triangle 𝒢|_U ⟶ ℱ|_U ⟶ C(f|_U) is zero in the homotopy category over U, and Triangle.coyoneda_exact₂ factors it through f|_U; any representative β of that factorization satisfies the conclusion.

public theorem exists_local_lift_homotopy
    {E F G : CochainComplex (OXMod.{u, u} X) ℤ} (α : E ⟶ F) (f : G ⟶ F) (a : ℤ)
    (hE : IsStrictlyPerfect E) (hEa : ∀ j : ℤ, j < a → IsZero (E.X j))
    (hf_gt : ∀ j : ℤ, a < j → IsIso (HomologicalComplex.homologyMap f j))
    (hf_a : Epi (HomologicalComplex.homologyMap f a)) :
    ∀ x : X.carrier, ∃ U : Opens X.carrier, x ∈ U ∧
      ∃ β : ((overFunctor (structureSheafOfRings X) U).mapHomologicalComplex
            (ComplexShape.up ℤ)).obj E ⟶
          ((overFunctor (structureSheafOfRings X) U).mapHomologicalComplex
            (ComplexShape.up ℤ)).obj G,
        Nonempty (Homotopy
          (β ≫ ((overFunctor (structureSheafOfRings X) U).mapHomologicalComplex
            (ComplexShape.up ℤ)).map f)
          (((overFunctor (structureSheafOfRings X) U).mapHomologicalComplex
            (ComplexShape.up ℤ)).map α))

Stacks.PseudoCoherence.DerivedCharacterization.exists_local_lift_homotopy, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PseudoCoherence/Defs.lean, line 138. References: SGA 6 I (4.2), “ringed space case”; SGA 6 I (4.1), “special case”.

A map from a strictly perfect complex lifts locally up to homotopy through a map that is cohomologically an isomorphism above the lower bound and surjective at the lower bound.

theorem exists_local_lift_homotopy (α : E ⟶ F) (f : G ⟶ F) (a : ℤ)
    (hE : IsStrictlyPerfect E) (hEa : ∀ j : ℤ, j < a → IsZero (E.X j))
    (hf_gt : ∀ j : ℤ, a < j → IsIso (HomologicalComplex.homologyMap f j))
    (hf_a : Epi (HomologicalComplex.homologyMap f a)) :
    ∀ x : X.carrier, ∃ U : Opens X.carrier, x ∈ U ∧
      ∃ β : ((overFunctor.{u} (structureSheafOfRings X) U).mapHomologicalComplex
            (ComplexShape.up ℤ)).obj E ⟶
          ((overFunctor.{u} (structureSheafOfRings X) U).mapHomologicalComplex
            (ComplexShape.up ℤ)).obj G,
        Nonempty (Homotopy
          (β ≫ ((overFunctor.{u} (structureSheafOfRings X) U).mapHomologicalComplex
            (ComplexShape.up ℤ)).map f)
          (((overFunctor.{u} (structureSheafOfRings X) U).mapHomologicalComplex
            (ComplexShape.up ℤ)).map α))

Tag 08C9, a lemma

Tag 08C9 in the Stacks Project.

AlgebraicGeometry.RingedSpace.exists_local_homotopy_zero_of_derived_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/StrictlyPerfectLocalRep.lean, line 338. The attribute's comment: “local_null_homotopy”. References: SGA 6 I (4.1), “special case”.

Stacks 08C9, part (2). Let α : ℰ ⟶ ℱ be a morphism of complexes of 𝒪_X-modules with ℰ strictly perfect whose image in the derived category of X is zero. Then every point of X has an open neighbourhood over which α is homotopic to zero.

The image of α in the derived category vanishes, so its image in the homotopy category is killed by a quasi-isomorphism t : 𝒵 ⟶ ℰ; that is, t ≫ α is null-homotopic. Stacks 08C8, applied to the identity of ℰ and to t, produces over some open neighbourhood U a map β : ℰ|_U ⟶ 𝒵|_U with β ≫ t|_U homotopic to the identity, and CochainComplex.nonempty_homotopy_zero_of_lift_homotopy_id concludes.

public theorem exists_local_homotopy_zero_of_derived_eq_zero
    [HasDerivedCategory.{d} (OXMod.{u, u} X)] {E F : CochainComplex (OXMod.{u, u} X) ℤ}
    (α : E ⟶ F) (hE : IsStrictlyPerfect E) (hα : DerivedCategory.Q.map α = 0) :
    ∀ x : X.carrier, ∃ U : Opens X.carrier, x ∈ U ∧
      Nonempty (Homotopy
        (((SheafOfModules.overFunctor (structureSheafOfRings X) U).mapHomologicalComplex
          (ComplexShape.up ℤ)).map α) 0)

AlgebraicGeometry.RingedSpace.exists_local_complex_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/StrictlyPerfectLocalRep.lean, line 433. The attribute's comment: “local_representation”.

Stacks 08C9, part (1). Let ℰ, ℱ be complexes of 𝒪_X-modules with ℰ strictly perfect and let α : ℰ ⟶ ℱ be a morphism in the derived category of X. Then every point of X has an open neighbourhood U over which α is induced by a morphism of complexes β : ℰ|_U ⟶ ℱ|_U, the comparison being made through the canonical isomorphism CategoryTheory.Functor.mapDerivedCategoryFactors of the exact functor restrictModules X U.

The exactness of restriction, which is what makes that comparison available, is part of the assertion; the witnesses are the instances AlgebraicGeometry.RingedSpace.restrictModules_additive, AlgebraicGeometry.RingedSpace.restrictModules_preservesFiniteLimits and AlgebraicGeometry.RingedSpace.restrictModules_preservesFiniteColimits, and the content is AlgebraicGeometry.RingedSpace.exists_local_complex_map_of_instances.

public theorem exists_local_complex_map [HasDerivedCategory.{d} (OXMod.{u, u} X)]
    [∀ U : Opens X.carrier,
      HasDerivedCategory.{d'} (OXMod.{u, u} (X.restrict U.isOpenEmbedding))]
    {E F : CochainComplex (OXMod.{u, u} X) ℤ} (hE : IsStrictlyPerfect E)
    (α : DerivedCategory.Q.obj E ⟶ DerivedCategory.Q.obj F) :
    ∀ x : X.carrier, ∃ U : Opens X.carrier, x ∈ U ∧
      ∃ (hadd : (restrictModules.{u, u} X U).Additive)
        (hlim : PreservesFiniteLimits (restrictModules.{u, u} X U))
        (hcolim : PreservesFiniteColimits (restrictModules.{u, u} X U)),
        letI := hadd
        letI := hlim
        letI := hcolim
        ∃ β : ((restrictModules.{u, u} X U).mapHomologicalComplex (ComplexShape.up ℤ)).obj E ⟶
            ((restrictModules.{u, u} X U).mapHomologicalComplex (ComplexShape.up ℤ)).obj F,
          (restrictModules.{u, u} X U).mapDerivedCategory.map α ≫
              (restrictModules.{u, u} X U).mapDerivedCategoryFactors.hom.app F =
            (restrictModules.{u, u} X U).mapDerivedCategoryFactors.hom.app E ≫
              DerivedCategory.Q.map β

Stacks.Cohomology.exists_local_complex_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/HomComplexAndStrictPerfection/LocalRepresentation.lean, line 216. The attribute's comment: “local_representation”.

A derived morphism out of a strictly perfect complex is locally represented by a morphism of complexes.

theorem exists_local_complex_map (hE : IsStrictlyPerfect E)
    (α : DerivedCategory.Q.obj E ⟶ DerivedCategory.Q.obj F) :
    ∀ x : X.carrier, ∃ U : Opens X.carrier, x ∈ U ∧
      ∃ (hadd : (RingedSpace.restrictModules.{u, u} X U).Additive)
        (hlim : PreservesFiniteLimits (RingedSpace.restrictModules.{u, u} X U))
        (hcolim : PreservesFiniteColimits (RingedSpace.restrictModules.{u, u} X U)),
        letI := hadd
        letI := hlim
        letI := hcolim
        ∃ β : ((RingedSpace.restrictModules.{u, u} X U).mapHomologicalComplex
              (ComplexShape.up ℤ)).obj E ⟶
            ((RingedSpace.restrictModules.{u, u} X U).mapHomologicalComplex
              (ComplexShape.up ℤ)).obj F,
          (RingedSpace.restrictModules.{u, u} X U).mapDerivedCategory.map α ≫
              (RingedSpace.restrictModules.{u, u} X U).mapDerivedCategoryFactors.hom.app F =
          (RingedSpace.restrictModules.{u, u} X U).mapDerivedCategoryFactors.hom.app E ≫
              DerivedCategory.Q.map β

Tag 08DM, a lemma

Tag 08DM in the Stacks Project.

Stacks.SheafOfModules.strictlyPerfectHomDegreeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/StrictlyPerfectHomRepresentation.lean, line 90. The attribute's comment: “finite direct-sum terms and Hom differential”.

Stacks 08DM, the degreewise description. The degree-n term of the internal Hom complex SheafHom(E, F) of a bounded complex E is the finite direct sum ⊕\_q Hom\_\{O\_X}(E^\{-q}, F^\{n-q}), that is ⊕\_\{n = p + q} Hom\_\{O\_X}(E^\{-q}, F^p).

def strictlyPerfectHomDegreeIso (hE : {i : ℤ | ¬ IsZero (E.X i)}.Finite) (n : ℤ) :
    (RingedSite.sheafHomComplex (ringedSite Rc) E F).obj.X n ≅
      ∐ (fun q : ℤ => RingedSite.internalHomSheaf (ringedSite Rc) (E.X (-q)) (F.X (n - q)))

Stacks.SheafOfModules.strictlyPerfectHomComparison_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/StrictlyPerfectHomRepresentation.lean, line 106. The attribute's comment: “representation by the finite direct-sum Hom complex”.

Stacks 08DM. For E strictly perfect — bounded, with every term a direct summand of a finite free O_X-module — the derived internal Hom RSheafHom(E, F) is represented by the ordinary internal Hom complex SheafHom(E, F) of Stacks 0A8Z, for every complex F, the comparison being the canonical one. No injective resolution of F is needed.

The comparison is an isomorphism exactly when the map of internal Hom complexes induced by the K-injective augmentation of F is a quasi-isomorphism, and strict perfectness of E makes it one: the statement holds for a source concentrated in one degree whose term is the structure sheaf, hence for finite free terms by direct sums, hence for direct summands of those by retracts, and the stupid filtration of the bounded complex E assembles the terms.

theorem strictlyPerfectHomComparison_isIso
    (hE : {i : ℤ | ¬ IsZero (E.X i)}.Finite)
    (hterm : ∀ i : ℤ, RingedSite.IsFiniteFreeSummand (ringedSite Rc) (E.X i)) :
    IsIso (strictlyPerfectHomComparison Rc E F)

Tag 0GM5, a lemma

Tag 0GM5 in the Stacks Project.

Stacks.SheafOfModules.isKFlat_sheafHomComplex_of_isKFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/StrictlyPerfectHomKFlat.lean, line 260. The attribute's comment: “the whole lemma on a ringed space: for E strictly perfect, written out as in Definition 20.46.1 -- hE is 'E^i is zero for all but finitely many i' and hterm is 'E^i is a direct summand of a finite free O_X-module for all i' -- and F K-flat (hF), the complex sheafHomComplex E F is K-flat”.

Stacks 0GM5. In the situation of Stacks 08DM — E strictly perfect, so that the internal Hom complex H = SheafHom(E, F) represents RSheafHom(E, F) — the complex H is K-flat as soon as F is.

For an acyclic G the argument is: F is K-flat and G is acyclic, so Tot(G ⊗ F) is acyclic; the internal Hom complex out of a strictly perfect source into an acyclic complex is acyclic, so the target of the Stacks 0BYR comparison Tot(G ⊗ SheafHom(E, F)) ⟶ SheafHom(E, Tot(G ⊗ F)) is acyclic; that comparison is a quasi-isomorphism at a strictly perfect source, by the dévissage along the termwise split stupid filtration of Homology, Section 0118 on the ringed site of the opens of X in AlgebraicGeometry.RingedSite.tensorHomInterchange_quasiIso_of_isFiniteFreeSummand; hence its source is acyclic too, and that source is the total complex K-flatness of H asks about.

theorem isKFlat_sheafHomComplex_of_isKFlat
    (E F : CochainComplex (StructureSheafModules Rc) ℤ)
    (hE : {i : ℤ | ¬ IsZero (E.X i)}.Finite)
    (hterm : ∀ i : ℤ, RingedSite.IsFiniteFreeSummand (ringedSite Rc) (E.X i))
    (hF : IsKFlat Rc F) :
    IsKFlat Rc (sheafHomComplex Rc E F).obj

AlgebraicGeometry.RingedSite.isKFlat_sheafHomComplex_of_isKFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/StrictlyPerfectHomKFlatSite.lean, line 124. The attribute's comment: “on a ringed site”.

Stacks 0GM5 on a ringed site. In the situation of Stacks 08DM — E with finitely many nonzero terms, each a direct summand of a finite free module, so that the internal Hom complex SheafHom(E, F) represents RSheafHom(E, F) — that complex is K-flat as soon as F is.

This is what makes the dual SheafHom(P, O[0]) of a strictly perfect complex P usable as the K-flat tensor factor in the invertibility criterion for the composition morphism of derived internal Homs, and so is the input the local step of the third assertion of Stacks 08DQ needs on the slices of the site.

theorem isKFlat_sheafHomComplex_of_isKFlat
    (E F : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ)
    (hE : {i : ℤ | ¬ IsZero (E.X i)}.Finite)
    (hterm : ∀ i : ℤ, IsFiniteFreeSummand X (E.X i))
    (hF : letI : X.J.WEqualsLocallyBijective AddCommGrpCat.{u} := inferInstance
      Stacks.SheafOfModules.IsKFlat X.O F) :
    letI : X.J.WEqualsLocallyBijective AddCommGrpCat.{u} := inferInstance
    Stacks.SheafOfModules.IsKFlat X.O (sheafHomComplex X E F).obj

Tag 08I5, a lemma

Tag 08I5 in the Stacks Project.

AlgebraicGeometry.RingedSite.homMap_quasiIso_of_boundedAbove_isFiniteFreeSummand, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/StrictlyPerfect/BoundedAboveHomComparison.lean, line 281. The attribute's comment: “invariance of the internal Hom complex under quasi-isomorphism”.

Stacks 08I5, the quasi-isomorphism invariance. Let E be a complex of O-modules which is bounded above and all of whose terms are direct summands of finite free O-modules. Then the internal Hom complex out of E carries a quasi-isomorphism between two complexes vanishing in all degrees below a common bound a to a quasi-isomorphism.

This is the whole content of the tag; the representation statement strictlyPerfectHomComparison_isIso_of_boundedAbove is obtained from it by the formal reduction strictlyPerfectHomComparison_isIso_iff.

Unlike homMap_quasiIso_of_isFiniteFreeSummand (Stacks 08JH) the source is not assumed to have finitely many nonzero terms, and in exchange the targets are assumed bounded below. The proof is degreewise: quasiIsoAt_homMap_of_boundedAbove at k = a - n - 1.

theorem homMap_quasiIso_of_boundedAbove_isFiniteFreeSummand (a : ℤ)
    (hF : ∀ i, i < a → IsZero (F.X i))
    (hG : ∀ i, i < a → IsZero (G.X i))
    (hE : ∃ b : ℤ, ∀ i, b < i → IsZero (E.X i))
    (hterm : ∀ i, IsFiniteFreeSummand X (E.X i))
    (f : F ⟶ G) [QuasiIso f] :
    QuasiIso (homMap X (𝟙 E) f)

AlgebraicGeometry.RingedSite.strictlyPerfectHomComparison_isIso_of_boundedAbove, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/StrictlyPerfect/BoundedAboveHomComparison.lean, line 309. The attribute's comment: “representation of derived internal Hom by the ordinary Hom complex”.

Stacks 08I5, the representation statement. Let E be a complex of O-modules which is bounded above and all of whose terms are direct summands of finite free O-modules, and let F vanish in all degrees below a. Then the derived internal Hom RSheafHom(E, F) is represented by the ordinary internal Hom complex SheafHom(E, F) of Stacks 0A8Z, the comparison being the canonical one of strictlyPerfectHomComparison.

By strictlyPerfectHomComparison_isIso_iff the claim is the quasi-isomorphy of the map of internal Hom complexes induced by the K-injective augmentation F ⟶ I of the target. The chosen resolution I carries no lower bound, so the invariance is applied instead to a degreewise injective resolution u : F ⟶ I₀ which is again zero below a, and transported to the augmentation of F along the naturality square of the augmentation; the two maps between K-injective complexes occurring there are handled by homMap_quasiIso (Stacks 0A95). See the implementation notes.

theorem strictlyPerfectHomComparison_isIso_of_boundedAbove (a : ℤ)
    (hF : ∀ i, i < a → IsZero (F.X i))
    (hE : ∃ b : ℤ, ∀ i, b < i → IsZero (E.X i))
    (hterm : ∀ i, IsFiniteFreeSummand X (E.X i)) :
    IsIso (strictlyPerfectHomComparison X D E F)

Sources

• Section 20.46, Tag 08C3
• AxiomMath/Stacks at 5ed82d14

LeanStrictlyPerfect.IsStrictlyPerfect · StrictlyPerfect.isStrictlyPerfect_mappingCone · strictlyPerfect_tensorObj · Stacks.Cohomology.StrictlyPerfectPullback.pullback_isStrictlyPerfect · StrictlyPerfect.exists_over_lift_of_isDirectSummandOfFiniteFree · StrictlyPerfect.exists_local_lift_of_isDirectSummandOfFiniteFree · AlgebraicGeometry.RingedSpace.exists_local_lift_of_isDirectSummandOfFiniteFree · StrictlyPerfect.LocalLifting.exists_local_lift

Section20.47 Pseudo-coherent modules#

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

Tag 08CB, a definition

Tag 08CB in the Stacks Project.

AlgebraicGeometry.RingedSpace.IsPseudoCoherentComplexFrom, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/SheafLevel.lean, line 109. The attribute's comment: “part (1)”.

A complex of 𝒪_X-modules is m-pseudo-coherent if every point of X has an open neighbourhood on which the complex admits a strictly perfect approximation in degrees at least m: a map from a strictly perfect complex which is an isomorphism on cohomology in every degree above m and an epimorphism on cohomology in degree m.

public abbrev IsPseudoCoherentComplexFrom
    (E : CochainComplex (StrictlyPerfect.OXMod.{u, u, u} X) ℤ) (m : ℤ) : Prop

AlgebraicGeometry.RingedSpace.IsPseudoCoherentComplex, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/SheafLevel.lean, line 122. The attribute's comment: “part (2)”.

A complex of 𝒪_X-modules is pseudo-coherent if it is m-pseudo-coherent for every integer m.

public abbrev IsPseudoCoherentComplex
    (E : CochainComplex (StrictlyPerfect.OXMod.{u, u, u} X) ℤ) : Prop

AlgebraicGeometry.RingedSpace.IsPseudoCoherentFrom, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/SheafLevel.lean, line 129. The attribute's comment: “part (3), m-pseudo-coherent”.

An object of the derived category of 𝒪_X-modules is m-pseudo-coherent if it is represented by an m-pseudo-coherent complex.

public abbrev IsPseudoCoherentFrom
    [HasDerivedCategory.{d} (StrictlyPerfect.OXMod.{u, u, u} X)]
    (E : DerivedCategory (StrictlyPerfect.OXMod.{u, u, u} X)) (m : ℤ) : Prop

AlgebraicGeometry.RingedSpace.IsPseudoCoherent, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/SheafLevel.lean, line 138. The attribute's comment: “part (3), pseudo-coherent”.

An object of the derived category of 𝒪_X-modules is pseudo-coherent if it is represented by a pseudo-coherent complex.

public abbrev IsPseudoCoherent
    [HasDerivedCategory.{d} (StrictlyPerfect.OXMod.{u, u, u} X)]
    (E : DerivedCategory (StrictlyPerfect.OXMod.{u, u, u} X)) : Prop

Tag 08CC, a lemma

Tag 08CC in the Stacks Project.

AlgebraicGeometry.RingedSpace.isPseudoCoherentComplexFrom_of_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/PseudoCoherentIso.lean, line 674. The attribute's comment: “part (2)”. References: SGA 6 I (2.2), “a)”.

Let E be an m-pseudo-coherent object of the derived category of 𝒪_X-modules. Then every complex of 𝒪_X-modules representing E is m-pseudo-coherent.

public theorem isPseudoCoherentComplexFrom_of_iso (E : DerivedCategory (OXMod.{u, u} X)) (m : ℤ)
    (hE : IsPseudoCoherentFrom E m) (K : CochainComplex (OXMod.{u, u} X) ℤ)
    (e : DerivedCategory.Q.obj K ≅ E) : IsPseudoCoherentComplexFrom K m

AlgebraicGeometry.RingedSpace.isPseudoCoherentFrom_of_local_derived_approximation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/PseudoCoherentIso.lean, line 704. The attribute's comment: “part (1)”. References: SGA 6 I (2.2), “b) (ii')=>(ii)”.

Let E be an object of the derived category of 𝒪_X-modules and suppose that every point of X has an open neighbourhood U on which some strictly perfect complex 𝒫 maps to E|_U in D(𝒪_U) by a morphism which is an isomorphism on cohomology above m and an epimorphism in degree m. Then E is m-pseudo-coherent. Here E|_U is presented as Q(𝒦|_U) for a complex 𝒦 representing E.

public theorem isPseudoCoherentFrom_of_local_derived_approximation
    [∀ U : Opens X.carrier,
      HasDerivedCategory.{d'} (OXMod.{u, u} (X.restrict U.isOpenEmbedding))]
    (E : DerivedCategory (OXMod.{u, u} X)) (m : ℤ) (K : CochainComplex (OXMod.{u, u} X) ℤ)
    (e : DerivedCategory.Q.obj K ≅ E)
    (h : ∀ x : X.carrier, ∃ U : Opens X.carrier, x ∈ U ∧
      ∃ P : CochainComplex (OXMod.{u, u} (X.restrict U.isOpenEmbedding)) ℤ,
        IsStrictlyPerfect P ∧
        ∃ α : DerivedCategory.Q.obj P ⟶ DerivedCategory.Q.obj (restrictComplex K U),
          (∀ j : ℤ, m < j → IsIso ((DerivedCategory.homologyFunctor _ j).map α)) ∧
          Epi ((DerivedCategory.homologyFunctor _ m).map α)) :
    IsPseudoCoherentFrom E m

Stacks.PseudoCoherence.DerivedCharacterization.isPseudoCoherentFrom_of_local_derived_approximation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PseudoCoherence/DerivedCharacterization.lean, line 244. The attribute's comment: “part (1)”.

Tag 08CC part (1). Local strictly perfect approximations in the derived category make a derived object m-pseudo-coherent.

theorem isPseudoCoherentFrom_of_local_derived_approximation
    [∀ U : Opens X.carrier,
      HasDerivedCategory.{d'} (OXMod.{u} (X.restrict U.isOpenEmbedding))]
    (E : DerivedCategory (OXMod.{u} X)) (m : ℤ) (K : CochainComplex (OXMod.{u} X) ℤ)
    (e : DerivedCategory.Q.obj K ≅ E)
    (h : ∀ x : X.carrier, ∃ U : Opens X.carrier, x ∈ U ∧
      ∃ P : CochainComplex (OXMod.{u} (X.restrict U.isOpenEmbedding)) ℤ,
        IsStrictlyPerfect P ∧
        ∃ α : DerivedCategory.Q.obj P ⟶
          DerivedCategory.Q.obj (AlgebraicGeometry.RingedSpace.PseudoCoherence.restrictComplex K U),
          (∀ j : ℤ, m < j → IsIso ((DerivedCategory.homologyFunctor _ j).map α)) ∧
          Epi ((DerivedCategory.homologyFunctor _ m).map α)) :
    AlgebraicGeometry.RingedSpace.PseudoCoherence.IsPseudoCoherentFrom (X := X) E m

Stacks.PseudoCoherence.DerivedCharacterization.isPseudoCoherentComplexFrom_of_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PseudoCoherence/DerivedCharacterization.lean, line 264. The attribute's comment: “part (2)”. References: SGA 6 I (2.2), “a)”.

Tag 08CC part (2). Every complex representing an m-pseudo-coherent derived object is m-pseudo-coherent.

theorem isPseudoCoherentComplexFrom_of_iso (E : DerivedCategory (OXMod.{u} X)) (m : ℤ)
    (hE : AlgebraicGeometry.RingedSpace.PseudoCoherence.IsPseudoCoherentFrom (X := X) E m)
    (K : CochainComplex (OXMod.{u} X) ℤ) (e : DerivedCategory.Q.obj K ≅ E) :
    AlgebraicGeometry.RingedSpace.PseudoCoherence.IsPseudoCoherentComplexFrom (X := X) K m

Tag 09U7, a lemma

Tag 09U7 in the Stacks Project.

AlgebraicGeometry.RingedSpace.KFlatDerivedPullback.isPseudoCoherentFrom_derivedPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PseudoCoherence/DerivedPullback.lean, line 189.

Stacks 09U7. The derived pullback of an m-pseudo-coherent object of D(𝒪_Y) along a morphism of ringed spaces is m-pseudo-coherent.

isPseudoCoherentFrom_derivedPullback_of_complexLevel reduces this to the complex level, which is AlgebraicGeometry.RingedSpace.KFlatDerivedPullback.isPseudoCoherentComplexFrom_modulePullback.

theorem isPseudoCoherentFrom_derivedPullback {X Y : RingedSpace.{u, u}} (f : X ⟶ Y)
    (E : DerivedCategory (OXMod.{u} Y)) (m : ℤ)
    (hE : AlgebraicGeometry.RingedSpace.PseudoCoherence.IsPseudoCoherentFrom (X := Y) E m) :
    AlgebraicGeometry.RingedSpace.PseudoCoherence.IsPseudoCoherentFrom (X := X)
      ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback f).obj E) m

Tag 08CD, a lemma

Tag 08CD in the Stacks Project.

AlgebraicGeometry.RingedSpace.isPseudoCoherentFrom_obj₃_of_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/PseudoCoherentTriangle.lean, line 483. The attribute's comment: “part (1)”.

Stacks 08CD, part (1). If the first term of a distinguished triangle in the derived category of 𝒪_X-modules is (m + 1)-pseudo-coherent and the second is m-pseudo-coherent, then the third is m-pseudo-coherent.

public theorem isPseudoCoherentFrom_obj₃_of_distinguished (m : ℤ)
    (T : Triangle (DerivedCategory (OXMod.{u, u} X))) (hT : T ∈ distinguishedTriangles)
    (hK : IsPseudoCoherentFrom T.obj₁ (m + 1)) (hL : IsPseudoCoherentFrom T.obj₂ m) :
    IsPseudoCoherentFrom T.obj₃ m

AlgebraicGeometry.RingedSpace.isPseudoCoherentFrom_obj₂_of_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/PseudoCoherentTriangle.lean, line 497. The attribute's comment: “part (2)”. References: SGA 6 I (2.5), “b), ringed space”.

Stacks 08CD, part (2). If the first and third terms of a distinguished triangle in the derived category of 𝒪_X-modules are m-pseudo-coherent, then so is the second.

Apply part (1) to the inverse rotation of the triangle, whose first two terms are M[-1] and K.

public theorem isPseudoCoherentFrom_obj₂_of_distinguished (m : ℤ)
    (T : Triangle (DerivedCategory (OXMod.{u, u} X))) (hT : T ∈ distinguishedTriangles)
    (hK : IsPseudoCoherentFrom T.obj₁ m) (hM : IsPseudoCoherentFrom T.obj₃ m) :
    IsPseudoCoherentFrom T.obj₂ m

AlgebraicGeometry.RingedSpace.isPseudoCoherentFrom_obj₁_of_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/PseudoCoherentTriangle.lean, line 511. The attribute's comment: “part (3)”.

Stacks 08CD, part (3). If the second term of a distinguished triangle in the derived category of 𝒪_X-modules is (m + 1)-pseudo-coherent and the third is m-pseudo-coherent, then the first is (m + 1)-pseudo-coherent.

Apply part (1) to the rotation of the triangle, whose third term is K[1].

public theorem isPseudoCoherentFrom_obj₁_of_distinguished (m : ℤ)
    (T : Triangle (DerivedCategory (OXMod.{u, u} X))) (hT : T ∈ distinguishedTriangles)
    (hL : IsPseudoCoherentFrom T.obj₂ (m + 1)) (hM : IsPseudoCoherentFrom T.obj₃ m) :
    IsPseudoCoherentFrom T.obj₁ (m + 1)

Tag 09J3, a lemma

Tag 09J3 in the Stacks Project.

AlgebraicGeometry.RingedSpace.isPseudoCoherentFrom_derivedTensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PseudoCoherence/DerivedTensorProduct.lean, line 480. The attribute's comment: “part (1)”. References: SGA 6 I (2.16), “special case”.

Tag 09J3, part (1). Let (X, 𝒪_X) be a ringed space and let K, L be objects of D(𝒪_X). If K is n-pseudo-coherent with H^i(K) = 0 for i > a, and L is m-pseudo-coherent with H^j(L) = 0 for j > b, then K ⊗_{𝒪_X}^{𝐋} L is t-pseudo-coherent for t = max (m + a, n + b).

If a < n then t > a + b, so the conclusion follows from right t-exactness of the derived tensor product alone; that is Stacks.Cohomology.PseudoCoherentTensor.isPseudoCoherentFrom_derivedTensorProduct_of_lt. Otherwise n ≤ a. Both factors are replaced by K-flat representatives 𝒜, ℬ with no terms above their own bounds (Tag 06YQ through Tag 05T7); on those the derived tensor product is Tot(𝒜 ⊗_{𝒪_X} ℬ) by the comparison of Tag 06YU, so that complex represents K ⊗^{𝐋} L and is the one fed to Tag 08CC part (1). Pseudo-coherence passes to 𝒜 and ℬ by Tag 08CC part (2), and AlgebraicGeometry.RingedSpace.localApproximationData produces the required local approximations in degree t.

theorem isPseudoCoherentFrom_derivedTensorProduct
    (T : Stacks.DerivedTensor.RingedSite.DerivedTensorProduct X.sheaf)
    (K L : DerivedCategory (KFlatDerivedPullback.Modules X)) (n m a b : ℤ)
    (hK : IsPseudoCoherentFrom (X := X) K n)
    (hKa : ∀ i : ℤ, a < i →
      IsZero ((DerivedCategory.homologyFunctor (KFlatDerivedPullback.Modules X) i).obj K))
    (hL : IsPseudoCoherentFrom (X := X) L m)
    (hLb : ∀ j : ℤ, b < j →
      IsZero ((DerivedCategory.homologyFunctor (KFlatDerivedPullback.Modules X) j).obj L)) :
    IsPseudoCoherentFrom (X := X) ((T.tensor.obj K).obj L) (max (m + a) (n + b))

AlgebraicGeometry.RingedSpace.isPseudoCoherent_derivedTensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PseudoCoherence/DerivedTensorProduct.lean, line 521. The attribute's comment: “part (2)”.

Tag 09J3, part (2). The derived tensor product of two pseudo-coherent objects of D(𝒪_X) is pseudo-coherent.

Neither factor is assumed bounded above, so the representatives come from the unrestricted K-flat resolutions of Tag 06YS rather than from a bounded one; Tot(𝒜 ⊗_{𝒪_X} ℬ) is then a representative of K ⊗^{𝐋} L, and it suffices to see that it is q-pseudo-coherent as a complex for every q. By Tag 08CC that is q-pseudo-coherence of K ⊗^{𝐋} L, which AlgebraicGeometry.RingedSpace.localApproximationData_of_isPseudoCoherentComplex supplies: the cohomological bounds that part (1) needs are produced on an open covering, which is the source's reduction to a covering on which both factors are bounded above.

theorem isPseudoCoherent_derivedTensorProduct
    (T : Stacks.DerivedTensor.RingedSite.DerivedTensorProduct X.sheaf)
    (K L : DerivedCategory (KFlatDerivedPullback.Modules X))
    (hK : IsPseudoCoherent (X := X) K) (hL : IsPseudoCoherent (X := X) L) :
    IsPseudoCoherent (X := X) ((T.tensor.obj K).obj L)

Tag 08CE, a lemma

Tag 08CE in the Stacks Project.

AlgebraicGeometry.RingedSpace.isPseudoCoherentFrom_of_biprod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/PseudoCoherentSummand.lean, line 159. The attribute's comment: “m-pseudo-coherent, both summands”. References: SGA 6 I (2.12), “n-pc: sum ⇒ F',F''”.

Stacks 064X on a ringed space: both summands of an m-pseudo-coherent binary biproduct in D(𝒪_X) are m-pseudo-coherent.

m-pseudo-coherence is local (AlgebraicGeometry.RingedSpace.isPseudoCoherentFrom_of_local_restrict), so it is enough to find, around every point, an open U on which the restriction of the summand is m-pseudo-coherent. Choose U so that A ⊞ B has no cohomology above some degree there (AlgebraicGeometry.RingedSpace.exists_isZero_homology_gt_derivedRestrict); restriction is additive, so (A ⊞ B)|_U ≅ A|_U ⊞ B|_U, and AlgebraicGeometry.RingedSpace.isPseudoCoherentFrom_of_biprod_of_isZero_homology_gt applies on X|U.

This is also Stacks 08CE for a fixed degree: the ringed-space statement of 08CE at a fixed degree is literally this one, and both of its conclusions are proved here at once.

public theorem isPseudoCoherentFrom_of_biprod (m : ℤ)
    {A B : DerivedCategory (OXMod.{u, u} X)} (h : IsPseudoCoherentFrom (A ⊞ B) m) :
    IsPseudoCoherentFrom A m ∧ IsPseudoCoherentFrom B m

AlgebraicGeometry.RingedSpace.isPseudoCoherentFrom_left_of_biprod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PseudoCoherence/DirectSummand.lean, line 177. The attribute's comment: “m-pseudo-coherent, first summand”. References: SGA 6 I (2.12), “n-pc: sum ⇒ F'”.

Stacks Project, Tag 08CE. The first summand of an m-pseudo-coherent biproduct is m-pseudo-coherent.

public theorem isPseudoCoherentFrom_left_of_biprod
    [HasDerivedCategory.{d} (OXMod.{u, u} X)]
    (K L : DerivedCategory (OXMod.{u, u} X)) (m : ℤ)
    (h : IsPseudoCoherentFrom (K ⊞ L) m) : IsPseudoCoherentFrom K m

AlgebraicGeometry.RingedSpace.isPseudoCoherentFrom_right_of_biprod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PseudoCoherence/DirectSummand.lean, line 234. The attribute's comment: “m-pseudo-coherent, second summand”. References: SGA 6 I (2.12), “n-pc: sum ⇒ F''”.

Stacks Project, Tag 08CE. The second summand of an m-pseudo-coherent biproduct is m-pseudo-coherent.

public theorem isPseudoCoherentFrom_right_of_biprod
    [HasDerivedCategory.{d} (OXMod.{u, u} X)]
    (K L : DerivedCategory (OXMod.{u, u} X)) (m : ℤ)
    (h : IsPseudoCoherentFrom (K ⊞ L) m) : IsPseudoCoherentFrom L m

AlgebraicGeometry.RingedSpace.isPseudoCoherent_left_of_biprod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PseudoCoherence/DirectSummand.lean, line 243. The attribute's comment: “pseudo-coherent, first summand”.

Stacks Project, Tag 08CE. The first summand of a pseudo-coherent biproduct is pseudo-coherent.

public theorem isPseudoCoherent_left_of_biprod
    [HasDerivedCategory.{d} (OXMod.{u, u} X)]
    (K L : DerivedCategory (OXMod.{u, u} X)) (h : IsPseudoCoherent (K ⊞ L)) :
    IsPseudoCoherent K

AlgebraicGeometry.RingedSpace.isPseudoCoherent_right_of_biprod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PseudoCoherence/DirectSummand.lean, line 257. The attribute's comment: “pseudo-coherent, second summand”.

Stacks Project, Tag 08CE. The second summand of a pseudo-coherent biproduct is pseudo-coherent.

public theorem isPseudoCoherent_right_of_biprod
    [HasDerivedCategory.{d} (OXMod.{u, u} X)]
    (K L : DerivedCategory (OXMod.{u, u} X)) (h : IsPseudoCoherent (K ⊞ L)) :
    IsPseudoCoherent L

Stacks.PseudoCoherence.Summands.isPseudoCoherent_of_biprod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PseudoCoherence/Summands.lean, line 62. The attribute's comment: “pseudo-coherent, both summands”.

Stacks 08CE. Both summands of a pseudo-coherent binary biproduct in D(O_X) are pseudo-coherent.

Pseudo-coherence is m-pseudo-coherence in every degree, by AlgebraicGeometry.RingedSpace.isPseudoCoherent_iff_forall, and in each degree the two summands are m-pseudo-coherent by AlgebraicGeometry.RingedSpace.isPseudoCoherentFrom_of_biprod.

theorem isPseudoCoherent_of_biprod {X : RingedSpace.{u, u}}
    [HasDerivedCategory.{d} (OXMod.{u, u} X)]
    [∀ V : Opens X.carrier,
      HasDerivedCategory.{d'} (OXMod.{u, u} (X.restrict V.isOpenEmbedding))]
    (A B : DerivedCategory (OXMod.{u, u} X))
    (h : AlgebraicGeometry.RingedSpace.IsPseudoCoherent (A ⊞ B)) :
    AlgebraicGeometry.RingedSpace.IsPseudoCoherent A ∧
      AlgebraicGeometry.RingedSpace.IsPseudoCoherent B

Tag 09V7, a lemma

Tag 09V7 in the Stacks Project.

AlgebraicGeometry.RingedSpace.isPseudoCoherentComplexFrom_of_locally_boundedAbove, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/BoundedComplex.lean, line 387. References: SGA 5 VIII (5.1), “'if' direction”.

Stacks 09V7. Let X be a ringed space, let m be an integer and let 𝒦 be a complex of 𝒪_X-modules which is bounded above on a neighbourhood of every point and whose term 𝒦^i is (m - i)-pseudo-coherent for every i. Then 𝒦 is an m-pseudo-coherent complex.

The hypothesis on the terms is turned into the form the induction uses by AlgebraicGeometry.RingedSpace.isPseudoCoherentFrom_singleFunctor_of_singleFunctor_zero, and AlgebraicGeometry.RingedSpace.isPseudoCoherentFrom_Q_of_locally_boundedAbove is read back on the complex through Stacks 08CC part (2).

public theorem isPseudoCoherentComplexFrom_of_locally_boundedAbove (m : ℤ)
    (K : CochainComplex (OXMod.{u, u} X) ℤ)
    (hbdd : ∀ x : X.carrier, ∃ U : Opens X.carrier, x ∈ U ∧ ∃ b : ℤ, ∀ p : ℤ, b < p →
      IsZero ((restrictComplex K U).X p))
    (hK : ∀ i : ℤ, IsPseudoCoherentFrom
      ((DerivedCategory.singleFunctor (OXMod.{u, u} X) 0).obj (K.X i)) (m - i)) :
    IsPseudoCoherentComplexFrom K m

Tag 09V8, a lemma

Tag 09V8 in the Stacks Project.

AlgebraicGeometry.RingedSpace.isPseudoCoherentFrom_of_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/PseudoCoherent/CohomologyBoundedAbove.lean, line 208.

Stacks Project, Tag 09V8. Let X be a ringed space, m : ℤ and E an object of the derived category of 𝒪_X-modules which is locally bounded above. If the cohomology sheaf Hⁱ(E) is (m - i)-pseudo-coherent for every i, then E is m-pseudo-coherent.

theorem isPseudoCoherentFrom_of_homology (E : DerivedCategory (OXMod.{u, u} X)) (m : ℤ)
    (hbdd : IsLocallyBoundedAbove E)
    (hcoh : ∀ i : ℤ, IsPseudoCoherentFrom
      ((DerivedCategory.singleFunctor (OXMod.{u, u} X) 0).obj
        ((DerivedCategory.homologyFunctor (OXMod.{u, u} X) i).obj E)) (m - i)) :
    IsPseudoCoherentFrom E m

Tag 08DN, a lemma

Tag 08DN in the Stacks Project.

AlgebraicGeometry.RingedSpace.isFinitePresentation_homology_of_isPseudoCoherentFrom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/FinitePresentationNextCohomology.lean, line 251. The attribute's comment: “part (2)”.

Let X be a ringed space and let K be an m-pseudo-coherent object of the derived category of 𝒪_X-modules with H^i(K) = 0 for i > m + 1. Then H^{m+1}(K) is an 𝒪_X-module of finite presentation.

public theorem isFinitePresentation_homology_of_isPseudoCoherentFrom
    [HasDerivedCategory.{d} (OXMod.{u, u} X)] (K : DerivedCategory (OXMod.{u, u} X)) (m : ℤ)
    (hK : IsPseudoCoherentFrom K m)
    (hvanish : ∀ i : ℤ, m + 1 < i →
      IsZero ((DerivedCategory.homologyFunctor (OXMod.{u, u} X) i).obj K)) :
    SheafOfModules.IsFinitePresentation (R := structureSheafOfRings X)
      ((DerivedCategory.homologyFunctor (OXMod.{u, u} X) (m + 1)).obj K)

AlgebraicGeometry.RingedSpace.isFiniteType_homology_of_isPseudoCoherentFrom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/ImmersionIndependence.lean, line 234. The attribute's comment: “part (1)”.

Stacks 08DN, part (1). Let X be a ringed space and let K be an m-pseudo-coherent object of the derived category of 𝒪_X-modules with H^i(K) = 0 for i > m. Then H^m(K) is an 𝒪_X-module of finite type.

Finite type is a local condition, so it is enough to produce, around each point of X, an epimorphism onto H^m(K) from a finite free module. Let E be a complex representing K which is m-pseudo-coherent as a complex, and let 𝒫 ⟶ E|_U be a strictly perfect approximation on an open neighbourhood U of the given point: it is an isomorphism on cohomology above m and an epimorphism in degree m. Since restriction is exact and H^i(K) vanishes above m, the cohomology of 𝒫 vanishes above m too, so AlgebraicGeometry.RingedSpace.exists_isDirectSummandOfFiniteFree_restrict_cycles makes Z^m(𝒫) a direct summand of a finite free module after restriction to a smaller W. Composing the retraction with Z^m(𝒫) ⟶ H^m(𝒫) ⟶ H^m(E|_U) ≅ H^m(E)|_U gives the required epimorphism, which AlgebraicGeometry.RingedSpace.exists_epi_free_over_of_epi_finiteFree reads in the slice idiom in which finite type is phrased.

public theorem isFiniteType_homology_of_isPseudoCoherentFrom
    [HasDerivedCategory.{d} (OXMod.{u, u} X)] (K : DerivedCategory (OXMod.{u, u} X)) (m : ℤ)
    (hK : IsPseudoCoherentFrom K m)
    (hvanish : ∀ i : ℤ, m < i →
      IsZero ((DerivedCategory.homologyFunctor (OXMod.{u, u} X) i).obj K)) :
    SheafOfModules.IsFiniteType (R := structureSheafOfRings X)
      ((DerivedCategory.homologyFunctor (OXMod.{u, u} X) m).obj K)

Tag 09V9, a lemma

Tag 09V9 in the Stacks Project.

AlgebraicGeometry.RingedSpace.isPseudoCoherentFrom_singleFunctor_zero_neg_one_iff_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/FinitePresentationDegreeMinusOne.lean, line 338. The attribute's comment: “finite_presentation_iff_minus_one_pseudo_coherent”.

Let X be a ringed space and let ℱ be a sheaf of 𝒪_X-modules. Then ℱ, viewed in degree zero as an object of the derived category of 𝒪_X-modules, is (-1)-pseudo-coherent if and only if ℱ is an 𝒪_X-module of finite presentation.

public theorem isPseudoCoherentFrom_singleFunctor_zero_neg_one_iff_isFinitePresentation
    [HasDerivedCategory.{d} (OXMod.{u, u} X)] (F : OXMod.{u, u} X) :
    IsPseudoCoherentFrom ((DerivedCategory.singleFunctor (OXMod.{u, u} X) 0).obj F) (-1) ↔
      SheafOfModules.IsFinitePresentation (R := structureSheafOfRings X) F

AlgebraicGeometry.RingedSpace.isPseudoCoherentFrom_singleFunctor_zero_iff_isFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/FiniteTypeDegreeZero.lean, line 146. The attribute's comment: “finite_type_iff_zero_pseudo_coherent”.

Let X be a ringed space and let ℱ be a sheaf of 𝒪_X-modules. Then ℱ, viewed in degree zero as an object of the derived category of 𝒪_X-modules, is 0-pseudo-coherent if and only if ℱ is an 𝒪_X-module of finite type.

public theorem isPseudoCoherentFrom_singleFunctor_zero_iff_isFiniteType
    [HasDerivedCategory.{d} (OXMod.{u, u} X)] (F : OXMod.{u, u} X) :
    IsPseudoCoherentFrom ((DerivedCategory.singleFunctor (OXMod.{u, u} X) 0).obj F) 0 ↔
      SheafOfModules.IsFiniteType (R := structureSheafOfRings X) F

Sources

• Section 20.47, Tag 08CA
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.RingedSpace.IsPseudoCoherentComplexFrom · AlgebraicGeometry.RingedSpace.IsPseudoCoherentComplex · AlgebraicGeometry.RingedSpace.IsPseudoCoherentFrom · AlgebraicGeometry.RingedSpace.IsPseudoCoherent · AlgebraicGeometry.RingedSpace.isPseudoCoherentComplexFrom_of_iso · AlgebraicGeometry.RingedSpace.isPseudoCoherentFrom_of_local_derived_approximation · Stacks.PseudoCoherence.DerivedCharacterization.isPseudoCoherentFrom_of_local_derived_approximation · Stacks.PseudoCoherence.DerivedCharacterization.isPseudoCoherentComplexFrom_of_iso

Section20.48 Tor dimension#

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

Tag 08CG, a definition

Tag 08CG in the Stacks Project.

AlgebraicGeometry.RingedSpace.CertifiedDerivedSheafTensoring.HasTorAmplitudeIn, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/TorDimension.lean, line 174. The attribute's comment: “tor amplitude in an interval”. References: SGA 6 I (5.2), “Tor-amp(F) ⊂ [m,n]”; SGA 4½ Rapport (4.5), “sheaf tor-dimension ≤ r”; SGA 4 XVII (4.1.9), “ringed space, (i)”.

Stacks 08CG (1). An object E of D(𝒪_X) has Tor amplitude in [a, b] if, for every 𝒪_X-module ℱ and every integer i outside [a, b], the cohomology sheaf H^i(E ⊗^{L}_{𝒪_X} ℱ) vanishes.

The derived tensor product is the one carried by D; see the implementation notes of this file for what the certificate buys and for why the interval is not assumed nonempty.

public def HasTorAmplitudeIn (D : CertifiedDerivedSheafTensoring.{d, u} X)
    (E : DerivedCategory (OXMod.{u, u} X)) (a b : ℤ) : Prop

AlgebraicGeometry.RingedSpace.CertifiedDerivedSheafTensoring.HasFiniteTorDimension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/TorDimension.lean, line 196. The attribute's comment: “finite tor dimension”. References: SGA 6 I (5.2), “finite flat amplitude”; SGA 4½ Rapport (4.5), “sheaf case, finite”.

Stacks 08CG (2). An object E of D(𝒪_X) has finite Tor dimension if it has Tor amplitude in some interval [a, b].

public def HasFiniteTorDimension (D : CertifiedDerivedSheafTensoring.{d, u} X)
    (E : DerivedCategory (OXMod.{u, u} X)) : Prop

AlgebraicGeometry.RingedSpace.CertifiedDerivedSheafTensoring.HasTorDimensionLE, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/TorDimension.lean, line 205. The attribute's comment: “tor dimension of a module”. References: SGA 4½ Rapport (4.5), “sheaf module case”; SGA 4 XVII (4.1.9), “ringed space, module”.

The last sentence of Stacks 08CG. An 𝒪_X-module ℱ has Tor dimension at most n if ℱ[0], viewed in D(𝒪_X), has Tor amplitude in [-n, 0].

public def HasTorDimensionLE (D : CertifiedDerivedSheafTensoring.{d, u} X)
    (F : OXMod.{u, u} X) (n : ℤ) : Prop

AlgebraicGeometry.RingedSpace.LocallyHasFiniteTorDimension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/TorDimension.lean, line 233. The attribute's comment: “locally finite tor dimension”.

Stacks 08CG (3). An object E of D(𝒪_X) locally has finite Tor dimension if there is an open covering X = ⋃ U i such that E|_{U i} has finite Tor dimension for every i.

A derived tensor product is needed on each open subspace, so the certificate is a family D indexed by the opens of X; E|_{U i} is AlgebraicGeometry.RingedSpace.derivedRestrictModules.

public def LocallyHasFiniteTorDimension
    (D : ∀ U : Opens X.carrier,
      CertifiedDerivedSheafTensoring.{d', u} (X.restrict U.isOpenEmbedding))
    (E : DerivedCategory (OXMod.{u, u} X)) : Prop

CategoryTheory.DerivedCategory.HasTorAmplitudeIn, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/TorAmplitudeStalkwise.lean, line 143. The attribute's comment: “tor amplitude in an interval, for a derived tensor bifunctor T over an arbitrary abelian category: H^i(E ⊗^L F) = 0 for every object F in degree 0 and every i outside [a, b]; at the derivedTensor of AlgebraicGeometry.RingedSpace.CertifiedDerivedSheafTensoring it is CertifiedDerivedSheafTensoring.HasTorAmplitudeIn by Iff.rfl”.

Stacks 08CG (1), for a derived tensor product given as a bifunctor on D(A). An object E of D(A) has Tor amplitude in [a, b] when H^i(E ⊗^{L} F) = 0 for every object F of A and every i outside [a, b], the object F being read in degree 0.

On A = OXMod X this is AlgebraicGeometry.RingedSpace.CertifiedDerivedSheafTensoring.HasTorAmplitudeIn with T the certificate's derivedTensor, and the identification is Iff.rfl; hasTorAmplitudeIn_iff_hasTorAmplitude identifies it with the TorAmplitude.HasTorAmplitude of Stacks 08CJ.

This form is stated for a bifunctor T on the derived category of an arbitrary abelian category. AlgebraicGeometry.RingedSpace.CertifiedDerivedSheafTensoring.HasTorAmplitudeIn (StacksFrontier/AlgebraicGeometry/Perfect/TorDimension.lean) is the same clause for a bundle that also records an underived tensor product, a comparison and an IsLeftDerivedFunctor field, and Stacks.Cohomology.TorAmplitude.HasTorAmplitude (StacksFrontier/Topology/Sheaves/Cohomology/TorAmplitude/OnARingedSpace.lean) is the clause for the derived tensor product of Stacks 06YU.

public def HasTorAmplitudeIn
    (T : DerivedCategory A ⥤ DerivedCategory A ⥤ DerivedCategory A)
    (E : DerivedCategory A) (a b : ℤ) : Prop

Stacks.Cohomology.TorAmplitude.HasTorAmplitude, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/TorAmplitude/OnARingedSpace.lean, line 113. The attribute's comment: “tor amplitude in an interval, at the derived tensor product of Tag 06YU”. References: SGA 6 I (5.2), “Tor-amp(F) ⊂ [m,n]”; SGA 4½ Rapport (4.5), “sheaf tor-dimension ≤ r”; SGA 4 XVII (4.1.9), “ringed space, (i)”.

An object of D(O_X) has Tor amplitude in [a, b] when its derived tensor product with every O_X-module, placed in degree 0, has vanishing cohomology in every degree outside [a, b].

def HasTorAmplitude (X : RingedSpace.{u, u}) [HasDerivedCategory.{d} (OXMod.{u} X)]
    (E : DerivedCategory (OXMod.{u} X)) (a b : ℤ) : Prop

Stacks.Cohomology.TorAmplitude.HasFiniteTorDimension, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/TorAmplitude/OnARingedSpace.lean, line 125. The attribute's comment: “finite tor dimension, at the derived tensor product of Tag 06YU”. References: SGA 6 I (5.2), “finite flat amplitude”; SGA 4½ Rapport (4.5), “sheaf case, finite”.

An object of D(O_X) has finite Tor dimension when it has Tor amplitude in some interval [a, b].

abbrev HasFiniteTorDimension (X : RingedSpace.{u, u}) [HasDerivedCategory.{d} (OXMod.{u} X)]
    (E : DerivedCategory (OXMod.{u} X)) : Prop

Stacks.Cohomology.TorAmplitude.HasTorDimensionLE, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/TorAmplitude/OnARingedSpace.lean, line 134. The attribute's comment: “tor dimension of a module, at the derived tensor product of Tag 06YU”. References: SGA 4½ Rapport (4.5), “sheaf module case”; SGA 4 XVII (4.1.9), “ringed space, module”.

An O_X-module F has Tor dimension at most n when F[0], viewed in D(O_X), has Tor amplitude in [-n, 0].

def HasTorDimensionLE (X : RingedSpace.{u, u}) [HasDerivedCategory.{d} (OXMod.{u} X)]
    (F : OXMod.{u} X) (n : ℤ) : Prop

Stacks.Cohomology.TorAmplitude.LocallyHasFiniteTorDimension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/TorAmplitude/OnARingedSpace.lean, line 165. The attribute's comment: “locally finite tor dimension, at the Tag 06YU tensor on each open subspace”.

An object of D(O_X) locally has finite Tor dimension when its restriction to each member of some open cover has finite Tor dimension.

def LocallyHasFiniteTorDimension (X : RingedSpace.{u, u})
    [HasDerivedCategory.{d} (OXMod.{u} X)]
    [∀ U : Opens X.carrier,
      HasDerivedCategory.{d'} (OXMod.{u} (X.restrict U.isOpenEmbedding))]
    (E : DerivedCategory (OXMod.{u} X)) : Prop

Tag 08CH, a lemma

Tag 08CH in the Stacks Project.

Stacks.Cohomology.TorAmplitude.FlatCokernel.isFlat_cokernel_of_hasTorAmplitude, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/TorAmplitude/FlatCokernel.lean, line 203.

Tag 08CH. The cokernel of the differential into the lowest degree of the Tor-amplitude interval of a bounded above complex of flat O_X-modules is a flat O_X-module.

The complex is K-flat by Tag 06YQ, so the Tor-amplitude hypothesis makes the three-term complex K^{a-2} ⊗ F ⟶ K^{a-1} ⊗ F ⟶ K^a ⊗ F exact for every O_X-module F. Hence Coker(d^{a-1}) ⊗ - preserves monomorphisms, and being right exact as well it is exact.

theorem isFlat_cokernel_of_hasTorAmplitude
    (K : CochainComplex (Modules X) ℤ) (a b : ℤ)
    (hbound : ∃ n : ℤ, K.IsStrictlyLE n)
    (hflat : ∀ i : ℤ,
      AlgebraicGeometry.SheafOfModules.IsFlat.{u, u, u, u} (O := X.sheaf) (K.X i))
    (hamp : Stacks.Cohomology.TorAmplitude.HasTorAmplitude X (DerivedCategory.Q.obj K) a b) :
    AlgebraicGeometry.SheafOfModules.IsFlat.{u, u, u, u} (O := X.sheaf)
      (cokernel (K.d (a - 1) a))

Tag 08CI, a lemma

Tag 08CI in the Stacks Project.

Stacks.Cohomology.TorAmplitude.BoundedFlatRepresentative.hasTorAmplitude_iff_exists_flat_representative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/TorAmplitude/BoundedFlatRepresentative.lean, line 280. References: SGA 4 XVII (4.1.9), “(i), (iii)”; SGA 6 I (5.1), “ringed space case”.

An object of D(O_X) has Tor amplitude in [a, b] exactly when some complex of flat O_X-modules vanishing in every degree outside [a, b] represents it.

theorem hasTorAmplitude_iff_exists_flat_representative (E : DerivedCategory (Modules X))
    (a b : ℤ) (hab : a ≤ b) :
    Stacks.Cohomology.TorAmplitude.HasTorAmplitude X E a b ↔
      ∃ K : CochainComplex (Modules X) ℤ,
        (∀ i : ℤ, AlgebraicGeometry.SheafOfModules.IsFlat.{u, u, u, u}
          (O := X.sheaf) (K.X i)) ∧
        (∀ i : ℤ, i ∉ Set.Icc a b → IsZero (K.X i)) ∧
        Nonempty (DerivedCategory.Q.obj K ≅ E)

Tag 09U8, a lemma

Tag 09U8 in the Stacks Project.

Stacks.Cohomology.TorAmplitude.Pullback.hasTorAmplitude_derivedPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/TorAmplitude/DerivedPullback.lean, line 96.

Tag 09U8. Derived pullback along a morphism of ringed spaces preserves Tor amplitude in a fixed interval.

A degenerate interval is replaced by a one-point interval above the degree under consideration, which is weaker, and hasTorAmplitude_derivedPullback_of_le applies.

theorem hasTorAmplitude_derivedPullback (E : DerivedCategory (OXMod.{u} Y)) (a b : ℤ)
    (hE : HasTorAmplitude Y E a b) :
    HasTorAmplitude X
      ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback f).obj E) a b

Tag 09U9, a lemma

Tag 09U9 in the Stacks Project.

Stacks.Cohomology.TorAmplitude.hasTorAmplitude_iff_forall_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/TorAmplitude/DerivedTensorStalk.lean, line 465. The attribute's comment: “Tor amplitude in [a, b] on a ringed space holds exactly when it holds at every stalk, for the derived tensor product of Stacks 06YU on D(O_X) and the canonical derived tensor product of Stacks 0BYI over each stalk ring; the derived form of Stacks 01CB that the source proof cites is derivedTensorStalkIso in this file.”. References: SGA 6 I (5.6.2), “ringed space case”; SGA 4 XVII (4.2.8), “clause (iii)”.

Stacks 09U9. Let (X, 𝒪_X) be a ringed space and E an object of D(𝒪_X). Then E has Tor amplitude in [a, b] if and only if, for every point x of X, the stalk E_x has Tor amplitude in [a, b] as an object of D(𝒪_{X, x}).

Both sides are read against the derived tensor product and against nothing else: Stacks.Cohomology.TorAmplitude.HasTorAmplitude is the Stacks 08CG predicate at Stacks.Cohomology.TorAmplitude.derTensor, the derived tensor product of Stacks 06YU on D(𝒪_X), and the stalk side is the Stacks 08CG predicate at Stacks.SheafOfModules.DerivedTensorStalk.stalkDerivedTensor, the canonical derived tensor product of Stacks 0BYI over the stalk ring. What the Stacks proof cites — Stacks 01CB and exactness of stalks — is Stacks.SheafOfModules.DerivedTensorStalk.derivedTensorStalkIso.

The two steps are both Iffs of the same proposition read in two vocabularies: AlgebraicGeometry.RingedSpace.hasTorAmplitudeIn_canonicalCertified_iff says the Stacks 08CG predicate at the canonical derived tensor product is this one, and AlgebraicGeometry.RingedSpace.hasTorAmplitudeIn_canonicalCertified_iff_forall_stalk is Stacks.SheafOfModules.DerivedTensorStalk.hasTorAmplitudeIn_canonical_iff_forall_stalk, the stalkwise criterion, at that derived tensor product.

AlgebraicGeometry.SheafOfModules.hasTorAmplitudeIn_iff_forall_stalk is the engine: the same equivalence for derived tensor products supplied as bare bifunctors on D(𝒪_X) and on each D(𝒪_{X, x}), together with the isomorphism identifying them on stalks.

theorem hasTorAmplitude_iff_forall_stalk
    (E : DerivedCategory (OXMod.{u, u} X)) (a b : ℤ) :
    HasTorAmplitude X E a b ↔
      ∀ x : X.carrier, CategoryTheory.DerivedCategory.HasTorAmplitudeIn
        (Stacks.SheafOfModules.DerivedTensorStalk.stalkDerivedTensor X.sheaf x)
        ((AlgebraicGeometry.SheafOfModules.stalkFunctor (structureSheafOfRings X) x
          ).mapDerivedCategory.obj E) a b

Stacks.Cohomology.TorAmplitude.hasTorAmplitude_iff_forall_hasTorAmplitudeCanonical_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/TorAmplitude/StalkwiseCriterion.lean, line 87. References: SGA 4 XVII (4.2.8), “(iii), special case”.

Stacks 09U9. Let (X, 𝒪_X) be a ringed space and E an object of D(𝒪_X). Then E has Tor amplitude in [a, b] if and only if, for every point x of X, the stalk E_x has Tor amplitude in [a, b] as an object of D(𝒪_{X, x}).

The left side is the Tor amplitude of Stacks 08CG for the derived tensor product of Stacks 06YU, Stacks.Cohomology.TorAmplitude.HasTorAmplitude; the right side is the Tor amplitude of Stacks 0652 over the ring 𝒪_{X, x} for its derived tensor product of Stacks 0BYI, StacksDraft.TorAmplitude.HasTorAmplitudeCanonical. The stalk E_x is the image of E under the exact stalk functor Mod(𝒪_X) ⥤ Mod(𝒪_{X, x}).

theorem hasTorAmplitude_iff_forall_hasTorAmplitudeCanonical_stalk
    (E : DerivedCategory (OXMod.{u, u} X)) (a b : ℤ) :
    HasTorAmplitude X E a b ↔
      ∀ x : X.carrier, StacksDraft.TorAmplitude.HasTorAmplitudeCanonical
        (TopCat.Presheaf.stalk (C := RingCat.{u}) (X.presheaf ⋙ forget₂ CommRingCat RingCat) x)
        ((SheafOfModules.stalkFunctor (structureSheafOfRings X) x).mapDerivedCategory.obj E)
        a b

Tag 08CJ, a lemma

Tag 08CJ in the Stacks Project.

Stacks.Cohomology.TorAmplitude.FlatOpcycles.hasTorAmplitude_obj₃, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/TwoTermResolution.lean, line 143. The attribute's comment: “(1), at the ringed-space Tor-amplitude predicate”.

Tag 08CJ (1) at the ringed-space Tor-amplitude predicate. In a distinguished triangle K ⟶ L ⟶ M ⟶ K[1] of D(O_X), if K has Tor amplitude in [a + 1, b + 1] and L has Tor amplitude in [a, b], then M has Tor amplitude in [a, b].

This is TorAmplitude.hasTorAmplitude_obj₃ read through Stacks.Cohomology.TorAmplitude.FlatOpcycles.tensorSingleFunctor, exactly as Stacks.Cohomology.TorAmplitude.FlatOpcycles.hasTorAmplitude_obj₁ reads part (3) through it; the only content is the translation between the two encodings of "outside [a, b]".

theorem hasTorAmplitude_obj₃
    (T : Triangle (DerivedCategory (RingedSpace.KFlatDerivedPullback.Modules X)))
    (hT : T ∈ distinguishedTriangles) (a b : ℤ)
    (hK : Stacks.Cohomology.TorAmplitude.HasTorAmplitude X T.obj₁ (a + 1) (b + 1))
    (hL : Stacks.Cohomology.TorAmplitude.HasTorAmplitude X T.obj₂ a b) :
    Stacks.Cohomology.TorAmplitude.HasTorAmplitude X T.obj₃ a b

Stacks.Cohomology.TorAmplitude.FlatOpcycles.hasTorAmplitude_obj₂, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/TorAmplitude/MiddleTwoOutOfThree.lean, line 67. The attribute's comment: “(2), at the ringed-space Tor-amplitude predicate”.

[Stacks, Tag 08CJ] (2) at the ringed-space Tor-amplitude predicate. In a distinguished triangle K ⟶ L ⟶ M ⟶ K[1] of D(O_X), if K has Tor amplitude in [a, b] and M has Tor amplitude in [a, b], then L has Tor amplitude in [a, b].

This is TorAmplitude.hasTorAmplitude_obj₂ read through tensorSingleFunctor; the only content is the translation between the two encodings of "outside [a, b]".

theorem hasTorAmplitude_obj₂ (T : Triangle (DerivedCategory (Modules X)))
    (hT : T ∈ distinguishedTriangles) (a b : ℤ)
    (hK : Stacks.Cohomology.TorAmplitude.HasTorAmplitude X T.obj₁ a b)
    (hM : Stacks.Cohomology.TorAmplitude.HasTorAmplitude X T.obj₃ a b) :
    Stacks.Cohomology.TorAmplitude.HasTorAmplitude X T.obj₂ a b

TorAmplitude.hasTorAmplitude_obj₃, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/TorAmplitude/Triangles.lean, line 91. The attribute's comment: “(1)”. References: SGA 6 I (5.3), “partial”; SGA 6 III (3.2), “Triangulatedness clause”.

Stacks Tag 08CJ (1): in a distinguished triangle K → L → M → K[1], if K has tor-amplitude in [a+1, b+1] and L has tor-amplitude in [a, b], then M has tor-amplitude in [a, b].

theorem hasTorAmplitude_obj₃ (T : Triangle (DerivedCategory M))
    (hT : T ∈ distinguishedTriangles) (a b : ℤ)
    (hK : HasTorAmplitude derTensor T.obj₁ (a + 1) (b + 1))
    (hL : HasTorAmplitude derTensor T.obj₂ a b) :
    HasTorAmplitude derTensor T.obj₃ a b

TorAmplitude.hasTorAmplitude_obj₂, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/TorAmplitude/Triangles.lean, line 114. The attribute's comment: “(2)”. References: SGA 6 I (5.3), “partial”; SGA 6 III (3.2), “Triangulatedness clause”.

Stacks Tag 08CJ (2): in a distinguished triangle K → L → M → K[1], if K and M both have tor-amplitude in [a, b], then L has tor-amplitude in [a, b].

theorem hasTorAmplitude_obj₂ (T : Triangle (DerivedCategory M))
    (hT : T ∈ distinguishedTriangles) (a b : ℤ)
    (hK : HasTorAmplitude derTensor T.obj₁ a b)
    (hM : HasTorAmplitude derTensor T.obj₃ a b) :
    HasTorAmplitude derTensor T.obj₂ a b

TorAmplitude.hasTorAmplitude_obj₁, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/TorAmplitude/Triangles.lean, line 137. The attribute's comment: “(3)”. References: SGA 6 I (5.3), “partial”; SGA 6 III (3.2), “Triangulatedness clause”.

Stacks Tag 08CJ (3): in a distinguished triangle K → L → M → K[1], if L has tor-amplitude in [a+1, b+1] and M has tor-amplitude in [a, b], then K has tor-amplitude in [a+1, b+1].

theorem hasTorAmplitude_obj₁ (T : Triangle (DerivedCategory M))
    (hT : T ∈ distinguishedTriangles) (a b : ℤ)
    (hL : HasTorAmplitude derTensor T.obj₂ (a + 1) (b + 1))
    (hM : HasTorAmplitude derTensor T.obj₃ a b) :
    HasTorAmplitude derTensor T.obj₁ (a + 1) (b + 1)

Tag 09J4, a lemma

Tag 09J4 in the Stacks Project.

Stacks.Cohomology.TorAmplitude.Tensor.hasTorAmplitude_derivedTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/TorAmplitude/TensorProduct.lean, line 157.

If K has Tor amplitude in [a, b] and L has Tor amplitude in [c, d], then K ⊗^L_{O_X} L has Tor amplitude in [a + c, b + d].

theorem hasTorAmplitude_derivedTensor (K L : DerivedCategory (Modules X)) (a b c d : ℤ)
    (hK : HasTorAmplitude X K a b)
    (hL : HasTorAmplitude X L c d) :
    HasTorAmplitude X
      (((derTensor X).tensor.obj K).obj L) (a + c) (b + d)

Tag 08CK, a lemma

Tag 08CK in the Stacks Project.

Stacks.Cohomology.TorAmplitude.hasTorAmplitude_biprod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/TorAmplitude/BiproductSum.lean, line 68. The attribute's comment: “from the summands to the sum, at the ringed-space Tor-amplitude predicate”.

[Stacks, Tag 08CK], from the summands to the sum. If K and L have Tor amplitude in [a, b] then so does K ⊞ L.

The split triangle K ⟶ K ⊞ L ⟶ L ⟶ K⟦1⟧ is distinguished, so this is clause (2) of [Stacks, Tag 08CJ].

theorem hasTorAmplitude_biprod (a b : ℤ) (K L : DerivedCategory (OXMod.{u, u} X))
    (hK : HasTorAmplitude X K a b) (hL : HasTorAmplitude X L a b) :
    HasTorAmplitude X (K ⊞ L) a b

Stacks.Cohomology.TorAmplitude.hasFiniteTorDimension_biprod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/TorAmplitude/BiproductSum.lean, line 78. The attribute's comment: “finite Tor dimension, from the summands to the sum”.

Finite Tor dimension passes from two summands to their sum. The two intervals are merged.

theorem hasFiniteTorDimension_biprod (K L : DerivedCategory (OXMod.{u, u} X))
    (hK : HasFiniteTorDimension X K) (hL : HasFiniteTorDimension X L) :
    HasFiniteTorDimension X (K ⊞ L)

Stacks.TorAmplitude.hasTorAmplitude_of_biprod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/TorAmplitude/Defs.lean, line 189.

Statement 1 (Tag 08CK / Lemma 20.48.8). Let (X, 𝒪_X) be a ringed space and a ≤ b. We work with THE derived tensor product - ⊗^L_{𝒪_X} - on D(𝒪_X): it is given as a bifunctor derivedTensor whose flips - ⊗^L F = derivedTensor.flip.obj (single F) are, together with the comparison natural transformation derivedTensorComparison F, the total left derived functors (IsLeftDerivedFunctor) of the underived tensor products - ⊗ F. This universal property determines derivedTensor up to canonical isomorphism, so it is genuinely the derived tensor product (introduced here as hypotheses rather than as axioms).

If the direct sum K ⊕ L (categorical biproduct K ⊞ L) has tor-amplitude in [a,b], then both K and L have tor-amplitude in [a,b].

theorem hasTorAmplitude_of_biprod
    (derivedTensor : DOX X ⥤ DOX X ⥤ DOX X)
    (a b : ℤ)
    (K L : DOX X) (h : HasTorAmplitude derivedTensor a b (K ⊞ L)) :
    HasTorAmplitude derivedTensor a b K ∧ HasTorAmplitude derivedTensor a b L

Sources

• Section 20.48, Tag 08CF
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.RingedSpace.CertifiedDerivedSheafTensoring.HasTorAmplitudeIn · AlgebraicGeometry.RingedSpace.CertifiedDerivedSheafTensoring.HasFiniteTorDimension · AlgebraicGeometry.RingedSpace.CertifiedDerivedSheafTensoring.HasTorDimensionLE · AlgebraicGeometry.RingedSpace.LocallyHasFiniteTorDimension · CategoryTheory.DerivedCategory.HasTorAmplitudeIn · Stacks.Cohomology.TorAmplitude.HasTorAmplitude · Stacks.Cohomology.TorAmplitude.HasFiniteTorDimension · Stacks.Cohomology.TorAmplitude.HasTorDimensionLE

Section20.49 Perfect complexes#

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

Tag 08CM, a definition

Tag 08CM in the Stacks Project.

Stacks.Cohomology.PerfectComplexes.IsPerfectComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PerfectComplexes/Defs.lean, line 59. The attribute's comment: “perfect complexes”.

A complex is perfect if an open cover admits strictly perfect complexes mapping to its restrictions by quasi-isomorphisms.

def IsPerfectComplex {X : RingedSpace.{u, v}}
    (E : CochainComplex (OXMod.{u, v} X) ℤ) : Prop

Stacks.Cohomology.PerfectComplexes.IsPerfect, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PerfectComplexes/Defs.lean, line 82. The attribute's comment: “perfect derived-category objects”.

An object of the derived category is perfect if represented by a perfect complex.

def IsPerfect {X : RingedSpace.{u, v}}
    [HasDerivedCategory.{d} (OXMod.{u, v} X)]
    (K : DerivedCategory (OXMod.{u, v} X)) : Prop

Tag 08CN, a lemma

Tag 08CN in the Stacks Project.

AlgebraicGeometry.RingedSpace.isPerfect_of_strictlyPerfect_local_models, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PerfectComplexes/LocalCriterion.lean, line 59. The attribute's comment: “local_criterion”.

An object of the derived category of 𝒪_X-modules which is, on an open covering of X, isomorphic in the derived category to a strictly perfect complex is perfect.

The hypothesis fixes a complex F representing the object, and asks the local strictly perfect models to be isomorphic, in the derived categories of the members of the covering, to the restrictions of F.

theorem isPerfect_of_strictlyPerfect_local_models (X : RingedSpace.{u, u})
    [HasDerivedCategory.{d} (OXMod.{u, u} X)]
    [∀ U : Opens X.carrier, HasDerivedCategory.{d'} (OXMod.{u, u} (X.restrict U.isOpenEmbedding))]
    (K : DerivedCategory (OXMod.{u, u} X))
    (h : ∃ F : CochainComplex (OXMod.{u, u} X) ℤ,
      Nonempty (DerivedCategory.Q.obj F ≅ K) ∧
        ∃ (I : Type u) (U : I → Opens X.carrier), (⨆ i, U i) = ⊤ ∧
          ∀ i : I, ∃ P : CochainComplex
            (OXMod.{u, u} (X.restrict (U i).isOpenEmbedding)) ℤ,
            IsStrictlyPerfect P ∧
              Nonempty (DerivedCategory.Q.obj P ≅
                DerivedCategory.Q.obj (restrictComplex F (U i)))) :
    IsPerfect K

AlgebraicGeometry.RingedSpace.isPerfectComplex_of_isPerfect_representation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PerfectComplexes/RepresentativeIndependence.lean, line 55. The attribute's comment: “representative_independence”.

Stacks 08CN. Every complex representing a perfect object of the derived category of 𝒪_X-modules is itself a perfect complex.

Perfectness of K provides one perfect representative E. The isomorphism Q(E) ≅ Q(F) with the complex F at hand is a roof of quasi-isomorphisms between E and F, and perfectness of complexes is invariant under roofs.

theorem isPerfectComplex_of_isPerfect_representation
    [HasDerivedCategory.{d} (OXMod.{u, u} X)]
    {K : DerivedCategory (OXMod.{u, u} X)} (hK : IsPerfect K)
    {F : CochainComplex (OXMod.{u, u} X) ℤ}
    (hF : Nonempty (DerivedCategory.Q.obj F ≅ K)) :
    IsPerfectComplex F

Tag 0BCJ, a lemma

Tag 0BCJ in the Stacks Project.

AlgebraicGeometry.RingedSpace.isPerfect_iff_hasFiniteLocallyFreeRepresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PerfectComplexes/LocalRingStalks.lean, line 58. The attribute's comment: “perfect iff locally finite locally free”.

Stacks 0BCJ. On a ringed space whose structure-sheaf stalks are local rings, a derived object is perfect exactly when it has local bounded finite locally free representatives.

theorem isPerfect_iff_hasFiniteLocallyFreeRepresentation
    [∀ x : X.carrier, IsLocalRing (ToType (X.presheaf.stalk x))]
    [HasDerivedCategory.{d} (OXMod.{u, u} X)] (K : DerivedCategory (OXMod.{u, u} X)) :
    IsPerfect K ↔ HasFiniteLocallyFreeRepresentation K

Declarations registered for the tag:

• AlgebraicGeometry.RingedSpace.hasFiniteLocallyFreeRepresentation_iff_hasFiniteFreeRepresentation, declared in the repository, registered with add_to_stacks in StacksFrontier/Topology/Sheaves/Cohomology/PerfectComplexes/LocalRingStalks.lean, line 81 (StacksFrontier): “finite locally free iff finite free locally”.

Tag 08CP, a lemma

Tag 08CP in the Stacks Project.

Stacks.Cohomology.PerfectFromTorAmplitude.isPerfect_of_hasTorAmplitude_of_isPseudoCoherentFrom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PerfectComplexes/BoundedLocalApproximation.lean, line 191. References: SGA 6 I (5.8), “(ii) ⟹ (i)”.

Tag 08CP. An object of D(O_X) on a ringed space with Tor amplitude in [a, b], for integers a ≤ b, which is (a - 1)-pseudo-coherent, is perfect.

The pseudo-coherence supplies a representative C and, near every point, a strictly perfect approximation of C|_U in degrees above a - 1 with no terms above b; its brutal truncation σ^{≥a-1}P is concentrated in [a-1, b] and still approximates above a - 1, and the Tor-amplitude hypothesis makes the degree-a opcycles of that truncation flat, hence locally a direct summand of a finite free module. That is what the truncation criterion consumes.

theorem isPerfect_of_hasTorAmplitude_of_isPseudoCoherentFrom
    (E : DerivedCategory (OXMod.{u, u} X)) (a b : ℤ) (hab : a ≤ b)
    (hamp : Stacks.Cohomology.TorAmplitude.HasTorAmplitude X E a b)
    (hpc : AlgebraicGeometry.RingedSpace.IsPseudoCoherentFrom E (a - 1)) :
    Stacks.Cohomology.PerfectComplexes.IsPerfect E

Tag 08CQ, a lemma

Tag 08CQ in the Stacks Project.

Stacks.Cohomology.TorAmplitude.isPseudoCoherent_and_locallyHasFiniteTorDimension_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PerfectComplexes/PseudoCoherentAndFiniteTorDimension.lean, line 218. The attribute's comment: “(1) implies (2)”. References: SGA 6 I (5.8.1), “necessity”; SGA 6 I (8.5), “special case”.

Tag 08CQ, the forward implication. A perfect object of D(O_X) is pseudo-coherent and locally has finite Tor dimension.

theorem isPseudoCoherent_and_locallyHasFiniteTorDimension_of_isPerfect
    (E : DerivedCategory (OXMod.{u} X)) (hE : Stacks.Cohomology.PerfectComplexes.IsPerfect E) :
    AlgebraicGeometry.RingedSpace.PseudoCoherence.IsPseudoCoherent (X := X) E ∧
      LocallyHasFiniteTorDimension X E

Stacks.Cohomology.TorAmplitude.isPerfect_of_isPseudoCoherent_of_locallyHasFiniteTorDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PerfectComplexes/PseudoCoherentAndFiniteTorDimension.lean, line 253. The attribute's comment: “(2) implies (1)”. References: SGA 6 I (5.8.1), “sufficiency”.

Tag 08CQ, the converse implication. A pseudo-coherent object of D(O_X) which locally has finite Tor dimension is perfect.

Perfectness is local on the space (Stacks.Cohomology.PerfectComplexTriangles.isPerfect_of_local_isPerfect), which is what makes the per-member Tor-amplitude intervals of LocallyHasFiniteTorDimension usable: over a member U of the cover witnessing finite Tor dimension there is a single interval [a, b], and the restriction of E to X|_U is still pseudo-coherent, hence (a-1)-pseudo-coherent, so Tag 08CP applies there. The interval is widened to [min a b, max a b] so that it is nonempty, which Tag 08CP requires.

theorem isPerfect_of_isPseudoCoherent_of_locallyHasFiniteTorDimension
    (E : DerivedCategory (OXMod.{u} X))
    (hpc : AlgebraicGeometry.RingedSpace.PseudoCoherence.IsPseudoCoherent (X := X) E)
    (htor : LocallyHasFiniteTorDimension X E) :
    Stacks.Cohomology.PerfectComplexes.IsPerfect E

Tag 09UA, a lemma

Tag 09UA in the Stacks Project.

AlgebraicGeometry.RingedSpace.KFlatDerivedPullback.isPerfect_derivedPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PerfectComplexes/PerfectDerivedPullback.lean, line 167.

The derived pullback of a perfect object of D(𝒪_Y) is a perfect object of D(𝒪_X), for any models of the two derived categories.

A representative K of the given object is resolved by a K-flat complex P (Tag 06YS); P is again a perfect complex, being quasi-isomorphic to K, and Lf^* of the object is the class of the degreewise pullback f^*P, which is perfect by AlgebraicGeometry.RingedSpace.KFlatDerivedPullback.isPerfectComplex_modulePullback.

theorem isPerfect_derivedPullback {X Y : RingedSpace.{u, u}} (f : X ⟶ Y)
    [hX : HasDerivedCategory.{w₁} (SheafOfModules.{u} (structureSheafRing X))]
    [hY : HasDerivedCategory.{w₂} (SheafOfModules.{u} (structureSheafRing Y))]
    (E : DerivedCategory (SheafOfModules.{u} (structureSheafRing Y)))
    (hE : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := Y) E) :
    Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X)
      ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback f).obj E)

Tag 08CR, a lemma

Tag 08CR in the Stacks Project.

Stacks.Cohomology.PerfectComplexTriangles.isPerfect_obj₃_of_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PerfectComplexes/Triangles.lean, line 239. The attribute's comment: “third object”.

Tag 08CR, third object. The third object of a distinguished triangle is perfect if the first two are. With perfect complexes E₁, E₂ representing the first two vertices, the third vertex is Q of the mapping cone of a chain map γ : E₁ ⟶ G with E₂ ⟶ G a quasi-isomorphism (Stacks.Cohomology.PerfectComplexTriangles.exists_mappingCone_iso_obj₃); G is perfect along with E₂, and the mapping cone of a morphism of perfect complexes is perfect (AlgebraicGeometry.RingedSpace.isPerfectComplex_mappingCone).

theorem isPerfect_obj₃_of_distinguished [HasDerivedCategory.{d} (OXMod.{u} X)]
  (T : Triangle (DerivedCategory (OXMod.{u} X))) (hT : T ∈ distinguishedTriangles)
  (h₁ : Stacks.Cohomology.PerfectComplexes.IsPerfect T.obj₁) (h₂ :
    Stacks.Cohomology.PerfectComplexes.IsPerfect T.obj₂) :
  Stacks.Cohomology.PerfectComplexes.IsPerfect T.obj₃

Stacks.Cohomology.PerfectComplexTriangles.isPerfect_obj₂_of_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PerfectComplexes/Triangles.lean, line 253. The attribute's comment: “second object”.

Tag 08CR, second object.

theorem isPerfect_obj₂_of_distinguished [HasDerivedCategory.{d} (OXMod.{u} X)]
  (T : Triangle (DerivedCategory (OXMod.{u} X))) (hT : T ∈ distinguishedTriangles)
  (h₁ : Stacks.Cohomology.PerfectComplexes.IsPerfect T.obj₁) (h₃ :
    Stacks.Cohomology.PerfectComplexes.IsPerfect T.obj₃) :
  Stacks.Cohomology.PerfectComplexes.IsPerfect T.obj₂

Stacks.Cohomology.PerfectComplexTriangles.isPerfect_obj₁_of_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PerfectComplexes/Triangles.lean, line 263. The attribute's comment: “first object”.

Tag 08CR, first object.

theorem isPerfect_obj₁_of_distinguished [HasDerivedCategory.{d} (OXMod.{u} X)]
  (T : Triangle (DerivedCategory (OXMod.{u} X))) (hT : T ∈ distinguishedTriangles)
  (h₂ : Stacks.Cohomology.PerfectComplexes.IsPerfect T.obj₂) (h₃ :
    Stacks.Cohomology.PerfectComplexes.IsPerfect T.obj₃) :
  Stacks.Cohomology.PerfectComplexes.IsPerfect T.obj₁

Tag 09J5, a lemma

Tag 09J5 in the Stacks Project.

AlgebraicGeometry.RingedSpace.isPerfect_derivedTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PerfectComplexes/DerivedTensorDatumBridge.lean, line 96. The attribute's comment: “at the derived tensor product of the internal Hom development”.

On a ringed space the derived tensor product Stacks.SheafOfModules.derivedTensor takes a pair of perfect objects of D(O_X) to a perfect object.

theorem isPerfect_derivedTensor
    (K L : DerivedCategory (StructureSheafModules X.sheaf))
    (hK : IsPerfect (X := X) K)
    (hL : IsPerfect (X := X) L) :
    IsPerfect (X := X)
      (((derivedTensor X.sheaf).obj K).obj L)

AlgebraicGeometry.RingedSpace.isPerfect_derivedTensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PerfectComplexes/TensorProduct.lean, line 163. References: SGA 6 I (4.19), “single ringed space”; SGA 6 0 (4.2), “more general”.

The derived tensor product of two perfect objects of D(𝒪_X) is perfect.

Represent the objects by perfect complexes E and F, and replace F by a K-flat resolution B, which is perfect as well. The derived tensor product is then the class of the total tensor complex Tot(E ⊗_{𝒪_X} B), which is perfect by AlgebraicGeometry.RingedSpace.isPerfectComplex_tensorComplex.

Stated for an arbitrary derived tensor product, since only its comparisonRight field is used.

theorem isPerfect_derivedTensorProduct
    (T : Stacks.DerivedTensor.RingedSite.DerivedTensorProduct X.sheaf)
    (K L : DerivedCategory (OXMod.{u, u} X)) (hK : IsPerfect K) (hL : IsPerfect L) :
    IsPerfect ((T.tensor.obj K).obj L)

Tag 08CS, a lemma

Tag 08CS in the Stacks Project.

Stacks.Cohomology.TorAmplitude.isPerfect_of_biprod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PerfectComplexes/PseudoCoherentAndFiniteTorDimension.lean, line 296.

Tag 08CS. If a binary biproduct in D(O_X) is perfect, then so are both of its summands.

By Tag 08CQ the biproduct is pseudo-coherent and locally of finite Tor dimension; both properties pass to the summands, pseudo-coherence by Tag 08CE and locally finite Tor dimension by Tag 08CK; and Tag 08CQ turns the pair back into perfectness of each summand.

theorem isPerfect_of_biprod (K L : DerivedCategory (OXMod.{u} X))
    (h : Stacks.Cohomology.PerfectComplexes.IsPerfect (K ⊞ L)) :
    Stacks.Cohomology.PerfectComplexes.IsPerfect K ∧
      Stacks.Cohomology.PerfectComplexes.IsPerfect L

Tag 08DP, a lemma

Tag 08DP in the Stacks Project.

Stacks.Cohomology.ClosedSupportPerfect.isPerfect_derivedPushforward_of_closedSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PerfectComplexes/ClosedSupportPerfect.lean, line 635.

Stacks 08DP. The derived pushforward of a perfect object on an open subspace is perfect if its cohomology is supported on a subset closed in the ambient space.

theorem isPerfect_derivedPushforward_of_closedSupport
    (X : RingedSpace.{u, u}) (U : Opens X) (T : Set (X.restrict U.isOpenEmbedding).carrier)
    (hT : IsClosed ((X.ofRestrict U.isOpenEmbedding).hom.base '' T))
    (Rj : DerivedCategory (SheafOfModules.{u} (structureSheafRing
      (X.restrict U.isOpenEmbedding))) ⥤
      DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (αj : (modulePushforward (X.ofRestrict U.isOpenEmbedding)).mapHomotopyCategory
        (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rj)
    [hRj : Rj.IsRightDerivedFunctor αj
      (HomotopyCategory.quasiIso _ (ComplexShape.up ℤ))]
    (E : DerivedCategory (SheafOfModules.{u} (structureSheafRing
      (X.restrict U.isOpenEmbedding))))
    (hE : RingedSpace.IsPerfect (X := X.restrict U.isOpenEmbedding) E)
    (hET : CohomologySupportedOn
      (structureSheafRing (X.restrict U.isOpenEmbedding)) T E) :
    RingedSpace.IsPerfect (X := X) (Rj.obj E)

Tag 0GT1, a lemma

Tag 0GT1 in the Stacks Project.

AlgebraicGeometry.RingedSpace.cohomologyFiniteFreeLocus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PerfectComplexes/CohomologyFiniteFreeLocus.lean, line 161. The attribute's comment: “the locus”.

The finite free cohomology locus of a derived object. These are the points at which every cohomology stalk H^i(E)_x is a finite free 𝒪_{X, x}-module.

def cohomologyFiniteFreeLocus [HasDerivedCategory.{d} (OXMod.{u, u} X)]
    (E : DerivedCategory (OXMod.{u, u} X)) : Set X.carrier

AlgebraicGeometry.RingedSpace.subset_cohomologyFiniteFreeLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PerfectComplexes/CohomologyFiniteFreeLocus.lean, line 188. The attribute's comment: “maximality of the locus”.

Stacks 0GT1, maximality. Every open set over which all the cohomology sheaves of a derived object are finite locally free is contained in the finite free cohomology locus: finite local freeness near a point makes the cohomology stalks there finite free.

theorem subset_cohomologyFiniteFreeLocus [HasDerivedCategory.{d} (OXMod.{u, u} X)]
    (E : DerivedCategory (OXMod.{u, u} X)) (V : Opens X.carrier)
    (hV : ∀ i : ℤ, IsFiniteLocallyFreeOver
      ((DerivedCategory.homologyFunctor (OXMod.{u, u} X) i).obj E) V) :
    (V : Set X.carrier) ⊆ cohomologyFiniteFreeLocus E

AlgebraicGeometry.RingedSpace.isOpen_cohomologyFiniteFreeLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PerfectComplexes/CohomologyFiniteFreeLocus.lean, line 698. The attribute's comment: “openness of the locus”.

Stacks 0GT1, openness. On a ringed space whose structure-sheaf stalks are local rings, the finite free cohomology locus of a perfect object of the derived category of 𝒪_X-modules is open: near a point of the locus the object is computed by a strictly perfect complex, whose opcycles are then free on a neighbourhood, and over such a neighbourhood all the cohomology stalks are again finite free.

theorem isOpen_cohomologyFiniteFreeLocus
    [hloc : ∀ x : X.carrier, IsLocalRing (ToType (X.presheaf.stalk x))]
    [HasDerivedCategory.{d} (OXMod.{u, u} X)] (E : DerivedCategory (OXMod.{u, u} X))
    (hE : IsPerfect E) : IsOpen (cohomologyFiniteFreeLocus E)

Stacks.Cohomology.PerfectComplexes.cohomologyFiniteFreeLocus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PerfectComplexes/FiniteFreeLocus/Locus.lean, line 130. The attribute's comment: “the locus”.

The set of points at which every cohomology sheaf of an object of D(𝒪_X) has a finite free stalk.

def cohomologyFiniteFreeLocus {X : RingedSpace.{u, v}}
    [HasDerivedCategory.{d} (OXMod.{u, v} X)]
    (E : DerivedCategory (OXMod.{u, v} X)) : Set X

Stacks.Cohomology.PerfectComplexes.isOpen_cohomologyFiniteFreeLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PerfectComplexes/FiniteFreeLocus/Openness.lean, line 719. The attribute's comment: “openness”.

The locus where all cohomology stalks of a perfect object are finite free is open.

theorem isOpen_cohomologyFiniteFreeLocus
    {X : RingedSpace.{u, v}}
    [∀ x : X, IsLocalRing (structureSheafStalk X x)]
    [HasDerivedCategory.{d} (OXMod.{u, v} X)]
    (E : DerivedCategory (OXMod.{u, v} X)) (hE : IsPerfect E) :
    IsOpen (cohomologyFiniteFreeLocus E)

Stacks.Cohomology.PerfectComplexes.isFiniteLocallyFree_homology_restrict_locus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PerfectComplexes/FiniteFreeLocus/Openness.lean, line 747. The attribute's comment: “finite locally free”.

On the finite free locus of a perfect object every cohomology sheaf is finite locally free.

theorem isFiniteLocallyFree_homology_restrict_locus
    {X : RingedSpace.{u, v}}
    [∀ x : X, IsLocalRing (structureSheafStalk X x)]
    [HasDerivedCategory.{d} (OXMod.{u, v} X)]
    (E : DerivedCategory (OXMod.{u, v} X)) (hE : IsPerfect E)
    (i : ℤ) :
    IsFiniteLocallyFree
      ((restrictModules X
        ⟨cohomologyFiniteFreeLocus E,
          isOpen_cohomologyFiniteFreeLocus E hE⟩).obj
        ((DerivedCategory.homologyFunctor (OXMod.{u, v} X) i).obj E))

Stacks.Cohomology.PerfectComplexes.le_cohomologyFiniteFreeLocus_of_isFiniteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PerfectComplexes/FiniteFreeLocus/Openness.lean, line 771. The attribute's comment: “maximality”.

An open set on which all cohomology sheaves of a perfect object are finite locally free is contained in its finite free locus; together with the previous result this says the locus is the largest such open set.

theorem le_cohomologyFiniteFreeLocus_of_isFiniteLocallyFree
    {X : RingedSpace.{u, v}}
    [∀ x : X, IsLocalRing (structureSheafStalk X x)]
    [HasDerivedCategory.{d} (OXMod.{u, v} X)]
    (E : DerivedCategory (OXMod.{u, v} X)) (hE : IsPerfect E)
    (V : Opens X)
    (hV : ∀ i : ℤ, IsFiniteLocallyFree
      ((restrictModules X V).obj
        ((DerivedCategory.homologyFunctor (OXMod.{u, v} X) i).obj E))) :
    V ≤ ⟨cohomologyFiniteFreeLocus E,
      isOpen_cohomologyFiniteFreeLocus E hE⟩

Sources

• Section 20.49, Tag 08CL
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Cohomology.PerfectComplexes.IsPerfectComplex · Stacks.Cohomology.PerfectComplexes.IsPerfect · AlgebraicGeometry.RingedSpace.isPerfect_of_strictlyPerfect_local_models · AlgebraicGeometry.RingedSpace.isPerfectComplex_of_isPerfect_representation · AlgebraicGeometry.RingedSpace.isPerfect_iff_hasFiniteLocallyFreeRepresentation · AlgebraicGeometry.RingedSpace.hasFiniteLocallyFreeRepresentation_iff_hasFiniteFreeRepresentation · Stacks.Cohomology.PerfectFromTorAmplitude.isPerfect_of_hasTorAmplitude_of_isPseudoCoherentFrom · Stacks.Cohomology.TorAmplitude.isPseudoCoherent_and_locallyHasFiniteTorDimension_of_isPerfect

Section20.50 Duals#

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

Tag 0FP8, a lemma

Tag 0FP8 in the Stacks Project.

Stacks.Cohomology.MonoidalComplexes.symmetricMonoidalComplexes, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/MonoidalStructure.lean, line 79. References: EGA 0 (4.1.5), “partial”.

Complexes of modules on a ringed space form a symmetric monoidal category; its tensor bifunctor is the total complex of the sheafified degreewise tensor product and its unit is the structure sheaf in degree zero. This is Tag 0FPQ at the ringed site of opens of X.

public def symmetricMonoidalComplexes :
    Stacks.Cohomology.MonoidalComplexesOfModules.SymmetricMonoidalComplexes X.sheaf

Tag 0FP9, an example

Tag 0FP9 in the Stacks Project.

Stacks.SheafOfModules.OnSpace.exists_exactPairing_ihomUnit_of_isLocallyBounded, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/StrictlyPerfect/LocallyBoundedDualComplex.lean, line 162.

[Stacks, Tag 0FP9]. Let (X, 𝒪_X) be a ringed space and ℱ^• a locally bounded complex of 𝒪_X-modules each of whose terms ℱ^n is locally a direct summand of a finite free 𝒪_X-module, and let 𝒢^• = Hom^•(ℱ^•, 𝒪_X). Let ηₙ : 𝒪_X ⟶ ℱ^n ⊗ 𝒢^{-n} and εₙ : 𝒢^{-n} ⊗ ℱ^n ⟶ 𝒪_X be the coevaluation and evaluation of the duality between ℱ^n and 𝒢^{-n}. Then there is a left dual structure on 𝒢^• over ℱ^• in the monoidal category of complexes of 𝒪_X-modules whose coevaluation is η = ∑ ηₙ and whose evaluation is ε = ∑ εₙ: in degree zero, read through the identification of the degree zero term of the unit complex with 𝒪_X, the component of η on the summand ℱ^n ⊗ 𝒢^{-n} of Tot(ℱ^• ⊗ 𝒢^•)^0 is ηₙ, and the component of ε on the summand 𝒢^{-n} ⊗ ℱ^n of Tot(𝒢^• ⊗ ℱ^•)^0 is εₙ. The structure is exactPairingIhomUnitComplexOfIsLocallyBounded.

theorem exists_exactPairing_ihomUnit_of_isLocallyBounded
    (F : CochainComplex (Strict.Mod X.sheaf) ℤ)
    (hb : IsLocallyBounded X F) (hF : ∀ n : ℤ, IsLocallyFiniteFreeSummand X (F.X n)) :
    letI : MonoidalCategory (_root_.SheafOfModules.{u}
        (Stacks.SheafOfModules.Tensor.ringSheaf X.sheaf)) :=
      Stacks.SheafOfModules.Strict.monoidalCategory X.sheaf.obj
        (Stacks.SheafOfModules.Tensor.ringSheaf X.sheaf).property
    letI : MonoidalPreadditive (Strict.Mod X.sheaf) :=
      Strict.monoidalPreadditiveRingSheaf X.sheaf
    letI : ∀ X₁ X₂ : GradedObject ℤ (Strict.Mod X.sheaf), GradedObject.HasTensor X₁ X₂ :=
      fun _ _ => inferInstance
    letI := Strict.monoidalCategoryCochainComplex X.sheaf
    letI := Strict.monoidalClosedCochainComplex X.sheaf
    ∃ P : ExactPairing F ((ihom F).obj (𝟙_ (CochainComplex (Strict.Mod X.sheaf) ℤ))),
      (∀ n : ℤ, P.coevaluation'.f 0 ≫
          GradedObject.Monoidal.πTensorObj F.X
            ((ihom F).obj (𝟙_ (CochainComplex (Strict.Mod X.sheaf) ℤ))).X n (-n) 0
            (add_neg_cancel n) =
        ((HomologicalComplex.tensorUnitIso (Strict.Mod X.sheaf) (ComplexShape.up ℤ)).inv 0 ≫
            GradedObject.Monoidal.tensorUnit₀.hom) ≫
          (Strict.exactPairingIhomComplexX X.sheaf F n
            (isLocallyDirectSummandOfFiniteFree_of_isLocallyFiniteFreeSummand X (F.X n)
              (hF n))).coevaluation') ∧
      ∀ n : ℤ, HomologicalComplex.ιTensorObj
          ((ihom F).obj (𝟙_ (CochainComplex (Strict.Mod X.sheaf) ℤ))) F (-n) n 0
          (neg_add_cancel n) ≫ P.evaluation'.f 0 =
        (Strict.exactPairingIhomComplexX X.sheaf F n
            (isLocallyDirectSummandOfFiniteFree_of_isLocallyFiniteFreeSummand X (F.X n)
              (hF n))).evaluation' ≫
          GradedObject.Monoidal.tensorUnit₀.inv ≫
            (HomologicalComplex.tensorUnitIso (Strict.Mod X.sheaf) (ComplexShape.up ℤ)).hom 0

Tag 0FPA, a lemma

Tag 0FPA in the Stacks Project.

Stacks.SheafOfModules.Strict.isLocallyBounded_and_isLocallyDirectSummand_and_isoDualComplex_of_exactPairing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Duals/ComplexWithALeftDual.lean, line 106. The attribute's comment: “the WHOLE statement of the tag under the tag's OWN hypothesis, for a ringed site — of which the ringed space of the tag is a case — and over the monoidal structure on complexes of 𝒪-modules whose tensor product is the one of Tag 01CA: a complex ℱ^• with a left dual 𝒢^• is (1) locally bounded, (2) has every term a local direct summand of a finite free module, and (3) has 𝒢^• the complex of Example 0FP9, namely SheafHom^•(ℱ^•, 𝒪) — Stacks.SheafOfModules.Strict.dualComplexOfLocallyStrictlyPerfect, the dual sheaves of Tag 0FNY in the opposite degrees with the signed-transpose differential — together WITH its pairings: the isomorphism carries η and ε to the η = ∑ ηₙ and ε = ∑ εₙ that Tag 0FPR puts on that complex, so the triple (𝒢^•, η, ε) is identified with Example 0FP9's triple and not merely the underlying complexes. (3) is uniqueness of left duals (Tag 0FFR, CategoryTheory.rightDualIso) applied to the left dual Tag 0FPR builds from the local strict perfectness of Tag 0FPS, which (1) and (2) supply. The site-level analogue of the whole tag is Tag 0FPS, Stacks.SheafOfModules.Strict.exists_cover_isStrictlyPerfect_of_exactPairing for its first assertion”.

[Stacks, Tag 0FPA]. Let (C, 𝒪) be a ringed site and let ℱ^• be a complex of 𝒪-modules. If ℱ^• has a left dual 𝒢^• in the monoidal category of complexes of 𝒪-modules, then all three of the following hold.

1. ℱ^• is locally bounded: every object of the site has a covering sieve on whose members all but finitely many terms of ℱ^• restrict to zero, the finite set of surviving degrees depending on the member.
2. Every term ℱ^n is locally a direct summand of a finite free 𝒪-module.
3. The left dual is the one constructed in [Stacks, Tag 0FP9]: 𝒢^• is isomorphic to the complex SheafHom^•(ℱ^•, 𝒪) of [Stacks, Tag 0FPR] by an isomorphism carrying the coevaluation and the evaluation of the given pairing to η = ∑ ηₙ and ε = ∑ εₙ.

theorem isLocallyBounded_and_isLocallyDirectSummand_and_isoDualComplex_of_exactPairing
    (p : @ExactPairing _ _ (monoidalCategoryCochainComplex R) K L) :
    letI := monoidalCategoryCochainComplex R
    letI := p
    letI := exactPairingDualComplexOfLocallyStrictlyPerfect
      (isLocallyStrictlyPerfect_of_exactPairing R K L p)
    (∀ U : C, ∃ T : Sieve U, T ∈ J U ∧ ∀ ⦃V : C⦄ (g : V ⟶ U), T g →
        ∃ S : Finset ℤ, ∀ n ∉ S, IsZero ((K.X n).over V)) ∧
      (∀ n : ℤ, IsLocallyDirectSummandOfFiniteFree R.obj (isSheaf_ringSheaf R) (K.X n)) ∧
      ∃ e : L ≅ dualComplexOfLocallyStrictlyPerfect R K
          (isLocallyStrictlyPerfect_of_exactPairing R K L p),
        η_ K L ≫ K ◁ e.hom =
            η_ K (dualComplexOfLocallyStrictlyPerfect R K
              (isLocallyStrictlyPerfect_of_exactPairing R K L p)) ∧
          e.hom ▷ K ≫ ε_ K (dualComplexOfLocallyStrictlyPerfect R K
              (isLocallyStrictlyPerfect_of_exactPairing R K L p)) = ε_ K L

Tag 0G40, a lemma

Tag 0G40 in the Stacks Project.

Stacks.SheafOfModules.derivedSheafHomEvaluation_isIso_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHomEvaluation/PerfectEvaluation.lean, line 210.

Stacks 0G40. Let (X, O_X) be a ringed space and let K, L, M be objects of D(O_X) with K perfect. The evaluation morphism

RSheafHom(L, M) ⊗^L_{O_X} K ⟶ RSheafHom(RSheafHom(K, L), M)

of Stacks 0A8U is an isomorphism, for every L and M.

This reads off the ringed-site statement AlgebraicGeometry.RingedSite.isIso_derivedSheafHomEvaluation_of_isPerfect at the site of opens of the space, for the canonical derived tensor product and the derived internal Hom of the ringed space; the two notions of perfection agree because the predicate used here is the site-level one of Stacks 08G5.

theorem derivedSheafHomEvaluation_isIso_of_isPerfect
    (K L M : DerivedCategory (StructureSheafModules Rc))
    (hK : (ringedSite Rc).IsPerfect K) :
    IsIso (derivedSheafHomEvaluation Rc K L M)

Tag 08DQ, a lemma

Tag 08DQ in the Stacks Project.

Stacks.SheafOfModules.derivedBidualIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/PerfectBidual.lean, line 176. The attribute's comment: “the second assertion: (K^∨)^∨ ≅ K for a perfect K”.

Stacks 08DQ, second assertion. Let (X, O_X) be a ringed space and let K be a perfect object of D(O_X). Then K is reflexive: the canonical map K ⟶ (K^∨)^∨ of derivedBidualMap is an isomorphism, so (K^∨)^∨ ≅ K.

This is the isomorphism form of isIso_derivedBidualMap; its .symm is the orientation (K^∨)^∨ ≅ K in which the source states the assertion. The three factors are the left unitor, the trivialisation O_X ≅ RSheafHom(O_X, O_X) and the derived evaluation morphism of Stacks 0A8U, the last being invertible by Stacks 0G40.

Perfectness is the site-level notion of Stacks 08G5 read at the site of opens of the space, as in StacksFrontier.Topology.Sheaves.Cohomology.InternalHomEvaluation.PerfectEvaluation, whose section "Perfectness model" records why that notion and not the ringed-space one of Stacks 08CM.

def derivedBidualIso (K : DerivedCategory (StructureSheafModules Rc))
    (hK : (ringedSite Rc).IsPerfect K) :
    K ≅ derivedDual Rc (derivedDual Rc K)

Stacks.SheafOfModules.isIso_derivedBidualMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/PerfectBidual.lean, line 214. The attribute's comment: “the second assertion: the canonical map K = RSheafHom(O_X, O_X) ⊗^L K ⟶ (K^∨)^∨ of Stacks 0A8U is an isomorphism for a perfect K”. References: SGA 6 I (7.2), “special case”.

Stacks 08DQ, second assertion. Let (X, O_X) be a ringed space and let K be a perfect object of D(O_X). The canonical map

K = RSheafHom(O_X, O_X) ⊗^L_{O_X} K ⟶ RSheafHom(RSheafHom(K, O_X), O_X) = (K^∨)^∨

of derivedBidualMap is an isomorphism; equivalently (K^∨)^∨ ≅ K, which is derivedBidualIso.

Perfectness of K is the only hypothesis. Its two outer factors are isomorphisms by construction, and its middle factor — the derived evaluation morphism of Stacks 0A8U at L = M = O_X — is an isomorphism by Stacks 0G40, which holds for every value of the two variables specialised here.

theorem isIso_derivedBidualMap (K : DerivedCategory (StructureSheafModules Rc))
    (hK : (ringedSite Rc).IsPerfect K) :
    IsIso (derivedBidualMap Rc K)

Stacks.SheafOfModules.isPerfect_derivedDual, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/PerfectDual.lean, line 145. The attribute's comment: “the dual of a perfect object is perfect”.

Stacks 08DQ, first assertion. Let (X, O_X) be a ringed space and let K be a perfect object of D(O_X). Then the dual K^∨ = RSheafHom(K, O_X) is perfect as well.

Perfectness is local, so it is enough to model K^∨ above a covering of each open. Over a member V on which K is modelled by a strictly perfect complex E, the restriction of K^∨ is RSheafHom(K|_V, O_V), which is the class of the internal Hom complex SheafHom(E, O_V); and that complex is strictly perfect because the dual of a direct summand of a finite free module is again one.

theorem isPerfect_derivedDual (K : DerivedCategory (StructureSheafModules Rc))
    (hK : (ringedSite Rc).IsPerfect K) :
    (ringedSite Rc).IsPerfect (derivedDual Rc K)

Stacks.SheafOfModules.isPerfect_derivedDual_of_isPerfectSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/PerfectDualAtTheSpaceHypothesis.lean, line 69. The attribute's comment: “the first assertion with perfectness in the RINGED-SPACE reading of Tag 08CM on both sides, rather than the site reading of Tag 08G5 that Stacks.SheafOfModules.isPerfect_derivedDual uses; the two are equivalent by Stacks.Cohomology.PerfectComplexes.isPerfect_of_ringedSite and Stacks.Cohomology.PerfectComplexes.isPerfect_ringedSite_of_isPerfect”.

Let (X, O_X) be a ringed space and let K be a perfect object of D(O_X) in the sense of [Stacks, Tag 08CM]. Then the dual K^∨ = RSheafHom(K, O_X) is perfect in that same sense.

theorem isPerfect_derivedDual_of_isPerfectSpace
    (hK : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X) K) :
    Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X) (derivedDual X.sheaf K)

Stacks.SheafOfModules.isIso_derivedBidualMap_of_isPerfectSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/PerfectDualAtTheSpaceHypothesis.lean, line 81. The attribute's comment: “the second assertion with perfectness in the RINGED-SPACE reading of Tag 08CM rather than the site reading of Tag 08G5 that Stacks.SheafOfModules.isIso_derivedBidualMap uses”. References: SGA 6 I (7.2), “special case”.

For a perfect object K of D(O_X) in the sense of [Stacks, Tag 08CM] the canonical map K ⟶ (K^∨)^∨ of Stacks.SheafOfModules.derivedBidualMap is an isomorphism.

theorem isIso_derivedBidualMap_of_isPerfectSpace
    (hK : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X) K) :
    IsIso (derivedBidualMap X.sheaf K)

Stacks.SheafOfModules.derivedBidualIsoOfIsPerfectSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/PerfectDualAtTheSpaceHypothesis.lean, line 92. The attribute's comment: “the second assertion as an isomorphism, with perfectness in the RINGED-SPACE reading of Tag 08CM rather than the site reading of Tag 08G5 that Stacks.SheafOfModules.derivedBidualIso uses”.

For a perfect object K of D(O_X) in the sense of [Stacks, Tag 08CM], the isomorphism K ≅ (K^∨)^∨.

def derivedBidualIsoOfIsPerfectSpace
    (hK : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X) K) :
    K ≅ derivedDual X.sheaf (derivedDual X.sheaf K)

Stacks.SheafOfModules.isIso_derivedTensorDualToSheafHom_of_isPerfectSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/PerfectDualAtTheSpaceHypothesis.lean, line 107. The attribute's comment: “the third assertion with perfectness in the RINGED-SPACE reading of Tag 08CM rather than the site reading of Tag 08G5 that Stacks.SheafOfModules.isIso_derivedTensorDualToSheafHom_of_isPerfect uses”.

For a perfect object K of D(O_X) in the sense of [Stacks, Tag 08CM] and any object M, the canonical map of [Stacks, Tag 08I1]

M ⊗^L_{O_X} K^∨ ⟶ RSheafHom(K, M)

is an isomorphism.

theorem isIso_derivedTensorDualToSheafHom_of_isPerfectSpace
    (hK : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X) K) :
    IsIso (derivedTensorDualToSheafHom X.sheaf K M)

Stacks.SheafOfModules.bijective_derivedTensorDualGlobalSectionsMap_of_isPerfectSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/PerfectDualAtTheSpaceHypothesis.lean, line 122. The attribute's comment: “the fourth assertion with perfectness in the RINGED-SPACE reading of Tag 08CM rather than the site reading of Tag 08G5 that Stacks.SheafOfModules.bijective_derivedTensorDualGlobalSectionsMap_of_isPerfect uses”.

For a perfect object K of D(O_X) in the sense of [Stacks, Tag 08CM] and any object M, the canonical map of [Stacks, Tag 08I1] on degree-zero global hypercohomology

H⁰(X, M ⊗^L_{O_X} K^∨) ⟶ Hom_{D(O_X)}(K, M)

is bijective.

theorem bijective_derivedTensorDualGlobalSectionsMap_of_isPerfectSpace
    (hK : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X) K) :
    Function.Bijective (derivedTensorDualGlobalSectionsMap X.sheaf K M)

Stacks.SheafOfModules.derivedTensorDualGlobalSectionsAddEquivOfIsPerfectSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/PerfectDualAtTheSpaceHypothesis.lean, line 136. The attribute's comment: “the fourth assertion as an isomorphism of abelian groups, with perfectness in the RINGED-SPACE reading of Tag 08CM rather than the site reading of Tag 08G5 that Stacks.SheafOfModules.derivedTensorDualGlobalSectionsAddEquiv uses; functoriality in M is Stacks.SheafOfModules.derivedTensorDualSections_naturality together with AlgebraicGeometry.RingedSite.derivedTensorDualGlobalSectionsMap_naturality”.

For a perfect object K of D(O_X) in the sense of [Stacks, Tag 08CM] and any object M, H⁰(X, M ⊗^L_{O_X} K^∨) = Hom_{D(O_X)}(K, M) as abelian groups, the identification being the canonical map of [Stacks, Tag 08I1].

def derivedTensorDualGlobalSectionsAddEquivOfIsPerfectSpace
    (hK : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X) K) :
    ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} 0).obj
        ((derivedModuleGlobalSections (ringedSite X.sheaf)).obj
          (((derivedTensor X.sheaf).obj M).obj (derivedDual X.sheaf K))) : Type u) ≃+ (K ⟶ M)

Stacks.SheafOfModules.bijective_derivedTensorDualGlobalSectionsMap_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/PerfectDualGlobalSections.lean, line 132. The attribute's comment: “the fourth assertion: the canonical map H⁰(X, M ⊗^L K^∨) ⟶ Hom_{D(O_X)}(K, M) of Stacks 08I1 is bijective for a perfect K”.

Stacks 08DQ, fourth assertion. Let (X, O_X) be a ringed space, let K be a perfect object of D(O_X) and let M be any object. The canonical map of Stacks 08I1 on degree-zero global hypercohomology

H⁰(X, M ⊗^L_{O_X} K^∨) ⟶ Hom_{D(O_X)}(K, M)

is bijective.

Perfectness of K is in the site-level reading of Stacks 08G5, and M is arbitrary. The proof is the source's: by Stacks 08I1 the assertion reduces to invertibility of the canonical map M ⊗^L_{O_X} K^∨ ⟶ RSheafHom(K, M), which is the third assertion of the tag, isIso_derivedTensorDualToSheafHom_of_isPerfect.

theorem bijective_derivedTensorDualGlobalSectionsMap_of_isPerfect
    (K M : DerivedCategory (StructureSheafModules Rc))
    (hK : (ringedSite Rc).IsPerfect K) :
    Function.Bijective (derivedTensorDualGlobalSectionsMap Rc K M)

Stacks.SheafOfModules.derivedTensorDualGlobalSectionsAddEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/PerfectDualGlobalSections.lean, line 151. The attribute's comment: “the fourth assertion: H⁰(X, M ⊗^L K^∨) = Hom_{D(O_X)}(K, M) for a perfect K, as an isomorphism of abelian groups along the canonical map of Stacks 08I1; not its functoriality in M”.

Stacks 08DQ, fourth assertion, in the equality form the source states it in: for a perfect object K of D(O_X) and any object M,

H⁰(X, M ⊗^L_{O_X} K^∨) = Hom_{D(O_X)}(K, M)

as abelian groups, the identification being the canonical map of Stacks 08I1.

Functoriality of this identification in M is not claimed; see the section "What is still missing" of this file.

def derivedTensorDualGlobalSectionsAddEquiv
    (K M : DerivedCategory (StructureSheafModules Rc))
    (hK : (ringedSite Rc).IsPerfect K) :
    ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} 0).obj
        ((derivedModuleGlobalSections (ringedSite Rc)).obj
          (((derivedTensor Rc).obj M).obj (derivedDual Rc K))) : Type u) ≃+ (K ⟶ M)

Stacks.SheafOfModules.isIso_derivedTensorDualToSheafHom_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/PerfectDualTensorHom.lean, line 152. The attribute's comment: “the third assertion: the canonical map M ⊗^L K^∨ ⟶ RSheafHom(K, M) of Stacks 08I1 is an isomorphism for a perfect K”. References: SGA 6 I (7.7), “special case”.

Stacks 08DQ, third assertion. Let (X, O_X) be a ringed space, let K be a perfect object of D(O_X) and let M be any object. The canonical map of Stacks 08I1

Φ : M ⊗^L_{O_X} K^∨ ⟶ RSheafHom(K, M)

is an isomorphism.

The only hypothesis is perfectness of K, in the site-level reading of Stacks 08G5: there is a complex of O_X-modules representing K and a covering of the space on each member of which the restriction of that complex receives a quasi-isomorphism from a strictly perfect complex. The object M is arbitrary.

This is the ringed-site statement AlgebraicGeometry.RingedSite.isIso_derivedTensorDualToSheafHom_of_isPerfect read at the site of opens of the space, for the canonical derived tensor product. The section "How it is proved" of this file sets out the argument.

The instances in the ambient variable block are setup, not hypotheses on the lemma: a ringed space whose slice sites admit sheafification and on which the tensor product of sheaves of modules is additive and totalisable is what it takes for the objects in the statement — the derived tensor product, the derived dual, and their restrictions to the slices appearing in the definition of perfection — to exist at all.

theorem isIso_derivedTensorDualToSheafHom_of_isPerfect
    (K M : DerivedCategory (StructureSheafModules Rc))
    (hK : (ringedSite Rc).IsPerfect K) :
    IsIso (derivedTensorDualToSheafHom Rc K M)

Stacks.SheafOfModules.derivedTensorDualNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/PerfectDualTensorHomFunctorial.lean, line 105. The attribute's comment: “the third assertion as a natural isomorphism of functors on D(O_X), i.e. together with the FUNCTORIALITY in M that the source asserts; its component at M is the canonical map of Tag 08I1 and is the content of Stacks.SheafOfModules.isIso_derivedTensorDualToSheafHom_of_isPerfect”.

Stacks 08DQ, third assertion, as a natural isomorphism. For a perfect object K of D(O_X) the canonical maps M ⊗^L_{O_X} K^∨ ⟶ RSheafHom(K, M) of [Stacks, Tag 08I1] assemble into an isomorphism of functors

(- ⊗^L_{O_X} K^∨) ≅ RSheafHom(K, -),

which is the source's assertion that the identification is functorial in M. Its component at M is the canonical map, invertible by Stacks.SheafOfModules.isIso_derivedTensorDualToSheafHom_of_isPerfect; the naturality square is Stacks.SheafOfModules.derivedTensorDualToSheafHom_naturality.

def derivedTensorDualNatIso (hK : (ringedSite Rc).IsPerfect K) :
    (derivedTensor Rc).flip.obj (derivedDual Rc K) ≅ (derivedSheafHom Rc).obj (op K)

Stacks.SheafOfModules.derivedTensorDualNatIsoOfIsPerfectSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/PerfectDualTensorHomFunctorial.lean, line 125. The attribute's comment: “the third assertion as a natural isomorphism of functors, with perfectness in the RINGED-SPACE reading of Tag 08CM rather than the site reading of Tag 08G5 that Stacks.SheafOfModules.derivedTensorDualNatIso uses”.

Stacks 08DQ, third assertion, as a natural isomorphism, at the ringed-space hypothesis. As Stacks.SheafOfModules.derivedTensorDualNatIso, with perfectness of K read as Stacks.Cohomology.PerfectComplexes.IsPerfect, the notion of [Stacks, Tag 08CM].

def derivedTensorDualNatIsoOfIsPerfectSpace
    (hK : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X) K) :
    (derivedTensor X.sheaf).flip.obj (derivedDual X.sheaf K) ≅
      (derivedSheafHom X.sheaf).obj (op K)

Stacks.SheafOfModules.derivedTensorDualNatIsoLeft, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/PerfectDualTensorHomLeftSlot.lean, line 130. The attribute's comment: “the third assertion as a natural isomorphism of functors on D(O_X), with the dual in the LEFT tensor slot rather than the right one in which Tag 08I1 writes the canonical map and in which Stacks.SheafOfModules.derivedTensorDualNatIso states it; the two differ by the commutativity constraint of Tag 0FPT, so this one is NOT claimed to be carried by the canonical map”.

Stacks 08DQ, third assertion, with the dual in the left tensor slot. For a perfect object K of D(O_X) there is an isomorphism of functors

(K^∨ ⊗^L_{O_X} -) ≅ RSheafHom(K, -)

on D(O_X), which is the source's assertion that the identification is functorial in the second variable, written with the dual tensored on the left.

It is Stacks.SheafOfModules.derivedTensorDualNatIso, the same assertion with the dual in the right slot, precomposed with the commutativity constraint of Stacks.SheafOfModules.derivedTensorBraidingNatIso. Unlike the right-slot form, it is not claimed to be carried by the canonical map of [Stacks, Tag 08I1]; see the implementation notes.

def derivedTensorDualNatIsoLeft (hK : (ringedSite Rc).IsPerfect K) :
    (derivedTensor Rc).obj (derivedDual Rc K) ≅ (derivedSheafHom Rc).obj (op K)

Stacks.SheafOfModules.derivedTensorDualNatIsoLeftOfIsPerfectSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/PerfectDualTensorHomLeftSlot.lean, line 146. The attribute's comment: “the third assertion as a natural isomorphism with the dual in the LEFT tensor slot, with perfectness in the RINGED-SPACE reading of Tag 08CM rather than the site reading of Tag 08G5 that Stacks.SheafOfModules.derivedTensorDualNatIsoLeft uses”.

Stacks 08DQ, third assertion in the left tensor slot, at the ringed-space hypothesis. As Stacks.SheafOfModules.derivedTensorDualNatIsoLeft, with perfectness of K read as Stacks.Cohomology.PerfectComplexes.IsPerfect, the notion of [Stacks, Tag 08CM].

def derivedTensorDualNatIsoLeftOfIsPerfectSpace
    (hK : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X) K) :
    (derivedTensor X.sheaf).obj (derivedDual X.sheaf K) ≅
      (derivedSheafHom X.sheaf).obj (op K)

Tag 0FPB, a lemma

Tag 0FPB in the Stacks Project.

Stacks.Cohomology.MonoidalDerived.symmetricMonoidalDerivedCategory, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedMonoidalStructure.lean, line 586.

The derived category of modules on a ringed space is a symmetric monoidal category, with tensor product the derived tensor product, unit the structure sheaf in degree zero, and the usual associativity and commutativity constraints. This is the ringed site statement at the site of opens of X, exactly as Tag 0FP8 is Tag 0FPQ there.

public def symmetricMonoidalDerivedCategory (X : RingedSpace.{u, u})
    [HasDerivedCategory.{d} (Mod X.sheaf)] :
    SymmetricMonoidalDerivedCategory X.sheaf

Tag 0FPC, an example

Tag 0FPC in the Stacks Project.

Stacks.SheafOfModules.derivedDual_isLeftDual, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/PerfectDualLeftDual.lean, line 125.

Stacks 0FPC. Let (X, O_X) be a ringed space and let K be a perfect object of D(O_X) (Tag 08CM), with K^∨ = RSheafHom(K, O_X). Then

• the map c : K ⊗^L_{O_X} K^∨ ⟶ RSheafHom(K, K) of Stacks 08I1 is an isomorphism;
• the coevaluation η : O_X ⟶ K ⊗^L_{O_X} K^∨ is the map sending 1 to the section corresponding to id_K under c: η ≫ c is that section;
• with ε : K^∨ ⊗^L_{O_X} K ⟶ O_X the evaluation map, K^∨, η, ε is a left dual of K (Categories, Definition 0FFP): (1 ⊗ ε) ∘ (η ⊗ 1) = id_K and (ε ⊗ 1) ∘ (1 ⊗ η) = id_{K^∨}, read through the associativity and unit constraints of the monoidal structure of Stacks 0FPT on D(O_X).

The evaluation is Stacks.SheafOfModules.derivedDualEvaluation, the application morphism of Stacks 08J8 at target O_X (Stacks.SheafOfModules.derivedSheafHomCounit_structureSheaf_eq_derivedDualEvaluation), and the coevaluation is Stacks.SheafOfModules.derivedDualCoevaluation.

theorem derivedDual_isLeftDual (hK : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X) K) :
    letI := derivedMonoidalStructure X.sheaf
    letI : MonoidalCategory (DerivedCategory (SheafOfModules.{u}
        (Tensor.ringSheaf.{u, u, u} X.sheaf))) := derivedMonoidalStructure X.sheaf
    IsIso (derivedTensorDualToSheafHom X.sheaf K K) ∧
      derivedDualCoevaluation X.sheaf K
          (Stacks.Cohomology.PerfectComplexes.isPerfect_ringedSite_of_isPerfect X K hK) ≫
          derivedTensorDualToSheafHom X.sheaf K K =
        RingedSite.derivedIdentitySection (ringedSite X.sheaf) K ∧
      derivedDualCoevaluation X.sheaf K
          (Stacks.Cohomology.PerfectComplexes.isPerfect_ringedSite_of_isPerfect X K hK) ▷ K ≫
          (α_ K (derivedDual X.sheaf K) K).hom ≫ K ◁ derivedDualEvaluation X.sheaf K =
        (λ_ K).hom ≫ (ρ_ K).inv ∧
      derivedDual X.sheaf K ◁ derivedDualCoevaluation X.sheaf K
          (Stacks.Cohomology.PerfectComplexes.isPerfect_ringedSite_of_isPerfect X K hK) ≫
          (α_ (derivedDual X.sheaf K) K (derivedDual X.sheaf K)).inv ≫
          derivedDualEvaluation X.sheaf K ▷ derivedDual X.sheaf K =
        (ρ_ (derivedDual X.sheaf K)).hom ≫ (λ_ (derivedDual X.sheaf K)).inv

Tag 0FPD, a lemma

Tag 0FPD in the Stacks Project.

Stacks.SheafOfModules.isIso_derivedDualToLeftDualMonoidal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/LeftDualOnARingedSpace.lean, line 232. The attribute's comment: “conclusion (b) only: that the left dual of M is the object constructed in Example 0FPC, namely the derived dual RSheafHom(M, O_X), the identification being the morphism matched with the evaluation of Example 0FPC by the pairing — see Stacks.SheafOfModules.whiskerRight_derivedDualToLeftDualMonoidal for the compatibility of the two evaluations and Stacks.SheafOfModules.derivedDualEvaluation_eq_ringedSite for the identification of that evaluation with the one Example 0FPC constructs. The monoidal structure on D(O_X) is the one of Tag 0FPB and a left dual is Mathlib's CategoryTheory.ExactPairing, which is Definition 0FFP. Conclusion (a) of the tag — that M is PERFECT — is NOT proved here and NOT assumed here: it needs the pairing to restrict to the slices D(O_X|_U), for which the derived restriction functor would have to be monoidal, and nothing in this library makes it so. The naturality of the bijection of Tag 08DK/08JA in its source variable, which the argument uses, is the theorem AlgebraicGeometry.RingedSite.derivedCurryHomEquiv_naturality_source, so the exact pairing itself is the one remaining input”.

Stacks 0FPD, second assertion: a left dual of M in D(O_X) is the dual object of Example 0FPC. The morphism M^∨ = RSheafHom(M, O_X) ⟶ N which the exact pairing matches with the evaluation of Example 0FPC is an isomorphism; its inverse is the morphism which the tensor–internal-Hom bijection of Stacks 08DK matches with the evaluation of the pairing.

theorem isIso_derivedDualToLeftDualMonoidal
    (pair : letI : MonoidalCategory (DerivedCategory (StructureSheafModules Rc)) :=
        RingedSite.derivedMonoidalStructure (ringedSite Rc)
      ExactPairing M N) :
    letI : @ExactPairing
        (DerivedCategory
          (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf (ringedSite Rc).O)))
        inferInstance (RingedSite.derivedMonoidalStructure (ringedSite Rc)) M N := pair
    IsIso (RingedSite.derivedDualToLeftDual (X := ringedSite Rc) M N)

Stacks.Cohomology.LeftDualPerfect.isPerfect_and_isIso_derivedDualToLeftDual, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/PerfectComplexes/LeftDualIsPerfect.lean, line 96. The attribute's comment: “both conclusions, for one pairing: M is perfect, and the left dual is the derived dual of Example 0FPC”.

Stacks 0FPD. Let (X, O_X) be a ringed space and let M be an object of D(O_X) with a left dual N in the symmetric monoidal category D(O_X) of Stacks 0FPB (an exact pairing, Categories, Definition 0FFP). Then

• (a) M is perfect (Tag 08CM), and
• (b) the left dual is the one constructed in Example 0FPC: the morphism M^∨ = RSheafHom(M, O_X) ⟶ N which the pairing matches with the evaluation of Example 0FPC is an isomorphism.

The monoidal structure is written in its ringed-site spelling, which is the structure of Stacks 0FPB on the nose (derivedCategoryMonoidalCategory_eq_ringedSite, by rfl). Conclusion (a) is isPerfect_of_exactPairing; conclusion (b) is Stacks.SheafOfModules.isIso_derivedDualToLeftDualMonoidal, whose morphism carries the evaluation of the pairing to the evaluation of Example 0FPC (Stacks.SheafOfModules.whiskerRight_derivedDualToLeftDualMonoidal).

theorem isPerfect_and_isIso_derivedDualToLeftDual (X : RingedSpace.{u, u})
    (M N : DerivedModules X.sheaf)
    (pair : letI := derivedMonoidalSpace X; ExactPairing M N) :
    Stacks.Cohomology.PerfectComplexes.IsPerfect M ∧
      (letI := derivedMonoidalSpace X
       let _ := pair
       IsIso (AlgebraicGeometry.RingedSite.derivedDualToLeftDual
        (X := Stacks.SheafOfModules.ringedSite X.sheaf) M N))

Sources

• Section 20.50, Tag 0FP7
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Cohomology.MonoidalComplexes.symmetricMonoidalComplexes · Stacks.SheafOfModules.OnSpace.exists_exactPairing_ihomUnit_of_isLocallyBounded · Stacks.SheafOfModules.Strict.isLocallyBounded_and_isLocallyDirectSummand_and_isoDualComplex_of_exactPairing · Stacks.SheafOfModules.derivedSheafHomEvaluation_isIso_of_isPerfect · Stacks.SheafOfModules.derivedBidualIso · Stacks.SheafOfModules.isIso_derivedBidualMap · Stacks.SheafOfModules.isPerfect_derivedDual · Stacks.SheafOfModules.isPerfect_derivedDual_of_isPerfectSpace

Section20.51 Miscellany#

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

Tag 0DJI, a lemma

Tag 0DJI in the Stacks Project.

Stacks.SheafOfModules.isDerivedLimit_tensorDerivedDual_of_isHomotopyColimit_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedHomOfAHomotopyColimit.lean, line 257. The attribute's comment: “the whole tag: for a system of perfect objects Kₙ of D(O_X) with K = hocolim Kₙ and every E in D(O_X), the identity RSheafHom(K, E) = R lim (E ⊗^L_{O_X} Kₙ^∨)”.

Stacks 0DJI. Let (X, O_X) be a ringed space, let (Kₙ) be a system of perfect objects of D(O_X) and let K = hocolim Kₙ. Then for every object E of D(O_X)

RSheafHom(K, E) = R lim (E ⊗^L_{O_X} Kₙ^∨).

The source uses the perfectness of the Kₙ to invoke the third assertion of Stacks 08DQ, which is isIso_derivedTensorDualToSheafHom_of_isPerfect.

theorem isDerivedLimit_tensorDerivedDual_of_isHomotopyColimit_of_isPerfect
    (F : ℕ ⥤ DerivedCategory (StructureSheafModules Rc))
    (E : DerivedCategory (StructureSheafModules Rc))
    (hperf : ∀ n : ℕ, (ringedSite Rc).IsPerfect (F.obj n))
    {K : DerivedCategory (StructureSheafModules Rc)} (hK : IsHomotopyColimit F K) :
    IsDerivedLimit (tensorDerivedDualSystem Rc F E)
      (((derivedSheafHom Rc).flip.obj E).obj (op K))

Tag 0FVB, a lemma

Tag 0FVB in the Stacks Project.

Stacks.SheafOfModules.derivedDualPairingSquare_cup, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DualityPairingCupProduct.lean, line 510.

Stacks 0FVB. Let (X, O_X) be a ringed space and let K and E be objects of D(O_X) with E perfect (Tag 08CM). The diagram

H⁰(X, K ⊗^L E^∨) × H⁰(X, E) ⟶ H⁰(X, (K ⊗^L E^∨) ⊗^L E) ↓ ↓ Hom_X(E, K) × H⁰(X, E) ⟶ H⁰(X, K)

commutes: the cup product ξ ∪ η (Section 0FKU, the relative cup product of Stacks 0B68 for (X, O_X) ⟶ (pt, Γ(X, O_X)), Stacks.SheafOfModules.globalCupProductZero) followed by the map induced on H⁰ by 1_K ⊗ ε and the unit constraint (ε : E^∨ ⊗^L E ⟶ O_X of Example 0FPC) is the morphism E ⟶ K attached to ξ by the identification H⁰(X, K ⊗^L E^∨) = Hom_{D(O_X)}(E, K) of Lemma 08DQ (Stacks.SheafOfModules.derivedTensorDualGlobalSectionsMap), evaluated on η.

theorem derivedDualPairingSquare_cup (K E : DerivedCategory (StructureSheafModules X.sheaf))
    (hE : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X) E)
    (ξ : ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} 0).obj
      ((derivedModuleGlobalSections (ringedSite X.sheaf)).obj
        (((derivedTensor X.sheaf).obj K).obj (derivedDual X.sheaf E))) : Type u))
    (η : ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} 0).obj
      ((derivedModuleGlobalSections (ringedSite X.sheaf)).obj E) : Type u)) :
    (DerivedCategory.homologyFunctor AddCommGrpCat.{u} 0).map
        ((derivedModuleGlobalSections (ringedSite X.sheaf)).map
          (derivedDualContraction X.sheaf K E))
        (globalCupProductZero X (((derivedTensor X.sheaf).obj K).obj (derivedDual X.sheaf E)) E
          ξ η) =
      (DerivedCategory.homologyFunctor AddCommGrpCat.{u} 0).map
        ((derivedModuleGlobalSections (ringedSite X.sheaf)).map
          (derivedTensorDualGlobalSectionsMap X.sheaf E K ξ)) η

Tag 0GM7, a lemma

Tag 0GM7 in the Stacks Project.

Stacks.Cohomology.DerivedInternalHomPullback.isIso_derivedPullbackSheafHomMap_of_hasFiniteTorDimensionOverInverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/InternalHomPullbackFiniteTorDimension.lean, line 220. The attribute's comment: “clause (3)”.

Pullback of a derived internal hom along a morphism of finite tor dimension. Let h : X ⟶ Y be a morphism of ringed spaces such that 𝒪_X has finite tor dimension over h⁻¹𝒪_Y. For a pseudo-coherent K ∈ D(𝒪_Y) and a locally bounded below M ∈ D(𝒪_Y), the canonical map Lh^*R𝓗om(K, M) ⟶ R𝓗om(Lh^*K, Lh^*M) of Tag 08I3 is an isomorphism.

theorem isIso_derivedPullbackSheafHomMap_of_hasFiniteTorDimensionOverInverseImage
    (hh : HasFiniteTorDimensionOverInverseImage h)
    (K : DerivedCategory (AlgebraicGeometry.RingedSpace.KFlatDerivedPullback.Modules Y))
    (hK : AlgebraicGeometry.RingedSpace.PseudoCoherence.IsPseudoCoherent (X := Y) K)
    (M : DerivedCategory (AlgebraicGeometry.RingedSpace.KFlatDerivedPullback.Modules Y))
    (hM : AlgebraicGeometry.RingedSpace.IsLocallyBoundedBelow Y M) :
    IsIso (derivedPullbackSheafHomMap h K M)

Stacks.Cohomology.DerivedInternalHomPullback.isIso_derivedPullbackSheafHomMap_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/InternalHomPullbackPerfectAndPseudoCoherent.lean, line 59. The attribute's comment: “clause (1)”.

Pullback of a derived internal hom out of a perfect object. For a morphism of ringed spaces h : X ⟶ Y, a perfect K ∈ D(𝒪_Y) and an arbitrary M ∈ D(𝒪_Y), the canonical map Lh^*R𝓗om(K, M) ⟶ R𝓗om(Lh^*K, Lh^*M) is an isomorphism.

theorem isIso_derivedPullbackSheafHomMap_of_isPerfect
    (K : DerivedCategory (AlgebraicGeometry.RingedSpace.KFlatDerivedPullback.Modules Y))
    (hK : AlgebraicGeometry.RingedSpace.IsPerfect (X := Y) K)
    (M : DerivedCategory (AlgebraicGeometry.RingedSpace.KFlatDerivedPullback.Modules Y)) :
    IsIso (derivedPullbackSheafHomMap h K M)

Stacks.Cohomology.DerivedInternalHomPullback.isIso_derivedPullbackSheafHomMap_of_isPseudoCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/InternalHomPullbackPerfectAndPseudoCoherent.lean, line 71. The attribute's comment: “clause (2)”.

Flat pullback of a derived internal hom out of a pseudo-coherent object. For a flat morphism of ringed spaces h : X ⟶ Y, a pseudo-coherent K ∈ D(𝒪_Y) and a locally bounded below M ∈ D(𝒪_Y), the canonical map Lh^*R𝓗om(K, M) ⟶ R𝓗om(Lh^*K, Lh^*M) is an isomorphism.

theorem isIso_derivedPullbackSheafHomMap_of_isPseudoCoherent (hh : AlgebraicGeometry.IsFlat h)
    (K : DerivedCategory (AlgebraicGeometry.RingedSpace.KFlatDerivedPullback.Modules Y))
    (hK : AlgebraicGeometry.RingedSpace.PseudoCoherence.IsPseudoCoherent (X := Y) K)
    (M : DerivedCategory (AlgebraicGeometry.RingedSpace.KFlatDerivedPullback.Modules Y))
    (hM : AlgebraicGeometry.RingedSpace.IsLocallyBoundedBelow Y M) :
    IsIso (derivedPullbackSheafHomMap h K M)

Tag 0GM8, a lemma

Tag 0GM8 in the Stacks Project.

Stacks.Cohomology.DerivedInternalHomStalk.isIso_stalkSheafHomMap_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/InternalHomStalkInvertibility.lean, line 66. The attribute's comment: “case (1): K perfect, M arbitrary”.

Tag 0GM8, case (1). For a ringed space X, a point x ∈ X, a perfect K ∈ D(𝒪_X) and an arbitrary M ∈ D(𝒪_X), the canonical map

R𝓗om_{𝒪_X}(K, M)_x ⟶ RHom_{𝒪_{X,x}}(K_x, M_x)

is an isomorphism. Here Y = {x} is the one-point ringed space with structure sheaf 𝒪_{X,x}, and the map is the canonical map of Tag 08I3 along the flat inclusion Y ⟶ X, read through the identification D(𝒪_Y) ≌ D(𝒪_{X,x}) given by the stalk.

theorem isIso_stalkSheafHomMap_of_isPerfect
    (hK : AlgebraicGeometry.RingedSpace.IsPerfect (X := X) K) :
    IsIso (stalkSheafHomMap X x (pointStalkPresentation X x) K M)

Stacks.Cohomology.DerivedInternalHomStalk.isIso_stalkSheafHomMap_of_isPseudoCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/InternalHomStalkInvertibility.lean, line 79. The attribute's comment: “case (2): K pseudo-coherent, M locally bounded below”.

Tag 0GM8, case (2). For a ringed space X, a point x ∈ X, a pseudo-coherent K ∈ D(𝒪_X) and a locally bounded below M ∈ D(𝒪_X), the canonical map

R𝓗om_{𝒪_X}(K, M)_x ⟶ RHom_{𝒪_{X,x}}(K_x, M_x)

is an isomorphism, the map being that of isIso_stalkSheafHomMap_of_isPerfect.

theorem isIso_stalkSheafHomMap_of_isPseudoCoherent
    (hK : AlgebraicGeometry.RingedSpace.PseudoCoherence.IsPseudoCoherent (X := X) K)
    (hM : AlgebraicGeometry.RingedSpace.IsLocallyBoundedBelow X M) :
    IsIso (stalkSheafHomMap X x (pointStalkPresentation X x) K M)

Sources

• Section 20.51, Tag 0GM6
• AxiomMath/Stacks at 5ed82d14

LeanStacks.SheafOfModules.isDerivedLimit_tensorDerivedDual_of_isHomotopyColimit_of_isPerfect · Stacks.SheafOfModules.derivedDualPairingSquare_cup · Stacks.Cohomology.DerivedInternalHomPullback.isIso_derivedPullbackSheafHomMap_of_hasFiniteTorDimensionOverInverseImage · Stacks.Cohomology.DerivedInternalHomPullback.isIso_derivedPullbackSheafHomMap_of_isPerfect · Stacks.Cohomology.DerivedInternalHomPullback.isIso_derivedPullbackSheafHomMap_of_isPseudoCoherent · Stacks.Cohomology.DerivedInternalHomStalk.isIso_stalkSheafHomMap_of_isPerfect · Stacks.Cohomology.DerivedInternalHomStalk.isIso_stalkSheafHomMap_of_isPseudoCoherent

Section20.52 Invertible objects in the derived category#

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

Tag 0FPF, a lemma

Tag 0FPF in the Stacks Project.

Stacks.Modules.globalSections_equivalence_finiteFreeSummand_finiteProjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/RecoveryB/FiniteFreeSummandsOnASpace.lean, line 470.

Stacks Project, Tag 0FPF. Global sections induce an equivalence from direct summands of finite free 𝒪-modules to finite projective modules over the ring of global sections.

public theorem globalSections_equivalence_finiteFreeSummand_finiteProjective :
    ∃ (e : ObjectProperty.FullSubcategory (IsDirectSummandOfFiniteFree 𝒪) ≌
        ObjectProperty.FullSubcategory
          (fun M : ModuleCat.{u} (𝒪.obj.obj (op (⊤ : Opens X))) =>
            Module.Finite (𝒪.obj.obj (op (⊤ : Opens X))) M ∧
              Module.Projective (𝒪.obj.obj (op (⊤ : Opens X))) M)),
      Nonempty
        (e.functor ⋙ ObjectProperty.ι _ ≅
          ObjectProperty.ι _ ⋙ globalSectionsFunctor 𝒪)

Tag 0FPG, a lemma

Tag 0FPG in the Stacks Project.

Stacks.Cohomology.InvertibleDerived.hasInvertibleModuleDecomposition_of_isInvertibleObject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InvertibleDerivedClauseOneToTwo.lean, line 124. The attribute's comment: “clause (1) implies clause (2): an invertible object of D(𝒪_X) has a locally finite invertible module decomposition”.

The implication (1) ⟹ (2) of Stacks 0FPG. If M is an invertible object of D(𝒪_X), there is a locally finite direct product decomposition 𝒪_X = ∏ 𝒪_n and invertible 𝒪_n-modules ℋ^n with M = ⨁ ℋ^n[-n].

public theorem hasInvertibleModuleDecomposition_of_isInvertibleObject
    [inst : HasDerivedCategory.{d} (Mod X.sheaf)] (M : DerivedModules X.sheaf)
    (hM : IsInvertibleObject M) : HasInvertibleModuleDecomposition X M

Stacks.Cohomology.InvertibleDerived.isInvertibleObject_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InvertibleDerivedClauseOneToTwo.lean, line 181.

Stacks 0FPG. Let (X, 𝒪_X) be a ringed space and M an object of D(𝒪_X). The following are equivalent: 1. M is invertible in D(𝒪_X) for the derived tensor product; 2. there is a locally finite direct product decomposition 𝒪_X = ∏ 𝒪_n and for each n an invertible 𝒪_n-module ℋ^n with M = ⨁ ℋ^n[-n] in D(𝒪_X).

If they hold, M is perfect. If every stalk 𝒪_{X,x} is a local ring, they are also equivalent to 3. there is an open covering X = ⋃ U_i and for each i an integer n_i such that M|_{U_i} is represented by an invertible 𝒪_{U_i}-module placed in degree n_i.

public theorem isInvertibleObject_tfae [inst : HasDerivedCategory.{d} (Mod X.sheaf)]
    (M : DerivedModules X.sheaf) :
    [IsInvertibleObject M, HasInvertibleModuleDecomposition X M].TFAE ∧
      (IsInvertibleObject M → @Stacks.Cohomology.PerfectComplexes.IsPerfect.{u, u, d} X inst M) ∧
      ((∀ x : X.carrier, IsLocalRing (X.presheaf.stalk x)) →
        [IsInvertibleObject M, HasInvertibleModuleDecomposition X M,
          HasLocalInvertibleDegree M].TFAE)

Stacks.Cohomology.InvertibleDerived.hasInvertibleModuleDecomposition_iff_hasLocalInvertibleDegree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InvertibleDerivedClauseThreeToTwo.lean, line 356. The attribute's comment: “if every stalk of 𝒪_X is a local ring, clauses (2) and (3) are equivalent”.

Stacks 0FPG, the equivalence of clauses (2) and (3). Let (X, 𝒪_X) be a ringed space all of whose stalks 𝒪_{X,x} are local rings, and let M be an object of D(𝒪_X). Then M admits a locally finite direct product decomposition 𝒪_X = ∏ 𝒪_n with invertible 𝒪_n-modules ℋ^n and M = ⨁ ℋ^n[-n] — clause (2) — if and only if there is an open covering X = ⋃ U_i and integers n_i such that M|_{U_i} is represented by an invertible 𝒪_{U_i}-module placed in degree n_i — clause (3).

public theorem hasInvertibleModuleDecomposition_iff_hasLocalInvertibleDegree
    [HasDerivedCategory.{d} (Mod X.sheaf)] (M : DerivedModules X.sheaf)
    (hloc : ∀ x : X.carrier, IsLocalRing (X.presheaf.stalk x)) :
    HasInvertibleModuleDecomposition X M ↔ HasLocalInvertibleDegree M

Stacks.Cohomology.InvertibleDerived.isInvertibleObject_of_hasInvertibleModuleDecomposition_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InvertibleDerivedFlatRestrictScalars.lean, line 85. The attribute's comment: “clause (2) implies clause (1): a locally finite invertible module decomposition of M makes M an invertible object of D(𝒪_X) for the derived tensor product of Stacks 0FPB”.

If M admits a locally finite invertible module decomposition, then M is an invertible object of D(𝒪_X).

public theorem isInvertibleObject_of_hasInvertibleModuleDecomposition_unconditional
    [HasDerivedCategory.{d} (Mod X.sheaf)] (M : DerivedModules X.sheaf)
    (hM : HasInvertibleModuleDecomposition X M) :
    IsInvertibleObject M

Stacks.Cohomology.InvertibleDerived.HasInvertibleModuleDecomposition, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InvertibleDerivedObjects.lean, line 317. The attribute's comment: “clause (2) as a condition on M: that there is a locally finite direct product decomposition 𝒪_X = ∏_{n ∈ ℤ} 𝒪_n and for each n an invertible 𝒪_n-module ℋ^n, in the sense of Stacks 01CS, with M = ⨁ ℋ^n[-n] in D(𝒪_X). This is the clause, not an implication between clauses; the decomposition itself is ProductDecomposition”.

Clause (2) of Stacks 0FPG. There is a locally finite direct product decomposition 𝒪_X = ∏_{n ∈ ℤ} 𝒪_n of the structure sheaf and for each n an invertible 𝒪_n-module ℋ^n such that M = ⨁_{n ∈ ℤ} ℋ^n[-n] in D(𝒪_X), the n-th summand being ℋ^n viewed as an 𝒪_X-module and placed in degree n.

public def HasInvertibleModuleDecomposition (M : DerivedModules X.sheaf) : Prop

Stacks.Cohomology.InvertibleDerived.isPerfect_of_hasInvertibleModuleDecomposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InvertibleDerivedObjects.lean, line 432. The attribute's comment: “clause (2) implies that M is a perfect object of D(𝒪_X)”.

Stacks 0FPG, the perfectness conclusion. Let (X, 𝒪_X) be a ringed space and let M be an object of D(𝒪_X). If there is a locally finite direct product decomposition 𝒪_X = ∏_{n ∈ ℤ} 𝒪_n and for each n an invertible 𝒪_n-module ℋ^n with M = ⨁ ℋ^n[-n] in D(𝒪_X), then M is a perfect object of D(𝒪_X).

Near a point only finitely many factors survive, each ℋ^n is locally a direct summand of a finite free 𝒪_n-module and 𝒪_n is a direct summand of 𝒪_X, so the complex with ℋ^n in degree n and zero differentials — which represents ⨁ ℋ^n[-n] — is locally strictly perfect.

public theorem isPerfect_of_hasInvertibleModuleDecomposition (M : DerivedModules X.sheaf)
    (hM : HasInvertibleModuleDecomposition X M) :
    @Stacks.Cohomology.PerfectComplexes.IsPerfect.{u, u, d} X inst M

Stacks.Cohomology.InvertibleDerived.IsInvertibleObject, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InvertibleDerivedObjects.lean, line 454. The attribute's comment: “clause (1) as a condition on M: that M is invertible in D(𝒪_X) in the sense of Stacks 0FFN, for the derived tensor product of Stacks 0FPB. This is the clause, not an implication between clauses”.

Clause (1) of Stacks 0FPG. M is an invertible object of D(𝒪_X): there is an object N of D(𝒪_X) with M ⊗^L N ≅ 𝒪_X and N ⊗^L M ≅ 𝒪_X, the tensor product being the derived tensor product and 𝒪_X the structure sheaf in degree zero.

public def IsInvertibleObject (M : DerivedModules X.sheaf) : Prop

Stacks.Cohomology.InvertibleDerived.HasLocalInvertibleDegree, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InvertibleDerivedObjects.lean, line 515. The attribute's comment: “clause (3) as a condition on M: that there is an open covering X = ⋃ U_i and for each i an integer n_i with M|_{U_i} represented by an invertible 𝒪_{U_i}-module placed in degree n_i. The source's condition that every stalk 𝒪_{X,x} is a local ring belongs to the equivalence of (3) with the other clauses, which is hasInvertibleModuleDecomposition_iff_hasLocalInvertibleDegree”.

Clause (3) of Stacks 0FPG. M is represented by a complex which, on each member of some open covering of X, is quasi-isomorphic to an invertible module placed in a single degree — the degree being allowed to vary with the member of the covering.

public def HasLocalInvertibleDegree (M : DerivedModules X.sheaf) : Prop

Sources

• Section 20.52, Tag 0FPE
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Modules.globalSections_equivalence_finiteFreeSummand_finiteProjective · Stacks.Cohomology.InvertibleDerived.hasInvertibleModuleDecomposition_of_isInvertibleObject · Stacks.Cohomology.InvertibleDerived.isInvertibleObject_tfae · Stacks.Cohomology.InvertibleDerived.hasInvertibleModuleDecomposition_iff_hasLocalInvertibleDegree · Stacks.Cohomology.InvertibleDerived.isInvertibleObject_of_hasInvertibleModuleDecomposition_unconditional · Stacks.Cohomology.InvertibleDerived.HasInvertibleModuleDecomposition · Stacks.Cohomology.InvertibleDerived.isPerfect_of_hasInvertibleModuleDecomposition · Stacks.Cohomology.InvertibleDerived.IsInvertibleObject

Section20.53 Compact objects#

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

Tag 0F5Z, a lemma

Tag 0F5Z in the Stacks Project.

Stacks.Cohomology.CompactObjects.isCompactObject_jShriek_structureSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/RecoveryB/CompactObjectExtensionByZero.lean, line 576.

Finite cohomological dimension and commutation of cohomology with direct sums make j_! 𝒪_U compact in the unbounded derived category of 𝒪_X-modules.

public theorem isCompactObject_jShriek_structureSheaf
    (X : SheafedSpace.{u + 1, u, u} RingCat.{u}) (U : Opens X.carrier)
    (d : ℤ)
    (hvanish : ∀ (p : ℕ) (M : SheafOfModules.{u} (OXSh X)),
      d < (p : ℤ) →
        IsZero (((SheafOfModules.evaluation (OXSh X) (op U)).rightDerived p).obj M))
    (hsums : ∀ (p : ℕ) (I : Type u),
      PreservesColimitsOfShape (Discrete I)
        ((SheafOfModules.evaluation (OXSh X) (op U)).rightDerived p)) :
    IsCompactObject.{u}
      ((DerivedCategory.singleFunctor (SheafOfModules.{u} (OXSh X)) 0).obj
        ((jShriek00A7 X U).obj (SheafOfModules.unit (OUSh X U))))

Tag 09J7, a lemma

Tag 09J7 in the Stacks Project.

Stacks.Cohomology.RingedSpaceCompact.isCompactObject_of_isPerfect_of_finiteCohomDim, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/CompactObjects/PerfectObjectsOnARingedSpaceUnconditional.lean, line 135. The attribute's comment: “(b): on a ringed space satisfying (1), (2) and (3) and of finite cohomological dimension, a perfect object is a compact object of D(O_X)”.

Stacks 09J7 (b). Let X be a ringed space whose underlying topological space is quasi-compact, has a basis of quasi-compact opens, and has quasi-compact intersections of quasi-compact opens — hypotheses (1), (2) and (3) of the tag. Let K be a perfect object of D(O_X) and suppose X has finite cohomological dimension, that is Hᵖ(X, F) = 0 for every O_X-module F and every p beyond a fixed bound d. Then K is a compact object of D(O_X).

The reduction the source performs first — by Stacks 08DQ morphisms out of K are morphisms out of j_{X!}O_X after applying K^∨ ⊗^L_{O_X} -, a functor commuting with direct sums — is AlgebraicGeometry.RingedSite.derivedDualHomEquivOfIsoStructureSheaf together with AlgebraicGeometry.RingedSite.preservesColimitsOfShape_derivedTensorFlip, and it is applied at the final object ⊤ of the site of opens. The three topological conditions enter through Stacks 01FF: they make the cohomology functors F ↦ Hᵖ(X, F) commute with arbitrary direct sums, which with the dimension bound is what Stacks 094D consumes.

theorem isCompactObject_of_isPerfect_of_finiteCohomDim [CompactSpace X.carrier]
    (hBasis : PrespectralSpace X.carrier)
    (hInter : QuasiSeparatedSpace X.carrier)
    (K : DerivedCategory (_root_.SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (RingedSpace.ringedSite X).O)))
    (hK : (RingedSpace.ringedSite X).IsPerfect K)
    (hcd : ∃ d : ℤ, ∀ (p : ℕ) (F : _root_.SheafOfModules.{u}
        (Stacks.SheafOfModules.Tensor.ringSheaf (RingedSpace.ringedSite X).O)),
      d < (p : ℤ) → IsZero (Hgroup
        (Stacks.SheafOfModules.Tensor.ringSheaf (RingedSpace.ringedSite X).O) ⊤ p F)) :
    IsCompactObject.{u} K

Stacks.Cohomology.RingedSpaceCompact.hom_coproduct_bijective_of_isPerfect_of_compactSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/CompactObjects/PerfectObjectsOnARingedSpaceUnconditional.lean, line 221. The attribute's comment: “(a): on a ringed space satisfying (1), (2) and (3), a perfect object K satisfies Hom(K, ⨁ M_i) = ⨁ Hom(K, M_i) whenever ⨁ M_i is bounded below”.

Stacks 09J7 (a). Let X be a ringed space whose underlying topological space is quasi-compact, has a basis of quasi-compact opens, and has quasi-compact intersections of quasi-compact opens — hypotheses (1), (2) and (3) of the tag. Let K be a perfect object of D(O_X) and let M : I → D(O_X) be a family whose coproduct is bounded below. Then Hom(K, ⨁ Mᵢ) = ⨁ Hom(K, Mᵢ): the canonical map from the direct sum of the Hom(K, Mᵢ) is bijective.

The proof applies hom_coproduct_bijective_of_isPerfect_of_hasFiniteTorDimension; the finite Tor dimension of K^∨ is the global form of Stacks 08G8, Stacks.Cohomology.TorAmplitude.hasFiniteTorDimension_of_ringedSite_isPerfect, applied to the dual K^∨, which is perfect by Stacks 08JJ (AlgebraicGeometry.RingedSite.isPerfect_derivedDual): perfectness gives the Tor amplitude of K^∨ only locally, quasi-compactness makes the local intervals one interval, and the bridge Stacks.Cohomology.TorAmplitude.hasTorAmplitude_iff_derivedTensorProduct reads that interval against the derived tensor product datum the reduction measures Tor dimension by.

The index type lies in the universe of the space, as for clause (b).

theorem hom_coproduct_bijective_of_isPerfect_of_compactSpace [CompactSpace X.carrier]
    (hBasis : PrespectralSpace X.carrier)
    (hInter : QuasiSeparatedSpace X.carrier)
    (K : DerivedCategory (_root_.SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (RingedSpace.ringedSite X).O)))
    (hK : (RingedSpace.ringedSite X).IsPerfect K)
    {I : Type u} [DecidableEq I]
    (M : I → DerivedCategory (_root_.SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (RingedSpace.ringedSite X).O))) [HasCoproduct M]
    (hplus : DerivedCategoryB.IsBoundedBelow (∐ M)) :
    Function.Bijective
      (DirectSum.toAddMonoid fun j => Preadditive.rightComp K (Limits.Sigma.ι M j))

Sources

• Section 20.53, Tag 09J6
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Cohomology.CompactObjects.isCompactObject_jShriek_structureSheaf · Stacks.Cohomology.RingedSpaceCompact.isCompactObject_of_isPerfect_of_finiteCohomDim · Stacks.Cohomology.RingedSpaceCompact.hom_coproduct_bijective_of_isPerfect_of_compactSpace

Section20.54 Projection formula#

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

Tag 01E7, a lemma

Tag 01E7 in the Stacks Project.

Stacks.SheafOfModules.OnSpace.injective_tensorSheaf_of_finiteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocallyFiniteFreeSummand/InjectiveTensor.lean, line 53.

Tensoring an injective sheaf of modules with a finite locally free sheaf of modules preserves injectivity.

theorem injective_tensorSheaf_of_finiteLocallyFree
    (I E : SheafOfModules.{u} (structureSheafRing X))
    [Injective I] [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} E] :
    Injective ((((Stacks.SheafOfModules.Tensor.sheafTensor
      ⟨((X)).presheaf, ((X)).IsSheaf⟩).obj (E)).obj (I)))

Tag 01E8, a lemma

Tag 01E8 in the Stacks Project.

Stacks.ProjectionFormula.derivedPushforwardTensorRightRingedSpacePlusIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectionFormula/HigherDirectImageRingedSpace.lean, line 246. The attribute's comment: “the D⁺ clause: for a morphism of ringed spaces f : X ⟶ Y and a finite locally free 𝒪_Y-module ℰ, the isomorphism ℰ ⊗_{𝒪_Y} Rf_ℱ ≅ Rf_(f^*ℰ ⊗_{𝒪_X} ℱ) in D^+(Y), functorial in ℱ”. References: EGA 0 (12.2.3), “more general”; SGA 6 III (5.8), “special case”.

The D⁺ clause of [Stacks, Tag 01E8]: for a morphism of ringed spaces f : X ⟶ Y and a finite locally free 𝒪_Y-module ℰ,

D(- ⊗_{𝒪_X} f^*ℰ) ⋙ Rf_* ≅ Rf_* ⋙ D(- ⊗_{𝒪_Y} ℰ)

as functors D⁺(𝒪_X) ⥤ D⁺(𝒪_Y): the projection formula in the bounded below derived category, for an arbitrary morphism of ringed spaces, every object of D⁺(𝒪_X) and ℰ of arbitrary rank.

def derivedPushforwardTensorRightRingedSpacePlusIso :
    (tensorRightSheaf X ((pullbackFunctor f).obj E)).mapDerivedCategoryPlus ⋙
        (pushforwardFunctor f).rightDerivedFunctorPlus ≅
      (pushforwardFunctor f).rightDerivedFunctorPlus ⋙
        (tensorRightSheaf Y E).mapDerivedCategoryPlus

Stacks.ProjectionFormula.higherDirectImageProjectionFormulaRingedSpaceIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectionFormula/HigherDirectImageRingedSpace.lean, line 298. The attribute's comment: “the higher direct image clause: for a morphism of ringed spaces f : X ⟶ Y, an 𝒪_X-module ℱ and a finite locally free 𝒪_Y-module ℰ, the isomorphisms R^n f_(ℱ ⊗_{𝒪_X} f^ℰ) ≅ R^n f_*ℱ ⊗_{𝒪_Y} ℰ for every integer n; the tag's q ≥ 0 is the case n = (q : ℤ)”. References: EGA 0 (12.2.3), “partial”.

The higher direct image clause of [Stacks, Tag 01E8]: for a morphism of ringed spaces f : X ⟶ Y, an arbitrary 𝒪_X-module ℱ and a finite locally free 𝒪_Y-module ℰ,

R^n f_*(ℱ ⊗_{𝒪_X} f^*ℰ) ≅ (R^n f_*ℱ) ⊗_{𝒪_Y} ℰ

for every integer n; the tag's q ≥ 0 is the case n = (q : ℤ).

def higherDirectImageProjectionFormulaRingedSpaceIso
    (F : SheafOfModules.{u} (structureRingSheaf X)) (n : ℤ) :
    ((pushforwardFunctor f).rightDerivedPlus n).obj
        (((Stacks.SheafOfModules.Tensor.sheafTensor.{u, u, u, u, u} X.sheaf).obj F).obj
          ((pullbackFunctor f).obj E)) ≅
      ((Stacks.SheafOfModules.Tensor.sheafTensor.{u, u, u, u, u} Y.sheaf).obj
        (((pushforwardFunctor f).rightDerivedPlus n).obj F)).obj E

Stacks.AffineProjectionFormula.isIso_projectionFormulaMap_of_isFiniteLocallyFree_class_ringedSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectionFormula/LocalityRingedSpace.lean, line 417. The attribute's comment: “the q = 0 clause: for a morphism of ringed spaces f, an arbitrary module 𝒢 on the source and a finite locally free module ℋ on the target, the projection formula map f_𝒢 ⊗ ℋ ⟶ f_(𝒢 ⊗ f^*ℋ) is an isomorphism”.

The projection formula for an arbitrary morphism of ringed spaces at a finite locally free module on the target, finite local freeness being the class of [Stacks, Tag 01C6]: for 𝒢 an arbitrary 𝒪_Z-module and ℋ a finite locally free 𝒪_X-module, the canonical map f_*𝒢 ⊗_{𝒪_X} ℋ ⟶ f_*(𝒢 ⊗_{𝒪_Z} f^*ℋ) is an isomorphism.

This is isIso_projectionFormulaMap_of_isFiniteLocallyFree_ringedSpace with its pointwise input supplied by exists_moduleRestriction_iso_free_of_isFiniteLocallyFree.

theorem isIso_projectionFormulaMap_of_isFiniteLocallyFree_class_ringedSpace
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} H] :
    IsIso (projectionFormulaMap f G H)

Tag 0B53, an equation

Tag 0B53 in the Stacks Project.

Stacks.Duality.projectionFormulaMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RightAdjointPushforward/PullbackComparison.lean, line 167. The attribute's comment: “the map”.

The projection-formula map K ⊗ᴸ_{𝒪_Y} Rf_*E ⟶ Rf_*(Lf^*K ⊗ᴸ_{𝒪_X} E): the adjoint transpose, for the adjunction Lf^* ⊣ Rf_* on the quasi-coherent derived categories, of the oplax monoidality of Lf^* followed by the counit of that adjunction in the pushforward factor. Its invertibility is [Stacks, Tag 08EU].

def projectionFormulaMap (E : quasiCoherentDerivedCategory X)
    (K : quasiCoherentDerivedCategory Y) :
    ((quasiCoherentDerivedTensor Y).obj K).obj
        ((quasiCoherentDerivedPushforward f hpush).obj E) ⟶
      (quasiCoherentDerivedPushforward f hpush).obj
        (((quasiCoherentDerivedTensor X).obj
          ((quasiCoherentDerivedPullback' f).obj K)).obj E)

Stacks.Duality.projectionFormulaMap_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RightAdjointPushforward/PullbackComparison.lean, line 180. The attribute's comment: “naturality”.

The projection-formula map is natural in both arguments.

theorem projectionFormulaMap_naturality {E E' : quasiCoherentDerivedCategory X}
    {K K' : quasiCoherentDerivedCategory Y} (φ : E ⟶ E') (h : K ⟶ K') :
    (((quasiCoherentDerivedTensor Y).map h).app
          ((quasiCoherentDerivedPushforward f hpush).obj E) ≫
        ((quasiCoherentDerivedTensor Y).obj K').map
          ((quasiCoherentDerivedPushforward f hpush).map φ)) ≫
      projectionFormulaMap f hpush α E' K' =
    projectionFormulaMap f hpush α E K ≫
      (quasiCoherentDerivedPushforward f hpush).map
        (((quasiCoherentDerivedTensor X).map
            ((quasiCoherentDerivedPullback' f).map h)).app E ≫
          ((quasiCoherentDerivedTensor X).obj
            ((quasiCoherentDerivedPullback' f).obj K')).map φ)

Stacks.Cohomology.DerivedProjectionFormula.projectionFormulaMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/ProjectionFormula.lean, line 164. The attribute's comment: “the map”.

The derived projection-formula morphism Rf_*E ⊗^L_{𝒪_Y} K ⟶ Rf_*(E ⊗^L_{𝒪_X} Lf^*K): the adjoint transpose of the derived pullback-tensor comparison of Stacks 079U followed by the counit of Lf^* ⊣ Rf_* in the left tensor factor. It is defined for arbitrary E ∈ D(𝒪_X) and K ∈ D(𝒪_Y).

def projectionFormulaMap
    (E : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing Y))) :
    ((Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor Y.sheaf).obj
        ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f).obj E)).obj K ⟶
      (Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f).obj
        (((Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor X.sheaf).obj E).obj
          ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback f).obj K))

Stacks.Cohomology.DerivedProjectionFormula.projectionFormulaMap_natural_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/ProjectionFormula.lean, line 197. The attribute's comment: “naturality in the source complex”.

The derived projection-formula morphism is natural in the derived module on the source.

theorem projectionFormulaMap_natural_left
    {E E' : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))}
    (e : E ⟶ E')
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing Y))) :
    ((Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor Y.sheaf).map
        ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f).map e)).app K ≫
        projectionFormulaMap f E' K =
      projectionFormulaMap f E K ≫
        (Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f).map
          (((Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor X.sheaf).map e).app
            ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback f).obj K))

Stacks.Cohomology.DerivedProjectionFormula.projectionFormulaMap_natural_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/ProjectionFormula.lean, line 216. The attribute's comment: “naturality in the target complex”.

The derived projection-formula morphism is natural in the derived module on the target.

theorem projectionFormulaMap_natural_right
    (E : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    {K K' : DerivedCategory (SheafOfModules.{u} (structureSheafRing Y))}
    (k : K ⟶ K') :
    ((Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor Y.sheaf).obj
        ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f).obj E)).map k ≫
        projectionFormulaMap f E K' =
      projectionFormulaMap f E K ≫
        (Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f).map
          (((Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor X.sheaf).obj E).map
            ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback f).map k))

Stacks.Cohomology.ProjectionFormulaPerfect.projectionFormulaTransformation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/ProjectionFormulaStrictlyPerfect.lean, line 128. The attribute's comment: “the map as a natural transformation in the target complex”.

The projection-formula morphism of [Stacks, Tag 0B53] as a natural transformation. Its component at K is Stacks.Cohomology.DerivedProjectionFormula.projectionFormulaMap f E K, and its naturality is projectionFormulaMap_natural_right.

def projectionFormulaTransformation
    (E : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))) :
    projectionFormulaSource f E ⟶ projectionFormulaTarget f E

Tag 0B54, a lemma

Tag 0B54 in the Stacks Project.

Stacks.Cohomology.DerivedProjectionFormula.isIso_projectionFormulaMap_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/ProjectionFormulaLocalStrictlyPerfect.lean, line 138. References: SGA 6 IV (2.11.1), “more general”.

Let f : (X, 𝒪_X) ⟶ (Y, 𝒪_Y) be a morphism of ringed spaces, let E ∈ D(𝒪_X) and let K ∈ D(𝒪_Y) be perfect. Then the projection-formula morphism of [Stacks, Tag 0B53]

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

is an isomorphism.

Perfectness is Stacks.Cohomology.PerfectComplexes.IsPerfect of [Stacks, Tag 08CM]: K is represented by a complex which on the members of some open cover of Y receives a quasi-isomorphism from a strictly perfect complex.

theorem isIso_projectionFormulaMap_of_isPerfect
    {X Y : RingedSpace.{u, u}} (f : X ⟶ Y)
    [HasSheafify (Opens.grothendieckTopology X.carrier) AddCommGrpCat.{u}]
    [(Opens.grothendieckTopology X.carrier).WEqualsLocallyBijective AddCommGrpCat.{u}]
    [HasSheafify (Opens.grothendieckTopology Y.carrier) AddCommGrpCat.{u}]
    [(Opens.grothendieckTopology Y.carrier).WEqualsLocallyBijective AddCommGrpCat.{u}]
    (E : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing Y)))
    (hK : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := Y) K) :
    IsIso (projectionFormulaMap f E K)

Stacks.Cohomology.ProjectionFormulaPerfect.isIso_projectionFormulaMap_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/ProjectionFormulaPerfect.lean, line 352. The attribute's comment: “the whole tag: for an arbitrary morphism of ringed spaces f : X ⟶ Y, an arbitrary E in D(𝒪_X) and a perfect K in D(𝒪_Y), the projection-formula morphism Rf_E ⊗ᴸ K ⟶ Rf_(E ⊗ᴸ Lf^*K) of Tag 0B53 is invertible”. References: SGA 6 III (3.7), “special case”; SGA 6 IV (2.11.1), “more general”.

The projection formula for a perfect complex [Stacks, Tag 0B54]. For a morphism of ringed spaces f : (X, 𝒪_X) ⟶ (Y, 𝒪_Y), an arbitrary E ∈ D(𝒪_X) and a perfect K ∈ D(𝒪_Y), the projection-formula morphism

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

of [Stacks, Tag 0B53] is invertible.

The base case K = 𝒪_Y[i]⟦n⟧ of the source's dévissage is Stacks.Cohomology.DerivedProjectionFormula.isIso_projectionFormulaMap_singleUnit_degree ([Stacks, Tag 08EU] at every degree), obtained from the abstract projection formula Stacks.ProjectionFormula.isIso_adjunctionTensorMap at an invertible object, and the dévissage over strictly perfect complexes is isIso_projectionFormulaMap_of_isStrictlyPerfect.

The proof. A perfect K is the class of a perfect complex A, so there is an open covering U of Y on each member of which A receives a quasi-isomorphism from a strictly perfect complex. Invertibility in D(𝒪_Y) is local on that covering (Stacks.Cohomology.isIso_of_isIso_jStar_mapDerivedCategory_map), restriction to a member is derived pullback along its inclusion (Stacks.Cohomology.DerivedOpenImmersion.derivedPullbackOpenRestrictionIso), and derived pullback of the projection-formula morphism along that inclusion is invertible as soon as the projection-formula morphism of the base change is (isIso_derivedPullback_map_projectionFormulaMap, which is [Stacks, Tag 0B6B] together with invertibility of the derived base-change map at a square of open immersions). The base change is taken as the genuine fibre product X ×_Y U in ringed spaces, which exists because the inclusion of an open subspace is an open immersion, so the square is Cartesian on the nose and Stacks.Cohomology.DerivedBaseChange.isIso_derivedBaseChangeMap_of_isOpenImmersions applies. Upstairs the complex is strictly perfect and isIso_projectionFormulaMap_derivedPullback_obj closes it.

theorem isIso_projectionFormulaMap_of_isPerfect {X Y : RingedSpace.{u, u}} (f : X ⟶ Y)
    (E : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing Y)))
    (hK : AlgebraicGeometry.RingedSpace.IsPerfect K) :
    IsIso (projectionFormulaMap f E K)

Stacks.Cohomology.ProjectionFormulaShiftedUnit.isIso_projectionFormulaMap_isStrictlyPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/ProjectionFormulaShiftedUnit.lean, line 333. The attribute's comment: “the dévissage from the structure sheaf to a strictly perfect complex, now with NO hypothesis: the case K = O_Y[i] shifted by any amount, which Stacks.Cohomology.ProjectionFormulaPerfect.isIso_projectionFormulaMap_of_isStrictlyPerfect carries as the hypothesis hunit, is discharged here. What is still not covered of the tag is the reduction of a PERFECT complex to a strictly perfect one, which is local on the base and needs the base-change square of Tag 0B6B along an open immersion composed with a locality statement for invertibility of the map; so this is the tag for a strictly perfect complex, not for a perfect one”.

The dévissage half of [Stacks, Tag 0B54] with no hypothesis at all. For an arbitrary morphism of ringed spaces f : X ⟶ Y, an arbitrary E in D(𝒪_X) and a strictly perfect complex P of 𝒪_Y-modules, the derived projection-formula morphism

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

of [Stacks, Tag 0B53] is an isomorphism.

This is Stacks.Cohomology.ProjectionFormulaPerfect.isIso_projectionFormulaMap_of_isStrictlyPerfect with its hypothesis hunit supplied by isIso_projectionFormulaMap_single_shift.

theorem isIso_projectionFormulaMap_isStrictlyPerfect
    (E : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (P : CochainComplex (OXMod.{u, u} Y) ℤ) (hP : IsStrictlyPerfect P) :
    IsIso (projectionFormulaMap f E (DerivedCategory.Q.obj P))

Tag 0B55, a lemma

Tag 0B55 in the Stacks Project.

Stacks.Cohomology.ClosedEmbeddingProjectionFormulaComplexes.complexProjectionFormulaIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/ClosedEmbeddingProjectionFormulaComplexes.lean, line 270. The attribute's comment: “step 2: the projection formula holds at the level of complexes”.

The projection formula for a closed embedding, at the level of complexes. For a morphism of ringed spaces f : X ⟶ Y whose underlying continuous map is a homeomorphism onto a closed subset, and for arbitrary cochain complexes A^• of 𝒪_X-modules and B^• of 𝒪_Y-modules,

Tot(f_*A^• ⊗_{𝒪_Y} B^•) ≅ f_* Tot(A^• ⊗_{𝒪_X} f^*B^•).

There is no flatness, boundedness or finiteness hypothesis on either complex.

This is the complex-level step of the source's proof of [Stacks, Tag 0B55]. It is the termwise isomorphism projectionBicomplexIso on totalizations, composed with the comparison Tot(f_*(-)) ⟶ f_*(Tot(-)), which is invertible by Stacks.Cohomology.ClosedEmbeddingPushforward.isIso_totalMap_modulePushforward because f_* commutes with arbitrary direct sums. The derived statement of [Stacks, Tag 0B55] does not follow from this without the identification described in the module docstring, and is not proved here.

def complexProjectionFormulaIso
    (hf : Topology.IsClosedEmbedding (ConcreteCategory.hom f.hom.base))
    (A : CochainComplex (SheafOfModules.{u} (structureSheafRing X)) ℤ)
    (B : CochainComplex (SheafOfModules.{u} (structureSheafRing Y)) ℤ) :
    ((tensorComplex Y.sheaf).obj
        (((modulePushforward f).mapHomologicalComplex (.up ℤ)).obj A)).obj B ≅
      ((modulePushforward f).mapHomologicalComplex (.up ℤ)).obj
        (((tensorComplex X.sheaf).obj A).obj
          (((modulePullback f).mapHomologicalComplex (.up ℤ)).obj B))

Stacks.Cohomology.DerivedProjectionFormula.isIso_projectionFormulaMap_of_isClosedEmbedding, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/ClosedEmbeddingProjectionFormulaDerived.lean, line 871. The attribute's comment: “for an arbitrary morphism of ringed spaces whose underlying map is a homeomorphism onto a closed subset; the derived statement, with no boundedness, flatness, finiteness, quasi-coherence or support hypothesis on either complex”.

[Stacks, Tag 0B55]. Let f : (X, 𝒪_X) ⟶ (Y, 𝒪_Y) be a morphism of ringed spaces whose underlying continuous map is a homeomorphism onto a closed subset. Then the projection-formula morphism of [Stacks, Tag 0B53]

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

is an isomorphism for every E in D(𝒪_X) and every K in D(𝒪_Y).

The proof is the source's: represent E by any complex and K by a K-flat complex, which is possible by [Stacks, Tag 06YF], and transport invertibility along the two representations, which is legitimate by Stacks.Cohomology.DerivedProjectionFormula.isIso_projectionFormulaMap_congr_left and isIso_projectionFormulaMap_congr_right. On representatives the morphism is Q of the complex-level projection formula up to isomorphism, which is projectionFormulaMap_eq_derivedModelIso in the namespace Stacks.Cohomology.ClosedEmbeddingProjectionFormulaComplexes.

theorem isIso_projectionFormulaMap_of_isClosedEmbedding
    (hf : Topology.IsClosedEmbedding (ConcreteCategory.hom f.hom.base))
    (E : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing Y))) :
    IsIso (projectionFormulaMap f E K)

Stacks.Cohomology.DerivedProjectionFormula.isIso_projectionFormulaMapRight_of_isClosedEmbedding, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/ClosedEmbeddingProjectionFormulaRightIso.lean, line 67. The attribute's comment: “the right-handed form: the pushforward in the right tensor factor, K ⊗^L Rf_E ⟶ Rf_(Lf^*K ⊗^L E), for an arbitrary morphism of ringed spaces whose underlying map is a homeomorphism onto a closed subset and arbitrary K and E”.

The projection formula along a closed embedding, with the pushforward in the right tensor factor. Let f : (X, 𝒪_X) ⟶ (Y, 𝒪_Y) be a morphism of ringed spaces whose underlying continuous map is a homeomorphism onto a closed subset. Then the projection-formula morphism

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

is an isomorphism for every K in D(𝒪_Y) and every E in D(𝒪_X).

theorem isIso_projectionFormulaMapRight_of_isClosedEmbedding
    (hf : Topology.IsClosedEmbedding (ConcreteCategory.hom f.hom.base))
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing Y)))
    (E : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))) :
    IsIso (projectionFormulaMapRight f K E)

Stacks.ClosedEmbeddingProjectionFormula.isIso_stalkMap_projectionFormulaMap'_of_notMemRange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/ClosedEmbeddingProjectionFormulaStalks.lean, line 317. The attribute's comment: “the stalk computation off the closed image: both stalks vanish there”.

Off the closed image the projection-formula morphism is invertible on stalks. This is the first half of the stalk verification in the source's proof of [Stacks, Tag 0B55]: for y outside the image of a homeomorphism onto a closed subset both stalks vanish, by isZero_stalk_source_of_notMemRange and isZero_stalk_target_of_notMemRange, and any morphism between zero objects is invertible.

The other half, the stalk over a point of the image, is isIso_stalkMap_projectionFormulaMap'_of_memRange; together the two give isIso_projectionFormulaMap'_of_isClosedEmbedding.

theorem isIso_stalkMap_projectionFormulaMap'_of_notMemRange
    (hf : Topology.IsClosedEmbedding (ConcreteCategory.hom f.hom.base)) (y : Y.carrier)
    (hy : y ∉ Set.range (ConcreteCategory.hom f.hom.base)) :
    IsIso ((TopCat.Presheaf.stalkFunctor AddCommGrpCat.{u} y).map
      ((ExtensionByZeroModules.toAb (structureRingSheaf Y)).map
        (projectionFormulaMap' f G H)))

Stacks.ClosedEmbeddingProjectionFormula.isIso_stalkMap_projectionFormulaMap'_of_memRange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/ClosedEmbeddingProjectionFormulaStalks.lean, line 516. The attribute's comment: “the stalk computation over a point of the image, by cancelling the base change”.

Over a point of the image the projection-formula morphism is invertible on stalks. This is the second half of the stalk verification in the source's proof of [Stacks, Tag 0B55], and the step where the mathematics sits: at y = f x the source stalk is G_x ⊗_R H_{f x} and the target stalk is G_x ⊗_S (S ⊗_R H_{f x}), and they are identified by cancelling the base change.

The stalk map is R-linear and carries the germ of m ⊗ k to the germ of m ⊗ η k by Stacks.ProjectionFormula.projectionFormulaMap'_unit_tmul, which under the three identifications stalkPushforwardEquiv, [Stacks, Tag 01CB] and [Stacks, Tag 0098] is exactly the formula m ⊗ n ↦ m ⊗ (1 ⊗ n) that tensorProjectionMap_bijective recognises.

theorem isIso_stalkMap_projectionFormulaMap'_of_memRange :
    IsIso ((TopCat.Presheaf.stalkFunctor AddCommGrpCat.{u} (f.hom.base x)).map
      ((ExtensionByZeroModules.toAb (structureRingSheaf Y)).map
        (projectionFormulaMap' f E K)))

Stacks.ClosedEmbeddingProjectionFormula.isIso_projectionFormulaMap'_of_isClosedEmbedding, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/ClosedEmbeddingProjectionFormulaStalks.lean, line 661. The attribute's comment: “step 1: the ordinary projection formula map is invertible for a closed embedding”. References: SGA 3 VIB (11.5), “Clause (a), special case”.

The ordinary projection formula for a closed embedding of ringed spaces. For a morphism of ringed spaces f : X ⟶ Y whose underlying continuous map is a homeomorphism onto a closed subset, and for arbitrary sheaves of modules G on X and H on Y, the canonical morphism

f_*G ⊗_{𝒪_Y} H ⟶ f_*(G ⊗_{𝒪_X} f^*H)

is an isomorphism.

This is step 1 of the source's proof of [Stacks, Tag 0B55]. A morphism of sheaves of modules which is invertible on every stalk is invertible (ExtensionByZeroModules.isIso_of_stalk_isIso), and the two stalk computations are isIso_stalkMap_projectionFormulaMap'_of_memRange on the image and isIso_stalkMap_projectionFormulaMap'_of_notMemRange off it.

No local surjectivity of 𝒪_Y ⟶ f_*𝒪_X is assumed, so the counit of f^* ⊣ f_* is not invertible and the formal argument of Stacks.AffineProjectionFormula.isIso_projectionFormulaMap is unavailable; that is why the proof goes through stalks. The derived statement of [Stacks, Tag 0B55] does not follow from this without the K-flat reduction, and is not proved here.

theorem isIso_projectionFormulaMap'_of_isClosedEmbedding
    (hf : Topology.IsClosedEmbedding (ConcreteCategory.hom f.hom.base)) :
    IsIso (projectionFormulaMap' f G H)

Stacks.Cohomology.ClosedEmbeddingPushforward.preservesColimitsOfSize_modulePushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/ClosedEmbeddingPushforwardColimits.lean, line 171. The attribute's comment: “f_* commutes with direct sums: the input of the source's proof”.

Pushforward of sheaves of modules along a morphism of ringed spaces which is a homeomorphism onto a closed subset preserves all small colimits, in particular arbitrary direct sums. This is the input "f_* commutes with direct sums" of the source's proof of [Stacks, Tag 0B55]; the library had only right exactness, Stacks.ClosedImmersion.preservesFiniteColimits_modulePushforward.

The statement is reduced to preservesColimits_sheafPushforward through the forgetful functor to abelian sheaves, which preserves colimits and reflects isomorphisms.

theorem preservesColimitsOfSize_modulePushforward
    (f : X ⟶ Y) (hf : Topology.IsClosedEmbedding f.hom.base) :
    PreservesColimitsOfSize.{0, 0} (modulePushforward f)

Stacks.Cohomology.ClosedEmbeddingPushforward.isIso_derivedPushforwardUnit_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/ClosedEmbeddingPushforwardColimits.lean, line 203. The attribute's comment: “step 1: Rf_ is computed by applying f_ termwise”.

For a morphism of ringed spaces which is a homeomorphism onto a closed subset the derived pushforward is computed by applying f_* termwise: the comparison Qh (f_* K) ⟶ Rf_* (Qh K) is invertible at every object K of the homotopy category, with no K-injectivity hypothesis.

This is the first step of the source's proof of [Stacks, Tag 0B55]. It is Stacks.Cohomology.ExactPushforwardAdjunction.isIso_derivedPushforwardUnit_app, whose hypothesis of right exactness is discharged by Stacks.ClosedImmersion.preservesFiniteColimits_modulePushforward, [Stacks, Tag 08KS].

theorem isIso_derivedPushforwardUnit_app (f : X ⟶ Y)
    (hf : Topology.IsClosedEmbedding f.hom.base)
    (K : HomotopyCategory (SheafOfModules.{u} (structureSheafRing X)) (ComplexShape.up ℤ)) :
    IsIso ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforwardUnit f).app K)

Stacks.Cohomology.ClosedEmbeddingPushforward.isIso_totalMap_modulePushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/ClosedEmbeddingPushforwardColimits.lean, line 218. The attribute's comment: “f_* commutes with the totalization of an unbounded bicomplex”.

f_* commutes with the total complex of a bicomplex when f is a homeomorphism onto a closed subset: the comparison Tot(f_* K) ⟶ f_* Tot(K) of HomologicalComplex₂.TotalMap.totalMap is an isomorphism. There is no boundedness hypothesis on the bicomplex, which is what the source's proof of [Stacks, Tag 0B55] needs: the totalizations it compares are those of unbounded bicomplexes.

theorem isIso_totalMap_modulePushforward (f : X ⟶ Y)
    (hf : Topology.IsClosedEmbedding f.hom.base)
    (K : HomologicalComplex₂ (SheafOfModules.{u} (structureSheafRing X))
      (ComplexShape.up ℤ) (ComplexShape.up ℤ))
    [K.HasTotal (ComplexShape.up ℤ)]
    [HomologicalComplex₂.HasTotal
      (HomologicalComplex₂.TotalMap.mapBicomplex (modulePushforward f) K)
      (ComplexShape.up ℤ)] :
    IsIso (HomologicalComplex₂.TotalMap.totalMap (c₁₂ := ComplexShape.up ℤ)
      (modulePushforward f) K)

Stacks.Cohomology.SupportedComplexes.isIso_projectionFormulaMap_closedSubsetInclusion_of_isClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/ProjectionFormulaClosedEmbeddingUnconditional.lean, line 344. The attribute's comment: “for the canonical inclusion of a closed subset, with its restricted structure sheaf; the conclusion is unconditional, but the source's hypothesis -- any morphism of ringed spaces that is a homeomorphism onto a closed subset -- is narrowed to that inclusion”.

[Stacks, Tag 0B55] for the inclusion of a closed subset. The projection-formula map of [Stacks, Tag 0B53]

Ri_*E ⊗^𝐋_{𝒪_X} K ⟶ Ri_*(E ⊗^𝐋_{𝒪_X|_Z} Li^*K)

is an isomorphism for arbitrary E in D(𝒪_X|_Z) and K in D(𝒪_X), with no hypothesis on either beyond closedness of Z, which is the source's hypothesis that i be a homeomorphism onto a closed subset.

This is isIso_projectionFormulaMap_closedSubsetInclusion with its support hypothesis supplied by cohomologySupportedOn_derivedTensor_derivedPushforward_closedSubsetInclusion.

theorem isIso_projectionFormulaMap_closedSubsetInclusion_of_isClosed
    (E : DerivedCategory (SheafOfModules.{u}
      (structureSheafRing (closedSubsetRingedSpace X Z))))
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))) :
    IsIso (projectionFormulaMap (closedSubsetInclusion X Z) E K)

Tag 0B6B, a remark

Tag 0B6B in the Stacks Project.

Stacks.Cohomology.DerivedProjectionFormula.projectionFormulaMap_derivedBaseChangeMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/ProjectionFormulaBaseChange.lean, line 310.

Stacks 0B6B: the derived projection-formula map is compatible with a commutative square of ringed spaces.

For a commutative square g' ≫ f = f' ≫ g of ringed spaces and arbitrary E ∈ D(𝒪_X), K ∈ D(𝒪_Y), the diagram ProjectionFormulaBaseChangeSquare commutes at the derived projection-formula map of Stacks 0B53 for f and for f', the derived base change map of Stacks 08HY and the identification derivedPullbackSquareIso: the comparison of Stacks 079U for g, followed by base change in the first tensor factor and by the projection-formula map for f', equals the derived pullback along g of the projection-formula map for f, followed by base change and by Rf'_* of the comparison of Stacks 079U for g' and of the identification in the second tensor factor.

There is no boundedness, flatness or quasi-coherence hypothesis on E and K, and no associator or symmetry of ⊗^L is used: the diagram has binary tensor products only.

theorem projectionFormulaMap_derivedBaseChangeMap
    (E : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing Y))) :
    ProjectionFormulaBaseChangeSquare (derivedPushforward f) (derivedPushforward f')
      (derivedPullback f) (derivedPullback f') (derivedPullback g) (derivedPullback g')
      (Functor.uncurry.obj (derivedTensorProductFunctor Y.sheaf))
      (Functor.uncurry.obj (derivedTensorProductFunctor X.sheaf))
      (Functor.uncurry.obj (derivedTensorProductFunctor Y'.sheaf))
      (Functor.uncurry.obj (derivedTensorProductFunctor X'.sheaf))
      (pullbackTensorComparison g) (pullbackTensorComparison g') E K
      (projectionFormulaMap f E K)
      (Stacks.Cohomology.DerivedBaseChange.derivedBaseChangeMap g' f' f g sq
        ((Functor.uncurry.obj (derivedTensorProductFunctor X.sheaf)).obj
          (E, (derivedPullback f).obj K)))
      (Stacks.Cohomology.DerivedBaseChange.derivedBaseChangeMap g' f' f g sq E)
      ((derivedPullbackSquareIso g' f' f g sq).inv.app K)
      (projectionFormulaMap f' ((derivedPullback g').obj E) ((derivedPullback g).obj K))

Stacks.Cohomology.DerivedProjectionFormula.projectionFormulaMapRight_derivedBaseChangeMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/ProjectionFormulaRightBaseChange.lean, line 108. The attribute's comment: “the right-handed form: the pushforward in the right tensor factor”.

The right-handed projection-formula map is compatible with a commutative square of ringed spaces.

For a commutative square g' ≫ f = f' ≫ g of ringed spaces and arbitrary E ∈ D(𝒪_X), K ∈ D(𝒪_Y), the diagram ProjectionFormulaBaseChangeSquare commutes at the right-handed projection-formula map projectionFormulaMapRight for f and for f', the derived base change map of Stacks 08HY and the identification derivedPullbackSquareIso, with the derived tensor products read with their arguments interchanged. This is projectionFormulaMap_derivedBaseChangeMap with the pushforward in the right tensor factor.

theorem projectionFormulaMapRight_derivedBaseChangeMap
    (E : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing Y))) :
    ProjectionFormulaBaseChangeSquare (derivedPushforward f) (derivedPushforward f')
      (derivedPullback f) (derivedPullback f') (derivedPullback g) (derivedPullback g')
      (CategoryTheory.Prod.swap _ _ ⋙ Functor.uncurry.obj (derivedTensorProductFunctor Y.sheaf))
      (CategoryTheory.Prod.swap _ _ ⋙ Functor.uncurry.obj (derivedTensorProductFunctor X.sheaf))
      (CategoryTheory.Prod.swap _ _ ⋙ Functor.uncurry.obj (derivedTensorProductFunctor Y'.sheaf))
      (CategoryTheory.Prod.swap _ _ ⋙ Functor.uncurry.obj (derivedTensorProductFunctor X'.sheaf))
      (pullbackTensorComparisonSwap g) (pullbackTensorComparisonSwap g') E K
      (projectionFormulaMapRight f K E)
      (Stacks.Cohomology.DerivedBaseChange.derivedBaseChangeMap g' f' f g sq
        ((CategoryTheory.Prod.swap _ _ ⋙
          Functor.uncurry.obj (derivedTensorProductFunctor X.sheaf)).obj
            (E, (derivedPullback f).obj K)))
      (Stacks.Cohomology.DerivedBaseChange.derivedBaseChangeMap g' f' f g sq E)
      ((derivedPullbackSquareIso g' f' f g sq).inv.app K)
      (projectionFormulaMapRight f' ((derivedPullback g).obj K) ((derivedPullback g').obj E))

Sources

• Section 20.54, Tag 01E6
• AxiomMath/Stacks at 5ed82d14

LeanStacks.SheafOfModules.OnSpace.injective_tensorSheaf_of_finiteLocallyFree · Stacks.ProjectionFormula.derivedPushforwardTensorRightRingedSpacePlusIso · Stacks.ProjectionFormula.higherDirectImageProjectionFormulaRingedSpaceIso · Stacks.AffineProjectionFormula.isIso_projectionFormulaMap_of_isFiniteLocallyFree_class_ringedSpace · Stacks.Duality.projectionFormulaMap · Stacks.Duality.projectionFormulaMap_naturality · Stacks.Cohomology.DerivedProjectionFormula.projectionFormulaMap · Stacks.Cohomology.DerivedProjectionFormula.projectionFormulaMap_natural_left

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.