85.33 Fppf hypercoverings of… to 85.36 Proper hypercoverings of…

Section85.33 Fppf hypercoverings of algebraic spaces#

Section 85.33 of the Stacks Project, Tag 0DH4. 6 tags here are carried by 8 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0DH5, a lemma

Tag 0DH5 in the Stacks Project.

Declarations registered for the tag:

Tag 0DH6, a lemma

Tag 0DH6 in the Stacks Project.

AlgebraicGeometry.Space.EtaleComponent.smallEtale_inverseImage_fullyFaithful, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SimplicialSpaces/FppfHypercoveringInverseImage.lean, line 420. The attribute's comment: “sheaves of sets”.

Stacks 0DH6, sheaves of sets. Let S be a scheme, X an algebraic space over S, and a : U → X an augmentation of a simplicial algebraic space over S which is an fppf hypercovering of X. Let a : Sh(U_étale) → Sh(X_étale) be the morphism of topoi of Section 0DE7, where X_étale is the small étale site of X (Stacks 03ED), its topos identified with that of X_spaces,étale by restriction along AlgebraicGeometry.Space.comparisonFunctor (Stacks 03G1, AlgebraicGeometry.Space.comparisonFunctor_sheafEquivalence). Then a⁻¹ : Sh(X_étale) ⥤ Sh(U_étale) is fully faithful, its essential image consists exactly of the cartesian sheaves, and a_* is a quasi-inverse: the unit of a⁻¹ ⊣ a_* is invertible, and so is its counit at every cartesian sheaf.

theorem smallEtale_inverseImage_fullyFaithful (hyp : IsFppfHypercovering A) :
    ((((comparisonFunctor B S hS A.right).sheafPushforwardContinuous
          (Type (u + 1))
          (SmallEtale.topology B S hS A.right.1)
          (SpacesEtale.topology B S hS A.right)).asEquivalence).inverse ⋙
        (etaleAugmentationMorphism A).inverseImage).Full ∧
      ((((comparisonFunctor B S hS A.right).sheafPushforwardContinuous
          (Type (u + 1))
          (SmallEtale.topology B S hS A.right.1)
          (SpacesEtale.topology B S hS A.right)).asEquivalence).inverse ⋙
        (etaleAugmentationMorphism A).inverseImage).Faithful ∧
      (∀ G, ((((comparisonFunctor B S hS A.right).sheafPushforwardContinuous
          (Type (u + 1))
          (SmallEtale.topology B S hS A.right.1)
          (SpacesEtale.topology B S hS A.right)).asEquivalence).inverse ⋙
          (etaleAugmentationMorphism A).inverseImage).essImage G ↔
        SimplicialSiteSituation.IsCartesianSheaf (etaleSimplicialSite A).situation G) ∧
      (∀ F, IsIso (((((comparisonFunctor B S hS A.right).sheafPushforwardContinuous
          (Type (u + 1))
          (SmallEtale.topology B S hS A.right.1)
          (SpacesEtale.topology B S hS A.right)).asEquivalence).symm.toAdjunction.comp
        (etaleAugmentationMorphism A).adj).unit.app F)) ∧
      (∀ G, SimplicialSiteSituation.IsCartesianSheaf (etaleSimplicialSite A).situation G →
        IsIso (((((comparisonFunctor B S hS A.right).sheafPushforwardContinuous
          (Type (u + 1))
          (SmallEtale.topology B S hS A.right.1)
          (SpacesEtale.topology B S hS A.right)).asEquivalence).symm.toAdjunction.comp
          (etaleAugmentationMorphism A).adj).counit.app G))

AlgebraicGeometry.Space.EtaleComponent.smallEtale_abelianInverseImage_fullyFaithful, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SimplicialSpaces/FppfHypercoveringInverseImage.lean, line 461. The attribute's comment: “sheaves of abelian groups”.

Stacks 0DH6, sheaves of abelian groups. Let S be a scheme, X an algebraic space over S, and a : U → X an augmentation of a simplicial algebraic space over S which is an fppf hypercovering of X. Let a : Sh(U_étale) → Sh(X_étale) be the morphism of topoi of Section 0DE7, where X_étale is the small étale site of X (Stacks 03ED), its category of abelian sheaves identified with that of X_spaces,étale by restriction along AlgebraicGeometry.Space.comparisonFunctor (Stacks 03G1, AlgebraicGeometry.Space.comparisonFunctor_sheafEquivalence). Then a⁻¹ : Ab(X_étale) ⥤ Ab(U_étale) is fully faithful, its essential image consists exactly of the cartesian abelian sheaves, and a_* is a quasi-inverse: the unit of a⁻¹ ⊣ a_* is invertible, and so is its counit at every cartesian abelian sheaf.

theorem smallEtale_abelianInverseImage_fullyFaithful (hyp : IsFppfHypercovering A) :
    ((((comparisonFunctor B S hS A.right).sheafPushforwardContinuous
          AddCommGrpCat.{u + 1}
          (SmallEtale.topology B S hS A.right.1)
          (SpacesEtale.topology B S hS A.right)).asEquivalence).inverse ⋙
        Sites.abelianInverseImage (etaleAugmentationMorphism A)).Full ∧
      ((((comparisonFunctor B S hS A.right).sheafPushforwardContinuous
          AddCommGrpCat.{u + 1}
          (SmallEtale.topology B S hS A.right.1)
          (SpacesEtale.topology B S hS A.right)).asEquivalence).inverse ⋙
        Sites.abelianInverseImage (etaleAugmentationMorphism A)).Faithful ∧
      (∀ G, ((((comparisonFunctor B S hS A.right).sheafPushforwardContinuous
          AddCommGrpCat.{u + 1}
          (SmallEtale.topology B S hS A.right.1)
          (SpacesEtale.topology B S hS A.right)).asEquivalence).inverse ⋙
          Sites.abelianInverseImage (etaleAugmentationMorphism A)).essImage G ↔
        SimplicialSiteSituation.IsCartesianAbSheaf (etaleSimplicialSite A).situation G) ∧
      (∀ F, IsIso (((((comparisonFunctor B S hS A.right).sheafPushforwardContinuous
          AddCommGrpCat.{u + 1}
          (SmallEtale.topology B S hS A.right.1)
          (SpacesEtale.topology B S hS A.right)).asEquivalence).symm.toAdjunction.comp
        (Stacks.Topos.AbelianPushforward.abelianInverseImageAdjPushforward
          (etaleSimplicialSite A).totalTopology (etaleAugmentationMorphism A))).unit.app F)) ∧
      (∀ G, SimplicialSiteSituation.IsCartesianAbSheaf (etaleSimplicialSite A).situation G →
        IsIso (((((comparisonFunctor B S hS A.right).sheafPushforwardContinuous
          AddCommGrpCat.{u + 1}
          (SmallEtale.topology B S hS A.right.1)
          (SpacesEtale.topology B S hS A.right)).asEquivalence).symm.toAdjunction.comp
          (Stacks.Topos.AbelianPushforward.abelianInverseImageAdjPushforward
            (etaleSimplicialSite A).totalTopology (etaleAugmentationMorphism A))).counit.app G))
Tag 0DH7, a lemma

Tag 0DH7 in the Stacks Project.

AlgebraicGeometry.Space.IsFppfHypercovering.isIso_smallEtaleDerivedUnit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SimplicialSpaces/FppfHypercoveringSmallEtaleDerived.lean, line 124.

