85.2 Simplicial topological… to 85.10 Cohomology on ringed…

Section85.2 Simplicial topological spaces#

Section 85.2 of the Stacks Project, Tag 09VK. 13 tags here are carried by 60 declarations of the repository (all in StacksFrontier) and 30 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 09VK, the section

Tag 09VK in the Stacks Project.

Stacks.Topology.Simplicial.ConstantSpace.systemCosimplicialEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/ConstantSpaceSheaves.lean, line 126. The attribute's comment: “systems (F_n, F(φ)) on the constant simplicial space X_• are cosimplicial objects in the category of sheaves on X”.

A system of sheaves on the constant simplicial space on X is the same thing as a cosimplicial sheaf on X.

def systemCosimplicialEquivalence :
    SimplicialSheafSystem (constantSpace X) A ≌ CosimplicialObject (TopCat.Sheaf A X)

Stacks.Topology.Simplicial.ConstantSpace.sheafCosimplicialEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/ConstantSpaceSheaves.lean, line 151. The attribute's comment: “by Lemma 09VM a sheaf on X_{•,Zar} is the same thing as a cosimplicial object in the category of sheaves on X”.

A sheaf on X_{•,Zar} is the same thing as a cosimplicial object in the category of sheaves on X. The equivalence is the description of Lemma 09VM (Stacks.Topology.Simplicial.sheafEquivalenceSimplicialSheafSystem) followed by systemCosimplicialEquivalence; the sheaf in degree [n] of the cosimplicial object attached to a sheaf F is the restriction F_n of F to the opens of the n-th copy of X.

def sheafCosimplicialEquivalence :
    Sheaf (SimplicialOpen.grothendieckTopology (constantSpace X)) A ≌
      CosimplicialObject (TopCat.Sheaf A X)

Stacks.Topology.Simplicial.cechNerveTerminalFrom_δ_π, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/SimplicialSpace.lean, line 119. The attribute's comment: “the face map d^n_i is the projection forgetting the i-th coordinate”.

The face map d^{n+1}_i forgets the i-th coordinate. On the simplicial object X_n = Y^{n+1}, the k-th coordinate of d_i is the (i.succAbove k)-th coordinate, i.e. the coordinates of d_i(y_0, …, y_{n+1}) are those of (y_0, …, y_{n+1}) with y_i left out.

theorem cechNerveTerminalFrom_δ_π {n : ℕ} (i : Fin (n + 2)) (k : Fin (n + 1)) :
    (cechNerveTerminalFrom Y).δ i ≫ Pi.π (fun _ : Fin (n + 1) => Y) k =
      Pi.π (fun _ : Fin (n + 2) => Y) (i.succAbove k)

Stacks.Topology.Simplicial.cechNerveTerminalFrom_σ_π, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/SimplicialSpace.lean, line 128. The attribute's comment: “the degeneracy map s^n_j is the diagonal repeating the j-th coordinate”.

The degeneracy map s^n_j repeats the j-th coordinate. On the simplicial object X_n = Y^{n+1}, the k-th coordinate of s_j is the (j.predAbove k)-th coordinate, i.e. s_j(y_0, …, y_n) = (y_0, …, y_j, y_j, …, y_n).

theorem cechNerveTerminalFrom_σ_π {n : ℕ} (j : Fin (n + 1)) (k : Fin (n + 2)) :
    (cechNerveTerminalFrom Y).σ j ≫ Pi.π (fun _ : Fin (n + 2) => Y) k =
      Pi.π (fun _ : Fin (n + 1) => Y) (j.predAbove k)

Stacks.Topology.Simplicial.SimplicialOpen.toTopCat, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/SimplicialSpace.lean, line 153. The attribute's comment: “a morphism U → V of X_Zar given by φ induces a continuous map U → V”.

A morphism of X_Zar induces a continuous map. An object U ⊆ X_n of the site of a simplicial space is a topological space, and a morphism U → V given by φ induces the continuous map U → V restricting X(φ) : X_n → X_m.

def toTopCat : SimplicialOpen X ⥤ TopCat.{u}

Stacks.Topology.Simplicial.SimplicialOpen.toTopCat_map_comp_inclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/SimplicialSpace.lean, line 172. The attribute's comment: “the induced continuous map U → V is the restriction of X(φ)”.

The continuous map U → V induced by a morphism given by φ is the restriction of X(φ) : X_n → X_m.

theorem toTopCat_map_comp_inclusion {U V : SimplicialOpen X} (f : U ⟶ V) :
    (toTopCat X).map f ≫ V.toOpens.inclusion' = U.toOpens.inclusion' ≫ X.map f.base

Stacks.Topology.Simplicial.componentPresheaf_isSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/SimplicialSpace.lean, line 204. The attribute's comment: “the restriction F_n of a sheaf F on X_Zar to the opens of X_n is a sheaf”.

The restriction F_n of a sheaf on X_Zar to the opens of X_n is a sheaf on X_n. This holds for sheaves with values in any category.

theorem componentPresheaf_isSheaf {X : SimplicialObject TopCat.{u}} {A : Type w} [Category.{v} A]
    (F : Sheaf (SimplicialOpen.grothendieckTopology X) A) (n : SimplexCategoryᵒᵖ) :
    TopCat.Presheaf.IsSheaf (componentPresheaf F.obj n)

Stacks.Topology.Simplicial.SimplicialSheafSystem.transitionMap_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/SimplicialSpace.lean, line 225. The attribute's comment: “F(φ) ∘ F(ψ) = F(φ ∘ ψ), composition of f-maps as in Sheaves 008L”.

F(φ) ∘ F(ψ) = F(φ ∘ ψ). The composite (Stacks 008L) of the f-maps F(φ) and F(ψ) is the f-map of the composite. It is an (X(φ) ≫ X(ψ))-map while F(φ ≫ ψ) is an X(φ ≫ ψ)-map, so the equality is heterogeneous.

theorem transitionMap_comp (P : (SimplicialOpen X)ᵒᵖ ⥤ A) {l m n : SimplexCategoryᵒᵖ}
    (φ : l ⟶ m) (ψ : m ⟶ n) :
    HEq ((transitionMap P φ).compPresheaf (transitionMap P ψ)) (transitionMap P (φ ≫ ψ))

Stacks.Topology.Simplicial.sheafSystem, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/SimplicialSpace.lean, line 255. The attribute's comment: “a sheaf F on X_Zar gives the system (F_n, F(φ))”.

The system (F_n, F(φ)) of a sheaf on X_Zar. A sheaf F on the site of a simplicial space gives the sheaves F_n on the spaces X_n, obtained by restricting F to the opens of X_n, together with the X(φ)-maps F(φ) : F_m → F_n formed by the restriction maps of F, which satisfy F(φ) ∘ F(ψ) = F(φ ∘ ψ) and F(id) = id.

def sheafSystem :
    Sheaf (SimplicialOpen.grothendieckTopology X) A ⥤ SimplicialSheafSystem X A

Stacks.Topology.Simplicial.systemSheafCompSheafSystemIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/SimplicialSpace.lean, line 384. The attribute's comment: “conversely, a system (F_n, F(φ)) with F(φ) ∘ F(ψ) = F(φ ∘ ψ) and F(id) = id gives a sheaf on X_Zar whose system it is”.

A system is the system of its sheaf. The sheaf on X_Zar defined by a system (F_n, F(φ)) has, as its restrictions to the opens of the X_n and as its restriction maps along the morphisms given by the φ, the system (F_n, F(φ)) again, naturally in the system.

def systemSheafCompSheafSystemIso : systemSheaf X A ⋙ sheafSystem X A ≅ 𝟭 _

Declarations registered for the tag:

Tag 09VL, a lemma

Tag 09VL in the Stacks Project.

Stacks.Topology.Simplicial.SimplicialOpen.precoverage_hasIsos, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/Site.lean, line 149. The attribute's comment: “the identity-covering axiom”.

Stacks 09VL. Singleton isomorphisms are levelwise open covering families.

theorem precoverage_hasIsos (X : SimplicialObject TopCat.{u}) :
    (precoverage X).HasIsos

Stacks.Topology.Simplicial.SimplicialOpen.precoverage_hasPullbacks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/Site.lean, line 217. The attribute's comment: “existence of pullbacks of coverings”.

Stacks 09VL. Pullbacks of arrows in a levelwise open covering family along arbitrary morphisms exist.

theorem precoverage_hasPullbacks (X : SimplicialObject TopCat.{u}) :
    (precoverage X).HasPullbacks

Stacks.Topology.Simplicial.SimplicialOpen.precoverage_isStableUnderBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/Site.lean, line 274. The attribute's comment: “the base-change axiom”.

Stacks 09VL. Levelwise open covering families are stable under base change.

theorem precoverage_isStableUnderBaseChange (X : SimplicialObject TopCat.{u}) :
    (precoverage X).IsStableUnderBaseChange

Stacks.Topology.Simplicial.SimplicialOpen.precoverage_isStableUnderComposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/Site.lean, line 310. The attribute's comment: “the composition axiom”.

Stacks 09VL. Levelwise open covering families are stable under composition.

theorem precoverage_isStableUnderComposition (X : SimplicialObject TopCat.{u}) :
    (precoverage X).IsStableUnderComposition
Tag 09VM, a lemma

Tag 09VM in the Stacks Project.

Stacks.Topology.Simplicial.isEquivalence_sheafToSimplicialSheafSystem, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/Sheaves.lean, line 869.

Stacks 09VM. Let X be a simplicial topological space. The functor sheafToSimplicialSheafSystem from sheaves on the site X_Zar of X (SimplicialOpen.grothendieckTopology X: opens of the spaces X n, morphisms over simplex maps, coverings by open coverings inside one degree) to the category SimplicialSheafSystem X A of systems (F_n, F(φ)) of sheaves F_n on X n with X.map φ-maps F(φ) satisfying F(φ) ∘ F(ψ) = F(φ ∘ ψ) and F(id) = id, which sends F to its restrictions to the degrees and its restriction maps over simplex maps, is an equivalence of categories. The values are in an arbitrary category A; sheaves of sets are the case A = Type _.

instance isEquivalence_sheafToSimplicialSheafSystem
    (X : SimplicialObject TopCat.{u}) (A : Type w) [Category.{v} A] :
    (sheafToSimplicialSheafSystem (X := X) (A := A)).IsEquivalence
Tag 09VN, a lemma

Tag 09VN in the Stacks Project.

Stacks.Topology.Simplicial.SimplicialOpen.pullback_isMorphismOfSites, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/Morphisms.lean, line 200.

Stacks 09VN. The simplicial-site morphism on sheaves in the universe of the spaces.

theorem pullback_isMorphismOfSites {X Y : SimplicialObject TopCat.{u}} (f : Y ⟶ X) :
    IsMorphismOfSites.{u} (pullback f)
      (SimplicialOpen.grothendieckTopology X)
      (SimplicialOpen.grothendieckTopology Y)
Tag 09VP, a lemma

Tag 09VP in the Stacks Project.

AlgebraicGeometry.SimplicialScheme.componentModulePushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ZariskiPushforwardQuasicoherent.lean, line 151. The attribute's comment: “part (1) for sheaves of modules on the total Zariski site of a simplicial scheme”.

Stacks 09VP, part (1), for sheaves of modules on the total Zariski site. The degree-n component of the pushforward of a sheaf of 𝒪_V-modules along a morphism f : V ⟶ U of simplicial schemes is the pushforward of its degree-n component along f_n : V_n ⟶ U_n.

public noncomputable def componentModulePushforwardIso (f : V ⟶ U) (G : Modules V)
    (n : SimplexCategoryᵒᵖ) :
    (componentModule U n).obj ((modulePushforward f).obj G) ≅
      (Scheme.Modules.pushforward (f.app n)).obj ((componentModule V n).obj G)

Stacks.Topology.Simplicial.pushforwardComponentIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/ComponentFunctoriality.lean, line 58. The attribute's comment: “part (1)”.

Stacks 09VP, part (1). The component in degree n of direct image along a morphism of simplicial spaces is the direct image along its degree-n component.

noncomputable def pushforwardComponentIso
    {X Y : SimplicialObject TopCat.{u}} (f : Y ⟶ X) (n : SimplexCategoryᵒᵖ) :
    letI : IsMorphismOfSites.{u} (SimplicialOpen.pullback f)
      (SimplicialOpen.grothendieckTopology X)
      (SimplicialOpen.grothendieckTopology Y) :=
        SimplicialOpen.pullback_isMorphismOfSites f
    (SimplicialOpen.pullback f).sheafPushforwardContinuous
        (Type u) (SimplicialOpen.grothendieckTopology X)
        (SimplicialOpen.grothendieckTopology Y) ⋙
      (sheafEquivalenceSimplicialSheafSystem X (Type u)).toEquivalence.functor ⋙
      SimplicialSheafSystem.componentFunctor X (Type u) n ≅
    (sheafEquivalenceSimplicialSheafSystem Y (Type u)).toEquivalence.functor ⋙
      SimplicialSheafSystem.componentFunctor Y (Type u) n ⋙
        TopCat.Sheaf.pushforward (Type u) (f.app n)

Stacks.Topology.Simplicial.pullbackComponentIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/ComponentFunctoriality.lean, line 158. The attribute's comment: “part (2)”.

Stacks 09VP, part (2). The component in degree n of inverse image along a morphism of simplicial spaces is the inverse image along its degree-n component.

noncomputable def pullbackComponentIso
    {X Y : SimplicialObject TopCat.{u}} (f : Y ⟶ X) (n : SimplexCategoryᵒᵖ) :
    letI : IsMorphismOfSites.{u} (SimplicialOpen.pullback f)
      (SimplicialOpen.grothendieckTopology X)
      (SimplicialOpen.grothendieckTopology Y) :=
        SimplicialOpen.pullback_isMorphismOfSites f
    (SimplicialOpen.pullback f).sheafPullback
        (Type u) (SimplicialOpen.grothendieckTopology X)
        (SimplicialOpen.grothendieckTopology Y) ⋙
      (sheafEquivalenceSimplicialSheafSystem Y (Type u)).toEquivalence.functor ⋙
      SimplicialSheafSystem.componentFunctor Y (Type u) n ≅
    (sheafEquivalenceSimplicialSheafSystem X (Type u)).toEquivalence.functor ⋙
      SimplicialSheafSystem.componentFunctor X (Type u) n ⋙
      TopCat.Sheaf.pullback (Type u) (f.app n)
Tag 09W0, a lemma

Tag 09W0 in the Stacks Project.

Stacks.Topology.Simplicial.levelFunctor_isContinuous_mk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/ComponentSite.lean, line 53. The attribute's comment: “component_site_inclusion”.

Stacks 09W0. The inclusion of the open-set site of one component into the site of simplicial opens is continuous.

theorem levelFunctor_isContinuous_mk (X : SimplicialObject TopCat.{u}) (n : ℕ) :
    (levelFunctor X (op (SimplexCategory.mk n))).IsContinuous
      (Opens.grothendieckTopology (X.obj (op (SimplexCategory.mk n))))
      (SimplicialOpen.grothendieckTopology X)

Stacks.Topology.Simplicial.levelFunctor_isCocontinuous_mk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/ComponentSite.lean, line 62. The attribute's comment: “component_site_inclusion”.

Stacks 09W0. The inclusion of the open-set site of one component into the site of simplicial opens is cocontinuous.

theorem levelFunctor_isCocontinuous_mk (X : SimplicialObject TopCat.{u}) (n : ℕ) :
    (levelFunctor X (op (SimplexCategory.mk n))).IsCocontinuous
      (Opens.grothendieckTopology (X.obj (op (SimplexCategory.mk n))))
      (SimplicialOpen.grothendieckTopology X)

Stacks.Topology.Simplicial.inverseImageIsoComponent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/ComponentSite.lean, line 71. The attribute's comment: “inverse_image_is_restriction”.

Stacks 09W0. Pulling a sheaf back to a simplicial component is, naturally in that sheaf, its component in the sheaf-system description.

noncomputable def inverseImageIsoComponent
    (X : SimplicialObject TopCat.{u}) (n : ℕ) :
    (levelFunctor X (op (SimplexCategory.mk n))).sheafPullbackCocontinuous
        (Type u) (Opens.grothendieckTopology (X.obj (op (SimplexCategory.mk n))))
        (SimplicialOpen.grothendieckTopology X) ≅
      (sheafEquivalenceSimplicialSheafSystem X (Type u)).toEquivalence.functor ⋙
        SimplicialSheafSystem.componentFunctor X (Type u)
          (op (SimplexCategory.mk n))

Stacks.Topology.Simplicial.componentLowerShriek, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/LowerShriek.lean, line 82. The attribute's comment: “sheaf_left_adjoint”.

The lower-shriek functor from sheaves of sets on one component to sheaves of sets on the simplicial site.

noncomputable def componentLowerShriek
    (X : SimplicialObject TopCat.{u}) (n : ℕ) :
    Sheaf (Opens.grothendieckTopology (X.obj (op (SimplexCategory.mk n)))) (Type u) ⥤
      Sheaf (SimplicialOpen.grothendieckTopology X) (Type u)

Stacks.Topology.Simplicial.componentLowerShriek_adjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/LowerShriek.lean, line 94. The attribute's comment: “sheaf_left_adjoint”.

Stacks 09W0. Lower shriek is left adjoint to inverse image from the total simplicial site to a component.

noncomputable def componentLowerShriek_adjunction
    (X : SimplicialObject TopCat.{u}) (n : ℕ) :
    componentLowerShriek X n ⊣
      (levelFunctor X (op (SimplexCategory.mk n))).sheafPullbackCocontinuous
        (Type u) (Opens.grothendieckTopology (X.obj (op (SimplexCategory.mk n))))
        (SimplicialOpen.grothendieckTopology X)

Stacks.Topology.Simplicial.componentLowerShriek_preservesFiniteConnectedLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/LowerShriek.lean, line 106. The attribute's comment: “sheaf_left_adjoint_connected_limits”.

Stacks 09W0. Lower shriek from a simplicial component preserves finite connected limits.

theorem componentLowerShriek_preservesFiniteConnectedLimits
    (X : SimplicialObject TopCat.{u}) (n : ℕ)
    (J : Type vC) [SmallCategory J] [FinCategory J] [IsConnected J] :
    PreservesLimitsOfShape J (componentLowerShriek X n)

Stacks.Topology.Simplicial.componentLowerShriekAb, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/LowerShriek.lean, line 120. The attribute's comment: “abelian_left_adjoint”.

Lower shriek from sheaves of abelian groups on a component to sheaves of abelian groups on the total simplicial site.

noncomputable def componentLowerShriekAb
    (X : SimplicialObject TopCat.{u}) (n : ℕ) :
    Sheaf (Opens.grothendieckTopology (X.obj (op (SimplexCategory.mk n)))) Ab.{u} ⥤
      Sheaf (SimplicialOpen.grothendieckTopology X) Ab.{u}

Stacks.Topology.Simplicial.componentLowerShriekAb_adjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/LowerShriek.lean, line 134. The attribute's comment: “abelian_left_adjoint”.

Stacks 09W0. Abelian lower shriek is left adjoint to restriction from the total simplicial site to a component.

noncomputable def componentLowerShriekAb_adjunction
    (X : SimplicialObject TopCat.{u}) (n : ℕ) :
    componentLowerShriekAb X n ⊣
      (levelFunctor X (op (SimplexCategory.mk n))).sheafPushforwardContinuous
        Ab.{u}
        (Opens.grothendieckTopology (X.obj (op (SimplexCategory.mk n))))
        (SimplicialOpen.grothendieckTopology X)

Stacks.Topology.Simplicial.componentLowerShriekAb_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/LowerShriek.lean, line 232. The attribute's comment: “abelian_left_adjoint_exact”.

Stacks 09W0. Abelian lower shriek from a component of a simplicial space is exact.

theorem componentLowerShriekAb_exact
    (X : SimplicialObject TopCat.{u}) (n : ℕ)
    [∀ F : (Opens (X.obj (op (SimplexCategory.mk n))))ᵒᵖ ⥤ Ab.{w},
      (levelFunctor X (op (SimplexCategory.mk n))).op.HasLeftKanExtension F]
    [HasSheafify (SimplicialOpen.grothendieckTopology X) Ab.{w}] :
    exactFunctor
      (Sheaf (Opens.grothendieckTopology (X.obj (op (SimplexCategory.mk n)))) Ab.{w})
      (Sheaf (SimplicialOpen.grothendieckTopology X) Ab.{w})
      (Functor.sheafPullbackConstruction.sheafPullback
        (levelFunctor X (op (SimplexCategory.mk n))) Ab.{w}
        (Opens.grothendieckTopology (X.obj (op (SimplexCategory.mk n))))
        (SimplicialOpen.grothendieckTopology X))

Stacks.Topology.Simplicial.exactFunctor_componentLowerShriekAb, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/LowerShriek.lean, line 267. The attribute's comment: “abelian_left_adjoint_exact”.

Stacks 09W0, part (5): g_{n!} is exact. This is componentLowerShriekAb_exact for the registered functor componentLowerShriekAb and with no hypotheses: on the small site of opens of a topological space, with coefficients in abelian groups of the same universe, both the left Kan extensions and the sheafification used to build lower shriek exist.

theorem exactFunctor_componentLowerShriekAb (X : SimplicialObject TopCat.{u}) (n : ℕ) :
    exactFunctor
      (Sheaf (Opens.grothendieckTopology (X.obj (op (SimplexCategory.mk n)))) Ab.{u})
      (Sheaf (SimplicialOpen.grothendieckTopology X) Ab.{u})
      (componentLowerShriekAb X n)
Tag 09W1, a lemma

Tag 09W1 in the Stacks Project.

Stacks.Topology.Simplicial.componentRestrictionAb_preservesInjectiveObjects, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/LowerShriek.lean, line 280. The attribute's comment: “restriction to a degree preserves injectives”.

Stacks 09W1. Restriction of abelian sheaves from the site of a simplicial space to the site of one of its degrees preserves injective objects: it is right adjoint to lower shriek, which is exact.

theorem componentRestrictionAb_preservesInjectiveObjects
    (X : SimplicialObject TopCat.{u}) (n : ℕ)
    [∀ F : (Opens (X.obj (op (SimplexCategory.mk n))))ᵒᵖ ⥤ Ab.{w},
      (levelFunctor X (op (SimplexCategory.mk n))).op.HasLeftKanExtension F]
    [HasSheafify (SimplicialOpen.grothendieckTopology X) Ab.{w}]
    [HasSheafify (Opens.grothendieckTopology (X.obj (op (SimplexCategory.mk n)))) Ab.{w}] :
    ((levelFunctor X (op (SimplexCategory.mk n))).sheafPushforwardContinuous Ab.{w}
        (Opens.grothendieckTopology (X.obj (op (SimplexCategory.mk n))))
        (SimplicialOpen.grothendieckTopology X)).PreservesInjectiveObjects

Stacks.Topology.Simplicial.injective_component, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/LowerShriek.lean, line 337.

Stacks 09W1. If I is an injective abelian sheaf on the site of a simplicial space X, then its degree-n component I n is an injective abelian sheaf on X n.

theorem injective_component (X : SimplicialObject TopCat.{u}) (n : ℕ)
    [∀ F : (Opens (X.obj (op (SimplexCategory.mk n))))ᵒᵖ ⥤ Ab.{w},
      (levelFunctor X (op (SimplexCategory.mk n))).op.HasLeftKanExtension F]
    [HasSheafify (SimplicialOpen.grothendieckTopology X) Ab.{w}]
    [HasSheafify (Opens.grothendieckTopology (X.obj (op (SimplexCategory.mk n)))) Ab.{w}]
    (E : SheafSystemEquivalence X Ab.{w})
    (I : Sheaf (SimplicialOpen.grothendieckTopology X) Ab.{w}) [Injective I] :
    Injective ((E.toEquivalence.functor.obj I).component (op (SimplexCategory.mk n)))
Tag 09W2, a lemma

Tag 09W2 in the Stacks Project.

Stacks.Topology.Simplicial.componentPullbackNaturalityIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/ComponentFunctoriality.lean, line 302.

Stacks 09W2. Restriction to the n-th component commutes, naturally in the sheaf, with inverse image along a map of simplicial spaces.

noncomputable def componentPullbackNaturalityIso
    {X Y : SimplicialObject TopCat.{u}} (f : Y ⟶ X) (n : ℕ) :
    letI : IsMorphismOfSites.{u} (SimplicialOpen.pullback f)
      (SimplicialOpen.grothendieckTopology X)
      (SimplicialOpen.grothendieckTopology Y) :=
        SimplicialOpen.pullback_isMorphismOfSites f
    (levelFunctor X (op (SimplexCategory.mk n))).sheafPullbackCocontinuous
        (Type u) (Opens.grothendieckTopology (X.obj (op (SimplexCategory.mk n))))
        (SimplicialOpen.grothendieckTopology X) ⋙
      TopCat.Sheaf.pullback (Type u) (f.app (op (SimplexCategory.mk n))) ≅
    (SimplicialOpen.pullback f).sheafPullback
        (Type u) (SimplicialOpen.grothendieckTopology X)
        (SimplicialOpen.grothendieckTopology Y) ⋙
      (levelFunctor Y (op (SimplexCategory.mk n))).sheafPullbackCocontinuous
        (Type u) (Opens.grothendieckTopology (Y.obj (op (SimplexCategory.mk n))))
        (SimplicialOpen.grothendieckTopology Y)
Tag 09W4, a lemma

Tag 09W4 in the Stacks Project.

Stacks.Topology.Simplicial.augmentationMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/Augmentation.lean, line 621. The attribute's comment: “the canonical morphism of topoi”.

The morphism from the topos of a simplicial space to that of its augmentation target, with the coherent component identifications from the construction in the source proof.

noncomputable def augmentationMorphism
    (a : Y ⟶ (SimplicialObject.const TopCat).obj X) :
    AugmentationMorphismData Y X a

