21.46 Tor dimension to 21.53 Complexes with locally…

Section21.46 Tor dimension#

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

Tag 08FZ, a definition

Tag 08FZ in the Stacks Project.

Stacks.SheafOfModules.DerivedTensorProduct.HasTorAmplitude, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/TorAmplitude/Defs.lean, line 88. 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), “(i)”.

Stacks 08FZ (1). An object E of D(O) has Tor amplitude in [a, b] for the derived tensor product T if, for every sheaf of O-modules F, the derived tensor product of E with F placed in degree zero has vanishing cohomology in every degree outside [a, b].

noncomputable def HasTorAmplitude
    (T : DerivedTensorProduct.{u, v, w, d} X) (E : RingedSite.DerivedModules.{u, v, w, d} X)
    (a b : ℤ) : Prop

Stacks.SheafOfModules.DerivedTensorProduct.HasFiniteTorDimension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/TorAmplitude/Defs.lean, line 131. 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 08FZ (2). An object E of D(O) has finite Tor dimension for the derived tensor product T if it has Tor amplitude in some interval.

noncomputable def HasFiniteTorDimension (T : DerivedTensorProduct.{u, v, w, d} X)
    (E : RingedSite.DerivedModules.{u, v, w, d} X) : Prop

Stacks.SheafOfModules.DerivedTensorProduct.HasTorDimensionLE, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/TorAmplitude/Defs.lean, line 149. The attribute's comment: “tor dimension of a module”. References: SGA 4½ Rapport (4.5), “sheaf module case”; SGA 4 XVII (4.1.9), “module case”.

Stacks 08FZ, the last sentence. A sheaf of O-modules F has Tor dimension at most n when F[0], viewed as an object of D(O), has Tor amplitude in [-n, 0].

noncomputable def HasTorDimensionLE (T : DerivedTensorProduct.{u, v, w, d} X)
    (F : RingedSite.Modules.{u, v, w} X) (n : ℤ) : Prop

Stacks.SheafOfModules.DerivedTensorProduct.hasTorAmplitude_of_coversTop, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/TorAmplitude/IntervalDescent.lean, line 107. The attribute's comment: “the descent of tor amplitude in a fixed interval from a covering family to the object covered”.

Tor amplitude in a fixed interval descends along a covering family. Let V : ι → C be a family of objects covering the final object of the site. If the restriction of E to the localized ringed site at each V i has Tor amplitude in [a, b], measured against the derived tensor product T' (V i) on that slice, then E has Tor amplitude in [a, b] for T.

