69.3 Higher direct images to 69.15 Limits of coherent modules

Section69.3 Higher direct images#

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

Tag 071Z, an equation

Tag 071Z in the Stacks Project.

AlgebraicGeometry.Space.isIso_moduleHigherPushforwardEtaleBaseChangeComparison_etaleSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleEtaleBaseChangeHFace.lean, line 751. The attribute's comment: “for the CANONICAL comparison map and for an ÉTALE square: g étale, not merely flat, so this is a special case of Stacks 073K part (1) and not that tag. The existing 071Z attribute carries an isomorphism with the right endpoints that is not identified with the canonical map”.

Stacks 071Z read as a statement about the canonical maps, in the étale case. For a cartesian square of algebraic spaces whose bottom arrow g is étale, the canonical base-change comparison

(R^n f_*F)|_{Y'} ⟶ R^n f'_*(F|_{X'})

is an isomorphism in every degree n.

This is AlgebraicGeometry.Space.isIso_moduleHigherPushforwardEtaleBaseChangeComparison with its underived hypothesis discharged by AlgebraicGeometry.Space.isIso_moduleEtaleBaseChangeComparison. The injective-preservation input of the comparison map — part (1) of Stacks 03F3 for étale restriction of modules along i, which is étale by Stacks 03FU — is AlgebraicGeometry.Space.preservesInjectiveObjects_etaleModulePullback and is used, not assumed. So nothing is assumed here beyond the cartesian square and the étaleness of g.

This is the étale case and not Stacks 073K, part (1), for the same reason as the underived statement: hg is AlgebraicGeometry.Space.IsEtale, and étale is strictly stronger than the flatness of g that Stacks 073K assumes.

theorem isIso_moduleHigherPushforwardEtaleBaseChangeComparison_etaleSquare
    (sq : IsPullback i f' f g) (hg : IsEtale B S hS g.hom) (n : ℕ) :
    IsIso (moduleHigherPushforwardEtaleBaseChangeComparison B S hS i f' f g sq hg
      (preservesInjectiveObjects_etaleModulePullback B S hS i
        (isEtale_of_isPullback B S hS f' i g f sq.flip hg)) n)

AlgebraicGeometry.Space.moduleHigherPushforwardChartBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleHigherPushforwardEtaleBaseChange.lean, line 187.

For a representable morphism f : X ⟶ Y of algebraic spaces and an étale scheme chart V of Y, the higher direct images of 𝒪_X-modules commute with restriction to the chart:

R^n f'_*(F|_U) = (R^n f_*F)|_V,

naturally in the 𝒪_X-module F, where U = V ×_Y X is the pullback chart of X and f' : U ⟶ V is the base change of f. The morphism f is not assumed quasi-compact or quasi-separated, V ⟶ Y is not assumed surjective and F is not assumed quasi-coherent.

noncomputable def moduleHigherPushforwardChartBaseChangeIso (f : X ⟶ Y)
    (hf : yoneda.relativelyRepresentable f.hom) (V : SmallEtale B S hS Y.1) (n : ℕ) :
    have := hasInjectiveResolutions_modules B S hS X.1 X.2
    have := hasInjectiveResolutions_modules B S hS
      (chartSpace B S hS X ((smallBaseChange B S hS f hf).obj V)).1
      (chartSpace B S hS X ((smallBaseChange B S hS f hf).obj V)).2
    etaleModulePullback B S hS
          (chartToSpace B S hS X ((smallBaseChange B S hS f hf).obj V))
          (isEtale_chartToSpace B S hS X ((smallBaseChange B S hS f hf).obj V)) ⋙
        (modulePushforward B S hS (smallBaseChangeChartMap B S hS f hf V)).rightDerived n ≅
      (modulePushforward B S hS f).rightDerived n ⋙
        etaleModulePullback B S hS (chartToSpace B S hS Y V)
          (isEtale_chartToSpace B S hS Y V)

Tag 0720, a lemma

Tag 0720 in the Stacks Project.

AlgebraicGeometry.Space.isQuasicoherentOnSite_rightDerived_modulePushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/HigherPushforwardQuasicoherent.lean, line 149. The attribute's comment: “the reduction to an affine base; the affine case is the hypothesis haffine”.

Stacks 0720. Let f : X ⟶ Y be a quasi-compact and quasi-separated morphism of algebraic spaces over a scheme S, and let F be a quasi-coherent 𝒪_X-module on the small étale site of X. Then the higher direct image R^i f_*F is quasi-coherent for every i.

The affine-base case of the source's proof is the hypothesis haffine, and the injective-preservation half of Stacks 03F3 for the chart base changes of f is the hypothesis h03F3; everything else is the source's reduction to an affine base, by Stacks 03M0, condition (4), and the higher-direct-image clause of Stacks 03LX, with the hypotheses of the affine case supplied from those of f by Stacks 03HF and Stacks 03KL, part (3).

theorem isQuasicoherentOnSite_rightDerived_modulePushforward {X Y : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (hfqc : IsQuasiCompact B S hS f.hom) (hfqs : IsQuasiSeparated B S hS f.hom)
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite] (i : ℕ)
    (h03F3 : ∀ V : SmallEtale B S hS Y.1,
      (chartBaseChangeModulePullback B S hS f V).PreservesInjectiveObjects)
    (haffine : AffineTargetHigherPushforwardQuasicoherent B S hS i) :
    have := hasInjectiveResolutions_modules B S hS X.1 X.2
    (((modulePushforward B S hS f).rightDerived i).obj F).IsQuasicoherentOnSite

AlgebraicGeometry.Space.isQuasicoherentOnSite_rightDerived_modulePushforward', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/HigherPushforwardQuasicoherentUnconditional.lean, line 80.

Stacks 0720. Let f : X ⟶ Y be a quasi-compact and quasi-separated morphism of algebraic spaces over a scheme S, and let F be a quasi-coherent 𝒪_X-module on the small étale site of X. Then the higher direct image R^i f_*F is quasi-coherent for every i.

theorem isQuasicoherentOnSite_rightDerived_modulePushforward' {X Y : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (hfqc : IsQuasiCompact B S hS f.hom) (hfqs : IsQuasiSeparated B S hS f.hom)
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite] (i : ℕ) :
    have := hasInjectiveResolutions_modules B S hS X.1 X.2
    (((modulePushforward B S hS f).rightDerived i).obj F).IsQuasicoherentOnSite

Tag 08EX, a lemma

Tag 08EX in the Stacks Project.

AlgebraicGeometry.Space.cohomologyAffineChartIsoSectionsHigherDirectImage, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/HigherDirectImageSectionsOverAffineChart.lean, line 92. The attribute's comment: “the source's statement and both steps of its proof at the source's own data: f quasi-compact and quasi-separated, F quasi-coherent, V an affine object of Y_etale. The cohomology over V times_Y X is read as the right derived functor of the composite Gamma(V, f'_* -), as in the library's form of Stacks 0D2U”.

Stacks 08EX. Let f : X ⟶ Y be a quasi-compact and quasi-separated morphism of algebraic spaces over S, let F be a quasi-coherent 𝒪_X-module and let V be an affine étale chart of Y. Then the cohomology of F over U = V ×_Y X agrees with the module of sections over V of the degree-q higher direct image R^q f_*F, in every degree:

H^q(V ×_Y X, F) = H^0(V, R^q f_*F).

def cohomologyAffineChartIsoSectionsHigherDirectImage (f : X ⟶ Y)
    (hfqc : IsQuasiCompact B S hS f.hom) (hfqs : IsQuasiSeparated B S hS f.hom)
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : F.IsQuasicoherentOnSite)
    (V : SmallEtale B S hS Y.1) (hV : IsAffineChart B S hS Y.1 V) (q : ℕ) :
    have := hasInjectiveResolutions_modules B S hS X.1 X.2
    have := hasInjectiveResolutions_modules B S hS (chartBaseChangeSpace B S hS f V).1
      (chartBaseChangeSpace B S hS f V).2
    have := enoughInjectives_modules B S hS (chartBaseChangeTarget B S hS V).1
      (chartBaseChangeTarget B S hS V).2
    ((modulePushforward B S hS (chartBaseChangeProjection B S hS f V) ⋙
            globalSectionsFunctor.{u + 1, u, u, u}
              ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS
                (chartBaseChangeTarget B S hS V).1
                (chartBaseChangeTarget B S hS V).2).O))).rightDerived q).obj
        ((chartBaseChangeModulePullback B S hS f V).obj F) ≅
      (globalSectionsFunctor.{u + 1, u, u, u}
          ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS
            (chartBaseChangeTarget B S hS V).1
            (chartBaseChangeTarget B S hS V).2).O))).obj
        ((etaleModulePullback B S hS (chartToSpace B S hS Y V)
            (isEtale_chartToSpace B S hS Y V)).obj
          (((modulePushforward B S hS f).rightDerived q).obj F))

AlgebraicGeometry.Space.cohomologyChartIsoSectionsHigherDirectImage, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/HigherDirectImageSectionsOverChart.lean, line 215. The attribute's comment: “both steps of the source's proof, with its three citations carried as named hypotheses -- h072Z is Stacks 072Z via Stacks 0731(3), hcoh is Stacks 0720 together with Stacks 01XB read on the small etale site (Stacks 03DW), and h03F3 is Stacks 03F3(1) for the etale morphism V times_Y X -> X; the cohomology over V times_Y X is read as the right derived functor of the composite Gamma(V, f'_* -)”.

Stacks 08EX. Let f : X ⟶ Y be a morphism of algebraic spaces over S, let F be an 𝒪_X-module and let V be an étale scheme chart of Y. Then the cohomology of F over U = V ×_Y X agrees with the module of sections over V of the degree-q higher direct image R^q f_*F, in every degree:

H^q(V ×_Y X, F) = H^0(V, R^q f_*F).

The right hand side is the restriction of R^q f_*F to the chart V, read through its global sections there, and the left hand side is the q-th right derived functor of Γ(V, f'_*−) for f' : U ⟶ V the base change of f. The proof is the source's: the higher-direct-image clause of Stacks 03LX identifies (R^q f_*F)|_V with R^q f'_*(F|_U), and the Leray spectral sequence of f' degenerates at E_2, which is AlgebraicGeometry.Space.globalSectionsRightDerivedIso.

Three hypotheses are carried, none of them part of this tag's own content: h072Z is Stacks 072Z through part (3) of Stacks 0731, hcoh is where the source invokes Stacks 0720 and Stacks 01XB — for an affine V and a quasi-coherent F along a quasi-compact and quasi-separated f it is exactly their conjunction — and h03F3 is the injective-preservation half of Stacks 03F3, part (1), which is discharged for a representable f by Stacks 071Z.

def cohomologyChartIsoSectionsHigherDirectImage (f : X ⟶ Y)
    (F : Modules.{u, u} B S hS X.1 X.2) (V : SmallEtale B S hS Y.1) (q : ℕ)
    (h03F3 : (chartBaseChangeModulePullback B S hS f V).PreservesInjectiveObjects)
    (h072Z : AcyclicPushforwardOfInjective B S hS (chartBaseChangeProjection B S hS f V))
    (hcoh : AcyclicHigherDirectImages B S hS (chartBaseChangeProjection B S hS f V)
      ((chartBaseChangeModulePullback B S hS f V).obj F)) :
    have := hasInjectiveResolutions_modules B S hS X.1 X.2
    have := hasInjectiveResolutions_modules B S hS (chartBaseChangeSpace B S hS f V).1
      (chartBaseChangeSpace B S hS f V).2
    have := enoughInjectives_modules B S hS (chartBaseChangeTarget B S hS V).1
      (chartBaseChangeTarget B S hS V).2
    ((modulePushforward B S hS (chartBaseChangeProjection B S hS f V) ⋙
            globalSectionsFunctor.{u + 1, u, u, u}
              ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS
                (chartBaseChangeTarget B S hS V).1
                (chartBaseChangeTarget B S hS V).2).O))).rightDerived q).obj
        ((chartBaseChangeModulePullback B S hS f V).obj F) ≅
      (globalSectionsFunctor.{u + 1, u, u, u}
          ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS (chartBaseChangeTarget B S hS V).1
            (chartBaseChangeTarget B S hS V).2).O))).obj
        ((etaleModulePullback B S hS (chartToSpace B S hS Y V)
            (isEtale_chartToSpace B S hS Y V)).obj
          (((modulePushforward B S hS f).rightDerived q).obj F))

Sources

• Section 69.3, Tag 071Y
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.isIso_moduleHigherPushforwardEtaleBaseChangeComparison_etaleSquare · AlgebraicGeometry.Space.moduleHigherPushforwardChartBaseChangeIso · AlgebraicGeometry.Space.isQuasicoherentOnSite_rightDerived_modulePushforward · AlgebraicGeometry.Space.isQuasicoherentOnSite_rightDerived_modulePushforward' · AlgebraicGeometry.Space.cohomologyAffineChartIsoSectionsHigherDirectImage · AlgebraicGeometry.Space.cohomologyChartIsoSectionsHigherDirectImage

Section69.4 Finite morphisms#

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

Tag 0A4K, a lemma

Tag 0A4K in the Stacks Project.

AlgebraicGeometry.Space.smallEtaleAbelianPushforward_exact_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePushforwardExact.lean, line 136. The attribute's comment: “exactness of f_*, the finite case”.

Stacks 0A4K, exactness, for a finite morphism. For a finite morphism f : X ⟶ Y of algebraic spaces over S the direct image on the abelian sheaves of the small étale sites is exact.

The source states this for an integral morphism, "integral (for example finite)"; that case is AlgebraicGeometry.Space.smallEtaleAbelianPushforward_exact_of_isIntegralHom. The step from surjections of sheaves of sets to exactness on abelian sheaves is Stacks 04DB, already available as Stacks.Topos.AbelianPushforward.abelianPushforward_exact, and the surjection statement is AlgebraicGeometry.Space.smallEtalePushforward_preservesEpimorphisms_of_isFinite.

theorem smallEtaleAbelianPushforward_exact_of_isFinite {X Y : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (hf : IsFinite B S hS f.hom) :
    exactFunctor (Sheaf (SmallEtale.topology B S hS X.obj) AddCommGrpCat.{u + 1})
      (Sheaf (SmallEtale.topology B S hS Y.obj) AddCommGrpCat.{u + 1})
      (Stacks.Topos.AbelianPushforward.abelianPushforward (SmallEtale.topology B S hS X.obj)
        (smallToposMorphism B S hS f))

AlgebraicGeometry.Space.smallEtaleAbelianPushforward_rightDerivedPlus_isZero_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePushforwardExact.lean, line 154. The attribute's comment: “vanishing of R^p f_* for p > 0, the finite case”. References: SGA 4 Vbis (4.3.4), “Remarque 4.3.4”; SGA 4½ Arcata (2.3.6), “more general”.

Stacks 0A4K, vanishing of the positive-degree higher direct images, for a finite morphism. For a finite morphism f : X ⟶ Y of algebraic spaces over S the right derived functors of the small étale direct image on abelian sheaves vanish in positive degree.

The integral case, which contains this one, is AlgebraicGeometry.Space.smallEtaleAbelianPushforward_rightDerivedPlus_isZero_of_isIntegralHom.

theorem smallEtaleAbelianPushforward_rightDerivedPlus_isZero_of_isFinite
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (hf : IsFinite B S hS f.hom)
    (F : Sheaf (SmallEtale.topology B S hS X.obj) AddCommGrpCat.{u + 1})
    (p : ℤ) (hp : 0 < p) :
    IsZero (((Stacks.Topos.AbelianPushforward.abelianPushforward
      (SmallEtale.topology B S hS X.obj)
      (smallToposMorphism B S hS f)).rightDerivedPlus p).obj F)

AlgebraicGeometry.Space.smallEtaleAbelianPushforward_exact_of_isIntegralHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralPushforwardExact.lean, line 112. The attribute's comment: “exactness of f_* for an integral morphism of algebraic spaces”.

Stacks 0A4K, exactness. For an integral morphism f : X ⟶ Y of algebraic spaces over S the direct image on the abelian sheaves of the small étale sites is exact.

The step from surjections of sheaves of sets to exactness on abelian sheaves is Stacks 04DB, available as Stacks.Topos.AbelianPushforward.abelianPushforward_exact, and the surjection statement is AlgebraicGeometry.Space.smallEtalePushforward_preservesEpimorphisms_of_isIntegralHom.

theorem smallEtaleAbelianPushforward_exact_of_isIntegralHom {X Y : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (hf : IsIntegralHom B S hS f.hom) :
    exactFunctor (Sheaf (SmallEtale.topology B S hS X.obj) AddCommGrpCat.{u + 1})
      (Sheaf (SmallEtale.topology B S hS Y.obj) AddCommGrpCat.{u + 1})
      (Stacks.Topos.AbelianPushforward.abelianPushforward (SmallEtale.topology B S hS X.obj)
        (smallToposMorphism B S hS f))

AlgebraicGeometry.Space.smallEtaleAbelianPushforward_rightDerivedPlus_isZero_of_isIntegralHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralPushforwardExact.lean, line 131. The attribute's comment: “vanishing of R^p f_* for p > 0 for an integral morphism of algebraic spaces”. References: SGA 4 VIII (5.6), “more general”; SGA 4 Vbis (4.3.4), “more general”; SGA 4½ Arcata (2.3.6), “more general”.

Stacks 0A4K, vanishing of the positive-degree higher direct images. For an integral morphism f : X ⟶ Y of algebraic spaces over S the right derived functors of the small étale direct image on abelian sheaves vanish in positive degree.

Given the exactness this is formal, by CategoryTheory.Functor.isZero_rightDerivedPlus_of_exact.

theorem smallEtaleAbelianPushforward_rightDerivedPlus_isZero_of_isIntegralHom
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (hf : IsIntegralHom B S hS f.hom)
    (F : Sheaf (SmallEtale.topology B S hS X.obj) AddCommGrpCat.{u + 1})
    (p : ℤ) (hp : 0 < p) :
    IsZero (((Stacks.Topos.AbelianPushforward.abelianPushforward
      (SmallEtale.topology B S hS X.obj)
      (smallToposMorphism B S hS f)).rightDerivedPlus p).obj F)

Tag 0DK3, a lemma

Tag 0DK3 in the Stacks Project.

AlgebraicGeometry.Space.finite_geometricLifts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteStalkPushforward.lean, line 180. The attribute's comment: “the lifts x₁, …, xₙ of y are finite in number”.

Stacks 0DK3, finiteness of the index set. A geometric point of the target of a finite morphism of algebraic spaces has finitely many lifts, so the product in the statement is a finite one.

The field spectrum of y is affine, so testing π against the section y produces an affine scheme V, a finite morphism V ⟶ Spec κ(y) and a pullback square exhibiting V as the base change of X. A lift of y therefore determines a section of that finite morphism, and AlgebraicGeometry.finite_lifts_of_isFinite makes those finite in number; the assignment is injective because the Yoneda embedding and the functor to schemes are faithful.

theorem finite_geometricLifts (hπ : IsFinite B S hS π.hom)
    (y : GeometricPoint B S hS Y.1) :
    Finite (GeometricLifts B S hS π y)

AlgebraicGeometry.Space.stalkPushforwardToProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteStalkPushforward.lean, line 301. The attribute's comment: “the canonical map (π_*F)_y ⟶ ∏ᵢ F_{xᵢ} over the lifts of y”.

The comparison map of Stacks 0DK3. For a finite morphism π : X ⟶ Y of algebraic spaces and a geometric point y of Y, the stalk at y of the direct image of a sheaf of sets F on X_étale maps canonically to the product of the stalks of F over the lifts of y, the component at a lift being AlgebraicGeometry.Space.stalkPushforwardComponent.

Stacks 0DK3 asserts that this map is bijective. That assertion is not proved for this map; it is proved for the comparison map CategoryTheory.GrothendieckTopology.Point.presheafFiberCompToPi as AlgebraicGeometry.Space.bijective_presheafFiberCompToPi_of_isFinite. What is proved about this map is its construction and its naturality in the sheaf.

def stalkPushforwardToProduct (y : GeometricPoint B S hS Y.1)
    (F : Sheaf (SmallEtale.topology B S hS X.1) (Type (u + 1))) :
    stalkSet y ((smallToposMorphism B S hS π).pushforward.obj F).obj →
      (∀ v : GeometricLifts B S hS π y,
        stalkSet (geometricLiftPoint B S hS π y v) F.obj)

AlgebraicGeometry.Space.stalkPushforwardToProduct_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteStalkPushforward.lean, line 323. The attribute's comment: “naturality of the comparison map in the sheaf”.

Stacks 0DK3 is natural in the sheaf. The comparison map commutes with the stalk maps induced by a morphism of sheaves of sets on X_étale.

theorem stalkPushforwardToProduct_natural (y : GeometricPoint B S hS Y.1)
    {F G : Sheaf (SmallEtale.topology B S hS X.1) (Type (u + 1))} (α : F ⟶ G)
    (z : stalkSet y ((smallToposMorphism B S hS π).pushforward.obj F).obj)
    (v : GeometricLifts B S hS π y) :
    stalkPushforwardToProduct B S hS π y G
        (stalkSetMap y ((smallToposMorphism B S hS π).pushforward.map α).hom z) v =
      stalkSetMap (geometricLiftPoint B S hS π y v) α.hom
        (stalkPushforwardToProduct B S hS π y F z v)

AlgebraicGeometry.Space.geometricLiftsEquivOfIsPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteStalkPushforward.lean, line 415. The attribute's comment: “the lifts of y are the lifts of v along the base change of π”.

Stacks 0DK3: the index set of the product is unchanged by base change. For a cartesian square

X' --i--> X
|         |
f'        π
↓         ↓
V --g---> Y

of algebraic spaces over S and a geometric point v of V, the lifts of v along f' are the lifts along π of the image of v in Y, the bijection sending a lift to its image under i.

This is the step with which the source's proof of Stacks 0DK3 begins, specialized to the index set: it replaces Y by an étale neighbourhood (V, v) of y and X by X ×_Y V, and the product over the lifts is the same product before and after exactly because of this bijection. Nothing is assumed of the four arrows beyond the square being cartesian, so neither finiteness of π nor étaleness of g is needed; the lifts of a geometric point are sections over its field spectrum, and sections over one object of the site of a cartesian square of algebraic spaces form a cartesian square of sets.

noncomputable def geometricLiftsEquivOfIsPullback {X' V : AlgebraicSpaces B S hS}
    {i : X' ⟶ X} {f' : X' ⟶ V} {g : V ⟶ Y} (sq : IsPullback i f' π g)
    (v : GeometricPoint B S hS V.1) :
    GeometricLifts B S hS f' v ≃ GeometricLifts B S hS π (geometricPointMap g.hom v)

AlgebraicGeometry.Space.bijective_presheafFiberCompToPi_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteStalkPushforwardProduct.lean, line 356.

Stacks 0DK3. Let π : X ⟶ Y be a finite morphism of algebraic spaces and y a geometric point of Y with lifts x₁, …, xₙ in X. For every sheaf of sets F on X_étale the stalk of the direct image π_*F at y is the product ∏ᵢ F_{xᵢ}: the canonical map CategoryTheory.GrothendieckTopology.Point.presheafFiberCompToPi, sending the germ at y of a section of F over a base-changed chart V ×_Y X to the family of its germs at the lifts, is bijective.

The direct image is that along base change of étale charts (π is representable, being finite, AlgebraicGeometry.Space.relativelyRepresentable_hom_of_isFinite), which is the direct image of the morphism of small étale topoi of Stacks 03G2, part (3) (AlgebraicGeometry.Space.smallEtaleRingedToposHom_representable); sheaves are valued in an arbitrary universe containing Type u, the universe of the fibres of the points AlgebraicGeometry.Space.etaleSitePoint at which stalks are taken.

theorem bijective_presheafFiberCompToPi_of_isFinite (hπ : IsFinite B S hS π.hom)
    (y : GeometricPoint B S hS Y.1)
    (F : Sheaf (SmallEtale.topology B S hS X.1) (Type (max u w))) :
    Function.Bijective (GrothendieckTopology.Point.presheafFiberCompToPi.{u, w, u, u + 1, u, u + 1}
      (smallBaseChange B S hS π (relativelyRepresentable_hom_of_isFinite B S hS π hπ))
      (etaleSitePoint B S hS Y.1 y Y.2)
      (fun v => etaleSitePoint B S hS X.1 (geometricLiftPoint B S hS π y v) X.2)
      (geometricFiberBaseChangeIso B S hS π (relativelyRepresentable_hom_of_isFinite B S hS π hπ) y)
      F.obj)

Tag 0DK4, a lemma

Tag 0DK4 in the Stacks Project.

AlgebraicGeometry.Space.smallEtaleRingedToposHomOfSharp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionModuleTensorPushforward.lean, line 181. The attribute's comment: “the morphism of ringed topoi determined by π, 𝒜, ℬ and φ”.

The morphism of ringed topoi of Stacks 04G0, f : (Sh(Z_étale), ℬ) ⟶ (Sh(X_étale), 𝒜): its underlying morphism of topoi is that of Stacks 03G2, part (3), and its structure map is φ.

No hypothesis on i enters, so this is equally the morphism of ringed topoi of Stacks 0DK4, whose datum is the same (i, φ) in the same direction, with i finite instead of a closed immersion.

noncomputable def smallEtaleRingedToposHomOfSharp (i : Z ⟶ X)
    {𝒜 : Sheaf (SmallEtale.topology B S hS X.1) CommRingCat.{u}}
    {ℬ : Sheaf (SmallEtale.topology B S hS Z.1) CommRingCat.{u}}
    (φ : 𝒜 ⟶ (pushforwardCommRingFunctor.{u, u, u, u + 1, u, u + 1}
      (smallToposMorphismTypeU B S hS i)).obj ℬ) :
    Stacks.Sheaves.RingedToposModules.RingedToposHom
      (smallEtaleRingedToposOfRings B S hS Z ℬ) (smallEtaleRingedToposOfRings B S hS X 𝒜)

AlgebraicGeometry.Space.tensorPushforwardMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionModuleTensorPushforward.lean, line 201. The attribute's comment: “the canonical map 𝓖 ⊗_ℬ f_*𝓕 ⟶ f_*(f^*𝓖 ⊗_𝒜 𝓕)”.

The canonical map of Stacks 04G0, 𝓕 ⊗_𝒜 f_*𝓖 ⟶ f_*(f^*𝓕 ⊗_ℬ 𝓖): the adjoint transpose of f^*(𝓕 ⊗_𝒜 f_*𝓖) = f^*𝓕 ⊗_ℬ f^*f_*𝓖 ⟶ f^*𝓕 ⊗_ℬ 𝓖, built from the identity of f^*𝓕 and the adjunction map f^*f_*𝓖 ⟶ 𝓖.

No hypothesis on i enters, so this is equally the canonical map of Stacks 0DK4, which is the adjoint transpose of the same comparison for the same datum with i finite.

noncomputable def tensorPushforwardMap (i : Z ⟶ X)
    {𝒜 : Sheaf (SmallEtale.topology B S hS X.1) CommRingCat.{u}}
    {ℬ : Sheaf (SmallEtale.topology B S hS Z.1) CommRingCat.{u}}
    (φ : 𝒜 ⟶ (pushforwardCommRingFunctor.{u, u, u, u + 1, u, u + 1}
      (smallToposMorphismTypeU B S hS i)).obj ℬ)
    (𝓕 : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedToposOfRings B S hS X 𝒜).O))
    (𝓖 : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedToposOfRings B S hS Z ℬ).O)) :
    ((Stacks.SheafOfModules.Tensor.sheafTensor.{u + 1, u, u, u, u} 𝒜).obj 𝓕).obj
      ((pushforwardModules (smallEtaleRingedToposHomOfSharp B S hS i φ)).obj 𝓖) ⟶
      (pushforwardModules (smallEtaleRingedToposHomOfSharp B S hS i φ)).obj
        (((Stacks.SheafOfModules.Tensor.sheafTensor.{u + 1, u, u, u, u} ℬ).obj
          (((smallEtaleRingedToposHomOfSharp B S hS i φ).pullbackModules).obj 𝓕)).obj 𝓖)

AlgebraicGeometry.Space.isIso_tensorPushforwardMap_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteTensorPushforwardIso.lean, line 108.

Stacks 0DK4. Let π : X ⟶ Y be a finite morphism of algebraic spaces over S, 𝒜 a sheaf of rings on X_étale, ℬ a sheaf of rings on Y_étale and φ : ℬ ⟶ π_*𝒜 a homomorphism of sheaves of rings, with associated morphism of ringed topoi f = (π, φ) : (Sh(X_étale), 𝒜) ⟶ (Sh(Y_étale), ℬ). For every sheaf of 𝒜-modules 𝓕 and every sheaf of ℬ-modules 𝓖 the canonical map 𝓖 ⊗_ℬ f_*𝓕 ⟶ f_*(f^*𝓖 ⊗_𝒜 𝓕) is an isomorphism.

theorem isIso_tensorPushforwardMap_of_isFinite (π : X ⟶ Y) (hπ : IsFinite B S hS π.hom)
    {𝒜 : Sheaf (SmallEtale.topology B S hS X.1) CommRingCat.{u}}
    {ℬ : Sheaf (SmallEtale.topology B S hS Y.1) CommRingCat.{u}}
    (φ : ℬ ⟶ (pushforwardCommRingFunctor.{u, u, u, u + 1, u, u + 1}
      (smallToposMorphismTypeU B S hS π)).obj 𝒜)
    (𝓕 : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedToposOfRings B S hS X 𝒜).O))
    (𝓖 : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedToposOfRings B S hS Y ℬ).O)) :
    IsIso (tensorPushforwardMap B S hS π φ 𝓖 𝓕)

Tag 0DK5, a lemma

Tag 0DK5 in the Stacks Project.

AlgebraicGeometry.Space.isIso_derivedProjectionFormulaMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DerivedModuleTensorPushforward.lean, line 164. The attribute's comment: “the invertibility clause, for a morphism of ringed topoi arising from a morphism of sites at a single universe, which is what the derived pullback tensor comparison of 07A4 requires — the small étale ringed topos of an algebraic space does not satisfy this — and given the counit of 07A6 at M and its unit at Rf_*M ⊗^L K, which is what finiteness of π is used for”.

Stacks 0DK5, the invertibility clause, reduced to the derived adjunction of Stacks 07A6: the canonical map Rf_*M ⊗^L_{𝒪_D} K ⟶ Rf_*(M ⊗^L_{𝒪_C} Lf^*K) of Equation 21.50.0.1 is an isomorphism once the counit of Lf^* ⊣ Rf_* is invertible at M and its unit is invertible at Rf_*M ⊗^L_{𝒪_D} K.

Writing the canonical map through the unit, projectionFormulaMap_eq_unit_comp, it becomes

Rf\_*M ⊗^L K --η--> Rf\_*Lf^*(Rf\_*M ⊗^L K) --Rf\_*(t)--> Rf\_*(Lf^*Rf\_*M ⊗^L Lf^*K) --Rf\_*(ε ⊗ 1)--> Rf\_*(M ⊗^L Lf^*K),

whose middle factor is the comparison of Stacks 07A4 and so invertible with no hypothesis, and whose two outer factors are hη and hε.

theorem isIso_derivedProjectionFormulaMap
    (M : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)))
    (hε : IsIso ((derivedAdjunction f hmos).counit.app M))
    (hη : IsIso ((derivedAdjunction f hmos).unit.app
      ((Functor.uncurry.obj (derivedTensorProductFunctor Y.O)).obj
        ((derivedPushforward f).obj M, K)))) :
    IsIso (projectionFormulaMap f hmos M K)

