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, thenf^* : QCoh(𝒪_𝒴) ⥤ QCoh(𝒪_𝒳)is an exact functor: it preserves finite colimits, as it does for everyf, and finite limits, because kernels of quasi-coherent modules are computed on flat objects (AlgebraicGeometry.Stack.AlgebraicStacks.quasicoherentKernelsOnFlatObjects) andfcarries 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 andx_i : U_i → 𝒳,i ∈ I, flat objects with∐ x_i : ∐ U_i → 𝒳surjective. An arrowφofQCoh(𝒪_𝒳)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 andx_i : U_i → 𝒳,i ∈ I, flat objects with∐ x_i : ∐ U_i → 𝒳surjective. An arrowφofQCoh(𝒪_𝒳)is surjective (an epimorphism ofQCoh(𝒪_𝒳)) 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 andx_i : U_i → 𝒳,i ∈ I, flat objects with∐ x_i : ∐ U_i → 𝒳surjective. An arrowφofQCoh(𝒪_𝒳)is injective (a monomorphism of the abelian categoryQCoh(𝒪_𝒳)) 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
Mbe a rule assigning to a category fibred in groupoids overSa predicate on the modules on its étale site. IfMcuts 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 inType (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 inType (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
Mbe a rule on the modules on the étale sites of the algebraic stacks overSsuch 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 inType (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 carryMintoM, 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
Mbe a rule which associates to every algebraic stack𝒳overSa subcategoryM_𝒳ofMod(𝒪_𝒳), the modules on the fppf site of𝒳, such that
M_𝒳is a weak Serre subcategory ofMod(𝒪_𝒳)for every algebraic stack𝒳;- for a smooth 1-morphism
f : 𝒳 ⟶ 𝒴the inverse imagef^*mapsM_𝒴intoM_𝒳;Mis smooth-local on the target; and- for a 1-morphism of stacks representable by affine schemes,
Rⁱf_*mapsMintoM.Then for every quasi-compact and quasi-separated 1-morphism
f : 𝒳 ⟶ 𝒴of algebraic stacks and everyFinM_𝒳, the higher direct imageRⁱf_* F, computed in the fppf topology, lies inM_𝒴.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,
hpresandhcech: 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
Mbe a rule which associates to every algebraic stack𝒳overSa propertyM_𝒳of the sheaves of𝒪_𝒳-modules on the fppf site of𝒳such that
M_𝒳is a weak Serre subcategory ofMod(𝒪_𝒳)for all algebraic stacks𝒳;- for a smooth 1-morphism
f : 𝒵 ⟶ 𝒳the inverse imagef^*mapsM_𝒳intoM_𝒵;- if
fᵢ : 𝒳ᵢ ⟶ 𝒳is a family of smooth 1-morphisms with|𝒳| = ⋃ᵢ |fᵢ|(|𝒳ᵢ|), then a moduleℱlies inM_𝒳if and only if everyfᵢ^*ℱlies inM_{𝒳ᵢ}; and- if
f : 𝒳 ⟶ 𝒴is a 1-morphism of algebraic stacks and𝒳and𝒴are representable by affine schemes, thenRⁱf_*mapsM_𝒳intoM_𝒴.Then for every quasi-compact and quasi-separated 1-morphism
f : 𝒳 ⟶ 𝒴of algebraic stacks,Rⁱf_*mapsM_𝒳intoM_𝒴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 overSwith|𝒳| = ⋃ j, |f j|(|𝒵 j|), and letFbe a sheaf of𝒪_𝒳-modules on𝒳_étale. If every inverse imagef j^{-1} Fis locally quasi-coherent, then so isF.
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 overSand letℱbe a locally quasi-coherent𝒪_𝒳-module on𝒳_étale(Stacks 06WJ). Then the higher direct imageRⁱf_*ℱ, computed in the étale topology, is locally quasi-coherent on𝒴_étale, in every degreei.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:
hcritis Stacks 076Z, quantified over every rule. Its proof runs the first-quadrant spectral sequence of Stacks 072G, which is not formalized here.hserreis hypothesis (1), the weak Serre condition, which is parts (1) to (3) of Stacks 06WM, proved at section universeuinStacksFrontier.AlgebraicGeometry.Stacks.Quasicoherent.LocallyQuasicoherentClosure; here it is read at section universeu + 1.hconvis the converse half of hypothesis (3), which is Stacks 075Y. That tag is proved, at section universeuonly, and the higher direct images produce modules with sections inu + 1; closing this gap is a universe generalization of Stacks 03DN, not a new theorem of the source.haffineis 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 imageRⁱf_*ℱ, computed in the étale topology, is locally quasi-coherent on𝒴_étale.Modules have sections in the universe
uof the schemes, andRⁱ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 siteEwith the cutoff ofB.
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 overSwith|𝒳| = ⋃ j, |f j|(|𝒵 j|), letFbe a sheaf of𝒪_𝒳-modules on𝒳_étaleand suppose every inverse imagef j^{-1} Fis locally quasi-coherent. Then every objectxof𝒳admits a family of arrowsφ i : y i ⟶ xlying over flat, locally finitely presented and jointly surjective morphisms of schemes, at every member of which the restriction ofFto 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 overSwith|𝒳| = ⋃ j, |f j|(|𝒵 j|)(Stacks 04XG), and letFbe a sheaf of𝒪_𝒳-modules on𝒳_fppf. If every inverse imagef j^{-1} Fis locally quasi-coherent (Stacks 06WJ), then so isF.The étale sheaf condition follows from the fppf one. At an object
xlying overU, the restrictionx^*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 forFalong arrows lying over étale morphisms of affine schemes, proved byAlgebraicGeometry.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:
restrictModulePullbackComparisonregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatBaseChangeProperty.lean, line 60 (StacksFrontier): “the comparison mapc_φ”.
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 mapc_φis the component of a natural transformation fromF ↦ a_{small}^*(F|_{V_ét})toF ↦ F|_{U_ét}. Both functors preserve colimits — the first becausea_{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_colimittransported 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, byAlgebraicGeometry.Stack.hasFlatBaseChangeProperty_of_isColimit.This is Stacks 0764, part (4), for presheaves of modules: through Mathlib's instances
CategoryTheory.Limits.hasColimitsOfShape_of_closedUnderColimitsandCategoryTheory.preservesColimitOfShape_of_createsColimitsOfShape_and_hasColimitsOfShape, the subcategory has colimits of shapeJand 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, byAlgebraicGeometry.Stack.hasFlatBaseChangeProperty_of_isColimit.This is Stacks 0764, part (4), for presheaves of modules: through Mathlib's instances
CategoryTheory.Limits.hasColimitsOfShape_of_closedUnderColimitsandCategoryTheory.preservesColimitOfShape_of_createsColimitsOfShape_and_hasColimitsOfShape, the subcategory has colimits of shapeJand 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_isColimitin 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 ofMod(𝒳_étale, 𝒪_𝒳).For an arrow
φof𝒳lying over a flat morphism of schemes,c_φ^{sh}is the component of a natural transformation fromF ↦ a_{small}^*(F|_{V_ét})toF ↦ F|_{U_ét}. Both functors preserve colimits — the first because the inverse image of sheaves of modules is a left adjoint, byAlgebraicGeometry.Stack.sheafifiedPullbackComparisonAdjunction, the second byAlgebraicGeometry.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_colimittransported 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 thatMod(𝒳_é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 ofMod(𝒳_é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 letF,Gbe étale sheaves of𝒪_𝒳-modules, withFof finite presentation on𝒳_étale(Stacks 03DL) andGwith the flat base change property of Stacks 0762. Then the internal Hom𝓗om_{𝒪_𝒳}(F, G)ofMod(𝒳_étale, 𝒪_𝒳)has the flat base change property.Let
φ : x ⟶ ylie over a flat morphism, and let{e_j : y_j ⟶ y}be an étale covering on whose membersFhas a finite presentation. At every arrow into somey_jlying over a flat morphism the comparison map of𝓗om(F, G)is invertible by the presented case proved above, and that suffices forc_φby the étale-local criterionAlgebraicGeometry.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 ofS, and letFbe 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 imagef^*Fof sheaves of modules has the flat base change property.An arrow
φof𝒳lies over the same morphism of schemes asf φ, so this isAlgebraicGeometry.Stack.isIso_restrictSheafPullbackComparison_modulePullback_iffat 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 overSwith|𝒳| = ⋃ j, |f j|(|𝒵 j|), and letFbe an étale sheaf of𝒪_𝒳-modules. If every inverse imagef j^* Fof sheaves of modules has the flat base change property of Stacks 0762, then so doesF.
AlgebraicGeometry.Stack.exists_etaleCovering_family_fibre_liftcovers the scheme below any object of𝒳by étale morphisms over which the object lifts through somef j, andAlgebraicGeometry.Stack.hasFlatBaseChangePropertySheaf_of_etaleLocalconcludes.
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.sheafTensorat the structure sheaf of the associated étale site; it isAlgebraicGeometry.Stack.etaleTensorSheafbyAlgebraicGeometry.Stack.etaleTensorSheaf_eq. The sheafification instances it is formed with hold for every𝒳, byAlgebraicGeometry.Stack.hasSheafify_etaleAssociatedTopologyandAlgebraicGeometry.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 ofMod(𝒳_é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 isAlgebraicGeometry.Stack.hasFlatBaseChangePropertySheaf_initial, the cokernels areAlgebraicGeometry.Stack.hasFlatBaseChangePropertySheaf_cokernel, the extensions areAlgebraicGeometry.Stack.hasFlatBaseChangePropertySheaf_of_shortExact, and the kernels areAlgebraicGeometry.Stack.hasFlatBaseChangePropertySheaf_kernel, the last with the left exactnessAlgebraicGeometry.Stack.preservesFiniteLimits_sheafifiedPullbackComparison: this isAlgebraicGeometry.Stack.isWeakSerreClass_flatBaseChangeEtaleModules_of_preservesFiniteLimitsat section universeu.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 byAlgebraicGeometry.Stack.hasSheafify_etaleAssociatedTopologyandAlgebraicGeometry.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 imageRⁱ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 inType (u + 1), where the higher direct images of Stacks 06WE live, and the source𝒳is presented strictly, its structure functor written as the functor offfollowed 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 overSand letℱbe a sheaf of𝒪_𝒳-modules on𝒳_étalewhich is locally quasi-coherent (Stacks 06WJ) and has the flat base change property (Stacks 0762). Then every higher direct imageRⁱ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 ofRⁱ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 atLQCoh^fbcor at the flat base change property alone, and each a result of the source this library does not have:
hcritis Stacks 076Z, quantified over every rule.hserreis hypothesis (1) forLQCoh^fbc, which is parts (1) to (3) of Stacks 06WM together with part (2) of Stacks 0764.hfbcPullis 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.hconvLqcandhconvFbcare the two halves of the converse of hypothesis (3), namely Stacks 075Y at section universeu + 1and part (3) of Stacks 0764.haffineis hypothesis (4) forLQCoh^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 letFbe a module on the fppf site of𝒴lying inLQCoh^fbc(𝒪_𝒴). Then the inverse imagef^*Flies inLQCoh^fbc(𝒪_𝒳).
AlgebraicGeometry.Stack.isLocallyQuasicoherentWithFlatBaseChange_stackInverseImageis this statement for the inverse image of presheaves of modules, stated at the structure functorf ⋙ 𝒪_𝒴of the composite presentation; the structure functor of the source is a parameterphere, together with the identificatione, so that substitutingeputs 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 overSand letFlie inLQCoh^fbc(𝒪_𝒳). Then the inverse imageg^{-1}Flies inLQCoh^fbc(𝒪_𝒵).Local quasi-coherence of
g^{-1}Fis Stacks 06WL, which holds for every 1-morphism of categories fibred in groupoids. The flat base change property ofg^{-1}Fis the hypothesishfbc: 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 ofLQCoh^fbc(𝒪_𝒳) ⊆ Mod(𝒳_ét, 𝒪_𝒳)on an algebraic stack is a module on the fppf site, with the same underlying presheaf of modules, and it lies inLQCoh^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^fbcasks the comparison mapc_φ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 afterAlgebraicGeometry.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 ofLQCoh^fbc(𝒪_𝒳), being a sheaf for the fppf topology byAlgebraicGeometry.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).objwhichever 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 overSand letℱbe a sheaf of𝒪_𝒳-modules on𝒳_étalewhich is locally quasi-coherent (Stacks 06WJ) and has the flat base change property (Stacks 0762). Then the higher direct imageRⁱf_*ℱof Stacks 06WE, computed in the étale topology, is again locally quasi-coherent and has the flat base change property, in every degreei: that is,Rⁱf_*carriesLQCoh^fbc(𝒪_𝒳)intoLQCoh^fbc(𝒪_𝒴).The flat base change property is read at section universe
u + 1, where the higher direct images of module sheaves live, byAlgebraicGeometry.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 hypothesesAlgebraicGeometry.Stack.hasFlatBaseChangePropertyUnivLE_moduleSheafHigherDirectImage(Stacks 0765) carries, each a result of the source this library does not have:hcritis Stacks 076Z quantified over every rule,hserreis parts (1) to (3) of Stacks 06WM with part (2) of Stacks 0764,hfbcPullis part (1) of Stacks 0764,hconvLqcandhconvFbcare Stacks 075Y at section universeu + 1and part (3) of Stacks 0764, andhaffineis 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(𝒪_𝒴). Letf : 𝒳 ⟶ 𝒴be a quasi-compact and quasi-separated 1-morphism of algebraic stacks andFan object ofLQCoh^fbc(𝒪_𝒳). Then each higher direct imageRⁱf_*F, computed in the fppf topology, is an object ofLQCoh^fbc(𝒪_𝒴).Modules have sections in the universe
uof the schemes; local quasi-coherence is read against an auxiliary big étale siteEwithE.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 andFan object ofLQCoh^fbc(𝒪_𝒳). ThenRⁱf_*Fis 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
uof the schemes. The assertion of the source about the total direct imageRf_*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 andFan object ofLQCoh^fbc(𝒪_𝒳), a module on𝒳_étalewhich is locally quasi-coherent with the flat base change property. Then each higher direct imageRⁱf_*F, computed in the étale topology, is an object ofLQCoh^fbc(𝒪_𝒴).Modules have sections in the universe
uof the schemes, local quasi-coherence is read against an auxiliary big étale siteEwithE.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 carriesLQCoh^fbc(𝒪_𝒴)intoLQCoh^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 carriesLQCoh^fbc(𝒪_𝒴)intoLQCoh^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 andFan object ofLQCoh^fbc(𝒪_𝒳) ⊆ Mod(𝒪_𝒳). The total direct image ofFcomputed in the étale topology is the one computed in the fppf topology, read on the étale site:Rf_{ét,*}(ε_*F) ≅ Rε_*(Rf_{fppf,*}F)inD⁺(Mod(𝒴_ét, 𝒪_𝒴)).Here
ε_* : Mod(𝒪_𝒴) ⥤ Mod(𝒴_ét, 𝒪_𝒴)is only left exact, so the fppf result is compared through its right derived functorRε_*. The isomorphism isAlgebraicGeometry.Stack.totalDirectImageEtaleComparisonIsotogether withRε_*F ≅ ε_*F, which is Stacks 075R (1),AlgebraicGeometry.Stack.isZero_rightDerived_etaleComparisonPushforward_of_lqcohSheafFbc. No quasi-compactness or quasi-separatedness offis needed for this form. Whenfis quasi-compact and quasi-separated, part (4)(b) and Stacks 075R (1) make the cohomology sheavesRⁱf_{fppf,*}FofRf_{fppf,*}Fthemselvesε_*-acyclic, so thatRε_*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, andAlgebraicGeometry.Stack.nonempty_homology_etaleComparison_totalDirectImage_isobelow.
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 inMod(𝒳_étale, 𝒪_𝒳)as well as inMod(𝒪_𝒳).In order:
LQCoh^fbc(𝒪_𝒳), read insideMod(𝒪_𝒳), has small colimits and its inclusion preserves them; read insideMod(𝒳_étale, 𝒪_𝒳)the same holds; and restricting a colimit cocone inMod(𝒪_𝒳)of objects ofLQCoh^fbc(𝒪_𝒳)to the étale site gives a colimit cocone inMod(𝒳_é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
Fan𝒪_𝒳-module of finite presentation andGinLQCoh^fbc(𝒪_𝒳)on an algebraic stack, the internal HomSheafHom_{𝒪_𝒳}(F, G)ofMod(𝒪_𝒳)is inLQCoh^fbc(𝒪_𝒳).
Gis cartesian along the flat arrows between objects over affine schemes (step R2 of Stacks 0779), hence so isSheafHom_{𝒪_𝒳}(F, G),Fbeing 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
FandGinLQCoh^fbc(𝒪_𝒳)on an algebraic stack, the tensor productF ⊗_{𝒪_𝒳} Gcomputed inMod(𝒪_𝒳)is again inLQCoh^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 ofMod(𝒳_ét, 𝒪_𝒳), for an algebraic stack𝒳, at module universeu, 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 ofMod(𝒪_𝒳), for an algebraic stack𝒳, at module universeu, with the abelian structure coming from the sheafification of abelian presheaves on the fppf site (AlgebraicGeometry.Stack.FlatFppf.hasSheafify_fppf_addCommGrpCat): it contains0and 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 overSwith|𝒳| = ⋃ j, |f j|(|𝒵 j|), and letFbe a sheaf of𝒪_𝒳-modules on𝒳_étale. If every inverse imagef j^{-1} Flies inLQCoh^fbc(𝒪_{𝒵 j})andFhas the flat base change property, thenFlies inLQCoh^fbc(𝒪_𝒳).Local quasi-coherence of
Fis Stacks 075Y, applied to the local quasi-coherence of the inverse images. The flat base change property ofFis the hypothesishfbc: 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|), andFa sheaf of𝒪_𝒳-modules on𝒳_ét. If everyf j^{-1} Fis inLQCoh^fbc(𝒪_{𝒵 j}), thenFis inLQCoh^fbc(𝒪_𝒳).The source's hypothesis reads
LQCoh^{fpc}, a misprint forLQCoh^{fbc}.LQCoh^fbcis 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|), andFa sheaf of𝒪_𝒳-modules on𝒳_fppf. If everyf j^{-1} Fis inLQCoh^fbc(𝒪_{𝒵 j}), thenFis inLQCoh^fbc(𝒪_𝒳).
LQCoh^fbcis 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 inAlgebraicGeometry.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 inLQCoh^{fbc}(𝒪_𝒳)(hF), and lety : V ⟶ 𝒴be an object of𝒴over a schemeV. Then:
- the 2-fibre product
U = V ×_𝒴 𝒳is represented by an algebraic space;- for every such presentation
eUofUby an algebraic space, withf' : U ⟶ Vthe base change off(AlgebraicGeometry.Stack.baseChangeSpacesHom), and for everyi,(Rⁱf_*ℱ)|_{V_étale} ≅ Rⁱf'_{small,*}(ℱ|_{U_étale}).Here
Rⁱf_*is the higher direct image ofMod(𝒪_𝒳), in the fppf topology.(-)|_{V_étale}reads an fppf module on the étale site (stackModulesEtaleComparison), pulls it back alongyand restricts it to the small étale site ofV(π_{V,*}, Stacks 073M).(-)|_{U_étale}does the same along the projectionU ⟶ 𝒳.f'_{small,*}is the direct image of the small étale sites of the algebraic spacesUandV.
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 spaceF = U, becausefis representable by algebraic spaces — andf' : 𝒰 ⥤ 𝒱the base change off, inducing a morphismU ⟶ Von 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_* ℱisH^iof the total right derived direct imageRfStack, 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,*}, andR^i f'_{small,*}isH^iof the total right derived direct imageRfSpaceof the small étale sites of the algebraic spacesUandV.The chain is the source's:
hDgandbcare its reduction to the representable case, andAlgebraicGeometry.Space.restrictedDerivedDirectImageIsotogether withAlgebraicGeometry.RingedToposHom.derivedPushforwardOfExactCompHomologyFunctorIsoare its appeal to Stacks 075N. See the implementation notes of this file for what each hypothesis is and where the source's hypotheses onfand 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 overS. The direct image restricts to a functorf_* : LQCoh^fbc(𝒪_𝒳) ⥤ LQCoh^fbc(𝒪_𝒴)(AlgebraicGeometry.Stack.affineLqcohSheafFbcPushforward, which isAlgebraicGeometry.Stack.fppfModulesPushforwardon objects and morphisms byAlgebraicGeometry.Stack.affineLqcohSheafFbcPushforwardCompιIso), and
f_*is exact: a sequence ofLQCoh^fbc(𝒪_𝒳)which is short exact inMod(𝒪_𝒳)goes to a sequence short exact inMod(𝒪_𝒴);f_*commutes with direct sums (indexed by anyι : Type u);Rⁱf_* F = 0for everyi > 0andFinLQCoh^fbc(𝒪_𝒳).Modules are on the fppf sites at the module universe
uof the schemes;LQCoh^fbcisAlgebraicGeometry.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 overSand suppose the higher direct imagesRⁱf_*vanish in positive degrees onLQCoh^fbc(𝒪_𝒳). Thenf_*carries a short exact sequence of𝒪_𝒳-modules on𝒳_étalewhose outer terms lie inLQCoh^fbc(𝒪_𝒳)to a short exact sequence of𝒪_𝒴-modules on𝒴_étale; that is,f_*is exact onLQCoh^fbc(𝒪_𝒳).The vanishing in positive degrees is right acyclicity for
f_*, by Stacks 015C and left exactness of the right adjointf_*, and Stacks 015D part (1) turns right acyclicity of the outer terms into short exactness of the image. Affineness is what dischargeshvanand 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 overS, 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
yof𝒴the covering ofAlgebraicGeometry.Stack.exists_fppfCovering_family_flatObject_liftsupplies an fppf covering family ofyby objectsf (a i)(x_i)withx_ia flat object of𝒳 (a i); the sections ofℱthere are the sections of(f (a i))^*ℱatx_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
Fis a parasitic presheaf of𝒪_𝒳-modules andg : 𝒴 ⟶ 𝒳is a flat 1-morphism of algebraic stacks, then the inverse imageg^*Fis a parasitic presheaf of𝒪_𝒴-modules.Let
ybe an object of𝒴lying over a schemeVfor whichy : V → 𝒴is flat. Theng y : V → 𝒴 → 𝒳is flat, being a composite of flat 1-morphisms (Stacks 06PX), soFvanishes atg yby hypothesis. The sections ofg^*Fatyare the sections ofFatg 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₃ → 0of modules on one of the sites associated with an algebraic stack, withF₁andF₃parasitic, the moduleF₂is parasitic.This is the source's "evaluate on
xlying over a scheme flat over𝒳": at a flat object the sections ofF₁and ofF₃vanish, and taking sections is left exact, so the sections ofF₂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 ⟶ Gis an epimorphism of modules on one of the sites associated with an algebraic stack andFis parasitic, thenGis parasitic.An epimorphism of sheaves of modules is locally surjective, so this is
AlgebraicGeometry.Stack.isParasitic_of_isLocallySurjective: at a flat object every section ofGcomes from a section ofFon a covering, and that covering may be refined by one whose sources are again flat objects, whereFvanishes.
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 overS, 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
yof𝒴, every point of the schemeylies over is hit by a smooth morphismmof the site carrying a lift ofyto some𝒳 jwhich 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. Refiningmby an étale morphism factoring through it (Stacks 055U) and taking a cartesian lift of the comparison morphism gives an étale covering family ofyalong 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
uof the schemes. Let𝒳be an algebraic stack andℱa parasitic sheaf of𝒪_𝒳-modules (Stacks 0773). ThenH^i(𝒳, ℱ) = 0for everyi, whereH^i(𝒳, -)isAlgebraicGeometry.Stack.FlatFppf.fppfModuleCohomology,Ext^iout of the structure sheaf, in any universetofExt-groups.The instance argument
HasExt.{t}is not a hypothesis onℱ:fppfModuleCohomology.{u, w, t}is only defined in its presence. Att = uit is supplied by the Grothendieck abelian structure (AlgebraicGeometry.Stack.isGrothendieckAbelian_fppfModules), which isAlgebraicGeometry.Stack.isZero_fppfModuleCohomology_of_isParasitic_ofGrothendieck.By
AlgebraicGeometry.Stack.fppfModuleCohomologyULiftIsothis is the vanishing ofExt^iout of the lifted structure sheaf of the universe lift ofℱ, which is parasitic asℱis, and that isAlgebraicGeometry.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 universeuof the schemes. Let𝒳be an algebraic stack andℱa parasitic sheaf of𝒪_𝒳-modules on𝒳_τ(Stacks 0773). ThenH^i_τ(𝒳, ℱ) = Ext^i(𝒪_𝒳, ℱ) = 0for everyi, forExt-groups in any universet.The instance argument
HasExt.{t}is not a hypothesis onℱ: it is what makesExt-groups in the universetexist at all, and it is always available att = u, the category of modules being Grothendieck abelian (AlgebraicGeometry.Stack.isGrothendieckAbelian_moduleRingSheaf, seeAlgebraicGeometry.Stack.isZero_ext_unit_of_isParasitic_atSchemeUniverse_ofGrothendieck).By
AlgebraicGeometry.Stack.isZero_ext_unit_iff_isZero_ext_uliftUnitthis is the vanishing ofExt^iout of the lifted structure sheaf of the universe lift ofℱ, which is parasitic asℱis, and that isAlgebraicGeometry.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). ThenH^i_τ(𝒳, ℱ) = 0for alli.The modules have their sections in the universe
u + 1of the objects of the site, where the structure sheaf𝒪_𝒳is a module through its universe liftStacks.SheafOfModules.uliftUnitandH^i_τ(𝒳, -) = Ext^i(𝒪_𝒳, -), in any universetofExt-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 + 1of the objects of the site. Letf : 𝒳 ⟶ 𝒴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 imageR^nf_*ℱ(Stacks 06WE,AlgebraicGeometry.Stack.moduleSheafHigherDirectImage) is a parasitic sheaf of𝒪_𝒴-modules.This is
AlgebraicGeometry.Stack.isParasitic_rightDerived_stackModuleDirectImageSuccmoved alongAlgebraicGeometry.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 universeuof the schemes. Letf : 𝒳 ⟶ 𝒴be a 1-morphism of algebraic stacks andℱa parasitic sheaf of𝒪_𝒳-modules on𝒳_τ(Stacks 0773). Then every higher direct imageR^nf_*ℱ(AlgebraicGeometry.Stack.stackModuleHigherDirectImage) is parasitic.The universe lift carries
R^nf_*ℱtoR^nf_*atu + 1of the lift ofℱ(AlgebraicGeometry.Stack.stackModuleHigherDirectImageULiftIso), the lift of a parasitic module is parasitic, and atu + 1this isAlgebraicGeometry.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-morphismf : 𝒳 ⟶ 𝒴of algebraic stacks, the higher direct imagesAlgebraicGeometry.Stack.fppfModulesHigherDirectImageof a parasitic module are parasitic. This isAlgebraicGeometry.Stack.isParasitic_stackModuleHigherDirectImageatτ = 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 inQCoh(𝒪_𝒳)withβ ∘ α = 0. The following are equivalent:
- in the abelian category
QCoh(𝒪_𝒳)the complex𝓕 ⟶ 𝓖 ⟶ 𝓗is exact at𝓖;Ker(β)/Im(α)computed inMod(𝒳_étale, 𝒪_𝒳)is parasitic;Ker(β)/Im(α)computed inMod(𝒳_fppf, 𝒪_𝒳)is parasitic.The abelian structure of
QCoh(𝒪_𝒳)isAlgebraicGeometry.Stack.AlgebraicStacks.instAbelianQuasicoherentModules;Ker(β)/Im(α)computed inMod(𝒳_τ, 𝒪_𝒳)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 inclusioni : 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 ∘ iis the identity functor ofQCoh(𝒪_𝒳), for the coheratorQonLQCoh^fbc(𝒪_𝒳)and the inclusioni.
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:
Qis right adjoint to the inclusioni.
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 ∘ iis the identity functor ofQCoh(𝒪_𝒳).
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 inclusioni : QCoh(𝒪_𝒳) ⥤ LQCoh^fbc(𝒪_𝒳)has the right adjointQ, andQ ∘ iis the identity functor ofQCoh(𝒪_𝒳).
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 coheratorQ : Mod(𝒪_𝒳) → QCoh(𝒪_𝒳)of Stacks 0778 exactly when it is parasitic: the kernel ofQonLQCoh^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
𝓕inLQCoh^fbc(𝒪_𝒳)both the kernel and the cokernel of the adjunction mapQ(𝓕) ⟶ 𝓕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 inclusionQCoh(𝒪_𝒳) → 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 ofu-small shapes, which are computed inMod(𝒪_𝒳).
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:
Qis 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
𝓕ofLQCoh^fbc(𝒪_𝒳)is in the kernel of the coheratorQof 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 𝓕))withr 𝓕, andi ⋙ ris an equivalence and so reflects zero objects; soQ 𝓕 = 0if and only ifr 𝓕 = 0, which byhrparis the parasitic condition. Hererstands for the restriction𝓕 ↦ 𝓕|_{U_étale}along a smooth surjective chartf : U → 𝒳, through which the source computesQ; see the module documentation for the three hypotheses it carries and for Stacks 06WT, whichhreqnames.
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_étalecommutes with direct sums.Here that is the hypothesis
hrcolimonr, carried through the identificationQ ≅ r ⋙ (i ⋙ r)⁻¹which the counit andhreqsupply; 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 becauseQis a right adjoint; the second isAlgebraicGeometry.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
iis fully faithful, soQapplied to the counit is invertible, in particular a monomorphism;Qpreserves the kernel fork, being a right adjoint; so the kernel is in the kernel ofQand therefore parasitic by part (1). The kernel is taken as an arbitrary limit kernel fork, so that nothing is assumed aboutLQCoh^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.
Qapplied to the counit is invertible, in particular an epimorphism;Qis right exact by part (3) and so preserves the cokernel cofork; so the cokernel is in the kernel ofQand 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. ThenQ_𝒳 ∘ f^* = f^* ∘ Q_𝒴, withQ_𝒳andQ_𝒴the coherators of Stacks 0778: the canonical comparisonf^* Q_𝒴(𝓕) ⟶ Q_𝒳(f^*𝓕)is an isomorphism for every𝓕inLQCoh^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
xbe an object of an algebraic stack𝒳lying over a schemeUsuch thatx : U → 𝒳is flat, and let𝓕be inLQCoh^fbc(𝒪_𝒳). ThenQ(𝓕)|_{U_ét} = 𝓕|_{U_ét}: the restriction to the small étale site ofUof the adjunction mapQ(𝓕) ⟶ 𝓕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 inMod(𝒪_𝒳), with its map to𝓕, is the kernel ofφinQCoh(𝒪_𝒳).
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 inMod(𝒪_𝒳)lies inLQCoh^fbc(𝒪_𝒳),LQCoh^fbc(𝒪_𝒳)being a weak Serre subcategory containingQCoh(𝒪_𝒳)(Stacks 0771 (2)). Its coherator is the kernel ofφinQCoh(𝒪_𝒳)(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 inMod(𝒪_𝒳)lies inLQCoh^fbc(𝒪_𝒳): it is the kernel of𝓖 ⟶ Coker(φ). It need not be quasi-coherent: part (2) as printed is refuted byAlgebraicGeometry.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 inMod(𝒪_𝒳), is the image ofφinQCoh(𝒪_𝒳): the epimorphism𝓕 ⟶ Im φlies inLQCoh^fbc(𝒪_𝒳), whereQis right exact (Stacks 0779 (3)), andQkeepsIm φ ⟶ 𝓖a monomorphism. Part (2) as printed, withIm φitself quasi-coherent, is refuted byAlgebraicGeometry.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 inMod(𝒪_𝒳)is quasi-coherent: multiplication by2on𝒪overSpec ℤis a counterexample. The corrected part (2) isAlgebraicGeometry.Stack.AlgebraicStacks.lqcohSheafFbc_image_quasicoherentInclusion(the image lies inLQCoh^fbc(𝒪_𝒳)) together withAlgebraicGeometry.Stack.AlgebraicStacks.coheratorImageIsImage(its coherator is the image inQCoh(𝒪_𝒳)).
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φinQCoh(𝒪_𝒳), included intoMod(𝒪_𝒳)together with its projection, is a cokernel ofφinMod(𝒪_𝒳).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 asAlgebraicGeometry.FibredSite.isQuasicoherent_cokernel_quasicoherentInclusion— and it is the cokernel inQCoh(𝒪_𝒳). 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 inMod(𝒪_𝒳)is quasi-coherent, because it is isomorphic to the inclusion of the cokernel computed inQCoh(𝒪_𝒳).
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 letKer(i φ)be its kernel insideLQCoh^fbc(𝒪_𝒳). ThenQ(Ker(i φ)), with the mapAlgebraicGeometry.Stack.quasicoheratorKernelιto𝓕, is a kernel ofφinQCoh(𝒪_𝒳).The proof is formal:
Qis a right adjoint, so it preserves the kernel, andQ ∘ iis the identity because the inclusion is fully faithful; transporting the kernel ofQ(i φ)along that identification gives the kernel ofφ.That
Ker(φ)computed inMod(𝒪_𝒳)lies inLQCoh^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 inLQCoh^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φinQCoh(𝒪_𝒳), included intoMod(𝒪_𝒳)with its projection, is a cokernel ofφinMod(𝒪_𝒳): the cokernel computed inMod(𝒪_𝒳)is the cokernel inQCoh(𝒪_𝒳).
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 subcategoryLQCoh^fbc(𝒪_𝒳)ofMod(𝒪_𝒳), with the coherator, right exact there, as coreflector.
instance instAbelianQuasicoherentModules : Abelian (quasicoherentModules B S hS 𝒳)
Declarations registered for the tag:
preservesFiniteColimits_quasicoherentInclusionregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentKernelCokernel.lean, line 90 (StacksFrontier): “the inclusion QCoh(𝒪_𝒳) → Mod(𝒪_𝒳) is right exact, over the closure of quasi-coherence under colimits”.
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 ofMod(𝒪_𝒳).
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 onLQCoh^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 fromMod(𝒪_𝒳).
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 comparisonQ(𝓕) ⊗ Q(𝓖) → Q(𝓕 ⊗ 𝓖)is the adjoint transpose of the tensor productQ(𝓕) ⊗ Q(𝓖) → 𝓕 ⊗ 𝓖of the two counits, the south-west arrow of the triangle of the source, and it is invertible becauseQinverts 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
𝓕, 𝓖inLQCoh^fbc(𝒪_𝒳)the canonical mapQ(𝓕) ⊗ 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 functorAlgebraicGeometry.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_tensorSheafat 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 inclusionQCoh(𝒪_𝒳) → 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 ofF ⊗_𝒪 GbyStacks.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 exhibitsQCoh(𝒪_𝒳)as the quotient ofLQCoh^fbc(𝒪_𝒳)by the Serre subcategory of parasitic objects (Stacks 02MS).The inclusion
iis fully faithful andQis its right adjoint (Stacks 0778), soQis a localization functor for the class of morphisms it inverts; byAlgebraicGeometry.Stack.parasiticIsoModSerre_eq_inverseImage_isomorphismsthat 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 ofLQCoh^fbc(𝒪_𝒳)at the morphisms with parasitic kernel and cokernel, is equivalent toQCoh(𝒪_𝒳), 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 byAlgebraicGeometry.Stack.serreQuotientEquivalenceQuasicoherentModules, this is an adjunction betweeniand the canonical quotient functorLQCoh^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 coheratorQ : LQCoh^fbc(𝒪_𝒳) ⥤ QCoh(𝒪_𝒳)of Stacks 0778 is a localization functor for the morphisms whose kernel and cokernel are parasitic, i.e. it exhibitsQCoh(𝒪_𝒳)as the Serre quotient (Stacks 02MS) ofLQCoh^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) andQCoh(𝒪_𝒳), 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 throughlqcohFbcSerreQuotientEquivalence, is left adjoint to the quotient functorLQCoh^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 ofMod(𝒳_é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 HomSheafHom_{𝒪_𝒳}(F, G)computed inMod(𝒳_étale, 𝒪_𝒳)and the one computed inMod(𝒪_𝒳)have the same underlying presheaf of abelian groups, for arbitrary modulesFandGon the fppf site; the source states it forFof finite presentation andGquasi-coherent.Both are the internal Hom of Stacks 03EM read in the universe
uof the module sections, and that construction depends only on the underlying presheaves ofF,Gand 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): forHquasi-coherent,Hom_𝒳(H, hom(F, G)) = Hom_𝒳(H ⊗_{𝒪_𝒳} F, G). This isAlgebraicGeometry.Stack.AlgebraicStacks.quasicoherentHomOfEquivat the coherator; it holds for arbitraryFandG.
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
Fan𝒪_𝒳-module of finite presentation andGa quasi-coherent𝒪_𝒳-module on an algebraic stack, the internal HomSheafHom_{𝒪_𝒳}(F, G), whose two computations agree byAlgebraicGeometry.Stack.AlgebraicStacks.fppfInternalHom_presheaf_eq_etaleInternalHom, is an object ofLQCoh^fbc(𝒪_𝒳). It is Stacks 0771 (7) applied toG ∈ 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,Fan𝒪_𝒴-module of finite presentation andGa quasi-coherent𝒪_𝒴-module. Thenf^* hom(F, G) = hom(f^* F, f^* G), withhomthe quasi-coherent internal Homhom(F, G) = Q(SheafHom_{𝒪_𝒴}(F, G))of Stacks 0GQN.The isomorphism is the composite of
f^* Q_𝒴 = Q_𝒳 f^*(Stacks 0GQJ, atSheafHom_{𝒪_𝒴}(F, G), which lies inLQCoh^fbc(𝒪_𝒴)by Stacks 0GQN) withQ_𝒳off^* 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 adjointf_{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 compositeQCoh(𝒪_𝒳) → LQCoh^fbc(𝒪_𝒳) → LQCoh^fbc(𝒪_𝒴) → QCoh(𝒪_𝒴)of the inclusion, the direct image of Stacks 0771 and the coheratorQof Stacks 0778, the restriction of the coherator toLQCoh^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 compositeQCoh(𝒪_𝒳) → LQCoh^fbc(𝒪_𝒳) → LQCoh^fbc(𝒪_𝒴) → QCoh(𝒪_𝒴)of the inclusion, the higher direct imageRⁱf_*of Stacks 0771 and the coheratorQof 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-morphismfof algebraic stacks. Its degree-ifunctor isAlgebraicGeometry.Stack.AlgebraicStacks.quasicoherentHigherDirectImage(byrfl), the compositeQ ∘ 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 definingf_{QCoh,*}with thei-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 adjointf_{QCoh,*}.The adjunction
f^* ⊣ f_*of Stacks 06WE composed with the coherator adjunction of Stacks 0781 part (2) is an adjunction betweenQCoh(𝒪_𝒴)and all ofMod(𝒪_𝒳); restricting it along the fully faithful inclusion ofQCoh(𝒪_𝒳), which is possible becausef^*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, theRⁱf_*of Stacks 0770, read inQCoh(𝒪_𝒴)rather than in all ofMod(𝒪_𝒴).
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 overS, letybe a flat object of𝒴and letℱbe an object ofQCoh(𝒪_𝒳). Then the canonical comparison from the sections atyof the quasi-coherent direct image of Stacks 077A to the sections atyof 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
yof the counitε : i Q(𝓖) ⟶ 𝓖of the adjunction of Stacks 0778 at𝓖 = D(i ℱ), whose domain isiof the composite of Stacks 077A byAlgebraicGeometry.Stack.quasicoherentToFlatBaseChange_quasicoherentDirectImageOfEtale_obj. Both halves of the source are covered at once:Dis the étale direct image for the first and itsi-th right derived functor for the second.The hypotheses
hkerandhcokerare 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, byAlgebraicGeometry.Stack.isIso_app_of_isParasitic. The two hypotheses onfare named_hqcand_hqsbecause the argument does not consume them: they are the source's, and they stand behind the carried dataD.
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,yan object of𝒴such thaty : V → 𝒴is flat, and𝓕a quasi-coherent𝒪_𝒳-module. Then(f_*𝓕)(y) = (f_{QCoh,*}𝓕)(y)and(Rⁱf_*𝓕)(y) = (Rⁱf_{QCoh,*}𝓕)(y)for alli: the adjunction mapsf_{QCoh,*}𝓕 = Q(f_*𝓕) ⟶ f_*𝓕andRⁱf_{QCoh,*}𝓕 = Q(Rⁱf_*𝓕) ⟶ Rⁱf_*𝓕of the coherator are bijective on sections aty. Bothf_*𝓕andRⁱf_*𝓕lie inLQCoh^fbc(𝒪_𝒴), so the kernels and cokernels of those maps are parasitic by Stacks 0779 part (2), and vanish aty. Fori < 0both 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 arrowcof Stacks 0GQR:f_*𝓕 ⊗ f_*𝓖 ⟶ f_*(𝓕 ⊗ 𝓖), adjoint to the comparison of Stacks 03EL followed by the counit off^* ⊣ f_*in each factor. It isStacks.Cohomology.DegreeZeroCupProduct.naiveRelativeCupProductat 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-morphismf : 𝒳 ⟶ 𝒴of algebraic stacks:Q(c)precomposed with the comparisonQ(A) ⊗ Q(B) ⟶ Q(A ⊗ B)of Remark 0GQM (AlgebraicGeometry.Stack.AlgebraicStacks.quasicoherentCupProduct_eq). Heref_{QCoh,*} = Q ∘ f_* ∘ i, withf_*the direct image of the morphism of ringed topoifinduces andQthe coheratorAlgebraicGeometry.Stack.AlgebraicStacks.coheratorof𝒴.
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 squaref_{QCoh,*}𝓕 ⊗ f_{QCoh,*}𝓖 ───→ f_*𝓕 ⊗ f_*𝓖 │ │ c ↓ ↓ f_{QCoh,*}(𝓕 ⊗ 𝓖) ─────────→ f_*(𝓕 ⊗ 𝓖)commutes: the left vertical arrow (
AlgebraicGeometry.Stack.AlgebraicStacks.quasicoherentCupProduct, the comparison of Remark 0GQM followed byQ(c)) followed by the counitQ ⟶ idatf_*(𝓕 ⊗ 𝓖)equals the top arrow (icommuting with⊗, then the counit atf_*𝓕and atf_*𝓖) followed by the naive relative cup productc(AlgebraicGeometry.FibredSite.directImageNaiveCupProduct).f_*is the direct image along the morphism of ringed topoifinduces, andQis the coheratorAlgebraicGeometry.Stack.AlgebraicStacks.coheratorof𝒴, 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
cin𝓕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 off^* ⊣ 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 ⊣ Qand the tensor comparisonα: the canonical mapA(Q(f_*F), Q(f_*G)) ⟶ Q(f_*F ⊗ f_*G)followed byQapplied toc.
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 ofadjin each tensor factor — and then downcagrees with going down the left vertical arrow and then right along the counit ofadj.
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 withE_2^{p,q} = H^p(𝒴, R^q f_{QCoh,*} ℱ)converging toH^{p+q}(𝒳, ℱ).The second page is identified for
p, q ≥ 0, vanishes outside the first quadrant, and the sequence abuts toH^n(𝒳, ℱ). HereR^q f_{QCoh,*}isAlgebraicGeometry.Stack.AlgebraicStacks.quasicoherentHigherDirectImage(Stacks 077A), andH^pis the right derived functor ofHom(𝒪, -)on modules at the universeuof the schemes, with values inAddCommGrpCat.{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 morphismf : 𝒳 → 𝒴of algebraic stacks, and letKbe a bounded below complex of𝒪_C-modules, standing for the quasi-coherent moduleℱplaced in degree zero. Suppose given
- a coreflection
incl ⊣ coheratorofMod(𝒪_D)onto a category𝒬: this is the coherator of Stacks 0778,Q : LQCoh^fbc(𝒪_𝒴) ⥤ QCoh(𝒪_𝒴), with its adjunction, whose counitQ 𝓖 ⟶ 𝓖is the adjunction map the source's proof uses;- a class
Parasiticof modules onD: the parasitic modules of Stacks 0773;hkerandhcoker: 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}(𝒳, ℱ), whereR^q f_{QCoh,*}isStacks.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_cokernelturns the counitQ(R^q f_* ℱ) ⟶ R^q f_* ℱ, whose kernel and cokernel are acyclic byhker,hcokerandhvanish, into an isomorphismH^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 : 𝒳 ⟶ 𝒴andg : 𝒴 ⟶ 𝒵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 ton ↦ R^n(g ∘ f)_{QCoh,*} ℱ, zero in negative degrees. HereR^i (-)_{QCoh,*}isAlgebraicGeometry.Stack.AlgebraicStacks.quasicoherentHigherDirectImage, the compositeQ ∘ R^i(-)_* ∘ iof Stacks 077A, andQCoh(𝒪_𝒵)carries its abelian structureAlgebraicGeometry.Stack.AlgebraicStacks.instAbelianQuasicoherentModules; modules have sections in the universeuof 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 coheratorQ_𝒵, which is exact onLQCoh^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 counitQ_𝒴(R^q f_*ℱ) ⟶ R^q f_*ℱ, whose kernel and cokernel are parasitic (Stacks 0779 (1)), hence carried byR^p g_*to parasitic modules (Stacks 0775 (2)) whichQ_𝒵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)andg : (Sh(D), 𝒪_D) → (Sh(E), 𝒪_E)be morphisms of ringed topoi standing for quasi-compact quasi-separated morphismsf : 𝒳 → 𝒴andg : 𝒴 → 𝒵of algebraic stacks, withg ∘ fpresented as their composite by a comparisonτof the geometric direct images, and letKbe a bounded below complex of𝒪_C-modules, standing for the quasi-coherent sheafℱplaced in degree zero. Suppose given
- a coreflection
inclY ⊣ coheratorYofMod(𝒪_D)onto a category𝒬_Y: this is the coherator of Stacks 0778,Q_𝒴 : LQCoh^fbc(𝒪_𝒴) ⥤ QCoh(𝒪_𝒴), with its adjunction, whose counitQ_𝒴 𝓖 ⟶ 𝓖is the adjunction map the source's proof uses;- an exact functor
coheratorZfromMod(𝒪_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
Parasiticof modules onD: the parasitic modules of Stacks 0773;hkerandhcoker: 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 areStacks.Cohomology.Leray.quasicoherentRelativeHigherDirectImageandStacks.Cohomology.Leray.quasicoherentHigherDirectImage, the composites of Stacks 077A, and the abutment isQ_𝒵applied toR^{p+q}(g ∘ f)_*ℱ, which is the same composite in degreep + 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 a1-morphism of algebraic stacks which is representable by algebraic spaces, surjective, flat and locally of finite presentation, and letFbe a sheaf of𝒪_𝒳-modules. Then there is a first-quadrant spectral sequenceE₁^{p,q} = H^q_fppf(𝒰ₚ, fₚ^*F) ⇒ H^{p+q}_fppf(𝒳, F), where𝒰ₚis the degreepterm of the relative Čech nerve offandfₚits projection to𝒳; the identification of the first page isAlgebraicGeometry.Stack.AlgebraicStacks.pageOneIsoModule.The source assumes
Fquasi-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 degreeqfppf cohomology, on the degreepterm𝒰ₚof the relative Čech nerve, of the inverse imagefₚ^*Fof the moduleF.
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 a1-morphism of algebraic stacks which is representable by algebraic spaces, surjective, flat and locally of finite presentation, and letFbe a sheaf of𝒪_𝒳-modules (for instance a quasi-coherent one). Then there is a first-quadrant spectral sequenceE₁^{p,q} = H^q(𝒰ₚ, fₚ^*F) ⇒ H^{p+q}(𝒳, F), where𝒰ₚ = 𝒰 ×_𝒳 ⋯ ×_𝒳 𝒰(p + 1factors) is the degreepterm of the relative Čech nerve offandfₚ : 𝒰ₚ ⟶ 𝒳its projection.The spectral sequence, its first-quadrant vanishing and its convergence to the cohomology of
Fon𝒳are the fields ofStacks.RelativeCech.SpectralSequenceDatafor the abelian sheaf underlyingF; the condition on that datum identifies itsE₁term at(p, q)with the degreeqcohomology of the inverse imagefₚ^*Fof the moduleFon𝒰ₚ.
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 letg : 𝒳 ⟶ 𝒴be a quasi-compact and quasi-separated 1-morphism of algebraic stacks. For a quasi-coherent𝒪_𝒳-module𝓕there is a spectral sequence inQCoh(𝒪_𝒴)withE₁^{p,q} = R^q (g ∘ fₚ)_{QCoh,*} fₚ^* 𝓕, vanishing outside the first quadrant and abutting toR^{p+q} g_{QCoh,*} 𝓕, wherefₚ : 𝒰ₚ ⟶ 𝒳is the projection of the degreepterm𝒰ₚ = 𝒰 ×_𝒳 ⋯ ×_𝒳 𝒰of the Čech nerve off.The source writes the first page as
E₂; its proof applies the coherator to theE₁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 degreeqhigher direct image alongg ∘ fₚof the inverse imagefₚ^*𝓕of the quasi-coherent module𝓕on the degreepterm𝒰ₚof the relative Čech nerve off, 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-morphismfand·|_{U_étale}is restriction alongu_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 spaceU, and letd : ℱ ↦ f^*ℱ|_{U_étale}be the restriction of Stacks 0GQS. For𝒪_𝒳-modulesℱand𝒢withℱquasi-coherent,d(hom(ℱ, 𝒢)) = 𝓗om_{𝒪_U}(d(ℱ), d(𝒢)), wherehom(ℱ, 𝒢) = 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
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.