21.17 Flat resolutions to 21.26 Mayer-Vietoris
Section21.17 Flat resolutions#
Section 21.17 of the Stacks Project, Tag 06YL. 17 tags here are carried by 51 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 06YM, a lemma
Tag 06YM in the Stacks Project.
Stacks.SheafOfModules.Tensor.statement1, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/BifunctorReductionMachinery/TensorIsTriangulated.lean, line 58. The attribute's comment: “the functor F ↦ Tot(G ⊗_O F), the fixed complex on the left”. References: SGA 4 XVII (4.1.6), “comm. O, G fixed, left”; SGA 4½ Etat 0 (1.3.3), “special case”.
Statement 1. Fix a complex
G^•ofO-modules. The functorF^• ↦ Tot(G^• ⊗_O F^•)on the homotopy categoryK(Mod(O))is an exact functor of triangulated categories (Definition 5).Concretely: there is a functor
Φ : K(Mod(O)) ⥤ K(Mod(O))together with a functorial isomorphismξ(aCommShift ℤstructure, incorporating the Koszul signs of tag 0FLG) such that *Φis additive; *Φlifts the complex-level functorF^• ↦ Tot(G^• ⊗_O F^•)through the homotopy quotient -- i.e.quotF ⋙ Φ ≅ leftTensorComplex ⋙ quotF-- so it is well defined onK(Mod(O))(sends homotopic maps to homotopic maps); and *Φ, equipped with the commutation-with-shift datumξ, is a triangulated functor: it commutes with the shift up toξand sends distinguished triangles to distinguished triangles.
theorem statement1
(G : HomologicalComplex (SheafOfModules (ringSheaf R)) (ComplexShape.up ℤ)) :
∃ (Φ : HomotopyCategory (SheafOfModules (ringSheaf R)) (ComplexShape.up ℤ) ⥤
HomotopyCategory (SheafOfModules (ringSheaf R)) (ComplexShape.up ℤ))
(ξ : Φ.CommShift ℤ),
Φ.Additive ∧
Nonempty (quotF R ⋙ Φ ≅ leftTensorComplex R G ⋙ quotF R) ∧
(letI := ξ; Φ.IsTriangulated)
Stacks.SheafOfModules.Tensor.statement2, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/BifunctorReductionMachinery/TensorIsTriangulated.lean, line 84. The attribute's comment: “the functor F ↦ Tot(F ⊗_O G), the fixed complex on the right”. References: SGA 4 XVII (4.1.6), “comm. O, G fixed, right”; SGA 4½ Etat 0 (1.3.3), “special case”.
Statement 2. Fix a complex
G^•ofO-modules. The functorF^• ↦ Tot(F^• ⊗_O G^•)on the homotopy categoryK(Mod(O))is an exact functor of triangulated categories (Definition 5).Concretely: there is a functor
Φ : K(Mod(O)) ⥤ K(Mod(O))together with a functorial isomorphismξ(aCommShift ℤstructure, incorporating the Koszul signs) such that *Φis additive; *Φlifts the complex-level functorF^• ↦ Tot(F^• ⊗_O G^•)through the homotopy quotient -- i.e.quotF ⋙ Φ ≅ rightTensorComplex ⋙ quotF; and *Φ, equipped with the commutation-with-shift datumξ, is a triangulated functor.
theorem statement2
(G : HomologicalComplex (SheafOfModules (ringSheaf R)) (ComplexShape.up ℤ)) :
∃ (Φ : HomotopyCategory (SheafOfModules (ringSheaf R)) (ComplexShape.up ℤ) ⥤
HomotopyCategory (SheafOfModules (ringSheaf R)) (ComplexShape.up ℤ))
(ξ : Φ.CommShift ℤ),
Φ.Additive ∧
Nonempty (quotF R ⋙ Φ ≅ rightTensorComplex R G ⋙ quotF R) ∧
(letI := ξ; Φ.IsTriangulated)
Tag 06YN, a definition
Tag 06YN in the Stacks Project.
Stacks.SheafOfModules.KFlat.KFlat, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/KFlat/KFlatComplexesDefinition.lean, line 97.
A cochain complex
Kof sheaves ofO-modules on a ringed site(C, O)is K-flat when the total tensor complexTot(F ⊗_O K)is acyclic for every acyclic cochain complexFof sheaves ofO-modules.
abbrev KFlat
(K : CochainComplex (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf R)) ℤ) :
Prop
Declarations registered for the tag:
Stacks.SheafOfModules.IsKFlat, declared in the repository, registered withadd_to_stacksin StacksFrontier/CategoryTheory/Sites/Cohomology/KFlat/KFlatComplexes.lean, line 38 (StacksFrontier).
Tag 06YP, a lemma
Tag 06YP in the Stacks Project.
Stacks.SheafOfModules.IsKFlat.tensorRight_preserves_quasiIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/KFlat/TensorPreservesQuasiIso.lean, line 204. The attribute's comment: “the K-flat complex as right tensor factor”.
Tensoring with a K-flat complex on the right and totalising preserves quasi-isomorphisms of the homotopy category.
theorem IsKFlat.tensorRight_preserves_quasiIso
(K : CochainComplex (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf R)) ℤ)
(hK : IsKFlat R K) :
HomotopyCategory.quasiIso
(SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf R)) (ComplexShape.up ℤ) ≤
MorphismProperty.inverseImage
(HomotopyCategory.quasiIso
(SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf R)) (ComplexShape.up ℤ))
(Stacks.SheafOfModules.Tensor.Reduction.bifunctorPhiR
(Stacks.SheafOfModules.Tensor.sheafTensor R) K)
Stacks.SheafOfModules.IsKFlat.tensorLeft_preserves_quasiIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/KFlat/TensorPreservesQuasiIso.lean, line 219. The attribute's comment: “the K-flat complex as left tensor factor”.
Tensoring with a K-flat complex on the left and totalising preserves quasi-isomorphisms of the homotopy category.
theorem IsKFlat.tensorLeft_preserves_quasiIso
(K : CochainComplex (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf R)) ℤ)
(hK : IsKFlat R K) :
HomotopyCategory.quasiIso
(SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf R)) (ComplexShape.up ℤ) ≤
MorphismProperty.inverseImage
(HomotopyCategory.quasiIso
(SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf R)) (ComplexShape.up ℤ))
(Stacks.SheafOfModules.Tensor.Reduction.bifunctorPhi
(Stacks.SheafOfModules.Tensor.sheafTensor R) K)
Stacks.SheafOfModules.IsKFlat.quasiIso_tensorComplex_map_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/KFlat/TensorPreservesQuasiIso.lean, line 305. The attribute's comment: “for complexes, the K-flat complex as right tensor factor”.
For
KK-flat andfa quasi-isomorphism, the total tensor productTot(f ⊗ 1_K)is a quasi-isomorphism.
theorem IsKFlat.quasiIso_tensorComplex_map_app
(K : CochainComplex (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf R)) ℤ)
(hK : IsKFlat R K)
{A B : CochainComplex (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf R)) ℤ}
(f : A ⟶ B) (hf : QuasiIso f) :
QuasiIso (((Stacks.SheafOfModules.Tensor.tensorComplex R).map f).app K)
Stacks.SheafOfModules.IsKFlat.quasiIso_tensorComplex_obj_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/KFlat/TensorPreservesQuasiIso.lean, line 323. The attribute's comment: “for complexes, the K-flat complex as left tensor factor”.
For
KK-flat andga quasi-isomorphism, the total tensor productTot(1_K ⊗ g)is a quasi-isomorphism.
theorem IsKFlat.quasiIso_tensorComplex_obj_map
(K : CochainComplex (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf R)) ℤ)
(hK : IsKFlat R K)
{A B : CochainComplex (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf R)) ℤ}
(g : A ⟶ B) (hg : QuasiIso g) :
QuasiIso (((Stacks.SheafOfModules.Tensor.tensorComplex R).obj K).map g)
Stacks.SheafOfModules.IsKFlat.quasiIso_mapBifunctorMap_id_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/KFlat/TensorPreservesQuasiIso.lean, line 341. The attribute's comment: “for complexes, right tensor factor, mapBifunctorMap spelling”.
The
HomologicalComplex.mapBifunctorMapspelling ofStacks.SheafOfModules.IsKFlat.quasiIso_tensorComplex_map_app.
theorem IsKFlat.quasiIso_mapBifunctorMap_id_right
(K : CochainComplex (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf R)) ℤ)
(hK : IsKFlat R K)
{A B : CochainComplex (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf R)) ℤ}
(f : A ⟶ B) (hf : QuasiIso f) :
QuasiIso (HomologicalComplex.mapBifunctorMap f (𝟙 K)
(Stacks.SheafOfModules.Tensor.sheafTensor R) (ComplexShape.up ℤ))
Stacks.SheafOfModules.IsKFlat.quasiIso_mapBifunctorMap_id_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/KFlat/TensorPreservesQuasiIso.lean, line 354. The attribute's comment: “for complexes, left tensor factor, mapBifunctorMap spelling”.
The
HomologicalComplex.mapBifunctorMapspelling ofStacks.SheafOfModules.IsKFlat.quasiIso_tensorComplex_obj_map.
theorem IsKFlat.quasiIso_mapBifunctorMap_id_left
(K : CochainComplex (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf R)) ℤ)
(hK : IsKFlat R K)
{A B : CochainComplex (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf R)) ℤ}
(g : A ⟶ B) (hg : QuasiIso g) :
QuasiIso (HomologicalComplex.mapBifunctorMap (𝟙 K) g
(Stacks.SheafOfModules.Tensor.sheafTensor R) (ComplexShape.up ℤ))
Stacks.SheafOfModules.KFlatQuasiIso.quasiIso_tensorComplex_of_KFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/KFlat/TensorPreservesQuasiIsoOnASite.lean, line 102.
Total tensor product with a K-flat complex preserves quasi-isomorphisms: if the maps on every cohomology sheaf are isomorphisms, so are those induced by tensoring with
K.
theorem quasiIso_tensorComplex_of_KFlat
(K : CochainComplex (SheafOfModules.{max u v w} (Stacks.SheafOfModules.Tensor.ringSheaf R)) ℤ)
(hK : CochainComplex.KFlatBifunctor.KFlat (Stacks.SheafOfModules.Tensor.sheafTensor R) K)
{F G : CochainComplex (SheafOfModules.{max u v w} (Stacks.SheafOfModules.Tensor.ringSheaf R)) ℤ}
(f : F ⟶ G)
(hf : ∀ n, IsIso (ShortComplex.leftHomologyMap
((HomologicalComplex.shortComplexFunctor _ (ComplexShape.up ℤ) n).map f))) :
∀ n, IsIso (ShortComplex.leftHomologyMap
((HomologicalComplex.shortComplexFunctor _ (ComplexShape.up ℤ) n).map
(((Stacks.SheafOfModules.Tensor.tensorComplex R).map f).app K)))
Tag 0E8K, a lemma
Tag 0E8K in the Stacks Project.
Stacks.DerivedTensor.ExtensionByZero.kFlat_restrictionComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/ExtensionByZeroTensor.lean, line 281.
Stacks Project, Tag 0E8K. Let
(C, O)be a ringed site and letUbe an object ofC. IfKis a K-flat complex ofO-modules, thenK|_Uis a K-flat complex ofO_U-modules.Let
Gbe an acyclic complex ofO_U-modules. Extension by zero is exact (Stacks 03DJ), soj_!Gis acyclic, and the K-flatness ofKthen makesTot(j_!G ⊗_O K)acyclic. That complex isj_!(Tot(G ⊗_{O_U} K|_U))bytensorComplexExtensionIso, and extension by zero reflects exactness (Stacks 0E8G), soTot(G ⊗_{O_U} K|_U)is acyclic as well.
theorem kFlat_restrictionComplex (Q : CochainComplex (Modules X.O) ℤ)
(hQ : Stacks.SheafOfModules.KFlat.KFlat X.O Q) :
Stacks.SheafOfModules.KFlat.KFlat (X.O.over U) ((restrictionComplex X U).obj Q)
Stacks.DerivedTensor.ExtensionByZero.OfEssentiallySmall.kFlat_restrictionComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/ExtensionByZeroTensorOfEssentiallySmall.lean, line 435. The attribute's comment: “for a site essentially u-small, objects in Type c, morphisms and modules in u”.
Stacks Project, Tag 0E8K over a site with large objects. Let
(C, O)be a ringed site whose objects form a type in an arbitrary universecwhile its morphisms, the sections ofOand the sections of its modules lie in one universeu, letCbe essentiallyu-small, and letUbe an object ofC. IfQis a K-flat complex ofO-modules, thenQ|_Uis a K-flat complex ofO|_U-modules.The proof is the source's. Let
Pbe an acyclic complex ofO|_U-modules. Extension by zero is exact (Stacks 03DJ), soj_{U!}Pis acyclic, and the K-flatness ofQthen makesTot(j_{U!}P ⊗_O Q)acyclic. That complex isj_{U!}(Tot(P ⊗_{O|_U} Q|_U))bytensorComplexExtensionIso, and extension by zero reflects exactness (Stacks 0E8G), soTot(P ⊗_{O|_U} Q|_U)is acyclic as well.The attribute records the universe shape. The tag is carried in full by
Stacks.DerivedTensor.ExtensionByZero.kFlat_restrictionComplex, where the objects, the morphisms and the sections lie in a single universe — the faithful reading of the tag's ringed site, which this statement specializes to atc := u; that registration stands and this one does not replace it.
theorem kFlat_restrictionComplex (hQ : Stacks.SheafOfModules.IsKFlat X.O Q) :
Stacks.SheafOfModules.IsKFlat (X.O.over U) ((restrictionComplex X U).obj Q)
Tag 07A2, a lemma
Tag 07A2 in the Stacks Project.
CochainComplex.KFlatMonoidal.KFlat.tensorObj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/KFlat/TensorOfTwoKFlatComplexes.lean, line 97.
If
K^•andL^•are K-flat complexes, then their total tensor productTot(K^• ⊗ L^•)is K-flat.
theorem KFlat.tensorObj {K L : CochainComplex A ℤ} (hK : KFlat K) (hL : KFlat L) :
KFlat (totalComplexTensor K L)
Tag 07A3, a lemma
Tag 07A3 in the Stacks Project.
Stacks.SheafOfModules.kFlat_of_second_third, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/KFlat/DistinguishedTriangles.lean, line 79. The attribute's comment: “first vertex”.
In a distinguished triangle, the first complex is K-flat if the second and third are K-flat.
theorem kFlat_of_second_third
{K₁ K₂ K₃ : CochainComplex
(SheafOfModules.{max u v w} (Stacks.SheafOfModules.Tensor.ringSheaf R)) ℤ}
(f : (HomotopyCategory.quotient _ (ComplexShape.up ℤ)).obj K₁ ⟶
(HomotopyCategory.quotient _ (ComplexShape.up ℤ)).obj K₂)
(g : (HomotopyCategory.quotient _ (ComplexShape.up ℤ)).obj K₂ ⟶
(HomotopyCategory.quotient _ (ComplexShape.up ℤ)).obj K₃)
(h : (HomotopyCategory.quotient _ (ComplexShape.up ℤ)).obj K₃ ⟶
((HomotopyCategory.quotient _ (ComplexShape.up ℤ)).obj K₁)⟦(1 : ℤ)⟧)
(hT : Triangle.mk f g h ∈ distTriang _)
(h₂ : CochainComplex.KFlatBifunctor.KFlat (Stacks.SheafOfModules.Tensor.sheafTensor R) K₂)
(h₃ : CochainComplex.KFlatBifunctor.KFlat (Stacks.SheafOfModules.Tensor.sheafTensor R) K₃) :
CochainComplex.KFlatBifunctor.KFlat (Stacks.SheafOfModules.Tensor.sheafTensor R) K₁
Stacks.SheafOfModules.kFlat_of_first_third, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/KFlat/DistinguishedTriangles.lean, line 97. The attribute's comment: “second vertex”.
In a distinguished triangle, the second complex is K-flat if the first and third are K-flat.
theorem kFlat_of_first_third
{K₁ K₂ K₃ : CochainComplex
(SheafOfModules.{max u v w} (Stacks.SheafOfModules.Tensor.ringSheaf R)) ℤ}
(f : (HomotopyCategory.quotient _ (ComplexShape.up ℤ)).obj K₁ ⟶
(HomotopyCategory.quotient _ (ComplexShape.up ℤ)).obj K₂)
(g : (HomotopyCategory.quotient _ (ComplexShape.up ℤ)).obj K₂ ⟶
(HomotopyCategory.quotient _ (ComplexShape.up ℤ)).obj K₃)
(h : (HomotopyCategory.quotient _ (ComplexShape.up ℤ)).obj K₃ ⟶
((HomotopyCategory.quotient _ (ComplexShape.up ℤ)).obj K₁)⟦(1 : ℤ)⟧)
(hT : Triangle.mk f g h ∈ distTriang _)
(h₁ : CochainComplex.KFlatBifunctor.KFlat (Stacks.SheafOfModules.Tensor.sheafTensor R) K₁)
(h₃ : CochainComplex.KFlatBifunctor.KFlat (Stacks.SheafOfModules.Tensor.sheafTensor R) K₃) :
CochainComplex.KFlatBifunctor.KFlat (Stacks.SheafOfModules.Tensor.sheafTensor R) K₂
Stacks.SheafOfModules.kFlat_of_first_second, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/KFlat/DistinguishedTriangles.lean, line 115. The attribute's comment: “third vertex”.
In a distinguished triangle, the third complex is K-flat if the first and second are K-flat.
theorem kFlat_of_first_second
{K₁ K₂ K₃ : CochainComplex
(SheafOfModules.{max u v w} (Stacks.SheafOfModules.Tensor.ringSheaf R)) ℤ}
(f : (HomotopyCategory.quotient _ (ComplexShape.up ℤ)).obj K₁ ⟶
(HomotopyCategory.quotient _ (ComplexShape.up ℤ)).obj K₂)
(g : (HomotopyCategory.quotient _ (ComplexShape.up ℤ)).obj K₂ ⟶
(HomotopyCategory.quotient _ (ComplexShape.up ℤ)).obj K₃)
(h : (HomotopyCategory.quotient _ (ComplexShape.up ℤ)).obj K₃ ⟶
((HomotopyCategory.quotient _ (ComplexShape.up ℤ)).obj K₁)⟦(1 : ℤ)⟧)
(hT : Triangle.mk f g h ∈ distTriang _)
(h₁ : CochainComplex.KFlatBifunctor.KFlat (Stacks.SheafOfModules.Tensor.sheafTensor R) K₁)
(h₂ : CochainComplex.KFlatBifunctor.KFlat (Stacks.SheafOfModules.Tensor.sheafTensor R) K₂) :
CochainComplex.KFlatBifunctor.KFlat (Stacks.SheafOfModules.Tensor.sheafTensor R) K₃
Stacks.SheafOfModules.kFlatObjects_isTriangulated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/KFlat/TriangulatedSubcategory.lean, line 185. The attribute's comment: “two out of three in a distinguished triangle”.
The K-flat complexes form a pre-triangulated subcategory of the homotopy category: the zero complex is K-flat, K-flatness is stable under shifts, and in a distinguished triangle two K-flat vertices force the third. The last assertion is Stacks 07A3.
theorem kFlatObjects_isTriangulated : (kFlatObjects.{u, v, w} R).IsTriangulated
Tag 0G7B, a lemma
Tag 0G7B in the Stacks Project.
Stacks.SheafOfModules.isKFlat_two_out_of_three, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/KFlat/TwoOutOfThree.lean, line 337.
Stacks 0G7B. In a short exact sequence of complexes of sheaves of modules on a ringed site whose third term has flat terms, if two out of the three complexes are K-flat, so is the third.
theorem isKFlat_two_out_of_three
(h : (IsKFlat X.O S.X₁ ∧ IsKFlat X.O S.X₂) ∨ (IsKFlat X.O S.X₁ ∧ IsKFlat X.O S.X₃) ∨
(IsKFlat X.O S.X₂ ∧ IsKFlat X.O S.X₃)) :
IsKFlat X.O S.X₁ ∧ IsKFlat X.O S.X₂ ∧ IsKFlat X.O S.X₃
Stacks.SheafOfModules.KFlatTwoOutOfThree.kFlat_left_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/KFlat/TwoOutOfThreeShortExact.lean, line 343. The attribute's comment: “left complex”.
Stacks 0G7B, left complex. In a short exact sequence of complexes of
O-modules whose right complex has flat terms, K-flatness of the middle and of the right complex implies K-flatness of the left complex.
theorem kFlat_left_of_shortExact (hS : S.ShortExact)
(hflat : ∀ i : ℤ, AlgebraicGeometry.SheafOfModules.IsFlat.{v, u, w, w} (O := R) (S.X₃.X i))
(h₂ : Stacks.SheafOfModules.KFlat.KFlat R S.X₂) (h₃ : Stacks.SheafOfModules.KFlat.KFlat R S.X₃)
:
Stacks.SheafOfModules.KFlat.KFlat R S.X₁
Stacks.SheafOfModules.KFlatTwoOutOfThree.kFlat_middle_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/KFlat/TwoOutOfThreeShortExact.lean, line 354. The attribute's comment: “middle complex”.
Stacks 0G7B, middle complex. In a short exact sequence of complexes of
O-modules whose right complex has flat terms, K-flatness of the two outer complexes implies K-flatness of the middle complex.
theorem kFlat_middle_of_shortExact (hS : S.ShortExact)
(hflat : ∀ i : ℤ, AlgebraicGeometry.SheafOfModules.IsFlat.{v, u, w, w} (O := R) (S.X₃.X i))
(h₁ : Stacks.SheafOfModules.KFlat.KFlat R S.X₁) (h₃ : Stacks.SheafOfModules.KFlat.KFlat R S.X₃)
:
Stacks.SheafOfModules.KFlat.KFlat R S.X₂
Stacks.SheafOfModules.KFlatTwoOutOfThree.kFlat_right_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/KFlat/TwoOutOfThreeShortExact.lean, line 365. The attribute's comment: “right complex”.
Stacks 0G7B, right complex. In a short exact sequence of complexes of
O-modules whose right complex has flat terms, K-flatness of the left and of the middle complex implies K-flatness of the right complex.
theorem kFlat_right_of_shortExact (hS : S.ShortExact)
(hflat : ∀ i : ℤ, AlgebraicGeometry.SheafOfModules.IsFlat.{v, u, w, w} (O := R) (S.X₃.X i))
(h₁ : Stacks.SheafOfModules.KFlat.KFlat R S.X₁) (h₂ : Stacks.SheafOfModules.KFlat.KFlat R S.X₂)
:
Stacks.SheafOfModules.KFlat.KFlat R S.X₃
Tag 06YQ, a lemma
Tag 06YQ in the Stacks Project.
Stacks.SheafOfModules.kFlat_of_boundedAbove_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/KFlat/BoundedAboveFlatComplexes.lean, line 328.
Stacks 06YQ. A bounded above cochain complex of flat sheaves of modules is K-flat.
theorem kFlat_of_boundedAbove_of_flat
(K : CochainComplex (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf R)) ℤ)
(hbound : ∃ n : ℤ, K.IsStrictlyLE n)
(hflat : ∀ i : ℤ, AlgebraicGeometry.SheafOfModules.IsFlat.{v, u, w, w}
(O := R) (K.X i)) :
IsKFlat R K
Stacks.Cohomology.LocallyBoundedKFlat.kFlat_of_isLocallyBounded_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/KFlat/LocallyBoundedIsKFlat.lean, line 156. The attribute's comment: “with the boundedness hypothesis localized: a complex of flat O_W-modules which is merely LOCALLY bounded — bounded on each member of some open cover of W, which a complex with no global bound above can be — is K-flat. The source states it for a complex bounded above, which is this statement at the one-member cover W = W”.
A locally bounded complex of flat
𝒪_W-modules is K-flat. This is [Stacks, Tag 06YQ] with its boundedness hypothesis localized: the complex is only assumed bounded on each member of some open cover ofW, which is strictly weaker than being bounded above.For an acyclic
L^•, the total complexTot(L^• ⊗_{𝒪_W} ℱ^•)has to be acyclic, and byacyclic_of_acyclic_restrictit is enough that each of its restrictions be. On an openVon whichℱ^•is bounded,restrictTotalTensorIsoidentifies that restriction withTot(L^•|_V ⊗_{𝒪_V} ℱ^•|_V); thereℱ^•|_Vis bounded above with flat terms (Stacks.Cohomology.TorAmplitude.isFlat_restrictModules, [Stacks, Tag 0E8J] on an open subspace) hence K-flat by [Stacks, Tag 06YQ], andL^•|_Vis acyclic because restriction is exact.
theorem kFlat_of_isLocallyBounded_of_flat
(F : CochainComplex (RingedSpace.KFlatDerivedPullback.Modules W) ℤ)
(hF : Stacks.SheafOfModules.OnSpace.IsLocallyBounded W F)
(hflat : ∀ i : ℤ, AlgebraicGeometry.SheafOfModules.IsFlat.{u, u, u, u}
(O := W.sheaf) (F.X i)) :
KFlat W F
Tag 06YR, a lemma
Tag 06YR in the Stacks Project.
colim_of_system_KFlat_isKFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/KFlat/FilteredColimitOfKFlatComplexes.lean, line 449.
Statement 1 (Stacks Lemma 21.17.9 / Tag 06YR).
Let
(C, O)be a ringed site and letD : K_1 → K_2 → K_3 → …be a system of complexes ofO-modules which are K-flat for the tensor product⊗_Oof Definition 1. Then the termwise colimitcolim_i K_iis K-flat.The two structural facts of the proof are the two hypotheses of
colim_of_system_KFlat_isKFlat_of_bifunctor, and both are theorems here:⊗_Ocommutes with colimits in each variable becauseMod(O)is monoidal closed, soℱ ⊗_O -is a left adjoint (SheafOfModules.preservesColimitsOfSize_sheafTensor_obj); and colimits overℕare exact inMod(O)by AB5 (SheafOfModules.DifferentialGradedModule.hasExactColimitsOfShape_nat), so a colimit of acyclic complexes is acyclic (CochainComplex.KFlat.acyclic_colimit).
theorem colim_of_system_KFlat_isKFlat (D : SystemOfComplexes (ringSheaf O))
(hD : ∀ i, IsKFlat (ringSheaf O) (sheafTensor O) (D.obj i)) :
IsKFlat (ringSheaf O) (sheafTensor O) (systemColimit (ringSheaf O) D)
Tag 077J, a lemma
Tag 077J in the Stacks Project.
Stacks.SheafOfModules.exists_resolutionByDirectSumsExtensionsByZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/ResolutionByExtensionsByZero.lean, line 358.
A complex of modules on a ringed site admits a compatible resolution by direct sums of extensions by zero, whose colimit is quasi-isomorphic to the complex.
theorem exists_resolutionByDirectSumsExtensionsByZero
(G : CochainComplex (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O))) ℤ) :
Nonempty (ResolutionByDirectSumsExtensionsByZero X G)
Tag 06YS, a lemma
Tag 06YS in the Stacks Project.
Stacks.SheafOfModules.exists_kFlat_quasiIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/KFlat/Resolution.lean, line 94. The attribute's comment: “existence of a K-flat resolution”.
Every cochain complex of sheaves of modules on a ringed site receives a quasi-isomorphism from a K-flat complex. This is the existence assertion of Stacks 06YS.
theorem exists_kFlat_quasiIso
(G : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ) :
∃ (P : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ) (p :
P ⟶ G),
IsKFlat X.O P ∧ QuasiIso p
Stacks.SheafOfModules.KFlatResolution.exists_kFlatResolution_ofSize, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/KFlat/ResolutionsOfSize.lean, line 299. The attribute's comment: “with the object and morphism universes of the site independent of the module universe, so that it applies at a site whose objects lie above the module universe”.
Stacks Tag 06YS with the module universe free of the site. Every complex of
O-modules on a ringed site admits a termwise surjective quasi-isomorphism from a K-flat complex whose terms are flat: the colimit of the ladder of Stacks 077J, resolved by flat modules.The object universe
u, the morphism universevand the module universeware independent, so the statement applies at a site whose objects lie above the module universe, such as the small étale site of an algebraic space, aRingedTopos.{u, u + 1, u}.
theorem exists_kFlatResolution_ofSize (G : CochainComplex (ModOfSize.{v, u, w} R) ℤ) :
∃ (K : CochainComplex (ModOfSize.{v, u, w} R) ℤ) (f : K ⟶ G),
CochainComplex.KFlatBifunctor.KFlat
(Stacks.SheafOfModules.Tensor.sheafTensor.{u, v, w, w, w} R) K ∧
(∀ i : ℤ, AlgebraicGeometry.SheafOfModules.IsFlat.{v, u, w, w} (O := R)
(K.X i)) ∧
QuasiIso f ∧ (∀ i : ℤ, Epi (f.f i))
Stacks.SheafOfModules.KFlatResolution.exists_kFlatResolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/KFlat/ResolutionsOnARingedSite.lean, line 238.
Stacks Tag 06YS. Every complex of
O-modules on a ringed site admits a termwise surjective quasi-isomorphism from a K-flat complex whose terms are flat: the colimit of the ladder of 077J.
theorem exists_kFlatResolution
(G : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf.{u, u, u} R)) ℤ)
:
∃ (K : CochainComplex
(SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf.{u, u, u} R)) ℤ) (f : K ⟶ G),
CochainComplex.KFlatBifunctor.KFlat
(Stacks.SheafOfModules.Tensor.sheafTensor.{u, u, u, u, u} R) K ∧
(∀ i : ℤ, AlgebraicGeometry.SheafOfModules.IsFlat.{u, u, u, u} (O := R) (K.X i)) ∧
QuasiIso f ∧ (∀ i : ℤ, Epi (f.f i))
Stacks.SheafOfModules.exists_isKFlat_isFlat_quasiIso_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/KFlat/ResolutionWithFlatTermsSurjective.lean, line 171.
Stacks 06YS. Every cochain complex
Gof modules on a ringed site receives a termwise surjective quasi-isomorphism from a K-flat complex whose terms are flat.The complex is the colimit of the ladder of [Stacks, Tag 077J]. It is K-flat because each rung is bounded above with flat terms, hence K-flat by [Stacks, Tag 06YQ], and a sequential colimit of K-flat complexes is K-flat by [Stacks, Tag 06YE]. Its terms are flat because they are filtered colimits of the flat terms of the rungs ([Stacks, Tag 05NG]), and the comparison is termwise surjective because each rung is termwise surjective onto a truncation of
G.
public theorem exists_isKFlat_isFlat_quasiIso_epi
(G : CochainComplex
(_root_.SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O))) ℤ) :
∃ (K : CochainComplex
(_root_.SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O))) ℤ) (s : K ⟶ G),
IsKFlat X.O K ∧
(∀ i : ℤ, AlgebraicGeometry.SheafOfModules.IsFlat.{u, u, u, u} (O := X.O) (K.X i)) ∧
QuasiIso s ∧ ∀ i : ℤ, Epi (s.f i)
Stacks.Cohomology.kFlatResolution_kFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/TorsorsAndColimits/KFlatResolution.lean, line 174. The attribute's comment: “K-flatness of the chosen resolution”.
The chosen resolution is K-flat.
theorem kFlatResolution_kFlat
(G : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ) :
Stacks.SheafOfModules.IsKFlat X.O (kFlatResolution X G)
Stacks.Cohomology.kFlatResolution_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/TorsorsAndColimits/KFlatResolution.lean, line 181. The attribute's comment: “flatness of the terms of the chosen resolution”.
Every term of the chosen resolution is flat.
theorem kFlatResolution_flat
(G : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ)
(i : ℤ) :
AlgebraicGeometry.SheafOfModules.IsFlat.{u, u, u, u} (O := X.O)
((kFlatResolution X G).X i)
Stacks.Cohomology.kFlatResolutionHom_quasiIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/TorsorsAndColimits/KFlatResolution.lean, line 190. The attribute's comment: “quasi-isomorphism of the augmentation”.
The augmentation from the chosen resolution is a quasi-isomorphism.
theorem kFlatResolutionHom_quasiIso
(G : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ) :
QuasiIso (kFlatResolutionHom X G)
Stacks.Cohomology.kFlatResolutionHom_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/TorsorsAndColimits/KFlatResolution.lean, line 197. The attribute's comment: “termwise surjectivity of the augmentation”.
The augmentation from the chosen resolution is epimorphic in each degree.
theorem kFlatResolutionHom_epi
(G : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ)
(i : ℤ) :
Epi ((kFlatResolutionHom X G).f i)
Tag 06YT, a lemma
Tag 06YT in the Stacks Project.
Stacks.SheafOfModules.quasiIso_mapBifunctorMap_id_of_kFlat_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/KFlat/ResolutionIndependence.lean, line 87. The attribute's comment: “the quasi-isomorphism in the right tensor factor”.
A quasi-isomorphism
αof K-flat complexes induces a quasi-isomorphismTot(F ⊗ α)for every complexF. This is Stacks 06YT.
theorem quasiIso_mapBifunctorMap_id_of_kFlat_right
{P Q : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ}
(α : P ⟶ Q) (hα : QuasiIso α) (hP : IsKFlat X.O P) (hQ : IsKFlat X.O Q)
(F : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ) :
QuasiIso (HomologicalComplex.mapBifunctorMap (𝟙 F) α (Stacks.SheafOfModules.Tensor.sheafTensor
X.O)
(ComplexShape.up ℤ))
Stacks.SheafOfModules.quasiIso_mapBifunctorMap_id_of_kFlat_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/KFlat/ResolutionIndependence.lean, line 107. The attribute's comment: “the quasi-isomorphism in the left tensor factor”.
A quasi-isomorphism
αof K-flat complexes induces a quasi-isomorphismTot(α ⊗ F)for every complexF. This is the mirror image of Stacks 06YT.
theorem quasiIso_mapBifunctorMap_id_of_kFlat_left
{P Q : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ}
(α : P ⟶ Q) (hα : QuasiIso α) (hP : IsKFlat X.O P) (hQ : IsKFlat X.O Q)
(F : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ) :
QuasiIso (HomologicalComplex.mapBifunctorMap α (𝟙 F) (Stacks.SheafOfModules.Tensor.sheafTensor
X.O)
(ComplexShape.up ℤ))
Stacks.SheafOfModules.quasiIso_tensorComplex_obj_map_of_kFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/KFlat/ResolutionIndependence.lean, line 130. The attribute's comment: “right tensor factor, tensorComplex spelling”.
Stacks 06YT in the
Stacks.SheafOfModules.Tensor.tensorComplexspelling: the quasi-isomorphismαof K-flat complexes sits in the right tensor slot. The square whose cancellation gives the result is the naturality square oftensorComplex.map ratα, for a K-flat resolutionr : M ⟶ F.
theorem quasiIso_tensorComplex_obj_map_of_kFlat
{P Q : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ}
(α : P ⟶ Q) (hα : QuasiIso α) (hP : IsKFlat X.O P) (hQ : IsKFlat X.O Q)
(F : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ) :
QuasiIso (((Stacks.SheafOfModules.Tensor.tensorComplex X.O).obj F).map α)
Stacks.SheafOfModules.quasiIso_tensorComplex_map_app_of_kFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/KFlat/ResolutionIndependence.lean, line 145. The attribute's comment: “left tensor factor, tensorComplex spelling”.
Stacks 06YT in the
Stacks.SheafOfModules.Tensor.tensorComplexspelling, mirror image: the quasi-isomorphismαof K-flat complexes sits in the left tensor slot.
theorem quasiIso_tensorComplex_map_app_of_kFlat
{P Q : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ}
(α : P ⟶ Q) (hα : QuasiIso α) (hP : IsKFlat X.O P) (hQ : IsKFlat X.O Q)
(F : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ) :
QuasiIso (((Stacks.SheafOfModules.Tensor.tensorComplex X.O).map α).app F)
Tag 06YU, a definition
Tag 06YU in the Stacks Project.
Stacks.DerivedTensor.RingedSite.preservesColimitsOfShape_discrete_derivedTensorProductFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/Coproducts.lean, line 203. The attribute's comment: “the derived tensor product commutes with arbitrary direct sums in the second variable”.
The derived tensor product of sheaves of modules on a ringed site commutes with arbitrary direct sums, in the second variable: for an arbitrary
AinD(Mod(𝒪))the functorA ⊗^𝐋_𝒪 -preserves direct sums indexed by any type of the module universe.
theorem preservesColimitsOfShape_discrete_derivedTensorProductFunctor
(I : Type u)
(A : DerivedCategory (Modules R)) :
PreservesColimitsOfShape (Discrete I) ((derivedTensorProductFunctor R).obj A)
Stacks.SheafOfModules.exists_derivedTensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/Existence.lean, line 122. The attribute's comment: “existence, for a site whose objects form a type in an arbitrary universe while its morphisms, structure sheaf and modules lie in one universe”.
Stacks 06YU. The derived tensor product of sheaves of modules on a ringed site exists, with its canonical natural map to the ordinary total tensor product, its one-sided K-flat comparisons, and exactness in both variables.
The objects of the site form a type in an arbitrary universe
c, while its morphisms, the sections of its structure sheaf and the sections of its modules lie in one universeu; the derived category's hom universedis independent of both. That is the configuration of a small étale site, whose objects sit one universe above its morphisms.
theorem exists_derivedTensorProduct :
Nonempty (DerivedTensorProduct.{c, u, u, d} X)
Stacks.SheafOfModules.canonicalDerivedTensorProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/Existence.lean, line 135. The attribute's comment: “the derived tensor product, at a site whose objects form a type in an arbitrary universe while its morphisms, structure sheaf and modules lie in one universe”.
The canonical derived tensor product of sheaves of modules on a ringed site, with its natural map to the ordinary total tensor product, K-flat comparisons, and exactness in both variables. The objects of the site live in a universe of their own.
It is the construction
Stacks.SheafOfModules.derivedTensorProductOfExact, made opaque withirreducible_def;canonicalDerivedTensorProduct_defis the defining equation.
irreducible_def canonicalDerivedTensorProduct : DerivedTensorProduct.{c, u, u, d} X
Stacks.DerivedTensor.RingedSite.exists_derivedTensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/ExistenceOnARingedSite.lean, line 136. The attribute's comment: “existence and characterization”. References: SGA 4½ Etat 0 (6.2), “existence of ⊗^L”; SGA 4 XVII (4.1.7), “(i)”.
The derived tensor product of sheaves of modules on a ringed site exists, with its canonical natural map to the ordinary total tensor product, its one-sided K-flat comparisons, and exactness in both variables.
theorem exists_derivedTensorProduct : Nonempty (DerivedTensorProduct R)
Stacks.DerivedTensor.RingedSite.canonicalDerivedTensorProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/ExistenceOnARingedSite.lean, line 147. The attribute's comment: “the derived tensor product”. References: SGA 4½ Etat 0 (6.2), “X ⊗^L Y on a site”; SGA 4 XVII (4.1.7), “(i)”.
The canonical derived tensor product of sheaves of modules on a ringed site, with its natural map to the ordinary total tensor product, its K-flat comparisons, and exactness in both variables. It is the construction
derivedTensorProductConstruction R, made opaque withirreducible_defso that definitional unfolding does not reach the construction;canonicalDerivedTensorProduct_defis the defining equation.
irreducible_def canonicalDerivedTensorProduct : DerivedTensorProduct R
Stacks.DerivedTensor.derivedTensorSheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/OnARingedSite.lean, line 113. The attribute's comment: “the derived tensor product with a K-flat complex”. References: SGA 4½ Etat 0 (6.2), “⊗^L via K-flat”.
The derived tensor product
- ⊗_O^{L} G : D(O) ⥤ D(O)with a K-flat complexGofO-modules: the functor induced on derived categories by the total tensor complexTot(- ⊗_O G).
abbrev derivedTensorSheaf : DerivedCategory (SheafMod R) ⥤ DerivedCategory (SheafMod R)
Stacks.DerivedTensor.derivedTensorSheafQIso, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/OnARingedSite.lean, line 119. The attribute's comment: “computed by the total tensor complex”.
- ⊗_O^{L} Gis the functor described by the total tensor complex: on the image of a complexKofO-modules inD(O)it isTot(K ⊗_O G), naturally inK.
abbrev derivedTensorSheafQIso :
DerivedCategory.Q ⋙ derivedTensorSheaf R G ≅
totRight (Stacks.SheafOfModules.Tensor.sheafTensor.{_, _, _, max u v w, max u v w} R) G ⋙
DerivedCategory.Q
Stacks.SheafOfModules.DerivedMonoidal.canonicalTensor_commShift₂Int, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Monoidal/CanonicalDerivedTensorCommShiftTwo.lean, line 82. The attribute's comment: “compatibility with the shifts in both variables”.
The canonical derived tensor product of [Stacks, Tag 06YU] commutes with the shifts in both variables, with Mathlib's sign
(-1) ^ (p * q): the datum ofCochainComplex.KFlatBifunctor.derivedBifunctor, transported alongStacks.SheafOfModules.DerivedMonoidal.canonicalTensorIso.It is a
def, not an instance: the instance onStacks.DerivedTensor.RingedSite.derivedTensorProductFunctor Ris the structure fieldStacks.DerivedTensor.RingedSite.DerivedTensorProduct.commShift₂, whichcanonicalDerivedTensorProduct_commShift₂_eqidentifies with this datum.
def canonicalTensor_commShift₂Int :
(Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor R).CommShift₂Int
Stacks.DerivedTensor.isTriangulated_derivedTensor, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedTensor/KFlatDescent.lean, line 199. The attribute's comment: “exact functor of triangulated categories”.
- ⊗ Gis an exact functor of triangulated categories. For sheaves of modules on a ringed site this is the caseF := Stacks.SheafOfModules.Tensor.sheafTensor R.
instance isTriangulated_derivedTensor [IsKFlat F G] : (derivedTensor F G).IsTriangulated
Tag 08FF, a definition
Tag 08FF in the Stacks Project.
Stacks.DerivedTensor.RingedSite.tor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/Tor.lean, line 126. References: SGA 4 XVII (4.1.8), “modules, not complexes”.
The Tor's of two
O-modules on a ringed site. TheO-moduleTor_p^O(F, G) = H^{-p}(F ⊗_O^{L} G).
def tor (p : ℤ) (F G : Modules R) : Modules R
Tag 08FG, a lemma
Tag 08FG in the Stacks Project.
Stacks.DerivedTensor.RingedSite.isFlat_iff_isZero_tor_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/Tor.lean, line 386.
Stacks Project, Tag 08FG. Let
(C, O)be a ringed site and letFbe anO-module. ThenFis a flatO-module if and only ifTor_1^O(F, G) = 0for everyO-moduleG.
theorem isFlat_iff_isZero_tor_one (F : Modules R) :
AlgebraicGeometry.SheafOfModules.IsFlat.{u, u, u, u} (O := R) F ↔
∀ G : Modules R, IsZero (tor R 1 F G)
Tag 0G7C, a lemma
Tag 0G7C in the Stacks Project.
Stacks.SheafOfModules.KFlatCycles.isFlat_kernel_d_of_kFlat_of_acyclic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/KFlat/CyclesOfAnAcyclicKFlatComplex.lean, line 332.
Stacks Tag 0G7C. Let
Kbe a K-flat, acyclic complex ofO-modules on a ringed site whose terms are flat. Then the kernel ofd^n : K^n ⟶ K^{n + 1}is a flatO-module.The hypothesis is K-flatness in the sense of Tag 06YN (
Stacks.SheafOfModules.KFlat.KFlat, which isIff.rflto the bifunctor-relative predicate written here).
theorem isFlat_kernel_d_of_kFlat_of_acyclic
(K : CochainComplex (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf.{u, v, w} R)) ℤ)
(hK : CochainComplex.KFlatBifunctor.KFlat
(Stacks.SheafOfModules.Tensor.sheafTensor.{u, v, w, w, w} R) K)
(hacyclic : K.Acyclic)
(hflat : ∀ i : ℤ, AlgebraicGeometry.SheafOfModules.IsFlat.{v, u, w, w} (O := R) (K.X i))
(n : ℤ) :
AlgebraicGeometry.SheafOfModules.IsFlat.{v, u, w, w} (O := R)
(kernel (K.d n (n + 1)))
Tag 0G7D, a lemma
Tag 0G7D in the Stacks Project.
Stacks.SheafOfModules.exists_isKFlat_factorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/KFlat/Factorization.lean, line 117. The attribute's comment: “the K-flat factorization”.
Tag 0G6V. A map
a : K^• ⟶ L^•of complexes ofO-modules withK^•K-flat factors, up to homotopy, through a K-flat complexN^•which maps toL^•by a quasi-isomorphism.
theorem exists_isKFlat_factorization
{K L : CochainComplex
(SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf.{u, u, u} X.O)) ℤ}
(a : K ⟶ L) (hK : IsKFlat X.O K) :
∃ (N : CochainComplex
(SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf.{u, u, u} X.O)) ℤ)
(b : K ⟶ N) (c : N ⟶ L),
IsKFlat X.O N ∧ QuasiIso c ∧ Nonempty (Homotopy a (b ≫ c))
Stacks.SheafOfModules.exists_isKFlat_isFlat_factorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/KFlat/Factorization.lean, line 132. The attribute's comment: “the factorization with flat terms”.
Tag 0G6V, second half. If in addition the terms of
K^•are flatO-modules, then the intermediate complex of the factorization can be chosen with flat terms as well.
theorem exists_isKFlat_isFlat_factorization
{K L : CochainComplex
(SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf.{u, u, u} X.O)) ℤ}
(a : K ⟶ L) (hK : IsKFlat X.O K)
(hKflat : ∀ i : ℤ,
AlgebraicGeometry.SheafOfModules.IsFlat.{u, u, u, u} (O := X.O) (K.X i)) :
∃ (N : CochainComplex
(SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf.{u, u, u} X.O)) ℤ)
(b : K ⟶ N) (c : N ⟶ L),
IsKFlat X.O N ∧
(∀ i : ℤ,
AlgebraicGeometry.SheafOfModules.IsFlat.{u, u, u, u} (O := X.O) (N.X i)) ∧
QuasiIso c ∧ Nonempty (Homotopy a (b ≫ c))
Sources
Section21.18 Derived pullback#
Section 21.18 of the Stacks Project, Tag 06YV. 8 tags here are carried by 39 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0G7E, a lemma
Tag 0G7E in the Stacks Project.
CategoryTheory.SimplicialSiteSituation.isFlat_componentModulesRestrictionComplex_X, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/ComponentTensorComplex.lean, line 195. The attribute's comment: “the flat-terms clause, for restriction to a simplicial component”.
The flat-terms clause of Stacks 0G7E at
g_n. The restriction to a component of a complex ofO-modules with flat terms has flat terms.
theorem isFlat_componentModulesRestrictionComplex_X
(K : CochainComplex (S.totalRingedTopos O).Modules ℤ)
(hflatK : ∀ i : ℤ, AlgebraicGeometry.SheafOfModules.IsFlat.{u, u, u, u}
(O := (S.totalRingedTopos O).O) (K.X i)) (i : ℤ) :
AlgebraicGeometry.SheafOfModules.IsFlat.{u, u, u, u}
(O := (S.componentRingedTopos O n).O)
(((S.componentModulesRestrictionComplex O n).obj K).X i)
CategoryTheory.SimplicialSiteSituation.kFlat_componentModulesRestrictionComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/ComponentTensorComplex.lean, line 210. The attribute's comment: “the K-flatness clause, for restriction to a simplicial component”.
The K-flatness clause of Stacks 0G7E at
g_n. The restriction to a component of a K-flat complex ofO-modules with flat terms is K-flat.
theorem kFlat_componentModulesRestrictionComplex
(K : CochainComplex (S.totalRingedTopos O).Modules ℤ)
(hK : Stacks.SheafOfModules.KFlat.KFlat (S.totalRingedTopos O).O K)
(hflatK : ∀ i : ℤ, AlgebraicGeometry.SheafOfModules.IsFlat.{u, u, u, u}
(O := (S.totalRingedTopos O).O) (K.X i)) :
Stacks.SheafOfModules.KFlat.KFlat (S.componentRingedTopos O n).O
((S.componentModulesRestrictionComplex O n).obj K)
Stacks.Sheaves.RingedToposModules.pullbackModules_preservesZeroMorphisms, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/DegreewisePullbackOfComplexes.lean, line 60. The attribute's comment: “degreewise pullback”.
Pullback of sheaves of modules along a morphism of ringed topoi preserves zero morphisms: it is a left adjoint by Stacks 03D7, and a left adjoint between categories with zero morphisms carries zero morphisms to zero morphisms. This is what lets
f^*be applied degreewise to a complex of modules, as in Stacks 0G7E.
instance pullbackModules_preservesZeroMorphisms (f : RingedToposHom X Y) :
(f.pullbackModules).PreservesZeroMorphisms
Stacks.Sheaves.DerivedPullback.KFlatPullback.pullbackTopos_preservesZeroMorphisms, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/KFlatPullbackAlongRingedTopoi.lean, line 185. The attribute's comment: “degreewise pullback”.
Pullback of sheaves of modules preserves zero morphisms, being additive. This is what makes the degreewise pullback functor on complexes available.
instance pullbackTopos_preservesZeroMorphisms
(f : AlgebraicGeometry.RingedToposSiteHom X Y) :
(show SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O) ⥤
SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O) from
f.pullbackTopos).PreservesZeroMorphisms
Stacks.Sheaves.DerivedPullback.KFlatPullbackOfToposHom.isKFlat_pullbackMapHomotopy, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/KFlatPullbackOfToposHom.lean, line 307. The attribute's comment: “K-flat with flat terms is preserved, for an arbitrary morphism of ringed topoi”.
Stacks 0G7E for an arbitrary morphism of ringed topoi, on the homotopy category. Degreewise pullback along
fcarries the class of K-flat complexes ofO-modules with flat terms into the same class forO'.Nothing happens on passage to the homotopy category: the underlying complex of
K(f^*)Kisf^*of the underlying complex ofK. The K-flatness clause iskFlat_pullbackComplexand the flat-terms clause isisFlat_pullbackComplex_X, i.e. Stacks 05VD alone.
theorem isKFlat_pullbackMapHomotopy (f : RingedToposHom X Y)
(K : HomotopyCategory (SheafOfModules.{w'} (SheafOfModules.Tensor.ringSheaf Y.O))
(ComplexShape.up ℤ))
(hK : Stacks.Cohomology.DerivedPullbackPushforwardAdjunction.IsKFlat (Y := Y) K) :
Stacks.Cohomology.DerivedPullbackPushforwardAdjunction.IsKFlat (Y := X)
((Stacks.Cohomology.DerivedPushforward.pullbackMapHomotopy f).obj K)
Tag 06YY, a lemma
Tag 06YY in the Stacks Project.
Stacks.Cohomology.DerivedPullbackOnRingedTopoi.derivedPullbackCommShift, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/DerivedPullbackAsATriangulatedFunctor.lean, line 97. The attribute's comment: “compatibility with shifts, for a morphism of ringed topoi presented by a morphism of the underlying sites, at RingedTopos.{u, u, u}”.
Tag 06YY, compatibility with shifts.
Lf^*commutes with the shift functors of the two derived categories. Together withderivedPullback_isTriangulated_of_isMorphismOfSitesthis is the assertion thatLf^*is exact as a functor of triangulated categories.This is
Stacks.Sheaves.RingedToposDerivedPullback.derivedPullback_commShiftwith its instance binder discharged; that instance never needed the exactness clause, only the existence of the derived functor.
def derivedPullbackCommShift :
haveI := hasLeftDerivedFunctor_pullbackOnHomotopy f hmos
(derivedPullback f).CommShift ℤ
Stacks.Cohomology.DerivedPullbackOnRingedTopoi.derivedPullback_isTriangulated_of_isMorphismOfSites, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/DerivedPullbackAsATriangulatedFunctor.lean, line 112. The attribute's comment: “exactness, for a morphism of ringed topoi presented by a morphism of the underlying sites, at RingedTopos.{u, u, u}”.
Tag 06YY, exactness.
Lf^*is an exact functor of triangulated categories: it carries a distinguished triangle ofD(O')to a distinguished triangle ofD(O).This is
Stacks.Sheaves.RingedToposDerivedPullback.derivedPullback_isTriangulatedwith both of its inputs discharged — the exactness clause bypullbackInvertsQuasiIso_isKFlatand the instance binder byhasLeftDerivedFunctor_pullbackOnHomotopy.
theorem derivedPullback_isTriangulated_of_isMorphismOfSites :
haveI := hasLeftDerivedFunctor_pullbackOnHomotopy f hmos
(derivedPullback f).IsTriangulated
Stacks.Cohomology.DerivedPullbackOnRingedTopoi.derivedPullbackComparison_isIso_of_kFlat_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/DerivedPullbackAsATriangulatedFunctor.lean, line 130. The attribute's comment: “computation on K-flat complexes with flat terms, for a morphism of ringed topoi presented by a morphism of the underlying sites, at RingedTopos.{u, u, u}”.
Tag 06YY, the computation
Lf^* K^• = f^* K^•. The canonical comparisonLf^* K^• ⟶ f^* K^•is invertible at a K-flat complexK^•ofO'-modules with flat terms: the derived pullback of such a complex is computed by degreewise pullback.This is
Stacks.Sheaves.RingedToposDerivedPullback.isIso_derivedPullbackComparison_app_of_kFlat_of_flatwith both of its inputs discharged. Both hypotheses onK^•are the source's, and both are used: they are the two clauses of the resolving classStacks.Cohomology.DerivedPullbackPushforwardAdjunction.IsKFlat.
theorem derivedPullbackComparison_isIso_of_kFlat_of_flat
(K : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) ℤ)
(hK : CochainComplex.KFlatBifunctor.KFlat
(Stacks.SheafOfModules.Tensor.sheafTensor.{u, u, u, u, u} Y.O) K)
(hflat : ∀ i : ℤ, SheafOfModules.IsFlat.{u, u, u, u} (O := Y.O) (K.X i)) :
haveI := hasLeftDerivedFunctor_pullbackOnHomotopy f hmos
IsIso ((derivedPullbackComparison f).app
((HomotopyCategory.quotient _ (ComplexShape.up ℤ)).obj K))
Stacks.Cohomology.DerivedPullbackOnRingedTopoi.derivedPullbackComparison_isIso_of_boundedAbove_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/DerivedPullbackAsATriangulatedFunctor.lean, line 151. The attribute's comment: “computation on bounded above complexes of flat modules, for a morphism of ringed topoi presented by a morphism of the underlying sites, at RingedTopos.{u, u, u}”.
Tag 06YY, the computation on a bounded above complex of flat modules. A bounded above complex of flat
O'-modules is K-flat by Tag 06YQ, so the canonical comparison is invertible there too. This is the "in particular" of the source's statement.This is
isIso_derivedPullbackComparison_app_of_boundedAbove_of_flatofStacks.Sheaves.RingedToposDerivedPullbackwith both of its inputs discharged.
theorem derivedPullbackComparison_isIso_of_boundedAbove_of_flat
(K : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) ℤ)
(hbound : ∃ n : ℤ, K.IsStrictlyLE n)
(hflat : ∀ i : ℤ, SheafOfModules.IsFlat.{u, u, u, u} (O := Y.O) (K.X i)) :
haveI := hasLeftDerivedFunctor_pullbackOnHomotopy f hmos
IsIso ((derivedPullbackComparison f).app
((HomotopyCategory.quotient _ (ComplexShape.up ℤ)).obj K))
Stacks.Cohomology.DerivedPullbackOnRingedTopoi.isTriangulated_derivedPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/DerivedPullbackExistence.lean, line 172. The attribute's comment: “exactness”.
Tag 06YY, exactness. The derived pullback along a morphism of ringed topoi is an exact functor of triangulated categories.
theorem isTriangulated_derivedPullback : (derivedPullback f).IsTriangulated
Stacks.Cohomology.DerivedPullbackOnRingedTopoi.isIso_derivedPullbackComparison_app_kFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/DerivedPullbackExistence.lean, line 180. The attribute's comment: “computation on K-flat complexes with flat terms”.
Tag 06YY, the computation. The canonical comparison
Lf^* K^• ⟶ f^* K^•is invertible at a K-flat complex ofO'-modules with flat terms: the derived pullback of such a complex is computed by degreewise pullback.
theorem isIso_derivedPullbackComparison_app_kFlat
(K : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) ℤ)
(hK :
letI := Stacks.SheafOfModules.Tensor.sheafTensor_obj_additive.{u, u, u, u, u} Y.O
@CochainComplex.KFlatBifunctor.KFlat
(_root_.SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))
(_root_.SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))
(_root_.SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))
inferInstance inferInstance inferInstance inferInstance inferInstance inferInstance
(Stacks.SheafOfModules.Tensor.sheafTensor.{u, u, u, u, u} Y.O)
(Stacks.SheafOfModules.Tensor.sheafTensor_additive.{u, u, u, u, u} Y.O)
(Stacks.SheafOfModules.Tensor.sheafTensor_obj_additive.{u, u, u, u, u} Y.O)
inferInstance K)
(hflat : ∀ i : ℤ, SheafOfModules.IsFlat.{u, u, u, u} (O := Y.O) (K.X i)) :
IsIso ((derivedPullbackComparison f).app
((HomotopyCategory.quotient _ (ComplexShape.up ℤ)).obj K))
Stacks.Cohomology.DerivedPullbackOnRingedTopoi.isIso_derivedPullbackComparison_app_boundedAbove, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/DerivedPullbackExistence.lean, line 204. The attribute's comment: “computation on bounded above flat complexes”.
Tag 06YY, the computation on bounded above complexes of flat modules. A bounded above complex of flat
O'-modules is K-flat by Tag 06YQ, so its derived pullback is computed by degreewise pullback.
theorem isIso_derivedPullbackComparison_app_boundedAbove
(K : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) ℤ)
(hbound : ∃ n : ℤ, K.IsStrictlyLE n)
(hflat : ∀ i : ℤ, SheafOfModules.IsFlat.{u, u, u, u} (O := Y.O) (K.X i)) :
IsIso ((derivedPullbackComparison f).app
((HomotopyCategory.quotient _ (ComplexShape.up ℤ)).obj K))
Stacks.Sheaves.RingedToposDerivedPullback.derivedPullback_commShift, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/DerivedPullbackOfRingedTopoi.lean, line 284. The attribute's comment: “compatibility with shifts”.
Tag 06YY, compatibility with shifts. The derived pullback commutes with the shift functors of the two derived categories.
noncomputable instance derivedPullback_commShift :
(Stacks.Cohomology.DerivedPullbackPushforwardAdjunction.derivedPullback f).CommShift ℤ
Stacks.Cohomology.DerivedPullbackOfToposHom.derivedPullback, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/DerivedPullbackOfToposHom.lean, line 217. The attribute's comment: “the derived pullback functor, for a morphism of ringed topoi whose two ringed topoi have their object, morphism and structure-ring universes free and unrelated, and whose geometric datum is a morphism of the underlying topoi rather than of the underlying sites”.
Tag 06YY, the derived pullback functor, at independent universes. The derived pullback
Lf^* : D(𝒪') ⥤ D(𝒪)along a morphism of ringed topoi, the total left derived functor of degreewise pullback followed by localization.The two ringed topoi have all six of their universes free, and the geometric datum is the two-field morphism of ringed topoi of Stacks 01D3, part (2); in particular this applies to the small étale ringed topos
AlgebraicGeometry.RingedTopos.{u, u + 1, u}of an algebraic space, whichStacks.Cohomology.DerivedPullbackPushforwardAdjunction.derivedPullbackdoes not.The instance argument is
Prop-valued and is supplied bypullbackOnHomotopy_hasLeftDerivedFunctorfrom a resolving datum forf^*.
noncomputable abbrev derivedPullback :
DerivedCategory (SheafOfModules.{w'} (SheafOfModules.Tensor.ringSheaf Y.O)) ⥤
DerivedCategory (SheafOfModules.{w} (SheafOfModules.Tensor.ringSheaf X.O))
Stacks.Cohomology.DerivedPullbackOfToposHom.derivedPullbackComparison, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/DerivedPullbackOfToposHom.lean, line 227. The attribute's comment: “the canonical comparison Lf^* ⟶ f^*, at free and unrelated universes for the two ringed topoi and for a geometric datum which is a morphism of the underlying topoi”.
Tag 06YY, the canonical comparison, at independent universes. The comparison
Lf^* ⟶ f^*from the derived pullback to degreewise pullback, whose invertibility on a resolving class is the computation assertion of Tag 06YY.
noncomputable abbrev derivedPullbackComparison :
DerivedCategory.Qh ⋙ derivedPullback f ⟶ pullbackOnHomotopy f
Stacks.Cohomology.DerivedPullbackOfToposHom.derivedPullback_commShift, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/DerivedPullbackOfToposHom.lean, line 235. The attribute's comment: “compatibility of Lf^* with the shift, at free and unrelated universes for the two ringed topoi”.
Tag 06YY, compatibility with shifts, at independent universes. The derived pullback commutes with the shift functors of the two derived categories.
noncomputable instance derivedPullback_commShift : (derivedPullback f).CommShift ℤ
Stacks.Cohomology.DerivedPullbackOfToposHom.isIso_derivedPullbackComparison_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/DerivedPullbackOfToposHom.lean, line 247. The attribute's comment: “the computation Lf^*𝒦 = f^*𝒦 on a resolving class, at free and unrelated universes for the two ringed topoi”.
Tag 06YY, the computation, at independent universes. The canonical comparison
Lf^* 𝒦^• ⟶ f^* 𝒦^•is invertible at an object of a resolving class forf^*: the derived pullback of such a complex is computed by degreewise pullback.At the class of K-flat complexes with flat terms, which is the class the source resolves by, this is the computation assertion of Tag 06YY in the form it states.
theorem isIso_derivedPullbackComparison_app
(P : ObjectProperty
(HomotopyCategory (SheafOfModules.{w'} (SheafOfModules.Tensor.ringSheaf Y.O))
(ComplexShape.up ℤ)))
(hP : HasResolutions (Y := Y) P) (hinv : PullbackInvertsQuasiIso f P)
(K : HomotopyCategory (SheafOfModules.{w'} (SheafOfModules.Tensor.ringSheaf Y.O))
(ComplexShape.up ℤ))
(hK : P K) :
IsIso ((derivedPullbackComparison f).app K)
Stacks.Cohomology.DerivedPullbackOfToposHom.derivedPullback_isTriangulated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/DerivedPullbackOfToposHomTriangulated.lean, line 87. The attribute's comment: “exactness of the derived pullback, for a morphism of ringed topoi whose geometric datum is a morphism of the underlying topoi”.
[Stacks, Tag 06YY], exactness, for a morphism of ringed topoi. The derived pullback
Lf^* : D(𝒪_D) ⟶ D(𝒪_C)is a triangulated functor. Every morphism ofD(𝒪_D)is, up to isomorphism, the image of a morphism between K-flat complexes with flat terms; its mapping cone is again such a complex, and on such complexesLf^*is computed by the degreewise pullback, which carries the mapping-cone triangle to a distinguished triangle.
theorem derivedPullback_isTriangulated :
(Stacks.Cohomology.DerivedPullbackOfToposHom.derivedPullback f).IsTriangulated
Stacks.Cohomology.DerivedPullbackPushforwardAdjunction.derivedPullback, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPushforward/AdjunctionForRingedTopoi.lean, line 425. The attribute's comment: “the derived pullback functor”.
Tag 06YY, the derived pullback functor. The derived pullback
Lf^* : D(𝒪') ⥤ D(𝒪), the total left derived functor of degreewise pullback followed by localization.The instance argument is discharged for every morphism of ringed topoi by
Stacks.Cohomology.DerivedPullbackOnRingedTopoi.hasLeftDerivedFunctor_pullbackOnHomotopy, so this is the functor Tag 06YY asserts to exist.
noncomputable abbrev derivedPullback :
DerivedCategory (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) ⥤
DerivedCategory (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
Stacks.Cohomology.DerivedPullbackPushforwardAdjunction.derivedPullbackComparison, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPushforward/AdjunctionForRingedTopoi.lean, line 436. The attribute's comment: “canonical comparison”.
Tag 06YY, the canonical comparison. The comparison
Lf^* ⟶ f^*from the derived pullback to degreewise pullback, whose invertibility on K-flat complexes with flat terms is the computation assertion of Tag 06YY.
noncomputable abbrev derivedPullbackComparison :
DerivedCategory.Qh ⋙ derivedPullback f ⟶ pullbackOnHomotopy f
Stacks.Cohomology.DerivedPullbackOfToposHom.pullbackInvertsQuasiIso_isKFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPushforward/PullbackInvertsQuasiIsoOfToposHom.lean, line 144. The attribute's comment: “exactness on K-flat complexes with flat terms, for an arbitrary morphism of ringed topoi”.
The exactness clause of Stacks 06YY for an arbitrary morphism of ringed topoi. Degreewise pullback along
fcarries a quasi-isomorphism between K-flat complexes ofO-modules with flat terms to an isomorphism ofD(O').The cone of such a quasi-isomorphism is acyclic and is again K-flat with flat terms, so its degreewise pullback is acyclic; the conclusion is then read off the image of the mapping-cone triangle under the triangulated functor
K(f^*).
theorem pullbackInvertsQuasiIso_isKFlat (f : RingedToposHom X Y) :
PullbackInvertsQuasiIso f (IsKFlat (Y := Y))
Tag 0D6D, a lemma
Tag 0D6D in the Stacks Project.
CategoryTheory.SimplicialSiteSituation.isIso_derivedTransitionCompComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/DerivedPullbackComposition.lean, line 164. The attribute's comment: “for the transition morphisms of a simplicial-site situation”.
The canonical comparison from the composite of the derived pullbacks along the transitions of
ψandφto the derived pullback along the transition ofψ ≫ φis an isomorphism, soLf_ψ^* ∘ Lf_φ^* = Lf_{ψ ≫ φ}^*.
theorem isIso_derivedTransitionCompComparison {l m n : SimplexCategory} (ψ : l ⟶ m)
(φ : m ⟶ n) :
IsIso (S.derivedTransitionCompComparison O ψ φ)
CategoryTheory.SimplicialSiteSituation.derivedTransitionCompIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/DerivedPullbackComposition.lean, line 177. The attribute's comment: “for the transition morphisms of a simplicial-site situation, as a natural isomorphism”.
The natural isomorphism
Lf_ψ^* ⋙ Lf_φ^* ≅ Lf_{ψ ≫ φ}^*given by the canonical comparison.
noncomputable def derivedTransitionCompIso {l m n : SimplexCategory} (ψ : l ⟶ m) (φ : m ⟶ n) :
S.derivedTransitionPullback O ψ ⋙ S.derivedTransitionPullback O φ ≅
S.derivedTransitionPullback O (ψ ≫ φ)
Stacks.Cohomology.DerivedPullbackCompositionOfToposHom.isIso_derivedPullbackCompComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/CompositionOfToposHom.lean, line 351. The attribute's comment: “for a morphism of ringed topoi whose geometric datum is a morphism of the underlying topoi rather than a continuous functor between the underlying sites, with no morphism-of-sites hypothesis”.
Stacks 0D6D. For composable morphisms of ringed topoi
fandg, the canonical comparison from the composite of the derived pullbacks to the derived pullback alongg ∘ fis an isomorphism, soLf^* ∘ Lg^* = L(g ∘ f)^*.There is no hypothesis: the geometric datum is the two-field morphism of ringed topoi of Stacks 01D3, part (2), with no continuous functor between underlying sites and no morphism-of-sites condition. Both functors are left derived functors of degreewise pullback along
g ∘ f, and a map between left derived functors induced by the universal property is invertible exactly then.
theorem isIso_derivedPullbackCompComparison :
IsIso (derivedPullbackCompComparison f g)
Stacks.Cohomology.DerivedPullbackCompositionOfToposHom.derivedPullbackCompIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/CompositionOfToposHom.lean, line 363. The attribute's comment: “as a natural isomorphism, for a morphism of ringed topoi whose geometric datum is a morphism of the underlying topoi rather than a continuous functor between the underlying sites, with no morphism-of-sites hypothesis”.
Stacks 0D6D as a natural isomorphism
Lg^* ⋙ Lf^* ≅ L(g ∘ f)^*, for morphisms of ringed topoi and with no hypothesis, obtained by inverting the canonical comparison.
def derivedPullbackCompIso :
derivedPullback g ⋙ derivedPullback f ≅ derivedPullback (g.comp f)
Stacks.Cohomology.DerivedPullbackCompositionOnTopoi.isIso_derivedPullbackCompComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/CompositionOnRingedTopoi.lean, line 381.
Stacks 0D6D. For composable morphisms of ringed topoi
fandg, the canonical comparison from the composite of the derived pullbacks to the derived pullback alongg ∘ fis an isomorphism, soLf^* ∘ Lg^* = L(g ∘ f)^*.Both functors are left derived functors of degreewise pullback along
g ∘ f, and a map between left derived functors induced by the universal property is invertible exactly then.
theorem isIso_derivedPullbackCompComparison :
IsIso (derivedPullbackCompComparison f g)
Stacks.Cohomology.DerivedPullbackCompositionOnTopoi.derivedPullbackCompIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/CompositionOnRingedTopoi.lean, line 394. The attribute's comment: “as a natural isomorphism”.
Stacks 0D6D as a natural isomorphism
Lg^* ⋙ Lf^* ≅ L(g ∘ f)^*, obtained by inverting the canonical comparison.
def derivedPullbackCompIso :
derivedPullback g ⋙ derivedPullback f ≅ derivedPullback (g.comp f)
Tag 07A4, a lemma
Tag 07A4 in the Stacks Project.
CategoryTheory.SimplicialSiteSituation.componentDerivedTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/ComponentDerivedTensor.lean, line 94. The attribute's comment: “the canonical bifunctorial isomorphism, for the component inverse image”.
The derived tensor comparison at the inclusion of a simplicial component. The canonical bifunctorial isomorphism
g_n^*(A ⊗^L_O B) ≅ g_n^*A ⊗^L_{O_n} g_n^*Bfor the derived restriction
Lg_n^*of sheaves of modules to the degree-ncomponent of a simplicial-site situation, stated between the two uncurried bifunctors onD(O) × D(O), so that naturality in both variables is part of its type.Its value on a pair of K-flat complexes with flat terms is
Stacks.DerivedTensor.ExactFunctorTensor.modelIso, and the passage to arbitrary objects ofD(O)is the descent of that value along the localization of pairs of models.
def componentDerivedTensorIso :
Functor.uncurry.obj (Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor
(S.totalRingedTopos O).O) ⋙
S.derivedComponentModuleRestriction O n ≅
(S.derivedComponentModuleRestriction O n).prod
(S.derivedComponentModuleRestriction O n) ⋙
Functor.uncurry.obj (Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor
(S.componentRingedTopos O n).O)
Stacks.Sheaves.DerivedPullback.derivedPullbackTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/DerivedPullbackTensorComparison.lean, line 638. The attribute's comment: “the canonical bifunctorial isomorphism”.
Stacks 07A4. The canonical bifunctorial isomorphism
Lf^*(K ⊗^L_{O'} L) ≅ Lf^*K ⊗^L_O Lf^*Lfor a morphism of ringed topoi
f : (Sh(C), O) ⟶ (Sh(D), O'), stated between the two uncurried bifunctors onD(O') × D(O'), so that naturality in both variables is part of its type.Its value on a pair of K-flat complexes with flat terms is the five-step composite of the source (
derivedPullbackTensorModelIso), and the passage to arbitrary objects ofD(O')is the descent of that value along the localization of pairs of models.
def derivedPullbackTensorIso :
Functor.uncurry.obj (Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor Y.O) ⋙
derivedPullback f ≅
(derivedPullback f).prod (derivedPullback f) ⋙
Functor.uncurry.obj
(Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor X.O)
Stacks.Sheaves.DerivedPullback.OfToposHom.derivedPullbackTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/DerivedPullbackTensorComparisonOfToposHom.lean, line 555. The attribute's comment: “the canonical bifunctorial isomorphism, for a morphism of ringed topoi whose geometric datum is a morphism of the underlying topoi rather than of the underlying sites”.
Stacks 07A4. The canonical bifunctorial isomorphism
Lf^*(K ⊗^L_{O'} L) ≅ Lf^*K ⊗^L_O Lf^*Lfor a morphism of ringed topoi
f : (Sh(C), O) ⟶ (Sh(D), O')— a morphism of the underlying topoi together with the structure map, with no hypothesis on the underlying sites — stated between the two uncurried bifunctors onD(O') × D(O'), so that naturality in both variables is part of its type.Its value on a pair of K-flat complexes with flat terms is the five-step composite of the source (
derivedPullbackTensorModelIso), and the passage to arbitrary objects ofD(O')is the descent of that value along the localization of pairs of models.
def derivedPullbackTensorIso :
Functor.uncurry.obj (Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor Y.O) ⋙
derivedPullback f ≅
(derivedPullback f).prod (derivedPullback f) ⋙
Functor.uncurry.obj
(Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor X.O)
Stacks.DerivedTensor.ExactFunctorTensor.derivedTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/ExactFunctorDerivedTensor.lean, line 467. The attribute's comment: “for an exact functor of sheaves of modules commuting with the total tensor complex”.
Stacks 07A4 for an exact functor commuting with the total tensor complex. The canonical bifunctorial isomorphism
LF(A ⊗^L_{O'} B) ≅ LF A ⊗^L_O LF B,stated between the two uncurried bifunctors on
D(O') × D(O'), so that naturality in both variables is part of its type.Its value on a pair of K-flat complexes with flat terms is
Stacks.DerivedTensor.ExactFunctorTensor.modelIso, and the passage to arbitrary objects ofD(O')is the descent of that value along the localization of pairs of models.
def derivedTensorIso :
Functor.uncurry.obj (Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor Y.O) ⋙
F.mapDerivedCategory ≅
F.mapDerivedCategory.prod F.mapDerivedCategory ⋙
Functor.uncurry.obj
(Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor X.O)
Tag 08I6, a lemma
Tag 08I6 in the Stacks Project.
Stacks.Cohomology.MixedDerivedTensor.derivedMixedTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/MixedDerivedTensor/DerivedMixedTensor.lean, line 604. The attribute's comment: “variant: the isomorphism read in D(f⁻¹O') after restriction of scalars, for a site-presented morphism; the tag in D(O) for an arbitrary morphism of ringed topoi is Stacks.Cohomology.MixedDerivedTensor.OfToposHom.derivedMixedTensorIso”.
Stacks 08I6, read after restriction of scalars to
f⁻¹O'. The bifunctorial isomorphism
(F ⊗^L_O Lf^*G)|_{f⁻¹O'} ≅ F|_{f⁻¹O'} ⊗^L_{f⁻¹O'} f⁻¹Gin
D(f⁻¹O'), for a site-presented morphism of ringed topoif : (Sh(C), O) ⟶ (Sh(C'), O'),FinD(O)andGinD(O'). It is stated between the two uncurried bifunctors onD(O) × D(O'), so that naturality in both variables is part of its type. The tag itself, inD(O)and for an arbitrary morphism of ringed topoi, isStacks.Cohomology.MixedDerivedTensor.OfToposHom.derivedMixedTensorIso.Its value at a complex of
O-modules and a K-flat complex ofO'-modules with flat terms is the chain of the source (derivedMixedTensorModelIso): there both sides are computed by total tensor complexes and the identity is the underived one of the source, applied in each bidegree. The passage to arbitrary objects is the descent of that value along the localization of pairs of models.
def derivedMixedTensorIso :
mixedDerivedTensorPullback f ≅ mixedDerivedTensorInverseImage f
Stacks.Cohomology.MixedDerivedTensor.OfToposHom.derivedMixedTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/MixedDerivedTensor/DerivedMixedTensorOfToposHom.lean, line 601. The attribute's comment: “the canonical bifunctorial isomorphism in D(O), for an arbitrary morphism of ringed topoi”.
Stacks 08I6. For a morphism of ringed topoi
f : (Sh(C), O) ⟶ (Sh(C'), O')— a morphism of the underlying topoi together with the structure map, with no hypothesis on the underlying sites — the canonical bifunctorial isomorphism
F ⊗^L_O Lf^*G ≅ F ⊗^L_{f⁻¹O'} f⁻¹Gin
D(O), forFinD(O)andGinD(O'). The right-hand side is the derived tensor product overf⁻¹O'(coeffMixedDerivedTensoralong the structure mapf⁻¹O' ⟶ O) ofFand the inverse imagef⁻¹G(derivedInverseImage), an object ofD(O)throughF. It is stated between the two uncurried bifunctors onD(O) × D(O'), so that bifunctoriality is part of its type.At a complex
FofO-modules and a K-flat complexGofO'-modules with flat terms both sides are total complexes and the isomorphism is the underived identityF ⊗_{f⁻¹O'} f⁻¹G ≅ F ⊗_O f^*Gin each bidegree (modelIso); the passage to arbitrary objects is the descent along the localization of pairs of models.
def derivedMixedTensorIso :
derivedTensorPullback f ≅ derivedMixedTensorInverseImage f
Tag 0DEN, a lemma
Tag 0DEN in the Stacks Project.
Stacks.SheafOfModules.SitePointStalkSheafify.kFlat_of_stalks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/SitePointStalkTensorSheafify.lean, line 80. The attribute's comment: “part (2)”.
Stacks 0DEN, part (2), with no extra hypothesis. On a ringed site whose underlying site has enough points, a complex of
O-modules whose stalk at every point is a K-flat complex of modules over the stalk ofOis itself K-flat.This is
Stacks.Sheaves.KFlatStalkCriterion.kFlat_of_stalkswith itsStacks.Sheaves.KFlatStalkCriterion.StalkTensorDataargument supplied bystalkTensorData.
theorem kFlat_of_stalks (hJ : J.HasConservativeFamily.{u})
(K : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf O)) ℤ)
(hK : ∀ Ψ : J.Point.{u},
CochainComplex.KFlat.{u, u} (Stacks.Sheaves.KFlatStalkCriterion.stalkComplex O Ψ K)) :
Stacks.SheafOfModules.IsKFlat O K
Stacks.Sheaves.KFlatStalkCriterion.kFlatStalk_of_kFlat_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/StalkRetractFromFreeModules.lean, line 246. The attribute's comment: “part (1)”.
Stacks 0DEN, part (1). On a ringed site, a K-flat complex of
O-modules has K-flat stalk complex at every point of the site.This is
Stacks.Sheaves.KFlatStalkCriterion.kFlatStalk_of_kFlat_of_stalkRetractwith its one remaining obligation discharged bystalkRetractFinitelyPresented, so the hypotheses are exactly those of the source. Part (2), the converse under the hypothesis that the site has enough points, isStacks.SheafOfModules.SitePointStalkSheafify.kFlat_of_stalks.
theorem kFlatStalk_of_kFlat_unconditional (Φ : J.Point.{u})
(K : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf O)) ℤ)
(hK : Stacks.SheafOfModules.IsKFlat O K) :
CochainComplex.KFlat.{u, u} (stalkComplex O Φ K)
Tag 0DEP, a lemma
Tag 0DEP in the Stacks Project.
Stacks.Sheaves.DerivedPullback.KFlatPullbackMorphismOfSites.kFlat_pullbackComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/StalkBaseChangeAtTheTargetPoint.lean, line 332.
Stacks 0DEP. Let
f : (Sh(C), O) ⟶ (Sh(C'), O')be a morphism of ringed topoi whose underlying functor of the sites is a morphism of sites, and suppose the siteChas a conservative family of points. Then the degreewise pullback alongfof a K-flat complex ofO'-modules is a K-flat complex ofO-modules.The proof is the source's. K-flatness of
f^*Kis tested at the points ofCby part (2) of Stacks 0DEN, which applies becauseChas a conservative family of points. At a pointΦofCthe stalk complex off^*Kis the extension of scalars, along a mapO'_Ψ ⟶ O_Φof stalk rings, of the stalk complex ofKat the pointΨ = f ∘ ΦofC'produced by part (2) of Stacks 00YA; that isstalkComplexIso, which is Stacks 05V5 at the level of complexes, built from Stacks 05V1 for the inverse image and the stalkwise formula for the extension of scalars alongf⁻¹O' ⟶ O. The stalk complexes ofKare K-flat by part (1) of Stacks 0DEN on the target, and extension of scalars preserves K-flatness by Stacks 06Y1.
theorem kFlat_pullbackComplex (hX : X.J.HasConservativeFamily.{u})
(K : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) ℤ)
(hK : Stacks.SheafOfModules.IsKFlat Y.O K) :
Stacks.SheafOfModules.IsKFlat X.O ((KFlatPullback.pullbackComplex f).obj K)
Stacks.Sheaves.DerivedPullback.StalkBaseChangeOfToposHom.kFlat_pullbackComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/StalkBaseChangeOfToposHom.lean, line 372.
Stacks 0DEP. Let
f : (Sh(C), O) ⟶ (Sh(C'), O')be a morphism of ringed topoi and suppose the siteChas a conservative family of points. Then the degreewise pullback alongfof a K-flat complex ofO'-modules is a K-flat complex ofO-modules.The proof is the source's. K-flatness of
f^*Kis tested at the points ofCby part (2) of Stacks 0DEN, which applies becauseChas a conservative family of points. At a pointΦofCthe stalk complex off^*Kis the extension of scalars, along the mapO'_Ψ ⟶ O_Φof stalk rings, of the stalk complex ofKat the pointΨ = f ∘ ΦofC'produced by part (2) of Stacks 00YA; that isstalkComplexIso, which is Stacks 05V5 at the level of complexes. The stalk complexes ofKare K-flat by part (1) of Stacks 0DEN on the target, and extension of scalars preserves K-flatness by Stacks 06Y1.
theorem kFlat_pullbackComplex (hX : X.J.HasConservativeFamily.{u})
(K : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) ℤ)
(hK : Stacks.SheafOfModules.IsKFlat Y.O K) :
Stacks.SheafOfModules.IsKFlat X.O ((KFlatPullbackOfToposHom.pullbackComplex f).obj K)
Tag 0FPH, a lemma
Tag 0FPH in the Stacks Project.
Stacks.Sheaves.DerivedPullback.OfToposHom.derivedPullback_toTensor_square, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/DerivedPullbackTensorTotalSquareOfToposHom.lean, line 172. The attribute's comment: “for an arbitrary morphism of ringed topoi in the two-field sense of Tag 01D3, part (2) (a morphism of the underlying topoi with its structure map, no functor between the underlying sites and no morphism-of-sites hypothesis), at RingedTopos.{u, u, u}, for all complexes K, M; the statement carries no hypothesis or class argument”.
Stacks 0FPH, for a morphism of ringed topoi. For a morphism of ringed topoi
f : (Sh(C), O_C) ⟶ (Sh(D), O_D)— a morphism of the underlying topoi together with the structure map — and cochain complexesK,MofO_D-modules, the square formed by the canonical maps from the derived tensor product to the ordinary total tensor complex, the comparisonLf^*(K ⊗^L_{O_D} M) ≅ Lf^*K ⊗^L_{O_C} Lf^*Mof Stacks 07A4 followed by the comparisonLf^* ⟶ f^*in each tensor factor, and that same comparison atTot(K ⊗ M)followed by the identificationf^*Tot(K ⊗_{O_D} M) ≅ Tot(f^*K ⊗_{O_C} f^*M)of Stacks 03EL, commutes.The statement has no hypothesis and no class argument of its own: instance search supplies every class argument of
derivedPullback_toTensor_square_of_instances.
theorem derivedPullback_toTensor_square {X Y : RingedTopos.{u, u, u}}
(f : AlgebraicGeometry.RingedToposHom X Y)
(K M : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) ℤ) :
(derivedPullback f).map
((Stacks.DerivedTensor.RingedSite.canonicalDerivedTensorProduct Y.O).toTensor K M) ≫
pullbackComparisonQ f
(((Stacks.SheafOfModules.Tensor.tensorComplex Y.O).obj K).obj M) ≫
DerivedCategory.Q.map (pullbackTensorComplexIso f K M).hom =
(derivedPullbackTensorIso f).hom.app (DerivedCategory.Q.obj K, DerivedCategory.Q.obj M) ≫
bifunctorMap (Stacks.DerivedTensor.RingedSite.canonicalDerivedTensorProduct X.O).tensor
(pullbackComparisonQ f K) (pullbackComparisonQ f M) ≫
(Stacks.DerivedTensor.RingedSite.canonicalDerivedTensorProduct X.O).toTensor
((pullbackComplex f).obj K) ((pullbackComplex f).obj M)
Stacks.Sheaves.DerivedPullback.derivedPullback_toTensor_square_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/DerivedPullbackTensorTotalSquareUnconditional.lean, line 113. The attribute's comment: “for a morphism of ringed topoi presented by a morphism of the underlying sites, at RingedTopos.{u, u, u}”.
Stacks 0FPH. For a morphism of ringed topoi
f : (Sh(C), O_C) ⟶ (Sh(D), O_D)and cochain complexesK,MofO_D-modules, the square formed by the canonical maps from the derived tensor product to the ordinary total tensor complex, the comparisonLf^*(K ⊗^L_{O_D} M) ⟶ Lf^*K ⊗^L_{O_C} Lf^*Mof Stacks 07A4 followed by the derived-to-degreewise pullback comparison in each tensor factor, and that same comparison followed by the identificationf^*Tot(K ⊗_{O_D} M) ≅ Tot(f^*K ⊗_{O_C} f^*M), commutes.The complexes are arbitrary and the only inputs are
fandhmos.hmosis not a hypothesis beyond the source's: it is this development's encoding of "fis a morphism of ringed topoi".AlgebraicGeometry.RingedToposSiteHompresents the geometric morphism by a functorf.ubetween the underlying sites and asks only that it be continuous; exactness off^{-1}is not a field of it, and along a merely continuous functor the inverse image need not be exact, so such anfneed not present a morphism of topoi at all.CategoryTheory.Functor.IsMorphismOfSitesis continuity together with that exactness — it is Stacks 00X1 — and it is exactly whatAlgebraicGeometry.RingedToposSiteHom.toToposHomconsumes to produce the underlying morphism of topoi.The existence of
Lf^*is not assumed: it ishasLeftDerivedFunctor_pullbackOnHomotopy, the existence assertion of Stacks 06YY, which holds along every morphism of ringed topoi.
theorem derivedPullback_toTensor_square_unconditional
(K M : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) ℤ) :
haveI := hasLeftDerivedFunctor_pullbackOnHomotopy f hmos
(derivedPullback f).map
((Stacks.DerivedTensor.RingedSite.canonicalDerivedTensorProduct Y.O).toTensor K M) ≫
pullbackComparisonQ f
(((Stacks.SheafOfModules.Tensor.tensorComplex Y.O).obj K).obj M) ≫
DerivedCategory.Q.map (pullbackTensorComplexIso f hmos K M).hom =
derivedPullbackTensorComparison f hmos (DerivedCategory.Q.obj K)
(DerivedCategory.Q.obj M) ≫
bifunctorMap (Stacks.DerivedTensor.RingedSite.canonicalDerivedTensorProduct X.O).tensor
(pullbackComparisonQ f K) (pullbackComparisonQ f M) ≫
(Stacks.DerivedTensor.RingedSite.canonicalDerivedTensorProduct X.O).toTensor
((pullbackComplex f).obj K) ((pullbackComplex f).obj M)
Sources
Section21.19 Cohomology of unbounded complexes#
Section 21.19 of the Stacks Project, Tag 07A5. 9 tags here are carried by 21 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 07A5, the section
Tag 07A5 in the Stacks Project.
Stacks.Cohomology.ModuleSections.globalSectionsKInjectiveIso_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedSections/KInjectiveSectionsNaturality.lean, line 60. The attribute's comment: “global sections of modules on a ringed site, naturality of the comparison”.
The comparison of global sections with derived global sections on a K-injective complex is natural. For a morphism
t : I ⟶ Jof K-injective complexes ofO-modules, the class of the induced morphism of global section complexes corresponds to the morphismRΓ(C, I) ⟶ RΓ(C, J)induced by the class oft.
theorem globalSectionsKInjectiveIso_naturality
{I J : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ}
[I.IsKInjective] [J.IsKInjective]
(t : I ⟶ J) :
DerivedCategory.Q.map
(((moduleGlobalSections X).mapHomologicalComplex (ComplexShape.up ℤ)).map t) ≫
(globalSectionsKInjectiveIso X J).hom =
(globalSectionsKInjectiveIso X I).hom ≫
(derivedModuleGlobalSections X).map (DerivedCategory.Q.map t)
Tag 07A6, a lemma
Tag 07A6 in the Stacks Project.
Stacks.Cohomology.DerivedPullbackOnRingedTopoi.derivedAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/DerivedPullbackExistence.lean, line 164. The attribute's comment: “for a morphism of ringed topoi presented by a morphism of the underlying sites, at RingedTopos.{u, u, u}”.
Stacks 07A6 along an arbitrary morphism of ringed topoi. The unbounded derived pullback
Lf^*is left adjoint to the unbounded derived pushforwardRf_*.This is
derivedPullbackPushforwardAdjunctionOfKFlatwith its one deferred input supplied bypullbackInvertsQuasiIso_isKFlat. AnAdjunctionis exactly the bifunctorial bijectionHom_{D(𝒪_C)}(Lf^*G, F) = Hom_{D(𝒪_D)}(G, Rf_*F)that the source states: itshomEquivis the bijection andAdjunction.homEquiv_naturality_left,homEquiv_naturality_rightare its naturality in the two arguments.The only input is
hmos, and it is not an assumption beyond the source's.RingedToposSiteHomrecords continuity off.uand nothing else, sofalone is a morphism of ringed sites;hmos : f.u.IsMorphismOfSites Y.J X.Jadds the exactness off^{-1}that Stacks 00X1 demands, which is what makesfa morphism of ringed topoi (Stacks 00XC,CategoryTheory.Functor.IsMorphismOfSites.morphismOfTopoi). Everything else the construction needed has been discharged: the deferred exactness input ispullbackInvertsQuasiIso_isKFlat, which holds along every morphism of ringed topoi, and theHasLeftDerivedFunctorbinder is aPropclass discharged byhasLeftDerivedFunctor_pullbackOnHomotopy.
noncomputable def derivedAdjunction : derivedPullback f ⊣ derivedPushforward f
Stacks.Cohomology.DerivedPullbackOfToposHom.derivedAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPushforward/DerivedAdjunctionOfToposHom.lean, line 195. The attribute's comment: “for a morphism of ringed topoi in the two-field sense of Tag 01D3, part (2) -- a morphism of the underlying topoi together with the structure map, with no continuous functor between the underlying sites -- and with no hypothesis beyond those making the two categories of modules exist”.
Stacks 07A6 for a morphism of ringed topoi. The total left derived pullback
Lf^*is left adjoint to the total right derived direct imageRf_*,Hom_{D(𝒪)}(Lf^*𝒢, ℱ) = Hom_{D(𝒪')}(𝒢, Rf_*ℱ), bifunctorially in the unbounded derived categories.This is
Stacks.Cohomology.DerivedPushforward.derivedPullbackPushforwardAdjunction, Stacks 07A6 relative to the Stacks 06YY datum, at the datumkFlatLeftDerivedPullback; the hypothesis for whose sake the attribute is withheld there is discharged, so there is none left.
def derivedAdjunction (f : RingedToposHom X Y) :
derivedPullback f ⊣ derivedPushforward (X := X) (Y := Y) f
Stacks.Cohomology.DerivedPushforward.derivedPullbackPushforwardAdjunctionOfToposHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPushforward/PullbackAdjunctionOfToposHom.lean, line 76. The attribute's comment: “for a morphism of ringed topoi whose two sites are small in the universe of the sections of their structure sheaves”.
For a morphism of ringed topoi
f, the derived pullbackLf^*is left adjoint to the derived direct imageRf_*on the unbounded derived categories,Hom_{D(𝒪)}(Lf^*G, F) = Hom_{D(𝒪')}(G, Rf_*F).
def derivedPullbackPushforwardAdjunctionOfToposHom :
DerivedPullbackOfToposHom.derivedPullback f ⊣ derivedPushforward (X := X) (Y := Y) f
Tag 0D6E, a lemma
Tag 0D6E in the Stacks Project.
Stacks.Cohomology.DerivedPushforwardCompositionOfToposHom.isIso_derivedPushforwardComparison_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPushforward/CompositionOfToposHomUnconditional.lean, line 560. The attribute's comment: “for a morphism of ringed topoi in the two-field sense of Tag 01D3, part (2) -- a morphism of the underlying topoi together with the structure map, with no continuous functor between the underlying sites -- and with no hypothesis on either morphism; the three universes of each of the three ringed topoi are free and unrelated”.
Stacks 0D6E for a morphism of ringed topoi. For composable morphisms of ringed topoi
f : (Sh(𝒞), 𝒪_𝒞) ⟶ (Sh(𝒟), 𝒪_𝒟)andg : (Sh(𝒟), 𝒪_𝒟) ⟶ (Sh(ℰ), 𝒪_ℰ), the canonical comparison from a derived direct image alongg ∘ fto the composite of the derived direct images alongfandgis an isomorphism, soRg_* ∘ Rf_* = R(g ∘ f)_*as functorsD(𝒪_𝒞) ⟶ D(𝒪_ℰ).There is no hypothesis on either morphism: the geometric datum is the two-field morphism of ringed topoi of Stacks 01D3, part (2), with no continuous functor between the underlying sites, and the condition that
AlgebraicGeometry.RingedToposHom.derivedPushforwardComparison_isIsocarries — Stacks 093Y forf, which at module coefficients Stacks 075L records as false in general — is discharged byisIso_app_pushforwardMapHomotopy_of_isKInjective.
theorem isIso_derivedPushforwardComparison_unconditional
[Rf.IsRightDerivedFunctor αf (HomotopyCategory.quasiIso X.Modules (ComplexShape.up ℤ))]
[Rg.IsRightDerivedFunctor αg (HomotopyCategory.quasiIso Y.Modules (ComplexShape.up ℤ))]
[Rh.IsRightDerivedFunctor αh (HomotopyCategory.quasiIso X.Modules (ComplexShape.up ℤ))] :
IsIso (derivedPushforwardComparison f g Rf Rg Rh αf αg αh)
Stacks.Cohomology.DerivedPushforwardCompositionOnTopoi.isIso_derivedPushforwardComparison_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPushforward/CompositionOnRingedTopoiUnconditional.lean, line 535.
Stacks 0D6E. For composable morphisms of ringed topoi
f : (Sh(𝒞), 𝒪_𝒞) ⟶ (Sh(𝒟), 𝒪_𝒟)andg : (Sh(𝒟), 𝒪_𝒟) ⟶ (Sh(ℰ), 𝒪_ℰ), the canonical comparison from a derived pushforward alongg ∘ fto the composite of derived pushforwards alongfandgis an isomorphism, soRg_* ∘ Rf_* = R(g ∘ f)_*as functorsD(𝒪_𝒞) ⟶ D(𝒪_ℰ).No hypothesis beyond the two morphisms and the three presentations of the derived pushforwards: the condition
PushforwardComputesDerived, whichisIso_derivedPushforwardComparison_iffshows to be equivalent to this statement, is discharged bypushforwardComputesDerived.
theorem isIso_derivedPushforwardComparison_unconditional
[Rf.IsRightDerivedFunctor αf
(HomotopyCategory.quasiIso (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
(ComplexShape.up ℤ))]
[Rg.IsRightDerivedFunctor αg
(HomotopyCategory.quasiIso (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))
(ComplexShape.up ℤ))]
[Rh.IsRightDerivedFunctor αh
(HomotopyCategory.quasiIso (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
(ComplexShape.up ℤ))] :
IsIso (derivedPushforwardComparison f g Rf Rg Rh αf αg αh)
Stacks.Cohomology.DerivedPushforwardCompositionOnTopoi.derivedPushforwardCompIsoUnconditional, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPushforward/CompositionOnRingedTopoiUnconditional.lean, line 555. The attribute's comment: “as a natural isomorphism”.
Stacks 0D6E as a natural isomorphism
Rf_* ⋙ Rg_* ≅ R(g ∘ f)_*, obtained by inverting the canonical comparison. This is the source's equality of composite functors, in the only form in which it can hold: the two functors are total derived functors of different functors on the homotopy category, so they agree up to the canonical isomorphism and not on the nose.
noncomputable def derivedPushforwardCompIsoUnconditional
[Rf.IsRightDerivedFunctor αf
(HomotopyCategory.quasiIso (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
(ComplexShape.up ℤ))]
[Rg.IsRightDerivedFunctor αg
(HomotopyCategory.quasiIso (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))
(ComplexShape.up ℤ))]
[Rh.IsRightDerivedFunctor αh
(HomotopyCategory.quasiIso (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
(ComplexShape.up ℤ))] :
Rf ⋙ Rg ≅ Rh
Tag 07A7, a remark
Tag 07A7 in the Stacks Project.
Stacks.Cohomology.DerivedBaseChangeOfToposHom.derivedBaseChangeMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPushforward/BaseChangeOfToposHom.lean, line 176. The attribute's comment: “the canonical derived base change map Lg^* Rf_* K ⟶ Rf'_* L(g')^* K of a commutative square of morphisms of ringed topoi in the two-field sense of Tag 01D3, part (2) -- a morphism of the underlying topoi together with the map of structure sheaves, with no continuous functor between the underlying sites -- at the twelve free universes of the four ringed topoi”. References: SGA 6 IV (3.1.0).
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) gand an object
Kof the unbounded derived categoryD(𝒪_C), the canonical base change map
Lg^* Rf_* K ⟶ Rf'_* L(g')^* Kin
D(𝒪_{D'}).
def derivedBaseChangeMap (h : g.comp f' = f.comp g')
(K : DerivedCategory
(SheafOfModules.{wC} ((Stacks.SheafOfModules.Tensor.ringSheaf (J := X.J)) X.O))) :
(derivedPullback g).obj ((derivedPushforward f).obj K) ⟶
(derivedPushforward f').obj ((derivedPullback g').obj K)
Stacks.Cohomology.DerivedBaseChangeOfToposHom.derivedBaseChangeMap_adjoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPushforward/BaseChangeOfToposHom.lean, line 192. The attribute's comment: “the adjoint characterization which the source gives of the base change map of a commutative square of morphisms of ringed topoi in the two-field sense of Tag 01D3, part (2), and which pins the map down: its adjunct under L(f')^* ⊣ Rf'_* is L(g')^* of the derived counit, across the two composition isomorphisms of Tag 0D6D”.
The adjoint characterization of the base change map. Under the derived adjunction
L(f')^* ⊣ Rf'_*, the base change map of a commutative square of morphisms of ringed topoi isL(g')^*of the derived counitLf^* Rf_* K ⟶ K, transported across the two composition isomorphisms.
theorem derivedBaseChangeMap_adjoint (h : g.comp f' = f.comp g')
(K : DerivedCategory
(SheafOfModules.{wC} ((Stacks.SheafOfModules.Tensor.ringSheaf (J := X.J)) X.O))) :
((derivedAdjunction f').homEquiv
((derivedPullback g).obj ((derivedPushforward f).obj K))
((derivedPullback g').obj K)).symm
(derivedBaseChangeMap f g' f' g h K) =
(derivedPullbackCompIsoLeft f' g).hom.app ((derivedPushforward f).obj K) ≫
(derivedPullbackCompIsoRight f g' f' g h).inv.app ((derivedPushforward f).obj K) ≫
(derivedPullback g').map ((derivedAdjunction f).counit.app K)
Tag 0E46, a remark
Tag 0E46 in the Stacks Project.
Stacks.Cohomology.DerivedBaseChangePasting.derivedBaseChangeMap_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPushforward/BaseChangePastingOnRingedTopoi.lean, line 1068. The attribute's comment: “variant: the special case of squares of morphisms of ringed topoi presented by morphisms of sites; the tag for arbitrary morphisms of ringed topoi is Stacks.Cohomology.DerivedBaseChangeOfToposHom.derivedBaseChangeMapOfTwoIso_vertical”.
The vertical pasting law, for ringed topoi presented by morphisms of sites. For two vertically composable commutative squares of ringed topoi whose arrows come from morphisms of the underlying sites, the composite of the derived base change maps of the two squares, read through the composition isomorphisms for the derived pushforward along the two composite vertical legs, is the derived base change map of the outer rectangle.
Stacks 0E46 for arbitrary morphisms of ringed topoi is
Stacks.Cohomology.DerivedBaseChangeOfToposHom.derivedBaseChangeMapOfTwoIso_vertical.
theorem derivedBaseChangeMap_comp (htop : l.comp f' = f.comp k) (hbot : m.comp g' = g.comp l)
(K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf B.O))) :
(derivedPullback m).map ((derivedPushforwardCompIso f g hmosf hmosg).inv.app K) ≫
derivedBaseChangeMap g l g' m hmosg hmosl hmosg' hmosm hbot
((derivedPushforward f).obj K) ≫
(derivedPushforward g').map
(derivedBaseChangeMap f k f' l hmosf hmosk hmosf' hmosl htop K) ≫
(derivedPushforwardCompIso f' g' hmosf' hmosg').hom.app ((derivedPullback k).obj K) =
derivedBaseChangeMap (g.comp f) k (g'.comp f') m
(RingedToposSiteHom.isMorphismOfSites_comp_u f g hmosf hmosg) hmosk
(RingedToposSiteHom.isMorphismOfSites_comp_u f' g' hmosf' hmosg') hmosm
(comp_stack f g f' g' k l m htop hbot) K
Stacks.Cohomology.DerivedBaseChangeOfToposHom.derivedBaseChangeMapOfTwoIso_vertical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPushforward/BaseChangeVerticalPastingOfToposHom.lean, line 456.
Stacks 0E46. Consider a commutative diagram of ringed topoi
k (Sh(B'), 𝒪) ———→ (Sh(B), 𝒪) │ f' │ f v l v (Sh(C'), 𝒪) ———→ (Sh(C), 𝒪) │ g' │ g v v (Sh(D'), 𝒪) ———→ (Sh(D), 𝒪) min which each square commutes up to the given 2-isomorphism (Stacks 04IC):
st : l ∘ f' ≅ f ∘ kandsb : m ∘ g' ≅ g ∘ l, the outer rectangle commuting up to their pastingAlgebraicGeometry.RingedToposHom.TwoIso.pasteVertical st sb. Then the base change maps of Remark 07A7 for the two squares compose to the base change map of the rectangle: forKinD(𝒪_B), the composite
Lm^* R(g ∘ f)\_* K = Lm^* Rg\_* Rf\_* K ⟶ Rg'\_* Ll^* Rf\_* K ⟶ Rg'\_* Rf'\_* Lk^* K = R(g' ∘ f')\_* Lk^* Kis the base change map of the rectangle. The two identifications
=are the composition isomorphisms of Stacks 0D6E,derivedPushforwardCompIsoOfAdjoints.The seven morphisms are arbitrary morphisms of ringed topoi in the sense of Stacks 01D3, part (2), the two 2-isomorphisms are arbitrary, and the eighteen universes of the six ringed topoi are free. As for the base change map of Remark 07A7 itself (
derivedBaseChangeMapOfTwoIso), the module categories of the ringed topoi at the sources of the vertical arrows carry the instanceCategoryTheory.IsGrothendieckAbelianat their section universes, which is what makes the unbounded derived pushforwards exist at free universes (see the implementation notes ofStacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPushforward/Existence.lean).
theorem derivedBaseChangeMapOfTwoIso_vertical
(st : RingedToposHom.TwoIso (l.comp f') (f.comp k))
(sb : RingedToposHom.TwoIso (m.comp g') (g.comp l)) (K :
DerivedCategory (SheafOfModules.{wB} (SheafOfModules.Tensor.ringSheaf B.O))) :
(derivedPullback m).map ((derivedPushforwardCompIsoOfAdjoints f g).inv.app K) ≫
derivedBaseChangeMapOfTwoIso g l g' m sb ((derivedPushforward f).obj K) ≫
(derivedPushforward g').map (derivedBaseChangeMapOfTwoIso f k f' l st K) ≫
(derivedPushforwardCompIsoOfAdjoints f' g').hom.app ((derivedPullback k).obj K) =
derivedBaseChangeMapOfTwoIso (g.comp f) k (g'.comp f') m
(RingedToposHom.TwoIso.pasteVertical st sb) K
Tag 0E47, a remark
Tag 0E47 in the Stacks Project.
Stacks.Cohomology.DerivedBaseChangeOfToposHom.derivedBaseChangeMapOfTwoIso_horizontal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPushforward/BaseChangePastingOfToposHom.lean, line 388.
Stacks 0E47. Consider a commutative diagram of ringed topoi
g' g (Sh(C''), 𝒪) ———→ (Sh(C'), 𝒪) ———→ (Sh(C), 𝒪) │ f'' │ f' │ f v v v (Sh(D''), 𝒪) ———→ (Sh(D'), 𝒪) ———→ (Sh(D), 𝒪) h' hin which each square commutes up to the given 2-isomorphism (Stacks 04IC):
s : h ∘ f' ≅ f ∘ gands' : h' ∘ f'' ≅ f' ∘ g', the outer rectangle commuting up to their pastingAlgebraicGeometry.RingedToposHom.TwoIso.pasteHorizontal s s'. Then the base change maps of Remark 07A7 for the two squares compose to the base change map of the rectangle: forKinD(𝒪_C), the composite
L(h ∘ h')^* Rf\_* K = L(h')^* Lh^* Rf\_* K ⟶ L(h')^* Rf'\_* Lg^* K ⟶ Rf''\_* L(g')^* Lg^* K = Rf''\_* L(g ∘ g')^* Kis the base change map of the rectangle. The two identifications
=are the composition isomorphisms of Stacks 0D6D.The six morphisms are arbitrary morphisms of ringed topoi in the sense of Stacks 01D3, part (2), the two 2-isomorphisms are arbitrary, and the eighteen universes of the six ringed topoi are free. As for the base change map of Remark 07A7 itself (
derivedBaseChangeMapOfTwoIso), the module categories of the three upper ringed topoi carry the instanceCategoryTheory.IsGrothendieckAbelianat their section universes, which is what makes the unboundedRf_*exist at free universes (see the implementation notes ofStacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPushforward/Existence.lean).
theorem derivedBaseChangeMapOfTwoIso_horizontal
(s : RingedToposHom.TwoIso (h.comp f') (f.comp g))
(s' : RingedToposHom.TwoIso (h'.comp f'') (f'.comp g')) (K :
DerivedCategory (SheafOfModules.{wC} (SheafOfModules.Tensor.ringSheaf X.O))) :
(derivedPullbackCompIso h' h).inv.app ((derivedPushforward f).obj K) ≫
(derivedPullback h').map (derivedBaseChangeMapOfTwoIso f g f' h s K) ≫
derivedBaseChangeMapOfTwoIso f' g' f'' h' s' ((derivedPullback g).obj K) ≫
(derivedPushforward f'').map ((derivedPullbackCompIso g' g).hom.app K) =
derivedBaseChangeMapOfTwoIso f (g.comp g') f'' (h.comp h')
(RingedToposHom.TwoIso.pasteHorizontal s s') K
Stacks.Cohomology.DerivedBaseChangePasting.derivedBaseChangeMap_horizontal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPushforward/BaseChangePastingOnRingedTopoi.lean, line 796.
Stacks 0E47. For two horizontally composable commutative squares of ringed topoi, the composite of the derived base change maps of the two squares, read through the composition isomorphisms of Stacks 0D6D for the two composite horizontal legs, is the derived base change map of the outer rectangle.
theorem derivedBaseChangeMap_horizontal (hmosf : f.u.IsMorphismOfSites Y.J X.J)
(hmosf' : f'.u.IsMorphismOfSites Y'.J X'.J) (hmosf'' : f''.u.IsMorphismOfSites Y''.J X''.J)
(hmosg' : g'.u.IsMorphismOfSites X.J X'.J) (hmosg'' : g''.u.IsMorphismOfSites X'.J X''.J)
(hmosg : g.u.IsMorphismOfSites Y.J Y'.J) (hmosh : h.u.IsMorphismOfSites Y'.J Y''.J)
(sq : g.comp f' = f.comp g') (sq' : h.comp f'' = f'.comp g'')
(K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
(derivedPullbackCompIso h g hmosh hmosg).inv.app ((derivedPushforward f).obj K) ≫
(derivedPullback h).map
(derivedBaseChangeMap f g' f' g hmosf hmosg' hmosf' hmosg sq K) ≫
derivedBaseChangeMap f' g'' f'' h hmosf' hmosg'' hmosf'' hmosh sq'
((derivedPullback g').obj K) ≫
(derivedPushforward f'').map
((derivedPullbackCompIso g'' g' hmosg'' hmosg').hom.app K) =
derivedBaseChangeMap f (g'.comp g'') f'' (g.comp h) hmosf
(RingedToposSiteHom.isMorphismOfSites_comp_u g'' g' hmosg'' hmosg') hmosf''
(RingedToposSiteHom.isMorphismOfSites_comp_u h g hmosh hmosg)
(comp_rectangle f f' f'' g' g'' g h sq sq') K
Tag 0FPI, a lemma
Tag 0FPI in the Stacks Project.
Stacks.Cohomology.DerivedPullbackOfToposHom.derivedAdjunction_counit_fac, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPushforward/DerivedAdjunctionOfToposHom.lean, line 225. The attribute's comment: “for a morphism of ringed topoi in the two-field sense of Tag 01D3, part (2) -- a morphism of the underlying topoi together with the structure map, with no continuous functor between the underlying sites -- and with no hypothesis beyond those making the two categories of modules exist; stated at an object of the unbounded homotopy category, which a complex gives through HomotopyCategory.quotient”.
Stacks 0FPI for a morphism of ringed topoi. For a complex
𝒦of𝒪-modules the squareLf^* f_* 𝒦 ⟶ f^* f_* 𝒦 ↓ ↓ Lf^* Rf_* 𝒦 ⟶ 𝒦commutes in
D(𝒪): its upper edge is the comparisonLf^* ⟶ f^*of Stacks 06YY atf_*𝒦, its left edge isLf^*applied to the comparisonf_* ⟶ Rf_*, its lower edge is the counit of the derived adjunctionLf^* ⊣ Rf_*of Stacks 07A6 atRf_*𝒦, and its right edge is the ordinary counitf^*f_*𝒦 ⟶ 𝒦of Stacks 03D7.The derived counit is by construction the one induced by the ordinary one, which is exactly this commutativity, so the proof is
Stacks.Cohomology.DerivedPushforward.derivedPullbackPushforwardAdjunction_counit_facat the datumkFlatLeftDerivedPullback.The square is stated for an object of the unbounded homotopy category rather than for a cochain complex, which is the form the comparison maps of the two derived functors take and is more general: a complex gives such an object through
HomotopyCategory.quotient.
theorem derivedAdjunction_counit_fac (f : RingedToposHom X Y)
(K : HomotopyCategory (SheafOfModules.{w} (SheafOfModules.Tensor.ringSheaf X.O))
(ComplexShape.up ℤ)) :
(derivedPullback f).map
(((pushforwardOnHomotopy (X := X) (Y := Y) f).totalRightDerivedUnit DerivedCategory.Qh
(sourceQuasiIso X)).app K) ≫
(derivedAdjunction f).counit.app (DerivedCategory.Qh.obj K) =
(derivedPullbackComparison f).app ((pushforwardMapHomotopy f).obj K) ≫
DerivedCategory.Qh.map ((pullbackAdjPushforwardMapHomotopy f).counit.app K)
Stacks.Cohomology.DerivedPullbackOnRingedTopoi.derivedAdjunction_counit_fac, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPushforward/OrdinaryAndDerivedCounit.lean, line 117.
Stacks 0FPI. For a complex
Kof𝒪_C-modules the squareLf^* f_* K ⟶ f^* f_* K ↓ ↓ Lf^* Rf_* K ⟶ Kcommutes in
D(𝒪_C): its upper edge is the comparisonLf^* ⟶ f^*, its left edge isLf^*applied to the comparisonf_* ⟶ Rf_*, its lower edge is the counit of the derived adjunctionLf^* ⊣ Rf_*, and its right edge is the ordinary counitf^* f_* ⟶ id.The derived counit is the one induced by the ordinary counit, which is exactly this commutativity, so the proof is
derivedPullbackPushforwardAdjunctionOfKFlat_counit_fac.The source's hypothesis is just that
fbe a morphism of ringed topoi, andhmosis how that is spelled here, not an extra condition:AlgebraicGeometry.RingedToposSiteHomrecords only the continuity off.u, whileCategoryTheory.Functor.IsMorphismOfSitesis the library's encoding of Stacks 00X1 — continuity together with exactness off^{-1}— and by Stacks 00XC (CategoryTheory.Functor.IsMorphismOfSites.morphismOfTopoi) it is exactlyhmosthat makes the geometric datum offa morphism of topoi. See the implementation notes above for the presentation restriction, which is the repository's convention for ringed topoi and is separate fromhmos.
theorem derivedAdjunction_counit_fac
(K : HomotopyCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
(ComplexShape.up ℤ)) :
(derivedPullback f).map ((derivedPushforwardUnit f).app K) ≫
(derivedAdjunction f hmos).counit.app (DerivedCategory.Qh.obj K) =
(derivedPullbackComparison f).app
((f.pushforwardTopos.mapHomotopyCategory (ComplexShape.up ℤ)).obj K) ≫
DerivedCategory.Qh.map
((homotopyPullbackPushforwardAdjunction f).counit.app K)
Tag 0B6C, a remark
Tag 0B6C in the Stacks Project.
Stacks.Cohomology.RelativeCupProductOnRingedTopoi.relativeCupProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/RelativeCupProduct.lean, line 250. The attribute's comment: “the relative cup product”.
[Stacks, Tag 0B6C]. For a morphism of ringed topoi
f : (Sh(C), O_C) ⟶ (Sh(D), O_D)and objectsK,LofD(O_C), the canonical relative cup product
Rf_*K ⊗^L_{O_D} Rf_*L ⟶ Rf_*(K ⊗^L_{O_C} L),with no further hypothesis. It is the map adjoint, for the adjunction
Lf^* ⊣ Rf_*of [Stacks, Tag 07A6], to the bifunctorial identificationLf^*(Rf_*K ⊗^L Rf_*L) ≅ Lf^*Rf_*K ⊗^L Lf^*Rf_*Lof [Stacks, Tag 07A4] followed by the counitLf^*Rf_* ⟶ idin each of the two factors.
def relativeCupProduct
(K L : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
((derivedTensorProductFunctor Y.O).obj ((derivedPushforward f).obj K)).obj
((derivedPushforward f).obj L) ⟶
(derivedPushforward f).obj (((derivedTensorProductFunctor X.O).obj K).obj L)
Stacks.Cohomology.RelativeCupProductOnRingedTopoi.relativeCupProduct_naturality_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/RelativeCupProduct.lean, line 278. The attribute's comment: “naturality in the first object”.
Naturality of the relative cup product of [Stacks, Tag 0B6C] in the first object.
theorem relativeCupProduct_naturality_left
{K K' : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))}
(k : K ⟶ K')
(L : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
((derivedTensorProductFunctor Y.O).map ((derivedPushforward f).map k)).app
((derivedPushforward f).obj L) ≫
relativeCupProduct f hmos K' L =
relativeCupProduct f hmos K L ≫
(derivedPushforward f).map (((derivedTensorProductFunctor X.O).map k).app L)
Stacks.Cohomology.RelativeCupProductOnRingedTopoi.relativeCupProduct_naturality_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/RelativeCupProduct.lean, line 293. The attribute's comment: “naturality in the second object”.
Naturality of the relative cup product of [Stacks, Tag 0B6C] in the second object.
theorem relativeCupProduct_naturality_right
(K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
{L L' : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))}
(l : L ⟶ L') :
((derivedTensorProductFunctor Y.O).obj ((derivedPushforward f).obj K)).map
((derivedPushforward f).map l) ≫
relativeCupProduct f hmos K L' =
relativeCupProduct f hmos K L ≫
(derivedPushforward f).map (((derivedTensorProductFunctor X.O).obj K).map l)
Stacks.Cohomology.RelativeCupProductOfToposHom.relativeCupProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/RelativeCupProductOfToposHom.lean, line 116. The attribute's comment: “the relative cup product, for a morphism of ringed topoi in the two-field sense of Tag 01D3, part (2) -- a morphism of the underlying topoi together with the structure map, with no continuous functor between the underlying sites and no morphism-of-sites hypothesis”.
For a morphism of ringed topoi
f : (Sh(C), 𝒪_C) ⟶ (Sh(D), 𝒪_D)— a morphism of the underlying topoi together with the structure map, with no functor between the underlying sites — and objectsK,LofD(𝒪_C), the relative cup product
Rf_*K ⊗^L_{𝒪_D} Rf_*L ⟶ Rf_*(K ⊗^L_{𝒪_C} L).It is the map adjoint, for the adjunction
Lf^* ⊣ Rf_*of [Stacks, Tag 07A6], to the identificationLf^*(Rf_*K ⊗^L Rf_*L) ≅ Lf^*Rf_*K ⊗^L Lf^*Rf_*Lof [Stacks, Tag 07A4] followed by the counitLf^*Rf_* ⟶ idin each of the two factors.
def relativeCupProduct
(K L : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
((derivedTensorProductFunctor Y.O).obj ((derivedPushforward f).obj K)).obj
((derivedPushforward f).obj L) ⟶
(derivedPushforward f).obj (((derivedTensorProductFunctor X.O).obj K).obj L)
Tag 0DD7, a lemma
Tag 0DD7 in the Stacks Project.
Stacks.Torsion.torsionSheafProperty_isSerreClass, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Torsion/DerivedCategoryOfTorsionSheaves.lean, line 566. The attribute's comment: “Serre subcategory”.
Torsion abelian sheaves form a Serre subcategory.
public instance torsionSheafProperty_isSerreClass :
(torsionSheafProperty J).IsSerreClass
Stacks.Torsion.exists_torsionDerivedEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Torsion/DerivedCategoryOfTorsionSheaves.lean, line 1118. The attribute's comment: “derived equivalence”.
Stacks 0DD7. The derived category of torsion abelian sheaves is equivalent to the full subcategory of the derived category of all abelian sheaves consisting of objects with torsion cohomology. Under this equivalence, the inclusion is the derived functor of the inclusion of torsion sheaves.
public theorem exists_torsionDerivedEquivalence :
∃ e : DerivedCategory (TorsionSheaf J) ≌ TorsionDerivedCategory J,
Nonempty (e.functor ⋙ (torsionCohomologyProperty J).ι ≅
(torsionSheafProperty J).ι.mapDerivedCategory)
Sources
Section21.20 Some properties of K-injective complexes#
Section 21.20 of the Stacks Project, Tag 08FH. 11 tags here are carried by 20 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 08FI, a lemma
Tag 08FI in the Stacks Project.
Stacks.Cohomology.Localization.isKInjective_overMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Localization/KInjectiveRestrictionAlongOverMap.lean, line 118. The attribute's comment: “for the restriction between two slices, along Over.map”.
Stacks 08FI for the slice-to-slice restriction. Restriction of sheaves of modules along
Over.map f, for an arrowf : V ⟶ Uof the site, carries K-injective complexes to K-injective complexes.Restriction along
Over.map fis restriction to the slice ofC/UatOver.mk ffollowed by the transport of that iterated slice toC/V. The first preserves K-injectivity by the library's form of Stacks 08FI forSheafOfModules.overFunctor, extension by zero being an exact left adjoint of it, and the second byisKInjective_sliceBackward.
theorem isKInjective_overMap
(I : CochainComplex (SheafOfModules.{u} (O.over U)) ℤ) [I.IsKInjective] :
CochainComplex.IsKInjective
((((_root_.SheafOfModules.overMap.{u} O f)).mapHomologicalComplex
(ComplexShape.up ℤ)).obj I)
Stacks.Cohomology.Localization.isKInjective_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Localization/RestrictionOfModules.lean, line 111.
Stacks 08FI. Restriction to the slice site over an object preserves K-injective complexes of sheaves of modules. Extension by zero is an exact left adjoint of the restriction, so the adjoint criterion for K-injectivity applies.
theorem isKInjective_over {C : Type u} [Category.{u} C]
(J : GrothendieckTopology C) (R : Sheaf J RingCat.{u}) (U : C)
(I : CochainComplex (SheafOfModules.{u} R) ℤ) [I.IsKInjective] :
CochainComplex.IsKInjective
(((SheafOfModules.overFunctor.{u} R U).mapHomologicalComplex
(ComplexShape.up ℤ)).obj I)
Tag 0D6F, a lemma
Tag 0D6F in the Stacks Project.
Stacks.Cohomology.Localization.cohomologyOverObjectIsoRestriction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Localization/RestrictionOfModules.lean, line 364.
Cohomology over
Uagrees naturally with cohomology of the restricted derived module on the slice siteC/U.
noncomputable def cohomologyOverObjectIsoRestriction
(X : RingedSite.{u, u, u}) (U : X.C)
[HasDerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))]
[HasDerivedCategory (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U))]
[HasDerivedCategory AddCommGrpCat.{u}] (p : ℤ) :
derivedSectionsOverObject X U ⋙ DerivedCategory.homologyFunctor AddCommGrpCat.{u} p ≅
derivedRestriction X U ⋙ derivedSectionsOnSlice X U ⋙
DerivedCategory.homologyFunctor AddCommGrpCat.{u} p
Tag 0BKV, a lemma
Tag 0BKV in the Stacks Project.
Stacks.Cohomology.SiteCohomologyPresheaf.sheafificationCohomologyPresheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedSections/SheafificationOfTheCohomologyPresheaf.lean, line 293. The attribute's comment: “associated sheaf”.
Sheafifying the presheaf
U ↦ H^q(U, K)gives theq-th cohomology sheaf ofK, naturally in the derived objectK.
def sheafificationCohomologyPresheafIso (q : ℤ) :
derivedSectionsPresheaf X ⋙
DerivedCategory.homologyFunctor (PresheafOfModules.{w}
(Stacks.SheafOfModules.Tensor.ringSheaf X.O).obj) q ⋙
PresheafOfModules.sheafification (𝟙 (Stacks.SheafOfModules.Tensor.ringSheaf X.O).obj) ≅
DerivedCategory.homologyFunctor (SheafOfModules.{w}
(Stacks.SheafOfModules.Tensor.ringSheaf X.O)) q
Stacks.Cohomology.SiteCohomologyPresheaf.sheafificationCohomologyPresheafIso_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedSections/SheafificationOfTheCohomologyPresheaf.lean, line 320. The attribute's comment: “canonical comparison”.
Characterization of the associated-sheaf isomorphism: on a complex, it agrees with the canonical exact-sheafification comparison after the unit of the total right derived presheaf-sections functor.
theorem sheafificationCohomologyPresheafIso_comp (q : ℤ)
(I : HomotopyCategory (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
(.up ℤ)) :
(DerivedCategory.homologyFunctor (PresheafOfModules.{w}
(Stacks.SheafOfModules.Tensor.ringSheaf X.O).obj) q ⋙
PresheafOfModules.sheafification (𝟙 (Stacks.SheafOfModules.Tensor.ringSheaf X.O).obj)).map
(((homotopySectionsPresheaf X).totalRightDerivedUnit DerivedCategory.Qh
(HomotopyCategory.quasiIso (SheafOfModules.{w}
(Stacks.SheafOfModules.Tensor.ringSheaf X.O)) (.up ℤ))).app I) ≫
(sheafificationCohomologyPresheafIso X q).hom.app (DerivedCategory.Qh.obj I) =
(homotopySheafificationHomologyIso X q).hom.app I ≫
(DerivedCategory.homologyFunctorFactorsh
(SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) q).inv.app I
Stacks.Cohomology.SiteCohomologyPresheaf.cohomologyPresheafEvaluationIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedSections/SheafificationOfTheCohomologyPresheaf.lean, line 402. The attribute's comment: “values on objects”.
Evaluation of the hypercohomology presheaf at
Uis the established cohomology functorH^q(U, -).
public def cohomologyPresheafEvaluationIso (X : RingedSite.{u, u, u}) (U : X.C) (q : ℤ) :
derivedSectionsPresheaf X ⋙
DerivedCategory.homologyFunctor (PresheafOfModules.{u}
(Stacks.SheafOfModules.Tensor.ringSheaf X.O).obj) q ⋙
PresheafOfModules.evaluation (Stacks.SheafOfModules.Tensor.ringSheaf X.O).obj
(Opposite.op U) ⋙
forget₂ (ModuleCat.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).obj.obj
(Opposite.op U))) AddCommGrpCat.{u} ≅
derivedSectionsOverObject X U ⋙
DerivedCategory.homologyFunctor AddCommGrpCat.{u} q
Stacks.Cohomology.SiteCohomologyPresheaf.cohomologyPresheafEvaluationIso_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedSections/SheafificationOfTheCohomologyPresheaf.lean, line 435. The attribute's comment: “restriction maps”.
The evaluation identifications commute with the restriction maps.
public theorem cohomologyPresheafEvaluationIso_naturality (X : RingedSite.{u, u, u})
{U V : X.C} (g : U ⟶ V)
(K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
(q : ℤ) :
(cohomologyPresheaf X K q).presheaf.map g.op ≫
(cohomologyPresheafEvaluationIso X U q).hom.app K =
(cohomologyPresheafEvaluationIso X V q).hom.app K ≫
(hypercohomologyRestriction X g q).app K
Stacks.Cohomology.SiteCohomologyPresheaf.cohomologyPresheafSliceIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedSections/SheafificationOfTheCohomologyPresheaf.lean, line 497. The attribute's comment: “cohomology on the slice site”.
The same evaluation, expressed using cohomology on the localized site
C/U; its second factor is the comparison of Tag 0D6F.
public def cohomologyPresheafSliceIso (X : RingedSite.{u, u, u}) (U : X.C) (q : ℤ) :
derivedSectionsPresheaf X ⋙
DerivedCategory.homologyFunctor (PresheafOfModules.{u}
(Stacks.SheafOfModules.Tensor.ringSheaf X.O).obj) q ⋙
PresheafOfModules.evaluation (Stacks.SheafOfModules.Tensor.ringSheaf X.O).obj
(Opposite.op U) ⋙
forget₂ (ModuleCat.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).obj.obj
(Opposite.op U))) AddCommGrpCat.{u} ≅
derivedRestriction X U ⋙ derivedSectionsOnSlice X U ⋙
DerivedCategory.homologyFunctor AddCommGrpCat.{u} q
Tag 0D6G, a lemma
Tag 0D6G in the Stacks Project.
Stacks.Cohomology.Localization.derivedPushforwardOverFunctorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Localization/DerivedDirectImageAndRestriction.lean, line 377.
Stacks 0D6G. For a morphism of ringed sites
f : (C, O_C) ⟶ (D, O_D)given by the continuous functoru : D ⥤ C, an objectVofDandU = u(V), restricting the unbounded derived direct imageRf_*to the localized siteD/Vis the derived direct imageRg_*along the localized morphismg : (C/U, O_U) ⟶ (D/V, O_V)of Stacks 04J0 of the restriction toC/U.
noncomputable def derivedPushforwardOverFunctorIso :
derivedPushforward.{u} f.toRingedToposSiteHom ⋙ derivedRestriction Y V ≅
derivedRestriction X (f.u.obj V) ⋙ derivedLocalizedPushforward f V
Tag 0D6H, a lemma
Tag 0D6H in the Stacks Project.
Stacks.Cohomology.LerayUnbounded.derivedGlobalSectionsPushforwardIsoGeneral, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPushforward/LerayForUnboundedGlobalSectionsGeneral.lean, line 282. The attribute's comment: “the clause on global sections, as functors into the derived category of modules over the global sections of the structure sheaf of the target, for an arbitrary morphism of ringed sites; the clause on sections over an object of the target site is derivedSectionsOverObjectPushforwardIsoGeneral”.
Stacks 0D6H, the global-sections clause, for an arbitrary morphism of ringed sites. Let
f : (C, O_C) ⟶ (D, O_D)be a morphism of ringed sites given by the continuous functoru : D ⥤ C. ThenRΓ(D, -) ∘ Rf_* = RΓ(C, -)as functorsD(O_C) ⟶ D(Γ(O_D)), the right hand side being the derived global sections onCwith scalars restricted along the induced ring mapΓ(O_D) ⟶ Γ(O_C).No flatness: this is
derivedGlobalSectionsPushforwardIsowith its hypothesis discharged bycomputesSecond_pushforwardTopos_globalSections. The source's other clause, the one on sections over an object ofD, isStacks.Cohomology.LerayUnbounded.derivedSectionsOverObjectPushforwardIsoGeneral.
noncomputable def derivedGlobalSectionsPushforwardIsoGeneral :
derivedPushforward.{u} f.toRingedToposSiteHom ⋙ derivedGlobalSections Y ≅
derivedGlobalSectionsRestricted f
Stacks.Cohomology.LerayUnbounded.derivedSectionsOverObjectPushforwardIsoGeneral, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPushforward/LerayForUnboundedSectionsGeneral.lean, line 256. The attribute's comment: “the clause on sections over an object of the target site, for an arbitrary morphism of ringed sites; the clause on global sections into the derived category of modules over the global sections of the structure sheaf of the target is derivedGlobalSectionsPushforwardIsoGeneral”.
Stacks 0D6H, the clause on sections over an object, for an arbitrary morphism of ringed sites. Let
f : (C, O_C) ⟶ (D, O_D)be a morphism of ringed sites given by the continuous functoru : D ⥤ C, letVbe an object ofDand putU = u(V). ThenRΓ(V, -) ∘ Rf_* = RΓ(U, -)as functorsD(O_C) ⟶ D(Ab).No flatness: this is
derivedSectionsOverObjectPushforwardIsowith its hypothesis discharged bycomputesSecond_pushforwardTopos_sectionsOverObject. The source's other clause, the one about global sections intoD(Γ(O_D)), isStacks.Cohomology.LerayUnbounded.derivedGlobalSectionsPushforwardIsoGeneral.
noncomputable def derivedSectionsOverObjectPushforwardIsoGeneral :
derivedPushforward.{u} f.toRingedToposSiteHom ⋙ derivedSectionsOverObject Y V ≅
derivedSectionsOverObject X (f.u.obj V)
Stacks.Cohomology.Localization.derivedGlobalSectionsOverPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Localization/LerayForTheSliceMorphism.lean, line 140. The attribute's comment: “the clause RGamma(V, -) . Rf_* = RGamma(U, -) on sections over an object, for ABELIAN sheaves and for the SLICE morphism of topoi Sh(C/X) -> Sh(C/Y) of a morphism f : X -> Y of the site, at the final object V = id Y of C/Y, where u = Over.pullback f and u(V) = id X. Unconditional: no analogue of the h093Y K-injectivity hypothesis, nor of the flatness, of Stacks.Cohomology.LerayUnbounded.derivedSectionsOverObjectPushforwardIso and ...IsoOfFlat, which carry this tag for sheaves of MODULES on ringed sites. Assumed instead is Limits.HasPullbacksAlong f, base change of the single morphism f, used only to present f_* as restriction along Over.pullback f. NOT covered: the clause on global sections into D(Gamma(O_D)) for a general morphism of ringed sites, and sections over a non-final object of C/Y”.
Stacks 0D6H for the slice morphism, on abelian sheaves. For a morphism
f : X ⟶ Yof a siteC, the unbounded derived global sections onC/Yof the unbounded derived direct image alongfare the unbounded derived global sections onC/X:RΓ(Y, -) ∘ Rf_* ≅ RΓ(X, -).Both sides are total right derived functors of one and the same functor on the unbounded homotopy category of abelian sheaves on
C/X, byoverPushforwardGlobalSectionsIso; the comparison forRf_*is invertible on a K-injective complex, and the comparison forRΓ(Y, -)is invertible atf_*I, which is again K-injective byoverPushforward_map_isKInjective. Uniqueness of right derived functors then identifies the two, which isStacks.Cohomology.LerayUnbounded.derivedCompIso.
def derivedGlobalSectionsOverPushforwardIso {X Y : C} (f : X ⟶ Y) [HasPullbacksAlong f] :
DerivedFunctor.totalRightDerived (overPushforward J f) ⋙
DerivedFunctor.totalRightDerived
((sheafSections (J.over Y) Ab.{max u v}).obj (op (Over.mk (𝟙 Y)))) ≅
DerivedFunctor.totalRightDerived
((sheafSections (J.over X) Ab.{max u v}).obj (op (Over.mk (𝟙 X))))
Tag 0D6I, a lemma
Tag 0D6I in the Stacks Project.
Stacks.Cohomology.UnboundedHigherDirectImageOnSites.cohomologySheavesOfTheDerivedDirectImage, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPushforward/CohomologySheavesOfTheDerivedDirectImageUnconditional.lean, line 160. The attribute's comment: “the i-th cohomology sheaf of Rf_K is the sheaf associated to the presheaf V ↦ H^i(u(V), K) = H^i(V, Rf_K), naturally in K, for an arbitrary morphism of ringed sites: the associated-sheaf clause and both readings of the value of the presheaf on an object”.
Stacks 0D6I. Let
f : (C, O_C) ⟶ (D, O_D)be a morphism of ringed sites corresponding to the continuous functoru : D ⥤ Cand leti : ℤ. Then thei-th cohomology sheaf ofRf_* Kis the sheaf associated to the presheaf
V ↦ H^i(u(V), K) = H^i(V, Rf_* K),naturally in the object
KofD(O_C).The presheaf is
derivedPushforwardCohomologyPresheaf, which carries its restriction maps, and the three components are the three assertions the source makes about it: that its sheafification is the cohomology sheaf ofRf_* K, and that its value onVisH^i(u(V), K)and isH^i(V, Rf_* K)— the two sides of the source's displayed equality, whose compositeH^i(u(V), K) ≅ H^i(V, Rf_* K)iscohomologyOverObjectPushforwardIsoGeneral.Everything is stated as an isomorphism of functors on
D(O_C), so the naturality inKthat the source leaves implicit is part of the statement. There is no hypothesis beyond the source's: the sheafification clause is Stacks 0BKV on the target site composed withRf_*, and the displayed equality isH^iof the clause of Stacks 0D6H on sections over an object, whichStacks.Cohomology.LerayUnbounded.derivedSectionsOverObjectPushforwardIsoGeneralproves for an arbitrary morphism of ringed sites.
def cohomologySheavesOfTheDerivedDirectImage (i : ℤ) :
(derivedPushforward.{u} f.toRingedToposSiteHom ⋙
DerivedCategory.homologyFunctor
(SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) i ≅
derivedPushforward.{u} f.toRingedToposSiteHom ⋙ derivedSectionsPresheaf Y ⋙
DerivedCategory.homologyFunctor
(PresheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O).obj) i ⋙
PresheafOfModules.sheafification (𝟙 (Stacks.SheafOfModules.Tensor.ringSheaf Y.O).obj)) ×
(∀ V : Y.C,
derivedPushforward.{u} f.toRingedToposSiteHom ⋙ derivedSectionsPresheaf Y ⋙
DerivedCategory.homologyFunctor
(PresheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O).obj) i ⋙
PresheafOfModules.evaluation (Stacks.SheafOfModules.Tensor.ringSheaf Y.O).obj
(Opposite.op V) ⋙
forget₂
(ModuleCat.{u}
((Stacks.SheafOfModules.Tensor.ringSheaf Y.O).obj.obj (Opposite.op V)))
AddCommGrpCat.{u} ≅
derivedSectionsOverObject X (f.u.obj V) ⋙
DerivedCategory.homologyFunctor AddCommGrpCat.{u} i) ×
(∀ V : Y.C,
derivedPushforward.{u} f.toRingedToposSiteHom ⋙ derivedSectionsPresheaf Y ⋙
DerivedCategory.homologyFunctor
(PresheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O).obj) i ⋙
PresheafOfModules.evaluation (Stacks.SheafOfModules.Tensor.ringSheaf Y.O).obj
(Opposite.op V) ⋙
forget₂
(ModuleCat.{u}
((Stacks.SheafOfModules.Tensor.ringSheaf Y.O).obj.obj (Opposite.op V)))
AddCommGrpCat.{u} ≅
derivedPushforward.{u} f.toRingedToposSiteHom ⋙ derivedSectionsOverObject Y V ⋙
DerivedCategory.homologyFunctor AddCommGrpCat.{u} i)
Tag 0D6J, a lemma
Tag 0D6J in the Stacks Project.
Stacks.Cohomology.ForgetModule.pushforwardForgetComparison_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPushforward/ForgettingTheModuleStructureForTheDirectImage.lean, line 389. The attribute's comment: “part (3): the unbounded derived direct image along a morphism of ringed sites”.
Stacks 0D6J, part (3). Let
f : (C, O_C) ⟶ (D, O_D)be a morphism of ringed sites. ForKin the unbounded derived categoryD(O_C)the canonical mapRf_*K ⟶ Rf_*(K_ab)from the image inD(Z_D)of the unbounded derived direct image ofKto the unbounded derived direct image of the underlying abelian complex ofKis an isomorphism, naturally inK.
theorem pushforwardForgetComparison_isIso : IsIso (pushforwardForgetComparison f)
Stacks.Cohomology.ForgetModule.sectionsForgetComparison_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedSections/ForgettingTheModuleStructure.lean, line 247. The attribute's comment: “part (2): sections over an object of the site”.
Stacks 0D6J, part (2). For every object
Uof the site, the canonical mapRΓ(U, K) ⟶ RΓ(U, K_ab)from unbounded derived sections of a sheaf of modules to derived sections of the underlying abelian sheaf is an isomorphism, naturally inK.
theorem sectionsForgetComparison_isIso (U : X.C) :
IsIso (sectionsForgetComparison X U)
Stacks.Cohomology.ForgetModule.globalSectionsForgetComparison_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedSections/ForgettingTheModuleStructure.lean, line 362. The attribute's comment: “part (1): global sections of the site”.
Stacks 0D6J, part (1). The canonical map
RΓ(C, K) ⟶ RΓ(C, K_ab)from unbounded derived global sections of a sheaf of modules to derived global sections of the underlying abelian sheaf is an isomorphism, naturally inK.
theorem globalSectionsForgetComparison_isIso :
IsIso (globalSectionsForgetComparison X)
Tag 08FJ, a lemma
Tag 08FJ in the Stacks Project.
Stacks.Cohomology.Localization.derivedExtensionByZeroRestrictionAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Localization/RestrictionOfModules.lean, line 235.
Stacks 08FJ. On the unbounded derived categories of modules over a ringed site, extension by zero along the localization at an object is left adjoint to restriction to the localized site. The adjunction is the canonical one: it is obtained by localizing the degreewise underived adjunction, so its unit and counit are the images of the underived unit and counit under the localization comparisons.
noncomputable def derivedExtensionByZeroRestrictionAdjunction
(X : RingedSite.{u, u, u}) (U : X.C)
[HasDerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))]
[HasDerivedCategory
(SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U))] :
let R := (Stacks.SheafOfModules.Tensor.ringSheaf X.O)
let jShriek := SheafOfModules.pullback.{u}
(F := Over.forget U) (𝟙 (R.over U) : (R.over U) ⟶ (R.over U))
let restriction := SheafOfModules.overFunctor R U
jShriek.mapDerivedCategory ⊣ restriction.mapDerivedCategory
Tag 0GL1, a lemma
Tag 0GL1 in the Stacks Project.
Stacks.DerivedTensor.ExtensionByZero.derivedTensorExtensionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/ExtensionByZeroTensor.lean, line 357.
Stacks 0GL1. Let
(C, O)be a ringed site,Uan object ofCandj_!extension by zero from the localized siteC/U. ForLinD(O_U)andKinD(O),
j_!L ⊗^L_O K = j_!(L ⊗^L_{O_U} K|_U).
def derivedTensorExtensionIso (L : DerivedCategory (Modules (X.O.over U)))
(K : DerivedCategory (Modules X.O)) :
((baseDerivedTensor X).tensor.obj ((extension X U).mapDerivedCategory.obj L)).obj K ≅
(extension X U).mapDerivedCategory.obj
(((sliceDerivedTensor X U).tensor.obj L).obj
((restriction X U).mapDerivedCategory.obj K))
Tag 093Y, a lemma
Tag 093Y in the Stacks Project.
AlgebraicGeometry.RingedToposHom.pushforwardModules_isKInjective_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedSections/FlatRingedToposPushforwardKInjective.lean, line 121. References: SGA 4 V (4.9), “more general”.
Stacks 093Y. Let
(f, f♯) : (Sh(C), O_C) ⟶ (Sh(D), O_D)be a flat morphism of ringed topoi — flat in the sense of Stacks 04JB, that the ring mapf♯ : f⁻¹O_D ⟶ O_Cis flat — and letIbe a K-injective complex ofO_C-modules. Then the degreewise direct imagef_*Iis a K-injective complex ofO_D-modules.The proof is the source's. The adjunction
f^* ⊣ f_*of Stacks 03D7 identifiesHom_{K(O_D)}(F, f_*I)withHom_{K(O_C)}(f^*F, I); flatness makesf^*exact (Stacks 04JC), so it carries an acyclicFto an acyclicf^*F, on which K-injectivity ofImakes every morphism intoInull-homotopic. That is Stacks 08BJ applied to this adjunction.
theorem pushforwardModules_isKInjective_of_isFlat
(f : RingedToposHom X Y) (hf : f.IsFlat)
(I : CochainComplex (SheafOfModules.{w}
(Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ) [I.IsKInjective] :
CochainComplex.IsKInjective
((f.pushforwardModules.mapHomologicalComplex (ComplexShape.up ℤ)).obj I)
Tag 093Z, a lemma
Tag 093Z in the Stacks Project.
Stacks.Sheaves.KInjectiveInternalHom.isKInjective_homSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/InternalHomKInjective.lean, line 60.
Stacks Project, Tag 093Z. Internal Hom from
O'takes K-injective complexes ofO-modules to K-injective complexes ofO'-modules.
theorem isKInjective_homSheaf (φ : O ⟶ O')
(I : CochainComplex (SheafOfModules.{u} O) ℤ) [I.IsKInjective] :
letI := (RingedSpaceModuleAdjunction.restrictScalarsHomAdjunction φ).right_adjoint_additive
CochainComplex.IsKInjective
(((RingedSpaceModuleAdjunction.homSheaf φ).mapHomologicalComplex (.up ℤ)).obj I)
Sources
Section21.21 Localization and cohomology#
Section 21.21 of the Stacks Project, Tag 0EYZ. 2 tags here are carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0EZ0, a lemma
Tag 0EZ0 in the Stacks Project.
Stacks.Cohomology.Localization.derivedOverPushforwardBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Localization/AbelianSheavesOnALocalizedSite.lean, line 682.
Stacks 0EZ0. For a Cartesian square
in a site, inverse image alongX' --a--> X |b |c Y' --d--> Ydafter derived direct image alongcis naturally isomorphic to derived direct image alongbafter inverse image alonga.All four derived functors are arbitrary choices with their canonical transformations from the corresponding functors on homotopy categories.
noncomputable def derivedOverPushforwardBaseChangeIso
(J : GrothendieckTopology C) {X' X Y' Y : C}
(a : X' ⟶ X) (b : X' ⟶ Y') (c : X ⟶ Y) (d : Y' ⟶ Y)
(h : IsPullback a b c d)
[∀ U : C, HasSheafify (J.over U) Ab.{max u v}]
[HasDerivedCategory.{wX} (AbelianSheaves J X)]
[HasDerivedCategory.{wY} (AbelianSheaves J Y)]
[HasDerivedCategory.{wU} (AbelianSheaves J X')]
[HasDerivedCategory.{wV'} (AbelianSheaves J Y')]
(Rc : DerivedCategory (AbelianSheaves J X) ⥤
DerivedCategory (AbelianSheaves J Y))
(Rb : DerivedCategory (AbelianSheaves J X') ⥤
DerivedCategory (AbelianSheaves J Y'))
(Ra : DerivedCategory (AbelianSheaves J X) ⥤
DerivedCategory (AbelianSheaves J X'))
(Rd : DerivedCategory (AbelianSheaves J Y) ⥤
DerivedCategory (AbelianSheaves J Y'))
(αc : homotopyToDerived (overPushforward J c) ⟶ DerivedCategory.Qh ⋙ Rc)
(αb : homotopyToDerived (overPushforward J b) ⟶ DerivedCategory.Qh ⋙ Rb)
(αa : homotopyToDerived (overPullback J a) ⟶ DerivedCategory.Qh ⋙ Ra)
(αd : homotopyToDerived (overPullback J d) ⟶ DerivedCategory.Qh ⋙ Rd)
[Rc.IsRightDerivedFunctor αc
(HomotopyCategory.quasiIso (AbelianSheaves J X) (ComplexShape.up ℤ))]
[Rb.IsRightDerivedFunctor αb
(HomotopyCategory.quasiIso (AbelianSheaves J X') (ComplexShape.up ℤ))]
[Ra.IsRightDerivedFunctor αa
(HomotopyCategory.quasiIso (AbelianSheaves J X) (ComplexShape.up ℤ))]
[Rd.IsRightDerivedFunctor αd
(HomotopyCategory.quasiIso (AbelianSheaves J Y) (ComplexShape.up ℤ))] :
Rc ⋙ Rd ≅ Ra ⋙ Rb
Tag 0FN5, a lemma
Tag 0FN5 in the Stacks Project.
Stacks.Cohomology.Localization.derivedModulesPushforwardBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Localization/DerivedBaseChangeOfModules.lean, line 127.
Stacks 0FN5. For a cartesian square
of a ringed siteX' --a--> X |b |c V V Y' --d--> Y(C, O), the inverse image of sheaves of modules along the relocalization atdafter the derived direct image along the relocalization atcis naturally isomorphic to the derived direct image along the relocalization atbafter the inverse image along the relocalization ata.All four derived functors are arbitrary choices with their canonical transformations from the corresponding functors on homotopy categories.
def derivedModulesPushforwardBaseChangeIso
(a : X' ⟶ X) (b : X' ⟶ Y') (c : X ⟶ Y) (d : Y' ⟶ Y) (hsq : IsPullback a b c d)
[HasDerivedCategory.{wX} (_root_.SheafOfModules.{u} (O.over X))]
[HasDerivedCategory.{wY} (_root_.SheafOfModules.{u} (O.over Y))]
[HasDerivedCategory.{wU} (_root_.SheafOfModules.{u} (O.over X'))]
[HasDerivedCategory.{wV} (_root_.SheafOfModules.{u} (O.over Y'))]
(Rc : DerivedCategory (_root_.SheafOfModules.{u} (O.over X)) ⥤
DerivedCategory (_root_.SheafOfModules.{u} (O.over Y)))
(Rb : DerivedCategory (_root_.SheafOfModules.{u} (O.over X')) ⥤
DerivedCategory (_root_.SheafOfModules.{u} (O.over Y')))
(Ra : DerivedCategory (_root_.SheafOfModules.{u} (O.over X)) ⥤
DerivedCategory (_root_.SheafOfModules.{u} (O.over X')))
(Rd : DerivedCategory (_root_.SheafOfModules.{u} (O.over Y)) ⥤
DerivedCategory (_root_.SheafOfModules.{u} (O.over Y')))
(αc : homotopyToDerived (Stacks.SheafOfModules.Relocalization.pushforward J O c) ⟶
DerivedCategory.Qh ⋙ Rc)
(αb : homotopyToDerived (Stacks.SheafOfModules.Relocalization.pushforward J O b) ⟶
DerivedCategory.Qh ⋙ Rb)
(αa : homotopyToDerived (_root_.SheafOfModules.overMap.{u} O a) ⟶ DerivedCategory.Qh ⋙ Ra)
(αd : homotopyToDerived (_root_.SheafOfModules.overMap.{u} O d) ⟶ DerivedCategory.Qh ⋙ Rd)
[Rc.IsRightDerivedFunctor αc
(HomotopyCategory.quasiIso (_root_.SheafOfModules.{u} (O.over X)) (ComplexShape.up ℤ))]
[Rb.IsRightDerivedFunctor αb
(HomotopyCategory.quasiIso (_root_.SheafOfModules.{u} (O.over X')) (ComplexShape.up ℤ))]
[Ra.IsRightDerivedFunctor αa
(HomotopyCategory.quasiIso (_root_.SheafOfModules.{u} (O.over X)) (ComplexShape.up ℤ))]
[Rd.IsRightDerivedFunctor αd
(HomotopyCategory.quasiIso (_root_.SheafOfModules.{u} (O.over Y)) (ComplexShape.up ℤ))] :
Rc ⋙ Rd ≅ Ra ⋙ Rb
Sources
Section21.22 Inverse systems and cohomology#
Section 21.22 of the Stacks Project, Tag 0GYP. 4 tags here are carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0GYQ, a lemma
Tag 0GYQ in the Stacks Project.
Stacks.Cohomology.AdicInverseSystems.exists_uniform_stable_image, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InverseSystems/AdicQuotientSystems/MittagLeffler.lean, line 274. The attribute's comment: “the uniform shift of the footnote”. References: SGA 2 IX (2.1), “(iii)”.
Stacks Project, Tag 0GYQ, the footnote: the images of
Hᵖ(C, F_k) → Hᵖ(C, Fᵢ)are the stable image already atk = i + c, for onecindependent ofi.
theorem exists_uniform_stable_image (hacc : WellFoundedGT (GradedSubmodule hF p)) :
∃ c : ℕ, ∀ i k : ℕ, ∀ h : i + c ≤ k,
transitionImage (F ⋙ globalModuleCohomology.{u, v, r, w} O p) i k (by omega) =
transitionImage (F ⋙ globalModuleCohomology.{u, v, r, w} O p) i (i + c) (by omega)
Stacks.Cohomology.AdicInverseSystems.isMittagLefflerCategorical_cohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InverseSystems/AdicQuotientSystems/MittagLeffler.lean, line 308.
Stacks Project, Tag 0GYQ. For an inverse system of sheaves of modules on a site with
Fₙ = Fₙ₊₁/IⁿFₙ₊₁, the ascending chain condition on the graded submodules of⨁ₙ H^(p+1)(C, IⁿFₙ₊₁)implies that the inverse systemn ↦ Hᵖ(C, Fₙ)satisfies the Mittag-Leffler condition.
theorem isMittagLefflerCategorical_cohomology (hacc : WellFoundedGT (GradedSubmodule hF p)) :
IsMittagLefflerCategorical (F ⋙ globalModuleCohomology.{u, v, r, w} O p)
Tag 0GYR, a lemma
Tag 0GYR in the Stacks Project.
Stacks.Cohomology.AdicInverseSystems.isMittagLefflerCategorical_cohomology_of_stableImages, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InverseSystems/AdicQuotientSystems/StableImages.lean, line 165.
Stacks Project, Tag 0GYR. For an inverse system of sheaves of modules on a site with
Fₙ = Fₙ₊₁/IⁿFₙ₊₁, the ascending chain condition on the graded submodules of⨁ₙ Nₙ, whereNₙ = ⋂_{m ≥ n} Im(H^(p+1)(C, IⁿF_m) → H^(p+1)(C, IⁿFₙ)), implies that the inverse systemn ↦ Hᵖ(C, Fₙ)satisfies the Mittag-Leffler condition.
theorem isMittagLefflerCategorical_cohomology_of_stableImages
(hacc : WellFoundedGT (StableGradedSubmodule hF p)) :
IsMittagLefflerCategorical (F ⋙ globalModuleCohomology.{u, v, r, w} O p)
Tag 0GYS, a lemma
Tag 0GYS in the Stacks Project.
Stacks.Cohomology.AdicInverseSystems.limitTopology_eq_adicModuleTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InverseSystems/AdicQuotientSystems/LimitTopology.lean, line 543.
Stacks Project, Tag 0GYS. For an inverse system of sheaves of modules on a site with
Fₙ = Fₙ₊₁/IⁿFₙ₊₁, the ascending chain condition on⨁ₙ Hᵖ(C, IⁿFₙ₊₁)as a graded⨁ₙ Iⁿ/Iⁿ⁺¹-module implies that the limit topology onlim Hᵖ(C, Fₙ)is theI-adic topology.
theorem limitTopology_eq_adicModuleTopology (hF : IsAdicQuotientSystem O I F) (p : ℕ)
(hACC : HasGradedACC O I F hF p) :
Stacks.AdicLimit.towerLimit.limitTopology
(fun n => ((cohomologySystem O F p).obj (op n) : Type _))
(cohomologyTransition O F p) =
I.adicModuleTopology (cohomologyLimit O F p)
Tag 0GYT, a lemma
Tag 0GYT in the Stacks Project.
Stacks.Cohomology.AdicInverseSystems.limitTopology_eq_adicModuleTopology_of_stableImages, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InverseSystems/AdicQuotientSystems/StableImages.lean, line 367.
Stacks Project, Tag 0GYT. For an inverse system of sheaves of modules on a site with
Fₙ = Fₙ₊₁/IⁿFₙ₊₁, the ascending chain condition on⨁ₙ Nₙas a graded⨁ₙ Iⁿ/Iⁿ⁺¹-module, whereNₙ = ⋂_{m ≥ n} Im(Hᵖ(C, IⁿF_m) → Hᵖ(C, IⁿFₙ)), implies that the limit topology onlim Hᵖ(C, Fₙ)is theI-adic topology.
theorem limitTopology_eq_adicModuleTopology_of_stableImages
(hF : IsAdicQuotientSystem O I F) (p : ℕ) (hACC : HasStableGradedACC O I F hF p) :
Stacks.AdicLimit.towerLimit.limitTopology
(fun n => ((cohomologySystem O F p).obj (op n) : Type _))
(cohomologyTransition O F p) =
I.adicModuleTopology (cohomologyLimit O F p)
Sources
Section21.23 Derived and homotopy limits#
Section 21.23 of the Stacks Project, Tag 0940. 12 tags here are carried by 22 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0941, a lemma
Tag 0941 in the Stacks Project.
Stacks.Cohomology.exists_rightDerivedLimit_isDerivedLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Recovery21/DerivedLimitsOfInverseSystems.lean, line 375.
Stacks Project Tag 0941. The value of the right derived functor of ordinary inverse limit at
Kexists and is a derived limit of the tower of the derived evaluationsKₙ.
theorem exists_rightDerivedLimit_isDerivedLimit
[IsGrothendieckAbelian.{wG} A]
[HasLimitsOfShape ℕᵒᵖ A]
(K : DerivedCategory (ℕᵒᵖ ⥤ A)) :
∃ (h : HasProduct fun n : ℕ => (derivedEvaluationTower K).obj ⟨n⟩),
∃ c : Cocone
(MorphismProperty.Under.forget
(HomotopyCategory.quasiIso (ℕᵒᵖ ⥤ A) (ComplexShape.up ℤ)) ⊤
(DerivedCategory.Qh.objPreimage K) ⋙
Under.forget (DerivedCategory.Qh.objPreimage K) ⋙
((lim : (ℕᵒᵖ ⥤ A) ⥤ A).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
DerivedCategory.Qh)),
(((lim : (ℕᵒᵖ ⥤ A) ⥤ A).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
DerivedCategory.Qh).IsRightDerivedValueAt
(HomotopyCategory.quasiIso (ℕᵒᵖ ⥤ A) (ComplexShape.up ℤ))
(DerivedCategory.Qh.objPreimage K) c) ∧
@IsDerivedLimit (DerivedCategory A) _ _ _ _ _ _
(derivedEvaluationTower K) h c.pt
Tag 0D6K, a lemma
Tag 0D6K in the Stacks Project.
Stacks.Cohomology.DerivedGlobalSections.isDerivedLimit_map_derivedGlobalSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedLimit/DerivedGlobalSectionsUnbounded.lean, line 114. The attribute's comment: “global derived sections commute with derived limits”.
Stacks Project, Tag 0D6K.
RΓ(C, -)commutes withRlim: global derived sections of a ringed site carry a derived inverse limit to a derived inverse limit.
public theorem isDerivedLimit_map_derivedGlobalSections
(K : ℕᵒᵖ ⥤ DerivedCategory
(SheafOfModules.{max u v w z} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
[HasProduct fun n : ℕ ↦ K.obj ⟨n⟩]
(L : DerivedCategory
(SheafOfModules.{max u v w z} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
(hL : IsDerivedLimit K L) :
∃ h : HasProduct (fun n : ℕ ↦ (derivedGlobalSections.{u, v, w, z} X).obj (K.obj ⟨n⟩)),
@IsDerivedLimit
(DerivedCategory (ModuleCat.{max u v w z}
(RingCat.sectionsSubring (Stacks.SheafOfModules.Tensor.ringSheaf X.O).obj)))
_ _ _ _ _ _ (K ⋙ derivedGlobalSections.{u, v, w, z} X) h
((derivedGlobalSections.{u, v, w, z} X).obj L)
Stacks.Cohomology.DerivedGlobalSections.exists_shortExact_limOne_cohomology_derivedGlobalSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedLimit/DerivedGlobalSectionsUnbounded.lean, line 136. The attribute's comment: “short exact sequence over the whole site”.
Stacks Project, Tag 0D6K. The canonical Milnor short exact sequence for the cohomology of the whole ringed site: the first derived inverse limit of the degree-
m - 1cohomologies includes into the degree-mcohomology ofRΓ(C, Rlim Kₙ), with quotient the inverse limit of the degree-mcohomologies.
public theorem exists_shortExact_limOne_cohomology_derivedGlobalSections
(K : ℕᵒᵖ ⥤ DerivedCategory
(SheafOfModules.{max u v w z} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
(L : DerivedCategory
(SheafOfModules.{max u v w z} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
[HasProduct fun n : ℕ ↦ K.obj ⟨n⟩]
(p : L ⟶ ∏ᶜ fun n : ℕ ↦ K.obj ⟨n⟩)
(hL : ∃ δ : (∏ᶜ fun n : ℕ ↦ K.obj ⟨n⟩) ⟶ L⟦(1 : ℤ)⟧,
Triangle.mk p (Pi.lift fun n : ℕ ↦
Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) n -
Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) (n + 1) ≫
K.map (homOfLE (Nat.le_succ n)).op) δ ∈
distTriang (DerivedCategory
(SheafOfModules.{max u v w z} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))))
(m : ℤ) :
let RGamma := derivedGlobalSections.{u, v, w, z} X
let A := ModuleCat.{max u v w z}
(RingCat.sectionsSubring (Stacks.SheafOfModules.Tensor.ringSheaf X.O).obj)
let Hprev := DerivedCategory.homologyFunctor A (m - 1)
let Hcur := DerivedCategory.homologyFunctor A m
let Fprev := K ⋙ RGamma ⋙ Hprev
let Fcur := K ⋙ RGamma ⋙ Hcur
let E := K ⋙ RGamma
let dprev : (∏ᶜ fun n : ℕ ↦ Fprev.obj ⟨n⟩) ⟶
(∏ᶜ fun n : ℕ ↦ Fprev.obj ⟨n⟩) := Pi.lift fun n : ℕ ↦
Pi.π (fun n : ℕ ↦ Fprev.obj ⟨n⟩) n -
Pi.π (fun n : ℕ ↦ Fprev.obj ⟨n⟩) (n + 1) ≫
Fprev.map (homOfLE (Nat.le_succ n)).op
∃ (h : HasProduct fun n : ℕ ↦ E.obj ⟨n⟩),
letI := h
∃ (a : RGamma.obj L ⟶ ∏ᶜ fun n : ℕ ↦ E.obj ⟨n⟩)
(b : (∏ᶜ fun n : ℕ ↦ E.obj ⟨n⟩) ⟶ (RGamma.obj L)⟦(1 : ℤ)⟧),
let T := Triangle.mk a (Pi.lift fun n : ℕ ↦
Pi.π (fun n : ℕ ↦ E.obj ⟨n⟩) n -
Pi.π (fun n : ℕ ↦ E.obj ⟨n⟩) (n + 1) ≫
E.map (homOfLE (Nat.le_succ n)).op) b
T ∈ distTriang (DerivedCategory A) ∧
(∀ n : ℕ, a ≫ Pi.π (fun n : ℕ ↦ E.obj ⟨n⟩) n =
RGamma.map (p ≫ Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) n)) ∧
∃ (ePrev : Hprev.obj (∏ᶜ fun n : ℕ ↦ E.obj ⟨n⟩) ≅
∏ᶜ fun n : ℕ ↦ Fprev.obj ⟨n⟩)
(i : cokernel dprev ⟶ Hcur.obj (RGamma.obj L))
(q : Hcur.obj (RGamma.obj L) ⟶ limit Fcur)
(zero : i ≫ q = 0),
(ePrev.hom = piComparison Hprev (fun n : ℕ ↦ E.obj ⟨n⟩) ∧
cokernel.π dprev ≫ i =
ePrev.inv ≫ (DerivedCategory.homologyFunctor A 0).homologySequenceδ
T (m - 1) m (by omega) ∧
(ShortComplex.mk i q zero).ShortExact ∧
∀ n : ℕ, q ≫ limit.π Fcur ⟨n⟩ =
Hcur.map (RGamma.map (p ≫ Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) n)))
Stacks.Cohomology.DerivedGlobalSections.isDerivedLimit_map_derivedSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedLimit/DerivedGlobalSectionsUnbounded.lean, line 239. The attribute's comment: “derived sections over an object commute with derived limits”.
Stacks Project, Tag 0D6K.
RΓ(U, -)commutes withRlim: derived sections over an object of a ringed site carry a derived inverse limit to a derived inverse limit.
public theorem isDerivedLimit_map_derivedSections
(K : ℕᵒᵖ ⥤ DerivedCategory
(SheafOfModules.{max u v w z} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
[HasProduct fun n : ℕ ↦ K.obj ⟨n⟩]
(L : DerivedCategory
(SheafOfModules.{max u v w z} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
(hL : IsDerivedLimit K L) :
∃ h : HasProduct (fun n : ℕ ↦ (derivedSections.{u, v, w, z} X U).obj (K.obj ⟨n⟩)),
@IsDerivedLimit
(DerivedCategory
(ModuleCat.{max u v w z} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).obj.obj U)))
_ _ _ _ _ _ (K ⋙ derivedSections.{u, v, w, z} X U) h
((derivedSections.{u, v, w, z} X U).obj L)
Stacks.Cohomology.DerivedGlobalSections.exists_shortExact_limOne_cohomology_derivedSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedLimit/DerivedGlobalSectionsUnbounded.lean, line 265. The attribute's comment: “short exact sequence over an object”.
Stacks Project, Tag 0D6K. The canonical Milnor short exact sequence for the cohomology over an object
Uof a ringed site: the first derived inverse limit of the degree-m - 1cohomologies includes into the degree-mcohomology ofRΓ(U, Rlim Kₙ), with quotient the inverse limit of the degree-mcohomologies.
public theorem exists_shortExact_limOne_cohomology_derivedSections
(K : ℕᵒᵖ ⥤ DerivedCategory
(SheafOfModules.{max u v w z} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
(L : DerivedCategory
(SheafOfModules.{max u v w z} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
[HasProduct fun n : ℕ ↦ K.obj ⟨n⟩]
(p : L ⟶ ∏ᶜ fun n : ℕ ↦ K.obj ⟨n⟩)
(hL : ∃ δ : (∏ᶜ fun n : ℕ ↦ K.obj ⟨n⟩) ⟶ L⟦(1 : ℤ)⟧,
Triangle.mk p (Pi.lift fun n : ℕ ↦
Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) n -
Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) (n + 1) ≫
K.map (homOfLE (Nat.le_succ n)).op) δ ∈
distTriang (DerivedCategory
(SheafOfModules.{max u v w z} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))))
(m : ℤ) :
let RGamma := derivedSections.{u, v, w, z} X U
let A := ModuleCat.{max u v w z} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).obj.obj U)
let Hprev := DerivedCategory.homologyFunctor A (m - 1)
let Hcur := DerivedCategory.homologyFunctor A m
let Fprev := K ⋙ RGamma ⋙ Hprev
let Fcur := K ⋙ RGamma ⋙ Hcur
let E := K ⋙ RGamma
let dprev : (∏ᶜ fun n : ℕ ↦ Fprev.obj ⟨n⟩) ⟶
(∏ᶜ fun n : ℕ ↦ Fprev.obj ⟨n⟩) := Pi.lift fun n : ℕ ↦
Pi.π (fun n : ℕ ↦ Fprev.obj ⟨n⟩) n -
Pi.π (fun n : ℕ ↦ Fprev.obj ⟨n⟩) (n + 1) ≫
Fprev.map (homOfLE (Nat.le_succ n)).op
∃ (h : HasProduct fun n : ℕ ↦ E.obj ⟨n⟩),
letI := h
∃ (a : RGamma.obj L ⟶ ∏ᶜ fun n : ℕ ↦ E.obj ⟨n⟩)
(b : (∏ᶜ fun n : ℕ ↦ E.obj ⟨n⟩) ⟶ (RGamma.obj L)⟦(1 : ℤ)⟧),
let T := Triangle.mk a (Pi.lift fun n : ℕ ↦
Pi.π (fun n : ℕ ↦ E.obj ⟨n⟩) n -
Pi.π (fun n : ℕ ↦ E.obj ⟨n⟩) (n + 1) ≫
E.map (homOfLE (Nat.le_succ n)).op) b
T ∈ distTriang (DerivedCategory A) ∧
(∀ n : ℕ, a ≫ Pi.π (fun n : ℕ ↦ E.obj ⟨n⟩) n =
RGamma.map (p ≫ Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) n)) ∧
∃ (ePrev : Hprev.obj (∏ᶜ fun n : ℕ ↦ E.obj ⟨n⟩) ≅
∏ᶜ fun n : ℕ ↦ Fprev.obj ⟨n⟩)
(i : cokernel dprev ⟶ Hcur.obj (RGamma.obj L))
(q : Hcur.obj (RGamma.obj L) ⟶ limit Fcur)
(zero : i ≫ q = 0),
(ePrev.hom = piComparison Hprev (fun n : ℕ ↦ E.obj ⟨n⟩) ∧
cokernel.π dprev ≫ i =
ePrev.inv ≫ (DerivedCategory.homologyFunctor A 0).homologySequenceδ
T (m - 1) m (by omega) ∧
(ShortComplex.mk i q zero).ShortExact ∧
∀ n : ℕ, q ≫ limit.π Fcur ⟨n⟩ =
Hcur.map (RGamma.map (p ≫ Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) n)))
Stacks.Cohomology.DerivedSectionsMilnor.isDerivedLimit_map_derivedSectionsOverObject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedLimit/DerivedSectionsAndInverseLimits.lean, line 169. The attribute's comment: “derived sections over an object commute with derived limits”.
Stacks Project Tag 0D6K. Derived sections over an object of a ringed site carry a derived inverse limit to a derived inverse limit.
Sections over an object are additive and preserve countable products, so Tag 08U1 applies.
theorem isDerivedLimit_map_derivedSectionsOverObject (X : RingedSite.{u, u, u}) (U : X.C)
[HasSheafify X.J AddCommGrpCat.{u}]
[X.J.WEqualsLocallyBijective AddCommGrpCat.{u}]
[IsGrothendieckAbelian.{g} (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))]
(K : ℕᵒᵖ ⥤ DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
[HasProduct fun n : ℕ ↦ K.obj ⟨n⟩]
(L : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
(hL : IsDerivedLimit K L) :
∃ h : HasProduct fun n : ℕ ↦ (K ⋙ derivedSectionsOverObject X U).obj ⟨n⟩,
letI := h
IsDerivedLimit (K ⋙ derivedSectionsOverObject X U)
((derivedSectionsOverObject X U).obj L)
Stacks.Cohomology.DerivedSectionsMilnor.exists_shortExact_limOne_cohomology_derivedSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedLimit/DerivedSectionsAndInverseLimits.lean, line 198. The attribute's comment: “short exact sequence over an object”.
Stacks Project Tag 0D6K. The canonical Milnor short exact sequence for cohomology over an object of a ringed site: the first derived inverse limit of the degree-
m - 1cohomologies includes into the degree-mcohomology of derived sections of the derived limit, with quotient the inverse limit of the degree-mcohomologies.
theorem exists_shortExact_limOne_cohomology_derivedSections (X : RingedSite.{u, u, u}) (U : X.C)
[HasSheafify X.J AddCommGrpCat.{u}]
[X.J.WEqualsLocallyBijective AddCommGrpCat.{u}]
[IsGrothendieckAbelian.{g} (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))]
(K : ℕᵒᵖ ⥤ DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
[HasProduct fun n : ℕ ↦ K.obj ⟨n⟩]
(L : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
(p : L ⟶ ∏ᶜ fun n : ℕ ↦ K.obj ⟨n⟩)
(hL : ∃ δ : (∏ᶜ fun n : ℕ ↦ K.obj ⟨n⟩) ⟶ L⟦(1 : ℤ)⟧,
Triangle.mk p (Pi.lift fun n : ℕ ↦
Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) n -
Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) (n + 1) ≫
K.map (homOfLE (Nat.le_succ n)).op) δ ∈
distTriang
(DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))))
(m : ℤ) :
let RG := derivedSectionsOverObject X U
let Hprev := DerivedCategory.homologyFunctor AddCommGrpCat.{u} (m - 1)
let Hcur := DerivedCategory.homologyFunctor AddCommGrpCat.{u} m
let E := K ⋙ RG
let Fprev := E ⋙ Hprev
let Fcur := E ⋙ Hcur
let dprev : (∏ᶜ fun n : ℕ ↦ Fprev.obj ⟨n⟩) ⟶ (∏ᶜ fun n : ℕ ↦ Fprev.obj ⟨n⟩) :=
Pi.lift fun n : ℕ ↦
Pi.π (fun n : ℕ ↦ Fprev.obj ⟨n⟩) n -
Pi.π (fun n : ℕ ↦ Fprev.obj ⟨n⟩) (n + 1) ≫
Fprev.map (homOfLE (Nat.le_succ n)).op
∃ h : HasProduct fun n : ℕ ↦ E.obj ⟨n⟩,
letI := h
∃ (a : RG.obj L ⟶ ∏ᶜ fun n : ℕ ↦ E.obj ⟨n⟩)
(b : (∏ᶜ fun n : ℕ ↦ E.obj ⟨n⟩) ⟶ (RG.obj L)⟦(1 : ℤ)⟧),
let T := Triangle.mk a (Pi.lift fun n : ℕ ↦
Pi.π (fun n : ℕ ↦ E.obj ⟨n⟩) n -
Pi.π (fun n : ℕ ↦ E.obj ⟨n⟩) (n + 1) ≫
E.map (homOfLE (Nat.le_succ n)).op) b
T ∈ distTriang (DerivedCategory AddCommGrpCat.{u}) ∧
(∀ n : ℕ, a ≫ Pi.π (fun n : ℕ ↦ E.obj ⟨n⟩) n =
RG.map (p ≫ Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) n)) ∧
∃ (ePrev : Hprev.obj (∏ᶜ fun n : ℕ ↦ E.obj ⟨n⟩) ≅ ∏ᶜ fun n : ℕ ↦ Fprev.obj ⟨n⟩)
(i : cokernel dprev ⟶ Hcur.obj (RG.obj L))
(q : Hcur.obj (RG.obj L) ⟶ limit Fcur)
(zero : i ≫ q = 0),
ePrev.hom = piComparison Hprev (fun n : ℕ ↦ E.obj ⟨n⟩) ∧
cokernel.π dprev ≫ i =
ePrev.inv ≫ DerivedCategory.HomologySequence.δ T (m - 1) m ∧
(ShortComplex.mk i q zero).ShortExact ∧
∀ n : ℕ, q ≫ limit.π Fcur ⟨n⟩ =
Hcur.map (RG.map (p ≫ Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) n))
Tag 0A07, a lemma
Tag 0A07 in the Stacks Project.
Stacks.Cohomology.DerivedPushforwardOnRingedTopoi.isDerivedLimit_map_derivedPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPushforward/DerivedLimits.lean, line 92.
Stacks Project, Tag 0A07. Derived pushforward along a morphism of ringed topoi commutes with derived limits: it carries an object exhibited as the derived limit of a countable inverse system to the derived limit of the pushed-forward system.
theorem isDerivedLimit_map_derivedPushforward
(K : ℕᵒᵖ ⥤ DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
[HasProduct fun n : ℕ ↦ K.obj ⟨n⟩]
(L : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
(hL : IsDerivedLimit K L) :
∃ h : HasProduct (fun n : ℕ ↦ (derivedPushforward f).obj (K.obj ⟨n⟩)),
@IsDerivedLimit
(DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)))
_ _ _ _ _ _
(K ⋙ derivedPushforward f) h ((derivedPushforward f).obj L)
Tag 0BKW, a remark
Tag 0BKW in the Stacks Project.
Stacks.Cohomology.DerivedLimitDiagram.cohomologyDerivedLimitDiagram_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedLimit/ComparisonDiagramUnconditional.lean, line 195. The attribute's comment: “the commuting square and the short exact sequences over the objects of the site”.
Stacks Project, Tag 0BKW. Let
(C, O)be a ringed site, let(Kₙ)be an inverse system inD(O)and letKbe a derived limit of it, presented by the structural mapp : K ⟶ ∏ Kₙof its distinguished product triangle. Fix a degreem, writePfor the cohomology presheaf functorM ↦ (U ↦ Hᵐ(U, M)),Hfor the cohomology sheaf functor,Sfor sheafification andefor the Tag 0BKV identificationS ∘ P ≅ H. Then:
- there are comparison maps
a : P K ⟶ lim P Kₙ,b : H K ⟶ lim H Kₙandc : S (lim P Kₙ) ⟶ lim H Kₙ, each determined by its composites with the limit projections, and the squareS a ≫ c = e ≫ bcommutes; and- for every object
UofCthere is a short exact sequence
0 ⟶ R¹lim Hᵐ⁻¹(U, Kₙ) ⟶ Hᵐ(U, K) ⟶ lim Hᵐ(U, Kₙ) ⟶ 0,whose surjection is determined by its composites with the limit projections and whose
R¹limis the cokernel of the difference map(xₙ) ↦ (xₙ - fₙ₊₁(xₙ₊₁)).The third comparison map is not asserted to be invertible: sheafification does not in general commute with this inverse limit, which is the caveat of the remark.
Nothing is assumed: sheafification, local bijectivity, Grothendieck abelianness, the right derived functor presenting cohomology and the countable product presenting the derived limit are all theorems at this module universe, and are supplied here.
theorem cohomologyDerivedLimitDiagram_unconditional
(K : ℕᵒᵖ ⥤ DerivedCategory
(SheafOfModules.{max u v r w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
(L : DerivedCategory
(SheafOfModules.{max u v r w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
(p : L ⟶ ∏ᶜ fun n : ℕ ↦ K.obj ⟨n⟩)
(hp : ∃ δ : (∏ᶜ fun n : ℕ ↦ K.obj ⟨n⟩) ⟶ L⟦(1 : ℤ)⟧,
Triangle.mk p (Pi.lift fun n : ℕ ↦
Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) n -
Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) (n + 1) ≫
K.map (homOfLE (Nat.le_succ n)).op) δ ∈
distTriang (DerivedCategory
(SheafOfModules.{max u v r w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))))
(m : ℤ) :
let P := DerivedLimitSections.derivedSectionsPresheafMax.{u, v, r, w} X ⋙
DerivedCategory.homologyFunctor
(PresheafOfModules.{max u v r w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O).obj) m
let H := DerivedCategory.homologyFunctor
(SheafOfModules.{max u v r w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) m
let S := sheafificationMax.{u, v, r, w} X
let e := sheafificationCohomologyPresheafIsoMax.{u, v, r, w} X m
(∃ (a : P.obj L ⟶ limit (K ⋙ P))
(b : H.obj L ⟶ limit (K ⋙ H))
(c : S.obj (limit (K ⋙ P)) ⟶ limit (K ⋙ H)),
(∀ n : ℕ,
a ≫ limit.π (K ⋙ P) ⟨n⟩ =
P.map (p ≫ Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) n)) ∧
(∀ n : ℕ,
b ≫ limit.π (K ⋙ H) ⟨n⟩ =
H.map (p ≫ Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) n)) ∧
(∀ n : ℕ,
c ≫ limit.π (K ⋙ H) ⟨n⟩ =
S.map (limit.π (K ⋙ P) ⟨n⟩) ≫ e.hom.app (K.obj ⟨n⟩)) ∧
(S.map a ≫ c = e.hom.app L ≫ b)) ∧
∀ U : X.C,
let RG := derivedSectionsMax.{u, v, r, w} X U
let Mprev := DerivedCategory.homologyFunctor
(ModuleCat.{max u v r w} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).obj.obj (.op U)))
(m - 1)
let Mcur := DerivedCategory.homologyFunctor
(ModuleCat.{max u v r w} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).obj.obj (.op U))) m
let E := K ⋙ RG
let Fprev := E ⋙ Mprev
let Fcur := E ⋙ Mcur
let dprev : (∏ᶜ fun n : ℕ ↦ Fprev.obj ⟨n⟩) ⟶ (∏ᶜ fun n : ℕ ↦ Fprev.obj ⟨n⟩) :=
Pi.lift fun n : ℕ ↦
Pi.π (fun n : ℕ ↦ Fprev.obj ⟨n⟩) n -
Pi.π (fun n : ℕ ↦ Fprev.obj ⟨n⟩) (n + 1) ≫
Fprev.map (homOfLE (Nat.le_succ n)).op
∃ (i : cokernel dprev ⟶ Mcur.obj (RG.obj L))
(q : Mcur.obj (RG.obj L) ⟶ limit Fcur)
(zero : i ≫ q = 0),
(ShortComplex.mk i q zero).ShortExact ∧
∀ n : ℕ, q ≫ limit.π Fcur ⟨n⟩ =
Mcur.map (RG.map (p ≫ Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) n))
Tag 0BKY, a lemma
Tag 0BKY in the Stacks Project.
Stacks.Cohomology.SiteInverseLimits.isDerivedLimit_single_limit_of_acyclic_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedLimit/InverseLimitOfAcyclicTower.lean, line 371. The attribute's comment: “ordinary limit is a derived limit”.
If the terms of a countable inverse system of modules on a ringed site are acyclic on a class of objects covering every object, and the first derived inverse limit of their sections vanishes there, then the ordinary inverse limit, placed in degree zero, is a derived inverse limit of the system.
theorem isDerivedLimit_single_limit_of_acyclic_cover
(F : ℕᵒᵖ ⥤ SheafOfModules.{z} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
(B : ObjectProperty X.C) (hB : X.J.HasEnoughObjects B)
(hcoh : ∀ U, B U →
letI : (SheafOfModules.evaluation.{z}
(Stacks.SheafOfModules.Tensor.ringSheaf X.O) (op U)).Additive :=
Stacks.SheafOfModules.evaluationAdditive.{z}
(R := (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) (op U);
∀ n p : ℕ, 0 < p →
IsZero (((sectionsFunctor.{u, v, w, z} X U).rightDerived p).obj (F.obj ⟨n⟩)))
(hlimOne : ∀ U, B U →
IsZero (Rlim.firstDerivedLimit (sectionsSystem.{u, v, w, z} X F U))) :
∃ h : HasProduct (fun n : ℕ =>
(F ⋙ DerivedCategory.singleFunctor
(SheafOfModules.{z} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) 0).obj ⟨n⟩),
@IsDerivedLimit
(DerivedCategory (SheafOfModules.{z} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
_ _ _ _ _ _
(F ⋙ DerivedCategory.singleFunctor
(SheafOfModules.{z} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) 0) h
((DerivedCategory.singleFunctor
(SheafOfModules.{z} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) 0).obj
(limit F))
Stacks.Cohomology.SiteInverseLimits.isZero_cohomology_limit_of_acyclic_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedLimit/InverseLimitOfAcyclicTower.lean, line 437. The attribute's comment: “acyclicity of the ordinary limit”.
Under the same hypotheses, the ordinary inverse limit has vanishing positive-degree cohomology on every member of the covering class.
theorem isZero_cohomology_limit_of_acyclic_cover
(F : ℕᵒᵖ ⥤ SheafOfModules.{z} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
(B : ObjectProperty X.C) (hB : X.J.HasEnoughObjects B)
(hcoh : ∀ U, B U →
letI : (SheafOfModules.evaluation.{z}
(Stacks.SheafOfModules.Tensor.ringSheaf X.O) (op U)).Additive :=
Stacks.SheafOfModules.evaluationAdditive.{z}
(R := (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) (op U);
∀ n p : ℕ, 0 < p →
IsZero (((sectionsFunctor.{u, v, w, z} X U).rightDerived p).obj (F.obj ⟨n⟩)))
(hlimOne : ∀ U, B U →
IsZero (Rlim.firstDerivedLimit (sectionsSystem.{u, v, w, z} X F U)))
(U : X.C) (hU : B U) (p : ℕ) (hp : 0 < p) :
letI : (SheafOfModules.evaluation.{z}
(Stacks.SheafOfModules.Tensor.ringSheaf X.O) (op U)).Additive :=
Stacks.SheafOfModules.evaluationAdditive.{z}
(R := (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) (op U);
IsZero (((sectionsFunctor.{u, v, w, z} X U).rightDerived p).obj (limit F))
Tag 0D6L, a lemma
Tag 0D6L in the Stacks Project.
Stacks.Cohomology.DerivedLimitSections.cohomology_derivedLimit_projection_mono_on_sections_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedLimit/SectionsInjectivityUnconditional.lean, line 135.
Stacks Project, Tag 0D6L. Let
(C, O)be a ringed site, let(Kₙ)be an inverse system inD(O)with derived limitL, letVbe an object ofCand letmbe an integer. Suppose there are an indexNand a cofinal system of coverings ofVsuch that over every memberVᵢof every covering in the system
R¹ lim Hᵐ⁻¹(Vᵢ, Kₙ) = 0, andHᵐ(Vᵢ, Kₙ) ⟶ Hᵐ(Vᵢ, K_N)is injective forn ≥ N.Then
Hᵐ(L)(V) ⟶ Hᵐ(K_N)(V)is injective.Nothing is assumed: sheafification, local bijectivity, Grothendieck abelianness, the right derived functor presenting cohomology and the countable product presenting the derived limit are all theorems at this module universe, and are supplied above.
theorem cohomology_derivedLimit_projection_mono_on_sections_unconditional
(K : ℕᵒᵖ ⥤ DerivedCategory
(SheafOfModules.{max u v r w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
(L : DerivedCategory
(SheafOfModules.{max u v r w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
(p : L ⟶ ∏ᶜ fun n : ℕ ↦ K.obj ⟨n⟩)
(hL : ∃ δ : (∏ᶜ fun n : ℕ ↦ K.obj ⟨n⟩) ⟶ L⟦(1 : ℤ)⟧,
Triangle.mk p (Pi.lift fun n : ℕ ↦
Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) n -
Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) (n + 1) ≫
K.map (homOfLE (Nat.le_succ n)).op) δ ∈
distTriang (DerivedCategory
(SheafOfModules.{max u v r w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))))
(V : X.C) (m : ℤ) (N : ℕ)
(Cov : CofinalCoveringSystem X.J V)
(hlimOne : ∀ 𝒰 : PreZeroHypercover.{max u v} V, Cov.cov 𝒰 →
∀ i : 𝒰.I₀,
let F := K ⋙ derivedSectionsPresheafMax.{u, v, r, w} X ⋙
DerivedCategory.homologyFunctor
(PresheafOfModules.{max u v r w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O).obj)
(m - 1) ⋙
PresheafOfModules.evaluation
(Stacks.SheafOfModules.Tensor.ringSheaf X.O).obj (.op (𝒰.X i))
IsZero (cokernel (Pi.lift fun n : ℕ ↦
Pi.π (fun n : ℕ ↦ F.obj ⟨n⟩) n -
Pi.π (fun n : ℕ ↦ F.obj ⟨n⟩) (n + 1) ≫
F.map (homOfLE (Nat.le_succ n)).op)))
(hinj : ∀ 𝒰 : PreZeroHypercover.{max u v} V, Cov.cov 𝒰 →
∀ i : 𝒰.I₀,
let F := K ⋙ derivedSectionsPresheafMax.{u, v, r, w} X ⋙
DerivedCategory.homologyFunctor
(PresheafOfModules.{max u v r w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O).obj) m ⋙
PresheafOfModules.evaluation
(Stacks.SheafOfModules.Tensor.ringSheaf X.O).obj (.op (𝒰.X i))
∀ (n : ℕ) (hn : N ≤ n), Mono (F.map (homOfLE hn).op)) :
Mono ((SheafOfModules.evaluation (Stacks.SheafOfModules.Tensor.ringSheaf X.O) (.op V)).map
((DerivedCategory.homologyFunctor
(SheafOfModules.{max u v r w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) m).map
(p ≫ Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) N)))
Tag 0D6M, a lemma
Tag 0D6M in the Stacks Project.
Stacks.Cohomology.isIso_to_isDerivedLimit_truncationGETower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedLimit/TruncationTowerConvergence.lean, line 1305.
Stacks Project, Tag 0D6M. Under local, eventually vanishing cohomology bounds, the canonical map from a derived object to any derived limit of its truncations from below is an isomorphism.
theorem isIso_to_isDerivedLimit_truncationGETower
{C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
(O : Sheaf J RingCat.{wRing})
[HasSheafify J AddCommGrpCat.{wModule}]
[J.WEqualsLocallyBijective AddCommGrpCat.{wModule}]
[EnoughInjectives (SheafOfModules.{wModule} O)]
(E : DerivedCategory (SheafOfModules.{wModule} O))
(B : Set C)
(basisCover : ∀ U : C, ∃ 𝒰 : PreZeroHypercover.{max u v} U,
𝒰.sieve₀ ∈ J U ∧ ∀ i, B (𝒰.X i))
(degreeBound : ∀ V : C, B V → ℤ → ℤ)
(Cov : ∀ V : C, B V → Set (PreZeroHypercover.{max u v} V))
(Cov_isCover : ∀ (V : C) (hV : B V) (𝒰 : PreZeroHypercover.{max u v} V),
Cov V hV 𝒰 → 𝒰.sieve₀ ∈ J V)
(Cov_cofinal : ∀ (V : C) (hV : B V) (𝒰 : PreZeroHypercover.{max u v} V),
𝒰.sieve₀ ∈ J V →
∃ 𝒱 : PreZeroHypercover.{max u v} V, Cov V hV 𝒱 ∧ Nonempty (𝒱.Hom 𝒰))
(vanishing : ∀ (V : C) (hV : B V) (𝒰 : PreZeroHypercover.{max u v} V),
Cov V hV 𝒰 → ∀ (i : 𝒰.I₀) (p : ℕ) (m : ℤ),
degreeBound V hV m < (p : ℤ) →
IsZero (moduleCohomology O (𝒰.X i) p
((DerivedCategory.homologyFunctor (SheafOfModules.{wModule} O)
(m - (p : ℤ))).obj E)))
[HasProduct fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{wModule} O) E).obj ⟨n⟩]
(L : DerivedCategory (SheafOfModules.{wModule} O))
(c : E ⟶ L)
(q : L ⟶ ∏ᶜ fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{wModule} O) E).obj ⟨n⟩)
(δ : (∏ᶜ fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{wModule} O) E).obj ⟨n⟩) ⟶ L⟦(1 : ℤ)⟧)
(hL : Triangle.mk q (Pi.lift fun n : ℕ ↦
Pi.π (fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{wModule} O) E).obj ⟨n⟩) n -
Pi.π (fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{wModule} O) E).obj ⟨n⟩) (n + 1) ≫
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{wModule} O) E).map
(homOfLE (Nat.le_succ n)).op) δ ∈
distTriang (DerivedCategory (SheafOfModules.{wModule} O)))
(hc : ∀ n : ℕ, c ≫ q ≫
Pi.π (fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{wModule} O) E).obj ⟨n⟩) n =
(DerivedCategory.TStructure.t.truncGEπ (-(n : ℤ))).app E) :
IsIso c
Stacks.Cohomology.isIso_to_isDerivedLimit_truncGETower_of_vanishing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedLimit/TruncationTowerConvergenceUnconditional.lean, line 100.
Stacks Project, Tag 0D6M. Let
Obe a sheaf of rings on a siteC, letEbe an object of the derived category of sheaves ofO-modules, and letBbe a set of objects ofClarge enough that every object is covered by members ofB. Suppose eachV ∈ Bcarries a degree boundp(V, -) : ℤ → ℤand a cofinal system of coverings ofVon whose membersHᵖ(Vᵢ, H^{m - p}(E)) = 0wheneverp > p(V, m). Then the canonical map fromEto the derived limit of the truncation towern ↦ τ_{≥ -n} Eis an isomorphism.Nothing is assumed: sheafification, enough injectives and the countable products presenting the derived limit are all theorems at this module universe, and are supplied as instances above.
theorem isIso_to_isDerivedLimit_truncGETower_of_vanishing
(O : Sheaf J RingCat.{r})
(E : DerivedCategory (SheafOfModules.{max u v r w} O))
(B : Set C)
(basisCover : ∀ U : C, ∃ 𝒰 : PreZeroHypercover.{max u v} U,
𝒰.sieve₀ ∈ J U ∧ ∀ i, B (𝒰.X i))
(degreeBound : ∀ V : C, B V → ℤ → ℤ)
(Cov : ∀ V : C, B V → Set (PreZeroHypercover.{max u v} V))
(Cov_isCover : ∀ (V : C) (hV : B V) (𝒰 : PreZeroHypercover.{max u v} V),
Cov V hV 𝒰 → 𝒰.sieve₀ ∈ J V)
(Cov_cofinal : ∀ (V : C) (hV : B V) (𝒰 : PreZeroHypercover.{max u v} V),
𝒰.sieve₀ ∈ J V →
∃ 𝒱 : PreZeroHypercover.{max u v} V, Cov V hV 𝒱 ∧ Nonempty (𝒱.Hom 𝒰))
(vanishing : ∀ (V : C) (hV : B V) (𝒰 : PreZeroHypercover.{max u v} V),
Cov V hV 𝒰 → ∀ (i : 𝒰.I₀) (p : ℕ) (m : ℤ),
degreeBound V hV m < (p : ℤ) →
IsZero (@moduleCohomology C instC J O hasSheafifyMax.{u, v, r, w}
wEqualsLocallyBijectiveMax.{u, v, r, w}
(SiteModules.moduleSheavesEnoughInjectives.{u, v, r, w} O)
(𝒰.X i) p
((DerivedCategory.homologyFunctor (SheafOfModules.{max u v r w} O)
(m - (p : ℤ))).obj E)))
(L : DerivedCategory (SheafOfModules.{max u v r w} O))
(c : E ⟶ L)
(q : L ⟶ ∏ᶜ fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{max u v r w} O) E).obj ⟨n⟩)
(δ : (∏ᶜ fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{max u v r w} O) E).obj ⟨n⟩) ⟶
L⟦(1 : ℤ)⟧)
(hL : Triangle.mk q (Pi.lift fun n : ℕ ↦
Pi.π (fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{max u v r w} O) E).obj ⟨n⟩) n -
Pi.π (fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{max u v r w} O) E).obj ⟨n⟩)
(n + 1) ≫
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{max u v r w} O) E).map
(homOfLE (Nat.le_succ n)).op) δ ∈
distTriang (DerivedCategory (SheafOfModules.{max u v r w} O)))
(hc : ∀ n : ℕ, c ≫ q ≫
Pi.π (fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{max u v r w} O) E).obj ⟨n⟩) n =
(DerivedCategory.TStructure.t.truncGEπ (-(n : ℤ))).app E) :
IsIso c
Tag 0D6N, a lemma
Tag 0D6N in the Stacks Project.
Stacks.Cohomology.isIso_to_isDerivedLimit_truncationGETower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedLimit/TruncationTowerConvergence.lean, line 1305. The attribute's comment: “the constant-bound case, by taking the degree bound at V to be max d_V m”.
Stacks Project, Tag 0D6M. Under local, eventually vanishing cohomology bounds, the canonical map from a derived object to any derived limit of its truncations from below is an isomorphism.
theorem isIso_to_isDerivedLimit_truncationGETower
{C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
(O : Sheaf J RingCat.{wRing})
[HasSheafify J AddCommGrpCat.{wModule}]
[J.WEqualsLocallyBijective AddCommGrpCat.{wModule}]
[EnoughInjectives (SheafOfModules.{wModule} O)]
(E : DerivedCategory (SheafOfModules.{wModule} O))
(B : Set C)
(basisCover : ∀ U : C, ∃ 𝒰 : PreZeroHypercover.{max u v} U,
𝒰.sieve₀ ∈ J U ∧ ∀ i, B (𝒰.X i))
(degreeBound : ∀ V : C, B V → ℤ → ℤ)
(Cov : ∀ V : C, B V → Set (PreZeroHypercover.{max u v} V))
(Cov_isCover : ∀ (V : C) (hV : B V) (𝒰 : PreZeroHypercover.{max u v} V),
Cov V hV 𝒰 → 𝒰.sieve₀ ∈ J V)
(Cov_cofinal : ∀ (V : C) (hV : B V) (𝒰 : PreZeroHypercover.{max u v} V),
𝒰.sieve₀ ∈ J V →
∃ 𝒱 : PreZeroHypercover.{max u v} V, Cov V hV 𝒱 ∧ Nonempty (𝒱.Hom 𝒰))
(vanishing : ∀ (V : C) (hV : B V) (𝒰 : PreZeroHypercover.{max u v} V),
Cov V hV 𝒰 → ∀ (i : 𝒰.I₀) (p : ℕ) (m : ℤ),
degreeBound V hV m < (p : ℤ) →
IsZero (moduleCohomology O (𝒰.X i) p
((DerivedCategory.homologyFunctor (SheafOfModules.{wModule} O)
(m - (p : ℤ))).obj E)))
[HasProduct fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{wModule} O) E).obj ⟨n⟩]
(L : DerivedCategory (SheafOfModules.{wModule} O))
(c : E ⟶ L)
(q : L ⟶ ∏ᶜ fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{wModule} O) E).obj ⟨n⟩)
(δ : (∏ᶜ fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{wModule} O) E).obj ⟨n⟩) ⟶ L⟦(1 : ℤ)⟧)
(hL : Triangle.mk q (Pi.lift fun n : ℕ ↦
Pi.π (fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{wModule} O) E).obj ⟨n⟩) n -
Pi.π (fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{wModule} O) E).obj ⟨n⟩) (n + 1) ≫
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{wModule} O) E).map
(homOfLE (Nat.le_succ n)).op) δ ∈
distTriang (DerivedCategory (SheafOfModules.{wModule} O)))
(hc : ∀ n : ℕ, c ≫ q ≫
Pi.π (fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{wModule} O) E).obj ⟨n⟩) n =
(DerivedCategory.TStructure.t.truncGEπ (-(n : ℤ))).app E) :
IsIso c
Stacks.Cohomology.isIso_to_isDerivedLimit_truncGETower_of_vanishing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedLimit/TruncationTowerConvergenceUnconditional.lean, line 100. The attribute's comment: “the constant-bound case, by taking the degree bound at V to be max d_V m”.
Stacks Project, Tag 0D6M. Let
Obe a sheaf of rings on a siteC, letEbe an object of the derived category of sheaves ofO-modules, and letBbe a set of objects ofClarge enough that every object is covered by members ofB. Suppose eachV ∈ Bcarries a degree boundp(V, -) : ℤ → ℤand a cofinal system of coverings ofVon whose membersHᵖ(Vᵢ, H^{m - p}(E)) = 0wheneverp > p(V, m). Then the canonical map fromEto the derived limit of the truncation towern ↦ τ_{≥ -n} Eis an isomorphism.Nothing is assumed: sheafification, enough injectives and the countable products presenting the derived limit are all theorems at this module universe, and are supplied as instances above.
theorem isIso_to_isDerivedLimit_truncGETower_of_vanishing
(O : Sheaf J RingCat.{r})
(E : DerivedCategory (SheafOfModules.{max u v r w} O))
(B : Set C)
(basisCover : ∀ U : C, ∃ 𝒰 : PreZeroHypercover.{max u v} U,
𝒰.sieve₀ ∈ J U ∧ ∀ i, B (𝒰.X i))
(degreeBound : ∀ V : C, B V → ℤ → ℤ)
(Cov : ∀ V : C, B V → Set (PreZeroHypercover.{max u v} V))
(Cov_isCover : ∀ (V : C) (hV : B V) (𝒰 : PreZeroHypercover.{max u v} V),
Cov V hV 𝒰 → 𝒰.sieve₀ ∈ J V)
(Cov_cofinal : ∀ (V : C) (hV : B V) (𝒰 : PreZeroHypercover.{max u v} V),
𝒰.sieve₀ ∈ J V →
∃ 𝒱 : PreZeroHypercover.{max u v} V, Cov V hV 𝒱 ∧ Nonempty (𝒱.Hom 𝒰))
(vanishing : ∀ (V : C) (hV : B V) (𝒰 : PreZeroHypercover.{max u v} V),
Cov V hV 𝒰 → ∀ (i : 𝒰.I₀) (p : ℕ) (m : ℤ),
degreeBound V hV m < (p : ℤ) →
IsZero (@moduleCohomology C instC J O hasSheafifyMax.{u, v, r, w}
wEqualsLocallyBijectiveMax.{u, v, r, w}
(SiteModules.moduleSheavesEnoughInjectives.{u, v, r, w} O)
(𝒰.X i) p
((DerivedCategory.homologyFunctor (SheafOfModules.{max u v r w} O)
(m - (p : ℤ))).obj E)))
(L : DerivedCategory (SheafOfModules.{max u v r w} O))
(c : E ⟶ L)
(q : L ⟶ ∏ᶜ fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{max u v r w} O) E).obj ⟨n⟩)
(δ : (∏ᶜ fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{max u v r w} O) E).obj ⟨n⟩) ⟶
L⟦(1 : ℤ)⟧)
(hL : Triangle.mk q (Pi.lift fun n : ℕ ↦
Pi.π (fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{max u v r w} O) E).obj ⟨n⟩) n -
Pi.π (fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{max u v r w} O) E).obj ⟨n⟩)
(n + 1) ≫
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{max u v r w} O) E).map
(homOfLE (Nat.le_succ n)).op) δ ∈
distTriang (DerivedCategory (SheafOfModules.{max u v r w} O)))
(hc : ∀ n : ℕ, c ≫ q ≫
Pi.π (fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{max u v r w} O) E).obj ⟨n⟩) n =
(DerivedCategory.TStructure.t.truncGEπ (-(n : ℤ))).app E) :
IsIso c
Tag 08U3, a lemma
Tag 08U3 in the Stacks Project.
Stacks.Cohomology.isIso_to_isDerivedLimit_truncGETower_of_degreeBound, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedLimit/TruncationConvergenceUnderBounds.lean, line 87. The attribute's comment: “variant: the single-universe form, for a ringed site whose module category has enough injectives and the countable product of the truncation tower; the tag, with neither of these, is Stacks.Cohomology.DegreeBound.isIso_to_isDerivedLimit_truncGETower_of_degreeBound”.
Degree-dependent bounds for cohomology on a locally covering class imply that the canonical map to the derived limit of the lower-truncation tower is an isomorphism.
This is a variant of [Stacks, Tag 08U3]: the enough-injectives and product hypotheses below are not hypotheses of the source, and they are avoidable. The full statement is
Stacks.Cohomology.DegreeBound.isIso_to_isDerivedLimit_truncGETower_of_degreeBound, which discharges them by taking the module universe large enough to contain the site and the structure rings. This single-universe form is kept for the consumers that are already stated at it.
theorem isIso_to_isDerivedLimit_truncGETower_of_degreeBound
(S : AlgebraicGeometry.RingedSite.{u, u, u})
[HasSheafify S.J AddCommGrpCat.{u}]
[S.J.WEqualsLocallyBijective AddCommGrpCat.{u}]
[EnoughInjectives (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf S.O))]
(E : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf S.O)))
(degreeBound : ℤ → ℤ) (B : Set S.C)
(basisCover : ∀ U : S.C, ∃ 𝒰 : PreZeroHypercover.{u} U,
𝒰.sieve₀ ∈ S.J U ∧ ∀ i, B (𝒰.X i))
(vanishing : ∀ (V : S.C), B V → ∀ (p : ℕ) (m : ℤ),
degreeBound m < (p : ℤ) →
IsZero (moduleCohomology (Stacks.SheafOfModules.Tensor.ringSheaf S.O) V p
((DerivedCategory.homologyFunctor
(SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf S.O))
(m - (p : ℤ))).obj E)))
(L : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf S.O)))
[HasProduct fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower
(SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf S.O)) E).obj ⟨n⟩]
(q : L ⟶ ∏ᶜ fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower
(SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf S.O)) E).obj ⟨n⟩)
(hL : ∃ δ :
(∏ᶜ fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower
(SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf S.O)) E).obj ⟨n⟩) ⟶
L⟦(1 : ℤ)⟧,
Triangle.mk q (Pi.lift fun n : ℕ ↦
Pi.π (fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower
(SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf S.O)) E).obj ⟨n⟩) n -
Pi.π (fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower
(SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf S.O)) E).obj ⟨n⟩)
(n + 1) ≫
(Stacks.DerivedLimit.truncGETower
(SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf S.O)) E).map
(homOfLE (Nat.le_succ n)).op) δ ∈
distTriang
(DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf S.O))))
(c : E ⟶ L)
(hc : ∀ n : ℕ, c ≫ q ≫ Pi.π
(fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower
(SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf S.O)) E).obj ⟨n⟩) n =
(DerivedCategory.TStructure.t.truncGEπ (-(n : ℤ))).app E) :
IsIso c
Stacks.Cohomology.DegreeBound.isIso_to_isDerivedLimit_truncGETower_of_degreeBound, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedLimit/TruncationConvergenceUnderBoundsUnconditional.lean, line 80.
Stacks Project, Tag 08U3. Let
Obe a sheaf of rings on a siteCand letEbe an object of the derived category of sheaves ofO-modules. Suppose there are a functionp(-) : ℤ → ℤand a setBof objects ofCsuch that every object ofChas a covering whose members are elements ofB, and such thatH^p(V, H^{m - p}(E)) = 0for allp > p(m)and allV ∈ B. Then the canonical mapE ⟶ R lim τ_{≥ -n} Eis an isomorphism.Nothing else is assumed: sheafification, enough injectives and the countable products presenting the derived limit are all theorems at this module universe.
theorem isIso_to_isDerivedLimit_truncGETower_of_degreeBound
(O : Sheaf J RingCat.{r})
(E : DerivedCategory (SheafOfModules.{max u v r w} O))
(degreeBound : ℤ → ℤ) (B : Set C)
(basisCover : ∀ U : C, ∃ 𝒰 : PreZeroHypercover.{max u v} U,
𝒰.sieve₀ ∈ J U ∧ ∀ i, B (𝒰.X i))
(vanishing : ∀ (V : C), B V → ∀ (p : ℕ) (m : ℤ), degreeBound m < (p : ℤ) →
IsZero (@moduleCohomology C instC J O hasSheafifyMax.{u, v, r, w}
wEqualsLocallyBijectiveMax.{u, v, r, w}
(SiteModules.moduleSheavesEnoughInjectives.{u, v, r, w} O) V p
((DerivedCategory.homologyFunctor (SheafOfModules.{max u v r w} O)
(m - (p : ℤ))).obj E)))
(L : DerivedCategory (SheafOfModules.{max u v r w} O))
(c : E ⟶ L)
(q : L ⟶ ∏ᶜ fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{max u v r w} O) E).obj ⟨n⟩)
(hL : ∃ δ : (∏ᶜ fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{max u v r w} O) E).obj ⟨n⟩) ⟶
L⟦(1 : ℤ)⟧,
Triangle.mk q (Pi.lift fun n : ℕ ↦
Pi.π (fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{max u v r w} O) E).obj ⟨n⟩) n -
Pi.π (fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{max u v r w} O) E).obj ⟨n⟩)
(n + 1) ≫
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{max u v r w} O) E).map
(homOfLE (Nat.le_succ n)).op) δ ∈
distTriang (DerivedCategory (SheafOfModules.{max u v r w} O)))
(hc : ∀ n : ℕ, c ≫ q ≫
Pi.π (fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{max u v r w} O) E).obj ⟨n⟩) n =
(DerivedCategory.TStructure.t.truncGEπ (-(n : ℤ))).app E) :
IsIso c
Tag 0D6P, a lemma
Tag 0D6P in the Stacks Project.
Stacks.Cohomology.UniformBound.isIso_to_isDerivedLimit_truncGETower_of_vanishing_uniform, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedLimit/TruncationConvergenceUniformBoundUnconditional.lean, line 57.
Let
Obe a sheaf of rings on a siteCand letEbe an object of the derived category of sheaves ofO-modules. Suppose there are an integerd ≥ 0and a setBof objects ofCsuch that every object ofChas a covering whose members are elements ofB, and such thatH^p(V, H^q(E)) = 0for allp > d, allq < 0and allV ∈ B. Then the canonical mapE ⟶ R lim τ_{≥ -n} Eis an isomorphism.Here
R lim τ_{≥ -n} Eis an objectLwith a distinguished triangleL ⟶ ∏ τ_{≥ -n} E ⟶ ∏ τ_{≥ -n} E ⟶ L[1], andc : E ⟶ Lis the map whose composites with the product projections are the truncation mapsE ⟶ τ_{≥ -n} E.
theorem isIso_to_isDerivedLimit_truncGETower_of_vanishing_uniform
(O : Sheaf J RingCat.{r})
(E : DerivedCategory (SheafOfModules.{max u v r w} O))
(d : ℤ) (hd : 0 ≤ d) (B : Set C)
(basisCover : ∀ U : C, ∃ 𝒰 : PreZeroHypercover.{max u v} U,
𝒰.sieve₀ ∈ J U ∧ ∀ i, B (𝒰.X i))
(vanishing : ∀ (V : C), B V → ∀ (p : ℕ), d < (p : ℤ) → ∀ (q : ℤ), q < 0 →
IsZero (@moduleCohomology C instC J O hasSheafifyMax.{u, v, r, w}
wEqualsLocallyBijectiveMax.{u, v, r, w}
(SiteModules.moduleSheavesEnoughInjectives.{u, v, r, w} O) V p
((DerivedCategory.homologyFunctor (SheafOfModules.{max u v r w} O) q).obj E)))
(L : DerivedCategory (SheafOfModules.{max u v r w} O))
(c : E ⟶ L)
(q : L ⟶ ∏ᶜ fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{max u v r w} O) E).obj ⟨n⟩)
(hL : ∃ δ : (∏ᶜ fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{max u v r w} O) E).obj ⟨n⟩) ⟶
L⟦(1 : ℤ)⟧,
Triangle.mk q (Pi.lift fun n : ℕ ↦
Pi.π (fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{max u v r w} O) E).obj ⟨n⟩) n -
Pi.π (fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{max u v r w} O) E).obj ⟨n⟩)
(n + 1) ≫
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{max u v r w} O) E).map
(homOfLE (Nat.le_succ n)).op) δ ∈
distTriang (DerivedCategory (SheafOfModules.{max u v r w} O)))
(hc : ∀ n : ℕ, c ≫ q ≫
Pi.π (fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{max u v r w} O) E).obj ⟨n⟩) n =
(DerivedCategory.TStructure.t.truncGEπ (-(n : ℤ))).app E) :
IsIso c
Tag 0BKZ, a lemma
Tag 0BKZ in the Stacks Project.
AlgebraicGeometry.isIso_hypercohomologyEdge_app_of_isAffineOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/AffineOpenHypercohomologyEdge.lean, line 72. The attribute's comment: “at the affine opens of a scheme, for an object with quasi-coherent cohomology”. References: EGA III (1.3.1), “more general”.
The hypercohomology edge morphism over an affine open of a scheme is invertible, at an object of
D(𝒪_X)whose cohomology sheaves are all quasi-coherent, in every degree and with no boundedness hypothesis.This is [Stacks, Tag 0BKZ] at the basis of affine opens of
X: the basis has enough objects, and the cohomology sheaves are acyclic over every member of it by Serre vanishing.
theorem isIso_hypercohomologyEdge_app_of_isAffineOpen
(hE : ∀ q : ℤ, ((DerivedCategory.homologyFunctor X.Modules q).obj E).IsQuasicoherent)
(U : X.Opens) (hU : U ∈ X.affineOpens) (q : ℤ) :
IsIso ((Stacks.Cohomology.HypercohomologyEdge.hypercohomologyEdge
X.ringCatSheaf U q).app E)
Stacks.Cohomology.HypercohomologyEdge.isIso_hypercohomologyEdge_app_of_acyclic_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/HypercohomologyEdge/AcyclicObject.lean, line 162.
Stacks Project Tag 0BKZ. If the cohomology sheaves of an object of the unbounded derived category of
O-modules have no higher cohomology over the members of a class of objects covering the site, then over each member its degree-qhypercohomology is the module of sections of its degree-qcohomology sheaf: the hypercohomology edge morphism is invertible there, in every degree.
theorem isIso_hypercohomologyEdge_app_of_acyclic_cover (U : C)
(K : DerivedCategory (SheafOfModules.{wModule} O))
(B : ObjectProperty C) (hB : J.HasEnoughObjects B)
(hvan : ∀ V : C, B V → ∀ p : ℕ, 0 < p → ∀ m : ℤ,
IsZero (((SheafOfModules.evaluation O (.op V)).rightDerived p).obj
((DerivedCategory.homologyFunctor (SheafOfModules.{wModule} O) m).obj K)))
(hU : B U) (q : ℤ) :
IsIso ((hypercohomologyEdge O U q).app K)
Tag 0A09, a lemma
Tag 0A09 in the Stacks Project.
Stacks.Cohomology.DerivedLimitAcyclic.isLimit_cohomology_of_isDerivedLimit_of_acyclic_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedLimit/CohomologyCommutesWithDerivedLimit.lean, line 80.
Stacks Project Tag 0A09. Cohomology commutes with a derived inverse limit if there is a class of objects covering the site on which all positive cohomology of the cohomology sheaves vanishes and the towers of their sections have vanishing first derived inverse limit.
The conclusion records the canonical limiting cone: the legs of the cone on the system of degree-
qcohomology sheaves are induced by the projections of a derived-limit triangle forL.
theorem isLimit_cohomology_of_isDerivedLimit_of_acyclic_cover
(K : ℕᵒᵖ ⥤ DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
(L : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
(hL : IsDerivedLimit K L)
(B : ObjectProperty X.C)
(hB : X.J.HasEnoughObjects B)
(hacyclic : ∀ U, B U → ∀ q : ℤ, ∀ n : ℕ, ∀ r : ℕ, 0 < r →
haveI := evaluation_additive (Stacks.SheafOfModules.Tensor.ringSheaf X.O) U
IsZero (((SheafOfModules.evaluation
(Stacks.SheafOfModules.Tensor.ringSheaf X.O) (op U)).rightDerived r).obj
((DerivedCategory.homologyFunctor
(SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) q).obj
(K.obj ⟨n⟩))))
(hlimOne : ∀ U, B U → ∀ q : ℤ,
IsZero (Rlim.firstDerivedLimit
(K ⋙ DerivedCategory.homologyFunctor
(SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) q ⋙
sectionsOverObject X U)))
(q : ℤ) :
∃ p : L ⟶ ∏ᶜ fun n : ℕ ↦ K.obj ⟨n⟩,
(∃ δ : (∏ᶜ fun n : ℕ ↦ K.obj ⟨n⟩) ⟶ L⟦(1 : ℤ)⟧,
Triangle.mk p (Pi.lift fun n : ℕ ↦
Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) n -
Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) (n + 1) ≫
K.map (homOfLE (Nat.le_succ n)).op) δ ∈
distTriang
(DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))) ∧
∃ τ : (Functor.const ℕᵒᵖ).obj
((DerivedCategory.homologyFunctor
(SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) q).obj L) ⟶
K ⋙ DerivedCategory.homologyFunctor
(SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) q,
(∀ n : ℕ, τ.app ⟨n⟩ =
(DerivedCategory.homologyFunctor
(SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) q).map
(p ≫ Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) n)) ∧
Nonempty (IsLimit (Cone.mk _ τ))
Sources
Section21.24 Producing K-injective resolutions#
Section 21.24 of the Stacks Project, Tag 070N. 3 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 070P, an equation
Tag 070P in the Stacks Project.
CochainComplex.toLimitOfTruncGEResolutions, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedLimit/IntoCandidateKInjective.lean, line 55.
Stacks Project, Tag 070P, the displayed arrow
ℱ• → ℐ•. Given an inverse system𝓘of cochain complexes and mapsf n : τ_{≥ -n} K ⟶ 𝓘ₙcommuting with the canonical truncation maps ofK, this is the induced mapK ⟶ lim 𝓘. For the tower of Stacks 070F the target is the candidate K-injective complex of Stacks 070L.
def toLimitOfTruncGEResolutions (𝓘 : ℕᵒᵖ ⥤ CochainComplex A ℤ) [HasLimit 𝓘]
(K : CochainComplex A ℤ) (f : ∀ n : ℕ, K.truncGE (-(n : ℤ)) ⟶ 𝓘.obj ⟨n⟩)
(hladder : ∀ n : ℕ, K.πTruncGE (-((n + 1 : ℕ) : ℤ)) ≫ f (n + 1) ≫
𝓘.map (homOfLE (Nat.le_succ n)).op = K.πTruncGE (-(n : ℤ)) ≫ f n) :
K ⟶ limit 𝓘
Tag 070Q, a lemma
Tag 070Q in the Stacks Project.
Stacks.Cohomology.quasiIso_to_limit_of_truncGE_resolutions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedLimit/KInjectiveTowerQuasiIso.lean, line 127.
Let
Obe a sheaf of rings on a site, letKbe a cochain complex ofO-modules, and let𝓘be an inverse system of K-injective complexes with degreewise split-epimorphic transition maps resolving the truncationsτ_{≥ -n} Kcompatibly with the canonical mapsK ⟶ τ_{≥ -n} K. If a subsetBof the objects of the site covers every object andH^p(V, H^q(K)) = 0for everyV ∈ B, everyp > dand everyq < 0, then the canonical mapγ : K ⟶ lim 𝓘is a quasi-isomorphism.
theorem quasiIso_to_limit_of_truncGE_resolutions {C : Type u} [Category.{u} C]
{J : GrothendieckTopology C} (O : Sheaf J RingCat.{u})
[HasSheafify J AddCommGrpCat.{u}]
[J.WEqualsLocallyBijective AddCommGrpCat.{u}]
[EnoughInjectives (SheafOfModules.{u} O)]
(K : CochainComplex (SheafOfModules.{u} O) ℤ)
(𝓘 : ℕᵒᵖ ⥤ CochainComplex (SheafOfModules.{u} O) ℤ)
(f : ∀ n : ℕ, K.truncGE (-(n : ℤ)) ⟶ 𝓘.obj ⟨n⟩)
(hf : ∀ n : ℕ, QuasiIso (f n))
(hcompat : ∀ n : ℕ,
K.πTruncGE (-((n + 1 : ℕ) : ℤ)) ≫ f (n + 1) ≫ 𝓘.map (homOfLE (Nat.le_succ n)).op =
K.πTruncGE (-(n : ℤ)) ≫ f n)
(h𝓘 : ∀ n : ℕ, (𝓘.obj ⟨n⟩).IsKInjective)
(hsplit : ∀ (n : ℕ) (i : ℤ), IsSplitEpi ((𝓘.map (homOfLE (Nat.le_succ n)).op).f i))
[HasLimit 𝓘] (γ : K ⟶ limit 𝓘)
(hγ : ∀ n : ℕ, γ ≫ limit.π 𝓘 ⟨n⟩ = K.πTruncGE (-(n : ℤ)) ≫ f n)
(B : Set C) (d : ℕ)
(hB : ∀ U : C, ∃ 𝒰 : PreZeroHypercover.{u} U, 𝒰.sieve₀ ∈ J U ∧ ∀ i, B (𝒰.X i))
(hvan : ∀ V : C, B V → ∀ p : ℕ, d < p → ∀ q : ℤ, q < 0 →
IsZero (moduleCohomology O V p
((DerivedCategory.homologyFunctor (SheafOfModules.{u} O) q).obj
(DerivedCategory.Q.obj K)))) :
QuasiIso γ
Tag 08CT, a lemma
Tag 08CT in the Stacks Project.
Stacks.Cohomology.InverseLimits.homology_isLimit_of_local_rlim_vanishing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedLimit/CohomologyOfInverseLimits.lean, line 536. The attribute's comment: “canonical cohomology-limit comparison”.
Stacks 08CT. The canonical cone from the degree-
mcohomology of the termwise inverse limit of an inverse system of complexes of modules on a ringed site to the degree-mcohomologies is a limit cone, provided the first derived limits of the sections vanish in degreesm - 2andm - 1and on the degreem - 1cohomology over a generating family, and the degree-mcohomology of sections is constant from stagen₀on.
public theorem homology_isLimit_of_local_rlim_vanishing
(X : AlgebraicGeometry.RingedSite.{u, v, w})
[HasSheafify X.J AddCommGrpCat.{t}]
[X.J.WEqualsLocallyBijective AddCommGrpCat.{t}]
(F : ℕᵒᵖ ⥤ CochainComplex (SheafOfModules.{t}
(Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ)
(m : ℤ) (B : Set X.C) (hB : X.J.HasEnoughObjects (· ∈ B))
(hneg2 : ∀ U ∈ B, IsZero (Rlim.firstDerivedLimit
(F ⋙ sectionsComplexFunctor (Stacks.SheafOfModules.Tensor.ringSheaf X.O) U ⋙
HomologicalComplex.eval Ab.{t} (ComplexShape.up ℤ) (m - 2))))
(hneg1 : ∀ U ∈ B, IsZero (Rlim.firstDerivedLimit
(F ⋙ sectionsComplexFunctor (Stacks.SheafOfModules.Tensor.ringSheaf X.O) U ⋙
HomologicalComplex.eval Ab.{t} (ComplexShape.up ℤ) (m - 1))))
(hHneg1 : ∀ U ∈ B, IsZero (Rlim.firstDerivedLimit
(F ⋙ sectionsComplexFunctor (Stacks.SheafOfModules.Tensor.ringSheaf X.O) U ⋙
HomologicalComplex.homologyFunctor Ab.{t} (ComplexShape.up ℤ) (m - 1))))
(n₀ : ℕ)
(hstable : ∀ U ∈ B, ∀ (n : ℕ) (hn : n₀ ≤ n), IsIso
((HomologicalComplex.homologyFunctor Ab.{t} (ComplexShape.up ℤ) m).map
((sectionsComplexFunctor (Stacks.SheafOfModules.Tensor.ringSheaf X.O) U).map
(F.map (homOfLE hn).op)))) :
Nonempty (IsLimit
((HomologicalComplex.homologyFunctor
(SheafOfModules.{t} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
(ComplexShape.up ℤ) m).mapCone (limit.cone F)))
Stacks.Cohomology.InverseLimits.homology_limit_projection_isIso_of_local_rlim_vanishing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedLimit/CohomologyOfInverseLimits.lean, line 588. The attribute's comment: “projection to a stable stage”.
Stacks 08CT. The limit of the degree-
mcohomology sheaves of an inverse system of complexes of modules on a ringed site projects isomorphically to any stage from which the degree-mcohomology of sections over a generating family is constant.
public theorem homology_limit_projection_isIso_of_local_rlim_vanishing
(X : AlgebraicGeometry.RingedSite.{u, v, w})
[HasSheafify X.J AddCommGrpCat.{t}]
[X.J.WEqualsLocallyBijective AddCommGrpCat.{t}]
(F : ℕᵒᵖ ⥤ CochainComplex (SheafOfModules.{t}
(Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ)
(m : ℤ) (B : Set X.C) (hB : X.J.HasEnoughObjects (· ∈ B)) (n₀ : ℕ)
(hstable : ∀ U ∈ B, ∀ (n : ℕ) (hn : n₀ ≤ n), IsIso
((HomologicalComplex.homologyFunctor Ab.{t} (ComplexShape.up ℤ) m).map
((sectionsComplexFunctor (Stacks.SheafOfModules.Tensor.ringSheaf X.O) U).map
(F.map (homOfLE hn).op)))) :
IsIso (limit.π (F ⋙ HomologicalComplex.homologyFunctor
(SheafOfModules.{t} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
(ComplexShape.up ℤ) m) (op n₀))
Sources
Section21.25 Bounded cohomological dimension#
Section 21.25 of the Stacks Project, Tag 0D6Q. 6 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0D6R, a situation
Tag 0D6R in the Stacks Project.
Stacks.Cohomology.OlssonLaszloSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedLimit/OlssonLaszloSituation.lean, line 99.
Stacks 0D6R. The standing Olsson--Laszlo situation: a weak Serre subcategory of modules on a site, together with a locally covering class of objects admitting cofinal systems of coverings on whose members higher cohomology vanishes uniformly in the module.
structure OlssonLaszloSituation
Tag 0D6S, a lemma
Tag 0D6S in the Stacks Project.
Stacks.Cohomology.OlssonLaszlo.truncGETower_presentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedLimit/PushforwardBoundedCohomologicalDimension.lean, line 194. The attribute's comment: “the conclusion with the derived limit, its defining distinguished triangle and the canonical map of Remark 0H72 constructed: for K in D_A(O) (hK) the truncation tower has a product and a presented derived limit, and the canonical map to it is an isomorphism”.
In the Olsson--Laszlo situation, the tower of truncations from below of an object of
D_A(O)has a derived limit, presented by its defining distinguished triangle, and the canonical map from the object to that derived limit is an isomorphism.
theorem truncGETower_presentation
(S : OlssonLaszloSituation.{v, u, wRing, wModule})
(K : DerivedCategory (SheafOfModules.{wModule} S.O))
(hK : DerivedCategoryB.derivedCategoryB S.A K) :
∃ (_hprod : HasProduct fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{wModule} S.O) K).obj ⟨n⟩)
(L : DerivedCategory (SheafOfModules.{wModule} S.O))
(c : K ⟶ L)
(p : L ⟶ ∏ᶜ fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{wModule} S.O) K).obj ⟨n⟩)
(δ : (∏ᶜ fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{wModule} S.O) K).obj ⟨n⟩) ⟶
L⟦(1 : ℤ)⟧),
Triangle.mk p (Pi.lift fun n : ℕ ↦
Pi.π (fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{wModule} S.O) K).obj ⟨n⟩) n -
Pi.π (fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower
(SheafOfModules.{wModule} S.O) K).obj ⟨n⟩) (n + 1) ≫
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{wModule} S.O) K).map
(homOfLE (Nat.le_succ n)).op) δ ∈
distTriang (DerivedCategory (SheafOfModules.{wModule} S.O)) ∧
(∀ n : ℕ, c ≫ p ≫ Pi.π (fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{wModule} S.O) K).obj ⟨n⟩) n =
(DerivedCategory.TStructure.t.truncGEπ (-(n : ℤ))).app K) ∧ IsIso c
Stacks.Cohomology.isIso_to_isDerivedLimit_truncGETower_of_derivedCategoryB, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedLimit/TruncationConvergenceWeakSerre.lean, line 115.
Stacks Project, Tag 0D6S. In the Olsson--Laszlo situation, for an object
Eof the derived category whose cohomology sheaves all lie in the weak Serre subcategoryA, the canonical map fromEto a derived limit of its tower of truncationsτ_{≥ -n} Efrom below is an isomorphism.
theorem isIso_to_isDerivedLimit_truncGETower_of_derivedCategoryB
(S : OlssonLaszloSituation.{v, u, wRing, wModule})
(E : DerivedCategory (SheafOfModules.{wModule} S.O))
(hE : DerivedCategoryB.derivedCategoryB S.A E)
(L : DerivedCategory (SheafOfModules.{wModule} S.O))
(q : L ⟶ ∏ᶜ fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{wModule} S.O) E).obj ⟨n⟩)
(hL : ∃ δ :
(∏ᶜ fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{wModule} S.O) E).obj ⟨n⟩) ⟶
L⟦(1 : ℤ)⟧,
Triangle.mk q (Pi.lift fun n : ℕ ↦
Pi.π (fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{wModule} S.O) E).obj ⟨n⟩) n -
Pi.π (fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower
(SheafOfModules.{wModule} S.O) E).obj ⟨n⟩) (n + 1) ≫
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{wModule} S.O) E).map
(homOfLE (Nat.le_succ n)).op) δ ∈
distTriang (DerivedCategory (SheafOfModules.{wModule} S.O)))
(c : E ⟶ L)
(hc : ∀ n : ℕ, c ≫ q ≫ Pi.π
(fun n : ℕ ↦
(Stacks.DerivedLimit.truncGETower (SheafOfModules.{wModule} S.O) E).obj ⟨n⟩) n =
(DerivedCategory.TStructure.t.truncGEπ (-(n : ℤ))).app E) :
IsIso c
Tag 0D6T, a lemma
Tag 0D6T in the Stacks Project.
Stacks.Cohomology.isIso_cohomologyToEventuallyConstantValue, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedLimit/EventuallyConstantDerivedLimit.lean, line 229.
Stacks Project, Tag 0D6T. If an inverse system in
D^+_Ahas eventually constant cohomology sheaves with valuesℋʲ, then the canonical map from the cohomology of any presented derived inverse limit toℋʲis an isomorphism, for everyj.
theorem isIso_cohomologyToEventuallyConstantValue
(S : OlssonLaszloSituation.{v, u, wRing, wModule})
(K : ℕᵒᵖ ⥤ DerivedCategory (SheafOfModules.{wModule} S.O))
(hK : ∀ n : ℕ, DerivedCategoryB.derivedCategoryBPlus S.A (K.obj ⟨n⟩))
[HasProduct fun n : ℕ ↦ K.obj ⟨n⟩]
(L : DerivedCategory (SheafOfModules.{wModule} S.O))
(p : L ⟶ ∏ᶜ fun n : ℕ ↦ K.obj ⟨n⟩)
(hL : ∃ δ : (∏ᶜ fun n : ℕ ↦ K.obj ⟨n⟩) ⟶ L⟦(1 : ℤ)⟧,
Triangle.mk p (Pi.lift fun n : ℕ ↦
Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) n -
Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) (n + 1) ≫
K.map (homOfLE (Nat.le_succ n)).op) δ ∈
distTriang (DerivedCategory (SheafOfModules.{wModule} S.O)))
(ℋ : ℤ → SheafOfModules.{wModule} S.O)
(e : ∀ j : ℤ, EventuallyConstantValue
(K ⋙ DerivedCategory.homologyFunctor (SheafOfModules.{wModule} S.O) j) (ℋ j)) :
∀ j : ℤ, IsIso (cohomologyToEventuallyConstantValue S K L p j (ℋ j) (e j))
Tag 0D6U, a lemma
Tag 0D6U in the Stacks Project.
Stacks.Cohomology.OlssonLaszlo.derivedCategoryB_derivedPushforward_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedLimit/PushforwardBoundedCohomologicalDimension.lean, line 908. The attribute's comment: “part (a)”.
Stacks Project, Tag 0D6U, part (a). Let
f : (Sh(C), O) ⟶ (Sh(C'), O')be a morphism of ringed topoi and letA,A'be weak Serre subcategories ofMod(O),Mod(O')for which both sites satisfy the Olsson--Laszlo hypothesis,Rᵖf_*carriesAintoA', andRᵖf_*F = 0forp > NandFinA. ThenRf_*carriesD_A(O)intoD_{A'}(O').
theorem derivedCategoryB_derivedPushforward_obj
(K : DerivedCategory (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
(hK : DerivedCategoryB.derivedCategoryB A K) :
DerivedCategoryB.derivedCategoryB A' ((derivedPushforward f).obj K)
Stacks.Cohomology.OlssonLaszlo.isIso_homology_derivedPushforward_truncGEπ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedLimit/PushforwardBoundedCohomologicalDimension.lean, line 962. The attribute's comment: “part (b)”.
Stacks Project, Tag 0D6U, part (b). In the situation of part (a), the canonical map
Hʲ(Rf_*K) ⟶ Hʲ(Rf_*(τ_{≥ -n}K))induced by the truncationK ⟶ τ_{≥ -n}Kis an isomorphism for everyj ≥ N - n.
theorem isIso_homology_derivedPushforward_truncGEπ
(K : DerivedCategory (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
(hK : DerivedCategoryB.derivedCategoryB A K)
(n : ℕ) (j : ℤ) (hj : N - (n : ℤ) ≤ j) :
IsIso ((DerivedCategory.homologyFunctor
(SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) j).map
((derivedPushforward f).map
((DerivedCategory.TStructure.t.truncGEπ (-(n : ℤ))).app K)))
Tag 0D6V, a situation
Tag 0D6V in the Stacks Project.
Stacks.Cohomology.OlssonLaszloPrimeSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedLimit/OlssonLaszloSituation.lean, line 194.
Stacks 0D6V. The relative Olsson--Laszlo situation for a morphism of ringed sites: the target has a locally covering collection of objects carrying cofinal systems of coverings on whose members the cohomology, on the source site, of the modules of the chosen weak Serre subcategory vanishes above an object-dependent integer bound.
public structure OlssonLaszloPrimeSituation
Tag 0D6W, a lemma
Tag 0D6W in the Stacks Project.
Stacks.Cohomology.OlssonLaszlo.isIso_homology_derivedPushforward_truncGEπ_of_relativeSituation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedLimit/BoundedCohomologicalDimensionPushforward.lean, line 496.
Stacks Project, Tag 0D6W. Let
f : (C, O) ⟶ (C', O')be a morphism of ringed sites, letA ⊂ Mod(O)be a weak Serre subcategory and letNbe an integer such that
C, O, Asatisfy the standing hypothesis of Stacks 0D6R: a classBof objects covering every object ofC, eachV ∈ Bcarrying an integer boundd_Vand a cofinal system of coverings ofVon whose members the cohomology of every module ofAvanishes aboved_V;fandAsatisfy the standing hypothesis of Stacks 0D6V: a classB'of objects covering every object ofC', eachV' ∈ B'carrying an integer boundd_{V'}and a cofinal system of coverings ofV'on the images underfof whose members the cohomology, computed onC, of every module ofAvanishes aboved_{V'};Rᵖf_*F = 0for everyp > Nand everyFofA.Then for every
KofD_A(O)the canonical mapHʲ(Rf_*K) ⟶ Hʲ(Rf_*(τ_{≥ -n}K))induced by the truncationK ⟶ τ_{≥ -n}Kis an isomorphism for everyj ≥ N - n.
theorem isIso_homology_derivedPushforward_truncGEπ_of_relativeSituation
(K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
(hK : DerivedCategoryB.derivedCategoryB A K)
(n : ℕ) (j : ℤ) (hj : N - (n : ℤ) ≤ j) :
IsIso ((DerivedCategory.homologyFunctor
(SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) j).map
((derivedPushforward.{u} f.toRingedToposSiteHom).map
((DerivedCategory.TStructure.t.truncGEπ (-(n : ℤ))).app K)))
Sources
Section21.26 Mayer-Vietoris#
Section 21.26 of the Stacks Project, Tag 0EVX. 4 tags here are carried by 18 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0F16, a lemma
Tag 0F16 in the Stacks Project.
Stacks.MayerVietoris.CanonicalMapOfComplexes.firstMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/MayerVietoris/CanonicalMapOfComplexes.lean, line 561. The attribute's comment: “the map alpha”.
The map
I(X) ⟶ I(Z) ⊞ I(Y).
noncomputable def firstMap (I : CochainComplex (SheafOfModules.{v} R) ℤ) :
(sectionsComplex R sq.X₄).obj I ⟶
(sectionsComplex R sq.X₃).obj I ⊞ (sectionsComplex R sq.X₂).obj I
Stacks.MayerVietoris.CanonicalMapOfComplexes.secondMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/MayerVietoris/CanonicalMapOfComplexes.lean, line 568. The attribute's comment: “the map beta”.
The signed map
I(Z) ⊞ I(Y) ⟶ I(E).
noncomputable def secondMap (I : CochainComplex (SheafOfModules.{v} R) ℤ) :
(sectionsComplex R sq.X₃).obj I ⊞ (sectionsComplex R sq.X₂).obj I ⟶
(sectionsComplex R sq.X₁).obj I
Stacks.MayerVietoris.CanonicalMapOfComplexes.cSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/MayerVietoris/CanonicalMapOfComplexes.lean, line 575. The attribute's comment: “the canonical map of complexes”.
The canonical map
I(X) ⟶ C(β)[-1], using the zero null-homotopy.
noncomputable def cSquare (I : CochainComplex (SheafOfModules.{v} R) ℤ) :
(sectionsComplex R sq.X₄).obj I ⟶ CochainComplex.mappingCocone (secondMap sq I)
Stacks.MayerVietoris.CanonicalMapOfComplexes.firstMap_comp_secondMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/MayerVietoris/CanonicalMapOfComplexes.lean, line 581. The attribute's comment: “the relation beta composed with alpha is zero”.
Signed restriction maps compose to zero.
theorem firstMap_comp_secondMap (I : CochainComplex (SheafOfModules.{v} R) ℤ) :
firstMap sq I ≫ secondMap sq I = 0
Stacks.MayerVietoris.CanonicalMapOfComplexes.cSquare_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/MayerVietoris/CanonicalMapOfComplexes.lean, line 631. The attribute's comment: “functoriality on complexes”.
The chain-level canonical maps commute with chain maps.
theorem cSquare_natural {I I' : CochainComplex (SheafOfModules.{v} R) ℤ} (f : I ⟶ I') :
(sectionsComplex R sq.X₄).map f ≫ cSquare sq I' =
cSquare sq I ≫ mappingCoconeMap sq f
Stacks.MayerVietoris.CanonicalMapOfComplexes.cSquare_arrow_iso_of_isKInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/MayerVietoris/CanonicalMapOfComplexes.lean, line 652. The attribute's comment: “independence of the K-injective representative”.
Changing a K-injective representative gives an isomorphic arrow in
D(Ab).Two K-injective representatives of the same derived object are homotopy equivalent, and the chain-level canonical map is natural; the induced map of mapping cocones is inverted by the localization functor because it is the third component of a morphism of distinguished triangles whose other two components are inverted.
theorem cSquare_arrow_iso_of_isKInjective
(K : DerivedCategory (SheafOfModules.{v} R))
(I I' : CochainComplex (SheafOfModules.{v} R) ℤ)
[I.IsKInjective] [I'.IsKInjective]
(_ : DerivedCategory.Q.obj I ≅ K) (_ : DerivedCategory.Q.obj I' ≅ K) :
Nonempty (Arrow.mk (DerivedCategory.Q.map (cSquare sq I)) ≅
Arrow.mk (DerivedCategory.Q.map (cSquare sq I')))
Stacks.MayerVietoris.CanonicalMapOfComplexes.DerivedCSquareData.cSquareTriangle, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/MayerVietoris/DerivedCanonicalMapAndTriangle.lean, line 1147. The attribute's comment: “the canonical triangle on derived objects”.
The triangle on derived sections, with boundary obtained using the inverse of
c.
noncomputable def cSquareTriangle (K : DerivedCategory (SheafOfModules.{v} R))
[D.IsCSquareIso K] : Triangle (DerivedCategory AddCommGrpCat.{v})
Stacks.MayerVietoris.CanonicalMapOfComplexes.DerivedCSquareData.isCSquareIso_iff_quasiIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/MayerVietoris/DerivedCanonicalMapAndTriangle.lean, line 1154. The attribute's comment: “computation of the isomorphism condition”.
The canonical condition on a derived object can be tested on any K-injective representative.
theorem isCSquareIso_iff_quasiIso (K : DerivedCategory (SheafOfModules.{v} R))
(I : CochainComplex (SheafOfModules.{v} R) ℤ) [I.IsKInjective]
(e : DerivedCategory.Q.obj I ≅ K) :
D.IsCSquareIso K ↔ QuasiIso (cSquare sq I)
Stacks.MayerVietoris.CanonicalMapOfComplexes.DerivedCSquareData.cSquareTriangle_functorial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/MayerVietoris/DerivedCanonicalMapAndTriangle.lean, line 1163. The attribute's comment: “functoriality of the triangle in the derived object”.
Every derived morphism induces a unique morphism of the derived triangles with the given three components.
theorem cSquareTriangle_functorial {K K' : DerivedCategory (SheafOfModules.{v} R)} (f : K ⟶ K')
[D.IsCSquareIso K] [D.IsCSquareIso K'] :
∃! t : D.cSquareTriangle K ⟶ D.cSquareTriangle K',
t.hom₁ = (D.derivedSections sq.X₄).map f ∧
t.hom₂ = biprod.map ((D.derivedSections sq.X₃).map f)
((D.derivedSections sq.X₂).map f) ∧
t.hom₃ = (D.derivedSections sq.X₁).map f
Stacks.MayerVietoris.CanonicalMapOfComplexes.derivedCSquareData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/MayerVietoris/DerivedCanonicalMapAndTriangle.lean, line 1319. The attribute's comment: “the functorial derived construction and its K-injective computation”.
The derived construction of the canonical map of a square, under
UnivLEbetween the universes of the site, of its homs, of the rings and of the modules.
noncomputable def derivedCSquareData [UnivLE.{u, v}] [UnivLE.{w, v}] [UnivLE.{r, v}] :
DerivedCSquareData.{u, v} (R := R) sq
Stacks.MayerVietoris.CanonicalMapOfComplexes.cSquareTriangle_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/MayerVietoris/DerivedCanonicalMapAndTriangle.lean, line 1330. The attribute's comment: “the triangle is distinguished”.
The derived-section triangle is distinguished at every derived object where the canonical map is invertible, under
UnivLEbetween the universes of the site, of its homs, of the rings and of the modules.
theorem cSquareTriangle_distinguished [UnivLE.{u, v}] [UnivLE.{w, v}] [UnivLE.{r, v}]
(K : DerivedCategory (SheafOfModules.{v} R))
[(derivedCSquareData.{u, v} (R := R) sq).IsCSquareIso K] :
(derivedCSquareData.{u, v} (R := R) sq).cSquareTriangle K ∈
distTriang (DerivedCategory AddCommGrpCat.{v})
Tag 0EWP, a lemma
Tag 0EWP in the Stacks Project.
Stacks.MayerVietoris.CanonicalMapOfComplexes.isCSquareIso_obj₃_of_distTriang, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/MayerVietoris/TwoOutOfThree.lean, line 390. The attribute's comment: “first and second vertices imply the third”.
Stacks Project, Tag 0EWP. The comparison for the third vertex is an isomorphism if it is so for the first two vertices of a distinguished triangle.
theorem isCSquareIso_obj₃_of_distTriang
(T : Triangle (DerivedCategory
(SheafOfModules.{v} (Stacks.SheafOfModules.Tensor.ringSheaf S.O))))
(hT : T ∈ distTriang (DerivedCategory
(SheafOfModules.{v} (Stacks.SheafOfModules.Tensor.ringSheaf S.O))))
(h₁ : (derivedCSquareData.{u, v} (R := (Stacks.SheafOfModules.Tensor.ringSheaf S.O))
sq).IsCSquareIso T.obj₁)
(h₂ : (derivedCSquareData.{u, v} (R := (Stacks.SheafOfModules.Tensor.ringSheaf S.O))
sq).IsCSquareIso T.obj₂) :
(derivedCSquareData.{u, v} (R := (Stacks.SheafOfModules.Tensor.ringSheaf S.O))
sq).IsCSquareIso T.obj₃
Stacks.MayerVietoris.CanonicalMapOfComplexes.isCSquareIso_obj₁_of_distTriang, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/MayerVietoris/TwoOutOfThree.lean, line 406. The attribute's comment: “second and third vertices imply the first”.
Stacks Project, Tag 0EWP. The comparison for the first vertex is an isomorphism if it is so for the second and third vertices of a distinguished triangle.
theorem isCSquareIso_obj₁_of_distTriang
(T : Triangle (DerivedCategory
(SheafOfModules.{v} (Stacks.SheafOfModules.Tensor.ringSheaf S.O))))
(hT : T ∈ distTriang (DerivedCategory
(SheafOfModules.{v} (Stacks.SheafOfModules.Tensor.ringSheaf S.O))))
(h₂ : (derivedCSquareData.{u, v} (R := (Stacks.SheafOfModules.Tensor.ringSheaf S.O))
sq).IsCSquareIso T.obj₂)
(h₃ : (derivedCSquareData.{u, v} (R := (Stacks.SheafOfModules.Tensor.ringSheaf S.O))
sq).IsCSquareIso T.obj₃) :
(derivedCSquareData.{u, v} (R := (Stacks.SheafOfModules.Tensor.ringSheaf S.O))
sq).IsCSquareIso T.obj₁
Stacks.MayerVietoris.CanonicalMapOfComplexes.isCSquareIso_obj₂_of_distTriang, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/MayerVietoris/TwoOutOfThree.lean, line 422. The attribute's comment: “first and third vertices imply the second”.
Stacks Project, Tag 0EWP. The comparison for the second vertex is an isomorphism if it is so for the first and third vertices of a distinguished triangle.
theorem isCSquareIso_obj₂_of_distTriang
(T : Triangle (DerivedCategory
(SheafOfModules.{v} (Stacks.SheafOfModules.Tensor.ringSheaf S.O))))
(hT : T ∈ distTriang (DerivedCategory
(SheafOfModules.{v} (Stacks.SheafOfModules.Tensor.ringSheaf S.O))))
(h₁ : (derivedCSquareData.{u, v} (R := (Stacks.SheafOfModules.Tensor.ringSheaf S.O))
sq).IsCSquareIso T.obj₁)
(h₃ : (derivedCSquareData.{u, v} (R := (Stacks.SheafOfModules.Tensor.ringSheaf S.O))
sq).IsCSquareIso T.obj₃) :
(derivedCSquareData.{u, v} (R := (Stacks.SheafOfModules.Tensor.ringSheaf S.O))
sq).IsCSquareIso T.obj₂
Tag 0EVY, a lemma
Tag 0EVY in the Stacks Project.
Stacks.Cohomology.MayerVietoris.isIso_derivedCSquare_of_isPushout, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/MayerVietoris/TriangleOfAPushoutSquare.lean, line 196.
Stacks 0EVY. If the sheafified representables of the square form a pushout square and
h_E^# ⟶ h_Y^#is a monomorphism, then the canonical natural transformation of Stacks 0F16 is an isomorphism, so that the Mayer-Vietoris triangle is distinguished and functorial for every object of the derived category of module sheaves.
theorem isIso_derivedCSquare_of_isPushout (sq : Square S.C)
(hpushout : (sq.map (Sheaf.sheafifiedYoneda S.J)).IsPushout)
(hmono : Mono ((Sheaf.sheafifiedYoneda S.J).map sq.f₁₂)) :
IsIso (CanonicalMapOfComplexes.derivedCSquareData.{u, v}
(R := (Stacks.SheafOfModules.Tensor.ringSheaf S.O)) sq).derivedCSquare
Tag 0EVZ, a lemma
Tag 0EVZ in the Stacks Project.
Stacks.MayerVietoris.PresheafSquare.isIso_derivedCSquare_of_isPushout, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/MayerVietoris/TriangleOfAPresheafPushoutSquare.lean, line 126. The attribute's comment: “the canonical comparison”.
Stacks 0EVZ. If the sheafifications of a square of presheaves of sets form a pushout square and
D^# ⟶ F^#is a monomorphism, then the canonical natural transformation of Stacks 0F16 from derived sections overGto the mapping cocone is an isomorphism, so that the Mayer–Vietoris triangle is defined at every object of the derived category of abelian sheaves.
theorem isIso_derivedCSquare_of_isPushout
(hpushout : (sq.map (presheafToSheaf J (Type u))).IsPushout)
(hmono : Mono ((presheafToSheaf J (Type u)).map sq.f₁₂)) :
IsIso (derivedCSquareData J sq).derivedCSquare
Stacks.MayerVietoris.PresheafSquare.cSquareTriangle_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/MayerVietoris/TriangleOfAPresheafPushoutSquare.lean, line 161. The attribute's comment: “the triangle is distinguished”.
Stacks 0EVZ. The Mayer–Vietoris triangle of a square of presheaves of sets whose sheafifications form a pushout square with monomorphic
D^# ⟶ F^#is a distinguished triangle of the derived category of abelian groups, at every object of the derived category of abelian sheaves.
theorem cSquareTriangle_distinguished (K : DerivedCategory (Sheaf J AddCommGrpCat.{u})) :
cSquareTriangle J sq hpushout hmono K ∈ distTriang (DerivedCategory AddCommGrpCat.{u})
Stacks.MayerVietoris.PresheafSquare.cSquareTriangle_functorial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/MayerVietoris/TriangleOfAPresheafPushoutSquare.lean, line 170. The attribute's comment: “functoriality of the triangle in the derived object”.
Stacks 0EVZ, the functoriality in the derived object. Every morphism of derived objects induces a unique morphism of Mayer–Vietoris triangles whose three components are the maps induced on derived sections and on the mapping cocone.
theorem cSquareTriangle_functorial
{K K' : DerivedCategory (Sheaf J AddCommGrpCat.{u})} (f : K ⟶ K') :
∃! t : cSquareTriangle J sq hpushout hmono K ⟶ cSquareTriangle J sq hpushout hmono K',
t.hom₁ = ((derivedCSquareData J sq).derivedSections sq.X₄).map f ∧
t.hom₂ = ((derivedCSquareData J sq).sectionsData.biprodFunctor sq).map f ∧
t.hom₃ = ((derivedCSquareData J sq).derivedSections sq.X₁).map f
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.