21.39 Homology on a category to 21.45 Pseudo-coherent modules

Section21.39 Homology on a category#

Section 21.39 of the Stacks Project, Tag 08RW. 13 tags here are carried by 87 declarations of the repository (all in StacksFrontier) and 17 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 08PF, an example

Tag 08PF in the Stacks Project.

Stacks.CategoryHomology.categoryHomology, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/HomologyOnACategory.lean, line 144. The attribute's comment: “homology_of_a_category”.

Stacks 08PF. The nth homology group of an abelian-group-valued presheaf on a small category is the value of the nth left derived functor of colim.

noncomputable abbrev categoryHomology {C : Type u} [SmallCategory C]
    (F : Cᵒᵖ ⥤ AddCommGrpCat.{max u v}) (n : ℕ) : AddCommGrpCat.{max u v}

Stacks.ChaoticSite.abelianLowerShriekColimitIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/LowerShriekAsAColimit.lean, line 219. The attribute's comment: “lower_shriek_colimit”.

Stacks 08PF. The established inverse image along the point, left adjoint to restriction, is canonically the colimit functor.

def abelianLowerShriekColimitIso :
    (Functor.star C).sheafPullback AddCommGrpCat.{max w (u + 1) v}
      (GrothendieckTopology.trivial C)
      (GrothendieckTopology.trivial (Discrete PUnit.{u + 1})) ≅
      abelianColimitLowerShriek.{w} C

Stacks.ChaoticSite.abelianLowerShriekColimitIso_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/LowerShriekAsAColimit.lean, line 232. The attribute's comment: “lower_shriek_colimit”.

Stacks 08PF. The abelian comparison preserves the canonical unit.

theorem abelianLowerShriekColimitIso_unit
    (F : Sheaf (GrothendieckTopology.trivial C) AddCommGrpCat.{max w (u + 1) v}) :
    ((Functor.star C).sheafAdjunctionContinuous AddCommGrpCat.{max w (u + 1) v}
      (GrothendieckTopology.trivial C)
      (GrothendieckTopology.trivial (Discrete PUnit.{u + 1}))).unit.app F ≫
      ((Functor.star C).sheafPushforwardContinuous AddCommGrpCat.{max w (u + 1) v}
        (GrothendieckTopology.trivial C)
        (GrothendieckTopology.trivial (Discrete PUnit.{u + 1}))).map
          ((abelianLowerShriekColimitIso.{w} C).hom.app F) =
    (abelianLowerShriekColimitAdjunction.{w} C).unit.app F

Stacks.ChaoticSite.abelianLowerShriekColimit_evalIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/LowerShriekAsAColimit.lean, line 247. The attribute's comment: “lower_shriek_colimit”.

Stacks 08PF. At each object, the colimit presentation evaluated at the point is the colimit of the underlying presheaf.

def abelianLowerShriekColimit_evalIso
    (F : Sheaf (GrothendieckTopology.trivial C) AddCommGrpCat.{max w (u + 1) v}) :
    ((abelianColimitLowerShriek.{w} C).obj F).obj.obj
      (op (Discrete.mk PUnit.unit)) ≅ colimit F.obj

Stacks.ChaoticSite.abelianLowerShriekColimit_unit_cocone, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/LowerShriekAsAColimit.lean, line 262. The attribute's comment: “lower_shriek_colimit”.

Stacks 08PF. At each object, the unit of the colimit presentation is the canonical map into the colimit of the underlying presheaf.

theorem abelianLowerShriekColimit_unit_cocone
    (F : Sheaf (GrothendieckTopology.trivial C) AddCommGrpCat.{max w (u + 1) v}) (U : C) :
    ((abelianLowerShriekColimitAdjunction.{w} C).unit.app F).hom.app (op U) ≫
      (abelianLowerShriekColimit_evalIso.{w} C F).hom =
      colimit.ι F.obj (op U)

Stacks.ChaoticSite.ModuleValued.moduleLowerShriekColimitIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/LowerShriekAsAColimitOfModules.lean, line 111. The attribute's comment: “lower_shriek_colimit”.

Stacks 08PF. The established lower shriek on module-valued sheaves is naturally the colimit functor, rather than merely another left adjoint to point restriction.

def moduleLowerShriekColimitIso :
    (Functor.star s.C).sheafPullback (ModuleCat.{max w (u + 1) v} s.B)
      (GrothendieckTopology.trivial s.C)
      (GrothendieckTopology.trivial (Discrete PUnit.{u + 1})) ≅
      moduleColimitLowerShriek s

Stacks.ChaoticSite.ModuleValued.moduleLowerShriekColimitIso_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/LowerShriekAsAColimitOfModules.lean, line 124. The attribute's comment: “lower_shriek_colimit”.

Stacks 08PF. The module comparison preserves the canonical unit.

theorem moduleLowerShriekColimitIso_unit
    (F : Sheaf (GrothendieckTopology.trivial s.C) (ModuleCat.{max w (u + 1) v} s.B)) :
    ((Functor.star s.C).sheafAdjunctionContinuous (ModuleCat.{max w (u + 1) v} s.B)
      (GrothendieckTopology.trivial s.C)
      (GrothendieckTopology.trivial (Discrete PUnit.{u + 1}))).unit.app F ≫
      ((Functor.star s.C).sheafPushforwardContinuous (ModuleCat.{max w (u + 1) v} s.B)
        (GrothendieckTopology.trivial s.C)
        (GrothendieckTopology.trivial (Discrete PUnit.{u + 1}))).map
          ((moduleLowerShriekColimitIso s).hom.app F) =
    (moduleLowerShriekColimitAdjunction s).unit.app F

Stacks.ChaoticSite.ModuleValued.moduleLowerShriekColimit_evalIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/LowerShriekAsAColimitOfModules.lean, line 139. The attribute's comment: “lower_shriek_colimit”.

Stacks 08PF. At each object, the colimit presentation evaluated at the point is the colimit of the underlying presheaf of modules.

def moduleLowerShriekColimit_evalIso
    (F : Sheaf (GrothendieckTopology.trivial s.C) (ModuleCat.{max w (u + 1) v} s.B)) :
    ((moduleColimitLowerShriek s).obj F).obj.obj
      (op (Discrete.mk PUnit.unit)) ≅ colimit F.obj

Stacks.ChaoticSite.ModuleValued.moduleLowerShriekColimit_unit_cocone, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/LowerShriekAsAColimitOfModules.lean, line 154. The attribute's comment: “lower_shriek_colimit”.

Stacks 08PF. At each object, the unit of the colimit presentation is the canonical map into the colimit of the underlying presheaf of modules.

theorem moduleLowerShriekColimit_unit_cocone
    (F : Sheaf (GrothendieckTopology.trivial s.C) (ModuleCat.{max w (u + 1) v} s.B)) (U : s.C) :
    ((moduleLowerShriekColimitAdjunction s).unit.app F).hom.app (op U) ≫
      (moduleLowerShriekColimit_evalIso s F).hom =
      colimit.ι F.obj (op U)

Stacks.ChaoticSite.pointFunctor_isContinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/PointMorphism.lean, line 84. The attribute's comment: “point_morphism”.

Stacks 08PF, point morphism (continuity). The unique functor to the one-object category is continuous when both categories carry the chaotic topology.

instance pointFunctor_isContinuous (C : Type u) [Category.{v} C] :
    (Functor.star C).IsContinuous
    (GrothendieckTopology.trivial C)
    (GrothendieckTopology.trivial (Discrete PUnit.{u + 1}))

Stacks.ChaoticSite.pointFunctor_isCocontinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/PointMorphism.lean, line 94. The attribute's comment: “point_morphism”.

Stacks 08PF, point morphism (cocontinuity). The unique functor to the one-object category is cocontinuous when both categories carry the chaotic topology.

instance pointFunctor_isCocontinuous (C : Type u) [Category.{v} C] :
    (Functor.star C).IsCocontinuous
    (GrothendieckTopology.trivial C)
    (GrothendieckTopology.trivial (Discrete PUnit.{u + 1}))

Stacks.ChaoticSite.pointMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/PointMorphism.lean, line 104. The attribute's comment: “point_morphism”.

Stacks 08PF, point morphism. A category with the chaotic topology has a canonical morphism from its sheaf topos to the point topos, induced by the unique functor to the one-object category.

noncomputable def pointMorphism (C : Type u) [Category.{v} C] :
    MorphismOfTopoi
      (Sheaf (GrothendieckTopology.trivial C) (Type (max w u v)))
      (Sheaf (GrothendieckTopology.trivial (Discrete PUnit.{u + 1}))
        (Type (max w u v)))

Stacks.ChaoticSite.pointMorphism_inverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/PointMorphism.lean, line 117. The attribute's comment: “point_morphism”.

The inverse image of the point morphism is restriction along the point functor.

theorem pointMorphism_inverseImage (C : Type u) [Category.{v} C] :
    (pointMorphism C).inverseImage =
      (Functor.star C).sheafPushforwardContinuous (Type (max w u v))
        (GrothendieckTopology.trivial C)
        (GrothendieckTopology.trivial (Discrete PUnit.{u + 1}))

Stacks.ChaoticSite.pointMorphism_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/PointMorphism.lean, line 126. The attribute's comment: “point_morphism”.

The direct image of the point morphism is the right Kan extension along the point functor.

theorem pointMorphism_pushforward (C : Type u) [Category.{v} C] :
    (pointMorphism C).pushforward =
      (Functor.star C).sheafPushforwardCocontinuous (Type (max w u v))
        (GrothendieckTopology.trivial C)
        (GrothendieckTopology.trivial (Discrete PUnit.{u + 1}))

Stacks.ChaoticSite.pointMorphism_adjunction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/PointMorphism.lean, line 135. The attribute's comment: “point_morphism”.

The adjunction of the point morphism is the canonical adjunction between restriction and the cocontinuous pushforward along the point functor.

theorem pointMorphism_adjunction (C : Type u) [Category.{v} C] :
    (pointMorphism C).adj =
      (Functor.star C).sheafAdjunctionCocontinuous (Type (max w u v))
        (GrothendieckTopology.trivial C)
        (GrothendieckTopology.trivial (Discrete PUnit.{u + 1}))

Stacks.ChaoticSite.pointFunctor_isFibered, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/RingedPoint.lean, line 82. The attribute's comment: “ringed_point”.

The projection of any category to the one-object category is a fibred category: every morphism of the base is an identity, and an identity lifts to an identity, which is strongly cartesian because it is an isomorphism.

instance pointFunctor_isFibered (C : Type u) [Category.{v} C] :
    (Functor.star C).IsFibered

Stacks.ChaoticSite.RingedPointSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/RingedPoint.lean, line 94. The attribute's comment: “ringed_point”.

A category with its chaotic topology and a ring on the point.

structure RingedPointSituation

Stacks.ChaoticSite.RingedPointSituation.fibredSituation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/RingedPoint.lean, line 119. The attribute's comment: “ringed_point”.

The fibred-category situation of Stacks 08P8 obtained from the unique functor to the ringed point.

def fibredSituation :
    Stacks.Sites.FibredCategory.FibredCategorySituation.{u, u, u, v, max w u v}

Stacks.ChaoticSite.RingedPointSituation.topology_eq_trivial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/RingedPoint.lean, line 143. The attribute's comment: “ringed_point”.

Stacks 08PF. The topology that C inherits from the chaotic point is the chaotic topology.

theorem topology_eq_trivial :
    s.fibredSituation.topology = GrothendieckTopology.trivial s.C

Stacks.ChaoticSite.RingedPointSituation.projection_eq_pointMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/RingedPoint.lean, line 200. The attribute's comment: “ringed_point”.

Stacks 08PF. The morphism of topoi underlying the ringed projection is the point morphism of the chaotic site.

theorem projection_eq_pointMorphism :
    HEq s.fibredSituation.projection (pointMorphism.{max w u v, v, u} s.C)

Declarations registered for the tag:

Tag 08PG, an example

Tag 08PG in the Stacks Project.

Stacks.CategoryHomology.categoryHomologyReplacementIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/DerivedColimits.lean, line 220. The attribute's comment: “derived_colimits”.

The homology of the simplicial replacement complex of an abelian-group-valued presheaf computes the left derived functors of the colimit, that is the homology groups H_n(C, F): the component at F of Stacks.CategoryHomology.categoryHomologyReplacementNatIso.

def categoryHomologyReplacementIso (F : Cᵒᵖ ⥤ AddCommGrpCat.{max u v}) (n : ℕ) :
    categoryHomology.{u, v} F n ≅ (simplicialReplacementComplex F).homology n

Stacks.CategoryHomology.representableReplacementComplex_homology_isZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/RepresentableAcyclicity.lean, line 71. The attribute's comment: “representable_acyclic”.

The simplicial replacement complex of the extension by zero of the constant integer sheaf from the slice site over U has vanishing homology in every positive degree.

theorem representableReplacementComplex_homology_isZero (U : C) (n : ℕ) (hn : 0 < n) :
    IsZero
      ((simplicialReplacementComplex
        ((sheafToPresheaf (GrothendieckTopology.trivial C) AddCommGrpCat.{u}).obj
          (integerExtensionByZero U))).homology n)

Stacks.CategoryHomology.overSimplexEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/RepresentableReplacementAsANerve.lean, line 108. The attribute's comment: “representable_contractible”.

A string in the slice category is a string in C together with a map from its right endpoint to U.

def overSimplexEquiv (n : ℕ) :
    (Σ x : ComposableArrows C n, x.right ⟶ U) ≃
      ComposableArrows (Over U) n

Stacks.CategoryHomology.overSimplexEquiv_forget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/RepresentableReplacementAsANerve.lean, line 152. The attribute's comment: “representable_contractible”.

The simplex comparison preserves the underlying string of arrows.

theorem overSimplexEquiv_forget (n : ℕ)
    (a : Σ x : ComposableArrows C n, x.right ⟶ U) :
    overSimplexEquiv U n a ⋙ Over.forget U = a.1

Stacks.CategoryHomology.overSimplexEquiv_last, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/RepresentableReplacementAsANerve.lean, line 163. The attribute's comment: “representable_contractible”.

The last object of the compared simplex has the prescribed arrow to U.

theorem overSimplexEquiv_last (n : ℕ)
    (a : Σ x : ComposableArrows C n, x.right ⟶ U) :
    HEq ((overSimplexEquiv U n a).obj (Fin.last n)).hom a.2

Stacks.CategoryHomology.integerExtensionByZero_iso_freeYoneda, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/RepresentableReplacementAsANerve.lean, line 182. The attribute's comment: “representable_contractible”.

On a chaotic site, extension by zero of the constant integer sheaf is the free abelian presheaf represented by U.

def integerExtensionByZero_iso_freeYoneda :
    (sheafToPresheaf (GrothendieckTopology.trivial C) AddCommGrpCat.{u}).obj
        (integerExtensionByZero U) ≅
      ((yoneda.obj U) ⋙ AddCommGrpCat.free)

Stacks.CategoryHomology.representableReplacementComplexIsoFreeNerve, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/RepresentableReplacementAsANerve.lean, line 369. The attribute's comment: “representable_contractible”.

The simplicial replacement complex of the extension by zero of the constant integer sheaf is isomorphic to the free abelian chain complex on the nerve of the category over U.

def representableReplacementComplexIsoFreeNerve :
    simplicialReplacementComplex
        ((sheafToPresheaf (GrothendieckTopology.trivial C) AddCommGrpCat.{u}).obj
          (integerExtensionByZero U)) ≅
      (AlgebraicTopology.alternatingFaceMapComplex _).obj
        (((SimplicialObject.whiskering (Type u) AddCommGrpCat).obj
          AddCommGrpCat.free).obj (nerve (Over U)))

Stacks.CategoryHomology.representableReplacementComplexIsoFreeNerve_generator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/RepresentableReplacementAsANerve.lean, line 382. The attribute's comment: “representable_contractible”.

The chain-complex comparison takes the generator indexed by a string and an arrow to U to the corresponding simplex of the slice category.

theorem representableReplacementComplexIsoFreeNerve_generator
    (n : ℕ) (x : ComposableArrows C n) (f : x.right ⟶ U) :
    (representableReplacementComplexIsoFreeNerve U).hom.f n
      ((@DirectSum.of (ComposableArrows C n)
        (fun y => ((sheafToPresheaf (GrothendieckTopology.trivial C)
          AddCommGrpCat.{u}).obj (integerExtensionByZero U)).obj (op y.right))
        _ (Classical.decEq _) x)
        (((integerExtensionByZero_iso_freeYoneda U).inv.app (op x.right))
          (FreeAbelianGroup.of f))) =
      FreeAbelianGroup.of (overSimplexEquiv U n ⟨x, f⟩)

Stacks.CategoryHomology.nerveOver_homotopyEquivalent_point, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/RepresentableReplacementAsANerve.lean, line 434. The attribute's comment: “representable_contractible”.

The nerve of the category over U, the simplicial set of strings of arrows ending in an arrow to U, is homotopy equivalent to a point.

theorem nerveOver_homotopyEquivalent_point :
    ∃ f : nerve (Over U) ⟶ (Functor.const SimplexCategoryᵒᵖ).obj PUnit.{u + 1},
      (SimplicialObject.homotopyEquivalences (Type u)) f

Stacks.CategoryHomology.simplicialReplacementComplex, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/SimplicialReplacement.lean, line 176. The attribute's comment: “simplicial_replacement_complex”.

Stacks 08PG, the simplicial replacement complex. The chain complex whose degree-n term is ⊕_(Uₙ → ⋯ → U₀) F(U₀) and whose differential is the alternating sum of the face maps.

noncomputable abbrev simplicialReplacementComplex
    (F : Cᵒᵖ ⥤ AddCommGrpCat.{v}) : ChainComplex AddCommGrpCat.{max u v} ℕ

Stacks.CategoryHomology.simplicialReplacementHomologyDeltaFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/SimplicialReplacementDeltaFunctor.lean, line 309. The attribute's comment: “delta_functor”.

Stacks Project, Tag 08PG (delta-functor). Homology of the simplicial replacement, with the natural connecting maps of degreewise short exact sequences, is a homological delta-functor. Its functor in degree n is exactly homology in degree n.

noncomputable def simplicialReplacementHomologyDeltaFunctor :
    { D : HomologicalDeltaFunctor
        (Sheaf (GrothendieckTopology.trivial C) AddCommGrpCat.{v})
        AddCommGrpCat.{max u v} //
      ∀ n, D.functor n = chaoticSheafReplacementComplexFunctor (C := C) ⋙
        HomologicalComplex.homologyFunctor AddCommGrpCat.{max u v} (ComplexShape.down ℕ) n }
Tag 08PH, an example

Tag 08PH in the Stacks Project.

Stacks.CategoryHomology.replacementChainMap_homologyMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/ExplicitChainMapOnHomology.lean, line 430. The attribute's comment: “the displayed chain map on homology”.

