103.4 Pullback of… to 103.12 Further remarks on…

Section103.4 Pullback of quasi-coherent modules#

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

Tag 076X, a lemma

Tag 076X in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.exactFunctor_quasicoherentPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentKernelsFlatObjects.lean, line 86.

Stacks 076X. If f : 𝒳 ⟶ 𝒴 is a flat morphism of algebraic stacks, then f^* : QCoh(𝒪_𝒴) ⥤ QCoh(𝒪_𝒳) is an exact functor: it preserves finite colimits, as it does for every f, and finite limits, because kernels of quasi-coherent modules are computed on flat objects (AlgebraicGeometry.Stack.AlgebraicStacks.quasicoherentKernelsOnFlatObjects) and f carries flat objects to flat objects.

theorem exactFunctor_quasicoherentPullback (hf : AlgebraicStacks.IsFlat B S hS f) :
    exactFunctor (quasicoherentModules B S hS 𝒴) (quasicoherentModules B S hS 𝒳)
      (quasicoherentPullback B S hS f)

AlgebraicGeometry.Stack.preservesFiniteColimits_quasicoherentPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/QuasicoherentPullbackExactness.lean, line 140. The attribute's comment: “right exactness”.

The inverse image of quasi-coherent modules along a 1-morphism of categories fibred in groupoids over the big fppf category of S, f^* : QCoh(𝒪_𝒴) ⥤ QCoh(𝒪_𝒳), is right exact.

theorem preservesFiniteColimits_quasicoherentPullback :
    PreservesFiniteColimits (quasicoherentPullback B S hS p q hp hq f hF)
Tag 0GQF, a lemma

Tag 0GQF in the Stacks Project.

AlgebraicGeometry.Stack.isIso_iff_restrictMapToSmallEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentFlatFamilyDetection.lean, line 344. The attribute's comment: “isomorphism”.

Stacks 0GQF, isomorphisms. Let 𝒳 be an algebraic stack and x_i : U_i → 𝒳, i ∈ I, flat objects with ∐ x_i : ∐ U_i → 𝒳 surjective. An arrow φ of QCoh(𝒪_𝒳) is an isomorphism if and only if each restriction φ_i = φ|_{(U_i)_{étale}} is.

theorem isIso_iff_restrictMapToSmallEtale :
    IsIso φ ↔ ∀ i, IsIso (restrictMapToSmallEtale B E h S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids
        (x i)
        ((PresheafOfModules.toPresheaf _).map φ.hom.val))

AlgebraicGeometry.Stack.epi_iff_restrictMapToSmallEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentFlatFamilyDetection.lean, line 370. The attribute's comment: “surjectivity”.

Stacks 0GQF, surjectivity. Let 𝒳 be an algebraic stack and x_i : U_i → 𝒳, i ∈ I, flat objects with ∐ x_i : ∐ U_i → 𝒳 surjective. An arrow φ of QCoh(𝒪_𝒳) is surjective (an epimorphism of QCoh(𝒪_𝒳)) if and only if each restriction φ_i = φ|_{(U_i)_{étale}} is surjective as a map of sheaves on (U_i)_{étale}, i.e. locally surjective for the étale topology.

theorem epi_iff_restrictMapToSmallEtale :
    Epi φ ↔ ∀ i, Presheaf.IsLocallySurjective (SmallEtale.topology E (𝒳.val.val.p.obj (x i)).left.1
        (contains_base B E h S hS 𝒳.val.val.p (x i)))
      (restrictMapToSmallEtale B E h S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids (x i)
        ((PresheafOfModules.toPresheaf _).map φ.hom.val))

AlgebraicGeometry.Stack.mono_iff_restrictMapToSmallEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentFlatFamilyMono.lean, line 73. The attribute's comment: “injectivity”.

Stacks 0GQF, injectivity. Let 𝒳 be an algebraic stack and x_i : U_i → 𝒳, i ∈ I, flat objects with ∐ x_i : ∐ U_i → 𝒳 surjective. An arrow φ of QCoh(𝒪_𝒳) is injective (a monomorphism of the abelian category QCoh(𝒪_𝒳)) if and only if each restriction φ_i = φ|_{(U_i)_{étale}} is injective on all sections.

theorem mono_iff_restrictMapToSmallEtale :
    Mono φ ↔ ∀ i V, Function.Injective ((restrictMapToSmallEtale B E h S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids (x i) ((PresheafOfModules.toPresheaf _).map φ.hom.val)).app V)
Sources

Section103.5 Higher direct images of types of modules#

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

Tag 076Z, a lemma

Tag 076Z in the Stacks Project.

AlgebraicGeometry.Stack.smoothLocalHigherDirectImageCriterion, an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/HigherDirectImageRuleSpectralSequence.lean, line 114. The attribute's comment: “the whole statement: every rule satisfying the source's four hypotheses, every quasi-compact quasi-separated 1-morphism of algebraic stacks and every degree; hypothesis (3) is read for the families indexed in a universe containing u, which the source's hypothesis implies, so the statement is no weaker than the source's”.

Stacks 076Z. Let M be a rule assigning to a category fibred in groupoids over S a predicate on the modules on its étale site. If M cuts out a weak Serre subcategory everywhere, is stable under inverse image along a smooth 1-morphism, is local for every jointly surjective family of smooth 1-morphisms indexed in Type (max u s), and is preserved by the higher direct images between algebraic stacks representable by affine schemes, then the higher direct images carry the rule into the rule along every quasi-compact (Stacks 050U) quasi-separated (Stacks 04YW) 1-morphism of algebraic stacks, in every degree.

This is AlgebraicGeometry.Stack.smoothLocalHigherDirectImageCriterion_unconditional. Hypothesis (3) is the source's, read for the families indexed in Type (max u s): the source asks it of every jointly surjective family whatever its index set, so its hypothesis implies this one and this statement implies the source's.

alias smoothLocalHigherDirectImageCriterion

AlgebraicGeometry.Stack.smoothLocalHigherDirectImageCriterion_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/SmoothLocalHigherDirectImageCriterionProof.lean, line 85. The attribute's comment: “the whole statement: every rule satisfying the source's four hypotheses, every quasi-compact quasi-separated 1-morphism of algebraic stacks and every degree; hypothesis (3) is read for the families indexed in a universe containing u, which the source's hypothesis implies, so the statement is no weaker than the source's”.

Let M be a rule on the modules on the étale sites of the algebraic stacks over S such that (1) it cuts out a weak Serre subcategory on every algebraic stack, (2) it is preserved by inverse image along every smooth 1-morphism, (3) membership in it is local for every jointly surjective family of smooth 1-morphisms indexed in Type (max u s), and (4) the higher direct images along every 1-morphism between algebraic stacks representable by affine schemes carry it into itself. Then the higher direct images along every quasi-compact quasi-separated 1-morphism of algebraic stacks carry M into M, in every degree.

Hypothesis (3) is the source's, read for the families indexed in Type (max u s): the source asks it of every jointly surjective family whatever its index set, so its hypothesis implies this one and this statement implies the source's (see the module documentation).

theorem smoothLocalHigherDirectImageCriterion_unconditional :
    SmoothLocalHigherDirectImageCriterion.{u, t, max u s} B S hS
Tag 0770, a lemma

Tag 0770 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.higherDirectImage_mem_of_quasiCompact_quasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/HigherDirectImageFppfWeakSerre.lean, line 486. The attribute's comment: “the reduction of the quasi-compact quasi-separated case to the affine case, which is the source's own clause (4), from clauses (1) to (4) together with two hypothesised prerequisites, the base-change isomorphisms of Stacks 075H and the fppf relative Cech pushforward spectral sequence of Stacks 072G part (2)(b)”.

Stacks 0770. Let M be a rule which associates to every algebraic stack 𝒳 over S a subcategory M_𝒳 of Mod(𝒪_𝒳), the modules on the fppf site of 𝒳, such that

  1. M_𝒳 is a weak Serre subcategory of Mod(𝒪_𝒳) for every algebraic stack 𝒳;
  2. for a smooth 1-morphism f : 𝒳 ⟶ 𝒴 the inverse image f^* maps M_𝒴 into M_𝒳;
  3. M is smooth-local on the target; and
  4. for a 1-morphism of stacks representable by affine schemes, Rⁱf_* maps M into M.

Then for every quasi-compact and quasi-separated 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks and every F in M_𝒳, the higher direct image Rⁱf_* F, computed in the fppf topology, lies in M_𝒴.

The proof is the source's: the first move (AlgebraicGeometry.Stack.AlgebraicStacks.higherDirectImagesMapInto_of_smoothAffineCover) transports the question along a smooth presentation of 𝒴 by affine-representable stacks, using clauses (1), (2), (3) and the base-change isomorphisms; the second (AlgebraicGeometry.Stack.AlgebraicStacks.higherDirectImagesMapInto_of_abutsTo) settles each base-changed 1-morphism, whose target is affine-representable and which is again quasi-compact and quasi-separated, from clauses (1), (2), (4) and the Čech spectral sequence.

Two prerequisites beyond the four clauses are hypothesised, hpres and hcech: the base-change isomorphisms of Stacks 075H and the Čech spectral sequence of Stacks 072G part (2).

theorem higherDirectImage_mem_of_quasiCompact_quasiSeparated (M : ModuleRule.{u, w} B S hS)
    (hSerre : ∀ 𝒳 : AlgebraicStacks.{u, w} B S hS, (M 𝒳).IsWeakSerreClass)
    (hSmooth : IsSmoothPullbackStable B S hS M) (hLocal : IsSmoothLocal B S hS M)
    (hAffine : AffineHigherDirectImagesMapInto B S hS M)
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hqc : Stack.IsQuasiCompactMorphism B S hS f)
    (hqs : AlgebraicStacks.IsQuasiSeparated B S hS f)
    (hpres : HasSmoothAffineBaseChange B S hS f)
    (hcech : ∀ {𝒳' 𝒴' : AlgebraicStacks.{u, w} B S hS} (f' : 𝒳' ⟶ 𝒴'),
      Stack.IsQuasiCompactMorphism B S hS f' →
      AlgebraicStacks.IsQuasiSeparated B S hS f' → IsAffineRepresentable B S hS 𝒴' →
      HasFppfCechPresentation B S hS f')
    (i : ℕ) (F : fppfModules B S hS 𝒳) (hF : M 𝒳 F) :
    M 𝒴 ((fppfHigherDirectImage B S hS f i).obj F)

AlgebraicGeometry.Stack.StackModuleRule.preservesHigherDirectImages_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/HigherDirectImageSmoothLocalRule.lean, line 153. The attribute's comment: “the whole statement: every rule satisfying (1)-(4), every quasi-compact quasi-separated 1-morphism of algebraic stacks and every degree, higher direct images in the fppf topology; (1) read as M_X weak Serre (the source's O_X is a typo), (3) asked for families indexed by Type u only”.

Stacks 0770. Let M be a rule which associates to every algebraic stack 𝒳 over S a property M_𝒳 of the sheaves of 𝒪_𝒳-modules on the fppf site of 𝒳 such that

  1. M_𝒳 is a weak Serre subcategory of Mod(𝒪_𝒳) for all algebraic stacks 𝒳;
  2. for a smooth 1-morphism f : 𝒵 ⟶ 𝒳 the inverse image f^* maps M_𝒳 into M_𝒵;
  3. if fᵢ : 𝒳ᵢ ⟶ 𝒳 is a family of smooth 1-morphisms with |𝒳| = ⋃ᵢ |fᵢ|(|𝒳ᵢ|), then a module ℱ lies in M_𝒳 if and only if every fᵢ^*ℱ lies in M_{𝒳ᵢ}; and
  4. if f : 𝒳 ⟶ 𝒴 is a 1-morphism of algebraic stacks and 𝒳 and 𝒴 are representable by affine schemes, then Rⁱf_* maps M_𝒳 into M_𝒴.

Then for every quasi-compact and quasi-separated 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks, Rⁱf_* maps M_𝒳 into M_𝒴 in every degree, the higher direct images being computed in the fppf topology.

Clause (1) is read as "M_𝒳 is a weak Serre subcategory": the source prints "𝒪_𝒳 is a weak Serre subcategory", a typo, as the identical clause (1) of Stacks 076Z shows. Clause (3) is asked only for families indexed by a type in the universe of the schemes, which makes the hypothesis weaker and the theorem stronger. "Representable by an affine scheme" in clause (4) is equivalence over the site with the big site of an affine scheme (AlgebraicGeometry.Stack.AlgebraicStacks.IsAffineRepresentable). Modules have sections in the universe of the schemes, and the higher direct images are the right derived functors of the direct image right adjoint to the inverse image.

theorem preservesHigherDirectImages_fppf (M : StackModuleRule.{u, t} B S hS .fppf)
    (h1 : IsWeakSerre .fppf M) (h2 : IsStableUnderSmoothPullback .fppf M)
    (h3 : IsSmoothLocal.{u, t, u} .fppf M)
    (h4 : PreservesHigherDirectImagesOfAffine (stackModuleDirectImageData.{u, t} B S hS .fppf) M) :
    PreservesHigherDirectImages (stackModuleDirectImageData.{u, t} B S hS .fppf) M
Sources

Section103.6 Locally quasi-coherent modules#

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

Tag 075Y, a lemma

Tag 075Y in the Stacks Project.

AlgebraicGeometry.Stack.isLocallyQuasicoherent_of_isSmooth_jointlySurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LocallyQuasicoherentSmoothDescent.lean, line 154.

Let f j : 𝒵 j ⟶ 𝒳 be a family of smooth 1-morphisms of algebraic stacks over S with |𝒳| = ⋃ j, |f j|(|𝒵 j|), and let F be a sheaf of 𝒪_𝒳-modules on 𝒳_étale. If every inverse image f j^{-1} F is locally quasi-coherent, then so is F.

theorem isLocallyQuasicoherent_of_isSmooth_jointlySurjective
    {J : Type v} {𝒵 : J → AlgebraicStacks.{u, w} B S hS} {𝒳 : AlgebraicStacks.{u, w} B S hS}
    (f : ∀ j, 𝒵 j ⟶ 𝒳)
    (hsmooth : ∀ j, AlgebraicStacks.IsSmooth B S hS (f j))
    (hjs : (Set.univ : Set (AlgebraicStacks.points B S hS 𝒳)) =
      ⋃ j, Set.range (AlgebraicStacks.pointsMap B S hS (f j)))
    (F : PresheafOfModules.{u} (ringStructureSheafCore B S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids (etaleTopology B) (etaleTopology_le_topology B)).obj)
    (hF : Presheaf.IsSheaf (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B)) F.presheaf)
    (hlqc : ∀ j, IsLocallyQuasicoherent B E h S hS
      (CatFiberedInGroupoids.homFunctor (f j).hom ⋙ 𝒳.val.val.p)
      (isFiberedInGroupoids_homFunctor_comp B S hS (f j).hom)
      ((stackModulePresheafPullback.{u, w, u} B S hS (f j)).obj F)) :
    IsLocallyQuasicoherent B E h S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids F
Tag 075Z, a lemma

Tag 075Z in the Stacks Project.

AlgebraicGeometry.Stack.isLocallyQuasicoherent_moduleSheafHigherDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/HigherDirectImageSmoothLocalCriterion.lean, line 537. The attribute's comment: “the whole statement, in every degree and with the source's hypotheses unweakened, granted four named hypotheses: the criterion of Stacks 076Z quantified over every rule, the weak Serre condition of Stacks 06WM parts (1)-(3), the converse half of the smooth-local criterion Stacks 075Y at section universe u+1, and the affine case (Stacks 075P and Stacks 0720). Hypothesis (2) of the criterion, Stacks 06WL, is proved rather than assumed”.

Stacks 075Z. Let f : 𝒳 ⟶ 𝒴 be a quasi-compact (Stacks 050U) and quasi-separated (Stacks 04YW) 1-morphism of algebraic stacks over S and let ℱ be a locally quasi-coherent 𝒪_𝒳-module on 𝒳_étale (Stacks 06WJ). Then the higher direct image Rⁱf_*ℱ, computed in the étale topology, is locally quasi-coherent on 𝒴_étale, in every degree i.

The conclusion is AlgebraicGeometry.Stack.IsLocallyQuasicoherentHigherDirectImage, the library's statement of the assertion of the source, unchanged and for every degree.

Three hypotheses are carried, each a clause of the criterion of Stacks 076Z at the rule of local quasi-coherence and each one a result of the source this library does not have:

  • hcrit is Stacks 076Z, quantified over every rule. Its proof runs the first-quadrant spectral sequence of Stacks 072G, which is not formalized here.
  • hserre is hypothesis (1), the weak Serre condition, which is parts (1) to (3) of Stacks 06WM, proved at section universe u in StacksFrontier.AlgebraicGeometry.Stacks.Quasicoherent.LocallyQuasicoherentClosure; here it is read at section universe u + 1.
  • hconv is the converse half of hypothesis (3), which is Stacks 075Y. That tag is proved, at section universe u only, and the higher direct images produce modules with sections in u + 1; closing this gap is a universe generalization of Stacks 03DN, not a new theorem of the source.
  • haffine is hypothesis (4), the case of stacks representable by affine schemes, which the source proves from Stacks 075P and Stacks 0720; the cohomological content of Stacks 075P and all of Stacks 0720 are absent.

Hypothesis (2) is not carried: it is Stacks 06WL and is supplied by AlgebraicGeometry.Stack.isStableUnderSmoothPullback_locallyQuasicoherentRule, which also supplies the forward half of hypothesis (3).

theorem isLocallyQuasicoherent_moduleSheafHigherDirectImage
    (hcrit : SmoothLocalHigherDirectImageCriterion.{u, t, s} B S hS)
    (hserre : StackEtaleModuleRule.IsWeakSerre.{u, t} B S hS (locallyQuasicoherentRule B E h S hS))
    (hconv : StackEtaleModuleRule.IsSmoothLocalConverse.{u, t, s} B S hS
      (locallyQuasicoherentRule B E h S hS))
    (haffine : StackEtaleModuleRule.PreservesHigherDirectImagesOfAffine.{u, t} B S hS
      (locallyQuasicoherentRule B E h S hS))
    {𝒳 𝒴 : AlgebraicStacks.{u, t} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hqc : IsQuasiCompactMorphism B S hS f)
    (hqs : AlgebraicStacks.IsQuasiSeparated B S hS f) (i : ℕ) :
    IsLocallyQuasicoherentHigherDirectImage B E h S hS f i

AlgebraicGeometry.Stack.isLocallyQuasicoherent_stackModuleHigherDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LocallyQuasicoherentHigherDirectImage.lean, line 124. The attribute's comment: “the whole statement, with modules and higher direct images at the module universe u of the schemes; local quasi-coherence read against an auxiliary big étale site E with E.cutoff = B.cutoff”.

Let f : 𝒳 ⟶ 𝒴 be a quasi-compact and quasi-separated 1-morphism of algebraic stacks and ℱ a locally quasi-coherent 𝒪_𝒳-module on 𝒳_étale. Then every higher direct image Rⁱf_*ℱ, computed in the étale topology, is locally quasi-coherent on 𝒴_étale.

Modules have sections in the universe u of the schemes, and Rⁱf_* is the right derived functor of the direct image right adjoint to the inverse image (AlgebraicGeometry.Stack.stackModuleHigherDirectImage). Local quasi-coherence is stated against an auxiliary big étale site E with the cutoff of B.

theorem isLocallyQuasicoherent_stackModuleHigherDirectImage
    {𝒳 𝒴 : AlgebraicStacks.{u, t} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hqc : IsQuasiCompactMorphism B S hS f) (hqs : AlgebraicStacks.IsQuasiSeparated B S hS f)
    (F : StackModules B S hS .etale 𝒳)
    (hF : IsLocallyQuasicoherent B E h S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids F.val)
    (i : ℕ) :
    IsLocallyQuasicoherent B E h S hS 𝒴.val.val.p 𝒴.val.isFiberedInGroupoids
      ((stackModuleHigherDirectImage B S hS f .etale i).obj F).val
Tag 07AP, a lemma

Tag 07AP in the Stacks Project.

AlgebraicGeometry.Stack.exists_fppfCovering_isQuasicoherentOnSite_restrictModuleToSmallEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LocallyQuasicoherentFlatDescent.lean, line 156. The attribute's comment: “the fppf-local half: every object acquires a jointly surjective family of flat, locally finitely presented arrows at whose sources the small étale restriction of the module is quasi-coherent, via the fppf-local factorisation of Stacks 07AN”.

Stacks 07AP, its fppf-local half. Let f j : 𝒵 j ⟶ 𝒳 be a family of flat, locally finitely presented 1-morphisms of algebraic stacks over S with |𝒳| = ⋃ j, |f j|(|𝒵 j|), let F be a sheaf of 𝒪_𝒳-modules on 𝒳_étale and suppose every inverse image f j^{-1} F is locally quasi-coherent. Then every object x of 𝒳 admits a family of arrows φ i : y i ⟶ x lying over flat, locally finitely presented and jointly surjective morphisms of schemes, at every member of which the restriction of F to the small étale site is quasi-coherent.

theorem exists_fppfCovering_isQuasicoherentOnSite_restrictModuleToSmallEtale {J : Type v}
    {𝒵 : J → AlgebraicStacks.{u, w} B S hS} {𝒳 : AlgebraicStacks.{u, w} B S hS}
    (f : ∀ j, 𝒵 j ⟶ 𝒳)
    (hflat : ∀ j, AlgebraicStacks.IsFlat B S hS (f j))
    (hlfp : ∀ j, AlgebraicStacks.IsLocallyOfFinitePresentation B S hS (f j))
    (hjs : (Set.univ : Set (AlgebraicStacks.points B S hS 𝒳)) =
      ⋃ j, Set.range (AlgebraicStacks.pointsMap B S hS (f j)))
    (F : PresheafOfModules.{m} (ringStructureSheafCore B S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids (etaleTopology B) (etaleTopology_le_topology B)).obj)
    (hF : Presheaf.IsSheaf (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B)) F.presheaf)
    (hlqc : ∀ j, IsLocallyQuasicoherent B E h S hS
      (CatFiberedInGroupoids.homFunctor (f j).hom ⋙ 𝒳.val.val.p)
      (isFiberedInGroupoids_homFunctor_comp B S hS (f j).hom)
      ((stackModulePresheafPullback.{u, w, m} B S hS (f j)).obj F))
    (x : 𝒳.val.val.obj) :
    ∃ (I : Type (u + 1)) (y : I → 𝒳.val.val.obj) (φ : ∀ i, y i ⟶ x),
      (∀ i, Flat (B.inclusion.map (𝒳.val.val.p.map (φ i)).left)) ∧
        (∀ i, LocallyOfFinitePresentation (B.inclusion.map (𝒳.val.val.p.map (φ i)).left)) ∧
          (∀ t : B.inclusion.obj (𝒳.val.val.p.obj x).left,
            ∃ i, t ∈ Set.range (B.inclusion.map (𝒳.val.val.p.map (φ i)).left)) ∧
            ∀ i, (⟨restrictModuleToSmallEtale B E h S hS 𝒳.val.val.p
                  𝒳.val.isFiberedInGroupoids (y i) (etaleTopology B)
                  (etaleTopology_le_topology B) F,
                restrictModuleToSmallEtale_isSheaf B E h S hS 𝒳.val.val.p
                  𝒳.val.isFiberedInGroupoids (y i) F hF⟩ :
              SheafOfModules.{m} (SmallEtale.structureSheaf E
                (𝒳.val.val.p.obj (y i)).left.1
                (contains_base B E h S hS 𝒳.val.val.p (y i)))).IsQuasicoherentOnSite

AlgebraicGeometry.Stack.isLocallyQuasicoherent_of_isFlat_isLfp_jointlySurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LocallyQuasicoherentFppfDescent.lean, line 385.

Stacks 07AP. Let f j : 𝒵 j ⟶ 𝒳 be a family of flat (Stacks 06PW) and locally finitely presented (Stacks 06Q2) 1-morphisms of algebraic stacks over S with |𝒳| = ⋃ j, |f j|(|𝒵 j|) (Stacks 04XG), and let F be a sheaf of 𝒪_𝒳-modules on 𝒳_fppf. If every inverse image f j^{-1} F is locally quasi-coherent (Stacks 06WJ), then so is F.

The étale sheaf condition follows from the fppf one. At an object x lying over U, the restriction x^*F|_{U_étale} is quasi-coherent because it is cartesian between affine objects (Descent, Proposition 03DX), which through the index functor of Stacks 06W1 is the cartesian condition for F along arrows lying over étale morphisms of affine schemes, proved by AlgebraicGeometry.Stack.isIso_restrictionBaseChange_of_isFlat_isLfp_jointlySurjective.

theorem isLocallyQuasicoherent_of_isFlat_isLfp_jointlySurjective {J : Type v}
    {𝒵 : J → AlgebraicStacks.{u, w} B S hS} {𝒳 : AlgebraicStacks.{u, w} B S hS}
    (f : ∀ j, 𝒵 j ⟶ 𝒳)
    (hflat : ∀ j, AlgebraicStacks.IsFlat B S hS (f j))
    (hlfp : ∀ j, AlgebraicStacks.IsLocallyOfFinitePresentation B S hS (f j))
    (hjs : (Set.univ : Set (AlgebraicStacks.points B S hS 𝒳)) =
      ⋃ j, Set.range (AlgebraicStacks.pointsMap B S hS (f j)))
    (F : PresheafOfModules.{u} (ringStructureSheafCore B S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids (etaleTopology B) (etaleTopology_le_topology B)).obj)
    (hF : Presheaf.IsSheaf (associatedTopology B S hS 𝒳.val.val.p B.topology) F.presheaf)
    (hlqc : ∀ j, IsLocallyQuasicoherent B E h S hS
      (CatFiberedInGroupoids.homFunctor (f j).hom ⋙ 𝒳.val.val.p)
      (isFiberedInGroupoids_homFunctor_comp B S hS (f j).hom)
      ((stackModulePresheafPullback.{u, w, u} B S hS (f j)).obj F)) :
    IsLocallyQuasicoherent B E h S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids F
Sources

Section103.7 Flat comparison maps#

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

Tag 0761, an equation

Tag 0761 in the Stacks Project.

Declarations registered for the tag:

Tag 0762, a definition

Tag 0762 in the Stacks Project.

AlgebraicGeometry.Stack.HasFlatBaseChangeProperty, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatBaseChangeProperty.lean, line 71.

Stacks 0762. A presheaf of modules over the structure sheaf of a category fibred in groupoids has the flat base change property when the comparison map c_φ of Stacks 0761 is an isomorphism for every arrow φ of 𝒳 lying over a flat morphism of schemes.

The source calls the name nonstandard.

noncomputable abbrev HasFlatBaseChangeProperty {𝒳 : Type v} [Category.{w} 𝒳]
    (p : 𝒳 ⥤ BigFppfOver B S hS) (hp : p.IsFiberedInGroupoids)
    (τ : GrothendieckTopology B.Schemes) (hτ : τ ≤ B.topology)
    (F : PresheafOfModules.{u} (ringStructureSheafCore B S hS p hp τ hτ).obj) : Prop
Tag 0764, a lemma

Tag 0764 in the Stacks Project.

AlgebraicGeometry.Stack.hasFlatBaseChangeProperty_colimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatBaseChangeColimits.lean, line 220. The attribute's comment: “part (4), with the ambient category the presheaves of modules rather than the étale sheaves of modules: a colimit of presheaves of modules with the flat base change property has the flat base change property”.

Stacks 0764, part (4), for presheaves of modules. The colimit of a diagram of presheaves of 𝒪_𝒳-modules each having the flat base change property of Stacks 0762 again has the flat base change property, and the colimit is the colimit of presheaves of modules.

For an arrow φ of 𝒳 lying over a flat morphism of schemes, the comparison map c_φ is the component of a natural transformation from F ↦ a_{small}^*(F|_{V_ét}) to F ↦ F|_{U_ét}. Both functors preserve colimits — the first because a_{small}^* is a left adjoint, the second because restriction to the small étale site is restriction along a functor followed by a change of scalars — and the component at a colimit of a natural transformation of colimit-preserving functors is an isomorphism as soon as every component on the diagram is.

theorem hasFlatBaseChangeProperty_colimit
    (K : J ⥤ PresheafOfModules.{u} (ringStructureSheafCore B S hS p hp τ hτ).obj)
    (hK : ∀ i, HasFlatBaseChangeProperty B E h S hS p hp τ hτ (K.obj i)) :
    HasFlatBaseChangeProperty B E h S hS p hp τ hτ (colimit K)

AlgebraicGeometry.Stack.hasFlatBaseChangeProperty_of_isColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatBaseChangeColimits.lean, line 237. The attribute's comment: “part (4), with the ambient category the presheaves of modules rather than the étale sheaves of modules: the vertex of a colimit cocone on a diagram of presheaves of modules with the flat base change property has the flat base change property”.

Stacks 0764, part (4), for presheaves of modules, in the form for an arbitrary colimit cocone: the vertex of a colimit cocone on a diagram of presheaves of 𝒪_𝒳-modules with the flat base change property has the flat base change property.

This is AlgebraicGeometry.Stack.hasFlatBaseChangeProperty_colimit transported along the canonical isomorphism of the vertex with the chosen colimit.

theorem hasFlatBaseChangeProperty_of_isColimit
    {K : J ⥤ PresheafOfModules.{u} (ringStructureSheafCore B S hS p hp τ hτ).obj}
    {c : Cocone K} (hc : IsColimit c)
    (hK : ∀ i, HasFlatBaseChangeProperty B E h S hS p hp τ hτ (K.obj i)) :
    HasFlatBaseChangeProperty B E h S hS p hp τ hτ c.pt

AlgebraicGeometry.Stack.isClosedUnderColimitsOfShape_flatBaseChangeModulePresheaves, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatBaseChangeColimits.lean, line 279. The attribute's comment: “part (4), with the ambient category the presheaves of modules rather than the étale sheaves of modules: the modules with the flat base change property have colimits”.

The presheaves of modules with the flat base change property are closed under colimits of shape J, by AlgebraicGeometry.Stack.hasFlatBaseChangeProperty_of_isColimit.

This is Stacks 0764, part (4), for presheaves of modules: through Mathlib's instances CategoryTheory.Limits.hasColimitsOfShape_of_closedUnderColimits and CategoryTheory.preservesColimitOfShape_of_createsColimitsOfShape_and_hasColimitsOfShape, the subcategory has colimits of shape J and its inclusion preserves them.

instance isClosedUnderColimitsOfShape_flatBaseChangeModulePresheaves :
    ObjectProperty.IsClosedUnderColimitsOfShape
      (flatBaseChangeModulePresheaves.{u, v, w} B E h S hS p hp τ hτ) J

AlgebraicGeometry.Stack.isClosedUnderColimitsOfShape_flatBaseChangeModulePresheaves, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatBaseChangeColimits.lean, line 279. The attribute's comment: “part (4), with the ambient category the presheaves of modules rather than the étale sheaves of modules: those colimits agree with the colimits of all modules”.

The presheaves of modules with the flat base change property are closed under colimits of shape J, by AlgebraicGeometry.Stack.hasFlatBaseChangeProperty_of_isColimit.

This is Stacks 0764, part (4), for presheaves of modules: through Mathlib's instances CategoryTheory.Limits.hasColimitsOfShape_of_closedUnderColimits and CategoryTheory.preservesColimitOfShape_of_createsColimitsOfShape_and_hasColimitsOfShape, the subcategory has colimits of shape J and its inclusion preserves them.

instance isClosedUnderColimitsOfShape_flatBaseChangeModulePresheaves :
    ObjectProperty.IsClosedUnderColimitsOfShape
      (flatBaseChangeModulePresheaves.{u, v, w} B E h S hS p hp τ hτ) J

AlgebraicGeometry.Stack.hasFlatBaseChangeProperty_cokernel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatBaseChangeColimits.lean, line 298. The attribute's comment: “part (2), with the ambient category the presheaves of modules rather than the étale sheaves of modules: the closure under cokernels asked for by Stacks 0754”.

Stacks 0764, part (2), for presheaves of modules. The cokernel of a morphism of presheaves of 𝒪_𝒳-modules with the flat base change property of Stacks 0762 has the flat base change property. This is the closure under cokernels asked for by Stacks 0754.

A cokernel is a colimit indexed by the walking parallel pair, whose two values are the source and the target of the morphism, so this is a case of AlgebraicGeometry.Stack.hasFlatBaseChangeProperty_colimit.

