85.18 Cohomological descent for… to 85.31 An example case

Section85.18 Cohomological descent for hypercoverings: modules #

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

Tag 0D9Z, a lemma

Tag 0D9Z in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.RingedAugmentation.isCartesianModule_of_mem_essImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/AugmentationModuleDescent.lean, line 148. The attribute's comment: “the essential image of a^ consists of cartesian O-modules. Faithfulness of a^ is faithful_pullbackModules; fullness of a^, and essential surjectivity onto the cartesian O-modules making a_ a quasi-inverse, are not proved”.

Stacks 0D9Z, the inclusion of the essential image in the cartesian modules. Every sheaf of O-modules on the total site isomorphic to a pullback a^*F along the ringed augmentation is a cartesian O-module.

This is Stacks 0D7H (3) together with invariance of the cartesian condition under isomorphism.

theorem isCartesianModule_of_mem_essImage
    {F : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf A.O)}
    (hF : A.totalRingedHom.toModulesHom.pullbackModules.essImage F) :
    S.IsModuleFiberTransitionIso A.O F

CategoryTheory.SimplicialSiteSituation.RingedAugmentation.faithful_pullbackModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/AugmentationModuleDescent.lean, line 271. The attribute's comment: “a^ on sheaves of modules is faithful, for a ringed augmentation of a hypercovering whose structure map is the identification O = a^{-1}O_C. The essential-image inclusion is isCartesianModule_of_mem_essImage; fullness of a^, and essential surjectivity onto the cartesian O-modules making a_* a quasi-inverse, are not proved”.

Stacks 0D9Z, the faithfulness half. Let C be a site with equalizers and fibre products, K a hypercovering of its final presheaf, and a the augmentation of the total site of K towards C. For a ringed augmentation along a whose structure map is the identification O = a^{-1}O_C of Stacks 0D9W, the pullback a^* : Mod(O_C) ⥤ Mod(O) of sheaves of modules is faithful.

Because the structure map is that identification, the underlying sheaf of sets of a^*M is the inverse image of the underlying sheaf of M; faithfulness then descends from Stacks 0D8E (1), faithfulness of a^{-1} on sheaves of sets.

theorem faithful_pullbackModules [IsIso A.totalRingedHom.fSharpInverseImage] :
    A.totalRingedHom.toModulesHom.pullbackModules.Faithful

CategoryTheory.SimplicialSiteSituation.RingedAugmentation.full_pullbackModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/AugmentationModuleDescent.lean, line 284. The attribute's comment: “a^* on sheaves of modules is full, for a ringed augmentation of a hypercovering whose structure map is the identification O = a^{-1}O_C”.

Stacks 0D9Z, the fullness half. For a ringed augmentation of a hypercovering whose structure map is the identification O = a^{-1}O_C of Stacks 0D9W, the pullback a^* : Mod(O_C) ⥤ Mod(O) of sheaves of modules is full.

Because the structure map is that identification, the pullback of modules is the Stacks 03D2 inverse image of modules followed by an equivalence; fullness then descends from Stacks 0D8E (1), full faithfulness of a^{-1} on sheaves of sets.

theorem full_pullbackModules [IsIso A.totalRingedHom.fSharpInverseImage] :
    A.totalRingedHom.toModulesHom.pullbackModules.Full

CategoryTheory.SimplicialSiteSituation.RingedAugmentation.fullyFaithfulPullbackModules, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/AugmentationModuleDescent.lean, line 292. The attribute's comment: “a^* on sheaves of modules is fully faithful, for a ringed augmentation of a hypercovering whose structure map is the identification O = a^{-1}O_C”.

Stacks 0D9Z, full faithfulness of a^* on sheaves of modules.

def fullyFaithfulPullbackModules [IsIso A.totalRingedHom.fSharpInverseImage] :
    A.totalRingedHom.toModulesHom.pullbackModules.FullyFaithful

CategoryTheory.SimplicialSiteSituation.RingedAugmentation.essImage_pullbackModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/AugmentationModuleDescent.lean, line 306. The attribute's comment: “every cartesian O-module is an a^*M, for a ringed augmentation of a hypercovering whose structure map is the identification O = a^{-1}O_C”.

Stacks 0D9Z, essential surjectivity onto the cartesian O-modules. For a ringed augmentation of a hypercovering whose structure map is the identification O = a^{-1}O_C of Stacks 0D9W, every cartesian sheaf of O-modules on the total site is a pullback a^*M.

The underlying sheaf of sets of a cartesian sheaf of modules is cartesian, hence an inverse image by Stacks 0D8E (1); and a sheaf of modules whose underlying sheaf of sets is an inverse image is a pullback.

theorem essImage_pullbackModules [IsIso A.totalRingedHom.fSharpInverseImage]
    {F : SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf
      (J := (situation P.toGrothendieck H.toSimplicialObject).totalTopology) A.O))}
    (hF : (situation P.toGrothendieck H.toSimplicialObject).IsModuleFiberTransitionIso A.O F) :
    A.totalRingedHom.toModulesHom.pullbackModules.essImage F

CategoryTheory.SimplicialSiteSituation.RingedAugmentation.mem_essImage_pullbackModules_iff_isCartesianModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/AugmentationModuleDescent.lean, line 321. The attribute's comment: “the essential image of a^* on sheaves of modules is exactly the cartesian O-modules, for a ringed augmentation of a hypercovering whose structure map is the identification O = a^{-1}O_C”.

Stacks 0D9Z, the essential image of a^* is exactly the cartesian O-modules. One inclusion is isCartesianModule_of_mem_essImage, which is Stacks 0D7H (3); the other is essImage_pullbackModules.

theorem mem_essImage_pullbackModules_iff_isCartesianModule
    [IsIso A.totalRingedHom.fSharpInverseImage]
    (F : SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf
      (J := (situation P.toGrothendieck H.toSimplicialObject).totalTopology) A.O))) :
    A.totalRingedHom.toModulesHom.pullbackModules.essImage F ↔
      (situation P.toGrothendieck H.toSimplicialObject).IsModuleFiberTransitionIso A.O F

CategoryTheory.SimplicialSiteSituation.RingedAugmentation.isIso_pullbackAdjPushforwardModules_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/AugmentationModuleDescent.lean, line 334. The attribute's comment: “M = a_ a^ M on sheaves of modules, for a ringed augmentation of a hypercovering whose structure map is the identification O = a^{-1}O_C”.

Stacks 0D9Z, a_* is a quasi-inverse on Mod(O_C). The unit M ⟶ a_*a^*M of the adjunction of Stacks 03D7 is an isomorphism for every sheaf of O_C-modules: a fully faithful left adjoint has invertible unit.

theorem isIso_pullbackAdjPushforwardModules_unit
    [IsIso A.totalRingedHom.fSharpInverseImage] :
    IsIso (RingedToposHom.pullbackAdjPushforwardModules A.totalRingedHom).unit

CategoryTheory.SimplicialSiteSituation.RingedAugmentation.isIso_pullbackAdjPushforwardModules_counit_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/AugmentationModuleDescent.lean, line 348. The attribute's comment: “a^ a_ F = F for a cartesian O-module F, for a ringed augmentation of a hypercovering whose structure map is the identification O = a^{-1}O_C”.

Stacks 0D9Z, a_* is a quasi-inverse on the cartesian O-modules. The counit a^*a_*F ⟶ F of the adjunction of Stacks 03D7 is an isomorphism at every cartesian sheaf of O-modules: a fully faithful left adjoint has invertible counit exactly on its essential image, which by mem_essImage_pullbackModules_iff_isCartesianModule is the cartesian O-modules.

theorem isIso_pullbackAdjPushforwardModules_counit_app
    [IsIso A.totalRingedHom.fSharpInverseImage]
    {F : SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf
      (J := (situation P.toGrothendieck H.toSimplicialObject).totalTopology) A.O))}
    (hF : (situation P.toGrothendieck H.toSimplicialObject).IsModuleFiberTransitionIso A.O F) :
    IsIso ((RingedToposHom.pullbackAdjPushforwardModules A.totalRingedHom).counit.app F)

Tag 0DA0, a lemma

Tag 0DA0 in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.isIso_derivedPullbackPushforwardUnit_app_of_hypercovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringModuleCohomologicalDescent.lean, line 364. The attribute's comment: “granted the module form of Tag 0D8E as hunit and the Ra_-acyclicity of a^ of a K-injective complex as hacyclic -- the two inputs that this library's Tag 0D8G, isIso_derivedAugmentationUnit_app_of_hypercovering, is itself granted”.

Stacks 0DA0, granted the two inputs this library's Stacks 0D8G is granted, in their module form. Let C be a site with equalizers and fibre products, let O_C be a sheaf of commutative rings on it and let K be a hypercovering of C. With O = a⁻¹O_C on the total site and a : (Sh((C/K)_total), O) ⟶ (Sh(C), O_C) the ringed augmentation of Stacks 0D9W, the canonical map

E ⟶ R a_* L a^* E

is an isomorphism for every object E of the unbounded derived category D(O_C) of sheaves of O_C-modules.

E is arbitrary: no boundedness is assumed and the coefficients are the full category of sheaves of modules. La^* is the degreewise pullback, which is the source's first observation, and nothing of Stacks 06YY, 0G6R or 05VD enters.

The two hypotheses are the two of Stacks.CategoryTheory.Hypercovering.isIso_derivedAugmentationUnit_app_of_hypercovering, read for sheaves of modules instead of abelian sheaves. hunit is Stacks 0D8E in its module form, that the underived unit M ⟶ a_*a^*M is an isomorphism; it is not available here because its proof needs the abelian form of Stacks 0D86, which this library has for sheaves of sets only. hacyclic says that a^* of a K-injective complex of O_C-modules computes Ra_*; it is the derived content of the source's computation of Ra_*a^* by the Čech complex, which rests on the spectral sequence of Stacks 0D7A that this library does not build. The source's own route — the abelian statement of Stacks 0D8G together with Stacks 0D6J — would carry the same two hypotheses through Stacks 0D8G and in addition the clause of Stacks 0D6J about the derived direct image, which this library does not have; so that route is not taken and the count of deferred inputs is exactly two.

theorem isIso_derivedPullbackPushforwardUnit_app_of_hypercovering
    (hunit : IsIso (AlgebraicGeometry.RingedToposHom.pullbackAdjPushforwardModules
      (hypercoveringRingedAugmentation J H OC).totalRingedHom).unit)
    (hacyclic : AlgebraicGeometry.RingedToposHom.PullbackComputesDerivedPushforward.{u}
      (hypercoveringRingedAugmentation J H OC).totalRingedHom)
    (E : DerivedCategory (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf (J := (hypercoveringRingedAugmentation J H OC).augmentationRingedTopos.J))
      (hypercoveringRingedAugmentation J H OC).augmentationRingedTopos.O))) :
    IsIso ((AlgebraicGeometry.RingedToposHom.derivedPullbackPushforwardUnit
      (hypercoveringRingedAugmentation J H OC).totalRingedHom).app E)

Declarations registered for the tag:

SimplicialSemiRepresentable.isIso_derivedPullbackPushforwardUnit_of_hypercoveringOfTerminal registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringModuleCohomologicalDescentTags.lean, line 23 (StacksFrontier).

Tag 0DA1, a lemma

Tag 0DA1 in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.derivedGlobalSectionsPullbackIsoOfHypercovering, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringModuleDerivedGlobalSections.lean, line 290. The attribute's comment: “granted the two inputs of this library's Tag 0DA0 -- the module form of Tag 0D8E as hunit and the Ra_-acyclicity of a^ of a K-injective complex as hacyclic -- and granted the underived identity Γ(C, a_*M) = Γ(total, M) of Tag 08J6 as hΓ. Unbounded: the isomorphism is of functors on all of D(O_C). Both sides are read in D(Ab), the module structure of global sections over Γ(C, O_C) being forgotten”.

Stacks 0DA1, granted the inputs the library does not have. For a site C with equalizers and fibre products, a sheaf of commutative rings O_C on it, a hypercovering K of C and the ringed augmentation a : (Sh((C/K)_total), O) ⟶ (Sh(C), O_C) of Stacks 0D9W with O = a⁻¹O_C, derived global sections on C are derived global sections on the total site of the derived pullback:

RΓ(C, E) = RΓ((C/K)_total, La^*E).

The statement is an isomorphism of functors on the unbounded derived category D(O_C) of sheaves of O_C-modules, so it holds at every object E with no boundedness assumption, which is the form the source states.

Three hypotheses are carried. hunit and hacyclic are the two inputs of this library's Stacks 0DA0, inherited unchanged from isIso_derivedPullbackPushforwardUnit_app_of_hypercovering: the first is Stacks 0D8E in its module form, that the underived unit M ⟶ a_*a^*M is an isomorphism, and the second is that a^* of a K-injective complex computes R a_*. hΓ is the underived identity Γ(C, a_*M) = Γ((C/K)_total, M) on which the factorisation of Stacks 08J6 rests; it is unavailable here for the same reason as its abelian counterpart in this library's Stacks 0D8H, namely that nothing says the inverse image of a morphism of topoi carries a constant abelian sheaf to a constant abelian sheaf. The derived content of Stacks 08J6 is not assumed: see the module docstring.

Both sides are read in D(Ab): global sections of a sheaf of modules are taken with the module structure forgotten, the source's D(Γ(C, O_C)) reading being unavailable in this library.

def derivedGlobalSectionsPullbackIsoOfHypercovering
    (hunit : IsIso (AlgebraicGeometry.RingedToposHom.pullbackAdjPushforwardModules
      (hypercoveringRingedAugmentation J H OC).totalRingedHom).unit)
    (hacyclic : AlgebraicGeometry.RingedToposHom.PullbackComputesDerivedPushforward.{u}
      (hypercoveringRingedAugmentation J H OC).totalRingedHom)
    (hΓ : AlgebraicGeometry.RingedToposHom.pushforwardModules
          (X := (hypercoveringSituation J H).totalRingedTopos
            (hypercoveringRingedAugmentation J H OC).O)
          (Y := (hypercoveringRingedAugmentation J H OC).augmentationRingedTopos)
          (hypercoveringRingedAugmentation J H OC).totalRingedHom ⋙
        AlgebraicGeometry.RingedTopos.moduleGlobalSections
          (hypercoveringRingedAugmentation J H OC).augmentationRingedTopos ≅
      AlgebraicGeometry.RingedTopos.moduleGlobalSections
        ((hypercoveringSituation J H).totalRingedTopos
          (hypercoveringRingedAugmentation J H OC).O)) :
    AlgebraicGeometry.RingedTopos.derivedModuleGlobalSections
        (hypercoveringRingedAugmentation J H OC).augmentationRingedTopos ≅
      (AlgebraicGeometry.RingedToposHom.leftDerivedPullbackOfIsIsoFSharp
          (X := (hypercoveringSituation J H).totalRingedTopos
            (hypercoveringRingedAugmentation J H OC).O)
          (Y := (hypercoveringRingedAugmentation J H OC).augmentationRingedTopos)
          (hypercoveringRingedAugmentation J H OC).totalRingedHom).functor ⋙
        AlgebraicGeometry.RingedTopos.derivedModuleGlobalSections
          ((hypercoveringSituation J H).totalRingedTopos
            (hypercoveringRingedAugmentation J H OC).O)

Stacks.CategoryTheory.Hypercovering.derivedLinearGlobalSectionsPullbackIsoOfHypercovering, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringModuleDerivedGlobalSectionsUnconditional.lean, line 205.

Stacks 0DA1. Let C be a site with equalizers and fibre products, let O_C be a sheaf of commutative rings on it and let K be a hypercovering of C. With O = a⁻¹O_C on the total site and a : (Sh((C/K)_total), O) ⟶ (Sh(C), O_C) the ringed augmentation of Stacks 0D9W, there is a canonical isomorphism

RΓ(C, E) = RΓ((C/K)_total, La^*E)

naturally in E in the unbounded derived category D(O_C). Here RΓ(C, -) takes values in D(Γ(C, O_C)), and the right hand side, which lives in D(Γ((C/K)_total, O)), is read in D(Γ(C, O_C)) through restriction of scalars along the ring map Γ(C, O_C) ⟶ Γ((C/K)_total, O) induced by a. Nothing is assumed beyond the hypercovering conditions on K. The forward map is pinned to the canonical one by derivedLinearGlobalSectionsPullbackIsoOfHypercovering_hom_app.

def derivedLinearGlobalSectionsPullbackIsoOfHypercovering :
    RingedTopos.derivedLinearGlobalSections
        (hypercoveringRingedAugmentation J H OC).augmentationRingedTopos ≅
      (RingedToposHom.leftDerivedPullbackOfIsIsoFSharp
          (X := (hypercoveringSituation J H).totalRingedTopos
            (hypercoveringRingedAugmentation J H OC).O)
          (Y := (hypercoveringRingedAugmentation J H OC).augmentationRingedTopos)
          (hypercoveringRingedAugmentation J H OC).totalRingedHom).functor ⋙
        RingedTopos.derivedLinearGlobalSections
          ((hypercoveringSituation J H).totalRingedTopos
            (hypercoveringRingedAugmentation J H OC).O) ⋙
        (ModuleCat.restrictScalars.{u} (globalSectionsRingHom
          (X := (hypercoveringSituation J H).totalRingedTopos
            (hypercoveringRingedAugmentation J H OC).O)
          (Y := (hypercoveringRingedAugmentation J H OC).augmentationRingedTopos)
          (hypercoveringRingedAugmentation J H OC).totalRingedHom.toModulesHom)).mapDerivedCategory

Stacks.CategoryTheory.Hypercovering.derivedLinearGlobalSectionsPullbackIsoOfHypercovering_hom_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringModuleDerivedGlobalSectionsUnconditional.lean, line 231. The attribute's comment: “the forward map of the isomorphism is the canonical one: RΓ(C, -) of the derived unit E ⟶ Ra_La^E, followed by the factorisation of Tag 08J6”.

Stacks 0DA1, the isomorphism is the canonical one. At every E of D(O_C) its forward map is RΓ(C, -) of the derived unit E ⟶ Ra_*La^*E of the ringed augmentation, followed by the factorisation RΓ(C, Ra_*-) = RΓ((C/K)_total, -) of Stacks 08J6.

theorem derivedLinearGlobalSectionsPullbackIsoOfHypercovering_hom_app
    (E : DerivedCategory (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf
      (J := (hypercoveringRingedAugmentation J H OC).augmentationRingedTopos.J))
      (hypercoveringRingedAugmentation J H OC).augmentationRingedTopos.O))) :
    (derivedLinearGlobalSectionsPullbackIsoOfHypercovering J H OC).hom.app E =
      (RingedTopos.derivedLinearGlobalSections
          (hypercoveringRingedAugmentation J H OC).augmentationRingedTopos).map
          ((RingedToposHom.derivedPullbackPushforwardUnit
            (hypercoveringRingedAugmentation J H OC).totalRingedHom).app E) ≫
        (RingedToposHom.derivedLinearGlobalSectionsPushforwardIso
          (hypercoveringRingedAugmentation J H OC).totalRingedHom).hom.app
          ((RingedToposHom.leftDerivedPullbackOfIsIsoFSharp
            (X := (hypercoveringSituation J H).totalRingedTopos
              (hypercoveringRingedAugmentation J H OC).O)
            (Y := (hypercoveringRingedAugmentation J H OC).augmentationRingedTopos)
            (hypercoveringRingedAugmentation J H OC).totalRingedHom).functor.obj E)

Tag 0DA2, a lemma

Tag 0DA2 in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.derivedPullbackEquivalenceOfHypercovering, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringModuleBoundedBelowEquivalence.lean, line 602. The attribute's comment: “granted the two inputs of this library's Tag 0DA0 -- the module form of Tag 0D8E as hunit and the Ra_-acyclicity of a^ of a K-injective complex as hacyclic -- and granted the essential-surjectivity clause of Tag 0D9Z as hsurj. The weak Serre property of the cartesian O-modules, Tag 0D7J (2), is not available in this library and is not used: D^+_A(O) is read as the bounded below objects whose cohomology modules are cartesian”. References: SGA 4 Vbis (2.2.7), “special case”; SGA 4 Vbis (2.4.12), “special case”.

Stacks 0DA2, granted the inputs the library does not have. For a site C with equalizers and fibre products, a sheaf of commutative rings O_C on it, a hypercovering K of C, the ringed augmentation a : (Sh((C/K)_total), O) ⟶ (Sh(C), O_C) of Stacks 0D9W with O = a⁻¹O_C, and the class 𝒜 ⊂ Mod(O) of cartesian O-modules, the derived pullback is an equivalence

La^* : D⁺(O_C) ⟶ D⁺_𝒜(O)

with quasi-inverse R a_*. Both functors of the equivalence are the restrictions of La^* and of R a_* on the nose, since the equivalence is the restricted adjunction.

Three hypotheses are carried. hunit and hacyclic are the two inputs of this library's Stacks 0DA0, inherited unchanged from isIso_derivedPullbackPushforwardUnit_app_of_hypercovering: the first is Stacks 0D8E in its module form, that the underived unit M ⟶ a_*a^*M is an isomorphism, and the second is that a^* of a K-injective complex computes R a_*. hsurj is the remaining clause of Stacks 0D9Z, that every cartesian O-module on the total site lies in the essential image of a^*; the development carries the converse inclusion (RingedAugmentation.isCartesianModule_of_mem_essImage) and faithfulness of a^*, and the degree-zero condition on a hypercovering does not supply the rest. The derived content of Stacks 0D7U is not assumed: see the module docstring.

𝒜 is read as the class of cartesian O-modules, closed under isomorphism; that it is a weak Serre subcategory, which is Stacks 0D7J (2) and which this library has only for abelian sheaves, is not used anywhere in the argument.

def derivedPullbackEquivalenceOfHypercovering
    (hunit : IsIso (AlgebraicGeometry.RingedToposHom.pullbackAdjPushforwardModules
      (hypercoveringRingedAugmentation J H OC).totalRingedHom).unit)
    (hacyclic : AlgebraicGeometry.RingedToposHom.PullbackComputesDerivedPushforward.{u}
      (hypercoveringRingedAugmentation J H OC).totalRingedHom)
    (hsurj : ∀ M, hypercoveringCartesianModules J H OC M →
      (Stacks.Sheaves.RingedToposModules.RingedToposHom.pullbackModules
        (X := (hypercoveringSituation J H).totalRingedTopos
          (hypercoveringRingedAugmentation J H OC).O)
        (Y := (hypercoveringRingedAugmentation J H OC).augmentationRingedTopos)
        (hypercoveringRingedAugmentation J H OC).totalRingedHom.toModulesHom).essImage M) :
    (AlgebraicGeometry.RingedToposHom.derivedPlusTarget
        (Y := (hypercoveringRingedAugmentation J H OC).augmentationRingedTopos)).FullSubcategory ≌
      (AlgebraicGeometry.RingedToposHom.derivedPlusProperty
        (hypercoveringCartesianModules J H OC)).FullSubcategory

Stacks.CategoryTheory.Hypercovering.derivedPullbackEquivalenceOfHypercovering_functor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringModuleBoundedBelowEquivalence.lean, line 639. The attribute's comment: “the forward functor of the equivalence is La^*, under the three hypotheses of derivedPullbackEquivalenceOfHypercovering”.

Stacks 0DA2, the forward functor of the equivalence is La^*: it is the restriction of the derived pullback to the bounded below subcategories.

theorem derivedPullbackEquivalenceOfHypercovering_functor
    (hunit : IsIso (AlgebraicGeometry.RingedToposHom.pullbackAdjPushforwardModules
      (hypercoveringRingedAugmentation J H OC).totalRingedHom).unit)
    (hacyclic : AlgebraicGeometry.RingedToposHom.PullbackComputesDerivedPushforward.{u}
      (hypercoveringRingedAugmentation J H OC).totalRingedHom)
    (hsurj : ∀ M, hypercoveringCartesianModules J H OC M →
      (Stacks.Sheaves.RingedToposModules.RingedToposHom.pullbackModules
        (X := (hypercoveringSituation J H).totalRingedTopos
          (hypercoveringRingedAugmentation J H OC).O)
        (Y := (hypercoveringRingedAugmentation J H OC).augmentationRingedTopos)
        (hypercoveringRingedAugmentation J H OC).totalRingedHom.toModulesHom).essImage M) :
    (derivedPullbackEquivalenceOfHypercovering J H OC hunit hacyclic hsurj).functor =
      AlgebraicGeometry.RingedToposHom.derivedPullbackPlus
        (X := (hypercoveringSituation J H).totalRingedTopos
          (hypercoveringRingedAugmentation J H OC).O)
        (Y := (hypercoveringRingedAugmentation J H OC).augmentationRingedTopos)
        (hypercoveringRingedAugmentation J H OC).totalRingedHom
        (hypercoveringCartesianModules J H OC)
        (isCartesianModule_pullbackModules_hypercovering J H OC)

Stacks.CategoryTheory.Hypercovering.derivedPullbackEquivalenceOfHypercovering_inverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringModuleBoundedBelowEquivalence.lean, line 664. The attribute's comment: “the quasi-inverse of the equivalence is Ra_*, under the three hypotheses of derivedPullbackEquivalenceOfHypercovering”.

Stacks 0DA2, the quasi-inverse of the equivalence is R a_*: it is the restriction of the derived direct image to the bounded below subcategories.

theorem derivedPullbackEquivalenceOfHypercovering_inverse
    (hunit : IsIso (AlgebraicGeometry.RingedToposHom.pullbackAdjPushforwardModules
      (hypercoveringRingedAugmentation J H OC).totalRingedHom).unit)
    (hacyclic : AlgebraicGeometry.RingedToposHom.PullbackComputesDerivedPushforward.{u}
      (hypercoveringRingedAugmentation J H OC).totalRingedHom)
    (hsurj : ∀ M, hypercoveringCartesianModules J H OC M →
      (Stacks.Sheaves.RingedToposModules.RingedToposHom.pullbackModules
        (X := (hypercoveringSituation J H).totalRingedTopos
          (hypercoveringRingedAugmentation J H OC).O)
        (Y := (hypercoveringRingedAugmentation J H OC).augmentationRingedTopos)
        (hypercoveringRingedAugmentation J H OC).totalRingedHom.toModulesHom).essImage M) :
    (derivedPullbackEquivalenceOfHypercovering J H OC hunit hacyclic hsurj).inverse =
      AlgebraicGeometry.RingedToposHom.derivedPushforwardPlus
        (X := (hypercoveringSituation J H).totalRingedTopos
          (hypercoveringRingedAugmentation J H OC).O)
        (Y := (hypercoveringRingedAugmentation J H OC).augmentationRingedTopos)
        (hypercoveringRingedAugmentation J H OC).totalRingedHom
        (hypercoveringCartesianModules J H OC)

Stacks.CategoryTheory.Hypercovering.exists_derivedPullbackEquivalence_hypercoveringOfTerminal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringModuleBoundedBelowEquivalenceUnconditional.lean, line 232.

Stacks 0DA2. Let C be a site with equalizers and fibre products, let O_C be a sheaf of commutative rings on it and let K be a hypercovering of C; let a : (Sh((C/K)_total), O) ⟶ (Sh(C), O_C) be the ringed augmentation of Stacks 0D9W, so O = a⁻¹O_C. Then the cartesian O-modules 𝒜 ⊂ Mod(O) form a weak Serre subcategory, and the functor La^* defines an equivalence

D⁺(O_C) ⟶ D⁺_𝒜(O)

with quasi-inverse R a_*: there is an equivalence of categories whose functor is the restriction of the derived pullback La^* to the bounded below subcategories and whose inverse is the restriction of the derived direct image R a_*. Here D⁺(O_C) is the full subcategory of bounded below objects of D(O_C), and D⁺_𝒜(O) that of bounded below objects of D(O) all of whose cohomology modules are cartesian. Nothing is assumed beyond the hypotheses of the source.

theorem exists_derivedPullbackEquivalence_hypercoveringOfTerminal :
    (hypercoveringCartesianModules J H OC).IsWeakSerreClass ∧
      ∃ e : (AlgebraicGeometry.RingedToposHom.derivedPlusTarget
          (Y := (hypercoveringRingedAugmentation J H OC).augmentationRingedTopos)).FullSubcategory ≌
        (AlgebraicGeometry.RingedToposHom.derivedPlusProperty
          (hypercoveringCartesianModules J H OC)).FullSubcategory,
        e.functor = AlgebraicGeometry.RingedToposHom.derivedPullbackPlus
          (X := (hypercoveringSituation J H).totalRingedTopos
            (hypercoveringRingedAugmentation J H OC).O)
          (Y := (hypercoveringRingedAugmentation J H OC).augmentationRingedTopos)
          (hypercoveringRingedAugmentation J H OC).totalRingedHom
          (hypercoveringCartesianModules J H OC)
          (isCartesianModule_pullbackModules_hypercovering J H OC) ∧
        e.inverse = AlgebraicGeometry.RingedToposHom.derivedPushforwardPlus
          (X := (hypercoveringSituation J H).totalRingedTopos
            (hypercoveringRingedAugmentation J H OC).O)
          (Y := (hypercoveringRingedAugmentation J H OC).augmentationRingedTopos)
          (hypercoveringRingedAugmentation J H OC).totalRingedHom
          (hypercoveringCartesianModules J H OC)

Sources

LeanCategoryTheory.SimplicialSiteSituation.RingedAugmentation.isCartesianModule_of_mem_essImage · CategoryTheory.SimplicialSiteSituation.RingedAugmentation.faithful_pullbackModules · CategoryTheory.SimplicialSiteSituation.RingedAugmentation.full_pullbackModules · CategoryTheory.SimplicialSiteSituation.RingedAugmentation.fullyFaithfulPullbackModules · CategoryTheory.SimplicialSiteSituation.RingedAugmentation.essImage_pullbackModules · CategoryTheory.SimplicialSiteSituation.RingedAugmentation.mem_essImage_pullbackModules_iff_isCartesianModule · CategoryTheory.SimplicialSiteSituation.RingedAugmentation.isIso_pullbackAdjPushforwardModules_unit · CategoryTheory.SimplicialSiteSituation.RingedAugmentation.isIso_pullbackAdjPushforwardModules_counit_app

Section85.19 Cohomological descent for hypercoverings of an object #

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

Tag 0D8K, a lemma

Tag 0D8K in the Stacks Project.

Stacks.Topology.LocallyQuasiCompactQcSite.mem_essImage_iff_isCartesianSheaf_qcAugmentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcSmallModel.lean, line 338. The attribute's comment: “part (1) for a hypercovering augmentation of the quasi-compact site LC_qc”.