AlgebraicGeometry.Space.derivedProjectionFormulaIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DerivedModuleTensorPushforward.lean, line 188. The attribute's comment: “the isomorphism, for a morphism of ringed topoi arising from a morphism of sites at a single universe, which is what the derived pullback tensor comparison of 07A4 requires — the small étale ringed topos of an algebraic space does not satisfy this — and given the counit of 07A6 at M and its unit at Rf_*M ⊗^L K, which is what finiteness of π is used for; the tensor factors in the order of Equation 21.50.0.1”.

Stacks 0DK5 as an isomorphism Rf_*M ⊗^L_{𝒪_D} K ≅ Rf_*(M ⊗^L_{𝒪_C} Lf^*K), with the tensor factors in the order Equation 21.50.0.1 of Stacks 0B56 is written in; the forward map is the canonical one, not an unspecified isomorphism of objects.

def derivedProjectionFormulaIso
    (M : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)))
    (hε : IsIso ((derivedAdjunction f hmos).counit.app M))
    (hη : IsIso ((derivedAdjunction f hmos).unit.app
      ((Functor.uncurry.obj (derivedTensorProductFunctor Y.O)).obj
        ((derivedPushforward f).obj M, K)))) :
    ((derivedTensorProductFunctor Y.O).obj ((derivedPushforward f).obj M)).obj K ≅
      (derivedPushforward f).obj
        (((derivedTensorProductFunctor X.O).obj M).obj ((derivedPullback f).obj K))

AlgebraicGeometry.Space.derivedProjectionFormulaIsoSourceOrder, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DerivedModuleTensorPushforward.lean, line 225. The attribute's comment: “the isomorphism in the source's order of tensor factors, for a morphism of ringed topoi arising from a morphism of sites at a single universe, which is what the derived pullback tensor comparison of 07A4 requires — the small étale ringed topos of an algebraic space does not satisfy this — and given the counit of 07A6 at M and its unit at Rf_*M ⊗^L K, which is what finiteness of π is used for”.

Stacks 0DK5 in the order the source writes it, K ⊗^L_{𝒪_D} Rf_*M ≅ Rf_*(Lf^*K ⊗^L_{𝒪_C} M).

This is AlgebraicGeometry.Space.derivedProjectionFormulaIso read through the commutativity constraint of the derived tensor product (Stacks 0FPT) on each side: on D(𝒪_D) to transpose the source, and inside Rf_* on D(𝒪_C) to transpose the target. No hypothesis is added.

def derivedProjectionFormulaIsoSourceOrder
    (M : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)))
    (hε : IsIso ((derivedAdjunction f hmos).counit.app M))
    (hη : IsIso ((derivedAdjunction f hmos).unit.app
      ((Functor.uncurry.obj (derivedTensorProductFunctor Y.O)).obj
        ((derivedPushforward f).obj M, K)))) :
    ((derivedTensorProductFunctor Y.O).obj K).obj ((derivedPushforward f).obj M) ≅
      (derivedPushforward f).obj
        (((derivedTensorProductFunctor X.O).obj ((derivedPullback f).obj K)).obj M)

AlgebraicGeometry.Space.nonempty_derivedTensorPushforwardIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteDerivedTensorPushforward.lean, line 525.

Stacks 0DK5. Let π : X ⟶ Y be a finite morphism of algebraic spaces over S, 𝒜 a sheaf of rings on X_étale, ℬ a sheaf of rings on Y_étale and φ : ℬ ⟶ π_*𝒜 a homomorphism of sheaves of rings, with associated morphism of ringed topoi f = (π, φ) : (Sh(X_étale), 𝒜) ⟶ (Sh(Y_étale), ℬ). Then for every K ∈ D(ℬ) and M ∈ D(𝒜)

K ⊗^L_ℬ Rf_*M ≅ Rf_*(Lf^*K ⊗^L_𝒜 M) in D(ℬ).

K is represented by a K-flat complex with flat terms (Stacks 06YS) and M by any complex; on such representatives the isomorphism is AlgebraicGeometry.Space.derivedTensorPushforwardIsoOfKFlat.

theorem nonempty_derivedTensorPushforwardIso (hπ : IsFinite B S hS π.hom)
    (K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf ℬ)))
    (M : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf 𝒜))) :
    Nonempty (((Stacks.SheafOfModules.derivedTensorProductFunctor
        (smallEtaleRingedToposOfRings B S hS Y ℬ).toRingedSite).obj K).obj
        ((Stacks.Cohomology.DerivedPushforward.derivedPushforward
          (X := smallEtaleRingedToposOfRings B S hS X 𝒜)
          (Y := smallEtaleRingedToposOfRings B S hS Y ℬ)
          (ringedToposHomOfSharp B S hS π φ)).obj M) ≅
      (Stacks.Cohomology.DerivedPushforward.derivedPushforward
          (X := smallEtaleRingedToposOfRings B S hS X 𝒜)
          (Y := smallEtaleRingedToposOfRings B S hS Y ℬ)
          (ringedToposHomOfSharp B S hS π φ)).obj
        (((Stacks.SheafOfModules.derivedTensorProductFunctor
          (smallEtaleRingedToposOfRings B S hS X 𝒜).toRingedSite).obj
            ((Stacks.Cohomology.DerivedPullbackOfToposHom.derivedPullback
              (ringedToposHomOfSharp B S hS π φ)).obj K)).obj M))

Sources

• Section 69.4, Tag 0DK2
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.smallEtaleAbelianPushforward_exact_of_isFinite · AlgebraicGeometry.Space.smallEtaleAbelianPushforward_rightDerivedPlus_isZero_of_isFinite · AlgebraicGeometry.Space.smallEtaleAbelianPushforward_exact_of_isIntegralHom · AlgebraicGeometry.Space.smallEtaleAbelianPushforward_rightDerivedPlus_isZero_of_isIntegralHom · AlgebraicGeometry.Space.finite_geometricLifts · AlgebraicGeometry.Space.stalkPushforwardToProduct · AlgebraicGeometry.Space.stalkPushforwardToProduct_natural · AlgebraicGeometry.Space.geometricLiftsEquivOfIsPullback

Section69.5 Colimits and cohomology#

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

Tag 073E, a lemma

Tag 073E in the Stacks Project.

AlgebraicGeometry.Space.isIso_colimit_post_rightDerived_globalSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleCohomologyFilteredColimits.lean, line 713. References: SGA 4 VII (3.3).

Stacks 073E. On a quasi-compact and quasi-separated algebraic space, the canonical map from a filtered colimit of étale cohomology groups to the étale cohomology of the filtered colimit is an isomorphism.

theorem isIso_colimit_post_rightDerived_globalSections
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (hZ : B.Contains (⊤_ Scheme.{u}))
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B S hS X)
    (hqc : IsQuasiCompactSpace B S hS X)
    (hqs : IsAbsolutelyQuasiSeparated B S hS hZ X)
    (p : ℕ) {I : Type w} [SmallCategory I] [IsFiltered I]
    [HasColimitsOfShape I Ab.{u + 1}]
    (F : I ⥤ Sheaf (SmallEtale.topology B S hS X) (Ab.{u + 1})) :
    IsIso (colimit.post F
      ((Sheaf.Γ (SmallEtale.topology B S hS X)
        (Ab.{u + 1})).rightDerived p))

Tag 07U6, a lemma

Tag 07U6 in the Stacks Project.

AlgebraicGeometry.Space.isIso_colimit_post_rightDerived_smallEtaleAbelianPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleCohomologyFilteredColimits.lean, line 890. References: SGA 4 VI (5.1), “étale alg. spaces”.

Stacks 07U6. Let f : X ⟶ Y be a quasi-compact and quasi-separated morphism of algebraic spaces over S. For every degree p and every filtered diagram F of abelian sheaves on the small étale site of X, the canonical map from the colimit of the degree-p higher direct images to the degree-p higher direct image of the colimit is an isomorphism: R^p f_* (colim F_i) = colim R^p f_* F_i.

The direct image is the direct image of abelian sheaves along the morphism of small étale topoi of Stacks 03G2, part (3). It is transported, along the comparison equivalence of Stacks 03G1 at abelian coefficients, to the direct image along the base-change morphism of sites of Stacks 03G2, part (1), where the statement is AlgebraicGeometry.Space.isIso_colimit_post_rightDerived_spacesPushforward.

theorem isIso_colimit_post_rightDerived_smallEtaleAbelianPushforward
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (hZ : B.Contains (⊤_ Scheme.{u})) {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hqc : IsQuasiCompact B S hS f.hom) (hqs : IsQuasiSeparated B S hS f.hom)
    (p : ℕ) {I : Type w} [SmallCategory I] [IsFiltered I]
    [HasColimitsOfShape I Ab.{u + 1}]
    (F : I ⥤ Sheaf (SmallEtale.topology B S hS X.obj) Ab.{u + 1}) :
    IsIso (colimit.post F
      ((abelianPushforward (SmallEtale.topology B S hS X.obj)
        (smallToposMorphism B S hS f)).rightDerived p))

Tag 07U7, a lemma

Tag 07U7 in the Stacks Project.

AlgebraicGeometry.Space.preservesColimitsOfShape_coyoneda_of_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleModelCoveringSet.lean, line 408.

Let X be a quasi-compact and quasi-separated algebraic space over a scheme S, let G be an 𝒪_X-module of finite presentation and let λ ↦ F_λ be a filtered system of 𝒪_X-modules. Then

colim_λ Hom_X(G, F_λ) = Hom_X(G, colim_λ F_λ),

here in the form that Hom_X(G, -) preserves colimits of the given filtered shape, which says exactly that the canonical comparison map out of any such colimit is a bijection. The module universe is the universe u of the schemes.

theorem preservesColimitsOfShape_coyoneda_of_isFinitePresentation
    (hqc : IsQuasiCompactSpace B S hS F) (hqs : IsAbsolutelyQuasiSeparated B S hS hZ F)
    (G : Modules.{u, u} B S hS F hF) [G.IsFinitePresentation]
    (K : Type u) [Category.{u} K] [IsFiltered K] :
    PreservesColimitsOfShape K (coyoneda.obj (Opposite.op G))

Sources

• Section 69.5, Tag 073D
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.isIso_colimit_post_rightDerived_globalSections · AlgebraicGeometry.Space.isIso_colimit_post_rightDerived_smallEtaleAbelianPushforward · AlgebraicGeometry.Space.preservesColimitsOfShape_coyoneda_of_isFinitePresentation

Section69.6 The alternating Čech complex#

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

Tag 0722, a lemma

Tag 0722 in the Stacks Project.

AlgebraicGeometry.Space.SpacesEtale.extensionByZeroConstant_preservesBinaryCoproduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpacesEtaleCoproduct.lean, line 584. The attribute's comment: “coproduct_sum”.

The two canonical maps induced by the inclusions into a binary coproduct of the spaces-étale site give a direct-sum decomposition of extensions by zero.

theorem extensionByZeroConstant_preservesBinaryCoproduct
    (U₁ U₂ U : SpacesEtale B S hS X)
    (i₁ : U₁ ⟶ U) (i₂ : U₂ ⟶ U)
    (hU : IsColimit (BinaryCofan.mk i₁ i₂)) :
    Nonempty (IsColimit (BinaryCofan.mk
      (extensionByZeroConstantMap B S hS X i₁)
      (extensionByZeroConstantMap B S hS X i₂)))

AlgebraicGeometry.Space.SpacesEtale.extensionByZeroConstantTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpacesEtaleTensor.lean, line 852. The attribute's comment: “product_tensor”.

The tensor product of the extensions by zero of the constant sheaf ℤ from two objects of the spaces-étale site of X is the extension by zero from their product.

def extensionByZeroConstantTensorIso (U₁ U₂ U₁₂ : SpacesEtale B S hS X) (p₁ : U₁₂ ⟶ U₁)
    (p₂ : U₁₂ ⟶ U₂) (h : IsLimit (BinaryFan.mk p₁ p₂)) :
    abelianSheafTensor B S hS X (extensionByZeroConstant B S hS X U₁)
        (extensionByZeroConstant B S hS X U₂) ≅
      extensionByZeroConstant B S hS X U₁₂

AlgebraicGeometry.Space.SpacesEtale.extensionByZeroConstantTensorIso_hom_generator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpacesEtaleTensor.lean, line 924. The attribute's comment: “product_tensor on generators”.

The tensor-product isomorphism sends the pure tensor of the generators indexed by φ₁ and φ₂ to the generator indexed by their pairing into the product.

theorem extensionByZeroConstantTensorIso_hom_generator (U₁ U₂ U₁₂ : SpacesEtale B S hS X)
    (p₁ : U₁₂ ⟶ U₁) (p₂ : U₁₂ ⟶ U₂) (h : IsLimit (BinaryFan.mk p₁ p₂))
    (V : SpacesEtale B S hS X) (φ₁ : V ⟶ U₁) (φ₂ : V ⟶ U₂) :
    ((extensionByZeroConstantTensorIso B S hS X U₁ U₂ U₁₂ p₁ p₂ h).hom.hom.app
        (Opposite.op V))
      (((toSheafify (topology B S hS X)
        (presheafTensor (extensionByZeroConstant B S hS X U₁).obj
          (extensionByZeroConstant B S hS X U₂).obj)).app (Opposite.op V))
        (TensorProduct.tmul ℤ (extensionByZeroConstantGenerator B S hS X U₁ V φ₁)
          (extensionByZeroConstantGenerator B S hS X U₂ V φ₂))) =
      extensionByZeroConstantGenerator B S hS X U₁₂ V (h.lift (BinaryFan.mk φ₁ φ₂))

Tag 0723, an equation

Tag 0723 in the Stacks Project.

AlgebraicGeometry.Space.SpacesEtale.koszulAugmentation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AlternatingCech/KoszulComplex.lean, line 176. The attribute's comment: “the augmentation K^• ⟶ ℤ[0]”.

Stacks 0723. The augmentation K^• ⟶ ℤ[0] of the complex K^• attached to an object of the spaces-étale site of X: the trace in degree 0 and zero in higher degrees.

def koszulAugmentation (U : SpacesEtale B S hS X) :
    koszulComplex B S hS X U ⟶
      (ChainComplex.single₀ (Sheaf (topology B S hS X) AddCommGrpCat.{u + 1})).obj
        (constantIntSheaf B S hS X)

AlgebraicGeometry.Space.SpacesEtale.koszulAugmentation_quasiIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AlternatingCech/KoszulResolution.lean, line 401. The attribute's comment: “the augmentation is a quasi-isomorphism for a surjective cover”.

Stacks 0723. For an algebraic space U étale and surjective over X, the augmentation K^• ⟶ ℤ[0] of the Koszul complex of the trace j_{U!} ℤ ⟶ ℤ is a quasi-isomorphism: K^• is a resolution of the constant sheaf ℤ on the spaces-étale site of X.

theorem koszulAugmentation_quasiIso (U : SpacesEtale B S hS X)
    (hsurj : IsSurjective B S hS U.obj.hom.hom) :
    QuasiIso (koszulAugmentation B S hS X U)

Tag 0724, a definition

Tag 0724 in the Stacks Project.

AlgebraicGeometry.Space.SpacesEtale.alternatingCechComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AlternatingCech/Complex.lean, line 66.

Stacks 0724. The alternating Čech complex Č^•_alt(f, F) associated to an abelian sheaf F on the spaces-étale site of X and an object U of that site: the complex Hom(K^0, F) → Hom(K^1, F) → Hom(K^2, F) → … with Hom groups computed in Ab(X_étale) and K^p = ∧^{p+1} j_{U!} ℤ.

def alternatingCechComplex (U : SpacesEtale B S hS X)
    (F : Sheaf (topology B S hS X) AddCommGrpCat.{u + 1}) :
    CochainComplex AddCommGrpCat.{u + 1} ℕ

Tag 0725, a lemma

Tag 0725 in the Stacks Project.

AlgebraicGeometry.Space.SpacesEtale.alternatingCechToDerivedGlobalSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AlternatingCech/DerivedGlobalSections.lean, line 557. The attribute's comment: “the canonical map Č^•_alt(f, ℱ) ⟶ RΓ(X, ℱ) in D(Ab)”.

Let S be a scheme, let f : U ⟶ X be a surjective étale morphism of algebraic spaces over S and let ℱ be an abelian sheaf on the spaces-étale site of X. There is a canonical map

Č^•_alt(f, ℱ) ⟶ RΓ(X, ℱ)

in D(Ab), where Č^•_alt(f, ℱ) is the alternating Čech complex of [Stacks 0724] and RΓ(X, ℱ) is represented by the global sections of an injective resolution of ℱ, so that H^n(RΓ(X, ℱ)) = H^n(X, ℱ) by derivedGlobalSectionsHomologyAddEquivSheafH.

It is the composite of the map into the total complex of the Hom bicomplex Hom(K^p, I^q) with the inverse of the quasi-isomorphism Γ(X, I^•) ⟶ Tot(Hom(K^•, I^•)) of [Stacks 0133].

The other assertion of [Stacks 0725], the spectral sequence with E₁^{p,q} = Ext^q(K^p, ℱ) converging to H^{p+q}(X, ℱ), is AlgebraicGeometry.Space.SpacesEtale.exists_alternatingCechCohomologySpectralSequence.

def alternatingCechToDerivedGlobalSections (U : SpacesEtale B S hS X)
    (hsurj : IsSurjective B S hS U.obj.hom.hom)
    (F : Sheaf (topology B S hS X) AddCommGrpCat.{u + 1}) :
    DerivedCategory.Q.obj (alternatingCechComplexExtend B S hS X U F) ⟶
      derivedGlobalSections B S hS X F

AlgebraicGeometry.Space.SpacesEtale.exists_alternatingCechExtSpectralSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AlternatingCech/ExtSpectralSequence.lean, line 167. The attribute's comment: “the spectral sequence with E₁^{p,q} = Ext^q(K^p, ℱ), abutting to Ext^{p+q}(K^•, ℱ)”.

Stacks 0725, the first page of the spectral sequence. Let X be an algebraic space over a scheme S, let U be an algebraic space étale over X and let ℱ be an abelian sheaf on the spaces-étale site of X. There is a cohomological spectral sequence, starting on page one, with E₁^{p,q} = Ext^q_{Ab(X_étale)}(K^p, ℱ) for K^p = ∧^{p+1} j_{U!} ℤ the terms of the Koszul complex, abutting to the hyper-Ext groups Ext^{p+q}(K^•, ℱ) of the Koszul complex.

It is the spectral sequence of the total complex of the Hom bicomplex Hom(K^p, I^q) filtered by the Koszul degree, for I^• an injective resolution of ℱ.

theorem exists_alternatingCechExtSpectralSequence (U : SpacesEtale B S hS X)
    (F : Sheaf (topology B S hS X) AddCommGrpCat.{u + 1}) :
    ∃ E : CohomologicalSpectralSequence AddCommGrpCat.{u + 2} 1,
      (∀ (p : ℕ) (q : ℤ), Nonempty ((E.page 1).X ((p : ℤ), q) ≅
        AddCommGrpCat.of (Abelian.zExt ((koszulComplex B S hS X U).X p) F q))) ∧
      SpectralSequence.AbutsTo E (fun n ↦ AddCommGrpCat.of
        (DerivedCategory.Ext (DerivedCategory.Q.obj (koszulCochainComplex B S hS X U))
          ((DerivedCategory.singleFunctor
            (Sheaf (topology B S hS X) AddCommGrpCat.{u + 1}) 0).obj F) n))

AlgebraicGeometry.Space.SpacesEtale.exists_alternatingCechCohomologySpectralSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AlternatingCech/ExtSpectralSequence.lean, line 256. The attribute's comment: “the abutment is the cohomology of X, for a surjective cover”.

Stacks 0725. Let X be an algebraic space over a scheme S, let U be an algebraic space étale and surjective over X and let ℱ be an abelian sheaf on the spaces-étale site of X. There is a first-quadrant cohomological spectral sequence, starting on page one, with E₁^{p,q} = Ext^q_{Ab(X_étale)}(K^p, ℱ) for K^p = ∧^{p+1} j_{U!} ℤ the terms of the Koszul complex, abutting to the sheaf cohomology H^{p+q}(X, ℱ).

The abutment is written as the Ext group out of the constant sheaf ℤ, which is Mathlib's definition of sheaf cohomology; the last conjunct records that identification.

theorem exists_alternatingCechCohomologySpectralSequence (U : SpacesEtale B S hS X)
    (hsurj : IsSurjective B S hS U.obj.hom.hom)
    (F : Sheaf (topology B S hS X) AddCommGrpCat.{u + 1}) :
    ∃ E : CohomologicalSpectralSequence AddCommGrpCat.{u + 2} 1,
      (∀ (p : ℕ) (q : ℤ), Nonempty ((E.page 1).X ((p : ℤ), q) ≅
        AddCommGrpCat.of (Abelian.zExt ((koszulComplex B S hS X U).X p) F q))) ∧
      (∀ p q : ℤ, p < 0 ∨ q < 0 → IsZero ((E.page 1).X (p, q))) ∧
      SpectralSequence.AbutsTo E
        (fun n ↦ AddCommGrpCat.of (Abelian.zExt (constantIntSheaf B S hS X) F n)) ∧
      ∀ n : ℕ, Nonempty (AddCommGrpCat.of (Sheaf.H F n) ≅
        AddCommGrpCat.of (Abelian.zExt (constantIntSheaf B S hS X) F (n : ℤ)))

Tag 0726, a lemma

Tag 0726 in the Stacks Project.

AlgebraicGeometry.Space.SpacesEtale.isIso_signTwistToKoszul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AlternatingCech/AntiInvariantSections.lean, line 847. The attribute's comment: “the canonical map ℤ(sign) ⟶ K^p is an isomorphism”.

Stacks 0726. The canonical map ℤ(sign) ⟶ K^p from the sign twist of W_p to the (p+1)-st exterior power of the extension by zero of ℤ from U is an isomorphism: it is the sheafification of a map of presheaves which is both locally injective and locally surjective.

theorem isIso_signTwistToKoszul (U : SpacesEtale B S hS X) (p : ℕ)
    (hsep : IsSeparated B S hS U.1.hom.hom) :
    IsIso (signTwistToKoszul B S hS X U p hsep)

AlgebraicGeometry.Space.SpacesEtale.bijective_koszulHomToSignSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AlternatingCech/AntiInvariantSections.lean, line 865. The attribute's comment: “bijectivity of the map Hom(K^p, F) ⟶ anti-invariant sections”.

Stacks 0726. The canonical map from Hom(K^p, ℱ) to the S_{p+1}-anti-invariant sections of ℱ over W_p is bijective: it is precomposition with the isomorphism ℤ(sign) ⟶ K^p followed by the identification of maps out of ℤ(sign) with anti-invariant sections.

theorem bijective_koszulHomToSignSections (U : SpacesEtale B S hS X) (p : ℕ)
    (hsep : IsSeparated B S hS U.1.hom.hom)
    (F : Sheaf (topology B S hS X) AddCommGrpCat.{u + 1}) :
    Function.Bijective (koszulHomToSignSections B S hS X U p hsep F).hom

AlgebraicGeometry.Space.SpacesEtale.koszulHomSignSectionsEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AlternatingCech/AntiInvariantSections.lean, line 883. The attribute's comment: “the map Hom(K^p, F) ⟶ anti-invariant sections is an isomorphism of groups”.

Stacks 0726. The identification of Hom(K^p, ℱ) with the group of S_{p+1}-anti-invariant sections of ℱ over W_p, as an isomorphism of abelian groups.

def koszulHomSignSectionsEquiv (U : SpacesEtale B S hS X) (p : ℕ)
    (hsep : IsSeparated B S hS U.1.hom.hom)
    (F : Sheaf (topology B S hS X) AddCommGrpCat.{u + 1}) :
    ((koszulComplex B S hS X U).X p ⟶ F) ≃+
      characterSections (diagonalComplement B S hS X U (p + 1) hsep)
        (diagonalComplementAut B S hS X U (p + 1) hsep) Equiv.Perm.sign F.obj

AlgebraicGeometry.Space.SpacesEtale.freeAction_and_bijective_koszulHomToSignSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AlternatingCech/AntiInvariantSections.lean, line 902.

Stacks 0726. For U étale and separated over X the space W_p = U ×_X ⋯ ×_X U ∖ (all diagonals) with p + 1 factors carries a free action of the symmetric group on p + 1 letters over X, and for every abelian sheaf ℱ on the spaces-étale site of X the canonical map from Hom(K^p, ℱ) to the S_{p+1}-anti-invariant sections of ℱ over W_p is bijective, functorially in ℱ.

Freeness is stated in the shape a site asks for: a morphism φ : V ⟶ W_p fixed by σ forces σ = 1 unless the empty sieve covers V. Surjectivity of U ⟶ X, which Stacks 0726 also assumes, is not used: it is what makes the Koszul complex a resolution.

