96.16 Cohomology to 96.26 Quasi-coherent objects in…

Section96.16 Cohomology #

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

Tag 075F, a lemma

Tag 075F in the Stacks Project.

AlgebraicGeometry.Stack.cohomologyOverObjectComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ObjectCohomologyLocalizationEtale.lean, line 596. References: SGA 4 VII (4.1), “more general”.

Stacks 075F. Let S be a scheme, p : 𝒳 ⥤ (Sch/S)_{fppf} a category fibred in groupoids, τ ∈ {Zariski, étale, smooth, syntomic, fppf}, and x an object of 𝒳 lying over the scheme U. For every degree n:

for F an abelian sheaf on 𝒳_τ, H^n_τ(x, F) = H^n((Sch/U)_τ, x^{-1}F);

for F a sheaf of O_𝒳-modules on 𝒳_τ, H^n_τ(x, F) = H^n((Sch/U)_τ, x^{-1}F);

if τ = étale, then also H^n_{étale}(x, F) = H^n(U_{étale}, F|_{U_{étale}}), for F an abelian sheaf and for F a sheaf of O_𝒳-modules on 𝒳_{étale}.

Each identification is a natural isomorphism of functors of F; they are AlgebraicGeometry.Stack.cohomologyOverObjectIso, AlgebraicGeometry.Stack.moduleCohomologyOverObjectIso, AlgebraicGeometry.Stack.etaleCohomologyOverObjectIso and AlgebraicGeometry.Stack.etaleModuleCohomologyOverObjectIso, the first two of which are stated there for any topology on the underlying category of schemes (coarser than the fppf topology, for modules).

The five topologies are B.baseTopology τ for τ : AlgebraicGeometry.SiteKind. Cohomology over x is the cohomology of the localized site 𝒳_τ/x of the restriction of F (Stacks 03F3); the cohomology of a sheaf of modules is computed in the category of sheaves of modules, as Ext out of the structure sheaf; (Sch/U)_τ is the big τ-site of U, identified with 𝒳_τ/x by the localization equivalence of Stacks 06W0, compatibly with the structure sheaves by Stacks 06W9; x^{-1}F is AlgebraicGeometry.Stack.objectInverseImage, resp. AlgebraicGeometry.Stack.objectModuleInverseImage; U_{étale} is the small étale site of U for the big étale site carried by B (Stacks 03FF); and F|_{U_{étale}} is the restriction of Stacks 06W1, AlgebraicGeometry.Stack.objectSmallEtaleRestriction, resp. AlgebraicGeometry.Stack.objectSmallEtaleModuleRestriction. Abelian sheaves and sheaves of modules have their sections in the universe max v w (u + 1) containing both sites, as explained in the module docstring of StacksFrontier/AlgebraicGeometry/Stacks/ObjectCohomologyLocalization.lean.

def cohomologyOverObjectComparison (τ : SiteKind) (n : ℕ) :
    (
      haveI := Stacks.Cohomology.SiteModules.site_hasSheafify_addCommGrp.{max v w, w, u + 1}
        (J := (associatedTopology B S hS p (B.baseTopology τ)).over x)
      haveI := Stacks.Cohomology.SiteModules.site_hasSheafify_addCommGrp.{u + 1, u, max v w}
        (J := (B.baseTopology τ).over (p.obj x).left)
      haveI := Stacks.Cohomology.SiteModules.site_hasExt_addCommGrp.{max v w, w, u + 1}
        (J := (associatedTopology B S hS p (B.baseTopology τ)).over x)
      haveI := Stacks.Cohomology.SiteModules.site_hasExt_addCommGrp.{u + 1, u, max v w}
        (J := (B.baseTopology τ).over (p.obj x).left)
      haveI := isDenseSubsite_overPost B S hS p hp (B.baseTopology τ) x
      (associatedTopology B S hS p (B.baseTopology τ)).overPullback
          AddCommGrpCat.{max v w (u + 1)} x ⋙
          Sheaf.functorH ((associatedTopology B S hS p (B.baseTopology τ)).over x) n ≅
        objectInverseImage B S hS p (B.baseTopology τ) x ⋙
          Sheaf.functorH ((B.baseTopology τ).over (p.obj x).left) n) ×
    (
      SheafOfModules.overFunctor (ringStructureSheaf.{u, v, w, u + 1} B S hS p hp
          (B.baseTopology τ) (B.baseTopology_le_topology τ)) x ⋙
          Stacks.Cohomology.BiggerSiteModules.moduleFunctorH.{u + 1, w, max v w}
            ((associatedTopology B S hS p (B.baseTopology τ)).over x)
            ((ringStructureSheaf.{u, v, w, u + 1} B S hS p hp (B.baseTopology τ)
              (B.baseTopology_le_topology τ)).over x) n ≅
        objectModuleInverseImage B S hS p hp (B.baseTopology τ) x
            (B.baseTopology_le_topology τ) ⋙
          Stacks.Cohomology.BiggerSiteModules.moduleFunctorH.{max v w, u, u + 1}
            ((B.baseTopology τ).over (p.obj x).left)
            (baseRingStructureSheafLift.{u, v, w} B (B.baseTopology τ)
              (B.baseTopology_le_topology τ) (p.obj x).left.1 (p.obj x).left.2) n) ×
    (τ = .etale →
      (
        haveI := Stacks.Cohomology.SiteModules.site_hasSheafify_addCommGrp.{max v w, w, u + 1}
          (J := (associatedTopology B S hS p B.etaleTopology).over x)
        haveI := Stacks.Cohomology.SiteModules.site_hasSheafify_addCommGrp.{u + 1, u, max v w}
          (J := SmallEtale.topology B.toBigEtaleSite (p.obj x).left.1
            (toBigEtaleSite_contains_left B S hS p x))
        haveI := Stacks.Cohomology.SiteModules.site_hasExt_addCommGrp.{max v w, w, u + 1}
          (J := (associatedTopology B S hS p B.etaleTopology).over x)
        haveI := Stacks.Cohomology.SiteModules.site_hasExt_addCommGrp.{u + 1, u, max v w}
          (J := SmallEtale.topology B.toBigEtaleSite (p.obj x).left.1
            (toBigEtaleSite_contains_left B S hS p x))
        (associatedTopology B S hS p B.etaleTopology).overPullback
            AddCommGrpCat.{max v w (u + 1)} x ⋙
            Sheaf.functorH ((associatedTopology B S hS p B.etaleTopology).over x) n ≅
          objectSmallEtaleRestriction B S hS p hp x ⋙
            Sheaf.functorH (SmallEtale.topology B.toBigEtaleSite (p.obj x).left.1
              (toBigEtaleSite_contains_left B S hS p x)) n) ×
      (
        SheafOfModules.overFunctor (ringStructureSheaf.{u, v, w, u + 1} B S hS p hp
            B.etaleTopology (etaleTopology_le_topology B)) x ⋙
            Stacks.Cohomology.BiggerSiteModules.moduleFunctorH.{u + 1, w, max v w}
              ((associatedTopology B S hS p B.etaleTopology).over x)
              ((ringStructureSheaf.{u, v, w, u + 1} B S hS p hp B.etaleTopology
                (etaleTopology_le_topology B)).over x) n ≅
          objectSmallEtaleModuleRestriction B S hS p hp x ⋙
            Stacks.Cohomology.BiggerSiteModules.moduleFunctorH.{max v w, u, u + 1}
              (SmallEtale.topology B.toBigEtaleSite (p.obj x).left.1
                (toBigEtaleSite_contains_left B S hS p x))
              (objectSmallEtaleRing B S hS p x) n))

Sources

LeanAlgebraicGeometry.Stack.cohomologyOverObjectComparison

Section96.17 Injective sheaves #

Section 96.17 of the Stacks Project, Tag 06WW. 6 tags here are carried by 25 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06WX, a lemma

Tag 06WX in the Stacks Project.

AlgebraicGeometry.Stack.preservesInjectiveObjects_abelianDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/InjectiveDirectImage.lean, line 74. The attribute's comment: “part (1)”.

Stacks 06WX, part (1). Direct image along a 1-morphism of fibred categories over the big fppf category of a scheme carries injective abelian sheaves to injective abelian sheaves, for the site each side inherits from an arbitrary topology on the base. The direct image is the right Kan extension along F.op, which exists for abelian groups in any universe containing the objects of the source and the morphisms of the target.

theorem preservesInjectiveObjects_abelianDirectImage
    [p.IsFibered] [q.IsFibered] (hF : p.IsFibredOneMorphism q F) :
    letI := (hF.isContinuous_and_isCocontinuous_inheritedTopology (τ.over (B.obj hS))).2
    (F.sheafPushforwardCocontinuous AddCommGrpCat.{max v₁ w₂ t}
      (associatedTopology B S hS p τ)
      (associatedTopology B S hS q τ)).PreservesInjectiveObjects

AlgebraicGeometry.Stack.preservesInjectiveObjects_sheafOfModulesDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/InjectiveDirectImage.lean, line 106. The attribute's comment: “part (2)”.

Stacks 06WX, part (2). Direct image along a 1-morphism of categories fibred in groupoids over the big fppf category of a scheme carries injective sheaves of O_𝒳-modules to injective sheaves of O_𝒴-modules, for every topology coarser than the fppf topology. The direct image is SheafOfModules.directImageOfEq, the right Kan extension along F.op with its module structure, which is right adjoint to the inverse image of modules.

theorem preservesInjectiveObjects_sheafOfModulesDirectImage
    (hp : p.IsFiberedInGroupoids) (hq : q.IsFiberedInGroupoids) (hcomp : F ⋙ q = p)
    (hτ : τ ≤ B.topology) :
    letI : p.IsFibered := hp.isFibered
    letI : q.IsFibered := hq.isFibered
    letI := ((hq.isFibredOneMorphism hcomp).isContinuous_and_isCocontinuous_inheritedTopology
      (τ.over (B.obj hS))).1
    letI := ((hq.isFibredOneMorphism hcomp).isContinuous_and_isCocontinuous_inheritedTopology
      (τ.over (B.obj hS))).2
    (SheafOfModules.directImageOfEq.{u, max v₁ w₂ t} F (associatedTopology B S hS p τ)
      (associatedTopology B S hS q τ) (ringStructureSheafCore B S hS q hq τ hτ)
      (ringStructureSheafCore_eq_sheafPushforwardContinuous_obj B S hS p q F τ hp hq hcomp
        hτ)).PreservesInjectiveObjects

AlgebraicGeometry.Stack.abelianDirectImage_preservesInjectiveObjects, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/InjectivePushforward.lean, line 64. The attribute's comment: “injective_pushforward_abelian”.

Stacks 06WX, part (1). Direct image under a fibred 1-morphism preserves injective abelian sheaves, for any of the five associated topologies.

theorem abelianDirectImage_preservesInjectiveObjects
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 : Type v₁} [Category.{w₁} 𝒳]
    {𝒴 : Type v₂} [Category.{w₂} 𝒴]
    {p𝒳 : 𝒳 ⥤ BigFppfOver B S hS}
    {p𝒴 : 𝒴 ⥤ BigFppfOver B S hS}
    [p𝒳.IsFibered] [p𝒴.IsFibered]
    {F : 𝒳 ⥤ 𝒴} (hF : p𝒳.IsFibredOneMorphism p𝒴 F)
    (τ : SiteKind)
    [∀ (G : 𝒳ᵒᵖ ⥤ AddCommGrpCat.{t}), F.op.HasPointwiseRightKanExtension G] :
    letI := (hF.isContinuous_and_isCocontinuous_inheritedTopology
      (BigFppfOver.baseOverTopology B S hS τ)).2
    (F.sheafPushforwardCocontinuous AddCommGrpCat.{t}
      (BigFppfOver.associatedTopology B S hS p𝒳 τ)
      (BigFppfOver.associatedTopology B S hS p𝒴 τ)).PreservesInjectiveObjects

AlgebraicGeometry.Stack.preservesInjectiveObjects_sheafPushforwardCocontinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Injectives.lean, line 143. The attribute's comment: “part (1)”.

Stacks 06WX, part (1). Direct image along a 1-morphism of fibred categories over the big fppf category of a scheme carries injective abelian sheaves to injective abelian sheaves, for the site each side inherits from an arbitrary topology on the base.

The inverse image is the left adjoint of direct image and preserves finite limits, hence monomorphisms, and a right adjoint of a monomorphism-preserving functor preserves injectives.

theorem preservesInjectiveObjects_sheafPushforwardCocontinuous
    [p.IsFibered] [q.IsFibered] (hF : p.IsFibredOneMorphism q F)
    [∀ G : 𝒳ᵒᵖ ⥤ AddCommGrpCat.{t}, F.op.HasPointwiseRightKanExtension G] :
    letI := (hF.isContinuous_and_isCocontinuous_inheritedTopology (τ.over (B.obj hS))).2
    (F.sheafPushforwardCocontinuous AddCommGrpCat.{t}
      (associatedTopology B S hS p τ)
      (associatedTopology B S hS q τ)).PreservesInjectiveObjects

AlgebraicGeometry.Stack.preservesInjectiveObjects_of_adjunction_sheafOfModules_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Injectives.lean, line 218. The attribute's comment: “part (2)”.

Stacks 06WX, part (2). Direct image along a 1-morphism of categories fibred in groupoids carries injective sheaves of modules to injective sheaves of modules: any functor G right adjoint to the inverse image of modules preserves injective objects.

G is the direct image of sheaves of modules; its existence is Stacks 06X0 and is taken as the hypothesis adj rather than constructed, so that the statement is about whichever functor is adjoint to the inverse image.

theorem preservesInjectiveObjects_of_adjunction_sheafOfModules_pushforward
    (hp : p.IsFiberedInGroupoids) (hq : q.IsFiberedInGroupoids) (hcomp : F ⋙ q = p)
    (hτ : τ ≤ B.topology)
    (G : letI : p.IsFibered := hp.isFibered
      SheafOfModules.{t} (ringStructureSheafCore B S hS p hp τ hτ) ⥤
        SheafOfModules.{t} (ringStructureSheafCore B S hS q hq τ hτ))
    (adj : letI : p.IsFibered := hp.isFibered
      letI : q.IsFibered := hq.isFibered
      letI := ((hq.isFibredOneMorphism hcomp).isContinuous_and_isCocontinuous_inheritedTopology
        (τ.over (B.obj hS))).1
      SheafOfModules.pushforward.{t}
        (ringStructureSheafCoreHom B S hS p q F τ hp hq hcomp hτ) ⊣ G) :
    G.PreservesInjectiveObjects

Tag 06WY, a lemma

Tag 06WY in the Stacks Project.

AlgebraicGeometry.Stack.hasEqualizers_of_isAlgebraicSpaceIsomPresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Equalizers.lean, line 68. The attribute's comment: “part (2)”.

Stacks 06WY (2). Let 𝒳 be a category fibred in groupoids over the big fppf site of S whose isomorphism presheaves Isom(x, y) are algebraic spaces. Then 𝒳 has equalizers.

theorem hasEqualizers_of_isAlgebraicSpaceIsomPresheaf
    (𝒳 : CatFiberedInGroupoids.{u, v, u + 1, w} (BigFppfOver B S hS))
    (h : IsAlgebraicSpaceIsomPresheaf B S hS 𝒳) : HasEqualizers 𝒳.val.obj

AlgebraicGeometry.Stack.hasEqualizers_of_isAlgebraicStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Equalizers.lean, line 92. The attribute's comment: “part (3)”.

Stacks 06WY, part (3). An algebraic stack over S has equalizers, its isomorphism presheaves being algebraic spaces.

theorem hasEqualizers_of_isAlgebraicStack
    (𝒳 : CatFiberedInGroupoids.{u, v, u + 1, t} (BigFppfOver B S hS))
    (h𝒳 : IsAlgebraicStack.{u, w} B S hS 𝒳.val) : HasEqualizers 𝒳.val.obj

AlgebraicGeometry.Stack.hasEqualizers_quotientStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Equalizers.lean, line 110. The attribute's comment: “part (3), the quotient stacks of its parenthetical”.

Stacks 06WY, part (3), for quotient stacks. The quotient stack [U/R] of a groupoid in algebraic spaces over S has equalizers.

Its isomorphism presheaves are algebraic spaces by Stacks 04TB, AlgebraicGeometry.Stack.isAlgebraicSpace_isomPresheaf, and part (2) applies.

theorem hasEqualizers_quotientStack {A : AlgebraicSpaces B S hS}
    (G : GroupoidInAlgebraicSpaces B S hS A) :
    HasEqualizers (quotientStack G).obj

AlgebraicGeometry.BigFppfOver.hasPullbacks_of_isFiberedInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/FibreProducts.lean, line 67. The attribute's comment: “part (1)”.

Stacks 06WY, part (1). A category fibred in groupoids over the big fppf category of a scheme has fibre products.

theorem hasPullbacks_of_isFiberedInGroupoids
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 : Type*} [Category 𝒳]
    (p : 𝒳 ⥤ BigFppfOver B S hS) (hp : p.IsFiberedInGroupoids) :
    HasPullbacks 𝒳

Tag 06WZ, a lemma

Tag 06WZ in the Stacks Project.

CategoryTheory.CatFiberedInGroupoids.preservesPullbacks_homFunctor, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/FibreProducts.lean, line 88. The attribute's comment: “preserves_fibre_products”.

Stacks 06WZ. A morphism of categories fibred in groupoids over a base category with fibre products preserves fibre products.

instance preservesPullbacks_homFunctor (f : 𝒳 ⟶ 𝒴) :
    PreservesLimitsOfShape WalkingCospan (homFunctor f)

CategoryTheory.CatFiberedInGroupoids.preservesEqualizers_homFunctor_of_faithful, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/FibreProducts.lean, line 214. The attribute's comment: “preserves_equalizers”.

Stacks 06WZ. A faithful morphism of categories fibred in groupoids preserves equalizers.

instance preservesEqualizers_homFunctor_of_faithful (f : 𝒳 ⟶ 𝒴)
    [Functor.Faithful (homFunctor f)] :
    PreservesLimitsOfShape WalkingParallelPair (homFunctor f)

Tag 06X0, a lemma

Tag 06X0 in the Stacks Project.

CategoryTheory.TwoFibreProductOver.faithful_fst_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/TwoFibreProductEqualizers.lean, line 260. The attribute's comment: “part (1)”.

Stacks 06X0, part (1). The 2-fibre product of faithful functors is faithful over their common target.

theorem faithful_fst_comp [F.Faithful] [G.Faithful] :
    (TwoFibreProductOver.fst p𝒳 p𝒵 p𝒴 F G ⋙ F).Faithful

CategoryTheory.TwoFibreProductOver.hasEqualizers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/TwoFibreProductEqualizers.lean, line 276. The attribute's comment: “part (2)”.

Stacks 06X0, part (2). Equalizers in the two source categories induce equalizers in their 2-fibre product over the common base.

theorem hasEqualizers
    (h𝒳 : p𝒳.IsFiberedInGroupoids) (h𝒵 : p𝒵.IsFiberedInGroupoids)
    (h𝒴 : p𝒴.IsFiberedInGroupoids)
    (hF : F ⋙ p𝒴 = p𝒳) (hG : G ⋙ p𝒴 = p𝒵)
    [F.Faithful] [G.Faithful] [HasEqualizers 𝒳] [HasEqualizers 𝒵] :
    HasEqualizers (TwoFibreProductOver p𝒳 p𝒵 p𝒴 F G)

Tag 06X1, a lemma

Tag 06X1 in the Stacks Project.

AlgebraicGeometry.Stack.exact_sheafPullback_of_faithful, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Injectives.lean, line 250. The attribute's comment: “part (1)”.

Stacks 06X1, part (1). For a faithful 1-morphism of categories fibred in groupoids whose source has equalizers, lower shriek f_! on abelian sheaves is exact.

Finite colimits are preserved because f_! is a left adjoint. Finite limits are preserved by the criterion of Stacks 04BH: the source has fibre products (Stacks 06WY) and equalizers by hypothesis, and f preserves both (Stacks 06WZ, in the form that places no constraint between the universes of source and target).

theorem exact_sheafPullback_of_faithful
    (hp : p.IsFiberedInGroupoids) (hq : q.IsFiberedInGroupoids) (hcomp : F ⋙ q = p)
    [F.Faithful] [HasEqualizers 𝒳]
    [∀ G : 𝒳ᵒᵖ ⥤ Ab.{t}, F.op.HasPointwiseLeftKanExtension G]
    [HasSheafify (associatedTopology B S hS q τ) Ab.{t}] :
    letI : p.IsFibered := hp.isFibered
    letI : q.IsFibered := hq.isFibered
    letI := ((hq.isFibredOneMorphism hcomp).isContinuous_and_isCocontinuous_inheritedTopology
      (τ.over (B.obj hS))).1
    exactFunctor _ _
      (Functor.sheafPullbackConstruction.sheafPullback F Ab.{t}
        (associatedTopology B S hS p τ) (associatedTopology B S hS q τ))

AlgebraicGeometry.Stack.injective_sheafPushforwardContinuous_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Injectives.lean, line 281. The attribute's comment: “part (2)”.

Stacks 06X1, part (2). The inverse image of an injective abelian sheaf is injective, when the 1-morphism is faithful and its source has equalizers.

The inverse image is right adjoint to the exact functor f_! of part (1), which therefore preserves monomorphisms.

theorem injective_sheafPushforwardContinuous_obj
    (hp : p.IsFiberedInGroupoids) (hq : q.IsFiberedInGroupoids) (hcomp : F ⋙ q = p)
    [F.Faithful] [HasEqualizers 𝒳]
    [∀ G : 𝒳ᵒᵖ ⥤ Ab.{t}, F.op.HasPointwiseLeftKanExtension G]
    [HasSheafify (associatedTopology B S hS q τ) Ab.{t}]
    (I : Sheaf (associatedTopology B S hS q τ) Ab.{t}) [Injective I] :
    letI : p.IsFibered := hp.isFibered
    letI : q.IsFibered := hq.isFibered
    letI := ((hq.isFibredOneMorphism hcomp).isContinuous_and_isCocontinuous_inheritedTopology
      (τ.over (B.obj hS))).1
    Injective ((F.sheafPushforwardContinuous Ab.{t}
      (associatedTopology B S hS p τ) (associatedTopology B S hS q τ)).obj I)

AlgebraicGeometry.Stack.isRightAdjoint_sheafPushforwardContinuous_of_essentiallySmall, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Injectives.lean, line 513. The attribute's comment: “f⁻¹ has a left adjoint f_!”.

Stacks 06X1, the left adjoint. For a 1-morphism f of categories fibred in groupoids over the big fppf category of S and any topology τ on the underlying category of schemes, the inverse image f⁻¹ : Ab(𝒴_τ) ⥤ Ab(𝒳_τ) has a left adjoint f_!.

The functor f is continuous for the associated topologies (Stacks 06NW). The pointwise left Kan extensions along f.op exist because 𝒳 is essentially small and 𝒴 locally small, and sheafification on 𝒴_τ exists because 𝒴 is essentially small; so f_! is the sheafified left Kan extension of Stacks 04BG, CategoryTheory.Functor.sheafPullbackConstruction.sheafAdjunctionContinuous.

theorem isRightAdjoint_sheafPushforwardContinuous_of_essentiallySmall
    (hp : p.IsFiberedInGroupoids) (hq : q.IsFiberedInGroupoids) (hcomp : F ⋙ q = p)
    [EssentiallySmall.{t} 𝒳] [EssentiallySmall.{t} 𝒴] :
    letI : p.IsFibered := hp.isFibered
    letI : q.IsFibered := hq.isFibered
    letI := ((hq.isFibredOneMorphism hcomp).isContinuous_and_isCocontinuous_inheritedTopology
      (τ.over (B.obj hS))).1
    (F.sheafPushforwardContinuous Ab.{t}
      (associatedTopology B S hS p τ) (associatedTopology B S hS q τ)).IsRightAdjoint

AlgebraicGeometry.Stack.exact_leftAdjoint_sheafPushforwardContinuous_of_faithful, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Injectives.lean, line 542. The attribute's comment: “part (1)”.

Stacks 06X1, part (1). For a faithful 1-morphism of categories fibred in groupoids over the big fppf category of S whose source has equalizers, the left adjoint f_! of the inverse image f⁻¹ : Ab(𝒴_τ) ⥤ Ab(𝒳_τ) is exact, for any topology τ on the underlying category of schemes.

The left adjoint is isomorphic to the sheafified left Kan extension, which is exact by AlgebraicGeometry.Stack.exact_sheafPullback_of_faithful (Stacks 04BH, with the hypotheses of that criterion supplied by Stacks 06WY and 06WZ); the pointwise Kan extensions and the sheafification it uses exist by essential smallness of 𝒳 and 𝒴.

theorem exact_leftAdjoint_sheafPushforwardContinuous_of_faithful
    (hp : p.IsFiberedInGroupoids) (hq : q.IsFiberedInGroupoids) (hcomp : F ⋙ q = p)
    [F.Faithful] [HasEqualizers 𝒳] [EssentiallySmall.{t} 𝒳] [EssentiallySmall.{t} 𝒴] :
    letI : p.IsFibered := hp.isFibered
    letI : q.IsFibered := hq.isFibered
    letI := ((hq.isFibredOneMorphism hcomp).isContinuous_and_isCocontinuous_inheritedTopology
      (τ.over (B.obj hS))).1
    letI : (F.sheafPushforwardContinuous Ab.{t}
        (associatedTopology B S hS p τ) (associatedTopology B S hS q τ)).IsRightAdjoint :=
      isRightAdjoint_sheafPushforwardContinuous_of_essentiallySmall B S hS p q F τ hp hq hcomp
    exactFunctor _ _ (F.sheafPushforwardContinuous Ab.{t}
      (associatedTopology B S hS p τ) (associatedTopology B S hS q τ)).leftAdjoint

AlgebraicGeometry.Stack.injective_sheafPushforwardContinuous_obj_of_essentiallySmall, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Injectives.lean, line 581. The attribute's comment: “part (2)”.

Stacks 06X1, part (2). For a faithful 1-morphism of categories fibred in groupoids over the big fppf category of S whose source has equalizers, the inverse image of an injective abelian sheaf on 𝒴_τ is an injective abelian sheaf on 𝒳_τ, for any topology τ on the underlying category of schemes.

The inverse image is right adjoint to the functor f_!, which is exact by part (1) and so preserves monomorphisms (Stacks 015Z).

theorem injective_sheafPushforwardContinuous_obj_of_essentiallySmall
    (hp : p.IsFiberedInGroupoids) (hq : q.IsFiberedInGroupoids) (hcomp : F ⋙ q = p)
    [F.Faithful] [HasEqualizers 𝒳] [EssentiallySmall.{t} 𝒳] [EssentiallySmall.{t} 𝒴]
    (I : Sheaf (associatedTopology B S hS q τ) Ab.{t}) [Injective I] :
    letI : p.IsFibered := hp.isFibered
    letI : q.IsFibered := hq.isFibered
    letI := ((hq.isFibredOneMorphism hcomp).isContinuous_and_isCocontinuous_inheritedTopology
      (τ.over (B.obj hS))).1
    Injective ((F.sheafPushforwardContinuous Ab.{t}
      (associatedTopology B S hS p τ) (associatedTopology B S hS q τ)).obj I)

Declarations registered for the tag:

CategoryTheory.Functor.sheafPullbackConstruction.sheafAdjunctionContinuous registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Injectives.lean, line 239 (StacksFrontier): “the adjunction f_! ⊣ f⁻¹”. References: SGA 4 III (1.3), “more general”; SGA 4 III (2.6); SGA 4 IV (4.7), “partial”; SGA 4 IV (4.9.1), “partial”; SGA 4 VI (7.4.13.4).

Tag 06X2, a lemma

Tag 06X2 in the Stacks Project.

AlgebraicGeometry.Stack.lowerShriekForgetIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Injectives.lean, line 318. The attribute's comment: “underlying abelian sheaves”.

Stacks 06X2. Lower shriek on sheaves of modules agrees, on underlying abelian sheaves, with lower shriek on abelian sheaves.

Both sides are computed by sheafifying a presheaf-level left adjoint, and at the presheaf level the two agree because every slice functor of a 1-morphism of categories fibred in groupoids is an equivalence: that is Stacks.ModuleLowerShriek.pullbackCompToPresheafIso. Without the slice hypothesis the statement is false, by Stacks.SheafOfModules.lowerShriekForget_not_isomorphic.

