21.35 Internal hom in the… to 21.38 Derived lower shriek for…

Section21.35 Internal hom in the derived category#

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

Tag 08J8, an equation

Tag 08J8 in the Stacks Project.

AlgebraicGeometry.RingedSite.derivedCurrySectionsEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/OpenLift/TensorHomSectionsCurrying.lean, line 142. The attribute's comment: “the bijection of morphism groups over an object of the site”.

The tensor–internal-Hom bijection of [Stacks, Tag 08J8] over an object U of the site. Morphisms K|_U ⟶ RSheafHom(B, Z)|_U are morphisms (K ⊗^L_O B)|_U ⟶ Z|_U.

It is the derived currying isomorphism of [Stacks, Tag 08J9] read on degree-zero hypercohomology over U, with both sides identified with groups of morphisms between restrictions by [Stacks, Tag 08JA]. The tensor product is the one taken on C.

def derivedCurrySectionsEquiv
    (K B Z : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
    ((SheafOfModules.overFunctor.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)
        U).mapDerivedCategory.obj K ⟶
        (SheafOfModules.overFunctor.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)
            U).mapDerivedCategory.obj
          (((derivedSheafHomBifunctor X).obj (op B)).obj Z)) ≃+
      ((SheafOfModules.overFunctor.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)
          U).mapDerivedCategory.obj
          (((Stacks.SheafOfModules.derivedTensorProductFunctor X).obj K).obj B) ⟶
        (SheafOfModules.overFunctor.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)
            U).mapDerivedCategory.obj Z)

AlgebraicGeometry.RingedSite.derivedCurrySectionsEquiv_restriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/OpenLift/TensorHomSectionsCurrying.lean, line 222. The attribute's comment: “the bijection over an object of the site restricts the global one”.

The bijection of [Stacks, Tag 08J8] over U is the restriction of the bijection over C. For g : K ⟶ RSheafHom(B, Z) the morphism (K ⊗^L_O B)|_U ⟶ Z|_U matched with g|_U over U is the restriction of the morphism K ⊗^L_O B ⟶ Z matched with g over C.

This is the compatibility of [Stacks, Tag 08JA] globally and over U under restriction of hypercohomology, applied at the two ends of the bijection, with the naturality of that restriction at the derived currying isomorphism in between.

theorem derivedCurrySectionsEquiv_restriction
    (K B Z : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (g : K ⟶ ((derivedSheafHomBifunctor X).obj (op B)).obj Z) :
    derivedCurrySectionsEquiv X U K B Z
        ((SheafOfModules.overFunctor.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)
            U).mapDerivedCategory.map g) =
      (SheafOfModules.overFunctor.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)
          U).mapDerivedCategory.map
        (derivedCurryHomEquiv X K B Z g)

AlgebraicGeometry.RingedSite.derivedCurrySectionsEquiv_naturality_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/OpenLift/TensorHomSectionsCurrying.lean, line 343. The attribute's comment: “functoriality in the source, over an object of the site”.

The bijection of [Stacks, Tag 08J8] over U is natural in its source variable. For a morphism u : K' ⟶ K of D(O), precomposing a morphism K|_U ⟶ RSheafHom(B, Z)|_U with u|_U corresponds to precomposing the matched morphism (K ⊗^L_O B)|_U ⟶ Z|_U with the restriction of u ⊗ 1.

theorem derivedCurrySectionsEquiv_naturality_source
    (K K' B Z : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (u : K' ⟶ K)
    (h : (SheafOfModules.overFunctor.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)
        U).mapDerivedCategory.obj K ⟶
      (SheafOfModules.overFunctor.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)
          U).mapDerivedCategory.obj
        (((derivedSheafHomBifunctor X).obj (op B)).obj Z)) :
    derivedCurrySectionsEquiv X U K' B Z
        ((SheafOfModules.overFunctor.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)
            U).mapDerivedCategory.map u ≫ h) =
      (SheafOfModules.overFunctor.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)
          U).mapDerivedCategory.map
          (((Stacks.SheafOfModules.derivedTensorProductFunctor X).map u).app B) ≫
        derivedCurrySectionsEquiv X U K B Z h

AlgebraicGeometry.RingedSite.derivedCurryHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedCurrying.lean, line 221. The attribute's comment: “the tensor-internal-Hom bijection of morphism groups”.

The tensor–internal-Hom isomorphism of morphism groups, Stacks 08J8 as 08J9 gives it: morphisms K ⟶ RSheafHom(L, M) in D(O) are morphisms K ⊗^L_O L ⟶ M.

It is the derived currying isomorphism read on degree-zero global hypercohomology, with both sides identified with groups of morphisms by Stacks 08JA.

def derivedCurryHomEquiv :
    (K ⟶ ((derivedSheafHomBifunctor X).obj (op L)).obj M) ≃+
      (((Stacks.SheafOfModules.derivedTensorProductFunctor X).obj K).obj L ⟶ M)

AlgebraicGeometry.RingedSite.derivedCurryHomEquiv_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedCurryingCounitFormula.lean, line 83. The attribute's comment: “the bijection is tensoring with the identity followed by the evaluation morphism”.

The tensor–internal-Hom bijection is tensoring and then evaluating. For objects K, A, B of D(O) it carries g : K ⟶ RSheafHom(A, B) to

(g ⊗^𝐋_O 1_A) ≫ e,

with e : RSheafHom(A, B) ⊗^𝐋_O A ⟶ B the evaluation morphism AlgebraicGeometry.RingedSite.derivedSheafHomCounit.

theorem derivedCurryHomEquiv_apply
    (K A B : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)))
    (g : K ⟶ ((derivedSheafHomBifunctor Y).obj (op A)).obj B) :
    derivedCurryHomEquiv Y K A B g =
      ((Stacks.SheafOfModules.derivedTensorProductFunctor Y).map g).app A ≫
        derivedSheafHomCounit Y A B

AlgebraicGeometry.RingedSite.derivedCurryHomEquiv_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedCurryingHomEquivNaturality.lean, line 73. The attribute's comment: “naturality of the tensor-internal-Hom bijection in all three objects”.

The tensor–internal-Hom bijection of Stacks 08J8 is natural in all three objects. For morphisms k : K' ⟶ K, l : L' ⟶ L and m : M ⟶ M' of D(O), the bijection carries a morphism θ : K ⟶ RSheafHom(L, M) precomposed with k and postcomposed with RSheafHom(l, m) to its transpose precomposed with the derived tensor product of k and l and postcomposed with m.

theorem derivedCurryHomEquiv_naturality
    {K K' L L' M M' :
      DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))}
    (k : K' ⟶ K) (l : L' ⟶ L) (m : M ⟶ M')
    (θ : K ⟶ ((derivedSheafHomBifunctor X).obj (op L)).obj M) :
    derivedCurryHomEquiv X K' L' M'
        (k ≫ θ ≫ (((derivedSheafHomBifunctor X).map l.op).app M ≫
          ((derivedSheafHomBifunctor X).obj (op L')).map m)) =
      (((Stacks.SheafOfModules.derivedTensorProductFunctor X).map k).app L' ≫
          ((Stacks.SheafOfModules.derivedTensorProductFunctor X).obj K).map l) ≫
        derivedCurryHomEquiv X K L M θ ≫ m

AlgebraicGeometry.RingedSite.derivedCurryHomEquiv_dinaturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedCurryingInternalHomNaturality.lean, line 136. The attribute's comment: “dinaturality of the bijection of morphism groups in the internal-Hom variable”.

Stacks 08J8, dinaturality in the internal-Hom variable. Postcomposing a morphism h : A ⟶ RSheafHom(B, Z) with the map RSheafHom(B, Z) ⟶ RSheafHom(B', Z) induced by v : B' ⟶ B corresponds, under the tensor–internal-Hom bijection, to precomposing the morphism A ⊗^L_O B ⟶ Z matched with h with 1 ⊗ v.

The variable B is contravariant on the left of the bijection and covariant on the right, so this is a dinaturality identity and not a naturality square.

theorem derivedCurryHomEquiv_dinaturality
    {B B' : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))}
    (A Z : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (v : B' ⟶ B)
    (h : A ⟶ ((derivedSheafHomBifunctor X).obj (op B)).obj Z) :
    derivedCurryHomEquiv X A B' Z
        (h ≫ ((derivedSheafHomBifunctor X).map v.op).app Z) =
      ((Stacks.SheafOfModules.derivedTensorProductFunctor X).obj A).map v ≫
        derivedCurryHomEquiv X A B Z h

AlgebraicGeometry.RingedSite.derivedCurryHomEquiv_naturality_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedCurrySourceNaturality.lean, line 537. The attribute's comment: “the tensor-internal-Hom bijection is natural in the source variable”.

Stacks 08J8 is natural in its source variable. Precomposing a morphism h : A ⟶ RSheafHom(B, Z) with u : A' ⟶ A corresponds, under the tensor-internal-Hom bijection derivedCurryHomEquiv, to precomposing the morphism A ⊗^L_O B ⟶ Z matched with h by u ⊗ 1.

The bijection is the derived currying isomorphism of Stacks 08J9 read on degree-zero global hypercohomology with both sides identified with morphism groups by Stacks 08JA, so this is the object-level naturality derivedCurryIso_natural together with the naturality of Stacks 08JA in its source variable, derivedSheafHomGlobalSectionsEquiv_naturality_source.

theorem derivedCurryHomEquiv_naturality_source
    {A A' B Z : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))}
    (u : A' ⟶ A)
    (h : A ⟶ ((derivedSheafHomBifunctor X).obj (op B)).obj Z) :
    derivedCurryHomEquiv X A' B Z (u ≫ h) =
      ((Stacks.SheafOfModules.derivedTensorProductFunctor X).map u).app B ≫
        derivedCurryHomEquiv X A B Z h

AlgebraicGeometry.RingedSite.derivedCurryHomEquiv_naturality_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedCurryTargetNaturality.lean, line 275. The attribute's comment: “the tensor-internal-Hom bijection is natural in the target variable”.

Stacks 08J8 is natural in its target variable. Postcomposing a morphism h : A ⟶ RSheafHom(B, Z) with RSheafHom(B, w), for w : Z ⟶ Z', corresponds under the tensor–internal-Hom bijection derivedCurryHomEquiv to postcomposing the morphism A ⊗^L_O B ⟶ Z matched with h by w.

The bijection is the derived currying isomorphism of Stacks 08J9 read on degree-zero global hypercohomology with both sides identified with morphism groups by Stacks 08JA, so this is the object-level naturality derivedCurryIso_natural together with the naturality of Stacks 08JA in its target variable, derivedSheafHomGlobalSectionsEquiv_naturality_target_globalMap.

theorem derivedCurryHomEquiv_naturality_target
    {A B Z Z' : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))}
    (w : Z ⟶ Z')
    (h : A ⟶ ((derivedSheafHomBifunctor X).obj (op B)).obj Z) :
    derivedCurryHomEquiv X A B Z'
        (h ≫ ((derivedSheafHomBifunctor X).obj (op B)).map w) =
      derivedCurryHomEquiv X A B Z h ≫ w

AlgebraicGeometry.RingedSite.derivedTensorSheafHomAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedCurryTargetNaturality.lean, line 314. The attribute's comment: “the tensor-internal-Hom bijection as an adjunction, at a fixed middle object”.

Stacks 08J8 as an adjunction. For an object B of D(O), the derived tensor product with B is left adjoint to the derived internal Hom out of B:

Hom_{D(O)}(A ⊗^L_O B, Z) ≅ Hom_{D(O)}(A, RSheafHom(B, Z)),

naturally in A and Z. The bijection is derivedCurryHomEquiv, its naturality in A is derivedCurryHomEquiv_naturality_source and its naturality in Z is derivedCurryHomEquiv_naturality_target.

def derivedTensorSheafHomAdjunction
    (B : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
    (Stacks.SheafOfModules.derivedTensorProductFunctor X).flip.obj B ⊣
      (derivedSheafHomBifunctor X).obj (op B)

Stacks.Cohomology.DerivedInternalHomPullback.tensorHomEquivDinatural_ringedSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/InternalHomPullbackDinaturality.lean, line 284. The attribute's comment: “dinaturality of the bijection of morphism groups of Tag 08DI in its internal-hom variable, read on a ringed space at the uncurried spelling of the derived tensor product; the companion clause in the source variable is tensorHomEquivNaturalLeft_ringedSpace”.

The bijection of Tag 08DI on a ringed space is dinatural in its internal-hom variable. This is Transpose.TensorHomEquivDinatural for the bijection of Tag 08DI, the companion of tensorHomEquivNaturalLeft_ringedSpace, and it is the clause the assembly of Stacks.Cohomology.DerivedInternalHomStalk.InternalHomComparison and the dévissage of Tag 0GM7 in the perfect variable both ask for.

The bijection is presented as the site-level RingedSite.derivedCurryHomEquiv of Stacks.SheafOfModules.ringedSite Z.sheaf rather than as Stacks.SheafOfModules.derivedSheafHomTensorEquiv Z.sheaf, which is the same family of additive equivalences; see the implementation notes of this file. convert … using 1 rather than exact for the reason recorded on tensorHomEquivNaturalLeft_ringedSpace: what is left to settle lives inside the FunLike instance of the coercion, where the two spellings of the derived tensor product and of the derived internal hom appear as instance arguments, and the congruence convert builds settles those argument by argument.

theorem tensorHomEquivDinatural_ringedSpace :
    Transpose.TensorHomEquivDinatural (Stacks.SheafOfModules.derivedSheafHom Z.sheaf)
      (internalHomTensorUncurried Z)
      (fun A B C => (RingedSite.derivedCurryHomEquiv
        (Stacks.SheafOfModules.ringedSite Z.sheaf) A B C).toEquiv)

Tag 08JA, a lemma

Tag 08JA in the Stacks Project.

AlgebraicGeometry.RingedSite.derivedSheafHomGlobalSectionsEquiv_naturality_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedCurrySourceNaturality.lean, line 446. The attribute's comment: “global sections, naturality in the source variable”.

Stacks 08JA globally is natural in the source variable, for an arbitrary morphism of D(O): the identification of the degree-zero global hypercohomology of RSheafHom(L, M) with Hom_{D(O)}(L, M) carries the map induced by u : L' ⟶ L to precomposition with u.

This is the global half of the naturality of Stacks 0A94 read at arbitrary objects of D(O): the two sides are compared at the chosen K-flat representative of the source and the chosen K-injective representative of the target, where it is derivedSheafHomGlobalSectionsEquivOfKFlat_naturality_derived.

theorem derivedSheafHomGlobalSectionsEquiv_naturality_source
    {A A' W : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))}
    (u : A' ⟶ A)
    (x : ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} 0).obj
      ((derivedModuleGlobalSections X).obj
        (((derivedSheafHomBifunctor X).obj (op A)).obj W)) : Type u)) :
    derivedSheafHomGlobalSectionsEquiv X A' W (derivedHomGlobalMap X u (𝟙 W) x) =
      u ≫ derivedSheafHomGlobalSectionsEquiv X A W x

AlgebraicGeometry.RingedSite.derivedSheafHomGlobalSectionsEquiv_naturality_target_globalMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedCurryTargetNaturality.lean, line 168. The attribute's comment: “global sections, naturality in the target variable”.

Stacks 08JA globally is natural in the target variable, for an arbitrary morphism of D(O): the identification of the degree-zero global hypercohomology of RSheafHom(A, W) with Hom_{D(O)}(A, W) carries the map induced by v : W ⟶ W' to postcomposition with v.

This is the target half of the naturality of Stacks 0A94 read at arbitrary objects of D(O): the two sides are compared at the chosen K-flat representative of the source and the chosen K-injective representatives of the two targets, where it is derivedSheafHomGlobalSectionsEquivOfKFlat_naturality_derived_snd.

theorem derivedSheafHomGlobalSectionsEquiv_naturality_target_globalMap
    {A W W' : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))}
    (v : W ⟶ W')
    (x : ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} 0).obj
      ((derivedModuleGlobalSections X).obj
        (((derivedSheafHomBifunctor X).obj (op A)).obj W)) : Type u)) :
    derivedSheafHomGlobalSectionsEquiv X A W' (derivedHomGlobalMap X (𝟙 A) v x) =
      derivedSheafHomGlobalSectionsEquiv X A W x ≫ v

AlgebraicGeometry.RingedSite.derivedSheafHomGlobalSectionsEquiv_naturality_bifunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedSectionsNaturality.lean, line 239. The attribute's comment: “global sections, naturality in both variables”.

Stacks 08JA globally is natural in both variables. For arbitrary morphisms f : L' ⟶ L and g : M ⟶ M' of D(O), the identification of the degree-zero global hypercohomology of RSheafHom(L, M) with Hom_{D(O)}(L, M) carries the derived internal Hom of f and g to precomposition with f and postcomposition with g.

theorem derivedSheafHomGlobalSectionsEquiv_naturality_bifunctor
    {L L' M M' : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))}
    (f : L' ⟶ L) (g : M ⟶ M')
    (z : ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} 0).obj
      ((derivedModuleGlobalSections X).obj
        (((derivedSheafHomBifunctor X).obj (op L)).obj M)) : Type u)) :
    derivedSheafHomGlobalSectionsEquiv X L' M'
        ((derivedSheafHomGlobalSectionsFunctor X).map
          ((f.op, g) : ((op L, M) :
            (DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))ᵒᵖ ×
              DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) ⟶
            (op L', M')) z) =
      f ≫ derivedSheafHomGlobalSectionsEquiv X L M z ≫ g

AlgebraicGeometry.RingedSite.derivedSheafHomGlobalSectionsEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedSectionsOnDerivedObjects.lean, line 227. The attribute's comment: “global sections”. References: SGA 6 I (8.1), “partial”.

Stacks 08JA globally. For arbitrary objects L, M of D(O) the degree-zero global hypercohomology of the derived internal Hom RSheafHom(L, M) is the group of morphisms L ⟶ M in the derived category of O-modules.

A K-injective complex representing M and a K-flat complex representing L are chosen; the internal Hom complex between them is K-injective by Stacks 0A96, so global sections compute derived global sections and the degree-zero cohomology is the group of derived-category morphisms, by Stacks 0A94.

def derivedSheafHomGlobalSectionsEquiv
    (L M : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
    ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} 0).obj
        ((derivedModuleGlobalSections X).obj
          (((derivedSheafHomBifunctor X).obj (op L)).obj M)) : Type u) ≃+ (L ⟶ M)

AlgebraicGeometry.RingedSite.derivedSheafHomSectionsEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedSectionsOnDerivedObjects.lean, line 269. The attribute's comment: “sections over an object”.

Stacks 08JA over an object of the site. For arbitrary objects L, M of D(O) the degree-zero hypercohomology over U of the derived internal Hom RSheafHom(L, M) is the group of morphisms L|_U ⟶ M|_U in the derived category of O|_U-modules.

A K-injective complex representing M and a K-flat complex representing L are chosen; the internal Hom complex between them is K-injective by Stacks 0A96, so sections compute derived sections and the degree-zero cohomology is the group of derived-category morphisms between the restrictions, by Stacks 0A94.

def derivedSheafHomSectionsEquiv
    (L M : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
    ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} 0).obj
        ((Stacks.Cohomology.Localization.derivedSectionsOverObject X U).obj
          (((derivedSheafHomBifunctor X).obj (op L)).obj M)) : Type u) ≃+
      ((SheafOfModules.overFunctor.{u}
          (Stacks.SheafOfModules.Tensor.ringSheaf X.O) U).mapDerivedCategory.obj L ⟶
        (SheafOfModules.overFunctor.{u}
          (Stacks.SheafOfModules.Tensor.ringSheaf X.O) U).mapDerivedCategory.obj M)

AlgebraicGeometry.RingedSite.derivedSheafHomSectionsEquiv_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedSectionsOverAnObjectNaturality.lean, line 475. The attribute's comment: “sections over an object, naturality in both variables”.

Stacks 08JA over an object of the site is natural in both variables. For arbitrary morphisms f : L' ⟶ L and g : M ⟶ M' of D(O), the identification of the degree-zero hypercohomology over U of RSheafHom(L, M) with Hom_{D(O|_U)}(L|_U, M|_U) carries the derived internal Hom of f and g to precomposition with f|_U and postcomposition with g|_U.

theorem derivedSheafHomSectionsEquiv_naturality
    {L L' M M' : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))}
    (f : L' ⟶ L) (g : M ⟶ M')
    (z : ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} 0).obj
      ((Stacks.Cohomology.Localization.derivedSectionsOverObject X U).obj
        (((derivedSheafHomBifunctor X).obj (op L)).obj M)) : Type u)) :
    derivedSheafHomSectionsEquiv X U L' M'
        ((derivedSheafHomSectionsFunctor X U).map
          ((f.op, g) : ((op L, M) :
              (DerivedCategory
                (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))ᵒᵖ ×
              DerivedCategory (SheafOfModules.{u}
                (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) ⟶
              (op L', M')) z) =
      (SheafOfModules.overFunctor.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)
        U).mapDerivedCategory.map f ≫
        derivedSheafHomSectionsEquiv X U L M z ≫
          (SheafOfModules.overFunctor.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)
            U).mapDerivedCategory.map g

AlgebraicGeometry.RingedSite.derivedSheafHomGlobalSectionsEquiv_naturality_source_homologyMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedSectionsSourceNaturality.lean, line 421. The attribute's comment: “global sections, naturality in the source”.

Stacks 08JA, naturality in the source variable. For objects L', L, M of D(O) and an arbitrary morphism u : L' ⟶ L, the identification of the degree-zero global hypercohomology of RSheafHom(L, M) with Hom_{D(O)}(L, M) carries the contravariant functoriality of the derived internal Hom to precomposition with u.

theorem derivedSheafHomGlobalSectionsEquiv_naturality_source_homologyMap
    {L L' : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))}
    (M : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (u : L' ⟶ L)
    (x : ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} 0).obj
      ((derivedModuleGlobalSections X).obj
        (((derivedSheafHomBifunctor X).obj (op L)).obj M)) : Type u)) :
    derivedSheafHomGlobalSectionsEquiv X L' M
        ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} 0).map
          ((derivedModuleGlobalSections X).map
            (((derivedSheafHomBifunctor X).map u.op).app M)) x) =
      u ≫ derivedSheafHomGlobalSectionsEquiv X L M x