theorem hasFlatBaseChangeProperty_cokernel
    {F G : PresheafOfModules.{u} (ringStructureSheafCore B S hS p hp τ hτ).obj} (α : F ⟶ G)
    (hF : HasFlatBaseChangeProperty B E h S hS p hp τ hτ F)
    (hG : HasFlatBaseChangeProperty B E h S hS p hp τ hτ G) :
    HasFlatBaseChangeProperty B E h S hS p hp τ hτ (cokernel α)

AlgebraicGeometry.Stack.hasFlatBaseChangeProperty_initial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatBaseChangeColimits.lean, line 317. The attribute's comment: “part (2), with the ambient category the presheaves of modules rather than the étale sheaves of modules: the zero object asked for by Stacks 0754”.

Stacks 0764, part (2), for presheaves of modules. An initial presheaf of 𝒪_𝒳-modules — equivalently, a zero object — has the flat base change property of Stacks 0762. This is the containment of a zero object asked for by Stacks 0754.

An initial object is the colimit of the empty diagram, so this is the case of AlgebraicGeometry.Stack.hasFlatBaseChangeProperty_of_isColimit in which the hypothesis on the diagram is vacuous.

theorem hasFlatBaseChangeProperty_initial
    {F : PresheafOfModules.{u} (ringStructureSheafCore B S hS p hp τ hτ).obj}
    (hF : IsInitial F) :
    HasFlatBaseChangeProperty B E h S hS p hp τ hτ F

AlgebraicGeometry.Stack.hasFlatBaseChangePropertySheaf_colimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatBaseChangeSheafColimits.lean, line 332. The attribute's comment: “part (4), with the ambient category the étale sheaves of modules, as the source states it -- and so with a_small^* the inverse image of sheaves of modules, not the inverse image of presheaves of modules used by the part (4) registrations of FlatBaseChangeColimits: a colimit of étale sheaves of modules with the flat base change property has the flat base change property”.

Stacks 0764, part (4), as the source states it. The colimit of a diagram of étale sheaves of 𝒪_𝒳-modules each having the flat base change property of Stacks 0762 again has the flat base change property, the colimit being the colimit of Mod(𝒳_étale, 𝒪_𝒳).

For an arrow φ of 𝒳 lying over a flat morphism of schemes, c_φ^{sh} is the component of a natural transformation from F ↦ a_{small}^*(F|_{V_ét}) to F ↦ F|_{U_ét}. Both functors preserve colimits — the first because the inverse image of sheaves of modules is a left adjoint, by AlgebraicGeometry.Stack.sheafifiedPullbackComparisonAdjunction, the second by AlgebraicGeometry.Stack.preservesColimitsOfShape_restrictSheafToSmallEtale — and the component at a colimit of a natural transformation of colimit-preserving functors is an isomorphism as soon as every component on the diagram is.

theorem hasFlatBaseChangePropertySheaf_colimit
    (K : J ⥤ SheafOfModules.{m} (ringStructureSheafCore B S hS p hp (etaleTopology B)
      (etaleTopology_le_topology B))) [HasColimit K]
    (hK : ∀ i, HasFlatBaseChangePropertySheafUnivLE B E h S hS p hp (K.obj i)) :
    HasFlatBaseChangePropertySheafUnivLE B E h S hS p hp (colimit K)

AlgebraicGeometry.Stack.hasFlatBaseChangePropertySheaf_of_isColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatBaseChangeSheafColimits.lean, line 378. The attribute's comment: “part (4), with the ambient category the étale sheaves of modules, as the source states it -- and so with a_small^* the inverse image of sheaves of modules, not the inverse image of presheaves of modules used by the part (4) registrations of FlatBaseChangeColimits: the vertex of a colimit cocone on a diagram of étale sheaves of modules with the flat base change property has the flat base change property”.

Stacks 0764, part (4), as the source states it, in the form for an arbitrary colimit cocone: the vertex of a colimit cocone on a diagram of étale sheaves of 𝒪_𝒳-modules with the flat base change property has the flat base change property.

This is AlgebraicGeometry.Stack.hasFlatBaseChangePropertySheaf_colimit transported along the canonical isomorphism of the vertex with the chosen colimit.

theorem hasFlatBaseChangePropertySheaf_of_isColimit
    {K : J ⥤ SheafOfModules.{m} (ringStructureSheafCore B S hS p hp (etaleTopology B)
      (etaleTopology_le_topology B))} {c : Cocone K} (hc : IsColimit c)
    (hK : ∀ i, HasFlatBaseChangePropertySheafUnivLE B E h S hS p hp (K.obj i)) :
    HasFlatBaseChangePropertySheafUnivLE B E h S hS p hp c.pt

AlgebraicGeometry.Stack.hasColimitsOfShape_flatBaseChangeEtaleModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatBaseChangeSheafColimits.lean, line 592. The attribute's comment: “part (4), in the source's ambient category Mod(X_etale, O_X): the full subcategory of etale sheaves of modules with the flat base change property has colimits”.

Stacks 0764, part (4), as the source states it: the category of étale sheaves of 𝒪_𝒳-modules with the flat base change property has the colimits that Mod(𝒳_étale, 𝒪_𝒳) has; those colimits exist, the étale sheafification of abelian presheaves on 𝒳 being available unconditionally.

theorem hasColimitsOfShape_flatBaseChangeEtaleModules :
    HasColimitsOfShape J (flatBaseChangeEtaleModules.{u, v, w} B E h S hS p hp).FullSubcategory

AlgebraicGeometry.Stack.preservesColimitsOfShape_flatBaseChangeEtaleModules_ι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatBaseChangeSheafColimits.lean, line 608. The attribute's comment: “part (4), in the source's ambient category Mod(X_etale, O_X): the colimits of the subcategory agree with the colimits in Mod(X_etale, O_X)”.

Stacks 0764, part (4), as the source states it: the colimits of étale sheaves of 𝒪_𝒳-modules with the flat base change property agree with the colimits of Mod(𝒳_étale, 𝒪_𝒳), the inclusion preserving them.

theorem preservesColimitsOfShape_flatBaseChangeEtaleModules_ι :
    PreservesColimitsOfShape J (flatBaseChangeEtaleModules.{u, v, w} B E h S hS p hp).ι

AlgebraicGeometry.Stack.hasFlatBaseChangePropertySheaf_etaleInternalHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatBaseChangeSheafInternalHom.lean, line 153. The attribute's comment: “part (6): for F, G in Mod(𝒳_étale, 𝒪_𝒳) with F of finite presentation and G with the flat base change property, the internal Hom 𝓗om_{𝒪_𝒳}(F, G) of Mod(𝒳_étale, 𝒪_𝒳) has the flat base change property”.

Stacks 0764, part (6). Let p : 𝒳 ⥤ (Sch/S)_{fppf} be a category fibred in groupoids and let F, G be étale sheaves of 𝒪_𝒳-modules, with F of finite presentation on 𝒳_étale (Stacks 03DL) and G with the flat base change property of Stacks 0762. Then the internal Hom 𝓗om_{𝒪_𝒳}(F, G) of Mod(𝒳_étale, 𝒪_𝒳) has the flat base change property.

Let φ : x ⟶ y lie over a flat morphism, and let {e_j : y_j ⟶ y} be an étale covering on whose members F has a finite presentation. At every arrow into some y_j lying over a flat morphism the comparison map of 𝓗om(F, G) is invertible by the presented case proved above, and that suffices for c_φ by the étale-local criterion AlgebraicGeometry.Stack.isIso_restrictSheafPullbackComparison_of_etaleCover.

theorem hasFlatBaseChangePropertySheaf_etaleInternalHom
    (F G : SheafOfModules.{u}
      (ringStructureSheafCore B S hS p hp (etaleTopology B) (etaleTopology_le_topology B)))
    (hfp : F.IsFinitePresentationOnSite)
    (hG : HasFlatBaseChangePropertySheafUnivLE B E h S hS p hp G) :
    HasFlatBaseChangePropertySheafUnivLE B E h S hS p hp (etaleInternalHom B S hS p hp F G)

AlgebraicGeometry.Stack.hasFlatBaseChangePropertySheaf_modulePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatBaseChangeSheafInverseImage.lean, line 267. The attribute's comment: “part (1), the whole part, in the source's ambient category of étale sheaves of modules (a_small^ the inverse image of sheaves of modules), for any 1-morphism f : 𝒳 ⥤ 𝒴 of categories fibred in groupoids over (Sch/S)_fppf, in particular any morphism of algebraic stacks: the inverse image f^F of a module F with the flat base change property has the flat base change property”.

Stacks 0764, part (1), in the source's ambient category. Let f : 𝒳 ⥤ 𝒴 be a 1-morphism of categories fibred in groupoids over the big fppf category of S, and let F be an étale sheaf of 𝒪_𝒴-modules with the flat base change property of Stacks 0762 (comparison maps taken with the inverse image of sheaves of modules on the small étale sites). Then the inverse image f^*F of sheaves of modules has the flat base change property.

An arrow φ of 𝒳 lies over the same morphism of schemes as f φ, so this is AlgebraicGeometry.Stack.isIso_restrictSheafPullbackComparison_modulePullback_iff at each arrow lying over a flat morphism.

theorem hasFlatBaseChangePropertySheaf_modulePullback
    (F : SheafOfModules.{m} (ringStructureSheafCore B S hS q hq (etaleTopology B)
      (etaleTopology_le_topology B)))
    (hF : HasFlatBaseChangePropertySheafUnivLE B E h S hS q hq F) :
    HasFlatBaseChangePropertySheafUnivLE B E h S hS p hp
      ((modulePullback B S hS p q hp hq f hf (etaleTopology B)
        (etaleTopology_le_topology B)).obj F)

AlgebraicGeometry.Stack.hasFlatBaseChangePropertySheaf_of_isSmooth_jointlySurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatBaseChangeSheafSmoothLocal.lean, line 120. The attribute's comment: “part (3), the whole part, in the source's ambient category of étale sheaves of modules (a_small^ the inverse image of sheaves of modules): for a family of smooth 1-morphisms f j : 𝒵 j ⟶ 𝒳 of algebraic stacks with |𝒳| = ⋃ j, |f j|(|𝒵 j|), if each inverse image f j^ F has the flat base change property then so does F”.

Stacks 0764, part (3), in the source's ambient category. Let f j : 𝒵 j ⟶ 𝒳 be a family of smooth 1-morphisms of algebraic stacks over S with |𝒳| = ⋃ j, |f j|(|𝒵 j|), and let F be an étale sheaf of 𝒪_𝒳-modules. If every inverse image f j^* F of sheaves of modules has the flat base change property of Stacks 0762, then so does F.

AlgebraicGeometry.Stack.exists_etaleCovering_family_fibre_lift covers the scheme below any object of 𝒳 by étale morphisms over which the object lifts through some f j, and AlgebraicGeometry.Stack.hasFlatBaseChangePropertySheaf_of_etaleLocal concludes.

theorem hasFlatBaseChangePropertySheaf_of_isSmooth_jointlySurjective [UnivLE.{u, m}]
    {J : Type v} {𝒵 : J → AlgebraicStacks.{u, w} B S hS} {𝒳 : AlgebraicStacks.{u, w} B S hS}
    (f : ∀ j, 𝒵 j ⟶ 𝒳)
    (hsmooth : ∀ j, AlgebraicStacks.IsSmooth B S hS (f j))
    (hjs : (Set.univ : Set (AlgebraicStacks.points B S hS 𝒳)) =
      ⋃ j, Set.range (AlgebraicStacks.pointsMap B S hS (f j)))
    (F : SheafOfModules.{m} (ringStructureSheafCore B S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids (etaleTopology B) (etaleTopology_le_topology B)))
    (hF : ∀ j, HasFlatBaseChangePropertySheafUnivLE B E h S hS
      (CatFiberedInGroupoids.homFunctor (f j).hom ⋙ 𝒳.val.val.p)
      (isFiberedInGroupoids_homFunctor_comp B S hS (f j).hom)
      ((modulePullback B S hS (CatFiberedInGroupoids.homFunctor (f j).hom ⋙ 𝒳.val.val.p)
        𝒳.val.val.p (isFiberedInGroupoids_homFunctor_comp B S hS (f j).hom)
        𝒳.val.isFiberedInGroupoids (CatFiberedInGroupoids.homFunctor (f j).hom) rfl
        (etaleTopology B) (etaleTopology_le_topology B)).obj F)) :
    HasFlatBaseChangePropertySheafUnivLE B E h S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids F

AlgebraicGeometry.Stack.hasFlatBaseChangePropertySheaf_tensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatBaseChangeSheafTensor.lean, line 816. The attribute's comment: “part (5), with the ambient category the étale sheaves of modules, as the source states it -- and so with a_small^* the inverse image of sheaves of modules: the tensor product in Mod(𝒳_étale, 𝒪_𝒳) of two modules with the flat base change property has the flat base change property”.

Stacks 0764, part (5). The tensor product, in Mod(𝒳_étale, 𝒪_𝒳), of two étale sheaves of 𝒪_𝒳-modules with the flat base change property of Stacks 0762 has the flat base change property.

The tensor product is the canonical one, Stacks.SheafOfModules.Tensor.sheafTensor at the structure sheaf of the associated étale site; it is AlgebraicGeometry.Stack.etaleTensorSheaf by AlgebraicGeometry.Stack.etaleTensorSheaf_eq. The sheafification instances it is formed with hold for every 𝒳, by AlgebraicGeometry.Stack.hasSheafify_etaleAssociatedTopology and AlgebraicGeometry.Stack.wEqualsLocallyBijective_etaleAssociatedTopology, and are supplied here.

At an arrow over a flat morphism of schemes this is AlgebraicGeometry.Stack.isIso_restrictSheafPullbackComparison_etaleTensorSheaf: the restrictions commute with tensor products, the pullback commutes with tensor products by Stacks 03EL, and under these identifications the comparison map of the tensor product is the tensor product of the comparison maps.

theorem hasFlatBaseChangePropertySheaf_tensor
    (F G : SheafOfModules.{u}
      (ringStructureSheafCore B S hS p hp (etaleTopology B) (etaleTopology_le_topology B)))
    (hF : HasFlatBaseChangePropertySheafUnivLE B E h S hS p hp F)
    (hG : HasFlatBaseChangePropertySheafUnivLE B E h S hS p hp G) :
    letI := hasSheafify_etaleAssociatedTopology B S hS p hp
    letI := wEqualsLocallyBijective_etaleAssociatedTopology B S hS p hp
    HasFlatBaseChangePropertySheafUnivLE B E h S hS p hp
      (((Stacks.SheafOfModules.Tensor.sheafTensor.{_, _, _, u, u}
        (structureSheaf B S hS p hp (etaleTopology B)
          (etaleTopology_le_topology B))).obj F).obj G)

AlgebraicGeometry.Stack.isWeakSerreClass_flatBaseChangeEtaleModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatBaseChangeSheafWeakSerre.lean, line 215. The attribute's comment: “part (2): the étale sheaves of O_X-modules with the flat base change property form a weak Serre subcategory of Mod(X_etale, O_X), in the form of Stacks 0754 -- strictly full, with a zero object, and closed under kernels, cokernels and extensions. The whole of part (2), in the source's ambient category, with a_small^* the inverse image of sheaves of modules, and with no hypothesis beyond the source's”.

Stacks 0764, part (2), as the source states it. The étale sheaves of 𝒪_𝒳-modules with the flat base change property of Stacks 0762 form a weak Serre subcategory of Mod(𝒳_étale, 𝒪_𝒳), in the form Stacks 0754 gives: a strictly full subcategory containing a zero object and closed under kernels, cokernels and extensions.

Strict fullness is AlgebraicGeometry.Stack.isClosedUnderIsomorphisms_flatBaseChangeEtaleModules, the zero object is AlgebraicGeometry.Stack.hasFlatBaseChangePropertySheaf_initial, the cokernels are AlgebraicGeometry.Stack.hasFlatBaseChangePropertySheaf_cokernel, the extensions are AlgebraicGeometry.Stack.hasFlatBaseChangePropertySheaf_of_shortExact, and the kernels are AlgebraicGeometry.Stack.hasFlatBaseChangePropertySheaf_kernel, the last with the left exactness AlgebraicGeometry.Stack.preservesFiniteLimits_sheafifiedPullbackComparison: this is AlgebraicGeometry.Stack.isWeakSerreClass_flatBaseChangeEtaleModules_of_preservesFiniteLimits at section universe u.

The abelian structure on Mod(𝒳_étale, 𝒪_𝒳) is the one coming from étale sheafification of abelian presheaves on 𝒳, whose two instances are supplied in the statement by AlgebraicGeometry.Stack.hasSheafify_etaleAssociatedTopology and AlgebraicGeometry.Stack.wEqualsLocallyBijective_etaleAssociatedTopology; they are not hypotheses.

theorem isWeakSerreClass_flatBaseChangeEtaleModules :
    letI := hasSheafify_etaleAssociatedTopology B S hS p hp
    letI := wEqualsLocallyBijective_etaleAssociatedTopology B S hS p hp
    letI : Abelian (SheafOfModules.{u} (ringStructureSheafCore B S hS p hp (etaleTopology B)
      (etaleTopology_le_topology B))) :=
      SheafOfModules.instAbelian (ringStructureSheafCore B S hS p hp (etaleTopology B)
        (etaleTopology_le_topology B))
    (flatBaseChangeEtaleModules.{u, v, w} B E h S hS p hp).IsWeakSerreClass
Tag 0765, a lemma

Tag 0765 in the Stacks Project.

AlgebraicGeometry.Stack.hasFlatBaseChangePropertySheaf_moduleSheafHigherDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/HigherDirectImageFlatBaseChangeSheaf.lean, line 168. The attribute's comment: “R^i f_* of a locally quasi-coherent étale module with the flat base change property has the flat base change property, for f quasi-compact and quasi-separated”.

Let f : 𝒳 ⟶ 𝒴 be a quasi-compact (Stacks 050U) and quasi-separated (Stacks 04YW) 1-morphism of algebraic stacks, and let ℱ be an étale sheaf of 𝒪_𝒳-modules which is locally quasi-coherent (Stacks 06WJ) and has the flat base change property (Stacks 0762). Then every higher direct image Rⁱf_*ℱ, computed in the étale topology, has the flat base change property.

The flat base change property is the source's, read on sheaves (AlgebraicGeometry.Stack.HasFlatBaseChangePropertySheafUnivLE); the sheaves of modules have their sections in Type (u + 1), where the higher direct images of Stacks 06WE live, and the source 𝒳 is presented strictly, its structure functor written as the functor of f followed by that of 𝒴.

theorem hasFlatBaseChangePropertySheaf_moduleSheafHigherDirectImage
    {𝒳 𝒴 : AlgebraicStacks.{u, t} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hqc : IsQuasiCompactMorphism B S hS f) (hqs : AlgebraicStacks.IsQuasiSeparated B S hS f)
    (F : SheafOfModules.{u + 1} (ringStructureSheafCore B S hS
      (CatFiberedInGroupoids.homFunctor f.hom ⋙ 𝒴.val.val.p)
      (isFiberedInGroupoids_homFunctor_comp B S hS f.hom) (etaleTopology B)
      (etaleTopology_le_topology B)))
    (hlqc : IsLocallyQuasicoherent B E h S hS
      (CatFiberedInGroupoids.homFunctor f.hom ⋙ 𝒴.val.val.p)
      (isFiberedInGroupoids_homFunctor_comp B S hS f.hom) F.val)
    (hfbc : HasFlatBaseChangePropertySheafUnivLE.{u, u + 1, u, u + 1} B E h S hS
      (CatFiberedInGroupoids.homFunctor f.hom ⋙ 𝒴.val.val.p)
      (isFiberedInGroupoids_homFunctor_comp B S hS f.hom) F)
    (i : ℕ) :
    letI := hasSheafify_associatedTopology_of_category_succ B S hS
      (CatFiberedInGroupoids.homFunctor f.hom ⋙ 𝒴.val.val.p)
    letI := wEqualsLocallyBijective_associatedTopology_of_category_succ B S hS
      (CatFiberedInGroupoids.homFunctor f.hom ⋙ 𝒴.val.val.p)
    letI := hasSheafify_associatedTopology_of_category_succ B S hS 𝒴.val.val.p
    letI := wEqualsLocallyBijective_associatedTopology_of_category_succ B S hS 𝒴.val.val.p
    HasFlatBaseChangePropertySheafUnivLE.{u, u + 1, u, u + 1} B E h S hS 𝒴.val.val.p
      𝒴.val.isFiberedInGroupoids
      ((moduleSheafHigherDirectImage.{u, u + 1, u, u + 1, u} B S hS
        (CatFiberedInGroupoids.homFunctor f.hom ⋙ 𝒴.val.val.p) 𝒴.val.val.p
        (isFiberedInGroupoids_homFunctor_comp B S hS f.hom) 𝒴.val.isFiberedInGroupoids
        (CatFiberedInGroupoids.homFunctor f.hom) rfl (etaleTopology B)
        (etaleTopology_le_topology B) i).obj F)

AlgebraicGeometry.Stack.hasFlatBaseChangePropertyUnivLE_moduleSheafHigherDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/HigherDirectImageSmoothLocalCriterion.lean, line 582. The attribute's comment: “the whole statement, in every degree and with the source's hypotheses unweakened, granted six named hypotheses: Stacks 076Z quantified over every rule; the weak Serre condition for LQCoh^fbc (Stacks 06WM (1)-(3), Stacks 0764 (2)); Stacks 0764 (1) and (3); Stacks 075Y at section universe u+1; and the affine case (Stacks 075P, Stacks 073K)”.

Stacks 0765. Let f : 𝒳 ⟶ 𝒴 be a quasi-compact (Stacks 050U) and quasi-separated (Stacks 04YW) 1-morphism of algebraic stacks over S and let ℱ be a sheaf of 𝒪_𝒳-modules on 𝒳_étale which is locally quasi-coherent (Stacks 06WJ) and has the flat base change property (Stacks 0762). Then every higher direct image Rⁱf_*ℱ, computed in the étale topology, has the flat base change property.

The conclusion is AlgebraicGeometry.Stack.HasFlatBaseChangePropertyHigherDirectImage: both hypotheses on ℱ are the source's, the conclusion is about the flat base change property alone as in the source, and it holds in every degree.

The route is the source's: the criterion of Stacks 076Z at the rule LQCoh^fbc, whose conclusion gives local quasi-coherence of Rⁱf_*ℱ — which is Stacks 075Z — and the flat base change property, of which only the latter is asserted. Five hypotheses are carried, each a clause of that criterion at LQCoh^fbc or at the flat base change property alone, and each a result of the source this library does not have:

  • hcrit is Stacks 076Z, quantified over every rule.
  • hserre is hypothesis (1) for LQCoh^fbc, which is parts (1) to (3) of Stacks 06WM together with part (2) of Stacks 0764.
  • hfbcPull is the flat base change half of hypothesis (2), which is part (1) of Stacks 0764; its local quasi-coherence half is Stacks 06WL and is proved.
  • hconvLqc and hconvFbc are the two halves of the converse of hypothesis (3), namely Stacks 075Y at section universe u + 1 and part (3) of Stacks 0764.
  • haffine is hypothesis (4) for LQCoh^fbc, which the source proves from Stacks 075P and Stacks 073K; Stacks 073K is proved but the cohomological content of Stacks 075P is not.
theorem hasFlatBaseChangePropertyUnivLE_moduleSheafHigherDirectImage
    (hcrit : SmoothLocalHigherDirectImageCriterion.{u, t, s} B S hS)
    (hserre : StackEtaleModuleRule.IsWeakSerre.{u, t} B S hS
      (locallyQuasicoherentFlatBaseChangeRule B E h S hS))
    (hfbcPull : StackEtaleModuleRule.IsStableUnderSmoothPullback.{u, t} B S hS
      (flatBaseChangePropertyRule B E h S hS))
    (hconvLqc : StackEtaleModuleRule.IsSmoothLocalConverse.{u, t, s} B S hS
      (locallyQuasicoherentRule B E h S hS))
    (hconvFbc : StackEtaleModuleRule.IsSmoothLocalConverse.{u, t, s} B S hS
      (flatBaseChangePropertyRule B E h S hS))
    (haffine : StackEtaleModuleRule.PreservesHigherDirectImagesOfAffine.{u, t} B S hS
      (locallyQuasicoherentFlatBaseChangeRule B E h S hS))
    {𝒳 𝒴 : AlgebraicStacks.{u, t} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hqc : IsQuasiCompactMorphism B S hS f)
    (hqs : AlgebraicStacks.IsQuasiSeparated B S hS f) (i : ℕ) :
    HasFlatBaseChangePropertyHigherDirectImage B E h S hS f i
Sources

Section103.8 Locally quasi-coherent modules with the flat base change property#

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

Tag 0771, a proposition

Tag 0771 in the Stacks Project.

AlgebraicGeometry.Stack.isLocallyQuasicoherentWithFlatBaseChange_fppfModulesPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatBaseChangeFppfPullback.lean, line 85. The attribute's comment: “part (3): the inverse image along a 1-morphism of algebraic stacks of a module in LQCoh^fbc lies in LQCoh^fbc, with the ambient category the modules on the fppf site, which is the source's own”.

Stacks 0771, part (3), in the source's ambient category. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks and let F be a module on the fppf site of 𝒴 lying in LQCoh^fbc(𝒪_𝒴). Then the inverse image f^*F lies in LQCoh^fbc(𝒪_𝒳).

AlgebraicGeometry.Stack.isLocallyQuasicoherentWithFlatBaseChange_stackInverseImage is this statement for the inverse image of presheaves of modules, stated at the structure functor f ⋙ 𝒪_𝒴 of the composite presentation; the structure functor of the source is a parameter p here, together with the identification e, so that substituting e puts the goal at the composite presentation where that statement applies. See the implementation notes.

theorem isLocallyQuasicoherentWithFlatBaseChange_fppfModulesPullback
    {p : 𝒳.val.val.obj ⥤ BigFppfOver B S hS}
    (e : CatFiberedInGroupoids.homFunctor f.hom ⋙ 𝒴.val.val.p = p)
    (hp : p.IsFiberedInGroupoids) (F : fppfModules B S hS 𝒴)
    (hF : locallyQuasicoherentFlatBaseChangeFppfModules B E hE S hS 𝒴 F) :
    IsLocallyQuasicoherentWithFlatBaseChange B E hE S hS p hp
      ((modulePullback.{u, u + 1, u, u, u + 1, u} B S hS p 𝒴.val.val.p hp
        𝒴.val.isFiberedInGroupoids (CatFiberedInGroupoids.homFunctor f.hom) e
        B.topology le_rfl).obj F).val

AlgebraicGeometry.Stack.isLocallyQuasicoherentWithFlatBaseChange_stackModulePresheafPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatBaseChangePullback.lean, line 100. The attribute's comment: “part (3), the local quasi-coherence half: the inverse image along a 1-morphism of algebraic stacks of a module in LQCoh^fbc lies in LQCoh^fbc, with the flat base change property of the inverse image assumed (Stacks 0764 part (1))”.

Stacks 0771, part (3), the local quasi-coherence half. Let g : 𝒵 ⟶ 𝒳 be a 1-morphism of algebraic stacks over S and let F lie in LQCoh^fbc(𝒪_𝒳). Then the inverse image g^{-1}F lies in LQCoh^fbc(𝒪_𝒵).

Local quasi-coherence of g^{-1}F is Stacks 06WL, which holds for every 1-morphism of categories fibred in groupoids. The flat base change property of g^{-1}F is the hypothesis hfbc: the source deduces it from Stacks 0764 part (1), whose module-level ingredient — the form of Stacks 075D part (4) for presheaves of modules — is not available; see the implementation notes of this file.

theorem isLocallyQuasicoherentWithFlatBaseChange_stackModulePresheafPullback
    {𝒵 𝒳 : AlgebraicStacks.{u, w} B S hS} (g : 𝒵 ⟶ 𝒳)
    (F : PresheafOfModules.{u} (ringStructureSheafCore B S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids (etaleTopology B) (etaleTopology_le_topology B)).obj)
    (hF : IsLocallyQuasicoherentWithFlatBaseChange B E h S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids F)
    (hfbc : HasFlatBaseChangeProperty B E h S hS
      (CatFiberedInGroupoids.homFunctor g.hom ⋙ 𝒳.val.val.p)
      (isFiberedInGroupoids_homFunctor_comp B S hS g.hom) (etaleTopology B)
      (etaleTopology_le_topology B)
      ((stackModulePresheafPullback.{u, w, u} B S hS g).obj F)) :
    IsLocallyQuasicoherentWithFlatBaseChange B E h S hS
      (CatFiberedInGroupoids.homFunctor g.hom ⋙ 𝒳.val.val.p)
      (isFiberedInGroupoids_homFunctor_comp B S hS g.hom)
      ((stackModulePresheafPullback.{u, w, u} B S hS g).obj F)

AlgebraicGeometry.Stack.isSheaf_fppf_of_isLocallyQuasicoherentWithSheafFlatBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FppfSheafFromSheafFlatBaseChange.lean, line 399. The attribute's comment: “part (1): a member of LQCoh^fbc (with the flat base change property of 0762 read on sheaves) is a sheaf for the fppf topology; for every category fibred in groupoids”.

Stacks 0771, part (1). A presheaf of modules over the structure sheaf of a category fibred in groupoids over the big fppf site which lies in LQCoh^fbc(𝒪_𝒳) — locally quasi-coherent (Stacks 06WJ) with the flat base change property of Stacks 0762 — is a sheaf for the fppf topology of Stacks 06TP.

This is Stacks 076T, AlgebraicGeometry.Stack.isSheaf_fppf_of_isLocallyQuasicoherent_of_sheafFlatLfpBaseChange, whose hypothesis (b) asks the flat base change property of fewer arrows. The module sections are in the universe of the schemes; the statement holds for every category fibred in groupoids, which generalizes the source's algebraic stack.

theorem isSheaf_fppf_of_isLocallyQuasicoherentWithSheafFlatBaseChange
    (hF : IsLocallyQuasicoherentWithSheafFlatBaseChange B E h S hS p hp F) :
    Presheaf.IsSheaf (associatedTopology B S hS p B.topology) F.presheaf

AlgebraicGeometry.Stack.fppfModuleOfLqcohSheafFbc, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FppfSheafFromSheafFlatBaseChange.lean, line 410. The attribute's comment: “part (1), the clause i.e. it is an object of Mod(𝒪_𝒳): the fppf module a member of LQCoh^fbc is, again in LQCoh^fbc”.

Stacks 0771, part (1), the clause "it is an object of Mod(𝒪_𝒳)": a member of LQCoh^fbc(𝒪_𝒳) ⊆ Mod(𝒳_ét, 𝒪_𝒳) on an algebraic stack is a module on the fppf site, with the same underlying presheaf of modules, and it lies in LQCoh^fbc(𝒪_𝒳) ⊆ Mod(𝒪_𝒳).