Stacks.Topology.Simplicial.augmentationMorphism_inverseImage_component, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/Augmentation.lean, line 645. The attribute's comment: “part (1): inverse image on components”.

Stacks 09W4 (1). Inverse image along the augmentation restricts in degree n to inverse image along the component map a_n.

noncomputable def augmentationMorphism_inverseImage_component
    (n : SimplexCategoryᵒᵖ) :
    (augmentationMorphism Y X a).inverseImage ⋙
      (sheafEquivalenceSimplicialSheafSystem Y (Type u)).toEquivalence.functor ⋙
        SimplicialSheafSystem.componentFunctor Y (Type u) n ≅
      TopCat.Sheaf.pullback (Type u) (a.app n)

Stacks.Topology.Simplicial.augmentationMorphism_inverseImage_transition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/Augmentation.lean, line 656. The attribute's comment: “part (1): compatibility of inverse-image transitions”.

The inverse-image component isomorphisms intertwine every system transition with the canonical map between pullbacks induced by the augmentation equation.

theorem augmentationMorphism_inverseImage_transition (F : TopCat.Sheaf (Type u) X)
    {n m : SimplexCategoryᵒᵖ} (φ : n ⟶ m) (V : (Opens (Y.obj m))ᵒᵖ) :
    let S := (sheafEquivalenceSimplicialSheafSystem Y (Type u)).toEquivalence.functor.obj
      ((augmentationMorphism Y X a).inverseImage.obj F)
    (S.transition φ).app V ≫
        ((TopCat.Sheaf.forget (Type u) (Y.obj n)).map
          ((augmentationMorphism_inverseImage_component Y X a n).app F).hom).app
            (op ((Opens.map (Y.map φ)).obj V.unop)) =
      ((TopCat.Sheaf.forget (Type u) (Y.obj m)).map
        ((augmentationMorphism_inverseImage_component Y X a m).app F).hom).app V ≫
          (augmentationPullbackTransition Y X a F φ).app V

Stacks.Topology.Simplicial.augmentationMorphism_comp_component, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/Augmentation.lean, line 672. The attribute's comment: “part (3): composition with a component inclusion”.

Stacks 09W4 (3). The composite of the component inclusion and the augmentation agrees with the topological morphism induced by a_n.

noncomputable def augmentationMorphism_comp_component (n : SimplexCategoryᵒᵖ) :
    (augmentationMorphism Y X a).inverseImage ⋙
      (levelFunctor Y n).sheafPullbackCocontinuous (Type u)
        (Opens.grothendieckTopology (Y.obj n))
        (SimplicialOpen.grothendieckTopology Y) ≅
      TopCat.Sheaf.pullback (Type u) (a.app n)

Stacks.Topology.Simplicial.augmentationMorphism_pushforwardEqualizer, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/Augmentation.lean, line 703. The attribute's comment: “part (4): direct image as an equalizer”.

Stacks 09W4 (4). The direct image of a sheaf on the simplicial site is the equalizer of the two degree-one transition maps on direct images.

noncomputable def augmentationMorphism_pushforwardEqualizer
    (G : Sheaf (SimplicialOpen.grothendieckTopology Y) (Type u)) :
    (augmentationMorphism Y X a).pushforward.obj G ≅
      equalizer (augmentationFaceMap Y X a G 0) (augmentationFaceMap Y X a G 1)

Declarations registered for the tag:

Tag 09W5, a lemma

Tag 09W5 in the Stacks Project.

Stacks.Topology.Simplicial.freeAbelianRepresentableComplex_quasiIso_constant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/Resolution.lean, line 203.

Stacks 09W5. The alternating face-map complex of the free abelian presheaves represented by X_n, augmented towards the constant presheaf of integers, is a resolution in abelian presheaves.

theorem freeAbelianRepresentableComplex_quasiIso_constant
    (X : SimplicialObject TopCat.{u}) :
    QuasiIso (AlternatingFaceMapComplex.ε.app
      (augmentedFreeAbelianPresheaf X))
Tag 09W6, a lemma

Tag 09W6 in the Stacks Project.

Stacks.Topology.Simplicial.cohomologySpectralSequence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/CohomologySpectralSequence.lean, line 317. The attribute's comment: “the spectral sequence, functorial in the abelian sheaf”.

Stacks 09W6. For an abelian sheaf F on the site of a simplicial topological space X there is a first-quadrant cohomological spectral sequence, functorial in F: the second spectral sequence of the double complex A^{q,p} = I^q(X_p) of a chosen injective resolution of F, presented from its first page. Its first page is cohomologySpectralSequence_pageOneIso, and its convergence to H^{p+q}(X_Zar, F) is cohomologySpectralSequence_abutment.

noncomputable def cohomologySpectralSequence :
    Sheaf (SimplicialOpen.grothendieckTopology X) Ab.{w} ⥤
      CohomologicalSpectralSequenceNat Ab.{w} 1

Stacks.Topology.Simplicial.cohomologySpectralSequence_pageOneIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/CohomologySpectralSequence.lean, line 614. The attribute's comment: “the first page is H^q(X_p, F_p)”.

Stacks 09W6. The first page of the spectral sequence of a simplicial topological space is E_1^{p,q} = H^q(X_p, F_p), the sheaf cohomology of the restriction of F to the space in simplicial degree p, naturally in the abelian sheaf F.

noncomputable def cohomologySpectralSequence_pageOneIso (q : ℕ) :
    pageOneFunctor.{u, w} X n q ≅ componentCohomologyFunctor.{u, w} X n q

Stacks.Topology.Simplicial.cohomologySpectralSequence_abutment, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/CohomologySpectralSequenceAbutment.lean, line 1270. The attribute's comment: “convergence to H^{p+q}(X_Zar, F), functorially in the abelian sheaf”.

Stacks 09W6, the convergence. The spectral sequence of a simplicial topological space, with first page E_1^{p,q} = H^q(X_p, F_p), converges to H^{p+q}(X_Zar, F), functorially in the abelian sheaf F: for every n there is a finite decreasing filtration of H^n(X_Zar, F) = R^nΓ(X_Zar, F), natural in F, which is the whole group in step 0 and zero in step n + 1, and whose graded pieces are naturally the terms E_∞^{p,n-p} of the infinity page.

The filtration is the one the filtration of the total complex of A^{q,p} = I^q(X_p) by the simplicial degree induces on its cohomology (simplicialFunctorialAbutment); that cohomology is H^n(X_Zar, F) by cohomologySpectralSequence_abutmentIso.

def cohomologySpectralSequence_abutment :
    FunctorialFirstQuadrantAbutsTo (cohomologySpectralSequence.{u, w} X)
      (fun n => (Sheaf.Γ (SimplicialOpen.grothendieckTopology X) Ab.{w}).rightDerived n)
Tag 0D84, a lemma

Tag 0D84 in the Stacks Project.

Stacks.Topology.Simplicial.fibreRestrictionAb_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/AugmentationFibreCohomology.lean, line 117. The attribute's comment: “the proof's use of exactness of restriction to the fibre”.

Restriction of abelian sheaves to the fibre is exact.

theorem fibreRestrictionAb_exact :
    exactFunctor (Sheaf (SimplicialOpen.grothendieckTopology X) Ab.{u})
      (Sheaf (SimplicialOpen.grothendieckTopology (fibreSpace X Y a V)) Ab.{u})
      (fibreRestrictionAb X Y a V)

Stacks.Topology.Simplicial.fibreRestrictedSections_rightDerived_iso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/AugmentationFibreCohomology.lean, line 185. The attribute's comment: “the proof's reduction: derived sections of the restriction are fibre cohomology”.

Stacks 0D84, the reduction step of the proof. The n-th right derived functor of F ↦ Γ((X ×_Y V)_Zar, F|) is the cohomology Hⁿ((X ×_Y V)_Zar, F|) of the restriction.

An injective resolution of F on X_Zar restricts to an injective resolution of F| on (X ×_Y V)_Zar, because restriction is exact (fibreRestrictionAb_exact) and carries injectives to injectives (part (1) of the source proof, fibreRestrictionAb_preservesInjectiveObjects); so one and the same complex computes both sides.

noncomputable def fibreRestrictedSections_rightDerived_iso (n : ℕ)
    (F : Sheaf (SimplicialOpen.grothendieckTopology X) Ab.{u}) :
    ((fibreRestrictedSections X Y a V).rightDerived n).obj F ≅
      (fibreCohomology X Y a V n).obj ((fibreRestrictionAb X Y a V).obj F)

Stacks.Topology.Simplicial.fibreRestrictionAb_preservesInjectiveObjects, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/AugmentationFibreInjectives.lean, line 141. The attribute's comment: “part (1) of the proof: restriction to the fibre preserves injectives”.

Stacks 0D84, part (1) of the proof. The restriction of an abelian sheaf on X_Zar to (X ×_Y V)_Zar preserves injective objects: its left adjoint, extension by zero, is exact, and a right adjoint of a functor preserving monomorphisms preserves injectives ([Stacks, Tag 015Z]).

theorem fibreRestrictionAb_preservesInjectiveObjects :
    (fibreRestrictionAb X Y a V).PreservesInjectiveObjects

Stacks.Topology.Simplicial.injective_fibreRestrictionAb_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/AugmentationFibreInjectives.lean, line 149. The attribute's comment: “part (1) of the proof: the restriction of an injective is injective”.

Stacks 0D84, part (1) of the proof. The restriction to (X ×_Y V)_Zar of an injective abelian sheaf on X_Zar is an injective abelian sheaf.

theorem injective_fibreRestrictionAb_obj
    (I : Sheaf (SimplicialOpen.grothendieckTopology X) Ab.{u}) [Injective I] :
    Injective ((fibreRestrictionAb X Y a V).obj I)

Stacks.Topology.Simplicial.augmentationCohomologyPresheaf_obj_iso_fibreCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/AugmentationFibreMain.lean, line 66. The attribute's comment: “the values of the displayed presheaf are the cohomology of the fibre”.

Stacks 0D84. The value over an open V of the target of the cohomology presheaf of an augmentation is the cohomology Hⁿ((X ×_Y V)_Zar, F|) of the restriction of F to the total site of the fibre X ×_Y V.

This is the displayed rule of the statement. Three steps: the value of the cohomology presheaf over V is the n-th right derived functor of the sections of the direct image over V (exactness of evaluation); those sections are the global sections of the restriction to the fibre, which is part (2) of the source proof; and the derived functors of the global sections of the restriction are the cohomology of the fibre, because restriction is exact and carries injectives to injectives, which is part (1) of the source proof.

theorem augmentationCohomologyPresheaf_obj_iso_fibreCohomology (n : ℕ)
    (F : Sheaf (SimplicialOpen.grothendieckTopology X) Ab.{u}) :
    Nonempty (((augmentationCohomologyPresheaf X Y a n).obj F).obj (op V) ≅
      (fibreCohomology X Y a V n).obj ((fibreRestrictionAb X Y a V).obj F))

Stacks.Topology.Simplicial.higherDirectImage_iso_sheafify_fibreCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/AugmentationFibreMain.lean, line 81.

Stacks 0D84. Let X be a simplicial space, let a : X ⟶ Y be an augmentation and let F be an abelian sheaf on X_Zar. Then Rⁿa_*F is the sheaf associated to the presheaf whose value over an open V of Y is Hⁿ((X ×_Y V)_Zar, F|_{(X ×_Y V)_Zar}).

theorem higherDirectImage_iso_sheafify_fibreCohomology (n : ℕ)
    (F : Sheaf (SimplicialOpen.grothendieckTopology X) Ab.{u}) :
    Nonempty (((augmentationPushforwardAb X Y a).rightDerived n).obj F ≅
        (presheafToSheaf (Opens.grothendieckTopology Y) Ab.{u}).obj
          ((augmentationCohomologyPresheaf X Y a n).obj F)) ∧
      ∀ V : Opens Y,
        Nonempty (((augmentationCohomologyPresheaf X Y a n).obj F).obj (op V) ≅
          (fibreCohomology X Y a V n).obj ((fibreRestrictionAb X Y a V).obj F))

Stacks.Topology.Simplicial.augmentationFibreSections_iso_fibreRestrictedSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/AugmentationFibrePartTwo.lean, line 343. The attribute's comment: “part (2) of the proof: the direct image over V is the sections over the fibre”.

Stacks 0D84, part (2) of the proof. The sections over V of the direct image of an abelian sheaf F on X_Zar along an augmentation are the global sections over the total site of the fibre X ×_Y V of the restriction of F, naturally in F.

noncomputable def augmentationFibreSections_iso_fibreRestrictedSections :
    augmentationFibreSections X Y a V ≅ fibreRestrictedSections X Y a V

Stacks.Topology.Simplicial.higherDirectImage_iso_sheafify_augmentationCohomologyPresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/AugmentationHigherDirectImage.lean, line 198. The attribute's comment: “the sheafification of the cohomology presheaf; not its fibrewise values”.

Stacks 0D84. Let X be a simplicial space, let a : X ⟶ Y be an augmentation and let F be an abelian sheaf on X_Zar. Then the n-th higher direct image Rⁿa_*F is the sheaf associated to the cohomology presheaf of the augmentation, whose value over an open V of Y is Hⁿ((X ×_Y V)_Zar, F|_{(X ×_Y V)_Zar}).

Sheafification is exact, so it commutes with the right derived functors of the presheaf-valued direct image; the higher direct image is the right derived functor of the sheaf-valued one, which is the sheafification of the presheaf-valued one.

theorem higherDirectImage_iso_sheafify_augmentationCohomologyPresheaf (n : ℕ)
    (F : Sheaf (SimplicialOpen.grothendieckTopology X) Ab.{u}) :
    Nonempty (((augmentationPushforwardAb X Y a).rightDerived n).obj F ≅
      (presheafToSheaf (Opens.grothendieckTopology Y) Ab.{u}).obj
        ((augmentationCohomologyPresheaf X Y a n).obj F))

Stacks.Topology.Simplicial.augmentationCohomologyPresheaf_evaluation_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/AugmentationHigherDirectImage.lean, line 220. The attribute's comment: “those values as derived sections of the direct image, not as fibre cohomology”.

Stacks 0D84. The value over an open V of the target of the cohomology presheaf of an augmentation is the n-th right derived functor of the sections of the direct image over V. By part (2) of the source proof the latter functor is F ↦ H⁰((X ×_Y V)_Zar, F|), so this is the displayed rule V ↦ Hⁿ((X ×_Y V)_Zar, F|) of the statement.

Evaluation of a presheaf of abelian groups at an open is exact, so it commutes with right derived functors.

theorem augmentationCohomologyPresheaf_evaluation_iso (n : ℕ)
    (F : Sheaf (SimplicialOpen.grothendieckTopology X) Ab.{u}) (V : Opens Y) :
    Nonempty (((augmentationCohomologyPresheaf X Y a n).obj F).obj (op V) ≅
      ((augmentationFibreSections X Y a V).rightDerived n).obj F)

Stacks.Topology.Simplicial.augmentationPushforwardAb_forget_isoEqualizer, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/AugmentationHigherDirectImage.lean, line 240. The attribute's comment: “degree zero: the direct image as an equalizer of fibrewise direct images”.

Stacks 0D84, part (2a) of the proof. The underlying sheaf of sets of the direct image a_*F of an abelian sheaf along an augmentation is the equalizer of the two maps induced by the vertices of the one-simplex between the direct images of the degree-zero and the degree-one components of F.

Over an open V of the target the two sheaves of that equalizer have sections the sections of F over the simplicial opens a_0⁻¹(V) and a_1⁻¹(V), which are the degree-zero and degree-one components of the simplicial space X ×_Y V. This is the fibrewise description of the sections of a_*F used in the source proof.

def augmentationPushforwardAb_forget_isoEqualizer
    (F : Sheaf (SimplicialOpen.grothendieckTopology X) Ab.{u}) :
    (sheafCompose (Opens.grothendieckTopology Y) (forget Ab.{u})).obj
        ((augmentationPushforwardAb X Y a).obj F) ≅
      equalizer
        (augmentationFaceMap X Y a
          ((sheafCompose (SimplicialOpen.grothendieckTopology X) (forget Ab.{u})).obj F) 0)
        (augmentationFaceMap X Y a
          ((sheafCompose (SimplicialOpen.grothendieckTopology X) (forget Ab.{u})).obj F) 1)
Tag 09W3, a lemma

Tag 09W3 in the Stacks Project.

Stacks.Topology.Simplicial.constantSiteFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/ConstantSpace.lean, line 70. The attribute's comment: “the functor on sites”.

The functor from the simplicial-open site of the constant simplicial space to the site of open subsets of its value.

def constantSiteFunctor (X : TopCat.{u}) :
    SimplicialOpen (constantSpace X) ⥤ Opens X

Stacks.Topology.Simplicial.constantSiteFunctor_isContinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/ConstantSpace.lean, line 117. The attribute's comment: “the functor is continuous”.

The constant-site functor preserves sheaves.

theorem constantSiteFunctor_isContinuous (X : TopCat.{u}) :
    (constantSiteFunctor X).IsContinuous
      (SimplicialOpen.grothendieckTopology (constantSpace X))
      (Opens.grothendieckTopology X)

Stacks.Topology.Simplicial.constantSiteFunctor_isCocontinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/ConstantSpace.lean, line 130. The attribute's comment: “the functor is cocontinuous”.

The constant-site functor lifts covers.

theorem constantSiteFunctor_isCocontinuous (X : TopCat.{u}) :
    (constantSiteFunctor X).IsCocontinuous
      (SimplicialOpen.grothendieckTopology (constantSpace X))
      (Opens.grothendieckTopology X)

Stacks.Topology.Simplicial.constantMorphism_inverseImage_isoRestriction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/ConstantSpace.lean, line 359. The attribute's comment: “inverse image is restriction along the functor”.

The canonical morphism has inverse image given by restriction along the constant-site functor, naturally in the sheaf.

noncomputable def constantMorphism_inverseImage_isoRestriction (X : TopCat.{u}) :
    (constantMorphism X).inverseImage ≅
    (constantSiteFunctor X).sheafPushforwardContinuous (Type u)
        (SimplicialOpen.grothendieckTopology (constantSpace X))
        (Opens.grothendieckTopology X)

Stacks.Topology.Simplicial.constantMorphism_inverseImage_component, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/ConstantSpace.lean, line 376. The attribute's comment: “part (1): constant cosimplicial inverse image”.

Inverse image of a sheaf is the same sheaf in every simplicial degree, naturally in the sheaf.

noncomputable def constantMorphism_inverseImage_component (X : TopCat.{u})
    (n : SimplexCategoryᵒᵖ) :
    (constantMorphism X).inverseImage ⋙
      (sheafEquivalenceSimplicialSheafSystem (constantSpace X)
        (Type u)).toEquivalence.functor ⋙
        SimplicialSheafSystem.componentFunctor (constantSpace X) (Type u) n ≅
      𝟭 (TopCat.Sheaf (Type u) X)

Stacks.Topology.Simplicial.constantMorphism_inverseImage_transition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/ConstantSpace.lean, line 388. The attribute's comment: “part (1): constant transition maps”.

The component identifications respect every cosimplicial transition: the transition maps of inverse image become identity maps of the original sheaf.

theorem constantMorphism_inverseImage_transition (X : TopCat.{u})
    (F : TopCat.Sheaf (Type u) X) {n m : SimplexCategoryᵒᵖ} (φ : n ⟶ m)
    (V : (Opens X)ᵒᵖ) :
    let S := (sheafEquivalenceSimplicialSheafSystem (constantSpace X)
        (Type u)).toEquivalence.functor.obj
        ((constantMorphism X).inverseImage.obj F)
    (S.transition φ).app V ≫
      ((TopCat.Sheaf.forget (Type u) X).map
        ((constantMorphism_inverseImage_component X n).app F).hom).app V =
      ((TopCat.Sheaf.forget (Type u) X).map
        ((constantMorphism_inverseImage_component X m).app F).hom).app V

Stacks.Topology.Simplicial.constantLowerShriek, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/ConstantSpace.lean, line 403. The attribute's comment: “part (2): lower shriek is the degree-zero component”.

Lower shriek takes the degree-zero sheaf.

def constantLowerShriek (X : TopCat.{u}) :
    Sheaf (SimplicialOpen.grothendieckTopology (constantSpace X)) (Type u) ⥤
      TopCat.Sheaf (Type u) X

Stacks.Topology.Simplicial.constantLowerShriek_adjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/ConstantSpace.lean, line 433. The attribute's comment: “the lower-shriek adjunction”.

Stacks 09W3. Lower shriek is left adjoint to the inverse image of the constant morphism.

noncomputable def constantLowerShriek_adjunction (X : TopCat.{u}) :
    constantLowerShriek X ⊣ (constantMorphism X).inverseImage

Stacks.Topology.Simplicial.constantMorphism_pushforwardEqualizer, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Simplicial/ConstantSpace.lean, line 463. The attribute's comment: “part (3): direct image as an equalizer”.

The direct image of a sheaf on the constant simplicial space is the equalizer of its two vertex transition maps from degree zero to degree one.

noncomputable def constantMorphism_pushforwardEqualizer (X : TopCat.{u})
    (G : Sheaf (SimplicialOpen.grothendieckTopology (constantSpace X)) (Type u)) :
    (constantMorphism X).pushforward.obj G ≅
      equalizer (constantFaceMap X G 0) (constantFaceMap X G 1)

Declarations registered for the tag:

Sources
LeanStacks.Topology.Simplicial.ConstantSpace.systemCosimplicialEquivalence · Stacks.Topology.Simplicial.ConstantSpace.sheafCosimplicialEquivalence · Stacks.Topology.Simplicial.cechNerveTerminalFrom_δ_π · Stacks.Topology.Simplicial.cechNerveTerminalFrom_σ_π · Stacks.Topology.Simplicial.SimplicialOpen.toTopCat · Stacks.Topology.Simplicial.SimplicialOpen.toTopCat_map_comp_inclusion · Stacks.Topology.Simplicial.componentPresheaf_isSheaf · Stacks.Topology.Simplicial.SimplicialSheafSystem.transitionMap_comp

Section85.3 Simplicial sites and topoi#

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

Tag 09WC, a lemma

Tag 09WC in the Stacks Project.

CategoryTheory.SimplicialSite.totalCoverage_hasPullbacks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/TotalPullbacks.lean, line 256. The attribute's comment: “existence of pullbacks of coverings”.

Pullbacks of fibrewise covering families along arbitrary total morphisms exist.

theorem totalCoverage_hasPullbacks (C : SimplicialSite.{u}) :
    C.totalCoverage.HasPullbacks

CategoryTheory.SimplicialSite.totalCoverage_isStableUnderBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/TotalPullbacks.lean, line 288. The attribute's comment: “the base-change axiom”.

The fibrewise covering families are stable under base change in the total category.

theorem totalCoverage_isStableUnderBaseChange (C : SimplicialSite.{u}) :
    C.totalCoverage.IsStableUnderBaseChange

Declarations registered for the tag:

Tag 09WD, a lemma

Tag 09WD in the Stacks Project.

CategoryTheory.SimplicialCoverings.total_isSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/TotalIsSite.lean, line 201. References: SGA 4 VI (7.4.1), “simplicial, cocontinuous”.

Stacks 09WD. If the transition functors in a simplicial family of sites are cocontinuous and satisfy property P, then the componentwise covering families make its Grothendieck construction into a site.

theorem total_isSite (F : SimplicialObject Cat.{v, u})
    (Cov : ∀ n, Covering.{u, v, max u v} (F.obj n) → Prop)
    (hsite : ∀ n, IsSite (Cov n))
    (_hcocont : IsCocontinuous F Cov)
    (hP : ∀ {m n : SimplexCategoryᵒᵖ} (f : m ⟶ n),
      Functor.HasCoverPullbacks (F.map f).toFunctor (Cov m) (Cov n)) :
    IsSite (total F Cov)
Tag 09WE, a situation

Tag 09WE in the Stacks Project.

CategoryTheory.SimplicialSiteSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/Situation.lean, line 89. The attribute's comment: “the two cases”.

The standing simplicial-site situation of Stacks 09WE. The left summand is case (A), in which transitions are morphisms of sites represented by continuous functors; the right summand is case (B), in which transitions are cocontinuous functors satisfying property P.

structure SimplicialSiteSituation

CategoryTheory.SimplicialSiteSituation.transitionMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/Situation.lean, line 123. The attribute's comment: “the induced morphisms of topoi”.

The morphism of topoi f_φ : Sh(C_n) → Sh(C_m) induced by a simplex map φ : [m] → [n].

noncomputable def transitionMorphism (S : SimplicialSiteSituation.{u})
    {m n : SimplexCategory} (φ : m ⟶ n) :
    MorphismOfTopoi
      (Sheaf (S.componentTopology n) (Type u))
      (Sheaf (S.componentTopology m) (Type u))

CategoryTheory.SimplicialSiteSituation.totalTopology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/Situation.lean, line 162. The attribute's comment: “the total site”. References: SGA 4 VI (7.4.1), “simplicial case”.

The topology of the total site: it is generated by covering families lying in one simplicial degree.

def totalTopology (S : SimplicialSiteSituation.{u}) :
    GrothendieckTopology S.totalCategory
Tag 09WF, a lemma

Tag 09WF in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.fiberTransitionModules, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/ModuleTransition.lean, line 278. The attribute's comment: “module transition”.

Stacks 09WF for sheaves of modules: the transition f_φ^*ℱₘ ⟶ ℱₙ between the restrictions of a sheaf of O-modules to the components of degrees m and n, obtained as the mate of the direct-image transition under the pullback-pushforward adjunction of the transition morphism of ringed topoi. This is the map the source writes f_φ^*ℱₘ → ℱₙ.

noncomputable def fiberTransitionModules (M : SheafOfModules.{u} (S.totalRingSheaf O)) :
    ((S.transitionRingedToposHom O φ).toModulesHom.pullbackModules).obj
        ((S.componentModuleRestriction (S.totalRingSheaf O) m).obj M) ⟶
      (S.componentModuleRestriction (S.totalRingSheaf O) n).obj M