theorem hasTorAmplitude_of_coversTop
    (T : DerivedTensorProduct.{c, u, u, d} X)
    (T' : ∀ U : X.C, DerivedTensorProduct.{max c u, u, u, d} (X.over U))
    {ι : Type t} {V : ι → X.C} (hV : X.J.CoversTop V)
    (E : RingedSite.DerivedModules.{c, u, u, d} X) (a b : ℤ)
    (hamp : ∀ i, HasTorAmplitude (T' (V i))
      ((RingedSite.derivedRestriction.{c, u, u, d} X (V i)).obj E) a b) :
    HasTorAmplitude T E a b

Stacks.SheafOfModules.DerivedTensorProduct.hasFiniteTorDimension_of_locallyHasFiniteTorDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/TorAmplitude/IntervalDescent.lean, line 127. The attribute's comment: “on a quasi-compact site, locally finite tor dimension is finite tor dimension”.

On a quasi-compact site, locally finite Tor dimension is finite Tor dimension. If the site has a terminal object which is quasi-compact in the sense of Stacks 090H and E locally has finite Tor dimension, then E has finite Tor dimension.

theorem hasFiniteTorDimension_of_locallyHasFiniteTorDimension
    (T : DerivedTensorProduct.{c, u, u, d} X)
    (T' : ∀ U : X.C, DerivedTensorProduct.{max c u, u, u, d} (X.over U))
    (E : RingedSite.DerivedModules.{c, u, u, d} X)
    (hE : LocallyHasFiniteTorDimension T' E)
    (U : X.C) (hU : IsTerminal U) (hqc : X.J.IsQuasiCompactObject U) :
    HasFiniteTorDimension T E

Stacks.SheafOfModules.DerivedTensorProduct.LocallyHasFiniteTorDimension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/TorAmplitude/LocallyFiniteTorDimension.lean, line 189. The attribute's comment: “locally finite tor dimension”.

Stacks 08FZ (3). An object E of D(O) locally has finite Tor dimension if every object U of C carries a covering family on each member V of which the restriction of E to the localized ringed site has finite Tor dimension. Finite Tor dimension on the slice over V is measured against the given derived tensor product T V on that slice.

def LocallyHasFiniteTorDimension
    (T : ∀ U : X.C, DerivedTensorProduct.{max u v, v, w, d} (X.over U))
    (E : RingedSite.DerivedModules.{u, v, w, d} X) : Prop

Tag 08G0, a lemma

Tag 08G0 in the Stacks Project.

Stacks.SheafOfModules.DerivedTensorProduct.isFlat_cokernel_of_hasTorAmplitude, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/TorAmplitude/FlatCokernel.lean, line 123. The attribute's comment: “variant: Tor amplitude measured against a derived tensor product datum T on D(O); the tag is Stacks.SheafOfModules.DerivedTensorProduct.isFlat_cokernel_of_hasTorAmplitude_canonical”.

Stacks 08G0. The cokernel of the differential into the lowest degree of the Tor-amplitude interval of a bounded above complex of flat O-modules is a flat O-module.

The complex is K-flat by Stacks 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-module F. Hence Coker(d^{a-1}) ⊗ - preserves monomorphisms, and being right exact as well it is exact.

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

Stacks.SheafOfModules.DerivedTensorProduct.isFlat_cokernel_of_hasTorAmplitude_canonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/TorAmplitude/FlatCokernelCanonical.lean, line 64.

Stacks 08G0, for the derived tensor product of the site. Let (C, O) be a ringed site and let K be a bounded above complex of flat O-modules which, as an object of D(O), has Tor amplitude in [a, b] for the derived tensor product Stacks.SheafOfModules.canonicalDerivedTensorProduct of Stacks 06YU. Then the cokernel of the differential K^{a-1} ⟶ K^a is a flat O-module.

No derived tensor product datum is supplied: the one Tor amplitude is measured against is the one Stacks 06YU constructs.

theorem isFlat_cokernel_of_hasTorAmplitude_canonical
    (K : CochainComplex (RingedSite.Modules.{u, u, u} X) ℤ) (a b : ℤ)
    (hbound : ∃ n : ℤ, K.IsStrictlyLE n)
    (hflat : ∀ i : ℤ,
      AlgebraicGeometry.SheafOfModules.IsFlat.{u, u, u, u} (O := X.O) (K.X i)) :
    letI : HasSheafify X.J AddCommGrpCat.{u} := inferInstance
    letI : X.J.WEqualsLocallyBijective AddCommGrpCat.{u} := inferInstance
    letI := Stacks.SheafOfModules.Tensor.sheafTensor_obj_additive.{u, u, u, u, u} X.O
    HasTorAmplitude (Stacks.SheafOfModules.canonicalDerivedTensorProduct.{u, u, d} X)
        (DerivedCategory.Q.obj K) a b →
      AlgebraicGeometry.SheafOfModules.IsFlat.{u, u, u, u} (O := X.O)
        (cokernel (K.d (a - 1) a))

Tag 08G1, a lemma

Tag 08G1 in the Stacks Project.

Stacks.SheafOfModules.DerivedTensorProduct.hasTorAmplitude_iff_exists_flatRepresentative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/TorAmplitude/FlatRepresentative.lean, line 288. References: SGA 4 XVII (4.1.9), “(i) <=> (iii)”; SGA 6 I (5.1).

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

theorem hasTorAmplitude_iff_exists_flatRepresentative
    (T : DerivedTensorProduct.{u, v, w, d} Y)
    (E : RingedSite.DerivedModules.{u, v, w, d} Y) (a b : ℤ) (hab : a ≤ b) :
    HasTorAmplitude T E a b ↔
      ∃ K : CochainComplex (RingedSite.Modules.{u, v, w} Y) ℤ,
        (∀ i : ℤ, AlgebraicGeometry.SheafOfModules.IsFlat.{v, u, w, w}
          (O := Y.O) (K.X i)) ∧
        (∀ i : ℤ, i ∉ Set.Icc a b → IsZero (K.X i)) ∧
        Nonempty (DerivedCategory.Q.obj K ≅ E)

Stacks.SheafOfModules.DerivedTensorProduct.hasTorAmplitude_canonical_iff_exists_flatRepresentative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/TorAmplitude/FlatRepresentativeCanonical.lean, line 70. The attribute's comment: “for the derived tensor product of the site, with no datum assumed”. References: SGA 4 XVII (4.1.9), “(i) <=> (iii)”; SGA 6 I (5.1).

Stacks 08G1, for the derived tensor product of the site. An object of D(O) has Tor amplitude in [a, b], measured against the derived tensor product Stacks.SheafOfModules.canonicalDerivedTensorProduct of Stacks 06YU, exactly when some complex of flat O-modules vanishing in every degree outside [a, b] represents it.

No derived tensor product datum is assumed: the one the statement speaks of is the one Stacks 06YU constructs.

theorem hasTorAmplitude_canonical_iff_exists_flatRepresentative
    (E : RingedSite.DerivedModules.{u, u, u, d} X) (a b : ℤ) (hab : a ≤ b) :
    letI : HasSheafify X.J AddCommGrpCat.{u} := inferInstance
    letI : X.J.WEqualsLocallyBijective AddCommGrpCat.{u} := inferInstance
    letI := Stacks.SheafOfModules.Tensor.sheafTensor_obj_additive.{u, u, u, u, u} X.O
    HasTorAmplitude (Stacks.SheafOfModules.canonicalDerivedTensorProduct.{u, u, d} X) E a b ↔
      ∃ K : CochainComplex (RingedSite.Modules.{u, u, u} X) ℤ,
        (∀ i : ℤ, AlgebraicGeometry.SheafOfModules.IsFlat.{u, u, u, u}
          (O := X.O) (K.X i)) ∧
        (∀ i : ℤ, i ∉ Set.Icc a b → IsZero (K.X i)) ∧
        Nonempty (DerivedCategory.Q.obj K ≅ E)

Tag 0F1M, a lemma

Tag 0F1M in the Stacks Project.

Stacks.SheafOfModules.hasTorAmplitudeGE_iff_exists_kFlatRepresentative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/TorAmplitude/BoundedBelowCanonical.lean, line 64. The attribute's comment: “equivalence”.

Stacks 0F1M. Let (C, O) be a ringed site, E an object of D(O) and a an integer. Then E has Tor amplitude in [a, ∞] for the derived tensor product of D(O) — that is, E ⊗^L_O F[0] has no cohomology below a for every O-module F — if and only if E is represented by a K-flat complex of flat O-modules vanishing in every degree below a.

theorem hasTorAmplitudeGE_iff_exists_kFlatRepresentative
    (E : RingedSite.DerivedModules.{u, u, u, d} X) (a : ℤ) :
    letI : X.J.WEqualsLocallyBijective AddCommGrpCat.{u} := inferInstance
    DerivedTensorProduct.HasTorAmplitudeGE (canonicalDerivedTensorProduct.{u, u, d} X) E a ↔
      ∃ K : CochainComplex (RingedSite.Modules.{u, u, u} X) ℤ,
        IsKFlat X.O K ∧
        (∀ i : ℤ, AlgebraicGeometry.SheafOfModules.IsFlat.{u, u, u, u} (O := X.O) (K.X i)) ∧
        (∀ i : ℤ, i < a → IsZero (K.X i)) ∧
        Nonempty (DerivedCategory.Q.obj K ≅ E)

Stacks.SheafOfModules.exists_pullbackStable_kFlatRepresentative_of_hasTorAmplitudeGE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/TorAmplitude/BoundedBelowCanonical.lean, line 85. The attribute's comment: “the Moreover clause: the representative stays K-flat, and keeps flat terms, under pullback”.

Stacks 0F1M, the "moreover" clause. An object E of D(O) with Tor amplitude in [a, ∞] for the derived tensor product of D(O) is represented by a complex K which is K-flat, has flat terms and vanishes in every degree below a, and which moreover stays K-flat with flat terms under pullback: for every morphism f of ringed topoi into (C, O) presented by a morphism of sites, the degreewise pullback f^*K is K-flat and each of its terms is flat.

theorem exists_pullbackStable_kFlatRepresentative_of_hasTorAmplitudeGE
    (E : RingedSite.DerivedModules.{u, u, u, d} X) (a : ℤ)
    (hE :
      letI : X.J.WEqualsLocallyBijective AddCommGrpCat.{u} := inferInstance
      DerivedTensorProduct.HasTorAmplitudeGE
        (canonicalDerivedTensorProduct.{u, u, d} X) E a) :
    letI : X.J.WEqualsLocallyBijective AddCommGrpCat.{u} := inferInstance
    ∃ K : CochainComplex (RingedSite.Modules.{u, u, u} X) ℤ,
      IsKFlat X.O K ∧
      (∀ i : ℤ, AlgebraicGeometry.SheafOfModules.IsFlat.{u, u, u, u} (O := X.O) (K.X i)) ∧
      (∀ i : ℤ, i < a → IsZero (K.X i)) ∧
      Nonempty (DerivedCategory.Q.obj K ≅ E) ∧
      ∀ X' : AlgebraicGeometry.RingedTopos.{u, u, u},
        letI : X'.J.WEqualsLocallyBijective AddCommGrpCat.{u} := inferInstance
        ∀ f : AlgebraicGeometry.RingedToposSiteHom X' (RingedSite.ringedTopos X),
          f.u.IsMorphismOfSites (RingedSite.ringedTopos X).J X'.J →
            IsKFlat X'.O
                ((Stacks.Sheaves.DerivedPullback.KFlatPullback.pullbackComplex f).obj K) ∧
              ∀ i : ℤ, AlgebraicGeometry.SheafOfModules.IsFlat.{u, u, u, u} (O := X'.O)
                (((Stacks.Sheaves.DerivedPullback.KFlatPullback.pullbackComplex f).obj K).X i)

Tag 08H5, a lemma

Tag 08H5 in the Stacks Project.

Stacks.SheafOfModules.DerivedTensorProduct.hasTorAmplitude_derivedPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/TorAmplitude/DerivedPullbackAlongRingedTopoi.lean, line 152.

Stacks 08H5. The derived pullback along a morphism of ringed topoi preserves Tor amplitude in a fixed interval.

A degenerate interval b < a says that the derived tensor products of E with every module vanish in every degree, so in particular E has Tor amplitude in the one-point interval [i + 1, i + 1] for whichever degree i is being examined, and hasTorAmplitude_derivedPullback_of_le applies there.

theorem hasTorAmplitude_derivedPullback
    (T : DerivedTensorProduct Y.toRingedSite) (T' : DerivedTensorProduct X.toRingedSite)
    (E : RingedSite.DerivedModules Y.toRingedSite) (a b : ℤ)
    (hamp : HasTorAmplitude T E a b) :
    HasTorAmplitude T' ((derivedPullback f).obj E) a b

Tag 08G2, a lemma

Tag 08G2 in the Stacks Project.

Stacks.SheafOfModules.DerivedTensorProduct.hasTorAmplitude_obj₃, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/TorAmplitude/DistinguishedTriangles.lean, line 60. The attribute's comment: “(1)”.

Stacks 08G2 (1). In a distinguished triangle K ⟶ L ⟶ M ⟶ K[1] of D(O), 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₃
    (tri : Triangle (RingedSite.DerivedModules.{u, v, w, d} X))
    (htri : tri ∈ distinguishedTriangles) (a b : ℤ)
    (hK : HasTorAmplitude T tri.obj₁ (a + 1) (b + 1))
    (hL : HasTorAmplitude T tri.obj₂ a b) :
    HasTorAmplitude T tri.obj₃ a b

Stacks.SheafOfModules.DerivedTensorProduct.hasTorAmplitude_obj₂, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/TorAmplitude/DistinguishedTriangles.lean, line 78. The attribute's comment: “(2)”.

Stacks 08G2 (2). In a distinguished triangle K ⟶ L ⟶ M ⟶ K[1] of D(O), if K and M both have Tor amplitude in [a, b], then so does L.

theorem hasTorAmplitude_obj₂
    (tri : Triangle (RingedSite.DerivedModules.{u, v, w, d} X))
    (htri : tri ∈ distinguishedTriangles) (a b : ℤ)
    (hK : HasTorAmplitude T tri.obj₁ a b)
    (hM : HasTorAmplitude T tri.obj₃ a b) :
    HasTorAmplitude T tri.obj₂ a b

Stacks.SheafOfModules.DerivedTensorProduct.hasTorAmplitude_obj₁, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/TorAmplitude/DistinguishedTriangles.lean, line 96. The attribute's comment: “(3)”.

Stacks 08G2 (3). In a distinguished triangle K ⟶ L ⟶ M ⟶ K[1] of D(O), 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₁
    (tri : Triangle (RingedSite.DerivedModules.{u, v, w, d} X))
    (htri : tri ∈ distinguishedTriangles) (a b : ℤ)
    (hL : HasTorAmplitude T tri.obj₂ (a + 1) (b + 1))
    (hM : HasTorAmplitude T tri.obj₃ a b) :
    HasTorAmplitude T tri.obj₁ (a + 1) (b + 1)

Tag 09JA, a lemma

Tag 09JA in the Stacks Project.

Stacks.SheafOfModules.DerivedTensorProduct.hasTorAmplitude_tensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/TorAmplitude/TensorProduct.lean, line 178.

Stacks 09JA. If K has Tor amplitude in [a, b] and L has Tor amplitude in [c, d], then K ⊗^L_O L has Tor amplitude in [a + c, b + d].

A degenerate interval is replaced by a one-point interval chosen below the degree under consideration, which is a weaker hypothesis, and hasTorAmplitude_tensor_of_le applies.

theorem hasTorAmplitude_tensor (a b c d : ℤ)
    (hK : HasTorAmplitude T K a b) (hL : HasTorAmplitude T L c d) :
    HasTorAmplitude T ((T.tensor.obj K).obj L) (a + c) (b + d)

Tag 08G3, a lemma

Tag 08G3 in the Stacks Project.

Stacks.SheafOfModules.DerivedTensorProduct.hasTorAmplitude_of_biprod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/TorAmplitude/DirectSummands.lean, line 79.

Stacks 08G3. If the direct sum K ⊕ L of two objects of D(O) has Tor amplitude in [a, b], then both K and L have Tor amplitude in [a, b].

theorem hasTorAmplitude_of_biprod (K L : RingedSite.DerivedModules.{u, v, w, d} X) (a b : ℤ)
    (h : HasTorAmplitude T (K ⊞ L) a b) :
    HasTorAmplitude T K a b ∧ HasTorAmplitude T L a b

Tag 0942, a lemma

Tag 0942 in the Stacks Project.

Stacks.Sites.isUniformlyBoundedAbove_tensor_adicQuotientModule_of_isBoundedAbove, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/TorAmplitude/AdicQuotientsBoundedAbove.lean, line 83. The attribute's comment: “uniformly bounded above”.

If K ⊗^L_O O/I is bounded above then K ⊗^L_O O/Iⁿ is uniformly bounded above: one integer bounds the cohomology of every K ⊗^L_O O/Iⁿ from above. The graded pieces Iⁿ/Iⁿ⁺¹ are killed by I, hence all bounded above by the bound of K ⊗^L_O O/I after tensoring with K, and the tower 0 → Iⁿ/Iⁿ⁺¹ → O/Iⁿ⁺¹ → O/Iⁿ → 0 carries that bound to every quotient.

theorem isUniformlyBoundedAbove_tensor_adicQuotientModule_of_isBoundedAbove
    (hQ : Stacks.DerivedCategory.IsBoundedAbove
      ((T.tensor.obj K).obj
        ((DerivedCategory.singleFunctor (RingedSite.Modules.{u, u, u} X) 0).obj
          (adicQuotientModule I 1))))
    :
    Stacks.DerivedCategory.IsUniformlyBoundedAbove
      (fun n : ℕ => (T.tensor.obj K).obj
        ((DerivedCategory.singleFunctor (RingedSite.Modules.{u, u, u} X) 0).obj
          (adicQuotientModule I n)))

Stacks.Sites.hasTorAmplitude_adicQuotient_of_hasTorAmplitude_adicQuotientOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/TorAmplitude/AdicQuotientsTorAmplitude.lean, line 135. The attribute's comment: “tor amplitude modulo every power of the ideal”.

Stacks 0942 part (2). If K ⊗^L_O O/I has Tor amplitude in [a, b] as an object of D(O/I), then K ⊗^L_O O/Iⁿ has Tor amplitude in [a, b] as an object of D(O/Iⁿ), for every n.

A sheaf F of O/Iⁿ-modules is tested by moving (K ⊗^L_O O/Iⁿ) ⊗^L_{O/Iⁿ} F[0] to D(O): restriction of scalars reflects a vanishing cohomology sheaf, and the projection formula at O ⟶ O/Iⁿ identifies the restriction with K ⊗^L_O F|_O. There the filtration of F|_O by the powers of I reaches zero, so the vanishing follows from the one at the sheaves of O-modules killed by I, which is the hypothesis.

theorem hasTorAmplitude_adicQuotient_of_hasTorAmplitude_adicQuotientOne
    (T : Stacks.SheafOfModules.DerivedTensorProduct.{u, u, u, _} X)
    (T₁ : Stacks.SheafOfModules.DerivedTensorProduct.{u, u, u, _}
      (adicQuotientRingedSite X I 1))
    (n : ℕ)
    (Tₙ : Stacks.SheafOfModules.DerivedTensorProduct.{u, u, u, _}
      (adicQuotientRingedSite X I n))
    (K : RingedSite.DerivedModules.{u, u, u, _} X) (a b : ℤ)
    (h : HasTorAmplitude T₁
      ((Stacks.Cohomology.derivedCoefficientChange (toAdicQuotient I 1)).obj K) a b) :
    HasTorAmplitude Tₙ
      ((Stacks.Cohomology.derivedCoefficientChange (toAdicQuotient I n)).obj K) a b

Tag 0DJJ, a lemma

Tag 0DJJ in the Stacks Project.

Stacks.SheafOfModules.DerivedTensorProduct.hasTorAmplitudeCanonical_derivedModuleFiber_canonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/TorAmplitude/StalksCanonical.lean, line 66. The attribute's comment: “part (1)”. References: SGA 6 I (5.6.2), “fiber direction”; SGA 6 III (3.3), “(i)=>(ii), f=id”; SGA 4 XVII (4.2.8), “(iii) f=id, forward”.

If an object E of D(O) has Tor amplitude in [a, b] for the derived tensor product of the ringed site, then for every point Φ of the site its derived stalk E_Φ has Tor amplitude in [a, b] as an object of D(O_Φ).

theorem hasTorAmplitudeCanonical_derivedModuleFiber_canonical
    (E : RingedSite.DerivedModules.{u, w, w, d} Y) (a b : ℤ)
    (hamp : HasTorAmplitude
      (Stacks.SheafOfModules.canonicalDerivedTensorProduct.{u, w, d} Y) E a b)
    (Φ : Y.J.Point.{w}) :
    letI : HasDerivedCategory.{d}
        (SheafOfModules.{w} (Stacks.commRingSheafToRingSheaf.{w, u, w} Y.O)) := hd
    StacksDraft.TorAmplitude.HasTorAmplitudeCanonical
      ((Φ.presheafFiber (A := CommRingCat.{w})).obj Y.O.obj)
      ((Stacks.derivedModuleFiber Φ Y.O).obj E) a b

Stacks.SheafOfModules.DerivedTensorProduct.hasTorAmplitude_canonical_of_forall_derivedModuleFiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/TorAmplitude/StalksCanonical.lean, line 84. The attribute's comment: “part (2)”. References: SGA 6 I (5.6.2), “converse, enough points”; SGA 6 III (3.3), “(ii)=>(i), f=id”; SGA 4 XVII (4.2.8), “(iii) f=id, converse”.

On a ringed site whose underlying site has a conservative family of points, an object E of D(O) has Tor amplitude in [a, b] for the derived tensor product of the site as soon as its derived stalk at every point of the site does.

theorem hasTorAmplitude_canonical_of_forall_derivedModuleFiber
    (E : RingedSite.DerivedModules.{u, w, w, d} Y) (a b : ℤ)
    (hY : Y.J.HasConservativeFamily.{w})
    (hE : ∀ Φ : Y.J.Point.{w},
      letI : HasDerivedCategory.{d}
          (SheafOfModules.{w} (Stacks.commRingSheafToRingSheaf.{w, u, w} Y.O)) := hd
      StacksDraft.TorAmplitude.HasTorAmplitudeCanonical
        ((Φ.presheafFiber (A := CommRingCat.{w})).obj Y.O.obj)
        ((Stacks.derivedModuleFiber Φ Y.O).obj E) a b) :
    HasTorAmplitude (Stacks.SheafOfModules.canonicalDerivedTensorProduct.{u, w, d} Y) E a b

Sources

• Section 21.46, Tag 08FY
• AxiomMath/Stacks at 5ed82d14

LeanStacks.SheafOfModules.DerivedTensorProduct.HasTorAmplitude · Stacks.SheafOfModules.DerivedTensorProduct.HasFiniteTorDimension · Stacks.SheafOfModules.DerivedTensorProduct.HasTorDimensionLE · Stacks.SheafOfModules.DerivedTensorProduct.hasTorAmplitude_of_coversTop · Stacks.SheafOfModules.DerivedTensorProduct.hasFiniteTorDimension_of_locallyHasFiniteTorDimension · Stacks.SheafOfModules.DerivedTensorProduct.LocallyHasFiniteTorDimension · Stacks.SheafOfModules.DerivedTensorProduct.isFlat_cokernel_of_hasTorAmplitude · Stacks.SheafOfModules.DerivedTensorProduct.isFlat_cokernel_of_hasTorAmplitude_canonical

Section21.47 Perfect complexes#

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

Tag 08G5, a definition

Tag 08G5 in the Stacks Project.

AlgebraicGeometry.RingedSite.IsPerfectComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/PerfectObjects.lean, line 66. The attribute's comment: “perfect complexes”.

Stacks 08G5, perfect complexes. A complex E of O-modules is perfect if every object U of the site admits a covering {V → U} over each member of which there are a strictly perfect complex P of O|_V-modules and a quasi-isomorphism P ⟶ E|_V.

noncomputable def IsPerfectComplex
    (E : CochainComplex (SheafOfModules.{m} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ) :
    Prop

AlgebraicGeometry.RingedSite.IsPerfect, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/PerfectObjects.lean, line 113. The attribute's comment: “perfect derived-category objects”.

Stacks 08G5, perfect objects of the derived category. An object of D(O) is perfect if it is isomorphic to the image of a perfect complex.

noncomputable def IsPerfect
    [HasDerivedCategory.{d} (SheafOfModules.{m} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))]
    (K : DerivedCategory (SheafOfModules.{m} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
    Prop

Tag 08G6, a lemma

Tag 08G6 in the Stacks Project.

AlgebraicGeometry.RingedSite.isPerfect_of_coveringFamily_strictlyPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/LocalModels.lean, line 250. The attribute's comment: “local_strictly_perfect_implies_perfect”.

Stacks 08G6, part (1). Let (C, O) be a ringed site whose underlying category has a final object T and let E be an object of D(O). If there are a covering {V → T}, strictly perfect complexes P_V of O|_V-modules and isomorphisms P_V ≅ E|_V in D(O|_V), then E is perfect.

theorem isPerfect_of_coveringFamily_strictlyPerfect
    (T : X.C) (hT : IsTerminal T)
    (E : DerivedCategory (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (h : ∃ S : Presieve T, Sieve.generate S ∈ X.J T ∧
      ∀ ⦃V : X.C⦄ (f : V ⟶ T), S f →
        ∃ P : CochainComplex
            (SheafOfModules.{w} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over V)) ℤ,
          IsStrictlyPerfect ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over V) P ∧
            Nonempty (DerivedCategory.Q.obj P ≅
              (SheafOfModules.overFunctor.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)
                V).mapDerivedCategory.obj E)) :
    X.IsPerfect E

AlgebraicGeometry.RingedSite.isPerfect_of_coveringFamily_strictlyPerfect_general, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/LocalModelsGeneral.lean, line 152. The attribute's comment: “local_strictly_perfect_implies_perfect”.

Let (C, O) be a ringed site whose underlying category has a final object T and let E be an object of D(O). If there are a covering {V → T}, strictly perfect complexes P_V of O|_V-modules and isomorphisms P_V ≅ E|_V in D(O|_V), then E is perfect.

theorem isPerfect_of_coveringFamily_strictlyPerfect_general
    (T : X.C) (hT : IsTerminal T)
    (E : DerivedCategory (SheafOfModules.{w}
      (Stacks.SheafOfModules.Tensor.ringSheaf.{u, v, w} X.O)))
    (h : ∃ S : Presieve T, Sieve.generate S ∈ X.J T ∧
      ∀ ⦃V : X.C⦄ (f : V ⟶ T), S f →
        ∃ P : CochainComplex
            (SheafOfModules.{w} ((Stacks.SheafOfModules.Tensor.ringSheaf.{u, v, w} X.O).over V)) ℤ,
          IsStrictlyPerfect ((Stacks.SheafOfModules.Tensor.ringSheaf.{u, v, w} X.O).over V) P ∧
            Nonempty (DerivedCategory.Q.obj P ≅
              (SheafOfModules.overFunctor.{w} (Stacks.SheafOfModules.Tensor.ringSheaf.{u, v, w} X.O)
                V).mapDerivedCategory.obj E)) :
    X.IsPerfect E

AlgebraicGeometry.RingedSite.isPerfectComplex_of_isPerfect_representation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/Representatives.lean, line 100. The attribute's comment: “perfect_independent_of_representative”.

Stacks 08G6, part (2). Let (C, O) be a ringed site and let K be a perfect object of D(O). Then every complex of O-modules representing K is a perfect complex.

theorem isPerfectComplex_of_isPerfect_representation
    {K : DerivedCategory (SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))}
    (hK : X.IsPerfect K)
    {F : CochainComplex (SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ}
    (hF : Nonempty (DerivedCategory.Q.obj F ≅ K)) :
    X.IsPerfectComplex F

Tag 08G7, a lemma

Tag 08G7 in the Stacks Project.

Stacks.SheafOfModules.DerivedTensorProduct.torAmplitudePerfectnessCriterion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/TorAmplitude/PerfectnessCriterion.lean, line 288. References: SGA 6 I (5.8), “(ii) ⟹ (i)”.

Stacks 08G7. Let (C, O) be a ringed site and let T be a derived tensor product on D(O). An object of D(O) with Tor amplitude in [a, b] for T, with a ≤ b, which is (a - 1)-pseudo-coherent, is perfect.

The proof reads Tor amplitude on each slice (C/U, O|_U), which needs a derived tensor product there; that is the derived tensor product of Stacks 06YU, Stacks.SheafOfModules.canonicalDerivedTensorProduct, which exists on each slice under the hypotheses already in force, so it is not a parameter of the statement.

theorem torAmplitudePerfectnessCriterion
    (T : DerivedTensorProduct.{0, 0, 0, d} Z) :
    TorAmplitudePerfectnessCriterion T

Tag 08G8, a lemma

Tag 08G8 in the Stacks Project.

Stacks.SheafOfModules.DerivedTensorProduct.isPerfect_iff_isPseudoCoherent_and_locallyHasFiniteTorDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/PerfectnessCriterion.lean, line 195. References: SGA 6 I (5.8.1).

Let (C, O) be a ringed site. An object of D(O) is perfect if and only if it is pseudo-coherent and locally has finite Tor dimension, measured on each slice (C/U, O|_U) against the derived tensor product Stacks.SheafOfModules.canonicalDerivedTensorProduct.

theorem isPerfect_iff_isPseudoCoherent_and_locallyHasFiniteTorDimension
    (E : RingedSite.DerivedModules.{0, 0, 0, d} Z) :
    Z.IsPerfect E ↔ Z.IsPseudoCoherent E ∧
      LocallyHasFiniteTorDimension
        (fun U : Z.C => canonicalDerivedTensorProduct.{0, 0, d} (Z.over U)) E

Stacks.Cohomology.TorAmplitude.hasFiniteTorDimension_of_ringedSite_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/TorAmplitude/FiniteTorDimensionOfAPerfectObject.lean, line 180. The attribute's comment: “a perfect object has finite tor dimension, globally on a quasi-compact space”. References: SGA 6 0 (3.1), “partial”; SGA 6 I (8.5), “partial”; SGA 6 III (4.2), “special case”.

Stacks 08G8 globally, on a quasi-compact ringed space. An object of D(O_X) which is perfect for the site of opens of X has finite Tor dimension against any derived tensor product datum of Stacks 06YU on that site.

Perfectness is transported to the ringed-space spelling by Stacks.Cohomology.PerfectComplexes.isPerfect_of_ringedSite, which is what makes the Tor-amplitude machinery applicable; locallyHasFiniteTorDimension_of_isPerfect then supplies the local intervals, quasi-compactness makes them one interval, and the bridge reads it against T.

theorem hasFiniteTorDimension_of_ringedSite_isPerfect [CompactSpace X.carrier]
    (T : Stacks.SheafOfModules.DerivedTensorProduct.{u, u, u, d}
      (AlgebraicGeometry.RingedSpace.ringedSite X))
    (E : DerivedCategory (OXMod.{u, u} X))
    (hE : (AlgebraicGeometry.RingedSpace.ringedSite X).IsPerfect E) :
    Stacks.SheafOfModules.DerivedTensorProduct.HasFiniteTorDimension
      (X := AlgebraicGeometry.RingedSpace.ringedSite X) T E

Tag 08H6, a lemma

Tag 08H6 in the Stacks Project.

AlgebraicGeometry.RingedSite.Hom.isPerfect_derivedPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/DerivedPullbackAlongRingedTopoi.lean, line 259.

Stacks 08H6. The derived pullback along a morphism of ringed sites of a perfect object of D(O') is perfect.

Stacks 08H2 makes the objects u(W) cover the final object of Sh(C), and CategoryTheory.GrothendieckTopology.coversTop_obj_subtype refines that covering to the u(W) over which K carries a strictly perfect derived model. Over such an object the pullback of the model is a strictly perfect derived model of (Lf^* E)|_{u(W)} (hasStrictlyPerfectModel_image), and it descends along any arrow into u(W) by exactness of restriction (hasStrictlyPerfectModel_of_hom), which is what the arrows of that covering supply; Stacks 08G6 (1) assembles.

theorem Hom.isPerfect_derivedPullback
    (E : DerivedCategory
      (SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf (ringedTopos Y).O)))
    (hE : Y.IsPerfect E) :
    X.IsPerfect ((derivedPullback f.toRingedToposSiteHom).obj E)

Tag 08G9, a lemma

Tag 08G9 in the Stacks Project.

AlgebraicGeometry.RingedSite.isPerfect_obj₃_of_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/DistinguishedTriangles.lean, line 233. The attribute's comment: “third object”.

Stacks 08G9, third object. In a distinguished triangle of D(O), the third object is perfect if the first two are.

theorem isPerfect_obj₃_of_distinguished
    (T : Triangle
      (DerivedCategory (SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))))
    (hT : T ∈ distinguishedTriangles)
    (h₁ : X.IsPerfect T.obj₁) (h₂ : X.IsPerfect T.obj₂) :
    X.IsPerfect T.obj₃

AlgebraicGeometry.RingedSite.isPerfect_obj₂_of_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/DistinguishedTriangles.lean, line 280. The attribute's comment: “second object”.

Stacks 08G9, second object. In a distinguished triangle of D(O), the second object is perfect if the other two are.

theorem isPerfect_obj₂_of_distinguished
    (T : Triangle
      (DerivedCategory (SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))))
    (hT : T ∈ distinguishedTriangles)
    (h₁ : X.IsPerfect T.obj₁) (h₃ : X.IsPerfect T.obj₃) :
    X.IsPerfect T.obj₂

AlgebraicGeometry.RingedSite.isPerfect_obj₁_of_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/DistinguishedTriangles.lean, line 292. The attribute's comment: “first object”.

Stacks 08G9, first object. In a distinguished triangle of D(O), the first object is perfect if the other two are.

theorem isPerfect_obj₁_of_distinguished
    (T : Triangle
      (DerivedCategory (SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))))
    (hT : T ∈ distinguishedTriangles)
    (h₂ : X.IsPerfect T.obj₂) (h₃ : X.IsPerfect T.obj₃) :
    X.IsPerfect T.obj₁

Tag 09JB, a lemma

Tag 09JB in the Stacks Project.

AlgebraicGeometry.RingedSite.isPerfect_derivedTensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/DerivedTensorProduct.lean, line 282.

Stacks 09JB. Let (C, O) be a ringed site. If K and L are perfect objects of D(O), then so is K ⊗^{𝐋}_O L.

Representatives of the two objects are replaced by resolutions A and B which are K-flat on the site and on every slice of it, so that K ⊗^{𝐋} L is the class of Tot(A ⊗_O B). Above an object of the site lying under a member of the covering that the perfectness of the first factor supplies and a member of the one the second supplies, both factors have strictly perfect models; the total tensor complex of those models is strictly perfect and is a local model of Tot(A ⊗_O B). Stacks 08G6 (1) turns that family of local models into perfectness.

Stated for an arbitrary derived tensor product of Stacks 06YU, since only its comparison field is used.

theorem isPerfect_derivedTensorProduct
    (T : Stacks.DerivedTensor.RingedSite.DerivedTensorProduct X.O)
    (K L : DerivedCategory (SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (hK : X.IsPerfect K) (hL : X.IsPerfect L) :
    X.IsPerfect ((T.tensor.obj K).obj L)

AlgebraicGeometry.RingedSite.isPerfect_tensor_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/TensorOfPerfectObjects.lean, line 240. The attribute's comment: “if K, L are perfect objects of D(O), then so is K ⊗^L_O L, on any ringed site RingedSite.{u,u,u}”.

Stacks 09JB. Let (C, O) be a ringed site whose objects, morphisms and sections lie in one universe. If K and L are perfect objects of D(O), then so is K ⊗^{𝐋}_O L.

Representatives of the two objects are replaced by resolutions A and B which are K-flat on the site and on every slice of it, so that K ⊗^{𝐋} L is the class of Tot(A ⊗_O B). Above an object of the site lying under a member of the covering that the perfectness of the first factor supplies and a member of the one the second supplies, both factors have strictly perfect models; the total tensor complex of those models is strictly perfect and is a local model of Tot(A ⊗_O B). Stacks 08G6 (1) turns that family of local models into perfectness.

Stated for an arbitrary derived tensor product of Stacks 06YU, since only its comparison field is used.

theorem isPerfect_tensor_of_isPerfect
    (T : Stacks.DerivedTensor.RingedSite.DerivedTensorProduct X.O)
    (K L : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (hK : X.IsPerfect K) (hL : X.IsPerfect L) :
    X.IsPerfect ((T.tensor.obj K).obj L)

Tag 08GA, a lemma

Tag 08GA in the Stacks Project.

Stacks.SheafOfModules.DerivedTensorProduct.isPerfect_left_of_biprod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/DirectSummands.lean, line 188. The attribute's comment: “first summand”.

Stacks 08GA. Let (C, O) be a ringed site and let K and L be objects of D(O). If K ⊞ L is perfect, then so is K.

By Stacks 08G8 the biproduct is pseudo-coherent and locally has finite Tor dimension; Stacks 08FW gives the first condition for K and Stacks 08G3 the second, and Stacks 08G8 read backwards gives perfectness. Stacks 08G8 is read against the derived tensor product of Stacks 06YU on the slices and on the iterated slices; neither occurs in the statement.

theorem isPerfect_left_of_biprod
    (K L : RingedSite.DerivedModules.{0, 0, 0, d} Z) (h : Z.IsPerfect (K ⊞ L)) :
    Z.IsPerfect K

Stacks.SheafOfModules.DerivedTensorProduct.isPerfect_right_of_biprod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/DirectSummands.lean, line 201. The attribute's comment: “second summand”.

Stacks 08GA. If K ⊞ L is perfect, then so is L.

theorem isPerfect_right_of_biprod
    (K L : RingedSite.DerivedModules.{0, 0, 0, d} Z) (h : Z.IsPerfect (K ⊞ L)) :
    Z.IsPerfect L

Sources

• Section 21.47, Tag 08G4
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.RingedSite.IsPerfectComplex · AlgebraicGeometry.RingedSite.IsPerfect · AlgebraicGeometry.RingedSite.isPerfect_of_coveringFamily_strictlyPerfect · AlgebraicGeometry.RingedSite.isPerfect_of_coveringFamily_strictlyPerfect_general · AlgebraicGeometry.RingedSite.isPerfectComplex_of_isPerfect_representation · Stacks.SheafOfModules.DerivedTensorProduct.torAmplitudePerfectnessCriterion · Stacks.SheafOfModules.DerivedTensorProduct.isPerfect_iff_isPseudoCoherent_and_locallyHasFiniteTorDimension · Stacks.Cohomology.TorAmplitude.hasFiniteTorDimension_of_ringedSite_isPerfect

Section21.48 Duals#

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

Tag 0FPQ, a lemma

Tag 0FPQ in the Stacks Project.

Stacks.Cohomology.MonoidalComplexesOfModules.symmetricMonoidalComplexes, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Monoidal/ComplexesOfModules.lean, line 133. References: SGA 4 XVII (4.1.6), “⊗ on complexes”.

Complexes of modules on any ringed site form a symmetric monoidal category; its tensor bifunctor is totalized sheaf tensor.

public def symmetricMonoidalComplexes : SymmetricMonoidalComplexes R

Tag 0FPR, an example

Tag 0FPR in the Stacks Project.

Stacks.SheafOfModules.Strict.dualComplexOfLocallyStrictlyPerfect, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Duals/DualComplexOfALocallyStrictlyPerfectComplex.lean, line 157. The attribute's comment: “the construction of the complex 𝒢^• = SheafHom^•(ℱ^•, 𝒪) under the tag's OWN hypothesis — that every object of the site has a covering on whose members ℱ^• is strictly perfect — rather than under the termwise condition that Stacks.SheafOfModules.Strict.dualComplex assumes. The terms and the signed-transpose differential are dualComplex_X and dualComplex_d, through which this is the same complex. NOT the left-dual assertion of the tag, which for this same complex is Stacks.SheafOfModules.Strict.exactPairingDualComplexOfLocallyStrictlyPerfect: Stacks.SheafOfModules.Strict.exactPairingDualComplex proves it only for a complex vanishing outside one global finite set of degrees, and the hypothesis here bounds ℱ^• only locally, so η = ∑ ηₙ is a locally finite sum of morphisms and has to be produced from its components”.

The dual complex 𝒢^• = SheafHom^•(ℱ^•, 𝒪) of [Stacks, Tag 0FPR], under the hypothesis of the tag. Its degree-j term is the dual sheaf SheafHom(ℱ^{-j}, 𝒪) and its differential is the signed transpose d_𝒢^j = -(-1)^j (d_ℱ^{-j-1})^∨, exactly as in Stacks.SheafOfModules.Strict.dualComplex; what is new is that the hypothesis is the tag's own local one, not the termwise condition extracted from it.

def dualComplexOfLocallyStrictlyPerfect (hK : IsLocallyStrictlyPerfect R K) :
    CochainComplex (Mod R) ℤ

Stacks.SheafOfModules.Strict.dualComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Duals/DualComplexOfModules.lean, line 138. The attribute's comment: “the construction of the complex 𝒢^• = SheafHom^•(ℱ^•, 𝒪): its degree-j term is the dual sheaf SheafHom(ℱ^{-j}, 𝒪) of Tag 0FNY — the single surviving factor of the degree-j term of the Hom complex of Tag 0A8X into 𝒪 placed in degree zero — and its differential is the signed transpose d_𝒢^j = -(-1)^j (d_ℱ^{-j-1})^∨ of Tag 0FNK. The remaining assertion of the tag, that 𝒢^• with η = ∑ ηₙ and ε = ∑ εₙ is a left dual of ℱ^•, is Stacks.SheafOfModules.Strict.exactPairingDualComplex, and under the tag's OWN hypothesis Stacks.SheafOfModules.Strict.exactPairingDualComplexOfLocallyStrictlyPerfect. Only the termwise half of the tag's hypothesis is assumed here; the same complex under the tag's OWN hypothesis is Stacks.SheafOfModules.Strict.dualComplexOfLocallyStrictlyPerfect”. References: SGA 4 XVII (1.1.6), “special case”.

The dual complex 𝒢^• = SheafHom^•(ℱ^•, 𝒪) of [Stacks, Tag 0FPR]. Its degree-j term is the dual sheaf SheafHom(ℱ^{-j}, 𝒪) of [Stacks, Tag 0FNY], and its differential is the signed transpose d_𝒢^j = -(-1)^j (d_ℱ^{-j-1})^∨, the sign convention of [Stacks, Tag 0FNK].

def dualComplex : CochainComplex (Mod R) ℤ

Stacks.SheafOfModules.Strict.exactPairingDualComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Duals/DualComplexOfModules.lean, line 187. The attribute's comment: “the left-dual assertion: 𝒢^• with η = ∑ ηₙ and ε = ∑ εₙ, the coevaluations and evaluations of Tag 0FNY at the terms, satisfies the two triangle identities of Tag 0FFP in the monoidal category of complexes of Tag 0FPQ. The complex 𝒢^• is Stacks.SheafOfModules.Strict.dualComplex, whose terms and signed-transpose differential are dualComplex_X and dualComplex_d. NOT under the tag's own hypothesis: that every object has a covering on which ℱ^• is strictly perfect gives the termwise local finiteness assumed here, but boundedness only locally, whereas s is one global finite set of degrees. The same conclusion under the tag's own hypothesis, with η = ∑ ηₙ made sense of as a locally finite sum, is Stacks.SheafOfModules.Strict.exactPairingDualComplexOfLocallyStrictlyPerfect; the converse local boundedness is Stacks.SheafOfModules.Strict.isLocallyBounded_of_exactPairing”.

[Stacks, Tag 0FPR] for a complex of bounded support. Let ℱ^• be a complex of 𝒪-modules each of whose terms is, locally on the site, a direct summand of a finite free 𝒪-module, and suppose ℱ^• vanishes outside a finite set s of degrees. Then the complex 𝒢^• = SheafHom^•(ℱ^•, 𝒪), together with η = ∑ ηₙ and ε = ∑ εₙ assembled from the coevaluations and evaluations of [Stacks, Tag 0FNY], is a left dual of ℱ^• in the monoidal category of complexes of 𝒪-modules of [Stacks, Tag 0FPQ]: both triangle identities hold.

def exactPairingDualComplex (s : Finset ℤ) (hb : ∀ m, m ∉ s → IsZero (F.X m)) :
    @ExactPairing _ _ (monoidalCategoryCochainComplex R) F (dualComplex R F hF)

Stacks.SheafOfModules.Strict.exactPairingDualComplexOfLocallyStrictlyPerfect, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Duals/LeftDualOfALocallyStrictlyPerfectComplex.lean, line 251. The attribute's comment: “the WHOLE assertion of the tag under the tag's OWN hypothesis: for a complex ℱ^• of 𝒪-modules such that every object of the site has a covering on whose members ℱ^• is strictly perfect (Tag 08FL), the complex 𝒢^• = SheafHom^•(ℱ^•, 𝒪) together with η = ∑ ηₙ and ε = ∑ εₙ — the coevaluations and evaluations of Tag 0FNY at the terms — is a left dual of ℱ^• in the monoidal category of complexes of Tag 0FPQ, i.e. both triangle identities of Tag 0FFP hold. No boundedness is assumed: Stacks.SheafOfModules.Strict.exactPairingDualComplex proves the same conclusion only for a complex vanishing outside one global finite set of degrees, and the hypothesis here bounds ℱ^• only locally, so that η = ∑ ηₙ is a locally finite sum. It is produced from its components, the degree-zero part of ℱ^• ⊗ 𝒢^• being a coproduct of locally finitely many nonzero summands and therefore also their product (Stacks.SheafOfModules.CoproductSheafification.isIso_coprodToProd). The complex 𝒢^• is Stacks.SheafOfModules.Strict.dualComplexOfLocallyStrictlyPerfect, with terms and signed-transpose differential dualComplexOfLocallyStrictlyPerfect_X and dualComplex_d. The converse, that a complex with a left dual is locally strictly perfect and has this very complex with these very pairings as its left dual, is Tag 0FPS, Stacks.SheafOfModules.Strict.exists_dualComplexIso_of_exactPairing”.

[Stacks, Tag 0FPR]. Let (C, 𝒪) be a ringed site and let ℱ^• be a complex of 𝒪-modules such that for every object U of C there exists a covering {U_i → U} with ℱ^•|_{U_i} strictly perfect. Then the complex 𝒢^• = SheafHom^•(ℱ^•, 𝒪), together with η = ∑ ηₙ and ε = ∑ εₙ assembled from the coevaluations and evaluations of [Stacks, Tag 0FNY] at the terms, is a left dual of ℱ^• in the monoidal category of complexes of 𝒪-modules of [Stacks, Tag 0FPQ]: both triangle identities hold.

The hypothesis is the tag's own and nothing else is assumed: in particular ℱ^• is bounded only locally, so η is only a locally finite sum. It exists because the degree-zero part of ℱ^• ⊗ 𝒢^• is a coproduct whose summands locally all but finitely many vanish, hence is also the product, and a morphism into it is given by — and determined by — its components.

def exactPairingDualComplexOfLocallyStrictlyPerfect (hK : IsLocallyStrictlyPerfect R K) :
    @ExactPairing _ _ (monoidalCategoryCochainComplex R) K
      (dualComplexOfLocallyStrictlyPerfect R K hK)

Stacks.SheafOfModules.termwiseExactPairingDualSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Duals/TermwiseDualsOfAComplexOfModules.lean, line 155. The attribute's comment: “the degreewise pairings only: for each n the dual sheaf SheafHom(ℱⁿ, 𝒪) is a left dual of the term ℱⁿ, with the coevaluation ηₙ and evaluation εₙ of Tag 0FNY, in the monoidal category of 𝒪-modules Strict.monoidalCategory. NOT the assertion of the tag, which is about the complex 𝒢^• = SheafHom^•(ℱ^•, 𝒪): neither the sums η = ∑ ηₙ and ε = ∑ εₙ, nor the triangle identities for them, nor the left-dual property of 𝒢^• in the monoidal category of complexes of Tag 0FPQ, is proved here. Those three are proved over a site by Stacks.SheafOfModules.Strict.dualComplex and Stacks.SheafOfModules.Strict.exactPairingDualComplex, for a complex of globally bounded support. The construction of 𝒢^• is available under the tag's own hypothesis, that every object has a covering on which ℱ^• is strictly perfect, as Stacks.SheafOfModules.Strict.dualComplexOfLocallyStrictlyPerfect, and the left-dual assertion under that hypothesis is Stacks.SheafOfModules.Strict.exactPairingDualComplexOfLocallyStrictlyPerfect. See the module's Implementation notes”.

[Stacks, Tag 0FPR], the degreewise pairings. For each degree n, the dual sheaf SheafHom(ℱ^n, 𝒪) is a left dual of the term ℱ^n in the monoidal category of 𝒪-modules: the coevaluation ηₙ : 𝒪 ⟶ ℱ^n ⊗ SheafHom(ℱ^n, 𝒪) and the evaluation εₙ : SheafHom(ℱ^n, 𝒪) ⊗ ℱ^n ⟶ 𝒪 of [Stacks, Tag 0FNY] satisfy the two triangle identities.

These are exactly the ηₙ and εₙ that [Stacks, Tag 0FPR] sums to form η and ε.

public def termwiseExactPairingDualSheaf
    (hF : IsTermwiseLocallyDirectSummandOfFiniteFree 𝒪 h𝒪 F) (n : ℤ) :
    ExactPairing (F.X n) (dualSheaf 𝒪 h𝒪 (F.X n))

Tag 0FPS, a lemma

Tag 0FPS in the Stacks Project.

Stacks.SheafOfModules.Strict.isLocallyStrictlyPerfect_and_isoDualComplex_of_exactPairing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Duals/ComplexWithALeftDual.lean, line 157. The attribute's comment: “the WHOLE tag, under the tag's OWN hypothesis that ℱ^• has a left dual 𝒢^• in the monoidal category of complexes of 𝒪-modules of Tag 0FPQ, whose tensor product is the one of Tag 01CA. Both conclusions: every object of the site has a covering on whose members ℱ^• is strictly perfect in the sense of Tag 08FL — the witness Stacks.SheafOfModules.Strict.IsLocallyStrictlyPerfect, unfolding to the covering sieve and IsStrictlyPerfect of the restricted complex — and 𝒢^• is the left dual of Example 0FPR with its pairings: it is isomorphic to Stacks.SheafOfModules.Strict.dualComplexOfLocallyStrictlyPerfect, the complex SheafHom^•(ℱ^•, 𝒪), by an isomorphism matching the coevaluation and the evaluation of the given pairing with those of Stacks.SheafOfModules.Strict.exactPairingDualComplexOfLocallyStrictlyPerfect, the η = ∑ ηₙ and ε = ∑ εₙ of that example — which is uniqueness of left duals (Tag 0FFR)”.

[Stacks, Tag 0FPS]. Let (C, 𝒪) be a ringed site and ℱ^• a complex of 𝒪-modules with a left dual 𝒢^• in the monoidal category of complexes of 𝒪-modules. Then every object of the site has a covering on whose members ℱ^• is strictly perfect, and the left dual is the complex of [Stacks, Tag 0FPR] together with its pairings.

theorem isLocallyStrictlyPerfect_and_isoDualComplex_of_exactPairing
    (p : @ExactPairing _ _ (monoidalCategoryCochainComplex R) K L) :
    letI := monoidalCategoryCochainComplex R
    letI := p
    letI := exactPairingDualComplexOfLocallyStrictlyPerfect
      (isLocallyStrictlyPerfect_of_exactPairing R K L p)
    IsLocallyStrictlyPerfect R K ∧
      ∃ 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 08JJ, a lemma

Tag 08JJ in the Stacks Project.

Stacks.SheafOfModules.isIso_tensorDualToSheafHom_of_localSummand, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorDualSheafHom.lean, line 543. The attribute's comment: “step (5) of the proof only: the canonical map F ⊗_𝒪 SheafHom(E, 𝒪) ⟶ SheafHom(E, F) is an isomorphism for E locally a summand of a finite free module and F arbitrary. None of the tag's four assertions is proved here; in particular the derived statement M ⊗^L_𝒪 K^∨ ≅ RSheafHom(K, M) for perfect K is not, and still needs a complex-level comparison with its Koszul signs, the tensor-side analogue of Tag 08JH, locality of the derived tensor product on a slice, and a K-flat representative on a ringed site.”. References: EGA 0 (5.4.2), “more general”; SGA 5 IIIB (5.0), “more general”.

Step (5) of the proof of Stacks 08JJ. Let (C, 𝒪) be a ringed site, let E be a sheaf of 𝒪-modules which is locally a direct summand of a finite free sheaf of modules, and let F be an arbitrary sheaf of 𝒪-modules. Then the canonical map

F ⊗_𝒪 SheafHom(E, 𝒪) ⟶ SheafHom(E, F)

is an isomorphism.

The map is Stacks.SheafOfModules.tensorDualToSheafHom, pinned down on local sections by Stacks.SheafOfModules.tensorDualToSheafHom_toTensorSheafSection. At E = F this is the first assertion of Tag 0FNY, Stacks.SheafOfModules.isIso_tensorDualToEndomorphism_of_localSummand.

The hypothesis is the one of Tag 0FNY, that E is a summand of a finite free module locally; Stacks 08JJ's step (5) asks for a global summand, which is a special case.

theorem isIso_tensorDualToSheafHom_of_localSummand
    (hE : IsLocallyDirectSummandOfFiniteFree 𝒪 h𝒪 E) :
    IsIso (tensorDualToSheafHom 𝒪 h𝒪 E F)

AlgebraicGeometry.RingedSite.isIso_derivedSheafHomEvaluation_of_coversTop, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/EvaluationLocality.lean, line 289. The attribute's comment: “the locality step for the evaluation morphism of Tag 0A97 only: invertibility of ev : RSheafHom(L, M) ⊗^L_O K ⟶ RSheafHom(RSheafHom(K, L), M), and hence of the bidual map K ⟶ (K^∨)^∨ of AlgebraicGeometry.RingedSite.derivedBidual, may be checked after restriction to the slices over a family of objects covering the final object, where it becomes quasi-isomorphy of the evaluation morphism of internal Hom complexes of Tag 0A92. NONE of the four assertions of Tag 08JJ is proved here and in particular the bidual map is NOT shown to be invertible for a perfect K: quasi-isomorphy over each member of the covering family is a HYPOTHESIS below. The base case that discharges it — that evaluationMap is a quasi-isomorphism when its source complex is strictly perfect (Tag 08FL) — is AlgebraicGeometry.RingedSite.quasiIso_evaluationMap_of_isStrictlyPerfect, and the second assertion of Tag 08JJ follows from the two together, in AlgebraicGeometry.RingedSite.isIso_derivedBidual_of_isPerfect. The reduction performed here is the same one Stacks.SheafOfModules.isIso_of_coversTop_mapDerivedCategory performs for an arbitrary morphism of D(Mod(O)), but carried out at the chain level, because the derived evaluation morphism has no restriction compatibility of its own; the chain-level square it uses is AlgebraicGeometry.RingedSite.evaluationMap_restrict_square”.

Invertibility of the evaluation morphism of derived internal Homs is local on the site. Let V : ι → C be a family of objects covering the final object of the site, let A be a K-flat complex representing K, and let B and C be K-injective complexes representing L and M. If the evaluation morphism of internal Hom complexes of Stacks 0A92 formed over each V i, at the restrictions of A, B and C, is a quasi-isomorphism, then the evaluation morphism of derived internal Homs of Stacks 0A97 at K, L, M is an isomorphism.

theorem isIso_derivedSheafHomEvaluation_of_coversTop
    (K L M : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    {A B C : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ}
    (hA : Stacks.SheafOfModules.IsKFlat X.O A) [B.IsKInjective] [C.IsKInjective]
    (eA : DerivedCategory.Q.obj A ≅ K) (eB : DerivedCategory.Q.obj B ≅ L)
    (eC : DerivedCategory.Q.obj C ≅ M)
    {ι : Type*} {V : ι → X.C} (hV : X.J.CoversTop V)
    (h : ∀ i, QuasiIso (evaluationMap (X.over (V i)) (restrictComplex X A (V i))
      (restrictComplex X B (V i)) (restrictComplex X C (V i)))) :
    IsIso (derivedSheafHomEvaluation X T Hd K L M)

AlgebraicGeometry.RingedSite.isIso_derivedBidual_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/EvaluationPerfect.lean, line 155. The attribute's comment: “the canonical map K ⟶ (K^∨)^∨ is an isomorphism for a perfect object K of D(O), where K^∨ is the derived dual RSheafHom_O(K, O); this is one of the four assertions of the tag, and the hypothesis is perfection of K alone”.

The bidual map of a perfect object is an isomorphism. For a perfect object K of D(O) the canonical map

K ⟶ (K^∨)^∨

of AlgebraicGeometry.RingedSite.derivedBidual is an isomorphism, where K^∨ is the derived dual RSheafHom(K, O).

theorem isIso_derivedBidual_of_isPerfect
    (K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (hK : X.IsPerfect K) :
    IsIso (derivedBidual X T K)

AlgebraicGeometry.RingedSite.isPerfect_derivedDual, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/Duals.lean, line 267. The attribute's comment: “the dual of a perfect object is perfect”. References: SGA 6 I (7.3), “perfect ⇒ dual perfect”; SGA 6 III (4.9), “Case S = X = Y”.

Stacks 08JJ, first assertion. Let (C, O) be a ringed site and let K be a perfect object of D(O). Then the dual K^∨ = RSheafHom(K, O) is perfect as well.

Perfectness is local, so it is enough to model K^∨ above a covering of each object of the site. 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) by Stacks 08JB, which is the class of the internal Hom complex SheafHom(E, O|_V) by Stacks 08JH; 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 (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (hK : X.IsPerfect K) : X.IsPerfect (derivedDual X K)

AlgebraicGeometry.RingedSite.derivedDualTensorSheafHomIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/DualTensorSheafHom.lean, line 196. The attribute's comment: “the isomorphism M ⊗^L_O K^∨ ≅ RSheafHom_O(K, M) for perfect K; not the invertibility of the canonical map of Stacks 08JD, which is a different morphism of the same type”.

Stacks 08JJ: tensoring with the dual of a perfect object is derived internal Hom. Let (C, O) be a ringed site, let K be a perfect object of D(O) with dual K^∨ = RSheafHom(K, O), and let M be an arbitrary object of D(O). Then

M ⊗^L_O K^∨ ≅ RSheafHom_O(K, M).

It is the diagonal morphism of Stacks 0BYS at tensor factor M, internal-Hom source K and target the structure sheaf in degree zero — invertible by Stacks 0ATN because K is perfect, its source being M ⊗^L_O RSheafHom(K, O) = M ⊗^L_O K^∨ — followed by the internal Hom out of K of the right unit constraint M ⊗^L_O O ≅ M of Stacks 0FPT.

def derivedDualTensorSheafHomIso
    (K M : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (hK : X.IsPerfect K) :
    ((Stacks.SheafOfModules.derivedTensorProductFunctor X).obj M).obj (derivedDual X K) ≅
      ((derivedSheafHomBifunctor X).obj (op K)).obj M

AlgebraicGeometry.RingedSite.derivedDualTensorSheafHomIso_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/DualTensorSheafHom.lean, line 212. The attribute's comment: “that isomorphism is functorial in M”.

Stacks 08JJ: the isomorphism is functorial in M. This is the functoriality the source asserts: the diagonal of Stacks 0BYS is natural in its tensor factor and the right unit constraint of Stacks 0FPT is natural, so the composite of the two is.

theorem derivedDualTensorSheafHomIso_naturality
    (K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (hK : X.IsPerfect K)
    {M M' : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))}
    (f : M ⟶ M') :
    ((Stacks.SheafOfModules.derivedTensorProductFunctor X).map f).app (derivedDual X K) ≫
        (derivedDualTensorSheafHomIso X K M' hK).hom =
      (derivedDualTensorSheafHomIso X K M hK).hom ≫
        ((derivedSheafHomBifunctor X).obj (op K)).map f

AlgebraicGeometry.RingedSite.derivedDualTensorGlobalSectionsEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/DualTensorSheafHom.lean, line 276. The attribute's comment: “the identification H⁰(C, M ⊗^L_O K^∨) = Hom_{D(O)}(K, M) for perfect K, as an isomorphism of abelian groups; not the bijectivity of the induced map of Stacks 08JD”.

Stacks 08JJ: H⁰(C, M ⊗^L_O K^∨) = Hom_{D(O)}(K, M) for perfect K. The degree-zero global hypercohomology of M ⊗^L_O K^∨ is the group of morphisms K ⟶ M in D(O).

It is the degree-zero global hypercohomology of derivedDualTensorSheafHomIso, which is an isomorphism of abelian groups because derived global sections and the degree-zero cohomology functor both preserve isomorphisms, followed by the identification H⁰(C, RSheafHom(K, M)) = Hom_{D(O)}(K, M) of Stacks 08JA.

def derivedDualTensorGlobalSectionsEquiv
    (K M : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (hK : X.IsPerfect K) :
    ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} 0).obj
        ((derivedModuleGlobalSections X).obj
          (((Stacks.SheafOfModules.derivedTensorProductFunctor X).obj M).obj
            (derivedDual X K))) : Type u) ≃+ (K ⟶ M)

AlgebraicGeometry.RingedSite.isIso_derivedTensorDualToSheafHom_of_isPerfect_canonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/DualTensorSheafHomCanonical.lean, line 482. The attribute's comment: “the canonical map M ⊗^L_O L^∨ ⟶ RSheafHom_O(L, M) of Stacks 08JD is an isomorphism for a perfect L”.

Stacks 08JJ, third assertion, for the canonical map of Stacks 08JD. Let (C, O) be a ringed site, let L be a perfect object of D(O) with dual L^∨ = RSheafHom(L, O) and let M be an arbitrary object of D(O). Then the canonical map

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

of Stacks 08JD, AlgebraicGeometry.RingedSite.derivedTensorDualToSheafHom, is an isomorphism.

The isomorphism itself was already in the library as AlgebraicGeometry.RingedSite.derivedDualTensorSheafHomIso, the diagonal of Stacks 0BYS at target object the structure sheaf; what is proved here is that the canonical map of Stacks 08JD is that diagonal, so that the invertibility supplied by Stacks 0ATN applies to it. The comparison is AlgebraicGeometry.RingedSite.derivedTensorDualToSheafHom_comp_derivedSheafHomComparison, whose chain-level content is AlgebraicGeometry.RingedSite.tensorHomInterchange_comp_homMap: the interchange morphism of Stacks 0BYR is the diagonal of Stacks 0A93 tensored with the identity followed by the composition morphism of Stacks 0A91, so no Koszul sign separates the two morphisms.

theorem isIso_derivedTensorDualToSheafHom_of_isPerfect_canonical
    (L M : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (hL : X.IsPerfect L) :
    IsIso (derivedTensorDualToSheafHom X
      (Stacks.SheafOfModules.canonicalDerivedTensorProduct X) L M)

Stacks.SheafOfModules.isIso_of_coversTop_mapDerivedCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Slice/DerivedIsomorphismLocality.lean, line 112. The attribute's comment: “the locality step of the proof only: invertibility of a morphism of D(Mod(O)) may be checked after restriction to the slices over a family of objects covering the final object. Stacks 08JJ uses this reduction twice, for the bidual map K ⟶ (K^∨)^∨ and for the canonical map M ⊗^L_O K^∨ ⟶ RSheafHom_O(K, M); neither of those maps is shown to be an isomorphism here, and none of the tag's four assertions is proved here.”.

Invertibility in the derived category of sheaves of modules is local on the site. Let V : ι → C be a family of objects covering the final object of the site. A morphism of D(Mod(R)) whose image under restriction to the slice site over each V i is an isomorphism is itself an isomorphism.

theorem isIso_of_coversTop_mapDerivedCategory {ι : Type*} {V : ι → C} (hV : J.CoversTop V)
    {K L : DerivedCategory (SheafOfModules.{w} R)} (f : K ⟶ L)
    (hf : ∀ i, IsIso ((SheafOfModules.overFunctor.{w} R (V i)).mapDerivedCategory.map f)) :
    IsIso f

Tag 0FPT, a lemma

Tag 0FPT in the Stacks Project.

Stacks.DerivedTensor.RingedSite.DerivedTensorProduct.braidingIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/DerivedSymmetryAndUnit.lean, line 116. The attribute's comment: “the commutativity constraint at a pair of objects, as an isomorphism; not the monoidal structure and not its coherence axioms”.

[Stacks, Tag 0FPT], the commutativity constraint. The derived tensor product of two objects of D(𝒪) is symmetric: A ⊗^L_𝒪 B ≅ B ⊗^L_𝒪 A.

Both objects are replaced by their chosen K-flat models, on which the derived tensor product is the ordinary total tensor complex; there the isomorphism is the Koszul symmetry Stacks.SheafOfModules.Tensor.tensorComplexFlipIso.

def braidingIso (A B : DerivedModules X.O) :
    (T.tensor.obj A).obj B ≅ (T.tensor.obj B).obj A

Stacks.DerivedTensor.RingedSite.DerivedTensorProduct.rightUnitIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/DerivedSymmetryAndUnit.lean, line 139. The attribute's comment: “the unit constraint on the right at an object, as an isomorphism; not the monoidal structure and not its coherence axioms”.

[Stacks, Tag 0FPT], the unit constraint on the right. The structure sheaf in degree zero is a unit for the derived tensor product: A ⊗^L_𝒪 𝒪 ≅ A.

The right factor is already K-flat by Stacks.SheafOfModules.isKFlat_single_unit, so only the left factor is replaced by its chosen K-flat model; on representatives the statement is the ordinary unit law Stacks.SheafOfModules.tensorComplexUnitIso.

def rightUnitIso (A : DerivedModules X.O) :
    (T.tensor.obj A).obj (unitObject X) ≅ A

Stacks.DerivedTensor.RingedSite.DerivedTensorProduct.leftUnitIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/DerivedSymmetryAndUnit.lean, line 154. The attribute's comment: “the unit constraint on the left at an object, as an isomorphism; not the monoidal structure and not its coherence axioms”.

[Stacks, Tag 0FPT], the unit constraint on the left. The structure sheaf in degree zero is a unit for the derived tensor product on the other side too: 𝒪 ⊗^L_𝒪 A ≅ A.

It is the right unit constraint read through the commutativity constraint.

def leftUnitIso (A : DerivedModules X.O) :
    (T.tensor.obj (unitObject X)).obj A ≅ A

Stacks.SheafOfModules.DerivedMonoidal.symmetricMonoidalDerivedTensor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Monoidal/DerivedTensorConstraints.lean, line 198.

The derived category of modules on a ringed site is a symmetric monoidal category with tensor product the derived tensor product and the usual associativity and commutativity constraints, the latter being those of the total tensor product of complexes with the Koszul sign convention.

public def symmetricMonoidalDerivedTensor : SymmetricMonoidalDerivedTensor R

Tag 0FPU, an example

Tag 0FPU in the Stacks Project.

AlgebraicGeometry.RingedSite.isIso_derivedTensorDualToSheafHom_self, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/DerivedDualLeftDual.lean, line 268. The attribute's comment: “tensor_hom_iso”. References: SGA 5 IIIB (5.0).

Stacks 0FPU: the canonical map K ⊗^𝐋_O K^∨ ⟶ R𝓗om_O(K, K) is an isomorphism. For a perfect object K of D(O) the canonical map of Stacks 08JD at M = K is invertible.

This is the assertion Stacks 0FPU cites, from [Stacks, Tag 08JJ], in order to define the coevaluation; the source states it only at M = K, which is the case registered here. The general statement, for an arbitrary target and an arbitrary derived tensor product datum, is AlgebraicGeometry.RingedSite.isIso_derivedTensorDualToSheafHom_of_isPerfect of StacksFrontier.Topology.Sheaves.Cohomology.InternalHom.DerivedCompositionPerfect, which is where the mathematics is; nothing is re-proved here.

theorem isIso_derivedTensorDualToSheafHom_self
    (K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (hK : X.IsPerfect K) :
    IsIso (derivedTensorDualToSheafHom X
      (Stacks.SheafOfModules.canonicalDerivedTensorProduct X) K K)

AlgebraicGeometry.RingedSite.coevaluation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/DerivedDualLeftDual.lean, line 290. The attribute's comment: “coevaluation”.

Stacks 0FPU: the coevaluation of a perfect object. For a perfect object K of D(O) with dual K^∨ = R𝓗om_O(K, O) the coevaluation is the morphism

η : O ⟶ K ⊗^𝐋_O K^∨

corresponding to id_K under the comparison K ⊗^𝐋_O K^∨ ≅ R𝓗om_O(K, K) of Stacks 08JD: the section corresponding to id_K (AlgebraicGeometry.RingedSite.derivedIdentitySection, the class of the identity under the two identifications of Stacks 08JA), followed by the inverse of that comparison.

This is AlgebraicGeometry.RingedSite.derivedDualCoevaluation, which takes the invertibility of the comparison as a hypothesis, with that hypothesis discharged for a perfect K by isIso_derivedTensorDualToSheafHom_self.

def coevaluation
    (K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (hK : X.IsPerfect K) :
    derivedStructureSheaf X ⟶
      ((Stacks.SheafOfModules.derivedTensorProductFunctor X).obj K).obj (derivedDual X K)

AlgebraicGeometry.RingedSite.evaluation_coevaluation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/DerivedDualLeftDual.lean, line 440. The attribute's comment: “left_dual”.

Stacks 0FPU, the triangle identity on the perfect object. For a perfect K, with the coevaluation η and the evaluation ε,

(η ▷ K) ≫ α ≫ (K ◁ ε) = λ ≫ ρ⁻¹.

The chain is (η ▷ K) ≫ α ≫ (K ◁ ε) ≫ ρ = ((η ≫ Φ) ▷ K) ≫ app = (ι ▷ K) ≫ app = λ, whose first step is (E1), whose middle step is monoidalCoevaluation_comp and whose last step is the unit law (UL), AlgebraicGeometry.RingedSite.derivedSheafHomCounit_unit_law_monoidal, at the section corresponding to id_K.

theorem evaluation_coevaluation
    (K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (hK : X.IsPerfect K) :
    monoidalCoevaluation X K hK ▷ K ≫ (α_ K (derivedDual X K) K).hom ≫
        K ◁ monoidalEvaluation X K = (λ_ K).hom ≫ (ρ_ K).inv

AlgebraicGeometry.RingedSite.derivedDualExactPairing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/DerivedDualLeftDual.lean, line 468. The attribute's comment: “left_dual”.

Stacks 0FPU: the derived dual of a perfect object is a left dual. For a perfect object K of D(O) the pair (η, ε) is an exact pairing — K^∨ = R𝓗om_O(K, O) is a left dual of K in the sense of [Stacks, Tag 0FFP] — in the monoidal structure of [Stacks, Tag 0FPT] on D(O).

Only the first triangle identity is checked: the second follows from it by CategoryTheory.ExactPairing.ofEvaluationCoevaluation, because the evaluation detects endomorphisms of K^∨ (eq_id_of_whiskerRight_comp_derivedDualEvaluation), which is what the closed structure of D(O) supplies.

def derivedDualExactPairing
    (K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (hK : X.IsPerfect K) : ExactPairing K (derivedDual X K)

AlgebraicGeometry.RingedSite.coevaluation_evaluation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/DerivedDualLeftDual.lean, line 482. The attribute's comment: “left_dual”.

Stacks 0FPU, the triangle identity on the derived dual. For a perfect K,

(K^∨ ◁ η) ≫ α⁻¹ ≫ (ε ▷ K^∨) = ρ ≫ λ⁻¹.

This is the second clause of derivedDualExactPairing, which CategoryTheory.ExactPairing.ofEvaluationCoevaluation derives from the first.

theorem coevaluation_evaluation
    (K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (hK : X.IsPerfect K) :
    derivedDual X K ◁ monoidalCoevaluation X K hK ≫
        (α_ (derivedDual X K) K (derivedDual X K)).inv ≫
        monoidalEvaluation X K ▷ derivedDual X K =
      (ρ_ (derivedDual X K)).hom ≫ (λ_ (derivedDual X K)).inv

AlgebraicGeometry.RingedSite.exists_exactPairing_derivedDual, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/DerivedDualLeftDual.lean, line 543. The attribute's comment: “left_dual”.

Stacks 0FPU: the derived dual of a perfect object is a left dual, on an arbitrary ringed site. Let (C, O) be a ringed site and K a perfect object of D(O), with dual K^∨ = R𝓗om_O(K, O), coevaluation η (the section corresponding to id_K under K ⊗^𝐋_O K^∨ ≅ R𝓗om_O(K, K)) and evaluation ε. Then (K^∨, η, ε) is a left dual of K in the monoidal category D(O) of [Stacks, Tag 0FPT], in the sense of [Stacks, Tag 0FFP]: there is an exact pairing between K and K^∨ whose coevaluation is η and whose evaluation is ε, that is, both triangle identities hold for η and ε.

The only hypothesis is the perfectness of K. The additivity of ⊗_O in each variable, the existence of the total tensor complexes, and sheafification of abelian sheaves on the site and on its slices hold for every ringed site, and are discharged here; the pairing is AlgebraicGeometry.RingedSite.derivedDualExactPairing.

theorem exists_exactPairing_derivedDual
    (K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)))
    (hK : Y.IsPerfect K) :
    ∃ P : ExactPairing K (derivedDual Y K),
      P.coevaluation' = monoidalCoevaluation Y K hK ∧
        P.evaluation' = monoidalEvaluation Y K

AlgebraicGeometry.RingedSite.derivedDualEvaluation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/DualityPairing.lean, line 210. The attribute's comment: “evaluation”.

Stacks 0FPU: the evaluation map. For an object K of D(O) with dual K^∨ = RSheafHom(K, O) the evaluation is the morphism

ε : K^∨ ⊗^L_O K ⟶ O

matched with the identity of K^∨ by the tensor–internal-Hom bijection of Stacks 08J8, under which morphisms K^∨ ⊗^L_O K ⟶ O are morphisms K^∨ ⟶ RSheafHom(K, O) = K^∨. No perfectness hypothesis is needed: evaluation exists for every object of D(O).

def derivedDualEvaluation
    (K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
    ((Stacks.SheafOfModules.derivedTensorProductFunctor X).obj (derivedDual X K)).obj K ⟶
      derivedStructureSheaf X

Tag 0FPV, a lemma

Tag 0FPV in the Stacks Project.

AlgebraicGeometry.RingedSite.isPerfect_and_isIso_derivedDualToLeftDual, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/LeftDualIsPerfect.lean, line 151. The attribute's comment: “both assertions: M is perfect, and the left dual N is the object RSheafHom(M, O) of Example 0FPU, by the morphism derivedDualToLeftDual which the pairing matches with the evaluation of Example 0FPU and which carries the evaluation of the pairing to that of Example 0FPU. The monoidal structure on D(O) is the one of Tag 0FPT, Stacks.SheafOfModules.DerivedMonoidal.derivedMonoidal, a left dual is Mathlib's CategoryTheory.ExactPairing (Definition 0FFP), and perfect is AlgebraicGeometry.RingedSite.IsPerfect (Definition 08G5)”.

Stacks 0FPV. Let (C, O) be a ringed site and let M be an object of D(O) with a left dual N in the symmetric monoidal category D(O) of Stacks 0FPT. Then M is perfect, and the left dual is the object M^∨ = RSheafHom(M, O) of Example 0FPU: the morphism M^∨ ⟶ N which the pairing matches with the evaluation of Example 0FPU is an isomorphism, and it carries the evaluation ε of the pairing to the evaluation ε' of Example 0FPU.

The first assertion is isPerfect_of_exactPairing, the second isIso_derivedDualToLeftDual together with whiskerRight_derivedDualToLeftDual.

theorem isPerfect_and_isIso_derivedDualToLeftDual
    (M N : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (pair : letI := derivedMonoidal X.O; ExactPairing M N) :
    X.IsPerfect M ∧
      (letI := derivedMonoidal X.O; letI := pair;
        IsIso (derivedDualToLeftDual M N) ∧
          derivedDualToLeftDual M N ▷ M ≫ ε_ M N = derivedDualEvaluationMonoidal M)

AlgebraicGeometry.RingedSite.isIso_derivedDualToLeftDual, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/LeftDualIsTheDerivedDual.lean, line 897. The attribute's comment: “the left dual is the object constructed in Example 0FPU, namely the derived dual RSheafHom(M, O) of Tag 08JD, and the identification is the morphism matched with the evaluation of Example 0FPU by the pairing; see AlgebraicGeometry.RingedSite.whiskerRight_derivedDualToLeftDual for the compatibility of the two evaluations. The monoidal structure on D(O) is the one of Tag 0FPT, Stacks.SheafOfModules.DerivedMonoidal.derivedMonoidal, and a left dual is Mathlib's CategoryTheory.ExactPairing, which is Definition 0FFP”.

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

theorem isIso_derivedDualToLeftDual : IsIso (derivedDualToLeftDual M N)

Tag 0A0A, a lemma

Tag 0A0A in the Stacks Project.

AlgebraicGeometry.RingedSite.isDerivedLimit_tensorDerivedDual_of_isHomotopyColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedHomOfAHomotopyColimit.lean, line 272. The attribute's comment: “the stated identity RSheafHom(K, E) = R lim (E ⊗^L_O Kₙ^∨) for K = hocolim Kₙ, with two inputs of the source's proof assumed rather than proved: hcomp, that the canonical map RSheafHom(⊕ Kₙ, E) ⟶ ∏ RSheafHom(Kₙ, E) is an isomorphism, which is the last step of the proof; and hdual, clause 3 of Stacks 08JJ, that the canonical map of Stacks 08JD E ⊗^L_O Kₙ^∨ ⟶ RSheafHom(Kₙ, E) is an isomorphism, which no declaration of this library asserts. The perfectness of the Kₙ is used in the source only to invoke that clause, so it is not assumed here, and the existence of the direct sum ⊕ Kₙ and of the two products is not assumed either, being supplied by the instances of Stacks 07D9; everything else of the tag is proved, in particular the whole comparison of triangles.”.

Stacks 0A0A. Let (Kₙ) be a system of objects of D(O) and let K = hocolim Kₙ. For every object E of D(O),

RSheafHom(K, E) = R lim (E ⊗^L_O Kₙ^∨),

granted the two inputs the source's proof uses and the library does not have: that the canonical map RSheafHom(⊕ Kₙ, E) ⟶ ∏ RSheafHom(Kₙ, E) is an isomorphism, and that the canonical map E ⊗^L_O Kₙ^∨ ⟶ RSheafHom(Kₙ, E) of Stacks 08JD is an isomorphism for every n, which is clause 3 of Stacks 08JJ and is where the perfectness of the Kₙ is used in the source.

Given the second hypothesis the tensor-dual system is isomorphic to the system n ↦ RSheafHom(Kₙ, E), so the assertion is AlgebraicGeometry.RingedSite.isDerivedLimit_derivedSheafHom_of_isHomotopyColimit transported along that isomorphism.

theorem isDerivedLimit_tensorDerivedDual_of_isHomotopyColimit
    (F : ℕ ⥤ DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (E : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (hcomp : IsIso (Pi.lift (fun n : ℕ ↦
        ((derivedSheafHomBifunctor X).flip.obj E).map (Sigma.ι F.obj n).op) :
      ((derivedSheafHomBifunctor X).flip.obj E).obj (op (∐ F.obj)) ⟶
        ∏ᶜ fun n : ℕ ↦ (derivedSheafHomSystem X F E).obj (op n)))
    (hdual : ∀ n : ℕ, IsIso (derivedTensorDualToSheafHom X T (F.obj n) E))
    {K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))}
    (hK : IsHomotopyColimit F K) :
    IsDerivedLimit (tensorDerivedDualSystem X T F E)
      (((derivedSheafHomBifunctor X).flip.obj E).obj (op K))

AlgebraicGeometry.RingedSite.derivedHom_isDerivedLimit_tensorDual, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/DerivedDualSystemLimit.lean, line 152. The attribute's comment: “the identity R𝑆heafHom(K, E) = R lim (E ⊗^L_O Kₙ^∨) for a system of perfect objects Kₙ with derived colimit K, at the hypotheses of the source: the perfectness of each Kₙ and K = hocolim Kₙ. The direct-sum comparison and the identification of Stacks 08JJ that the source's proof uses are both proved in the library, so this needs nothing beyond those two hypotheses: the ringed site carries no hypothesis, the sheafification and additivity instances the statement's constructions need being synthesized rather than assumed, and the existence of ⊕ Kₙ and of the products coming from the instances of Stacks 07D9”.

Stacks 0A0A: derived internal Hom out of a homotopy colimit of perfect objects. Let (𝒞, 𝒪) be a ringed site, let (Kₙ) be a system of perfect objects of D(𝒪), let K = hocolim Kₙ and let E be an object of D(𝒪). Then

R𝑆heafHom_𝒪(K, E) = R lim (E ⊗^𝐋_𝒪 Kₙ^∨).

Perfectness of the terms turns the system of tensor products with the duals into the system n ↦ R𝑆heafHom_𝒪(Kₙ, E), by Stacks 08JJ and its contravariant naturality; the latter system has R𝑆heafHom_𝒪(K, E) as its derived limit for every system with derived colimit K.

theorem derivedHom_isDerivedLimit_tensorDual
    (F : ℕ ⥤ DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (K E : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (hF : ∀ n : ℕ, X.IsPerfect (F.obj n))
    (hK : IsHomotopyColimit F K) :
    IsDerivedLimit
        (tensorDerivedDualSystem X (Stacks.SheafOfModules.canonicalDerivedTensorProduct X) F E)
      (((derivedSheafHomBifunctor X).obj (op K)).obj E)

AlgebraicGeometry.RingedSite.isDerivedLimit_tensorDerivedDual_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/DualTensorDerivedLimit.lean, line 122. The attribute's comment: “the stated identity RSheafHom(K, E) = R lim (E ⊗^L_O Kₙ^∨) for K = hocolim Kₙ with the Kₙ perfect, for the canonical derived tensor product, with both inputs of the source's proof proved rather than assumed”.

Stacks 0A0A for a system of perfect objects. Let (Kₙ) be a system of perfect objects of D(𝒪) whose direct sum exists and let K = hocolim Kₙ. For every object E of D(𝒪),

R𝑆heafHom_𝒪(K, E) = R lim (E ⊗^𝐋_𝒪 Kₙ^∨),

the derived tensor product being the canonical one of [Stacks, Tag 06YU].

Both inputs of the source's proof are discharged: the direct-sum comparison R𝑆heafHom_𝒪(⊕ Kₙ, E) ⟶ ∏ R𝑆heafHom_𝒪(Kₙ, E) by AlgebraicGeometry.RingedSite.isIso_derivedSheafHomSigmaComparison, and clause 3 of [Stacks, Tag 08JJ] by AlgebraicGeometry.RingedSite.tensorDerivedDualSystemIsoOfPerfect, which is where perfectness is used — exactly as in the source.

theorem isDerivedLimit_tensorDerivedDual_of_isPerfect
    (F : ℕ ⥤ DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    [HasCoproduct F.obj]
    (E : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    [HasProduct fun n : ℕ ↦ (derivedSheafHomSystem X F E).obj (op n)]
    [HasProduct fun n : ℕ ↦ (tensorDerivedDualSystem X
      (Stacks.SheafOfModules.canonicalDerivedTensorProduct.{u} X) F E).obj (op n)]
    (hF : ∀ n : ℕ, X.IsPerfect (F.obj n))
    {K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))}
    (hK : IsHomotopyColimit F K) :
    IsDerivedLimit (tensorDerivedDualSystem X
        (Stacks.SheafOfModules.canonicalDerivedTensorProduct.{u} X) F E)
      (((derivedSheafHomBifunctor X).flip.obj E).obj (op K))

Sources

• Section 21.48, Tag 0FPP
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Cohomology.MonoidalComplexesOfModules.symmetricMonoidalComplexes · Stacks.SheafOfModules.Strict.dualComplexOfLocallyStrictlyPerfect · Stacks.SheafOfModules.Strict.dualComplex · Stacks.SheafOfModules.Strict.exactPairingDualComplex · Stacks.SheafOfModules.Strict.exactPairingDualComplexOfLocallyStrictlyPerfect · Stacks.SheafOfModules.termwiseExactPairingDualSheaf · Stacks.SheafOfModules.Strict.isLocallyStrictlyPerfect_and_isoDualComplex_of_exactPairing · Stacks.SheafOfModules.isIso_tensorDualToSheafHom_of_localSummand

Section21.49 Invertible objects in the derived category#

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

Tag 0FPX, a lemma

Tag 0FPX in the Stacks Project.

AlgebraicGeometry.RingedSite.finiteFreeSummandEquivalenceFiniteProjective, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/StrictlyPerfect/SummandsOfFiniteFreeModules.lean, line 585. The attribute's comment: “the equivalence”.

On a ringed site (C, O) with R = Γ(C, O), the category of O-modules which are summands of finite free modules is equivalent to the category of finite projective R-modules.

def finiteFreeSummandEquivalenceFiniteProjective :
    ObjectProperty.FullSubcategory X.IsDirectSummandOfFiniteFree ≌
      ObjectProperty.FullSubcategory
        (fun M : ModuleCat.{max u w}
            (Stacks.Cohomology.SiteModules.GlobalSectionRing
              (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) =>
          Module.Finite
              (Stacks.Cohomology.SiteModules.GlobalSectionRing
                (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) M ∧
            Module.Projective
              (Stacks.Cohomology.SiteModules.GlobalSectionRing
                (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) M)

AlgebraicGeometry.RingedSite.finiteFreeSummandEquivalenceFiniteProjective_iso_globalSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/StrictlyPerfect/SummandsOfFiniteFreeModules.lean, line 699. The attribute's comment: “identification with global sections”.

The equivalence finiteFreeSummandEquivalenceFiniteProjective is given by taking global sections.

def finiteFreeSummandEquivalenceFiniteProjective_iso_globalSections :
    X.finiteFreeSummandEquivalenceFiniteProjective.functor ⋙ ObjectProperty.ι _ ≅
      ObjectProperty.ι _ ⋙
        Stacks.Cohomology.SiteModules.globalSectionsFunctor
          (Stacks.SheafOfModules.Tensor.ringSheaf X.O)

Tag 0FPY, a lemma

Tag 0FPY in the Stacks Project.

AlgebraicGeometry.RingedSite.InvertibleDerived.isPerfect_of_hasInvertibleModuleDecomposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/InvertibleObjects.lean, line 459. The attribute's comment: “clause (2) implies that M is a perfect object of D(O)”.

Stacks 0FPY, the perfectness conclusion. Let (C, O) be a ringed site and let M be an object of D(O). If there is a locally finite direct product decomposition O = ∏_{n ∈ ℤ} O_n of the structure sheaf and for each n an invertible O_n-module ℋ^n with M = ⨁ ℋ^n[-n] in D(O), then M is a perfect object of D(O).

On a covering of every object only finitely many factors survive, each ℋ^n is there a direct summand of a finite free O_n-module and O_n is a direct summand of O, so the complex with ℋ^n in degree n and zero differentials — which represents ⨁ ℋ^n[-n] — is locally strictly perfect.

theorem isPerfect_of_hasInvertibleModuleDecomposition (M : DerivedModules X.O)
    (hM : HasInvertibleModuleDecomposition X M) : X.IsPerfect M

AlgebraicGeometry.RingedSite.InvertibleDerived.IsInvertibleObject, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/InvertibleObjectsClauseThree.lean, line 114. The attribute's comment: “clause (1) as a condition on M: that M is invertible in D(O) in the sense of Stacks 0FFN, for the symmetric monoidal structure of Stacks 0FPT. This is the clause, not an implication between clauses”.

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

def IsInvertibleObject (M : DerivedModules X.O) : Prop

AlgebraicGeometry.RingedSite.InvertibleDerived.HasLocalInvertibleDegree, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/InvertibleObjectsClauseThree.lean, line 172. The attribute's comment: “clause (3) as a condition on M: that every object U of the site has a covering {U_i → U} and for each i an integer n_i with M|_{U_i} isomorphic in D(O_{U_i}) to an invertible O_{U_i}-module placed in degree n_i. This is the clause, not an implication between clauses”.

Clause (3) of Stacks 0FPY. Every object U of the site has a covering {U_i → U} and for each i an integer n_i such that M|_{U_i} is represented by an invertible O_{U_i}-module placed in degree n_i: there are an invertible O_{U_i}-module L and an isomorphism M|_{U_i} ≅ L[-n_i] in D(O_{U_i}).

M|_{U_i} is the image of M under the functor D(O) ⥤ D(O_{U_i}) induced by the exact restriction functor Mod(O) ⥤ Mod(O_{U_i}), and L[-n_i] is L placed in degree n_i. The derived category D(O_{U_i}) is read in its standard model HasDerivedCategory.standard; any two models are equivalent compatibly with their localization functors, so the condition does not depend on that reading.

def HasLocalInvertibleDegree (M : DerivedModules X.O) : Prop

AlgebraicGeometry.RingedSite.InvertibleDerived.isInvertibleObject_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Perfect/InvertibleObjectsTFAE.lean, line 165. The attribute's comment: “All of the tag: (1) ⟺ (2) on every ringed site; (1) implies that M is perfect; and (1) ⟺ (2) ⟺ (3) on a locally ringed site. The ringed site is RingedSite.{u, u, u} -- objects, morphisms and sections of O in one universe u. This is the library's one-universe convention for D(O) as a symmetric monoidal category: the derived tensor product of Stacks 0FPT on a ringed site (Stacks.SheafOfModules.DerivedMonoidal.derivedMonoidal) is built from the K-flat resolutions of Stacks 06YS, which the library constructs at that universe pattern only, so clause (1) has no meaning off it. The four HasSheafify / WEqualsLocallyBijective instance arguments are the library's standard ones, and Mathlib synthesizes all four for every RingedSite.{u, u, u}”.

Stacks 0FPY. Let (C, O) be a ringed site and let M be an object of D(O). The following are equivalent:

1. M is invertible in D(O) (IsInvertibleObject: Stacks 0FFN for the derived tensor product of Stacks 0FPT);
2. there is a locally finite direct product decomposition O = ∏_{n ∈ ℤ} O_n and for each n an invertible O_n-module ℋ^n (Stacks 0409) with M = ⨁ ℋ^n[-n] in D(O) (HasInvertibleModuleDecomposition).

If they hold, M is a perfect object of D(O) (AlgebraicGeometry.RingedSite.IsPerfect, Stacks 08G5). If (C, O) is a locally ringed site (Stacks 04EU) they are also equivalent to

1. for every object U of C there are a covering {U_i → U} and integers n_i such that M|_{U_i} is isomorphic in D(O_{U_i}) to an invertible O_{U_i}-module placed in degree n_i (HasLocalInvertibleDegree).

D(O) is any model of the derived category. The ringed site has its objects, its morphisms and its rings of sections in one universe; see the note of the stacks attribute.

theorem isInvertibleObject_tfae (M : DerivedCategory (Mod X.O)) :
    [IsInvertibleObject X M, HasInvertibleModuleDecomposition X M].TFAE ∧
      (IsInvertibleObject X M → X.IsPerfect M) ∧
      (IsLocallyRinged X →
        [IsInvertibleObject X M, HasInvertibleModuleDecomposition X M,
          HasLocalInvertibleDegree X M].TFAE)

Sources

• Section 21.49, Tag 0FPW
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.RingedSite.finiteFreeSummandEquivalenceFiniteProjective · AlgebraicGeometry.RingedSite.finiteFreeSummandEquivalenceFiniteProjective_iso_globalSections · AlgebraicGeometry.RingedSite.InvertibleDerived.isPerfect_of_hasInvertibleModuleDecomposition · AlgebraicGeometry.RingedSite.InvertibleDerived.IsInvertibleObject · AlgebraicGeometry.RingedSite.InvertibleDerived.HasLocalInvertibleDegree · AlgebraicGeometry.RingedSite.InvertibleDerived.isInvertibleObject_tfae

Section21.50 Projection formula#

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

Tag 0943, the section

Tag 0943 in the Stacks Project.

Stacks.Cohomology.ProjectionFormulaSection.projectionFormula, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/ProjectionFormulaSection.lean, line 144. The attribute's comment: “the canonical map of Section 21.50, natural in the two complexes together”.

The canonical map of Section 21.50 of [Stacks, Tag 0943], as a morphism of bifunctors on D(𝒪_𝒞) × D(𝒪_𝒟):

Rf_*E ⊗^𝐋_{𝒪_𝒟} K ⟶ Rf_*(E ⊗^𝐋_{𝒪_𝒞} Lf^*K),

natural in E and K together. Its value at a pair is the map of [Stacks, Tag 0B56], the adjoint for Lf^* ⊣ Rf_* of the comparison Lf^*(Rf_*E ⊗^𝐋 K) ≅ Lf^*Rf_*E ⊗^𝐋 Lf^*K of [Stacks, Tag 07A4] followed by the counit Lf^*Rf_*E ⟶ E in the first factor. There is no hypothesis on f, E or K: the section stresses that the map exists for every morphism of ringed topoi, and the joint naturality is the naturality of the adjoint-transpose construction the map instantiates.

def projectionFormula : pushforwardTensor f ⟶ tensorPullbackPushforward f

Stacks.Cohomology.ProjectionFormulaSection.isIso_projectionFormulaNatTransSource, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/ProjectionFormulaSection.lean, line 205. The attribute's comment: “the lemma of Section 21.50: at a perfect complex the canonical map is invertible, here as an isomorphism of the two functors of the complex on the source”.

The lemma of Section 21.50 of [Stacks, Tag 0943], as an isomorphism of functors. Let f : (Sh(𝒞), 𝒪_𝒞) ⟶ (Sh(𝒟), 𝒪_𝒟) be a morphism of ringed topoi and let K ∈ D(𝒪_𝒟) be perfect. Then the canonical map of the section is invertible as a natural transformation of functors of the complex on the source:

Rf_*(-) ⊗^𝐋_{𝒪_𝒟} K ≅ Rf_*(- ⊗^𝐋_{𝒪_𝒞} Lf^*K) on D(𝒪_𝒞) ⥤ D(𝒪_𝒟).

A natural transformation is invertible as soon as each of its components is, and each component is [Stacks, Tag 0944].

theorem isIso_projectionFormulaNatTransSource
    (K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)))
    (hK : RingedSite.IsPerfect Y.toRingedSite K) :
    IsIso (projectionFormulaNatTransSource f K)

Tag 0B56, an equation

Tag 0B56 in the Stacks Project.

Stacks.Cohomology.ProjectionFormulaOnRingedTopoi.projectionFormulaMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/ProjectionFormula.lean, line 259. The attribute's comment: “the map”.

Equation 21.50.0.1 of [Stacks, Tag 0B56]. For a morphism of ringed topoi f : (Sh(C), O_C) ⟶ (Sh(D), O_D), E ∈ D(O_C) and K ∈ D(O_D), the canonical map

Rf_*E ⊗^L_{O_D} K ⟶ Rf_*(E ⊗^L_{O_C} Lf^*K),

with no further hypothesis. It is the map adjoint, for the adjunction Lf^* ⊣ Rf_* of [Stacks, Tag 07A6], to the bifunctorial identification Lf^*(Rf_*E ⊗^L K) ≅ Lf^*Rf_*E ⊗^L Lf^*K of [Stacks, Tag 07A4] followed by the counit Lf^*Rf_*E ⟶ E in the first factor.

def projectionFormulaMap (hmos : f.u.IsMorphismOfSites Y.J X.J)
    (E : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))) :
    ((derivedTensorProductFunctor Y.O).obj ((derivedPushforward f).obj E)).obj K ⟶
      (derivedPushforward f).obj
        (((derivedTensorProductFunctor X.O).obj E).obj ((derivedPullback f).obj K))

Stacks.Cohomology.ProjectionFormulaOnRingedTopoi.projectionFormulaMap_naturality_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/ProjectionFormula.lean, line 286. The attribute's comment: “naturality in the source complex”.

Naturality of Equation 21.50.0.1 in the complex on the source, E ∈ D(O_C).

theorem projectionFormulaMap_naturality_source
    {E E' : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))} (φ : E ⟶ E')
    (K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))) :
    ((derivedTensorProductFunctor Y.O).map ((derivedPushforward f).map φ)).app K ≫
        projectionFormulaMap f hmos E' K =
      projectionFormulaMap f hmos E K ≫
        (derivedPushforward f).map
          (((derivedTensorProductFunctor X.O).map φ).app ((derivedPullback f).obj K))

Stacks.Cohomology.ProjectionFormulaOnRingedTopoi.projectionFormulaMap_naturality_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/ProjectionFormula.lean, line 298. The attribute's comment: “naturality in the target complex”.

Naturality of Equation 21.50.0.1 in the complex on the target, K ∈ D(O_D).

theorem projectionFormulaMap_naturality_target
    (E : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    {K K' : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))} (k : K ⟶ K') :
    ((derivedTensorProductFunctor Y.O).obj ((derivedPushforward f).obj E)).map k ≫
        projectionFormulaMap f hmos E K' =
      projectionFormulaMap f hmos E K ≫
        (derivedPushforward f).map
          (((derivedTensorProductFunctor X.O).obj E).map ((derivedPullback f).map k))

Stacks.Cohomology.ProjectionFormulaPerfectOnRingedTopoi.projectionFormulaTransformation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/ProjectionFormulaStrictlyPerfect.lean, line 155. The attribute's comment: “the map as a natural transformation in the target complex”.

Equation 21.50.0.1 of [Stacks, Tag 0B56] as a natural transformation of functors of the complex on the base. Its component at K is Stacks.Cohomology.ProjectionFormulaOnRingedTopoi.projectionFormulaMap f hmos E K, and its naturality is projectionFormulaMap_naturality_target.

def projectionFormulaTransformation :
    projectionFormulaSource f E ⟶ projectionFormulaTarget f E

Tag 0944, a lemma

Tag 0944 in the Stacks Project.

Stacks.Cohomology.ProjectionFormulaOfToposHom.isIso_projectionFormulaMap_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/ProjectionFormulaPerfectOfToposHom.lean, line 122.

[Stacks, Tag 0944], the projection formula for a perfect complex. Let f : (Sh(𝒞), 𝒪_𝒞) ⟶ (Sh(𝒟), 𝒪_𝒟) be a morphism of ringed topoi, E ∈ D(𝒪_𝒞) and K ∈ D(𝒪_𝒟). If K is perfect, then the canonical map of [Stacks, Tag 0B56] Rf_*E ⊗^𝐋_{𝒪_𝒟} K ⟶ Rf_*(E ⊗^𝐋_{𝒪_𝒞} Lf^*K) is an isomorphism.

theorem isIso_projectionFormulaMap_of_isPerfect {X Y : RingedTopos.{u, u, u}}
    (f : RingedToposHom X Y)
    (E : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)))
    (hK : RingedSite.IsPerfect Y.toRingedSite K) :
    IsIso (projectionFormulaMap f E K)

Tag 0E48, a remark

Tag 0E48 in the Stacks Project.

Stacks.Cohomology.ProjectionFormulaOfToposHom.projectionFormulaMap_baseChange_square, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/ProjectionFormulaBaseChange.lean, line 108.

[Stacks, Tag 0E48]. For a commutative square of morphisms of ringed topoi

             g'
  (Sh(C'), 𝒪_{C'}) --→ (Sh(C), 𝒪_C)
      |  f'                |  f
      v                    v
  (Sh(D'), 𝒪_{D'}) --→ (Sh(D), 𝒪_D)
             g

and E in D(𝒪_C), K in D(𝒪_D), the map p of Equation 21.50.0.1 is compatible with the base change map b of [Stacks, Tag 07A7]: going down the left (t, the comparison of [Stacks, Tag 07A4] for g, then b ⊗ 1, then p for f') equals going down the right (Lg^* of p for f, then b, then R(f')_* of t for g' followed by 1 ⊗ c, where c : L(g')^*Lf^*K ⟶ L(f')^*Lg^*K identifies the two iterated pullbacks around the square), as maps Lg^*(Rf_*E ⊗^L K) ⟶ R(f')_*(L(g')^*E ⊗^L L(f')^*Lg^*K) in D(𝒪_{D'}).

theorem projectionFormulaMap_baseChange_square (h : g.comp f' = f.comp g')
    (E : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))) :
    (derivedPullbackTensorIso g).hom.app ((derivedPushforward f).obj E, K) ≫
        (Functor.uncurry.obj (derivedTensorProductFunctor Y'.O)).map
            (derivedBaseChangeMap f g' f' g h E ×ₘ 𝟙 ((derivedPullback g).obj K)) ≫
          adjunctionTensorMap (derivedAdjunction f')
            (Functor.uncurry.obj (derivedTensorProductFunctor Y'.O))
            (Functor.uncurry.obj (derivedTensorProductFunctor X'.O))
            (derivedPullbackTensorIso f').hom
            ((derivedPullback g').obj E) ((derivedPullback g).obj K) =
      (derivedPullback g).map
          (adjunctionTensorMap (derivedAdjunction f)
            (Functor.uncurry.obj (derivedTensorProductFunctor Y.O))
            (Functor.uncurry.obj (derivedTensorProductFunctor X.O))
            (derivedPullbackTensorIso f).hom E K) ≫
        derivedBaseChangeMap f g' f' g h
            (((derivedTensorProductFunctor X.O).obj E).obj ((derivedPullback f).obj K)) ≫
          (derivedPushforward f').map
            ((derivedPullbackTensorIso g').hom.app (E, (derivedPullback f).obj K) ≫
              (Functor.uncurry.obj (derivedTensorProductFunctor X'.O)).map
                (𝟙 ((derivedPullback g').obj E) ×ₘ
                  (Stacks.AffineProjectionFormula.squareCompositeIso
                    (derivedPullbackCompIsoLeft f' g)
                    (derivedPullbackCompIsoRight f g' f' g h)).inv.app K))

Sources

• Section 21.50, Tag 0943
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Cohomology.ProjectionFormulaSection.projectionFormula · Stacks.Cohomology.ProjectionFormulaSection.isIso_projectionFormulaNatTransSource · Stacks.Cohomology.ProjectionFormulaOnRingedTopoi.projectionFormulaMap · Stacks.Cohomology.ProjectionFormulaOnRingedTopoi.projectionFormulaMap_naturality_source · Stacks.Cohomology.ProjectionFormulaOnRingedTopoi.projectionFormulaMap_naturality_target · Stacks.Cohomology.ProjectionFormulaPerfectOnRingedTopoi.projectionFormulaTransformation · Stacks.Cohomology.ProjectionFormulaOfToposHom.isIso_projectionFormulaMap_of_isPerfect · Stacks.Cohomology.ProjectionFormulaOfToposHom.projectionFormulaMap_baseChange_square

Section21.51 Weakly contractible objects#

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

Tag 0946, a lemma

Tag 0946 in the Stacks Project.

Stacks.WeaklyContractible.exact_sheafSections_of_isWeaklyContractible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/WeaklyContractible/CohomologyOverAWeaklyContractibleObject.lean, line 108. The attribute's comment: “part (1)”.

Evaluation of abelian sheaves at a weakly contractible object is exact, with weak contractibility tested in the value universe w.

theorem exact_sheafSections_of_isWeaklyContractible
    [HasSheafify J AddCommGrpCat.{w}]
    (U : C)
    (hU : ∀ (F G : Sheaf J (Type w)) (φ : F ⟶ G),
      Sheaf.IsLocallySurjective φ → Function.Surjective (φ.hom.app (op U))) :
    exactFunctor (Sheaf J AddCommGrpCat.{w}) AddCommGrpCat.{w}
      ((sheafSections J AddCommGrpCat.{w}).obj (op U))

Stacks.WeaklyContractible.subsingleton_cohomology_of_isWeaklyContractible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/WeaklyContractible/CohomologyOverAWeaklyContractibleObject.lean, line 139. The attribute's comment: “part (2)”.

The positive-degree cohomology of an abelian sheaf over a weakly contractible object vanishes.

theorem subsingleton_cohomology_of_isWeaklyContractible
    [HasSheafify J AddCommGrpCat.{v}]
    [HasExt.{w'} (Sheaf J AddCommGrpCat.{v})]
    (U : C) (hU : J.IsWeaklyContractible U)
    (F : Sheaf J AddCommGrpCat.{v}) (p : ℕ) (hp : 1 ≤ p) :
    Subsingleton (Sheaf.H'.{w', v} F p U)

Stacks.WeaklyContractible.nonempty_sections_of_isWeaklyContractible_of_isTorsor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/WeaklyContractible/CohomologyOverAWeaklyContractibleObject.lean, line 153. The attribute's comment: “part (3)”.

Every torsor has a section over a weakly contractible object.

theorem nonempty_sections_of_isWeaklyContractible_of_isTorsor
    (U : C) (hU : J.IsWeaklyContractible U)
    (G : SheafOfGroups.{v, v, u} (C := C) J)
    (F : PseudoTorsor (C := C) G) (hF : F.IsTorsor) :
    Nonempty (F.presheaf.obj (op U))

Tag 0947, a proposition

Tag 0947 in the Stacks Project.

Stacks.SheafOfModules.WeaklyContractible.hasExactLimitsOfShape_discrete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/WeaklyContractibleProducts.lean, line 214. The attribute's comment: “(4)”.

Stacks 0947(4). On a site every object of which has a covering by weakly contractible objects, products of sheaves of modules are exact -- over an arbitrary index type ι, in an arbitrary universe, subject only to the t-smallness that makes the product exist at all.

theorem hasExactLimitsOfShape_discrete (ι : Type u₀) [Small.{t} ι] (B : ObjectProperty C)
    (hB : J.HasEnoughObjects B)
    (hwc : ∀ ⦃U : C⦄, B U → ∀ (F G : Sheaf J (Type t)) (φ : F ⟶ G),
      Sheaf.IsLocallySurjective φ → Function.Surjective (φ.hom.app (op U))) :
    HasExactLimitsOfShape (Discrete ι) (SheafOfModules.{t} R)

Stacks.WeaklyContractible.isZero_homology_of_isDerivedLimit_single, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/WeaklyContractible/DerivedLimitOfModules.lean, line 99. The attribute's comment: “(6), vanishing of the higher derived limits”.

Stacks 0947(6). On a ringed site with a covering collection of weakly contractible objects, the derived limit of a countable inverse system (Fₙ) of sheaves of modules has no cohomology outside degrees 0 and 1: Rᵖ lim Fₙ = 0 for every p ≠ 0, 1, in particular for every p > 1.

theorem isZero_homology_of_isDerivedLimit_single
    (S : WeaklyContractibleObjectsSituation.{w, v, u, t} C J)
    [HasDerivedCategory (SheafOfModules.{t} S.O)]
    (G : ℕᵒᵖ ⥤ SheafOfModules.{t} S.O)
    (L : DerivedCategory (SheafOfModules.{t} S.O))
    (hL : IsDerivedLimit (G ⋙ DerivedCategory.singleFunctor (SheafOfModules.{t} S.O) 0) L)
    (p : ℤ) (hp₀ : p ≠ 0) (hp₁ : p ≠ 1) :
    IsZero ((DerivedCategory.homologyFunctor (SheafOfModules.{t} S.O) p).obj L)

Stacks.WeaklyContractible.nonempty_cokernel_iso_homology_one_of_isDerivedLimit_single, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/WeaklyContractible/DerivedLimitOfModules.lean, line 119. The attribute's comment: “(6), R¹lim as a cokernel”.

Stacks 0947(6). On a ringed site with a covering collection of weakly contractible objects, the first derived limit of a countable inverse system (Fₙ) of sheaves of modules is the cokernel of the difference map (xₙ) ↦ (xₙ - fₙ₊₁(xₙ₊₁)) on the product ∏ₙ Fₙ.

theorem nonempty_cokernel_iso_homology_one_of_isDerivedLimit_single
    (S : WeaklyContractibleObjectsSituation.{w, v, u, t} C J)
    [HasDerivedCategory (SheafOfModules.{t} S.O)]
    (G : ℕᵒᵖ ⥤ SheafOfModules.{t} S.O)
    (L : DerivedCategory (SheafOfModules.{t} S.O))
    (hL : IsDerivedLimit (G ⋙ DerivedCategory.singleFunctor (SheafOfModules.{t} S.O) 0) L) :
    Nonempty (cokernel (Pi.lift fun n : ℕ ↦ Pi.π (fun n : ℕ ↦ G.obj ⟨n⟩) n -
        Pi.π (fun n : ℕ ↦ G.obj ⟨n⟩) (n + 1) ≫ G.map (homOfLE (Nat.le_succ n)).op) ≅
      (DerivedCategory.homologyFunctor (SheafOfModules.{t} S.O) 1).obj L)

Stacks.WeaklyContractible.isLimit_productFanInDerivedCategory_of_weaklyContractibleObjectsSituation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/WeaklyContractible/DerivedProducts.lean, line 68. The attribute's comment: “derived_products_termwise”.

Stacks 0947(5). On a ringed site with a covering collection of weakly contractible objects, products in the derived category of sheaves of modules are computed by termwise products of representing complexes: for every family K of cochain complexes of sheaves of modules indexed by an arbitrary type ι, the fan whose apex is the image of the termwise product complex ∏ᶜ K and whose legs are the images of the projections Pi.π K i is a limit fan.

theorem isLimit_productFanInDerivedCategory_of_weaklyContractibleObjectsSituation
    (S : WeaklyContractibleObjectsSituation.{w, v, u, t} C J)
    [HasDerivedCategory (SheafOfModules.{t} S.O)] (ι : Type u₀) [Small.{t} ι]
    (K : ι → CochainComplex (SheafOfModules.{t} S.O) ℤ) :
    Nonempty (IsLimit (Stacks.DerivedProducts.productFanInDerivedCategory K))

Stacks.WeaklyContractible.exact_iff_exact_sections_of_weaklyContractibleObjectsSituation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/WeaklyContractible/ExactSections.lean, line 98. The attribute's comment: “exact_iff_sections”.

In a site covered by weakly contractible objects, a complex of sheaves of modules is exact if and only if it is exact on sections over every chosen weakly contractible object.

theorem exact_iff_exact_sections_of_weaklyContractibleObjectsSituation
    [HasSheafify J AddCommGrpCat.{t}]
    [J.WEqualsLocallyBijective AddCommGrpCat.{t}]
    (h : WeaklyContractibleObjectsSituation.{w, v, u, t} C J)
    (S : ShortComplex (SheafOfModules.{t} h.O)) :
    S.Exact ↔ ∀ ⦃U : C⦄, h.B U →
      Function.Exact (S.f.val.app (op U)) (S.g.val.app (op U))

Stacks.WeaklyContractible.exists_milnor_shortExact_of_weaklyContractibleObjectsSituation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/WeaklyContractible/MilnorSequence.lean, line 57. The attribute's comment: “(7)”.

Milnor sequences. On a ringed site with a covering collection of weakly contractible objects, an inverse system K in the derived category of sheaves of modules and a derived limit L of it fit, in every degree r, into a short exact sequence

0 ⟶ R¹lim Hʳ⁻¹(Kₙ) ⟶ Hʳ(L) ⟶ lim Hʳ(Kₙ) ⟶ 0,

where R¹lim of an inverse system of sheaves of modules is the cokernel of the difference map 1 - shift on the product of its terms. The first map is induced by the connecting morphism of the triangle L ⟶ ∏ Kₙ ⟶ ∏ Kₙ ⟶ L[1] through the comparison Hʳ⁻¹(∏ Kₙ) ≅ ∏ Hʳ⁻¹(Kₙ), and the second is the map whose components are Hʳ of the composites L ⟶ ∏ Kₙ ⟶ Kₙ.

theorem exists_milnor_shortExact_of_weaklyContractibleObjectsSituation
    (S : WeaklyContractibleObjectsSituation.{w, v, u, t} C J)
    [HasDerivedCategory (SheafOfModules.{t} S.O)]
    (F : ℕᵒᵖ ⥤ DerivedCategory (SheafOfModules.{t} S.O))
    (L : DerivedCategory (SheafOfModules.{t} S.O)) (hL : IsDerivedLimit F L) :
    let X : ℕ → DerivedCategory (SheafOfModules.{t} S.O) := fun n ↦ F.obj (Opposite.op n)
    let d : (∏ᶜ X) ⟶ ∏ᶜ X := Pi.lift fun n : ℕ ↦
      Pi.π X n - Pi.π X (n + 1) ≫ F.map (homOfLE (Nat.le_succ n)).op
    ∃ (a : L ⟶ ∏ᶜ X) (b : (∏ᶜ X) ⟶ L⟦(1 : ℤ)⟧),
      let T := Triangle.mk a d b
      T ∈ distTriang (DerivedCategory (SheafOfModules.{t} S.O)) ∧
        ∀ r : ℤ,
          let H := DerivedCategory.homologyFunctor (SheafOfModules.{t} S.O) r
          let H₁ := DerivedCategory.homologyFunctor (SheafOfModules.{t} S.O) (r - 1)
          let homologySystem : ℕᵒᵖ ⥤ SheafOfModules.{t} S.O := F ⋙ H
          let shiftedHomologySystem : ℕᵒᵖ ⥤ SheafOfModules.{t} S.O := F ⋙ H₁
          let P : SheafOfModules.{t} S.O :=
            ∏ᶜ fun n : ℕ ↦ shiftedHomologySystem.obj (Opposite.op n)
          let δ : P ⟶ P := Pi.lift fun n : ℕ ↦
            Pi.π (fun n : ℕ ↦ shiftedHomologySystem.obj (Opposite.op n)) n -
              Pi.π (fun n : ℕ ↦ shiftedHomologySystem.obj (Opposite.op n)) (n + 1) ≫
                shiftedHomologySystem.map (homOfLE (Nat.le_succ n)).op
          ∃ (e : H₁.obj (∏ᶜ X) ≅ P)
            (i : cokernel δ ⟶ H.obj L) (q : H.obj L ⟶ limit homologySystem)
            (w : i ≫ q = 0),
            e.hom = piComparison H₁ X ∧
              cokernel.π δ ≫ i = e.inv ≫
                DerivedCategory.HomologySequence.δ T (r - 1) r ∧
              (∀ n : ℕ, q ≫ limit.π homologySystem (Opposite.op n) =
                H.map a ≫ H.map (Pi.π X n)) ∧
              (ShortComplex.mk i q w).ShortExact

Stacks.WeaklyContractible.epi_limit_π_zero_of_epi_map_succ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/WeaklyContractible/SurjectiveTower.lean, line 85. The attribute's comment: “(3)”.

Stacks 0947(3). On a ringed site with a covering collection of weakly contractible objects, let G be a countable inverse system of sheaves of modules whose transition maps Gₙ₊₁ ⟶ Gₙ are all epimorphisms. Then the projection lim G ⟶ G₀ from the inverse limit onto the bottom term of the tower is an epimorphism.

theorem epi_limit_π_zero_of_epi_map_succ
    (S : WeaklyContractibleObjectsSituation.{w, v, u, t} C J)
    (G : ℕᵒᵖ ⥤ SheafOfModules.{t} S.O)
    (hG : ∀ n : ℕ, Epi (G.map (homOfLE (Nat.le_succ n)).op)) :
    Epi (limit.π G ⟨0⟩)

Stacks.WeaklyContractible.exists_isDerivedLimit_truncGETower_of_weaklyContractibleObjectsSituation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/WeaklyContractible/TruncationDerivedLimit.lean, line 145. The attribute's comment: “(2)”.

Stacks 0947(2). On a ringed site with a covering collection of weakly contractible objects, every object E of the unbounded derived category of sheaves of modules is a derived limit of the tower n ↦ τ_{≥ -n} E of its canonical truncations from below: E = R lim τ_{≥ -n} E. The product of the tower exists because each of its stages is bounded below, and is part of the conclusion.

theorem exists_isDerivedLimit_truncGETower_of_weaklyContractibleObjectsSituation
    [HasSheafify J AddCommGrpCat.{max u v w t}]
    [J.WEqualsLocallyBijective AddCommGrpCat.{max u v w t}]
    (S : WeaklyContractibleObjectsSituation.{w, v, u, max u v w t} C J)
    (E : DerivedCategory (SheafOfModules.{max u v w t} S.O)) :
    ∃ _ : HasProduct fun n : ℕ ↦
        (Stacks.DerivedLimit.truncGETower (SheafOfModules.{max u v w t} S.O) E).obj ⟨n⟩,
      IsDerivedLimit (Stacks.DerivedLimit.truncGETower (SheafOfModules.{max u v w t} S.O) E)
        E

Sources

• Section 21.51, Tag 0945
• AxiomMath/Stacks at 5ed82d14

LeanStacks.WeaklyContractible.exact_sheafSections_of_isWeaklyContractible · Stacks.WeaklyContractible.subsingleton_cohomology_of_isWeaklyContractible · Stacks.WeaklyContractible.nonempty_sections_of_isWeaklyContractible_of_isTorsor · Stacks.SheafOfModules.WeaklyContractible.hasExactLimitsOfShape_discrete · Stacks.WeaklyContractible.isZero_homology_of_isDerivedLimit_single · Stacks.WeaklyContractible.nonempty_cokernel_iso_homology_one_of_isDerivedLimit_single · Stacks.WeaklyContractible.isLimit_productFanInDerivedCategory_of_weaklyContractibleObjectsSituation · Stacks.WeaklyContractible.exact_iff_exact_sections_of_weaklyContractibleObjectsSituation

Section21.52 Compact objects#

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

Tag 094B, a lemma

Tag 094B in the Stacks Project.

Stacks.Cohomology.CompactObjects.exists_retract_finiteComplex_of_isCompactObject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CompactObjects/FromAGeneratingSet.lean, line 650.

A compact derived object is a summand of a finite complex of finite sums of compact generators of the abelian category.

public theorem exists_retract_finiteComplex_of_isCompactObject
    {A : Type u} [Category.{v} A] [Abelian A]
    [IsGrothendieckAbelian.{w} A] [HasDerivedCategory.{z} A]
    (S : Set A)
    (hS : ∀ X : A, ∃ (I : Type w) (E : I → A),
      (∀ i, E i ∈ S) ∧ ∃ f : (∐ E) ⟶ X, Epi f)
    (hcompact : ∀ E ∈ S, IsCompactObject.{w} E)
    (K : DerivedCategory A) [IsCompactObject.{w} K] :
    ∃ (L : CochainComplex A ℤ) (a b : ℤ),
      L.IsStrictlyGE a ∧ L.IsStrictlyLE b ∧
      (∀ i : ℤ, ∃ (n : ℕ) (E : Fin n → A),
        (∀ j, E j ∈ S) ∧ Nonempty (L.X i ≅ ∐ E)) ∧
      Nonempty (Retract K (DerivedCategory.Q.obj L))

Tag 094C, a lemma

Tag 094C in the Stacks Project.

Stacks.Cohomology.exists_retract_finiteComplex_extensionByZero_of_isCompactObject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LowerShriekAndPerfection/CompactObjectsOnRingedSites.lean, line 207.

Stacks 094C. On a ringed site every object of which is covered by quasi-compact objects, a compact object of the derived category of sheaves of modules is a direct summand of a bounded complex whose terms are finite direct sums of the modules j_{U!} O_U for quasi-compact U.

public theorem exists_retract_finiteComplex_extensionByZero_of_isCompactObject
    (hqc : ∀ U : X.C, ∃ 𝒰 : PreZeroHypercover.{max u v} U,
      𝒰.sieve₀ ∈ X.J U ∧ ∀ i, X.J.IsQuasiCompactObject (𝒰.X i))
    (K : DerivedCategory
      (SheafOfModules.{max u v w m} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    [IsCompactObject.{max u v w m} K] :
    ∃ (L : CochainComplex
        (SheafOfModules.{max u v w m} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ)
      (a b : ℤ),
      L.IsStrictlyGE a ∧ L.IsStrictlyLE b ∧
      (∀ i : ℤ, ∃ (n : ℕ) (U : Fin n → X.C),
        (∀ j, X.J.IsQuasiCompactObject (U j)) ∧
        Nonempty (L.X i ≅ ∐ fun j : Fin n ↦
          extensionByZeroUnit.{v, u, w, m} X.J
            (Stacks.SheafOfModules.Tensor.ringSheaf X.O) (U j))) ∧
      Nonempty (Retract K (DerivedCategory.Q.obj L))

Tag 0G21, a lemma

Tag 0G21 in the Stacks Project.

Stacks.Cohomology.extensionByZero_unit_hom_coproduct_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LowerShriekAndPerfection/ExtensionByZeroRelativeCompactness.lean, line 676.

Extension by zero of the unit module on U is compact with respect to bounded-below direct sums, provided cohomology on U commutes with direct sums.

public theorem extensionByZero_unit_hom_coproduct_bijective
    (X : RingedSite.{u, v, r}) (U : X.C)
    (hsums :
      letI : EnoughInjectives (SheafOfModules.{max u v r m}
          (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) :=
        enoughInjectives_of_ringedSite.{u, v, r, m} X
      letI : (SheafOfModules.evaluation.{max u v r m} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)
          (op U)).Additive :=
        evaluation_additive_of_ringedSite.{u, v, r, m} X U
      ∀ (p : ℕ) (I : Type w),
      PreservesColimitsOfShape (Discrete I)
        ((SheafOfModules.evaluation.{max u v r m} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)
            (op U)).rightDerived p))
    (I : Type w) [DecidableEq I]
    (M : I → DerivedCategory (SheafOfModules.{max u v r m}
        (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) [HasCoproduct M]
    (hM : (DerivedCategory.TStructure.t
      (C := SheafOfModules.{max u v r m} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))).plus
          (∐ M)) :
    let K : DerivedCategory (SheafOfModules.{max u v r m}
        (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) :=
      ((DerivedCategory.singleFunctor
        (SheafOfModules.{max u v r m} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) 0).obj
        (extensionByZeroUnit.{v, u, r, m} X.J (Stacks.SheafOfModules.Tensor.ringSheaf X.O) U))
    Function.Bijective
      (DirectSum.toAddMonoid (β := fun i : I => K ⟶ M i) (γ := K ⟶ ∐ M)
        fun i => Preadditive.rightComp K (Limits.Sigma.ι M i))

Tag 0G22, a lemma

Tag 0G22 in the Stacks Project.

Stacks.Cohomology.extensionByZero_unit_hom_coproduct_bijective_of_hasIntersectionsIn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CompactnessFromCoverings/CompactnessFromFiniteCoverings.lean, line 370.

On a ringed site with a cofinal collection of finite coverings closed under finite intersections, extension by zero of the unit module over U is compact with respect to bounded-below coproducts.

public theorem extensionByZero_unit_hom_coproduct_bijective_of_hasIntersectionsIn
    (X : RingedSite.{u, u, u})
    (B : Set X.C) (Cov : ∀ U : X.C, Set (PreZeroHypercover.{c} U))
    (hCov : ∀ (U : X.C) (E : PreZeroHypercover.{c} U), Cov U E → E.sieve₀ ∈ X.J U)
    (hfinite : ∀ (U : X.C) (E : PreZeroHypercover.{c} U), Cov U E →
      HasIntersectionsIn B E)
    (hcofinal : ∀ (U : X.C), B U → ∀ S ∈ X.J U,
      ∃ E : PreZeroHypercover.{c} U, Cov U E ∧ E.sieve₀ ≤ S)
    (U : X.C) (hU : B U)
    (I : Type i) [DecidableEq I]
    (M : I → DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    [HasCoproduct M]
    (hM : (DerivedCategory.TStructure.t
      (C := SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))).plus (∐ M)) :
    let K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) :=
      ((DerivedCategory.singleFunctor
        (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) 0).obj
        (extensionByZeroUnit.{u, u, u, u} X.J (Stacks.SheafOfModules.Tensor.ringSheaf X.O) U))
    Function.Bijective
      (DirectSum.toAddMonoid (β := fun j : I => K ⟶ M j) (γ := K ⟶ ∐ M)
        fun j => Preadditive.rightComp K (Limits.Sigma.ι M j))

Tag 094D, a lemma

Tag 094D in the Stacks Project.

Stacks.Cohomology.CompactExtensionByZero.isCompactObject_singleFunctor_extensionByZeroUnit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CompactObjects/ExtensionByZeroIsCompact.lean, line 768.

Let (C, O) be a ringed site and U an object of C. If cohomology over U has finite cohomological dimension and H^p(U, -) commutes with direct sums for every p, then j_{U!} O_U, placed in degree zero, is a compact object of the unbounded derived category of O-modules. Compactness is tested against families indexed by types in Type w, the universe of the hypothesis on direct sums.

theorem isCompactObject_singleFunctor_extensionByZeroUnit
    (hcd : ∃ d : ℤ, ∀ (p : ℕ) (G : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)),
      d < (p : ℤ) →
      IsZero (((SheafOfModules.evaluation (Stacks.SheafOfModules.Tensor.ringSheaf X.O)
        (op U)).rightDerived p).obj G))
    (hsums : ∀ (p : ℕ) (I : Type w), PreservesColimitsOfShape (Discrete I)
      ((SheafOfModules.evaluation (Stacks.SheafOfModules.Tensor.ringSheaf X.O)
        (op U)).rightDerived p)) :
    IsCompactObject.{w}
      ((DerivedCategory.singleFunctor (SheafOfModules.{u}
        (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) 0).obj
        ((SheafOfModules.pullback.{u} (F := Over.forget U)
          (𝟙 ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U))).obj
          (SheafOfModules.unit ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U))))

Tag 094E, a lemma

Tag 094E in the Stacks Project.

Stacks.Cohomology.CompactExtensionByZero.isCompactObject_singleFunctor_extensionByZeroUnit_of_isWeaklyContractible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CompactObjects/ExtensionByZeroOverAWeaklyContractibleObject.lean, line 174.

Stacks 094E. Let (C, O) be a ringed site and let U be an object of C which is quasi-compact and weakly contractible. Then j_{U!} O_U, placed in degree zero, is a compact object of the unbounded derived category of O-modules.

The two hypotheses of Stacks 094D are discharged: weak contractibility makes Γ(U, -) exact, so cohomology over U vanishes in positive degrees and in particular has finite cohomological dimension, and together with quasi-compactness it makes every R ᵖ Γ(U, -) commute with direct sums.

theorem isCompactObject_singleFunctor_extensionByZeroUnit_of_isWeaklyContractible
    (hU : X.J.IsQuasiCompactObject U) (hU' : X.J.IsWeaklyContractible U) :
    IsCompactObject.{u}
      ((DerivedCategory.singleFunctor
          (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) 0).obj
        ((SheafOfModules.pullback.{u} (F := Over.forget U)
          (𝟙 ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U))).obj
          (SheafOfModules.unit ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U))))

Tag 09JC, a lemma

Tag 09JC in the Stacks Project.

Stacks.Cohomology.hom_coproduct_bijective_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CompactObjects/PerfectObjectsAreCompact.lean, line 317. The attribute's comment: “(a) bounded-below compactness; assumes the 08JJ reduction, not formalized”.

Stacks 09JC (a). Let (C, O) be a ringed site, let B be a collection of objects of C with a cofinal system of finite coverings whose fibre products again lie in B — hypotheses (1), (2) and (3) of the tag, with B the quasi-compact objects — and let X₀ be a member of B, the quasi-compact final object of the tag. Let K be a perfect object of D(O). If M : I → D(O) has a bounded-below coproduct, then morphisms from K into that coproduct are finite sums, Hom(K, ⨁ M_i) = ⨁ Hom(K, M_i): the object K is compact relative to D⁺(O).

The hypothesis hreduce is the reduction the source performs, and is what perfectness of K is used for: by Stacks 08JJ the dual K^∨ satisfies Hom_{D(O)}(K, N) = H⁰(X₀, K^∨ ⊗^L_O N) naturally in N, the functor T = K^∨ ⊗^L_O - commutes with direct sums, and T keeps a bounded-below coproduct bounded below. None of those three facts is available in this library — see "What this file assumes" in the module documentation — so the reduction is assumed; granted it, this is Stacks 0G22 at U = X₀.

theorem hom_coproduct_bijective_of_isPerfect
    (B : Set X.C) (Cov : ∀ U : X.C, Set (PreZeroHypercover.{c} U))
    (hCov : ∀ (U : X.C) (F : PreZeroHypercover.{c} U), Cov U F → F.sieve₀ ∈ X.J U)
    (hfinite : ∀ (U : X.C) (F : PreZeroHypercover.{c} U), Cov U F → HasIntersectionsIn B F)
    (hcofinal : ∀ (U : X.C), B U → ∀ S ∈ X.J U,
      ∃ F : PreZeroHypercover.{c} U, Cov U F ∧ F.sieve₀ ≤ S)
    (X₀ : X.C) (hX₀ : B X₀)
    (K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (hK : X.IsPerfect K)
    {I : Type i} [DecidableEq I]
    (M : I → DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    [HasCoproduct M]
    (hreduce : X.IsPerfect K →
      ∃ T : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ⥤
          DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)),
        ∃ _ : PreservesColimit (Discrete.functor M) T,
          (DerivedCategory.TStructure.t
            (C := SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))).plus
              (T.obj (∐ M)) ∧
          ∃ e : ∀ N : DerivedCategory
              (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)), (K ⟶ N) ≃+
              ((DerivedCategory.singleFunctor
                  (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) 0).obj
                (extensionByZeroUnit.{u, u, u, u} X.J
                  (Stacks.SheafOfModules.Tensor.ringSheaf X.O) X₀) ⟶ T.obj N),
            ∀ {N N' : DerivedCategory
                (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))}
              (f : K ⟶ N) (g : N ⟶ N'), e N' (f ≫ g) = e N f ≫ T.map g) :
    Function.Bijective
      (DirectSum.toAddMonoid fun j => Preadditive.rightComp K (Limits.Sigma.ι M j))

Stacks.Cohomology.isCompactObject_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CompactObjects/PerfectObjectsAreCompact.lean, line 363. The attribute's comment: “(b) unbounded compactness; assumes the 08JJ reduction, 0739 sums; not formalized”.

Stacks 09JC (b). Let (C, O) be a ringed site, let X₀ be an object of C — the quasi-compact final object of the tag — and let K be a perfect object of D(O). If cohomology over X₀ has finite cohomological dimension, that is (C, O) has finite cohomological dimension, and if the functors F ↦ H^p(X₀, F) commute with direct sums, then K is a compact object of D(O).

The hypothesis hreduce is the reduction the source performs, and is what perfectness of K is used for: by Stacks 08JJ the dual K^∨ satisfies Hom_{D(O)}(K, N) = H⁰(X₀, K^∨ ⊗^L_O N) naturally in N, and T = K^∨ ⊗^L_O - commutes with direct sums. Neither fact is available in this library — see "What this file assumes" in the module documentation — so the reduction is assumed; granted it, this is Stacks 094D at U = X₀. The hypothesis hsums is what hypotheses (2) and (3) of the tag supply through Stacks 0739.

theorem isCompactObject_of_isPerfect (X₀ : X.C)
    (K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (hK : X.IsPerfect K)
    (hcd : ∃ d : ℤ, ∀ (p : ℕ)
      (G : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)), d < (p : ℤ) →
        IsZero (((SheafOfModules.evaluation.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)
          (op X₀)).rightDerived p).obj G))
    (hsums : ∀ (p : ℕ) (I : Type w), PreservesColimitsOfShape (Discrete I)
      ((SheafOfModules.evaluation.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)
        (op X₀)).rightDerived p))
    (hreduce : X.IsPerfect K →
      ∃ T : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ⥤
          DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)),
        ∃ _ : ∀ I : Type w, PreservesColimitsOfShape (Discrete I) T,
          ∃ e : ∀ N : DerivedCategory
              (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)), (K ⟶ N) ≃+
              ((DerivedCategory.singleFunctor
                  (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) 0).obj
                ((SheafOfModules.pullback.{u} (F := Over.forget X₀)
                  (𝟙 ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over X₀))).obj
                    (SheafOfModules.unit ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over X₀))) ⟶
                T.obj N),
            ∀ {N N' : DerivedCategory
                (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))}
              (f : K ⟶ N) (g : N ⟶ N'), e N' (f ≫ g) = e N f ≫ T.map g) :
    IsCompactObject.{w} K

AlgebraicGeometry.RingedSite.isCompactObject_of_isPerfect_of_isTerminal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/CompactObjects/PerfectDualReduction.lean, line 239. The attribute's comment: “(b) unbounded compactness of a perfect object, with the 08JJ reduction DISCHARGED rather than assumed; the 0739 commutation of the cohomology functors with direct sums is still a hypothesis here, and is discharged from hypotheses (2) and (3) of the tag in Stacks.Cohomology.QuasiCompactSite.hom_coproduct_bijective_and_isCompactObject_of_isPerfect, which states both clauses”.

Stacks 09JC (b). Let (C, O) be a ringed site with a final object X₀ and let K be a perfect object of D(O). If (C, O) has finite cohomological dimension, that is H^p(X₀, F) = 0 for every O-module F and every p beyond a fixed bound, and if the functors F ↦ H^p(X₀, F) commute with direct sums, then K is a compact object of D(O).

Unlike Stacks.Cohomology.isCompactObject_of_isPerfect this carries no hypothesis standing in for the reduction of Stacks 08JJ: the functor is - ⊗^L_O K^∨ for the canonical derived tensor product of Stacks 06YU, it commutes with direct sums by preservesColimitsOfShape_derivedTensorFlip, and the natural bijection is derivedDualHomEquivOfIsoStructureSheaf at the identification derivedExtensionByZeroUnitIsoStructureSheaf of j_{X₀!}O_{X₀}[0] with O[0]. Perfectness of K is used exactly where the source uses it, to produce that bijection. What is still a hypothesis, as in the conditional form, is the commutation hsums of the higher cohomology functors with direct sums, which the source supplies from Stacks 0739.

theorem isCompactObject_of_isPerfect_of_isTerminal (X₀ : X.C) (hX₀ : IsTerminal X₀)
    (K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (hK : X.IsPerfect K)
    (hcd : ∃ d : ℤ, ∀ (p : ℕ)
      (G : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)), d < (p : ℤ) →
      IsZero (((SheafOfModules.evaluation.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)
        (op X₀)).rightDerived p).obj G))
    (hsums : ∀ (p : ℕ) (I : Type u), PreservesColimitsOfShape (Discrete I)
      ((SheafOfModules.evaluation.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)
        (op X₀)).rightDerived p)) :
    IsCompactObject.{u} K

Stacks.Cohomology.QuasiCompactSite.hom_coproduct_bijective_and_isCompactObject_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/CompactObjects/PerfectObjectsOnAQuasiCompactSite.lean, line 227.

Stacks 09JC. Let (C, O) be a ringed site and assume C has the three properties of the tag: a quasi-compact final object X₀, a cofinal system of finite coverings by quasi-compact objects for every quasi-compact object, and quasi-compact fibre products inside such a covering. Let K be a perfect object of D(O). Then

• (a) K is a compact object of D⁺(O) in the sense of the tag: if M : I → D(O) is a family whose coproduct ⨁ M_i is bounded below, then the canonical map ⨁ Hom(K, M_i) → Hom(K, ⨁ M_i) is bijective; and
• (b) if (C, O) has finite cohomological dimension, that is if there is a d with H^p(X₀, F) = 0 for p > d and every O-module F, then K is a compact object of D(O).

Hypothesis (1) of the tag is hterm, hqc and hX₀; hypotheses (2) and (3) are the covering data B, Cov, hCov, hcofinal and hfinite, Stacks.Cohomology.HasIntersectionsIn carrying the finiteness clause of (2) together with the whole of (3). See "How the hypotheses of the tag are read" in the module documentation.

Both clauses rest on the source's reduction to j_{X₀!}O_{X₀}, which is AlgebraicGeometry.RingedSite.derivedDualHomEquivOfIsoStructureSheaf together with AlgebraicGeometry.RingedSite.preservesColimitsOfShape_derivedTensorFlip. Clause (a) then needs the global Tor amplitude of K^∨, which is hasFiniteTorDimension_derivedDual_of_isPerfect from (1); clause (b) needs the commutation of the cohomology functors over X₀ with direct sums, which is preservesCoproducts_rightDerived_evaluation_of_covers from (2) and (3).

theorem hom_coproduct_bijective_and_isCompactObject_of_isPerfect
    (B : Set X.C) (Cov : ∀ U : X.C, Set (PreZeroHypercover.{c} U))
    (hCov : ∀ (U : X.C) (F : PreZeroHypercover.{c} U), Cov U F → F.sieve₀ ∈ X.J U)
    (hfinite : ∀ (U : X.C) (F : PreZeroHypercover.{c} U), Cov U F →
      Stacks.Cohomology.HasIntersectionsIn B F)
    (hcofinal : ∀ (U : X.C), B U → ∀ S ∈ X.J U,
      ∃ F : PreZeroHypercover.{c} U, Cov U F ∧ F.sieve₀ ≤ S)
    (X₀ : X.C) (hterm : IsTerminal X₀) (hqc : X.J.IsQuasiCompactObject X₀) (hX₀ : B X₀)
    (K : DerivedCategory (_root_.SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) (hK : X.IsPerfect K) :
    (∀ {I : Type u} [DecidableEq I]
        (M : I → DerivedCategory (_root_.SheafOfModules.{u}
          (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) [HasCoproduct M],
        DerivedCategoryB.IsBoundedBelow (∐ M) →
        Function.Bijective
          (DirectSum.toAddMonoid fun j => Preadditive.rightComp K (Limits.Sigma.ι M j))) ∧
      ((∃ d : ℤ, ∀ (p : ℕ) (G : _root_.SheafOfModules.{u}
            (Stacks.SheafOfModules.Tensor.ringSheaf X.O)), d < (p : ℤ) →
          IsZero (((_root_.SheafOfModules.evaluation.{u}
            (Stacks.SheafOfModules.Tensor.ringSheaf X.O) (op X₀)).rightDerived p).obj G)) →
        IsCompactObject.{u} K)

Sources

• Section 21.52, Tag 0948
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Cohomology.CompactObjects.exists_retract_finiteComplex_of_isCompactObject · Stacks.Cohomology.exists_retract_finiteComplex_extensionByZero_of_isCompactObject · Stacks.Cohomology.extensionByZero_unit_hom_coproduct_bijective · Stacks.Cohomology.extensionByZero_unit_hom_coproduct_bijective_of_hasIntersectionsIn · Stacks.Cohomology.CompactExtensionByZero.isCompactObject_singleFunctor_extensionByZeroUnit · Stacks.Cohomology.CompactExtensionByZero.isCompactObject_singleFunctor_extensionByZeroUnit_of_isWeaklyContractible · Stacks.Cohomology.hom_coproduct_bijective_of_isPerfect · Stacks.Cohomology.isCompactObject_of_isPerfect

Section21.53 Complexes with locally constant cohomology sheaves#

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

Tag 094G, a lemma

Tag 094G in the Stacks Project.

Stacks.ConstantSheaf.exists_cover_isRepresentedByLocallyConstantComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/LocallyConstant/BoundedComplexes.lean, line 195. The attribute's comment: “the case of at most one nonzero cohomology sheaf”.

Stacks Tag 094G, the case of at most one nonzero cohomology sheaf. Let K be an object of the derived category of sheaves of Λ-modules whose cohomology is concentrated in a single degree n and whose cohomology sheaves are locally constant of finite type. Then every object U of the site has a covering family V i ⟶ U such that the restriction of K to each slice site C/V i is represented by a complex of locally constant sheaves of Λ-modules of finite type, concentrated in degree n.

theorem exists_cover_isRepresentedByLocallyConstantComplex (n : ℤ) (U : C)
    (K : DerivedCategory (Sheaf J (ModuleCat.{max u v w} Λ)))
    [K.IsGE n] [K.IsLE n]
    (hK : ∀ i : ℤ, IsFiniteTypeLocallyConstantModuleSheaf.{v, u, w} J Λ
      ((DerivedCategory.homologyFunctor _ i).obj K)) :
    ∃ (I : Type (max u v)) (V : I → C) (f : ∀ i, V i ⟶ U),
      Sieve.ofArrows V f ∈ J U ∧ ∀ i : I,
        IsRepresentedByLocallyConstantComplex.{v, max u v, w} (J.over (V i)) Λ n n
          ((J.overPullback (ModuleCat.{max u v w} Λ) (V i)).mapDerivedCategory.obj K)

Stacks.ConstantSheaf.exists_cover_isRepresentedByLocallyConstantComplex_of_isGE_of_isLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/LocallyConstant/BoundedComplexInduction.lean, line 707. The attribute's comment: “the general case: the induction on the number of nonzero cohomology sheaves”.

Stacks Tag 094G, the general case. Let K be an object of the derived category of sheaves of Λ-modules over a Noetherian ring whose cohomology is concentrated in the degrees [a, b] and all of whose cohomology sheaves are locally constant of finite type. Then every object U of the site has a covering family V i ⟶ U such that the restriction of K to each slice site C / V i is represented by a complex of locally constant sheaves of Λ-modules of finite type, concentrated in the degrees [a, b].

This is the statement of the source for an arbitrary number of nonzero cohomology sheaves, proved by the source's induction on b - a; Stacks.ConstantSheaf.exists_cover_isRepresentedByLocallyConstantComplex is the base case a = b of that induction. The complex produced here is in fact degreewise constant on each member of the covering family, which is more than the conclusion records.

public theorem exists_cover_isRepresentedByLocallyConstantComplex_of_isGE_of_isLE
    {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
    (Λ : Type w) [CommRing Λ] [IsNoetherianRing Λ]
    [∀ V : C, HasWeakSheafify (J.over V) (ModuleCat.{max u v w} Λ)]
    (a b : ℤ) (hab : a ≤ b) (U : C)
    (K : DerivedCategory (Sheaf J (ModuleCat.{max u v w} Λ)))
    [K.IsGE a] [K.IsLE b]
    (hK : ∀ i : ℤ, IsFiniteTypeLocallyConstantModuleSheaf.{v, u, w} J Λ
      ((DerivedCategory.homologyFunctor _ i).obj K)) :
    ∃ (I : Type (max u v)) (V : I → C) (f : ∀ i, V i ⟶ U),
      Sieve.ofArrows V f ∈ J U ∧ ∀ i : I,
        IsRepresentedByLocallyConstantComplex.{v, max u v, w} (J.over (V i)) Λ a b
          ((J.overPullback (ModuleCat.{max u v w} Λ) (V i)).mapDerivedCategory.obj K)

Tag 09BD, a lemma

Tag 09BD in the Stacks Project.

AlgebraicGeometry.RingedSite.exists_coveringSieve_complexMap_constant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/StrictlyPerfect/MapOutOfAConstantComplex.lean, line 395. The attribute's comment: “local_representation_for_the_constant_complex”.

Maps out of the complex of constant sheaves of modules. Let Λ be a commutative ring, let K^• be a bounded complex of finite projective Λ-modules, and let L^• be a complex of sheaves of modules over the restriction to U of the structure sheaf Λ̲ of the constant ringed site. Any morphism K̲^• ⟶ L^• of D(Λ̲|_U) is, after restriction along the arrows of a covering sieve of U, the image under the localisation functor of a morphism of complexes.

theorem exists_coveringSieve_complexMap_constant
    [∀ W : C, HasSheafify (J.over W) AddCommGrpCat.{0}]
    [∀ W : C, (J.over W).WEqualsLocallyBijective AddCommGrpCat.{0}]
    [HasDerivedCategory.{d}
      (_root_.SheafOfModules.{0}
        ((Stacks.SheafOfModules.Tensor.ringSheaf (constantRingedSite J Λ).O).over U))]
    {P : CochainComplex (ModuleCat.{0} Λ) ℤ} (a b : ℤ)
    [P.IsStrictlyGE a] [P.IsStrictlyLE b]
    (hfin : ∀ i : ℤ, Module.Finite Λ (P.X i)) (hproj : ∀ i : ℤ, Module.Projective Λ (P.X i))
    {F : CochainComplex
      (_root_.SheafOfModules.{0}
        ((Stacks.SheafOfModules.Tensor.ringSheaf (constantRingedSite J Λ).O).over U)) ℤ}
    (α : DerivedCategory.Q.obj
        (((constantFunctorOver J Λ U).mapHomologicalComplex (ComplexShape.up ℤ)).obj P) ⟶
      DerivedCategory.Q.obj F) :
    ∃ S : Sieve U, S ∈ J U ∧
      ∀ {V : C} (f : V ⟶ U), S f →
        let H := _root_.SheafOfModules.overMap
          (Stacks.SheafOfModules.Tensor.ringSheaf (constantRingedSite J Λ).O) f
        ∃ (hsheaf : HasSheafify (J.over V) AddCommGrpCat)
          (hlocal : (J.over V).WEqualsLocallyBijective AddCommGrpCat),
          letI := hsheaf
          letI := hlocal
          letI : HasDerivedCategory
              (_root_.SheafOfModules
                ((Stacks.SheafOfModules.Tensor.ringSheaf (constantRingedSite J Λ).O).over V)) :=
            HasDerivedCategory.standard _
          ∃ (hadd : H.Additive)
            (hlim : PreservesFiniteLimits H)
            (hcolim : PreservesFiniteColimits H),
            letI := hadd
            letI := hlim
            letI := hcolim
            ∃ β : (H.mapHomologicalComplex (ComplexShape.up ℤ)).obj
                (((constantFunctorOver J Λ U).mapHomologicalComplex (ComplexShape.up ℤ)).obj P) ⟶
                (H.mapHomologicalComplex (ComplexShape.up ℤ)).obj F,
              H.mapDerivedCategory.map α ≫ H.mapDerivedCategoryFactors.hom.app F =
                H.mapDerivedCategoryFactors.hom.app
                    (((constantFunctorOver J Λ U).mapHomologicalComplex
                      (ComplexShape.up ℤ)).obj P) ≫
                  DerivedCategory.Q.map β

Stacks.SheafOfModules.Constant.isStrictlyPerfect_constantModuleSheafFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/StrictlyPerfect/MapOutOfALocallyConstantComplex.lean, line 158. The attribute's comment: “strict_perfectness_of_the_constant_complex”.

The complex of constant sheaves of modules on a bounded complex of finite projective Λ-modules is strictly perfect over the constant sheaf of rings Λ̲.

theorem isStrictlyPerfect_constantModuleSheafFunctor
    {P : CochainComplex (ModuleCat.{w} Λ) ℤ} (a b : ℤ)
    [P.IsStrictlyGE a] [P.IsStrictlyLE b]
    (hfin : ∀ i : ℤ, Module.Finite Λ (P.X i)) (hproj : ∀ i : ℤ, Module.Projective Λ (P.X i)) :
    IsStrictlyPerfect ((constantSheaf J RingCat.{w}).obj (RingCat.of Λ))
      (((constantModuleSheafFunctor J (R := Λ)).mapHomologicalComplex
        (ComplexShape.up ℤ)).obj P)

AlgebraicGeometry.RingedSite.exists_coveringSieve_complexMap_of_finite_projective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/StrictlyPerfect/MapOutOfALocallyConstantComplex.lean, line 258. The attribute's comment: “local_representation_for_a_transported_finite_projective_complex”.

Let Φ be an additive right exact functor from Λ-modules to sheaves of O|_U-modules taking Λ to the unit object. Let K^• be a bounded complex of finite projective Λ-modules and L^• a complex of sheaves of O|_U-modules. Any morphism Φ(K^•) ⟶ L^• of D(O|_U) is, after restriction along the arrows of a covering sieve of U, the image under the localisation functor of a morphism of complexes.

theorem exists_coveringSieve_complexMap_of_finite_projective
    {Λ : Type} [Ring Λ]
    (Φ : ModuleCat.{0} Λ ⥤ SheafOfModules.{0} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U))
    [Φ.Additive]
    [PreservesFiniteColimits Φ]
    (e : Φ.obj (ModuleCat.of Λ Λ) ≅
      SheafOfModules.unit ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U))
    {P : CochainComplex (ModuleCat.{0} Λ) ℤ} (a b : ℤ)
    [P.IsStrictlyGE a] [P.IsStrictlyLE b]
    (hfin : ∀ i : ℤ, Module.Finite Λ (P.X i)) (hproj : ∀ i : ℤ, Module.Projective Λ (P.X i))
    {F : CochainComplex
      (SheafOfModules.{0} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U)) ℤ}
    (α : DerivedCategory.Q.obj ((Φ.mapHomologicalComplex (ComplexShape.up ℤ)).obj P) ⟶
      DerivedCategory.Q.obj F) :
    ∃ S : Sieve U, S ∈ X.J U ∧
      ∀ {V : X.C} (f : V ⟶ U), S f →
        let H := SheafOfModules.overMap (Stacks.SheafOfModules.Tensor.ringSheaf X.O) f
        ∃ (hsheaf : HasSheafify (X.J.over V) AddCommGrpCat)
          (hlocal : (X.J.over V).WEqualsLocallyBijective AddCommGrpCat),
          letI := hsheaf
          letI := hlocal
          letI : HasDerivedCategory
              (SheafOfModules ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over V)) :=
            HasDerivedCategory.standard _
          ∃ (hadd : H.Additive)
            (hlim : PreservesFiniteLimits H)
            (hcolim : PreservesFiniteColimits H),
            letI := hadd
            letI := hlim
            letI := hcolim
            ∃ β : (H.mapHomologicalComplex (ComplexShape.up ℤ)).obj
                ((Φ.mapHomologicalComplex (ComplexShape.up ℤ)).obj P) ⟶
                (H.mapHomologicalComplex (ComplexShape.up ℤ)).obj F,
              H.mapDerivedCategory.map α ≫ H.mapDerivedCategoryFactors.hom.app F =
                H.mapDerivedCategoryFactors.hom.app
                    ((Φ.mapHomologicalComplex (ComplexShape.up ℤ)).obj P) ≫
                  DerivedCategory.Q.map β

Tag 09BE, a lemma

Tag 09BE in the Stacks Project.

Stacks.ConstantSheaf.exists_cover_overPullback_eq_constantSheaf_mapHomologicalComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafComplexLocalHom.lean, line 278. The attribute's comment: “local_constancy_of_a_map_of_constant_complexes”.

The local constancy of a map of complexes of constant sheaves of modules. Let P be a complex of finite projective Λ-modules which is nonzero in only finitely many degrees, let T be any complex of Λ-modules, and write P̲, T̲ for the associated complexes of constant sheaves of Λ-modules. A map of complexes β : P̲|_U ⟶ T̲|_U on a slice site is, after restriction along the arrows of a covering sieve of U, the image of an honest map of complexes P ⟶ T of Λ-modules.

This is the content Stacks 09BE adds to Stacks 09BD at the level of complexes, i.e. the application of Stacks 093S (3) made in the source's proof.

theorem exists_cover_overPullback_eq_constantSheaf_mapHomologicalComplex
    [J.WEqualsLocallyBijective (ModuleCat.{w} Λ)]
    [∀ V : C, HasWeakSheafify (J.over V) (ModuleCat.{w} Λ)]
    [∀ V : C, (J.over V).WEqualsLocallyBijective (ModuleCat.{w} Λ)]
    (P T : CochainComplex (ModuleCat.{w} Λ) ℤ)
    (hs : {n : ℤ | ¬ IsZero (P.X n)}.Finite)
    (hfin : ∀ n : ℤ, Module.Finite Λ (P.X n))
    (hproj : ∀ n : ℤ, Module.Projective Λ (P.X n)) (U : C)
    (β : ((J.overPullback (ModuleCat.{w} Λ) U).mapHomologicalComplex (ComplexShape.up ℤ)).obj
        (((constantSheaf J (ModuleCat.{w} Λ)).mapHomologicalComplex (ComplexShape.up ℤ)).obj P) ⟶
      ((J.overPullback (ModuleCat.{w} Λ) U).mapHomologicalComplex (ComplexShape.up ℤ)).obj
        (((constantSheaf J (ModuleCat.{w} Λ)).mapHomologicalComplex (ComplexShape.up ℤ)).obj T)) :
    ∃ S : Sieve U, S ∈ J U ∧ ∀ {V : C} (f : V ⟶ U), S f →
      ∃ g : P ⟶ T, ∀ n,
        (J.overMapPullback (ModuleCat.{w} Λ) f).map (β.f n) =
          (J.overPullback (ModuleCat.{w} Λ) V).map
            ((constantSheaf J (ModuleCat.{w} Λ)).map (g.f n))

Stacks.ConstantDerivedMap.exists_cover_overPullback_map_eq_overConstantSheaf_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/StrictlyPerfect/DerivedMapOfConstantComplexes.lean, line 515.

Stacks 09BE. Let (C, J) be a site, X an object of C (in the source, its final object), Λ a ring, and K, L objects of D(Λ) with K perfect. Let φ : K̲ ⟶ L̲ be a map in D(C, Λ). There exists a covering {U_i ⟶ X} such that φ|_{U_i} is equal to α̲_i for some map α_i : K ⟶ L in D(Λ).

Here φ|_{U_i} is the image of φ under the functor D(C, Λ) ⥤ D(C/U_i, Λ) induced by restriction, and α̲_i is the map K̲ ⟶ L̲ of D(C/U_i, Λ) induced by the constant sheaf functor of the slice site C/U_i; the two objects (K̲)|_{U_i} and K̲ of D(C/U_i, Λ) are identified by the canonical isomorphism Stacks.ConstantDerivedMap.overConstantSheafMapDerivedCategoryIso (and likewise for L), which is the first conjunct. The second conjunct records the equivalent form φ|_{U_i} = (α̲_i)|_{U_i}, with α̲_i the constant map on C.

The derived categories D(Λ), D(C, Λ) and D(C/V, Λ) are taken with arbitrary models (HasDerivedCategory instances, which always exist: HasDerivedCategory.standard). The site is small and the modules live in its universe u, the library's standard one-universe convention for sheaves of modules on a site; the ring is commutative, as are all rings of the Stacks Project; and the final object X of the source is generalized to an arbitrary object.

theorem exists_cover_overPullback_map_eq_overConstantSheaf_map
    [HasDerivedCategory.{d} (ModuleCat.{u} Λ)]
    (X : C) {K L : DerivedCategory (ModuleCat.{u} Λ)} (hK : StacksDraft.Perfect.IsPerfect K)
    (φ : (constantSheaf J (ModuleCat.{u} Λ)).mapDerivedCategory.obj K ⟶
      (constantSheaf J (ModuleCat.{u} Λ)).mapDerivedCategory.obj L) :
    ∃ (ι : Type u) (U : ι → C) (f : ∀ i, U i ⟶ X), Sieve.ofArrows U f ∈ J X ∧
      ∀ i, ∃ α : K ⟶ L,
        (J.overPullback (ModuleCat.{u} Λ) (U i)).mapDerivedCategory.map φ =
          (overConstantSheafMapDerivedCategoryIso J Λ (U i)).inv.app K ≫
            (constantSheaf (J.over (U i)) (ModuleCat.{u} Λ)).mapDerivedCategory.map α ≫
              (overConstantSheafMapDerivedCategoryIso J Λ (U i)).hom.app L ∧
        (J.overPullback (ModuleCat.{u} Λ) (U i)).mapDerivedCategory.map φ =
          (J.overPullback (ModuleCat.{u} Λ) (U i)).mapDerivedCategory.map
            ((constantSheaf J (ModuleCat.{u} Λ)).mapDerivedCategory.map α)

Tag 094H, a lemma

Tag 094H in the Stacks Project.

Stacks.ConstantRingModules.isFiniteTypeLocallyConstantModuleSheaf_homology_constantDerivedTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/LocallyConstant/ConstantDerivedTensorLocallyConstant.lean, line 302. The attribute's comment: “the full statement for the derived tensor product over the constant sheaf of commutative rings on Λ: for K and L in D^- of the sheaves of Λ-modules whose cohomology sheaves are locally constant of finite type, so are those of K ⊗^L_Λ L. The site is small and every universe is one, which is the configuration in which the derived tensor product of Stacks 06YU is available; apart from that nothing is assumed, and in particular the bounded case of the tag is proved here and not supposed”.

Let (C, J) be a small site, Λ a Noetherian commutative ring, and let K and L be objects of D^- of the sheaves of Λ-modules whose cohomology sheaves are locally constant of finite type. Then the cohomology sheaves of K ⊗^L_Λ L are locally constant of finite type, where the derived tensor product is Stacks.ConstantRingModules.constantDerivedTensor, taken over the constant sheaf of commutative rings on Λ.

theorem isFiniteTypeLocallyConstantModuleSheaf_homology_constantDerivedTensor
    (K L : DerivedCategory.Minus (Sheaf J (ModuleCat.{u} Λ)))
    (hK : ∀ i : ℤ, IsFiniteTypeLocallyConstantModuleSheaf.{u, u, u} J Λ
      ((DerivedCategory.homologyFunctor _ i).obj K.obj))
    (hL : ∀ i : ℤ, IsFiniteTypeLocallyConstantModuleSheaf.{u, u, u} J Λ
      ((DerivedCategory.homologyFunctor _ i).obj L.obj)) (i : ℤ) :
    IsFiniteTypeLocallyConstantModuleSheaf.{u, u, u} J Λ
      ((DerivedCategory.homologyFunctor _ i).obj
        (((constantDerivedTensor J Λ).obj K.obj).obj L.obj))

Stacks.ConstantSheaf.isFiniteTypeLocallyConstantModuleSheaf_mapBifunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/LocallyConstant/DerivedTensorBoundedAbove.lean, line 367. The attribute's comment: “the termwise conclusion: every term of the total complex of an additive bifunctor applied to two bounded above complexes of locally constant sheaves of finite type is locally constant of finite type”.

Stacks Tag 094H, the termwise conclusion. Let P and Q be cochain complexes of sheaves of Λ-modules, bounded strictly above, all of whose terms are locally constant of finite type, and let T be a bifunctor on sheaves of Λ-modules, additive in each variable, whose values on those terms are locally constant of finite type — for the sheafified tensor product this is Stacks.ConstantSheaf.isFiniteTypeLocallyConstantModuleSheaf_tensor. Then every term of the total complex of T applied to P and Q is locally constant of finite type.

This is what the bounded case of Tag 094H consumes once Tag 094G and a finite free model have produced the two complexes: the derived tensor product of two such complexes is the class of their total tensor complex, so its cohomology sheaves are subquotients of these terms, and the weak Serre property of Tag 093U finishes the argument.

theorem isFiniteTypeLocallyConstantModuleSheaf_mapBifunctor
    (T : Sheaf J (ModuleCat.{max u v w} Λ) ⥤ Sheaf J (ModuleCat.{max u v w} Λ) ⥤
      Sheaf J (ModuleCat.{max u v w} Λ)) [T.Additive] [∀ X, (T.obj X).Additive]
    (P Q : CochainComplex (Sheaf J (ModuleCat.{max u v w} Λ)) ℤ)
    [HomologicalComplex.HasMapBifunctor P Q T (ComplexShape.up ℤ)] (a b : ℤ)
    [P.IsStrictlyLE a] [Q.IsStrictlyLE b]
    (hT : ∀ p q, IsFiniteTypeLocallyConstantModuleSheaf.{v, u, w} J Λ
      ((T.obj (P.X p)).obj (Q.X q))) (n : ℤ) :
    IsFiniteTypeLocallyConstantModuleSheaf.{v, u, w} J Λ
      ((HomologicalComplex.mapBifunctor P Q T (ComplexShape.up ℤ)).X n)

Stacks.ConstantSheaf.isFiniteTypeLocallyConstantModuleSheaf_homology_of_bounded, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/LocallyConstant/DerivedTensorBoundedAbove.lean, line 392. The attribute's comment: “the reduction of the bounded above case to the bounded case, for a bifunctor exact in each variable which carries bounds above to their sum; the bounded case is a hypothesis”.

Stacks Tag 094H, the reduction of the bounded above case to the bounded case. Let T be a bifunctor on the derived category of sheaves of Λ-modules which is exact in each variable and carries objects in degrees ≤ a and ≤ b to objects in degrees ≤ a + b — both are properties of the derived tensor product of Tag 06YU. If the conclusion of Tag 094H holds for bounded K and L, then it holds for K and L in D^-.

The proof is the first half of the source's: H^i((T.obj K).obj L) is computed by the bounded truncations τ^{> i-b-1}K and τ^{> i-a-1}L.

theorem isFiniteTypeLocallyConstantModuleSheaf_homology_of_bounded
    (T : DerivedCategory (Sheaf J (ModuleCat.{max u v w} Λ)) ⥤
      DerivedCategory (Sheaf J (ModuleCat.{max u v w} Λ)) ⥤
      DerivedCategory (Sheaf J (ModuleCat.{max u v w} Λ)))
    [∀ K, (T.obj K).CommShift ℤ] [∀ K, (T.obj K).IsTriangulated]
    [∀ L, (T.flip.obj L).CommShift ℤ] [∀ L, (T.flip.obj L).IsTriangulated]
    (hbound : ∀ (K L : DerivedCategory (Sheaf J (ModuleCat.{max u v w} Λ))) (a b : ℤ),
      K.IsLE a → L.IsLE b → ((T.obj K).obj L).IsLE (a + b))
    (hbounded : ∀ (K L : DerivedCategory.Bounded (Sheaf J (ModuleCat.{max u v w} Λ))),
      (∀ i, IsFiniteTypeLocallyConstantModuleSheaf.{v, u, w} J Λ
        ((DerivedCategory.homologyFunctor _ i).obj K.obj)) →
      (∀ i, IsFiniteTypeLocallyConstantModuleSheaf.{v, u, w} J Λ
        ((DerivedCategory.homologyFunctor _ i).obj L.obj)) →
      ∀ i, IsFiniteTypeLocallyConstantModuleSheaf.{v, u, w} J Λ
        ((DerivedCategory.homologyFunctor _ i).obj ((T.obj K.obj).obj L.obj)))
    (K L : DerivedCategory.Minus (Sheaf J (ModuleCat.{max u v w} Λ)))
    (hK : ∀ i, IsFiniteTypeLocallyConstantModuleSheaf.{v, u, w} J Λ
      ((DerivedCategory.homologyFunctor _ i).obj K.obj))
    (hL : ∀ i, IsFiniteTypeLocallyConstantModuleSheaf.{v, u, w} J Λ
      ((DerivedCategory.homologyFunctor _ i).obj L.obj)) (i : ℤ) :
    IsFiniteTypeLocallyConstantModuleSheaf.{v, u, w} J Λ
      ((DerivedCategory.homologyFunctor _ i).obj ((T.obj K.obj).obj L.obj))

Tag 094I, a lemma

Tag 094I in the Stacks Project.

Stacks.ConstantRingModules.isFiniteTypeLocallyConstantModuleSheaf_homology_constantDerivedTensor_quotientIdealPow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/LocallyConstant/ConstantRingDerivedTensor.lean, line 300. The attribute's comment: “for a site whose objects, morphisms and coefficient ring lie in one universe, which is where the library's derived tensor product over a sheaf of commutative rings is available; the derived tensor product is constructed, not a parameter. Beyond the source's own hypotheses the binders hold only SmallCategory C, CommRing Λ and IsNoetherianRing Λ: the sheafification conditions this file's construction uses — HasSheafify, WEqualsLocallyBijective and HasSheafCompose for the forgetful functor to abelian groups — are synthesized at such a site, not assumed”.

Stacks Tag 094I. Let (C, J) be a site, Λ a Noetherian commutative ring, I ⊆ Λ an ideal and K an object of D^- of the sheaves of Λ-modules. If the cohomology sheaves of K ⊗^L_Λ Λ/I are locally constant of finite type, then so are those of K ⊗^L_Λ Λ/Iⁿ for every n ≥ 1.

The derived tensor product is Stacks.ConstantRingModules.constantDerivedTensor, the derived tensor product of Stacks 06YU over the constant sheaf of commutative rings on Λ read through the identification of sheaves of modules over it with sheaves of Λ-modules. The proof is isFiniteTypeLocallyConstantModuleSheaf_homology_tensor_quotientIdealPow_of_isLE, in the namespace Stacks.ConstantSheaf, whose bifunctor parameter is instantiated here and whose two properties of it, exactness in the second variable and the degree bound, are Stacks.ConstantRingModules.derivedTensor_isTriangulated and Stacks.ConstantRingModules.isLE_constantDerivedTensor.

theorem isFiniteTypeLocallyConstantModuleSheaf_homology_constantDerivedTensor_quotientIdealPow
    [IsNoetherianRing Λ] (I : Ideal Λ) (b : ℤ)
    (K : DerivedCategory (Sheaf J (ModuleCat.{u} Λ))) [K.IsLE b]
    (hbase : ∀ i : ℤ, IsFiniteTypeLocallyConstantModuleSheaf.{u, u, u} J Λ
      ((DerivedCategory.homologyFunctor _ i).obj
        (derivedTensorConstant J Λ (constantDerivedTensor J Λ) K
          (ModuleCat.of Λ (Λ ⧸ I)))))
    (n : ℕ) (hn : 1 ≤ n) (i : ℤ) :
    IsFiniteTypeLocallyConstantModuleSheaf.{u, u, u} J Λ
      ((DerivedCategory.homologyFunctor _ i).obj
        (derivedTensorConstant J Λ (constantDerivedTensor J Λ) K
          (ModuleCat.of Λ (Λ ⧸ I ^ n))))

Stacks.ConstantSheaf.isFiniteTypeLocallyConstantModuleSheaf_homology_derivedTensorConstant_quotientIdealPow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/LocallyConstant/DerivedTensorConstructed.lean, line 345. The attribute's comment: “the derived tensor product is constructed, not assumed: it is Tag 06YU for the constant ringed site read through the equivalence Sheaf J (ModuleCat Λ) ≌ SheafOfModules Λ̲; the source's own hypotheses only”.

Stacks Tag 094I. Let (C, J) be a site, let Λ be a Noetherian commutative ring, let I ⊆ Λ be an ideal and let K be an object of D^-(C, Λ). If the cohomology sheaves of K ⊗^L_Λ Λ/I are locally constant sheaves of finite type, then so are those of K ⊗^L_Λ Λ/Iⁿ for every n ≥ 1.

The derived tensor product is Stacks.ConstantSheaf.constantDerivedTensor, the derived tensor product of Tag 06YU for the constant ringed site read through the equivalence of Tag 03ET. Nothing about it is assumed: its exactness in the second variable and its bound above are the instances and the theorem of this file, and the mathematics of the tag is isFiniteTypeLocallyConstantModuleSheaf_homology_tensor_quotientIdealPow_of_isLE.

The hypothesis K.IsLE b is the source's K ∈ D^-(C, Λ). Local constancy of finite type is stated over Λ rather than over Λ/Iⁿ, which is equivalent: a Λ-module killed by Iⁿ is of finite type over Λ exactly when it is over Λ/Iⁿ, by Stacks.ConstantSheaf.module_finite_iff_finite_quotient, and constant for one ring exactly when constant for the other.

HasSheafify J (ModuleCat.{u} Λ) is deliberately not a binder here: the namespace is reopened above with a variable line that does not carry it, so that the binder list is the source's own hypotheses and nothing else. At these universes instance search finds it, through Mathlib's sheafification instance for small sites.

theorem isFiniteTypeLocallyConstantModuleSheaf_homology_derivedTensorConstant_quotientIdealPow
    (I : Ideal Λ) (b : ℤ) (K : DerivedCategory (Sheaf J (ModuleCat.{u} Λ))) [K.IsLE b]
    (hbase : ∀ i : ℤ, IsFiniteTypeLocallyConstantModuleSheaf.{u, u, u} J Λ
      ((DerivedCategory.homologyFunctor _ i).obj
        (derivedTensorConstant J Λ (constantDerivedTensor J Λ) K (ModuleCat.of Λ (Λ ⧸ I)))))
    (n : ℕ) (hn : 1 ≤ n) :
    ∀ i : ℤ, IsFiniteTypeLocallyConstantModuleSheaf.{u, u, u} J Λ
      ((DerivedCategory.homologyFunctor _ i).obj
        (derivedTensorConstant J Λ (constantDerivedTensor J Λ) K
          (ModuleCat.of Λ (Λ ⧸ I ^ n))))

Stacks.ConstantSheaf.isFiniteTypeLocallyConstantModuleSheaf_homology_tensor_quotientIdealPow_of_isLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/LocallyConstant/DerivedTensorGradedPieces.lean, line 459. The attribute's comment: “the induction on n from Λ/I to Λ/Iⁿ, with the source's distinguished triangles and its base change to Λ/I both proved rather than assumed. The derived tensor product enters as a bifunctor parameter, and two of its properties are hypotheses: exactness in the second variable, and that it takes objects in degrees ≤ a and ≤ b to objects in degrees ≤ a + b. The parameter is instantiated, and this tag registered with nothing assumed of the derived tensor product, on Stacks.ConstantRingModules.isFiniteTypeLocallyConstantModuleSheaf_homology_constantDerivedTensor_quotientIdealPow”.

Stacks Tag 094I. Let (C, J) be a site, let Λ be a Noetherian ring, let I ⊆ Λ be an ideal and let K be an object of D^- of the sheaves of Λ-modules. Let T stand for the derived tensor product over Λ: a bifunctor on that derived category which is exact in its second variable and carries objects in degrees ≤ a and ≤ b to objects in degrees ≤ a + b. If the cohomology sheaves of K ⊗^L_Λ Λ/I are locally constant of finite type, then so are those of K ⊗^L_Λ Λ/Iⁿ for every n ≥ 1.

For the constructed derived tensor product Stacks.ConstantSheaf.constantDerivedTensor — Tag 06YU for the constant ringed site, read through the equivalence of Tag 03ET — the bifunctor T, its two exactness instances and hbound are discharged in isFiniteTypeLocallyConstantModuleSheaf_homology_derivedTensorConstant_quotientIdealPow, which applies this theorem; the generality Λ : Type (max u v w) here is one the construction cannot be given.

The proof is the source's induction on n along the distinguished triangles

K ⊗^L_Λ Iⁿ/Iⁿ⁺¹ ⟶ K ⊗^L_Λ Λ/Iⁿ⁺¹ ⟶ K ⊗^L_Λ Λ/Iⁿ ⟶ (K ⊗^L_Λ Iⁿ/Iⁿ⁺¹)[1],

supplied by Stacks.ConstantSheaf.exists_distTriang_derivedTensorConstant, with the locally constant sheaves of finite type absorbing the middle vertex because they form a weak Serre subcategory (Tag 093U, through Tag 06UQ). Its remaining input, the local constancy of the graded pieces K ⊗^L_Λ Iⁿ/Iⁿ⁺¹, is isFiniteTypeLocallyConstantModuleSheaf_homology_derivedTensorConstant_of_annihilated: Iⁿ/Iⁿ⁺¹ is a finitely generated Λ-module killed by I, hence has a resolution by finite free Λ/I-modules, which computes each cohomology sheaf of K ⊗^L_Λ Iⁿ/Iⁿ⁺¹ out of finitely many copies of K ⊗^L_Λ Λ/I. That replaces the source's base change identification K ⊗^L_Λ Iⁿ/Iⁿ⁺¹ = (K ⊗^L_Λ Λ/I) ⊗^L_{Λ/I} Iⁿ/Iⁿ⁺¹ together with Tag 094H, and needs neither a derived tensor product over Λ/I nor Tag 094H.

The conclusion is stated over Λ, not over Λ/Iⁿ: a Λ-module killed by Iⁿ is of finite type over Λ exactly when it is over Λ/Iⁿ (Stacks.ConstantSheaf.module_finite_iff_finite_quotient), and constant for one ring exactly when constant for the other.

Besides the source's own hypotheses — Λ Noetherian, I ⊆ Λ an ideal, K in D^-, and the local constancy of K ⊗^L_Λ Λ/I — the binders hold only the bifunctor T with the two properties of a derived tensor product that the argument consumes: exactness in the second variable, and the bound above.

theorem isFiniteTypeLocallyConstantModuleSheaf_homology_tensor_quotientIdealPow_of_isLE
    (T : DerivedCategory (Sheaf J (ModuleCat.{max u v w} Λ)) ⥤
      DerivedCategory (Sheaf J (ModuleCat.{max u v w} Λ)) ⥤
      DerivedCategory (Sheaf J (ModuleCat.{max u v w} Λ)))
    [∀ K, (T.obj K).CommShift ℤ] [∀ K, (T.obj K).IsTriangulated]
    (hbound : ∀ (K L : DerivedCategory (Sheaf J (ModuleCat.{max u v w} Λ))) (a b : ℤ),
      K.IsLE a → L.IsLE b → ((T.obj K).obj L).IsLE (a + b))
    (b : ℤ) (K : DerivedCategory (Sheaf J (ModuleCat.{max u v w} Λ))) [K.IsLE b]
    (hbase : ∀ i : ℤ, IsFiniteTypeLocallyConstantModuleSheaf.{v, u, w} J Λ
      ((DerivedCategory.homologyFunctor _ i).obj
        (derivedTensorConstant J Λ T K (ModuleCat.of Λ (Λ ⧸ I)))))
    (n : ℕ) (hn : 1 ≤ n) :
    ∀ i : ℤ, IsFiniteTypeLocallyConstantModuleSheaf.{v, u, w} J Λ
      ((DerivedCategory.homologyFunctor _ i).obj
        (derivedTensorConstant J Λ T K (ModuleCat.of Λ (Λ ⧸ I ^ n))))

Sources

• Section 21.53, Tag 094F
• AxiomMath/Stacks at 5ed82d14

LeanStacks.ConstantSheaf.exists_cover_isRepresentedByLocallyConstantComplex · Stacks.ConstantSheaf.exists_cover_isRepresentedByLocallyConstantComplex_of_isGE_of_isLE · AlgebraicGeometry.RingedSite.exists_coveringSieve_complexMap_constant · Stacks.SheafOfModules.Constant.isStrictlyPerfect_constantModuleSheafFunctor · AlgebraicGeometry.RingedSite.exists_coveringSieve_complexMap_of_finite_projective · Stacks.ConstantSheaf.exists_cover_overPullback_eq_constantSheaf_mapHomologicalComplex · Stacks.ConstantDerivedMap.exists_cover_overPullback_map_eq_overConstantSheaf_map · Stacks.ConstantRingModules.isFiniteTypeLocallyConstantModuleSheaf_homology_constantDerivedTensor

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.