Stacks 0DH7. Let S be a scheme, X an algebraic space over S, U a simplicial algebraic space over S and a : U → X an augmentation which is an fppf hypercovering of X. Then for every K ∈ D⁺(X_étale) the map K ⟶ Ra_*(a⁻¹K) is an isomorphism. Here a : Sh(U_étale) → Sh(X_étale) is the morphism of topoi of Section 0DE7, with X_étale the small étale site of X (Stacks 03ED) and its abelian sheaves identified with those of X_spaces,étale by the equivalence of Stacks 03G1, so that a⁻¹ ⊣ a_* is the composite of that equivalence with the adjunction of Section 0DE7; the map is the unit of the derived adjunction a⁻¹ ⊣ Ra_* on bounded below derived categories.

theorem IsFppfHypercovering.isIso_smallEtaleDerivedUnit (hA : IsFppfHypercovering A)
    (K : DerivedCategory.Plus
      (Sheaf (SmallEtale.topology B S hS A.right.1) AddCommGrpCat.{u + 1})) :
    IsIso ((Stacks.ComparingTopologies.derivedPlusAdjunction
      (((comparisonFunctor B S hS A.right).sheafPushforwardContinuous AddCommGrpCat.{u + 1}
        (SmallEtale.topology B S hS A.right.1)
        (SpacesEtale.topology B S hS A.right)).asEquivalence.symm.toAdjunction.comp
          (etaleAugmentationAbelianAdjunction A))).unit.app K)
Tag 0DH8, a lemma

Tag 0DH8 in the Stacks Project.

AlgebraicGeometry.Space.IsFppfHypercovering.smallEtaleDerivedGlobalSectionsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SimplicialSpaces/FppfHypercoveringSmallEtaleDerived.lean, line 193.

Stacks 0DH8. Let S be a scheme, X an algebraic space over S, U a simplicial algebraic space over S and a : U → X an augmentation which is an fppf hypercovering of X. Then RΓ(X_étale, K) = RΓ(U_étale, a⁻¹K) for K ∈ D⁺(X_étale), naturally in K. Here a : Sh(U_étale) → Sh(X_étale) is the morphism of topoi of Section 0DE7, with X_étale the small étale site of X (Stacks 03ED) and a⁻¹ as in IsFppfHypercovering.isIso_smallEtaleDerivedUnit. The isomorphism is the pullback on derived global sections: RΓ(X_étale, -) of the map K ⟶ Ra_*(a⁻¹K) of Stacks 0DH7 followed by the factorization RΓ(U_étale, -) = RΓ(X_étale, -) ∘ Ra_* of Stacks 08J6.

def IsFppfHypercovering.smallEtaleDerivedGlobalSectionsIso (hA : IsFppfHypercovering A) :
    (Sheaf.Γ (SmallEtale.topology B S hS A.right.1) AddCommGrpCat.{u + 1}).rightDerivedFunctorPlus ≅
      (((comparisonFunctor B S hS A.right).sheafPushforwardContinuous AddCommGrpCat.{u + 1}
        (SmallEtale.topology B S hS A.right.1)
        (SpacesEtale.topology B S hS A.right)).asEquivalence.symm.functor ⋙
          etaleAugmentationAbelianInverseImage A).mapDerivedCategoryPlus ⋙
        (Sheaf.Γ (etaleSimplicialSite A).totalTopology
          AddCommGrpCat.{u + 1}).rightDerivedFunctorPlus
Tag 0DH9, a lemma

Tag 0DH9 in the Stacks Project.

AlgebraicGeometry.Space.derivedPlusEquivalenceOfIsFppfHypercovering, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SimplicialSpaces/FppfHypercoveringDerivedEquivalence.lean, line 93.

Stacks Project, Tag 0DH9. Let S be a scheme, X an algebraic space over S, U a simplicial algebraic space over S and a : U → X an augmentation, and let 𝒜 ⊂ Ab(U_étale) be the weak Serre subcategory of cartesian abelian sheaves. If U is an fppf hypercovering of X, then a⁻¹ defines an equivalence

D⁺(X_étale) ⟶ D⁺_𝒜(U_étale)

with quasi-inverse Ra_*, where a : Sh(U_étale) → Sh(X_étale) is the morphism of topoi of Section 0DE7 and D⁺_𝒜(U_étale) consists of the bounded below complexes whose cohomology sheaves are cartesian. The functors are identified by AlgebraicGeometry.Space.derivedPlusEquivalenceOfIsFppfHypercovering_functor and AlgebraicGeometry.Space.derivedPlusEquivalenceOfIsFppfHypercovering_inverse.

The proof is the source's: the content of Stacks 0DH6 (every cartesian abelian sheaf on U_étale is a⁻¹ of an abelian sheaf on X_étale) and of Stacks 0DH7 (K ≅ Ra_*a⁻¹K on D⁺(X_étale)) are the inputs of the formal equivalence of Stacks 0D7U, CategoryTheory.SimplicialSiteSituation.Augmentation.derivedPlusInverseImageEquivalence.

def derivedPlusEquivalenceOfIsFppfHypercovering (hA : IsFppfHypercovering A) :
    DerivedCategory.Plus (Sheaf (SpacesEtale.topology B S hS A.right) AddCommGrpCat.{u + 1}) ≌
      (cartesianDerivedPlus (etaleSituation A)).FullSubcategory

AlgebraicGeometry.Space.derivedPlusEquivalenceOfIsFppfHypercovering_functor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SimplicialSpaces/FppfHypercoveringDerivedEquivalence.lean, line 104. The attribute's comment: “the equivalence is a⁻¹”.

The equivalence of Tag 0DH9 is a⁻¹: its forward functor, followed by the inclusion of D⁺_𝒜(U_étale) into D⁺(U_étale), is a⁻¹ : D⁺(X_étale) ⥤ D⁺(U_étale), the right derived functor of the exact functor a⁻¹.

theorem derivedPlusEquivalenceOfIsFppfHypercovering_functor (hA : IsFppfHypercovering A) :
    (derivedPlusEquivalenceOfIsFppfHypercovering hA).functor ⋙
        (cartesianDerivedPlus (etaleSituation A)).ι =
      (totalInverseImageAb (etaleSituation A) _ _ (etaleAugmentation A)).rightDerivedFunctorPlus

AlgebraicGeometry.Space.derivedPlusEquivalenceOfIsFppfHypercovering_inverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SimplicialSpaces/FppfHypercoveringDerivedEquivalence.lean, line 113. The attribute's comment: “the quasi-inverse is Ra_*”.

The quasi-inverse of the equivalence of Tag 0DH9 is Ra_*: its inverse functor is the inclusion of D⁺_𝒜(U_étale) into D⁺(U_étale) followed by Ra_* : D⁺(U_étale) ⥤ D⁺(X_étale).

theorem derivedPlusEquivalenceOfIsFppfHypercovering_inverse (hA : IsFppfHypercovering A) :
    (derivedPlusEquivalenceOfIsFppfHypercovering hA).inverse =
      (cartesianDerivedPlus (etaleSituation A)).ι ⋙
        (abelianTotalPushforward (etaleSituation A) _ _
          (etaleAugmentation A)).rightDerivedFunctorPlus
Tag 0DHA, a lemma

Tag 0DHA in the Stacks Project.

AlgebraicGeometry.Space.IsFppfHypercovering.etaleSpectralSequence_pageOne_abutsTo, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SimplicialSpaces/FppfHypercoveringEtaleSpectralSequence.lean, line 123.