CategoryTheory.SimplicialSiteSituation.fiberTransitionModules_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/ModuleTransitionCocycle.lean, line 119. The attribute's comment: “the unit law for the transition of modules”.

Stacks 09WF for sheaves of modules: the unit law. The transition of the restrictions of a sheaf of O-modules attached to an identity simplex map is the canonical identification of f_𝟙^* with the identity functor.

theorem fiberTransitionModules_id (n : SimplexCategory)
    (M : SheafOfModules.{u} (S.totalRingSheaf O)) :
    S.fiberTransitionModules O (𝟙 n) M =
      (S.transitionPullbackModulesIdIso O n).hom.app
        ((S.componentModuleRestriction (S.totalRingSheaf O) n).obj M)

CategoryTheory.SimplicialSiteSituation.fiberTransitionModules_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/ModuleTransitionCocycle.lean, line 246. The attribute's comment: “the cocycle law for the transition of modules”.

Stacks 09WF for sheaves of modules: the cocycle law. The transition of the restrictions of a sheaf of O-modules attached to a composite simplex map is the composite of the two transitions, compared by the pullback compositor of Stacks 09WE.

theorem fiberTransitionModules_comp {l m n : SimplexCategory} (ψ : l ⟶ m) (φ : m ⟶ n)
    (M : SheafOfModules.{u} (S.totalRingSheaf O)) :
    S.fiberTransitionModules O (ψ ≫ φ) M =
      (S.transitionPullbackModulesCompIso O ψ φ).hom.app
          ((S.componentModuleRestriction (S.totalRingSheaf O) l).obj M) ≫
        (S.transitionRingedToposHom O φ).toModulesHom.pullbackModules.map
            (S.fiberTransitionModules O ψ M) ≫
          S.fiberTransitionModules O φ M

CategoryTheory.SimplicialSiteSituation.totalPresentation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/Descent.lean, line 774. The attribute's comment: “equivalence of categories”.

Stacks 09WF. The presentation of the sheaves on the total site as systems on the component topoi, with no hypotheses: the system of restrictions is an equivalence. The equivalence Sh(C_total) ≌ SimplicialSheafSystem (componentPseudofunctor S) of the tag is its totalEquivalence field.

noncomputable def totalPresentation (S : SimplicialSiteSituation.{u}) :
    SimplicialSheafPresentation S

CategoryTheory.SimplicialSiteSituation.totalPresentation_transition_restriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/Descent.lean, line 782. The attribute's comment: “transition by restriction”.

Stacks 09WF. The transition of the system attached to a sheaf on the total site is the inverse-image transition of its restrictions: under the identification of the components of the system with those restrictions, transition is fiberTransition.

theorem totalPresentation_transition_restriction (S : SimplicialSiteSituation.{u})
    (F : Sheaf S.totalTopology (Type u)) {m n : SimplexCategory} (φ : m ⟶ n) :
    (totalPresentation S).transition F φ ≫
        ((totalPresentation S).componentRestrictionIso F n).hom =
      (S.transitionMorphism φ).inverseImage.map
          ((totalPresentation S).componentRestrictionIso F m).hom ≫
        (S.fiberTransition φ).app F

CategoryTheory.SimplicialSiteSituation.fiberRestrictionData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/FiberRestriction.lean, line 325. The attribute's comment: “fibre restrictions and their specified transitions”.

Stacks Project, Tag 09WF. The fibre restrictions of a sheaf on the total site of a simplicial site, together with their specified transitions.

noncomputable def fiberRestrictionData (S : SimplicialSiteSituation.{u}) :
    FiberRestrictionData S

CategoryTheory.SimplicialSiteSituation.fiberTransition, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RestrictTransition.lean, line 249. The attribute's comment: “transition induced by total-site restriction”.

Stacks 09WF. The inverse-image transition on the restrictions of a total-site sheaf: the mate of restrictTransition under the topos adjunction of f_φ.

noncomputable def fiberTransition (S : SimplicialSiteSituation.{u})
    {m n : SimplexCategory} (φ : m ⟶ n) :
    S.restrict m ⋙ (S.transitionMorphism φ).inverseImage ⟶ S.restrict n

CategoryTheory.SimplicialSiteSituation.SimplicialSheafPresentation.systemTransition_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/Sheaves.lean, line 224. The attribute's comment: “identity transitions”.

The lax unit law of a system, read off on the component in degree n.

public theorem systemTransition_id {S : SimplicialSiteSituation.{u}}
    (P : SimplicialSheafPresentation S) (F : SimplicialSheafSystem P.diagram)
    (n : SimplexCategory) :
    P.systemTransition F (𝟙 n) =
      (canonicalIdentityComparison S n).hom.app (P.systemComponent F n)

CategoryTheory.SimplicialSiteSituation.SimplicialSheafPresentation.systemTransition_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/Sheaves.lean, line 264. The attribute's comment: “composition of transitions”.

The lax composition law of a system, read off on the component in degree l: the transition attached to a composite simplex map is the composite of the two transitions, compared by the canonical inverse-image compositor.

public theorem systemTransition_comp {S : SimplicialSiteSituation.{u}}
    (P : SimplicialSheafPresentation S) (F : SimplicialSheafSystem P.diagram)
    {l m n : SimplexCategory} (ψ : l ⟶ m) (φ : m ⟶ n) :
    P.systemTransition F (ψ ≫ φ) =
      (canonicalCompositionComparison S ψ φ).hom.app (P.systemComponent F l) ≫
        (S.transitionMorphism φ).inverseImage.map (P.systemTransition F ψ) ≫
          P.systemTransition F φ

Declarations registered for the tag:

Tag 09WG, a lemma

Tag 09WG in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.componentLowerShriek_preservesLimitsOfShape, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/ComponentConnectedLimits.lean, line 77. The attribute's comment: “sheaf_connected_limits”.

Stacks 09WG (4). Lower shriek from one component of a simplicial site to the total site commutes with finite connected limits.

theorem componentLowerShriek_preservesLimitsOfShape (S : SimplicialSiteSituation.{u})
    (n : SimplexCategory) (L : Type) [SmallCategory L] [FinCategory L] [IsConnected L] :
    PreservesLimitsOfShape L (componentLowerShriek.{u, u} S n)

CategoryTheory.SimplicialSiteSituation.componentLowerShriek_exactFunctor, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/ComponentExact.lean, line 384. The attribute's comment: “abelian_exact”.

Stacks 09WG (7) for an arbitrary simplicial-site situation: lower shriek from a simplicial component is exact on abelian sheaves.

The coefficients here are the abelian groups of the site's own universe. The source says nothing about universes, and the independent coefficient universe is not reachable: in case (A) the isMorphismOfSites field of CategoryTheory.SimplicialSite fixes the sheaf-value universe of CategoryTheory.Functor.IsMorphismOfSites to the site universe, so Situation 09WE supplies no morphism of topoi at any other, and Stacks 04JC — which is the source's own Case A argument — has no input there.

This declaration carries the tag. An independent coefficient universe is not part of what Stacks 09WG asserts, on three grounds: the source states clause (7) as "\(g_{n!}\) is exact" with no universe quantifier at all; clause (6), Stmt_09WG__abelian_sum_formula, which is the stated input of clause (7)'s one-sentence proof, is stated with universe u only and has its conclusion at Ab.{u}; and the extra universe is unreachable from the data Situation 09WE carries, as the paragraph above establishes. So the statement proved here is the source's clause (7).

The neighbouring clause 09WH__component_injective is different: its case (A) is not proved here at all, and whether ComponentInjective/ComponentKInjective generalise is open. The two are not symmetric — case (A) of clause (7) is proved above.

lemma componentLowerShriek_exactFunctor (S : SimplicialSiteSituation.{u})
    (n : SimplexCategory) :
    exactFunctor
      (Sheaf (S.componentTopology n) Ab.{u})
      (Sheaf S.totalTopology Ab.{u})
      (sheafPullbackConstruction.sheafPullback (componentFunctor S n) Ab.{u}
        (S.componentTopology n) S.totalTopology)

CategoryTheory.SimplicialSiteSituation.componentFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/ComponentInclusion.lean, line 176. The attribute's comment: “component_inclusion”.

Stacks 09WG. The canonical inclusion of the category in simplicial degree n into the total category.

def componentFunctor (S : SimplicialSiteSituation.{u}) (n : SimplexCategory) :
    S.component n ⥤ S.totalCategory

CategoryTheory.SimplicialSiteSituation.componentFunctor_isCocontinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/ComponentInclusion.lean, line 184. The attribute's comment: “component_inclusion”.

Stacks 09WG. The inclusion of a component in the total site is cocontinuous.

instance componentFunctor_isCocontinuous (S : SimplicialSiteSituation.{u})
    (n : SimplexCategory) :
    (componentFunctor S n).IsCocontinuous (S.componentTopology n) S.totalTopology

CategoryTheory.SimplicialSiteSituation.componentFunctor_pullbacksPreservedBy_inl, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/ComponentInclusion.lean, line 252. The attribute's comment: “component_inclusion”.

Stacks 09WG, case (A). The inclusion of a component into the total category preserves the pullback of any two members of a covering family of that component.

This is the pullback clause of the continuity criterion of Stacks 00WW for the component inclusion, and it is what CategoryTheory.SimplicialSiteSituation.componentFunctor_isContinuous feeds to that criterion in case (A). It is stated separately because a functor out of the total category also needs it: for a morphism between simplicial sites in the continuous case, the functor between the total categories is continuous because the component inclusions are, and the argument goes through the preserved pullback of this lemma rather than through continuity itself.

theorem componentFunctor_pullbacksPreservedBy_inl (C : SimplicialSite.{u})
    (n : SimplexCategory) :
    (C.coverage n).PullbacksPreservedBy
      (componentFunctor (⟨Sum.inl C⟩ : SimplicialSiteSituation.{u}) n)

CategoryTheory.SimplicialSiteSituation.componentFunctor_isContinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/ComponentInclusion.lean, line 260. The attribute's comment: “component_inclusion”. References: SGA 4 VI (7.4.4), “1)”.

Stacks 09WG. The inclusion of a component in the total site is continuous.

instance componentFunctor_isContinuous (S : SimplicialSiteSituation.{u})
    (n : SimplexCategory) :
    (componentFunctor S n).IsContinuous (S.componentTopology n) S.totalTopology

CategoryTheory.SimplicialSiteSituation.componentMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/ComponentInclusion.lean, line 383. The attribute's comment: “component_inclusion”.

Stacks 09WG. The morphism g_n : Sh(C_n) ⟶ Sh(C_total) induced by the cocontinuous component inclusion.

noncomputable def componentMorphism (S : SimplicialSiteSituation.{u}) (n : SimplexCategory)
    [(componentFunctor S n).IsCocontinuous (S.componentTopology n) S.totalTopology] :
    MorphismOfTopoi
      (Sheaf (S.componentTopology n) (Type u))
      (Sheaf S.totalTopology (Type u))

CategoryTheory.SimplicialSiteSituation.componentLowerShriek, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/ComponentInclusion.lean, line 400. The attribute's comment: “sheaf_left_adjoint”.

The lower-shriek functor from sheaves on a simplicial component to sheaves on the total site.

noncomputable def componentLowerShriek (S : SimplicialSiteSituation.{u}) (n : SimplexCategory)
    [HasWeakSheafify S.totalTopology (Type w)]
    [∀ G : (S.component n)ᵒᵖ ⥤ Type w, (componentFunctor S n).op.HasLeftKanExtension G] :
    Sheaf (S.componentTopology n) (Type w) ⥤ Sheaf S.totalTopology (Type w)

CategoryTheory.SimplicialSiteSituation.componentLowerShriek_adjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/ComponentInclusion.lean, line 420. The attribute's comment: “sheaf_left_adjoint”.

The lower-shriek functor is left adjoint to inverse image along the morphism of topoi associated to a simplicial component.

noncomputable def componentLowerShriek_adjunction (S : SimplicialSiteSituation.{u})
    (n : SimplexCategory) :
    componentLowerShriek.{u, u} S n ⊣ (componentMorphism S n).inverseImage

CategoryTheory.SimplicialSiteSituation.componentLowerShriek_restrictIsoCoproduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/ComponentSheafSumFormula.lean, line 241. The attribute's comment: “sheaf_coproduct_formula”.

Stacks 09WG, the sheaf coproduct formula. On a simplicial site, the degree-m restriction of lower shriek from degree n of a sheaf of sets is the coproduct, over the simplex maps φ : [n] ⟶ [m], of the inverse images of that sheaf along the transitions.

noncomputable def componentLowerShriek_restrictIsoCoproduct (n m : SimplexCategory)
    (G : Sheaf (S.componentTopology n) (Type u)) :
    (componentMorphism S m).inverseImage.obj ((componentLowerShriek.{u, u} S n).obj G) ≅
      ∐ fun φ : n ⟶ m => (S.transitionMorphism φ).inverseImage.obj G

CategoryTheory.SimplicialSiteSituation.componentLowerShriekRestrictionIsoCoproduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/ComponentSumFormula.lean, line 189. The attribute's comment: “abelian_sum_formula”.

Stacks 09WG, the abelian sum formula. On a simplicial site, lower shriek on abelian sheaves from simplicial degree n, restricted back to degree m, is naturally the direct sum over the simplex maps φ : [n] ⟶ [m] of the inverse images along the transitions.

noncomputable def componentLowerShriekRestrictionIsoCoproduct
    (S : SimplicialSiteSituation.{u}) (n m : SimplexCategory) :
    sheafPullbackConstruction.sheafPullback (componentFunctor S n) Ab.{u}
        (S.componentTopology n) S.totalTopology ⋙
      (componentFunctor S m).sheafPushforwardContinuous Ab.{u}
        (S.componentTopology m) S.totalTopology ≅
      ∐ fun φ : n ⟶ m => transitionInverseImageAb S φ

Declarations registered for the tag:

Tag 09WH, a lemma

Tag 09WH in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.injective_componentRestriction, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/ComponentInjective.lean, line 69. The attribute's comment: “component_injective”.

Stacks 09WH, first assertion: the restriction of an injective abelian sheaf on the total site of a simplicial-site situation to a component is injective.

Restriction to the component is right adjoint to lower shriek, which is exact by CategoryTheory.SimplicialSiteSituation.componentLowerShriek_exactFunctor and so preserves monomorphisms; Mathlib's CategoryTheory.Adjunction.map_injective is then the Homology 015Z step. Exactness holds for an arbitrary situation, so no case distinction is made.

Coefficients sit at the site universe: at an independent coefficient universe the adjunction used here is not available from the data of a situation, since neither HasLeftKanExtension nor HasWeakSheafify S.totalTopology Ab holds there in general.

lemma injective_componentRestriction (S : SimplicialSiteSituation.{u}) (n : SimplexCategory)
    (Inj : Sheaf S.totalTopology Ab.{u}) [Injective Inj] :
    Injective ((S.restrictAb n).obj Inj)

CategoryTheory.SimplicialSiteSituation.isKInjective_componentRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/ComponentKInjective.lean, line 67. The attribute's comment: “component_k_injective”.

Stacks 09WH, second assertion: restriction of a K-injective complex of abelian sheaves on the total site of a simplicial-site situation to a component is K-injective.

Restriction to the component is right adjoint to lower shriek, which is exact by CategoryTheory.SimplicialSiteSituation.componentLowerShriek_exactFunctor, and CochainComplex.isKInjective_mapHomologicalComplex_of_exact is the Stacks 08BJ step. Exactness is available for an arbitrary situation, so no case distinction is made.

Coefficients sit at the site universe, as in the first assertion and for the same reason.

theorem isKInjective_componentRestriction (S : SimplicialSiteSituation.{u})
    (n : SimplexCategory)
    (I : CochainComplex (Sheaf S.totalTopology Ab.{u}) ℤ) [I.IsKInjective] :
    CochainComplex.IsKInjective
      (((S.restrictAb n).mapHomologicalComplex
          (ComplexShape.up ℤ)).obj I)
Sources
LeanCategoryTheory.SimplicialSite.totalCoverage_hasPullbacks · CategoryTheory.SimplicialSite.totalCoverage_isStableUnderBaseChange · CategoryTheory.Pseudofunctor.CoGrothendieck · CategoryTheory.Pseudofunctor.CoGrothendieck.Hom · CategoryTheory.Pseudofunctor.CoGrothendieck.category · CategoryTheory.SimplicialSite.totalCoverage · CategoryTheory.SimplicialSite.totalCoverage_hasIsos · CategoryTheory.SimplicialSite.totalCoverage_isStableUnderComposition

Section85.4 Augmentations of simplicial sites#

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

Tag 0D6Z, a remark

Tag 0D6Z in the Stacks Project.

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

Stacks 0D6Z. An augmentation of a simplicial site towards (D, K). In case (A) it is a morphism of sites represented by a continuous functor in the opposite direction; in case (B) it is represented by a cocontinuous functor. In either case its composite with a vertex functor is independent of the chosen vertex.

def Augmentation (S : SimplicialSiteSituation.{u}) (D : Cat.{u, u})
    (K : GrothendieckTopology D) : Type u
Tag 0D70, a lemma

Tag 0D70 in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.Augmentation.componentAugmentation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/AugmentationPushforward.lean, line 168. The attribute's comment: “part (1): the morphisms of topoi of the components”.

Stacks 0D70, part (1). The morphism of topoi from the sheaves on the component in simplicial degree n to the sheaves on the augmentation site, obtained by composing the degree-zero morphism of the augmentation with the transition morphism of a vertex.

public noncomputable def componentAugmentation (n : SimplexCategory) :
    MorphismOfTopoi (Sheaf (S.componentTopology n) (Type u)) (Sheaf K (Type u))

CategoryTheory.SimplicialSiteSituation.Augmentation.transitionPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/AugmentationPushforward.lean, line 302. The attribute's comment: “compatibility (1): composition with a simplicial transition”.

Stacks 0D70, compatibility (1). Composing the direct image of a simplicial transition with the direct image of the component augmentation of its target agrees canonically with the direct image of the component augmentation of its source.

public noncomputable def transitionPushforwardIso {m n : SimplexCategory} (φ : m ⟶ n) :
    (S.transitionMorphism φ).pushforward ⋙
        (componentAugmentation S D K a m).pushforward ≅
      (componentAugmentation S D K a n).pushforward

CategoryTheory.SimplicialSiteSituation.Augmentation.totalPushforwardForkIsLimit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/TotalAugmentationEqualizer.lean, line 92. The attribute's comment: “compatibility (3): the total direct image is the equalizer”.

Stacks 0D70, compatibility (3). For a sheaf F on the total site, the direct image a_* F along the total augmentation is the equalizer of the two maps a_{0,*} F_0 ⟶ a_{1,*} F_1 attached to the two maps [0] ⟶ [1].

def totalPushforwardForkIsLimit (F : Sheaf S.totalTopology (Type u)) :
    IsLimit (totalPushforwardFork S D K a F)

CategoryTheory.SimplicialSiteSituation.Augmentation.totalMorphismOfTopoi, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/TotalAugmentationMorphism.lean, line 768. The attribute's comment: “part (2): the morphism of topoi of the total site”.

Stacks 0D70, part (2). The morphism of topoi from the sheaves on the total site to the sheaves on the augmentation site induced by an augmentation: its inverse image is the descent of the inverse images along the component augmentations, its direct image is the limit of the cosimplicial sheaf of their direct images, and the two are adjoint.

def totalMorphismOfTopoi :
    MorphismOfTopoi (Sheaf S.totalTopology (Type u)) (Sheaf K (Type u))

CategoryTheory.SimplicialSiteSituation.Augmentation.totalMorphismOfTopoi_componentMorphism_iso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/TotalAugmentationMorphism.lean, line 790. The attribute's comment: “compatibility (2): composition with a component inclusion”.

Stacks 0D70, compatibility (2), in inverse images. The inverse image of the total augmentation followed by the inverse image of the morphism of topoi which Stacks 09WG attaches to the simplicial degree n is the inverse image of the augmentation of that degree: the augmentation of a simplicial degree is the total augmentation composed with that morphism.

def totalMorphismOfTopoi_componentMorphism_iso (n : SimplexCategory) :
    (totalMorphismOfTopoi S D K a).inverseImage ⋙ (componentMorphism S n).inverseImage ≅
      (componentAugmentation S D K a n).inverseImage
Sources
LeanCategoryTheory.SimplicialSiteSituation.Augmentation · CategoryTheory.SimplicialSiteSituation.Augmentation.componentAugmentation · CategoryTheory.SimplicialSiteSituation.Augmentation.transitionPushforwardIso · CategoryTheory.SimplicialSiteSituation.Augmentation.totalPushforwardForkIsLimit · CategoryTheory.SimplicialSiteSituation.Augmentation.totalMorphismOfTopoi · CategoryTheory.SimplicialSiteSituation.Augmentation.totalMorphismOfTopoi_componentMorphism_iso

Section85.5 Morphisms of simplicial sites#

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

Tag 0D95, a remark

Tag 0D95 in the Stacks Project.

CategoryTheory.SimplicialSiteMorphism, an inductive in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/Morphism.lean, line 91. The attribute's comment: “morphism_between_simplicial_sites”.

Stacks 0D95. A morphism between simplicial sites: degreewise morphisms of sites commuting with the transitions in case (A), or degreewise cocontinuous functors commuting with the transitions in case (B).

inductive SimplicialSiteMorphism :
    SimplicialSiteSituation.{u} → SimplicialSiteSituation.{u} → Type (u + 1)

CategoryTheory.SimplicialSiteMorphism.transitionPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/Morphism.lean, line 126.

Stacks 0D95. The component morphisms of a morphism between simplicial sites commute, up to the canonical comparison, with every simplicial transition morphism of topoi.