noncomputable def fppfModuleOfLqcohSheafFbc (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (G : SheafOfModules.{u} (ringStructureSheafCore B S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids (etaleTopology B) (etaleTopology_le_topology B)))
    (hG : lqcohSheafFbcEtaleModules.{u, w, u} B E h S hS 𝒳 G) :
    (lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳).FullSubcategory

AlgebraicGeometry.Stack.isSheaf_fppf_of_isLocallyQuasicoherentWithFlatBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LocallyQuasicoherentFlatBaseChangeSummary.lean, line 164. The attribute's comment: “part (1): a member of LQCoh^fbc is a sheaf for the fppf topology of Stacks 06TP; stated for every category fibred in groupoids, which generalizes the source's algebraic stack”.

Stacks 0771, part (1). A presheaf of modules over the structure sheaf of a category fibred in groupoids over the big fppf site which is locally quasi-coherent (Stacks 06WJ) and has the flat base change property (Stacks 0762) — that is, a member of LQCoh^fbc(𝒪_𝒳) — is a sheaf for the fppf topology of Stacks 06TP.

Membership in LQCoh^fbc asks the comparison map c_φ of Stacks 06WC to be an isomorphism along every arrow lying over a flat morphism of schemes, which is more than the hypothesis of Stacks 076T, where only the arrows lying over a flat morphism locally of finite presentation are looked at. So part (1) is Stacks 076T after AlgebraicGeometry.Stack.hasFlatLfpBaseChangeProperty_of_hasFlatBaseChangeProperty.

theorem isSheaf_fppf_of_isLocallyQuasicoherentWithFlatBaseChange
    (F : PresheafOfModules.{u} (ringStructureSheafCore B S hS p hp (etaleTopology B)
      (etaleTopology_le_topology B)).obj)
    (hF : IsLocallyQuasicoherentWithFlatBaseChange B E h S hS p hp F) :
    Presheaf.IsSheaf (associatedTopology B S hS p B.topology) F.presheaf

AlgebraicGeometry.Stack.fppfModuleOfLocallyQuasicoherentWithFlatBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LocallyQuasicoherentFlatBaseChangeSummary.lean, line 190. The attribute's comment: “part (1), the clause hence lies in Mod(𝒪_𝒳): the module on the fppf site of an algebraic stack that a member of LQCoh^fbc is”.

Stacks 0771, part (1), the object of Mod(𝒪_𝒳) the source's clause ends with: a member of LQCoh^fbc(𝒪_𝒳), being a sheaf for the fppf topology by AlgebraicGeometry.Stack.isSheaf_fppf_of_isLocallyQuasicoherentWithFlatBaseChange, is a module on the fppf site of the algebraic stack.

No transport is involved. The presheaf of rings underlying the structure sheaf of Stacks 06TV is p.op ⋙ (BigFppfOver.structureSheaf B S hS).obj whichever of the five topologies of Stacks 06TP it is read at, so the presheaf of modules is already a presheaf of modules over the fppf structure sheaf, and only its sheaf condition has to be improved.

def fppfModuleOfLocallyQuasicoherentWithFlatBaseChange
    (F : PresheafOfModules.{u} (ringStructureSheafCore B S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids (etaleTopology B) (etaleTopology_le_topology B)).obj)
    (hF : IsLocallyQuasicoherentWithFlatBaseChange B E h S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids F) :
    fppfModules B S hS 𝒳

AlgebraicGeometry.Stack.isLocallyQuasicoherentWithFlatBaseChangeUnivLE_moduleSheafHigherDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LocallyQuasicoherentFlatBaseChangeSummary.lean, line 259. The attribute's comment: “part (4)(b), in every degree, over the six hypotheses Stacks 0765 carries (Stacks 076Z; Stacks 06WM (1)-(3) with 0764 (2); 0764 (1) and (3); 075Y at u+1; 075P and 073K). THIS IS THE ETALE READING AND NOT THE TAG'S DEFAULT FPPF ONE: part (4)(a), the agreement of the two, is not asserted here”.

Stacks 0771, part (4)(b). Let f : 𝒳 ⟶ 𝒴 be a quasi-compact (Stacks 050U) and quasi-separated (Stacks 04YW) 1-morphism of algebraic stacks over S and let ℱ be a sheaf of 𝒪_𝒳-modules on 𝒳_étale which is locally quasi-coherent (Stacks 06WJ) and has the flat base change property (Stacks 0762). Then the higher direct image Rⁱf_*ℱ of Stacks 06WE, computed in the étale topology, is again locally quasi-coherent and has the flat base change property, in every degree i: that is, Rⁱf_* carries LQCoh^fbc(𝒪_𝒳) into LQCoh^fbc(𝒪_𝒴).

The flat base change property is read at section universe u + 1, where the higher direct images of module sheaves live, by AlgebraicGeometry.Stack.HasFlatBaseChangePropertyUnivLE.

This is the conclusion of the criterion of Stacks 076Z at the rule LQCoh^fbc, so it is obtained from exactly the six hypotheses AlgebraicGeometry.Stack.hasFlatBaseChangePropertyUnivLE_moduleSheafHigherDirectImage (Stacks 0765) carries, each a result of the source this library does not have: hcrit is Stacks 076Z quantified over every rule, hserre is parts (1) to (3) of Stacks 06WM with part (2) of Stacks 0764, hfbcPull is part (1) of Stacks 0764, hconvLqc and hconvFbc are Stacks 075Y at section universe u + 1 and part (3) of Stacks 0764, and haffine is the affine case, from Stacks 075P and Stacks 073K. Stacks 0765 is the same criterion with only the flat base change conjunct of its conclusion kept, and Stacks 075Z is the criterion at the rule of local quasi-coherence alone; neither of them states the conjunction, and the conjunction is what part (4)(b) asserts.

Hypothesis (2) of the criterion for local quasi-coherence is Stacks 06WL and is not carried: it is supplied by AlgebraicGeometry.Stack.isStableUnderSmoothPullback_locallyQuasicoherentRule, which also supplies the forward half of hypothesis (3).

theorem isLocallyQuasicoherentWithFlatBaseChangeUnivLE_moduleSheafHigherDirectImage
    (hcrit : SmoothLocalHigherDirectImageCriterion.{u, t, s} B S hS)
    (hserre : StackEtaleModuleRule.IsWeakSerre.{u, t} B S hS
      (locallyQuasicoherentFlatBaseChangeRule B E h S hS))
    (hfbcPull : StackEtaleModuleRule.IsStableUnderSmoothPullback.{u, t} B S hS
      (flatBaseChangePropertyRule B E h S hS))
    (hconvLqc : StackEtaleModuleRule.IsSmoothLocalConverse.{u, t, s} B S hS
      (locallyQuasicoherentRule B E h S hS))
    (hconvFbc : StackEtaleModuleRule.IsSmoothLocalConverse.{u, t, s} B S hS
      (flatBaseChangePropertyRule B E h S hS))
    (haffine : StackEtaleModuleRule.PreservesHigherDirectImagesOfAffine.{u, t} B S hS
      (locallyQuasicoherentFlatBaseChangeRule B E h S hS))
    {𝒳 𝒴 : AlgebraicStacks.{u, t} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hqc : IsQuasiCompactMorphism B S hS f)
    (hqs : AlgebraicStacks.IsQuasiSeparated B S hS f) (i : ℕ) :
    letI := hasSheafify_associatedTopology_of_category_succ B S hS
      (CatFiberedInGroupoids.homFunctor f.hom ⋙ 𝒴.val.val.p)
    letI := wEqualsLocallyBijective_associatedTopology_of_category_succ B S hS
      (CatFiberedInGroupoids.homFunctor f.hom ⋙ 𝒴.val.val.p)
    letI := hasSheafify_associatedTopology_of_category_succ B S hS 𝒴.val.val.p
    letI := wEqualsLocallyBijective_associatedTopology_of_category_succ B S hS 𝒴.val.val.p
    ∀ ℱ : SheafOfModules.{u + 1} (ringStructureSheafCore B S hS
        (CatFiberedInGroupoids.homFunctor f.hom ⋙ 𝒴.val.val.p)
        (isFiberedInGroupoids_homFunctor_comp B S hS f.hom)
        (etaleTopology B) (etaleTopology_le_topology B)),
      IsLocallyQuasicoherent B E h S hS
          (CatFiberedInGroupoids.homFunctor f.hom ⋙ 𝒴.val.val.p)
          (isFiberedInGroupoids_homFunctor_comp B S hS f.hom) ℱ.val →
        HasFlatBaseChangePropertyUnivLE B E h S hS
            (CatFiberedInGroupoids.homFunctor f.hom ⋙ 𝒴.val.val.p)
            (isFiberedInGroupoids_homFunctor_comp B S hS f.hom)
            (etaleTopology B) (etaleTopology_le_topology B) ℱ.val →
          IsLocallyQuasicoherent B E h S hS 𝒴.val.val.p 𝒴.val.isFiberedInGroupoids
              ((moduleSheafHigherDirectImage.{u, u + 1, u, u + 1, u} B S hS
                (CatFiberedInGroupoids.homFunctor f.hom ⋙ 𝒴.val.val.p) 𝒴.val.val.p
                (isFiberedInGroupoids_homFunctor_comp B S hS f.hom) 𝒴.val.isFiberedInGroupoids
                (CatFiberedInGroupoids.homFunctor f.hom) rfl (etaleTopology B)
                (etaleTopology_le_topology B) i).obj ℱ).val ∧
            HasFlatBaseChangePropertyUnivLE B E h S hS 𝒴.val.val.p
              𝒴.val.isFiberedInGroupoids (etaleTopology B) (etaleTopology_le_topology B)
              ((moduleSheafHigherDirectImage.{u, u + 1, u, u + 1, u} B S hS
                (CatFiberedInGroupoids.homFunctor f.hom ⋙ 𝒴.val.val.p) 𝒴.val.val.p
                (isFiberedInGroupoids_homFunctor_comp B S hS f.hom) 𝒴.val.isFiberedInGroupoids
                (CatFiberedInGroupoids.homFunctor f.hom) rfl (etaleTopology B)
                (etaleTopology_le_topology B) i).obj ℱ).val

AlgebraicGeometry.Stack.lqcohSheafFbcFppfModules_fppfModulesHigherDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LqcohSheafFbcFppfHigherDirectImage.lean, line 101. The attribute's comment: “part (4)(b), in Mod(O_Y): the higher direct images computed in the fppf topology, modules at the module universe u of the schemes”.

Stacks 0771, part (4)(b), in Mod(𝒪_𝒴). Let f : 𝒳 ⟶ 𝒴 be a quasi-compact and quasi-separated 1-morphism of algebraic stacks and F an object of LQCoh^fbc(𝒪_𝒳). Then each higher direct image Rⁱf_*F, computed in the fppf topology, is an object of LQCoh^fbc(𝒪_𝒴).

Modules have sections in the universe u of the schemes; local quasi-coherence is read against an auxiliary big étale site E with E.cutoff = B.cutoff, and the flat base change property is the sheaf-level one of Stacks 0762.

theorem lqcohSheafFbcFppfModules_fppfModulesHigherDirectImage
    {𝒳 𝒴 : AlgebraicStacks.{u, t} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hqc : IsQuasiCompactMorphism B S hS f) (hqs : AlgebraicStacks.IsQuasiSeparated B S hS f)
    (F : StackModules B S hS .fppf 𝒳) (hF : lqcohSheafFbcFppfModules.{u, t, u} B E h S hS 𝒳 F)
    (i : ℕ) :
    lqcohSheafFbcFppfModules.{u, t, u} B E h S hS 𝒴
      ((fppfModulesHigherDirectImage B S hS f i).obj F)

AlgebraicGeometry.Stack.nonempty_etaleComparison_fppfModulesHigherDirectImage_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LqcohSheafFbcFppfHigherDirectImage.lean, line 125. The attribute's comment: “part (4)(a), for the higher direct images R^i f_ (not the total direct image Rf_), modules at the module universe u of the schemes”.

Stacks 0771, part (4)(a), for the higher direct images. Let f : 𝒳 ⟶ 𝒴 be a quasi-compact and quasi-separated 1-morphism of algebraic stacks and F an object of LQCoh^fbc(𝒪_𝒳). Then Rⁱf_*F is the same whether computed in the étale or in the fppf topology: ε_*(Rⁱf_{fppf,*}F) ≅ Rⁱf_{ét,*}(ε_*F), where ε_* reads an fppf module on the étale site.

Modules have sections in the universe u of the schemes. The assertion of the source about the total direct image Rf_* is not included: there is no derived direct image at that universe on the sites of algebraic stacks in the library.

theorem nonempty_etaleComparison_fppfModulesHigherDirectImage_iso
    {𝒳 𝒴 : AlgebraicStacks.{u, t} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hqc : IsQuasiCompactMorphism B S hS f) (hqs : AlgebraicStacks.IsQuasiSeparated B S hS f)
    (F : StackModules B S hS .fppf 𝒳) (hF : lqcohSheafFbcFppfModules.{u, t, u} B E h S hS 𝒳 F)
    (i : ℕ) :
    Nonempty ((stackModulesEtaleComparison B S hS 𝒴).obj
        ((fppfModulesHigherDirectImage B S hS f i).obj F) ≅
      (stackModuleHigherDirectImage B S hS f .etale i).obj
        ((stackModulesEtaleComparison B S hS 𝒳).obj F))

AlgebraicGeometry.Stack.lqcohSheafFbcModuleRule_stackModuleHigherDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LqcohSheafFbcHigherDirectImage.lean, line 59. The attribute's comment: “part (4)(b), with the higher direct images computed in the étale topology, modules at the module universe u of the schemes”.

Stacks 0771, part (4)(b), in the étale topology. Let f : 𝒳 ⟶ 𝒴 be a quasi-compact and quasi-separated 1-morphism of algebraic stacks and F an object of LQCoh^fbc(𝒪_𝒳), a module on 𝒳_étale which is locally quasi-coherent with the flat base change property. Then each higher direct image Rⁱf_*F, computed in the étale topology, is an object of LQCoh^fbc(𝒪_𝒴).

Modules have sections in the universe u of the schemes, local quasi-coherence is read against an auxiliary big étale site E with E.cutoff = B.cutoff, and the flat base change property is the sheaf-level one of Stacks 0762 (AlgebraicGeometry.Stack.HasSheafFlatBaseChangeProperty).

theorem lqcohSheafFbcModuleRule_stackModuleHigherDirectImage
    {𝒳 𝒴 : AlgebraicStacks.{u, t} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hqc : IsQuasiCompactMorphism B S hS f) (hqs : AlgebraicStacks.IsQuasiSeparated B S hS f)
    (F : StackModules B S hS .etale 𝒳)
    (hF : IsLocallyQuasicoherentWithSheafFlatBaseChange B E h S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids F.val) (i : ℕ) :
    IsLocallyQuasicoherentWithSheafFlatBaseChange B E h S hS 𝒴.val.val.p
      𝒴.val.isFiberedInGroupoids ((stackModuleHigherDirectImage B S hS f .etale i).obj F).val

AlgebraicGeometry.Stack.lqcohSheafFbcEtaleModules_stackModuleInverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LqcohSheafFbcPullback.lean, line 374. The attribute's comment: “part (3), on Mod(𝒳_ét, 𝒪_𝒳), with the flat base change property of 0762 read on sheaves; the module sections in the universe of the schemes”.

Stacks 0771, part (3), on Mod(𝒳_ét, 𝒪_𝒳): the inverse image along a 1-morphism of algebraic stacks of the étale sites carries LQCoh^fbc(𝒪_𝒴) into LQCoh^fbc(𝒪_𝒳).

theorem lqcohSheafFbcEtaleModules_stackModuleInverseImage (F : StackModules B S hS .etale 𝒴)
    (hF : lqcohSheafFbcEtaleModules.{u, w, u} B E h S hS 𝒴 F) :
    lqcohSheafFbcEtaleModules.{u, w, u} B E h S hS 𝒳
      ((stackModuleInverseImage B S hS .etale f).obj F)

AlgebraicGeometry.Stack.lqcohSheafFbcFppfModules_fppfModulesPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LqcohSheafFbcPullback.lean, line 387. The attribute's comment: “part (3), on Mod(𝒪_𝒳), with the flat base change property of 0762 read on sheaves; the module sections in the universe of the schemes”.

Stacks 0771, part (3), on Mod(𝒪_𝒳): the inverse image along a 1-morphism of algebraic stacks of the fppf sites carries LQCoh^fbc(𝒪_𝒴) into LQCoh^fbc(𝒪_𝒳).

theorem lqcohSheafFbcFppfModules_fppfModulesPullback (F : fppfModules B S hS 𝒴)
    (hF : lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒴 F) :
    lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳 ((fppfModulesPullback B S hS f).obj F)

AlgebraicGeometry.Stack.lqcohSheafFbcTotalDirectImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LqcohSheafFbcTotalDirectImage.lean, line 115. The attribute's comment: “part (4)(a), total direct image Rf_: Rf_{ét,}(ε_F) ≅ Rε_(Rf_{fppf,*}F) in D⁺(𝒴_ét), for F in LQCoh^fbc and every 1-morphism f, modules at the module universe u of the schemes”.

Stacks 0771, part (4)(a), for the total direct image. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks and F an object of LQCoh^fbc(𝒪_𝒳) ⊆ Mod(𝒪_𝒳). The total direct image of F computed in the étale topology is the one computed in the fppf topology, read on the étale site: Rf_{ét,*}(ε_*F) ≅ Rε_*(Rf_{fppf,*}F) in D⁺(Mod(𝒴_ét, 𝒪_𝒴)).

Here ε_* : Mod(𝒪_𝒴) ⥤ Mod(𝒴_ét, 𝒪_𝒴) is only left exact, so the fppf result is compared through its right derived functor Rε_*. The isomorphism is AlgebraicGeometry.Stack.totalDirectImageEtaleComparisonIso together with Rε_*F ≅ ε_*F, which is Stacks 075R (1), AlgebraicGeometry.Stack.isZero_rightDerived_etaleComparisonPushforward_of_lqcohSheafFbc. No quasi-compactness or quasi-separatedness of f is needed for this form. When f is quasi-compact and quasi-separated, part (4)(b) and Stacks 075R (1) make the cohomology sheaves Rⁱf_{fppf,*}F of Rf_{fppf,*}F themselves ε_*-acyclic, so that Rε_* there is ε_* applied to the cohomology sheaves: that is the form of part (4)(a) for the higher direct images, AlgebraicGeometry.Stack.nonempty_etaleComparison_fppfModulesHigherDirectImage_iso, and AlgebraicGeometry.Stack.nonempty_homology_etaleComparison_totalDirectImage_iso below.

noncomputable def lqcohSheafFbcTotalDirectImageIso (f : 𝒳 ⟶ 𝒴) (F : StackModules B S hS .fppf 𝒳)
    (hF : lqcohSheafFbcFppfModules.{u, t, u} B E h S hS 𝒳 F) :
    (stackModuleDirectImage B S hS f .etale).rightDerivedFunctorPlus.obj
        ((DerivedCategory.Plus.singleFunctor _ 0).obj
          ((stackModulesEtaleComparison B S hS 𝒳).obj F)) ≅
      (stackModulesEtaleComparison B S hS 𝒴).rightDerivedFunctorPlus.obj
        ((stackModuleDirectImage B S hS f .fppf).rightDerivedFunctorPlus.obj
          ((DerivedCategory.Plus.singleFunctor _ 0).obj F))

AlgebraicGeometry.Stack.lqcohSheafFbc_hasColimits_and_agree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/SheafFlatBaseChangeColimits.lean, line 261. The attribute's comment: “part (5): LQCoh^fbc(𝒪_𝒳) has small colimits, agreeing with those of Mod(𝒪_𝒳) and of Mod(𝒳_étale, 𝒪_𝒳)”.

Stacks 0771, part (5). The category LQCoh^fbc(𝒪_𝒳) has colimits, and they agree with colimits in Mod(𝒳_étale, 𝒪_𝒳) as well as in Mod(𝒪_𝒳).

In order: LQCoh^fbc(𝒪_𝒳), read inside Mod(𝒪_𝒳), has small colimits and its inclusion preserves them; read inside Mod(𝒳_étale, 𝒪_𝒳) the same holds; and restricting a colimit cocone in Mod(𝒪_𝒳) of objects of LQCoh^fbc(𝒪_𝒳) to the étale site gives a colimit cocone in Mod(𝒳_étale, 𝒪_𝒳), so the two readings compute the same colimits.

theorem lqcohSheafFbc_hasColimits_and_agree :
    HasColimitsOfSize.{u, u} (lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳).FullSubcategory ∧
      PreservesColimitsOfSize.{u, u} (lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳).ι ∧
      (HasColimitsOfSize.{u, u}
          (lqcohSheafFbcEtaleModules.{u, w, u} B E h S hS 𝒳).FullSubcategory ∧
        PreservesColimitsOfSize.{u, u} (lqcohSheafFbcEtaleModules.{u, w, u} B E h S hS 𝒳).ι) ∧
      ∀ {K : Type u} [Category.{u} K] {D : K ⥤ fppfModules B S hS 𝒳},
        (∀ k, lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳 (D.obj k)) →
          ∀ {c : Cocone D}, IsColimit c →
            Nonempty (IsColimit ((fppfToEtaleModules B S hS 𝒳).mapCocone c))

AlgebraicGeometry.Stack.lqcohSheafFbcFppfModules_fppfInternalHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/SheafFlatBaseChangeInternalHom.lean, line 66. The attribute's comment: “part (7): LQCoh^fbc is closed under SheafHom(F, -) of Mod(𝒪_𝒳) for F of finite presentation in Mod(𝒪_𝒳)”.

Stacks 0771, part (7). For F an 𝒪_𝒳-module of finite presentation and G in LQCoh^fbc(𝒪_𝒳) on an algebraic stack, the internal Hom SheafHom_{𝒪_𝒳}(F, G) of Mod(𝒪_𝒳) is in LQCoh^fbc(𝒪_𝒳).

G is cartesian along the flat arrows between objects over affine schemes (step R2 of Stacks 0779), hence so is SheafHom_{𝒪_𝒳}(F, G), F being of finite presentation; a module cartesian along those arrows is locally quasi-coherent and has the flat base change property.

theorem lqcohSheafFbcFppfModules_fppfInternalHom (F G : fppfModules B S hS 𝒳)
    [F.IsFinitePresentationOnSite]
    (hG : lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳 G) :
    lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳
      (AlgebraicStacks.fppfInternalHom B S hS 𝒳 F G)

AlgebraicGeometry.Stack.lqcohSheafFbcFppfModules_sheafTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/SheafFlatBaseChangeTensor.lean, line 67. The attribute's comment: “part (6): LQCoh^fbc is closed under the tensor product of Mod(𝒪_𝒳)”.

Stacks 0771, part (6). For F and G in LQCoh^fbc(𝒪_𝒳) on an algebraic stack, the tensor product F ⊗_{𝒪_𝒳} G computed in Mod(𝒪_𝒳) is again in LQCoh^fbc(𝒪_𝒳).

Both factors are cartesian along the flat arrows between objects over affine schemes (step R2 of Stacks 0779), hence so is their tensor product, whose sections over an affine object are the tensor product of the sections; a module cartesian along those arrows is locally quasi-coherent and has the flat base change property.

theorem lqcohSheafFbcFppfModules_sheafTensor (F G : fppfModules B S hS 𝒳)
    (hF : lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳 F)
    (hG : lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳 G) :
    lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳
      (((Stacks.SheafOfModules.Tensor.sheafTensor.{u + 1, u, u, u, u}
        (FlatFppf.fppfRingedTopos B S hS 𝒳).O).obj
        F).obj G)

AlgebraicGeometry.Stack.isWeakSerreClass_lqcohSheafFbcEtaleModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/SheafFlatBaseChangeWeakSerre.lean, line 500. The attribute's comment: “part (2), the étale half: LQCoh^fbc is a weak Serre subcategory of Mod(𝒳_ét, 𝒪_𝒳), with the flat base change property of 0762 read on sheaves”.

Stacks 0771, part (2), the étale half: LQCoh^fbc(𝒪_𝒳) is a weak Serre subcategory of Mod(𝒳_ét, 𝒪_𝒳), for an algebraic stack 𝒳, at module universe u, with the abelian structure coming from the sheafification of abelian presheaves on the associated étale site (AlgebraicGeometry.Stack.hasSheafify_etaleAssociatedTopology).

theorem isWeakSerreClass_lqcohSheafFbcEtaleModules (𝒳 : AlgebraicStacks.{u, w} B S hS) :
    letI := hasSheafify_etaleAssociatedTopology B S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids
    letI := wEqualsLocallyBijective_etaleAssociatedTopology B S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids
    (lqcohSheafFbcEtaleModules.{u, w, u} B E h S hS 𝒳).IsWeakSerreClass

AlgebraicGeometry.Stack.isWeakSerreClass_lqcohSheafFbcFppfModules, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/SheafFlatBaseChangeWeakSerreFppf.lean, line 291. The attribute's comment: “part (2), fppf half: LQCoh^fbc is a weak Serre subcategory of Mod(𝒪_𝒳)”.

Stacks 0771, part (2), the fppf half: LQCoh^fbc(𝒪_𝒳) is a weak Serre subcategory of Mod(𝒪_𝒳), for an algebraic stack 𝒳, at module universe u, with the abelian structure coming from the sheafification of abelian presheaves on the fppf site (AlgebraicGeometry.Stack.FlatFppf.hasSheafify_fppf_addCommGrpCat): it contains 0 and is closed under isomorphisms, kernels, cokernels and extensions (Stacks 0754).

instance isWeakSerreClass_lqcohSheafFbcFppfModules :
    (lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳).IsWeakSerreClass
Tag 07AQ, a lemma

Tag 07AQ in the Stacks Project.

AlgebraicGeometry.Stack.isLocallyQuasicoherentWithFlatBaseChange_of_isSmooth_jointlySurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatBaseChangeSmoothLocal.lean, line 154. The attribute's comment: “part (1), the local quasi-coherence half: the criterion along a jointly surjective family of smooth morphisms, with the flat base change property of the source assumed (Stacks 0764 part (3))”.

Stacks 07AQ, part (1), the local quasi-coherence half. Let f j : 𝒵 j ⟶ 𝒳 be a family of smooth 1-morphisms of algebraic stacks over S with |𝒳| = ⋃ j, |f j|(|𝒵 j|), and let F be a sheaf of 𝒪_𝒳-modules on 𝒳_étale. If every inverse image f j^{-1} F lies in LQCoh^fbc(𝒪_{𝒵 j}) and F has the flat base change property, then F lies in LQCoh^fbc(𝒪_𝒳).

Local quasi-coherence of F is Stacks 075Y, applied to the local quasi-coherence of the inverse images. The flat base change property of F is the hypothesis hfbc: the source deduces it from Stacks 0764 part (3), whose argument is not available for the presheaf-level inverse image that the flat base change property is formulated with here; see the implementation notes of this file.

theorem isLocallyQuasicoherentWithFlatBaseChange_of_isSmooth_jointlySurjective
    {J : Type v} {𝒵 : J → AlgebraicStacks.{u, w} B S hS} {𝒳 : AlgebraicStacks.{u, w} B S hS}
    (f : ∀ j, 𝒵 j ⟶ 𝒳)
    (hsmooth : ∀ j, AlgebraicStacks.IsSmooth B S hS (f j))
    (hjs : (Set.univ : Set (AlgebraicStacks.points B S hS 𝒳)) =
      ⋃ j, Set.range (AlgebraicStacks.pointsMap B S hS (f j)))
    (F : PresheafOfModules.{u} (ringStructureSheafCore B S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids (etaleTopology B) (etaleTopology_le_topology B)).obj)
    (hF : Presheaf.IsSheaf (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B)) F.presheaf)
    (hfbc : HasFlatBaseChangeProperty B E h S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids
      (etaleTopology B) (etaleTopology_le_topology B) F)
    (hlqc : ∀ j, IsLocallyQuasicoherentWithFlatBaseChange B E h S hS
      (CatFiberedInGroupoids.homFunctor (f j).hom ⋙ 𝒳.val.val.p)
      (isFiberedInGroupoids_homFunctor_comp B S hS (f j).hom)
      ((stackModulePresheafPullback.{u, w, u} B S hS (f j)).obj F)) :
    IsLocallyQuasicoherentWithFlatBaseChange B E h S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids
      F

AlgebraicGeometry.Stack.lqcohSheafFbcEtaleModules_of_isSmooth_jointlySurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LqcohSheafFbcFlatDescent.lean, line 98. The attribute's comment: “part (1), on Mod(𝒳_ét, 𝒪_𝒳), with the flat base change property of 0762 read on sheaves; the module sections in the universe of the schemes”.

Stacks 07AQ, part (1). Let f j : 𝒵 j ⟶ 𝒳 be a family of smooth 1-morphisms of algebraic stacks with |𝒳| = ⋃ |f j|(|𝒵 j|), and F a sheaf of 𝒪_𝒳-modules on 𝒳_ét. If every f j^{-1} F is in LQCoh^fbc(𝒪_{𝒵 j}), then F is in LQCoh^fbc(𝒪_𝒳).

The source's hypothesis reads LQCoh^{fpc}, a misprint for LQCoh^{fbc}. LQCoh^fbc is the sheaf-level one (AlgebraicGeometry.Stack.lqcohSheafFbcEtaleModules), with the flat base change property of Stacks 0762; the module sections are in the universe of the schemes.

theorem lqcohSheafFbcEtaleModules_of_isSmooth_jointlySurjective
    {J : Type v} {𝒵 : J → AlgebraicStacks.{u, w} B S hS} {𝒳 : AlgebraicStacks.{u, w} B S hS}
    (f : ∀ j, 𝒵 j ⟶ 𝒳) (hsmooth : ∀ j, AlgebraicStacks.IsSmooth B S hS (f j))
    (hjs : (Set.univ : Set (AlgebraicStacks.points B S hS 𝒳)) =
      ⋃ j, Set.range (AlgebraicStacks.pointsMap B S hS (f j)))
    (F : StackModules B S hS .etale 𝒳)
    (hF : ∀ j, lqcohSheafFbcEtaleModules.{u, w, u} B E h S hS (𝒵 j)
      ((stackModuleInverseImage B S hS .etale (f j)).obj F)) :
    lqcohSheafFbcEtaleModules.{u, w, u} B E h S hS 𝒳 F

AlgebraicGeometry.Stack.lqcohSheafFbcFppfModules_of_isFlat_isLocallyOfFinitePresentation_jointlySurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LqcohSheafFbcFlatDescent.lean, line 203. The attribute's comment: “part (2), on Mod(𝒪_𝒳) (fppf), with the flat base change property of 0762 read on sheaves; the module sections in the universe of the schemes”.

Stacks 07AQ, part (2). Let f j : 𝒵 j ⟶ 𝒳 be a family of flat and locally finitely presented 1-morphisms of algebraic stacks with |𝒳| = ⋃ |f j|(|𝒵 j|), and F a sheaf of 𝒪_𝒳-modules on 𝒳_fppf. If every f j^{-1} F is in LQCoh^fbc(𝒪_{𝒵 j}), then F is in LQCoh^fbc(𝒪_𝒳).

LQCoh^fbc is the sheaf-level one (AlgebraicGeometry.Stack.lqcohSheafFbcFppfModules), with the flat base change property of Stacks 0762; the module sections are in the universe of the schemes. The proof is the source's ("analogous to the proof of 07AP"), carried out for a general module rule in AlgebraicGeometry.Stack.mem_of_isFlat_isLocallyOfFinitePresentation_jointlySurjective.

theorem lqcohSheafFbcFppfModules_of_isFlat_isLocallyOfFinitePresentation_jointlySurjective
    {J : Type v} {𝒵 : J → AlgebraicStacks.{u, w} B S hS} {𝒳 : AlgebraicStacks.{u, w} B S hS}
    (f : ∀ j, 𝒵 j ⟶ 𝒳) (hflat : ∀ j, AlgebraicStacks.IsFlat B S hS (f j))
    (hlfp : ∀ j, AlgebraicStacks.IsLocallyOfFinitePresentation B S hS (f j))
    (hjs : (Set.univ : Set (AlgebraicStacks.points B S hS 𝒳)) =
      ⋃ j, Set.range (AlgebraicStacks.pointsMap B S hS (f j)))
    (F : fppfModules B S hS 𝒳)
    (hF : ∀ j, lqcohSheafFbcFppfModules.{u, w, u} B E h S hS (𝒵 j)
      ((fppfModulesPullback B S hS (f j)).obj F)) :
    lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳 F
Tag 0GQH, a lemma

Tag 0GQH in the Stacks Project.

AlgebraicGeometry.Stack.restrictedFppfModulesHigherDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/RestrictedFppfHigherDirectImage.lean, line 69. The attribute's comment: “the whole lemma, at the module universe u of the schemes: for f : X -> Y quasi-compact, quasi-separated and representable by algebraic spaces, F in LQCoh^fbc(O_X) (the flat base change property read on sheaves, Stacks 0762) and an object y : V -> Y over a scheme V, the 2-fibre product U = V x_Y X is an algebraic space, and for every presentation of it and every i, (R^i f_ F)|_{V_etale} = R^i f'_{small,}(F|_{U_etale}), with R^i f_* the fppf higher direct image of Mod(O_X)”.

Stacks 0GQH. Let f : 𝒳 ⟶ 𝒴 be a quasi-compact (hqc), quasi-separated (hqs) 1-morphism of algebraic stacks which is representable by algebraic spaces (hrep). Let ℱ be in LQCoh^{fbc}(𝒪_𝒳) (hF), and let y : V ⟶ 𝒴 be an object of 𝒴 over a scheme V. Then:

  • the 2-fibre product U = V ×_𝒴 𝒳 is represented by an algebraic space;
  • for every such presentation eU of U by an algebraic space, with f' : U ⟶ V the base change of f (AlgebraicGeometry.Stack.baseChangeSpacesHom), and for every i, (Rⁱf_*ℱ)|_{V_étale} ≅ Rⁱf'_{small,*}(ℱ|_{U_étale}).