noncomputable def lowerShriekForgetIso
    (hp : p.IsFiberedInGroupoids) (hq : q.IsFiberedInGroupoids) (hcomp : F ⋙ q = p)
    (hτ : τ ≤ B.topology)
    (hPresheaf :
      letI : p.IsFibered := hp.isFibered
      letI : q.IsFibered := hq.isFibered
      letI := ((hq.isFibredOneMorphism hcomp).isContinuous_and_isCocontinuous_inheritedTopology
        (τ.over (B.obj hS))).1
      (PresheafOfModules.pushforward.{t}
        (ringStructureSheafCoreHom B S hS p q F τ hp hq hcomp hτ).hom).IsRightAdjoint)
    [∀ G : 𝒳ᵒᵖ ⥤ AddCommGrpCat.{t}, F.op.HasPointwiseLeftKanExtension G]
    [HasWeakSheafify (associatedTopology B S hS q τ) AddCommGrpCat.{t}]
    [(associatedTopology B S hS q τ).WEqualsLocallyBijective AddCommGrpCat.{t}] :
    letI : p.IsFibered := hp.isFibered
    letI : q.IsFibered := hq.isFibered
    letI := ((hq.isFibredOneMorphism hcomp).isContinuous_and_isCocontinuous_inheritedTopology
      (τ.over (B.obj hS))).1
    letI : (PresheafOfModules.pushforward.{t}
      (ringStructureSheafCoreHom B S hS p q F τ hp hq hcomp hτ).hom).IsRightAdjoint := hPresheaf
    letI : (SheafOfModules.pushforward.{t}
      (ringStructureSheafCoreHom B S hS p q F τ hp hq hcomp hτ)).IsRightAdjoint :=
      SheafOfModules.instIsRightAdjointPushforward _
    SheafOfModules.pullback.{t} (ringStructureSheafCoreHom B S hS p q F τ hp hq hcomp hτ) ⋙
        SheafOfModules.toSheaf.{t} (ringStructureSheafCore B S hS q hq τ hτ) ≅
      SheafOfModules.toSheaf.{t} (ringStructureSheafCore B S hS p hp τ hτ) ⋙
        Functor.sheafPullbackConstruction.sheafPullback F AddCommGrpCat.{t}
          (associatedTopology B S hS p τ) (associatedTopology B S hS q τ)

AlgebraicGeometry.Stack.exact_sheafOfModules_pullback_of_faithful, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Injectives.lean, line 384. The attribute's comment: “part (1)”.

Stacks 06X2, part (1). For a faithful 1-morphism of categories fibred in groupoids whose source has equalizers, lower shriek f_! on sheaves of modules is exact.

Finite colimits are preserved because f_! is a left adjoint. Finite limits are preserved because SheafOfModules.toSheaf reflects them and, composed with f_!, is the abelian f_! of Stacks 06X1 (1) up to lowerShriekForgetIso, which is exact.

theorem exact_sheafOfModules_pullback_of_faithful
    (hp : p.IsFiberedInGroupoids) (hq : q.IsFiberedInGroupoids) (hcomp : F ⋙ q = p)
    (hτ : τ ≤ B.topology) [F.Faithful] [HasEqualizers 𝒳]
    (hPresheaf :
      letI : p.IsFibered := hp.isFibered
      letI : q.IsFibered := hq.isFibered
      letI := ((hq.isFibredOneMorphism hcomp).isContinuous_and_isCocontinuous_inheritedTopology
        (τ.over (B.obj hS))).1
      (PresheafOfModules.pushforward.{t}
        (ringStructureSheafCoreHom B S hS p q F τ hp hq hcomp hτ).hom).IsRightAdjoint)
    [∀ G : 𝒳ᵒᵖ ⥤ AddCommGrpCat.{t}, F.op.HasPointwiseLeftKanExtension G]
    [HasSheafify (associatedTopology B S hS q τ) AddCommGrpCat.{t}]
    [(associatedTopology B S hS q τ).WEqualsLocallyBijective AddCommGrpCat.{t}] :
    letI : p.IsFibered := hp.isFibered
    letI : q.IsFibered := hq.isFibered
    letI := ((hq.isFibredOneMorphism hcomp).isContinuous_and_isCocontinuous_inheritedTopology
      (τ.over (B.obj hS))).1
    letI : (PresheafOfModules.pushforward.{t}
      (ringStructureSheafCoreHom B S hS p q F τ hp hq hcomp hτ).hom).IsRightAdjoint := hPresheaf
    letI : (SheafOfModules.pushforward.{t}
      (ringStructureSheafCoreHom B S hS p q F τ hp hq hcomp hτ)).IsRightAdjoint :=
      SheafOfModules.instIsRightAdjointPushforward _
    exactFunctor _ _
      (SheafOfModules.pullback.{t}
        (ringStructureSheafCoreHom B S hS p q F τ hp hq hcomp hτ))

AlgebraicGeometry.Stack.injective_sheafOfModules_pushforward_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Injectives.lean, line 441. The attribute's comment: “part (2)”.

Stacks 06X2, part (2). The inverse image of an injective sheaf of modules is injective, when the 1-morphism is faithful and its source has equalizers.

The inverse image of modules is right adjoint to the exact functor f_! of part (1), which therefore preserves monomorphisms.

theorem injective_sheafOfModules_pushforward_obj
    (hp : p.IsFiberedInGroupoids) (hq : q.IsFiberedInGroupoids) (hcomp : F ⋙ q = p)
    (hτ : τ ≤ B.topology) [F.Faithful] [HasEqualizers 𝒳]
    (hPresheaf :
      letI : p.IsFibered := hp.isFibered
      letI : q.IsFibered := hq.isFibered
      letI := ((hq.isFibredOneMorphism hcomp).isContinuous_and_isCocontinuous_inheritedTopology
        (τ.over (B.obj hS))).1
      (PresheafOfModules.pushforward.{t}
        (ringStructureSheafCoreHom B S hS p q F τ hp hq hcomp hτ).hom).IsRightAdjoint)
    [∀ G : 𝒳ᵒᵖ ⥤ AddCommGrpCat.{t}, F.op.HasPointwiseLeftKanExtension G]
    [HasSheafify (associatedTopology B S hS q τ) AddCommGrpCat.{t}]
    [(associatedTopology B S hS q τ).WEqualsLocallyBijective AddCommGrpCat.{t}]
    (I : SheafOfModules.{t} (ringStructureSheafCore B S hS q hq τ hτ)) [Injective I] :
    letI : p.IsFibered := hp.isFibered
    letI : q.IsFibered := hq.isFibered
    letI := ((hq.isFibredOneMorphism hcomp).isContinuous_and_isCocontinuous_inheritedTopology
      (τ.over (B.obj hS))).1
    Injective ((SheafOfModules.pushforward.{t}
      (ringStructureSheafCoreHom B S hS p q F τ hp hq hcomp hτ)).obj I)

AlgebraicGeometry.Stack.isRightAdjoint_sheafOfModules_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/ModuleLowerShriek.lean, line 93. The attribute's comment: “f^* on sheaves of modules has a left adjoint f_!”.

Stacks 06X2, existence of f_!. Inverse image of sheaves of modules along a 1-morphism of categories fibred in groupoids over the big fppf category of a scheme has a left adjoint f_!.

theorem isRightAdjoint_sheafOfModules_pushforward
    [EssentiallySmall.{t} 𝒳] [EssentiallySmall.{t} 𝒴] [UnivLE.{u, t}]
    (hp : p.IsFiberedInGroupoids) (hq : q.IsFiberedInGroupoids) (hcomp : F ⋙ q = p)
    (hτ : τ ≤ B.topology) :
    letI : p.IsFibered := hp.isFibered
    letI : q.IsFibered := hq.isFibered
    letI := ((hq.isFibredOneMorphism hcomp).isContinuous_and_isCocontinuous_inheritedTopology
      (τ.over (B.obj hS))).1
    (SheafOfModules.pushforward.{t}
      (ringStructureSheafCoreHom B S hS p q F τ hp hq hcomp hτ)).IsRightAdjoint

AlgebraicGeometry.Stack.lowerShriekModulesForgetIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/ModuleLowerShriek.lean, line 129. The attribute's comment: “f_! on sheaves of modules agrees with f_! on abelian sheaves”.

Stacks 06X2, comparison with abelian sheaves. The lower shriek f_! of sheaves of modules along a 1-morphism of categories fibred in groupoids agrees, on underlying abelian sheaves, with the lower shriek of abelian sheaves of Stacks 06X1.

noncomputable def lowerShriekModulesForgetIso
    [EssentiallySmall.{t} 𝒳] [EssentiallySmall.{t} 𝒴] [UnivLE.{u, t}]
    (hp : p.IsFiberedInGroupoids) (hq : q.IsFiberedInGroupoids) (hcomp : F ⋙ q = p)
    (hτ : τ ≤ B.topology) :
    letI : p.IsFibered := hp.isFibered
    letI : q.IsFibered := hq.isFibered
    letI := ((hq.isFibredOneMorphism hcomp).isContinuous_and_isCocontinuous_inheritedTopology
      (τ.over (B.obj hS))).1
    letI := isRightAdjoint_sheafOfModules_pushforward.{u, v₁, v₂, w₁, w₂, t}
      B S hS p q F τ hp hq hcomp hτ
    letI := fun G : 𝒳ᵒᵖ ⥤ AddCommGrpCat.{t} ↦
      Functor.hasPointwiseLeftKanExtension_of_essentiallySmall_of_locallySmall.{t} F.op G
    letI := hasSheafify_associatedTopology_of_essentiallySmall.{u, v₂, w₂, t} B S hS q τ
    SheafOfModules.pullback.{t} (ringStructureSheafCoreHom B S hS p q F τ hp hq hcomp hτ) ⋙
        SheafOfModules.toSheaf.{t} (ringStructureSheafCore B S hS q hq τ hτ) ≅
      SheafOfModules.toSheaf.{t} (ringStructureSheafCore B S hS p hp τ hτ) ⋙
        Functor.sheafPullbackConstruction.sheafPullback F AddCommGrpCat.{t}
          (associatedTopology B S hS p τ) (associatedTopology B S hS q τ)

AlgebraicGeometry.Stack.exactFunctor_sheafOfModules_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/ModuleLowerShriek.lean, line 157. The attribute's comment: “part (1)”.

Stacks 06X2, part (1). For a faithful 1-morphism of categories fibred in groupoids whose source has equalizers, the lower shriek f_! of sheaves of modules is exact.

theorem exactFunctor_sheafOfModules_pullback
    [EssentiallySmall.{t} 𝒳] [EssentiallySmall.{t} 𝒴] [UnivLE.{u, t}]
    (hp : p.IsFiberedInGroupoids) (hq : q.IsFiberedInGroupoids) (hcomp : F ⋙ q = p)
    (hτ : τ ≤ B.topology) [F.Faithful] [HasEqualizers 𝒳] :
    letI : p.IsFibered := hp.isFibered
    letI : q.IsFibered := hq.isFibered
    letI := ((hq.isFibredOneMorphism hcomp).isContinuous_and_isCocontinuous_inheritedTopology
      (τ.over (B.obj hS))).1
    letI := isRightAdjoint_sheafOfModules_pushforward.{u, v₁, v₂, w₁, w₂, t}
      B S hS p q F τ hp hq hcomp hτ
    exactFunctor _ _
      (SheafOfModules.pullback.{t}
        (ringStructureSheafCoreHom B S hS p q F τ hp hq hcomp hτ))

AlgebraicGeometry.Stack.injective_sheafOfModules_pushforward_obj_of_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/ModuleLowerShriek.lean, line 178. The attribute's comment: “part (2)”.

Stacks 06X2, part (2). For a faithful 1-morphism of categories fibred in groupoids whose source has equalizers, the inverse image of an injective sheaf of modules is an injective sheaf of modules.

theorem injective_sheafOfModules_pushforward_obj_of_injective
    [EssentiallySmall.{t} 𝒳] [EssentiallySmall.{t} 𝒴] [UnivLE.{u, t}]
    (hp : p.IsFiberedInGroupoids) (hq : q.IsFiberedInGroupoids) (hcomp : F ⋙ q = p)
    (hτ : τ ≤ B.topology) [F.Faithful] [HasEqualizers 𝒳]
    (I : SheafOfModules.{t} (ringStructureSheafCore B S hS q hq τ hτ)) [Injective I] :
    letI : p.IsFibered := hp.isFibered
    letI : q.IsFibered := hq.isFibered
    letI := ((hq.isFibredOneMorphism hcomp).isContinuous_and_isCocontinuous_inheritedTopology
      (τ.over (B.obj hS))).1
    Injective ((SheafOfModules.pushforward.{t}
      (ringStructureSheafCoreHom B S hS p q F τ hp hq hcomp hτ)).obj I)

Declarations registered for the tag:

SheafOfModules.instIsRightAdjointPushforward registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Injectives.lean, line 306 (StacksFrontier): “the adjunction f_! ⊣ f^* on modules”.

Sources

Section96.18 The Čech complex #

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

Tag 06X3, the section

Tag 06X3 in the Stacks Project.

Stacks.RelativeCech.isEquivalence_fibreProductToNerve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/NerveFibreProduct.lean, line 204. The attribute's comment: “the nerve in degree n + 1 is the 2-fibre product of the covering with degree n”.

The degree n + 1 piece of the Čech nerve of a covering f : U ⥤ X is the 2-fibre product U ×_X U_n of the covering with the degree n piece: prepending a coordinate is an equivalence of categories.

public theorem isEquivalence_fibreProductToNerve (n : ℕ) :
    (fibreProductToNerve p f n).IsEquivalence

Stacks.RelativeCech.isEquivalence_coordinate_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/NerveFibreProduct.lean, line 223. The attribute's comment: “the nerve in degree zero is the covering”.

The degree 0 piece of the Čech nerve of a covering f : U ⥤ X is the covering U itself: reading off the single coordinate of a tuple is an equivalence of categories.

public theorem isEquivalence_coordinate_zero :
    (Tuple.coordinate p f (0 : Fin 1)).IsEquivalence

Tag 06X5, a lemma

Tag 06X5 in the Stacks Project.

Stacks.Cech.complexPullbackMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/Complex.lean, line 328. The attribute's comment: “part (1), the morphism of complexes”.

Stacks 06X5 (1). A 2-commutative square of coverings over the base induces a morphism of Čech complexes Č(U → X, F) ⟶ Č(V → Y, e⁻¹F), given in degree n by pullback along the induced functor V_n ⥤ U_n of Čech nerves.

public def complexPullbackMap : complex pX f F ⟶ complex pY g (e.op ⋙ F)

Stacks.Cech.complexPullbackMap_π, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/Complex.lean, line 334. The attribute's comment: “part (1), the degreewise description”.

Stacks 06X5 (1). The morphism of Čech complexes is pullback along the induced functor of Čech nerves, degreewise on the limit cones.

public theorem complexPullbackMap_π (n : ℕ) (a : Tuple pY g n) :
    (complexPullbackMap pX pY f g h e α he hα F).f n ≫
        limit.π ((Tuple.projection pY g n).op ⋙ e.op ⋙ F) (op a) =
      limit.π ((Tuple.projection pX f n).op ⋙ F)
        (op ((nerveMap pX pY f g h e α he hα n).obj a))

Stacks.Cech.isIso_complexPullbackMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/Complex.lean, line 344. The attribute's comment: “part (2)”.

Stacks 06X5 (2). If the two horizontal functors of the square are equivalences, the morphism of Čech complexes of part (1) is an isomorphism.

public theorem isIso_complexPullbackMap [h.IsEquivalence] [e.IsEquivalence]
    (hpV : (g ⋙ pY).IsFiberedInGroupoids) :
    IsIso (complexPullbackMap pX pY f g h e α he hα F)

Stacks.Cech.nonempty_complexIso_of_natIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/Complex.lean, line 362. The attribute's comment: “part (3)”.

Stacks 06X5 (3). 2-isomorphic coverings f, f' : U ⥤ X have isomorphic Čech complexes.