Stacks 0D8K (1) for a hypercovering augmentation of LC_qc. Let a : U ⟶ Y be a hypercovering augmentation of an object Y of the quasi-compact site, in the sense of Stacks 09X8. Then on the total site of the associated simplicial semi-representable object, carried to the small model, the sheaves of sets which are inverse images along the augmentation are exactly the cartesian ones.

This is the statement the smallness reconciliation buys. Its hypothesis is a datum on LC_qc, which is where Stacks 0DAF's diagram lives; its conclusion is about the total site of the small model, which is where the apparatus of Stacks 09WE exists at all; and smallSheafEquiv identifies the base topos of the two.

theorem mem_essImage_iff_isCartesianSheaf_qcAugmentation {Y : S.category}
    (U : SimplicialObject S.category)
    (a : U ⟶ (SimplicialObject.const S.category).obj Y)
    (h : IsHypercoveringAugmentation S.pretopology U a)
    (E : Sheaf (situation (S.smallOverTopology Y)
      (S.smallAssociatedSimplicialObject U a)).totalTopology (Type u)) :
    (totalLocalizationMorphism (S.smallOverTopology Y)
        (S.smallAssociatedSimplicialObject U a)).inverseImage.essImage E ↔
      (situation (S.smallOverTopology Y)
        (S.smallAssociatedSimplicialObject U a)).IsCartesianSheaf E

Stacks.Topology.LocallyQuasiCompactQcSite.mem_essImage_iff_isCartesianAbSheaf_qcAugmentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcSmallModel.lean, line 357. The attribute's comment: “part (2) for a hypercovering augmentation of the quasi-compact site LC_qc”.

Stacks 0D8K (2) for a hypercovering augmentation of LC_qc. The same for sheaves of abelian groups: on the total site of the associated simplicial semi-representable object carried to the small model, the abelian sheaves which are inverse images along the augmentation are exactly the cartesian ones.

theorem mem_essImage_iff_isCartesianAbSheaf_qcAugmentation {Y : S.category}
    (U : SimplicialObject S.category)
    (a : U ⟶ (SimplicialObject.const S.category).obj Y)
    (h : IsHypercoveringAugmentation S.pretopology U a)
    (G : Sheaf (situation (S.smallOverTopology Y)
      (S.smallAssociatedSimplicialObject U a)).totalTopology Ab.{u}) :
    ((totalForget (S.smallAssociatedSimplicialObject U a)).sheafPushforwardContinuous Ab.{u}
        ((situation (S.smallOverTopology Y)
          (S.smallAssociatedSimplicialObject U a)).totalTopology)
        (S.smallOverTopology Y)).essImage G ↔
      (situation (S.smallOverTopology Y)
        (S.smallAssociatedSimplicialObject U a)).IsCartesianAbSheaf G

CategoryTheory.SimplicialSemiRepresentable.faithful_inverseImage_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringObjectDescent.lean, line 222. The attribute's comment: “part (1): a^{-1} on sheaves of sets is faithful”.

Stacks 0D8K (1), the faithfulness half. For a hypercovering K of X the inverse image a^{-1} : Sh(C/X) ⥤ Sh((C/K)_total) of the augmentation is faithful.

The inverse image is restriction along j_total, which is continuous and cover dense, and restriction along such a functor is faithful by Stacks 04D9.

theorem faithful_inverseImage_over (hK : IsHypercovering P K) :
    (totalLocalizationMorphism (P.toGrothendieck.over X) K).inverseImage.Faithful

CategoryTheory.SimplicialSemiRepresentable.faithful_totalInverseImage_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringObjectDescent.lean, line 230. The attribute's comment: “part (1): a^{-1} of Stacks 0D70 on sheaves of sets is faithful”.

Stacks 0D8K (1), the faithfulness half, for the inverse image of the morphism of topoi which Stacks 0D70 attaches to the augmentation. By Stacks 0D8B that functor is isomorphic to restriction along j_total, and faithfulness is invariant under isomorphism of functors.

theorem faithful_totalInverseImage_over (hK : IsHypercovering P K) :
    Functor.Faithful
      (augmentation (P.toGrothendieck.over X) K).totalMorphismOfTopoi.inverseImage

CategoryTheory.SimplicialSemiRepresentable.faithful_abelianInverseImage_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringObjectDescent.lean, line 243. The attribute's comment: “part (2): a^{-1} on abelian sheaves is faithful”.

Stacks 0D8K (2), the faithfulness half. For a hypercovering K of X the inverse image a^{-1} : Ab(C/X) ⥤ Ab((C/K)_total) of the augmentation — restriction along j_total on abelian sheaves, as in Stacks 09WM (2) — is faithful.

Cover density of j_total is a statement about the site, so the argument of faithful_inverseImage_over applies at any coefficient category.

theorem faithful_abelianInverseImage_over (hK : IsHypercovering P K) :
    ((totalForget K).sheafPushforwardContinuous Ab.{u}
      ((situation (P.toGrothendieck.over X) K).totalTopology)
      (P.toGrothendieck.over X)).Faithful

CategoryTheory.SimplicialSemiRepresentable.full_inverseImage_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringObjectDescent.lean, line 259. The attribute's comment: “part (1): a^{-1} on sheaves of sets is full”.

Stacks 0D8K (1), the fullness half. For a hypercovering K of X the inverse image a^{-1} : Sh(C/X) ⥤ Sh((C/K)_total) of the augmentation is full.

The inverse image is restriction along j_total, which is continuous, cover dense by the degree-zero clause of Stacks 01G5 and locally full by CategoryTheory.SimplicialSemiRepresentable.isLocallyFull_totalForget_over; restriction along such a functor is full.

theorem full_inverseImage_over (hK : IsHypercovering P K) :
    (totalLocalizationMorphism (P.toGrothendieck.over X) K).inverseImage.Full

CategoryTheory.SimplicialSemiRepresentable.isIso_unit_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringObjectDescent.lean, line 277. The attribute's comment: “part (1): the unit E = a_*a⁻¹E on sheaves of sets is an isomorphism”.

Stacks 0D8K (1), the degree-zero identification E = a_* a^{-1} E. For a hypercovering K of X and every sheaf of sets E on C/X the canonical map E ⟶ a_* a^{-1} E is an isomorphism, a^{-1} being restriction along j_total.

The unit of an adjunction with fully faithful left adjoint is invertible, and a^{-1} is fully faithful by fullyFaithfulInverseImageOver.

theorem isIso_unit_over (hK : IsHypercovering P K) :
    IsIso (totalLocalizationMorphism (P.toGrothendieck.over X) K).adj.unit

CategoryTheory.SimplicialSemiRepresentable.full_abelianInverseImage_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringObjectDescent.lean, line 288. The attribute's comment: “part (2): a^{-1} on abelian sheaves is full”.

Stacks 0D8K (2), the fullness half. The inverse image a^{-1} : Ab(C/X) ⥤ Ab((C/K)_total) of the augmentation is full.

Cover density and local fullness of j_total are statements about the site, so the argument of full_inverseImage_over applies at any coefficient category.

theorem full_abelianInverseImage_over (hK : IsHypercovering P K) :
    ((totalForget K).sheafPushforwardContinuous Ab.{u}
      ((situation (P.toGrothendieck.over X) K).totalTopology)
      (P.toGrothendieck.over X)).Full

CategoryTheory.SimplicialSemiRepresentable.isIso_abelianUnit_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringObjectDescent.lean, line 300. The attribute's comment: “part (2): the unit M = a_*a⁻¹M on abelian sheaves is an isomorphism”.

Stacks 0D8K (2), the degree-zero identification M = a_* a^{-1} M on sheaves of abelian groups: for a hypercovering K of X and every sheaf of abelian groups M on C/X the canonical map M ⟶ a_* a^{-1} M is an isomorphism, a^{-1} being restriction along j_total.

theorem isIso_abelianUnit_over (hK : IsHypercovering P K) :
    IsIso (abelianTotalAdjunction (P.toGrothendieck.over X) K).unit

CategoryTheory.SimplicialSemiRepresentable.isCartesianSheaf_of_mem_essImage_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringObjectDescent.lean, line 314. The attribute's comment: “part (1): the essential image of a^{-1} consists of cartesian sheaves of sets”.

Stacks 0D8K (1), the inclusion of the essential image in the cartesian sheaves. Every sheaf of sets on the total site (C/K)_total isomorphic to an inverse image along the augmentation towards C/X is cartesian.

This is Stacks 0D7H (1) together with invariance of cartesianness under isomorphism, and uses no condition on the simplicial semi-representable object K.

theorem isCartesianSheaf_of_mem_essImage_over (J : GrothendieckTopology C)
    {F : Sheaf (situation (J.over X) K).totalTopology (Type u)}
    (hF : (totalLocalizationMorphism (J.over X) K).inverseImage.essImage F) :
    (situation (J.over X) K).IsCartesianSheaf F

CategoryTheory.SimplicialSemiRepresentable.isCartesianAbSheaf_of_mem_essImage_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringObjectDescent.lean, line 328. The attribute's comment: “part (2): the essential image of a^{-1} consists of cartesian abelian sheaves”.

Stacks 0D8K (2), the inclusion of the essential image in the cartesian sheaves. Every sheaf of abelian groups on the total site (C/K)_total isomorphic to an inverse image along the augmentation towards C/X is cartesian.

Cartesianness of an abelian sheaf is cartesianness of its underlying sheaf of sets, and the underlying sheaf of the restriction of 𝒢 along j_total is the restriction of the underlying sheaf of 𝒢, both being a composition of functors.

theorem isCartesianAbSheaf_of_mem_essImage_over (J : GrothendieckTopology C)
    {F : Sheaf (situation (J.over X) K).totalTopology Ab.{u}}
    (hF : ((totalForget K).sheafPushforwardContinuous Ab.{u}
      ((situation (J.over X) K).totalTopology) (J.over X)).essImage F) :
    (situation (J.over X) K).IsCartesianAbSheaf F

CategoryTheory.SimplicialSemiRepresentable.essImage_of_isCartesianSheaf_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringSituationDescent.lean, line 159. The attribute's comment: “part (1): every cartesian sheaf of sets on the total site is an a^{-1}E”.

Stacks 0D8K (1), essential surjectivity onto the cartesian sheaves of sets, for restriction along the localization functor j_total of a hypercovering K of an object X: every cartesian sheaf of sets on the total site is isomorphic to a restriction of a sheaf on C/X.

A hypercovering of X in C is a hypercovering of the final presheaf of the localized site C/X with the same simplicial object, by Stacks.CategoryTheory.Hypercovering.exists_hypercoveringOfTerminal_over_of_isHypercovering, and hence has the same total site, total topology and localization morphism; so this is Stacks 0D8E (1) read over C/X. The hypercovering that identification produces is one for the pretopology of covering families of C/X, which generates the localized topology P.toGrothendieck.over X itself by the Galois insertion between pretopologies and topologies; the sheaf is quantified inside the statement because its category depends on that topology.

theorem essImage_of_isCartesianSheaf_over (hK : IsHypercovering P K) :
    ∀ E : Sheaf (situation (P.toGrothendieck.over X) K).totalTopology (Type u),
      (situation (P.toGrothendieck.over X) K).IsCartesianSheaf E →
        (totalLocalizationMorphism (P.toGrothendieck.over X) K).inverseImage.essImage E

CategoryTheory.SimplicialSemiRepresentable.mem_essImage_inverseImage_iff_isCartesianSheaf_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringSituationDescent.lean, line 176. The attribute's comment: “part (1): the essential image of a^{-1} on sheaves of sets is exactly the cartesian sheaves of sets”.

Stacks 0D8K (1), the essential image is exactly the cartesian sheaves of sets, for restriction along j_total for a hypercovering of an object X. One inclusion is isCartesianSheaf_of_mem_essImage_over, which is Stacks 0D7H (1) and uses no condition on K; the other is essImage_of_isCartesianSheaf_over.

theorem mem_essImage_inverseImage_iff_isCartesianSheaf_over (hK : IsHypercovering P K)
    (E : Sheaf (situation (P.toGrothendieck.over X) K).totalTopology (Type u)) :
    (totalLocalizationMorphism (P.toGrothendieck.over X) K).inverseImage.essImage E ↔
      (situation (P.toGrothendieck.over X) K).IsCartesianSheaf E

CategoryTheory.SimplicialSemiRepresentable.isIso_counit_app_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringSituationDescent.lean, line 190. The attribute's comment: “part (1): a^{-1} a_* F = F for cartesian F on sheaves of sets”.

Stacks 0D8K (1), a_* is a quasi-inverse on the cartesian sheaves of sets. For a cartesian sheaf of sets F on the total site of a hypercovering of an object X the counit a⁻¹ a_* F ⟶ F is an isomorphism.

a⁻¹ is fully faithful, so its counit is invertible at exactly the objects of its essential image, and essImage_of_isCartesianSheaf_over puts F there.

theorem isIso_counit_app_over (hK : IsHypercovering P K)
    (E : Sheaf (situation (P.toGrothendieck.over X) K).totalTopology (Type u))
    (hE : (situation (P.toGrothendieck.over X) K).IsCartesianSheaf E) :
    IsIso ((totalLocalizationMorphism (P.toGrothendieck.over X) K).adj.counit.app E)

CategoryTheory.SimplicialSemiRepresentable.essImage_situationTotalInverseImage_of_isCartesianSheaf_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringSituationDescent.lean, line 223. The attribute's comment: “part (1): every cartesian sheaf of sets is an a^{-1}E for the a of Stacks 0D70 at the simplicial-site situation of C/X”.

Stacks 0D8K (1), essential surjectivity onto the cartesian sheaves of sets, for the inverse image of the total augmentation as Stacks 0D70 constructs it from the simplicial-site situation of C/X.

By Stacks 0D8B that inverse image is restriction along j_total, for which every cartesian sheaf of sets is an inverse image by essImage_of_isCartesianSheaf_over; the essential image is invariant under isomorphism of functors.

theorem essImage_situationTotalInverseImage_of_isCartesianSheaf_over (hK : IsHypercovering P K)
    (E : Sheaf (situation (P.toGrothendieck.over X) K).totalTopology (Type u))
    (hE : (situation (P.toGrothendieck.over X) K).IsCartesianSheaf E) :
    (Augmentation.totalMorphismOfTopoi
      (situation (P.toGrothendieck.over X) K) (Cat.of (Over X)) (P.toGrothendieck.over X)
      (situationAugmentation (P.toGrothendieck.over X) K)).inverseImage.essImage E

CategoryTheory.SimplicialSemiRepresentable.mem_essImage_situationTotalInverseImage_iff_isCartesianSheaf_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringSituationDescent.lean, line 241. The attribute's comment: “part (1): the essential image of the a^{-1} of Stacks 0D70 at the simplicial-site situation of C/X is exactly the cartesian sheaves of sets”.

Stacks 0D8K (1), the essential image is exactly the cartesian sheaves of sets, for the inverse image of the morphism of topoi of Stacks 0D70 at the simplicial-site situation of C/X. One inclusion is mem_essImage_inverseImage_iff_isCartesianSheaf_over carried across Stacks 0D8B, the other is essImage_situationTotalInverseImage_of_isCartesianSheaf_over.

theorem mem_essImage_situationTotalInverseImage_iff_isCartesianSheaf_over
    (hK : IsHypercovering P K)
    (E : Sheaf (situation (P.toGrothendieck.over X) K).totalTopology (Type u)) :
    (Augmentation.totalMorphismOfTopoi
        (situation (P.toGrothendieck.over X) K) (Cat.of (Over X)) (P.toGrothendieck.over X)
        (situationAugmentation (P.toGrothendieck.over X) K)).inverseImage.essImage E ↔
      (situation (P.toGrothendieck.over X) K).IsCartesianSheaf E

CategoryTheory.SimplicialSemiRepresentable.essImage_of_isCartesianAbSheaf_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringSituationDescentAb.lean, line 179. The attribute's comment: “part (2): every cartesian abelian sheaf on the total site is an a^{-1}G”.

For a hypercovering L of an object X, every cartesian sheaf of abelian groups on the total site is isomorphic to the restriction along the localization functor j_total of a sheaf of abelian groups on C/X.

theorem essImage_of_isCartesianAbSheaf_over (hL : IsHypercovering P L) :
    ∀ G : Sheaf (situation (P.toGrothendieck.over X) L).totalTopology Ab.{u},
      (situation (P.toGrothendieck.over X) L).IsCartesianAbSheaf G →
        ((totalForget L).sheafPushforwardContinuous Ab.{u}
          ((situation (P.toGrothendieck.over X) L).totalTopology)
          (P.toGrothendieck.over X)).essImage G

CategoryTheory.SimplicialSemiRepresentable.mem_essImage_abelianInverseImage_iff_isCartesianAbSheaf_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringSituationDescentAb.lean, line 196. The attribute's comment: “part (2): the essential image of a^{-1} on abelian sheaves is exactly the cartesian abelian sheaves”.

For a hypercovering L of an object X, the essential image of restriction of abelian sheaves along j_total is exactly the cartesian abelian sheaves.

theorem mem_essImage_abelianInverseImage_iff_isCartesianAbSheaf_over (hL : IsHypercovering P L)
    (G : Sheaf (situation (P.toGrothendieck.over X) L).totalTopology Ab.{u}) :
    ((totalForget L).sheafPushforwardContinuous Ab.{u}
        ((situation (P.toGrothendieck.over X) L).totalTopology)
        (P.toGrothendieck.over X)).essImage G ↔
      (situation (P.toGrothendieck.over X) L).IsCartesianAbSheaf G

CategoryTheory.SimplicialSemiRepresentable.isIso_abelianCounit_app_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringSituationDescentAb.lean, line 208. The attribute's comment: “part (2): a^{-1} a_* F = F for cartesian F on abelian sheaves”.

For a cartesian sheaf of abelian groups ℱ on the total site of a hypercovering of an object X, the counit a⁻¹ a_* ℱ ⟶ ℱ is an isomorphism.

theorem isIso_abelianCounit_app_over (hL : IsHypercovering P L)
    (G : Sheaf (situation (P.toGrothendieck.over X) L).totalTopology Ab.{u})
    (hG : (situation (P.toGrothendieck.over X) L).IsCartesianAbSheaf G) :
    IsIso ((abelianTotalAdjunction (P.toGrothendieck.over X) L).counit.app G)

CategoryTheory.SimplicialSemiRepresentable.essImage_situationTotalInverseImageAb_of_isCartesianAbSheaf_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringSituationDescentAb.lean, line 221. The attribute's comment: “part (2): every cartesian abelian sheaf is an a^{-1}G for the a of Stacks 0D70 at the simplicial-site situation of C/X”.

For a hypercovering L of an object X, every cartesian abelian sheaf on the total site lies in the essential image of the abelian inverse image of the total augmentation which Stacks 0D70 constructs from the simplicial-site situation of C/X.

theorem essImage_situationTotalInverseImageAb_of_isCartesianAbSheaf_over
    (hL : IsHypercovering P L)
    (G : Sheaf (situation (P.toGrothendieck.over X) L).totalTopology Ab.{u})
    (hG : (situation (P.toGrothendieck.over X) L).IsCartesianAbSheaf G) :
    (Augmentation.totalInverseImageAb (situation (P.toGrothendieck.over X) L)
      (Cat.of (Over X)) (P.toGrothendieck.over X)
      (situationAugmentation (P.toGrothendieck.over X) L)).essImage G

CategoryTheory.SimplicialSemiRepresentable.mem_essImage_situationTotalInverseImageAb_iff_isCartesianAbSheaf_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringSituationDescentAb.lean, line 237. The attribute's comment: “part (2): the essential image of the a^{-1} of Stacks 0D70 at the simplicial-site situation of C/X is exactly the cartesian abelian sheaves”.

For a hypercovering L of an object X, the essential image of the abelian inverse image of the morphism of topoi of Stacks 0D70 at the simplicial-site situation of C/X is exactly the cartesian abelian sheaves.

theorem mem_essImage_situationTotalInverseImageAb_iff_isCartesianAbSheaf_over
    (hL : IsHypercovering P L)
    (G : Sheaf (situation (P.toGrothendieck.over X) L).totalTopology Ab.{u}) :
    (Augmentation.totalInverseImageAb (situation (P.toGrothendieck.over X) L)
        (Cat.of (Over X)) (P.toGrothendieck.over X)
        (situationAugmentation (P.toGrothendieck.over X) L)).essImage G ↔
      (situation (P.toGrothendieck.over X) L).IsCartesianAbSheaf G

CategoryTheory.SimplicialSemiRepresentable.isIso_situationTotalAdjunctionUnit_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringUnit.lean, line 383. The attribute's comment: “part (1): the unit E = a_*a⁻¹E of the morphism of topoi of Stacks 0D70 on sheaves of sets is an isomorphism”.

Stacks 0D8K (1), the degree-zero identification E = a_* a^{-1} E, for the morphism of topoi which Stacks 0D70 attaches to the simplicial-site situation of a hypercovering K of an object X: for every sheaf of sets E on C/X the canonical map E ⟶ a_* a^{-1} E is an isomorphism, with no condition carried beyond K being a hypercovering of X.

This is the comparison isIso_situationTotalAdjunctionUnit_of_isIso_unit at the site C/X, applied to isIso_unit_over.

theorem isIso_situationTotalAdjunctionUnit_over (hK : IsHypercovering P K) :
    IsIso (SimplicialSiteSituation.Augmentation.totalMorphismOfTopoi
      (situation (P.toGrothendieck.over X) K) (Cat.of (Over X)) (P.toGrothendieck.over X)
      (situationAugmentation (P.toGrothendieck.over X) K)).adj.unit

CategoryTheory.SimplicialSemiRepresentable.isIso_situationAbelianTotalAdjunctionUnit_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringUnit.lean, line 400. The attribute's comment: “part (2): the unit M = a_*a⁻¹M of the morphism of topoi of Stacks 0D70 on abelian sheaves is an isomorphism”.

Stacks 0D8K (2), the degree-zero identification M = a_* a^{-1} M on sheaves of abelian groups, for the morphism of topoi which Stacks 0D70 attaches to the simplicial-site situation of a hypercovering K of an object X: for every sheaf of abelian groups M on C/X the canonical map M ⟶ a_* a^{-1} M is an isomorphism, with no condition carried beyond K being a hypercovering of X.

This is the spelling of the unit which the derived statements of Stacks 0D8L consume, and it discharges the clause those statements would otherwise carry as a hypothesis.

theorem isIso_situationAbelianTotalAdjunctionUnit_over (hK : IsHypercovering P K) :
    IsIso (SimplicialSiteSituation.Augmentation.abelianTotalAdjunction
      (situation (P.toGrothendieck.over X) K) (Cat.of (Over X)) (P.toGrothendieck.over X)
      (situationAugmentation (P.toGrothendieck.over X) K)).unit

Tag 0D8L, a lemma

Tag 0D8L in the Stacks Project.

CategoryTheory.SimplicialSemiRepresentable.isIso_derivedAugmentationUnitOver_app_of_isHypercovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObjectDerivedPushforwardUnconditional.lean, line 205. The attribute's comment: “for a hypercovering K of X by semi-representable objects, with the Ra_-acyclicity of a⁻¹ of a K-injective complex taken as an explicit input; the degree-zero identification M = a_a⁻¹M is discharged here from the hypercovering conditions, being Tag 0D8K part (2). The acyclicity is discharged, and this tag carried unconditionally, by ...SimplicialSemiRepresentable .isIso_derivedAugmentationUnitOver_app_of_isHypercovering_unconditional”.

Stacks Project, Tag 0D8L, granted the one input this library does not have. For a site C with fibre products, an object X of C and a hypercovering K of X by semi-representable objects, the canonical map E ⟶ Ra_* a^{-1} E is an isomorphism for every object E of the unbounded derived category of abelian sheaves on C/X.

E is arbitrary: no boundedness is assumed and the coefficients are all abelian sheaves.

Of the two inputs carried by isIso_derivedAugmentationUnitOver_app, the first is discharged here from the hypercovering conditions on K alone, by isIso_homotopyAugmentationUnitOver_of_isHypercovering; that theorem states the same invertibility for an arbitrary K and so has to carry it. What remains is hacyclic, that the direct image of a^{-1} of a K-injective complex needs no derivation, that is, that R^p a_* a^{-1} vanishes in positive degrees; the source reads that off the spectral sequence of Stacks 0D7A, which this library builds but without the convergence to R^{p+q} a_* that the reading needs. It is asked only at the K-injective complexes, which is where the source's argument supplies it. No unconditional invertibility is claimed.

theorem isIso_derivedAugmentationUnitOver_app_of_isHypercovering (hK : IsHypercovering P K)
    (hacyclic : ∀ I : CochainComplex (AbelianSheavesOver P.toGrothendieck X) ℤ,
      I.IsKInjective →
        IsIso ((derivedAbelianTotalPushforwardOverUnit P.toGrothendieck X K).app
          (((abelianTotalInverseImageOver P.toGrothendieck X K).mapHomotopyCategory
            (ComplexShape.up ℤ)).obj
              ((HomotopyCategory.quotient (AbelianSheavesOver P.toGrothendieck X)
                (ComplexShape.up ℤ)).obj I))))
    (E : DerivedCategory (AbelianSheavesOver P.toGrothendieck X)) :
    IsIso ((derivedAugmentationUnitOver P.toGrothendieck X K).app E)

CategoryTheory.SimplicialSemiRepresentable.isIso_derivedAugmentationUnitOver_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringObjectDerivedPushforward.lean, line 370. The attribute's comment: “granted two inputs this library does not have: the degree-zero identification M = a_a⁻¹M, which is the unproved clause of Tag 0D8K, and the vanishing of R^p a_ a⁻¹ in positive degrees; the isomorphism is not proved unconditionally”.

Stacks Project, Tag 0D8L, granted its two inputs. For a simplicial semi-representable object K over an object X of a site with fibre products, the canonical map E ⟶ Ra_* a^{-1} E is an isomorphism for every E of D(C/X) — as soon as, at every complex of abelian sheaves on C/X, the ordinary augmentation unit is invertible and the direct image of its inverse image needs no derivation.

These are the two steps of the source's argument for cohomological descent, and this reduces that argument to them. Neither is discharged in this library, so both are carried as hypotheses and the invertibility is not proved unconditionally.

theorem isIso_derivedAugmentationUnitOver_app
    (hunit : ∀ M, IsIso ((homotopyAugmentationUnitOver J X K).app M))
    (hacyclic : ∀ M, IsIso ((derivedAbelianTotalPushforwardOverUnit J X K).app
      (((abelianTotalInverseImageOver J X K).mapHomotopyCategory
        (ComplexShape.up ℤ)).obj M)))
    (E : DerivedCategory (AbelianSheavesOver J X)) :
    IsIso ((derivedAugmentationUnitOver J X K).app E)

CategoryTheory.SimplicialSemiRepresentable.isIso_derivedAugmentationUnitOver_app_of_isHypercovering_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringObjectDerivedPushforwardUnconditional.lean, line 140.

For a hypercovering K of an object X of a site C with fibre products, the canonical map E ⟶ Ra_* a⁻¹ E is invertible at every object E of the unbounded derived category of abelian sheaves on C/X.

theorem isIso_derivedAugmentationUnitOver_app_of_isHypercovering_unconditional
    (P : Pretopology C) {X : C} (K : SimplicialObject (FormalCoproduct.{u} (Over X)))
    (hK : IsHypercovering P K)
    (E : DerivedCategory (AbelianSheavesOver P.toGrothendieck X)) :
    IsIso ((derivedAugmentationUnitOver P.toGrothendieck X K).app E)

Tag 09X7, a lemma

Tag 09X7 in the Stacks Project.

CategoryTheory.SimplicialSemiRepresentable.derivedGlobalSectionsInverseImageIsoOver, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringObjectDerivedDescent.lean, line 159. The attribute's comment: “RESTRICTED: granted the two inputs of Tag 0D8L — the underived unit F = a_a⁻¹F and the Ra_-acyclicity of a⁻¹ of a K-injective complex — and the underived identity Γ(C/X, a_*F) = Γ(total, F); stated for every simplicial semi-representable object over X, hence for a hypercovering of X”.

Stacks 09X7, granted the inputs the library does not have. For a site C with fibre products, an object X of C, a simplicial semi-representable object K over X — in particular a hypercovering of X — and the augmentation a : Sh((C/K)_total) ⟶ Sh(C/X) of Stacks 0D8B read over the slice site, derived global sections over X are derived global sections on the total site of the inverse image:

RΓ(X, E) = RΓ((C/K)_total, a⁻¹E).

The statement is an isomorphism of functors on the unbounded derived category of abelian sheaves on C/X, so it holds at every object E of D(C/X) with no boundedness assumption, which is the form the source states.

Three hypotheses are carried. hunit and hacyclic are the two inputs of Stacks 0D8L, the statement over C/X of what Stacks 0D8G states over C: the first is the degree-zero identification of Stacks 0D8K, that the underived unit F ⟶ a_*a⁻¹F is an isomorphism, and the second is that a⁻¹ of a K-injective complex computes Ra_*. hΓ is the underived identity Γ(C/X, a_*F) = Γ((C/K)_total, F) on which the factorisation of Stacks 08J6 rests. The derived content of Stacks 08J6 is not assumed: see the module docstring.

def derivedGlobalSectionsInverseImageIsoOver
    (hunit : IsIso (Augmentation.abelianTotalAdjunction (situationOver P K) (Cat.of (Over X))
      (P.toGrothendieck.over X) (augmentationOver P K)).unit)
    (hacyclic : Augmentation.InverseImageComputesDerivedPushforward (situationOver P K)
      (Cat.of (Over X)) (P.toGrothendieck.over X) (augmentationOver P K))
    (hΓ : Augmentation.abelianTotalPushforward (situationOver P K) (Cat.of (Over X))
          (P.toGrothendieck.over X) (augmentationOver P K) ⋙
        Sheaf.Γ (P.toGrothendieck.over X) AddCommGrpCat.{u} ≅
      Sheaf.Γ (situationOver P K).totalTopology AddCommGrpCat.{u}) :
    Augmentation.derivedGlobalSectionsBase (Cat.of (Over X)) (P.toGrothendieck.over X) ≅
      Augmentation.derivedTotalInverseImage (situationOver P K) (Cat.of (Over X))
          (P.toGrothendieck.over X) (augmentationOver P K) ⋙
        Augmentation.derivedGlobalSectionsTotal (situationOver P K)