noncomputable def transitionPushforwardIso
    {S S' : SimplicialSiteSituation.{u}}
    (h : SimplicialSiteMorphism S S')
    {m n : SimplexCategory} (φ : m ⟶ n) :
    (h.componentMorphism n).pushforward ⋙ (S'.transitionMorphism φ).pushforward ≅
      (S.transitionMorphism φ).pushforward ⋙ (h.componentMorphism m).pushforward
Tag 0D96, a lemma

Tag 0D96 in the Stacks Project.

CategoryTheory.SimplicialSite.Morphism.totalFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/TotalContinuousFunctor.lean, line 86. The attribute's comment: “case (A), the functor of total sites”.

The functor between the total categories attached to a morphism between simplicial sites in the continuous case: in each simplicial degree it is the given functor.

def totalFunctor (h : SimplicialSite.Morphism C C') :
    CoGrothendieck C'.totalPseudofunctor ⥤ CoGrothendieck C.totalPseudofunctor

CategoryTheory.SimplicialSite.Morphism.totalFunctor_isContinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/TotalContinuousFunctor.lean, line 193. The attribute's comment: “case (A), continuity of the functor of total sites”. References: SGA 4 VI (7.4.9), “simplicial, continuous”.

The functor between the total categories is continuous.

theorem totalFunctor_isContinuous (h : SimplicialSite.Morphism C C') :
    h.totalFunctor.IsContinuous C'.totalTopology C.totalTopology

CategoryTheory.CocontinuousSimplicialSite.Morphism.totalMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/TotalMorphism.lean, line 136. The attribute's comment: “case (B), the morphism of total topoi”. References: SGA 4 VI (7.4.9), “simplicial case, m_*”.

The morphism between the total topoi induced by a morphism between simplicial sites in the cocontinuous case.

noncomputable def totalMorphism (h : CocontinuousSimplicialSite.Morphism C C') :
    MorphismOfTopoi
      (Sheaf (⟨Sum.inr C⟩ : SimplicialSiteSituation.{u}).totalTopology (Type u))
      (Sheaf (⟨Sum.inr C'⟩ : SimplicialSiteSituation.{u}).totalTopology (Type u))

CategoryTheory.CocontinuousSimplicialSite.Morphism.totalComponentPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/TotalMorphism.lean, line 154. The attribute's comment: “case (B), the commutative square”.

The square formed by the total morphism of topoi, the morphism of topoi in simplicial degree n, and the two component morphisms of that degree commutes, as witnessed by a natural isomorphism of direct-image functors.

noncomputable def totalComponentPushforwardIso
    (h : CocontinuousSimplicialSite.Morphism C C') (n : SimplexCategory) :
    ((SimplicialSiteMorphism.ofCocontinuous h).componentMorphism n).pushforward ⋙
        (SimplicialSiteSituation.componentMorphism
          (⟨Sum.inr C'⟩ : SimplicialSiteSituation.{u}) n).pushforward ≅
      (SimplicialSiteSituation.componentMorphism
          (⟨Sum.inr C⟩ : SimplicialSiteSituation.{u}) n).pushforward ⋙
        h.totalMorphism.pushforward

CategoryTheory.CocontinuousSimplicialSite.Morphism.totalInverseImageRestrictIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/TotalMorphism.lean, line 198. The attribute's comment: “case (B), restriction of the inverse image”. References: SGA 4 VI (7.4.9), “simplicial, f^{-1}”.

Stacks 0D96, case (B). Inverse image to the component of simplicial degree n, applied to the inverse image along the total morphism, is the inverse image in degree n applied to the inverse image to the component of that degree: h_total^{-1} is degreewise h_n^{-1}.

The two composites of inverse images are the left adjoints of the two composites of direct images compared by totalComponentPushforwardIso, so this is that comparison conjugated by uniqueness of left adjoints.

noncomputable def totalInverseImageRestrictIso
    (h : CocontinuousSimplicialSite.Morphism C C') (n : SimplexCategory) :
    h.totalMorphism.inverseImage ⋙
        (SimplicialSiteSituation.componentMorphism
          (⟨Sum.inr C⟩ : SimplicialSiteSituation.{u}) n).inverseImage ≅
      (SimplicialSiteSituation.componentMorphism
          (⟨Sum.inr C'⟩ : SimplicialSiteSituation.{u}) n).inverseImage ⋙
        ((SimplicialSiteMorphism.ofCocontinuous h).componentMorphism n).inverseImage

CategoryTheory.CocontinuousSimplicialSite.Morphism.totalPushforwardRestrictIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/TotalMorphism.lean, line 219. The attribute's comment: “case (B), restriction of the direct image”. References: SGA 4 VI (7.4.9), “simplicial, (7.4.9.2)”.

Inverse image to the component of simplicial degree n, applied to the direct image along the total morphism, is the direct image in degree n applied to the inverse image to the component of that degree.

noncomputable def totalPushforwardRestrictIso
    (h : CocontinuousSimplicialSite.Morphism C C') (n : SimplexCategory) :
    h.totalMorphism.pushforward ⋙
        (SimplicialSiteSituation.componentMorphism
          (⟨Sum.inr C'⟩ : SimplicialSiteSituation.{u}) n).inverseImage ≅
      (SimplicialSiteSituation.componentMorphism
          (⟨Sum.inr C⟩ : SimplicialSiteSituation.{u}) n).inverseImage ⋙
        ((SimplicialSiteMorphism.ofCocontinuous h).componentMorphism n).pushforward

CategoryTheory.SimplicialSite.Morphism.totalInverseImageRestrictIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/TotalMorphismCaseA.lean, line 380. The attribute's comment: “case (A), restriction of the inverse image”. References: SGA 4 VI (7.4.9), “simplicial, f^{-1}”.

Stacks 0D96, case (A). Restriction to the component of simplicial degree n, applied to the inverse image along the total morphism, is the inverse image in degree n applied to restriction to the component of that degree: h_total^{-1} is degreewise h_n^{-1}.

def totalInverseImageRestrictIso (h : SimplicialSite.Morphism C C') (n : SimplexCategory) :
    h.totalInverseImage ⋙ restrict (⟨Sum.inl C⟩ : SimplicialSiteSituation.{u}) n ≅
      restrict (⟨Sum.inl C'⟩ : SimplicialSiteSituation.{u}) n ⋙ h.componentInverseImage n

CategoryTheory.SimplicialSiteMorphism.totalMorphismSquares, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/TotalMorphismOfTopoi.lean, line 88. The attribute's comment: “the morphism of total topoi, its commutative squares with the component morphisms, and the restriction of its direct image, in both cases”.

Stacks 0D96. A morphism h between simplicial sites, in either case of Stacks 0D95, induces a morphism of topoi h_total : Sh(C_total) → Sh(C'_total) (h.totalMorphism) such that for every n the square formed by h_total, the morphism of topoi h_n of degree n and the morphisms of topoi g_n, g'_n of the component inclusions commutes, and (g'_n)^{-1} ∘ h_{total,*} = h_{n,*} ∘ g_n^{-1}.

def totalMorphismSquares : (h : SimplicialSiteMorphism S S') → h.TotalMorphismSquares
Tag 0D97, a lemma

Tag 0D97 in the Stacks Project.

CategoryTheory.SimplicialSite.Morphism.derivedTotalPushforwardRestrictIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/TotalContinuousMorphismDerivedPushforward.lean, line 344. The attribute's comment: “case (A)”.

For a morphism between simplicial sites built from morphisms of sites (case (A)), and K in the unbounded derived category of abelian sheaves on the total site, (g'_n)^{-1} Rh_{total,*} K = Rh_{n,*} g_n^{-1} K, as a natural isomorphism of functors on the derived categories.

def derivedTotalPushforwardRestrictIso (h : SimplicialSite.Morphism C C')
    (n : SimplexCategory) :
    h.derivedAbelianTotalPushforward ⋙
        (abelianComponent (⟨Sum.inl C'⟩ : SimplicialSiteSituation.{u}) n).mapDerivedCategory ≅
      (abelianComponent (⟨Sum.inl C⟩ : SimplicialSiteSituation.{u}) n).mapDerivedCategory ⋙
        h.derivedAbelianComponentPushforward n

CategoryTheory.CocontinuousSimplicialSite.Morphism.derivedTotalPushforwardRestrictIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/TotalMorphismDerivedPushforward.lean, line 548. The attribute's comment: “case (B)”.

In case (B), with notation and hypotheses as in Stacks 0D96: the natural isomorphism (g'_n)^{-1} Rh_{total,*} K ≅ Rh_{n,*} g_n^{-1} K for K in the unbounded derived category of abelian sheaves on the total site.

def derivedTotalPushforwardRestrictIso (h : CocontinuousSimplicialSite.Morphism C C')
    (n : SimplexCategory) :
    h.derivedAbelianTotalPushforward ⋙
        (abelianComponent (⟨Sum.inr C'⟩ : SimplicialSiteSituation.{u}) n).mapDerivedCategory ≅
      (abelianComponent (⟨Sum.inr C⟩ : SimplicialSiteSituation.{u}) n).mapDerivedCategory ⋙
        h.derivedAbelianComponentPushforward n

CategoryTheory.CocontinuousSimplicialSite.Morphism.derivedTotalPushforwardRestrictIso', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/TotalMorphismDerivedPushforward.lean, line 569. The attribute's comment: “case (B)”.

In case (B), with notation and hypotheses as in Stacks 0D96: the natural isomorphism (g'_n)^{-1} Rh_{total,*} K ≅ Rh_{n,*} g_n^{-1} K for K in the unbounded derived category of abelian sheaves on the total site, with restriction written as CategoryTheory.SimplicialSiteSituation.restrictAb.

def derivedTotalPushforwardRestrictIso' (h : CocontinuousSimplicialSite.Morphism C C')
    (n : SimplexCategory) :
    h.derivedAbelianTotalPushforward ⋙
        (restrictAb (⟨Sum.inr C'⟩ : SimplicialSiteSituation.{u}) n).mapDerivedCategory ≅
      (restrictAb (⟨Sum.inr C⟩ : SimplicialSiteSituation.{u}) n).mapDerivedCategory ⋙
        h.derivedAbelianComponentPushforward n
Tag 0D98, a remark

Tag 0D98 in the Stacks Project.

CategoryTheory.SimplicialSiteMorphism.CompatibleWithAugmentations, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/AugmentedMorphism.lean, line 68. The attribute's comment: “compatibility_with_augmentations”.

Compatibility of a morphism of topoi between augmentation sites with a morphism of simplicial sites and the two augmentations.

def CompatibleWithAugmentations
    {S S' : SimplicialSiteSituation.{u}}
    {D D' : Cat.{u, u}} {K : GrothendieckTopology D}
    {K' : GrothendieckTopology D'}
    (h : SimplicialSiteMorphism S S')
    (a : SimplicialSiteSituation.Augmentation S D K)
    (a' : SimplicialSiteSituation.Augmentation S' D' K')
    (g : MorphismOfTopoi (Sheaf K (Type u)) (Sheaf K' (Type u))) : Prop

CategoryTheory.SimplicialSiteMorphism.augmentationPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/AugmentedMorphism.lean, line 94.

The degree-zero square of a morphism of augmented simplicial sites commutes, as witnessed by a natural isomorphism of direct-image functors.

noncomputable def augmentationPushforwardIso
    {S S' : SimplicialSiteSituation.{u}}
    {D D' : Cat.{u, u}} {K : GrothendieckTopology D}
    {K' : GrothendieckTopology D'}
    (h : SimplicialSiteMorphism S S')
    (a : SimplicialSiteSituation.Augmentation S D K)
    (a' : SimplicialSiteSituation.Augmentation S' D' K')
    (g : MorphismOfTopoi (Sheaf K (Type u)) (Sheaf K' (Type u)))
    (hg : CompatibleWithAugmentations h a a' g) :
    (h.componentMorphism (SimplexCategory.mk 0)).pushforward ⋙
        (SimplicialSiteSituation.Augmentation.morphismOfTopoi S' D' K' a').pushforward ≅
      (SimplicialSiteSituation.Augmentation.morphismOfTopoi S D K a).pushforward ⋙
        g.pushforward
Tag 0D99, a lemma

Tag 0D99 in the Stacks Project.

CategoryTheory.SimplicialSiteMorphism.totalAugmentationPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/AugmentedTotalMorphismSquare.lean, line 245.

Stacks 0D99. Let h be a morphism between simplicial sites (Stacks 0D95), in either case of Stacks 09WE, let a, a' be augmentations of its source and target towards sites D, D' (Stacks 0D6Z), and let g : Sh(D) → Sh(D') be a morphism of topoi compatible with h, a, a' (Stacks 0D98). Then the square formed by the morphism of total topoi h_total (Stacks 0D96), the morphisms of topoi a : Sh(C_total) → Sh(D) and a' : Sh(C'_total) → Sh(D') of the total augmentations (Stacks 0D70) and g commutes: a' ∘ h_total = g ∘ a, as witnessed by a natural isomorphism of direct-image functors.

def totalAugmentationPushforwardIso {S S' : SimplicialSiteSituation.{u}}
    {D D' : Cat.{u, u}} {K : GrothendieckTopology D} {K' : GrothendieckTopology D'}
    (h : SimplicialSiteMorphism S S')
    (a : SimplicialSiteSituation.Augmentation S D K)
    (a' : SimplicialSiteSituation.Augmentation S' D' K')
    (g : MorphismOfTopoi (Sheaf K (Type u)) (Sheaf K' (Type u)))
    (hg : h.CompatibleWithAugmentations a a' g) :
    h.totalMorphism.pushforward ⋙
        (SimplicialSiteSituation.Augmentation.totalMorphismOfTopoi S' D' K' a').pushforward ≅
      (SimplicialSiteSituation.Augmentation.totalMorphismOfTopoi S D K a).pushforward ⋙
        g.pushforward

CategoryTheory.CocontinuousSimplicialSite.Morphism.totalAugmentationPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/TotalAugmentedMorphism.lean, line 159.

Stacks 0D99. Let a morphism between simplicial sites, augmentations of its source and its target, and a morphism of the augmentation topoi compatible with them be given. Then the square formed by the total topoi, the augmentation topoi, the total morphism of the simplicial sites and that morphism of the augmentation topoi commutes, as witnessed by a natural isomorphism of direct-image functors.

noncomputable def totalAugmentationPushforwardIso
    (h : CocontinuousSimplicialSite.Morphism C C')
    (a : C.Augmentation D K) (a' : C'.Augmentation D' K')
    (g : MorphismOfTopoi (Sheaf K (Type u)) (Sheaf K' (Type u)))
    (hg : SimplicialSiteMorphism.CompatibleWithAugmentations
      (SimplicialSiteMorphism.ofCocontinuous h) a a' g) :
    h.totalMorphism.pushforward ⋙ (Augmentation.totalMorphismOfTopoi a').pushforward ≅
      (Augmentation.totalMorphismOfTopoi a).pushforward ⋙ g.pushforward
Sources
LeanCategoryTheory.SimplicialSiteMorphism · CategoryTheory.SimplicialSiteMorphism.transitionPushforwardIso · CategoryTheory.SimplicialSite.Morphism.totalFunctor · CategoryTheory.SimplicialSite.Morphism.totalFunctor_isContinuous · CategoryTheory.CocontinuousSimplicialSite.Morphism.totalMorphism · CategoryTheory.CocontinuousSimplicialSite.Morphism.totalComponentPushforwardIso · CategoryTheory.CocontinuousSimplicialSite.Morphism.totalInverseImageRestrictIso · CategoryTheory.CocontinuousSimplicialSite.Morphism.totalPushforwardRestrictIso

Section85.6 Ringed simplicial sites#

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

Tag 0D72, a lemma

Tag 0D72 in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.componentRingedTopos_restrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/Basic.lean, line 134. The attribute's comment: “component_ringed_topos”.

The inverse image of sheaves of commutative rings along the component morphism of topoi is canonically and naturally isomorphic to restriction along the component inclusion.

noncomputable def componentRingedTopos_restrictionIso (S : SimplicialSiteSituation.{u})
    (n : SimplexCategory) :
    inverseImageCommRingFunctor (J := S.componentTopology n) (K := S.totalTopology)
        (componentMorphism S n) ≅
      (componentFunctor S n).sheafPushforwardContinuous CommRingCat.{u}
        (S.componentTopology n) S.totalTopology

CategoryTheory.SimplicialSiteSituation.componentRingedTopos_restrictionIso_forget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/Basic.lean, line 148. The attribute's comment: “component_ringed_topos”.

The restriction isomorphism is the canonical comparison of Stacks 09WG after forgetting the ring operations. In particular its scalar map is not an arbitrary natural automorphism of restriction.

theorem componentRingedTopos_restrictionIso_forget (S : SimplicialSiteSituation.{u})
    (n : SimplexCategory) (O : Sheaf S.totalTopology CommRingCat.{u}) :
    (sheafCompose (S.componentTopology n) (forget CommRingCat.{u})).map
        ((componentRingedTopos_restrictionIso S n).hom.app O) =
      (inverseImageCommRingForgetIso (S.componentTopology n)
          (componentMorphism S n)).hom.app O ≫
        ((componentFunctor S n).sheafPullbackCocontinuousIsoSheafPushforwardContinuous
          (Type u) (S.componentTopology n) S.totalTopology).hom.app
          ((sheafCompose S.totalTopology (forget CommRingCat.{u})).obj O)

CategoryTheory.SimplicialSiteSituation.componentRingedToposHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/Basic.lean, line 166. The attribute's comment: “component_ringed_topos”.

The canonical morphism of ringed topoi from a simplicial component to the total site. Its structure map is the adjoint of the comparison gₙ⁻¹O ⟶ Oₙ of structure sheaves.

noncomputable def componentRingedToposHom (S : SimplicialSiteSituation.{u})
    (O : Sheaf S.totalTopology CommRingCat.{u}) (n : SimplexCategory) :
    RingedToposHom (componentRingedTopos S O n) (totalRingedTopos S O)

CategoryTheory.SimplicialSiteSituation.componentRingedToposHom_toToposHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/Basic.lean, line 176. The attribute's comment: “component_ringed_topos”.

The underlying geometric morphism is the component morphism of Stacks 09WG.

theorem componentRingedToposHom_toToposHom (S : SimplicialSiteSituation.{u})
    (O : Sheaf S.totalTopology CommRingCat.{u}) (n : SimplexCategory) :
    (componentRingedToposHom S O n).toToposHom = componentMorphism S n

CategoryTheory.SimplicialSiteSituation.moduleSumFormulaLegEq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/CartesianDerivedModuleOfModuleSystem.lean, line 72. The attribute's comment: “the summand inclusions of the direct-sum formula on sheaves of modules are the canonical maps f_φ^G ⟶ g_m^g_{n!}G, in Situation 09WE (both cases)”.

The leg equation of Stacks 0D72 (6) in every simplicial-site situation. For every simplex map φ : [n] ⟶ [m] the φth summand inclusion of the componentwise direct-sum formula for sheaves of modules, followed by the inverse of that formula, is the canonical map attached to φ. In case (A) of Stacks 09WE this is CategoryTheory.SimplicialSite.moduleSumFormulaLegEq_situation, and in case (B) it is CategoryTheory.CocontinuousSimplicialSite.moduleSumFormulaLegEqB.

theorem moduleSumFormulaLegEq : S.ModuleSumFormulaLegEq O

CategoryTheory.SimplicialSiteSituation.componentRingedToposHom_fSharpInverseImageRing_ringSheafMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/ComponentPullbackRestriction.lean, line 107. The attribute's comment: “the structure map of the component morphism on underlying sheaves of sets”.

The inverse-image form of the structure map of g_n on underlying sheaves of sets is the comparison of Stacks 09WG. The structure map is recorded through the adjunction for sheaves of commutative rings and used through the adjunction for sheaves of rings; the two agree on underlying sheaves of sets, where the first is Stacks 09WG by construction of the component ringed topos.

theorem componentRingedToposHom_fSharpInverseImageRing_ringSheafMap :
    (sheafCompose (S.componentTopology n) (forget RingCat.{u})).map
        (componentRingedToposHom S O n).fSharpInverseImageRing =
      (componentRingedTopos_setRestrictionIso S n).hom.app
        ((sheafCompose S.totalTopology (forget CommRingCat.{u})).obj O)

CategoryTheory.SimplicialSiteSituation.componentPullbackModulesRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/ComponentPullbackRestriction.lean, line 171. The attribute's comment: “the pullback of modules along g_n is restriction to the component”.

Stacks 0D72: the pullback of sheaves of modules to a simplicial component is the literal restriction. The two presentations of restriction to the degree-n component that this development carries — pullback of modules along the component morphism of ringed topoi, and restriction of sections along the component inclusion — are canonically isomorphic.

def componentPullbackModulesRestrictionIso :
    (componentRingedToposHom S O n).toModulesHom.pullbackModules ≅
      S.componentModulesRestriction O n

CategoryTheory.SimplicialSiteSituation.componentPullbackModulesRestrictionIso_underlying, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/ComponentPullbackUnderlying.lean, line 210. The attribute's comment: “the comparison of the two presentations of restriction, on underlying sheaves of sets”.

Stacks 0D72 on underlying sheaves of sets is Stacks 09WG. Read through the identification of the underlying sheaf of a pullback of modules with an inverse image, the comparison of Stacks 0D72 between the pullback of sheaves of modules along the component morphism of ringed topoi and the literal restriction to the component is the comparison of Stacks 09WG between the inverse image of sheaves of sets and restriction along the component inclusion.

theorem componentPullbackModulesRestrictionIso_underlying
    (M : SheafOfModules.{u} (S.totalRingSheaf O)) :
    (AlgebraicGeometry.RingedToposHom.pullbackUnderlyingIsoOfIsIso
          (componentRingedToposHom S O n)).inv.app M ≫
        (Sheaf.moduleSheafFunctor
            (Stacks.SheafOfModules.Tensor.ringSheaf (S.componentRingedTopos O n).O)).map
          ((componentPullbackModulesRestrictionIso S O n).hom.app M) =
      (componentRingedTopos_setRestrictionIso S n).hom.app
        (Sheaf.moduleSheaf.{u, u, u} (S.totalRingSheaf O) M)

CategoryTheory.SimplicialSiteSituation.componentPullbackComplexRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/ComponentTensorComplex.lean, line 84. The attribute's comment: “degreewise pullback of complexes along g_n is degreewise restriction”.

Stacks 0D72 on cochain complexes. Degreewise pullback of complexes of modules along the component morphism of ringed topoi is degreewise restriction to the component.

def componentPullbackComplexRestrictionIso :
    Stacks.Sheaves.DerivedPullback.pullbackComplexFunctor
        (X := S.componentRingedTopos O n) (Y := S.totalRingedTopos O)
        (componentRingedToposHom S O n).toModulesHom ≅
      S.componentModulesRestrictionComplex O n

CategoryTheory.SimplicialSiteSituation.componentModuleLowerShriekAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/ModuleLowerShriek.lean, line 128. The attribute's comment: “existence of the left adjoint g_{n!} of g_n^* on modules”.

Stacks 0D72. The defining adjunction g_{n!} ⊣ g_n^* of lower shriek of modules on a simplicial component, exhibiting the left adjoint g_{n!} of g_n^* whose existence the tag asserts.

noncomputable def componentModuleLowerShriekAdjunction :
    componentModuleLowerShriek S O n ⊣ componentModuleRestriction S O n

CategoryTheory.SimplicialSite.componentModuleSumFormulaA, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/ModuleSumFormulaCaseA.lean, line 137. The attribute's comment: “direct-sum formula in case (A), on sheaves of modules”.

Stacks 0D72, the componentwise direct-sum formula for sheaves of modules in case (A). The restriction to simplicial degree m of lower shriek g_{n!} of sheaves of O-modules from degree n is the direct sum, over the simplex maps φ : [n] ⟶ [m], of the pullbacks f_φ^* of sheaves of modules along the transitions, each taken along the ring map O(φ).

def componentModuleSumFormulaA (n m : SimplexCategory) :
    (∐ fun φ : n ⟶ m => transitionModulePullbackA C O φ) ≅
      (situation C).componentModuleLowerShriek O n ⋙
        (situation C).componentModuleRestriction O m

CategoryTheory.CocontinuousSimplicialSite.componentModuleSumFormulaB, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/ModuleSumFormulaCaseB.lean, line 155. The attribute's comment: “direct-sum formula in case (B), on sheaves of modules”.

The componentwise direct-sum formula for sheaves of modules in case (B). The restriction to simplicial degree m of lower shriek g_{n!} of sheaves of O-modules from degree n is the direct sum, over the simplex maps φ : [n] ⟶ [m], of the pullbacks f_φ^* of sheaves of modules along the transitions.

def componentModuleSumFormulaB :
    (∐ fun φ : n ⟶ m => transitionModulePullbackB C P n m φ) ≅
      (situation C).componentModuleLowerShriek (totalRingSheafB C P) n ⋙
        (situation C).componentModuleRestriction (totalRingSheafB C P) m

CategoryTheory.SimplicialSiteSituation.moduleSumFormula, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/ModuleSumFormulaSituation.lean, line 101. The attribute's comment: “direct-sum formula on sheaves of modules, in Situation 09WE (both cases)”.

The componentwise direct-sum formula of Stacks 0D72 (6) for sheaves of modules, for an arbitrary simplicial-site situation and in the summand spelling Stacks 0D74 consumes: the restriction to degree m of lower shriek from degree n is the direct sum, over the simplex maps φ : [n] ⟶ [m], of the pullbacks of sheaves of modules along the transition morphisms of ringed topoi.

A situation is one of the two cases of Stacks 09WE, and the formula is proved in each: CategoryTheory.SimplicialSite.moduleSumFormulaA in case (A), where the transitions are morphisms of sites, and CategoryTheory.CocontinuousSimplicialSite.moduleSumFormulaB in case (B), where they are cocontinuous functors.

def moduleSumFormula : ∀ (S : SimplicialSiteSituation.{u})
    (P : Sheaf S.totalTopology CommRingCat.{u}) (n : SimplexCategory), S.ModuleSumFormula' P n

Stacks.Sites.ComponentModuleSumFormula.colimitPullbackRestrictionIsoCoproduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/ComponentModuleSumFormulaPresheaf.lean, line 220. The attribute's comment: “direct-sum formula in case (B), on presheaves of modules”.

The restriction to simplicial degree m of the presheaf-level module lower shriek from degree n is, as a functor, the direct sum over the simplex maps φ : [n] ⟶ [m] of the presheaf-level module pullbacks f_φ^* along the transitions, the summand labelled φ being the pullback along the transition of φ.

noncomputable def colimitPullbackRestrictionIsoCoproduct :
    Stacks.PullbackColimit.colimitPullback (Grothendieck.ι C.underlying (op n)) R ⋙
        PresheafOfModules.pushforward₀OfCommRingCat
          (Grothendieck.ι C.underlying (op m)) R ≅
      ∐ fun φ : n ⟶ m => transitionPullbackPresheafModules C R φ

CategoryTheory.SimplicialSiteSituation.componentRingedToposHom_fSharpInverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphism.lean, line 711. The attribute's comment: “the structure map of the component morphism, in inverse-image form”.

The structure map of the canonical morphism from a simplicial component to the total ringed topos is, in inverse-image form, the comparison of structure sheaves of Stacks 0D72.

theorem componentRingedToposHom_fSharpInverseImage (S : SimplicialSiteSituation.{u})
    (O : Sheaf S.totalTopology CommRingCat.{u}) (n : SimplexCategory) :
    (componentRingedToposHom S O n).fSharpInverseImage =
      (componentRingedTopos_restrictionIso S n).hom.app O
Tag 0D73, a lemma

Tag 0D73 in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.isTotallyAcyclic_component_of_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/ComponentTotalAcyclicity.lean, line 83.

Stacks Project, Tag 0D73. Let O be a sheaf of rings on the total site of a simplicial-site situation and let I be an injective sheaf of O-modules. The abelian sheaf underlying the restriction I_n of I to the degree-n simplicial component is totally acyclic: its cohomology over every sheaf of sets on C_n vanishes in every positive degree.

theorem isTotallyAcyclic_component_of_injective
    [HasExt.{u} (Sheaf (S.componentTopology n) AddCommGrpCat.{u})]
    [HasExt.{u} (Sheaf S.totalTopology AddCommGrpCat.{u})]
    (O : Sheaf S.totalTopology RingCat.{u}) (I : SheafOfModules.{u} O) [Injective I] :
    IsTotallyAcyclic.{u} (S.componentTopology n)
      ((S.restrictAb n).obj ((SheafOfModules.toSheaf O).obj I))

CategoryTheory.SimplicialSiteSituation.isTotallyAcyclic_componentModule_of_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/ComponentTotalAcyclicity.lean, line 118. The attribute's comment: “the conclusion read on the restricted sheaf of modules rather than on the restriction of the underlying abelian sheaf”.

Stacks Project, Tag 0D73, with the conclusion read on the restricted sheaf of modules. The restriction of an injective sheaf of O-modules to the degree-n simplicial component — reindexing the sections and restricting the scalars along the identity of the restricted sheaf of rings — has totally acyclic underlying abelian sheaf.

theorem isTotallyAcyclic_componentModule_of_injective
    [HasExt.{u} (Sheaf (S.componentTopology n) AddCommGrpCat.{u})]
    [HasExt.{u} (Sheaf S.totalTopology AddCommGrpCat.{u})]
    (O : Sheaf S.totalTopology RingCat.{u}) (I : SheafOfModules.{u} O) [Injective I] :
    IsTotallyAcyclic.{u} (S.componentTopology n)
      ((SheafOfModules.toSheaf _).obj
        ((SheafOfModules.pushforward (F := componentFunctor S n)
          (𝟙 (((componentFunctor S n).sheafPushforwardContinuous RingCat.{u}
            (S.componentTopology n) S.totalTopology).obj O))).obj I))
Tag 0D74, a lemma

Tag 0D74 in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.exactFunctor_componentModuleLowerShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/ModuleLowerShriekExact.lean, line 194. The attribute's comment: “with the componentwise direct-sum formula of Tag 0D72 proved in either case of 09WE”.

Stacks 0D74. Lower shriek g_{n!} of sheaves of modules from the degree-n simplicial component is exact as soon as every structure-sheaf transition f_φ⁻¹O_n ⟶ O_m out of degree n is flat.

Right exactness is formal. For left exactness: the restrictions to the components detect finite limits, the componentwise direct-sum formula of Stacks 0D72 (CategoryTheory.SimplicialSiteSituation.moduleSumFormula) presents the restriction of g_{n!} to degree m as the direct sum over the finitely many simplex maps [n] ⟶ [m] of the transition pullbacks, hence as their product, and each of those is left exact by Stacks 04JC. This is CategoryTheory.SimplicialSiteSituation.exactFunctor_componentModuleLowerShriek'.

theorem exactFunctor_componentModuleLowerShriek
    (hflat : ∀ (m : SimplexCategory) (φ : n ⟶ m), (S.transitionRingedToposHom P φ).IsFlat) :
    exactFunctor
      (SheafOfModules.{u} (S.componentRingSheaf ((Stacks.SheafOfModules.Tensor.ringSheaf (J := S.totalTopology)) P) n))
      (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf (J := S.totalTopology)) P))
      (S.componentModuleLowerShriek ((Stacks.SheafOfModules.Tensor.ringSheaf (J := S.totalTopology)) P) n)

CategoryTheory.SimplicialSiteSituation.exactFunctor_componentModuleLowerShriek', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/ModuleSumFormulaSituation.lean, line 118.

Stacks 0D74. Lower shriek g_{n!} of sheaves of modules from the degree-n simplicial component is exact as soon as every structure-sheaf transition f_φ⁻¹O_n ⟶ O_m out of degree n is flat.

Right exactness is formal. For left exactness: the restrictions to the components detect finite limits, the componentwise direct-sum formula of Stacks 0D72 presents the restriction of g_{n!} to degree m as the direct sum over the finitely many simplex maps [n] ⟶ [m] of the transition pullbacks, hence as their product, and each of those is left exact by Stacks 04JC.

theorem exactFunctor_componentModuleLowerShriek'
    (hflat : ∀ (m : SimplexCategory) (φ : n ⟶ m), (S.transitionRingedToposHom P φ).IsFlat) :
    exactFunctor
      (SheafOfModules.{u} (S.componentRingSheaf
        ((Stacks.SheafOfModules.Tensor.ringSheaf (J := S.totalTopology) P)) n))
      (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf (J := S.totalTopology) P)))
      (S.componentModuleLowerShriek
        ((Stacks.SheafOfModules.Tensor.ringSheaf (J := S.totalTopology) P)) n)
Tag 0D75, a lemma

Tag 0D75 in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.injective_componentModuleRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/ModuleLowerShriekExact.lean, line 227. The attribute's comment: “with the componentwise direct-sum formula of Tag 0D72 proved in either case of 09WE”.

Stacks 0D75. Let O be a sheaf of rings on the total site whose structure-sheaf transitions f_φ⁻¹O_n ⟶ O_m out of degree n are flat. An injective sheaf of O-modules restricts to an injective sheaf of O_n-modules on the degree-n simplicial component.

Restriction is right adjoint to g_{n!}, which is exact by Stacks 0D74, so Homology 015Z applies; the componentwise direct-sum formula of Tag 0D72 that Stacks 0D74 starts from is CategoryTheory.SimplicialSiteSituation.moduleSumFormula.

theorem injective_componentModuleRestriction
    (hflat : ∀ (m : SimplexCategory) (φ : n ⟶ m), (S.transitionRingedToposHom P φ).IsFlat)
    (I : SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf (J := S.totalTopology)) P)) [Injective I] :
    Injective ((S.componentModuleRestriction ((Stacks.SheafOfModules.Tensor.ringSheaf (J := S.totalTopology)) P) n).obj I)

CategoryTheory.SimplicialSiteSituation.injective_componentModuleRestriction', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/ModuleSumFormulaSituation.lean, line 177.

Stacks 0D75. Let O be a sheaf of rings on the total site whose structure-sheaf transitions f_φ⁻¹O_n ⟶ O_m out of degree n are flat. An injective sheaf of O-modules restricts to an injective sheaf of O_n-modules on the degree-n simplicial component.

Restriction is right adjoint to g_{n!}, which is exact by Stacks 0D74, so Homology 015Z applies.

theorem injective_componentModuleRestriction'
    (hflat : ∀ (m : SimplexCategory) (φ : n ⟶ m), (S.transitionRingedToposHom P φ).IsFlat)
    (I : SheafOfModules.{u}
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := S.totalTopology) P))) [Injective I] :
    Injective ((S.componentModuleRestriction
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := S.totalTopology) P)) n).obj I)
Sources
LeanCategoryTheory.SimplicialSiteSituation.componentRingedTopos_restrictionIso · CategoryTheory.SimplicialSiteSituation.componentRingedTopos_restrictionIso_forget · CategoryTheory.SimplicialSiteSituation.componentRingedToposHom · CategoryTheory.SimplicialSiteSituation.componentRingedToposHom_toToposHom · CategoryTheory.SimplicialSiteSituation.moduleSumFormulaLegEq · CategoryTheory.SimplicialSiteSituation.componentRingedToposHom_fSharpInverseImageRing_ringSheafMap · CategoryTheory.SimplicialSiteSituation.componentPullbackModulesRestrictionIso · CategoryTheory.SimplicialSiteSituation.componentPullbackModulesRestrictionIso_underlying

Section85.7 Morphisms of ringed simplicial sites#

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

Tag 0DGZ, a remark

Tag 0DGZ in the Stacks Project.

CategoryTheory.CocontinuousSimplicialSite.RingedMorphism, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedMorphism.lean, line 95. The attribute's comment: “ringed simplicial site morphism, case (B) of Situation 09WE”.

Stacks 0DGZ, case (B). A morphism between ringed simplicial sites: a morphism h between the underlying simplicial sites, together with a homomorphism of sheaves of rings h♯ : h_total⁻¹ 𝒪' ⟶ 𝒪 on the total site.

structure RingedMorphism (C C' : CocontinuousSimplicialSite.{u})
    (O : Sheaf (⟨Sum.inr C⟩ : SimplicialSiteSituation.{u}).totalTopology RingCat.{u})
    (O' : Sheaf (⟨Sum.inr C'⟩ : SimplicialSiteSituation.{u}).totalTopology RingCat.{u})

CategoryTheory.CocontinuousSimplicialSite.RingedMorphism.ringHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedMorphism.lean, line 122. The attribute's comment: “the two equivalent forms of the ring map, case (B)”. References: SGA 4 XVII (0.2.1), “ringed simplicial sites”.

Stacks 0DGZ, case (B). A homomorphism of sheaves of rings h_total⁻¹ 𝒪' ⟶ 𝒪 is the same thing as a homomorphism 𝒪' ⟶ h_{total, *} 𝒪: the two are exchanged by the adjunction between the inverse image and the direct image of sheaves of rings along the morphism of total topoi.

def ringHomEquiv (h : CocontinuousSimplicialSite.Morphism C C')
    (O : Sheaf (⟨Sum.inr C⟩ : SimplicialSiteSituation.{u}).totalTopology RingCat.{u})
    (O' : Sheaf (⟨Sum.inr C'⟩ : SimplicialSiteSituation.{u}).totalTopology RingCat.{u}) :
    (h.totalInverseImageRing O' ⟶ O) ≃ (O' ⟶ h.totalPushforwardRing O)

CategoryTheory.SimplicialSite.RingedMorphism, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedMorphismContinuous.lean, line 155. The attribute's comment: “ringed simplicial site morphism, case (A) of Situation 09WE”.

Stacks 0DGZ, case (A). A morphism between ringed simplicial sites: a morphism h between the underlying simplicial sites, together with a homomorphism of sheaves of rings h♯ : h_total⁻¹ 𝒪' ⟶ 𝒪 on the total site.

structure RingedMorphism (C C' : SimplicialSite.{u})
    (O : Sheaf C.totalTopology RingCat.{u})
    (O' : Sheaf C'.totalTopology RingCat.{u})

CategoryTheory.SimplicialSite.RingedMorphism.ringHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedMorphismContinuous.lean, line 181. The attribute's comment: “the two equivalent forms of the ring map, case (A)”. References: SGA 4 XVII (0.2.1), “ringed simplicial sites”.

Stacks 0DGZ, case (A). A homomorphism of sheaves of rings h_total⁻¹ 𝒪' ⟶ 𝒪 is the same thing as a homomorphism 𝒪' ⟶ h_{total, *} 𝒪: the two are exchanged by the adjunction between the inverse image and the direct image of sheaves of rings along the total functor.

def ringHomEquiv (h : SimplicialSite.Morphism C C')
    (O : Sheaf C.totalTopology RingCat.{u})
    (O' : Sheaf C'.totalTopology RingCat.{u}) :
    (h.totalInverseImageRing O' ⟶ O) ≃ (O' ⟶ h.totalPushforwardRing O)

CategoryTheory.SimplicialSiteMorphism.ringHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedMorphismSituation.lean, line 141. The attribute's comment: “the two equivalent forms of the ring map, case (A)”. References: SGA 4 XVII (0.2.1), “ringed simplicial sites”.

Stacks 0DGZ, both cases of Situation 09WE. A homomorphism of sheaves of rings h_total⁻¹ 𝒪' ⟶ 𝒪 is the same thing as a homomorphism 𝒪' ⟶ h_{total, *} 𝒪: the two are exchanged by the adjunction between the inverse image and the direct image of sheaves of rings along the morphism of total topoi.

def ringHomEquiv (h : SimplicialSiteMorphism S S')
    (O : Sheaf S.totalTopology RingCat.{u}) (O' : Sheaf S'.totalTopology RingCat.{u}) :
    (h.totalInverseImageRing O' ⟶ O) ≃ (O' ⟶ h.totalPushforwardRing O)

CategoryTheory.SimplicialSiteMorphism.ringHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedMorphismSituation.lean, line 141. The attribute's comment: “the two equivalent forms of the ring map, case (B)”. References: SGA 4 XVII (0.2.1), “ringed simplicial sites”.

Stacks 0DGZ, both cases of Situation 09WE. A homomorphism of sheaves of rings h_total⁻¹ 𝒪' ⟶ 𝒪 is the same thing as a homomorphism 𝒪' ⟶ h_{total, *} 𝒪: the two are exchanged by the adjunction between the inverse image and the direct image of sheaves of rings along the morphism of total topoi.

def ringHomEquiv (h : SimplicialSiteMorphism S S')
    (O : Sheaf S.totalTopology RingCat.{u}) (O' : Sheaf S'.totalTopology RingCat.{u}) :
    (h.totalInverseImageRing O' ⟶ O) ≃ (O' ⟶ h.totalPushforwardRing O)

CategoryTheory.SimplicialSiteSituation.RingedMorphism, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedMorphismSituation.lean, line 171. The attribute's comment: “ringed simplicial site morphism, case (A) of Situation 09WE”.

Stacks 0DGZ, both cases of Situation 09WE. A morphism between ringed simplicial sites: a morphism h between the underlying simplicial sites, together with a homomorphism of sheaves of rings h♯ : h_total⁻¹ 𝒪' ⟶ 𝒪 on the total site.

structure SimplicialSiteSituation.RingedMorphism (S S' : SimplicialSiteSituation.{u})
    (O : Sheaf S.totalTopology RingCat.{u})
    (O' : Sheaf S'.totalTopology RingCat.{u})

CategoryTheory.SimplicialSiteSituation.RingedMorphism, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedMorphismSituation.lean, line 171. The attribute's comment: “ringed simplicial site morphism, case (B) of Situation 09WE”.

Stacks 0DGZ, both cases of Situation 09WE. A morphism between ringed simplicial sites: a morphism h between the underlying simplicial sites, together with a homomorphism of sheaves of rings h♯ : h_total⁻¹ 𝒪' ⟶ 𝒪 on the total site.

structure SimplicialSiteSituation.RingedMorphism (S S' : SimplicialSiteSituation.{u})
    (O : Sheaf S.totalTopology RingCat.{u})
    (O' : Sheaf S'.totalTopology RingCat.{u})
Tag 0DH0, a lemma

Tag 0DH0 in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.componentPullbackUnderlyingIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphism.lean, line 737. The attribute's comment: “restriction of modules to components”.

Stacks 0DH0. Restriction of sheaves of modules to the simplicial component of degree n has the inverse image of sheaves of sets as its underlying sheaf, naturally in the module: the component structure sheaf is itself the restriction of the total structure sheaf, so the pullback of modules extends scalars along an isomorphism.

def componentPullbackUnderlyingIso :
    (componentRingedToposHom S O n).toModulesHom.pullbackModules ⋙
        Sheaf.moduleSheafFunctor
          ((Stacks.SheafOfModules.Tensor.ringSheaf (J := (componentRingedTopos S O n).J))
          (componentRingedTopos S O n).O) ≅
      Sheaf.moduleSheafFunctor
        ((Stacks.SheafOfModules.Tensor.ringSheaf (J := (totalRingedTopos S O).J))
          (totalRingedTopos S O).O) ⋙
        (componentRingedToposHom S O n).toToposHom.inverseImage

CategoryTheory.SimplicialSiteSituation.componentPullbackUnderlyingIso_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphism.lean, line 756. The attribute's comment: “the canonical restriction of modules”.

Stacks 0DH0. The comparison of the previous declaration is the canonical one, not an arbitrary isomorphism: precomposing it with the unit of extension of scalars along the component structure map — which is what AlgebraicGeometry.RingedToposHom.pullbackUnitUnderlyingIso is, by AlgebraicGeometry.RingedToposHom.pullbackUnitUnderlyingIso_hom_app — returns the comparison of Stacks 03D2 between the underlying sheaf of the inverse image of modules and the inverse image of the underlying sheaf.

theorem componentPullbackUnderlyingIso_unit :
    RingedToposHom.pullbackUnitUnderlyingIso (componentRingedToposHom S O n) ≪≫
        componentPullbackUnderlyingIso S O n =
      inverseImageModuleSheafIso (componentRingedToposHom S O n).toToposHom
        ((Stacks.SheafOfModules.Tensor.ringSheaf (J := (totalRingedTopos S O).J))
          (totalRingedTopos S O).O)

CategoryTheory.CocontinuousSimplicialSite.Morphism.componentInverseImageCommRingIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphism.lean, line 810. The attribute's comment: “the canonical ring comparison”.

Stacks 0DH0. The comparison of the two inverse images of sheaves of commutative rings around the square of simplicial degree n. This is the identification gₙ⁻¹h_{total}⁻¹𝒪' = hₙ⁻¹(g'ₙ)⁻¹𝒪' through which the source defines the degreewise structure map.

def componentInverseImageCommRingIso (h : Morphism C C') (n : SimplexCategory) :
    inverseImageCommRingFunctor.{u, u, u, u, u, u} (viaTotalMorphism h n) ≅
      inverseImageCommRingFunctor.{u, u, u, u, u, u} (viaComponentMorphism h n)

CategoryTheory.CocontinuousSimplicialSite.Morphism.componentInverseImageCommRingIso_forget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphism.lean, line 823. The attribute's comment: “the canonical underlying comparison”.

Stacks 0DH0. The comparison of inverse images of sheaves of commutative rings has the comparison of inverse images of sheaves of sets as its underlying map, which determines it uniquely by Stacks.Sheaves.ToposPushforward.inverseImageCommRingIsoOfToposIso_existsUnique.

theorem componentInverseImageCommRingIso_forget (h : Morphism C C') (n : SimplexCategory)
    (O' : Sheaf C'.situation.totalTopology CommRingCat.{u}) :
    (sheafCompose (C.situation.componentTopology n) (forget CommRingCat.{u})).map
        ((componentInverseImageCommRingIso h n).hom.app O') =
      (componentInverseImageIso h n).hom.app
        ((sheafCompose C'.situation.totalTopology (forget CommRingCat.{u})).obj O')

CategoryTheory.CocontinuousSimplicialSite.Morphism.totalRingedToposHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphism.lean, line 950. The attribute's comment: “the total morphism of ringed topoi”.

Stacks 0DH0. The morphism of total ringed topoi induced by a morphism between ringed simplicial sites.

def totalRingedToposHom
    (h : Morphism C C') (φ : h.totalInverseImageRing
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := C'.situation.totalTopology) O')) ⟶
        (Stacks.SheafOfModules.Tensor.ringSheaf (J := C.situation.totalTopology) O)) :
    RingedToposHom (C.situation.totalRingedTopos O) (C'.situation.totalRingedTopos O')

CategoryTheory.CocontinuousSimplicialSite.Morphism.componentRingedToposHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphism.lean, line 1003. The attribute's comment: “the component morphisms of ringed topoi”.

Stacks 0DH0. The morphism of component ringed topoi in simplicial degree n induced by a morphism between ringed simplicial sites.

def componentRingedToposHom
    (h : Morphism C C') (φ : h.totalInverseImageRing
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := C'.situation.totalTopology) O')) ⟶
        (Stacks.SheafOfModules.Tensor.ringSheaf (J := C.situation.totalTopology) O))
    (n : SimplexCategory) :
    RingedToposHom (C.situation.componentRingedTopos O n)
      (C'.situation.componentRingedTopos O' n)

CategoryTheory.CocontinuousSimplicialSite.Morphism.componentRingedToposHom_toToposHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphism.lean, line 1021. The attribute's comment: “the underlying degreewise geometric morphisms”.

Stacks 0DH0. The underlying geometric morphism of the degreewise morphism of ringed topoi is the component morphism of topoi of Stacks 0D95.

theorem componentRingedToposHom_toToposHom
    (h : Morphism C C') (φ : h.totalInverseImageRing
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := C'.situation.totalTopology) O')) ⟶
        (Stacks.SheafOfModules.Tensor.ringSheaf (J := C.situation.totalTopology) O))
    (n : SimplexCategory) :
    ((h.componentRingedToposHom φ) n).toToposHom =
      (SimplicialSiteMorphism.ofCocontinuous h).componentMorphism n

CategoryTheory.CocontinuousSimplicialSite.Morphism.componentRingedToposHom_commutes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphism.lean, line 1043. The attribute's comment: “the commutative squares of ringed topoi”.

Stacks 0DH0. The square of ringed topoi formed by the total morphism, the degreewise morphism and the two canonical morphisms from the components of simplicial degree n commutes: the comparison of inverse images identifies the two composite structure maps.

theorem componentRingedToposHom_commutes
    (h : Morphism C C') (φ : h.totalInverseImageRing
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := C'.situation.totalTopology) O')) ⟶
        (Stacks.SheafOfModules.Tensor.ringSheaf (J := C.situation.totalTopology) O))
    (n : SimplexCategory) :
    (h.componentInverseImageCommRingIso n).hom.app O' ≫
        ((C'.situation.componentRingedToposHom O' n).comp
          ((h.componentRingedToposHom φ) n)).fSharpInverseImage =
      ((h.totalRingedToposHom φ).comp
        (C.situation.componentRingedToposHom O n)).fSharpInverseImage

CategoryTheory.CocontinuousSimplicialSite.Morphism.componentPushforwardModulesForgetIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphism.lean, line 1085. The attribute's comment: “the underlying restriction of the direct image of modules”.

Stacks 0DH0, the assertion on sheaves of modules, on underlying sheaves of sets. Inverse image to the simplicial component of degree n of a direct image of sheaves of modules along the total morphism is the degreewise direct image of the inverse image to that component.

The comparison is the one of Stacks 0D96 and nothing else: the pullback of modules along a component inclusion is inverse image on underlying sheaves of sets, by CategoryTheory.SimplicialSiteSituation.componentPullbackUnderlyingIso, and the direct image of modules is direct image there on the nose.

def componentPushforwardModulesForgetIso
    (h : Morphism C C') (φ : h.totalInverseImageRing
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := C'.situation.totalTopology) O')) ⟶
        (Stacks.SheafOfModules.Tensor.ringSheaf (J := C.situation.totalTopology) O))
    (n : SimplexCategory) :
    (h.totalRingedToposHom φ).pushforwardModules ⋙
        (C'.situation.componentRingedToposHom O' n).toModulesHom.pullbackModules ⋙
          Sheaf.moduleSheafFunctor
            ((Stacks.SheafOfModules.Tensor.ringSheaf
              (J := (C'.situation.componentRingedTopos O' n).J)
              (C'.situation.componentRingedTopos O' n).O)) ≅
      (C.situation.componentRingedToposHom O n).toModulesHom.pullbackModules ⋙
        ((h.componentRingedToposHom φ) n).pushforwardModules ⋙
          Sheaf.moduleSheafFunctor
            ((Stacks.SheafOfModules.Tensor.ringSheaf
              (J := (C'.situation.componentRingedTopos O' n).J)
              (C'.situation.componentRingedTopos O' n).O))

CategoryTheory.CocontinuousSimplicialSite.Morphism.componentRingedToposHom_twoIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphism.lean, line 1166. The attribute's comment: “the degreewise square as a 2-isomorphism of ringed topoi”.

Stacks 0DH0. The degreewise square commutes as a square of ringed topoi, in the sense of Stacks 04IC: the two composites h_{total} ∘ g_n and g'_n ∘ h_n are 2-isomorphic.

The comparison of the direct images is the one of Stacks 0D96, and the compatibility with the three structure maps is componentRingedToposHom_commutes read on underlying sheaves of sets, through AlgebraicGeometry.RingedToposHom.TwoIso.ofInverseImageIso, which transposes a compatibility of the inverse-image forms into one of the direct-image forms. The underlying comparison of inverse images is pinned by CategoryTheory.CocontinuousSimplicialSite.Morphism.componentInverseImageCommRingIso_forget, so this 2-isomorphism is not an arbitrary one.

noncomputable def componentRingedToposHom_twoIso
    (h : Morphism C C') (φ : h.totalInverseImageRing
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := C'.situation.totalTopology) O')) ⟶
        (Stacks.SheafOfModules.Tensor.ringSheaf (J := C.situation.totalTopology) O))
    (n : SimplexCategory) :
    RingedToposHom.TwoIso.{u, u, u, u, u, u}
      (viaTotalRingedToposHom h φ n) (viaComponentRingedToposHom h φ n)

CategoryTheory.CocontinuousSimplicialSite.Morphism.componentPushforwardModulesSquareIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphism.lean, line 1199. The attribute's comment: “the commutative squares, on direct images of sheaves of modules”.

Stacks 0DH0, the degreewise square on direct images of sheaves of modules. Direct image to the total ringed topos of the target, taken through the component of degree n of the source, agrees with direct image taken through the component of degree n of the target:

h_{total,*} ∘ g_{n,*} ≅ g'_{n,*} ∘ h_{n,*} on Mod(𝒪_n).

This is the commuting square of ringed topoi of componentRingedToposHom_twoIso read on sheaves of modules, and it is a genuine module-level statement: the comparison is additive and linear, not merely a comparison of underlying sheaves of sets.

noncomputable def componentPushforwardModulesSquareIso
    (h : Morphism C C') (φ : h.totalInverseImageRing
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := C'.situation.totalTopology) O')) ⟶
        (Stacks.SheafOfModules.Tensor.ringSheaf (J := C.situation.totalTopology) O))
    (n : SimplexCategory) :
    (C.situation.componentRingedToposHom O n).pushforwardModules ⋙
        (h.totalRingedToposHom φ).pushforwardModules ≅
      ((h.componentRingedToposHom φ) n).pushforwardModules ⋙
        (C'.situation.componentRingedToposHom O' n).pushforwardModules

CategoryTheory.CocontinuousSimplicialSite.Morphism.componentPullbackModulesSquareIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphism.lean, line 1222. The attribute's comment: “the commutative squares, on pullbacks of sheaves of modules”.

Stacks 0DH0, the degreewise square on pullbacks of sheaves of modules. The same square, read on pullbacks:

g_n^* ∘ h_{total}^* ≅ h_n^* ∘ (g'_n)^* on Mod(𝒪').

Both sides are left adjoint to the two sides of componentPushforwardModulesSquareIso, so this is uniqueness of left adjoints applied to that isomorphism.

noncomputable def componentPullbackModulesSquareIso
    (h : Morphism C C') (φ : h.totalInverseImageRing
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := C'.situation.totalTopology) O')) ⟶
        (Stacks.SheafOfModules.Tensor.ringSheaf (J := C.situation.totalTopology) O))
    (n : SimplexCategory) :
    (h.totalRingedToposHom φ).toModulesHom.pullbackModules ⋙
        (C.situation.componentRingedToposHom O n).toModulesHom.pullbackModules ≅
      (C'.situation.componentRingedToposHom O' n).toModulesHom.pullbackModules ⋙
        ((h.componentRingedToposHom φ) n).toModulesHom.pullbackModules

CategoryTheory.CocontinuousSimplicialSite.Morphism.componentPushforwardModulesComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphism.lean, line 1247. The attribute's comment: “the comparison of the last assertion, on sheaves of modules”.

Stacks 0DH0, the comparison of the last assertion. The canonical morphism of functors Mod(𝒪) ⟶ Mod(𝒪'_n)

(g'_n)^* ∘ h_{total,*} ⟶ h_{n,*} ∘ g_n^*

attached to the degreewise square: the mate of componentPushforwardModulesSquareIso under the two adjunctions g_n^* ⊣ g_{n,*} and (g'_n)^* ⊣ (g'_n)_* of Stacks 03D7. The source's last assertion is that this comparison is invertible, which is the Beck–Chevalley content of the degreewise square; see the implementation notes of this file.

noncomputable def componentPushforwardModulesComparison
    (h : Morphism C C') (φ : h.totalInverseImageRing
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := C'.situation.totalTopology) O')) ⟶
        (Stacks.SheafOfModules.Tensor.ringSheaf (J := C.situation.totalTopology) O))
    (n : SimplexCategory) :
    (h.totalRingedToposHom φ).pushforwardModules ⋙
        (C'.situation.componentRingedToposHom O' n).toModulesHom.pullbackModules ⟶
      (C.situation.componentRingedToposHom O n).toModulesHom.pullbackModules ⋙
        ((h.componentRingedToposHom φ) n).pushforwardModules

CategoryTheory.CocontinuousSimplicialSite.Morphism.componentPushforwardModulesComparison_mate, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphism.lean, line 1267. The attribute's comment: “the comparison of the last assertion is the mate of the square”.

Stacks 0DH0. The comparison of the last assertion is pinned by the degreewise square: its mate under the two adjunctions of Stacks 03D7 is the square of direct images of sheaves of modules. In particular it is not an arbitrary natural transformation.

theorem componentPushforwardModulesComparison_mate
    (h : Morphism C C') (φ : h.totalInverseImageRing
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := C'.situation.totalTopology) O')) ⟶
        (Stacks.SheafOfModules.Tensor.ringSheaf (J := C.situation.totalTopology) O))
    (n : SimplexCategory) :
    mateEquiv
        (RingedToposHom.pullbackAdjPushforwardModules
          (C.situation.componentRingedToposHom O n))
        (RingedToposHom.pullbackAdjPushforwardModules
          (C'.situation.componentRingedToposHom O' n))
        (componentPushforwardModulesComparison h φ n) =
      TwoSquare.mk _ _ _ _ (componentPushforwardModulesSquareIso h φ n).hom

CategoryTheory.CocontinuousSimplicialSite.Morphism.componentPushforwardModulesIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphism.lean, line 1429. The attribute's comment: “the last assertion, on sheaves of modules”.

Stacks 0DH0, the last assertion, on sheaves of modules. Inverse image to the simplicial component of degree n of a direct image of sheaves of modules along the total morphism is the degreewise direct image of the inverse image to that component:

(g'_n)^* ∘ h_{total,*} ≅ h_{n,*} ∘ g_n^* as functors Mod(𝒪) ⟶ Mod(𝒪'_n),

the isomorphism being the canonical comparison componentPushforwardModulesComparison attached to the degreewise square. That comparison is invertible by isIso_componentPushforwardModulesComparison, which is the Beck–Chevalley statement for the square; so this is unconditional, as is the assertion on underlying sheaves of sets, componentPushforwardModulesForgetIso.

noncomputable def componentPushforwardModulesIso
    (h : Morphism C C') (φ : h.totalInverseImageRing
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := C'.situation.totalTopology) O')) ⟶
        (Stacks.SheafOfModules.Tensor.ringSheaf (J := C.situation.totalTopology) O))
    (n : SimplexCategory) :
    (h.totalRingedToposHom φ).pushforwardModules ⋙
        (C'.situation.componentRingedToposHom O' n).toModulesHom.pullbackModules ≅
      (C.situation.componentRingedToposHom O n).toModulesHom.pullbackModules ⋙
        ((h.componentRingedToposHom φ) n).pushforwardModules

CategoryTheory.CocontinuousSimplicialSite.RingedMorphism.totalRingedToposHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphism.lean, line 1480. The attribute's comment: “the total morphism of ringed topoi”.

Stacks 0DH0. The morphism of total ringed topoi induced by a morphism between ringed simplicial sites.

def totalRingedToposHom
    (h : RingedMorphism C C'
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := C.situation.totalTopology)) O)
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := C'.situation.totalTopology)) O')) :
    RingedToposHom (C.situation.totalRingedTopos O) (C'.situation.totalRingedTopos O')

CategoryTheory.CocontinuousSimplicialSite.RingedMorphism.componentRingedToposHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphism.lean, line 1533. The attribute's comment: “the component morphisms of ringed topoi”.

Stacks 0DH0. The morphism of component ringed topoi in simplicial degree n induced by a morphism between ringed simplicial sites.

def componentRingedToposHom
    (h : RingedMorphism C C'
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := C.situation.totalTopology)) O)
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := C'.situation.totalTopology)) O'))
    (n : SimplexCategory) :
    RingedToposHom (C.situation.componentRingedTopos O n)
      (C'.situation.componentRingedTopos O' n)

CategoryTheory.CocontinuousSimplicialSite.RingedMorphism.componentRingedToposHom_toToposHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphism.lean, line 1551. The attribute's comment: “the underlying degreewise geometric morphisms”.

Stacks 0DH0. The underlying geometric morphism of the degreewise morphism of ringed topoi is the component morphism of topoi of Stacks 0D95.

theorem componentRingedToposHom_toToposHom
    (h : RingedMorphism C C'
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := C.situation.totalTopology)) O)
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := C'.situation.totalTopology)) O'))
    (n : SimplexCategory) :
    (h.componentRingedToposHom n).toToposHom =
      (SimplicialSiteMorphism.ofCocontinuous h.hom).componentMorphism n

CategoryTheory.CocontinuousSimplicialSite.RingedMorphism.componentRingedToposHom_commutes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphism.lean, line 1573. The attribute's comment: “the commutative squares of ringed topoi”.

Stacks 0DH0. The square of ringed topoi formed by the total morphism, the degreewise morphism and the two canonical morphisms from the components of simplicial degree n commutes: the comparison of inverse images identifies the two composite structure maps.

theorem componentRingedToposHom_commutes
    (h : RingedMorphism C C'
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := C.situation.totalTopology)) O)
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := C'.situation.totalTopology)) O'))
    (n : SimplexCategory) :
    (h.hom.componentInverseImageCommRingIso n).hom.app O' ≫
        ((C'.situation.componentRingedToposHom O' n).comp
          (h.componentRingedToposHom n)).fSharpInverseImage =
      (h.totalRingedToposHom.comp
        (C.situation.componentRingedToposHom O n)).fSharpInverseImage

CategoryTheory.CocontinuousSimplicialSite.RingedMorphism.componentPushforwardModulesForgetIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphism.lean, line 1594. The attribute's comment: “the underlying restriction of the direct image of modules”.

Stacks 0DH0, the assertion on sheaves of modules, on underlying sheaves of sets. Inverse image to the simplicial component of degree n of a direct image of sheaves of modules along the total morphism is the degreewise direct image of the inverse image to that component.

The comparison is the one of Stacks 0D96 and nothing else: the pullback of modules along a component inclusion is inverse image on underlying sheaves of sets, by CategoryTheory.SimplicialSiteSituation.componentPullbackUnderlyingIso, and the direct image of modules is direct image there on the nose.

def componentPushforwardModulesForgetIso
    (h : RingedMorphism C C'
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := C.situation.totalTopology)) O)
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := C'.situation.totalTopology)) O'))
    (n : SimplexCategory) :
    h.totalRingedToposHom.pushforwardModules ⋙
        (C'.situation.componentRingedToposHom O' n).toModulesHom.pullbackModules ⋙
          Sheaf.moduleSheafFunctor
            ((Stacks.SheafOfModules.Tensor.ringSheaf
              (J := (C'.situation.componentRingedTopos O' n).J))
              (C'.situation.componentRingedTopos O' n).O) ≅
      (C.situation.componentRingedToposHom O n).toModulesHom.pullbackModules ⋙
        (h.componentRingedToposHom n).pushforwardModules ⋙
          Sheaf.moduleSheafFunctor
            ((Stacks.SheafOfModules.Tensor.ringSheaf
              (J := (C'.situation.componentRingedTopos O' n).J))
              (C'.situation.componentRingedTopos O' n).O)

CategoryTheory.CocontinuousSimplicialSite.RingedMorphism.componentRingedToposHom_twoIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphism.lean, line 1675. The attribute's comment: “the degreewise square as a 2-isomorphism of ringed topoi”.

Stacks 0DH0. The degreewise square commutes as a square of ringed topoi, in the sense of Stacks 04IC: the two composites h_{total} ∘ g_n and g'_n ∘ h_n are 2-isomorphic.

The comparison of the direct images is the one of Stacks 0D96, and the compatibility with the three structure maps is componentRingedToposHom_commutes read on underlying sheaves of sets, through AlgebraicGeometry.RingedToposHom.TwoIso.ofInverseImageIso, which transposes a compatibility of the inverse-image forms into one of the direct-image forms. The underlying comparison of inverse images is pinned by CategoryTheory.CocontinuousSimplicialSite.Morphism.componentInverseImageCommRingIso_forget, so this 2-isomorphism is not an arbitrary one.

noncomputable def componentRingedToposHom_twoIso
    (h : RingedMorphism C C'
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := C.situation.totalTopology)) O)
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := C'.situation.totalTopology)) O'))
    (n : SimplexCategory) :
    RingedToposHom.TwoIso.{u, u, u, u, u, u}
      (viaTotalRingedToposHom h n) (viaComponentRingedToposHom h n)

CategoryTheory.CocontinuousSimplicialSite.RingedMorphism.componentPushforwardModulesSquareIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphism.lean, line 1708. The attribute's comment: “the commutative squares, on direct images of sheaves of modules”.

Stacks 0DH0, the degreewise square on direct images of sheaves of modules. Direct image to the total ringed topos of the target, taken through the component of degree n of the source, agrees with direct image taken through the component of degree n of the target:

h_{total,*} ∘ g_{n,*} ≅ g'_{n,*} ∘ h_{n,*} on Mod(𝒪_n).

This is the commuting square of ringed topoi of componentRingedToposHom_twoIso read on sheaves of modules, and it is a genuine module-level statement: the comparison is additive and linear, not merely a comparison of underlying sheaves of sets.

noncomputable def componentPushforwardModulesSquareIso
    (h : RingedMorphism C C'
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := C.situation.totalTopology)) O)
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := C'.situation.totalTopology)) O'))
    (n : SimplexCategory) :
    (C.situation.componentRingedToposHom O n).pushforwardModules ⋙
        h.totalRingedToposHom.pushforwardModules ≅
      (h.componentRingedToposHom n).pushforwardModules ⋙
        (C'.situation.componentRingedToposHom O' n).pushforwardModules

CategoryTheory.CocontinuousSimplicialSite.RingedMorphism.componentPullbackModulesSquareIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphism.lean, line 1731. The attribute's comment: “the commutative squares, on pullbacks of sheaves of modules”.

Stacks 0DH0, the degreewise square on pullbacks of sheaves of modules. The same square, read on pullbacks:

g_n^* ∘ h_{total}^* ≅ h_n^* ∘ (g'_n)^* on Mod(𝒪').

Both sides are left adjoint to the two sides of componentPushforwardModulesSquareIso, so this is uniqueness of left adjoints applied to that isomorphism.

noncomputable def componentPullbackModulesSquareIso
    (h : RingedMorphism C C' (Stacks.SheafOfModules.Tensor.ringSheaf O)
      (Stacks.SheafOfModules.Tensor.ringSheaf O')) (n : SimplexCategory) :
    h.totalRingedToposHom.toModulesHom.pullbackModules ⋙
        (C.situation.componentRingedToposHom O n).toModulesHom.pullbackModules ≅
      (C'.situation.componentRingedToposHom O' n).toModulesHom.pullbackModules ⋙
        (h.componentRingedToposHom n).toModulesHom.pullbackModules

CategoryTheory.CocontinuousSimplicialSite.RingedMorphism.componentPushforwardModulesComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphism.lean, line 1754. The attribute's comment: “the comparison of the last assertion, on sheaves of modules”.

Stacks 0DH0, the comparison of the last assertion. The canonical morphism of functors Mod(𝒪) ⟶ Mod(𝒪'_n)

(g'_n)^* ∘ h_{total,*} ⟶ h_{n,*} ∘ g_n^*

attached to the degreewise square: the mate of componentPushforwardModulesSquareIso under the two adjunctions g_n^* ⊣ g_{n,*} and (g'_n)^* ⊣ (g'_n)_* of Stacks 03D7. The source's last assertion is that this comparison is invertible, which is isIso_componentPushforwardModulesComparison.

noncomputable def componentPushforwardModulesComparison
    (h : RingedMorphism C C'
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := C.situation.totalTopology)) O)
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := C'.situation.totalTopology)) O'))
    (n : SimplexCategory) :
    h.totalRingedToposHom.pushforwardModules ⋙
        (C'.situation.componentRingedToposHom O' n).toModulesHom.pullbackModules ⟶
      (C.situation.componentRingedToposHom O n).toModulesHom.pullbackModules ⋙
        (h.componentRingedToposHom n).pushforwardModules

CategoryTheory.CocontinuousSimplicialSite.RingedMorphism.componentPushforwardModulesComparison_mate, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphism.lean, line 1774. The attribute's comment: “the comparison of the last assertion is the mate of the square”.

Stacks 0DH0. The comparison of the last assertion is pinned by the degreewise square: its mate under the two adjunctions of Stacks 03D7 is the square of direct images of sheaves of modules. In particular it is not an arbitrary natural transformation.

theorem componentPushforwardModulesComparison_mate
    (h : RingedMorphism C C'
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := C.situation.totalTopology)) O)
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := C'.situation.totalTopology)) O'))
    (n : SimplexCategory) :
    mateEquiv
        (RingedToposHom.pullbackAdjPushforwardModules
          (C.situation.componentRingedToposHom O n))
        (RingedToposHom.pullbackAdjPushforwardModules
          (C'.situation.componentRingedToposHom O' n))
        (componentPushforwardModulesComparison h n) =
      TwoSquare.mk _ _ _ _ (componentPushforwardModulesSquareIso h n).hom