theorem freeAction_and_bijective_koszulHomToSignSections (U : SpacesEtale B S hS X) (p : ℕ)
    (hsep : IsSeparated B S hS U.1.hom.hom) :
    (∀ (V : SpacesEtale B S hS X) (φ : V ⟶ diagonalComplement B S hS X U (p + 1) hsep)
        (σ : Equiv.Perm (Fin (p + 1))),
        φ ≫ (diagonalComplementAut B S hS X U (p + 1) hsep σ).asIso.hom = φ →
          (⊥ : Sieve V) ∈ topology B S hS X V ∨ σ = 1) ∧
      (∀ F : Sheaf (topology B S hS X) AddCommGrpCat.{u + 1},
        Function.Bijective (koszulHomToSignSections B S hS X U p hsep F).hom) ∧
      (∀ (F F' : Sheaf (topology B S hS X) AddCommGrpCat.{u + 1}) (k : F ⟶ F')
        (g : (koszulComplex B S hS X U).X p ⟶ F),
        (((koszulHomToSignSections B S hS X U p hsep F').hom (g ≫ k)).1 :
            F'.obj.obj (op (diagonalComplement B S hS X U (p + 1) hsep))) =
          k.hom.app (op (diagonalComplement B S hS X U (p + 1) hsep))
            (((koszulHomToSignSections B S hS X U p hsep F).hom g).1))

AlgebraicGeometry.Space.SpacesEtale.diagonalComplement, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AlternatingCech/DiagonalComplement.lean, line 487. The attribute's comment: “the space W_p”.

Stacks 0726. The space W = U ×_X ⋯ ×_X U ∖ (all diagonals) with n factors, as an object of the spaces-étale site of X: the complement of the diagonals is an open subspace of U^n, and an open subspace of an object of the site is again one.

def diagonalComplement (U : SpacesEtale B S hS X) (n : ℕ)
    (hsep : IsSeparated B S hS U.1.hom.hom) : SpacesEtale B S hS X

AlgebraicGeometry.Space.SpacesEtale.diagonalComplementAut, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AlternatingCech/DiagonalComplement.lean, line 637. The attribute's comment: “the action of S_{p+1} on W_p over X”.

Stacks 0726. The action of the symmetric group on n letters on W by permuting the factors of U^n. It is an action over X because W and the permutations of the factors live in the spaces-étale site of X.

def diagonalComplementAut (U : SpacesEtale B S hS X) (n : ℕ)
    (hsep : IsSeparated B S hS U.1.hom.hom) :
    Equiv.Perm (Fin n) →* Aut (diagonalComplement B S hS X U n hsep)

AlgebraicGeometry.Space.SpacesEtale.isEmpty_points_of_comp_diagonalComplementAut, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AlternatingCech/DiagonalComplement.lean, line 695. The attribute's comment: “freeness of the action of S_{p+1} on W_p: a fixed morphism has empty source”.

Stacks 0726. The action of the symmetric group on W is free: an object of the site carrying a morphism to W fixed by a permutation σ ≠ 1 has no points.

Pick i with σ⁻¹ i ≠ i. A point of V would give a point of U^n at which the factors of index i and σ⁻¹ i agree, whereas the points of W avoid all the diagonals.

theorem isEmpty_points_of_comp_diagonalComplementAut (U : SpacesEtale B S hS X) (n : ℕ)
    (hsep : IsSeparated B S hS U.1.hom.hom) {V : SpacesEtale B S hS X}
    (φ : V ⟶ diagonalComplement B S hS X U n hsep) (σ : Equiv.Perm (Fin n)) (hσ : σ ≠ 1)
    (hφ : φ ≫ (diagonalComplementAut B S hS X U n hsep σ).asIso.hom = φ) :
    IsEmpty (points B S hS (underlying B S hS X V).1)

AlgebraicGeometry.Space.SpacesEtale.eq_one_of_comp_diagonalComplementAut, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AlternatingCech/DiagonalComplement.lean, line 724. The attribute's comment: “freeness of the action of S_{p+1} on W_p”.

Stacks 0726. The action of the symmetric group on W is free, in the shape the site-theoretic notion of a torsor asks for: a morphism φ : V ⟶ W fixed by σ forces σ = 1 unless the empty sieve covers V.

theorem eq_one_of_comp_diagonalComplementAut (U : SpacesEtale B S hS X) (n : ℕ)
    (hsep : IsSeparated B S hS U.1.hom.hom) {V : SpacesEtale B S hS X}
    (φ : V ⟶ diagonalComplement B S hS X U n hsep) (σ : Equiv.Perm (Fin n))
    (hφ : φ ≫ (diagonalComplementAut B S hS X U n hsep σ).asIso.hom = φ) :
    (⊥ : Sieve V) ∈ topology B S hS X V ∨ σ = 1

AlgebraicGeometry.Space.SpacesEtale.signTwistToKoszul, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AlternatingCech/DiagonalComplement.lean, line 867. The attribute's comment: “the canonical map ℤ(sign) ⟶ K^p”.

Stacks 0726. The canonical map ℤ(sign) ⟶ K^p from the sign twist of W_p to the (p+1)-st exterior power of the extension by zero of ℤ from U: the sheafification of the map sending the class of a morphism V ⟶ W_p to the wedge of its p + 1 components.

def signTwistToKoszul (U : SpacesEtale B S hS X) (p : ℕ)
    (hsep : IsSeparated B S hS U.1.hom.hom) :
    signTwist B S hS X U (p + 1) hsep ⟶ (koszulComplex B S hS X U).X p

AlgebraicGeometry.Space.SpacesEtale.koszulHomToSignSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AlternatingCech/DiagonalComplement.lean, line 879. The attribute's comment: “the map Hom(K^p, F) ⟶ S_{p+1}-anti-invariant sections of F over W_p”.

Stacks 0726. The canonical map from Hom(K^p, ℱ) to the S_{p+1}-anti-invariant sections of ℱ over W_p: precompose with ℤ(sign) ⟶ K^p and use that a map out of ℤ(sign) is the same thing as an anti-invariant section over W_p.

Stacks 0726 asserts in addition that this map is bijective, which is not proved here.

def koszulHomToSignSections (U : SpacesEtale B S hS X) (p : ℕ)
    (hsep : IsSeparated B S hS U.1.hom.hom)
    (F : Sheaf (topology B S hS X) AddCommGrpCat.{u + 1}) :
    AddCommGrpCat.of ((koszulComplex B S hS X U).X p ⟶ F) ⟶
      AddCommGrpCat.of (characterSections (diagonalComplement B S hS X U (p + 1) hsep)
        (diagonalComplementAut B S hS X U (p + 1) hsep) Equiv.Perm.sign F.obj)

AlgebraicGeometry.Space.SpacesEtale.koszulHomToSignSections_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AlternatingCech/DiagonalComplement.lean, line 898. The attribute's comment: “functoriality in F of the map Hom(K^p, F) ⟶ anti-invariant sections”.

Stacks 0726. The map from Hom(K^p, ℱ) to the S_{p+1}-anti-invariant sections of ℱ over W_p is functorial in ℱ: composing a map K^p ⟶ ℱ with ℱ ⟶ ℱ' takes the corresponding section to its image over W_p.

theorem koszulHomToSignSections_naturality (U : SpacesEtale B S hS X) (p : ℕ)
    (hsep : IsSeparated B S hS U.1.hom.hom)
    {F F' : Sheaf (topology B S hS X) AddCommGrpCat.{u + 1}} (k : F ⟶ F')
    (g : (koszulComplex B S hS X U).X p ⟶ F) :
    (((koszulHomToSignSections B S hS X U p hsep F').hom (g ≫ k)).1 :
        F'.obj.obj (op (diagonalComplement B S hS X U (p + 1) hsep))) =
      k.hom.app (op (diagonalComplement B S hS X U (p + 1) hsep))
        (((koszulHomToSignSections B S hS X U p hsep F).hom g).1)

Tag 0727, a lemma

Tag 0727 in the Stacks Project.

AlgebraicGeometry.Space.freeActionChartSectionsEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/FreeActionQuotientSignTwist.lean, line 83. The attribute's comment: “the identification of the chi-semi-invariant sections over the chart with the global sections of the twist, for the quotient of an object of a big fppf site by a free action of a u-small group. The source's group is finite; finiteness is not used here. The locally free rank one half is freeActionChartTwistOverIso”.

[Stacks, Tag 0727], the sections half, for the quotient of an object of a big fppf site by a free action. The χ-semi-invariant sections of an abelian sheaf ℱ on the spaces-étale site of the quotient U = V/G over the chart h_V are the global sections over U of the twist ℱ ⊗_ℤ ℤ(χ).

The chart is a G-torsor over the final object of that site, which is what CategoryTheory.IsTorsorObject.twistTensorSectionsEquiv asks for; the final object is terminal by AlgebraicGeometry.Space.SpacesEtale.final_isTerminal.

def freeActionChartSectionsEquiv
    (F : Sheaf (SpacesEtale.topology B S hS (actionQuotientSpace G B S hS V a ha))
      AddCommGrpCat.{u + 1}) :
    characterSections (freeActionQuotientChart G B S hS V a ha)
        (freeActionChartAut G B S hS V a ha) χ F.obj ≃+
      (characterTwistTensor F.obj (freeActionChartAut G B S hS V a ha) χ
        (SpacesEtale.topology B S hS (actionQuotientSpace G B S hS V a ha))).obj.obj
        (op (SpacesEtale.final B S hS (actionQuotientSpace G B S hS V a ha)))

AlgebraicGeometry.Space.freeActionChartTwistOverIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/FreeActionQuotientSignTwist.lean, line 101. The attribute's comment: “the twist is locally free of rank one, for the quotient of an object of a big fppf site by a free action of a u-small group: it restricts to the constant sheaf Z on the site localized at the chart. The sections half is freeActionChartSectionsEquiv”.

[Stacks, Tag 0727], the local freeness half, for the quotient of an object of a big fppf site by a free action. The twist ℤ(χ) on the spaces-étale site of the quotient U = V/G restricts to the constant sheaf ℤ on the site localized at the chart h_V, which is the sheaf-theoretic form of being locally free of rank one.

def freeActionChartTwistOverIso :
    (constantSheaf ((SpacesEtale.topology B S hS (actionQuotientSpace G B S hS V a ha)).over
        (freeActionQuotientChart G B S hS V a ha)) AddCommGrpCat.{u + 1}).obj
        (AddCommGrpCat.of (ULift.{u + 1} ℤ)) ≅
      ((SpacesEtale.topology B S hS (actionQuotientSpace G B S hS V a ha)).overPullback
          AddCommGrpCat.{u + 1} (freeActionQuotientChart G B S hS V a ha)).obj
        (characterTwist (freeActionQuotientChart G B S hS V a ha)
          (freeActionChartAut G B S hS V a ha) χ
          (SpacesEtale.topology B S hS (actionQuotientSpace G B S hS V a ha)))

AlgebraicGeometry.Space.characterTwistOfOrbitQuotient, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/FreeActionSpacesEtaleCharacterTwist.lean, line 90.

Stacks 0727. Let W be an algebraic space over a scheme S carrying a free action of a group G, let U = W/G be the quotient of [Stacks 071S] and let χ : G → ℤˣ be a character. Then there is a sheaf of ℤ-modules ℤ(χ) on the spaces-étale site of U which is locally free of rank one — trivial over the covering of U by W — and satisfies

H⁰(W, F|_W)^χ = H⁰(U, F ⊗_ℤ ℤ(χ))

for every abelian sheaf F on that site.

This is CategoryTheory.characterTwistOfQuotient at the spaces-étale site of U: the action of G on W is free there and the quotient morphism exhibits the final object as W/G.

def characterTwistOfOrbitQuotient (χ : G →* ℤˣ) :
    CharacterTwistOfQuotient (orbitQuotientEtaleSource hnat hW hfree)
      (orbitQuotientAut hnat hW hfree) χ
      (SpacesEtale.topology B S hS (orbitQuotientSpace hnat hW hfree))
      (SpacesEtale.final B S hS (orbitQuotientSpace hnat hW hfree))

CategoryTheory.IsTorsorObject.twistTensorSectionsEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpacesEtaleCharacterTwistTorsor.lean, line 555. The attribute's comment: “the sections transforming according to the character”.

For a torsor W under a group G over the final object of a site and a character χ : G → ℤˣ, the sections of an abelian sheaf F over W that transform according to χ are the global sections of F ⊗_ℤ ℤ(χ), where ℤ(χ) is the twisted free abelian sheaf on W.

def twistTensorSectionsEquiv (F : Sheaf J AddCommGrpCat.{u + 1}) :
    characterSections W act χ F.obj ≃+ (characterTwistTensor F.obj act χ J).obj.obj (op T)

CategoryTheory.characterTwistOverIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/CharacterTwistLocalFreeness.lean, line 146. The attribute's comment: “the twist is locally free of rank one”.

The twist ℤ(χ) becomes constant on the localized site Over W: its pullback along Over.forget W is the constant sheaf with value ℤ. This is the sheaf-theoretic form of the freeness of rank one of ℤ(χ) over a torsor.

noncomputable def characterTwistOverIso (h : IsTorsorObject act J) (χ : G →* ℤˣ) :
    (constantSheaf (J.over W) AddCommGrpCat.{v}).obj (AddCommGrpCat.of (ULift.{v} ℤ)) ≅
      (J.overPullback AddCommGrpCat.{v} W).obj (characterTwist W act χ J)

CategoryTheory.characterTwistOfQuotient, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/FreeQuotientCharacterTwist.lean, line 120.

Stacks 0727. Let C be a site with final object T, let a group G act freely by automorphisms on an object W of C, let q : W ⟶ T exhibit T as the quotient W/G and let χ : G → ℤˣ be a character. Then there is a sheaf of ℤ-modules ℤ(χ) on the base which is locally free of rank one — trivial over the covering of the base by W — and satisfies H⁰(W, F|_W)^χ = H⁰(T, F ⊗_ℤ ℤ(χ)) for every abelian sheaf F on the base.

That W is a G-torsor over the base is not assumed: it is the first sentence of the source's proof, and is proved from freeness and the quotient identification in CategoryTheory.IsOrbitQuotient.isTorsorObject.

noncomputable def characterTwistOfQuotient {T : C} {q : W ⟶ T} (hfree : ActsFreelyOnObject act J)
    (hq : IsOrbitQuotient act J q) (hT : IsTerminal T) (χ : G →* ℤˣ) :
    CharacterTwistOfQuotient W act χ J T

Tag 0728, a lemma

Tag 0728 in the Stacks Project.

AlgebraicGeometry.Space.SpacesEtale.exists_alternatingCechSignTwistedSpectralSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AlternatingCech/ExtSpectralSequence.lean, line 330. The attribute's comment: “the row q = 0 of the E₁-page, as the S_{p+1}-anti-invariant sections of ℱ over W_p, and the convergence to H^{p+q}(X, ℱ)”.

Stacks 0728. Let S be a scheme, let f : U ⟶ X be a surjective, étale and separated morphism of algebraic spaces over S and let ℱ be an abelian sheaf on the spaces-étale site of X. The spectral sequence of [Stacks 0725] is concentrated in the first quadrant, the row q = 0 of its first page is the group of S_{p+1}-anti-invariant sections of ℱ over W_p = U ×_X ⋯ ×_X U ∖ (all diagonals), and it converges to the sheaf cohomology H^{p+q}(X, ℱ).

The group of anti-invariant sections is what [Stacks 0727] identifies with H^0(U_p, ℱ|_{U_p} ⊗_ℤ ℤ(χ_p)) for U_p = W_p/S_{p+1}; the higher rows of the first page are stated here as the Ext groups out of K^p of [Stacks 0725], the quotient U_p of an algebraic space by a free action of a finite group not being available.

theorem exists_alternatingCechSignTwistedSpectralSequence (U : SpacesEtale B S hS X)
    (hsurj : IsSurjective B S hS U.obj.hom.hom)
    (hsep : IsSeparated B S hS U.obj.hom.hom)
    (F : Sheaf (topology B S hS X) AddCommGrpCat.{u + 1}) :
    ∃ E : CohomologicalSpectralSequence AddCommGrpCat.{u + 2} 1,
      (∀ (p : ℕ) (q : ℤ), Nonempty ((E.page 1).X ((p : ℤ), q) ≅
        AddCommGrpCat.of (Abelian.zExt ((koszulComplex B S hS X U).X p) F q))) ∧
      (∀ p : ℕ, Nonempty ((E.page 1).X ((p : ℤ), 0) ≃+
        characterSections (diagonalComplement B S hS X U (p + 1) hsep)
          (diagonalComplementAut B S hS X U (p + 1) hsep) Equiv.Perm.sign F.obj)) ∧
      (∀ p q : ℤ, p < 0 ∨ q < 0 → IsZero ((E.page 1).X (p, q))) ∧
      SpectralSequence.AbutsTo E
        (fun n ↦ AddCommGrpCat.of (Abelian.zExt (constantIntSheaf B S hS X) F n)) ∧
      ∀ n : ℕ, Nonempty (AddCommGrpCat.of (Sheaf.H F n) ≅
        AddCommGrpCat.of (Abelian.zExt (constantIntSheaf B S hS X) F (n : ℤ)))

AlgebraicGeometry.Space.SpacesEtale.exists_alternatingCechQuotientSpectralSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AlternatingCech/QuotientSpectralSequence.lean, line 103. The attribute's comment: “the E₁-page is H^q(U_p, F|_{U_p} ⊗ Z(χ_p)) in every degree q, and the convergence to H^{p+q}(X, F)”.

Stacks 0728. Let S be a scheme, let f : U ⟶ X be a surjective, étale and separated morphism of algebraic spaces over S and let ℱ be an abelian sheaf on the spaces-étale site of X. Write W_p = U ×_X ⋯ ×_X U ∖ (all diagonals) with p + 1 factors, let U_p = W_p/S_{p+1} and let ℤ(χ_p) be the rank one twist of [Stacks 0727] attached to the sign character of S_{p+1}. The spectral sequence of [Stacks 0725] is concentrated in the first quadrant, its first page is

E₁^{p,q} = H^q(U_p, ℱ|_{U_p} ⊗_ℤ ℤ(χ_p))

in every degree q, and it converges to the sheaf cohomology H^{p+q}(X, ℱ).

Cohomology is written as the Ext group out of the constant sheaf ℤ read in the derived category; two conjuncts identify those groups with Mathlib's sheaf cohomology, on X for the abutment and on U_p for the first page, and the last one identifies the coefficient sheaf on U_p with the tensor product of ℱ|_{U_p} against the twist of [Stacks 0727]. The first conjunct records the first page in the Ext form of [Stacks 0725] out of the terms K^p = ∧^{p+1} j_{U!} ℤ of the Koszul complex.

theorem exists_alternatingCechQuotientSpectralSequence
    (hsurj : IsSurjective B S hS U.1.hom.hom)
    (F : Sheaf (topology B S hS X) AddCommGrpCat.{u + 1}) :
    ∃ E : CohomologicalSpectralSequence AddCommGrpCat.{u + 2} 1,
      (∀ (p : ℕ) (q : ℤ), Nonempty ((E.page 1).X ((p : ℤ), q) ≅
        AddCommGrpCat.of (zExt ((koszulComplex B S hS X U).X p) F q))) ∧
      (∀ p q : ℕ, Nonempty ((E.page 1).X ((p : ℤ), (q : ℤ)) ≃+
        zExt (constantIntSheaf B S hS (diagonalComplementQuotient B S hS X U (p + 1) hsep))
          (diagonalComplementTwistedRestriction B S hS X U hsep p F) (q : ℤ))) ∧
      (∀ p q : ℤ, p < 0 ∨ q < 0 → IsZero ((E.page 1).X (p, q))) ∧
      SpectralSequence.AbutsTo E
        (fun n ↦ AddCommGrpCat.of (zExt (constantIntSheaf B S hS X) F n)) ∧
      (∀ n : ℕ, Nonempty (AddCommGrpCat.of (Sheaf.H F n) ≅
        AddCommGrpCat.of (zExt (constantIntSheaf B S hS X) F (n : ℤ)))) ∧
      (∀ p q : ℕ, Nonempty (AddCommGrpCat.of
          (Sheaf.H (diagonalComplementTwistedRestriction B S hS X U hsep p F) q) ≅
        AddCommGrpCat.of
          (zExt (constantIntSheaf B S hS (diagonalComplementQuotient B S hS X U (p + 1) hsep))
            (diagonalComplementTwistedRestriction B S hS X U hsep p F) (q : ℤ)))) ∧
      ∀ p : ℕ, Nonempty (diagonalComplementTwistedRestriction B S hS X U hsep p F ≅
        (presheafToSheaf (topology B S hS (diagonalComplementQuotient B S hS X U (p + 1) hsep))
            AddCommGrpCat.{u + 1}).obj
          (AddCommGrpCat.presheafTensor
            ((diagonalComplementQuotientRestriction B S hS X U (p + 1) hsep).obj F).obj
            (characterTwistOfDiagonalComplement B S hS X U (p + 1) hsep
              (diagonalComplementSignCharacter (p + 1))).twist.obj))

Sources

• Section 69.6, Tag 0721
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.SpacesEtale.extensionByZeroConstant_preservesBinaryCoproduct · AlgebraicGeometry.Space.SpacesEtale.extensionByZeroConstantTensorIso · AlgebraicGeometry.Space.SpacesEtale.extensionByZeroConstantTensorIso_hom_generator · AlgebraicGeometry.Space.SpacesEtale.koszulAugmentation · AlgebraicGeometry.Space.SpacesEtale.koszulAugmentation_quasiIso · AlgebraicGeometry.Space.SpacesEtale.alternatingCechComplex · AlgebraicGeometry.Space.SpacesEtale.alternatingCechToDerivedGlobalSections · AlgebraicGeometry.Space.SpacesEtale.exists_alternatingCechExtSpectralSequence

Section69.7 Higher vanishing for quasi-coherent sheaves#

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

Tag 072A, a lemma

Tag 072A in the Stacks Project.

AlgebraicGeometry.Space.SignTwistSetup.isQuasicoherentOnSite_twist, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpacesEtaleSignTwist.lean, line 577.

Stacks 072A. With S, W, G, U, χ as in Stacks 0727: if F is a quasi-coherent 𝒪_U-module, then so is F ⊗_ℤ ℤ(χ).

Quasi-coherence may be checked étale locally, and ℤ(χ) is free of rank one on a covering of U; on each member of that covering a trivializing section identifies the twist with F itself.

theorem isQuasicoherentOnSite_twist
    (F : Modules.{u, u + 1} B S hS h.quotient.1 h.quotient.2) (hF : F.IsQuasicoherentOnSite) :
    (h.twist F).IsQuasicoherentOnSite

Tag 072B, a proposition

Tag 072B in the Stacks Project.

AlgebraicGeometry.Space.SpacesEtale.isZero_sheafH_of_isEmpty_diagonalComplement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AlternatingCech/HigherVanishing.lean, line 150. The attribute's comment: “the vanishing H^n(X, F) = 0 above the fibre bound of the chart. The bound used is the degree bound of Stacks 03JL on the fibres of the chart, which is what empties W_p and so what the source's proof uses, rather than the source's stated bound on the cardinality of the topological fibres of the chart; the degree is existentially quantified because the predicate of Stacks 03JL hides its own bound, and the emptiness of W_p above it is proved here. What the source draws from the quasi-compactness and separatedness of X and the affineness of the chart is the vanishing of the rows q > 0 of the E_1-page of Stacks 0728; that rests on the affineness of the quotients U_p = W_p/S_{p+1}, hence on Stacks 071S for a free action of a finite group on an arbitrary algebraic space, which this subtree does not state in any shape, and it is the binder hUpVanishing”.

Let S be a scheme, let X be an algebraic space over S and let c : W ⟶ X be a surjective, étale and separated morphism from a scheme whose fibres are universally bounded in the sense of [Stacks, Tag 03JL]. If the rows q > 0 of the first page of the alternating Čech spectral sequence of [Stacks, Tag 0728] vanish, then H^n(X, ℱ) = 0 above the fibre bound of c.

theorem isZero_sheafH_of_isEmpty_diagonalComplement (W : BigFppfOver B S hS)
    (c : yoneda.obj W ⟶ X.obj) (hc : IsEtale B S hS c)
    (hsurj : IsSurjective B S hS c) (hsep : IsSeparated B S hS c)
    (hbound : HasUniversallyBoundedFibers B S hS W c)
    (F : Sheaf (topology B S hS X) AddCommGrpCat.{u + 1})
    (hUpVanishing : ∀ (p : ℕ) (q : ℤ), 0 < q →
      IsZero (AddCommGrpCat.of (Abelian.zExt
        ((koszulComplex B S hS X (chartObj B S hS X W c hc)).X p) F q))) :
    ∃ d : ℕ, ∀ n : ℕ, d ≤ n → IsZero (AddCommGrpCat.of (Sheaf.H F n))

AlgebraicGeometry.Space.isZero_rightDerived_globalSectionsFunctor_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AlternatingCech/QuasicoherentHigherVanishing.lean, line 540. The attribute's comment: “The reading of d as a degree bound: the base changes of f to fields have degree at most d, which is what the source's proof uses and what Lemma 69.7.3 (Tag 072C) supplies. The literal reading (at most d points in each fibre of |U| → |X|) is neither proved nor refuted here; for it the proof's step W_p = ∅ for p ≥ d fails (Spec k' → Spec k with k'/k separable quadratic: one point per fibre, degree 2), although the conclusion holds in that example. Quasi-compactness of X is implied by the affine surjection and not assumed.”.

Stacks 072B. Let X be a separated algebraic space, U an affine scheme and f : U → X a surjective étale morphism whose base changes to fields are finite locally free of degree at most d. Then Hᵠ(X, ℱ) = 0 for every quasi-coherent 𝒪_X-module ℱ and every q ≥ d.

theorem isZero_rightDerived_globalSectionsFunctor_of_isSeparated
    (hZ : B.Contains (⊤_ Scheme.{u})) (X : AlgebraicSpaces B S hS)
    (hsepX : IsAbsolutelySeparated B S hS hZ X.1)
    (W : BigFppfOver B S hS) (hW : IsAffine ((BigFppfOver.toScheme B S hS).obj W))
    (c : yoneda.obj W ⟶ X.obj) (hc : IsEtale B S hS c) (hsurj : IsSurjective B S hS c)
    (d : ℕ) (hd : ∀ (k : Type u) [Field k] (T : BigFppfOver B S hS),
      ((BigFppfOver.toScheme B S hS).obj T ≅ Spec (.of k)) →
      ∀ ξ : yoneda.obj T ⟶ X.obj,
        ∃ (V : BigFppfOver B S hS) (p : V ⟶ T) (i : yoneda.obj V ⟶ yoneda.obj W) (r : ℕ),
          r ≤ d ∧ Stacks.Morphisms.IsFiniteLocallyFreeOfRank
              ((BigFppfOver.toScheme B S hS).map p) r ∧
            IsPullback i (yoneda.map p) c ξ)
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : F.IsQuasicoherentOnSite) (q : ℕ) (hq : d ≤ q) :
    IsZero (((Stacks.Cohomology.SiteModules.globalSectionsFunctor.{u + 1, u, u, u}
      (Stacks.SheafOfModules.Tensor.ringSheaf
        (smallEtaleRingedSite B S hS X.1 X.2).O)).rightDerived q).obj F)

Tag 072C, a lemma

Tag 072C in the Stacks Project.

AlgebraicGeometry.Space.exists_affine_etale_surjective_cover_diagonalComplementQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AlternatingCech/DiagonalComplementQuotientCover.lean, line 206. The attribute's comment: “parts (4)-(5), together with parts (1)-(3) restated, for Y a quasi-compact and quasi-separated algebraic space over an arbitrary base scheme S: an affine scheme V_p, a surjective etale morphism V_p -> U_p onto the quotient U_p = W_p/S_{p+1} of Tag 0726, and an integer bounding the degrees of its fibres, for every p -- the source's range 0 <= p <= d being dropped, which is stronger. The integer max(d_p + p) is formed at AlgebraicGeometry.Space.exists_bound_affine_etale_surjective_cover_diagonalComplementQuotient; the vanishing these choices feed is AlgebraicGeometry.Space.isZero_sheafH_of_data_072C”.

The choices (1)–(5) of Stacks 072C. On a quasi-compact, quasi-separated algebraic space Y over an arbitrary base scheme S one may choose an affine scheme U, a surjective étale morphism f : U ⟶ Y and a universal bound on the degrees of its fibres — and then, for every p, an affine scheme V_p, a surjective étale morphism V_p ⟶ U_p onto the quotient U_p = W_p/S_{p+1} of [Stacks, Tag 0726], and a universal bound on the degrees of its fibres.

The separatedness of f, under which W_p and U_p are formed, is produced here rather than assumed. The source restricts p to 0 ≤ p ≤ d; the restriction is dropped, which is stronger.

Choices (1)–(3) are AlgebraicGeometry.Space.exists_affine_etale_surjective_cover_hasUniversallyBoundedFibers', and (4)–(5) are that same statement applied to U_p, which is quasi-compact by AlgebraicGeometry.Space.SpacesEtale.isQuasiCompactSpace_diagonalComplementQuotient and quasi-separated because it is separated, by AlgebraicGeometry.Space.SpacesEtale.isAbsolutelySeparated_diagonalComplementQuotient and [Stacks, Tag 02X3]. Separatedness of U_p is what the source itself records — "since U is separated, the schemes W_p are separated, hence U_p is separated" — and it needs nothing of the base, which is why the base here is an arbitrary scheme.

theorem exists_affine_etale_surjective_cover_diagonalComplementQuotient
    (hqc : IsQuasiCompactSpace B S hS Y)
    (hqs : IsAbsolutelyQuasiSeparated B S hS hZ Y) :
    ∃ (U : BigFppfOver B S hS) (g : yoneda.obj U ⟶ Y)
        (het : IsEtale B S hS g) (hsep : IsSeparated B S hS g),
      IsAffine ((BigFppfOver.toScheme B S hS).obj U) ∧
        (MorphismProperty.inverseImage (@Surjective.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf g ∧
        HasUniversallyBoundedFibers B S hS U g ∧
        ∀ p : ℕ, ∃ (V : BigFppfOver B S hS)
            (f : yoneda.obj V ⟶ (SpacesEtale.diagonalComplementQuotient B S hS
              ⟨Y, hY⟩ (SpacesEtale.chartObj B S hS ⟨Y, hY⟩ U g het)
              (p + 1) hsep).obj),
          IsAffine ((BigFppfOver.toScheme B S hS).obj V) ∧
            (MorphismProperty.inverseImage (@Surjective.{u} : MorphismProperty Scheme.{u})
              (BigFppfOver.toScheme B S hS)).presheaf f ∧
            IsEtale B S hS f ∧
            HasUniversallyBoundedFibers B S hS V f

AlgebraicGeometry.Space.exists_bound_affine_etale_surjective_cover_diagonalComplementQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AlternatingCech/DiagonalComplementQuotientCover.lean, line 265. The attribute's comment: “the integer max(d_p + p), for Y a quasi-compact and quasi-separated algebraic space over an arbitrary base scheme S: a single integer dominating d_p + p on the range where the column p can be nonzero. The d of this statement is the emptiness threshold produced from the fibre bound of choice (3) -- W_q has no points for q > d -- and the domination is asserted for the p with p + 1 <= d. The tag's own bound, max(d_p + p) over 0 <= p <= d for d the fibre bound of choice (3), is the hypothesis of AlgebraicGeometry.Space.isZero_sheafH_of_data_072C, where the vanishing at it is proved”.

The integer max(d_p + p) of Stacks 072C. Beside the five choices there is a single integer N dominating d_p + p for every p whose column can be nonzero: the d produced here is the threshold above which W_q has no points, got from the fibre bound of choice (3), the domination is asserted for the p with p + 1 ≤ d, and N is the maximum of d_p + p over those.

This is the integer at which [Stacks, Tag 072C] asserts the cohomology of every quasi-coherent module to vanish; that vanishing, from these choices, is AlgebraicGeometry.Space.isZero_sheafH_of_data_072C. What is proved here is that the choices (1)–(5) determine such an N.

theorem exists_bound_affine_etale_surjective_cover_diagonalComplementQuotient
    (hqc : IsQuasiCompactSpace B S hS Y)
    (hqs : IsAbsolutelyQuasiSeparated B S hS hZ Y) :
    ∃ (U : BigFppfOver B S hS) (g : yoneda.obj U ⟶ Y)
        (het : IsEtale B S hS g) (hsep : IsSeparated B S hS g)
        (d : ℕ) (N : ℤ),
      IsAffine ((BigFppfOver.toScheme B S hS).obj U) ∧
        (MorphismProperty.inverseImage (@Surjective.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf g ∧
        HasUniversallyBoundedFibers B S hS U g ∧
        (∀ q : ℕ, d < q → IsEmpty (points B S hS
          (SpacesEtale.underlying B S hS ⟨Y, hY⟩
            (SpacesEtale.diagonalComplement B S hS ⟨Y, hY⟩
              (SpacesEtale.chartObj B S hS ⟨Y, hY⟩ U g het) q hsep)).obj)) ∧
        ∀ p : ℕ, ∃ (V : BigFppfOver B S hS)
            (f : yoneda.obj V ⟶ (SpacesEtale.diagonalComplementQuotient B S hS
              ⟨Y, hY⟩ (SpacesEtale.chartObj B S hS ⟨Y, hY⟩ U g het)
              (p + 1) hsep).obj) (dp : ℤ),
          IsAffine ((BigFppfOver.toScheme B S hS).obj V) ∧
            (MorphismProperty.inverseImage (@Surjective.{u} : MorphismProperty Scheme.{u})
              (BigFppfOver.toScheme B S hS)).presheaf f ∧
            IsEtale B S hS f ∧
            BoundsFibreDegrees B S hS V f dp ∧
            (p + 1 ≤ d → dp + p ≤ N)

AlgebraicGeometry.Space.isZero_sheafH_of_data_072C, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AlternatingCech/QuasiSeparatedVanishing.lean, line 226. The attribute's comment: “the conclusion: for X a quasi-compact and quasi-separated algebraic space over a scheme S, given the choices (1)-(5) -- an affine U with a surjective etale U -> X, an integer d bounding its fibre degrees, and for each p <= d an affine V_p with a surjective etale V_p -> U_p = W_{p+1}/S_{p+1} and an integer d_p bounding its fibre degrees -- the cohomology H^q(X, F) vanishes for every quasi-coherent module F and every q at least the source's max(d_p + p) over 0 <= p <= d. The cohomology is the sheaf cohomology of the underlying abelian sheaf of F on the spaces-etale site of X”.

The vanishing of [Stacks, Tag 072C] from the choices (1)–(5). Let S be a scheme and let X be a quasi-compact and quasi-separated algebraic space over S. Choose an affine scheme U, a surjective étale morphism f : U ⟶ X and an integer d bounding the degrees of the fibres of f; for each p with 0 ≤ p ≤ d choose an affine scheme V_p, a surjective étale morphism V_p ⟶ U_p onto the quotient U_p = W_{p+1}/S_{p+1} of [Stacks, Tag 0726], and an integer d_p bounding the degrees of its fibres. Then

H^q(X, ℱ) = 0

for every quasi-coherent 𝒪_X-module ℱ and every q at least max (d_p + p).

The bound is the source's, formed as the supremum of d_p + p over 0 ≤ p ≤ d. The vanishing is read on the spaces-étale site of X, as the sheaf cohomology of the underlying abelian sheaf of ℱ; the cohomological descent that identifies that with the derived functors of global sections on modules is [Stacks, Tag 03FD].

The one input of the recursion that the recursion cannot supply is the positive-degree vanishing on an affine algebraic space — the clause of [Stacks, Tag 03DW] in positive degrees, AlgebraicGeometry.Space.SpacesEtale.AffineSerreVanishing. It is supplied here by AlgebraicGeometry.Space.SpacesEtale.affineSerreVanishing_of_isZero_cechCohomology, the Čech-to-derived criterion of [Stacks, Tag 03F9] on the cofinal affine objects of the small étale site, whose Čech hypothesis is AlgebraicGeometry.Space.SmallEtale.isZero_cechCohomology_comparisonCoefficients_forall.

theorem isZero_sheafH_of_data_072C
    (X : AlgebraicSpaces B S hS)
    (hqc : IsQuasiCompactSpace B S hS X.obj)
    (hqs : IsAbsolutelyQuasiSeparated B S hS hZ X.obj)
    (U : BigFppfOver B S hS) (hU : IsAffine ((BigFppfOver.toScheme B S hS).obj U))
    (f : yoneda.obj U ⟶ X.obj) (hf : IsEtale B S hS f) (hfsurj : IsSurjective B S hS f)
    (d : ℕ) (hd : BoundsFibreDegrees B S hS U f (d : ℤ)) (dp : ℕ → ℕ)
    (hdata : ∀ (hsep : IsSeparated B S hS f) (p : ℕ), p ≤ d →
      ∃ (V : BigFppfOver B S hS)
        (g : yoneda.obj V ⟶ (SpacesEtale.diagonalComplementQuotient B S hS X
          (SpacesEtale.chartObj B S hS X U f hf) (p + 1) hsep).obj),
        IsAffine ((BigFppfOver.toScheme B S hS).obj V) ∧
          IsEtale B S hS g ∧ IsSurjective B S hS g ∧
          BoundsFibreDegrees B S hS V g (dp p : ℤ))
    (M : SheafOfModules.{u + 1} (SpacesEtale.spacesEtaleRing B S hS X))
    (hM : M.IsQuasicoherentOnSite)
    (n : ℕ) (hn : (Finset.range (d + 1)).sup (fun p => dp p + p) ≤ n) :
    IsZero (AddCommGrpCat.of (Sheaf.H
      ((SheafOfModules.toSheaf.{u + 1} (SpacesEtale.spacesEtaleRing B S hS X)).obj M) n))

AlgebraicGeometry.Space.exists_forall_isZero_sheafH_of_isQuasiCompactSpace_072C, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AlternatingCech/QuasiSeparatedVanishing.lean, line 292. The attribute's comment: “the tag end to end, over an arbitrary base scheme S: for X a quasi-compact and quasi-separated algebraic space over S there is a single degree N beyond which the sheaf cohomology on the spaces-etale site of X of the underlying abelian sheaf of every quasi-coherent module vanishes. N is constructed in the proof as the source's max(d_p + p) for the choices (1)-(5) made there; the statement quantifies N existentially, and the identification of N with that maximum is stated at AlgebraicGeometry.Space.isZero_sheafH_of_data_072C”.

[Stacks, Tag 072C], end to end. Let S be a scheme and let X be a quasi-compact and quasi-separated algebraic space over S. Then there is a single degree N beyond which the cohomology of X with quasi-coherent coefficients vanishes:

H^q(X, ℱ) = 0 for every quasi-coherent 𝒪_X-module ℱ and every q ≥ N.

The base is an arbitrary scheme, as in the source. This is the five choices of the tag, AlgebraicGeometry.Space.exists_affine_etale_surjective_cover_diagonalComplementQuotient, fed into the vanishing they give, AlgebraicGeometry.Space.isZero_sheafH_of_data_072C, with N the source's max (d_p + p) over 0 ≤ p ≤ d; the two fibre bounds are produced as integers by AlgebraicGeometry.Space.HasUniversallyBoundedFibers and enlarged to natural numbers by AlgebraicGeometry.Space.BoundsFibreDegrees.mono. The uniformity in ℱ — one degree for all quasi-coherent coefficients at once — is what the tag asserts and is what makes the Euler characteristic of a coherent module a finite alternating sum.

theorem exists_forall_isZero_sheafH_of_isQuasiCompactSpace_072C
    (X : AlgebraicSpaces B S hS)
    (hqc : IsQuasiCompactSpace B S hS X.obj)
    (hqs : IsAbsolutelyQuasiSeparated B S hS hZ X.obj) :
    ∃ N : ℕ, ∀ (M : SheafOfModules.{u + 1} (SpacesEtale.spacesEtaleRing B S hS X)),
      M.IsQuasicoherentOnSite → ∀ n : ℕ, N ≤ n →
        IsZero (AddCommGrpCat.of (Sheaf.H
          ((SheafOfModules.toSheaf.{u + 1} (SpacesEtale.spacesEtaleRing B S hS X)).obj M) n))

AlgebraicGeometry.Space.exists_affine_etale_surjective_cover_hasUniversallyBoundedFibers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohomologicalDimension.lean, line 94. The attribute's comment: “parts (1)-(3): an affine scheme U, a surjective étale morphism U ⟶ X, and an integer bounding the degrees of its fibres”.

The choices (1)–(3) of Stacks 072C. A quasi-compact, quasi-separated algebraic space carries a surjective étale morphism from an affine scheme whose fibres are universally bounded in the sense of Stacks 03JL.

theorem exists_affine_etale_surjective_cover_hasUniversallyBoundedFibers
    (hqc : IsQuasiCompactSpace B (Spec (.of A)) hA X)
    (hqs : IsAbsolutelyQuasiSeparated B (Spec (.of A)) hA hZ X) :
    ∃ (U : BigFppfOver B (Spec (.of A)) hA) (g : yoneda.obj U ⟶ X),
      IsAffine ((BigFppfOver.toScheme B (Spec (.of A)) hA).obj U) ∧
        (MorphismProperty.inverseImage (@Surjective.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B (Spec (.of A)) hA)).presheaf g ∧
        IsEtale B (Spec (.of A)) hA g ∧
        HasUniversallyBoundedFibers B (Spec (.of A)) hA U g

AlgebraicGeometry.Space.exists_forall_isZero_cohomologyOverBase_of_isQuasiCompactSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohomologicalDimension.lean, line 119. The attribute's comment: “the conclusion, uniformly in the quasi-coherent module, with Stacks 072B carried as the hypothesis h072B: the alternating Čech spectral sequence of Stacks 0728 and the quotients U_p that both its proof and the reduction to the separated case need are absent”.

Stacks 072C. On a quasi-compact, quasi-separated algebraic space over Spec A there is a single degree N beyond which the cohomology over A of every quasi-coherent 𝒪_X-module vanishes.

theorem exists_forall_isZero_cohomologyOverBase_of_isQuasiCompactSpace
    (hqc : IsQuasiCompactSpace B (Spec (.of A)) hA X)
    (hqs : IsAbsolutelyQuasiSeparated B (Spec (.of A)) hA hZ X)
    (h072B : ∀ (U : BigFppfOver B (Spec (.of A)) hA) (g : yoneda.obj U ⟶ X),
      IsAffine ((BigFppfOver.toScheme B (Spec (.of A)) hA).obj U) →
      (MorphismProperty.inverseImage (@Surjective.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B (Spec (.of A)) hA)).presheaf g →
      IsEtale B (Spec (.of A)) hA g →
      HasUniversallyBoundedFibers B (Spec (.of A)) hA U g →
      ∃ N : ℕ, ∀ F : Modules.{u, max (u + 1) w} B (Spec (.of A)) hA X hX,
        F.IsQuasicoherentOnSite → ∀ q, N ≤ q →
          IsZero (cohomologyOverBase.{u, w} A B hA X hX F q)) :
    ∃ N : ℕ, ∀ F : Modules.{u, max (u + 1) w} B (Spec (.of A)) hA X hX,
      F.IsQuasicoherentOnSite → ∀ q, N ≤ q →
        IsZero (cohomologyOverBase.{u, w} A B hA X hX F q)

AlgebraicGeometry.Space.exists_affine_etale_surjective_cover_hasUniversallyBoundedFibers', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohomologicalDimensionGeneralBase.lean, line 60. The attribute's comment: “parts (1)-(3): an affine scheme U, a surjective étale morphism U ⟶ X, and an integer bounding the degrees of its fibres, for X a quasi-compact and quasi-separated algebraic space over an arbitrary base scheme S”.

The choices (1)–(3) of Stacks 072C. A quasi-compact, quasi-separated algebraic space over an arbitrary base scheme S carries a surjective étale morphism from an affine scheme whose fibres are universally bounded in the sense of Stacks 03JL.

The base is an arbitrary scheme, as in the source: nothing in the two inputs — the affine étale chart of [Stacks, Tag 03H6] and the chain (η) ⇒ (ζ) ⇒ (ε) ⇒ (δ) of [Stacks, Tag 03JX] — restricts it, and quasi-separatedness is taken in the absolute form of [Stacks, Tag 03BS] part (3), which does not mention S either.

theorem exists_affine_etale_surjective_cover_hasUniversallyBoundedFibers'
    (hqc : IsQuasiCompactSpace B S hS X)
    (hqs : IsAbsolutelyQuasiSeparated B S hS hZ X) :
    ∃ (U : BigFppfOver B S hS) (g : yoneda.obj U ⟶ X),
      IsAffine ((BigFppfOver.toScheme B S hS).obj U) ∧
        (MorphismProperty.inverseImage (@Surjective.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf g ∧
        IsEtale B S hS g ∧
        HasUniversallyBoundedFibers B S hS U g

AlgebraicGeometry.Space.exists_forall_isZero_rightDerived_globalSectionsFunctor_of_isQuasiCompactSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohomologicalDimensionUniform.lean, line 108. The attribute's comment: “the uniform vanishing degree, for every quasi-coherent module; the value max (d_p + p) of the degree is not part of this statement”.

Stacks 072C, the uniform vanishing. On a quasi-compact and quasi-separated algebraic space X there is a single degree N beyond which the cohomology of every quasi-coherent 𝒪_X-module vanishes: Hᑫ(X, 𝓕) = 0 for q ≥ N.

theorem exists_forall_isZero_rightDerived_globalSectionsFunctor_of_isQuasiCompactSpace
    (X : AlgebraicSpaces B S hS) (hqc : IsQuasiCompactSpace B S hS X.1)
    (hqs : IsAbsolutelyQuasiSeparated B S hS hZ X.1) :
    ∃ N : ℕ, ∀ F : Modules.{u, u} B S hS X.1 X.2, F.IsQuasicoherentOnSite → ∀ q, N ≤ q →
      IsZero (((globalSectionsFunctor.{u + 1, u, u, u}
        (Stacks.SheafOfModules.Tensor.ringSheaf
          (smallEtaleRingedSite B S hS X.1 X.2).O)).rightDerived q).obj F)

Sources

• Section 69.7, Tag 0729
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.SignTwistSetup.isQuasicoherentOnSite_twist · AlgebraicGeometry.Space.SpacesEtale.isZero_sheafH_of_isEmpty_diagonalComplement · AlgebraicGeometry.Space.isZero_rightDerived_globalSectionsFunctor_of_isSeparated · AlgebraicGeometry.Space.exists_affine_etale_surjective_cover_diagonalComplementQuotient · AlgebraicGeometry.Space.exists_bound_affine_etale_surjective_cover_diagonalComplementQuotient · AlgebraicGeometry.Space.isZero_sheafH_of_data_072C · AlgebraicGeometry.Space.exists_forall_isZero_sheafH_of_isQuasiCompactSpace_072C · AlgebraicGeometry.Space.exists_affine_etale_surjective_cover_hasUniversallyBoundedFibers

Section69.8 Vanishing for higher direct images#

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

Tag 073G, a lemma

Tag 073G in the Stacks Project.

AlgebraicGeometry.Space.exists_forall_isZero_rightDerived_modulePushforward_of_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/HigherDirectImageUniformBound.lean, line 503.

[Stacks, Tag 073G]. Let f : X ⟶ Y be a quasi-compact and quasi-separated morphism of algebraic spaces over S, with Y quasi-compact. There is a single degree n(X → Y) such that for every algebraic space Y', every morphism Y' ⟶ Y, every algebraic space X' making X' ⟶ X, X' ⟶ Y' a cartesian square over f, and every quasi-coherent 𝒪_{X'}-module 𝓕', the higher direct images R^q f'_*𝓕' vanish for q ≥ n(X → Y).

theorem exists_forall_isZero_rightDerived_modulePushforward_of_qcqs {X Y : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (hfqc : IsQuasiCompact B S hS f.hom) (hfqs : IsQuasiSeparated B S hS f.hom)
    (hYqc : IsQuasiCompactSpace B S hS Y.1) :
    ∃ N : ℕ, ∀ (Y' X' : AlgebraicSpaces B S hS) (g : Y' ⟶ Y) (i' : X' ⟶ X) (f' : X' ⟶ Y'),
      IsPullback i' f' f g →
      ∀ F' : Modules.{u, u} B S hS X'.1 X'.2, F'.IsQuasicoherentOnSite → ∀ q : ℕ, N ≤ q →
        IsZero (((modulePushforward B S hS f').rightDerived q).obj F')

AlgebraicGeometry.Space.exists_forall_isZero_rightDerived_modulePushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniformHigherDirectImageVanishing.lean, line 252. The attribute's comment: “the source's quantifier order -- one n from f alone, outside the base change, the module and the degree -- and step (2) of its proof, the reduction of an arbitrary base to a scheme base. No number is produced: hscheme (that bound over a scheme base: Stacks 0720, 0733 and 072C) and h03F3 (Stacks 03F3(1), needed by 03LX) are carried; Y quasi-compact not assumed”.

[Stacks, Tag 073G], with the scheme-base case carried. Let f : X ⟶ Y be a quasi-compact and quasi-separated morphism of algebraic spaces over S. Then there is a single degree n(X → Y) such that for every algebraic space Y', every morphism Y' ⟶ Y, every algebraic space X' making X' ⟶ X, X' ⟶ Y' a cartesian square over f, and every quasi-coherent 𝒪_{X'}-module 𝓕', the higher direct images R^q f'_*𝓕' vanish for q ≥ n(X → Y).

The quantifiers are the source's and in the source's order: n(X → Y) is produced once and for all from f, before any base change and before any coefficient module. The uniformity in Y' is what AlgebraicGeometry.Space.isZero_rightDerived_modulePushforward_of_schemeBase supplies; the integer itself comes from hscheme, the case of a base which is a scheme, which is not proved in this development.

theorem exists_forall_isZero_rightDerived_modulePushforward {X Y : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (hfqc : IsQuasiCompact B S hS f.hom) (hfqs : IsQuasiSeparated B S hS f.hom)
    (h03F3 : ∀ (Z W : AlgebraicSpaces B S hS) (i : W ⟶ Z) (hi : IsEtale B S hS i.hom),
      (etaleModulePullback.{u, u} B S hS i hi).PreservesInjectiveObjects)
    (hscheme : ∃ N : ℕ, SchemeBaseUniformVanishing B S hS f N) :
    ∃ N : ℕ, ∀ (Y' X' : AlgebraicSpaces B S hS) (g : Y' ⟶ Y) (i' : X' ⟶ X) (f' : X' ⟶ Y'),
      IsPullback i' f' f g →
      ∀ F' : Modules.{u, u} B S hS X'.1 X'.2, F'.IsQuasicoherentOnSite → ∀ q : ℕ, N ≤ q →
        have := hasInjectiveResolutions_modules B S hS X'.1 X'.2
        IsZero (((modulePushforward B S hS f').rightDerived q).obj F')

AlgebraicGeometry.Space.exists_forall_isZero_rightDerived_modulePushforward_of_representable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniformHigherDirectImageVanishing.lean, line 332. The attribute's comment: “the same for a REPRESENTABLE f, with h03F3 discharged: there the chartwise identification is Stacks 071Z, which proves Stacks 03F3(1). hscheme is still carried and Y quasi-compact is still not assumed”.

[Stacks, Tag 073G] for a representable morphism, with only the scheme-base case carried. Let f : X ⟶ Y be a representable, quasi-compact and quasi-separated morphism of algebraic spaces over S. Then there is a single degree n(X → Y) above which every higher direct image of every quasi-coherent module along every base change of f vanishes.

This is AlgebraicGeometry.Space.exists_forall_isZero_rightDerived_modulePushforward with the injective-preservation hypothesis h03F3 discharged by representability.

theorem exists_forall_isZero_rightDerived_modulePushforward_of_representable
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (hf : yoneda.relativelyRepresentable f.hom)
    (hfqc : IsQuasiCompact B S hS f.hom) (hfqs : IsQuasiSeparated B S hS f.hom)
    (hscheme : ∃ N : ℕ, SchemeBaseUniformVanishing B S hS f N) :
    ∃ N : ℕ, ∀ (Y' X' : AlgebraicSpaces B S hS) (g : Y' ⟶ Y) (i' : X' ⟶ X) (f' : X' ⟶ Y'),
      IsPullback i' f' f g →
      ∀ F' : Modules.{u, u} B S hS X'.1 X'.2, F'.IsQuasicoherentOnSite → ∀ q : ℕ, N ≤ q →
        have := hasInjectiveResolutions_modules B S hS X'.1 X'.2
        IsZero (((modulePushforward B S hS f').rightDerived q).obj F')

Tag 073H, a lemma

Tag 073H in the Stacks Project.

AlgebraicGeometry.Space.isZero_rightDerived_modulePushforward_of_isQuasicoherentOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineHigherPushforwardUnconditional.lean, line 44.

For an affine morphism f : X ⟶ Y of algebraic spaces over S, a quasi-coherent 𝒪_X-module 𝓕 and n > 0, the higher direct image vanishes: R^n f_* 𝓕 = 0.

theorem isZero_rightDerived_modulePushforward_of_isQuasicoherentOnSite
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (haff : IsAffineHom B S hS f.hom)
    (G : Modules.{u, u} B S hS X.1 X.2) (hG : G.IsQuasicoherentOnSite) (n : ℕ) (hn : 0 < n) :
    have := hasInjectiveResolutions_modules B S hS X.1 X.2
    IsZero (((modulePushforward B S hS f).rightDerived n).obj G)

AlgebraicGeometry.Space.isZero_rightDerived_modulePushforward_of_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineHigherPushforwardVanishing.lean, line 255. The attribute's comment: “the reduction of the source's statement along étale scheme charts, by Stacks 071Z; the affine case of the source's proof — the étale-site analogue of Stacks 01XC, that is Stacks 03DW — is carried as the hypothesis h03DW and is not proved”.

Stacks 073H with the affine case carried as h03DW.

If f : X ⟶ Y is an affine morphism of algebraic spaces over S whose chart base changes have vanishing degree-n higher direct images, then R^n f_* 𝓕 = 0.

This is the previous theorem with representability supplied by AlgebraicGeometry.Space.relativelyRepresentable_of_isAffineHom. The source's statement is this one for n > 0 and quasi-coherent 𝓕 with h03DW discharged; neither restriction on n nor on 𝓕 is used by the reduction, and h03DW is not available in this repository.

theorem isZero_rightDerived_modulePushforward_of_isAffineHom {X Y : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (hf : IsAffineHom B S hS f.hom)
    (F : Modules.{u, u} B S hS X.obj X.property) (n : ℕ)
    (h03DW : ChartwiseIsZeroHigherDirectImage B S hS f
      (relativelyRepresentable_of_isAffineHom B S hS f hf) F n) :
    have := hasInjectiveResolutions_modules B S hS X.obj X.property
    IsZero (((modulePushforward B S hS f).rightDerived n).obj F)

AlgebraicGeometry.Space.isZero_rightDerived_modulePushforward_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineHigherPushforwardVanishingUnconditional.lean, line 140.

Let f : X ⟶ Y be an affine morphism of algebraic spaces over a scheme S contained in a big fppf site B, and let 𝓕 be a quasi-coherent 𝒪_X-module. Then the higher direct images R^p f_* 𝓕 vanish for p > 0, the direct image being AlgebraicGeometry.Space.modulePushforward.

theorem isZero_rightDerived_modulePushforward_isAffineHom (f : X ⟶ Y)
    (haff : IsAffineHom B S hS f.hom) (F : Modules.{u, u} B S hS X.1 X.2)
    (hF : F.IsQuasicoherentOnSite) (p : ℕ) (hp : 0 < p) :
    IsZero (((modulePushforward B S hS f).rightDerived p).obj F)

AlgebraicGeometry.Space.isZero_rightDerived_modulePushforward_of_isAffineHom_of_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineMorphismHigherDirectImageVanishing.lean, line 99.

Stacks 073H. Let f : X ⟶ Y be an affine morphism of algebraic spaces over S and let 𝓕 be a quasi-coherent 𝒪_X-module. Then R^n f_*𝓕 = 0 for every n > 0.

The direct image along the representable f is the direct image along base change of étale charts (AlgebraicGeometry.Space.modulePushforwardChartIso); by Stacks 072W its higher direct images vanish once the cohomology of 𝓕 vanishes over the base changes of a covering family of each chart of Y; the affine charts form such a family, their base changes are affine charts of X because f is affine, and over an affine chart a quasi-coherent module has no higher cohomology.

theorem isZero_rightDerived_modulePushforward_of_isAffineHom_of_isQuasicoherent (f : X ⟶ Y)
    (hf : IsAffineHom B S hS f.hom) (F : Modules.{u, u} B S hS X.1 X.2)
    (hF : F.IsQuasicoherentOnSite) (n : ℕ) (hn : 0 < n) :
    have := hasInjectiveResolutions_modules B S hS X.1 X.2
    IsZero (((modulePushforward B S hS f).rightDerived n).obj F)

Tag 0D2U, a lemma

Tag 0D2U in the Stacks Project.

AlgebraicGeometry.Space.cohomologyCollapseIsoOfIsAffineHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineMorphismCohomologyCollapse.lean, line 171. The attribute's comment: “Leray collapse of the source's one-line proof; carries two unproved hypotheses, h03DW (073H's own) and h072Z (072Z via 0731(3)) -- see the notes”.

Stacks 0D2U with h03DW and h072Z carried.

Let f : X ⟶ Y be an affine morphism of algebraic spaces over S and 𝓕 an 𝒪_X-module. Then the cohomology of 𝓕 on X — computed as the derived functor of Γ(Y, f_* −) — is the cohomology of f_*𝓕 on Y, in every degree.

This is the previous isomorphism with representability supplied by AlgebraicGeometry.Space.relativelyRepresentable_of_isAffineHom, so that h03DW is exactly the hypothesis carried by AlgebraicGeometry.Space.isZero_rightDerived_modulePushforward_of_isAffineHom, the library's form of Stacks 073H. The source's statement is this one with h03DW and h072Z discharged, for a quasi-coherent 𝓕; quasi-coherence is not used, and neither hypothesis is available in this repository.

def cohomologyCollapseIsoOfIsAffineHom (f : X ⟶ Y) (hf : IsAffineHom B S hS f.hom)
    (F : Modules.{u, u} B S hS X.1 X.2)
    (h03DW : ∀ n, 0 < n → ChartwiseIsZeroHigherDirectImage B S hS f
      (relativelyRepresentable_of_isAffineHom B S hS f hf) F n)
    (h072Z : AcyclicPushforwardOfInjective B S hS f) (i : ℕ) :
    have := hasInjectiveResolutions_modules B S hS X.1 X.2
    have := enoughInjectives_modules B S hS Y.1 Y.2
    (((modulePushforward B S hS f ⋙ globalSectionsFunctor.{u + 1, u, u, u}
          ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS Y.1 Y.2).O))).rightDerived i).obj F ≅
      ((globalSectionsFunctor.{u + 1, u, u, u}
          ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS Y.1 Y.2).O))).rightDerived i).obj
        ((modulePushforward B S hS f).obj F))

AlgebraicGeometry.Space.cohomologyUliftIsoOfIsAffineHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineMorphismCohomologyOverRing.lean, line 359.

Stacks 0D2U. Let f : X ⟶ Y be an affine morphism of algebraic spaces over S and 𝓕 a quasi-coherent 𝒪_X-module. Then Hⁱ(X, 𝓕) = Hⁱ(Y, f_*𝓕) for every i ≥ 0.

The cohomology is that of the universe lifts of the two modules to the universe of the small étale sites, the universe in which AlgebraicGeometry.Space.eulerCharacteristic (Stacks 0DN1) is taken; the isomorphism is one of abelian groups, and of A-modules for any ring maps to the global functions compatible with f (AlgebraicGeometry.Space.cohomologyUliftOverRingIsoOfIsAffineHom).

def cohomologyUliftIsoOfIsAffineHom.{w} (haff : IsAffineHom B S hS f.hom)
    (G : Modules.{u, u} B S hS X.1 X.2) (hG : G.IsQuasicoherentOnSite) (q : ℕ) :
    (forget₂ _ AddCommGrpCat.{max (u + 1) w}).obj
        ((globalModuleCohomology.{u + 1, u, u, w}
          ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS X.1 X.2).O)) q).obj
          (SheafOfModules.uliftForPresentation.{u + 1, u, u, u, max (u + 1) w} G)) ≅
      (forget₂ _ AddCommGrpCat.{max (u + 1) w}).obj
        ((globalModuleCohomology.{u + 1, u, u, w}
          ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS Y.1 Y.2).O)) q).obj
          (SheafOfModules.uliftForPresentation.{u + 1, u, u, u, max (u + 1) w}
            ((modulePushforward B S hS f).obj G)))

AlgebraicGeometry.Space.cohomologyCollapseIsoOfIsFlatOfIsAffineHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatAffineCohomologyCollapse.lean, line 78. The attribute's comment: “for a FLAT affine morphism, with both of 0D2U's hypotheses discharged; flatness is not the source's hypothesis and is used only to reach 072Z's conclusion through 0730 instead -- see the notes”.

Let f : X ⟶ Y be a flat affine morphism of algebraic spaces over S and 𝓕 a quasi-coherent 𝒪_X-module. Then for every i the i-th right derived functor of Γ(Y, f_*−) at 𝓕 is isomorphic to the i-th cohomology of f_*𝓕 on Y.

def cohomologyCollapseIsoOfIsFlatOfIsAffineHom (f : X ⟶ Y) (haff : IsAffineHom B S hS f.hom)
    (hflat : IsFlat B S hS f.hom) (F : Modules.{u, u} B S hS X.1 X.2)
    (hF : F.IsQuasicoherentOnSite) (i : ℕ) :
    have := hasInjectiveResolutions_modules B S hS X.1 X.2
    have := enoughInjectives_modules B S hS Y.1 Y.2
    (((modulePushforward B S hS f ⋙ globalSectionsFunctor.{u + 1, u, u, u}
          (ringSheaf (smallEtaleRingedSite B S hS Y.1 Y.2).O)).rightDerived i).obj F ≅
      ((globalSectionsFunctor.{u + 1, u, u, u}
          (ringSheaf (smallEtaleRingedSite B S hS Y.1 Y.2).O)).rightDerived i).obj
        ((modulePushforward B S hS f).obj F))

Declarations registered for the tag:

• AlgebraicGeometry.Space.cohomologyIsoOfIsAffineHom, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/AffineMorphismCohomologyCollapseUnconditional.lean, line 128 (StacksFrontier).

Sources

• Section 69.8, Tag 073F
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.exists_forall_isZero_rightDerived_modulePushforward_of_qcqs · AlgebraicGeometry.Space.exists_forall_isZero_rightDerived_modulePushforward · AlgebraicGeometry.Space.exists_forall_isZero_rightDerived_modulePushforward_of_representable · AlgebraicGeometry.Space.isZero_rightDerived_modulePushforward_of_isQuasicoherentOnSite · AlgebraicGeometry.Space.isZero_rightDerived_modulePushforward_of_isAffineHom · AlgebraicGeometry.Space.isZero_rightDerived_modulePushforward_isAffineHom · AlgebraicGeometry.Space.isZero_rightDerived_modulePushforward_of_isAffineHom_of_isQuasicoherent · AlgebraicGeometry.Space.cohomologyCollapseIsoOfIsAffineHom

Section69.9 Cohomology with support in a closed subspace#

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

Tag 0A4L, the section

Tag 0A4L in the Stacks Project.

AlgebraicGeometry.Space.derivedSectionsWithSupportOnClosedSubspace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DerivedSectionsWithSupportEquivalence.lean, line 131. The attribute's comment: “the derived functor R𝓗_Z on unbounded derived categories”.

The derived functor R𝓗_Z : D(X_étale) ⥤ D(Z_étale), on the unbounded derived categories of abelian sheaves on small étale sites: the total right derived functor of the functor 𝓗_Z of sections with support in the point set of a closed immersion i : Z ⟶ X.

The bounded below version is AlgebraicGeometry.Space.derivedSectionsWithSupportInClosedSubspace.

def derivedSectionsWithSupportOnClosedSubspace :
    smallEtaleDerivedCategory.{u + 1} B S hS X ⥤ smallEtaleDerivedCategory.{u + 1} B S hS Z

AlgebraicGeometry.Space.sectionsWithSupportSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SectionsWithSupport.lean, line 280. The attribute's comment: “the subsheaf of sections with support in a closed subspace”.

Stacks 0A4L. The abelian subsheaf of sections supported on a set T of points: over an étale chart it consists of the sections of F whose support maps into T.

For T the point set of a closed immersion i : Z ⟶ X this is the sheaf H_Z(F) of the source, before it is viewed on the small étale site of Z.

def sectionsWithSupportSheaf (T : Set (points B S hS X))
    (F : Sheaf (SmallEtale.topology B S hS X) AddCommGrpCat.{v}) :
    Sheaf (SmallEtale.topology B S hS X) AddCommGrpCat.{v}

AlgebraicGeometry.Space.sectionsWithSupport, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SectionsWithSupport.lean, line 362. The attribute's comment: “sections with support in a closed subspace, functorially”.

Stacks 0A4L. Sections with support on a fixed set of points, as an endofunctor of the abelian sheaves on the small étale site of X.

def sectionsWithSupport (T : Set (points B S hS X)) :
    Sheaf (SmallEtale.topology B S hS X) AddCommGrpCat.{v} ⥤
      Sheaf (SmallEtale.topology B S hS X) AddCommGrpCat.{v}

AlgebraicGeometry.Space.sectionsWithSupportInClosedSubspace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SectionsWithSupport.lean, line 489. The attribute's comment: “the functor H_Z on abelian sheaves of the small étale site”.

Stacks 0A4L. The functor H_Z of a closed immersion i : Z ⟶ X of algebraic spaces: the sections with support in |Z|, viewed on the small étale site of Z through the inverse image along i.

The first factor is the subsheaf of F of sections whose support maps into the point set of i, which is the source's H_Z(F); the second is the inverse image along i, which is what the source means by viewing that subsheaf on Z_étale.

def sectionsWithSupportInClosedSubspace (i : Z ⟶ X)
    (hi : IsClosedImmersion B S hS i.hom) :
    Sheaf (SmallEtale.topology B S hS X.1) AddCommGrpCat.{u + 1} ⥤
      Sheaf (SmallEtale.topology B S hS Z.1) AddCommGrpCat.{u + 1}

Tag 0A4M, a lemma

Tag 0A4M in the Stacks Project.

AlgebraicGeometry.Space.injective_sectionsWithSupportInClosedSubspace_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/InjectiveSectionsWithSupport.lean, line 62.

Stacks 0A4M. Let S be a scheme, let i : Z ⟶ X be a closed immersion of algebraic spaces over S and let I be an injective abelian sheaf on the small étale site of X. Then the sections of I with support in |Z| form an injective abelian sheaf on the small étale site of Z.

theorem injective_sectionsWithSupportInClosedSubspace_of_isClosedImmersion
    (I : Sheaf (SmallEtale.topology B S hS X.1) AddCommGrpCat.{u + 1}) [Injective I] :
    Injective ((sectionsWithSupportInClosedSubspace B S hS i hi).obj I)

Tag 0A4N, a lemma

Tag 0A4N in the Stacks Project.

AlgebraicGeometry.Space.isZero_rightDerivedPlus_sectionsWithSupportInClosedSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SectionsWithSupportVanishing.lean, line 115.

Stacks 0A4N. Let S be a scheme, let i : Z ⟶ X be a closed immersion of algebraic spaces over S and let G be an injective abelian sheaf on the small étale site of Z. Then the higher sections with support in |Z| of the direct image i_*G vanish: H^p_Z(i_*G) = 0 for p > 0.

The direct image of an injective abelian sheaf is injective, and the higher right derived functors of an additive functor vanish on an injective object.

theorem isZero_rightDerivedPlus_sectionsWithSupportInClosedSubspace (i : Z ⟶ X)
    (hi : IsClosedImmersion B S hS i.hom)
    (G : Sheaf (SmallEtale.topology B S hS Z.1) AddCommGrpCat.{u + 1}) [Injective G]
    (p : ℤ) (hp : 0 < p) :
    IsZero (((sectionsWithSupportInClosedSubspace B S hS i hi).rightDerivedPlus p).obj
      ((smallEtaleAbelianPushforward.{u + 1} B S hS i hi.rep).obj G))

Tag 0A4P, a lemma

Tag 0A4P in the Stacks Project.

AlgebraicGeometry.Space.closedCohomologyWithSupportEtaleExcisionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GlobalSectionsWithSupportEtaleExcision.lean, line 368. The attribute's comment: “conclusion (2), every degree q: H^q_Z(Y, F) = H^q_{f⁻¹Z}(X, f⁻¹F) for f étale and f⁻¹Z ≅ Z”.

Stacks 0A4P, conclusion (2): the global cohomology-with-support identity, in every degree. Let f : X ⟶ Y be an étale morphism of algebraic spaces over S, let iY : Z ⟶ Y be a closed subspace and let iX : W ⟶ X be its inverse image, presented by the cartesian square hk and carried isomorphically onto Z by k. Then for every abelian sheaf F on the small étale site of Y and every degree q,

H^q_Z(Y, F) = H^q_{f⁻¹Z}(X, f⁻¹F),

naturally in F.

In degree zero this is AlgebraicGeometry.Space.closedGlobalSectionsWithSupportEtaleExcisionIso, the source's excision argument on the spaces-étale site. The passage to all degrees is the source's own reasoning, Stacks 015Z: inverse image along an étale morphism is exact and preserves injective abelian sheaves, so it comes out of the right derived functor of the composite.

def closedCohomologyWithSupportEtaleExcisionIso (f : X ⟶ Y) (hf : IsEtale B S hS f.hom)
    (iY : Z ⟶ Y) (hiY : IsClosedImmersion B S hS iY.hom) (iX : W ⟶ X) (k : W ⟶ Z) [IsIso k]
    (hk : IsPullback k.hom iX.hom iY.hom f.hom) (q : ℕ) :
    closedCohomologyWithSupport B S hS iY q ≅
      etaleAbelianRestriction.{u + 1} B S hS f hf ⋙
        closedCohomologyWithSupport B S hS iX q

AlgebraicGeometry.Space.closedSectionsWithSupportEtaleRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SectionsWithSupportEtaleLocal.lean, line 192. The attribute's comment: “degree zero, on the ambient site: f⁻¹ H_Z(F) = H_{f⁻¹Z}(f⁻¹F)”.

Let f : X ⟶ Y be an étale morphism of algebraic spaces over S, let Z ⟶ Y be a subspace and let f⁻¹Z ⟶ X be its inverse image, presented by the cartesian square hk. Then inverse image along f identifies the sections with support in Z of an abelian sheaf F on Y_étale with the sections with support in f⁻¹Z of f⁻¹F: f⁻¹ ℋ_Z(F) = ℋ_{f⁻¹Z}(f⁻¹F) as subsheaves of f⁻¹F on X_étale.

def closedSectionsWithSupportEtaleRestrictionIso {W Z : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (hf : IsEtale B S hS f.hom) (iY : Z ⟶ Y) (iX : W ⟶ X) (k : W ⟶ Z)
    (hk : IsPullback k.hom iX.hom iY.hom f.hom) :
    closedSectionsWithSupport.{v} B S hS iY ⋙ etaleAbelianRestriction.{v} B S hS f hf ≅
      etaleAbelianRestriction.{v} B S hS f hf ⋙ closedSectionsWithSupport.{v} B S hS iX

AlgebraicGeometry.Space.closedHigherSectionsWithSupportEtaleRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SectionsWithSupportEtaleLocalHigher.lean, line 465. The attribute's comment: “every degree q, on the ambient site: f⁻¹ H^q_Z(F) = H^q_{f⁻¹Z}(f⁻¹F)”.

Stacks 0A4P, the sheaf-level conclusion in every degree, for a subspace. Let f : X ⟶ Y be an étale morphism of algebraic spaces over S, let iY : Z ⟶ Y be a subspace and let iX : W ⟶ X be its inverse image, presented by the cartesian square hk. Then inverse image along f identifies the higher sections with support in Z with the higher sections with support in f⁻¹Z, in every degree q: f⁻¹ H^q_Z(F) = H^q_{f⁻¹Z}(f⁻¹F) as abelian sheaves on X_étale.

As in degree zero, the point sets match by Stacks 03H4, and the source's further hypothesis that f⁻¹Z → Z is an isomorphism — which is what lets the source read both sides as sheaves on Z itself — plays no part in the identification of the ambient sheaves proved here.

def closedHigherSectionsWithSupportEtaleRestrictionIso {W Z : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (hf : IsEtale B S hS f.hom) (iY : Z ⟶ Y) (iX : W ⟶ X) (k : W ⟶ Z)
    (hk : IsPullback k.hom iX.hom iY.hom f.hom) (q : ℕ) :
    (closedSectionsWithSupport.{u + 1} B S hS iY).rightDerived q ⋙
        etaleAbelianRestriction.{u + 1} B S hS f hf ≅
      etaleAbelianRestriction.{u + 1} B S hS f hf ⋙
        (closedSectionsWithSupport.{u + 1} B S hS iX).rightDerived q

AlgebraicGeometry.Space.closedHigherSectionsWithSupportOnSubspaceIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleAbelianInverseImageSquare.lean, line 355. The attribute's comment: “every degree q, read on the subspaces: k⁻¹(H^q_Z(F)|_Z) = H^q_{f⁻¹Z}(f⁻¹F)|_{f⁻¹Z}”.

Stacks 0A4P, in every degree, read on the subspaces. Let f : X ⟶ Y be an étale morphism of algebraic spaces over S, let iY : Z ⟶ Y be a subspace and let iX : W ⟶ X be its inverse image, presented by the cartesian square hk with k : W ⟶ Z. Then, in every degree q and naturally in the abelian sheaf F on Y_étale,

k⁻¹(H^q_Z(F)|_Z) = H^q_{f⁻¹Z}(f⁻¹F)|_{f⁻¹Z}

as abelian sheaves on W = f⁻¹Z. This is the form of the conclusion the source states — the sheaf identity read on the subspace rather than on the ambient small étale site — with the source's hypothesis that k is an isomorphism removed: under that hypothesis k⁻¹ is an equivalence and the left-hand side is the source's H^q_Z(F) read on Z.

The ambient-site statement is AlgebraicGeometry.Space.closedHigherSectionsWithSupportEtaleRestrictionIso. What is added is one whiskering by inverse image along iX, after which AlgebraicGeometry.Space.smallToposMorphism_abelianInverseImageIso — Stacks 03LQ at abelian coefficients — turns restriction along postcomposition with f into the inverse image of the morphism of small étale topoi, and AlgebraicGeometry.Space.smallEtaleAbelianInverseImageSquareIsoOfComm exchanges the two routes around the square. Only commutativity of hk is used, through CategoryTheory.ObjectProperty.hom_ext.

def closedHigherSectionsWithSupportOnSubspaceIso {W Z : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (hf : IsEtale B S hS f.hom) (iY : Z ⟶ Y) (iX : W ⟶ X) (k : W ⟶ Z)
    (hk : IsPullback k.hom iX.hom iY.hom f.hom) (q : ℕ) :
    (closedSectionsWithSupport.{u + 1} B S hS iY).rightDerived q ⋙
        (Sites.abelianInverseImage (smallToposMorphism B S hS iY) ⋙
          Sites.abelianInverseImage (smallToposMorphism B S hS k)) ≅
      etaleAbelianRestriction.{u + 1} B S hS f hf ⋙
        ((closedSectionsWithSupport.{u + 1} B S hS iX).rightDerived q ⋙
          Sites.abelianInverseImage (smallToposMorphism B S hS iX))

AlgebraicGeometry.Space.closedHigherSectionsWithSupportOnZIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleAbelianInverseImageSquare.lean, line 405. The attribute's comment: “every degree q, on Z itself, with the source's hypothesis that k is an iso”.

Stacks 0A4P, in every degree, on Z itself, with the source's hypothesis that k : f⁻¹Z ⟶ Z is an isomorphism. Let f : X ⟶ Y be an étale morphism of algebraic spaces over S, let iY : Z ⟶ Y be a subspace and let iX : W ⟶ X be its inverse image, presented by the cartesian square hk with k : W ⟶ Z an isomorphism. Then, in every degree q and naturally in the abelian sheaf F on Y_étale,

H^q_Z(F)|_Z = H^q_{f⁻¹Z}(f⁻¹F)|_{f⁻¹Z}

as abelian sheaves on Z, the right-hand side read on Z through k — that is, pulled back along inv k : Z ⟶ f⁻¹Z. This is the reading of the conclusion that the source states.

It is AlgebraicGeometry.Space.closedHigherSectionsWithSupportOnSubspaceIso, which states the same identity on f⁻¹Z and assumes nothing about k, with AlgebraicGeometry.Space.smallToposMorphism_comp_abelianInverseImage used twice to cancel k⁻¹ against (inv k)⁻¹: once at inv k ≫ k = 𝟙 Z, which turns the composite into the inverse image along 𝟙 Z, and once at 𝟙 Z ≫ iY = iY, which absorbs that into the inverse image along iY. No unit law for AlgebraicGeometry.Space.smallToposMorphism is needed: the composition isomorphism at the second of those two identities does the cancelling without the inverse image along 𝟙 Z ever being identified with the identity functor.

Every intermediate isomorphism is named with its type written out and every reassociation is an explicit CategoryTheory.Functor.associator, for the reason recorded in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleRestrictionInverseImage.lean: although CategoryTheory.Functor.assoc is an equality, leaving a functor composition to definitional unfolding here hands the unifier the small étale inverse image to whnf and the elaboration runs out of heartbeats.

def closedHigherSectionsWithSupportOnZIso {W Z : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (hf : IsEtale B S hS f.hom) (iY : Z ⟶ Y) (iX : W ⟶ X) (k : W ⟶ Z) [IsIso k]
    (hk : IsPullback k.hom iX.hom iY.hom f.hom) (q : ℕ) :
    (closedSectionsWithSupport.{u + 1} B S hS iY).rightDerived q ⋙
        Sites.abelianInverseImage (smallToposMorphism B S hS iY) ≅
      etaleAbelianRestriction.{u + 1} B S hS f hf ⋙
        ((closedSectionsWithSupport.{u + 1} B S hS iX).rightDerived q ⋙
          (Sites.abelianInverseImage (smallToposMorphism B S hS iX) ⋙
            Sites.abelianInverseImage (smallToposMorphism B S hS (inv k))))

Tag 0AEI, a lemma

Tag 0AEI in the Stacks Project.

AlgebraicGeometry.Space.derivedSmallEtalePushforwardSupportedEquivalence_inverse_derivedSectionsWithSupport, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DerivedSectionsWithSupportEquivalence.lean, line 224. The attribute's comment: “the identification of the quasi-inverse with the derived sections with support R𝓗_Z, the second description in the displayed formula”.

The quasi-inverse is the derived sections with support. The quasi-inverse of the equivalence D(Z_étale) ≌ D_{|Z|}(X_étale) induced by the direct image along a closed immersion i : Z ⟶ X of algebraic spaces over S is the derived functor R𝓗_Z of sections with support in |Z|, restricted to D_{|Z|}(X_étale).

def derivedSmallEtalePushforwardSupportedEquivalence_inverse_derivedSectionsWithSupport :
    (derivedSmallEtalePushforwardSupportedEquivalence B S hS i hi).inverse ≅
      (cohomologySupportedOn.{u + 1} B S hS X
          (Set.range (pointsMap B S hS Z.1 i.hom))).ι ⋙
        derivedSectionsWithSupportOnClosedSubspace B S hS i hi

AlgebraicGeometry.Space.derivedSmallEtaleInverseImage_iso_derivedSectionsWithSupport_of_supported, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DerivedSectionsWithSupportEquivalence.lean, line 258. The attribute's comment: “the displayed equality i^{-1}|_{D_Z} = R𝓗_Z|_{D_{|Z|}} of the two descriptions of the quasi-inverse”.

The inverse image agrees with the derived sections with support. On the subcategory D_{|Z|}(X_étale) of complexes of abelian sheaves whose cohomology sheaves are supported on the point set of a closed immersion i : Z ⟶ X, the inverse image i^{-1} and the derived functor R𝓗_Z of sections with support in |Z| agree:

i^{-1}|_{D_Z(X_étale)} = R𝓗_Z|_{D_{|Z|}(X_étale)}.

Both are the quasi-inverse of the equivalence AlgebraicGeometry.Space.derivedSmallEtalePushforwardSupportedEquivalence.

def derivedSmallEtaleInverseImage_iso_derivedSectionsWithSupport_of_supported :
    letI := additive_smallEtaleAbelianInverseImage B S hS i hi.rep
    letI := preservesFiniteLimits_smallEtaleAbelianInverseImage B S hS i hi.rep
    letI := preservesFiniteColimits_smallEtaleAbelianInverseImage B S hS i hi.rep
    (cohomologySupportedOn.{u + 1} B S hS X
          (Set.range (pointsMap B S hS Z.1 i.hom))).ι ⋙
        (smallEtaleAbelianInverseImage B S hS i hi.rep).mapDerivedCategory ≅
      (cohomologySupportedOn.{u + 1} B S hS X
          (Set.range (pointsMap B S hS Z.1 i.hom))).ι ⋙
        derivedSectionsWithSupportOnClosedSubspace B S hS i hi

AlgebraicGeometry.Space.isRightDerivedFunctor_mapDerivedCategory_smallEtaleAbelianPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DerivedSectionsWithSupportEquivalence.lean, line 279. The attribute's comment: “Ri_ = i_, the pushforward along a closed immersion being its own right derived functor”.

Ri_* = i_*. For a closed immersion i, the degreewise action of the direct image i_* on unbounded derived categories is the right derived functor Ri_*.

theorem isRightDerivedFunctor_mapDerivedCategory_smallEtaleAbelianPushforward :
    letI := preservesFiniteColimits_smallEtaleAbelianPushforward_of_isClosedImmersion B S hS i hi
    (smallEtaleAbelianPushforward.{u + 1} B S hS i hi.rep).mapDerivedCategory.IsRightDerivedFunctor
      (smallEtaleAbelianPushforward.{u + 1} B S hS i hi.rep).mapDerivedCategoryFactorsh.inv
      (HomotopyCategory.quasiIso _ (ComplexShape.up ℤ))

AlgebraicGeometry.Space.fullyFaithfulDerivedSmallEtaleAbelianPushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SupportedComplexesEquivalence.lean, line 113. The attribute's comment: “full faithfulness of the pushforward”.

Stacks 0AEI: the pushforward is fully faithful. For a closed immersion i : Z ⟶ X of algebraic spaces over S the functor D(Z_étale) ⥤ D(X_étale) induced by the exact direct image i_* of abelian sheaves is fully faithful.

def fullyFaithfulDerivedSmallEtaleAbelianPushforward :
    letI := additive_smallEtaleAbelianInverseImage B S hS i hi.rep
    letI := preservesFiniteColimits_smallEtaleAbelianPushforward_of_isClosedImmersion B S hS i hi
    (smallEtaleAbelianPushforward.{u + 1} B S hS i hi.rep).mapDerivedCategory.FullyFaithful

AlgebraicGeometry.Space.essImage_mapDerivedCategory_of_cohomologySupportedOn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SupportedComplexesEquivalence.lean, line 189. The attribute's comment: “essential surjectivity onto the supported subcategory”.

Stacks 0AEI: essential surjectivity onto the supported subcategory. A complex of abelian sheaves on the small étale site of X all of whose cohomology sheaves are supported on the point set of a closed immersion i : Z ⟶ X is isomorphic in D(X_étale) to the direct image of a complex on Z_étale.

theorem essImage_mapDerivedCategory_of_cohomologySupportedOn
    (K : smallEtaleDerivedCategory.{u + 1} B S hS X)
    (hK : cohomologySupportedOn.{u + 1} B S hS X
      (Set.range (pointsMap B S hS Z.1 i.hom)) K) :
    letI := preservesFiniteColimits_smallEtaleAbelianPushforward_of_isClosedImmersion B S hS i hi
    (smallEtaleAbelianPushforward.{u + 1} B S hS i hi.rep).mapDerivedCategory.essImage K

AlgebraicGeometry.Space.derivedSmallEtalePushforwardSupportedEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SupportedComplexesEquivalence.lean, line 208. The attribute's comment: “the equivalence of D(Z_étale) with D_{|Z|}(X_étale)”.

Stacks 0AEI: the equivalence. Direct image along a closed immersion i : Z ⟶ X of algebraic spaces over S induces an equivalence of D(Z_étale) with the full subcategory D_{|Z|}(X_étale) of D(X_étale) of complexes whose cohomology sheaves are all supported on the point set of Z.

def derivedSmallEtalePushforwardSupportedEquivalence :
    smallEtaleDerivedCategory.{u + 1} B S hS Z ≌
      smallEtaleDerivedCategoryOnClosedSubspace.{u + 1} B S hS i

AlgebraicGeometry.Space.derivedSmallEtalePushforwardSupportedEquivalence_functor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SupportedComplexesEquivalence.lean, line 230. The attribute's comment: “the equivalence is induced by the pushforward”.

Stacks 0AEI: the equivalence is induced by the pushforward. Composed with the inclusion of D_{|Z|}(X_étale) into D(X_étale), the forward functor of the equivalence is the functor induced by the exact direct image i_*.

def derivedSmallEtalePushforwardSupportedEquivalence_functor :
    letI := preservesFiniteColimits_smallEtaleAbelianPushforward_of_isClosedImmersion B S hS i hi
    (derivedSmallEtalePushforwardSupportedEquivalence B S hS i hi).functor ⋙
        (cohomologySupportedOn.{u + 1} B S hS X (Set.range (pointsMap B S hS Z.1 i.hom))).ι ≅
      (smallEtaleAbelianPushforward.{u + 1} B S hS i hi.rep).mapDerivedCategory

AlgebraicGeometry.Space.derivedSmallEtalePushforwardSupportedEquivalence_inverse, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SupportedComplexesEquivalence.lean, line 245. The attribute's comment: “the identification of the quasi-inverse with the inverse image”.

Stacks 0AEI: the quasi-inverse is the inverse image. The quasi-inverse of the equivalence is the functor induced by the exact inverse image i^{-1}, restricted to D_{|Z|}(X_étale).

def derivedSmallEtalePushforwardSupportedEquivalence_inverse :
    letI := additive_smallEtaleAbelianInverseImage B S hS i hi.rep
    letI := preservesFiniteLimits_smallEtaleAbelianInverseImage B S hS i hi.rep
    letI := preservesFiniteColimits_smallEtaleAbelianInverseImage B S hS i hi.rep
    (derivedSmallEtalePushforwardSupportedEquivalence B S hS i hi).inverse ≅
      (cohomologySupportedOn.{u + 1} B S hS X
          (Set.range (pointsMap B S hS Z.1 i.hom))).ι ⋙
        (smallEtaleAbelianInverseImage B S hS i hi.rep).mapDerivedCategory

Sources

• Section 69.9, Tag 0A4L
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.derivedSectionsWithSupportOnClosedSubspace · AlgebraicGeometry.Space.sectionsWithSupportSheaf · AlgebraicGeometry.Space.sectionsWithSupport · AlgebraicGeometry.Space.sectionsWithSupportInClosedSubspace · AlgebraicGeometry.Space.injective_sectionsWithSupportInClosedSubspace_of_isClosedImmersion · AlgebraicGeometry.Space.isZero_rightDerivedPlus_sectionsWithSupportInClosedSubspace · AlgebraicGeometry.Space.closedCohomologyWithSupportEtaleExcisionIso · AlgebraicGeometry.Space.closedSectionsWithSupportEtaleRestrictionIso

Section69.10 Vanishing above the dimension#

Section 69.10 of the Stacks Project, Tag 0A4Q. 1 tag here is carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0A4R, a lemma

Tag 0A4R in the Stacks Project.

AlgebraicGeometry.subsingleton_smallEtaleCohomology_quasicoherent_of_topologicalKrullDim_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/VanishingAboveTheDimension.lean, line 261. The attribute's comment: “clause (1) for a scheme: for a quasi-compact quasi-separated scheme X of dimension at most d and a quasi-coherent module F, the small étale cohomology of the associated abelian sheaf Fᵃ vanishes above degree d”.

Stacks 0A4R, clause (1), for a quasi-compact quasi-separated scheme. Let X be a quasi-compact quasi-separated scheme whose dimension — the Krull dimension of its underlying topological space — is at most d, and let F be a quasi-coherent 𝒪_X-module. Then the small étale cohomology of the associated abelian sheaf Fᵃ of Stacks 03DU vanishes in every degree q > d.

The proof is the base case of the source's induction. The space of X is spectral by Stacks 094L, so clause (1) of Stacks 0A3G makes the Zariski cohomology of the abelian sheaf underlying F vanish above d (AlgebraicGeometry.subsingleton_zariskiCohomology_of_topologicalKrullDim_le); Stacks 03P2 for 𝒞 = S_étale — which is the comparison the source cites as Stacks 03DW, available here in all degrees — transports that vanishing to the small étale site.

Quasi-coherence cannot be dropped: on X = Spec ℝ, which is zero-dimensional, the constant abelian sheaf ℤ/2 on X_étale has H^q(X_étale, ℤ/2) = ℤ/2 for every q > 0.

theorem subsingleton_smallEtaleCohomology_quasicoherent_of_topologicalKrullDim_le
    (X : Scheme.{u}) [CompactSpace X] [QuasiSeparatedSpace X] (F : X.Modules)
    [F.IsQuasicoherent] (d q : ℕ) (hdim : topologicalKrullDim X ≤ (d : WithBot ℕ∞))
    (hq : d < q) :
    Subsingleton (Sheaf.H' (smallEtaleAssociatedSheaf X F) q ((opensToEtale X).obj ⊤))

AlgebraicGeometry.Space.isZero_rightDerived_globalSectionsFunctor_of_dimension_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/VanishingAboveTheDimensionQcqs.lean, line 120. The attribute's comment: “part (1)”.

Stacks 0A4R, clause (1). Let S be a scheme and X a quasi-compact quasi-separated algebraic space over S with dim X ≤ d, and let F be a quasi-coherent 𝒪_X-module. Then Hᑫ(X, F) = 0 for every q > d.

The dimension bound d ranges over WithBot ℕ∞, where the dimension of an algebraic space lives, so it covers every integer of the source: for d = ⊤ there is nothing to prove, and a negative d (in particular d = ⊥) forces X to have no points, so that every module on X is zero. For a natural number d this is the induction of Stacks 08GP along elementary distinguished squares, AlgebraicGeometry.Space.isZero_rightDerived_globalSectionsAb_of_dimension_le; the cohomology is that of the module over the global functions, and it vanishes exactly when the underlying abelian group does.

theorem isZero_rightDerived_globalSectionsFunctor_of_dimension_le (B : BigFppfSite.{u})
    (S : Scheme.{u}) (hS : B.Contains S) (X : AlgebraicSpaces B S hS)
    (hXqc : IsQuasiCompactSpace B S hS X.1)
    (hXqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal X.1) (d : WithBot ℕ∞)
    (hdim : dimension B S hS X.1 X.2 ≤ d) (F : Modules.{u, u} B S hS X.1 X.2)
    (hF : F.IsQuasicoherentOnSite) (q : ℕ) (hq : d < q) :
    IsZero (((globalSectionsFunctor.{u + 1, u, u, u} (Stacks.SheafOfModules.Tensor.ringSheaf
      (smallEtaleRingedSite B S hS X.1 X.2).O)).rightDerived q).obj F)

AlgebraicGeometry.Space.surjective_cohomologyRestriction_of_dimension_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/VanishingAboveTheDimensionQcqs.lean, line 162. The attribute's comment: “part (2)”.

Stacks 0A4R, clause (2). Let S be a scheme and X a quasi-compact quasi-separated algebraic space over S with dim X ≤ d, and let F be a quasi-coherent 𝒪_X-module. Then the restriction map H^d(X, F) ⟶ H^d(U, F|_U) is surjective for every quasi-compact open subspace U of X.

The open subspace is given by an open immersion j : U ⟶ X from a quasi-compact algebraic space, which covers every quasi-compact open subspace (through its inclusion) and every space isomorphic to one; the restriction map is AlgebraicGeometry.Space.cohomologyRestriction, the right derived map of Γ(X, -) ⟶ Γ(U, (-)|_U). The bound d is a natural number: for a negative integer d the source's statement is about H^d, which is zero. The proof is AlgebraicGeometry.Space.epi_rightDerived_globalSectionsAbRestriction_of_dimension_le, the induction of Stacks 08GP with the Mayer–Vietoris sequence of Stacks 08GW in place of the excision of Stacks 0A4P.

theorem surjective_cohomologyRestriction_of_dimension_le (B : BigFppfSite.{u})
    (S : Scheme.{u}) (hS : B.Contains S) (X : AlgebraicSpaces B S hS)
    (hXqc : IsQuasiCompactSpace B S hS X.1)
    (hXqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal X.1) (d : ℕ)
    (hdim : dimension B S hS X.1 X.2 ≤ d) {U : AlgebraicSpaces B S hS} (j : U ⟶ X)
    (hj : IsOpenImmersion B S hS j.hom) (hUqc : IsQuasiCompactSpace B S hS U.1)
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : F.IsQuasicoherentOnSite) :
    Function.Surjective
      (cohomologyRestriction B S hS j (isEtale_of_isOpenImmersion B S hS hj) F d)

AlgebraicGeometry.Space.isZero_rightDerived_globalSectionsAbRestrictionKer_of_dimension_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/VanishingAboveTheDimensionQcqs.lean, line 193. The attribute's comment: “part (3)”.

Stacks 0A4R, clause (3). Let S be a scheme and X a quasi-compact quasi-separated algebraic space over S with dim X ≤ d, and let F be a quasi-coherent 𝒪_X-module. Then H^q_Z(X, F) = 0 for every q > d and every closed subspace Z ⊆ X whose complement is quasi-compact.

The complement U = X ∖ Z is given by an open immersion j : U ⟶ X from a quasi-compact algebraic space, and H^q_Z(X, -) is the q-th right derived functor of Γ_Z(X, -) = Ker(Γ(X, -) ⟶ Γ(U, (-)|_U)), AlgebraicGeometry.Space.globalSectionsAbRestrictionKer; this depends on Z only through its open complement, which is how the source's H^q_Z depends on Z. As in clause (1) the bound d ranges over WithBot ℕ∞; a negative d forces X to have no points. For a natural number d the proof is the source's formal argument: in the long exact sequence of the pair H^{q-1}(X, F) ⟶ H^{q-1}(U, F) ⟶ H^q_Z(X, F) ⟶ H^q(X, F) the last group vanishes by clause (1), and the first map is onto, by clause (2) when q - 1 = d and because its target vanishes by clause (1) on the quasi-compact quasi-separated space U when q - 1 > d.

theorem isZero_rightDerived_globalSectionsAbRestrictionKer_of_dimension_le (B : BigFppfSite.{u})
    (S : Scheme.{u}) (hS : B.Contains S) (X : AlgebraicSpaces B S hS)
    (hXqc : IsQuasiCompactSpace B S hS X.1)
    (hXqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal X.1) (d : WithBot ℕ∞)
    (hdim : dimension B S hS X.1 X.2 ≤ d) {U : AlgebraicSpaces B S hS} (j : U ⟶ X)
    (hj : IsOpenImmersion B S hS j.hom) (hUqc : IsQuasiCompactSpace B S hS U.1)
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : F.IsQuasicoherentOnSite) (q : ℕ) (hq : d < q) :
    IsZero (((globalSectionsAbRestrictionKer B S hS j
      (isEtale_of_isOpenImmersion B S hS hj)).rightDerived q).obj F)

Sources

• Section 69.10, Tag 0A4Q
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.subsingleton_smallEtaleCohomology_quasicoherent_of_topologicalKrullDim_le · AlgebraicGeometry.Space.isZero_rightDerived_globalSectionsFunctor_of_dimension_le · AlgebraicGeometry.Space.surjective_cohomologyRestriction_of_dimension_le · AlgebraicGeometry.Space.isZero_rightDerived_globalSectionsAbRestrictionKer_of_dimension_le

Section69.11 Cohomology and base change, I#

Section 69.11 of the Stacks Project, Tag 073I. 4 tags here are carried by 14 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 073J, an equation

Tag 073J in the Stacks Project.

AlgebraicGeometry.Space.BaseChangeDiagram, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohomologyBaseChange.lean, line 167. The attribute's comment: “the cartesian square and its coefficient”.

The base-change diagram for cohomology of algebraic spaces: a cartesian square of algebraic spaces over S, together with a quasi-coherent 𝒪_X-module 𝓕 on the source X of the morphism f that is being base changed.

structure BaseChangeDiagram

AlgebraicGeometry.Space.BaseChangeDiagram.pulledBack, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohomologyBaseChange.lean, line 198. The attribute's comment: “the pulled-back coefficient”.

The coefficient 𝓕' = (g')^*𝓕 on the base-changed source.

abbrev pulledBack : Modules.{u, u} B S hS D.X'.1 D.X'.2

AlgebraicGeometry.Space.BaseChangeDiagram.derivedPushforward, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohomologyBaseChange.lean, line 203. The attribute's comment: “the lower-right derived direct image”.

The total derived direct image Rf_*𝓕 on the lower-right corner.

abbrev derivedPushforward : DerivedCategory.Plus (Modules.{u, u} B S hS D.Y.1 D.Y.2)

AlgebraicGeometry.Space.BaseChangeDiagram.derivedPushforward', an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohomologyBaseChange.lean, line 210. The attribute's comment: “the lower-left derived direct image”.

The total derived direct image Rf'_*𝓕' on the lower-left corner.

abbrev derivedPushforward' : DerivedCategory.Plus (Modules.{u, u} B S hS D.Y'.1 D.Y'.2)

Tag 07U8, a lemma

Tag 07U8 in the Stacks Project.

AlgebraicGeometry.Space.isIso_rightDerivedFunctorPlusUnit_app_modulePushforward_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineDirectImageDerivedComparison.lean, line 122. The attribute's comment: “f_F ≅ Rf_F: the canonical map from the direct image to the derived direct image is an isomorphism”.

Stacks 07U8, f_*F ≅ Rf_*F. Let f : X ⟶ Y be an affine morphism of algebraic spaces over S and let F be a quasi-coherent 𝒪_X-module. Then the canonical map from the direct image f_*F, placed in degree zero, to the derived direct image Rf_*F is an isomorphism: the unit of the right derived functor Rf_* of f_* on bounded below derived categories is invertible at F[0].

Equivalently R^p f_*F = 0 for p > 0, which is AlgebraicGeometry.Space.isZero_rightDerived_modulePushforward_isAffineHom (Stacks 073H, the reduction of the source to Stacks 02KG through Equation 69.3.0.1); the two are equivalent for the left exact functor f_* by part (2) of Stacks 015C. No model of the derived categories is fixed.

theorem isIso_rightDerivedFunctorPlusUnit_app_modulePushforward_isAffineHom
    [HasDerivedCategory.{w} (Modules.{u, u} B S hS X.1 X.2)]
    [HasDerivedCategory.{w'} (Modules.{u, u} B S hS Y.1 Y.2)]
    (f : X ⟶ Y) (hf : IsAffineHom B S hS f.hom) (F : Modules.{u, u} B S hS X.1 X.2)
    (hF : F.IsQuasicoherentOnSite) :
    IsIso ((modulePushforward B S hS f).rightDerivedFunctorPlusUnith.app
      ((HomotopyCategory.Plus.singleFunctor (Modules.{u, u} B S hS X.1 X.2) 0).obj F))

AlgebraicGeometry.Space.isQuasicoherentOnSite_modulePushforward_of_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineDirectImageQuasicoherent.lean, line 105. The attribute's comment: “quasi-coherence of the direct image, reduced chartwise to the case of a target represented by a scheme of the site, which is the hypothesis h”.

Stacks 07U8, the quasi-coherence of the direct image. Let f : X ⟶ Y be an affine morphism of algebraic spaces over S and let F be a quasi-coherent 𝒪_X-module. Then the direct image f_*F is quasi-coherent.

The hypothesis h is the same statement for a target represented by a scheme of the site. Everything else is the reduction of the source: quasi-coherence is chartwise by Stacks 03LZ, the restriction of f_*F to a chart is the direct image along the base change of f by Stacks 03LX, and a base change of an affine morphism is affine.

theorem isQuasicoherentOnSite_modulePushforward_of_isAffineHom
    (h : SchemeTargetAffinePushforwardQuasicoherent B S hS)
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (hf : IsAffineHom B S hS f.hom)
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : F.IsQuasicoherentOnSite) :
    ((modulePushforward B S hS f).obj F).IsQuasicoherentOnSite

AlgebraicGeometry.Space.isQuasicoherentOnSite_modulePushforward_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffinePushforwardQuasicoherentUnconditional.lean, line 176. The attribute's comment: “quasi-coherence of the direct image”.

Stacks 07U8, the quasi-coherence of the direct image, with no hypothesis. Let f : X ⟶ Y be an affine morphism of algebraic spaces over S and let F be a quasi-coherent 𝒪_X-module. Then the direct image f_*F is quasi-coherent.

This is AlgebraicGeometry.Space.isQuasicoherentOnSite_modulePushforward_of_isAffineHom with its hypothesis supplied by AlgebraicGeometry.Space.schemeTargetAffinePushforwardQuasicoherent.

theorem isQuasicoherentOnSite_modulePushforward_isAffineHom {X Y : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (hf : IsAffineHom B S hS f.hom) (F : Modules.{u, u} B S hS X.1 X.2)
    (hF : F.IsQuasicoherentOnSite) :
    ((modulePushforward B S hS f).obj F).IsQuasicoherentOnSite

AlgebraicGeometry.Space.isIso_moduleBaseChangeMap_app_of_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleAffineBaseChange.lean, line 229. The attribute's comment: “base change: g^f_F = f'_(g')^F for f affine and F quasi-coherent”.

Affine base change for the direct image of a quasi-coherent module (the base change clause of Stacks 07U8; Stacks 02KG for schemes). For a cartesian square of algebraic spaces whose right morphism f is affine, the base change map g^*f_*F ⟶ f'_*(g')^*F is an isomorphism at every quasi-coherent 𝒪_X-module F. The bottom morphism g is arbitrary.

theorem isIso_moduleBaseChangeMap_app_of_isAffineHom (sq : IsPullback g' f' f g)
    (hf : IsAffineHom B S hS f.hom) (F : Modules.{u, u} B S hS X.1 X.2)
    (hF : F.IsQuasicoherentOnSite) :
    IsIso ((moduleBaseChangeMap f g f' g' sq.w).app F)

Tag 073K, a lemma

Tag 073K in the Stacks Project.

AlgebraicGeometry.Space.cohomologyFlatBaseChangeEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohomologyAffineFlatBaseChange.lean, line 289. The attribute's comment: “part (2)”.

Flat base change of cohomology over an affine base.

Let q : W ⟶ V be a flat morphism of affine schemes of the site, A = Γ(V, 𝒪) and R = Γ(W, 𝒪). Let p : X ⟶ V be a quasi-compact and quasi-separated morphism of algebraic spaces over S, X' = W ×_V X with projections pr' : X' ⟶ W and pr : X' ⟶ X, and ℱ a quasi-coherent 𝒪_X-module with pullback ℱ' = pr^* ℱ. Then for every i ≥ 0

R ⊗_A H^i(X, ℱ) ≅ H^i(X', ℱ')

as R-modules, A acting on H^i(X, ℱ) through p and R acting on H^i(X', ℱ') through pr'.

def cohomologyFlatBaseChangeEquiv [Flat ((BigFppfOver.toScheme B S hS).map q)]
    (hpc : IsQuasiCompact B S hS p.hom) (hps : IsQuasiSeparated B S hS p.hom)
    (hF : F.IsQuasicoherentOnSite) (i : ℕ) :
    letI := ((BigFppfOver.toScheme B S hS).map q).appTop.hom.toAlgebra
    Γ((BigFppfOver.toScheme B S hS).obj W, ⊤) ⊗[Γ((BigFppfOver.toScheme B S hS).obj V, ⊤)]
        cohomologyRes (baseFunctionsToGlobalSections B S hS p) i F
      ≃ₗ[Γ((BigFppfOver.toScheme B S hS).obj W, ⊤)]
      cohomologyRes (baseFunctionsToGlobalSections B S hS (pullback.fst (schemeSpaceMap q) p)) i
        ((modulePullback B S hS (pullback.snd (schemeSpaceMap q) p)).obj F)

AlgebraicGeometry.Space.BaseChangeDiagram.baseChangeMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohomologyFlatBaseChange.lean, line 200. The attribute's comment: “the base change map of Tag 0736 for the cartesian square, whose invertibility is what part (1) asserts. The map is CONSTRUCTED and characterized; neither part (1) nor part (2) of the tag is proved here”.

The base change map g^*Rf_* ⟶ Rf'_*(g')^* of Stacks 0736, for the cartesian square of small étale ringed topoi attached to a cartesian square of algebraic spaces whose lower horizontal morphism g is flat.

Stacks 073K, part (1) asserts that it is invertible. It is built from the comparison directImageSquareIso of the two composite direct images and the flatness of the morphisms of ringed topoi of g and g' (isFlat_smallEtaleRingedToposHom_base, isFlat_smallEtaleRingedToposHom_source).

def baseChangeMap (hg : IsFlat B S hS D.g.hom) :
    (pushforwardModules (X := smallEtaleRingedTopos B S hS D.X)
          (Y := smallEtaleRingedTopos B S hS D.Y)
          (smallEtaleRingedToposHom B S hS D.f).toRingedToposModulesHom).rightDerivedFunctorPlus ⋙
        D.flatPullbackBase hg ⟶
      D.flatPullbackSource hg ⋙
        (pushforwardModules (X := smallEtaleRingedTopos B S hS D.X')
          (Y := smallEtaleRingedTopos B S hS D.Y')
          (smallEtaleRingedToposHom B S hS D.f').toRingedToposModulesHom).rightDerivedFunctorPlus

AlgebraicGeometry.Space.BaseChangeDiagram.baseChangeMap_fac, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohomologyFlatBaseChange.lean, line 222. The attribute's comment: “canonical characterization of the base change map of Tag 0736 for the cartesian square: it is determined by its agreement, after the derived-functor unit of Rf_*, with the degreewise comparison. Neither part (1) nor part (2) of the tag is proved here”.

The base change map of the square is the canonical one. Composed with the derived-functor unit of Rf_*, it is the degreewise comparison on the bounded below homotopy category of 𝒪_X-modules. Since Rf_* ⋙ g^* is a right derived functor of f_* ⋙ g^* with that unit, this equation determines the map.

theorem baseChangeMap_fac (hg : IsFlat B S hS D.g.hom) :
    Functor.whiskerRight
        (pushforwardModules (X := smallEtaleRingedTopos B S hS D.X)
          (Y := smallEtaleRingedTopos B S hS D.Y)
          (smallEtaleRingedToposHom B S hS D.f).toRingedToposModulesHom).rightDerivedFunctorPlusUnith
        (D.flatPullbackBase hg) ≫
      (Functor.associator _ _ _).hom ≫
      Functor.whiskerLeft DerivedCategory.Plus.Qh (D.baseChangeMap hg) =
        Stacks.Cohomology.ToposBaseChange.baseChangeOnHomotopyCategory
          (smallEtaleRingedToposHom B S hS D.f) (smallEtaleRingedToposHom B S hS D.f')
          (smallEtaleRingedToposHom B S hS D.g) (smallEtaleRingedToposHom B S hS D.g')
          D.directImageSquareIso (D.isFlat_smallEtaleRingedToposHom_base hg)
          (D.isFlat_smallEtaleRingedToposHom_source hg)

AlgebraicGeometry.Space.BaseChangeDiagram.affineCohomologyBaseChangeIsoBase, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatAffineCohomologyBaseChangeBLinear.lean, line 744. The attribute's comment: “part (2), the affine case: H^i(X,F) ⊗_A B = H^i(X',F') as B-modules”.

Flat base change of cohomology over affine bases: H^i(X, 𝓕) ⊗_A B = H^i(X', 𝓕') as B-modules. For the cartesian square of Stacks 073J with 𝓕 quasi-coherent, g flat, f quasi-compact and quasi-separated and the two bases affine — Y = Spec(A) and Y' = Spec(B), presented by the charts V₀ and V₀' with A and B their coordinate rings — the extension of scalars of H^i(X, 𝓕) along A ⟶ B is the cohomology of the pulled back coefficient on X', in every degree i, as modules over B: the left hand side by its tensor factor B and the right hand side because X' lives over Y' = Spec(B). The left hand side is written B ⊗_A H^i(X, 𝓕), the extension of scalars.

def affineCohomologyBaseChangeIsoBase (hZ : B.Contains (⊤_ Scheme.{u}))
    (hg : IsFlat B S hS D.g.hom) (hqc : IsQuasiCompact B S hS D.f.hom)
    (hqs : IsQuasiSeparated B S hS D.f.hom)
    [IsAffine (chartScheme V₀)] [IsAffine (chartScheme V₀')] (i : ℕ) :
    have := hasInjectiveResolutions_modules B S hS D.X.1 D.X.2
    have := hasInjectiveResolutions_modules B S hS D.X'.1 D.X'.2
    have := enoughInjectives_modules B S hS D.X.1 D.X.2
    letI := baseChartAlgebra B S hS D.g V₀ V₀'
    ModuleCat.of (baseChartRing B S hS D.Y' V₀')
        (baseChartRing B S hS D.Y' V₀' ⊗[baseChartRing B S hS D.Y V₀]
          ↥(D.affineCohomologyOverBaseChart V₀ i)) ≅
      (baseChartRestrictScalars B S hS D.Y' (isTerminal_of_isIso_chart B S hS D.Y' V₀')).obj
        (D.affineCohomologyTarget i)

AlgebraicGeometry.Space.isIso_higherDirectImageBaseChangeMap_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/HigherDirectImageFlatBaseChange.lean, line 246. The attribute's comment: “part (1): for a cartesian square of algebraic spaces with g flat and f quasi-compact and quasi-separated, the base change map g^R^if_F ⟶ R^if'_*F' of Tag 0736 is an isomorphism for every quasi-coherent F and every i ≥ 0”.

Stacks 073K, part (1): flat base change for higher direct images. Let

  X' ———→ X
   | f'    | f
   v       v
  Y' ———→ Y
      g

be a cartesian square of algebraic spaces over S with g flat and f quasi-compact and quasi-separated, and let 𝓕 be a quasi-coherent 𝒪_X-module with pullback 𝓕' = (g')^*𝓕. For every i ≥ 0 the base change map of Stacks 0736

g^*R^if_*𝓕 ⟶ R^if'_*𝓕'

(AlgebraicGeometry.Space.higherDirectImageBaseChangeMap) is an isomorphism.

The exactness of the two inverse images g^* and (g')^* that the base change map is constructed against is Stacks 04JC for the flat g and, g' being flat by Stacks 03MO, for g'.

theorem isIso_higherDirectImageBaseChangeMap_of_isFlat {f : X ⟶ Y} {g : Y' ⟶ Y}
    {f' : X' ⟶ Y'} {g' : X' ⟶ X} (sq : IsPullback g' f' f g) (hg : IsFlat B S hS g.hom)
    (hfqc : IsQuasiCompact B S hS f.hom) (hfqs : IsQuasiSeparated B S hS f.hom)
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : F.IsQuasicoherentOnSite) (i : ℕ) :
    have := preservesFiniteLimits_modulePullback_of_isFlat_hom B S hS g hg
    have := preservesFiniteColimits_modulePullback_smallEtale B S hS g
    have := preservesFiniteLimits_modulePullback_of_isFlat_hom B S hS g'
      ((isFlat_isStableUnderBaseChange B S hS).of_isPullback sq.flip hg)
    have := preservesFiniteColimits_modulePullback_smallEtale B S hS g'
    IsIso ((higherDirectImageBaseChangeMap f g f' g' sq.w i).app F)

Tag 0HAP, a lemma

Tag 0HAP in the Stacks Project.

AlgebraicGeometry.Space.counitSplitEpiOfSeparatedEtale, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SeparatedEtaleDiagonalSplitEpi.lean, line 257.

Stacks 0HAP. Let f : X ⟶ Y be a separated étale morphism of algebraic spaces over a scheme S contained in a big fppf site B, and let ℱ be an 𝒪_X-module. Then the counit f^*f_*ℱ ⟶ ℱ of the adjunction of Stacks 03LU is a split epimorphism.

The reduction to the diagonal is AlgebraicGeometry.Space.counitSplitEpiOfSplitEpiChartUnit, and the splitting along the diagonal is AlgebraicGeometry.Space.splitEpiDiagonalChartUnit: extension by zero across the clopen diagonal.

Stacks 0HAP assumes f quasi-compact and ℱ quasi-coherent; neither hypothesis is used here, see the implementation notes.

noncomputable def counitSplitEpiOfSeparatedEtale (F : Modules.{u, u} B S hS X.1 X.2) :
    SplitEpi ((modulePullbackAdjunction B S hS f).counit.app F)

Sources

• Section 69.11, Tag 073I
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.BaseChangeDiagram · AlgebraicGeometry.Space.BaseChangeDiagram.pulledBack · AlgebraicGeometry.Space.BaseChangeDiagram.derivedPushforward · AlgebraicGeometry.Space.BaseChangeDiagram.derivedPushforward' · AlgebraicGeometry.Space.isIso_rightDerivedFunctorPlusUnit_app_modulePushforward_isAffineHom · AlgebraicGeometry.Space.isQuasicoherentOnSite_modulePushforward_of_isAffineHom · AlgebraicGeometry.Space.isQuasicoherentOnSite_modulePushforward_isAffineHom · AlgebraicGeometry.Space.isIso_moduleBaseChangeMap_app_of_isAffineHom

Section69.12 Coherent modules on locally Noetherian algebraic spaces#

Section 69.12 of the Stacks Project, Tag 07U9. 9 tags here are carried by 33 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07UA, a definition

Tag 07UA in the Stacks Project.

AlgebraicGeometry.Space.IsCoherent, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentModules.lean, line 389.

A coherent module on an algebraic space is a quasi-coherent module which is coherent on its small étale ringed site.

The predicate is on all modules rather than only on the quasi-coherent ones, so that it applies directly to kernels, cokernels and extensions formed in the ambient category of modules. It does not need the locally Noetherian assumption; that assumption enters the characterizations of Stacks 07UB and the closure results of Stacks 07UC.

class IsCoherent (M : Modules.{u, m} B S hS F hF) : Prop
    extends SheafOfModules.IsQuasicoherentOnSite M, SheafOfModules.IsCoherentOnSite M

Tag 07UB, a lemma

Tag 07UB in the Stacks Project.

AlgebraicGeometry.Space.isCoherent_iff_forall_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentEtaleChartTfae.lean, line 149. The attribute's comment: “conditions (1) and (4)”.

Stacks 07UB, conditions (1) and (4). A module on an algebraic space is coherent if and only if its restriction to the slice at every étale chart is coherent there.

The restriction is restriction to the slice of the small étale site at the chart; see the implementation notes. The module universe is the universe of the structure rings, which AlgebraicGeometry.Space.isCoherent_iff_isCoherentOnSite pins.

theorem isCoherent_iff_forall_over (M : Modules.{u, u} B S hS F hF) :
    IsCoherent B S hS F hF M ↔
      ∀ U : (smallEtaleRingedSite B S hS F hF).C,
        SheafOfModules.IsCoherentOnSite
          (R := (Stacks.SheafOfModules.Tensor.ringSheaf
            ((smallEtaleRingedSite B S hS F hF).over U).O)) (M.over U)

AlgebraicGeometry.Space.isCoherent_iff_exists_surjective_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentEtaleChartTfae.lean, line 168. The attribute's comment: “conditions (1) and (5)”.

Stacks 07UB, conditions (1) and (5). A module on an algebraic space is coherent if and only if there is an étale chart whose structure morphism is surjective on points and whose slice restriction is coherent.

The forward implication uses that an algebraic space has such a chart at all, namely its atlas: AlgebraicGeometry.Space.exists_surjective_smallEtale_chart. The restriction is restriction to the slice of the small étale site at the chart; see the implementation notes. The module universe is the universe of the structure rings, which AlgebraicGeometry.Space.isCoherent_iff_isCoherentOnSite pins.

theorem isCoherent_iff_exists_surjective_over (M : Modules.{u, u} B S hS F hF) :
    IsCoherent B S hS F hF M ↔
      ∃ U : (smallEtaleRingedSite B S hS F hF).C, IsSurjective B S hS U.1.hom ∧
        SheafOfModules.IsCoherentOnSite
          (R := (Stacks.SheafOfModules.Tensor.ringSheaf
            ((smallEtaleRingedSite B S hS F hF).over U).O)) (M.over U)

AlgebraicGeometry.Space.forall_over_iff_exists_surjective_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentEtaleChartTfae.lean, line 190. The attribute's comment: “conditions (4) and (5)”.

Stacks 07UB, conditions (4) and (5). The slice restriction of a module on an algebraic space is coherent at every étale chart if and only if it is coherent at one étale chart whose structure morphism is surjective on points.

This is the adjacent equivalence at the bottom of the chain of Stacks 07UB, stated without reference to its condition (1). Unlike the two equivalences with condition (1) it is at a free module universe: both implications pass through coherence of the module on the whole small étale ringed site, and only the identification of that with condition (1) needs the universe fixed. The restriction is restriction to the slice of the small étale site at the chart; see the implementation notes.

theorem forall_over_iff_exists_surjective_over (M : Modules.{u, m} B S hS F hF) :
    (∀ U : (smallEtaleRingedSite B S hS F hF).C,
        SheafOfModules.IsCoherentOnSite
          (R := (Stacks.SheafOfModules.Tensor.ringSheaf
            ((smallEtaleRingedSite B S hS F hF).over U).O)) (M.over U)) ↔
      ∃ U : (smallEtaleRingedSite B S hS F hF).C, IsSurjective B S hS U.1.hom ∧
        SheafOfModules.IsCoherentOnSite
          (R := (Stacks.SheafOfModules.Tensor.ringSheaf
            ((smallEtaleRingedSite B S hS F hF).over U).O)) (M.over U)

AlgebraicGeometry.Space.isCoherent_iff_isFinitePresentationOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentFinitePresentation.lean, line 44. The attribute's comment: “conditions (1) and (3)”.

A module on a locally Noetherian algebraic space is coherent if and only if it is an 𝒪_F-module of finite presentation.

theorem isCoherent_iff_isFinitePresentationOnSite
    [Fact (HasEtaleLocalProperty B S hS F (fun V : Scheme.{u} => IsLocallyNoetherian V))]
    (M : Modules.{u, u} B S hS F hF) :
    IsCoherent B S hS F hF M ↔ M.IsFinitePresentationOnSite

AlgebraicGeometry.Space.isCoherent_structureSheaf, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentStructureSheaf.lean, line 391. The attribute's comment: “structure sheaf”.

Stacks 07UB, the structure sheaf. The structure sheaf of a locally Noetherian algebraic space is a coherent 𝒪_F-module.

Quasi-coherence is SheafOfModules.isQuasicoherentOnSite_unit and finite type is PresheafOfModules.isFiniteType_unit, neither of which needs the hypothesis; the relations clause is AlgebraicGeometry.RingedSite.isFiniteType_relations_unit, applied to the covering by Noetherian affine charts of AlgebraicGeometry.Space.exists_covering_through_noetherianAffine.

instance isCoherent_structureSheaf
    [Fact (HasEtaleLocalProperty B S hS F (fun V : Scheme.{u} => IsLocallyNoetherian V))] :
    IsCoherent B S hS F hF
      (SheafOfModules.unit (ringSheaf (smallEtaleRingedSite B S hS F hF).O))

AlgebraicGeometry.Space.isCoherent_iff_isQuasicoherentOnSite_and_isFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteDirectImageCoherence.lean, line 124. The attribute's comment: “conditions (1) and (2)”.

Stacks 07UB, conditions (1) and (2). A module on a locally Noetherian algebraic space is coherent if and only if it is quasi-coherent and of finite type.

The base change property of the sections over the affine charts, which the conditional form in StacksFrontier.AlgebraicGeometry.Spaces.CoherentNoetherian carries, is Descent, Proposition 03DX (2) and follows from quasi-coherence, which is a hypothesis in the direction that needs it.

theorem isCoherent_iff_isQuasicoherentOnSite_and_isFiniteType
    [Fact (HasEtaleLocalProperty B S hS F (fun V : Scheme.{u} => IsLocallyNoetherian V))]
    (M : Modules.{u, u} B S hS F hF) :
    IsCoherent B S hS F hF M ↔
      (M.IsQuasicoherentOnSite ∧
        PresheafOfModules.IsFiniteType (smallEtaleRingedSite B S hS F hF).J M.val)

AlgebraicGeometry.Space.isCoherent_of_fact_isFiniteLocallyFreeOnSite, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteLocallyFreeCoherent.lean, line 567. The attribute's comment: “finite locally free modules”.

Stacks 07UB, finite locally free modules. A finite locally free module on a locally Noetherian algebraic space is coherent, as an instance.

This is AlgebraicGeometry.Space.isCoherent_of_isFiniteLocallyFreeOnSite with finite local freeness supplied by instance search through Fact, which is how the predicate — an abbrev and not a class — can be an instance hypothesis. The same wrapping is used by the locally Noetherian hypothesis of AlgebraicGeometry.Space.isCoherent_structureSheaf.

instance isCoherent_of_fact_isFiniteLocallyFreeOnSite
    [Fact (HasEtaleLocalProperty B S hS F (fun V : Scheme.{u} => IsLocallyNoetherian V))]
    (M : Modules.{u, m} B S hS F hF)
    [Fact (SheafOfModules.IsFiniteLocallyFreeOnSite M)] :
    IsCoherent B S hS F hF M

AlgebraicGeometry.Space.isCoherent_of_isInvertible_instance, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/InvertibleCoherent.lean, line 636. The attribute's comment: “invertible modules”.

Stacks 07UB, invertible modules. An invertible module on a locally Noetherian algebraic space is coherent, as an instance.

This is AlgebraicGeometry.Space.isCoherent_of_isInvertible with invertibility taken as an instance-implicit binder, discharged from the local context. Stacks.SheafOfModules.IsInvertible is a class, which is what lets the hypothesis be written that way; it does not mean instance search finds invertibility, and on this site it finds it for nothing at all, the structure sheaf included — Stacks.SheafOfModules.isInvertible_unit does not apply here, its CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective hypothesis not being synthesized for the topology as the small étale ringed site spells it. That is also what makes the instance free: the branch it adds to the search for AlgebraicGeometry.Space.IsCoherent closes on the invertibility subgoal unless the caller has already put invertibility in its context, which is the only situation the instance is for.

instance isCoherent_of_isInvertible_instance
    [Fact (HasEtaleLocalProperty B S hS F (fun V : Scheme.{u} => IsLocallyNoetherian V))]
    (M : Modules.{u, u} B S hS F hF)
    [Stacks.SheafOfModules.IsInvertible (structurePresheaf B S hS F)
      ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS F hF).O)).property M] :
    IsCoherent B S hS F hF M

Tag 07UC, a lemma

Tag 07UC in the Stacks Project.

AlgebraicGeometry.Space.isCoherent_kernel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentAbelian.lean, line 94. The attribute's comment: “kernel”.

[Stacks, Tag 07UC]. The kernel of a map of coherent modules on an algebraic space is coherent.

The kernel of a map of coherent sheaves of modules on an arbitrary site is coherent, by Stacks 01BY (3); quasi-coherence of the kernel is then free at this module universe.

theorem isCoherent_kernel {M N : Modules.{u, u} B S hS F hF} (hM : IsCoherent B S hS F hF M)
    (hN : IsCoherent B S hS F hF N) (φ : M ⟶ N) : IsCoherent B S hS F hF (kernel φ)

AlgebraicGeometry.Space.isCoherent_cokernel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentAbelian.lean, line 106. The attribute's comment: “cokernel”.

[Stacks, Tag 07UC]. The cokernel of a map of coherent modules on an algebraic space is coherent.

The cokernel of a map of coherent sheaves of modules on an arbitrary site is coherent, by Stacks 01BY (3); quasi-coherence of the cokernel is then free at this module universe.

theorem isCoherent_cokernel {M N : Modules.{u, u} B S hS F hF} (hM : IsCoherent B S hS F hF M)
    (hN : IsCoherent B S hS F hF N) (φ : M ⟶ N) : IsCoherent B S hS F hF (cokernel φ)

AlgebraicGeometry.Space.isCoherent_X₂_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentAbelian.lean, line 122. The attribute's comment: “extensions”.

[Stacks, Tag 07UC]. An extension of coherent modules on an algebraic space is coherent: the middle term of a short exact sequence of 𝒪_F-modules whose outer terms are coherent is coherent.

An extension is represented by a short exact complex of 𝒪_F-modules, so the statement quantifies over all extensions of the third term by the first rather than over a choice of one. The content is Stacks 01BY (4) on the small étale ringed site of F; quasi-coherence of the middle term is free at this module universe.

theorem isCoherent_X₂_of_shortExact {T : ShortComplex (Modules.{u, u} B S hS F hF)}
    (hT : T.ShortExact) (h₁ : IsCoherent B S hS F hF T.X₁)
    (h₃ : IsCoherent B S hS F hF T.X₃) : IsCoherent B S hS F hF T.X₂

AlgebraicGeometry.Space.nonempty_abelian_coherentModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentAbelian.lean, line 166. The attribute's comment: “abelian category”.

[Stacks, Tag 07UC]. The category Coh(𝒪_F) of coherent modules on an algebraic space is abelian.

The abelian structure is the one a full subcategory of an abelian category closed under kernels, cokernels and finite coproducts carries, assembled by AlgebraicGeometry.Space.coherentModules_abelian_of_closure; the kernel and cokernel closure properties are Stacks 01BY (3) on the small étale ringed site and the coproduct one comes from the extension result above.

theorem nonempty_abelian_coherentModules :
    Nonempty (Abelian (CoherentModules.{u, u} B S hS F hF))

Tag 07UD, a lemma

Tag 07UD in the Stacks Project.

AlgebraicGeometry.Space.isCoherentOnSite_of_mono_of_isQuasicoherentOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentSubquotientNoetherian.lean, line 359. The attribute's comment: “a quasi-coherent submodule of a coherent module is coherent”.

The submodule clause of Stacks 07UD on the small étale ringed site. A quasi-coherent submodule of a module coherent on the small étale ringed site of a locally Noetherian algebraic space is itself coherent on that site.

The submodule is of finite type by AlgebraicGeometry.Space.isFiniteType_of_mono_of_isQuasicoherentOnSite, and a submodule of finite type of a coherent module is coherent by AlgebraicGeometry.Space.isCoherentOnSite_of_mono_of_isFiniteType.

theorem isCoherentOnSite_of_mono_of_isQuasicoherentOnSite
    [Fact (HasEtaleLocalProperty B S hS F (fun V : Scheme.{u} => IsLocallyNoetherian V))]
    {M N : Modules.{u, u} B S hS F hF} (ι : N ⟶ M) [Mono ι]
    (hN : N.IsQuasicoherentOnSite) (hM : SheafOfModules.IsCoherentOnSite M) :
    SheafOfModules.IsCoherentOnSite N

AlgebraicGeometry.Space.isCoherent_of_mono_of_isQuasicoherentOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentSubquotientNoetherian.lean, line 371. The attribute's comment: “a quasi-coherent submodule of a coherent module is coherent”.

The submodule clause of Stacks 07UD. A quasi-coherent submodule of a coherent module on a locally Noetherian algebraic space is coherent, for the predicate AlgebraicGeometry.Space.IsCoherent of Stacks 07UA.

theorem isCoherent_of_mono_of_isQuasicoherentOnSite
    [Fact (HasEtaleLocalProperty B S hS F (fun V : Scheme.{u} => IsLocallyNoetherian V))]
    {M N : Modules.{u, u} B S hS F hF} (ι : N ⟶ M) [Mono ι]
    (hN : N.IsQuasicoherentOnSite) (hM : IsCoherent B S hS F hF M) :
    IsCoherent B S hS F hF N

AlgebraicGeometry.Space.isCoherentOnSite_of_epi_of_isQuasicoherentOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentSubquotientNoetherian.lean, line 391. The attribute's comment: “a quasi-coherent quotient module of a coherent module is coherent”.

The quotient clause of Stacks 07UD on the small étale ringed site. A quasi-coherent quotient module of a module coherent on the small étale ringed site of a locally Noetherian algebraic space is itself coherent on that site. The quotient is given by an epimorphism p : M ⟶ Q of 𝒪_F-modules.

The kernel of p is a quasi-coherent submodule of M, being cartesian on affine charts by AlgebraicGeometry.Space.isCartesianOnAffineCharts_kernel, so it is of finite type by AlgebraicGeometry.Space.isFiniteType_of_mono_of_isQuasicoherentOnSite, and a quotient of a coherent module by a submodule of finite type is coherent by AlgebraicGeometry.Space.isCoherentOnSite_of_epi_of_isFiniteType_kernel.

theorem isCoherentOnSite_of_epi_of_isQuasicoherentOnSite
    [Fact (HasEtaleLocalProperty B S hS F (fun V : Scheme.{u} => IsLocallyNoetherian V))]
    {M Q : Modules.{u, u} B S hS F hF} (p : M ⟶ Q) [Epi p]
    (hQ : Q.IsQuasicoherentOnSite) (hM : SheafOfModules.IsCoherentOnSite M) :
    SheafOfModules.IsCoherentOnSite Q

AlgebraicGeometry.Space.isCoherent_of_epi_of_isQuasicoherentOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentSubquotientNoetherian.lean, line 408. The attribute's comment: “a quasi-coherent quotient module of a coherent module is coherent”.

The quotient clause of Stacks 07UD. A quasi-coherent quotient module of a coherent module on a locally Noetherian algebraic space is coherent, for the predicate AlgebraicGeometry.Space.IsCoherent of Stacks 07UA.

theorem isCoherent_of_epi_of_isQuasicoherentOnSite
    [Fact (HasEtaleLocalProperty B S hS F (fun V : Scheme.{u} => IsLocallyNoetherian V))]
    {M Q : Modules.{u, u} B S hS F hF} (p : M ⟶ Q) [Epi p]
    (hQ : Q.IsQuasicoherentOnSite) (hM : IsCoherent B S hS F hF M) :
    IsCoherent B S hS F hF Q

Tag 07UE, a lemma

Tag 07UE in the Stacks Project.

AlgebraicGeometry.Space.isCoherent_smallEtaleInternalHomSmall, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentInternalHom.lean, line 164. The attribute's comment: “internal Hom”.

Stacks 07UE, the sheaf-hom clause. The internal Hom 𝓗om_{𝒪_F}(M, N) of two coherent 𝒪_F-modules on an algebraic space is coherent.

theorem isCoherent_smallEtaleInternalHomSmall (M N : Modules.{u, u} B S hS F hF)
    [IsCoherent B S hS F hF M] [IsCoherent B S hS F hF N] :
    IsCoherent B S hS F hF (smallEtaleInternalHomSmall B S hS F hF M N)

AlgebraicGeometry.Space.isCoherent_tensorModule_and_smallEtaleInternalHomSmall, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentInternalHom.lean, line 174.

Stacks 07UE. Let F be an algebraic space over a scheme S and let M, N be coherent 𝒪_F-modules. Then M ⊗_{𝒪_F} N and 𝓗om_{𝒪_F}(M, N) are coherent.

theorem isCoherent_tensorModule_and_smallEtaleInternalHomSmall
    (M N : Modules.{u, u} B S hS F hF)
    [IsCoherent B S hS F hF M] [IsCoherent B S hS F hF N] :
    IsCoherent B S hS F hF (tensorModule B S hS F hF M N) ∧
      IsCoherent B S hS F hF (smallEtaleInternalHomSmall B S hS F hF M N)

AlgebraicGeometry.Space.isCoherent_tensorModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentTensorProduct.lean, line 78. The attribute's comment: “tensor product”.

The tensor product AlgebraicGeometry.Space.tensorModule of two coherent 𝒪_F-modules on an algebraic space is coherent.

theorem isCoherent_tensorModule (M N : Modules.{u, u} B S hS F hF)
    [IsCoherent B S hS F hF M] [IsCoherent B S hS F hF N] :
    IsCoherent B S hS F hF (tensorModule B S hS F hF M N)

Tag 07UF, a lemma

Tag 07UF in the Stacks Project.

AlgebraicGeometry.Space.exists_isOpen_isZero_restrictToOpenPoints_of_isCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentStalkLocalProperties.lean, line 458. The attribute's comment: “part (1)”.

Stacks 07UF, part (1). A coherent 𝒪_X-module whose stalk at a geometric point x̄ vanishes vanishes on an open subspace of X containing the image of x̄.

The locally Noetherian hypothesis of the cited statement is not used: the support of a module of finite type is closed by Stacks 07TZ on any algebraic space, so the statement here is a strict generalisation.

theorem exists_isOpen_isZero_restrictToOpenPoints_of_isCoherent (X : AlgebraicSpaces B S hS)
    (M : Modules.{u, u} B S hS X.1 X.2) [IsCoherent B S hS X.1 X.2 M]
    (x : points B S hS X.1) (p : GeometricPoint B S hS X.1) (hp : p.LiesOver x)
    (hstalk : Subsingleton (stalkSet p (M.val.presheaf ⋙ forget AddCommGrpCat.{u}))) :
    ∃ (W : Set (points B S hS X.1)) (hW : IsOpen W), x ∈ W ∧
      IsZero ((restrictToOpenPoints.{u, u} B S hS X W hW).obj M)

AlgebraicGeometry.Space.exists_isOpen_mono_restrictToOpenPoints_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentStalkLocalProperties.lean, line 475. The attribute's comment: “part (2)”.

Stacks 07UF, part (2). A morphism of coherent 𝒪_X-modules injective on the stalk at a geometric point x̄ is a monomorphism after restriction to an open subspace of X containing the image of x̄.

The kernel is coherent on the small étale site, hence of finite type, and its stalk at x̄ vanishes; part (1) applies to it, and étale restriction is left exact. The locally Noetherian hypothesis of the cited statement is not used.

theorem exists_isOpen_mono_restrictToOpenPoints_map (X : AlgebraicSpaces B S hS)
    {M N : Modules.{u, u} B S hS X.1 X.2} [IsCoherent B S hS X.1 X.2 M]
    [IsCoherent B S hS X.1 X.2 N] (φ : M ⟶ N)
    (x : points B S hS X.1) (p : GeometricPoint B S hS X.1) (hp : p.LiesOver x)
    (hinj : Function.Injective (moduleStalkSetMap B S hS X p φ)) :
    ∃ (W : Set (points B S hS X.1)) (hW : IsOpen W), x ∈ W ∧
      Mono ((restrictToOpenPoints.{u, u} B S hS X W hW).map φ)

AlgebraicGeometry.Space.exists_isOpen_epi_restrictToOpenPoints_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentStalkLocalProperties.lean, line 496. The attribute's comment: “part (3)”.

Stacks 07UF, part (3). A morphism of coherent 𝒪_X-modules surjective on the stalk at a geometric point x̄ is an epimorphism after restriction to an open subspace of X containing the image of x̄.

The cokernel is coherent on the small étale site, hence of finite type, and its stalk at x̄ vanishes; part (1) applies to it, and étale restriction is right exact. The locally Noetherian hypothesis of the cited statement is not used.

theorem exists_isOpen_epi_restrictToOpenPoints_map (X : AlgebraicSpaces B S hS)
    {M N : Modules.{u, u} B S hS X.1 X.2} [IsCoherent B S hS X.1 X.2 M]
    [IsCoherent B S hS X.1 X.2 N] (φ : M ⟶ N)
    (x : points B S hS X.1) (p : GeometricPoint B S hS X.1) (hp : p.LiesOver x)
    (hsurj : Function.Surjective (moduleStalkSetMap B S hS X p φ)) :
    ∃ (W : Set (points B S hS X.1)) (hW : IsOpen W), x ∈ W ∧
      Epi ((restrictToOpenPoints.{u, u} B S hS X W hW).map φ)

AlgebraicGeometry.Space.exists_isOpen_isIso_restrictToOpenPoints_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentStalkLocalProperties.lean, line 518. The attribute's comment: “part (4)”.

Stacks 07UF, part (4). A morphism of coherent 𝒪_X-modules bijective on the stalk at a geometric point x̄ becomes an isomorphism after restriction to an open subspace of X containing the image of x̄.

Kernel and cokernel are both of finite type with vanishing stalk at x̄, so both vanish on the complement of the union of their two closed supports; there the restriction is both a monomorphism and an epimorphism. The locally Noetherian hypothesis of the cited statement is not used.

theorem exists_isOpen_isIso_restrictToOpenPoints_map (X : AlgebraicSpaces B S hS)
    {M N : Modules.{u, u} B S hS X.1 X.2} [IsCoherent B S hS X.1 X.2 M]
    [IsCoherent B S hS X.1 X.2 N] (φ : M ⟶ N)
    (x : points B S hS X.1) (p : GeometricPoint B S hS X.1) (hp : p.LiesOver x)
    (hbij : Function.Bijective (moduleStalkSetMap B S hS X p φ)) :
    ∃ (W : Set (points B S hS X.1)) (hW : IsOpen W), x ∈ W ∧
      IsIso ((restrictToOpenPoints.{u, u} B S hS X W hW).map φ)

Tag 07UG, a lemma

Tag 07UG in the Stacks Project.

AlgebraicGeometry.Space.isCoherent_module_on_schemeTheoreticSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentSchemeTheoreticSupport.lean, line 142.

Stacks 07UG. Let X be a locally Noetherian algebraic space over S, let F be a coherent 𝒪_X-module, let i : Z → X be the scheme-theoretic support of F and let G be the quasi-coherent 𝒪_Z-module with i_*G ≅ F. Then G is a coherent 𝒪_Z-module.

Here the witness hZ that the support is a closed subspace is an argument; it is a proposition that always holds, by AlgebraicGeometry.Space.isClosedSubspace_schemeTheoreticSupport_of_isCoherent, and the form with no such argument is AlgebraicGeometry.Space.isCoherent_module_on_coherentSchemeTheoreticSupport.

theorem isCoherent_module_on_schemeTheoreticSupport
    (hX : HasEtaleLocalProperty B S hS X.1 (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (F : Modules.{u, u} B S hS X.1 X.2) [IsCoherent B S hS X.1 X.2 F]
    (hZ : IsClosedSubspace B S hS (schemeTheoreticSupport B S hS X F))
    (G : Modules.{u, u} B S hS
      (closedSubspaceToSpace B S hS X ⟨schemeTheoreticSupport B S hS X F, hZ⟩).1
      (closedSubspaceToSpace B S hS X ⟨schemeTheoreticSupport B S hS X F, hZ⟩).2)
    (hG : G.IsQuasicoherentOnSite)
    (e : (modulePushforward B S hS (closedSubspaceInclusion B S hS X
      ⟨schemeTheoreticSupport B S hS X F, hZ⟩)).obj G ≅ F) :
    IsCoherent B S hS
      (closedSubspaceToSpace B S hS X ⟨schemeTheoreticSupport B S hS X F, hZ⟩).1
      (closedSubspaceToSpace B S hS X ⟨schemeTheoreticSupport B S hS X F, hZ⟩).2 G

AlgebraicGeometry.Space.isCoherent_module_on_coherentSchemeTheoreticSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentSchemeTheoreticSupport.lean, line 166.

Stacks 07UG. Let X be a locally Noetherian algebraic space over S, let F be a coherent 𝒪_X-module, let i : Z → X be the scheme-theoretic support of F and let G be the quasi-coherent 𝒪_Z-module with i_*G ≅ F. Then G is a coherent 𝒪_Z-module.

The scheme-theoretic support is read as the closed subspace AlgebraicGeometry.Space.coherentSchemeTheoreticSupport, so no witness of closedness is assumed.

theorem isCoherent_module_on_coherentSchemeTheoreticSupport
    (hX : HasEtaleLocalProperty B S hS X.1 (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (F : Modules.{u, u} B S hS X.1 X.2) [IsCoherent B S hS X.1 X.2 F]
    (G : Modules.{u, u} B S hS
      (closedSubspaceToSpace B S hS X (coherentSchemeTheoreticSupport B S hS X F)).1
      (closedSubspaceToSpace B S hS X (coherentSchemeTheoreticSupport B S hS X F)).2)
    (hG : G.IsQuasicoherentOnSite)
    (e : (modulePushforward B S hS (closedSubspaceInclusion B S hS X
      (coherentSchemeTheoreticSupport B S hS X F))).obj G ≅ F) :
    IsCoherent B S hS
      (closedSubspaceToSpace B S hS X (coherentSchemeTheoreticSupport B S hS X F)).1
      (closedSubspaceToSpace B S hS X (coherentSchemeTheoreticSupport B S hS X F)).2 G

Tag 08AM, a lemma

Tag 08AM in the Stacks Project.

AlgebraicGeometry.Space.pushforwardCoherentEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionCoherentEquivalence.lean, line 299.

Stacks 08AM. Let S be a scheme, let i : Z ⟶ X be a closed immersion of locally Noetherian algebraic spaces over S and let ℐ ⊆ 𝒪_X be the quasi-coherent sheaf of ideals cutting out Z. The functor i_* induces an equivalence between the category of coherent 𝒪_Z-modules and the category of coherent 𝒪_X-modules annihilated by ℐ.

The equivalence comes paired with the natural isomorphism identifying its functor, composed with the inclusion of the full subcategory, with AlgebraicGeometry.Space.modulePushforward — so what is asserted is that i_* itself is an equivalence onto the coherent annihilated modules, and not merely that the two categories are equivalent. The pairing is the shape in which the scheme-level Stacks 087T is stated at Stacks.AlgebraicGeometry.Tag087TCoherentImage.coherentPushforwardEquivalence.

The functor is AlgebraicGeometry.Space.pushforwardCoherent, its full faithfulness is AlgebraicGeometry.Space.fullyFaithfulPushforwardCoherent — part (2) of Stacks 04CJ, the 67.14.1 of the source's proof — and its essential surjectivity is AlgebraicGeometry.Space.essSurj_pushforwardCoherent, which rests on coherence of the inverse image together with the essential-image clause of Stacks 08KS for algebraic spaces. That the functor lands in the coherent annihilated modules is AlgebraicGeometry.Space.isCoherent_modulePushforward_of_isClosedImmersion.

def pushforwardCoherentEquivalence
    (hX : HasEtaleLocalProperty B S hS X.1 (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (hZ : HasEtaleLocalProperty B S hS Z.1 (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (i : Z ⟶ X) (hi : IsClosedImmersion B S hS i.hom) :
    Σ e : CoherentModules.{u, u} B S hS Z.1 Z.2 ≌
        (coherentAnnihilatedByKerIdeal B S hS i).FullSubcategory,
      e.functor ⋙ ObjectProperty.ι (coherentAnnihilatedByKerIdeal B S hS i) ≅
        ObjectProperty.ι _ ⋙ modulePushforward B S hS i

AlgebraicGeometry.Space.coherentModulePushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionModulePushforward.lean, line 340. The attribute's comment: “the induced functor into the modules annihilated by the ideal”.

Stacks 08AM, the induced functor, with the target weakened: direct image as a functor Coh(𝒪_X) ⥤ {𝓕 ∈ Mod(𝒪_Y) | 𝓘𝓕 = 0} from the coherent modules of Stacks 07UA.

The source states the target as the coherent 𝒪_Y-modules annihilated by 𝓘, which would need coherence of f_* of a coherent module; see the implementation notes.

def coherentModulePushforward (f : X ⟶ Y) :
    CoherentModules.{u, u} B S hS X.1 X.2 ⥤
      (annihilatedByKerIdeal B S hS f).FullSubcategory

AlgebraicGeometry.Space.fullyFaithfulCoherentModulePushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionModulePushforward.lean, line 361. The attribute's comment: “full faithfulness of the direct image on coherent modules”.

Stacks 08AM, the full-faithfulness half of the equivalence: direct image along a closed immersion of algebraic spaces is fully faithful on coherent modules.

Essential surjectivity is not proved; see the implementation notes for the one input it is missing and for the coherence of f_* that its target needs.

def fullyFaithfulCoherentModulePushforward (f : X ⟶ Y)
    (hf : IsClosedImmersion B S hS f.hom) :
    (coherentModulePushforward B S hS f).FullyFaithful

Tag 07UH, a lemma

Tag 07UH in the Stacks Project.

AlgebraicGeometry.Space.isZero_rightDerived_modulePushforward_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteDirectImageCoherence.lean, line 150. The attribute's comment: “vanishing of the higher direct images, granted the étale-affine case h03DW of Stacks 03DW”.

The vanishing assertion of Stacks 07UH, granted the chart case h03DW. Let f : X ⟶ Y be a finite morphism of algebraic spaces over S whose chart base changes have vanishing degree-n higher direct images. Then R^n f_*𝓕 = 0.

A finite morphism is affine, AlgebraicGeometry.Space.IsFinite.isAffineHom, so this is AlgebraicGeometry.Space.isZero_rightDerived_modulePushforward_of_isAffineHom, the reduction of Stacks 073H through Equation 69.3.0.1 of Stacks 071Z. The source's hypotheses that Y be locally Noetherian, that 𝓕 be coherent and that n > 0 are not used; h03DW is the étale-site form of Stacks 01Y6, that is Stacks 03DW, which this development does not carry.

theorem isZero_rightDerived_modulePushforward_of_isFinite (f : X ⟶ Y)
    (hf : IsFinite B S hS f.hom) (G : Modules.{u, u} B S hS X.obj X.property) (n : ℕ)
    (h03DW : ChartwiseIsZeroHigherDirectImage B S hS f
      (relativelyRepresentable_of_isAffineHom B S hS f hf.isAffineHom)
      G n) :
    have := hasInjectiveResolutions_modules B S hS X.obj X.property
    IsZero (((modulePushforward B S hS f).rightDerived n).obj G)

AlgebraicGeometry.Space.isCoherent_modulePushforward_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteDirectImageCoherence.lean, line 206. The attribute's comment: “coherence of the direct image, granted the chart case hchart of Stacks 03DW”.

The coherence assertion of Stacks 07UH, granted the chart case hchart. Let f : X ⟶ Y be a finite morphism of algebraic spaces over S with Y locally Noetherian, let 𝓕 be a coherent 𝒪_X-module, and let V be an étale scheme chart of Y surjective on points. Then f_*𝓕 is coherent.

Coherence is tested on V by Stacks 07UB (1) and (5) and over V the direct image is the localized direct image of Stacks 04CF, by AlgebraicGeometry.Space.isCoherentOnSite_modulePushforward_of_over_of_isSurjective. The two geometric premises of hchart are discharged: the base change of f along V is finite by Stacks 03ZS, and V is locally Noetherian by Stacks 03E8. So hchart is the étale-site form of Stacks 01Y6, that is Stacks 03DW, which this development does not carry.

Unlike AlgebraicGeometry.Space.isCoherent_modulePushforward_of_isFinite_of_chartCase the chart is the caller's, not the atlas that hY supplies, which is what lets hchart be met at an affine chart; that is possible here because local Noetherianity of an arbitrary chart is available, by AlgebraicGeometry.Space.isLocallyNoetherian_chart.

theorem isCoherent_modulePushforward_of_isFinite (f : X ⟶ Y) (hf : IsFinite B S hS f.hom)
    (hY : HasEtaleLocalProperty B S hS Y.1 (fun T : Scheme.{u} ↦ IsLocallyNoetherian T))
    (G : Modules.{u, u} B S hS X.1 X.2) (hG : IsCoherent B S hS X.1 X.2 G)
    (V : SmallEtale B S hS Y.1) (hsurj : IsSurjective B S hS V.1.hom)
    (hchart : IsFinite B S hS (chartBaseChangeProjection B S hS f V).hom →
      HasEtaleLocalProperty B S hS
        ((SpacesEtale.toSpaces B S hS Y).obj ((comparisonFunctor B S hS Y).obj V)).1
        (fun T : Scheme.{u} ↦ IsLocallyNoetherian T) →
      IsCoherent B S hS X.1 X.2 G →
      ((chartLocalizedModulePushforward B S hS f V).obj
        ((moduleChartBaseChangeRestriction B S hS f V).obj G)).IsCoherentOnSite) :
    IsCoherent B S hS Y.1 Y.2 ((modulePushforward B S hS f).obj G)

AlgebraicGeometry.Space.isZero_rightDerived_modulePushforward_of_isFinite_of_isCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteDirectImageVanishingUnconditional.lean, line 81. The attribute's comment: “vanishing of the higher direct images, with nothing carried”.

The vanishing half of Stacks 07UH. For a finite morphism f : X ⟶ Y of algebraic spaces over S, a coherent 𝒪_X-module 𝓕 and p > 0, the higher direct image vanishes: R^p f_* 𝓕 = 0.

A finite morphism is affine, AlgebraicGeometry.Space.IsFinite.isAffineHom, and a coherent module is quasi-coherent, so this is Stacks 073H, AlgebraicGeometry.Space.isZero_rightDerived_modulePushforward_of_isQuasicoherentOnSite.

AlgebraicGeometry.Space.isZero_rightDerived_modulePushforward_of_isFinite is the same statement with the affine case carried as the hypothesis h03DW and with 𝓕 only required to be a module; that hypothesis is now discharged by AlgebraicGeometry.Space.chartwiseIsZeroHigherDirectImage_of_isAffineHom, which asks for 𝓕 quasi-coherent and p > 0 — exactly what the source assumes here.

The source also assumes Y locally Noetherian; that is used by the coherence half of the tag, not by this one.

theorem isZero_rightDerived_modulePushforward_of_isFinite_of_isCoherent
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (hf : IsFinite B S hS f.hom)
    (G : Modules.{u, u} B S hS X.1 X.2) (hG : IsCoherent B S hS X.1 X.2 G) (p : ℕ)
    (hp : 0 < p) :
    have := hasInjectiveResolutions_modules B S hS X.1 X.2
    IsZero (((modulePushforward B S hS f).rightDerived p).obj G)

AlgebraicGeometry.Space.isCoherent_modulePushforward_of_isFinite', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperRepresentableDirectImageCoherence.lean, line 189. The attribute's comment: “coherence of the direct image”.

Stacks 07UH, coherence of the direct image. Let f : X ⟶ Y be a finite morphism of algebraic spaces over S with Y locally Noetherian, and let 𝓕 be a coherent 𝒪_X-module. Then f_*𝓕 is a coherent 𝒪_Y-module.

A finite morphism is affine, hence representable (AlgebraicGeometry.Space.relativelyRepresentable_of_isAffineHom), and proper by Stacks 04NZ (AlgebraicGeometry.Space.isFinite_iff_isAffineHom_and_isProper), so this is AlgebraicGeometry.Space.isCoherent_modulePushforward_of_isProper. The vanishing assertion of Stacks 07UH is AlgebraicGeometry.Space.isZero_rightDerived_modulePushforward_of_isFinite.

theorem isCoherent_modulePushforward_of_isFinite' (f : X ⟶ Y) (hf : IsFinite B S hS f.hom)
    (hY : HasEtaleLocalProperty B S hS Y.1 (fun T : Scheme.{u} ↦ IsLocallyNoetherian T))
    (M : Modules.{u, u} B S hS X.1 X.2) (hM : IsCoherent B S hS X.1 X.2 M) :
    IsCoherent B S hS Y.1 Y.2 ((modulePushforward B S hS f).obj M)

Declarations registered for the tag:

• AlgebraicGeometry.Space.isZero_rightDerived_modulePushforward_of_isFinite_of_isQuasicoherent, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/FinitePushforwardTwist.lean, line 127 (StacksFrontier): “vanishing of the higher direct images R^p f_* F, p > 0”.

Sources

• Section 69.12, Tag 07U9
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.IsCoherent · AlgebraicGeometry.Space.isCoherent_iff_forall_over · AlgebraicGeometry.Space.isCoherent_iff_exists_surjective_over · AlgebraicGeometry.Space.forall_over_iff_exists_surjective_over · AlgebraicGeometry.Space.isCoherent_iff_isFinitePresentationOnSite · AlgebraicGeometry.Space.isCoherent_structureSheaf · AlgebraicGeometry.Space.isCoherent_iff_isQuasicoherentOnSite_and_isFiniteType · AlgebraicGeometry.Space.isCoherent_of_fact_isFiniteLocallyFreeOnSite

Section69.13 Coherent sheaves on Noetherian spaces#

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

Tag 07UJ, a lemma

Tag 07UJ in the Stacks Project.

AlgebraicGeometry.Space.exists_eventually_constant_quasicoherentSubobjects, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentAscendingChain.lean, line 311.

Stacks 07UJ. The ascending chain condition holds for the quasi-coherent submodules of a coherent module on a Noetherian algebraic space: an ascending sequence of quasi-coherent subobjects of a coherent 𝒪_F-module is eventually constant.

theorem exists_eventually_constant_quasicoherentSubobjects
    (hZ : B.Contains (⊤_ Scheme.{u})) (hN : IsNoetherian B S hS hZ F)
    (M : Modules.{u, u} B S hS F hF) (hM : IsCoherent B S hS F hF M)
    (G : ℕ → Subobject M)
    (hG : ∀ n, SheafOfModules.IsQuasicoherentOnSite (G n : Modules.{u, u} B S hS F hF))
    (hmono : Monotone G) :
    ∃ n, ∀ k, n ≤ k → G k = G n

Tag 07UK, a lemma

Tag 07UK in the Stacks Project.

AlgebraicGeometry.Space.exists_idealPowSmul_eq_bot_iff_supportOfSheaf_subset_idealZeroLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IdealPowerSupport.lean, line 815. References: EGA I (9.3.4), “more general”.

Stacks 07UK. Let X be a Noetherian algebraic space over a scheme S, let F be a coherent 𝒪_X-module and let ℐ ⊆ 𝒪_X be a quasi-coherent sheaf of ideals, cutting out the closed subspace Z ⊆ X. Then ℐⁿ F = 0 for some n ≥ 0 if and only if the support of F is contained in Z, set theoretically.

The closed subspace enters only through its point set |V(ℐ)|, which is what the set-theoretic containment refers to. For the forward implication no finiteness is needed: over a chart on which ℐ is the whole structure sheaf, and over every chart below it, F has no sections at all, so the support misses the image of that chart. The converse is the substantial half: on a surjective affine chart with Noetherian ring of sections, which a Noetherian algebraic space has, the sections of F form a finite module annihilated by a power of each section of ℐ, hence by a power of ℐ(U) because the ring is Noetherian; and quasi-coherence carries that single annihilation to every chart.

theorem exists_idealPowSmul_eq_bot_iff_supportOfSheaf_subset_idealZeroLocus
    (hZ : B.Contains (⊤_ Scheme.{u})) (X : AlgebraicSpaces B S hS)
    (hN : IsNoetherian B S hS hZ X.1)
    (M : Modules.{u, u} B S hS X.1 X.2) (hM : IsCoherent B S hS X.1 X.2 M)
    (I : (SheafOfModules.unit (structureRingSheaf B S hS X)).Submodule)
    (hI : I.toSheafOfModules.IsQuasicoherentOnSite) :
    (∃ n : ℕ, Stacks.Sites.idealSmul (M := M)
        (Stacks.Sites.idealPow (O := (smallEtaleRingedSite B S hS X.1 X.2).O) I n) ⊤ = ⊥) ↔
      supportOfSheaf B S hS X.1 ((SheafOfModules.toSheaf _).obj M) ⊆
        idealZeroLocus B S hS X I

Tag 07UL, a lemma

Tag 07UL in the Stacks Project.

AlgebraicGeometry.Space.exists_idealPowSmul_inf_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentArtinRees.lean, line 511.

Artin-Rees for a quasi-coherent submodule G of a coherent module M and a quasi-coherent sheaf of ideals I on a Noetherian algebraic space: there is a c ≥ 0 with I ⁿ⁻ᶜ (I ᶜ M ⊓ G) = I ⁿ M ⊓ G for every n ≥ c.

theorem exists_idealPowSmul_inf_eq (hZ : B.Contains (⊤_ Scheme.{u}))
    (hN : IsNoetherian B S hS hZ F) (M : Modules.{u, u} B S hS F hF)
    (hM : IsCoherent B S hS F hF M) (G : M.Submodule)
    (hG : G.toSheafOfModules.IsQuasicoherentOnSite) (I : IdealSheaves B S hS F hF)
    (hI : I.toSheafOfModules.IsQuasicoherentOnSite) :
    ∃ c : ℕ, ∀ n : ℕ, c ≤ n →
      Stacks.Sites.idealPowSmul I (n - c) (idealPowSubmodule I c M ⊓ G)
        = idealPowSubmodule I n M ⊓ G

Tag 07UM, a lemma

Tag 07UM in the Stacks Project.

AlgebraicGeometry.Space.canonicalMapToHomRestrict_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentHomColimitBijective.lean, line 84. The attribute's comment: “first display”.

[Stacks, Tag 07UM], first display. For a Noetherian algebraic space X over S, a quasi-coherent sheaf of ideals ℐ with open complement U = X ∖ V(ℐ), a coherent 𝒪_X-module 𝒢 and a quasi-coherent 𝒪_X-module ℱ, the canonical map

colim_n Hom_{𝒪_X}(ℐⁿ 𝒢, ℱ) ⟶ Hom_{𝒪_U}(𝒢|_U, ℱ|_U)

is bijective.

Injectivity is AlgebraicGeometry.Space.canonicalMapToHomRestrict_injective: a morphism φ : ℐⁿ𝒢 ⟶ ℱ vanishing on U has coherent image supported in V(ℐ), so some power of ℐ annihilates that image and φ dies on a deeper step of the filtration. Surjectivity is AlgebraicGeometry.Space.canonicalMapToHomRestrict_surjective: a morphism 𝒢|_U ⟶ ℱ|_U is transported to a surjective Noetherian affine chart, extended there by the first display of [Stacks, Tag 01YB] on the chart's scheme, made compatible on the kernel pair by raising the exponent of the ideal, and glued.

theorem canonicalMapToHomRestrict_bijective (hZ : B.Contains (⊤_ Scheme.{u}))
    (hN : IsNoetherian B S hS hZ X.1) (hI : I.toSheafOfModules.IsQuasicoherentOnSite)
    (G F : Modules.{u, u} B S hS X.1 X.2) (hG : IsCoherent B S hS X.1 X.2 G)
    [F.IsQuasicoherentOnSite] :
    Function.Bijective (canonicalMapToHomRestrict B S hS X I G F)

AlgebraicGeometry.Space.canonicalMapToSections_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentHomColimitBijective.lean, line 109. The attribute's comment: “the in particular display”.

[Stacks, Tag 07UM], the "in particular" display. For a Noetherian algebraic space X over S, a quasi-coherent sheaf of ideals ℐ with open complement U = X ∖ V(ℐ) and a quasi-coherent 𝒪_X-module ℱ, the canonical map

colim_n Hom_{𝒪_X}(ℐⁿ, ℱ) ⟶ Γ(U, ℱ|_U)

is bijective.

This is AlgebraicGeometry.Space.canonicalMapToHomRestrict_bijective at 𝒢 = 𝒪_X, which is legitimate because the structure sheaf of a Noetherian algebraic space is coherent (AlgebraicGeometry.Space.isCoherent_structureSheaf, the structure-sheaf clause of [Stacks, Tag 07UB]), composed with the bijection SheafOfModules.unitHomEquiv identifying the morphisms 𝒪_U ⟶ ℱ|_U with the sections of ℱ|_U. Noetherian implies the étale-local Noetherian property that the coherence of the structure sheaf asks for, which is hN.2.2.

theorem canonicalMapToSections_bijective (hZ : B.Contains (⊤_ Scheme.{u}))
    (hN : IsNoetherian B S hS hZ X.1) (hI : I.toSheafOfModules.IsQuasicoherentOnSite)
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite] :
    Function.Bijective (canonicalMapToSections B S hS X I F)

AlgebraicGeometry.Space.idealPowHomRestrict, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/HomOverIdealUnitLocus.lean, line 325. The attribute's comment: “the canonical map of the first display, term by term”.

The canonical map of the first display of [Stacks, Tag 07UM], term by term. A morphism φ : ℐⁿ G ⟶ F restricts along an étale morphism j : Y ⟶ X whose image misses V(ℐ) to a morphism G|_Y ⟶ F|_Y, the source being read through the isomorphism ℐⁿ G|_Y ≅ G|_Y of AlgebraicGeometry.Space.isIso_etaleModulePullback_idealPowModuleι.

These maps agree along the transition maps of the direct system, which is AlgebraicGeometry.Space.idealPowHomRestrict_homOfLE, so together they are a single map out of colim_n Hom_{𝒪_X}(ℐⁿ G, F). The bijectivity asserted by the tag is not proved; see the section "What is not proved" of the module documentation.

noncomputable def idealPowHomRestrict {Y : AlgebraicSpaces B S hS} (j : Y ⟶ X)
    (hj : IsEtale B S hS j.hom) (I : IdealSheaves B S hS X.1 X.2)
    (hjU : Set.range (pointsMap B S hS Y.1 j.hom) ⊆ idealUnitLocus B S hS X I)
    (n : ℕ) {M N : Modules.{u, u} B S hS X.1 X.2} (φ : idealPowModule I n M ⟶ N) :
    (etaleModulePullback B S hS j hj).obj M ⟶ (etaleModulePullback B S hS j hj).obj N

Sources

• Section 69.13, Tag 07UI
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.exists_eventually_constant_quasicoherentSubobjects · AlgebraicGeometry.Space.exists_idealPowSmul_eq_bot_iff_supportOfSheaf_subset_idealZeroLocus · AlgebraicGeometry.Space.exists_idealPowSmul_inf_eq · AlgebraicGeometry.Space.canonicalMapToHomRestrict_bijective · AlgebraicGeometry.Space.canonicalMapToSections_bijective · AlgebraicGeometry.Space.idealPowHomRestrict

Section69.14 Devissage of coherent sheaves#

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

Tag 07UP, a lemma

Tag 07UP in the Stacks Project.

AlgebraicGeometry.Space.exists_shortExact_coherent_supportOfSheaf_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentSupportSeparation.lean, line 180.

Stacks 07UP. Let X be a Noetherian algebraic space over a scheme S and let F be a coherent 𝒪_X-module whose support is the union Z ∪ Z' of two closed subsets of |X|. Then there is a short exact sequence 0 → 𝒢' → F → 𝒢 → 0 of coherent 𝒪_X-modules with 𝒢' supported in Z' and 𝒢 supported in Z.

The sequence produced is the canonical one: 𝒢' is the subsheaf of sections of F supported in Z' and 𝒢 is the quotient of F by it. Quasi-coherence of 𝒢' is part (3) of Stacks 0859, whose hypotheses hold because the complement of Z' is an open subspace of X and its inclusion is quasi-compact, X being Noetherian; 𝒢' is then coherent by Stacks 07UD and 𝒢 by Stacks 07UC.

theorem exists_shortExact_coherent_supportOfSheaf_subset
    (hTop : B.Contains (⊤_ Scheme.{u})) (hN : IsNoetherian B S hS hTop X.1)
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : IsCoherent B S hS X.1 X.2 F)
    (Z Z' : Set (points B S hS X.1)) (hZ : IsClosed Z) (hZ' : IsClosed Z')
    (hsupp : supportOfSheaf B S hS X.1 (moduleAddSheaf B S hS X.1 X.2 F) = Z ∪ Z') :
    ∃ (G' G : Modules.{u, u} B S hS X.1 X.2) (i : G' ⟶ F) (p : F ⟶ G) (w : i ≫ p = 0),
      (ShortComplex.mk i p w).ShortExact ∧ IsCoherent B S hS X.1 X.2 G' ∧
        IsCoherent B S hS X.1 X.2 G ∧
        supportOfSheaf B S hS X.1 (moduleAddSheaf B S hS X.1 X.2 G') ⊆ Z' ∧
        supportOfSheaf B S hS X.1 (moduleAddSheaf B S hS X.1 X.2 G) ⊆ Z

Tag 07UQ, a lemma

Tag 07UQ in the Stacks Project.

AlgebraicGeometry.Space.exists_mono_modulePushforward_idealSum_of_schemeTheoreticSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentIrreducibleIdealInjection.lean, line 667.

[Stacks, Tag 07UQ]. Let X be a Noetherian algebraic space over S and let ℱ be a coherent 𝒪_X-module whose scheme-theoretic support i : Z → X is reduced with |Z| irreducible. Then there are an integer r > 0, a nonzero quasi-coherent sheaf of ideals ℐ ⊆ 𝒪_Z and an injective map of coherent modules i_*(ℐ^{⊕ r}) → ℱ whose cokernel is supported on a proper closed subspace of Z, namely on the image of a closed T ⊊ |Z|.

The scheme-theoretic support is a closed subspace (it is part of the conclusion), ℱ = i_*𝒢 for a quasi-coherent 𝒪_Z-module 𝒢 by [Stacks, Tag 07U0], 𝒢 is coherent by [Stacks, Tag 07UG], and its support is all of |Z| because the support of ℱ is the image of |Z| and i is injective on points. The case Z = X, AlgebraicGeometry.Space.exists_mono_biproduct_idealSheaf_cokernel_support_subset, applies to 𝒢 on the Noetherian space Z; the direct image is exact, so it keeps the injection and carries the cokernel to the cokernel, whose support is then in the image of T. The source i_*(ℐ^{⊕ r}) is quasi-coherent, the direct image along a closed immersion preserving quasi-coherence, and it is a submodule of the coherent ℱ, hence coherent by [Stacks, Tag 07UD].

theorem exists_mono_modulePushforward_idealSum_of_schemeTheoreticSupport
    (noeth : IsNoetherian B S hS hZt X.1) (F : Modules.{u, u} B S hS X.1 X.2)
    (coh : IsCoherent B S hS X.1 X.2 F)
    (redIrr : IsReducedIrreducible B S hS (schemeTheoreticSupport B S hS X F)) :
    ∃ hZ : IsClosedSubspace B S hS (schemeTheoreticSupport B S hS X F),
      ∃ (r : ℕ) (I : (SheafOfModules.unit ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS
          (closedSubfunctorSpace B S hS hZ).1 (closedSubfunctorSpace B S hS hZ).2).O))).Submodule),
        I.toSheafOfModules.IsQuasicoherentOnSite ∧ 0 < r ∧ I ≠ ⊥ ∧
        IsCoherent B S hS X.1 X.2 ((modulePushforward B S hS (closedSubfunctorι B S hS hZ)).obj
          (⨁ fun _ : Fin r => I.toSheafOfModules)) ∧
        ∃ φ : (modulePushforward B S hS (closedSubfunctorι B S hS hZ)).obj
            (⨁ fun _ : Fin r => I.toSheafOfModules) ⟶ F, Mono φ ∧
          ∃ (Q : Modules.{u, u} B S hS X.1 X.2) (q : F ⟶ Q) (w : φ ≫ q = 0),
            Nonempty (IsColimit (CokernelCofork.ofπ q w)) ∧
            ∃ T : Set (points B S hS (schemeTheoreticSupport B S hS X F).toFunctor),
              IsClosed T ∧ T ≠ Set.univ ∧
              supportOfSheaf B S hS X.1 ((SheafOfModules.toSheaf _).obj Q) ⊆
                pointsMap B S hS _ (closedSubfunctorι B S hS hZ).hom '' T

Tag 07UR, a lemma

Tag 07UR in the Stacks Project.

AlgebraicGeometry.Space.hasIdealDevissage_of_isCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentDevissageFiltration.lean, line 872.

Stacks Project, Tag 07UR. Let X be a Noetherian algebraic space over a scheme S and let F be a coherent 𝒪_X-module. Then F carries a filtration

0 = F₀ ⊆ F₁ ⊆ … ⊆ F_m = F

by coherent submodules such that for each j there are a reduced closed subspace Z_j ⊆ X with |Z_j| irreducible and a quasi-coherent sheaf of ideals I_j ⊆ 𝒪_{Z_j} with F_j / F_{j-1} ≅ (Z_j → X)_* I_j.

The filtration is produced as a structure by AlgebraicGeometry.Space.hasTagFiltration_of_isCoherent and read in this existential form by AlgebraicGeometry.Space.hasIdealDevissage_of_hasTagFiltration.

theorem hasIdealDevissage_of_isCoherent (terminal : B.Contains (⊤_ Scheme.{u}))
    (X : AlgebraicSpaces B S hS) (noeth : IsNoetherian B S hS terminal X.1)
    (M : Modules.{u, u} B S hS X.1 X.2) (coh : IsCoherent B S hS X.1 X.2 M) :
    HasIdealDevissage B S hS X M

Tag 07US, a lemma

Tag 07US in the Stacks Project.

AlgebraicGeometry.Space.property_of_ideal_pushforward_and_extensions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentDevissageInduction.lean, line 131.

Let X be a Noetherian algebraic space over S and let P be a property of 𝒪_X-modules such that

1. for a short exact sequence 0 → F₁ → F → F₂ → 0 of coherent modules, if F₁ and F₂ have P then so does F;
2. for every reduced closed subspace i : Z → X with |Z| irreducible and every quasi-coherent sheaf of ideals I ⊆ 𝒪_Z, P holds for i_*I.

Suppose moreover that X has a point or that P holds for every zero module. Then P holds for every coherent module on X.

Without the alternative the statement fails when |X| is empty (AlgebraicGeometry.Space.exists_isNoetherian_not_forall_property).

theorem property_of_ideal_pushforward_and_extensions (X : AlgebraicSpaces B S hS)
    (noetherian : IsNoetherian B S hS B.contains_terminal X.1)
    (P : Modules.{u, u} B S hS X.1 X.2 → Prop)
    (nonempty_or_zero : Nonempty (points B S hS X.1) ∨
      ∀ M : Modules.{u, u} B S hS X.1 X.2, IsZero M → P M)
    (extensions : ClosedUnderCoherentExtensions B S hS X P)
    (idealPushforward : ∀ (Z : Subfunctor X.1) (closed : IsClosedSubspace B S hS Z),
      IsReducedIrreducible B S hS Z →
      ∀ I : QuasicoherentIdeals B S hS (closedSubfunctorSpace B S hS closed),
        P ((modulePushforward B S hS (closedSubfunctorι B S hS closed)).obj
          I.1.toSheafOfModules))
    (M : Modules.{u, u} B S hS X.1 X.2) (coherent : IsCoherent B S hS X.1 X.2 M) : P M

Tag 07UT, a lemma

Tag 07UT in the Stacks Project.

AlgebraicGeometry.Space.property_of_isCoherent_of_hasGenericSubsheaves, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentDevissageCriterion.lean, line 621.

Stacks Project, Tag 07UT. Let X be a Noetherian algebraic space over a scheme S and let P be a property of coherent 𝒪_X-modules such that

1. for a short exact sequence 0 → F₁ → F → F₂ → 0 of coherent modules, if F₁ and F₂ have P then so does F;
2. if P holds for F^{⊕ r} for some r ≥ 1, then it holds for F;
3. for every reduced closed subspace i : Z → X with |Z| irreducible there is a coherent 𝒪_Z-module 𝒢 with Supp(𝒢) = Z such that for every nonzero quasi-coherent sheaf of ideals ℐ ⊆ 𝒪_Z there is a quasi-coherent 𝒢' ⊆ ℐ𝒢 with Supp(𝒢/𝒢') a proper closed subset of |Z| and P(i_*𝒢')

and such that P holds for the zero module. Then P holds for every coherent 𝒪_X-module.

The source does not list the zero module among its hypotheses, and its conclusion fails without it: the property "is nonzero" satisfies (1), (2) and (3) — in (3) take 𝒢 = 𝒪_Z and 𝒢' = ℐ𝒪_Z — and does not hold for the zero module. The source's proof runs over the nonempty supports only.

The proof is the source's Noetherian induction on the support of F, run over the closed subsets of |X|, a Noetherian topological space by Stacks 04ZF. A module with empty support is zero; a reducible support is split by Stacks 07UP and (1) concludes; an irreducible support is AlgebraicGeometry.Space.property_of_isIrreducible.

theorem property_of_isCoherent_of_hasGenericSubsheaves
    (noeth : IsNoetherian B S hS B.contains_terminal X.1)
    (zero : ∀ M : Modules.{u, u} B S hS X.1 X.2, IsZero M → P M)
    (extension : ClosedUnderCoherentExtensions B S hS X P)
    (ofSum : ∀ F : Modules.{u, u} B S hS X.1 X.2, IsCoherent B S hS X.1 X.2 F →
      ∀ r : ℕ, 1 ≤ r → P (⨁ fun _ : Fin r => F) → P F)
    (generic : HasGenericSubsheaves B S hS X P)
    (F : Modules.{u, u} B S hS X.1 X.2) (coherent : IsCoherent B S hS X.1 X.2 F) : P F

Tag 08AN, a lemma

Tag 08AN in the Stacks Project.

AlgebraicGeometry.Space.property_of_integralWitness_and_twoOutOfThree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentDevissageHigherRank.lean, line 874. The attribute's comment: “the dévissage principle in its higher-rank form: the Noetherian induction, the minimal-subspace step, the support of a nonzero ideal direct image, the ideal-intersection paragraph and 07UQ in the shape the step consumes, from 07US, 07UR and 07UQ, carrying the conclusion of 07UR, the coherence clause of 07UH for the direct image of a quasi-coherent sheaf of ideals, and 07UQ's own two inputs: 07U0's module on the support and the surjectivity half of 07UM”.

Stacks Project, Tag 08AN. Let X be a Noetherian algebraic space over a scheme S and let P be a property of coherent 𝒪_X-modules such that

1. for a short exact sequence of coherent modules, if two out of three terms have P then so does the third;
2. if P holds for the direct sum of r ≥ 1 copies of a module, for some r ≥ 1, then it holds for that module;
3. for every reduced closed subspace Z ⊆ X with |Z| irreducible there is a coherent module on X whose scheme-theoretic support is Z and which has P.

Then P holds for every coherent module on X.

Three hypotheses are carried beyond the source's list, and each is discussed in the module documentation. None of them is mathematics of Stacks 08AN: each is the conclusion, or a named clause, of another tag, and each is a statement that tag's own formalization here still carries.

• hdev, the conclusion of Stacks 07UR for every coherent module on X, which is AlgebraicGeometry.Space.hasIdealDevissage_of_isCoherent.
• h07UH, AlgebraicGeometry.Space.IdealPushforwardCoherent: the coherence clause of Stacks 07UH at the inclusion of a closed subspace and a quasi-coherent sheaf of ideals on it.
• hinputs, AlgebraicGeometry.Space.ExistsSupportModuleAndGenericTrivialization: the two inputs of Stacks 07UQ, namely the module on the scheme-theoretic support from Stacks 07U0 — which rests on the essential-image assertion of Stacks 04CJ part (3) — and the generically bijective map of the surjectivity half of Stacks 07UM.

Everything else — the Noetherian induction, the step at a minimal subspace, the equality of the supports of the direct images of two nonzero sheaves of ideals on Z, the last paragraph of the source's proof in AlgebraicGeometry.Space.idealPushforwardComparison, Stacks 07UQ itself in AlgebraicGeometry.Space.existsIdealInjectionDevissageStep, and the passage from sheaves of ideals to all coherent modules through Stacks 07US — is proved here.

The hypothesis hzero is not in the source's list and cannot be dropped, for the reason recorded at the library's Stacks 07US: on an algebraic space with no points the property fun _ => False satisfies the source's three conditions while the zero module is coherent and does not have it.

theorem property_of_integralWitness_and_twoOutOfThree (hZtop : B.Contains (⊤_ Scheme.{u}))
    (X : AlgebraicSpaces B S hS) (hX : IsNoetherian B S hS hZtop X.1)
    (hdev : ∀ M : Modules.{u, u} B S hS X.1 X.2, IsCoherent B S hS X.1 X.2 M →
      HasIdealDevissage B S hS X M)
    (h07UH : IdealPushforwardCoherent B S hS X)
    (hinputs : ExistsSupportModuleAndGenericTrivialization B S hS X)
    (P : Modules.{u, u} B S hS X.1 X.2 → Prop)
    (hzero : ∀ M : Modules.{u, u} B S hS X.1 X.2, IsZero M → P M)
    (h1 : TwoOutOfThreeCoherent B S hS X P) (h2 : ClosedUnderDirectSumDescent B S hS X P)
    (h3 : HasCoherentWitnessOnIntegralSubspaces B S hS X P)
    (M : Modules.{u, u} B S hS X.1 X.2) (hM : IsCoherent B S hS X.1 X.2 M) : P M

AlgebraicGeometry.Space.property_of_integralWitness_and_twoOutOfThree', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentDevissageHigherRankIdeal.lean, line 266. The attribute's comment: “the dévissage principle in its higher-rank form: the Noetherian induction, the minimal-subspace step, the support of a nonzero ideal direct image, the ideal-intersection paragraph and 07UQ in the shape the step consumes, from 07US, 07UR and 07UQ. The one argument beside the source's list is the conclusion of 07UR for every coherent module on X”.

Let X be a Noetherian algebraic space over a scheme S and let P be a property of coherent 𝒪_X-modules such that

1. for a short exact sequence of coherent modules, if two out of three terms have P then so does the third;
2. if P holds for the direct sum of r ≥ 1 copies of a module, for some r ≥ 1, then it holds for that module;
3. for every reduced closed subspace Z ⊆ X with |Z| irreducible there is a coherent module on X whose scheme-theoretic support is Z and which has P.

Then P holds for every coherent module on X.

One hypothesis stands beside the source's list, hdev: the conclusion of Stacks 07UR for every coherent module on X, which is AlgebraicGeometry.Space.hasIdealDevissage_of_isCoherent. It is not mathematics of Stacks 08AN — it is the conclusion of another tag, stated in the shape this proof uses.

Everything else is proved: the Noetherian induction, the step at a minimal subspace, the equality of the supports of the direct images of two nonzero sheaves of ideals on Z, the last paragraph of the source's proof in AlgebraicGeometry.Space.idealPushforwardComparison, Stacks 07UQ in AlgebraicGeometry.Space.existsIdealInjectionDevissageStep', and the passage from sheaves of ideals to all coherent modules through Stacks 07US, with the coherence clause of Stacks 07UH from AlgebraicGeometry.Space.idealPushforwardCoherent.

The hypothesis hzero is not in the source's list and cannot be dropped, for the reason recorded at Stacks 07US: on an algebraic space with no points the property fun _ => False satisfies the source's three conditions while the zero module is coherent and does not have it.

theorem property_of_integralWitness_and_twoOutOfThree' (hZtop : B.Contains (⊤_ Scheme.{u}))
    (X : AlgebraicSpaces B S hS) (hX : IsNoetherian B S hS hZtop X.1)
    (hdev : ∀ M : Modules.{u, u} B S hS X.1 X.2, IsCoherent B S hS X.1 X.2 M →
      HasIdealDevissage B S hS X M)
    (P : Modules.{u, u} B S hS X.1 X.2 → Prop)
    (hzero : ∀ M : Modules.{u, u} B S hS X.1 X.2, IsZero M → P M)
    (h1 : TwoOutOfThreeCoherent B S hS X P) (h2 : ClosedUnderDirectSumDescent B S hS X P)
    (h3 : HasCoherentWitnessOnIntegralSubspaces B S hS X P)
    (M : Modules.{u, u} B S hS X.1 X.2) (hM : IsCoherent B S hS X.1 X.2 M) : P M

AlgebraicGeometry.Space.property_of_integralWitness_and_twoOutOfThree_of_isNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentDevissageHigherRankNoetherian.lean, line 221. The attribute's comment: “for a property which holds on zero modules: the source's statement fails for an X with no points, and for X with a point that hypothesis follows from (1) and (3)”.

Stacks Project, Tag 08AN. Let X be a Noetherian algebraic space over a scheme S and let P be a property of coherent 𝒪_X-modules, holding on zero modules, such that

1. for a short exact sequence of coherent modules, if two out of three terms have P then so does the third;
2. if P holds for the direct sum of r ≥ 1 copies of a module, for some r ≥ 1, then it holds for that module;
3. for every reduced closed subspace Z ⊆ X with |Z| irreducible there is a coherent module on X whose scheme-theoretic support is Z and which has P.

Then P holds for every coherent module on X.

The hypothesis hzero is not in the source's list, and the source's statement is false without it when X has no points (AlgebraicGeometry.Space.not_forall_false_of_isEmpty_points); when X has a point it follows from (1) and (3), which is AlgebraicGeometry.Space.property_of_integralWitness_and_twoOutOfThree_of_nonempty.

theorem property_of_integralWitness_and_twoOutOfThree_of_isNoetherian
    (hZtop : B.Contains (⊤_ Scheme.{u}))
    (X : AlgebraicSpaces B S hS) (hX : IsNoetherian B S hS hZtop X.1)
    (P : Modules.{u, u} B S hS X.1 X.2 → Prop)
    (hzero : ∀ M : Modules.{u, u} B S hS X.1 X.2, IsZero M → P M)
    (h1 : TwoOutOfThreeCoherent B S hS X P) (h2 : ClosedUnderCoherentDirectSumDescent B S hS X P)
    (h3 : HasCoherentWitnessOnIntegralSubspaces B S hS X P)
    (M : Modules.{u, u} B S hS X.1 X.2) (hM : IsCoherent B S hS X.1 X.2 M) : P M

AlgebraicGeometry.Space.property_of_coherent_of_isNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentDevissageNoetherian.lean, line 97. The attribute's comment: “corrected: P is also required to hold for zero modules, without which the statement fails on an algebraic space with no points”.

Stacks Project, Tag 08AN. Let X be a Noetherian algebraic space over a scheme S and let P be a property of coherent 𝒪_X-modules such that

1. for a short exact sequence of coherent modules, if two out of three terms have P then so does the third;
2. if P holds for the direct sum of r ≥ 1 copies of a coherent module then it holds for that module;
3. for every reduced closed subspace Z ⊆ X with |Z| irreducible there is a coherent module on X whose scheme-theoretic support is Z and which has P.

Then P holds for every coherent module on X.

The hypothesis hzero, that P holds for zero modules, corrects the source, whose statement fails on an algebraic space with no points; see the module documentation. Condition (2) is asked only of coherent modules, as in the source, where P is a property of coherent sheaves; the proof runs the dévissage for the property M ↦ (M coherent → P M), for which condition (2) holds at every module. The three inputs that AlgebraicGeometry.Space.property_of_integralWitness_and_twoOutOfThree carries are discharged: Stacks 07UR by AlgebraicGeometry.Space.hasIdealDevissage_of_isCoherent, coherence of i_*I by AlgebraicGeometry.Space.isCoherent_modulePushforward_quasicoherentIdeal, and Stacks 07UQ by AlgebraicGeometry.Space.existsIdealInjectionDevissageStep_of_isNoetherian.

theorem property_of_coherent_of_isNoetherian (hZtop : B.Contains (⊤_ Scheme.{u}))
    (X : AlgebraicSpaces B S hS) (hX : IsNoetherian B S hS hZtop X.1)
    (P : Modules.{u, u} B S hS X.1 X.2 → Prop)
    (hzero : ∀ M : Modules.{u, u} B S hS X.1 X.2, IsZero M → P M)
    (h1 : TwoOutOfThreeCoherent B S hS X P)
    (h2 : ∀ F : Modules.{u, u} B S hS X.1 X.2, IsCoherent B S hS X.1 X.2 F → ∀ r : ℕ, 1 ≤ r →
      P (⨁ fun _ : Fin r => F) → P F)
    (h3 : HasCoherentWitnessOnIntegralSubspaces B S hS X P)
    (M : Modules.{u, u} B S hS X.1 X.2) (hM : IsCoherent B S hS X.1 X.2 M) : P M

AlgebraicGeometry.Space.property_of_isCoherent_of_devissage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentDevissageUnconditional.lean, line 218. The attribute's comment: “with the hypothesis that P holds for zero modules added: without it the statement fails on an algebraic space with no points, for the property False”.

Stacks Project, Tag 08AN. Let X be a Noetherian algebraic space over a scheme S and let P be a property of coherent 𝒪_X-modules such that

1. for a short exact sequence of coherent modules, if two out of three terms have P then so does the third;
2. if P holds for the direct sum of r ≥ 1 copies of a module then it holds for that module;
3. for every reduced closed subspace Z ⊆ X with |Z| irreducible there is a coherent module on X whose scheme-theoretic support is Z and which has P.

Then P holds for every coherent module on X.

The hypothesis hzero is the one correction to the source's statement: see the module documentation. Nothing else is carried: the conclusion of Stacks 07UR is AlgebraicGeometry.Space.hasIdealDevissage_of_isCoherent, the coherence of the direct image of a sheaf of ideals is AlgebraicGeometry.Space.idealPushforwardCoherent, and Stacks 07UQ is AlgebraicGeometry.Space.existsIdealInjectionDevissageStep_of_isNoetherian.

theorem property_of_isCoherent_of_devissage (hZtop : B.Contains (⊤_ Scheme.{u}))
    (X : AlgebraicSpaces B S hS) (hX : IsNoetherian B S hS hZtop X.1)
    (P : Modules.{u, u} B S hS X.1 X.2 → Prop)
    (hzero : ∀ M : Modules.{u, u} B S hS X.1 X.2, IsZero M → P M)
    (h1 : TwoOutOfThreeCoherent B S hS X P) (h2 : ClosedUnderDirectSumDescent B S hS X P)
    (h3 : HasCoherentWitnessOnIntegralSubspaces B S hS X P)
    (M : Modules.{u, u} B S hS X.1 X.2) (hM : IsCoherent B S hS X.1 X.2 M) : P M

Sources

• Section 69.14, Tag 07UN
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.exists_shortExact_coherent_supportOfSheaf_subset · AlgebraicGeometry.Space.exists_mono_modulePushforward_idealSum_of_schemeTheoreticSupport · AlgebraicGeometry.Space.hasIdealDevissage_of_isCoherent · AlgebraicGeometry.Space.property_of_ideal_pushforward_and_extensions · AlgebraicGeometry.Space.property_of_isCoherent_of_hasGenericSubsheaves · AlgebraicGeometry.Space.property_of_integralWitness_and_twoOutOfThree · AlgebraicGeometry.Space.property_of_integralWitness_and_twoOutOfThree' · AlgebraicGeometry.Space.property_of_integralWitness_and_twoOutOfThree_of_isNoetherian

Section69.15 Limits of coherent modules#

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

Tag 07UV, a lemma

Tag 07UV in the Stacks Project.

AlgebraicGeometry.Space.isFiltered_and_nonempty_isColimit_coherentSubobjectCocone, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentSubmoduleColimitNoetherian.lean, line 846.

Let X be a Noetherian algebraic space over a scheme S. Every quasi-coherent 𝒪_X-module F is the filtered colimit of its coherent submodules: the coherent submodules of F form a filtered category, and the cocone of their inclusions into F is a colimit cocone.

theorem isFiltered_and_nonempty_isColimit_coherentSubobjectCocone
    (terminal_mem : B.Contains (⊤_ Scheme.{u})) (noetherian : IsNoetherian B S hS terminal_mem X)
    (F : Modules.{u, u} B S hS X hX) [hFq : F.IsQuasicoherentOnSite] :
    IsFiltered (CoherentSubobject B S hS X hX F) ∧
      Nonempty (IsColimit (coherentSubobjectCocone B S hS X hX F))

Tag 07UW, a lemma

Tag 07UW in the Stacks Project.

AlgebraicGeometry.Space.isFilteredColimit_isFinitePresentation_of_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePresentationColimitAffineOverNoetherian.lean, line 188. The attribute's comment: “granted five general cited inputs: hNoeth (the Noetherian case, Stacks 07UV with 07UB), hpush (Stacks 08AI), hpull (Stacks 03LU, 05VR), hepi (Stacks 03LX, step 3) and hqcqs”.

Stacks 07UW. Let f : X ⟶ Y be an affine morphism of algebraic spaces over a scheme S with Y Noetherian. Then every quasi-coherent 𝒪_X-module is a filtered colimit of 𝒪_X-modules of finite presentation.

No clause of the tag's conclusion is dropped or weakened, and the tag's own hypotheses — f affine, Y Noetherian, the module quasi-coherent — are the hypotheses here. What is granted beyond them are the five general cited inputs hNoeth, hpush, hpull, hepi and hqcqs, each quantified over its own algebraic spaces, morphisms and modules and none of them mentioning f, X, Y or F; see the module docstring for what each one is and for which tag it stands in. In particular hNoeth is the assertion for a Noetherian space, namely Stacks 07UV with Stacks 07UB, which the source quotes here and which is not the conclusion below: X is affine over a Noetherian space, not Noetherian, and the transfer along f is the content of the tag.

Everything else in the source's proof is discharged: the pullback of the presentation and the quotient presentation of an arbitrary quasi-coherent module (AlgebraicGeometry.Space.exists_epi_isColimit_isFinitePresentation_of_isAffineHom), the identification of F as a cokernel of a map between two such colimits, Stacks 07U7 on X, and the formal passage from that cokernel to the filtered colimit of the cokernels of the representing maps.

theorem isFilteredColimit_isFinitePresentation_of_isAffineHom
    (hNoeth : ∀ Z : AlgebraicSpaces B S hS, IsNoetherian B S hS hZ Z.1 →
      ∀ N : Modules.{u, u} B S hS Z.1 Z.2, N.IsQuasicoherentOnSite →
        ∃ (I : Type u) (inst : SmallCategory I),
          let _ := inst
          ∃ (_ : IsFiltered I) (D : I ⥤ Modules.{u, u} B S hS Z.1 Z.2)
            (φ : D ⟶ (Functor.const I).obj N),
            (∀ i, (D.obj i).IsFinitePresentation) ∧ Nonempty (IsColimit (Cocone.mk N φ)))
    (hpush : ∀ (Z W : AlgebraicSpaces B S hS) (g : Z ⟶ W), IsAffineHom B S hS g.hom →
      ∀ N : Modules.{u, u} B S hS Z.1 Z.2, N.IsQuasicoherentOnSite →
        ((modulePushforward B S hS g).obj N).IsQuasicoherentOnSite)
    (hpull : ∀ (Z W : AlgebraicSpaces B S hS) (g : Z ⟶ W) (N : Modules.{u, u} B S hS W.1 W.2),
      (N.IsQuasicoherentOnSite → ((modulePullback B S hS g).obj N).IsQuasicoherentOnSite) ∧
        (N.IsFinitePresentation → ((modulePullback B S hS g).obj N).IsFinitePresentation))
    (hepi : ∀ (Z W : AlgebraicSpaces B S hS) (g : Z ⟶ W), IsAffineHom B S hS g.hom →
      ∀ N : Modules.{u, u} B S hS Z.1 Z.2, N.IsQuasicoherentOnSite →
        Epi ((modulePullbackAdjunction B S hS g).counit.app N))
    (hqcqs : ∀ (Z W : AlgebraicSpaces B S hS) (g : Z ⟶ W), IsAffineHom B S hS g.hom →
      IsNoetherian B S hS hZ W.1 →
        IsQuasiCompactSpace B S hS Z.1 ∧ IsAbsolutelyQuasiSeparated B S hS hZ Z.1)
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (hf : IsAffineHom B S hS f.hom)
    (hY : IsNoetherian B S hS hZ Y.1)
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : F.IsQuasicoherentOnSite) :
    ∃ (K : Type (u + 1)) (inst : Category.{u} K),
      let _ := inst
      ∃ (_ : IsFiltered K) (D : K ⥤ Modules.{u, u} B S hS X.1 X.2)
        (φ : D ⟶ (Functor.const K).obj F),
        (∀ k, (D.obj k).IsFinitePresentation) ∧ Nonempty (IsColimit (Cocone.mk F φ))

AlgebraicGeometry.Space.exists_isFiltered_isColimit_isFinitePresentation_of_isAffineHom_of_isNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePresentationColimitAffineOverNoetherianUnconditional.lean, line 209. The attribute's comment: “every quasi-coherent 𝒪_X-module is a filtered colimit of finitely presented 𝒪_X-modules, for f : X ⟶ Y affine with Y Noetherian”.

Stacks 07UW. Let f : X ⟶ Y be an affine morphism of algebraic spaces over a scheme S with Y Noetherian. Then every quasi-coherent 𝒪_X-module is a filtered colimit of 𝒪_X-modules of finite presentation.

This is AlgebraicGeometry.Space.isFilteredColimit_isFinitePresentation_of_isAffineHom with its five inputs proved: the Noetherian case (AlgebraicGeometry.Space.exists_isFiltered_isColimit_isFinitePresentation_of_isNoetherian), Stacks 07U8 for the direct image, Stacks 03GA and 03DO (7) for the pullback, the surjectivity of the counit (AlgebraicGeometry.Space.epi_modulePullbackAdjunction_counit_app_of_isAffineHom) and the quasi-compactness and quasi-separatedness of X (AlgebraicGeometry.Space.isQuasiCompactSpace_and_isAbsolutelyQuasiSeparated_of_isAffineHom).

The index category is the category of triples (i, j, α) that the source's proof constructs, whose objects carry a morphism of 𝒪_X-modules, and so lives in Type (u + 1) with Hom-types in Type u.

theorem exists_isFiltered_isColimit_isFinitePresentation_of_isAffineHom_of_isNoetherian
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (hf : IsAffineHom B S hS f.hom)
    (hY : IsNoetherian B S hS hZ Y.1)
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : F.IsQuasicoherentOnSite) :
    ∃ (K : Type (u + 1)) (inst : Category.{u} K),
      let _ := inst
      ∃ (_ : IsFiltered K) (D : K ⥤ Modules.{u, u} B S hS X.1 X.2)
        (φ : D ⟶ (Functor.const K).obj F),
        (∀ k, (D.obj k).IsFinitePresentation) ∧ Nonempty (IsColimit (Cocone.mk F φ))

Sources

• Section 69.15, Tag 07UU
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.isFiltered_and_nonempty_isColimit_coherentSubobjectCocone · AlgebraicGeometry.Space.isFilteredColimit_isFinitePresentation_of_isAffineHom · AlgebraicGeometry.Space.exists_isFiltered_isColimit_isFinitePresentation_of_isAffineHom_of_isNoetherian

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.