85.11 Cohomology and… to 85.17 Cohomological descent for…

Section85.11 Cohomology and augmentations of ringed simplicial sites #

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

Tag 0D9D, the section

Tag 0D9D in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.RingedAugmentation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/Augmentation.lean, line 103. The attribute's comment: “the data O, O_D and a^♯ of a ringed augmentation”.

Stacks 0D9D. The data of a ringed augmentation of a simplicial site: a sheaf of commutative rings O on the total site, a sheaf of commutative rings O_D on the augmentation site, and a map a^♯ : O_D ⟶ a_*O into the direct image of O along the total augmentation.

structure RingedAugmentation (S : SimplicialSiteSituation.{u}) (D : Cat.{u, u})
    (K : GrothendieckTopology D) (a : Augmentation S D K)

CategoryTheory.SimplicialSiteSituation.RingedAugmentation.totalRingedHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/Augmentation.lean, line 128. The attribute's comment: “the morphism of ringed topoi a : (Sh(C_total), O) ⟶ (Sh(D), O_D)”.

Stacks 0D9D. The morphism of ringed topoi a : (Sh(C_total), O) ⟶ (Sh(D), O_D) determined by the total augmentation of Stacks 0D70 and the structure map a^♯.

def totalRingedHom :
    RingedToposHom (S.totalRingedTopos A.O) A.augmentationRingedTopos

CategoryTheory.SimplicialSiteSituation.RingedAugmentation.componentRingedHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/Augmentation.lean, line 142. The attribute's comment: “the morphisms of ringed topoi a_n = a ∘ g_n”.

Stacks 0D9D. The morphism of ringed topoi a_n = a ∘ g_n : (Sh(C_n), O_n) ⟶ (Sh(D), O_D), the composite of the component inclusion of Stacks 0D72 with the ringed augmentation.

def componentRingedHom (n : SimplexCategory) :
    RingedToposHom (S.componentRingedTopos A.O n) A.augmentationRingedTopos

CategoryTheory.SimplicialSiteSituation.RingedAugmentation.transitionComponentPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/Augmentation.lean, line 166. The attribute's comment: “a_m ∘ f_φ = a_n, on direct images of sheaves of sets”.

Stacks 0D9D. The identification a_m ∘ f_φ = a_n on direct images of sheaves of sets: the direct image of the simplicial transition followed by that of a_m is the direct image of a_n, for every simplex map φ : m ⟶ n.

def transitionComponentPushforwardIso {m n : SimplexCategory} (φ : m ⟶ n) :
    ((A.componentRingedHom m).comp (S.transitionRingedToposHom A.O φ)).toToposHom.pushforward ≅
      (A.componentRingedHom n).toToposHom.pushforward

CategoryTheory.SimplicialSiteSituation.RingedAugmentation.componentRingedTwoIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/AugmentationRingedTwoIso.lean, line 90. The attribute's comment: “a_m ∘ f_φ = a_n, as a 2-isomorphism of the morphisms of ringed topoi”.

a_m ∘ f_φ = a_n, as a 2-isomorphism of morphisms of ringed topoi. For every simplex map φ : [m] ⟶ [n] the canonical 2-morphism a_n ⟶ a_m ∘ f_φ is invertible. This is the identity the source's proof of Stacks 0D7H appeals to, read for morphisms of ringed topoi.

It is componentRingedTwoIsoAux followed by the reassociation of a ∘ (g_m ∘ f_φ) into (a ∘ g_m) ∘ f_φ = a_m ∘ f_φ; the source a ∘ g_n is a_n on the nose.

def componentRingedTwoIso {m n : SimplexCategory} (φ : m ⟶ n) :
    AlgebraicGeometry.RingedToposHom.TwoIso.{u, u, u, u, u, u}
      (A.componentRingedHom n)
      (AlgebraicGeometry.RingedToposHom.comp (X := S.componentRingedTopos A.O n)
        (Y := S.componentRingedTopos A.O m) (Z := A.augmentationRingedTopos)
        (A.componentRingedHom m) (S.transitionRingedToposHom A.O φ))

Tag 0DH3, a lemma

Tag 0DH3 in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.componentRingedAugmentation_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/AugmentationFlat.lean, line 111. The attribute's comment: “the forward implication: flatness of a gives flatness of every a_n”.

If the augmentation a of the total ringed topos is flat, then so is the augmentation a_n of every simplicial component.

theorem componentRingedAugmentation_isFlat (ha : a.IsFlat) (n : SimplexCategory) :
    (componentRingedAugmentation S O a n).IsFlat

CategoryTheory.SimplicialSiteSituation.componentRingedAugmentation_isFlat_iff_forall, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/AugmentationFlatConverse.lean, line 116.

The augmentation a of the total ringed topos of a simplicial-site situation is flat if and only if the augmentation a_n of every simplicial component is flat.

theorem componentRingedAugmentation_isFlat_iff_forall :
    a.IsFlat ↔ ∀ n : SimplexCategory, (componentRingedAugmentation S O a n).IsFlat

Tag 0D7C, a lemma

Tag 0D7C in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.RingedAugmentation.nonempty_moduleResolution, an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/AugmentationModuleBarResolution.lean, line 105.

With the notation of Stacks 0D9D, for a sheaf of O_D-modules G there is an exact complex

… ⟶ g_{2!}(a_2^*G) ⟶ g_{1!}(a_1^*G) ⟶ g_{0!}(a_0^*G) ⟶ a^*G ⟶ 0

of sheaves of O-modules on the total site, with g_{n!} the lower shriek of Stacks 0D72: a chain complex whose degree-n term is g_{n!}(a_n^*G), whose differentials are the alternating sums of the face maps of a simplicial structure on its terms, augmented onto a^*G, exact in every positive degree and at the augmentation, the augmentation being an epimorphism.

alias nonempty_moduleResolution

CategoryTheory.SimplicialSiteSituation.RingedAugmentation.nonempty_moduleResolution_of_iso_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/AugmentationModuleResolution.lean, line 393. The attribute's comment: “for an arbitrary coefficient module, by the simplex-coefficient resolution”.

Stacks 0D7C. With the notation of Stacks 0D9D, for a sheaf of O_D-modules G the lower shriek images g_{n!}(a_n^*G) of Stacks 0D72 carry an exact complex

… ⟶ g_{2!}(a_2^*G) ⟶ g_{1!}(a_1^*G) ⟶ g_{0!}(a_0^*G) ⟶ a^*G ⟶ 0

of sheaves of O-modules on the total site, with differentials the alternating sums of the canonical face maps. The complex is simplexModuleResolution, the simplex-coefficient resolution of a^*G.

theorem nonempty_moduleResolution_of_iso_unit
    (G : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf A.OD)) :
    Nonempty (A.ModuleResolution G)

Tag 0D7D, a lemma

Tag 0D7D in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.RingedAugmentation.moduleCechComplex_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/AugmentationModuleCechComplex.lean, line 469.

With the notation of Stacks 0D9D, let F be a sheaf of O-modules on the total site. The canonical complex of O_D-modules

0 ⟶ a_*F ⟶ a_{0,*}F_0 ⟶ a_{1,*}F_1 ⟶ a_{2,*}F_2 ⟶ …

(moduleCechComplex, with a_*F in degree 0 and a_{n,*}F_n in degree n + 1) is exact in degrees -1 and 0 (the Lean degrees 0 and 1). If F is an injective O-module, the complex is exact in all degrees and remains exact on applying Hom_{O_D}(G, -) for any O_D-module G.

The complex is the source's: its differentials are the transposes, along the adjunctions a^* ⊣ a_* and g_{n!}a_n^* ⊣ a_{n,*}g_n^*, of the augmentation and of the differentials of the resolution … ⟶ g_{1!}(a_1^*G) ⟶ g_{0!}(a_0^*G) ⟶ a^*G ⟶ 0 of Stacks 0D7C (homEquiv_cechAug, homEquiv_cechD), so Hom(G, -) of it is Hom(-, F) of that resolution; Hom(-, F) is left exact, and exact when F is injective.

theorem moduleCechComplex_spec :
    (A.moduleCechComplex F).X 0 = A.totalRingedHom.pushforwardModules.obj F ∧
    (∀ n : ℕ, (A.moduleCechComplex F).X (n + 1) =
      (A.componentRingedHom ⦋n⦌).pushforwardModules.obj
        ((S.componentModulesRestriction A.O ⦋n⦌).obj F)) ∧
    (A.moduleCechComplex F).ExactAt 0 ∧ (A.moduleCechComplex F).ExactAt 1 ∧
    (Injective F →
      (∀ k : ℕ, (A.moduleCechComplex F).ExactAt k) ∧
      ∀ (G : A.augmentationRingedTopos.Modules) (k : ℕ),
        (((preadditiveCoyoneda.obj (op G)).mapHomologicalComplex _).obj
          (A.moduleCechComplex F)).ExactAt k)

Tag 0D7F, a lemma

Tag 0D7F in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.RingedAugmentation.higherDirectImageSpectralSequence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/AugmentationModuleSpectralSequence.lean, line 359.

Stacks 0D7F. With the notation of Stacks 0D9D (a ringed augmentation A of a simplicial-site situation towards a ringed site (D, K, O_D)), for M in D⁺(O) there is a spectral sequence (E_r, d_r) in Mod(O_D), presented from its first page and functorial in M, with

E_1^{p,q} = R^q a_{p,*} M_p ⇒ R^{p+q} a_* M.

Here M_p is the restriction of M to the component C_p (Stacks 0D72), R^q a_{p,*} the cohomology of the right derived direct image along a_p = a ∘ g_p and R^n a_* that of the right derived direct image along a. The identification of the first page is natural in M, and the first page vanishes in the negative columns.

It is the spectral sequence of the double complex A^{p,q} = a_{p,*} I^q_p of a bounded below complex of injectives I^• representing M, whose horizontal maps are those of the complex of Stacks 0D7D, filtered by p.

def higherDirectImageSpectralSequence : A.HigherDirectImageSpectralSequence

Sources

Section85.12 Cartesian sheaves and modules #

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

Tag 07TF, a definition

Tag 07TF in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.IsModuleFiberTransitionIso, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/CartesianModule.lean, line 278. The attribute's comment: “part (2), for the module fibre transition of the component 2-morphism”.

The cartesian condition of Stacks 07TF for sheaves of modules, expressed through the 2-morphism of this file: a sheaf of O-modules on the total site of a simplicial site is cartesian when every canonical transition f_φ^*F_m ⟶ F_n between its component restrictions, namely moduleFiberTransition, is an isomorphism.

This is part (2) of the source definition; parts (1), (3) and (4) are CategoryTheory.SimplicialSiteSituation.IsCartesianSheaf, .IsCartesianAbSheaf and the derived-category conditions. The same condition stated through the transition of StacksFrontier.AlgebraicGeometry.Simplicial.ComponentRingedTopos.ModuleTransition is CategoryTheory.SimplicialSiteSituation.IsCartesianModule.

abbrev IsModuleFiberTransitionIso
    (F : SheafOfModules.{u}
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := S.totalTopology)) O)) : Prop

CategoryTheory.SimplicialSiteSituation.IsCartesianDerivedModule, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/DerivedModuleSystemOfObject.lean, line 298. The attribute's comment: “part (4), cartesian objects of D(O): the derived transitions Lf_phi^* K_m -> K_n are isomorphisms”.

Stacks 07TF (4). An object K of the derived category of O-modules on the total site is cartesian when the derived transition Lf_φ^* K_m ⟶ K_n of its restrictions along every simplex map φ : [m] ⟶ [n] is an isomorphism.

Parts (1), (2) and (3) of the source definition are CategoryTheory.SimplicialSiteSituation.IsCartesianSheaf and .IsCartesianAbSheaf, .IsModuleFiberTransitionIso, and .IsCartesianDerived'.

abbrev IsCartesianDerivedModule (K : DerivedCategory (S.totalRingedTopos O).Modules) : Prop

CategoryTheory.SimplicialSiteSituation.IsCartesianModule, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/ModuleTransition.lean, line 300. The attribute's comment: “cartesian modules”.

Stacks 07TF (2). A sheaf of O-modules on the total site of a simplicial-site situation is cartesian if every canonical transition f_φ^*ℱₘ ⟶ ℱₙ between its restrictions to the components is an isomorphism.

abbrev IsCartesianModule (O : Sheaf S.totalTopology CommRingCat.{u})
    (M : SheafOfModules.{u} (S.totalRingSheaf O)) : Prop

AlgebraicGeometry.SimplicialScheme.IsCartesianModule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ZariskiCartesianModule.lean, line 256. The attribute's comment: “part (2), for the total Zariski site of a simplicial scheme (the site of 09VL, which this development does not carry as a term of Situation 09WE), with the component modules of ZariskiModulePushforward and the transition of 09WF constructed here”.

Stacks 07TF (2) for the total Zariski site of a simplicial scheme. A sheaf of 𝒪_X-modules on the total Zariski site of a simplicial scheme X is cartesian when every transition (X φ)^* F_m ⟶ F_n is an isomorphism.

public def IsCartesianModule (X : SimplicialObject Scheme.{u}) (F : Modules X) : Prop

CategoryTheory.SimplicialSiteSituation.IsCartesianSheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/Cartesian.lean, line 54. The attribute's comment: “cartesian sheaves of sets”.

Stacks 07TF. A sheaf of sets on the total site of a simplicial site is cartesian if every canonical transition f_φ⁻¹ Fₘ ⟶ Fₙ between its components is an isomorphism.

abbrev IsCartesianSheaf (S : SimplicialSiteSituation.{u})
    (F : Sheaf S.totalTopology (Type u)) : Prop

CategoryTheory.SimplicialSiteSituation.IsCartesianAbSheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/Cartesian.lean, line 61. The attribute's comment: “cartesian sheaves of abelian groups”.

Stacks 07TF. A sheaf of abelian groups on the total site of a simplicial site is cartesian if the canonical transitions of its underlying sheaf of sets are isomorphisms.

abbrev IsCartesianAbSheaf (S : SimplicialSiteSituation.{u})
    (F : Sheaf S.totalTopology Ab.{u}) : Prop

CategoryTheory.SimplicialSiteSituation.IsCartesianDerived', an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CartesianDerived.lean, line 184. The attribute's comment: “cartesian objects of the derived category”.

Stacks 07TF. An object of the derived category of abelian sheaves on the total site of a simplicial site is cartesian if the canonical transition along every simplex map is an isomorphism.

The derived categories are the standard ones and the transition is derivedComponentTransition; CategoryTheory.SimplicialSiteSituation.IsCartesianDerived states the condition for an arbitrary choice of derived categories.

abbrev IsCartesianDerived' (K : DerivedCategory (Sheaf S.totalTopology Ab.{u})) : Prop

CategoryTheory.SimplicialSiteSituation.IsCartesianDerived, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CartesianDerivedSheaves.lean, line 417. The attribute's comment: “cartesian_derived_sheaf”.

Stacks 07TF (3). An object of the derived category of abelian sheaves on the total site is cartesian when the canonical transition along every simplex map is an isomorphism.

abbrev IsCartesianDerived (K : DerivedCategory (Sheaf S.totalTopology Ab.{u})) : Prop

Tag 07TG, a lemma

Tag 07TG in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.isCartesianDerivedModule_iff_faces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/DerivedModuleFaceCriterion.lean, line 167. The attribute's comment: “face criterion for objects of D(O)”.

Stacks 07TG (4). An object of the derived category of O-modules on the total site of a simplicial site is cartesian if and only if the derived transition along every face map is an isomorphism.

The simplex maps whose derived transition is invertible form a multiplicative class: the identity law is isIso_derivedComponentModuleTransition_id and the composition law is the cocycle condition derivedComponentModuleTransition_comp of Stacks 0D9P together with Stacks 0D6D. Every arrow of the simplex category is a composite of faces and degeneracies, and SimplexCategory.δ_comp_σ_self exhibits each degeneracy as the second factor of a composite that is an identity, so no separate hypothesis on the degeneracies is needed.

theorem isCartesianDerivedModule_iff_faces
    (K : DerivedCategory (S.totalRingedTopos O).Modules) :
    S.IsCartesianDerivedModule O K ↔
      ∀ (k : ℕ) (i : Fin (k + 2)),
        IsIso ((S.derivedComponentModuleTransition O (SimplexCategory.δ i)).app K)

AlgebraicGeometry.SimplicialScheme.isCartesianModule_iff_faces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ZariskiCartesianModuleFaces.lean, line 285. The attribute's comment: “part (3), the criterion for sheaves of MODULES, for the total Zariski site of a simplicial scheme (the site of 09VL, which this development does not carry as a term of Situation 09WE) with the cartesian condition of ZariskiCartesianModule. Parts (1) and (2) of the source, for sheaves of sets and for objects of the derived category of the total site, and part (4), for the derived pullbacks, are not covered here; parts (1) and (2) for a simplicial-site situation are CategoryTheory.SimplicialSiteSituation.isCartesianSheaf_iff_faces and isCartesianAbSheaf_iff_faces”.

Stacks 07TG (3) for the total Zariski site of a simplicial scheme. A sheaf of 𝒪_X-modules on the total Zariski site of a simplicial scheme is cartesian if and only if the transition (d^{k+1}_i)^* F_k ⟶ F_{k+1} along every face map is an isomorphism.

public theorem isCartesianModule_iff_faces (X : SimplicialObject Scheme.{u}) (F : Modules X) :
    IsCartesianModule X F ↔
      ∀ (k : ℕ) (i : Fin (k + 2)),
        IsIso (componentModuleTransition X (SimplexCategory.δ i).op F)

CategoryTheory.SimplicialSiteSituation.isCartesianDerived_iff_faces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CartesianDerivedFaceCriterion.lean, line 56. The attribute's comment: “face criterion for objects of D(C_total)”.

Stacks 07TG (2). An object of the derived category of abelian sheaves on the total site of a simplicial site is cartesian if and only if the canonical derived transition along every face map is an isomorphism.

theorem isCartesianDerived_iff_faces (K : DerivedCategory (Sheaf S.totalTopology Ab.{u})) :
    S.IsCartesianDerived K ↔
      ∀ (k : ℕ) (i : Fin (k + 2)),
        IsIso ((derivedTransition S (SimplexCategory.δ i)).app K)

CategoryTheory.SimplicialSiteSituation.isCartesianSheaf_iff_faces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CartesianFaceCriterion.lean, line 44. The attribute's comment: “face criterion for sheaves of sets”.

Stacks 07TG. A sheaf of sets on the total site of a simplicial site is cartesian if and only if the canonical transition along every face map is an isomorphism.

theorem isCartesianSheaf_iff_faces (F : Sheaf S.totalTopology (Type u)) :
    IsCartesianSheaf S F ↔
      ∀ (n : ℕ) (i : Fin (n + 2)),
        IsIso ((fiberTransition S (SimplexCategory.δ i)).app F)

CategoryTheory.SimplicialSiteSituation.isCartesianAbSheaf_iff_faces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CartesianFaceCriterion.lean, line 74. The attribute's comment: “face criterion for sheaves of abelian groups”.

Stacks 07TG. A sheaf of abelian groups on the total site of a simplicial site is cartesian if and only if the canonical transition along every face map is an isomorphism.

theorem isCartesianAbSheaf_iff_faces (F : Sheaf S.totalTopology Ab.{u}) :
    IsCartesianAbSheaf S F ↔
      ∀ (n : ℕ) (i : Fin (n + 2)),
        IsIso ((abelianFiberTransition S (SimplexCategory.δ i)).app F)

CategoryTheory.SimplicialSiteSituation.isCartesianModule_iff_faces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CartesianWeakSerreModules.lean, line 286. The attribute's comment: “face criterion for sheaves of modules”.

Stacks 07TG (3). A sheaf of O-modules on the total site of a simplicial site is cartesian if and only if the canonical transition along every face map is an isomorphism.

The simplex maps whose transition is invertible form a multiplicative class, the identity and composition laws being the unit and cocycle laws fiberTransitionModules_id and fiberTransitionModules_comp of Stacks 09WF for modules. Every arrow of the simplex category is a composite of faces and degeneracies, and SimplexCategory.δ_comp_σ_self exhibits each degeneracy as the second factor of a composite that is an identity, so no separate hypothesis on the degeneracies is needed.

theorem isCartesianModule_iff_faces (M : SheafOfModules.{u} (S.totalRingSheaf O)) :
    IsCartesianModule S O M ↔
      ∀ (k : ℕ) (i : Fin (k + 2)),
        IsIso (S.fiberTransitionModules O (SimplexCategory.δ i) M)

Tag 0D7H, a lemma

Tag 0D7H in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.RingedAugmentation.isCartesianDerivedModule_derivedPullbackModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/AugmentationCartesianDerivedModule.lean, line 138. The attribute's comment: “part (4)”.

Let E be an object of D(O_D). Then the derived pullback La^*E along the ringed augmentation of Stacks 0D9D is a cartesian object of D(O): every derived transition Lf_φ^*(La^*E)_m ⟶ (La^*E)_n is an isomorphism.

theorem isCartesianDerivedModule_derivedPullbackModules
    (E : DerivedCategory A.augmentationRingedTopos.Modules) :
    S.IsCartesianDerivedModule A.O (A.derivedPullbackModules.obj E)

CategoryTheory.SimplicialSiteSituation.Augmentation.isCartesian_pullbacks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/AugmentationCartesianDerivedModule.lean, line 170.

Let a be an augmentation of a simplicial-site situation towards a site (D, K). Then every pullback along a is cartesian:

a⁻¹𝒢, for a sheaf of sets 𝒢 on (D, K) and for a sheaf of abelian groups 𝒢;

a⁻¹E, for an object E of D(D);

a^*F, for a ringed augmentation A of Stacks 0D9D and a sheaf of O_D-modules F;

La^*E, for a ringed augmentation A and an object E of D(O_D).

theorem isCartesian_pullbacks (S : SimplicialSiteSituation.{u}) (D : Cat.{u, u})
    (K : GrothendieckTopology D) (a : Augmentation S D K) :
    ((∀ G : Sheaf K (Type u),
        IsCartesianSheaf S ((totalMorphismOfTopoi S D K a).inverseImage.obj G)) ∧
      ∀ G : Sheaf K Ab.{u}, IsCartesianAbSheaf S ((totalInverseImageAb S D K a).obj G)) ∧
    (∀ E : DerivedCategory (Sheaf K AddCommGrpCat.{u}),
      S.IsCartesianDerived ((derivedTotalInverseImage S D K a).obj E)) ∧
    (∀ (A : RingedAugmentation S D K a)
      (F : SheafOfModules.{u}
        ((Stacks.SheafOfModules.Tensor.ringSheaf (J := A.augmentationRingedTopos.J)
          A.augmentationRingedTopos.O))),
      S.IsModuleFiberTransitionIso A.O (A.totalRingedHom.toModulesHom.pullbackModules.obj F)) ∧
    ∀ (A : RingedAugmentation S D K a) (E : DerivedCategory A.augmentationRingedTopos.Modules),
      S.IsCartesianDerivedModule A.O (A.derivedPullbackModules.obj E)

CategoryTheory.SimplicialSiteSituation.RingedAugmentation.isCartesianModule_pullbackModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/AugmentationCartesianModule.lean, line 192. The attribute's comment: “part (3)”.

Stacks 0D7H (3). The pullback a^*F of a sheaf of O_D-modules along the ringed augmentation of Stacks 0D9D is a cartesian sheaf of O-modules on the total site: every transition f_φ^*(a^*F)_m ⟶ (a^*F)_n of sheaves of modules is invertible.

The transition is the compositor of Stacks 03D8 followed by the transformation of pullbacks induced by the 2-morphism g_n ⟶ g_m ∘ f_φ, and that transformation is invertible after the pullback along the ringed augmentation by CategoryTheory.SimplicialSiteSituation.RingedAugmentation.isIso_whiskerLeft_pullbackModulesMap, which rests on Stacks 0D7H (1).

theorem isCartesianModule_pullbackModules
    (F : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf A.augmentationRingedTopos.O)) :
    S.IsModuleFiberTransitionIso A.O ((A.totalRingedHom.toModulesHom.pullbackModules).obj F)

CategoryTheory.SimplicialSiteSituation.Augmentation.isCartesianSheaf_inverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/AugmentationCartesian.lean, line 91. The attribute's comment: “part (1), sheaves of sets”.

The inverse image along the total augmentation of a sheaf of sets on the augmentation site is a cartesian sheaf on the total site.

theorem isCartesianSheaf_inverseImage (G : Sheaf K (Type u)) :
    IsCartesianSheaf S ((inverseImage S D K a).obj G)

CategoryTheory.SimplicialSiteSituation.Augmentation.isCartesianAbSheaf_totalInverseImageAb, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/AugmentationCartesian.lean, line 107. The attribute's comment: “part (1), sheaves of abelian groups”.

The inverse image along the total augmentation of an abelian sheaf on the augmentation site is a cartesian abelian sheaf on the total site.

theorem isCartesianAbSheaf_totalInverseImageAb (G : Sheaf K Ab.{u}) :
    IsCartesianAbSheaf S ((totalInverseImageAb S D K a).obj G)

CategoryTheory.SimplicialSiteSituation.Augmentation.isCartesianDerived_derivedTotalInverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/AugmentationCartesianDerived.lean, line 53. The attribute's comment: “part (2), the derived inverse image of an object of D(D) is cartesian”.

For an object E of the derived category of abelian sheaves on the augmentation site, the derived inverse image a⁻¹E is a cartesian object of the derived category of abelian sheaves on the total site.