CategoryTheory.SimplicialSemiRepresentable.derivedGlobalSectionsInverseImageIsoOverOfHypercovering, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringObjectDerivedDescentUnconditional.lean, line 88.

Let C be a site with fibre products, X an object of C, K a hypercovering of X and a : Sh((C/K)_total) ⟶ Sh(C/X) the augmentation of the simplicial family of sites n ↦ (C/X)/K_n. Derived global sections over X are derived global sections on the total site of the inverse image:

RΓ(X, E) = RΓ((C/K)_total, a⁻¹E),

as an isomorphism of functors on the unbounded derived category of abelian sheaves on C/X.

def derivedGlobalSectionsInverseImageIsoOverOfHypercovering :
    Augmentation.derivedGlobalSectionsBase (Cat.of (Over X)) (P.toGrothendieck.over X) ≅
      Augmentation.derivedTotalInverseImage (situationOver P K) (Cat.of (Over X))
          (P.toGrothendieck.over X) (augmentationOver P K) ⋙
        Augmentation.derivedGlobalSectionsTotal (situationOver P K)

Tag 0D8M, a lemma

Tag 0D8M in the Stacks Project.

CategoryTheory.SimplicialSemiRepresentable.derivedCategoryBPlus_derivedTotalInverseImageOver_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/ObjectDerivedBoundedBelowFunctors.lean, line 188. The attribute's comment: “the first half of the well-definedness clause only: a⁻¹ sends D⁺(C/X) into D⁺_𝒜((C/K)_total); the equivalence itself is not proved”.

Stacks Project, Tag 0D8M, the first half of the well-definedness clause. For a site C with fibre products, an object X of C, a simplicial semi-representable object K over X — in particular a hypercovering of X — and the augmentation a : Sh((C/K)_total) ⟶ Sh(C/X) of Stacks 0D8B read over the slice site, the derived inverse image sends D⁺(C/X) into D⁺_𝒜((C/K)_total): it preserves boundedness below, and its cohomology sheaves are cartesian by isCartesianAbSheaf_homology_derivedTotalInverseImageOver_obj.

This is the clause of Stacks 0D8M which says that the functor whose invertibility the source asserts is defined at all. The invertibility is not proved here.

theorem derivedCategoryBPlus_derivedTotalInverseImageOver_obj
    (E : DerivedCategory (Sheaf (P.toGrothendieck.over X) AddCommGrpCat.{u}))
    (hE : DerivedCategoryB.IsBoundedBelow E) :
    derivedPlusCartesianOver P K
      ((Augmentation.derivedTotalInverseImage (situationOver P K) (Cat.of (Over X))
        (P.toGrothendieck.over X) (augmentationOver P K)).obj E)

CategoryTheory.SimplicialSemiRepresentable.derivedCategoryBPlus_derivedTotalPushforwardOver_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/ObjectDerivedBoundedBelowFunctors.lean, line 205. The attribute's comment: “the second half of the well-definedness clause only: Ra_* sends D⁺_𝒜((C/K)_total) into D⁺(C/X); the equivalence itself is not proved”.

Stacks Project, Tag 0D8M, the second half of the well-definedness clause. In the same situation the derived direct image sends D⁺_𝒜((C/K)_total) into D⁺(C/X). Only boundedness below is at stake, the weak Serre subcategory on C/X being all of Ab(C/X).

This is the clause of Stacks 0D8M which says that the quasi-inverse the source names is defined at all. That it is a quasi-inverse is not proved here.

theorem derivedCategoryBPlus_derivedTotalPushforwardOver_obj
    (E : DerivedCategory (Sheaf (situationOver P K).totalTopology AddCommGrpCat.{u}))
    (hE : DerivedCategoryB.IsBoundedBelow E) :
    derivedPlusBaseOver P X
      ((Augmentation.derivedTotalPushforward (situationOver P K) (Cat.of (Over X))
        (P.toGrothendieck.over X) (augmentationOver P K)).obj E)

CategoryTheory.SimplicialSemiRepresentable.derivedTotalInverseImageEquivalenceOver, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringObjectDerivedDescent.lean, line 223. The attribute's comment: “RESTRICTED: granted the two inputs of Tag 0D8L — the underived unit F = a_a⁻¹F and the Ra_-acyclicity of a⁻¹ of a K-injective complex — and the essential surjectivity clause of Tag 0D8K (2); stated for every simplicial semi-representable object over X, hence for a hypercovering of X”.

Stacks 0D8M, granted the inputs the library does not have. For a site C with fibre products, an object X of C, a simplicial semi-representable object K over X — in particular a hypercovering of X — the augmentation a of Stacks 0D8B read over the slice site C/X, and the weak Serre subcategory 𝒜 ⊂ Ab((C/K)_total) of cartesian abelian sheaves of Stacks 0D7J, the derived inverse image is an equivalence

a⁻¹ : D⁺(C/X) ⟶ D⁺_𝒜((C/K)_total)

with quasi-inverse Ra_*. Both functors of the equivalence are the restrictions of a⁻¹ and of Ra_* on the nose, since the equivalence is the restricted adjunction; for the forward functor this is derivedTotalInverseImageEquivalenceOver_functor.

Three hypotheses are carried. hunit and hacyclic are the two inputs of Stacks 0D8L, the statement over C/X of what Stacks 0D8G states over C. hsurj is the remaining clause of Stacks 0D8K (2), that every cartesian abelian sheaf on the total site lies in the essential image of a⁻¹. The derived content — that both functors restrict to the bounded below subcategories, that the cohomology sheaves of a⁻¹E are cartesian, and the propagation of the counit from 𝒜 to all of D⁺_𝒜 — is not assumed.

def derivedTotalInverseImageEquivalenceOver :
    (DerivedCategoryB.derivedCategoryBPlus
        (⊤ : ObjectProperty
          (Sheaf (P.toGrothendieck.over X) AddCommGrpCat.{u}))).FullSubcategory ≌
      (DerivedCategoryB.derivedCategoryBPlus
        ((situationOver P K).IsCartesianAbSheaf)).FullSubcategory

CategoryTheory.SimplicialSemiRepresentable.derivedTotalInverseImageEquivalenceOver_functor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringObjectDerivedDescent.lean, line 240. The attribute's comment: “RESTRICTED: the forward functor of the equivalence is a⁻¹, for the equivalence built granted the two inputs of Tag 0D8L and the essential surjectivity clause of Tag 0D8K (2)”.

Stacks 0D8M, the forward functor of the equivalence is a⁻¹: it is the restriction of the derived inverse image to the bounded below subcategories.

theorem derivedTotalInverseImageEquivalenceOver_functor :
    (derivedTotalInverseImageEquivalenceOver P K hunit hacyclic hsurj).functor =
      Augmentation.derivedTotalInverseImagePlus (situationOver P K) (Cat.of (Over X))
        (P.toGrothendieck.over X) (augmentationOver P K)

CategoryTheory.SimplicialSemiRepresentable.derivedTotalInverseImageEquivalenceOverOfHypercovering, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringObjectDerivedDescentUnconditional.lean, line 107.

Let C be a site with fibre products, X an object of C, K a hypercovering of X, a the augmentation of the simplicial family of sites n ↦ (C/X)/K_n, and 𝒜 ⊂ Ab((C/K)_total) the weak Serre subcategory of cartesian abelian sheaves. The derived inverse image is an equivalence

a⁻¹ : D⁺(C/X) ⟶ D⁺_𝒜((C/K)_total)

with quasi-inverse Ra_*.

def derivedTotalInverseImageEquivalenceOverOfHypercovering :
    (DerivedCategoryB.derivedCategoryBPlus
        (⊤ : ObjectProperty
          (Sheaf (P.toGrothendieck.over X) AddCommGrpCat.{u}))).FullSubcategory ≌
      (DerivedCategoryB.derivedCategoryBPlus
        ((situationOver P K).IsCartesianAbSheaf)).FullSubcategory

CategoryTheory.SimplicialSemiRepresentable.derivedTotalInverseImageEquivalenceOverOfHypercovering_functor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringObjectDerivedDescentUnconditional.lean, line 122. The attribute's comment: “the forward functor of the equivalence is a⁻¹”.

The forward functor of derivedTotalInverseImageEquivalenceOverOfHypercovering is the restriction of the derived inverse image a⁻¹ to the bounded below subcategories.

theorem derivedTotalInverseImageEquivalenceOverOfHypercovering_functor :
    (derivedTotalInverseImageEquivalenceOverOfHypercovering P K hK).functor =
      Augmentation.derivedTotalInverseImagePlus (situationOver P K) (Cat.of (Over X))
        (P.toGrothendieck.over X) (augmentationOver P K)

CategoryTheory.SimplicialSemiRepresentable.derivedTotalInverseImageEquivalenceOverOfHypercovering_inverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringObjectDerivedDescentUnconditional.lean, line 132. The attribute's comment: “the quasi-inverse of the equivalence is Ra_*”.

The quasi-inverse of derivedTotalInverseImageEquivalenceOverOfHypercovering is the restriction of the derived direct image Ra_* to the bounded below subcategories.

theorem derivedTotalInverseImageEquivalenceOverOfHypercovering_inverse :
    (derivedTotalInverseImageEquivalenceOverOfHypercovering P K hK).inverse =
      Augmentation.derivedTotalPushforwardPlus (situationOver P K) (Cat.of (Over X))
        (P.toGrothendieck.over X) (augmentationOver P K)

Sources

LeanStacks.Topology.LocallyQuasiCompactQcSite.mem_essImage_iff_isCartesianSheaf_qcAugmentation · Stacks.Topology.LocallyQuasiCompactQcSite.mem_essImage_iff_isCartesianAbSheaf_qcAugmentation · CategoryTheory.SimplicialSemiRepresentable.faithful_inverseImage_over · CategoryTheory.SimplicialSemiRepresentable.faithful_totalInverseImage_over · CategoryTheory.SimplicialSemiRepresentable.faithful_abelianInverseImage_over · CategoryTheory.SimplicialSemiRepresentable.full_inverseImage_over · CategoryTheory.SimplicialSemiRepresentable.isIso_unit_over · CategoryTheory.SimplicialSemiRepresentable.full_abelianInverseImage_over

Section85.20 Cohomological descent for hypercoverings of an object: modules #

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

Tag 0DA4, a lemma

Tag 0DA4 in the Stacks Project.

CategoryTheory.SimplicialSemiRepresentable.faithful_pullbackModules_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringObjectModuleDescent.lean, line 290. The attribute's comment: “a^ on sheaves of modules is faithful. The essential-image inclusion is isCartesianModule_of_mem_essImage_over; fullness of a^, and essential surjectivity onto the cartesian O-modules making a_* a quasi-inverse, are not proved”.

Stacks 0DA4, the faithfulness half. Let C be a site with fibre products, X an object of it, O_C a sheaf of commutative rings on C and K a hypercovering of X. With O_X = O_C|_{C/X} and O = a⁻¹O_X, the pullback a^* : Mod(O_X) ⥤ Mod(O) of sheaves of modules along the augmentation of the total site of K over C/X is faithful.

theorem faithful_pullbackModules_over (hK : IsHypercovering P K) :
    (hypercoveringObjectRingedAugmentation P K
      OC).totalRingedHom.toModulesHom.pullbackModules.Faithful

CategoryTheory.SimplicialSemiRepresentable.isCartesianModule_of_mem_essImage_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringObjectModuleDescent.lean, line 306. The attribute's comment: “the essential image of a^ consists of cartesian O-modules. Faithfulness of a^ is faithful_pullbackModules_over; fullness of a^, and essential surjectivity onto the cartesian O-modules making a_ a quasi-inverse, are not proved”.

Stacks 0DA4, the inclusion of the essential image in the cartesian modules. In the situation above, every sheaf of O-modules on the total site isomorphic to a pullback a^*F is a cartesian O-module.

This is Stacks 0D7H (3) together with invariance of the cartesian condition under isomorphism, and uses no condition on K.

theorem isCartesianModule_of_mem_essImage_over
    {F : SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf
      (J := (situation (P.toGrothendieck.over X) K).totalTopology))
      (hypercoveringObjectRingedAugmentation P K OC).O)}
    (hF : (hypercoveringObjectRingedAugmentation P K
      OC).totalRingedHom.toModulesHom.pullbackModules.essImage F) :
    (situation (P.toGrothendieck.over X) K).IsModuleFiberTransitionIso
      (hypercoveringObjectRingedAugmentation P K OC).O F

CategoryTheory.SimplicialSemiRepresentable.full_pullbackModules_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringObjectModuleDescent.lean, line 324. The attribute's comment: “a^* on sheaves of modules is full”.

Stacks 0DA4, the fullness half. In the situation above, the pullback a^* : Mod(O_X) ⥤ Mod(O) of sheaves of modules is full.

Because the structure map of a is the identification O = a⁻¹O_X, the pullback of modules is the Stacks 03D2 inverse image of modules followed by an equivalence; fullness then descends from Stacks 0D8K (1), full faithfulness of a⁻¹ on sheaves of sets over C/X.

theorem full_pullbackModules_over (hK : IsHypercovering P K) :
    (hypercoveringObjectRingedAugmentation P K
      OC).totalRingedHom.toModulesHom.pullbackModules.Full

CategoryTheory.SimplicialSemiRepresentable.fullyFaithfulPullbackModulesOver, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringObjectModuleDescent.lean, line 334. The attribute's comment: “a^* on sheaves of modules is fully faithful”.

Stacks 0DA4, full faithfulness of a^* on sheaves of modules.

def fullyFaithfulPullbackModulesOver (hK : IsHypercovering P K) :
    (hypercoveringObjectRingedAugmentation P K
      OC).totalRingedHom.toModulesHom.pullbackModules.FullyFaithful

CategoryTheory.SimplicialSemiRepresentable.essImage_pullbackModules_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringObjectModuleDescent.lean, line 348. The attribute's comment: “every cartesian O-module is an a^*M”.

Stacks 0DA4, essential surjectivity onto the cartesian O-modules. In the situation above, every cartesian sheaf of O-modules on the total site is a pullback a^*M.

The underlying sheaf of sets of a cartesian sheaf of modules is cartesian — the structure sheaf itself being cartesian because it is a⁻¹O_X — hence an inverse image by Stacks 0D8K (1); and a sheaf of modules whose underlying sheaf of sets is an inverse image is a pullback.

theorem essImage_pullbackModules_over (hK : IsHypercovering P K)
    {F : SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf
      (J := (situation (P.toGrothendieck.over X) K).totalTopology)
      (hypercoveringObjectRingedAugmentation P K OC).O))}
    (hF : (situation (P.toGrothendieck.over X) K).IsModuleFiberTransitionIso
      (hypercoveringObjectRingedAugmentation P K OC).O F) :
    (hypercoveringObjectRingedAugmentation P K
      OC).totalRingedHom.toModulesHom.pullbackModules.essImage F

CategoryTheory.SimplicialSemiRepresentable.mem_essImage_pullbackModules_iff_isCartesianModule_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringObjectModuleDescent.lean, line 367. The attribute's comment: “the essential image of a^* on sheaves of modules is exactly the cartesian O-modules”.

Stacks 0DA4, the essential image of a^* is exactly the cartesian O-modules. One inclusion is isCartesianModule_of_mem_essImage_over, which is Stacks 0D7H (3); the other is essImage_pullbackModules_over.

theorem mem_essImage_pullbackModules_iff_isCartesianModule_over (hK : IsHypercovering P K)
    (F : SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf
      (J := (situation (P.toGrothendieck.over X) K).totalTopology)
      (hypercoveringObjectRingedAugmentation P K OC).O))) :
    (hypercoveringObjectRingedAugmentation P K
      OC).totalRingedHom.toModulesHom.pullbackModules.essImage F ↔
      (situation (P.toGrothendieck.over X) K).IsModuleFiberTransitionIso
        (hypercoveringObjectRingedAugmentation P K OC).O F

CategoryTheory.SimplicialSemiRepresentable.isIso_pullbackAdjPushforwardModules_unit_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringObjectModuleDescent.lean, line 381. The attribute's comment: “M = a_ a^ M on sheaves of modules”.

Stacks 0DA4, a_* is a quasi-inverse on Mod(O_X). The unit M ⟶ a_*a^*M of the adjunction of Stacks 03D7 is an isomorphism for every sheaf of O_X-modules: a fully faithful left adjoint has invertible unit.

theorem isIso_pullbackAdjPushforwardModules_unit_over (hK : IsHypercovering P K) :
    IsIso (RingedToposHom.pullbackAdjPushforwardModules
      (hypercoveringObjectRingedAugmentation P K OC).totalRingedHom).unit

CategoryTheory.SimplicialSemiRepresentable.isIso_pullbackAdjPushforwardModules_counit_app_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringObjectModuleDescent.lean, line 396. The attribute's comment: “a^ a_ F = F for a cartesian O-module F”.

Stacks 0DA4, a_* is a quasi-inverse on the cartesian O-modules. The counit a^*a_*F ⟶ F of the adjunction of Stacks 03D7 is an isomorphism at every cartesian sheaf of O-modules: a fully faithful left adjoint has invertible counit exactly on its essential image, which by mem_essImage_pullbackModules_iff_isCartesianModule_over is the cartesian O-modules.

theorem isIso_pullbackAdjPushforwardModules_counit_app_over (hK : IsHypercovering P K)
    {F : SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf
      (J := (situation (P.toGrothendieck.over X) K).totalTopology)
      (hypercoveringObjectRingedAugmentation P K OC).O))}
    (hF : (situation (P.toGrothendieck.over X) K).IsModuleFiberTransitionIso
      (hypercoveringObjectRingedAugmentation P K OC).O F) :
    IsIso ((RingedToposHom.pullbackAdjPushforwardModules
      (hypercoveringObjectRingedAugmentation P K OC).totalRingedHom).counit.app F)

Tag 0DA5, a lemma

Tag 0DA5 in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.isIso_derivedPullbackPushforwardUnit_app_of_hypercovering_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringModuleCohomologicalDescent.lean, line 399. The attribute's comment: “granted the module form of Tag 0D8E as hunit and the Ra_-acyclicity of a^ of a K-injective complex as hacyclic -- the same two inputs this library's Tag 0DA0, isIso_derivedPullbackPushforwardUnit_app_of_hypercovering, is itself granted”.

Stacks 0DA5. Let C be a site with fibre products, X an object of it, O_C a sheaf of rings and K a hypercovering of X. Writing O_X = O_C|_{C/X} and a for the augmentation of the total site of K over the slice site C/X, the canonical map E ⟶ Ra_*La^*E is an isomorphism for every E in the derived category of O_X-modules.

The slice site C/X has a terminal object and inherits fibre products from C, so it has all finite limits; this is why the source asks only for fibre products on C here, where Stacks 0DA0 asks for equalizers as well. The augmentation is the ringed one of Stacks 0D9X, and the two pinning lemmas hypercoveringObjectRingedAugmentation_augmentationRingedTopos_J and _O certify that the coefficients are the sheaves of O_X-modules on C/X. The hypercovering condition on K is recorded as hK, and, exactly as in Stacks 0DA0, it is absorbed into the two deferred inputs rather than consumed directly.

theorem isIso_derivedPullbackPushforwardUnit_app_of_hypercovering_over
    (_hK : IsHypercovering P K)
    (hunit : IsIso (AlgebraicGeometry.RingedToposHom.pullbackAdjPushforwardModules
      (hypercoveringObjectRingedAugmentation P K O).totalRingedHom).unit)
    (hacyclic : AlgebraicGeometry.RingedToposHom.PullbackComputesDerivedPushforward.{u}
      (hypercoveringObjectRingedAugmentation P K O).totalRingedHom)
    (E : DerivedCategory (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf (J := (hypercoveringObjectRingedAugmentation P K O).augmentationRingedTopos.J))
      (hypercoveringObjectRingedAugmentation P K O).augmentationRingedTopos.O))) :
    IsIso ((AlgebraicGeometry.RingedToposHom.derivedPullbackPushforwardUnit
      (hypercoveringObjectRingedAugmentation P K O).totalRingedHom).app E)

CategoryTheory.SimplicialSemiRepresentable.isIso_derivedPullbackPushforwardUnit_app_of_isHypercovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringSimplicialObjectModuleCohomologicalDescentUnconditional.lean, line 264.

Stacks 0DA5. Let C be a site with fibre products, X an object of C, O_C a sheaf of commutative rings on C and K a hypercovering of X. With O_X = O_C|_{C/X}, O = a⁻¹O_X on the total site of K and a : (Sh((C/K)_total), O) ⟶ (Sh(C/X), O_X) the ringed augmentation of Stacks 0D9X, the canonical map

E ⟶ R a_* L a^* E

is an isomorphism for every object E of the unbounded derived category D(O_X) of sheaves of O_X-modules.

theorem isIso_derivedPullbackPushforwardUnit_app_of_isHypercovering (hK : IsHypercovering P K)
    (E : DerivedCategory (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf
      (J := (hypercoveringObjectRingedAugmentation P K OC).augmentationRingedTopos.J))
      (hypercoveringObjectRingedAugmentation P K OC).augmentationRingedTopos.O))) :
    IsIso ((AlgebraicGeometry.RingedToposHom.derivedPullbackPushforwardUnit
      (hypercoveringObjectRingedAugmentation P K OC).totalRingedHom).app E)

Tag 0DA6, a lemma

Tag 0DA6 in the Stacks Project.

CategoryTheory.SimplicialSemiRepresentable.derivedModuleSectionsOverObjectIsoOfIsHypercovering, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringObjectModuleDerivedSections.lean, line 321.

Let C be a site with fibre products, given by a pretopology P, let X be an object of C, let O_C be a sheaf of commutative rings on C and let K be a hypercovering of X (a simplicial object of SR(C, X) whose degree-zero family covers X and whose matching maps K_{n+1} ⟶ (cosk_n sk_n K)_{n+1} are covering). With O_X = O_C|_{C/X}, O = a⁻¹O_X on the total site (C/K)_total and a : (Sh((C/K)_total), O) ⟶ (Sh(C/X), O_X) the ringed augmentation, there is a canonical isomorphism

RΓ(X, E) = RΓ((C/K)_total, La^*E)

naturally in E in the unbounded derived category D(O_C). Here RΓ(X, -) is the total right derived functor of sections over X, with values in D(O_C(X)); La^*E is La^* of the restriction of E to C/X (the target of a being (Sh(C/X), O_X)); and RΓ((C/K)_total, -), with values in D(Γ((C/K)_total, O)), is read in D(O_C(X)) through the canonical ring map O_C(X) ⟶ Γ((C/K)_total, O) (totalSectionsRingHom).

def derivedModuleSectionsOverObjectIsoOfIsHypercovering (hK : IsHypercovering P K) :
    derivedModuleSectionsOverObject P X OC ≅
      Stacks.Cohomology.Localization.derivedRestriction (ringedSite P OC) X ⋙
        (RingedToposHom.leftDerivedPullbackOfIsIsoFSharp
          (X := totalTopos P K OC) (Y := sliceTopos P K OC) (augmentationHom P K OC)).functor ⋙
        derivedTotalGlobalSections P K OC ⋙
          (ModuleCat.restrictScalars (totalSectionsRingHom P K OC)).mapDerivedCategory

CategoryTheory.SimplicialSemiRepresentable.derivedModuleSectionsOverObjectIsoOfIsHypercovering_hom_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringObjectModuleDerivedSections.lean, line 337. The attribute's comment: “the forward map of the isomorphism is the canonical one: RΓ(C/X, -) of the derived unit E|_X ⟶ Ra_La^(E|_X), between RΓ(X, E) = RΓ(C/X, E|_X) and the factorisation of Tag 08J6”.

The forward map of derivedModuleSectionsOverObjectIsoOfIsHypercovering at E is RΓ(C/X, -) of the derived unit E|_X ⟶ Ra_*La^*(E|_X) of the ringed augmentation, between the comparison RΓ(X, E) = RΓ(C/X, E|_X) and the factorisation RΓ(C/X, Ra_*-) = RΓ((C/K)_total, -).

theorem derivedModuleSectionsOverObjectIsoOfIsHypercovering_hom_app (hK : IsHypercovering P K)
    (E : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf OC))) :
    (derivedModuleSectionsOverObjectIsoOfIsHypercovering P K OC hK).hom.app E =
      (derivedModuleSectionsOverObjectIsoRestriction P OC).hom.app E ≫
        (derivedModuleSectionsAtId P X OC).map
          ((RingedToposHom.derivedPullbackPushforwardUnit (augmentationHom P K OC)).app
            ((Stacks.Cohomology.Localization.derivedRestriction (ringedSite P OC) X).obj E)) ≫
        (derivedPushforwardModuleSectionsAtIdIso P K OC).hom.app
          ((RingedToposHom.leftDerivedPullbackOfIsIsoFSharp
            (X := totalTopos P K OC) (Y := sliceTopos P K OC) (augmentationHom P K OC)).functor.obj
              ((Stacks.Cohomology.Localization.derivedRestriction (ringedSite P OC) X).obj E))

Tag 0DA7, a lemma

Tag 0DA7 in the Stacks Project.

CategoryTheory.SimplicialSemiRepresentable.exists_derivedPullbackEquivalence_isHypercovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringObjectModuleBoundedBelowDescent.lean, line 84.

Let C be a site with fibre products, given by a pretopology P, let X be an object of C, let O_C be a sheaf of commutative rings on C and let K be a hypercovering of X (Stacks 01G5: a simplicial object of SR(C, X) whose degree-zero family covers X and whose matching maps K_{n+1} ⟶ (cosk_n sk_n K)_{n+1} are covering). Let O_X = O_C|_{C/X}, let O = a⁻¹O_X on the total site (C/K)_total and let a : (Sh((C/K)_total), O) ⟶ (Sh(C/X), O_X) be the ringed augmentation of Remarks 0D9V and 0D9X. Then

the cartesian O-modules form a weak Serre subcategory 𝒜 ⊂ Mod(O), and

the functor La^* defines an equivalence D⁺(O_X) ⟶ D⁺_𝒜(O) with quasi-inverse R a_*: there is an equivalence of categories whose functor, followed by the inclusion of D⁺_𝒜(O), is La^* on D⁺(O_X), and whose inverse, followed by the inclusion of D⁺(O_X), is R a_* on D⁺_𝒜(O).

Here D⁺(O_X) is the full subcategory of bounded below objects of D(O_X), and D⁺_𝒜(O) that of bounded below objects of D(O) all of whose cohomology modules are cartesian. Nothing is assumed beyond the hypotheses of the source; the equivalence is derivedPullbackEquivalenceOfIsHypercovering.

theorem exists_derivedPullbackEquivalence_isHypercovering (hK : IsHypercovering P K) :
    ObjectProperty.IsWeakSerreClass
        ((situation (P.toGrothendieck.over X) K).IsModuleFiberTransitionIso
          (hypercoveringObjectRingedAugmentation P K OC).O) ∧
      ∃ e : (RingedToposHom.derivedPlusTarget (Y := sliceTopos P K OC)).FullSubcategory ≌
          (RingedToposHom.derivedPlusProperty (X := totalTopos P K OC)
            ((situation (P.toGrothendieck.over X) K).IsModuleFiberTransitionIso
              (hypercoveringObjectRingedAugmentation P K OC).O)).FullSubcategory,
        e.functor ⋙ (RingedToposHom.derivedPlusProperty (X := totalTopos P K OC)
            ((situation (P.toGrothendieck.over X) K).IsModuleFiberTransitionIso
              (hypercoveringObjectRingedAugmentation P K OC).O)).ι =
          (RingedToposHom.derivedPlusTarget (Y := sliceTopos P K OC)).ι ⋙
            (RingedToposHom.leftDerivedPullbackOfIsIsoFSharp (X := totalTopos P K OC)
              (Y := sliceTopos P K OC) (augmentationHom P K OC)).functor ∧
        e.inverse ⋙ (RingedToposHom.derivedPlusTarget (Y := sliceTopos P K OC)).ι =
          (RingedToposHom.derivedPlusProperty (X := totalTopos P K OC)
            ((situation (P.toGrothendieck.over X) K).IsModuleFiberTransitionIso
              (hypercoveringObjectRingedAugmentation P K OC).O)).ι ⋙
            Stacks.Cohomology.DerivedPushforward.derivedPushforward (X := totalTopos P K OC)
              (Y := sliceTopos P K OC) (augmentationHom P K OC)

Sources

Section85.21 Hypercovering by a simplicial object of the site #

Section 85.21 of the Stacks Project, Tag 09X8. 6 tags here are carried by 51 declarations of the repository (all in StacksFrontier) and 9 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 09X8, the section

Tag 09X8 in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.IsHypercoveringAugmentation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObject.lean, line 90. The attribute's comment: “the definition of the section: an augmentation of a simplicial object of the site is a hypercovering of X in C when the three displayed families are coverings”.

An augmentation a : U ⟶ X of a simplicial object U of the site given by the pretopology J is a hypercovering of X in C when {U₀ ⟶ X} is a covering, the canonical morphism U₁ ⟶ U₀ ×_X U₀ generates a covering, and the canonical morphism U_{n+1} ⟶ (cosk_n sk_n U)_{n+1} generates a covering for every n ≥ 1, the coskeleton being formed in the slice category C/X.

def IsHypercoveringAugmentation (J : Pretopology C) (U : SimplicialObject C)
    (a : U ⟶ (SimplicialObject.const C).obj X) : Prop

CategoryTheory.SimplicialOver.homEquivCommSq, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObjectTotalSite.lean, line 143. The attribute's comment: “a morphism (φ, f) : V/U_n → W/U_m of (C/U)_total is φ : [m] → [n] and f : V → W with commutative square”.

A morphism V/U_n ⟶ W/U_m of (C/U)_total is a pair (φ, f) of a simplex map φ : [m] ⟶ [n] and a morphism f : V ⟶ W of C such that the square formed with V ⟶ U_n, W ⟶ U_m and f_φ : U_n ⟶ U_m commutes.

def homEquivCommSq (A B : Grothendieck (slices U)) :
    (A ⟶ B) ≃ {p : (A.base ⟶ B.base) × ((A.fiber : Over (U.obj A.base)).left ⟶
        (B.fiber : Over (U.obj B.base)).left) //
      p.2 ≫ (B.fiber : Over (U.obj B.base)).hom = (A.fiber : Over (U.obj A.base)).hom ≫ U.map p.1}