CategoryTheory.CocontinuousSimplicialSite.RingedMorphism.isIso_componentPushforwardModulesComparison, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphism.lean, line 1809. The attribute's comment: “the comparison of the last assertion is invertible”.

Stacks 0DH0, the last assertion: the comparison is invertible. The canonical comparison (g'_n)^* ∘ h_{total,*} ⟶ h_{n,*} ∘ g_n^* of sheaves of modules is an isomorphism. On underlying sheaves of sets it is the mate of the degreewise square of topoi, which is invertible by the Beck–Chevalley property of the square of component inclusions, CategoryTheory.CocontinuousSimplicialSite.Morphism.isIso_totalComponentPushforwardMate; and the two pullbacks g_n^*, (g'_n)^* are inverse images on underlying sheaves of sets, so the module-level mate lies over that one (AlgebraicGeometry.RingedToposHom.isIso_mateEquiv_symm_pushforwardModules_of_isIso).

instance isIso_componentPushforwardModulesComparison
    (h : RingedMorphism C C'
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := C.situation.totalTopology)) O)
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := C'.situation.totalTopology)) O'))
    (n : SimplexCategory) :
    IsIso (componentPushforwardModulesComparison h n)

CategoryTheory.CocontinuousSimplicialSite.RingedMorphism.componentPushforwardModulesIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphism.lean, line 1834. The attribute's comment: “the last assertion, on sheaves of modules”.