It suffices that every cohomology sheaf of a⁻¹E be cartesian (isCartesianDerived_iff_forall_isCartesianAbSheaf_homology'); those cohomology sheaves are the inverse images of the cohomology sheaves of E, since a⁻¹ is exact, and the inverse image of an abelian sheaf along the augmentation is cartesian (isCartesianAbSheaf_totalInverseImageAb).

theorem isCartesianDerived_derivedTotalInverseImage
    (E : DerivedCategory (Sheaf K AddCommGrpCat.{u})) :
    S.IsCartesianDerived ((derivedTotalInverseImage S D K a).obj E)

Tag 0D7I, a lemma

Tag 0D7I in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.cartesianAbSheafEquivCartesianAbPair, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CartesianAbPairEquivalence.lean, line 1063. The attribute's comment: “sheaves of abelian groups”.

Stacks 0D7I. The category of cartesian sheaves of abelian groups on the total site of a simplicial-site situation is equivalent to the category of pairs (ℱ, α) consisting of a sheaf of abelian groups ℱ on the degree-zero component and an isomorphism α : (f_{δ¹₁})⁻¹ℱ ≅ (f_{δ¹₀})⁻¹ℱ of sheaves of abelian groups on the degree-one component satisfying the cocycle condition (f_{δ²₁})⁻¹α = (f_{δ²₀})⁻¹α ∘ (f_{δ²₂})⁻¹α on the degree-two component.

noncomputable def cartesianAbSheafEquivCartesianAbPair :
    CartesianAbSheaf S ≌ CartesianAbPair S

CategoryTheory.SimplicialSiteSituation.cartesianSheafEquivCartesianPair, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CartesianPairEquivalence.lean, line 551. The attribute's comment: “sheaves of sets”.

Stacks 0D7I. The category of cartesian sheaves of sets on the total site of a simplicial-site situation is equivalent to the category of pairs (ℱ, α) consisting of a sheaf of sets ℱ on the degree-zero component and an isomorphism α : (f_{δ¹₁})⁻¹ℱ ≅ (f_{δ¹₀})⁻¹ℱ of sheaves on the degree-one component satisfying the cocycle condition (f_{δ²₁})⁻¹α = (f_{δ²₀})⁻¹α ∘ (f_{δ²₂})⁻¹α on the degree-two component.

noncomputable def cartesianSheafEquivCartesianPair : CartesianSheaf S ≌ CartesianPair S

Tag 07TH, a lemma

Tag 07TH in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.cartesianModuleSheafEquivCartesianModulePair, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/CartesianModulePairEquivalence.lean, line 176.

Stacks 07TH. Let S be a simplicial-site situation and O a sheaf of commutative rings on its total site. The category of cartesian sheaves of O-modules is equivalent to the category of pairs (ℱ, α), where ℱ is an O₀-module and α : f_{δ¹₁}^*ℱ ≅ f_{δ¹₀}^*ℱ is an isomorphism of O₁-modules such that f_{δ²₁}^*α = f_{δ²₀}^*α ∘ f_{δ²₂}^*α as O₂-module maps. The functor of the equivalence takes a cartesian module to its degree-zero restriction and the comparison of its two transitions to degree one.

def cartesianModuleSheafEquivCartesianModulePair :
    S.CartesianModuleSheaf O ≌ CartesianModulePair S O

Tag 0D7J, a lemma

Tag 0D7J in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.isCartesianAbSheaf_weakSerre_colimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CartesianWeakSerre.lean, line 354. The attribute's comment: “part (1)”.

Stacks 0D7J (1). The cartesian abelian sheaves on the total site of a simplicial site form a weak Serre subcategory of all abelian sheaves there, and colimits of systems of cartesian abelian sheaves are cartesian.

theorem isCartesianAbSheaf_weakSerre_colimits (S : SimplicialSiteSituation.{u}) :
    ObjectProperty.IsWeakSerreClass (IsCartesianAbSheaf S) ∧
      ∀ (J : Type*) [Category* J],
        ObjectProperty.IsClosedUnderColimitsOfShape (IsCartesianAbSheaf S) J

CategoryTheory.SimplicialSiteSituation.isCartesianModule_isWeakSerreClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CartesianWeakSerreModules.lean, line 337. The attribute's comment: “part (2), cartesian modules are a weak Serre subcategory of Mod(O). The hypothesis is left exactness of the pullback of sheaves of modules along the transition morphism of each face map, which for a flat face transition is Stacks 04JC and is weaker than flatness of the face transitions, so the statement is more general than the source's; the implementation notes record why flatness itself cannot be fed in at this pullback. NOT covered here: the second sentence of part (2), that colimits of systems of cartesian O-modules are cartesian, for which the argument needs restriction of modules to a component to preserve colimits of arbitrary shape and this development has only the finite case”.

Let O be a sheaf of rings on the total site of a simplicial site such that the pullback of sheaves of modules along the transition morphism of every face map is left exact. Then the cartesian O-modules form a weak Serre subcategory of Mod(O).

By Stacks 07TG (3) it is enough to test the face maps, which is why only the face transitions occur in the hypothesis; at a face the conditions are the zero module, which is cartesian with no hypothesis, and the four lemma applied to the transition read as a natural transformation of the two restriction functors.

theorem isCartesianModule_isWeakSerreClass
    (hflat : ∀ (k : ℕ) (i : Fin (k + 2)),
      PreservesFiniteLimits
        ((S.transitionRingedToposHom O (SimplexCategory.δ i)).toModulesHom.pullbackModules)) :
    ObjectProperty.IsWeakSerreClass (IsCartesianModule S O)

CategoryTheory.SimplicialSiteSituation.isCartesianModule_weakSerre_colimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CartesianWeakSerreModules.lean, line 428. The attribute's comment: “part (2)”.

Stacks 0D7J (2). Let O be a sheaf of rings on the total site of a simplicial site such that the morphisms of ringed topoi f_{δ^n_j} : (Sh(C_n), O_n) ⟶ (Sh(C_{n-1}), O_{n-1}) are flat. Then the cartesian O-modules form a weak Serre subcategory of Mod(O), and colimits of systems of cartesian O-modules are cartesian.

Flatness of a face transition makes its pullback of modules exact (Stacks 04JC), which is what the four lemma consumes; the colimit statement holds with no hypothesis.

theorem isCartesianModule_weakSerre_colimits
    (flat : ∀ (k : ℕ) (i : Fin (k + 2)),
      (S.transitionRingedToposHom O (SimplexCategory.δ i)).IsFlat) :
    ObjectProperty.IsWeakSerreClass (IsCartesianModule S O) ∧
      ∀ (J : Type*) [Category* J] [Small.{u} J],
        ObjectProperty.IsClosedUnderColimitsOfShape (IsCartesianModule S O) J

Tag 0D7K, a remark

Tag 0D7K in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.cartesianModuleSheafAbelian, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CartesianModuleAbelian.lean, line 556. The attribute's comment: “corrected form of the positive assertion, which is false as written (the source's hypothesis, flatness of f_{δ¹₁} and f_{δ¹₀} alone, does not suffice: see CategoryTheory.PointSimplicialSite.RatioCounterexample.exists_not_abelian_cartesianModuleSheaf); with one of f_{δ²₀}, f_{δ²₁}, f_{δ²₂} flat as well the cartesian O-modules form an abelian category, with the additive structure of Mod(O)”.

Stacks 0D7K, corrected form. If the morphisms of ringed topoi f_{δ¹₁} and f_{δ¹₀} are flat, and so is one of the three degree-two faces f_{δ²₀}, f_{δ²₁}, f_{δ²₂}, then the cartesian O-modules form an abelian category, with the additive structure of Mod(O); its cokernels are those of Mod(O), and its kernels are those of the pairs of Stacks 07TH, computed in degree zero.

The source asserts this under flatness of f_{δ¹₁} and f_{δ¹₀} alone, which is false: see CategoryTheory.PointSimplicialSite.RatioCounterexample.exists_not_abelian_cartesianModuleSheaf. The kernel of a morphism of pairs carries the restricted comparison isomorphism, but its cocycle condition lives on the degree-two component; it can be cancelled against the pullback of the kernel inclusion to the vertex 2 (through δ²₁ or δ²₀) or to the vertex 0 (through δ²₁ or δ²₂), which is a monomorphism as soon as one degree-two face is flat.

abbrev cartesianModuleSheafAbelian
    (h₁ : (S.transitionRingedToposHom O (SimplexCategory.δ (1 : Fin 2))).IsFlat)
    (h₀ : (S.transitionRingedToposHom O (SimplexCategory.δ (0 : Fin 2))).IsFlat)
    (h₂ : ∃ i : Fin 3, (S.transitionRingedToposHom O (SimplexCategory.δ i)).IsFlat) :
    Abelian (S.CartesianModuleSheaf O)

CategoryTheory.PointSimplicialSite.RatioCounterexample.exists_not_abelian_cartesianModuleSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CartesianModuleCounterexample.lean, line 483. The attribute's comment: “the positive assertion is false as written: counterexample with f_{δ¹₁} and f_{δ¹₀} flat but the cartesian O-modules not an abelian category (constant simplicial site on the point, O the cosimplicial ring of unit ratios); the corrected form is CategoryTheory.SimplicialSiteSituation.cartesianModuleSheafAbelian”.

Stacks 0D7K: the positive assertion is false as written. There is a simplicial site (the constant simplicial site on the point, in case (A) of Stacks 09WE) and a sheaf of rings O on its total site (the cosimplicial ring of unit ratios Rₙ = ℤ[xᵢ, wᵢⱼ^{±1} (i ≤ j)]/(xᵢ = wᵢⱼxⱼ, wᵢᵢ = 1)) such that the morphisms of ringed topoi f_{δ¹₁} and f_{δ¹₀} are flat, but the category of cartesian O-modules is not abelian, for any choice of abelian structure: the quotient map 𝒪 ⟶ 𝒪/(x₀) is a monomorphism and an epimorphism of cartesian modules, but not an isomorphism.

theorem exists_not_abelian_cartesianModuleSheaf :
    ∃ (S : SimplicialSiteSituation.{u}) (O : Sheaf S.totalTopology CommRingCat.{u}),
      (S.transitionRingedToposHom O (SimplexCategory.δ (1 : Fin 2))).IsFlat ∧
      (S.transitionRingedToposHom O (SimplexCategory.δ (0 : Fin 2))).IsFlat ∧
      IsEmpty (Abelian (S.CartesianModuleSheaf O))

CategoryTheory.PointSimplicialSite.SphereExample.exists_abelian_not_isSerreClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CartesianModuleNotWeakSerre.lean, line 113. The attribute's comment: “the assertion that the category of cartesian O-modules can be abelian without being a Serre subcategory of Mod(O): an example with f_{δ¹₁}, f_{δ¹₀} flat where the cartesian O-modules form an abelian category but are neither a Serre nor a weak Serre subcategory of Mod(O). The source's remark that, when f_{δ²₀} is not flat, there is no reason for the inclusion into Mod(O) to be exact is a heuristic, not an assertion; in this example the non-flat transitions are those into degree three”.

Stacks 0D7K: cartesian modules can be abelian without being a Serre subcategory. There is a simplicial site (the constant simplicial site on the point, in case (A) of Stacks 09WE) and a sheaf of rings O on its total site with f_{δ¹₁} and f_{δ¹₀} flat, such that the cartesian O-modules form an abelian category but are neither a Serre subcategory nor a weak Serre subcategory of Mod(O): they are not closed under kernels in Mod(O). Here O is the cosimplicial ring of functions on Spec ℤ ⊔ (Δ[3] / ∂Δ[3]); the non-flat transitions are those into degree three.

theorem exists_abelian_not_isSerreClass :
    ∃ (S : SimplicialSiteSituation.{u}) (O : Sheaf S.totalTopology CommRingCat.{u}),
      (S.transitionRingedToposHom O (SimplexCategory.δ (1 : Fin 2))).IsFlat ∧
      (S.transitionRingedToposHom O (SimplexCategory.δ (0 : Fin 2))).IsFlat ∧
      Nonempty (Abelian (S.CartesianModuleSheaf O)) ∧
      ¬ ObjectProperty.IsSerreClass (S.IsCartesianModule O) ∧
      ¬ ObjectProperty.IsWeakSerreClass (S.IsCartesianModule O)

CategoryTheory.SimplicialSiteSituation.CartesianModulePair.kernelIso_hom_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CartesianModulePairExactness.lean, line 334. The attribute's comment: “the kernel half of the positive assertion, in degree one: under left exactness of f_{δ¹₁}^ and f_{δ¹₀}^ (which flatness of f_{δ¹₁} and f_{δ¹₀} gives by Stacks 04JC), the kernel of a morphism of the pairs of Stacks 07TH carries a comparison isomorphism restricting that of the source pair, and it is the only morphism that does. NOT covered here: the degree-two cocycle condition for that isomorphism, hence not the kernel object in the category of pairs and not the abelian structure; and not the assertion that the inclusion of cartesian O-modules into all O-modules fails to be exact, which the source states as the absence of a reason for exactness and not as a counterexample”.

Stacks 0D7K, the kernel half of the positive assertion, in degree one. If the two degree-one pullbacks are left exact — which, for flat f_{δ¹₁} and f_{δ¹₀}, is Stacks 04JC — then the kernel of the degree-zero morphism of a morphism of pairs carries a comparison isomorphism restricting the comparison isomorphism of the source pair along the kernel inclusion.

theorem kernelIso_hom_comp :
    (kernelIso S O f).hom ≫
        (S.componentModulePullback O (SimplexCategory.δ (0 : Fin 2))).map (kernel.ι f.map) =
      (S.componentModulePullback O (SimplexCategory.δ (1 : Fin 2))).map (kernel.ι f.map) ≫
        A.iso.hom

CategoryTheory.SimplicialSiteSituation.CartesianModulePair.map_comp_cokernelIso_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CartesianModulePairExactness.lean, line 378. The attribute's comment: “the cokernel half of the positive assertion, in degree one, and with no flatness hypothesis at all, the pullback of modules being right exact unconditionally: the cokernel of a morphism of the pairs of Stacks 07TH carries a comparison isomorphism corestricting that of the target pair, and it is the only morphism that does. NOT covered here: the degree-two cocycle condition for that isomorphism, hence not the cokernel object in the category of pairs and not the abelian structure; and not the assertion that the inclusion of cartesian O-modules into all O-modules fails to be exact, which the source states as the absence of a reason for exactness and not as a counterexample”.

Stacks 0D7K, the cokernel half of the positive assertion, in degree one. The pullback of sheaves of modules is right exact unconditionally, so with no flatness hypothesis at all the cokernel of the degree-zero morphism of a morphism of pairs carries a comparison isomorphism corestricting the comparison isomorphism of the target pair along the cokernel projection.

theorem map_comp_cokernelIso_hom :
    (S.componentModulePullback O (SimplexCategory.δ (1 : Fin 2))).map (cokernel.π f.map) ≫
        (cokernelIso S O f).hom =
      B.iso.hom ≫
        (S.componentModulePullback O (SimplexCategory.δ (0 : Fin 2))).map (cokernel.π f.map)

Tag 0D7L, a lemma

Tag 0D7L in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.isCartesianDerivedModule_iff_forall_isCartesianModule_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/CartesianDerivedModuleCohomology.lean, line 151. The attribute's comment: “part (2), cartesian objects of D(O) for flat face transitions”.

Let O be a sheaf of rings on the total site of a simplicial site such that the morphisms of ringed topoi f_{δ^n_j} : (Sh(C_n), O_n) ⟶ (Sh(C_{n-1}), O_{n-1}) of the face maps are flat. Then an object K of D(O) is cartesian if and only if H^q(K) is a cartesian O-module for all q.

theorem isCartesianDerivedModule_iff_forall_isCartesianModule_homology
    (flat : ∀ (k : ℕ) (i : Fin (k + 2)),
      (S.transitionRingedToposHom O (SimplexCategory.δ i)).IsFlat)
    (K : DerivedCategory (S.totalRingedTopos O).Modules) :
    S.IsCartesianDerivedModule O K ↔
      ∀ q : ℤ, IsCartesianModule S O
        ((DerivedCategory.homologyFunctor (S.totalRingedTopos O).Modules q).obj K)

CategoryTheory.SimplicialSiteSituation.isCartesianDerived_iff_forall_isCartesianAbSheaf_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CartesianDerivedCohomology.lean, line 92. The attribute's comment: “cartesian derived sheaves are those with cartesian cohomology”.

Stacks 0D7L (1). An object of the derived category of abelian sheaves on the total site of a simplicial site is cartesian if and only if all of its cohomology sheaves are cartesian abelian sheaves.

theorem isCartesianDerived_iff_forall_isCartesianAbSheaf_homology
    (K : DerivedCategory (Sheaf S.totalTopology Ab.{u})) :
    IsCartesianDerived' S K ↔
      ∀ q : ℤ, IsCartesianAbSheaf S
        ((DerivedCategory.homologyFunctor (Sheaf S.totalTopology Ab.{u}) q).obj K)

CategoryTheory.SimplicialSiteSituation.isCartesianDerived_iff_forall_isCartesianAbSheaf_homology', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CartesianDerivedSheaves.lean, line 454. The attribute's comment: “cartesian derived sheaves are those with cartesian cohomology”.

Stacks 0D7L (1). An object of the derived category of abelian sheaves on the total site of a simplicial site is cartesian if and only if all of its cohomology sheaves are cartesian abelian sheaves.

theorem isCartesianDerived_iff_forall_isCartesianAbSheaf_homology'
    (K : DerivedCategory (Sheaf S.totalTopology Ab.{u})) :
    IsCartesianDerived S K ↔
      ∀ q : ℤ, IsCartesianAbSheaf S
        ((DerivedCategory.homologyFunctor (Sheaf S.totalTopology Ab.{u}) q).obj K)

Tag 0D9E, a lemma

Tag 0D9E in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.isCartesianDerivedModule_iff_forall_isIso_moduleProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/CartesianDerivedModuleProjectionSituation.lean, line 82. The attribute's comment: “part (2)”.

Stacks 0D9E (2). In a simplicial-site situation (Stacks 09WE, either case) let O be a sheaf of rings on the total site such that the structure-sheaf transitions f_φ^{-1}O_n ⟶ O_m are flat for every simplex map φ : [n] ⟶ [m]. Then an object K of D(O) is cartesian if and only if the canonical map g_{n!}K_n ⟶ g_{n!}O_n ⊗^L_O K is an isomorphism for every n.

theorem isCartesianDerivedModule_iff_forall_isIso_moduleProjection
    (hflat : ∀ (n m : SimplexCategory) (φ : n ⟶ m), (S.transitionRingedToposHom O φ).IsFlat)
    (K : DerivedCategory (S.totalRingedTopos O).Modules) :
    S.IsCartesianDerivedModule O K ↔
      ∀ n : SimplexCategory, IsIso (S.moduleProjection O n (hflat n) K)

CategoryTheory.SimplicialSiteSituation.isCartesianDerived_iff_isIso_integerProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CartesianDerivedLowerShriek.lean, line 246. The attribute's comment: “part (1)”.

Stacks 0D9E (1). An object K of D(𝒞_total) is cartesian if and only if the canonical map g_{n!}K_n ⟶ g_{n!}ℤ ⊗^L_ℤ K is an isomorphism for every simplicial degree n.

Since K is cartesian exactly when all of its cohomology sheaves are (Stacks 0D7L), this is the sheaf-level statement isCartesianAbSheaf_iff_isIso_componentLowerShriekMap read through isIso_integerProjection_iff.

theorem isCartesianDerived_iff_isIso_integerProjection
    (K : DerivedCategory (Sheaf S.totalTopology Ab.{u})) :
    S.IsCartesianDerived K ↔ ∀ n : SimplexCategory, IsIso (S.integerProjection K n)

Tag 0D7M, a lemma

Tag 0D7M in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.IsCartesianWithQuasicoherentComponents, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/QuasicoherentCartesian.lean, line 208. The attribute's comment: “the right-hand side of the equivalence only: F is cartesian in the sense of 07TF (2) and every component module F_n is a quasi-coherent O_n-module in the sense of 03DL (6). Neither direction of the equivalence with quasi-coherence of F on the total site is proved: both need a localization of the total site at an object, which the development does not have”.

The right-hand side of Stacks 0D7M. A sheaf of O-modules on the total site of a simplicial-site situation is cartesian in the sense of Stacks 07TF (2) and each of its component modules F_n is a quasi-coherent O_n-module in the sense of Stacks 03DL (6).

The source asserts that this condition is equivalent to quasi-coherence of F itself on the total site; that equivalence is not proved in this development.

noncomputable abbrev IsCartesianWithQuasicoherentComponents
    (F : SheafOfModules.{u} (S.totalRingSheaf O)) : Prop

CategoryTheory.SimplicialSiteSituation.isQuasicoherentOnSite_iff_isCartesianModule_and_isQuasicoherentOnSite_componentModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/QuasicoherentCartesian/Equivalence.lean, line 59.

Stacks 0D7M. In Situation 09WE, let O be a sheaf of rings on the total site and F a sheaf of O-modules. Then F is quasi-coherent in the sense of Stacks 03DL if and only if F is cartesian in the sense of Stacks 07TF (2) and every component Fₙ is a quasi-coherent Oₙ-module.

The right-hand side is CategoryTheory.SimplicialSiteSituation.IsCartesianWithQuasicoherentComponents, spelled out.

theorem isQuasicoherentOnSite_iff_isCartesianModule_and_isQuasicoherentOnSite_componentModule
    (S : SimplicialSiteSituation.{u}) (O : Sheaf S.totalTopology CommRingCat.{u})
    (F : SheafOfModules.{u} (S.totalRingSheaf O)) :
    F.IsQuasicoherentOnSite ↔
      S.IsCartesianModule O F ∧
        ∀ n : SimplexCategory, (S.componentModule O F n).IsQuasicoherentOnSite

AlgebraicGeometry.SimplicialScheme.isQuasicoherentOnSite_iff_isCartesianModule_and_components, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ZariskiQuasicoherentCartesian.lean, line 198. The attribute's comment: “for the total Zariski site of a simplicial scheme, which is the site of 09VL; the cartesian condition is AlgebraicGeometry.SimplicialScheme.IsCartesianModule, 07TF (2) at the transition of 09WF, and quasi-coherence of the components is 03DL (6) over the structure sheaf of the degree, with the component functors of ZariskiModulePushforward”.

Stacks 0D7M for the total Zariski site of a simplicial scheme. A sheaf of 𝒪_X-modules on the total Zariski site is quasi-coherent in the sense of Stacks 03DL (6) if and only if it is cartesian in the sense of Stacks 07TF (2) and every one of its component modules F_n is a quasi-coherent 𝒪_{X_n}-module.

public theorem isQuasicoherentOnSite_iff_isCartesianModule_and_components (F : Modules X) :
    F.IsQuasicoherentOnSite ↔
      IsCartesianModule X F ∧
        ∀ k : SimplexCategoryᵒᵖ,
          ((componentModule X k).obj F).IsQuasicoherentOnSite

Sources

LeanCategoryTheory.SimplicialSiteSituation.IsModuleFiberTransitionIso · CategoryTheory.SimplicialSiteSituation.IsCartesianDerivedModule · CategoryTheory.SimplicialSiteSituation.IsCartesianModule · AlgebraicGeometry.SimplicialScheme.IsCartesianModule · CategoryTheory.SimplicialSiteSituation.IsCartesianSheaf · CategoryTheory.SimplicialSiteSituation.IsCartesianAbSheaf · CategoryTheory.SimplicialSiteSituation.IsCartesianDerived' · CategoryTheory.SimplicialSiteSituation.IsCartesianDerived

Section85.13 Simplicial systems of the derived category #

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

Tag 0D9G, a definition

Tag 0D9G in the Stacks Project.

CategoryTheory.SimplicialDerivedSystem, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/DerivedSystem.lean, line 478. The attribute's comment: “the simplicial system”.

A simplicial system of the derived category for S: an object K_n of the derived category of abelian sheaves on each component site, and for every simplex map φ : [m] ⟶ [n] a map K_φ : f_φ⁻¹K_m ⟶ K_n from the derived inverse image, such that K_{φ ∘ ψ} is K_φ ∘ f_φ⁻¹K_ψ under the canonical identification f_{φ ∘ ψ}⁻¹ ≅ f_φ⁻¹ ∘ f_ψ⁻¹. As in the source, no condition is imposed at identities.

structure SimplicialDerivedSystem

CategoryTheory.SimplicialDerivedSystem.Cartesian, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/DerivedSystem.lean, line 494. The attribute's comment: “cartesian systems”.

A system is cartesian if all its transition maps are isomorphisms.

abbrev Cartesian (K : SimplicialDerivedSystem S) : Prop

CategoryTheory.SimplicialDerivedSystem.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/DerivedSystem.lean, line 499. The attribute's comment: “morphisms of simplicial systems”.

A morphism is a degreewise morphism commuting with every transition map.

structure Hom (K L : SimplicialDerivedSystem S)

CategoryTheory.SimplicialDerivedSystem.cartesianInclusion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/DerivedSystem.lean, line 550.

Simplicial systems of the derived category: the category whose objects are the systems (K_n, K_φ) of SimplicialDerivedSystem S and whose morphisms are the degreewise maps commuting with the transitions (SimplicialDerivedSystem.Hom), together with its full subcategory of cartesian systems, those whose transitions K_φ are all isomorphisms.

def cartesianInclusion : (cartesian S).FullSubcategory ⥤ SimplicialDerivedSystem S

Tag 0D9H, a lemma

Tag 0D9H in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.associatedDerivedSystemData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/AssociatedDerivedSystem.lean, line 461. The attribute's comment: “associated simplicial system”.

The canonical simplicial system of the derived category attached to an object K of the derived category of abelian sheaves on the total site, together with the equations stating that its object in degree n is the derived restriction of K and its transition along a simplex map is the canonical derived transition at K.

def associatedDerivedSystemData (K : DerivedCategory (Sheaf S.totalTopology Ab.{u})) :
    { T : SimplicialDerivedSystem S //
      (∀ n, T.obj n = (derivedComponent S n).obj K) ∧
      (∀ ⦃m n : SimplexCategory⦄ (φ : m ⟶ n),
        HEq (T.map φ) ((derivedTransition S φ).app K)) }

CategoryTheory.SimplicialSiteSituation.associatedDerivedSystem_cartesian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/AssociatedDerivedSystem.lean, line 479. The attribute's comment: “cartesian objects give cartesian systems”.

The simplicial system of derived restrictions of a cartesian object is cartesian.

theorem associatedDerivedSystem_cartesian
    (K : DerivedCategory (Sheaf S.totalTopology Ab.{u})) (hK : S.IsCartesianDerived K) :
    (associatedDerivedSystem S K).Cartesian

Tag 0GME, a lemma

Tag 0GME in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.pairDerivedSystem, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/DerivedCocycleSystem.lean, line 979. The attribute's comment: “the simplicial system”.

Stacks 0GME. The cartesian simplicial system of the derived category attached to a pair (K₀, α): in degree n the derived inverse image of K₀ along the last vertex of ⦋n⦌.

def pairDerivedSystem (P : DerivedCocyclePair S) : SimplicialDerivedSystem S

CategoryTheory.SimplicialSiteSituation.pairDerivedSystem_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/DerivedCocycleSystem.lean, line 989. The attribute's comment: “the objects of the system”.

Stacks 0GME. The object of the system in degree n is f_{τⁿₙ}⁻¹K₀, the derived inverse image of K₀ along the last vertex of ⦋n⦌.