public theorem nonempty_complexIso_of_natIso [Preadditive A] (p : X ⥤ C) (f f' : U ⥤ X)
    (α : f ≅ f') (hα : ∀ u : U, p.IsHomLift (𝟙 (p.obj (f.obj u))) (α.hom.app u))
    (hpU' : (f' ⋙ p).IsFiberedInGroupoids) (F : Xᵒᵖ ⥤ A)
    [∀ n : ℕ, HasLimitsOfShape (Tuple p f n)ᵒᵖ A]
    [∀ n : ℕ, HasLimitsOfShape (Tuple p f' n)ᵒᵖ A] :
    Nonempty (complex p f F ≅ complex p f' F)

Tag 06X6, a lemma

Tag 06X6 in the Stacks Project.

Stacks.Cech.nonempty_homotopy_extendedComplex_id_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/Homotopy.lean, line 407.

Stacks 06X6. If there is a 1-morphism s : X ⥤ U such that f ∘ s is 2-isomorphic to id_X, then the extended Čech complex is homotopic to zero: its identity is homotopic to its zero endomorphism.

public theorem nonempty_homotopy_extendedComplex_id_zero (s : X ⥤ U) (t : s ⋙ f ≅ 𝟭 X)
    (ht : ∀ x : X, p.IsHomLift (𝟙 (p.obj x)) (t.hom.app x)) :
    Nonempty (Homotopy (𝟙 (extendedComplex p f F)) 0)

Sources

LeanStacks.RelativeCech.isEquivalence_fibreProductToNerve · Stacks.RelativeCech.isEquivalence_coordinate_zero · Stacks.Cech.complexPullbackMap · Stacks.Cech.complexPullbackMap_π · Stacks.Cech.isIso_complexPullbackMap · Stacks.Cech.nonempty_complexIso_of_natIso · Stacks.Cech.nonempty_homotopy_extendedComplex_id_zero

Section96.19 The relative Čech complex #

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

Tag 06X8, a remark

Tag 06X8 in the Stacks Project.

Stacks.RelativeCech.complex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/RelativeCechComplex.lean, line 221. The attribute's comment: “presheaf_relative_cech_complex”.

Stacks 06X8. The relative Čech complex of an abelian presheaf for a functor over a base category: the alternating-coface complex of the relative Čech cosimplicial presheaf.

public noncomputable def complex (F : Xᵒᵖ ⥤ AddCommGrpCat.{max uU uX vX w}) :
    CochainComplex (Xᵒᵖ ⥤ AddCommGrpCat.{max uU uX vX w}) ℕ

Stacks.presheafPullbackMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/PullbackMap.lean, line 83. The attribute's comment: “the pullback map on presheaf direct images”.

Stacks 06X8. The canonical map from the direct image of a presheaf along f to the direct image along h ⋙ f of its restriction along h: the direct image of the adjunction unit for h, followed by the comparison from iterated direct image to direct image along the composite.

public noncomputable def presheafPullbackMap (G : Uᵒᵖ ⥤ A) :
    f.op.ran.obj G ⟶ (h.op ⋙ f.op).ran.obj (h.op ⋙ G)

Stacks.presheafPullbackMap_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/PullbackMap.lean, line 90. The attribute's comment: “naturality of the pullback map on presheaf direct images”.

Stacks 06X8. The presheaf pullback map is natural in the presheaf.

public theorem presheafPullbackMap_natural {G H : Uᵒᵖ ⥤ A} (α : G ⟶ H) :
    f.op.ran.map α ≫ presheafPullbackMap f h H =
      presheafPullbackMap f h G ≫
        (h.op ⋙ f.op).ran.map (Functor.whiskerLeft h.op α)

Stacks.presheafPullbackMap_whiskerLeft_ranCounit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/PullbackMap.lean, line 151. The attribute's comment: “the counit factorisation of the presheaf pullback map”.

Stacks 06X8. The defining property of the presheaf pullback map against the Kan-extension counits: restricting the counit of f along h factors through it.

public theorem presheafPullbackMap_whiskerLeft_ranCounit (G : Xᵒᵖ ⥤ A) :
    Functor.whiskerLeft h.op (f.op.ranCounit.app (f.op ⋙ G)) =
      Functor.whiskerLeft (h.op ⋙ f.op) (presheafPullbackMap f h (f.op ⋙ G)) ≫
        (h.op ⋙ f.op).ranCounit.app (h.op ⋙ f.op ⋙ G)

Stacks.RelativeCech.reindexMap_eq_presheafPullbackMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/PullbackMap.lean, line 190. The attribute's comment: “the Čech reindexing maps are pullback maps”.

Stacks 06X8. Each reindexing map of the relative Čech complex of an abelian presheaf is the canonical pullback map along the corresponding reindexing functor of relative Čech tuples.

public theorem reindexMap_eq_presheafPullbackMap {U : Type uU} {X : Type uX} {C : Type uC}
    [Category.{vU} U] [Category.{vX} X] [Category.{vC} C] (p : X ⥤ C) (f : U ⥤ X)
    (F : Xᵒᵖ ⥤ AddCommGrpCat.{max uU uX vX vU vC w}) {m n : ℕ} (φ : ⦋m⦌ ⟶ ⦋n⦌) :
    reindexMap.{vU, vX, vC, uU, uX, uC, max vU vC w} p f F φ =
      presheafPullbackMap (Tuple.projection p f m)
        (Tuple.reindex p f φ.toOrderHom) ((Tuple.projection p f m).op ⋙ F)

Stacks.sheafPullbackMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/PullbackMap.lean, line 226. The attribute's comment: “the pullback map on sheaf direct images”.

Stacks 06X8. The canonical map from the direct image of a sheaf along f to the direct image along h ⋙ f of its restriction along h, formed from the unit of the restriction/direct-image adjunction for h and the direct-image compositor.

public noncomputable def sheafPullbackMap (G : Sheaf K A) :
    letI := isCocontinuous_comp h f J K (L := L)
    (f.sheafPushforwardCocontinuous A K L).obj G ⟶
      ((h ⋙ f).sheafPushforwardCocontinuous A J L).obj
        ((h.sheafPushforwardContinuous A J K).obj G)

Stacks.sheafPullbackMap_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/PullbackMap.lean, line 240. The attribute's comment: “agreement of the sheaf and presheaf pullback maps”.

Stacks 06X8. The underlying presheaf morphism of the sheaf pullback map is the presheaf pullback map.

public theorem sheafPullbackMap_hom (G : Sheaf K A) :
    letI : ∀ P : Vᵒᵖ ⥤ A, (h.op ⋙ f.op).HasRightKanExtension P :=
      fun P => inferInstanceAs ((h ⋙ f).op.HasRightKanExtension P)
    (sheafPullbackMap J K L f h G).hom = presheafPullbackMap f h G.obj

Stacks.sheafPullbackMap_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/PullbackMap.lean, line 255. The attribute's comment: “naturality of the pullback map on sheaf direct images”.

Stacks 06X8. The sheaf pullback map is natural in the sheaf.

public theorem sheafPullbackMap_natural {G H : Sheaf K A} (α : G ⟶ H) :
    letI := isCocontinuous_comp h f J K (L := L)
    (f.sheafPushforwardCocontinuous A K L).map α ≫ sheafPullbackMap J K L f h H =
      sheafPullbackMap J K L f h G ≫
        ((h ⋙ f).sheafPushforwardCocontinuous A J L).map
          ((h.sheafPushforwardContinuous A J K).map α)

Tag 06X9, a lemma

Tag 06X9 in the Stacks Project.

Stacks.RelativeCech.baseChangeMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/RelativeGeneralities.lean, line 249. The attribute's comment: “part (1)”.

Stacks 06X9, part (1). The canonical comparison is assembled from the right-Kan-extension adjunction in each Čech degree.

public noncomputable def baseChangeMap
    (F : Xᵒᵖ ⥤ AddCommGrpCat.{max uU uX vX uV uY vY w}) :
    (((Functor.whiskeringLeft Yᵒᵖ Xᵒᵖ
      AddCommGrpCat.{max uU uX vX uV uY vY w}).obj e.op).mapHomologicalComplex
        (ComplexShape.up ℕ)).obj
        (complex.{vU, vX, vC, uU, uX, uC, max uV uY vY w} pX f F) ⟶
      complex.{vV, vY, vC, uV, uY, uC, max uU uX vX w}
        (e ⋙ pX) g (e.op ⋙ F)

Stacks.RelativeCech.isIso_baseChangeMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/RelativeGeneralities.lean, line 264. The attribute's comment: “part (2)”.

Stacks 06X9, part (2). If the two horizontal 1-morphisms h and e of the square are equivalences, then the base-change morphism of part (1) is an isomorphism of complexes of abelian presheaves.

public theorem isIso_baseChangeMap
    [h.IsEquivalence] [e.IsEquivalence]
    (hpV : (g ⋙ e ⋙ pX).IsFiberedInGroupoids)
    (F : Xᵒᵖ ⥤ AddCommGrpCat.{max uU uX vX uV uY vY w}) :
    IsIso (baseChangeMap pX f e g h α hα F)

Stacks.RelativeCech.nonempty_complexIso_of_natIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/RelativeGeneralities.lean, line 278. The attribute's comment: “part (3)”.

Stacks 06X9, part (3). 2-isomorphic 1-morphisms f, f' : 𝒰 ⟶ 𝒳 over the base have isomorphic relative Čech complexes.

public theorem nonempty_complexIso_of_natIso
    {C : Type uC} {X : Type uX} {U : Type uU} [Category.{vC} C] [Category.{vX} X]
    [Category.{vU} U] (pX : X ⥤ C) (f f' : U ⥤ X) (β : f ≅ f')
    (hβ : ∀ u : U, pX.IsHomLift (𝟙 (pX.obj (f.obj u))) (β.hom.app u))
    (hpU' : (f' ⋙ pX).IsFiberedInGroupoids)
    (F : Xᵒᵖ ⥤ AddCommGrpCat.{max uU uX vX w}) :
    Nonempty (complex pX f F ≅ complex pX f' F)

Tag 06XA, a lemma

Tag 06XA in the Stacks Project.

Stacks.RelativeCech.nonempty_homotopy_extendedSheafComplex_id_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/RelativeHomotopy.lean, line 639.

Stacks 06XA. If there is a 1-morphism s : 𝒳 ⥤ 𝒰 such that f ∘ s is 2-isomorphic to id_𝒳 by a vertical 2-isomorphism, then the extended relative Čech complex is homotopic to zero: its identity is homotopic to its zero endomorphism.

public theorem nonempty_homotopy_extendedSheafComplex_id_zero
    (s : 𝒳 ⥤ 𝒰) (α : s ⋙ f ≅ 𝟭 𝒳)
    (hα : ∀ x : 𝒳, q.IsHomLift (𝟙 (q.obj x)) (α.hom.app x)) :
    Nonempty (Homotopy
      (𝟙 (extendedSheafComplex.{u, vᵤ, vₓ, wᵤ, wₓ, t} B S hS q f τ 𝓕)) 0)

Tag 06XB, a remark

Tag 06XB in the Stacks Project.

Stacks.RelativeCech.nerveBaseChangeEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/RelativeSections.lean, line 479. The attribute's comment: “equivalence of Čech nerves”.

The Čech nerve of the base change of f to the slice over p(x) is, in each degree, the base change of the Čech nerve of f.

public def nerveBaseChangeEquivalence (p : X ⥤ C) (f : U ⥤ X) (c : p.ChoiceOfPullbacks)
    {V : C} (x : p.Fiber V) (n : ℕ) :
    Tuple (Over.forget V)
        (TwoFibreProductOver.fst (Over.forget V) (f ⋙ p) p (c.sliceFunctor x) f) n ≌
      TwoFibreProductOver (Over.forget V) (Tuple.projection p f n ⋙ p) p
        (c.sliceFunctor x) (Tuple.projection p f n)

Stacks.RelativeCech.nerveBaseChangeEquivalence_functor_comp_fst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/RelativeSections.lean, line 490. The attribute's comment: “equivalence of Čech nerves”.

The first projection of the base change of the Čech nerve corresponds, under the equivalence, to the projection of the Čech nerve of the base change.

public theorem nerveBaseChangeEquivalence_functor_comp_fst (p : X ⥤ C) (f : U ⥤ X)
    (c : p.ChoiceOfPullbacks) {V : C} (x : p.Fiber V) (n : ℕ) :
    (nerveBaseChangeEquivalence p f c x n).functor ⋙
        TwoFibreProductOver.fst (Over.forget V) (Tuple.projection p f n ⋙ p) p
          (c.sliceFunctor x) (Tuple.projection p f n) =
      Tuple.projection (Over.forget V)
        (TwoFibreProductOver.fst (Over.forget V) (f ⋙ p) p (c.sliceFunctor x) f) n

Stacks.RelativeCech.nerveBaseChangeEquivalence_functor_comp_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/RelativeSections.lean, line 502. The attribute's comment: “equivalence of Čech nerves”.

The second projection of the base change of the Čech nerve corresponds, under the equivalence, to the 1-morphism of Čech nerves of Stacks.Cech.nerveMap.

public theorem nerveBaseChangeEquivalence_functor_comp_snd (p : X ⥤ C) (f : U ⥤ X)
    (c : p.ChoiceOfPullbacks) {V : C} (x : p.Fiber V) (n : ℕ) :
    (nerveBaseChangeEquivalence p f c x n).functor ⋙
        TwoFibreProductOver.snd (Over.forget V) (Tuple.projection p f n ⋙ p) p
          (c.sliceFunctor x) (Tuple.projection p f n) =
      Cech.nerveMap p (Over.forget V) f
        (TwoFibreProductOver.fst (Over.forget V) (f ⋙ p) p (c.sliceFunctor x) f)
        (TwoFibreProductOver.snd (Over.forget V) (f ⋙ p) p (c.sliceFunctor x) f)
        (c.sliceFunctor x)
        (TwoFibreProductOver.psiIso (Over.forget V) (f ⋙ p) p (c.sliceFunctor x) f).symm
        (c.sliceFunctor_comp x)
        (isHomLift_psi_inv (Over.forget V) p (c.sliceFunctor x) f) n

Stacks.RelativeCech.complexSectionsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/RelativeSections.lean, line 663. The attribute's comment: “isomorphism of complexes”.

The value at an object x of 𝒳 of the relative Čech complex of f is canonically the Čech complex of the base change of f to the slice 𝒞/p(x), which represents x. This is an isomorphism of complexes: it is compatible with the Čech differentials.

public def complexSectionsIso (p : X ⥤ C) (f : U ⥤ X) (hp : p.IsFiberedInGroupoids)
    (c : p.ChoiceOfPullbacks) {V : C} (x : p.Fiber V)
    (F : Xᵒᵖ ⥤ AddCommGrpCat.{max uU uX uC vU vX vC w}) :
    (((evaluation Xᵒᵖ AddCommGrpCat.{max uU uX uC vU vX vC w}).obj
          (op x.1)).mapHomologicalComplex (ComplexShape.up ℕ)).obj
        (complex.{vU, vX, vC, uU, uX, uC, max uC vC vU w} p f F) ≅
      Cech.complex (Over.forget V)
        (TwoFibreProductOver.fst (Over.forget V) (f ⋙ p) p (c.sliceFunctor x) f)
        ((c.sliceFunctor x).op ⋙ F)

Stacks.RelativeCech.complexSectionsIso_π, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/RelativeSections.lean, line 695. The attribute's comment: “componentwise identification”.

On a Čech tuple of the base-changed covering, the identification of complexes restricts a relative section along the chosen pullback comparison of the tuple's target and then applies the right-Kan-extension counit.

public theorem complexSectionsIso_π (p : X ⥤ C) (f : U ⥤ X) (hp : p.IsFiberedInGroupoids)
    (c : p.ChoiceOfPullbacks) {V : C} (x : p.Fiber V)
    (F : Xᵒᵖ ⥤ AddCommGrpCat.{max uU uX uC vU vX vC w}) (n : ℕ)
    (a : Tuple (Over.forget V)
      (TwoFibreProductOver.fst (Over.forget V) (f ⋙ p) p (c.sliceFunctor x) f) n)
    (s : (term.{vU, vX, vC, uU, uX, uC, max uC vC vU w} p f F n).obj (op x.1)) :
    ((complexSectionsIso p f hp c x F).hom.f n ≫
        limit.π ((Tuple.projection (Over.forget V)
          (TwoFibreProductOver.fst (Over.forget V) (f ⋙ p) p (c.sliceFunctor x) f) n).op ⋙
            (c.sliceFunctor x).op ⋙ F) (op a)) s =
      ((Tuple.projection p f n).op.ranCounit.app ((Tuple.projection p f n).op ⋙ F)).app
          (op ((Cech.nerveMap p (Over.forget V) f
            (TwoFibreProductOver.fst (Over.forget V) (f ⋙ p) p (c.sliceFunctor x) f)
            (TwoFibreProductOver.snd (Over.forget V) (f ⋙ p) p (c.sliceFunctor x) f)
            (c.sliceFunctor x)
            (TwoFibreProductOver.psiIso (Over.forget V) (f ⋙ p) p (c.sliceFunctor x) f).symm
            (c.sliceFunctor_comp x)
            (isHomLift_psi_inv (Over.forget V) p (c.sliceFunctor x) f) n).obj a))
        ((term.{vU, vX, vC, uU, uX, uC, max uC vC vU w} p f F n).map
          (c.map a.target.hom x).op s)

Stacks.RelativeCech.complexSectionsIso_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/RelativeSections.lean, line 720. The attribute's comment: “naturality in the coefficient presheaf”.

The identification commutes in every degree with a morphism of coefficient presheaves; in particular it is natural in the abelian presheaf.

public theorem complexSectionsIso_naturality (p : X ⥤ C) (f : U ⥤ X)
    (hp : p.IsFiberedInGroupoids) (c : p.ChoiceOfPullbacks) {V : C} (x : p.Fiber V)
    (F G : Xᵒᵖ ⥤ AddCommGrpCat.{max uU uX uC vU vX vC w}) (η : F ⟶ G) (n : ℕ) :
    ((Tuple.projection p f n).op.ran.map
          (Functor.whiskerLeft (Tuple.projection p f n).op η)).app (op x.1) ≫
        (complexSectionsIso p f hp c x G).hom.f n =
      (complexSectionsIso p f hp c x F).hom.f n ≫
        limMap (Functor.whiskerLeft ((Tuple.projection (Over.forget V)
          (TwoFibreProductOver.fst (Over.forget V) (f ⋙ p) p (c.sliceFunctor x) f) n) ⋙
            c.sliceFunctor x).op η)

Tag 06XC, a lemma

Tag 06XC in the Stacks Project.

Stacks.RelativeCech.isIso_baseChangeMap_of_isTwoFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/RelativeBaseChange.lean, line 371.

Stacks 06XC. Base change along a 2-fibre-product square induces an isomorphism of relative Čech complexes of abelian presheaves. The comparison with the concrete 2-fibre product is required to be an equivalence, including when its category of objects lives in a larger universe.

public theorem isIso_baseChangeMap_of_isTwoFibreProduct
    {X₀ : Type uX} {U₀ : Type uU} {Y₀ : Type uY} {V₀ : Type uV}
    [Category.{vX} X₀] [Category.{vU} U₀]
    [Category.{vY} Y₀] [Category.{vV} V₀]
    (pX : X₀ ⥤ C) (pU : U₀ ⥤ C) (pY : Y₀ ⥤ C) (pV : V₀ ⥤ C)
    (f₀ : U₀ ⥤ X₀) (e₀ : Y₀ ⥤ X₀) (g₀ : V₀ ⥤ Y₀) (h₀ : V₀ ⥤ U₀)
    (hf : f₀ ⋙ pX = pU) (he : e₀ ⋙ pX = pY)
    (hg : g₀ ⋙ pY = pV) (hh : h₀ ⋙ pU = pV)
    (α : h₀ ⋙ f₀ ≅ g₀ ⋙ e₀)
    (hα : ∀ v : V₀, pX.IsHomLift
      (𝟙 (pX.obj (f₀.obj (h₀.obj v)))) (α.hom.app v))
    (hpX : pX.IsFiberedInGroupoids) (hpU : pU.IsFiberedInGroupoids)
    (hpY : pY.IsFiberedInGroupoids) (hpV : pV.IsFiberedInGroupoids)
    (hP : (TwoFibreProductOver.lift pU pY pX f₀ e₀ pV h₀ g₀
      hh hg α (by
        intro v
        have hv : pX.obj (f₀.obj (h₀.obj v)) = pV.obj v := by
          calc
            _ = pU.obj (h₀.obj v) := Functor.congr_obj hf _
            _ = pV.obj v := Functor.congr_obj hh _
        rw [← hv]
        exact hα v)).IsEquivalence)
    (F : X₀ᵒᵖ ⥤ AddCommGrpCat.{max uU uX vX uV uY vY w}) :
    IsIso (baseChangeMap pX f₀ e₀ g₀ h₀ α hα F)

Tag 06XD, a lemma

Tag 06XD in the Stacks Project.

Stacks.exact_of_exact_inverseImage_of_covering_image, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/ExactnessCriterion.lean, line 56.

Exactness of a complex of abelian sheaves can be checked after pullback to a fibred category whose image covers the target locally.

public theorem exact_of_exact_inverseImage_of_covering_image
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒰 : Type vᵤ} [Category.{wᵤ} 𝒰]
    {𝒳 : Type vₓ} [Category.{wₓ} 𝒳]
    (p : 𝒰 ⥤ AlgebraicGeometry.BigFppfOver B S hS)
    (q : 𝒳 ⥤ AlgebraicGeometry.BigFppfOver B S hS)
    (F : 𝒰 ⥤ 𝒳)
    (hp : p.IsFiberedInGroupoids) (hq : q.IsFiberedInGroupoids)
    (hF : p.IsFibredOneMorphism q F)
    (τ : AlgebraicGeometry.SiteKind)
    (hcover : ∀ x : 𝒳, ∃ R : Sieve x,
      R ∈ AlgebraicGeometry.BigFppfOver.associatedTopology B S hS q τ x ∧
        ∀ ⦃y : 𝒳⦄ (g : y ⟶ x), R g →
          ∃ z : 𝒰, Nonempty (y ≅ F.obj z))
    (C : ShortComplex (CategoryTheory.Sheaf
      (AlgebraicGeometry.BigFppfOver.associatedTopology B S hS q τ) Ab.{a})) :
    (letI : p.IsFibered := hp.isFibered
     letI : q.IsFibered := hq.isFibered
     letI := (hF.isContinuous_and_isCocontinuous_inheritedTopology
       ((AlgebraicGeometry.BigFppfSite.baseTopology B τ).over (B.obj hS))).1
     letI : (F.sheafPushforwardContinuous Ab.{a}
       (AlgebraicGeometry.BigFppfOver.associatedTopology B S hS p τ)
       (AlgebraicGeometry.BigFppfOver.associatedTopology B S hS q τ)).PreservesZeroMorphisms :=
       ⟨by intros; rfl⟩
     (C.map (F.sheafPushforwardContinuous Ab.{a}
       (AlgebraicGeometry.BigFppfOver.associatedTopology B S hS p τ)
       (AlgebraicGeometry.BigFppfOver.associatedTopology B S hS q τ))).Exact) → C.Exact

Tag 06XE, a proposition

Tag 06XE in the Stacks Project.

Stacks.RelativeCech.mono_sheafAugmentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/RelativeExactness.lean, line 615. The attribute's comment: “exactness at the initial sheaf”.

Stacks 06XE. Exactness of the extended relative Čech complex at its initial term: if the image of f covers every object of 𝒳 locally, the augmentation of an abelian sheaf into degree 0 of its sheafified relative Čech complex is a monomorphism.

public theorem mono_sheafAugmentation
    (hcover : ∀ x : 𝒳, ∃ R : Presieve x,
      Sieve.generate R ∈ AlgebraicGeometry.BigFppfOver.associatedTopology B S hS q τ x ∧
        ∀ ⦃y : 𝒳⦄ (g : y ⟶ x), R g → ∃ z : 𝒰, Nonempty (y ≅ f.obj z))
    [HasSheafify (AlgebraicGeometry.BigFppfOver.associatedTopology B S hS q τ)
      AddCommGrpCat.{max vᵤ vₓ wₓ t}]
    (𝓕 : Sheaf (AlgebraicGeometry.BigFppfOver.associatedTopology B S hS q τ)
      AddCommGrpCat.{max vᵤ vₓ wₓ t}) :
    Mono (sheafAugmentation.{u, vᵤ, vₓ, wᵤ, wₓ, t} B S hS q f τ 𝓕)

Stacks.RelativeCech.exact_sheafAugmentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/RelativeExactness.lean, line 682. The attribute's comment: “exactness at degree zero”.

Stacks 06XE. Exactness of the extended relative Čech complex in degree zero: if f is a 1-morphism of categories fibred in groupoids whose image covers every object of 𝒳 locally, the augmentation of an abelian sheaf is the kernel of the first differential of its sheafified relative Čech complex.

public theorem exact_sheafAugmentation
    (hp : p.IsFiberedInGroupoids) (hq : q.IsFiberedInGroupoids)
    (hf : p.IsFibredOneMorphism q f)
    (hcover : ∀ x : 𝒳, ∃ R : Presieve x,
      Sieve.generate R ∈ AlgebraicGeometry.BigFppfOver.associatedTopology B S hS q τ x ∧
        ∀ ⦃y : 𝒳⦄ (g : y ⟶ x), R g → ∃ z : 𝒰, Nonempty (y ≅ f.obj z))
    [HasSheafify (AlgebraicGeometry.BigFppfOver.associatedTopology B S hS q τ)
      AddCommGrpCat.{max vᵤ vₓ wₓ t}]
    (𝓕 : Sheaf (AlgebraicGeometry.BigFppfOver.associatedTopology B S hS q τ)
      AddCommGrpCat.{max vᵤ vₓ wₓ t}) :
    (ShortComplex.mk (sheafAugmentation.{u, vᵤ, vₓ, wᵤ, wₓ, t} B S hS q f τ 𝓕)
      ((sheafComplex.{u, vᵤ, vₓ, wᵤ, wₓ, t} B S hS q f τ 𝓕).d 0 1)
      (sheafAugmentation_comp_d.{u, vᵤ, vₓ, wᵤ, wₓ, t} B S hS q f τ 𝓕)).Exact

Stacks.RelativeCech.exactAt_sheafComplex_succ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/RelativeExactness.lean, line 707. The attribute's comment: “exactness in positive degrees”.

Stacks 06XE. Exactness of the extended relative Čech complex in every positive degree: if f is a 1-morphism of categories fibred in groupoids whose image covers every object of 𝒳 locally, the sheafified relative Čech complex of an abelian sheaf is exact in every positive degree.

public theorem exactAt_sheafComplex_succ
    (hp : p.IsFiberedInGroupoids) (hq : q.IsFiberedInGroupoids)
    (hf : p.IsFibredOneMorphism q f)
    (hcover : ∀ x : 𝒳, ∃ R : Presieve x,
      Sieve.generate R ∈ AlgebraicGeometry.BigFppfOver.associatedTopology B S hS q τ x ∧
        ∀ ⦃y : 𝒳⦄ (g : y ⟶ x), R g → ∃ z : 𝒰, Nonempty (y ≅ f.obj z))
    [HasSheafify (AlgebraicGeometry.BigFppfOver.associatedTopology B S hS q τ)
      AddCommGrpCat.{max vᵤ vₓ wₓ t}]
    (𝓕 : Sheaf (AlgebraicGeometry.BigFppfOver.associatedTopology B S hS q τ)
      AddCommGrpCat.{max vᵤ vₓ wₓ t}) (n : ℕ) :
    (sheafComplex.{u, vᵤ, vₓ, wᵤ, wₓ, t} B S hS q f τ 𝓕).ExactAt (n + 1)

Tag 06XF, a lemma

Tag 06XF in the Stacks Project.

Stacks.RelativeCech.exists_spectralSequenceData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/RelativeSpectralSequence/Abelian.lean, line 120.

For a faithful 1-morphism f : 𝒰 ⥤ 𝒳 of categories fibred in groupoids over the big fppf site of S, with equalizers in 𝒰 and image covering 𝒳 locally, there is a first-quadrant spectral sequence E₁^{i,j} = Hʲ((𝒰ᵢ)_τ, fᵢ⁻¹𝓕) ⇒ Hⁱ⁺ʲ(𝒳_τ, 𝓕).

public theorem exists_spectralSequenceData
    (hp : p.IsFiberedInGroupoids) (hq : q.IsFiberedInGroupoids)
    (hf : p.IsFibredOneMorphism q f) [f.Faithful] [HasEqualizers 𝒰]
    (hcover : ∀ x : 𝒳, ∃ R : Presieve x,
      Sieve.generate R ∈ BigFppfOver.associatedTopology B S hS q τ x ∧
        ∀ ⦃y : 𝒳⦄ (g : y ⟶ x), R g → ∃ z : 𝒰, Nonempty (y ≅ f.obj z))
    [HasSheafify (BigFppfOver.associatedTopology B S hS q τ)
      AddCommGrpCat.{max vᵤ vₓ wₓ a}]
    [HasExt.{b} (Sheaf (BigFppfOver.associatedTopology B S hS q τ)
      AddCommGrpCat.{max vᵤ vₓ wₓ a})]
    [∀ n : ℕ, HasSheafify
      (BigFppfOver.associatedTopology B S hS (Tuple.projection q f n ⋙ q) τ)
        AddCommGrpCat.{max vᵤ vₓ wₓ a}]
    [∀ n : ℕ, HasExt.{b} (Sheaf
      (BigFppfOver.associatedTopology B S hS (Tuple.projection q f n ⋙ q) τ)
        AddCommGrpCat.{max vᵤ vₓ wₓ a})]
    (𝓕 : Sheaf (BigFppfOver.associatedTopology B S hS q τ)
      AddCommGrpCat.{max vᵤ vₓ wₓ a}) :
    Nonempty (SpectralSequenceData (B := B) (S := S) (hS := hS)
      (q := q) (f := f) (τ := τ) 𝓕)

Tag 06XG, a lemma

Tag 06XG in the Stacks Project.

Stacks.RelativeCech.exists_moduleSpectralSequenceData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/RelativeSpectralSequenceModules/Abutment.lean, line 484.

For a faithful 1-morphism f : 𝒰 ⥤ 𝒳 of categories fibred in groupoids over (Sch/S)_fppf with equalizers in 𝒰, whose image covers 𝒳 locally in the τ-topology, every sheaf of 𝒪_𝒳-modules 𝓕 has a first-quadrant spectral sequence of Γ(𝒪_𝒳)-modules E₁^{i,j} = Hʲ((𝒰ᵢ)_τ, fᵢ^*𝓕) ⇒ Hⁱ⁺ʲ(𝒳_τ, 𝓕).

public theorem exists_moduleSpectralSequenceData
    (hp : p.IsFiberedInGroupoids) (hq : q.IsFiberedInGroupoids)
    (hf : p.IsFibredOneMorphism q f) [f.Faithful] [HasEqualizers 𝒰]
    (hcover : ∀ x : 𝒳, ∃ R : Presieve x,
      Sieve.generate R ∈ AlgebraicGeometry.BigFppfOver.associatedTopology B S hS q τ x ∧
        ∀ ⦃y : 𝒳⦄ (g : y ⟶ x), R g →
          ∃ z : 𝒰, Nonempty (y ≅ f.obj z))
    (𝓕 : SheafOfModules.{max u vᵤ vₓ wᵤ wₓ a}
      (AlgebraicGeometry.Stack.ringStructureSheafCore B S hS q hq (B.baseTopology τ)
        (B.baseTopology_le_topology τ))) :
    Nonempty (ModuleSpectralSequenceData.{u, vᵤ, vₓ, wᵤ, wₓ, a}
      B S hS q f τ hq 𝓕)

Tag 06XH, a lemma

Tag 06XH in the Stacks Project.

AlgebraicGeometry.Stack.exists_singleton_fppf_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/LocalLifts.lean, line 55. The attribute's comment: “part (1): fppf-local lifts along a surjective flat morphism”.

Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of categories fibred in groupoids over the big fppf site of S which is representable by algebraic spaces, and assume that the structure morphism of the algebraic space representing the base change of f along any scheme-valued point of 𝒴 is surjective, flat and locally of finite presentation. Then every object y of 𝒴 admits a morphism f(x) ⟶ y from the image of an object x of 𝒳 whose generated sieve covers y in the associated fppf site of 𝒴.

theorem exists_singleton_fppf_lift
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, v, u + 1, w} (BigFppfOver B S hS)} (f : 𝒳 ⟶ 𝒴)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom)
    (hsurj : ∀ (U : BigFppfOver B S hS) (q : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.val.obj)
      (hq : q ⋙ 𝒴.val.p = Over.map U.hom),
      Space.IsSurjective B S hS (baseChangeStructureMap B S hS f.hom hf U q hq).hom)
    (hflat : ∀ (U : BigFppfOver B S hS) (q : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.val.obj)
      (hq : q ⋙ 𝒴.val.p = Over.map U.hom),
      Space.IsFlat B S hS (baseChangeStructureMap B S hS f.hom hf U q hq).hom)
    (hlfp : ∀ (U : BigFppfOver B S hS) (q : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.val.obj)
      (hq : q ⋙ 𝒴.val.p = Over.map U.hom),
      Space.IsLocallyOfFinitePresentation B S hS
        (baseChangeStructureMap B S hS f.hom hf U q hq).hom)
    (y : 𝒴.val.obj) :
    ∃ (x : 𝒳.val.obj) (a : (CatFiberedInGroupoids.homFunctor f).obj x ⟶ y),
      Sieve.generate (Presieve.singleton a) ∈ fppfTopology B S hS 𝒴 y

AlgebraicGeometry.Stack.exists_etaleLocalLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/EtaleLocalLifts.lean, line 291. The attribute's comment: “part (2): étale-local lifts along a surjective smooth morphism”.

Let f : 𝒳 ⟶ 𝒴 be a surjective smooth 1-morphism of algebraic stacks. Then every object y of 𝒴 admits an object x of 𝒳 and a morphism f(x) ⟶ y whose singleton generates a covering sieve of the étale topology that 𝒴 inherits from the site.

theorem exists_etaleLocalLift {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hsurj : IsSurjective B S hS f)
    (hsmooth : AlgebraicStacks.IsSmooth B S hS f)
    (y : 𝒴.val.val.obj) :
    ∃ (x : 𝒳.val.val.obj) (a : (CatFiberedInGroupoids.homFunctor f.hom).obj x ⟶ y),
      Sieve.generate (Presieve.singleton a) ∈
        BigFppfOver.associatedTopology B S hS 𝒴.val.val.p .etale y

AlgebraicGeometry.Stack.exists_etaleCovering_fibre_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/EtaleLocalLifts.lean, line 305. The attribute's comment: “part (2): étale covering of the base with a lift over every arrow”.

Along a surjective smooth 1-morphism of algebraic stacks, every object of the base carries a covering sieve of the étale topology over each of whose arrows the given object of the fibre lifts.

theorem exists_etaleCovering_fibre_lift {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hsurj : IsSurjective B S hS f)
    (hsmooth : AlgebraicStacks.IsSmooth B S hS f)
    (U : BigFppfOver B S hS) (y : 𝒴.val.val.p.Fiber U) :
    ∃ R ∈ BigFppfOver.baseOverTopology B S hS .etale U,
      ∀ ⦃V : BigFppfOver B S hS⦄ ⦃k : V ⟶ U⦄, R.arrows k →
        ∃ (x : 𝒳.val.val.obj) (α : (CatFiberedInGroupoids.homFunctor f.hom).obj x ⟶ y.1),
          𝒴.val.val.p.IsHomLift k α

AlgebraicGeometry.Stack.exists_etaleLocalLift_of_representable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/EtaleLocalLifts.lean, line 390. The attribute's comment: “part (2) in full generality: étale-local lifts along a 1-morphism of CFGs”.

Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of categories fibred in groupoids over the big fppf site of S which is representable by algebraic spaces, and suppose that every algebraic space representing the base change of f along a scheme-valued point of 𝒴 has surjective and smooth structural morphism. Then every object y of 𝒴 admits an object x of 𝒳 and a morphism a : f(x) ⟶ y whose singleton generates a covering sieve of the étale topology 𝒴 inherits from the site.

theorem exists_etaleLocalLift_of_representable
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, v, u + 1, w} (BigFppfOver B S hS)} (f : 𝒳 ⟶ 𝒴)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom)
    (hprop : ∀ (V : BigFppfOver B S hS)
      (yv : BigFppfOver B V.left.1 V.left.2 ⥤ 𝒴.val.obj)
      (_hyv : yv ⋙ 𝒴.val.p = Over.map V.hom)
      (F : (BigFppfOver B V.left.1 V.left.2)ᵒᵖ ⥤ Type u)
      (hF : IsAlgebraicSpace B V.left.1 V.left.2 F),
      Nonempty (StacksRepresentableCFG.EquivalenceOver
        (TwoFibreProductOver.fst (Over.map V.hom) 𝒳.val.p 𝒴.val.p yv
          (CatFiberedInGroupoids.homFunctor f))
        (presheafOfCategories (F ⋙ typeToCat)).p) →
      (let h := (algebraicSpaceMap B S hS V
        ((spacesOverSmallerBaseFunctor B V.left.1 S V.left.2 hS V.hom).obj ⟨F, hF⟩)).hom
       Space.IsSurjective B S hS h ∧ Space.IsSmooth B S hS h))
    (y : 𝒴.val.obj) :
    ∃ (x : 𝒳.val.obj) (a : (CatFiberedInGroupoids.homFunctor f).obj x ⟶ y),
      Sieve.generate (Presieve.singleton a) ∈
        BigFppfOver.associatedTopology B S hS 𝒴.val.p .etale y

AlgebraicGeometry.Stack.exists_etaleCovering_fibre_lift_of_representable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/EtaleLocalLifts.lean, line 418. The attribute's comment: “part (2) in full generality, family form: an étale covering of the base”.

Along a 1-morphism of categories fibred in groupoids representable by algebraic spaces whose base change along every scheme-valued point is surjective and smooth, every object of the base carries a covering sieve of the étale topology over each of whose arrows the given object of the fibre lifts.

theorem exists_etaleCovering_fibre_lift_of_representable
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, v, u + 1, w} (BigFppfOver B S hS)} (f : 𝒳 ⟶ 𝒴)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom)
    (hprop : ∀ (V : BigFppfOver B S hS)
      (yv : BigFppfOver B V.left.1 V.left.2 ⥤ 𝒴.val.obj)
      (_hyv : yv ⋙ 𝒴.val.p = Over.map V.hom)
      (F : (BigFppfOver B V.left.1 V.left.2)ᵒᵖ ⥤ Type u)
      (hF : IsAlgebraicSpace B V.left.1 V.left.2 F),
      Nonempty (StacksRepresentableCFG.EquivalenceOver
        (TwoFibreProductOver.fst (Over.map V.hom) 𝒳.val.p 𝒴.val.p yv
          (CatFiberedInGroupoids.homFunctor f))
        (presheafOfCategories (F ⋙ typeToCat)).p) →
      (let h := (algebraicSpaceMap B S hS V
        ((spacesOverSmallerBaseFunctor B V.left.1 S V.left.2 hS V.hom).obj ⟨F, hF⟩)).hom
       Space.IsSurjective B S hS h ∧ Space.IsSmooth B S hS h))
    (U : BigFppfOver B S hS) (y : 𝒴.val.p.Fiber U) :
    ∃ R ∈ BigFppfOver.baseOverTopology B S hS .etale U,
      ∀ ⦃V : BigFppfOver B S hS⦄ ⦃k : V ⟶ U⦄, R.arrows k →
        ∃ (x : 𝒳.val.obj) (α : (CatFiberedInGroupoids.homFunctor f).obj x ⟶ y.1),
          𝒴.val.p.IsHomLift k α

AlgebraicGeometry.Stack.exists_fppfLocalLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/FppfLocalLifts.lean, line 130. The attribute's comment: “fppf_local_lifts”.

Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of categories fibred in groupoids over the big fppf site of S which is representable by algebraic spaces, and suppose that every algebraic space representing the base change of f along a scheme-valued point of 𝒴 has surjective, flat and locally finitely presented structural morphism. Then every object y of 𝒴 admits an object x of 𝒳 and a morphism a : f(x) ⟶ y whose singleton generates a covering sieve of the fppf topology 𝒴 inherits from the site.