AlgebraicGeometry.RingedSite.derivedSheafHomGlobalSectionsEquiv_naturality_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedSectionsTargetNaturality.lean, line 326. The attribute's comment: “global sections, naturality in the target”.

Stacks 08JA, naturality in the target variable. For objects L, M, M' of D(O) and an arbitrary morphism φ : M ⟶ M', the identification of the degree-zero global hypercohomology of RSheafHom(L, M) with Hom_{D(O)}(L, M) carries the covariant functoriality of the derived internal Hom to postcomposition with φ.

theorem derivedSheafHomGlobalSectionsEquiv_naturality_target
    (L : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    {M M' : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))}
    (φ : M ⟶ M')
    (x : ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} 0).obj
      ((derivedModuleGlobalSections X).obj
        (((derivedSheafHomBifunctor X).obj (op L)).obj M)) : Type u)) :
    derivedSheafHomGlobalSectionsEquiv X L M'
        ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} 0).map
          ((derivedModuleGlobalSections X).map
            (((derivedSheafHomBifunctor X).obj (op L)).map φ)) x) =
      derivedSheafHomGlobalSectionsEquiv X L M x ≫ φ

AlgebraicGeometry.RingedSite.globalDerivedHomDegreeEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/GlobalDerivedHomShift.lean, line 186. The attribute's comment: “global sections in every degree, via the translation in the covariant variable”.

Stacks 0B6E, the cohomology of the global derived hom in every degree. The degree-n cohomology of RHom_O(K, L) is the group of morphisms K ⟶ L[n] in D(O), that is the Ext-group Ext^n_{D(O)}(K, L). This is the abelian-group-valued reading AlgebraicGeometry.RingedSite.globalDerivedHom of the global derived hom.

The degree is moved into the covariant variable: the homology functors of the derived category form a shift sequence, derived global sections commute with the translation, and the derived internal Hom commutes with the translation in its covariant variable by AlgebraicGeometry.RingedSite.derivedSheafHomTargetShiftIso; in degree zero the cohomology is the morphism group by Stacks 08JA, which is AlgebraicGeometry.RingedSite.derivedSheafHomGlobalSectionsEquiv.

def globalDerivedHomDegreeEquiv
    (K L : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (n : ℤ) :
    ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} n).obj
        (((globalDerivedHom X).obj (op K)).obj L) : Type u) ≃+ (K ⟶ L⟦n⟧)

AlgebraicGeometry.RingedSite.derivedStructureSheafGlobalSectionsDegreeEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/StructureSheafHypercohomology.lean, line 72. The attribute's comment: “hypercohomology out of the structure sheaf in every degree”.

Hypercohomology in every degree is morphisms out of the structure sheaf. For an object Z of D(O) the hypercohomology group H^n(C, Z), the degree-n homology of unbounded derived global sections, is the group Hom_{D(O)}(O[0], Z[n]).

This is Tag 08JA at source the structure sheaf in every degree: derived global sections of the identification RSheafHom(O[0], Z) ≅ Z of AlgebraicGeometry.RingedSite.derivedStructureSheafHomIso turn H^n(C, Z) into the degree-n cohomology of the global derived hom RHom_O(O[0], Z), which is Hom(O[0], Z[n]) by Tag 0B6E (AlgebraicGeometry.RingedSite.globalDerivedHomDegreeEquiv). In degree zero it is AlgebraicGeometry.RingedSite.derivedStructureSheafGlobalSectionsEquiv.

def derivedStructureSheafGlobalSectionsDegreeEquiv
    (Z : DerivedCategory (SheafOfModules.{u} (ringSheaf X.O))) (n : ℤ) :
    ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} n).obj
        ((derivedModuleGlobalSections X).obj Z) : Type u) ≃+
      (derivedStructureSheaf X ⟶ Z⟦n⟧)

Stacks.SheafOfModules.derivedStructureSheafGlobalSectionsDegreeEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/StructureSheafHypercohomologyOnASpace.lean, line 57. The attribute's comment: “hypercohomology of a ringed space out of the structure sheaf in every degree”.

Hypercohomology of a ringed space in every degree is morphisms out of the structure sheaf. For an object Z of D(O_X) the hypercohomology group H^n(X, Z), the degree-n homology of unbounded derived global sections, is Hom_{D(O_X)}(O_X[0], Z[n]).

This is AlgebraicGeometry.RingedSite.derivedStructureSheafGlobalSectionsDegreeEquiv read at the site of opens of X.

def derivedStructureSheafGlobalSectionsDegreeEquiv
    (Z : DerivedCategory (StructureSheafModules Rc)) (n : ℤ) :
    ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} n).obj
        ((derivedModuleGlobalSections (ringedSite Rc)).obj Z) : Type u) ≃+
      (RingedSite.derivedStructureSheaf (ringedSite Rc) ⟶ Z⟦n⟧)

Tag 08J9, a lemma

Tag 08J9 in the Stacks Project.

AlgebraicGeometry.RingedSite.derivedCurryHomEquiv_globalSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedCurrying.lean, line 235. The attribute's comment: “recovers the morphism-group bijection on H^0”.

The isomorphism of morphism groups is the derived currying isomorphism on global hypercohomology. This is the last assertion of Stacks 08J9: taking degree-zero global hypercohomology of derivedCurryIso and identifying both sides with morphism groups by Stacks 08JA gives derivedCurryHomEquiv, the bijection (21.35.0.1) of Stacks 08J8.

theorem derivedCurryHomEquiv_globalSections
    (x : ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} 0).obj
      ((derivedModuleGlobalSections X).obj
        (((derivedSheafHomBifunctor X).obj (op K)).obj
          (((derivedSheafHomBifunctor X).obj (op L)).obj M))) : Type u)) :
    derivedCurryHomEquiv X K L M
        (derivedSheafHomGlobalSectionsEquiv X K
          (((derivedSheafHomBifunctor X).obj (op L)).obj M) x) =
      derivedSheafHomGlobalSectionsEquiv X
        (((Stacks.SheafOfModules.derivedTensorProductFunctor X).obj K).obj L) M
        (derivedCurryGlobalEquiv X K L M x)

AlgebraicGeometry.RingedSite.derivedCurryHomEquiv_globalSections_homologyMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedCurrying.lean, line 252. The attribute's comment: “recovers the morphism-group bijection on H^0”.

derivedCurryHomEquiv_globalSections with the additive equivalence derivedCurryGlobalEquiv spelled out as the map induced by derivedCurryIso.

theorem derivedCurryHomEquiv_globalSections_homologyMap
    (x : ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} 0).obj
      ((derivedModuleGlobalSections X).obj
        (((derivedSheafHomBifunctor X).obj (op K)).obj
          (((derivedSheafHomBifunctor X).obj (op L)).obj M))) : Type u)) :
    derivedCurryHomEquiv X K L M
        (derivedSheafHomGlobalSectionsEquiv X K
          (((derivedSheafHomBifunctor X).obj (op L)).obj M) x) =
      derivedSheafHomGlobalSectionsEquiv X
        (((Stacks.SheafOfModules.derivedTensorProductFunctor X).obj K).obj L) M
        ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} 0).map
          ((derivedModuleGlobalSections X).map (derivedCurryIso X K L M).hom) x)

AlgebraicGeometry.RingedSite.derivedCurryNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedCurryingNaturality.lean, line 514. The attribute's comment: “functoriality in all three objects”. References: SGA 6 I (7.4), “first isomorphism”.

Stacks 08J9: the derived currying isomorphism is a natural isomorphism. The canonical isomorphism

RSheafHom(K, RSheafHom(L, M)) ≅ RSheafHom(K ⊗^L_O L, M)

of AlgebraicGeometry.RingedSite.derivedCurryIso, bundled as an isomorphism between the trifunctor (K, L, M) ↦ RSheafHom(K, RSheafHom(L, M)) and the trifunctor (K, L, M) ↦ RSheafHom(K ⊗^L_O L, M) on D(O)ᵒᵖ × D(O)ᵒᵖ × D(O). It is obtained by extending the comparison on models.

def derivedCurryNatIso : iteratedHomFunctor X ≅ tensorHomFunctor X

AlgebraicGeometry.RingedSite.derivedCurryIso_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedCurryingNaturality.lean, line 559. The attribute's comment: “functoriality in all three objects”. References: SGA 6 I (7.4), “functoriality, 1st iso”.

Functoriality of the derived currying isomorphism in all three objects. For morphisms k : K' ⟶ K, l : L' ⟶ L and m : M ⟶ M' of D(O) the square formed by derivedCurryIso at (K, L, M) and at (K', L', M') commutes: the derived currying isomorphism is natural contravariantly in the source and in the middle object and covariantly in the target.