Stacks 0DH0, the last assertion, on sheaves of modules. Inverse image to the simplicial component of degree n of a direct image of sheaves of modules along the total morphism is the degreewise direct image of the inverse image to that component:

(g'_n)^* ∘ h_{total,*} ≅ h_{n,*} ∘ g_n^* as functors Mod(𝒪) ⟶ Mod(𝒪'_n),

the isomorphism being the canonical comparison componentPushforwardModulesComparison attached to the degreewise square, which is invertible by isIso_componentPushforwardModulesComparison.

noncomputable def componentPushforwardModulesIso
    (h : RingedMorphism C C'
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := C.situation.totalTopology)) O)
      ((Stacks.SheafOfModules.Tensor.ringSheaf (J := C'.situation.totalTopology)) O'))
    (n : SimplexCategory) :
    h.totalRingedToposHom.pushforwardModules ⋙
        (C'.situation.componentRingedToposHom O' n).toModulesHom.pullbackModules ≅
      (C.situation.componentRingedToposHom O n).toModulesHom.pullbackModules ⋙
        (h.componentRingedToposHom n).pushforwardModules

CategoryTheory.SimplicialSite.Morphism.componentInverseImageCommRingIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphismContinuous.lean, line 134. The attribute's comment: “the canonical ring comparison, case (A)”.

Stacks 0DH0, case (A). The comparison of the two inverse images of sheaves of commutative rings around the square of simplicial degree n: the identification gₙ⁻¹h_{total}⁻¹𝒪' = hₙ⁻¹(g'ₙ)⁻¹𝒪' through which the source defines the degreewise structure map.