theorem exists_fppfLocalLift
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, v, u + 1, w} (BigFppfOver B S hS)} (f : 𝒳 ⟶ 𝒴)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom)
    (hprops : ∀ (T : BigFppfOver B S hS)
      (y : BigFppfOver B T.left.1 T.left.2 ⥤ 𝒴.val.obj)
      (_hy : y ⋙ 𝒴.val.p = Over.map T.hom)
      (F : (BigFppfOver B T.left.1 T.left.2)ᵒᵖ ⥤ Type u)
      (hF : IsAlgebraicSpace B T.left.1 T.left.2 F),
      Nonempty (StacksRepresentableCFG.EquivalenceOver
        (TwoFibreProductOver.fst (Over.map T.hom) 𝒳.val.p 𝒴.val.p y
          (CatFiberedInGroupoids.homFunctor f))
        (presheafOfCategories (F ⋙ typeToCat)).p) →
      (let g := (algebraicSpaceMap B S hS T
        ((spacesOverSmallerBaseFunctor B T.left.1 S T.left.2 hS T.hom).obj ⟨F, hF⟩)).hom
       Space.IsSurjective B S hS g ∧ Space.IsFlat B S hS g ∧
         Space.IsLocallyOfFinitePresentation B S hS g))
    (y : 𝒴.val.obj) :
    ∃ (x : 𝒳.val.obj) (a : (CatFiberedInGroupoids.homFunctor f).obj x ⟶ y),
      Sieve.generate (Presieve.singleton a) ∈
        BigFppfOver.associatedTopology B S hS 𝒴.val.p .fppf y

Tag 072D, a lemma

Tag 072D in the Stacks Project.

Stacks.RelativeCech.exists_pushforwardSpectralSequenceData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/RelativeSpectralSequence/Abelian.lean, line 429.

Let f : 𝒰 ⥤ 𝒳 and g : 𝒳 ⥤ 𝒴 be 1-morphisms of categories fibred in groupoids over the big fppf site of S, with f faithful, with equalizers in 𝒰 and with the image of f covering 𝒳 locally for the topology τ. For an abelian sheaf 𝓕 on 𝒳_τ there is a first-quadrant spectral sequence of abelian sheaves on 𝒴_τ with first page E₁^{i,j} = Rʲ(g ∘ fᵢ)_* fᵢ⁻¹𝓕 abutting to Rⁱ⁺ʲ g_* 𝓕.

public theorem exists_pushforwardSpectralSequenceData
    (hp : p.IsFiberedInGroupoids) (hq : q.IsFiberedInGroupoids) (hr : r.IsFiberedInGroupoids)
    (hf : p.IsFibredOneMorphism q f) (hg : q.IsFibredOneMorphism r g)
    [f.Faithful] [HasEqualizers 𝒰]
    (hcover : ∀ x : 𝒳, ∃ R : Presieve x,
      Sieve.generate R ∈ BigFppfOver.associatedTopology B S hS q τ x ∧
        ∀ ⦃y : 𝒳⦄ (k : y ⟶ x), R k → ∃ z : 𝒰, Nonempty (y ≅ f.obj z))
    [HasSheafify (BigFppfOver.associatedTopology B S hS q τ)
      AddCommGrpCat.{max v₁ w₁ v₂ w₂ v₃ w₃ a}]
    [HasSheafify (BigFppfOver.associatedTopology B S hS r τ)
      AddCommGrpCat.{max v₁ w₁ v₂ w₂ v₃ w₃ a}]
    [∀ n : ℕ, HasSheafify
      (BigFppfOver.associatedTopology B S hS (Tuple.projection q f n ⋙ q) τ)
        AddCommGrpCat.{max v₁ w₁ v₂ w₂ v₃ w₃ a}]
    [∀ P : 𝒳ᵒᵖ ⥤ AddCommGrpCat.{max v₁ w₁ v₂ w₂ v₃ w₃ a},
      g.op.HasPointwiseRightKanExtension P]
    [∀ (n : ℕ) (P : (Tuple q f n)ᵒᵖ ⥤ AddCommGrpCat.{max v₁ w₁ v₂ w₂ v₃ w₃ a}),
      (Tuple.projection q f n ⋙ g).op.HasPointwiseRightKanExtension P]
    (𝓕 : Sheaf (BigFppfOver.associatedTopology B S hS q τ)
      AddCommGrpCat.{max v₁ w₁ v₂ w₂ v₃ w₃ a}) :
    Nonempty (PushforwardSpectralSequenceData (B := B) (S := S) (hS := hS)
      (q := q) (r := r) (f := f) (g := g) (τ := τ) 𝓕)

Tag 072E, a lemma

Tag 072E in the Stacks Project.

Stacks.RelativeCech.nonempty_modulePushforwardSpectralSequenceData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/ModulePushforwardSpectralSequence.lean, line 79.

Stacks 072E. Let f : 𝒰 ⥤ 𝒳 and g : 𝒳 ⥤ 𝒴 be 1-morphisms of categories fibred in groupoids over the big fppf site of S, with f faithful, with equalizers in 𝒰 and with the image of f covering 𝒳 locally for the topology τ. For a sheaf of 𝒪_𝒳-modules 𝓕 on 𝒳_τ there is a first-quadrant spectral sequence of sheaves of 𝒪_𝒴-modules on 𝒴_τ with first page E₁^{i,j} = Rʲ(g ∘ fᵢ)_* fᵢ⁻¹𝓕 abutting to Rⁱ⁺ʲ g_* 𝓕, all higher direct images being computed in the τ-topology.

public theorem nonempty_modulePushforwardSpectralSequenceData
    [f.Faithful] [HasEqualizers 𝒰]
    (hcover : ∀ x : 𝒳, ∃ R : Presieve x,
      Sieve.generate R ∈ AlgebraicGeometry.BigFppfOver.associatedTopology B S hS q τ x ∧
        ∀ ⦃y : 𝒳⦄ (k : y ⟶ x), R k → ∃ z : 𝒰, Nonempty (y ≅ f.obj z))
    (𝓕 : SheafOfModules.{max u v₁ w₁ v₂ w₂ v₃ w₃ a} (moduleRingSheaf B S hS q hq τ)) :
    Nonempty (ModulePushforwardSpectralSequenceData.{u, v₁, v₂, v₃, w₁, w₂, w₃, a}
      B S hS p q r f g τ hp hq hr hf hg 𝓕)

Stacks.RelativeCech.exists_modulePushforwardSpectralSequenceData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/RelativeSpectralSequence/Modules.lean, line 325.

Let f : 𝒰 ⥤ 𝒳 and g : 𝒳 ⥤ 𝒴 be 1-morphisms of categories fibred in groupoids over the big fppf site of S, with f faithful, with equalizers in 𝒰 and with the image of f covering 𝒳 locally for the topology τ. For a sheaf of 𝒪_𝒳-modules 𝓕 on 𝒳_τ there is a first-quadrant spectral sequence of sheaves of 𝒪_𝒴-modules on 𝒴_τ with first page E₁^{i,j} = Rʲ(g ∘ fᵢ)_* fᵢ⁻¹𝓕 abutting to Rⁱ⁺ʲ g_* 𝓕, all higher direct images being computed in the τ-topology.

public theorem exists_modulePushforwardSpectralSequenceData
    [f.Faithful] [HasEqualizers 𝒰]
    (hcover : ∀ x : 𝒳, ∃ R : Presieve x,
      Sieve.generate R ∈ AlgebraicGeometry.BigFppfOver.associatedTopology B S hS q τ x ∧
        ∀ ⦃y : 𝒳⦄ (k : y ⟶ x), R k → ∃ z : 𝒰, Nonempty (y ≅ f.obj z))
    (hRightAdjoint : ∀ n : ℕ, (PresheafOfModules.pushforward.{max u v₁ w₁ v₂ w₂ v₃ w₃ a}
      (AlgebraicGeometry.Stack.ringStructureSheafCoreHom B S hS
        (Tuple.projection q f n ⋙ q) q (Tuple.projection q f n) (B.baseTopology τ)
        (tupleProjection_comp_isFiberedInGroupoids B S hS p q f hp hq hf n) hq rfl
        (B.baseTopology_le_topology τ)).hom).IsRightAdjoint)
    [∀ (n : ℕ) (G : (Tuple q f n)ᵒᵖ ⥤ AddCommGrpCat.{max u v₁ w₁ v₂ w₂ v₃ w₃ a}),
      (Tuple.projection q f n).op.HasPointwiseLeftKanExtension G]
    [HasSheafify (AlgebraicGeometry.BigFppfOver.associatedTopology B S hS q τ)
      AddCommGrpCat.{max u v₁ w₁ v₂ w₂ v₃ w₃ a}]
    [(AlgebraicGeometry.BigFppfOver.associatedTopology B S hS q τ).WEqualsLocallyBijective
      AddCommGrpCat.{max u v₁ w₁ v₂ w₂ v₃ w₃ a}]
    [HasSheafify (AlgebraicGeometry.BigFppfOver.associatedTopology B S hS r τ)
      AddCommGrpCat.{max u v₁ w₁ v₂ w₂ v₃ w₃ a}]
    [(AlgebraicGeometry.BigFppfOver.associatedTopology B S hS r τ).WEqualsLocallyBijective
      AddCommGrpCat.{max u v₁ w₁ v₂ w₂ v₃ w₃ a}]
    [∀ n : ℕ, HasSheafify (AlgebraicGeometry.BigFppfOver.associatedTopology B S hS
      (Tuple.projection q f n ⋙ q) τ) AddCommGrpCat.{max u v₁ w₁ v₂ w₂ v₃ w₃ a}]
    [∀ n : ℕ, (AlgebraicGeometry.BigFppfOver.associatedTopology B S hS
      (Tuple.projection q f n ⋙ q) τ).WEqualsLocallyBijective
        AddCommGrpCat.{max u v₁ w₁ v₂ w₂ v₃ w₃ a}]
    [∀ n : ℕ, EnoughInjectives (SheafOfModules.{max u v₁ w₁ v₂ w₂ v₃ w₃ a}
      (moduleRingSheaf B S hS (Tuple.projection q f n ⋙ q)
        (tupleProjection_comp_isFiberedInGroupoids B S hS p q f hp hq hf n) τ))]
    [EnoughInjectives (SheafOfModules.{max u v₁ w₁ v₂ w₂ v₃ w₃ a} (moduleRingSheaf B S hS q hq τ))]
    (𝓕 : SheafOfModules.{max u v₁ w₁ v₂ w₂ v₃ w₃ a} (moduleRingSheaf B S hS q hq τ)) :
    Nonempty (ModulePushforwardSpectralSequenceData.{u, v₁, v₂, v₃, w₁, w₂, w₃, a}
      B S hS p q r f g τ hp hq hr hf hg 𝓕)

Sources

LeanStacks.RelativeCech.complex · Stacks.presheafPullbackMap · Stacks.presheafPullbackMap_natural · Stacks.presheafPullbackMap_whiskerLeft_ranCounit · Stacks.RelativeCech.reindexMap_eq_presheafPullbackMap · Stacks.sheafPullbackMap · Stacks.sheafPullbackMap_hom · Stacks.sheafPullbackMap_natural

Section96.20 Cohomology on algebraic stacks #

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

Tag 06XJ, a proposition

Tag 06XJ in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.exists_etaleCechSpectralSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/SmoothCoveringSpectralSequence.lean, line 266. The attribute's comment: “part (1): the étale spectral sequence of a presentation which is representable by algebraic spaces, surjective and smooth”.

Stacks 06XJ, part (1). Let f : 𝒰 ⟶ 𝒳 be a 1-morphism of algebraic stacks which is representable by algebraic spaces, surjective and smooth, and let 𝓕 be an abelian sheaf on the étale site of 𝒳. Then there is a first-quadrant spectral sequence E₁^{p,q} = H^q_étale(𝒰ₚ, fₚ⁻¹𝓕) ⇒ H^{p+q}_étale(𝒳, 𝓕), where 𝒰ₚ = 𝒰 ×_𝒳 ⋯ ×_𝒳 𝒰 (p + 1 factors) is the degree p term of the relative Čech nerve of f and fₚ : 𝒰ₚ ⟶ 𝒳 its projection; the first page, the first-quadrant vanishing and the convergence to the étale cohomology of 𝓕 are the fields of Stacks.RelativeCech.SpectralSequenceData.

theorem exists_etaleCechSpectralSequence
    (hrep : Stack.IsRepresentableByAlgebraicSpaces B S hS f.hom.hom)
    (hsurj : Stack.IsSurjective B S hS f) (hsmooth : IsSmooth B S hS f)
    (𝓕 : Sheaf (BigFppfOver.associatedTopology B S hS 𝒳.val.val.p SiteKind.etale)
      AddCommGrpCat.{max (u + 1) a}) :
    Nonempty (Stacks.RelativeCech.SpectralSequenceData B S hS 𝒳.val.val.p
      (CatFiberedInGroupoids.homFunctor f.hom) SiteKind.etale 𝓕)

AlgebraicGeometry.Stack.AlgebraicStacks.exists_fppfCechSpectralSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/SmoothCoveringSpectralSequence.lean, line 285. The attribute's comment: “part (2): the fppf spectral sequence of a presentation which is representable by algebraic spaces, surjective, flat and locally of finite presentation”.

Stacks 06XJ, part (2). Let f : 𝒰 ⟶ 𝒳 be a 1-morphism of algebraic stacks which is representable by algebraic spaces, surjective, flat and locally of finite presentation, and let 𝓕 be an abelian sheaf on (the fppf site of) 𝒳. Then there is a first-quadrant spectral sequence E₁^{p,q} = H^q_fppf(𝒰ₚ, fₚ⁻¹𝓕) ⇒ H^{p+q}_fppf(𝒳, 𝓕), where 𝒰ₚ = 𝒰 ×_𝒳 ⋯ ×_𝒳 𝒰 (p + 1 factors) is the degree p term of the relative Čech nerve of f and fₚ : 𝒰ₚ ⟶ 𝒳 its projection; the first page, the first-quadrant vanishing and the convergence to the fppf cohomology of 𝓕 are the fields of Stacks.RelativeCech.SpectralSequenceData.

theorem exists_fppfCechSpectralSequence
    (hrep : Stack.IsRepresentableByAlgebraicSpaces B S hS f.hom.hom)
    (hsurj : Stack.IsSurjective B S hS f) (hflat : IsFlat B S hS f)
    (hlfp : IsLocallyOfFinitePresentation B S hS f)
    (𝓕 : Sheaf (BigFppfOver.associatedTopology B S hS 𝒳.val.val.p SiteKind.fppf)
      AddCommGrpCat.{max (u + 1) a}) :
    Nonempty (Stacks.RelativeCech.SpectralSequenceData B S hS 𝒳.val.val.p
      (CatFiberedInGroupoids.homFunctor f.hom) SiteKind.fppf 𝓕)

Sources

LeanAlgebraicGeometry.Stack.AlgebraicStacks.exists_etaleCechSpectralSequence · AlgebraicGeometry.Stack.AlgebraicStacks.exists_fppfCechSpectralSequence

Section96.21 Higher direct images and algebraic stacks #

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

Tag 072G, a proposition

Tag 072G in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.exists_etaleDirectImageSpectralSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/PresentationDirectImageSpectralSequence.lean, line 123. The attribute's comment: “part (1)(a): spectral sequence in Ab(𝒴_étale) along a smooth surjective presentation”.

Let f : 𝒰 ⟶ 𝒳 and g : 𝒳 ⟶ 𝒴 be composable 1-morphisms of algebraic stacks and assume f is representable by algebraic spaces, surjective and smooth. For an abelian sheaf 𝓕 on the étale site of 𝒳 there is a first-quadrant spectral sequence of abelian sheaves on the étale site of 𝒴 E₁^{p,q} = R^q (g ∘ fₚ)_* fₚ⁻¹𝓕 ⇒ R^{p+q} g_* 𝓕, all higher direct images computed in the étale topology, where 𝒰ₚ is the degree p term of the relative Čech nerve of f, that is the (p+1)-fold fibre product of 𝒰 over 𝒳, and fₚ its projection to 𝒳. The first page, the first-quadrant vanishing and the abutment are the fields of Stacks.RelativeCech.PushforwardSpectralSequenceData.

theorem exists_etaleDirectImageSpectralSequence
    (hrep : Stack.IsRepresentableByAlgebraicSpaces B S hS f.hom.hom)
    (hsurj : Stack.IsSurjective B S hS f) (hsmooth : IsSmooth B S hS f)
    (𝓕 : Sheaf (BigFppfOver.associatedTopology B S hS 𝒳.val.val.p SiteKind.etale)
      AddCommGrpCat.{max (u + 1) a}) :
    Nonempty (Stacks.RelativeCech.PushforwardSpectralSequenceData B S hS 𝒳.val.val.p
      𝒴.val.val.p (CatFiberedInGroupoids.homFunctor f.hom)
      (CatFiberedInGroupoids.homFunctor g.hom) SiteKind.etale 𝓕)

AlgebraicGeometry.Stack.AlgebraicStacks.exists_etaleModuleDirectImageSpectralSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/PresentationDirectImageSpectralSequence.lean, line 144. The attribute's comment: “part (1)(b): spectral sequence in Mod(𝒴_étale, 𝒪_𝒴) along a smooth surjective presentation”.

Let f : 𝒰 ⟶ 𝒳 and g : 𝒳 ⟶ 𝒴 be composable 1-morphisms of algebraic stacks and assume f is representable by algebraic spaces, surjective and smooth. For a sheaf of 𝒪_𝒳-modules 𝓕 on the étale site of 𝒳 there is a first-quadrant spectral sequence of sheaves of 𝒪_𝒴-modules on the étale site of 𝒴 E₁^{p,q} = R^q (g ∘ fₚ)_* fₚ⁻¹𝓕 ⇒ R^{p+q} g_* 𝓕, all higher direct images computed in sheaves of modules for the étale topology, where 𝒰ₚ is the degree p term of the relative Čech nerve of f and fₚ its projection to 𝒳. The first page, the first-quadrant vanishing and the abutment are the fields of Stacks.RelativeCech.ModulePushforwardSpectralSequenceData.

theorem exists_etaleModuleDirectImageSpectralSequence
    (hrep : Stack.IsRepresentableByAlgebraicSpaces B S hS f.hom.hom)
    (hsurj : Stack.IsSurjective B S hS f) (hsmooth : IsSmooth B S hS f)
    (𝓕 : SheafOfModules.{max (u + 1) a} (Stacks.RelativeCech.moduleRingSheaf B S hS
      𝒳.val.val.p 𝒳.val.isFiberedInGroupoids SiteKind.etale)) :
    Nonempty (Stacks.RelativeCech.ModulePushforwardSpectralSequenceData.{u, u + 1, u + 1, u + 1,
      u, u, u, a} B S hS 𝒰.val.val.p 𝒳.val.val.p 𝒴.val.val.p
      (CatFiberedInGroupoids.homFunctor f.hom) (CatFiberedInGroupoids.homFunctor g.hom)
      SiteKind.etale 𝒰.val.isFiberedInGroupoids 𝒳.val.isFiberedInGroupoids
      𝒴.val.isFiberedInGroupoids
      (Functor.isFibredOneMorphism_of_isFiberedInGroupoids 𝒳.val.isFiberedInGroupoids
        f.hom.hom.w)
      (Functor.isFibredOneMorphism_of_isFiberedInGroupoids 𝒴.val.isFiberedInGroupoids
        g.hom.hom.w) 𝓕)

AlgebraicGeometry.Stack.AlgebraicStacks.exists_fppfDirectImageSpectralSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/PresentationDirectImageSpectralSequence.lean, line 178. The attribute's comment: “part (2)(a): spectral sequence in Ab(𝒴) along a flat, locally finitely presented, surjective presentation”.

Let f : 𝒰 ⟶ 𝒳 and g : 𝒳 ⟶ 𝒴 be composable 1-morphisms of algebraic stacks and assume f is representable by algebraic spaces, surjective, flat and locally of finite presentation. For an abelian sheaf 𝓕 on the fppf site of 𝒳 there is a first-quadrant spectral sequence of abelian sheaves on the fppf site of 𝒴 E₁^{p,q} = R^q (g ∘ fₚ)_* fₚ⁻¹𝓕 ⇒ R^{p+q} g_* 𝓕, all higher direct images computed in the fppf topology, where 𝒰ₚ is the degree p term of the relative Čech nerve of f and fₚ its projection to 𝒳. The first page, the first-quadrant vanishing and the abutment are the fields of Stacks.RelativeCech.PushforwardSpectralSequenceData.

theorem exists_fppfDirectImageSpectralSequence
    (hrep : Stack.IsRepresentableByAlgebraicSpaces B S hS f.hom.hom)
    (hsurj : Stack.IsSurjective B S hS f) (hflat : IsFlat B S hS f)
    (hlfp : IsLocallyOfFinitePresentation B S hS f)
    (𝓕 : Sheaf (BigFppfOver.associatedTopology B S hS 𝒳.val.val.p SiteKind.fppf)
      AddCommGrpCat.{max (u + 1) a}) :
    Nonempty (Stacks.RelativeCech.PushforwardSpectralSequenceData B S hS 𝒳.val.val.p
      𝒴.val.val.p (CatFiberedInGroupoids.homFunctor f.hom)
      (CatFiberedInGroupoids.homFunctor g.hom) SiteKind.fppf 𝓕)

AlgebraicGeometry.Stack.AlgebraicStacks.exists_fppfModuleDirectImageSpectralSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/PresentationDirectImageSpectralSequence.lean, line 200. The attribute's comment: “part (2)(b): spectral sequence in Mod(𝒪_𝒴) along a flat, locally finitely presented, surjective presentation”.

Let f : 𝒰 ⟶ 𝒳 and g : 𝒳 ⟶ 𝒴 be composable 1-morphisms of algebraic stacks and assume f is representable by algebraic spaces, surjective, flat and locally of finite presentation. For a sheaf of 𝒪_𝒳-modules 𝓕 on the fppf site of 𝒳 there is a first-quadrant spectral sequence of sheaves of 𝒪_𝒴-modules on the fppf site of 𝒴 E₁^{p,q} = R^q (g ∘ fₚ)_* fₚ⁻¹𝓕 ⇒ R^{p+q} g_* 𝓕, all higher direct images computed in sheaves of modules for the fppf topology, where 𝒰ₚ is the degree p term of the relative Čech nerve of f and fₚ its projection to 𝒳. The first page, the first-quadrant vanishing and the abutment are the fields of Stacks.RelativeCech.ModulePushforwardSpectralSequenceData.

theorem exists_fppfModuleDirectImageSpectralSequence
    (hrep : Stack.IsRepresentableByAlgebraicSpaces B S hS f.hom.hom)
    (hsurj : Stack.IsSurjective B S hS f) (hflat : IsFlat B S hS f)
    (hlfp : IsLocallyOfFinitePresentation B S hS f)
    (𝓕 : SheafOfModules.{max (u + 1) a} (Stacks.RelativeCech.moduleRingSheaf B S hS
      𝒳.val.val.p 𝒳.val.isFiberedInGroupoids SiteKind.fppf)) :
    Nonempty (Stacks.RelativeCech.ModulePushforwardSpectralSequenceData.{u, u + 1, u + 1, u + 1,
      u, u, u, a} B S hS 𝒰.val.val.p 𝒳.val.val.p 𝒴.val.val.p
      (CatFiberedInGroupoids.homFunctor f.hom) (CatFiberedInGroupoids.homFunctor g.hom)
      SiteKind.fppf 𝒰.val.isFiberedInGroupoids 𝒳.val.isFiberedInGroupoids
      𝒴.val.isFiberedInGroupoids
      (Functor.isFibredOneMorphism_of_isFiberedInGroupoids 𝒳.val.isFiberedInGroupoids
        f.hom.hom.w)
      (Functor.isFibredOneMorphism_of_isFiberedInGroupoids 𝒴.val.isFiberedInGroupoids
        g.hom.hom.w) 𝓕)

AlgebraicGeometry.Stack.AlgebraicStacks.exists_etaleDirectImageSpectralSequenceData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/SmoothCoveringSpectralSequence.lean, line 379. The attribute's comment: “part (1)(a): the étale spectral sequence for higher direct images along a smooth surjective presentation”.

Stacks 072G, part (1)(a). Let f : 𝒰 ⟶ 𝒳 and g : 𝒳 ⟶ 𝒴 be composable 1-morphisms of algebraic stacks and assume f is representable by algebraic spaces, surjective and smooth. For an abelian sheaf 𝓕 on the étale site of 𝒳 there is a first-quadrant spectral sequence of abelian sheaves on the étale site of 𝒴 E₁^{p,q} = R^q (g ∘ fₚ)_* fₚ⁻¹𝓕 ⇒ R^{p+q} g_* 𝓕, all higher direct images computed in the étale topology, where 𝒰ₚ is the degree p term of the relative Čech nerve of f, that is the (p+1)-fold fibre product of 𝒰 over 𝒳, and fₚ its projection to 𝒳.

theorem exists_etaleDirectImageSpectralSequenceData
    (𝓕 : Sheaf (BigFppfOver.associatedTopology B S hS 𝒳.val.val.p SiteKind.etale)
      AddCommGrpCat.{max (u + 1) a}) :
    Nonempty (Stacks.RelativeCech.PushforwardSpectralSequenceData B S hS 𝒳.val.val.p
      𝒴.val.val.p (CatFiberedInGroupoids.homFunctor f.hom)
      (CatFiberedInGroupoids.homFunctor g.hom) SiteKind.etale 𝓕)

AlgebraicGeometry.Stack.AlgebraicStacks.exists_fppfDirectImageSpectralSequenceData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/SmoothCoveringSpectralSequence.lean, line 423. The attribute's comment: “part (2)(a): the fppf spectral sequence for higher direct images along a flat surjective presentation”.

Stacks 072G, part (2)(a). Let f : 𝒰 ⟶ 𝒳 and g : 𝒳 ⟶ 𝒴 be composable 1-morphisms of algebraic stacks and assume f is representable by algebraic spaces, surjective, flat and locally of finite presentation. For an abelian sheaf 𝓕 on the fppf site of 𝒳 there is a first-quadrant spectral sequence of abelian sheaves on the fppf site of 𝒴 E₁^{p,q} = R^q (g ∘ fₚ)_* fₚ⁻¹𝓕 ⇒ R^{p+q} g_* 𝓕, all higher direct images computed in the fppf topology, where 𝒰ₚ is the degree p term of the relative Čech nerve of f, that is the (p+1)-fold fibre product of 𝒰 over 𝒳, and fₚ its projection to 𝒳.

theorem exists_fppfDirectImageSpectralSequenceData
    (𝓕 : Sheaf (BigFppfOver.associatedTopology B S hS 𝒳.val.val.p SiteKind.fppf)
      AddCommGrpCat.{max (u + 1) a}) :
    Nonempty (Stacks.RelativeCech.PushforwardSpectralSequenceData B S hS 𝒳.val.val.p
      𝒴.val.val.p (CatFiberedInGroupoids.homFunctor f.hom)
      (CatFiberedInGroupoids.homFunctor g.hom) SiteKind.fppf 𝓕)

Tag 075G, a lemma

Tag 075G in the Stacks Project.

AlgebraicGeometry.Stack.derivedDirectImageIsoSheafifyDerivedPresheafDirectImage, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/HigherDirectImage.lean, line 104. The attribute's comment: “abelian sheafification formula”.

Stacks 075G. Higher direct image of abelian sheaves is the sheafification of the derived presheaf direct image.

noncomputable def derivedDirectImageIsoSheafifyDerivedPresheafDirectImage
    [p.IsFibered] [q.IsFibered] (hF : p.IsFibredOneMorphism q F) (n : ℕ)
    [∀ G : 𝒳ᵒᵖ ⥤ AddCommGrpCat.{a}, F.op.HasPointwiseRightKanExtension G]
    [HasSheafify (associatedTopology B S hS p τ) AddCommGrpCat.{a}]
    [HasSheafify (associatedTopology B S hS q τ) AddCommGrpCat.{a}]
    [HasInjectiveResolutions (Sheaf (associatedTopology B S hS p τ) AddCommGrpCat.{a})] :
    letI := (hF.isContinuous_and_isCocontinuous_inheritedTopology (τ.over (B.obj hS))).2
    letI := additive_sheafPushforwardCocontinuous B S hS p q F τ hF
    (F.sheafPushforwardCocontinuous AddCommGrpCat.{a}
        (associatedTopology B S hS p τ) (associatedTopology B S hS q τ)).rightDerived n ≅
      derivedPresheafDirectImage B S hS p F τ n ⋙
        presheafToSheaf (associatedTopology B S hS q τ) AddCommGrpCat.{a}