Stacks Project, Tag 0DHA. Let S be a scheme, X an algebraic space over S, U a simplicial algebraic space over S and a : U → X an augmentation. Let 𝓕 be an abelian sheaf on X_étale and 𝓕_p its pullback to U_{p, étale}. If U is an fppf hypercovering of X, then the canonical spectral sequence etaleSpectralSequence A at 𝓕 has

E_1^{p,q} = H^q_ét(U_p, 𝓕_p)

(vanishing outside the first quadrant) and converges to H^{p+q}_ét(X, 𝓕).

Here X = A.right, U = A.left and a = A.hom, the étale sites are the spaces-étale sites of Section 0DE7, 𝓕_p is the abelian inverse image along the morphism of topoi of Stacks 03G2 induced by a_p : U_p → X, and H^n_ét is CategoryTheory.Sheaf.functorH; the first page is identified naturally in 𝓕 by AlgebraicGeometry.Space.etaleSpectralSequence_pageOneIso, and the abutment is zero in negative degrees.

theorem IsFppfHypercovering.etaleSpectralSequence_pageOne_abutsTo (hA : IsFppfHypercovering A)
    (F : Sheaf (SpacesEtale.topology B S hS A.right) AddCommGrpCat.{u + 1}) :
    (∀ p q : ℕ, Nonempty ((((etaleSpectralSequence A).obj F).page 1 le_rfl).X ((p : ℤ), (q : ℤ)) ≅
      (Sheaf.functorH.{u + 1, u + 1} (SpacesEtale.topology B S hS (A.left.obj (op ⦋p⦌))) q).obj
        ((Sites.abelianInverseImage (EtaleComponent.baseChangeMorphism (A := A) ⦋p⦌)).obj F))) ∧
    (∀ p q : ℤ, p < 0 ∨ q < 0 → IsZero ((((etaleSpectralSequence A).obj F).page 1 le_rfl).X
      (p, q))) ∧
    SpectralSequence.AbutsTo ((etaleSpectralSequence A).obj F)
      (fun n => if 0 ≤ n then Sheaf.functorH.{u + 1, u + 1}
          (SpacesEtale.topology B S hS A.right) n.toNat |>.obj F
        else AddCommGrpCat.of PUnit)
Sources
LeanAlgebraicGeometry.Space.SimplicialSpacesEtaleSite.bigFppfAugmentationSquareIso · AlgebraicGeometry.Space.EtaleComponent.smallEtale_inverseImage_fullyFaithful · AlgebraicGeometry.Space.EtaleComponent.smallEtale_abelianInverseImage_fullyFaithful · AlgebraicGeometry.Space.IsFppfHypercovering.isIso_smallEtaleDerivedUnit · AlgebraicGeometry.Space.IsFppfHypercovering.smallEtaleDerivedGlobalSectionsIso · AlgebraicGeometry.Space.derivedPlusEquivalenceOfIsFppfHypercovering · AlgebraicGeometry.Space.derivedPlusEquivalenceOfIsFppfHypercovering_functor · AlgebraicGeometry.Space.derivedPlusEquivalenceOfIsFppfHypercovering_inverse

Section85.34 Fppf hypercoverings of algebraic spaces: modules#

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

Tag 0DHC, a lemma

Tag 0DHC in the Stacks Project.

Declarations registered for the tag:

Tag 0DHD, a lemma

Tag 0DHD in the Stacks Project.

Declarations registered for the tag:

Tag 0DHE, a lemma

Tag 0DHE in the Stacks Project.

Declarations registered for the tag:

Tag 0DHF, a lemma

Tag 0DHF in the Stacks Project.

Declarations registered for the tag:

Tag 0DHG, a lemma

Tag 0DHG in the Stacks Project.

AlgebraicGeometry.Space.IsFppfHypercovering.isIso_derivedGlobalSectionsSemilinearMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SimplicialSpaces/FppfHypercoveringQuasicoherentCohomology.lean, line 164.

Stacks Project, Tag 0DHG. Let S be a scheme, X an algebraic space over S, U a simplicial algebraic space over S and a : U → X an augmentation. If a : U → X is an fppf hypercovering of X, then

RΓ(X_étale, K) = RΓ(U_étale, a^*K)

for K ∈ D_QCoh(𝒪_X), where a : (Sh(U_étale), 𝒪_U) → (Sh(X_étale), 𝒪_X) is the morphism of ringed topoi of Section 0DE7 (AlgebraicGeometry.Space.etaleAugmentationRingedHom) and a^* its derived pullback: the canonical map RΓ(X_étale, K) ⟶ RΓ(U_étale, a^*K) is an isomorphism.

Here RΓ(X_étale, -) and RΓ(U_étale, -) are the total right derived functors of global sections, with values in the derived categories of modules over coefficient rings R' and R mapping to Γ(X, 𝒪_X) and to Γ(U, 𝒪_U) through ψ' and ψ, compatibly (h) with ρ : R' → R and the map Γ(X, 𝒪_X) → Γ(U, 𝒪_U) of a; the right hand side is read in D(R') through restriction of scalars along ρ. For instance R = R' = ℤ. The canonical map (Stacks.Cohomology.LerayOfToposHom.derivedGlobalSectionsSemilinearMap) is RΓ(X_étale, -) of the derived unit K → Ra_*a^*K, invertible on D_QCoh(𝒪_X) by AlgebraicGeometry.Space.IsFppfHypercovering.isIso_derivedAdjunction_unit_app, followed by the identification RΓ(X_étale, -) ∘ Ra_* = RΓ(U_étale, -) of Cohomology on Sites, Remark 08J6.