CategoryTheory.SimplicialOver.toAssociatedTotal_comp_totalForget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObjectTotalSite.lean, line 296. The attribute's comment: “the morphism of topoi a is given by the cocontinuous functor V/U_n ↦ V/X: j_total of (C/K)_total is V/U_n ↦ V/X under the identification”.

Under the identification of (C/U)_total with (C/K)_total, the localization functor j_total : (C/K)_total ⥤ C/X is the functor V/U_n ↦ V/X: precomposed with (C/U)_total ⥤ (C/K)_total it is augmentationFunctor on the nose.

theorem toAssociatedTotal_comp_totalForget :
    toAssociatedTotal U a ⋙
        SimplicialSemiRepresentable.totalForget (associatedSimplicialObject.{u} U a) =
      augmentationFunctor U a

CategoryTheory.SimplicialOver.associatedTotalEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObjectTotalSite.lean, line 392. The attribute's comment: “the site (C/U)_total, with objects V/U_n and morphisms (φ, f), is (C/K)_total of Remark 0D8C: the equivalence of categories”.

The equivalence of categories (C/K)_total ≌ (C/U)_total between the total site attached to K and the category whose objects are the V/U_n and whose morphisms are the pairs (φ, f). Its functor is fromAssociatedTotal, and its inverse is toAssociatedTotal by associatedTotalEquivalenceInverseIso.

def associatedTotalEquivalence :
    Grothendieck (SimplicialSemiRepresentable.slices (associatedSimplicialObject.{u} U a)) ≌
      Grothendieck (slices U)

CategoryTheory.SimplicialOver.associatedTotalEquivalence_isDenseSubsite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObjectTotalSite.lean, line 410. The attribute's comment: “the site (C/U)_total is (C/K)_total of Remark 0D8C: the coverings agree”.

The equivalence (C/K)_total ≌ (C/U)_total identifies the topologies: it is a dense subsite inclusion, so a sieve is covering exactly when its image is.

theorem associatedTotalEquivalence_isDenseSubsite :
    (associatedTotalEquivalence U a).functor.IsDenseSubsite
      (associatedTotalTopology U a J) (SimplicialOver.totalTopology J U)

CategoryTheory.SimplicialOver.augmentationPushforwardIsoAssociated, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObjectTotalSite.lean, line 495. The attribute's comment: “the augmentation morphism of topoi a : Sh((C/U)_total) → Sh(C/X): the one of Remark 0D8C and the one of V/U_n ↦ V/X agree, direct images”.

The direct image of the augmentation a : Sh((C/U)_total) ⟶ Sh(C/X) given by V/U_n ↦ V/X is the direct image of the morphism of topoi Sh((C/K)_total) ⟶ Sh(C/X) induced by the total site of K, transported along associatedTotalSheafEquivalence.

def augmentationPushforwardIsoAssociated :
    (augmentationMorphismOfTopoi J U a).pushforward ≅
      (associatedTotalSheafEquivalence U a J).inverse ⋙
        (SimplicialSemiRepresentable.totalLocalizationMorphism (J.over X)
          (associatedSimplicialObject.{u} U a)).pushforward

CategoryTheory.SimplicialOver.augmentationInverseImageIsoAssociated, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObjectTotalSite.lean, line 508. The attribute's comment: “the augmentation morphism of topoi a : Sh((C/U)_total) → Sh(C/X): the one of Remark 0D8C and the one of V/U_n ↦ V/X agree, inverse images”.

The inverse image of the augmentation a : Sh((C/U)_total) ⟶ Sh(C/X) is the inverse image of the morphism of topoi Sh((C/K)_total) ⟶ Sh(C/X) followed by associatedTotalSheafEquivalence.

def augmentationInverseImageIsoAssociated :
    (augmentationMorphismOfTopoi J U a).inverseImage ≅
      (SimplicialSemiRepresentable.totalLocalizationMorphism (J.over X)
          (associatedSimplicialObject.{u} U a)).inverseImage ⋙
        (associatedTotalSheafEquivalence U a J).functor

Declarations registered for the tag:

Stacks.CategoryTheory.Hypercovering.associatedSimplicialObject, declared in the repository, registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObjectTotalSite.lean, line 525 (StacksFrontier): “the simplicial object K of SR(C, X) with K_n = {U_n → X}”.
CategoryTheory.SimplicialSemiRepresentable.totalSituation, declared in the repository, registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObjectTotalSite.lean, line 528 (StacksFrontier): “the simplicial site (C/U)_total obtained from K by Remark 0D8C, that is (C/K)_total”.
CategoryTheory.SimplicialSemiRepresentable.augmentationMorphismOfTopoi, declared in the repository, registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObjectTotalSite.lean, line 532 (StacksFrontier): “the augmentation morphism of topoi a : Sh((C/U)_total) → Sh(C/X) obtained from K by Remark 0D8C”.
CategoryTheory.SimplicialOver.totalTopology, declared in the repository, registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObjectTotalSite.lean, line 536 (StacksFrontier): “the site (C/U)_total with objects V/U_n and morphisms (φ, f): its topology”.
CategoryTheory.SimplicialOver.situation, declared in the repository, registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObjectTotalSite.lean, line 539 (StacksFrontier): “the site (C/U)_total with objects V/U_n and morphisms (φ, f), as a simplicial site”.
CategoryTheory.SimplicialOver.augmentationFunctor, declared in the repository, registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObjectTotalSite.lean, line 543 (StacksFrontier): “the cocontinuous functor V/U_n ↦ V/X”.
CategoryTheory.SimplicialOver.augmentationMorphismOfTopoi, declared in the repository, registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObjectTotalSite.lean, line 546 (StacksFrontier): “the morphism of topoi a : Sh((C/U)_total) → Sh(C/X) given by the cocontinuous functor V/U_n ↦ V/X”.
CategoryTheory.SimplicialOver.augmentationMorphismOfTopoi_pushforward, declared in the repository, registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObjectTotalSite.lean, line 550 (StacksFrontier): “the morphism of topoi a is given by the cocontinuous functor V/U_n ↦ V/X: direct images”.
Stacks.CategoryTheory.Hypercovering.isHypercoveringAugmentation_iff_isHypercovering, declared in the repository, registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObjectTotalSite.lean, line 554 (StacksFrontier): “being a hypercovering of X in C is equivalent to K being a hypercovering of X, Example 0GM9”.

Tag 0DA8, a lemma

Tag 0DA8 in the Stacks Project.

CategoryTheory.SimplicialSemiRepresentable.faithful_inverseImage_augmented, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObject.lean, line 224. The attribute's comment: “part (1): a^{-1} on sheaves of sets is faithful”.

For a hypercovering a : U ⟶ X of X in C the inverse image a^{-1} : Sh(C/X) ⥤ Sh((C/U)_total) of the augmentation is faithful.

theorem faithful_inverseImage_augmented (h : IsHypercoveringAugmentation P U a) :
    (augmentationMorphismOfTopoi P U a).inverseImage.Faithful

CategoryTheory.SimplicialSemiRepresentable.full_inverseImage_augmented, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObject.lean, line 232. The attribute's comment: “part (1): a^{-1} on sheaves of sets is full, carrying local fullness of j_total”.

For a hypercovering a : U ⟶ X of X in C such that j_total is locally full for the topology of C/X, the inverse image a^{-1} : Sh(C/X) ⥤ Sh((C/U)_total) is full.

theorem full_inverseImage_augmented (h : IsHypercoveringAugmentation P U a)
    (hlf : (totalForget (associatedSimplicialObject.{u} U a)).IsLocallyFull
      (P.toGrothendieck.over X)) :
    (augmentationMorphismOfTopoi P U a).inverseImage.Full

CategoryTheory.SimplicialSemiRepresentable.full_inverseImage_augmented', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObject.lean, line 242. The attribute's comment: “part (1): a^{-1} on sheaves of sets is full”.

For a hypercovering a : U ⟶ X of X in C the inverse image a^{-1} : Sh(C/X) ⥤ Sh((C/U)_total) is full.

theorem full_inverseImage_augmented' (h : IsHypercoveringAugmentation P U a) :
    (augmentationMorphismOfTopoi P U a).inverseImage.Full

CategoryTheory.SimplicialSemiRepresentable.fullyFaithfulInverseImageAugmented, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObject.lean, line 249. The attribute's comment: “part (1): a^{-1} on sheaves of sets is fully faithful, carrying local fullness”.

For a hypercovering a : U ⟶ X of X in C such that j_total is locally full, the inverse image a^{-1} : Sh(C/X) ⥤ Sh((C/U)_total) is fully faithful.

def fullyFaithfulInverseImageAugmented (h : IsHypercoveringAugmentation P U a)
    (hlf : (totalForget (associatedSimplicialObject.{u} U a)).IsLocallyFull
      (P.toGrothendieck.over X)) :
    (augmentationMorphismOfTopoi P U a).inverseImage.FullyFaithful

CategoryTheory.SimplicialSemiRepresentable.fullyFaithfulInverseImageAugmented', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObject.lean, line 259. The attribute's comment: “part (1): a^{-1} on sheaves of sets is fully faithful”.

For a hypercovering a : U ⟶ X of X in C the inverse image a^{-1} : Sh(C/X) ⥤ Sh((C/U)_total) is fully faithful.

def fullyFaithfulInverseImageAugmented' (h : IsHypercoveringAugmentation P U a) :
    (augmentationMorphismOfTopoi P U a).inverseImage.FullyFaithful

CategoryTheory.SimplicialSemiRepresentable.isIso_unit_augmented, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObject.lean, line 268. The attribute's comment: “part (1): E = a_* a^{-1} E on sheaves of sets, carrying local fullness”.

For a hypercovering augmentation such that j_total is locally full, the canonical map E ⟶ a_* a^{-1} E is an isomorphism for every sheaf of sets E on C/X.

theorem isIso_unit_augmented (h : IsHypercoveringAugmentation P U a)
    (hlf : (totalForget (associatedSimplicialObject.{u} U a)).IsLocallyFull
      (P.toGrothendieck.over X)) :
    IsIso (augmentationMorphismOfTopoi P U a).adj.unit

CategoryTheory.SimplicialSemiRepresentable.isIso_unit_augmented', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObject.lean, line 278. The attribute's comment: “part (1): E = a_* a^{-1} E on sheaves of sets”.

For a hypercovering augmentation, the canonical map E ⟶ a_* a^{-1} E is an isomorphism for every sheaf of sets E on C/X.

theorem isIso_unit_augmented' (h : IsHypercoveringAugmentation P U a) :
    IsIso (augmentationMorphismOfTopoi P U a).adj.unit

CategoryTheory.SimplicialSemiRepresentable.isCartesianSheaf_of_mem_essImage_augmented, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObject.lean, line 285. The attribute's comment: “part (1): the essential image of a^{-1} consists of cartesian sheaves of sets”.

Every sheaf of sets on (C/U)_total isomorphic to an inverse image along the augmentation is cartesian.

theorem isCartesianSheaf_of_mem_essImage_augmented
    {F : Sheaf (totalSituation P U a).totalTopology (Type u)}
    (hF : (augmentationMorphismOfTopoi P U a).inverseImage.essImage F) :
    (totalSituation P U a).IsCartesianSheaf F

CategoryTheory.SimplicialSemiRepresentable.mem_essImage_iff_isCartesianSheaf_augmented, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObject.lean, line 295. The attribute's comment: “part (1): essential image = cartesian sheaves of sets, carrying surjectivity”.

If every cartesian sheaf of sets on (C/U)_total lies in the essential image of a^{-1}, then the essential image of a^{-1} is exactly the cartesian sheaves of sets.

theorem mem_essImage_iff_isCartesianSheaf_augmented
    (hsurj : ∀ G : Sheaf (totalSituation P U a).totalTopology (Type u),
      (totalSituation P U a).IsCartesianSheaf G →
        (augmentationMorphismOfTopoi P U a).inverseImage.essImage G)
    (F : Sheaf (totalSituation P U a).totalTopology (Type u)) :
    (augmentationMorphismOfTopoi P U a).inverseImage.essImage F ↔
      (totalSituation P U a).IsCartesianSheaf F

CategoryTheory.SimplicialSemiRepresentable.mem_essImage_iff_isCartesianSheaf_augmented', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObject.lean, line 307. The attribute's comment: “part (1): the essential image of a^{-1} is exactly the cartesian sheaves of sets”.

For a hypercovering augmentation, the essential image of a^{-1} : Sh(C/X) ⥤ Sh((C/U)_total) is exactly the cartesian sheaves of sets.

theorem mem_essImage_iff_isCartesianSheaf_augmented' (h : IsHypercoveringAugmentation P U a)
    (F : Sheaf (totalSituation P U a).totalTopology (Type u)) :
    (augmentationMorphismOfTopoi P U a).inverseImage.essImage F ↔
      (totalSituation P U a).IsCartesianSheaf F

CategoryTheory.SimplicialSemiRepresentable.isIso_counit_app_augmented, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObject.lean, line 318. The attribute's comment: “part (1): a^{-1} a_* F = F for cartesian F, carrying the two clauses of 0D8E”.

For a hypercovering augmentation such that j_total is locally full and every cartesian sheaf of sets on (C/U)_total lies in the essential image of a^{-1}, the canonical map a^{-1} a_* F ⟶ F is an isomorphism for every cartesian sheaf of sets F on (C/U)_total.

theorem isIso_counit_app_augmented (h : IsHypercoveringAugmentation P U a)
    (hlf : (totalForget (associatedSimplicialObject.{u} U a)).IsLocallyFull
      (P.toGrothendieck.over X))
    (hsurj : ∀ G : Sheaf (totalSituation P U a).totalTopology (Type u),
      (totalSituation P U a).IsCartesianSheaf G →
        (augmentationMorphismOfTopoi P U a).inverseImage.essImage G)
    {F : Sheaf (totalSituation P U a).totalTopology (Type u)}
    (hF : (totalSituation P U a).IsCartesianSheaf F) :
    IsIso ((augmentationMorphismOfTopoi P U a).adj.counit.app F)

CategoryTheory.SimplicialSemiRepresentable.isIso_counit_app_augmented', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObject.lean, line 334. The attribute's comment: “part (1): a^{-1} a_* F = F for a cartesian sheaf of sets F”.

For a hypercovering augmentation, the canonical map a^{-1} a_* F ⟶ F is an isomorphism for every cartesian sheaf of sets F on (C/U)_total.

theorem isIso_counit_app_augmented' (h : IsHypercoveringAugmentation P U a)
    {F : Sheaf (totalSituation P U a).totalTopology (Type u)}
    (hF : (totalSituation P U a).IsCartesianSheaf F) :
    IsIso ((augmentationMorphismOfTopoi P U a).adj.counit.app F)

CategoryTheory.SimplicialSemiRepresentable.faithful_abelianInverseImage_augmented, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObject.lean, line 346. The attribute's comment: “part (2): a^{-1} on abelian sheaves is faithful”.

For a hypercovering a : U ⟶ X of X in C the inverse image a^{-1} : Ab(C/X) ⥤ Ab((C/U)_total) of the augmentation is faithful.

theorem faithful_abelianInverseImage_augmented (h : IsHypercoveringAugmentation P U a) :
    (abelianInverseImage P U a).Faithful

CategoryTheory.SimplicialSemiRepresentable.full_abelianInverseImage_augmented, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObject.lean, line 354. The attribute's comment: “part (2): a^{-1} on abelian sheaves is full, carrying local fullness of j_total”.

For a hypercovering a : U ⟶ X of X in C such that j_total is locally full, the inverse image a^{-1} : Ab(C/X) ⥤ Ab((C/U)_total) is full.

theorem full_abelianInverseImage_augmented (h : IsHypercoveringAugmentation P U a)
    (hlf : (totalForget (associatedSimplicialObject.{u} U a)).IsLocallyFull
      (P.toGrothendieck.over X)) :
    (abelianInverseImage P U a).Full

CategoryTheory.SimplicialSemiRepresentable.full_abelianInverseImage_augmented', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObject.lean, line 364. The attribute's comment: “part (2): a^{-1} on abelian sheaves is full”.

For a hypercovering a : U ⟶ X of X in C the inverse image a^{-1} : Ab(C/X) ⥤ Ab((C/U)_total) is full.

theorem full_abelianInverseImage_augmented' (h : IsHypercoveringAugmentation P U a) :
    (abelianInverseImage P U a).Full

CategoryTheory.SimplicialSemiRepresentable.fullyFaithfulAbelianInverseImageAugmented, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObject.lean, line 371. The attribute's comment: “part (2): a^{-1} on abelian sheaves is fully faithful, carrying local fullness”.

For a hypercovering a : U ⟶ X of X in C such that j_total is locally full, the inverse image a^{-1} : Ab(C/X) ⥤ Ab((C/U)_total) is fully faithful.

def fullyFaithfulAbelianInverseImageAugmented (h : IsHypercoveringAugmentation P U a)
    (hlf : (totalForget (associatedSimplicialObject.{u} U a)).IsLocallyFull
      (P.toGrothendieck.over X)) :
    (abelianInverseImage P U a).FullyFaithful

CategoryTheory.SimplicialSemiRepresentable.fullyFaithfulAbelianInverseImageAugmented', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObject.lean, line 381. The attribute's comment: “part (2): a^{-1} on abelian sheaves is fully faithful”.

For a hypercovering a : U ⟶ X of X in C the inverse image a^{-1} : Ab(C/X) ⥤ Ab((C/U)_total) is fully faithful.

def fullyFaithfulAbelianInverseImageAugmented' (h : IsHypercoveringAugmentation P U a) :
    (abelianInverseImage P U a).FullyFaithful

CategoryTheory.SimplicialSemiRepresentable.isIso_abelianUnit_augmented, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObject.lean, line 390. The attribute's comment: “part (2): E = a_* a^{-1} E on abelian sheaves, carrying local fullness”.

For a hypercovering augmentation such that j_total is locally full, the canonical map E ⟶ a_* a^{-1} E is an isomorphism for every sheaf of abelian groups E on C/X.

theorem isIso_abelianUnit_augmented (h : IsHypercoveringAugmentation P U a)
    (hlf : (totalForget (associatedSimplicialObject.{u} U a)).IsLocallyFull
      (P.toGrothendieck.over X)) :
    IsIso (abelianAdjunction P U a).unit

CategoryTheory.SimplicialSemiRepresentable.isIso_abelianUnit_augmented', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObject.lean, line 400. The attribute's comment: “part (2): E = a_* a^{-1} E on abelian sheaves”.

For a hypercovering augmentation, the canonical map E ⟶ a_* a^{-1} E is an isomorphism for every sheaf of abelian groups E on C/X.

theorem isIso_abelianUnit_augmented' (h : IsHypercoveringAugmentation P U a) :
    IsIso (abelianAdjunction P U a).unit

CategoryTheory.SimplicialSemiRepresentable.isCartesianAbSheaf_of_mem_essImage_augmented, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObject.lean, line 407. The attribute's comment: “part (2): the essential image of a^{-1} consists of cartesian abelian sheaves”.

Every sheaf of abelian groups on (C/U)_total isomorphic to an inverse image along the augmentation is cartesian.

theorem isCartesianAbSheaf_of_mem_essImage_augmented
    {F : Sheaf (totalSituation P U a).totalTopology Ab.{u}}
    (hF : (abelianInverseImage P U a).essImage F) :
    (totalSituation P U a).IsCartesianAbSheaf F

CategoryTheory.SimplicialSemiRepresentable.mem_essImage_iff_isCartesianAbSheaf_augmented, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObject.lean, line 417. The attribute's comment: “part (2): essential image = cartesian abelian sheaves, carrying surjectivity”.

If every cartesian sheaf of abelian groups on (C/U)_total lies in the essential image of a^{-1}, then the essential image of a^{-1} is exactly the cartesian abelian sheaves.

theorem mem_essImage_iff_isCartesianAbSheaf_augmented
    (hsurj : ∀ G : Sheaf (totalSituation P U a).totalTopology Ab.{u},
      (totalSituation P U a).IsCartesianAbSheaf G → (abelianInverseImage P U a).essImage G)
    (F : Sheaf (totalSituation P U a).totalTopology Ab.{u}) :
    (abelianInverseImage P U a).essImage F ↔
      (totalSituation P U a).IsCartesianAbSheaf F

CategoryTheory.SimplicialSemiRepresentable.mem_essImage_iff_isCartesianAbSheaf_augmented', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObject.lean, line 428. The attribute's comment: “part (2): the essential image of a^{-1} is exactly the cartesian abelian sheaves”.

For a hypercovering augmentation, the essential image of a^{-1} : Ab(C/X) ⥤ Ab((C/U)_total) is exactly the cartesian abelian sheaves.

theorem mem_essImage_iff_isCartesianAbSheaf_augmented' (h : IsHypercoveringAugmentation P U a)
    (F : Sheaf (totalSituation P U a).totalTopology Ab.{u}) :
    (abelianInverseImage P U a).essImage F ↔
      (totalSituation P U a).IsCartesianAbSheaf F

CategoryTheory.SimplicialSemiRepresentable.isIso_abelianCounit_app_augmented, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObject.lean, line 439. The attribute's comment: “part (2): a^{-1} a_* F = F for cartesian F, carrying the two clauses of 0D8E”.

For a hypercovering augmentation such that j_total is locally full and every cartesian sheaf of abelian groups on (C/U)_total lies in the essential image of a^{-1}, the canonical map a^{-1} a_* F ⟶ F is an isomorphism for every cartesian sheaf of abelian groups F.

theorem isIso_abelianCounit_app_augmented (h : IsHypercoveringAugmentation P U a)
    (hlf : (totalForget (associatedSimplicialObject.{u} U a)).IsLocallyFull
      (P.toGrothendieck.over X))
    (hsurj : ∀ G : Sheaf (totalSituation P U a).totalTopology Ab.{u},
      (totalSituation P U a).IsCartesianAbSheaf G → (abelianInverseImage P U a).essImage G)
    {F : Sheaf (totalSituation P U a).totalTopology Ab.{u}}
    (hF : (totalSituation P U a).IsCartesianAbSheaf F) :
    IsIso ((abelianAdjunction P U a).counit.app F)

CategoryTheory.SimplicialSemiRepresentable.isIso_abelianCounit_app_augmented', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObject.lean, line 454. The attribute's comment: “part (2): a^{-1} a_* F = F for a cartesian abelian sheaf F”.

For a hypercovering augmentation, the canonical map a^{-1} a_* F ⟶ F is an isomorphism for every cartesian sheaf of abelian groups F on (C/U)_total.

theorem isIso_abelianCounit_app_augmented' (h : IsHypercoveringAugmentation P U a)
    {F : Sheaf (totalSituation P U a).totalTopology Ab.{u}}
    (hF : (totalSituation P U a).IsCartesianAbSheaf F) :
    IsIso ((abelianAdjunction P U a).counit.app F)

Tag 0D8N, a lemma

Tag 0D8N in the Stacks Project.

CategoryTheory.SimplicialSemiRepresentable.isIso_derivedAugmentationUnitAugmented_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObjectDerivedPushforward.lean, line 290. The attribute's comment: “granted two inputs this library does not have: local fullness of j_total, which is the unproved clause of Tag 0D8E, and the Ra_*-acyclicity of a⁻¹ of a K-injective complex, which is the content of the spectral sequence of Tag 0D7A; the isomorphism is not proved unconditionally”.

Stacks Project, Tag 0D8N, granted the two inputs this library does not have. For a site C with fibre products, an object X of C and a hypercovering a : U ⟶ X of X in C by a simplicial object U of C, the canonical map E ⟶ Ra_* a^{-1} E is an isomorphism for every object E of the unbounded derived category of abelian sheaves on C/X.

E is arbitrary: no boundedness is assumed and the coefficients are all abelian sheaves. The source deduces this from Stacks 0D8L for the associated simplicial semi-representable object over X, and that is the deduction performed, the hypercovering conditions on a entering through cover density of j_total.

The two carried hypotheses are the ones discussed in the module docstring. hlf, local fullness of j_total, is the clause of Stacks 0D8E which the library does not prove; together with the degree-zero clause of h it supplies the underived unit F ⟶ a_* a^{-1} F of Stacks 0DA8 (2), which is the first input of Stacks 0D8L. hacyclic says that the direct image of a^{-1} of a K-injective complex needs no derivation, that is, that R^p a_* a^{-1} vanishes in positive degrees; the source reads that off the spectral sequence of Stacks 0D7A, which this library builds but without the convergence to R^{p+q} a_* that the reading needs. No unconditional invertibility is claimed.

theorem isIso_derivedAugmentationUnitAugmented_app
    (h : IsHypercoveringAugmentation P U a)
    (hlf : (totalForget (associatedSimplicialObject.{u} U a)).IsLocallyFull
      (P.toGrothendieck.over X))
    (hacyclic : ∀ I : CochainComplex (AbelianSheavesOver P.toGrothendieck X) ℤ,
      I.IsKInjective →
        IsIso ((derivedAbelianTotalPushforwardOverUnit P.toGrothendieck X
          (associatedSimplicialObject.{u} U a)).app
            (((abelianTotalInverseImageOver P.toGrothendieck X
              (associatedSimplicialObject.{u} U a)).mapHomotopyCategory
                (ComplexShape.up ℤ)).obj
                  ((HomotopyCategory.quotient (AbelianSheavesOver P.toGrothendieck X)
                    (ComplexShape.up ℤ)).obj I))))
    (E : DerivedCategory (AbelianSheavesOver P.toGrothendieck X)) :
    IsIso ((derivedAugmentationUnitAugmented P U a).app E)

CategoryTheory.SimplicialSemiRepresentable.isIso_derivedAugmentationUnitAugmented_app', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObjectDerivedPushforwardUnconditional.lean, line 249. The attribute's comment: “with the Ra_*-acyclicity of a⁻¹ of a K-injective complex taken as an explicit input. It is discharged, and this tag carried unconditionally, by ...SimplicialSemiRepresentable.isIso_derivedAugmentationUnitAugmented_app_unconditional”.

Stacks Project, Tag 0D8N, granted the one input this library does not have. For a site C with fibre products, an object X of C and a hypercovering a : U ⟶ X of X in C by a simplicial object U of C, the canonical map E ⟶ Ra_* a^{-1} E is an isomorphism for every object E of the unbounded derived category of abelian sheaves on C/X.

E is arbitrary: no boundedness is assumed and the coefficients are all abelian sheaves. The source deduces this from Stacks 0D8L for the associated simplicial semi-representable object over X, and that is the deduction performed, the hypercovering conditions on a entering through cover density and local fullness of j_total.

The first input of Stacks 0D8L is discharged from the hypercovering conditions alone: it is the underived unit F ⟶ a_* a^{-1} F of Stacks 0DA8 (2), CategoryTheory.SimplicialSemiRepresentable.isIso_abelianUnit_augmented'. What remains carried is the hypothesis discussed in the module docstring: hacyclic says that the direct image of a^{-1} of a K-injective complex needs no derivation, that is, that R^p a_* a^{-1} vanishes in positive degrees; the source reads that off the spectral sequence of Stacks 0D7A, which this library builds but without the convergence to R^{p+q} a_* that the reading needs. No unconditional invertibility is claimed.

theorem isIso_derivedAugmentationUnitAugmented_app'
    (h : IsHypercoveringAugmentation P U a)
    (hacyclic : ∀ I : CochainComplex (AbelianSheavesOver P.toGrothendieck X) ℤ,
      I.IsKInjective →
        IsIso ((derivedAbelianTotalPushforwardOverUnit P.toGrothendieck X
          (associatedSimplicialObject.{u} U a)).app
            (((abelianTotalInverseImageOver P.toGrothendieck X
              (associatedSimplicialObject.{u} U a)).mapHomotopyCategory
                (ComplexShape.up ℤ)).obj
                  ((HomotopyCategory.quotient (AbelianSheavesOver P.toGrothendieck X)
                    (ComplexShape.up ℤ)).obj I))))
    (E : DerivedCategory (AbelianSheavesOver P.toGrothendieck X)) :
    IsIso ((derivedAugmentationUnitAugmented P U a).app E)

CategoryTheory.SimplicialSemiRepresentable.isIso_derivedAugmentationUnitAugmented_app_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringObjectDerivedPushforwardUnconditional.lean, line 151.

For a hypercovering augmentation a : U ⟶ X of a simplicial object of C, the canonical map E ⟶ Ra_* a⁻¹ E is invertible at every object E of D(C/X).

theorem isIso_derivedAugmentationUnitAugmented_app_unconditional (P : Pretopology C) {X : C}
    (U : SimplicialObject C) (a : U ⟶ (SimplicialObject.const C).obj X)
    (h : IsHypercoveringAugmentation P U a)
    (E : DerivedCategory (AbelianSheavesOver P.toGrothendieck X)) :
    IsIso ((derivedAugmentationUnitAugmented P U a).app E)

Tag 09X9, a lemma

Tag 09X9 in the Stacks Project.

CategoryTheory.SimplicialSemiRepresentable.derivedGlobalSectionsInverseImageIsoAugmented', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObjectDerivedDescentUnconditional.lean, line 87.

Stacks Project, Tag 09X9. For a site C with fibre products, an object X of C and a hypercovering a : U ⟶ X of X in C by a simplicial object U of C, with a : Sh((C/U)_total) ⟶ Sh(C/X) the augmentation of Stacks 09X8, derived global sections over X are derived global sections on the total site of the inverse image:

RΓ(X, E) = RΓ((C/U)_total, a⁻¹E).

The statement is an isomorphism of functors on the unbounded derived category of abelian sheaves on C/X, so it holds at every object E of D(C/X).

def derivedGlobalSectionsInverseImageIsoAugmented'
    (h : IsHypercoveringAugmentation P U a) :
    Augmentation.derivedGlobalSectionsBase (Cat.of (Over X)) (P.toGrothendieck.over X) ≅
      Augmentation.derivedTotalInverseImage (totalSituation P U a) (Cat.of (Over X))
          (P.toGrothendieck.over X) (augmentationAugmented P U a) ⋙
        Augmentation.derivedGlobalSectionsTotal (totalSituation P U a)

CategoryTheory.SimplicialSemiRepresentable.derivedGlobalSectionsInverseImageIsoAugmented_hom_app', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObjectDerivedDescentUnconditional.lean, line 102. The attribute's comment: “the forward map of the isomorphism is the canonical one — RΓ(X, -) of the canonical map E ⟶ Ra_*a⁻¹E of Tag 0D8L followed by the derived factorisation of Tag 08J6”.