AlgebraicGeometry.Stack.higherDirectImageIsoSheafifyFibreCohomology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/HigherDirectImageFibreCohomology.lean, line 348. The attribute's comment: “abelian sheaves: R^n f_* F is the sheafification of y ↦ H^n((Sch/V) ×_{y,Y} X, pr^{-1} F)”. References: SGA 4 V (5.1), “clause 1”.

Stacks 075G, abelian sheaves. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S and τ one of the Zariski, étale, smooth, syntomic and fppf topologies. For an abelian sheaf ℱ on 𝒳_τ, the higher direct image Rⁿf_*ℱ is the sheaf associated to the presheaf y ↦ H^n_τ((Sch/V)_{fppf} ×_{y, 𝒴} 𝒳, pr⁻¹ℱ), y an object of 𝒴 lying over the scheme V.

The direct image is right Kan extension followed by sheafification, and sheafification is exact (abelianHigherDirectImage_iso_sheafify_fibreCohomology); the derived presheaf direct image is computed objectwise (CategoryTheory.Functor.rightDerivedFlipObjIso), and its value at y is the cohomology of the 2-fibre product by Stacks 06W6 and Stacks 06X1 (derivedPresheafDirectImageEvaluationIso).

def higherDirectImageIsoSheafifyFibreCohomology (n : ℕ)
    (F : Sheaf JX AddCommGrpCat.{max (u + 1) a}) :
    (((g).sheafPushforwardCocontinuous AddCommGrpCat.{max (u + 1) a} JX JY).rightDerived n).obj F ≅
      (presheafToSheaf JY AddCommGrpCat.{max (u + 1) a}).obj
        (objectFibreCohomologyPresheaf.{u, w, a} B S hS f c τ n F)

AlgebraicGeometry.Stack.moduleHigherDirectImageIsoSheafifyFibreModuleCohomology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/HigherDirectImageFibreCohomologyScalars.lean, line 350. The attribute's comment: “sheaves of modules: R^n f_* F is, as an O_Y-module, the sheafification of the presheaf of O_Y-modules y ↦ H^n((Sch/V) ×_{y,Y} X, pr^{-1} F)”.

Stacks 075G, sheaves of modules. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S and τ one of the Zariski, étale, smooth, syntomic and fppf topologies. For a sheaf ℱ of 𝒪_𝒳-modules on 𝒳_τ, the higher direct image Rⁿf_*ℱ is, as a sheaf of 𝒪_𝒴-modules, the sheaf associated to the presheaf of 𝒪_𝒴-modules y ↦ H^n_τ((Sch/V)_{fppf} ×_{y, 𝒴} 𝒳, pr⁻¹ℱ), y an object of 𝒴 lying over the scheme V, the cohomology of the sheaf of modules pr⁻¹ℱ being an 𝒪_𝒴(y)-module through the pullback of functions 𝒪_𝒴(y) ⟶ Γ(…, 𝒪).

The direct image is the presheaf direct image followed by sheafification, which is exact (moduleHigherDirectImageIsoSheafify); evaluation at y is exact, and the sections over y of the presheaf direct image are the global sections over the 2-fibre product as 𝒪_𝒴(y)-modules (modulePresheafDirectImageEvaluationLinearIso, Stacks 06W6), whose derived functors are the cohomology of the 2-fibre product because pr⁻¹ preserves injectives (Stacks 06X2).

def moduleHigherDirectImageIsoSheafifyFibreModuleCohomology (n : ℕ)
    (F : SheafOfModules.{max (u + 1) a} OX) :
    ((moduleSheafPushforward.{u, u + 1, u, a, u + 1, u} B S hS 𝒳.val.val.p 𝒴.val.val.p
        𝒳.val.isFiberedInGroupoids 𝒴.val.isFiberedInGroupoids g
        (CatFiberedInGroupoids.homFunctor_comp_p f.hom) (B.baseTopology τ)
        (B.baseTopology_le_topology τ)).rightDerived n).obj F ≅
      (PresheafOfModules.sheafification.{max (u + 1) a} (𝟙 (OY).obj)).obj
        (objectFibreModuleCohomologyPresheafOfModules.{u, w, a} B S hS f c τ n F)

Tag 075H, a lemma

Tag 075H in the Stacks Project.

AlgebraicGeometry.Stack.abelianDirectImageBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/HigherDirectImageBaseChange.lean, line 358. The attribute's comment: “degree zero, abelian sheaves: g⁻¹f_ℱ ≅ f'_(g')⁻¹ℱ”.

Stacks 075H in degree zero. For the canonical 2-cartesian square of categories fibred in groupoids over the big fppf category of S and any topology τ on B.Schemes, the base-change map g⁻¹f_*ℱ ⟶ f'_*(g')⁻¹ℱ of abelian sheaves on the associated sites is an isomorphism, naturally in ℱ.

This is the identification the source quotes from Stacks 075B at the start of the proof of Stacks 075H. Both composites become, on underlying presheaves, the two ways round the square of a right Kan extension and a restriction (Stacks 06NW), where they are identified by AlgebraicGeometry.Stack.abelianPresheafBaseChangeIso; the descent to sheaves is full faithfulness of sheafToPresheaf.