theorem IsFppfHypercovering.isIso_derivedGlobalSectionsSemilinearMap (hA : IsFppfHypercovering A)
    {R : Type r} [Ring R] [HasDerivedCategory (ModuleCat.{u + 1} R)]
    {R' : Type r'} [Ring R'] [HasDerivedCategory (ModuleCat.{u + 1} R')]
    (ψ : R →+* RingCat.sectionsSubring ((Stacks.SheafOfModules.Tensor.ringSheaf
      (J := ((etaleSituation A).totalRingedTopos (etaleStructureSheaf A)).J))
        ((etaleSituation A).totalRingedTopos (etaleStructureSheaf A)).O).obj)
    (ψ' : R' →+* RingCat.sectionsSubring ((Stacks.SheafOfModules.Tensor.ringSheaf
      (J := (etaleRingedAugmentation A).augmentationRingedTopos.J))
        (etaleRingedAugmentation A).augmentationRingedTopos.O).obj)
    (ρ : R' →+* R)
    (h : (toposGlobalSectionsRingHom (etaleAugmentationRingedHom A)).comp ψ' = ψ.comp ρ)
    (K : @DerivedCategory (SheafOfModules.{u + 1}
      (Stacks.SheafOfModules.Tensor.ringSheaf (spacesEtaleRingedTopos B S hS A.right).O)) _ _
      (HasDerivedCategory.standard _))
    (hK : etaleQuasicoherentComplexes A K) :
    IsIso (derivedGlobalSectionsSemilinearMap.{u + 1, u + 1, u + 1, u + 1, u + 1, u + 1, r, r',
      _, _}
      (etaleAugmentationRingedHom A) ψ ψ' ρ h K)
Tag 0DHH, a lemma

Tag 0DHH in the Stacks Project.

AlgebraicGeometry.Space.SimplicialSpacesEtaleSite.moduleSpectralSequence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SimplicialModuleSpectralSequence.lean, line 84. The attribute's comment: “the spectral sequence”.

The spectral sequence of a module pulled back to a simplicial algebraic space a : U → X, as a functor of the 𝒪_X-module 𝓕: the spectral sequence of Stacks 0D7E for the pullback of 𝓕 to the total site of the strict components of U_{spaces, étale}.

def moduleSpectralSequence :
    SheafOfModules.{u + 1} (Stacks.SheafOfModules.Tensor.ringSheaf
        (spacesEtaleRingedTopos B S hS X).O) ⥤
      CohomologicalSpectralSequence AddCommGrpCat.{u + 1} 1

AlgebraicGeometry.Space.SimplicialSpacesEtaleSite.moduleSpectralSequencePageOneIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SimplicialModuleSpectralSequence.lean, line 124. The attribute's comment: “its first page E_1^{p,q} = H^q_ét(U_p, 𝓕_p)”.

E_1^{p,q} = H^q_ét(U_p, a_p^*𝓕), naturally in the 𝒪_X-module 𝓕, where a_p^* is the pullback of modules along the morphism of ringed topoi (Sh((U_p)_{spaces, étale}), 𝒪_{U_p}) ⟶ (Sh(X_{spaces, étale}), 𝒪_X) of a_p : U_p → X.

def moduleSpectralSequencePageOneIso (p q : ℕ) :
    moduleSpectralSequence a ⋙
        (CategoryTheory.SpectralSequence.pageFunctor AddCommGrpCat.{u + 1} _ 1 1 le_rfl ⋙
          HomologicalComplex.eval AddCommGrpCat.{u + 1} _ ((p : ℤ), (q : ℤ))) ≅
      (spacesEtaleRingedToposHom (Z₂ := X) (a.app (op ⦋p⦌))).toModulesHom.pullbackModules ⋙
        (spacesEtaleRingedTopos B S hS (U.obj (op ⦋p⦌))).moduleGlobalSections.rightDerived q

AlgebraicGeometry.Space.SimplicialSpacesEtaleSite.moduleSpectralSequence_abutsTo_of_isFppfHypercovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SimplicialQuasicoherentSpectralSequence.lean, line 94. The attribute's comment: “the spectral sequence converges to H^{p+q}_ét(X, 𝓕)”.

Stacks 0DHH. Let S be a scheme, X an algebraic space over S, U a simplicial algebraic space over S and a : U → X an augmentation which is an fppf hypercovering of X. Let 𝓕 be a quasi-coherent 𝒪_X-module and 𝓕_p = a_p^*𝓕 its pullback to U_{p, étale}. Then the spectral sequence moduleSpectralSequence, with first page E_1^{p,q} = H^q_ét(U_p, 𝓕_p) (moduleSpectralSequencePageOneIso), converges to H^{p+q}_ét(X, 𝓕). The algebraic spaces are those of a big fppf site T of algebraic spaces over S (Stacks 0DBV).

theorem moduleSpectralSequence_abutsTo_of_isFppfHypercovering
    {A : SimplicialObject.Augmented T.Spaces} (hA : IsFppfHypercovering A)
    (F : SheafOfModules.{u + 1} (Stacks.SheafOfModules.Tensor.ringSheaf
      (spacesEtaleRingedTopos T.schemeSite S T.scheme_mem A.right).O))
    [F.IsQuasicoherentOnSite] :
    CategoryTheory.SpectralSequence.AbutsTo ((moduleSpectralSequence A.hom).obj F)
      (fun n => if 0 ≤ n then
        ((spacesEtaleRingedTopos T.schemeSite S T.scheme_mem
            A.right).moduleGlobalSections.rightDerived n.toNat).obj F
        else AddCommGrpCat.of PUnit.{u + 2})
Sources
LeanAlgebraicGeometry.Space.SimplicialSpacesEtaleSite.bigFppfAugmentationSquareTwoIso · AlgebraicGeometry.Space.SimplicialSpacesEtaleSite.descent_quasicoherent_of_isHypercoveringAugmentation · AlgebraicGeometry.Space.SimplicialSpacesEtaleSite.isIso_unit_and_isZero_rightDerived_of_isHypercoveringAugmentation · AlgebraicGeometry.Space.SimplicialSpacesEtaleSite.isWeakSerreClass_and_derivedPullback_equivalence · AlgebraicGeometry.Space.IsFppfHypercovering.isIso_derivedGlobalSectionsSemilinearMap · AlgebraicGeometry.Space.SimplicialSpacesEtaleSite.moduleSpectralSequence · AlgebraicGeometry.Space.SimplicialSpacesEtaleSite.moduleSpectralSequencePageOneIso · AlgebraicGeometry.Space.SimplicialSpacesEtaleSite.moduleSpectralSequence_abutsTo_of_isFppfHypercovering

Section85.35 Fppf descent of complexes#

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

Tag 0DL9, a lemma

Tag 0DL9 in the Stacks Project.

AlgebraicGeometry.Space.SimplicialSpacesEtaleSite.negativeExt_eq_zero_and_exact_derivedPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SimplicialQuasicoherentDerivedHomDescent.lean, line 482.

Let a : U → X be an fppf hypercovering of an algebraic space and K, E objects of D_{QCoh}(𝒪_X) with Ext^i_{U_n}(La_n^*K, La_n^*E) = 0 for i < 0 and all n. Then (1) Ext^i_X(K, E) = 0 for i < 0, and (2) the sequence 0 ⟶ Hom_X(K, E) ⟶ Hom_{U_0}(La_0^*K, La_0^*E) ⟶ Hom_{U_1}(La_1^*K, La_1^*E) is exact, where the first map is La_0^* and the second the difference of the pullbacks along the two faces.

theorem negativeExt_eq_zero_and_exact_derivedPullback
    {K E : @DerivedCategory (SheafOfModules.{u + 1} (Stacks.SheafOfModules.Tensor.ringSheaf
      (spacesEtaleRingedTopos T.schemeSite S T.scheme_mem X).O)) _ _
      (HasDerivedCategory.standard _)}
    (hK : (@DerivedCategoryB.derivedCategoryB _ _ _ (HasDerivedCategory.standard _)
      (SheafOfModules.isQuasicoherentOnSite.{u + 1, u + 1, u + 1, u + 1}
        (Stacks.SheafOfModules.Tensor.ringSheaf
          (spacesEtaleRingedTopos T.schemeSite S T.scheme_mem X).O))) K)
    (hE : (@DerivedCategoryB.derivedCategoryB _ _ _ (HasDerivedCategory.standard _)
      (SheafOfModules.isQuasicoherentOnSite.{u + 1, u + 1, u + 1, u + 1}
        (Stacks.SheafOfModules.Tensor.ringSheaf
          (spacesEtaleRingedTopos T.schemeSite S T.scheme_mem X).O))) E)
    (hvan : ∀ (n : SimplexCategory) (i : ℤ), i < 0 →
      ∀ g : (derivedPullback
          (X := spacesEtaleRingedTopos T.schemeSite S T.scheme_mem (U.obj (op n)))
          (Y := spacesEtaleRingedTopos T.schemeSite S T.scheme_mem X)
          (spacesEtaleRingedToposHom (a.app (op n)))).obj K ⟶
        ((derivedPullback (X := spacesEtaleRingedTopos T.schemeSite S T.scheme_mem (U.obj (op n)))
          (Y := spacesEtaleRingedTopos T.schemeSite S T.scheme_mem X)
          (spacesEtaleRingedToposHom (a.app (op n)))).obj E)⟦i⟧, g = 0) :
    (∀ (i : ℤ), i < 0 → ∀ g : K ⟶ E⟦i⟧, g = 0) ∧
      Function.Injective (fun g : K ⟶ E ↦
        (derivedPullback (X := spacesEtaleRingedTopos T.schemeSite S T.scheme_mem (U.obj (op ⦋0⦌)))
          (Y := spacesEtaleRingedTopos T.schemeSite S T.scheme_mem X)
          (spacesEtaleRingedToposHom (a.app (op ⦋0⦌)))).map g) ∧
      Function.Exact (fun g : K ⟶ E ↦
        (derivedPullback (X := spacesEtaleRingedTopos T.schemeSite S T.scheme_mem (U.obj (op ⦋0⦌)))
          (Y := spacesEtaleRingedTopos T.schemeSite S T.scheme_mem X)
          (spacesEtaleRingedToposHom (a.app (op ⦋0⦌)))).map g)
        (fun ψ ↦ augmentationFaceTransport a 0 ψ - augmentationFaceTransport a 1 ψ)
Tag 0DLA, a lemma

Tag 0DLA in the Stacks Project.

AlgebraicGeometry.Space.SimplicialSpacesEtaleSite.exists_derivedPullback_degreeZero_iso_compatible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SimplicialQuasicoherentDerivedGluing.lean, line 476.

Stacks 0DLA: gluing quasi-coherent derived descent data along an fppf hypercovering. Let a : U → X be an fppf hypercovering of an algebraic space X, K₀ ∈ D_{QCoh}(𝒪_{U_0}) and α : L(f_{δ¹₁})^* K₀ ≅ L(f_{δ¹₀})^* K₀ an isomorphism satisfying the cocycle condition (on U_2, through the canonical identifications of the composite face maps). Set K_n = L(f_{τⁿₙ})^* K₀ with τⁿₙ : ⦋0⦌ → ⦋n⦌, 0 ↦ n, and assume Ext^i(K_n, K_n) = 0 for i < 0. Then there are K ∈ D_{QCoh}(𝒪_X) and an isomorphism e : La_0^* K ≅ K₀ compatible with α: L(f_{δ¹₁})^* e ≫ α = θ₁ ≫ θ₀⁻¹ ≫ L(f_{δ¹₀})^* e, where θ_i : L(f_{δ¹ᵢ})^* La_0^* ≅ La_1^* are the canonical isomorphisms (a_0 ∘ f_{δ¹ᵢ} = a_1).

theorem exists_derivedPullback_degreeZero_iso_compatible
    (h : IsHypercoveringAugmentation T.pretopologyBigFppfPretopology U a)
    (K₀ : @DerivedCategory (SheafOfModules.{u + 1} (Stacks.SheafOfModules.Tensor.ringSheaf
      (spacesEtaleRingedTopos T.schemeSite S T.scheme_mem (U.obj (op ⦋0⦌))).O)) _ _
      (HasDerivedCategory.standard _))
    (hK₀ : @DerivedCategoryB.derivedCategoryB _ _ _ (HasDerivedCategory.standard _)
      (SheafOfModules.isQuasicoherentOnSite.{u + 1, u + 1, u + 1, u + 1}
        (Stacks.SheafOfModules.Tensor.ringSheaf
          (spacesEtaleRingedTopos T.schemeSite S T.scheme_mem (U.obj (op ⦋0⦌))).O)) K₀)
    (α : (derivedPullback (spacesEtaleRingedToposHom
        (U.map (SimplexCategory.δ (1 : Fin 2)).op))).obj K₀ ≅
      (derivedPullback (spacesEtaleRingedToposHom
        (U.map (SimplexCategory.δ (0 : Fin 2)).op))).obj K₀)
    (hα : SpacesEtaleDerivedCocycle U K₀ α)
    (hExt : ∀ (n : ℕ) (i : ℤ), i < 0 →
      ∀ g : (derivedPullback (spacesEtaleRingedToposHom
          (U.map (SimplexCategory.const ⦋0⦌ ⦋n⦌ (Fin.last n)).op))).obj K₀ ⟶
        (shiftFunctor (@DerivedCategory (SheafOfModules.{u + 1}
          (Stacks.SheafOfModules.Tensor.ringSheaf
            (spacesEtaleRingedTopos T.schemeSite S T.scheme_mem (U.obj (op ⦋n⦌))).O)) _ _
          (HasDerivedCategory.standard _)) i).obj
          ((derivedPullback (spacesEtaleRingedToposHom
            (U.map (SimplexCategory.const ⦋0⦌ ⦋n⦌ (Fin.last n)).op))).obj K₀), g = 0) :
    ∃ K : @DerivedCategory (SheafOfModules.{u + 1} (Stacks.SheafOfModules.Tensor.ringSheaf
        (spacesEtaleRingedTopos T.schemeSite S T.scheme_mem X).O)) _ _
        (HasDerivedCategory.standard _),
      @DerivedCategoryB.derivedCategoryB _ _ _ (HasDerivedCategory.standard _)
        (SheafOfModules.isQuasicoherentOnSite.{u + 1, u + 1, u + 1, u + 1}
          (Stacks.SheafOfModules.Tensor.ringSheaf
            (spacesEtaleRingedTopos T.schemeSite S T.scheme_mem X).O)) K ∧
      ∃ e : (derivedPullback (X := spacesEtaleRingedTopos T.schemeSite S T.scheme_mem
          (U.obj (op ⦋0⦌))) (Y := spacesEtaleRingedTopos T.schemeSite S T.scheme_mem X)
          (spacesEtaleRingedToposHom (a.app (op ⦋0⦌)))).obj K ≅ K₀,
        (derivedPullback (spacesEtaleRingedToposHom (U.map (SimplexCategory.δ (1 : Fin 2)).op))).map
            e.hom ≫ α.hom =
          ((augmentationTransitionDerivedIso a (SimplexCategory.δ (1 : Fin 2))).hom.app K ≫
            (augmentationTransitionDerivedIso a (SimplexCategory.δ (0 : Fin 2))).inv.app K) ≫
            (derivedPullback (spacesEtaleRingedToposHom
              (U.map (SimplexCategory.δ (0 : Fin 2)).op))).map e.hom
Sources
LeanAlgebraicGeometry.Space.SimplicialSpacesEtaleSite.negativeExt_eq_zero_and_exact_derivedPullback · AlgebraicGeometry.Space.SimplicialSpacesEtaleSite.exists_derivedPullback_degreeZero_iso_compatible

Section85.36 Proper hypercoverings of algebraic spaces#

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

Tag 0DHJ, a lemma

Tag 0DHJ in the Stacks Project.

AlgebraicGeometry.Space.phComparisonMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SimplicialSpaces/PhComparisonFunctor.lean, line 604. The attribute's comment: “the upper horizontal arrow h : Sh((Spaces/U)_{ph, total}) → Sh(U_étale)”.

The upper horizontal arrow of Tag 0DHJ, h : Sh((Spaces/U)_total) → Sh(U_étale), the morphism of topoi of the morphism of sites given by V/U_n ↦ V/U_n.

def phComparisonMorphism :
    MorphismOfTopoi (Sheaf (SimplicialOver.totalTopology J A.left) (Type (u + 1)))
      (Sheaf (etaleSimplicialSite A).totalTopology (Type (u + 1)))

AlgebraicGeometry.Space.spacesEtaleComparisonMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SimplicialSpaces/PhComparisonFunctor.lean, line 627. The attribute's comment: “the lower horizontal arrow h_{-1} : Sh((Spaces/X)_ph) → Sh(X_étale)”.

The lower horizontal arrow of Tag 0DHJ, h_{-1} : Sh(Spaces/X) → Sh(X_étale), the morphism of topoi of the inclusion X_{spaces, étale} → Spaces/X, W ↦ W/X.

def spacesEtaleComparisonMorphism (X : AlgebraicSpaces B S hS) :
    MorphismOfTopoi (Sheaf (J.over X) (Type (u + 1)))
      (Sheaf (SpacesEtale.topology B S hS X) (Type (u + 1)))

AlgebraicGeometry.BigPHSpaceSite.phEtaleComparisonSquarePushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SimplicialSpaces/PhComparisonSquare.lean, line 623. The attribute's comment: “the commutative diagram of topoi, on direct images”.

Tag 0DHJ, on direct images. Let a : U → X be an augmented simplicial algebraic space over S. The diagram of topoi 

Sh((Spaces/U)_{ph, total}) --h--> Sh(U_étale)
        | a_ph                       | a
Sh((Spaces/X)_ph)        --h₋₁--> Sh(X_étale)
commutes: the direct image of h₋₁ ∘ a_ph is that of a ∘ h.

def phEtaleComparisonSquarePushforwardIso :
    (SimplicialOver.augmentationMorphismOfTopoi P.topology A.left A.hom).pushforward ⋙
        (spacesEtaleComparisonMorphism P.topology A.right).pushforward ≅
      (phComparisonMorphism A P.topology).pushforward ⋙ (etaleAugmentationMorphism A).pushforward

AlgebraicGeometry.BigPHSpaceSite.phEtaleComparisonSquareInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SimplicialSpaces/PhComparisonSquare.lean, line 631. The attribute's comment: “the commutative diagram of topoi, on inverse images”.

Tag 0DHJ, on inverse images: h⁻¹ ∘ a⁻¹ ≅ a_ph⁻¹ ∘ h₋₁⁻¹.

def phEtaleComparisonSquareInverseImageIso :
    (etaleAugmentationMorphism A).inverseImage ⋙ (phComparisonMorphism A P.topology).inverseImage ≅
      (spacesEtaleComparisonMorphism P.topology A.right).inverseImage ⋙
        (SimplicialOver.augmentationMorphismOfTopoi P.topology A.left A.hom).inverseImage
Tag 0DHK, a lemma

Tag 0DHK in the Stacks Project.

AlgebraicGeometry.BigPHSpaceSite.etaleAugmentation_inverseImage_fullyFaithful_of_isProperHypercovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SimplicialSpaces/ProperHypercoveringFullyFaithful.lean, line 235. The attribute's comment: “sheaves of sets”.

Stacks 0DHK, sheaves of sets. Let S be a scheme, X an algebraic space over S, U a simplicial algebraic space over S and a : U → X an augmentation which is a proper hypercovering of X. Then a⁻¹ : Sh(X_étale) ⥤ Sh(U_étale) is fully faithful, its essential image consists exactly of the cartesian sheaves, and a_* is a quasi-inverse: the unit of a⁻¹ ⊣ a_* is invertible, and so is its counit at every cartesian sheaf. Here a : Sh(U_étale) → Sh(X_étale) is the morphism of topoi of Section 0DE7, and the category of algebraic spaces over S is the one of a big ph site P.

theorem etaleAugmentation_inverseImage_fullyFaithful_of_isProperHypercovering
    (hA : IsProperHypercovering P.fppfSite S P.fppf_mem A) :
    (etaleAugmentationMorphism A).inverseImage.Full ∧
      (etaleAugmentationMorphism A).inverseImage.Faithful ∧
      (∀ G, (etaleAugmentationMorphism A).inverseImage.essImage G ↔
        (etaleSituation A).IsCartesianSheaf G) ∧
      (∀ F, IsIso ((etaleAugmentationMorphism A).adj.unit.app F)) ∧
      (∀ G, (etaleSituation A).IsCartesianSheaf G →
        IsIso ((etaleAugmentationMorphism A).adj.counit.app G))

AlgebraicGeometry.BigPHSpaceSite.etaleAugmentation_abelianInverseImage_fullyFaithful_of_isProperHypercovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SimplicialSpaces/ProperHypercoveringFullyFaithful.lean, line 271. The attribute's comment: “sheaves of abelian groups”.

Stacks 0DHK, sheaves of abelian groups. Let a : U → X be an augmented simplicial algebraic space which is a proper hypercovering of X. Then the inverse image a⁻¹ : Ab(X_étale) ⥤ Ab(U_étale) on abelian sheaves is fully faithful, its essential image consists exactly of the cartesian abelian sheaves, and the abelian direct image a_* is a quasi-inverse: the unit of a⁻¹ ⊣ a_* is invertible, and so is its counit at every cartesian abelian sheaf.

theorem etaleAugmentation_abelianInverseImage_fullyFaithful_of_isProperHypercovering
    (hA : IsProperHypercovering P.fppfSite S P.fppf_mem A) :
    (Sites.abelianInverseImage (etaleAugmentationMorphism A)).Full ∧
      (Sites.abelianInverseImage (etaleAugmentationMorphism A)).Faithful ∧
      (∀ G, (Sites.abelianInverseImage (etaleAugmentationMorphism A)).essImage G ↔
        (etaleSituation A).IsCartesianAbSheaf G) ∧
      (∀ F, IsIso ((Stacks.Topos.AbelianPushforward.abelianInverseImageAdjPushforward
        (etaleSimplicialSite A).totalTopology (etaleAugmentationMorphism A)).unit.app F)) ∧
      (∀ G, (etaleSituation A).IsCartesianAbSheaf G →
        IsIso ((Stacks.Topos.AbelianPushforward.abelianInverseImageAdjPushforward
          (etaleSimplicialSite A).totalTopology (etaleAugmentationMorphism A)).counit.app G))
Tag 0DHL, a lemma

Tag 0DHL in the Stacks Project.

AlgebraicGeometry.Space.isIso_etaleAugmentation_derivedPlusUnit_of_isProperHypercovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SimplicialSpaces/ProperHypercoveringDerivedDescent.lean, line 331.

Stacks Project, Tag 0DHL, for torsion coefficients. Let S be a scheme, X an algebraic space over S, U a simplicial algebraic space over S and a : U → X an augmentation. If a : U → X is a proper hypercovering of X, then for K ∈ D⁺(X_étale) with torsion cohomology sheaves the canonical map

K → Ra_*(a⁻¹K)

is an isomorphism, where a : Sh(U_étale) → Sh(X_étale) is the morphism of topoi of Section 0DE7.

Here X = A.right, U = A.left and a = A.hom; X_étale is the spaces-étale site of X, the proper hypercovering condition is Section 0DHI (AlgebraicGeometry.Space.IsProperHypercovering), and D⁺ is the bounded below derived category of abelian sheaves. The map is the unit at K of the adjunction a⁻¹ ⊣ Ra_* on D⁺, a⁻¹ being exact and applied degreewise.

The statement of the source is for every K ∈ D⁺(X_étale), and as written it is false: its proof cites Stacks 0DGU, which holds only for complexes with torsion cohomology sheaves. For a counterexample with rational coefficients let X be a normal surface over an algebraically closed field with a cusp singularity x, let π : X̃ → X be a resolution whose exceptional curve E over x is a cycle of rational curves, and let U be the Čech nerve of the proper surjective morphism X̃ ⊔ {x} → X, a proper hypercovering. Descent ℚ = Ra_*a⁻¹ℚ would give, through the spectral sequence of the hypercovering, H²(X_étale, ℚ) ≠ 0, coming from H¹(E, ℚ) = ℚ; but Hⁱ(X_étale, ℚ) = 0 for i > 0 because X is normal. The torsion hypothesis on K is therefore part of the statement, and this is the corrected form.

The proof is that of the source: a big ph site (Spaces/S)_ph on the algebraic spaces over S exists (AlgebraicGeometry.BigFppfSite.bigPHSpaceSite), and in it the square of Tag 0DHJ, the comparison of ph and étale cohomology of torsion sheaves (Stacks 0DGT, Stacks 0DGU), and descent along the ph hypercovering U of X (Stacks 0DA8, Stacks 0D8N) give Ra_*a⁻¹K = Rh₋₁,* Ra_{ph,*} a_ph⁻¹ h₋₁⁻¹ K = K; see AlgebraicGeometry.BigPHSpaceSite.isIso_etaleAugmentation_derivedPlusUnit_of_torsion.

theorem isIso_etaleAugmentation_derivedPlusUnit_of_isProperHypercovering
    (hA : IsProperHypercovering B S hS A)
    (K : DerivedCategory.Plus (Sheaf (SpacesEtale.topology B S hS A.right) AddCommGrpCat.{u + 1}))
    (hK : ∀ i : ℤ, Stacks.Torsion.torsionSheafProperty _
      ((DerivedCategory.homologyFunctor _ i).obj (DerivedCategory.Plus.ι.obj K))) :
    IsIso ((Stacks.ComparingTopologies.derivedPlusAdjunction
      (abelianInverseImageAdjPushforward (etaleSimplicialSite A).totalTopology
        (etaleAugmentationMorphism A))).unit.app K)
Tag 0DHM, a lemma

Tag 0DHM in the Stacks Project.

AlgebraicGeometry.Space.derivedGlobalSectionsIsoOfIsProperHypercovering, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SimplicialSpaces/ProperHypercoveringDerivedDescent.lean, line 363.

Stacks Project, Tag 0DHM, for torsion coefficients. Let S be a scheme, X an algebraic space over S, U a simplicial algebraic space over S and a : U → X an augmentation. If a : U → X is a proper hypercovering of X, then

RΓ(X_étale, K) = RΓ(U_étale, a⁻¹K)

for K ∈ D⁺(X_étale) with torsion cohomology sheaves, where a : Sh(U_étale) → Sh(X_étale) is the morphism of topoi of Section 0DE7.

The isomorphism is the canonical one: RΓ(X_étale, -) of the unit K → Ra_*a⁻¹K followed by the factorisation RΓ(U_étale, -) = RΓ(X_étale, -) ∘ Ra_* of Cohomology on Sites, Remark 08J6 (Stacks.LerayPullbackComparison.lerayPullback), invertible by isIso_etaleAugmentation_derivedPlusUnit_of_isProperHypercovering (Stacks 0DHL).

As for Stacks 0DHL, the source states this for every K ∈ D⁺(X_étale), and as written it is false: for the proper hypercovering of a normal surface with a cusp by the Čech nerve of X̃ ⊔ {x} → X described at isIso_etaleAugmentation_derivedPlusUnit_of_isProperHypercovering, the spectral sequence of the hypercovering computes H²(U_étale, ℚ) ≠ 0 from H¹(E, ℚ) = ℚ for the exceptional curve E, while H²(X_étale, ℚ) = 0 since X is normal. The torsion hypothesis on K is the correction.

def derivedGlobalSectionsIsoOfIsProperHypercovering (hA : IsProperHypercovering B S hS A)
    (K : DerivedCategory.Plus (Sheaf (SpacesEtale.topology B S hS A.right) AddCommGrpCat.{u + 1}))
    (hK : ∀ i : ℤ, Stacks.Torsion.torsionSheafProperty _
      ((DerivedCategory.homologyFunctor _ i).obj (DerivedCategory.Plus.ι.obj K))) :
    (Sheaf.Γ (SpacesEtale.topology B S hS A.right)
        AddCommGrpCat.{u + 1}).rightDerivedFunctorPlus.obj
        K ≅
      (Sheaf.Γ (etaleSimplicialSite A).totalTopology
        AddCommGrpCat.{u + 1}).rightDerivedFunctorPlus.obj
        ((CategoryTheory.Sites.abelianInverseImage
          (etaleAugmentationMorphism A)).mapDerivedCategoryPlus.obj
          K)
Tag 0DHN, a lemma

Tag 0DHN in the Stacks Project.

AlgebraicGeometry.Space.derivedPlusTorsionEquivalenceOfIsProperHypercovering, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SimplicialSpaces/ProperHypercoveringTorsionDerivedEquivalence.lean, line 162. The attribute's comment: “torsion coefficients: a⁻¹ : D⁺_tors(X_étale) ≌ D⁺_{𝒜, tors}(U_étale); the statement for all of D⁺(X_étale) is false”.

Stacks Project, Tag 0DHN, for torsion coefficients. Let S be a scheme, X an algebraic space over S, U a simplicial algebraic space over S and a : U → X an augmentation, and let 𝒜 ⊂ Ab(U_étale) be the weak Serre subcategory of cartesian abelian sheaves. If U is a proper hypercovering of X, then a⁻¹ defines an equivalence

D⁺_tors(X_étale) ⟶ D⁺_{𝒜, tors}(U_étale)

with quasi-inverse Ra_*, where a : Sh(U_étale) → Sh(X_étale) is the morphism of topoi of Section 0DE7, D⁺_tors(X_étale) consists of the bounded below complexes with torsion cohomology sheaves and D⁺_{𝒜, tors}(U_étale) of those whose cohomology sheaves are cartesian and torsion. The functors are identified by AlgebraicGeometry.Space.derivedPlusTorsionEquivalenceOfIsProperHypercovering_functor and AlgebraicGeometry.Space.derivedPlusTorsionEquivalenceOfIsProperHypercovering_inverse.

The source states this for D⁺(X_étale) ⟶ D⁺_𝒜(U_étale), and as written it is false: its proof uses Stacks 0DHL, whose proof cites Stacks 0DGU, which holds only for complexes with torsion cohomology sheaves. For a counterexample with rational coefficients let X be a normal surface over an algebraically closed field with a cusp singularity x, let π : X̃ → X be a resolution whose exceptional curve E over x is a cycle of rational curves, and let U be the Čech nerve of the proper surjective morphism X̃ ⊔ {x} → X, a proper hypercovering. If a⁻¹ were fully faithful on D⁺(X_étale) with quasi-inverse Ra_*, then ℚ = Ra_*a⁻¹ℚ, and the spectral sequence of the hypercovering would give H²(X_étale, ℚ) ≠ 0, coming from H¹(E, ℚ) = ℚ; but Hⁱ(X_étale, ℚ) = 0 for i > 0 because X is normal. The torsion hypothesis is therefore part of the statement, and this is the corrected form.

The proof is the source's: Stacks 0DHK (a⁻¹ on abelian sheaves is fully faithful with essential image the cartesian sheaves) and Stacks 0DHL (K ≅ Ra_*a⁻¹K on D⁺_tors(X_étale)) are the inputs of the formal equivalence of Stacks 0D7U, CategoryTheory.SimplicialSiteSituation.Augmentation.derivedPlusTorsionEquivalence.

def derivedPlusTorsionEquivalenceOfIsProperHypercovering (hA : IsProperHypercovering B S hS A) :
    ((DerivedCategoryB.derivedCategoryB
      (Stacks.Torsion.torsionSheafProperty.{u + 1, u + 1, u + 1}
        (SpacesEtale.topology B S hS A.right))).inverseImage
          DerivedCategory.Plus.ι).FullSubcategory ≌
      ((DerivedCategoryB.derivedCategoryB
        (cartesianTorsionAbSheaf (etaleSituation A))).inverseImage
          DerivedCategory.Plus.ι).FullSubcategory

AlgebraicGeometry.Space.derivedPlusTorsionEquivalenceOfIsProperHypercovering_functor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SimplicialSpaces/ProperHypercoveringTorsionDerivedEquivalence.lean, line 179. The attribute's comment: “the equivalence is a⁻¹”.

The equivalence of Tag 0DHN is a⁻¹: its forward functor, followed by the inclusion into D⁺(U_étale), is the inclusion of D⁺_tors(X_étale) followed by a⁻¹ : D⁺(X_étale) ⥤ D⁺(U_étale), the right derived functor of the exact functor a⁻¹.

theorem derivedPlusTorsionEquivalenceOfIsProperHypercovering_functor
    (hA : IsProperHypercovering B S hS A) :
    (derivedPlusTorsionEquivalenceOfIsProperHypercovering hA).functor ⋙
        ((DerivedCategoryB.derivedCategoryB
          (cartesianTorsionAbSheaf (etaleSituation A))).inverseImage DerivedCategory.Plus.ι).ι =
      ((DerivedCategoryB.derivedCategoryB
        (Stacks.Torsion.torsionSheafProperty.{u + 1, u + 1, u + 1}
          (SpacesEtale.topology B S hS A.right))).inverseImage DerivedCategory.Plus.ι).ι ⋙
        (totalInverseImageAb (etaleSituation A) _ _
          (etaleAugmentation A)).rightDerivedFunctorPlus

AlgebraicGeometry.Space.derivedPlusTorsionEquivalenceOfIsProperHypercovering_inverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SimplicialSpaces/ProperHypercoveringTorsionDerivedEquivalence.lean, line 195. The attribute's comment: “the quasi-inverse is Ra_*”.

The quasi-inverse of the equivalence of Tag 0DHN is Ra_*: its inverse functor, followed by the inclusion into D⁺(X_étale), is the inclusion of D⁺_{𝒜, tors}(U_étale) followed by Ra_* : D⁺(U_étale) ⥤ D⁺(X_étale).

theorem derivedPlusTorsionEquivalenceOfIsProperHypercovering_inverse
    (hA : IsProperHypercovering B S hS A) :
    (derivedPlusTorsionEquivalenceOfIsProperHypercovering hA).inverse ⋙
        ((DerivedCategoryB.derivedCategoryB
          (Stacks.Torsion.torsionSheafProperty.{u + 1, u + 1, u + 1}
            (SpacesEtale.topology B S hS A.right))).inverseImage DerivedCategory.Plus.ι).ι =
      ((DerivedCategoryB.derivedCategoryB
        (cartesianTorsionAbSheaf (etaleSituation A))).inverseImage DerivedCategory.Plus.ι).ι ⋙
        (abelianTotalPushforward (etaleSituation A) _ _
          (etaleAugmentation A)).rightDerivedFunctorPlus
Tag 0DHP, a lemma

Tag 0DHP in the Stacks Project.

AlgebraicGeometry.BigPHSpaceSite.phHypercoveringEtaleSpectralSequenceOfTorsion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/PhHypercoveringEtaleSpectralSequence.lean, line 297.

Let S be a scheme, X an algebraic space over S, U a simplicial algebraic space over S and a : U → X an augmentation. Let 𝓕 be a torsion abelian sheaf on X_étale and let 𝓕_p be its pullback to U_{p, étale}. If U is a ph hypercovering of X, there is a canonical spectral sequence

E₁^{p,q} = H^q_étale(U_p, 𝓕_p)

converging to H^{p+q}_étale(X, 𝓕).

The spectral sequence is phHypercoveringEtaleSpectralSequence, the ph cohomology spectral sequence of the hypercovering (Stacks 09WJ on the total ph site, with ph descent along the hypercovering) at the pullback of 𝓕 to the big ph site of X; its first page and abutment are identified with étale cohomology by Stacks 0DGV and Stacks 0DGW.

The source states the lemma for an arbitrary abelian sheaf 𝓕 and deduces it from Stacks 0DHM, whose proof only covers torsion coefficients (it rests on Stacks 0DGU). As written, for all abelian sheaves, the statement is false, and this is the corrected form, for torsion sheaves, which is the form the proof gives. A counterexample with 𝓕 = ℚ: let X be a normal surface over an algebraically closed field with a cusp singularity x, let X̃ → X be its resolution, with exceptional curve E a cycle of rational curves, so that H¹_étale(E, ℚ) = ℚ, and let U be the Čech nerve of the proper surjective morphism X̃ ⊔ {x} → X, a proper and hence ph hypercovering. Convergence of the canonical spectral sequence to H^{p+q}_étale(X, ℚ) is cohomological descent for ℚ along U, which yields the Mayer–Vietoris sequence H¹(X̃, ℚ) ⊕ H¹(x, ℚ) → H¹(E, ℚ) → H²(X, ℚ) of the abstract blow-up square; as X̃ is normal, H¹(X̃, ℚ) = 0, so H²_étale(X, ℚ) ≠ 0. But H^i_étale(X, ℚ) = 0 for i > 0 on the normal scheme X.

def phHypercoveringEtaleSpectralSequenceOfTorsion
    (hA : MorphismProperty.IsHypercovering P.IsPHCoveringMorphism A)
    (F : Sheaf (etaleTopology P E h A.right) AddCommGrpCat.{u + 1})
    (hF : Stacks.Torsion.torsionSheafProperty _ F) :
    PhHypercoveringEtaleSpectralSequence P E h A F
Sources
LeanAlgebraicGeometry.Space.phComparisonMorphism · AlgebraicGeometry.Space.spacesEtaleComparisonMorphism · AlgebraicGeometry.BigPHSpaceSite.phEtaleComparisonSquarePushforwardIso · AlgebraicGeometry.BigPHSpaceSite.phEtaleComparisonSquareInverseImageIso · AlgebraicGeometry.BigPHSpaceSite.etaleAugmentation_inverseImage_fullyFaithful_of_isProperHypercovering · AlgebraicGeometry.BigPHSpaceSite.etaleAugmentation_abelianInverseImage_fullyFaithful_of_isProperHypercovering · AlgebraicGeometry.Space.isIso_etaleAugmentation_derivedPlusUnit_of_isProperHypercovering · AlgebraicGeometry.Space.derivedGlobalSectionsIsoOfIsProperHypercovering

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.