Stacks 09X9, the isomorphism is invertibility of the canonical comparison map. At every object E of D(C/X) the forward map of the isomorphism of Stacks 09X9 is derived global sections over X applied to the canonical map E ⟶ Ra_*a⁻¹E of Stacks 0D8L, followed by the derived factorisation Ra_* ⋙ RΓ(X, -) ≅ RΓ((C/U)_total, -) of Stacks 08J6.

theorem derivedGlobalSectionsInverseImageIsoAugmented_hom_app'
    (h : IsHypercoveringAugmentation P U a)
    (E : DerivedCategory (Sheaf (P.toGrothendieck.over X) AddCommGrpCat.{u})) :
    (derivedGlobalSectionsInverseImageIsoAugmented' P U a h).hom.app E =
      (Augmentation.derivedGlobalSectionsBase (Cat.of (Over X))
          (P.toGrothendieck.over X)).map
        ((Augmentation.derivedAugmentationUnit (totalSituation P U a) (Cat.of (Over X))
          (P.toGrothendieck.over X) (augmentationAugmented P U a)).app E) ≫
        (Augmentation.derivedGlobalSectionsPushforwardIso (totalSituation P U a)
          (Cat.of (Over X)) (P.toGrothendieck.over X) (augmentationAugmented P U a)
            (abelianTotalPushforwardGammaIsoOver P
              (associatedSimplicialObject.{u} U a))).hom.app
            ((Augmentation.derivedTotalInverseImage (totalSituation P U a) (Cat.of (Over X))
              (P.toGrothendieck.over X) (augmentationAugmented P U a)).obj E)

Tag 0DA9, a lemma

Tag 0DA9 in the Stacks Project.

CategoryTheory.SimplicialSemiRepresentable.derivedTotalInverseImageEquivalenceAugmented', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObjectDerivedDescentUnconditional.lean, line 136.

Stacks Project, Tag 0DA9. For a site C with fibre products, an object X of C, a hypercovering a : U ⟶ X of X in C by a simplicial object U of C, the augmentation a : Sh((C/U)_total) ⟶ Sh(C/X) of Stacks 09X8, and the weak Serre subcategory 𝒜 ⊂ Ab((C/U)_total) of cartesian abelian sheaves of Stacks 0D7J, the derived inverse image is an equivalence

a⁻¹ : D⁺(C/X) ⟶ D⁺_𝒜((C/U)_total)

with quasi-inverse Ra_*.

def derivedTotalInverseImageEquivalenceAugmented'
    (h : IsHypercoveringAugmentation P U a) :
    (DerivedCategoryB.derivedCategoryBPlus
        (⊤ : ObjectProperty
          (Sheaf (P.toGrothendieck.over X) AddCommGrpCat.{u}))).FullSubcategory ≌
      (DerivedCategoryB.derivedCategoryBPlus
        ((totalSituation P U a).IsCartesianAbSheaf)).FullSubcategory

CategoryTheory.SimplicialSemiRepresentable.derivedTotalInverseImageEquivalenceAugmented_functor', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObjectDerivedDescentUnconditional.lean, line 149. The attribute's comment: “the forward functor of the equivalence is a⁻¹”.

Stacks 0DA9, the forward functor of the equivalence is a⁻¹: it is the restriction of the derived inverse image along the augmentation to the bounded below subcategories.

theorem derivedTotalInverseImageEquivalenceAugmented_functor'
    (h : IsHypercoveringAugmentation P U a) :
    (derivedTotalInverseImageEquivalenceAugmented' P U a h).functor =
      Augmentation.derivedTotalInverseImagePlus (totalSituation P U a) (Cat.of (Over X))
        (P.toGrothendieck.over X) (augmentationAugmented P U a)

CategoryTheory.SimplicialSemiRepresentable.derivedTotalInverseImageEquivalenceAugmented_inverse', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBySimplicialObjectDerivedDescentUnconditional.lean, line 159. The attribute's comment: “the quasi-inverse of the equivalence is Ra_*”.

Stacks 0DA9, the quasi-inverse of the equivalence is Ra_*: it is the restriction of the derived direct image along the augmentation to the bounded below subcategories.

theorem derivedTotalInverseImageEquivalenceAugmented_inverse'
    (h : IsHypercoveringAugmentation P U a) :
    (derivedTotalInverseImageEquivalenceAugmented' P U a h).inverse =
      Augmentation.derivedTotalPushforwardPlus (totalSituation P U a) (Cat.of (Over X))
        (P.toGrothendieck.over X) (augmentationAugmented P U a)

Tag 09WL, a lemma

Tag 09WL in the Stacks Project.

CategoryTheory.SimplicialOver.isMorphismOfSites_pullbackMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/OverSimplicialObject.lean, line 161. The attribute's comment: “part (1), each transition is a morphism of sites”.

Stacks 09WL part (1). For a simplex map φ : [m] ⟶ [n] the base change functor v_φ = Over.pullback f_φ : C/U_m ⥤ C/U_n along f_φ : U_n ⟶ U_m represents a morphism of sites C/U_n ⟶ C/U_m between the localizations of (C, J) in the two degrees: it is continuous and the induced pullback on sheaves of sets is exact.

This is Stacks 09W9 applied to f_φ, and it is the datum making the localizations C/U_n into a simplicial object in the category whose objects are sites and whose morphisms are morphisms of sites.

theorem isMorphismOfSites_pullbackMap {m n : SimplexCategory} (φ : m ⟶ n) :
    (Over.pullback (U.map φ.op)).IsMorphismOfSites
      (J.over (U.obj (op m))) (J.over (U.obj (op n)))

CategoryTheory.SimplicialOver.pullbackMapId, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/OverSimplicialObject.lean, line 170. The attribute's comment: “part (1), the identity isomorphism”.

Stacks 09WL part (1). The transition morphism of sites attached to an identity simplex map is the identity: base change along f_{𝟙} = 𝟙 U_n is isomorphic to the identity functor of C/U_n.

def pullbackMapId (n : SimplexCategory) :
    Over.pullback (U.map (𝟙 n).op) ≅ 𝟭 (Over (U.obj (op n)))

CategoryTheory.SimplicialOver.pullbackMapComp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/OverSimplicialObject.lean, line 179. The attribute's comment: “part (1), the composition isomorphism”.

Stacks 09WL part (1). The transition morphisms of sites are compatible with composition of simplex maps: base change along f_{ψ ≫ φ} = f_φ ≫ f_ψ is isomorphic to base change along f_ψ followed by base change along f_φ, by the canonical isomorphism W ×_{U_l} U_n ≅ (W ×_{U_l} U_m) ×_{U_m} U_n of chosen fibre products.

def pullbackMapComp {l m n : SimplexCategory} (ψ : l ⟶ m) (φ : m ⟶ n) :
    Over.pullback (U.map (ψ ≫ φ).op) ≅
      Over.pullback (U.map ψ.op) ⋙ Over.pullback (U.map φ.op)

CategoryTheory.SimplicialOver.sheafPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/OverSimplicialObject.lean, line 190. The attribute's comment: “part (1), the transitions induce the localization morphisms of topoi”.

Stacks 09WL part (1). The morphism of topoi Sh(C/U_n) ⟶ Sh(C/U_m) attached to the transition morphism of sites of a simplex map φ : [m] ⟶ [n] is the one attached to the localization functor j = Over.map f_φ: the direct image of the cocontinuous functor j is the direct image of the continuous functor v_φ = Over.pullback f_φ.

def sheafPushforwardIso {m n : SimplexCategory} (φ : m ⟶ n) :
    (Over.map (U.map φ.op)).sheafPushforwardCocontinuous (Type u)
        (J.over (U.obj (op n))) (J.over (U.obj (op m))) ≅
      (Over.pullback (U.map φ.op)).sheafPushforwardContinuous (Type u)
        (J.over (U.obj (op m))) (J.over (U.obj (op n)))

CategoryTheory.SimplicialOver.totalComparisonEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/OverSimplicialObjectTotalSite.lean, line 352. The attribute's comment: “part (2), the comparison of the two total categories”.

Stacks 09WL part (2). The construction of Stacks 09WC applied to the simplicial object in sites of part (1) reproduces the category (C/U)_total: the comparison functor, which is the identity on objects and the bijection totalHomEquiv on morphisms, is an isomorphism of categories.

def totalComparisonEquivalence : Grothendieck (slices U) ≌ PullbackTotal U

CategoryTheory.SimplicialOver.pullbackTotalCoverings_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/OverSimplicialObjectTotalSite.lean, line 389. The attribute's comment: “part (2), the coverings of the two total sites agree”.

Stacks 09WL part (2). The two sites have the same covering families: a family of the total category of Stacks 09WC is covering exactly when it is the image under the comparison of a covering family of (C/U)_total. Both topologies are generated by these families.

theorem pullbackTotalCoverings_iff (𝒱 : Covering.{u, u, u} (PullbackTotal U)) :
    pullbackTotalCoverings J U 𝒱 ↔
      ∃ 𝒰 : Covering.{u, u, u} (Grothendieck (slices U)),
        SimplicialCoverings.total (slices U) (sliceCoverings J U) 𝒰 ∧
          𝒱 = ⟨(totalComparison U).obj 𝒰.1, 𝒰.2.map (totalComparison U)⟩

CategoryTheory.SimplicialOver.totalTopology_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/OverSimplicialObjectTotalSite.lean, line 525. The attribute's comment: “part (2), the generic total site is (C/U)_total”.

Stacks 09WL part (2). The total site of that situation is the site (C/U)_total: the generic construction of the total site, applied to the simplicial family of sites n ↦ C/U_n, gives the category (C/U)_total and the topology totalTopology on the nose.

theorem totalTopology_eq : (situation J U).totalTopology = SimplicialOver.totalTopology J U

CategoryTheory.SimplicialOver.isMorphismOfSites_augmentationPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/OverSimplicialObjectTotalSite.lean, line 547. The attribute's comment: “part (3), a_0 is a morphism of sites”.

Stacks 09WL part (3). For an augmentation a : U → X, base change along a_0 : U_0 ⟶ X is continuous with exact pullback on sheaves of sets, that is, it represents a morphism of sites a_0 : C/U_0 → C/X. This is Stacks 09W9 applied to a_0.

theorem isMorphismOfSites_augmentationPullback :
    (Over.pullback (augmentationApp U a (op (SimplexCategory.mk 0)))).IsMorphismOfSites
      (J.over X) (J.over (U.obj (op (SimplexCategory.mk 0))))

CategoryTheory.SimplicialOver.augmentationVertexCompat, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/OverSimplicialObjectTotalSite.lean, line 567. The attribute's comment: “part (3), the vertex compatibility of the augmentation”.

Stacks 09WL part (3). The functor u_0 = Over.pullback a_0 representing the augmentation satisfies the compatibility of Stacks 0D6Z part (A): the composites u_φ ∘ u_0 for the vertices φ : [0] ⟶ [n] of a simplicial degree agree, both being canonically isomorphic to base change along a_n. Chosen fibre products make this an isomorphism rather than the equality of functors the source writes, exactly as in part (1).

def augmentationVertexCompat (n : SimplexCategory) (φ ψ : SimplexCategory.mk 0 ⟶ n) :
    Over.pullback (augmentationApp U a (op (SimplexCategory.mk 0))) ⋙
        Over.pullback (U.map φ.op) ≅
      Over.pullback (augmentationApp U a (op (SimplexCategory.mk 0))) ⋙
        Over.pullback (U.map ψ.op)

CategoryTheory.SimplicialOver.augmentation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/OverSimplicialObjectTotalSite.lean, line 616. The attribute's comment: “part (3), a_0 is an augmentation of the simplicial site C/U”.

Stacks 09WL part (3). The augmentation a_0 : C/U_0 → C/X of the simplicial family of sites n ↦ C/U_n: the localization functor j_{a_0} = Over.map a_0 is cocontinuous and its composite with the functor of any vertex of a simplicial degree is j_{a_n}, which does not mention the vertex. By isMorphismOfSites_augmentationPullback and augmentationSheafPushforwardIso this is the augmentation given by the morphism of sites a_0 of Stacks 0D6Z part (A): the two presentations of a_0 give the same morphism of topoi Sh(C/U_0) ⟶ Sh(C/X).

def augmentation : (simplicialSite J U).Augmentation (Cat.of (Over X)) (J.over X)

CategoryTheory.SimplicialOver.augmentationMorphismOfTopoi, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/OverSimplicialObjectTotalSite.lean, line 713. The attribute's comment: “part (3), the morphism of topoi Sh((C/U)_total) to Sh(C/X) of the augmentation”.

Stacks 09WL part (3). The morphism of topoi a : Sh((C/U)_total) ⟶ Sh(C/X) which the augmentation a_0 gives: the morphism of topoi of Stacks 0D70 attached to the augmentation of the simplicial family of sites n ↦ C/U_n determined by a_0.

noncomputable def augmentationMorphismOfTopoi :
    MorphismOfTopoi (Sheaf (SimplicialOver.totalTopology J U) (Type u))
      (Sheaf (J.over X) (Type u))

CategoryTheory.SimplicialOver.augmentationMorphismOfTopoi_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/OverSimplicialObjectTotalSite.lean, line 722. The attribute's comment: “part (3), the augmentation gives the morphism of topoi above”.

Stacks 09WL part (3). That morphism of topoi is the one above: its direct image is the direct image of the cocontinuous functor V/U_n ↦ V/X of Stacks 09X8. The two are equal, not merely isomorphic.

theorem augmentationMorphismOfTopoi_pushforward :
    (augmentationMorphismOfTopoi J U a).pushforward =
      (augmentationFunctor U a).sheafPushforwardCocontinuous (Type u)
        (SimplicialOver.totalTopology J U) (J.over X)

Sources

LeanStacks.CategoryTheory.Hypercovering.IsHypercoveringAugmentation · CategoryTheory.SimplicialOver.homEquivCommSq · CategoryTheory.SimplicialOver.toAssociatedTotal_comp_totalForget · CategoryTheory.SimplicialOver.associatedTotalEquivalence · CategoryTheory.SimplicialOver.associatedTotalEquivalence_isDenseSubsite · CategoryTheory.SimplicialOver.augmentationPushforwardIsoAssociated · CategoryTheory.SimplicialOver.augmentationInverseImageIsoAssociated · Stacks.CategoryTheory.Hypercovering.associatedSimplicialObject

Section85.22 Hypercovering by a simplicial object of the site: modules #

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

Tag 0DAB, a lemma

Tag 0DAB in the Stacks Project.

CategoryTheory.SimplicialSemiRepresentable.faithful_pullbackModules_simplicialObject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringSimplicialObjectModuleDescent.lean, line 117. The attribute's comment: “a^ on sheaves of modules is faithful, for a hypercovering of X by a simplicial object of the site. The essential-image inclusion is isCartesianModule_of_mem_essImage_simplicialObject; fullness of a^, and essential surjectivity onto the cartesian O-modules making a_* a quasi-inverse, are not proved”.

Stacks 0DAB, the faithfulness half. Let C be a site with fibre products, X an object of it, O_C a sheaf of commutative rings on C, and U a simplicial object of C augmented to X which is a hypercovering of X in the sense of Stacks, Section 85.21: the degree-zero augmentation, the canonical map U_1 ⟶ U_0 ×_X U_0, and every higher matching map generate covering presieves. With O_X = O_C|_{C/X} and O = a⁻¹O_X, the pullback a^* : Mod(O_X) ⥤ Mod(O) of sheaves of modules along the augmentation of the total site of U over C/X is faithful.

This is Stacks 0DA4 for the associated simplicial semi-representable object of Stacks 0GM9, whose hypercovering condition is exactly the three hypotheses.

theorem faithful_pullbackModules_simplicialObject
    (h₀ : Presieve.singleton (a.app (op ⦋0⦌)) ∈ P X)
    (h₁ : Presieve.singleton (oneSimplexToFiberProduct U a) ∈
      P (pullback (a.app (op ⦋0⦌)) (a.app (op ⦋0⦌))))
    (hmatch : ∀ n : ℕ, 1 ≤ n → Presieve.singleton (matchingMap U a n) ∈
      P ((((SimplicialObject.cosk n).obj (Over.lift U a)).obj (op ⦋n + 1⦌)).left)) :
    (hypercoveringObjectRingedAugmentation P (associatedSimplicialObject.{u} U a)
      OC).totalRingedHom.toModulesHom.pullbackModules.Faithful

CategoryTheory.SimplicialSemiRepresentable.isCartesianModule_of_mem_essImage_simplicialObject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringSimplicialObjectModuleDescent.lean, line 138. The attribute's comment: “the essential image of a^ consists of cartesian O-modules, for a hypercovering of X by a simplicial object of the site. Faithfulness of a^ is faithful_pullbackModules_simplicialObject; fullness of a^, and essential surjectivity onto the cartesian O-modules making a_ a quasi-inverse, are not proved”.

Stacks 0DAB, the inclusion of the essential image in the cartesian modules. In the situation above, every sheaf of O-modules on the total site of a simplicial object of C augmented to X which is isomorphic to a pullback a^*F is a cartesian O-module.

This is Stacks 0DA4 for the associated simplicial semi-representable object of Stacks 0GM9, and uses no condition on U.

theorem isCartesianModule_of_mem_essImage_simplicialObject
    {F : SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf
      (J := (situation (P.toGrothendieck.over X)
        (associatedSimplicialObject.{u} U a)).totalTopology))
      (hypercoveringObjectRingedAugmentation P (associatedSimplicialObject.{u} U a) OC).O)}
    (hF : (hypercoveringObjectRingedAugmentation P (associatedSimplicialObject.{u} U a)
      OC).totalRingedHom.toModulesHom.pullbackModules.essImage F) :
    (situation (P.toGrothendieck.over X)
      (associatedSimplicialObject.{u} U a)).IsModuleFiberTransitionIso
        (hypercoveringObjectRingedAugmentation P (associatedSimplicialObject.{u} U a) OC).O F

CategoryTheory.SimplicialSemiRepresentable.full_pullbackModules_simplicialObject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringSimplicialObjectModuleDescent.lean, line 157. The attribute's comment: “a^* on sheaves of modules is full, for a hypercovering of X by a simplicial object of the site”.

Stacks 0DAB, the fullness half. In the situation above, the pullback a^* : Mod(O_X) ⥤ Mod(O) of sheaves of modules is full.

This is Stacks 0DA4 for the associated simplicial semi-representable object of Stacks 0GM9, whose hypercovering condition is exactly the three hypotheses.

theorem full_pullbackModules_simplicialObject
    (h₀ : Presieve.singleton (a.app (op ⦋0⦌)) ∈ P X)
    (h₁ : Presieve.singleton (oneSimplexToFiberProduct U a) ∈
      P (pullback (a.app (op ⦋0⦌)) (a.app (op ⦋0⦌))))
    (hmatch : ∀ n : ℕ, 1 ≤ n → Presieve.singleton (matchingMap U a n) ∈
      P ((((SimplicialObject.cosk n).obj (Over.lift U a)).obj (op ⦋n + 1⦌)).left)) :
    (hypercoveringObjectRingedAugmentation P (associatedSimplicialObject.{u} U a)
      OC).totalRingedHom.toModulesHom.pullbackModules.Full

CategoryTheory.SimplicialSemiRepresentable.fullyFaithfulPullbackModulesSimplicialObject, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringSimplicialObjectModuleDescent.lean, line 171. The attribute's comment: “a^* on sheaves of modules is fully faithful, for a hypercovering of X by a simplicial object of the site”.

Stacks 0DAB, full faithfulness of a^* on sheaves of modules.

def fullyFaithfulPullbackModulesSimplicialObject
    (h₀ : Presieve.singleton (a.app (op ⦋0⦌)) ∈ P X)
    (h₁ : Presieve.singleton (oneSimplexToFiberProduct U a) ∈
      P (pullback (a.app (op ⦋0⦌)) (a.app (op ⦋0⦌))))
    (hmatch : ∀ n : ℕ, 1 ≤ n → Presieve.singleton (matchingMap U a n) ∈
      P ((((SimplicialObject.cosk n).obj (Over.lift U a)).obj (op ⦋n + 1⦌)).left)) :
    (hypercoveringObjectRingedAugmentation P (associatedSimplicialObject.{u} U a)
      OC).totalRingedHom.toModulesHom.pullbackModules.FullyFaithful

CategoryTheory.SimplicialSemiRepresentable.essImage_pullbackModules_simplicialObject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringSimplicialObjectModuleDescent.lean, line 188. The attribute's comment: “every cartesian O-module is an a^*M, for a hypercovering of X by a simplicial object of the site”.

Stacks 0DAB, essential surjectivity onto the cartesian O-modules. In the situation above, every cartesian sheaf of O-modules on the total site is a pullback a^*M.

This is Stacks 0DA4 for the associated simplicial semi-representable object of Stacks 0GM9.

theorem essImage_pullbackModules_simplicialObject
    (h₀ : Presieve.singleton (a.app (op ⦋0⦌)) ∈ P X)
    (h₁ : Presieve.singleton (oneSimplexToFiberProduct U a) ∈
      P (pullback (a.app (op ⦋0⦌)) (a.app (op ⦋0⦌))))
    (hmatch : ∀ n : ℕ, 1 ≤ n → Presieve.singleton (matchingMap U a n) ∈
      P ((((SimplicialObject.cosk n).obj (Over.lift U a)).obj (op ⦋n + 1⦌)).left))
    {F : SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf
      (J := (situation (P.toGrothendieck.over X)
        (associatedSimplicialObject.{u} U a)).totalTopology)
      (hypercoveringObjectRingedAugmentation P (associatedSimplicialObject.{u} U a) OC).O))}
    (hF : (situation (P.toGrothendieck.over X)
      (associatedSimplicialObject.{u} U a)).IsModuleFiberTransitionIso
        (hypercoveringObjectRingedAugmentation P (associatedSimplicialObject.{u} U a) OC).O F) :
    (hypercoveringObjectRingedAugmentation P (associatedSimplicialObject.{u} U a)
      OC).totalRingedHom.toModulesHom.pullbackModules.essImage F

CategoryTheory.SimplicialSemiRepresentable.mem_essImage_pullbackModules_iff_isCartesianModule_simplicialObject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringSimplicialObjectModuleDescent.lean, line 211. The attribute's comment: “the essential image of a^* on sheaves of modules is exactly the cartesian O-modules, for a hypercovering of X by a simplicial object of the site”.

Stacks 0DAB, the essential image of a^* is exactly the cartesian O-modules. One inclusion is isCartesianModule_of_mem_essImage_simplicialObject, the other is essImage_pullbackModules_simplicialObject.

theorem mem_essImage_pullbackModules_iff_isCartesianModule_simplicialObject
    (h₀ : Presieve.singleton (a.app (op ⦋0⦌)) ∈ P X)
    (h₁ : Presieve.singleton (oneSimplexToFiberProduct U a) ∈
      P (pullback (a.app (op ⦋0⦌)) (a.app (op ⦋0⦌))))
    (hmatch : ∀ n : ℕ, 1 ≤ n → Presieve.singleton (matchingMap U a n) ∈
      P ((((SimplicialObject.cosk n).obj (Over.lift U a)).obj (op ⦋n + 1⦌)).left))
    (F : SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf
      (J := (situation (P.toGrothendieck.over X)
        (associatedSimplicialObject.{u} U a)).totalTopology)
      (hypercoveringObjectRingedAugmentation P (associatedSimplicialObject.{u} U a) OC).O))) :
    (hypercoveringObjectRingedAugmentation P (associatedSimplicialObject.{u} U a)
        OC).totalRingedHom.toModulesHom.pullbackModules.essImage F ↔
      (situation (P.toGrothendieck.over X)
        (associatedSimplicialObject.{u} U a)).IsModuleFiberTransitionIso
          (hypercoveringObjectRingedAugmentation P (associatedSimplicialObject.{u} U a) OC).O F

CategoryTheory.SimplicialSemiRepresentable.isIso_pullbackAdjPushforwardModules_unit_simplicialObject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringSimplicialObjectModuleDescent.lean, line 234. The attribute's comment: “M = a_ a^ M on sheaves of modules, for a hypercovering of X by a simplicial object of the site”.

Stacks 0DAB, a_* is a quasi-inverse on Mod(O_X). The unit M ⟶ a_*a^*M of the adjunction of Stacks 03D7 is an isomorphism for every sheaf of O_X-modules.

theorem isIso_pullbackAdjPushforwardModules_unit_simplicialObject
    (h₀ : Presieve.singleton (a.app (op ⦋0⦌)) ∈ P X)
    (h₁ : Presieve.singleton (oneSimplexToFiberProduct U a) ∈
      P (pullback (a.app (op ⦋0⦌)) (a.app (op ⦋0⦌))))
    (hmatch : ∀ n : ℕ, 1 ≤ n → Presieve.singleton (matchingMap U a n) ∈
      P ((((SimplicialObject.cosk n).obj (Over.lift U a)).obj (op ⦋n + 1⦌)).left)) :
    IsIso (AlgebraicGeometry.RingedToposHom.pullbackAdjPushforwardModules
      (hypercoveringObjectRingedAugmentation P (associatedSimplicialObject.{u} U a)
        OC).totalRingedHom).unit

CategoryTheory.SimplicialSemiRepresentable.isIso_pullbackAdjPushforwardModules_counit_app_simplicialObject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringSimplicialObjectModuleDescent.lean, line 251. The attribute's comment: “a^ a_ F = F for a cartesian O-module F, for a hypercovering of X by a simplicial object of the site”.

Stacks 0DAB, a_* is a quasi-inverse on the cartesian O-modules. The counit a^*a_*F ⟶ F of the adjunction of Stacks 03D7 is an isomorphism at every cartesian sheaf of O-modules.

theorem isIso_pullbackAdjPushforwardModules_counit_app_simplicialObject
    (h₀ : Presieve.singleton (a.app (op ⦋0⦌)) ∈ P X)
    (h₁ : Presieve.singleton (oneSimplexToFiberProduct U a) ∈
      P (pullback (a.app (op ⦋0⦌)) (a.app (op ⦋0⦌))))
    (hmatch : ∀ n : ℕ, 1 ≤ n → Presieve.singleton (matchingMap U a n) ∈
      P ((((SimplicialObject.cosk n).obj (Over.lift U a)).obj (op ⦋n + 1⦌)).left))
    {F : SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf
      (J := (situation (P.toGrothendieck.over X)
        (associatedSimplicialObject.{u} U a)).totalTopology)
      (hypercoveringObjectRingedAugmentation P (associatedSimplicialObject.{u} U a) OC).O))}
    (hF : (situation (P.toGrothendieck.over X)
      (associatedSimplicialObject.{u} U a)).IsModuleFiberTransitionIso
        (hypercoveringObjectRingedAugmentation P (associatedSimplicialObject.{u} U a) OC).O F) :
    IsIso ((AlgebraicGeometry.RingedToposHom.pullbackAdjPushforwardModules
      (hypercoveringObjectRingedAugmentation P (associatedSimplicialObject.{u} U a)
        OC).totalRingedHom).counit.app F)

Tag 0DAC, a lemma

Tag 0DAC in the Stacks Project.

CategoryTheory.SimplicialSemiRepresentable.isIso_derivedPullbackPushforwardUnit_app_of_isHypercoveringAugmentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringSimplicialObjectModuleCohomologicalDescentUnconditional.lean, line 297.

Stacks 0DAC. Let C be a site with fibre products, X an object of C, O_C a sheaf of commutative rings on C and a : U ⟶ X a hypercovering of X in C by a simplicial object U of C (Stacks, Section 85.21). With O_X = O_C|_{C/X}, O = a⁻¹O_X on the total site of U and a : (Sh((C/U)_total), O) ⟶ (Sh(C/X), O_X) the ringed augmentation of Stacks 0D9X, the canonical map

E ⟶ R a_* L a^* E

is an isomorphism for every object E of the unbounded derived category D(O_X) of sheaves of O_X-modules.

As in the source this is Stacks 0DA5 for the hypercovering of X by semi-representable objects with one summand in each degree that a determines (CategoryTheory.SimplicialSemiRepresentable.IsHypercoveringAugmentation.isHypercovering).

theorem isIso_derivedPullbackPushforwardUnit_app_of_isHypercoveringAugmentation
    (h : IsHypercoveringAugmentation P U a)
    (E : DerivedCategory (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf
      (J := (hypercoveringObjectRingedAugmentation P (associatedSimplicialObject.{u} U a)
        OC).augmentationRingedTopos.J))
      (hypercoveringObjectRingedAugmentation P (associatedSimplicialObject.{u} U a)
        OC).augmentationRingedTopos.O))) :
    IsIso ((AlgebraicGeometry.RingedToposHom.derivedPullbackPushforwardUnit
      (hypercoveringObjectRingedAugmentation P (associatedSimplicialObject.{u} U a)
        OC).totalRingedHom).app E)

Tag 0DAD, a lemma

Tag 0DAD in the Stacks Project.

CategoryTheory.SimplicialSemiRepresentable.derivedModuleSectionsOverObjectIsoOfIsHypercoveringAugmentation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringObjectModuleDerivedSections.lean, line 375.

Let C be a site with fibre products, X an object of C, O_C a sheaf of commutative rings on C and a : U ⟶ X a hypercovering of X in C by a simplicial object U of C. With O_X = O_C|_{C/X}, O = a⁻¹O_X on the total site (C/U)_total and a : (Sh((C/U)_total), O) ⟶ (Sh(C/X), O_X) the ringed augmentation, there is a canonical isomorphism

RΓ(X, E) = RΓ((C/U)_total, La^*E)

naturally in E in the unbounded derived category D(O_C). Here RΓ(X, -) takes values in D(O_C(X)), La^*E is La^* of the restriction of E to C/X, and the right hand side, which lives in D(Γ((C/U)_total, O)), is read in D(O_C(X)) through the canonical ring map O_C(X) ⟶ Γ((C/U)_total, O) (totalSectionsRingHom).

This is derivedModuleSectionsOverObjectIsoOfIsHypercovering for the hypercovering of X by semi-representable objects with one summand in each degree that a determines (IsHypercoveringAugmentation.isHypercovering).

def derivedModuleSectionsOverObjectIsoOfIsHypercoveringAugmentation
    (h : IsHypercoveringAugmentation P U a) :
    derivedModuleSectionsOverObject P X OC ≅
      Stacks.Cohomology.Localization.derivedRestriction (ringedSite P OC) X ⋙
        (RingedToposHom.leftDerivedPullbackOfIsIsoFSharp
          (X := totalTopos P (associatedSimplicialObject.{u} U a) OC)
          (Y := sliceTopos P (associatedSimplicialObject.{u} U a) OC)
          (augmentationHom P (associatedSimplicialObject.{u} U a) OC)).functor ⋙
        derivedTotalGlobalSections P (associatedSimplicialObject.{u} U a) OC ⋙
          (ModuleCat.restrictScalars
            (totalSectionsRingHom P (associatedSimplicialObject.{u} U a) OC)).mapDerivedCategory