Stacks 08PH, the identification of the homology map. Under the comparison of Stacks 08PG between the homology of a category and the homology of its simplicial replacement, the explicit chain map K_•(F') ⟶ K_•(F) induced by a functor f : C' ⥤ C and a morphism t : F' ⟶ f⁻¹F induces the canonical map Stacks.CategoryHomology.categoryHomologyMap.

The coefficient half is the naturality of the 08PG comparison; the index half is homologyMapAux_homologyMap, which rests on the canonical map being a morphism of homological δ-functors.

theorem replacementChainMap_homologyMap (f : C' ⥤ C)
    {F : Cᵒᵖ ⥤ AddCommGrpCat.{max u u' v}} {F' : C'ᵒᵖ ⥤ AddCommGrpCat.{max u u' v}}
    (t : F' ⟶ f.op ⋙ F) (n : ℕ) :
    (categoryHomologyReplacementIso.{u', max u v} F' n).hom ≫
        HomologicalComplex.homologyMap (replacementChainMap f t) n =
      categoryHomologyMap f t n ≫ (categoryHomologyReplacementIso.{u, max u' v} F n).hom

Stacks.CategoryHomology.categoryHomologyMapData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/Functoriality.lean, line 386. The attribute's comment: “homology_map”.

The canonical maps on the homology of a category induced by an indexing functor and a coefficient morphism, together with their invariance under natural isomorphisms of indexing functors.

def categoryHomologyMapData (F : Cᵒᵖ ⥤ AddCommGrpCat.{max u u' v})
    (F' : C'ᵒᵖ ⥤ AddCommGrpCat.{max u u' v}) (n : ℕ) : CategoryHomologyMapData F F' n

Stacks.CategoryHomology.categoryHomologyMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/Functoriality.lean, line 397. The attribute's comment: “homology_map”.

The canonical map on homology induced by a functor f : C' ⥤ C and a morphism t : F' ⟶ f.op ⋙ F to the inverse-image presheaf.

def categoryHomologyMap (f : C' ⥤ C) {F : Cᵒᵖ ⥤ AddCommGrpCat.{max u u' v}}
    {F' : C'ᵒᵖ ⥤ AddCommGrpCat.{max u u' v}} (t : F' ⟶ f.op ⋙ F) (n : ℕ) :
    categoryHomology.{u', max u v} F' n ⟶ categoryHomology.{u, max u' v} F n

Stacks.CategoryHomology.categoryHomologyMap_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/Functoriality.lean, line 405. The attribute's comment: “homology_map”.

Naturally isomorphic functors induce the same map on category homology when the coefficient morphisms agree under the induced reindexing isomorphism.

theorem categoryHomologyMap_iso (f g : C' ⥤ C) (e : f ≅ g)
    {F : Cᵒᵖ ⥤ AddCommGrpCat.{max u u' v}} {F' : C'ᵒᵖ ⥤ AddCommGrpCat.{max u u' v}}
    (t : F' ⟶ f.op ⋙ F) (s : F' ⟶ g.op ⋙ F)
    (h : t = s ≫ Functor.whiskerRight (NatTrans.op e.hom) F) (n : ℕ) :
    categoryHomologyMap f t n = categoryHomologyMap g s n

Stacks.CategoryHomology.categoryHomologyMap_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/Functoriality.lean, line 415. The attribute's comment: “homology_map”.

The canonical map associated with the identity functor and the identity coefficient morphism is the identity on homology.

theorem categoryHomologyMap_id {C : Type u} [SmallCategory C]
    (F : Cᵒᵖ ⥤ AddCommGrpCat.{max u v}) (n : ℕ) :
    categoryHomologyMap (𝟭 C) (𝟙 F) n = 𝟙 _

Stacks.CategoryHomology.categoryHomologyMap_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/Functoriality.lean, line 424. The attribute's comment: “homology_map”.

Canonical homology maps compose under successive functors and coefficient morphisms.

theorem categoryHomologyMap_comp {C : Type u} {C' : Type u'} {C'' : Type u''} [SmallCategory C]
    [SmallCategory C'] [SmallCategory C''] (f : C' ⥤ C) (g : C'' ⥤ C')
    {F : Cᵒᵖ ⥤ AddCommGrpCat.{max u u' u'' v}} {F' : C'ᵒᵖ ⥤ AddCommGrpCat.{max u u' u'' v}}
    {F'' : C''ᵒᵖ ⥤ AddCommGrpCat.{max u u' u'' v}} (t : F' ⟶ f.op ⋙ F) (s : F'' ⟶ g.op ⋙ F')
    (n : ℕ) :
    categoryHomologyMap.{u, u'', max u' v} (g ⋙ f) (s ≫ Functor.whiskerLeft g.op t) n =
      categoryHomologyMap.{u', u'', max u v} g s n ≫
        categoryHomologyMap.{u, u', max u'' v} f t n

Stacks.CategoryHomology.replacementChainMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/SimplicialReplacementChainMap.lean, line 146. The attribute's comment: “the displayed chain map”.

The map of simplicial replacement complexes K_•(F') ⟶ K_•(F) induced by a functor f : C' ⥤ C and a morphism t : F' ⟶ f.op ⋙ F of abelian presheaves.

noncomputable def replacementChainMap (f : C' ⥤ C)
    {F : Cᵒᵖ ⥤ AddCommGrpCat.{max u u' v}} {F' : C'ᵒᵖ ⥤ AddCommGrpCat.{max u u' v}}
    (t : F' ⟶ f.op ⋙ F) :
    simplicialReplacementComplex F' ⟶ simplicialReplacementComplex F

Stacks.CategoryHomology.replacementChainMap_on_summand, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/SimplicialReplacementChainMap.lean, line 156. The attribute's comment: “the displayed chain map on summands”.

On the summand indexed by a string of arrows of C', the chain map Stacks.CategoryHomology.replacementChainMap applies f to that string and the coefficient morphism t at its right endpoint.

theorem replacementChainMap_on_summand (f : C' ⥤ C)
    {F : Cᵒᵖ ⥤ AddCommGrpCat.{max u u' v}} {F' : C'ᵒᵖ ⥤ AddCommGrpCat.{max u u' v}}
    (t : F' ⟶ f.op ⋙ F) (n : ℕ)
    (x : ComposableArrows C' n) (s : F'.obj (op x.right)) :
    ((replacementChainMap f t).f n).hom (replacementSummand F' n x s) =
      replacementSummand F n ((f.mapComposableArrows n).obj x)
        ((t.app (op x.right)).hom s)

Declarations registered for the tag:

Tag 08Q6, a remark

Tag 08Q6 in the Stacks Project.

Stacks.CategoryHomology.evaluationToTotalDerivedColimit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/EvaluationToDerivedColimit.lean, line 506. The attribute's comment: “the canonical map”.

The canonical map F^•(U) ⟶ Lπ_!(F^•). For a complex F^• of diagrams on Cᵒᵖ and an object U of C, the canonical map F^•(U) ⟶ Lπ_!(F^•) in the unbounded derived category, natural in F^•. For D = AddCommGrpCat this is a map in D(Ab), and for D = ModuleCat B it is the same map read in D(B).

def evaluationToTotalDerivedColimit (U : C) :
    ((evaluation Cᵒᵖ D).obj (op U)).mapHomologicalComplex (ComplexShape.up ℤ) ⋙
        DerivedCategory.Q ⟶
      DerivedCategory.Q ⋙ totalDerivedColimit C D

Stacks.CategoryHomology.evaluationToTotalDerivedColimit_comp_counit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/EvaluationToDerivedColimit.lean, line 521. The attribute's comment: “the canonical map”.

The canonical map is the colimit cocone. After the canonical comparisons of the total left derived functor with the degreewise colimit, the map of evaluationToTotalDerivedColimit is the colimit cocone of the complex.

theorem evaluationToTotalDerivedColimit_comp_counit (U : C) (K : CochainComplex (Cᵒᵖ ⥤ D) ℤ) :
    (evaluationToTotalDerivedColimit C D U).app K ≫
      (totalDerivedColimit C D).map ((DerivedCategory.quotientCompQhIso _).inv.app K) ≫
      (totalDerivedColimitCounit C D).app
        ((HomotopyCategory.quotient _ (ComplexShape.up ℤ)).obj K) ≫
      DerivedCategory.Qh.map
        (((colim : (Cᵒᵖ ⥤ D) ⥤ D).mapHomotopyCategoryFactors
          (ComplexShape.up ℤ)).hom.app K) ≫
      (DerivedCategory.quotientCompQhIso _).hom.app
        (((colim : (Cᵒᵖ ⥤ D) ⥤ D).mapHomologicalComplex (ComplexShape.up ℤ)).obj K) =
    DerivedCategory.Q.map
      ((NatTrans.mapHomologicalComplex (sectionsToColimit C D U) (ComplexShape.up ℤ)).app K)

Stacks.CategoryHomology.evaluationToTotalDerivedColimit', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/EvaluationToDerivedColimit.lean, line 637. The attribute's comment: “the canonical map”.

The canonical map F^•(U) ⟶ Lπ_!(F^•). For a complex F^• of diagrams on Cᵒᵖ and an object U of C, the canonical map F^•(U) ⟶ Lπ_!(F^•) in the unbounded derived category, natural in F^•. For D = AddCommGrpCat this is a map in D(Ab), and for D = ModuleCat B it is the same map read in D(B).

def evaluationToTotalDerivedColimit' (U : C) :
    ((evaluation Cᵒᵖ D).obj (op U)).mapHomologicalComplex (ComplexShape.up ℤ) ⋙
        DerivedCategory.Q ⟶
      DerivedCategory.Q ⋙ totalDerivedColimit' C D

Stacks.CategoryHomology.evaluationToTotalDerivedColimit_comp_counit', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/EvaluationToDerivedColimit.lean, line 652. The attribute's comment: “the canonical map”.

The canonical map is the colimit cocone. After the canonical comparisons of the total left derived functor with the degreewise colimit, the map of evaluationToTotalDerivedColimit' is the colimit cocone of the complex.

theorem evaluationToTotalDerivedColimit_comp_counit' (U : C) (K : CochainComplex (Cᵒᵖ ⥤ D) ℤ) :
    (evaluationToTotalDerivedColimit' C D U).app K ≫
      (totalDerivedColimit' C D).map ((DerivedCategory.quotientCompQhIso _).inv.app K) ≫
      (totalDerivedColimitCounit' C D).app
        ((HomotopyCategory.quotient _ (ComplexShape.up ℤ)).obj K) ≫
      DerivedCategory.Qh.map
        (((colim : (Cᵒᵖ ⥤ D) ⥤ D).mapHomotopyCategoryFactors
          (ComplexShape.up ℤ)).hom.app K) ≫
      (DerivedCategory.quotientCompQhIso _).hom.app
        (((colim : (Cᵒᵖ ⥤ D) ⥤ D).mapHomologicalComplex (ComplexShape.up ℤ)).obj K) =
    DerivedCategory.Q.map
      ((NatTrans.mapHomologicalComplex (sectionsToColimit' C D U) (ComplexShape.up ℤ)).app K)

Stacks.CategoryHomology.evaluationToDerivedColimitOfAbelianDiagrams, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/EvaluationToDerivedColimit.lean, line 714. The attribute's comment: “ab_map”.

The canonical map for abelian presheaves. The canonical map F^•(U) ⟶ Lπ_!(F^•) in D(Ab), for a complex F^• of abelian presheaves — equivalently, of abelian sheaves for the chaotic topology — on a small category.

def evaluationToDerivedColimitOfAbelianDiagrams (C : Type u) [SmallCategory C] (U : C) :
    ((evaluation Cᵒᵖ AddCommGrpCat.{max u v}).obj (op U)).mapHomologicalComplex
        (ComplexShape.up ℤ) ⋙ DerivedCategory.Q ⟶
      DerivedCategory.Q ⋙ totalDerivedColimit C AddCommGrpCat.{max u v}

Stacks.CategoryHomology.evaluationToDerivedColimitOfModuleDiagrams, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/EvaluationToDerivedColimit.lean, line 723. The attribute's comment: “module_map”.

The canonical map for modules. The canonical map F^•(U) ⟶ Lπ_!(F^•), read in D(B), for a complex of modules over the constant sheaf of rings B̲ on a small chaotic site.

def evaluationToDerivedColimitOfModuleDiagrams (C : Type u) [SmallCategory C]
    (B : Type w) [Ring B] (U : C) :
    ((evaluation Cᵒᵖ (ModuleCat.{max u w} B)).obj (op U)).mapHomologicalComplex
        (ComplexShape.up ℤ) ⋙ DerivedCategory.Q ⟶
      DerivedCategory.Q ⋙ totalDerivedColimit C (ModuleCat.{max u w} B)
Tag 08Q7, a lemma

Tag 08Q7 in the Stacks Project.

Stacks.ChaoticSite.abelianDerivedLowerShriekInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/DerivedLowerShriekOfAdjointFunctor.lean, line 172. The attribute's comment: “for a functor of chaotic sites with a fully faithful right adjoint, of which the projection to the point of a category with a final object is the case in the source”.

Tag 08Q7 for a functor with a fully faithful right adjoint. Let u : C ⥤ D be a functor between categories carrying the chaotic topology and let g be the induced morphism of topoi, so that g⁻¹ is restriction along u. If u has a fully faithful right adjoint, then inverse image followed by derived lower shriek is the identity of D(Ab(D)): for any left derived functor L of lower shriek, presented by a comparison α, and any derived functor G of inverse image, presented by e, there is a natural isomorphism G ⋙ L ≅ 𝟭.

def abelianDerivedLowerShriekInverseImageIso (adj : uf ⊣ sf) [sf.Full] [sf.Faithful]
    (hJ : J = ⊥) (hK : K = ⊥)
    [HasSheafify J A] [HasSheafify K A]
    [uf.IsContinuous J K] [sf.IsContinuous K J]
    [(uf.sheafPushforwardContinuous A J K).IsRightAdjoint]
    (L : DerivedCategory (Sheaf J A) ⥤ DerivedCategory (Sheaf K A))
    (α : DerivedCategory.Qh ⋙ L ⟶
      (uf.sheafPullback A J K).mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh)
    [L.IsLeftDerivedFunctor α (HomotopyCategory.quasiIso (Sheaf J A) (ComplexShape.up ℤ))]
    (G : DerivedCategory (Sheaf K A) ⥤ DerivedCategory (Sheaf J A))
    (e : DerivedCategory.Qh ⋙ G ≅
      (uf.sheafPushforwardContinuous A J K).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
        DerivedCategory.Qh) :
    G ⋙ L ≅ 𝟭 _

Stacks.ChaoticSite.derivedConstCompColimitIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/DerivedLowerShriekOfInverseImage.lean, line 570. The attribute's comment: “derived colimit presentation”.

Stacks 08Q7, unconditionally. In the colimit presentation of lower shriek on a chaotic site — π_! = colim_{Cᵒᵖ} and π^{-1} = const — the identity Lπ_! ∘ π^{-1} = id holds with no hypothesis on the existence of the derived functor: the total left derived colimit of Stacks.CategoryHomology.totalDerivedColimit exists for any coefficient category with enough projectives and exact countable filtered colimits.

def derivedConstCompColimitIso (C : Type u) [SmallCategory C]
    (Dc : Type uA) [Category.{vA} Dc] [Abelian Dc]
    [EnoughProjectives (Cᵒᵖ ⥤ Dc)] [HasColimitsOfShape ℕ Dc]
    [HasExactColimitsOfShape ℕ Dc] [HasColimitsOfShape Cᵒᵖ Dc]
    (hC : HasInitial C ∨ HasTerminal C) :
    (Functor.const Cᵒᵖ : Dc ⥤ (Cᵒᵖ ⥤ Dc)).mapDerivedCategory ⋙
      Stacks.CategoryHomology.totalDerivedColimit C Dc ≅ 𝟭 _

Stacks.ChaoticSite.derivedConstCompColimitIso', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/DerivedLowerShriekOfInverseImage.lean, line 600. The attribute's comment: “derived colimit presentation”.

Stacks 08Q7, unconditionally, for a category that need not be small. In the colimit presentation of lower shriek on a chaotic site — π_! = colim_{Cᵒᵖ} and π^{-1} = const — the identity Lπ_! ∘ π^{-1} = id holds with no hypothesis on the existence of the derived functor: the total left derived colimit of Stacks.CategoryHomology.totalDerivedColimit' exists for any coefficient category with enough projectives and exact countable filtered colimits.

No smallness is asked of the site either: the objects of C and its morphisms may live in different universes, as they do at the site of [Stacks, Tag 08PR]. Everything the proof consumes is size-general — Stacks.CategoryHomology.totalDerivedColimit' and its two companions carry only instance hypotheses, and the abstract form derivedCompositeOfConstant is stated for an arbitrary category.

def derivedConstCompColimitIso' (C : Type u) [Category.{v} C]
    (Dc : Type uA) [Category.{vA} Dc] [Abelian Dc]
    [EnoughProjectives (Cᵒᵖ ⥤ Dc)] [HasColimitsOfShape ℕ Dc]
    [HasExactColimitsOfShape ℕ Dc] [HasColimitsOfShape Cᵒᵖ Dc]
    (hC : HasInitial C ∨ HasTerminal C) :
    (Functor.const Cᵒᵖ : Dc ⥤ (Cᵒᵖ ⥤ Dc)).mapDerivedCategory ⋙
      Stacks.CategoryHomology.totalDerivedColimit' C Dc ≅ 𝟭 _

Stacks.ChaoticSite.abelianDerivedInverseImageCompLowerShriekIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/DerivedLowerShriekOfInverseImage.lean, line 624. The attribute's comment: “abelian groups”.

Stacks 08Q7 for abelian sheaves. On the chaotic site of a category with an initial or a final object, inverse image from the point followed by derived lower shriek is the identity of D(Ab): for any left derived functor L of lower shriek, presented by a comparison α, and any derived functor G of inverse image, presented by e, there is a natural isomorphism G ⋙ L ≅ 𝟭.

def abelianDerivedInverseImageCompLowerShriekIso
    (C : Type u) [Category.{v} C]
    (hC : HasInitial C ∨ HasTerminal C)
    [HasSheafify (GrothendieckTopology.trivial C) AddCommGrpCat.{max w (u + 1) v}]
    [HasSheafify (GrothendieckTopology.trivial (Discrete PUnit.{u + 1}))
      AddCommGrpCat.{max w (u + 1) v}]
    [((Functor.star C).sheafPushforwardContinuous AddCommGrpCat.{max w (u + 1) v}
      (GrothendieckTopology.trivial C)
      (GrothendieckTopology.trivial (Discrete PUnit.{u + 1}))).IsRightAdjoint]
    [((Functor.star C).sheafPullback AddCommGrpCat.{max w (u + 1) v}
      (GrothendieckTopology.trivial C)
      (GrothendieckTopology.trivial (Discrete PUnit.{u + 1}))).Additive]
    [((Functor.star C).sheafPushforwardContinuous AddCommGrpCat.{max w (u + 1) v}
      (GrothendieckTopology.trivial C)
      (GrothendieckTopology.trivial (Discrete PUnit.{u + 1}))).Additive]
    (L : DerivedCategory
      (Sheaf (GrothendieckTopology.trivial C) AddCommGrpCat.{max w (u + 1) v}) ⥤
      DerivedCategory (Sheaf (GrothendieckTopology.trivial (Discrete PUnit.{u + 1}))
        AddCommGrpCat.{max w (u + 1) v}))
    (α : DerivedCategory.Qh ⋙ L ⟶
      ((Functor.star C).sheafPullback AddCommGrpCat.{max w (u + 1) v}
        (GrothendieckTopology.trivial C)
        (GrothendieckTopology.trivial (Discrete PUnit.{u + 1}))).mapHomotopyCategory
          (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh)
    [L.IsLeftDerivedFunctor α
      (HomotopyCategory.quasiIso
        (Sheaf (GrothendieckTopology.trivial C) AddCommGrpCat.{max w (u + 1) v})
        (ComplexShape.up ℤ))]
    (G : DerivedCategory (Sheaf (GrothendieckTopology.trivial (Discrete PUnit.{u + 1}))
        AddCommGrpCat.{max w (u + 1) v}) ⥤
      DerivedCategory (Sheaf (GrothendieckTopology.trivial C)
        AddCommGrpCat.{max w (u + 1) v}))
    (e : DerivedCategory.Qh ⋙ G ≅
      ((Functor.star C).sheafPushforwardContinuous AddCommGrpCat.{max w (u + 1) v}
        (GrothendieckTopology.trivial C)
        (GrothendieckTopology.trivial (Discrete PUnit.{u + 1}))).mapHomotopyCategory
          (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh) :
    G ⋙ L ≅ 𝟭 _

Stacks.ChaoticSite.moduleDerivedInverseImageCompLowerShriekIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/DerivedLowerShriekOfInverseImage.lean, line 675. The attribute's comment: “modules over a ring”.

Stacks 08Q7 for sheaves of modules. The same identity for sheaves of modules over the constant coefficient ring of a ringed-point situation whose category has an initial or a final object.

def moduleDerivedInverseImageCompLowerShriekIso
    (hC : HasInitial s.C ∨ HasTerminal s.C)
    [HasSheafify (GrothendieckTopology.trivial s.C) AddCommGrpCat.{max w u v}]
    [HasSheafify (GrothendieckTopology.trivial (Discrete PUnit.{u + 1}))
      AddCommGrpCat.{max w u v}]
    [(GrothendieckTopology.trivial s.C).WEqualsLocallyBijective AddCommGrpCat.{max w u v}]
    [(GrothendieckTopology.trivial (Discrete PUnit.{u + 1})).WEqualsLocallyBijective
      AddCommGrpCat.{max w u v}]
    [(SheafOfModules.pushforward (𝟙 (pointSituationConstantRing s))).IsRightAdjoint]
    [(SheafOfModules.pullback (𝟙 (pointSituationConstantRing s))).Additive]
    [(SheafOfModules.pushforward (𝟙 (pointSituationConstantRing s))).Additive]
    (L : DerivedCategory (SheafOfModules.{max w u v} (pointSituationConstantRing s)) ⥤
      DerivedCategory (SheafOfModules.{max w u v} (pointRing s)))
    (α : DerivedCategory.Qh ⋙ L ⟶
      (SheafOfModules.pullback (𝟙 (pointSituationConstantRing s))).mapHomotopyCategory
        (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh)
    [L.IsLeftDerivedFunctor α (HomotopyCategory.quasiIso _ (ComplexShape.up ℤ))]
    (G : DerivedCategory (SheafOfModules.{max w u v} (pointRing s)) ⥤
      DerivedCategory (SheafOfModules.{max w u v} (pointSituationConstantRing s)))
    (e : DerivedCategory.Qh ⋙ G ≅
      (SheafOfModules.pushforward (𝟙 (pointSituationConstantRing s))).mapHomotopyCategory
        (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh) :
    G ⋙ L ≅ 𝟭 _
Tag 08Q8, a lemma

Tag 08Q8 in the Stacks Project.

Stacks.ChaoticSite.derivedColimitExtendScalarsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/DerivedChangeOfCoefficients.lean, line 306.

Stacks 08Q8. For a ring map f : B ⟶ B' and the resulting commutative square of ringed topoi over a chaotic site, derived lower shriek to the point commutes with derived extension of coefficients: Lπ'_! ∘ Lh^* ≅ Lf^* ∘ Lπ_!.

Both sides are left adjoint to the degreewise derived functor of the constant diagram of the restriction of scalars, so they agree by uniqueness of left adjoints.

def derivedColimitExtendScalarsIso :
    derivedDiagramExtendScalars f C ⋙ totalDerivedColimit C (ModuleCat.{max u w} B') ≅
      totalDerivedColimit C (ModuleCat.{max u w} B) ⋙ derivedPointExtendScalars.{w, u} f
Tag 08Q9, a lemma

Tag 08Q9 in the Stacks Project.

Stacks.ChaoticSite.leftDerivedColimitIsoMooreComplexHomology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/CosimplicialResolution.lean, line 252. The attribute's comment: “for the abelian sheaves ℱ = j_{W!}ℤ_W, the free abelian presheaves on representables, which are the projective generators the source's proof reduces to; Lπ_! is read degreewise as the left derived functors L_nπ_! = H_n(C, -) of the colimit over Cᵒᵖ of Tag 08PF, and ℱ(U_•) as the Moore complex of the simplicial abelian group obtained by evaluating ℱ on U_•”.

Let U_• be a cosimplicial object of a small category C such that every simplicial set Mor_C(U_•, W) is homotopy equivalent to a singleton. The homology L_nπ_! of C with coefficients the free abelian presheaf j_{W!}ℤ_W on a representable is the homology of the Moore complex of j_{W!}ℤ_W(U_•).

def leftDerivedColimitIsoMooreComplexHomology (hU : IsPointResolution U) (W : C) (n : ℕ) :
    ((colim : (Cᵒᵖ ⥤ AddCommGrpCat.{u}) ⥤ AddCommGrpCat.{u}).leftDerived n).obj
        (freeRepresentablePresheaf W) ≅
      ((cosimplicialMooreComplex U).obj (freeRepresentablePresheaf W)).homology n

Stacks.ChaoticSite.leftDerivedColimitNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/CosimplicialResolution.lean, line 692.

Let U_• be a cosimplicial object of a small category C such that every simplicial set Mor_C(U_•, W) is homotopy equivalent to a singleton. For every abelian presheaf ℱ the homology L_nπ_! of C with coefficients ℱ is the homology of the Moore complex of ℱ(U_•), naturally in ℱ.

def leftDerivedColimitNatIso (hU : IsPointResolution U) (n : ℕ) :
    (colim : (Cᵒᵖ ⥤ AddCommGrpCat.{u}) ⥤ AddCommGrpCat.{u}).leftDerived n ≅
      cosimplicialMooreComplex U ⋙
        HomologicalComplex.homologyFunctor AddCommGrpCat.{u} (ComplexShape.down ℕ) n

Stacks.ChaoticSite.ModuleValued.moduleLeftDerivedColimitNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/CosimplicialResolutionOfModules.lean, line 598. The attribute's comment: “module half: Lπ_!(ℱ) = ℱ(U_•) in D(B) functorially in ℱ in Mod(B̲), read degreewise as L_nπ_! = L_n colim of Tag 08PF and as the Moore complex of the simplicial B-module obtained by evaluating ℱ on U_•”.

Let U_• be a cosimplicial object of a small category C such that every simplicial set Mor_C(U_•, W) is homotopy equivalent to a singleton, and let B be a ring. For every B̲-module ℱ on the chaotic site C — that is, every diagram of B-modules on Cᵒᵖ — the homology L_nπ_! of C with coefficients ℱ is the homology of the Moore complex of ℱ(U_•), naturally in ℱ, as B-modules.

def moduleLeftDerivedColimitNatIso (hU : IsPointResolution U) (n : ℕ) :
    (colim : (Cᵒᵖ ⥤ ModuleCat.{u} B) ⥤ ModuleCat.{u} B).leftDerived n ≅
      moduleCosimplicialMooreComplex U ⋙
        HomologicalComplex.homologyFunctor (ModuleCat.{u} B) (ComplexShape.down ℕ) n

Stacks.ChaoticSite.AbelianValued.mooreCochainNatIsoDerivedColimit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/DerivedColimitByPointResolutionAbelian.lean, line 459. The attribute's comment: “derived-category form at abelian coefficients, natural in the coefficient presheaf: the extended Moore complex of the evaluation on a point resolution is derived lower shriek as an isomorphism of functors. The degreewise form Stacks.ChaoticSite.leftDerivedColimitNatIso gives only the cohomology of the two sides and cannot transport a morphism of coefficients”.

The derived form of [Stacks, Tag 08Q9] at abelian coefficients, as an isomorphism of functors. Let C be a small category with the chaotic topology and let U_• be a cosimplicial object of C which is a point resolution. Then

Q(ℱ(U_•)) ≅ Lπ_!(ℱ) in D(Ab),

naturally in the abelian presheaf ℱ, where the left side is the extended Moore complex of the simplicial abelian group ℱ(U_•) and Lπ_! is the total left derived functor of the colimit over Cᵒᵖ, which is π_! on the chaotic site by [Stacks, Tag 08PF].

def mooreCochainNatIsoDerivedColimit (hU : IsPointResolution U) :
    mooreCochainComplex U ⋙ DerivedCategory.Q ≅
      HomologicalComplex.single (Cᵒᵖ ⥤ AddCommGrpCat.{u}) (ComplexShape.up ℤ) 0 ⋙
        DerivedCategory.Q ⋙ totalDerivedColimit C AddCommGrpCat.{u}

Stacks.ChaoticSite.AbelianValued.mooreCochainNatIsoDerivedColimitOfLarge, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/DerivedColimitByPointResolutionLargeSite.lean, line 158. The attribute's comment: “derived-category form at abelian coefficients, natural in the coefficient presheaf, with the smallness hypothesis on the site removed: the site's objects and its morphisms may live in different universes, the coefficients being read at their maximum. The lemma Stacks.ChaoticSite.AbelianValued.mooreCochainNatIsoDerivedColimit is this statement for a small site”.

The derived form of [Stacks, Tag 08Q9] at abelian coefficients, for a site that need not be small. Let U_• be a cosimplicial object of C which is a point resolution. Then

Q(ℱ(U_•)) ≅ Lπ_!(ℱ) in D(Ab),

naturally in the abelian presheaf ℱ, where the left side is the extended Moore complex of the simplicial abelian group ℱ(U_•) and Lπ_! is the total left derived functor of the colimit over Cᵒᵖ, which is π_! on the chaotic site by [Stacks, Tag 08PF].

The objects of C and its morphisms may live in different universes; the coefficients are read at max v u, the smallest universe in which Cᵒᵖ has colimits of abelian groups. The form Stacks.ChaoticSite.AbelianValued.mooreCochainNatIsoDerivedColimit asks for a small site, and so does not apply to the site of [Stacks, Tag 08PR].

def mooreCochainNatIsoDerivedColimitOfLarge (hU : IsPointResolution U) :
    GeneralValued.mooreCochainComplex' U AddCommGrpCat.{max v u} ⋙ DerivedCategory.Q ≅
      HomologicalComplex.single (Cᵒᵖ ⥤ AddCommGrpCat.{max v u}) (ComplexShape.up ℤ) 0 ⋙
        DerivedCategory.Q ⋙ totalDerivedColimit' C AddCommGrpCat.{max v u}

Stacks.ChaoticSite.ModuleValued.mooreCochainNatIsoDerivedColimitOfLarge, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/DerivedColimitByPointResolutionLargeSite.lean, line 218. The attribute's comment: “derived-category form at module coefficients, natural in the coefficient module, with the smallness hypothesis on the site removed. The lemma Stacks.ChaoticSite.ModuleValued.mooreCochainNatIsoDerivedColimit is this statement for a small site”.

The derived form of [Stacks, Tag 08Q9] at linear coefficients, for a site that need not be small. Let U_• be a cosimplicial object of C which is a point resolution and let B be a ring. Then

Q(ℱ(U_•)) ≅ Lπ_!(ℱ) in D(B),

naturally in the diagram of B-modules ℱ -- equivalently, in the B̲-module ℱ, the topology being chaotic. This is the module half beside Stacks.ChaoticSite.AbelianValued.mooreCochainNatIsoDerivedColimitOfLarge, and as there the objects of C and its morphisms may live in different universes.

def mooreCochainNatIsoDerivedColimitOfLarge (hU : IsPointResolution U) :
    GeneralValued.mooreCochainComplex' U (ModuleCat.{max v u} B) ⋙ DerivedCategory.Q ≅
      HomologicalComplex.single (Cᵒᵖ ⥤ ModuleCat.{max v u} B) (ComplexShape.up ℤ) 0 ⋙
        DerivedCategory.Q ⋙ totalDerivedColimit' C (ModuleCat.{max v u} B)

Stacks.ChaoticSite.ModuleValued.mooreCochainNatIsoDerivedColimit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/DerivedColimitOfComplexesByPointResolution.lean, line 374. The attribute's comment: “derived-category form at module coefficients, natural in the coefficient module: the extended Moore complex of the evaluation on a point resolution is derived lower shriek as an isomorphism of functors. Neither the degreewise form Stacks.ChaoticSite.leftDerivedColimitNatIso nor the object-level Stacks.ChaoticSite.ModuleValued.mooreCochainQIsoDerivedColimit provides this”.

The derived form of [Stacks, Tag 08Q9] at module coefficients, as an isomorphism of functors. Let C be a small category with the chaotic topology, B a ring, and U_• a cosimplicial object of C which is a point resolution. Then

Q(ℱ(U_•)) ≅ Lπ_!(ℱ) in D(B),

naturally in the diagram ℱ of B-modules, where the left side is the extended Moore complex of the simplicial B-module ℱ(U_•) and Lπ_! is the total left derived functor of the colimit over Cᵒᵖ, which is π_! on the chaotic site by [Stacks, Tag 08PF].

def mooreCochainNatIsoDerivedColimit (hU : IsPointResolution U) :
    mooreCochainComplex (B := B) U ⋙ DerivedCategory.Q ≅
      HomologicalComplex.single (Cᵒᵖ ⥤ ModuleCat.{u} B) (ComplexShape.up ℤ) 0 ⋙
        DerivedCategory.Q ⋙ totalDerivedColimit C (ModuleCat.{u} B)

Stacks.ChaoticSite.simplexCategoryLeftDerivedColimitNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/SimplexCategoryMooreComplex.lean, line 99. The attribute's comment: “at C = Δ with U_• = 𝟭: L_n of the colimit over Δᵒᵖ is the homology of the alternating-face-map complex of the simplicial abelian group itself, there being no cosimplicial object left in the statement. Abelian coefficients in the universe of Δ, which is 0”.

Stacks 08Q9 at C = Δ. For a simplicial abelian group ℱ, the homology L_nπ_! of Δ with coefficients ℱ is the nth homology of the alternating-face-map complex of ℱ, naturally in ℱ.

def simplexCategoryLeftDerivedColimitNatIso (n : ℕ) :
    (colim : (SimplexCategoryᵒᵖ ⥤ AddCommGrpCat.{0}) ⥤ AddCommGrpCat.{0}).leftDerived n ≅
      alternatingFaceMapComplex AddCommGrpCat.{0} ⋙
        HomologicalComplex.homologyFunctor AddCommGrpCat.{0} (ComplexShape.down ℕ) n

Stacks.ChaoticSite.categoryHomology_simplexCategory, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/SimplexCategoryMooreComplex.lean, line 109. The attribute's comment: “at C = Δ, written with Stacks.CategoryHomology.categoryHomology”.

Stacks 08Q9 at C = Δ, in the categoryHomology spelling. The homology of Δ with coefficients in a simplicial abelian group is the Moore homology of that simplicial abelian group. This is the form the fibrewise machinery of Stacks 08PI and 08PJ consumes.

def categoryHomology_simplexCategory (F : SimplexCategoryᵒᵖ ⥤ AddCommGrpCat.{0}) (n : ℕ) :
    categoryHomology F n ≅
      ((alternatingFaceMapComplex AddCommGrpCat.{0}).obj F).homology n

Stacks.ChaoticSite.AbelianValued.simplexCategoryMooreCochainNatIsoDerivedColimit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/SimplexCategoryMooreComplex.lean, line 127. The attribute's comment: “at C = Δ, derived-category form, natural in the coefficient presheaf”.

Stacks 08Q9 at C = Δ, in the derived category. The extended alternating-face-map complex of a simplicial abelian group is derived lower shriek of that simplicial abelian group placed in degree zero, as an isomorphism of functors into D(Ab).

def simplexCategoryMooreCochainNatIsoDerivedColimit :
    (alternatingFaceMapComplex AddCommGrpCat.{0} ⋙
        (ComplexShape.embeddingUpIntLE (0 : ℤ)).extendFunctor AddCommGrpCat.{0}) ⋙
        DerivedCategory.Q ≅
      HomologicalComplex.single (SimplexCategoryᵒᵖ ⥤ AddCommGrpCat.{0}) (ComplexShape.up ℤ) 0 ⋙
        DerivedCategory.Q ⋙ totalDerivedColimit SimplexCategory AddCommGrpCat.{0}

Stacks.ChaoticSite.ModuleValued.simplexCategoryModuleLeftDerivedColimitNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/SimplexCategoryMooreComplex.lean, line 153. The attribute's comment: “at C = Δ with U_• = 𝟭, module coefficients: L_n of the colimit over Δᵒᵖ is the homology of the alternating-face-map complex of the simplicial B-module itself. The ring and the module sections lie in the universe of Δ, which is 0”.

Stacks 08Q9 at C = Δ, module coefficients. For a simplicial B-module ℱ, the homology L_nπ_! of Δ with coefficients ℱ is the nth homology of the alternating-face-map complex of ℱ, naturally in ℱ, as B-modules.

def simplexCategoryModuleLeftDerivedColimitNatIso (n : ℕ) :
    (colim : (SimplexCategoryᵒᵖ ⥤ ModuleCat.{0} B) ⥤ ModuleCat.{0} B).leftDerived n ≅
      alternatingFaceMapComplex (ModuleCat.{0} B) ⋙
        HomologicalComplex.homologyFunctor (ModuleCat.{0} B) (ComplexShape.down ℕ) n
Tag 08QA, a lemma

Tag 08QA in the Stacks Project.

Stacks.ChaoticSite.leftDerivedColimitPresheafRestrictionNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/CosimplicialResolutionFunctoriality.lean, line 85. The attribute's comment: “the identification L_nπ'_! ∘ g^{-1} = L_nπ_! degreewise, for the left derived functors of colim at abelian coefficients. The derived-category forms at a single module of coefficients are Stacks.ChaoticSite.AbelianValued.derivedColimitPresheafRestrictionNatIso and Stacks.ChaoticSite.ModuleValued.derivedColimitInverseImageNatIso, and at an arbitrary bounded above COMPLEX of coefficients — the form the source states — Stacks.ChaoticSite.AbelianValued.derivedColimitPresheafRestrictionComplexNatIso and Stacks.ChaoticSite.ModuleValued.derivedColimitInverseImageComplexNatIso”.

Stacks 08QA. Let f : C' ⥤ C be a functor between small categories and let U_• be a cosimplicial object of C' such that both U_• and f(U_•) are point resolutions. Then the homology of C' with coefficients the restriction of an abelian presheaf ℱ on C along f is the homology of C with coefficients ℱ, in every degree and naturally in ℱ: that is, L_nπ'_! ∘ g^{-1} = L_nπ_!.

def leftDerivedColimitPresheafRestrictionNatIso (f : C' ⥤ C) (U : CosimplicialObject C')
    (hU : IsPointResolution U) (hfU : IsPointResolution (U ⋙ f)) (n : ℕ) :
    Stacks.CategoryHomology.presheafRestriction.{u, u, u} f ⋙
        (colim : (C'ᵒᵖ ⥤ AddCommGrpCat.{u}) ⥤ AddCommGrpCat.{u}).leftDerived n ≅
      (colim : (Cᵒᵖ ⥤ AddCommGrpCat.{u}) ⥤ AddCommGrpCat.{u}).leftDerived n

Stacks.ChaoticSite.AbelianValued.derivedColimitPresheafRestrictionNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/DerivedColimitByPointResolutionFunctorialityAbelian.lean, line 81. The attribute's comment: “the identification Lπ'_! ∘ g^{-1} = Lπ_! with values in D(Ab), at abelian coefficients, as an isomorphism of functors whose domain is the category of abelian presheaves on C — the heart. The same identification for an arbitrary bounded above COMPLEX of abelian presheaves, which is what the source's D(C) ⥤ D(Ab) says, is Stacks.ChaoticSite.AbelianValued.derivedColimitPresheafRestrictionComplexNatIso; the unbounded case is open and the implementation note says what it needs”.

Let f : C' ⥤ C be a functor between small categories with their chaotic topologies, let g^{-1} be restriction of abelian presheaves along f, and let U_• be a cosimplicial object of C' such that both U_• and f(U_•) are point resolutions. Then the derived lower shriek on C' of the restriction of an abelian presheaf ℱ on C is the derived lower shriek of ℱ on C, as an isomorphism of functors into D(Ab) and naturally in ℱ: that is, Lπ'_! ∘ g^{-1} = Lπ_!.

def derivedColimitPresheafRestrictionNatIso (f : C' ⥤ C) (U : CosimplicialObject C')
    (hU : IsPointResolution U) (hfU : IsPointResolution (U ⋙ f)) :
    Stacks.CategoryHomology.presheafRestriction.{u, u, u} f ⋙
        HomologicalComplex.single (C'ᵒᵖ ⥤ AddCommGrpCat.{u}) (ComplexShape.up ℤ) 0 ⋙
          DerivedCategory.Q ⋙ totalDerivedColimit C' AddCommGrpCat.{u} ≅
      HomologicalComplex.single (Cᵒᵖ ⥤ AddCommGrpCat.{u}) (ComplexShape.up ℤ) 0 ⋙
        DerivedCategory.Q ⋙ totalDerivedColimit C AddCommGrpCat.{u}

Stacks.ChaoticSite.ModuleValued.derivedColimitInverseImageNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/DerivedColimitByPointResolutionFunctorialityModule.lean, line 78. The attribute's comment: “the identification Lπ'_! ∘ g^{-1} = Lπ_! with values in D(B), at module coefficients, as an isomorphism of functors whose domain is the category of B̲-modules on C — the heart. The same identification for an arbitrary bounded above COMPLEX of B̲-modules, which is what the source's D(C, B̲) ⥤ D(B) says, is Stacks.ChaoticSite.ModuleValued.derivedColimitInverseImageComplexNatIso; the unbounded case is open and the implementation note says what it needs”.

Let f : C' ⥤ C be a functor between small categories with their chaotic topologies, let B be a ring, let g^{-1} be the inverse image of the induced morphism of ringed topoi — restriction of diagrams of B-modules along f — and let U_• be a cosimplicial object of C' such that both U_• and f(U_•) are point resolutions. Then the derived lower shriek on C' of the inverse image of a B̲-module ℱ on C is the derived lower shriek of ℱ on C, as an isomorphism of functors into D(B) and naturally in ℱ: that is, Lπ'_! ∘ g^{-1} = Lπ_!.

def derivedColimitInverseImageNatIso (f : C' ⥤ C) (U : CosimplicialObject C')
    (hU : IsPointResolution U) (hfU : IsPointResolution (U ⋙ f)) :
    inverseImageAlongAFunctor C C' f B ⋙
        HomologicalComplex.single (C'ᵒᵖ ⥤ ModuleCat.{u} B) (ComplexShape.up ℤ) 0 ⋙
          DerivedCategory.Q ⋙ totalDerivedColimit C' (ModuleCat.{u} B) ≅
      HomologicalComplex.single (Cᵒᵖ ⥤ ModuleCat.{u} B) (ComplexShape.up ℤ) 0 ⋙
        DerivedCategory.Q ⋙ totalDerivedColimit C (ModuleCat.{u} B)

Stacks.ChaoticSite.ModuleValued.derivedColimitInverseImageComplexNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/DerivedColimitOfComplexesFunctoriality.lean, line 291. The attribute's comment: “the identification Lπ'_! ∘ g^{-1} = Lπ_! with values in D(B), at module coefficients, as an isomorphism of functors of a COMPLEX of coefficients strictly bounded above by 0, whose domain contains the complexes concentrated in degree 0, so that the statement specialises to the form at the heart (the two isomorphisms are not compared). The source states the identification on the unbounded D(C, B̲); the module docstring records what the unbounded case needs, namely the dévissage along the compact generators, the total complex of the double complex of an unbounded complex not being Lπ_! of it”.

Stacks 08QA in D(B) for bounded above complexes, as an isomorphism of functors. Let f : C' ⥤ C be a functor between small categories with their chaotic topologies, let B be a ring, let g^{-1} be the inverse image of the induced morphism of ringed topoi — restriction of diagrams of B-modules along f — and let U_• be a cosimplicial object of C' such that both U_• and f(U_•) are point resolutions. Then

Lπ'_! ∘ g^{-1} = Lπ_!

as functors from the complexes of B̲-modules on C strictly bounded above by 0 to D(B).

def derivedColimitInverseImageComplexNatIso (f : C' ⥤ C) (U : CosimplicialObject C')
    (hU : IsPointResolution U) (hfU : IsPointResolution (U ⋙ f)) :
    (strictlyLEZero (Cᵒᵖ ⥤ ModuleCat.{u} B)).ι ⋙
        (inverseImageAlongAFunctor C C' f B).mapHomologicalComplex (ComplexShape.up ℤ) ⋙
          DerivedCategory.Q ⋙ totalDerivedColimit C' (ModuleCat.{u} B) ≅
      (strictlyLEZero (Cᵒᵖ ⥤ ModuleCat.{u} B)).ι ⋙
        DerivedCategory.Q ⋙ totalDerivedColimit C (ModuleCat.{u} B)

Stacks.ChaoticSite.AbelianValued.derivedColimitPresheafRestrictionComplexNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/DerivedColimitOfComplexesFunctoriality.lean, line 461. The attribute's comment: “the identification Lπ'_! ∘ g^{-1} = Lπ_! with values in D(Ab), at abelian coefficients, as an isomorphism of functors of a COMPLEX of coefficients strictly bounded above by 0, whose domain contains the complexes concentrated in degree 0, so that the statement specialises to the form at the heart (the two isomorphisms are not compared). The source states the identification on the unbounded D(C); the module docstring records what the unbounded case needs, namely the dévissage along the compact generators, the total complex of the double complex of an unbounded complex not being Lπ_! of it”.

Stacks 08QA in D(Ab) for bounded above complexes, as an isomorphism of functors. Let f : C' ⥤ C be a functor between small categories with their chaotic topologies, let g^{-1} be restriction of abelian presheaves along f, and let U_• be a cosimplicial object of C' such that both U_• and f(U_•) are point resolutions. Then

Lπ'_! ∘ g^{-1} = Lπ_!

as functors from the complexes of abelian presheaves on C strictly bounded above by 0 to D(Ab).

def derivedColimitPresheafRestrictionComplexNatIso (f : C' ⥤ C) (U : CosimplicialObject C')
    (hU : IsPointResolution U) (hfU : IsPointResolution (U ⋙ f)) :
    (strictlyLEZero (Cᵒᵖ ⥤ AddCommGrpCat.{u})).ι ⋙
        (Stacks.CategoryHomology.presheafRestriction.{u, u, u} f).mapHomologicalComplex
          (ComplexShape.up ℤ) ⋙
          DerivedCategory.Q ⋙ totalDerivedColimit C' AddCommGrpCat.{u} ≅
      (strictlyLEZero (Cᵒᵖ ⥤ AddCommGrpCat.{u})).ι ⋙
        DerivedCategory.Q ⋙ totalDerivedColimit C AddCommGrpCat.{u}

Stacks.ChaoticSite.ModuleValued.isIso_derivedColimitInverseImageUnboundedComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/DerivedColimitUnboundedIsIso.lean, line 204. The attribute's comment: “the identification Lπ'_! ∘ g^{-1} = Lπ_! with values in D(B), at module coefficients, as an isomorphism of functors on the UNBOUNDED derived category D(C, B̲), which is what the source's resp. D(C, B̲) ⥤ D(B) says. The other half of the source's resp., the unbounded statement with values in D(Ab), is Stacks.ChaoticSite.AbelianValued.isIso_derivedColimitPresheafRestrictionUnboundedComparison in DerivedColimitUnboundedIsIsoAbelian.lean: the same mechanism at AddCommGrpCat, whose separating family of projective compact objects is ULift ℤ.”.

For a functor f : C' ⥤ C between small categories with their chaotic topologies and a cosimplicial object U_• of C' such that both U_• and f(U_•) are point resolutions, the comparison Lπ'_! ∘ g^{-1} ⟶ Lπ_! of Stacks.ChaoticSite.ModuleValued.derivedColimitInverseImageUnboundedComparison is an isomorphism of functors D(C, B̲) ⥤ D(B) on the unbounded derived category.

theorem ModuleValued.isIso_derivedColimitInverseImageUnboundedComparison
    {U : CosimplicialObject C'} (hU : IsPointResolution U) (hfU : IsPointResolution (U ⋙ f)) :
    IsIso (ModuleValued.derivedColimitInverseImageUnboundedComparison (B := B) f)

Stacks.ChaoticSite.ModuleValued.derivedColimitInverseImageUnboundedNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/DerivedColimitUnboundedIsIso.lean, line 216. The attribute's comment: “the identification Lπ'_! ∘ g^{-1} = Lπ_! with values in D(B) as an ISOMORPHISM OF FUNCTORS on the unbounded derived category D(C, B̲), packaged from the invertibility of the comparison”.

The isomorphism of functors Lπ'_! ∘ g^{-1} ≅ Lπ_! from D(C, B̲) to D(B) on the unbounded derived category, when U_• and f(U_•) are point resolutions.

def ModuleValued.derivedColimitInverseImageUnboundedNatIso
    {U : CosimplicialObject C'} (hU : IsPointResolution U) (hfU : IsPointResolution (U ⋙ f)) :
    (inverseImageAlongAFunctor C C' f B).mapDerivedCategory ⋙
        totalDerivedColimit C' (ModuleCat.{u} B) ≅
      totalDerivedColimit C (ModuleCat.{u} B)

Stacks.ChaoticSite.AbelianValued.isIso_derivedColimitPresheafRestrictionUnboundedComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/DerivedColimitUnboundedIsIsoAbelian.lean, line 102. The attribute's comment: “the identification Lπ'_! ∘ g^{-1} = Lπ_! with values in D(Ab), at abelian coefficients, as an isomorphism of functors on the UNBOUNDED derived category D(C), which is what the source's as functors D(C) ⥤ D(Ab) says”.

For a functor f : C' ⥤ C between small categories with their chaotic topologies and a cosimplicial object U_• of C' such that both U_• and f(U_•) are point resolutions, the comparison Lπ'_! ∘ g^{-1} ⟶ Lπ_! of Stacks.ChaoticSite.AbelianValued.derivedColimitPresheafRestrictionUnboundedComparison is an isomorphism of functors D(C) ⥤ D(Ab) on the unbounded derived category D(C).

theorem AbelianValued.isIso_derivedColimitPresheafRestrictionUnboundedComparison
    {U : CosimplicialObject C'} (hU : IsPointResolution U) (hfU : IsPointResolution (U ⋙ f)) :
    IsIso (AbelianValued.derivedColimitPresheafRestrictionUnboundedComparison f)

Stacks.ChaoticSite.AbelianValued.derivedColimitPresheafRestrictionUnboundedNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/DerivedColimitUnboundedIsIsoAbelian.lean, line 116. The attribute's comment: “the identification Lπ'_! ∘ g^{-1} = Lπ_! with values in D(Ab) as an ISOMORPHISM OF FUNCTORS on the unbounded derived category D(C), packaged from the invertibility of the comparison”.

For a functor f : C' ⥤ C between small categories with their chaotic topologies and a cosimplicial object U_• of C' such that both U_• and f(U_•) are point resolutions, the isomorphism of functors Lπ'_! ∘ g^{-1} ≅ Lπ_! from D(C) to D(Ab) on the unbounded derived category.

def AbelianValued.derivedColimitPresheafRestrictionUnboundedNatIso
    {U : CosimplicialObject C'} (hU : IsPointResolution U) (hfU : IsPointResolution (U ⋙ f)) :
    (Stacks.CategoryHomology.presheafRestriction.{u, u, u} f).mapDerivedCategory ⋙
        totalDerivedColimit C' AddCommGrpCat.{u} ≅
      totalDerivedColimit C AddCommGrpCat.{u}

Stacks.ChaoticSite.leftDerivedPointLowerShriekPresheafRestrictionNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/DerivedLowerShriekOfAResolutionFunctoriality.lean, line 70. The attribute's comment: “the identification L_nπ'_! ∘ g^{-1} = L_nπ_! for the sheaf-theoretic lower shriek along the point morphism, read through the sections at the point”.

Tag 08QA for Lπ_!. Let f : C' ⥤ C be a functor between small categories with their chaotic topologies and let U_• be a cosimplicial object of C' such that both U_• and f(U_•) are point resolutions. Then the sections at the point of L_nπ'_! applied to the inverse image of an abelian sheaf ℱ on C are the sections at the point of L_nπ_!(ℱ), in every degree and naturally in ℱ: that is, L_nπ'_! ∘ g^{-1} = L_nπ_!.

def leftDerivedPointLowerShriekPresheafRestrictionNatIso (f : C' ⥤ C) (U : CosimplicialObject C')
    (hU : IsPointResolution U) (hfU : IsPointResolution (U ⋙ f)) (n : ℕ) :
    f.sheafPushforwardContinuous AddCommGrpCat.{u} (GrothendieckTopology.trivial C')
          (GrothendieckTopology.trivial C) ⋙
        (abelianPointLowerShriek C').leftDerived n ⋙
          pointSections.{u, u + 1, u} AddCommGrpCat.{u} ≅
      (abelianPointLowerShriek C).leftDerived n ⋙
        pointSections.{u, u + 1, u} AddCommGrpCat.{u}
Tag 08QB, a lemma

Tag 08QB in the Stacks Project.

Stacks.CategoryHomology.isIso_derivedExternalTensorComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/DerivedExternalTensorProductFormula.lean, line 737.

Stacks 08QB. Let C₁ and C₂ be categories, g_i the morphisms of ringed topoi induced by the two projections of C₁ × C₂, and R a ring. For K_i ∈ D(C_i, R) the canonical comparison

L(π₁ × π₂)_!(g₁^{-1}K₁ ⊗^L_{R̲} g₂^{-1}K₂) ⟶ Lπ_{1,!}K₁ ⊗^L_R Lπ_{2,!}K₂

is an isomorphism in D(R).

theorem isIso_derivedExternalTensorComparison
    (K₁ : DerivedCategory (C₁ᵒᵖ ⥤ ModuleCat.{u} R))
    (K₂ : DerivedCategory (C₂ᵒᵖ ⥤ ModuleCat.{u} R)) :
    IsIso (derivedExternalTensorComparison C₁ C₂ R exists_kFlat_quasiIso_diagrams K₁ K₂)

Stacks.CategoryHomology.colimExternalTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/ExternalTensorProduct.lean, line 147. The attribute's comment: “the identity with both derived functors replaced by the underived ones, π_!(g₁⁻¹F ⊗_B̲ g₂⁻¹G) ≅ π_{1,!}F ⊗_B π_{2,!}G for diagrams of B-modules, with π_! the colimit over the site of Tag 08PF; the derived identity is not covered”.

Stacks 08QB, the identity with the derived functors replaced by the underived ones. The colimit over the product of two opposite categories of an external tensor product of diagrams is the tensor product of the two colimits.

def colimExternalTensorIso (F : C₁ᵒᵖ ⥤ ModuleCat.{max u₁ u₂ w} B)
    (G : C₂ᵒᵖ ⥤ ModuleCat.{max u₁ u₂ w} B) :
    (colim : ((C₁ × C₂)ᵒᵖ ⥤ ModuleCat.{max u₁ u₂ w} B) ⥤ _).obj (externalTensor F G) ≅
      (colim : (C₁ᵒᵖ ⥤ ModuleCat.{max u₁ u₂ w} B) ⥤ _).obj F ⊗
        (colim : (C₂ᵒᵖ ⥤ ModuleCat.{max u₁ u₂ w} B) ⥤ _).obj G

Stacks.CategoryHomology.externalTensorFreeYonedaIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/ExternalTensorProduct.lean, line 274. The attribute's comment: “the computation g₁⁻¹j_{U!}B̲_U ⊗_B̲ g₂⁻¹j_{V!}B̲_V = j_{(U,V)!}B̲_{(U,V)} made in the proof, for arbitrary coefficient modules in place of B̲; the derived identity that it is used to prove is not covered”.

Stacks 08QB, the computation of its proof on the generators. For U an object of C₁ and V an object of C₂, the external tensor product of the free diagram on U with coefficients P and the free diagram on V with coefficients Q is the free diagram on (U, V) with coefficients P ⊗_B Q.

def externalTensorFreeYonedaIso (U : C₁) (V : C₂)
    (P Q : ModuleCat.{max u₁ u₂ w} B) :
    externalTensor (C₂ := C₂) (Presheaf.freeYoneda U P) (Presheaf.freeYoneda V Q) ≅
      Presheaf.freeYoneda ((U, V) : C₁ × C₂) (P ⊗ Q)
Tag 08QC, a lemma

Tag 08QC in the Stacks Project.

Stacks.ChaoticSite.totalDerivedColimitTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/DerivedLowerShriekTensor.lean, line 282.

[Stacks, Tag 08QC]. Let C be a small category with the chaotic topology and R a commutative ring, as in Example 08PF, and suppose C carries a cosimplicial object U_• to which Tag 08Q9 applies: for every object W the simplicial set Mor_C(U_•, W) is homotopy equivalent to a point. Then derived lower shriek to the point preserves derived tensor products:

Lπ_!(K₁ ⊗^L_{R̲} K₂) ≅ Lπ_!(K₁) ⊗^L_R Lπ_!(K₂)

for all K₁, K₂ ∈ D(R̲), naturally in both, as an isomorphism of bifunctors D(Cᵒᵖ ⥤ R-Mod) × D(Cᵒᵖ ⥤ R-Mod) ⥤ D(R).

It is Stacks.ChaoticSite.totalDerivedColimitTensorIsoOfExternal (Tags 07A4, 08Q4 and 08QA along the diagonal) applied to [Stacks, Tag 08QB] on C × C, Stacks.CategoryHomology.isIso_derivedExternalTensorComparisonNatTrans.

def totalDerivedColimitTensorIso (U : CosimplicialObject C) (hU : IsPointResolution U) :
    letI := derivedMonoidal (ModuleCat.{u} R)
      (CochainComplex.DerivedTensor.OneSided.exists_kFlat_quasiIso R)
    letI := derivedMonoidal (Cᵒᵖ ⥤ ModuleCat.{u} R) (exists_kFlat_quasiIso_diagrams (J := Cᵒᵖ))
    MonoidalCategory.tensor (DerivedCategory (Cᵒᵖ ⥤ ModuleCat.{u} R)) ⋙
        totalDerivedColimit C (ModuleCat.{u} R) ≅
      (totalDerivedColimit C (ModuleCat.{u} R)).prod (totalDerivedColimit C (ModuleCat.{u} R)) ⋙
        MonoidalCategory.tensor (DerivedCategory (ModuleCat.{u} R))

Stacks.ChaoticSite.isIso_totalDerivedColimitTensorComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/EilenbergZilber.lean, line 421. The attribute's comment: “RESTRICTED: assumes Tags 07A4, 08PH, 08QA (diagonal and both projections) and 08QB at the derived level”.

The canonical comparison Lπ_!(K₁ ⊗^L K₂) ⟶ Lπ_!(K₁) ⊗^L Lπ_!(K₂) of derived lower shriek on the chaotic site C, Stacks.CategoryHomology.totalDerivedColimitTensorComparison, is an isomorphism when C carries a cosimplicial object U which is a point resolution, given the following hypotheses:

  • _h07A4: (diagPresheafRestriction C E).mapDerivedCategory is strong monoidal;
  • _h08PH: the transformation α from the derived Δ^{-1} ∘ π^{-1}_{C × C} to the derived π^{-1}_C is monoidal;
  • _h08QA: the mate Lπ_!(Δ^{-1}M) ⟶ L(π × π)_!(M) of α is invertible whenever some cosimplicial object V of C and its diagonal image are point resolutions;
  • _h08QA₁, _h08QA₂: the mates L(π × π)_!(g_i^{-1}M) ⟶ Lπ_!(M) of the transformations α₁, α₂ are invertible whenever some cosimplicial object V of C × C and its i-th projection are point resolutions;
  • _h08QB: the external mate L(π × π)_!(g₁^{-1}K₁ ⊗^L g₂^{-1}K₂) ⟶ Lπ_!K₁ ⊗^L Lπ_!K₂ of α₁ and α₂ is invertible.

The hypotheses hresE, hresCE, hresCCE provide the K-flat resolutions defining the three derived tensor products.

theorem isIso_totalDerivedColimitTensorComparison
    (U : CosimplicialObject C) (hU : IsPointResolution U)
    (K₁ K₂ : DerivedCategory (Cᵒᵖ ⥤ E)) :
    letI := derivedMonoidal E hresE
    letI := derivedMonoidal (Cᵒᵖ ⥤ E) hresCE
    letI := derivedMonoidal ((C × C)ᵒᵖ ⥤ E) hresCCE
    letI := Functor.constMapDerivedCategoryMonoidal hresE hresCE
    letI := Functor.constMapDerivedCategoryMonoidal hresE hresCCE
    letI := totalDerivedColimitOplaxMonoidal C E hresE hresCE
    letI := totalDerivedColimitOplaxMonoidal (C × C) E hresE hresCCE
    ∀ (_h07A4 : (diagPresheafRestriction C E).mapDerivedCategory.Monoidal)
      (α : (Functor.const ((C × C)ᵒᵖ) : E ⥤ _).mapDerivedCategory ⋙
            (diagPresheafRestriction C E).mapDerivedCategory ⟶
          (Functor.const Cᵒᵖ : E ⥤ _).mapDerivedCategory)
      (_h08PH : NatTrans.IsMonoidal α)
      (_h08QA : ∀ V : CosimplicialObject C, IsPointResolution V →
          IsPointResolution (V ⋙ Functor.diag C) →
          ∀ M : DerivedCategory ((C × C)ᵒᵖ ⥤ E),
            IsIso ((totalDerivedColimitAdjunction C E).restrictionMate
              (totalDerivedColimitAdjunction (C × C) E)
              (diagPresheafRestriction C E).mapDerivedCategory α M))
      (α₁ : (Functor.const Cᵒᵖ : E ⥤ _).mapDerivedCategory ⋙
            (fstPresheafRestriction C E).mapDerivedCategory ⟶
          (Functor.const ((C × C)ᵒᵖ) : E ⥤ _).mapDerivedCategory)
      (α₂ : (Functor.const Cᵒᵖ : E ⥤ _).mapDerivedCategory ⋙
            (sndPresheafRestriction C E).mapDerivedCategory ⟶
          (Functor.const ((C × C)ᵒᵖ) : E ⥤ _).mapDerivedCategory)
      (_h08QA₁ : ∀ V : CosimplicialObject (C × C), IsPointResolution V →
          IsPointResolution (V ⋙ CategoryTheory.Prod.fst C C) →
          ∀ M : DerivedCategory (Cᵒᵖ ⥤ E),
            IsIso ((totalDerivedColimitAdjunction (C × C) E).restrictionMate
              (totalDerivedColimitAdjunction C E)
              (fstPresheafRestriction C E).mapDerivedCategory α₁ M))
      (_h08QA₂ : ∀ V : CosimplicialObject (C × C), IsPointResolution V →
          IsPointResolution (V ⋙ CategoryTheory.Prod.snd C C) →
          ∀ M : DerivedCategory (Cᵒᵖ ⥤ E),
            IsIso ((totalDerivedColimitAdjunction (C × C) E).restrictionMate
              (totalDerivedColimitAdjunction C E)
              (sndPresheafRestriction C E).mapDerivedCategory α₂ M))
      (_h08QB : IsIso ((totalDerivedColimitAdjunction (C × C) E).externalMate
          (totalDerivedColimitAdjunction C E) (totalDerivedColimitAdjunction C E)
          (fstPresheafRestriction C E).mapDerivedCategory
          (sndPresheafRestriction C E).mapDerivedCategory α₁ α₂ K₁ K₂)),
      IsIso (totalDerivedColimitTensorComparison C E hresE hresCE K₁ K₂)
Tag 08QD, a remark

Tag 08QD in the Stacks Project.

Stacks.ChaoticSite.quasiIso_alexanderWhitney, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/FlatEilenbergZilber.lean, line 138. The attribute's comment: “flat_eilenberg_zilber”.

Stacks Project, Tag 08QD. The Alexander–Whitney map of two simplicial modules is a quasi-isomorphism. This is the Eilenberg–Zilber theorem: the Moore complex s(M ⊗_B N) of the degreewise tensor product is computed, through the canonical comparison, by the total complex s(M) ⊗_B s(N) of the double complex of the two Moore complexes.

public instance quasiIso_alexanderWhitney : QuasiIso (alexanderWhitney M N)

Stacks.ChaoticSite.simplexCategoryModuleEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/SimplexCategoryModuleCoefficients.lean, line 109. The attribute's comment: “Mod(B̲) is the category of simplicial B-modules”.

Stacks 08QD, Mod(B̲) on Δ. For the chaotic site Δ and a ring B, the category Mod(B̲) of modules over the constant sheaf of rings B̲ is the category of simplicial B-modules.

def simplexCategoryModuleEquivalence :
    SheafOfModules.{w} (simplexCategoryConstantRingSheaf B) ≌
      SimplicialObject (ModuleCat.{w} B)

Stacks.ChaoticSite.simplexCategoryMooreNatIsoDerivedLowerShriek, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/SimplexCategoryModuleCoefficients.lean, line 173. The attribute's comment: “Lπ_! sends a simplicial B-module M_• to its associated complex s(M_•), as an isomorphism in D(B) natural in M_•”.

Stacks 08QD, Lπ_! of a simplicial module is its associated complex. For the chaotic site Δ and a ring B, the derived lower shriek Lπ_! : D(B̲) ⥤ D(B) sends a simplicial B-module M_•, placed in degree zero, to its associated complex s(M_•), the alternating-face-map complex, read as a cochain complex in nonpositive degrees:

Q(s(M_•)) ≅ Lπ_!(M_•) in D(B), naturally in M_•.

Here Lπ_! is the total left derived functor of the colimit over Δᵒᵖ, which is π_! on the chaotic site by Example 08PF, and a B̲-module is a simplicial B-module by Stacks.ChaoticSite.simplexCategoryModuleEquivalence. The proof is Lemma 08Q9 for the point resolution U_• = 𝟭 Δ, at which the evaluation M(U_•) is M_• itself.

def simplexCategoryMooreNatIsoDerivedLowerShriek :
    alternatingFaceMapComplex (ModuleCat.{w} B) ⋙
        (ComplexShape.embeddingUpIntLE (0 : ℤ)).extendFunctor (ModuleCat.{w} B) ⋙
          DerivedCategory.Q ≅
      HomologicalComplex.single (SimplicialObject (ModuleCat.{w} B)) (ComplexShape.up ℤ) 0 ⋙
        DerivedCategory.Q ⋙ totalDerivedColimit SimplexCategory (ModuleCat.{w} B)

Stacks.ChaoticSite.flatEilenbergZilber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/SimplexCategoryModuleCoefficients.lean, line 200. The attribute's comment: “flat_eilenberg_zilber: for flat simplicial B-modules M_•, M'_•, the complex s(M_• ⊗_B M'_•) is quasi-isomorphic to the total complex of s(M_•) ⊗_B s(M'_•)”.

The Eilenberg–Zilber comparison holds for every commutative ring. For two degreewise flat simplicial B-modules the Moore complex of the degreewise tensor product is quasi-isomorphic to the total tensor product of the Moore complexes, the quasi-isomorphism being the Alexander–Whitney map AlgebraicTopology.alexanderWhitney (Stacks 08QD, Stacks.ChaoticSite.quasiIso_alexanderWhitney, which needs no flatness).

theorem flatEilenbergZilber.{t, s} (B : Type s) [CommRing B] :
    FlatEilenbergZilber.{t, s} B

Declarations registered for the tag:

Tag 08RX, a lemma

Tag 08RX in the Stacks Project.

Stacks.ChaoticSite.isIso_leftDerivedColimit_map_extensionByZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/CoefficientQuasiIsomorphism.lean, line 139. The attribute's comment: “the generators j_{U!}O_U; see the scope paragraph in the module docstring”.

Let C be a small category with the chaotic topology, let U_• be a cosimplicial object of C which is a point resolution, and let a : 𝒪 ⟶ 𝒪' be a morphism of abelian presheaves such that L_nπ_!(a) is invertible. Then for every object W of C the induced morphism j_{W!}𝒪_W ⟶ j_{W!}𝒪'_W of extensions by zero is also inverted by L_nπ_!.

Evaluated on U_• the two extensions by zero are the products of the simplicial set Mor_C(U_•, W) with the simplicial abelian groups 𝒪(U_•) and 𝒪'(U_•), and Mor_C(U_•, W) is homotopy equivalent to a singleton; so the projections to 𝒪(U_•) and 𝒪'(U_•) are inverted by the homology of the Moore complex, which reduces the claim to the hypothesis on a.

theorem isIso_leftDerivedColimit_map_extensionByZero (hU : IsPointResolution U)
    {P P' : Cᵒᵖ ⥤ AddCommGrpCat.{u}} (a : P ⟶ P') (W : C) (n : ℕ)
    (ha : IsIso (((colim : (Cᵒᵖ ⥤ AddCommGrpCat.{u}) ⥤ AddCommGrpCat.{u}).leftDerived n).map a)) :
    IsIso (((colim : (Cᵒᵖ ⥤ AddCommGrpCat.{u}) ⥤ AddCommGrpCat.{u}).leftDerived n).map
      (extensionByZeroPresheafMap a W))

Stacks.ChaoticSite.isIso_derivedColimitTensorComparison_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/CoefficientQuasiIsomorphismUnbounded.lean, line 146.

Tag 08RX. Let C be a small category with the chaotic topology and let a : 𝒪 ⟶ 𝒪' be a morphism of presheaves of rings on C (on a chaotic site, of sheaves of rings). Assume

  1. there is a cosimplicial object U_• of C as in Tag 08Q9, i.e. a point resolution: every Mor_C(U_•, W) is homotopy equivalent to the constant simplicial set on a singleton, and
  2. Lπ_!(𝒪) ⟶ Lπ_!(𝒪') is an isomorphism in D(Ab), where Lπ_! is derived lower shriek of abelian sheaves applied to the underlying morphism of abelian presheaves placed in degree zero.

Then for every object K of the unbounded derived category D(𝒪) = D(Mod(𝒪)) the canonical comparison

Lπ_!(K) ⟶ Lπ_!(K ⊗^L_𝒪 𝒪')

of Stacks.ChaoticSite.derivedColimitTensorComparison (induced by K ⟶ K ⊗^L_𝒪 𝒪') is an isomorphism in D(Ab).

The comparison is Lπ_! applied to the unit of the derived change-of-coefficients adjunction, followed by the identification Stacks.ChaoticSite.restrictScalarsDerivedColimitIso of Lπ_! on 𝒪'-modules with Lπ_! on their underlying 𝒪-modules (Stacks.ChaoticSite.isIso_derivedColimitTensorComparison_app_iff); so the assertion is the invertibility of the whiskered unit, which is a morphism of exact direct-sum-preserving functors on D(Mod(𝒪)) compatible with the shift. The free presheaves of modules on the representables — the generators j_{W!}𝒪_W of the source's proof — are projective, separating and compact, so the dévissage along compact generators of StacksDraft.CompactDevissage.isIso_of_isIso_app_single_anyModel reduces the assertion to those generators placed in degree zero, where it is Stacks.ChaoticSite.isIso_derivedColimitTensorComparison_app_single.

theorem isIso_derivedColimitTensorComparison_app (hU : IsPointResolution U)
    (ha : IsIso ((totalDerivedColimit C AddCommGrpCat.{u}).map
      ((DerivedCategory.singleFunctor (Cᵒᵖ ⥤ AddCommGrpCat.{u}) 0).map
        (Functor.whiskerRight a (forget₂ RingCat.{u} AddCommGrpCat.{u})))))
    (K : DerivedCategory (PresheafOfModules.{u} O)) :
    IsIso ((derivedColimitTensorComparison a).app K)
Tag 09CZ, a remark

Tag 09CZ in the Stacks Project.

Stacks.ChaoticSite.derivedColimitWithCoefficients, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/DerivedLowerShriek.lean, line 289. The attribute's comment: “derived_colimit_with_b_coefficients_2”.

Stacks 09CZ. For a map φ : O ⟶ B̲ from a sheaf of rings on a chaotic site to the constant sheaf of rings of a ring B, derived lower shriek with coefficients in O is the functor Lπ_! : D(O) ⟶ D(B) obtained by composing derived extension of scalars - ⊗^L_O B̲ with derived lower shriek D(B̲) ⟶ D(B).

def derivedColimitWithCoefficients :
    DerivedCategory (PresheafOfModules.{u} O) ⥤ DerivedCategory (ModuleCat.{u} B)

Stacks.ChaoticSite.derivedColimitWithCoefficients_commShift, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/DerivedLowerShriek.lean, line 305. The attribute's comment: “derived_colimit_with_b_coefficients_exact”.

Stacks 09CZ: derived lower shriek with coefficients commutes with the shift, being a left adjoint of a functor that does.

instance derivedColimitWithCoefficients_commShift :
    (derivedColimitWithCoefficients B O φ).CommShift ℤ

Stacks.ChaoticSite.derivedColimitWithCoefficients_isTriangulated, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/DerivedLowerShriek.lean, line 312. The attribute's comment: “derived_colimit_with_b_coefficients_exact”.

Stacks 09CZ: derived lower shriek with coefficients is an exact functor of triangulated categories D(O) ⟶ D(B).

instance derivedColimitWithCoefficients_isTriangulated :
    (derivedColimitWithCoefficients B O φ).IsTriangulated

Stacks.ChaoticSite.derivedColimitWithCoefficientsForgetNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/DerivedLowerShriekModuleStructure.lean, line 182. The attribute's comment: “the B-module structure on Lpi_!(K): the identification of Lpi^{Ab}_!(K) with the underlying object of D(Ab) of Lpi_!(K) read in D(B), for a cosimplicial point resolution and a coefficient map O -> B inducing an isomorphism Lpi_!O -> Lpi_!B. The functor Lpi_! : D(O) -> D(B) and its exactness, which need no hypothesis on the coefficient map, are Stacks.ChaoticSite.derivedColimitWithCoefficients, Stacks.ChaoticSite.derivedColimitWithCoefficients_commShift and Stacks.ChaoticSite.derivedColimitWithCoefficients_isTriangulated”.

Stacks 09CZ: the B-module structure on Lπ_!(K). Let C and B be as in Example 08PF, let U_• be a cosimplicial object of C which is a point resolution (Lemma 08Q9), and let φ : O ⟶ B̲ be a map to the constant sheaf of rings which induces an isomorphism Lπ_!O ⟶ Lπ_!B̲. Then derived lower shriek with coefficients in O on underlying abelian sheaves is derived lower shriek with coefficients in B, read on underlying abelian groups:

Lπ^{Ab}_!(K) ≅ Lπ_!(K) in D(Ab), naturally in K ∈ D(Mod(O)),

where the right-hand side is Stacks.ChaoticSite.derivedColimitWithCoefficients, the functor D(O) ⟶ D(B) of the tag. This is the remark's closing assertion, that Lπ_!(K) carries a B-module structure "coming from the (canonical, functorial) identification of Lπ_!(K) with Lπ_!(K ⊗_O^L B̲) of the lemma".

The remark is covered by this declaration together with the three that state the functor and its exactness: Stacks.ChaoticSite.derivedColimitWithCoefficients (the functor Lπ_! : D(O) ⟶ D(B), defined as - ⊗^L_O B̲ followed by Lπ_! : D(B̲) ⟶ D(B)), Stacks.ChaoticSite.derivedColimitWithCoefficients_commShift and Stacks.ChaoticSite.derivedColimitWithCoefficients_isTriangulated (it is an exact functor of triangulated categories), all in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/DerivedLowerShriek.lean. Those exist for every φ; the hypotheses of the remark enter only here, through Stacks 08RX (Stacks.ChaoticSite.derivedColimitTensorNatIso), and they are what makes the functor a lift of Lπ^{Ab}_!.

def derivedColimitWithCoefficientsForgetNatIso (U : CosimplicialObject C)
    (hU : IsPointResolution U)
    (ha : IsIso ((totalDerivedColimit C AddCommGrpCat.{u}).map
      ((DerivedCategory.singleFunctor (Cᵒᵖ ⥤ AddCommGrpCat.{u}) 0).map
        (Functor.whiskerRight φ (forget₂ RingCat.{u} AddCommGrpCat.{u}))))) :
    abelianDerivedColimitOfModules O ≅
      derivedColimitWithCoefficients B O φ ⋙
        (forget₂ (ModuleCat.{u} B) AddCommGrpCat.{u}).mapDerivedCategory
Sources
LeanStacks.CategoryHomology.categoryHomology · Stacks.ChaoticSite.abelianLowerShriekColimitIso · Stacks.ChaoticSite.abelianLowerShriekColimitIso_unit · Stacks.ChaoticSite.abelianLowerShriekColimit_evalIso · Stacks.ChaoticSite.abelianLowerShriekColimit_unit_cocone · Stacks.ChaoticSite.ModuleValued.moduleLowerShriekColimitIso · Stacks.ChaoticSite.ModuleValued.moduleLowerShriekColimitIso_unit · Stacks.ChaoticSite.ModuleValued.moduleLowerShriekColimit_evalIso

Section21.40 Calculating derived lower shriek#

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

Tag 08PI, a lemma

Tag 08PI in the Stacks Project.

Stacks.Sites.FibredCategory.fiberHomologyPresheafFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/FibreHomologyPresheaf.lean, line 124. The attribute's comment: “the presheaf of fibre homology”.

The presheaf of fibre homology. The presheaf L_{n,p}(F) on the base whose value at V is the homology H_n(C_V, F|_{C_V}) of the fibre at V, with restriction maps given by the chosen pullback functors and restriction of F along the chosen cartesian lifts, and regarded as a functor of the coefficient presheaf F.

def fiberHomologyPresheafFunctor (n : ℕ) :
    (s.Cᵒᵖ ⥤ AddCommGrpCat.{max w uD vD uC}) ⥤
      (s.base.Cᵒᵖ ⥤ AddCommGrpCat.{max w uD vD uC})

Stacks.Sites.FibredCategory.fiberHomologyPresheaf_obj, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/FibreHomologyPresheaf.lean, line 196. The attribute's comment: “the values of the presheaf of fibre homology”.

The values of the presheaf of fibre homology. Its value at V is the homology H_n(C_V, F|_{C_V}) of the fibre at V.

lemma fiberHomologyPresheaf_obj (F : s.Cᵒᵖ ⥤ AddCommGrpCat.{max w uD vD uC}) (n : ℕ)
    (V : s.base.Cᵒᵖ) :
    (fiberHomologyPresheaf s F n).obj V =
      CategoryHomology.categoryHomology.{uC, max w uD vD uC}
        ((Functor.Fiber.fiberInclusion (p := s.p) (S := V.unop)).op ⋙ F) n

Stacks.Sites.FibredCategory.fiberHomologyPresheaf_map, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/FibreHomologyPresheaf.lean, line 207. The attribute's comment: “the restriction maps of the presheaf of fibre homology”.

The restriction maps of the presheaf of fibre homology. The restriction map along h : V' ⟶ V is the map on homology of Stacks 08PH attached to the chosen pullback functor h^* and to restriction of F along the chosen cartesian lifts of h.

lemma fiberHomologyPresheaf_map (F : s.Cᵒᵖ ⥤ AddCommGrpCat.{max w uD vD uC}) (n : ℕ)
    {V V' : s.base.C} (h : V' ⟶ V) :
    (fiberHomologyPresheaf s F n).map h.op =
      CategoryHomology.categoryHomologyMap.{uC, uC, max w uD vD uC}
        ((Functor.chosenPullbacks s.p).pullbackFunctor h) (fiberCartesianRestriction s F h) n

Stacks.Sites.FibredCategory.fiberHomologyPresheafFunctor_map_app, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/FibreHomologyPresheaf.lean, line 218. The attribute's comment: “functoriality of the presheaf of fibre homology in the coefficients”.

Functoriality of the presheaf of fibre homology in the coefficients. The map induced by α : F ⟶ G is the map on homology of Stacks 08PH attached to the identity functor of the fibre and to α restricted to it.

lemma fiberHomologyPresheafFunctor_map_app {F G : s.Cᵒᵖ ⥤ AddCommGrpCat.{max w uD vD uC}}
    (α : F ⟶ G) (n : ℕ) (V : s.base.Cᵒᵖ) :
    ((fiberHomologyPresheafFunctor s n).map α).app V =
      CategoryHomology.categoryHomologyMap.{uC, uC, max w uD vD uC} (𝟭 (s.p.Fiber V.unop))
        (Functor.whiskerLeft (Functor.Fiber.fiberInclusion (p := s.p) (S := V.unop)).op α) n

Stacks.Sites.FibredCategory.fiberHomologySheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/FibreHomologyPresheaf.lean, line 228. The attribute's comment: “the sheaf of fibre homology”.

The sheaf L_n(F) of fibre homology. The abelian sheaf on the base associated to the presheaf of fibre homology.

abbrev fiberHomologySheaf [HasWeakSheafify s.base.J AddCommGrpCat.{max w uD vD uC}]
    (F : s.Cᵒᵖ ⥤ AddCommGrpCat.{max w uD vD uC}) (n : ℕ) :
    Sheaf s.base.J AddCommGrpCat.{max w uD vD uC}

Stacks.Sites.FibredCategory.fiberHomologySheaf_sheafify, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/FibreHomologySheafification.lean, line 1245.

Sheafifying the coefficients on the total category does not change the associated sheaf of fibre homology.

theorem fiberHomologySheaf_sheafify
    [HasWeakSheafify s.base.J AddCommGrpCat.{max w uD vD uC}]
    [HasWeakSheafify s.topology AddCommGrpCat.{max w uD vD uC}]
    (F : s.Cᵒᵖ ⥤ AddCommGrpCat.{max w uD vD uC}) (n : ℕ) :
    IsIso ((presheafToSheaf s.base.J AddCommGrpCat.{max w uD vD uC}).map
      ((fiberHomologyPresheafFunctor s n).map
        ((sheafificationAdjunction s.topology AddCommGrpCat.{max w uD vD uC}).unit.app F)))

Stacks.Sites.FibredCategory.fiberHomologySheafSheafifyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/FibreHomologySheafification.lean, line 1290. The attribute's comment: “the sheaf of fibre homology is unchanged by sheafifying the coefficients”.

Stacks 08PI. The sheaf L_n(F) of fibre homology is unchanged when the coefficient presheaf is replaced by its sheafification on the total category: the canonical map L_n(F) ⟶ L_n(F^#) of fiberHomologySheaf_sheafify is an isomorphism.

def fiberHomologySheafSheafifyIso
    [HasWeakSheafify s.base.J AddCommGrpCat.{max w uD vD uC}]
    [HasWeakSheafify s.topology AddCommGrpCat.{max w uD vD uC}]
    (F : s.Cᵒᵖ ⥤ AddCommGrpCat.{max w uD vD uC}) (n : ℕ) :
    fiberHomologySheaf s F n ≅
      fiberHomologySheaf s
        ((sheafToPresheaf s.topology AddCommGrpCat.{max w uD vD uC}).obj
          ((presheafToSheaf s.topology AddCommGrpCat.{max w uD vD uC}).obj F)) n
Tag 08PJ, a lemma

Tag 08PJ in the Stacks Project.

Stacks.Sites.FibredCategory.FibredCategorySituation.derivedLowerShriekHomologyIsoFiberHomology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/UliftFreeCoverGenerators.lean, line 356.

Stacks 08PJ. Let p : C ⥤ D be a fibred category over a ringed site D, with C carrying the inherited topology and π the induced morphism of topoi (Stacks 08P8). For every n ≥ 0, the functor F ↦ L_n π_!(F) = H^{-n}(Lπ_! F) on abelian sheaves on C is the functor F ↦ L_n(F) of Stacks 08PI, the sheaf on D associated to the presheaf V ↦ H_n(C_V, F|_{C_V}), naturally in F.

Here Lπ_! is the left derived functor whose existence is Stacks 07AC (hasPointwiseLeftDerivedFunctor_abelianLowerShriekOnHomotopy), and the two acyclicity inputs of the comparison derivedLowerShriekHomologyIso are proved for every fibred situation: abelianLowerShriekAcyclic and abelianLowerShriekGeneratorsAcyclic.

def derivedLowerShriekHomologyIsoFiberHomology (n : ℕ) :
    s.derivedAbelianLowerShriekHomology n ≅
      sheafToPresheaf s.topology AddCommGrpCat.{max w uD vD uC} ⋙
        fiberHomologyPresheafFunctor s n ⋙
          presheafToSheaf s.base.J AddCommGrpCat.{max w uD vD uC}
Tag 08PK, a lemma

Tag 08PK in the Stacks Project.

Stacks.Sites.FibredCategory.MorphismSituation.derivedAbelianLowerShriekHomologyObjIsoFiberHomologySheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/DerivedLowerShriekMorphismFibreHomology.lean, line 574. The attribute's comment: “L_n g_!(F') is the sheaf of H_n(I_U, F'_U); assumes 07AC and cover acyclicity”.

For an abelian sheaf F' on the source, L_n g_!(F') is the sheaf on the total category associated to the presheaf U ↦ H_n(I_U, F'_U). This takes as hypotheses the acyclicity conditions h for g_! and h'' for g''_! and the cover acyclicity hcov of the amelioration.

def derivedAbelianLowerShriekHomologyObjIsoFiberHomologySheaf
    (h : S.AbelianLowerShriekAcyclic)
    (h'' : (amelioratedSituation S).AbelianLowerShriekAcyclic)
    (hcov : (amelioratedSituation S).UliftFreeCoverLowerShriekAcyclic) (n : ℕ)
    (F' : Sheaf S.sourceTopology AddCommGrpCat.{max w u₀ u₁ u₂ v₀ v₁ v₂}) :
    (S.derivedAbelianLowerShriekHomology n).obj F' ≅
      fiberHomologySheaf (amelioratedSituation S)
        ((amelioratedLowerShriek S).obj F').obj n

Stacks.Sites.FibredCategory.MorphismSituation.derivedAbelianLowerShriekHomologyObjIsoFiberHomologySheaf_unconditional, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/DerivedLowerShriekMorphismFibreHomologyUnconditional.lean, line 121. The attribute's comment: “L_n g_!(F') is the sheaf of H_n(I_U, F'_U)”.

For an abelian sheaf F' on the source, L_n g_!(F') is the sheaf on the total category associated to the presheaf U ↦ H_n(I_U, F'_U), where I_U is the fibre over U of the amelioration of u.

def derivedAbelianLowerShriekHomologyObjIsoFiberHomologySheaf_unconditional (n : ℕ)
    (F' : Sheaf S.sourceTopology AddCommGrpCat.{max w u₀ u₁ u₂ v₀ v₁ v₂}) :
    (S.derivedAbelianLowerShriekHomology n).obj F' ≅
      fiberHomologySheaf (amelioratedSituation S)
        ((amelioratedLowerShriek S).obj F').obj n
Sources
LeanStacks.Sites.FibredCategory.fiberHomologyPresheafFunctor · Stacks.Sites.FibredCategory.fiberHomologyPresheaf_obj · Stacks.Sites.FibredCategory.fiberHomologyPresheaf_map · Stacks.Sites.FibredCategory.fiberHomologyPresheafFunctor_map_app · Stacks.Sites.FibredCategory.fiberHomologySheaf · Stacks.Sites.FibredCategory.fiberHomologySheaf_sheafify · Stacks.Sites.FibredCategory.fiberHomologySheafSheafifyIso · Stacks.Sites.FibredCategory.FibredCategorySituation.derivedLowerShriekHomologyIsoFiberHomology

Section21.41 Simplicial modules#

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

Tag 09D0, the section

Tag 09D0 in the Stacks Project.

Stacks.SimplicialModules.derivedProjectionLowerShriekIsoMooreComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Simplicial/DerivedProjectionMooreComplex.lean, line 496. The attribute's comment: “Lπ_!(ℱ_•) is represented by the alternating-face-map complex s(ℱ_•) of the simplicial abelian sheaf ℱ_•, for every abelian sheaf on Δ × C — in particular for the underlying abelian sheaf of a simplicial A_•-module over any simplicial sheaf of rings A_•, the Lπ_! of the section being the abelian one of Remark 09CY. Proved from Stacks 08PJ's two inputs as the source directs: the acyclicity of π_! and the Moore computation over Δ”.

Stacks 09D0. Let (C, J) be a small site and let Δ × C carry the topology inherited from (C, J) along the projection π : Δ × C ⥤ C. For every sheaf of abelian groups ℱ on Δ × C, the abelian derived lower shriek of Remark 09CY carries ℱ to the associated chain complex of the simplicial abelian sheaf ℱ_• that ℱ is:

Lπ_!(ℱ[0]) ≅ s(ℱ_•) in D(Ab(C)),

where s(ℱ_•) is the alternating-face-map complex of ℱ_• = fibrewise ℱ, read as a cochain complex over ℤ in non-positive degrees.

This is the source's own argument: a resolution of ℱ by direct sums of the free abelian sheaves j_{W!}ℤ_W (Stacks 06XX) computes Lπ_! because π_! is acyclic on those (Stacks.SimplicialModules.abelianLowerShriekAcyclic_projection, which is Lemma 21.40.2), and the degreewise colimit over Δᵒᵖ of such a resolution is the Moore complex (Stacks.ChaoticSite.GeneralValued.mooreCochainQIsoColimOfResolution, which is Lemma 21.39.7).

def derivedProjectionLowerShriekIsoMooreComplex
    (F : Sheaf (projectionTopology C J) AddCommGrpCat.{w}) :
    (derivedAbelianLowerShriek.{w} (projectionTopology C J) J (projection C)).obj
        (DerivedCategory.Q.obj
          ((HomologicalComplex.single (Sheaf (projectionTopology C J) AddCommGrpCat.{w})
            (ComplexShape.up ℤ) 0).obj F)) ≅
      DerivedCategory.Q.obj
        ((Stacks.ChaoticSite.GeneralValued.mooreCochainComplex (𝟭 SimplexCategory)
          (Sheaf J AddCommGrpCat.{w})).obj ((fibrewise J AddCommGrpCat.{w}).obj F))

Stacks.SimplicialModules.derivedProjectionLowerShriekIsoMooreComplexModules, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Simplicial/DerivedProjectionMooreComplexModules.lean, line 236. The attribute's comment: “the MODULE-coefficient representation: for a simplicial sheaf of O-modules ℱ_•, equivalently a sheaf of π^{-1}O-modules on Δ × C, Lπ_!(ℱ_•) is represented by the associated chain complex s(ℱ_•) in D(O). This is the form in which the untagged paragraph of Section 09D0 is used by Tag 09DH, whose triangle lives in D(ℬ); the abelian registration beside it, derivedProjectionLowerShriekIsoMooreComplex, cannot reach it because derived lower shriek does not commute with forgetting the module structure”.

Stacks 09D0 at module coefficients. Let (C, J) be a small site, let O be a sheaf of rings on it and let Δ × C carry the topology inherited from (C, J) along the projection π : Δ × C ⥤ C. For every sheaf of π^{-1}O-modules ℱ on Δ × C, the derived lower shriek of Remark 09CY carries ℱ to the associated chain complex of the simplicial sheaf of O-modules ℱ_• that ℱ is:

Lπ_!(ℱ[0]) ≅ s(ℱ_•) in D(O),

where s(ℱ_•) is the alternating-face-map complex of ℱ_• = fibrewiseMod ℱ, read as a cochain complex over ℤ in non-positive degrees.

This is the source's own argument, run at module coefficients: a resolution of ℱ by direct sums of the j_{W!}(π^{-1}O)_W (Stacks 06XX) computes Lπ_! because π_! is acyclic on those (Stacks.Cohomology.DerivedLowerShriek.lowerShriekAcyclic_of_preservesCoveringPullbacks, which is Lemma 21.40.2), and the degreewise colimit over Δᵒᵖ of such a resolution is the Moore complex (Stacks.ChaoticSite.GeneralValued.mooreCochainQIsoColimOfResolution, which is Lemma 21.39.7).

def derivedProjectionLowerShriekIsoMooreComplexModules
    (F : SheafOfModules.{w} (projectionRing C J O)) :
    (derivedProjectionLowerShriek C J O).obj
        (DerivedCategory.Q.obj
          ((HomologicalComplex.single (SheafOfModules.{w} (projectionRing C J O))
            (ComplexShape.up ℤ) 0).obj F)) ≅
      DerivedCategory.Q.obj
        ((Stacks.ChaoticSite.GeneralValued.mooreCochainComplex (𝟭 SimplexCategory)
          (SheafOfModules.{w} O)).obj ((fibrewiseMod C J O).obj F))

Stacks.SimplicialModules.simplicialSheafEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Simplicial/SimplicialSheafEquivalence.lean, line 362. The attribute's comment: “a simplicial sheaf on C is the same thing as a sheaf on Δ × C for the topology inherited along π”.

Stacks 09D0. A sheaf on Δ × C is a simplicial sheaf on C: levelwise restriction to the fibres and uncurrying are an equivalence of categories.

def simplicialSheafEquivalence (A : Type u₁) [Category.{v₁} A] :
    Sheaf ((CategoryTheory.Prod.snd SimplexCategory C).inheritedTopology J) A ≌
      CategoryTheory.SimplicialObject (Sheaf J A)
Tag 09D1, a definition

Tag 09D1 in the Stacks Project.

Stacks.SimplicialModules.SimplicialModule, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Simplicial/SimplicialModules.lean, line 50.

A simplicial module over a simplicial sheaf of rings A is a presheaf of modules over the associated ring presheaf on Δ × C whose underlying abelian-group presheaf is a sheaf for the topology inherited from C.

abbrev SimplicialModule (A : SimplicialObject (Sheaf J RingCat.{r}))

Stacks.SimplicialModules.ringSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Simplicial/SimplicialModulesAbelian.lean, line 275. The attribute's comment: “the sheaf of rings on Δ × C associated to A_•”.

Stacks 09D1. The sheaf of rings on Δ × C associated to a simplicial sheaf of rings. The sheaf condition is isSheaf_associatedRingPresheaf.

def ringSheaf :
    Sheaf ((CategoryTheory.Prod.snd SimplexCategory C).inheritedTopology J) RingCat.{r}
Tag 09D2, a lemma

Tag 09D2 in the Stacks Project.

Stacks.SimplicialModules.isIso_derivedBaseChangeComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Simplicial/LowerShriekBaseChange.lean, line 330.

Let C be a site and A_• ⟶ B_• a homomorphism of simplicial sheaves of (commutative) rings on C. If Lπ_!A_• ⟶ Lπ_!B_• is an isomorphism in D(C), then the canonical map Lπ_!(K) ⟶ Lπ_!(K ⊗^L_{A_•} B_•) is an isomorphism for every K in D(A_•).

theorem isIso_derivedBaseChangeComparison : IsIso (derivedBaseChangeComparison J φ)

Stacks.SimplicialModules.isIso_derivedLowerShriekHomology_map_of_fibrewise, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Simplicial/SimplicialSiteLowerShriek.lean, line 146. The attribute's comment: “the reduction to the fibre categories Δ × U”.

The reduction of Stacks 09D2 to the fibre categories. Let C be a site and let π : Δ × C ⥤ C be the projection. A morphism a of abelian sheaves on Δ × C which induces an isomorphism on the degree n homology of the fibre over every object of C is inverted by L_nπ_!.

This is the step of the proof of Stacks 09D2 which, both sides of the asserted identity being sheaves, computes their cohomology sheaves by the procedure of Stacks 08PI and so reduces the lemma to the restriction of the coefficients to the fibre categories Δ × U, where the source appeals to Stacks 08RX. It is not the lemma: the derived tensor product, the flat resolution and Stacks 08RX itself do not appear. See the scope paragraph of the module docstring.

The two acyclicity statements of Stacks 08PJ are taken as arguments here; isIso_derivedLowerShriekHomology_map_of_fibrewise_unconditional is the same reduction with both discharged.

theorem isIso_derivedLowerShriekHomology_map_of_fibrewise
    (h : (simplicialSituation B).AbelianLowerShriekAcyclic)
    (hcov : (simplicialSituation B).UliftFreeCoverLowerShriekAcyclic) (n : ℕ)
    {F G : Sheaf (simplicialSituation B).topology AddCommGrpCat.{max w u}} (a : F ⟶ G)
    (ha : ∀ U : B.Cᵒᵖ, IsIso (((fiberHomologyPresheafFunctor (simplicialSituation B) n).map
      ((sheafToPresheaf (simplicialSituation B).topology
        AddCommGrpCat.{max w u}).map a)).app U)) :
    IsIso (((simplicialSituation B).derivedAbelianLowerShriekHomology n).map a)

Stacks.SimplicialModules.isIso_derivedLowerShriekHomology_map_of_fibrewise_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Simplicial/SimplicialSiteLowerShriek.lean, line 172. The attribute's comment: “the reduction to the fibre categories Δ × U”.

The reduction of Stacks 09D2 to the fibre categories, with no hypothesis. Let C be a site and let π : Δ × C ⥤ C be the projection. A morphism a of abelian sheaves on Δ × C which induces an isomorphism on the degree n homology of the fibre over every object of C is inverted by L_nπ_!.

Both acyclicity statements of Stacks 08PJ are discharged rather than carried: StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/ProjectionLowerShriekAcyclic.lean proves Stacks 0D6X along the projection of a fibred category, hence FibredCategorySituation.abelianLowerShriekAcyclic and the instance giving Lπ_!, and StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/UliftFreeCoverGenerators.lean proves FibredCategorySituation.abelianLowerShriekGeneratorsAcyclic, from which the acyclicity of the sheafified canonical presentation follows by uliftFreeCoverLowerShriekAcyclic_of_generatorsAcyclic.

It is still not the lemma, for the reasons in the scope paragraph of the module docstring.

theorem isIso_derivedLowerShriekHomology_map_of_fibrewise_unconditional (n : ℕ)
    {F G : Sheaf (simplicialSituation B).topology AddCommGrpCat.{max w u}} (a : F ⟶ G)
    (ha : ∀ U : B.Cᵒᵖ, IsIso (((fiberHomologyPresheafFunctor (simplicialSituation B) n).map
      ((sheafToPresheaf (simplicialSituation B).topology
        AddCommGrpCat.{max w u}).map a)).app U)) :
    IsIso (((simplicialSituation B).derivedAbelianLowerShriekHomology n).map a)
Tag 09D3, a remark

Tag 09D3 in the Stacks Project.

Stacks.SimplicialModules.augmentedDerivedLowerShriek, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Simplicial/AugmentedDerivedLowerShriek.lean, line 149. The attribute's comment: “the functor Lπ_! : D(A_•) ⟶ D(O), the composition of - ⊗^L_{A_•} O with the functor Lπ_! : D(Δ × C, π^{-1}O) ⟶ D(O) of Remark 09CY”.

Remark 09D3, the functor. For an augmentation ε : A_• ⟶ O of a simplicial sheaf of rings by a sheaf of rings, Lπ_! : D(A_•) ⥤ D(O) is the composite of derived base change - ⊗^L_{A_•} O : D(A_•) ⥤ D(Δ × C, π^{-1}O) with the functor Lπ_! : D(Δ × C, π^{-1}O) ⥤ D(O) of Remark 09CY.

def augmentedDerivedLowerShriek (ε : CommAugmentation J A O) :
    DerivedCategory (Modules J A) ⥤
      DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf O))

Stacks.SimplicialModules.augmentedDerivedLowerShriek_commShift, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Simplicial/AugmentedDerivedLowerShriek.lean, line 157. The attribute's comment: “Lπ_! : D(A_•) ⟶ D(O) is a functor of triangulated categories: it commutes with the shift”.

Remark 09D3, exactness: the functor commutes with the shift.

instance augmentedDerivedLowerShriek_commShift (ε : CommAugmentation J A O) :
    (augmentedDerivedLowerShriek J ε).CommShift ℤ

Stacks.SimplicialModules.augmentedDerivedLowerShriek_isTriangulated, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Simplicial/AugmentedDerivedLowerShriek.lean, line 164. The attribute's comment: “Lπ_! : D(A_•) ⟶ D(O) is an exact functor of triangulated categories”.

Remark 09D3, exactness: Lπ_! : D(A_•) ⥤ D(O) is an exact functor of triangulated categories, as a composite of two exact functors.

instance augmentedDerivedLowerShriek_isTriangulated (ε : CommAugmentation J A O) :
    (augmentedDerivedLowerShriek J ε).IsTriangulated

Stacks.SimplicialModules.augmentedDerivedLowerShriekForgetIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Simplicial/AugmentedDerivedLowerShriek.lean, line 398. The attribute's comment: “the O-module structure on Lπ_!(K): under the hypothesis that ε induces a quasi-isomorphism s(A_•) ⟶ O, the canonical, functorial identification of Lπ_!(K) with Lπ_!(K ⊗^L_{A_•} O) of Lemma 09D2, read as the underlying complex of abelian sheaves of the object Lπ_!(K) of D(O)”.

Remark 09D3, the O-module structure on Lπ_!(K). Let ε : A_• ⟶ O be an augmentation inducing a quasi-isomorphism s(A_•) ⟶ O. For K in D(A_•), Lπ_!(K) is canonically and functorially identified with Lπ_!(K ⊗^L_{A_•} O) by Lemma 09D2, and the latter is, by Remark 09CY, the underlying complex of abelian sheaves of the object Lπ_!(K) of D(O) of augmentedDerivedLowerShriek. So, naturally in K, forgetting the O-module structure of the functor of the source gives back Lπ_!(K).

def augmentedDerivedLowerShriekForgetIso (ε : CommAugmentation J A O)
    (hε : InducesQuasiIso J ε) :
    augmentedDerivedLowerShriek J ε ⋙
        (SheafOfModules.toSheaf (Stacks.SheafOfModules.Tensor.ringSheaf O)).mapDerivedCategory ≅
      moduleDerivedLowerShriek J A

Stacks.SimplicialModules.augmentedLowerShriek, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Simplicial/AugmentedLowerShriek.lean, line 155. The attribute's comment: “the functor Lπ_! : D(A_•) ⟶ D(O). Two inputs of the source are carried as explicit parameters, the library not yet having them: base is derived extension of scalars - ⊗^L_{A_•} O, introduced in the untagged prose before Lemma 09D2, and proj is the functor Lπ_! : D(π^{-1}O) ⟶ D(O) of Tag 09CY, which is Tag 08PC part (3) for modules and is reduced in this library to the acyclicity statement of Tag 0794 at the class of direct sums of the j_{U!} O_U; see the implementation notes for what that still owes”.

Stacks 09D3. Derived lower shriek along an augmented simplicial sheaf of rings: Lπ_! : D(A_•) ⟶ D(O), the composite of derived extension of scalars along the augmentation with derived lower shriek on modules over π^{-1}O.

def augmentedLowerShriek (_ε : Augmentation J A O)
    (base : DerivedCategory (SimplicialModule.{w, v, u, r} J A) ⥤
      DerivedCategory (SimplicialModule.{w, v, u, r} J (constantRing J O)))
    (proj : DerivedCategory (SimplicialModule.{w, v, u, r} J (constantRing J O)) ⥤
      DerivedCategory D) :
    DerivedCategory (SimplicialModule.{w, v, u, r} J A) ⥤ DerivedCategory D

Stacks.SimplicialModules.augmentedLowerShriek_commShift, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Simplicial/AugmentedLowerShriek.lean, line 166. The attribute's comment: “the functor commutes with the shift”.

Stacks 09D3. Derived lower shriek along an augmented simplicial sheaf of rings commutes with the shift.

instance augmentedLowerShriek_commShift (ε : Augmentation J A O)
    (base : DerivedCategory (SimplicialModule.{w, v, u, r} J A) ⥤
      DerivedCategory (SimplicialModule.{w, v, u, r} J (constantRing J O)))
    (proj : DerivedCategory (SimplicialModule.{w, v, u, r} J (constantRing J O)) ⥤
      DerivedCategory D) [base.CommShift ℤ] [proj.CommShift ℤ] :
    (augmentedLowerShriek J ε base proj).CommShift ℤ

Stacks.SimplicialModules.augmentedLowerShriek_isTriangulated, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Simplicial/AugmentedLowerShriek.lean, line 177. The attribute's comment: “the functor is exact”.

Stacks 09D3. Derived lower shriek along an augmented simplicial sheaf of rings is an exact functor of triangulated categories.

instance augmentedLowerShriek_isTriangulated (ε : Augmentation J A O)
    (base : DerivedCategory (SimplicialModule.{w, v, u, r} J A) ⥤
      DerivedCategory (SimplicialModule.{w, v, u, r} J (constantRing J O)))
    (proj : DerivedCategory (SimplicialModule.{w, v, u, r} J (constantRing J O)) ⥤
      DerivedCategory D) [base.CommShift ℤ] [proj.CommShift ℤ]
    [base.IsTriangulated] [proj.IsTriangulated] :
    (augmentedLowerShriek J ε base proj).IsTriangulated

Stacks.SimplicialModules.augmentedLowerShriek_derivedTarget, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Simplicial/AugmentedLowerShriek.lean, line 210. The attribute's comment: “the functor Lπ_! : D(A_•) ⟶ D(O), at the target D(O) the source names and with the abelian structure and the derived category of both categories of simplicial modules discharged rather than assumed. Two inputs of the source are carried as explicit parameters, the library not yet having them: base is derived extension of scalars - ⊗^L_{A_•} O, introduced in the untagged prose before Lemma 09D2, and proj is the functor Lπ_! : D(π^{-1}O) ⟶ D(O) of Tag 09CY, whose underived half is Stacks.SimplicialModules.moduleLowerShriek and whose total left derived functor is part (3) of Tag 08PC, open here”.

Stacks 09D3. Derived lower shriek along an augmented simplicial sheaf of rings, Lπ_! : D(A_•) ⟶ D(O) with D(O) the derived category of the sheaves of O-modules on C, which is the D(O) of the source.

Nothing is assumed about either category of simplicial modules: the abelian structure is Stacks.SimplicialModules.abelian and the derived category is HasDerivedCategory.standard, both seated as local instances. That abelian structure is supplied at sections universe max u v r w, which is why the module sections are taken there.

def augmentedLowerShriek_derivedTarget (_ε : Augmentation J A O)
    (base : DerivedCategory (SimplicialModule.{max u v r w, v, u, r} J A) ⥤
      DerivedCategory (SimplicialModule.{max u v r w, v, u, r} J (constantRing J O)))
    (proj : DerivedCategory (SimplicialModule.{max u v r w, v, u, r} J (constantRing J O)) ⥤
      DerivedCategory (SheafOfModules.{max u v r w} O)) :
    DerivedCategory (SimplicialModule.{max u v r w, v, u, r} J A) ⥤
      DerivedCategory (SheafOfModules.{max u v r w} O)

Stacks.SimplicialModules.augmentedLowerShriek_derivedTarget_commShift, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Simplicial/AugmentedLowerShriek.lean, line 222. The attribute's comment: “the functor commutes with the shift, at the target D(O) the source names”.

Stacks 09D3. Derived lower shriek along an augmented simplicial sheaf of rings commutes with the shift, at the target D(O).

instance augmentedLowerShriek_derivedTarget_commShift (ε : Augmentation J A O)
    (base : DerivedCategory (SimplicialModule.{max u v r w, v, u, r} J A) ⥤
      DerivedCategory (SimplicialModule.{max u v r w, v, u, r} J (constantRing J O)))
    (proj : DerivedCategory (SimplicialModule.{max u v r w, v, u, r} J (constantRing J O)) ⥤
      DerivedCategory (SheafOfModules.{max u v r w} O))
    [base.CommShift ℤ] [proj.CommShift ℤ] :
    (augmentedLowerShriek_derivedTarget.{w} J ε base proj).CommShift ℤ

Stacks.SimplicialModules.augmentedLowerShriek_derivedTarget_isTriangulated, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Simplicial/AugmentedLowerShriek.lean, line 234. The attribute's comment: “the functor is exact, at the target D(O) the source names”.

Stacks 09D3. Derived lower shriek along an augmented simplicial sheaf of rings is an exact functor of triangulated categories, at the target D(O).

instance augmentedLowerShriek_derivedTarget_isTriangulated (ε : Augmentation J A O)
    (base : DerivedCategory (SimplicialModule.{max u v r w, v, u, r} J A) ⥤
      DerivedCategory (SimplicialModule.{max u v r w, v, u, r} J (constantRing J O)))
    (proj : DerivedCategory (SimplicialModule.{max u v r w, v, u, r} J (constantRing J O)) ⥤
      DerivedCategory (SheafOfModules.{max u v r w} O))
    [base.CommShift ℤ] [proj.CommShift ℤ]
    [base.IsTriangulated] [proj.IsTriangulated] :
    (augmentedLowerShriek_derivedTarget.{w} J ε base proj).IsTriangulated
Sources
LeanStacks.SimplicialModules.derivedProjectionLowerShriekIsoMooreComplex · Stacks.SimplicialModules.derivedProjectionLowerShriekIsoMooreComplexModules · Stacks.SimplicialModules.simplicialSheafEquivalence · Stacks.SimplicialModules.SimplicialModule · Stacks.SimplicialModules.ringSheaf · Stacks.SimplicialModules.isIso_derivedBaseChangeComparison · Stacks.SimplicialModules.isIso_derivedLowerShriekHomology_map_of_fibrewise · Stacks.SimplicialModules.isIso_derivedLowerShriekHomology_map_of_fibrewise_unconditional

Section21.42 Cohomology on a category#

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

Tag 08RZ, an example

Tag 08RZ in the Stacks Project.

Stacks.CategoryCohomology.cochainReplacement, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/CochainReplacement.lean, line 226. The attribute's comment: “the cochain replacement”.

The functorial cosimplicial cochain replacement of an abelian presheaf.

noncomputable def cochainReplacement
    (C : Type u) [SmallCategory C] :
    {K : (Cᵒᵖ ⥤ AddCommGrpCat.{max u v}) ⥤ CosimplicialObject AddCommGrpCat.{max u v} //
      IsCochainReplacement C K}

Stacks.CategoryCohomology.cochainReplacementComplex_preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/CochainReplacement.lean, line 332. The attribute's comment: “left exactness of the replacement”.

The cochain replacement preserves finite limits, degree by degree.

theorem cochainReplacementComplex_preservesFiniteLimits
    (C : Type u) [SmallCategory C] :
    PreservesFiniteLimits (cochainReplacementComplex C)

Stacks.CategoryCohomology.cochainReplacementComplex_preservesFiniteColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/CochainReplacement.lean, line 340. The attribute's comment: “right exactness of the replacement”.

The cochain replacement preserves finite colimits, degree by degree.

theorem cochainReplacementComplex_preservesFiniteColimits
    (C : Type u) [SmallCategory C] :
    PreservesFiniteColimits (cochainReplacementComplex C)

Stacks.CategoryCohomology.cochainReplacementDeltaFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/CochainReplacement.lean, line 410. The attribute's comment: “cohomological delta functor”.

The homology functors of the replacement, with their natural connecting morphisms, form a cohomological delta functor.

noncomputable def cochainReplacementDeltaFunctor
    (C : Type u) [SmallCategory C] :
    {D : DeltaFunctor (Cᵒᵖ ⥤ AddCommGrpCat.{max u v}) AddCommGrpCat.{max u v} //
      ∀ n, D.functor n = cochainReplacementComplex C ⋙
        HomologicalComplex.homologyFunctor AddCommGrpCat.{max u v} (ComplexShape.up ℕ) n}

Stacks.CategoryCohomology.cochainReplacementZeroHomologyIsoLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/CochainReplacement.lean, line 562. The attribute's comment: “degree-zero cohomology”.

The zeroth cohomology of the replacement is naturally the limit of the presheaf.

theorem cochainReplacementZeroHomologyIsoLimit
    (C : Type u) [SmallCategory C] :
    Nonempty
      (cochainReplacementComplex C ⋙
          HomologicalComplex.homologyFunctor AddCommGrpCat.{max u v} (ComplexShape.up ℕ) 0 ≅
        (lim : (Cᵒᵖ ⥤ AddCommGrpCat.{max u v}) ⥤ AddCommGrpCat.{max u v}))

Stacks.CategoryCohomology.pointSimplicialReplacement_contractible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/CochainReplacement.lean, line 652. The attribute's comment: “contractibility of the point simplicial replacement”.

The simplicial set of chains U₀ ⟶ ⋯ ⟶ Uₙ equipped with a map U ⟶ U₀ is the nerve of the under-category of U, and is simplicially homotopy equivalent to a point.

theorem pointSimplicialReplacement_contractible
    (C : Type u) [SmallCategory C] (U : C) :
    ∃ f : nerve (Under U) ⟶ ⊤_ SSet.{u},
      SimplicialObject.homotopyEquivalences (Type u) f

Stacks.CategoryCohomology.cochainReplacementPointIsoNerve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/CochainReplacement.lean, line 808. The attribute's comment: “point-pushforward replacement as maps from the nerve”.

The degree-n replacement of the point-pushforward of A is the group of maps from the n-simplices of the nerve of Under U to A. These identifications intertwine every coface with precomposition by the corresponding simplicial face, hence identify the cochain complexes.

theorem cochainReplacementPointIsoNerve
    (C : Type u) [SmallCategory C] (U : C) (A : AddCommGrpCat.{max u v}) :
    ∃ e : ∀ n : ℕ,
        (((cochainReplacement C).1.obj
          ((sheafBotEquivalence (C := C) AddCommGrpCat.{max u v}).functor.obj
            ((GrothendieckTopology.pointBot U).skyscraperSheafFunctor.obj A))).obj (.mk n)) ≅
          AddCommGrpCat.of (ComposableArrows (Under U) n → A),
      ∀ (n : ℕ) (i : Fin (n + 2)) (x : ComposableArrows (Under U) (n + 1))
          (s : ((cochainReplacement C).1.obj
            ((sheafBotEquivalence (C := C) AddCommGrpCat.{max u v}).functor.obj
              ((GrothendieckTopology.pointBot U).skyscraperSheafFunctor.obj A))).obj (.mk n)),
        ((e (n + 1)).hom
          (((cochainReplacement C).1.obj
            ((sheafBotEquivalence (C := C) AddCommGrpCat.{max u v}).functor.obj
              ((GrothendieckTopology.pointBot U).skyscraperSheafFunctor.obj A))).δ i s)) x =
          ((e n).hom s) ((nerve (Under U)).δ i x)

Stacks.CategoryCohomology.cochainReplacementPointAcyclic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/CochainReplacement.lean, line 871. The attribute's comment: “point-pushforward acyclicity”.

Pushforward from a point of the chaotic site is acyclic for the cochain replacement in every positive degree.

theorem cochainReplacementPointAcyclic
    (C : Type u) [SmallCategory C] (U : C) (A : AddCommGrpCat.{max u v})
    (n : ℕ) (hn : 0 < n) :
    IsZero ((HomologicalComplex.homologyFunctor AddCommGrpCat.{max u v} (ComplexShape.up ℕ) n).obj
      ((cochainReplacementComplex C).obj
        ((sheafBotEquivalence (C := C) AddCommGrpCat.{max u v}).functor.obj
          ((GrothendieckTopology.pointBot U).skyscraperSheafFunctor.obj A))))

Stacks.CategoryCohomology.cochainReplacementPointProductAcyclic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/CochainReplacement.lean, line 965. The attribute's comment: “product acyclicity”.

A product of pushforwards from points is acyclic in positive degrees.

theorem cochainReplacementPointProductAcyclic
    (C : Type u) [SmallCategory C] (I : Type u)
    (U : I → C) (A : I → AddCommGrpCat.{max u v})
    (n : ℕ) (hn : 0 < n) :
    IsZero ((HomologicalComplex.homologyFunctor AddCommGrpCat.{max u v} (ComplexShape.up ℕ) n).obj
      ((cochainReplacementComplex C).obj
        (∏ᶜ fun i : I ↦
          (sheafBotEquivalence (C := C) AddCommGrpCat.{max u v}).functor.obj
            ((GrothendieckTopology.pointBot (U i)).skyscraperSheafFunctor.obj (A i)))))

Stacks.CategoryCohomology.presheafEmbedsInPointProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/CochainReplacement.lean, line 990. The attribute's comment: “embedding into a product of point pushforwards”.

Every abelian presheaf embeds in a product of point-pushforwards.

theorem presheafEmbedsInPointProduct
    (C : Type u) [SmallCategory C] (F : Cᵒᵖ ⥤ AddCommGrpCat.{max u v}) :
    ∃ (I : Type u) (U : I → C) (A : I → AddCommGrpCat.{max u v}),
      ∃ f : F ⟶
        (∏ᶜ fun i : I ↦
          (sheafBotEquivalence (C := C) AddCommGrpCat.{max u v}).functor.obj
            ((GrothendieckTopology.pointBot (U i)).skyscraperSheafFunctor.obj (A i))),
        Mono f

Stacks.CategoryCohomology.cochainReplacementHomologyIsoSiteCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/CochainReplacement.lean, line 1033. The attribute's comment: “right-derived global sections”.

The cohomology of the cochain replacement computes the right-derived functors of global sections on the chaotic site.

theorem cochainReplacementHomologyIsoSiteCohomology
    {C : Type u} [SmallCategory C]
    (n : ℕ) :
    Nonempty
      (cochainReplacementComplex.{u, u} C ⋙
          HomologicalComplex.homologyFunctor AddCommGrpCat.{u} (ComplexShape.up ℕ) n ≅
        (sheafBotEquivalence (C := C) AddCommGrpCat.{u}).inverse ⋙
          Stacks.Cohomology.CompositeRightDerived.siteCohomology
            (⊥ : GrothendieckTopology C) n)
Tag 08S0, an example

Tag 08S0 in the Stacks Project.

Stacks.CategoryExt.extCochainComplexBifunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/ExtCochainComplex.lean, line 340. The attribute's comment: “the cochain bifunctor”.

Stacks 08S0. The cochain complex computing homomorphisms of O-modules, as a bifunctor contravariant in the source module and covariant in the target module.

def extCochainComplexBifunctor (C : Type u) [SmallCategory C] (O : Cᵒᵖ ⥤ RingCat.{v}) :
    ((PresheafOfModules.{m} O)ᵒᵖ × PresheafOfModules.{m} O) ⥤
      CochainComplex AddCommGrpCat.{max u m} ℕ

Stacks.CategoryExt.extCochainComplex_d_apply, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/ExtCochainComplex.lean, line 368. The attribute's comment: “the alternating differential”.

The differential of K^•(G, F) is the alternating sum of the coface maps.

lemma extCochainComplex_d_apply (n : ℕ) (φ : extCochain G F n)
    (x : ComposableArrows C (n + 1)) (s : G.obj (op (x.obj (Fin.last (n + 1))))) :
    (extCochainComplex G F).d n (n + 1) φ x s =
      ∑ i : Fin (n + 2), ((-1 : ℤ) ^ (i : ℕ)) •
        (extCochainSimplexMap G F (SimplexCategory.δ i) φ x s)

Stacks.CategoryExt.extCochainComplex_d_zero_apply, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/ExtCochainComplex.lean, line 397. The attribute's comment: “the degree-zero differential”.

The degree-zero differential of K^•(G, F): on an arrow U₀ ⟶ U₁ it is ρ^{U₁}_{U₀} ∘ φ_{U₁} - φ_{U₀} ∘ ρ^{U₁}_{U₀}.

lemma extCochainComplex_d_zero_apply (φ : extCochain G F 0) (x : ComposableArrows C 1)
    (s : G.obj (op (x.obj (Fin.last 1)))) (p q : F.obj (op (x.obj 0)))
    (hp : p = F.restrictₛₗ (stringSpine x).op (φ ((nerve C).δ 0 x) s))
    (hq : q = φ ((nerve C).δ 1 x) (G.restrictₛₗ (stringSpine x).op s)) :
    (extCochainComplex G F).d 0 1 φ x s = p - q

Stacks.CategoryExt.extCochainComplex_d_one_apply, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/ExtCochainComplex.lean, line 419. The attribute's comment: “the degree-one differential”.

The degree-one differential of K^•(G, F): on a string U₀ ⟶ U₁ ⟶ U₂ it is φ_{U₀ → U₁} ∘ ρ^{U₂}_{U₁} - φ_{U₀ → U₂} + ρ^{U₁}_{U₀} ∘ φ_{U₁ → U₂}.

lemma extCochainComplex_d_one_apply (φ : extCochain G F 1) (x : ComposableArrows C 2)
    (s : G.obj (op (x.obj (Fin.last 2)))) (p q r : F.obj (op (x.obj 0)))
    (hp : p = φ ((nerve C).δ 2 x) (G.restrictₛₗ (x.map' 1 2).op s))
    (hq : q = φ ((nerve C).δ 1 x) s)
    (hr : r = F.restrictₛₗ (x.map' 0 1).op (φ ((nerve C).δ 0 x) s)) :
    (extCochainComplex G F).d 1 2 φ x s = p - q + r

Stacks.CategoryExt.extCochainComplexHomologyZeroIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/ExtCochainComplex.lean, line 592. The attribute's comment: “degree-zero cohomology”.

Stacks 08S0. The degree-zero cohomology of K^•(G, F) is the group of homomorphisms of O-modules from G to F.

def extCochainComplexHomologyZeroIso (G F : PresheafOfModules.{m} O) :
    (extCochainComplex G F).homology 0 ≅ AddCommGrpCat.of (G ⟶ F)

Stacks.CategoryExt.shortExact_extCochainComplexShortComplexRight, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/ExtCochainComplexComputesExt.lean, line 367. The attribute's comment: “exactness in the second variable”.

Exactness in the second variable: if G is projective at every object, the cochain complex carries a short exact sequence of targets to a short exact sequence of complexes.

lemma shortExact_extCochainComplexShortComplexRight
    (hG : ∀ U : C, Projective (G.obj (op U))) (hS : S.ShortExact) :
    (extCochainComplexShortComplexRight G S).ShortExact

Stacks.CategoryExt.shortExact_extCochainComplexShortComplexLeft, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/ExtCochainComplexComputesExt.lean, line 378. The attribute's comment: “exactness in the first variable, when F(U) is injective over O(V) for every arrow U ⟶ V”.

Exactness in the first variable: if the target stays injective after restriction of scalars along every arrow, the cochain complex carries a short exact sequence of sources to a short exact sequence of complexes.

lemma shortExact_extCochainComplexShortComplexLeft
    (hF : ∀ {U V : C} (f : U ⟶ V),
      Injective ((ModuleCat.restrictScalars (O.map f.op).hom).obj (F.obj (op U))))
    (hS : S.ShortExact) :
    (extCochainComplexShortComplexLeft F S).ShortExact

Stacks.CategoryExt.extAddEquivCohomology_of_objectwiseProjective, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/ExtCochainComplexComputesExt.lean, line 855. The attribute's comment: “objectwise-projective case, every degree”.

Case (1): if the first module is projective at every object, the cochain complex computes all its Ext groups: Ext^n_O(G, F) ≅ H^n(K^•(G, F)) for every n.

def extAddEquivCohomology_of_objectwiseProjective (G F : PresheafOfModules.{max u v m} O)
    (hG : ∀ U : C, Projective (G.obj (op U))) (n : ℕ) :
    Abelian.zExt G F (n : ℤ) ≃+ (extCochainComplex G F).homology n

Stacks.CategoryExt.extAddEquivCohomology_of_arrowwiseInjective, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/ExtCochainComplexComputesExt.lean, line 1123. The attribute's comment: “case (2), every degree, F(U) injective over O(V) for every arrow U ⟶ V; objectwise injectivity does not suffice, see Stacks.CategoryExt.ArrowCounterexample.injective_obj_and_not_nonempty_extAddEquiv_two”.

Case (2): if each section of the second module remains injective after restriction of scalars along every arrow, the cochain complex computes all Ext groups into it: Ext^n_O(G, F) ≅ H^n(K^•(G, F)) for every n.

Injectivity of each F(U) over O(U) alone does not suffice: Stacks.CategoryExt.ArrowCounterexample.injective_obj_and_not_nonempty_extAddEquiv_two is a counterexample in degree two.

def extAddEquivCohomology_of_arrowwiseInjective (G F : PresheafOfModules.{max u v m} O)
    (hF : ∀ {U V : C} (f : U ⟶ V),
      Injective ((ModuleCat.restrictScalars (O.map f.op).hom).obj (F.obj (op U))))
    (n : ℕ) :
    Abelian.zExt G F (n : ℤ) ≃+ (extCochainComplex G F).homology n

Stacks.CategoryExt.ArrowCounterexample.injective_obj_and_not_nonempty_extAddEquiv_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/ExtCochainComplexCounterexample.lean, line 495. The attribute's comment: “the counterexample: objectwise injectivity of F does not suffice in case (2)”.

Stacks 08S0, the counterexample to case (2) with objectwise injectivity. On the category false ⟶ true with O(true) = ℤ, O(false) = ℤ/2, the module F = target has F(true) = 0 and F(false) = ℤ/2, so each F(U) is an injective O(U)-module; yet for G = source, with G(true) = ℤ/2 and G(false) = 0, the groups Ext²_O(G, F) and H²(K^•(G, F)) are not isomorphic.

theorem injective_obj_and_not_nonempty_extAddEquiv_two :
    (∀ U : Bool, Injective (target.obj (op U))) ∧
      ¬ Nonempty (Abelian.zExt source target ((2 : ℕ) : ℤ) ≃+
        (extCochainComplex source target).homology 2)

Stacks.CategoryExt.isLimitExtCochainComplexFanOfDirectSum, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/ExtCochainComplexProducts.lean, line 212. The attribute's comment: “direct sums in the first variable become products”.

Stacks 08S0. The cochain bifunctor transforms direct sums in the first variable into products: if the cofan c exhibits its point as the direct sum of a family Gι of O-modules, then the maps which the bifunctor induces from the inclusions Gι i ⟶ c.pt exhibit K^•(c.pt, F) as the product of the complexes K^•(Gι i, F).

def isLimitExtCochainComplexFanOfDirectSum {ι : Type t} [Small.{m} ι]
    {Gι : ι → PresheafOfModules.{m} O} (c : Cofan Gι) (hc : IsColimit c)
    (F : PresheafOfModules.{m} O) :
    IsLimit (Fan.mk (f := fun i ↦ extCochainComplex (Gι i) F) (extCochainComplex c.pt F)
      (fun i ↦ (extCochainComplexBifunctor C O).map ((c.inj i).op, 𝟙 F)))

Stacks.CategoryExt.isLimitExtCochainComplexFanOfProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CategoryHomology/ExtCochainComplexProducts.lean, line 225. The attribute's comment: “products in the second variable”.

Stacks 08S0. The cochain bifunctor commutes with products in the second variable: if the fan c exhibits its point as the product of a family Fι of O-modules, then the maps which the bifunctor induces from the projections c.pt ⟶ Fι i exhibit K^•(G, c.pt) as the product of the complexes K^•(G, Fι i).

def isLimitExtCochainComplexFanOfProduct {ι : Type t} [Small.{m} ι]
    (G : PresheafOfModules.{m} O) {Fι : ι → PresheafOfModules.{m} O}
    (c : Fan Fι) (hc : IsLimit c) :
    IsLimit (Fan.mk (f := fun i ↦ extCochainComplex G (Fι i)) (extCochainComplex G c.pt)
      (fun i ↦ (extCochainComplexBifunctor C O).map (𝟙 (op G), c.proj i)))
Sources
LeanStacks.CategoryCohomology.cochainReplacement · Stacks.CategoryCohomology.cochainReplacementComplex_preservesFiniteLimits · Stacks.CategoryCohomology.cochainReplacementComplex_preservesFiniteColimits · Stacks.CategoryCohomology.cochainReplacementDeltaFunctor · Stacks.CategoryCohomology.cochainReplacementZeroHomologyIsoLimit · Stacks.CategoryCohomology.pointSimplicialReplacement_contractible · Stacks.CategoryCohomology.cochainReplacementPointIsoNerve · Stacks.CategoryCohomology.cochainReplacementPointAcyclic

Section21.43 Modules on a category#

Section 21.43 of the Stacks Project, Tag 0GYU. 13 tags here are carried by 32 declarations of the repository (all in StacksFrontier) and 4 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0GYV, a definition

Tag 0GYV in the Stacks Project.

Stacks.ModulesOnACategory.CartesianObjects.IsCartesian, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ModulesOnACategory/CartesianObjects.lean, line 160. The attribute's comment: “cartesian-object condition”.

An object of D(O) has cartesian derived sections if for every morphism U → V of C the canonical derived base-change comparison RΓ(V, K) ⊗^L_{O(V)} O(U) ⟶ RΓ(U, K) is an isomorphism.

abbrev IsCartesian (K : Stacks.ModulesOnACategory.QuasiCoherentEquivalence.DMod.{0} O) : Prop

Stacks.ModulesOnACategory.CartesianObjects.cartesianDerivedModules, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ModulesOnACategory/CartesianObjects.lean, line 166. The attribute's comment: “the full subcategory QC(O)”.

The full subcategory QC(O) ⊆ D(O) consisting of the objects with cartesian derived sections.

abbrev cartesianDerivedModules : Type _
Tag 0GYW, a lemma

Tag 0GYW in the Stacks Project.

Stacks.ModulesOnACategory.QuasiCoherentEquivalence.isQC_isClosedUnderIsomorphisms, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ModulesOnACategory/CartesianObjectsLocalizing.lean, line 330. The attribute's comment: “strictly full”.

Stacks 0GYW, strict fullness: the cartesian objects form a subcategory of D(O) closed under isomorphisms.

instance isQC_isClosedUnderIsomorphisms :
    ObjectProperty.IsClosedUnderIsomorphisms (IsQC.{w} bc)

Stacks.ModulesOnACategory.QuasiCoherentEquivalence.isQC_isSaturated, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ModulesOnACategory/CartesianObjectsLocalizing.lean, line 353. The attribute's comment: “saturated”.

Stacks 0GYW, saturation: a direct summand of a cartesian object is cartesian.

instance isQC_isSaturated : ObjectProperty.IsSaturated (IsQC.{w} bc)

Stacks.ModulesOnACategory.QuasiCoherentEquivalence.isQC_isTriangulated, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ModulesOnACategory/CartesianObjectsLocalizing.lean, line 375. The attribute's comment: “triangulated”.

Stacks 0GYW, triangulatedness: the cartesian objects form a triangulated subcategory of D(O).

instance isQC_isTriangulated : ObjectProperty.IsTriangulated (IsQC.{w} bc)

Stacks.ModulesOnACategory.QuasiCoherentEquivalence.isQC_isClosedUnderColimitsOfShape, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ModulesOnACategory/CartesianObjectsLocalizing.lean, line 397. The attribute's comment: “arbitrary direct sums”.

Stacks 0GYW, direct sums: a direct sum of cartesian objects, indexed by an arbitrary type, is cartesian.

instance isQC_isClosedUnderColimitsOfShape (J : Type j) :
    ObjectProperty.IsClosedUnderColimitsOfShape (IsQC.{w} bc) (Discrete J)

Stacks.ModulesOnACategory.CartesianSubcategory.isCartesian_isClosedUnderIsomorphisms, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ModulesOnACategory/CartesianObjectsTriangulatedSubcategory.lean, line 100. The attribute's comment: “strictly full”.

Tag 0GYW, strict fullness. The cartesian objects of D(O) are closed under isomorphism, so QC(O) is a strictly full subcategory of D(O).

instance isCartesian_isClosedUnderIsomorphisms :
    ObjectProperty.IsClosedUnderIsomorphisms (Stacks.ModulesOnACategory.CartesianObjects.IsCartesian
      O hO)

Stacks.ModulesOnACategory.CartesianSubcategory.isCartesian_isSaturated, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ModulesOnACategory/CartesianObjectsTriangulatedSubcategory.lean, line 109. The attribute's comment: “saturated”.

Tag 0GYW, saturation. The cartesian objects of D(O) are closed under direct summands, so QC(O) is a saturated (thick) subcategory of D(O).

instance isCartesian_isSaturated :
    ObjectProperty.IsSaturated (Stacks.ModulesOnACategory.CartesianObjects.IsCartesian O hO)

Stacks.ModulesOnACategory.CartesianSubcategory.isCartesian_isTriangulated, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ModulesOnACategory/CartesianObjectsTriangulatedSubcategory.lean, line 119. The attribute's comment: “triangulated”.

Tag 0GYW, triangulatedness. QC(O) is a triangulated subcategory of D(O): for each a : V ⟶ U the comparison maps are the components of a shift-compatible natural transformation between triangulated functors, - ⊗^L_{O(V)} O(U) being triangulated as a left adjoint of a triangulated functor, and the locus where such a transformation is invertible is triangulated.

instance isCartesian_isTriangulated :
    ObjectProperty.IsTriangulated (Stacks.ModulesOnACategory.CartesianObjects.IsCartesian O hO)

Stacks.ModulesOnACategory.CartesianSubcategory.isCartesian_isClosedUnderCoproducts_of_smallSite, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ModulesOnACategory/CartesianObjectsTriangulatedSubcategory.lean, line 228. The attribute's comment: “arbitrary direct sums”.

Tag 0GYW, arbitrary direct sums. QC(O) is closed under direct sums indexed by an arbitrary type. Discarding the zero summands leaves an index type small in the module universe, because D(O) is locally small there by tag 079Q, and both RΓ(V, -) ⋙ (- ⊗^L_{O(V)} O(U)) and RΓ(U, -) preserve direct sums of that size — the first as a left adjoint, the second as the derived functor of the exact evaluation. Stated for a small site, the standing smallness convention of the source.

instance isCartesian_isClosedUnderCoproducts_of_smallSite {C : Type} [SmallCategory C]
    (O : Cᵒᵖ ⥤ RingCat.{0}) (hO : ∀ (U : Cᵒᵖ) (x y : O.obj U), x * y = y * x) (J : Type j) :
    ObjectProperty.IsClosedUnderColimitsOfShape
      (Stacks.ModulesOnACategory.CartesianObjects.IsCartesian O hO) (Discrete J)
Tag 0GZQ, a lemma

Tag 0GZQ in the Stacks Project.

Stacks.ModulesOnACategory.TopCohomology.isQuasicoherentOnSite_topHomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ModulesOnACategory/QuasiCoherenceOfTopCohomology.lean, line 446.

Quasi-coherence of the top cohomology module. Let C be a category viewed as a site with the chaotic topology and let O be its sheaf of rings. If M is an object of QC(O) and b is an integer such that H^i(M) = 0 for all i > b, then H^b(M) is a quasi-coherent module on (C, O).

theorem isQuasicoherentOnSite_topHomology (hJ : J = ⊥) (bc : BaseChangeData.{w} R.obj)
    (M : DMod.{w} R.obj) (hM : IsQC.{w} bc M) (b : ℤ)
    (hvan : ∀ i : ℤ, b < i → IsZero ((DerivedCategory.homologyFunctor
      (PresheafOfModules.{max u v r w} R.obj) i).obj M)) :
    ∃ hsh : Presheaf.IsSheaf J ((DerivedCategory.homologyFunctor
        (PresheafOfModules.{max u v r w} R.obj) b).obj M).presheaf,
      (⟨_, hsh⟩ : SheafOfModules.{max u v r w} R).IsQuasicoherentOnSite
Tag 0H0R, a lemma

Tag 0H0R in the Stacks Project.

Stacks.ModulesOnACategory.QuasiCoherentEquivalence.main_equivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ModulesOnACategory/TerminalMorphismOfSitesEquivalence.lean, line 67.

Lemma 21.43.4 (tag 0H0R). The adjunction Lf^* ⊣ Rf_* along the morphism of sites f : (C, O) → (pt, O(X)) of a terminal object X exhibits Lf^* and Rf_* as mutually quasi-inverse equivalences between D(O(X)) and QC(O): the derived pullback lands in QC(O), the unit is invertible on all of D(O(X)), and the counit is invertible on every object of QC(O).

Both the base change and the derived pullback are the library's own constructions here — the canonical base-change datum, and the morphism of sites of X — so the only hypothesis is the commutativity hO of the section rings of O.

theorem main_equivalence (hO : ∀ (U : Cᵒᵖ) (x y : O.obj U), x * y = y * x) :
    (∀ P, IsQC.{w} (baseChangeDataOfComm.{r, v, u, w} O hO)
        ((morphismOfSites O hO hX).Lpullback.obj P)) ∧
    (∀ P : DerivedCategory (ModuleCat.{max u v r w} (O.obj (Opposite.op X))),
      IsIso ((morphismOfSites O hO hX).adj.unit.app P)) ∧
    (∀ K, IsQC.{w} (baseChangeDataOfComm.{r, v, u, w} O hO) K →
      IsIso ((morphismOfSites O hO hX).adj.counit.app K))
Tag 0H0S, a lemma

Tag 0H0S in the Stacks Project.

Stacks.ModulesOnACategory.MorphismsOverAnObject.homDerivedRestriction_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ModulesOnACategory/MorphismsOverAnObject.lean, line 356.

Let K be a derived module with cartesian derived sections and let M be an arbitrary derived module. Applying derived sections over the terminal object id_U of C/U and conjugating by derivedSectionsIso identifies the morphisms K|_U ⟶ M|_U in D(O_U) with the morphisms RΓ(U, K) ⟶ RΓ(U, M) in D(O(U)).

theorem homDerivedRestriction_bijective
    (hO : ∀ (V : Cᵒᵖ) (x y : O.obj V), x * y = y * x)
    (K M : DMod.{w} O)
    (hK : IsQC.{w} (baseChangeDataOfComm.{r, v, u, w} O hO) K) :
    Function.Bijective (fun f : (derivedRestriction.{w} O U).obj K ⟶
        (derivedRestriction.{w} O U).obj M =>
      ((derivedSectionsIso.{w} O U).app K).inv ≫
        (RGamma.{w} (overRingPresheaf O U)
          (Opposite.op (Over.mk (𝟙 U)))).map f ≫
        ((derivedSectionsIso.{w} O U).app M).hom)
Tag 0GYX, a lemma

Tag 0GYX in the Stacks Project.

Stacks.ModulesOnACategory.QuasiCoherentEquivalence.exists_subcomplex_containing_sections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ModulesOnACategory/SmallSubcomplexEnlargements.lean, line 123. The attribute's comment: “presheaf model”.

Stacks 0GYX in the presheaf model. There is a cardinal, depending only on the category and its presheaf of rings, such that every family of prescribed sections of a complex of O-modules is contained in a subcomplex whose number of sections is bounded by the maximum of that cardinal and the size of the family.

This is the transport of Stacks.ModulesOnACategory.exists_subcomplex_containing_sections_of_size_le across the equivalence between sheaves of modules on the chaotic site and presheaves of modules, which preserves monomorphisms and identifies the two counts of sections.

theorem exists_subcomplex_containing_sections (O : Cᵒᵖ ⥤ RingCat.{r}) :
    ∃ kappa : Cardinal.{max u v r w},
      ∀ (F : CochainComplex (PresheafOfModules.{max u v r w} O) ℤ)
        (Omega : ∀ (i : ℤ) (U : C), Set ((F.X i).obj (op U))),
        ∃ (H : CochainComplex (PresheafOfModules.{max u v r w} O) ℤ) (inclusion : H ⟶ F),
          Mono inclusion ∧
            (∀ (i : ℤ) (U : C) (x : (F.X i).obj (op U)), x ∈ Omega i U →
              ∃ y : (H.X i).obj (op U), (inclusion.f i).app (op U) y = x) ∧
            complexSectionSize.{w} O H ≤ max kappa (presheafSectionFamilySize.{w} Omega)

Stacks.ModulesOnACategory.exists_subcomplex_containing_sections_of_size_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ModulesOnACategory/SmallSubcomplexesOfSections.lean, line 476.

Stacks 0GYX. There is a cardinal, depending only on the category and its sheaf of rings, such that every family of prescribed sections of a complex is contained in a subcomplex whose size is bounded by the maximum of that cardinal and the size of the family.

theorem exists_subcomplex_containing_sections_of_size_le
    (R : Sheaf (⊥ : GrothendieckTopology C) RingCat.{r}) :
    ∃ kappa : Cardinal.{max u v m r},
      ∀ (F : CochainComplex (SheafOfModules.{m} R) ℤ)
        (Omega : ∀ (i : ℤ) (U : C), Set ((F.X i).val.obj (op U))),
        ∃ (H : CochainComplex (SheafOfModules.{m} R) ℤ) (inclusion : H ⟶ F),
          Mono inclusion ∧
            (∀ (i : ℤ) (U : C) (x : (F.X i).val.obj (op U)), x ∈ Omega i U →
              ∃ y : (H.X i).val.obj (op U), (inclusion.f i).val.app (op U) y = x) ∧
            complexSectionSize H ≤ max kappa (sectionFamilySize Omega)
Tag 0GYY, a lemma

Tag 0GYY in the Stacks Project.

Stacks.ModulesOnACategory.exists_small_quasiIso_subcomplex_presheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ModulesOnACategory/ChaoticModelTransport.lean, line 289. The attribute's comment: “presheaf model”.

There is a cardinal, depending only on the category and its sheaf of rings, such that every complex of presheaves of modules representing a derived object contains a quasi-isomorphic subcomplex bounded by that cardinal and the size of the derived object.

theorem exists_small_quasiIso_subcomplex_presheaf :
    ∃ κ : Cardinal.{max u v r w},
      ∀ (F : CochainComplex (PresheafOfModules.{max u v r w} R.obj) ℤ)
        (K : DerivedCategory (PresheafOfModules.{max u v r w} R.obj)),
        Nonempty (DerivedCategory.Q.obj F ≅ K) →
          ∃ (H : CochainComplex (PresheafOfModules.{max u v r w} R.obj) ℤ) (f : H ⟶ F),
            Mono f ∧ QuasiIso f ∧
              QuasiCoherentEquivalence.complexSectionSize.{w} R.obj H ≤
                max κ (QuasiCoherentEquivalence.derivedObjectSize.{w} R.obj K)

Stacks.ModulesOnACategory.exists_small_quasiIso_subcomplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ModulesOnACategory/SmallRepresentatives.lean, line 1232.

There is a cardinal, depending only on the category and its sheaf of rings, such that every representative of a derived object contains a quasi-isomorphic subcomplex bounded by that cardinal and the size of the derived object.

theorem exists_small_quasiIso_subcomplex :
    ∃ κ : Cardinal.{max u v m r},
      ∀ (F : CochainComplex (SheafOfModules.{m} R) ℤ)
        (K : DerivedCategory (SheafOfModules.{m} R)),
        Nonempty (DerivedCategory.Q.obj F ≅ K) →
          ∃ (H : CochainComplex (SheafOfModules.{m} R) ℤ) (f : H ⟶ F),
            Mono f ∧ QuasiIso f ∧
              complexSectionSize H ≤
                max κ (derivedObjectSize R K)
Tag 0GYZ, a lemma

Tag 0GYZ in the Stacks Project.

Stacks.ModulesOnACategory.QuasiCoherentEquivalence.exists_cardinal_small_nonzero_map_and_factorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ModulesOnACategory/CartesianEnlargementExists.lean, line 269. The attribute's comment: “both conclusions, at one cardinal, for a presheaf of commutative rings”.

Stacks 0GYZ. Let C be a category, regarded as a site with the chaotic topology, and let O be a presheaf of commutative rings on C. There is a cardinal κ such that

  1. every nonzero object K of QC(O) receives a nonzero morphism from an object of QC(O) of size at most κ, and
  2. every morphism α : E ⟶ ⨁_n K_n of QC(O) with |E| ≤ κ factors through a morphism ⨁_n E_n ⟶ ⨁_n K_n induced by morphisms E_n ⟶ K_n of QC(O) with |E_n| ≤ κ.

Conclusion (1) is exists_nonzero_map_of_size_le_of_cartesianEnlargement fed with exists_hasCartesianEnlargement. Conclusion (2) comes from its analogue for D(O), exists_factorization_of_sum_of_derivedObjectSize_le, by replacing each of the summands it produces with a cartesian object of the same size bound, which is exists_small_cartesian_factorization.

theorem exists_cardinal_small_nonzero_map_and_factorization (bc : BaseChangeData.{w} O)
    (hO : ∀ (V : Cᵒᵖ) (x y : O.obj V), x * y = y * x) :
    ∃ κ : Cardinal.{max u v r w},
      (∀ K : QC.{w} bc, ¬ IsZero K.obj →
          ∃ (E : QC.{w} bc) (f : E ⟶ K), f ≠ 0 ∧ derivedObjectSize.{w} O E.obj ≤ κ) ∧
        (∀ (E : QC.{w} bc) (K : ℕ → QC.{w} bc) (α : E.obj ⟶ ∐ fun n => (K n).obj),
          derivedObjectSize.{w} O E.obj ≤ κ →
          ∃ (E' : ℕ → QC.{w} bc) (f : ∀ n, E' n ⟶ K n)
            (β : E.obj ⟶ ∐ fun n => (E' n).obj),
            (∀ n, derivedObjectSize.{w} O (E' n).obj ≤ κ) ∧
              α = β ≫ Limits.Sigma.map fun n => (QCι.{w} bc).map (f n))

Stacks.ModulesOnACategory.QuasiCoherentEquivalence.exists_factorization_of_sum_of_derivedObjectSize_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ModulesOnACategory/SmallFactorizationThroughSums.lean, line 429. The attribute's comment: “part (2) for D(O) in place of QC(O): cartesianness dropped from the source and from the summands”.

Conclusion (2) of Stacks 0GYZ with the cartesianness demand dropped. There is a cardinal κ₀, depending only on the category and its presheaf of rings, such that for every cardinal κ above it, every morphism from an object of D(O) of size at most κ into a countable direct sum factors through a direct sum of objects of size at most κ mapping to the summands.

The conclusion is stated at every κ ≥ κ₀ rather than at κ₀ alone — which is the source's form, recovered by taking κ = κ₀ — because the hypothesis and the conclusion both read ≤ κ, so the property is monotone in neither direction and the form at a single cardinal cannot be combined with conclusion (1) at one cardinal, as Stacks 0GYZ asserts it is.

theorem exists_factorization_of_sum_of_derivedObjectSize_le :
    ∃ κ₀ : Cardinal.{max u v r w}, ∀ κ : Cardinal.{max u v r w}, κ₀ ≤ κ →
      ∀ (E : DMod.{w} O) (K : ℕ → DMod.{w} O) (α : E ⟶ ∐ K),
        derivedObjectSize.{w} O E ≤ κ →
        ∃ (E' : ℕ → DMod.{w} O) (f : ∀ n, E' n ⟶ K n) (β : E ⟶ ∐ E'),
          (∀ n, derivedObjectSize.{w} O (E' n) ≤ κ) ∧ α = β ≫ Limits.Sigma.map f

Stacks.ModulesOnACategory.QuasiCoherentEquivalence.exists_nonzero_map_of_derivedObjectSize_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ModulesOnACategory/SmallNonzeroMaps.lean, line 330. The attribute's comment: “part (1) for D(O) in place of QC(O): cartesianness dropped from both objects”.

Every nonzero object of D(O) receives a nonzero morphism from an object of size at most singleGeneratorBound O. This is the detection step of conclusion (1) of Stacks 0GYZ with the cartesianness demand dropped from both objects: the subcomplex produced by exists_small_subcomplex_detecting_nonzero is used as the source as it stands, with no enlargement.

theorem exists_nonzero_map_of_derivedObjectSize_le (K : DMod.{w} O) (hK : ¬ IsZero K) :
    ∃ (E : DMod.{w} O) (f : E ⟶ K),
      f ≠ 0 ∧ derivedObjectSize.{w} O E ≤ singleGeneratorBound.{w} O
Tag 0GZ0, a proposition

Tag 0GZ0 in the Stacks Project.

AlgebraicGeometry.exists_isTriangulated_rightAdjoint_smallAffineChaoticDerivedQuasiCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/AffineSiteBrownRepresentability.lean, line 132. The attribute's comment: “part (3) on D_QCoh(S_affine, 𝒪) of an arbitrary scheme, through the equality of that subcategory with QC(S_affine, 𝒪) which is the comparison (4) ≃ (5) of Stacks 0GZZ”.

[Stacks, Tag 0GZ0] part (3) on D_QCoh(S_affine, 𝒪). Let S be a scheme and let (S_affine, 𝒪) be its small affine Zariski site read with the chaotic topology. An exact functor F : D_QCoh(S_affine, 𝒪) ⥤ D' of triangulated categories which transforms direct sums into direct sums has a right adjoint G, which is again exact: the adjunction F ⊣ G is a triangulated adjunction for a Functor.CommShift ℤ structure on G.

No hypothesis is carried: no compact generation, and no quasi-compactness or quasi-separatedness. The two inputs are [Stacks, Tag 0GZ0] part (3) for the cartesian objects, which is Brown representability without compact generation, and the identification of D_QCoh(S_affine, 𝒪) with QC(S_affine, 𝒪), which is the comparison (4) ≃ (5) of [Stacks, Tag 0GZZ] in the sharp form AlgebraicGeometry.smallAffineChaotic_isQC_eq_hasQuasicoherentCohomology: on the chaotic site the two subcategories of D(S_affine, 𝒪) are equal, not merely equivalent.

This is the abstract input of the Stacks proof of [Stacks, Tag 0A9E], but on the affine site; nothing here is a statement about D_QCoh(𝒪_S), and Tag 0A9E does not follow. See the coverage note of this file.

theorem exists_isTriangulated_rightAdjoint_smallAffineChaoticDerivedQuasiCoherent
    {D' : Type u'} [Category.{max (u + 1) w} D'] [HasZeroObject D'] [Preadditive D']
    [HasShift D' ℤ] [∀ n : ℤ, (shiftFunctor D' n).Additive] [Pretriangulated D']
    (F : (qcohCohomologyProperty.{w} (smallAffineChaoticRingedSite B S hS)).FullSubcategory ⥤ D')
    [F.CommShift ℤ] [F.IsTriangulated]
    [∀ α : Type (max (u + 1) w), PreservesColimitsOfShape (Discrete α) F] :
    ∃ (G : D' ⥤
        (qcohCohomologyProperty.{w} (smallAffineChaoticRingedSite B S hS)).FullSubcategory)
      (adj : F ⊣ G) (_ : G.CommShift ℤ), adj.IsTriangulated

Stacks.ModulesOnACategory.QuasiCoherentEquivalence.exists_iso_preadditiveYoneda_of_isHomological_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ModulesOnACategory/BrownRepresentabilityUnconditional.lean, line 129. The attribute's comment: “part (2), for a presheaf of commutative rings”.

[Stacks, Tag 0GZ0] part (2). Let C be a category with the chaotic topology, let O be a presheaf of commutative rings on C and let bc be derived base-change data for O. Every contravariant cohomological functor on QC(O) which transforms direct sums into products is representable.

This is weak Brown representability [Stacks, Tag 0GYG] applied to the generating family Stacks.ModulesOnACategory.QuasiCoherentEquivalence.exists_small_generating_family, which is [Stacks, Tag 0GYZ].

theorem exists_iso_preadditiveYoneda_of_isHomological_unconditional
    (hO : ∀ (V : Cᵒᵖ) (x y : O.obj V), x * y = y * x)
    (H : (QC.{w} bc)ᵒᵖ ⥤ AddCommGrpCat.{max u v r w}) [H.IsHomological]
    [∀ J : Type (max u v r w), PreservesLimitsOfShape (Discrete J) H] :
    ∃ K : QC.{w} bc, Nonempty (preadditiveYoneda.obj K ≅ H)

Stacks.ModulesOnACategory.QuasiCoherentEquivalence.exists_isTriangulated_rightAdjoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ModulesOnACategory/BrownRepresentabilityUnconditional.lean, line 148. The attribute's comment: “part (3), for a presheaf of commutative rings”.

[Stacks, Tag 0GZ0] part (3). Let C be a category with the chaotic topology, let O be a presheaf of commutative rings on C and let bc be derived base-change data for O. An exact functor F : QC(O) ⥤ D' of triangulated categories which transforms direct sums into direct sums has a right adjoint G, which is again exact: the adjunction F ⊣ G is a triangulated adjunction for a Functor.CommShift ℤ structure on G.

This is Brown representability in the form [Stacks, Tag 0GYH] applied to the generating family Stacks.ModulesOnACategory.QuasiCoherentEquivalence.exists_small_generating_family, which is [Stacks, Tag 0GYZ].

theorem exists_isTriangulated_rightAdjoint
    (hO : ∀ (V : Cᵒᵖ) (x y : O.obj V), x * y = y * x)
    {D' : Type u'} [Category.{max u v r w} D'] [HasZeroObject D'] [Preadditive D']
    [HasShift D' ℤ] [∀ n : ℤ, (shiftFunctor D' n).Additive] [Pretriangulated D']
    (F : QC.{w} bc ⥤ D') [F.CommShift ℤ] [F.IsTriangulated]
    [∀ α : Type (max u v r w), PreservesColimitsOfShape (Discrete α) F] :
    ∃ (G : D' ⥤ QC.{w} bc) (adj : F ⊣ G) (_ : G.CommShift ℤ), adj.IsTriangulated

Stacks.ModulesOnACategory.QuasiCoherentEquivalence.exists_isTriangulated_rightAdjoint_QCι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ModulesOnACategory/BrownRepresentabilityUnconditional.lean, line 166. The attribute's comment: “part (4), for a presheaf of commutative rings”.

[Stacks, Tag 0GZ0] part (4). The inclusion QC(O) ⥤ D(O) of the cartesian objects has an exact right adjoint. The inclusion is exact and transforms direct sums into direct sums, because QC(O) is a triangulated subcategory closed under direct sums ([Stacks, Tag 0GYW]), so this is the special case F = QCι of Stacks.ModulesOnACategory.QuasiCoherentEquivalence.exists_isTriangulated_rightAdjoint.

theorem exists_isTriangulated_rightAdjoint_QCι
    (hO : ∀ (V : Cᵒᵖ) (x y : O.obj V), x * y = y * x) :
    ∃ (G : DMod.{w} O ⥤ QC.{w} bc) (adj : QCι.{w} bc ⊣ G) (_ : G.CommShift ℤ),
      adj.IsTriangulated

Stacks.ModulesOnACategory.QuasiCoherentEquivalence.exists_iso_preadditiveYoneda_of_isHomological, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ModulesOnACategory/CartesianBrownRepresentability.lean, line 201. The attribute's comment: “part (2); part (1) is on the covering set of 0GYW, parts (3) and (4) below”.

Stacks 0GZ0, assertion (2). Let C be a category, regarded as a site with the chaotic topology, and let O be a presheaf of commutative rings on C. Every contravariant cohomological functor on QC(O) which transforms direct sums into products is representable.

This is weak Brown representability (Stacks 0GYG) applied to the generating family of exists_qc_generating_family, which is Stacks 0GYZ.

theorem exists_iso_preadditiveYoneda_of_isHomological (bc : BaseChangeData.{w} O)
    (hO : ∀ (V : Cᵒᵖ) (x y : O.obj V), x * y = y * x)
    (H : (QC.{w} bc)ᵒᵖ ⥤ AddCommGrpCat.{max u v r w}) [H.IsHomological]
    [∀ J : Type (max u v r w), PreservesLimitsOfShape (Discrete J) H] :
    ∃ K : QC.{w} bc, Nonempty (preadditiveYoneda.obj K ≅ H)

Stacks.ModulesOnACategory.QuasiCoherentEquivalence.exists_isTriangulated_rightAdjoint_of_preservesCoproducts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ModulesOnACategory/CartesianBrownRepresentability.lean, line 227. The attribute's comment: “part (3); part (1) is on the covering set of 0GYW, part (2) above, part (4) below”.

Stacks 0GZ0, assertion (3). Let C be a category, regarded as a site with the chaotic topology, and let O be a presheaf of commutative rings on C. Every exact functor F : QC(O) ⥤ D of triangulated categories which transforms direct sums into direct sums has a right adjoint G, and G is again exact: the adjunction F ⊣ G is triangulated for a (unique) Functor.CommShift ℤ structure on G.

This is Stacks 0GYH applied to the generating family of exists_qc_generating_family, which is Stacks 0GYZ.

theorem exists_isTriangulated_rightAdjoint_of_preservesCoproducts (bc : BaseChangeData.{w} O)
    (hO : ∀ (V : Cᵒᵖ) (x y : O.obj V), x * y = y * x)
    (F : QC.{w} bc ⥤ D) [F.CommShift ℤ] [F.IsTriangulated]
    [∀ α : Type (max u v r w), PreservesColimitsOfShape (Discrete α) F] :
    ∃ (G : D ⥤ QC.{w} bc) (adj : F ⊣ G) (_ : G.CommShift ℤ), adj.IsTriangulated

Stacks.ModulesOnACategory.QuasiCoherentEquivalence.exists_isTriangulated_rightAdjoint_qcι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ModulesOnACategory/CartesianBrownRepresentability.lean, line 246. The attribute's comment: “part (4); part (1) is on the covering set of 0GYW, parts (2) and (3) above”.

Stacks 0GZ0, assertion (4). Let C be a category, regarded as a site with the chaotic topology, and let O be a presheaf of commutative rings on C. The inclusion QC(O) ⥤ D(O) has an exact right adjoint.

This is assertion (3) at the inclusion functor: the inclusion is exact and transforms direct sums into direct sums, QC(O) being a triangulated subcategory of D(O) closed under arbitrary direct sums (Stacks 0GYW), so that the inclusion creates them.

theorem exists_isTriangulated_rightAdjoint_qcι (bc : BaseChangeData.{w} O)
    (hO : ∀ (V : Cᵒᵖ) (x y : O.obj V), x * y = y * x) :
    ∃ (G : DMod.{w} O ⥤ QC.{w} bc) (adj : QCι.{w} bc ⊣ G) (_ : G.CommShift ℤ),
      adj.IsTriangulated

Declarations registered for the tag:

Tag 0GZ1, a lemma

Tag 0GZ1 in the Stacks Project.

Stacks.ModulesOnACategory.PullbackPreservesQuasiCoherent.isQC_derivedPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ModulesOnACategory/DerivedPullbackOfModules/RestrictionMaps.lean, line 705. The attribute's comment: “Lg^* carries QC(O) into QC(O'), for the derived pullback constructed here”.

Derived pullback along a morphism of ringed topoi on chaotic sites carries cartesian objects to cartesian objects. If the derived sections of K are cartesian then so are the derived sections of Lg^*K, the cartesian condition on either side being taken with respect to the derived base changes along the restriction homomorphisms of the structure sheaf there.

theorem isQC_derivedPullback (K : DMod.{max u' v'} O)
    (hK : IsQC.{max u' v'}
      (PullbackQuasiCoherentBaseChange.baseChangeDataOfComm.{r, v, u, max u' v'} O hO) K) :
    IsQC.{max u v}
      (PullbackQuasiCoherentBaseChange.baseChangeDataOfComm.{r, v', u', max u v} O' hO')
      ((derivedPullback F O O' φ).obj K)

Stacks.ModulesOnACategory.PullbackQuasiCoherentBaseChange.isQC_Lpullback_of_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ModulesOnACategory/PullbackQuasiCoherentBaseChange.lean, line 213. The attribute's comment: “pullback of cartesian objects, for a derived pullback with its sections”.

Stacks 0GZ1. Derived pullback along a morphism of ringed topoi carries cartesian objects to cartesian objects. If the derived sections of K are cartesian then so are the derived sections of Lg^*K, the cartesian condition on either side being taken with respect to the derived base changes along the restriction homomorphisms of the structure sheaf there.

The derived pullback is supplied as data, together with the computation of its derived sections of Stacks 0D6D, in the same way that Stacks.ModulesOnACategory.QuasiCoherentEquivalence.MorphismOfSites supplies it for the statements of Stacks 0H0R and 0H0S.

theorem isQC_Lpullback_of_comm
    (d : DerivedPullbackData (structureBaseChange F O O' φ hO hO')
      (baseChangeDataOfComm.{r, v, u, max u' v'} O hO)
      (baseChangeDataOfComm.{r, v', u', max u v} O' hO'))
    (K : DMod.{max u' v'} O)
    (hK : IsQC.{max u' v'} (baseChangeDataOfComm.{r, v, u, max u' v'} O hO) K) :
    IsQC.{max u v} (baseChangeDataOfComm.{r, v', u', max u v} O' hO') (d.Lpullback.obj K)
Tag 0GZR, a lemma

Tag 0GZR in the Stacks Project.

Stacks.ModulesOnACategory.QuasiCoherentCohomology.isQC_iff_hasQuasicoherentCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ModulesOnACategory/QuasiCoherentCohomologyUnderFlatRestrictions.lean, line 301.

Quasi-coherent cohomology under flat restrictions. Let C be a category viewed as a site with the chaotic topology, let O be its sheaf of rings, and assume that for every morphism U → V of C the restriction homomorphism O(V) → O(U) is flat. Then an object of D(O) lies in QC(O) exactly when all of its cohomology sheaves are quasi-coherent, that is, QC(O) = D_QCoh(O).

theorem isQC_iff_hasQuasicoherentCohomology (X : RingedSite.{u, v, r}) (hX : X.J = ⊥)
    (hflat : ∀ {U V : X.Cᵒᵖ} (a : V ⟶ U), RingHom.Flat (X.O.obj.map a).hom)
    (bc : BaseChangeData.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O).obj)
    (K : DMod.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O).obj) :
    IsQC.{w} bc K ↔ hasQuasicoherentCohomology.{w} X K
Tag 0GZS, a lemma

Tag 0GZS in the Stacks Project.

Stacks.ModulesOnACategory.ChaoticComparison.cartesianEquivalenceOfLocallyKFlatAcyclic, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ModulesOnACategory/ChaoticComparisonUnitSquare.lean, line 425.

Let C carry a Grothendieck topology τ, let τ' be the chaotic topology on C and let O be a τ-sheaf of rings with commuting sections. Assume hypothesis (2) of the source: for every object U of C and every K-flat complex M^• of O(U)-modules the canonical map M^• ⟶ RΓ((C/U)_τ, (M^• ⊗_{O(U)} O_U)^#) is a quasi-isomorphism. Then ε^* and Rε_* are mutually quasi-inverse equivalences between QC(O) and the full subcategory of D(C_τ, O_τ) consisting of the objects K with Rε_*K in QC(O).

Hypothesis (1) of the source, that τ' is the chaotic topology, is structural here: a module on (C_τ', O_τ') is a presheaf of O-modules, ε_* is the forgetful functor and ε^* is τ-sheafification. Hypothesis (2) is IsLocallyKFlatAcyclic, read on the localized site (C/U, τ). The commutativity hO gives the canonical base-change datum Stacks.ModulesOnACategory.PullbackQuasiCoherentBaseChange.baseChangeDataOfComm; the cartesian condition does not depend on the choice of datum.

The objects and the morphisms of C and the section rings lie in independent universes u, v and r, and the modules in max u v r w; the site therefore need not be small, as is the case for the associated affine site of a category fibred in groupoids (Stacks 0H0J).

def cartesianEquivalenceOfLocallyKFlatAcyclic (h2 : IsLocallyKFlatAcyclic.{w} R hO) :
    (IsCartesianPushforward.{w} R
          (baseChangeDataOfComm.{r, v, u, w} R.obj hO)).FullSubcategory ≌
      QC.{w} (baseChangeDataOfComm.{r, v, u, w} R.obj hO)
Tag 0H0T, a lemma

Tag 0H0T in the Stacks Project.

Stacks.ModulesOnACategory.ChaoticComparison.homEpsilonPullback_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ModulesOnACategory/ChaoticComparisonOnCartesianObjects.lean, line 197. The attribute's comment: “morphisms out of a sheafified cartesian object are maps of derived sections over U”.

Let K be an object of QC(O) and let M be an arbitrary object of D((O_U)_τ). Transposing under the adjunction ε^* ⊣ Rε_* over C/U and then taking derived sections over the terminal object id_U of C/U identifies the morphisms ε^*(K|_U) ⟶ M of D((O_U)_τ) with the morphisms RΓ(U, K) ⟶ RΓ(U, Rε_*M) of D(O(U)).

theorem homEpsilonPullback_bijective
    (hO : ∀ (V : Cᵒᵖ) (x y : R.obj.obj V), x * y = y * x)
    (K : DMod.{w} R.obj)
    (hK : IsQC.{w} (baseChangeDataOfComm.{r, v, u, w} R.obj hO) K)
    (M : DerivedCategory (SheafOfModules.{max u v r w} (overRingSheaf R U))) :
    Function.Bijective (fun f : (epsilonPullback.{w} (overRingSheaf R U)).mapDerivedCategory.obj
        ((derivedRestriction.{w} R.obj U).obj K) ⟶ M =>
      ((derivedSectionsIso.{w} R.obj U).app K).inv ≫
        (RGamma.{w} (overRingPresheaf R.obj U) (Opposite.op (Over.mk (𝟙 U)))).map
          ((derivedEpsilonAdjunction.{w} (overRingSheaf R U)).unit.app
              ((derivedRestriction.{w} R.obj U).obj K) ≫
            (derivedEpsilonPushforward.{w} (overRingSheaf R U)).map f))
Sources
LeanStacks.ModulesOnACategory.CartesianObjects.IsCartesian · Stacks.ModulesOnACategory.CartesianObjects.cartesianDerivedModules · Stacks.ModulesOnACategory.QuasiCoherentEquivalence.isQC_isClosedUnderIsomorphisms · Stacks.ModulesOnACategory.QuasiCoherentEquivalence.isQC_isSaturated · Stacks.ModulesOnACategory.QuasiCoherentEquivalence.isQC_isTriangulated · Stacks.ModulesOnACategory.QuasiCoherentEquivalence.isQC_isClosedUnderColimitsOfShape · Stacks.ModulesOnACategory.CartesianSubcategory.isCartesian_isClosedUnderIsomorphisms · Stacks.ModulesOnACategory.CartesianSubcategory.isCartesian_isSaturated

Section21.44 Strictly perfect complexes#

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

Tag 08FL, a definition

Tag 08FL in the Stacks Project.

Declarations registered for the tag:

Tag 08FM, a lemma

Tag 08FM in the Stacks Project.

mappingCone_isStrictlyPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/StrictlyPerfect/ConeOfAMorphism.lean, line 230.

Statement 1 (Stacks Tag 08FM). Let (C, O) be a ringed site, and let f : A ⟶ B be a morphism of complexes of O-modules. If A and B are both strictly perfect (Definition 2), then the cone C(f) = CochainComplex.mappingCone f (Definition 4) is strictly perfect.

Proof sketch (Tag 08FM, "immediate from the definitions"): * Boundedness. By CochainComplex.mappingCone.isZero_X_iff, IsZero ((mappingCone f).X i) ↔ IsZero (A.X (i+1)) ∧ IsZero (B.X i), so {i | ¬ IsZero ((mappingCone f).X i)} ⊆ {i | ¬ IsZero (A.X (i+1))} ∪ {i | ¬ IsZero (B.X i)}. The second set is hB.bounded; the first is the preimage of hA.bounded under i ↦ i+1, hence finite. A finite union of finite sets is finite. * Term condition. Fix i. We have (mappingCone f).X i ≅ A.X (i+1) ⊞ B.X i via HomologicalComplex.homotopyCofiber.XIsoBiprod f i (i+1) rfl (mappingCone f is definitionally homotopyCofiber f, and for CochainComplex … ℤ the relation c.Rel i j is i+1 = j). By Helper 2, A.X (i+1) ⊞ B.X i is a direct summand of a finite free module (since A.X (i+1) and B.X i are, by hA.termDirectSummand, hB.termDirectSummand); by Helper 1 (transport along that iso) so is (mappingCone f).X i.

theorem mappingCone_isStrictlyPerfect
    {A B : CochainComplex (SheafOfModules.{m} R) ℤ} (f : A ⟶ B)
    [HomologicalComplex.HasHomotopyCofiber f]
    (hA : IsStrictlyPerfect R A) (hB : IsStrictlyPerfect R B) :
    IsStrictlyPerfect R (CochainComplex.mappingCone f)
Tag 09J8, a lemma

Tag 09J8 in the Stacks Project.

Stacks.StrictlyPerfect.Modules.isStrictlyPerfect_tensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/StrictlyPerfect/DirectSummandsOfFiniteFree.lean, line 218.

If E and F are strictly perfect complexes of R-modules, then so is their tensor product E ⊗ F, the total complex of the tensor product double complex.

theorem isStrictlyPerfect_tensor
    (E F : CochainComplex (ModuleCat R) ℤ)
    (hE : IsStrictlyPerfect E) (hF : IsStrictlyPerfect F) :
    IsStrictlyPerfect (E ⊗ F)

Stacks.SheafOfModules.Tensor.isStrictlyPerfect_tensorComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/StrictlyPerfect/TensorOfStrictlyPerfectComplexes.lean, line 399.

Stacks 09J8. The total tensor complex Tot(K ⊗_O L) of two strictly perfect complexes of O-modules on a ringed site is strictly perfect.

Each degree of Tot(K ⊗_O L) is the coproduct of the K^t ⊗_O L^r with t + r that degree. Such a summand vanishes unless both K^t and L^r are nonzero, which happens for finitely many pairs only, so the degree vanishes outside the sum of the two ranges of nonvanishing; and each surviving summand is a direct summand of a finite free O-module because both of its factors are.

theorem isStrictlyPerfect_tensorComplex
    (K L : CochainComplex (SheafOfModules.{w} (ringSheaf R)) ℤ)
    (hK : IsStrictlyPerfect (ringSheaf R) K) (hL : IsStrictlyPerfect (ringSheaf R) L) :
    IsStrictlyPerfect (ringSheaf R) (((tensorComplex R).obj K).obj L)
Tag 08H3, a lemma

Tag 08H3 in the Stacks Project.

AlgebraicGeometry.RingedToposHom.isStrictlyPerfect_pullbackModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/StrictlyPerfect/PullbackAlongAMorphismOfRingedTopoi.lean, line 53.

Let f : (C, O_C) → (D, O_D) be a morphism of ringed topoi. If E is a strictly perfect complex of O_D-modules, then f^*E, the degreewise pullback, is a strictly perfect complex of O_C-modules.

theorem isStrictlyPerfect_pullbackModules (f : RingedToposHom X Y)
    {E : CochainComplex (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) ℤ}
    (hE : IsStrictlyPerfect (Stacks.SheafOfModules.Tensor.ringSheaf Y.O) E) :
    IsStrictlyPerfect (Stacks.SheafOfModules.Tensor.ringSheaf X.O)
      (((f.toModulesHom.pullbackModules).mapHomologicalComplex (ComplexShape.up ℤ)).obj E)

Stacks.Sheaves.StrictlyPerfectPullback.pullbackModules_preservesZeroMorphisms, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/StrictlyPerfect/ToposPullback.lean, line 133. The attribute's comment: “additivity of pullback”.

Stacks 08H3, the additivity clause. Pullback of sheaves of modules along a morphism of ringed topoi preserves zero morphisms, being a left adjoint. This is what lets the functor be applied degreewise to a complex.

theorem pullbackModules_preservesZeroMorphisms :
    (f.pullbackModules).PreservesZeroMorphisms

Stacks.Sheaves.StrictlyPerfectPullback.isStrictlyPerfect_pullbackModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/StrictlyPerfect/ToposPullback.lean, line 142. The attribute's comment: “strict perfectness of the pullback complex”.

Stacks 08H3, the strict-perfectness clause. The degreewise pullback of a strictly perfect complex of O_Y-modules along a morphism of ringed topoi is a strictly perfect complex of O_X-modules.

theorem isStrictlyPerfect_pullbackModules
    (E : CochainComplex (SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) ℤ)
    (hE : IsStrictlyPerfect (Stacks.SheafOfModules.Tensor.ringSheaf Y.O) E) :
    letI := pullbackModules_preservesZeroMorphisms f
    IsStrictlyPerfect (Stacks.SheafOfModules.Tensor.ringSheaf X.O)
      (((f.pullbackModules).mapHomologicalComplex (ComplexShape.up ℤ)).obj E)
Tag 08FN, a lemma

Tag 08FN in the Stacks Project.

AlgebraicGeometry.RingedSite.exists_coveringSieve_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/StrictlyPerfect/LocalLiftingThroughEpimorphisms.lean, line 277.

Stacks 08FN. Let (C, O) be a ringed site, U an object of C, and let p : G ⟶ F be an epimorphism of O|_U-modules. A map e : E ⟶ F whose source is a direct summand of a finite free O|_U-module lifts through p locally on U: there is a covering sieve S of U such that for every f : V ⟶ U in S the restriction of e to C/V factors through the restriction of p.

The lift is produced one coordinate at a time. Writing E as a retract of O|_U^{⊕n} by j : E ⟶ O|_U^{⊕n} and r : O|_U^{⊕n} ⟶ E with j ≫ r = 𝟙, the composite q = r ≫ e is determined by n global sections of F over U. Each of them lifts through p on a covering sieve, since p is locally surjective; the intersection of those n sieves is still covering, and over it the chosen lifts assemble, by the universal property of the free module, into a map O|_U^{⊕n}|_V ⟶ G|_V over p. Precomposing with j|_V gives the lift of e.

theorem exists_coveringSieve_lift (X : RingedSite.{u, t, 0}) (U : X.C)
    [HasWeakSheafify (X.J.over U) AddCommGrpCat.{0}]
    [(X.J.over U).WEqualsLocallyBijective AddCommGrpCat.{0}]
    (E F G : SheafOfModules.{0} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U))
    (e : E ⟶ F) (p : G ⟶ F) [Epi p]
    (hE : IsDirectSummandOfFiniteFree ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U) E) :
    ∃ S : Sieve U, (S ∈ X.J U) ∧
      (∀ {V : X.C} (f : V ⟶ U), S f →
        ∃ l : E.over (Over.mk f) ⟶ G.over (Over.mk f),
          l ≫ p.over (Over.mk f) = e.over (Over.mk f))
Tag 08FP, a lemma

Tag 08FP in the Stacks Project.

AlgebraicGeometry.RingedSite.exists_coveringSieve_homotopy_zero_of_acyclic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/StrictlyPerfect/LocalNullHomotopy.lean, line 643. The attribute's comment: “part (1)”. References: SGA 6 I (4.1).

Stacks 08FP (1). A map from a strictly perfect complex of O|_U-modules to an acyclic complex is null-homotopic after restriction along every arrow of a covering sieve of U.

theorem exists_coveringSieve_homotopy_zero_of_acyclic
    (hE : IsStrictlyPerfect ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U) E)
    (hF : F.Acyclic) :
    ∃ S : Sieve U, S ∈ X.J U ∧
      ∀ {V : X.C} (f : V ⟶ U), S f →
        Nonempty (Homotopy
          (((SheafOfModules.overFunctor ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U)
            (Over.mk f)).mapHomologicalComplex
            (ComplexShape.up ℤ)).map α) 0)

AlgebraicGeometry.RingedSite.exists_coveringSieve_homotopy_zero_of_isZero_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/StrictlyPerfect/LocalNullHomotopy.lean, line 658. The attribute's comment: “part (2)”. References: SGA 6 I (4.1).

Stacks 08FP (2). A map from a strictly perfect complex of O|_U-modules supported in degrees ≥ a is null-homotopic after restriction along every arrow of a covering sieve of U, provided the target has vanishing cohomology in those degrees.

theorem exists_coveringSieve_homotopy_zero_of_isZero_homology (a : ℤ)
    (hE : IsStrictlyPerfect ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U) E)
    (hE₀ : ∀ i : ℤ, i < a → IsZero (E.X i))
    (hF : ∀ i : ℤ, a ≤ i → IsZero (F.homology i)) :
    ∃ S : Sieve U, S ∈ X.J U ∧
      ∀ {V : X.C} (f : V ⟶ U), S f →
        Nonempty (Homotopy
          (((SheafOfModules.overFunctor ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U)
            (Over.mk f)).mapHomologicalComplex
            (ComplexShape.up ℤ)).map α) 0)
Tag 08FQ, a lemma

Tag 08FQ in the Stacks Project.

AlgebraicGeometry.RingedSite.exists_coveringSieve_lift_homotopy, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/StrictlyPerfect/LocalLiftingThroughCohomologyIsomorphisms.lean, line 199. References: SGA 6 I (4.2).

Stacks 08FQ. Let (C, O) be a ringed site and U an object of C. Given a solid diagram of complexes of O|_U-modules 

E --α--> F
     ↗
    G
with E strictly perfect, Eʲ = 0 for j < a, Hʲ(f) an isomorphism for j > a and an epimorphism for j = a, there is a covering sieve of U such that over each of its arrows a dotted arrow exists making the diagram commute up to homotopy.

theorem exists_coveringSieve_lift_homotopy (α : E ⟶ F) (f : G ⟶ F) (a : ℤ)
    (hE : IsStrictlyPerfect ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U) E)
    (hEa : ∀ j : ℤ, j < a → IsZero (E.X j))
    (hf_gt : ∀ j : ℤ, a < j → IsIso (HomologicalComplex.homologyMap f j))
    (hf_a : Epi (HomologicalComplex.homologyMap f a)) :
    ∃ S : Sieve U, S ∈ X.J U ∧
      ∀ {V : X.C} (g : V ⟶ U), S g →
        ∃ β : ((SheafOfModules.overFunctor ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U)
              (Over.mk g)).mapHomologicalComplex (ComplexShape.up ℤ)).obj E ⟶
          ((SheafOfModules.overFunctor ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U)
              (Over.mk g)).mapHomologicalComplex (ComplexShape.up ℤ)).obj G,
          Nonempty (Homotopy
            (β ≫ ((SheafOfModules.overFunctor ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U)
              (Over.mk g)).mapHomologicalComplex (ComplexShape.up ℤ)).map f)
            (((SheafOfModules.overFunctor ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U)
              (Over.mk g)).mapHomologicalComplex (ComplexShape.up ℤ)).map α))
Tag 08FR, a lemma

Tag 08FR in the Stacks Project.

AlgebraicGeometry.RingedSite.exists_coveringSieve_homotopy_zero_of_derived_zero_overMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/StrictlyPerfect/LocalComplexMapOfARetraction.lean, line 117. The attribute's comment: “local_null_homotopy, along an arrow of the site”.

Stacks 08FR (2), with the restriction to the slice over an arrow V ⟶ U of the covering sieve expressed by SheafOfModules.overMap rather than by restriction to an iterated slice.

This is the same statement as AlgebraicGeometry.RingedSite.exists_coveringSieve_homotopy_zero_of_derived_zero_general, in the presentation of the restriction that Stacks 08FR (1) and pseudo-coherence use. The general form of 08FR (2) is the one read here, the module sections living in the ring universe w.

theorem exists_coveringSieve_homotopy_zero_of_derived_zero_overMap
    {E F : CochainComplex
      (SheafOfModules.{w} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U)) ℤ}
    (hE : IsStrictlyPerfect ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U) E) (α : E ⟶ F)
    (hα : DerivedCategory.Q.map α = 0) :
    ∃ S : Sieve U, S ∈ X.J U ∧ ∀ ⦃V : X.C⦄ (g : V ⟶ U), S g →
      Nonempty (Homotopy (((SheafOfModules.overMap.{w}
        (Stacks.SheafOfModules.Tensor.ringSheaf X.O) g).mapHomologicalComplex
          (ComplexShape.up ℤ)).map α) 0)

AlgebraicGeometry.RingedSite.exists_coveringSieve_homotopy_zero_of_derived_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/StrictlyPerfect/LocalNullHomotopyOfDerivedZero.lean, line 75. The attribute's comment: “local_null_homotopy”. References: SGA 6 I (4.1), “special case”.

Let (C, O) be a ringed site and U an object of C. Let α : E ⟶ F be a map of complexes of O|_U-modules with E strictly perfect, and suppose the image of α in D(O|_U) is zero. Then there is a covering sieve of U such that the restriction of α along each of its arrows is homotopic to zero.

theorem exists_coveringSieve_homotopy_zero_of_derived_zero
    {E F : CochainComplex
      (SheafOfModules.{0} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U)) ℤ}
    (hE : IsStrictlyPerfect ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U) E) (α : E ⟶ F)
    (hα : DerivedCategory.Q.map α = 0) :
    ∃ S : Sieve U, S ∈ X.J U ∧
      ∀ {V : X.C} (f : V ⟶ U), S f →
        Nonempty (Homotopy
          (((SheafOfModules.overFunctor ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U)
            (Over.mk f)).mapHomologicalComplex (ComplexShape.up ℤ)).map α) 0)

AlgebraicGeometry.RingedSite.exists_coveringSieve_complexMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/StrictlyPerfect/LocalRepresentationOfADerivedMap.lean, line 250. The attribute's comment: “local_representation”.

Stacks 08FR (1). Let (C, O) be a ringed site and U an object of C. Let E, F be complexes of O|_U-modules with E strictly perfect. Any morphism α : E ⟶ F of D(O|_U) is, after restriction along the arrows of a covering sieve of U, the image under the localisation functor of a morphism of complexes.

theorem exists_coveringSieve_complexMap
    {E F : CochainComplex
      (SheafOfModules.{w} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U)) ℤ}
    (hE : IsStrictlyPerfect ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U) E)
    (α : DerivedCategory.Q.obj E ⟶ DerivedCategory.Q.obj F) :
    ∃ S : Sieve U, S ∈ X.J U ∧
      ∀ {V : X.C} (f : V ⟶ U), S f →
        let H := SheafOfModules.overMap (Stacks.SheafOfModules.Tensor.ringSheaf X.O) f
        ∃ (hsheaf : HasSheafify (X.J.over V) AddCommGrpCat.{w})
          (hlocal : (X.J.over V).WEqualsLocallyBijective AddCommGrpCat.{w}),
          letI := hsheaf
          letI := hlocal
          letI : HasDerivedCategory
              (SheafOfModules.{w} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over V)) :=
            HasDerivedCategory.standard _
          ∃ (hadd : H.Additive)
            (hlim : PreservesFiniteLimits H)
            (hcolim : PreservesFiniteColimits H),
            letI := hadd
            letI := hlim
            letI := hcolim
            ∃ β : (H.mapHomologicalComplex (ComplexShape.up ℤ)).obj E ⟶
                (H.mapHomologicalComplex (ComplexShape.up ℤ)).obj F,
              H.mapDerivedCategory.map α ≫ H.mapDerivedCategoryFactors.hom.app F =
                H.mapDerivedCategoryFactors.hom.app E ≫ DerivedCategory.Q.map β
Tag 08JH, a lemma

Tag 08JH in the Stacks Project.

AlgebraicGeometry.RingedSite.strictlyPerfectHomComparison_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/StrictlyPerfect/HomComplexComparison.lean, line 159. The attribute's comment: “representation by the finite direct-sum Hom complex”.

Stacks 08JH, the representation statement. For E strictly perfect — bounded, with every term a direct summand of a finite free O-module — the derived internal Hom RSheafHom(E, F) is represented by the ordinary internal Hom complex SheafHom(E, F) of Stacks 0A8Z, the comparison being the canonical one.

By strictlyPerfectHomComparison_isIso_iff this is the quasi-isomorphy of the map of internal Hom complexes induced by the K-injective augmentation of the target, which is homMap_quasiIso_of_isFiniteFreeSummand.

The degreewise direct-sum description of that complex, the other half of Stacks 08JH, is strictlyPerfectHomDegreeIso.

theorem strictlyPerfectHomComparison_isIso
    (hbdd : {i : ℤ | ¬ IsZero (E.X i)}.Finite)
    (hterm : ∀ i : ℤ, IsFiniteFreeSummand X (E.X i)) :
    IsIso (strictlyPerfectHomComparison X D E F)

AlgebraicGeometry.RingedSite.strictlyPerfectHomDegreeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/StrictlyPerfect/HomComplexOfAStrictlyPerfectComplex.lean, line 350. The attribute's comment: “finite direct-sum terms and Hom differential”.

Stacks 08JH, degreewise statement. For E bounded, the n-th term of the internal Hom complex SheafHom(E, F) of Stacks 0A8Z is the direct sum, over q : ℤ, of the internal Hom sheaves SheafHom(E^{-q}, F^{n-q}).

By homDegreeIsLimit the term is the product of those sheaves, with no hypothesis on E. Boundedness makes E^{-q} vanish outside a finite set of q, hence each summand vanish there by internalHomSheaf_isZero_of_isZero, and productCoproductIsoOfFiniteSupport then identifies the product with the coproduct.

The source lemma assumes E strictly perfect; boundedness is the bounded field of that condition and the only part used, so this is the source statement generalized. See the implementation notes for why the strict-perfectness predicate cannot be named at these universes.

The differential needs no separate description: that it is the standard Hom-complex differential is part of the data of SheafHomComplex, whose sectionsIso is an isomorphism of complexes onto CochainComplex.HomComplex on every slice site.

def strictlyPerfectHomDegreeIso
    (E F : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ)
    (hE : {i : ℤ | ¬ IsZero (E.X i)}.Finite) (n : ℤ) :
    ((sheafHomComplex X E F).obj.X n) ≅
      ∐ (fun q : ℤ => internalHomSheaf X (E.X (-q)) (F.X (n - q)))
Tag 08JI, a lemma

Tag 08JI in the Stacks Project.

AlgebraicGeometry.RingedSite.boundedAboveHomRepresentation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedHomOfBoundedAboveSummands.lean, line 145. The attribute's comment: “derived internal Hom represented by the Hom complex, with finite direct-sum terms”.

Stacks 08JI, the whole statement. Let E be a complex of O-modules vanishing above b all of whose terms are direct summands of finite free O-modules, and let F be a complex of O-modules vanishing below a. Then the derived internal Hom RSheafHom(E, F) is represented by the internal Hom complex H = SheafHom(E, F) of Stacks 0A8Z — the comparison being the canonical strictlyPerfectHomComparison — and that complex has H^n = ⨁_{n = p + q} SheafHom(E^{-q}, F^p) in every degree.

The two components are exactly the two assertions of the source, and neither is restated here: the first is strictlyPerfectHomComparison_isIso_of_boundedAbove, the library's Stacks 08I5, at exactly the hypotheses of Stacks 08JI; the second is boundedAboveHomDegreeIso. The differential needs no separate component; see the implementation notes.

def boundedAboveHomRepresentation (D : DerivedInternalHom.{u, d} X) (a b : ℤ)
    (hF : ∀ i : ℤ, i < a → IsZero (F.X i)) (hE : ∀ i : ℤ, b < i → IsZero (E.X i))
    (hterm : ∀ i : ℤ, IsFiniteFreeSummand X (E.X i)) :
    Σ' _ : IsIso (strictlyPerfectHomComparison X D E F),
      ∀ n : ℤ, (sheafHomComplex X E F).obj.X n ≅
        ∐ (fun q : ℤ => internalHomSheaf X (E.X (-q)) (F.X (n - q)))
Sources
LeanIsStrictlyPerfect · mappingCone_isStrictlyPerfect · Stacks.StrictlyPerfect.Modules.isStrictlyPerfect_tensor · Stacks.SheafOfModules.Tensor.isStrictlyPerfect_tensorComplex · AlgebraicGeometry.RingedToposHom.isStrictlyPerfect_pullbackModules · Stacks.Sheaves.StrictlyPerfectPullback.pullbackModules_preservesZeroMorphisms · Stacks.Sheaves.StrictlyPerfectPullback.isStrictlyPerfect_pullbackModules · AlgebraicGeometry.RingedSite.exists_coveringSieve_lift

Section21.45 Pseudo-coherent modules#

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

Tag 08FT, a definition

Tag 08FT in the Stacks Project.

AlgebraicGeometry.RingedSite.IsPseudoCoherentComplexFrom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/PseudoCoherent/PseudoCoherentObjects.lean, line 79. The attribute's comment: “part (1)”.

Stacks 08FT, part (1). A complex E of O-modules is m-pseudo-coherent if every object U of the site admits a covering {V → U} over each member of which there are a strictly perfect complex P of O|_V-modules and a map P ⟶ E|_V inducing isomorphisms on cohomology in every degree > m and an epimorphism on cohomology in degree m.

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

AlgebraicGeometry.RingedSite.IsPseudoCoherentComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/PseudoCoherent/PseudoCoherentObjects.lean, line 94. The attribute's comment: “part (2)”.

Stacks 08FT, part (2). A complex of O-modules is pseudo-coherent if it is m-pseudo-coherent for every integer m.

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

AlgebraicGeometry.RingedSite.IsPseudoCoherentFrom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/PseudoCoherent/PseudoCoherentObjects.lean, line 105. The attribute's comment: “part (3), m-pseudo-coherent”.

Stacks 08FT, part (3), first clause. An object of D(O) is m-pseudo-coherent if it is isomorphic to the image of an m-pseudo-coherent complex.

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

AlgebraicGeometry.RingedSite.IsPseudoCoherent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/PseudoCoherent/PseudoCoherentObjects.lean, line 115. The attribute's comment: “part (3), pseudo-coherent”.

Stacks 08FT, part (3), second clause. An object of D(O) is pseudo-coherent if it is isomorphic to the image of a pseudo-coherent complex.

noncomputable def IsPseudoCoherent
    [HasDerivedCategory.{d} (SheafOfModules.{m} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))]
    (E : DerivedCategory (SheafOfModules.{m} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
    Prop
Tag 08FU, a lemma

Tag 08FU in the Stacks Project.

AlgebraicGeometry.RingedSite.isPseudoCoherent_derivedRestriction_general, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherentSites/RestrictionGeneral.lean, line 276. The attribute's comment: “part (3), all degrees, restriction to a slice”.

Stacks 08FU, part (3), all degrees at once, in the direction which restricts pseudo-coherence to a slice, at independent universes. If an object E of D(O) is pseudo-coherent, then its restriction to the localized ringed site over any object V of C is pseudo-coherent there.

This is not the fixed-degree statement read in each degree: the all-degrees clause of Stacks 08FT (3) asks for one complex which is m-pseudo-coherent for every m, and a family of degreewise statements does not provide it. What the proof restricts is the single complex that pseudo-coherence of E already provides, and it stays m-pseudo-coherent for every m by AlgebraicGeometry.RingedSite.isPseudoCoherentComplexFrom_restrictComplex_general, which is itself stated at one complex and an arbitrary degree; so no quantifier swap is needed.

theorem isPseudoCoherent_derivedRestriction_general
    (E : DerivedCategory (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (hE : X.IsPseudoCoherent E) (V : X.C) :
    (X.over V).IsPseudoCoherent
      ((SheafOfModules.overFunctor.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)
        V).mapDerivedCategory.obj E)

AlgebraicGeometry.RingedSite.isPseudoCoherentFrom_of_locally, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/PseudoCoherent/LocalNature.lean, line 442. The attribute's comment: “part (3)”.

Stacks 08FU, part (3). Let (C, O) be a ringed site and let E be an object of D(O). If every object U of C admits a covering {V → U} over each member of which the restriction of E is m-pseudo-coherent, then E is m-pseudo-coherent.

theorem isPseudoCoherentFrom_of_locally
    (E : DerivedCategory (SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) (m : ℤ)
    (h : ∀ U : X.C, ∃ S : Presieve U, Sieve.generate S ∈ X.J U ∧
      ∀ ⦃V : X.C⦄ (f : V ⟶ U), S f →
        (X.over V).IsPseudoCoherentFrom
          ((SheafOfModules.overFunctor.{0}
            (Stacks.SheafOfModules.Tensor.ringSheaf X.O) V).mapDerivedCategory.obj E) m) :
    X.IsPseudoCoherentFrom E m

AlgebraicGeometry.RingedSite.isPseudoCoherentComplexFrom_of_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/PseudoCoherent/Representatives.lean, line 504. The attribute's comment: “part (2)”. References: SGA 6 I (2.2), “a)”.

Stacks 08FU, part (2). Let (C, O) be a ringed site and let E be an object of D(O) which is m-pseudo-coherent. Then every complex of O-modules representing E is m-pseudo-coherent.

theorem isPseudoCoherentComplexFrom_of_iso
    [HasDerivedCategory.{d} (SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))]
    (E : DerivedCategory (SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) (m : ℤ)
    (hE : X.IsPseudoCoherentFrom E m)
    (K : CochainComplex (SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ)
    (e : DerivedCategory.Q.obj K ≅ E) :
    X.IsPseudoCoherentComplexFrom K m

AlgebraicGeometry.RingedSite.isPseudoCoherentFrom_derivedRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/PseudoCoherent/Restriction.lean, line 203. The attribute's comment: “part (3), restriction to a slice”.

Stacks 08FU, part (3), in the direction which restricts pseudo-coherence to a slice. If an object E of D(O) is m-pseudo-coherent, then its restriction to the localized ringed site over any object V of C is m-pseudo-coherent there.

theorem isPseudoCoherentFrom_derivedRestriction
    (E : DerivedCategory (SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) (m : ℤ)
    (hE : X.IsPseudoCoherentFrom E m) (V : X.C) :
    (X.over V).IsPseudoCoherentFrom
      ((SheafOfModules.overFunctor.{0} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)
        V).mapDerivedCategory.obj E) m

AlgebraicGeometry.RingedSite.isPseudoCoherentFrom_of_covering_of_terminal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/PseudoCoherent/TerminalCovering.lean, line 76. The attribute's comment: “part (1)”.

Let (C, O) be a ringed site, let E be an object of D(O) and let T be a final object of C. If a covering {V → T} of T carries over each of its members a strictly perfect complex P of O|_V-modules and a morphism P ⟶ E|_V of D(O|_V) which is an isomorphism on cohomology in every degree > m and an epimorphism on cohomology in degree m, then E is m-pseudo-coherent.

theorem isPseudoCoherentFrom_of_covering_of_terminal
    (T : X.C) (hT : IsTerminal T)
    (E : DerivedCategory (SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) (m : ℤ)
    (S : Presieve T) (hS : Sieve.generate S ∈ X.J T)
    (hdata : ∀ ⦃V : X.C⦄ (f : V ⟶ T), S f →
      ∃ P : CochainComplex
          (SheafOfModules.{0} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over V)) ℤ,
        IsStrictlyPerfect ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over V) P ∧
        ∃ α : DerivedCategory.Q.obj P ⟶
            (SheafOfModules.overFunctor.{0}
              (Stacks.SheafOfModules.Tensor.ringSheaf X.O) V).mapDerivedCategory.obj E,
          (∀ j : ℤ, m < j → IsIso ((DerivedCategory.homologyFunctor _ j).map α)) ∧
          Epi ((DerivedCategory.homologyFunctor _ m).map α)) :
    X.IsPseudoCoherentFrom E m
Tag 08H4, a lemma

Tag 08H4 in the Stacks Project.

AlgebraicGeometry.RingedSite.Hom.isPseudoCoherentFrom_derivedPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/PseudoCoherent/DerivedPullbackAlongRingedTopoi.lean, line 321.

Stacks 08H4. The derived pullback along a morphism of ringed sites of an m-pseudo-coherent object of D(O') is m-pseudo-coherent.

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

theorem Hom.isPseudoCoherentFrom_derivedPullback
    (E : DerivedCategory
      (SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf (ringedTopos Y).O)))
    (m : ℤ)
    (hE : Y.IsPseudoCoherentFrom E m) :
    X.IsPseudoCoherentFrom ((derivedPullback f.toRingedToposSiteHom).obj E) m
Tag 08FV, a lemma

Tag 08FV in the Stacks Project.

AlgebraicGeometry.RingedSite.isPseudoCoherentFrom_of_distinguished_one_general, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/PseudoCoherent/DistinguishedTriangles.lean, line 749. The attribute's comment: “part (1), general universes”.

Stacks 08FV, part (1), with the site, its morphisms and the sections of the structure sheaf at independent universes. Let (C, O) be a ringed site and let K ⟶ L ⟶ M ⟶ K[1] be a distinguished triangle of D(O). If K is (m + 1)-pseudo-coherent and L is m-pseudo-coherent, then M is m-pseudo-coherent.

theorem isPseudoCoherentFrom_of_distinguished_one_general (m : ℤ)
    (T : Triangle
      (DerivedCategory (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))))
    (hT : T ∈ distinguishedTriangles)
    (hK : X.IsPseudoCoherentFrom T.obj₁ (m + 1))
    (hL : X.IsPseudoCoherentFrom T.obj₂ m) :
    X.IsPseudoCoherentFrom T.obj₃ m

AlgebraicGeometry.RingedSite.isPseudoCoherentFrom_of_distinguished_two_general, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/PseudoCoherent/DistinguishedTriangles.lean, line 773. The attribute's comment: “part (2), general universes”.

Stacks 08FV, part (2), at independent site, morphism and module universes. If the first and third vertices of a distinguished triangle of D(O) are m-pseudo-coherent, so is the second.

Apply part (1) to the inverse rotation M[-1] ⟶ K ⟶ L ⟶ M.

theorem isPseudoCoherentFrom_of_distinguished_two_general (m : ℤ)
    (T : Triangle
      (DerivedCategory (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))))
    (hT : T ∈ distinguishedTriangles)
    (hK : X.IsPseudoCoherentFrom T.obj₁ m)
    (hM : X.IsPseudoCoherentFrom T.obj₃ m) :
    X.IsPseudoCoherentFrom T.obj₂ m

AlgebraicGeometry.RingedSite.isPseudoCoherentFrom_of_distinguished_three_general, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/PseudoCoherent/DistinguishedTriangles.lean, line 792. The attribute's comment: “part (3), general universes”.

Stacks 08FV, part (3), at independent site, morphism and module universes. If the second vertex of a distinguished triangle of D(O) is (m + 1)-pseudo-coherent and the third is m-pseudo-coherent, then the first is (m + 1)-pseudo-coherent.

Apply part (1) to the rotation L ⟶ M ⟶ K[1] ⟶ L[1] and shift back.

theorem isPseudoCoherentFrom_of_distinguished_three_general (m : ℤ)
    (T : Triangle
      (DerivedCategory (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))))
    (hT : T ∈ distinguishedTriangles)
    (hL : X.IsPseudoCoherentFrom T.obj₂ (m + 1))
    (hM : X.IsPseudoCoherentFrom T.obj₃ m) :
    X.IsPseudoCoherentFrom T.obj₁ (m + 1)

AlgebraicGeometry.RingedSite.isPseudoCoherentFrom_of_distinguished_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/PseudoCoherent/DistinguishedTriangles.lean, line 819. The attribute's comment: “part (1)”.

Stacks 08FV, part (1). Let (C, O) be a ringed site and let K ⟶ L ⟶ M ⟶ K[1] be a distinguished triangle of D(O). If K is (m + 1)-pseudo-coherent and L is m-pseudo-coherent, then M is m-pseudo-coherent.

theorem isPseudoCoherentFrom_of_distinguished_one (m : ℤ)
    (T : Triangle
      (DerivedCategory (SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))))
    (hT : T ∈ distinguishedTriangles)
    (hK : X.IsPseudoCoherentFrom T.obj₁ (m + 1))
    (hL : X.IsPseudoCoherentFrom T.obj₂ m) :
    X.IsPseudoCoherentFrom T.obj₃ m

AlgebraicGeometry.RingedSite.isPseudoCoherentFrom_of_distinguished_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/PseudoCoherent/DistinguishedTriangles.lean, line 833. The attribute's comment: “part (2)”. References: SGA 6 I (2.5), “b)”.

Stacks 08FV, part (2). If the first and third vertices of a distinguished triangle of D(O) are m-pseudo-coherent, so is the second.

Apply part (1) to the inverse rotation M[-1] ⟶ K ⟶ L ⟶ M.

theorem isPseudoCoherentFrom_of_distinguished_two (m : ℤ)
    (T : Triangle
      (DerivedCategory (SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))))
    (hT : T ∈ distinguishedTriangles)
    (hK : X.IsPseudoCoherentFrom T.obj₁ m)
    (hM : X.IsPseudoCoherentFrom T.obj₃ m) :
    X.IsPseudoCoherentFrom T.obj₂ m

AlgebraicGeometry.RingedSite.isPseudoCoherentFrom_of_distinguished_three, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/PseudoCoherent/DistinguishedTriangles.lean, line 848. The attribute's comment: “part (3)”.

Stacks 08FV, part (3). If the second vertex of a distinguished triangle of D(O) is (m + 1)-pseudo-coherent and the third is m-pseudo-coherent, then the first is (m + 1)-pseudo-coherent.

Apply part (1) to the rotation L ⟶ M ⟶ K[1] ⟶ L[1] and shift back.

theorem isPseudoCoherentFrom_of_distinguished_three (m : ℤ)
    (T : Triangle
      (DerivedCategory (SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))))
    (hT : T ∈ distinguishedTriangles)
    (hL : X.IsPseudoCoherentFrom T.obj₂ (m + 1))
    (hM : X.IsPseudoCoherentFrom T.obj₃ m) :
    X.IsPseudoCoherentFrom T.obj₁ (m + 1)
Tag 09J9, a lemma

Tag 09J9 in the Stacks Project.

Stacks.SheafOfModules.DerivedTensorProduct.isPseudoCoherentFrom_derivedTensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/PseudoCoherent/DerivedTensorProduct.lean, line 734. The attribute's comment: “part (1)”.

Stacks 09J9, part (1). Let (C, O) be a ringed site and let K, L be objects of D(O). If K is n-pseudo-coherent with H^i(K) = 0 for i > a, and L is m-pseudo-coherent with H^j(L) = 0 for j > b, then K ⊗^{𝐋}_O L is t-pseudo-coherent for t = max (m + a) (n + b). Here ⊗^{𝐋}_O is the derived tensor product of Stacks 06YU, Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor.

theorem isPseudoCoherentFrom_derivedTensorProduct
    (K L : DerivedCategory (_root_.SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (n m a b : ℤ)
    (hK : X.IsPseudoCoherentFrom K n)
    (hKa : ∀ i : ℤ, a < i →
      IsZero ((DerivedCategory.homologyFunctor
        (_root_.SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) i).obj K))
    (hL : X.IsPseudoCoherentFrom L m)
    (hLb : ∀ j : ℤ, b < j →
      IsZero ((DerivedCategory.homologyFunctor
        (_root_.SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) j).obj L)) :
    X.IsPseudoCoherentFrom
      ((Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor X.O |>.obj K).obj L)
      (max (m + a) (n + b))

Stacks.SheafOfModules.DerivedTensorProduct.isPseudoCoherent_derivedTensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/PseudoCoherent/DerivedTensorProduct.lean, line 755. The attribute's comment: “part (2)”.

Stacks 09J9, part (2). Let (C, O) be a ringed site. If K and L are pseudo-coherent objects of D(O), then K ⊗^{𝐋}_O L is pseudo-coherent. Here ⊗^{𝐋}_O is the derived tensor product of Stacks 06YU, Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor.

theorem isPseudoCoherent_derivedTensorProduct
    (K L : DerivedCategory (_root_.SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (hK : X.IsPseudoCoherent K) (hL : X.IsPseudoCoherent L) :
    X.IsPseudoCoherent
      ((Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor X.O |>.obj K).obj L)
Tag 08FW, a lemma

Tag 08FW in the Stacks Project.

AlgebraicGeometry.RingedSite.isPseudoCoherentFrom_left_of_biprod_general, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/PseudoCoherent/Summands.lean, line 375. The attribute's comment: “m-pseudo-coherent, first summand, general universes”.

Stacks 08FW, at independent site, morphism and module universes. Let (C, O) be a ringed site and n : ℤ. If K ⊞ L is n-pseudo-coherent in D(O), then so is K.

Over an object V of the site carrying a strictly perfect approximation of (K ⊞ L)|_V, the cohomology of K|_V and of L|_V vanishes above the support of the approximation, so both are N-pseudo-coherent for that N; descending through the split distinguished triangles makes K|_V and L|_V n-pseudo-coherent, and Stacks 08FU (3) globalizes that.

theorem isPseudoCoherentFrom_left_of_biprod_general
    (K L : DerivedCategory (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (n : ℤ) (h : X.IsPseudoCoherentFrom (K ⊞ L) n) : X.IsPseudoCoherentFrom K n

AlgebraicGeometry.RingedSite.isPseudoCoherentFrom_right_of_biprod_general, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/PseudoCoherent/Summands.lean, line 455. The attribute's comment: “m-pseudo-coherent, second summand, general universes”.

Stacks 08FW, at independent site, morphism and module universes. If K ⊞ L is n-pseudo-coherent in D(O), then so is L: exchange the two summands.

theorem isPseudoCoherentFrom_right_of_biprod_general
    (K L : DerivedCategory (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (n : ℤ) (h : X.IsPseudoCoherentFrom (K ⊞ L) n) : X.IsPseudoCoherentFrom L n

AlgebraicGeometry.RingedSite.isPseudoCoherent_left_of_biprod_general, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/PseudoCoherent/Summands.lean, line 464. The attribute's comment: “pseudo-coherent, first summand, general universes”.

Stacks 08FW, at independent site, morphism and module universes. If K ⊞ L is pseudo-coherent in D(O), then so is K.

theorem isPseudoCoherent_left_of_biprod_general
    (K L : DerivedCategory (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (h : X.IsPseudoCoherent (K ⊞ L)) : X.IsPseudoCoherent K

AlgebraicGeometry.RingedSite.isPseudoCoherent_right_of_biprod_general, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/PseudoCoherent/Summands.lean, line 474. The attribute's comment: “pseudo-coherent, second summand, general universes”.

Stacks 08FW, at independent site, morphism and module universes. If K ⊞ L is pseudo-coherent in D(O), then so is L.

theorem isPseudoCoherent_right_of_biprod_general
    (K L : DerivedCategory (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (h : X.IsPseudoCoherent (K ⊞ L)) : X.IsPseudoCoherent L

AlgebraicGeometry.RingedSite.isPseudoCoherentFrom_left_of_biprod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/PseudoCoherent/Summands.lean, line 544. The attribute's comment: “m-pseudo-coherent, first summand”. References: SGA 6 I (2.12), “n-pc: sum ⇒ F'”.

Stacks 08FW. Let (C, O) be a ringed site and n : ℤ. If K ⊞ L is n-pseudo-coherent in D(O), then so is K.

Over an object V of the site carrying a strictly perfect approximation of (K ⊞ L)|_V, the cohomology of K|_V and of L|_V vanishes above the support of the approximation, so both are N-pseudo-coherent for that N; descending through the split distinguished triangles makes K|_V and L|_V n-pseudo-coherent, and Stacks 08FU (3) globalizes that.

theorem isPseudoCoherentFrom_left_of_biprod
    (K L : DerivedCategory (SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (n : ℤ) (h : X.IsPseudoCoherentFrom (K ⊞ L) n) : X.IsPseudoCoherentFrom K n

AlgebraicGeometry.RingedSite.isPseudoCoherentFrom_right_of_biprod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/PseudoCoherent/Summands.lean, line 552. The attribute's comment: “m-pseudo-coherent, second summand”. References: SGA 6 I (2.12), “n-pc: sum ⇒ F''”.

Stacks 08FW. If K ⊞ L is n-pseudo-coherent in D(O), then so is L: exchange the two summands and apply the previous statement.

theorem isPseudoCoherentFrom_right_of_biprod
    (K L : DerivedCategory (SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (n : ℤ) (h : X.IsPseudoCoherentFrom (K ⊞ L) n) : X.IsPseudoCoherentFrom L n

AlgebraicGeometry.RingedSite.isPseudoCoherent_left_of_biprod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/PseudoCoherent/Summands.lean, line 560. The attribute's comment: “pseudo-coherent, first summand”. References: SGA 6 I (2.12), “pc: sum ⇒ F'”.

Stacks 08FW. If K ⊞ L is pseudo-coherent in D(O), then so is K.

theorem isPseudoCoherent_left_of_biprod
    (K L : DerivedCategory (SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (h : X.IsPseudoCoherent (K ⊞ L)) : X.IsPseudoCoherent K

AlgebraicGeometry.RingedSite.isPseudoCoherent_right_of_biprod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/PseudoCoherent/Summands.lean, line 569. The attribute's comment: “pseudo-coherent, second summand”.

Stacks 08FW. If K ⊞ L is pseudo-coherent in D(O), then so is L.

theorem isPseudoCoherent_right_of_biprod
    (K L : DerivedCategory (SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (h : X.IsPseudoCoherent (K ⊞ L)) : X.IsPseudoCoherent L
Tag 08FX, a lemma

Tag 08FX in the Stacks Project.

AlgebraicGeometry.RingedSite.isFiniteType_homology_general, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherentSites/TopCohomologyFinitenessGeneral.lean, line 55. The attribute's comment: “finite_type_top_cohomology, at independent universes”.

The degree-m cohomology of an m-pseudo-coherent object of the derived category of modules over a ringed site RingedSite.{u, v, w}, whose cohomology vanishes above m, is of finite type.

theorem isFiniteType_homology_general (X : RingedSite.{u, v, w})
    [X.J.HasSheafCompose (forget₂ CommRingCat.{w} RingCat.{w})]
    [HasSheafify X.J AddCommGrpCat.{w}]
    [X.J.WEqualsLocallyBijective AddCommGrpCat.{w}]
    [∀ U : X.C, HasSheafify (X.J.over U) AddCommGrpCat.{w}]
    [∀ U : X.C, (X.J.over U).WEqualsLocallyBijective AddCommGrpCat.{w}]
    [∀ U : X.C, (X.J.over U).HasSheafCompose (forget₂ RingCat.{w} AddCommGrpCat.{w})]
    [HasDerivedCategory.{d} (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))]
    (K : DerivedCategory (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) (m : ℤ)
    (hK : X.IsPseudoCoherentFrom K m)
    (hvanish : ∀ i : ℤ, m < i →
      IsZero ((DerivedCategory.homologyFunctor
        (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) i).obj K)) :
    ((DerivedCategory.homologyFunctor
      (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) m).obj K).IsFiniteType

AlgebraicGeometry.RingedSite.isFiniteType_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LowerShriekAndPerfection/TopCohomologyFiniteness.lean, line 76. The attribute's comment: “finite_type_top_cohomology”.

Stacks 08FX, finite type of the top cohomology. The degree-m cohomology of an m-pseudo-coherent object of the derived category whose higher cohomology vanishes is of finite type.

theorem isFiniteType_homology (X : RingedSite.{u, u, 0})
    [X.J.HasSheafCompose (forget₂ CommRingCat.{0} RingCat.{0})]
    [HasSheafify X.J AddCommGrpCat.{0}]
    [X.J.WEqualsLocallyBijective AddCommGrpCat.{0}]
    [∀ U : X.C, HasSheafify (X.J.over U) AddCommGrpCat.{0}]
    [∀ U : X.C, (X.J.over U).WEqualsLocallyBijective AddCommGrpCat.{0}]
    [∀ U : X.C, (X.J.over U).HasSheafCompose (forget₂ RingCat.{0} AddCommGrpCat.{0})]
    [HasDerivedCategory.{d} (SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))]
    (K : DerivedCategory (SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) (m : ℤ)
    (hK : X.IsPseudoCoherentFrom K m)
    (hvanish : ∀ i : ℤ, m < i →
      IsZero ((DerivedCategory.homologyFunctor
        (SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) i).obj K)) :
    ((DerivedCategory.homologyFunctor
      (SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) m).obj K).IsFiniteType

AlgebraicGeometry.RingedSite.isFinitePresentation_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LowerShriekAndPerfection/TopCohomologyFiniteness.lean, line 214. The attribute's comment: “finite_presentation_top_cohomology”.

Stacks 08FX, finite presentation of the top cohomology. The degree-m + 1 cohomology of an m-pseudo-coherent object of the derived category whose cohomology vanishes above m + 1 is finitely presented.

theorem isFinitePresentation_homology (X : RingedSite.{u, u, 0})
    [X.J.HasSheafCompose (forget₂ CommRingCat.{0} RingCat.{0})]
    [HasSheafify X.J AddCommGrpCat.{0}]
    [X.J.WEqualsLocallyBijective AddCommGrpCat.{0}]
    [∀ U : X.C, HasSheafify (X.J.over U) AddCommGrpCat.{0}]
    [∀ U : X.C, (X.J.over U).WEqualsLocallyBijective AddCommGrpCat.{0}]
    [∀ U : X.C, (X.J.over U).HasSheafCompose (forget₂ RingCat.{0} AddCommGrpCat.{0})]
    [HasDerivedCategory.{d} (SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))]
    (K : DerivedCategory (SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) (m : ℤ)
    (hK : X.IsPseudoCoherentFrom K m)
    (hvanish : ∀ i : ℤ, m + 1 < i →
      IsZero ((DerivedCategory.homologyFunctor
        (SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) i).obj K)) :
    ((DerivedCategory.homologyFunctor
      (SheafOfModules.{0} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) (m + 1)).obj
        K).IsFinitePresentation
Sources
LeanAlgebraicGeometry.RingedSite.IsPseudoCoherentComplexFrom · AlgebraicGeometry.RingedSite.IsPseudoCoherentComplex · AlgebraicGeometry.RingedSite.IsPseudoCoherentFrom · AlgebraicGeometry.RingedSite.IsPseudoCoherent · AlgebraicGeometry.RingedSite.isPseudoCoherent_derivedRestriction_general · AlgebraicGeometry.RingedSite.isPseudoCoherentFrom_of_locally · AlgebraicGeometry.RingedSite.isPseudoCoherentComplexFrom_of_iso · AlgebraicGeometry.RingedSite.isPseudoCoherentFrom_derivedRestriction

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.