noncomputable def abelianDirectImageBaseChangeIso
    [p𝒳.IsFibered] [p𝒴'.IsFibered] [p𝒴.IsFibered]
    (h𝒳 : p𝒳.IsFiberedInGroupoids) (h𝒴' : p𝒴'.IsFiberedInGroupoids)
    (h𝒴 : p𝒴.IsFiberedInGroupoids) (hfc : f ⋙ p𝒴 = p𝒳) (hgc : g ⋙ p𝒴 = p𝒴')
    [∀ G : 𝒳ᵒᵖ ⥤ AddCommGrpCat.{a}, f.op.HasPointwiseRightKanExtension G]
    [∀ G : (TwoFibreProductOver p𝒳 p𝒴' p𝒴 f g)ᵒᵖ ⥤ AddCommGrpCat.{a},
      (TwoFibreProductOver.snd p𝒳 p𝒴' p𝒴 f g).op.HasPointwiseRightKanExtension G] :
    letI : (TwoFibreProductOver.structureFunctor p𝒳 p𝒴' p𝒴 f g).IsFibered :=
      isFibered_twoFibreProductStructureFunctor p𝒳 p𝒴' p𝒴 f g h𝒳 h𝒴' h𝒴 hfc hgc
    letI := isCocontinuous_of_isFiberedInGroupoids B S hS p𝒳 p𝒴 f τ h𝒴 hfc
    letI := isContinuous_of_isFiberedInGroupoids B S hS p𝒴' p𝒴 g τ h𝒴 hgc
    letI := isContinuous_of_isFiberedInGroupoids B S hS
      (TwoFibreProductOver.structureFunctor p𝒳 p𝒴' p𝒴 f g) p𝒳
      (TwoFibreProductOver.fst p𝒳 p𝒴' p𝒴 f g) τ h𝒳 TwoFibreProductOver.fst_comp_eq
    letI := isCocontinuous_of_isFiberedInGroupoids B S hS
      (TwoFibreProductOver.structureFunctor p𝒳 p𝒴' p𝒴 f g) p𝒴'
      (TwoFibreProductOver.snd p𝒳 p𝒴' p𝒴 f g) τ h𝒴' TwoFibreProductOver.snd_comp_eq
    f.sheafPushforwardCocontinuous AddCommGrpCat.{a}
          (associatedTopology B S hS p𝒳 τ) (associatedTopology B S hS p𝒴 τ) ⋙
        g.sheafPushforwardContinuous AddCommGrpCat.{a}
          (associatedTopology B S hS p𝒴' τ) (associatedTopology B S hS p𝒴 τ) ≅
      (TwoFibreProductOver.fst p𝒳 p𝒴' p𝒴 f g).sheafPushforwardContinuous AddCommGrpCat.{a}
          (associatedTopology B S hS
            (TwoFibreProductOver.structureFunctor p𝒳 p𝒴' p𝒴 f g) τ)
          (associatedTopology B S hS p𝒳 τ) ⋙
        (TwoFibreProductOver.snd p𝒳 p𝒴' p𝒴 f g).sheafPushforwardCocontinuous
          AddCommGrpCat.{a}
          (associatedTopology B S hS
            (TwoFibreProductOver.structureFunctor p𝒳 p𝒴' p𝒴 f g) τ)
          (associatedTopology B S hS p𝒴' τ)

AlgebraicGeometry.Stack.abelianHigherDirectImageBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/HigherDirectImageBaseChange.lean, line 438. The attribute's comment: “all degrees, abelian sheaves; Rⁱf'_(g')⁻¹ as the right derived functor of the composite f'_ ∘ (g')⁻¹”.

Stacks 075H in every degree. For the canonical 2-cartesian square of categories fibred in groupoids over the big fppf category of S and any topology τ on B.Schemes, the base-change map is an isomorphism g⁻¹Rⁱf_*ℱ ≅ Rⁱ(f'_*(g')⁻¹)ℱ of abelian sheaves on the associated site of 𝒴', naturally in ℱ.

The right-hand side is the i-th right derived functor of the composite f'_* ∘ (g')⁻¹. The source writes instead Rⁱf'_*((g')⁻¹ℱ), the i-th right derived functor of f'_* evaluated at (g')⁻¹ℱ; the two differ by whether (g')⁻¹ sends injective abelian sheaves to f'_*-acyclic ones, which is not available here. See the implementation notes of this file.

The proof uses nothing beyond the degree-zero isomorphism AlgebraicGeometry.Stack.abelianDirectImageBaseChangeIso and exactness of g⁻¹ (Stacks 06NW): an exact functor may be pulled out of a right derived functor, so (f_* ⋙ g⁻¹).rightDerived i ≅ (f_*).rightDerived i ⋙ g⁻¹, and the degree-zero isomorphism rewrites the left-hand side.

noncomputable def abelianHigherDirectImageBaseChangeIso
    [p𝒳.IsFibered] [p𝒴'.IsFibered] [p𝒴.IsFibered]
    (h𝒳 : p𝒳.IsFiberedInGroupoids) (h𝒴' : p𝒴'.IsFiberedInGroupoids)
    (h𝒴 : p𝒴.IsFiberedInGroupoids) (hfc : f ⋙ p𝒴 = p𝒳) (hgc : g ⋙ p𝒴 = p𝒴') (n : ℕ)
    [∀ G : 𝒳ᵒᵖ ⥤ AddCommGrpCat.{a}, f.op.HasPointwiseRightKanExtension G]
    [∀ G : 𝒴'ᵒᵖ ⥤ AddCommGrpCat.{a}, g.op.HasPointwiseRightKanExtension G]
    [∀ G : (TwoFibreProductOver p𝒳 p𝒴' p𝒴 f g)ᵒᵖ ⥤ AddCommGrpCat.{a},
      (TwoFibreProductOver.snd p𝒳 p𝒴' p𝒴 f g).op.HasPointwiseRightKanExtension G]
    [HasSheafify (associatedTopology B S hS p𝒳 τ) AddCommGrpCat.{a}]
    [HasSheafify (associatedTopology B S hS p𝒴' τ) AddCommGrpCat.{a}]
    [HasSheafify (associatedTopology B S hS p𝒴 τ) AddCommGrpCat.{a}]
    [HasSheafify (associatedTopology B S hS
      (TwoFibreProductOver.structureFunctor p𝒳 p𝒴' p𝒴 f g) τ) AddCommGrpCat.{a}]
    [HasInjectiveResolutions
      (Sheaf (associatedTopology B S hS p𝒳 τ) AddCommGrpCat.{a})] :
    letI : (TwoFibreProductOver.structureFunctor p𝒳 p𝒴' p𝒴 f g).IsFibered :=
      isFibered_twoFibreProductStructureFunctor p𝒳 p𝒴' p𝒴 f g h𝒳 h𝒴' h𝒴 hfc hgc
    letI := isCocontinuous_of_isFiberedInGroupoids B S hS p𝒳 p𝒴 f τ h𝒴 hfc
    letI := isContinuous_of_isFiberedInGroupoids B S hS p𝒴' p𝒴 g τ h𝒴 hgc
    letI := isContinuous_of_isFiberedInGroupoids B S hS
      (TwoFibreProductOver.structureFunctor p𝒳 p𝒴' p𝒴 f g) p𝒳
      (TwoFibreProductOver.fst p𝒳 p𝒴' p𝒴 f g) τ h𝒳 TwoFibreProductOver.fst_comp_eq
    letI := isCocontinuous_of_isFiberedInGroupoids B S hS
      (TwoFibreProductOver.structureFunctor p𝒳 p𝒴' p𝒴 f g) p𝒴'
      (TwoFibreProductOver.snd p𝒳 p𝒴' p𝒴 f g) τ h𝒴' TwoFibreProductOver.snd_comp_eq
    letI : (f.sheafPushforwardCocontinuous AddCommGrpCat.{a}
        (associatedTopology B S hS p𝒳 τ) (associatedTopology B S hS p𝒴 τ)).Additive :=
      additive_sheafPushforwardCocontinuous B S hS p𝒳 p𝒴 f τ (h𝒴.isFibredOneMorphism hfc)
    letI : ((TwoFibreProductOver.fst p𝒳 p𝒴' p𝒴 f g).sheafPushforwardContinuous
        AddCommGrpCat.{a}
        (associatedTopology B S hS
          (TwoFibreProductOver.structureFunctor p𝒳 p𝒴' p𝒴 f g) τ)
        (associatedTopology B S hS p𝒳 τ)).Additive :=
      additive_sheafPushforwardContinuous B S hS
        (TwoFibreProductOver.structureFunctor p𝒳 p𝒴' p𝒴 f g) p𝒳
        (TwoFibreProductOver.fst p𝒳 p𝒴' p𝒴 f g) τ
        (h𝒳.isFibredOneMorphism TwoFibreProductOver.fst_comp_eq)
    letI : ((TwoFibreProductOver.snd p𝒳 p𝒴' p𝒴 f g).sheafPushforwardCocontinuous
        AddCommGrpCat.{a}
        (associatedTopology B S hS
          (TwoFibreProductOver.structureFunctor p𝒳 p𝒴' p𝒴 f g) τ)
        (associatedTopology B S hS p𝒴' τ)).Additive :=
      additive_sheafPushforwardCocontinuous B S hS
        (TwoFibreProductOver.structureFunctor p𝒳 p𝒴' p𝒴 f g) p𝒴'
        (TwoFibreProductOver.snd p𝒳 p𝒴' p𝒴 f g) τ
        (h𝒴'.isFibredOneMorphism TwoFibreProductOver.snd_comp_eq)
    (f.sheafPushforwardCocontinuous AddCommGrpCat.{a}
            (associatedTopology B S hS p𝒳 τ)
            (associatedTopology B S hS p𝒴 τ)).rightDerived n ⋙
        g.sheafPushforwardContinuous AddCommGrpCat.{a}
          (associatedTopology B S hS p𝒴' τ) (associatedTopology B S hS p𝒴 τ) ≅
      ((TwoFibreProductOver.fst p𝒳 p𝒴' p𝒴 f g).sheafPushforwardContinuous AddCommGrpCat.{a}
            (associatedTopology B S hS
              (TwoFibreProductOver.structureFunctor p𝒳 p𝒴' p𝒴 f g) τ)
            (associatedTopology B S hS p𝒳 τ) ⋙
          (TwoFibreProductOver.snd p𝒳 p𝒴' p𝒴 f g).sheafPushforwardCocontinuous
            AddCommGrpCat.{a}
            (associatedTopology B S hS
              (TwoFibreProductOver.structureFunctor p𝒳 p𝒴' p𝒴 f g) τ)
            (associatedTopology B S hS p𝒴' τ)).rightDerived n

AlgebraicGeometry.Stack.AlgebraicStacks.abelianHigherDirectImageBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/HigherDirectImageBaseChangeAlgebraicStacks.lean, line 938. The attribute's comment: “abelian sheaves: g⁻¹Rⁱf_F ≅ Rⁱf'_((g')⁻¹F) for every i, naturally in F”.

Stacks 075H for abelian sheaves. Let f : 𝒳 ⟶ 𝒴 and g : 𝒴' ⟶ 𝒴 be 1-morphisms of algebraic stacks over S, with 2-cartesian square
𝒴' ×_𝒴 𝒳 --- g' ---> 𝒳
   |                 |
   f'                f
   v                 v
  𝒴' ------ g -----> 𝒴
For every topology τ on the schemes of the big fppf site, the base change map is an isomorphism g⁻¹Rⁱf_*ℱ ≅ Rⁱf'_*((g')⁻¹ℱ) of abelian sheaves on 𝒴'_τ, functorially in the abelian sheaf ℱ on 𝒳_τ, for every i.

noncomputable def abelianHigherDirectImageBaseChangeIso {𝒳 𝒴 𝒴' : AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴' ⟶ 𝒴) (τ : GrothendieckTopology B.Schemes) (n : ℕ) :
    letI : (TwoFibreProductOver.structureFunctor 𝒳.val.val.p 𝒴'.val.val.p 𝒴.val.val.p
        (CatFiberedInGroupoids.homFunctor f.hom)
        (CatFiberedInGroupoids.homFunctor g.hom)).IsFibered :=
      isFibered_twoFibreProductStructureFunctor _ _ _ _ _ 𝒳.val.property 𝒴'.val.property
        𝒴.val.property (CatFiberedInGroupoids.homFunctor_comp_p f.hom)
        (CatFiberedInGroupoids.homFunctor_comp_p g.hom)
    letI : 𝒳.val.val.p.IsFibered := 𝒳.val.property.isFibered
    letI : 𝒴'.val.val.p.IsFibered := 𝒴'.val.property.isFibered
    letI : 𝒴.val.val.p.IsFibered := 𝒴.val.property.isFibered
    letI := isCocontinuous_of_isFiberedInGroupoids B S hS _ _
      (CatFiberedInGroupoids.homFunctor f.hom) τ 𝒴.val.property
      (CatFiberedInGroupoids.homFunctor_comp_p f.hom)
    letI := isContinuous_of_isFiberedInGroupoids B S hS _ _
      (CatFiberedInGroupoids.homFunctor g.hom) τ 𝒴.val.property
      (CatFiberedInGroupoids.homFunctor_comp_p g.hom)
    letI := isContinuous_of_isFiberedInGroupoids B S hS _ _
      (TwoFibreProductOver.fst 𝒳.val.val.p 𝒴'.val.val.p 𝒴.val.val.p
        (CatFiberedInGroupoids.homFunctor f.hom) (CatFiberedInGroupoids.homFunctor g.hom))
      τ 𝒳.val.property TwoFibreProductOver.fst_comp_eq
    letI := isCocontinuous_of_isFiberedInGroupoids B S hS _ _
      (TwoFibreProductOver.snd 𝒳.val.val.p 𝒴'.val.val.p 𝒴.val.val.p
        (CatFiberedInGroupoids.homFunctor f.hom) (CatFiberedInGroupoids.homFunctor g.hom))
      τ 𝒴'.val.property TwoFibreProductOver.snd_comp_eq
    letI : ((CatFiberedInGroupoids.homFunctor f.hom).sheafPushforwardCocontinuous
        AddCommGrpCat.{max (u + 1) a}
        (associatedTopology B S hS 𝒳.val.val.p τ)
        (associatedTopology B S hS 𝒴.val.val.p τ)).Additive :=
      additive_sheafPushforwardCocontinuous B S hS _ _ _ τ
        (𝒴.val.property.isFibredOneMorphism (CatFiberedInGroupoids.homFunctor_comp_p f.hom))
    letI : ((TwoFibreProductOver.snd 𝒳.val.val.p 𝒴'.val.val.p 𝒴.val.val.p
        (CatFiberedInGroupoids.homFunctor f.hom)
        (CatFiberedInGroupoids.homFunctor g.hom)).sheafPushforwardCocontinuous
        AddCommGrpCat.{max (u + 1) a}
        (associatedTopology B S hS (TwoFibreProductOver.structureFunctor 𝒳.val.val.p
          𝒴'.val.val.p 𝒴.val.val.p (CatFiberedInGroupoids.homFunctor f.hom)
          (CatFiberedInGroupoids.homFunctor g.hom)) τ)
        (associatedTopology B S hS 𝒴'.val.val.p τ)).Additive :=
      additive_sheafPushforwardCocontinuous B S hS _ _ _ τ
        (𝒴'.val.property.isFibredOneMorphism TwoFibreProductOver.snd_comp_eq)
    ((CatFiberedInGroupoids.homFunctor f.hom).sheafPushforwardCocontinuous
          AddCommGrpCat.{max (u + 1) a}
          (associatedTopology B S hS 𝒳.val.val.p τ)
          (associatedTopology B S hS 𝒴.val.val.p τ)).rightDerived n ⋙
        (CatFiberedInGroupoids.homFunctor g.hom).sheafPushforwardContinuous
          AddCommGrpCat.{max (u + 1) a}
          (associatedTopology B S hS 𝒴'.val.val.p τ)
          (associatedTopology B S hS 𝒴.val.val.p τ) ≅
      (TwoFibreProductOver.fst 𝒳.val.val.p 𝒴'.val.val.p 𝒴.val.val.p
          (CatFiberedInGroupoids.homFunctor f.hom)
          (CatFiberedInGroupoids.homFunctor g.hom)).sheafPushforwardContinuous
          AddCommGrpCat.{max (u + 1) a}
          (associatedTopology B S hS (TwoFibreProductOver.structureFunctor 𝒳.val.val.p
            𝒴'.val.val.p 𝒴.val.val.p (CatFiberedInGroupoids.homFunctor f.hom)
            (CatFiberedInGroupoids.homFunctor g.hom)) τ)
          (associatedTopology B S hS 𝒳.val.val.p τ) ⋙
        ((TwoFibreProductOver.snd 𝒳.val.val.p 𝒴'.val.val.p 𝒴.val.val.p
            (CatFiberedInGroupoids.homFunctor f.hom)
            (CatFiberedInGroupoids.homFunctor g.hom)).sheafPushforwardCocontinuous
            AddCommGrpCat.{max (u + 1) a}
            (associatedTopology B S hS (TwoFibreProductOver.structureFunctor 𝒳.val.val.p
              𝒴'.val.val.p 𝒴.val.val.p (CatFiberedInGroupoids.homFunctor f.hom)
              (CatFiberedInGroupoids.homFunctor g.hom)) τ)
            (associatedTopology B S hS 𝒴'.val.val.p τ)).rightDerived n

AlgebraicGeometry.Stack.AlgebraicStacks.moduleHigherDirectImageBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/HigherDirectImageBaseChangeAlgebraicStacks.lean, line 1018. The attribute's comment: “sheaves of modules: g⁻¹Rⁱf_F ≅ Rⁱf'_((g')⁻¹F) in Mod(O) for every i, naturally in F”.

Stacks 075H for sheaves of modules. For 1-morphisms f : 𝒳 ⟶ 𝒴 and g : 𝒴' ⟶ 𝒴 of algebraic stacks over S with 2-cartesian square 𝒴' ×_𝒴 𝒳 as in AlgebraicStacks.abelianHigherDirectImageBaseChangeIso, and every topology τ coarser than the fppf topology, the base change map is an isomorphism g^*Rⁱf_*ℱ ≅ Rⁱf'_*((g')^*ℱ) of sheaves of 𝒪_{𝒴'}-modules, functorially in the sheaf of 𝒪_𝒳-modules ℱ, for every i; the higher direct images are the right derived functors on sheaves of modules.

noncomputable def moduleHigherDirectImageBaseChangeIso {𝒳 𝒴 𝒴' : AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴' ⟶ 𝒴) (τ : GrothendieckTopology B.Schemes) (hτ : τ ≤ B.topology)
    (n : ℕ) :
    (moduleSheafPushforward.{u, u + 1, u, max (u + 1) a} B S hS 𝒳.val.val.p 𝒴.val.val.p
          𝒳.val.property 𝒴.val.property (CatFiberedInGroupoids.homFunctor f.hom)
          (CatFiberedInGroupoids.homFunctor_comp_p f.hom) τ hτ).rightDerived n ⋙
        modulePullback B S hS 𝒴'.val.val.p 𝒴.val.val.p 𝒴'.val.property 𝒴.val.property
          (CatFiberedInGroupoids.homFunctor g.hom)
          (CatFiberedInGroupoids.homFunctor_comp_p g.hom) τ hτ ≅
      modulePullback B S hS (TwoFibreProductOver.structureFunctor 𝒳.val.val.p 𝒴'.val.val.p
          𝒴.val.val.p (CatFiberedInGroupoids.homFunctor f.hom)
          (CatFiberedInGroupoids.homFunctor g.hom)) 𝒳.val.val.p
          (TwoFibreProductOver.isFiberedInGroupoids _ _ _ _ _ 𝒳.val.property 𝒴'.val.property
            𝒴.val.property (CatFiberedInGroupoids.homFunctor_comp_p f.hom)
            (CatFiberedInGroupoids.homFunctor_comp_p g.hom)) 𝒳.val.property
          (TwoFibreProductOver.fst 𝒳.val.val.p 𝒴'.val.val.p 𝒴.val.val.p
            (CatFiberedInGroupoids.homFunctor f.hom) (CatFiberedInGroupoids.homFunctor g.hom))
          TwoFibreProductOver.fst_comp_eq τ hτ ⋙
        (moduleSheafPushforward.{u, u + 1, u, max (u + 1) a} B S hS
          (TwoFibreProductOver.structureFunctor 𝒳.val.val.p 𝒴'.val.val.p 𝒴.val.val.p
            (CatFiberedInGroupoids.homFunctor f.hom) (CatFiberedInGroupoids.homFunctor g.hom))
          𝒴'.val.val.p
          (TwoFibreProductOver.isFiberedInGroupoids _ _ _ _ _ 𝒳.val.property 𝒴'.val.property
            𝒴.val.property (CatFiberedInGroupoids.homFunctor_comp_p f.hom)
            (CatFiberedInGroupoids.homFunctor_comp_p g.hom)) 𝒴'.val.property
          (TwoFibreProductOver.snd 𝒳.val.val.p 𝒴'.val.val.p 𝒴.val.val.p
            (CatFiberedInGroupoids.homFunctor f.hom) (CatFiberedInGroupoids.homFunctor g.hom))
          TwoFibreProductOver.snd_comp_eq τ hτ).rightDerived n

AlgebraicGeometry.Stack.AlgebraicStacks.isIso_abelianDerivedDirectImageBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/HigherDirectImageBaseChangeMap.lean, line 640. The attribute's comment: “abelian sheaves: the base change map g⁻¹Rf_F ⟶ Rf'_(g')⁻¹F is an isomorphism, functorially in F in D⁺(Ab(𝒳_τ))”.

Stacks 075H for abelian sheaves. Let f : 𝒳 ⟶ 𝒴 and g : 𝒴' ⟶ 𝒴 be 1-morphisms of algebraic stacks over S, with 2-cartesian square
𝒴' ×_𝒴 𝒳 --- g' ---> 𝒳
   |                 |
   f'                f
   v                 v
  𝒴' ------ g -----> 𝒴
For every topology τ on the schemes of the big fppf site, the base change map g⁻¹Rf_*ℱ ⟶ Rf'_*(g')⁻¹ℱ (AlgebraicGeometry.Stack.abelianDerivedDirectImageBaseChange, the map of Stacks 0736 built from the adjunctions f⁻¹ ⊣ f_*, f'⁻¹ ⊣ f'_* and the 2-commutativity of the square) is an isomorphism, functorially in ℱ in the bounded below derived category of abelian sheaves on 𝒳_τ; in particular for ℱ an abelian sheaf, placed in degree zero.

theorem isIso_abelianDerivedDirectImageBaseChange {𝒳 𝒴 𝒴' : AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴' ⟶ 𝒴) (τ : GrothendieckTopology B.Schemes) :
    IsIso (abelianDerivedDirectImageBaseChange.{u, a} B S hS _ _ _
      (CatFiberedInGroupoids.homFunctor f.hom) (CatFiberedInGroupoids.homFunctor g.hom) τ
      𝒳.val.property 𝒴'.val.property 𝒴.val.property
      (CatFiberedInGroupoids.homFunctor_comp_p f.hom)
      (CatFiberedInGroupoids.homFunctor_comp_p g.hom))

AlgebraicGeometry.Stack.AlgebraicStacks.isIso_moduleDerivedDirectImageBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/HigherDirectImageBaseChangeMap.lean, line 663. The attribute's comment: “sheaves of modules: the base change map g⁻¹Rf_F ⟶ Rf'_(g')⁻¹F is an isomorphism, functorially in F in D⁺(Mod(𝒳_τ, O_𝒳))”.

Stacks 075H for sheaves of modules. For 1-morphisms f : 𝒳 ⟶ 𝒴 and g : 𝒴' ⟶ 𝒴 of algebraic stacks over S with 2-cartesian square 𝒴' ×_𝒴 𝒳 as in AlgebraicGeometry.Stack.AlgebraicStacks.isIso_abelianDerivedDirectImageBaseChange, and every topology τ coarser than the fppf topology, the base change map g^*Rf_*ℱ ⟶ Rf'_*(g')^*ℱ (AlgebraicGeometry.Stack.moduleDerivedDirectImageBaseChange) is an isomorphism, functorially in ℱ in the bounded below derived category of sheaves of 𝒪_𝒳-modules on 𝒳_τ; in particular for ℱ a sheaf of 𝒪_𝒳-modules, placed in degree zero.

theorem isIso_moduleDerivedDirectImageBaseChange {𝒳 𝒴 𝒴' : AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴' ⟶ 𝒴) (τ : GrothendieckTopology B.Schemes) (hτ : τ ≤ B.topology) :
    IsIso (moduleDerivedDirectImageBaseChange.{u, a} B S hS _ _ _
      (CatFiberedInGroupoids.homFunctor f.hom) (CatFiberedInGroupoids.homFunctor g.hom) τ hτ
      𝒳.val.property 𝒴'.val.property 𝒴.val.property
      (CatFiberedInGroupoids.homFunctor_comp_p f.hom)
      (CatFiberedInGroupoids.homFunctor_comp_p g.hom))

Sources

Section96.22 Comparison #

Section 96.22 of the Stacks Project, Tag 073L. 3 tags here are carried by 7 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 075L, a lemma

Tag 075L in the Stacks Project.

AlgebraicGeometry.Space.injective_restrictionAbSheafFunctor_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RestrictionToAlgebraicSpaceInjectives.lean, line 204. The attribute's comment: “part (1), injective abelian sheaves”.

Stacks Project, Tag 075L, part (1). Let 𝒳 be a category fibred in groupoids over the big fppf site of S representable by the algebraic space F. If I is injective in Ab(𝒳_étale), then I|_{F_étale} is injective in Ab(F_étale).

theorem injective_restrictionAbSheafFunctor_obj (hp : p.IsFiberedInGroupoids)
    (e : StacksRepresentableCFG.EquivalenceOver p
      (presheafOfCategories (F ⋙ typeToCat)).p)
    [HasSheafify (BigFppfOver.associatedTopology B S hS p .etale) Ab.{t}]
    [HasSheafify (SmallEtale.topology B S hS F) Ab.{t}]
    [∀ G : (SmallEtale B S hS F)ᵒᵖ ⥤ Ab.{t},
      (restrictionFunctor B S hS F p e).op.HasPointwiseLeftKanExtension G]
    (I : Sheaf (BigFppfOver.associatedTopology B S hS p .etale) Ab.{t}) [Injective I] :
    Injective ((restrictionAbSheafFunctor B S hS F p hp e).obj I)

AlgebraicGeometry.Space.isKInjective_restrictionAbSheafFunctor_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RestrictionToAlgebraicSpaceInjectives.lean, line 222. The attribute's comment: “part (2), K-injective complexes”.

Stacks Project, Tag 075L, part (2). Let 𝒳 be a category fibred in groupoids over the big fppf site of S representable by the algebraic space F. If I is a K-injective complex in Ab(𝒳_étale), then I|_{F_étale} is a K-injective complex in Ab(F_étale).

theorem isKInjective_restrictionAbSheafFunctor_obj (hp : p.IsFiberedInGroupoids)
    (e : StacksRepresentableCFG.EquivalenceOver p
      (presheafOfCategories (F ⋙ typeToCat)).p)
    [HasSheafify (BigFppfOver.associatedTopology B S hS p .etale) Ab.{t}]
    [HasSheafify (SmallEtale.topology B S hS F) Ab.{t}]
    [∀ G : (SmallEtale B S hS F)ᵒᵖ ⥤ Ab.{t},
      (restrictionFunctor B S hS F p e).op.HasPointwiseLeftKanExtension G]
    (I : CochainComplex
      (Sheaf (BigFppfOver.associatedTopology B S hS p .etale) Ab.{t}) ℤ) [I.IsKInjective] :
    CochainComplex.IsKInjective
      (((restrictionAbSheafFunctor B S hS F p hp e).mapHomologicalComplex
        (ComplexShape.up ℤ)).obj I)

Tag 075N, a lemma

Tag 075N in the Stacks Project.

AlgebraicGeometry.Space.restrictedDerivedDirectImageIsoClauses, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/RestrictionDerivedDirectImageAbelian.lean, line 1006. The attribute's comment: “BOTH clauses. (1) for ABELIAN sheaves, (Rf_F)|_{G_etale} = Rf_{small,}(F|_{F_etale}) in D(G_etale), which is AlgebraicGeometry.Space.restrictedAbelianDerivedDirectImageIso; (2) for sheaves of MODULES, the same identity in D(O_G), which is AlgebraicGeometry.Space.restrictedDerivedDirectImageIso. In both, the two restriction functors appear UNDERIVED as in the source, being their own right derived functors because they are exact, and the isomorphism is the canonical comparison of the two derived composites around the square of Tag 073N. The morphism f : F -> G of algebraic spaces is INDUCED, as the source has it -- it says: denote f : F -> G the induced morphism of algebraic spaces -- and is therefore no parameter of this statement: the derived direct images of the small sites, their units and the square of Tag 073N are all stated at AlgebraicGeometry.Space.inducedAlgebraicSpacesHom, which Tag 04SW characterises (eq_inducedSpacesHom_iff_forall_sectionOfObj, morphismSpaceEquiv_eq_inducedSpaceMap). So the hypotheses here are the source's: S, the 1-morphism, the two presentations, and the complex, together with the right derived direct images whose existence each display presupposes. Every mathematical input is a theorem of this development. Tag 073N, the 2-isomorphism of the two legs of the square, is AlgebraicGeometry.Space.restrictionRingedSquareInducedAlgebraicSpaces, assembled from invertibility of the comparison map of equation 075M (AlgebraicGeometry.Space.isIso_restrictedDirectImageComparison, settled chartwise: the pushforward formula of Tag 06W6 and the chart correspondence of Tag 03G8 give injectivity, and gluing a compatible family over the chart diagrams against Properties of Spaces 03H7 gives surjectivity) together with its structure-sheaf compatibility (AlgebraicGeometry.Space.restrictedDirectImageComparison_structureSheafCompatible, whose verticality input is AlgebraicGeometry.Space.isHomLift_schemeChartPostcompIso_hom_app). Exactness of the two restriction functors, the source's own stated reason for the closing step, is AlgebraicGeometry.Space.exactFunctor_pushforwardModules_projectionRingedToposHom for modules and AlgebraicGeometry.Space.exactFunctor_abelianRestrictionFunctor for abelian sheaves. Tag 093Y for degreewise f_ is unnecessary, the unit of the exact pi_{G,} being invertible everywhere. The condition the composition criterion consumes at the leg f_small . pi_F is AlgebraicGeometry.Space.pushforwardComputesDerived_smallEtaleRingedToposHom for modules, out of the unconditional Tag 0D6E for a morphism of ringed topoi, and Stacks.Topos.AbelianPushforward.isKInjective_mapHomologicalComplex_abelianPushforward, Tag 075L part (2) at abelian coefficients, for abelian sheaves”.

Stacks 075N. Let S be a scheme in a big fppf site, let f : 𝒳 ⥤ 𝒴 be a 1-morphism of categories fibred in groupoids over (Sch/S)_{fppf} with 𝒳 presented by an algebraic space F and 𝒴 by an algebraic space G, and let f : F ⟶ G be the induced morphism of algebraic spaces. Then both clauses of Stacks 075N hold:

for an abelian sheaf ℱ on 𝒳_étale, (Rf_*ℱ)|_{G_étale} = Rf_{small,*}(ℱ|_{F_étale}) in D(G_étale);

for a complex ℱ of 𝒪_𝒳-modules, the same identity in D(𝒪_G).

The two components are AlgebraicGeometry.Space.restrictedAbelianDerivedDirectImageIso and AlgebraicGeometry.Space.restrictedDerivedDirectImageIso, and each is the canonical comparison of the two derived composites around the square of Stacks 073N, shown invertible — not a chosen isomorphism of abstractly isomorphic functors. In both clauses the two restriction functors appear underived, as they do in the source, being their own right derived functors because they are exact; that is the source's closing step.

The two clauses are collected as a pair rather than as a new structure because each component is already a single isomorphism of functors and nothing is shared between their types: the derived categories of D(𝒳_étale) and of D(𝒪_𝒳) are different categories, so the two clauses need their own derived direct images Rab, Rmod and their own units. A pair asserts exactly the conjunction of the two displays while keeping each one a term one can use on its own, which a Nonempty-style conjunction in Prop would not: it would assert that the two sides are abstractly isomorphic and forget that the comparison map realizing it is the canonical one.

The hypotheses are the source's — S, the 1-morphism, the two presentations eF, eG — along with the right derived direct images whose existence each display presupposes.

noncomputable def restrictedDerivedDirectImageIsoClauses :
    (Rab ⋙ (abelianRestrictionFunctor B S hS G q hq hG eG).mapDerivedCategory ≅
        (abelianRestrictionFunctor B S hS F p hp hF eF).mapDerivedCategory ⋙ RabSpace) ×
      (Rmod ⋙ RingedToposHom.derivedPushforwardOfExact
            (projectionRingedToposHom B S hS G q hq hG eG) ≅
        RingedToposHom.derivedPushforwardOfExact
            (projectionRingedToposHom B S hS F p hp hF eF) ⋙ RmodSpace)

AlgebraicGeometry.Space.restrictedTotalDerivedDirectImageIsoClauses, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/RestrictionTotalDerivedDirectImage.lean, line 370. The attribute's comment: “Both clauses, with the four derived direct images constructed: (1) for abelian sheaves (Rf_F)|_{G_etale} = Rf_{small,}(F|_{F_etale}) in D(G_etale), (2) the same identity in D(O_G) for sheaves of modules. Rf_ and Rf_{small,} are the total right derived functors of degreewise direct image, which exist by K-injective resolutions (Tag 079P) on the four essentially small sites; the only inputs are S, the 1-morphism and the two presentations.”.

Stacks 075N. Let S be a scheme in a big fppf site, let f : 𝒳 ⥤ 𝒴 be a 1-morphism of categories fibred in groupoids over (Sch/S)_{fppf} with 𝒳 presented by an algebraic space F and 𝒴 by an algebraic space G, and let f : F ⟶ G be the induced morphism of algebraic spaces. Then

for an abelian sheaf ℱ on 𝒳_étale, (Rf_*ℱ)|_{G_étale} = Rf_{small,*}(ℱ|_{F_étale}) in D(G_étale);

for a complex ℱ of 𝒪_𝒳-modules, the same identity in D(𝒪_G).

Here Rf_* and Rf_{small,*} are the total right derived direct images derivedAbelianDirectImageFibred, derivedAbelianDirectImageSpace, derivedDirectImageFibred and derivedDirectImageSpace, which exist because the four sites are essentially small — 𝒳 and 𝒴 by their presentations — so that K-injective resolutions exist (Stacks 079P). The restrictions (-)|_{F_étale}, (-)|_{G_étale} are exact and appear underived, as in the source. Each component is the canonical comparison of the two derived composites around the square of Stacks 073N, shown invertible.

def restrictedTotalDerivedDirectImageIsoClauses
    [HasDerivedCategory.{dF} (Sheaf (smallEtaleRingedTopos B S hS ⟨F, hF⟩).J AddCommGrpCat.{u})]
    [HasDerivedCategory.{dG} (Sheaf (smallEtaleRingedTopos B S hS ⟨G, hG⟩).J AddCommGrpCat.{u})]
    [HasDerivedCategory.{mF} (smallEtaleRingedTopos B S hS ⟨F, hF⟩).Modules]
    [HasDerivedCategory.{mG} (smallEtaleRingedTopos B S hS ⟨G, hG⟩).Modules]
    [letI : EssentiallySmall.{u} 𝒳 := essentiallySmall_of_equivalenceOver B S hS F p eF;
      letI : EssentiallySmall.{u} 𝒴 := essentiallySmall_of_equivalenceOver B S hS G q eG;
      HasDerivedCategory.{dX}
        (Sheaf (FibredSite.associatedRingedTopos B S hS p hp .etale).J AddCommGrpCat.{u})]
    [letI : EssentiallySmall.{u} 𝒳 := essentiallySmall_of_equivalenceOver B S hS F p eF;
      letI : EssentiallySmall.{u} 𝒴 := essentiallySmall_of_equivalenceOver B S hS G q eG;
      HasDerivedCategory.{dY}
        (Sheaf (FibredSite.associatedRingedTopos B S hS q hq .etale).J AddCommGrpCat.{u})]
    [letI : EssentiallySmall.{u} 𝒳 := essentiallySmall_of_equivalenceOver B S hS F p eF;
      letI : EssentiallySmall.{u} 𝒴 := essentiallySmall_of_equivalenceOver B S hS G q eG;
      HasDerivedCategory.{mX} (FibredSite.associatedRingedTopos B S hS p hp .etale).Modules]
    [letI : EssentiallySmall.{u} 𝒳 := essentiallySmall_of_equivalenceOver B S hS F p eF;
      letI : EssentiallySmall.{u} 𝒴 := essentiallySmall_of_equivalenceOver B S hS G q eG;
      HasDerivedCategory.{mY} (FibredSite.associatedRingedTopos B S hS q hq .etale).Modules] :
    letI : EssentiallySmall.{u} 𝒳 := essentiallySmall_of_equivalenceOver B S hS F p eF
    letI : EssentiallySmall.{u} 𝒴 := essentiallySmall_of_equivalenceOver B S hS G q eG
    (derivedAbelianDirectImageFibred B S hS p q hp hq fStack hfStack ⋙
        (abelianRestrictionFunctor B S hS G q hq hG eG).mapDerivedCategory ≅
      (abelianRestrictionFunctor B S hS F p hp hF eF).mapDerivedCategory ⋙
        derivedAbelianDirectImageSpace B S hS F G p q hF hG eF eG fStack hfStack) ×
      (derivedDirectImageFibred B S hS p q hp hq fStack hfStack ⋙
          derivedModuleRestriction B S hS q hq G hG eG ≅
        derivedModuleRestriction B S hS p hp F hF eF ⋙
          derivedDirectImageSpace B S hS F G p q hF hG eF eG fStack hfStack)

Tag 075P, a lemma

Tag 075P in the Stacks Project.

AlgebraicGeometry.Stack.inducedSquareSpacesHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/RepresentableBaseChangeSquare.lean, line 142. The attribute's comment: “the induced morphism of algebraic spaces f' : F' ⟶ G' named in the conclusion, through chosen equivalences of the apex with F' and of Y' with G'. The displayed base change identity of this tag is NOT proved”.

The morphism of algebraic spaces f' : F' ⟶ G' of Stacks 075P. For a 2-fibre product square over the cospan (g, f), with the apex represented by an algebraic space F' and the base 𝒴' of g represented by an algebraic space G', the left-hand leg f' of the square induces a morphism F' ⟶ G' of algebraic spaces: an element of F' over U is an object of the apex over U, whose image under f' is an object of 𝒴' over U, hence an element of G' over U.

This is the construction of Stacks 0GQA, AlgebraicGeometry.Space.inducedSpacesHom, read at the left-hand leg of the square. Only the two chosen equivalences and the verticality of the leg over the site enter; representability of the apex, which Stacks 0300 supplies, is what makes such an equivalence available in the first place.

The displayed identity of Stacks 075P, which is the direct image along this morphism of a restricted derived direct image, is not proved; see the implementation notes of this module.

noncomputable def inducedSquareSpacesHom
    {𝒳 𝒴 𝒴' : CatFiberedInGroupoids.{u, max u v, u + 1, max (max (u + 1) w) v}
      (BigFppfOver B S hS)}
    {f : 𝒳 ⟶ 𝒴} {g : 𝒴' ⟶ 𝒴} (P : Bicategory.TwoCommSq g f)
    {F' G' : AlgebraicSpaces B S hS}
    (eF' : StacksRepresentableCFG.EquivalenceOver P.pt.val.p
      (presheafOfCategories (F'.1 ⋙ typeToCat)).p)
    (eG' : StacksRepresentableCFG.EquivalenceOver 𝒴'.val.p
      (presheafOfCategories (G'.1 ⋙ typeToCat)).p) :
    F' ⟶ G'

AlgebraicGeometry.Stack.RepresentableBaseChangeSquare.exists_isAlgebraicSpace_apex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/RepresentableBaseChangeSquareDerived.lean, line 305. The attribute's comment: “The first assertion: the apex X' of the 2-fibre product square is representable by an algebraic space F', given that f is representable by algebraic spaces and that Y' is representable by an algebraic space.”.

The apex of the square is representable by an algebraic space, when f is representable by algebraic spaces and 𝒴' is representable by an algebraic space. This is Stacks 0300, AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpace_twoFibreProduct, for the 2-fibre product with the factors in the order of the source's square, read through the exchange of the two factors CategoryTheory.TwoFibreProductOver.swapEquivalenceOver.

theorem exists_isAlgebraicSpace_apex (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom.hom)
    (h𝒴' : IsRepresentableByAlgebraicSpace B S hS 𝒴'.val) :
    ∃ F' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u, IsAlgebraicSpace B S hS F' ∧
      Nonempty (StacksRepresentableCFG.EquivalenceOver (apexP B S hS f g)
        (presheafOfCategories (F' ⋙ typeToCat)).p)

AlgebraicGeometry.Stack.RepresentableBaseChangeSquare.restrictedDerivedBaseChangeIsoClauses, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/RepresentableBaseChangeSquareDerived.lean, line 1120. The attribute's comment: “The displayed identity, both clauses, as isomorphisms of functors on the unbounded derived categories: (1) g^{-1}(Rf_F)|_{G'_etale} = Rf'_{small,}((g')^{-1}F|_{F'_etale}) for F in D(X_etale), (2) the same identity for F in D(O_X), for any presentations of Y' and of the apex X' by algebraic spaces G' and F'.”.

Stacks 075P. Let S be a scheme and let
𝒴' ×_𝒴 𝒳 --g'--> 𝒳
    |            |
    f'           f
    v            v
    𝒴' ---g--->  𝒴
be the 2-fibre product square of algebraic stacks over S. If 𝒴' is represented by an algebraic space G' and the apex by an algebraic space F' — which is the case as soon as f is representable by algebraic spaces, by exists_isAlgebraicSpace_apex — and f' : F' ⟶ G' is the induced morphism of algebraic spaces, then

g⁻¹(Rf_*ℱ)|_{G'_étale} = Rf'_{small,*}((g')⁻¹ℱ|_{F'_étale})

for ℱ in D(𝒳_étale), in particular for an abelian sheaf on 𝒳_étale, and

for ℱ in D(𝒪_𝒳), in particular for a sheaf of 𝒪_𝒳-modules,

as isomorphisms of functors. The derived direct images are the total right derived functors of Stacks 075N, AlgebraicGeometry.Space.derivedAbelianDirectImageFibred, AlgebraicGeometry.Space.derivedAbelianDirectImageSpace, AlgebraicGeometry.Space.derivedDirectImageFibred and AlgebraicGeometry.Space.derivedDirectImageSpace.

def restrictedDerivedBaseChangeIsoClauses :
    (Space.derivedAbelianDirectImageFibred B S hS 𝒳.val.val.p 𝒴.val.val.p
        (𝒳.val.isFiberedInGroupoids) (𝒴.val.isFiberedInGroupoids) f.hom.hom.toFunctor
        ((𝒴.val.isFiberedInGroupoids).isFibredOneMorphism f.hom.hom.w) ⋙
        (inverseImageAb B S hS g).mapDerivedCategory ⋙
          (restrictionG'Ab B S hS G' hG' eG').mapDerivedCategory ≅
      (fstInverseImageAb B S hS f g).mapDerivedCategory ⋙
        (restrictionF'Ab B S hS f g F' hF' eF').mapDerivedCategory ⋙
          Space.derivedAbelianDirectImageSpace B S hS F' G' (apexP B S hS f g) 𝒴'.val.val.p hF'
            hG' eF' eG' (TwoFibreProductOver.snd _ _ _ f.hom.hom.toFunctor g.hom.hom.toFunctor)
            (snd_isFibredOneMorphism B S hS f g)) ×
    (Space.derivedDirectImageFibred B S hS 𝒳.val.val.p 𝒴.val.val.p
        (𝒳.val.isFiberedInGroupoids) (𝒴.val.isFiberedInGroupoids) f.hom.hom.toFunctor
        ((𝒴.val.isFiberedInGroupoids).isFibredOneMorphism f.hom.hom.w) ⋙
        (inverseImageMod B S hS g).mapDerivedCategory ⋙
          (Space.projectionRingedToposHom B S hS G' 𝒴'.val.val.p (𝒴'.val.isFiberedInGroupoids)
            hG' eG').derivedPushforwardOfExact ≅
      (fstInverseImageMod B S hS f g).mapDerivedCategory ⋙
        (Space.projectionRingedToposHom B S hS F' (apexP B S hS f g)
          (apexP_isFiberedInGroupoids B S hS f g) hF' eF').derivedPushforwardOfExact ⋙
          Space.derivedDirectImageSpace B S hS F' G' (apexP B S hS f g) 𝒴'.val.val.p hF'
            hG' eF' eG' (TwoFibreProductOver.snd _ _ _ f.hom.hom.toFunctor g.hom.hom.toFunctor)
            (snd_isFibredOneMorphism B S hS f g))

Declarations registered for the tag:

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpace_of_isTwoFibreProduct, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/RepresentableBaseChangeSquare.lean, line 113 (StacksFrontier): “the first assertion of the conclusion: the apex X' of the 2-fibre product square is representable by an algebraic space F', given that f is representable by algebraic spaces and that Y' is representable by an algebraic space. This is Tag 0300, at hypotheses weaker than the source's. The displayed base change identity of this tag is NOT proved; see the implementation notes of StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/RepresentableBaseChangeSquare.lean”.

Sources

LeanAlgebraicGeometry.Space.injective_restrictionAbSheafFunctor_obj · AlgebraicGeometry.Space.isKInjective_restrictionAbSheafFunctor_obj · AlgebraicGeometry.Space.restrictedDerivedDirectImageIsoClauses · AlgebraicGeometry.Space.restrictedTotalDerivedDirectImageIsoClauses · AlgebraicGeometry.Stack.inducedSquareSpacesHom · AlgebraicGeometry.Stack.RepresentableBaseChangeSquare.exists_isAlgebraicSpace_apex · AlgebraicGeometry.Stack.RepresentableBaseChangeSquare.restrictedDerivedBaseChangeIsoClauses · AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpace_of_isTwoFibreProduct

Section96.23 Change of topology #

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

Tag 076T, a lemma

Tag 076T in the Stacks Project.

AlgebraicGeometry.Stack.isSheaf_fppf_of_isLocallyQuasicoherent_of_flatBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FppfSheafFlatBaseChangeProved.lean, line 90.

Stacks 076T. Let F be a presheaf of modules over the structure sheaf of a category fibred in groupoids over the big fppf category of schemes over S. If F is locally quasi-coherent (Stacks 06WJ) and the comparison map c_φ of Stacks 06WC is an isomorphism for every arrow of 𝒳 lying over a morphism of schemes which is flat and locally of finite presentation, then F is a sheaf for the fppf topology of Stacks 06TP.

The sheaf condition is tested, by AlgebraicGeometry.Stack.isSheaf_of_isSheafFor_flatLfp, on the families of arrows lying over an fppf covering of schemes; along such a family hypothesis (b) applies to every member, and the sheaf condition for it is AlgebraicGeometry.Stack.isSheafForLiftedFppfFamily_of_isFiberedInGroupoids.

theorem isSheaf_fppf_of_isLocallyQuasicoherent_of_flatBaseChange
    (F : PresheafOfModules.{u} (ringStructureSheafCore B S hS p hp (etaleTopology B)
      (etaleTopology_le_topology B)).obj)
    (hlqc : IsLocallyQuasicoherent B E h S hS p hp F)
    (hbc : HasFlatLfpBaseChangeProperty B E h S hS p hp (etaleTopology B)
      (etaleTopology_le_topology B) F) :
    Presheaf.IsSheaf (associatedTopology B S hS p B.topology) F.presheaf

AlgebraicGeometry.Stack.isSheaf_fppf_of_isLocallyQuasicoherent_of_isLocallyBijective_flatLfp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FppfSheafOfLocallyBijectiveFlatLfpComparison.lean, line 62. The attribute's comment: “with the pullback of sheaves of Stacks 06WC in hypothesis (b)”.

Stacks 076T, with the pullback of sheaves of Stacks 06WC. Let F be a presheaf of modules over the structure sheaf of a category fibred in groupoids over (Sch/S)_{fppf}. If F is locally quasi-coherent (Stacks 06WJ) and the comparison map c_φ : f_{small}^*(F|_{V_ét}) ⟶ F|_{U_ét} is an isomorphism of sheaves (it is locally injective and locally surjective for the étale topology of the small site of U) for every arrow φ of 𝒳 lying over a morphism of schemes which is flat and locally of finite presentation, then F is a sheaf for the fppf topology of Stacks 06TP.

theorem isSheaf_fppf_of_isLocallyQuasicoherent_of_isLocallyBijective_flatLfp
    (hlqc : IsLocallyQuasicoherent B E h S hS p hp F)
    (hbc : ∀ {x y : 𝒳} (φ : x ⟶ y), Flat (B.inclusion.map (p.map φ).left) →
      LocallyOfFinitePresentation (B.inclusion.map (p.map φ).left) →
        IsLocallyBijectiveRestrictModulePullbackComparisonUnivLE B E h S hS p hp
          (etaleTopology B) (etaleTopology_le_topology B) φ F) :
    Presheaf.IsSheaf (associatedTopology B S hS p B.topology) F.presheaf

Tag 075R, a lemma

Tag 075R in the Stacks Project.

AlgebraicGeometry.Stack.isZero_rightDerived_etaleComparisonPushforward_of_lqcFbc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/EtaleComparisonAcyclicity.lean, line 197. The attribute's comment: “clause (1), Rε_*ℱ = ε_*ℱ for the comparison ε : 𝒳_fppf ⟶ 𝒳_étale and a module which is locally quasi-coherent with flat base change: the vanishing of the higher direct images, reduced through Stacks 072W to the affine-object vanishing Stacks 08IY and 08IZ carry, which is carried here as that same predicate hvan, together with the étale covering class of the affine objects as hB. Clauses (2) and (3), which the source deduces from (1) by the Leray spectral sequence and by Stacks 075G, are not covered”.

Stacks 075R, clause (1). Let 𝒳 be a category fibred in groupoids over the big fppf site of S, let ε : 𝒳_fppf ⟶ 𝒳_étale be the comparison morphism, and let ℱ be a sheaf of 𝒪_𝒳-modules on the fppf site which is locally quasi-coherent (Stacks 06WJ) and has the flat base change property (Stacks 0762). Then

R^iε_*ℱ = 0 for i > 0,

that is, Rε_*ℱ = ε_*ℱ.

This is the source's reduction: by Stacks 072W the sheaf R^iε_*ℱ is the étale sheafification of the presheaf x ↦ H^i_{fppf}(x, ℱ), and that presheaf vanishes on the objects lying over an affine scheme, which cover étale-locally.

The affine vanishing hvan and the covering class hB are carried; see this file's module documentation.

theorem isZero_rightDerived_etaleComparisonPushforward_of_lqcFbc
    [HasSheafify (BigFppfOver.associatedTopology B S hS p .etale) AddCommGrpCat.{u}]
    [(BigFppfOver.associatedTopology B S hS p .etale).WEqualsLocallyBijective AddCommGrpCat.{u}]
    (hB : (BigFppfOver.associatedTopology B S hS p .etale).HasEnoughObjects
      (fun x => IsAffineOver B S hS (p.obj x)))
    (hvan : HasAffineAcyclicLqcFbcModules B E h S hS p hp)
    (ℱ : fppfSiteModules B S hS p hp)
    (hℱ : IsLocallyQuasicoherentWithFlatBaseChange B E h S hS p hp ℱ.val)
    (i : ℕ) (hi : 0 < i) :
    IsZero (((etaleComparisonPushforward B S hS p hp).rightDerived i).obj ℱ)

AlgebraicGeometry.Stack.isSheaf_fppf_of_lqc_flatLfp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FppfEtaleComparisonLqcFbc.lean, line 107. The attribute's comment: “the first assertion: a presheaf of modules satisfying (a) and (b) is an 𝒪_𝒳-module, i.e. a sheaf for the fppf topology”.

Stacks 075R, the first assertion. A presheaf of 𝒪_𝒳-modules which is locally quasi-coherent (Stacks 06WJ) and whose comparison maps c_φ of Stacks 06WC are isomorphisms along the arrows lying over flat morphisms locally of finite presentation is a sheaf for the fppf topology of 𝒳, that is, an 𝒪_𝒳-module.

theorem isSheaf_fppf_of_lqc_flatLfp :
    Presheaf.IsSheaf (BigFppfOver.associatedTopology B S hS p .fppf) F.presheaf

AlgebraicGeometry.Stack.isZero_rightDerived_etaleComparisonPushforward_lqcFbcModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FppfEtaleComparisonLqcFbc.lean, line 200. The attribute's comment: “clause (1): Rε_*ℱ = ε_*ℱ, i.e. R^iε_*ℱ = 0 for i > 0, for the comparison ε : 𝒳_fppf ⟶ 𝒳_étale and a module satisfying (a) and (b)”.

Stacks 075R, clause (1). Let ℱ be a presheaf of 𝒪_𝒳-modules which is locally quasi-coherent (Stacks 06WJ) and whose comparison maps c_φ of Stacks 06WC are isomorphisms along the arrows lying over flat morphisms locally of finite presentation, and let ε : 𝒳_{fppf} ⟶ 𝒳_{étale} be the comparison morphism. Then

R^iε_*ℱ = 0 for i > 0,

that is, Rε_*ℱ = ε_*ℱ. Here ℱ is the 𝒪_𝒳-module of the first assertion, AlgebraicGeometry.Stack.lqcFbcModule.

theorem isZero_rightDerived_etaleComparisonPushforward_lqcFbcModule (i : ℕ) (hi : 0 < i) :
    IsZero (((etaleComparisonPushforward B S hS p hp).rightDerived i).obj
      (lqcFbcModule B E h S hS p hp F hlqc hbc))

AlgebraicGeometry.Stack.nonempty_fppfCohomologyIso_etaleCohomology_lqcFbcModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LqcFbcModuleFppfEtaleCohomology.lean, line 203. The attribute's comment: “clause (2): fppf cohomology H^p(𝒳, ℱ), H^p(x, ℱ) and the derived sections RΓ(𝒳, ℱ), RΓ(x, ℱ) of a module satisfying (a) and (b) agree with those computed in the étale topology”.

Stacks 075R, clause (2). Let ℱ be a presheaf of 𝒪_𝒳-modules satisfying (a) and (b) of Stacks 075R, so an 𝒪_𝒳-module (AlgebraicGeometry.Stack.lqcFbcModule), and let ε : 𝒳_{fppf} ⟶ 𝒳_{étale} be the comparison morphism. The cohomology of ℱ computed in the fppf topology agrees with the cohomology of ε_*ℱ, the same presheaf of modules, computed in the étale topology:

H^n_{fppf}(𝒳, ℱ) ≅ H^n_{étale}(𝒳, ε_*ℱ) for all n;

H^n_{fppf}(x, ℱ) ≅ H^n_{étale}(x, ε_*ℱ) for every object x of 𝒳 and all n;

RΓ_{fppf}(𝒳, ℱ) ≅ RΓ_{étale}(𝒳, ε_*ℱ) and RΓ_{fppf}(x, ℱ) ≅ RΓ_{étale}(x, ε_*ℱ), the derived sections being the complexes of sections of injective resolutions, up to homotopy.

As in the source this follows formally from clause (1): ε_* is left exact and preserves injectives, and ℱ is ε_*-acyclic by AlgebraicGeometry.Stack.isZero_rightDerived_etaleComparisonPushforward_lqcFbcModule, so ε_* carries an injective resolution of ℱ to one of ε_*ℱ, and both cohomologies are computed by the same complex of sections.

theorem nonempty_fppfCohomologyIso_etaleCohomology_lqcFbcModule :
    (∀ n : ℕ, Nonempty (((Stacks.Cohomology.SiteModules.globalSectionsFunctor.{v, u, u, u}
        (fppfSiteRingSheaf B S hS p hp)).rightDerived n).obj
        (lqcFbcModule B E h S hS p hp F hlqc hbc) ≅
      ((Stacks.Cohomology.SiteModules.globalSectionsFunctor.{v, u, u, u}
        (etaleSiteRingSheaf B S hS p hp)).rightDerived n).obj
        ((etaleComparisonPushforward B S hS p hp).obj
          (lqcFbcModule B E h S hS p hp F hlqc hbc)))) ∧
    (∀ (x : 𝒳) (n : ℕ), Nonempty
      (((SheafOfModules.evaluation.{u} (fppfSiteRingSheaf B S hS p hp) (op x)).rightDerived n).obj
        (lqcFbcModule B E h S hS p hp F hlqc hbc) ≅
      ((SheafOfModules.evaluation.{u} (etaleSiteRingSheaf B S hS p hp) (op x)).rightDerived n).obj
        ((etaleComparisonPushforward B S hS p hp).obj
          (lqcFbcModule B E h S hS p hp F hlqc hbc)))) ∧
    Nonempty ((Stacks.Cohomology.SiteModules.globalSectionsFunctor.{v, u, u, u}
        (fppfSiteRingSheaf B S hS p hp)).rightDerivedToHomotopyCategory.obj
        (lqcFbcModule B E h S hS p hp F hlqc hbc) ≅
      (Stacks.Cohomology.SiteModules.globalSectionsFunctor.{v, u, u, u}
        (etaleSiteRingSheaf B S hS p hp)).rightDerivedToHomotopyCategory.obj
        ((etaleComparisonPushforward B S hS p hp).obj
          (lqcFbcModule B E h S hS p hp F hlqc hbc))) ∧
    (∀ x : 𝒳, Nonempty
      ((SheafOfModules.evaluation.{u} (fppfSiteRingSheaf B S hS p hp)
          (op x)).rightDerivedToHomotopyCategory.obj
        (lqcFbcModule B E h S hS p hp F hlqc hbc) ≅
      (SheafOfModules.evaluation.{u} (etaleSiteRingSheaf B S hS p hp)
          (op x)).rightDerivedToHomotopyCategory.obj
        ((etaleComparisonPushforward B S hS p hp).obj
          (lqcFbcModule B E h S hS p hp F hlqc hbc))))

AlgebraicGeometry.Stack.nonempty_higherDirectImageIso_sheafify_etale_lqcFbcModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LqcFbcModuleFppfEtaleHigherDirectImage.lean, line 282. The attribute's comment: “clause (3): for a 1-morphism f : 𝒳 → 𝒴 of categories fibred in groupoids and a module ℱ satisfying (a) and (b), R^if_*ℱ is the fppf sheafification of the higher direct image computed in the étale topology, and similarly for the derived direct image”.

Stacks 075R, clause (3). Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of categories fibred in groupoids over (Sch/S)_{fppf} and let ℱ be a presheaf of 𝒪_𝒳-modules satisfying (a) and (b) of Stacks 075R, so an 𝒪_𝒳-module (AlgebraicGeometry.Stack.lqcFbcModule). Then

R^i f_*ℱ, computed in the fppf topology, is the fppf sheafification of the higher direct image R^i f_{étale,*}(ε_*ℱ) computed in the étale topology, for every i;

similarly for the derived direct image: Rf_*ℱ is ε⁻¹(Rf_{étale,*}(ε_*ℱ)), the direct images being those of injective resolutions, up to homotopy, and ε⁻¹ the fppf sheafification of étale modules (Stacks.SheafOfModules.comparisonPullbackIso).

The source deduces this from (2) and Stacks 075G. Here it is deduced from (1) directly: f_{fppf,*} ≅ ε⁻¹ ∘ f_{étale,*} ∘ ε_* (AlgebraicGeometry.Stack.moduleDirectImageIsoEtale), ε_* carries an injective resolution of the ε_*-acyclic module ℱ to one of ε_*ℱ, and ε⁻¹ is exact.

theorem nonempty_higherDirectImageIso_sheafify_etale_lqcFbcModule :
    (∀ i : ℕ, Nonempty (((moduleDirectImageSmall B S hS p q hp hq f hf .fppf).rightDerived i).obj
        (lqcFbcModule B E h S hS p hp F hlqc hbc) ≅
      (PresheafOfModules.sheafification.{u} (𝟙 (fppfSiteRingSheaf B S hS q hq).obj)).obj
        (((moduleDirectImageSmall B S hS p q hp hq f hf .etale).rightDerived i).obj
          ((etaleComparisonPushforward B S hS p hp).obj
            (lqcFbcModule B E h S hS p hp F hlqc hbc))).val)) ∧
    Nonempty
      ((moduleDirectImageSmall B S hS p q hp hq f hf .fppf).rightDerivedToHomotopyCategory.obj
          (lqcFbcModule B E h S hS p hp F hlqc hbc) ≅
        ((etaleComparisonPullback B S hS q hq).mapHomotopyCategory (ComplexShape.up ℕ)).obj
          ((moduleDirectImageSmall B S hS p q hp hq f hf .etale).rightDerivedToHomotopyCategory.obj
            ((etaleComparisonPushforward B S hS p hp).obj
              (lqcFbcModule B E h S hS p hp F hlqc hbc))))

Tag 07AK, a lemma

Tag 07AK in the Stacks Project.

AlgebraicGeometry.Stack.inclusionToposMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubcategorySiteKind.lean, line 133. The attribute's comment: “the morphism of topoi g : Sh(𝒳'_τ) ⟶ Sh(𝒳_τ) defined by the inclusion, whose inverse image is restriction to 𝒳'”.

Stacks 07AK, the morphism of topoi. Cocontinuity of the inclusion gives the adjoint pair g^{-1} ⊣ g_* between the topos of the subcategory site and that of the ambient site, with g^{-1} left exact: the morphism of topoi g : Sh(𝒳'_τ) ⟶ Sh(𝒳_τ) of the source.

The sheaves take values in Type max v w, which is the universe in which the sheaves of sets on either site live.

def inclusionToposMorphism (τ : SiteKind) (hp : p.IsFiberedInGroupoids)
    (hclose : IsClosedUnderSitePullback B S hS p P τ) :
    MorphismOfTopoi
      (Sheaf (P.ι.inheritedTopology (BigFppfOver.associatedTopology B S hS p τ))
        (Type max v w))
      (Sheaf (BigFppfOver.associatedTopology B S hS p τ) (Type max v w))

AlgebraicGeometry.Stack.subsite_cohomology_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteCohomologyAtlas.lean, line 238.

Stacks 07AK. Let 𝒳 be an algebraic stack over S, let τ be the étale or the fppf topology, and let 𝒳' ⊆ 𝒳 be a full subcategory such that

if x ⟶ x' is a morphism of 𝒳 lying over a smooth (respectively flat and locally finitely presented) morphism of schemes and x' is in 𝒳', then x is in 𝒳' — this is AlgebraicGeometry.Stack.IsClosedUnderSitePullback, which also pins τ down to one of the two admissible topologies; and

there is an object x of 𝒳' lying over a scheme U whose associated 1-morphism x : (Sch/U)_fppf ⟶ 𝒳 is smooth and surjective.

Give 𝒳' the topology whose coverings are the families of 𝒳' that are coverings of 𝒳_τ. Then the inclusion 𝒳' ⟶ 𝒳_τ is fully faithful, continuous and cocontinuous, so it defines a morphism of topoi g : Sh(𝒳'_τ) ⟶ Sh(𝒳_τ) — AlgebraicGeometry.Stack.inclusionToposMorphism, whose inverse image is restriction to 𝒳' — and H^p(𝒳'_τ, g⁻¹ℱ) ≅ H^p(𝒳_τ, ℱ) for all p ≥ 0 and all abelian sheaves ℱ on 𝒳_τ, where on abelian sheaves g⁻¹ is again restriction to 𝒳'.

The isomorphism of cohomology groups is the natural isomorphism AlgebraicGeometry.Stack.subsiteCohomologyIsoOfAtlas.

theorem subsite_cohomology_comparison :
    P.ι.Full ∧ P.ι.Faithful ∧
      P.ι.IsContinuous (P.ι.inheritedTopology (BigFppfOver.associatedTopology B S hS
        𝒳.val.val.p τ)) (BigFppfOver.associatedTopology B S hS 𝒳.val.val.p τ) ∧
      P.ι.IsCocontinuous (P.ι.inheritedTopology (BigFppfOver.associatedTopology B S hS
        𝒳.val.val.p τ)) (BigFppfOver.associatedTopology B S hS 𝒳.val.val.p τ) ∧
      (haveI := isContinuous_ι_associatedTopology_of_isClosedUnderSitePullback B S hS
          𝒳.val.val.p P τ 𝒳.val.isFiberedInGroupoids hcl;
        Nonempty ((inclusionToposMorphism B S hS 𝒳.val.val.p P τ 𝒳.val.isFiberedInGroupoids
          hcl).inverseImage ≅ P.ι.sheafPushforwardContinuous (Type (u + 1))
            (P.ι.inheritedTopology (BigFppfOver.associatedTopology B S hS 𝒳.val.val.p τ))
            (BigFppfOver.associatedTopology B S hS 𝒳.val.val.p τ))) ∧
      ∀ q : ℕ,
        haveI := isContinuous_ι_associatedTopology_of_isClosedUnderSitePullback B S hS
          𝒳.val.val.p P τ 𝒳.val.isFiberedInGroupoids hcl;
        Nonempty (P.ι.sheafPushforwardContinuous AddCommGrpCat.{u + 1}
            (P.ι.inheritedTopology (BigFppfOver.associatedTopology B S hS 𝒳.val.val.p τ))
            (BigFppfOver.associatedTopology B S hS 𝒳.val.val.p τ) ⋙
          Sheaf.functorH.{u + 1, u + 1, u, u + 1}
            (P.ι.inheritedTopology (BigFppfOver.associatedTopology B S hS 𝒳.val.val.p τ)) q ≅
          Sheaf.functorH.{u + 1, u + 1, u, u + 1}
            (BigFppfOver.associatedTopology B S hS 𝒳.val.val.p τ) q)

Sources

LeanAlgebraicGeometry.Stack.isSheaf_fppf_of_isLocallyQuasicoherent_of_flatBaseChange · AlgebraicGeometry.Stack.isSheaf_fppf_of_isLocallyQuasicoherent_of_isLocallyBijective_flatLfp · AlgebraicGeometry.Stack.isZero_rightDerived_etaleComparisonPushforward_of_lqcFbc · AlgebraicGeometry.Stack.isSheaf_fppf_of_lqc_flatLfp · AlgebraicGeometry.Stack.isZero_rightDerived_etaleComparisonPushforward_lqcFbcModule · AlgebraicGeometry.Stack.nonempty_fppfCohomologyIso_etaleCohomology_lqcFbcModule · AlgebraicGeometry.Stack.nonempty_higherDirectImageIso_sheafify_etale_lqcFbcModule · AlgebraicGeometry.Stack.inclusionToposMorphism

Section96.24 Restricting to affines #

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

Tag 0H09, a definition

Tag 0H09 in the Stacks Project.

AlgebraicGeometry.Stack.associatedAffineChaoticTopology, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/AffineSite.lean, line 167.

Stacks 0H09. The associated affine site of a category p : 𝒳 ⥤ (Sch/S)_{fppf}: the affine subcategory 𝒳_{affine} carrying the chaotic topology, in which the maximal sieve is the only covering sieve.

abbrev associatedAffineChaoticTopology : GrothendieckTopology (AffineCategory B S hS p)

AlgebraicGeometry.Stack.sheafAssociatedAffineChaoticEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/AffineSite.lean, line 173. The attribute's comment: “sheaves are presheaves”.

Stacks 0H09. Sheaves on the associated affine site are the same as presheaves on the affine subcategory: the forgetful functor from sheaves to presheaves is an equivalence.

def sheafAssociatedAffineChaoticEquivalence (A : Type*) [Category A] :
    Sheaf (associatedAffineChaoticTopology B S hS p) A ≌ (AffineCategory B S hS p)ᵒᵖ ⥤ A

Tag 0H0A, a definition

Tag 0H0A in the Stacks Project.

AlgebraicGeometry.Stack.AffineCategory, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/AffineSite.lean, line 102. The attribute's comment: “the affine subcategory”.

Stacks 0H0A. The affine subcategory of a category over the big fppf category of S: the full subcategory of the objects lying over an affine scheme.

abbrev AffineCategory

AlgebraicGeometry.Stack.AffineCategory.isStronglyCartesian_toAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/AffineSite.lean, line 117. The attribute's comment: “arrows are strongly cartesian”.

Stacks 0H0A. Every arrow between affine objects of a category fibred in groupoids is strongly cartesian for the restricted structure functor.

theorem isStronglyCartesian_toAffine (hp : p.IsFiberedInGroupoids)
    {x y : AffineCategory B S hS p} (φ : y ⟶ x) :
    (toAffine B S hS p).IsStronglyCartesian ((toAffine B S hS p).map φ) φ

AlgebraicGeometry.Stack.associatedAffineTopology, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/AffineSite.lean, line 142. The attribute's comment: “the associated affine topology”.

Stacks 0H0A. The associated affine site of a category p : 𝒳 ⥤ (Sch/S)_{fppf} and a topology τ on the affine schemes over S: the topology the affine subcategory inherits from τ.

The five associated affine sites of the source — Zariski, étale, smooth, syntomic and fppf — are the values of this at the five big affine topologies.

abbrev associatedAffineTopology (τ : GrothendieckTopology (BigAffineFppf B S hS)) :
    GrothendieckTopology (AffineCategory B S hS p)

AlgebraicGeometry.Stack.generate_mem_associatedAffineTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/AffineSite.lean, line 153. The attribute's comment: “the covering families”.

Stacks 0H0A. A family in the affine subcategory of a category fibred in groupoids whose image in the affine schemes over S generates a covering sieve generates a covering sieve for the associated affine topology.

This is the description of the coverings of 𝒳_{affine, τ} in the paragraph following the source's definition.

theorem generate_mem_associatedAffineTopology (hp : p.IsFiberedInGroupoids)
    (τ : GrothendieckTopology (BigAffineFppf B S hS))
    (E : Covering.{v, w, u + 1} (AffineCategory B S hS p))
    (hE : Sieve.generate (E.2.map (AffineCategory.toAffine B S hS p)).presieve₀ ∈
      τ ((AffineCategory.toAffine B S hS p).obj E.1)) :
    Sieve.generate E.2.presieve₀ ∈ associatedAffineTopology B S hS p τ E.1

Tag 0H0B, a lemma

Tag 0H0B in the Stacks Project.

AlgebraicGeometry.Stack.AffineCategory.isFiberedInGroupoids_toAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/AffineSiteEquivalence.lean, line 168. The attribute's comment: “the affine structure functor is fibred in groupoids”.

Stacks 0H0B. The structure functor of the affine subcategory of a category fibred in groupoids is again fibred in groupoids, over the big affine fppf category of S.

theorem isFiberedInGroupoids_toAffine (hp : p.IsFiberedInGroupoids) :
    (toAffine B S hS p).IsFiberedInGroupoids

AlgebraicGeometry.Stack.AffineCategory.isCoverDense_inclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/AffineSiteEquivalence.lean, line 205. The attribute's comment: “cover density”.

Stacks 0H0B. The affine inclusion of a category fibred in groupoids is cover dense for the inherited topology, as soon as the affine inclusion of the big fppf category over S is cover dense.

theorem isCoverDense_inclusion (hp : p.IsFiberedInGroupoids)
    (K : GrothendieckTopology (BigFppfOver B S hS))
    (hj : (BigAffineFppf.inclusion B S hS).IsCoverDense K) :
    (inclusion B S hS p).IsCoverDense (p.inheritedTopology K)

AlgebraicGeometry.Stack.AffineCategory.inclusion_isSpecialCocontinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/AffineSiteEquivalence.lean, line 235.

Stacks 0H0B. The inclusion of the affine subcategory of a category fibred in groupoids is a special cocontinuous functor from the associated affine site to the associated site, for any topology on the big affine fppf category of S and any topology on the big fppf category over S for which the affine inclusion downstairs is a dense subsite inclusion.

Consequently the inclusion induces an equivalence of sheaf topoi. The five topologies of the source are the five instances.

theorem inclusion_isSpecialCocontinuous (hp : p.IsFiberedInGroupoids)
    (J : GrothendieckTopology (BigAffineFppf B S hS))
    (K : GrothendieckTopology (BigFppfOver B S hS))
    (hbase : (BigAffineFppf.inclusion B S hS).IsDenseSubsite J K) :
    IsSpecialCocontinuous (associatedAffineTopology B S hS p J) (p.inheritedTopology K)
      (inclusion B S hS p)

AlgebraicGeometry.Stack.AffineCategory.inclusion_isSpecialCocontinuous_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/AffineSiteEquivalence.lean, line 267. The attribute's comment: “the fppf topology”.

Stacks 0H0B for the fppf topology: the inclusion of the affine subcategory into a category fibred in groupoids is special cocontinuous from the associated affine fppf site to the associated fppf site, and so induces an equivalence of the sheaf topoi.

theorem inclusion_isSpecialCocontinuous_fppf (hp : p.IsFiberedInGroupoids) :
    IsSpecialCocontinuous
      (associatedAffineTopology B S hS p (BigAffineFppf.topology B S hS))
      (associatedTopology B S hS p B.topology) (inclusion B S hS p)

AlgebraicGeometry.Stack.AffineCategory.inclusion_isSpecialCocontinuous_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/AffineSiteEtaleSmooth.lean, line 60. The attribute's comment: “the étale topology”.

Stacks 0H0B for the étale topology: the inclusion of the affine subcategory into a category fibred in groupoids is special cocontinuous from the associated affine étale site to the associated étale site, and so induces an equivalence of the sheaf topoi.

theorem inclusion_isSpecialCocontinuous_etale (hp : p.IsFiberedInGroupoids) :
    IsSpecialCocontinuous
      (associatedAffineTopology B S hS p (BigAffineEtale.topology B.toBigEtaleSite S hS))
      (p.inheritedTopology (BigEtaleOver.topology B.toBigEtaleSite S hS))
      (inclusion B S hS p)

AlgebraicGeometry.Stack.AffineCategory.inclusion_isSpecialCocontinuous_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/AffineSiteEtaleSmooth.lean, line 72. The attribute's comment: “the smooth topology”.

Stacks 0H0B for the smooth topology: the inclusion of the affine subcategory into a category fibred in groupoids is special cocontinuous from the associated affine smooth site to the associated smooth site, and so induces an equivalence of the sheaf topoi.

theorem inclusion_isSpecialCocontinuous_smooth (hp : p.IsFiberedInGroupoids) :
    IsSpecialCocontinuous
      (associatedAffineTopology B S hS p (BigAffineSmooth.topology B.toBigSmoothSite S hS))
      (p.inheritedTopology (BigSmoothOver.topology B.toBigSmoothSite S hS))
      (inclusion B S hS p)

AlgebraicGeometry.Stack.AffineCategory.inclusion_isSpecialCocontinuous_zariski, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/AffineSiteZariskiSyntomic.lean, line 56. The attribute's comment: “the Zariski topology”.

Stacks 0H0B for the Zariski topology: the inclusion of the affine subcategory into a category fibred in groupoids is special cocontinuous from the associated affine Zariski site to the associated Zariski site, and so induces an equivalence of the sheaf topoi.

theorem inclusion_isSpecialCocontinuous_zariski (hp : p.IsFiberedInGroupoids) :
    IsSpecialCocontinuous
      (associatedAffineTopology B S hS p (BigAffineZariski.topology B.toBigZariskiSite S hS))
      (p.inheritedTopology (BigZariskiOver.topology B.toBigZariskiSite S hS))
      (inclusion B S hS p)

AlgebraicGeometry.Stack.AffineCategory.inclusion_isSpecialCocontinuous_syntomic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/AffineSiteZariskiSyntomic.lean, line 68. The attribute's comment: “the syntomic topology”.

Stacks 0H0B for the syntomic topology: the inclusion of the affine subcategory into a category fibred in groupoids is special cocontinuous from the associated affine syntomic site to the associated syntomic site, and so induces an equivalence of the sheaf topoi.

theorem inclusion_isSpecialCocontinuous_syntomic (hp : p.IsFiberedInGroupoids) :
    IsSpecialCocontinuous
      (associatedAffineTopology B S hS p (BigAffineSyntomic.topology B.toBigSyntomicSite S hS))
      (p.inheritedTopology (BigSyntomicOver.topology B.toBigSyntomicSite S hS))
      (inclusion B S hS p)

Tag 0H0C, an equation

Tag 0H0C in the Stacks Project.

AlgebraicGeometry.Stack.affineToFull, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/AffineRingedTopos.lean, line 168. The attribute's comment: “the morphism of ringed topoi”.

The morphism of ringed topoi induced by the inclusion of the affine subsite: its underlying morphism of topoi is the equivalence of Stacks 0H0B and its structure morphism is the adjunct of the identification of the inverse image of the structure sheaf with its restriction.

noncomputable def affineToFull
    (O : Sheaf (associatedTopology B S hS p τ) CommRingCat.{max u v w}) :
    AlgebraicGeometry.RingedToposHom (affineRingedTopos B S hS p τ J O)
      (fullRingedTopos B S hS p τ O)

AlgebraicGeometry.Stack.isIso_affineToFull_fSharpInverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/AffineRingedTopos.lean, line 186. The attribute's comment: “the structure morphism is an isomorphism”.

The structure morphism of affineToFull is an isomorphism.

theorem isIso_affineToFull_fSharpInverseImage
    (O : Sheaf (associatedTopology B S hS p τ) CommRingCat.{max u v w}) :
    IsIso (affineToFull B S hS p τ J O).fSharpInverseImage

AlgebraicGeometry.Stack.isEquivalence_affineToFull_inverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/AffineRingedTopos.lean, line 194. The attribute's comment: “the inverse image is an equivalence”.

The inverse image of affineToFull is an equivalence.

theorem isEquivalence_affineToFull_inverseImage
    (O : Sheaf (associatedTopology B S hS p τ) CommRingCat.{max u v w}) :
    (affineToFull B S hS p τ J O).toToposHom.inverseImage.IsEquivalence

AlgebraicGeometry.Stack.affineToFullFppf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/AffineRingedTopos.lean, line 224. The attribute's comment: “the fppf topology”.

The inclusion of the affine subsite of the associated fppf site of a category fibred in groupoids, as a morphism of ringed topoi for the lifted structure sheaf of Stacks 06TV.

noncomputable def affineToFullFppf (hp : p.IsFiberedInGroupoids) :
    letI : (AffineCategory.inclusion B S hS p).IsDenseSubsite
        (associatedAffineTopology B S hS p (BigAffineFppf.topology B S hS))
        (associatedTopology B S hS p B.topology) :=
      isDenseSubsite_affineInclusion_fppf B S hS p hp
    AlgebraicGeometry.RingedToposHom
      (affineRingedTopos B S hS p B.topology (BigAffineFppf.topology B S hS)
        (liftedStructureSheaf B S hS p B.topology hp le_rfl))
      (fullRingedTopos B S hS p B.topology
        (liftedStructureSheaf B S hS p B.topology hp le_rfl))

AlgebraicGeometry.Stack.affineToFullZariski, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/AffineRingedToposTopologies.lean, line 135. The attribute's comment: “the Zariski topology”.

The inclusion of the affine subsite of the associated Zariski site of a category fibred in groupoids, as a morphism of ringed topoi for the lifted structure sheaf of Stacks 06TV. Its inverse image is an equivalence and its structure morphism is an isomorphism, by AlgebraicGeometry.Stack.isEquivalence_affineToFull_inverseImage and AlgebraicGeometry.Stack.isIso_affineToFull_fSharpInverseImage.

noncomputable def affineToFullZariski (hp : p.IsFiberedInGroupoids) :
    letI : (AffineCategory.inclusion B S hS p).IsDenseSubsite
        (associatedAffineTopology B S hS p
          (BigAffineZariski.topology B.toBigZariskiSite S hS))
        (associatedTopology B S hS p B.zariskiTopology) :=
      isDenseSubsite_affineInclusion_zariski B S hS p hp
    AlgebraicGeometry.RingedToposHom
      (affineRingedTopos B S hS p B.zariskiTopology
        (BigAffineZariski.topology B.toBigZariskiSite S hS)
        (liftedStructureSheaf B S hS p B.zariskiTopology hp (zariskiTopology_le_topology B)))
      (fullRingedTopos B S hS p B.zariskiTopology
        (liftedStructureSheaf B S hS p B.zariskiTopology hp
          (zariskiTopology_le_topology B)))

AlgebraicGeometry.Stack.affineToFullEtale, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/AffineRingedToposTopologies.lean, line 159. The attribute's comment: “the étale topology”.

The inclusion of the affine subsite of the associated étale site of a category fibred in groupoids, as a morphism of ringed topoi for the lifted structure sheaf of Stacks 06TV. Its inverse image is an equivalence and its structure morphism is an isomorphism, by AlgebraicGeometry.Stack.isEquivalence_affineToFull_inverseImage and AlgebraicGeometry.Stack.isIso_affineToFull_fSharpInverseImage.

noncomputable def affineToFullEtale (hp : p.IsFiberedInGroupoids) :
    letI : (AffineCategory.inclusion B S hS p).IsDenseSubsite
        (associatedAffineTopology B S hS p (BigAffineEtale.topology B.toBigEtaleSite S hS))
        (associatedTopology B S hS p B.etaleTopology) :=
      isDenseSubsite_affineInclusion_etale B S hS p hp
    AlgebraicGeometry.RingedToposHom
      (affineRingedTopos B S hS p B.etaleTopology
        (BigAffineEtale.topology B.toBigEtaleSite S hS)
        (liftedStructureSheaf B S hS p B.etaleTopology hp (etaleTopology_le_topology B)))
      (fullRingedTopos B S hS p B.etaleTopology
        (liftedStructureSheaf B S hS p B.etaleTopology hp (etaleTopology_le_topology B)))

AlgebraicGeometry.Stack.affineToFullSmooth, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/AffineRingedToposTopologies.lean, line 180. The attribute's comment: “the smooth topology”.

The inclusion of the affine subsite of the associated smooth site of a category fibred in groupoids, as a morphism of ringed topoi for the lifted structure sheaf of Stacks 06TV. Its inverse image is an equivalence and its structure morphism is an isomorphism, by AlgebraicGeometry.Stack.isEquivalence_affineToFull_inverseImage and AlgebraicGeometry.Stack.isIso_affineToFull_fSharpInverseImage.

noncomputable def affineToFullSmooth (hp : p.IsFiberedInGroupoids) :
    letI : (AffineCategory.inclusion B S hS p).IsDenseSubsite
        (associatedAffineTopology B S hS p (BigAffineSmooth.topology B.toBigSmoothSite S hS))
        (associatedTopology B S hS p B.smoothTopology) :=
      isDenseSubsite_affineInclusion_smooth B S hS p hp
    AlgebraicGeometry.RingedToposHom
      (affineRingedTopos B S hS p B.smoothTopology
        (BigAffineSmooth.topology B.toBigSmoothSite S hS)
        (liftedStructureSheaf B S hS p B.smoothTopology hp (smoothTopology_le_topology B)))
      (fullRingedTopos B S hS p B.smoothTopology
        (liftedStructureSheaf B S hS p B.smoothTopology hp (smoothTopology_le_topology B)))

AlgebraicGeometry.Stack.affineToFullSyntomic, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/AffineRingedToposTopologies.lean, line 201. The attribute's comment: “the syntomic topology”.

The inclusion of the affine subsite of the associated syntomic site of a category fibred in groupoids, as a morphism of ringed topoi for the lifted structure sheaf of Stacks 06TV. Its inverse image is an equivalence and its structure morphism is an isomorphism, by AlgebraicGeometry.Stack.isEquivalence_affineToFull_inverseImage and AlgebraicGeometry.Stack.isIso_affineToFull_fSharpInverseImage.

noncomputable def affineToFullSyntomic (hp : p.IsFiberedInGroupoids) :
    letI : (AffineCategory.inclusion B S hS p).IsDenseSubsite
        (associatedAffineTopology B S hS p
          (BigAffineSyntomic.topology B.toBigSyntomicSite S hS))
        (associatedTopology B S hS p B.syntomicTopology) :=
      isDenseSubsite_affineInclusion_syntomic B S hS p hp
    AlgebraicGeometry.RingedToposHom
      (affineRingedTopos B S hS p B.syntomicTopology
        (BigAffineSyntomic.topology B.toBigSyntomicSite S hS)
        (liftedStructureSheaf B S hS p B.syntomicTopology hp
          (syntomicTopology_le_topology B)))
      (fullRingedTopos B S hS p B.syntomicTopology
        (liftedStructureSheaf B S hS p B.syntomicTopology hp
          (syntomicTopology_le_topology B)))

Sources

LeanAlgebraicGeometry.Stack.associatedAffineChaoticTopology · AlgebraicGeometry.Stack.sheafAssociatedAffineChaoticEquivalence · AlgebraicGeometry.Stack.AffineCategory · AlgebraicGeometry.Stack.AffineCategory.isStronglyCartesian_toAffine · AlgebraicGeometry.Stack.associatedAffineTopology · AlgebraicGeometry.Stack.generate_mem_associatedAffineTopology · AlgebraicGeometry.Stack.AffineCategory.isFiberedInGroupoids_toAffine · AlgebraicGeometry.Stack.AffineCategory.isCoverDense_inclusion

Section96.25 Quasi-coherent modules and affines #

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

Tag 0H0E, a lemma

Tag 0H0E in the Stacks Project.

AlgebraicGeometry.Stack.AffineCategory.tfae_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/QuasiCoherentModulesAndAffines.lean, line 210.

Stacks 0H0E. Let p : 𝒳 ⥤ (Sch/S)_{fppf} be a category fibred in groupoids and let 𝓕 be an 𝒪-module on 𝒳_{affine}, that is, a sheaf of modules on the chaotic ringed site (𝒳_{affine}, 𝒪) of Stacks 0H09 and 0H0D. The following are equivalent:

for every morphism x ⟶ x' of 𝒳_{affine} the map 𝓕(x') ⊗_{𝒪(x')} 𝒪(x) ⟶ 𝓕(x) is an isomorphism;

𝓕 is a quasi-coherent module on (𝒳_{affine}, 𝒪) in the sense of Stacks 03DL;

𝓕 is a sheaf for the Zariski topology on 𝒳_{affine} and a quasi-coherent module on (𝒳_{affine, Zar}, 𝒪);

the same for the étale topology;

the same for the smooth topology;

the same for the syntomic topology;

the same for the fppf topology;

𝓕 corresponds to a quasi-coherent module on 𝒳 via the equivalence of Stacks 0H0C: it is a sheaf for the fppf topology, and as such it is isomorphic to the restriction to 𝒳_{affine, fppf} of a quasi-coherent module on (𝒳_{fppf}, 𝒪_𝒳).

The equivalence of Stacks 0H0C is restriction along the affine inclusion, which on sheaves of modules with sections in the universe of the schemes is an equivalence by AlgebraicGeometry.Stack.AffineCategory.isEquivalence_moduleRestriction; condition (8) asks that 𝓕 lie in its image of the quasi-coherent modules.

theorem tfae_isQuasicoherent (hp : p.IsFiberedInGroupoids)
    (F : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (siteKindRingedSite B S hS p hp .fppf).chaotic.O)) :
    [∀ ⦃x x' : AffineCategory B S hS p⦄ (f : x ⟶ x'),
        IsIso (Stacks.SheafOfModules.canonicalMap
          (siteKindRingedSite B S hS p hp .fppf).chaotic F f),
      F.IsQuasicoherentOnSite,
      ∃ h : Presheaf.IsSheaf (siteKindRingedSite B S hS p hp .zariski).J F.val.presheaf,
        (⟨F.val, h⟩ : SheafOfModules.{u}
          (Stacks.SheafOfModules.Tensor.ringSheaf
            (siteKindRingedSite B S hS p hp .zariski).O)).IsQuasicoherentOnSite,
      ∃ h : Presheaf.IsSheaf (siteKindRingedSite B S hS p hp .etale).J F.val.presheaf,
        (⟨F.val, h⟩ : SheafOfModules.{u}
          (Stacks.SheafOfModules.Tensor.ringSheaf
            (siteKindRingedSite B S hS p hp .etale).O)).IsQuasicoherentOnSite,
      ∃ h : Presheaf.IsSheaf (siteKindRingedSite B S hS p hp .smooth).J F.val.presheaf,
        (⟨F.val, h⟩ : SheafOfModules.{u}
          (Stacks.SheafOfModules.Tensor.ringSheaf
            (siteKindRingedSite B S hS p hp .smooth).O)).IsQuasicoherentOnSite,
      ∃ h : Presheaf.IsSheaf (siteKindRingedSite B S hS p hp .syntomic).J F.val.presheaf,
        (⟨F.val, h⟩ : SheafOfModules.{u}
          (Stacks.SheafOfModules.Tensor.ringSheaf
            (siteKindRingedSite B S hS p hp .syntomic).O)).IsQuasicoherentOnSite,
      ∃ h : Presheaf.IsSheaf (siteKindRingedSite B S hS p hp .fppf).J F.val.presheaf,
        (⟨F.val, h⟩ : SheafOfModules.{u}
          (Stacks.SheafOfModules.Tensor.ringSheaf
            (siteKindRingedSite B S hS p hp .fppf).O)).IsQuasicoherentOnSite,
      ∃ h : Presheaf.IsSheaf (siteKindRingedSite B S hS p hp .fppf).J F.val.presheaf,
        letI := isDenseSubsite_inclusion_siteKind B S hS p hp .fppf
        ∃ G : SheafOfModules.{u} (FibredSite.ringStructureSheafCore B S hS p hp .fppf),
          G.IsQuasicoherentOnSite ∧
            Nonempty ((Stacks.DenseSubsiteModules.moduleRestriction
              (siteKindRingedSite B S hS p hp .fppf).J
              (BigFppfOver.associatedTopology B S hS p .fppf) (inclusion B S hS p)
              (FibredSite.ringStructureSheafCore B S hS p hp .fppf)).obj G ≅
              (⟨F.val, h⟩ : SheafOfModules.{u}
                (Stacks.SheafOfModules.Tensor.ringSheaf
                  (siteKindRingedSite B S hS p hp .fppf).O)))].TFAE

Tag 0H0F, a lemma

Tag 0H0F in the Stacks Project.

AlgebraicGeometry.Stack.tfae_locallyQuasicoherent_affine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/LocallyQuasiCoherentModulesAndAffines.lean, line 314.

Let p : 𝒳 ⥤ (Sch/S)_{fppf} be a category fibred in groupoids and 𝓕 a module over the structure sheaf 𝒪 of the affine subcategory 𝒳_{affine}. The following are equivalent:

for every arrow x ⟶ x' of 𝒳_{affine} lying over an étale morphism of affine schemes, the map 𝓕(x') ⊗_{𝒪(x')} 𝒪(x) ⟶ 𝓕(x) is an isomorphism;

𝓕 is a sheaf for the étale topology on 𝒳_{affine} and, for every object x of 𝒳_{affine}, the restriction x^*𝓕|_{U_{affine, étale}} to the small affine étale site of U = p(x) is quasi-coherent;

𝓕 corresponds to a locally quasi-coherent module on 𝒳 via the equivalence of Stacks 0H0C for the étale topology: it is isomorphic to the restriction to 𝒳_{affine} of a locally quasi-coherent module 𝓖 on 𝒳.

theorem tfae_locallyQuasicoherent_affine
    (F : PresheafOfModules.{u} (affineStructurePresheaf B S hS p)) :
    List.TFAE [
      ∀ ⦃x x' : AffineCategory B S hS p⦄ (f : x ⟶ x'),
        Etale ((p ⋙ BigFppfOver.toScheme B S hS).map f.hom) →
          IsIso (restrictionBaseChange.{v, w, u, u}
            (R := affineStructureCommPresheaf B S hS p) F f.op),
      Presheaf.IsSheaf
          (associatedAffineTopology B S hS p (BigAffineEtale.topology B.toBigEtaleSite S hS))
          F.presheaf ∧
        ∀ x : AffineCategory B S hS p,
          ∃ hM : Presheaf.IsSheaf
              (SmallAffineEtale.topology E (p.obj x.obj).left.1 (contains_base B E h S hS p x.obj))
              (affineChartModule B E h S hS p hp x F).presheaf,
            (⟨affineChartModule B E h S hS p hp x F, hM⟩ : SheafOfModules.{u}
              (Stacks.SheafOfModules.Tensor.ringSheaf
                (smallAffineEtaleRingedSite E (p.obj x.obj).left.1
                  (contains_base B E h S hS p x.obj)).O)).IsQuasicoherentOnSite,
      ∃ G : PresheafOfModules.{u}
          (ringStructureSheafCore B S hS p hp (etaleTopology B) (etaleTopology_le_topology B)).obj,
        IsLocallyQuasicoherent B E h S hS p hp G ∧
          Nonempty ((PresheafOfModules.pushforward₀ (AffineCategory.inclusion B S hS p) _).obj G ≅
            F)]

Sources

LeanAlgebraicGeometry.Stack.AffineCategory.tfae_isQuasicoherent · AlgebraicGeometry.Stack.tfae_locallyQuasicoherent_affine

Section96.26 Quasi-coherent objects in the derived category #

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

Tag 0H0H, a definition

Tag 0H0H in the Stacks Project.

AlgebraicGeometry.Stack.quasiCoherentDerived, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/QuasiCoherentDerivedCategory.lean, line 159.

The triangulated category of quasi-coherent objects in the derived category of a category p : 𝒳 ⥤ (Sch/S)_{fppf} over the big fppf category of S:

QC(𝒳) = QC(𝒳_{affine}, O),

the full subcategory of D(𝒳_{affine}, O) of the objects K such that for every arrow U → V of 𝒳_{affine} the canonical map RΓ(V, K) ⊗^L_{O(V)} O(U) ⟶ RΓ(U, K) is an isomorphism, where 𝒳_{affine} is the associated affine site of Stacks 0H09 with its chaotic topology and O is the structure sheaf of 𝒳 restricted to it.

abbrev quasiCoherentDerived : Type _

Tag 0H0I, a lemma

Tag 0H0I in the Stacks Project.

AlgebraicGeometry.Stack.isQuasicoherentOnSite_affineHomologySheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/QuasiCoherentDerivedTopCohomology.lean, line 166.

Stacks 0H0I. Let p : 𝒳 ⥤ (Sch/S)_{fppf} be a category fibred in groupoids, let M be an object of the triangulated category QC(𝒳) of Stacks 0H0H, and let b ∈ ℤ be such that H^i(M) = 0 for all i > b. Then H^b(M) is a quasi-coherent module on the ringed site (𝒳_{affine}, O), in the sense of Stacks 0H0E.

theorem isQuasicoherentOnSite_affineHomologySheaf
    (M : quasiCoherentDerived.{u, v, w, t} B S hS p) (b : ℤ)
    (hvan : ∀ i : ℤ, b < i → IsZero ((DerivedCategory.homologyFunctor
      (PresheafOfModules.{max v w u t} (affineStructurePresheaf B S hS p)) i).obj M.obj)) :
    (affineHomologySheaf.{u, v, w, t} B S hS p M.obj b).IsQuasicoherentOnSite

Tag 0H0J, a lemma

Tag 0H0J in the Stacks Project.

AlgebraicGeometry.Stack.isLocallyKFlatAcyclic_affineEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/QuasiCoherentDerivedComparison.lean, line 151. The attribute's comment: “ε : 𝒳_{affine,étale} ⟶ 𝒳_{affine} satisfies the assumptions of Stacks 0GZS: hypothesis (2), the target being the chaotic site by construction”.

Stacks 0H0J, hypothesis (2) of Stacks 0GZS. Let p : 𝒳 ⥤ (Sch/S)_{fppf} be a category fibred in groupoids and ε : (𝒳_{affine, étale}, O) ⟶ (𝒳_{affine}, O) the comparison morphism to the associated affine site with its chaotic topology. For every object x of 𝒳_{affine} and every K-flat complex M^• of O(x)-modules the canonical map M^• ⟶ RΓ((𝒳_{affine, étale}/x), (M^• ⊗_{O(x)} O_x)^#) is a quasi-isomorphism. (Hypothesis (1) of Stacks 0GZS, that the target topology is chaotic, is the construction of ε: modules on the chaotic site are presheaves of modules.)

theorem isLocallyKFlatAcyclic_affineEtale :
    IsLocallyKFlatAcyclic.{t}
      (Stacks.SheafOfModules.Tensor.ringSheaf
        (AffineCategory.siteKindRingedSite B S hS p hp .etale).O)
      (affineStructurePresheaf_comm B S hS p)

AlgebraicGeometry.Stack.affineEtaleQuasiCoherentEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/QuasiCoherentDerivedComparison.lean, line 167. The attribute's comment: “ε : 𝒳_{affine,étale} ⟶ 𝒳_{affine} satisfies the conclusions of Stacks 0GZS: ε^ and Rε_ are mutually quasi-inverse equivalences between QC(𝒳) and the objects K of D(𝒳_{affine,étale}, O) with Rε_*K in QC(𝒳)”.

Stacks 0H0J, the conclusion of Stacks 0GZS. For a category fibred in groupoids p : 𝒳 ⥤ (Sch/S)_{fppf} and the comparison ε : (𝒳_{affine, étale}, O) ⟶ (𝒳_{affine}, O), ε^* and Rε_* are mutually quasi-inverse equivalences between QC(𝒳) (Stacks 0H0H) and the full subcategory of D(𝒳_{affine, étale}, O) of the objects K with Rε_*K in QC(𝒳). The functor of the equivalence is ε^* and its inverse is Rε_*, both on the nose (AlgebraicGeometry.Stack.affineQuasiCoherentEquivalence_functor and _inverse).

def affineEtaleQuasiCoherentEquivalence :
    quasiCoherentDerived.{u, v, w, t} B S hS p ≌
      (pushforwardProperty.{t}
        (Stacks.SheafOfModules.Tensor.ringSheaf
          (AffineCategory.siteKindRingedSite B S hS p hp .etale).O)
        (IsQuasiCoherentObject.{u, v, w, t} B S hS p)).FullSubcategory

Tag 0H0K, a proposition

Tag 0H0K in the Stacks Project.

AlgebraicGeometry.Stack.representableQuasiCoherentDerivedEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/RepresentableQC/Equivalence.lean, line 112. The attribute's comment: “QC(𝒳) is canonically equivalent to D_QCoh(O_X) for 𝒳 represented by an algebraic space X”.

Stacks 0H0K. Let p : 𝒳 ⥤ (Sch/S)_{fppf} be a category fibred in groupoids, represented by the algebraic space F through the equivalence e over the site between 𝒳 and the category of elements of F (Stacks 04SV). Then QC(𝒳) (Stacks 0H0H) is canonically equivalent to D_QCoh(O_F) (Stacks 071X), with modules in the universe max v w u t.

The equivalence is the composite of the three equivalences of the source's proof, on the single-universe lifts X↑ of 𝒳_{affine, étale} and Y↑ of F_{affine, étale}: ε^* from QC(𝒳) onto the objects K of D(X↑) with Rε_*K cartesian (Stacks 0H0J, 0GZS); the direct image f_* along the morphism of ringed sites f : X↑ ⟶ Y↑ given by the affine étale charts of F (Stacks 073M), inverse to the derived pullback Lf^* on the 0GZS subcategories (the argument of Stacks 09J1); and the identification of the 0GZS subcategory of D(Y↑) with D_QCoh(O_F) (Stacks 0H0J, 0H06, 03DX).

def representableQuasiCoherentDerivedEquivalence :
    quasiCoherentDerived.{u, v, w, t} B S hS p ≌
      Space.QuasicoherentDerivedCategory.{u, max v w u t} B S hS F hF

Tag 0H0L, a proposition

Tag 0H0L in the Stacks Project.

AlgebraicGeometry.FormalSpace.quasiCoherentDerivedEquivalenceDerivedComplete, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/FormalSpectrumQuasiCoherentDerived.lean, line 237. The attribute's comment: “QC(𝒳) ≌ D_comp(A, I) for 𝒳 the category fibred in sets of Spf(A), A an adic Noetherian topological S-algebra with ideal of definition I”.

Stacks 0H0L. Let S be a scheme and X = Spf(A), where A is an adic Noetherian topological S-algebra with ideal of definition I (More on Algebra, Definition 07E8; Formal Spaces, Definition 0AIF). Let p : 𝒳 → (Sch/S)_{fppf} be the category fibred in sets associated to the functor X (Categories, Example 04TM). Then QC(𝒳) (Definition 0H0H) is equivalent to the category D_comp(A, I) of objects of D(A) which are derived complete with respect to I.

The equivalence is constructed: if the powers of I stabilize, I^{N+1} = I^{N+2}, then I^{N+1} = 0, Spec(A) = Spec(A/I^{N+1}) is a final object of 𝒳_{affine} and the equivalence is RΓ(Spec(A), -) (Stacks 0H0R), every object of D(A) being derived complete; otherwise it is the composite of the source's proof, qcEquivalenceOfStrict. Here D(A) is the derived category of A-modules in the universe max (u + 1) t of the modules of QC(𝒳), in any model.

def quasiCoherentDerivedEquivalenceDerivedComplete :
    Stack.quasiCoherentDerived.{u, u + 1, u, t} B S hS (formalSpectrumProjection D) ≌
      ObjectProperty.FullSubcategory
        (fun K : DerivedCategory (ModuleCat.{max (u + 1) t} A) => IsDerivedComplete I K)

Tag 0H0X, a lemma

Tag 0H0X in the Stacks Project.

AlgebraicGeometry.Stack.isLocallyKFlatAcyclic_affineFppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/QuasiCoherentDerivedComparison.lean, line 186. The attribute's comment: “ε : 𝒳_{affine,fppf} ⟶ 𝒳_{affine} satisfies the assumptions of Stacks 0GZS: hypothesis (2), the target being the chaotic site by construction”.

Stacks 0H0X, hypothesis (2) of Stacks 0GZS. Let p : 𝒳 ⥤ (Sch/S)_{fppf} be a category fibred in groupoids and ε : (𝒳_{affine, fppf}, O) ⟶ (𝒳_{affine}, O) the comparison morphism to the associated affine site with its chaotic topology. For every object x of 𝒳_{affine} and every K-flat complex M^• of O(x)-modules the canonical map M^• ⟶ RΓ((𝒳_{affine, fppf}/x), (M^• ⊗_{O(x)} O_x)^#) is a quasi-isomorphism. (Hypothesis (1) of Stacks 0GZS, that the target topology is chaotic, is the construction of ε: modules on the chaotic site are presheaves of modules.)

theorem isLocallyKFlatAcyclic_affineFppf :
    IsLocallyKFlatAcyclic.{t}
      (Stacks.SheafOfModules.Tensor.ringSheaf
        (AffineCategory.siteKindRingedSite B S hS p hp .fppf).O)
      (affineStructurePresheaf_comm B S hS p)

AlgebraicGeometry.Stack.affineFppfQuasiCoherentEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/QuasiCoherentDerivedComparison.lean, line 202. The attribute's comment: “ε : 𝒳_{affine,fppf} ⟶ 𝒳_{affine} satisfies the conclusions of Stacks 0GZS: ε^ and Rε_ are mutually quasi-inverse equivalences between QC(𝒳) and the objects K of D(𝒳_{affine,fppf}, O) with Rε_*K in QC(𝒳)”.

Stacks 0H0X, the conclusion of Stacks 0GZS. For a category fibred in groupoids p : 𝒳 ⥤ (Sch/S)_{fppf} and the comparison ε : (𝒳_{affine, fppf}, O) ⟶ (𝒳_{affine}, O), ε^* and Rε_* are mutually quasi-inverse equivalences between QC(𝒳) (Stacks 0H0H) and the full subcategory of D(𝒳_{affine, fppf}, O) of the objects K with Rε_*K in QC(𝒳). The functor of the equivalence is ε^* and its inverse is Rε_*, both on the nose (AlgebraicGeometry.Stack.affineQuasiCoherentEquivalence_functor and _inverse).

def affineFppfQuasiCoherentEquivalence :
    quasiCoherentDerived.{u, v, w, t} B S hS p ≌
      (pushforwardProperty.{t}
        (Stacks.SheafOfModules.Tensor.ringSheaf
          (AffineCategory.siteKindRingedSite B S hS p hp .fppf).O)
        (IsQuasiCoherentObject.{u, v, w, t} B S hS p)).FullSubcategory

Sources

LeanAlgebraicGeometry.Stack.quasiCoherentDerived · AlgebraicGeometry.Stack.isQuasicoherentOnSite_affineHomologySheaf · AlgebraicGeometry.Stack.isLocallyKFlatAcyclic_affineEtale · AlgebraicGeometry.Stack.affineEtaleQuasiCoherentEquivalence · AlgebraicGeometry.Stack.representableQuasiCoherentDerivedEquivalence · AlgebraicGeometry.FormalSpace.quasiCoherentDerivedEquivalenceDerivedComplete · AlgebraicGeometry.Stack.isLocallyKFlatAcyclic_affineFppf · AlgebraicGeometry.Stack.affineFppfQuasiCoherentEquivalence

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

96.16 Cohomology to 96.26 Quasi-coherent objects in…

Section96.16 Cohomology#

Tag 075F, a lemma

Sources

Section96.17 Injective sheaves#

Tag 06WX, a lemma

Tag 06WY, a lemma

Tag 06WZ, a lemma

Tag 06X0, a lemma

Tag 06X1, a lemma

Tag 06X2, a lemma

Sources

Section96.18 The Čech complex#

Tag 06X3, the section

Tag 06X5, a lemma

Tag 06X6, a lemma

Sources

Section96.19 The relative Čech complex#

Tag 06X8, a remark

Tag 06X9, a lemma

Tag 06XA, a lemma

Tag 06XB, a remark

Tag 06XC, a lemma

Tag 06XD, a lemma

Tag 06XE, a proposition

Tag 06XF, a lemma

Tag 06XG, a lemma

Tag 06XH, a lemma

Tag 072D, a lemma

Tag 072E, a lemma

Sources

Section96.20 Cohomology on algebraic stacks#

Tag 06XJ, a proposition

Sources

Section96.21 Higher direct images and algebraic stacks#

Tag 072G, a proposition

Tag 075G, a lemma

Tag 075H, a lemma

Sources

Section96.22 Comparison#

Tag 075L, a lemma

Tag 075N, a lemma

Tag 075P, a lemma

Sources

Section96.23 Change of topology#

Tag 076T, a lemma

Tag 075R, a lemma

Tag 07AK, a lemma

Sources

Section96.24 Restricting to affines#

Tag 0H09, a definition

Tag 0H0A, a definition

Tag 0H0B, a lemma

Tag 0H0C, an equation

Sources

Section96.25 Quasi-coherent modules and affines#

Tag 0H0E, a lemma

Tag 0H0F, a lemma

Sources

Section96.26 Quasi-coherent objects in the derived category#

Tag 0H0H, a definition

Tag 0H0I, a lemma

Tag 0H0J, a lemma

Tag 0H0K, a proposition

Tag 0H0L, a proposition

Tag 0H0X, a lemma

Sources

Section96.16 Cohomology #

Section96.17 Injective sheaves #

Section96.18 The Čech complex #

Section96.19 The relative Čech complex #

Section96.20 Cohomology on algebraic stacks #

Section96.21 Higher direct images and algebraic stacks #

Section96.22 Comparison #

Section96.23 Change of topology #

Section96.24 Restricting to affines #

Section96.25 Quasi-coherent modules and affines #

Section96.26 Quasi-coherent objects in the derived category #