CategoryTheory.SimplicialSemiRepresentable.derivedModuleSectionsOverObjectIsoOfIsHypercoveringAugmentation_hom_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringObjectModuleDerivedSections.lean, line 396. The attribute's comment: “the forward map of the isomorphism is the canonical one: RΓ(C/X, -) of the derived unit E|_X ⟶ Ra_La^(E|_X), between RΓ(X, E) = RΓ(C/X, E|_X) and the factorisation of Tag 08J6”.

At every E of D(O_C) the forward map of derivedModuleSectionsOverObjectIsoOfIsHypercoveringAugmentation is RΓ(C/X, -) of the derived unit E|_X ⟶ Ra_*La^*(E|_X) of the ringed augmentation, preceded by the comparison RΓ(X, E) = RΓ(C/X, E|_X) and followed by the factorisation RΓ(C/X, Ra_*-) = RΓ((C/U)_total, -).

theorem derivedModuleSectionsOverObjectIsoOfIsHypercoveringAugmentation_hom_app
    (h : IsHypercoveringAugmentation P U a)
    (E : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf OC))) :
    (derivedModuleSectionsOverObjectIsoOfIsHypercoveringAugmentation P OC U a h).hom.app E =
      (derivedModuleSectionsOverObjectIsoRestriction P OC).hom.app E ≫
        (derivedModuleSectionsAtId P X OC).map
          ((RingedToposHom.derivedPullbackPushforwardUnit
            (augmentationHom P (associatedSimplicialObject.{u} U a) OC)).app
            ((Stacks.Cohomology.Localization.derivedRestriction (ringedSite P OC) X).obj E)) ≫
        (derivedPushforwardModuleSectionsAtIdIso P (associatedSimplicialObject.{u} U a) OC).hom.app
          ((RingedToposHom.leftDerivedPullbackOfIsIsoFSharp
            (X := totalTopos P (associatedSimplicialObject.{u} U a) OC)
            (Y := sliceTopos P (associatedSimplicialObject.{u} U a) OC)
            (augmentationHom P (associatedSimplicialObject.{u} U a) OC)).functor.obj
              ((Stacks.Cohomology.Localization.derivedRestriction (ringedSite P OC) X).obj E))

Tag 0DAE, a lemma

Tag 0DAE in the Stacks Project.

CategoryTheory.SimplicialSemiRepresentable.exists_derivedPullbackEquivalence_isHypercoveringAugmentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/HypercoveringObjectModuleBoundedBelowEquivalence.lean, line 352.

Let C be a site with fibre products, given by a pretopology P, let X be an object of C, let O_C be a sheaf of commutative rings on C and let a : U ⟶ X be a hypercovering of X in C by a simplicial object U of C (IsHypercoveringAugmentation). Let O_X = O_C|_{C/X}, let O = a⁻¹O_X on the total site (C/U)_total and let a : (Sh((C/U)_total), O) ⟶ (Sh(C/X), O_X) be the ringed augmentation of Stacks 0D9X. Then

the cartesian O-modules form a weak Serre subcategory 𝒜 ⊂ Mod(O), and

the functor La^* defines an equivalence D⁺(O_X) ⟶ D⁺_𝒜(O) with quasi-inverse R a_*: there is an equivalence of categories whose functor, followed by the inclusion of D⁺_𝒜(O), is La^* on D⁺(O_X), and whose inverse, followed by the inclusion of D⁺(O_X), is R a_* on D⁺_𝒜(O).

Here D⁺(O_X) is the full subcategory of bounded below objects of D(O_X), and D⁺_𝒜(O) that of bounded below objects of D(O) all of whose cohomology modules are cartesian. The equivalence is derivedPullbackEquivalenceOfIsHypercoveringAugmentation.

theorem exists_derivedPullbackEquivalence_isHypercoveringAugmentation
    (h : IsHypercoveringAugmentation P U a) :
    ObjectProperty.IsWeakSerreClass
        ((situation (P.toGrothendieck.over X)
          (associatedSimplicialObject.{u} U a)).IsModuleFiberTransitionIso
          (hypercoveringObjectRingedAugmentation P (associatedSimplicialObject.{u} U a) OC).O) ∧
      ∃ e : (RingedToposHom.derivedPlusTarget
          (Y := sliceTopos P (associatedSimplicialObject.{u} U a) OC)).FullSubcategory ≌
          (RingedToposHom.derivedPlusProperty
          (X := totalTopos P (associatedSimplicialObject.{u} U a) OC)
          ((situation (P.toGrothendieck.over X)
          (associatedSimplicialObject.{u} U a)).IsModuleFiberTransitionIso
          (hypercoveringObjectRingedAugmentation P
            (associatedSimplicialObject.{u} U a) OC).O)).FullSubcategory,
        e.functor ⋙ (RingedToposHom.derivedPlusProperty
          (X := totalTopos P (associatedSimplicialObject.{u} U a) OC)
          ((situation (P.toGrothendieck.over X)
          (associatedSimplicialObject.{u} U a)).IsModuleFiberTransitionIso
          (hypercoveringObjectRingedAugmentation P (associatedSimplicialObject.{u} U a) OC).O)).ι =
          (RingedToposHom.derivedPlusTarget
          (Y := sliceTopos P (associatedSimplicialObject.{u} U a) OC)).ι ⋙
            (RingedToposHom.leftDerivedPullbackOfIsIsoFSharp
          (X := totalTopos P (associatedSimplicialObject.{u} U a) OC)
          (Y := sliceTopos P (associatedSimplicialObject.{u} U a) OC)
          (augmentationHom P (associatedSimplicialObject.{u} U a) OC)).functor ∧
        e.inverse ⋙ (RingedToposHom.derivedPlusTarget
          (Y := sliceTopos P (associatedSimplicialObject.{u} U a) OC)).ι =
          (RingedToposHom.derivedPlusProperty
          (X := totalTopos P (associatedSimplicialObject.{u} U a) OC)
          ((situation (P.toGrothendieck.over X)
          (associatedSimplicialObject.{u} U a)).IsModuleFiberTransitionIso
          (hypercoveringObjectRingedAugmentation P (associatedSimplicialObject.{u} U a) OC).O)).ι ⋙
            Stacks.Cohomology.DerivedPushforward.derivedPushforward
          (X := totalTopos P (associatedSimplicialObject.{u} U a) OC)
          (Y := sliceTopos P (associatedSimplicialObject.{u} U a) OC)
          (augmentationHom P (associatedSimplicialObject.{u} U a) OC)

Sources

Section85.23 Unbounded cohomological descent for hypercoverings #

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

Tag 0DC2, an item

Tag 0DC2 in the Stacks Project.

Stacks.Cohomology.CohomologicalDescent.IsStableUnderRestriction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/LocalSerreFamily.lean, line 100. The attribute's comment: “condition (1): restriction along U ⟶ V sends A_V into A_U”.

The first condition on a family of subcategories A_U of the categories of modules on the localizations of a ringed site: for every morphism f : U ⟶ V of the site, the restriction functor from modules on C/V to modules on C/U sends A_V into A_U.

def IsStableUnderRestriction (A : SliceProperties X) : Prop

Tag 0DC3, an item

Tag 0DC3 in the Stacks Project.

Stacks.Cohomology.CohomologicalDescent.IsLocalOnCoverings, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/LocalSerreFamily.lean, line 109. The attribute's comment: “condition (2): membership in A_U is local on coverings of U”.

The second condition on a family of subcategories A_U of the categories of modules on the localizations of a ringed site: for every covering {U_i ⟶ U} of the site, a module on C/U lies in A_U if and only if its restriction to C/U_i lies in A_{U_i} for every i.

def IsLocalOnCoverings (A : SliceProperties X) : Prop

Tag 0DC4, an item

Tag 0DC4 in the Stacks Project.

Stacks.Cohomology.CohomologicalDescent.LocalCohomologicalBound, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/LocalSerreFamily.lean, line 121. The attribute's comment: “condition (3): a locally covering set, with coverings acyclic for A_V above d_V”.

The third condition on a family of subcategories A_U of the categories of modules on the localizations of a ringed site: there is a set B of objects of the site such that every object has a covering by members of B, and every V in B carries an integer d_V and a cofinal system of coverings of V on whose members the cohomology of every module of A_V vanishes in degrees above d_V. The set, the bounds and the covering systems are stored as chosen data.

structure LocalCohomologicalBound (A : SliceProperties X)

Tag 0DC5, an example

Tag 0DC5 in the Stacks Project.

AlgebraicGeometry.Space.isStableUnderRestriction_spacesEtaleQuasicoherentSlices, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpacesEtaleQuasicoherentLocalSerre.lean, line 108. The attribute's comment: “property (1), i.e. condition 0DC2 for the family A_U of quasi-coherent modules on the slices of the spaces-etale site of an algebraic space: restriction along a morphism U -> V of the site sends A_V into A_U. NOT covered by this declaration: property (2) (condition 0DC3, locality on coverings), property (3) (condition 0DC4, the set B = Ob(C) with d_V = 0 and the cofinal affine coverings), and the standing assumption that each A_U is a weak Serre subcategory; no LocalSerreFamily is assembled. See the module documentation for why each of those is unreachable in this development -- in particular the positive-degree vanishing of the cohomology of a quasi-coherent module on an affine object of the etale site, the clause of Stacks 03DW that the source's reference to Stacks 01XB and Stacks 071Y supplies, is proved nowhere here and also blocks Stacks 0720 and Stacks 08EX”.

Stability under restriction. Let X be an algebraic space over a scheme S and let C = X_{spaces, étale} be the étale site on the algebraic spaces étale over X, with its structure sheaf. Then the family which assigns to an object U of C the quasi-coherent modules on C/U is stable under restriction: for a morphism f : U ⟶ V of C, the restriction functor from modules on C/V to modules on C/U sends quasi-coherent modules to quasi-coherent modules.

This is condition (1) of Tag 0DC1, i.e. the condition Stacks.Cohomology.CohomologicalDescent.IsStableUnderRestriction of Tag 0DC2, for this family.

theorem isStableUnderRestriction_spacesEtaleQuasicoherentSlices :
    Stacks.Cohomology.CohomologicalDescent.IsStableUnderRestriction
      (spacesEtaleRingedSite B S hS X) (spacesEtaleQuasicoherentSlices B S hS X)

AlgebraicGeometry.Space.spacesEtaleQuasicoherent_localSerre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpacesEtaleQuasicoherentLocalSerreFamily.lean, line 119.

Stacks 0DC5. Let S be a scheme, X an algebraic space over S, C = X_{spaces, étale} with its structure sheaf, and A_U the quasi-coherent 𝒪_U-modules on the slice C/U. Then each A_U is a weak Serre subcategory, and the three conditions of Stacks 0DC1 hold: restriction along a morphism U ⟶ V of C sends A_V into A_U (Stacks 0DC2); membership in A_U is local on coverings of U (Stacks 0DC3); and condition (3) (Stacks 0DC4) holds with B = Ob(C), d_V = 0 and Cov_V the coverings {V_i ⟶ V} with every V_i affine, that is, for such a covering, every p > 0 and every F in A_V, H^p(V_i, F) = 0.

theorem spacesEtaleQuasicoherent_localSerre :
    (∀ U, (spacesEtaleQuasicoherentSlices B S hS X U).IsWeakSerreClass) ∧
      IsStableUnderRestriction (spacesEtaleRingedSite B S hS X)
        (spacesEtaleQuasicoherentSlices B S hS X) ∧
      IsLocalOnCoverings (spacesEtaleRingedSite B S hS X)
        (spacesEtaleQuasicoherentSlices B S hS X) ∧
      ∃ b : LocalCohomologicalBound (spacesEtaleRingedSite B S hS X)
          (spacesEtaleQuasicoherentSlices B S hS X),
        b.B = Set.univ ∧ (∀ V hV, b.degreeBound V hV = 0) ∧
          ∀ V hV (𝒰 : PreZeroHypercover.{u + 1} V), (b.coverings V hV).cov 𝒰 ↔
            𝒰.sieve₀ ∈ (spacesEtaleRingedSite B S hS X).J V ∧
              ∀ i, IsAffineSpace B S hS (𝒰.X i).obj.left.1

Tag 0DC6, an example

Tag 0DC6 in the Stacks Project.

AlgebraicGeometry.Scheme.LocallyFiniteTypeEtale.localSerre_of_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/LocallyFiniteTypeFieldLocalSerreFamily.lean, line 262. The attribute's comment: “type (1): S the spectrum of a finite field”.

Stacks 0DC6, type (1): S the spectrum of a finite field. Let S ≅ Spec k with k a finite field, let Λ be a finite ring whose order is invertible on S, let C be the category of schemes locally of finite type over S with the étale topology, ringed by the constant sheaf Λ (ringedSite S Λ), and let A_U be the category of all sheaves of Λ-modules on C/U. Then the conditions (1), (2), (3) of Stacks 0DC1 hold: each A_U is a weak Serre subcategory, restriction along U ⟶ V sends A_V into A_U (Stacks 0DC2), membership in A_U is local on coverings (Stacks 0DC3), and (Stacks 0DC4) with B the set of quasi-compact objects, for V ∈ B the integer d_V = 1 + 2 dim(S) + sup_{v ∈ V} (trdeg_{κ(s)} κ(v) + 2 dim 𝒪_{V, v}), and Cov_V the étale coverings {V_i ⟶ V} with every V_i quasi-compact, H^p(V_i, F) = 0 for every {V_i ⟶ V} in Cov_V, every p > d_V and every F in A_V.

theorem localSerre_of_finite (k : Type u) [Field k] [Finite k] (e : S ≅ Spec (.of k)) :
    ∀ (Λ : Type u) [CommRing Λ] [Finite Λ], IsUnit (Nat.card Λ : Γ(S, ⊤)) →
      (∀ U, (allModules S Λ U).IsWeakSerreClass) ∧
        IsStableUnderRestriction (ringedSite S Λ) (allModules S Λ) ∧
        IsLocalOnCoverings (ringedSite S Λ) (allModules S Λ) ∧
        ∃ b : LocalCohomologicalBound (ringedSite S Λ) (allModules S Λ),
          b.B = {V | IsQuasiCompact ((liftedEquiv S).inverse.obj V)} ∧
          (∀ V hV, ∃ d : ℕ, b.degreeBound V hV = d ∧
            ((liftedEquiv S).inverse.obj V).obj.hom.etaleCohomologyBound = d) ∧
          ∀ V hV (𝒰 : PreZeroHypercover.{u + 1} V),
            (b.coverings V hV).cov 𝒰 ↔ IsQuasiCompactEtaleCovering 𝒰

AlgebraicGeometry.Scheme.LocallyFiniteTypeEtale.localSerre_of_isSepClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/LocallyFiniteTypeFieldLocalSerreFamily.lean, line 287. The attribute's comment: “type (2): S the spectrum of a separably closed field”.

Stacks 0DC6, type (2): S the spectrum of a separably closed field. Let S ≅ Spec k with k a separably closed field, let Λ be a finite ring whose order is invertible on S, let C be the category of schemes locally of finite type over S with the étale topology, ringed by the constant sheaf Λ (ringedSite S Λ), and let A_U be the category of all sheaves of Λ-modules on C/U. Then the conditions (1), (2), (3) of Stacks 0DC1 hold: each A_U is a weak Serre subcategory, restriction along U ⟶ V sends A_V into A_U (Stacks 0DC2), membership in A_U is local on coverings (Stacks 0DC3), and (Stacks 0DC4) with B the set of quasi-compact objects, for V ∈ B the integer d_V = 1 + 2 dim(S) + sup_{v ∈ V} (trdeg_{κ(s)} κ(v) + 2 dim 𝒪_{V, v}), and Cov_V the étale coverings {V_i ⟶ V} with every V_i quasi-compact, H^p(V_i, F) = 0 for every {V_i ⟶ V} in Cov_V, every p > d_V and every F in A_V.

theorem localSerre_of_isSepClosed (k : Type u) [Field k] [IsSepClosed k]
    (e : S ≅ Spec (.of k)) :
    ∀ (Λ : Type u) [CommRing Λ] [Finite Λ], IsUnit (Nat.card Λ : Γ(S, ⊤)) →
      (∀ U, (allModules S Λ U).IsWeakSerreClass) ∧
        IsStableUnderRestriction (ringedSite S Λ) (allModules S Λ) ∧
        IsLocalOnCoverings (ringedSite S Λ) (allModules S Λ) ∧
        ∃ b : LocalCohomologicalBound (ringedSite S Λ) (allModules S Λ),
          b.B = {V | IsQuasiCompact ((liftedEquiv S).inverse.obj V)} ∧
          (∀ V hV, ∃ d : ℕ, b.degreeBound V hV = d ∧
            ((liftedEquiv S).inverse.obj V).obj.hom.etaleCohomologyBound = d) ∧
          ∀ V hV (𝒰 : PreZeroHypercover.{u + 1} V),
            (b.coverings V hV).cov 𝒰 ↔ IsQuasiCompactEtaleCovering 𝒰

AlgebraicGeometry.Scheme.Hom.etaleCohomologyBound, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/LocallyFiniteTypeSite.lean, line 77. The attribute's comment: “the bound d_V”.

The degree 1 + 2 dim S + sup_v (trdeg_{κ(s)} κ(v) + 2 dim 𝒪_{X, v}) attached to a morphism f : X ⟶ S, where s is the image of v under f.

public def Hom.etaleCohomologyBound {X S : Scheme.{u}} (f : X ⟶ S) : WithBot ℕ∞

AlgebraicGeometry.Scheme.LocallyFiniteTypeEtale, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/LocallyFiniteTypeSite.lean, line 91. The attribute's comment: “the site C of schemes locally of finite type over S”.

The schemes locally of finite type over S, as a full subcategory of the schemes over S.

public abbrev LocallyFiniteTypeEtale (S : Scheme.{u}) : Type _

AlgebraicGeometry.Scheme.LocallyFiniteTypeEtale.topology, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/LocallyFiniteTypeSite.lean, line 103. The attribute's comment: “the étale topology on C”.

The étale topology on the schemes locally of finite type over S: the coarsest topology containing every sieve whose underlying family of schemes generates an étale covering.

public abbrev topology (S : Scheme.{u}) : GrothendieckTopology (LocallyFiniteTypeEtale S)

AlgebraicGeometry.Scheme.LocallyFiniteTypeEtale.IsQuasiCompact, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/LocallyFiniteTypeSite.lean, line 111. The attribute's comment: “the set B of quasi-compact objects”.

An object of the locally-finite-type étale site is quasi-compact when the scheme underlying it is.

public def IsQuasiCompact (V : LocallyFiniteTypeEtale S) : Prop

AlgebraicGeometry.Scheme.LocallyFiniteTypeEtale.IsQuasiCompactCovering, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/LocallyFiniteTypeSite.lean, line 116. The attribute's comment: “the coverings Cov_V”.

A family {U i ⟶ V} in the locally-finite-type étale site is a distinguished covering of V when every U i is quasi-compact and the family generates a covering sieve.

public def IsQuasiCompactCovering {V : LocallyFiniteTypeEtale S} {I : Type w}
    (U : I → LocallyFiniteTypeEtale S) (f : ∀ i, U i ⟶ V) : Prop

AlgebraicGeometry.Scheme.LocallyFiniteTypeEtale.exists_isQuasiCompactCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/LocallyFiniteTypeSite.lean, line 174. The attribute's comment: “every object of C is covered by members of B”.

Every scheme locally of finite type over S has an étale covering whose members are quasi-compact.

public theorem exists_isQuasiCompactCovering (V : LocallyFiniteTypeEtale S) :
    ∃ (I : Type u) (U : I → LocallyFiniteTypeEtale S) (f : ∀ i, U i ⟶ V),
      IsQuasiCompactCovering U f

AlgebraicGeometry.Scheme.LocallyFiniteTypeEtale.exists_isQuasiCompactCovering_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/LocallyFiniteTypeSite.lean, line 182. The attribute's comment: “Cov_V is a cofinal system of coverings”.

Every étale covering sieve of a scheme locally of finite type over S is refined by an étale covering whose members are quasi-compact.

public theorem exists_isQuasiCompactCovering_le (V : LocallyFiniteTypeEtale S) (R : Sieve V)
    (hR : R ∈ topology S V) :
    ∃ (I : Type (u + 1)) (U : I → LocallyFiniteTypeEtale S) (f : ∀ i, U i ⟶ V),
      IsQuasiCompactCovering U f ∧ Sieve.generate (Presieve.ofArrows U f) ≤ R

AlgebraicGeometry.Scheme.IsUnboundedDescentEtaleBase, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/LocallyFiniteTypeSiteBound.lean, line 175. The attribute's comment: “the four types of base scheme S”.

The types of base scheme of Stacks 0DC6. S is the spectrum of a finite field, the spectrum of a separably closed field, the spectrum of a strictly henselian Noetherian local ring, or the spectrum of a henselian Noetherian local ring with finite residue field.

def IsUnboundedDescentEtaleBase (S : Scheme.{u}) : Prop

AlgebraicGeometry.Scheme.IsUnboundedDescentEtaleBase.exists_natCast_eq_etaleCohomologyBound, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/LocallyFiniteTypeSiteBound.lean, line 211. The attribute's comment: “d_V is an integer for V in B”.

The bound d_V of Stacks 0DC6 is an integer. For S of one of the four types of Stacks 0DC6 and V a quasi-compact scheme locally of finite type over S, the bound d_V = 1 + 2 dim(S) + sup_{v ∈ V} (trdeg_{κ(s)} κ(v) + 2 dim 𝒪_{V, v}) is a natural number.

theorem exists_natCast_eq_etaleCohomologyBound {S : Scheme.{u}}
    (hS : IsUnboundedDescentEtaleBase S) (V : LocallyFiniteTypeEtale S)
    (hV : LocallyFiniteTypeEtale.IsQuasiCompact V) :
    ∃ d : ℕ, V.obj.hom.etaleCohomologyBound = d

AlgebraicGeometry.Scheme.LocallyFiniteTypeEtale.localSerre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/LocallyFiniteTypeSiteGabberUnconditional.lean, line 102. The attribute's comment: “all four types”.

Stacks 0DC6. Let S be the spectrum of a finite field, of a separably closed field, of a strictly henselian Noetherian local ring, or of a henselian Noetherian local ring with finite residue field, and let Λ be a finite ring whose order is invertible on S. On the ringed site (C, Λ) of schemes locally of finite type over S, the family A_U of all sheaves of Λ-modules satisfies conditions (1), (2), (3) of Stacks 0DC1, with B the quasi-compact objects, d_V = 1 + 2 dim(S) + sup_{v ∈ V} (trdeg_{κ(s)} κ(v) + 2 dim 𝒪_{V, v}) and Cov_V the étale coverings of V by quasi-compact objects.

theorem localSerre (Λ : Type u) [CommRing Λ] [Finite Λ]
    (hS : IsUnboundedDescentEtaleBase S) (hn : IsUnit (Nat.card Λ : Γ(S, ⊤))) :
    (∀ U, (allModules S Λ U).IsWeakSerreClass) ∧
      IsStableUnderRestriction (ringedSite S Λ) (allModules S Λ) ∧
      IsLocalOnCoverings (ringedSite S Λ) (allModules S Λ) ∧
      ∃ b : LocalCohomologicalBound (ringedSite S Λ) (allModules S Λ),
        b.B = {V | IsQuasiCompact ((liftedEquiv S).inverse.obj V)} ∧
        (∀ V hV, ∃ d : ℕ, b.degreeBound V hV = d ∧
          ((liftedEquiv S).inverse.obj V).obj.hom.etaleCohomologyBound = d) ∧
        ∀ V hV (𝒰 : PreZeroHypercover.{u + 1} V),
          (b.coverings V hV).cov 𝒰 ↔ IsQuasiCompactEtaleCovering 𝒰

Tag 0DC7, a lemma

Tag 0DC7 in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.exists_derivedPullbackEquivalence_localSerreFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/HypercoveringUnboundedEquivalence.lean, line 167.

Stacks 0DC7. Let (C, O_C) be a ringed site with equalizers and fibre products, and let A_U ⊂ Mod(O_U) be weak Serre subcategories satisfying conditions 0DC2, 0DC3 and 0DC4 (the fields of T : LocalSerreFamily), with A ⊂ Mod(O_C) the modules whose restriction to every C/U lies in A_U. Let K be a hypercovering of C, let a : ((C/K)_total, O) ⟶ (C, O_C) be the ringed augmentation of Remark 0D9W, with O = a⁻¹O_C, and let A_total ⊂ Mod(O) be the cartesian O-modules F whose restriction F_n lies in A_{K_n} = ∏_i A_{U_{n,i}} for every n. Then A_total is a weak Serre subcategory of Mod(O), and La^* defines an equivalence

D_A(O_C) ⟶ D_{A_total}(O)

with quasi-inverse Ra_*: there is an equivalence of the full subcategories of the unbounded derived categories on the objects with cohomology in A, respectively A_total, whose functor is the restriction of the derived pullback La^* and whose inverse is the restriction of the derived direct image Ra_*.

theorem exists_derivedPullbackEquivalence_localSerreFamily :
    (totalLocalSerre J H OC T).IsWeakSerreClass ∧
      ∃ e : (DerivedCategoryB.derivedCategoryB (baseLocalSerre J OC T)).FullSubcategory ≌
          (DerivedCategoryB.derivedCategoryB (totalLocalSerre J H OC T)).FullSubcategory,
        e.functor ⋙ (DerivedCategoryB.derivedCategoryB (totalLocalSerre J H OC T)).ι =
            (DerivedCategoryB.derivedCategoryB (baseLocalSerre J OC T)).ι ⋙
              (RingedToposHom.leftDerivedPullbackOfIsIsoFSharp
                (hypercoveringRingedAugmentation J H OC).totalRingedHom).functor ∧
          e.inverse ⋙ (DerivedCategoryB.derivedCategoryB (baseLocalSerre J OC T)).ι =
            (DerivedCategoryB.derivedCategoryB (totalLocalSerre J H OC T)).ι ⋙
              derivedPushforward (X := (hypercoveringSituation J H).totalRingedTopos
                (hypercoveringRingedAugmentation J H OC).O)
                (Y := (hypercoveringRingedAugmentation J H OC).augmentationRingedTopos)
                (hypercoveringRingedAugmentation J H OC).totalRingedHom

Stacks.Cohomology.CohomologicalDescent.isWeakSerreClass_cartesianDegreewiseModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/HypercoveringUnboundedLocalSerre.lean, line 122. The attribute's comment: “the class A_total of cartesian O-modules whose restriction to each simplicial component lies in the prescribed class there is a weak Serre subcategory of Mod(O). Two hypotheses are carried: hflat, left exactness of the pullback of modules along the transition morphism of each face map, which is the hypothesis in the shape this library's Tag 0D7J (2) takes it and is weaker than the source's flatness of the face transitions; and hA, that each A_n is a weak Serre subcategory. The family A_n is arbitrary, where the source takes the family A_{K_n} = prod_i A_{U_{n,i}} attached to a LocalSerreFamily, i.e. to Tags 0DC2, 0DC3 and 0DC4; assembling that particular family needs the module form of Tag 0D89 and is not available. NOT covered: the equivalence D_A(O_C) = D_{A_total}(O), the two assertions that La^ and Ra_ preserve the classes, and the identification of the two functors of the equivalence -- the unbounded engine of Tag 0D7V is stated for a RingedToposSiteHom and the augmentation of a hypercovering admits no such presentation. NOT covered either: that a^* induces an equivalence A = A_total, whose descent half needs the covering argument on the slices C/U_{n,i}”.

A_total is a weak Serre subcategory of Mod(O). Let O be a sheaf of commutative rings on the total site of a simplicial-site situation such that the pullback of modules along the transition morphism of each face map is left exact, and let A_n be a weak Serre subcategory of the category of modules on the degree-n component, for every n. Then the cartesian O-modules whose restriction to each component lies in the class there form a weak Serre subcategory of Mod(O).

theorem isWeakSerreClass_cartesianDegreewiseModules
    (hflat : ∀ (k : ℕ) (i : Fin (k + 2)),
      PreservesFiniteLimits
        ((S.transitionRingedToposHom O (SimplexCategory.δ i)).toModulesHom.pullbackModules))
    (hA : ∀ n : SimplexCategory, (A n).IsWeakSerreClass) :
    (cartesianDegreewiseModules S O A).IsWeakSerreClass

Stacks.Cohomology.CohomologicalDescent.isWeakSerreClass_cartesianDegreewiseModules_hypercovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/CohomologicalDescent/HypercoveringUnboundedLocalSerre.lean, line 174. The attribute's comment: “the class A_total is a weak Serre subcategory of Mod(O), at the total ringed site of a hypercovering with O = a^{-1}O_C, i.e. for the site and structure sheaf of Tag 0D9W. Same two hypotheses as the general form: hflat, left exactness of the pullback of modules along the transition morphism of each face map, and hA, that each A_n is a weak Serre subcategory; and the same restriction, that the family A_n is arbitrary rather than the source's prod_i A_{U_{n,i}}. None of the derived assertions of the tag are covered here”.

A_total is a weak Serre subcategory, at the total ringed site of a hypercovering. Let C be a site with equalizers and fibre products, let O_C be a sheaf of commutative rings on it and let K be a hypercovering of C; let a : (Sh((C/K)_total), O) ⟶ (Sh(C), O_C) be the ringed augmentation of Stacks 0D9W, so that O = a⁻¹O_C. For a family A_n of weak Serre subcategories of the categories of modules on the localizations C/K_n, the cartesian O-modules whose restriction F_n lies in A_n for every n form a weak Serre subcategory of Mod(O).