theorem pairDerivedSystem_obj (P : DerivedCocyclePair S) (n : SimplexCategory) :
    (S.pairDerivedSystem P).obj n =
      (derivedInverseImage S
        (SimplexCategory.const (SimplexCategory.mk 0) n (Fin.last n.len))).obj P.obj

CategoryTheory.SimplicialSiteSituation.pairDerivedSystem_cartesian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/DerivedCocycleSystem.lean, line 996. The attribute's comment: “the system is cartesian”.

Stacks 0GME. The system attached to a pair is cartesian.

theorem pairDerivedSystem_cartesian (P : DerivedCocyclePair S) :
    (S.pairDerivedSystem P).Cartesian

Tag 0D9I, a lemma

Tag 0D9I in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.derivedTensorIntegerResolutionPostnikovSystem, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/IntegerResolutionDerivedTensor.lean, line 142.

Stacks 0D9I(1) for - ⊗^L_ℤ K. For each length N, the images under - ⊗^L_ℤ K of the brutal-truncation triangles Yₙ₊₁ ⟶ Xₙ₊₁ ⟶ Yₙ ⟶ Yₙ₊₁[1] of the integral resolution are a Postnikov system (Derived Categories, Definition 0D7Z) for X_N ⟶ ⋯ ⟶ X₁ ⟶ X₀, where Xₙ = g_{n!}ℤ ⊗^L_ℤ K by derivedTensorIntegerResolutionTermIso.

def derivedTensorIntegerResolutionPostnikovSystem (N : ℕ) :
    Triangulated.PostnikovSystem
      (fun i : Fin (N + 1) =>
        (integerDerivedTensorRight S K).obj (integerResolutionTerm S (i : ℕ)))
      (fun i : Fin N =>
        (integerDerivedTensorRight S K).map
          (termDiff (integerResolutionComplex S) (i : ℕ)))

CategoryTheory.SimplicialSiteSituation.isHomotopyColimit_derivedTensorIntegerResolutionSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/IntegerResolutionDerivedTensor.lean, line 186.

Stacks 0D9I(2) for - ⊗^L_ℤ K. The object K is the derived colimit of the system Yₙ[n] = (g_{n!}ℤ → … → g_{0!}ℤ) ⊗^L_ℤ K.

theorem isHomotopyColimit_derivedTensorIntegerResolutionSystem :
    IsHomotopyColimit (integerResolutionSystem S ⋙ integerDerivedTensorRight S K) K

CategoryTheory.SimplicialSiteSituation.map_integerResolutionPostnikovSystem, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/IntegerResolutionPostnikov.lean, line 942.

Stacks 0D9I(1). For an exact functor T of D(𝒞_total) — such as - ⊗^L_ℤ K for an object K of D(𝒞_total) — the images under T of the brutal-truncation triangles of the integral resolution are a Postnikov system for T(X_N) ⟶ ⋯ ⟶ T(X₁) ⟶ T(X₀).

def map_integerResolutionPostnikovSystem
    (T : DerivedCategory (Sheaf S.totalTopology Ab.{u}) ⥤
      DerivedCategory (Sheaf S.totalTopology Ab.{u})) [T.CommShift ℤ] [T.IsTriangulated]
    (N : ℕ) :
    Triangulated.PostnikovSystem
      (fun i : Fin (N + 1) => T.obj (integerResolutionTerm S (i : ℕ)))
      (fun i : Fin N => T.map (termDiff (integerResolutionComplex S) (i : ℕ)))

CategoryTheory.SimplicialSiteSituation.isHomotopyColimit_map_integerResolutionSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/IntegerResolutionPostnikov.lean, line 969.

Stacks 0D9I(2). For an exact functor T of D(𝒞_total) commuting with countable direct sums — such as - ⊗^L_ℤ K for an object K of D(𝒞_total) — the object T(ℤ) is the derived colimit of the system T(Yₙ[n]).

theorem isHomotopyColimit_map_integerResolutionSystem
    (T : DerivedCategory (Sheaf S.totalTopology Ab.{u}) ⥤
      DerivedCategory (Sheaf S.totalTopology Ab.{u})) [T.CommShift ℤ] [T.IsTriangulated]
    [PreservesColimit (Discrete.functor (integerResolutionSystem S).obj) T] :
    IsHomotopyColimit (integerResolutionSystem S ⋙ T)
      (T.obj (DerivedCategory.Q.obj (integerResolutionComplex S)))

Tag 0D9J, a lemma

Tag 0D9J in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.eq_zero_of_derivedComponent_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CartesianDerivedMapVanishing.lean, line 537.

Stacks 0D9J. In the simplicial-site situation of Stacks 09WE, let K and K' be objects of D(𝒞_total) with K cartesian, and suppose that every morphism Kᵢ[i] ⟶ K'ᵢ vanishes for i > 0 and that every morphism Kᵢ[i + 1] ⟶ K'ᵢ vanishes for i ≥ 0. Then a map K ⟶ K' inducing the zero map K₀ ⟶ K'₀ is zero.

The proof is the source's. Stacks 0D9I presents K as the derived colimit of the system Yₙ[n], whose successive quotients are the shifted terms Xₙ[n]; Stacks 0D9E identifies Xₙ with g_{n!}Kₙ, which turns the two vanishing hypotheses into the vanishing of the groups Hom(Xᵢ[t], K') the induction consumes.

