21.28 Formalities on… to 21.34 Hom complexes

Section21.28 Formalities on cohomological descent #

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

Tag 0D7Q, a lemma

Tag 0D7Q in the Stacks Project.

CategoryTheory.Adjunction.unitIsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/UnitAndCounitIsomorphisms.lean, line 89. The attribute's comment: “variant: the subcategory of objects at which the unit is invertible, for an arbitrary adjunction F ⊣ G; the tag, for the derived adjunction Lf^ ⊣ Rf_ of a morphism of ringed topoi, is Stacks.Cohomology.CohomologicalDescent.unitIsIso_saturated_triangulated_fullyFaithful”.

The objects K of the source of the left adjoint of an adjunction F ⊣ G at which the unit K ⟶ G (F K) is invertible.

def unitIsIso : ObjectProperty C

CategoryTheory.Adjunction.isClosedUnderIsomorphisms_unitIsIso, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/UnitAndCounitIsomorphisms.lean, line 133. The attribute's comment: “variant: the unit subcategory is strictly full, for an arbitrary adjunction F ⊣ G; the tag, for the derived adjunction Lf^ ⊣ Rf_ of a morphism of ringed topoi, is Stacks.Cohomology.CohomologicalDescent.unitIsIso_saturated_triangulated_fullyFaithful”.

The unit subcategory is strictly full: it is closed under isomorphisms, by naturality of the unit.

lemma isClosedUnderIsomorphisms_unitIsIso : adj.unitIsIso.IsClosedUnderIsomorphisms

CategoryTheory.Adjunction.unitIsIso_isSaturated, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/UnitAndCounitIsomorphisms.lean, line 149. The attribute's comment: “variant: the unit subcategory is saturated, for an arbitrary adjunction F ⊣ G; the tag, for the derived adjunction Lf^ ⊣ Rf_ of a morphism of ringed topoi, is Stacks.Cohomology.CohomologicalDescent.unitIsIso_saturated_triangulated_fullyFaithful”.

The unit subcategory is saturated: a direct summand of an object at which the unit is invertible is again such an object.

instance unitIsIso_isSaturated [HasZeroMorphisms C] : adj.unitIsIso.IsSaturated

CategoryTheory.Adjunction.fullyFaithfulιCompLeftAdjoint, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/UnitAndCounitIsomorphisms.lean, line 166. The attribute's comment: “variant: the left adjoint is fully faithful on the unit subcategory, for an arbitrary adjunction F ⊣ G; the tag, for the derived adjunction Lf^ ⊣ Rf_ of a morphism of ringed topoi, is Stacks.Cohomology.CohomologicalDescent.unitIsIso_saturated_triangulated_fullyFaithful”.

The left adjoint is fully faithful on the unit subcategory. The preimage of g : F K ⟶ F L is the morphism K ⟶ G (F L) adjoint to g, followed by the inverse of the unit at L.

noncomputable def fullyFaithfulιCompLeftAdjoint : (adj.unitIsIso.ι ⋙ F).FullyFaithful

CategoryTheory.Adjunction.unitIsIso_isTriangulated, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/UnitAndCounitIsomorphisms.lean, line 256. The attribute's comment: “variant: the unit subcategory is triangulated, for a triangulated adjunction, for an arbitrary adjunction F ⊣ G; the tag, for the derived adjunction Lf^ ⊣ Rf_ of a morphism of ringed topoi, is Stacks.Cohomology.CohomologicalDescent.unitIsIso_saturated_triangulated_fullyFaithful”.

The unit subcategory is triangulated: it contains the zero object, is stable under the shift because the unit commutes with it, and passes from two vertices of a distinguished triangle to the third by the five lemma for triangles.

instance unitIsIso_isTriangulated : adj.unitIsIso.IsTriangulated

Stacks.Cohomology.CohomologicalDescent.unitIsIso_saturated_triangulated_fullyFaithful, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/UnitAndCounitIsomorphismsOfToposHom.lean, line 105.

The subcategory of D(O_D) on which the unit of Lf^* ⊣ Rf_* is invertible. For a morphism of ringed topoi f : (Sh(C), O_C) ⟶ (Sh(D), O_D), the full subcategory D' of D(O_D) of the objects K such that the unit K ⟶ Rf_* Lf^* K is an isomorphism is strictly full (closed under isomorphisms), saturated and triangulated, and Lf^* : D' ⥤ D(O_C) is full and faithful.

theorem unitIsIso_saturated_triangulated_fullyFaithful :
    (derivedAdjunction f).unitIsIso.IsClosedUnderIsomorphisms ∧
      (derivedAdjunction f).unitIsIso.IsSaturated ∧
      (derivedAdjunction f).unitIsIso.IsTriangulated ∧
      ((derivedAdjunction f).unitIsIso.ι ⋙ derivedPullback f).Full ∧
      ((derivedAdjunction f).unitIsIso.ι ⋙ derivedPullback f).Faithful

Tag 0D7R, a lemma

Tag 0D7R in the Stacks Project.

CategoryTheory.Adjunction.counitIsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/UnitAndCounitIsomorphisms.lean, line 96. The attribute's comment: “variant: the subcategory of objects at which the counit is invertible, for an arbitrary adjunction F ⊣ G; the tag, for the derived adjunction Lf^ ⊣ Rf_ of a morphism of ringed topoi, is Stacks.Cohomology.CohomologicalDescent.counitIsIso_saturated_triangulated_fullyFaithful”.

The objects K of the source of the right adjoint of an adjunction F ⊣ G at which the counit F (G K) ⟶ K is invertible.

def counitIsIso : ObjectProperty D

CategoryTheory.Adjunction.isClosedUnderIsomorphisms_counitIsIso, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/UnitAndCounitIsomorphisms.lean, line 141. The attribute's comment: “variant: the counit subcategory is strictly full, for an arbitrary adjunction F ⊣ G; the tag, for the derived adjunction Lf^ ⊣ Rf_ of a morphism of ringed topoi, is Stacks.Cohomology.CohomologicalDescent.counitIsIso_saturated_triangulated_fullyFaithful”.

The counit subcategory is strictly full: it is closed under isomorphisms, by naturality of the counit.

lemma isClosedUnderIsomorphisms_counitIsIso : adj.counitIsIso.IsClosedUnderIsomorphisms

CategoryTheory.Adjunction.counitIsIso_isSaturated, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/UnitAndCounitIsomorphisms.lean, line 157. The attribute's comment: “variant: the counit subcategory is saturated, for an arbitrary adjunction F ⊣ G; the tag, for the derived adjunction Lf^ ⊣ Rf_ of a morphism of ringed topoi, is Stacks.Cohomology.CohomologicalDescent.counitIsIso_saturated_triangulated_fullyFaithful”.

The counit subcategory is saturated: a direct summand of an object at which the counit is invertible is again such an object.

instance counitIsIso_isSaturated [HasZeroMorphisms D] : adj.counitIsIso.IsSaturated

CategoryTheory.Adjunction.fullyFaithfulιCompRightAdjoint, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/UnitAndCounitIsomorphisms.lean, line 191. The attribute's comment: “variant: the right adjoint is fully faithful on the counit subcategory, for an arbitrary adjunction F ⊣ G; the tag, for the derived adjunction Lf^ ⊣ Rf_ of a morphism of ringed topoi, is Stacks.Cohomology.CohomologicalDescent.counitIsIso_saturated_triangulated_fullyFaithful”. References: SGA 4 I (6.4), “more general”.

The right adjoint is fully faithful on the counit subcategory. The preimage of g : G A ⟶ G B is the inverse of the counit at A, followed by the morphism F (G A) ⟶ B adjoint to g.

noncomputable def fullyFaithfulιCompRightAdjoint : (adj.counitIsIso.ι ⋙ G).FullyFaithful

CategoryTheory.Adjunction.counitIsIso_isTriangulated, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/UnitAndCounitIsomorphisms.lean, line 263. The attribute's comment: “variant: the counit subcategory is triangulated, for a triangulated adjunction, for an arbitrary adjunction F ⊣ G; the tag, for the derived adjunction Lf^ ⊣ Rf_ of a morphism of ringed topoi, is Stacks.Cohomology.CohomologicalDescent.counitIsIso_saturated_triangulated_fullyFaithful”.

The counit subcategory is triangulated.

instance counitIsIso_isTriangulated : adj.counitIsIso.IsTriangulated

Stacks.Cohomology.CohomologicalDescent.counitIsIso_saturated_triangulated_fullyFaithful, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/UnitAndCounitIsomorphismsOfToposHom.lean, line 121.

The subcategory of D(O_C) on which the counit of Lf^* ⊣ Rf_* is invertible. For a morphism of ringed topoi f : (Sh(C), O_C) ⟶ (Sh(D), O_D), the full subcategory D' of D(O_C) of the objects K such that the counit Lf^* Rf_* K ⟶ K is an isomorphism is strictly full (closed under isomorphisms), saturated and triangulated, and Rf_* : D' ⥤ D(O_D) is full and faithful.

theorem counitIsIso_saturated_triangulated_fullyFaithful :
    (derivedAdjunction f).counitIsIso.IsClosedUnderIsomorphisms ∧
      (derivedAdjunction f).counitIsIso.IsSaturated ∧
      (derivedAdjunction f).counitIsIso.IsTriangulated ∧
      ((derivedAdjunction f).counitIsIso.ι ⋙ derivedPushforward (X := X) (Y := Y) f).Full ∧
      ((derivedAdjunction f).counitIsIso.ι ⋙ derivedPushforward (X := X) (Y := Y) f).Faithful

Tag 0D7S, a lemma

Tag 0D7S in the Stacks Project.

Stacks.Cohomology.CohomologicalDescent.isIso_derivedCounit_app_of_isIso_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/BoundedBelowDescent.lean, line 242.

Stacks 0D7S. Let f be a flat morphism of ringed topoi and let K be a bounded below object of D(O_X). If the counit Lf^*Rf_*H^q(K) ⟶ H^q(K) of the derived adjunction is an isomorphism for every q, with each cohomology object placed in degree zero, then the counit Lf^*Rf_*K ⟶ K is an isomorphism.

This is the previous statement with the pair of functors reversed: here it is (Rf_* ⋙ Lf^*, 𝟭), and the theorem applied at the counit.

theorem isIso_derivedCounit_app_of_isIso_homology :
    letI := f.pullbackTopos_preservesFiniteLimits hmos hf
    letI := f.pullbackTopos_preservesFiniteColimits
    letI := pullbackOnHomotopy_hasLeftDerivedFunctor_of_exact f
    ∀ (K : DerivedCategory (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))),
      DerivedCategory.TStructure.t.plus K →
      (∀ q : ℤ, IsIso ((derivedPullbackPushforwardAdjunctionOfExact f).counit.app
        ((DerivedCategory.singleFunctor
            (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) 0).obj
          ((DerivedCategory.homologyFunctor
            (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) q).obj K)))) →
      IsIso ((derivedPullbackPushforwardAdjunctionOfExact f).counit.app K)

Tag 0D7T, a lemma

Tag 0D7T in the Stacks Project.

Stacks.Cohomology.CohomologicalDescent.isIso_derivedUnit_app_of_isIso_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/BoundedBelowDescent.lean, line 212.

Stacks 0D7T. Let f be a flat morphism of ringed topoi and let K be a bounded below object of D(O_Y). If the unit H^q(K) ⟶ Rf_*Lf^*H^q(K) of the derived adjunction is an isomorphism for every q, with each cohomology object placed in degree zero, then the unit K ⟶ Rf_*Lf^*K is an isomorphism.

The pair of functors is (𝟭, Lf^* ⋙ Rf_*): both are exact, both commute with the shift, and both carry D^{≥m} into D^{≥m}, so this is CategoryTheory.NatTrans.isIso_app_of_isGE at the unit.

theorem isIso_derivedUnit_app_of_isIso_homology :
    letI := f.pullbackTopos_preservesFiniteLimits hmos hf
    letI := f.pullbackTopos_preservesFiniteColimits
    letI := pullbackOnHomotopy_hasLeftDerivedFunctor_of_exact f
    ∀ (K : DerivedCategory (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))),
      DerivedCategory.TStructure.t.plus K →
      (∀ q : ℤ, IsIso ((derivedPullbackPushforwardAdjunctionOfExact f).unit.app
        ((DerivedCategory.singleFunctor
            (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) 0).obj
          ((DerivedCategory.homologyFunctor
            (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) q).obj K)))) →
      IsIso ((derivedPullbackPushforwardAdjunctionOfExact f).unit.app K)

Tag 0D7U, a lemma

Tag 0D7U in the Stacks Project.

Stacks.Cohomology.CohomologicalDescent.derivedCategoryBPlus_derivedPullback_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/BoundedBelowEquivalence.lean, line 307. The attribute's comment: “derived pullback”.

Stacks 0D7U, the assertion that derived pullback restricts. Let f be a flat morphism of ringed topoi and let 𝒜 ⊂ Mod(𝒪), 𝒜' ⊂ Mod(𝒪') be weak Serre subcategories with f^*𝒜' ⊂ 𝒜. Then Lf^* carries D⁺_{𝒜'}(𝒪') into D⁺_𝒜(𝒪).

theorem derivedCategoryBPlus_derivedPullback_obj :
    letI := f.pullbackTopos_preservesFiniteLimits hmos hf
    letI := f.pullbackTopos_preservesFiniteColimits
    letI := pullbackOnHomotopy_hasLeftDerivedFunctor_of_exact f
    ∀ (K : DerivedCategory (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))),
      DerivedCategoryB.derivedCategoryBPlus A' K →
        DerivedCategoryB.derivedCategoryBPlus A ((derivedPullback f).obj K)

Stacks.Cohomology.CohomologicalDescent.derivedCategoryBPlus_derivedPushforward_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/BoundedBelowEquivalence.lean, line 328. The attribute's comment: “derived pushforward”.

Stacks 0D7U, the assertion that derived pushforward restricts. Under the hypotheses of the source — f flat, f^* inducing an equivalence 𝒜' ⟶ 𝒜, and the unit ℱ' ⟶ Rf_*f^*ℱ' invertible on 𝒜' — the pushforward Rf_* carries D⁺_𝒜(𝒪) into D⁺_{𝒜'}(𝒪').

theorem derivedCategoryBPlus_derivedPushforward_obj :
    letI := f.pullbackTopos_preservesFiniteLimits hmos hf
    letI := f.pullbackTopos_preservesFiniteColimits
    letI := pullbackOnHomotopy_hasLeftDerivedFunctor_of_exact f
    (∀ M, A' M → IsIso ((derivedPullbackPushforwardAdjunctionOfExact f).unit.app
      ((DerivedCategory.singleFunctor
        (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) 0).obj M))) →
      ∀ (K : DerivedCategory (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))),
        DerivedCategoryB.derivedCategoryBPlus A K →
          DerivedCategoryB.derivedCategoryBPlus A' ((derivedPushforward f).obj K)

Stacks.Cohomology.CohomologicalDescent.derivedPullbackEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/BoundedBelowEquivalence.lean, line 351. The attribute's comment: “equivalence”.