theorem isWeakSerreClass_cartesianDegreewiseModules_hypercovering {C : Type u} [SmallCategory C]
    [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasPullbacks C]
    (J : Pretopology C)
    (H : Stacks.CategoryTheory.Hypercovering.HypercoveringOfTerminal.{u, u} J)
    (OC : Sheaf J.toGrothendieck CommRingCat.{u})
    (A : ∀ n : SimplexCategory, ObjectProperty (SheafOfModules.{u}
      (componentRingSheaf (hypercoveringSituation J H)
        ((hypercoveringSituation J H).totalRingSheaf
          (hypercoveringRingedAugmentation J H OC).O) n)))
    (hflat : ∀ (k : ℕ) (i : Fin (k + 2)), PreservesFiniteLimits
      (((hypercoveringSituation J H).transitionRingedToposHom
        (hypercoveringRingedAugmentation J H OC).O
        (SimplexCategory.δ i)).toModulesHom.pullbackModules))
    (hA : ∀ n : SimplexCategory, (A n).IsWeakSerreClass) :
    (cartesianDegreewiseModules (hypercoveringSituation J H)
      (hypercoveringRingedAugmentation J H OC).O A).IsWeakSerreClass

Sources

LeanStacks.Cohomology.CohomologicalDescent.IsStableUnderRestriction · Stacks.Cohomology.CohomologicalDescent.IsLocalOnCoverings · Stacks.Cohomology.CohomologicalDescent.LocalCohomologicalBound · AlgebraicGeometry.Space.isStableUnderRestriction_spacesEtaleQuasicoherentSlices · AlgebraicGeometry.Space.spacesEtaleQuasicoherent_localSerre · AlgebraicGeometry.Scheme.LocallyFiniteTypeEtale.localSerre_of_finite · AlgebraicGeometry.Scheme.LocallyFiniteTypeEtale.localSerre_of_isSepClosed · AlgebraicGeometry.Scheme.Hom.etaleCohomologyBound

Section85.24 Glueing complexes #

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

Tag 0DC9, a situation

Tag 0DC9 in the Stacks Project.

AlgebraicGeometry.RingedSite.LocallyGiven, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/LocallyGivenDerived.lean, line 209.

Derived objects given locally on a category mapping to a ringed site, with isomorphisms on restriction satisfying the cocycle condition: a category B with a functor u : B ⥤ 𝒞, an object E_U of D(𝒪_{u(U)}) for every object U of B, and an isomorphism ρ_a : E_U|_{𝒞/u(V)} ⟶ E_V for every arrow a : V ⟶ U of B, such that ρ_{a ∘ b} = ρ_b ∘ ρ_a|_{𝒞/u(W)} for composable arrows b : W ⟶ V and a : V ⟶ U.

structure LocallyGiven.{uM, u, v, w, uB, vB} (X : RingedSite.{u, v, w})

Tag 0DCA, a lemma

Tag 0DCA in the Stacks Project.

AlgebraicGeometry.RingedSite.LocallyGiven.exists_unique_cartesian_summandIdentification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/LocallyGivenGlueing.lean, line 113.

Stacks 0DCA. In Situation 0DC9, assume the negative self-exts of every E_U in D(O_{u(U)}) vanish. Let L be a simplicial object of SR(B), let K = u(L) and let ((C/K)_total, O) be the ringed site of Remark 0D9W, with O = a⁻¹O_C. Then

there is a cartesian object E of D(O) whose restriction to D(O_{C/u(U_{n,i})}) is E_{U_{n,i}} compatibly with the isomorphisms ρ_a (a AlgebraicGeometry.RingedSite.LocallyGiven.SummandIdentification), and

such an E is unique up to unique isomorphism: for two of them, (E, σ) and (E', σ'), there is exactly one isomorphism E ≅ E' carrying σ to σ'.

theorem exists_unique_cartesian_summandIdentification
    (hneg : ∀ (U : G.B) (t : ℤ), 0 < t →
      ∀ g : (shiftFunctor (LocalDerivedCategory.{0} X (G.u.obj U)) t).obj (G.obj U) ⟶ G.obj U,
        g = 0) :
    (∃ E : DerivedCategory ((situation X.J (G.image L)).totalRingedTopos
        (structureSheaf X (G.image L))).Modules,
      (situation X.J (G.image L)).IsCartesianDerivedModule (structureSheaf X (G.image L)) E ∧
        Nonempty (G.SummandIdentification L E)) ∧
    ∀ (E E' : DerivedCategory ((situation X.J (G.image L)).totalRingedTopos
        (structureSheaf X (G.image L))).Modules),
      (situation X.J (G.image L)).IsCartesianDerivedModule (structureSheaf X (G.image L)) E →
      (situation X.J (G.image L)).IsCartesianDerivedModule (structureSheaf X (G.image L)) E' →
      ∀ (σ : G.SummandIdentification L E) (σ' : G.SummandIdentification L E'),
        ∃! ε : E ≅ E', ∀ (n : SimplexCategory) (i : (L.obj (op n)).I),
          (G.summandDerivedRestriction L n i).map
              (((situation X.J (G.image L)).derivedComponentModuleRestriction
                (structureSheaf X (G.image L)) n).map ε.hom) ≫ (σ'.iso n i).hom =
            (σ.iso n i).hom

Tag 0DCB, a lemma

Tag 0DCB in the Stacks Project.

AlgebraicGeometry.RingedSite.LocallyGiven.exists_unique_solution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/LocallyGivenBBDGlueing.lean, line 593.

Stacks 0DCB (BBD glueing lemma). In Situation 0DC9 — a ringed site (C, O_C), a category B with a functor u : B ⥤ C, objects E_U of D(O_{u(U)}) and isomorphisms ρ_a : E_U|_{C/u(V)} ⟶ E_V satisfying the cocycle condition — assume

C has equalizers and fibre products;

there is a morphism of sites f : C ⟶ D given by a continuous functor u : D ⥤ C (here f, with IsMorphismOfSites), such that D has equalizers and fibre products and u commutes with them, B is a full subcategory of D (a fully faithful i : B ⥤ D) with u : B ⥤ C the restriction of u (i ⋙ f = G.u), and every object of D has a covering whose members are objects of B;

for all U in B all negative self-exts of E_U in D(O_{u(U)}) are zero, that is, every map E_U[t] ⟶ E_U with t > 0 vanishes;

there exists t ∈ ℤ with H^i(E_U) = 0 for i < t and all U.

Then there exists a solution (E, ρ_U), and it is unique up to unique isomorphism: between two solutions there is exactly one isomorphism compatible with their identifications ρ_U.

theorem exists_unique_solution {X : RingedSite.{u, u, u}} [HasEqualizers X.C] [HasPullbacks X.C]
    (G : LocallyGiven.{0, u, u, u, u, u} X)
    {D : Type u} [SmallCategory D] [HasEqualizers D] [HasPullbacks D] (P : Pretopology D)
    (f : D ⥤ X.C) [IsMorphismOfSites.{u} f P.toGrothendieck X.J]
    [PreservesLimitsOfShape WalkingParallelPair f] [PreservesLimitsOfShape WalkingCospan f]
    (i : G.B ⥤ D) [i.Full] [i.Faithful] (hi : i ⋙ f = G.u)
    (hcover : ∀ V : D, ∃ (ι : Type u) (U : ι → G.B) (g : ∀ k, i.obj (U k) ⟶ V),
      Presieve.ofArrows (fun k ↦ i.obj (U k)) g ∈ P V)
    (hneg : ∀ (U : G.B) (t : ℤ), 0 < t →
      ∀ g : (shiftFunctor (LocalDerivedCategory.{0} X (G.u.obj U)) t).obj (G.obj U) ⟶ G.obj U,
        g = 0)
    (hbound : ∃ t : ℤ, ∀ (U : G.B) (q : ℤ), q < t → IsZero
      ((DerivedCategory.homologyFunctor (SheafOfModules.{u}
        ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over (G.u.obj U))) q).obj (G.obj U))) :
    Nonempty G.Solution ∧
      ∀ S S' : G.Solution, ∃! e : S.obj ≅ S'.obj, Solution.IsCompatibleIso G e

Tag 0DCC, a lemma

Tag 0DCC in the Stacks Project.

AlgebraicGeometry.RingedSite.LocallyGiven.exists_unique_solution_localSerre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/LocallyGivenUnboundedBBDGlueing.lean, line 125.

The unbounded BBD glueing lemma. In Situation 0DC9 — a ringed site (C, O_C), a category B with a functor u : B ⥤ C, objects E_U of D(O_{u(U)}) and isomorphisms ρ_a : E_U|_{C/u(V)} ⟶ E_V satisfying the cocycle condition — assume

C has equalizers and fibre products;

there is a morphism of sites f : C ⟶ D given by a continuous functor u : D ⥤ C (here f, with IsMorphismOfSites), such that D has equalizers and fibre products and u commutes with them, B is a full subcategory of D (a fully faithful i : B ⥤ D) with u : B ⥤ C the restriction of u (i ⋙ f = G.u), and every object of D has a covering whose members are objects of B;

all negative self-exts of E_U in D(O_{u(U)}) are zero, that is, every map E_U[t] ⟶ E_U with t > 0 vanishes;

there are weak Serre subcategories A_U ⊂ Mod(O_U) for all objects U of C satisfying conditions 0DC2, 0DC3 and 0DC4 (T : LocalSerreFamily X);

E_U ∈ D_{A_U}(O_U): every cohomology module of E_U lies in A_{u(U)}.

Then there exists a solution (E, ρ_U), and it is unique up to unique isomorphism: between two solutions there is exactly one isomorphism compatible with their identifications ρ_U.

theorem exists_unique_solution_localSerre {X : RingedSite.{u, u, u}} [HasEqualizers X.C]
    [HasPullbacks X.C] (G : LocallyGiven.{0, u, u, u, u, u} X)
    {D : Type u} [SmallCategory D] [HasEqualizers D] [HasPullbacks D] (P : Pretopology D)
    (f : D ⥤ X.C) [IsMorphismOfSites.{u} f P.toGrothendieck X.J]
    [PreservesLimitsOfShape WalkingParallelPair f] [PreservesLimitsOfShape WalkingCospan f]
    (i : G.B ⥤ D) [i.Full] [i.Faithful] (hi : i ⋙ f = G.u)
    (hcover : ∀ V : D, ∃ (ι : Type u) (U : ι → G.B) (g : ∀ k, i.obj (U k) ⟶ V),
      Presieve.ofArrows (fun k ↦ i.obj (U k)) g ∈ P V)
    (hneg : ∀ (U : G.B) (t : ℤ), 0 < t →
      ∀ g : (shiftFunctor (LocalDerivedCategory.{0} X (G.u.obj U)) t).obj (G.obj U) ⟶ G.obj U,
        g = 0)
    (T : LocalSerreFamily.{u} X)
    (hA : ∀ (U : G.B) (q : ℤ), T.A (G.u.obj U)
      ((DerivedCategory.homologyFunctor (SheafOfModules.{u}
        ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over (G.u.obj U))) q).obj (G.obj U))) :
    Nonempty G.Solution ∧
      ∀ S S' : G.Solution, ∃! e : S.obj ≅ S'.obj, Solution.IsCompatibleIso G e

Tag 0GMG, a lemma

Tag 0GMG in the Stacks Project.

AlgebraicGeometry.RingedSite.CoveringGlueing.existsUnique_glueing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/CoveringGlueing/Glueing.lean, line 315.

Let (C, O_C) be a ringed site with fibre products and {U_i ⟶ X}_{i ∈ I} a covering in C. For i ∈ I let E_i be an object of D(O_{U_i}) and for i, j ∈ I let ρ_{ij} : E_i|_{C/U_{ij}} ⟶ E_j|_{C/U_{ij}} be an isomorphism in D(O_{U_{ij}}), where U_{ij} = U_i ×_X U_j. Assume

the ρ_{ij} satisfy the cocycle condition on U_i ×_X U_j ×_X U_k for all i, j, k ∈ I,

SheafExt^p_{O_{U_i}}(E_i, E_i) = 0 for all p < 0 and i ∈ I (stated as the vanishing of the negative self-exts of E_i|_{C/V} for every object V over U_i), and

there exists a t ∈ ℤ such that H^p(E_i) = 0 for p < t and all i ∈ I.

Then there exists a pair (E, ρ_i), with E an object of D(O_X) and ρ_i : E|_{U_i} ⟶ E_i isomorphisms in D(O_{U_i}) compatible with the ρ_{ij}, and it is unique: two such pairs are isomorphic by exactly one isomorphism compatible with the ρ_i.

theorem existsUnique_glueing {X : RingedSite.{u, u, u}} [hX : HasPullbacks X.C] {X₀ : X.C}
    {ι : Type u} {U : ι → X.C} (f : ∀ i, U i ⟶ X₀) (E : ∀ i, LocalDerivedCategory.{0} X (U i))
    (ρ : ∀ i j, (derivedOverMap.{0} X (pullback.fst (f i) (f j))).obj (E i) ≅
      (derivedOverMap.{0} X (pullback.snd (f i) (f j))).obj (E j))
    (hf : Sieve.generate (Presieve.ofArrows U f) ∈ X.J X₀)
    (hρ : IsCocycle f ρ)
    (hExt : ∀ (i : ι) {V : X.C} (a : V ⟶ U i) (n : ℤ), n < 0 →
      Subsingleton (DerivedCategory.Ext ((derivedOverMap.{0} X a).obj (E i))
        ((derivedOverMap.{0} X a).obj (E i)) n))
    (hBound : ∃ t : ℤ, ∀ (i : ι) (n : ℤ), n < t →
      IsZero ((DerivedCategory.homologyFunctor _ n).obj (E i))) :
    Nonempty (Glueing f E ρ) ∧
      ∀ A B : Glueing f E ρ, ∃! e : A.obj ≅ B.obj, ∀ i : ι,
        (derivedOverMap.{0} X (f i)).map e.hom ≫ (B.iso i).hom = (A.iso i).hom

Sources

LeanAlgebraicGeometry.RingedSite.LocallyGiven · AlgebraicGeometry.RingedSite.LocallyGiven.exists_unique_cartesian_summandIdentification · AlgebraicGeometry.RingedSite.LocallyGiven.exists_unique_solution · AlgebraicGeometry.RingedSite.LocallyGiven.exists_unique_solution_localSerre · AlgebraicGeometry.RingedSite.CoveringGlueing.existsUnique_glueing

Section85.25 Proper hypercoverings in topology #

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

Tag 0DAF, a lemma

Tag 0DAF in the Stacks Project.

Stacks.Topology.LocallyQuasiCompactZariskiSituation.comparisonSquarePushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/ProperHypercovering/ComparisonSquare.lean, line 277.

Stacks Tag 0DAF. Let U be a simplicial object of LC and let a : U → X be an augmentation. There is a commutative diagram of topoi
Sh((LC_qc/U)_total) --h--> Sh(U_Zar)
        | a_qc                 | a
Sh(LC_qc/X)       --h₋₁--> Sh(X)
where the left vertical arrow is the augmentation qcAugmentation of Stacks Section 09X8, the right vertical arrow is the augmentation augmentationMorphism of Tag 09W4, the top arrow totalComparisonMorphism is the morphism of topoi of the continuous functor U_Zar → (LC_qc/U)_total, V ↦ V/U_n, and the bottom arrow qcTopologicalMorphism is the comparison morphism of the continuous functor X_Zar → LC_qc/X, V ↦ V/X. Commutativity is the natural isomorphism a_* ∘ h_* ≅ h₋₁,* ∘ a_qc,* of direct images.

def comparisonSquarePushforwardIso :
    (totalComparisonMorphism.{x} S U a).pushforward ⋙
        (augmentationMorphism (simplicialSpace S U) ((toTop S).obj X)
          (spaceAugmentation S U a)).pushforward ≅
      (qcAugmentation.{x} S U a).pushforward ⋙ (qcTopologicalMorphism.{u, w, 0} S X).pushforward

Stacks.Topology.Simplicial.qcSmallBottomMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/QcComparisonSquare.lean, line 203. The attribute's comment: “the lower horizontal arrow h_{-1} : Sh(LC_qc/X) → Sh(X) of the diagram”.

The bottom horizontal arrow of the diagram of Tag 0DAF, the comparison morphism of topoi h₋₁ = a_X : Sh(LC_qc/X) → Sh(X) of Section 09WY, with Sh(LC_qc/X) read as the sheaves on the localization of the small model.

def qcSmallBottomMorphism :
    MorphismOfTopoi (Sheaf (S.qcSite.smallOverTopology X) (Type u))
      (Sheaf (Opens.grothendieckTopology X.obj.obj) (Type u))

Stacks.Topology.Simplicial.qcComparisonSquarePushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/QcComparisonSquare.lean, line 711. The attribute's comment: “the commutative diagram of topoi, on direct images”.

Tag 0DAF. The diagram of topoi
Sh((LC_qc/U)_total) --h--> Sh(U_Zar)
        | a_qc                 | a
Sh(LC_qc/X)       --h₋₁--> Sh(X)
commutes: the direct image of h₋₁ ∘ a_qc is that of a ∘ h.

def qcComparisonSquarePushforwardIso :
    (qcAugmentationMorphism S X U a).pushforward ⋙ (qcSmallBottomMorphism S X).pushforward ≅
      (qcSmallComparisonMorphism S X U a).pushforward ⋙
        (qcZariskiAugmentation S X U a).pushforward

Stacks.Topology.Simplicial.qcComparisonSquareInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/QcComparisonSquare.lean, line 722. The attribute's comment: “the commutative diagram of topoi, on inverse images”.

Tag 0DAF, on inverse images: a_qc⁻¹ ∘ h₋₁⁻¹ ≅ h⁻¹ ∘ a⁻¹. The inverse images are left adjoint to the direct images, so this is the conjugate of qcComparisonSquarePushforwardIso.

def qcComparisonSquareInverseImageIso :
    (qcZariskiAugmentation S X U a).inverseImage ⋙
        (qcSmallComparisonMorphism S X U a).inverseImage ≅
      qcSmallTopologicalInverseImage S X ⋙ (qcAugmentationMorphism S X U a).inverseImage

Stacks.Topology.Simplicial.exists_qcComparisonSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/QcComparisonSquare.lean, line 763. The attribute's comment: “for an arbitrary simplicial object U of LC and augmentation a : U → X: a site LC_qc containing X and the U_n exists, and for it the diagram of topoi commutes”.

Tag 0DAF for an arbitrary simplicial object of LC. Let U be a simplicial object of LC and let a : U → X be an augmentation. Then a site LC_qc of Tag 09X2 can be chosen containing X and every U_n, and for it the square of topoi h₋₁ ∘ a_qc = a ∘ h commutes, both on direct images and on inverse images. The right-hand column is the augmentation of U_Zar towards X of Tag 09W4 for the underlying simplicial space of U itself: the simplicial space of the lift is U followed by the inclusion of LC into topological spaces, on the nose.

theorem exists_qcComparisonSquare (Y : SimplicialObject LocallyQuasiCompactHausdorff.{u})
    (T : LocallyQuasiCompactHausdorff.{u}) (b : Y ⟶ (SimplicialObject.const _).obj T) :
    ∃ (S : LocallyQuasiCompactZariskiSituation.{u, u + 1} (Set.range Y.obj ∪ {T})
        Cardinal.stacksBound) (hY : ∀ n, S.qcSite.Contains (Y.obj n))
      (hT : S.qcSite.Contains T),
      qcSimplicialSpace S (qcLift S Y hY) = Y ⋙ locallyQuasiCompactHausdorffToTop ∧
      Nonempty ((qcAugmentationMorphism S ⟨T, hT⟩ (qcLift S Y hY)
          (qcLiftAugmentation S b hY hT)).pushforward ⋙
            (qcSmallBottomMorphism S ⟨T, hT⟩).pushforward ≅
        (qcSmallComparisonMorphism S ⟨T, hT⟩ (qcLift S Y hY)
          (qcLiftAugmentation S b hY hT)).pushforward ⋙
            (qcZariskiAugmentation S ⟨T, hT⟩ (qcLift S Y hY)
              (qcLiftAugmentation S b hY hT)).pushforward) ∧
      Nonempty ((qcZariskiAugmentation S ⟨T, hT⟩ (qcLift S Y hY)
          (qcLiftAugmentation S b hY hT)).inverseImage ⋙
            (qcSmallComparisonMorphism S ⟨T, hT⟩ (qcLift S Y hY)
              (qcLiftAugmentation S b hY hT)).inverseImage ≅
        qcSmallTopologicalInverseImage S ⟨T, hT⟩ ⋙
          (qcAugmentationMorphism S ⟨T, hT⟩ (qcLift S Y hY)
            (qcLiftAugmentation S b hY hT)).inverseImage)

Stacks.Topology.Simplicial.qcSmallComparisonMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/QcSmallTotalSiteComparison.lean, line 477. The attribute's comment: “the upper horizontal arrow h : Sh((LC_qc/U)_total) → Sh(U_Zar) of the diagram”.

The upper horizontal arrow of the diagram of Tag 0DAF, the morphism of topoi h : Sh((LC_qc/U)_total) ⟶ Sh(U_Zar) of the comparison functor, with (LC_qc/U)_total formed in the small model as in Section 09X8. Its direct image is restriction along the comparison functor.

def qcSmallComparisonMorphism :
    MorphismOfTopoi (Sheaf (qcSmallTotalTopology S X U a) (Type u))
      (Sheaf (SimplicialOpen.grothendieckTopology (qcSimplicialSpace S U)) (Type u))

Tag 0DAG, a lemma

Tag 0DAG in the Stacks Project.

Stacks.Topology.Simplicial.ProperHypercovering.inverseImage_fullyFaithful_of_isHypercovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/ProperHypercoveringFullyFaithful.lean, line 221. The attribute's comment: “sheaves of sets”.

Stacks 0DAG, sheaves of sets. Let U be a simplicial object of LC and a : U ⟶ X an augmentation which is a proper hypercovering of X. Then a^{-1} : Sh(X) ⥤ Sh(U_Zar) is fully faithful, its essential image consists exactly of the cartesian sheaves, and a_* is a quasi-inverse: the unit of a^{-1} ⊣ a_* is invertible, and so is its counit at every cartesian sheaf. Here a : Sh(U_Zar) ⟶ Sh(X) is the morphism of topoi of Tag 09W4.

theorem inverseImage_fullyFaithful_of_isHypercovering
    (hyp : MorphismProperty.IsHypercovering properSurjective ⟨Y, X, a⟩) :
    (inverseImage Y X a).Full ∧ (inverseImage Y X a).Faithful ∧
      (∀ G, (inverseImage Y X a).essImage G ↔ IsCartesian (U Y) G) ∧
      (∀ F, IsIso ((augmentationTopoi Y X a).adj.unit.app F)) ∧
      (∀ G, IsCartesian (U Y) G → IsIso ((augmentationTopoi Y X a).adj.counit.app G))

Stacks.Topology.Simplicial.ProperHypercovering.abelianInverseImage_fullyFaithful_of_isHypercovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/ProperHypercoveringFullyFaithful.lean, line 238. The attribute's comment: “sheaves of abelian groups”.

Stacks 0DAG, sheaves of abelian groups. Let U be a simplicial object of LC and a : U ⟶ X an augmentation which is a proper hypercovering of X. Then a^{-1} : Ab(X) ⥤ Ab(U_Zar) is fully faithful, its essential image consists exactly of the cartesian abelian sheaves, and a_* is a quasi-inverse: the unit of a^{-1} ⊣ a_* is invertible, and so is its counit at every cartesian abelian sheaf.

theorem abelianInverseImage_fullyFaithful_of_isHypercovering
    (hyp : MorphismProperty.IsHypercovering properSurjective ⟨Y, X, a⟩) :
    (abelianInverseImage Y X a).Full ∧ (abelianInverseImage Y X a).Faithful ∧
      (∀ G, (abelianInverseImage Y X a).essImage G ↔ IsCartesianAb (U Y) G) ∧
      (∀ F, IsIso ((abelianAdjunction Y X a).unit.app F)) ∧
      (∀ G, IsCartesianAb (U Y) G → IsIso ((abelianAdjunction Y X a).counit.app G))

Tag 09XS, a lemma

Tag 09XS in the Stacks Project.

Stacks.Topology.Simplicial.ProperHypercovering.isIso_derivedAdjunction_unit_app_of_isHypercovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/ProperHypercovering/DerivedUnit.lean, line 556.

Let U be a simplicial object of the category LC of Hausdorff, locally quasi-compact spaces and let a : U → X be an augmentation. If a : U → X gives a proper hypercovering of X, then for K in D⁺(X) the canonical map

K ⟶ Ra_*(a^{-1}K)

is an isomorphism, where a : Sh(U_Zar) → Sh(X) is the morphism of topoi of Stacks 09W4.

Here U = Y; the proper hypercovering condition of Stacks Section 09XA is MorphismProperty.IsHypercovering properSurjective; D⁺(X) is the bounded below derived category of abelian sheaves on X, for any model of the derived categories involved; a^{-1} is the exact inverse image of abelian sheaves of the morphism of topoi of Stacks 09W4 applied degreewise, and Ra_* is the right derived functor on bounded below derived categories of its direct image. The canonical map is the unit at K of the adjunction a^{-1} ⊣ Ra_* (derivedAdjunction).

By Leray's acyclicity lemma (Stacks 015E) the statement reduces to the underived unit F ⟶ a_* a^{-1} F being an isomorphism, which is Stacks 0DAG, and to R^q a_*(a^{-1}F) = 0 for q > 0, isZero_rightDerived_abelianDirectImage_of_isHypercovering, which is the computation of the source through the diagram of Stacks 0DAF; see the module documentation.

theorem isIso_derivedAdjunction_unit_app_of_isHypercovering
    (hyp : MorphismProperty.IsHypercovering properSurjective ⟨Y, X, a⟩)
    (K : DerivedCategory.Plus (Sheaf (Opens.grothendieckTopology
      (locallyQuasiCompactHausdorffToTop.obj X)) AddCommGrpCat.{u})) :
    IsIso ((derivedAdjunction Y X a).unit.app K)

Tag 09XC, a lemma

Tag 09XC in the Stacks Project.

Stacks.Topology.Simplicial.ProperHypercovering.derivedGlobalSectionsIsoOfIsHypercovering, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/ProperHypercovering/DerivedDescent.lean, line 134.

Stacks Project, Tag 09XC. Let U be a simplicial object of LC and let a : U → X be an augmentation. If U is a proper hypercovering of X, then

RΓ(X, K) = RΓ(U_Zar, a^{-1}K)

for K ∈ D⁺(X), where a : Sh(U_Zar) → Sh(X) is the morphism of topoi of Lemma 09W4.

Here U = Y, X = T and a = b; the proper hypercovering condition of Stacks Section 09XA is MorphismProperty.IsHypercovering properSurjective, a^{-1} is the inverse image of abelian sheaves along the morphism of topoi of Stacks 09W4, extended to D⁺ degreewise because it is exact, and RΓ(X, -), RΓ(U_Zar, -) are the right derived functors on D⁺ of the global sections functors of the space X and of the site U_Zar. The derived categories are arbitrary models. The isomorphism is the canonical one: its forward map is the pullback on derived sections, RΓ(X, -) of the unit K → Ra_*a^{-1}K followed by the factorization RΓ(U_Zar, -) = RΓ(X, -) ∘ Ra_* of Stacks 08J6 (derivedGlobalSectionsIsoOfIsHypercovering_hom). It is invertible because the unit is, by isIso_derivedAdjunction_unit_app_of_isHypercovering (Stacks 09XS).

def derivedGlobalSectionsIsoOfIsHypercovering
    (hyp : MorphismProperty.IsHypercovering properSurjective ⟨Y, T, b⟩) :
    (Sheaf.Γ (Opens.grothendieckTopology (locallyQuasiCompactHausdorffToTop.obj T))
        AddCommGrpCat.{u}).rightDerivedFunctorPlus ≅
      (abelianInverseImage Y T b).mapDerivedCategoryPlus ⋙
        (Sheaf.Γ (SimplicialOpen.grothendieckTopology (U Y))
          AddCommGrpCat.{u}).rightDerivedFunctorPlus

Tag 0DAH, a lemma

Tag 0DAH in the Stacks Project.

Stacks.Topology.Simplicial.ProperHypercovering.derivedInverseImage_equivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/ProperHypercovering/DerivedEquivalence.lean, line 85.

Stacks Project, Tag 0DAH. Let U be a simplicial object of the category LC of Hausdorff, locally quasi-compact spaces and let a : U → X be an augmentation. Let 𝒜 ⊂ Ab(U_Zar) denote the weak Serre subcategory of cartesian abelian sheaves. If U is a proper hypercovering of X, then the functor a⁻¹ defines an equivalence

D⁺(X) ⟶ D⁺_𝒜(U_Zar)

with quasi-inverse R a_*, where a : Sh(U_Zar) → Sh(X) is the morphism of topoi of Stacks 09W4.

Here U = Y; the proper hypercovering condition of Stacks Section 09XA is MorphismProperty.IsHypercovering properSurjective; 𝒜 is IsCartesianAb (U Y), which is a weak Serre subcategory (the first conjunct); D⁺_𝒜(U_Zar) is cartesianPlus Y, the objects of D⁺(U_Zar) all of whose cohomology sheaves are cartesian; a⁻¹ is the exact functor (abelianInverseImage Y X a).mapDerivedCategoryPlus and R a_* the total right derived functor of a_*. The derived categories are arbitrary models.

theorem derivedInverseImage_equivalence
    (hyp : MorphismProperty.IsHypercovering properSurjective ⟨Y, X, a⟩) :
    ObjectProperty.IsWeakSerreClass (IsCartesianAb (U Y)) ∧
      ∃ e : DerivedCategory.Plus (Sheaf (Opens.grothendieckTopology
          (locallyQuasiCompactHausdorffToTop.obj X)) AddCommGrpCat.{u}) ≌
            (cartesianPlus Y).FullSubcategory,
        e.functor = (cartesianPlus Y).lift (abelianInverseImage Y X a).mapDerivedCategoryPlus
          (cartesianPlus_mapDerivedCategoryPlus_obj Y X a) ∧
        e.inverse = (cartesianPlus Y).ι ⋙ (abelianDirectImage Y X a).rightDerivedFunctorPlus

Tag 09XB, a lemma

Tag 09XB in the Stacks Project.

Stacks.Topology.Simplicial.properHypercoveringSpectralSequence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/ProperHypercovering/SpectralSequence.lean, line 340.

Let U be a simplicial object of the category LC of Hausdorff, locally quasi-compact spaces and let a : U → X be an augmentation. Let F be an abelian sheaf on X and let F_n be its pullback to U_n. If U is a proper hypercovering of X, there is a canonical spectral sequence

E_1^{p,q} = H^q(U_p, F_p)

converging to H^{p+q}(X, F).

Here U = Y, X = T and a = b; the proper hypercovering condition of Stacks Section 09XA is MorphismProperty.IsHypercovering properSurjective. The spectral sequence is a functor of F, its first page is identified with H^q(U_p, F_p) naturally in F, and it abuts to H^n(X, F) (SpectralSequence.AbutsTo, the convergence of Stacks 01F2).