theorem derivedCurryIso_natural
    {K K' L L' M M' :
      DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))}
    (k : K' ⟶ K) (l : L' ⟶ L) (m : M ⟶ M') :
    ((derivedSheafHomBifunctor X).map k.op).app
          (((derivedSheafHomBifunctor X).obj (op L)).obj M) ≫
        ((derivedSheafHomBifunctor X).obj (op K')).map
          (((derivedSheafHomBifunctor X).map l.op).app M ≫
            ((derivedSheafHomBifunctor X).obj (op L')).map m) ≫
        (derivedCurryIso X K' L' M').hom =
      (derivedCurryIso X K L M).hom ≫
        ((derivedSheafHomBifunctor X).map
            ((((Stacks.SheafOfModules.derivedTensorProductFunctor X).map k).app L' ≫
              ((Stacks.SheafOfModules.derivedTensorProductFunctor X).obj K).map l).op)).app M ≫
          ((derivedSheafHomBifunctor X).obj
            (op (((Stacks.SheafOfModules.derivedTensorProductFunctor X).obj K').obj L'))).map
              m

AlgebraicGeometry.RingedSite.derivedCurryIso_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedCurryingNaturality.lean, line 604. The attribute's comment: “comparison with currying of complexes”.

The comparison of Stacks 08J9 with the currying isomorphism of complexes of Stacks 0A90. For complexes A, B, I with B K-flat and I K-injective, derivedCurryIso on the classes of A, B, I is, after the two identifications

RSheafHom(QA, RSheafHom(QB, QI)) ≅ Q SheafHom(A, SheafHom(B, I)) and RSheafHom(QA ⊗^L_O QB, QI) ≅ Q SheafHom(Tot(A ⊗_O B), I),

the class of the complex-level currying isomorphism SheafHom(A, SheafHom(B, I)) ≅ SheafHom(Tot(A ⊗\_O B), I).

theorem derivedCurryIso_comparison
    (A B I : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ)
    (hB : Stacks.SheafOfModules.IsKFlat X.O B) [I.IsKInjective] :
    (derivedCurryIso X (DerivedCategory.Q.obj A) (DerivedCategory.Q.obj B)
            (DerivedCategory.Q.obj I)).hom ≫
        (tensorHomRepresentativeIso X A B I hB).hom =
      (iteratedHomRepresentativeIso X A B I hB).hom ≫
        DerivedCategory.Q.map (sheafHomTensorCurryIso X A B I).hom

Tag 08JB, a lemma

Tag 08JB in the Stacks Project.

AlgebraicGeometry.RingedSite.DerivedHomRestriction.complexMap_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedHomRestriction.lean, line 727. The attribute's comment: “restriction on local homogeneous cochains”.

The component of the complex map restricts each local homogeneous map along the iterated slice, as in the canonical comparison of Tag 0E8H.

theorem DerivedHomRestriction.complexMap_apply
    (r : DerivedHomRestriction X U)
    (A B : CochainComplex (SheafOfModules.{u} (ringSheaf X.O)) ℤ)
    (V : (Over U)ᵒᵖ) (W : (Over V.unop)ᵒᵖ)
    (n p q : ℤ) (hpq : p + n = q)
    (s : ((sheafHomComplex X A B).obj.X n).val.obj (op V.unop.left))
    (x : ((restrictComplex (X.over U)
      (restrictComplex X A U) V.unop).X p).val.obj W) :
    (((AddCommGrpCat.Hom.hom
      (((sheafHomComplex (X.over U)
        (restrictComplex X A U) (restrictComplex X B U)).sectionsIso V.unop).hom.f n)
      (((r.complexMap A B).f n).val.app V s)).v p q hpq).val.app W x) =
      (((AddCommGrpCat.Hom.hom
        (((sheafHomComplex X A B).sectionsIso V.unop.left).hom.f n) s).v p q hpq).val.app
          (op (Over.mk W.unop.hom.left)) x)

AlgebraicGeometry.RingedSite.derivedHom_restriction_exists, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedHomRestriction.lean, line 809.

Derived internal Hom commutes, naturally in both arguments, with restriction to the slice site over any object.

theorem derivedHom_restriction_exists :
    Nonempty (DerivedHomRestriction X U)

AlgebraicGeometry.RingedSite.derivedHomRestriction_complexMap_isRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedHomRestriction.lean, line 864. The attribute's comment: “restriction of internal-Hom complexes”.

Restriction of internal-Hom complexes is induced on every homogeneous component by the canonical internal-Hom restriction isomorphism of Tag 0E8H.

theorem derivedHomRestriction_complexMap_isRestriction
    (A B : CochainComplex (SheafOfModules.{u} (ringSheaf X.O)) ℤ) :
    IsInternalHomRestrictionMap X U A B
      ((derivedHomRestriction X U).complexMap A B)

AlgebraicGeometry.RingedSite.derivedHomRestriction_model, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedHomRestriction.lean, line 874. The attribute's comment: “canonical model characterization”.

Under the fixed K-injective and exact-restriction comparisons, the full derived comparison is the localization of the restriction map of internal-Hom complexes induced by Stacks.SheafOfModules.InternalHom.internalHomOverIso.

theorem derivedHomRestriction_model
    (A B : CochainComplex (SheafOfModules.{u} (ringSheaf X.O)) ℤ) [B.IsKInjective] :
    ((derivedHomRestriction X U).iso
      (DerivedCategory.Q.obj A) (DerivedCategory.Q.obj B)).hom ≫
        (restrictionTargetComparison X U A B).hom =
      (restrictionSourceComparison X U A B).hom ≫
        DerivedCategory.Q.map ((derivedHomRestriction X U).complexMap A B)

Tag 08JC, a lemma

Tag 08JC in the Stacks Project.

AlgebraicGeometry.RingedSite.exists_distinguished_derivedSheafHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedHomTriangulated.lean, line 174. The attribute's comment: “contravariant variable”.

Stacks 08JC, contravariant variable. The derived internal Hom into a fixed object carries a distinguished triangle of D(O) to a distinguished triangle: for any distinguished T and any E, the two morphisms RSheafHom(T.obj₃, E) ⟶ RSheafHom(T.obj₂, E) ⟶ RSheafHom(T.obj₁, E) induced by T.mor₂ and T.mor₁ extend by a connecting morphism to a distinguished triangle.

Every distinguished triangle is presented by a termwise split short exact sequence of complexes, so this follows from AlgebraicGeometry.RingedSite.exists_distinguished_derivedSheafHom_of_ses_obj.

theorem exists_distinguished_derivedSheafHom
    (E : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (T : Triangle
      (DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))))
    (hT : T ∈ distTriang
      (DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))) :
    ∃ δ : ((derivedSheafHomBifunctor X).flip.obj E).obj (op T.obj₁) ⟶
        (((derivedSheafHomBifunctor X).flip.obj E).obj (op T.obj₃))⟦(1 : ℤ)⟧,
      Triangle.mk
        (((derivedSheafHomBifunctor X).flip.obj E).map T.mor₂.op)
        (((derivedSheafHomBifunctor X).flip.obj E).map T.mor₁.op)
        δ ∈ distTriang
          (DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))

AlgebraicGeometry.RingedSite.exists_distinguished_derivedSheafHom_second, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/Exactness.lean, line 176. The attribute's comment: “covariant variable”.

The derived internal Hom out of a fixed object carries a distinguished triangle of D(O) to a distinguished triangle: for any distinguished T and any E, the two morphisms RSheafHom(E, T.obj₁) ⟶ RSheafHom(E, T.obj₂) ⟶ RSheafHom(E, T.obj₃) induced by T.mor₁ and T.mor₂ extend by a connecting morphism to a distinguished triangle.

theorem exists_distinguished_derivedSheafHom_second
    (E : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (T : Triangle
      (DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))))
    (hT : T ∈ distTriang
      (DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))) :
    ∃ δ : ((derivedSheafHomBifunctor X).obj (op E)).obj T.obj₃ ⟶
        (((derivedSheafHomBifunctor X).obj (op E)).obj T.obj₁)⟦(1 : ℤ)⟧,
      Triangle.mk
        (((derivedSheafHomBifunctor X).obj (op E)).map T.mor₁)
        (((derivedSheafHomBifunctor X).obj (op E)).map T.mor₂)
        δ ∈ distTriang
          (DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))

Tag 0A97, a lemma

Tag 0A97 in the Stacks Project.

AlgebraicGeometry.RingedSite.derivedEvaluation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedEvaluation.lean, line 505. The attribute's comment: “the canonical evaluation morphism”.

Stacks 0A97: the canonical evaluation morphism of derived internal Homs. For arbitrary objects K, L, M of D(Mod(O)) there is a canonical morphism

RSheafHom(L, M) ⊗^L_O K ⟶ RSheafHom(RSheafHom(K, L), M).

def derivedEvaluation
    (K L M : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
    ((Stacks.SheafOfModules.derivedTensorProductFunctor.{u, u, d} X).obj
        (((derivedInternalHomFunctor.{u, d} X).obj (op L)).obj M)).obj K ⟶
      ((derivedInternalHomFunctor.{u, d} X).obj
        (op (((derivedInternalHomFunctor.{u, d} X).obj (op K)).obj L))).obj M

AlgebraicGeometry.RingedSite.derivedEvaluation_model, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedEvaluation.lean, line 517. The attribute's comment: “comparison with evaluation of complexes”.

Stacks 0A97. On a K-flat source and K-injective targets, the canonical evaluation morphism is the class of the evaluation morphism of internal Hom complexes of Stacks 0A92.

theorem derivedEvaluation_model
    (A B C : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ)
    (hA : Stacks.SheafOfModules.IsKFlat X.O A) [B.IsKInjective] [C.IsKInjective] :
    derivedEvaluation X (DerivedCategory.Q.obj A) (DerivedCategory.Q.obj B)
          (DerivedCategory.Q.obj C) ≫
        (derivedEvaluationTargetComparison X (canonicalDerivedInternalHom.{u, d} X)
          A B C).hom =
      (derivedEvaluationSourceComparison X
          (Stacks.SheafOfModules.canonicalDerivedTensorProduct.{u, u, d} X)
          (canonicalDerivedInternalHom.{u, d} X) A B C hA).hom ≫
        DerivedCategory.Q.map (evaluationMap X A B C)

AlgebraicGeometry.RingedSite.derivedEvaluation_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedEvaluation.lean, line 533. The attribute's comment: “functoriality in all three objects”.

Stacks 0A97. The canonical evaluation morphism is natural in the source object and in the target object, and contranatural in the intermediate object.

theorem derivedEvaluation_natural
    {K K' L L' M M' :
      DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))}
    (f : K ⟶ K') (g : L' ⟶ L) (h : M ⟶ M') :
    derivedEvaluation X K L M ≫
        ((derivedInternalHomFunctor.{u, d} X).map
          ((((derivedInternalHomFunctor.{u, d} X).obj (op K')).map g ≫
            ((derivedInternalHomFunctor.{u, d} X).map f.op).app L).op)).app M ≫
        ((derivedInternalHomFunctor.{u, d} X).obj
          (op (((derivedInternalHomFunctor.{u, d} X).obj (op K')).obj L'))).map h =
      ((Stacks.SheafOfModules.derivedTensorProductFunctor.{u, u, d} X).map
          (((derivedInternalHomFunctor.{u, d} X).map g.op).app M ≫
            ((derivedInternalHomFunctor.{u, d} X).obj (op L')).map h)).app K ≫
        ((Stacks.SheafOfModules.derivedTensorProductFunctor.{u, u, d} X).obj
          (((derivedInternalHomFunctor.{u, d} X).obj (op L')).obj M')).map f ≫
        derivedEvaluation X K' L' M'

Tag 0A98, a lemma

Tag 0A98 in the Stacks Project.

AlgebraicGeometry.RingedSite.derivedSheafHomCompositionConstruction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedCompositionConstruction.lean, line 263.

Stacks 0A98: the composition morphism of derived internal Homs. For arbitrary objects K, L, M of D(Mod(O)) there is a canonical morphism

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

which on a K-flat model of the second internal Hom complex is the composition morphism of internal Hom complexes of Stacks 0A91, and which is contravariant in the source, covariant in the target and dinatural in the intermediate object.

def derivedSheafHomCompositionConstruction : DerivedSheafHomComposition X T Hd

Tag 0BYU, a lemma

Tag 0BYU in the Stacks Project.

AlgebraicGeometry.RingedSite.derivedTensorHomInterchange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedTensorHomInterchange.lean, line 568. The attribute's comment: “the canonical morphism”.

Stacks 0BYU. For objects K, L, M of D(O) there is a canonical morphism

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

in D(O): on a K-flat representative A of K, a K-injective representative I of L and an arbitrary representative C of M it is the interchange morphism of complexes of Stacks 0BYT, followed by the augmentation of Tot(A ⊗_O I) into a K-injective resolution.

def derivedTensorHomInterchange
    (K L M : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
    ((Stacks.SheafOfModules.derivedTensorProductFunctor X).obj K).obj
        (((derivedSheafHomBifunctor X).obj (op M)).obj L) ⟶
      ((derivedSheafHomBifunctor X).obj (op M)).obj
        (((Stacks.SheafOfModules.derivedTensorProductFunctor X).obj K).obj L)

AlgebraicGeometry.RingedSite.derivedTensorHomInterchange_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedTensorHomInterchange.lean, line 597. The attribute's comment: “comparison with the interchange morphism of complexes”.

The comparison of Stacks 0BYU with the interchange morphism of complexes of Stacks 0BYT. For complexes A, I, C with A K-flat and I K-injective, the canonical morphism on their classes is, after the two identifications

QA ⊗^L_O RSheafHom(QC, QI) ≅ Q Tot(A ⊗_O SheafHom(C, I)) and RSheafHom(QC, QA ⊗^L_O QI) ≅ Q SheafHom(C, J) with J the chosen K-injective resolution of Tot(A ⊗_O I),

the class of the interchange morphism of complexes Tot(A ⊗\_O SheafHom(C, I)) ⟶ SheafHom(C, Tot(A ⊗\_O I)) followed by the resolution augmentation.

theorem derivedTensorHomInterchange_comparison
    (A I C : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ)
    (hA : Stacks.SheafOfModules.IsKFlat X.O A) [I.IsKInjective] :
    derivedTensorHomInterchange X (DerivedCategory.Q.obj A) (DerivedCategory.Q.obj I)
          (DerivedCategory.Q.obj C) ≫
        (interchangeTargetIso X A I C hA).hom =
      (interchangeSourceIso X A I C hA).hom ≫
        DerivedCategory.Q.map (tensorHomInterchange X A I C ≫
          homMap X (𝟙 C) ((kInjectiveAugmentation X).app (tensorTotal X A I)))

AlgebraicGeometry.RingedSite.derivedTensorHomInterchange_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedTensorHomInterchange.lean, line 615. The attribute's comment: “functoriality in all three objects”.

Functoriality of the interchange morphism of Stacks 0BYU in all three objects. For morphisms k : K ⟶ K', l : L ⟶ L' and m : M' ⟶ M of D(O) the square formed by the canonical morphism at (K, L, M) and at (K', L', M') commutes: the interchange morphism is natural covariantly in the tensor factor and in the target of the internal Hom and contravariantly in its source.

theorem derivedTensorHomInterchange_natural
    {K K' L L' M M' :
      DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))}
    (k : K ⟶ K') (l : L ⟶ L') (m : M' ⟶ M) :
    ((Stacks.SheafOfModules.derivedTensorProductFunctor X).map k).app
          (((derivedSheafHomBifunctor X).obj (op M)).obj L) ≫
        ((Stacks.SheafOfModules.derivedTensorProductFunctor X).obj K').map
          (((derivedSheafHomBifunctor X).map m.op).app L ≫
            ((derivedSheafHomBifunctor X).obj (op M')).map l) ≫
        derivedTensorHomInterchange X K' L' M' =
      derivedTensorHomInterchange X K L M ≫
        ((derivedSheafHomBifunctor X).map m.op).app
            (((Stacks.SheafOfModules.derivedTensorProductFunctor X).obj K).obj L) ≫
          ((derivedSheafHomBifunctor X).obj (op M')).map
            (((Stacks.SheafOfModules.derivedTensorProductFunctor X).map k).app L ≫
              ((Stacks.SheafOfModules.derivedTensorProductFunctor X).obj K').map l)

Tag 0A99, a lemma

Tag 0A99 in the Stacks Project.

AlgebraicGeometry.RingedSite.canonicalDerivedDiagonal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedDiagonal.lean, line 336. The attribute's comment: “the canonical morphism”.

Stacks 0A99. For objects K, L of D(O) the canonical morphism

K ⟶ RSheafHom(L, K ⊗_O^L L)

in D(O): on the chosen K-flat representative A of K and the chosen K-injective representative B of L it is the diagonal morphism of complexes of Stacks 0A93, followed by the augmentation of Tot(A ⊗_O B) into its chosen K-injective resolution.

def canonicalDerivedDiagonal
    (K L : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
    K ⟶ ((derivedSheafHomBifunctor X).obj (op L)).obj
      (((Stacks.SheafOfModules.derivedTensorProductFunctor X).obj K).obj L)

AlgebraicGeometry.RingedSite.canonicalDerivedDiagonal_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedDiagonal.lean, line 348. The attribute's comment: “the characterisation on representatives”.

The canonical morphism of Stacks 0A99 is the class of the resolved diagonal of complexes, read through the comparisons of its source and target with classes of complexes. In particular it is not an arbitrary morphism between the two objects.

theorem canonicalDerivedDiagonal_eq
    (K L : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
    (kFlatModelIso X K).hom ≫ canonicalDerivedDiagonal X K L ≫
        (diagonalTargetIso X K L L).hom =
      DerivedCategory.Q.map (diagonalComplexMap X (kFlatModel X K) (kInjectiveModel X L))

AlgebraicGeometry.RingedSite.canonicalDerivedDiagonal_natural_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedDiagonal.lean, line 530. The attribute's comment: “functoriality in L”.

Stacks 0A99: the canonical morphism is functorial in L. For a morphism l : L' ⟶ L of D(O) the square

u_{K,L} ≫ RSheafHom(l, 𝟙) = u_{K,L'} ≫ RSheafHom(𝟙, 𝟙_K ⊗ l)

commutes in D(O): the second variable of the diagonal acts contravariantly in the source of the internal Hom and covariantly inside the derived tensor product, which is the dinaturality that the statement of the tag asserts.

The chosen representative of L is K-injective, so l is the class of a morphism of the chosen representatives and the square is the dinaturality of Stacks 0A93 at the level of complexes, conjugated by the target comparisons.

theorem canonicalDerivedDiagonal_natural_right
    (K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    {L L' : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))}
    (l : L' ⟶ L) :
    canonicalDerivedDiagonal X K L ≫
        ((derivedSheafHomBifunctor X).map l.op).app
          (((Stacks.SheafOfModules.derivedTensorProductFunctor X).obj K).obj L) =
      canonicalDerivedDiagonal X K L' ≫
        ((derivedSheafHomBifunctor X).obj (op L')).map
          (((Stacks.SheafOfModules.derivedTensorProductFunctor X).obj K).map l)

AlgebraicGeometry.RingedSite.canonicalDerivedDiagonal_natural_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedDiagonal.lean, line 774. The attribute's comment: “functoriality in K”.

Stacks 0A99: the canonical morphism is functorial in K. For a morphism f : K ⟶ K' of D(O) the square

f ≫ u_{K',L} = u_{K,L} ≫ RSheafHom(𝟙_L, f ⊗ 𝟙_L)

commutes in D(O): the first variable of the diagonal acts covariantly.

A morphism of D(O) does not lift to the chosen K-flat representatives, which are not K-injective. It is instead written as a right fraction inv (Q s₀) ≫ Q g₀ (DerivedCategory.right_fac) and the apex of that roof is replaced by a K-flat resolution of it (Stacks 06YS), giving a roof A ⟵ P ⟶ A' with all three complexes K-flat and the left leg invertible in D(O). The one-sided K-flat comparison of Stacks 06YU is then available at all three vertices, which makes the tensored left leg invertible with no K-flatness of the other factor, and the square closes from the complex-level functoriality of Stacks 0A93.

theorem canonicalDerivedDiagonal_natural_left
    (L : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    {K K' : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))}
    (f : K ⟶ K') :
    f ≫ canonicalDerivedDiagonal X K' L =
      canonicalDerivedDiagonal X K L ≫
        ((derivedSheafHomBifunctor X).obj (op L)).map
          (((Stacks.SheafOfModules.derivedTensorProductFunctor X).map f).app L)

Tag 08JD, a lemma

Tag 08JD in the Stacks Project.

AlgebraicGeometry.RingedSite.derivedTensorDualGlobalSectionsMap_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedSectionsTargetNaturality.lean, line 411. The attribute's comment: “functoriality in M of the map on degree-zero derived global sections”.

The map of Stacks 08JD on degree-zero global hypercohomology is natural in M. For m : M ⟶ M' the map H⁰(C, M ⊗^L_O L^∨) ⟶ Hom_{D(O)}(L, M) of AlgebraicGeometry.RingedSite.derivedTensorDualGlobalSectionsMap carries the map induced by m on the left to postcomposition with m on the right.

That map is the degree-zero global hypercohomology of the canonical map M ⊗^L_O L^∨ ⟶ RSheafHom(L, M) followed by Stacks 08JA, so this is the naturality in M of those two pieces: derivedTensorDualSectionsMap_naturality for the first, and derivedSheafHomGlobalSectionsEquiv_naturality_target above for the second. No bijectivity of the map, hence no perfectness of L, is involved: this is functoriality of the comparison of Stacks 08JD, not Stacks 08DQ.

theorem derivedTensorDualGlobalSectionsMap_naturality
    (L : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    {M M' : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))}
    (m : M ⟶ M')
    (z : ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} 0).obj
      ((derivedModuleGlobalSections X).obj
        ((T.tensor.obj M).obj (derivedDual X L))) : Type u)) :
    derivedTensorDualGlobalSectionsMap X T L M'
        ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} 0).map
          ((derivedModuleGlobalSections X).map
            ((T.tensor.map m).app (derivedDual X L))) z) =
      derivedTensorDualGlobalSectionsMap X T L M z ≫ m

AlgebraicGeometry.RingedSite.derivedTensorDualToSheafHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedTensorDual.lean, line 169. The attribute's comment: “the canonical map”.

Stacks 08JD: the canonical map M ⊗^L_O L^∨ ⟶ RSheafHom(L, M). It is the composition morphism of derived internal Homs of Stacks 0A98, taken at intermediate object the structure sheaf, after the left tensor factor M has been identified with RSheafHom(O, M).

def derivedTensorDualToSheafHom
    (L M : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
    (T.tensor.obj M).obj (derivedDual X L) ⟶
      ((derivedSheafHomBifunctor X).obj (op L)).obj M

AlgebraicGeometry.RingedSite.derivedTensorDualGlobalSectionsMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedTensorDual.lean, line 303. The attribute's comment: “map on degree-zero derived global sections”.

Stacks 08JD: the canonical map on degree-zero global hypercohomology. The canonical map M ⊗^L_O L^∨ ⟶ RSheafHom(L, M) induces a map of abelian groups

H⁰(C, M ⊗^L_O L^∨) ⟶ Hom_{D(O)}(L, M),

namely its degree-zero global hypercohomology followed by the identification H⁰(C, RSheafHom(L, M)) ≅ Hom_{D(O)}(L, M) of Stacks 08JA.

def derivedTensorDualGlobalSectionsMap
    (L M : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
    ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} 0).obj
        ((derivedModuleGlobalSections X).obj
          ((T.tensor.obj M).obj (derivedDual X L))) : Type u) →+ (L ⟶ M)

Tag 0B6D, a remark

Tag 0B6D in the Stacks Project.

Stacks.Cohomology.ProjectionFormulaInternalHomOnRingedTopoi.derivedPushforwardSheafHomMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/ProjectionFormulaInternalHom.lean, line 403. The attribute's comment: “the canonical map, variant: the special case of a morphism of ringed topoi presented by a morphism of sites; the tag for an arbitrary morphism of ringed topoi is Stacks.Cohomology.PushforwardInternalHomOfToposHom.derivedPushforwardSheafHomMap”.

The canonical map of [Stacks, Tag 0B6D] when the morphism of ringed topoi f : (Sh(C), O_C) ⟶ (Sh(D), O_D) comes from a morphism of sites: for objects L, M of D(O_C), the map

Rf_*RHom_{O_C}(L, M) ⟶ RHom_{O_D}(Rf_*L, Rf_*M).

It is the morphism which the tensor–internal-Hom bijection of [Stacks, Tag 08J8] on D(O_D) sends to the relative cup product of [Stacks, Tag 0B6C] followed by Rf_* of the evaluation morphism RHom_{O_C}(L, M) ⊗^L_{O_C} L ⟶ M.

def derivedPushforwardSheafHomMap
    (L M : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
    (derivedPushforward f).obj
        (((RingedSite.derivedSheafHomBifunctor (RingedTopos.toRingedSite X)).obj (op L)).obj M) ⟶
      ((RingedSite.derivedSheafHomBifunctor (RingedTopos.toRingedSite Y)).obj
        (op ((derivedPushforward f).obj L))).obj ((derivedPushforward f).obj M)

Stacks.Cohomology.ProjectionFormulaInternalHomOnRingedTopoi.derivedPushforwardSheafHomMap_homEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/ProjectionFormulaInternalHom.lean, line 435. The attribute's comment: “the defining adjunction property, variant: the special case of a morphism of ringed topoi presented by a morphism of sites; the tag for an arbitrary morphism of ringed topoi is Stacks.Cohomology.PushforwardInternalHomOfToposHom.derivedPushforwardSheafHomMap_homEquiv”.

The defining property of the canonical map of [Stacks, Tag 0B6D]: its adjunct under the tensor–internal-Hom bijection of [Stacks, Tag 08J8] on D(O_D) is the relative cup product of [Stacks, Tag 0B6C] followed by Rf_* of the evaluation morphism RHom_{O_C}(L, M) ⊗^L_{O_C} L ⟶ M.

theorem derivedPushforwardSheafHomMap_homEquiv
    (L M : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
    (derivedTensorHomBijection (RingedTopos.toRingedSite Y)).homEquiv
        ((derivedPushforward f).obj
          (((RingedSite.derivedSheafHomBifunctor
            (RingedTopos.toRingedSite X)).obj (op L)).obj M))
        ((derivedPushforward f).obj L) ((derivedPushforward f).obj M)
        (derivedPushforwardSheafHomMap f hmos L M) =
      relativeCupProduct f hmos
          (((RingedSite.derivedSheafHomBifunctor
            (RingedTopos.toRingedSite X)).obj (op L)).obj M) L ≫
        (derivedPushforward f).map
          ((derivedTensorHomBijection (RingedTopos.toRingedSite X)).evaluation L M)

Stacks.Cohomology.PushforwardInternalHomOfToposHom.derivedPushforwardSheafHomMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/PushforwardInternalHomOfToposHom.lean, line 210. The attribute's comment: “the canonical map, for an arbitrary morphism of ringed topoi (no morphism-of-sites hypothesis); its defining property is derivedPushforwardSheafHomMap_homEquiv”.

[Stacks, Tag 0B6D]. For a morphism of ringed topoi f : (Sh(C), O_C) ⟶ (Sh(D), O_D) and objects L, M of D(O_C), the canonical map

Rf_*RHom_{O_C}(L, M) ⟶ RHom_{O_D}(Rf_*L, Rf_*M).

It is the morphism which the tensor–internal-Hom bijection of [Stacks, Tag 08J8] on D(O_D) sends to the relative cup product Rf_*RHom(L, M) ⊗^L_{O_D} Rf_*L ⟶ Rf_*(RHom(L, M) ⊗^L_{O_C} L) of [Stacks, Tag 0B6C] followed by Rf_* of the evaluation morphism RHom_{O_C}(L, M) ⊗^L_{O_C} L ⟶ M.

def derivedPushforwardSheafHomMap
    (L M : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
    (derivedPushforward f).obj
        (((RingedSite.derivedSheafHomBifunctor (RingedTopos.toRingedSite X)).obj (op L)).obj M) ⟶
      ((RingedSite.derivedSheafHomBifunctor (RingedTopos.toRingedSite Y)).obj
        (op ((derivedPushforward f).obj L))).obj ((derivedPushforward f).obj M)

Stacks.Cohomology.PushforwardInternalHomOfToposHom.derivedPushforwardSheafHomMap_homEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/PushforwardInternalHomOfToposHom.lean, line 240. The attribute's comment: “the defining property: the 08J8 adjunct of the canonical map is the relative cup product of 0B6C followed by Rf_* of evaluation, for an arbitrary morphism of ringed topoi”.

The defining property of the canonical map of [Stacks, Tag 0B6D]: its adjunct under the tensor–internal-Hom bijection of [Stacks, Tag 08J8] on D(O_D) is the relative cup product of [Stacks, Tag 0B6C] followed by Rf_* of the evaluation morphism RHom_{O_C}(L, M) ⊗^L_{O_C} L ⟶ M.

theorem derivedPushforwardSheafHomMap_homEquiv
    (L M : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
    (derivedTensorHomBijection (RingedTopos.toRingedSite Y)).homEquiv
        ((derivedPushforward f).obj
          (((RingedSite.derivedSheafHomBifunctor
            (RingedTopos.toRingedSite X)).obj (op L)).obj M))
        ((derivedPushforward f).obj L) ((derivedPushforward f).obj M)
        (derivedPushforwardSheafHomMap f L M) =
      relativeCupProduct f
          (((RingedSite.derivedSheafHomBifunctor
            (RingedTopos.toRingedSite X)).obj (op L)).obj M) L ≫
        (derivedPushforward f).map
          ((derivedTensorHomBijection (RingedTopos.toRingedSite X)).evaluation L M)

Tag 08JF, a remark

Tag 08JF in the Stacks Project.

AlgebraicGeometry.RingedToposSiteHom.derivedPullbackSheafHomMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedPullbackOfInternalHom.lean, line 176.

Stacks 08JF: the canonical map Lh^* RSheafHom(K, L) ⟶ RSheafHom(Lh^* K, Lh^* L) in D(O), for a morphism of ringed topoi h : (Sh(C), O) ⟶ (Sh(C'), O') and objects K, L of D(O'). It is the arrow corresponding to derivedPullbackSheafHomPairing under the tensor–internal-Hom bijection of Stacks 08J8 on the source topos.

def derivedPullbackSheafHomMap :
    (derivedPullback h).obj
        (((RingedSite.derivedSheafHomBifunctor
          (RingedTopos.toRingedSite Y)).obj (op K)).obj L) ⟶
      ((RingedSite.derivedSheafHomBifunctor (RingedTopos.toRingedSite X)).obj
        (op ((derivedPullback h).obj K))).obj ((derivedPullback h).obj L)

AlgebraicGeometry.RingedToposHom.derivedPullbackSheafHomMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedPullbackOfInternalHomOfToposHom.lean, line 110. The attribute's comment: “for a morphism of ringed topoi in the sense of Tag 01D3, part (2) -- a morphism of the underlying topoi together with the map of structure sheaves, with no functor between the underlying sites”.

Stacks 08JF: the canonical map Lh^* RSheafHom(K, L) ⟶ RSheafHom(Lh^* K, Lh^* L) in D(O), for a morphism of ringed topoi h : (Sh(C), O) ⟶ (Sh(C'), O') in the sense of Stacks 01D3, part (2), and objects K, L of D(O'). It is the arrow corresponding to derivedPullbackSheafHomPairing under the tensor–internal-Hom bijection of Stacks 08J8.

def derivedPullbackSheafHomMap :
    (derivedPullback h).obj
        (((RingedSite.derivedSheafHomBifunctor
          (RingedTopos.toRingedSite Y)).obj (op K)).obj L) ⟶
      ((RingedSite.derivedSheafHomBifunctor (RingedTopos.toRingedSite X)).obj
        (op ((derivedPullback h).obj K))).obj ((derivedPullback h).obj L)

Tag 08JG, a remark

Tag 08JG in the Stacks Project.

Stacks.Cohomology.DerivedInternalHomBaseChangeOnTopoi.derivedBaseChangeSheafHomMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedBaseChangeOfInternalHom.lean, line 175. The attribute's comment: “derived_base_change_sheaf_hom_map, variant: the special case of a square of morphisms of ringed topoi presented by morphisms of sites; the tag for an arbitrary commutative square of morphisms of ringed topoi is Stacks.Cohomology.DerivedInternalHomBaseChangeOfToposHom.derivedBaseChangeSheafHomMap”.

The base change map for the internal hom in the derived category (Stacks 08JG), for a square of morphisms of sites. For a commutative square of ringed topoi with h : (Sh(C'), O_{C'}) ⟶ (Sh(C), O_C) over g : (Sh(D'), O_{D'}) ⟶ (Sh(D), O_D) and objects K, L of D(O_C), the canonical map

Lg^* Rf_* RSheafHom(K, L) ⟶ R(f')_* RSheafHom(Lh^* K, Lh^* L)

in D(O_{D'}). It is the derived base change map of Stacks 07A7 at RSheafHom(K, L) followed by R(f')_* of the canonical map of Stacks 08JF, which is the adjoint of the three-step composition the source describes.

def derivedBaseChangeSheafHomMap :
    (derivedPullback g).obj
        ((derivedPushforward f).obj
          (((RingedSite.derivedSheafHomBifunctor
            (RingedTopos.toRingedSite C)).obj (op K)).obj L)) ⟶
      (derivedPushforward f').obj
        (((RingedSite.derivedSheafHomBifunctor (RingedTopos.toRingedSite C')).obj
            (op ((derivedPullback h).obj K))).obj ((derivedPullback h).obj L))

Stacks.Cohomology.DerivedInternalHomBaseChangeOnTopoi.derivedBaseChangeSheafHomMap_adjoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedBaseChangeOfInternalHom.lean, line 201. The attribute's comment: “derived_base_change_sheaf_hom_map: adjoint characterization, variant: the special case of a square of morphisms of ringed topoi presented by morphisms of sites; the tag for an arbitrary commutative square of morphisms of ringed topoi is Stacks.Cohomology.DerivedInternalHomBaseChangeOfToposHom.derivedBaseChangeSheafHomMap_adjoint”.

The adjoint characterization of the base change map (Stacks 08JG), for a square of morphisms of sites. Under the derived adjunction L(f')^* ⊣ R(f')_* of Stacks 07A6, the base change map for the internal hom is the three-step composition the source prescribes: the two identifications of the iterated derived pullbacks around the square with the derived pullback along its common composite, then the derived pullback along h of the derived counit Lf^* Rf_* ⟶ id at RSheafHom(K, L), then the canonical map of Stacks 08JF.

Since transposition is a bijection this determines the map.

theorem derivedBaseChangeSheafHomMap_adjoint :
    ((derivedAdjunction f' hmosf').homEquiv
        ((derivedPullback g).obj ((derivedPushforward f).obj
          (((RingedSite.derivedSheafHomBifunctor
            (RingedTopos.toRingedSite C)).obj (op K)).obj L)))
        (((RingedSite.derivedSheafHomBifunctor (RingedTopos.toRingedSite C')).obj
            (op ((derivedPullback h).obj K))).obj ((derivedPullback h).obj L))).symm
        (derivedBaseChangeSheafHomMap f h f' g hmosf hmosh hmosf' hmosg sq K L) =
      (derivedPullbackCompIsoLeft f' g hmosf' hmosg).hom.app
          ((derivedPushforward f).obj
            (((RingedSite.derivedSheafHomBifunctor
              (RingedTopos.toRingedSite C)).obj (op K)).obj L)) ≫
        (derivedPullbackCompIsoRight f h f' g hmosf hmosh sq).inv.app
          ((derivedPushforward f).obj
            (((RingedSite.derivedSheafHomBifunctor
              (RingedTopos.toRingedSite C)).obj (op K)).obj L)) ≫
        (derivedPullback h).map ((derivedAdjunction f hmosf).counit.app
          (((RingedSite.derivedSheafHomBifunctor
            (RingedTopos.toRingedSite C)).obj (op K)).obj L)) ≫
        RingedToposSiteHom.derivedPullbackSheafHomMap h hmosh K L

Stacks.Cohomology.DerivedInternalHomBaseChangeOfToposHom.derivedBaseChangeSheafHomMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedBaseChangeOfInternalHomOfToposHom.lean, line 117. The attribute's comment: “for a commutative square of morphisms of ringed topoi in the sense of Tag 01D3, part (2), with no hypothesis beyond commutativity”.

Stacks 08JG: the base change map for the internal hom in the derived category. For a commutative square of morphisms of ringed topoi, with h : (Sh(C'), O_{C'}) ⟶ (Sh(C), O_C) over g : (Sh(D'), O_{D'}) ⟶ (Sh(D), O_D), and objects K, L of D(O_C), the canonical map

Lg^* Rf_* RSheafHom(K, L) ⟶ R(f')_* RSheafHom(Lh^* K, Lh^* L)

in D(O_{D'}): the derived base change map of Stacks 07A7 at RSheafHom(K, L) followed by R(f')_* of the canonical map of Stacks 08JF. Its transpose is the three-step composition of the source, derivedBaseChangeSheafHomMap_adjoint.

def derivedBaseChangeSheafHomMap :
    (derivedPullback g).obj
        ((derivedPushforward f).obj
          (((RingedSite.derivedSheafHomBifunctor
            (RingedTopos.toRingedSite C)).obj (op K)).obj L)) ⟶
      (derivedPushforward f').obj
        (((RingedSite.derivedSheafHomBifunctor (RingedTopos.toRingedSite C')).obj
            (op ((derivedPullback h).obj K))).obj ((derivedPullback h).obj L))

Stacks.Cohomology.DerivedInternalHomBaseChangeOfToposHom.derivedBaseChangeSheafHomMap_adjoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DerivedBaseChangeOfInternalHomOfToposHom.lean, line 137. The attribute's comment: “adjoint characterization, for a commutative square of morphisms of ringed topoi in the sense of Tag 01D3, part (2)”.

Stacks 08JG, the adjoint characterization. Under the derived adjunction L(f')^* ⊣ R(f')_* of Stacks 07A6, the base change map for the internal hom is the composition the source prescribes: the identification L(f')^* Lg^* = Lh^* Lf^* of the iterated derived pullbacks around the square (through the derived pullback along its common composite), then Lh^* of the derived counit Lf^* Rf_* ⟶ id at RSheafHom(K, L), then the canonical map of Stacks 08JF. Since transposition is a bijection this determines the map.

theorem derivedBaseChangeSheafHomMap_adjoint :
    ((derivedAdjunction f').homEquiv
        ((derivedPullback g).obj ((derivedPushforward f).obj
          (((RingedSite.derivedSheafHomBifunctor
            (RingedTopos.toRingedSite C)).obj (op K)).obj L)))
        (((RingedSite.derivedSheafHomBifunctor (RingedTopos.toRingedSite C')).obj
            (op ((derivedPullback h).obj K))).obj ((derivedPullback h).obj L))).symm
        (derivedBaseChangeSheafHomMap f h f' g sq K L) =
      (derivedPullbackCompIsoLeft f' g).hom.app
          ((derivedPushforward f).obj
            (((RingedSite.derivedSheafHomBifunctor
              (RingedTopos.toRingedSite C)).obj (op K)).obj L)) ≫
        (derivedPullbackCompIsoRight f h f' g sq).inv.app
          ((derivedPushforward f).obj
            (((RingedSite.derivedSheafHomBifunctor
              (RingedTopos.toRingedSite C)).obj (op K)).obj L)) ≫
        (derivedPullback h).map ((derivedAdjunction f).counit.app
          (((RingedSite.derivedSheafHomBifunctor
            (RingedTopos.toRingedSite C)).obj (op K)).obj L)) ≫
        RingedToposHom.derivedPullbackSheafHomMap h K L

Sources

• Section 21.35, Tag 08J7
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.RingedSite.derivedCurrySectionsEquiv · AlgebraicGeometry.RingedSite.derivedCurrySectionsEquiv_restriction · AlgebraicGeometry.RingedSite.derivedCurrySectionsEquiv_naturality_source · AlgebraicGeometry.RingedSite.derivedCurryHomEquiv · AlgebraicGeometry.RingedSite.derivedCurryHomEquiv_apply · AlgebraicGeometry.RingedSite.derivedCurryHomEquiv_naturality · AlgebraicGeometry.RingedSite.derivedCurryHomEquiv_dinaturality · AlgebraicGeometry.RingedSite.derivedCurryHomEquiv_naturality_source

Section21.36 Global derived hom#

Section 21.36 of the Stacks Project, Tag 0B6E. 1 tag here is carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0B6E, the section

Tag 0B6E in the Stacks Project.

AlgebraicGeometry.RingedSite.globalDerivedHomModules, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/GlobalDerivedHom.lean, line 312. The attribute's comment: “the global derived hom RHom_O(K, L) = RΓ(C, RHom(K, L)) in D(Γ(C, O))”.

Stacks 0B6E. Applying the construction of the internal hom in the derived category we get the object RHom_O(K, L) = RΓ(C, RHom(K, L)) in D(Γ(C, O)): the derived internal Hom of two objects of D(O), followed by derived global sections valued in modules over the ring of global sections of the structure sheaf.

def globalDerivedHomModules :
    (DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))ᵒᵖ ⥤
      DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ⥤
        DerivedCategory
          (ModuleCat.{u} (GlobalSectionRing (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))

AlgebraicGeometry.RingedSite.globalDerivedHomModulesDegreeZeroEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/GlobalDerivedHom.lean, line 355. The attribute's comment: “the degree-zero cohomology of RHom_O(K, L) is Hom_{D(O)}(K, L)”.

Stacks 0B6E, the cohomology of the global derived hom. The degree-zero cohomology of RHom_O(K, L) is the group of morphisms K ⟶ L in D(O). This is Stacks 08JA, which is the statement the source cites for the cohomology modules of the global derived hom, transported to RHom_O(K, L) of D(Γ(C, O)) along AlgebraicGeometry.RingedSite.derivedGlobalSectionsModulesForget; the cohomology is read on the underlying complex of abelian groups, as Stacks 08JA states it.

def globalDerivedHomModulesDegreeZeroEquiv
    (K L : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
    ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} 0).obj
        ((underlyingDerivedGroup X).obj
          (((globalDerivedHomModules X).obj (op K)).obj L)) : Type u) ≃+ (K ⟶ L)

AlgebraicGeometry.RingedSite.globalDerivedHomDegreeEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/GlobalDerivedHomShift.lean, line 186. The attribute's comment: “the degree-n cohomology of RHom_O(K, L) is Hom_{D(O)}(K, L[n])”.

Stacks 0B6E, the cohomology of the global derived hom in every degree. The degree-n cohomology of RHom_O(K, L) is the group of morphisms K ⟶ L[n] in D(O), that is the Ext-group Ext^n_{D(O)}(K, L). This is the abelian-group-valued reading AlgebraicGeometry.RingedSite.globalDerivedHom of the global derived hom.

The degree is moved into the covariant variable: the homology functors of the derived category form a shift sequence, derived global sections commute with the translation, and the derived internal Hom commutes with the translation in its covariant variable by AlgebraicGeometry.RingedSite.derivedSheafHomTargetShiftIso; in degree zero the cohomology is the morphism group by Stacks 08JA, which is AlgebraicGeometry.RingedSite.derivedSheafHomGlobalSectionsEquiv.

def globalDerivedHomDegreeEquiv
    (K L : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (n : ℤ) :
    ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} n).obj
        (((globalDerivedHom X).obj (op K)).obj L) : Type u) ≃+ (K ⟶ L⟦n⟧)

AlgebraicGeometry.RingedSite.globalDerivedHomModulesDegreeEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/GlobalDerivedHomShift.lean, line 211. The attribute's comment: “the degree-n cohomology of RHom_O(K, L) in D(Γ(C, O)) is Hom_{D(O)}(K, L[n])”.

Stacks 0B6E, the cohomology of the global derived hom in every degree, for the D(Γ(C, O))-valued global derived hom AlgebraicGeometry.RingedSite.globalDerivedHomModules: the degree-n cohomology of RHom_O(K, L), read on the underlying complex of abelian groups as Stacks 08JA states it, is the group of morphisms K ⟶ L[n] of D(O).

This is AlgebraicGeometry.RingedSite.globalDerivedHomDegreeEquiv transported along AlgebraicGeometry.RingedSite.derivedGlobalSectionsModulesForget, and it is the degree-n form of AlgebraicGeometry.RingedSite.globalDerivedHomModulesDegreeZeroEquiv.

def globalDerivedHomModulesDegreeEquiv
    (K L : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (n : ℤ) :
    ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} n).obj
        ((underlyingDerivedGroup X).obj
          (((globalDerivedHomModules X).obj (op K)).obj L)) : Type u) ≃+ (K ⟶ L⟦n⟧)

AlgebraicGeometry.RingedSite.derivedStructureSheafGlobalSectionsDegreeEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/StructureSheafHypercohomology.lean, line 72. The attribute's comment: “the case K = O[0], where RHom_O(O[0], Z) is RGamma(C, Z)”.

Hypercohomology in every degree is morphisms out of the structure sheaf. For an object Z of D(O) the hypercohomology group H^n(C, Z), the degree-n homology of unbounded derived global sections, is the group Hom_{D(O)}(O[0], Z[n]).

This is Tag 08JA at source the structure sheaf in every degree: derived global sections of the identification RSheafHom(O[0], Z) ≅ Z of AlgebraicGeometry.RingedSite.derivedStructureSheafHomIso turn H^n(C, Z) into the degree-n cohomology of the global derived hom RHom_O(O[0], Z), which is Hom(O[0], Z[n]) by Tag 0B6E (AlgebraicGeometry.RingedSite.globalDerivedHomDegreeEquiv). In degree zero it is AlgebraicGeometry.RingedSite.derivedStructureSheafGlobalSectionsEquiv.

def derivedStructureSheafGlobalSectionsDegreeEquiv
    (Z : DerivedCategory (SheafOfModules.{u} (ringSheaf X.O))) (n : ℤ) :
    ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} n).obj
        ((derivedModuleGlobalSections X).obj Z) : Type u) ≃+
      (derivedStructureSheaf X ⟶ Z⟦n⟧)

Sources

• Section 21.36, Tag 0B6E
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.RingedSite.globalDerivedHomModules · AlgebraicGeometry.RingedSite.globalDerivedHomModulesDegreeZeroEquiv · AlgebraicGeometry.RingedSite.globalDerivedHomDegreeEquiv · AlgebraicGeometry.RingedSite.globalDerivedHomModulesDegreeEquiv · AlgebraicGeometry.RingedSite.derivedStructureSheafGlobalSectionsDegreeEquiv

Section21.37 Derived lower shriek#

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

Tag 0D6X, a lemma

Tag 0D6X in the Stacks Project.

AlgebraicGeometry.Stack.subsiteSliceCohomology_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteAcyclicity.lean, line 153. The attribute's comment: “for the inclusion of a full subsite of the site of Stacks 06TP, localized at an object of the subsite”.

Stacks 0D6X for a slice of the inclusion of a full subsite. Let P cut out a full subcategory of the objects of a category fibred in groupoids over the big fppf category of S, let x be an object of P, and suppose the covering morphisms of the slice at x of the subsite admit the fibre products of Stacks 00WV, preserved by the slice functor. Then the restriction along that functor of an injective abelian sheaf on the slice of the ambient site at x has vanishing cohomology in positive degrees.

Cohomology over x is the global cohomology of the slice at x, which is cohomology over the terminal object id : x ⟶ x of that slice. The coefficient universe is the join of the two universes of the site, which is where the sheaves on these slices live and which is what Stacks.CechSite.injective_sheaf_subsingleton_sheafH_of_functor allows, neither site being small.

theorem subsiteSliceCohomology_eq_zero (hp : p.IsFiberedInGroupoids)
    (τ : GrothendieckTopology B.Schemes) (P : ObjectProperty X)
    [P.ι.IsContinuous (subsiteTopology B S hS p τ P) (associatedTopology B S hS p τ)]
    (x : P.FullSubcategory)
    [Stacks.Sites.PreservesCoveringPullbacks ((subsiteTopology B S hS p τ P).over x)
      (Over.post (X := x) P.ι)]
    (I : Sheaf ((associatedTopology B S hS p τ).over (P.ι.obj x)) AddCommGrpCat.{max v w})
    [Injective I] (n : ℕ)
    (a : Sheaf.H ((subsiteSliceRestriction B S hS p τ P x).obj I) (n + 1)) : a = 0

AlgebraicGeometry.Stack.FlatFppf.sliceAcyclic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteAcyclicity.lean, line 260. The attribute's comment: “for the inclusion of the flat-fppf site of Stacks 0787, localized at a flat object”.

Stacks 0D6X for the inclusion of the flat-fppf site, localized at a flat object. The restriction to the slice at x of the flat-fppf site of an injective abelian sheaf on the slice at x of the fppf site of an algebraic stack has vanishing cohomology in positive degrees.

This is the hypothesis hacyclic of AlgebraicGeometry.Stack.FlatFppf.cohomologyOverObjectIso, part (2)(b) of Stacks 0GR0.

theorem sliceAcyclic (x : ObjectProperty.FullSubcategory (objectProperty B S hS 𝒳)) :
    haveI := isContinuous_inclusion B S hS 𝒳 (closedUnderFlatMorphisms B S hS 𝒳)
    ∀ I : Sheaf ((fppfTopology B S hS 𝒳).over ((objectProperty B S hS 𝒳).ι.obj x))
        AddCommGrpCat.{u + 1}, Injective I → ∀ (n : ℕ)
      (a : Sheaf.H ((subsiteSliceRestriction B S hS 𝒳.val.val.p B.topology
        (objectProperty B S hS 𝒳) x).obj I) (n + 1)), a = 0

AlgebraicGeometry.Stack.LisseEtale.sliceAcyclic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteAcyclicity.lean, line 327. The attribute's comment: “for the inclusion of the lisse-étale site of Stacks 0787, localized at a smooth object”.

Stacks 0D6X for the inclusion of the lisse-étale site, localized at a smooth object. The restriction to the slice at x of the lisse-étale site of an injective abelian sheaf on the slice at x of the étale site of an algebraic stack has vanishing cohomology in positive degrees.

This is the hypothesis hacyclic of AlgebraicGeometry.Stack.LisseEtale.cohomologyOverObjectIso, part (1)(b) of Stacks 0GR0.

theorem sliceAcyclic (x : ObjectProperty.FullSubcategory (smoothObject.{u, w} B S hS 𝒳)) :
    haveI := isContinuous_inclusion B S hS 𝒳 (closedUnderSmoothMorphisms.{u, w} B S hS 𝒳)
    ∀ I : Sheaf ((associatedTopology B S hS 𝒳.val.val.p (etaleTopology B)).over
        ((smoothObject.{u, w} B S hS 𝒳).ι.obj x)) AddCommGrpCat.{u + 1},
        Injective I → ∀ (n : ℕ)
      (a : Sheaf.H ((subsiteSliceRestriction B S hS 𝒳.val.val.p (etaleTopology B)
        (smoothObject.{u, w} B S hS 𝒳) x).obj I) (n + 1)), a = 0

AlgebraicGeometry.Stack.subsiteObjectCohomology_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteCohomologyComparison.lean, line 234. The attribute's comment: “for the inclusion of a full subsite of the site of Stacks 06TP, over an object of the subsite”.

Stacks 0D6X for the inclusion of a full subsite, over an object of the subsite. Let P cut out a full subcategory of the objects of a category fibred in groupoids over the big fppf category of S, and suppose the covering morphisms of the subsite admit the fibre products of Stacks 00WV, preserved by the inclusion. Then for every object x of the subsite the restriction along the inclusion of an injective abelian sheaf on the ambient site has vanishing cohomology over x in positive degrees.

Cohomology over x is Ext out of the free abelian sheaf on the representable presheaf of x, lifted to the coefficient universe, which is CategoryTheory.extensionByZeroUnitAb. The coefficient universe is the join of the two universes of the site, which is where the sheaves on these sites live and which is what Stacks.CechSite.injective_sheaf_subsingleton_ext_of_functor allows, neither site being small.

theorem subsiteObjectCohomology_eq_zero (hp : p.IsFiberedInGroupoids)
    (τ : GrothendieckTopology B.Schemes) (P : ObjectProperty X)
    [P.ι.IsContinuous (subsiteTopology B S hS p τ P) (associatedTopology B S hS p τ)]
    [Stacks.Sites.PreservesCoveringPullbacks (subsiteTopology B S hS p τ P) P.ι]
    (I : Sheaf (associatedTopology B S hS p τ) AddCommGrpCat.{max v w}) [Injective I]
    (x : P.FullSubcategory) (n : ℕ)
    (a : Ext (extensionByZeroUnitAb.{max v w} (subsiteTopology B S hS p τ P) x)
      ((subsiteRestriction B S hS p τ P).obj I) (n + 1)) :
    a = 0

AlgebraicGeometry.Stack.FlatFppf.objectAcyclic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteCohomologyComparison.lean, line 301. The attribute's comment: “for the inclusion of the flat-fppf site of Stacks 0787, over a flat object”.

Stacks 0D6X for the inclusion of the flat-fppf site, over a flat object. The restriction to the flat-fppf site of an injective abelian sheaf on the fppf site of an algebraic stack has vanishing cohomology over every flat object in positive degrees.

theorem objectAcyclic :
    haveI := isContinuous_inclusion B S hS 𝒳 (closedUnderFlatMorphisms B S hS 𝒳)
    ∀ I : Sheaf (fppfTopology B S hS 𝒳) AddCommGrpCat.{u + 1}, Injective I →
      ∀ (x : ObjectProperty.FullSubcategory (objectProperty B S hS 𝒳)) (n : ℕ)
      (a : Ext (extensionByZeroUnitAb.{u + 1} (inclusionTopology B S hS 𝒳) x)
        ((subsiteRestriction B S hS 𝒳.val.val.p B.topology
          (objectProperty B S hS 𝒳)).obj I) (n + 1)), a = 0

AlgebraicGeometry.Stack.LisseEtale.objectAcyclic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteCohomologyComparison.lean, line 420. The attribute's comment: “for the inclusion of the lisse-étale site of Stacks 0787, over a smooth object”.

Stacks 0D6X for the inclusion of the lisse-étale site, over a smooth object. The restriction to the lisse-étale site of an injective abelian sheaf on the étale site of an algebraic stack has vanishing cohomology over every smooth object in positive degrees.

theorem objectAcyclic :
    haveI := isContinuous_inclusion B S hS 𝒳 (closedUnderSmoothMorphisms.{u, w} B S hS 𝒳)
    ∀ I : Sheaf (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
        AddCommGrpCat.{u + 1}, Injective I →
      ∀ (x : ObjectProperty.FullSubcategory (smoothObject.{u, w} B S hS 𝒳)) (n : ℕ)
      (a : Ext (extensionByZeroUnitAb.{u + 1} (inclusionTopology.{u, w} B S hS 𝒳) x)
        ((subsiteRestriction B S hS 𝒳.val.val.p (etaleTopology B)
          (smoothObject.{u, w} B S hS 𝒳)).obj I) (n + 1)), a = 0

AlgebraicGeometry.Stack.subsiteGlobalCohomology_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteTerminalCohomology.lean, line 55. The attribute's comment: “for the inclusion of a full subsite of the site of Stacks 06TP, for the global cohomology of a subsite with a terminal object”.

Vanishing of the global cohomology of a restricted injective sheaf. Let P cut out a full subcategory of the objects of a category fibred in groupoids over the big fppf category of S, suppose the covering morphisms of the subsite admit the fibre products of Stacks 00WV, preserved by the inclusion, and suppose the subsite has a terminal object. Then the restriction along the inclusion of an injective abelian sheaf on the ambient site has vanishing global cohomology CategoryTheory.Sheaf.H in positive degrees.

theorem subsiteGlobalCohomology_eq_zero (hp : p.IsFiberedInGroupoids)
    (τ : GrothendieckTopology B.Schemes) (P : ObjectProperty X)
    [P.ι.IsContinuous (subsiteTopology B S hS p τ P) (associatedTopology B S hS p τ)]
    [Stacks.Sites.PreservesCoveringPullbacks (subsiteTopology B S hS p τ P) P.ι]
    {e : P.FullSubcategory} (he : IsTerminal e)
    (I : Sheaf (associatedTopology B S hS p τ) AddCommGrpCat.{max v w}) [Injective I]
    (n : ℕ) (a : Sheaf.H ((subsiteRestriction B S hS p τ P).obj I) (n + 1)) :
    a = 0

Stacks.CechSite.injective_module_subsingleton_ext_of_continuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Cech/VanishingAlongAContinuousFunctor.lean, line 221. The attribute's comment: “the Čech comparison derived from continuity; cocontinuity is not needed, neither site is small, and cohomology over U is Ext out of the free abelian sheaf on the lifted representable”.

Stacks Project, Tag 0D6X. Let u : C ⥤ D be a continuous functor of sites and let g : Sh(C) → Sh(D) be the corresponding morphism of topoi, so that g⁻¹ is restriction along u (Sites, Lemma 00XR). Let O_D be a sheaf of rings on D and let I be an injective O_D-module. Then H^p(U, g⁻¹I) = 0 for all p > 0 and all objects U of C.

Continuity of u (Sites, Definition 00WV) is CategoryTheory.Functor.IsContinuous together with its covering-pullback clause Stacks.Sites.PreservesCoveringPullbacks, and the identification of Čech complexes Ȟ^p(𝒰, g⁻¹I) = Ȟ^p(u(𝒰), I) of the source's proof is derived from it, by isIso_cechProductMapOfFunctor_of_continuityCovering. Cohomology over U is Ext out of the free abelian sheaf on the (lifted) representable presheaf of U, and the cohomology of a module is that of its underlying abelian sheaf. Cocontinuity of u, which makes g a morphism of topoi, is not needed. Neither site is assumed small; the universes of the two sites, of the sections of O_D and of Ext are free.

theorem injective_module_subsingleton_ext_of_continuous
    (I : SheafOfModules.{max a u v u₂ v₂ r} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))
    [Injective I] (U : C) (p : ℕ) (hp : 0 < p) :
    Subsingleton (Ext ((presheafToSheaf J AddCommGrpCat.{max a u v u₂ v₂ r}).obj
      (uliftYoneda.{max a u v u₂ v₂ r}.obj U ⋙ AddCommGrpCat.free))
      ((u.sheafPushforwardContinuous AddCommGrpCat.{max a u v u₂ v₂ r} J Y.J).obj
        ((SheafOfModules.toSheaf (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)).obj I)) p)

Stacks.CechSite.injective_module_sheafCohomology_isZero_of_functor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Cech/VanishingAlongAFunctor.lean, line 297.

Stacks Project, Tag 0D6X. Let u : C ⥤ D be a continuous functor of sites and let g : Sh(C) → Sh(D) be the corresponding morphism of topoi, so that g⁻¹ is restriction along u by Sites, Lemma 00XR. Let O_D be a sheaf of rings on D and let I be an injective O_D-module. Then H^p(U, g⁻¹I) = 0 for all p > 0 and every object U of the cofinal system of coverings, in particular for every object of C when the system is cofinal everywhere. As in the source, the cohomology of a module is that of its underlying abelian sheaf.

theorem injective_module_sheafCohomology_isZero_of_functor
    (hCovObjects : ∀ {U : C}
      (E : { E : PreZeroHypercover.{w} U // E.sieve₀ ∈ J U }) (hE : E ∈ Cov U),
      U ∈ B ∧ (∀ i, E.1.X i ∈ B) ∧
        ∀ (p : ℕ) (i : Fin (p + 1) → E.1.I₀),
          letI : ∀ (q : ℕ) (j : Fin (q + 1) → E.1.I₀),
            HasProduct (fun a ↦ Over.mk (E.1.f (j a))) := hProducts E hE
          (∏ᶜ (fun a ↦ Over.mk (E.1.f (i a)))).left ∈ B)
    (hCovCofinal : ∀ U ∈ B, ∀ R ∈ J U,
      ∃ (E : { E : PreZeroHypercover.{w} U // E.sieve₀ ∈ J U }),
        E ∈ Cov U ∧ E.1.sieve₀ ≤ R)
    (hComparison : ∀ {U : C}
      (E : { E : PreZeroHypercover.{w} U // E.sieve₀ ∈ J U }) (hE : E ∈ Cov U)
      (p : ℕ) (i : Fin (p + 1) → E.1.I₀),
        letI : ∀ (q : ℕ) (j : Fin (q + 1) → E.1.I₀),
          HasProduct (fun a ↦ Over.mk (E.1.f (j a))) := hProducts E hE
        letI : ∀ (q : ℕ) (j : Fin (q + 1) → (E.1.map u).I₀),
          HasProduct (fun a ↦ Over.mk ((E.1.map u).f (j a))) := hImageProducts E hE
        IsIso (cechProductMapOfFunctor u E.1 p i))
    (I : SheafOfModules.{max a u₂ v₂ r w} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))
    [Injective I]
    (U : C) (hU : U ∈ B) (p : ℕ) (hp : 0 < p) :
    IsZero (Sheaf.H' ((u.sheafPushforwardContinuous AddCommGrpCat.{max a u₂ v₂ r w} J Y.J).obj
      ((SheafOfModules.toSheaf (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)).obj I)) p U)

Stacks.CechSite.injective_module_sheafCohomology_isZero_of_functor_sheafOfRings, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Cech/VanishingAlongAFunctor.lean, line 366.

Stacks Project, Tag 0D6X. Let u : C ⥤ D be a continuous functor of sites and let g : Sh(C) → Sh(D) be the corresponding morphism of topoi, so that g⁻¹ is restriction along u by Sites, Lemma 00XR. Let O_D be a sheaf of rings on D and let I be an injective O_D-module. Then H^p(U, g⁻¹I) = 0 for all p > 0 and every object U of the cofinal system of coverings, in particular for every object of C when the system is cofinal everywhere. As in the source, the cohomology of a module is that of its underlying abelian sheaf.

theorem injective_module_sheafCohomology_isZero_of_functor_sheafOfRings
    (hCovObjects : ∀ {U : C}
      (E : { E : PreZeroHypercover.{w} U // E.sieve₀ ∈ J U }) (hE : E ∈ Cov U),
      U ∈ B ∧ (∀ i, E.1.X i ∈ B) ∧
        ∀ (p : ℕ) (i : Fin (p + 1) → E.1.I₀),
          letI : ∀ (q : ℕ) (j : Fin (q + 1) → E.1.I₀),
            HasProduct (fun a ↦ Over.mk (E.1.f (j a))) := hProducts E hE
          (∏ᶜ (fun a ↦ Over.mk (E.1.f (i a)))).left ∈ B)
    (hCovCofinal : ∀ U ∈ B, ∀ R ∈ J U,
      ∃ (E : { E : PreZeroHypercover.{w} U // E.sieve₀ ∈ J U }),
        E ∈ Cov U ∧ E.1.sieve₀ ≤ R)
    (hComparison : ∀ {U : C}
      (E : { E : PreZeroHypercover.{w} U // E.sieve₀ ∈ J U }) (hE : E ∈ Cov U)
      (p : ℕ) (i : Fin (p + 1) → E.1.I₀),
        letI : ∀ (q : ℕ) (j : Fin (q + 1) → E.1.I₀),
          HasProduct (fun a ↦ Over.mk (E.1.f (j a))) := hProducts E hE
        letI : ∀ (q : ℕ) (j : Fin (q + 1) → (E.1.map u).I₀),
          HasProduct (fun a ↦ Over.mk ((E.1.map u).f (j a))) := hImageProducts E hE
        IsIso (cechProductMapOfFunctor u E.1 p i))
    (I : SheafOfModules.{max a u₂ v₂ r w} O) [Injective I]
    (U : C) (hU : U ∈ B) (p : ℕ) (hp : 0 < p) :
    IsZero (Sheaf.H' ((u.sheafPushforwardContinuous AddCommGrpCat.{max a u₂ v₂ r w} J K).obj
      ((SheafOfModules.toSheaf O).obj I)) p U)

Stacks.CechSite.injective_module_subsingleton_ext_of_functor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Cech/VanishingAlongAFunctorEssentiallySmall.lean, line 452. The attribute's comment: “the morphism universes of the two sites are free and the sites are not assumed small; the coefficient universe contains their objects, and cohomology over an object is Ext out of the free abelian sheaf on the lifted representable”.

Stacks Project, Tag 0D6X, with the morphism universes free. Let u : C ⥤ D be a continuous functor of sites and let g : Sh(C) → Sh(D) be the corresponding morphism of topoi, so that g⁻¹ is restriction along u by Sites, Lemma 00XR. Let O_D be a sheaf of rings on D and let I be an injective O_D-module. Then H^p(U, g⁻¹I) = 0 for all p > 0 and every object U of the cofinal system of coverings, in particular for every object of C when the system is cofinal everywhere. As in the source, the cohomology of a module is that of its underlying abelian sheaf.

Neither site is assumed small, and the morphism universes of the two sites are unrelated to the coefficient universe, which need only contain them and the objects.

theorem injective_module_subsingleton_ext_of_functor
    (hCovObjects : ∀ {U : C}
      (E : { E : PreZeroHypercover.{w} U // E.sieve₀ ∈ J U }) (hE : E ∈ Cov U),
      U ∈ B ∧ (∀ i, E.1.X i ∈ B) ∧
        ∀ (p : ℕ) (i : Fin (p + 1) → E.1.I₀),
          letI : ∀ (q : ℕ) (j : Fin (q + 1) → E.1.I₀),
            HasProduct (fun a ↦ Over.mk (E.1.f (j a))) := hProducts E hE
          (∏ᶜ (fun a ↦ Over.mk (E.1.f (i a)))).left ∈ B)
    (hCovCofinal : ∀ U ∈ B, ∀ R ∈ J U,
      ∃ (E : { E : PreZeroHypercover.{w} U // E.sieve₀ ∈ J U }),
        E ∈ Cov U ∧ E.1.sieve₀ ≤ R)
    (hComparison : ∀ {U : C}
      (E : { E : PreZeroHypercover.{w} U // E.sieve₀ ∈ J U }) (hE : E ∈ Cov U)
      (p : ℕ) (i : Fin (p + 1) → E.1.I₀),
        letI : ∀ (q : ℕ) (j : Fin (q + 1) → E.1.I₀),
          HasProduct (fun a ↦ Over.mk (E.1.f (j a))) := hProducts E hE
        letI : ∀ (q : ℕ) (j : Fin (q + 1) → (E.1.map u).I₀),
          HasProduct (fun a ↦ Over.mk ((E.1.map u).f (j a))) := hImageProducts E hE
        IsIso (cechProductMapOfFunctor u E.1 p i))
    (I : SheafOfModules.{max a u v u₂ v₂ r w} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))
    [Injective I]
    (U : C) (hU : U ∈ B) (p : ℕ) (hp : 0 < p) :
    Subsingleton (Ext ((presheafToSheaf J AddCommGrpCat.{max a u v u₂ v₂ r w}).obj
      (uliftYoneda.{max a u v u₂ v₂ r w}.obj U ⋙ AddCommGrpCat.free))
      ((u.sheafPushforwardContinuous AddCommGrpCat.{max a u v u₂ v₂ r w} J Y.J).obj
        ((SheafOfModules.toSheaf (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)).obj I)) p)

Stacks.CechSite.injective_module_subsingleton_ext_of_functor_sheafOfRings, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Cech/VanishingAlongAFunctorEssentiallySmall.lean, line 526. The attribute's comment: “the morphism universes of the two sites are free and the sites are not assumed small; the coefficient universe contains their objects, and cohomology over an object is Ext out of the free abelian sheaf on the lifted representable”.

Stacks Project, Tag 0D6X, with the morphism universes free. Let u : C ⥤ D be a continuous functor of sites and let g : Sh(C) → Sh(D) be the corresponding morphism of topoi, so that g⁻¹ is restriction along u by Sites, Lemma 00XR. Let O_D be a sheaf of rings on D and let I be an injective O_D-module. Then H^p(U, g⁻¹I) = 0 for all p > 0 and every object U of the cofinal system of coverings, in particular for every object of C when the system is cofinal everywhere. As in the source, the cohomology of a module is that of its underlying abelian sheaf.

Neither site is assumed small, and the morphism universes of the two sites are unrelated to the coefficient universe, which need only contain them and the objects.

theorem injective_module_subsingleton_ext_of_functor_sheafOfRings
    (hCovObjects : ∀ {U : C}
      (E : { E : PreZeroHypercover.{w} U // E.sieve₀ ∈ J U }) (hE : E ∈ Cov U),
      U ∈ B ∧ (∀ i, E.1.X i ∈ B) ∧
        ∀ (p : ℕ) (i : Fin (p + 1) → E.1.I₀),
          letI : ∀ (q : ℕ) (j : Fin (q + 1) → E.1.I₀),
            HasProduct (fun a ↦ Over.mk (E.1.f (j a))) := hProducts E hE
          (∏ᶜ (fun a ↦ Over.mk (E.1.f (i a)))).left ∈ B)
    (hCovCofinal : ∀ U ∈ B, ∀ R ∈ J U,
      ∃ (E : { E : PreZeroHypercover.{w} U // E.sieve₀ ∈ J U }),
        E ∈ Cov U ∧ E.1.sieve₀ ≤ R)
    (hComparison : ∀ {U : C}
      (E : { E : PreZeroHypercover.{w} U // E.sieve₀ ∈ J U }) (hE : E ∈ Cov U)
      (p : ℕ) (i : Fin (p + 1) → E.1.I₀),
        letI : ∀ (q : ℕ) (j : Fin (q + 1) → E.1.I₀),
          HasProduct (fun a ↦ Over.mk (E.1.f (j a))) := hProducts E hE
        letI : ∀ (q : ℕ) (j : Fin (q + 1) → (E.1.map u).I₀),
          HasProduct (fun a ↦ Over.mk ((E.1.map u).f (j a))) := hImageProducts E hE
        IsIso (cechProductMapOfFunctor u E.1 p i))
    (I : SheafOfModules.{max a u v u₂ v₂ r w} O) [Injective I]
    (U : C) (hU : U ∈ B) (p : ℕ) (hp : 0 < p) :
    Subsingleton (Ext ((presheafToSheaf J AddCommGrpCat.{max a u v u₂ v₂ r w}).obj
      (uliftYoneda.{max a u v u₂ v₂ r w}.obj U ⋙ AddCommGrpCat.free))
      ((u.sheafPushforwardContinuous AddCommGrpCat.{max a u v u₂ v₂ r w} J K).obj
        ((SheafOfModules.toSheaf O).obj I)) p)

Stacks.CechSite.injective_sheaf_subsingleton_sheafH_of_functor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Cech/VanishingAlongAFunctorEssentiallySmall.lean, line 704. The attribute's comment: “global cohomology of the source site, at a terminal object; the morphism universes of the two sites are free and the sites are not assumed small”.

Stacks Project, Tag 0D6X for the global cohomology of the source site. Let u : C ⥤ D be a continuous functor of sites, let g : Sh(C) → Sh(D) be the corresponding morphism of topoi and let e be a terminal object of C belonging to the cofinal system of coverings. If I is an injective abelian sheaf on D then the global cohomology H^p(C, g⁻¹I) vanishes for p > 0.

This is the form in which the acyclicity hypothesis of Stacks 07AK is stated: the cohomology over an object of a site is the global cohomology of the slice at that object, and the slice has a terminal object.

theorem injective_sheaf_subsingleton_sheafH_of_functor
    (hCovObjects : ∀ {U : C}
      (E : { E : PreZeroHypercover.{w} U // E.sieve₀ ∈ J U }) (hE : E ∈ Cov U),
      U ∈ B ∧ (∀ i, E.1.X i ∈ B) ∧
        ∀ (p : ℕ) (i : Fin (p + 1) → E.1.I₀),
          letI : ∀ (q : ℕ) (j : Fin (q + 1) → E.1.I₀),
            HasProduct (fun a ↦ Over.mk (E.1.f (j a))) := hProducts E hE
          (∏ᶜ (fun a ↦ Over.mk (E.1.f (i a)))).left ∈ B)
    (hCovCofinal : ∀ U ∈ B, ∀ R ∈ J U,
      ∃ (E : { E : PreZeroHypercover.{w} U // E.sieve₀ ∈ J U }),
        E ∈ Cov U ∧ E.1.sieve₀ ≤ R)
    (hComparison : ∀ {U : C}
      (E : { E : PreZeroHypercover.{w} U // E.sieve₀ ∈ J U }) (hE : E ∈ Cov U)
      (p : ℕ) (i : Fin (p + 1) → E.1.I₀),
        letI : ∀ (q : ℕ) (j : Fin (q + 1) → E.1.I₀),
          HasProduct (fun a ↦ Over.mk (E.1.f (j a))) := hProducts E hE
        letI : ∀ (q : ℕ) (j : Fin (q + 1) → (E.1.map u).I₀),
          HasProduct (fun a ↦ Over.mk ((E.1.map u).f (j a))) := hImageProducts E hE
        IsIso (cechProductMapOfFunctor u E.1 p i))
    (I : Sheaf K AddCommGrpCat.{max a u v u₂ v₂ w}) [Injective I]
    {e : C} (he : IsTerminal e) (heB : e ∈ B) (p : ℕ) (hp : 0 < p) :
    Subsingleton (Sheaf.H
      ((u.sheafPushforwardContinuous AddCommGrpCat.{max a u v u₂ v₂ w} J K).obj I) p)

Tag 07AC, a lemma

Tag 07AC in the Stacks Project.

Stacks.Cohomology.DerivedLowerShriek.derivedLowerShriek_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LowerShriek/ModuleDerivedLowerShriek.lean, line 369.

Stacks 07AC. Let u : C ⥤ D be a continuous and cocontinuous functor of sites, let g : Sh(C) ⟶ Sh(D) be the corresponding morphism of topoi, let O_D be a sheaf of rings on D and set O_C = g^{-1} O_D. Then the functor g_! : Mod(O_C) ⥤ Mod(O_D) of Stacks 0797 has a left derived functor Lg_! : D(O_C) ⥤ D(O_D), which is left adjoint to g^*, and for every object U of C

Lg_!(j_{U!} O_U) = g_! j_{U!} O_U = j_{u(U)!} O_{u(U)}.

Continuity of u in the sense of the source (Stacks 00WV) is Functor.IsContinuous together with its covering-pullback clause Stacks.Sites.PreservesCoveringPullbacks. The derived functor is derivedLowerShriek, the total left derived functor of SheafOfModules.pullback along the identity of O_C, which is the lower shriek of Stacks 0797 up to the canonical isomorphism Stacks.SheafOfModules.lowerShriekIsoPullback; g^* on derived categories is derivedRestriction, induced by the exact restriction functor.

theorem derivedLowerShriek_spec :
    (lowerShriekOnHomotopy J K f (Stacks.SheafOfModules.Tensor.ringSheaf (targetRingedSite K O).O) ⋙
        DerivedCategory.Qh).HasPointwiseLeftDerivedFunctor
      (sourceQuasiIso J K f (Stacks.SheafOfModules.Tensor.ringSheaf (targetRingedSite K O).O)) ∧
    (derivedLowerShriek J K f
      (Stacks.SheafOfModules.Tensor.ringSheaf (targetRingedSite K O).O)).IsLeftDerivedFunctor
      (derivedLowerShriekComparison J K f
        (Stacks.SheafOfModules.Tensor.ringSheaf (targetRingedSite K O).O))
      (sourceQuasiIso J K f (Stacks.SheafOfModules.Tensor.ringSheaf (targetRingedSite K O).O)) ∧
    Nonempty (derivedLowerShriek J K f
      (Stacks.SheafOfModules.Tensor.ringSheaf (targetRingedSite K O).O) ⊣
      derivedRestriction J K f (Stacks.SheafOfModules.Tensor.ringSheaf (targetRingedSite K O).O)) ∧
    ∀ U : C,
      Nonempty ((derivedLowerShriek J K f
        (Stacks.SheafOfModules.Tensor.ringSheaf (targetRingedSite K O).O)).obj
          ((DerivedCategory.singleFunctor _ 0).obj (extensionByZeroUnit
            (inverseImageRing J K f
              (Stacks.SheafOfModules.Tensor.ringSheaf (targetRingedSite K O).O)) U)) ≅
        (DerivedCategory.singleFunctor _ 0).obj
          ((Stacks.SheafOfModules.lowerShriek.{u} J K f
            (Stacks.SheafOfModules.Tensor.ringSheaf (targetRingedSite K O).O)).obj
            (extensionByZeroUnit (inverseImageRing J K f
              (Stacks.SheafOfModules.Tensor.ringSheaf (targetRingedSite K O).O)) U))) ∧
      Nonempty ((Stacks.SheafOfModules.lowerShriek.{u} J K f
        (Stacks.SheafOfModules.Tensor.ringSheaf (targetRingedSite K O).O)).obj
          (extensionByZeroUnit (inverseImageRing J K f
            (Stacks.SheafOfModules.Tensor.ringSheaf (targetRingedSite K O).O)) U) ≅
        extensionByZeroUnit
          (Stacks.SheafOfModules.Tensor.ringSheaf (targetRingedSite K O).O) (f.obj U))

Stacks.Cohomology.DerivedLowerShriek.pullbackExtensionByZeroUnitIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LowerShriek/PullbackExtensionByZeroUnit.lean, line 100. The attribute's comment: “the second equality of the displayed chain, g_! j_{U!} O_U = j_{u(U)!} O_{u(U)}, on sheaves of modules, for an arbitrary structure morphism of sheaves of rings O' ⟶ u_* O and for the sheafified-free spelling of the extensions by zero. The first equality and the existence and adjointness of Lg_! are NOT covered: no unbounded total left derived functor of the module-level g_! is constructed in this library”.

g_! (j_{V!} O'_V) ≅ j_{u(V)!} O_{u(V)} for an arbitrary structure morphism of sheaves of rings. For a continuous functor of sites u : C ⥤ D, a sheaf of rings O on D, a sheaf of rings O' on C, any morphism phi : O' ⟶ u_* O whose module pushforward has a left adjoint, and every object V of C,

g_! (j_{V!} O'_V) ≅ j_{u(V)!} O_{u(V)},

where g_! = SheafOfModules.pullback phi and both extensions by zero are the sheafified free modules Stacks.SheafOfModules.extensionByZeroUnit.

def pullbackExtensionByZeroUnitIso (V : C) :
    (SheafOfModules.pullback.{max u₁ v₁ u₂ v₂ w t} phi).obj
        (Stacks.SheafOfModules.extensionByZeroUnit.{u₁, v₁, w, max u₂ v₂ t} O' V) ≅
      Stacks.SheafOfModules.extensionByZeroUnit.{u₂, v₂, w, max u₁ v₁ t} O (u.obj V)

Tag 07AE, a remark

Tag 07AE in the Stacks Project.

Stacks.SheafOfModules.lowerShriekForget_not_isomorphic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LowerShriekForget.lean, line 448. The attribute's comment: “underived noncommutation”.

The lower shriek of modules may differ, even as an abelian sheaf, from lower shriek of the underlying abelian sheaf.

theorem lowerShriekForget_not_isomorphic :
    ∃ (J : GrothendieckTopology PUnit) (K : GrothendieckTopology Bool)
      (F : PUnit ⥤ Bool) (R : Sheaf K RingCat.{0})
      (hF : F.IsContinuous J K) (_hFc : F.IsCocontinuous J K),
      letI : F.IsContinuous J K := hF
      let S : Sheaf J RingCat.{0} :=
        (F.sheafPushforwardContinuous RingCat.{0} J K).obj R
      let φ : S ⟶ (F.sheafPushforwardContinuous RingCat.{0} J K).obj R := 𝟙 S
      ∃ (hAb : (F.sheafPushforwardContinuous AddCommGrpCat.{0} J K).IsRightAdjoint)
        (hMod : (SheafOfModules.pushforward.{0} φ).IsRightAdjoint),
      letI : (F.sheafPushforwardContinuous AddCommGrpCat.{0} J K).IsRightAdjoint := hAb
      letI : (SheafOfModules.pushforward.{0} φ).IsRightAdjoint := hMod
      ∃ M : SheafOfModules.{0} S,
        ¬ Nonempty
          (((SheafOfModules.toSheaf.{0} S ⋙
              F.sheafPullback AddCommGrpCat.{0} J K).obj M) ≅
            ((SheafOfModules.pullback.{0} φ ⋙
              SheafOfModules.toSheaf.{0} R).obj M))

Stacks.Cohomology.DerivedLowerShriek.existsUnique_derivedForgetComparison_of_acyclic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LowerShriek/ForgetComparison.lean, line 218. The attribute's comment: “the comparison transformation Lg_!^{Ab} ∘ forget ⟶ forget ∘ Lg_!”.

The comparison transformation, conditional only on the acyclicity statement of Stacks 0794 for lower shriek: there is exactly one natural transformation Lg_!^{Ab} ∘ forget ⟶ forget ∘ Lg_! compatible with the counits of the two left derived functors and the comparison of Stacks 0798.

theorem existsUnique_derivedForgetComparison_of_acyclic [Small.{w} C]
    [∀ U : C, (_root_.SheafOfModules.pushforward.{w} (F := Over.forget U)
      (𝟙 ((inverseImageRing J K f O).over U) :
        (inverseImageRing J K f O).over U ⟶ (inverseImageRing J K f O).over U)).IsRightAdjoint]
    (hFP : ∀ (a : ℤ)
      (Lc : CochainComplex (_root_.SheafOfModules.{w} (inverseImageRing J K f O)) ℤ),
      Lc.IsStrictlyLE a →
      (∀ n, IsSumOfExtensionByZeroUnits (inverseImageRing J K f O) (Lc.X n)) → Lc.Acyclic →
      (((lowerShriekModules J K f O).mapHomologicalComplex (ComplexShape.up ℤ)).obj Lc).Acyclic) :
    ∃! t : (forgetSourceModules J K f O).mapDerivedCategory ⋙
        derivedLowerShriekAbelian J K f ⟶
      derivedLowerShriek J K f O ⋙ (forgetTargetModules K O).mapDerivedCategory,
      Functor.whiskerLeft DerivedCategory.Qh t ≫ derivedLowerShriekForgetCounit J K f O =
        derivedForgetComparisonCounit J K f O

Stacks.Cohomology.DerivedLowerShriek.exists_isIso_forgetComparison_not_isIso_derivedForgetComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LowerShriek/ForgetComparisonCounterexample.lean, line 810. The attribute's comment: “the warning: the square forget ∘ Lg_! vs Lg_!^{Ab} ∘ forget need not commute even when g_! = g_!^{Ab} -- an example of sites, a functor satisfying the hypotheses of Stacks 07AC and a sheaf of rings for which the comparison of Stacks 0798 is an isomorphism and the comparison Lg_!^{Ab} ∘ forget ⟶ forget ∘ Lg_! is not, nor are the two composites isomorphic by any natural isomorphism; the example lives in universe 0, an existence statement needing one”.

Stacks Project, Tag 07AE, the warning. Let u : C ⥤ D, g, O_D and O_C = g^{-1} O_D be as in Stacks 07AC. In general the square

D(O_C) --Lg_!--> D(O_D)
  |                 |
forget            forget
  v                 v
D(C) --Lg_!^{Ab}--> D(D)

does not commute, and this can happen even if g_! = g_!^{Ab}.

Stated as an existence: there are small sites C, D, a functor u : C ⥤ D satisfying the hypotheses of Stacks 07AC (continuous in the sense of Stacks 00WV, which is Functor.IsContinuous together with Stacks.Sites.PreservesCoveringPullbacks, and cocontinuous) and a sheaf of rings O_D on D such that

• g_! = g_!^{Ab}: the canonical comparison g_!^{Ab} ∘ forget ⟶ forget ∘ g_! of Stacks 0798 (forgetComparison) is an isomorphism, and yet
• the canonical comparison Lg_!^{Ab} ∘ forget ⟶ forget ∘ Lg_! of Stacks 07AE (derivedForgetComparison, characterised by existsUnique_derivedForgetComparison_of_continuous) is not an isomorphism, and indeed the two composites Lg_!^{Ab} ∘ forget and forget ∘ Lg_! are not isomorphic by any natural isomorphism whatsoever.

The example: C is the cospan category left ⟶ one ⟵ right and D is Bool ordered by false ≤ true, both with the trivial topology, u sends the legs to false ≤ true, and O_D is ℤ at true and the zero ring at false. Every O_C-module vanishes at left and right, which forces g_! = g_!^{Ab} (isIso_forgetComparison); but the underlying abelian sheaf of j_{one!} O_one = O_C has a nonzero Ext^1 into the restriction of an injective abelian sheaf of D (not_subsingleton_ext_unit), which is the homotopy pushout 0 ← ℤ → 0 computing Lg_!^{Ab} at false having nonzero H^{-1}, so the comparison is not invertible (not_isIso_derivedForgetComparison, via the criterion of this tag, extAcyclic_forget_extensionByZeroUnit).

theorem exists_isIso_forgetComparison_not_isIso_derivedForgetComparison :
    ∃ (C D : Type) (_ : SmallCategory C) (_ : SmallCategory D)
      (J : GrothendieckTopology C) (K : GrothendieckTopology D) (f : C ⥤ D)
      (_ : f.IsContinuous J K) (_ : f.IsCocontinuous J K)
      (_ : Stacks.Sites.PreservesCoveringPullbacks J f) (O : Sheaf K CommRingCat.{0}),
      IsIso (forgetComparison J K f
          (Stacks.SheafOfModules.Tensor.ringSheaf (targetRingedSite K O).O)) ∧
        ¬ IsIso (derivedForgetComparison J K f
          (Stacks.SheafOfModules.Tensor.ringSheaf (targetRingedSite K O).O)) ∧
        ¬ Nonempty ((forgetSourceModules J K f
            (Stacks.SheafOfModules.Tensor.ringSheaf (targetRingedSite K O).O)).mapDerivedCategory ⋙
              derivedLowerShriekAbelian J K f ≅
          derivedLowerShriek J K f
              (Stacks.SheafOfModules.Tensor.ringSheaf (targetRingedSite K O).O) ⋙
            (forgetTargetModules K (Stacks.SheafOfModules.Tensor.ringSheaf
              (targetRingedSite K O).O)).mapDerivedCategory)

Stacks.Cohomology.DerivedLowerShriek.isIso_derivedForgetComparison_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LowerShriek/ForgetComparisonCriterionFromContinuity.lean, line 725. The attribute's comment: “the criterion: Lg_! agrees with Lg_!^{Ab} (the comparison Lg_!^{Ab} ∘ forget ⟶ forget ∘ Lg_! is invertible) iff every canonical map Lg_!^{Ab} j_{U!}O_U ⟶ j_{u(U)!}O_{u(U)} is invertible in D(D); both directions, under the hypotheses of Stacks 07AC only, in the library's convention for it: small sites with objects, morphisms and module sections in one universe, and a sheaf of (commutative) rings”.

Stacks Project, Tag 07AE, the criterion. Let u : C ⥤ D be a continuous and cocontinuous functor of sites, g the corresponding morphism of topoi, O_D a sheaf of rings on D and O_C = g^{-1}O_D. Then Lg_! agrees with Lg_!^{Ab}, in the sense that the canonical comparison Lg_!^{Ab} ∘ forget ⟶ forget ∘ Lg_! is an isomorphism, if and only if the canonical maps Lg_!^{Ab} j_{U!}O_U ⟶ j_{u(U)!}O_{u(U)} are isomorphisms in D(D) for all objects U of C.

The comparison is derivedForgetComparison, the unique transformation compatible with the two counits and the comparison of Stacks 0798 (existsUnique_derivedForgetComparison_of_continuous). The canonical map at U is derivedForgetComparisonGenerator: the component of the comparison at j_{U!}O_U in degree zero, followed by the identification Lg_!(j_{U!}O_U) = g_!j_{U!}O_U = j_{u(U)!}O_{u(U)} of Stacks 07AC. The hypotheses are those of Stacks 07AC; continuity in the sense of Stacks 00WV is Functor.IsContinuous with Stacks.Sites.PreservesCoveringPullbacks. The forward implication is isIso_derivedForgetComparisonGenerator, the converse isIso_derivedForgetComparison_of_isIso_generator.

theorem isIso_derivedForgetComparison_iff :
    IsIso (derivedForgetComparison J K f (Stacks.SheafOfModules.Tensor.ringSheaf
      (targetRingedSite K O).O)) ↔
      ∀ U : C, IsIso (derivedForgetComparisonGenerator J K f
        (Stacks.SheafOfModules.Tensor.ringSheaf (targetRingedSite K O).O) U)

Stacks.Cohomology.DerivedLowerShriek.existsUnique_derivedForgetComparison_of_continuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LowerShriek/ForgetComparisonFromContinuity.lean, line 119. The attribute's comment: “the comparison transformation Lg_!^{Ab} ∘ forget ⟶ forget ∘ Lg_!, with no hypothesis beyond those of Stacks 07AC: continuity of u (Stacks 00WV) is Functor.IsContinuous with Stacks.Sites.PreservesCoveringPullbacks; the existence of g_!, g_!^{Ab}, Lg_! and Lg_!^{Ab} is proved, not assumed; the sites are small and the ring sheaf commutative, as in Stacks 07AC”.

Stacks Project, Tag 07AE. Let u : C ⥤ D be a continuous and cocontinuous functor of sites, let g : Sh(C) ⟶ Sh(D) be the corresponding morphism of topoi, let O_D be a sheaf of rings on D and set O_C = g^{-1}O_D. There is exactly one natural transformation

Lg_!^{Ab} ∘ forget ⟶ forget ∘ Lg_!

compatible with the counits exhibiting the two functors as left derived functors and with the comparison g_!^{Ab} ∘ forget ⟶ forget ∘ g_! of Stacks 0798.

That is all the warning allows: the undifferentiated functors already need not agree, which is Stacks.SheafOfModules.lowerShriekForget_not_isomorphic, and the square commutes exactly when the canonical maps Lg_!^{Ab} j_{U!}O_U ⟶ j_{u(U)!}O_{u(U)} are isomorphisms, which they need not be. Uniqueness is what makes this the comparison of the warning rather than some transformation between the two composites: a left derived functor is a right Kan extension along the localization, so a transformation into Lg_! ⋙ forget is the same thing as one out of Q_h ⋙ (forget ⋙ Lg_!^{Ab}) into degreewise g_! ⋙ forget followed by Q_h, and the lift is unique.

This is existsUnique_derivedForgetComparison_of_acyclic with its inputs discharged; see the module docstring. The hypotheses are exactly those of Stacks 07AC: [f.IsContinuous J K] and [Stacks.Sites.PreservesCoveringPullbacks J f] together are continuity of u in the sense of Stacks 00WV, [f.IsCocontinuous J K] is cocontinuity, and O is the sheaf of rings O_D. The acyclicity statement of Stacks 0794 that the conditional form takes as hFP, the left adjoints g_! and g_!^{Ab} of restriction, and the existence of both derived functors are all found by instance search from the instances proved in ModuleDerivedLowerShriek.lean, AbelianAcyclicityFromContinuity.lean and AdjointExistence.lean; the transformation itself is derivedForgetComparison.

theorem existsUnique_derivedForgetComparison_of_continuous :
    ∃! t : (forgetSourceModules J K f
          (Stacks.SheafOfModules.Tensor.ringSheaf (targetRingedSite K O).O)).mapDerivedCategory ⋙
        derivedLowerShriekAbelian J K f ⟶
      derivedLowerShriek J K f (Stacks.SheafOfModules.Tensor.ringSheaf (targetRingedSite K O).O) ⋙
        (forgetTargetModules K
          (Stacks.SheafOfModules.Tensor.ringSheaf (targetRingedSite K O).O)).mapDerivedCategory,
      Functor.whiskerLeft DerivedCategory.Qh t ≫
          derivedLowerShriekForgetCounit J K f
            (Stacks.SheafOfModules.Tensor.ringSheaf (targetRingedSite K O).O) =
        derivedForgetComparisonCounit J K f
          (Stacks.SheafOfModules.Tensor.ringSheaf (targetRingedSite K O).O)

Tag 0D6Y, a lemma

Tag 0D6Y in the Stacks Project.

Stacks.Cohomology.DerivedLowerShriek.isTotallyAcyclic_inverseImage_of_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LowerShriek/TotalAcyclicityOfTheInverseImage.lean, line 451.

Stacks Project, Tag 0D6Y. Let u : C ⥤ D be a continuous and cocontinuous functor of sites and let g : Sh(C) → Sh(D) be the corresponding morphism of topoi, so that g^{-1} is restriction along u by Sites, Lemma 00XR. Let O_D be a sheaf of rings on D and let I be an injective O_D-module. If g_!^{Sh} : Sh(C) → Sh(D) commutes with fibre products, then g^{-1}I is totally acyclic: its cohomology over every sheaf of sets on C vanishes in every positive degree.

As in the source, total acyclicity of a module is that of its underlying abelian sheaf; the abelian sheaf underlying g^{-1}I is the restriction along u of the abelian sheaf underlying I, which is how the conclusion is phrased.

theorem isTotallyAcyclic_inverseImage_of_injective
    [∀ n : ℕ, PreservesLimitsOfShape (WidePullbackShape (Fin (n + 1)))
      (u.sheafPullback (Type w) J Y.J)]
    (I : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) [Injective I] :
    IsTotallyAcyclic.{w} J
      ((u.sheafPushforwardContinuous AddCommGrpCat.{w} J Y.J).obj
        ((SheafOfModules.toSheaf (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)).obj I))

Stacks.Cohomology.DerivedLowerShriek.isTotallyAcyclic_inverseImage_of_injective_of_pullbacks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LowerShriek/TotalAcyclicityOfTheInverseImage.lean, line 468. The attribute's comment: “the case of the footnote's sufficient condition: C has finite connected limits and u commutes with them”.

Stacks Project, Tag 0D6Y, under the sufficient condition of its footnote. If C has fibre products and equalizers — equivalently, all finite connected limits — and u preserves them, then g_!^{Sh} commutes with fibre products by Sites, Lemma 00XS, and the inverse image of an injective O_D-module is totally acyclic.

theorem isTotallyAcyclic_inverseImage_of_injective_of_pullbacks [HasPullbacks C] [HasEqualizers C]
    [PreservesLimitsOfShape WalkingCospan u] [PreservesLimitsOfShape WalkingParallelPair u]
    (I : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) [Injective I] :
    IsTotallyAcyclic.{w} J
      ((u.sheafPushforwardContinuous AddCommGrpCat.{w} J Y.J).obj
        ((SheafOfModules.toSheaf (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)).obj I))

Stacks.Cohomology.DerivedLowerShriek.isTotallyAcyclic_pushforwardModule_of_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LowerShriek/TotalAcyclicityOfTheInverseImage.lean, line 485. The attribute's comment: “the conclusion read on the inverse image module rather than on the restriction of the underlying abelian sheaf”.

Stacks Project, Tag 0D6Y, read on the inverse image module. The abelian sheaf underlying the inverse image g^{-1}I of an injective O_D-module — restriction along u, as a module over the inverse image g^{-1}O_D of the structure sheaf — is totally acyclic.

theorem isTotallyAcyclic_pushforwardModule_of_injective
    [∀ n : ℕ, PreservesLimitsOfShape (WidePullbackShape (Fin (n + 1)))
      (u.sheafPullback (Type w) J Y.J)]
    (I : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) [Injective I] :
    IsTotallyAcyclic.{w} J
      ((SheafOfModules.toSheaf _).obj
        ((SheafOfModules.pushforward (F := u)
          (𝟙 ((u.sheafPushforwardContinuous RingCat.{w} J Y.J).obj
            (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)))).obj I))

Stacks.Cohomology.DerivedLowerShriek.isTotallyAcyclic_inverseImage_of_injective_of_cospans, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LowerShriek/TotalAcyclicityOfTheInverseImage.lean, line 510. The attribute's comment: “the tag at the source's own hypothesis, that g_!^{Sh} commute with binary fibre products; the iterated fibre powers the proof uses follow from it”.

Stacks Project, Tag 0D6Y, with the hypothesis the source states. Let u : C ⥤ D be a continuous and cocontinuous functor of sites and let g : Sh(C) → Sh(D) be the corresponding morphism of topoi. Let O_D be a sheaf of rings on D and let I be an injective O_D-module. If g_!^{Sh} : Sh(C) → Sh(D) commutes with binary fibre products, then g^{-1}I is totally acyclic.

The complex of Stacks 07A1 is built from the iterated fibre powers of a surjection of sheaves of sets, so it is commutation with those that the proof uses. Commutation with binary fibre products supplies it: an iterated fibre power is a fibre product of one fewer of its factors against the remaining one, and Sh(C) has fibre products, so CategoryTheory.Limits.preservesLimitsOfShape_widePullbackShape applies.

theorem isTotallyAcyclic_inverseImage_of_injective_of_cospans
    [PreservesLimitsOfShape WalkingCospan (u.sheafPullback (Type w) J Y.J)]
    (I : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) [Injective I] :
    IsTotallyAcyclic.{w} J
      ((u.sheafPushforwardContinuous AddCommGrpCat.{w} J Y.J).obj
        ((SheafOfModules.toSheaf (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)).obj I))

Stacks.Cohomology.DerivedLowerShriek.isTotallyAcyclic_inverseImage_of_injective_sheafOfRings, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LowerShriek/TotalAcyclicityOfTheInverseImage.lean, line 570.

Stacks Project, Tag 0D6Y. Let u : C ⥤ D be a continuous and cocontinuous functor of sites and let g : Sh(C) → Sh(D) be the corresponding morphism of topoi, so that g^{-1} is restriction along u by Sites, Lemma 00XR. Let O_D be a sheaf of rings on D and let I be an injective O_D-module. If g_!^{Sh} : Sh(C) → Sh(D) commutes with fibre products, then g^{-1}I is totally acyclic: its cohomology over every sheaf of sets on C vanishes in every positive degree.

As in the source, total acyclicity of a module is that of its underlying abelian sheaf; the abelian sheaf underlying g^{-1}I is the restriction along u of the abelian sheaf underlying I, which is how the conclusion is phrased.

theorem isTotallyAcyclic_inverseImage_of_injective_sheafOfRings
    [∀ n : ℕ, PreservesLimitsOfShape (WidePullbackShape (Fin (n + 1)))
      (u.sheafPullback (Type w) J K)]
    (I : SheafOfModules.{w} O) [Injective I] :
    IsTotallyAcyclic.{w} J
      ((u.sheafPushforwardContinuous AddCommGrpCat.{w} J K).obj
        ((SheafOfModules.toSheaf O).obj I))

Stacks.Cohomology.DerivedLowerShriek.isTotallyAcyclic_inverseImage_of_injective_of_pullbacks_sheafOfRings, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LowerShriek/TotalAcyclicityOfTheInverseImage.lean, line 587. The attribute's comment: “the case of the footnote's sufficient condition: C has finite connected limits and u commutes with them”.

Stacks Project, Tag 0D6Y, under the sufficient condition of its footnote. If C has fibre products and equalizers — equivalently, all finite connected limits — and u preserves them, then g_!^{Sh} commutes with fibre products by Sites, Lemma 00XS, and the inverse image of an injective O_D-module is totally acyclic.

theorem isTotallyAcyclic_inverseImage_of_injective_of_pullbacks_sheafOfRings
    [HasPullbacks C] [HasEqualizers C]
    [PreservesLimitsOfShape WalkingCospan u] [PreservesLimitsOfShape WalkingParallelPair u]
    (I : SheafOfModules.{w} O) [Injective I] :
    IsTotallyAcyclic.{w} J
      ((u.sheafPushforwardContinuous AddCommGrpCat.{w} J K).obj
        ((SheafOfModules.toSheaf O).obj I))

Stacks.Cohomology.DerivedLowerShriek.isTotallyAcyclic_pushforwardModule_of_injective_sheafOfRings, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LowerShriek/TotalAcyclicityOfTheInverseImage.lean, line 605. The attribute's comment: “the conclusion read on the inverse image module rather than on the restriction of the underlying abelian sheaf”.

Stacks Project, Tag 0D6Y, read on the inverse image module. The abelian sheaf underlying the inverse image g^{-1}I of an injective O_D-module — restriction along u, as a module over the inverse image g^{-1}O_D of the structure sheaf — is totally acyclic.

theorem isTotallyAcyclic_pushforwardModule_of_injective_sheafOfRings
    [∀ n : ℕ, PreservesLimitsOfShape (WidePullbackShape (Fin (n + 1)))
      (u.sheafPullback (Type w) J K)]
    (I : SheafOfModules.{w} O) [Injective I] :
    IsTotallyAcyclic.{w} J
      ((SheafOfModules.toSheaf _).obj
        ((SheafOfModules.pushforward (F := u)
          (𝟙 ((u.sheafPushforwardContinuous RingCat.{w} J K).obj O))).obj I))

Stacks.Cohomology.DerivedLowerShriek.isTotallyAcyclic_inverseImage_of_injective_of_cospans_sheafOfRings, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LowerShriek/TotalAcyclicityOfTheInverseImage.lean, line 629. The attribute's comment: “the tag at the source's own hypothesis, that g_!^{Sh} commute with binary fibre products; the iterated fibre powers the proof uses follow from it”.

Stacks Project, Tag 0D6Y, with the hypothesis the source states. Let u : C ⥤ D be a continuous and cocontinuous functor of sites and let g : Sh(C) → Sh(D) be the corresponding morphism of topoi. Let O_D be a sheaf of rings on D and let I be an injective O_D-module. If g_!^{Sh} : Sh(C) → Sh(D) commutes with binary fibre products, then g^{-1}I is totally acyclic.

The complex of Stacks 07A1 is built from the iterated fibre powers of a surjection of sheaves of sets, so it is commutation with those that the proof uses. Commutation with binary fibre products supplies it: an iterated fibre power is a fibre product of one fewer of its factors against the remaining one, and Sh(C) has fibre products, so CategoryTheory.Limits.preservesLimitsOfShape_widePullbackShape applies.

theorem isTotallyAcyclic_inverseImage_of_injective_of_cospans_sheafOfRings
    [PreservesLimitsOfShape WalkingCospan (u.sheafPullback (Type w) J K)]
    (I : SheafOfModules.{w} O) [Injective I] :
    IsTotallyAcyclic.{w} J
      ((u.sheafPushforwardContinuous AddCommGrpCat.{w} J K).obj
        ((SheafOfModules.toSheaf O).obj I))

Tag 0DD8, a lemma

Tag 0DD8 in the Stacks Project.

Stacks.Cohomology.DerivedLowerShriek.derivedAbelianSectionsRestrictionIso_of_continuous, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LowerShriek/DerivedSectionsAlongAContinuousFunctor.lean, line 96. The attribute's comment: “part (1); the two sites are small and the coefficients are in their universe, the library's standard one-universe convention for sites”.

Stacks Project, Tag 0DD8, part (1). Let u : C ⥤ D be a continuous and cocontinuous functor of sites and let g : Sh(C) ⟶ Sh(D) be the corresponding morphism of topoi. For every object U of C and every M in the unbounded derived category of abelian sheaves on D, RΓ(U, g⁻¹M) = RΓ(u(U), M), naturally in M.

This is derivedAbelianSectionsRestrictionIso with all of its inputs discharged. The invertibility of the derived lower-shriek counit at the single complex on j_{U!} ℤ_U is isIso_derivedAbelianLowerShriekComparison_app, which holds because that complex is cellular for the class with which Lg_!^{Ab} is built; the existence of Lg_!^{Ab} and its absoluteness against derived restriction are the two instances of AbelianAcyclicityFromContinuity.lean. All three come from the acyclicity statement of Stacks 0794 for lower shriek on abelian sheaves, which that file derives from Stacks 0D6X and so from the covering-pullback clause Stacks.Sites.PreservesCoveringPullbacks of continuity in the sense of Sites, Definition 00WV.

def derivedAbelianSectionsRestrictionIso_of_continuous :
    derivedAbelianRestriction.{u} J K f ⋙ derivedAbelianSections J U ≅
      derivedAbelianSections K (f.obj U)

Stacks.Cohomology.DerivedLowerShriek.derivedModuleSectionsRestrictionIso_of_continuous, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LowerShriek/DerivedSectionsAlongAContinuousFunctor.lean, line 123. The attribute's comment: “part (2); the two sites are small and the module sections are in their universe, the library's standard one-universe convention for sites; the structure sheaf is a sheaf of commutative rings, which is what a sheaf of rings is in the source (Stacks 0006)”.

Stacks Project, Tag 0DD8, part (2). Let u : C ⥤ D be a continuous and cocontinuous functor of sites, let g : Sh(C) ⟶ Sh(D) be the corresponding morphism of topoi, let O_D be a sheaf of rings on D and let O_C = g⁻¹O_D. For every object U of C and every M in the unbounded derived category of O_D-modules, RΓ(U, g^*M) = RΓ(u(U), M), naturally in M.

This is derivedModuleSectionsRestrictionIso with all of its inputs discharged. The invertibility of the derived lower-shriek counit at the single complex on j_{U!} O_U is isIso_derivedLowerShriekComparison_app, and the existence of Lg_! and its absoluteness against derived restriction are the two instances of ModuleDerivedLowerShriek.lean; all three come from lowerShriekModules_acyclic, the acyclicity statement of Stacks 0794 for lower shriek on modules, which that file derives from Stacks 0D6X and so from the covering-pullback clause Stacks.Sites.PreservesCoveringPullbacks of continuity in the sense of Sites, Definition 00WV.

def derivedModuleSectionsRestrictionIso_of_continuous (O : Sheaf K CommRingCat.{u}) :
    derivedRestriction J K f (Stacks.SheafOfModules.Tensor.ringSheaf (targetRingedSite K O).O) ⋙
        derivedModuleSections J (inverseImageRing J K f
          (Stacks.SheafOfModules.Tensor.ringSheaf (targetRingedSite K O).O)) U ≅
      derivedModuleSections K (Stacks.SheafOfModules.Tensor.ringSheaf (targetRingedSite K O).O)
        (f.obj U)

Stacks.Cohomology.DerivedLowerShriek.derivedModuleSectionsRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LowerShriek/DerivedSectionsAlongAFunctor.lean, line 564. The attribute's comment: “part (2)”.

Stacks 0DD8, part (2). Let u : C ⥤ D be a continuous and cocontinuous functor of sites, let g : Sh(C) ⟶ Sh(D) be the corresponding morphism of topoi, let O_D be a sheaf of rings on D and let O_C = g⁻¹O_D. For every object U of C and every M in the unbounded derived category of O_D-modules, RΓ(U, g^*M) = RΓ(u(U), M), naturally in M.

def derivedModuleSectionsRestrictionIso
    (hgen : DerivedLowerShriekComputesGenerator J K f O U) :
    derivedRestriction J K f O ⋙ derivedModuleSections J (inverseImageRing J K f O) U ≅
      derivedModuleSections K O (f.obj U)

Stacks.Cohomology.DerivedLowerShriek.derivedAbelianSectionsRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LowerShriek/DerivedSectionsAlongAFunctor.lean, line 689. The attribute's comment: “part (1)”.

Stacks 0DD8, part (1). Let u : C ⥤ D be a continuous and cocontinuous functor of sites and let g : Sh(C) ⟶ Sh(D) be the corresponding morphism of topoi. For every object U of C and every M in the unbounded derived category of abelian sheaves on D, RΓ(U, g⁻¹M) = RΓ(u(U), M), naturally in M.

def derivedAbelianSectionsRestrictionIso
    (hgen : DerivedAbelianLowerShriekComputesGenerator J K f U) :
    derivedAbelianRestriction.{u} J K f ⋙ derivedAbelianSections J U ≅
      derivedAbelianSections K (f.obj U)

Tag 0FN6, a lemma

Tag 0FN6 in the Stacks Project.

Stacks.Cohomology.DerivedBaseChange.nonempty_inverseImage_comp_totalDerivedPushforwardOf_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPushforward/UnboundedBaseChangeForACocontinuousSquare.lean, line 498. The attribute's comment: “Rf'_* ∘ (g')^* ≅ g^* ∘ Rf_* on the unbounded derived categories D(O_C) → D(O_{D'}), for a commutative square of ringed topoi whose four functors u, u', v, v' are cocontinuous, with u' ⋙ v = v' ⋙ u, with v, v' continuous as well, with the comparison functors {}^{u'}_{V'} I → {}^u_{v(V')} I of the index categories of Section 00XF cofinal, with g^{-1} O_D = O_{D'} and (g')^{-1} O_C = O_{C'}, and with the tag's condition (6) in the source's own form: exactness of g'_! : Ab(C') → Ab(C), written PreservesFiniteLimits (v'.sheafPullback AddCommGrpCat J' J), right exactness of a left adjoint being automatic. Rf_* and Rf'_* are constructed, as the total right derived functors of the degreewise direct images of sheaves of modules, and nothing about them is required. The price of the source's condition (6) is that the four sites lie in one universe, which is where Stacks 0D6J, the transport from abelian sheaves to modules that the source's proof opens with, is available. An isomorphism rather than an equality, and asserted through Nonempty as its underived input Stacks 0FN3 is, a right derived functor being determined only up to a canonical isomorphism and the sheaf-level comparison of Stacks 0FN1 being a base change of right Kan extensions.”.

Stacks 0FN6. For a commutative square of ringed topoi whose four functors u : C ⥤ D, u' : C' ⥤ D', v : D' ⥤ D, v' : C' ⥤ C are cocontinuous — giving f, f', g, g' with f_* = {}_su, f'_* = {}_su' — with u' ⋙ v = v' ⋙ u, with v and v' continuous as well as cocontinuous so that g^{-1}, (g')^{-1} are restriction, with the comparison functors {}^{u'}_{V'} I ⥤ {}^u_{v(V')} I of the index categories of Section 00XF all cofinal, with g^{-1} O_D = O_{D'} and (g')^{-1} O_C = O_{C'}, and with g'_! : Ab(C') ⥤ Ab(C) exact, we have Rf'_* ∘ (g')^* = g^* ∘ Rf_* as functors D(O_C) ⥤ D(O_{D'}).

Condition (5) is built into the statement by taking the restrictions along v and v' as the sheaves of rings on D' and C', so that g^* = g^{-1} and (g')^* = (g')^{-1} are Stacks.SheafOfModules.inverseImage and are exact; (f')^♯ is the structure map the square forces, as in Stacks 0FN3. Condition (6) is the hypothesis PreservesFiniteLimits (v'.sheafPullback AddCommGrpCat J' J): v'.sheafPullback is the left adjoint g'_! = (v')_s of the inverse image (g')^{-1} = (v')^p of abelian sheaves, which Stacks 00XR produces for a continuous and cocontinuous v', and right exactness of a left adjoint is automatic, so left exactness is the whole of the condition.

Both Rf_* and Rf'_* are the total right derived functors of the degreewise direct images of sheaves of modules; nothing about them is assumed. The source's proof is followed exactly: the underived identity is Stacks 0FN3, which is what the cofinality hypothesis hfinal — condition (4) — feeds; condition (6) and Stacks 08BJ make (g')^{-1} preserve K-injectivity of abelian sheaves, Stacks 0FN1 gives the underived identity there, and Stacks 0D6J carries the resulting statement — that the inverse image of a K-injective complex of O_C-modules computes Rf'_* — back to modules.

theorem nonempty_inverseImage_comp_totalDerivedPushforwardOf_iso
    [PreservesFiniteLimits (v'.sheafPullback AddCommGrpCat.{u} J' J)]
    (fSharp : OD ⟶ (u.sheafPushforwardCocontinuous RingCat.{u} J K).obj OC)
    (hsq : u' ⋙ v = v' ⋙ u)
    (hcomm : f'Sharp = structureMapSquare (J' := J') (K' := K') fSharp hsq)
    (hfinal : ∀ V' : D',
      (CostructuredArrow.map₂ (S := u') (T := V') (U := u) (V := v.obj V') (F := v') (G := v)
        (eqToHom hsq.symm) (𝟙 (v.obj V'))).Final) :
    Nonempty ((inverseImage.{u} J' J v' OC).mapDerivedCategory ⋙
        UnboundedComplexes.totalRightDerivedOfAdditive
          (pushforwardCocontinuous.{u} u' f'Sharp) ≅
      UnboundedComplexes.totalRightDerivedOfAdditive (pushforwardCocontinuous.{u} u fSharp) ⋙
        (inverseImage.{u} K' K v OD).mapDerivedCategory)

Tag 0FN7, a lemma

Tag 0FN7 in the Stacks Project.

Stacks.Cohomology.DerivedBaseChange.inverseImageCompDerivedPushforwardPlusIsoOfRingedSite, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPushforward/BoundedBelowBaseChangeOverASquareOfSites.lean, line 338. The attribute's comment: “first conclusion: Rf'_* ∘ (g')^* ≅ g^* ∘ Rf_* on the bounded below derived categories D⁺(O_C) → D⁺(O_{D'}), for a commutative square of ringed topoi whose horizontal functors u, u' are continuous and whose vertical functors v, v' are continuous as well as cocontinuous, with v ⋙ u = u' ⋙ v', g^{-1} O_D = O_{D'} and (g')^{-1} O_C = O_{C'}, and WITHOUT the tag's condition (6), exactness of g'_! — which is what the second conclusion, on the unbounded derived categories, needs; that conclusion, under the source's own condition (6), is Stacks.Cohomology.DerivedBaseChange.inverseImageCompTotalDerivedPushforwardIsoOfExactLowerShriek. Proved as in the source, through the vanishing of Stacks 0D6X, the sheafified cohomology presheaf of Stacks 072W, and Leray's acyclicity lemma Stacks 015E. An isomorphism rather than an equality, a right derived functor being determined only up to a canonical isomorphism. The sites C and C' are at the single universe at which Stacks 0D6X and the Ext-to-derived-sections comparison of Stacks 03FD are available in this library — C' small and C the site of a ringed site — and v' is continuous in the sense of Sites, Definition 00WV, which is the hypothesis Stacks 0D6X uses and which Mathlib's IsContinuous does not supply; that is not an extra assumption relative to the source, where v' is continuous in exactly that sense, and Stacks.Sites.preservesCoveringPullbacks_of_isContinuous derives it from the project's formalization of Definition 00WV.”.

Stacks 0FN7, first conclusion, with the acyclicity step discharged. The same statement as inverseImageCompDerivedPushforwardPlusIso, in the universes at which Stacks 0D6X and Stacks 072W are available: C' is a small site and C is the site of a ringed site Y whose structure sheaf, module sections and Ext-groups lie in the universe of its objects, while D and D' keep arbitrary universes.

The source's condition (6) is not a hypothesis, and neither is the acyclicity it would be used for: it is proved here from Stacks 0D6X and Stacks 072W by rightAcyclic_pushforward_inverseImage_of_injective.

def inverseImageCompDerivedPushforwardPlusIsoOfRingedSite (hsq : v ⋙ u = u' ⋙ v')
    (hcomm : f'Sharp =
      restrictStructureMap J' Y.J K' K u u' v v' (Stacks.SheafOfModules.Tensor.ringSheaf Y.O) OD
        fSharp hsq) :
    (inverseImage.{w} J' Y.J v'
      (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)).mapDerivedCategoryPlus ⋙
        (_root_.SheafOfModules.pushforward.{w} f'Sharp).rightDerivedFunctorPlus ≅
      (_root_.SheafOfModules.pushforward.{w} fSharp).rightDerivedFunctorPlus ⋙
        (inverseImage.{w} K' K v OD).mapDerivedCategoryPlus

Stacks.Cohomology.DerivedBaseChange.inverseImageCompTotalDerivedPushforwardIsoOfExactLowerShriek, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPushforward/UnboundedBaseChangeForAnExactLowerShriek.lean, line 310. The attribute's comment: “the second conclusion, at the source's full statement of it: Rf'_* ∘ (g')^* ≅ g^* ∘ Rf_* on the unbounded derived categories D(O_C) → D(O_{D'}), for a commutative square of ringed topoi whose horizontal functors u, u' are continuous and whose vertical functors v, v' are continuous as well as cocontinuous, with v ⋙ u = u' ⋙ v', g^{-1} O_D = O_{D'} and (g')^{-1} O_C = O_{C'}, and with the tag's condition (6) as the source states it — exactness of g'_! : Ab(C') → Ab(C), written PreservesFiniteLimits (v'.sheafPullback AddCommGrpCat J' J), right exactness of a left adjoint being automatic. Nothing else is assumed: in particular NOT the module-level substitution for condition (6) that Stacks.Cohomology.DerivedBaseChange.inverseImageCompDerivedPushforwardIso and Stacks.Cohomology.DerivedBaseChange.inverseImageCompTotalDerivedPushforwardIso grant in its place, those two adding four independent universes instead. The price here is that the four sites lie in one universe, which is where Stacks 0D6J, the transport from abelian sheaves to modules that the source's proof opens with, is available. Rf_* and Rf'_* are constructed, as the total right derived functors of the degreewise direct images, and nothing about them is assumed. An isomorphism rather than an equality, a right derived functor being determined only up to a canonical isomorphism. The first conclusion of the tag, the same identity on D^+ without condition (6), is Stacks.Cohomology.DerivedBaseChange.inverseImageCompDerivedPushforwardPlusIsoOfRingedSite.”.

Stacks 0FN7, second conclusion, under the source's own condition (6). For a commutative square of ringed topoi whose horizontal functors u : D ⥤ C, u' : D' ⥤ C' are continuous — giving f, f' with f_* = u^s, f'_* = (u')^s — whose vertical functors v : D' ⥤ D, v' : C' ⥤ C are continuous as well as cocontinuous — giving g, g' with g^{-1}, (g')^{-1} restriction — with v ⋙ u = u' ⋙ v', with g^{-1} O_D = O_{D'} and (g')^{-1} O_C = O_{C'}, and with g'_! : Ab(C') ⥤ Ab(C) exact, we have Rf'_* ∘ (g')^* = g^* ∘ Rf_* as functors D(O_C) ⥤ D(O_{D'}).

Condition (6) is the hypothesis PreservesFiniteLimits (v'.sheafPullback AddCommGrpCat J' J): v'.sheafPullback is the left adjoint g'_! = (v')_s of the inverse image (g')^{-1} = (v')^p of abelian sheaves, which Stacks 00XR produces for a continuous and cocontinuous v', and right exactness of a left adjoint is automatic, so left exactness is the whole of the condition.

Both Rf_* and Rf'_* are the total right derived functors of the degreewise direct images; nothing about them is assumed. The source's proof is followed exactly: condition (6) and Stacks 08BJ make (g')^{-1} preserve K-injectivity of abelian sheaves, Stacks 0FN2 gives the underived identity there, and Stacks 0D6J carries the resulting statement — that the inverse image of a K-injective complex of O_C-modules computes Rf'_* — back to modules.

def inverseImageCompTotalDerivedPushforwardIsoOfExactLowerShriek
    [PreservesFiniteLimits (v'.sheafPullback AddCommGrpCat.{u} J' J)]
    (fSharp : OD ⟶ (u.sheafPushforwardContinuous RingCat.{u} K J).obj OC)
    (hsq : v ⋙ u = u' ⋙ v')
    (hcomm : f'Sharp = restrictStructureMap J' J K' K u u' v v' OC OD fSharp hsq) :
    (inverseImage.{u} J' J v' OC).mapDerivedCategory ⋙
        UnboundedComplexes.totalRightDerivedOfAdditive
          (_root_.SheafOfModules.pushforward.{u} f'Sharp) ≅
      UnboundedComplexes.totalRightDerivedOfAdditive
          (_root_.SheafOfModules.pushforward.{u} fSharp) ⋙
        (inverseImage.{u} K' K v OD).mapDerivedCategory

Sources

• Section 21.37, Tag 07AB
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.subsiteSliceCohomology_eq_zero · AlgebraicGeometry.Stack.FlatFppf.sliceAcyclic · AlgebraicGeometry.Stack.LisseEtale.sliceAcyclic · AlgebraicGeometry.Stack.subsiteObjectCohomology_eq_zero · AlgebraicGeometry.Stack.FlatFppf.objectAcyclic · AlgebraicGeometry.Stack.LisseEtale.objectAcyclic · AlgebraicGeometry.Stack.subsiteGlobalCohomology_eq_zero · Stacks.CechSite.injective_module_subsingleton_ext_of_continuous

Section21.38 Derived lower shriek for fibred categories#

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

Tag 08P8, a situation

Tag 08P8 in the Stacks Project.

Stacks.Sites.FibredCategory.FibredCategorySituation.totalRingedTopos, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/RingedProjection.lean, line 83. The attribute's comment: “inverse-image structure sheaf”.

Stacks 08P8, the inverse-image structure sheaf. The total ringed topos, with O_C = π⁻¹O_D.

def totalRingedTopos : RingedTopos.{vC, uC, max w uD vD uC vC}

Stacks.Sites.FibredCategory.FibredCategorySituation.ringedProjection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/RingedProjection.lean, line 91. The attribute's comment: “morphism of ringed topoi”.

Stacks 08P8, the morphism of ringed topoi. The projection as a morphism of ringed topoi; its structure map is the unit of the adjunction π⁻¹ ⊣ π_* on sheaves of rings.

def ringedProjection : RingedToposHom s.totalRingedTopos s.baseRingedTopos

Stacks.Sites.FibredCategory.FibredCategorySituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/RingedToposOfAFibredCategory.lean, line 321. The attribute's comment: “standing data”.

A ringed site (D, O_D) together with a fibred category p : C ⥤ D over its underlying site.

structure FibredCategorySituation

Stacks.Sites.FibredCategory.FibredCategorySituation.inducedProjection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/RingedToposOfAFibredCategory.lean, line 375. The attribute's comment: “associated morphism of topoi”.

Stacks 08P8, the associated morphism of topoi. The morphism of topoi π : Sh(C) ⟶ Sh(D) canonically associated to the fibred projection: its inverse image is restriction along p.op, which is left exact because restriction is computed on underlying presheaves, where it is precomposition.

noncomputable def inducedProjection : ProjectionData s

Stacks.Sites.FibredCategory.FibredCategorySituation.commRingRingedProjection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LowerShriekAndPerfection/FibredCategoryRingedTopos.lean, line 75. The attribute's comment: “morphism of ringed topoi”.

The projection of a fibred category as a morphism of ringed topoi; its structure map is the unit of the adjunction π⁻¹ ⊣ π_* on sheaves of commutative rings.

noncomputable def commRingRingedProjection :
    AlgebraicGeometry.RingedToposHom s.totalRingedTopos s.baseRingedTopos

Declarations registered for the tag:

• Stacks.Sites.FibredCategory.FibredCategorySituation, declared in the repository, registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/Cohomology/LowerShriekAndPerfection/FibredCategoryRingedTopos.lean, line 51 (StacksFrontier): “standing data”.
• Stacks.Sites.FibredCategory.FibredCategorySituation.inducedProjection, declared in the repository, registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/Cohomology/LowerShriekAndPerfection/FibredCategoryRingedTopos.lean, line 54 (StacksFrontier): “associated morphism of topoi”.
• Stacks.Sites.FibredCategory.FibredCategorySituation.totalRingedTopos, declared in the repository, registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/Cohomology/LowerShriekAndPerfection/FibredCategoryRingedTopos.lean, line 57 (StacksFrontier): “inverse-image structure sheaf”.

Tag 08P9, a lemma

Tag 08P9 in the Stacks Project.

Stacks.Sites.FibredCategory.localizedProjectionSection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LowerShriekAndPerfection/FibredCategorySection.lean, line 527.

The canonical localized projection has a section whose inverse image is its direct image.

public noncomputable def localizedProjectionSection : LocalizedProjectionSection s U

Tag 08PA, a situation

Tag 08PA in the Stacks Project.

Stacks.Sites.FibredCategory.MorphismSituation.ringedToposDiagram, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/RingedToposDiagram.lean, line 185. The attribute's comment: “canonical commutative triangle of ringed topoi”.

Stacks 08PA. The canonical commutative triangle of ringed topoi associated to a 1-morphism of fibred categories over a ringed site: the three morphisms of topoi of Stacks 06NW, each pinned by the identification of its inverse image with restriction and of its direct image with the right Kan extension, the morphism of ringed topoi g whose inverse-image structure map is the identification g⁻¹O_C ≅ O_{C'}, and the 2-isomorphism π_* ∘ g_* ≅ (π')_* exhibited as the mate of the comparison of inverse images.

noncomputable def ringedToposDiagram : S.RingedToposDiagram

Stacks.Sites.FibredCategory.MorphismSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/RingedToposOfAMorphism.lean, line 136. The attribute's comment: “standing data”.

Stacks 08PA, standing data. A ringed site (D, O_D), two fibred categories over its underlying site, and a 1-morphism of fibred categories between them.

structure MorphismSituation.{a₀, a₁, a₂, b₀, b₁, b₂, c}

Tag 08PB, a lemma

Tag 08PB in the Stacks Project.

Stacks.Sites.FibredCategory.MorphismSituation.compatibleLocalizedSection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LowerShriekAndPerfection/MorphismOfFibredCategoriesSection.lean, line 622.

Stacks 08PB. The localized projections of a 1-morphism of fibred categories admit a common section: a morphism of topoi σ' : Sh(D/V) ⟶ Sh(C'/U') with π'_{U'} ∘ σ' = id and (σ')^{-1} = π'_{U',*}, whose composite σ = g' ∘ σ' satisfies π_U ∘ σ = id and σ^{-1} = π_{U,*}.

def compatibleLocalizedSection : CompatibleLocalizedSection S U'

Tag 08PC, a lemma

Tag 08PC in the Stacks Project.

Stacks.Sites.FibredCategory.MorphismSituation.abelianInverseImage_isRightAdjoint, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/AbelianLowerShriek.lean, line 98. The attribute's comment: “part (1), abelian sheaves”.

Stacks 08PC, part (1) for abelian sheaves. The inverse image of abelian sheaves along g admits a left adjoint g_!^{Ab}. The left adjoint is the sheafification of the left Kan extension along u.op, so the only hypothesis is that abelian groups can be sheafified on the target site.

instance abelianInverseImage_isRightAdjoint
    [HasWeakSheafify S.totalTopology AddCommGrpCat.{max w u₀ u₁ u₂ v₀ v₁ v₂}] :
    S.abelianInverseImage.IsRightAdjoint

Stacks.Sites.FibredCategory.MorphismSituation.isIso_derivedModuleLowerShriekForgetComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/ModuleDerivedLowerShriekForget.lean, line 334. The attribute's comment: “part (4): the canonical comparison Lg_!^{Ab} ∘ forget ⟶ forget ∘ Lg_! is an isomorphism”.

Stacks 08PC, part (4). In Situation 08PA the canonical comparison of Stacks 07AE

Lg_!^{Ab} ∘ forget ⟶ forget ∘ Lg_!

of functors D(O_{C'}) ⥤ D(C) (derivedModuleLowerShriekForgetComparison) is an isomorphism: the derived lower shriek on sheaves of modules commutes with forgetting the module structure.

Lg_!^{Ab} ∘ forget is a left derived functor of g_!^{Ab} ∘ forget on the homotopy category of Mod(O_{C'}) (isLeftDerivedFunctor_derivedForgetAbelianLowerShriek), hence of forget ∘ g_!, the degreewise comparison being invertible by part (2) (isIso_moduleLowerShriekForgetComparison); and the lift of a comparison between two left derived functors of the same functor is an isomorphism.

theorem isIso_derivedModuleLowerShriekForgetComparison :
    IsIso S.derivedModuleLowerShriekForgetComparison

Stacks.Sites.FibredCategory.MorphismSituation.moduleDiagramInverseImage_isRightAdjoint, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/ModuleInverseImage.lean, line 212. The attribute's comment: “part (1), modules”.

Stacks 08PC, part (1) for sheaves of modules. The inverse image of sheaves of modules along the g of a commutative triangle of ringed topoi over the situation admits a left adjoint g_!. The inverse image is the one of Stacks 03D2 followed by extension of scalars along g♯; the first factor is a right adjoint because g⁻¹ is restriction along the continuous functor u, and the second because g♯ is an isomorphism, which the triangle records.

instance moduleDiagramInverseImage_isRightAdjoint (D : S.RingedToposDiagram) :
    (D.gRinged.toModulesHom.pullbackModules).IsRightAdjoint

Stacks.Sites.FibredCategory.MorphismSituation.moduleDiagramInverseImage_isRightAdjointUnconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/ModuleLowerShriekForgetSquare.lean, line 138. The attribute's comment: “part (1), modules: g^* has a left adjoint g_!”.

Stacks 08PC, part (1), for sheaves of modules, with no sheafification hypothesis. The inverse image g^* of sheaves of modules along the g of any commutative triangle of ringed topoi over Situation 08PA has a left adjoint g_!. This is MorphismSituation.moduleDiagramInverseImage_isRightAdjoint with its sheafification hypotheses discharged: at the situation's universe of sections both inherited sites are essentially small.

theorem moduleDiagramInverseImage_isRightAdjointUnconditional (D : S.RingedToposDiagram) :
    (D.gRinged.toModulesHom.pullbackModules).IsRightAdjoint

Stacks.Sites.FibredCategory.MorphismSituation.abelianInverseImage_isRightAdjointUnconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/ModuleLowerShriekForgetSquare.lean, line 147. The attribute's comment: “part (1), abelian sheaves: g^{-1} has a left adjoint g_!^{Ab}”.

Stacks 08PC, part (1), for abelian sheaves, with no sheafification hypothesis. The inverse image g^{-1} of abelian sheaves has a left adjoint g_!^{Ab}. This is MorphismSituation.abelianInverseImage_isRightAdjoint with its sheafification hypothesis discharged.

theorem abelianInverseImage_isRightAdjointUnconditional :
    S.abelianInverseImage.IsRightAdjoint

Stacks.Sites.FibredCategory.MorphismSituation.isIso_moduleLowerShriekForgetComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/ModuleLowerShriekForgetSquare.lean, line 289. The attribute's comment: “part (2): the canonical comparison g_!^{Ab} ∘ forget ⟶ forget ∘ g_! is an isomorphism”.

Stacks 08PC, part (2). In Situation 08PA the canonical comparison of Stacks 0798

g_!^{Ab} ∘ forget ⟶ forget ∘ g_!

(MorphismSituation.moduleLowerShriekForgetComparison, the transformation adjoint to the forgotten unit of g_! ⊣ g^*, for the structure sheaf O_{C'} = (π')^{-1} O_D of the situation) is an isomorphism: lower shriek on sheaves of modules commutes with forgetting the module structure.

The comparison is an isomorphism for the structure sheaf u⁻¹O_C of C' (isIso_lowerShriekForgetComparison_structureMap, which is where Stacks 08PB enters), and the structure sheaf of Situation 08PA is isomorphic to it through the structure map MorphismSituation.moduleStructureMap, built from the invertible g♯; the comparison along an isomorphic structure map is the same comparison up to restriction of scalars (Stacks.SheafOfModules.isIso_lowerShriekForgetComparison_of_restrictScalars).

theorem isIso_moduleLowerShriekForgetComparison :
    IsIso S.moduleLowerShriekForgetComparison

Stacks.Sites.FibredCategory.MorphismSituation.derivedAbelianLowerShriekAdjunctionUnconditional, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/MorphismDerivedAbelianLowerShriek.lean, line 50. The attribute's comment: “part (3), abelian sheaves: the adjunction Lg_!^Ab ⊣ g^-1”.

Stacks 08PC part (3) for abelian sheaves, the adjunction. The unbounded left derived lower-shriek functor Lg_!^{Ab} : D(Ab(C')) ⥤ D(Ab(C)) is left adjoint to g^{-1} on the unbounded derived categories. This is MorphismSituation.derivedAbelianLowerShriekAdjunction with its acyclicity input supplied by abelianLowerShriekAcyclic.

def derivedAbelianLowerShriekAdjunctionUnconditional :
    S.derivedAbelianLowerShriek ⊣ S.derivedAbelianInverseImage

Stacks.Sites.FibredCategory.MorphismSituation.hasPointwiseLeftDerivedModuleLowerShriekUnconditional, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/MorphismModuleLowerShriekAcyclic.lean, line 317. The attribute's comment: “part (3), modules: existence of Lg_! : D(O_{C'}) ⥤ D(O_C)”.

Stacks 08PC part (3) for sheaves of modules, existence. Degreewise g_!, followed by the localization of the homotopy category of Mod(O_C), has a pointwise left derived functor along the localization of the homotopy category of Mod(O_{C'}); that is, Lg_! : D(O_{C'}) ⥤ D(O_C) exists. This is MorphismSituation.hasPointwiseLeftDerivedModuleLowerShriek with the acyclicity statement of Stacks 07AC supplied by moduleLowerShriekAcyclic.

instance hasPointwiseLeftDerivedModuleLowerShriekUnconditional :
    (S.moduleLowerShriekOnHomotopy ⋙ DerivedCategory.Qh).HasPointwiseLeftDerivedFunctor
      S.moduleSourceQuasiIso

Stacks.Sites.FibredCategory.MorphismSituation.derivedModuleLowerShriekAdjunctionUnconditional, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/MorphismModuleLowerShriekAcyclic.lean, line 328. The attribute's comment: “part (3), modules: the adjunction Lg_! ⊣ g^*”.

Stacks 08PC part (3) for sheaves of modules, the adjunction. The unbounded left derived lower-shriek functor Lg_! : D(O_{C'}) ⥤ D(O_C) is left adjoint to g^* = g^{-1} on the unbounded derived categories. This is MorphismSituation.derivedModuleLowerShriekAdjunction (Stacks 09T5) with the acyclicity statement of Stacks 07AC supplied by moduleLowerShriekAcyclic; nothing beyond Situation 08PA is assumed.

def derivedModuleLowerShriekAdjunctionUnconditional :
    S.derivedModuleLowerShriek ⊣ S.derivedModuleInverseImage

Declarations registered for the tag:

• Stacks.Sites.FibredCategory.MorphismSituation.hasPointwiseLeftDerivedFunctor_abelianLowerShriekOnHomotopy, declared in the repository, registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/MorphismDerivedAbelianLowerShriek.lean, line 42 (StacksFrontier): “part (3), abelian sheaves: existence of Lg_!^Ab”.

Tag 09CY, a remark

Tag 09CY in the Stacks Project.

Stacks.Sites.FibredCategory.FibredCategorySituation.toMorphismSituation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/ProjectionAsAMorphismOfFibredCategories.lean, line 103. The attribute's comment: “the reduction of Situation 08P8 to Situation 08PA, by C = D and u = p”.

Stacks 09CY, the reduction. The standing data of Stacks 08PA obtained from that of Stacks 08P8: the same ringed base site, the target fibred category taken to be the base itself fibred over itself by the identity functor, the source fibred category taken to be C, and the 1-morphism taken to be the structure functor p.

def toMorphismSituation : MorphismSituation.{uD, uD, uC, vD, vD, vC, w}

Stacks.Sites.FibredCategory.FibredCategorySituation.abelianInverseImage_toMorphismSituation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/ProjectionAsAMorphismOfFibredCategories.lean, line 161. The attribute's comment: “the reduced situation's g^{-1} is the π^{-1} of Situation 08P8”.

g^{-1} of the reduced situation is π^{-1}: both are restriction of abelian sheaves along p between the same two sites.

theorem abelianInverseImage_toMorphismSituation :
    HEq s.toMorphismSituation.abelianInverseImage s.abelianInverseImage

Stacks.Sites.FibredCategory.FibredCategorySituation.abelianLowerShriek_toMorphismSituation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/ProjectionAsAMorphismOfFibredCategories.lean, line 176. The attribute's comment: “the reduced situation's g_!^{Ab} is the π_!^{Ab} of Situation 08P8”.

g_!^{Ab} of the reduced situation is π_!^{Ab}: both are the chosen left adjoint of restriction of abelian sheaves along p between the same two sites.

theorem abelianLowerShriek_toMorphismSituation :
    HEq (@MorphismSituation.abelianLowerShriek.{uD, uD, uC, vD, vD, vC, w} s.toMorphismSituation
        s.hasWeakSheafifyToMorphismSituationTotalTopology) s.abelianLowerShriek

Stacks.Sites.FibredCategory.FibredCategorySituation.derivedAbelianLowerShriekAdjunctionUnconditional, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/ProjectionLowerShriekAcyclic.lean, line 339. The attribute's comment: “the derived abelian Lπ_!^{Ab} of Situation 08P8 and its adjunction Lπ_!^{Ab} ⊣ π^{-1}, with the acyclicity statement of Stacks 07AC discharged”.

Stacks 09CY, the derived abelian Lπ_!^{Ab} of Situation 08P8. Remark 09CY reduces Situation 08P8 to Situation 08PA and reads off from Lemma 08PC the four functors π_!, π_!^{Ab}, Lπ_! and Lπ_!^{Ab}. This is the third of them: Lπ_!^{Ab} : D(Ab(C)) ⥤ D(Ab(D)) is left adjoint to derived π^{-1}, which is part (3) of Stacks 08PC on abelian sheaves.

It is stated here rather than transported along the reduction because the acyclicity statement of Stacks 07AC, which is what part (3) rests on, is discharged for π in this file, as abelianLowerShriekAcyclic; the conditional form derivedAbelianLowerShriekAdjunction takes it as an argument, and this is that argument supplied, so the adjunction holds under the hypotheses of Situation 08P8 alone.

def derivedAbelianLowerShriekAdjunctionUnconditional :
    s.derivedAbelianLowerShriek ⊣ s.derivedAbelianInverseImage

Stacks.Sites.FibredCategory.FibredCategorySituation.derivedModuleLowerShriekAdjunctionAtBaseModuleRing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/ProjectionModuleDerivedLowerShriek.lean, line 333. The attribute's comment: “the derived Lπ_! of Situation 08P8 on sheaves of modules and its adjunction Lπ_! ⊣ π^*”.

Stacks 09CY, the derived Lπ_! on sheaves of modules. The unbounded left derived functor Lπ_! : D(O_C) ⥤ D(O_D) of the lower-shriek functor on sheaves of modules exists and is left adjoint to π^* : D(O_D) ⥤ D(O_C). This is Stacks 08PC part (3) for modules in the situation of the remark; the acyclicity statement of Stacks 07AC it rests on is moduleLowerShriekAcyclic.

def derivedModuleLowerShriekAdjunctionAtBaseModuleRing :
    s.derivedModuleLowerShriekAtBaseModuleRing ⊣ s.derivedModuleRestriction

Stacks.Sites.FibredCategory.FibredCategorySituation.isIso_derivedModuleLowerShriekForgetComparison, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/ProjectionModuleDerivedLowerShriek.lean, line 354. The attribute's comment: “forget ∘ Lπ_! = Lπ_!^{Ab} ∘ forget: the canonical comparison of Stacks 07AE is an isomorphism”.

Stacks 09CY, forget ∘ Lπ_! = Lπ_!^{Ab} ∘ forget. The canonical comparison Lπ_!^{Ab} ∘ forget ⟶ forget ∘ Lπ_! of Stacks 07AE is an isomorphism. This is Stacks 08PC part (4) in the situation of the remark.

instance isIso_derivedModuleLowerShriekForgetComparison :
    IsIso s.derivedModuleLowerShriekForgetComparison

Stacks.Sites.FibredCategory.FibredCategorySituation.moduleLowerShriekAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/ProjectionModuleLowerShriek.lean, line 164. The attribute's comment: “the module-level π_! of Situation 08P8 and its adjunction π_! ⊣ π^*”.

Stacks 09CY, the module-level π_!. The lower-shriek functor π_! on sheaves of modules is left adjoint to π^* = π⁻¹, restriction of sheaves of modules along p.

def moduleLowerShriekAdjunction : s.moduleLowerShriek ⊣ s.sheafModuleRestriction

Stacks.Sites.FibredCategory.FibredCategorySituation.isIso_moduleLowerShriekForgetComparison, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/ProjectionModuleLowerShriek.lean, line 204. The attribute's comment: “forget ∘ π_! = π_!^{Ab} ∘ forget: the canonical comparison of Stacks 0798 is an isomorphism”.

Stacks 09CY, forget ∘ π_! = π_!^{Ab} ∘ forget. The canonical comparison π_!^{Ab} ∘ forget ⟶ forget ∘ π_! of Stacks 0798 between lower shriek of abelian sheaves and lower shriek of sheaves of modules, for the projection of a fibred category, is an isomorphism.

By the criterion of Stacks 0798 this reduces to the canonical maps (π_U)_!^{Ab} O_U ⟶ O_{p(U)}, which are isomorphisms by isIso_localizedStructureSheafComparison_baseModuleRing. This is Stacks 08PC part (2) in the situation of the remark.

instance isIso_moduleLowerShriekForgetComparison :
    IsIso s.moduleLowerShriekForgetComparison

Tag 08PD, a remark

Tag 08PD in the Stacks Project.

Stacks.Sites.FibredCategory.MorphismSituation.derivedAbelianLowerShriekCompIso', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/CanonicalDerivedLowerShriekMap.lean, line 92. The attribute's comment: “the identification Lπ'_! = Lπ_! ∘ Lg_!”.

Stacks 08PD, the identification Lπ'_! = Lπ_! ∘ Lg_!, for every situation of Stacks 08PA. The three derived lower-shriek functors are left adjoint to the three derived restrictions, by Stacks 07AC at the three discharged acyclicity statements, and restriction to the source fibred category is restriction to the target followed by restriction along the 1-morphism; so this is uniqueness of left adjoints applied to derivedAbelianInverseImageCompIso.

def derivedAbelianLowerShriekCompIso' :
    S.derivedAbelianLowerShriek ⋙ S.derivedTotalAbelianLowerShriek ≅
      S.derivedSourceAbelianLowerShriek

Stacks.Sites.FibredCategory.MorphismSituation.canonicalDerivedLowerShriekMap', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/CanonicalDerivedLowerShriekMap.lean, line 118. The attribute's comment: “canonical map”.

Stacks 08PD, the canonical map, for every situation of Stacks 08PA. Let F be an abelian sheaf on C, let F' be an abelian sheaf on C' and let t : F' ⟶ g⁻¹F be a map of abelian sheaves. The canonical map Lπ'_!(F') ⟶ Lπ_!(F) is the identification Lπ'_! = Lπ_! ∘ Lg_! followed by Lπ_! applied to the composite of the comparison Lg_!(F') ⟶ g_!F' with the adjoint g_!F' ⟶ F of t.

def canonicalDerivedLowerShriekMap'
    (F : Sheaf S.totalTopology AddCommGrpCat.{max w u₀ u₁ u₂ v₀ v₁ v₂})
    (F' : Sheaf S.sourceTopology AddCommGrpCat.{max w u₀ u₁ u₂ v₀ v₁ v₂})
    (t : F' ⟶ S.abelianInverseImage.obj F) :
    S.derivedSourceAbelianLowerShriek.obj ((DerivedCategory.singleFunctor
        (Sheaf S.sourceTopology AddCommGrpCat.{max w u₀ u₁ u₂ v₀ v₁ v₂}) 0).obj F') ⟶
      S.derivedTotalAbelianLowerShriek.obj ((DerivedCategory.singleFunctor
        (Sheaf S.totalTopology AddCommGrpCat.{max w u₀ u₁ u₂ v₀ v₁ v₂}) 0).obj F)

Stacks.Sites.FibredCategory.MorphismSituation.derivedAbelianLowerShriekCompIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/DerivedLowerShriekFunctoriality.lean, line 476. The attribute's comment: “the identification Lπ'_! = Lπ_! ∘ Lg_!”.

The identification Lπ'_! = Lπ_! ∘ Lg_!, the isomorphism of left adjoints induced by derivedAbelianInverseImageCompIso.

def derivedAbelianLowerShriekCompIso (h : S.AbelianLowerShriekAcyclic)
    (hp : S.TotalAbelianLowerShriekAcyclic) (hp' : S.SourceAbelianLowerShriekAcyclic) :
    S.derivedAbelianLowerShriek ⋙ S.derivedTotalAbelianLowerShriek ≅
      S.derivedSourceAbelianLowerShriek

Stacks.Sites.FibredCategory.MorphismSituation.canonicalDerivedLowerShriekMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/DerivedLowerShriekFunctoriality.lean, line 524. The attribute's comment: “canonical map”.

The canonical map. Let F be an abelian sheaf on C, let F' be an abelian sheaf on C' and let t : F' ⟶ g⁻¹F be a map of abelian sheaves. The canonical map Lπ'_!(F') ⟶ Lπ_!(F) is the identification Lπ'_! = Lπ_! ∘ Lg_! followed by Lπ_! applied to the composite of the comparison Lg_!(F') ⟶ g_!F' with the adjoint g_!F' ⟶ F of t.

def canonicalDerivedLowerShriekMap (h : S.AbelianLowerShriekAcyclic)
    (hp : S.TotalAbelianLowerShriekAcyclic) (hp' : S.SourceAbelianLowerShriekAcyclic)
    (F : Sheaf S.totalTopology AddCommGrpCat.{max w u₀ u₁ u₂ v₀ v₁ v₂})
    (F' : Sheaf S.sourceTopology AddCommGrpCat.{max w u₀ u₁ u₂ v₀ v₁ v₂})
    (t : F' ⟶ S.abelianInverseImage.obj F) :
    S.derivedSourceAbelianLowerShriek.obj ((DerivedCategory.singleFunctor
        (Sheaf S.sourceTopology AddCommGrpCat.{max w u₀ u₁ u₂ v₀ v₁ v₂}) 0).obj F') ⟶
      S.derivedTotalAbelianLowerShriek.obj ((DerivedCategory.singleFunctor
        (Sheaf S.totalTopology AddCommGrpCat.{max w u₀ u₁ u₂ v₀ v₁ v₂}) 0).obj F)

Tag 08PE, a lemma

Tag 08PE in the Stacks Project.

Stacks.Sites.FibredCategory.fiberwiseColimitFormula, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/FibredCategory/LowerShriekAsAFibrewiseColimit.lean, line 333.

Stacks 08PE. The lower shriek of an abelian sheaf along the projection of a fibred category is the sheaf associated to the presheaf of fibrewise colimits, with restriction maps induced by the chosen cartesian lifts.

def fiberwiseColimitFormula
    [HasWeakSheafify s.base.J AddCommGrpCat.{max w uD vD uC vC}] :
    FiberwiseColimitFormula s

Sources

• Section 21.38, Tag 08RV
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Sites.FibredCategory.FibredCategorySituation.totalRingedTopos · Stacks.Sites.FibredCategory.FibredCategorySituation.ringedProjection · Stacks.Sites.FibredCategory.FibredCategorySituation · Stacks.Sites.FibredCategory.FibredCategorySituation.inducedProjection · Stacks.Sites.FibredCategory.FibredCategorySituation.commRingRingedProjection · Stacks.Sites.FibredCategory.localizedProjectionSection · Stacks.Sites.FibredCategory.MorphismSituation.ringedToposDiagram · Stacks.Sites.FibredCategory.MorphismSituation

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.