Here Rⁱf_* is the higher direct image of Mod(𝒪_𝒳), in the fppf topology. (-)|_{V_étale} reads an fppf module on the étale site (stackModulesEtaleComparison), pulls it back along y and restricts it to the small étale site of V (π_{V,*}, Stacks 073M). (-)|_{U_étale} does the same along the projection U ⟶ 𝒳. f'_{small,*} is the direct image of the small étale sites of the algebraic spaces U and V.

theorem restrictedFppfModulesHigherDirectImage {𝒳 𝒴 : AlgebraicStacks.{u, t} B S hS}
    (f : 𝒳 ⟶ 𝒴) (hqc : IsQuasiCompactMorphism B S hS f)
    (hqs : AlgebraicStacks.IsQuasiSeparated B S hS f)
    (hrep : IsRepresentableByAlgebraicSpaces B S hS f.hom.hom)
    (F : StackModules B S hS .fppf 𝒳) (hF : lqcohSheafFbcFppfModules.{u, t, u} B E h S hS 𝒳 F)
    {V : BigFppfOver B S hS} (y : schemeStack.{u, t} B S hS V ⟶ 𝒴) :
    (∃ U : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u, IsAlgebraicSpace B S hS U ∧
      Nonempty (StacksRepresentableCFG.EquivalenceOver
        (twoFibreProductSquareAlgebraicStacks B S hS f y).pt.val.val.p
        (presheafOfCategories (U ⋙ typeToCat)).p)) ∧
    ∀ (U : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hU : IsAlgebraicSpace B S hS U)
      (eU : StacksRepresentableCFG.EquivalenceOver
        (twoFibreProductSquareAlgebraicStacks B S hS f y).pt.val.val.p
        (presheafOfCategories (U ⋙ typeToCat)).p) (i : ℕ),
      Nonempty ((AlgebraicGeometry.RingedToposHom.pushforwardModules
          (Space.projectionRingedToposHom B S hS (yoneda.obj V)
            (schemeStack.{u, t} B S hS V).val.val.p
            (schemeStack.{u, t} B S hS V).val.isFiberedInGroupoids
            (isAlgebraicSpace_yoneda B S hS V) (schemeStackEquivalenceOver B S hS))).obj
          ((stackModuleInverseImage B S hS .etale y).obj
            ((stackModulesEtaleComparison B S hS 𝒴).obj
              ((fppfModulesHigherDirectImage B S hS f i).obj F))) ≅
        (Space.smallEtaleHigherDirectImage
            (baseChangeSpacesHom B S hS f y (yoneda.obj V) (isAlgebraicSpace_yoneda B S hS V)
              (schemeStackEquivalenceOver B S hS) U hU eU) i).obj
          ((AlgebraicGeometry.RingedToposHom.pushforwardModules
            (Space.projectionRingedToposHom B S hS U
              (twoFibreProductSquareAlgebraicStacks B S hS f y).pt.val.val.p
              (twoFibreProductSquareAlgebraicStacks B S hS f y).pt.val.isFiberedInGroupoids
              hU eU)).obj
            ((stackModuleInverseImage B S hS .etale
              (twoFibreProductSquareAlgebraicStacks B S hS f y).fst).obj
              ((stackModulesEtaleComparison B S hS 𝒳).obj F))))

AlgebraicGeometry.Space.restrictedHigherDirectImageChartIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/RestrictedHigherDirectImage.lean, line 331. The attribute's comment: “(R^i f_F)|_{V_etale} = R^i f'_{small,}(F|_{U_etale}) for the base change f' of f along an object y : V -> Y of Y, with U = V x_Y X an ALGEBRAIC SPACE (f is representable by algebraic spaces, so U need not be a scheme) and f'_{small,} the direct image of the small etale sites of algebraic spaces; stated for every i and naturally in the complex of O_X-modules, with R^i the i-th cohomology of the total right derived direct image, which is what composes with Tag 075N. PROVED here from four inputs, two of which are themselves assumed, and all named: (1) bc, the BASE CHANGE isomorphism of the 2-cartesian square in derived form, which is Tag 075H -- carried in this library only for ABELIAN sheaves (abelianHigherDirectImageBaseChangeIso), the module-coefficient statement nonempty_moduleHigherDirectImageBaseChangeIso being itself conditional on a linearity hypothesis that is 075H's own module-coefficient assertion, so the module case is ASSUMED; (2) hDg, that the derived inverse image along the chart is computed degreewise, which is exactness of the inverse image of sheaves of modules; (3) Tag 075N, via restrictedDerivedDirectImageIso, which is now UNCONDITIONAL -- four inputs that carrier used to ask for are gone: Tag 073N itself, the 2-isomorphism of the two legs of the square, is PROVED, as AlgebraicGeometry.Space.restrictionRingedSquareInducedAlgebraicSpaces, out of invertibility of the comparison map of equation 075M (AlgebraicGeometry.Space.isIso_restrictedDirectImageComparison) and its structure-sheaf compatibility; exactness of the module-level restrictions pi_{U,}, pi_{V,} is PROVED, as AlgebraicGeometry.Space.exactFunctor_pushforwardModules_projectionRingedToposHom; Tag 093Y for degreewise f_ is no longer needed, the unit of the exact pi_{V,} being invertible; and the condition the composition criterion consumes at the leg f_small . pi_U is PROVED, as AlgebraicGeometry.Space.pushforwardComputesDerived_smallEtaleRingedToposHom, out of the unconditional Tag 0D6E for a morphism of ringed topoi; and (4) the commutation of H^i with an exact direct image, which IS proved here (derivedPushforwardOfExactCompHomologyFunctorIso). The source's remaining hypotheses are consumed rather than restated: representability of f by algebraic spaces is hF,eF,hG,eG, the presentations that make the right-hand side exist; quasi-compactness and quasi-separatedness enter only through hf; and F in LQCoh^fbc, whose role (Tag 0771 part (4)(a)) is to license computing R^i f_ in the etale topology, is built into the statement, every site here being the etale one, so the conclusion is stated for an arbitrary complex of O_X-modules and contains that case. The reduction of Tag 0771 part (3) is not needed and not used”.

Stacks 0GQH. For an object y : V ⟶ 𝒴 of 𝒴, with 𝒱 the category fibred in groupoids of that object, 𝒰 = 𝒱 ×_𝒴 𝒳 the 2-fibre product — presented by the algebraic space F = U, because f is representable by algebraic spaces — and f' : 𝒰 ⥤ 𝒱 the base change of f, inducing a morphism U ⟶ V on presenting algebraic spaces (AlgebraicGeometry.Space.inducedAlgebraicSpacesHom):

(R^i f_* ℱ)|_{V_étale} ≅ R^i f'_{small,*}(ℱ|_{U_étale}),

naturally in the complex ℱ of 𝒪_𝒳-modules. On the left, R^i f_* ℱ is H^i of the total right derived direct image RfStack, and (-)|_{V_étale} is inverse image along 𝒱 ⥤ 𝒴 followed by the restriction π_{V,*} of Stacks 073M. On the right, (-)|_{U_étale} is derived inverse image along 𝒰 ⥤ 𝒳 followed by π_{U,*}, and R^i f'_{small,*} is H^i of the total right derived direct image RfSpace of the small étale sites of the algebraic spaces U and V.

The chain is the source's: hDg and bc are its reduction to the representable case, and AlgebraicGeometry.Space.restrictedDerivedDirectImageIso together with AlgebraicGeometry.RingedToposHom.derivedPushforwardOfExactCompHomologyFunctorIso are its appeal to Stacks 075N. See the implementation notes of this file for what each hypothesis is and where the source's hypotheses on f and on ℱ are consumed.

noncomputable def restrictedHigherDirectImageChartIso
    (Dy : DerivedCategory
        (FibredSite.associatedRingedTopos B S hS p𝒴 h𝒴 .etale).Modules ⥤
      DerivedCategory (FibredSite.associatedRingedTopos B S hS q hq .etale).Modules)
    (Dy' : DerivedCategory
        (FibredSite.associatedRingedTopos B S hS p𝒳 h𝒳 .etale).Modules ⥤
      DerivedCategory (FibredSite.associatedRingedTopos B S hS p hp .etale).Modules)
    (i : ℤ)
    (hDy : Dy ⋙ DerivedCategory.homologyFunctor
          (FibredSite.associatedRingedTopos B S hS q hq .etale).Modules i ≅
        DerivedCategory.homologyFunctor
            (FibredSite.associatedRingedTopos B S hS p𝒴 h𝒴 .etale).Modules i ⋙
          Stacks.Sheaves.RingedToposModules.RingedToposHom.pullbackModules
            (FibredSite.ringedToposMorphism B S hS q p𝒴 hq h𝒴 y hy .etale).toModulesHom)
    (bc : RfStack ⋙ Dy ≅ Dy' ⋙ Rf) :
    RfStack ⋙ DerivedCategory.homologyFunctor
          (FibredSite.associatedRingedTopos B S hS p𝒴 h𝒴 .etale).Modules i ⋙
        Stacks.Sheaves.RingedToposModules.RingedToposHom.pullbackModules
            (FibredSite.ringedToposMorphism B S hS q p𝒴 hq h𝒴 y hy .etale).toModulesHom ⋙
          RingedToposHom.pushforwardModules
            (projectionRingedToposHom B S hS G q hq hG eG) ≅
      Dy' ⋙ RingedToposHom.derivedPushforwardOfExact
            (projectionRingedToposHom B S hS F p hp hF eF) ⋙
        RfSpace ⋙ DerivedCategory.homologyFunctor
          (smallEtaleRingedTopos B S hS ⟨G, hG⟩).Modules i
Tag 0GQI, a lemma

Tag 0GQI in the Stacks Project.

AlgebraicGeometry.Stack.stacks0GQI, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/AffineDirectImageFppfVanishing.lean, line 431. The attribute's comment: “all three assertions, unconditionally, for an affine 1-morphism f, on the fppf sites at module universe u: f_ restricts to LQCoh^fbc(O_X) -> LQCoh^fbc(O_Y); (1) it is exact (short exact sequences of LQCoh^fbc, read in Mod, go to short exact sequences); (2) it commutes with direct sums; (3) R^i f_ F = 0 for i > 0 and F in LQCoh^fbc(O_X)”.

Stacks 0GQI. Let f : 𝒳 ⟶ 𝒴 be an affine 1-morphism of algebraic stacks over S. The direct image restricts to a functor f_* : LQCoh^fbc(𝒪_𝒳) ⥤ LQCoh^fbc(𝒪_𝒴) (AlgebraicGeometry.Stack.affineLqcohSheafFbcPushforward, which is AlgebraicGeometry.Stack.fppfModulesPushforward on objects and morphisms by AlgebraicGeometry.Stack.affineLqcohSheafFbcPushforwardCompιIso), and

  1. f_* is exact: a sequence of LQCoh^fbc(𝒪_𝒳) which is short exact in Mod(𝒪_𝒳) goes to a sequence short exact in Mod(𝒪_𝒴);
  2. f_* commutes with direct sums (indexed by any ι : Type u);
  3. Rⁱf_* F = 0 for every i > 0 and F in LQCoh^fbc(𝒪_𝒳).

Modules are on the fppf sites at the module universe u of the schemes; LQCoh^fbc is AlgebraicGeometry.Stack.lqcohSheafFbcFppfModules.

theorem stacks0GQI :
    (∀ Sq : ShortComplex (lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳).FullSubcategory,
        (Sq.map (lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳).ι).ShortExact →
        (Sq.map (affineLqcohSheafFbcPushforward B E h S hS f hf ⋙
          (lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒴).ι)).ShortExact) ∧
      (∀ ι : Type u, PreservesColimitsOfShape (Discrete ι)
        (affineLqcohSheafFbcPushforward B E h S hS f hf)) ∧
      (∀ (i : ℕ), 0 < i → ∀ F : fppfModules B S hS 𝒳,
        lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳 F →
          IsZero ((fppfModulesHigherDirectImage B S hS f i).obj F))

AlgebraicGeometry.Stack.shortExact_map_etaleModuleDirectImage_of_isZero_higherDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/AffineDirectImageLocallyQuasicoherent.lean, line 324. The attribute's comment: “ASSERTION (1) ONLY, exactness of f_*, on the ETALE reading of LQCoh^fbc (Tag 0771 part (4)(a), the agreement with the source's default fppf reading, is absent here). It is DEDUCED from assertion (3) exactly as the source deduces it, through Tag 015D, and that deduction is the content of this declaration; the positive-degree vanishing is the hypothesis hvan and is NOT proved anywhere in this repository. Assertion (2), commutation with direct sums, and assertion (3) itself are NOT delivered by this file: see the module's implementation notes, and note that stacks0GQI_of_objectwise_of_preservesDirectSums deliberately carries NO attribute because its direct-sums conjunct is returned verbatim from its own hypothesis. Stated as preservation of short exact sequences rather than as an exact functor between the subcategories because Tag 0771 part (2) is absent, so LQCoh^fbc is not known to be a weak Serre subcategory and hence not known abelian; only the OUTER terms are required to lie in LQCoh^fbc, which is weaker than the source's hypothesis. AFFINENESS IS THE BINDER _hf AND IS CONSUMED NOWHERE: given the vanishing, this implication holds for an arbitrary 1-morphism, so it is a generalisation of the tag's assertion (1), not a weakening. The blocking input for the rest is Tag 03DW, the etale-site analogue of Tag 01XC, which is absent from the whole repository and also blocks Tags 073H and 03M9”.

Assertion (1) of Stacks 0GQI from assertion (3), which is the source's own deduction.

Let f : 𝒳 ⟶ 𝒴 be an affine 1-morphism of algebraic stacks over S and suppose the higher direct images Rⁱf_* vanish in positive degrees on LQCoh^fbc(𝒪_𝒳). Then f_* carries a short exact sequence of 𝒪_𝒳-modules on 𝒳_étale whose outer terms lie in LQCoh^fbc(𝒪_𝒳) to a short exact sequence of 𝒪_𝒴-modules on 𝒴_étale; that is, f_* is exact on LQCoh^fbc(𝒪_𝒳).

The vanishing in positive degrees is right acyclicity for f_*, by Stacks 015C and left exactness of the right adjoint f_*, and Stacks 015D part (1) turns right acyclicity of the outer terms into short exactness of the image. Affineness is what discharges hvan and is consumed nowhere in the deduction, which is why the binder is written _hf.

theorem shortExact_map_etaleModuleDirectImage_of_isZero_higherDirectImage (f : 𝒳 ⟶ 𝒴)
    (_hf : AlgebraicStacks.IsAffineHom B S hS f)
    (hvan : ∀ (i : ℕ), 0 < i → ∀ ℱ : etaleModulesOfHomSource B S hS f,
      IsLocallyQuasicoherentWithFlatBaseChangeUnivLE B E h S hS
          (CatFiberedInGroupoids.homFunctor f.hom ⋙ 𝒴.val.val.p)
          (isFiberedInGroupoids_homFunctor_comp B S hS f.hom) ℱ.val →
        IsZero ((etaleModuleHigherDirectImage B S hS f i).obj ℱ))
    (Sq : ShortComplex (etaleModulesOfHomSource B S hS f)) (hSq : Sq.ShortExact)
    (h₁ : IsLocallyQuasicoherentWithFlatBaseChangeUnivLE B E h S hS
      (CatFiberedInGroupoids.homFunctor f.hom ⋙ 𝒴.val.val.p)
      (isFiberedInGroupoids_homFunctor_comp B S hS f.hom) Sq.X₁.val)
    (h₃ : IsLocallyQuasicoherentWithFlatBaseChangeUnivLE B E h S hS
      (CatFiberedInGroupoids.homFunctor f.hom ⋙ 𝒴.val.val.p)
      (isFiberedInGroupoids_homFunctor_comp B S hS f.hom) Sq.X₃.val) :
    (Sq.map (etaleModuleDirectImage B S hS f)).ShortExact
Sources

Section103.9 Parasitic modules#

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

Tag 0773, a definition

Tag 0773 in the Stacks Project.

AlgebraicGeometry.Stack.IsParasitic, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/ParasiticModules.lean, line 64. The attribute's comment: “parasitic”.

Stacks 0773. A presheaf of modules over the structure sheaf of one of the sites associated with an algebraic stack 𝒳 is parasitic when its module of sections at every flat object of 𝒳 vanishes — an object being flat, as in Stacks 0787, when the 1-morphism it names out of the scheme it lies over is flat.

abbrev IsParasitic
    (F : PresheafOfModules.{t}
      (FibredSite.ringStructureSheafCore B S hS 𝒳.val.val.p
        𝒳.val.isFiberedInGroupoids τ).obj) : Prop
Tag 0774, a lemma

Tag 0774 in the Stacks Project.

AlgebraicGeometry.Stack.isParasitic_of_isFlat_isLfp_jointlySurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/ParasiticFlatDescent.lean, line 89. The attribute's comment: “part (4): an fppf sheaf of modules whose inverse images along a jointly surjective family of flat, locally finitely presented 1-morphisms of algebraic stacks are all parasitic is parasitic”.

Stacks 0774 (4). Let f j : 𝒳 j ⟶ 𝒴 be a jointly surjective family of flat, locally finitely presented 1-morphisms of algebraic stacks over S, and let ℱ be a sheaf of 𝒪_𝒴-modules on the fppf site of 𝒴. If every inverse image (f j)^*ℱ is parasitic, then ℱ is parasitic.

At a flat object y of 𝒴 the covering of AlgebraicGeometry.Stack.exists_fppfCovering_family_flatObject_lift supplies an fppf covering family of y by objects f (a i)(x_i) with x_i a flat object of 𝒳 (a i); the sections of ℱ there are the sections of (f (a i))^*ℱ at x_i, which vanish, and a sheaf is separated.

theorem isParasitic_of_isFlat_isLfp_jointlySurjective {J : Type v}
    {𝒳 : J → AlgebraicStacks.{u, w} B S hS} {𝒴 : AlgebraicStacks.{u, w} B S hS}
    (f : ∀ j, 𝒳 j ⟶ 𝒴)
    (hflat : ∀ j, AlgebraicStacks.IsFlat B S hS (f j))
    (hlfp : ∀ j, AlgebraicStacks.IsLocallyOfFinitePresentation B S hS (f j))
    (hjs : (Set.univ : Set (AlgebraicStacks.points B S hS 𝒴)) =
      ⋃ j, Set.range (AlgebraicStacks.pointsMap B S hS (f j)))
    (F : SheafOfModules.{t}
      (FibredSite.ringStructureSheafCore B S hS 𝒴.val.val.p
        𝒴.val.isFiberedInGroupoids SiteKind.fppf))
    (hF : ∀ j, IsParasitic B S hS (𝒳 j) SiteKind.fppf
      ((modulePresheafPullbackOfHom.{u, w, t} B S hS (f j) SiteKind.fppf).obj F.val)) :
    IsParasitic B S hS 𝒴 SiteKind.fppf F.val

AlgebraicGeometry.Stack.isParasitic_modulePresheafPullbackOfHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/ParasiticPullback.lean, line 127. The attribute's comment: “part (1): the inverse image of a parasitic presheaf of modules along a flat 1-morphism of algebraic stacks is parasitic”.

Stacks 0774 (1). If F is a parasitic presheaf of 𝒪_𝒳-modules and g : 𝒴 ⟶ 𝒳 is a flat 1-morphism of algebraic stacks, then the inverse image g^*F is a parasitic presheaf of 𝒪_𝒴-modules.

Let y be an object of 𝒴 lying over a scheme V for which y : V → 𝒴 is flat. Then g y : V → 𝒴 → 𝒳 is flat, being a composite of flat 1-morphisms (Stacks 06PX), so F vanishes at g y by hypothesis. The sections of g^*F at y are the sections of F at g y, whence the conclusion.

theorem isParasitic_modulePresheafPullbackOfHom
    (hg : AlgebraicStacks.IsFlat B S hS g)
    (F : PresheafOfModules.{t}
      (FibredSite.ringStructureSheafCore B S hS 𝒳.val.val.p
        𝒳.val.isFiberedInGroupoids τ).obj)
    (hF : IsParasitic B S hS 𝒳 τ F) :
    IsParasitic B S hS 𝒴 τ
      ((modulePresheafPullbackOfHom.{u, w, t} B S hS g τ).obj F)

AlgebraicGeometry.Stack.isParasitic_of_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/ParasiticSerreSubcategory.lean, line 181. The attribute's comment: “part (2)(b), the closure under submodules: a submodule of a parasitic module is parasitic”.

Stacks 0774 (2)(b), the closure under submodules. A submodule of a parasitic module on one of the sites associated with an algebraic stack is parasitic.

It is immediate from the definition, as the source says: a monomorphism of sheaves of modules is injective on sections, so at a flat object the sections of the submodule inject into the vanishing sections of the ambient module.