def properHypercoveringSpectralSequence
    (hyp : MorphismProperty.IsHypercovering ProperHypercovering.properSurjective ⟨Y, T, b⟩) :
    ProperHypercoveringSpectralSequence Y T b

Sources

LeanStacks.Topology.LocallyQuasiCompactZariskiSituation.comparisonSquarePushforwardIso · Stacks.Topology.Simplicial.qcSmallBottomMorphism · Stacks.Topology.Simplicial.qcComparisonSquarePushforwardIso · Stacks.Topology.Simplicial.qcComparisonSquareInverseImageIso · Stacks.Topology.Simplicial.exists_qcComparisonSquare · Stacks.Topology.Simplicial.qcSmallComparisonMorphism · Stacks.Topology.Simplicial.ProperHypercovering.inverseImage_fullyFaithful_of_isHypercovering · Stacks.Topology.Simplicial.ProperHypercovering.abelianInverseImage_fullyFaithful_of_isHypercovering

Section85.27 Descent in terms of simplicial schemes #

Section 85.27 of the Stacks Project, Tag 0248. 5 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 0249, a definition

Tag 0249 in the Stacks Project.

Declarations registered for the tag:

CategoryTheory.NatTrans.Equifibered registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch85.lean, line 19 (StacksFrontier): “more general: an equifibered natural transformation of functors J ⥤ C; here J = SimplexCategoryᵒᵖ and C = Scheme, so a morphism of simplicial schemes”. References: EGA I (10.12.2), “more general”.

Tag 07TC, a lemma

Tag 07TC in the Stacks Project.

Stacks.Simplicial.Descent.cartesianObjectsOverEquivalenceDescentData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/CartesianDescentData.lean, line 1179.

Cartesian simplicial objects over X are equivalent to descent data consisting of an object over X₀ and a normalized transition isomorphism satisfying the cocycle condition.

noncomputable def cartesianObjectsOverEquivalenceDescentData (X : SimplicialObject C) :
    ObjectProperty.FullSubcategory (fun Y : Over X ↦ Y.hom.Equifibered) ≌
      DescentDatum X

Tag 024A, a definition

Tag 024A in the Stacks Project.

AlgebraicGeometry.simplicialScheme, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/DescentViaSimplicialSchemes.lean, line 72.

The simplicial scheme (X/S)_• associated to f : X ⟶ S: its degree-n part is the (n + 1)-fold fibre product of X over S, i.e. it is the Čech nerve of f.

def simplicialScheme : SimplicialObject Scheme.{u}

Tag 024B, a lemma

Tag 024B in the Stacks Project.

AlgebraicGeometry.SimplicialScheme.toDescentDatum, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/DescentViaSimplicialSchemes.lean, line 555. The attribute's comment: “the descent datum (V, φ) attached to a descent datum on (X/S)_•”.

The descent datum (V, φ) relative to f : X ⟶ S attached to a descent datum on (X/S)_•.

def toDescentDatum (D : Stacks.Simplicial.Descent.DescentDatum (simplicialScheme f)) :
    AlgebraicGeometry.DescentDatum f

AlgebraicGeometry.SimplicialScheme.isPullback_cartesianLeft, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/DescentViaSimplicialSchemes.lean, line 623. The attribute's comment: “the isomorphism V ×_S X ← Y_1 given by (d¹_1, pr_1 ∘ π_1)”.

(d¹₁, pr₁ ∘ π₁) : Y₁ ⟶ V ×_S X is an isomorphism.

lemma isPullback_cartesianLeft (Y : Stacks.Simplicial.Descent.Cartesian (simplicialScheme f)) :
    IsPullback (Y.1.left.δ (1 : Fin 2)) (Y.1.hom.app (op ⦋1⦌) ≫ proj f 1 1)
      ((descentObj (cartesianDatum Y)).hom ≫ f) f

AlgebraicGeometry.SimplicialScheme.isPullback_cartesianRight, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/DescentViaSimplicialSchemes.lean, line 632. The attribute's comment: “the isomorphism Y_1 → X ×_S V given by (pr_0 ∘ π_1, d¹_0)”.

(pr₀ ∘ π₁, d¹₀) : Y₁ ⟶ X ×_S V is an isomorphism.

lemma isPullback_cartesianRight (Y : Stacks.Simplicial.Descent.Cartesian (simplicialScheme f)) :
    IsPullback (Y.1.hom.app (op ⦋1⦌) ≫ proj f 1 0) (Y.1.left.δ (0 : Fin 2)) f
      ((descentObj (cartesianDatum Y)).hom ≫ f)

AlgebraicGeometry.SimplicialScheme.cartesian_actMap, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/DescentViaSimplicialSchemes.lean, line 642. The attribute's comment: “φ is the isomorphism resulting from d¹_0 and π_1”.

φ is the isomorphism induced by d¹₀ and π₁: a point of V ×_S X lifted to a point y of Y₁ is sent to the zeroth face of y.

lemma cartesian_actMap (Y : Stacks.Simplicial.Descent.Cartesian (simplicialScheme f)) {W : Over S}
    (q : W ⟶ (Over.map f).obj (descentObj (cartesianDatum Y)) ⨯ Over.mk f)
    (y : W.left ⟶ Y.1.left.obj (op ⦋1⦌))
    (h₁ : y ≫ Y.1.left.δ (1 : Fin 2) = (q ≫ prod.fst).left)
    (h₂ : y ≫ Y.1.hom.app (op ⦋1⦌) ≫ proj f 1 1 = (q ≫ prod.snd).left) :
    (q ≫ actMap (cartesianDatum Y)).left = y ≫ Y.1.left.δ (0 : Fin 2)

AlgebraicGeometry.SimplicialScheme.cartesianDescentDatum, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/DescentViaSimplicialSchemes.lean, line 681. The attribute's comment: “(V, φ) is a descent datum relative to X ⟶ S, for cartesian Y over (X/S)_•”.

(V, φ) is a descent datum relative to X ⟶ S, for V = Y₀ over X and φ the isomorphism V ×_S X ≅ X ×_S V induced by d¹₀, d¹₁ and π₁ on a cartesian simplicial scheme Y over (X/S)_•.

def cartesianDescentDatum (Y : Stacks.Simplicial.Descent.Cartesian (simplicialScheme f)) :
    AlgebraicGeometry.DescentDatum f

Tag 024C, a lemma

Tag 024C in the Stacks Project.

AlgebraicGeometry.SimplicialScheme.cartesianDescentDatumFunctor_isEquivalence, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/CartesianSchemesDescentEquivalence.lean, line 748.

The construction of Lemma 024B, from cartesian schemes over (X/S)_• to descent data relative to X/S, is an equivalence of categories.

instance cartesianDescentDatumFunctor_isEquivalence (f : X ⟶ S) :
    (cartesianDescentDatumFunctor f).IsEquivalence

Sources

LeanCategoryTheory.NatTrans.Equifibered · Stacks.Simplicial.Descent.cartesianObjectsOverEquivalenceDescentData · AlgebraicGeometry.simplicialScheme · AlgebraicGeometry.SimplicialScheme.toDescentDatum · AlgebraicGeometry.SimplicialScheme.isPullback_cartesianLeft · AlgebraicGeometry.SimplicialScheme.isPullback_cartesianRight · AlgebraicGeometry.SimplicialScheme.cartesian_actMap · AlgebraicGeometry.SimplicialScheme.cartesianDescentDatum

Section85.28 Quasi-coherent modules on simplicial schemes #

Section 85.28 of the Stacks Project, Tag 07TE. 4 tags here are carried by 10 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07TI, a lemma

Tag 07TI in the Stacks Project.

AlgebraicGeometry.SimplicialScheme.isQuasicoherentOnSite_modulePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ZariskiPullbackQuasicoherent.lean, line 51. The attribute's comment: “for a quasi-coherent module, which is the hypothesis the source states; proved through the localization 04J0 of a morphism of ringed sites at an object, in the form asking only that every object of the source site admit an arrow into the image of the functor, applied on the equi-universe model of the total Zariski site, and not through 0D7M”.

Let f : V ⟶ U be a morphism of simplicial schemes and let F be a quasi-coherent module on U_Zar. Then the pullback f^*F is a quasi-coherent module on V_Zar.

public theorem isQuasicoherentOnSite_modulePullback (f : V ⟶ U) {F : Modules U}
    (hF : F.IsQuasicoherentOnSite) :
    ((modulePullback f).obj F).IsQuasicoherentOnSite

AlgebraicGeometry.SimplicialScheme.isQuasicoherentOnSite_modulePullback_of_presentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ZariskiRingedTopos.lean, line 316. The attribute's comment: “for a module admitting a GLOBAL presentation on the total Zariski site, a strengthening of the source's hypothesis that it be quasi-coherent, i.e. presented only locally. The source's statement is proved in full at AlgebraicGeometry.SimplicialScheme.isQuasicoherentOnSite_modulePullback, through the localization 04J0 of a morphism of ringed sites at an object on the equi-universe model of the total Zariski site; this is the direct specialization of 03DO, which needs no localization”.

Stacks 07TI for a globally presented module. For a morphism of simplicial schemes f : V ⟶ U and a sheaf of 𝒪_U-modules on U_Zar admitting a global presentation, the pullback f^*F is a quasi-coherent sheaf of 𝒪_V-modules on V_Zar.

public theorem isQuasicoherentOnSite_modulePullback_of_presentation (f : V ⟶ U)
    {F : Modules U} (P : F.Presentation) :
    ((modulePullback f).obj F).IsQuasicoherentOnSite

Tag 07TJ, a lemma

Tag 07TJ in the Stacks Project.

AlgebraicGeometry.SimplicialScheme.isQuasicoherent_componentModule_modulePushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ZariskiPushforwardQuasicoherent.lean, line 185. The attribute's comment: “the quasi-coherence of the COMPONENTS of the pushforward only: (f_*G)_n is a quasi-coherent module on U_n as soon as f_n is quasi-compact and quasi-separated and G_n is quasi-coherent. This is the source's identification F_n = f_{n,*}G_n (09VP, here componentModulePushforwardIso) together with 01LC, and it needs neither the cartesian hypothesis on f nor the flatness of the face maps of U. What is NOT proved is that f_*G is quasi-coherent on the total Zariski site: the source gets that from 0D7M, of which this development has only the right-hand side (CategoryTheory.SimplicialSiteSituation.IsCartesianWithQuasicoherentComponents, neither direction of the equivalence), and the other half of that right-hand side -- that f_*G is cartesian, which is where 02KH and the flatness of the face maps enter -- cannot even be stated here, the development carrying no cartesian-module predicate for the total Zariski site of a simplicial scheme”.

Stacks 07TJ for the components of the pushforward. Let f : V ⟶ U be a morphism of simplicial schemes and G a sheaf of 𝒪_V-modules on the total Zariski site. If f_n is quasi-compact and quasi-separated and the degree-n component G_n is a quasi-coherent 𝒪_{V_n}-module, then the degree-n component (f_*G)_n of the pushforward is a quasi-coherent 𝒪_{U_n}-module.

public theorem isQuasicoherent_componentModule_modulePushforward (f : V ⟶ U)
    (n : SimplexCategoryᵒᵖ) [QuasiCompact (f.app n)] [QuasiSeparated (f.app n)]
    (G : Modules V) [((componentModule V n).obj G).IsQuasicoherent] :
    ((componentModule U n).obj ((modulePushforward f).obj G)).IsQuasicoherent

AlgebraicGeometry.SimplicialScheme.isQuasicoherentOnSite_modulePushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ZariskiPushforwardQuasicoherentTotal.lean, line 61.

Stacks 07TJ. Let f : V ⟶ U be a cartesian morphism of simplicial schemes, assume that the face maps d^n_j of U are flat and that the components f_n : V_n ⟶ U_n are quasi-compact and quasi-separated. Then for a quasi-coherent module G on the total Zariski site of V the direct image f_*G is a quasi-coherent module on the total Zariski site of U.

public theorem isQuasicoherentOnSite_modulePushforward (f : V ⟶ U)
    (hcart : NatTrans.Equifibered f)
    (hflat : ∀ (k : ℕ) (j : Fin (k + 2)), Flat (U.δ j))
    (hqc : ∀ k : SimplexCategoryᵒᵖ, QuasiCompact (f.app k))
    (hqs : ∀ k : SimplexCategoryᵒᵖ, QuasiSeparated (f.app k))
    (G : Modules V) (hG : G.IsQuasicoherentOnSite) :
    ((modulePushforward f).obj G).IsQuasicoherentOnSite

Tag 07TK, a lemma

Tag 07TK in the Stacks Project.

AlgebraicGeometry.SimplicialScheme.quasicoherentModulePullbackAdjPushforward', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ZariskiQuasicoherentAdjunctionUnconditional.lean, line 116.

Stacks 07TK. Let f : V ⟶ U be a cartesian morphism of simplicial schemes such that every face map of U is flat and every component f_n : V_n ⟶ U_n is quasi-compact and quasi-separated. Then the pullback f^* and the pushforward f_* are an adjoint pair between the category of quasi-coherent modules on U_Zar and the category of quasi-coherent modules on V_Zar.

Quasi-coherence of the pullback is Stacks 07TI and of the pushforward is Stacks 07TJ; adjointness itself is the adjunction of Stacks 03D7 on all sheaves of modules, restricted along the two full subcategory inclusions.

public noncomputable def quasicoherentModulePullbackAdjPushforward' (f : V ⟶ U)
    (hcart : NatTrans.Equifibered f)
    (hflat : ∀ (k : ℕ) (j : Fin (k + 2)), Flat (U.δ j))
    (hqc : ∀ k : SimplexCategoryᵒᵖ, QuasiCompact (f.app k))
    (hqs : ∀ k : SimplexCategoryᵒᵖ, QuasiSeparated (f.app k)) :
    quasicoherentModulePullback f ⊣ quasicoherentModulePushforward' f hcart hflat hqc hqs

Tag 07TL, a lemma

Tag 07TL in the Stacks Project.

AlgebraicGeometry.pullbackToSimplicialSchemeComponentIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/QuasiCoherentModulesSimplicialSection.lean, line 147. The attribute's comment: “the functor is pullback: its component in degree n is the pullback along the structure morphism (X/S)_n ⟶ S”.

The pullback is computed degreewise: the component in degree n of the pullback of a quasi-coherent O_S-module M to the total Zariski site of (X/S)_• is the pullback of M along the structure morphism (X/S)_n ⟶ S, naturally in M.

def pullbackToSimplicialSchemeComponentIso (n : ℕ) :
    pullbackToSimplicialScheme f ⋙ ObjectProperty.ι _ ⋙ componentModule _ (op ⦋n⦌) ≅
      ObjectProperty.ι _ ⋙ Scheme.Modules.pullback (baseMap f n)

AlgebraicGeometry.isEquivalence_pullbackToSimplicialScheme_of_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/QuasiCoherentModulesSimplicialSection.lean, line 166.

Let f : X ⟶ S be a morphism of schemes with a section σ, and let (X/S)_• be the simplicial scheme of Stacks 024A. Then pullback is an equivalence between the quasi-coherent O_S-modules and the quasi-coherent modules on the total Zariski site ((X/S)_•)_Zar. The pullback functor is AlgebraicGeometry.pullbackToSimplicialScheme; its component in degree n is the pullback along (X/S)_n ⟶ S (AlgebraicGeometry.pullbackToSimplicialSchemeComponentIso).

theorem isEquivalence_pullbackToSimplicialScheme_of_section (σ : S ⟶ X) (hσ : σ ≫ f = 𝟙 S) :
    (pullbackToSimplicialScheme f).IsEquivalence

AlgebraicGeometry.isEquivalence_pullbackToSimplicialScheme_of_fpqcLocalSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/QuasiCoherentModulesSimplicialSection.lean, line 176. The attribute's comment: “the footnote: it is enough that f have a section fpqc locally on S”.

Pullback is an equivalence between the quasi-coherent O_S-modules and the quasi-coherent modules on ((X/S)_•)_Zar already when f has a section only fpqc locally on S: there is an fpqc covering {p_i : T_i ⟶ S} and morphisms s_i : T_i ⟶ X with s_i ≫ f = p_i.

theorem isEquivalence_pullbackToSimplicialScheme_of_fpqcLocalSection {I : Type*}
    {T : I → Scheme.{u}} (p : ∀ i, T i ⟶ S)
    (hp : Presieve.ofArrows T p ∈ Scheme.fpqcPrecoverage.{u} S)
    (s : ∀ i, T i ⟶ X) (hs : ∀ i, s i ≫ f = p i) :
    (pullbackToSimplicialScheme f).IsEquivalence

AlgebraicGeometry.quasicoherentDescentEquivalenceOfSection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/QuasiCoherentModulesWithSection.lean, line 185. The attribute's comment: “the equivalence, with its target in descent-data form: the quasi-coherent descent data for {f}, not yet identified with QCoh(((X/S)_bullet)_Zar); that identification is the cited 07TJ together with 07TH, and 07TJ is absent here”.

Stacks 07TL, in its descent-data form. For a morphism of schemes f : X ⟶ S with a section, pullback is an equivalence between the category of quasi-coherent O_S-modules and the category of quasi-coherent descent data for {f}, i.e. the quasi-coherent modules on the simplicial scheme (X/S)_• of Stacks 024A.

def quasicoherentDescentEquivalenceOfSection
    (f : X ⟶ S) (σ : S ⟶ X) (hσ : σ ≫ f = 𝟙 S) :
    (SheafOfModules.isQuasicoherent S.ringCatSheaf).FullSubcategory ≌
      QuasicoherentDescentData (PreZeroHypercover.singleton.{0} f).f

AlgebraicGeometry.quasicoherentDescentEquivalenceOfFpqcLocalSection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/QuasiCoherentModulesWithSection.lean, line 222. The attribute's comment: “the footnote's stronger form, f having a section only fpqc locally on S; target in descent-data form as above, its identification with QCoh(((X/S)_bullet)_Zar) being the cited 07TJ together with 07TH, and 07TJ is absent here”.

Stacks 07TL in the stronger form of its footnote, in the descent-data form. If f admits a section after an fpqc covering of S, pullback is an equivalence between the quasi-coherent O_S-modules and the quasi-coherent descent data for {f}, i.e. the quasi-coherent modules on the simplicial scheme (X/S)_• of Stacks 024A.

def quasicoherentDescentEquivalenceOfFpqcLocalSection
    (f : X ⟶ S) {I : Type v} {T : I → Scheme.{u}} (p : ∀ i, T i ⟶ S)
    (hp : Presieve.ofArrows T p ∈ Scheme.fpqcPrecoverage.{u} S)
    (s : ∀ i, T i ⟶ X) (hs : ∀ i, s i ≫ f = p i) :
    (SheafOfModules.isQuasicoherent S.ringCatSheaf).FullSubcategory ≌
      QuasicoherentDescentData (PreZeroHypercover.singleton.{0} f).f

Sources

LeanAlgebraicGeometry.SimplicialScheme.isQuasicoherentOnSite_modulePullback · AlgebraicGeometry.SimplicialScheme.isQuasicoherentOnSite_modulePullback_of_presentation · AlgebraicGeometry.SimplicialScheme.isQuasicoherent_componentModule_modulePushforward · AlgebraicGeometry.SimplicialScheme.isQuasicoherentOnSite_modulePushforward · AlgebraicGeometry.SimplicialScheme.quasicoherentModulePullbackAdjPushforward' · AlgebraicGeometry.pullbackToSimplicialSchemeComponentIso · AlgebraicGeometry.isEquivalence_pullbackToSimplicialScheme_of_section · AlgebraicGeometry.isEquivalence_pullbackToSimplicialScheme_of_fpqcLocalSection

Section85.29 Groupoids and simplicial schemes #

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

Tag 07TN, a lemma

Tag 07TN in the Stacks Project.

Stacks.Groupoids.GroupoidScheme.groupoidSimplicialScheme, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/GroupoidNerve.lean, line 879.

Stacks 07TN. The simplicial scheme associated to a groupoid scheme.

noncomputable def groupoidSimplicialScheme {S : Scheme.{u}}
    (G : GroupoidScheme S) : GroupoidSimplicialScheme G

Tag 07TP, a lemma

Tag 07TP in the Stacks Project.

Stacks.Groupoids.GroupoidScheme.quasicoherentModuleEquivQuasicoherentOnTotalSite, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/GroupoidQuasiCoherentComparison.lean, line 666. The attribute's comment: “The normalization e^*α = id of Stacks 03LI, which the source's proof passes over, is proved here: it is automatic for an invertible descent morphism satisfying the cocycle condition.”.

Stacks 07TP. Let S be a scheme, (U,R,s,t,c) a groupoid scheme over S and X the simplicial scheme of Stacks 07TN. The category of quasi-coherent modules on (U,R,s,t,c) in the sense of Stacks 03LI is equivalent to the category of quasi-coherent modules on X_{Zar}.

The equivalence is the composite of three steps. Quasi-coherent modules on the total Zariski site are the pairs (ℱ, α) of Stacks 07TH with quasi-coherent degree-zero module, by Stacks 07TH and Stacks 0D7M; such pairs are the groupoid descent data of (U,R,s,t,c), because in degrees ≤ 2 the nerve is U, R and R ×_{s,U,t} R with faces the source, the target, the two projections and the composition law; and groupoid descent data are the quasi-coherent modules of Stacks 03LI, which is descentDataEquivQuasicoherentModule.

noncomputable def quasicoherentModuleEquivQuasicoherentOnTotalSite :
    QuasicoherentModule G ≌ QuasicoherentZariskiModule (groupoidSimplicialScheme G).toSchemes

Tag 07TQ, a lemma

Tag 07TQ in the Stacks Project.

Stacks.Groupoids.GroupoidScheme.groupoidCechNerveTarget, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/GroupoidCechNerve.lean, line 389.

The canonical cartesian map from the Čech nerve of the source of a groupoid scheme to its nerve.

noncomputable def groupoidCechNerveTarget {S : Scheme.{u}}
    (G : GroupoidScheme S) :
    CartesianTargetMap G (groupoidSimplicialScheme G)

Sources

LeanStacks.Groupoids.GroupoidScheme.groupoidSimplicialScheme · Stacks.Groupoids.GroupoidScheme.quasicoherentModuleEquivQuasicoherentOnTotalSite · Stacks.Groupoids.GroupoidScheme.groupoidCechNerveTarget

Section85.30 Descent data give equivalence relations #

Section 85.30 of the Stacks Project, Tag 024D. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 024E, a lemma

Tag 024E in the Stacks Project.

CategoryTheory.SimplicialObject.isEquivalenceRelation_faceMaps_of_equifibered, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/CechNerveEquivalenceRelation.lean, line 586. References: SGA 4 I (10.9), “special case”.

If a simplicial object maps cartesianly to the Čech nerve of f, its two face maps from degree one form an internal equivalence relation.

theorem isEquivalenceRelation_faceMaps_of_equifibered {X S : C} (f : X ⟶ S)
    {Y : SimplicialObject C} (π : Y ⟶ (Arrow.mk f).cechNerve)
    (hπ : NatTrans.Equifibered π) :
    IsEquivalenceRelation (Y.δ (1 : Fin 2)) (Y.δ (0 : Fin 2))

Sources

LeanCategoryTheory.SimplicialObject.isEquivalenceRelation_faceMaps_of_equifibered

Section85.31 An example case #

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

Tag 024G, a lemma

Tag 024G in the Stacks Project.

AlgebraicGeometry.Simplicial.pointClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/CechNervePointClass.lean, line 135. The attribute's comment: “the subset T_y”.

The points reached from y by a one-simplex whose first face is y.

def pointClass (Y : SimplicialObject Scheme.{u}) (y : Y _⦋0⦌) :
    Set (Y _⦋0⦌)

AlgebraicGeometry.Simplicial.mem_pointClass_self, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/CechNervePointClass.lean, line 142. The attribute's comment: “membership of y in T_y”.

A point belongs to the subset of points reachable from it.

theorem mem_pointClass_self {X S : Scheme.{u}} (f : X ⟶ S)
    {Y : SimplicialObject Scheme.{u}} (π : Y ⟶ (Arrow.mk f).cechNerve)
    (hπ : NatTrans.Equifibered π) (y : Y _⦋0⦌) :
    y ∈ pointClass Y y

AlgebraicGeometry.Simplicial.pointClass_eq_of_nonempty_inter, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/CechNervePointClass.lean, line 151. The attribute's comment: “intersecting classes are equal”.

If two subsets of reachable points meet, they are the same subset.

theorem pointClass_eq_of_nonempty_inter {X S : Scheme.{u}} (f : X ⟶ S)
    {Y : SimplicialObject Scheme.{u}} (π : Y ⟶ (Arrow.mk f).cechNerve)
    (hπ : NatTrans.Equifibered π) (y y' : Y _⦋0⦌)
    (h : (pointClass Y y ∩ pointClass Y y').Nonempty) :
    pointClass Y y = pointClass Y y'

Tag 024H, a lemma

Tag 024H in the Stacks Project.

AlgebraicGeometry.Simplicial.isCompact_relatedPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/CechNervePointClass.lean, line 220.

The vertices connected to a fixed vertex in a cartesian simplicial scheme over the Čech nerve of a quasi-compact morphism form a quasi-compact set.

theorem isCompact_relatedPoints {X S : Scheme.{u}} (f : X ⟶ S)
    [QuasiCompact f] {Y : SimplicialObject Scheme.{u}}
    (π : Y ⟶ (Arrow.mk f).cechNerve) (hπ : NatTrans.Equifibered π)
    (y : (Y _⦋0⦌)) :
    IsCompact {y' : (Y _⦋0⦌) | ∃ y₁ : (Y _⦋1⦌),
      (Y.δ (1 : Fin 2)).base y₁ = y ∧ (Y.δ (0 : Fin 2)).base y₁ = y'}

Tag 024I, a lemma

Tag 024I in the Stacks Project.

AlgebraicGeometry.DescentDatum.isEffective_of_iso_sigma_spec_isArtinianRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ArtinianDisjointUnionDescent.lean, line 199. The attribute's comment: “effectivity of a datum carried by a disjoint union of Artinian spectra”.

Let f : X ⟶ S be a quasi-compact, flat, surjective morphism of schemes and let (V, φ) be a descent datum relative to X/S. If V is a disjoint union of spectra of Artinian rings then (V, φ) is effective.

theorem isEffective_of_iso_sigma_spec_isArtinianRing [QuasiCompact f] [Flat f] [Surjective f]
    (D : DescentDatum f)
    (hV : ∃ (ι : Type u) (A : ι → CommRingCat.{u}), (∀ i, IsArtinianRing (A i)) ∧
      Nonempty (D.over.left ≅ ∐ fun i ↦ Spec (A i))) :
    DescentData.IsEffective D

Sources

LeanAlgebraicGeometry.Simplicial.pointClass · AlgebraicGeometry.Simplicial.mem_pointClass_self · AlgebraicGeometry.Simplicial.pointClass_eq_of_nonempty_inter · AlgebraicGeometry.Simplicial.isCompact_relatedPoints · AlgebraicGeometry.DescentDatum.isEffective_of_iso_sigma_spec_isArtinianRing

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

85.18 Cohomological descent for… to 85.31 An example case

Section85.18 Cohomological descent for hypercoverings: modules#

Tag 0D9Z, a lemma

Tag 0DA0, a lemma

Tag 0DA1, a lemma

Tag 0DA2, a lemma

Sources

Section85.19 Cohomological descent for hypercoverings of an object#

Tag 0D8K, a lemma

Tag 0D8L, a lemma

Tag 09X7, a lemma

Tag 0D8M, a lemma

Sources

Section85.20 Cohomological descent for hypercoverings of an object: modules#

Tag 0DA4, a lemma

Tag 0DA5, a lemma

Tag 0DA6, a lemma

Tag 0DA7, a lemma

Sources

Section85.21 Hypercovering by a simplicial object of the site#

Tag 09X8, the section

Tag 0DA8, a lemma

Tag 0D8N, a lemma

Tag 09X9, a lemma

Tag 0DA9, a lemma

Tag 09WL, a lemma

Sources

Section85.22 Hypercovering by a simplicial object of the site: modules#

Tag 0DAB, a lemma

Tag 0DAC, a lemma

Tag 0DAD, a lemma

Tag 0DAE, a lemma

Sources

Section85.23 Unbounded cohomological descent for hypercoverings#

Tag 0DC2, an item

Tag 0DC3, an item

Tag 0DC4, an item

Tag 0DC5, an example

Tag 0DC6, an example

Tag 0DC7, a lemma

Sources

Section85.24 Glueing complexes#

Tag 0DC9, a situation

Tag 0DCA, a lemma

Tag 0DCB, a lemma

Tag 0DCC, a lemma

Tag 0GMG, a lemma

Sources

Section85.25 Proper hypercoverings in topology#

Tag 0DAF, a lemma

Tag 0DAG, a lemma

Tag 09XS, a lemma

Tag 09XC, a lemma

Tag 0DAH, a lemma

Tag 09XB, a lemma

Sources

Section85.27 Descent in terms of simplicial schemes#

Tag 0249, a definition

Tag 07TC, a lemma

Tag 024A, a definition

Tag 024B, a lemma

Tag 024C, a lemma

Sources

Section85.28 Quasi-coherent modules on simplicial schemes#

Tag 07TI, a lemma

Tag 07TJ, a lemma

Tag 07TK, a lemma

Tag 07TL, a lemma

Sources

Section85.29 Groupoids and simplicial schemes#

Tag 07TN, a lemma

Tag 07TP, a lemma

Tag 07TQ, a lemma

Sources

Section85.30 Descent data give equivalence relations#

Tag 024E, a lemma

Sources

Section85.31 An example case#

Tag 024G, a lemma

Tag 024H, a lemma

Section85.18 Cohomological descent for hypercoverings: modules #

Section85.19 Cohomological descent for hypercoverings of an object #

Section85.20 Cohomological descent for hypercoverings of an object: modules #

Section85.21 Hypercovering by a simplicial object of the site #

Section85.22 Hypercovering by a simplicial object of the site: modules #

Section85.23 Unbounded cohomological descent for hypercoverings #

Section85.24 Glueing complexes #

Section85.25 Proper hypercoverings in topology #

Section85.27 Descent in terms of simplicial schemes #

Section85.28 Quasi-coherent modules on simplicial schemes #

Section85.29 Groupoids and simplicial schemes #

Section85.30 Descent data give equivalence relations #

Section85.31 An example case #