Stacks 0D7U. For a flat morphism of ringed topoi f and weak Serre subcategories 𝒜 ⊂ Mod(𝒪), 𝒜' ⊂ Mod(𝒪') such that f^* induces an equivalence 𝒜' ⟶ 𝒜 and the unit ℱ' ⟶ Rf_*f^*ℱ' is invertible for every ℱ' of 𝒜', the derived pullback is an equivalence D⁺_{𝒜'}(𝒪') ≌ D⁺_𝒜(𝒪).

The hypothesis on the unit propagates from 𝒜' to all of D⁺_{𝒜'}(𝒪') by Tag 0D7T, and the corresponding statement for the counit from 𝒜 to all of D⁺_𝒜(𝒪) by Tag 0D7S.

noncomputable def derivedPullbackEquivalence
    (hUnit :
      letI := f.pullbackTopos_preservesFiniteLimits hmos hf
      letI := f.pullbackTopos_preservesFiniteColimits
      letI := pullbackOnHomotopy_hasLeftDerivedFunctor_of_exact f
      ∀ M, A' M → IsIso ((derivedPullbackPushforwardAdjunctionOfExact f).unit.app
        ((DerivedCategory.singleFunctor
          (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) 0).obj M))) :
    (DerivedCategoryB.derivedCategoryBPlus A').FullSubcategory ≌
      (DerivedCategoryB.derivedCategoryBPlus A).FullSubcategory

Stacks.Cohomology.CohomologicalDescent.derivedPullbackEquivalence_functor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/BoundedBelowEquivalence.lean, line 374. The attribute's comment: “forward functor”.

Stacks 0D7U, the identification of the forward functor of the equivalence with the restriction of the derived pullback.

theorem derivedPullbackEquivalence_functor
    (hUnit :
      letI := f.pullbackTopos_preservesFiniteLimits hmos hf
      letI := f.pullbackTopos_preservesFiniteColimits
      letI := pullbackOnHomotopy_hasLeftDerivedFunctor_of_exact f
      ∀ M, A' M → IsIso ((derivedPullbackPushforwardAdjunctionOfExact f).unit.app
        ((DerivedCategory.singleFunctor
          (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) 0).obj M))) :
    letI := f.pullbackTopos_preservesFiniteLimits hmos hf
    letI := f.pullbackTopos_preservesFiniteColimits
    letI := pullbackOnHomotopy_hasLeftDerivedFunctor_of_exact f
    (derivedPullbackEquivalence f A A' hmos hf hA hEquiv hUnit).functor =
      (DerivedCategoryB.derivedCategoryBPlus A).lift
        ((DerivedCategoryB.derivedCategoryBPlus A').ι ⋙ derivedPullback f)
        (fun K ↦ derivedCategoryBPlus_derivedPullback_obj f A A' hmos hf hA K.obj K.property)

Stacks.Cohomology.CohomologicalDescent.derivedPullbackEquivalence_inverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/BoundedBelowEquivalence.lean, line 394. The attribute's comment: “quasi-inverse”.

Stacks 0D7U, the identification of the quasi-inverse of the equivalence with the restriction of the derived pushforward.

theorem derivedPullbackEquivalence_inverse
    (hUnit :
      letI := f.pullbackTopos_preservesFiniteLimits hmos hf
      letI := f.pullbackTopos_preservesFiniteColimits
      letI := pullbackOnHomotopy_hasLeftDerivedFunctor_of_exact f
      ∀ M, A' M → IsIso ((derivedPullbackPushforwardAdjunctionOfExact f).unit.app
        ((DerivedCategory.singleFunctor
          (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) 0).obj M))) :
    letI := f.pullbackTopos_preservesFiniteLimits hmos hf
    letI := f.pullbackTopos_preservesFiniteColimits
    letI := pullbackOnHomotopy_hasLeftDerivedFunctor_of_exact f
    (derivedPullbackEquivalence f A A' hmos hf hA hEquiv hUnit).inverse =
      (DerivedCategoryB.derivedCategoryBPlus A').lift
        ((DerivedCategoryB.derivedCategoryBPlus A).ι ⋙ derivedPushforward f)
        (fun K ↦ derivedCategoryBPlus_derivedPushforward_obj f A A' hmos hf hA hEquiv hUnit
          K.obj K.property)

Tag 0D7V, a lemma

Tag 0D7V in the Stacks Project.

Stacks.Cohomology.CohomologicalDescent.derivedCategoryB_derivedPullback_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/UnboundedEquivalence.lean, line 512. The attribute's comment: “derived pullback”.

Stacks 0D7V, the assertion that derived pullback restricts. Let f be a flat morphism of ringed topoi and let 𝒜 ⊂ Mod(𝒪), 𝒜' ⊂ Mod(𝒪') be weak Serre subcategories with f^*𝒜' ⊂ 𝒜. Then Lf^* carries D_{𝒜'}(𝒪') into D_𝒜(𝒪).

theorem derivedCategoryB_derivedPullback_obj :
    letI := f.pullbackTopos_preservesFiniteLimits hmos hf
    letI := f.pullbackTopos_preservesFiniteColimits
    letI := pullbackOnHomotopy_hasLeftDerivedFunctor_of_exact f
    ∀ (K : DerivedCategory (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))),
      DerivedCategoryB.derivedCategoryB A' K →
        DerivedCategoryB.derivedCategoryB A ((derivedPullback f).obj K)

Stacks.Cohomology.CohomologicalDescent.derivedCategoryB_derivedPushforward_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/UnboundedEquivalence.lean, line 530. The attribute's comment: “derived pushforward”.

Stacks 0D7V, the assertion that derived pushforward restricts. Under the hypotheses of the source — f flat, f^* inducing an equivalence 𝒜' ⟶ 𝒜, the unit ℱ' ⟶ Rf_*f^*ℱ' invertible on 𝒜', and both sites satisfying the Olsson--Laszlo hypothesis of Tag 0D6R — the pushforward Rf_* carries D_𝒜(𝒪) into D_{𝒜'}(𝒪').

theorem derivedCategoryB_derivedPushforward_obj :
    letI := f.pullbackTopos_preservesFiniteLimits hmos hf
    letI := f.pullbackTopos_preservesFiniteColimits
    letI := pullbackOnHomotopy_hasLeftDerivedFunctor_of_exact f
    (∀ M, A' M → IsIso ((derivedPullbackPushforwardAdjunctionOfExact f).unit.app
      ((DerivedCategory.singleFunctor (SheafOfModules.{w}
          (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) 0).obj M))) →
      ∀ (K : DerivedCategory (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))),
        DerivedCategoryB.derivedCategoryB A K →
          DerivedCategoryB.derivedCategoryB A' ((derivedPushforward f).obj K)

Stacks.Cohomology.CohomologicalDescent.derivedPullbackEquivalenceUnbounded, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/UnboundedEquivalence.lean, line 564. The attribute's comment: “equivalence”.

Stacks 0D7V. Let f : (Sh(C), 𝒪) ⟶ (Sh(C'), 𝒪') be a flat morphism of ringed topoi and let 𝒜 ⊂ Mod(𝒪), 𝒜' ⊂ Mod(𝒪') be weak Serre subcategories such that f^* induces an equivalence 𝒜' ⟶ 𝒜 and the unit ℱ' ⟶ Rf_*f^*ℱ' is invertible for every ℱ' of 𝒜', and assume that C, 𝒪, 𝒜 and C', 𝒪', 𝒜' both satisfy the standing hypothesis of Tag 0D6R. Then the derived pullback is an equivalence D_{𝒜'}(𝒪') ≌ D_𝒜(𝒪).

The hypothesis on the unit propagates from 𝒜' to all of D⁺_{𝒜'}(𝒪') by Tag 0D7T and the corresponding statement for the counit from 𝒜 to all of D⁺_𝒜(𝒪) by Tag 0D7S; the Olsson--Laszlo hypotheses then carry both from the bounded below subcategories to the whole derived categories, through Tag 0D6U.

def derivedPullbackEquivalenceUnbounded
    (hUnit :
      letI := f.pullbackTopos_preservesFiniteLimits hmos hf
      letI := f.pullbackTopos_preservesFiniteColimits
      letI := pullbackOnHomotopy_hasLeftDerivedFunctor_of_exact f
      ∀ M, A' M → IsIso ((derivedPullbackPushforwardAdjunctionOfExact f).unit.app
        ((DerivedCategory.singleFunctor (SheafOfModules.{w}
            (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) 0).obj M))) :
    (DerivedCategoryB.derivedCategoryB A').FullSubcategory ≌
      (DerivedCategoryB.derivedCategoryB A).FullSubcategory

Stacks.Cohomology.CohomologicalDescent.derivedPullbackEquivalenceUnbounded_functor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/UnboundedEquivalence.lean, line 587. The attribute's comment: “forward functor”.

Stacks 0D7V, the identification of the forward functor of the equivalence with the restriction of the derived pullback.

theorem derivedPullbackEquivalenceUnbounded_functor
    (hUnit :
      letI := f.pullbackTopos_preservesFiniteLimits hmos hf
      letI := f.pullbackTopos_preservesFiniteColimits
      letI := pullbackOnHomotopy_hasLeftDerivedFunctor_of_exact f
      ∀ M, A' M → IsIso ((derivedPullbackPushforwardAdjunctionOfExact f).unit.app
        ((DerivedCategory.singleFunctor (SheafOfModules.{w}
            (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) 0).obj M))) :
    letI := f.pullbackTopos_preservesFiniteLimits hmos hf
    letI := f.pullbackTopos_preservesFiniteColimits
    letI := pullbackOnHomotopy_hasLeftDerivedFunctor_of_exact f
    (derivedPullbackEquivalenceUnbounded f A A' hmos hf hA hEquiv
      B basisCover degreeBound coverings vanishing
      B' basisCover' degreeBound' coverings' vanishing' hUnit).functor =
      (DerivedCategoryB.derivedCategoryB A).lift
        ((DerivedCategoryB.derivedCategoryB A').ι ⋙ derivedPullback f)
        (fun K ↦ derivedCategoryB_derivedPullback_obj f A A' hmos hf hA K.obj K.property)

Stacks.Cohomology.CohomologicalDescent.derivedPullbackEquivalenceUnbounded_inverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/UnboundedEquivalence.lean, line 609. The attribute's comment: “quasi-inverse”.

Stacks 0D7V, the identification of the quasi-inverse of the equivalence with the restriction of the derived pushforward.

theorem derivedPullbackEquivalenceUnbounded_inverse
    (hUnit :
      letI := f.pullbackTopos_preservesFiniteLimits hmos hf
      letI := f.pullbackTopos_preservesFiniteColimits
      letI := pullbackOnHomotopy_hasLeftDerivedFunctor_of_exact f
      ∀ M, A' M → IsIso ((derivedPullbackPushforwardAdjunctionOfExact f).unit.app
        ((DerivedCategory.singleFunctor (SheafOfModules.{w}
            (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) 0).obj M))) :
    letI := f.pullbackTopos_preservesFiniteLimits hmos hf
    letI := f.pullbackTopos_preservesFiniteColimits
    letI := pullbackOnHomotopy_hasLeftDerivedFunctor_of_exact f
    (derivedPullbackEquivalenceUnbounded f A A' hmos hf hA hEquiv
      B basisCover degreeBound coverings vanishing
      B' basisCover' degreeBound' coverings' vanishing' hUnit).inverse =
      (DerivedCategoryB.derivedCategoryB A').lift
        ((DerivedCategoryB.derivedCategoryB A).ι ⋙ derivedPushforward f)
        (fun K ↦ derivedCategoryB_derivedPushforward_obj f A A' hmos hf hA hEquiv
          B basisCover degreeBound coverings vanishing
          B' basisCover' degreeBound' coverings' vanishing' hUnit K.obj K.property)

Tag 0D7W, a lemma

Tag 0D7W in the Stacks Project.

Stacks.Cohomology.CohomologicalDescent.derivedCategoryB_derivedPullback_obj_relative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/UnboundedEquivalenceRelativeSituation.lean, line 429. The attribute's comment: “derived pullback”.

Stacks 0D7W, the assertion that derived pullback restricts. Let f be a flat morphism of ringed sites and let 𝒜 ⊂ Mod(𝒪), 𝒜' ⊂ Mod(𝒪') be weak Serre subcategories with f^*𝒜' ⊂ 𝒜. Then Lf^* carries D_{𝒜'}(𝒪') into D_𝒜(𝒪). Neither standing hypothesis is needed: derived pullback is degreewise pullback, which is exact, so Hʲ(Lf^*K) is f^*Hʲ(K), and f^* carries 𝒜' into 𝒜.

theorem derivedCategoryB_derivedPullback_obj_relative :
    letI := f.toRingedToposSiteHom.pullbackTopos_preservesFiniteLimits
      f.isMorphismOfSites_toRingedToposSiteHom hf
    letI := f.toRingedToposSiteHom.pullbackTopos_preservesFiniteColimits
    letI := pullbackOnHomotopy_hasLeftDerivedFunctor_of_exact f.toRingedToposSiteHom
    ∀ (K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))),
      DerivedCategoryB.derivedCategoryB A' K →
        DerivedCategoryB.derivedCategoryB A
          ((derivedPullback f.toRingedToposSiteHom).obj K)

Stacks.Cohomology.CohomologicalDescent.derivedCategoryB_derivedPushforward_obj_relative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/UnboundedEquivalenceRelativeSituation.lean, line 495. The attribute's comment: “derived pushforward”.

Stacks 0D7W, the assertion that derived pushforward restricts. Under the hypotheses of the source — f flat, f^* inducing an equivalence 𝒜' ⟶ 𝒜, the unit ℱ' ⟶ Rf_*f^*ℱ' invertible on 𝒜', the source satisfying the Olsson--Laszlo hypothesis of Tag 0D6R and f together with 𝒜 satisfying the relative hypothesis of Tag 0D6V — the pushforward Rf_* carries D_𝒜(𝒪) into D_{𝒜'}(𝒪').

theorem derivedCategoryB_derivedPushforward_obj_relative
    (hUnit :
      letI := f.toRingedToposSiteHom.pullbackTopos_preservesFiniteLimits
        f.isMorphismOfSites_toRingedToposSiteHom hf
      letI := f.toRingedToposSiteHom.pullbackTopos_preservesFiniteColimits
      letI := pullbackOnHomotopy_hasLeftDerivedFunctor_of_exact f.toRingedToposSiteHom
      ∀ M, A' M → IsIso
        ((derivedPullbackPushforwardAdjunctionOfExact f.toRingedToposSiteHom).unit.app
          ((DerivedCategory.singleFunctor (SheafOfModules.{u}
              (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) 0).obj M))) :
    letI := f.toRingedToposSiteHom.pullbackTopos_preservesFiniteLimits
      f.isMorphismOfSites_toRingedToposSiteHom hf
    letI := f.toRingedToposSiteHom.pullbackTopos_preservesFiniteColimits
    letI := pullbackOnHomotopy_hasLeftDerivedFunctor_of_exact f.toRingedToposSiteHom
    ∀ (K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))),
      DerivedCategoryB.derivedCategoryB A K →
        DerivedCategoryB.derivedCategoryB A'
          ((derivedPushforward f.toRingedToposSiteHom).obj K)

Stacks.Cohomology.CohomologicalDescent.derivedPullbackEquivalenceUnboundedRelative, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/UnboundedEquivalenceRelativeSituation.lean, line 534. The attribute's comment: “equivalence”.

Stacks 0D7W. Let f : (C, 𝒪) ⟶ (C', 𝒪') be a flat morphism of ringed sites and let 𝒜 ⊂ Mod(𝒪), 𝒜' ⊂ Mod(𝒪') be weak Serre subcategories such that f^* induces an equivalence 𝒜' ⟶ 𝒜 and the unit ℱ' ⟶ Rf_*f^*ℱ' is invertible for every ℱ' of 𝒜', and assume that C, 𝒪, 𝒜 satisfy the standing hypothesis of Tag 0D6R and that f together with 𝒜 satisfies the relative standing hypothesis of Tag 0D6V. Then the derived pullback is an equivalence D_{𝒜'}(𝒪') ≌ D_𝒜(𝒪).

The hypothesis on the unit propagates from 𝒜 to all of D⁺_𝒜(𝒪) by Tag 0D7S; the two standing hypotheses then carry the counit from the bounded below subcategory to the whole derived category, through Tag 0D6W. This is Tag 0D7V with its appeal to Tag 0D6U replaced by one to Tag 0D6W, which is the source's own description of the proof.

def derivedPullbackEquivalenceUnboundedRelative
    (hUnit :
      letI := f.toRingedToposSiteHom.pullbackTopos_preservesFiniteLimits
        f.isMorphismOfSites_toRingedToposSiteHom hf
      letI := f.toRingedToposSiteHom.pullbackTopos_preservesFiniteColimits
      letI := pullbackOnHomotopy_hasLeftDerivedFunctor_of_exact f.toRingedToposSiteHom
      ∀ M, A' M → IsIso
        ((derivedPullbackPushforwardAdjunctionOfExact f.toRingedToposSiteHom).unit.app
          ((DerivedCategory.singleFunctor (SheafOfModules.{u}
              (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) 0).obj M))) :
    (DerivedCategoryB.derivedCategoryB A').FullSubcategory ≌
      (DerivedCategoryB.derivedCategoryB A).FullSubcategory

Stacks.Cohomology.CohomologicalDescent.derivedPullbackEquivalenceUnboundedRelative_functor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/UnboundedEquivalenceRelativeSituation.lean, line 563. The attribute's comment: “forward functor”.

Stacks 0D7W, the identification of the forward functor of the equivalence with the restriction of the derived pullback.

theorem derivedPullbackEquivalenceUnboundedRelative_functor
    (hUnit :
      letI := f.toRingedToposSiteHom.pullbackTopos_preservesFiniteLimits
        f.isMorphismOfSites_toRingedToposSiteHom hf
      letI := f.toRingedToposSiteHom.pullbackTopos_preservesFiniteColimits
      letI := pullbackOnHomotopy_hasLeftDerivedFunctor_of_exact f.toRingedToposSiteHom
      ∀ M, A' M → IsIso
        ((derivedPullbackPushforwardAdjunctionOfExact f.toRingedToposSiteHom).unit.app
          ((DerivedCategory.singleFunctor (SheafOfModules.{u}
              (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) 0).obj M))) :
    letI := f.toRingedToposSiteHom.pullbackTopos_preservesFiniteLimits
      f.isMorphismOfSites_toRingedToposSiteHom hf
    letI := f.toRingedToposSiteHom.pullbackTopos_preservesFiniteColimits
    letI := pullbackOnHomotopy_hasLeftDerivedFunctor_of_exact f.toRingedToposSiteHom
    (derivedPullbackEquivalenceUnboundedRelative f hf A A' hA hEquiv
      B basisCover degreeBound coverings vanishing
      B' basisCover' degreeBound' coverings' vanishing' hUnit).functor =
      (DerivedCategoryB.derivedCategoryB A).lift
        ((DerivedCategoryB.derivedCategoryB A').ι ⋙
          derivedPullback.{u} f.toRingedToposSiteHom)
        (fun K ↦ derivedCategoryB_derivedPullback_obj_relative f hf A A' hA K.obj
          K.property)

Stacks.Cohomology.CohomologicalDescent.derivedPullbackEquivalenceUnboundedRelative_inverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/UnboundedEquivalenceRelativeSituation.lean, line 590. The attribute's comment: “quasi-inverse”.

Stacks 0D7W, the identification of the quasi-inverse of the equivalence with the restriction of the derived pushforward.

theorem derivedPullbackEquivalenceUnboundedRelative_inverse
    (hUnit :
      letI := f.toRingedToposSiteHom.pullbackTopos_preservesFiniteLimits
        f.isMorphismOfSites_toRingedToposSiteHom hf
      letI := f.toRingedToposSiteHom.pullbackTopos_preservesFiniteColimits
      letI := pullbackOnHomotopy_hasLeftDerivedFunctor_of_exact f.toRingedToposSiteHom
      ∀ M, A' M → IsIso
        ((derivedPullbackPushforwardAdjunctionOfExact f.toRingedToposSiteHom).unit.app
          ((DerivedCategory.singleFunctor (SheafOfModules.{u}
              (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) 0).obj M))) :
    letI := f.toRingedToposSiteHom.pullbackTopos_preservesFiniteLimits
      f.isMorphismOfSites_toRingedToposSiteHom hf
    letI := f.toRingedToposSiteHom.pullbackTopos_preservesFiniteColimits
    letI := pullbackOnHomotopy_hasLeftDerivedFunctor_of_exact f.toRingedToposSiteHom
    (derivedPullbackEquivalenceUnboundedRelative f hf A A' hA hEquiv
      B basisCover degreeBound coverings vanishing
      B' basisCover' degreeBound' coverings' vanishing' hUnit).inverse =
      (DerivedCategoryB.derivedCategoryB A').lift
        ((DerivedCategoryB.derivedCategoryB A).ι ⋙
          derivedPushforward.{u} f.toRingedToposSiteHom)
        (fun K ↦ derivedCategoryB_derivedPushforward_obj_relative f hf A A' hA hEquiv
          B basisCover degreeBound coverings vanishing
          B' basisCover' degreeBound' coverings' vanishing' hUnit K.obj K.property)

Sources

LeanCategoryTheory.Adjunction.unitIsIso · CategoryTheory.Adjunction.isClosedUnderIsomorphisms_unitIsIso · CategoryTheory.Adjunction.unitIsIso_isSaturated · CategoryTheory.Adjunction.fullyFaithfulιCompLeftAdjoint · CategoryTheory.Adjunction.unitIsIso_isTriangulated · Stacks.Cohomology.CohomologicalDescent.unitIsIso_saturated_triangulated_fullyFaithful · CategoryTheory.Adjunction.counitIsIso · CategoryTheory.Adjunction.isClosedUnderIsomorphisms_counitIsIso

Section21.29 Comparing two topologies, II #

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

Tag 07A8, a lemma

Tag 07A8 in the Stacks Project.

Stacks.Cohomology.CompareTopologies.isWeakSerreClass_imageOfLE_of_vanishing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/CoarseningDerivedEquivalence.lean, line 286. The attribute's comment: “the weak Serre subcategory for the coarser topology, with the dévissage step discharged”.

[Stacks, Tag 07A8], first conclusion, with no hypothesis beyond the source's. The image A' of A under ε_* is a weak Serre subcategory of Mod(R_τ'). This is Stacks.Cohomology.CompareTopologies.isWeakSerreClass_imageOfLE with its dévissage hypothesis hdev discharged by exact_map_pushforward_of_vanishing.

theorem isWeakSerreClass_imageOfLE_of_vanishing [A.IsWeakSerreClass] :
    (imageOfLE.{u, v, r, m} h R A).IsWeakSerreClass

Stacks.Cohomology.CompareTopologies.derivedPullbackEquivalenceImageOfLE, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/CoarseningDerivedEquivalence.lean, line 369. The attribute's comment: “the equivalence of derived categories given by ε^ and Rε_”.

[Stacks, Tag 07A8], second conclusion. Let J' ≤ S.J be two topologies on the category of a ringed site S, so that the identity functor of that category is the comparison morphism of ringed sites ε : (C_τ, 𝒪_τ) ⟶ (C_τ', 𝒪_τ'). Let A be a weak Serre subcategory of Mod(𝒪_τ) and let B be a set of objects such that every object has a τ'-covering by members of B and H^p_τ(U, F) vanishes for U in B, p > 0 and F in A. Then derived pullback and derived pushforward are quasi-inverse equivalences of the unbounded derived categories

D_{A'}(𝒪_τ') ≌ D_A(𝒪_τ),

where A' is the image class of the first conclusion, Stacks.Cohomology.CompareTopologies.imageOfLE.

The five assumptions of [Stacks, Tag 0D7W] are discharged as described in the module docstring. Nothing is carried: the hypotheses above are exactly the source's own, the dévissage hypothesis hdev of Stacks.Cohomology.CompareTopologies.isWeakSerre_imageOfLE being proved rather than assumed, as exact_map_pushforward_of_vanishing.

def derivedPullbackEquivalenceImageOfLE
    [HasSheafify J' AddCommGrpCat.{u}] [J'.WEqualsLocallyBijective AddCommGrpCat.{u}]
    [EnoughInjectives (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf S.O))]
    [EnoughInjectives (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf S.O).ofLE h))]
    [J'.HasSheafCompose (CategoryTheory.forget AddCommGrpCat.{u})]
    [A.IsWeakSerreClass] (B : Set S.C)
    (hB : ∀ U : S.C, ∃ 𝒰 : PreZeroHypercover.{u} U, 𝒰.sieve₀ ∈ J' U ∧ ∀ i, B (𝒰.X i))
    (hvan : ∀ U : S.C, B U → ∀ p : ℕ, 0 < p →
      ∀ F : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf S.O), A F →
      IsZero (Stacks.Cohomology.moduleCohomology
        (Stacks.SheafOfModules.Tensor.ringSheaf S.O) U p F)) :
    (DerivedCategoryB.derivedCategoryB
      (imageOfLE h (Stacks.SheafOfModules.Tensor.ringSheaf S.O) A)).FullSubcategory ≌
      (DerivedCategoryB.derivedCategoryB A).FullSubcategory

Stacks.Cohomology.CompareTopologies.derivedPullbackEquivalenceImageOfLE_functor_comp_ι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/CoarseningDerivedEquivalence.lean, line 423. The attribute's comment: “the forward functor of the equivalence is the derived pullback”.

The equivalence of [Stacks, Tag 07A8] is given by ε^*: its forward functor, followed by the inclusion of D_A(𝒪_τ) into D(𝒪_τ), is the inclusion of D_{A'}(𝒪_τ') followed by the derived pullback Lε^* = ε^*.

theorem derivedPullbackEquivalenceImageOfLE_functor_comp_ι :
    letI : (pullbackOnHomotopy (S.coarseningHom h).toRingedToposSiteHom).HasLeftDerivedFunctor
        (HomotopyCategory.quasiIso
          (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf (S.ofLe h).ringedTopos.O))
          (ComplexShape.up ℤ)) :=
      S.hasLeftDerivedFunctor_pullbackOnHomotopy_coarseningHom h
    (derivedPullbackEquivalenceImageOfLE S h A B hB hvan).functor ⋙
        (DerivedCategoryB.derivedCategoryB A).ι =
      (DerivedCategoryB.derivedCategoryB
        (imageOfLE h (Stacks.SheafOfModules.Tensor.ringSheaf S.O) A)).ι ⋙
        derivedPullback (S.coarseningHom h).toRingedToposSiteHom

Stacks.Cohomology.CompareTopologies.derivedPullbackEquivalenceImageOfLE_inverse_comp_ι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/CoarseningDerivedEquivalence.lean, line 440. The attribute's comment: “the quasi-inverse of the equivalence is the derived pushforward”.

The quasi-inverse of the equivalence of [Stacks, Tag 07A8] is Rε_*: it, followed by the inclusion of D_{A'}(𝒪_τ') into D(𝒪_τ'), is the inclusion of D_A(𝒪_τ) followed by the derived pushforward Rε_*.

theorem derivedPullbackEquivalenceImageOfLE_inverse_comp_ι :
    (derivedPullbackEquivalenceImageOfLE S h A B hB hvan).inverse ⋙
        (DerivedCategoryB.derivedCategoryB
          (imageOfLE h (Stacks.SheafOfModules.Tensor.ringSheaf S.O) A)).ι =
      (DerivedCategoryB.derivedCategoryB A).ι ⋙
        derivedPushforward (S.coarseningHom h).toRingedToposSiteHom

Stacks.Cohomology.CompareTopologies.derivedEquivalenceImageOfLE_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/DerivedWeakSerreAcrossTopologies.lean, line 442. The attribute's comment: “second conclusion: the equivalence of triangulated categories D_A(𝒪_τ) ≌ D_{A'}(𝒪_τ') given by ε^* and Rε_*”.

Stacks 07A8, second conclusion. Under the hypotheses of Stacks.Cohomology.CompareTopologies.derivedEquivalenceImageOfLE, that equivalence D_A(𝒪_τ) ≌ D_{A'}(𝒪_τ'), where A' = ε_*A, is an equivalence of triangulated categories, and it is given by ε^* and Rε_*:

it is a triangulated equivalence, for the shift structure of Lε^* on its quasi-inverse and the compatible one on its functor;

its functor, read in D(𝒪_τ'), is the derived pushforward Rε_*;

its quasi-inverse, read in D(𝒪_τ), is the derived pullback Lε^*, compatibly with the shift;

since ε^* is exact, that quasi-inverse is ε^* applied termwise to complexes.

That A' is a weak Serre subcategory of Mod(𝒪_τ'), which is what makes D_{A'}(𝒪_τ') a triangulated subcategory of D(𝒪_τ'), is the first conclusion, Stacks.Cohomology.CompareTopologies.isWeakSerre_imageOfLE_of_univLE.

theorem derivedEquivalenceImageOfLE_spec :
    haveI : (DerivedCategoryB.derivedCategoryB
        (imageOfLE.{u, u, u, u} h (Stacks.SheafOfModules.Tensor.ringSheaf S.O) A)).IsTriangulated :=
      DerivedCategoryB.derivedCategoryB_isTriangulated _ (isWeakSerre_imageOfLE_of_univLE h
        (Stacks.SheafOfModules.Tensor.ringSheaf S.O) A (WeakSerre.isWeakSerre_of_isWeakSerreClass A)
        B hB hvan)
    letI := (S.coarseningHom h).toRingedToposSiteHom.pullbackTopos_preservesFiniteLimits
      (S.coarseningHom h).isMorphismOfSites_toRingedToposSiteHom
      (S.isFlatMapULift_fSharp_auxHomH_coarseningHom h)
    letI := (S.coarseningHom h).toRingedToposSiteHom.pullbackTopos_preservesFiniteColimits
    letI := Functor.additive_of_preserves_binary_products
      (S.coarseningHom h).toRingedToposSiteHom.pullbackTopos
    letI := pullbackOnHomotopy_hasLeftDerivedFunctor_of_exact
      (S.coarseningHom h).toRingedToposSiteHom
    letI := derivedPullbackRestrictionCommShift S h A B hB hvan
    letI := derivedEquivalenceImageOfLEInverseCommShift S h A B hB hvan
    letI := (derivedEquivalenceImageOfLE S h A B hB hvan).commShiftFunctor ℤ
    haveI := (derivedEquivalenceImageOfLE S h A B hB hvan).commShift_of_inverse ℤ
    (derivedEquivalenceImageOfLE S h A B hB hvan).IsTriangulated ∧
      (derivedEquivalenceImageOfLE S h A B hB hvan).functor ⋙
          (DerivedCategoryB.derivedCategoryB
            (imageOfLE.{u, u, u, u} h (Stacks.SheafOfModules.Tensor.ringSheaf S.O) A)).ι =
        (DerivedCategoryB.derivedCategoryB A).ι ⋙
          derivedPushforward.{u} (S.coarseningHom h).toRingedToposSiteHom ∧
      ∃ e : (derivedEquivalenceImageOfLE S h A B hB hvan).inverse ⋙
          (DerivedCategoryB.derivedCategoryB A).ι =
        (DerivedCategoryB.derivedCategoryB
            (imageOfLE.{u, u, u, u} h (Stacks.SheafOfModules.Tensor.ringSheaf S.O) A)).ι ⋙
          derivedPullback.{u} (S.coarseningHom h).toRingedToposSiteHom,
        NatTrans.CommShift (eqToIso e).hom ℤ ∧
      Nonempty ((derivedEquivalenceImageOfLE S h A B hB hvan).inverse ⋙
          (DerivedCategoryB.derivedCategoryB A).ι ≅
        (DerivedCategoryB.derivedCategoryB
            (imageOfLE.{u, u, u, u} h (Stacks.SheafOfModules.Tensor.ringSheaf S.O) A)).ι ⋙
          (S.coarseningHom h).toRingedToposSiteHom.pullbackTopos.mapDerivedCategory)

Stacks.Cohomology.CompareTopologies.isWeakSerre_imageOfLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/WeakSerreAcrossTopologies.lean, line 284. The attribute's comment: “the weak Serre subcategory for the coarser topology”.

Let J' ≤ J be two topologies on C and let R be a sheaf of rings for the finer topology J, so that the identity functor of C is the comparison morphism of ringed sites ε : (C_τ, R_τ) ⟶ (C_τ', R_τ'). Let A be a class of sheaves of R-modules for J — the source's assumption (1), that every object of A is a sheaf for the finer topology, is this — and let B be a set of objects of C. Assume

A is a weak Serre subcategory of Mod(R_τ),

every object of C has a J'-covering whose members lie in B,

for every U in B the cohomology H^p_τ(U, F) vanishes for p > 0 and F in A.

Then the image A' of A under ε_* is a weak Serre subcategory of Mod(R_τ').

The hypothesis hdev is the step of the source's proof that assumptions (2) and (3) above force ε_* to carry an exact short complex with terms in A to an exact short complex. In the source that step is Stacks 072W, identifying R^pε_* with the sheafification of U ↦ H^p_τ(U, F), followed by a dévissage.

theorem isWeakSerre_imageOfLE [HasSheafify J' AddCommGrpCat.{m}]
    [J'.WEqualsLocallyBijective AddCommGrpCat.{m}]
    [EnoughInjectives (_root_.SheafOfModules.{m} R)]
    (hA : WeakSerre.IsWeakSerre A) (B : Set C)
    (hB : ∀ U : C, ∃ 𝒰 : PreZeroHypercover.{max u v} U, 𝒰.sieve₀ ∈ J' U ∧ ∀ i, B (𝒰.X i))
    (hvan : ∀ U : C, B U → ∀ p : ℕ, 0 < p → ∀ F : _root_.SheafOfModules.{m} R, A F →
      IsZero (Stacks.Cohomology.moduleCohomology R U p F))
    (hdev : (∀ U : C, ∃ 𝒰 : PreZeroHypercover.{max u v} U, 𝒰.sieve₀ ∈ J' U ∧ ∀ i, B (𝒰.X i)) →
      (∀ U : C, B U → ∀ p : ℕ, 0 < p → ∀ F : _root_.SheafOfModules.{m} R, A F →
        IsZero (Stacks.Cohomology.moduleCohomology R U p F)) →
      ∀ S : ShortComplex (_root_.SheafOfModules.{m} R), S.Exact →
        A S.X₁ → A S.X₂ → A S.X₃ → (S.map (pushforward.{u, v, r, m} h R)).Exact) :
    WeakSerre.IsWeakSerre (imageOfLE.{u, v, r, m} h R A)

Stacks.Cohomology.CompareTopologies.isWeakSerreClass_imageOfLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/WeakSerreAcrossTopologies.lean, line 373. The attribute's comment: “the same conclusion in the closure form of Stacks 0754”.

The same statement as Stacks.Cohomology.CompareTopologies.isWeakSerre_imageOfLE, with the conclusion phrased in the closure form CategoryTheory.ObjectProperty.IsWeakSerreClass of Stacks 0754.

theorem isWeakSerreClass_imageOfLE [HasSheafify J' AddCommGrpCat.{m}]
    [J'.WEqualsLocallyBijective AddCommGrpCat.{m}]
    [EnoughInjectives (_root_.SheafOfModules.{m} R)]
    (hA : WeakSerre.IsWeakSerre A) (B : Set C)
    (hB : ∀ U : C, ∃ 𝒰 : PreZeroHypercover.{max u v} U, 𝒰.sieve₀ ∈ J' U ∧ ∀ i, B (𝒰.X i))
    (hvan : ∀ U : C, B U → ∀ p : ℕ, 0 < p → ∀ F : _root_.SheafOfModules.{m} R, A F →
      IsZero (Stacks.Cohomology.moduleCohomology R U p F))
    (hdev : (∀ U : C, ∃ 𝒰 : PreZeroHypercover.{max u v} U, 𝒰.sieve₀ ∈ J' U ∧ ∀ i, B (𝒰.X i)) →
      (∀ U : C, B U → ∀ p : ℕ, 0 < p → ∀ F : _root_.SheafOfModules.{m} R, A F →
        IsZero (Stacks.Cohomology.moduleCohomology R U p F)) →
      ∀ S : ShortComplex (_root_.SheafOfModules.{m} R), S.Exact →
        A S.X₁ → A S.X₂ → A S.X₃ → (S.map (pushforward.{u, v, r, m} h R)).Exact) :
    (imageOfLE.{u, v, r, m} h R A).IsWeakSerreClass

Stacks.Cohomology.CompareTopologies.isWeakSerre_imageOfLE_of_univLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/WeakSerreAcrossTopologiesOfVanishing.lean, line 191. The attribute's comment: “first conclusion: the image of A is a weak Serre subcategory of Mod(𝒪_τ')”.

Stacks 07A8, first conclusion. Let J' ≤ J be two topologies on C and let R be a sheaf of rings for the finer topology J, so that the identity functor of C is the comparison morphism of ringed sites ε : (C_τ, R_τ) ⟶ (C_τ', R_τ'). Let A be a class of sheaves of R-modules for J — the source's assumption (1), that every object of A is a sheaf for the finer topology, is this — and let B be a set of objects of C. Assume

A is a weak Serre subcategory of Mod(R_τ),

every object of C has a J'-covering whose members lie in B,

for every U in B the cohomology H^p_τ(U, F) vanishes for p > 0 and F in A.

Then the image A' of A under ε_* is a weak Serre subcategory of Mod(R_τ').

The modules live in a universe containing those of the objects and morphisms of C and of the rings; in it sheafification exists for both topologies, inverts exactly the locally bijective morphisms, and sheaves of R-modules have enough injectives, so that H^p_τ(U, -) is defined. Assumptions 2 and 3 enter through Stacks.Cohomology.CompareTopologies.exact_map_pushforward_of_prop, which proves from them that ε_* carries an exact short complex with terms in A to an exact short complex.

theorem isWeakSerre_imageOfLE_of_univLE (hA : WeakSerre.IsWeakSerre A) (B : Set C)
    (hB : ∀ U : C, ∃ 𝒰 : PreZeroHypercover.{max u v} U, 𝒰.sieve₀ ∈ J' U ∧ ∀ i, B (𝒰.X i))
    (hvan : ∀ U : C, B U → ∀ p : ℕ, 0 < p → ∀ F : _root_.SheafOfModules.{m} R, A F →
      IsZero (Stacks.Cohomology.moduleCohomology R U p F)) :
    WeakSerre.IsWeakSerre (imageOfLE.{u, v, r, m} h R A)

Stacks.Cohomology.CompareTopologies.isWeakSerreClass_imageOfLE_of_univLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/WeakSerreAcrossTopologiesOfVanishing.lean, line 204. The attribute's comment: “first conclusion, in the closure form of Stacks 0754”.

Stacks 07A8, first conclusion, in the closure form of Stacks 0754. The same statement as Stacks.Cohomology.CompareTopologies.isWeakSerre_imageOfLE_of_univLE, with the conclusion phrased as CategoryTheory.ObjectProperty.IsWeakSerreClass, the form in which the derived category results consume it.

theorem isWeakSerreClass_imageOfLE_of_univLE (hA : WeakSerre.IsWeakSerre A) (B : Set C)
    (hB : ∀ U : C, ∃ 𝒰 : PreZeroHypercover.{max u v} U, 𝒰.sieve₀ ∈ J' U ∧ ∀ i, B (𝒰.X i))
    (hvan : ∀ U : C, B U → ∀ p : ℕ, 0 < p → ∀ F : _root_.SheafOfModules.{m} R, A F →
      IsZero (Stacks.Cohomology.moduleCohomology R U p F)) :
    (imageOfLE.{u, v, r, m} h R A).IsWeakSerreClass

Tag 0F18, a lemma

Tag 0F18 in the Stacks Project.

Stacks.Cohomology.MayerVietoris.essImage_iff_forall_isCSquareIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/MayerVietoris/DescentForAFamilyOfSquares.lean, line 1171.

Stacks 0F18. Let C carry two Grothendieck topologies J' ≤ J and let 𝒪 be a sheaf of rings for J, so that the identity of C is a comparison of ringed sites ε : (C_J, 𝒪_J) ⟶ (C_{J'}, 𝒪_{J'}). Let A be a type and for each α : A let
E α ⟶ Y α
  ↓      ↓
Z α ⟶ X α
be a commutative square in C. Assume

a J'-sheaf of sets F' is a J-sheaf whenever F'(X α) = F'(Z α) ×_{F'(E α)} F'(Y α) for all α, and

for every K' in D(𝒪_{J'}) in the essential image of Rε_* the canonical comparison maps c^{K'}_{X α, Z α, Y α, E α} of [Stacks, Tag 0F16] are isomorphisms for all α.

Then an object K' of D⁺(𝒪_{J'}) lies in the essential image of Rε_* if and only if the maps c^{K'}_{X α, Z α, Y α, E α} are isomorphisms for all α.

Rε_* is any right derived functor of ε_* together with its unit; the hypothesis that it is a right derived functor is what makes the essential image independent of the choice.

theorem essImage_iff_forall_isCSquareIso {A : Type*} (sq : A → Square S.C)
    (hdetect : ∀ F : Sheaf J' (Type max u w),
      (∀ a, ((sq a).op.map F.obj).IsPullback) → Presheaf.IsSheaf S.J F.obj)
    (Rε : DerivedCategory (SheafOfModules.{v} (Stacks.SheafOfModules.Tensor.ringSheaf S.O)) ⥤
      DerivedCategory (SheafOfModules.{v} (ringSheafOfLe h
          (Stacks.SheafOfModules.Tensor.ringSheaf S.O))))
    (η : letI := modulePushforward_additive.{u, v, w, r} h
            (Stacks.SheafOfModules.Tensor.ringSheaf S.O);
      (modulePushforward.{u, v, w, r} h
          (Stacks.SheafOfModules.Tensor.ringSheaf S.O)).mapHomotopyCategory
        (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rε)
    [Rε.IsRightDerivedFunctor η
      (HomotopyCategory.quasiIso (SheafOfModules.{v}
          (Stacks.SheafOfModules.Tensor.ringSheaf S.O)) (ComplexShape.up ℤ))]
    (hcomparison : ∀ K' : DerivedCategory (SheafOfModules.{v} (ringSheafOfLe h
        (Stacks.SheafOfModules.Tensor.ringSheaf S.O))),
      Rε.essImage K' → ∀ a, (CanonicalMapOfComplexes.derivedCSquareData.{u, v}
        (R := (Stacks.SheafOfModules.Tensor.ringSheaf (S.ofLe h).O)) (sq a)).IsCSquareIso K')
    (K' : DerivedCategory (SheafOfModules.{v} (ringSheafOfLe h
        (Stacks.SheafOfModules.Tensor.ringSheaf S.O))))
    (hplus : (DerivedCategory.TStructure.t
      (C := SheafOfModules.{v} (ringSheafOfLe h
          (Stacks.SheafOfModules.Tensor.ringSheaf S.O)))).plus K') :
    Rε.essImage K' ↔ ∀ a, (CanonicalMapOfComplexes.derivedCSquareData.{u, v}
      (R := (Stacks.SheafOfModules.Tensor.ringSheaf (S.ofLe h).O)) (sq a)).IsCSquareIso K'

Tag 0F19, a lemma

Tag 0F19 in the Stacks Project.

Stacks.Cohomology.MayerVietoris.isCSquareIso_ofLe_of_isPushout, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/MayerVietoris/DescentForACoarserTopology.lean, line 151.

Stacks 0F19. Let J' ≤ J be two topologies on C and let 𝒪 be a sheaf of rings for J, so that the identity of C is a comparison ε : (C_J, 𝒪_J) ⟶ (C_{J'}, 𝒪_{J'}). Let a commutative square in C be given whose J-sheafified representables form a pushout square and whose map h_E^# ⟶ h_Y^# is a monomorphism. Then for every object K' of D(𝒪_{J'}) in the essential image of the derived direct image Rε_*, the canonical map c^{K'}_{X,Z,Y,E} of Stacks 0F16 for the coarser topology is an isomorphism.

theorem isCSquareIso_ofLe_of_isPushout (sq : Square S.C)
    (hpushout : (sq.map (Sheaf.sheafifiedYoneda S.J)).IsPushout)
    (hmono : Mono ((Sheaf.sheafifiedYoneda S.J).map sq.f₁₂))
    (Rε : DerivedCategory (SheafOfModules.{v} (Stacks.SheafOfModules.Tensor.ringSheaf S.O)) ⥤
      DerivedCategory (SheafOfModules.{v} (Stacks.SheafOfModules.Tensor.ringSheaf (S.ofLe h).O)))
    (η : letI := (modulePushforward_additive.{u, v, w, r} h
        (Stacks.SheafOfModules.Tensor.ringSheaf S.O));
      (modulePushforward.{u, v, w, r} h
        (Stacks.SheafOfModules.Tensor.ringSheaf S.O)).mapHomotopyCategory
        (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rε)
    [Rε.IsRightDerivedFunctor η
      (HomotopyCategory.quasiIso (SheafOfModules.{v} (Stacks.SheafOfModules.Tensor.ringSheaf S.O))
        (ComplexShape.up ℤ))]
    (K' : DerivedCategory
      (SheafOfModules.{v} (Stacks.SheafOfModules.Tensor.ringSheaf (S.ofLe h).O)))
    (hK' : Rε.essImage K') :
    (CanonicalMapOfComplexes.derivedCSquareData.{u, v}
      (R := (Stacks.SheafOfModules.Tensor.ringSheaf (S.ofLe h).O)) sq).IsCSquareIso K'

Sources

LeanStacks.Cohomology.CompareTopologies.isWeakSerreClass_imageOfLE_of_vanishing · Stacks.Cohomology.CompareTopologies.derivedPullbackEquivalenceImageOfLE · Stacks.Cohomology.CompareTopologies.derivedPullbackEquivalenceImageOfLE_functor_comp_ι · Stacks.Cohomology.CompareTopologies.derivedPullbackEquivalenceImageOfLE_inverse_comp_ι · Stacks.Cohomology.CompareTopologies.derivedEquivalenceImageOfLE_spec · Stacks.Cohomology.CompareTopologies.isWeakSerre_imageOfLE · Stacks.Cohomology.CompareTopologies.isWeakSerreClass_imageOfLE · Stacks.Cohomology.CompareTopologies.isWeakSerre_imageOfLE_of_univLE

Section21.30 Comparing cohomology #

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

Tag 0EZ2, an equation

Tag 0EZ2 in the Stacks Project.

Stacks.ComparingTopologies.comparisonPullbackOverMapPullbackIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/ComparisonSituation.lean, line 318. The attribute's comment: “commutativity of the square of topoi”.

Stacks 0EZ2. For two comparable topologies, change of topology commutes with restriction along a morphism, up to the canonical natural isomorphism of inverse-image functors.

noncomputable def comparisonPullbackOverMapPullbackIso
    {J K : GrothendieckTopology C} (h : K ≤ J) {X Y : C} (f : X ⟶ Y) :
    comparisonPullback (over_le_over h Y) ⋙ J.overMapPullback (Type (max u v)) f ≅
      K.overMapPullback (Type (max u v)) f ⋙ comparisonPullback (over_le_over h X)

Stacks.ComparingTopologies.overMapPullback_comp_comparisonPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/ComparisonSituation.lean, line 349. The attribute's comment: “the identity ε_{X,*} f_J^{-1} = f_K^{-1} ε_{Y,*}”.

Stacks 0EZ2. On direct images for the comparison morphisms and inverse images for restriction, the square commutes strictly: ε_{X,*} ∘ f_J^{-1} = f_K^{-1} ∘ ε_{Y,*}.

theorem overMapPullback_comp_comparisonPushforward
    {J K : GrothendieckTopology C} (h : K ≤ J) {X Y : C} (f : X ⟶ Y) :
    J.overMapPullback (Type (max u v)) f ⋙ comparisonPushforward (over_le_over h X) =
      comparisonPushforward (over_le_over h Y) ⋙ K.overMapPullback (Type (max u v)) f

Tag 0EZ3, a situation

Tag 0EZ3 in the Stacks Project.

Stacks.ComparingTopologies.CohomologyComparison, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/ComparisonSituation.lean, line 116.

Stacks 0EZ3. The standing situation for comparing cohomology computed in a finer coverage with cohomology computed in a coarser one.

structure CohomologyComparison (C : Type u) [Category.{v} C]

Tag 0EZ9, a lemma

Tag 0EZ9 in the Stacks Project.

Stacks.ComparingTopologies.CohomologyComparison.fineWeakSerre, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/ComparisonClass.lean, line 71. The attribute's comment: “the category 𝒜_X”.

Stacks 0EZ9. The class 𝒜_X of abelian sheaves on the finer localized site: those of the form ε⁻¹ F for F in the given weak Serre class 𝒜'_X on the coarser localized site, with ε the change-of-topology morphism.

noncomputable abbrev fineWeakSerre (S : CohomologyComparison C) (X : C) :
    ObjectProperty (Sheaf (S.fineCoverage.toGrothendieck.over X) Ab.{max u v})

Stacks.ComparingTopologies.CohomologyComparison.fineWeakSerre_iff_weakSerre_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/ComparisonClass.lean, line 78. The attribute's comment: “the membership criterion for 𝒜_X”.

Stacks 0EZ9. A sheaf on the finer localized site belongs to 𝒜_X if and only if its change-of-topology direct image belongs to 𝒜'_X.

theorem fineWeakSerre_iff_weakSerre_pushforward
    (S : CohomologyComparison C) (X : C)
    (F : Sheaf (S.fineCoverage.toGrothendieck.over X) Ab.{max u v}) :
    S.fineWeakSerre X F ↔
      S.weakSerre X
        ((abelianComparisonPushforward S.fineCoverage S.coarseCoverage
          S.coarse_le_fine X).obj F)

Stacks.ComparingTopologies.CohomologyComparison.fineWeakSerre_overMapPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/ComparisonClass.lean, line 154. The attribute's comment: “stability of 𝒜_X under restriction”.

Stacks 0EZ9. Restriction along a morphism of the site preserves the class 𝒜 of abelian sheaves on the finer localized sites.

theorem fineWeakSerre_overMapPullback (S : CohomologyComparison C)
    {X Y : C} (f : X ⟶ Y)
    (F : Sheaf (S.fineCoverage.toGrothendieck.over Y) Ab.{max u v})
    (hF : S.fineWeakSerre Y F) :
    S.fineWeakSerre X
      ((S.fineCoverage.toGrothendieck.overMapPullback Ab.{max u v} f).obj F)

Tag 0EZA, a lemma

Tag 0EZA in the Stacks Project.

Stacks.ComparingTopologies.higherDirectImageComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/HigherDirectImages.lean, line 210. The attribute's comment: “canonical comparison transformation”.

The comparison transformation. The canonical degree-i map from the coarse higher direct image of the change-of-topology direct image to the change-of-topology direct image of the fine higher direct image,

R^i f_{τ',*} ε_{X,*} ℱ ⟶ ε_{Y,*} R^i f_{τ,*} ℱ,

natural in the abelian sheaf ℱ on the finer localized site over X.

It is the composite of the two edge morphisms of the Grothendieck spectral sequence of the square of topoi abelianComparisonPushforward_square: the edge E₂^{i,0} ⟶ H^i for the pair (ε_{X,*}, f_{τ',*}), followed by the edge H^i ⟶ E₂^{0,i} for the pair (f_{τ,*}, ε_{Y,*}).

def higherDirectImageComparison (S : CohomologyComparison C) {X Y : C} (f : X ⟶ Y) (i : ℕ) :
    abelianComparisonPushforward S.fineCoverage S.coarseCoverage S.coarse_le_fine X ⋙
        (overPushforward S.coarseCoverage.toGrothendieck f).rightDerived i ⟶
      (overPushforward S.fineCoverage.toGrothendieck f).rightDerived i ⋙
        abelianComparisonPushforward S.fineCoverage S.coarseCoverage S.coarse_le_fine Y

Stacks.ComparingTopologies.isIso_higherDirectImageComparison_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/VanishingConditionInduction.lean, line 250. The attribute's comment: “the comparison is an isomorphism through degree n”.

Stacks 0EZA. Assume the vanishing condition (V_n). For a morphism f : X ⟶ Y of the distinguished class, an abelian sheaf ℱ of 𝒜_X on the finer localized site over X, and a degree i ≤ n, the comparison

R^i f_{τ',*} ε_{X,*} ℱ ⟶ ε_{Y,*} R^i f_{τ,*} ℱ

is an isomorphism.

Both factors of the comparison are invertible, for different reasons. The first edge morphism is invertible in degree i as soon as R^q ε_{X,*} ℱ vanishes for 1 ≤ q ≤ i, which is (V_n); this is Stacks.Cohomology.RightDerivedEdgeIso.isIso_edge_app, and no spectral sequence is needed for it. The second edge morphism is invertible as soon as the object it starts from lies in the essential image of the change-of-topology direct image, by Stacks.Cohomology.RightDerivedCoEdge.isIso_secondEdge_app_of_isIso_unit; and that object is R^i f_{τ',*} ε_{X,*} ℱ — by the first edge morphism, which has just been seen to be invertible — which lies in the weak Serre class 𝒜'_Y because ε_{X,*} ℱ lies in 𝒜'_X and the distinguished class is stable under higher direct images.

theorem isIso_higherDirectImageComparison_app (S : CohomologyComparison C) (n : ℕ)
    (hV : S.vanishingCondition n) {X Y : C} (f : X ⟶ Y) (hf : S.morphismProperty f)
    (i : ℕ) (hi : i ≤ n) (F : Sheaf (S.fineCoverage.toGrothendieck.over X) Ab.{max u v})
    (hF : S.fineWeakSerre X F) :
    IsIso ((higherDirectImageComparison S f i).app F)

Tag 0EZB, a lemma

Tag 0EZB in the Stacks Project.

Stacks.ComparingTopologies.isIso_homology_derivedCohomologyComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/ComparingCohomology.lean, line 396.

Stacks 0EZB. In the comparison situation of Stacks 0EZ3, assume the vanishing condition (V_n). Let X be an object of C and let L be an object of D(C_{τ'}/X) whose cohomology sheaves vanish in negative degrees and lie in the weak Serre class 𝒜'_X in the degrees 0 ≤ i ≤ n. Then the canonical map

H^n_{τ'}(X, L) ⟶ H^n_τ(X, ε_X^{-1}L)

of Stacks.ComparingTopologies.derivedCohomologyComparison is an isomorphism.

The truncation τ_{≤n}L has all of its cohomology in 𝒜'_X and none outside the degrees 0, …, n, so the comparison is invertible in degree n there; and the truncation morphism τ_{≤n}L ⟶ L becomes invertible on H^n after applying either RΓ_{τ'}(X, -) or ε_X^{-1} followed by RΓ_τ(X, -). The naturality square of the comparison then carries the conclusion from τ_{≤n}L to L.

theorem isIso_homology_derivedCohomologyComparison (S : CohomologyComparison C) (n : ℕ)
    (hV : S.vanishingCondition n) (X : C)
    (L : DerivedCategory (AbelianSheaves S.coarseCoverage.toGrothendieck X))
    (hneg : ∀ i : ℤ, i < 0 → IsZero ((DerivedCategory.homologyFunctor
      (AbelianSheaves S.coarseCoverage.toGrothendieck X) i).obj L))
    (hmem : ∀ i : ℕ, i ≤ n → S.weakSerre X ((DerivedCategory.homologyFunctor
      (AbelianSheaves S.coarseCoverage.toGrothendieck X) (i : ℤ)).obj L)) :
    IsIso ((DerivedCategory.Plus.homologyFunctor Ab.{max u v} (n : ℤ)).map
      ((derivedCohomologyComparison S X).app
        (DerivedCategory.Plus.ofNonnegative L hneg)))

Tag 0EZC, a lemma

Tag 0EZC in the Stacks Project.

Stacks.ComparingTopologies.cohomologyComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/Cohomology.lean, line 313. The attribute's comment: “canonical cohomology map”.

The natural change-of-topology map H^i_{τ'}(X, ε_{X,*} F) ⟶ H^i_τ(X, F), given by pulling back cohomology classes along ε_X.

def cohomologyComparison (S : CohomologyComparison C) (X : C) (i : ℕ) :
    abelianComparisonPushforward S.fineCoverage S.coarseCoverage S.coarse_le_fine X ⋙
        (globalSectionsOver S.coarseCoverage.toGrothendieck X).rightDerived i ⟶
      (globalSectionsOver S.fineCoverage.toGrothendieck X).rightDerived i

Stacks.ComparingTopologies.cohomologyComparison_eq_injectiveResolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/Cohomology.lean, line 347. The attribute's comment: “canonical map via injective resolutions”.

An augmentation-preserving comparison from an injective resolution of the coarse direct image to the direct image of an injective resolution computes the canonical cohomology map. This characterizes its components in every degree.

theorem cohomologyComparison_eq_injectiveResolution (S : CohomologyComparison C) (X : C) (i : ℕ)
    (F : Sheaf (S.fineCoverage.toGrothendieck.over X) Ab.{max u v})
    (I : InjectiveResolution F)
    (J : InjectiveResolution ((abelianComparisonPushforward S.fineCoverage
      S.coarseCoverage S.coarse_le_fine X).obj F))
    (φ : J.cocomplex ⟶
      ((abelianComparisonPushforward S.fineCoverage S.coarseCoverage
        S.coarse_le_fine X).mapHomologicalComplex (.up ℕ)).obj I.cocomplex)
    (hφ : J.ι.f 0 ≫ φ.f 0 =
      (abelianComparisonPushforward S.fineCoverage S.coarseCoverage
        S.coarse_le_fine X).map (I.ι.f 0)) :
    (cohomologyComparison S X i).app F =
      (J.isoRightDerivedObj (globalSectionsOver S.coarseCoverage.toGrothendieck X) i).hom ≫
        HomologicalComplex.homologyMap
          (((globalSectionsOver S.coarseCoverage.toGrothendieck X).mapHomologicalComplex
            (.up ℕ)).map φ) i ≫
          (I.isoRightDerivedObj (globalSectionsOver S.fineCoverage.toGrothendieck X) i).inv

Stacks.ComparingTopologies.mono_cohomologyComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/Cohomology.lean, line 922. The attribute's comment: “injectivity”.

Stacks 0EZC. Under (Vₙ), the change-of-topology map on cohomology in degree n + 1 is injective.

theorem mono_cohomologyComparison (S : CohomologyComparison C) (n : ℕ)
    (hV : S.vanishingCondition n) (X : C)
    (F : Sheaf (S.fineCoverage.toGrothendieck.over X) Ab.{max u v})
    (hF : S.fineWeakSerre X F) :
    Mono ((cohomologyComparison S X (n + 1)).app F)

Stacks.ComparingTopologies.mem_range_cohomologyComparison_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/Cohomology.lean, line 933. The attribute's comment: “image of the map”.

Stacks 0EZC. Under (Vₙ), a class in degree n + 1 is in the image of the change-of-topology map on cohomology precisely when it becomes zero on the members of a covering for the coarser topology.

theorem mem_range_cohomologyComparison_iff (S : CohomologyComparison C) (n : ℕ)
    (hV : S.vanishingCondition n) (X : C)
    (F : Sheaf (S.fineCoverage.toGrothendieck.over X) Ab.{max u v})
    (hF : S.fineWeakSerre X F)
    (ξ : sheafCohomology (S.fineCoverage.toGrothendieck.over X) F (Over.mk (𝟙 X)) (n + 1)) :
    (∃ η : sheafCohomology (S.coarseCoverage.toGrothendieck.over X)
        ((abelianComparisonPushforward S.fineCoverage S.coarseCoverage
          S.coarse_le_fine X).obj F) (Over.mk (𝟙 X)) (n + 1),
        (cohomologyComparison S X (n + 1)).app F η = ξ) ↔
      (∃ R : Presieve X, R ∈ S.coarseCoverage X ∧
        ∀ ⦃V : C⦄ (f : V ⟶ X), R f →
          sheafCohomologyRestriction (S.fineCoverage.toGrothendieck.over X)
            (Over.homMk (U := Over.mk f) (V := Over.mk (𝟙 X)) f (by simp))
            (n + 1) F ξ = 0)

Tag 0EZD, a lemma

Tag 0EZD in the Stacks Project.

Stacks.ComparingTopologies.exists_coarseCovering_restrict_eq_zero_of_equalizer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/DescentOfCohomologyClasses.lean, line 175.

Stacks 0EZD. Let f : X ⟶ Y be a morphism of the distinguished class which by itself is a covering for the finer topology, and let F be a sheaf of the weak Serre class 𝒜'_Y on the coarser site localized at Y. If a cohomology class of degree n + 1 over X has equal restrictions along the two projections from X ×_Y X, then there is a covering of Y for the coarser topology such that the class restricts to zero over every base change Yᵢ ×_Y X.

theorem exists_coarseCovering_restrict_eq_zero_of_equalizer (S : CohomologyComparison C)
    {X Y : C} (f : X ⟶ Y) (hf : S.morphismProperty f)
    (hcover : Presieve.singleton f ∈ S.fineCoverage Y)
    (F : Sheaf (S.coarseCoverage.toGrothendieck.over Y) Ab.{max u v}) (hF : S.weakSerre Y F) (n : ℕ)
    (P : Over Y) (p₁ p₂ : P ⟶ Over.mk f) (hP : IsPullback p₁.left p₂.left f f)
    (θ : Stacks.sheafCohomology (S.coarseCoverage.toGrothendieck.over Y) F (Over.mk f) (n + 1))
    (hθ : Stacks.sheafCohomologyRestriction (S.coarseCoverage.toGrothendieck.over Y) p₁
        (n + 1) F θ =
      Stacks.sheafCohomologyRestriction (S.coarseCoverage.toGrothendieck.over Y) p₂
        (n + 1) F θ) :
    ∃ R : Presieve Y, R ∈ S.coarseCoverage Y ∧
      ∀ ⦃Z : C⦄ (g : Z ⟶ Y), R g →
        ∃ (Q : Over Y) (a : Q ⟶ Over.mk f) (b : Q ⟶ Over.mk g),
          IsPullback a.left b.left f g ∧
            Stacks.sheafCohomologyRestriction (S.coarseCoverage.toGrothendieck.over Y) a
              (n + 1) F θ = 0

Tag 0EZE, a lemma

Tag 0EZE in the Stacks Project.

Stacks.ComparingTopologies.CohomologyComparison.vanishingCondition_succ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/HigherDirectImageVanishing.lean, line 62.

Stacks 0EZE. In the comparison situation of Stacks 0EZ3 the vanishing condition (V_n) implies (V_{n+1}).

theorem CohomologyComparison.vanishingCondition_succ (S : CohomologyComparison C) (n : ℕ)
    (hV : S.vanishingCondition n) : S.vanishingCondition (n + 1)

Tag 0EZF, a lemma

Tag 0EZF in the Stacks Project.

Stacks.ComparingTopologies.rightDerivedPushforward_mem_derivedCategoryBPlus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/DerivedPushforwardPreservesComparison.lean, line 116. The attribute's comment: “part (2), membership: R f_{τ',*} carries D⁺_{𝒜'_X} into D⁺_{𝒜'_Y}”.

Stacks 0EZF, the first assertion of part (2). In a cohomology comparison situation, total right derived direct image along a morphism of the distinguished class P carries D⁺_{𝒜'_X} into D⁺_{𝒜'_Y}.

No hypothesis beyond those of the tag is used: in particular the vanishing conditions (V_n), which the tag asserts first, are not needed for this half. See the implementation notes for the other clauses of the tag and where they live.

theorem rightDerivedPushforward_mem_derivedCategoryBPlus
    (S : CohomologyComparison C) {X Y : C} (f : X ⟶ Y)
    (hf : S.morphismProperty f)
    (K : DerivedCategory.Plus
      (Sheaf (S.coarseCoverage.toGrothendieck.over X) Ab.{max u v}))
    (hK : DerivedCategoryB.derivedCategoryBPlus (S.weakSerre X) K.obj) :
    DerivedCategoryB.derivedCategoryBPlus (S.weakSerre Y)
      ((((Over.map f).sheafPushforwardCocontinuous Ab.{max u v}
          (S.coarseCoverage.toGrothendieck.over X)
          (S.coarseCoverage.toGrothendieck.over Y)).rightDerivedFunctorPlus.obj K).obj)

Stacks.ComparingTopologies.CohomologyComparison.vanishingCondition_all, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/HigherDirectImageVanishing.lean, line 70. The attribute's comment: “(V_n) holds for all n”.

Stacks 0EZF, the leading assertion. In the comparison situation of Stacks 0EZ3 the vanishing condition (V_n) holds for every n: (V_0) is empty and Stacks 0EZE is the induction step.

theorem CohomologyComparison.vanishingCondition_all (S : CohomologyComparison C) (n : ℕ) :
    S.vanishingCondition n

Stacks.ComparingTopologies.isIso_derivedComparisonUnit_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/HigherDirectImageVanishing.lean, line 79. The attribute's comment: “(1)”.

Stacks 0EZF (1). For X in C and K' in D⁺_{𝒜'_X}(C_{τ'}/X) the canonical map K' ⟶ Rε_{X,*}(ε_X^{-1}K') is an isomorphism.

theorem isIso_derivedComparisonUnit_app (S : CohomologyComparison C) (X : C)
    (K : DerivedCategory.Plus (AbelianSheaves S.coarseCoverage.toGrothendieck X))
    (hK : ∀ i : ℤ, S.weakSerre X ((DerivedCategory.Plus.homologyFunctor _ i).obj K)) :
    IsIso ((derivedComparisonUnit S X).app K)

Stacks.ComparingTopologies.isIso_derivedComparisonBaseChange_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/HigherDirectImageVanishing.lean, line 89. The attribute's comment: “(2), base change”.

Stacks 0EZF (2), the base change. For a morphism f : X ⟶ Y of C and K' in D⁺_{𝒜'_X}(C_{τ'}/X) the base change map ε_Y^{-1}(Rf_{τ',*}K') ⟶ Rf_{τ,*}(ε_X^{-1}K') is an isomorphism. The source states this for f in the distinguished class; it holds for every f.

theorem isIso_derivedComparisonBaseChange_app (S : CohomologyComparison C) {X Y : C} (f : X ⟶ Y)
    (K : DerivedCategory.Plus (AbelianSheaves S.coarseCoverage.toGrothendieck X))
    (hK : ∀ n : ℤ, S.weakSerre X
      ((DerivedCategory.Plus.homologyFunctor
        (AbelianSheaves S.coarseCoverage.toGrothendieck X) n).obj K)) :
    IsIso ((derivedComparisonBaseChange S f).app K)

Tag 0EZG, a lemma

Tag 0EZG in the Stacks Project.

Stacks.ComparingTopologies.CohomologyComparison.fineWeakSerre_isWeakSerreClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/DerivedComparisonEquivalence.lean, line 61. The attribute's comment: “first assertion: 𝒜_X is a weak Serre subcategory of Ab(C_τ/X)”.

First assertion of Stacks 0EZG. In the comparison situation of Stacks 0EZ3, for any object X of C the class 𝒜_X ⊂ Ab(C_τ/X) of Stacks 0EZ9 is a weak Serre subcategory.

theorem fineWeakSerre_isWeakSerreClass (S : CohomologyComparison C) (X : C) :
    (S.fineWeakSerre X).IsWeakSerreClass

Stacks.ComparingTopologies.boundedBelowComparisonEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/DerivedComparisonEquivalence.lean, line 137. The attribute's comment: “second assertion: Rε_{X,*} : D⁺_{𝒜_X}(C_τ/X) ⟶ D⁺_{𝒜'_X}(C_{τ'}/X) is an equivalence”.

Second assertion of Stacks 0EZG. In the comparison situation of Stacks 0EZ3, for any object X of C the derived change-of-topology direct image

Rε_{X,*} : D⁺_{𝒜_X}(C_τ/X) ⟶ D⁺_{𝒜'_X}(C_{τ'}/X)

is an equivalence of categories, with quasi-inverse ε_X^{-1}.

def boundedBelowComparisonEquivalence (S : CohomologyComparison C) (X : C) :
    (derivedFineWeakSerre S X).FullSubcategory ≌
      (derivedWeakSerre S X).FullSubcategory

Stacks.ComparingTopologies.boundedBelowComparisonEquivalence_functor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/DerivedComparisonEquivalence.lean, line 162. The attribute's comment: “the second assertion: the functor of the equivalence is Rε_{X,*}”.

Stacks 0EZG, the identification of the functor of the equivalence with the restriction of the derived change-of-topology direct image Rε_{X,*}.

theorem boundedBelowComparisonEquivalence_functor (S : CohomologyComparison C) (X : C) :
    (boundedBelowComparisonEquivalence S X).functor =
      derivedComparisonPushforwardLift S X

Stacks.ComparingTopologies.boundedBelowComparisonEquivalence_inverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/DerivedComparisonEquivalence.lean, line 170. The attribute's comment: “the second assertion: the quasi-inverse of the equivalence is ε_X^{-1}”.

Stacks 0EZG, the identification of the quasi-inverse of the equivalence with the restriction of the change-of-topology inverse image ε_X^{-1}.

theorem boundedBelowComparisonEquivalence_inverse (S : CohomologyComparison C) (X : C) :
    (boundedBelowComparisonEquivalence S X).inverse =
      derivedComparisonPullbackLift S X

Tag 0EZH, a lemma

Tag 0EZH in the Stacks Project.

Stacks.ComparingTopologies.isIso_cohomologyChangeOfTopology_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/CohomologyComparisonIsomorphism.lean, line 91. The attribute's comment: “(1)”.

Clause (1) of Stacks 0EZH. In the comparison situation of Stacks 0EZ3, let X be an object of C and let ℱ' be a sheaf of the weak Serre class 𝒜'_X on the coarser localized site. Then for every n the canonical map

H^n_{τ'}(X, ℱ') ⟶ H^n_τ(X, ε_X^{-1}ℱ')

is an isomorphism.

theorem isIso_cohomologyChangeOfTopology_app (S : CohomologyComparison C) (X : C)
    (F : Sheaf (S.coarseCoverage.toGrothendieck.over X) Ab.{max u v})
    (hF : S.weakSerre X F) (n : ℕ) :
    IsIso ((cohomologyChangeOfTopology S X n).app F)

Stacks.ComparingTopologies.isIso_derivedCohomologyComparison_app_of_weakSerre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/CohomologyComparisonIsomorphism.lean, line 118. The attribute's comment: “(2), as an isomorphism of derived global sections”.

Clause (2) of Stacks 0EZH, as an isomorphism in D⁺(Ab). In the comparison situation of Stacks 0EZ3, let X be an object of C and let K' be a bounded below object of the derived category of abelian sheaves on C_{τ'}/X all of whose cohomology sheaves lie in 𝒜'_X, that is, an object of D⁺_{𝒜'_X}(C_{τ'}/X). Then the canonical map

RΓ_{τ'}(X, K') ⟶ RΓ_τ(X, ε_X^{-1}K')

is an isomorphism.

theorem isIso_derivedCohomologyComparison_app_of_weakSerre (S : CohomologyComparison C) (X : C)
    (K : DerivedCategory.Plus (AbelianSheaves S.coarseCoverage.toGrothendieck X))
    (hK : ∀ i : ℤ, S.weakSerre X ((DerivedCategory.Plus.homologyFunctor _ i).obj K)) :
    IsIso ((derivedCohomologyComparison S X).app K)

Stacks.ComparingTopologies.isIso_homology_derivedCohomologyComparison_app_of_weakSerre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChangeOfTopology/CohomologyComparisonIsomorphism.lean, line 131. The attribute's comment: “(2)”.

Clause (2) of Stacks 0EZH. With X and K' as above, the canonical map

H^n_{τ'}(X, K') ⟶ H^n_τ(X, ε_X^{-1}K')

is an isomorphism for every n.

theorem isIso_homology_derivedCohomologyComparison_app_of_weakSerre
    (S : CohomologyComparison C) (X : C)
    (K : DerivedCategory.Plus (AbelianSheaves S.coarseCoverage.toGrothendieck X))
    (hK : ∀ i : ℤ, S.weakSerre X ((DerivedCategory.Plus.homologyFunctor _ i).obj K))
    (n : ℤ) :
    IsIso ((DerivedCategory.Plus.homologyFunctor Ab.{max u v} n).map
      ((derivedCohomologyComparison S X).app K))

Sources

Section21.31 Cohomology on Hausdorff and locally quasi-compact spaces #

Section 21.31 of the Stacks Project, Tag 09WY. 13 tags here are carried by 78 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 09WY, the section

Tag 09WY in the Stacks Project.

Stacks.Topology.LocallyQuasiCompactZariskiSituation.isContinuous_id_zariski_qc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcComparisonNaturality.lean, line 112. The attribute's comment: “ε_X comes from the identity functor of LC/X, which is continuous”.

A quasi-compact sheaf on a localized site is a Zariski sheaf.

theorem isContinuous_id_zariski_qc (X : S.category) :
    (Functor.id (Over X)).IsContinuous (S.zariskiTopology.over X)
      (S.qcSite.grothendieckTopology.over X)

Stacks.Topology.LocallyQuasiCompactZariskiSituation.qcComparisonMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcComparisonNaturality.lean, line 163. The attribute's comment: “the induced morphism ε_X : LC_qc/X → LC_Zar/X”.

The change-of-topology morphism of topoi ε_X : Sh(LC_qc/X) → Sh(LC_Zar/X).

def qcComparisonMorphism (X : S.category) :
    MorphismOfTopoi
      (Sheaf (S.qcSite.grothendieckTopology.over X) (Type (max u t)))
      (Sheaf (S.zariskiTopology.over X) (Type (max u t)))

Stacks.Topology.LocallyQuasiCompactZariskiSituation.zariskiComparisonMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcComparisonNaturality.lean, line 178. The attribute's comment: “the morphism π_X : Sh(LC_Zar/X) → Sh(X)”.

The Zariski comparison morphism of topoi π_X : Sh(LC_Zar/X) → Sh(X).

def zariskiComparisonMorphism (X : S.category) :
    MorphismOfTopoi
      (Sheaf (S.zariskiTopology.over X) (Type (max u t)))
      (Sheaf (Opens.grothendieckTopology X.obj) (Type (max u t)))

Stacks.Topology.LocallyQuasiCompactZariskiSituation.qcTopologicalMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcComparisonNaturality.lean, line 190. The attribute's comment: “the morphism of topoi a_X = π_X ∘ ε_X : Sh(LC_qc/X) → Sh(X)”.

The comparison morphism of topoi a_X : Sh(LC_qc/X) → Sh(X), defined as the composite π_X ∘ ε_X.

def qcTopologicalMorphism (X : S.category) :
    MorphismOfTopoi
      (Sheaf (S.qcSite.grothendieckTopology.over X) (Type (max u t)))
      (Sheaf (Opens.grothendieckTopology X.obj) (Type (max u t)))

IsQcCovering.of_isOpenEmbedding, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcTopology.lean, line 73. The attribute's comment: “an open covering of an object of LC is a qc covering”.

An open covering is a qc covering. A jointly surjective family of open embeddings into a locally quasi-compact space is a qc covering: a point x lies in the image of some fᵢ, which is open, so x has a quasi-compact neighbourhood K inside that image, and K is the image of the quasi-compact set fᵢ⁻¹(K).

theorem IsQcCovering.of_isOpenEmbedding {ι : Type*} {X : ι → Type*} {Y : Type*}
    [∀ i, TopologicalSpace (X i)] [TopologicalSpace Y] [LocallyCompactSpace Y]
    {f : ∀ i, X i → Y} (hf : ∀ i, IsOpenEmbedding (f i))
    (hsurj : ∀ y, ∃ i, y ∈ Set.range (f i)) : IsQcCovering f

IsQcCovering.of_iSup_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcTopology.lean, line 92. The attribute's comment: “an open covering of an object of LC is a qc covering”.

An open covering X = ⋃ Uᵢ gives a qc covering {Uᵢ → X}, for a locally quasi-compact space X.

theorem IsQcCovering.of_iSup_eq_top {ι : Type*} {X : Type*} [TopologicalSpace X]
    [LocallyCompactSpace X] (U : ι → TopologicalSpace.Opens X) (hU : iSup U = ⊤) :
    IsQcCovering (fun i => (Subtype.val : U i → X))

Stacks.Topology.LocallyQuasiCompactHausdorff.qcPretopology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcTopology.lean, line 208. The attribute's comment: “LC with the collection of qc coverings forms a site”.

LC with its qc coverings is a site. The qc coverings of Stacks 09X0 form a pretopology on LC, by Stacks 09X1.

noncomputable def qcPretopology : Pretopology LocallyQuasiCompactHausdorff.{u}

Stacks.Topology.LocallyQuasiCompactHausdorff.qcTopology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcTopology.lean, line 213. The attribute's comment: “the qc topology on LC”.

The qc topology on LC: the Grothendieck topology generated by the qc coverings.

def qcTopology : GrothendieckTopology LocallyQuasiCompactHausdorff.{u}

Stacks.Topology.LocallyQuasiCompactHausdorff.comap_precoverage_le_qcPrecoverage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcTopology.lean, line 225. The attribute's comment: “the qc topology is stronger than the usual one”.

The qc topology is stronger than the usual one. Every open covering of an object of LC, i.e. every jointly surjective family of open embeddings, is a qc covering, because the objects of LC are locally quasi-compact.

theorem comap_precoverage_le_qcPrecoverage :
    TopCat.precoverage.comap locallyQuasiCompactHausdorffToTop.{u} ≤ qcPrecoverage

Stacks.Topology.LocallyQuasiCompactHausdorff.toGrothendieck_comap_precoverage_le_qcTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcTopology.lean, line 241. The attribute's comment: “the qc topology is stronger than the usual one, as topologies”.

The topology of open coverings of LC is coarser than the qc topology.

theorem toGrothendieck_comap_precoverage_le_qcTopology :
    (TopCat.precoverage.comap locallyQuasiCompactHausdorffToTop.{u}).toGrothendieck ≤
      qcTopology

Stacks.Topology.LocallyQuasiCompactZariskiSituation.zariskiTopology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ZariskiSite.lean, line 213. The attribute's comment: “the topology of the site LC_Zar”.

The Zariski Grothendieck topology, on the same category as the quasi-compact site.

def zariskiTopology
    (S : LocallyQuasiCompactZariskiSituation.{u, w} S₀ Bound) :
    GrothendieckTopology S.category

Stacks.Topology.LocallyQuasiCompactZariskiSituation.zariskiObjectCohomology, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ZariskiSite.lean, line 283. The attribute's comment: “the cohomology H^n_Zar(U, H) over an object U of LC_Zar/X”.

Cohomology of an abelian sheaf on the localized Zariski site LC_Zar/X, over an object U over X.

abbrev zariskiObjectCohomology
    (S : LocallyQuasiCompactZariskiSituation.{u, w} S₀ Bound) (X : S.category)
    (F : Sheaf (S.zariskiTopology.over X) AddCommGrpCat.{max (u + 1) v})
    (U : Over X) (n : ℕ)
    [HasSheafify ((S.zariskiTopology.over X).over U) AddCommGrpCat.{max (u + 1) v}]
    [HasExt.{a} (Sheaf ((S.zariskiTopology.over X).over U)
      AddCommGrpCat.{max (u + 1) v})] : Type a

Stacks.Topology.LocallyQuasiCompactZariskiSituation.opensToSlice, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ZariskiSite.lean, line 297. The attribute's comment: “the functor X_Zar → LC_Zar/X, U ↦ U”.

The open subsets of X, as objects over X: the functor Opens X ⥤ LC_Zar/X sending an open U to the open immersion U → X. The accompanying property fixes the underlying map of U as the open embedding with image exactly U, which determines the functor up to the unique isomorphism over X.

noncomputable def opensToSlice
    (S : LocallyQuasiCompactZariskiSituation.{u, w} S₀ Bound) (X : S.category) :
    {F : Opens X.obj ⥤ Over X // ∀ U : Opens X.obj,
      Topology.IsOpenEmbedding ((F.obj U).hom : ((F.obj U).left).obj → X.obj) ∧
      Set.range ((F.obj U).hom : ((F.obj U).left).obj → X.obj) = U.1}

Stacks.Topology.LocallyQuasiCompactZariskiSituation.opensToSlice_isContinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ZariskiSite.lean, line 478. The attribute's comment: “the functor X_Zar → LC_Zar/X is continuous”.

The open-subset functor is continuous from the small Zariski site of X to the localized Zariski site of LC, so it induces the comparison morphism of topoi.

theorem opensToSlice_isContinuous
    (S : LocallyQuasiCompactZariskiSituation.{u, w} S₀ Bound) (X : S.category) :
    (S.opensToSlice X).1.IsContinuous (Opens.grothendieckTopology X.obj)
      (S.zariskiTopology.over X)

Stacks.Topology.opens_hasPullbacks_and_hasTerminal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ZariskiSiteComparison.lean, line 71. The attribute's comment: “X_Zar has fibre products and a final object”.

X_Zar has fibre products and a final object. The category of open subsets of a topological space has fibre products (intersections) and a final object (the whole space).

theorem opens_hasPullbacks_and_hasTerminal (X : TopCat.{u}) :
    HasPullbacks (Opens X) ∧ HasTerminal (Opens X)

Stacks.Topology.sheaf_opens_grothendieckTopology_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ZariskiSiteComparison.lean, line 78. The attribute's comment: “the equality Sh(X_Zar) = Sh(X)”.

Sh(X_Zar) = Sh(X). The sheaves on the small site X_Zar of open subsets of X are by definition the sheaves on the topological space X.

theorem sheaf_opens_grothendieckTopology_eq (X : TopCat.{u}) (A : Type*) [Category* A] :
    Sheaf (Opens.grothendieckTopology X) A = TopCat.Sheaf A X

Stacks.Topology.LocallyQuasiCompactZariskiSituation.ofArrows_mem_zariskiPrecoverage_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ZariskiSiteComparison.lean, line 92. The attribute's comment: “the site LC_Zar: the coverings of LC_qc by open immersions”.

The coverings of LC_Zar. A family of morphisms of LC_qc is a covering of LC_Zar exactly when it is a covering of LC_qc all of whose members are open immersions. A family of open immersions is a qc covering iff it is jointly surjective: a qc covering is jointly surjective, and an open covering is a qc covering because the target is locally quasi-compact.

theorem ofArrows_mem_zariskiPrecoverage_iff {ι : Type*} {T : S.category}
    {Y : ι → S.category} (f : ∀ i, Y i ⟶ T) :
    Presieve.ofArrows Y f ∈ S.zariskiPrecoverage T ↔
      Presieve.ofArrows Y f ∈ S.qcSite.pretopology T ∧
        ∀ i, IsOpenEmbedding (f i : (Y i).obj → T.obj)

Stacks.Topology.LocallyQuasiCompactZariskiSituation.isContinuous_id_zariskiTopology_qc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ZariskiSiteComparison.lean, line 120. The attribute's comment: “the identity functor LC_Zar → LC_qc is continuous”.

The identity functor LC_Zar → LC_qc is continuous, because every covering of LC_Zar is a covering of LC_qc.

theorem isContinuous_id_zariskiTopology_qc :
    (𝟭 S.category).IsContinuous S.zariskiTopology S.qcSite.grothendieckTopology

Stacks.Topology.LocallyQuasiCompactZariskiSituation.qcSiteComparisonMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ZariskiSiteComparison.lean, line 185. The attribute's comment: “the morphism of sites ε : LC_qc → LC_Zar”.

The morphism of sites ε : LC_qc → LC_Zar. The identity functor LC_Zar → LC_qc is continuous (isContinuous_id_zariskiTopology_qc) and its induced functor on sheaves of sets, qc sheafification qcSiteInverseImage, is exact (qcSiteInverseImage_preservesFiniteLimits, qcSiteInverseImage_preservesFiniteColimits); so it defines a morphism of sites, whose morphism of topoi Sh(LC_qc) → Sh(LC_Zar) is this one.

noncomputable def qcSiteComparisonMorphism :
    MorphismOfTopoi
      (Sheaf S.qcSite.grothendieckTopology (Type (max u t)))
      (Sheaf S.zariskiTopology (Type (max u t)))

Stacks.Topology.LocallyQuasiCompactZariskiSituation.opensToSlice_preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ZariskiSiteComparison.lean, line 198. The attribute's comment: “the functor X_Zar → LC_Zar/X commutes with fibre products and final object”.

The functor X_Zar → LC_Zar/X commutes with fibre products and the final object. The functor U ↦ (U → X) is representably flat, so it preserves all finite limits; in particular it carries intersections of opens to fibre products and X to the final object id : X → X.

theorem opensToSlice_preservesFiniteLimits (X : S.category) :
    PreservesFiniteLimits (S.opensToSlice X).1

Stacks.Topology.LocallyQuasiCompactHausdorff, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Compact/LocallyQuasiCompactHausdorffCat.lean, line 48. The attribute's comment: “the category LC of Hausdorff and locally quasi-compact spaces”.

The category of Hausdorff, locally quasi-compact topological spaces and continuous maps.

abbrev LocallyQuasiCompactHausdorff

Stacks.Topology.t2Space_and_locallyCompactSpace_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Compact/LocallyQuasiCompactHausdorffProper.lean, line 47. The attribute's comment: “Hausdorff and locally quasi-compact is the literature's locally compact”.

The convention "Hausdorff and locally quasi-compact". A topological space is Hausdorff and locally quasi-compact (every point has a fundamental system of quasi-compact neighbourhoods) if and only if it is locally compact in the sense often used in the literature: Hausdorff, with every point having a quasi-compact neighbourhood.

theorem t2Space_and_locallyCompactSpace_iff (X : Type u) [TopologicalSpace X] :
    T2Space X ∧ LocallyCompactSpace X ↔ T2Space X ∧ WeaklyLocallyCompactSpace X

Stacks.Topology.LocallyQuasiCompactHausdorff.isSeparatedMap_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Compact/LocallyQuasiCompactHausdorffProper.lean, line 56. The attribute's comment: “any morphism of LC is a separated continuous map”.

Morphisms of LC are separated. The source of a morphism of LC is Hausdorff, so the morphism is a separated continuous map.

theorem isSeparatedMap_hom {X Y : LocallyQuasiCompactHausdorff.{u}} (f : X ⟶ Y) :
    IsSeparatedMap f.hom

Stacks.Topology.LocallyQuasiCompactHausdorff.isProperMap_iff_isUniversallyClosedMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Compact/LocallyQuasiCompactHausdorffProper.lean, line 63. The attribute's comment: “a morphism of LC is proper iff it is universally closed”.

A morphism of LC is proper iff it is universally closed. Proper means separated and universally closed, and every morphism of LC is separated.

theorem isProperMap_iff_isUniversallyClosedMap {X Y : LocallyQuasiCompactHausdorff.{u}}
    (f : X ⟶ Y) :
    StacksDraft.Topology.IsProperMap.{u, u, w} f.hom ↔
      StacksDraft.Topology.IsUniversallyClosedMap.{u, u, w} f.hom

Tag 09WZ, a lemma

Tag 09WZ in the Stacks Project.

Stacks.Topology.LocallyQuasiCompactHausdorff.hasPullbacks, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/FiniteLimits.lean, line 96. The attribute's comment: “fibre_products”.

Stacks 09WZ, the fibre-product clause. The category of Hausdorff, locally quasi-compact spaces has fibre products.

public noncomputable instance hasPullbacks :
    HasPullbacks (LocallyQuasiCompactHausdorff.{u})

Stacks.Topology.LocallyQuasiCompactHausdorff.hasTerminal, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/FiniteLimits.lean, line 119. The attribute's comment: “final_object”.

Stacks 09WZ, the final-object clause. The category of Hausdorff, locally quasi-compact spaces has a final object.

public instance hasTerminal : HasTerminal LocallyQuasiCompactHausdorff.{u}

Stacks.Topology.LocallyQuasiCompactHausdorff.hasFiniteLimits, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/FiniteLimits.lean, line 125. The attribute's comment: “finite_limits”.

Stacks 09WZ, the finite-limits clause. The category of Hausdorff, locally quasi-compact spaces has all finite limits: it has a final object and fibre products.

public noncomputable instance hasFiniteLimits :
    HasFiniteLimits LocallyQuasiCompactHausdorff.{u}

Stacks.Topology.LocallyQuasiCompactHausdorff.compactSpace_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcFibreProducts.lean, line 95. The attribute's comment: “quasi_compact”.

Stacks 09WZ, the quasi-compactness clause. Given morphisms f : X ⟶ Z and g : Y ⟶ Z of Hausdorff, locally quasi-compact spaces with X and Y quasi-compact, the fibre product X ×_Z Y in LC is quasi-compact.

theorem compactSpace_pullback {X Y Z : LocallyQuasiCompactHausdorff.{u}} (f : X ⟶ Z)
    (g : Y ⟶ Z) [CompactSpace X] [CompactSpace Y] :
    CompactSpace (pullback f g : LocallyQuasiCompactHausdorff.{u})

Tag 09X0, a definition

Tag 09X0 in the Stacks Project.

Declarations registered for the tag:

IsQcCovering, declared in the repository, registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcFibreProducts.lean, line 67 (StacksFrontier): “qc coverings of locally quasi-compact Hausdorff spaces”.

Tag 09X1, a lemma

Tag 09X1 in the Stacks Project.

isQcCovering_of_homeomorph, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcCoveringAxioms.lean, line 122. The attribute's comment: “(1)”.

Stacks 09X1 (1). If X' → X is an isomorphism in LC, that is, a homeomorphism of Hausdorff locally quasi-compact spaces, then the singleton family {X' → X} is a qc covering.

theorem isQcCovering_of_homeomorph {X' X : Type*}
    [TopologicalSpace X'] [T2Space X'] [WeaklyLocallyCompactSpace X']
    [TopologicalSpace X] [T2Space X] [WeaklyLocallyCompactSpace X]
    (e : X' ≃ₜ X) :
    IsQcCovering (X := fun _ : Unit => X') (fun _ => (e : X' → X))

isQcCovering_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcCoveringAxioms.lean, line 142. The attribute's comment: “(2)”.

Stacks 09X1 (2). If f is a qc covering of Y and each g i is a qc covering of X i, then the family of composites (i, j) ↦ f i ∘ g i j is a qc covering of Y.

theorem isQcCovering_comp {ι : Type*} {X : ι → Type*} {Y : Type*}
    {J : ι → Type*} {Z : ∀ i, J i → Type*}
    [∀ i, TopologicalSpace (X i)] [TopologicalSpace Y]
    [∀ i, T2Space (X i)] [∀ i, WeaklyLocallyCompactSpace (X i)]
    [T2Space Y] [WeaklyLocallyCompactSpace Y]
    [∀ i j, TopologicalSpace (Z i j)]
    [∀ i j, T2Space (Z i j)] [∀ i j, WeaklyLocallyCompactSpace (Z i j)]
    (f : ∀ i, X i → Y) (hf : ∀ i, Continuous (f i))
    (g : ∀ i (j : J i), Z i j → X i)
    (hcov : IsQcCovering f)
    (hcov' : ∀ i, IsQcCovering (g i)) :
    IsQcCovering (X := fun p : Σ i, J i => Z p.1 p.2)
      (fun p => f p.1 ∘ g p.1 p.2)

isQcCovering_base_change, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcCoveringAxioms.lean, line 175. The attribute's comment: “(3)”.

Stacks 09X1 (3). If f is a qc covering of Y and h : X' → Y is a morphism of LC, then the family of projections pr_{X'} : X' ×_Y X i → X' is a qc covering of X'.

theorem isQcCovering_base_change {ι : Type*} {X : ι → Type*} {Y X' : Type*}
    [∀ i, TopologicalSpace (X i)] [TopologicalSpace Y] [TopologicalSpace X']
    [∀ i, T2Space (X i)] [∀ i, WeaklyLocallyCompactSpace (X i)]
    [T2Space Y] [WeaklyLocallyCompactSpace Y]
    [T2Space X'] [WeaklyLocallyCompactSpace X']
    (f : ∀ i, X i → Y) (hf : ∀ i, Continuous (f i))
    (h : X' → Y) (hh : Continuous h)
    (hcov : IsQcCovering f) :
    IsQcCovering (X := fun i => FiberProd h (f i))
      (fun i => FiberProd.prX' h (f i))

Tag 09X5, a lemma

Tag 09X5 in the Stacks Project.

proper_surjective_isQcCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ProperSurjectiveQcCovering.lean, line 69.

Stacks Tag 09X5 / Lemma 21.31.4. Let X and Y be Hausdorff and locally quasi-compact topological spaces (objects of LC) and let f : X → Y be continuous (a morphism of LC). If f is proper and surjective, then the family {f : X → Y} is a qc covering.

theorem proper_surjective_isQcCovering {X Y : Type*}
    [TopologicalSpace X] [TopologicalSpace Y]
    [T2Space X] [LocallyCompactSpace X] [T2Space Y] [LocallyCompactSpace Y]
    (f : X → Y) (hproper : IsProperMap f)
    (hsurj : Function.Surjective f) :
    IsQuasiCompactCovering f

Tag 09X2, a remark

Tag 09X2 in the Stacks Project.

Stacks.Topology.exists_boundedLCSubcategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/BoundedSubcategory.lean, line 268. The attribute's comment: “the bounded subcategory LC_α”.

Stacks 09X2, the bounded-subcategory clause. Any prescribed small set of Hausdorff, locally quasi-compact spaces is contained in a bounded full subcategory of LC which is closed under existing countable limits and colimits and under the cardinal bound of Equation 046U.

theorem exists_boundedLCSubcategory
    (S₀ : Set LocallyQuasiCompactHausdorff.{u}) [Small.{u} S₀] :
    Nonempty (BoundedLCSubcategory S₀)

Stacks.Topology.LocallyQuasiCompactQcSite, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcSite.lean, line 201. The attribute's comment: “the site LC_qc”.

Stacks 09X2, the site clause. The data defining the big quasi-compact site LC_qc.

Its objects form the cardinal-cutoff bounded subcategory supplied by Stacks.Topology.BoundedLCSubcategory, with an additional representative condition for the prescribed cardinal bound. Its chosen pretopology is represented by quasi-compact covering families indexed in Type w, and every quasi-compact presieve has a combinatorially equivalent chosen representative.

structure LocallyQuasiCompactQcSite
    (initialObjects : Set LocallyQuasiCompactHausdorff.{u})
    (bound : Cardinal.{u} → Cardinal.{u})

Stacks.Topology.exists_locallyQuasiCompactQcSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcSite.lean, line 434. The attribute's comment: “the set of coverings”.

Stacks 09X2, the covering-set clause. On any prescribed bounded subcategory LC_α of LC there is a set of quasi-compact covering families which forms a pretopology and contains a combinatorially equivalent representative of every quasi-compact covering family; that is, the quasi-compact site LC_qc exists on LC_α.

The set of coverings is the one generated by all quasi-compact families: the three site axioms are Stacks 09X1, and the representative condition is satisfied by the family itself, which is legitimate because the families on LC_α indexed in Type (u + 1) already form a set.

theorem exists_locallyQuasiCompactQcSite
    (S₀ : Set LocallyQuasiCompactHausdorff.{u})
    (B : BoundedLCSubcategory S₀) :
    ∃ S : LocallyQuasiCompactQcSite.{u, u + 1} S₀ Cardinal.stacksBound,
      S.boundedSubcategory = B

Stacks.Topology.LocallyQuasiCompactQcSite.mem_smallPretopology_iff_isQcCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcSmallModel.lean, line 193. The attribute's comment: “the coverings of a small model of LC_qc are the quasi-compact coverings”.

Stacks 09X2, the smallness clause. The small model really is the quasi-compact site: a presieve of it is covering exactly when the sieve it generates, read in LC_qc, is refined by a quasi-compact covering family.

The pretopology of the small model is the maximal one generating the transported topology, so membership in it unwinds to membership of a generated sieve in the topology generated by the chosen set Cov of quasi-compact coverings, which is isCovering_iff_isQcCovering.

theorem mem_smallPretopology_iff_isQcCovering {Y : S.smallSite} (R : Presieve Y) :
    R ∈ S.smallPretopology Y ↔
      ∃ E : PreZeroHypercover.{u + 1} (S.smallEquivalence.inverse.obj Y),
        S.IsQcCovering E ∧
          E.presieve₀ ≤
            ((Sieve.generate R).functorPushforward S.smallEquivalence.inverse).arrows

Stacks.Topology.LocallyQuasiCompactQcSite.smallSheafEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcSmallModel.lean, line 238. The attribute's comment: “LC_qc and a small model of it have the same topos”.

Stacks 09X2, the topos clause. Sheaves on LC_qc and sheaves on its small model are the same, at any coefficients. The comparison is a dense subsite inclusion for the transported topology, so restriction along it is an equivalence.

def smallSheafEquiv (A : Type t₁) [Category.{t₂} A] :
    Sheaf S.grothendieckTopology A ≌ Sheaf S.smallTopology A

Tag 09X3, a lemma

Tag 09X3 in the Stacks Project.

Stacks.Topology.LocallyQuasiCompactZariskiSituation.qcDirectImageTopologicalInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcComparisonEmbedding.lean, line 87. The attribute's comment: “the identification eps_{X,*}a_X^{-1} = pi_X^{-1} on sheaves of sets”.

Stacks 09X3, the identification ε_{X,*} a_X^{-1} = π_X^{-1}. Direct image along the change-of-topology morphism undoes quasi-compact sheafification on the Zariski comparison inverse images, because those are already quasi-compact sheaves.

def qcDirectImageTopologicalInverseImageIso (X : S.category) :
    qcTopologicalInverseImage.{u, w, t} S X ⋙ qcDirectImage.{u, w, t} S X ≅
      comparisonInverseImage.{u, w, t} S X

Stacks.Topology.LocallyQuasiCompactZariskiSituation.qcTopologicalInverseImage_fullyFaithful, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcComparisonEmbedding.lean, line 108. The attribute's comment: “full faithfulness of the composite inverse image a_X^{-1} on sheaves of sets”.

Stacks 09X3, full faithfulness of a_X^{-1}. The inverse image along the comparison morphism a_X = π_X ∘ ε_X : Sh(LC_qc/X) → Sh(X) is full and faithful on sheaves of sets.

This is the sentence Stacks 0DAG opens with, for the bottom horizontal arrow of the diagram of Stacks 0DAF: (h_{-1})^{-1} is fully faithful with quasi-inverse h_{-1,*}.

Composing with ε_{X,*} gives π_X^{-1} up to the isomorphism qcDirectImageTopologicalInverseImageIso; that composite is therefore fully faithful, and ε_{X,*} is faithful, so a_X^{-1} is fully faithful.

theorem qcTopologicalInverseImage_fullyFaithful (X : S.category) :
    (qcTopologicalInverseImage.{u, w, t} S X).Full ∧
      (qcTopologicalInverseImage.{u, w, t} S X).Faithful

Stacks.Topology.LocallyQuasiCompactZariskiSituation.qcTopologicalAdjunction_unit_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcComparisonEmbedding.lean, line 129. The attribute's comment: “the unit of a_X^{-1} is invertible on sheaves of sets”.

Stacks 09X3, the quasi-inverse clause. The unit of the adjunction a_X^{-1} ⊣ a_{X,*} of the comparison morphism of topoi is an isomorphism: a_{X,*} recovers every sheaf on the space from its inverse image.

theorem qcTopologicalAdjunction_unit_isIso (X : S.category) :
    IsIso (qcTopologicalMorphism.{u, w, t} S X).adj.unit

Stacks.Topology.LocallyQuasiCompactZariskiSituation.isSheaf_qc_germSectionsPresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcGermSectionsSheaf.lean, line 208. The attribute's comment: “the qc sheaf condition”.

The presheaf on the localized quasi-compact site LC_qc/X' whose sections over h : W ⟶ X' are the global sections of the germ-model inverse image h^{-1}F is a sheaf.

theorem isSheaf_qc_germSectionsPresheaf
    (S : LocallyQuasiCompactZariskiSituation.{u, w} S₀ Bound) (X' : S.category)
    (F : Sheaf (Opens.grothendieckTopology X'.obj) (Type (max u t))) :
    Presheaf.IsSheaf (S.qcSite.grothendieckTopology.over X')
      (germSectionsPresheaf S X' F)

Stacks.Topology.LocallyQuasiCompactZariskiSituation.isIso_toSheafify_comparisonInverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcGermSectionsSheaf.lean, line 296. The attribute's comment: “the composite inverse image”.

The unit of quasi-compact sheafification is an isomorphism on the comparison inverse image π_{X'}^{-1}F: ε_{X'}^{-1}π_{X'}^{-1}F is π_{X'}^{-1}F.

theorem isIso_toSheafify_comparisonInverseImage
    (S : LocallyQuasiCompactZariskiSituation.{u, w} S₀ Bound) (X' : S.category)
    (F : Sheaf (Opens.grothendieckTopology X'.obj) (Type (max u t))) :
    IsIso (toSheafify (S.qcSite.grothendieckTopology.over X')
      ((comparisonInverseImage.{u, w, t} S X').obj F).obj)

Stacks.Topology.LocallyQuasiCompactZariskiSituation.isSheaf_germSectionsPresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ZariskiGermSectionsSheaf.lean, line 262. The attribute's comment: “the Zariski sheaf condition”.

The germ-model sections presheaf is a sheaf. The presheaf on the localized Zariski site LC_Zar/X' whose sections over h : W ⟶ X' are the global sections of the germ-model inverse image h^{-1}F satisfies the sheaf condition for the localized Zariski topology: an open covering of W by objects of the site and a family of germ sections agreeing on the overlaps determine a unique germ section on W. This is the first assertion of Stacks 09X3.

theorem isSheaf_germSectionsPresheaf
    (S : LocallyQuasiCompactZariskiSituation.{u, w} S₀ Bound) (X' : S.category)
    (F : Sheaf (Opens.grothendieckTopology X'.obj) (Type (max u t))) :
    Presheaf.IsSheaf (S.zariskiTopology.over X') (germSectionsPresheaf S X' F)

Stacks.Topology.LocallyQuasiCompactZariskiSituation.germSectionsPresheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ZariskiProperBaseChangeClause.lean, line 93. The attribute's comment: “the sections formula on LC_Zar/X”.

The sections formula of Stacks 09X3 for the Zariski site, naturally in the object of the localized site. For an object X' of the locally quasi-compact Zariski site and a sheaf of sets F on its space, the comparison inverse image π_{X'}^{-1}F is the germ-model sections presheaf

(h : W ⟶ X') ↦ Γ(W, h^{-1}F),

as presheaves on the localized Zariski site LC_Zar/X'.

The identification is read off the universal property rather than computed on either side: the germ-model sections sheaf corepresents morphisms out of the comparison inverse image (germSectionsMapOutProperty), which the comparison inverse image corepresents by its own adjunction, so the two agree.

def germSectionsPresheafIso (X' : S.category)
    (F : Sheaf (Opens.grothendieckTopology X'.obj) (Type (max u t))) :
    ((comparisonInverseImage.{u, w, t} S X').obj F).obj ≅ germSectionsPresheaf S X' F

Tag 0DCU, a lemma

Tag 0DCU in the Stacks Project.

Stacks.Topology.LocallyQuasiCompactZariskiSituation.properDirectImageComparisonIsoOfProperMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ProperBaseChangeSurjective.lean, line 603. The attribute's comment: “proper_direct_image”.

Stacks 0DCU, clause (7a): the proper direct image clause. For a proper morphism f of the locally quasi-compact Zariski site, ordinary direct image of sheaves of sets along the underlying continuous map commutes with inverse image along the comparison morphisms to the Zariski slice topoi:

π_Y^{-1} ∘ f_* ≅ f_{Zar,*} ∘ π_X^{-1}.

Properness is the only hypothesis. This is properDirectImageComparisonIso, whose hypothesis on the Y-side counit is discharged by isIso_properBaseChangeCounit, which is proper base change for sheaves of sets, Stacks 0D90, in the form the Zariski comparison needs.

def properDirectImageComparisonIsoOfProperMap
    (hf : StacksDraft.Topology.IsProperMap.{u, u, u}
      (((S.qcSite.inclusion ⋙ locallyQuasiCompactHausdorffToTop).map f) : X.obj → Y.obj)) :
    TopCat.Sheaf.pushforward (Type (max (u + 1) v))
        ((S.qcSite.inclusion ⋙ locallyQuasiCompactHausdorffToTop).map f) ⋙
      S.comparisonInverseImage.{u, w, max (u + 1) v} Y ≅
    S.comparisonInverseImage.{u, w, max (u + 1) v} X ⋙
      (zariskiSliceMorphism.{u, w, max (u + 1) v} S f).pushforward

Stacks.Topology.LocallyQuasiCompactZariskiSituation.properDerivedImageComparison_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ProperDerivedImageIso.lean, line 348. The attribute's comment: “proper_derived_image”.

[Stacks, Tag 0DCU], the derived clause: the derived Zariski base-change map of a proper morphism is an isomorphism. For f : X ⟶ Y a proper morphism of the locally quasi-compact Zariski site, the comparison π_Y^{-1} ∘ Rf_* ⟶ Rf_{Zar,*} ∘ π_X^{-1} of properDerivedImageComparison is invertible.

This is isIso_properDerivedImageComparison_of_locallyZero_cohomologyPresheaf fed equalizerSieve_mem_over_of_isProperMap.

theorem properDerivedImageComparison_isIso
    (hf : StacksDraft.Topology.IsProperMap.{u, u, u}
      (((S.qcSite.inclusion ⋙ locallyQuasiCompactHausdorffToTop).map f) : X.obj → Y.obj)) :
    IsIso (properDerivedImageComparison.{u, w, v} S f)

Stacks.Topology.LocallyQuasiCompactZariskiSituation.properDerivedImageComparison_isIso_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ProperDerivedImageIso.lean, line 372. The attribute's comment: “proper_derived_image, with the four sheafifications and the three enough-injectives inputs discharged rather than assumed”.

[Stacks, Tag 0DCU], the derived clause, with properness as the only hypothesis. For f : X ⟶ Y a proper morphism of the locally quasi-compact Zariski site, the comparison π_Y^{-1} ∘ Rf_* ⟶ Rf_{Zar,*} ∘ π_X^{-1} of properDerivedImageComparison is invertible.

The four sheafifications and the three enough-injectives inputs the derived functors are built from are not assumed: all four sites are essentially small at this coefficient universe, so hasSheafify_opensSite, hasSheafify_zariskiSlice, enoughInjectives_spaceSheaf and enoughInjectives_zariskiSliceSheaf supply them.

theorem properDerivedImageComparison_isIso_unconditional
    (hf : StacksDraft.Topology.IsProperMap.{u, u, u}
      (((S.qcSite.inclusion ⋙ locallyQuasiCompactHausdorffToTop).map f) : X.obj → Y.obj)) :
    letI := hasSheafify_opensSite.{u, w, v} S X
    letI := hasSheafify_opensSite.{u, w, v} S Y
    letI := hasSheafify_zariskiSlice.{u, w, v} S X
    letI := hasSheafify_zariskiSlice.{u, w, v} S Y
    letI := enoughInjectives_spaceSheaf.{u, w, v} S X
    letI := enoughInjectives_spaceSheaf.{u, w, v} S Y
    letI := enoughInjectives_zariskiSliceSheaf.{u, w, v} S X
    IsIso (properDerivedImageComparison.{u, w, v} S f)

Stacks.Topology.LocallyQuasiCompactZariskiSituation.zariskiCohomologyComparisonIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ZariskiCohomologyComparison.lean, line 291. The attribute's comment: “cohomology_comparison”.

The cohomology comparison for the Zariski comparison morphism. For an abelian sheaf F on the space of an object X of the locally quasi-compact Zariski site, the cohomology of the localized Zariski site with coefficients in π_X^{-1}F is the cohomology of the space X with coefficients in F:

H^n_{Zar}(X, π_X^{-1}F) ≅ H^n(X, F),

naturally in F. This is clause (1) of Stacks 0DCU.

def zariskiCohomologyComparisonIso (n : ℕ) :
    S.abelianComparisonInverseImage.{u, w, max (u + 1) v} X ⋙
        Sheaf.functorH (S.zariskiTopology.over X) n ≅
      Sheaf.functorH (Opens.grothendieckTopology X.obj) n

Stacks.Topology.LocallyQuasiCompactZariskiSituation.zariskiCohomologyComparisonIso_unconditional, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ZariskiCohomologyComparison.lean, line 327. The attribute's comment: “cohomology_comparison, with the sheafifications, the injective resolutions and the universe of the Ext-groups discharged rather than assumed”.

The cohomology comparison for the Zariski comparison morphism, with no hypothesis. For an abelian sheaf F on the space of an object X of the locally quasi-compact Zariski site,

H^n_{Zar}(X, π_X^{-1}F) ≅ H^n(X, F),

naturally in F. This is clause (1) of Stacks 0DCU.

Nothing is assumed of the two sites: both are essentially small at this coefficient universe, so the sheafifications, the injective resolutions and the universe of the Ext-groups that Sheaf.functorH is built from are supplied by hasSheafify_opensSite, hasSheafify_zariskiSlice, hasInjectiveResolutions_spaceSheaf, hasInjectiveResolutions_zariskiSliceSheaf, hasExt_spaceSheaf and hasExt_zariskiSliceSheaf.

def zariskiCohomologyComparisonIso_unconditional (n : ℕ) :
    letI := hasSheafify_opensSite.{u, w, v} S X
    letI := hasSheafify_zariskiSlice.{u, w, v} S X
    letI := hasExt_spaceSheaf.{u, w, v} S X
    letI := hasExt_zariskiSliceSheaf.{u, w, v} S X
    letI := hasInjectiveResolutions_spaceSheaf.{u, w, v} S X
    letI := hasInjectiveResolutions_zariskiSliceSheaf.{u, w, v} S X
    S.abelianComparisonInverseImage.{u, w, max (u + 1) v} X ⋙
        Sheaf.functorH (S.zariskiTopology.over X) n ≅
      Sheaf.functorH (Opens.grothendieckTopology X.obj) n

Stacks.Topology.LocallyQuasiCompactZariskiSituation.abelianComparisonAdjunction_unit_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ZariskiComparisonEmbedding.lean, line 292. The attribute's comment: “unit_isomorphism”.

Stacks 0DCU, the unit clause. The unit of the Zariski comparison adjunction on abelian sheaves is an isomorphism: the inverse image π_X^{-1} is fully faithful, because opensToSlice is continuous, cocontinuous, full and faithful.

theorem abelianComparisonAdjunction_unit_isIso
    (S : LocallyQuasiCompactZariskiSituation.{u, w} S₀ Bound)
    (X : S.category) :
    IsIso (S.abelianComparisonAdjunction.{u, w, max (u + 1) v} X).unit

Stacks.Topology.LocallyQuasiCompactZariskiSituation.abelianComparisonDirectImage_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ZariskiComparisonExactness.lean, line 362. The attribute's comment: “exact_direct_image”.

Stacks 0DCU, the exact-direct-image clause. The direct image from the Zariski slice site of an object to the Zariski site of its underlying space is exact on abelian sheaves.

theorem abelianComparisonDirectImage_exact
    {S₀ : Set LocallyQuasiCompactHausdorff.{u}} {Bound : Cardinal.{u} → Cardinal.{u}}
    (S : LocallyQuasiCompactZariskiSituation.{u, w} S₀ Bound)
    (X : S.category) :
    exactFunctor
      (Sheaf (S.zariskiTopology.over X) AddCommGrpCat.{max (u + 1) v})
      (Sheaf (Opens.grothendieckTopology X.obj) AddCommGrpCat.{max (u + 1) v})
      (S.comparisonDirectImage X AddCommGrpCat.{max (u + 1) v})

Stacks.Topology.LocallyQuasiCompactZariskiSituation.zariskiComparisonSquareIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ZariskiComparisonNaturality.lean, line 398. The attribute's comment: “commutative_square”.

Stacks 0DCU, clause (5): the commutative square of topoi. The square whose horizontal arrows are f_Zar : Sh(LC_Zar/X) → Sh(LC_Zar/Y) and f : Sh(X_Zar) → Sh(Y_Zar) and whose vertical arrows are the comparison morphisms π_X and π_Y commutes: read on inverse images, which is where a morphism of topoi lives, π_X^{-1} ∘ f^{-1} ≅ f_Zar^{-1} ∘ π_Y^{-1}.

It is obtained from zariskiComparisonDirectImageSquareIso by uniqueness of left adjoints, using the specified comparison and slice adjunctions.

The coefficients are types in an arbitrary universe containing the universe of the spaces.

def zariskiComparisonSquareIso :
    (Opens.map ((S.qcSite.inclusion ⋙ locallyQuasiCompactHausdorffToTop).map f)).sheafPullback
        (Type (max u t))
        (Opens.grothendieckTopology
          ((S.qcSite.inclusion ⋙ locallyQuasiCompactHausdorffToTop).obj Y))
        (Opens.grothendieckTopology
          ((S.qcSite.inclusion ⋙ locallyQuasiCompactHausdorffToTop).obj X)) ⋙
      comparisonInverseImage.{u, w, t} S X ≅
    comparisonInverseImage.{u, w, t} S Y ⋙ (zariskiSliceMorphism.{u, w, t} S f).inverseImage

Stacks.Topology.LocallyQuasiCompactZariskiSituation.abelianDerivedComparisonAdjunction_unit_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ZariskiDerivedUnit.lean, line 164. The attribute's comment: “derived_unit”.

Stacks 0DCU, the derived-unit clause. The canonical map from a complex of abelian sheaves on the space X to the derived direct image of its inverse image on the localized Zariski site is an isomorphism, naturally in the complex.

theorem abelianDerivedComparisonAdjunction_unit_isIso
    (S : LocallyQuasiCompactZariskiSituation.{u, w} S₀ Bound)
    (X : S.category)
    [HasSheafify (Opens.grothendieckTopology X.obj) AddCommGrpCat.{max (u + 1) v}]
    [HasSheafify (S.zariskiTopology.over X) AddCommGrpCat.{max (u + 1) v}] :
    IsIso (abelianDerivedComparisonAdjunction.{u, w, v} S X).unit

Stacks.Topology.LocallyQuasiCompactZariskiSituation.abelianDerivedComparisonAdjunction_unit_isIso_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ZariskiDerivedUnit.lean, line 204. The attribute's comment: “derived_unit, with the two sheafifications discharged rather than assumed”.

Stacks 0DCU, the derived-unit clause, with no hypothesis. The canonical map from a complex of abelian sheaves on the space X to the derived direct image of its inverse image on the localized Zariski site is an isomorphism, naturally in the complex.

The two sheafifications the derived adjunction is built from are not assumed: both sites are essentially small at this coefficient universe, so hasSheafify_opensSite and hasSheafify_zariskiSlice supply them.

theorem abelianDerivedComparisonAdjunction_unit_isIso_unconditional
    (S : LocallyQuasiCompactZariskiSituation.{u, w} S₀ Bound)
    (X : S.category) :
    letI := hasSheafify_opensSite.{u, w, v} S X
    letI := hasSheafify_zariskiSlice.{u, w, v} S X
    IsIso (abelianDerivedComparisonAdjunction.{u, w, v} S X).unit

Stacks.Topology.LocallyQuasiCompactZariskiSituation.relativeZariskiCohomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ZariskiRelativeCohomology.lean, line 434. The attribute's comment: “relative_cohomology”.

Stacks 0DCU, clause (6): the relative-cohomology clause. For a morphism f : X ⟶ Y of the locally quasi-compact Zariski site and L ∈ D⁺(Y), the cohomology of π_Y^{-1}L over the object X/Y of the localized Zariski site is the cohomology of the space X with coefficients in f^{-1}L:

H^n_{Zar}(X, π_Y^{-1}L) ≅ H^n(X, f^{-1}L),

naturally in L.

def relativeZariskiCohomologyIso
    (S : LocallyQuasiCompactZariskiSituation.{u, w} S₀ Bound) {X Y : S.category} (f : X ⟶ Y)
    (n : ℤ)
    [HasSheafify (Opens.grothendieckTopology X.obj) AddCommGrpCat.{max (u + 1) v}]
    [HasSheafify (Opens.grothendieckTopology Y.obj) AddCommGrpCat.{max (u + 1) v}]
    [HasSheafify (S.zariskiTopology.over X) AddCommGrpCat.{max (u + 1) v}]
    [HasSheafify (S.zariskiTopology.over Y) AddCommGrpCat.{max (u + 1) v}]
    [EnoughInjectives
      (Sheaf (Opens.grothendieckTopology X.obj) AddCommGrpCat.{max (u + 1) v})]
    [EnoughInjectives
      (Sheaf (Opens.grothendieckTopology Y.obj) AddCommGrpCat.{max (u + 1) v})]
    [EnoughInjectives (Sheaf (S.zariskiTopology.over X) AddCommGrpCat.{max (u + 1) v})]
    [EnoughInjectives (Sheaf (S.zariskiTopology.over Y) AddCommGrpCat.{max (u + 1) v})] :
    (S.abelianComparisonInverseImage.{u, w, max (u + 1) v} Y).rightDerivedFunctorPlus ⋙
        ((sheafSections (S.zariskiTopology.over Y)
            AddCommGrpCat.{max (u + 1) v}).obj (op (Over.mk f))).rightDerivedFunctorPlus ⋙
        DerivedCategory.Plus.homologyFunctor AddCommGrpCat.{max (u + 1) v} n ≅
      ((Opens.map
              ((S.qcSite.inclusion ⋙ locallyQuasiCompactHausdorffToTop).map f)).sheafPullback
            AddCommGrpCat.{max (u + 1) v} (Opens.grothendieckTopology Y.obj)
            (Opens.grothendieckTopology X.obj)).rightDerivedFunctorPlus ⋙
        ((sheafSections (Opens.grothendieckTopology X.obj)
            AddCommGrpCat.{max (u + 1) v}).obj
          (op (⊤ : Opens X.obj))).rightDerivedFunctorPlus ⋙
        DerivedCategory.Plus.homologyFunctor AddCommGrpCat.{max (u + 1) v} n

Stacks.Topology.LocallyQuasiCompactZariskiSituation.relativeZariskiCohomologyIso_unconditional, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ZariskiRelativeCohomology.lean, line 552. The attribute's comment: “relative_cohomology, with the four sheafifications and the four enough-injectives inputs discharged rather than assumed”.

Stacks 0DCU, clause (6): the relative-cohomology clause, with no hypothesis. For a morphism f : X ⟶ Y of the locally quasi-compact Zariski site and L ∈ D⁺(Y),

H^n_{Zar}(X, π_Y^{-1}L) ≅ H^n(X, f^{-1}L),

naturally in L.

Nothing is assumed of the two sites. The four sheafifications and the four enough-injectives inputs the bounded below right derived functors are built from are supplied by hasSheafify_opensSite, hasSheafify_zariskiSlice, enoughInjectives_spaceSheaf and enoughInjectives_zariskiSliceSheaf, each of which holds because the site in question is essentially small at this coefficient universe.

def relativeZariskiCohomologyIso_unconditional
    (S : LocallyQuasiCompactZariskiSituation.{u, w} S₀ Bound) {X Y : S.category} (f : X ⟶ Y)
    (n : ℤ) :
    letI := hasSheafify_opensSite.{u, w, v} S X
    letI := hasSheafify_opensSite.{u, w, v} S Y
    letI := hasSheafify_zariskiSlice.{u, w, v} S X
    letI := hasSheafify_zariskiSlice.{u, w, v} S Y
    letI := enoughInjectives_spaceSheaf.{u, w, v} S X
    letI := enoughInjectives_spaceSheaf.{u, w, v} S Y
    letI := enoughInjectives_zariskiSliceSheaf.{u, w, v} S X
    letI := enoughInjectives_zariskiSliceSheaf.{u, w, v} S Y
    (S.abelianComparisonInverseImage.{u, w, max (u + 1) v} Y).rightDerivedFunctorPlus ⋙
        ((sheafSections (S.zariskiTopology.over Y)
            AddCommGrpCat.{max (u + 1) v}).obj (op (Over.mk f))).rightDerivedFunctorPlus ⋙
        DerivedCategory.Plus.homologyFunctor AddCommGrpCat.{max (u + 1) v} n ≅
      ((Opens.map
              ((S.qcSite.inclusion ⋙ locallyQuasiCompactHausdorffToTop).map f)).sheafPullback
            AddCommGrpCat.{max (u + 1) v} (Opens.grothendieckTopology Y.obj)
            (Opens.grothendieckTopology X.obj)).rightDerivedFunctorPlus ⋙
        ((sheafSections (Opens.grothendieckTopology X.obj)
            AddCommGrpCat.{max (u + 1) v}).obj
          (op (⊤ : Opens X.obj))).rightDerivedFunctorPlus ⋙
        DerivedCategory.Plus.homologyFunctor AddCommGrpCat.{max (u + 1) v} n

Tag 0D92, a lemma

Tag 0D92 in the Stacks Project.

Stacks.Topology.LocallyQuasiCompactZariskiSituation.topologyChangeSquareIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcComparisonNaturality.lean, line 251. The attribute's comment: “change-of-topology square”.

Stacks 0D92, the change-of-topology square. The change-of-topology morphisms commute with the morphisms of slice topoi induced by f: ε_X^{-1} ∘ f_{Zar}^{-1} ≅ f_{qc}^{-1} ∘ ε_Y^{-1}.

On direct images the square commutes strictly, because the change-of-topology direct image leaves the underlying presheaf unchanged; both sides of the square on inverse images are left adjoints of the two sides of that identity, so the isomorphism is the one supplied by uniqueness of left adjoints.

def topologyChangeSquareIso :
    (zariskiSliceMorphism.{u, w, t} S f).inverseImage ⋙ qcInverseImage.{u, w, t} S X ≅
      qcInverseImage.{u, w, t} S Y ⋙ qcSliceInverseImage.{u, w, t} S f

Stacks.Topology.LocallyQuasiCompactZariskiSituation.qcTopologicalComparisonSquareIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcComparisonNaturality.lean, line 281. The attribute's comment: “topological comparison square”.

Stacks 0D92, the topological comparison square. The comparison morphisms a_X = π_X ∘ ε_X to sheaves on the underlying spaces commute with the morphisms of slice topoi induced by f: a_X^{-1} ∘ g^{-1} ≅ f_{qc}^{-1} ∘ a_Y^{-1}, where g is the underlying continuous map of f.

It is the Zariski square of Stacks 0DCU followed by the change-of-topology square.

def qcTopologicalComparisonSquareIso :
    (Opens.map ((S.qcSite.inclusion ⋙ locallyQuasiCompactHausdorffToTop).map f)).sheafPullback
        (Type (max u t))
        (Opens.grothendieckTopology
          ((S.qcSite.inclusion ⋙ locallyQuasiCompactHausdorffToTop).obj Y))
        (Opens.grothendieckTopology
          ((S.qcSite.inclusion ⋙ locallyQuasiCompactHausdorffToTop).obj X)) ⋙
      qcTopologicalInverseImage.{u, w, t} S X ≅
    qcTopologicalInverseImage.{u, w, t} S Y ⋙ qcSliceInverseImage.{u, w, t} S f

Stacks.Topology.LocallyQuasiCompactZariskiSituation.qcTopologicalProperDirectImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcComparisonNaturality.lean, line 395. The attribute's comment: “proper direct image”.

Stacks 0D92, the proper direct image clause. If the underlying continuous map of f : X ⟶ Y is proper, then direct image of sheaves of sets along it commutes with inverse image along the comparison morphisms a_X, a_Y to sheaves on the underlying spaces: a_Y^{-1} ∘ f_* = f_{qc,*} ∘ a_X^{-1}.

This is qcTopologicalBaseChangeMap with its invertibility supplied by isIso_qcTopologicalBaseChangeMap.

def qcTopologicalProperDirectImageIso
    (hf : StacksDraft.Topology.IsProperMap.{u, u, u} ⇑((siteToTop S).map f)) :
    spaceDirectImage S f (Type u) ⋙ qcTopologicalInverseImage.{u, w, u} S Y ≅
      qcTopologicalInverseImage.{u, w, u} S X ⋙ qcSliceDirectImage.{u, w, u} S f

Tag 0EZI, a lemma

Tag 0EZI in the Stacks Project.

Stacks.Topology.LocallyQuasiCompactZariskiSituation.exists_isPullback_properMorphisms, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ZariskiComparisonSituationData.lean, line 75. The attribute's comment: “condition (0EZ4) of Situation 0EZ3 for the proper maps of LC”.

A proper arrow of the site admits a base change along an arbitrary arrow, and that base change is again proper.

theorem exists_isPullback_properMorphisms
    (S : LocallyQuasiCompactZariskiSituation.{u, w} S₀ Bound)
    ⦃X Y Y' : S.category⦄ (f : X ⟶ Y) (hf : S.properMorphisms f) (g : Y' ⟶ Y) :
    ∃ (Z : S.category) (q : Z ⟶ X) (p : Z ⟶ Y'),
      IsPullback q p f g ∧ S.properMorphisms p

Stacks.Topology.LocallyQuasiCompactZariskiSituation.zariskiPullbackClass_overMapPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ZariskiComparisonSituationData.lean, line 138. The attribute's comment: “condition (0EZ5) of Situation 0EZ3 for the sheaves pulled back from the space”.

Restriction along an arrow f : X ⟶ Y of the site carries the sheaves pulled back from Y to the sheaves pulled back from X: a restriction of π_Y^{-1}G is π_X^{-1} of the inverse image of G along the underlying map of f.

theorem zariskiPullbackClass_overMapPullback
    (S : LocallyQuasiCompactZariskiSituation.{u, w} S₀ Bound)
    ⦃X Y : S.category⦄ (f : X ⟶ Y)
    (F : Sheaf (S.zariskiTopology.over Y) AddCommGrpCat.{max (u + 1) v})
    (hF : S.zariskiPullbackClass.{u, w, v} Y F) :
    S.zariskiPullbackClass.{u, w, v} X
      ((S.zariskiTopology.overMapPullback AddCommGrpCat.{max (u + 1) v} f).obj F)

Stacks.Topology.LocallyQuasiCompactZariskiSituation.zariskiPullbackClass_rightDerived_overMapPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ZariskiHigherDirectImageClass.lean, line 224. The attribute's comment: “condition (4) of Situation 0EZ3 for this situation: all higher direct images along a proper arrow of a sheaf pulled back from the space are again pulled back from the space. This is the field ComparingTopologies.CohomologyComparison.weakSerre_rightDerived_relocalizationPushforward, proved outright for every i, with the witness R^i g_* G specified rather than obtained from the existential. The five conditions of Situation 0EZ3 are items (1)-(5) of that tag; the (0EZ4)/(0EZ5)/(0EZ6)/(0EZ7) names used elsewhere in this directory are this development's own, and this is (0EZ7). ALL FIVE CONDITIONS ARE NOW PROVED: the other four are morphismProperty_baseChange and weakSerre_relocalizationInverseImage (ZariskiComparisonSituationData.lean), weakSerre_isSheaf_fine (isSheaf_qc_zariskiPullbackClass, ZariskiPullbackClassQcSheaf.lean) and covering_refinement (exists_zariskiRefinement_properMorphisms, ZariskiQcCoveringRefinement.lean). SITUATION 0EZ3 IS STILL NOT INSTANTIATED HERE, AND THIS CONDITION IS WHAT BLOCKS IT. The carrier is settled: CohomologyComparison is declared for [SmallCategory C] with coefficients Ab in the carrier's own universe, S.category is Type (u+1) with morphisms in Type u, and the carrier is CategoryTheory.SmallModel S.category in Type u, EssentiallySmall.{u} S.category being the instance LocallyQuasiCompactQcSite.category_essentiallySmall. That fixes the coefficients at AddCommGrpCat.{u}, where the sheaf condition is proved and where the restriction condition zariskiPullbackClass_overMapPullback now also holds, being stated for every AddCommGrpCat.{max u t}. THIS condition is stated only at AddCommGrpCat.{max (u+1) v}. ONE of the seven inputs of its proof now reaches AddCommGrpCat.{u}, being stated for every AddCommGrpCat.{max u t}: abelianComparisonInverseImage_exact (ZariskiSite.lean). That was the input believed OBSTRUCTED rather than merely unrestated, because it went through Small.{max (u+1) v} ((S.zariskiTopology.over X).Cover Y)ᵒᵖ and the slice's covering sieves do live in Type (u+1); it turns out not to need them, and now takes the essentiallySmall_over route, its Kan-extension shapes being u-small by small_costructuredArrow_opensToSlice. The other six still carry max (u+1) v -- topologicalPushforward and zariskiBaseChange (ProperDerivedImage.lean), isIso_zariskiBaseChange_of_properMap (AbelianProperDirectImage.lean), preservesFiniteLimits_zariskiSlicePushforward (AcyclicityReduction.lean), and isZero_rightDerived_sliceDirectImage_abelianComparisonInverseImage with rightDerivedZariskiBaseChangeIso here. THE NEXT ONE NEEDS A LEMMA THAT DOES NOT EXIST: restating preservesFiniteLimits_zariskiSlicePushforward at max u t fails even with both sheafifications built from essentiallySmall_over, because (Over.pullback f).sheafPushforwardContinuous is a right adjoint only when the left Kan extension along (Over.pullback f).op exists, which needs Small.{max u t} (CostructuredArrow (Over.pullback f).op Z). Those comma categories are indexed by Over Y, in Type (u+1); at max (u+1) v their smallness is free from Small.{max (u+1) v} α for every α : Type (max (u+1) v) (Sheafification.lean), the one step that really uses u+1 ≤ max (u+1) v, and at max u t there is no such instance. What is owed is the analogue of small_costructuredArrow_opensToSlice for Over.pullback f. Past it the rest is RESTATEMENT, made large only because these facts are supplied as INSTANCES and an instance generalized to max u t is unusable -- max u ?t =?= max (u+1) v is not solvable by instance synthesis -- so each remaining input must take them as local haves, across the 32 files here that mention max (u+1) v. Transporting the conditions along equivSmallModel is also not done”.

Every higher direct image along a proper arrow f : X ⟶ Y of a sheaf pulled back from the space X is again pulled back from the space Y: if F lies in zariskiPullbackClass X then R^i f_{Zar,*}F lies in zariskiPullbackClass Y, for every i : ℕ.

theorem zariskiPullbackClass_rightDerived_overMapPushforward (hf : S.properMorphisms f)
    (F : Sheaf (S.zariskiTopology.over X) AddCommGrpCat.{max (u + 1) v})
    (hF : S.zariskiPullbackClass.{u, w, v} X F) (i : ℕ) :
    S.zariskiPullbackClass.{u, w, v} Y
      ((((Over.map f).sheafPushforwardCocontinuous AddCommGrpCat.{max (u + 1) v}
        (S.zariskiTopology.over X) (S.zariskiTopology.over Y)).rightDerived i).obj F)

Stacks.Topology.LocallyQuasiCompactZariskiSituation.exists_zariski_properMorphisms_refinement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ZariskiProperRefinement.lean, line 312. The attribute's comment: “condition (0EZ8) of Situation 0EZ3: a quasi-compact covering is refined by a Zariski covering, then one proper arrow, then a Zariski covering”.

Stacks 0EZI, the refinement condition. Every quasi-compact covering of an object U of the site is refined in three stages: by a Zariski covering {V ⟶ U}, then over each V by a single proper arrow f : W ⟶ V which is itself a quasi-compact covering, and finally by a Zariski covering of W whose composites factor through the given covering. This is condition (0EZ8) of Situation 0EZ3 with the proper arrows as the class P, the quasi-compact topology as τ and the Zariski topology as τ'.

theorem exists_zariski_properMorphisms_refinement
    (S : LocallyQuasiCompactZariskiSituation.{u, w} S₀ Bound)
    (U : S.category) (R : Presieve U) (hR : R ∈ S.qcSite.pretopology U) :
    ∃ T : Presieve U, T ∈ S.zariskiPrecoverage U ∧
      ∀ ⦃V : S.category⦄ (v : V ⟶ U), T v →
        ∃ (W : S.category) (f : W ⟶ V), S.properMorphisms f ∧
          Presieve.singleton f ∈ S.qcSite.pretopology V ∧
            ∃ P : Presieve W, P ∈ S.zariskiPrecoverage W ∧
              P.FactorsThruAlong R (f ≫ v)

Stacks.Topology.LocallyQuasiCompactZariskiSituation.isSheaf_qc_zariskiPullbackClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ZariskiPullbackClassQcSheaf.lean, line 94. The attribute's comment: “condition (3) of Situation 0EZ3 for this situation: every abelian sheaf on the localized Zariski site that is pulled back from the space satisfies the sheaf condition for quasi-compact coverings. This is the field ComparingTopologies.CohomologyComparison.weakSerre_isSheaf_fine, proved outright, with the sheaf on the space and the isomorphism to it taken from the essential image rather than from a choice. The five conditions of Situation 0EZ3 are items (1)-(5) of that tag; the (0EZ4)/(0EZ5)/(0EZ6)/(0EZ7) names used elsewhere in this directory are this development's own, and this is (0EZ6). ALL FIVE CONDITIONS ARE NOW PROVED for this situation, but SITUATION 0EZ3 IS STILL NOT INSTANTIATED HERE. CohomologyComparison is declared (C : Type u') [SmallCategory C] (ChangeOfTopology/ComparisonSituation.lean:117) and takes its coefficients in Ab.{u'}, so the carrier's universe fixes the coefficient universe. S.category is Type (u+1) with morphisms in Type u, so SmallCategory S.category does not synthesize and the carrier is CategoryTheory.SmallModel S.category, in Type u; EssentiallySmall.{u} S.category IS now an instance, LocallyQuasiCompactQcSite.category_essentiallySmall. The coefficients are therefore AddCommGrpCat.{u}, which is where this condition is proved and is why the carrier cannot be AsSmall.{v} S.category: that one would want AddCommGrpCat.{max (u+1) v}, where the germ model this condition is read off cannot even be stated. Condition (0EZ5) (zariskiPullbackClassOfSize_overMapPullback) is now stated for every AddCommGrpCat.{max u t} and so holds at AddCommGrpCat.{u}. WHAT BLOCKS THE BRIDGE is condition (0EZ7) (zariskiPullbackClass_rightDerived_overMapPushforward), still stated only at AddCommGrpCat.{max (u+1) v}. ONE of the seven inputs of its proof now reaches AddCommGrpCat.{u}: abelianComparisonInverseImage_exact, which was the one believed obstructed rather than merely unrestated and turns out not to need the slice's covering sieves at all. The next to move, preservesFiniteLimits_zariskiSlicePushforward, needs a lemma the library does not have -- Small.{max u t} (CostructuredArrow (Over.pullback f).op Z), the analogue of small_costructuredArrow_opensToSlice for Over.pullback f, without which (Over.pullback f).sheafPushforwardContinuous is not known to be a right adjoint at max u t. Past that the remaining five are a RESTATEMENT rather than new proper-base-change mathematics, made large only because the smallness and sheafification facts are supplied as INSTANCES, which cannot be generalized to max u t because max u ?t =?= max (u+1) v is not solvable by instance synthesis. See ZariskiHigherDirectImageClass.lean for the list. Transport of both precoverages and of the class along equivSmallModel is also not done”.

Stacks 0EZI. An abelian sheaf on the localized Zariski site over X which is pulled back from the space underlying X satisfies the sheaf condition for the quasi-compact topology over X.

theorem isSheaf_qc_zariskiPullbackClass
    (S : LocallyQuasiCompactZariskiSituation.{u, w} S₀ Bound) (X : S.category)
    (G : Sheaf (S.zariskiTopology.over X) AddCommGrpCat.{u})
    (hG : S.zariskiPullbackClassOfSize.{u, w, u} X G) :
    Presheaf.IsSheaf (S.qcSite.grothendieckTopology.over X) G.obj

Stacks.Topology.LocallyQuasiCompactZariskiSituation.zariskiPullbackClass_rightDerived_sliceDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ZariskiPullbackHigherDirectImage.lean, line 119. The attribute's comment: “condition (0EZ7) of Situation 0EZ3: higher direct images along a proper arrow stay in the class”.

Stacks 0EZI, the condition on higher direct images. Let f : X ⟶ Y be a proper arrow of the locally quasi-compact Zariski site and let G be an abelian sheaf on the localized Zariski site over X of the form π_X^{-1}G₀. Then for every i the higher direct image R^i f_{Zar,*}G is again of that form: it is π_Y^{-1} of the i-th higher direct image of G₀ along the continuous map underlying f.

This is condition (0EZ7) of Situation 0EZ3 for the data chosen by Stacks 0EZI — the proper arrows as the class P, the sheaves pulled back from the space as A'.

theorem zariskiPullbackClass_rightDerived_sliceDirectImage
    (S : LocallyQuasiCompactZariskiSituation.{u, w} S₀ Bound)
    ⦃X Y : S.category⦄ (f : X ⟶ Y) (hf : S.properMorphisms f)
    (G : Sheaf (S.zariskiTopology.over X) AddCommGrpCat.{max (u + 1) v})
    (hG : S.zariskiPullbackClass.{u, w, v} X G) (i : ℕ) :
    S.zariskiPullbackClass.{u, w, v} Y
      (((sliceDirectImage S f AddCommGrpCat.{max (u + 1) v}).rightDerived i).obj G)

Stacks.Topology.LocallyQuasiCompactZariskiSituation.zariskiPullbackClass_isSheaf_qc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ZariskiPullbackQcSheaf.lean, line 49. The attribute's comment: “condition (0EZ6) of Situation 0EZ3 for the sheaves pulled back from the space”.

An abelian sheaf on the localized Zariski site over X which is pulled back from the space X is already a sheaf for the quasi-compact topology: F' = ε_{X,*}ε_X^{-1}F'.

theorem zariskiPullbackClass_isSheaf_qc
    (S : LocallyQuasiCompactZariskiSituation.{u, w} S₀ Bound) (X : S.category)
    (F : Sheaf (S.zariskiTopology.over X) AddCommGrpCat.{max (u + 1) v})
    (hF : S.zariskiPullbackClass.{u, w, v} X F) :
    Presheaf.IsSheaf (S.qcSite.grothendieckTopology.over X) F.obj

Stacks.Topology.LocallyQuasiCompactZariskiSituation.zariskiPullbackClass_isWeakSerreClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ZariskiPullbackWeakSerre.lean, line 149. The attribute's comment: “the class A'_X of Situation 0EZ3 is a weak Serre class”.

Stacks 0EZI, the weak Serre condition on the class A'_X. Situation 0EZ3 requires the class it is handed over each object of the site to be a weak Serre subcategory of the abelian sheaves on the localized coarse site. For the choice Stacks 0EZI makes — the sheaves of the form π_X^{-1}F on the localized Zariski site — this holds because π_X^{-1} is exact and fully faithful and π_{X,*} is exact, all three being parts of Stacks 0DCU.

theorem zariskiPullbackClass_isWeakSerreClass
    (S : LocallyQuasiCompactZariskiSituation.{u, w} S₀ Bound) (X : S.category) :
    (S.zariskiPullbackClass.{u, w, v} X).IsWeakSerreClass

Stacks.Topology.LocallyQuasiCompactZariskiSituation.exists_zariskiRefinement_properMorphisms, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/ZariskiQcCoveringRefinement.lean, line 248. The attribute's comment: “condition (5) of Situation 0EZ3 for this situation: the three-stage refinement of a quasi-compact covering, by a Zariski covering, then one proper arrow over each member, then a Zariski covering of its source. This is the field ComparingTopologies.CohomologyComparison.covering_refinement, proved outright and carrying no hypothesis beyond the covering itself. The five conditions of Situation 0EZ3 are items (1)-(5) of that tag (0EZ7) names used elsewhere in this directory are this development's own. ALL FIVE ARE NOW PROVED for this situation, and Situation 0EZ3 is nevertheless still NOT instantiated here: condition (1) is morphismProperty_baseChange (ZariskiComparisonSituationData.lean), condition (2) is weakSerre_relocalizationInverseImage (same file), condition (3) is isSheaf_qc_zariskiPullbackClass (ZariskiPullbackClassQcSheaf.lean) and condition (4) is zariskiPullbackClass_rightDerived_overMapPushforward (ZariskiHigherDirectImageClass.lean). What is missing is one coefficient universe. The carrier of a CohomologyComparison has to be CategoryTheory.SmallModel S.category, S.category having morphisms in Type u and only EssentiallySmall.{u} LocallyQuasiCompactQcSite.category_essentiallySmall, so the small model and CategoryTheory.equivSmallModel are available coefficients at AddCommGrpCat.{u}. Conditions (1) and (5) are universe-free, (3) is proved there, and (2) now holds at every AddCommGrpCat.{max u t}, but (4) is stated only at AddCommGrpCat.{max (u+1) v} and every input of its proof carries that universe in its own statement, so it cannot be instantiated at u without generalizing the proper-base-change chain. Transporting the five conditions along equivSmallModel is also not done”.

Stacks 0EZI, the covering-refinement condition. Every quasi-compact covering R of an object U of the site is refined in three stages: a Zariski covering Q of U, then over each member v : V ⟶ U of Q a single proper arrow f : W ⟶ V which is itself a quasi-compact covering of V, and then a Zariski covering of W all of whose members factor through R along f ≫ v.

The quasi-compact coverings are stated as membership in the underlying precoverage of the site's chosen pretopology, which is the same condition.

theorem exists_zariskiRefinement_properMorphisms
    (U : S.category) (R : Presieve U) (hR : R ∈ S.qcSite.pretopology.toPrecoverage U) :
    ∃ Q : Presieve U, Q ∈ S.zariskiPrecoverage U ∧
      ∀ ⦃V : S.category⦄ (v : V ⟶ U), Q v →
        ∃ (W : S.category) (f : W ⟶ V), S.properMorphisms f ∧
          Presieve.singleton f ∈ S.qcSite.pretopology.toPrecoverage V ∧
          ∃ T : Presieve W, T ∈ S.zariskiPrecoverage W ∧ T.FactorsThruAlong R (f ≫ v)

Tag 0DCY, a lemma

Tag 0DCY in the Stacks Project.

Stacks.Topology.LocallyQuasiCompactZariskiSituation.qcAbelianDirectImageTopologicalInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcAbelianComparison.lean, line 376. The attribute's comment: “clause (1), the identification eps_{X,*}a_X^{-1}F = pi_X^{-1}F. PROVED, from condition (0EZ6) of Situation 0EZ3 for this situation, carried as h0EZI: that condition is one of the clauses of Tag 0EZI absent from this repository (see LocallyQuasiCompact/ ZariskiComparisonSituationData.lean:52). The sheaves-of-sets version of (0EZ6) IS proved, as isSheaf_qc_comparisonInverseImage (LocallyQuasiCompact/QcComparisonNaturality.lean:357, which carries no tag of its own; the tagged 09X3 carriers are isSheaf_qc_germSectionsPresheaf and isIso_toSheafify_comparisonInverseImage, both in LocallyQuasiCompact/QcGermSectionsSheaf.lean), but only at coefficients Type u, which is why the abelian form is carried”.

Stacks 0DCY (1), the identification ε_{X,*}(a_X^{-1}F) = π_X^{-1}F. For an object X of the site and an abelian sheaf F on the space underlying X, the change-of-topology direct image of a_X^{-1}F is π_X^{-1}F.

The hypothesis h0EZI is condition (0EZ6) of Situation 0EZ3 for this situation, one of the five conditions asserted by Stacks 0EZI: a sheaf pulled back from the space already satisfies the sheaf condition for quasi-compact coverings. Granted it, the unit of the change-of-topology adjunction is invertible at π_X^{-1}F, which is the assertion.

def qcAbelianDirectImageTopologicalInverseImageIso
    (h0EZI : ∀ G : Sheaf (S.zariskiTopology.over X) AddCommGrpCat.{max (u + 1) v},
      S.zariskiPullbackClass.{u, w, v} X G →
        Presheaf.IsSheaf (S.qcSite.grothendieckTopology.over X) G.obj)
    (F : Sheaf (Opens.grothendieckTopology X.obj) AddCommGrpCat.{max (u + 1) v}) :
    (qcAbelianDirectImage.{u, w, v} S X).obj
        ((qcTopologicalAbelianInverseImage.{u, w, v} S X).obj F) ≅
      (S.abelianComparisonInverseImage.{u, w, max (u + 1) v} X).obj F

Stacks.Topology.LocallyQuasiCompactZariskiSituation.isZero_rightDerived_qcAbelianDirectImage_qcTopologicalInverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcAbelianComparison.lean, line 404. The attribute's comment: “clause (1), the vanishing R^i eps_{X,*}(a_X^{-1}F) = 0 for i > 0. NOT PROVED: it IS the vanishing condition (V_n) of Situation 0EZ3, carried as hV. The leading assertion of Tag 0EZF supplies that condition only granted SingleCoveringDescent -- see ChangeOfTopology/VanishingConditionAllDegrees.lean:117 -- and that descent statement is not proved anywhere. What IS proved here is only that pi_X^{-1}F lies in the class A'_X”.

Stacks 0DCY (1), the vanishing R^i ε_{X,*}(a_X^{-1}F) = 0 for i > 0.

The hypothesis hV is the family of vanishing conditions (V_n) of Situation 0EZ3 for this situation, stated for the class of sheaves pulled back from the space: it is the leading assertion of Stacks 0EZF, which this development does not prove — see Stacks.ComparingTopologies.CohomologyComparison.vanishingCondition_of_singleCoveringDescent, where it is reduced to a descent statement for a single covering arrow of the distinguished class. This clause is therefore carried, not proved; the content here is only that π_X^{-1}F belongs to the class.

theorem isZero_rightDerived_qcAbelianDirectImage_qcTopologicalInverseImage
    [EnoughInjectives
      (Sheaf (S.qcSite.grothendieckTopology.over X) AddCommGrpCat.{max (u + 1) v})]
    (hV : ∀ G : Sheaf (S.zariskiTopology.over X) AddCommGrpCat.{max (u + 1) v},
      S.zariskiPullbackClass.{u, w, v} X G → ∀ i : ℕ, 0 < i →
        IsZero (((qcAbelianDirectImage.{u, w, v} S X).rightDerived i).obj
          ((qcAbelianInverseImage.{u, w, v} S X).obj G)))
    (F : Sheaf (Opens.grothendieckTopology X.obj) AddCommGrpCat.{max (u + 1) v})
    (i : ℕ) (hi : 0 < i) :
    IsZero (((qcAbelianDirectImage.{u, w, v} S X).rightDerived i).obj
      ((qcTopologicalAbelianInverseImage.{u, w, v} S X).obj F))

Stacks.Topology.LocallyQuasiCompactZariskiSituation.isIso_qcAbelianComparisonAdjunction_unit_app_and_isZero_rightDerived, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcDerivedComparison.lean, line 74. The attribute's comment: “clause (1): ε_{X,*}a_X^{-1}F = π_X^{-1}F (the unit is an isomorphism) and R^i ε_{X,*}(a_X^{-1}F) = 0 for i > 0”.

Stacks 0DCY (1). For X in LC_qc and an abelian sheaf F on X, the change-of-topology unit π_X^{-1}F ⟶ ε_{X,*}ε_X^{-1}π_X^{-1}F = ε_{X,*}a_X^{-1}F is an isomorphism, that is ε_{X,*}a_X^{-1}F = π_X^{-1}F, and R^i ε_{X,*}(a_X^{-1}F) = 0 for i > 0.

theorem isIso_qcAbelianComparisonAdjunction_unit_app_and_isZero_rightDerived
    (S : LocallyQuasiCompactZariskiSituation.{u, w} S₀ Bound) (X : S.category)
    (F : Sheaf (Opens.grothendieckTopology X.obj) AddCommGrpCat.{max (u + 1) v}) :
    IsIso ((qcAbelianComparisonAdjunction.{u, w, v} S X).unit.app
        ((S.abelianComparisonInverseImage.{u, w, max (u + 1) v} X).obj F)) ∧
      ∀ i : ℕ, 0 < i → IsZero (((qcAbelianDirectImage.{u, w, v} S X).rightDerived i).obj
        ((qcTopologicalAbelianInverseImage.{u, w, v} S X).obj F))

Stacks.Topology.LocallyQuasiCompactZariskiSituation.qcTopologicalHigherDirectImageIsoOfProper, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcDerivedComparison.lean, line 90. The attribute's comment: “clause (2): a_Y^{-1}(R^i f_* F) = R^i f_{qc,*}(a_X^{-1}F) for proper f and every i”.

Stacks 0DCY (2). For a proper morphism f : X ⟶ Y of LC_qc and an abelian sheaf F on X, a_Y^{-1}(R^i f_*F) = R^i f_{qc,*}(a_X^{-1}F) for every i.

def qcTopologicalHigherDirectImageIsoOfProper
    (S : LocallyQuasiCompactZariskiSituation.{u, w} S₀ Bound) {X Y : S.category} (f : X ⟶ Y)
    (hf : S.properMorphisms f) (i : ℕ)
    (F : Sheaf (Opens.grothendieckTopology X.obj) AddCommGrpCat.{max (u + 1) v}) :
    (qcTopologicalAbelianInverseImage.{u, w, v} S Y).obj
        (((spaceDirectImage S f AddCommGrpCat.{max (u + 1) v}).rightDerived i).obj F) ≅
      ((qcAbelianSliceDirectImage.{u, w, v} S f).rightDerived i).obj
        ((qcTopologicalAbelianInverseImage.{u, w, v} S X).obj F)

Stacks.Topology.LocallyQuasiCompactZariskiSituation.isIso_qcDerivedComparisonUnit_app_abelianComparisonInverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcDerivedComparison.lean, line 165. The attribute's comment: “clause (3): π_X^{-1}K ⟶ Rε_{X,*}(a_X^{-1}K) is an isomorphism for K in D⁺(X)”.

Stacks 0DCY (3). For X in LC_qc and K in D⁺(X), the canonical map π_X^{-1}K ⟶ Rε_{X,*}(a_X^{-1}K) is an isomorphism.

theorem isIso_qcDerivedComparisonUnit_app_abelianComparisonInverseImage
    (S : LocallyQuasiCompactZariskiSituation.{u, w} S₀ Bound) (X : S.category)
    (K : DerivedCategory.Plus
      (Sheaf (Opens.grothendieckTopology X.obj) AddCommGrpCat.{max (u + 1) v})) :
    IsIso ((qcDerivedComparisonUnit.{u, w, v} S X).app
      ((S.abelianComparisonInverseImage.{u, w, max (u + 1) v} X).mapDerivedCategoryPlus.obj
        K))

Stacks.Topology.LocallyQuasiCompactZariskiSituation.isIso_qcTopologicalDerivedBaseChangeMap_app_of_proper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcDerivedComparison.lean, line 342. The attribute's comment: “clause (4): a_Y^{-1}(Rf_*K) = Rf_{qc,*}(a_X^{-1}K) for proper f and K in D⁺(X)”.

Stacks 0DCY (4). For a proper morphism f : X ⟶ Y of LC_qc and K in D⁺(X), the canonical map a_Y^{-1}(Rf_*K) ⟶ Rf_{qc,*}(a_X^{-1}K) is an isomorphism.

theorem isIso_qcTopologicalDerivedBaseChangeMap_app_of_proper
    (S : LocallyQuasiCompactZariskiSituation.{u, w} S₀ Bound) {X Y : S.category} (f : X ⟶ Y)
    (hf : S.properMorphisms f)
    (K : DerivedCategory.Plus
      (Sheaf (Opens.grothendieckTopology X.obj) AddCommGrpCat.{max (u + 1) v})) :
    IsIso ((qcTopologicalDerivedBaseChangeMap.{u, w, v} S f).app K)

Tag 0D91, a lemma

Tag 0D91 in the Stacks Project.

Stacks.Topology.LocallyQuasiCompactZariskiSituation.isIso_qcTopologicalDerivedUnit_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcCohomologicalDescent.lean, line 302. The attribute's comment: “cohomological descent for LC_qc: for X in LC_qc and K in D^+(X), the canonical map K -> Ra_{X,*}a_X^{-1}K is an isomorphism”.

Stacks 0D91: cohomological descent for the quasi-compact site. For X an object of LC_qc and K in D⁺(X) the canonical map K ⟶ Ra_{X,*}a_X^{-1}K is an isomorphism.

theorem isIso_qcTopologicalDerivedUnit_app
    (K : DerivedCategory.Plus
      (Sheaf (Opens.grothendieckTopology X.obj) AddCommGrpCat.{max (u + 1) v})) :
    IsIso ((qcTopologicalDerivedUnit.{u, w, v} S X).app K)

Tag 09X4, a lemma

Tag 09X4 in the Stacks Project.

Stacks.Topology.LocallyQuasiCompactZariskiSituation.qcCohomologyComparisonIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcCohomologyComparison.lean, line 303. The attribute's comment: “part (1): H^n(X, F) = H^n_qc(X, a_X^{-1}F) for an abelian sheaf F on X, naturally in F, with cohomology read as the right derived functors of global sections”.

Stacks 09X4 for abelian sheaves. For an object X of LC_qc and an abelian sheaf F on the space underlying X, the cohomology of the localized quasi-compact site with coefficients in a_X^{-1}F is the cohomology of the space with coefficients in F:

H^n_{qc}(X, a_X^{-1}F) ≅ H^n(X, F),

naturally in F.

def qcCohomologyComparisonIso (n : ℕ) :
    qcTopologicalAbelianInverseImage.{u, w, v} S X ⋙
        (qcGlobalSections.{u, w, v} S X).rightDerived n ≅
      (spaceGlobalSections.{u, w, v} S X).rightDerived n

Stacks.Topology.LocallyQuasiCompactZariskiSituation.constantSheafQcCohomologyComparisonIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcCohomologyComparison.lean, line 356. The attribute's comment: “the example: H^n(X, A) = H^n_qc(X, A) for an abelian group A, naturally in A”.

Stacks 09X4, the constant-sheaf example. For an abelian group A, the cohomology of the space X with coefficients in the constant sheaf on A is the cohomology of the localized quasi-compact site with coefficients in its constant sheaf on A:

H^n(X, A) ≅ H^n_{qc}(X, A),

naturally in A.

def constantSheafQcCohomologyComparisonIso (n : ℕ) :
    constantSheaf (Opens.grothendieckTopology X.obj) AddCommGrpCat.{max (u + 1) v} ⋙
        (spaceGlobalSections.{u, w, v} S X).rightDerived n ≅
      constantSheaf (S.qcSite.grothendieckTopology.over X) AddCommGrpCat.{max (u + 1) v} ⋙
        (qcGlobalSections.{u, w, v} S X).rightDerived n

Stacks.Topology.LocallyQuasiCompactZariskiSituation.qcHypercohomologyComparisonIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcCohomologyComparison.lean, line 437. The attribute's comment: “part (2): H^n(X, K) = H^n_qc(X, a_X^{-1}K) for K in D^+(X), naturally in K, with hypercohomology read as the cohomology of the right derived functor of global sections on D^+”.

Stacks 09X4 for bounded below complexes. For an object X of LC_qc and K in D⁺(X), the hypercohomology of the space with coefficients in K is the hypercohomology of the localized quasi-compact site with coefficients in a_X^{-1}K:

H^n(X, K) ≅ H^n_{qc}(X, a_X^{-1}K),

naturally in K.

def qcHypercohomologyComparisonIso (n : ℤ) :
    spaceHypercohomology.{u, w, v} S X n ≅
      (qcTopologicalAbelianInverseImage.{u, w, v} S X).mapDerivedCategoryPlus ⋙
        qcHypercohomology.{u, w, v} S X n

Sources

LeanStacks.Topology.LocallyQuasiCompactZariskiSituation.isContinuous_id_zariski_qc · Stacks.Topology.LocallyQuasiCompactZariskiSituation.qcComparisonMorphism · Stacks.Topology.LocallyQuasiCompactZariskiSituation.zariskiComparisonMorphism · Stacks.Topology.LocallyQuasiCompactZariskiSituation.qcTopologicalMorphism · IsQcCovering.of_isOpenEmbedding · IsQcCovering.of_iSup_eq_top · Stacks.Topology.LocallyQuasiCompactHausdorff.qcPretopology · Stacks.Topology.LocallyQuasiCompactHausdorff.qcTopology

Section21.32 Spectral sequences for Ext #

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

Tag 07AA, an example

Tag 07AA in the Stacks Project.

CochainComplex.exists_cohomologyExtSpectralSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/HomBicomplexSpectralSequences.lean, line 104. The attribute's comment: “cohomology_ext”.

Stacks Project, Tag 07AA, the hyper-Ext spectral sequence. Let C be an abelian category with enough injectives, let K^• be a bounded above complex of C and let F be an object of C. There is a cohomological spectral sequence, starting on page two, with E₂^{i,j} = Extⁱ(H⁻ʲ(K^•), F), abutting to Extⁱ⁺ʲ(K^•, F).

It is the spectral sequence of the total complex of the Hom bicomplex Hom_C(K⁻ᵖ, Iᑫ) filtered by the second coordinate, for I^• an injective resolution of F.

public theorem exists_cohomologyExtSpectralSequence (K : CochainComplex C ℤ)
    (hK : CochainComplex.minus C K) (F : C) :
    ∃ E : CohomologicalSpectralSequence AddCommGrpCat.{max u v} 2,
      (∀ i j : ℤ, Nonempty
        ((E.page 2).X (i, j) ≅
          AddCommGrpCat.of (Abelian.zExt (K.homology (-j)) F i))) ∧
      SpectralSequence.AbutsTo E (fun n ↦
        AddCommGrpCat.of
          (DerivedCategory.Ext (DerivedCategory.Q.obj K)
            ((DerivedCategory.singleFunctor C 0).obj F) n))

CochainComplex.exists_termwiseExtSpectralSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/HomBicomplexSpectralSequences.lean, line 143. The attribute's comment: “termwise_ext”.

Stacks Project, Tag 07AA, the termwise Ext spectral sequence. Let C be an abelian category with enough injectives, let K^• be a bounded above complex of C and let F be an object of C. There is a cohomological spectral sequence, starting on page one, with E₁^{i,j} = Extʲ(K⁻ⁱ, F), abutting to Extⁱ⁺ʲ(K^•, F).

It is the spectral sequence of the total complex of the Hom bicomplex Hom_C(K⁻ᵖ, Iᑫ) filtered by the first coordinate, for I^• an injective resolution of F.

public theorem exists_termwiseExtSpectralSequence (K : CochainComplex C ℤ)
    (hK : CochainComplex.minus C K) (F : C) :
    ∃ E : CohomologicalSpectralSequence AddCommGrpCat.{max u v} 1,
      (∀ i j : ℤ, Nonempty
        ((E.page 1).X (i, j) ≅ AddCommGrpCat.of (Abelian.zExt (K.X (-i)) F j))) ∧
      SpectralSequence.AbutsTo E (fun n ↦
        AddCommGrpCat.of
          (DerivedCategory.Ext (DerivedCategory.Q.obj K)
            ((DerivedCategory.singleFunctor C 0).obj F) n))

Sources

LeanCochainComplex.exists_cohomologyExtSpectralSequence · CochainComplex.exists_termwiseExtSpectralSequence

Section21.33 Cup product #

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

Tag 0FPK, a lemma

Tag 0FPK in the Stacks Project.

Stacks.Cohomology.CupProductAndDerivedPushforward.naiveCupProduct_relativeCupProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/CupProductAndDerivedPushforward.lean, line 298. The attribute's comment: “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.CupProductAndDerivedPushforwardOfToposHom.naiveCupProduct_relativeCupProduct”.

Stacks 0FPK, site-presented. For a morphism of ringed topoi f : (Sh(C), O_C) ⟶ (Sh(D), O_D) presented by a morphism of sites and unbounded cochain complexes K, M of O_C-modules, the hexagon
f_*K ⊗^L_{O_D} f_*M ───────────→ Rf_*K ⊗^L_{O_D} Rf_*M
        │                                 │
        ↓                                 ↓
Tot(f_*K ⊗_{O_D} f_*M)            Rf_*(K ⊗^L_{O_C} M)
        │                                 │
        ↓                                 ↓
f_*Tot(K ⊗_{O_C} M) ───────────→ Rf_*Tot(K ⊗_{O_C} M)
commutes in D(O_D). Its horizontal edges and its top right edge are the comparison f_* ⟶ Rf_*; the top left and bottom right edges are the canonical map from the derived tensor product to the ordinary total tensor complex of Stacks 06YU; the middle left edge is the naive cup product and the middle right edge is the relative cup product of Stacks 0B6C.

theorem naiveCupProduct_relativeCupProduct
    (K M : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ) :
    (canonicalDerivedTensorProduct Y.O).toTensor ((pushforwardComplex f).obj K)
          ((pushforwardComplex f).obj M) ≫
        DerivedCategory.Q.map (naiveCupProduct f hmos K M) ≫
        pushforwardComparisonQ f (HomologicalComplex.mapBifunctor K M
          (Stacks.SheafOfModules.Tensor.sheafTensor X.O) (ComplexShape.up ℤ)) =
      bifunctorMap (derivedTensorProductFunctor Y.O) (pushforwardComparisonQ f K)
            (pushforwardComparisonQ f M) ≫
        relativeCupProduct f hmos (DerivedCategory.Q.obj K) (DerivedCategory.Q.obj M) ≫
        (derivedPushforward f).map ((canonicalDerivedTensorProduct X.O).toTensor K M)

Stacks.Cohomology.CupProductAndDerivedPushforwardOfToposHom.naiveCupProduct_relativeCupProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/CupProductAndDerivedPushforwardOfToposHom.lean, line 279. The attribute's comment: “the whole tag, for an arbitrary morphism of ringed topoi in the two-field sense of Tag 01D3, part (2) (a morphism of the underlying topoi with its structure map, no functor between the underlying sites and no morphism-of-sites hypothesis), at RingedTopos.{u, u, u}, for all unbounded complexes K, M; the statement carries no hypothesis or class argument”.

Stacks 0FPK. For a morphism of ringed topoi f : (Sh(C), O_C) ⟶ (Sh(D), O_D) — a morphism of the underlying topoi together with the structure map, with no functor between the underlying sites — and unbounded cochain complexes K, M of O_C-modules, the hexagon
f_*K ⊗^L_{O_D} f_*M ───────────→ Rf_*K ⊗^L_{O_D} Rf_*M
        │                                 │
        ↓                                 ↓
Tot(f_*K ⊗_{O_D} f_*M)            Rf_*(K ⊗^L_{O_C} M)
        │                                 │
        ↓                                 ↓
f_*Tot(K ⊗_{O_C} M) ───────────→ Rf_*Tot(K ⊗_{O_C} M)
commutes in D(O_D). Its horizontal edges and its top right edge are the comparison f_* ⟶ Rf_*; the top left and bottom right edges are the canonical map from the derived tensor product to the ordinary total tensor complex of Stacks 06YU; the middle left edge is the naive cup product and the middle right edge is the relative cup product of Stacks 0B6C.

The statement has no hypothesis and no class argument of its own: instance search supplies every class argument of naiveCupProduct_relativeCupProduct_of_instances.

theorem naiveCupProduct_relativeCupProduct {X Y : RingedTopos.{u, u, u}} (f : RingedToposHom X Y)
    (K M : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ) :
    (canonicalDerivedTensorProduct Y.O).toTensor ((pushforwardComplex f).obj K)
          ((pushforwardComplex f).obj M) ≫
        DerivedCategory.Q.map (naiveCupProduct f K M) ≫
        pushforwardComparisonQ f (HomologicalComplex.mapBifunctor K M
          (Stacks.SheafOfModules.Tensor.sheafTensor.{u, u, u, u, u} X.O) (ComplexShape.up ℤ)) =
      bifunctorMap (derivedTensorProductFunctor Y.O) (pushforwardComparisonQ f K)
            (pushforwardComparisonQ f M) ≫
        relativeCupProduct f (DerivedCategory.Q.obj K) (DerivedCategory.Q.obj M) ≫
        (derivedPushforward f).map ((canonicalDerivedTensorProduct X.O).toTensor K M)

Tag 0FPL, a lemma

Tag 0FPL in the Stacks Project.

Stacks.Cohomology.RelativeCupProductOnRingedTopoi.relativeCupProduct_assoc_canonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/RelativeCupProductAssociativity.lean, line 212. The attribute's comment: “associativity of the relative cup product, unconditionally, over the canonical associativity constraints of the two derived tensor products (derivedAssociator, the associator of the monoidal structure of Tag 0FPT whose tensor product is the derived tensor product of Tag 06YU on the nose): their naturality is derivedAssociator_naturality and the associativity law of the comparison of Tag 07A4 for them, which the source's proof uses silently, is pullbackTensorComparisonAssociative”.

The relative cup product is associative: for all K, L, M in D(𝒪) the square
(Rf_*K ⊗' Rf_*L) ⊗' Rf_*M --→ Rf_*(K ⊗ L) ⊗' Rf_*M --→ Rf_*((K ⊗ L) ⊗ M)
          |                                                     |
          | a                                                   | Rf_*a
          ↓                                                     ↓
Rf_*K ⊗' (Rf_*L ⊗' Rf_*M) --→ Rf_*K ⊗' Rf_*(L ⊗ M) --→ Rf_*(K ⊗ (L ⊗ M))
commutes in D(𝒪'). The four unlabelled arrows are relative cup products in one or the other tensor factor; the two edges a are the canonical associativity constraints derivedAssociator of ⊗^L_{𝒪'} and ⊗^L_𝒪.

theorem relativeCupProduct_assoc_canonical (K L M : DerivedModules X.O) :
    (uncurriedDerivedTensor Y).map
          (relativeCupProduct f hmos K L ×ₘ 𝟙 ((derivedPushforward f).obj M)) ≫
        relativeCupProduct f hmos ((uncurriedDerivedTensor X).obj (K, L)) M ≫
          (derivedPushforward f).map (derivedAssociator X K L M).hom =
      (derivedAssociator Y ((derivedPushforward f).obj K) ((derivedPushforward f).obj L)
            ((derivedPushforward f).obj M)).hom ≫
        (uncurriedDerivedTensor Y).map
            (𝟙 ((derivedPushforward f).obj K) ×ₘ relativeCupProduct f hmos L M) ≫
          relativeCupProduct f hmos K ((uncurriedDerivedTensor X).obj (L, M))

Stacks.Cohomology.RelativeCupProductOfToposHom.relativeCupProduct_assoc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/RelativeCupProductAssociativityOfToposHom.lean, line 176. The attribute's comment: “the whole tag, for an arbitrary morphism of ringed topoi in the two-field sense of Tag 01D3, part (2) (a morphism of the underlying topoi with its structure map, no functor between the underlying sites and no morphism-of-sites hypothesis), at RingedTopos.{u, u, u}, for all K, L, M in D(𝒪); the edges a are the associativity constraints derivedAssociator of Tag 0FPT and the statement carries no hypothesis or class argument; the associativity law of the comparison of Tag 07A4, which the source's proof uses silently, is pullbackTensorComparisonAssociative”.

[Stacks, Tag 0FPL]. The relative cup product of [Stacks, Tag 0B6C] is associative. Let f : (Sh(C), 𝒪) ⟶ (Sh(C'), 𝒪') be a morphism of ringed topoi: a morphism of the underlying topoi together with the structure map. Then for all K, L, M in D(𝒪) the square
(Rf_*K ⊗' Rf_*L) ⊗' Rf_*M --→ Rf_*(K ⊗ L) ⊗' Rf_*M --→ Rf_*((K ⊗ L) ⊗ M)
          |                                                     |
          | a                                                   | Rf_*a
          ↓                                                     ↓
Rf_*K ⊗' (Rf_*L ⊗' Rf_*M) --→ Rf_*K ⊗' Rf_*(L ⊗ M) --→ Rf_*(K ⊗ (L ⊗ M))
commutes in D(𝒪'). The four unlabelled arrows are relative cup products in one or the other tensor factor; the two edges a are the associativity constraints derivedAssociator of ⊗^L_{𝒪'} and ⊗^L_𝒪, the associators of the monoidal structures of [Stacks, Tag 0FPT] whose tensor product is the derived tensor product of [Stacks, Tag 06YU] on the nose; they appear because the source draws its square with ⊗^L strictly associative.

The statement has no hypothesis and no class argument of its own. The associativity law of the comparison of [Stacks, Tag 07A4] that the source's proof uses silently is pullbackTensorComparisonAssociative, proved above.

theorem relativeCupProduct_assoc {X Y : RingedTopos.{u, u, u}} (f : RingedToposHom X Y)
    (K L M : DerivedModules X.O) :
    (uncurriedDerivedTensor Y).map
          (relativeCupProduct f K L ×ₘ 𝟙 ((derivedPushforward f).obj M)) ≫
        relativeCupProduct f ((uncurriedDerivedTensor X).obj (K, L)) M ≫
          (derivedPushforward f).map (derivedAssociator X K L M).hom =
      (derivedAssociator Y ((derivedPushforward f).obj K) ((derivedPushforward f).obj L)
            ((derivedPushforward f).obj M)).hom ≫
        (uncurriedDerivedTensor Y).map
            (𝟙 ((derivedPushforward f).obj K) ×ₘ relativeCupProduct f L M) ≫
          relativeCupProduct f K ((uncurriedDerivedTensor X).obj (L, M))

Stacks.Cohomology.RelativeCupProductOnRingedTopoi.relativeCupProduct_assoc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/RelativeCupProductCoherence.lean, line 387. The attribute's comment: “associativity of the relative cup product, with the associativity constraints of the two derived tensor products supplied as data and their naturality and the monoidality of the comparison of Tag 07A4 for them carried as explicit hypotheses: this development has neither the symmetric monoidal structure of Tag 0FPT assembled nor that monoidality”.

[Stacks, Tag 0FPL]. The relative cup product of [Stacks, Tag 0B6C] is associative: for K, L, M in D(𝒪) the square
(Rf_*K ⊗' Rf_*L) ⊗' Rf_*M --→ Rf_*(K ⊗ L) ⊗' Rf_*M --→ Rf_*((K ⊗ L) ⊗ M)
          |                                                     ↑
          ↓                                                     |
Rf_*K ⊗' (Rf_*L ⊗' Rf_*M) --→ Rf_*K ⊗' Rf_*(L ⊗ M) --→ Rf_*(K ⊗ (L ⊗ M))
commutes in D(𝒪'). The upper route contracts K ⊗ L first, the lower route contracts L ⊗ M first; the two are different composites.

The source draws the square with ⊗^L strictly associative, so the associativity constraints are explicit here: aY is the one for ⊗^L_{𝒪'} and aX the one for ⊗^L_𝒪. The hypotheses beyond the source are haX, the naturality of aX, and hcomp, the compatibility of the comparison of [Stacks, Tag 07A4] with the two constraints — i.e. that Lf^* is a monoidal functor for it. The source gets both from the symmetric monoidal structure of [Stacks, Tag 0FPT], which this development does not assemble.

theorem relativeCupProduct_assoc
    (aY : ∀ P Q S : DerivedModules Y.O,
      (uncurriedDerivedTensor Y).obj ((uncurriedDerivedTensor Y).obj (P, Q), S) ⟶
        (uncurriedDerivedTensor Y).obj (P, (uncurriedDerivedTensor Y).obj (Q, S)))
    (aX : ∀ U V W : DerivedModules X.O,
      (uncurriedDerivedTensor X).obj ((uncurriedDerivedTensor X).obj (U, V), W) ≅
        (uncurriedDerivedTensor X).obj (U, (uncurriedDerivedTensor X).obj (V, W)))
    (haX : ∀ {U U' V V' W W' : DerivedModules X.O} (u : U ⟶ U') (v : V ⟶ V') (w : W ⟶ W'),
      (aX U V W).hom ≫
          (uncurriedDerivedTensor X).map (u ×ₘ (uncurriedDerivedTensor X).map (v ×ₘ w)) =
        (uncurriedDerivedTensor X).map ((uncurriedDerivedTensor X).map (u ×ₘ v) ×ₘ w) ≫
          (aX U' V' W').hom)
    (hcomp : ∀ P Q S : DerivedModules Y.O,
      (Stacks.Sheaves.DerivedPullback.derivedPullbackTensorIso f hmos).hom.app
            ((uncurriedDerivedTensor Y).obj (P, Q), S) ≫
          (uncurriedDerivedTensor X).map
            ((Stacks.Sheaves.DerivedPullback.derivedPullbackTensorIso f hmos).hom.app (P, Q) ×ₘ
              𝟙 ((derivedPullback f).obj S)) ≫
          (aX ((derivedPullback f).obj P) ((derivedPullback f).obj Q)
            ((derivedPullback f).obj S)).hom =
        (derivedPullback f).map (aY P Q S) ≫
          (Stacks.Sheaves.DerivedPullback.derivedPullbackTensorIso f hmos).hom.app
            (P, (uncurriedDerivedTensor Y).obj (Q, S)) ≫
          (uncurriedDerivedTensor X).map (𝟙 ((derivedPullback f).obj P) ×ₘ
            (Stacks.Sheaves.DerivedPullback.derivedPullbackTensorIso f hmos).hom.app (Q, S)))
    (K L M : DerivedModules X.O) :
    (uncurriedDerivedTensor Y).map
          (relativeCupProduct f hmos K L ×ₘ 𝟙 ((derivedPushforward f).obj M)) ≫
        relativeCupProduct f hmos ((uncurriedDerivedTensor X).obj (K, L)) M =
      aY ((derivedPushforward f).obj K) ((derivedPushforward f).obj L)
            ((derivedPushforward f).obj M) ≫
        (uncurriedDerivedTensor Y).map
            (𝟙 ((derivedPushforward f).obj K) ×ₘ relativeCupProduct f hmos L M) ≫
          relativeCupProduct f hmos K ((uncurriedDerivedTensor X).obj (L, M)) ≫
            (derivedPushforward f).map (aX K L M).inv

Tag 0FPM, a lemma

Tag 0FPM in the Stacks Project.

Stacks.Cohomology.RelativeCupProductOnRingedTopoi.relativeCupProduct_braiding_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/RelativeCupProductBraiding.lean, line 238. The attribute's comment: “the whole tag, unconditionally: for a morphism of ringed topoi and all K, L in D(𝒪), the commutativity square of the relative cup product commutes. ψ on both edges is the genuine commutativity constraint of Tag 0FPT (canonicalBraidingHom, the braiding of canonicalDerivedSymmetric, whose tensor product is the derived tensor product of Tag 06YU on the nose) rather than a symmetry supplied as data, and its naturality is proved rather than assumed. The one-time hypothesis PullbackTensorComparisonBraided -- that the comparison of Tag 07A4 is braided, i.e. that Lf^* is a braided and not merely a monoidal functor -- is now proved too, as pullbackTensorComparisonBraided, by descent along Tag 06YS from a pair of K-flat complexes with flat terms through the braided clause of Tag 03EL on modules”.

[Stacks, Tag 0FPM]. The relative cup product of [Stacks, Tag 0B6C] is commutative: for a morphism of ringed topoi f : (Sh(C), 𝒪) ⟶ (Sh(C'), 𝒪') and all K, L in D(𝒪) the square
Rf_*K ⊗^L_{𝒪'} Rf_*L --cup--→ Rf_*(K ⊗^L_𝒪 L)
        | ψ                          | Rf_*ψ
        ↓                            ↓
Rf_*L ⊗^L_{𝒪'} Rf_*K --cup--→ Rf_*(L ⊗^L_𝒪 K)
commutes in D(𝒪'). The horizontal arrows are the relative cup product, the left edge is ψ at (Rf_*K, Rf_*L) and the right edge is Rf_* applied to ψ at (K, L), exactly as the source draws them. ψ is the commutativity constraint of [Stacks, Tag 0FPT], Stacks.SheafOfModules.DerivedMonoidal.canonicalBraidingHom, on each of the two derived categories — not a symmetry supplied as data — and no hypothesis is placed on K or L.

Nothing is assumed. The braidedness of the comparison of [Stacks, Tag 07A4], which is the whole content of the tag, is pullbackTensorComparisonBraided above.

theorem relativeCupProduct_braiding_unconditional (K L : DerivedModules X.O) :
    relativeCupProduct f hmos K L ≫
        (derivedPushforward f).map (canonicalBraidingHom X.O K L) =
      canonicalBraidingHom Y.O ((derivedPushforward f).obj K) ((derivedPushforward f).obj L) ≫
        relativeCupProduct f hmos L K

Stacks.Cohomology.RelativeCupProductOfToposHom.relativeCupProduct_braiding, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/RelativeCupProductBraidingOfToposHom.lean, line 182. The attribute's comment: “the whole tag, for an arbitrary morphism of ringed topoi in the two-field sense of Tag 01D3, part (2) (a morphism of the underlying topoi with its structure map, no functor between the underlying sites and no morphism-of-sites hypothesis), at RingedTopos.{u, u, u}, for all K, L in D(𝒪); ψ on both edges is the commutativity constraint of Tag 0FPT and the statement carries no hypothesis or class argument”.

[Stacks, Tag 0FPM]. The relative cup product of [Stacks, Tag 0B6C] is commutative. Let f : (Sh(C), 𝒪) ⟶ (Sh(C'), 𝒪') be a morphism of ringed topoi: a morphism of the underlying topoi together with the structure map. Then for all K, L in D(𝒪) the square
Rf_*K ⊗^L_{𝒪'} Rf_*L --cup--→ Rf_*(K ⊗^L_𝒪 L)
        | ψ                          | Rf_*ψ
        ↓                            ↓
Rf_*L ⊗^L_{𝒪'} Rf_*K --cup--→ Rf_*(L ⊗^L_𝒪 K)
commutes in D(𝒪'). The horizontal arrows are the relative cup product. The left edge is ψ at (Rf_*K, Rf_*L) and the right edge is Rf_* applied to ψ at (K, L), as the source draws them. ψ is the commutativity constraint of [Stacks, Tag 0FPT] on each of the two derived categories.

The statement has no hypothesis and no class argument of its own.

theorem relativeCupProduct_braiding {X Y : RingedTopos.{u, u, u}} (f : RingedToposHom X Y)
    (K L : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
    relativeCupProduct f K L ≫ (derivedPushforward f).map (canonicalBraidingHom X.O K L) =
      canonicalBraidingHom Y.O ((derivedPushforward f).obj K) ((derivedPushforward f).obj L) ≫
        relativeCupProduct f L K

Stacks.Cohomology.RelativeCupProductOnRingedTopoi.relativeCupProduct_braiding, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/RelativeCupProductCoherence.lean, line 449. The attribute's comment: “commutativity of the relative cup product, with the commutativity constraints of the two derived tensor products supplied as data and their naturality and the compatibility of the comparison of Tag 07A4 with them carried as explicit hypotheses: this development has neither the symmetric monoidal structure of Tag 0FPT assembled nor that compatibility”.

[Stacks, Tag 0FPM]. The relative cup product of [Stacks, Tag 0B6C] is commutative: for K, L in D(𝒪) the square
Rf_*K ⊗' Rf_*L --cup--→ Rf_*(K ⊗ L)
      | ψ                     | Rf_*ψ
      ↓                       ↓
Rf_*L ⊗' Rf_*K --cup--→ Rf_*(L ⊗ K)
commutes in D(𝒪'). The left edge is the commutativity constraint sY of ⊗^L_{𝒪'} at the pair (Rf_*K, Rf_*L); the right edge is Rf_* applied to the commutativity constraint sX of ⊗^L_𝒪 at (K, L). These are the source's ψ and Rf_*ψ, and they are different maps.

The constraint of [Stacks, Tag 0FPT] is supplied as data on each side, because this development has it only one pair of objects at a time and not as part of an assembled monoidal structure (Stacks.DerivedTensor.RingedSite.DerivedTensorProduct.braidingIso). The hypotheses beyond the source are hsX, its naturality, and hcomp, the compatibility of the comparison of [Stacks, Tag 07A4] with the two constraints — i.e. that Lf^* is a braided functor for it.

theorem relativeCupProduct_braiding
    (sY : ∀ P Q : DerivedModules Y.O,
      (uncurriedDerivedTensor Y).obj (P, Q) ⟶ (uncurriedDerivedTensor Y).obj (Q, P))
    (sX : ∀ U V : DerivedModules X.O,
      (uncurriedDerivedTensor X).obj (U, V) ⟶ (uncurriedDerivedTensor X).obj (V, U))
    (hsX : ∀ {U U' V V' : DerivedModules X.O} (u : U ⟶ U') (v : V ⟶ V'),
      (uncurriedDerivedTensor X).map (u ×ₘ v) ≫ sX U' V' =
        sX U V ≫ (uncurriedDerivedTensor X).map (v ×ₘ u))
    (hcomp : ∀ P Q : DerivedModules Y.O,
      (derivedPullback f).map (sY P Q) ≫
          (Stacks.Sheaves.DerivedPullback.derivedPullbackTensorIso f hmos).hom.app (Q, P) =
        (Stacks.Sheaves.DerivedPullback.derivedPullbackTensorIso f hmos).hom.app (P, Q) ≫
          sX ((derivedPullback f).obj P) ((derivedPullback f).obj Q))
    (K L : DerivedModules X.O) :
    relativeCupProduct f hmos K L ≫ (derivedPushforward f).map (sX K L) =
      sY ((derivedPushforward f).obj K) ((derivedPushforward f).obj L) ≫
        relativeCupProduct f hmos L K

Tag 0FPN, a lemma

Tag 0FPN in the Stacks Project.

Stacks.Cohomology.RelativeCupProductOnRingedTopoi.relativeCupProduct_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/RelativeCupProductCoherence.lean, line 545. The attribute's comment: “compatibility of the relative cup product with composition, with R(f' ∘ f)_ realized as the composite Rf_ ⋙ Rf'_* and its adjunction the composite adjunction of Tag 0DV0 (the source's equality edge), and the comparison of Tag 07A4 for the composite taken to be the composite of the two comparisons, for every pair of composable morphisms of sites”.

[Stacks, Tag 0FPN]. The relative cup product of [Stacks, Tag 0B6C] is compatible with composition: for f : (Sh(C), 𝒪) ⟶ (Sh(C'), 𝒪'), f' : (Sh(C'), 𝒪') ⟶ (Sh(C''), 𝒪'') and K, L in D(𝒪) the diagram
R(f'f)_*K ⊗'' R(f'f)_*L  ====  Rf'_*Rf_*K ⊗'' Rf'_*Rf_*L
        |                                  |
        ↓                                  ↓
R(f'f)_*(K ⊗ L)  ====  Rf'_*Rf_*(K ⊗ L)  ←--  Rf'_*(Rf_*K ⊗' Rf_*L)
commutes in D(𝒪''): the cup product for the composite is the cup product for f' at (Rf_*K, Rf_*L) followed by Rf'_* of the cup product for f.

How the source's @{=} edges are handled. The source draws the two horizontal edges as equalities R(f' ∘ f)_* = Rf'_* ∘ Rf_*. In this development the two functors are not equal: they are isomorphic by Stacks.Cohomology.DerivedBaseChangePasting.derivedPushforwardCompIso. Accordingly R(f' ∘ f)_* is realized here as the composite Rf_* ⋙ Rf'_* with the composite adjunction L(f')^* ⋙ Lf^* ⊣ Rf_* ⋙ Rf'_* of CategoryTheory.Adjunction.comp, whose counit is the composition of the two counits — which is exactly the identification the source's proof appeals to ([Stacks, Tag 0DV0]). With that realization the two @{=} edges are identities and no isomorphism is absorbed silently. The comparison for the composite is correspondingly the composite comparison compComparison, the monoidal structure of the composite of two monoidal functors. The statement holds for every pair of composable morphisms of ringed topoi that are morphisms of sites.

Transporting this statement to relativeCupProduct (f'.comp f) — the cup product built from DerivedPullbackOnRingedTopoi.derivedAdjunction (f'.comp f) and Stacks.Sheaves.DerivedPullback.derivedPullbackTensorIso (f'.comp f) — would additionally require the compatibility of [Stacks, Tag 07A4] with composition of morphisms of ringed topoi, which this development does not have. The same gap is recorded on derivedBaseChangeMap_projectionFormulaMap_square in Stacks.Cohomology.ProjectionFormulaOnRingedTopoi.

theorem relativeCupProduct_comp (K L : DerivedModules X.O) :
    adjunctionCupProduct
        ((DerivedPullbackOnRingedTopoi.derivedAdjunction f' hmosf').comp
          (DerivedPullbackOnRingedTopoi.derivedAdjunction f hmosf))
        (uncurriedDerivedTensor Z) (uncurriedDerivedTensor X)
        (compComparison (uncurriedDerivedTensor X) (uncurriedDerivedTensor Y)
          (uncurriedDerivedTensor Z)
          (Stacks.Sheaves.DerivedPullback.derivedPullbackTensorIso f hmosf).hom
          (Stacks.Sheaves.DerivedPullback.derivedPullbackTensorIso f' hmosf').hom) K L =
      relativeCupProduct f' hmosf' ((derivedPushforward f).obj K)
            ((derivedPushforward f).obj L) ≫
        (derivedPushforward f').map (relativeCupProduct f hmosf K L)

Stacks.Cohomology.RelativeCupProductOfToposHom.relativeCupProduct_comp_pushforwardCompIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/RelativeCupProductCompositionOfToposHom.lean, line 136. The attribute's comment: “for morphisms of ringed topoi in the two-field sense of Tag 01D3, part (2) -- morphisms of the underlying topoi together with the structure maps, with no continuous functor between the underlying sites and no morphism-of-sites hypothesis; the left edge is the relative cup product of Tag 0B6C for f' ∘ f and the two equality edges of the source are the components of the composition isomorphism of derived pushforward, the conjugate of the Tag 0D6D isomorphism”.

[Stacks, Tag 0FPN]. Let f : (Sh(C), 𝒪) ⟶ (Sh(C'), 𝒪') and f' : (Sh(C'), 𝒪') ⟶ (Sh(C''), 𝒪'') be morphisms of ringed topoi. The relative cup product of [Stacks, Tag 0B6C] is compatible with composition: for all K, L in D(𝒪) the diagram
R(f'f)_*K ⊗'' R(f'f)_*L --c⊗c--→ Rf'_*Rf_*K ⊗'' Rf'_*Rf_*L
        |                                   |
        ↓ cup for f'∘f                      ↓ cup for f'
R(f'f)_*(K ⊗ L) --c--→ Rf'_*Rf_*(K ⊗ L) ←--Rf'_*(cup for f)-- Rf'_*(Rf_*K ⊗' Rf_*L)
commutes in D(𝒪''). The left edge is the relative cup product of the composite f' ∘ f; the two edges c the source draws as equalities R(f' ∘ f)_* = Rf'_*Rf_* are the components of the composition isomorphism derivedPushforwardCompIsoOfAdjoints, the conjugate of the isomorphism of [Stacks, Tag 0D6D] (conjugateEquiv_derivedPullbackCompIso_hom).

There is no hypothesis beyond the two morphisms of ringed topoi and the ambient instances making the derived categories and derived tensor products exist.

theorem relativeCupProduct_comp_pushforwardCompIso (K L : DerivedModules X.O) :
    relativeCupProduct (RingedToposHom.comp (X := X) f' f) K L ≫
        (derivedPushforwardCompIsoOfAdjoints f f').inv.app
          ((uncurriedDerivedTensor X).obj (K, L)) =
      (uncurriedDerivedTensor Z).map
          ((derivedPushforwardCompIsoOfAdjoints f f').inv.app K ×ₘ
            (derivedPushforwardCompIsoOfAdjoints f f').inv.app L) ≫
        relativeCupProduct f' ((derivedPushforward f).obj K) ((derivedPushforward f).obj L) ≫
          (derivedPushforward f').map (relativeCupProduct f K L)

Stacks.Cohomology.RelativeCupProductOnRingedTopoi.relativeCupProduct_comp_pushforwardCompIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/RelativeCupProductCompositionTransport.lean, line 160. The attribute's comment: “the square at the composite morphism itself, with no carried input: the left edge is the relative cup product of Tag 0B6C for f' ∘ f and the two equality edges of the source are the components of the composition isomorphism of derived pushforward, the conjugate of the Tag 0D6D isomorphism”.

For f : (Sh(C), 𝒪) ⟶ (Sh(C'), 𝒪'), f' : (Sh(C'), 𝒪') ⟶ (Sh(C''), 𝒪'') and K, L in D(𝒪) the diagram
R(f'f)_*K ⊗'' R(f'f)_*L --c⊗c--→ Rf'_*Rf_*K ⊗'' Rf'_*Rf_*L
        |                                   |
        ↓ cup for f'∘f                      ↓ cup for f'
R(f'f)_*(K ⊗ L) --c--→ Rf'_*Rf_*(K ⊗ L) ←--Rf'_*(cup for f)-- Rf'_*(Rf_*K ⊗' Rf_*L)
commutes in D(𝒪''). The left-hand vertical arrow is the relative cup product for the composite morphism f' ∘ f itself, and the two horizontal edges c are the components of the composition isomorphism derivedPushforwardCompIso.

theorem relativeCupProduct_comp_pushforwardCompIso (K L : DerivedModules X.O) :
    relativeCupProduct (f'.comp f)
          (RingedToposSiteHom.isMorphismOfSites_comp_u f f' hmosf hmosf') K L ≫
        (derivedPushforwardCompIso f f' hmosf hmosf').inv.app
          ((uncurriedDerivedTensor X).obj (K, L)) =
      (uncurriedDerivedTensor Z).map
          ((derivedPushforwardCompIso f f' hmosf hmosf').inv.app K ×ₘ
            (derivedPushforwardCompIso f f' hmosf hmosf').inv.app L) ≫
        relativeCupProduct f' hmosf' ((derivedPushforward f).obj K)
              ((derivedPushforward f).obj L) ≫
          (derivedPushforward f').map (relativeCupProduct f hmosf K L)

Tag 0H9A, a lemma

Tag 0H9A in the Stacks Project.

Stacks.Cohomology.RelativeCupProductOnRingedTopoi.relativeCupProduct_baseChange_square, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/RelativeCupProductBaseChangeOfToposHom.lean, line 103.

[Stacks, Tag 0H9A]. For a commutative square of morphisms of ringed topoi
                g'
  (Sh(C'), 𝒪_{C'}) --→ (Sh(C), 𝒪_C)
        |  f'                |  f
        v                    v
  (Sh(D'), 𝒪_{D'}) --→ (Sh(D), 𝒪_D)
                g
and arbitrary K, L in D(𝒪_C), the relative cup product of [Stacks, Tag 0B6C] is compatible with the square: the composite down the left (the comparison of [Stacks, Tag 07A4] for g, then the base change map of [Stacks, Tag 07A7] in each tensor factor) and along the bottom (the relative cup product for f') equals the composite along the top (Lg^* of the relative cup product for f) and down the right (the base change map, then R(f')_* of the comparison of [Stacks, Tag 07A4] for g'), as maps Lg^*(Rf_*K ⊗^L Rf_*L) ⟶ R(f')_*(L(g')^*K ⊗^L L(g')^*L) in D(𝒪_{D'}).

The four morphisms are morphisms of ringed topoi in the sense of Tag 01D3, part (2), and the only hypothesis on them is the commutativity h of the square. The relative cup product of Tag 0B6C is written out as adjunctionCupProduct of the derived adjunction of Tag 07A6 and the comparison of Tag 07A4.

theorem relativeCupProduct_baseChange_square
    (K L : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
    (Stacks.Sheaves.DerivedPullback.OfToposHom.derivedPullbackTensorIso g).hom.app
          ((Stacks.Cohomology.DerivedPushforward.derivedPushforward f).obj K,
            (Stacks.Cohomology.DerivedPushforward.derivedPushforward f).obj L) ≫
        (Functor.uncurry.obj (derivedTensorProductFunctor Y'.O)).map
            (Stacks.Cohomology.DerivedBaseChangeOfToposHom.derivedBaseChangeMap f g' f' g h K ×ₘ
              Stacks.Cohomology.DerivedBaseChangeOfToposHom.derivedBaseChangeMap f g' f' g h L) ≫
          adjunctionCupProduct (Stacks.Cohomology.DerivedPullbackOfToposHom.derivedAdjunction f')
            (Functor.uncurry.obj (derivedTensorProductFunctor Y'.O))
            (Functor.uncurry.obj (derivedTensorProductFunctor X'.O))
            (Stacks.Sheaves.DerivedPullback.OfToposHom.derivedPullbackTensorIso f').hom
            ((Stacks.Cohomology.DerivedPullbackOfToposHom.derivedPullback g').obj K)
            ((Stacks.Cohomology.DerivedPullbackOfToposHom.derivedPullback g').obj L) =
      (Stacks.Cohomology.DerivedPullbackOfToposHom.derivedPullback g).map
          (adjunctionCupProduct (Stacks.Cohomology.DerivedPullbackOfToposHom.derivedAdjunction f)
            (Functor.uncurry.obj (derivedTensorProductFunctor Y.O))
            (Functor.uncurry.obj (derivedTensorProductFunctor X.O))
            (Stacks.Sheaves.DerivedPullback.OfToposHom.derivedPullbackTensorIso f).hom K L) ≫
        Stacks.Cohomology.DerivedBaseChangeOfToposHom.derivedBaseChangeMap f g' f' g h
            (((derivedTensorProductFunctor X.O).obj K).obj L) ≫
          (Stacks.Cohomology.DerivedPushforward.derivedPushforward f').map
            ((Stacks.Sheaves.DerivedPullback.OfToposHom.derivedPullbackTensorIso g').hom.app
              (K, L))

Sources

LeanStacks.Cohomology.CupProductAndDerivedPushforward.naiveCupProduct_relativeCupProduct · Stacks.Cohomology.CupProductAndDerivedPushforwardOfToposHom.naiveCupProduct_relativeCupProduct · Stacks.Cohomology.RelativeCupProductOnRingedTopoi.relativeCupProduct_assoc_canonical · Stacks.Cohomology.RelativeCupProductOfToposHom.relativeCupProduct_assoc · Stacks.Cohomology.RelativeCupProductOnRingedTopoi.relativeCupProduct_assoc · Stacks.Cohomology.RelativeCupProductOnRingedTopoi.relativeCupProduct_braiding_unconditional · Stacks.Cohomology.RelativeCupProductOfToposHom.relativeCupProduct_braiding · Stacks.Cohomology.RelativeCupProductOnRingedTopoi.relativeCupProduct_braiding

Section21.34 Hom complexes #

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

Tag 0A8X, the section

Tag 0A8X in the Stacks Project.

AlgebraicGeometry.RingedSite.sheafHomComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/HomComplex.lean, line 931.

The canonical internal sheaf Hom complex SheafHom•(L, M): in degree n its sections over an object U are the degree-n cochains from L|_U to M|_U, that is the product over the pairs p + n = q of the sections of SheafHom(L^p, M^q), with the differential d(f) = d_M ∘ f - (-1)^n f ∘ d_L, together with its description on every slice site and the compatibility of these descriptions.

noncomputable def sheafHomComplex (X : RingedSite.{u, v, w})
    (L M : CochainComplex (SheafOfModules.{m} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ) :
        SheafHomComplex X L M

Tag 0A8Y, an equation

Tag 0A8Y in the Stacks Project.

AlgebraicGeometry.RingedSite.sheafHomComplexSectionHomologyEquivHomotopyCategory, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/HomComplex.lean, line 1045.

The n-th cohomology of the sections over U of the internal Hom complex from L to M is the group of morphisms L|_U ⟶ M|_U[n] in the homotopy category of O|_U-modules.

def sheafHomComplexSectionHomologyEquivHomotopyCategory
    (X : RingedSite.{u, u, u})
    (L M : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ)
    (U : X.C) (n : ℤ) :
    (sectionComplex X (sheafHomComplex X L M).obj U).homology n ≃+
    ((HomotopyCategory.quotient
          (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U))
          (ComplexShape.up ℤ)).obj
            (restrictComplex X L U) ⟶
        (HomotopyCategory.quotient
          (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U))
          (ComplexShape.up ℤ)).obj
            ((restrictComplex X M U)⟦n⟧))

Tag 0A8Z, an equation

Tag 0A8Z in the Stacks Project.

AlgebraicGeometry.RingedSite.sheafHomComplexHomologyEquivHomotopyCategory, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/HomComplex.lean, line 1023.

The n-th cohomology of the global sections of the internal sheaf Hom complex from L to M is canonically the group of morphisms from L to M[n] in the homotopy category.

noncomputable def sheafHomComplexHomologyEquivHomotopyCategory
    (X : RingedSite.{u, v, w})
    (L M : CochainComplex (SheafOfModules.{m} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ)
    (n : ℤ) :
    (globalSectionsComplex X (sheafHomComplex X L M).obj).homology n ≃+
      ((HomotopyCategory.quotient (SheafOfModules.{m} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
          (ComplexShape.up ℤ)).obj L ⟶
        (HomotopyCategory.quotient (SheafOfModules.{m} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
          (ComplexShape.up ℤ)).obj (M⟦n⟧))

Tag 0A90, a lemma

Tag 0A90 in the Stacks Project.

AlgebraicGeometry.RingedSite.sheafHomTensorIsoConstruction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/CurryingForComplexesOfModules.lean, line 153.

For complexes K, L, M of O-modules on a ringed site (C, O) there is an isomorphism SheafHom•(K, SheafHom•(L, M)) ≅ SheafHom•(Tot(K ⊗_O L), M) of complexes of O-modules, functorial in K, L and M.

def sheafHomTensorIsoConstruction : SheafHomTensorIsoConstruction X

AlgebraicGeometry.RingedSite.sheafHomTensorCurryIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/CurryingIsomorphism.lean, line 736. The attribute's comment: “the currying isomorphism”.

Stacks 0A90. The canonical currying isomorphism of internal Hom complexes on a ringed site: SheafHom(K, SheafHom(L, M)) ≅ SheafHom(Tot(K ⊗_O L), M).

def sheafHomTensorCurryIso :
    (sheafHomComplex X K (sheafHomComplex X L M).obj).obj ≅
      (sheafHomComplex X (((Stacks.SheafOfModules.Tensor.tensorComplex X.O).obj K).obj L) M).obj

Tag 0A91, a lemma

Tag 0A91 in the Stacks Project.

AlgebraicGeometry.RingedSite.compositionConstruction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/CompositionMorphism.lean, line 406.

Stacks 0A91. For complexes K, L, M of modules on a ringed site there is a canonical morphism of complexes of O-modules

Tot(SheafHom(L, M) ⊗_O SheafHom(K, L)) ⟶ SheafHom(K, M),

namely the one sending each homogeneous local pure tensor to the composite of its two factors, with no extra sign.

A ringed space is a ringed site, namely the site of its opens with the open-cover topology, so this also gives the composition morphism for complexes of modules on a ringed space.

noncomputable def compositionConstruction : CompositionConstruction X

Stacks.Cohomology.compositionConstruction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/MayerVietorisAndHom/HomComplexComposition.lean, line 601.

The canonical composition of internal Hom complexes of module sheaves.

noncomputable def compositionConstruction : CompositionConstruction X

Tag 0BYT, a lemma

Tag 0BYT in the Stacks Project.

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

Stacks 0BYT. For complexes K, L, M of modules on a ringed site there is a canonical morphism of complexes of O-modules

Tot(K ⊗_O SheafHom(M, L)) ⟶ SheafHom(M, Tot(K ⊗_O L)),

namely the one sending each homogeneous local pure tensor x ⊗ φ to the local section m ↦ x ⊗ φ(m).

noncomputable def tensorHomInterchangeConstruction : TensorHomInterchangeConstruction X

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

Stacks 0BYT. The interchange morphism is functorial in all three complexes at once: covariant in the tensor factor K and in the target L of the internal Hom, contravariant in its source M.

theorem tensorHomInterchange_natural (f : K ⟶ K') (g : L ⟶ L') (h : M' ⟶ M) :
    tensorHomInterchange X K L M ≫ homMap X h (tensorTotalMap X f g) =
      tensorTotalMap X f (homMap X h g) ≫ tensorHomInterchange X K' L' M'

Tag 0A93, a lemma

Tag 0A93 in the Stacks Project.

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

Stacks 0A93. For complexes K, L of modules on a ringed site there is a canonical morphism of complexes of O-modules

K ⟶ SheafHom(L, Tot(K ⊗_O L)),

namely the one sending each homogeneous local section k of K to the local section l ↦ k ⊗ l of the internal Hom complex.

noncomputable def diagonalConstruction : DiagonalConstruction X

AlgebraicGeometry.RingedSite.diagonalMap_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/DiagonalMorphism.lean, line 632. The attribute's comment: “functoriality in both complexes”.

Stacks 0A93. The diagonal morphism is natural in K and dinatural in L: a morphism g : L ⟶ L' acts covariantly inside the tensor product and contravariantly in the source of the internal Hom.

theorem diagonalMap_natural (f : K ⟶ K') (g : L ⟶ L') :
    diagonalMap X K L ≫ homMap X (𝟙 L) (tensorTotalMap X f g) =
      f ≫ diagonalMap X K' L' ≫ homMap X g (𝟙 (tensorTotal X K' L'))

Tag 0A92, a lemma

Tag 0A92 in the Stacks Project.

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

Stacks 0A92. For complexes K, L, M of modules on a ringed site there is a canonical morphism of complexes of O-modules

Tot(SheafHom(L, M) ⊗_O K) ⟶ SheafHom(SheafHom(K, L), M),

namely the one sending each homogeneous local pure tensor φ ⊗ k to the local section taking ψ to φ(ψ(k)), with the Koszul sign.

noncomputable def evaluationConstruction : EvaluationConstruction X

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

Stacks 0A92. The evaluation morphism is natural in K, contranatural in L and natural in M.

theorem evaluationMap_natural (k : K ⟶ K') (l : L' ⟶ L) (m : M ⟶ M') :
    tensorTotalMap X (homMap X l m) k ≫ evaluationMap X K' L' M' =
      evaluationMap X K L M ≫ homMap X (homMap X k l) m

Stacks.Cohomology.evaluationConstruction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/MayerVietorisAndHom/HomComplexEvaluation/EvaluationMorphism.lean, line 443. The attribute's comment: “canonical evaluation morphism”.

The canonical evaluation morphism for every three complexes of modules.

noncomputable def evaluationConstruction : EvaluationConstruction X

Stacks.Cohomology.evaluation_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/MayerVietorisAndHom/HomComplexEvaluation/EvaluationMorphism.lean, line 455. The attribute's comment: “functoriality in all three complexes”.

Evaluation is natural in K, contranatural in L, and natural in M.

theorem evaluation_natural
    {K K' L L' M M' : CochainComplex (SheafOfModules.{u}
        (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ}
    (k : K ⟶ K') (l : L' ⟶ L) (m : M ⟶ M') :
    tensorTotalMap X (sheafHomComplexMap X l m) k ≫
        evaluation X K' L' M' =
      evaluation X K L M ≫
        sheafHomComplexMap X (sheafHomComplexMap X k l) m

Tag 0A94, a lemma

Tag 0A94 in the Stacks Project.

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

Stacks 0A94, global sections, naturality. The identification of the degree-zero cohomology of the global sections of SheafHom(L, I) with Hom_{D(O)}(L, I) is natural in both variables: homMap k m, for k : L' ⟶ L and m : I ⟶ I', acts on it by precomposition with k and postcomposition with m in the derived category.

This is the global companion of AlgebraicGeometry.RingedSite.sheafHomSectionHomologyEquivDerivedCategoryHom_naturality, and it is what a consumer identifying two such bijections of morphism groups needs.

theorem sheafHomGlobalHomologyEquivDerivedCategoryHom_naturality
    {L L' I I' : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ}
    [I.IsKInjective] [I'.IsKInjective] (k : L' ⟶ L) (m : I ⟶ I')
    (η : (globalSectionsComplex X (sheafHomComplex X L I).obj).homology 0) :
    sheafHomGlobalHomologyEquivDerivedCategoryHom X L' I'
        (HomologicalComplex.homologyMap (globalSectionsComplexMap X (homMap X k m)) 0 η) =
      DerivedCategory.Q.map k ≫ sheafHomGlobalHomologyEquivDerivedCategoryHom X L I η ≫
        DerivedCategory.Q.map m

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

Stacks 0A94, sections over an object. If I is K-injective then the degree-zero cohomology of the sections over U of the internal Hom complex from L to I is the group of morphisms L|_U ⟶ I|_U in the derived category of O|_U-modules.

This is Stacks 0A8Y in degree 0 followed by the identification of homotopy-category with derived-category morphisms into a K-injective target; the restriction I|_U is K-injective by Stacks 08FI.

noncomputable def sheafHomSectionHomologyEquivDerivedCategoryHom
    (X : RingedSite.{u, u, u})
    (L I : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ)
    [I.IsKInjective] (U : X.C) :
    (sectionComplex X (sheafHomComplex X L I).obj U).homology 0 ≃+
      (DerivedCategory.Q.obj (restrictComplex X L U) ⟶
        DerivedCategory.Q.obj (restrictComplex X I U))

AlgebraicGeometry.RingedSite.sheafHomGlobalHomologyEquivDerivedCategoryHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/IntoAKInjectiveComplex.lean, line 204. The attribute's comment: “global sections”.

Stacks 0A94, global sections. If I is K-injective then the degree-zero cohomology of the global sections of the internal Hom complex from L to I is the group of morphisms L ⟶ I in the derived category of O-modules.

This is Stacks 0A8Z in degree 0 followed by the same identification of homotopy-category with derived-category morphisms into a K-injective target.

noncomputable def sheafHomGlobalHomologyEquivDerivedCategoryHom
    (X : RingedSite.{u, v, r})
    [HasSheafify X.J AddCommGrpCat.{max u v w}]
    [X.J.WEqualsLocallyBijective AddCommGrpCat.{max u v w}]
    (L I : CochainComplex
      (SheafOfModules.{max u v w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ)
    [I.IsKInjective] :
    (globalSectionsComplex X (sheafHomComplex X L I).obj).homology 0 ≃+
      (DerivedCategory.Q.obj L ⟶ DerivedCategory.Q.obj I)

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

Stacks 0A94, sections over an object, naturality. The identification of the degree-zero cohomology of the sections over U of SheafHom(L, I) with Hom_{D(O|_U)}(L|_U, I|_U) is natural in both variables: homMap k m, for k : L' ⟶ L and m : I ⟶ I', acts on it by precomposition with k|_U and postcomposition with m|_U in the derived category.

theorem sheafHomSectionHomologyEquivDerivedCategoryHom_naturality
    {L L' I I' : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ}
    [I.IsKInjective] [I'.IsKInjective] (k : L' ⟶ L) (m : I ⟶ I') (U : X.C)
    (η : (sectionComplex X (sheafHomComplex X L I).obj U).homology 0) :
    sheafHomSectionHomologyEquivDerivedCategoryHom X L' I' U
        (HomologicalComplex.homologyMap (sectionComplexMap X U (homMap X k m)) 0 η) =
      DerivedCategory.Q.map (restrictComplexMap X U k) ≫
        sheafHomSectionHomologyEquivDerivedCategoryHom X L I U η ≫
          DerivedCategory.Q.map (restrictComplexMap X U m)

Tag 0A95, a lemma

Tag 0A95 in the Stacks Project.

AlgebraicGeometry.RingedSite.homMap_quasiIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/QuasiIsoInvariance.lean, line 169.

Stacks 0A95. A quasi-isomorphism l : L' ⟶ L and a quasi-isomorphism i : I' ⟶ I between K-injective complexes of O-modules induce a quasi-isomorphism SheafHom(L, I') ⟶ SheafHom(L', I) of internal Hom complexes.

This is what makes the derived internal Hom well defined. The objects of the site need not lie in the universe of its morphisms; at c = u the extra size conditions above the tag's are automatic, which is AlgebraicGeometry.RingedSite.homMap_quasiIso_of_collapsed.

theorem homMap_quasiIso (i : I' ⟶ I) [QuasiIso i] [I'.IsKInjective] [I.IsKInjective]
    (l : L' ⟶ L) [QuasiIso l] : QuasiIso (homMap X l i)

Stacks.Cohomology.InternalHom.sheafHomComplexMap_quasiIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/MayerVietorisAndHom/HomComplexQuasiIso.lean, line 286.

Quasi-isomorphisms in both variables, with K-injective complexes in the second variable, induce a quasi-isomorphism of internal Hom complexes.

theorem sheafHomComplexMap_quasiIso
    (X : RingedSite.{u, u, u})
    {I' I L' L : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ}
    (i : I' ⟶ I) [QuasiIso i] [I'.IsKInjective] [I.IsKInjective]
    (l : L' ⟶ L) [QuasiIso l] :
    QuasiIso (sheafHomComplexMap X l i)

Tag 0A96, a lemma

Tag 0A96 in the Stacks Project.

AlgebraicGeometry.RingedSite.isKInjective_sheafHomComplex_of_isKFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/KFlatIntoKInjectiveIsKInjective.lean, line 68.

Stacks 0A96. The internal Hom complex SheafHom(L, I) from a K-flat complex L of O-modules into a K-injective complex I of O-modules is K-injective.

theorem isKInjective_sheafHomComplex_of_isKFlat
    (L I : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) ℤ)
    (hL : Stacks.SheafOfModules.IsKFlat X.O L) [I.IsKInjective] :
    (sheafHomComplex X L I).obj.IsKInjective

Sources

LeanAlgebraicGeometry.RingedSite.sheafHomComplex · AlgebraicGeometry.RingedSite.sheafHomComplexSectionHomologyEquivHomotopyCategory · AlgebraicGeometry.RingedSite.sheafHomComplexHomologyEquivHomotopyCategory · AlgebraicGeometry.RingedSite.sheafHomTensorIsoConstruction · AlgebraicGeometry.RingedSite.sheafHomTensorCurryIso · AlgebraicGeometry.RingedSite.compositionConstruction · Stacks.Cohomology.compositionConstruction · AlgebraicGeometry.RingedSite.tensorHomInterchangeConstruction

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

21.28 Formalities on… to 21.34 Hom complexes

Section21.28 Formalities on cohomological descent#

Tag 0D7Q, a lemma

Tag 0D7R, a lemma

Tag 0D7S, a lemma

Tag 0D7T, a lemma

Tag 0D7U, a lemma

Tag 0D7V, a lemma

Tag 0D7W, a lemma

Sources

Section21.29 Comparing two topologies, II#

Tag 07A8, a lemma

Tag 0F18, a lemma

Tag 0F19, a lemma

Sources

Section21.30 Comparing cohomology#

Tag 0EZ2, an equation

Tag 0EZ3, a situation

Tag 0EZ9, a lemma

Tag 0EZA, a lemma

Tag 0EZB, a lemma

Tag 0EZC, a lemma

Tag 0EZD, a lemma

Tag 0EZE, a lemma

Tag 0EZF, a lemma

Tag 0EZG, a lemma

Tag 0EZH, a lemma

Sources

Section21.31 Cohomology on Hausdorff and locally quasi-compact spaces#

Tag 09WY, the section

Tag 09WZ, a lemma

Tag 09X0, a definition

Tag 09X1, a lemma

Tag 09X5, a lemma

Tag 09X2, a remark

Tag 09X3, a lemma

Tag 0DCU, a lemma

Tag 0D92, a lemma

Tag 0EZI, a lemma

Tag 0DCY, a lemma

Tag 0D91, a lemma

Tag 09X4, a lemma

Sources

Section21.32 Spectral sequences for Ext#

Tag 07AA, an example

Sources

Section21.33 Cup product#

Tag 0FPK, a lemma

Tag 0FPL, a lemma

Tag 0FPM, a lemma

Tag 0FPN, a lemma

Tag 0H9A, a lemma

Sources

Section21.34 Hom complexes#

Tag 0A8X, the section

Tag 0A8Y, an equation

Tag 0A8Z, an equation

Tag 0A90, a lemma

Tag 0A91, a lemma

Tag 0BYT, a lemma

Tag 0A93, a lemma

Tag 0A92, a lemma

Tag 0A94, a lemma

Tag 0A95, a lemma

Tag 0A96, a lemma

Sources

Section21.28 Formalities on cohomological descent #

Section21.29 Comparing two topologies, II #

Section21.30 Comparing cohomology #

Section21.31 Cohomology on Hausdorff and locally quasi-compact spaces #

Section21.32 Spectral sequences for Ext #

Section21.33 Cup product #

Section21.34 Hom complexes #