theorem isParasitic_of_mono
    {F' F : SheafOfModules.{t}
      (FibredSite.ringStructureSheafCore B S hS 𝒳.val.val.p
        𝒳.val.isFiberedInGroupoids τ)}
    (i : F' ⟶ F) [Mono i] (hF : IsParasitic B S hS 𝒳 τ F.val) :
    IsParasitic B S hS 𝒳 τ F'.val

AlgebraicGeometry.Stack.isParasitic_X₂_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/ParasiticSerreSubcategory.lean, line 205. The attribute's comment: “part (2)(b), the closure under extensions: the middle term of a short exact sequence of modules whose outer terms are parasitic is parasitic”.

Stacks 0774 (2)(b), the closure under extensions. Given a short exact sequence 0 → F₁ → F₂ → F₃ → 0 of modules on one of the sites associated with an algebraic stack, with F₁ and F₃ parasitic, the module F₂ is parasitic.

This is the source's "evaluate on x lying over a scheme flat over 𝒳": at a flat object the sections of F₁ and of F₃ vanish, and taking sections is left exact, so the sections of F₂ vanish too.

theorem isParasitic_X₂_of_shortExact
    {Sq : ShortComplex (SheafOfModules.{t}
      (FibredSite.ringStructureSheafCore B S hS 𝒳.val.val.p
        𝒳.val.isFiberedInGroupoids τ))}
    (hSq : Sq.ShortExact)
    (h₁ : IsParasitic B S hS 𝒳 τ Sq.X₁.val) (h₃ : IsParasitic B S hS 𝒳 τ Sq.X₃.val) :
    IsParasitic B S hS 𝒳 τ Sq.X₂.val

AlgebraicGeometry.Stack.isParasitic_of_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/ParasiticSerreSubcategory.lean, line 237. The attribute's comment: “part (2)(b), the closure under quotients: a quotient of a parasitic module is parasitic”.

Stacks 0774 (2)(b), the closure under quotients. If p : F ⟶ G is an epimorphism of modules on one of the sites associated with an algebraic stack and F is parasitic, then G is parasitic.

An epimorphism of sheaves of modules is locally surjective, so this is AlgebraicGeometry.Stack.isParasitic_of_isLocallySurjective: at a flat object every section of G comes from a section of F on a covering, and that covering may be refined by one whose sources are again flat objects, where F vanishes.

theorem isParasitic_of_epi
    {F G : SheafOfModules.{t}
      (FibredSite.ringStructureSheafCore B S hS 𝒳.val.val.p
        𝒳.val.isFiberedInGroupoids τ)}
    (p : F ⟶ G) [Epi p] (hF : IsParasitic B S hS 𝒳 τ F.val) :
    IsParasitic B S hS 𝒳 τ G.val

AlgebraicGeometry.Stack.isSerreClass_parasiticModules, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/ParasiticSerreSubcategory.lean, line 255. The attribute's comment: “part (2)(b): the parasitic modules are a Serre subcategory of Mod(𝒳_τ, 𝒪_𝒳)”.

Stacks 0774 (2)(b). The full subcategory of Mod(𝒳_τ, 𝒪_𝒳) consisting of the parasitic modules is a Serre subcategory: it contains a zero object and is closed under submodules, under quotients and under extensions, which are the four instances above.

instance isSerreClass_parasiticModules :
    (parasiticModules.{u, w, t} B S hS 𝒳 τ).IsSerreClass

AlgebraicGeometry.Stack.isParasitic_sheafification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/ParasiticSheafification.lean, line 133. The attribute's comment: “part (2)(a): the τ-sheafification of a parasitic presheaf of modules is parasitic”.

Stacks 0774 (2)(a). The τ-sheafification of a parasitic presheaf of 𝒪_𝒳-modules is parasitic, for each of the five topologies τ of Stacks 06TP.

The map from a presheaf of modules to its sheafification is locally surjective, so this is AlgebraicGeometry.Stack.isParasitic_of_isLocallySurjective.

theorem isParasitic_sheafification
    (F : PresheafOfModules.{t}
      (FibredSite.ringStructureSheafCore B S hS 𝒳.val.val.p
        𝒳.val.isFiberedInGroupoids τ).obj)
    (hF : IsParasitic B S hS 𝒳 τ F) :
    IsParasitic B S hS 𝒳 τ
      ((PresheafOfModules.sheafification.{t}
        (𝟙 (FibredSite.ringStructureSheafCore B S hS 𝒳.val.val.p
          𝒳.val.isFiberedInGroupoids τ).obj)).obj F).val

AlgebraicGeometry.Stack.isParasitic_of_isSmooth_jointlySurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/ParasiticSmoothDescent.lean, line 186. The attribute's comment: “part (3): an étale sheaf of modules whose inverse images along a jointly surjective family of smooth 1-morphisms of algebraic stacks are all parasitic is parasitic”.

Stacks 0774 (3). Let f j : 𝒳 j ⟶ 𝒴 be a jointly surjective family of smooth 1-morphisms of algebraic stacks over S, and let ℱ be a sheaf of 𝒪_𝒴-modules on the étale site of 𝒴. If every inverse image (f j)^*ℱ is parasitic, then ℱ is parasitic.

At a flat object y of 𝒴, every point of the scheme y lies over is hit by a smooth morphism m of the site carrying a lift of y to some 𝒳 j which is a flat object there (AlgebraicGeometry.Stack.exists_flatObject_lift_of_isSmooth_at_point), so the sections of ℱ restrict to zero along the comparison morphism. Refining m by an étale morphism factoring through it (Stacks 055U) and taking a cartesian lift of the comparison morphism gives an étale covering family of y along every member of which the sections of ℱ restrict to zero; ℱ is an étale sheaf, hence separated, so they vanish.

theorem isParasitic_of_isSmooth_jointlySurjective {J : Type v}
    {𝒳 : J → AlgebraicStacks.{u, w} B S hS} {𝒴 : AlgebraicStacks.{u, w} B S hS}
    (f : ∀ j, 𝒳 j ⟶ 𝒴)
    (hsmooth : ∀ j, AlgebraicStacks.IsSmooth B S hS (f j))
    (hjs : (Set.univ : Set (AlgebraicStacks.points B S hS 𝒴)) =
      ⋃ j, Set.range (AlgebraicStacks.pointsMap B S hS (f j)))
    (F : SheafOfModules.{t}
      (FibredSite.ringStructureSheafCore B S hS 𝒴.val.val.p
        𝒴.val.isFiberedInGroupoids SiteKind.etale))
    (hF : ∀ j, IsParasitic B S hS (𝒳 j) SiteKind.etale
      ((modulePresheafPullbackOfHom.{u, w, t} B S hS (f j) SiteKind.etale).obj F.val)) :
    IsParasitic B S hS 𝒴 SiteKind.etale F.val
Tag 0775, a lemma

Tag 0775 in the Stacks Project.

AlgebraicGeometry.Stack.isZero_fppfModuleCohomology_of_isParasitic_atSchemeUniverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/ParasiticCohomologyVanishingAtSchemeUniverse.lean, line 65. The attribute's comment: “part (1) for τ = fppf at the module universe u of the schemes: H^i(𝒳, ℱ) = 0 for a parasitic ℱ, with H^i = Ext^i(𝒪_𝒳, -) as in FlatFppf.fppfModuleCohomology”.

Stacks 0775 part (1), for the fppf topology, at the module universe u of the schemes. Let 𝒳 be an algebraic stack and ℱ a parasitic sheaf of 𝒪_𝒳-modules (Stacks 0773). Then H^i(𝒳, ℱ) = 0 for every i, where H^i(𝒳, -) is AlgebraicGeometry.Stack.FlatFppf.fppfModuleCohomology, Ext^i out of the structure sheaf, in any universe t of Ext-groups.

The instance argument HasExt.{t} is not a hypothesis on ℱ: fppfModuleCohomology.{u, w, t} is only defined in its presence. At t = u it is supplied by the Grothendieck abelian structure (AlgebraicGeometry.Stack.isGrothendieckAbelian_fppfModules), which is AlgebraicGeometry.Stack.isZero_fppfModuleCohomology_of_isParasitic_ofGrothendieck.

By AlgebraicGeometry.Stack.fppfModuleCohomologyULiftIso this is the vanishing of Ext^i out of the lifted structure sheaf of the universe lift of ℱ, which is parasitic as ℱ is, and that is AlgebraicGeometry.Stack.isZero_ext_uliftUnit_of_isParasitic.

theorem isZero_fppfModuleCohomology_of_isParasitic_atSchemeUniverse
    {𝒳 : AlgebraicStacks.{u, w} B S hS} [HasExt.{t} (fppfModules B S hS 𝒳)]
    (N : fppfModules B S hS 𝒳) (hN : IsParasitic B S hS 𝒳 .fppf N.val) (i : ℕ) :
    IsZero ((FlatFppf.fppfModuleCohomology.{u, w, t} B S hS 𝒳 i).obj N)

AlgebraicGeometry.Stack.isZero_ext_unit_of_isParasitic_atSchemeUniverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/ParasiticCohomologyVanishingAtSchemeUniverse.lean, line 109. The attribute's comment: “part (1) for τ the étale or the fppf topology, at the module universe u of the schemes: H^i_τ(𝒳, ℱ) = Ext^i(𝒪_𝒳, ℱ) = 0 for a parasitic ℱ”.

Stacks 0775 part (1), for τ the étale or the fppf topology, at the module universe u of the schemes. Let 𝒳 be an algebraic stack and ℱ a parasitic sheaf of 𝒪_𝒳-modules on 𝒳_τ (Stacks 0773). Then H^i_τ(𝒳, ℱ) = Ext^i(𝒪_𝒳, ℱ) = 0 for every i, for Ext-groups in any universe t.

The instance argument HasExt.{t} is not a hypothesis on ℱ: it is what makes Ext-groups in the universe t exist at all, and it is always available at t = u, the category of modules being Grothendieck abelian (AlgebraicGeometry.Stack.isGrothendieckAbelian_moduleRingSheaf, see AlgebraicGeometry.Stack.isZero_ext_unit_of_isParasitic_atSchemeUniverse_ofGrothendieck).

By AlgebraicGeometry.Stack.isZero_ext_unit_iff_isZero_ext_uliftUnit this is the vanishing of Ext^i out of the lifted structure sheaf of the universe lift of ℱ, which is parasitic as ℱ is, and that is AlgebraicGeometry.Stack.isZero_ext_uliftUnit_of_isParasitic.

theorem isZero_ext_unit_of_isParasitic_atSchemeUniverse {τ : SiteKind}
    (hτ : τ = .etale ∨ τ = .fppf) {𝒳 : AlgebraicStacks.{u, w} B S hS}
    [HasExt.{t} (SheafOfModules.{u}
      (Stacks.RelativeCech.moduleRingSheaf B S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids τ))]
    (N : SheafOfModules.{u}
      (Stacks.RelativeCech.moduleRingSheaf B S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids τ))
    (hN : IsParasitic B S hS 𝒳 τ N.val) (i : ℕ) :
    IsZero ((extFunctorObj.{t} (SheafOfModules.unit _) i).obj N)

AlgebraicGeometry.Stack.isZero_ext_uliftUnit_of_isParasitic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/ParasiticFlatSubsiteCohomology.lean, line 218. The attribute's comment: “part (1), for τ the étale or the fppf topology, with no hypothesis: H^i_τ(𝒳, ℱ) = 0 for a parasitic ℱ, at the module universe u + 1 of the objects of the site”.

Stacks 0775 part (1). Let 𝒳 be an algebraic stack, let τ be the étale or the fppf topology, and let ℱ be a parasitic sheaf of 𝒪_𝒳-modules on 𝒳_τ (Stacks 0773). Then H^i_τ(𝒳, ℱ) = 0 for all i.

The modules have their sections in the universe u + 1 of the objects of the site, where the structure sheaf 𝒪_𝒳 is a module through its universe lift Stacks.SheafOfModules.uliftUnit and H^i_τ(𝒳, -) = Ext^i(𝒪_𝒳, -), in any universe t of Ext-groups. By Stacks 03FD this is the cohomology of the underlying abelian sheaf (Stacks.Cohomology.ULiftUnitComparison.extULiftUnitIso), which vanishes because that sheaf vanishes at the flat objects (AlgebraicGeometry.Stack.isZero_functorH_of_subsingleton_flatObject, from the cohomology comparison of Stacks 07AK along the inclusion of the flat objects).

theorem isZero_ext_uliftUnit_of_isParasitic (hτ : τ = .etale ∨ τ = .fppf)
    [HasExt.{t} (SheafOfModules.{u + 1}
      (FibredSite.ringStructureSheafCore B S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids τ))]
    (F : SheafOfModules.{u + 1}
      (FibredSite.ringStructureSheafCore B S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids τ))
    (hF : IsParasitic B S hS 𝒳 τ F.val) (i : ℕ) :
    IsZero ((extFunctorObj.{t} (Stacks.SheafOfModules.uliftUnit.{u + 1}
      (FibredSite.ringStructureSheafCore B S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids τ))
        i).obj F)

AlgebraicGeometry.Stack.isParasitic_moduleSheafHigherDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/ParasiticHigherDirectImage.lean, line 407. The attribute's comment: “part (2), for τ the étale or the fppf topology, at the module universe u + 1 of the objects of the site: R^if_*ℱ is parasitic for a parasitic ℱ”.

Stacks 0775 (2) at the module universe u + 1 of the objects of the site. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks, τ the étale or the fppf topology, and ℱ a parasitic sheaf of 𝒪_𝒳-modules on 𝒳_τ (Stacks 0773). Then every higher direct image R^nf_*ℱ (Stacks 06WE, AlgebraicGeometry.Stack.moduleSheafHigherDirectImage) is a parasitic sheaf of 𝒪_𝒴-modules.

This is AlgebraicGeometry.Stack.isParasitic_rightDerived_stackModuleDirectImageSucc moved along AlgebraicGeometry.AlgebraicStacks.moduleDirectImageRightDerivedIso.

theorem isParasitic_moduleSheafHigherDirectImage (hτ : τ = .etale ∨ τ = .fppf)
    (N : SheafOfModules.{u + 1} (Stacks.RelativeCech.moduleRingSheaf B S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids τ)) (hN : IsParasitic B S hS 𝒳 τ N.val) (n : ℕ) :
    IsParasitic B S hS 𝒴 τ ((moduleSheafHigherDirectImage.{u, u + 1, u, u + 1, u} B S hS
      𝒳.val.val.p 𝒴.val.val.p 𝒳.val.isFiberedInGroupoids 𝒴.val.isFiberedInGroupoids
      (CatFiberedInGroupoids.homFunctor k.hom) (CatFiberedInGroupoids.homFunctor_comp_p k.hom)
      (B.baseTopology τ) (B.baseTopology_le_topology τ) n).obj N).val

AlgebraicGeometry.Stack.isParasitic_stackModuleHigherDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/ParasiticHigherDirectImage.lean, line 431. The attribute's comment: “part (2), for τ the étale or the fppf topology, at the module universe u of the schemes: R^if_*ℱ is parasitic for a parasitic ℱ”.

Stacks 0775 (2), for τ the étale or the fppf topology, at the module universe u of the schemes. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks and ℱ a parasitic sheaf of 𝒪_𝒳-modules on 𝒳_τ (Stacks 0773). Then every higher direct image R^nf_*ℱ (AlgebraicGeometry.Stack.stackModuleHigherDirectImage) is parasitic.

The universe lift carries R^nf_*ℱ to R^nf_* at u + 1 of the lift of ℱ (AlgebraicGeometry.Stack.stackModuleHigherDirectImageULiftIso), the lift of a parasitic module is parasitic, and at u + 1 this is AlgebraicGeometry.Stack.isParasitic_moduleSheafHigherDirectImage.

theorem isParasitic_stackModuleHigherDirectImage (hτ : τ = .etale ∨ τ = .fppf)
    (N : SheafOfModules.{u} (Stacks.RelativeCech.moduleRingSheaf B S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids τ)) (hN : IsParasitic B S hS 𝒳 τ N.val) (n : ℕ) :
    IsParasitic B S hS 𝒴 τ ((stackModuleHigherDirectImage B S hS k τ n).obj N).val

AlgebraicGeometry.Stack.isParasitic_fppfModulesHigherDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/ParasiticHigherDirectImage.lean, line 446. The attribute's comment: “part (2) for τ = fppf at the module universe u of the schemes: R^if_ℱ is parasitic for a parasitic ℱ, with R^if_ as in fppfModulesHigherDirectImage”.

Stacks 0775 (2) for the fppf topology at the module universe u: for every 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks, the higher direct images AlgebraicGeometry.Stack.fppfModulesHigherDirectImage of a parasitic module are parasitic. This is AlgebraicGeometry.Stack.isParasitic_stackModuleHigherDirectImage at τ = fppf.

theorem isParasitic_fppfModulesHigherDirectImage
    (N : SheafOfModules.{u} (Stacks.RelativeCech.moduleRingSheaf B S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids .fppf)) (hN : IsParasitic B S hS 𝒳 .fppf N.val) (n : ℕ) :
    IsParasitic B S hS 𝒴 .fppf ((fppfModulesHigherDirectImage B S hS k n).obj N).val
Tag 0776, a lemma

Tag 0776 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.tfae_exact_isParasitic_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/ExactParasiticHomology.lean, line 514.

Stacks 0776. Let 𝒳 be an algebraic stack and let α : 𝓕 ⟶ 𝓖 and β : 𝓖 ⟶ 𝓗 be maps in QCoh(𝒪_𝒳) with β ∘ α = 0. The following are equivalent:

  1. in the abelian category QCoh(𝒪_𝒳) the complex 𝓕 ⟶ 𝓖 ⟶ 𝓗 is exact at 𝓖;
  2. Ker(β)/Im(α) computed in Mod(𝒳_étale, 𝒪_𝒳) is parasitic;
  3. Ker(β)/Im(α) computed in Mod(𝒳_fppf, 𝒪_𝒳) is parasitic.

The abelian structure of QCoh(𝒪_𝒳) is AlgebraicGeometry.Stack.AlgebraicStacks.instAbelianQuasicoherentModules; Ker(β)/Im(α) computed in Mod(𝒳_τ, 𝒪_𝒳) is the homology of the complex 𝓕 ⟶ 𝓖 ⟶ 𝓗 regarded as a complex of sheaves of modules on the site of τ (Stacks 06TP), and parasitic is Stacks 0773.

theorem tfae_exact_isParasitic_homology {F G H : quasicoherentModules B S hS 𝒳} (α : F ⟶ G)
    (β : G ⟶ H) (w : α ≫ β = 0) :
    List.TFAE [(ShortComplex.mk α β w).Exact,
      IsParasitic B S hS 𝒳 .etale ((ShortComplex.mk α β w).map
        (FibredSite.toSiteModules.{u, u + 1, u, u} B S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids
          .etale)).homology.val,
      IsParasitic B S hS 𝒳 .fppf ((ShortComplex.mk α β w).map
        (FibredSite.toSiteModules.{u, u + 1, u, u} B S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids
          .fppf)).homology.val]
Sources

Section103.10 Quasi-coherent modules#

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

Tag 0778, a lemma

Tag 0778 in the Stacks Project.

AlgebraicGeometry.Stack.flatBaseChangeQuasicoherator, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Coherator.lean, line 257. The attribute's comment: “the right adjoint Q : LQCoh^fbc(𝒪_𝒳) ⥤ QCoh(𝒪_𝒳)”.

The coherator on LQCoh^fbc(𝒪_𝒳). The right adjoint of the inclusion i : QCoh(𝒪_𝒳) → LQCoh^fbc(𝒪_𝒳): it sends a locally quasi-coherent module with the flat base change property to the terminal quasi-coherent module equipped with a map to it.

def flatBaseChangeQuasicoherator
    (hinc : ∀ F : FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS p hp,
      IsLocallyQuasicoherentWithFlatBaseChange B E h S hS p hp
        ((FibredSite.toSiteModules.{u, u + 1, u, u} B S hS p hp .etale).obj F).val)
    (hclosed : SheafOfModules.ClosedUnderColimitsOfSize.{u, u + 1, u, u, u}
      (FibredSite.ringStructureSheafCore B S hS p hp .fppf))
    (hpres : PreservesColimitsOfSize.{u, u} (quasicoherentToFlatBaseChange B E h S hS p hp hinc))
    (hls : LocallySmall.{u} (FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS p hp))
    (hlsD : LocallySmall.{u}
      (locallyQuasicoherentFlatBaseChangeModules.{u, u + 1, u} B E h S hS p hp))
    (hwp : WellPowered.{u} (FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS p hp)ᵒᵖ)
    (hsep : HasSeparator (FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS p hp)) :
    locallyQuasicoherentFlatBaseChangeModules.{u, u + 1, u} B E h S hS p hp ⥤
      FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS p hp

AlgebraicGeometry.Stack.flatBaseChangeQuasicoheratorAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Coherator.lean, line 279. The attribute's comment: “the adjunction between the inclusion and the right adjoint”.

The coherator on LQCoh^fbc(𝒪_𝒳) is right adjoint to the inclusion. The adjunction is the universal property of the terminal objects the coherator is built from.

def flatBaseChangeQuasicoheratorAdjunction
    (hinc : ∀ F : FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS p hp,
      IsLocallyQuasicoherentWithFlatBaseChange B E h S hS p hp
        ((FibredSite.toSiteModules.{u, u + 1, u, u} B S hS p hp .etale).obj F).val)
    (hclosed : SheafOfModules.ClosedUnderColimitsOfSize.{u, u + 1, u, u, u}
      (FibredSite.ringStructureSheafCore B S hS p hp .fppf))
    (hpres : PreservesColimitsOfSize.{u, u} (quasicoherentToFlatBaseChange B E h S hS p hp hinc))
    (hls : LocallySmall.{u} (FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS p hp))
    (hlsD : LocallySmall.{u}
      (locallyQuasicoherentFlatBaseChangeModules.{u, u + 1, u} B E h S hS p hp))
    (hwp : WellPowered.{u} (FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS p hp)ᵒᵖ)
    (hsep : HasSeparator (FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS p hp)) :
    quasicoherentToFlatBaseChange B E h S hS p hp hinc ⊣
      flatBaseChangeQuasicoherator B E h S hS p hp hinc hclosed hpres hls hlsD hwp hsep

AlgebraicGeometry.Stack.flatBaseChangeQuasicoheratorCompInclusionIsoId, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Coherator.lean, line 301. The attribute's comment: “the composite of the right adjoint with the inclusion is the identity functor”.

Q ∘ i is the identity functor of QCoh(𝒪_𝒳), for the coherator Q on LQCoh^fbc(𝒪_𝒳) and the inclusion i.

def flatBaseChangeQuasicoheratorCompInclusionIsoId
    (hinc : ∀ F : FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS p hp,
      IsLocallyQuasicoherentWithFlatBaseChange B E h S hS p hp
        ((FibredSite.toSiteModules.{u, u + 1, u, u} B S hS p hp .etale).obj F).val)
    (hclosed : SheafOfModules.ClosedUnderColimitsOfSize.{u, u + 1, u, u, u}
      (FibredSite.ringStructureSheafCore B S hS p hp .fppf))
    (hpres : PreservesColimitsOfSize.{u, u} (quasicoherentToFlatBaseChange B E h S hS p hp hinc))
    (hls : LocallySmall.{u} (FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS p hp))
    (hlsD : LocallySmall.{u}
      (locallyQuasicoherentFlatBaseChangeModules.{u, u + 1, u} B E h S hS p hp))
    (hwp : WellPowered.{u} (FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS p hp)ᵒᵖ)
    (hsep : HasSeparator (FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS p hp)) :
    quasicoherentToFlatBaseChange B E h S hS p hp hinc ⋙
        flatBaseChangeQuasicoherator B E h S hS p hp hinc hclosed hpres hls hlsD hwp hsep ≅
      𝟭 (FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS p hp)

AlgebraicGeometry.Stack.AlgebraicStacks.lqcohFbcCoherator, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatBaseChangeCoherator.lean, line 68. The attribute's comment: “the right adjoint Q : LQCoh^fbc(𝒪_𝒳) ⥤ QCoh(𝒪_𝒳) of the inclusion”.

Stacks 0778: the right adjoint Q : LQCoh^fbc(𝒪_𝒳) ⥤ QCoh(𝒪_𝒳).

abbrev lqcohFbcCoherator :
    (lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳).FullSubcategory ⥤
      quasicoherentModules B S hS 𝒳

AlgebraicGeometry.Stack.AlgebraicStacks.lqcohFbcCoheratorAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatBaseChangeCoherator.lean, line 75. The attribute's comment: “the inclusion QCoh(𝒪_𝒳) → LQCoh^fbc(𝒪_𝒳) is left adjoint to Q”.

Stacks 0778: Q is right adjoint to the inclusion i.

def lqcohFbcCoheratorAdjunction :
    quasicoherentToLqcohFbc B E h S hS 𝒳 ⊣ lqcohFbcCoherator B E h S hS 𝒳

AlgebraicGeometry.Stack.AlgebraicStacks.lqcohFbcCoheratorCompIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatBaseChangeCoherator.lean, line 81. The attribute's comment: “Q ∘ i is the identity functor”.

Stacks 0778: Q ∘ i is the identity functor of QCoh(𝒪_𝒳).

def lqcohFbcCoheratorCompIso :
    quasicoherentToLqcohFbc B E h S hS 𝒳 ⋙ lqcohFbcCoherator B E h S hS 𝒳 ≅
      𝟭 (quasicoherentModules B S hS 𝒳)

AlgebraicGeometry.Stack.AlgebraicStacks.lqcohFbcCoheratorAdjunctionAndCompIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatBaseChangeCoherator.lean, line 90. The attribute's comment: “the whole statement: i has a right adjoint Q, and Q ∘ i is the identity”.

Stacks 0778, the whole statement. For an algebraic stack 𝒳, the inclusion i : QCoh(𝒪_𝒳) ⥤ LQCoh^fbc(𝒪_𝒳) has the right adjoint Q, and Q ∘ i is the identity functor of QCoh(𝒪_𝒳).

def lqcohFbcCoheratorAdjunctionAndCompIso :
    (quasicoherentToLqcohFbc B E h S hS 𝒳 ⊣ lqcohFbcCoherator B E h S hS 𝒳) ×
      (quasicoherentToLqcohFbc B E h S hS 𝒳 ⋙ lqcohFbcCoherator B E h S hS 𝒳 ≅
        𝟭 (quasicoherentModules B S hS 𝒳))
Tag 0779, a lemma

Tag 0779 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isZero_coherator_obj_iff_isParasitic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/CoheratorCanonical.lean, line 94. The attribute's comment: “part (1): the kernel of Q on LQCoh^fbc(𝒪_𝒳) is exactly its parasitic objects”.

Stacks 0779 (1). An object of LQCoh^fbc(𝒪_𝒳) is killed by the coherator Q : Mod(𝒪_𝒳) → QCoh(𝒪_𝒳) of Stacks 0778 exactly when it is parasitic: the kernel of Q on LQCoh^fbc(𝒪_𝒳) is exactly the collection of its parasitic objects.

theorem isZero_coherator_obj_iff_isParasitic (F : Stack.fppfModules B S hS 𝒳)
    (hF : lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳 F) :
    IsZero ((coherator B S hS 𝒳).obj F) ↔ IsParasitic B S hS 𝒳 .fppf F.val

AlgebraicGeometry.Stack.AlgebraicStacks.isParasitic_kernel_and_cokernel_coheratorAdjunction_counit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/CoheratorCanonical.lean, line 103. The attribute's comment: “part (2): the kernel and the cokernel of the adjunction map Q(F) → F are parasitic, for F in LQCoh^fbc(𝒪_𝒳)”.

Stacks 0779 (2). For 𝓕 in LQCoh^fbc(𝒪_𝒳) both the kernel and the cokernel of the adjunction map Q(𝓕) ⟶ 𝓕 are parasitic.

theorem isParasitic_kernel_and_cokernel_coheratorAdjunction_counit
    (F : Stack.fppfModules B S hS 𝒳) (hF : lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳 F) :
    IsParasitic B S hS 𝒳 .fppf (kernel ((coheratorAdjunction B S hS 𝒳).counit.app F)).val ∧
      IsParasitic B S hS 𝒳 .fppf
        (cokernel ((coheratorAdjunction B S hS 𝒳).counit.app F)).val

AlgebraicGeometry.Stack.AlgebraicStacks.preservesLimitsOfSize_lqcohSheafFbc_ι_comp_coherator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/CoheratorCanonical.lean, line 148. The attribute's comment: “part (3): Q on LQCoh^fbc(𝒪_𝒳) commutes with all limits”.

Stacks 0779 (3), limits: the coherator Q : LQCoh^fbc(𝒪_𝒳) → QCoh(𝒪_𝒳) commutes with all limits, being right adjoint to the inclusion QCoh(𝒪_𝒳) → LQCoh^fbc(𝒪_𝒳).

theorem preservesLimitsOfSize_lqcohSheafFbc_ι_comp_coherator :
    PreservesLimitsOfSize.{u, u}
      ((lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳).ι ⋙ coherator B S hS 𝒳)

AlgebraicGeometry.Stack.AlgebraicStacks.preservesColimitsOfShape_lqcohSheafFbc_ι_comp_coherator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/CoheratorCanonical.lean, line 156. The attribute's comment: “part (3): Q on LQCoh^fbc(𝒪_𝒳) commutes with all colimits”.

Stacks 0779 (3), colimits: the coherator Q : LQCoh^fbc(𝒪_𝒳) → QCoh(𝒪_𝒳) commutes with all colimits of u-small shapes, which are computed in Mod(𝒪_𝒳).

theorem preservesColimitsOfShape_lqcohSheafFbc_ι_comp_coherator (J : Type u) [Category.{u} J] :
    PreservesColimitsOfShape J
      ((lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳).ι ⋙ coherator B S hS 𝒳)

AlgebraicGeometry.Stack.AlgebraicStacks.preservesFiniteLimits_and_preservesFiniteColimits_lqcohSheafFbc_ι_comp_coherator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/CoheratorCanonical.lean, line 164. The attribute's comment: “part (3): Q is exact on LQCoh^fbc(𝒪_𝒳)”.

Stacks 0779 (3), exactness: the coherator Q : LQCoh^fbc(𝒪_𝒳) → QCoh(𝒪_𝒳) is exact, it preserves finite limits and finite colimits.

theorem preservesFiniteLimits_and_preservesFiniteColimits_lqcohSheafFbc_ι_comp_coherator :
    PreservesFiniteLimits
        ((lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳).ι ⋙ coherator B S hS 𝒳) ∧
      PreservesFiniteColimits
        ((lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳).ι ⋙ coherator B S hS 𝒳)

AlgebraicGeometry.Stack.preservesLimitsOfSize_flatBaseChangeQuasicoherator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/CoheratorParasiticKernel.lean, line 231. The attribute's comment: “part (3): Q commutes with all limits”.

Stacks 0779, part (3): the coherator commutes with all limits. This is the one assertion of Stacks 0779 which needs nothing beyond the adjunction of Stacks 0778: Q is a right adjoint, and a right adjoint preserves all limits.

theorem preservesLimitsOfSize_flatBaseChangeQuasicoherator :
    PreservesLimitsOfSize.{vJ, uJ}
      (flatBaseChangeQuasicoherator B E h S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids
        hinc hclosed hpres hls hlsD hwp hsep)

AlgebraicGeometry.Stack.isZero_flatBaseChangeQuasicoherator_iff_isParasitic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/CoheratorParasiticKernel.lean, line 279. The attribute's comment: “part (1): the kernel of Q is exactly the parasitic objects, in both directions, over the chart data of the construction of Stacks 0778”.

Stacks 0779, part (1). An object 𝓕 of LQCoh^fbc(𝒪_𝒳) is in the kernel of the coherator Q of Stacks 0778 if and only if it is parasitic (Stacks 0773). Both directions are proved: the statement is an equality of the two collections.

The counit of the adjunction identifies r (i (Q 𝓕)) with r 𝓕, and i ⋙ r is an equivalence and so reflects zero objects; so Q 𝓕 = 0 if and only if r 𝓕 = 0, which by hrpar is the parasitic condition. Here r stands for the restriction 𝓕 ↦ 𝓕|_{U_étale} along a smooth surjective chart f : U → 𝒳, through which the source computes Q; see the module documentation for the three hypotheses it carries and for Stacks 06WT, which hreq names.

theorem isZero_flatBaseChangeQuasicoherator_iff_isParasitic
    (F : locallyQuasicoherentFlatBaseChangeModules.{u, u + 1, u} B E h S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids) :
    IsZero ((flatBaseChangeQuasicoherator B E h S hS 𝒳.val.val.p
        𝒳.val.isFiberedInGroupoids hinc hclosed hpres hls hlsD hwp hsep).obj F) ↔
      IsParasitic.{u, w, u} B S hS 𝒳 .etale F.obj.val

AlgebraicGeometry.Stack.preservesColimitsOfSize_flatBaseChangeQuasicoherator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/CoheratorParasiticKernel.lean, line 301. The attribute's comment: “part (3): Q commutes with all colimits, over the chart data of the construction of Stacks 0778”.

Stacks 0779, part (3): the coherator commutes with all colimits. The source does not get this from adjointness — a right adjoint need not preserve colimits. It gets it from the explicit construction: by exactness it suffices to treat direct sums (Stacks 002P), and restriction to U_étale commutes with direct sums.

Here that is the hypothesis hrcolim on r, carried through the identification Q ≅ r ⋙ (i ⋙ r)⁻¹ which the counit and hreq supply; the inverse of an equivalence preserves all colimits.

theorem preservesColimitsOfSize_flatBaseChangeQuasicoherator
    (hrcolim : PreservesColimitsOfSize.{vJ, uJ} r) :
    PreservesColimitsOfSize.{vJ, uJ}
      (flatBaseChangeQuasicoherator B E h S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids
        hinc hclosed hpres hls hlsD hwp hsep)

AlgebraicGeometry.Stack.exact_flatBaseChangeQuasicoherator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/CoheratorParasiticKernel.lean, line 338. The attribute's comment: “part (3): Q is exact, over the chart data of the construction of Stacks 0778”.

Stacks 0779, part (3): the coherator is exact. Exactness of an additive functor between abelian categories is the preservation of finite limits and of finite colimits. The first half is AlgebraicGeometry.Stack.preservesFiniteLimits_flatBaseChangeQuasicoherator, which holds because Q is a right adjoint; the second is AlgebraicGeometry.Stack.preservesFiniteColimits_flatBaseChangeQuasicoherator, which needs the chart data.

theorem exact_flatBaseChangeQuasicoherator (hrfincolim : PreservesFiniteColimits r) :
    PreservesFiniteLimits
        (flatBaseChangeQuasicoherator B E h S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids
          hinc hclosed hpres hls hlsD hwp hsep) ∧
      PreservesFiniteColimits
        (flatBaseChangeQuasicoherator B E h S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids
          hinc hclosed hpres hls hlsD hwp hsep)

AlgebraicGeometry.Stack.isParasitic_of_isLimit_kernelFork_flatBaseChangeQuasicoherator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/CoheratorParasiticKernel.lean, line 360. The attribute's comment: “part (2), the kernel: the kernel of the adjunction map Q(F) ⟶ F is parasitic”.

Stacks 0779, part (2), the kernel. The kernel of the adjunction map Q 𝓕 ⟶ 𝓕 is parasitic.

The left adjoint i is fully faithful, so Q applied to the counit is invertible, in particular a monomorphism; Q preserves the kernel fork, being a right adjoint; so the kernel is in the kernel of Q and therefore parasitic by part (1). The kernel is taken as an arbitrary limit kernel fork, so that nothing is assumed about LQCoh^fbc(𝒪_𝒳) having kernels (Stacks 0771 part (2)).

theorem isParasitic_of_isLimit_kernelFork_flatBaseChangeQuasicoherator
    {F : locallyQuasicoherentFlatBaseChangeModules.{u, u + 1, u} B E h S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids}
    {c : KernelFork ((flatBaseChangeQuasicoheratorAdjunction B E h S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids hinc hclosed hpres hls hlsD hwp hsep).counit.app F)}
    (hc : IsLimit c) : IsParasitic.{u, w, u} B S hS 𝒳 .etale c.pt.obj.val

AlgebraicGeometry.Stack.isParasitic_of_isColimit_cokernelCofork_flatBaseChangeQuasicoherator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/CoheratorParasiticKernel.lean, line 385. The attribute's comment: “part (2), the cokernel: the cokernel of the adjunction map Q(F) ⟶ F is parasitic”.

Stacks 0779, part (2), the cokernel. The cokernel of the adjunction map Q 𝓕 ⟶ 𝓕 is parasitic.

Q applied to the counit is invertible, in particular an epimorphism; Q is right exact by part (3) and so preserves the cokernel cofork; so the cokernel is in the kernel of Q and therefore parasitic by part (1). As for the kernel, the cokernel is taken as an arbitrary colimit cokernel cofork.

theorem isParasitic_of_isColimit_cokernelCofork_flatBaseChangeQuasicoherator
    (hrfincolim : PreservesFiniteColimits r)
    {F : locallyQuasicoherentFlatBaseChangeModules.{u, u + 1, u} B E h S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids}
    {c : CokernelCofork ((flatBaseChangeQuasicoheratorAdjunction B E h S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids hinc hclosed hpres hls hlsD hwp hsep).counit.app F)}
    (hc : IsColimit c) : IsParasitic.{u, w, u} B S hS 𝒳 .etale c.pt.obj.val
Tag 0GQJ, a lemma

Tag 0GQJ in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isIso_lqcohFbcCoheratorPullbackComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/CoheratorFlatPullback.lean, line 142. The attribute's comment: “the canonical comparison f^ ∘ Q_𝒴 ⟶ Q_𝒳 ∘ f^, the mate of i ∘ f^ = f^ ∘ i under the adjunctions of Stacks 0778, is an isomorphism”.

Stacks 0GQJ. Let f : 𝒳 ⟶ 𝒴 be a flat morphism of algebraic stacks. Then Q_𝒳 ∘ f^* = f^* ∘ Q_𝒴, with Q_𝒳 and Q_𝒴 the coherators of Stacks 0778: the canonical comparison f^* Q_𝒴(𝓕) ⟶ Q_𝒳(f^*𝓕) is an isomorphism for every 𝓕 in LQCoh^fbc(𝒪_𝒴).

theorem isIso_lqcohFbcCoheratorPullbackComparison (hf : AlgebraicStacks.IsFlat B S hS f) :
    IsIso (lqcohFbcCoheratorPullbackComparison B E h S hS f)
Tag 0GQK, a lemma

Tag 0GQK in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isIso_restrict_coheratorAdjunction_counit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/CoheratorFlatObjectIso.lean, line 52. The attribute's comment: “Q(F)|_{U_ét} = F|_{U_ét} for x : U → 𝒳 flat and F in LQCoh^fbc(𝒪_𝒳): the restriction of the adjunction map Q(F) → F to U_ét is an isomorphism”.

Stacks 0GQK. Let x be an object of an algebraic stack 𝒳 lying over a scheme U such that x : U → 𝒳 is flat, and let 𝓕 be in LQCoh^fbc(𝒪_𝒳). Then Q(𝓕)|_{U_ét} = 𝓕|_{U_ét}: the restriction to the small étale site of U of the adjunction map Q(𝓕) ⟶ 𝓕 of the coherator of Stacks 0778 is an isomorphism.

theorem isIso_restrict_coheratorAdjunction_counit (F : Stack.fppfModules B S hS 𝒳)
    (hF : lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳 F)
    (x : 𝒳.val.val.obj) (hx : flatObject B S hS 𝒳.val x) :
    IsIso ((restrictModuleFunctorToSmallEtale B E h S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids x (etaleTopology B) (etaleTopology_le_topology B)).map
        ((coheratorAdjunction B S hS 𝒳).counit.app F).val)
Tag 0GQL, a remark

Tag 0GQL in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isLimitKernelForkCoherator, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/CoheratorCanonical.lean, line 81. The attribute's comment: “part (3), the second half: Q(Ker φ), with its map to 𝓕, is the kernel of φ in QCoh(𝒪_𝒳), for the coherator Q of Stacks 0778”.

Stacks 0GQL, part (3), the kernel in QCoh(𝒪_𝒳). For a map φ : 𝓕 ⟶ 𝓖 of quasi-coherent modules on an algebraic stack, Q(Ker(i φ)), the coherator of the kernel computed in Mod(𝒪_𝒳), with its map to 𝓕, is the kernel of φ in QCoh(𝒪_𝒳).

def isLimitKernelForkCoherator {F G : quasicoherentModules B S hS 𝒳} (φ : F ⟶ G) :
    IsLimit (KernelFork.ofι (Abelian.coreflectorKernelι (coheratorAdjunction B S hS 𝒳) φ)
      (Abelian.coreflectorKernelι_comp (coheratorAdjunction B S hS 𝒳) φ))

AlgebraicGeometry.Stack.AlgebraicStacks.lqcohSheafFbc_kernel_quasicoherentInclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/CoheratorCanonical.lean, line 350. The attribute's comment: “part (3), the first half: the kernel computed in Mod(𝒪_𝒳) of a map of quasi-coherent modules lies in LQCoh^fbc(𝒪_𝒳)”.

Stacks 0GQL, part (3), the kernel in Mod(𝒪_𝒳). For a map φ : 𝓕 ⟶ 𝓖 of quasi-coherent modules on an algebraic stack, the kernel of φ computed in Mod(𝒪_𝒳) lies in LQCoh^fbc(𝒪_𝒳), LQCoh^fbc(𝒪_𝒳) being a weak Serre subcategory containing QCoh(𝒪_𝒳) (Stacks 0771 (2)). Its coherator is the kernel of φ in QCoh(𝒪_𝒳) (AlgebraicGeometry.Stack.AlgebraicStacks.isLimitKernelForkCoherator).

theorem lqcohSheafFbc_kernel_quasicoherentInclusion {F G : quasicoherentModules B S hS 𝒳}
    (φ : F ⟶ G) :
    lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳
      (kernel ((quasicoherentInclusion B S hS 𝒳).map φ))

AlgebraicGeometry.Stack.AlgebraicStacks.lqcohSheafFbc_image_quasicoherentInclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/CoheratorCanonical.lean, line 363. The attribute's comment: “part (2), corrected, the first half: the image computed in Mod(𝒪_𝒳) of a map of quasi-coherent modules lies in LQCoh^fbc(𝒪_𝒳); it need not be quasi-coherent”.

Stacks 0GQL, part (2), corrected, the image in Mod(𝒪_𝒳). For a map φ : 𝓕 ⟶ 𝓖 of quasi-coherent modules on an algebraic stack, the image of φ computed in Mod(𝒪_𝒳) lies in LQCoh^fbc(𝒪_𝒳): it is the kernel of 𝓖 ⟶ Coker(φ). It need not be quasi-coherent: part (2) as printed is refuted by AlgebraicGeometry.Stack.ImageCounterexample.not_forall_isQuasicoherentOnSite_image.

theorem lqcohSheafFbc_image_quasicoherentInclusion {F G : quasicoherentModules B S hS 𝒳}
    (φ : F ⟶ G) :
    lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳
      (Abelian.image ((quasicoherentInclusion B S hS 𝒳).map φ))

AlgebraicGeometry.Stack.AlgebraicStacks.coheratorImageIsImage, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/CoheratorCanonical.lean, line 377. The attribute's comment: “part (2), corrected, the second half: Q(Im φ) is the image of φ in QCoh(𝒪_𝒳), for the coherator Q of Stacks 0778”.

Stacks 0GQL, part (2), corrected, the image in QCoh(𝒪_𝒳). For a map φ : 𝓕 ⟶ 𝓖 of quasi-coherent modules on an algebraic stack, Q(Im φ), the coherator of the image computed in Mod(𝒪_𝒳), is the image of φ in QCoh(𝒪_𝒳): the epimorphism 𝓕 ⟶ Im φ lies in LQCoh^fbc(𝒪_𝒳), where Q is right exact (Stacks 0779 (3)), and Q keeps Im φ ⟶ 𝓖 a monomorphism. Part (2) as printed, with Im φ itself quasi-coherent, is refuted by AlgebraicGeometry.Stack.ImageCounterexample.not_forall_isQuasicoherentOnSite_image.

def coheratorImageIsImage {F G : quasicoherentModules B S hS 𝒳} (φ : F ⟶ G) :
    IsImage (Abelian.coreflectorImageMonoFactorisation (coheratorAdjunction B S hS 𝒳) φ)

AlgebraicGeometry.Stack.ImageCounterexample.not_forall_isQuasicoherentOnSite_image, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentImageCounterexample.lean, line 330. The attribute's comment: “part (2) as printed is false, and the inclusion QCoh(𝒪_𝒳) → Mod(𝒪_𝒳) is not exact in general: for multiplication by 2 on 𝒪 over Spec ℤ the image computed in Mod(𝒪_𝒳) is not quasi-coherent (it vanishes on Spec 𝔽₂ while its would-be module 2ℤ ⊗ 𝔽₂ does not); the corrected part (2) is lqcohSheafFbc_image_quasicoherentInclusion and coheratorImageIsImage”.

Stacks 0GQL, part (2), fails as written. It is not true that for every map φ of quasi-coherent modules on an algebraic stack the image of φ computed in Mod(𝒪_𝒳) is quasi-coherent: multiplication by 2 on 𝒪 over Spec ℤ is a counterexample. The corrected part (2) is AlgebraicGeometry.Stack.AlgebraicStacks.lqcohSheafFbc_image_quasicoherentInclusion (the image lies in LQCoh^fbc(𝒪_𝒳)) together with AlgebraicGeometry.Stack.AlgebraicStacks.coheratorImageIsImage (its coherator is the image in QCoh(𝒪_𝒳)).

theorem not_forall_isQuasicoherentOnSite_image :
    ¬ ∀ (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
      (𝒳 : AlgebraicStacks.{u, w} B S hS) (F G : AlgebraicStacks.quasicoherentModules B S hS 𝒳)
      (φ : F ⟶ G),
      (Abelian.image
        ((AlgebraicStacks.quasicoherentInclusion B S hS 𝒳).map φ)).IsQuasicoherentOnSite

AlgebraicGeometry.FibredSite.isColimitCokernelCoforkMapQuasicoherentInclusion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentKernelCokernel.lean, line 114. The attribute's comment: “part (1): the cokernel of a map of quasi-coherent modules computed in Mod(𝒪_𝒳) is the inclusion of the cokernel computed in QCoh(𝒪_𝒳), over the closure of quasi-coherence under colimits”.

Stacks 0GQL, part (1). Let φ : 𝓕 → 𝓖 be a map of quasi-coherent 𝒪_𝒳-modules. The cokernel of φ in QCoh(𝒪_𝒳), included into Mod(𝒪_𝒳) together with its projection, is a cokernel of φ in Mod(𝒪_𝒳).

So the cokernel computed in Mod(𝒪_𝒳) is the image of a quasi-coherent module — which is the quasi-coherence half of the clause, recorded separately as AlgebraicGeometry.FibredSite.isQuasicoherent_cokernel_quasicoherentInclusion — and it is the cokernel in QCoh(𝒪_𝒳). The proof is the right exactness of the inclusion, which is how the source gets the clause.

def isColimitCokernelCoforkMapQuasicoherentInclusion
    {F G : quasicoherentModules.{u, u + 1, u, u} B S hS p hp} (φ : F ⟶ G) :
    IsColimit (Cofork.ofπ
      ((SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
          (ringStructureSheafCore B S hS p hp .fppf)).ι.map (cokernel.π φ))
      (by simp only [← Functor.map_comp, cokernel.condition, zero_comp, Functor.map_zero]) :
      Cofork ((SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
        (ringStructureSheafCore B S hS p hp .fppf)).ι.map φ) 0)

AlgebraicGeometry.FibredSite.isQuasicoherent_cokernel_quasicoherentInclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentKernelCokernel.lean, line 130. The attribute's comment: “part (1), the quasi-coherence half: the cokernel computed in Mod(𝒪_𝒳) of a map of quasi-coherent modules is quasi-coherent, over the closure of quasi-coherence under colimits”.

Stacks 0GQL, part (1), the quasi-coherence half. The cokernel of a map of quasi-coherent 𝒪_𝒳-modules computed in Mod(𝒪_𝒳) is quasi-coherent, because it is isomorphic to the inclusion of the cokernel computed in QCoh(𝒪_𝒳).

theorem isQuasicoherent_cokernel_quasicoherentInclusion
    {F G : quasicoherentModules.{u, u + 1, u, u} B S hS p hp} (φ : F ⟶ G) :
    (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
        (ringStructureSheafCore B S hS p hp .fppf))
      (cokernel ((SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
        (ringStructureSheafCore B S hS p hp .fppf)).ι.map φ))

AlgebraicGeometry.Stack.isLimitKernelForkFlatBaseChangeQuasicoherator, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentKernelCokernel.lean, line 240. The attribute's comment: “part (3), second half: Q(Ker φ) is the kernel of φ in QCoh(𝒪_𝒳), over the existence of Ker φ inside LQCoh^fbc(𝒪_𝒳) — the first half of the clause, which is Stacks 0771 part (2) and is not available”.

Stacks 0GQL, part (3), second half. Let φ : 𝓕 → 𝓖 be a map of quasi-coherent 𝒪_𝒳-modules and let Ker(i φ) be its kernel inside LQCoh^fbc(𝒪_𝒳). Then Q(Ker(i φ)), with the map AlgebraicGeometry.Stack.quasicoheratorKernelι to 𝓕, is a kernel of φ in QCoh(𝒪_𝒳).

The proof is formal: Q is a right adjoint, so it preserves the kernel, and Q ∘ i is the identity because the inclusion is fully faithful; transporting the kernel of Q(i φ) along that identification gives the kernel of φ.

That Ker(φ) computed in Mod(𝒪_𝒳) lies in LQCoh^fbc(𝒪_𝒳) is the first half of the clause and is Stacks 0771 part (2); it is not available, and it enters here only as the instance hypothesis that the kernel exists in LQCoh^fbc(𝒪_𝒳).

def isLimitKernelForkFlatBaseChangeQuasicoherator
    {F G : FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS p hp} (φ : F ⟶ G)
    [HasKernel ((quasicoherentToFlatBaseChange B E h S hS p hp hinc).map φ)] :
    IsLimit (KernelFork.ofι
      (quasicoheratorKernelι B E h S hS p hp hinc hclosed hpres hls hlsD hwp hsep φ)
      (quasicoheratorKernelι_comp B E h S hS p hp hinc hclosed hpres hls hlsD hwp hsep φ))

AlgebraicGeometry.Stack.AlgebraicStacks.preservesFiniteColimits_quasicoherentInclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentKernelImageCokernel.lean, line 78. The attribute's comment: “the inclusion QCoh(𝒪_𝒳) → Mod(𝒪_𝒳) is right exact”.

Stacks 0GQL, the right exactness of the inclusion. The inclusion QCoh(𝒪_𝒳) → Mod(𝒪_𝒳) of the quasi-coherent modules on an algebraic stack is right exact.

theorem preservesFiniteColimits_quasicoherentInclusion :
    PreservesFiniteColimits (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
      (FibredSite.ringStructureSheafCore B S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids .fppf)).ι

AlgebraicGeometry.Stack.AlgebraicStacks.isColimitCokernelCoforkQuasicoherentInclusion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentKernelImageCokernel.lean, line 111. The attribute's comment: “part (1): the cokernel computed in Mod(𝒪_𝒳) of a map of quasi-coherent modules is the cokernel computed in QCoh(𝒪_𝒳)”.

Stacks 0GQL, part (1). Let φ : 𝓕 → 𝓖 be a map of quasi-coherent modules on an algebraic stack 𝒳. The cokernel of φ in QCoh(𝒪_𝒳), included into Mod(𝒪_𝒳) with its projection, is a cokernel of φ in Mod(𝒪_𝒳): the cokernel computed in Mod(𝒪_𝒳) is the cokernel in QCoh(𝒪_𝒳).

def isColimitCokernelCoforkQuasicoherentInclusion
    {F G : FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids} (φ : F ⟶ G) :
    IsColimit (Cofork.ofπ
      ((SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
          (FibredSite.ringStructureSheafCore B S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids
            .fppf)).ι.map (cokernel.π φ))
      (by simp only [← Functor.map_comp, cokernel.condition, zero_comp, Functor.map_zero]) :
      Cofork ((SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
        (FibredSite.ringStructureSheafCore B S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids
          .fppf)).ι.map φ) 0)

AlgebraicGeometry.Stack.AlgebraicStacks.isQuasicoherent_cokernel_quasicoherentInclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentKernelImageCokernel.lean, line 128. The attribute's comment: “part (1), the quasi-coherence half: the cokernel computed in Mod(𝒪_𝒳) of a map of quasi-coherent modules is quasi-coherent”.

Stacks 0GQL, part (1), the quasi-coherence half. The cokernel computed in Mod(𝒪_𝒳) of a map of quasi-coherent modules on an algebraic stack is quasi-coherent.

theorem isQuasicoherent_cokernel_quasicoherentInclusion
    {F G : FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids} (φ : F ⟶ G) :
    (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
        (FibredSite.ringStructureSheafCore B S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids .fppf))
      (cokernel ((SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
        (FibredSite.ringStructureSheafCore B S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids
          .fppf)).ι.map φ))

AlgebraicGeometry.Stack.AlgebraicStacks.instAbelianQuasicoherentModules, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentModulesAbelian.lean, line 70. The attribute's comment: “the category QCoh(𝒪_𝒳) is abelian, for every algebraic stack 𝒳”.

Stacks 0GQL: QCoh(𝒪_𝒳) is abelian, for every algebraic stack 𝒳 (also Stacks 06WV part (2)). It is coreflective in the weak Serre subcategory LQCoh^fbc(𝒪_𝒳) of Mod(𝒪_𝒳), with the coherator, right exact there, as coreflector.

instance instAbelianQuasicoherentModules : Abelian (quasicoherentModules B S hS 𝒳)

Declarations registered for the tag:

Tag 0GQM, a remark

Tag 0GQM in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isMonoidal_lqcohSheafFbc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/CoheratorCanonical.lean, line 207. The attribute's comment: “(ii): LQCoh^fbc(𝒪_𝒳) is closed under the tensor product, a monoidal subcategory of Mod(𝒪_𝒳)”.

Stacks 0GQM, (ii). LQCoh^fbc(𝒪_𝒳) is closed under the tensor product of 𝒪_𝒳-modules (Stacks 0771 (6)) and contains 𝒪_𝒳: it is a monoidal subcategory of Mod(𝒪_𝒳).

theorem isMonoidal_lqcohSheafFbc :
    (lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳).IsMonoidal

AlgebraicGeometry.Stack.AlgebraicStacks.lqcohSheafFbcInclusionBraided, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/CoheratorCanonical.lean, line 222. The attribute's comment: “(iii): the inclusion LQCoh^fbc(𝒪_𝒳) → Mod(𝒪_𝒳) is a functor of symmetric monoidal categories”.

Stacks 0GQM, (iii), the inclusion LQCoh^fbc(𝒪_𝒳) → Mod(𝒪_𝒳): a functor of symmetric monoidal categories, for the tensor product of 𝒪_𝒳-modules and the structure it induces on LQCoh^fbc(𝒪_𝒳).

def lqcohSheafFbcInclusionBraided :
    letI := isMonoidal_lqcohSheafFbc B S hS 𝒳 E h
    (lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳).ι.Braided

AlgebraicGeometry.Stack.AlgebraicStacks.quasicoherentToLqcohSheafFbcBraided, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/CoheratorCanonical.lean, line 232. The attribute's comment: “(iii): the inclusion QCoh(𝒪_𝒳) → LQCoh^fbc(𝒪_𝒳) is a functor of symmetric monoidal categories”.

Stacks 0GQM, (iii), the inclusion QCoh(𝒪_𝒳) → LQCoh^fbc(𝒪_𝒳): a functor of symmetric monoidal categories, for the structures both inherit from Mod(𝒪_𝒳).

def quasicoherentToLqcohSheafFbcBraided :
    letI := isMonoidal_lqcohSheafFbc B S hS 𝒳 E h
    (ObjectProperty.ιOfLE (isQuasicoherentOnSite_le_lqcohSheafFbc B S hS 𝒳 E h)).Braided

AlgebraicGeometry.Stack.AlgebraicStacks.coheratorBraided, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/CoheratorCanonical.lean, line 288. The attribute's comment: “(iv): the coherator Q : LQCoh^fbc(𝒪_𝒳) → QCoh(𝒪_𝒳) is a functor of symmetric monoidal categories”.

Stacks 0GQM, (iv). The coherator Q : LQCoh^fbc(𝒪_𝒳) → QCoh(𝒪_𝒳) is a functor of symmetric monoidal categories. Its comparison Q(𝓕) ⊗ Q(𝓖) → Q(𝓕 ⊗ 𝓖) is the adjoint transpose of the tensor product Q(𝓕) ⊗ Q(𝓖) → 𝓕 ⊗ 𝓖 of the two counits, the south-west arrow of the triangle of the source, and it is invertible because Q inverts that tensor product of counits (AlgebraicGeometry.Stack.AlgebraicStacks.isIso_coherator_map_tensorHom_counit).

def coheratorBraided :
    letI := isMonoidal_lqcohSheafFbc B S hS 𝒳 E h
    ((lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳).ι ⋙ coherator B S hS 𝒳).Braided

AlgebraicGeometry.Stack.AlgebraicStacks.isIso_coheratorTensorComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/CoheratorCanonical.lean, line 299. The attribute's comment: “(iv): the canonical map Q(F) ⊗ Q(G) → Q(F ⊗ G) is an isomorphism”.

Stacks 0GQM, (iv), the tensor comparison. For 𝓕, 𝓖 in LQCoh^fbc(𝒪_𝒳) the canonical map Q(𝓕) ⊗ Q(𝓖) → Q(𝓕 ⊗ 𝓖), the adjoint transpose of the tensor product of the two counits, is an isomorphism.

theorem isIso_coheratorTensorComparison
    (F G : (lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳).FullSubcategory) :
    letI := isMonoidal_lqcohSheafFbc B S hS 𝒳 E h
    letI := (lqcohSheafFbcCoheratorAdjunction B S hS 𝒳 E h).rightAdjointLaxMonoidal
    IsIso (Functor.LaxMonoidal.μ
      ((lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳).ι ⋙ coherator B S hS 𝒳) F G)

AlgebraicGeometry.Stack.AlgebraicStacks.coheratorTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/CoheratorCanonical.lean, line 313. The attribute's comment: “(iv): the isomorphism Q(F) ⊗ Q(G) ≅ Q(F ⊗ G)”.

Stacks 0GQM, (iv), the isomorphism Q(𝓕) ⊗ Q(𝓖) ≅ Q(𝓕 ⊗ 𝓖) of the symmetric monoidal functor AlgebraicGeometry.Stack.AlgebraicStacks.coheratorBraided; its forward map is the canonical comparison (AlgebraicGeometry.Stack.AlgebraicStacks.coheratorTensorIso_hom).

def coheratorTensorIso
    (F G : (lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳).FullSubcategory) :
    letI := isMonoidal_lqcohSheafFbc B S hS 𝒳 E h
    (coherator B S hS 𝒳).obj F.obj ⊗ (coherator B S hS 𝒳).obj G.obj ≅
      (coherator B S hS 𝒳).obj (F ⊗ G).obj

AlgebraicGeometry.Stack.AlgebraicStacks.isQuasicoherentOnSite_sheafTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/CoheratorMonoidal.lean, line 121. The attribute's comment: “(i): the tensor product of two quasi-coherent modules on an algebraic stack is quasi-coherent”.

Stacks 0GQM, (i). The tensor product 𝓕 ⊗_{𝒪_𝒳} 𝓖 of two quasi-coherent modules on an algebraic stack is quasi-coherent (Stacks 06WV part (5)). The tensor product is the tensor product sheaf, the sheafification of the objectwise tensor product, on the fppf site of 𝒳.

This is AlgebraicGeometry.FibredSite.isQuasicoherentOnSite_tensorSheaf at the fppf site of the algebraic stack, which is essentially small.

theorem isQuasicoherentOnSite_sheafTensor (F G : Stack.fppfModules B S hS 𝒳)
    (hF : F.IsQuasicoherentOnSite) (hG : G.IsQuasicoherentOnSite) :
    (((Stacks.SheafOfModules.Tensor.sheafTensor (FibredSite.structureSheaf B S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids .fppf)).obj F).obj G).IsQuasicoherentOnSite

AlgebraicGeometry.Stack.AlgebraicStacks.quasicoherentInclusionBraided, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/CoheratorMonoidal.lean, line 147. The attribute's comment: “(iii): the inclusion QCoh(𝒪_𝒳) → Mod(𝒪_𝒳) is a functor of symmetric monoidal categories”.

Stacks 0GQM, (iii), the first inclusion into Mod(𝒪_𝒳). QCoh(𝒪_𝒳) is a symmetric monoidal category for the tensor product of 𝒪_𝒳-modules, and the inclusion QCoh(𝒪_𝒳) → Mod(𝒪_𝒳) is a functor of symmetric monoidal categories.

def quasicoherentInclusionBraided : (quasicoherentInclusion B S hS 𝒳).Braided

Stacks.SheafOfModules.TensorProduct.isQuasicoherent_tensorSheaf', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/TensorProduct/Quasicoherent.lean, line 303. The attribute's comment: “tensor products of quasi-coherent modules are quasi-coherent”. References: EGA I (9.1.1), “more general”.

Stacks 0GQM. The tensor product of two quasi-coherent sheaves of modules on a site is quasi-coherent.

Each factor is presented on some family covering the final object. The two families are refined by the objects carrying a morphism into a member of each, which again covers the final object: given an object, the first family covers it, each member of that cover is covered by the second family, and every object of the resulting cover maps to a member of both. On such an object the two presentations restrict, their tensor product presents the tensor product of the restrictions by Stacks.SheafOfModules.TensorProduct.tensorPresentation, and that is the restriction of F ⊗_𝒪 G by Stacks.SheafOfModules.TensorProduct.tensorSheafificationOverIso.

theorem isQuasicoherent_tensorSheaf'
    (F G : SheafOfModules.{w} (structureSheaf 𝒪 h𝒪))
    [F.IsQuasicoherent] [G.IsQuasicoherent] :
    ((((Stacks.SheafOfModules.Tensor.sheafTensor
        ⟨𝒪, Presheaf.isSheaf_of_isSheaf_comp _ (𝒪) (forget₂ CommRingCat RingCat)
          (h𝒪)⟩).obj (F)).obj (G))).IsQuasicoherent
Tag 07B2, a remark

Tag 07B2 in the Stacks Project.

AlgebraicGeometry.Stack.isLocalization_flatBaseChangeQuasicoherator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/CoheratorSerreQuotient.lean, line 316. The attribute's comment: “the displayed identification QCoh(𝒪_𝒳) = LQCoh^fbc(𝒪_𝒳) / Parasitic(𝒪_𝒳) ∩ LQCoh^fbc(𝒪_𝒳): the coherator Q of 0778 is a localization functor for the Serre class of parasitic objects; over the hypotheses of 0778 and 0779 and the abelian structures of 06WV (2) and 0771 (2)”.

Stacks 07B2, the displayed identification

QCoh(𝒪_𝒳) = LQCoh^fbc(𝒪_𝒳) / Parasitic(𝒪_𝒳) ∩ LQCoh^fbc(𝒪_𝒳).

The coherator Q : LQCoh^fbc(𝒪_𝒳) ⥤ QCoh(𝒪_𝒳) of Stacks 0778 is a localization functor for the class of morphisms whose kernel and cokernel are parasitic, that is, it exhibits QCoh(𝒪_𝒳) as the quotient of LQCoh^fbc(𝒪_𝒳) by the Serre subcategory of parasitic objects (Stacks 02MS).

The inclusion i is fully faithful and Q is its right adjoint (Stacks 0778), so Q is a localization functor for the class of morphisms it inverts; by AlgebraicGeometry.Stack.parasiticIsoModSerre_eq_inverseImage_isomorphisms that class is the one attached to the parasitic part.

theorem isLocalization_flatBaseChangeQuasicoherator :
    (flatBaseChangeQuasicoherator B E h S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids
        hinc hclosed hpres hls hlsD hwp hsep).IsLocalization
      (parasiticIsoModSerre B E h S hS 𝒳 hinc hclosed hpres hls hlsD hwp hsep r hrpar
        hrcounit hreq hrfincolim)

AlgebraicGeometry.Stack.serreQuotientEquivalenceQuasicoherentModules, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/CoheratorSerreQuotient.lean, line 339. The attribute's comment: “the displayed identification read as an equivalence of categories between the Serre quotient of LQCoh^fbc(𝒪_𝒳) by Parasitic(𝒪_𝒳) ∩ LQCoh^fbc(𝒪_𝒳) and QCoh(𝒪_𝒳); over the hypotheses of 0778 and 0779 and the abelian structures of 06WV (2) and 0771 (2)”.

Stacks 07B2, the displayed identification as an equivalence of categories. The Serre quotient LQCoh^fbc(𝒪_𝒳) / Parasitic(𝒪_𝒳) ∩ LQCoh^fbc(𝒪_𝒳), built as the localization of LQCoh^fbc(𝒪_𝒳) at the morphisms with parasitic kernel and cokernel, is equivalent to QCoh(𝒪_𝒳), the equivalence being the one through which the coherator of Stacks 0778 factors.

def serreQuotientEquivalenceQuasicoherentModules :
    (parasiticIsoModSerre B E h S hS 𝒳 hinc hclosed hpres hls hlsD hwp hsep r hrpar hrcounit
        hreq hrfincolim).Localization ≌
      FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS 𝒳.val.val.p
        𝒳.val.isFiberedInGroupoids

AlgebraicGeometry.Stack.serreQuotientAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/CoheratorSerreQuotient.lean, line 364. The attribute's comment: “the key feature: the inclusion i : QCoh(𝒪_𝒳) ⥤ LQCoh^fbc(𝒪_𝒳) is left adjoint to the quotient functor LQCoh^fbc(𝒪_𝒳) ⥤ LQCoh^fbc(𝒪_𝒳) / Parasitic(𝒪_𝒳) ∩ LQCoh^fbc(𝒪_𝒳); over the hypotheses of 0778 and 0779 and the abelian structures of 06WV (2) and 0771 (2)”.

Stacks 07B2, the key feature: the inclusion i : QCoh(𝒪_𝒳) ⥤ LQCoh^fbc(𝒪_𝒳) is left adjoint to the quotient functor.

Read with QCoh(𝒪_𝒳) identified with the Serre quotient by AlgebraicGeometry.Stack.serreQuotientEquivalenceQuasicoherentModules, this is an adjunction between i and the canonical quotient functor LQCoh^fbc(𝒪_𝒳) ⥤ LQCoh^fbc(𝒪_𝒳) / Parasitic(𝒪_𝒳) ∩ LQCoh^fbc(𝒪_𝒳). It is the adjunction of Stacks 0778 composed with the adjoint equivalence, transported along the isomorphism which identifies the quotient functor with the coherator followed by that equivalence.

def serreQuotientAdjunction :
    (serreQuotientEquivalenceQuasicoherentModules B E h S hS 𝒳 hinc hclosed hpres hls hlsD hwp
          hsep r hrpar hrcounit hreq hrfincolim).functor ⋙
        quasicoherentToFlatBaseChange B E h S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids hinc ⊣
      (parasiticIsoModSerre B E h S hS 𝒳 hinc hclosed hpres hls hlsD hwp hsep r hrpar hrcounit
        hreq hrfincolim).Q

AlgebraicGeometry.Stack.AlgebraicStacks.isLocalization_lqcohFbcCoherator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentSerreQuotient.lean, line 142. The attribute's comment: “the displayed identification QCoh(𝒪_𝒳) = LQCoh^fbc(𝒪_𝒳) / Parasitic(𝒪_𝒳) ∩ LQCoh^fbc(𝒪_𝒳): the coherator Q of 0778 is a localization functor for the Serre class of parasitic objects”.

Stacks 07B2, the displayed identification QCoh(𝒪_𝒳) = LQCoh^fbc(𝒪_𝒳) / Parasitic(𝒪_𝒳) ∩ LQCoh^fbc(𝒪_𝒳): for an algebraic stack 𝒳, the coherator Q : LQCoh^fbc(𝒪_𝒳) ⥤ QCoh(𝒪_𝒳) of Stacks 0778 is a localization functor for the morphisms whose kernel and cokernel are parasitic, i.e. it exhibits QCoh(𝒪_𝒳) as the Serre quotient (Stacks 02MS) of LQCoh^fbc(𝒪_𝒳) by its parasitic objects.

theorem isLocalization_lqcohFbcCoherator :
    (lqcohFbcCoherator B E h S hS 𝒳).IsLocalization
      (parasiticLqcohFbc B E h S hS 𝒳).isoModSerre

AlgebraicGeometry.Stack.AlgebraicStacks.lqcohFbcSerreQuotientEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentSerreQuotient.lean, line 154. The attribute's comment: “the displayed identification read as an equivalence of categories between the Serre quotient of LQCoh^fbc(𝒪_𝒳) by Parasitic(𝒪_𝒳) ∩ LQCoh^fbc(𝒪_𝒳) and QCoh(𝒪_𝒳)”.

Stacks 07B2, the displayed identification as an equivalence of categories between the Serre quotient LQCoh^fbc(𝒪_𝒳) / Parasitic(𝒪_𝒳) ∩ LQCoh^fbc(𝒪_𝒳) (the localization at the morphisms with parasitic kernel and cokernel) and QCoh(𝒪_𝒳), the one through which the coherator of Stacks 0778 factors.

def lqcohFbcSerreQuotientEquivalence :
    (parasiticLqcohFbc B E h S hS 𝒳).isoModSerre.Localization ≌ quasicoherentModules B S hS 𝒳

AlgebraicGeometry.Stack.AlgebraicStacks.lqcohFbcSerreQuotientAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentSerreQuotient.lean, line 165. The attribute's comment: “the key feature: the inclusion i : QCoh(𝒪_𝒳) ⥤ LQCoh^fbc(𝒪_𝒳) is left adjoint to the quotient functor LQCoh^fbc(𝒪_𝒳) ⥤ LQCoh^fbc(𝒪_𝒳) / Parasitic(𝒪_𝒳) ∩ LQCoh^fbc(𝒪_𝒳)”.

Stacks 07B2, the key feature: the inclusion i : QCoh(𝒪_𝒳) ⥤ LQCoh^fbc(𝒪_𝒳), read on the Serre quotient through lqcohFbcSerreQuotientEquivalence, is left adjoint to the quotient functor LQCoh^fbc(𝒪_𝒳) ⥤ LQCoh^fbc(𝒪_𝒳) / Parasitic(𝒪_𝒳) ∩ LQCoh^fbc(𝒪_𝒳).

def lqcohFbcSerreQuotientAdjunction :
    (lqcohFbcSerreQuotientEquivalence B E h S hS 𝒳).functor ⋙
        quasicoherentToLqcohFbc B E h S hS 𝒳 ⊣
      (parasiticLqcohFbc B E h S hS 𝒳).isoModSerre.Q
Tag 0GQN, a lemma

Tag 0GQN in the Stacks Project.

AlgebraicGeometry.FibredSite.internalHomSheaf_restrictSiteModules_val, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/InternalHomSiteAgreement.lean, line 107. The attribute's comment: “the two internal Homs have the same presheaf of modules”.

Stacks 0GQN, the first assertion, on underlying presheaves of modules. The internal Hom of two sheaves of modules on the associated fppf site of a category fibred in groupoids has the same underlying presheaf of modules whether it is computed on the associated fppf site or on any of the five associated sites; the source's case is the étale one.

The internal Hom of Stacks 03EM is built from the presheaves of modules underlying its two arguments and from the presheaf of rings underlying the structure sheaf, and none of the three depends on the topology, so the two presheaves of modules are equal on the nose.

public theorem internalHomSheaf_restrictSiteModules_val (τ : SiteKind)
    (F G : SheafOfModules.{m} (ringStructureSheafCore B S hS p hp .fppf)) :
    ((ringedSite B S hS p hp τ).internalHomSheaf
        (restrictSiteModules.{u, v, w, m} B S hS p hp τ F)
        (restrictSiteModules.{u, v, w, m} B S hS p hp τ G)).val =
      ((ringedSite B S hS p hp .fppf).internalHomSheaf F G).val

AlgebraicGeometry.FibredSite.isSheaf_internalHomSheaf_restrictSiteModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/InternalHomSiteAgreement.lean, line 123. The attribute's comment: “the common value is a sheaf for the fppf topology”.

Stacks 0GQN, the first assertion, on the sheaf condition. The internal Hom computed on one of the five associated sites of a category fibred in groupoids is a sheaf for the associated fppf topology, so it is an object of Mod(𝒪_𝒳) and not merely of Mod(𝒳_étale, 𝒪_𝒳).

By Stacks 03EM the internal Hom is a sheaf for any topology for which its target is one, and the target here is a sheaf for the associated fppf topology.

public theorem isSheaf_internalHomSheaf_restrictSiteModules (τ : SiteKind)
    (F G : SheafOfModules.{m} (ringStructureSheafCore B S hS p hp .fppf)) :
    Presheaf.IsSheaf (BigFppfOver.associatedTopology B S hS p .fppf)
      ((ringedSite B S hS p hp τ).internalHomSheaf
        (restrictSiteModules.{u, v, w, m} B S hS p hp τ F)
        (restrictSiteModules.{u, v, w, m} B S hS p hp τ G)).val.presheaf

AlgebraicGeometry.FibredSite.internalHomSheaf_restrictSiteModules_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/InternalHomSiteAgreement.lean, line 139. The attribute's comment: “the two internal Homs agree as objects of Mod(𝒪_𝒳)”.

Stacks 0GQN, the first assertion. The internal Hom of two sheaves of modules on the associated fppf site of a category fibred in groupoids, computed on one of the five associated sites, agrees as an object of Mod(𝒪_𝒳) with the one computed on the associated fppf site; the source's case is the étale one.

This is the conjunction of the two statements above: the underlying presheaves of modules are equal, and the common presheaf is a sheaf for the associated fppf topology.

public theorem internalHomSheaf_restrictSiteModules_eq (τ : SiteKind)
    (F G : SheafOfModules.{m} (ringStructureSheafCore B S hS p hp .fppf)) :
    (⟨((ringedSite B S hS p hp τ).internalHomSheaf
          (restrictSiteModules.{u, v, w, m} B S hS p hp τ F)
          (restrictSiteModules.{u, v, w, m} B S hS p hp τ G)).val,
        isSheaf_internalHomSheaf_restrictSiteModules.{u, v, w, m} B S hS p hp τ F G⟩ :
        SheafOfModules.{max v w m} (ringStructureSheafCore B S hS p hp .fppf)) =
      (ringedSite B S hS p hp .fppf).internalHomSheaf F G

AlgebraicGeometry.Stack.AlgebraicStacks.fppfInternalHom_presheaf_eq_etaleInternalHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentInternalHom.lean, line 107. The attribute's comment: “the agreement of the internal Homs of Mod(𝒳_étale, 𝒪_𝒳) and Mod(𝒪_𝒳), for arbitrary F and G”.

Stacks 0GQN, the agreement of the two internal Homs at module universe u. The internal Hom SheafHom_{𝒪_𝒳}(F, G) computed in Mod(𝒳_étale, 𝒪_𝒳) and the one computed in Mod(𝒪_𝒳) have the same underlying presheaf of abelian groups, for arbitrary modules F and G on the fppf site; the source states it for F of finite presentation and G quasi-coherent.

Both are the internal Hom of Stacks 03EM read in the universe u of the module sections, and that construction depends only on the underlying presheaves of F, G and of the structure sheaf, none of which changes with the topology.

theorem fppfInternalHom_presheaf_eq_etaleInternalHom (F G : Stack.fppfModules B S hS 𝒳) :
    (fppfInternalHom B S hS 𝒳 F G).val.presheaf =
      (etaleInternalHom B S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids
        (FibredSite.restrictSiteModules B S hS _ _ .etale F)
        (FibredSite.restrictSiteModules B S hS _ _ .etale G)).val.presheaf

AlgebraicGeometry.Stack.AlgebraicStacks.quasicoherentHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentInternalHom.lean, line 148. The attribute's comment: “the universal property of hom(F, G) = Q(SheafHom(F, G)), for arbitrary F and G”.

The universal property of hom(F, G) (Stacks 0GQN): for H quasi-coherent, Hom_𝒳(H, hom(F, G)) = Hom_𝒳(H ⊗_{𝒪_𝒳} F, G). This is AlgebraicGeometry.Stack.AlgebraicStacks.quasicoherentHomOfEquiv at the coherator; it holds for arbitrary F and G.

def quasicoherentHomEquiv (F G : Stack.fppfModules B S hS 𝒳)
    (H : quasicoherentModules B S hS 𝒳) :
    (H ⟶ quasicoherentHom B S hS 𝒳 F G) ≃
      (fppfTensor B S hS 𝒳 ((quasicoherentInclusion B S hS 𝒳).obj H) F ⟶ G)

AlgebraicGeometry.Stack.AlgebraicStacks.lqcohSheafFbcFppfModules_fppfInternalHom_of_isQuasicoherentOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/SheafFlatBaseChangeInternalHom.lean, line 100. The attribute's comment: “the common value SheafHom(F, G) is an object of LQCoh^fbc(𝒪_𝒳), for F of finite presentation and G quasi-coherent”.

Stacks 0GQN, the membership clause: for F an 𝒪_𝒳-module of finite presentation and G a quasi-coherent 𝒪_𝒳-module on an algebraic stack, the internal Hom SheafHom_{𝒪_𝒳}(F, G), whose two computations agree by AlgebraicGeometry.Stack.AlgebraicStacks.fppfInternalHom_presheaf_eq_etaleInternalHom, is an object of LQCoh^fbc(𝒪_𝒳). It is Stacks 0771 (7) applied to G ∈ QCoh(𝒪_𝒳) ⊆ LQCoh^fbc(𝒪_𝒳).

theorem lqcohSheafFbcFppfModules_fppfInternalHom_of_isQuasicoherentOnSite
    (F G : Stack.fppfModules B S hS 𝒳) [F.IsFinitePresentationOnSite]
    (hG : G.IsQuasicoherentOnSite) :
    lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳 (fppfInternalHom B S hS 𝒳 F G)
Tag 0GQP, a lemma

Tag 0GQP in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.quasicoherentHomFlatPullbackIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentHomFlatPullback.lean, line 76.

Stacks 0GQP. Let f : 𝒳 ⟶ 𝒴 be a flat morphism of algebraic stacks, F an 𝒪_𝒴-module of finite presentation and G a quasi-coherent 𝒪_𝒴-module. Then f^* hom(F, G) = hom(f^* F, f^* G), with hom the quasi-coherent internal Hom hom(F, G) = Q(SheafHom_{𝒪_𝒴}(F, G)) of Stacks 0GQN.

The isomorphism is the composite of f^* Q_𝒴 = Q_𝒳 f^* (Stacks 0GQJ, at SheafHom_{𝒪_𝒴}(F, G), which lies in LQCoh^fbc(𝒪_𝒴) by Stacks 0GQN) with Q_𝒳 of f^* SheafHom_{𝒪_𝒴}(F, G) = SheafHom_{𝒪_𝒳}(f^* F, f^* G).

def quasicoherentHomFlatPullbackIso (hf : AlgebraicStacks.IsFlat B S hS f)
    (F G : Stack.fppfModules B S hS 𝒴) [F.IsFinitePresentationOnSite]
    (hG : G.IsQuasicoherentOnSite) :
    (quasicoherentPullback B S hS f).obj (quasicoherentHom B S hS 𝒴 F G) ≅
      quasicoherentHom B S hS 𝒳 ((fppfModulesPullback B S hS f).obj F)
        ((fppfModulesPullback B S hS f).obj G)
Sources

Section103.11 Pushforward of quasi-coherent modules#

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

Tag 077A, a proposition

Tag 077A in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.quasicoherentPullbackDirectImageAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentDirectImage.lean, line 234. The attribute's comment: “first assertion: f^ on quasi-coherent modules has the right adjoint f_{QCoh,} = Q ∘ f_* ∘ i, for every 1-morphism of algebraic stacks”.

Stacks 077A, the first assertion: f^* : QCoh(𝒪_𝒴) ⥤ QCoh(𝒪_𝒳) has the right adjoint f_{QCoh,*}, defined as the composite of the inclusion, the direct image of modules (Stacks 06WE) and the coherator (Stacks 0778, Stacks 0781 part (2)).

It holds for every 1-morphism; the source states it for quasi-compact and quasi-separated ones, for which the direct image of a quasi-coherent module lies in LQCoh^fbc(𝒪_𝒴), where the coherator is the one of Stacks 0778.

def quasicoherentPullbackDirectImageAdjunction :
    quasicoherentPullback B S hS f ⊣ quasicoherentDirectImage B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.quasicoherentDirectImageIsoComposite, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentHigherDirectImageDeltaFunctor.lean, line 143. The attribute's comment: “f_{QCoh,} is the composite QCoh(O_X) → LQCoh^fbc(O_X) → LQCoh^fbc(O_Y) → QCoh(O_Y) of the inclusion, f_ of Stacks 0771 and Q of Stacks 0778”.

Stacks 077A: f_{QCoh,*} is the composite QCoh(𝒪_𝒳) → LQCoh^fbc(𝒪_𝒳) → LQCoh^fbc(𝒪_𝒴) → QCoh(𝒪_𝒴) of the inclusion, the direct image of Stacks 0771 and the coherator Q of Stacks 0778, the restriction of the coherator to LQCoh^fbc(𝒪_𝒴).

def quasicoherentDirectImageIsoComposite :
    quasicoherentDirectImage B S hS f ≅
      (lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳).lift (quasicoherentInclusion B S hS 𝒳)
          (lqcohSheafFbcFppfModules_quasicoherentInclusion B E h S hS 𝒳) ⋙
        lqcohSheafFbcDirectImage B E h S hS f hqc hqs ⋙
          ((lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒴).ι ⋙ coherator B S hS 𝒴)

AlgebraicGeometry.Stack.AlgebraicStacks.quasicoherentHigherDirectImageIsoComposite, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentHigherDirectImageDeltaFunctor.lean, line 156. The attribute's comment: “R^i f_{QCoh,} is the composite QCoh(O_X) → LQCoh^fbc(O_X) → LQCoh^fbc(O_Y) → QCoh(O_Y) of the inclusion, R^i f_ of Stacks 0771 and Q of Stacks 0778”.

Stacks 077A: Rⁱf_{QCoh,*} is the composite QCoh(𝒪_𝒳) → LQCoh^fbc(𝒪_𝒳) → LQCoh^fbc(𝒪_𝒴) → QCoh(𝒪_𝒴) of the inclusion, the higher direct image Rⁱf_* of Stacks 0771 and the coherator Q of Stacks 0778.

def quasicoherentHigherDirectImageIsoComposite (i : ℕ) :
    quasicoherentHigherDirectImage B S hS f i ≅
      (lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳).lift (quasicoherentInclusion B S hS 𝒳)
          (lqcohSheafFbcFppfModules_quasicoherentInclusion B E h S hS 𝒳) ⋙
        lqcohSheafFbcHigherDirectImage B E h S hS f hqc hqs i ⋙
          ((lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒴).ι ⋙ coherator B S hS 𝒴)

AlgebraicGeometry.Stack.AlgebraicStacks.quasicoherentHigherDirectImageDeltaFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentHigherDirectImageDeltaFunctor.lean, line 172. The attribute's comment: “second assertion: {R^i f_{QCoh,*}}_{i ≥ 0} forms a cohomological δ-functor QCoh(O_X) ⥤ QCoh(O_Y), for f quasi-compact and quasi-separated”.

Stacks 077A, the second assertion: {Rⁱf_{QCoh,*}}_{i ≥ 0} is a cohomological δ-functor (Stacks 010Q) QCoh(𝒪_𝒳) ⥤ QCoh(𝒪_𝒴), for a quasi-compact and quasi-separated 1-morphism f of algebraic stacks. Its degree-i functor is AlgebraicGeometry.Stack.AlgebraicStacks.quasicoherentHigherDirectImage (by rfl), the composite Q ∘ Rⁱf_* ∘ i.

def quasicoherentHigherDirectImageDeltaFunctor :
    DeltaFunctor (quasicoherentModules B S hS 𝒳) (quasicoherentModules B S hS 𝒴)

AlgebraicGeometry.Stack.quasicoherentPushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentPushforward.lean, line 349. The attribute's comment: “f_{QCoh,*} as the composite of the inclusion of Stacks 06WG, the direct image of Stacks 06WE on all modules, and the coherator of Stacks 0781 part (2); the coherator's three special-adjoint-functor-theorem inputs from Stacks 0781 part (1) are carried as the named hypotheses hclosed, hwp, hsep”.

Stacks 077A: the quasi-coherent direct image f_{QCoh,*}. Include the quasi-coherent modules of 𝒳 into all modules on its associated fppf site, take the direct image of Stacks 06WE, and come back with the coherator of Stacks 0781 part (2).

The source's middle slot is the direct image of Stacks 0771 on LQCoh^fbc(𝒪_𝒳) and its coherator is the one of Stacks 0778; the two readings agree on the quasi-compact and quasi-separated 1-morphisms the source states 077A for, and this one needs neither hypothesis. See the implementation notes.

def quasicoherentPushforward :
    FibredSite.quasicoherentModules.{u, u + 1, u, u + 1} B S hS p hp ⥤
      FibredSite.quasicoherentModules.{u, u + 1, u, u + 1} B S hS q hq

AlgebraicGeometry.Stack.higherDirectImageQuasicoherent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentPushforward.lean, line 361. The attribute's comment: “R^i f_{QCoh,*} as the same composite with the i-th higher direct image of modules in the middle slot; the coherator's three inputs from Stacks 0781 part (1) are carried as the named hypotheses hclosed, hwp, hsep”.

Stacks 077A: the higher direct images R^i f_{QCoh,*}. The composite defining f_{QCoh,*} with the i-th higher direct image of modules in its middle slot.

def higherDirectImageQuasicoherent (i : ℕ) :
    FibredSite.quasicoherentModules.{u, u + 1, u, u + 1} B S hS p hp ⥤
      FibredSite.quasicoherentModules.{u, u + 1, u, u + 1} B S hS q hq

AlgebraicGeometry.Stack.quasicoherentPullbackPushforwardAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentPushforward.lean, line 378. The attribute's comment: “the assertion: the inverse image of quasi-coherent modules is left adjoint to f_{QCoh,*}; the coherator's three inputs from Stacks 0781 part (1) are carried as the named hypotheses hclosed, hwp, hsep”.

Stacks 077A, the assertion itself: f^* on quasi-coherent modules has the right adjoint f_{QCoh,*}.

The adjunction f^* ⊣ f_* of Stacks 06WE composed with the coherator adjunction of Stacks 0781 part (2) is an adjunction between QCoh(𝒪_𝒴) and all of Mod(𝒪_𝒳); restricting it along the fully faithful inclusion of QCoh(𝒪_𝒳), which is possible because f^* preserves quasi-coherence by Stacks 06WH, is the asserted adjunction.

def quasicoherentPullbackPushforwardAdjunction :
    quasicoherentModulePullback B S hS p q hp hq f hf ⊣
      quasicoherentPushforward B S hS p q hp hq f hf hclosed hwp hsep

AlgebraicGeometry.Stack.AlgebraicStacks.fppfQuasicoherentPushforward, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentPushforward.lean, line 440. The attribute's comment: “g_{QCoh,*} for a 1-morphism of algebraic stacks over S; the coherator's three inputs from Stacks 0781 part (1) are carried as the named hypotheses hclosed, hwp, hsep”.

Stacks 077A for a 1-morphism of algebraic stacks: the quasi-coherent direct image g_{QCoh,*} : QCoh(𝒪_𝒳) ⥤ QCoh(𝒪_𝒴).

abbrev fppfQuasicoherentPushforward :
    fppfQuasicoherentModules B S hS 𝒳 ⥤ fppfQuasicoherentModules B S hS 𝒴

AlgebraicGeometry.Stack.AlgebraicStacks.fppfHigherDirectImageQuasicoherent, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentPushforward.lean, line 452. The attribute's comment: “R^i g_{QCoh,*} for a 1-morphism of algebraic stacks over S; the coherator's three inputs from Stacks 0781 part (1) are carried as the named hypotheses hclosed, hwp, hsep”.

Stacks 077A for a 1-morphism of algebraic stacks: the higher direct images R^i g_{QCoh,*} : QCoh(𝒪_𝒳) ⥤ QCoh(𝒪_𝒴). This is the higher direct image of modules on the fppf sites, the Rⁱf_* of Stacks 0770, read in QCoh(𝒪_𝒴) rather than in all of Mod(𝒪_𝒴).

abbrev fppfHigherDirectImageQuasicoherent (i : ℕ) :
    fppfQuasicoherentModules B S hS 𝒳 ⥤ fppfQuasicoherentModules B S hS 𝒴
Tag 0GQQ, a lemma

Tag 0GQQ in the Stacks Project.

AlgebraicGeometry.Stack.isIso_app_quasicoherentDirectImageOfEtale_counit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentDirectImageFlatObject.lean, line 221. The attribute's comment: “the canonical comparison, namely the counit of Stacks 0778, is invertible on sections over a flat object: both (f_F)(y) = (f_{QCoh,}F)(y) and (R^i f_F)(y) = (R^i f_{QCoh,}F)(y), never an unspecified isomorphism. Carried: the middle étale direct image of Stacks 077A on LQCoh^fbc, as data D exactly as in 0GQX; and hker, hcoker, which are Stacks 0779 part (2), its library form needing Stacks 0771 part (2) to reach this reading”.

Stacks 0GQQ. Let f : 𝒳 ⟶ 𝒴 be a quasi-compact and quasi-separated 1-morphism of algebraic stacks over S, let y be a flat object of 𝒴 and let ℱ be an object of QCoh(𝒪_𝒳). Then the canonical comparison from the sections at y of the quasi-coherent direct image of Stacks 077A to the sections at y of the étale direct image is invertible:

(f_*ℱ)(y) = (f_{QCoh,*}ℱ)(y) and (R^i f_*ℱ)(y) = (R^i f_{QCoh,*}ℱ)(y).

The comparison is the component at y of the counit ε : i Q(𝓖) ⟶ 𝓖 of the adjunction of Stacks 0778 at 𝓖 = D(i ℱ), whose domain is i of the composite of Stacks 077A by AlgebraicGeometry.Stack.quasicoherentToFlatBaseChange_quasicoherentDirectImageOfEtale_obj. Both halves of the source are covered at once: D is the étale direct image for the first and its i-th right derived functor for the second.

The hypotheses hker and hcoker are Stacks 0779 part (2) read at the presheaf level; see "Carried versus proved" in the module documentation for why the library's part (2) does not discharge them. Everything else is proved, by AlgebraicGeometry.Stack.isIso_app_of_isParasitic. The two hypotheses on f are named _hqc and _hqs because the argument does not consume them: they are the source's, and they stand behind the carried data D.

theorem isIso_app_quasicoherentDirectImageOfEtale_counit
    (_hqc : IsQuasiCompactMorphism B S hS f)
    (_hqs : AlgebraicStacks.IsQuasiSeparated B S hS f)
    (D : locallyQuasicoherentFlatBaseChangeModules.{u, u + 1, u} B E h S hS
        (CatFiberedInGroupoids.homFunctor f.hom ⋙ 𝒴.val.val.p)
        (isFiberedInGroupoids_homFunctor_comp B S hS f.hom) ⥤
      locallyQuasicoherentFlatBaseChangeModules.{u, u + 1, u} B E h S hS 𝒴.val.val.p
        𝒴.val.isFiberedInGroupoids)
    (F : FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS
      (CatFiberedInGroupoids.homFunctor f.hom ⋙ 𝒴.val.val.p)
      (isFiberedInGroupoids_homFunctor_comp B S hS f.hom))
    (hker : IsParasitic B S hS 𝒴 .etale
      (kernel ((flatBaseChangeQuasicoheratorAdjunction B E h S hS 𝒴.val.val.p
        𝒴.val.isFiberedInGroupoids hinc hclosed hpres hls hlsD hwp hsep).counit.app
          (D.obj ((quasicoherentToFlatBaseChange B E h S hS
            (CatFiberedInGroupoids.homFunctor f.hom ⋙ 𝒴.val.val.p)
            (isFiberedInGroupoids_homFunctor_comp B S hS f.hom) hincX).obj F))).hom.val))
    (hcoker : IsParasitic B S hS 𝒴 .etale
      (cokernel ((flatBaseChangeQuasicoheratorAdjunction B E h S hS 𝒴.val.val.p
        𝒴.val.isFiberedInGroupoids hinc hclosed hpres hls hlsD hwp hsep).counit.app
          (D.obj ((quasicoherentToFlatBaseChange B E h S hS
            (CatFiberedInGroupoids.homFunctor f.hom ⋙ 𝒴.val.val.p)
            (isFiberedInGroupoids_homFunctor_comp B S hS f.hom) hincX).obj F))).hom.val))
    (y : 𝒴.val.val.obj) (hy : flatObject B S hS 𝒴.val y) :
    IsIso (((flatBaseChangeQuasicoheratorAdjunction B E h S hS 𝒴.val.val.p
      𝒴.val.isFiberedInGroupoids hinc hclosed hpres hls hlsD hwp hsep).counit.app
        (D.obj ((quasicoherentToFlatBaseChange B E h S hS
          (CatFiberedInGroupoids.homFunctor f.hom ⋙ 𝒴.val.val.p)
          (isFiberedInGroupoids_homFunctor_comp B S hS f.hom) hincX).obj F))).hom.val.app
            (op y))

AlgebraicGeometry.Stack.AlgebraicStacks.bijective_coheratorAdjunction_counit_directImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentHigherDirectImageDeltaFunctor.lean, line 205. The attribute's comment: “(f_F)(y) = (f_{QCoh,}F)(y) and (R^i f_F)(y) = (R^i f_{QCoh,}F)(y) for f qcqs, y flat and F quasi-coherent: the adjunction maps of the coherator are bijective at y; i ≥ 0, both sides vanishing for i < 0”.

Stacks 0GQQ. Let f : 𝒳 ⟶ 𝒴 be a quasi-compact and quasi-separated 1-morphism of algebraic stacks, y an object of 𝒴 such that y : V → 𝒴 is flat, and 𝓕 a quasi-coherent 𝒪_𝒳-module. Then (f_*𝓕)(y) = (f_{QCoh,*}𝓕)(y) and (Rⁱf_*𝓕)(y) = (Rⁱf_{QCoh,*}𝓕)(y) for all i: the adjunction maps f_{QCoh,*}𝓕 = Q(f_*𝓕) ⟶ f_*𝓕 and Rⁱf_{QCoh,*}𝓕 = Q(Rⁱf_*𝓕) ⟶ Rⁱf_*𝓕 of the coherator are bijective on sections at y. Both f_*𝓕 and Rⁱf_*𝓕 lie in LQCoh^fbc(𝒪_𝒴), so the kernels and cokernels of those maps are parasitic by Stacks 0779 part (2), and vanish at y. For i < 0 both sides are zero.

theorem bijective_coheratorAdjunction_counit_directImage (F : quasicoherentModules B S hS 𝒳)
    (y : 𝒴.val.val.obj) (hy : flatObject B S hS 𝒴.val y) :
    Function.Bijective (((coheratorAdjunction B S hS 𝒴).counit.app
        ((fppfModulesPushforward B S hS f).obj ((quasicoherentInclusion B S hS 𝒳).obj F))).val.app
          (op y)) ∧
      ∀ i, Function.Bijective (((coheratorAdjunction B S hS 𝒴).counit.app
        ((fppfModulesHigherDirectImage B S hS f i).obj
          ((quasicoherentInclusion B S hS 𝒳).obj F))).val.app (op y))
Tag 0GQR, a remark

Tag 0GQR in the Stacks Project.

AlgebraicGeometry.FibredSite.directImageNaiveCupProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentDirectImageCupProduct.lean, line 250. The attribute's comment: “the vertical arrow c on the right, the naive relative cup product in degree 0”.

The naive relative cup product in degree 0 (Stacks 0FPJ), the right vertical arrow c of Stacks 0GQR: f_*𝓕 ⊗ f_*𝓖 ⟶ f_*(𝓕 ⊗ 𝓖), adjoint to the comparison of Stacks 03EL followed by the counit of f^* ⊣ f_* in each factor. It is Stacks.Cohomology.DegreeZeroCupProduct.naiveRelativeCupProduct at this morphism of ringed topoi.

def directImageNaiveCupProduct (M N : quasicoherentModules.{u, u + 1, u, u} B S hS p hp) :
    (fppfSheafTensor B S hS q hq).obj
        ((fppfPushforwardModules B S hS p q hp hq F hF).obj
            ((quasicoherentModulesInclusion B S hS p hp).obj M),
          (fppfPushforwardModules B S hS p q hp hq F hF).obj
            ((quasicoherentModulesInclusion B S hS p hp).obj N)) ⟶
      (fppfPushforwardModules B S hS p q hp hq F hF).obj
        ((quasicoherentModulesInclusion B S hS p hp).obj
          ((quasicoherentSheafTensor B S hS p hp).obj (M, N)))

AlgebraicGeometry.Stack.AlgebraicStacks.quasicoherentCupProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentDirectImageCupProduct.lean, line 336. The attribute's comment: “the left vertical arrow, Q applied to c through the comparison of Remark 0GQM”.

The left vertical arrow of Stacks 0GQR, f_{QCoh,*}𝓕 ⊗ f_{QCoh,*}𝓖 ⟶ f_{QCoh,*}(𝓕 ⊗ 𝓖), for a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks: Q(c) precomposed with the comparison Q(A) ⊗ Q(B) ⟶ Q(A ⊗ B) of Remark 0GQM (AlgebraicGeometry.Stack.AlgebraicStacks.quasicoherentCupProduct_eq). Here f_{QCoh,*} = Q ∘ f_* ∘ i, with f_* the direct image of the morphism of ringed topoi f induces and Q the coherator AlgebraicGeometry.Stack.AlgebraicStacks.coherator of 𝒴.

def quasicoherentCupProduct (𝓕 𝓖 : quasicoherentModules B S hS 𝒳) :
    (tensorQ𝒴).obj ((Q𝒴).obj ((fStar).obj ((i𝒳).obj 𝓕)), (Q𝒴).obj ((fStar).obj ((i𝒳).obj 𝓖))) ⟶
      (Q𝒴).obj ((fStar).obj ((i𝒳).obj ((tensorQ𝒳).obj (𝓕, 𝓖))))

AlgebraicGeometry.Stack.AlgebraicStacks.map_quasicoherentCupProduct_comp_counit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentDirectImageCupProduct.lean, line 396. The attribute's comment: “commutativity of the diagram, for a quasi-compact quasi-separated 1-morphism of algebraic stacks”.

Stacks 0GQR. Let f : 𝒳 ⟶ 𝒴 be a quasi-compact and quasi-separated 1-morphism of algebraic stacks and let 𝓕, 𝓖 be quasi-coherent 𝒪_𝒳-modules. The square

f_{QCoh,*}𝓕 ⊗ f_{QCoh,*}𝓖 ───→ f_*𝓕 ⊗ f_*𝓖
        │                              │ c
        ↓                              ↓
f_{QCoh,*}(𝓕 ⊗ 𝓖) ─────────→ f_*(𝓕 ⊗ 𝓖)

commutes: the left vertical arrow (AlgebraicGeometry.Stack.AlgebraicStacks.quasicoherentCupProduct, the comparison of Remark 0GQM followed by Q(c)) followed by the counit Q ⟶ id at f_*(𝓕 ⊗ 𝓖) equals the top arrow (i commuting with ⊗, then the counit at f_*𝓕 and at f_*𝓖) followed by the naive relative cup product c (AlgebraicGeometry.FibredSite.directImageNaiveCupProduct). f_* is the direct image along the morphism of ringed topoi f induces, and Q is the coherator AlgebraicGeometry.Stack.AlgebraicStacks.coherator of 𝒴, which takes no input.

theorem map_quasicoherentCupProduct_comp_counit
    (_hqc : IsQuasiCompactMorphism B S hS f) (_hqs : AlgebraicStacks.IsQuasiSeparated B S hS f)
    (𝓕 𝓖 : quasicoherentModules B S hS 𝒳) :
    (i𝒴).map (quasicoherentCupProduct B S hS f 𝓕 𝓖) ≫
        (adjQ).counit.app ((fStar).obj ((i𝒳).obj ((tensorQ𝒳).obj (𝓕, 𝓖)))) =
      (tensorIso𝒴).hom.app ((Q𝒴).obj ((fStar).obj ((i𝒳).obj 𝓕)),
          (Q𝒴).obj ((fStar).obj ((i𝒳).obj 𝓖))) ≫
        (tensor𝒴).map ((adjQ).counit.app ((fStar).obj ((i𝒳).obj 𝓕)) ×ₘ
          (adjQ).counit.app ((fStar).obj ((i𝒳).obj 𝓖))) ≫
        cupC 𝓕 𝓖

AlgebraicGeometry.Stack.AlgebraicStacks.quasicoherentCupProduct_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentDirectImageCupProduct.lean, line 413. The attribute's comment: “the construction is functorial in F and G: the left vertical arrow”.

Stacks 0GQR, functoriality of the left vertical arrow in 𝓕 and 𝓖, for a quasi-compact quasi-separated 1-morphism of algebraic stacks.

theorem quasicoherentCupProduct_natural
    (_hqc : IsQuasiCompactMorphism B S hS f) (_hqs : AlgebraicStacks.IsQuasiSeparated B S hS f)
    {𝓕 𝓕' 𝓖 𝓖' : quasicoherentModules B S hS 𝒳} (a : 𝓕 ⟶ 𝓕') (b : 𝓖 ⟶ 𝓖') :
    (tensorQ𝒴).map ((fQCoh).map a ×ₘ (fQCoh).map b) ≫ quasicoherentCupProduct B S hS f 𝓕' 𝓖' =
      quasicoherentCupProduct B S hS f 𝓕 𝓖 ≫ (fQCoh).map ((tensorQ𝒳).map (a ×ₘ b))

AlgebraicGeometry.Stack.AlgebraicStacks.quasicoherentNaiveCupProduct_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentDirectImageCupProduct.lean, line 428. The attribute's comment: “the construction is functorial in F and G: the arrow c”.

Stacks 0GQR, functoriality of the naive relative cup product c in 𝓕 and 𝓖, for a quasi-compact quasi-separated 1-morphism of algebraic stacks.

theorem quasicoherentNaiveCupProduct_natural
    (_hqc : IsQuasiCompactMorphism B S hS f) (_hqs : AlgebraicStacks.IsQuasiSeparated B S hS f)
    {𝓕 𝓕' 𝓖 𝓖' : quasicoherentModules B S hS 𝒳} (a : 𝓕 ⟶ 𝓕') (b : 𝓖 ⟶ 𝓖') :
    (tensor𝒴).map ((fStar).map ((i𝒳).map a) ×ₘ (fStar).map ((i𝒳).map b)) ≫ cupC 𝓕' 𝓖' =
      cupC 𝓕 𝓖 ≫ (fStar).map ((i𝒳).map ((tensorQ𝒳).map (a ×ₘ b)))

Stacks.Cohomology.DegreeZeroCupProduct.naiveRelativeCupProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/DegreeZeroCupProductAndCoherator.lean, line 140. The attribute's comment: “the vertical arrow c on the right, for a morphism of ringed topoi”.

The naive relative cup product in degree zero, the map f_*F ⊗_{O_D} f_*G ⟶ f_*(F ⊗_{O_C} G) adjoint to the comparison of Tag 03EL followed by the counit of f^* ⊣ f_* in each tensor factor.

def naiveRelativeCupProduct
    (F G : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) :
    (Functor.uncurry.obj (sheafTensor.{u', v', w', w', w'} Y.O)).obj
          ((pushforwardModules f).obj F, (pushforwardModules f).obj G) ⟶
      (pushforwardModules f).obj
        ((Functor.uncurry.obj (sheafTensor.{u, v, w, w, w} X.O)).obj (F, G))

Stacks.Cohomology.DegreeZeroCupProduct.quasicoherentRelativeCupProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/DegreeZeroCupProductAndCoherator.lean, line 180. The attribute's comment: “the left vertical arrow, over an adjunction with a tensor comparison”.

The naive relative cup product in degree zero carried through the comparison attached to the adjunction adj : i ⊣ Q and the tensor comparison α: the canonical map A(Q(f_*F), Q(f_*G)) ⟶ Q(f_*F ⊗ f_*G) followed by Q applied to c.

def quasicoherentRelativeCupProduct
    (F G : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) :
    A.obj (Q.obj ((pushforwardModules f).obj F), Q.obj ((pushforwardModules f).obj G)) ⟶
      Q.obj ((pushforwardModules f).obj
        ((Functor.uncurry.obj (sheafTensor.{u, v, w, w, w} X.O)).obj (F, G)))

Stacks.Cohomology.DegreeZeroCupProduct.map_quasicoherentRelativeCupProduct_comp_counit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/DegreeZeroCupProductAndCoherator.lean, line 192. The attribute's comment: “commutativity of the diagram, over an adjunction with a tensor comparison”.

The square commutes. Going right along the upper horizontal arrow — the comparison α followed by the counit of adj in each tensor factor — and then down c agrees with going down the left vertical arrow and then right along the counit of adj.

theorem map_quasicoherentRelativeCupProduct_comp_counit
    (F G : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) :
    i.map (quasicoherentRelativeCupProduct f adj A α F G) ≫
        adj.counit.app ((pushforwardModules f).obj
          (((sheafTensor.{u, v, w, w, w} X.O).obj F).obj G)) =
      α.app (Q.obj ((pushforwardModules f).obj F), Q.obj ((pushforwardModules f).obj G)) ≫
        (Functor.uncurry.obj (sheafTensor.{u', v', w', w', w'} Y.O)).map
            (adj.counit.app ((pushforwardModules f).obj F) ×ₘ
              adj.counit.app ((pushforwardModules f).obj G)) ≫
          naiveRelativeCupProduct f F G

Stacks.Cohomology.DegreeZeroCupProduct.quasicoherentRelativeCupProduct_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/DegreeZeroCupProductAndCoherator.lean, line 207. The attribute's comment: “functoriality in the two modules, over an adjunction with a tensor comparison”.

The construction is functorial in the two modules.

theorem quasicoherentRelativeCupProduct_natural
    {F F' G G' : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)}
    (u : F ⟶ F') (v : G ⟶ G') :
    A.map (Q.map ((pushforwardModules f).map u) ×ₘ Q.map ((pushforwardModules f).map v)) ≫
        quasicoherentRelativeCupProduct f adj A α F' G' =
      quasicoherentRelativeCupProduct f adj A α F G ≫
        Q.map ((pushforwardModules f).map
          ((Functor.uncurry.obj (sheafTensor.{u, v, w, w, w} X.O)).map (u ×ₘ v)))
Tag 0782, a lemma

Tag 0782 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.exists_quasicoherentLeraySpectralSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentLeraySpectralSequence.lean, line 83. The attribute's comment: “the whole statement, with modules at the module universe u of the schemes; cohomology the right derived functors of Hom(𝒪, -), valued in AddCommGrpCat.{u + 1}”.

Stacks 0782. Let f : 𝒳 ⟶ 𝒴 be a quasi-compact and quasi-separated 1-morphism of algebraic stacks and ℱ a quasi-coherent 𝒪_𝒳-module. There is a spectral sequence with E_2^{p,q} = H^p(𝒴, R^q f_{QCoh,*} ℱ) converging to H^{p+q}(𝒳, ℱ).

The second page is identified for p, q ≥ 0, vanishes outside the first quadrant, and the sequence abuts to H^n(𝒳, ℱ). Here R^q f_{QCoh,*} is AlgebraicGeometry.Stack.AlgebraicStacks.quasicoherentHigherDirectImage (Stacks 077A), and H^p is the right derived functor of Hom(𝒪, -) on modules at the universe u of the schemes, with values in AddCommGrpCat.{u + 1}.

theorem exists_quasicoherentLeraySpectralSequence
    (hqc : IsQuasiCompactMorphism B S hS f) (hqs : AlgebraicStacks.IsQuasiSeparated B S hS f)
    (F : quasicoherentModules B S hS 𝒳) :
    ∃ E : CohomologicalSpectralSequence AddCommGrpCat.{u + 1} 0,
      (∀ p q : ℕ, Nonempty ((E.page 2 zero_le_two).X ((p : ℤ), (q : ℤ)) ≅
        ((preadditiveCoyoneda.obj (Opposite.op (SheafOfModules.unit _))).rightDerivedPlus
          (p : ℤ)).obj ((quasicoherentInclusion B S hS 𝒴).obj
            ((quasicoherentHigherDirectImage B S hS f q).obj F)))) ∧
      (∀ p q : ℤ, p < 0 ∨ q < 0 → IsZero ((E.page 2 zero_le_two).X (p, q))) ∧
      SpectralSequence.AbutsTo E (fun n =>
        ((preadditiveCoyoneda.obj (Opposite.op (SheafOfModules.unit _))).rightDerivedPlus n).obj
          ((quasicoherentInclusion B S hS 𝒳).obj F))

Stacks.Cohomology.Leray.exists_quasicoherentLeraySpectralSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Modules/CoheratorLeraySpectralSequence.lean, line 348. The attribute's comment: “the spectral sequence H^p(𝒴, R^q f_{QCoh,} ℱ) ⟹ H^{p+q}(𝒳, ℱ), read in abelian groups FOR A MORPHISM OF RINGED TOPOI, NOT for a morphism of algebraic stacks as the source states it. This is NOT a generalization of the tag: it does not instantiate to the source's setting, because the Leray sequence of 0732 here lives at RingedTopos.{u, u, u} while the ringed topos of an algebraic stack is RingedTopos.{u, u+1, u}, so the two cannot be matched up; the three universe blockers are set out in this module's docstring. The tag's own statement, over algebraic stacks, therefore remains undelivered. Further carried here: the coherator Q of 0778, as a coreflection, and the two lemmas the proof cites — 0779 part (2), that the kernel and cokernel of Q 𝓖 ⟶ 𝓖 are parasitic, and 0775 part (1), that a parasitic module has vanishing cohomology — as the hypotheses hker, hcoker and hvanish. 077A, which builds f_{QCoh,} and is where quasi-compactness and quasi-separatedness enter, is not proved and is absent from the library: only its definition R^q f_{QCoh,} = Q ∘ R^q f_ is reproduced”. References: SGA 4 V (5.3), “more general”; SGA 4 V (5.4), “special case”.

Stacks 0782, the Leray spectral sequence for the quasi-coherent direct image, read in abelian groups. Let f : (Sh(C), 𝒪_C) → (Sh(D), 𝒪_D) be a morphism of ringed topoi standing for a quasi-compact quasi-separated morphism f : 𝒳 → 𝒴 of algebraic stacks, and let K be a bounded below complex of 𝒪_C-modules, standing for the quasi-coherent module ℱ placed in degree zero. Suppose given

  • a coreflection incl ⊣ coherator of Mod(𝒪_D) onto a category 𝒬: this is the coherator of Stacks 0778, Q : LQCoh^fbc(𝒪_𝒴) ⥤ QCoh(𝒪_𝒴), with its adjunction, whose counit Q 𝓖 ⟶ 𝓖 is the adjunction map the source's proof uses;
  • a class Parasitic of modules on D: the parasitic modules of Stacks 0773;
  • hker and hcoker: the kernel and the cokernel of the counit are parasitic, which is Stacks 0779 part (2);
  • hvanish: a parasitic module has vanishing cohomology, which is Stacks 0775 part (1).

Then there is a spectral sequence with

E_2^{p,q} = H^p(𝒴, R^q f_{QCoh,*} ℱ)

converging to H^{p+q}(𝒳, ℱ), where R^q f_{QCoh,*} is Stacks.Cohomology.Leray.quasicoherentHigherDirectImage, the composite of Stacks 077A.

The spectral sequence is the one of Stacks 0732, Stacks.Cohomology.Leray.exists_leraySpectralSequence, and its abutment clause is that theorem's abutment clause unchanged. What is added is the identification of its second page: Stacks.Cohomology.isIso_rightDerivedPlus_map_of_isZero_kernel_cokernel turns the counit Q(R^q f_* ℱ) ⟶ R^q f_* ℱ, whose kernel and cokernel are acyclic by hker, hcoker and hvanish, into an isomorphism H^p(𝒴, Q(R^q f_* ℱ)) ≅ H^p(𝒴, R^q f_* ℱ) in every degree. That is precisely the step the source performs and calls formal.

See the module documentation for why the coherator and the two cited lemmas are carried as hypotheses rather than instantiated: the Leray spectral sequence of this development is available only at RingedTopos.{u, u, u}, while the ringed topos of an algebraic stack has its site one universe up, and the coherator, the higher direct images and the cohomology of an algebraic stack are formalized over three mutually incomparable categories of modules.

theorem exists_quasicoherentLeraySpectralSequence {𝒬 : Type u₁} [Category.{v₁} 𝒬]
    (incl : 𝒬 ⥤ SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))
    (coherator : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O) ⥤ 𝒬) (adj : incl ⊣ coherator)
    (Parasitic : ObjectProperty (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)))
    (hvanish : ∀ P : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O), Parasitic P → ∀ p : ℕ,
      IsZero (((globalSectionsAb Y).rightDerivedPlus (p : ℤ)).obj P))
    (hker : ∀ M : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O),
      Parasitic (kernel (adj.counit.app M)))
    (hcoker : ∀ M : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O),
      Parasitic (cokernel (adj.counit.app M)))
    (K : DerivedCategory.Plus (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
    ∃ E : CohomologicalSpectralSequence AddCommGrpCat.{u} 0,
      (∀ p q : ℤ, Nonempty ((E.page 2 zero_le_two).X (p, q) ≅
        ((globalSectionsAb Y).rightDerivedPlus p).obj
          (incl.obj ((quasicoherentHigherDirectImage f coherator q).obj K)))) ∧
      SpectralSequence.AbutsTo E (fun n =>
        (DerivedCategory.Plus.homologyFunctor AddCommGrpCat.{u} n).obj
          ((globalSectionsAb X).rightDerivedFunctorPlus.obj K))
Tag 0783, a lemma

Tag 0783 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.exists_quasicoherentRelativeLeraySpectralSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentRelativeLeraySpectralSequence.lean, line 271. The attribute's comment: “the spectral sequence E_2^{p,q} = R^p g_{QCoh,}(R^q f_{QCoh,} F) converging to R^{p+q}(g ∘ f)_{QCoh,*} F for qcqs morphisms of algebraic stacks, modules at the universe u of the schemes”.

Stacks 0783: the relative Leray spectral sequence for the quasi-coherent direct image. Let f : 𝒳 ⟶ 𝒴 and g : 𝒴 ⟶ 𝒵 be quasi-compact and quasi-separated 1-morphisms of algebraic stacks and let ℱ be a quasi-coherent 𝒪_𝒳-module. There is a spectral sequence of quasi-coherent 𝒪_𝒵-modules, from its second page on, with

E_2^{p,q} = R^p g_{QCoh,*}(R^q f_{QCoh,*} ℱ)

(zero outside the first quadrant) converging to R^{p+q}(g ∘ f)_{QCoh,*} ℱ: it abuts to n ↦ R^n(g ∘ f)_{QCoh,*} ℱ, zero in negative degrees. Here R^i (-)_{QCoh,*} is AlgebraicGeometry.Stack.AlgebraicStacks.quasicoherentHigherDirectImage, the composite Q ∘ R^i(-)_* ∘ i of Stacks 077A, and QCoh(𝒪_𝒵) carries its abelian structure AlgebraicGeometry.Stack.AlgebraicStacks.instAbelianQuasicoherentModules; modules have sections in the universe u of the schemes.

The proof is the source's: the Grothendieck spectral sequence of (g ∘ f)_* = g_* ∘ f_* on fppf modules (Stacks 0734 for stacks), pushed along the coherator Q_𝒵, which is exact on LQCoh^fbc(𝒪_𝒵) (Stacks 0779 (3)) where all of its terms lie from the second page on (Stacks 0771 (2), (4)(b)); the second page is identified through the counit Q_𝒴(R^q f_*ℱ) ⟶ R^q f_*ℱ, whose kernel and cokernel are parasitic (Stacks 0779 (1)), hence carried by R^p g_* to parasitic modules (Stacks 0775 (2)) which Q_𝒵 kills.

theorem exists_quasicoherentRelativeLeraySpectralSequence
    (hfqc : IsQuasiCompactMorphism B S hS f) (hfqs : AlgebraicStacks.IsQuasiSeparated B S hS f)
    (hgqc : IsQuasiCompactMorphism B S hS g) (hgqs : AlgebraicStacks.IsQuasiSeparated B S hS g)
    (ℱ : quasicoherentModules B S hS 𝒳) :
    ∃ E : CohomologicalSpectralSequence (quasicoherentModules B S hS 𝒵) 2,
      (∀ p q : ℕ, Nonempty ((E.page 2 le_rfl).X ((p : ℤ), (q : ℤ)) ≅
        (quasicoherentHigherDirectImage B S hS g p).obj
          ((quasicoherentHigherDirectImage B S hS f q).obj ℱ))) ∧
      (∀ p q : ℤ, p < 0 ∨ q < 0 → IsZero ((E.page 2 le_rfl).X (p, q))) ∧
      SpectralSequence.AbutsTo E (extendNatByZero fun n =>
        (quasicoherentHigherDirectImage B S hS (f ≫ g) n).obj ℱ)

Stacks.Cohomology.Leray.exists_quasicoherentRelativeLeraySpectralSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Modules/CoheratorRelativeLeraySpectralSequence.lean, line 337. The attribute's comment: “the E₂ page R^p g_{QCoh,}(R^q f_{QCoh,} ℱ) and convergence, FOR RINGED TOPOI, not algebraic stacks, hence NOT a generalization: 0734 is proved at RingedTopos.{u,u,u}, a stack's is {u,u+1,u}. Carried: the 0778 coherators, 0779(3)(2)(1) and 0775(2), the last absent here; 077A is absent too, only its recipe Q ∘ R^i(-)_* ∘ i is reused. See the module docstring”. References: EGA 0 (12.2.4), “more general”; SGA 2 VIII (3.1), “more general”; SGA 4 V (5.3), “more general”; SGA 4 V (5.4), “more general”; SGA 4½ Arcata (2.3.3), “more general”.

Stacks 0783, the relative Leray spectral sequence for the quasi-coherent direct image. Let f : (Sh(C), 𝒪_C) → (Sh(D), 𝒪_D) and g : (Sh(D), 𝒪_D) → (Sh(E), 𝒪_E) be morphisms of ringed topoi standing for quasi-compact quasi-separated morphisms f : 𝒳 → 𝒴 and g : 𝒴 → 𝒵 of algebraic stacks, with g ∘ f presented as their composite by a comparison τ of the geometric direct images, and let K be a bounded below complex of 𝒪_C-modules, standing for the quasi-coherent sheaf ℱ placed in degree zero. Suppose given

  • a coreflection inclY ⊣ coheratorY of Mod(𝒪_D) onto a category 𝒬_Y: this is the coherator of Stacks 0778, Q_𝒴 : LQCoh^fbc(𝒪_𝒴) ⥤ QCoh(𝒪_𝒴), with its adjunction, whose counit Q_𝒴 𝓖 ⟶ 𝓖 is the adjunction map the source's proof uses;
  • an exact functor coheratorZ from Mod(𝒪_E) to a category 𝒬_Z: the coherator of Stacks 0778 on 𝒵, exact by Stacks 0779 part (3), which is the functor the source applies to the whole spectral sequence;
  • a class Parasitic of modules on D: the parasitic modules of Stacks 0773;
  • hker and hcoker: the kernel and the cokernel of the counit are parasitic, which is Stacks 0779 part (2);
  • hvanish: Q_𝒵 ∘ R^p g_* kills a parasitic module, which is Stacks 0775 part (2) followed by Stacks 0779 part (1).

Then there is a spectral sequence with

E_2^{p,q} = R^p g_{QCoh,*}(R^q f_{QCoh,*} ℱ)

converging to R^{p+q}(g ∘ f)_{QCoh,*} ℱ, where the two quasi-coherent higher direct images are Stacks.Cohomology.Leray.quasicoherentRelativeHigherDirectImage and Stacks.Cohomology.Leray.quasicoherentHigherDirectImage, the composites of Stacks 077A, and the abutment is Q_𝒵 applied to R^{p+q}(g ∘ f)_*ℱ, which is the same composite in degree p + q.

See the module documentation for why the coherators and the cited lemmas are carried as hypotheses rather than instantiated.

theorem exists_quasicoherentRelativeLeraySpectralSequence {𝒬Y : Type u₁} [Category.{v₁} 𝒬Y]
    {𝒬Z : Type u₂} [Category.{v₂} 𝒬Z] [Abelian 𝒬Z]
    (inclY : 𝒬Y ⥤ SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))
    (coheratorY : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O) ⥤ 𝒬Y)
    (adjY : inclY ⊣ coheratorY)
    (coheratorZ : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Z.O) ⥤ 𝒬Z)
    [coheratorZ.Additive] [coheratorZ.PreservesHomology] [coheratorZ.PreservesMonomorphisms]
    (Parasitic : ObjectProperty (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)))
    (hvanish : ∀ P : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O),
      Parasitic P → ∀ p : ℕ,
        IsZero (coheratorZ.obj (((pushforwardModules g).rightDerivedPlus (p : ℤ)).obj P)))
    (hker : ∀ M : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O),
      Parasitic (kernel (adjY.counit.app M)))
    (hcoker : ∀ M : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O),
      Parasitic (cokernel (adjY.counit.app M)))
    (K : DerivedCategory.Plus (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
    ∃ E : CohomologicalSpectralSequence 𝒬Z 0,
      (∀ p q : ℤ, Nonempty ((E.page 2 zero_le_two).X (p, q) ≅
        (quasicoherentRelativeHigherDirectImage g inclY coheratorZ p).obj
          ((quasicoherentHigherDirectImage f coheratorY q).obj K))) ∧
      SpectralSequence.AbutsTo E (fun n => coheratorZ.obj
        ((DerivedCategory.Plus.homologyFunctor
          (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Z.O)) n).obj
            ((pushforwardModules gf).rightDerivedFunctorPlus.obj K)))
Tag 0784, a proposition

Tag 0784 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.exists_fppfSpectralSequenceData_module, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatCoveringSpectralSequence.lean, line 123. The attribute's comment: “the E₁ form, which is what Sheaves on Stacks 06XJ gives and what makes the first differential the Čech differential; the tag's own text writes E₂. Stated for an arbitrary sheaf of modules rather than only a quasi-coherent one. Carries the hypothesis that 𝒰 has equalizers, as Tag 06XJ does”.

Stacks 0784. Let f : 𝒰 ⟶ 𝒳 be a 1-morphism of algebraic stacks which is representable by algebraic spaces, surjective, flat and locally of finite presentation, and let F be a sheaf of 𝒪_𝒳-modules. Then there is a first-quadrant spectral sequence E₁^{p,q} = H^q_fppf(𝒰ₚ, fₚ^*F) ⇒ H^{p+q}_fppf(𝒳, F), where 𝒰ₚ is the degree p term of the relative Čech nerve of f and fₚ its projection to 𝒳; the identification of the first page is AlgebraicGeometry.Stack.AlgebraicStacks.pageOneIsoModule.

The source assumes F quasi-coherent; the spectral sequence needs no such hypothesis, so it is stated here for an arbitrary sheaf of 𝒪_𝒳-modules, which contains the source's statement. No hypothesis that 𝒰 has equalizers is needed.

theorem exists_fppfSpectralSequenceData_module
    (F : SheafOfModules.{max (u + 1) a} (FibredSite.ringStructureSheafCore B S hS
      𝒳.val.val.p 𝒳.val.isFiberedInGroupoids SiteKind.fppf)) :
    Nonempty (Stacks.RelativeCech.SpectralSequenceData B S hS 𝒳.val.val.p
      (CatFiberedInGroupoids.homFunctor f.hom) SiteKind.fppf
      (fppfAbelianSheaf B S hS F))

AlgebraicGeometry.Stack.AlgebraicStacks.pageOneIsoModule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatCoveringSpectralSequence.lean, line 136. The attribute's comment: “the reading of the E₁ page as the cohomology of the inverse image of the module”.

Stacks 0784, the first page. The term of the spectral sequence of a flat presentation in position (p, q) is the degree q fppf cohomology, on the degree p term 𝒰ₚ of the relative Čech nerve, of the inverse image fₚ^*F of the module F.

def pageOneIsoModule
    (F : SheafOfModules.{max (u + 1) a} (FibredSite.ringStructureSheafCore B S hS
      𝒳.val.val.p 𝒳.val.isFiberedInGroupoids SiteKind.fppf))
    (data : Stacks.RelativeCech.SpectralSequenceData B S hS 𝒳.val.val.p
      (CatFiberedInGroupoids.homFunctor f.hom) SiteKind.fppf
      (fppfAbelianSheaf B S hS F)) (i j : ℕ) :
    letI := data.continuous i
    (data.sequence.page 1).X ((i : ℤ), (j : ℤ)) ≅
      (Sheaf.functorH (BigFppfOver.associatedTopology B S hS
        (Stacks.RelativeCech.Tuple.projection 𝒳.val.val.p
          (CatFiberedInGroupoids.homFunctor f.hom) i ⋙ 𝒳.val.val.p) SiteKind.fppf) j).obj
        ((SheafOfModules.toSheaf _).obj
          ((SheafOfModules.restrictAlongContinuous
            (Stacks.RelativeCech.Tuple.projection 𝒳.val.val.p
              (CatFiberedInGroupoids.homFunctor f.hom) i)
            (FibredSite.ringStructureSheafCore B S hS 𝒳.val.val.p
              𝒳.val.isFiberedInGroupoids SiteKind.fppf)).obj F))

AlgebraicGeometry.Stack.AlgebraicStacks.exists_fppfModuleCechSpectralSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatPresentationModuleCohomology.lean, line 79. The attribute's comment: “for an arbitrary sheaf of modules, which contains the quasi-coherent case; the equalizers of 𝒰 needed by Tag 06XJ are Tag 06WY (3), proved for algebraic stacks”.

Let f : 𝒰 ⟶ 𝒳 be a 1-morphism of algebraic stacks which is representable by algebraic spaces, surjective, flat and locally of finite presentation, and let F be a sheaf of 𝒪_𝒳-modules (for instance a quasi-coherent one). Then there is a first-quadrant spectral sequence E₁^{p,q} = H^q(𝒰ₚ, fₚ^*F) ⇒ H^{p+q}(𝒳, F), where 𝒰ₚ = 𝒰 ×_𝒳 ⋯ ×_𝒳 𝒰 (p + 1 factors) is the degree p term of the relative Čech nerve of f and fₚ : 𝒰ₚ ⟶ 𝒳 its projection.

The spectral sequence, its first-quadrant vanishing and its convergence to the cohomology of F on 𝒳 are the fields of Stacks.RelativeCech.SpectralSequenceData for the abelian sheaf underlying F; the condition on that datum identifies its E₁ term at (p, q) with the degree q cohomology of the inverse image fₚ^*F of the module F on 𝒰ₚ.

theorem exists_fppfModuleCechSpectralSequence
    (hrep : Stack.IsRepresentableByAlgebraicSpaces B S hS f.hom.hom)
    (hsurj : Stack.IsSurjective B S hS f) (hflat : IsFlat B S hS f)
    (hlfp : IsLocallyOfFinitePresentation B S hS f)
    (F : SheafOfModules.{max (u + 1) a} (FibredSite.ringStructureSheafCore B S hS
      𝒳.val.val.p 𝒳.val.isFiberedInGroupoids SiteKind.fppf)) :
    ∃ data : Stacks.RelativeCech.SpectralSequenceData B S hS 𝒳.val.val.p
        (CatFiberedInGroupoids.homFunctor f.hom) SiteKind.fppf
        ((SheafOfModules.toSheaf _).obj F),
      ∀ p q : ℕ, letI := data.continuous p
        Nonempty ((data.sequence.page 1).X ((p : ℤ), (q : ℤ)) ≅
          (Sheaf.functorH (BigFppfOver.associatedTopology B S hS
            (Stacks.RelativeCech.Tuple.projection 𝒳.val.val.p
              (CatFiberedInGroupoids.homFunctor f.hom) p ⋙ 𝒳.val.val.p) SiteKind.fppf) q).obj
            ((SheafOfModules.toSheaf _).obj
              ((SheafOfModules.restrictAlongContinuous
                (Stacks.RelativeCech.Tuple.projection 𝒳.val.val.p
                  (CatFiberedInGroupoids.homFunctor f.hom) p)
                (FibredSite.ringStructureSheafCore B S hS 𝒳.val.val.p
                  𝒳.val.isFiberedInGroupoids SiteKind.fppf)).obj F)))
Tag 0785, a proposition

Tag 0785 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.exists_quasicoherentCoveringSpectralSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentCoveringSpectralSequence.lean, line 275. The attribute's comment: “the stated terms sit on the first page: the proof applies Q_𝒴 to the E₁ spectral sequence of 072G, whose first differential is the Čech differential”.

Stacks 0785. Let f : 𝒰 ⟶ 𝒳 be a 1-morphism of algebraic stacks which is representable by algebraic spaces, surjective, flat, locally of finite presentation, quasi-compact and quasi-separated, and let g : 𝒳 ⟶ 𝒴 be a quasi-compact and quasi-separated 1-morphism of algebraic stacks. For a quasi-coherent 𝒪_𝒳-module 𝓕 there is a spectral sequence in QCoh(𝒪_𝒴) with E₁^{p,q} = R^q (g ∘ fₚ)_{QCoh,*} fₚ^* 𝓕, vanishing outside the first quadrant and abutting to R^{p+q} g_{QCoh,*} 𝓕, where fₚ : 𝒰ₚ ⟶ 𝒳 is the projection of the degree p term 𝒰ₚ = 𝒰 ×_𝒳 ⋯ ×_𝒳 𝒰 of the Čech nerve of f.

The source writes the first page as E₂; its proof applies the coherator to the E₁ spectral sequence of Stacks 072G, whose first differential is the Čech differential, and that is the page on which the stated terms appear.

theorem exists_quasicoherentCoveringSpectralSequence
    (hrep : IsRepresentableByAlgebraicSpaces B S hS f.hom.hom)
    (hsurj : Stack.IsSurjective B S hS f) (hflat : IsFlat B S hS f)
    (hlfp : IsLocallyOfFinitePresentation B S hS f)
    (hfqc : IsQuasiCompactMorphism B S hS f) (hfqs : AlgebraicStacks.IsQuasiSeparated B S hS f)
    (hgqc : IsQuasiCompactMorphism B S hS g) (hgqs : AlgebraicStacks.IsQuasiSeparated B S hS g)
    (𝓕 : quasicoherentModules B S hS 𝒳) :
    ∃ D : CohomologicalSpectralSequence (quasicoherentModules B S hS 𝒴) 1,
      (∀ i j : ℕ, Nonempty ((D.page 1 le_rfl).X ((i : ℤ), (j : ℤ)) ≅
        (quasicoherentHigherDirectImage B S hS (cechNerveProjection B S hS f i ≫ g) j).obj
          ((quasicoherentPullback B S hS (cechNerveProjection B S hS f i)).obj 𝓕))) ∧
      (∀ i j : ℤ, i < 0 ∨ j < 0 → IsZero ((D.page 1 le_rfl).X (i, j))) ∧
      SpectralSequence.AbutsTo D (fun n : ℤ => if n < 0 then 0 else
        (quasicoherentHigherDirectImage B S hS g n.toNat).obj 𝓕)

AlgebraicGeometry.Stack.AlgebraicStacks.pushforwardPageOneIsoQuasicoherent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Cech/QCohCoveringSpectralSequence.lean, line 141. The attribute's comment: “the reading of the E₁ page as the higher direct image of the inverse image of the quasi-coherent module, the inverse image being taken as a sheaf of modules and the higher direct image being the abelian one along the morphism of sites”.

Stacks 0785, the first page. The term of the covering pushforward spectral sequence of a flat presentation in position (p, q) is the degree q higher direct image along g ∘ fₚ of the inverse image fₚ^*𝓕 of the quasi-coherent module 𝓕 on the degree p term 𝒰ₚ of the relative Čech nerve of f, the inverse image being taken as a sheaf of modules.

def pushforwardPageOneIsoQuasicoherent
    (𝓕 : FibredSite.quasicoherentModules.{u, u + 1, u, max (u + 1) a} B S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids)
    (data : Stacks.RelativeCech.PushforwardSpectralSequenceData B S hS 𝒳.val.val.p
      𝒴.val.val.p (CatFiberedInGroupoids.homFunctor f.hom)
      (CatFiberedInGroupoids.homFunctor g.hom) SiteKind.fppf
      (fppfAbelianSheaf B S hS (fppfQuasicoherentSiteModule B S hS 𝓕))) (i j : ℕ) :
    letI := data.continuous i
    letI := data.cocontinuous i
    letI := data.gCocontinuous
    letI := data.enoughInjectives i
    letI : (Stacks.RelativeCech.Tuple.projection 𝒳.val.val.p
        (CatFiberedInGroupoids.homFunctor f.hom) i ⋙
        CatFiberedInGroupoids.homFunctor g.hom).IsCocontinuous
        (BigFppfOver.associatedTopology B S hS
          (Stacks.RelativeCech.Tuple.projection 𝒳.val.val.p
            (CatFiberedInGroupoids.homFunctor f.hom) i ⋙ 𝒳.val.val.p) SiteKind.fppf)
        (BigFppfOver.associatedTopology B S hS 𝒴.val.val.p SiteKind.fppf) :=
      isCocontinuous_comp (Stacks.RelativeCech.Tuple.projection 𝒳.val.val.p
          (CatFiberedInGroupoids.homFunctor f.hom) i)
        (CatFiberedInGroupoids.homFunctor g.hom)
        (BigFppfOver.associatedTopology B S hS
          (Stacks.RelativeCech.Tuple.projection 𝒳.val.val.p
            (CatFiberedInGroupoids.homFunctor f.hom) i ⋙ 𝒳.val.val.p) SiteKind.fppf)
        (BigFppfOver.associatedTopology B S hS 𝒳.val.val.p SiteKind.fppf)
    letI := Stacks.RelativeCech.additive_pushforwardCocontinuous AddCommGrpCat.{max (u + 1) a}
      (BigFppfOver.associatedTopology B S hS
        (Stacks.RelativeCech.Tuple.projection 𝒳.val.val.p
          (CatFiberedInGroupoids.homFunctor f.hom) i ⋙ 𝒳.val.val.p) SiteKind.fppf)
      (BigFppfOver.associatedTopology B S hS 𝒴.val.val.p SiteKind.fppf)
      (Stacks.RelativeCech.Tuple.projection 𝒳.val.val.p
        (CatFiberedInGroupoids.homFunctor f.hom) i ⋙
        CatFiberedInGroupoids.homFunctor g.hom)
    (data.sequence.page 1).X ((i : ℤ), (j : ℤ)) ≅
      (((Stacks.RelativeCech.Tuple.projection 𝒳.val.val.p
            (CatFiberedInGroupoids.homFunctor f.hom) i ⋙
          CatFiberedInGroupoids.homFunctor g.hom).sheafPushforwardCocontinuous
            AddCommGrpCat.{max (u + 1) a}
            (BigFppfOver.associatedTopology B S hS
              (Stacks.RelativeCech.Tuple.projection 𝒳.val.val.p
                (CatFiberedInGroupoids.homFunctor f.hom) i ⋙ 𝒳.val.val.p) SiteKind.fppf)
            (BigFppfOver.associatedTopology B S hS 𝒴.val.val.p SiteKind.fppf)).rightDerived
          j).obj
        ((SheafOfModules.toSheaf _).obj
          ((SheafOfModules.restrictAlongContinuous
            (Stacks.RelativeCech.Tuple.projection 𝒳.val.val.p
              (CatFiberedInGroupoids.homFunctor f.hom) i)
            (FibredSite.ringStructureSheafCore B S hS 𝒳.val.val.p
              𝒳.val.isFiberedInGroupoids SiteKind.fppf)).obj
            (fppfQuasicoherentSiteModule B S hS 𝓕)))
Sources

Section103.12 Further remarks on quasi-coherent modules#

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

Tag 0GQS, the section

Tag 0GQS in the Stacks Project.

AlgebraicGeometry.Space.preservesFiniteLimits_etaleRestrictedModuleInverseImageFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RestrictionToAlgebraicSpaceExactness.lean, line 166. The attribute's comment: “part (1), the left exact half: a preserves finite limits”.

Stacks 0GQS, part (1), the left exact half. The functor a : ℱ ↦ f^*ℱ|_{U_étale} preserves finite limits.

Limits of sheaves of modules are computed in presheaves, where restriction along a functor is pointwise, so this holds for the direct image along any continuous functor of ringed sites.

theorem preservesFiniteLimits_etaleRestrictedModuleInverseImageFunctor
    (hp : p.IsFiberedInGroupoids) (hr : r.IsFiberedInGroupoids)
    (eU : StacksRepresentableCFG.EquivalenceOver p
      (presheafOfCategories (U.1 ⋙ typeToCat)).p)
    (f : 𝒰 ⥤ 𝒳) (hf : p.IsFibredOneMorphism r f) :
    PreservesFiniteLimits (etaleRestrictedModuleInverseImageFunctor B S hS p r hp hr eU f hf)

AlgebraicGeometry.Space.exactFunctor_etaleRestrictedModuleInverseImageFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RestrictionToAlgebraicSpaceExactness.lean, line 185. The attribute's comment: “part (1): the functor a from all modules on the étale site of the stack to all modules on the small étale site of the algebraic space is exact”.

Stacks 0GQS, part (1). The functor a : Mod(𝒳_étale, 𝒪_𝒳) ⥤ Mod(U_étale, 𝒪_U), ℱ ↦ f^*ℱ|_{U_étale}, is exact.

The source's two reasons are the continuity and the cocontinuity of the functor U_étale ⥤ 𝒳 along which the restriction is taken: f^{-1} is restriction along the 1-morphism f and ·|_{U_étale} is restriction along u_U, and both functors are continuous and cocontinuous, so Stacks 04BD (2) applies to their composite.

theorem exactFunctor_etaleRestrictedModuleInverseImageFunctor [EssentiallySmall.{u} 𝒳]
    (hp : p.IsFiberedInGroupoids) (hr : r.IsFiberedInGroupoids)
    (eU : StacksRepresentableCFG.EquivalenceOver p
      (presheafOfCategories (U.1 ⋙ typeToCat)).p)
    (f : 𝒰 ⥤ 𝒳) (hf : p.IsFibredOneMorphism r f) :
    exactFunctor (inheritedEtaleModules B S hS r hr)
      (SheafOfModules.{u} (structureRingSheaf B S hS U))
      (etaleRestrictedModuleInverseImageFunctor B S hS p r hp hr eU f hf)
Tag 0GQT, an item

Tag 0GQT in the Stacks Project.

AlgebraicGeometry.Stack.FlatFppf.spaceChartRestrictionCoheratorInternalHomIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/CoheratorInternalHomRestriction.lean, line 105.

Stacks 0GQT. Let f : 𝒰 ⟶ 𝒳 be a flat 1-morphism of algebraic stacks with 𝒰 the algebraic stack of an algebraic space U, and let d : ℱ ↦ f^*ℱ|_{U_étale} be the restriction of Stacks 0GQS. For 𝒪_𝒳-modules ℱ and 𝒢 with ℱ quasi-coherent, d(hom(ℱ, 𝒢)) = 𝓗om_{𝒪_U}(d(ℱ), d(𝒢)), where hom(ℱ, 𝒢) = Q(𝓗om_{𝒪_𝒳}(ℱ, 𝒢)) is the object of Stacks 0GQN.

def spaceChartRestrictionCoheratorInternalHomIso (hf : AlgebraicStacks.IsFlat B S hS f)
    (F G : _root_.SheafOfModules.{u} (ambientRingStructureSheaf B S hS 𝒳))
    (hF : F.IsQuasicoherentOnSite) :
    spaceChartRestriction B S hS 𝒳 U hU f (coheratorInternalHom B S hS 𝒳 F G) ≅
      Space.smallEtaleInternalHomSmall B S hS U hU (spaceChartRestriction B S hS 𝒳 U hU f F)
        (spaceChartRestriction B S hS 𝒳 U hU f G)
Sources

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.