def componentInverseImageCommRingIso (h : SimplicialSite.Morphism C C') (n : SimplexCategory) :
    inverseImageCommRingFunctor.{u, u, u, u, u, u} (viaTotalMorphism h n) ≅
      inverseImageCommRingFunctor.{u, u, u, u, u, u} (viaComponentMorphism h n)

CategoryTheory.SimplicialSite.Morphism.componentInverseImageCommRingIso_forget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphismContinuous.lean, line 145. The attribute's comment: “the canonical underlying comparison, case (A)”.

Stacks 0DH0, case (A). The comparison of inverse images of sheaves of commutative rings has the comparison of inverse images of sheaves of sets as its underlying map.

theorem componentInverseImageCommRingIso_forget (h : SimplicialSite.Morphism C C')
    (n : SimplexCategory) (O' : Sheaf C'.situation.totalTopology CommRingCat.{u}) :
    (sheafCompose (C.situation.componentTopology n) (forget CommRingCat.{u})).map
        ((componentInverseImageCommRingIso h n).hom.app O') =
      (componentInverseImageIso h n).hom.app
        ((sheafCompose C'.situation.totalTopology (forget CommRingCat.{u})).obj O')

CategoryTheory.SimplicialSite.RingedMorphism.totalRingedToposHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphismContinuous.lean, line 189. The attribute's comment: “the total morphism of ringed topoi, case (A)”.

Stacks 0DH0, case (A). The morphism of total ringed topoi induced by a morphism between ringed simplicial sites.

def totalRingedToposHom
    (h : RingedMorphism C C' (C.totalRingSheaf O) (C'.totalRingSheaf O')) :
    RingedToposHom (C.situation.totalRingedTopos O) (C'.situation.totalRingedTopos O')

CategoryTheory.SimplicialSite.RingedMorphism.componentRingedToposHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphismContinuous.lean, line 227. The attribute's comment: “the component morphisms of ringed topoi, case (A)”.

Stacks 0DH0, case (A). The morphism of component ringed topoi in simplicial degree n induced by a morphism between ringed simplicial sites.

def componentRingedToposHom
    (h : RingedMorphism C C' (C.totalRingSheaf O) (C'.totalRingSheaf O')) (n : SimplexCategory) :
    RingedToposHom (C.situation.componentRingedTopos O n)
      (C'.situation.componentRingedTopos O' n)

CategoryTheory.SimplicialSite.RingedMorphism.componentRingedToposHom_toToposHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphismContinuous.lean, line 242. The attribute's comment: “the underlying degreewise geometric morphisms, case (A)”.

Stacks 0DH0, case (A). The underlying geometric morphism of the degreewise morphism of ringed topoi is the component morphism of topoi of Stacks 0D95.

theorem componentRingedToposHom_toToposHom
    (h : RingedMorphism C C' (C.totalRingSheaf O) (C'.totalRingSheaf O')) (n : SimplexCategory) :
    (h.componentRingedToposHom n).toToposHom =
      (SimplicialSiteMorphism.ofMorphismOfSites h.hom).componentMorphism n

CategoryTheory.SimplicialSite.RingedMorphism.componentRingedToposHom_commutes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphismContinuous.lean, line 258. The attribute's comment: “the commutative squares of ringed topoi, case (A)”.

Stacks 0DH0, case (A). The square of ringed topoi formed by the total morphism, the degreewise morphism and the two canonical morphisms from the components of simplicial degree n commutes: the comparison of inverse images identifies the two composite structure maps.

theorem componentRingedToposHom_commutes
    (h : RingedMorphism C C' (C.totalRingSheaf O) (C'.totalRingSheaf O')) (n : SimplexCategory) :
    (h.hom.componentInverseImageCommRingIso n).hom.app O' ≫
        ((C'.situation.componentRingedToposHom O' n).comp
          (h.componentRingedToposHom n)).fSharpInverseImage =
      (h.totalRingedToposHom.comp
        (C.situation.componentRingedToposHom O n)).fSharpInverseImage

CategoryTheory.SimplicialSite.RingedMorphism.componentRingedToposHom_twoIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphismContinuous.lean, line 319. The attribute's comment: “the degreewise square as a 2-isomorphism of ringed topoi, case (A)”.

Stacks 0DH0, case (A). The degreewise square commutes as a square of ringed topoi, in the sense of Stacks 04IC: the two composites h_{total} ∘ g_n and g'_n ∘ h_n are 2-isomorphic, the comparison of direct images being the one of Stacks 0D96.

noncomputable def componentRingedToposHom_twoIso
    (h : RingedMorphism C C' (C.totalRingSheaf O) (C'.totalRingSheaf O')) (n : SimplexCategory) :
    RingedToposHom.TwoIso.{u, u, u, u, u, u}
      (viaTotalRingedToposHom h n) (viaComponentRingedToposHom h n)

CategoryTheory.SimplicialSite.RingedMorphism.componentPushforwardModulesSquareIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphismContinuous.lean, line 341. The attribute's comment: “the commutative squares, on direct images of sheaves of modules, case (A)”.

Stacks 0DH0, case (A), the degreewise square on direct images of sheaves of modules: h_{total,*} ∘ g_{n,*} ≅ g'_{n,*} ∘ h_{n,*} on Mod(𝒪_n).

noncomputable def componentPushforwardModulesSquareIso
    (h : RingedMorphism C C' (C.totalRingSheaf O) (C'.totalRingSheaf O')) (n : SimplexCategory) :
    (C.situation.componentRingedToposHom O n).pushforwardModules ⋙
        h.totalRingedToposHom.pushforwardModules ≅
      (h.componentRingedToposHom n).pushforwardModules ⋙
        (C'.situation.componentRingedToposHom O' n).pushforwardModules

CategoryTheory.SimplicialSite.RingedMorphism.componentPullbackModulesSquareIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphismContinuous.lean, line 356. The attribute's comment: “the commutative squares, on pullbacks of sheaves of modules, case (A)”.

Stacks 0DH0, case (A), the degreewise square on pullbacks of sheaves of modules: g_n^* ∘ h_{total}^* ≅ h_n^* ∘ (g'_n)^* on Mod(𝒪').

noncomputable def componentPullbackModulesSquareIso
    (h : RingedMorphism C C' (C.totalRingSheaf O) (C'.totalRingSheaf O')) (n : SimplexCategory) :
    h.totalRingedToposHom.toModulesHom.pullbackModules ⋙
        (C.situation.componentRingedToposHom O n).toModulesHom.pullbackModules ≅
      (C'.situation.componentRingedToposHom O' n).toModulesHom.pullbackModules ⋙
        (h.componentRingedToposHom n).toModulesHom.pullbackModules

CategoryTheory.SimplicialSite.RingedMorphism.componentPushforwardModulesComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphismContinuous.lean, line 376. The attribute's comment: “the comparison of the last assertion, on sheaves of modules, case (A)”.

Stacks 0DH0, case (A), the comparison of the last assertion: the canonical morphism of functors Mod(𝒪) ⟶ Mod(𝒪'_n)

(g'_n)^* ∘ h_{total,*} ⟶ h_{n,*} ∘ g_n^*,

the mate of componentPushforwardModulesSquareIso under the two adjunctions g_n^* ⊣ g_{n,*} and (g'_n)^* ⊣ (g'_n)_* of Stacks 03D7.

noncomputable def componentPushforwardModulesComparison
    (h : RingedMorphism C C' (C.totalRingSheaf O) (C'.totalRingSheaf O')) (n : SimplexCategory) :
    h.totalRingedToposHom.pushforwardModules ⋙
        (C'.situation.componentRingedToposHom O' n).toModulesHom.pullbackModules ⟶
      (C.situation.componentRingedToposHom O n).toModulesHom.pullbackModules ⋙
        (h.componentRingedToposHom n).pushforwardModules

CategoryTheory.SimplicialSite.RingedMorphism.componentPushforwardModulesComparison_mate, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphismContinuous.lean, line 393. The attribute's comment: “the comparison of the last assertion is the mate of the square, case (A)”.

Stacks 0DH0, case (A). The comparison of the last assertion is pinned by the degreewise square: its mate under the two adjunctions of Stacks 03D7 is the square of direct images of sheaves of modules.

theorem componentPushforwardModulesComparison_mate
    (h : RingedMorphism C C' (C.totalRingSheaf O) (C'.totalRingSheaf O')) (n : SimplexCategory) :
    mateEquiv
        (RingedToposHom.pullbackAdjPushforwardModules
          (C.situation.componentRingedToposHom O n))
        (RingedToposHom.pullbackAdjPushforwardModules
          (C'.situation.componentRingedToposHom O' n))
        (componentPushforwardModulesComparison h n) =
      TwoSquare.mk _ _ _ _ (componentPushforwardModulesSquareIso h n).hom

CategoryTheory.SimplicialSite.RingedMorphism.isIso_componentPushforwardModulesComparison, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphismContinuous.lean, line 417. The attribute's comment: “the comparison of the last assertion is invertible, case (A)”.

Stacks 0DH0, case (A), the last assertion: the comparison is invertible. On underlying sheaves of sets it is the mate of the degreewise square of topoi, which is invertible by CategoryTheory.SimplicialSite.Morphism.isIso_totalComponentPushforwardMate.

instance isIso_componentPushforwardModulesComparison
    (h : RingedMorphism C C' (C.totalRingSheaf O) (C'.totalRingSheaf O')) (n : SimplexCategory) :
    IsIso (componentPushforwardModulesComparison h n)

CategoryTheory.SimplicialSite.RingedMorphism.componentPushforwardModulesIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphismContinuous.lean, line 435. The attribute's comment: “the last assertion, on sheaves of modules, case (A)”.

Stacks 0DH0, case (A), the last assertion, on sheaves of modules:

(g'_n)^* ∘ h_{total,*} ≅ h_{n,*} ∘ g_n^* as functors Mod(𝒪) ⟶ Mod(𝒪'_n),

the isomorphism being the canonical comparison componentPushforwardModulesComparison.

noncomputable def componentPushforwardModulesIso
    (h : RingedMorphism C C' (C.totalRingSheaf O) (C'.totalRingSheaf O')) (n : SimplexCategory) :
    h.totalRingedToposHom.pushforwardModules ⋙
        (C'.situation.componentRingedToposHom O' n).toModulesHom.pullbackModules ≅
      (C.situation.componentRingedToposHom O n).toModulesHom.pullbackModules ⋙
        (h.componentRingedToposHom n).pushforwardModules
Tag 0DH1, a lemma

Tag 0DH1 in the Stacks Project.

CategoryTheory.SimplicialSite.RingedMorphism.derivedComponentPushforwardModulesIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphismContinuousDerivedPushforward.lean, line 459. The attribute's comment: “case (A)”.

Stacks 0DH1, case (A). With notation and hypotheses as in Stacks 0DH0, for simplicial sites whose transitions are morphisms of sites and a morphism of ringed simplicial sites built from morphisms of sites: for K in the unbounded derived category of sheaves of 𝒪-modules on the total site,

(g'_n)^* Rh_{total,*} K = Rh_{n,*} g_n^* K.

The source's equality is read as a natural isomorphism of functors on the derived category. Both sides are right derived functors of one and the same functor on the unbounded homotopy category of 𝒪-modules, by isRightDerivedFunctor_derivedTotalPushforwardRestrictModulesUnit and isRightDerivedFunctor_derivedRestrictTotalPushforwardModulesUnit of this namespace, the two being identified by the canonical comparison of Stacks 0DH0, componentPushforwardModulesIso. The isomorphism is the induced comparison of the two right derived functors, pinned down by derivedComponentPushforwardModulesIso_fac.

def derivedComponentPushforwardModulesIso
    (h : SimplicialSite.RingedMorphism C C' (C.totalRingSheaf O) (C'.totalRingSheaf O'))
    (n : SimplexCategory) :
    derivedTotalPushforwardModules h ⋙
        C'.situation.derivedComponentPullbackModules O' n ≅
      C.situation.derivedComponentPullbackModules O n ⋙
        derivedComponentPushforwardModules h n

CategoryTheory.SimplicialSiteSituation.componentPullbackModules_preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphismDerivedPushforward.lean, line 242. The attribute's comment: “exactness of the pullback of modules to a component”. References: SGA 4 IV (13.7), “special case”.

Pullback of sheaves of modules to the simplicial component of degree n is left exact. The component structure sheaf is the restriction of the total one, so the component structure map is invertible and the pullback of modules has the inverse image of sheaves of sets as its underlying sheaf, by CategoryTheory.SimplicialSiteSituation.componentPullbackUnderlyingIso; the inverse image is left exact because g_n is a morphism of topoi, and the underlying-sheaf functor on sheaves of modules preserves finite limits and reflects isomorphisms, hence reflects finite limits.

This is the source's observation that g_n^* = g_n^{-1} is exact, which is what makes Lg_n^* computable on any representative complex.

theorem componentPullbackModules_preservesFiniteLimits :
    PreservesFiniteLimits (componentRingedToposHom S O n).toModulesHom.pullbackModules

CategoryTheory.SimplicialSiteSituation.componentPullbackModules_preservesFiniteColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphismDerivedPushforward.lean, line 264. The attribute's comment: “exactness of the pullback of modules to a component”.

Pullback of sheaves of modules to the simplicial component of degree n is right exact, being a left adjoint. This is the finite case of Stacks 03DC part (2).

theorem componentPullbackModules_preservesFiniteColimits :
    PreservesFiniteColimits (componentRingedToposHom S O n).toModulesHom.pullbackModules

CategoryTheory.CocontinuousSimplicialSite.RingedMorphism.derivedComponentPushforwardModulesIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphismDerivedPushforward.lean, line 543. The attribute's comment: “case (B)”.

Stacks 0DH1, case (B). With notation and hypotheses as in Stacks 0DH0: for K in the unbounded derived category of sheaves of 𝒪-modules on the total site,

(g'_n)^* Rh_{total,*} K = Rh_{n,*} g_n^* K.

The source's equality is read as a natural isomorphism of functors on the derived category. Both sides are right derived functors of one and the same functor on the unbounded homotopy category of 𝒪-modules, by isRightDerivedFunctor_derivedTotalPushforwardRestrictModulesUnit and isRightDerivedFunctor_derivedRestrictTotalPushforwardModulesUnit of this namespace, the two being identified by the canonical comparison of Stacks 0DH0, componentPushforwardModulesIso. The isomorphism is the induced comparison of the two right derived functors, pinned down by derivedComponentPushforwardModulesIso_fac.

def derivedComponentPushforwardModulesIso :
    derivedTotalPushforwardModules h ⋙
        C'.situation.derivedComponentPullbackModules O' n ≅
      C.situation.derivedComponentPullbackModules O n ⋙
        derivedComponentPushforwardModules h n

CategoryTheory.CocontinuousSimplicialSite.Morphism.derivedComponentPushforwardModulesIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphismDerivedPushforward.lean, line 749. The attribute's comment: “case (B)”.

Stacks 0DH1, case (B). With notation and hypotheses as in Stacks 0DH0: for K in the unbounded derived category of sheaves of 𝒪-modules on the total site,

(g'_n)^* Rh_{total,*} K = Rh_{n,*} g_n^* K.

The source's equality is read as a natural isomorphism of functors on the derived category. Both sides are right derived functors of one and the same functor on the unbounded homotopy category of 𝒪-modules, by isRightDerivedFunctor_derivedTotalPushforwardRestrictModulesUnit and isRightDerivedFunctor_derivedRestrictTotalPushforwardModulesUnit of this namespace, the two being identified by the underived comparison e.

The hypothesis e is the last assertion of Stacks 0DH0 at the level of sheaves of modules, and hK is Stacks 09WH for sheaves of modules; see the implementation notes of this file for why both are deferred.

def derivedComponentPushforwardModulesIso
    (e : (h.totalRingedToposHom φ).pushforwardModules ⋙
        (C'.situation.componentRingedToposHom O' n).toModulesHom.pullbackModules ≅
      (C.situation.componentRingedToposHom O n).toModulesHom.pullbackModules ⋙
        ((h.componentRingedToposHom φ) n).pushforwardModules)
    (hK : ∀ I : CochainComplex (SheafOfModules.{u}
        ((Stacks.SheafOfModules.Tensor.ringSheaf (J := (C.situation.totalRingedTopos O).J)
            (C.situation.totalRingedTopos O).O))) ℤ,
      I.IsKInjective →
        CochainComplex.IsKInjective
          (((C.situation.componentRingedToposHom O n).toModulesHom.pullbackModules
              |>.mapHomologicalComplex (ComplexShape.up ℤ)).obj I)) :
    derivedTotalPushforwardModules h φ ⋙
        C'.situation.derivedComponentPullbackModules O' n ≅
      C.situation.derivedComponentPullbackModules O n ⋙
        derivedComponentPushforwardModules h φ n

CategoryTheory.CocontinuousSimplicialSite.Morphism.derivedComponentPushforwardModulesIso_fac, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphismDerivedPushforward.lean, line 780. The attribute's comment: “case (B), the canonical comparison”.

Stacks 0DH1, the isomorphism is the canonical one. Composing the canonical comparison into the first right derived functor with the isomorphism gives the underived comparison followed by the canonical comparison into the second. Since a morphism out of a right derived functor is determined by that identity, this pins the isomorphism down completely.

theorem derivedComponentPushforwardModulesIso_fac
    (e : (h.totalRingedToposHom φ).pushforwardModules ⋙
        (C'.situation.componentRingedToposHom O' n).toModulesHom.pullbackModules ≅
      (C.situation.componentRingedToposHom O n).toModulesHom.pullbackModules ⋙
        ((h.componentRingedToposHom φ) n).pushforwardModules)
    (hK : ∀ I : CochainComplex (SheafOfModules.{u}
        ((Stacks.SheafOfModules.Tensor.ringSheaf (J := (C.situation.totalRingedTopos O).J)
            (C.situation.totalRingedTopos O).O))) ℤ,
      I.IsKInjective →
        CochainComplex.IsKInjective
          (((C.situation.componentRingedToposHom O n).toModulesHom.pullbackModules
              |>.mapHomologicalComplex (ComplexShape.up ℤ)).obj I)) :
    derivedTotalPushforwardRestrictModulesUnit h φ n ≫
        Functor.whiskerLeft DerivedCategory.Qh
          (derivedComponentPushforwardModulesIso h φ n e hK).hom =
      (Functor.isoWhiskerRight (homotopyComponentPushforwardModulesIso h φ n e)
            DerivedCategory.Qh).hom ≫
        derivedRestrictTotalPushforwardModulesUnit h φ n

CategoryTheory.CocontinuousSimplicialSite.Morphism.derivedComponentPushforwardModulesIsoOfSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphismDerivedPushforward.lean, line 831. The attribute's comment: “case (B), over the canonical comparison of the degreewise square”.

Stacks 0DH1, case (B), over the canonical comparison of the degreewise square. With notation and hypotheses as in Stacks 0DH0: for K in the unbounded derived category of sheaves of 𝒪-modules on the total site,

(g'_n)^* Rh_{total,*} K = Rh_{n,*} g_n^* K.

This is derivedComponentPushforwardModulesIso with the underived comparison taken to be the canonical one of CategoryTheory.CocontinuousSimplicialSite.Morphism.componentPushforwardModulesIso, rather than an arbitrary isomorphism. The only hypothesis is hK, Stacks 09WH for sheaves of modules; see the implementation notes of this file.

def derivedComponentPushforwardModulesIsoOfSquare
    (hK : ∀ I : CochainComplex (SheafOfModules.{u}
        ((Stacks.SheafOfModules.Tensor.ringSheaf (J := (C.situation.totalRingedTopos O).J)
            (C.situation.totalRingedTopos O).O))) ℤ,
      I.IsKInjective →
        CochainComplex.IsKInjective
          (((C.situation.componentRingedToposHom O n).toModulesHom.pullbackModules
              |>.mapHomologicalComplex (ComplexShape.up ℤ)).obj I)) :
    derivedTotalPushforwardModules h φ ⋙
        C'.situation.derivedComponentPullbackModules O' n ≅
      C.situation.derivedComponentPullbackModules O n ⋙
        derivedComponentPushforwardModules h φ n

CategoryTheory.CocontinuousSimplicialSite.Morphism.derivedComponentPushforwardModulesIsoOfSquare_fac, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/RingedToposMorphismDerivedPushforward.lean, line 853. The attribute's comment: “case (B), the canonical comparison of the degreewise square pins the isomorphism”.

Stacks 0DH1, case (B) over the canonical comparison: the isomorphism is pinned by the canonical comparison of the degreewise square. Composing the canonical comparison into the first right derived functor with it gives the canonical underived comparison, applied degreewise to complexes, followed by the canonical comparison into the second right derived functor. Since a morphism out of a right derived functor is determined by that identity, this determines the isomorphism completely from the square of ringed topoi.

theorem derivedComponentPushforwardModulesIsoOfSquare_fac
    (hK : ∀ I : CochainComplex (SheafOfModules.{u}
        ((Stacks.SheafOfModules.Tensor.ringSheaf (J := (C.situation.totalRingedTopos O).J)
            (C.situation.totalRingedTopos O).O))) ℤ,
      I.IsKInjective →
        CochainComplex.IsKInjective
          (((C.situation.componentRingedToposHom O n).toModulesHom.pullbackModules
              |>.mapHomologicalComplex (ComplexShape.up ℤ)).obj I)) :
    derivedTotalPushforwardRestrictModulesUnit h φ n ≫
        Functor.whiskerLeft DerivedCategory.Qh
          (derivedComponentPushforwardModulesIsoOfSquare h φ n hK).hom =
      (Functor.isoWhiskerRight
            (homotopyComponentPushforwardModulesIso h φ n
              (componentPushforwardModulesIso h φ n)) DerivedCategory.Qh).hom ≫
        derivedRestrictTotalPushforwardModulesUnit h φ n
Sources
LeanCategoryTheory.CocontinuousSimplicialSite.RingedMorphism · CategoryTheory.CocontinuousSimplicialSite.RingedMorphism.ringHomEquiv · CategoryTheory.SimplicialSite.RingedMorphism · CategoryTheory.SimplicialSite.RingedMorphism.ringHomEquiv · CategoryTheory.SimplicialSiteMorphism.ringHomEquiv · CategoryTheory.SimplicialSiteSituation.RingedMorphism · CategoryTheory.SimplicialSiteSituation.componentPullbackUnderlyingIso · CategoryTheory.SimplicialSiteSituation.componentPullbackUnderlyingIso_unit

Section85.8 Cohomology on simplicial sites#

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

Tag 09WI, a lemma

Tag 09WI in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.simplicialIntegerResolution, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/IntegerResolution.lean, line 2511. The attribute's comment: “the resolution”. References: SGA 4 VIII (8.2), “resolution of Z”.

Stacks 09WI. The lower shriek images of the constant integer sheaves form an alternating-face resolution of the constant integer sheaf on the total site.

noncomputable def simplicialIntegerResolution (S : SimplicialSiteSituation.{u}) :
    SimplicialIntegerResolution S

CategoryTheory.SimplicialSiteSituation.simplicialIntegerComplex, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/IntegerResolution.lean, line 2528. The attribute's comment: “the complex”.

The alternating-face chain complex … → g_{2!} Z → g_{1!} Z → g_{0!} Z of the simplicial resolution of Stacks 09WI.

noncomputable abbrev simplicialIntegerComplex (S : SimplicialSiteSituation.{u}) :
    ChainComplex (Sheaf S.totalTopology Ab.{u}) ℕ
Tag 0D77, a lemma

Tag 0D77 in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.cechSectionsComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/SectionsComplex.lean, line 225. The attribute's comment: “the canonical complex”.

The canonical complex Γ(C_0, F_0) → Γ(C_1, F_1) → Γ(C_2, F_2) → … of an abelian sheaf F on the total site of a simplicial site, functorially in F. Its augmentation by Γ(C_total, F) is cechSectionsAugmentation.

def cechSectionsComplex : Sheaf S.totalTopology Ab.{u} ⥤ CochainComplex Ab.{u} ℕ

CategoryTheory.SimplicialSiteSituation.cechSectionsAugmentation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/SectionsComplex.lean, line 260. The attribute's comment: “the augmentation”.

The augmentation Γ(C_total, F) → Γ(C_0, F_0) of the canonical complex, natural in the abelian sheaf F. It is the canonical restriction of a global section to simplicial degree zero; see cechSectionsAugmentation_eq.

def cechSectionsAugmentation :
    Sheaf.Γ S.totalTopology Ab.{u} ⟶ S.componentSectionsFunctor ⦋0⦌

CategoryTheory.SimplicialSiteSituation.cechSectionsAugmentation_app_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/SectionsComplex.lean, line 298. The attribute's comment: “exactness in degree -1”.

Exactness in degree -1: the augmentation Γ(C_total, F) → Γ(C_0, F_0) of the canonical complex is a monomorphism.

theorem cechSectionsAugmentation_app_mono (F : Sheaf S.totalTopology Ab.{u}) :
    Mono ((S.cechSectionsAugmentation).app F)

CategoryTheory.SimplicialSiteSituation.cechSectionsAugmentation_app_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/SectionsComplex.lean, line 309. The attribute's comment: “exactness in degree -1”.

Exactness in degree -1, concretely: the augmentation Γ(C_total, F) → Γ(C_0, F_0) of the canonical complex is injective.

theorem cechSectionsAugmentation_app_injective (F : Sheaf S.totalTopology Ab.{u}) :
    Function.Injective ((S.cechSectionsAugmentation).app F)

CategoryTheory.SimplicialSiteSituation.cechSectionsComplex_exactAt_of_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/SectionsComplex.lean, line 377. The attribute's comment: “exactness in positive degrees for an injective sheaf”.

Exactness in positive degrees for an injective sheaf: if F is an injective abelian sheaf on the total site, the canonical complex Γ(C_0, F_0) → Γ(C_1, F_1) → Γ(C_2, F_2) → … is exact at Γ(C_n, F_n) for every n > 0.

theorem cechSectionsComplex_exactAt_of_injective (F : Sheaf S.totalTopology Ab.{u})
    [Injective F] (n : ℕ) (hn : 0 < n) :
    ((S.cechSectionsComplex).obj F).ExactAt n

CategoryTheory.SimplicialSiteSituation.cechSectionsComplex_shortComplexZero_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/SectionsComplex.lean, line 401. The attribute's comment: “exactness in degree 0”.

Exactness in degree 0: the sequence Γ(C_total, F) → Γ(C_0, F_0) → Γ(C_1, F_1) is exact at Γ(C_0, F_0).

theorem cechSectionsComplex_shortComplexZero_exact (F : Sheaf S.totalTopology Ab.{u}) :
    (ShortComplex.mk ((S.cechSectionsAugmentation).app F)
      (((S.cechSectionsComplex).obj F).d 0 1)
      (S.cechSectionsAugmentation_comp_d F)).Exact
Tag 09WJ, a lemma

Tag 09WJ in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.derivedSpectralSequence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CohomologySpectralSequenceTagDerived.lean, line 202. The attribute's comment: “the spectral sequence for K in D^+(C_total), as a functor of K”.

Stacks 09WJ, the spectral sequence. For an object K of D^+(C_total) there is a cohomological spectral sequence, functorial in K: the right derived functor, along the localization of the bounded below homotopy category at the quasi-isomorphisms, of the spectral sequence of the double complex A^{q,p} = Γ(C_p, Z^q_p) read from its first page.

A bounded below complex of injectives I^• representing K is exactly an object at which the unit of this right derived functor is invertible (isIso_derivedSpectralSequenceUnit_app), so the value at K is the spectral sequence of the double complex A^{q,p} = Γ(C_p, I^q_p) of the source's proof.

def derivedSpectralSequence :
    DerivedCategory.Plus (Sheaf S.totalTopology Ab.{u}) ⥤
      CohomologicalSpectralSequence Ab.{u} 1

CategoryTheory.SimplicialSiteSituation.derivedSpectralSequence_pageOneIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CohomologySpectralSequenceTagDerived.lean, line 395. The attribute's comment: “the first page E_1^{p,q} = H^q(C_p, K_p) for K in D^+(C_total), naturally in K”.

Stacks 09WJ, the first page. E_1^{p,q} = H^q(C_p, K_p): the first page of the spectral sequence of Stacks 09WJ at (p, q) is the sheaf cohomology on the component site C_p of the restriction of K to C_p, naturally in the object K of D^+(C_total).

Together with isZero_derivedPageOne_d_of_ne, which pins the shape of d_1^{p,q} : E_1^{p,q} → E_1^{p+1,q}, this is the first page and the first differential of Stacks 09WJ.

def derivedSpectralSequence_pageOneIso :
    S.derivedSpectralSequence ⋙ pageOneEval (n : ℤ) q ≅
      S.componentDerivedCohomologyFunctor n q

CategoryTheory.SimplicialSiteSituation.isZero_derivedPageOne_d_of_ne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CohomologySpectralSequenceTagDerived.lean, line 411. The attribute's comment: “the first differential d_1^{p,q} : E_1^{p,q} → E_1^{p+1,q} for K in D^+(C_total)”.

Stacks 09WJ, the first differential. d_1^{p,q} : E_1^{p,q} → E_1^{p+1,q}: the differential of the first page out of the bidegree (p, q) lands in the bidegree (p + 1, q), every other component being zero. Together with the type of CategoryTheory.SimplicialSiteSituation.derivedSpectralSequence, which provides d (p, q) (p + 1, q) : E_1^{p,q} ⟶ E_1^{p+1,q}, this is the shape of d_1 that Stacks 09WJ asserts.

theorem isZero_derivedPageOne_d_of_ne (K : DerivedCategory.Plus (Sheaf S.totalTopology Ab.{u}))
    (p q p' q' : ℤ) (h : (p', q') ≠ (p + 1, q)) :
    ((S.derivedSpectralSequence.obj K).page 1 le_rfl).d (p, q) (p', q') = 0

CategoryTheory.SimplicialSiteSituation.derivedSpectralSequence_abutsTo, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CohomologySpectralSequenceTagDerived.lean, line 488. The attribute's comment: “the abutment H^{p+q}(C_total, K) for K in D^+(C_total)”.

Stacks 09WJ, the convergence. The spectral sequence of Stacks 09WJ abuts to H^{p+q}(C_total, K): its infinity page at (p, q) is the p-th graded piece of a finite filtration of the sheaf cohomology of the total site in degree p + q.

Every object of D^+(C_total) is represented by a bounded below complex of injective abelian sheaves -- the inclusion of the bounded below homotopy category of complexes of injectives into D^+(C_total) is essentially surjective -- and at such a complex the convergence is derivedSpectralSequence_abutsTo_of_injective.

theorem derivedSpectralSequence_abutsTo
    (K : DerivedCategory.Plus (Sheaf S.totalTopology Ab.{u})) :
    CategoryTheory.SpectralSequence.AbutsTo (S.derivedSpectralSequence.obj K)
      (fun n => (S.totalDerivedCohomologyFunctor n).obj K)

CategoryTheory.SimplicialSiteSituation.cohomologySpectralSequence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CohomologySpectralSequenceTagSheaf.lean, line 168. The attribute's comment: “the spectral sequence, for an abelian sheaf on the total site, functorial in it”.

Stacks 09WJ, the spectral sequence. For an abelian sheaf F on the total site of a simplicial-site situation there is a cohomological spectral sequence, functorial in F: the spectral sequence of the filtration by the simplicial coordinate of the double complex A^{q,p} = Γ(C_p, I^q_p) of the chosen injective resolution of F, presented from its first page.

The functor laws hold because filtered homotopic morphisms of double complexes induce the same maps on the pages from the first on; an injective resolution is functorial only up to homotopy, which is why the presentation starts at the first page.

def cohomologySpectralSequence :
    Sheaf S.totalTopology Ab.{u} ⥤ CohomologicalSpectralSequence Ab.{u} 1

CategoryTheory.SimplicialSiteSituation.cohomologySpectralSequence_pageOneIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CohomologySpectralSequenceTagSheaf.lean, line 298. The attribute's comment: “the first page E_1^{p,q} = H^q(C_p, F_p) for an abelian sheaf, naturally in it”.

Stacks 09WJ, the first page. E_1^{p,q} = H^q(C_p, F_p): the first page of the spectral sequence of the simplicial-site situation at (p, q) is the sheaf cohomology of the restriction of F to the component site C_p, naturally in the abelian sheaf F.

Together with CategoryTheory.SimplicialSiteSituation.pageOneIsoColumnHomology_hom_d, which identifies d_1^{p,q} : E_1^{p,q} → E_1^{p+1,q} with the differential of the complex of Stacks 0D77, this is the first page and the first differential of Stacks 09WJ.

def cohomologySpectralSequence_pageOneIso :
    S.pageOneFunctor n q ≅ S.componentCohomologyFunctor ⦋n⦌ q

CategoryTheory.SimplicialSiteSituation.isZero_pageOne_d_of_ne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CohomologySpectralSequenceTagSheaf.lean, line 323. The attribute's comment: “the first differential d_1^{p,q} : E_1^{p,q} → E_1^{p+1,q}”.

Stacks 09WJ, the first differential. d_1^{p,q} : E_1^{p,q} → E_1^{p+1,q}: the differential of the first page out of the bidegree (p, q) lands in the bidegree (p + 1, q), every other component being zero. Together with the type of CategoryTheory.SimplicialSiteSituation.cohomologySpectralSequence, which provides d (p, q) (p + 1, q) : E_1^{p,q} ⟶ E_1^{p+1,q}, this is the shape of d_1 that Stacks 09WJ asserts.

What that differential is under the identification of the first page is CategoryTheory.SimplicialSiteSituation.pageOneIsoColumnHomology_hom_d: up to the sign (-1)^q, the map induced on H^q by the differential of the complex of Stacks 0D77.

theorem isZero_pageOne_d_of_ne (F : Sheaf S.totalTopology Ab.{u}) (p q p' q' : ℤ)
    (h : (p', q') ≠ (p + 1, q)) :
    (((S.cohomologySpectralSequence).obj F).page 1 le_rfl).d (p, q) (p', q') = 0

CategoryTheory.SimplicialSiteSituation.cohomologySpectralSequence_abutsTo, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CohomologySpectralSequenceTagSheaf.lean, line 364. The attribute's comment: “the abutment H^{p+q}(C_total, F) for an abelian sheaf”.

Stacks 09WJ, the convergence. The spectral sequence of the simplicial-site situation abuts to H^{p+q}(C_total, F): its infinity page at (p, q) is the p-th graded piece of a finite filtration of the sheaf cohomology of the total site in degree p + q.

This is sectionsSpectralSequence_abutsTo_total, whose abutment is the cohomology of the total complex of A^{•,•}, transported along the comparison of Stacks 0133 and read from the first page.

theorem cohomologySpectralSequence_abutsTo :
    CategoryTheory.SpectralSequence.AbutsTo
      ((S.cohomologySpectralSequence).obj F) (S.totalCohomologyZ F)
Tag 0H0V, a remark

Tag 0H0V in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.sectionsProductSpectralSequence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CohomologySpectralSequence.lean, line 362. The attribute's comment: “the spectral sequence of the filtration by the simplicial coordinate of the product totalization, for a complex that is not bounded below; the identification of the first page with H^q(C_p, K_p) is not carried”.

Stacks 0H0V, the spectral sequence. For a cochain complex Z^• of abelian sheaves on the total site of a simplicial-site situation, with no boundedness hypothesis, the filtration F^i Tot_π^n = ∏_{p + q = n, p ≥ i} Γ(C_p, Z^q_p) of the product totalization of A^{p,q} = Γ(C_p, Z^q_p) by the simplicial coordinate has a spectral sequence.

For Z^• a K-injective complex of injectives representing K in D(C_total) this is the spectral sequence the source constructs; as in the source, no convergence is asserted.

def sectionsProductSpectralSequence : CohomologicalSpectralSequence Ab.{u} 0

CategoryTheory.SimplicialSiteSituation.sectionsProductSpectralSequenceZeroPageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CohomologySpectralSequence.lean, line 372. The attribute's comment: “the zeroth page of the spectral sequence is Γ(C_p, Z^q_p)”.

E_0^{p,q} = Γ(C_p, Z^q_p): the zeroth page of the spectral sequence of Stacks 0H0V is the complex of sections over C_p of the restriction of Z^q.

The isomorphism is pinned by HomologicalComplex₂.π_productTotalColumnZeroPageIso_hom: it carries the class of an element of F^p Tot_π^{p+q} to its component in simplicial degree p.

def sectionsProductSpectralSequenceZeroPageIso (p : ℕ) (q : ℤ) :
    ((S.sectionsProductSpectralSequence Z).page 0 le_rfl).X ((p : ℤ), q) ≅
      (S.componentSectionsFunctor ⦋p⦌).obj (Z.X q)

CategoryTheory.SimplicialSiteSituation.sectionsProductSpectralSequenceOnePageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CohomologySpectralSequence.lean, line 381. The attribute's comment: “the first page of the spectral sequence is H^q(Γ(C_p, Z^•_p))”.

E_1^{p,q} = H^q(Γ(C_p, Z^•_p)): the first page of the spectral sequence of Stacks 0H0V is the q-th cohomology of the complex of sections over C_p of the restriction of Z^•, not the H^q(C_p, K_p) of the statement of Stacks 0H0V.

def sectionsProductSpectralSequenceOnePageIso (p : ℕ) (q : ℤ) :
    ((S.sectionsProductSpectralSequence Z).page 1 zero_le_one).X ((p : ℤ), q) ≅
      (((S.componentSectionsFunctor ⦋p⦌).mapHomologicalComplex
        (ComplexShape.up ℤ)).obj Z).homology q

CategoryTheory.SimplicialSiteSituation.sectionsProductSpectralSequencePageOneAddEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CohomologySpectralSequenceUnbounded.lean, line 253. The attribute's comment: “the first page of the spectral sequence is H^q(C_p, K_p), for a complex that is not bounded below”.

Stacks 0H0V, the first page: E_1^{p,q} = H^q(C_p, K_p). For I^• a K-injective complex of abelian sheaves on the total site representing K in D(C_total), the first page of the spectral sequence of the filtration by the simplicial coordinate of the product totalization of A^{p,q} = Γ(C_p, I^q_p) is the cohomology of the component site C_p of the restriction K_p.

No boundedness hypothesis is made on I^•, as in the source. Cohomology is written in its derived-Hom form, and K_p is the restriction of K = Q(I^•) to the component in simplicial degree p; the proof uses that restriction to a component preserves K-injectivity, which is Stacks 09WH.

def sectionsProductSpectralSequencePageOneAddEquiv
    (I : CochainComplex (Sheaf S.totalTopology Ab.{u}) ℤ) [I.IsKInjective] (p : ℕ) (q : ℤ) :
    (((S.sectionsProductSpectralSequence I).page 1 zero_le_one).X ((p : ℤ), q)) ≃+
      ((DerivedCategory.singleFunctor (Sheaf (S.componentTopology ⦋p⦌) Ab.{u}) 0).obj
          (integerSheaf (S.componentTopology ⦋p⦌)) ⟶
        ((S.componentRestrictionDerived ⦋p⦌).obj (DerivedCategory.Q.obj I))⟦q⟧)

CategoryTheory.SimplicialSiteSituation.quasiIso_totalSectionsToProductTotal, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CohomologySpectralSequenceUnbounded.lean, line 313. The attribute's comment: “Tot_π(A^{•,•}) = RΓ(C_total, K) for a K-injective representative, as a quasi-isomorphism of complexes”.

Stacks 0H0V, Tot_π(A^{•,•}) = RΓ(C_total, K). For I^• a K-injective complex of abelian sheaves on the total site, the comparison from the complex of global sections Γ(C_total, I^•) — which is RΓ(C_total, K) for K = Q(I^•) — to the product totalization of A^{p,q} = Γ(C_p, I^q_p) is a quasi-isomorphism.

This is the source's chain of equalities. The global sections complex is the Hom complex out of the constant integer sheaf Z, which is R Hom(Z, K); the integral resolution … → g_{2!}Z → g_{1!}Z → g_{0!}Z of Stacks 09WI resolves Z, so for the K-injective target I^• the Hom complex out of it computes the same thing; and that Hom complex is the product totalization of A^{p,q} = Hom(g_{p!}Z, I^q) = Γ(C_p, I^q_p). No boundedness hypothesis is made on I^•: K-injectivity is what replaces it.

instance quasiIso_totalSectionsToProductTotal
    (I : CochainComplex (Sheaf S.totalTopology Ab.{u}) ℤ) [I.IsKInjective] :
    QuasiIso (S.totalSectionsToProductTotal I)

CategoryTheory.SimplicialSiteSituation.sectionsProductTotalHomologyAddEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CohomologySpectralSequenceUnbounded.lean, line 328. The attribute's comment: “H^n(Tot_π(A^{•,•})) = H^n(C_total, K) for a K-injective representative”.

Stacks 0H0V, Tot_π(A^{•,•}) = RΓ(C_total, K) degreewise on cohomology: H^n(Tot_π(A^{•,•})) = H^n(C_total, K).

Cohomology is written in its derived-Hom form, so the right-hand side is literally the source's R Hom(Z, K) in degree n, which is RΓ(C_total, K) because the first equality of the source "holds in any site".

def sectionsProductTotalHomologyAddEquiv
    (I : CochainComplex (Sheaf S.totalTopology Ab.{u}) ℤ) [I.IsKInjective] (n : ℤ) :
    ((S.sectionsProductTotal I).homology n) ≃+
      ((DerivedCategory.singleFunctor (Sheaf S.totalTopology Ab.{u}) 0).obj S.totalIntegerSheaf ⟶
        (DerivedCategory.Q.obj I)⟦n⟧)

CategoryTheory.SimplicialSiteSituation.quasiIso_globalSectionsToProductTotal, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CohomologySpectralSequenceUnbounded.lean, line 355. The attribute's comment: “Γ(C_total, I^•) = Tot_π(A^{•,•}) for a K-injective complex, as a quasi-isomorphism of complexes”.

Stacks 0H0V, Γ(C_total, I^•) = Tot_π(A^{•,•}). For I^• a K-injective complex of abelian sheaves on the total site, the comparison from its complex of global sections to the product totalization of A^{p,q} = Γ(C_p, I^q_p) is a quasi-isomorphism. This is the previous statement with its source written as the complex of global sections rather than as the Hom complex out of the constant integer sheaf.

instance quasiIso_globalSectionsToProductTotal
    (I : CochainComplex (Sheaf S.totalTopology Ab.{u}) ℤ) [I.IsKInjective] :
    QuasiIso (S.globalSectionsToProductTotal I)

CategoryTheory.SimplicialSiteSituation.unboundedSpectralSequence, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CohomologySpectralSequenceUnbounded.lean, line 369. The attribute's comment: “the spectral sequence of an arbitrary object of the unbounded derived category of the total site”.

Stacks 0H0V, the spectral sequence of an object K of D(C_total) with no boundedness hypothesis: the spectral sequence of CategoryTheory.SimplicialSiteSituation.sectionsProductSpectralSequence for the chosen K-injective complex with injective terms representing K.

abbrev unboundedSpectralSequence (K : DerivedCategory (Sheaf S.totalTopology Ab.{u})) :
    CohomologicalSpectralSequence Ab.{u} 0

CategoryTheory.SimplicialSiteSituation.unboundedSpectralSequencePageOneAddEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CohomologySpectralSequenceUnbounded.lean, line 381. The attribute's comment: “the first page is E_1^{p,q} = H^q(C_p, K_p), for an arbitrary object of the unbounded derived category of the total site”.

Stacks 0H0V, the first page: E_1^{p,q} = H^q(C_p, K_p) for an arbitrary object K of D(C_total).

The first differential of the first page of a cohomological spectral sequence has bidegree (1, 0) by construction, so under this identification it is a map H^q(C_p, K_p) → H^q(C_{p + 1}, K_{p + 1}), as the source's reference to Stacks 09WJ asks.

def unboundedSpectralSequencePageOneAddEquiv
    (K : DerivedCategory (Sheaf S.totalTopology Ab.{u})) (p : ℕ) (q : ℤ) :
    (((S.unboundedSpectralSequence K).page 1 zero_le_one).X ((p : ℤ), q)) ≃+
      ((DerivedCategory.singleFunctor (Sheaf (S.componentTopology ⦋p⦌) Ab.{u}) 0).obj
          (integerSheaf (S.componentTopology ⦋p⦌)) ⟶
        ((S.componentRestrictionDerived ⦋p⦌).obj K)⟦q⟧)

CategoryTheory.SimplicialSiteSituation.unboundedProductTotalHomologyAddEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/CohomologySpectralSequenceUnbounded.lean, line 398. The attribute's comment: “H^n(Tot_π(A^{•,•})) = H^n(C_total, K) for an arbitrary object of the unbounded derived category of the total site”.

Stacks 0H0V, Tot_π(A^{•,•}) = RΓ(C_total, K) for an arbitrary object K of D(C_total), degreewise on cohomology.

def unboundedProductTotalHomologyAddEquiv
    (K : DerivedCategory (Sheaf S.totalTopology Ab.{u})) (n : ℤ) :
    ((S.sectionsProductTotal (S.totalKInjectiveModel K)).homology n) ≃+
      ((DerivedCategory.singleFunctor (Sheaf S.totalTopology Ab.{u}) 0).obj S.totalIntegerSheaf ⟶
        K⟦n⟧)
Tag 0H0W, a lemma

Tag 0H0W in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.subsingleton_hom_totalIntegerSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/VanishingCohomology.lean, line 704. The attribute's comment: “part (1): vanishing of H^0”.

Stacks 0H0W (1). In the situation of Stacks 09WE, let K be an object of D(C_total). If H^{-p}(C_p, K_p) = 0 for all p ≥ 0, then H^0(C_total, K) = 0.

Cohomology is written in its derived-Hom form: H^i(C, K) is the group of morphisms from the constant integer sheaf of C, placed in degree zero, to K[i]; and the restriction K_p of K to the component in simplicial degree p is componentRestrictionDerived S ⦋p⦌ applied to K.

theorem subsingleton_hom_totalIntegerSheaf
    (K : DerivedCategory (Sheaf S.totalTopology Ab.{u}))
    (h : ∀ p : ℕ, Subsingleton
      ((DerivedCategory.singleFunctor (Sheaf (S.componentTopology ⦋p⦌) Ab.{u}) 0).obj
          (integerSheaf (S.componentTopology ⦋p⦌)) ⟶
        ((componentRestrictionDerived S ⦋p⦌).obj K)⟦-(p : ℤ)⟧)) :
    Subsingleton ((DerivedCategory.singleFunctor (Sheaf S.totalTopology Ab.{u}) 0).obj
      S.totalIntegerSheaf ⟶ K)

CategoryTheory.SimplicialSiteSituation.subsingleton_hom_totalIntegerSheaf_shift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/VanishingCohomology.lean, line 745. The attribute's comment: “part (2): vanishing of RΓ”.

Stacks 0H0W (2). In the situation of Stacks 09WE, let K be an object of D(C_total). If RΓ(C_p, K_p) = 0 for all p ≥ 0, then RΓ(C_total, K) = 0.

Vanishing of RΓ is the vanishing of every cohomology group, written in derived-Hom form as in subsingleton_hom_totalIntegerSheaf.

theorem subsingleton_hom_totalIntegerSheaf_shift
    (K : DerivedCategory (Sheaf S.totalTopology Ab.{u}))
    (h : ∀ (p : ℕ) (i : ℤ), Subsingleton
      ((DerivedCategory.singleFunctor (Sheaf (S.componentTopology ⦋p⦌) Ab.{u}) 0).obj
          (integerSheaf (S.componentTopology ⦋p⦌)) ⟶
        ((componentRestrictionDerived S ⦋p⦌).obj K)⟦i⟧)) (i : ℤ) :
    Subsingleton ((DerivedCategory.singleFunctor (Sheaf S.totalTopology Ab.{u}) 0).obj
      S.totalIntegerSheaf ⟶ K⟦i⟧)
Tag 0DBZ, a lemma

Tag 0DBZ in the Stacks Project.

Stacks.Cohomology.SimplicialComponent.cohomologyObj_iso_component, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/ComponentSumNaturality/ComponentCohomology.lean, line 141.

Stacks 0DBZ. Cohomology over an object of one simplicial component agrees with cohomology over the corresponding object of the total site, with coefficients restricted to that component.

The restriction is the pullback of sheaves along the cocontinuous component inclusion. This is Stacks 03YU statement 2 — Stacks.Cohomology.BiggerSite.cohomologyObjIso, read at an arbitrary Ext universe as cohomologyObjIsoExtUniv — applied to the component inclusion, whose exactness hypothesis is Stacks 09WG (7), Stacks.Sites.ComponentSumFormula.preservesMonomorphisms_sheafPullback_componentFunctor.

def cohomologyObj_iso_component
    (S : SimplicialSiteSituation.{u}) (n : SimplexCategory) (U : S.component n)
    [HasSheafify S.totalTopology Ab.{u}]
    [HasSheafify (S.componentTopology n) Ab.{u}]
    [HasExt.{w} (Sheaf S.totalTopology Ab.{u})]
    [HasExt.{w} (Sheaf (S.componentTopology n) Ab.{u})]
    (F : Sheaf S.totalTopology Ab.{u}) (p : ℕ) :
    Sheaf.H'.{w, u, u} F p ((SimplicialSiteSituation.componentFunctor S n).obj U) ≅
      Sheaf.H'.{w, u, u}
        (((SimplicialSiteSituation.componentFunctor S n).sheafPullbackCocontinuous
          Ab.{u} (S.componentTopology n) S.totalTopology).obj F) p U
Sources
LeanCategoryTheory.SimplicialSiteSituation.simplicialIntegerResolution · CategoryTheory.SimplicialSiteSituation.simplicialIntegerComplex · CategoryTheory.SimplicialSiteSituation.cechSectionsComplex · CategoryTheory.SimplicialSiteSituation.cechSectionsAugmentation · CategoryTheory.SimplicialSiteSituation.cechSectionsAugmentation_app_mono · CategoryTheory.SimplicialSiteSituation.cechSectionsAugmentation_app_injective · CategoryTheory.SimplicialSiteSituation.cechSectionsComplex_exactAt_of_injective · CategoryTheory.SimplicialSiteSituation.cechSectionsComplex_shortComplexZero_exact

Section85.9 Cohomology and augmentations of simplicial sites#

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

Tag 0D78, a lemma

Tag 0D78 in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.Augmentation.resolution, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/AugmentationResolutionTerms.lean, line 939.

Stacks 0D78. The exact complex … ⟶ g_{1!}(a_1⁻¹𝒢) ⟶ g_{0!}(a_0⁻¹𝒢) ⟶ a⁻¹𝒢 ⟶ 0 of abelian sheaves on the total site: the alternating-face complex of the simplex-coefficient resolution of a⁻¹𝒢, whose degree-n term is the extension by zero g_{n!}(a_n⁻¹𝒢).

def resolution : Resolution S D K a G
Tag 0D79, a lemma

Tag 0D79 in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.Augmentation.augmentedCechComplex_exactAt_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/AugmentationCechComplex.lean, line 485. The attribute's comment: “exactness in degree -1”.

Exactness in degree -1: the complex

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

is exact at a_*F, which is Lean degree 0 because the augmentation shifts the complex by one.

theorem augmentedCechComplex_exactAt_zero : (augmentedCechComplex S D K a F).ExactAt 0

CategoryTheory.SimplicialSiteSituation.Augmentation.augmentedCechComplex_exactAt_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/AugmentationCechComplex.lean, line 496. The attribute's comment: “exactness in degree 0”.

Exactness in degree 0: the complex

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

is exact at a_{0,*}F_0, which is Lean degree 1 because the augmentation shifts the complex by one.

theorem augmentedCechComplex_exactAt_one : (augmentedCechComplex S D K a F).ExactAt 1

CategoryTheory.SimplicialSiteSituation.Augmentation.augmentedCechComplex_exactAt_of_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/AugmentationCechExact.lean, line 210. The attribute's comment: “exactness in every degree for an injective abelian sheaf”.

Stacks 0D79, exactness in every degree for an injective abelian sheaf: the complex

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

is exact at every term when F is an injective abelian sheaf on the total site. Degrees 0 and 1 — the source's degrees -1 and 0 — hold for every F and are augmentedCechComplex_exactAt_zero and augmentedCechComplex_exactAt_one. Above them the argument is the source's: a complex of abelian sheaves is exact at a term as soon as Hom(𝒢, -) of it is exact for every 𝒢, each term of this complex is a right adjoint whose left adjoint is the corresponding term of the resolution of Stacks 0D78, the mate of each cosimplicial transition is the corresponding structure map of that resolution, and Hom(-, F) of the resolution is exact because F is injective.

theorem augmentedCechComplex_exactAt_of_injective (F : Sheaf S.totalTopology Ab.{u})
    [Injective F] (k : ℕ) : (augmentedCechComplex S D K a F).ExactAt k
Tag 0D7A, a lemma

Tag 0D7A in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.Augmentation.higherDirectImageSpectralSequence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Simplicial/AugmentationDerivedSpectralSequence.lean, line 179.

Stacks 0D7A. For an augmentation a of a simplicial-site situation towards a site (D, K) and M in D⁺(C_total) there is a spectral sequence

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

functorial in M. It is the spectral sequence of the double complex A^{q,p} = a_{p,*} I^q_p of a bounded below complex of injectives I^• representing M, filtered by the simplicial degree.

def higherDirectImageSpectralSequence : HigherDirectImageSpectralSequence S D K a
Sources
LeanCategoryTheory.SimplicialSiteSituation.Augmentation.resolution · CategoryTheory.SimplicialSiteSituation.Augmentation.augmentedCechComplex_exactAt_zero · CategoryTheory.SimplicialSiteSituation.Augmentation.augmentedCechComplex_exactAt_one · CategoryTheory.SimplicialSiteSituation.Augmentation.augmentedCechComplex_exactAt_of_injective · CategoryTheory.SimplicialSiteSituation.Augmentation.higherDirectImageSpectralSequence

Section85.10 Cohomology on ringed simplicial sites#

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

Tag 0D9B, a lemma

Tag 0D9B in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.nonempty_simplicialModuleResolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/ModuleResolution.lean, line 1529.

Stacks 0D9B. There is a complex of modules over the structure sheaf of the total simplicial site whose term in degree n is the lower-shriek image g_{n!}𝒪_n of the n-th component structure sheaf, whose differentials are the canonical alternating face maps, and which is a resolution of the structure sheaf.

public theorem nonempty_simplicialModuleResolution (S : SimplicialSiteSituation.{u})
    (O : Sheaf S.totalTopology RingCat.{u}) :
    Nonempty (SimplicialModuleResolutionActual S O)
Tag 0D9C, a lemma

Tag 0D9C in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.SimplicialModuleResolution.sectionsComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/SectionsComplex.lean, line 207. The attribute's comment: “the complex”.

Stacks 0D9C. The canonical complex

0 → Γ(C_total, F) → Γ(C_0, F_0) → Γ(C_1, F_1) → …

obtained by applying Hom(-, F) to the resolution … → g_{1!} O_1 → g_{0!} O_0 → O. Its term in index 0 is Hom(O, F) = Γ(C_total, F) and its term in index n + 1 is Γ(C_n, F_n).

public def sectionsComplex : CochainComplex AddCommGrpCat.{u} ℕ

CategoryTheory.SimplicialSiteSituation.SimplicialModuleResolution.sectionsComplex_exactAt_le_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/SectionsComplex.lean, line 304. The attribute's comment: “exactness in degrees -1 and 0”.

Stacks 0D9C. The complex 0 → Γ(C_total, F) → Γ(C_0, F_0) → … is exact in degrees -1 and 0, i.e. in indices 0 and 1, for every sheaf of O-modules F.

public theorem sectionsComplex_exactAt_le_one (i : ℕ) (hi : i ≤ 1) :
    (D.sectionsComplex F).ExactAt i

CategoryTheory.SimplicialSiteSituation.SimplicialModuleResolution.sectionsComplex_acyclic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/SectionsComplex.lean, line 313. The attribute's comment: “exactness in all degrees for an injective module”.

Stacks 0D9C. The complex 0 → Γ(C_total, F) → Γ(C_0, F_0) → … is exact in every degree when F is an injective O-module.

public theorem sectionsComplex_acyclic [Injective F] : (D.sectionsComplex F).Acyclic
Tag 0D7E, a lemma

Tag 0D7E in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.SimplicialModuleResolution.exists_sectionsSpectralSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/ModuleCohomologySpectralSequence.lean, line 688.

Stacks 0D7E. In Situation 09WE let O be a sheaf of rings on the total site. For K in D⁺(O) there is a spectral sequence (E_r, d_r), functorial in K and presented from its first page, with

E_1^{p,q} = H^q(C_p, K_p), d_1^{p,q} : E_1^{p,q} → E_1^{p+1,q}

converging to H^{p+q}(C_total, K). Here K_p = g_p^* K is the restriction of K to the component C_p (Stacks 0D72), H^q(C_p, -) is the cohomology of RΓ(C_p, -) on D⁺(O_p) and H^n(C_total, -) that of RΓ(C_total, -) on D⁺(O), global sections of a sheaf of modules being those of its underlying abelian sheaf. The identification of the first page is natural in K, and the first page vanishes in the negative columns.

public theorem exists_sectionsSpectralSequence :
    ∃ E : DerivedCategory.Plus (SheafOfModules.{u} O) ⥤
        CohomologicalSpectralSequence AddCommGrpCat.{u} 1,
      (∀ (p : ℕ) (q : ℤ), Nonempty (E ⋙
          CategoryTheory.SpectralSequence.pageFunctor AddCommGrpCat.{u} _ 1 1 le_rfl ⋙
            HomologicalComplex.eval AddCommGrpCat.{u} _ ((p : ℤ), q) ≅
        (componentModuleRestriction S O ⦋p⦌).mapDerivedCategoryPlus ⋙
          (SheafOfModules.toSheaf (componentRingSheaf S O ⦋p⦌) ⋙
            Sheaf.Γ (S.componentTopology ⦋p⦌) AddCommGrpCat.{u}).rightDerivedFunctorPlus ⋙
            DerivedCategory.Plus.homologyFunctor AddCommGrpCat.{u} q)) ∧
      (∀ (K : DerivedCategory.Plus (SheafOfModules.{u} O)) (p q : ℤ), p < 0 →
        IsZero (((E.obj K).page 1 le_rfl).X (p, q))) ∧
      ∀ K : DerivedCategory.Plus (SheafOfModules.{u} O),
        CategoryTheory.SpectralSequence.AbutsTo (E.obj K)
          (fun n => (DerivedCategory.Plus.homologyFunctor AddCommGrpCat.{u} n).obj
            ((SheafOfModules.toSheaf O ⋙
              Sheaf.Γ S.totalTopology AddCommGrpCat.{u}).rightDerivedFunctorPlus.obj K))
Tag 0DH2, a lemma

Tag 0DH2 in the Stacks Project.

CategoryTheory.SimplicialSiteSituation.componentModuleCohomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/ModuleCohomology.lean, line 104.

In the situation of Stacks 09WE let O be a sheaf of rings on the total site, let U be an object of the degree-n component and let p : ℕ. For a sheaf of O-modules F one has H^p(U, g_n^*F) ≅ H^p(U, F), where on the right-hand side U is viewed as an object of the total category; the isomorphism is natural in F.

noncomputable def componentModuleCohomologyIso (U : S.component n) (p : ℕ) :
    componentModuleRestriction S O n ⋙ SheafOfModules.toSheaf.{u} (componentRingSheaf S O n) ⋙
        cohomology (S.componentTopology n) U p ≅
      SheafOfModules.toSheaf.{u} O ⋙
        cohomology S.totalTopology ((componentFunctor S n).obj U) p

CategoryTheory.SimplicialSiteSituation.componentModuleCohomologyObjIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/ModuleCohomology.lean, line 125.

H^p(U, g_n^*F) ≅ H^p(U, F) at a single sheaf of modules. For F a sheaf of O-modules on the total site of a simplicial-site situation and U an object of the degree-n component, H^p(U, g_n^*F) ≅ H^p(U, F) with U viewed on the right-hand side as an object of the total category.

noncomputable def componentModuleCohomologyObjIso (F : SheafOfModules.{u} O)
    (U : S.component n) (p : ℕ) :
    (cohomology (S.componentTopology n) U p).obj
        ((SheafOfModules.toSheaf.{u} (componentRingSheaf S O n)).obj
          ((componentModuleRestriction S O n).obj F)) ≅
      (cohomology S.totalTopology ((componentFunctor S n).obj U) p).obj
        ((SheafOfModules.toSheaf.{u} O).obj F)
Sources
LeanCategoryTheory.SimplicialSiteSituation.nonempty_simplicialModuleResolution · CategoryTheory.SimplicialSiteSituation.SimplicialModuleResolution.sectionsComplex · CategoryTheory.SimplicialSiteSituation.SimplicialModuleResolution.sectionsComplex_exactAt_le_one · CategoryTheory.SimplicialSiteSituation.SimplicialModuleResolution.sectionsComplex_acyclic · CategoryTheory.SimplicialSiteSituation.SimplicialModuleResolution.exists_sectionsSpectralSequence · CategoryTheory.SimplicialSiteSituation.componentModuleCohomologyIso · CategoryTheory.SimplicialSiteSituation.componentModuleCohomologyObjIso

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.