theorem eq_zero_of_derivedComponent_zero
    (hK : IsCartesianDerived S K)
    (hHom : ∀ i : ℕ, 0 < i →
      ∀ g : ((derivedComponent S ⦋i⦌).obj K)⟦(i : ℤ)⟧ ⟶ (derivedComponent S ⦋i⦌).obj K', g = 0)
    (hHomSucc : ∀ i : ℕ, ∀ g : ((derivedComponent S ⦋i⦌).obj K)⟦((i + 1 : ℕ) : ℤ)⟧ ⟶
      (derivedComponent S ⦋i⦌).obj K', g = 0)
    (f : K ⟶ K') (hf : (derivedComponent S ⦋0⦌).map f = 0) :
    f = 0

Tag 0D9K, a lemma

Tag 0D9K in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.exists_hom_of_isCartesianDerived, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CartesianDerivedLiftMorphism.lean, line 150. The attribute's comment: “a morphism of simplicial systems comes from the total site, at the source's hypotheses (1) and (2): the degree-zero lift is CategoryTheory.SimplicialSiteSituation.exists_hom_derivedComponent_zero_eq, which makes the source's two omitted computations -- the vanishing of X_1 ⟶ X_0 ⟶ K' against the transition of the realization, and the reading of the structural map X_0 ⟶ K as the counit -- and the passage from degree zero to all degrees is CategoryTheory.SimplicialSiteSituation.exists_hom_iff_exists_hom_zero”.

Stacks 0D9K. In the simplicial-site situation of Stacks 09WE, let K and K' be objects of the derived category of abelian sheaves on the total site. If K is cartesian in the sense of Stacks 07TF (3) and Hom(K_i[i - 1], K'_i) = 0 for i > 1, then every morphism of the associated simplicial systems of Stacks 0D9H is induced by a morphism K ⟶ K': there is a γ : K ⟶ K' whose derived restriction to every simplicial degree is the given component.

theorem exists_hom_of_isCartesianDerived
    (K K' : DerivedCategory (Sheaf S.totalTopology Ab.{u}))
    (hK : S.IsCartesianDerived K)
    (hHom : S.ShiftedComponentHomVanishing K K')
    (f : SimplicialDerivedSystem.Hom (S.associatedDerivedSystem K)
      (S.associatedDerivedSystem K')) :
    ∃ γ : K ⟶ K', ∀ n : SimplexCategory, (derivedComponent S n).map γ = f.app n

Tag 0D9L, a lemma

Tag 0D9L in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.exists_isCartesianDerived_of_simplicialDerivedSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CartesianDerivedOfSystem.lean, line 344.

A cartesian simplicial system of the derived categories of the components, whose objects have no positively shifted self-maps, is the system associated with a cartesian object of the derived category of the total site.

theorem exists_isCartesianDerived_of_simplicialDerivedSystem (T : SimplicialDerivedSystem S)
    (hT : SimplicialDerivedSystem.Cartesian T)
    (hHom : ∀ (k : SimplexCategory) (t : ℕ), 0 < t →
      ∀ f : (shiftFunctor (DerivedCategory (Sheaf (S.componentTopology k) Ab.{u}))
        (t : ℤ)).obj (T.obj k) ⟶ T.obj k, f = 0) :
    ∃ K : DerivedCategory (Sheaf S.totalTopology Ab.{u}),
      S.IsCartesianDerived K ∧
        ∃ γ : ∀ n, T.obj n ≅ (S.associatedDerivedSystem K).obj n,
          ∀ ⦃m n : SimplexCategory⦄ (φ : m ⟶ n),
            T.map φ ≫ (γ n).hom =
              (derivedInverseImage S φ).map ((γ m).hom) ≫
                (S.associatedDerivedSystem K).map φ

CategoryTheory.SimplicialSiteSituation.nonempty_sequentialPostnikovSystem_realizationComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CartesianDerivedPostnikov.lean, line 341. The attribute's comment: “the Postnikov system of the realization complex”.

Stacks 0D9L, the Postnikov system of the realization. The complex whose term in degree n is the extension by lower shriek of the object of the system in degree n, and whose differential is the alternating sum of the transitions along the face maps, carries a sequential Postnikov system: its differentials compose to zero, and all positively shifted morphisms between its terms vanish.

This is the construction step of Stacks 0D9L. The totalization of this Postnikov system, the identification of its restriction to each simplicial degree with the object of the system in that degree, and the cartesianness of the result are in StacksFrontier.CategoryTheory.Sites.Simplicial.CartesianDerivedOfSystem.

theorem nonempty_sequentialPostnikovSystem_realizationComplex (T : SimplicialDerivedSystem S)
    (hT : SimplicialDerivedSystem.Cartesian T)
    (hHom : ∀ (k : SimplexCategory) (t : ℕ), 0 < t →
      ∀ f : (shiftFunctor (DerivedCategory (Sheaf (S.componentTopology k) Ab.{u}))
        (t : ℤ)).obj (T.obj k) ⟶ T.obj k, f = 0) :
    Nonempty (Triangulated.SequentialPostnikovSystem
      (fun n : ℕ => realizationTerm S T ⦋n⦌)
      (fun n : ℕ => (realizationComplex T hT).d (n + 1) n))

Sources

LeanCategoryTheory.SimplicialDerivedSystem · CategoryTheory.SimplicialDerivedSystem.Cartesian · CategoryTheory.SimplicialDerivedSystem.Hom · CategoryTheory.SimplicialDerivedSystem.cartesianInclusion · CategoryTheory.SimplicialSiteSituation.associatedDerivedSystemData · CategoryTheory.SimplicialSiteSituation.associatedDerivedSystem_cartesian · CategoryTheory.SimplicialSiteSituation.pairDerivedSystem · CategoryTheory.SimplicialSiteSituation.pairDerivedSystem_obj

Section85.14 Simplicial systems of the derived category: modules #

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

Tag 0D9N, a definition

Tag 0D9N in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.SimplicialDerivedModuleSystem, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/DerivedModuleSystem.lean, line 87. The attribute's comment: “the data of a simplicial system and its cocycle condition”.

Stacks 0D9N. A simplicial system of the derived category of modules for a sheaf of commutative rings O on the total site of a simplicial-site situation: an object K_n of the derived category of O_n-modules in every simplicial degree n, a map K_φ : Lf_φ^* K_m ⟶ K_n for every simplex map φ : m ⟶ n, and the cocycle condition K_{ψ ≫ φ} = K_φ ∘ Lf_φ^* K_ψ under the canonical identification of Lf_{ψ ≫ φ}^* with Lf_ψ^* ⋙ Lf_φ^*.

structure SimplicialDerivedModuleSystem

CategoryTheory.SimplicialSiteSituation.SimplicialDerivedModuleSystem.Cartesian, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/DerivedModuleSystem.lean, line 106. The attribute's comment: “cartesian systems”.

Stacks 0D9N. A simplicial system of the derived category of modules is cartesian if all of its transition maps K_φ are isomorphisms.

abbrev Cartesian (K : SimplicialDerivedModuleSystem S O) : Prop

CategoryTheory.SimplicialSiteSituation.SimplicialDerivedModuleSystem.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/DerivedModuleSystem.lean, line 112. The attribute's comment: “morphisms of simplicial systems”.

Stacks 0D9N. A morphism of simplicial systems of the derived category of modules: a morphism in every simplicial degree commuting with all of the transition maps.

structure Hom (K L : SimplicialDerivedModuleSystem S O)

Tag 0D9P, a lemma

Tag 0D9P in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.derivedModuleSystemData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/DerivedModuleSystemOfObject.lean, line 308. The attribute's comment: “the system (K_n, K(φ)) is a simplicial system of the derived category of modules”.

Stacks 0D9P. The restrictions K_n of an object K of the derived category of O-modules on the total site, together with the derived transitions K(φ), form a simplicial system of the derived category of modules in the sense of Stacks 0D9N. The two equations are part of the datum, so no unrelated family of transitions can satisfy the cocycle condition in its place.

noncomputable def derivedModuleSystemData
    (K : DerivedCategory (S.totalRingedTopos O).Modules) :
    { T : SimplicialDerivedModuleSystem S O //
      (∀ n, T.obj n = (S.derivedComponentModuleRestriction O n).obj K) ∧
      (∀ ⦃m n : SimplexCategory⦄ (φ : m ⟶ n),
        HEq (T.map φ) ((S.derivedComponentModuleTransition O φ).app K)) }

CategoryTheory.SimplicialSiteSituation.derivedModuleSystem_cartesian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/DerivedModuleSystemOfObject.lean, line 329. The attribute's comment: “if K is cartesian then so is the system”.

Stacks 0D9P. The simplicial system of a cartesian object of the derived category of O-modules is cartesian: its transitions are the derived transitions, which are isomorphisms by hypothesis.

theorem derivedModuleSystem_cartesian (K : DerivedCategory (S.totalRingedTopos O).Modules)
    (hK : S.IsCartesianDerivedModule O K) : (S.derivedModuleSystem O K).Cartesian

Tag 0GMF, a lemma

Tag 0GMF in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.pairDerivedModuleSystem, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/DerivedCocycleSystem/CocyclePairSystem.lean, line 698. The attribute's comment: “the simplicial system”.

Stacks 0GMF. The simplicial system of the derived category of modules attached to a pair (K₀, α): in degree n the derived pullback of K₀ along the last vertex of ⦋n⦌, with the transition at φ given by pulling back to the image of the last vertex and transporting along the edge to the last vertex. The cocycle condition of Stacks 0D9N is pairDerivedModuleTransition_comp.

def pairDerivedModuleSystem (Pr : S.DerivedModuleCocyclePair O) :
    SimplicialDerivedModuleSystem S O

CategoryTheory.SimplicialSiteSituation.pairDerivedModuleSystem_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/DerivedCocycleSystem/CocyclePairSystem.lean, line 707. The attribute's comment: “the objects of the system”.

Stacks 0GMF. The object of the system in degree n is Lf_{τⁿₙ}^* K₀, the derived pullback of K₀ along the last vertex of ⦋n⦌.

theorem pairDerivedModuleSystem_obj (Pr : S.DerivedModuleCocyclePair O) (n : SimplexCategory) :
    (S.pairDerivedModuleSystem O Pr).obj n =
      (S.derivedTransitionPullback O
        (SimplexCategory.const (SimplexCategory.mk 0) n (Fin.last n.len))).obj Pr.obj

CategoryTheory.SimplicialSiteSituation.pairDerivedModuleSystem_cartesian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/DerivedCocycleSystem/CocyclePairSystem.lean, line 716. The attribute's comment: “the system is cartesian”.

Stacks 0GMF. The system attached to a pair is cartesian: every transition map is an isomorphism, for every simplex map and not only for the faces.

theorem pairDerivedModuleSystem_cartesian (Pr : S.DerivedModuleCocyclePair O) :
    (S.pairDerivedModuleSystem O Pr).Cartesian

Tag 0D9Q, a lemma

Tag 0D9Q in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.moduleResolutionTensorPostnikovSystem, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/ModuleResolutionDerivedTensor.lean, line 344. The attribute's comment: “part (1), the Postnikov system of - ⊗^L_O K”.

Stacks 0D9Q(1). For each length N, the triangles Yₙ₊₁ ⟶ Xₙ₊₁ ⟶ Yₙ ⟶ Yₙ₊₁[1] with Xₙ = (g_{n!}Oₙ) ⊗^L_O K and Yₙ = (g_{n!}Oₙ → … → g_{0!}O₀)[-n] ⊗^L_O K form a Postnikov system (Derived Categories, Definition 0D7Z) for X_N ⟶ ⋯ ⟶ X₁ ⟶ X₀.

The triangles are the images under - ⊗^L_O K of the brutal-truncation triangles of the resolution of Stacks 0D9B, and - ⊗^L_O K is exact by isTriangulated_derivedTensorRight; the terms are the source's Xₙ by moduleResolutionTensorTermIso.

def moduleResolutionTensorPostnikovSystem (N : ℕ) :
    Triangulated.PostnikovSystem
      (fun i : Fin (N + 1) => (derivedTensorRight R T K).obj (moduleResolutionTerm D (i : ℕ)))
      (fun i : Fin N => (derivedTensorRight R T K).map (moduleResolutionTermDiff D (i : ℕ)))

CategoryTheory.SimplicialSiteSituation.isHomotopyColimit_moduleResolutionTensorSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/ModuleResolutionDerivedTensor.lean, line 360. The attribute's comment: “part (2), the homotopy colimit, K = hocolim Yₙ[n] for Yₙ = (…)[-n] ⊗^L_O K”.

Stacks 0D9Q(2). K = hocolim Yₙ[n] in D(O), where Yₙ = (g_{n!}Oₙ → … → g_{0!}O₀)[-n] ⊗^L_O K.

The system Yₙ[n] is the image under - ⊗^L_O K of the tower of brutal truncations of the resolution of Stacks 0D9B, whose derived colimit is the structure sheaf (isHomotopyColimit_moduleResolutionSystem, Stacks 0D9Q(2) for O); the functor - ⊗^L_O K is exact and commutes with countable direct sums, so it carries that derived colimit to the derived colimit of the images, and it sends O to K by derivedTensorRightUnitIso.

theorem isHomotopyColimit_moduleResolutionTensorSystem :
    IsHomotopyColimit (moduleResolutionSystem D ⋙ derivedTensorRight R T K) K

CategoryTheory.SimplicialSiteSituation.map_moduleResolutionPostnikovSystem, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/ModuleResolutionPostnikov.lean, line 293. The attribute's comment: “part (1), the Postnikov system, for an exact functor in place of - ⊗^L_O K”.

Stacks 0D9Q(1). For an exact functor T of D(O) — such as - ⊗^L_O K for an object K of D(O) — the images under T of the brutal-truncation triangles of the module resolution are a Postnikov system for T(X_N) ⟶ ⋯ ⟶ T(X₁) ⟶ T(X₀), where Xₙ = g_{n!}Oₙ.

def map_moduleResolutionPostnikovSystem
    (T : DerivedCategory (SheafOfModules.{u} O) ⥤ DerivedCategory (SheafOfModules.{u} O))
    [T.CommShift ℤ] [T.IsTriangulated] (N : ℕ) :
    Triangulated.PostnikovSystem
      (fun i : Fin (N + 1) => T.obj (moduleResolutionTerm D (i : ℕ)))
      (fun i : Fin N => T.map (moduleResolutionTermDiff D (i : ℕ)))

CategoryTheory.SimplicialSiteSituation.isHomotopyColimit_map_moduleResolutionSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/ModuleResolutionPostnikov.lean, line 305. The attribute's comment: “part (2), the homotopy colimit, for an exact functor in place of - ⊗^L_O K”.

Stacks 0D9Q(2). For an exact functor T of D(O) commuting with countable direct sums — such as - ⊗^L_O K for an object K of D(O), for which T(O) = K — the object T(O) is the derived colimit of the system T(Yₙ[n]).

theorem isHomotopyColimit_map_moduleResolutionSystem
    (T : DerivedCategory (SheafOfModules.{u} O) ⥤ DerivedCategory (SheafOfModules.{u} O))
    [T.CommShift ℤ] [T.IsTriangulated]
    [PreservesColimit (Discrete.functor (moduleResolutionSystem D).obj) T] :
    IsHomotopyColimit (moduleResolutionSystem D ⋙ T)
      (T.obj ((DerivedCategory.singleFunctor (SheafOfModules.{u} O) 0).obj
        (SheafOfModules.unit O)))

Tag 0D9R, a lemma

Tag 0D9R in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.eq_zero_of_derivedComponentModuleRestriction_map_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/CartesianDerivedModuleProjectionSituation.lean, line 101.

Stacks 0D9R. In a simplicial-site situation (Stacks 09WE, either case) let O be a sheaf of rings on the total site and K, K' objects of D(O). Assume

f_φ^{-1}O_n ⟶ O_m is flat for every simplex map φ,

K is cartesian,

Hom(K_i[i], K'_i) = 0 for i > 0, and

Hom(K_i[i + 1], K'_i) = 0 for i ≥ 0.

Then a map K ⟶ K' inducing the zero map K_0 ⟶ K'_0 is zero.

theorem eq_zero_of_derivedComponentModuleRestriction_map_eq_zero
    (K K' : DerivedCategory (S.totalRingedTopos O).Modules)
    (hflat : ∀ ⦃m n : SimplexCategory⦄ (φ : m ⟶ n), (S.transitionRingedToposHom O φ).IsFlat)
    (hK : S.IsCartesianDerivedModule O K)
    (hHom : ∀ i : ℕ, 0 < i →
      ∀ g : (shiftFunctor (DerivedCategory ((S.componentRingedTopos O ⦋i⦌).Modules)) (i : ℤ)).obj
          ((S.derivedComponentModuleRestriction O ⦋i⦌).obj K) ⟶
        (S.derivedComponentModuleRestriction O ⦋i⦌).obj K', g = 0)
    (hHomSucc : ∀ i : ℕ,
      ∀ g : (shiftFunctor (DerivedCategory ((S.componentRingedTopos O ⦋i⦌).Modules))
            ((i : ℤ) + 1)).obj ((S.derivedComponentModuleRestriction O ⦋i⦌).obj K) ⟶
        (S.derivedComponentModuleRestriction O ⦋i⦌).obj K', g = 0)
    (f : K ⟶ K')
    (hf : (S.derivedComponentModuleRestriction O ⦋0⦌).map f = 0) :
    f = 0

Tag 0D9S, a lemma

Tag 0D9S in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.exists_hom_of_cartesian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CartesianDerivedModuleMorphism.lean, line 269.

Stacks 0D9S. In Situation 09WE, let O be a sheaf of rings on the total site and let K, K' be objects of D(O). Assume

the structure-sheaf transitions f_φ^{-1}O_n ⟶ O_m are flat,

K is cartesian, and

Hom(K_i[i - 1], K'_i) = 0 for i > 1.

Then any morphism {K_n ⟶ K'_n} between the associated simplicial systems of the derived category of modules comes from a morphism K ⟶ K' in D(O).

The situation S is an arbitrary term of CategoryTheory.SimplicialSiteSituation, so both cases of Situation 09WE are covered. The proof is the source's: the Postnikov system of Stacks 0D9Q produces a morphism agreeing with the given one in degree zero (exists_hom_derivedComponentModuleRestriction_zero_eq), and cartesianness of K makes it agree in every degree (SimplicialDerivedModuleSystem.Hom.app_eq_of_cartesian).

theorem exists_hom_of_cartesian
    (K K' : DerivedCategory (S.totalRingedTopos O).Modules)
    (hflat : ∀ (m n : SimplexCategory) (φ : m ⟶ n), (S.transitionRingedToposHom O φ).IsFlat)
    (hK : S.IsCartesianDerivedModule O K)
    (hHom : ∀ i : ℕ, 1 < i →
      ∀ g : (shiftFunctor (DerivedCategory ((S.componentRingedTopos O ⦋i⦌).Modules))
          ((i : ℤ) - 1)).obj ((S.derivedComponentModuleRestriction O ⦋i⦌).obj K) ⟶
          (S.derivedComponentModuleRestriction O ⦋i⦌).obj K', g = 0)
    (f : SimplicialDerivedModuleSystem.Hom (S.derivedModuleSystem O K)
      (S.derivedModuleSystem O K')) :
    ∃ γ : K ⟶ K', ∀ i : SimplexCategory,
      (S.derivedComponentModuleRestriction O i).map γ = f.app i

Tag 0D9T, a lemma

Tag 0D9T in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.exists_isCartesianDerivedModule_of_moduleSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/CartesianDerivedModuleOfModuleSystem.lean, line 97.

Stacks 0D9T. In a simplicial-site situation (Stacks 09WE, either case) let O be a sheaf of rings on the total site and let (K_n, K_φ) be a simplicial system of the derived category of modules. Assume

f_φ^{-1}O_n ⟶ O_m is flat for every simplex map φ,

(K_n, K_φ) is cartesian, and

Hom(K_i[t], K_i) = 0 for all i and all t > 0.

Then there exists a cartesian object K of D(O) whose associated simplicial system is isomorphic to (K_n, K_φ).

theorem exists_isCartesianDerivedModule_of_moduleSystem
    (hflat : ∀ (n m : SimplexCategory) (φ : n ⟶ m), (S.transitionRingedToposHom O φ).IsFlat)
    (T : SimplicialDerivedModuleSystem S O) (hT : T.Cartesian)
    (hHom : ∀ (k : SimplexCategory) (t : ℕ), 0 < t →
      ∀ f : (shiftFunctor (DerivedCategory (S.componentRingedTopos O k).Modules)
        (t : ℤ)).obj (T.obj k) ⟶ T.obj k, f = 0) :
    ∃ K : DerivedCategory (S.totalRingedTopos O).Modules,
      S.IsCartesianDerivedModule O K ∧ Nonempty (T ≅ S.derivedModuleSystem O K)

Sources

Section85.15 The site associated to a semi-representable object #

Section 85.15 of the Stacks Project, Tag 09WK. 7 tags here are carried by 54 declarations of the repository (all in StacksFrontier) and 8 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0D85, a lemma

Tag 0D85 in the Stacks Project.

CategoryTheory.SemiRepresentable.LocalizationSites.localizationFunctor_isContinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Continuity.lean, line 258. The attribute's comment: “semi_representable_localization_has_p”.

Stacks 0D85. The componentwise localization functor C / K ⥤ C is continuous.

instance localizationFunctor_isContinuous (S : LocalizationSites.{w} C J) :
    S.localizationFunctor.IsContinuous S.sourceTopology J

CategoryTheory.SemiRepresentable.LocalizationSites.localizationFunctor_isCocontinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Continuity.lean, line 301. The attribute's comment: “semi_representable_localization_has_p”.

Stacks 0D85. The componentwise localization functor C / K ⥤ C is cocontinuous.

instance localizationFunctor_isCocontinuous (S : LocalizationSites.{w} C J) :
    S.localizationFunctor.IsCocontinuous S.sourceTopology J

CategoryTheory.SemiRepresentable.LocalizationSites.localizationFunctor_hasCoverPullbacks, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Continuity.lean, line 318. The attribute's comment: “semi_representable_localization_has_p”.

Stacks 0D85. The componentwise localization functor has property P under the site's covering-pullback axiom: relative pullbacks of covering families exist and their projections cover.

lemma localizationFunctor_hasCoverPullbacks (S : LocalizationSites.{w} C J)
    [J.toCoverage.HasPullbacks] :
    ∀ (𝒱 : Covering.{u, v, w'} C), 𝒱.2.presieve₀ ∈ J.toCoverage 𝒱.1 →
      ∀ (U : S.source) (g : S.localizationFunctor.obj U ⟶ 𝒱.1),
        ∃ (P : 𝒱.2.I₀ → S.source) (p₁ : ∀ i, P i ⟶ U)
          (p₂ : ∀ i, S.localizationFunctor.obj (P i) ⟶ 𝒱.2.X i),
          (∀ i,
            S.localizationFunctor.map (p₁ i) ≫ g = p₂ i ≫ 𝒱.2.f i ∧
              ∀ (T : S.source) (a : T ⟶ U)
                (b : S.localizationFunctor.obj T ⟶ 𝒱.2.X i),
                S.localizationFunctor.map a ≫ g = b ≫ 𝒱.2.f i →
                  ∃! l : T ⟶ P i,
                    (l ≫ p₁ i = a ∧ S.localizationFunctor.map l ≫ p₂ i = b)) ∧
            (PreZeroHypercover.mk 𝒱.2.I₀ P p₁).presieve₀ ∈
              S.sourceTopology.toCoverage U

CategoryTheory.SemiRepresentable.LocalizationSites.relocalizationFunctor_isContinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Continuity.lean, line 430. The attribute's comment: “semi_representable_relocalization_has_p”.

Stacks 0D85. The componentwise relocalization functor C / K ⥤ C / L is continuous.

instance relocalizationFunctor_isContinuous (S : LocalizationSites.{w} C J) :
    S.relocalizationFunctor.IsContinuous S.sourceTopology S.targetTopology

CategoryTheory.SemiRepresentable.LocalizationSites.relocalizationFunctor_isCocontinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Continuity.lean, line 454. The attribute's comment: “semi_representable_relocalization_has_p”.

Stacks 0D85. The componentwise relocalization functor C / K ⥤ C / L is cocontinuous.

instance relocalizationFunctor_isCocontinuous (S : LocalizationSites.{w} C J) :
    S.relocalizationFunctor.IsCocontinuous S.sourceTopology S.targetTopology

CategoryTheory.SemiRepresentable.LocalizationSites.relocalizationFunctor_hasCoverPullbacks, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Continuity.lean, line 469. The attribute's comment: “semi_representable_relocalization_has_p”.

Stacks 0D85. The componentwise relocalization functor has property P: covering families admit representable pullbacks, and those pullbacks cover.

lemma relocalizationFunctor_hasCoverPullbacks (S : LocalizationSites.{w} C J)
    [J.toCoverage.HasPullbacks] :
    S.relocalizationFunctor.HasCoverPullbacks
      (fun 𝒰 ↦ 𝒰.2.presieve₀ ∈ S.sourceTopology.toCoverage 𝒰.1)
      (fun 𝒱 ↦ 𝒱.2.presieve₀ ∈ S.targetTopology.toCoverage 𝒱.1)

Tag 0D86, a lemma

Tag 0D86 in the Stacks Project.

CategoryTheory.SemiRepresentable.abelianLocalizationPushforwardPullbackNatIsoSheafHomPrime, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/AbelianPushPull.lean, line 273. The attribute's comment: “the abelian form: abelian-sheaf coefficients, primed internal hom”.

Stacks 0D86 for abelian coefficients. For a semi-representable object K = {U i} of a small site (C, J), the product of the localization push-pull functors j_{i,*} j_i^{-1} on abelian sheaves is naturally isomorphic to ℋom'(F(K)^#, -).

This is the source's j_* j^{-1} F = ℋom'(F(K)^#, F) under the product description of sheaves on C / K, for F an abelian sheaf and naturally in F, which is the form in which Stacks 0D8F uses Stacks 0D86. Both sides are the abelian readings of Stacks 04DB of the corresponding functors of sheaves of sets — the same reading by which the terms a_{n,*}a_n^{-1}F of the Čech complex of Stacks 0D79 are built — and the isomorphism is the one of Stacks 0D86 carried through that reading, which is possible because both functors preserve finite products and the reading is functorial in the finite-product-preserving functor.

def abelianLocalizationPushforwardPullbackNatIsoSheafHomPrime
    (J : GrothendieckTopology C) (K : FormalCoproduct.{u} C) :
    abelianLocalizationPushPull J K ≅ abelianSheafHomPrime J K

CategoryTheory.SemiRepresentable.localizationPushforwardPullbackNatIsoSheafHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/PushPull.lean, line 263.

Stacks 0D86. For a semi-representable object K = {U i}, the product of the localization push-pull functors j_{i,*} j_i^{-1} is naturally isomorphic to SheafHom(F(K)^#, -). This is the source's j_* j^{-1} F = SheafHom(F(K)^#, F) under the product description of sheaves on C / K, naturally in F.

noncomputable def localizationPushforwardPullbackNatIsoSheafHom
    (J : GrothendieckTopology C) (K : FormalCoproduct.{u} C) :
    (Functor.pi' (fun i : K.I =>
        localizationPullback (K.obj i) J ⋙ localizationPushforward (K.obj i) J) ⋙
        Pi.functor K.I) ≅
      CategoryTheory.SheafHomAdj.sheafHomFunctor
        ((presheafToSheaf J (Type u)).obj ((FormalCoproduct.yoneda (C := C)).obj K))

Tag 0D87, a lemma

Tag 0D87 in the Stacks Project.

CategoryTheory.SemiRepresentable.componentwiseRelocalization_comp_sheafEquivalence_iso_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Relocalization.lean, line 405. The attribute's comment: “(3): f^{-1} corresponds to base change along F(K)^sharp to F(L)^sharp”.

Stacks 0D87 part (3). Under the identifications of part (1), the relocalization inverse image f^{-1} : Sh(C / L) ⥤ Sh(C / K) along a morphism f : K ⟶ L of semi-representable objects is base change along F(K)^♯ ⟶ F(L)^♯: an object G ⟶ F(L)^♯ is sent to G ×_{F(L)^♯} F(K)^♯ ⟶ F(K)^♯.

Following the source, this is Stacks 04IL applied to each re-localization morphism C / K.obj i ⟶ C / L.obj (f.f i) — that is hComponent — and then assembled over the index set by assembleOverPullbackIso, which is where the van Kampen property of the coproduct F(K)^♯ = ∐ i, h_{K.obj i}^♯ is used.

theorem componentwiseRelocalization_comp_sheafEquivalence_iso_pullback
    {K L : FormalCoproduct.{v} C} (f : K ⟶ L) :
    Nonempty
      (componentwiseRelocalization J f ⋙ (sheafEquivalence J K).functor ≅
        (sheafEquivalence J L).functor ⋙
          Over.pullback (formalCoproductSheafificationMap J f))

CategoryTheory.SemiRepresentable.isEquivalence_sheafFunctorToOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/SheavesOverSheafification.lean, line 200. The attribute's comment: “(1): the functor j_! is an equivalence Sh(C/K) to Sh(C)/F(K)^sharp”. References: SGA 4 III (5.4), “special case”.

Stacks 0D87 part (1). The lower shriek functor j_! identifies sheaves on the localization of C at a semi-representable object K with sheaves over the associated sheaf F(K)^♯.

Following the source: Sh(C / K) is the product of the Sh(C / K.obj i) — which is how SheafOverFormalCoproduct presents it — and Sh(C)/F(K)^♯ is the product of the Sh(C)/h_{K.obj i}^♯ by isEquivalence_sheafCoproductToOver, so the statement follows from Stacks 00Y1 for each component.

theorem isEquivalence_sheafFunctorToOver : (sheafFunctorToOver J K).IsEquivalence

CategoryTheory.SemiRepresentable.sheafEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/SheavesOverSheafification.lean, line 208. The attribute's comment: “(1): the resulting equivalence of categories Sh(C/K) to Sh(C)/F(K)^sharp”.

Stacks 0D87 part (1), as an equivalence of categories Sh(C / K) ≌ Sh(C) / F(K)^♯. Its functor is sheafFunctorToOver, the sheaf level j_! viewed as a functor into the slice (sheafEquivalence_functor).

noncomputable def sheafEquivalence :
    SheafOverFormalCoproduct J K ≌ Over (formalCoproductSheafification J K)

CategoryTheory.SemiRepresentable.componentwiseRestrictionCompSheafFunctorToOverIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/SheavesOverSheafification.lean, line 373. The attribute's comment: “(2): j^{-1} corresponds to F maps to (F times F(K)^sharp over F(K)^sharp)”.

Stacks 0D87 part (2). Under the identification of part (1), restriction j^{-1} : Sh(C) ⥤ Sh(C / K) is F ↦ (F × F(K)^♯ ⟶ F(K)^♯), i.e. Mathlib's CategoryTheory.toOver (F(K)^♯).

Following the source: toOver A is right adjoint to Over.forget A, and so is j^{-1} ⋙ j_! read in the slice, because j_! ⋙ Over.forget A ⊣ j^{-1} (sheafFunctorToOverForgetAdjunction) and j_! is an equivalence by part (1). Uniqueness of right adjoints identifies them.

noncomputable def componentwiseRestrictionCompSheafFunctorToOverIso :
    componentwiseRestriction J K ⋙ sheafFunctorToOver J K ≅
      toOver (formalCoproductSheafification J K)

CategoryTheory.SemiRepresentable.componentwiseRestriction_comp_sheafEquivalence_iso_toOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/SheavesOverSheafification.lean, line 387. The attribute's comment: “(2): under the equivalence of (1), j^{-1} is toOver of F(K)^sharp”.

Stacks 0D87 part (2), stated through the equivalence of categories of part (1): under sheafEquivalence, componentwise restriction corresponds to toOver (F(K)^♯).

theorem componentwiseRestriction_comp_sheafEquivalence_iso_toOver :
    Nonempty (componentwiseRestriction J K ⋙ (sheafEquivalence J K).functor ≅
      toOver (formalCoproductSheafification J K))

Tag 0D88, a lemma

Tag 0D88 in the Stacks Project.

CategoryTheory.SemiRepresentable.injective_localizationInverseImage_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Injective.lean, line 88. The attribute's comment: “injectives are preserved”.

Stacks 0D88. The inverse image along the localization at a semi-representable object sends injective abelian sheaves to injective abelian sheaves.

theorem injective_localizationInverseImage_obj
    (I : Sheaf J AddCommGrpCat.{max u v t}) [Injective I] :
    Injective ((localizationInverseImage J K AddCommGrpCat.{max u v t}).obj I)

CategoryTheory.SemiRepresentable.isKInjective_localizationInverseImage_mapHomologicalComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/KInjective.lean, line 176. The attribute's comment: “K-injective complexes are preserved”.

Stacks 0D88. Inverse image along the localization at a semi-representable object sends a K-injective complex of abelian sheaves to a K-injective complex.

theorem isKInjective_localizationInverseImage_mapHomologicalComplex
    (I : CochainComplex (Sheaf J AddCommGrpCat.{max u v w}) ℤ) [I.IsKInjective] :
    ((localizationInverseImageMapHomologicalComplex J K).obj I).IsKInjective

Tag 0D89, a remark

Tag 0D89 in the Stacks Project.

CategoryTheory.SemiRepresentable.componentwiseLocalizationFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Over.lean, line 87. The attribute's comment: “localization”.

The localization functor from the componentwise site C / K of a semi-representable object K over X to C / X. On the component indexed by i it is relocalization along K.obj i : U i ⟶ X.

def componentwiseLocalizationFunctor {X : C} (K : FormalCoproduct.{w} (Over X)) :
    ComponentOver (⟨K.I, fun i => (K.obj i).left⟩ : FormalCoproduct.{w} C) ⥤ Over X

CategoryTheory.SemiRepresentable.componentwiseLocalizationFunctorCompIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Over.lean, line 94. The attribute's comment: “localization”.

On each component, the functor C / K ⥤ C / X is canonically the relocalization functor associated to the structural map U i ⟶ X.

def componentwiseLocalizationFunctorCompIso {X : C} (K : FormalCoproduct.{w} (Over X))
    (i : K.I) :
    CategoryTheory.Sigma.incl (C := fun i : K.I => Over (K.obj i).left) i ⋙
      componentwiseLocalizationFunctor K ≅ Over.map (K.obj i).hom

CategoryTheory.SemiRepresentable.componentwiseLocalization_isContinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Over.lean, line 195. The attribute's comment: “localization_property”.

Stacks 0D89. The componentwise localization functor to C / X is continuous.

instance componentwiseLocalization_isContinuous :
    (componentwiseLocalizationFunctor K).IsContinuous
      (componentwiseTopology J
        (⟨K.I, fun i => (K.obj i).left⟩ : FormalCoproduct.{w} C))
  (J.over X)

CategoryTheory.SemiRepresentable.componentwiseLocalization_isCocontinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Over.lean, line 211. The attribute's comment: “localization_property”.

Stacks 0D89. The componentwise localization functor to C / X is cocontinuous.

instance componentwiseLocalization_isCocontinuous :
    (componentwiseLocalizationFunctor K).IsCocontinuous
      (componentwiseTopology J
        (⟨K.I, fun i => (K.obj i).left⟩ : FormalCoproduct.{w} C))
  (J.over X)

CategoryTheory.SemiRepresentable.componentwiseLocalization_hasCoverPullbacks, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Over.lean, line 228. The attribute's comment: “localization_property”.

Stacks 0D89. The componentwise localization functor to C / X has property P: pullbacks of covering families along maps out of its image are representable and cover.

lemma componentwiseLocalization_hasCoverPullbacks
    [(J.over X).toCoverage.HasPullbacks] :
    ∀ (𝒱 : Covering.{max u v, v, w'} (Over X)),
      𝒱.2.presieve₀ ∈ (J.over X).toCoverage 𝒱.1 →
      ∀ (U : ComponentOver
        (⟨K.I, fun i => (K.obj i).left⟩ : FormalCoproduct.{w} C))
        (g : (componentwiseLocalizationFunctor K).obj U ⟶ 𝒱.1),
        ∃ (P : 𝒱.2.I₀ → ComponentOver
            (⟨K.I, fun i => (K.obj i).left⟩ : FormalCoproduct.{w} C))
          (p₁ : ∀ i, P i ⟶ U)
          (p₂ : ∀ i, (componentwiseLocalizationFunctor K).obj (P i) ⟶ 𝒱.2.X i),
          (∀ i,
            (componentwiseLocalizationFunctor K).map (p₁ i) ≫ g =
              p₂ i ≫ 𝒱.2.f i ∧
              ∀ (T : ComponentOver
                  (⟨K.I, fun i => (K.obj i).left⟩ : FormalCoproduct.{w} C))
                (a : T ⟶ U)
                (b : (componentwiseLocalizationFunctor K).obj T ⟶ 𝒱.2.X i),
                (componentwiseLocalizationFunctor K).map a ≫ g = b ≫ 𝒱.2.f i →
                  ∃! l : T ⟶ P i,
                    (l ≫ p₁ i = a ∧
                      (componentwiseLocalizationFunctor K).map l ≫ p₂ i = b)) ∧
            (PreZeroHypercover.mk 𝒱.2.I₀ P p₁).presieve₀ ∈
              (componentwiseTopology J
                (⟨K.I, fun i => (K.obj i).left⟩ : FormalCoproduct.{w} C)).toCoverage U

CategoryTheory.SemiRepresentable.componentwiseRelocalizationMorphismOfTopoi, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Over.lean, line 358. The attribute's comment: “relocalization”.

Stacks 0D89. The morphism of topoi from Sh(C / K) to Sh(C / L) induced by componentwise relocalization along a morphism K ⟶ L of SR(C, X), together with the identification of its inverse image with restriction along the componentwise functor.

noncomputable def componentwiseRelocalizationMorphismOfTopoi
    {K L : FormalCoproduct.{w} (Over X)} (f : K ⟶ L) :
    let S := componentwiseLocalizationSitesOver J X f
    { g : MorphismOfTopoi
        (Sheaf S.sourceTopology (Type (max w v u)))
        (Sheaf S.targetTopology (Type (max w v u))) //
      g.inverseImage ⋙ sheafToPresheaf S.sourceTopology (Type (max w v u)) =
        sheafToPresheaf S.targetTopology (Type (max w v u)) ⋙
          (CategoryTheory.Functor.whiskeringLeft _ _ _).obj S.relocalizationFunctor.op }

CategoryTheory.SemiRepresentable.componentwiseRelocalization_isContinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Over.lean, line 379. The attribute's comment: “relocalization_property”.

Stacks 0D89. The componentwise relocalization functor is continuous.

instance componentwiseRelocalization_isContinuous
    {K L : FormalCoproduct.{w} (Over X)} (f : K ⟶ L) :
    let S := componentwiseLocalizationSitesOver J X f
    S.relocalizationFunctor.IsContinuous S.sourceTopology S.targetTopology

CategoryTheory.SemiRepresentable.componentwiseRelocalization_isCocontinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Over.lean, line 387. The attribute's comment: “relocalization_property”.

Stacks 0D89. The componentwise relocalization functor is cocontinuous.

instance componentwiseRelocalization_isCocontinuous
    {K L : FormalCoproduct.{w} (Over X)} (f : K ⟶ L) :
    let S := componentwiseLocalizationSitesOver J X f
    S.relocalizationFunctor.IsCocontinuous S.sourceTopology S.targetTopology

CategoryTheory.SemiRepresentable.componentwiseRelocalization_hasCoverPullbacks, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Over.lean, line 396. The attribute's comment: “relocalization_property”.

Stacks 0D89. The componentwise relocalization functor has property P: pullbacks of covering families along maps out of its image are representable and covering.

lemma componentwiseRelocalization_hasCoverPullbacks
    {K L : FormalCoproduct.{w} (Over X)} (f : K ⟶ L)
    [J.toCoverage.HasPullbacks] :
    let S := componentwiseLocalizationSitesOver J X f
    S.relocalizationFunctor.HasCoverPullbacks
      (fun 𝒰 ↦ 𝒰.2.presieve₀ ∈ S.sourceTopology.toCoverage 𝒰.1)
      (fun 𝒱 ↦ 𝒱.2.presieve₀ ∈ S.targetTopology.toCoverage 𝒱.1)

CategoryTheory.SemiRepresentable.componentwiseLocalizationPushforwardPullbackNatIsoSheafHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/OverPushPull.lean, line 260. The attribute's comment: “push_pull”.

Stacks 0D89. The localization push-pull on C / X at a semi-representable object K over X is naturally the sheaf internal hom out of the sheafification of the semi-representable presheaf associated to K.

noncomputable def componentwiseLocalizationPushforwardPullbackNatIsoSheafHom
    {C : Type u} [SmallCategory C] (J : GrothendieckTopology C) (X : C)
    (K : FormalCoproduct.{u} (Over X)) :
    ((componentwiseLocalizationFunctor K).sheafPushforwardContinuous
      (Type u)
      (componentwiseTopology J
        (⟨K.I, fun i => (K.obj i).left⟩ : FormalCoproduct.{u} C))
      (J.over X)) ⋙
      ((componentwiseLocalizationFunctor K).sheafPushforwardCocontinuous
        (Type u)
        (componentwiseTopology J
          (⟨K.I, fun i => (K.obj i).left⟩ : FormalCoproduct.{u} C))
        (J.over X)) ≅
      CategoryTheory.SheafHomAdj.sheafHomFunctor
        ((presheafToSheaf (J.over X) (Type u)).obj
        ((FormalCoproduct.yoneda (C := Over X)).obj K))

Declarations registered for the tag:

CategoryTheory.SemiRepresentable.ComponentOver, declared in the repository, registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Over.lean, line 409 (StacksFrontier): “site”.
CategoryTheory.SemiRepresentable.componentwiseTopology, declared in the repository, registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Over.lean, line 410 (StacksFrontier): “site”.
CategoryTheory.SemiRepresentable.formalCoproductSliceSheavesEquivalence, declared in the repository, registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Over.lean, line 411 (StacksFrontier): “product”.

Tag 0D9U, a remark

Tag 0D9U in the Stacks Project.

AlgebraicGeometry.RingedSite.familyLowerShriek_iso_directSum, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Family/DirectSum.lean, line 215. The attribute's comment: “part (3): j_! is the direct sum of the j_{i,!}”.

Stacks 0D9U, part (3): the direct-sum formula. In terms of the product decomposition of part (2), j_! sends a family (F i) to ⨁ i, j_{i,!} F i: both are left adjoint to j^*.

noncomputable def familyLowerShriek_iso_directSum :
    familyLowerShriek X K ≅ familyDirectSumLowerShriek X K

AlgebraicGeometry.RingedSite.familyLowerShriek_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Family/DirectSum.lean, line 241. The attribute's comment: “part (3): j_! is exact”.

Stacks 0D9U, part (3). The lower shriek j_! is exact: it preserves finite colimits because it is a left adjoint, and finite limits because it is the direct sum of the exact functors j_{i,!}.

theorem familyLowerShriek_exact : exactFunctor _ _ (familyLowerShriek X K)

AlgebraicGeometry.RingedSite.lowerShriekModules_iso_familyLowerShriek, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Family/DirectSum.lean, line 357. The attribute's comment: “part (3): j_! is the left adjoint of the pullback of modules along j”.

Stacks 0D9U, part (3). The lower shriek of the morphism of ringed topoi j — the left adjoint of the pullback j^* of sheaves of modules, which is what the source means by j_! — is familyLowerShriek up to the equivalence by which j^* differs from restriction.

noncomputable def lowerShriekModules_iso_familyLowerShriek :
    (familyLocalizationMorphism X K).lowerShriekModules ≅
      (familyPullbackScalarsEquivalence X K).inverse ⋙ familyLowerShriek X K

AlgebraicGeometry.RingedSite.lowerShriekModules_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Family/DirectSum.lean, line 383. The attribute's comment: “part (3): the left adjoint of j^* is exact”.

Stacks 0D9U, part (3). The lower shriek of the morphism of ringed topoi j, the left adjoint of j^*, is exact: it is familyLowerShriek, which is exact, composed with an equivalence.

theorem lowerShriekModules_exact (X : RingedSite.{u, u, u}) (K : FormalCoproduct.{u} X.C) :
    exactFunctor _ _ ((familyLocalizationMorphism X K).lowerShriekModules)

AlgebraicGeometry.RingedSite.morphismRestr_isRightAdjoint, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Family/DirectSum.lean, line 729. The attribute's comment: “f^* has a left adjoint f_!”.

Stacks 0D9U. f^* has a left adjoint f_!.

instance morphismRestr_isRightAdjoint : (morphismRestr X f).IsRightAdjoint

AlgebraicGeometry.RingedSite.morphismLowerShriek_iso_directSum, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Family/DirectSum.lean, line 735. The attribute's comment: “f_! is the direct sum of the componentwise lower shrieks”.

Stacks 0D9U. In terms of the product decomposition of part (2), f_! sends a family (F i) to ⨁ i, f_{i,!} F i: both are left adjoint to f^*.

noncomputable def morphismLowerShriek_iso_directSum :
    (morphismRestr X f).leftAdjoint ≅
      (componentwiseModuleRestrictionEquivalence X K).functor ⋙
        piCoproduct (morphismComponentLowerShriek X f)

AlgebraicGeometry.RingedSite.morphismLowerShriek_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Family/DirectSum.lean, line 746. The attribute's comment: “f_! is exact”.

Stacks 0D9U. The lower shriek f_! is exact: it preserves finite colimits because it is a left adjoint, and finite limits because it is the direct sum of the exact functors f_{i,!}, coproducts of sheaves of modules being exact.

theorem morphismLowerShriek_exact : exactFunctor _ _ (morphismRestr X f).leftAdjoint

AlgebraicGeometry.RingedSite.familyMorphism_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Family/Flat.lean, line 248. The attribute's comment: “f_flat”.

Stacks 0D9U. The morphism of ringed topoi induced by a morphism of semi-representable objects is flat.

theorem familyMorphism_isFlat (X : RingedSite.{u, v, max u v w r})
    {K L : FormalCoproduct.{w} X.C} (f : K ⟶ L) :
    Stacks.Sheaf.RingedToposFlat.RingedToposHom.IsFlat.{max u v w, max u v w,
        max u v w r, max u v w, max u v w, max u v w r}
      (familyMorphism.{w, v, u, r} X f).val

AlgebraicGeometry.RingedSite.familyLocalizationMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Family/Localization.lean, line 191. The attribute's comment: “part (3): the localization morphism j of ringed topoi”.

Stacks 0D9U, part (3). The localization morphism j : (Sh(C / K), O_K) ⟶ (Sh(C), O_X) of ringed topoi attached to a semi-representable object K: its geometric morphism is restriction along the componentwise localization functor and its structure map is the canonical identity comparison of structure sheaves.

noncomputable def familyLocalizationMorphism (X : RingedSite.{u, v, max u v w})
    (K : FormalCoproduct.{w} X.C) :
    RingedToposHom (localizationRingedTopos X K) (ringedTopos.{u, v, w} X)

AlgebraicGeometry.RingedSite.familyLocalizationMorphism_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Family/Localization.lean, line 234. The attribute's comment: “part (3): j is flat”.

Stacks 0D9U. The localization morphism j is flat: its inverse-image structure map is an isomorphism, and an isomorphism of sheaves of commutative rings is flat.

theorem familyLocalizationMorphism_isFlat (X : RingedSite.{u, v, max u v w})
    (K : FormalCoproduct.{w} X.C) :
    AlgebraicGeometry.SheafOfModules.IsFlatMapULift
      (familyLocalizationMorphism X K).fSharpInverseImage

AlgebraicGeometry.RingedSite.familyLocalizationMorphism_pullback_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Family/Localization.lean, line 246. The attribute's comment: “part (3): j^* is exact”.

Stacks 0D9U. Pullback of sheaves of modules along the localization morphism is exact, the morphism being flat.

theorem familyLocalizationMorphism_pullback_exact (X : RingedSite.{u, v, max u v w})
    (K : FormalCoproduct.{w} X.C) :
    exactFunctor _ _ (Stacks.Sheaves.RingedToposModules.RingedToposHom.pullbackModules
      (X := localizationRingedTopos X K) (Y := ringedTopos.{u, v, w} X)
      (familyLocalizationMorphism X K).toRingedToposModulesHom)

AlgebraicGeometry.RingedSite.familyLocalizationMorphism_pullback_isRightAdjoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Family/Localization.lean, line 260. The attribute's comment: “part (3): j^* has a left adjoint j_!”.

Stacks 0D9U. Pullback of sheaves of modules along the localization morphism has a left adjoint j_!, namely AlgebraicGeometry.RingedToposHom.lowerShriekModules of that morphism: the structure map is an isomorphism, and the inverse image of sheaves of modules is restriction along the componentwise localization functor, which has a left adjoint because C / K is essentially small.

theorem familyLocalizationMorphism_pullback_isRightAdjoint (X : RingedSite.{u, v, max u v w})
    (K : FormalCoproduct.{w} X.C) :
    (familyLocalizationMorphism X K).toModulesHom.pullbackModules.IsRightAdjoint

AlgebraicGeometry.RingedSite.familyMorphism_pullback_isRightAdjoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Family/Localization.lean, line 275. The attribute's comment: “part (3): f^* has a left adjoint f_!”.

Stacks 0D9U. Pullback of sheaves of modules along the morphism of ringed topoi attached to a morphism f : K ⟶ L of semi-representable objects has a left adjoint f_!, namely AlgebraicGeometry.RingedToposHom.lowerShriekModules of that morphism: the structure map is an isomorphism and the inverse image of sheaves of modules is restriction along the componentwise relocalization functor, which has a left adjoint because C / K is essentially small.

theorem familyMorphism_pullback_isRightAdjoint (X : RingedSite.{u, v, max u v w})
    {K L : FormalCoproduct.{w} X.C} (f : K ⟶ L) :
    (familyMorphism.{w, v, u, u} X f).val.toModulesHom.pullbackModules.IsRightAdjoint

AlgebraicGeometry.RingedSite.familyComponentInclLowerShriek_comp_familyLowerShriek, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Family/Localization.lean, line 395. The attribute's comment: “part (3): j_! is j_{i,!} on the i-th summand”.

Stacks 0D9U, part (3). On the i-th summand of the decomposition Mod(O_K) = ∏ Mod(O_{U i}) the lower shriek j_! is the extension by zero j_{i,!} of that component: the inclusion of the i-th component followed by the componentwise localization functor is the localization functor of U i, so the two left adjoints agree. This is the sentence of the source that j_! sends (F i) to ⨁ j_{i,!} F i, read one summand at a time.

noncomputable def familyComponentInclLowerShriek_comp_familyLowerShriek
    (X : RingedSite.{u, v, max u v w}) (K : FormalCoproduct.{w} X.C) (i : K.I) :
    familyComponentInclLowerShriek X K i ⋙ familyLowerShriek X K ≅
      familyComponentLowerShriek X K i

AlgebraicGeometry.RingedSite.moduleSheavesProductEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Family/ModuleProduct.lean, line 411. The attribute's comment: “module_product”.

Modules on the disjoint union of localized ringed sites are componentwise modules, via the canonical componentwise restriction functor.

noncomputable def moduleSheavesProductEquivalence
    (X : RingedSite.{u, u, u}) (K : FormalCoproduct.{w} X.C) :
    { e : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf (X.localization K).O) ≌
      ((i : K.I) → SheafOfModules.{u}
          (Stacks.SheafOfModules.Tensor.ringSheaf (X.over (K.obj i)).O)) //
      e.functor = componentwiseModuleRestriction X K }

AlgebraicGeometry.RingedSite.moduleSheavesProductEquivalence', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Family/ModuleProduct.lean, line 467. The attribute's comment: “module_product”.

Modules on the disjoint union of localized ringed sites are componentwise modules, via the canonical componentwise restriction functor.

noncomputable def moduleSheavesProductEquivalence'
    (X : RingedSite.{u, v, r}) (K : FormalCoproduct.{w} X.C) :
    { e : SheafOfModules.{t} (Stacks.SheafOfModules.Tensor.ringSheaf (X.localization' K).O) ≌
      ((i : K.I) → SheafOfModules.{t}
          (Stacks.SheafOfModules.Tensor.ringSheaf (X.over (K.obj i)).O)) //
      e.functor = componentwiseModuleRestriction' X K }

AlgebraicGeometry.RingedSite.familyMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Family/Morphism.lean, line 104. The attribute's comment: “family_morphism”.

Stacks 0D9U. A morphism of semi-representable objects induces a morphism of the ringed topoi of their componentwise localizations: its inverse image on sheaves of sets is restriction along the componentwise relocalization functor, and its structure map is the canonical identity comparison, which is an isomorphism.

noncomputable def familyMorphism (X : RingedSite.{u, v, max u v w r})
    {K L : FormalCoproduct.{w} X.C} (f : K ⟶ L) :
    let S : LocalizationSites.{w} X.C X.J := ⟨K, L, f⟩
    { g : RingedToposHom (localizationRingedTopos X K) (localizationRingedTopos X L) //
      (g.toToposHom.inverseImage ⋙
          sheafToPresheaf S.sourceTopology (Type (max u v w r)) =
        sheafToPresheaf S.targetTopology (Type (max u v w r)) ⋙
          (CategoryTheory.Functor.whiskeringLeft _ _ _).obj S.relocalizationFunctor.op) ∧
      (∃ h : (localizationRingedTopos X K).forgetRing.obj
          ((inverseImageCommRingFunctor g.toToposHom).obj
            (localizationRingedTopos X L).O) =
          (localizationRingedTopos X K).forgetRing.obj (localizationRingedTopos X K).O,
        (localizationRingedTopos X K).forgetRing.map g.fSharpInverseImage =
          eqToHom h) ∧
      IsIso g.fSharpInverseImage }

AlgebraicGeometry.RingedSite.familyMorphism_pullback_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Family/PullbackExact.lean, line 54. The attribute's comment: “f_flat”.

Stacks 0D9U. Pullback of sheaves of modules along the morphism of ringed topoi induced by a morphism of semi-representable objects is exact.

theorem familyMorphism_pullback_exact (X : RingedSite.{u, v, max u v w r})
    {K L : FormalCoproduct.{w} X.C} (f : K ⟶ L)
    [(componentwiseTopology X.J K).HasSheafCompose
      (forget₂ CommRingCat.{max u v w r} RingCat.{max u v w r})]
    [(componentwiseTopology X.J L).HasSheafCompose
      (forget₂ CommRingCat.{max u v w r} RingCat.{max u v w r})]
    [(componentwiseTopology X.J K).HasSheafCompose (forget RingCat.{max u v w r})]
    [(componentwiseTopology X.J L).HasSheafCompose (forget RingCat.{max u v w r})]
    [(componentwiseTopology X.J K).HasSheafCompose (forget AddCommGrpCat.{max u v w r})]
    [(componentwiseTopology X.J L).HasSheafCompose (forget AddCommGrpCat.{max u v w r})]
    [HasWeakSheafify (componentwiseTopology X.J K) AddCommGrpCat.{max u v w r}]
    [(componentwiseTopology X.J K).WEqualsLocallyBijective
      AddCommGrpCat.{max u v w r}] :
    exactFunctor _ _
      ((familyMorphism.{w, v, u, r} X f).val.toRingedToposModulesHom.pullbackModules)

Declarations registered for the tag:

AlgebraicGeometry.RingedSite.localizationStructureSheaf, declared in the repository, registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Family/PullbackExact.lean, line 80 (StacksFrontier): “structure_sheaf_o_k”.
AlgebraicGeometry.RingedSite.localization, declared in the repository, registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/Family/PullbackExact.lean, line 83 (StacksFrontier): “ringed_site”.

Tag 0D9V, a remark

Tag 0D9V in the Stacks Project.

AlgebraicGeometry.RingedSite.localizationToposMorphismOver, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/RingedOver.lean, line 185. The attribute's comment: “part (3): the geometric morphism underlying the localization over Y”.

Stacks 0D9V, part (3). The geometric morphism Sh(C / K) ⟶ Sh(C / Y) underlying the localization morphism of a semi-representable object K over Y: its inverse image is restriction along the componentwise localization functor C / K ⥤ C / Y and its direct image is the right adjoint of that restriction.

noncomputable def localizationToposMorphismOver (X : RingedSite.{u, v, max u v w}) {Y : X.C}
    (K : FormalCoproduct.{w} (Over Y)) :
    MorphismOfTopoi
      (Sheaf (componentwiseTopology X.J (underlyingFormalCoproduct X K)) (Type (max u v w)))
      (Sheaf (X.J.over Y) (Type (max u v w)))

AlgebraicGeometry.RingedSite.localizationStructureIsoOver, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/RingedOver.lean, line 213. The attribute's comment: “part (3): the structure map of the localization over Y”.

Stacks 0D9V, part (3). The structure map of the localization morphism over Y, in inverse-image form: the inverse image of O_Y along restriction is the restriction of O_Y, and that restriction is O_K because the composite of the componentwise localization functor with the slice projection is the componentwise localization functor to C.

noncomputable def localizationStructureIsoOver (X : RingedSite.{u, v, max u v w}) {Y : X.C}
    (K : FormalCoproduct.{w} (Over Y)) :
    (inverseImageCommRingFunctor (localizationToposMorphismOver X K)).obj
        (ringedTopos.{max u v, v, w} (X.over Y)).O ≅
      (localizationRingedTopos X (underlyingFormalCoproduct X K)).O

AlgebraicGeometry.RingedSite.localizationMorphismOver, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/RingedOver.lean, line 236. The attribute's comment: “part (3): the localization morphism of ringed topoi over Y”.

Stacks 0D9V, part (3). The localization morphism j : (Sh(C / K), O_K) ⟶ (Sh(C / Y), O_Y) of ringed topoi attached to a semi-representable object K over Y: its geometric morphism is restriction along the componentwise localization functor and its structure map is the canonical identity comparison of structure sheaves.

noncomputable def localizationMorphismOver (X : RingedSite.{u, v, max u v w}) {Y : X.C}
    (K : FormalCoproduct.{w} (Over Y)) :
    RingedToposHom (localizationRingedTopos X (underlyingFormalCoproduct X K))
      (ringedTopos.{max u v, v, w} (X.over Y))

AlgebraicGeometry.RingedSite.forgetRing_localizationMorphismOver_fSharpInverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/RingedOver.lean, line 308. The attribute's comment: “part (3): the structure map of the localization over Y is the identity”.

Stacks 0D9V, part (3). The structure map of the localization morphism over Y is the canonical identity comparison: on underlying sheaves of sets it is the identification forgetRing_inverseImage_structureSheaf_over and nothing more.

theorem forgetRing_localizationMorphismOver_fSharpInverseImage
    (X : RingedSite.{u, v, max u v w}) {Y : X.C} (K : FormalCoproduct.{w} (Over Y)) :
    (localizationRingedTopos X (underlyingFormalCoproduct X K)).forgetRing.map
        (localizationMorphismOver X K).fSharpInverseImage =
      eqToHom (forgetRing_inverseImage_structureSheaf_over X K)

AlgebraicGeometry.RingedSite.localizationMorphismOver_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/RingedOver.lean, line 335. The attribute's comment: “flatness of the localization morphism over Y”.

Stacks 0D9V. The localization morphism over Y is flat: its inverse-image structure map is an isomorphism, and an isomorphism of sheaves of commutative rings is flat.

theorem localizationMorphismOver_isFlat (X : RingedSite.{u, v, max u v w}) {Y : X.C}
    (K : FormalCoproduct.{w} (Over Y)) :
    AlgebraicGeometry.SheafOfModules.IsFlatMapULift
      (localizationMorphismOver X K).fSharpInverseImage

AlgebraicGeometry.RingedSite.localizationMorphismOver_pullback_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/RingedOver.lean, line 348. The attribute's comment: “exactness of the pullback of modules along the localization over Y”.

Stacks 0D9V. Pullback of sheaves of modules along the localization morphism over Y is exact, the morphism being flat.

theorem localizationMorphismOver_pullback_exact (X : RingedSite.{u, v, max u v w}) {Y : X.C}
    (K : FormalCoproduct.{w} (Over Y)) :
    exactFunctor _ _ ((localizationMorphismOver X K).toRingedToposModulesHom.pullbackModules)

AlgebraicGeometry.RingedSite.localizationMorphismOver_pullback_isRightAdjoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/RingedOver.lean, line 360. The attribute's comment: “the left adjoint of the pullback of modules along the localization over Y”.

Stacks 0D9V. Pullback of sheaves of modules along the localization morphism over Y has a left adjoint j_!, namely AlgebraicGeometry.RingedToposHom.lowerShriekModules of that morphism: the structure map is an isomorphism, and the inverse image of sheaves of modules is restriction along the componentwise localization functor, which has a left adjoint because C / K is essentially small.

theorem localizationMorphismOver_pullback_isRightAdjoint (X : RingedSite.{u, v, max u v w})
    {Y : X.C} (K : FormalCoproduct.{w} (Over Y)) :
    (localizationMorphismOver X K).toModulesHom.pullbackModules.IsRightAdjoint

AlgebraicGeometry.RingedSite.familyMorphismOver, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/RingedOver.lean, line 376. The attribute's comment: “part (4): the morphism of ringed topoi attached to a morphism of SR(C, Y)”.

Stacks 0D9V, part (4). The morphism of ringed topoi (Sh(C / K), O_K) ⟶ (Sh(C / L), O_L) attached to a morphism K ⟶ L of semi-representable objects over Y: it is the morphism of Stacks 0D9U attached to the induced morphism of the underlying semi-representable objects of C, since neither the two localization sites nor their structure sheaves see the structural maps to Y. Its inverse image and its structure map are specified by AlgebraicGeometry.RingedSite.familyMorphism.

noncomputable def familyMorphismOver (X : RingedSite.{u, v, max u v w}) {Y : X.C}
    {K L : FormalCoproduct.{w} (Over Y)} (f : K ⟶ L) :
    RingedToposHom (localizationRingedTopos X (underlyingFormalCoproduct X K))
      (localizationRingedTopos X (underlyingFormalCoproduct X L))

AlgebraicGeometry.RingedSite.familyMorphismOver_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/RingedOver.lean, line 407. The attribute's comment: “flatness of the morphism attached to a morphism of SR(C, Y)”.

Stacks 0D9V. The morphism attached to a morphism of SR(C, Y) is flat. This is the corresponding clause of Stacks 0D9U for the induced morphism of underlying semi-representable objects of C.

theorem familyMorphismOver_isFlat (X : RingedSite.{u, v, max u v w}) {Y : X.C}
    {K L : FormalCoproduct.{w} (Over Y)} (f : K ⟶ L) :
    AlgebraicGeometry.SheafOfModules.IsFlatMapULift
      (familyMorphismOver X f).fSharpInverseImage

AlgebraicGeometry.RingedSite.familyMorphismOver_pullback_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/RingedOver.lean, line 418. The attribute's comment: “exactness of the pullback of modules along a morphism of SR(C, Y)”.

Stacks 0D9V. Pullback of sheaves of modules along the morphism attached to a morphism of SR(C, Y) is exact, that morphism being flat.

theorem familyMorphismOver_pullback_exact (X : RingedSite.{u, v, max u v w}) {Y : X.C}
    {K L : FormalCoproduct.{w} (Over Y)} (f : K ⟶ L) :
    exactFunctor _ _ ((familyMorphismOver X f).toRingedToposModulesHom.pullbackModules)

AlgebraicGeometry.RingedSite.familyMorphismOver_pullback_isRightAdjoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/RingedOver.lean, line 430. The attribute's comment: “the left adjoint of the pullback of modules along a morphism of SR(C, Y)”.

Stacks 0D9V. Pullback of sheaves of modules along the morphism attached to a morphism of SR(C, Y) has a left adjoint f_!, namely AlgebraicGeometry.RingedToposHom.lowerShriekModules of that morphism: the structure map is an isomorphism and the inverse image of sheaves of modules is restriction along the componentwise relocalization functor, which has a left adjoint because C / K is essentially small.

theorem familyMorphismOver_pullback_isRightAdjoint (X : RingedSite.{u, v, max u v w}) {Y : X.C}
    {K L : FormalCoproduct.{w} (Over Y)} (f : K ⟶ L) :
    (familyMorphismOver X f).toModulesHom.pullbackModules.IsRightAdjoint

Declarations registered for the tag:

AlgebraicGeometry.RingedSite.localizationStructureSheaf, declared in the repository, registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/RingedOver.lean, line 461 (StacksFrontier): “part (1): the structure sheaf O_K”.
AlgebraicGeometry.RingedSite.localization, declared in the repository, registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/RingedOver.lean, line 464 (StacksFrontier): “part (1): the ringed site (C / K, O_K)”.
AlgebraicGeometry.RingedSite.moduleSheavesProductEquivalence, declared in the repository, registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/SemiRepresentable/RingedOver.lean, line 467 (StacksFrontier): “part (2): the decomposition of Mod(O_K) into componentwise modules”.

Sources

Section85.16 The site associate to a simplicial semi-representable object #

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

Tag 0D8B, a lemma

Tag 0D8B in the Stacks Project.

CategoryTheory.SimplicialSemiRepresentable.augmentation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/SimplicialSemiRepresentableSite.lean, line 588. The attribute's comment: “j_0 defines an augmentation a_0 : Sh(C/K_0) to Sh(C), case (B) of 0D6Z”.

Stacks 0D8B. The localization functor j_0 : C/K_0 ⥤ C defines an augmentation of the simplicial site n ↦ C/K_n towards (C, J), as in case (B) of Stacks 0D6Z: it is cocontinuous, and its composite with the functor of a vertex of simplicial degree n is the localization functor j_n, which does not mention the vertex.

def augmentation : (simplicialSite J K).Augmentation (Cat.of C) J

CategoryTheory.SimplicialSemiRepresentable.augmentation_functor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/SimplicialSemiRepresentableSite.lean, line 603. The attribute's comment: “the functor underlying that augmentation is j_0”.

Stacks 0D8B. The functor underlying that augmentation is the degree-zero localization functor j_0. Together with CategoryTheory.SimplicialSemiRepresentable.augmentation this is the assertion that j_0 defines the augmentation.

theorem augmentation_functor :
    (augmentation J K).functor = sliceForget K (op (SimplexCategory.mk 0))

CategoryTheory.SimplicialSemiRepresentable.componentPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/SimplicialSemiRepresentableSite.lean, line 702. The attribute's comment: “a_n is the morphism of topoi of j_n: direct images”.

Stacks 0D8B. The morphism of topoi a_n : Sh(C/K_n) ⟶ Sh(C) which Stacks 0D70 attaches to the augmentation j_0 is the morphism of topoi of the localization functor j_n: their direct images agree canonically.

This one is an isomorphism and not an equality. Stacks 0D70 attaches to the augmentation the composite of the degree-zero morphism of topoi with the transition morphism of a vertex, whose direct image is a composite of two direct images; the direct image of j_n is a single one, for the composite site functor C/K_n ⥤ C/K_0 ⥤ C, which equals j_n. Direct images along cocontinuous functors compose only up to the canonical comparison, which is what this is.

noncomputable def componentPushforwardIso (n : SimplexCategory) :
    (SimplicialSiteSituation.Augmentation.componentAugmentation (situation J K) (Cat.of C) J
        (situationAugmentation J K) n).pushforward ≅
      (localizationMorphism J K n).pushforward

CategoryTheory.SimplicialSemiRepresentable.componentInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/SimplicialSemiRepresentableSite.lean, line 733. The attribute's comment: “a_n is the morphism of topoi of j_n: inverse images”.

Stacks 0D8B. The same identification in inverse images, obtained from uniqueness of left adjoints.

noncomputable def componentInverseImageIso (n : SimplexCategory) :
    (SimplicialSiteSituation.Augmentation.componentAugmentation (situation J K) (Cat.of C) J
        (situationAugmentation J K) n).inverseImage ≅
      (localizationMorphism J K n).inverseImage

CategoryTheory.SimplicialSemiRepresentable.totalPushforward_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/SimplicialSemiRepresentableSite.lean, line 757. The attribute's comment: “a is the morphism of topoi of j_total: the direct images are equal”.

Stacks 0D8B. The morphism of topoi a : Sh((C/K)_total) ⟶ Sh(C) which Stacks 0D70 attaches to the augmentation j_0 is the morphism of topoi of the localization functor j_total: their direct images are equal, not merely isomorphic, because the cocontinuous functor which Stacks 0D70 attaches to the augmentation is j_total on the nose.

theorem totalPushforward_eq :
    (CocontinuousSimplicialSite.Augmentation.totalMorphismOfTopoi
        (augmentation J K)).pushforward = (totalLocalizationMorphism J K).pushforward

CategoryTheory.SimplicialSemiRepresentable.totalInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/SimplicialSemiRepresentableSite.lean, line 782. The attribute's comment: “a is the morphism of topoi of j_total: inverse images”.

Stacks 0D8B. The same identification in inverse images, obtained from uniqueness of left adjoints.

noncomputable def totalInverseImageIso :
    (CocontinuousSimplicialSite.Augmentation.totalMorphismOfTopoi
        (augmentation J K)).inverseImage ≅ (totalLocalizationMorphism J K).inverseImage

Tag 09WM, a lemma

Tag 09WM in the Stacks Project.

CategoryTheory.SimplicialSemiRepresentable.augmentationSheafLowerShriekAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/SimplicialSemiRepresentableLowerShriek.lean, line 116. The attribute's comment: “part (1): the left adjoint on sheaves of sets”.

Stacks 09WM, part (1). The functor a^{Sh}_! : Sh((C/K)_total) ⥤ Sh(C) is left adjoint to the inverse image a^{-1} : Sh(C) ⥤ Sh((C/K)_total) of the augmentation.

The inverse image of the augmentation is restriction along j_total, because j_total is cocontinuous as well as continuous, and restriction along a continuous functor has a left adjoint.

def augmentationSheafLowerShriekAdjunction :
    augmentationSheafLowerShriek J K ⊣
      (CocontinuousSimplicialSite.Augmentation.totalMorphismOfTopoi
        (augmentation J K)).inverseImage

CategoryTheory.SimplicialSemiRepresentable.augmentationAbelianLowerShriekAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/SimplicialSemiRepresentableLowerShriek.lean, line 136. The attribute's comment: “part (2): the left adjoint on abelian sheaves”.

Stacks 09WM, part (2). The functor a_! : Ab((C/K)_total) ⥤ Ab(C) is left adjoint to the inverse image a^{-1} : Ab(C) ⥤ Ab((C/K)_total) of the augmentation, which on abelian sheaves as on sheaves of sets is restriction along j_total.

def augmentationAbelianLowerShriekAdjunction :
    augmentationAbelianLowerShriek J K ⊣
      (totalForget K).sheafPushforwardContinuous AddCommGrpCat.{u}
        ((situation J K).totalTopology) J

CategoryTheory.SimplicialSemiRepresentable.augmentationInverseImageComponentIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/SimplicialSemiRepresentableLowerShriek.lean, line 151. The attribute's comment: “part (3): the inverse image in each simplicial degree”.

Stacks 09WM, part (3). The inverse image of the augmentation followed by restriction to the simplicial degree n is the inverse image a_n^{-1} of the augmentation of that degree, which by Stacks 0D8B is the inverse image of the morphism of topoi of the localization functor j_n : C/K_n ⥤ C, that is restriction along j_n. So a^{-1}ℱ is in degree n the sheaf a_n^{-1}ℱ.

def augmentationInverseImageComponentIso (n : SimplexCategory) :
    (CocontinuousSimplicialSite.Augmentation.totalMorphismOfTopoi
          (augmentation J K)).inverseImage ⋙ (situation J K).restrict n ≅
      (localizationMorphism J K n).inverseImage

CategoryTheory.SimplicialSemiRepresentable.augmentationAbelianPushforwardFork, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/SimplicialSemiRepresentableLowerShriek.lean, line 191. The attribute's comment: “part (4): the direct image is the equalizer of the two vertex maps”.

Stacks 09WM, part (4). The fork of the direct image a_*𝒢 of an abelian sheaf on the total site over the two maps a_{0,*}𝒢_0 ⟶ a_{1,*}𝒢_1 attached to the two vertices of the one-simplex, which are the two cofaces of the cosimplicial sheaf n ↦ a_{n,*}𝒢_n. Its map is the canonical projection of a_*𝒢 onto a_{0,*}𝒢_0, and it equalises the two because the projections form a cone.

def augmentationAbelianPushforwardFork :
    Fork ((augmentationAbelianComponentDiagram J K G).map
        (SimplexCategory.const (SimplexCategory.mk 0) (SimplexCategory.mk 1) 0))
      ((augmentationAbelianComponentDiagram J K G).map
        (SimplexCategory.const (SimplexCategory.mk 0) (SimplexCategory.mk 1) 1))

CategoryTheory.SimplicialSemiRepresentable.augmentationAbelianPushforwardForkIsLimit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/SimplicialSemiRepresentableLowerShriek.lean, line 215. The attribute's comment: “part (4): the equalizer is a limit”.

Stacks 09WM, part (4). That fork is a limit: the direct image a_*𝒢 is the equalizer of the two maps a_{0,*}𝒢_0 ⟶ a_{1,*}𝒢_1.

The direct image is by construction the limit of the cosimplicial sheaf n ↦ a_{n,*}𝒢_n over the whole simplex category, and the degree-zero leg of such a limit is a limit fork of the two maps in degrees 0 ⇉ 1, which is the dual of Simplicial, Lemma 14.20.2.

def augmentationAbelianPushforwardForkIsLimit :
    IsLimit (augmentationAbelianPushforwardFork J K G)

Tag 0DC0, a lemma

Tag 0DC0 in the Stacks Project.

Stacks.Cohomology.SimplicialSummand.cohomologyObj_iso_summand, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/ComponentSumNaturality/SummandCohomology.lean, line 168.

Stacks 0DC0. Cohomology over an object of one summand of a simplicial semi-representable site agrees with the cohomology, with coefficients in the corresponding member of the family of sheaves attached to the restriction of the sheaf to that simplicial degree.

This is Stacks 0DBZ (Stacks.Cohomology.SimplicialComponent.cohomologyObj_iso_component) for the component inclusion, transported along the identification hsite of the degree-n site with the disjoint union of the summand slices, followed by the same bigger-site comparison again for the inclusion of the i-th summand slice.

def cohomologyObj_iso_summand
    (J : GrothendieckTopology C) (K : FormalCoproduct.{u} C)
    (S : SimplicialSiteSituation.{u}) (n : SimplexCategory)
    (hsite : (⟨S.component n, S.componentTopology n⟩ :
        Σ D : Cat.{u, u}, GrothendieckTopology D) =
      ⟨Cat.of (ComponentOver K), componentwiseTopology J K⟩)
    [HasSheafify S.totalTopology Ab.{u}]
    [HasSheafify (S.componentTopology n) Ab.{u}]
    [HasSheafify (componentwiseTopology J K) Ab.{u}]
    [HasExt.{w} (Sheaf S.totalTopology Ab.{u})]
    [HasExt.{w} (Sheaf (S.componentTopology n) Ab.{u})]
    [HasExt.{w} (Sheaf (componentwiseTopology J K) Ab.{u})]
    (i : K.I) (U : Over (K.obj i))
    [HasSheafify (J.over (K.obj i)) Ab.{u}]
    [HasExt.{w} (Sheaf (J.over (K.obj i)) Ab.{u})]
    (F : Sheaf S.totalTopology Ab.{u}) (p : ℕ) :
    let V : S.component n :=
      Eq.mp (congrArg (fun T : Σ D : Cat.{u, u}, GrothendieckTopology D =>
        (T.1 : Type u)) hsite.symm) (⟨i, U⟩ : ComponentOver K)
    let Fn : Sheaf (componentwiseTopology J K) Ab.{u} :=
      Eq.mp (congrArg (fun T : Σ D : Cat.{u, u}, GrothendieckTopology D =>
        Sheaf T.2 Ab.{u}) hsite)
        (((SimplicialSiteSituation.componentFunctor S n).sheafPullbackCocontinuous
          Ab.{u} (S.componentTopology n) S.totalTopology).obj F)
    Sheaf.H'.{w, u, u} F p ((SimplicialSiteSituation.componentFunctor S n).obj V) ≅
      Sheaf.H'.{w, u, u}
        (((formalCoproductSliceSheavesEquivalence J K Ab.{u}).val.functor.obj Fn) i) p U

Tag 0D9W, a remark

Tag 0D9W in the Stacks Project.

CategoryTheory.SemiRepresentable.Simplicial.totalRingedSite, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/SemiRepresentableRingedAugmentation.lean, line 183. The attribute's comment: “total_ringed_site”.

Stacks 0D9W, total ringed site. The total localization of a simplicial semi-representable object K of the underlying site of a ringed site X, equipped with the pulled-back structure sheaf a⁻¹O_C.

def totalRingedSite (X : AlgebraicGeometry.RingedSite.{u, v, w})
    (K : SimplicialObject (FormalCoproduct.{x} X.C)) : AlgebraicGeometry.RingedSite

CategoryTheory.SemiRepresentable.Simplicial.degreewiseRingedAugmentation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/SemiRepresentableRingedAugmentation.lean, line 272. The attribute's comment: “degreewise_ringed_augmentations”.

Stacks 0D9W, degreewise ringed augmentations. For a simplicial semi-representable object K of the underlying site of a ringed site X, each simplicial degree carries a morphism of ringed topoi a_n : (Sh(C/K_n), O_n) ⟶ (Sh(C), O_C) from the localization at the degree-n term to the ambient ringed topos.

def degreewiseRingedAugmentation (X : AlgebraicGeometry.RingedSite.{u, v, max x u v w})
    (K : SimplicialObject (FormalCoproduct.{x} X.C)) (n : SimplexCategory) :
    AlgebraicGeometry.RingedToposHom
      (AlgebraicGeometry.RingedSite.localizationRingedTopos X (K.obj (op n)))
      (AlgebraicGeometry.RingedSite.ringedTopos.{u, v, max x w} X)

CategoryTheory.SemiRepresentable.Simplicial.totalRingedAugmentation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/SemiRepresentableRingedAugmentation.lean, line 372. The attribute's comment: “ringed_augmentation”.

Stacks 0D9W, ringed augmentation. For a simplicial semi-representable object K of the underlying site of a ringed site X, the total ringed site is augmented over X by a morphism of ringed topoi a : (Sh((C/K)_total), O) ⟶ (Sh(C), O_C).

def totalRingedAugmentation (X : AlgebraicGeometry.RingedSite.{u, v, w})
    (K : SimplicialObject (FormalCoproduct.{x} X.C)) :
    AlgebraicGeometry.RingedToposHom
      (AlgebraicGeometry.RingedSite.ringedTopos.{max u v x, v, w}
        (totalRingedSite (AlgebraicGeometry.RingedSite.liftedRingedSite.{x, u, v, w} X) K))
      (AlgebraicGeometry.RingedSite.ringedTopos.{u, v, max x w}
        (AlgebraicGeometry.RingedSite.liftedRingedSite.{x, u, v, w} X))

CategoryTheory.SemiRepresentable.Simplicial.ringedTransitionMorphism_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/SemiRepresentableRingedAugmentation.lean, line 434. The attribute's comment: “flat_transition_morphisms”.

Stacks 0D9W, flat transition morphisms. For a simplicial semi-representable object K of the underlying site of a ringed site X, the morphism of ringed topoi attached to a simplex map φ : [m] ⟶ [n] is flat.

theorem ringedTransitionMorphism_isFlat
    (X : AlgebraicGeometry.RingedSite.{u, v, max x u v w})
    (K : SimplicialObject (FormalCoproduct.{x} X.C))
    {m n : SimplexCategory} (φ : m ⟶ n) :
    Stacks.Sheaf.RingedToposFlat.RingedToposHom.IsFlat.{max u v x, max u v x,
        max x u v w, max u v x, max u v x, max x u v w}
      (ringedTransitionMorphism.{x, u, v, w} X K φ).val

CategoryTheory.SemiRepresentable.Simplicial.degreewiseRingedAugmentation_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/SemiRepresentableRingedAugmentation.lean, line 497. The attribute's comment: “flat_degreewise_augmentations”.

Stacks 0D9W, flat degreewise augmentations. For a simplicial semi-representable object K of the underlying site of a ringed site X, the morphism of ringed topoi a_n : (Sh(C/K_n), O_n) ⟶ (Sh(C), O_C) is flat in every simplicial degree.

theorem degreewiseRingedAugmentation_isFlat
    (X : AlgebraicGeometry.RingedSite.{u, v, max x u v w})
    (K : SimplicialObject (FormalCoproduct.{x} X.C)) (n : SimplexCategory) :
    Stacks.Sheaf.RingedToposFlat.RingedToposHom.IsFlat.{max u v x, max u v x,
        max x u v w, v, u, max x u v w}
      (degreewiseRingedAugmentation.{x, u, v, w} X K n)

CategoryTheory.SemiRepresentable.Simplicial.totalRingedAugmentation_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/SemiRepresentableRingedAugmentation.lean, line 530. The attribute's comment: “flat_augmentation”.

Stacks 0D9W, flat augmentation. For a simplicial semi-representable object K of the underlying site of a ringed site X, the augmentation a : (Sh((C/K)_total), O) ⟶ (Sh(C), O_C) of the total ringed site is flat.

theorem totalRingedAugmentation_isFlat (X : AlgebraicGeometry.RingedSite.{u, v, w})
    (K : SimplicialObject (FormalCoproduct.{x} X.C)) :
    Stacks.Sheaf.RingedToposFlat.RingedToposHom.IsFlat.{v, max u v x,
        max x u v w, v, u, max x u v w}
      (totalRingedAugmentation.{x, u, v, w} X K)

CategoryTheory.SemiRepresentable.Simplicial.totalLowerShriekAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/SemiRepresentableRingedLowerShriek.lean, line 232. The attribute's comment: “lower_shriek”.

Stacks 0D9W, item (4). For a simplicial semi-representable object K of the underlying site of a ringed site X, the inverse image a^* of sheaves of modules along the augmentation of the total ringed site has a left adjoint a_! : Mod(O) ⥤ Mod(O_C).

def totalLowerShriekAdjunction :
    totalLowerShriek.{x, u, v, w} X K ⊣ totalInverseImageModules.{x, u, v, w} X K

CategoryTheory.SemiRepresentable.Simplicial.degreewiseLowerShriekAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/SemiRepresentableRingedLowerShriek.lean, line 270. The attribute's comment: “degreewise_lower_shriek_adjunction”.

Stacks 0D9W, the degreewise lower shriek. The inverse image a_n^* of sheaves of modules along the degreewise augmentation a_n : (Sh(C/K_n), O_n) ⟶ (Sh(C), O_C) has a left adjoint a_{n!} : Mod(O_n) ⥤ Mod(O_C).

Exactness of a_{n!}, which the source asserts as well, is CategoryTheory.SemiRepresentable.Simplicial.exactFunctor_degreewiseLowerShriek.

def degreewiseLowerShriekAdjunction :
    degreewiseLowerShriek.{x, u, v, w} X K n ⊣
      degreewiseInverseImageModules.{x, u, v, w} X K n

CategoryTheory.SemiRepresentable.Simplicial.exactFunctor_degreewiseLowerShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/SemiRepresentableRingedLowerShriek.lean, line 331. The attribute's comment: “degreewise_lower_shriek_exact”.

Stacks 0D9W, exactness of the degreewise lower shriek. The functor a_{n!} : Mod(O_n) ⥤ Mod(O_C) left adjoint to the inverse image a_n^* of the degreewise augmentation is exact.

Right exactness is formal, a_{n!} being a left adjoint. Left exactness is the direct-sum formula: the sections of a_{n!}G over V are the sum, over the pairs (i, V ⟶ K_{n,i}), of the sections of G at the corresponding object of the slice site, so a_{n!} is injective on sections as soon as G ⟶ G' is. That is the content of Stacks.Sites.ReducedLowerShriek.lowerShriek_exact at the reduction data CategoryTheory.SemiRepresentable.Simplicial.localizationReduction.

theorem exactFunctor_degreewiseLowerShriek :
    exactFunctor
      (SheafOfModules.{max x u v w} (Stacks.SheafOfModules.Tensor.ringSheaf
        (AlgebraicGeometry.RingedSite.localizationRingedTopos X (K.obj (op n))).O))
      (SheafOfModules.{max x u v w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
      (degreewiseLowerShriek.{x, u, v, w} X K n)

CategoryTheory.SemiRepresentable.Simplicial.transitionLowerShriekAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/SemiRepresentableRingedLowerShriek.lean, line 388. The attribute's comment: “transition_lower_shriek_adjunction”.

Stacks 0D9W, the lower shriek of a transition morphism. For a simplex map φ : [m] ⟶ [n], the inverse image f_φ^* of sheaves of modules along the transition morphism of ringed topoi f_φ : (Sh(C/K_n), O_n) ⟶ (Sh(C/K_m), O_m) has a left adjoint f_{φ!} : Mod(O_n) ⥤ Mod(O_m).

Exactness of f_{φ!}, which the source asserts as well, is CategoryTheory.SemiRepresentable.Simplicial.exactFunctor_transitionLowerShriek.

def transitionLowerShriekAdjunction (φ : m ⟶ n) :
    transitionLowerShriek.{x, u, v, w} X K φ ⊣ transitionInverseImageModules.{x, u, v, w} X K φ

CategoryTheory.SemiRepresentable.Simplicial.exactFunctor_transitionLowerShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/SemiRepresentableRingedLowerShriek.lean, line 525. The attribute's comment: “transition_lower_shriek_exact”.

Stacks 0D9W, exactness of the lower shriek of a transition morphism. For a simplex map φ : [m] ⟶ [n], the functor f_{φ!} : Mod(O_n) ⥤ Mod(O_m) left adjoint to the inverse image f_φ^* is exact.

Right exactness is formal, f_{φ!} being a left adjoint. Left exactness is the direct-sum formula: the sections of f_{φ!}G over an object W of the degree-m localization are the sum, over the components i of K_n and the arrows W.left ⟶ K_{n,i} under K(φ), of the sections of G at the corresponding object of the slice site.

theorem exactFunctor_transitionLowerShriek (φ : m ⟶ n) :
    exactFunctor
      (SheafOfModules.{max x u v w} (Stacks.SheafOfModules.inverseImageRing
        (componentwiseTopology X.J (K.obj (op n))) (componentwiseTopology X.J (K.obj (op m)))
        (⟨K.obj (op n), K.obj (op m), K.map φ.op⟩ :
          LocalizationSites.{x} X.C X.J).relocalizationFunctor
        (Stacks.SheafOfModules.Tensor.ringSheaf
          (AlgebraicGeometry.RingedSite.localizationRingedTopos X (K.obj (op m))).O)))
      (SheafOfModules.{max x u v w} (Stacks.SheafOfModules.Tensor.ringSheaf
        (AlgebraicGeometry.RingedSite.localizationRingedTopos X (K.obj (op m))).O))
      (transitionLowerShriek.{x, u, v, w} X K φ)

CategoryTheory.SemiRepresentable.Simplicial.componentRingedMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/SemiRepresentableRingedLowerShriek.lean, line 826. The attribute's comment: “component_morphism”.

Stacks 0D9W, the morphism of a simplicial degree into the total ringed site. For a simplicial semi-representable object K of the underlying site of a ringed site X, the degree-n componentwise localization is a ringed topos over the total ringed site by a morphism of ringed topoi g_n : (Sh(C/K_n), O_n) ⟶ (Sh((C/K)_total), O).

def componentRingedMorphism :
    AlgebraicGeometry.RingedToposHom (componentRingedTopos.{x, u, v, w} X K n)
      (AlgebraicGeometry.RingedSite.ringedTopos.{max u v x, v, w}
        (totalRingedSite.{x, u, v, max x u v w} X K))

CategoryTheory.SemiRepresentable.Simplicial.componentRingedMorphism_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/SemiRepresentableRingedLowerShriek.lean, line 845. The attribute's comment: “flat_component_morphism”.

Stacks 0D9W, flat component morphism. The morphism of ringed topoi g_n : (Sh(C/K_n), O_n) ⟶ (Sh((C/K)_total), O) is flat: its structure map in inverse-image form is the identification of g_n⁻¹O with O_n, hence an isomorphism, and an isomorphism of sheaves of commutative rings is flat.

theorem componentRingedMorphism_isFlat :
    Stacks.Sheaf.RingedToposFlat.RingedToposHom.IsFlat.{max x u v, max x u v,
        max x u v w, v, max u v x, max x u v w}
      (componentRingedMorphism.{x, u, v, w} X K n)

CategoryTheory.SemiRepresentable.Simplicial.componentLowerShriekAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/SemiRepresentableRingedLowerShriek.lean, line 881. The attribute's comment: “component_lower_shriek_adjunction”.

Stacks 0D9W, the lower shriek of a component morphism. The inverse image g_n^* of sheaves of modules along g_n has a left adjoint g_{n!} : Mod(O_n) ⥤ Mod(O).

Exactness of g_{n!}, which the source asserts as well, is CategoryTheory.SemiRepresentable.Simplicial.exactFunctor_componentLowerShriek.

def componentLowerShriekAdjunction :
    componentLowerShriek.{x, u, v, w} X K n ⊣ componentInverseImageModules.{x, u, v, w} X K n

CategoryTheory.SemiRepresentable.Simplicial.exactFunctor_componentLowerShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/SemiRepresentableRingedLowerShriek.lean, line 959. The attribute's comment: “component_lower_shriek_exact”.

Stacks 0D9W, exactness of the lower shriek of a component morphism. The functor g_{n!} : Mod(O_n) ⥤ Mod(O) left adjoint to the inverse image g_n^* is exact.

This is Stacks 0D74 for the Comma-category model of the total site: right exactness is formal, g_{n!} being a left adjoint, and left exactness is the direct-sum formula, whose index set at an object Z of the total site is componentFibre — a component of K_n, a simplex map Z.right ⟶ [n] and an arrow of the ambient site into that component. The simplex maps are the φ : [n] ⟶ [m] of the direct-sum formula of Tag 0D72. The flatness hypothesis of 0D74 is not needed here: the structure sheaf of the total site is pulled back from the ambient site, so it does not see the arrow along which a summand is taken.

theorem exactFunctor_componentLowerShriek :
    exactFunctor
      (SheafOfModules.{max x u v w} (Stacks.SheafOfModules.inverseImageRing
        (componentwiseTopology X.J (K.obj (op n))) (totalLocalizationTopology K X.J)
        (componentInclusion K n) (pulledBackRingSheaf X K)))
      (SheafOfModules.{max x u v w} (pulledBackRingSheaf X K))
      (componentLowerShriek.{x, u, v, w} X K n)

CategoryTheory.SemiRepresentable.Simplicial.pulledBackStructureSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/SemiRepresentableStructureSheaf.lean, line 258. The attribute's comment: “pulled_back_structure_sheaf”.

Stacks 0D9W, pulled-back structure sheaf. For the canonical localization augmentation attached to K, set O = a⁻¹ O_C. This is restriction along j_total, viewed as a sheaf valued in commutative rings.

def pulledBackStructureSheaf (X : AlgebraicGeometry.RingedSite.{u, v, w})
    (K : SimplicialObject (FormalCoproduct.{x} X.C)) :
    Sheaf (totalLocalizationTopology K X.J) CommRingCat.{w}

Tag 0D9X, a remark

Tag 0D9X in the Stacks Project.

CategoryTheory.SemiRepresentable.Simplicial.totalRingedSiteOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/SemiRepresentable/RingedOverObject.lean, line 142. The attribute's comment: “item (1): the ringed site ((C/K)_total, O)”.

For a ringed site (C, O_C), an object U of C and a simplicial object K of SR(C, U) = SR(C/U), the total localization site (C/K)_total of K over the slice site C/U, with the structure sheaf O = a⁻¹O_U pulled back from O_U = O_C|_{C/U}.

abbrev totalRingedSiteOver : AlgebraicGeometry.RingedSite

CategoryTheory.SemiRepresentable.Simplicial.totalRingedAugmentationOver, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/SemiRepresentable/RingedOverObject.lean, line 156. The attribute's comment: “item (2): the morphism of ringed topoi a”.

The augmentation a : (Sh((C/K)_total), O) ⟶ (Sh(C/U), O_U) of the total ringed site of a simplicial object K of SR(C, U), as a morphism of ringed topoi.

def totalRingedAugmentationOver :
    AlgebraicGeometry.RingedToposHom
      (AlgebraicGeometry.RingedSite.ringedTopos.{max u v x, v, w}
        (totalRingedSite (AlgebraicGeometry.RingedSite.liftedRingedSite.{x} (X.over U)) K))
      (AlgebraicGeometry.RingedSite.ringedTopos.{max u v, v, max x w}
        (AlgebraicGeometry.RingedSite.liftedRingedSite.{x} (X.over U)))

CategoryTheory.SemiRepresentable.Simplicial.degreewiseRingedAugmentationOver, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/SemiRepresentable/RingedOverObject.lean, line 175. The attribute's comment: “item (3): the morphisms of ringed topoi a_n”.

The degreewise augmentations a_n : (Sh(C/K_n), O_n) ⟶ (Sh(C/U), O_U) of a simplicial object K of SR(C, U), as morphisms of ringed topoi.

def degreewiseRingedAugmentationOver (n : SimplexCategory) :
    AlgebraicGeometry.RingedToposHom
      (AlgebraicGeometry.RingedSite.localizationRingedTopos
        (AlgebraicGeometry.RingedSite.liftedRingedSite.{x} (X.over U)) (K.obj (op n)))
      (AlgebraicGeometry.RingedSite.ringedTopos.{max u v, v, max x w}
        (AlgebraicGeometry.RingedSite.liftedRingedSite.{x} (X.over U)))

CategoryTheory.SemiRepresentable.Simplicial.totalLowerShriekOverAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/SemiRepresentable/RingedOverObject.lean, line 198. The attribute's comment: “item (4): a_! is left adjoint to a^*”.

For a simplicial object K of SR(C, U), the functor a_! : Mod(O) ⥤ Mod(O_U) is left adjoint to the pullback a^* of sheaves of modules along the augmentation a : (Sh((C/K)_total), O) ⟶ (Sh(C/U), O_U).

def totalLowerShriekOverAdjunction :
    totalLowerShriekOver.{x, u, v, w} X U K ⊣
      (totalRingedAugmentationOver.{x, u, v, w} X U K).toModulesHom.pullbackModules

CategoryTheory.SemiRepresentable.Simplicial.totalRingedAugmentationOver_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/SemiRepresentable/RingedOverObject.lean, line 208. The attribute's comment: “the results of 0D9W: a is flat”.

The augmentation a : (Sh((C/K)_total), O) ⟶ (Sh(C/U), O_U) of a simplicial object K of SR(C, U) is flat.

theorem totalRingedAugmentationOver_isFlat :
    Stacks.Sheaf.RingedToposFlat.RingedToposHom.IsFlat.{v, max u v x,
        max x u v w, v, max u v, max x u v w}
      (totalRingedAugmentationOver.{x, u, v, w} X U K)

CategoryTheory.SemiRepresentable.Simplicial.degreewiseRingedAugmentationOver_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/SemiRepresentable/RingedOverObject.lean, line 217. The attribute's comment: “the results of 0D9W: a_n is flat”.

Every degreewise augmentation a_n : (Sh(C/K_n), O_n) ⟶ (Sh(C/U), O_U) of a simplicial object K of SR(C, U) is flat.

theorem degreewiseRingedAugmentationOver_isFlat (n : SimplexCategory) :
    Stacks.Sheaf.RingedToposFlat.RingedToposHom.IsFlat.{max u v x, max u v x,
        max x u v w, v, max u v, max x u v w}
      (degreewiseRingedAugmentationOver.{x, u, v, w} X U K n)

CategoryTheory.SemiRepresentable.Simplicial.degreewiseLowerShriekOverAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/SemiRepresentable/RingedOverObject.lean, line 228. The attribute's comment: “the results of 0D9W: a_{n!} is left adjoint to a_n^*”.

For a simplicial object K of SR(C, U), the inverse image a_n^* of sheaves of modules along the degreewise augmentation a_n : (Sh(C/K_n), O_n) ⟶ (Sh(C/U), O_U) has the left adjoint a_{n!} : Mod(O_n) ⥤ Mod(O_U).

def degreewiseLowerShriekOverAdjunction (n : SimplexCategory) :
    degreewiseLowerShriek.{x, max u v, v, w}
        (AlgebraicGeometry.RingedSite.liftedRingedSite.{x} (X.over U)) K n ⊣
      degreewiseInverseImageModules.{x, max u v, v, w}
        (AlgebraicGeometry.RingedSite.liftedRingedSite.{x} (X.over U)) K n

CategoryTheory.SemiRepresentable.Simplicial.exactFunctor_degreewiseLowerShriekOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/SemiRepresentable/RingedOverObject.lean, line 239. The attribute's comment: “the results of 0D9W: a_{n!} is exact”.

For a simplicial object K of SR(C, U), the functor a_{n!} : Mod(O_n) ⥤ Mod(O_U) is exact.

theorem exactFunctor_degreewiseLowerShriekOver (n : SimplexCategory) :
    exactFunctor _ _ (degreewiseLowerShriek.{x, max u v, v, w}
      (AlgebraicGeometry.RingedSite.liftedRingedSite.{x} (X.over U)) K n)

CategoryTheory.SemiRepresentable.Simplicial.ringedTransitionMorphismOver_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/SemiRepresentable/RingedOverObject.lean, line 248. The attribute's comment: “the results of 0D9W: f_φ is flat”.

For a simplicial object K of SR(C, U) and a simplex map φ : [m] ⟶ [n], the morphism of ringed topoi f_φ : (Sh(C/K_n), O_n) ⟶ (Sh(C/K_m), O_m) is flat.

theorem ringedTransitionMorphismOver_isFlat {m n : SimplexCategory} (φ : m ⟶ n) :
    Stacks.Sheaf.RingedToposFlat.RingedToposHom.IsFlat.{max u v x, max u v x,
        max x u v w, max u v x, max u v x, max x u v w}
      (ringedTransitionMorphism.{x, max u v, v, w}
        (AlgebraicGeometry.RingedSite.liftedRingedSite.{x} (X.over U)) K φ).val

CategoryTheory.SemiRepresentable.Simplicial.transitionLowerShriekOverAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/SemiRepresentable/RingedOverObject.lean, line 259. The attribute's comment: “the results of 0D9W: f_{φ!} is left adjoint to f_φ^*”.

For a simplicial object K of SR(C, U) and a simplex map φ : [m] ⟶ [n], the inverse image f_φ^* of sheaves of modules has the left adjoint f_{φ!} : Mod(O_n) ⥤ Mod(O_m).

def transitionLowerShriekOverAdjunction {m n : SimplexCategory} (φ : m ⟶ n) :
    transitionLowerShriek.{x, max u v, v, w}
        (AlgebraicGeometry.RingedSite.liftedRingedSite.{x} (X.over U)) K φ ⊣
      transitionInverseImageModules.{x, max u v, v, w}
        (AlgebraicGeometry.RingedSite.liftedRingedSite.{x} (X.over U)) K φ

CategoryTheory.SemiRepresentable.Simplicial.exactFunctor_transitionLowerShriekOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/SemiRepresentable/RingedOverObject.lean, line 270. The attribute's comment: “the results of 0D9W: f_{φ!} is exact”.

For a simplicial object K of SR(C, U) and a simplex map φ : [m] ⟶ [n], the functor f_{φ!} : Mod(O_n) ⥤ Mod(O_m) is exact.

theorem exactFunctor_transitionLowerShriekOver {m n : SimplexCategory} (φ : m ⟶ n) :
    exactFunctor _ _ (transitionLowerShriek.{x, max u v, v, w}
      (AlgebraicGeometry.RingedSite.liftedRingedSite.{x} (X.over U)) K φ)

CategoryTheory.SemiRepresentable.Simplicial.componentRingedMorphismOver_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/SemiRepresentable/RingedOverObject.lean, line 279. The attribute's comment: “the results of 0D9W: g_n is flat”.

For a simplicial object K of SR(C, U), the morphism of ringed topoi g_n : (Sh(C/K_n), O_n) ⟶ (Sh((C/K)_total), O) is flat.

theorem componentRingedMorphismOver_isFlat (n : SimplexCategory) :
    Stacks.Sheaf.RingedToposFlat.RingedToposHom.IsFlat.{max x u v, max x u v,
        max x u v w, v, max u v x, max x u v w}
      (componentRingedMorphism.{x, max u v, v, w}
        (AlgebraicGeometry.RingedSite.liftedRingedSite.{x} (X.over U)) K n)

CategoryTheory.SemiRepresentable.Simplicial.componentLowerShriekOverAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/SemiRepresentable/RingedOverObject.lean, line 290. The attribute's comment: “the results of 0D9W: g_{n!} is left adjoint to g_n^*”.

For a simplicial object K of SR(C, U), the inverse image g_n^* of sheaves of modules along g_n has the left adjoint g_{n!} : Mod(O_n) ⥤ Mod(O).

def componentLowerShriekOverAdjunction (n : SimplexCategory) :
    componentLowerShriek.{x, max u v, v, w}
        (AlgebraicGeometry.RingedSite.liftedRingedSite.{x} (X.over U)) K n ⊣
      componentInverseImageModules.{x, max u v, v, w}
        (AlgebraicGeometry.RingedSite.liftedRingedSite.{x} (X.over U)) K n

CategoryTheory.SemiRepresentable.Simplicial.exactFunctor_componentLowerShriekOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/SemiRepresentable/RingedOverObject.lean, line 301. The attribute's comment: “the results of 0D9W: g_{n!} is exact”.

For a simplicial object K of SR(C, U), the functor g_{n!} : Mod(O_n) ⥤ Mod(O) is exact.

theorem exactFunctor_componentLowerShriekOver (n : SimplexCategory) :
    exactFunctor _ _ (componentLowerShriek.{x, max u v, v, w}
      (AlgebraicGeometry.RingedSite.liftedRingedSite.{x} (X.over U)) K n)

AlgebraicGeometry.SemiRepresentable.Simplicial.totalRingedSite, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/SemiRepresentable/TotalRingedSite.lean, line 89. The attribute's comment: “ringed_total_site”.

The total localization of a simplicial semi-representable object over a ringed site, together with its pulled-back structure sheaf, is a ringed site.

def totalRingedSite (X : AlgebraicGeometry.RingedSite.{u, v, w})
    (K : SimplicialObject (FormalCoproduct.{x} X.C)) : AlgebraicGeometry.RingedSite

AlgebraicGeometry.SemiRepresentable.Simplicial.ringedAugmentation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/SemiRepresentable/TotalRingedSite.lean, line 140. The attribute's comment: “ringed_augmentation”.

The total localization of a simplicial semi-representable object over a ringed site has a canonical augmentation to the base as a morphism of ringed topoi.

def ringedAugmentation (X : AlgebraicGeometry.RingedSite.{u, v, w})
    (K : SimplicialObject (FormalCoproduct.{x} X.C)) :
    AlgebraicGeometry.RingedToposHom
      (AlgebraicGeometry.RingedSite.ringedTopos.{max x u v, v, w}
        (totalRingedSite.{x, v, u, max x u v w} (liftedRingedSite.{x, v, u, w} X) K))
      (AlgebraicGeometry.RingedSite.ringedTopos.{u, v, max x w}
        (liftedRingedSite.{x, v, u, w} X))

CategoryTheory.SemiRepresentable.Simplicial.totalRingedSite, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/SemiRepresentableRingedAugmentation.lean, line 183. The attribute's comment: “ringed_total_site”.

Stacks 0D9W, total ringed site. The total localization of a simplicial semi-representable object K of the underlying site of a ringed site X, equipped with the pulled-back structure sheaf a⁻¹O_C.

def totalRingedSite (X : AlgebraicGeometry.RingedSite.{u, v, w})
    (K : SimplicialObject (FormalCoproduct.{x} X.C)) : AlgebraicGeometry.RingedSite

Sources

Section85.17 Cohomological descent for hypercoverings #

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

Tag 0D8E, a lemma

Tag 0D8E in the Stacks Project.

CategoryTheory.SimplicialSemiRepresentable.faithful_situationTotalInverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringDegreeZeroFaithful.lean, line 86. The attribute's comment: “part (1): a^{-1} of Stacks 0D70 on sheaves of sets is faithful, for the simplicial-site situation attached to a hypercovering”.

Stacks 0D8E (1), the faithfulness half, for the inverse image of the total augmentation as Stacks 0D70 constructs it from the simplicial-site situation of a hypercovering: that inverse image is faithful.

theorem faithful_situationTotalInverseImage :
    (SimplicialSiteSituation.Augmentation.totalMorphismOfTopoi
      (situation P.toGrothendieck H.toSimplicialObject) (Cat.of C) P.toGrothendieck
      (situationAugmentation P.toGrothendieck H.toSimplicialObject)).inverseImage.Faithful

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

Stacks 0D8E (1), the faithfulness half. For a hypercovering K the inverse image a^{-1} : Sh(C) ⥤ 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 [HasEqualizers C] [HasPullbacks C] (P : Pretopology C)
    (H : HypercoveringOfTerminal.{u, u, u} P) :
    (totalLocalizationMorphism P.toGrothendieck H.toSimplicialObject).inverseImage.Faithful

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

Stacks 0D8E (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 [HasEqualizers C] [HasPullbacks C] (P : Pretopology C)
    (H : HypercoveringOfTerminal.{u, u, u} P) :
    Functor.Faithful
      (augmentation P.toGrothendieck H.toSimplicialObject).totalMorphismOfTopoi.inverseImage

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

Stacks 0D8E (2), the faithfulness half. For a hypercovering K the inverse image a^{-1} : Ab(C) ⥤ 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 applies at any coefficient category.

theorem faithful_abelianInverseImage [HasEqualizers C] [HasPullbacks C] (P : Pretopology C)
    (H : HypercoveringOfTerminal.{u, u, u} P) :
    ((totalForget H.toSimplicialObject).sheafPushforwardContinuous Ab.{u}
      ((situation P.toGrothendieck H.toSimplicialObject).totalTopology)
      P.toGrothendieck).Faithful

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

Stacks 0D8E (1), the inclusion of the essential image in the cartesian sheaves. Every sheaf of sets on the total site isomorphic to an inverse image along the augmentation 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 {F : Sheaf (situation J K).totalTopology (Type u)}
    (hF : (totalLocalizationMorphism J K).inverseImage.essImage F) :
    (situation J K).IsCartesianSheaf F

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

Stacks 0D8E (2), the inclusion of the essential image in the cartesian sheaves. Every sheaf of abelian groups on the total site isomorphic to an inverse image along the augmentation 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. So the abelian statement follows from the statement for sheaves of sets applied to the underlying sheaf.

theorem isCartesianAbSheaf_of_mem_essImage {F : Sheaf (situation J K).totalTopology Ab.{u}}
    (hF : ((totalForget K).sheafPushforwardContinuous Ab.{u}
      ((situation J K).totalTopology) J).essImage F) :
    (situation J K).IsCartesianAbSheaf F

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

Stacks 0D8E (1), fullness, carrying local fullness of j_total.

For a hypercovering K the inverse image a^{-1} : Sh(C) ⥤ Sh((C/K)_total) of the augmentation is full as soon as the localization functor j_total is locally full for the topology of C. That local fullness — unwound at two objects of the total site, the local existence of a simplex of K carrying two prescribed charts on two of its faces — is the input the degree-zero condition does not supply, and it is carried here as a hypothesis.

theorem full_inverseImage
    (hlf : (totalForget H.toSimplicialObject).IsLocallyFull P.toGrothendieck) :
    (totalLocalizationMorphism P.toGrothendieck H.toSimplicialObject).inverseImage.Full

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

Stacks 0D8E (1), full faithfulness, carrying local fullness of j_total.

def fullyFaithfulInverseImageHypercovering
    (hlf : (totalForget H.toSimplicialObject).IsLocallyFull P.toGrothendieck) :
    (totalLocalizationMorphism P.toGrothendieck
      H.toSimplicialObject).inverseImage.FullyFaithful

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

Stacks 0D8E (1), the unit is invertible, carrying local fullness of j_total: for every sheaf of sets E on C the canonical map E ⟶ a_* a^{-1} E is an isomorphism. This is the half of "a_* is a quasi-inverse" that holds on all of Sh(C).

theorem isIso_unit_hypercovering
    (hlf : (totalForget H.toSimplicialObject).IsLocallyFull P.toGrothendieck) :
    IsIso (totalLocalizationMorphism P.toGrothendieck H.toSimplicialObject).adj.unit

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

Stacks 0D8E (1), the essential image is exactly the cartesian sheaves, carrying essential surjectivity onto them. One inclusion is isCartesianSheaf_of_mem_essImage; the other is the clause the degree-zero condition does not supply, and it is carried as a hypothesis.

theorem mem_essImage_iff_isCartesianSheaf
    (hsurj : ∀ G : Sheaf (situation P.toGrothendieck H.toSimplicialObject).totalTopology
        (Type u),
      (situation P.toGrothendieck H.toSimplicialObject).IsCartesianSheaf G →
        (totalLocalizationMorphism P.toGrothendieck
          H.toSimplicialObject).inverseImage.essImage G)
    (F : Sheaf (situation P.toGrothendieck H.toSimplicialObject).totalTopology (Type u)) :
    (totalLocalizationMorphism P.toGrothendieck
        H.toSimplicialObject).inverseImage.essImage F ↔
      (situation P.toGrothendieck H.toSimplicialObject).IsCartesianSheaf F

CategoryTheory.SimplicialSemiRepresentable.isIso_counit_app_hypercovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringDescent.lean, line 513. The attribute's comment: “part (1): a^{-1} a_* F = F for cartesian F, carrying both remaining clauses”.

Stacks 0D8E (1), the counit is invertible on cartesian sheaves, carrying both of the two clauses: for a cartesian sheaf of sets F on the total site the canonical map a^{-1} a_* F ⟶ F is an isomorphism. This is the half of "a_* is a quasi-inverse" that holds on the cartesian sheaves; the two carried hypotheses supply full faithfulness of a^{-1} and membership of F in its essential image.

theorem isIso_counit_app_hypercovering
    (hlf : (totalForget H.toSimplicialObject).IsLocallyFull P.toGrothendieck)
    (hsurj : ∀ G : Sheaf (situation P.toGrothendieck H.toSimplicialObject).totalTopology
        (Type u),
      (situation P.toGrothendieck H.toSimplicialObject).IsCartesianSheaf G →
        (totalLocalizationMorphism P.toGrothendieck
          H.toSimplicialObject).inverseImage.essImage G)
    {F : Sheaf (situation P.toGrothendieck H.toSimplicialObject).totalTopology (Type u)}
    (hF : (situation P.toGrothendieck H.toSimplicialObject).IsCartesianSheaf F) :
    IsIso ((totalLocalizationMorphism P.toGrothendieck
      H.toSimplicialObject).adj.counit.app F)

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

Stacks 0D8E (2), fullness, carrying local fullness of j_total. Local fullness is a condition on the site, so the same input serves at abelian coefficients.

theorem full_abelianInverseImage
    (hlf : (totalForget H.toSimplicialObject).IsLocallyFull P.toGrothendieck) :
    ((totalForget H.toSimplicialObject).sheafPushforwardContinuous Ab.{u}
      ((situation P.toGrothendieck H.toSimplicialObject).totalTopology)
      P.toGrothendieck).Full

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

Stacks 0D8E (2), full faithfulness, carrying local fullness of j_total.

def fullyFaithfulAbelianInverseImageHypercovering
    (hlf : (totalForget H.toSimplicialObject).IsLocallyFull P.toGrothendieck) :
    ((totalForget H.toSimplicialObject).sheafPushforwardContinuous Ab.{u}
      ((situation P.toGrothendieck H.toSimplicialObject).totalTopology)
      P.toGrothendieck).FullyFaithful

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

Stacks 0D8E (2), the unit is invertible, carrying local fullness of j_total: for every sheaf of abelian groups E on C the canonical map E ⟶ a_* a^{-1} E is an isomorphism.

theorem isIso_abelianUnit_hypercovering
    (hlf : (totalForget H.toSimplicialObject).IsLocallyFull P.toGrothendieck) :
    IsIso (abelianTotalAdjunction P.toGrothendieck H.toSimplicialObject).unit

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

Stacks 0D8E (2), the essential image is exactly the cartesian abelian sheaves, carrying essential surjectivity onto them.

theorem mem_essImage_iff_isCartesianAbSheaf
    (hsurj : ∀ G : Sheaf (situation P.toGrothendieck H.toSimplicialObject).totalTopology Ab.{u},
      (situation P.toGrothendieck H.toSimplicialObject).IsCartesianAbSheaf G →
        ((totalForget H.toSimplicialObject).sheafPushforwardContinuous Ab.{u}
          ((situation P.toGrothendieck H.toSimplicialObject).totalTopology)
          P.toGrothendieck).essImage G)
    (F : Sheaf (situation P.toGrothendieck H.toSimplicialObject).totalTopology Ab.{u}) :
    ((totalForget H.toSimplicialObject).sheafPushforwardContinuous Ab.{u}
        ((situation P.toGrothendieck H.toSimplicialObject).totalTopology)
        P.toGrothendieck).essImage F ↔
      (situation P.toGrothendieck H.toSimplicialObject).IsCartesianAbSheaf F

CategoryTheory.SimplicialSemiRepresentable.isIso_abelianCounit_app_hypercovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringDescent.lean, line 577. The attribute's comment: “part (2): a^{-1} a_* F = F for cartesian F, carrying both remaining clauses”.

Stacks 0D8E (2), the counit is invertible on cartesian abelian sheaves, carrying both of the two clauses: for a cartesian sheaf of abelian groups F on the total site the canonical map a^{-1} a_* F ⟶ F is an isomorphism.

theorem isIso_abelianCounit_app_hypercovering
    (hlf : (totalForget H.toSimplicialObject).IsLocallyFull P.toGrothendieck)
    (hsurj : ∀ G : Sheaf (situation P.toGrothendieck H.toSimplicialObject).totalTopology Ab.{u},
      (situation P.toGrothendieck H.toSimplicialObject).IsCartesianAbSheaf G →
        ((totalForget H.toSimplicialObject).sheafPushforwardContinuous Ab.{u}
          ((situation P.toGrothendieck H.toSimplicialObject).totalTopology)
          P.toGrothendieck).essImage G)
    {F : Sheaf (situation P.toGrothendieck H.toSimplicialObject).totalTopology Ab.{u}}
    (hF : (situation P.toGrothendieck H.toSimplicialObject).IsCartesianAbSheaf F) :
    IsIso ((abelianTotalAdjunction P.toGrothendieck
      H.toSimplicialObject).counit.app F)

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

Stacks 0D8E (1), the essential image is exactly the cartesian sheaves of sets. A sheaf of sets on the total site of a hypercovering of the final presheaf lies in the essential image of restriction along the localization functor j_total if and only if it is cartesian.

theorem mem_essImage_iff_isCartesianSheaf' (P : Pretopology C)
    (H : HypercoveringOfTerminal.{u, u, u} P)
    (E : Sheaf (situation P.toGrothendieck H.toSimplicialObject).totalTopology (Type u)) :
    (totalLocalizationMorphism P.toGrothendieck
        H.toSimplicialObject).inverseImage.essImage E ↔
      (situation P.toGrothendieck H.toSimplicialObject).IsCartesianSheaf E

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

Stacks 0D8E (1), a⁻¹ a_* F = F for cartesian F. For a cartesian sheaf of sets E on the total site of a hypercovering of the final presheaf, the counit a⁻¹ a_* E ⟶ E is an isomorphism.

theorem isIso_counit_app_hypercovering' (P : Pretopology C)
    (H : HypercoveringOfTerminal.{u, u, u} P)
    (E : Sheaf (situation P.toGrothendieck H.toSimplicialObject).totalTopology (Type u))
    (hE : (situation P.toGrothendieck H.toSimplicialObject).IsCartesianSheaf E) :
    IsIso ((totalLocalizationMorphism P.toGrothendieck
      H.toSimplicialObject).adj.counit.app E)

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

Stacks 0D8E (2), the essential image is exactly the cartesian abelian sheaves. One inclusion is isCartesianAbSheaf_of_mem_essImage, the other is essImage_of_isCartesianAbSheaf.

theorem mem_essImage_iff_isCartesianAbSheaf' (P : Pretopology C)
    (H : HypercoveringOfTerminal.{u, u, u} P)
    (G : Sheaf (situation P.toGrothendieck H.toSimplicialObject).totalTopology Ab.{u}) :
    ((totalForget H.toSimplicialObject).sheafPushforwardContinuous Ab.{u}
        ((situation P.toGrothendieck H.toSimplicialObject).totalTopology)
        P.toGrothendieck).essImage G ↔
      (situation P.toGrothendieck H.toSimplicialObject).IsCartesianAbSheaf G

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

Stacks 0D8E (2), a⁻¹ a_* F = F for cartesian F. For a cartesian sheaf of abelian groups F on the total site the canonical map a⁻¹ a_* F ⟶ F is an isomorphism. This is the half of "a_* is a quasi-inverse" that holds on the cartesian abelian sheaves: a⁻¹ is fully faithful, so its counit is invertible exactly on its essential image, and essImage_of_isCartesianAbSheaf puts F there.

theorem isIso_abelianCounit_app_hypercovering' (P : Pretopology C)
    (H : HypercoveringOfTerminal.{u, u, u} P)
    (G : Sheaf (situation P.toGrothendieck H.toSimplicialObject).totalTopology Ab.{u})
    (hG : (situation P.toGrothendieck H.toSimplicialObject).IsCartesianAbSheaf G) :
    IsIso ((abelianTotalAdjunction P.toGrothendieck
      H.toSimplicialObject).counit.app G)

CategoryTheory.SimplicialSemiRepresentable.essImage_situationTotalInverseImage_of_isCartesianSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringSituationDescent.lean, line 106. 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”.

Stacks 0D8E (1), essential surjectivity onto the cartesian sheaves of sets, for the inverse image of the morphism of topoi which Stacks 0D70 attaches to the augmentation of the simplicial-site situation of a hypercovering.

By Stacks 0D8B that inverse image is restriction along j_total, for which every cartesian sheaf of sets is an inverse image by CategoryTheory.SimplicialSemiRepresentable.essImage_of_isCartesianSheaf.

theorem essImage_situationTotalInverseImage_of_isCartesianSheaf
    (E : Sheaf (situation P.toGrothendieck H.toSimplicialObject).totalTopology (Type u))
    (hE : (situation P.toGrothendieck H.toSimplicialObject).IsCartesianSheaf E) :
    (Augmentation.totalMorphismOfTopoi
      (situation P.toGrothendieck H.toSimplicialObject) (Cat.of C) P.toGrothendieck
      (situationAugmentation P.toGrothendieck H.toSimplicialObject)).inverseImage.essImage E

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

Stacks 0D8E (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. One inclusion is mem_essImage_iff_isCartesianSheaf' carried across Stacks 0D8B, the other is essImage_situationTotalInverseImage_of_isCartesianSheaf.

theorem mem_essImage_situationTotalInverseImage_iff_isCartesianSheaf
    (E : Sheaf (situation P.toGrothendieck H.toSimplicialObject).totalTopology (Type u)) :
    (Augmentation.totalMorphismOfTopoi
        (situation P.toGrothendieck H.toSimplicialObject) (Cat.of C) P.toGrothendieck
        (situationAugmentation P.toGrothendieck H.toSimplicialObject)).inverseImage.essImage E ↔
      (situation P.toGrothendieck H.toSimplicialObject).IsCartesianSheaf E

CategoryTheory.SimplicialSemiRepresentable.essImage_situationTotalInverseImageAb_of_isCartesianAbSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringSituationDescentAb.lean, line 140. 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”.

Every cartesian abelian sheaf on the total site lies in the essential image of the abelian inverse image of the morphism of topoi which Stacks 0D70 attaches to the augmentation of the simplicial-site situation of a hypercovering.

theorem essImage_situationTotalInverseImageAb_of_isCartesianAbSheaf (P : Pretopology C)
    (H : HypercoveringOfTerminal.{u, u, u} P)
    (G : Sheaf (situation P.toGrothendieck H.toSimplicialObject).totalTopology Ab.{u})
    (hG : (situation P.toGrothendieck H.toSimplicialObject).IsCartesianAbSheaf G) :
    (Augmentation.totalInverseImageAb (situation P.toGrothendieck H.toSimplicialObject)
      (Cat.of C) P.toGrothendieck
      (situationAugmentation P.toGrothendieck H.toSimplicialObject)).essImage G

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

The essential image of the abelian inverse image of the morphism of topoi of Stacks 0D70 at the simplicial-site situation of a hypercovering is exactly the cartesian abelian sheaves.

theorem mem_essImage_situationTotalInverseImageAb_iff_isCartesianAbSheaf (P : Pretopology C)
    (H : HypercoveringOfTerminal.{u, u, u} P)
    (G : Sheaf (situation P.toGrothendieck H.toSimplicialObject).totalTopology Ab.{u}) :
    (Augmentation.totalInverseImageAb (situation P.toGrothendieck H.toSimplicialObject)
        (Cat.of C) P.toGrothendieck
        (situationAugmentation P.toGrothendieck H.toSimplicialObject)).essImage G ↔
      (situation P.toGrothendieck H.toSimplicialObject).IsCartesianAbSheaf G

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

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

The localization functor j_total is cover dense by isCoverDense_totalForget and locally full by isLocallyFull_totalForget, and restriction along a continuous functor which is both is full.

theorem full_inverseImage' :
    (totalLocalizationMorphism P.toGrothendieck H.toSimplicialObject).inverseImage.Full

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

Stacks 0D8E (1), full faithfulness. For a hypercovering K the inverse image a^{-1} : Sh(C) ⥤ Sh((C/K)_total) of the augmentation is fully faithful: it is faithful by faithful_inverseImage_of_isCoverDense and full by full_inverseImage'.

def fullyFaithfulInverseImageHypercovering' :
    (totalLocalizationMorphism P.toGrothendieck
      H.toSimplicialObject).inverseImage.FullyFaithful

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

Stacks 0D8E (1), E = a_* a^{-1} E. For every sheaf of sets E on C the canonical map E ⟶ a_* a^{-1} E is an isomorphism, a^{-1} being restriction along j_total. This is the half of "a_* is a quasi-inverse" that holds on all of Sh(C): the unit of an adjunction with fully faithful left adjoint is invertible.

theorem isIso_unit_hypercovering' :
    IsIso (totalLocalizationMorphism P.toGrothendieck H.toSimplicialObject).adj.unit

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

Stacks 0D8E (2), fullness. For a hypercovering K the inverse image a^{-1} : Ab(C) ⥤ Ab((C/K)_total) of the augmentation is full. Cover density and local fullness of j_total are conditions on the site, so the same input serves at abelian coefficients.

theorem full_abelianInverseImage' :
    ((totalForget H.toSimplicialObject).sheafPushforwardContinuous Ab.{u}
      ((situation P.toGrothendieck H.toSimplicialObject).totalTopology)
      P.toGrothendieck).Full

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

Stacks 0D8E (2), full faithfulness. For a hypercovering K the inverse image a^{-1} : Ab(C) ⥤ Ab((C/K)_total) of the augmentation is fully faithful.

def fullyFaithfulAbelianInverseImageHypercovering' :
    ((totalForget H.toSimplicialObject).sheafPushforwardContinuous Ab.{u}
      ((situation P.toGrothendieck H.toSimplicialObject).totalTopology)
      P.toGrothendieck).FullyFaithful

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

Stacks 0D8E (2), E = a_* a^{-1} E. For every sheaf of abelian groups E on C the canonical map E ⟶ a_* a^{-1} E is an isomorphism, a^{-1} being restriction along j_total.

theorem isIso_abelianUnit_hypercovering' :
    IsIso (abelianTotalAdjunction P.toGrothendieck H.toSimplicialObject).unit

Tag 0D8F, a lemma

Tag 0D8F in the Stacks Project.

CategoryTheory.SimplicialSemiRepresentable.cechComplexIsoSheafHomComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringForkVertexCosimplicial.lean, line 442.

Stacks 0D8F. The Čech complex of Stacks 0D79 associated to a⁻¹F,

a_{0,*}a_0⁻¹F ⟶ a_{1,*}a_1⁻¹F ⟶ a_{2,*}a_2⁻¹F ⟶ …

is canonically isomorphic — the source says equal, and the comparison is indeed the identity in every degree once the terms are identified — to the cochain complex SheafHom(s(ℤ_{F(K)}^#), F) obtained by applying the abelian internal hom ℋom(-, F) to the complex of free abelian sheaves of Stacks 01GB.

The differentials of both complexes are the alternating sums induced by the simplicial structure of K, so a cosimplicial identification of the terms suffices; that is the whole of the source's argument. The identification of the terms itself, a_{n,*}a_n⁻¹F = ℋom'(F(K_n)^#, F) = ℋom(ℤ_{F(K_n)}^#, F), is cechCosimplicialObjectIsoSheafHomCosimplicialObject.

def cechComplexIsoSheafHomComplex (F : Sheaf J AddCommGrpCat.{u}) :
    cechComplex J K F ≅ sheafHomComplex J K F

Tag 0D8G, a lemma

Tag 0D8G in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.isIso_derivedAugmentationUnit_app_of_hypercovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringCohomologicalDescent.lean, line 465. The attribute's comment: “granted Tag 0D8E and the Ra_*-acyclicity of a⁻¹ of a K-injective complex”.

Stacks 0D8G, granted the two inputs the library does not have. For a site C with equalizers and fibre products, a hypercovering K of it, and the augmentation a : Sh((C/K)_total) ⟶ Sh(C) of Stacks 0D8B, the canonical map E ⟶ R a_* a⁻¹ E is an isomorphism for every object E of the unbounded derived category of abelian sheaves on C.

E is arbitrary: no boundedness is assumed, and the coefficients are the full category of abelian sheaves.

The two hypotheses are the inputs discussed in the module docstring. hunit is Stacks 0D8E in its abelian form, that the underived unit F ⟶ a_*a⁻¹F is an isomorphism. hacyclic says that a⁻¹ of a K-injective complex of abelian sheaves on C computes R a_*; it is the derived content of the source's computation of R a_*a⁻¹ by the Čech complex, which rests on the spectral sequence of Stacks 0D7A and the product total complex. Neither hypothesis is used by the construction of a⁻¹, of R a_*, of their adjunction or of its unit.

theorem isIso_derivedAugmentationUnit_app_of_hypercovering
    (hunit : IsIso (Augmentation.abelianTotalAdjunction (hypercoveringSituation J H) (Cat.of C)
      J.toGrothendieck (hypercoveringAugmentation J H)).unit)
    (hacyclic : Augmentation.InverseImageComputesDerivedPushforward
      (hypercoveringSituation J H) (Cat.of C) J.toGrothendieck (hypercoveringAugmentation J H))
    (E : DerivedCategory (Sheaf J.toGrothendieck AddCommGrpCat.{u})) :
    IsIso ((Augmentation.derivedAugmentationUnit (hypercoveringSituation J H) (Cat.of C)
      J.toGrothendieck (hypercoveringAugmentation J H)).app E)

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

For a site C with equalizers and fibre products, a hypercovering K of it and the augmentation a : Sh((C/K)_total) ⟶ Sh(C) of Stacks 0D8B, the canonical map E ⟶ Ra_* a⁻¹ E is an isomorphism at every object E of the unbounded derived category of abelian sheaves on C.

theorem isIso_derivedAugmentationUnit_app_of_hypercovering_unconditional
    (E : DerivedCategory (Sheaf P.toGrothendieck AddCommGrpCat.{u})) :
    IsIso ((Augmentation.derivedAugmentationUnit (hypercoveringSituation P H) (Cat.of C)
      P.toGrothendieck (hypercoveringAugmentation P H)).app E)

Stacks.CategoryTheory.Hypercovering.isIso_derivedAugmentationUnit_app_of_hypercovering', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringUnit.lean, line 444. The attribute's comment: “the Ra_*-acyclicity of a⁻¹ of a K-injective complex taken as an explicit input; it is discharged for a hypercovering in ...SimplicialSemiRepresentable.isIso_derivedAugmentationUnit_app_of_hypercovering_unconditional, which carries the tag unconditionally”.

Stacks 0D8G, granted the one input the library does not have. For a site C with equalizers and fibre products, a hypercovering K of it, and the augmentation a : Sh((C/K)_total) ⟶ Sh(C) of Stacks 0D8B, the canonical map E ⟶ R a_* a⁻¹ E is an isomorphism for every object E of the unbounded derived category of abelian sheaves on C.

E is arbitrary: no boundedness is assumed, and the coefficients are the full category of abelian sheaves.

The underived unit F ⟶ a_*a⁻¹F is invertible with nothing carried, by CategoryTheory.SimplicialSemiRepresentable.isIso_situationAbelianTotalAdjunctionUnit, which is Stacks 0D8E in its abelian form for this very augmentation. The one hypothesis left is hacyclic, that a⁻¹ of a K-injective complex of abelian sheaves on C computes R a_*. It is proved for a hypercovering, by CategoryTheory.SimplicialSemiRepresentable .inverseImageComputesDerivedPushforward_of_hypercoveringOfTerminal, and CategoryTheory.SimplicialSemiRepresentable .isIso_derivedAugmentationUnit_app_of_hypercovering_unconditional is this statement with it discharged. It remains a binder here only because that proof rests on the resolution of Stacks 0D78 and on Stacks 01GE, which sit far above this module in the import order; this module defines InverseImageComputesDerivedPushforward itself.

theorem isIso_derivedAugmentationUnit_app_of_hypercovering'
    (hacyclic : Augmentation.InverseImageComputesDerivedPushforward
      (hypercoveringSituation J H) (Cat.of C) J.toGrothendieck (hypercoveringAugmentation J H))
    (E : DerivedCategory (Sheaf J.toGrothendieck AddCommGrpCat.{u})) :
    IsIso ((Augmentation.derivedAugmentationUnit (hypercoveringSituation J H) (Cat.of C)
      J.toGrothendieck (hypercoveringAugmentation J H)).app E)

Tag 0D8H, a lemma

Tag 0D8H in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.derivedGlobalSectionsInverseImageIsoOfHypercovering, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringDerivedGlobalSections.lean, line 223. The attribute's comment: “for the augmentation of Tag 0D8B attached to a hypercovering”.

Stacks 0D8H. For a site C with equalizers and fibre products, a hypercovering K of it, and the augmentation a : Sh((C/K)_total) ⟶ Sh(C) of Stacks 0D8B, derived global sections on C are derived global sections on the total site of the inverse image:

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

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

No hypothesis beyond the hypercovering conditions on K is carried: the three inputs of the general CategoryTheory.SimplicialSiteSituation.Augmentation.derivedGlobalSectionsInverseImageIso are proved for this augmentation. The underived unit F ⟶ a_*a⁻¹F is invertible by CategoryTheory.SimplicialSemiRepresentable.isIso_situationAbelianTotalAdjunctionUnit (Stacks 0D8E in its abelian form), a⁻¹ of a K-injective complex computes R a_* by CategoryTheory.SimplicialSemiRepresentable.inverseImageComputesDerivedPushforward_of_hypercoveringOfTerminal, and the underived identity Γ(C, a_*F) = Γ((C/K)_total, F) is CategoryTheory.SimplicialSemiRepresentable.abelianTotalPushforwardGammaIso.

def derivedGlobalSectionsInverseImageIsoOfHypercovering :
    Augmentation.derivedGlobalSectionsBase (Cat.of C) J.toGrothendieck ≅
      Augmentation.derivedTotalInverseImage (hypercoveringSituation J H) (Cat.of C)
          J.toGrothendieck (hypercoveringAugmentation J H) ⋙
        Augmentation.derivedGlobalSectionsTotal (hypercoveringSituation J H)

Stacks.CategoryTheory.Hypercovering.derivedGlobalSectionsInverseImageIsoOfHypercovering', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringDerivedGlobalSectionsUnconditional.lean, line 155.

Stacks 0D8H. For a site C with equalizers and fibre products, a hypercovering K of it, and the augmentation a : Sh((C/K)_total) ⟶ Sh(C) of Stacks 0D8B, derived global sections on C are derived global sections on the total site of the inverse image:

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

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

No hypothesis beyond the hypercovering conditions on K is carried. The R a_*-acyclicity of a⁻¹ of a K-injective complex, which is the one remaining input of Stacks 0D8G, is CategoryTheory.SimplicialSemiRepresentable .inverseImageComputesDerivedPushforward_of_hypercoveringOfTerminal. The other input of Stacks 0D8G, that the underived unit F ⟶ a_*a⁻¹F is an isomorphism, is Stacks 0D8E in its abelian form, which CategoryTheory.SimplicialSemiRepresentable.isIso_situationAbelianTotalAdjunctionUnit proves for this augmentation. The underived identity Γ(C, a_*F) = Γ((C/K)_total, F) on which the factorisation of Stacks 08J6 rests is CategoryTheory.SimplicialSemiRepresentable.abelianTotalPushforwardGammaIso. The derived content of Stacks 08J6 is not assumed: see the module docstring.

def derivedGlobalSectionsInverseImageIsoOfHypercovering' :
    Augmentation.derivedGlobalSectionsBase (Cat.of C) J.toGrothendieck ≅
      Augmentation.derivedTotalInverseImage (hypercoveringSituation J H) (Cat.of C)
          J.toGrothendieck (hypercoveringAugmentation J H) ⋙
        Augmentation.derivedGlobalSectionsTotal (hypercoveringSituation J H)

Tag 0D8I, a lemma

Tag 0D8I in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.derivedTotalInverseImageEquivalenceOfHypercovering, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBoundedBelowEquivalence.lean, line 435. The attribute's comment: “granted the two inputs of Tag 0D8G and the essential surjectivity clause of 0D8E”.

Stacks 0D8I, granted the inputs the library does not have. For a site C with equalizers and fibre products, a hypercovering K of it, the augmentation a of Stacks 0D8B 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) ⟶ D⁺_𝒜((C/K)_total)

with quasi-inverse R a_*. Both functors of the equivalence are the restrictions of a⁻¹ 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 Stacks 0D8G, inherited unchanged from isIso_derivedAugmentationUnit_app_of_hypercovering: the first is Stacks 0D8E in its abelian form, that the underived unit F ⟶ a_*a⁻¹F is an isomorphism, and the second is that a⁻¹ of a K-injective complex computes R a_*. hsurj is the remaining clause of Stacks 0D8E (2), that every cartesian abelian sheaf on the total site lies in the essential image of a⁻¹; it is carried in the same shape as in mem_essImage_iff_isCartesianAbSheaf. The derived content of Stacks 0D7U is not assumed: see the module docstring.

def derivedTotalInverseImageEquivalenceOfHypercovering :
    (DerivedCategoryB.derivedCategoryBPlus
        (⊤ : ObjectProperty (Sheaf J.toGrothendieck AddCommGrpCat.{u}))).FullSubcategory ≌
      (DerivedCategoryB.derivedCategoryBPlus
        ((hypercoveringSituation J H).IsCartesianAbSheaf)).FullSubcategory

Stacks.CategoryTheory.Hypercovering.derivedTotalInverseImageEquivalenceOfHypercovering_functor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBoundedBelowEquivalence.lean, line 450. The attribute's comment: “the forward functor of the equivalence is a⁻¹”.

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

theorem derivedTotalInverseImageEquivalenceOfHypercovering_functor :
    (derivedTotalInverseImageEquivalenceOfHypercovering J H hunit hacyclic hsurj).functor =
      Augmentation.derivedTotalInverseImagePlus (hypercoveringSituation J H) (Cat.of C)
        J.toGrothendieck (hypercoveringAugmentation J H)

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

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

theorem derivedTotalInverseImageEquivalenceOfHypercovering_inverse :
    (derivedTotalInverseImageEquivalenceOfHypercovering J H hunit hacyclic hsurj).inverse =
      Augmentation.derivedTotalPushforwardPlus (hypercoveringSituation J H) (Cat.of C)
        J.toGrothendieck (hypercoveringAugmentation J H)

Stacks.CategoryTheory.Hypercovering.derivedTotalInverseImageEquivalenceOfHypercovering', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBoundedBelowEquivalenceUnconditional.lean, line 132. References: SGA 4 Vbis (2.2.7), “special case”.

Stacks 0D8I. For a site C with equalizers and fibre products, a hypercovering K of it, the augmentation a of Stacks 0D8B 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) ⟶ D⁺_𝒜((C/K)_total)

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

The Ra_*-acyclicity input of Stacks 0D8G, that a⁻¹ of a K-injective complex computes R a_*, is CategoryTheory.SimplicialSemiRepresentable .inverseImageComputesDerivedPushforward_of_hypercoveringOfTerminal. The other input of Stacks 0D8G, that the underived unit F ⟶ a_*a⁻¹F is an isomorphism, is Stacks 0D8E in its abelian form, which CategoryTheory.SimplicialSemiRepresentable.isIso_situationAbelianTotalAdjunctionUnit proves for this augmentation. The essential surjectivity input of Augmentation.isIso_derivedCounit_app_of_isCartesian, that every cartesian abelian sheaf on the total site lies in the essential image of a⁻¹, is discharged here by CategoryTheory.SimplicialSemiRepresentable .essImage_situationTotalInverseImageAb_of_isCartesianAbSheaf, the Stacks 0D8E (2) clause in the spelling of a⁻¹ as Augmentation.totalInverseImageAb.

def derivedTotalInverseImageEquivalenceOfHypercovering' :
    (DerivedCategoryB.derivedCategoryBPlus
        (⊤ : ObjectProperty (Sheaf J.toGrothendieck AddCommGrpCat.{u}))).FullSubcategory ≌
      (DerivedCategoryB.derivedCategoryBPlus
        ((hypercoveringSituation J H).IsCartesianAbSheaf)).FullSubcategory

Stacks.CategoryTheory.Hypercovering.derivedTotalInverseImageEquivalenceOfHypercovering_functor', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/HypercoveringBoundedBelowEquivalenceUnconditional.lean, line 150. The attribute's comment: “the forward functor of the equivalence is a⁻¹”.

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

theorem derivedTotalInverseImageEquivalenceOfHypercovering_functor' :
    (derivedTotalInverseImageEquivalenceOfHypercovering' J H).functor =
      Augmentation.derivedTotalInverseImagePlus (hypercoveringSituation J H) (Cat.of C)
        J.toGrothendieck (hypercoveringAugmentation J H)

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

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

theorem derivedTotalInverseImageEquivalenceOfHypercovering_inverse' :
    (derivedTotalInverseImageEquivalenceOfHypercovering' J H).inverse =
      Augmentation.derivedTotalPushforwardPlus (hypercoveringSituation J H) (Cat.of C)
        J.toGrothendieck (hypercoveringAugmentation J H)

Tag 09X6, a remark

Tag 09X6 in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.LocalizationAtPresheaf.hasPullbacks_and_hasEqualizers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/LocalizationAtPresheaf.lean, line 332. The attribute's comment: “the site C/G of pairs (U, s), s ∈ G(U), has fibre products and equalizers”.

Stacks 09X6, the site C/G has fibre products and equalizers. If C has fibre products and equalizers, so does the localization C/G of C at a presheaf of sets G: the projection C/G ⥤ C creates connected limits.

theorem hasPullbacks_and_hasEqualizers [HasPullbacks C] [HasEqualizers C] :
    HasPullbacks (CostructuredArrow (yoneda (C := C)) G) ∧
      HasEqualizers (CostructuredArrow (yoneda (C := C)) G)

Stacks.CategoryTheory.Hypercovering.LocalizationAtPresheaf.sectionsOverPresheafSheafifyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/LocalizationAtPresheafCohomology.lean, line 116. The attribute's comment: “H⁰(G, -) = H⁰(G^#, -), the functor whose derived functor is RΓ(G, -)”.

H⁰(G, -) = H⁰(G^#, -) (Stacks 079X, observation (1), quoted in Stacks 09X6): the free abelian sheaf functor inverts the sheafification map G ⟶ G^#.

def sectionsOverPresheafSheafifyIso :
    sectionsOverPresheaf J G ≅
      sectionsOverPresheaf J (sheafify J G)

Stacks.CategoryTheory.Hypercovering.LocalizationAtPresheaf.derivedSectionsOverPresheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/LocalizationAtPresheafCohomology.lean, line 342. The attribute's comment: “RΓ(G, E) = RΓ(C/G, j⁻¹E) for the localization functor j : C/G → C, the analogue of Tag 03F3; an isomorphism of functors on the unbounded derived category”.

Stacks 09X6, RΓ(G, E) = RΓ(C/G, j⁻¹E). Let C be a site and G a presheaf of sets on C, let RΓ(G, -) be the derived functor of H⁰(G, -) = H⁰(G^#, -), maps out of G (Stacks 079X), and let j : C/G ⥤ C be the localization functor of Stacks 0791. Then

RΓ(G, E) = RΓ(C/G, j⁻¹E)

naturally in E in the unbounded derived category of abelian sheaves on C: the analogue of Stacks 03F3 for the localization at G.

def derivedSectionsOverPresheafIso [HasDerivedCategory (Sheaf J AddCommGrpCat.{u})]
    [HasDerivedCategory (Sheaf (localizationTopology J G) AddCommGrpCat.{u})]
    [HasDerivedCategory AddCommGrpCat.{u}] :
    derivedSectionsOverPresheaf J G ≅
      ((CostructuredArrow.proj yoneda G).sheafPushforwardContinuous AddCommGrpCat.{u}
          (localizationTopology J G) J).mapDerivedCategory ⋙
        Stacks.DerivedFunctor.totalRightDerived
          (Sheaf.Γ (localizationTopology J G) AddCommGrpCat.{u})

Stacks.CategoryTheory.Hypercovering.LocalizationAtPresheaf.derivedGlobalSectionsLocalizationIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/LocalizationAtPresheafCohomology.lean, line 413. The attribute's comment: “for a hypercovering K of G, RΓ(C/G, E) = RΓ((C/K)_total, a⁻¹E) with a the canonical augmentation; an isomorphism of functors on the unbounded derived category, which contains D⁺(C/G)”.

Stacks 09X6, RΓ(C/G, E) = RΓ((C/K)_total, a⁻¹E). For a hypercovering K of a presheaf of sets G on a site C with equalizers and fibre products, regarded as a hypercovering of the site C/G, and the canonical augmentation a : Sh((C/K)_total) ⟶ Sh(C/G), derived global sections on C/G are derived global sections on the total site of the inverse image. This is Stacks 0D8H for the site C/G, as the remark says.

def derivedGlobalSectionsLocalizationIso :
    Augmentation.derivedGlobalSectionsBase (Cat.of (CostructuredArrow (yoneda (C := C)) G))
        (localizationPretopology G P).toGrothendieck ≅
      Augmentation.derivedTotalInverseImage
          (hypercoveringSituation (localizationPretopology G P) (localizedHypercovering G P H))
          (Cat.of (CostructuredArrow (yoneda (C := C)) G))
          (localizationPretopology G P).toGrothendieck
          (hypercoveringAugmentation (localizationPretopology G P)
            (localizedHypercovering G P H)) ⋙
        Augmentation.derivedGlobalSectionsTotal
          (hypercoveringSituation (localizationPretopology G P) (localizedHypercovering G P H))

Stacks.CategoryTheory.Hypercovering.LocalizationAtPresheaf.derivedSectionsOverPresheafInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/LocalizationAtPresheafCohomology.lean, line 429. The attribute's comment: “RΓ(G, E) = RΓ((C/K)_total, a⁻¹j⁻¹E) for a hypercovering K of G”.

Stacks 09X6, RΓ(G, E) = RΓ((C/K)_total, a⁻¹j⁻¹E).

def derivedSectionsOverPresheafInverseImageIso :
    derivedSectionsOverPresheaf P.toGrothendieck G ≅
      (localizationInverseImage G P).mapDerivedCategory ⋙
        Augmentation.derivedTotalInverseImage
            (hypercoveringSituation (localizationPretopology G P) (localizedHypercovering G P H))
            (Cat.of (CostructuredArrow (yoneda (C := C)) G))
            (localizationPretopology G P).toGrothendieck
            (hypercoveringAugmentation (localizationPretopology G P)
              (localizedHypercovering G P H)) ⋙
          Augmentation.derivedGlobalSectionsTotal
            (hypercoveringSituation (localizationPretopology G P) (localizedHypercovering G P H))

Stacks.CategoryTheory.Hypercovering.LocalizationAtPresheaf.derivedSectionsOverPresheafCompositeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/LocalizationAtPresheafCohomology.lean, line 563. The attribute's comment: “for a hypercovering K of G, RΓ(G, E) = RΓ((C/K)_total, g⁻¹E) with g the composition of a and j; an isomorphism of functors on the unbounded derived category, which contains D⁺(C)”.

Stacks 09X6, RΓ(G, E) = RΓ((C/K)_total, g⁻¹E). Let C be a site with equalizers and fibre products, G a presheaf of sets on C and K a hypercovering of G. Let g : Sh((C/K)_total) ⟶ Sh(C) be the composition of the canonical augmentation a : Sh((C/K)_total) ⟶ Sh(C/G) and of the localization morphism j : Sh(C/G) ⟶ Sh(C). Then

RΓ(G, E) = RΓ((C/K)_total, g⁻¹E)

naturally in E in the unbounded derived category of abelian sheaves on C, in particular for E ∈ D⁺(C).

def derivedSectionsOverPresheafCompositeIso :
    derivedSectionsOverPresheaf P.toGrothendieck G ≅
      (compositeInverseImage G P H).mapDerivedCategory ⋙
        Augmentation.derivedGlobalSectionsTotal
          (hypercoveringSituation (localizationPretopology G P) (localizedHypercovering G P H))

Stacks.CategoryTheory.Hypercovering.LocalizationAtPresheaf.hypercoveringOfEquivLocalization, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/LocalizationAtPresheafHypercovering.lean, line 745. The attribute's comment: “a hypercovering of G in C is the same thing as a hypercovering for the site C/G, for the site C/G of Stacks 0791 (coverings: families whose image generates a covering sieve of C)”.

A hypercovering of G is the same thing as a hypercovering of the site C/G. Let C be a site, given by a pretopology J, with equalizers and fibre products, and let G be a presheaf of sets on C. Hypercoverings of G in C (Stacks 09VU) correspond bijectively to hypercoverings of the localized site C/G of Stacks 0791: a hypercovering K of G goes to the simplicial object n ↦ {(K_{n,i}, s_{n,i})} of SR(C/G), where s_{n,i} is the restriction of the augmentation F(K_n) ⟶ G to the summand h_{K_{n,i}}, and the three conditions of Stacks 09VU for K over G are the three conditions for it over the final presheaf of C/G.

def hypercoveringOfEquivLocalization :
    HypercoveringOf.{v, w} J G ≃ HypercoveringOfTerminal.{w} (localizationPretopology G J)

Stacks.Sites.PresheafLocalization.mem_restrictedTopology_iff, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topos/PresheafLocalization.lean, line 85. The attribute's comment: “The remark's instruction to define C/G for a PRESHEAF of sets G exactly as in Stacks 0791: the coverings of C/G are those coming from coverings of C, and the topology they generate is already j.restrictedTopology J, with no sheaf hypothesis on G. Carried: nothing. Claimed: this covering characterisation, which is what fixes the topology appearing in nonempty_sheafEquiv_over_sheafification. Disclaimed: fibre products and equalizers of C/G (Mathlib's CostructuredArrow.hasLimitsOfShape_of_isConnected), the hypercovering correspondence, and the RΓ transfer statements.”.

Stacks 09X6, the covering sieves of the localization of C at a presheaf G: a sieve of an object (U, s) of C/G belongs to j.restrictedTopology J, for j = CostructuredArrow.proj yoneda G, exactly when its image under j is a covering sieve of U.

lemma mem_restrictedTopology_iff (X : CostructuredArrow (yoneda (C := C)) G) (S : Sieve X) :
    S ∈ (CostructuredArrow.proj yoneda G).restrictedTopology J X ↔
      S.functorPushforward (CostructuredArrow.proj yoneda G) ∈ J X.left

Stacks.Sites.PresheafLocalization.nonempty_sheafEquiv_over_sheafification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topos/PresheafLocalization.lean, line 255. The attribute's comment: “The parenthetical claim of the remark: the site C/G of pairs (U, s) with s ∈ G(U) for a PRESHEAF of sets G, with the coverings of C, satisfies Sh(C/G) = Sh(C)/G^#. Carried: Stacks 0791 (Presheaf.IsSheaf.exists_sheafEquivalence_costructuredArrow_yoneda) for the SHEAF G^#, supplying the right-hand equivalence. Claimed: the equivalence of categories, for a small site. Disclaimed: the rest of the remark — that C/G is a site with fibre products and equalizers (Mathlib's CostructuredArrow.hasLimitsOfShape_of_isConnected), that hypercoverings of G (Stacks 09VU) correspond to hypercoverings of C/G, and every RΓ transfer statement.”. References: SGA 3 IV (4.5.4), “more general”; SGA 4 III (5.4), “partial”.

Stacks 09X6, the parenthetical claim: on a small site, the topos of sheaves on the localization of C at a presheaf of sets G is the localization of the topos Sh(C) at the sheaf G^#, that is, Sh(C/G) is equivalent to the slice category Sh(C)/G^#.

theorem nonempty_sheafEquiv_over_sheafification :
    Nonempty (Sheaf ((CostructuredArrow.proj yoneda G).restrictedTopology J) (Type u) ≌
      Over ((presheafToSheaf J (Type u)).obj G))

Sources

LeanCategoryTheory.SimplicialSemiRepresentable.faithful_situationTotalInverseImage · CategoryTheory.SimplicialSemiRepresentable.faithful_inverseImage · CategoryTheory.SimplicialSemiRepresentable.faithful_totalInverseImage · CategoryTheory.SimplicialSemiRepresentable.faithful_abelianInverseImage · CategoryTheory.SimplicialSemiRepresentable.isCartesianSheaf_of_mem_essImage · CategoryTheory.SimplicialSemiRepresentable.isCartesianAbSheaf_of_mem_essImage · CategoryTheory.SimplicialSemiRepresentable.full_inverseImage · CategoryTheory.SimplicialSemiRepresentable.fullyFaithfulInverseImageHypercovering

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

85.11 Cohomology and… to 85.17 Cohomological descent for…

Section85.11 Cohomology and augmentations of ringed simplicial sites#

Tag 0D9D, the section

Tag 0DH3, a lemma

Tag 0D7C, a lemma

Tag 0D7D, a lemma

Tag 0D7F, a lemma

Sources

Section85.12 Cartesian sheaves and modules#

Tag 07TF, a definition

Tag 07TG, a lemma

Tag 0D7H, a lemma

Tag 0D7I, a lemma

Tag 07TH, a lemma

Tag 0D7J, a lemma

Tag 0D7K, a remark

Tag 0D7L, a lemma

Tag 0D9E, a lemma

Tag 0D7M, a lemma

Sources

Section85.13 Simplicial systems of the derived category#

Tag 0D9G, a definition

Tag 0D9H, a lemma

Tag 0GME, a lemma

Tag 0D9I, a lemma

Tag 0D9J, a lemma

Tag 0D9K, a lemma

Tag 0D9L, a lemma

Sources

Section85.14 Simplicial systems of the derived category: modules#

Tag 0D9N, a definition

Tag 0D9P, a lemma

Tag 0GMF, a lemma

Tag 0D9Q, a lemma

Tag 0D9R, a lemma

Tag 0D9S, a lemma

Tag 0D9T, a lemma

Sources

Section85.15 The site associated to a semi-representable object#

Tag 0D85, a lemma

Tag 0D86, a lemma

Tag 0D87, a lemma

Tag 0D88, a lemma

Tag 0D89, a remark

Tag 0D9U, a remark

Tag 0D9V, a remark

Sources

Section85.16 The site associate to a simplicial semi-representable object#

Tag 0D8B, a lemma

Tag 09WM, a lemma

Tag 0DC0, a lemma

Tag 0D9W, a remark

Tag 0D9X, a remark

Sources

Section85.17 Cohomological descent for hypercoverings#

Tag 0D8E, a lemma

Tag 0D8F, a lemma

Tag 0D8G, a lemma

Tag 0D8H, a lemma

Tag 0D8I, a lemma

Tag 09X6, a remark

Sources

Section85.11 Cohomology and augmentations of ringed simplicial sites #

Section85.12 Cartesian sheaves and modules #

Section85.13 Simplicial systems of the derived category #

Section85.14 Simplicial systems of the derived category: modules #

Section85.15 The site associated to a semi-representable object #

Section85.16 The site associate to a simplicial semi-representable object #

Section85.17 Cohomological descent for hypercoverings #