103.13 Colimits and cohomology to 103.16 Quasi-coherent modules…

Section103.13 Colimits and cohomology#

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

Tag 0GQV, a lemma

Tag 0GQV in the Stacks Project.

AlgebraicGeometry.Stack.isIso_colimit_post_rightDerived_globalSections_associatedTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ColimitsOfCohomology.lean, line 246. The attribute's comment: “the site-theoretic step, at an arbitrary one of the five topologies of Stacks 06TP, hence for the fppf and the étale assertion alike; all four conditions of 0GN4 are assumed here”.

Stacks 0GQV at any one of the sites of Stacks 06TP, from all four conditions of Stacks 0GN4. Let 𝒳 be a category fibred in groupoids over the big fppf category of a scheme S contained in a big fppf site, let τ be a topology on the underlying category of schemes of B, give the total category of 𝒳 the topology it inherits from τ localized at S (Stacks 06TP), and assume of the collection affineObjects of its objects lying over affine schemes that

1. finitely many of them have sheafified representables jointly covering the final sheaf,
2. every covering sieve of a member of it contains a finite covering family by members of it,
3. the product of the sheafified representables of two of them is covered by a finite coproduct of sheafified representables of members of it, and
4. the equalizer of the sheafified representables of two parallel morphisms between members of it is covered by such a finite coproduct.

Then colim_i H^p(𝒳, F_i) ⟶ H^p(𝒳, colim_i F_i) is an isomorphism in every degree p, for every filtered diagram F of abelian sheaves on that site.

This is the site-theoretic step of the source's proof, and the source takes it at two values of τ: the big fppf topology and the big étale topology. Nothing below uses which topology was chosen — the step is an instance of Stacks.Cohomology.ColimitsOfCohomology.isIso_colimit_post_rightDerived_globalSections_of_covers, the form of Stacks 0GN4 for a site whose objects and morphisms do not share a universe, and the site of a category fibred in groupoids over the big fppf category of S does not, its objects lying in Type (u + 1) and its morphisms in Type u. Coefficients, sheaves of sets and the index category of the diagram all live at the join u + 1 of those two universes.

So the two assertions of the source differ only in the four conditions fed to this result. Its fppf and étale instances are AlgebraicGeometry.Stack.isIso_colimit_post_rightDerived_globalSections_fppf, where condition (2) is discharged, and AlgebraicGeometry.Stack.isIso_colimit_post_rightDerived_globalSections_etale, where none of the four is; see "What is proved and what is assumed" in the module docstring for the state of each condition in each topology.

theorem isIso_colimit_post_rightDerived_globalSections_associatedTopology
    (τ : GrothendieckTopology B.Schemes)
    (h_terminal : ∃ (m : ℕ) (U : Fin m → 𝒳.val.obj),
      (∀ i, U i ∈ affineObjects B S hS 𝒳) ∧
        Sheaf.IsLocallySurjective
          (Limits.Sigma.desc fun i => terminal.from
            ((Sheaf.sheafifiedYoneda (associatedTopology B S hS 𝒳.val.p τ)).obj (U i))))
    (h_refine : ∀ x ∈ affineObjects B S hS 𝒳,
      HasFiniteCoverRefinementsFrom (associatedTopology B S hS 𝒳.val.p τ)
        (affineObjects B S hS 𝒳) x)
    (h_product : ∀ U ∈ affineObjects B S hS 𝒳, ∀ U' ∈ affineObjects B S hS 𝒳,
      ∃ (m : ℕ) (V : Fin m → 𝒳.val.obj),
        (∀ i, V i ∈ affineObjects B S hS 𝒳) ∧
          ∃ (p : ∀ i, V i ⟶ U) (q : ∀ i, V i ⟶ U'),
          Sheaf.IsLocallySurjective (Limits.Sigma.desc fun i =>
            prod.lift ((Sheaf.sheafifiedYoneda (associatedTopology B S hS 𝒳.val.p τ)).map (p i))
              ((Sheaf.sheafifiedYoneda (associatedTopology B S hS 𝒳.val.p τ)).map (q i))))
    (h_equalizer : ∀ {U U' : 𝒳.val.obj} (a b : U ⟶ U'),
      U ∈ affineObjects B S hS 𝒳 → U' ∈ affineObjects B S hS 𝒳 →
      ∃ (m : ℕ) (V : Fin m → 𝒳.val.obj),
        (∀ i, V i ∈ affineObjects B S hS 𝒳) ∧
          ∃ (p : ∀ i, V i ⟶ U) (hp : ∀ i, p i ≫ a = p i ≫ b),
          Sheaf.IsLocallySurjective (Limits.Sigma.desc fun i =>
            equalizer.lift
              (f := (Sheaf.sheafifiedYoneda (associatedTopology B S hS 𝒳.val.p τ)).map a)
              (g := (Sheaf.sheafifiedYoneda (associatedTopology B S hS 𝒳.val.p τ)).map b)
              ((Sheaf.sheafifiedYoneda (associatedTopology B S hS 𝒳.val.p τ)).map (p i)) (by
                simpa only [Functor.map_comp] using
                  congrArg (Sheaf.sheafifiedYoneda (associatedTopology B S hS 𝒳.val.p τ)).map
                    (hp i))))
    (p : ℕ) {I : Type (u + 1)} [SmallCategory I] [IsFiltered I]
    (F : I ⥤ Sheaf (associatedTopology B S hS 𝒳.val.p τ) Ab.{u + 1}) :
    IsIso (colimit.post F
      ((Sheaf.Γ (associatedTopology B S hS 𝒳.val.p τ) Ab.{u + 1}).rightDerived p))

AlgebraicGeometry.Stack.isIso_colimit_post_rightDerived_globalSections_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ColimitsOfCohomology.lean, line 311. The attribute's comment: “the site-theoretic step for the fppf site; conditions (1), (3) and (4) of 0GN4 are assumed here”.

Stacks 0GQV in the fppf topology, from conditions (1), (3) and (4) of Stacks 0GN4. Let 𝒳 be a category fibred in groupoids over the big fppf category of a scheme S contained in a big fppf site, give its total category the fppf topology of Stacks 06TP, and assume of the collection affineObjects of its objects lying over affine schemes that

1. finitely many of them have sheafified representables jointly covering the final sheaf,
2. the product of the sheafified representables of two of them is covered by a finite coproduct of sheafified representables of members of it, and
3. the equalizer of the sheafified representables of two parallel morphisms between members of it is covered by such a finite coproduct.

Then colim_i H^p(𝒳, F_i) ⟶ H^p(𝒳, colim_i F_i) is an isomorphism in every degree p, for every filtered diagram F of abelian fppf sheaves on 𝒳.

Condition (2) of Stacks 0GN4 is not assumed: it holds for every category fibred in groupoids, by AlgebraicGeometry.Stack.hasFiniteCoverRefinementsFrom_fppfTopology. Conditions (1), (3) and (4) are what the source derives from quasi-compactness and quasi-separatedness of an algebraic stack; see "What is proved and what is assumed" in the module docstring for the state of each, and Stack.isIso_colimit_post_rightDerived_globalSections_fppf_of_isQuasiCompactStack below for the form of this result in which (1) too is discharged.

This is the fppf instance of AlgebraicGeometry.Stack.isIso_colimit_post_rightDerived_globalSections_associatedTopology, the site-theoretic step taken at an arbitrary topology; the fppf topology of Stacks 06TP is that construction at AlgebraicGeometry.BigFppfSite.topology.

theorem isIso_colimit_post_rightDerived_globalSections_fppf
    (h_terminal : ∃ (m : ℕ) (U : Fin m → 𝒳.val.obj),
      (∀ i, U i ∈ affineObjects B S hS 𝒳) ∧
        Sheaf.IsLocallySurjective
          (Limits.Sigma.desc fun i => terminal.from
            ((Sheaf.sheafifiedYoneda (fppfTopology B S hS 𝒳)).obj (U i))))
    (h_product : ∀ U ∈ affineObjects B S hS 𝒳, ∀ U' ∈ affineObjects B S hS 𝒳,
      ∃ (m : ℕ) (V : Fin m → 𝒳.val.obj),
        (∀ i, V i ∈ affineObjects B S hS 𝒳) ∧
          ∃ (p : ∀ i, V i ⟶ U) (q : ∀ i, V i ⟶ U'),
          Sheaf.IsLocallySurjective (Limits.Sigma.desc fun i =>
            prod.lift ((Sheaf.sheafifiedYoneda (fppfTopology B S hS 𝒳)).map (p i))
              ((Sheaf.sheafifiedYoneda (fppfTopology B S hS 𝒳)).map (q i))))
    (h_equalizer : ∀ {U U' : 𝒳.val.obj} (a b : U ⟶ U'),
      U ∈ affineObjects B S hS 𝒳 → U' ∈ affineObjects B S hS 𝒳 →
      ∃ (m : ℕ) (V : Fin m → 𝒳.val.obj),
        (∀ i, V i ∈ affineObjects B S hS 𝒳) ∧
          ∃ (p : ∀ i, V i ⟶ U) (hp : ∀ i, p i ≫ a = p i ≫ b),
          Sheaf.IsLocallySurjective (Limits.Sigma.desc fun i =>
            equalizer.lift
              (f := (Sheaf.sheafifiedYoneda (fppfTopology B S hS 𝒳)).map a)
              (g := (Sheaf.sheafifiedYoneda (fppfTopology B S hS 𝒳)).map b)
              ((Sheaf.sheafifiedYoneda (fppfTopology B S hS 𝒳)).map (p i)) (by
                simpa only [Functor.map_comp] using
                  congrArg (Sheaf.sheafifiedYoneda (fppfTopology B S hS 𝒳)).map (hp i))))
    (p : ℕ) {I : Type (u + 1)} [SmallCategory I] [IsFiltered I]
    (F : I ⥤ Sheaf (fppfTopology B S hS 𝒳) Ab.{u + 1}) :
    IsIso (colimit.post F
      ((Sheaf.Γ (fppfTopology B S hS 𝒳) Ab.{u + 1}).rightDerived p))

AlgebraicGeometry.Stack.isIso_colimit_post_rightDerived_globalSections_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ColimitsOfCohomology.lean, line 372. The attribute's comment: “the second assertion, in the étale topology: the site-theoretic step for the étale site of Stacks 06TP; conditions (1), (3) and (4) of 0GN4 are assumed here”.

The second assertion of Stacks 0GQV: the same statement in the étale topology, from conditions (1), (3) and (4) of Stacks 0GN4. Let 𝒳 be a category fibred in groupoids over the big fppf category of a scheme S contained in a big fppf site, give its total category the étale topology of Stacks 06TP — the one it inherits from the big étale topology AlgebraicGeometry.etaleTopology of Stacks 03FF localized at S — and assume of the collection affineObjects of its objects lying over affine schemes those three conditions. Then colim_i H^p(𝒳, F_i) ⟶ H^p(𝒳, colim_i F_i) is an isomorphism in every degree p, for every filtered diagram F of abelian étale sheaves on 𝒳.

This is AlgebraicGeometry.Stack.isIso_colimit_post_rightDerived_globalSections_associatedTopology at the big étale topology, and it is the shape in which the source's second assertion — "the same is true for abelian sheaves on 𝒳_étale taking cohomology in the étale topology" — becomes a statement of this library.

Condition (2) of Stacks 0GN4 is not assumed, exactly as in the fppf case: it holds for every category fibred in groupoids, by AlgebraicGeometry.Stack.hasFiniteCoverRefinementsFrom_etaleTopology, whose geometric input is Stacks 0218 where the fppf proof uses Stacks 021P. Condition (1) is likewise available for the étale site, by AlgebraicGeometry.Stack.exists_isAffineObject_isLocallySurjective_terminal_from_etale, and AlgebraicGeometry.Stack .isIso_colimit_post_rightDerived_globalSections_etale_of_isQuasiCompactStack is the form of this result in which it too is discharged. Conditions (3) and (4) remain open for the étale site; see "What is proved and what is assumed" in the module docstring for the state of each of the four.

theorem isIso_colimit_post_rightDerived_globalSections_etale
    (h_terminal : ∃ (m : ℕ) (U : Fin m → 𝒳.val.obj),
      (∀ i, U i ∈ affineObjects B S hS 𝒳) ∧
        Sheaf.IsLocallySurjective
          (Limits.Sigma.desc fun i => terminal.from
            ((Sheaf.sheafifiedYoneda
              (associatedTopology B S hS 𝒳.val.p (etaleTopology B))).obj (U i))))
    (h_product : ∀ U ∈ affineObjects B S hS 𝒳, ∀ U' ∈ affineObjects B S hS 𝒳,
      ∃ (m : ℕ) (V : Fin m → 𝒳.val.obj),
        (∀ i, V i ∈ affineObjects B S hS 𝒳) ∧
          ∃ (p : ∀ i, V i ⟶ U) (q : ∀ i, V i ⟶ U'),
          Sheaf.IsLocallySurjective (Limits.Sigma.desc fun i =>
            prod.lift ((Sheaf.sheafifiedYoneda
                (associatedTopology B S hS 𝒳.val.p (etaleTopology B))).map (p i))
              ((Sheaf.sheafifiedYoneda
                (associatedTopology B S hS 𝒳.val.p (etaleTopology B))).map (q i))))
    (h_equalizer : ∀ {U U' : 𝒳.val.obj} (a b : U ⟶ U'),
      U ∈ affineObjects B S hS 𝒳 → U' ∈ affineObjects B S hS 𝒳 →
      ∃ (m : ℕ) (V : Fin m → 𝒳.val.obj),
        (∀ i, V i ∈ affineObjects B S hS 𝒳) ∧
          ∃ (p : ∀ i, V i ⟶ U) (hp : ∀ i, p i ≫ a = p i ≫ b),
          Sheaf.IsLocallySurjective (Limits.Sigma.desc fun i =>
            equalizer.lift
              (f := (Sheaf.sheafifiedYoneda
                (associatedTopology B S hS 𝒳.val.p (etaleTopology B))).map a)
              (g := (Sheaf.sheafifiedYoneda
                (associatedTopology B S hS 𝒳.val.p (etaleTopology B))).map b)
              ((Sheaf.sheafifiedYoneda
                (associatedTopology B S hS 𝒳.val.p (etaleTopology B))).map (p i)) (by
                simpa only [Functor.map_comp] using
                  congrArg (Sheaf.sheafifiedYoneda
                    (associatedTopology B S hS 𝒳.val.p (etaleTopology B))).map (hp i))))
    (p : ℕ) {I : Type (u + 1)} [SmallCategory I] [IsFiltered I]
    (F : I ⥤ Sheaf (associatedTopology B S hS 𝒳.val.p (etaleTopology B)) Ab.{u + 1}) :
    IsIso (colimit.post F
      ((Sheaf.Γ (associatedTopology B S hS 𝒳.val.p (etaleTopology B))
        Ab.{u + 1}).rightDerived p))

AlgebraicGeometry.Stack.isIso_colimit_post_rightDerived_globalSections_fppf_of_isQuasiCompactStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ColimitsOfCohomology.lean, line 488. The attribute's comment: “for a quasi-compact algebraic stack; conditions (3) and (4) of 0GN4 are assumed”.

Stacks 0GQV in the fppf topology for a quasi-compact algebraic stack, from conditions (3) and (4) of Stacks 0GN4. Let 𝒴 be a quasi-compact algebraic stack over a scheme S contained in a big fppf site and assume of the collection affineObjects of the objects of its fppf site lying over affine schemes that

1. the product of the sheafified representables of two of them is covered by a finite coproduct of sheafified representables of members of it, and
2. the equalizer of the sheafified representables of two parallel morphisms between members of it is covered by such a finite coproduct.

Then colim_i H^p(𝒴, F_i) ⟶ H^p(𝒴, colim_i F_i) is an isomorphism in every degree p, for every filtered diagram F of abelian fppf sheaves on 𝒴.

This is AlgebraicGeometry.Stack.isIso_colimit_post_rightDerived_globalSections_fppf with its condition (1) discharged from quasi-compactness by AlgebraicGeometry.Stack.exists_isAffineObject_isLocallySurjective_terminal_from. The hypothesis is stated for an AlgebraicGeometry.Stack.AlgebraicStacks rather than for a bare category fibred in groupoids because that is what Stacks 04YC and Stacks 075S are about; the conclusion is the one of the previous result at the underlying category fibred in groupoids.

Conditions (3) and (4) are the two the source derives from quasi-separatedness of 𝒴, and both are available: (3) is AlgebraicGeometry.Stack.exists_fin_affineObjects_isLocallySurjective_prodLift and (4) is AlgebraicGeometry.Stack.exists_fin_affineObjects_isLocallySurjective_equalizerLift, each for a stack quasi-separated over a quasi-separated base scheme. They are hypotheses here because this statement asks nothing of quasi-separatedness — no hypothesis of it appears, the two conditions standing in for it — so this is not the full assertion of Stacks 0GQV, whose hypotheses are quasi-compactness and quasi-separatedness alone. That assertion is AlgebraicGeometry.Stack.isIso_colimit_post_rightDerived_globalSections_fppf_of_isQuasiCompact, in StacksFrontier/AlgebraicGeometry/Stacks/ColimitsOfCohomologyEqualizerAffineCover.lean. See "What is proved and what is assumed" in the module docstring.

theorem isIso_colimit_post_rightDerived_globalSections_fppf_of_isQuasiCompactStack
    (𝒴 : AlgebraicStacks.{u, w} B S hS)
    (hqc : IsQuasiCompactStack.{u, w} B S hS 𝒴.val 𝒴.property)
    (h_product : ∀ U ∈ affineObjects B S hS 𝒴.val, ∀ U' ∈ affineObjects B S hS 𝒴.val,
      ∃ (m : ℕ) (V : Fin m → 𝒴.val.val.obj),
        (∀ i, V i ∈ affineObjects B S hS 𝒴.val) ∧
          ∃ (p : ∀ i, V i ⟶ U) (q : ∀ i, V i ⟶ U'),
          Sheaf.IsLocallySurjective (Limits.Sigma.desc fun i =>
            prod.lift ((Sheaf.sheafifiedYoneda (fppfTopology B S hS 𝒴.val)).map (p i))
              ((Sheaf.sheafifiedYoneda (fppfTopology B S hS 𝒴.val)).map (q i))))
    (h_equalizer : ∀ {U U' : 𝒴.val.val.obj} (a b : U ⟶ U'),
      U ∈ affineObjects B S hS 𝒴.val → U' ∈ affineObjects B S hS 𝒴.val →
      ∃ (m : ℕ) (V : Fin m → 𝒴.val.val.obj),
        (∀ i, V i ∈ affineObjects B S hS 𝒴.val) ∧
          ∃ (p : ∀ i, V i ⟶ U) (hp : ∀ i, p i ≫ a = p i ≫ b),
          Sheaf.IsLocallySurjective (Limits.Sigma.desc fun i =>
            equalizer.lift
              (f := (Sheaf.sheafifiedYoneda (fppfTopology B S hS 𝒴.val)).map a)
              (g := (Sheaf.sheafifiedYoneda (fppfTopology B S hS 𝒴.val)).map b)
              ((Sheaf.sheafifiedYoneda (fppfTopology B S hS 𝒴.val)).map (p i)) (by
                simpa only [Functor.map_comp] using
                  congrArg (Sheaf.sheafifiedYoneda (fppfTopology B S hS 𝒴.val)).map (hp i))))
    (p : ℕ) {I : Type (u + 1)} [SmallCategory I] [IsFiltered I]
    (F : I ⥤ Sheaf (fppfTopology B S hS 𝒴.val) Ab.{u + 1}) :
    IsIso (colimit.post F
      ((Sheaf.Γ (fppfTopology B S hS 𝒴.val) Ab.{u + 1}).rightDerived p))

AlgebraicGeometry.Stack.isIso_colimit_post_rightDerived_globalSections_etale_of_isQuasiCompactStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ColimitsOfCohomology.lean, line 549. The attribute's comment: “the second assertion, in the étale topology, for a quasi-compact algebraic stack; conditions (1) and (2) of 0GN4 are now proved for the étale site, conditions (3) and (4) are assumed”.

The second assertion of Stacks 0GQV, in the étale topology, for a quasi-compact algebraic stack, from conditions (3) and (4) of Stacks 0GN4. Let 𝒴 be a quasi-compact algebraic stack over a scheme S contained in a big fppf site and assume of the collection affineObjects of the objects of its étale site lying over affine schemes that

1. the product of the sheafified representables of two of them is covered by a finite coproduct of sheafified representables of members of it, and
2. the equalizer of the sheafified representables of two parallel morphisms between members of it is covered by such a finite coproduct.

Then colim_i H^p(𝒴, F_i) ⟶ H^p(𝒴, colim_i F_i) is an isomorphism in every degree p, for every filtered diagram F of abelian étale sheaves on 𝒴.

This is AlgebraicGeometry.Stack.isIso_colimit_post_rightDerived_globalSections_etale with its condition (1) discharged from quasi-compactness by AlgebraicGeometry.Stack.exists_isAffineObject_isLocallySurjective_terminal_from_etale, exactly as Stack.isIso_colimit_post_rightDerived_globalSections_fppf_of_isQuasiCompactStack discharges it in the fppf topology — the two use Stacks 06XH part (2) and Stacks 06QA respectively on the one affine smooth presentation of Stacks 04YC.

Condition (2) is not assumed, as it is not in the fppf case: for the étale site it is AlgebraicGeometry.Stack.hasFiniteCoverRefinementsFrom_etaleTopology, whose geometric input is Stacks 0218 where the fppf proof uses Stacks 021P. Conditions (3) and (4) are open in both topologies for the same reasons, about the 2-fibre products the source covers rather than about the topology; see "What is proved and what is assumed" in the module docstring. So this is not the full second assertion of Stacks 0GQV, whose hypotheses are quasi-compactness and quasi-separatedness alone; in particular no hypothesis of quasi-separatedness appears here at all, the two conditions standing in for it.

theorem isIso_colimit_post_rightDerived_globalSections_etale_of_isQuasiCompactStack
    (𝒴 : AlgebraicStacks.{u, w} B S hS)
    (hqc : IsQuasiCompactStack.{u, w} B S hS 𝒴.val 𝒴.property)
    (h_product : ∀ U ∈ affineObjects B S hS 𝒴.val, ∀ U' ∈ affineObjects B S hS 𝒴.val,
      ∃ (m : ℕ) (V : Fin m → 𝒴.val.val.obj),
        (∀ i, V i ∈ affineObjects B S hS 𝒴.val) ∧
          ∃ (p : ∀ i, V i ⟶ U) (q : ∀ i, V i ⟶ U'),
          Sheaf.IsLocallySurjective (Limits.Sigma.desc fun i =>
            prod.lift ((Sheaf.sheafifiedYoneda
                (associatedTopology B S hS 𝒴.val.val.p (etaleTopology B))).map (p i))
              ((Sheaf.sheafifiedYoneda
                (associatedTopology B S hS 𝒴.val.val.p (etaleTopology B))).map (q i))))
    (h_equalizer : ∀ {U U' : 𝒴.val.val.obj} (a b : U ⟶ U'),
      U ∈ affineObjects B S hS 𝒴.val → U' ∈ affineObjects B S hS 𝒴.val →
      ∃ (m : ℕ) (V : Fin m → 𝒴.val.val.obj),
        (∀ i, V i ∈ affineObjects B S hS 𝒴.val) ∧
          ∃ (p : ∀ i, V i ⟶ U) (hp : ∀ i, p i ≫ a = p i ≫ b),
          Sheaf.IsLocallySurjective (Limits.Sigma.desc fun i =>
            equalizer.lift
              (f := (Sheaf.sheafifiedYoneda
                (associatedTopology B S hS 𝒴.val.val.p (etaleTopology B))).map a)
              (g := (Sheaf.sheafifiedYoneda
                (associatedTopology B S hS 𝒴.val.val.p (etaleTopology B))).map b)
              ((Sheaf.sheafifiedYoneda
                (associatedTopology B S hS 𝒴.val.val.p (etaleTopology B))).map (p i)) (by
                simpa only [Functor.map_comp] using
                  congrArg (Sheaf.sheafifiedYoneda
                    (associatedTopology B S hS 𝒴.val.val.p (etaleTopology B))).map (hp i))))
    (p : ℕ) {I : Type (u + 1)} [SmallCategory I] [IsFiltered I]
    (F : I ⥤ Sheaf (associatedTopology B S hS 𝒴.val.val.p (etaleTopology B)) Ab.{u + 1}) :
    IsIso (colimit.post F
      ((Sheaf.Γ (associatedTopology B S hS 𝒴.val.val.p (etaleTopology B))
        Ab.{u + 1}).rightDerived p))

AlgebraicGeometry.Stack.isIso_colimit_post_rightDerived_globalSections_fppf_of_isQuasiCompact_absolute, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ColimitsOfCohomologyAbsolute.lean, line 730. The attribute's comment: “the first assertion, in the fppf topology; all four conditions of 0GN4 proved, under the source's own hypotheses -- quasi-compactness of the stack and its absolute quasi-separatedness, with nothing asked of the base scheme of the site”.

Stacks 0GQV in the fppf topology: on a quasi-compact and quasi-separated algebraic stack, cohomology commutes with filtered colimits. Let 𝒳 be such a stack and give its total category the fppf topology of Stacks 06TP. Then colim_i H^p(𝒳, F_i) ⟶ H^p(𝒳, colim_i F_i) is an isomorphism in every degree p, for every filtered diagram F of abelian fppf sheaves on 𝒳.

The hypotheses are the source's and nothing more: quasi-compactness in the sense of Stacks 04YB and quasi-separatedness in the absolute sense of Stacks 050D part (8), quasi-separatedness over Spec ℤ. In particular nothing is asked of the base scheme S of the big fppf site, which the source has no notion of; the containment of the terminal scheme that the absolute notion is stated with is discharged by AlgebraicGeometry.BigFppfSite.contains_terminal rather than assumed.

All four conditions of Stacks 0GN4 are discharged: (1) from quasi-compactness by AlgebraicGeometry.Stack.exists_isAffineObject_isLocallySurjective_terminal_from, (2) for every category fibred in groupoids by AlgebraicGeometry.Stack.hasFiniteCoverRefinementsFrom_fppfTopology, (3) by AlgebraicGeometry.Stack.exists_fin_affineObjects_isLocallySurjective_prodLift_absolute and (4) by AlgebraicGeometry.Stack.exists_fin_affineObjects_isLocallySurjective_equalizerLift_absolute above.

Conditions (3) and (4) need the 2-fibre products the source covers by an affine to be quasi-compact, and that is Stacks 075S. The repository's over-the-base statement of that tag, AlgebraicGeometry.Stack.isQuasiCompactStack_and_isQuasiSeparatedOver_twoFibreProduct, cannot serve: the proof of its part (1) cancels the structure morphism to S, so it needs that morphism to be quasi-compact for a quasi-compact 𝒳, which is AlgebraicGeometry.Stack.compactSpace_prod_of_quasiSeparatedSpace — compactness of V ×_S T for affine objects V, T of the site — and that fails over a base scheme which is not quasi-separated, two affine opens of such a scheme being free to meet in a non-quasi-compact open. So it carries QuasiSeparatedSpace S, which the source does not ask for.

What is used instead is the absolute form, AlgebraicGeometry.Stack.isQuasiCompactMorphism_of_isQuasiCompactStack_absolute, which cancels the structure morphism to Spec ℤ as the source does. It is proved by running the over-the-base statement at the terminal base, where QuasiSeparatedSpace is free — the terminal scheme is affine — and carrying its conclusion back to S along Construction A of Stacks 04X5. That passage is two results: AlgebraicGeometry.Stack.changeBaseTwoFibreProductInv, which identifies the 2-fibre product of the views with the view of the 2-fibre product, and AlgebraicGeometry.Stack.isQuasiCompactStack_changeBaseAlgebraicStack_iff, which descends quasi-compactness from the view to the stack itself through the presentation characterisation of Stacks 04YC and the bijection AlgebraicGeometry.Stack.changeBasePointsEquiv on the point sets of Stacks 04XG.

theorem isIso_colimit_post_rightDerived_globalSections_fppf_of_isQuasiCompact_absolute
    (hqc : IsQuasiCompactStack.{u, w} B S hS 𝒳.val 𝒳.property)
    (h𝒳qs : AlgebraicStacks.IsAbsolutelyQuasiSeparated.{u, w} B S hS B.contains_terminal 𝒳)
    (p : ℕ) {I : Type (u + 1)} [SmallCategory I] [IsFiltered I]
    (F : I ⥤ Sheaf (fppfTopology B S hS 𝒳.val) Ab.{u + 1}) :
    IsIso (colimit.post F
      ((Sheaf.Γ (fppfTopology B S hS 𝒳.val) Ab.{u + 1}).rightDerived p))

AlgebraicGeometry.Stack.isIso_colimit_post_rightDerived_globalSections_etale_of_isQuasiCompact_absolute, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ColimitsOfCohomologyAbsolute.lean, line 831. The attribute's comment: “the second assertion, in the étale topology; all four conditions of 0GN4 proved, under the source's own hypotheses -- quasi-compactness of the stack and its absolute quasi-separatedness, with nothing asked of the base scheme of the site”.

The second assertion of Stacks 0GQV: the same statement in the étale topology. Let 𝒳 be a quasi-compact and quasi-separated algebraic stack and give its total category the étale topology of Stacks 06TP. Then colim_i H^p(𝒳, F_i) ⟶ H^p(𝒳, colim_i F_i) is an isomorphism in every degree p, for every filtered diagram F of abelian étale sheaves on 𝒳.

All four conditions of Stacks 0GN4 are discharged for the étale site: (1) from quasi-compactness by AlgebraicGeometry.Stack.exists_isAffineObject_isLocallySurjective_terminal_from_etale, (2) for every category fibred in groupoids by AlgebraicGeometry.Stack.hasFiniteCoverRefinementsFrom_etaleTopology, (3) by AlgebraicGeometry.Stack .exists_fin_affineObjects_isLocallySurjective_prodLift_etale_absolute and (4) by AlgebraicGeometry.Stack .exists_fin_affineObjects_isLocallySurjective_equalizerLift_etale_absolute above.

The hypotheses are the ones the fppf assertion AlgebraicGeometry.Stack .isIso_colimit_post_rightDerived_globalSections_fppf_of_isQuasiCompact_absolute carries, and they are the source's: quasi-compactness in the sense of Stacks 04YB and quasi-separatedness in the absolute sense of Stacks 050D part (8). Nothing is asked of the base scheme S of the big fppf site, and the containment of the terminal scheme the absolute notion is stated with is discharged by AlgebraicGeometry.BigFppfSite.contains_terminal rather than assumed.

The two topologies agree on where quasi-separatedness is used, and on what form of it: conditions (3) and (4) are about the 2-fibre products the source covers by an affine scheme and not about the topology, so both reach Stacks 075S and both take it in the absolute form AlgebraicGeometry.Stack.isQuasiCompactMorphism_of_isQuasiCompactStack_absolute, which cancels the structure morphism to Spec ℤ as the source does rather than the one to S. See the docstring of the fppf assertion for why the over-the-base statement of Stacks 075S cannot serve, and StacksFrontier/AlgebraicGeometry/Stacks/QuasiCompactQuasiSeparatedStackAbsolute.lean for how the absolute form is proved from it.

theorem isIso_colimit_post_rightDerived_globalSections_etale_of_isQuasiCompact_absolute
    (hqc : IsQuasiCompactStack.{u, w} B S hS 𝒳.val 𝒳.property)
    (h𝒳qs : AlgebraicStacks.IsAbsolutelyQuasiSeparated.{u, w} B S hS B.contains_terminal 𝒳)
    (p : ℕ) {I : Type (u + 1)} [SmallCategory I] [IsFiltered I]
    (F : I ⥤ Sheaf (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B)) Ab.{u + 1}) :
    IsIso (colimit.post F
      ((Sheaf.Γ (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
        Ab.{u + 1}).rightDerived p))

AlgebraicGeometry.Stack.hasFiniteCoverRefinementsFrom_fppfTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ColimitsOfCohomologyAffineRefinement.lean, line 167. The attribute's comment: “condition (2) of Stacks 0GN4 for the fppf site, from Stacks 021P”.

Condition (2) of Stacks 0GN4 for the fppf site of a category fibred in groupoids over the big fppf category of S, at the objects lying over affine schemes. Every covering sieve of an object of 𝒳 lying over an affine scheme contains a finite covering family whose members again lie over affine schemes.

This is the second of the four conditions the proof of Stacks 0GQV checks, the collection B of that proof being the objects of the site lying over affine schemes; the source derives it from Stacks 021P, and so does the proof here.

The refinement is produced downstairs by AlgebraicGeometry.BigFppfOver.exists_finite_affine_covering_refinement and transported to 𝒳 by AlgebraicGeometry.Stack.exists_chosenCovering_le_of_mem_associatedTopology; the transported family covers because its image is a chosen covering family of the big fppf category over S and because in a category fibred in groupoids every morphism is strongly cartesian over its image, which is what the covering families of Stacks 06NU ask of its members. See the module documentation for the two bookkeeping steps: restricting the base-level input to affine targets, and reindexing a finite index type by Fin n.

The tag registers this one condition of the proof of Stacks 0GQV and nothing more: the assertion of Stacks 0GN4 is that the four conditions suffice, which is Stacks.Cohomology.ColimitsOfCohomology.isIso_colimit_post_rightDerived_globalSections_of_covers, and the full assertions of Stacks 0GQV are AlgebraicGeometry.Stack.isIso_colimit_post_rightDerived_globalSections_fppf_of_isQuasiCompact and AlgebraicGeometry.Stack.isIso_colimit_post_rightDerived_globalSections_etale_of_isQuasiCompact.

theorem hasFiniteCoverRefinementsFrom_fppfTopology
    {x : 𝒳.val.obj} (hx : IsAffineObject B S hS 𝒳.val.p x) :
    HasFiniteCoverRefinementsFrom (fppfTopology B S hS 𝒳)
      {y : 𝒳.val.obj | IsAffineObject B S hS 𝒳.val.p y} x

AlgebraicGeometry.Stack.exists_isAffineObject_isLocallySurjective_terminal_from, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ColimitsOfCohomologyAtlasCovers.lean, line 325. The attribute's comment: “condition (1) of Stacks 0GN4 for the fppf site, from Stacks 04YC and Stacks 06QA”.

Condition (1) of Stacks 0GN4 for the fppf site of a quasi-compact algebraic stack, with one object. There is an object x of the site lying over an affine scheme for which the sheafification h_x^# of its representable surjects onto the final sheaf.

This is exists_isAffineObject_isLocallySurjective_terminal_from_associatedTopology at the big fppf topology, with Stacks 06QA for the fibre lifts as in AlgebraicGeometry.Stack.exists_isAffineObject_cover_nonempty_hom.

theorem exists_isAffineObject_isLocallySurjective_terminal_from
    (hqc : IsQuasiCompactStack.{u, w} B S hS 𝒳.val 𝒳.property) :
    ∃ x : 𝒳.val.val.obj, IsAffineObject B S hS 𝒳.val.val.p x ∧
      Sheaf.IsLocallySurjective (terminal.from
        ((Sheaf.sheafifiedYoneda (fppfTopology B S hS 𝒳.val)).obj x))

AlgebraicGeometry.Stack.exists_isAffineObject_isLocallySurjective_terminal_from_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ColimitsOfCohomologyAtlasCovers.lean, line 350. The attribute's comment: “condition (1) of Stacks 0GN4 for the étale site, from Stacks 04YC and Stacks 06XH part (2)”.

Condition (1) of Stacks 0GN4 for the étale site of a quasi-compact algebraic stack, with one object. There is an object x of the site lying over an affine scheme for which the sheafification h_x^# of its representable surjects onto the final sheaf in the étale topology.

This is the first of the four conditions the proof of Stacks 0GQV checks, for the second of the two topologies the source asserts the tag in. It is exists_isAffineObject_isLocallySurjective_terminal_from_associatedTopology at the big étale topology, with Stacks 06XH part (2) for the fibre lifts as in AlgebraicGeometry.Stack.exists_isAffineObject_cover_nonempty_hom_etale.

The source checks this condition by saying that the affine smooth surjection of Stacks 04YC makes h_x^# ⟶ * an epimorphism of sheaves on 𝒳_τ, which for τ the étale topology is the assertion that a surjective smooth 1-morphism has sections étale-locally. That is Stacks 06XH part (2), and it is the only place the étale proof of this condition differs from the fppf one.

theorem exists_isAffineObject_isLocallySurjective_terminal_from_etale
    (hqc : IsQuasiCompactStack.{u, w} B S hS 𝒳.val 𝒳.property) :
    ∃ x : 𝒳.val.val.obj, IsAffineObject B S hS 𝒳.val.val.p x ∧
      Sheaf.IsLocallySurjective (terminal.from
        ((Sheaf.sheafifiedYoneda
          (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))).obj x))

AlgebraicGeometry.Stack.isIso_colimit_post_rightDerived_globalSections_fppf_of_isQuasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ColimitsOfCohomologyEqualizerAffineCover.lean, line 634. The attribute's comment: “the first assertion, in the fppf topology, for a quasi-compact algebraic stack quasi-separated over a quasi-separated base scheme; all four conditions of 0GN4 proved”.

Stacks 0GQV in the fppf topology for a quasi-compact algebraic stack which is quasi-separated over a quasi-separated base scheme. Let 𝒳 be such a stack and give its total category the fppf topology of Stacks 06TP. Then colim_i H^p(𝒳, F_i) ⟶ H^p(𝒳, colim_i F_i) is an isomorphism in every degree p, for every filtered diagram F of abelian fppf sheaves on 𝒳.

All four conditions of Stacks 0GN4 are discharged: (1) from quasi-compactness by AlgebraicGeometry.Stack.exists_isAffineObject_isLocallySurjective_terminal_from, (2) for every category fibred in groupoids by AlgebraicGeometry.Stack.hasFiniteCoverRefinementsFrom_fppfTopology, (3) by AlgebraicGeometry.Stack.exists_fin_affineObjects_isLocallySurjective_prodLift and (4) by AlgebraicGeometry.Stack.exists_fin_affineObjects_isLocallySurjective_equalizerLift above.

The quasi-separatedness hypothesis is AlgebraicGeometry.Stack.IsQuasiSeparatedOver of 𝒳 together with quasi-separatedness of the base scheme S, which is what Stacks 075S asks for and what conditions (3) and (4) use.

theorem isIso_colimit_post_rightDerived_globalSections_fppf_of_isQuasiCompact
    (hqc : IsQuasiCompactStack.{u, w} B S hS 𝒳.val 𝒳.property)
    (p : ℕ) {I : Type (u + 1)} [SmallCategory I] [IsFiltered I]
    (F : I ⥤ Sheaf (fppfTopology B S hS 𝒳.val) Ab.{u + 1}) :
    IsIso (colimit.post F
      ((Sheaf.Γ (fppfTopology B S hS 𝒳.val) Ab.{u + 1}).rightDerived p))

AlgebraicGeometry.Stack.hasFiniteCoverRefinementsFrom_etaleTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ColimitsOfCohomologyEtaleAffineRefinement.lean, line 173. The attribute's comment: “condition (2) of Stacks 0GN4 for the étale site, from Stacks 0218”.

Condition (2) of Stacks 0GN4 for the étale site of a category fibred in groupoids over the big fppf category of S, at the objects lying over affine schemes. Every covering sieve of an object of 𝒳 lying over an affine scheme contains a finite covering family whose members again lie over affine schemes, the topology on 𝒳 being the one it inherits (Stacks 06TP) from the big étale topology of Stacks 03FF localized at S.

This is the second of the four conditions the proof of Stacks 0GQV checks, the collection B of that proof being the objects of the site lying over affine schemes. For the fppf site the source derives it from Stacks 021P; in the étale topology the corresponding input is Stacks 0218, and that is what is used here, through AlgebraicGeometry.BigFppfOver.exists_finite_affine_etaleCovering_refinement.

The refinement is transported to 𝒳 by AlgebraicGeometry.Stack.exists_chosenCovering_le_of_mem_associatedTopology at the big étale topology; the transported family covers because its image is a selected étale covering family of the big fppf category over S and because in a category fibred in groupoids every morphism is strongly cartesian over its image, which is what the covering families of Stacks 06NU ask of its members. See the module documentation for the two bookkeeping steps: restricting the base-level input to affine targets, and reindexing a finite index type by Fin n.

This is the étale counterpart of AlgebraicGeometry.Stack.hasFiniteCoverRefinementsFrom_fppfTopology, and like it holds for every category fibred in groupoids, with no quasi-compactness hypothesis.

theorem hasFiniteCoverRefinementsFrom_etaleTopology
    {x : 𝒳.val.obj} (hx : IsAffineObject B S hS 𝒳.val.p x) :
    HasFiniteCoverRefinementsFrom (associatedTopology B S hS 𝒳.val.p (etaleTopology B))
      {y : 𝒳.val.obj | IsAffineObject B S hS 𝒳.val.p y} x

AlgebraicGeometry.Stack.isIso_colimit_post_rightDerived_globalSections_etale_of_isQuasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ColimitsOfCohomologyEtaleEqualizerAffineCover.lean, line 177. The attribute's comment: “the second assertion, in the étale topology, for a quasi-compact algebraic stack quasi-separated over a quasi-separated base scheme; all four conditions of 0GN4 proved”.

Stacks 0GQV in the étale topology for a quasi-compact algebraic stack which is quasi-separated over a quasi-separated base scheme. Let 𝒳 be such a stack and give its total category the étale topology of Stacks 06TP. Then colim_i H^p(𝒳, F_i) ⟶ H^p(𝒳, colim_i F_i) is an isomorphism in every degree p, for every filtered diagram F of abelian étale sheaves on 𝒳.

All four conditions of Stacks 0GN4 are discharged for the étale site: (1) from quasi-compactness by AlgebraicGeometry.Stack.exists_isAffineObject_isLocallySurjective_terminal_from_etale, (2) for every category fibred in groupoids by AlgebraicGeometry.Stack.hasFiniteCoverRefinementsFrom_etaleTopology, (3) by AlgebraicGeometry.Stack.exists_fin_affineObjects_isLocallySurjective_prodLift_etale and (4) by AlgebraicGeometry.Stack.exists_fin_affineObjects_isLocallySurjective_equalizerLift_etale above.

The quasi-separatedness hypothesis is AlgebraicGeometry.Stack.IsQuasiSeparatedOver of 𝒳 together with quasi-separatedness of the base scheme S, which is what Stacks 075S asks for and what conditions (3) and (4) use. It is the same hypothesis the fppf assertion AlgebraicGeometry.Stack.isIso_colimit_post_rightDerived_globalSections_fppf_of_isQuasiCompact carries, and for the same reason: quasi-compactness of the 2-fibre products the source covers by an affine scheme is Stacks 075S part (3).

theorem isIso_colimit_post_rightDerived_globalSections_etale_of_isQuasiCompact
    (hqsS : QuasiSeparatedSpace S)
    (hqc : IsQuasiCompactStack.{u, w} B S hS 𝒳.val 𝒳.property)
    (h𝒳 : IsQuasiSeparatedOver.{u, w} B S hS 𝒳)
    (p : ℕ) {I : Type (u + 1)} [SmallCategory I] [IsFiltered I]
    (F : I ⥤ Sheaf (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B)) Ab.{u + 1}) :
    IsIso (colimit.post F
      ((Sheaf.Γ (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
        Ab.{u + 1}).rightDerived p))

AlgebraicGeometry.Stack.isIso_colimit_post_rightDerived_globalSections_etale_of_isQuasiSeparatedOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ColimitsOfCohomologyEtaleProductAffineCover.lean, line 428. The attribute's comment: “the second assertion, in the étale topology, for a quasi-compact algebraic stack quasi-separated over a quasi-separated base; conditions (1), (2) and (3) of 0GN4 are now proved for the étale site, condition (4) is still assumed”.

The second assertion of Stacks 0GQV, in the étale topology, for a quasi-compact algebraic stack which is quasi-separated over a quasi-separated base scheme, from condition (4) of Stacks 0GN4 alone.

This is AlgebraicGeometry.Stack .isIso_colimit_post_rightDerived_globalSections_etale_of_isQuasiCompactStack with its condition (3) discharged by AlgebraicGeometry.Stack.exists_fin_affineObjects_isLocallySurjective_prodLift_etale. Condition (4), the corresponding assertion for the equalizer of two parallel morphisms, is still assumed: the 2-fibre product the source covers by an affine scheme in that case is the one of a single 1-morphism against the diagonal, not of two 2-Yoneda 1-morphisms, so the quadruple of this file does not discharge it, in this topology any more than in the fppf one. So this is not yet the full second assertion of Stacks 0GQV.

theorem isIso_colimit_post_rightDerived_globalSections_etale_of_isQuasiSeparatedOver
    (hqsS : QuasiSeparatedSpace S)
    (hqc : IsQuasiCompactStack.{u, w} B S hS 𝒳.val 𝒳.property)
    (h𝒳 : IsQuasiSeparatedOver.{u, w} B S hS 𝒳)
    (h_equalizer : ∀ {U U' : 𝒳.val.val.obj} (a b : U ⟶ U'),
      U ∈ affineObjects B S hS 𝒳.val → U' ∈ affineObjects B S hS 𝒳.val →
      ∃ (m : ℕ) (V : Fin m → 𝒳.val.val.obj),
        (∀ i, V i ∈ affineObjects B S hS 𝒳.val) ∧
          ∃ (p : ∀ i, V i ⟶ U) (hp : ∀ i, p i ≫ a = p i ≫ b),
          Sheaf.IsLocallySurjective (Limits.Sigma.desc fun i =>
            equalizer.lift
              (f := (Sheaf.sheafifiedYoneda
                (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))).map a)
              (g := (Sheaf.sheafifiedYoneda
                (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))).map b)
              ((Sheaf.sheafifiedYoneda
                (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))).map (p i)) (by
                simpa only [Functor.map_comp] using
                  congrArg (Sheaf.sheafifiedYoneda
                    (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))).map (hp i))))
    (p : ℕ) {I : Type (u + 1)} [SmallCategory I] [IsFiltered I]
    (F : I ⥤ Sheaf (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B)) Ab.{u + 1}) :
    IsIso (colimit.post F
      ((Sheaf.Γ (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
        Ab.{u + 1}).rightDerived p))

AlgebraicGeometry.Stack.isIso_colimit_post_rightDerived_globalSections_fppf_of_isQuasiSeparatedOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ColimitsOfCohomologyProductAffineCover.lean, line 433. The attribute's comment: “for a quasi-compact algebraic stack quasi-separated over a quasi-separated base; condition (3) of 0GN4 is proved here and condition (4) is a hypothesis, discharged in ColimitsOfCohomologyEqualizerAffineCover”.

Stacks 0GQV in the fppf topology for a quasi-compact algebraic stack which is quasi-separated over a quasi-separated base scheme, from condition (4) of Stacks 0GN4 alone.

This is Stack.isIso_colimit_post_rightDerived_globalSections_fppf_of_isQuasiCompactStack with its condition (3) discharged by AlgebraicGeometry.Stack.exists_fin_affineObjects_isLocallySurjective_prodLift. Condition (4), the corresponding assertion for the equalizer of two parallel morphisms, remains a hypothesis here because the quadruple of this file does not give it: the 2-fibre product it is about is not the one of two 2-Yoneda 1-morphisms but the one of the two graphs of a and b over that one. It is proved, for a stack quasi-separated over a quasi-separated base scheme, as AlgebraicGeometry.Stack.exists_fin_affineObjects_isLocallySurjective_equalizerLift in StacksFrontier/AlgebraicGeometry/Stacks/ColimitsOfCohomologyEqualizerAffineCover.lean, and discharging it there turns this result into the full fppf assertion of Stacks 0GQV, AlgebraicGeometry.Stack.isIso_colimit_post_rightDerived_globalSections_fppf_of_isQuasiCompact.

theorem isIso_colimit_post_rightDerived_globalSections_fppf_of_isQuasiSeparatedOver
    (hqsS : QuasiSeparatedSpace S)
    (hqc : IsQuasiCompactStack.{u, w} B S hS 𝒳.val 𝒳.property)
    (h𝒳 : IsQuasiSeparatedOver.{u, w} B S hS 𝒳)
    (h_equalizer : ∀ {U U' : 𝒳.val.val.obj} (a b : U ⟶ U'),
      U ∈ affineObjects B S hS 𝒳.val → U' ∈ affineObjects B S hS 𝒳.val →
      ∃ (m : ℕ) (V : Fin m → 𝒳.val.val.obj),
        (∀ i, V i ∈ affineObjects B S hS 𝒳.val) ∧
          ∃ (p : ∀ i, V i ⟶ U) (hp : ∀ i, p i ≫ a = p i ≫ b),
          Sheaf.IsLocallySurjective (Limits.Sigma.desc fun i =>
            equalizer.lift
              (f := (Sheaf.sheafifiedYoneda (fppfTopology B S hS 𝒳.val)).map a)
              (g := (Sheaf.sheafifiedYoneda (fppfTopology B S hS 𝒳.val)).map b)
              ((Sheaf.sheafifiedYoneda (fppfTopology B S hS 𝒳.val)).map (p i)) (by
                simpa only [Functor.map_comp] using
                  congrArg (Sheaf.sheafifiedYoneda (fppfTopology B S hS 𝒳.val)).map (hp i))))
    (p : ℕ) {I : Type (u + 1)} [SmallCategory I] [IsFiltered I]
    (F : I ⥤ Sheaf (fppfTopology B S hS 𝒳.val) Ab.{u + 1}) :
    IsIso (colimit.post F
      ((Sheaf.Γ (fppfTopology B S hS 𝒳.val) Ab.{u + 1}).rightDerived p))

Tag 0GQW, a lemma

Tag 0GQW in the Stacks Project.

AlgebraicGeometry.Stack.preservesColimitsOfShape_rightDerived_abelianDirectImage_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ColimitsOfHigherDirectImages.lean, line 254. The attribute's comment: “fppf topology; the sheafification step only — that the cohomology of the fibres of f commutes with the colimit is assumed, as is the value half of 075G that identifies it”.

The sheafification step of Stacks 0GQW in the fppf topology. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over a scheme S contained in a big fppf site. If for every object y of the fppf site of 𝒴 the n-th derived functor of AlgebraicGeometry.Stack.fibreSections at y commutes with colimits of shape I, then so does the n-th higher direct image R^n f_* of abelian fppf sheaves.

This is AlgebraicGeometry.Stack.preservesColimitsOfShape_rightDerived_abelianDirectImage at the fppf topology of Stacks 06TP. It is the first of the two steps of the source's proof; the hypothesis is the second, and is what quasi-compactness and quasi-separatedness of f are used for. See "What is proved and what is assumed" in the module docstring for exactly what is missing: the value half of Stacks 075G, and conditions (3) and (4) of Stacks 0GN4 in the library's form of Stacks 0GQV.

theorem preservesColimitsOfShape_rightDerived_abelianDirectImage_fppf (n : ℕ)
    {I : Type v} [Category.{v'} I] [IsFiltered I]
    (h :
      letI := site_hasSheafify_addCommGrp.{u + 1, u, a}
        (J := BigFppfOver.associatedTopology B S hS 𝒳.val.val.p .fppf)
      letI := Sheaf.isGrothendieckAbelian_of_essentiallySmall.{max (u + 1) a}
        (BigFppfOver.associatedTopology B S hS 𝒳.val.val.p .fppf)
        AddCommGrpCat.{max (u + 1) a}
      letI := IsGrothendieckAbelian.enoughInjectives
        (C := Sheaf (BigFppfOver.associatedTopology B S hS 𝒳.val.val.p .fppf)
          AddCommGrpCat.{max (u + 1) a})
      ∀ y : 𝒴.val.val.obj, PreservesColimitsOfShape I
        ((fibreSections.{u, a} B S hS 𝒳.val.val.p
          (CatFiberedInGroupoids.homFunctor f.hom) .fppf y).rightDerived n)) :
    letI := site_hasSheafify_addCommGrp.{u + 1, u, a}
      (J := BigFppfOver.associatedTopology B S hS 𝒳.val.val.p .fppf)
    letI := site_hasSheafify_addCommGrp.{u + 1, u, a}
      (J := BigFppfOver.associatedTopology B S hS 𝒴.val.val.p .fppf)
    letI := Sheaf.isGrothendieckAbelian_of_essentiallySmall.{max (u + 1) a}
      (BigFppfOver.associatedTopology B S hS 𝒳.val.val.p .fppf) AddCommGrpCat.{max (u + 1) a}
    letI := IsGrothendieckAbelian.enoughInjectives
      (C := Sheaf (BigFppfOver.associatedTopology B S hS 𝒳.val.val.p .fppf)
        AddCommGrpCat.{max (u + 1) a})
    letI := abelianDirectImageAdditive.{u, w, a} B S hS f .fppf
    PreservesColimitsOfShape I
      (((CatFiberedInGroupoids.homFunctor f.hom).sheafPushforwardCocontinuous
        AddCommGrpCat.{max (u + 1) a}
        (BigFppfOver.associatedTopology B S hS 𝒳.val.val.p .fppf)
        (BigFppfOver.associatedTopology B S hS 𝒴.val.val.p .fppf)).rightDerived n)

AlgebraicGeometry.Stack.preservesColimitsOfShape_rightDerived_abelianDirectImage_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ColimitsOfHigherDirectImages.lean, line 299. The attribute's comment: “étale topology; the sheafification step only — that the cohomology of the fibres of f commutes with the colimit is assumed, as is the value half of 075G that identifies it”.

The sheafification step of Stacks 0GQW in the étale topology. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over a scheme S contained in a big fppf site. If for every object y of the étale site of 𝒴 the n-th derived functor of AlgebraicGeometry.Stack.fibreSections at y commutes with colimits of shape I, then so does the n-th higher direct image R^n f_* of abelian étale sheaves.

This is AlgebraicGeometry.Stack.preservesColimitsOfShape_rightDerived_abelianDirectImage at the étale topology of Stacks 06TP. It is the first of the two steps of the source's proof; the hypothesis is the second, and is what quasi-compactness and quasi-separatedness of f are used for. See "What is proved and what is assumed" in the module docstring for exactly what is missing: the value half of Stacks 075G, and the étale analogues of conditions (3) and (4) of Stacks 0GN4 in the library's form of Stacks 0GQV.

theorem preservesColimitsOfShape_rightDerived_abelianDirectImage_etale (n : ℕ)
    {I : Type v} [Category.{v'} I] [IsFiltered I]
    (h :
      letI := site_hasSheafify_addCommGrp.{u + 1, u, a}
        (J := BigFppfOver.associatedTopology B S hS 𝒳.val.val.p .etale)
      letI := Sheaf.isGrothendieckAbelian_of_essentiallySmall.{max (u + 1) a}
        (BigFppfOver.associatedTopology B S hS 𝒳.val.val.p .etale)
        AddCommGrpCat.{max (u + 1) a}
      letI := IsGrothendieckAbelian.enoughInjectives
        (C := Sheaf (BigFppfOver.associatedTopology B S hS 𝒳.val.val.p .etale)
          AddCommGrpCat.{max (u + 1) a})
      ∀ y : 𝒴.val.val.obj, PreservesColimitsOfShape I
        ((fibreSections.{u, a} B S hS 𝒳.val.val.p
          (CatFiberedInGroupoids.homFunctor f.hom) .etale y).rightDerived n)) :
    letI := site_hasSheafify_addCommGrp.{u + 1, u, a}
      (J := BigFppfOver.associatedTopology B S hS 𝒳.val.val.p .etale)
    letI := site_hasSheafify_addCommGrp.{u + 1, u, a}
      (J := BigFppfOver.associatedTopology B S hS 𝒴.val.val.p .etale)
    letI := Sheaf.isGrothendieckAbelian_of_essentiallySmall.{max (u + 1) a}
      (BigFppfOver.associatedTopology B S hS 𝒳.val.val.p .etale) AddCommGrpCat.{max (u + 1) a}
    letI := IsGrothendieckAbelian.enoughInjectives
      (C := Sheaf (BigFppfOver.associatedTopology B S hS 𝒳.val.val.p .etale)
        AddCommGrpCat.{max (u + 1) a})
    letI := abelianDirectImageAdditive.{u, w, a} B S hS f .etale
    PreservesColimitsOfShape I
      (((CatFiberedInGroupoids.homFunctor f.hom).sheafPushforwardCocontinuous
        AddCommGrpCat.{max (u + 1) a}
        (BigFppfOver.associatedTopology B S hS 𝒳.val.val.p .etale)
        (BigFppfOver.associatedTopology B S hS 𝒴.val.val.p .etale)).rightDerived n)

AlgebraicGeometry.Stack.preservesColimitsOfShape_rightDerived_abelianDirectImage_fppf_of_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ColimitsOfHigherDirectImagesQcqs.lean, line 699. The attribute's comment: “first assertion: the fppf topology, for f quasi-compact and quasi-separated”.

Stacks 0GQW, first assertion: the fppf topology. Let f : 𝒳 ⟶ 𝒴 be a quasi-compact and quasi-separated 1-morphism of algebraic stacks. Then for every p ≥ 0 the higher direct image Rᵖf_* of abelian fppf sheaves commutes with filtered colimits: Rᵖf_*(colim_i ℱ_i) = colim_i Rᵖf_*ℱ_i.

The proof is the source's. Rᵖf_*ℱ is the sheaf associated to the presheaf y ↦ Hᵖ((Sch/V) ×_{y, 𝒴} 𝒳, pr⁻¹ℱ) (Stacks 075G: the sheafification half is AlgebraicGeometry.Stack.abelianHigherDirectImage_iso_sheafify_fibreCohomology, the value half AlgebraicGeometry.Stack.rightDerivedFibreSectionsIso), and the colimit of sheaves is the sheaf associated to the presheaf colimit. When V is affine the 2-fibre product is quasi-compact and quasi-separated (AlgebraicGeometry.Stack .isQuasiCompactStack_and_isAbsolutelyQuasiSeparated_twoFibreProduct_objectMorphism), so Stacks 0GQV applies to its cohomology (AlgebraicGeometry.Stack.preservesColimitsOfShape_rightDerived_fibreSections_fppf), and every object of the fppf site of 𝒴 has a covering by objects lying over affine schemes (AlgebraicGeometry.FibredSite.exists_affine_ofArrows), which is AlgebraicGeometry.Stack .preservesColimitsOfShape_rightDerived_abelianDirectImage_of_isAffineObject.

Quasi-compactness is Stacks 050U (AlgebraicGeometry.Stack.IsQuasiCompactMorphism) and quasi-separatedness Stacks 04YW (AlgebraicGeometry.Stack.AlgebraicStacks.IsQuasiSeparated). The abelian sheaves take values in AddCommGrpCat.{u + 1} and the diagram is indexed by a small filtered category at that universe, as in Stacks 0GQV.

theorem preservesColimitsOfShape_rightDerived_abelianDirectImage_fppf_of_qcqs
    (hfqc : IsQuasiCompactMorphism.{u, w} B S hS f)
    (hfqs : AlgebraicStacks.IsQuasiSeparated.{u, w} B S hS f) (n : ℕ)
    (I : Type (u + 1)) [SmallCategory I] [IsFiltered I] :
    letI := site_hasSheafify_addCommGrp.{u + 1, u, 0}
      (J := BigFppfOver.associatedTopology B S hS 𝒳.val.val.p .fppf)
    letI := site_hasSheafify_addCommGrp.{u + 1, u, 0}
      (J := BigFppfOver.associatedTopology B S hS 𝒴.val.val.p .fppf)
    letI := Sheaf.isGrothendieckAbelian_of_essentiallySmall.{u + 1}
      (BigFppfOver.associatedTopology B S hS 𝒳.val.val.p .fppf) AddCommGrpCat.{u + 1}
    letI := IsGrothendieckAbelian.enoughInjectives
      (C := Sheaf (BigFppfOver.associatedTopology B S hS 𝒳.val.val.p .fppf) AddCommGrpCat.{u + 1})
    letI := abelianDirectImageAdditive.{u, w, 0} B S hS f .fppf
    PreservesColimitsOfShape I
      (((Fn).sheafPushforwardCocontinuous AddCommGrpCat.{u + 1}
        (BigFppfOver.associatedTopology B S hS 𝒳.val.val.p .fppf)
        (BigFppfOver.associatedTopology B S hS 𝒴.val.val.p .fppf)).rightDerived n)

AlgebraicGeometry.Stack.preservesColimitsOfShape_rightDerived_abelianDirectImage_etale_of_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ColimitsOfHigherDirectImagesQcqs.lean, line 733. The attribute's comment: “second assertion: the étale topology, for f quasi-compact and quasi-separated”.

Stacks 0GQW, second assertion: the étale topology. Let f : 𝒳 ⟶ 𝒴 be a quasi-compact and quasi-separated 1-morphism of algebraic stacks. Then for every p ≥ 0 the higher direct image Rᵖf_* of abelian sheaves on the étale sites, taken in the étale topology, commutes with filtered colimits: Rᵖf_*(colim_i ℱ_i) = colim_i Rᵖf_*ℱ_i.

The proof is that of the fppf assertion AlgebraicGeometry.Stack.preservesColimitsOfShape_rightDerived_abelianDirectImage_fppf_of_qcqs, with the étale assertion of Stacks 0GQV (AlgebraicGeometry.Stack.preservesColimitsOfShape_rightDerived_fibreSections_etale) and the covering of every object of the étale site of 𝒴 by objects lying over affine schemes (AlgebraicGeometry.Stack.exists_affine_ofArrows_etale).

theorem preservesColimitsOfShape_rightDerived_abelianDirectImage_etale_of_qcqs
    (hfqc : IsQuasiCompactMorphism.{u, w} B S hS f)
    (hfqs : AlgebraicStacks.IsQuasiSeparated.{u, w} B S hS f) (n : ℕ)
    (I : Type (u + 1)) [SmallCategory I] [IsFiltered I] :
    letI := site_hasSheafify_addCommGrp.{u + 1, u, 0}
      (J := BigFppfOver.associatedTopology B S hS 𝒳.val.val.p .etale)
    letI := site_hasSheafify_addCommGrp.{u + 1, u, 0}
      (J := BigFppfOver.associatedTopology B S hS 𝒴.val.val.p .etale)
    letI := Sheaf.isGrothendieckAbelian_of_essentiallySmall.{u + 1}
      (BigFppfOver.associatedTopology B S hS 𝒳.val.val.p .etale) AddCommGrpCat.{u + 1}
    letI := IsGrothendieckAbelian.enoughInjectives
      (C := Sheaf (BigFppfOver.associatedTopology B S hS 𝒳.val.val.p .etale) AddCommGrpCat.{u + 1})
    letI := abelianDirectImageAdditive.{u, w, 0} B S hS f .etale
    PreservesColimitsOfShape I
      (((Fn).sheafPushforwardCocontinuous AddCommGrpCat.{u + 1}
        (BigFppfOver.associatedTopology B S hS 𝒳.val.val.p .etale)
        (BigFppfOver.associatedTopology B S hS 𝒴.val.val.p .etale)).rightDerived n)

Tag 0GQX, a lemma

Tag 0GQX in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.preservesCoproducts_and_filteredColimits_quasicoherentDirectImages_of_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentDirectImageFilteredColimits.lean, line 165. The attribute's comment: “the whole lemma, for f quasi-compact and quasi-separated and the functors f_{QCoh,} and R^i f_{QCoh,} (i ≥ 0) of Stacks 077A: each commutes with direct sums (indexed by ι : Type u) and with filtered colimits (indexed by filtered J : Type u)”.

Stacks 0GQX. Let f : 𝒳 ⟶ 𝒴 be a quasi-compact and quasi-separated 1-morphism of algebraic stacks. The functor f_{QCoh,*} and the functors Rⁱf_{QCoh,*} (i ≥ 0) of Stacks 077A commute with direct sums and filtered colimits:

1. f_{QCoh,*} commutes with direct sums indexed by any ι : Type u;
2. f_{QCoh,*} commutes with colimits indexed by any filtered category J : Type u (morphisms in u);
3. for every i, Rⁱf_{QCoh,*} commutes with direct sums indexed by any ι : Type u and with colimits indexed by any filtered category J : Type u.

The functors are quasicoherentDirectImage and quasicoherentHigherDirectImage, the composites Q ∘ f_* ∘ i and Q ∘ Rⁱf_* ∘ i of the inclusion, the direct images of modules on the fppf sites and the coherator of Stacks 0778, at module universe u.

theorem preservesCoproducts_and_filteredColimits_quasicoherentDirectImages_of_qcqs :
    (∀ ι : Type u, PreservesColimitsOfShape (Discrete ι) (quasicoherentDirectImage B S hS f)) ∧
      (∀ (J : Type u) [Category.{u} J] [IsFiltered J],
        PreservesColimitsOfShape J (quasicoherentDirectImage B S hS f)) ∧
      ∀ i : ℕ,
        (∀ ι : Type u,
          PreservesColimitsOfShape (Discrete ι) (quasicoherentHigherDirectImage B S hS f i)) ∧
        (∀ (J : Type u) [Category.{u} J] [IsFiltered J],
          PreservesColimitsOfShape J (quasicoherentHigherDirectImage B S hS f i))

Tag 0GQY, a lemma

Tag 0GQY in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isZero_quasicoherentHigherDirectImage_and_exact_preservesColimits_of_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/AffineQuasicoherentDirectImageExact.lean, line 179. The attribute's comment: “the whole lemma, for an affine 1-morphism f of algebraic stacks and the functors R^i f_{QCoh,} and f_{QCoh,} of Stacks 077A: R^i f_{QCoh,} = 0 for i > 0; f_{QCoh,} is exact (preserves finite limits and finite colimits); it commutes with direct sums; it commutes with all colimits (indexed in the universe u of the site)”.

Stacks 0GQY. Let f : 𝒳 ⟶ 𝒴 be an affine 1-morphism of algebraic stacks. Then

1. the functors Rⁱf_{QCoh,*}, i > 0, vanish;
2. f_{QCoh,*} is exact: it preserves finite limits and finite colimits;
3. f_{QCoh,*} commutes with direct sums (indexed by any ι : Type u);
4. f_{QCoh,*} commutes with all colimits (indexed by categories J : Type u with morphisms in u).

The functors are those of Stacks 077A, quasicoherentHigherDirectImage and quasicoherentDirectImage, at module universe u.

theorem isZero_quasicoherentHigherDirectImage_and_exact_preservesColimits_of_isAffineHom :
    (∀ (i : ℕ), 0 < i → ∀ F : quasicoherentModules B S hS 𝒳,
        IsZero ((quasicoherentHigherDirectImage B S hS f i).obj F)) ∧
      (PreservesFiniteLimits (quasicoherentDirectImage B S hS f) ∧
        PreservesFiniteColimits (quasicoherentDirectImage B S hS f)) ∧
      (∀ ι : Type u, PreservesColimitsOfShape (Discrete ι) (quasicoherentDirectImage B S hS f)) ∧
      PreservesColimitsOfSize.{u, u} (quasicoherentDirectImage B S hS f)

Tag 0GQZ, a lemma

Tag 0GQZ in the Stacks Project.

AlgebraicGeometry.FibredSite.isIso_colimit_post_hom_of_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ColimitsOfHom.lean, line 480. The attribute's comment: “all modules; condition 0GMR (4) for the equi-universe model of the fppf site is a hypothesis, so quasi-compactness, quasi-separatedness and algebraicity of the stack do not appear; finite presentation is Mathlib's, not 03DL's; the index category is small”.

Stacks 0GQZ for all modules. Let 𝒳 be a category fibred in groupoids over the big fppf category of a scheme S contained in a big fppf site, with the fppf topology of Stacks 06TP and the structure sheaf of Stacks 06TV, and assume its total category essentially small. Let 𝒢 be an 𝒪_𝒳-module of finite presentation and D a filtered system of 𝒪_𝒳-modules. Then the canonical comparison

colim_i Hom_𝒳(𝒢, ℱ_i) ⟶ Hom_𝒳(𝒢, colim_i ℱ_i)

is a bijection, granted the hypothesis hX.

hX is the condition of Stacks 0GMR part (4) for the equi-universe model AlgebraicGeometry.FibredSite.fppfModelRingedSite, which is the site Stacks 0GN0 applies to and which the fppf site itself — whose objects lie one universe above its morphisms — is not. It is what the source checks for the objects of the site lying over affine schemes, through Stacks 0GMS case (2), using quasi-compactness and quasi-separatedness of the algebraic stack. Neither of those two hypotheses of the source appears here, and 𝒳 is not assumed to be an algebraic stack: they enter only through hX.

Finite presentation is SheafOfModules.IsFinitePresentation, Mathlib's predicate, which is the one Stacks 0GN0 is stated over; the site predicate SheafOfModules.IsFinitePresentationOnSite of Stacks 03DL used elsewhere in the stacks development is not bridged to it anywhere in the tree. See "What is proved and what is assumed" in the module docstring.

theorem isIso_colimit_post_hom_of_isFinitePresentation (hp : p.IsFiberedInGroupoids)
    (G : SheafOfModules.{u} (ringStructureSheafCore B S hS p hp .fppf))
    (hG : G.IsFinitePresentation)
    {K : Type u} [Category.{u} K] [IsFiltered K]
    (D : K ⥤ SheafOfModules.{u} (ringStructureSheafCore B S hS p hp .fppf))
    (hX : ∃ T : Set (Sheaf (fppfModelRingedSite B S hS p hp).J (Type u)),
      (∀ H : Sheaf (fppfModelRingedSite B S hS p hp).J (Type u),
          Sheaf.IsLocallySurjective (terminal.from H) →
            ∃ L ∈ T, Nonempty (L ⟶ H) ∧ Sheaf.IsLocallySurjective (terminal.from L)) ∧
        ∀ L ∈ T, Sheaf.IsQuasiCompact (L ⨯ L))
    [HasColimit D] [HasColimit (D ⋙ coyoneda.obj (Opposite.op G))] :
    IsIso (colimit.post D (coyoneda.obj (Opposite.op G)))

AlgebraicGeometry.FibredSite.isIso_colimit_post_hom_quasicoherent_of_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ColimitsOfHom.lean, line 509. The attribute's comment: “quasi-coherent modules; condition 0GMR (4) for the equi-universe model of the fppf site and preservation of the colimit by the inclusion of QCoh (the colimit clause of 03M1) are hypotheses, so quasi-compactness, quasi-separatedness and algebraicity of the stack do not appear; finite presentation is Mathlib's, not 03DL's; the index category is small”.

Stacks 0GQZ for quasi-coherent modules. The same comparison, for a filtered colimit taken in the category QCoh(𝒪_𝒳) of Stacks 06WG rather than in all 𝒪_𝒳-modules.

Beyond the hypothesis hX of AlgebraicGeometry.FibredSite.isIso_colimit_post_hom_of_isFinitePresentation this carries one more: that the inclusion of the quasi-coherent modules into all modules preserves colimits of shape K, which is the colimit clause of Stacks 03M1 for the fppf site of 𝒳. That clause is available for an algebraic space only conditionally, in AlgebraicGeometry.Space.isQuasicoherent_colimit_of_h03DX, and is not available for a stack.

theorem isIso_colimit_post_hom_quasicoherent_of_isFinitePresentation
    (hp : p.IsFiberedInGroupoids) (G : quasicoherentModules.{u, u + 1, u, u} B S hS p hp)
    (hG : G.obj.IsFinitePresentation)
    {K : Type u} [Category.{u} K] [IsFiltered K]
    (D : K ⥤ quasicoherentModules.{u, u + 1, u, u} B S hS p hp)
    (hX : ∃ T : Set (Sheaf (fppfModelRingedSite B S hS p hp).J (Type u)),
      (∀ H : Sheaf (fppfModelRingedSite B S hS p hp).J (Type u),
          Sheaf.IsLocallySurjective (terminal.from H) →
            ∃ L ∈ T, Nonempty (L ⟶ H) ∧ Sheaf.IsLocallySurjective (terminal.from L)) ∧
        ∀ L ∈ T, Sheaf.IsQuasiCompact (L ⨯ L))
    [PreservesColimitsOfShape K
      (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
        (ringStructureSheafCore B S hS p hp .fppf)).ι]
    [HasColimit D] [HasColimit (D ⋙ coyoneda.obj (Opposite.op G))] :
    IsIso (colimit.post D (coyoneda.obj (Opposite.op G)))

AlgebraicGeometry.Stack.isIso_colimit_post_hom_of_isQuasiCompactStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ColimitsOfHomQuasiCompactStack.lean, line 452. The attribute's comment: “the displayed colimit equality, for all 𝒪_𝒳-modules”.

Stacks 0GQZ, the displayed equality. Let 𝒳 be a quasi-compact and quasi-separated algebraic stack over a scheme S contained in a big fppf site, with the fppf topology of Stacks 06TP and the structure sheaf of Stacks 06TV. Let 𝒢 be an 𝒪_𝒳-module of finite presentation (Stacks 03DL (7)) and D a filtered system i ↦ ℱ_i of 𝒪_𝒳-modules. Then

colim_i Hom_𝒳(𝒢, ℱ_i) = Hom_𝒳(𝒢, colim_i ℱ_i),

in the form that the canonical comparison map out of the colimit is a bijection. Both colimits exist (AlgebraicGeometry.FibredSite.hasColimitsOfShape_sheafOfModules_ringStructureSheafCore).

Quasi-separatedness is that of Stacks 050D part (8), quasi-separatedness over Spec(ℤ), and no condition is put on S. The index category is a small filtered category, the index set of the source being a set of the ambient universe.

The proof is the source's. The equality is the case of Stacks 0GN0 for the fppf ringed site of 𝒳, applied through its equi-universe model, which is AlgebraicGeometry.FibredSite.preservesColimitsOfShape_coyoneda_fppf_of_isFinitePresentation_model at the site hypothesis of Stacks 0GN0. That hypothesis is discharged by AlgebraicGeometry.Stack.FppfModel.exists_set_isLocallySurjective_and_isQuasiCompact_prod_self through Stacks 0GMS case (2), which is where quasi-compactness and quasi-separatedness are used.

theorem isIso_colimit_post_hom_of_isQuasiCompactStack
    (hqc : IsQuasiCompactStack.{u, w} B S hS 𝒳.val 𝒳.property)
    (h𝒳 : IsQuasiSeparatedAbs.{u, w, w'} B S hS 𝒳)
    (G : _root_.SheafOfModules.{u} (FibredSite.ringStructureSheafCore B S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids .fppf))
    (hG : G.IsFinitePresentationOnSite)
    {K : Type u} [Category.{u} K] [IsFiltered K]
    (D : K ⥤ _root_.SheafOfModules.{u} (FibredSite.ringStructureSheafCore B S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids .fppf)) :
    letI := FibredSite.hasColimitsOfShape_sheafOfModules_ringStructureSheafCore B S hS
      𝒳.val.val.p 𝒳.val.isFiberedInGroupoids .fppf K
    IsIso (colimit.post D (coyoneda.obj (Opposite.op G)))

AlgebraicGeometry.Stack.isIso_colimit_post_hom_quasicoherent_of_isQuasiCompactStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ColimitsOfHomQuasiCompactStack.lean, line 482. The attribute's comment: “the 'in particular' clause: filtered colimits in QCoh(𝒪_𝒳)”.

Stacks 0GQZ, the "in particular" clause. For a quasi-compact and quasi-separated algebraic stack and an 𝒪_𝒳-module 𝒢 of finite presentation, Hom_𝒳(𝒢, -) commutes with filtered colimits taken in the category QCoh(𝒪_𝒳) of Stacks 06WG: for a filtered system D of quasi-coherent modules the comparison map from colim_i Hom_𝒳(𝒢, ℱ_i) to Hom_𝒳(𝒢, colim_i ℱ_i), the colimit taken in QCoh(𝒪_𝒳), is a bijection. Both colimits exist (AlgebraicGeometry.FibredSite.hasColimitsOfSize_quasicoherentModules').

Hom_𝒳(𝒢, -) on QCoh(𝒪_𝒳) is Hom in all modules after the full inclusion, so no quasi-coherence of 𝒢 is asked for. This is not a restatement of the displayed equality: the colimit is the one of QCoh(𝒪_𝒳), and the source's argument is the one used here, that the inclusion of QCoh(𝒪_𝒳) preserves colimits by the colimit clause of Stacks 06WV (4), AlgebraicGeometry.FibredSite.preservesColimitsOfSize_quasicoherentInclusion'.

theorem isIso_colimit_post_hom_quasicoherent_of_isQuasiCompactStack
    (hqc : IsQuasiCompactStack.{u, w} B S hS 𝒳.val 𝒳.property)
    (h𝒳 : IsQuasiSeparatedAbs.{u, w, w'} B S hS 𝒳)
    (G : _root_.SheafOfModules.{u} (FibredSite.ringStructureSheafCore B S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids .fppf))
    (hG : G.IsFinitePresentationOnSite)
    {K : Type u} [Category.{u} K] [IsFiltered K]
    (D : K ⥤ FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids) :
    letI := FibredSite.hasColimitsOfSize_quasicoherentModules' B S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids
    IsIso (colimit.post D ((_root_.SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
      (FibredSite.ringStructureSheafCore B S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids
        .fppf)).ι ⋙ coyoneda.obj (Opposite.op G)))

AlgebraicGeometry.Stack.isIso_colimit_post_hom_and_quasicoherent_of_isQuasiCompactStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ColimitsOfHomQuasiCompactStack.lean, line 519. The attribute's comment: “the whole statement: the displayed colimit equality together with the 'in particular' clause for QCoh(𝒪_𝒳)”.

Stacks 0GQZ in full. For a quasi-compact and quasi-separated algebraic stack 𝒳 (Stacks 04YB, Stacks 050D part (8)) and every small filtered index category K: for every 𝒪_𝒳-module 𝒢 of finite presentation (Stacks 03DL (7)), the displayed equality colim_i Hom_𝒳(𝒢, ℱ_i) = Hom_𝒳(𝒢, colim_i ℱ_i) holds for every system i ↦ ℱ_i of 𝒪_𝒳-modules indexed by K, and Hom_𝒳(𝒢, -) commutes with colimits of shape K taken in QCoh(𝒪_𝒳).

The two conjuncts are AlgebraicGeometry.Stack.isIso_colimit_post_hom_of_isQuasiCompactStack and AlgebraicGeometry.Stack.isIso_colimit_post_hom_quasicoherent_of_isQuasiCompactStack; the colimits involved exist in both module categories.

theorem isIso_colimit_post_hom_and_quasicoherent_of_isQuasiCompactStack
    (hqc : IsQuasiCompactStack.{u, w} B S hS 𝒳.val 𝒳.property)
    (h𝒳 : IsQuasiSeparatedAbs.{u, w, w'} B S hS 𝒳)
    (K : Type u) [Category.{u} K] [IsFiltered K] :
    ∀ (G : _root_.SheafOfModules.{u} (FibredSite.ringStructureSheafCore B S hS 𝒳.val.val.p
        𝒳.val.isFiberedInGroupoids .fppf)),
      G.IsFinitePresentationOnSite →
        (∀ (D : K ⥤ _root_.SheafOfModules.{u} (FibredSite.ringStructureSheafCore B S hS
            𝒳.val.val.p 𝒳.val.isFiberedInGroupoids .fppf)),
          letI := FibredSite.hasColimitsOfShape_sheafOfModules_ringStructureSheafCore B S hS
            𝒳.val.val.p 𝒳.val.isFiberedInGroupoids .fppf K
          IsIso (colimit.post D (coyoneda.obj (Opposite.op G)))) ∧
        ∀ (D : K ⥤ FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS 𝒳.val.val.p
            𝒳.val.isFiberedInGroupoids),
          letI := FibredSite.hasColimitsOfSize_quasicoherentModules' B S hS 𝒳.val.val.p
            𝒳.val.isFiberedInGroupoids
          IsIso (colimit.post D ((_root_.SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
            (FibredSite.ringStructureSheafCore B S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids
              .fppf)).ι ⋙ coyoneda.obj (Opposite.op G)))

Sources

• Section 103.13, Tag 0GQU
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.isIso_colimit_post_rightDerived_globalSections_associatedTopology · AlgebraicGeometry.Stack.isIso_colimit_post_rightDerived_globalSections_fppf · AlgebraicGeometry.Stack.isIso_colimit_post_rightDerived_globalSections_etale · AlgebraicGeometry.Stack.isIso_colimit_post_rightDerived_globalSections_fppf_of_isQuasiCompactStack · AlgebraicGeometry.Stack.isIso_colimit_post_rightDerived_globalSections_etale_of_isQuasiCompactStack · AlgebraicGeometry.Stack.isIso_colimit_post_rightDerived_globalSections_fppf_of_isQuasiCompact_absolute · AlgebraicGeometry.Stack.isIso_colimit_post_rightDerived_globalSections_etale_of_isQuasiCompact_absolute · AlgebraicGeometry.Stack.hasFiniteCoverRefinementsFrom_fppfTopology

Section103.14 The lisse-étale and the flat-fppf sites#

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

Tag 0787, a definition

Tag 0787 in the Stacks Project.

AlgebraicGeometry.Stack.FlatFppf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfSite.lean, line 100. The attribute's comment: “the flat-fppf site: its underlying category of flat objects”.

Stacks 0787, flat_fppf_site. The full subcategory of the flat objects of an algebraic stack over S.

abbrev FlatFppf

AlgebraicGeometry.Stack.FlatFppf.IsCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfSite.lean, line 112. The attribute's comment: “the flat-fppf site: its coverings”.

Stacks 0787, flat_fppf_site. A family of morphisms of flat objects of an algebraic stack covers when its image in the big fppf category of S is a chosen covering family there.

abbrev IsCovering (E : Covering (FlatFppf B S hS 𝒳)) : Prop

AlgebraicGeometry.Stack.FlatFppf.topology, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfSite.lean, line 126. The attribute's comment: “the flat-fppf site: its Grothendieck topology”.

Stacks 0787, flat_fppf_site. The Grothendieck topology of the flat-fppf site: the one generated by the inherited fppf covering families between flat objects.

abbrev topology : GrothendieckTopology (FlatFppf B S hS 𝒳)

AlgebraicGeometry.Stack.LisseEtale, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleSite.lean, line 91. The attribute's comment: “the lisse-etale site: its underlying category of smooth objects”.

The full subcategory of the smooth objects of an algebraic stack over S.

abbrev LisseEtale

AlgebraicGeometry.Stack.LisseEtale.IsCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleSite.lean, line 106. The attribute's comment: “the lisse-etale site: its coverings”.

A family of morphisms of smooth objects of an algebraic stack covers when the family of schemes underneath it is a chosen étale covering family of the big site.

abbrev IsCovering (E : Covering (LisseEtale.{u, w} B S hS 𝒳)) : Prop

AlgebraicGeometry.Stack.LisseEtale.topology, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleSite.lean, line 119. The attribute's comment: “the lisse-etale site: its Grothendieck topology”.

The Grothendieck topology of the lisse-étale site: the one generated by the inherited étale covering families between smooth objects.

abbrev topology : GrothendieckTopology (LisseEtale.{u, w} B S hS 𝒳)

AlgebraicGeometry.Stack.smoothObject_schemeStack_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleSmoothObject.lean, line 132. The attribute's comment: “lisse_etale_site: smooth objects of the stack of a scheme”.

Stacks 0787. An object of the algebraic stack of a scheme U over S — that is, a scheme x over U in the big fppf category — is a smooth object exactly when the morphism of schemes underlying its structure morphism is smooth.

theorem smoothObject_schemeStack_iff (U : BigFppfOver B S hS) (x : Over U) :
    smoothObject.{u, w} B S hS (schemeStack.{u, w} B S hS U) x ↔
      Smooth ((BigFppfOver.toScheme B S hS).map x.hom)

Declarations registered for the tag:

• AlgebraicGeometry.Stack.flatObject, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfSite.lean, line 93 (StacksFrontier): “flat_fppf_site: flat objects”.

Tag 0788, a lemma

Tag 0788 in the Stacks Project.

AlgebraicGeometry.Stack.FlatFppf.isContinuous_inclusion', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfInclusion.lean, line 516. The attribute's comment: “the inclusion of the flat-fppf site is continuous”.

Continuity of the inclusion of the flat-fppf site (Stacks 0788 (2)). This is the fppf case of Stacks 07AK, whose closure hypothesis is AlgebraicGeometry.Stack.FlatFppf.closedUnderFlatMorphisms.

theorem isContinuous_inclusion' :
    (objectProperty B S hS 𝒳).ι.IsContinuous (inclusionTopology B S hS 𝒳)
      (associatedTopology B S hS 𝒳.val.val.p B.topology)

AlgebraicGeometry.Stack.FlatFppf.isCocontinuous_inclusion', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfInclusion.lean, line 523. The attribute's comment: “the inclusion of the flat-fppf site is cocontinuous”.

Cocontinuity of the inclusion of the flat-fppf site (Stacks 0788 (2)).

theorem isCocontinuous_inclusion' :
    (objectProperty B S hS 𝒳).ι.IsCocontinuous (inclusionTopology B S hS 𝒳)
      (associatedTopology B S hS 𝒳.val.val.p B.topology)

AlgebraicGeometry.Stack.FlatFppf.isContinuous_inclusion_topology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfInclusion.lean, line 539. The attribute's comment: “continuity of the inclusion, read at the topologies”.

Continuity of the inclusion of the flat-fppf site, for the chosen-family topology (Stacks 0788 (2)). The same assertion at AlgebraicGeometry.Stack.FlatFppf.topology rather than at AlgebraicGeometry.Stack.FlatFppf.inclusionTopology.

Continuity passes from a topology to any smaller one, because a sheaf for the larger topology is a sheaf for the smaller, so this follows from AlgebraicGeometry.Stack.FlatFppf.isContinuous_inclusion' and AlgebraicGeometry.Stack.FlatFppf.topology_le_inclusionTopology. Cocontinuity does not pass in that direction, which is why the two are recorded differently here.

theorem isContinuous_inclusion_topology :
    (objectProperty B S hS 𝒳).ι.IsContinuous (topology B S hS 𝒳)
      (associatedTopology B S hS 𝒳.val.val.p B.topology)

AlgebraicGeometry.Stack.FlatFppf.isCocontinuous_inclusion_topology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfInclusion.lean, line 554. The attribute's comment: “cocontinuity of the inclusion, read at the topologies”.

Cocontinuity of the inclusion of the flat-fppf site, for the chosen-family topology (Stacks 0788 (2)). The same assertion at AlgebraicGeometry.Stack.FlatFppf.topology rather than at AlgebraicGeometry.Stack.FlatFppf.inclusionTopology.

Unlike continuity, cocontinuity does not transfer from a topology to a smaller one, so this needs the equality AlgebraicGeometry.Stack.FlatFppf.inclusionTopology_eq_topology and not merely AlgebraicGeometry.Stack.FlatFppf.topology_le_inclusionTopology.

theorem isCocontinuous_inclusion_topology :
    (objectProperty B S hS 𝒳).ι.IsCocontinuous (topology B S hS 𝒳)
      (associatedTopology B S hS 𝒳.val.val.p B.topology)

AlgebraicGeometry.Stack.FlatFppf.toposMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfInclusion.lean, line 565. The attribute's comment: “the morphism of topoi induced by the inclusion”.

The morphism of topoi g of Stacks 0788 (2)(a): g : Sh(𝒳_{flat,fppf}) ⟶ Sh(𝒳_{fppf}), with inverse image restriction along the inclusion of the flat objects, pushforward its cocontinuous right adjoint, and left exactness of the inverse image automatic.

noncomputable def toposMorphism :
    MorphismOfTopoi
      (Sheaf (inclusionTopology B S hS 𝒳) (Type (u + 1)))
      (Sheaf (associatedTopology B S hS 𝒳.val.val.p B.topology) (Type (u + 1)))

AlgebraicGeometry.Stack.FlatFppf.toposMorphismTopology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfInclusion.lean, line 585. The attribute's comment: “that morphism of topoi, read at the topologies”.

The morphism of topoi g of Stacks 0788 (2)(a), for the chosen-family topology: the same morphism of topoi as AlgebraicGeometry.Stack.FlatFppf.toposMorphism, transported along AlgebraicGeometry.Stack.FlatFppf.inclusionTopology_eq_topology, so that its source is the topos of sheaves for AlgebraicGeometry.Stack.FlatFppf.topology. No second construction is involved: the two topologies are equal, and this is the one morphism of topoi read at the other description.

noncomputable def toposMorphismTopology :
    MorphismOfTopoi
      (Sheaf (topology B S hS 𝒳) (Type (u + 1)))
      (Sheaf (associatedTopology B S hS 𝒳.val.val.p B.topology) (Type (u + 1)))

AlgebraicGeometry.Stack.FlatFppf.setsShriekAdjunction, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfInclusion.lean, line 620. The attribute's comment: “the lower-shriek adjunction on sheaves of sets”.

Stacks 0788 (2)(b). The inverse image of the morphism of topoi g of Stacks 0788 (2)(a) has a left adjoint on sheaves of sets, namely AlgebraicGeometry.Stack.FlatFppf.setsShriek.

This is CategoryTheory.Functor.sheafAdjunctionLowerShriek (Stacks 00XR (2)) at the inclusion of the flat objects, whose continuity is AlgebraicGeometry.Stack.FlatFppf.isContinuous_inclusion_topology. The right-hand side is the inverse image of AlgebraicGeometry.Stack.FlatFppf.toposMorphismTopology, restriction along the inclusion.

noncomputable abbrev setsShriekAdjunction :
    setsShriek B S hS 𝒳 ⊣
      (objectProperty B S hS 𝒳).ι.sheafPushforwardContinuous (Type (u + 1))
        (topology B S hS 𝒳) (associatedTopology B S hS 𝒳.val.val.p B.topology)

AlgebraicGeometry.Stack.FlatFppf.isIso_setsShriekAdjunction_unit, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfInclusion.lean, line 633. The attribute's comment: “the unit of the sets lower-shriek adjunction is invertible”.

Stacks 0788 (2)(c), the half about g_!. The canonical map F ⟶ g⁻¹g_!F on sheaves of sets — the unit of AlgebraicGeometry.Stack.FlatFppf.setsShriekAdjunction — is an isomorphism.

This is Stacks 00XT for a fully faithful, continuous and cocontinuous functor of sites, all three of which hold for the inclusion of the flat objects at this topology.

instance isIso_setsShriekAdjunction_unit : IsIso (setsShriekAdjunction B S hS 𝒳).unit

AlgebraicGeometry.Stack.FlatFppf.abelianShriekAdjunction, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfInclusion.lean, line 706. The attribute's comment: “the lower-shriek adjunction on abelian sheaves”.

Stacks 0788 (2)(d). Restriction of abelian sheaves along the inclusion of the flat objects has a left adjoint, namely AlgebraicGeometry.Stack.FlatFppf.abelianShriek.

noncomputable abbrev abelianShriekAdjunction :
    abelianShriek.{u, w, v} B S hS 𝒳 ⊣
      (objectProperty B S hS 𝒳).ι.sheafPushforwardContinuous Ab.{max u v}
        (topology B S hS 𝒳) (associatedTopology B S hS 𝒳.val.val.p B.topology)

AlgebraicGeometry.Stack.FlatFppf.isIso_abelianShriekAdjunction_unit, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfInclusion.lean, line 728. The attribute's comment: “the unit of the abelian lower-shriek adjunction is invertible”.

Stacks 0788 (2)(e): the canonical map F ⟶ g⁻¹g_!F on abelian sheaves — the unit of AlgebraicGeometry.Stack.FlatFppf.abelianShriekAdjunction — is an isomorphism. This is Stacks 00XT again, now at abelian coefficients.

instance isIso_abelianShriekAdjunction_unit :
    IsIso (abelianShriekAdjunction.{u, w, v} B S hS 𝒳).unit

AlgebraicGeometry.Stack.FlatFppf.structureSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfRinged.lean, line 193. The attribute's comment: “the structure sheaf of the flat-fppf site”.

Stacks 0788, flat_ringed. The structure sheaf of the flat-fppf site of an algebraic stack: the restriction, along the inclusion of the flat objects, of the structure sheaf of its fppf site. The rings of sections are unchanged — they are those of the fppf structure sheaf at the flat objects.

noncomputable def structureSheaf : Sheaf (topology B S hS 𝒳) CommRingCat.{u}

AlgebraicGeometry.Stack.FlatFppf.structureSheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfRinged.lean, line 252. The attribute's comment: “the structure sheaf is the restriction of the big one”.

Stacks 0788, flat_ringed: g⁻¹𝒪_𝒳 ≅ 𝒪_{𝒳_{flat,fppf}}. The inverse image of the fppf structure sheaf along the morphism of topoi of Stacks 0788 (2)(a) is the structure sheaf of the flat-fppf site.

The inverse image of g on sheaves of sets is restriction along the inclusion of the flat objects, so this is the comparison of the transported commutative ring operations with those of the restricted sheaf, and that comparison is the identity on sections (AlgebraicGeometry.Stack.FlatFppf.structureSheafIso_apply).

noncomputable def structureSheafIso :
    (inverseImageCommRingFunctor (toposMorphismOnRings B S hS 𝒳)).obj
        (fppfRingedTopos B S hS 𝒳).O ≅ (ringedTopos B S hS 𝒳).O

AlgebraicGeometry.Stack.FlatFppf.structureSheafIso_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfRinged.lean, line 263. The attribute's comment: “that identification, on sections”.

Stacks 0788, flat_ringed. The identification g⁻¹𝒪_𝒳 ≅ 𝒪_{𝒳_{flat,fppf}} is the identity on sections over a flat object. This pins it: it is not an arbitrary automorphism of the restricted structure sheaf.

theorem structureSheafIso_apply (U : (FlatFppf B S hS 𝒳)ᵒᵖ)
    (a : ((inverseImageCommRingFunctor (toposMorphismOnRings B S hS 𝒳)).obj
      (fppfRingedTopos B S hS 𝒳).O).obj.obj U) :
    (structureSheafIso B S hS 𝒳).hom.hom.app U a = a

AlgebraicGeometry.Stack.FlatFppf.ringedToposMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfRinged.lean, line 273. The attribute's comment: “the induced morphism of ringed topoi”.

Stacks 0788, flat_ringed. The morphism of ringed topoi (g, g♯) : (Sh(𝒳_{flat,fppf}), 𝒪_{𝒳_{flat,fppf}}) ⟶ (Sh(𝒳_{fppf}), 𝒪_𝒳) of Stacks 01D3 part (2), whose structure map is the adjoint of the identification AlgebraicGeometry.Stack.FlatFppf.structureSheafIso.

noncomputable def ringedToposMorphism :
    RingedToposHom (ringedTopos B S hS 𝒳) (fppfRingedTopos B S hS 𝒳)

AlgebraicGeometry.Stack.FlatFppf.ringedToposMorphism_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfRinged.lean, line 291. The attribute's comment: “that morphism of ringed topoi is flat”.

Stacks 0788, flat_ringed. The flat-fppf morphism of ringed topoi is flat, in the sense of Stacks 04JB: its inverse-image structure map is an isomorphism, by AlgebraicGeometry.Stack.FlatFppf.ringedToposMorphism_fSharpInverseImage, and an isomorphism of sheaves of commutative rings is a flat morphism.

theorem ringedToposMorphism_isFlat : (ringedToposMorphism B S hS 𝒳).IsFlat

AlgebraicGeometry.Stack.FlatFppf.moduleRestriction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfRinged.lean, line 315. The attribute's comment: “restriction of modules along it”.

Stacks 0788, flat_ringed. Restriction of sheaves of modules along the inclusion of the flat objects, over the fppf structure sheaf and its restriction. The scalar comparison is the identity, because the structure sheaf of the flat-fppf site is the restriction of the fppf one with its original rings of sections.

This is the functor that the third assertion of Stacks 0788 (2)(f) identifies pullback of modules along AlgebraicGeometry.Stack.FlatFppf.ringedToposMorphism with; the identification is AlgebraicGeometry.Stack.FlatFppf.modulePullbackIso, in StacksFrontier.AlgebraicGeometry.Stacks.FlatFppfRingedModules.

noncomputable def moduleRestriction :
    SheafOfModules.{u}
        (Stacks.SheafOfModules.Tensor.ringSheaf.{u + 1, u, u}
          (ambientStructureSheaf B S hS 𝒳)) ⥤
      SheafOfModules.{u}
        (Stacks.SheafOfModules.Tensor.ringSheaf.{u + 1, u, u}
          (structureSheaf B S hS 𝒳))

AlgebraicGeometry.Stack.FlatFppf.modulePullbackIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfRingedModules.lean, line 108. The attribute's comment: “pullback of modules along it, as an identification”.

Pullback of sheaves of modules along the flat-fppf morphism of ringed topoi is restriction of sheaves of modules along the inclusion of the flat objects, over the fppf structure sheaf and its restriction.

noncomputable def modulePullbackIso :
    Stacks.Sheaves.RingedToposModules.RingedToposHom.pullbackModules.{u, u, u, u + 1, u, u + 1}
        (ringedToposModulesHom B S hS 𝒳) ≅
      moduleRestriction B S hS 𝒳

AlgebraicGeometry.Stack.LisseEtale.modulePullbackIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleRingedModules.lean, line 256. The attribute's comment: “part (1)(f): pullback of modules along it is restriction of modules”.

Stacks 0788, part (1)(f), third assertion: g^{-1} = g^*. Pullback of sheaves of modules along the lisse-étale morphism of ringed topoi AlgebraicGeometry.Stack.LisseEtale.ringedToposMorphism' is restriction of sheaves of modules along the inclusion of the smooth objects, over the étale structure sheaf of Stacks 06TV and its restriction. No hypothesis is carried: this is AlgebraicGeometry.Stack.subsiteModulePullbackIso at P = AlgebraicGeometry.Stack.smoothObject and the étale topology, where the two locality hypotheses hold for every algebraic stack.

noncomputable def modulePullbackIso :
    Stacks.Sheaves.RingedToposModules.RingedToposHom.pullbackModules.{u, u, u, u + 1, u, u + 1}
        (subsiteRingedToposModulesHom B S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids
          (etaleTopology B) (etaleTopology_le_topology B) (smoothObject.{u, t} B S hS 𝒳)) ≅
      subsiteRingedToposModuleRestriction B S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids
        (etaleTopology B) (etaleTopology_le_topology B) (smoothObject.{u, t} B S hS 𝒳)

AlgebraicGeometry.Stack.LisseEtale.isContinuous_inclusion', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleSmoothClosure.lean, line 229. The attribute's comment: “the inclusion of the lisse-etale site is continuous”.

Stacks 0788, part (1): continuity of the inclusion of the lisse-étale site. The étale case of Stacks 07AK at the chosen étale precoverage of Stacks 03FF, with the closure condition of 07AK (1) discharged.

theorem isContinuous_inclusion' :
    (smoothObject.{u, w} B S hS 𝒳).ι.IsContinuous (inclusionTopology.{u, w} B S hS 𝒳)
      (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))

AlgebraicGeometry.Stack.LisseEtale.isCocontinuous_inclusion', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleSmoothClosure.lean, line 236. The attribute's comment: “the inclusion of the lisse-etale site is cocontinuous”.

Stacks 0788, part (1): cocontinuity of the inclusion of the lisse-étale site.

theorem isCocontinuous_inclusion' :
    (smoothObject.{u, w} B S hS 𝒳).ι.IsCocontinuous (inclusionTopology.{u, w} B S hS 𝒳)
      (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))

AlgebraicGeometry.Stack.LisseEtale.isContinuous_inclusion_topology', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleSmoothClosure.lean, line 246. The attribute's comment: “continuity of that inclusion, read at the topologies”.

Stacks 0788, part (1): continuity of the inclusion of the lisse-étale site, for the chosen-family topology. The same assertion at AlgebraicGeometry.Stack.LisseEtale.topology, which is the description Stacks 0787 is recorded at.

theorem isContinuous_inclusion_topology' :
    (smoothObject.{u, w} B S hS 𝒳).ι.IsContinuous (topology.{u, w} B S hS 𝒳)
      (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))

AlgebraicGeometry.Stack.LisseEtale.isCocontinuous_inclusion_topology', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleSmoothClosure.lean, line 254. The attribute's comment: “cocontinuity of that inclusion, read at the topologies”.

Stacks 0788, part (1): cocontinuity of the inclusion of the lisse-étale site, for the chosen-family topology.

theorem isCocontinuous_inclusion_topology' :
    (smoothObject.{u, w} B S hS 𝒳).ι.IsCocontinuous (topology.{u, w} B S hS 𝒳)
      (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))

AlgebraicGeometry.Stack.LisseEtale.toposMorphism', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleSmoothClosure.lean, line 264. The attribute's comment: “the morphism of topoi induced by the lisse-etale inclusion”.

The morphism of topoi of Stacks 0788 (1)(a): g : Sh(𝒳_{lisse,étale}) ⟶ Sh(𝒳_étale), with inverse image restriction along the inclusion of the smooth objects. This is AlgebraicGeometry.Stack.LisseEtale.toposMorphism with its hypothesis discharged.

noncomputable def toposMorphism' :
    MorphismOfTopoi
      (Sheaf (inclusionTopology.{u, w} B S hS 𝒳) (Type (u + 1)))
      (Sheaf (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B)) (Type (u + 1)))

AlgebraicGeometry.Stack.LisseEtale.toposMorphismTopology', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleSmoothClosure.lean, line 273. The attribute's comment: “the lisse-etale morphism of topoi, read at the topologies”.

The morphism of topoi of Stacks 0788 (1)(a), for the chosen-family topology: the same morphism of topoi read at AlgebraicGeometry.Stack.LisseEtale.topology.

noncomputable def toposMorphismTopology' :
    MorphismOfTopoi
      (Sheaf (topology.{u, w} B S hS 𝒳) (Type (u + 1)))
      (Sheaf (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B)) (Type (u + 1)))

AlgebraicGeometry.Stack.LisseEtale.setsShriekAdjunction, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleSmoothClosure.lean, line 311. The attribute's comment: “part (1)(b): the lower-shriek adjunction on sheaves of sets”.

Stacks 0788, part (1)(b). The inverse image of the morphism of topoi g of Stacks 0788 (1)(a) has a left adjoint on sheaves of sets, namely AlgebraicGeometry.Stack.LisseEtale.setsShriek.

This is CategoryTheory.Functor.sheafAdjunctionLowerShriek (Stacks 00XR (2)) at the inclusion of the smooth objects, whose continuity is AlgebraicGeometry.Stack.LisseEtale.isContinuous_inclusion_topology'. The right-hand side is the inverse image of AlgebraicGeometry.Stack.LisseEtale.toposMorphismTopology', restriction along the inclusion.

noncomputable abbrev setsShriekAdjunction :
    setsShriek.{u, w} B S hS 𝒳 ⊣
      (smoothObject.{u, w} B S hS 𝒳).ι.sheafPushforwardContinuous (Type (u + 1))
        (topology.{u, w} B S hS 𝒳)
        (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))

AlgebraicGeometry.Stack.LisseEtale.isIso_setsShriekAdjunction_unit, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleSmoothClosure.lean, line 326. The attribute's comment: “part (1)(c): the unit of the sets lower-shriek adjunction is invertible”.

Stacks 0788, part (1)(c), the half about g_!^{Sh}. The canonical map F ⟶ g⁻¹g_!F on sheaves of sets — the unit of AlgebraicGeometry.Stack.LisseEtale.setsShriekAdjunction — is an isomorphism.

This is Stacks 00XT for a fully faithful, continuous and cocontinuous functor of sites, all three of which hold for the inclusion of the smooth objects at this topology.

instance isIso_setsShriekAdjunction_unit : IsIso (setsShriekAdjunction.{u, w} B S hS 𝒳).unit

AlgebraicGeometry.Stack.LisseEtale.abelianLowerShriekAdjunction', an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleSmoothClosure.lean, line 342. The attribute's comment: “part (1)(d): the lower-shriek adjunction on abelian sheaves”.

The adjunction g_! ⊣ g⁻¹ of Stacks 0788 (1)(d) on abelian sheaves, with no hypothesis: AlgebraicGeometry.Stack.LisseEtale.abelianLowerShriekAdjunction with its closure property discharged.

noncomputable abbrev abelianLowerShriekAdjunction' :
    abelianLowerShriek.{u, w} B S hS 𝒳 (closedUnderSmoothMorphisms B S hS 𝒳) ⊣
      abelianInverseImage.{u, w} B S hS 𝒳 (closedUnderSmoothMorphisms B S hS 𝒳)

AlgebraicGeometry.Stack.LisseEtale.isIso_abelianLowerShriek_unit', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleSmoothClosure.lean, line 352. The attribute's comment: “part (1)(e): the unit of the abelian lower-shriek adjunction is invertible”.

Stacks 0788, part (1)(e), with no hypothesis: the canonical map F ⟶ g⁻¹(g_!F) on abelian sheaves — the unit of AlgebraicGeometry.Stack.LisseEtale.abelianLowerShriekAdjunction' — is an isomorphism. This is Stacks 077I, whose three hypotheses on the inclusion of the smooth objects are full faithfulness, isContinuous_inclusion' and isCocontinuous_inclusion'.

theorem isIso_abelianLowerShriek_unit'
    (F : Sheaf (inclusionTopology.{u, w} B S hS 𝒳) AbCat.{u, u + 1}) :
    IsIso ((abelianLowerShriekAdjunction'.{u, w} B S hS 𝒳).unit.app F)

AlgebraicGeometry.Stack.LisseEtale.structureSheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleSmoothClosure.lean, line 393. The attribute's comment: “part (1)(f): the inverse image of the structure sheaf is the lisse-etale structure sheaf”.

Stacks 0788, part (1)(f), first assertion: g⁻¹𝒪_𝒳 = 𝒪_{𝒳_{lisse,étale}}. The inverse image of the étale structure sheaf of Stacks 06TV along the morphism of topoi of Stacks 0788 (1)(a) is the structure sheaf of the lisse-étale site.

The inverse image of g on sheaves of sets is restriction along the inclusion of the smooth objects, so this is the comparison of the transported commutative ring operations with those of the restricted sheaf, and that comparison is the identity on sections (AlgebraicGeometry.Stack.LisseEtale.structureSheafIso_apply).

noncomputable def structureSheafIso :
    (inverseImageCommRingFunctor (toposMorphismOnRings.{u, w} B S hS 𝒳)).obj
        (etaleRingedTopos.{u, w} B S hS 𝒳).O ≅ (ringedTopos'.{u, w} B S hS 𝒳).O

AlgebraicGeometry.Stack.LisseEtale.structureSheafIso_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleSmoothClosure.lean, line 403. The attribute's comment: “part (1)(f): that identification, on sections”.

Stacks 0788, part (1)(f). The identification g⁻¹𝒪_𝒳 ≅ 𝒪_{𝒳_{lisse,étale}} is the identity on sections over a smooth object. This pins it: it is not an arbitrary automorphism of the restricted structure sheaf.

theorem structureSheafIso_apply (U : (LisseEtale.{u, w} B S hS 𝒳)ᵒᵖ)
    (a : ((inverseImageCommRingFunctor (toposMorphismOnRings.{u, w} B S hS 𝒳)).obj
      (etaleRingedTopos.{u, w} B S hS 𝒳).O).obj.obj U) :
    (structureSheafIso.{u, w} B S hS 𝒳).hom.hom.app U a = a

AlgebraicGeometry.Stack.LisseEtale.ringedToposMorphism', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleSmoothClosure.lean, line 416. The attribute's comment: “part (1)(f): the induced morphism of ringed topoi”.

The morphism of ringed topoi of Stacks 0788 (1)(f), with no hypothesis: (g, g♯) : (Sh(𝒳_{lisse,étale}), 𝒪_{𝒳_{lisse,étale}}) ⟶ (Sh(𝒳_étale), 𝒪_𝒳), whose structure map is the adjoint of AlgebraicGeometry.Stack.LisseEtale.structureSheafIso. This is AlgebraicGeometry.Stack.LisseEtale.ringedToposMorphism with its closure property discharged.

noncomputable def ringedToposMorphism' :
    RingedToposHom (ringedTopos'.{u, w} B S hS 𝒳) (etaleRingedTopos.{u, w} B S hS 𝒳)

AlgebraicGeometry.Stack.LisseEtale.isFlat_ringedToposMorphism', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleSmoothClosure.lean, line 424. The attribute's comment: “part (1)(f): that morphism of ringed topoi is flat”.

Stacks 0788, part (1)(f), second assertion, with no hypothesis: the lisse-étale morphism of ringed topoi is flat in the sense of Stacks 04JB, its inverse-image structure map being the isomorphism AlgebraicGeometry.Stack.LisseEtale.structureSheafIso.

theorem isFlat_ringedToposMorphism' :
    RingedToposHom.IsFlat
      (X := ringedTopos'.{u, w} B S hS 𝒳) (Y := etaleRingedTopos.{u, w} B S hS 𝒳)
      (ringedToposMorphism'.{u, w} B S hS 𝒳)

CategoryTheory.Functor.isIso_sheafAdjunctionCocontinuous_counit, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Continuous.lean, line 204. The attribute's comment: “(1)(c) and (2)(c): the counit of the cocontinuous sheaf adjunction is invertible”. References: SGA 4 III (2.6), “u ff ⇒ u_* ff”; SGA 4 IV (4.10.5), “more general”.

If u : C ⥤ D is cocontinuous, continuous and fully faithful, the counit g^{-1}g_*F ⟶ F of g^{-1} ⊣ g_* is an isomorphism; equivalently g_* is fully faithful.

public instance isIso_sheafAdjunctionCocontinuous_counit
    {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] (u : C ⥤ D)
    (A : Type w) [Category.{w'} A]
    (J : GrothendieckTopology C) (K : GrothendieckTopology D)
    [u.IsCocontinuous J K] [u.IsContinuous J K] [u.Full] [u.Faithful]
    [∀ F : Cᵒᵖ ⥤ A, u.op.HasPointwiseRightKanExtension F] :
    IsIso (u.sheafAdjunctionCocontinuous A J K).counit

Declarations registered for the tag:

• CategoryTheory.ObjectProperty.fullyFaithfulι registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfInclusion.lean, line 820 (StacksFrontier): “flat_inclusion”. References: SGA 3 I (1.1.1), “Hom_C(X,Y) = Hom_D(X,Y)”; SGA 6 II (3.0), “more general”.
• CategoryTheory.ObjectProperty.fullyFaithfulι registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleSmoothClosure.lean, line 436 (StacksFrontier): “lisse_inclusion”. References: SGA 3 I (1.1.1), “Hom_C(X,Y) = Hom_D(X,Y)”; SGA 6 II (3.0), “more general”.
• CategoryTheory.Functor.sheafPullbackConstruction.sheafPullback registered with add_to_stacks in StacksFrontier/Exercises/NonExercises/LisseEtaleLowerShriek.lean, line 25 (StacksFrontier): “lisse_sets_shriek”.
• CategoryTheory.Functor.sheafAdjunctionLowerShriek, declared in the repository, registered with add_to_stacks in StacksFrontier/Exercises/NonExercises/LisseEtaleLowerShriek.lean, line 27 (StacksFrontier): “lisse_sets_shriek”.

Tag 0GR0, a lemma

Tag 0GR0 in the Stacks Project.

AlgebraicGeometry.Stack.FlatFppf.cohomologyOverObjectIso', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteAcyclicity.lean, line 284. The attribute's comment: “part (2)(b), cohomology over a flat object”.

Stacks 0GR0, part (2)(b). For an algebraic stack 𝒳, an abelian sheaf F on the fppf site of 𝒳 and a flat object x of 𝒳,

H^q(x, F) = H^q(𝒳_{flat,fppf}/x, g⁻¹ F),

naturally in F, where g⁻¹ is restriction to the flat-fppf site of Stacks 0787 and cohomology over an object is the global cohomology on the slice site.

This is AlgebraicGeometry.Stack.FlatFppf.cohomologyOverObjectIso with its acyclicity hypothesis discharged by AlgebraicGeometry.Stack.FlatFppf.sliceAcyclic.

def cohomologyOverObjectIso'
    (x : ObjectProperty.FullSubcategory (objectProperty B S hS 𝒳)) (q : ℕ) :
    haveI := isContinuous_inclusion B S hS 𝒳 (closedUnderFlatMorphisms B S hS 𝒳)
    haveI := Functor.isContinuous_overPost (inclusionTopology B S hS 𝒳)
      (fppfTopology B S hS 𝒳) (objectProperty B S hS 𝒳).ι x
    (objectProperty B S hS 𝒳).ι.sheafPushforwardContinuous AddCommGrpCat.{u + 1}
          (inclusionTopology B S hS 𝒳) (fppfTopology B S hS 𝒳) ⋙
        (inclusionTopology B S hS 𝒳).overPullback AddCommGrpCat.{u + 1} x ⋙
          Sheaf.functorH ((inclusionTopology B S hS 𝒳).over x) q ≅
      (fppfTopology B S hS 𝒳).overPullback AddCommGrpCat.{u + 1}
            ((objectProperty B S hS 𝒳).ι.obj x) ⋙
        Sheaf.functorH ((fppfTopology B S hS 𝒳).over
          ((objectProperty B S hS 𝒳).ι.obj x)) q

AlgebraicGeometry.Stack.LisseEtale.cohomologyOverObjectIso', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteAcyclicity.lean, line 351. The attribute's comment: “part (1)(b), cohomology over a smooth object”.

Stacks 0GR0, part (1)(b). For an algebraic stack 𝒳, an abelian sheaf F on the étale site of 𝒳 and a smooth object x of 𝒳,

H^q(x, F) = H^q(𝒳_{lisse,étale}/x, g⁻¹ F),

naturally in F, where g⁻¹ is restriction to the lisse-étale site of Stacks 0787.

This is AlgebraicGeometry.Stack.LisseEtale.cohomologyOverObjectIso with its acyclicity hypothesis discharged by AlgebraicGeometry.Stack.LisseEtale.sliceAcyclic.

def cohomologyOverObjectIso'
    (x : ObjectProperty.FullSubcategory (smoothObject.{u, w} B S hS 𝒳)) (q : ℕ) :
    haveI := isContinuous_inclusion B S hS 𝒳 (closedUnderSmoothMorphisms.{u, w} B S hS 𝒳)
    haveI := Functor.isContinuous_overPost (inclusionTopology.{u, w} B S hS 𝒳)
      (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
      (smoothObject.{u, w} B S hS 𝒳).ι x
    (smoothObject.{u, w} B S hS 𝒳).ι.sheafPushforwardContinuous AddCommGrpCat.{u + 1}
          (inclusionTopology.{u, w} B S hS 𝒳)
          (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B)) ⋙
        (inclusionTopology.{u, w} B S hS 𝒳).overPullback AddCommGrpCat.{u + 1} x ⋙
          Sheaf.functorH ((inclusionTopology.{u, w} B S hS 𝒳).over x) q ≅
      (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B)).overPullback
            AddCommGrpCat.{u + 1} ((smoothObject.{u, w} B S hS 𝒳).ι.obj x) ⋙
        Sheaf.functorH ((associatedTopology B S hS 𝒳.val.val.p (etaleTopology B)).over
          ((smoothObject.{u, w} B S hS 𝒳).ι.obj x)) q

AlgebraicGeometry.Stack.LisseEtale.globalCohomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteGlobalCohomologyAtlas.lean, line 159. The attribute's comment: “part (1)(a), global cohomology on the lisse-étale site”.

Stacks 0GR0, part (1)(a). For an algebraic stack 𝒳, every degree q and every abelian sheaf ℱ on the étale site of 𝒳,

H^q(𝒳_{lisse,étale}, g⁻¹ℱ) ≅ H^q(𝒳_étale, ℱ),

naturally in ℱ, where g⁻¹ is restriction to the lisse-étale site of Stacks 0787 — the inverse image of the morphism of topoi of Stacks 0788, by AlgebraicGeometry.Stack.inclusionToposMorphism_inverseImageIso.

This is Stacks 07AK, AlgebraicGeometry.Stack.subsiteCohomologyIsoOfAtlas, for the inclusion of the smooth objects, with both its hypotheses discharged: AlgebraicGeometry.Stack.LisseEtale.isClosedUnderSitePullback and AlgebraicGeometry.Stack.LisseEtale.exists_atlas.

def globalCohomologyIso (q : ℕ) :
    subsiteRestriction B S hS 𝒳.val.val.p (etaleTopology B) (smoothObject.{u, w} B S hS 𝒳) ⋙
        Sheaf.functorH.{u + 1, u + 1, u, u + 1} (inclusionTopology.{u, w} B S hS 𝒳) q ≅
      Sheaf.functorH.{u + 1, u + 1, u, u + 1}
        (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B)) q

AlgebraicGeometry.Stack.FlatFppf.globalCohomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteGlobalCohomologyAtlas.lean, line 209. The attribute's comment: “part (2)(a), global cohomology on the flat-fppf site”.

Stacks 0GR0, part (2)(a). For an algebraic stack 𝒳, every degree q and every abelian sheaf ℱ on the fppf site of 𝒳,

H^q(𝒳_{flat,fppf}, g⁻¹ℱ) ≅ H^q(𝒳_fppf, ℱ),

naturally in ℱ, where g⁻¹ is restriction to the flat-fppf site of Stacks 0787 — the inverse image of the morphism of topoi of Stacks 0788, by AlgebraicGeometry.Stack.inclusionToposMorphism_inverseImageIso.

This is Stacks 07AK, AlgebraicGeometry.Stack.subsiteCohomologyIsoOfAtlas, for the inclusion of the flat objects, with both its hypotheses discharged: AlgebraicGeometry.Stack.FlatFppf.isClosedUnderSitePullback and AlgebraicGeometry.Stack.FlatFppf.exists_atlas.

def globalCohomologyIso (q : ℕ) :
    subsiteRestriction B S hS 𝒳.val.val.p B.topology (objectProperty B S hS 𝒳) ⋙
        Sheaf.functorH.{u + 1, u + 1, u, u + 1} (inclusionTopology B S hS 𝒳) q ≅
      Sheaf.functorH.{u + 1, u + 1, u, u + 1} (fppfTopology B S hS 𝒳) q

AlgebraicGeometry.Stack.LisseEtale.globalModuleCohomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteGlobalModuleCohomologyAtlas.lean, line 89. The attribute's comment: “part (1)(a), sheaves of modules”.

Stacks 0GR0, part (1)(a), for sheaves of modules. For an algebraic stack 𝒳, every degree q and every sheaf ℱ of 𝒪_𝒳-modules on the étale site of 𝒳,

H^q(𝒳_{lisse,étale}, g^*ℱ) ≅ H^q(𝒳_étale, ℱ),

naturally in ℱ, where g^* is restriction of sheaves of modules to the lisse-étale site of Stacks 0787, over the restriction of 𝒪_𝒳, and H^q of a sheaf of modules is Ext^q out of the structure sheaf.

It is the abelian comparison, Stacks 07AK at the coefficients of the modules (AlgebraicGeometry.Stack.subsiteCohomologyIsoOfAtlasOfLe, with the hypotheses of AlgebraicGeometry.Stack.LisseEtale.globalCohomologyIso), read through Stacks 03FD, Stacks.Cohomology.ModuleAbelianComparison.moduleFunctorHIso, on both sites.

def globalModuleCohomologyIso (q : ℕ) :
    subsiteModuleRestriction.{u, u + 1, u, t} B S hS 𝒳.val.val.p (etaleTopology B)
          (smoothObject.{u, w} B S hS 𝒳) (etaleStructureRing.{u, w, t} B S hS 𝒳) ⋙
        moduleFunctorH.{t, u, u + 1} (inclusionTopology.{u, w} B S hS 𝒳)
          (subsiteRing.{u, u + 1, u, t} B S hS 𝒳.val.val.p (etaleTopology B)
            (smoothObject.{u, w} B S hS 𝒳) (etaleStructureRing.{u, w, t} B S hS 𝒳)) q ≅
      moduleFunctorH.{t, u, u + 1} (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
        (etaleStructureRing.{u, w, t} B S hS 𝒳) q

AlgebraicGeometry.Stack.FlatFppf.globalModuleCohomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteGlobalModuleCohomologyAtlas.lean, line 140. The attribute's comment: “part (2)(a), sheaves of modules”.

Stacks 0GR0, part (2)(a), for sheaves of modules. For an algebraic stack 𝒳, every degree q and every sheaf ℱ of 𝒪_𝒳-modules on the fppf site of 𝒳,

H^q(𝒳_{flat,fppf}, g^*ℱ) ≅ H^q(𝒳_fppf, ℱ),

naturally in ℱ, where g^* is restriction of sheaves of modules to the flat-fppf site of Stacks 0787, over the restriction of 𝒪_𝒳, and H^q of a sheaf of modules is Ext^q out of the structure sheaf.

It is the abelian comparison, Stacks 07AK at the coefficients of the modules (AlgebraicGeometry.Stack.subsiteCohomologyIsoOfAtlasOfLe, with the hypotheses of AlgebraicGeometry.Stack.FlatFppf.globalCohomologyIso), read through Stacks 03FD, Stacks.Cohomology.ModuleAbelianComparison.moduleFunctorHIso, on both sites.

def globalModuleCohomologyIso (q : ℕ) :
    subsiteModuleRestriction.{u, u + 1, u, t} B S hS 𝒳.val.val.p B.topology
          (objectProperty B S hS 𝒳) (fppfStructureRing.{u, w, t} B S hS 𝒳) ⋙
        moduleFunctorH.{t, u, u + 1} (inclusionTopology B S hS 𝒳)
          (subsiteRing.{u, u + 1, u, t} B S hS 𝒳.val.val.p B.topology
            (objectProperty B S hS 𝒳) (fppfStructureRing.{u, w, t} B S hS 𝒳)) q ≅
      moduleFunctorH.{t, u, u + 1} (fppfTopology B S hS 𝒳)
        (fppfStructureRing.{u, w, t} B S hS 𝒳) q

AlgebraicGeometry.Stack.FlatFppf.cohomologyOverObjectIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteObjectwiseCohomology.lean, line 336. The attribute's comment: “part (2)(b), cohomology over a flat object; conditional on the acyclicity statement of 0D6X only”.

Stacks 0GR0, part (2)(b). For an algebraic stack 𝒳, an abelian sheaf F on the fppf site of 𝒳 and a flat object x of 𝒳,

H^q(x, F) = H^q(𝒳_{flat,fppf}/x, g⁻¹ F),

naturally in F, where g⁻¹ is restriction to the flat-fppf site of Stacks 0787 and cohomology over an object is the global cohomology on the slice site.

The closure condition of Stacks 07AK (1) is discharged — it holds for every algebraic stack, by AlgebraicGeometry.Stack.FlatFppf.closedUnderFlatMorphisms — so the inclusion of the flat objects is continuous and cocontinuous with no hypothesis. What remains open is the acyclicity statement of Stacks 0D6X for the slice at x, carried here as the hypothesis hacyclic: see the module docstring for why the library's form of 0D6X does not apply at these universes.

def cohomologyOverObjectIso
    (x : ObjectProperty.FullSubcategory (objectProperty B S hS 𝒴))
    (hacyclic : haveI := isContinuous_inclusion B S hS 𝒴 flatClosure
      ∀ I : Sheaf ((fppfTopology B S hS 𝒴).over ((objectProperty B S hS 𝒴).ι.obj x))
          AddCommGrpCat.{u + 1}, Injective I → ∀ (n : ℕ)
        (a : Sheaf.H ((subsiteSliceRestriction B S hS 𝒴.val.val.p B.topology
          (objectProperty B S hS 𝒴) x).obj I) (n + 1)), a = 0)
    (q : ℕ) :
    haveI := isContinuous_inclusion B S hS 𝒴 flatClosure
    haveI := Functor.isContinuous_overPost (inclusionTopology B S hS 𝒴)
      (fppfTopology B S hS 𝒴) (objectProperty B S hS 𝒴).ι x
    (objectProperty B S hS 𝒴).ι.sheafPushforwardContinuous AddCommGrpCat.{u + 1}
          (inclusionTopology B S hS 𝒴) (fppfTopology B S hS 𝒴) ⋙
        (inclusionTopology B S hS 𝒴).overPullback AddCommGrpCat.{u + 1} x ⋙
          Sheaf.functorH ((inclusionTopology B S hS 𝒴).over x) q ≅
      (fppfTopology B S hS 𝒴).overPullback AddCommGrpCat.{u + 1}
            ((objectProperty B S hS 𝒴).ι.obj x) ⋙
        Sheaf.functorH ((fppfTopology B S hS 𝒴).over
          ((objectProperty B S hS 𝒴).ι.obj x)) q

AlgebraicGeometry.Stack.FlatFppf.moduleCohomologyOverObjectIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteObjectwiseCohomology.lean, line 396. The attribute's comment: “part (2)(b), modules; conditional on the module form of the acyclicity statement of 0D6X only”.

Stacks 0GR0, part (2)(b) for sheaves of modules — the source's "the same holds for sheaves of modules". For an algebraic stack 𝒳, a sheaf F of O_𝒳-modules and a flat object x of 𝒳,

H^q(x, F) = H^q(𝒳_{flat,fppf}/x, g^*F),

naturally in F, where g^* is restriction of sheaves of modules to the flat-fppf site of Stacks 0787, cohomology over an object is the global cohomology on the slice site, and H^q of a sheaf of modules is Ext^q out of the structure sheaf.

Three of the four inputs are discharged rather than assumed. The closure condition of Stacks 07AK (1) holds for every algebraic stack, by AlgebraicGeometry.Stack.FlatFppf.closedUnderFlatMorphisms. The existence of g_! on sheaves of modules on the slices — the first sentence of Stacks 0789 — is AlgebraicGeometry.Stack.isRightAdjoint_subsiteSliceModuleRestriction, from essential smallness of the slice of a full subsite. Exactness of g^* is Stacks.Cohomology.DerivedLowerShriek.restriction_exact. What remains open is the module form of the acyclicity statement of Stacks 0D6X for the slice at x, carried here as the hypothesis hacyclic: see the module docstring for why the library's form of 0D6X does not apply at these universes.

The sheaf of modules is quantified over the slice site at x rather than over 𝒳 itself, which is the generalization the comparison naturally has: the source's H^q(x, F) for F on 𝒳 is the cohomology of the restriction of F to the slice, so instantiating at that restriction gives the source's statement.

noncomputable def moduleCohomologyOverObjectIso
    (x : ObjectProperty.FullSubcategory (objectProperty B S hS 𝒴))
    (hacyclic : haveI := isContinuous_inclusion B S hS 𝒴 flatClosure
      haveI := isCocontinuous_inclusion B S hS 𝒴 flatClosure
      ∀ I : SheafOfModules.{max (u + 1) t} (sliceStructureRing.{u, w, t} B S hS 𝒴 x),
          Injective I → ∀ (n : ℕ)
        (a : Ext (SheafOfModules.unit (subsiteSliceRing.{u, u + 1, u, t} B S hS 𝒴.val.val.p
              B.topology (objectProperty B S hS 𝒴) x
              (sliceStructureRing.{u, w, t} B S hS 𝒴 x)))
            ((subsiteSliceModuleRestriction.{u, u + 1, u, t} B S hS 𝒴.val.val.p B.topology
              (objectProperty B S hS 𝒴) x
              (sliceStructureRing.{u, w, t} B S hS 𝒴 x)).obj I) (n + 1)), a = 0)
    (q : ℕ) :
    haveI := isContinuous_inclusion B S hS 𝒴 flatClosure
    haveI := isCocontinuous_inclusion B S hS 𝒴 flatClosure
    haveI := isRightAdjoint_subsiteSliceModuleRestriction.{u, u + 1, u, t} B S hS 𝒴.val.val.p
      B.topology (objectProperty B S hS 𝒴) x (sliceStructureRing.{u, w, t} B S hS 𝒴 x)
    subsiteSliceModuleRestriction.{u, u + 1, u, t} B S hS 𝒴.val.val.p B.topology
          (objectProperty B S hS 𝒴) x (sliceStructureRing.{u, w, t} B S hS 𝒴 x) ⋙
        moduleFunctorH.{t, u, u + 1} ((inclusionTopology B S hS 𝒴).over x)
          (subsiteSliceRing.{u, u + 1, u, t} B S hS 𝒴.val.val.p B.topology
            (objectProperty B S hS 𝒴) x (sliceStructureRing.{u, w, t} B S hS 𝒴 x)) q ≅
      moduleFunctorH.{t, u, u + 1}
        ((fppfTopology B S hS 𝒴).over ((objectProperty B S hS 𝒴).ι.obj x))
        (sliceStructureRing.{u, w, t} B S hS 𝒴 x) q

AlgebraicGeometry.Stack.LisseEtale.cohomologyOverObjectIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteObjectwiseCohomology.lean, line 452. The attribute's comment: “part (1)(b), cohomology over a smooth object; conditional on the acyclicity statement of 0D6X only”.

Stacks 0GR0, part (1)(b). For an algebraic stack 𝒳, an abelian sheaf F on the étale site of 𝒳 and a smooth object x of 𝒳,

H^q(x, F) = H^q(𝒳_{lisse,étale}/x, g⁻¹ F),

naturally in F, where g⁻¹ is restriction to the lisse-étale site of Stacks 0787.

The closure condition of Stacks 07AK (1) for the smooth objects is discharged — it holds for every algebraic stack, by AlgebraicGeometry.Stack.LisseEtale.closedUnderSmoothMorphisms — so the inclusion of the smooth objects is continuous and cocontinuous with no hypothesis. What remains open is the acyclicity statement of Stacks 0D6X for the slice at x, carried here as the hypothesis hacyclic: see the module docstring for why the library's form of 0D6X does not apply at these universes.

def cohomologyOverObjectIso
    (x : ObjectProperty.FullSubcategory (smoothObject.{u, w} B S hS 𝒴))
    (hacyclic : haveI := isContinuous_inclusion B S hS 𝒴 (closedUnderSmoothMorphisms B S hS 𝒴)
      ∀ I : Sheaf ((associatedTopology B S hS 𝒴.val.val.p (etaleTopology B)).over
            ((smoothObject.{u, w} B S hS 𝒴).ι.obj x)) AddCommGrpCat.{u + 1},
          Injective I → ∀ (n : ℕ)
        (a : Sheaf.H ((subsiteSliceRestriction B S hS 𝒴.val.val.p (etaleTopology B)
          (smoothObject.{u, w} B S hS 𝒴) x).obj I) (n + 1)), a = 0)
    (q : ℕ) :
    haveI := isContinuous_inclusion B S hS 𝒴 (closedUnderSmoothMorphisms B S hS 𝒴)
    haveI := Functor.isContinuous_overPost (inclusionTopology.{u, w} B S hS 𝒴)
      (associatedTopology B S hS 𝒴.val.val.p (etaleTopology B))
      (smoothObject.{u, w} B S hS 𝒴).ι x
    (smoothObject.{u, w} B S hS 𝒴).ι.sheafPushforwardContinuous AddCommGrpCat.{u + 1}
          (inclusionTopology.{u, w} B S hS 𝒴)
          (associatedTopology B S hS 𝒴.val.val.p (etaleTopology B)) ⋙
        (inclusionTopology.{u, w} B S hS 𝒴).overPullback AddCommGrpCat.{u + 1} x ⋙
          Sheaf.functorH ((inclusionTopology.{u, w} B S hS 𝒴).over x) q ≅
      (associatedTopology B S hS 𝒴.val.val.p (etaleTopology B)).overPullback
            AddCommGrpCat.{u + 1} ((smoothObject.{u, w} B S hS 𝒴).ι.obj x) ⋙
        Sheaf.functorH ((associatedTopology B S hS 𝒴.val.val.p (etaleTopology B)).over
          ((smoothObject.{u, w} B S hS 𝒴).ι.obj x)) q

AlgebraicGeometry.Stack.LisseEtale.moduleCohomologyOverObjectIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteObjectwiseCohomology.lean, line 512. The attribute's comment: “part (1)(b), modules; conditional on the module form of the acyclicity statement of 0D6X only”.

Stacks 0GR0, part (1)(b) for sheaves of modules — the source's "the same holds for sheaves of modules". For an algebraic stack 𝒳, a sheaf F of O_𝒳-modules and a smooth object x of 𝒳,

H^q(x, F) = H^q(𝒳_{lisse,étale}/x, g^*F),

naturally in F, where g^* is restriction of sheaves of modules to the lisse-étale site of Stacks 0787 and H^q of a sheaf of modules is Ext^q out of the structure sheaf.

As in the flat-fppf case, three of the four inputs are discharged rather than assumed: the closure condition of Stacks 07AK (1) by AlgebraicGeometry.Stack.LisseEtale.closedUnderSmoothMorphisms, the existence of g_! on sheaves of modules on the slices by AlgebraicGeometry.Stack.isRightAdjoint_subsiteSliceModuleRestriction, and exactness of g^* by Stacks.Cohomology.DerivedLowerShriek.restriction_exact. What remains open is the module form of the acyclicity statement of Stacks 0D6X for the slice at x, carried here as the hypothesis hacyclic.

The sheaf of modules is quantified over the slice site at x, which is the generalization the comparison naturally has; see AlgebraicGeometry.Stack.FlatFppf.moduleCohomologyOverObjectIso.

noncomputable def moduleCohomologyOverObjectIso
    (x : ObjectProperty.FullSubcategory (smoothObject.{u, w} B S hS 𝒴))
    (hacyclic :
      haveI := isContinuous_inclusion B S hS 𝒴 (closedUnderSmoothMorphisms B S hS 𝒴)
      haveI := isCocontinuous_inclusion B S hS 𝒴 (closedUnderSmoothMorphisms B S hS 𝒴)
      ∀ I : SheafOfModules.{max (u + 1) t} (sliceStructureRing.{u, w, t} B S hS 𝒴 x),
          Injective I → ∀ (n : ℕ)
        (a : Ext (SheafOfModules.unit (subsiteSliceRing.{u, u + 1, u, t} B S hS 𝒴.val.val.p
              (etaleTopology B) (smoothObject.{u, w} B S hS 𝒴) x
              (sliceStructureRing.{u, w, t} B S hS 𝒴 x)))
            ((subsiteSliceModuleRestriction.{u, u + 1, u, t} B S hS 𝒴.val.val.p (etaleTopology B)
              (smoothObject.{u, w} B S hS 𝒴) x
              (sliceStructureRing.{u, w, t} B S hS 𝒴 x)).obj I) (n + 1)), a = 0)
    (q : ℕ) :
    haveI := isContinuous_inclusion B S hS 𝒴 (closedUnderSmoothMorphisms B S hS 𝒴)
    haveI := isCocontinuous_inclusion B S hS 𝒴 (closedUnderSmoothMorphisms B S hS 𝒴)
    haveI := isRightAdjoint_subsiteSliceModuleRestriction.{u, u + 1, u, t} B S hS 𝒴.val.val.p
      (etaleTopology B) (smoothObject.{u, w} B S hS 𝒴) x
      (sliceStructureRing.{u, w, t} B S hS 𝒴 x)
    subsiteSliceModuleRestriction.{u, u + 1, u, t} B S hS 𝒴.val.val.p (etaleTopology B)
          (smoothObject.{u, w} B S hS 𝒴) x (sliceStructureRing.{u, w, t} B S hS 𝒴 x) ⋙
        moduleFunctorH.{t, u, u + 1} ((inclusionTopology.{u, w} B S hS 𝒴).over x)
          (subsiteSliceRing.{u, u + 1, u, t} B S hS 𝒴.val.val.p (etaleTopology B)
            (smoothObject.{u, w} B S hS 𝒴) x
            (sliceStructureRing.{u, w, t} B S hS 𝒴 x)) q ≅
      moduleFunctorH.{t, u, u + 1}
        ((associatedTopology B S hS 𝒴.val.val.p (etaleTopology B)).over
          ((smoothObject.{u, w} B S hS 𝒴).ι.obj x))
        (sliceStructureRing.{u, w, t} B S hS 𝒴 x) q

AlgebraicGeometry.Stack.FlatFppf.sliceModuleCohomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteObjectwiseModuleCohomology.lean, line 227. The attribute's comment: “part (2)(b), sheaves of modules”.

Stacks 0GR0, part (2)(b), for sheaves of modules — the source's "the same holds for sheaves of modules". For an algebraic stack 𝒳, a flat object x of 𝒳 and a sheaf ℱ of 𝒪_𝒳-modules on the fppf site of 𝒳 over x,

H^q(x, ℱ) = H^q(𝒳_{flat,fppf}/x, g^*ℱ),

naturally in ℱ, where g^* is restriction of sheaves of modules to the flat-fppf site of Stacks 0787, cohomology over an object is the global cohomology on the slice site, and H^q of a sheaf of modules is Ext^q out of the structure sheaf.

This is AlgebraicGeometry.Stack.FlatFppf.moduleCohomologyOverObjectIso with its acyclicity hypothesis removed: it is AlgebraicGeometry.Stack.subsiteSliceModuleCohomologyIso for the flat objects, whose covering-pullback condition is AlgebraicGeometry.Stack.FlatFppf.preservesCoveringPullbacks_over_inclusion. As there, the sheaf of modules is quantified over the slice site at x, which is the generalization the comparison naturally has: the source's H^q(x, ℱ) for ℱ on 𝒳 is the cohomology of the restriction of ℱ to the slice.

def sliceModuleCohomologyIso
    (x : ObjectProperty.FullSubcategory (objectProperty B S hS 𝒴)) (q : ℕ) :
    haveI := isContinuous_inclusion B S hS 𝒴 flatClosure
    haveI := isCocontinuous_inclusion B S hS 𝒴 flatClosure
    subsiteSliceModuleRestriction.{u, u + 1, u, t} B S hS 𝒴.val.val.p B.topology
          (objectProperty B S hS 𝒴) x (sliceStructureRing.{u, w, t} B S hS 𝒴 x) ⋙
        moduleFunctorH.{t, u, u + 1} ((inclusionTopology B S hS 𝒴).over x)
          (subsiteSliceRing.{u, u + 1, u, t} B S hS 𝒴.val.val.p B.topology
            (objectProperty B S hS 𝒴) x (sliceStructureRing.{u, w, t} B S hS 𝒴 x)) q ≅
      moduleFunctorH.{t, u, u + 1}
        ((fppfTopology B S hS 𝒴).over ((objectProperty B S hS 𝒴).ι.obj x))
        (sliceStructureRing.{u, w, t} B S hS 𝒴 x) q

AlgebraicGeometry.Stack.LisseEtale.sliceModuleCohomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteObjectwiseModuleCohomology.lean, line 270. The attribute's comment: “part (1)(b), sheaves of modules”.

Stacks 0GR0, part (1)(b), for sheaves of modules — the source's "the same holds for sheaves of modules". For an algebraic stack 𝒳, a smooth object x of 𝒳 and a sheaf ℱ of 𝒪_𝒳-modules on the étale site of 𝒳 over x,

H^q(x, ℱ) = H^q(𝒳_{lisse,étale}/x, g^*ℱ),

naturally in ℱ, where g^* is restriction of sheaves of modules to the lisse-étale site of Stacks 0787 and H^q of a sheaf of modules is Ext^q out of the structure sheaf.

This is AlgebraicGeometry.Stack.LisseEtale.moduleCohomologyOverObjectIso with its acyclicity hypothesis removed: it is AlgebraicGeometry.Stack.subsiteSliceModuleCohomologyIso for the smooth objects, whose covering-pullback condition is AlgebraicGeometry.Stack.LisseEtale.preservesCoveringPullbacks_over_inclusion. The sheaf of modules is quantified over the slice site at x; see AlgebraicGeometry.Stack.FlatFppf.sliceModuleCohomologyIso.

def sliceModuleCohomologyIso
    (x : ObjectProperty.FullSubcategory (smoothObject.{u, w} B S hS 𝒴)) (q : ℕ) :
    haveI := isContinuous_inclusion B S hS 𝒴 (closedUnderSmoothMorphisms B S hS 𝒴)
    haveI := isCocontinuous_inclusion B S hS 𝒴 (closedUnderSmoothMorphisms B S hS 𝒴)
    subsiteSliceModuleRestriction.{u, u + 1, u, t} B S hS 𝒴.val.val.p (etaleTopology B)
          (smoothObject.{u, w} B S hS 𝒴) x (sliceStructureRing.{u, w, t} B S hS 𝒴 x) ⋙
        moduleFunctorH.{t, u, u + 1} ((inclusionTopology.{u, w} B S hS 𝒴).over x)
          (subsiteSliceRing.{u, u + 1, u, t} B S hS 𝒴.val.val.p (etaleTopology B)
            (smoothObject.{u, w} B S hS 𝒴) x
            (sliceStructureRing.{u, w, t} B S hS 𝒴 x)) q ≅
      moduleFunctorH.{t, u, u + 1}
        ((associatedTopology B S hS 𝒴.val.val.p (etaleTopology B)).over
          ((smoothObject.{u, w} B S hS 𝒴).ι.obj x))
        (sliceStructureRing.{u, w, t} B S hS 𝒴 x) q

Tag 0789, a lemma

Tag 0789 in the Stacks Project.

AlgebraicGeometry.Stack.FlatFppf.isRightAdjoint_modulePullback, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfModuleShriek.lean, line 169. The attribute's comment: “flat_module_shriek”.

Stacks 0789, part (2), first assertion: pullback of sheaves of modules along the flat-fppf morphism of ringed topoi g admits a left adjoint g_!.

Registered as an instance, because the functor g_! and its adjunction are then the canonical choices it supplies.

instance isRightAdjoint_modulePullback :
    (RingedToposHom.pullbackModules.{u, u, u, u + 1, u, u + 1}
      (ringedToposModulesHom B S hS 𝒳)).IsRightAdjoint

AlgebraicGeometry.Stack.LisseEtale.moduleLowerShriek, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubcategoryModuleLowerShriek.lean, line 302. The attribute's comment: “part (1), existence of the functor g_! on sheaves of modules for the lisse-étale site of an arbitrary algebraic stack”.

The functor g_! of Stacks 0789 (1) on sheaves of modules: the left adjoint of the pullback g^* along the lisse-étale morphism of ringed topoi.

noncomputable abbrev moduleLowerShriek

AlgebraicGeometry.Stack.LisseEtale.moduleLowerShriekAdjunction, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubcategoryModuleLowerShriek.lean, line 310. The attribute's comment: “part (1), left adjointness of g_! to g^* on sheaves of modules for the lisse-étale site of an arbitrary algebraic stack”.

The adjunction g_! ⊣ g^* of Stacks 0789 (1) on sheaves of modules.

noncomputable abbrev moduleLowerShriekAdjunction :
    moduleLowerShriek.{u, t} B S hS 𝒳 ⊣ modulePullback.{u, t} B S hS 𝒳

AlgebraicGeometry.Stack.LisseEtale.isIso_moduleLowerShriekAdjunction_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubcategoryModuleLowerShriek.lean, line 320. The attribute's comment: “part (1), g^*g_! = id on sheaves of modules for the lisse-étale site of an arbitrary algebraic stack”.

Stacks 0789 (1), g^*g_! = id: the unit of the adjunction g_! ⊣ g^* on sheaves of modules for the lisse-étale site is an isomorphism.

theorem isIso_moduleLowerShriekAdjunction_unit :
    IsIso (moduleLowerShriekAdjunction.{u, t} B S hS 𝒳).unit

AlgebraicGeometry.Stack.FlatFppf.moduleLowerShriek, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubcategoryModuleLowerShriek.lean, line 379. The attribute's comment: “part (2), existence of the functor g_! on sheaves of modules for the flat-fppf site of an arbitrary algebraic stack”.

The functor g_! of Stacks 0789 (2) on sheaves of modules: the left adjoint of the pullback g^* along the flat-fppf morphism of ringed topoi.

noncomputable abbrev moduleLowerShriek

AlgebraicGeometry.Stack.FlatFppf.moduleLowerShriekAdjunction, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubcategoryModuleLowerShriek.lean, line 386. The attribute's comment: “part (2), left adjointness of g_! to g^* on sheaves of modules for the flat-fppf site of an arbitrary algebraic stack”.

The adjunction g_! ⊣ g^* of Stacks 0789 (2) on sheaves of modules.

noncomputable abbrev moduleLowerShriekAdjunction :
    moduleLowerShriek B S hS 𝒳 ⊣ modulePullback B S hS 𝒳

AlgebraicGeometry.Stack.FlatFppf.isIso_moduleLowerShriekAdjunction_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubcategoryModuleLowerShriek.lean, line 395. The attribute's comment: “part (2), g^*g_! = id on sheaves of modules for the flat-fppf site of an arbitrary algebraic stack”.

Stacks 0789 (2), g^*g_! = id: the unit of the adjunction g_! ⊣ g^* on sheaves of modules for the flat-fppf site is an isomorphism.

theorem isIso_moduleLowerShriekAdjunction_unit :
    IsIso (moduleLowerShriekAdjunction B S hS 𝒳).unit

AlgebraicGeometry.Stack.LisseEtale.moduleLowerShriekForgetIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubcategoryModuleLowerShriekForget.lean, line 291. The attribute's comment: “part (1), g_! on sheaves of modules agrees with g_! on abelian sheaves, for the lisse-étale site of an arbitrary algebraic stack”.

Stacks 0789 (1), g_! on modules agrees with g_! on abelian sheaves. For the lisse-étale site of an arbitrary algebraic stack 𝒳, the underlying abelian sheaf of g_!M, for g_! the lower shriek AlgebraicGeometry.Stack.LisseEtale.moduleLowerShriek on sheaves of modules, is the lower shriek of the underlying abelian sheaf of M, for g_! the left adjoint of restriction of abelian sheaves along the inclusion of the smooth objects (Stacks 0788 (1)(d)); naturally in M. The abelian sheaves are taken at the universe of the module sections, which is where the underlying abelian sheaves of the modules live.

The isomorphism is the canonical comparison of Stacks 0798 (Stacks.SheafOfModules.lowerShriekForgetComparison), which is invertible here because the structure sheaf of each slice 𝒳_étale/x is the left Kan extension of its restriction to 𝒳_{lisse,étale}/x (Stacks 07AJ on the slice; see AlgebraicGeometry.Stack.bijective_whiskerLeft_overPost_structureSheaf).

def moduleLowerShriekForgetIso :
    SheafOfModules.toSheaf _ ⋙ (smoothObject.{u, t} B S hS 𝒳).ι.sheafPullback AddCommGrpCat.{u}
        (inclusionTopology.{u, t} B S hS 𝒳)
        (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B)) ≅
      moduleLowerShriek.{u, t} B S hS 𝒳 ⋙ SheafOfModules.toSheaf _

AlgebraicGeometry.Stack.LisseEtale.moduleLowerShriek_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubcategoryModuleLowerShriekForget.lean, line 309. The attribute's comment: “part (1), all four assertions, for the lisse-étale site of an arbitrary algebraic stack”.

Stacks 0789 (1), the whole part, for the lisse-étale site of an arbitrary algebraic stack 𝒳: the pullback g^* of sheaves of modules has a left adjoint g_! (AlgebraicGeometry.Stack.LisseEtale.moduleLowerShriek, with adjunction AlgebraicGeometry.Stack.LisseEtale.moduleLowerShriekAdjunction); g_! agrees with the functor g_! on abelian sheaves, i.e. forgetting the module structure commutes with it (AlgebraicGeometry.Stack.LisseEtale.moduleLowerShriekForgetIso); and g^*g_! = id, the unit of the adjunction being an isomorphism.

theorem moduleLowerShriek_spec :
    (modulePullback.{u, t} B S hS 𝒳).IsRightAdjoint ∧
      Nonempty (SheafOfModules.toSheaf _ ⋙
          (smoothObject.{u, t} B S hS 𝒳).ι.sheafPullback AddCommGrpCat.{u}
            (inclusionTopology.{u, t} B S hS 𝒳)
            (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B)) ≅
        moduleLowerShriek.{u, t} B S hS 𝒳 ⋙ SheafOfModules.toSheaf _) ∧
      IsIso (moduleLowerShriekAdjunction.{u, t} B S hS 𝒳).unit

AlgebraicGeometry.Stack.FlatFppf.moduleLowerShriekForgetIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubcategoryModuleLowerShriekForget.lean, line 345. The attribute's comment: “part (2), g_! on sheaves of modules agrees with g_! on abelian sheaves, for the flat-fppf site of an arbitrary algebraic stack”.

Stacks 0789 (2), g_! on modules agrees with g_! on abelian sheaves. For the flat-fppf site of an arbitrary algebraic stack 𝒳, the underlying abelian sheaf of g_!M, for g_! the lower shriek AlgebraicGeometry.Stack.FlatFppf.moduleLowerShriek on sheaves of modules, is the lower shriek of the underlying abelian sheaf of M, for g_! the left adjoint of restriction of abelian sheaves along the inclusion of the flat objects (Stacks 0788 (2)(d)); naturally in M. The abelian sheaves are taken at the universe of the module sections.

The isomorphism is the canonical comparison of Stacks 0798, invertible because the structure sheaf of each slice 𝒳_fppf/x is the left Kan extension of its restriction to 𝒳_{flat,fppf}/x (Stacks 07AJ on the slice): the affine line and plane over a flat object are flat objects.

def moduleLowerShriekForgetIso :
    SheafOfModules.toSheaf _ ⋙ (objectProperty B S hS 𝒳).ι.sheafPullback AddCommGrpCat.{u}
        (inclusionTopology B S hS 𝒳) (associatedTopology B S hS 𝒳.val.val.p B.topology) ≅
      moduleLowerShriek B S hS 𝒳 ⋙ SheafOfModules.toSheaf _

AlgebraicGeometry.Stack.FlatFppf.moduleLowerShriek_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubcategoryModuleLowerShriekForget.lean, line 362. The attribute's comment: “part (2), all four assertions, for the flat-fppf site of an arbitrary algebraic stack”.

Stacks 0789 (2), the whole part, for the flat-fppf site of an arbitrary algebraic stack 𝒳: the pullback g^* of sheaves of modules has a left adjoint g_! (AlgebraicGeometry.Stack.FlatFppf.moduleLowerShriek, with adjunction AlgebraicGeometry.Stack.FlatFppf.moduleLowerShriekAdjunction); g_! agrees with the functor g_! on abelian sheaves, i.e. forgetting the module structure commutes with it (AlgebraicGeometry.Stack.FlatFppf.moduleLowerShriekForgetIso); and g^*g_! = id, the unit of the adjunction being an isomorphism.

theorem moduleLowerShriek_spec :
    (modulePullback B S hS 𝒳).IsRightAdjoint ∧
      Nonempty (SheafOfModules.toSheaf _ ⋙
          (objectProperty B S hS 𝒳).ι.sheafPullback AddCommGrpCat.{u}
            (inclusionTopology B S hS 𝒳) (associatedTopology B S hS 𝒳.val.val.p B.topology) ≅
        moduleLowerShriek B S hS 𝒳 ⋙ SheafOfModules.toSheaf _) ∧
      IsIso (moduleLowerShriekAdjunction B S hS 𝒳).unit

Tag 078A, a lemma

Tag 078A in the Stacks Project.

AlgebraicGeometry.Stack.LisseEtale.isIso_unitLowerShriekMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubcategoryUnitLowerShriek.lean, line 260. The attribute's comment: “part (1); conditional on essential smallness of the category underlying the algebraic stack and on restriction along the lisse-étale inclusion being bijective on morphisms out of the structure sheaf of modules of the stack”.

Stacks 078A (1): g_!O_{𝒳_{lisse,étale}} = O_𝒳, the canonical map from the lower shriek of the structure sheaf of the lisse-étale site to the structure sheaf of 𝒳 being an isomorphism.

theorem isIso_unitLowerShriekMap
    (hres : ∀ T : SheafOfModules.{u}
        (Stacks.SheafOfModules.Tensor.ringSheaf (associatedRingedTopos B S hS 𝒳.val.val.p
          𝒳.val.isFiberedInGroupoids (etaleTopology B) (etaleTopology_le_topology B)).O),
      Function.Bijective fun x : SheafOfModules.unit
          (Stacks.SheafOfModules.Tensor.ringSheaf (associatedRingedTopos B S hS 𝒳.val.val.p
            𝒳.val.isFiberedInGroupoids (etaleTopology B) (etaleTopology_le_topology B)).O) ⟶ T =>
        (subsiteModulePullback B S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids
          (etaleTopology B) (etaleTopology_le_topology B)
          (smoothObject.{u, t} B S hS 𝒳)).map x) :
    IsIso (unitLowerShriekMap.{u, t} B S hS 𝒳)

AlgebraicGeometry.Stack.FlatFppf.isIso_unitLowerShriekMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubcategoryUnitLowerShriek.lean, line 296. The attribute's comment: “part (2); conditional on essential smallness of the category underlying the algebraic stack and on restriction along the flat-fppf inclusion being bijective on morphisms out of the structure sheaf of modules of the stack”.

Stacks 078A (2): g_!O_{𝒳_{flat,fppf}} = O_𝒳, the canonical map from the lower shriek of the structure sheaf of the flat-fppf site to the structure sheaf of 𝒳 being an isomorphism.

theorem isIso_unitLowerShriekMap
    (hres : ∀ T : SheafOfModules.{u}
        (Stacks.SheafOfModules.Tensor.ringSheaf (associatedRingedTopos B S hS 𝒳.val.val.p
          𝒳.val.isFiberedInGroupoids B.topology le_rfl).O),
      Function.Bijective fun x : SheafOfModules.unit
          (Stacks.SheafOfModules.Tensor.ringSheaf (associatedRingedTopos B S hS 𝒳.val.val.p
            𝒳.val.isFiberedInGroupoids B.topology le_rfl).O) ⟶ T =>
        (subsiteModulePullback B S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids B.topology le_rfl
          (objectProperty B S hS 𝒳)).map x) :
    IsIso (unitLowerShriekMap B S hS 𝒳)

AlgebraicGeometry.Stack.LisseEtale.isIso_unitLowerShriekMap_algebraicStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubcategoryUnitLowerShriekAtlas.lean, line 338. The attribute's comment: “part (1)”.

Stacks 078A (1): g_!O_{𝒳_{lisse,étale}} = O_𝒳 for every algebraic stack 𝒳. The canonical map from the lower shriek, along the morphism of ringed topoi g : (Sh(𝒳_{lisse,étale}), O_{𝒳_{lisse,étale}}) ⟶ (Sh(𝒳_étale), O_𝒳) of Stacks 0788, of the structure sheaf of the lisse-étale site to the structure sheaf of 𝒳 — the transpose under the adjunction g_! ⊣ g^* of Stacks 0789 (1) of the identification O_{𝒳_{lisse,étale}} = g^{-1}O_𝒳 — is an isomorphism.

theorem isIso_unitLowerShriekMap_algebraicStack : IsIso (unitLowerShriekMap.{u, t} B S hS 𝒳)

AlgebraicGeometry.Stack.FlatFppf.isIso_unitLowerShriekMap_algebraicStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubcategoryUnitLowerShriekAtlas.lean, line 377. The attribute's comment: “part (2)”.

Stacks 078A (2): g_!O_{𝒳_{flat,fppf}} = O_𝒳 for every algebraic stack 𝒳. The canonical map from the lower shriek, along the morphism of ringed topoi g : (Sh(𝒳_{flat,fppf}), O_{𝒳_{flat,fppf}}) ⟶ (Sh(𝒳_fppf), O_𝒳) of Stacks 0788, of the structure sheaf of the flat-fppf site to the structure sheaf of 𝒳 — the transpose under the adjunction g_! ⊣ g^* of Stacks 0789 (2) of the identification O_{𝒳_{flat,fppf}} = g^{-1}O_𝒳 — is an isomorphism.

theorem isIso_unitLowerShriekMap_algebraicStack : IsIso (unitLowerShriekMap B S hS 𝒳)

Tag 07AR, a lemma

Tag 07AR in the Stacks Project.

AlgebraicGeometry.Stack.LisseEtale.isParasitic_iff_isZero_pullbackModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ParasiticLisseEtalePullbackVanishing.lean, line 103. The attribute's comment: “part (1), the lisse-étale site”.

Stacks 07AR (1). A sheaf of modules on the étale site of an algebraic stack which has the flat base change property of Stacks 0762 is parasitic exactly when its pullback along the lisse-étale morphism of ringed topoi of Stacks 0788 (1) vanishes.

The pullback is restriction to the smooth objects (AlgebraicGeometry.Stack.LisseEtale.modulePullbackIso), so the right-hand side says that the sections of F vanish at every smooth object. A smooth object is flat, which gives one implication with no hypothesis; the converse is where the flat base change property is used, to carry the vanishing along a flat arrow out of an object covering a given flat object.

theorem isParasitic_iff_isZero_pullbackModules
    (F : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf.{u + 1, u, u}
      (etaleRingedTopos.{u, w} B S hS 𝒳).O))
    (hfbc : HasFlatBaseChangeProperty B E h S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids
      (etaleTopology B) (etaleTopology_le_topology B) F.val) :
    IsParasitic.{u, w, u} B S hS 𝒳 .etale F.val ↔
      IsZero ((RingedToposHom.pullbackModules.{u, u, u, u + 1, u, u + 1}
        (ringedToposModulesHom.{u, w} B S hS 𝒳)).obj F)

AlgebraicGeometry.Stack.isParasitic_iff_isZero_pullbackModules_lisseEtale_and_flatFppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ParasiticLisseEtalePullbackVanishing.lean, line 146. The attribute's comment: “the whole statement: parts (1) and (2) conjoined”.

Stacks 07AR, the whole statement. For an algebraic stack 𝒳:

• (1) a sheaf of 𝒪_𝒳-modules F on 𝒳_étale with the flat base change property of Stacks 0762 is parasitic exactly when g^*F = 0 for the lisse-étale morphism of ringed topoi of Stacks 0788 (1); and
• (2) a sheaf of 𝒪_𝒳-modules G on 𝒳_fppf is parasitic exactly when g^*G = 0 for the flat-fppf morphism of ringed topoi of Stacks 0788 (2), with no hypothesis.

The two conjuncts are AlgebraicGeometry.Stack.LisseEtale.isParasitic_iff_isZero_pullbackModules and AlgebraicGeometry.Stack.FlatFppf.isParasitic_iff_isZero_pullbackModules.

theorem isParasitic_iff_isZero_pullbackModules_lisseEtale_and_flatFppf
    (F : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf.{u + 1, u, u}
      (LisseEtale.etaleRingedTopos.{u, w} B S hS 𝒳).O))
    (hfbc : HasFlatBaseChangeProperty B E h S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids
      (etaleTopology B) (etaleTopology_le_topology B) F.val)
    (G : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf.{u + 1, u, u}
      (FlatFppf.fppfRingedTopos B S hS 𝒳).O)) :
    (IsParasitic.{u, w, u} B S hS 𝒳 .etale F.val ↔
        IsZero ((RingedToposHom.pullbackModules.{u, u, u, u + 1, u, u + 1}
          (LisseEtale.ringedToposModulesHom.{u, w} B S hS 𝒳)).obj F)) ∧
      (IsParasitic.{u, w, u} B S hS 𝒳 .fppf G.val ↔
        IsZero ((RingedToposHom.pullbackModules.{u, u, u, u + 1, u, u + 1}
          (FlatFppf.ringedToposModulesHom B S hS 𝒳)).obj G))

AlgebraicGeometry.Stack.FlatFppf.isParasitic_iff_isZero_pullbackModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ParasiticPullbackVanishing.lean, line 76. The attribute's comment: “part (2), the flat-fppf site”.

Stacks 07AR (2). A sheaf of modules on the fppf site of an algebraic stack is parasitic exactly when its pullback along the flat-fppf morphism of ringed topoi of Stacks 0788 (2) vanishes.

The flat-fppf site has the flat objects of 𝒳 for its objects, and the pullback along g is restriction to them (AlgebraicGeometry.Stack.FlatFppf.modulePullbackIso), so the two conditions are the same condition read on the two sites.

theorem isParasitic_iff_isZero_pullbackModules
    (F : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf.{u + 1, u, u} (fppfRingedTopos B S hS 𝒳).O)) :
    IsParasitic B S hS 𝒳 .fppf F.val ↔
      IsZero ((RingedToposHom.pullbackModules.{u, u, u, u + 1, u, u + 1}
        (ringedToposModulesHom B S hS 𝒳)).obj F)

Sources

• Section 103.14, Tag 0786
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.FlatFppf · AlgebraicGeometry.Stack.FlatFppf.IsCovering · AlgebraicGeometry.Stack.FlatFppf.topology · AlgebraicGeometry.Stack.LisseEtale · AlgebraicGeometry.Stack.LisseEtale.IsCovering · AlgebraicGeometry.Stack.LisseEtale.topology · AlgebraicGeometry.Stack.smoothObject_schemeStack_iff · AlgebraicGeometry.Stack.flatObject

Section103.15 Functoriality of the lisse-étale and flat-fppf sites#

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

Tag 07AT, a lemma

Tag 07AT in the Stacks Project.

AlgebraicGeometry.Stack.FlatFppf.siteFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfSiteFunctor.lean, line 261. The attribute's comment: “the functor of flat-fppf sites along a flat 1-morphism”.

The restriction of a flat 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S to a functor between the flat-fppf sites, specified by the property that its composite with the inclusion of the flat objects of 𝒴 is the inclusion of those of 𝒳 followed by the underlying functor of f.

def siteFunctor (f : 𝒳 ⟶ 𝒴) (hf : AlgebraicStacks.IsFlat B S hS f) :
    {F : FlatFppf B S hS 𝒳 ⥤ FlatFppf B S hS 𝒴 //
      F ⋙ inclusion B S hS 𝒴 =
        inclusion B S hS 𝒳 ⋙ f.hom.hom.toFunctor}

AlgebraicGeometry.Stack.FlatFppf.siteFunctor_isContinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfSiteFunctor.lean, line 287. The attribute's comment: “that functor is continuous”.

The restriction of a flat 1-morphism to the flat-fppf sites is continuous.

theorem siteFunctor_isContinuous (f : 𝒳 ⟶ 𝒴) (hf : AlgebraicStacks.IsFlat B S hS f) :
    (siteFunctor B S hS f hf).1.IsContinuous
      (topology B S hS 𝒳) (topology B S hS 𝒴)

AlgebraicGeometry.Stack.FlatFppf.siteFunctor_isCocontinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfSiteFunctor.lean, line 309. The attribute's comment: “that functor is cocontinuous”.

The restriction of a flat 1-morphism to the flat-fppf sites is cocontinuous.

theorem siteFunctor_isCocontinuous (f : 𝒳 ⟶ 𝒴) (hf : AlgebraicStacks.IsFlat B S hS f) :
    (siteFunctor B S hS f hf).1.IsCocontinuous
      (topology B S hS 𝒳) (topology B S hS 𝒴)

AlgebraicGeometry.Stack.LisseEtale.siteFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleSiteFunctor.lean, line 143. The attribute's comment: “the functor of lisse-etale sites along a smooth 1-morphism”.

Stacks 07AT (1), the site functor. A smooth 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S restricts to a functor between the lisse-étale sites, specified by the property that its composite with the inclusion of the smooth objects of 𝒴 is the inclusion of those of 𝒳 followed by the underlying functor of f.

The restriction exists because f carries smooth objects to smooth objects (AlgebraicGeometry.Stack.LisseEtale.smoothObject_map), and that equality of composites is what says its action on objects and arrows is the action of f.

def siteFunctor (f : 𝒳 ⟶ 𝒴) (hf : AlgebraicStacks.IsSmooth B S hS f) :
    {F : LisseEtale.{u, w} B S hS 𝒳 ⥤ LisseEtale.{u, w} B S hS 𝒴 //
      F ⋙ inclusion.{u, w} B S hS 𝒴 =
        inclusion.{u, w} B S hS 𝒳 ⋙ f.hom.hom.toFunctor}

AlgebraicGeometry.Stack.LisseEtale.siteFunctor_isContinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleSiteFunctor.lean, line 155. The attribute's comment: “that functor is continuous, in the smooth case”.

Stacks 07AT (1), continuity. The restriction of a smooth 1-morphism to the lisse-étale sites is continuous: its composite with the inclusion of 𝒴 is, and continuity descends along that inclusion, which is fully faithful and cocontinuous by Stacks 0788 (1).

theorem siteFunctor_isContinuous (f : 𝒳 ⟶ 𝒴) (hf : AlgebraicStacks.IsSmooth B S hS f) :
    (siteFunctor.{u, w} B S hS f hf).1.IsContinuous
      (topology.{u, w} B S hS 𝒳) (topology.{u, w} B S hS 𝒴)

AlgebraicGeometry.Stack.LisseEtale.siteFunctor_isCocontinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleSiteFunctor.lean, line 174. The attribute's comment: “that functor is cocontinuous, in the smooth case”.

Stacks 07AT (1), cocontinuity. The same descent, with the roles of continuity and cocontinuity of the inclusion exchanged.

theorem siteFunctor_isCocontinuous (f : 𝒳 ⟶ 𝒴) (hf : AlgebraicStacks.IsSmooth B S hS f) :
    (siteFunctor.{u, w} B S hS f hf).1.IsCocontinuous
      (topology.{u, w} B S hS 𝒳) (topology.{u, w} B S hS 𝒴)

AlgebraicGeometry.Stack.FlatFppf.primedPushforwardAmbientEquiv', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsitePushforwardAmbientUnconditional.lean, line 176. The attribute's comment: “part (2), the identity f'_*(g')^{-1} = g^{-1}f_* for the flat-fppf site, at one flat object y of 𝒴 and for a sheaf of sets, with NO hypothesis beyond the sheaf condition on ℱ: the topology on the 2-fibre product V ×_{y, 𝒴} 𝒳 that AlgebraicGeometry.Stack.FlatFppf.primedPushforwardAmbientEquiv takes as J is AlgebraicGeometry.Stack.ambientTwoFibreProductTopology, and its arguments hℱ, hfac and hconn are the theorems AlgebraicGeometry.Stack.isSheaf_comp_ambientProjection, AlgebraicGeometry.Stack.FlatFppf.hasLocalFactorizations_primedInclusion and AlgebraicGeometry.Stack.FlatFppf.hasLocallyConnectedFactorizations_primedInclusion, each proved for every algebraic stack. The site functor itself and its continuity and cocontinuity, which are the first assertion of the tag, are registered in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfSiteFunctor.lean. Three pieces of the tag are not covered here: naturality of the bijection in y, so that it becomes an equality of sheaves on 𝒴_{flat,fppf} rather than a family of bijections; the same identity at abelian rather than set coefficients; and the second identity g'_!(f')^{-1} = f^{-1}g_!. The first and the third are registered in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteSheafPushforwardBaseChange.lean; the abelian form is claimed nowhere in the tree, and the tag does not ask for it -- the source's ℱ is a sheaf of sets, which is what the functors of a morphism of topoi act on”.

Stacks 07AT (2), the identity f'_*(g')^{-1} = g^{-1}f_*, at one flat object of 𝒴 and for a sheaf of sets, with no further hypothesis. For a flat 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks, a flat object y of 𝒴 and a sheaf ℱ of sets on the fppf site of 𝒳, the value at y of the pushforward along the restriction f' of f to the flat-fppf sites of the restriction of ℱ to the flat-fppf site of 𝒳 is the value at y of the pushforward of ℱ along f.

This is AlgebraicGeometry.Stack.FlatFppf.primedPushforwardAmbientEquiv at the topology of AlgebraicGeometry.Stack.ambientTwoFibreProductTopology, whose three remaining inputs are AlgebraicGeometry.Stack.isSheaf_comp_ambientProjection, AlgebraicGeometry.Stack.FlatFppf.hasLocalFactorizations_primedInclusion and AlgebraicGeometry.Stack.FlatFppf.hasLocallyConnectedFactorizations_primedInclusion.

def primedPushforwardAmbientEquiv' (hf : AlgebraicStacks.IsFlat B S hS f)
    (y : FlatFppf B S hS 𝒴) (ℱ : (𝒳.val.val.obj)ᵒᵖ ⥤ Type (u + 1))
    (hℱ : Presieve.IsSheaf (BigFppfOver.associatedTopology B S hS 𝒳.val.val.p .fppf) ℱ) :
    ((primedSiteFunctor B S hS f hf).op.ran.obj ((inclusion B S hS 𝒳).op ⋙ ℱ)).obj (op y) ≃
      (f.hom.hom.toFunctor.op.ran.obj ℱ).obj (op y.obj)

AlgebraicGeometry.Stack.LisseEtale.primedPushforwardAmbientEquiv', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsitePushforwardAmbientUnconditional.lean, line 246. The attribute's comment: “part (1), the identity f'_*(g')^{-1} = g^{-1}f_* for the lisse-étale site, at one smooth object y of 𝒴 and for a sheaf of sets, with NO hypothesis beyond the sheaf condition on ℱ: the topology on the 2-fibre product V ×_{y, 𝒴} 𝒳 that AlgebraicGeometry.Stack.LisseEtale.primedPushforwardAmbientEquiv takes as J is AlgebraicGeometry.Stack.ambientTwoFibreProductTopology, and its arguments hℱ, hfac and hconn are the theorems AlgebraicGeometry.Stack.isSheaf_comp_ambientProjection, AlgebraicGeometry.Stack.LisseEtale.hasLocalFactorizations_primedInclusion and AlgebraicGeometry.Stack.LisseEtale.hasLocallyConnectedFactorizations_primedInclusion, each proved for every algebraic stack. The site functor itself and its continuity and cocontinuity, which are the first assertion of the tag, are registered in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleSiteFunctor.lean. Three pieces of the tag are not covered here: naturality of the bijection in y, so that it becomes an equality of sheaves on 𝒴_{lisse,étale} rather than a family of bijections; the same identity at abelian rather than set coefficients; and the second identity g'_!(f')^{-1} = f^{-1}g_!. The first and the third are registered in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteSheafPushforwardBaseChange.lean; the abelian form is claimed nowhere in the tree, and the tag does not ask for it -- the source's ℱ is a sheaf of sets, which is what the functors of a morphism of topoi act on”.

Stacks 07AT (1), the identity f'_*(g')^{-1} = g^{-1}f_*, at one smooth object of 𝒴 and for a sheaf of sets, with no further hypothesis. For a smooth 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks, a smooth object y of 𝒴 and a sheaf ℱ of sets on the étale site of 𝒳, the value at y of the pushforward along the restriction f' of f to the lisse-étale sites of the restriction of ℱ to the lisse-étale site of 𝒳 is the value at y of the pushforward of ℱ along f.

This is AlgebraicGeometry.Stack.LisseEtale.primedPushforwardAmbientEquiv at the topology of AlgebraicGeometry.Stack.ambientTwoFibreProductTopology, whose three remaining inputs are AlgebraicGeometry.Stack.isSheaf_comp_ambientProjection, AlgebraicGeometry.Stack.LisseEtale.hasLocalFactorizations_primedInclusion and AlgebraicGeometry.Stack.LisseEtale.hasLocallyConnectedFactorizations_primedInclusion.

def primedPushforwardAmbientEquiv' (hf : AlgebraicStacks.IsSmooth B S hS f)
    (y : LisseEtale.{u, w} B S hS 𝒴) (ℱ : (𝒳.val.val.obj)ᵒᵖ ⥤ Type (u + 1))
    (hℱ : Presieve.IsSheaf (BigFppfOver.associatedTopology B S hS 𝒳.val.val.p .etale) ℱ) :
    ((primedSiteFunctor.{u, w} B S hS f hf).op.ran.obj
        ((inclusion.{u, w} B S hS 𝒳).op ⋙ ℱ)).obj (op y) ≃
      (f.hom.hom.toFunctor.op.ran.obj ℱ).obj (op y.obj)

AlgebraicGeometry.Stack.LisseEtale.siteFunctorRingedToposHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteRingedSquare.lean, line 226. The attribute's comment: “part (1), clause (d): the restriction f' of a smooth 1-morphism to the lisse-étale sites is a morphism of ringed topoi, at the universe in which the structure sheaf of Stacks 06TV takes its sections. Its structure map is the canonical identification of the two restricted structure sheaves”.

Stacks 07AT (1), clause (d). The restriction f' of a smooth 1-morphism to the lisse-étale sites is a morphism of ringed topoi. Its inverse image is restriction along the site functor, and its structure map is the canonical identification of the two lisse-étale structure sheaves: both are restrictions of the structure sheaf of Stacks 06TV of the base, along the two composites of the square, which agree on the nose.

def siteFunctorRingedToposHom (f : 𝒳 ⟶ 𝒴) (hf : AlgebraicStacks.IsSmooth B S hS f) :
    RingedToposHom
      (ringedTopos.{u, w} B S hS 𝒳 (closedUnderSmoothMorphisms.{u, w} B S hS 𝒳))
      (ringedTopos.{u, w} B S hS 𝒴 (closedUnderSmoothMorphisms.{u, w} B S hS 𝒴))

AlgebraicGeometry.Stack.LisseEtale.isIso_fSharpInverseImage_siteFunctorRingedToposHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteRingedSquare.lean, line 248. The attribute's comment: “part (1), clause (d): the structure map of f' on the lisse-étale sites is an isomorphism, so f' is a flat morphism of ringed topoi”.

Stacks 07AT (1), clause (d). The structure map of f' is an isomorphism: it is the canonical identification of the two restricted structure sheaves.

theorem isIso_fSharpInverseImage_siteFunctorRingedToposHom (f : 𝒳 ⟶ 𝒴)
    (hf : AlgebraicStacks.IsSmooth B S hS f) :
    IsIso (siteFunctorRingedToposHom.{u, w} B S hS f hf).fSharpInverseImage

AlgebraicGeometry.Stack.LisseEtale.ringedSquareTwoIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteRingedSquare.lean, line 367. The attribute's comment: “part (1), clause (e): the square of ringed topoi formed by f, its restriction f' to the lisse-étale sites and the two inclusions g, g' of Stacks 0788 2-commutes. The invertible 2-morphism is the adjoint mate of the canonical morphism of the equality of the two inverse images”.

Stacks 07AT (1), clause (e). The square of ringed topoi 2-commutes: the composite g' ∘ f' and the composite f ∘ g are 2-isomorphic as morphisms of ringed topoi (Sh(𝒳_{lisse,étale}), O) ⟶ (Sh(𝒴_{étale}), O).

The 2-isomorphism is the adjoint mate of the canonical morphism of AlgebraicGeometry.Stack.LisseEtale.ringedSquare_inverseImage_eq: the two ways around the square restrict along the same functor of sites, so their inverse images are equal, and every structure map in sight is the restriction comparison followed by an equality of structure sheaves, hence a transport. Compatibility of the mate with the structure maps is then automatic, both sides of it being transports between the same two objects.

def ringedSquareTwoIso (f : 𝒳 ⟶ 𝒴) (hf : AlgebraicStacks.IsSmooth B S hS f) :
    RingedToposHom.TwoIso
      (A := ringedTopos.{u, w} B S hS 𝒳 (closedUnderSmoothMorphisms.{u, w} B S hS 𝒳))
      (B := etaleRingedTopos.{u, w} B S hS 𝒴)
      (ringedSquareDownAcross.{u, w} B S hS f)
      (ringedSquareAcrossDown.{u, w} B S hS f hf)

AlgebraicGeometry.Stack.FlatFppf.siteFunctorRingedToposHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteRingedSquare.lean, line 425. The attribute's comment: “part (2), clause (d): the restriction f' of a flat 1-morphism to the flat-fppf sites is a morphism of ringed topoi, at the universe in which the structure sheaf of Stacks 06TV takes its sections. Its structure map is the canonical identification of the two restricted structure sheaves”.

Stacks 07AT (2), clause (d). The restriction f' of a flat 1-morphism to the flat-fppf sites is a morphism of ringed topoi. Its inverse image is restriction along the site functor, and its structure map is the canonical identification of the two flat-fppf structure sheaves.

def siteFunctorRingedToposHom (f : 𝒳 ⟶ 𝒴) (hf : AlgebraicStacks.IsFlat B S hS f) :
    RingedToposHom (ringedTopos B S hS 𝒳) (ringedTopos B S hS 𝒴)

AlgebraicGeometry.Stack.FlatFppf.isIso_fSharpInverseImage_siteFunctorRingedToposHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteRingedSquare.lean, line 442. The attribute's comment: “part (2), clause (d): the structure map of f' on the flat-fppf sites is an isomorphism, so f' is a flat morphism of ringed topoi”.

Stacks 07AT (2), clause (d). The structure map of f' is an isomorphism.

theorem isIso_fSharpInverseImage_siteFunctorRingedToposHom (f : 𝒳 ⟶ 𝒴)
    (hf : AlgebraicStacks.IsFlat B S hS f) :
    IsIso (siteFunctorRingedToposHom B S hS f hf).fSharpInverseImage

AlgebraicGeometry.Stack.FlatFppf.ringedSquareTwoIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteRingedSquare.lean, line 536. The attribute's comment: “part (2), clause (e): the square of ringed topoi formed by f, its restriction f' to the flat-fppf sites and the two inclusions g, g' of Stacks 0788 2-commutes. The invertible 2-morphism is the adjoint mate of the canonical morphism of the equality of the two inverse images”.

Stacks 07AT (2), clause (e). The square of ringed topoi 2-commutes: g' ∘ f' and f ∘ g are 2-isomorphic as morphisms of ringed topoi (Sh(𝒳_{flat,fppf}), O) ⟶ (Sh(𝒳_{fppf}), O), the 2-isomorphism being the adjoint mate of the canonical morphism of AlgebraicGeometry.Stack.FlatFppf.ringedSquare_inverseImage_eq.

def ringedSquareTwoIso (f : 𝒳 ⟶ 𝒴) (hf : AlgebraicStacks.IsFlat B S hS f) :
    RingedToposHom.TwoIso (A := ringedTopos B S hS 𝒳) (B := fppfRingedTopos B S hS 𝒴)
      (ringedSquareDownAcross B S hS f) (ringedSquareAcrossDown B S hS f hf)

AlgebraicGeometry.Stack.LisseEtale.isIso_sheafBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteSheafPushforwardBaseChange.lean, line 103. The attribute's comment: “part (1), the identity f'_*(g')^{-1} = g^{-1}f_* for the lisse-étale site, on sheaves of sets and natural in the object of the lisse-étale site of 𝒴: the canonical map of Sites, Section 06UM, which is CategoryTheory.SubsitePushforward.subsiteRanBaseChange at the square of f, its restriction f' and the two inclusions, is invertible. The site functor and its continuity and cocontinuity are registered in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleSiteFunctor.lean”.

Stacks 07AT (1), the identity f'_*(g')^{-1} = g^{-1}f_*. For a smooth 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks, the canonical map of Sites, Section 06UM from the restriction along the inclusion g of the lisse-étale site of 𝒴 of the pushforward along f, to the pushforward along the restriction f' of the restriction along the inclusion g' of the lisse-étale site of 𝒳, is an isomorphism of functors on sheaves of sets.

theorem isIso_sheafBaseChange :
    IsIso (SubsitePushforward.subsiteSheafBaseChange.{_, _, _, _, u + 1} f.hom.hom.toFunctor
      (smoothObject.{u, w} B S hS 𝒳) (smoothObject_map.{u, w} B S hS f hf)
      (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
      (associatedTopology B S hS 𝒴.val.val.p (etaleTopology B))
      (topology.{u, w} B S hS 𝒳) (topology.{u, w} B S hS 𝒴)
      (isContinuous_and_isCocontinuous_homFunctor_associatedTopology B S hS f
        (etaleTopology B)).2
      (isCocontinuous_subsiteFunctor_topology.{u, w} B S hS f hf)
      (isContinuous_inclusion_topology'.{u, w} B S hS 𝒳)
      (isContinuous_inclusion_topology'.{u, w} B S hS 𝒴))

AlgebraicGeometry.Stack.LisseEtale.shriekBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteSheafPushforwardBaseChange.lean, line 136. The attribute's comment: “part (1), the identity g'_!(f')^{-1} = f^{-1}g_! for the lisse-étale site, on sheaves of sets: the conjugate of the first identity along the four adjunctions, exactly as the source derives it”.

Stacks 07AT (1), the identity g'_!(f')^{-1} = f^{-1}g_!. It is the conjugate of AlgebraicGeometry.Stack.LisseEtale.isIso_sheafBaseChange along the adjointness of f^{-1} and f_*, of g_! and g^{-1}, and of their primed versions.

noncomputable def shriekBaseChangeIso :
    letI := (isContinuous_and_isCocontinuous_homFunctor_associatedTopology B S hS f
      (etaleTopology B)).1
    letI := (isContinuous_and_isCocontinuous_homFunctor_associatedTopology B S hS f
      (etaleTopology B)).2
    letI := isContinuous_subsiteFunctor_topology.{u, w} B S hS f hf
    letI := isCocontinuous_subsiteFunctor_topology.{u, w} B S hS f hf
    (SubsitePushforward.subsiteFunctor f.hom.hom.toFunctor (smoothObject.{u, w} B S hS 𝒳)
          (smoothObject_map.{u, w} B S hS f hf)).sheafPushforwardContinuous (Type (u + 1))
          (topology.{u, w} B S hS 𝒳) (topology.{u, w} B S hS 𝒴) ⋙
        setsShriek B S hS 𝒳 ≅
      setsShriek B S hS 𝒴 ⋙ f.hom.hom.toFunctor.sheafPushforwardContinuous (Type (u + 1))
        (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
        (associatedTopology B S hS 𝒴.val.val.p (etaleTopology B))

AlgebraicGeometry.Stack.FlatFppf.isIso_sheafBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteSheafPushforwardBaseChange.lean, line 214. The attribute's comment: “part (2), the identity f'_*(g')^{-1} = g^{-1}f_* for the flat-fppf site, on sheaves of sets and natural in the object of the flat-fppf site of 𝒴: the canonical map of Sites, Section 06UM, which is CategoryTheory.SubsitePushforward.subsiteRanBaseChange at the square of f, its restriction f' and the two inclusions, is invertible. The site functor and its continuity and cocontinuity are registered in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfSiteFunctor.lean”.

Stacks 07AT (2), the identity f'_*(g')^{-1} = g^{-1}f_*. For a flat 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks, the canonical map of Sites, Section 06UM from the restriction along the inclusion g of the flat-fppf site of 𝒴 of the pushforward along f, to the pushforward along the restriction f' of the restriction along the inclusion g' of the flat-fppf site of 𝒳, is an isomorphism of functors on sheaves of sets.

theorem isIso_sheafBaseChange :
    IsIso (SubsitePushforward.subsiteSheafBaseChange.{_, _, _, _, u + 1} f.hom.hom.toFunctor
      (objectProperty B S hS 𝒳) (flatObject_map B S hS f hf)
      (associatedTopology B S hS 𝒳.val.val.p B.topology)
      (associatedTopology B S hS 𝒴.val.val.p B.topology)
      (topology B S hS 𝒳) (topology B S hS 𝒴)
      (isContinuous_and_isCocontinuous_homFunctor_associatedTopology B S hS f B.topology).2
      (isCocontinuous_subsiteFunctor_topology B S hS f hf)
      (isContinuous_inclusion_topology B S hS 𝒳)
      (isContinuous_inclusion_topology B S hS 𝒴))

AlgebraicGeometry.Stack.FlatFppf.shriekBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteSheafPushforwardBaseChange.lean, line 247. The attribute's comment: “part (2), the identity g'_!(f')^{-1} = f^{-1}g_! for the flat-fppf site, on sheaves of sets: the conjugate of the first identity along the four adjunctions, exactly as the source derives it”.

Stacks 07AT (2), the identity g'_!(f')^{-1} = f^{-1}g_!. It is the conjugate of AlgebraicGeometry.Stack.FlatFppf.isIso_sheafBaseChange along the adjointness of f^{-1} and f_*, of g_! and g^{-1}, and of their primed versions. The two lower-shriek adjunctions are the ones of Stacks 0788 already in the tree.

noncomputable def shriekBaseChangeIso :
    letI := (isContinuous_and_isCocontinuous_homFunctor_associatedTopology B S hS f
      B.topology).1
    letI := (isContinuous_and_isCocontinuous_homFunctor_associatedTopology B S hS f
      B.topology).2
    letI := isContinuous_subsiteFunctor_topology B S hS f hf
    letI := isCocontinuous_subsiteFunctor_topology B S hS f hf
    (SubsitePushforward.subsiteFunctor f.hom.hom.toFunctor (objectProperty B S hS 𝒳)
          (flatObject_map B S hS f hf)).sheafPushforwardContinuous (Type (u + 1))
          (topology B S hS 𝒳) (topology B S hS 𝒴) ⋙
        setsShriek B S hS 𝒳 ≅
      setsShriek B S hS 𝒴 ⋙ f.hom.hom.toFunctor.sheafPushforwardContinuous (Type (u + 1))
        (associatedTopology B S hS 𝒳.val.val.p B.topology)
        (associatedTopology B S hS 𝒴.val.val.p B.topology)

Tag 07AU, an equation

Tag 07AU in the Stacks Project.

CategoryTheory.SubsitePushforward.subsitePushforwardSectionsEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsitePushforwardFormula.lean, line 315.

Stacks 07AU, equation 103.15.1.1. Let f : 𝒳 ⥤ 𝒴 be a 1-morphism of categories over a base 𝒞 with 𝒴 fibred in groupoids, and let 𝒳' ⊆ 𝒳 and 𝒴' ⊆ 𝒴 be full subcategories such that f carries 𝒳' into 𝒴', so that it restricts to f' : 𝒳' ⥤ 𝒴'. Then for a presheaf ℋ on 𝒳' and an object y of 𝒴' lying over V : 𝒞,

f'_*ℋ(y) = Γ((V ×_{y, 𝒴} 𝒳)', (pr')^{-1}ℋ),

where f'_* is the right Kan extension along f'.op, the primed 2-fibre product is the full subcategory of V ×_{y, 𝒴} 𝒳 whose objects have their 𝒳-component in 𝒳', and (pr')^{-1} is restriction along the projection pr' to 𝒳'.

This is the source's equation for the lisse-étale and the flat-fppf site: no property of the subcategories beyond fullness is used, and neither the topologies nor their closure conditions enter the identification.

def subsitePushforwardSectionsEquiv (p𝒳 : 𝒳 ⥤ 𝒞) (p𝒴 : 𝒴 ⥤ 𝒞) (f : 𝒳 ⥤ 𝒴) (P : ObjectProperty 𝒳)
    {Q : ObjectProperty 𝒴} (hPQ : ∀ x : P.FullSubcategory, Q (f.obj x.obj))
    (h𝒴 : p𝒴.IsFiberedInGroupoids) (hf : f ⋙ p𝒴 = p𝒳) (c : p𝒴.ChoiceOfPullbacks)
    (y : Q.FullSubcategory) (ℋ : (P.FullSubcategory)ᵒᵖ ⥤ Type w)
    [∀ G : (P.FullSubcategory)ᵒᵖ ⥤ Type w,
      (subsiteFunctor f P hPQ).op.HasPointwiseRightKanExtension G]
    [∀ G : (P.FullSubcategory)ᵒᵖ ⥤ Type w, (P.ι ⋙ f).op.HasPointwiseRightKanExtension G] :
    ((subsiteFunctor f P hPQ).op.ran.obj ℋ).obj (op y) ≃
      Presheaf.globalSections ((primedProjection p𝒳 p𝒴 f P c y).op ⋙ ℋ)

AlgebraicGeometry.Stack.FlatFppf.sheafPrimedPushforwardSectionsEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsitePushforwardFormula.lean, line 424.

Stacks 07AU, the flat-fppf case, equation 103.15.1.1. Let f : 𝒳 ⟶ 𝒴 be a flat 1-morphism of algebraic stacks, let ℋ be a sheaf of sets on the flat-fppf site of 𝒳 and let y be a flat object of 𝒴 lying over the scheme V. The direct image of ℋ along the morphism of flat-fppf topoi induced by f has

f'_*ℋ(y) = Γ((V ×_{y, 𝒴} 𝒳)', (pr')^{-1}ℋ),

the global sections of ℋ restricted along the projection pr' of the primed 2-fibre product. The direct image is CategoryTheory.Functor.sheafPushforwardCocontinuous along the site functor of Stacks 07AT, whose cocontinuity is AlgebraicGeometry.Stack.FlatFppf.siteFunctor_isCocontinuous.

def sheafPrimedPushforwardSectionsEquiv (y : FlatFppf B S hS 𝒴)
    (ℋ : Sheaf (topology B S hS 𝒳) (Type a))
    [∀ F : (FlatFppf B S hS 𝒳)ᵒᵖ ⥤ Type a,
      (primedSiteFunctor B S hS f hf).op.HasPointwiseRightKanExtension F]
    [∀ F : (FlatFppf B S hS 𝒳)ᵒᵖ ⥤ Type a,
      (inclusion B S hS 𝒳 ⋙ f.hom.hom.toFunctor).op.HasPointwiseRightKanExtension F] :
    letI : (primedSiteFunctor B S hS f hf).IsCocontinuous
        (topology B S hS 𝒳) (topology B S hS 𝒴) :=
      siteFunctor_isCocontinuous B S hS f hf
    ((((primedSiteFunctor B S hS f hf).sheafPushforwardCocontinuous (Type a)
        (topology B S hS 𝒳) (topology B S hS 𝒴)).obj ℋ).obj.obj (op y)) ≃
      Presheaf.globalSections ((primedProjection B S hS f y).op ⋙ ℋ.obj)

AlgebraicGeometry.Stack.LisseEtale.sheafPrimedPushforwardSectionsEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsitePushforwardFormula.lean, line 513.

Stacks 07AU, the lisse-étale case, equation 103.15.1.1. Let f : 𝒳 ⟶ 𝒴 be a smooth 1-morphism of algebraic stacks, let ℋ be a sheaf of sets on the lisse-étale site of 𝒳 and let y be a smooth object of 𝒴 lying over the scheme V. The direct image of ℋ along the morphism of lisse-étale topoi induced by f has

f'_*ℋ(y) = Γ((V ×_{y, 𝒴} 𝒳)', (pr')^{-1}ℋ),

the global sections of ℋ restricted along the projection pr' of the primed 2-fibre product. The direct image is CategoryTheory.Functor.sheafPushforwardCocontinuous along the site functor of Stacks 07AT, whose cocontinuity is AlgebraicGeometry.Stack.LisseEtale.siteFunctor_isCocontinuous.

def sheafPrimedPushforwardSectionsEquiv (y : LisseEtale.{u, w} B S hS 𝒴)
    (ℋ : Sheaf (topology.{u, w} B S hS 𝒳) (Type a))
    [∀ F : (LisseEtale.{u, w} B S hS 𝒳)ᵒᵖ ⥤ Type a,
      (primedSiteFunctor.{u, w} B S hS f hf).op.HasPointwiseRightKanExtension F]
    [∀ F : (LisseEtale.{u, w} B S hS 𝒳)ᵒᵖ ⥤ Type a,
      (inclusion.{u, w} B S hS 𝒳 ⋙ f.hom.hom.toFunctor).op.HasPointwiseRightKanExtension F] :
    letI : (primedSiteFunctor.{u, w} B S hS f hf).IsCocontinuous
        (topology.{u, w} B S hS 𝒳) (topology.{u, w} B S hS 𝒴) :=
      siteFunctor_isCocontinuous.{u, w} B S hS f hf
    ((((primedSiteFunctor.{u, w} B S hS f hf).sheafPushforwardCocontinuous (Type a)
        (topology.{u, w} B S hS 𝒳) (topology.{u, w} B S hS 𝒴)).obj ℋ).obj.obj (op y)) ≃
      Presheaf.globalSections ((primedProjection B S hS f y).op ⋙ ℋ.obj)

Tag 0GR2, a lemma

Tag 0GR2 in the Stacks Project.

AlgebraicGeometry.Stack.FlatFppf.rightDerived_sheafPushforward_iso_sheafify_derivedPresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfHigherDirectImage.lean, line 74. The attribute's comment: “flat-fppf sheafification formula”.

Stacks 0GR2, the flat-fppf case. The p-th higher direct image along the morphism of flat-fppf topoi induced by a flat 1-morphism of algebraic stacks is the sheaf associated to the p-th right derived presheaf direct image, naturally in the abelian sheaf of coefficients.

The flat-fppf site of an algebraic stack is a category of type Type (u + 1) with morphisms in Type u, so it is essentially small at any coefficient universe max (u + 1) a; abelian sheaves on it then form a Grothendieck abelian category and in particular have enough injectives, which is what makes the right derived functors available.

public theorem rightDerived_sheafPushforward_iso_sheafify_derivedPresheaf (p : ℕ) :
    letI : (siteFunctor B S hS f hf).1.IsCocontinuous
        (topology B S hS 𝒳) (topology B S hS 𝒴) :=
      siteFunctor_isCocontinuous B S hS f hf
    letI : HasSheafify (topology B S hS 𝒳) AddCommGrpCat.{max (u + 1) a} :=
      Stacks.Cohomology.SiteModules.site_hasSheafify_addCommGrp
    letI : HasSheafify (topology B S hS 𝒴) AddCommGrpCat.{max (u + 1) a} :=
      Stacks.Cohomology.SiteModules.site_hasSheafify_addCommGrp
    letI : EssentiallySmall.{max (u + 1) a} (FlatFppf B S hS 𝒳) :=
      essentiallySmallSelf (FlatFppf B S hS 𝒳)
    letI := Sheaf.isGrothendieckAbelian_of_essentiallySmall
      (topology B S hS 𝒳) AddCommGrpCat.{max (u + 1) a}
    letI := IsGrothendieckAbelian.enoughInjectives
      (C := Sheaf (topology B S hS 𝒳) AddCommGrpCat.{max (u + 1) a})
    letI := Functor.sheafPushforwardCocontinuous_additive.{u + 1, u + 1, u, u, a}
      (siteFunctor B S hS f hf).1
      (topology B S hS 𝒳) (topology B S hS 𝒴)
    Nonempty
      (((siteFunctor B S hS f hf).1.sheafPushforwardCocontinuous
          AddCommGrpCat.{max (u + 1) a} (topology B S hS 𝒳)
          (topology B S hS 𝒴)).rightDerived p ≅
        Functor.derivedPresheafDirectImage.{u + 1, u + 1, u, u, a}
            (topology B S hS 𝒳) (siteFunctor B S hS f hf).1 p ⋙
          presheafToSheaf (topology B S hS 𝒴) AddCommGrpCat.{max (u + 1) a})

AlgebraicGeometry.Stack.FlatFppf.rightDerived_sheafPushforward_iso_sheafify_fibreCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfHigherDirectImageFibre.lean, line 73. The attribute's comment: “flat-fppf case: Rᵖf'_*ℋ is the sheaf associated to y ↦ Hᵖ((V ×_y 𝒳)', pr'⁻¹ℋ)”.

Stacks 0GR2, the flat-fppf case. Let f : 𝒳 ⟶ 𝒴 be a flat 1-morphism of algebraic stacks and f' the induced morphism of flat-fppf topoi. For every p and every abelian sheaf ℋ on 𝒳_{flat,fppf},

Rᵖ f'_* ℋ = sheaf associated to y ↦ Hᵖ((V ×_{y, 𝒴} 𝒳)', (pr')⁻¹ ℋ).

Precisely: Rᵖ f'_* is the sheafification of the presheaf-valued functor derivedPresheafDirectImage, and for every object y of 𝒴_{flat,fppf} the value at y of that presheaf is Hᵖ of the fibre site (V ×_{y, 𝒴} 𝒳)' — the pairs (x, φ : f(x) ⟶ y), i.e. the localization of 𝒳_{flat,fppf} at (f')⁻¹ h_y — with coefficients in the restriction (pr')⁻¹ ℋ, both naturally in ℋ.

public theorem rightDerived_sheafPushforward_iso_sheafify_fibreCohomology (p : ℕ) :
    letI : (siteFunctor.{u, w} B S hS f hf).1.IsCocontinuous
        (topology.{u, w} B S hS 𝒳) (topology.{u, w} B S hS 𝒴) :=
      siteFunctor_isCocontinuous.{u, w} B S hS f hf
    letI : HasSheafify (topology.{u, w} B S hS 𝒳) AddCommGrpCat.{max (u + 1) a} :=
      Stacks.Cohomology.SiteModules.site_hasSheafify_addCommGrp
    letI : HasSheafify (topology.{u, w} B S hS 𝒴) AddCommGrpCat.{max (u + 1) a} :=
      Stacks.Cohomology.SiteModules.site_hasSheafify_addCommGrp
    letI : EssentiallySmall.{max (u + 1) a} (FlatFppf.{u, w} B S hS 𝒳) :=
      essentiallySmallSelf (FlatFppf.{u, w} B S hS 𝒳)
    letI := Sheaf.isGrothendieckAbelian_of_essentiallySmall
      (topology.{u, w} B S hS 𝒳) AddCommGrpCat.{max (u + 1) a}
    letI := IsGrothendieckAbelian.enoughInjectives
      (C := Sheaf (topology.{u, w} B S hS 𝒳) AddCommGrpCat.{max (u + 1) a})
    letI := Functor.sheafPushforwardCocontinuous_additive.{u + 1, u + 1, u, u, a}
      (siteFunctor.{u, w} B S hS f hf).1
      (topology.{u, w} B S hS 𝒳) (topology.{u, w} B S hS 𝒴)
    Nonempty
        (((siteFunctor.{u, w} B S hS f hf).1.sheafPushforwardCocontinuous
            AddCommGrpCat.{max (u + 1) a} (topology.{u, w} B S hS 𝒳)
            (topology.{u, w} B S hS 𝒴)).rightDerived p ≅
          Functor.derivedPresheafDirectImage.{u + 1, u + 1, u, u, a}
              (topology.{u, w} B S hS 𝒳) (siteFunctor.{u, w} B S hS f hf).1 p ⋙
            presheafToSheaf (topology.{u, w} B S hS 𝒴) AddCommGrpCat.{max (u + 1) a}) ∧
      ∀ y : FlatFppf.{u, w} B S hS 𝒴,
        letI := Stacks.Cohomology.SiteModules.site_hasSheafify_addCommGrp.{u + 1, u, max (u + 1) a}
          (J := fibreTopology (topology.{u, w} B S hS 𝒳) (siteFunctor.{u, w} B S hS f hf).1 y)
        letI := Stacks.Cohomology.SiteModules.site_hasExt_addCommGrp.{u + 1, u, max (u + 1) a}
          (J := fibreTopology (topology.{u, w} B S hS 𝒳) (siteFunctor.{u, w} B S hS f hf).1 y)
        Nonempty
          (Functor.derivedPresheafDirectImage.{u + 1, u + 1, u, u, a}
                (topology.{u, w} B S hS 𝒳) (siteFunctor.{u, w} B S hS f hf).1 p ⋙
              (evaluation (FlatFppf.{u, w} B S hS 𝒴)ᵒᵖ AddCommGrpCat.{max (u + 1) a}).obj
                (op y) ≅
            fibreRestriction.{u + 1, u + 1, u, a} (topology.{u, w} B S hS 𝒳)
                (siteFunctor.{u, w} B S hS f hf).1 y ⋙
              Sheaf.functorH.{max (u + 1) a, max (u + 1) a, u, u + 1}
                (fibreTopology (topology.{u, w} B S hS 𝒳) (siteFunctor.{u, w} B S hS f hf).1 y)
                p)

AlgebraicGeometry.Stack.LisseEtale.rightDerived_sheafPushforward_iso_sheafify_derivedPresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleHigherDirectImage.lean, line 81. The attribute's comment: “lisse-étale sheafification formula”.

Stacks 0GR2, the lisse-étale case. The p-th higher direct image along the morphism of lisse-étale topoi induced by a smooth 1-morphism of algebraic stacks is the sheaf associated to the p-th right derived presheaf direct image, naturally in the abelian sheaf of coefficients.

The lisse-étale site of an algebraic stack is a category of type Type (u + 1) with morphisms in Type u, so it is essentially small at any coefficient universe max (u + 1) a; abelian sheaves on it then form a Grothendieck abelian category and in particular have enough injectives, which is what makes the right derived functors available.

public theorem rightDerived_sheafPushforward_iso_sheafify_derivedPresheaf (p : ℕ) :
    letI : (siteFunctor.{u, w} B S hS f hf).1.IsCocontinuous
        (topology.{u, w} B S hS 𝒳) (topology.{u, w} B S hS 𝒴) :=
      siteFunctor_isCocontinuous.{u, w} B S hS f hf
    letI : HasSheafify (topology.{u, w} B S hS 𝒳) AddCommGrpCat.{max (u + 1) a} :=
      Stacks.Cohomology.SiteModules.site_hasSheafify_addCommGrp
    letI : HasSheafify (topology.{u, w} B S hS 𝒴) AddCommGrpCat.{max (u + 1) a} :=
      Stacks.Cohomology.SiteModules.site_hasSheafify_addCommGrp
    letI : EssentiallySmall.{max (u + 1) a} (LisseEtale.{u, w} B S hS 𝒳) :=
      essentiallySmallSelf (LisseEtale.{u, w} B S hS 𝒳)
    letI := Sheaf.isGrothendieckAbelian_of_essentiallySmall
      (topology.{u, w} B S hS 𝒳) AddCommGrpCat.{max (u + 1) a}
    letI := IsGrothendieckAbelian.enoughInjectives
      (C := Sheaf (topology.{u, w} B S hS 𝒳) AddCommGrpCat.{max (u + 1) a})
    letI := Functor.sheafPushforwardCocontinuous_additive.{u + 1, u + 1, u, u, a}
      (siteFunctor.{u, w} B S hS f hf).1
      (topology.{u, w} B S hS 𝒳) (topology.{u, w} B S hS 𝒴)
    Nonempty
      (((siteFunctor.{u, w} B S hS f hf).1.sheafPushforwardCocontinuous
          AddCommGrpCat.{max (u + 1) a} (topology.{u, w} B S hS 𝒳)
          (topology.{u, w} B S hS 𝒴)).rightDerived p ≅
        Functor.derivedPresheafDirectImage.{u + 1, u + 1, u, u, a}
            (topology.{u, w} B S hS 𝒳) (siteFunctor.{u, w} B S hS f hf).1 p ⋙
          presheafToSheaf (topology.{u, w} B S hS 𝒴) AddCommGrpCat.{max (u + 1) a})

AlgebraicGeometry.Stack.LisseEtale.rightDerived_sheafPushforward_iso_sheafify_fibreCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleHigherDirectImageFibre.lean, line 73. The attribute's comment: “lisse-étale case: Rᵖf'_*ℋ is the sheaf associated to y ↦ Hᵖ((V ×_y 𝒳)', pr'⁻¹ℋ)”.

Stacks 0GR2, the lisse-étale case. Let f : 𝒳 ⟶ 𝒴 be a smooth 1-morphism of algebraic stacks and f' the induced morphism of lisse-étale topoi. For every p and every abelian sheaf ℋ on 𝒳_{lisse,étale},

Rᵖ f'_* ℋ = sheaf associated to y ↦ Hᵖ((V ×_{y, 𝒴} 𝒳)', (pr')⁻¹ ℋ).

Precisely: Rᵖ f'_* is the sheafification of the presheaf-valued functor derivedPresheafDirectImage, and for every object y of 𝒴_{lisse,étale} the value at y of that presheaf is Hᵖ of the fibre site (V ×_{y, 𝒴} 𝒳)' — the pairs (x, φ : f(x) ⟶ y), i.e. the localization of 𝒳_{lisse,étale} at (f')⁻¹ h_y — with coefficients in the restriction (pr')⁻¹ ℋ, both naturally in ℋ.

public theorem rightDerived_sheafPushforward_iso_sheafify_fibreCohomology (p : ℕ) :
    letI : (siteFunctor.{u, w} B S hS f hf).1.IsCocontinuous
        (topology.{u, w} B S hS 𝒳) (topology.{u, w} B S hS 𝒴) :=
      siteFunctor_isCocontinuous.{u, w} B S hS f hf
    letI : HasSheafify (topology.{u, w} B S hS 𝒳) AddCommGrpCat.{max (u + 1) a} :=
      Stacks.Cohomology.SiteModules.site_hasSheafify_addCommGrp
    letI : HasSheafify (topology.{u, w} B S hS 𝒴) AddCommGrpCat.{max (u + 1) a} :=
      Stacks.Cohomology.SiteModules.site_hasSheafify_addCommGrp
    letI : EssentiallySmall.{max (u + 1) a} (LisseEtale.{u, w} B S hS 𝒳) :=
      essentiallySmallSelf (LisseEtale.{u, w} B S hS 𝒳)
    letI := Sheaf.isGrothendieckAbelian_of_essentiallySmall
      (topology.{u, w} B S hS 𝒳) AddCommGrpCat.{max (u + 1) a}
    letI := IsGrothendieckAbelian.enoughInjectives
      (C := Sheaf (topology.{u, w} B S hS 𝒳) AddCommGrpCat.{max (u + 1) a})
    letI := Functor.sheafPushforwardCocontinuous_additive.{u + 1, u + 1, u, u, a}
      (siteFunctor.{u, w} B S hS f hf).1
      (topology.{u, w} B S hS 𝒳) (topology.{u, w} B S hS 𝒴)
    Nonempty
        (((siteFunctor.{u, w} B S hS f hf).1.sheafPushforwardCocontinuous
            AddCommGrpCat.{max (u + 1) a} (topology.{u, w} B S hS 𝒳)
            (topology.{u, w} B S hS 𝒴)).rightDerived p ≅
          Functor.derivedPresheafDirectImage.{u + 1, u + 1, u, u, a}
              (topology.{u, w} B S hS 𝒳) (siteFunctor.{u, w} B S hS f hf).1 p ⋙
            presheafToSheaf (topology.{u, w} B S hS 𝒴) AddCommGrpCat.{max (u + 1) a}) ∧
      ∀ y : LisseEtale.{u, w} B S hS 𝒴,
        letI := Stacks.Cohomology.SiteModules.site_hasSheafify_addCommGrp.{u + 1, u, max (u + 1) a}
          (J := fibreTopology (topology.{u, w} B S hS 𝒳) (siteFunctor.{u, w} B S hS f hf).1 y)
        letI := Stacks.Cohomology.SiteModules.site_hasExt_addCommGrp.{u + 1, u, max (u + 1) a}
          (J := fibreTopology (topology.{u, w} B S hS 𝒳) (siteFunctor.{u, w} B S hS f hf).1 y)
        Nonempty
          (Functor.derivedPresheafDirectImage.{u + 1, u + 1, u, u, a}
                (topology.{u, w} B S hS 𝒳) (siteFunctor.{u, w} B S hS f hf).1 p ⋙
              (evaluation (LisseEtale.{u, w} B S hS 𝒴)ᵒᵖ AddCommGrpCat.{max (u + 1) a}).obj
                (op y) ≅
            fibreRestriction.{u + 1, u + 1, u, a} (topology.{u, w} B S hS 𝒳)
                (siteFunctor.{u, w} B S hS f hf).1 y ⋙
              Sheaf.functorH.{max (u + 1) a, max (u + 1) a, u, u + 1}
                (fibreTopology (topology.{u, w} B S hS 𝒳) (siteFunctor.{u, w} B S hS f hf).1 y)
                p)

Tag 0GR3, a lemma

Tag 0GR3 in the Stacks Project.

AlgebraicGeometry.Stack.LisseEtale.isIso_baseChangeMapPlus_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteDerivedBaseChangeMap.lean, line 186. The attribute's comment: “the lisse-étale case: the canonical base change map g⁻¹ Rf_ ℱ ⟶ Rf'_ (g')⁻¹ ℱ is an isomorphism for every abelian sheaf ℱ on 𝒳_étale, in D⁺ for any model of the derived categories. The map is Stacks.Cohomology.BoundedBelowComplexes.baseChangeMapPlus (the identification g⁻¹ ∘ Rf_ = R(g⁻¹ ∘ f_) for the exact g⁻¹, the derived map of the canonical map g⁻¹f_ ⟶ f'_(g')⁻¹ of Sites 06UM, and the canonical comparison R(f'_ ∘ (g')⁻¹) ⟶ Rf'_ ∘ (g')⁻¹ of 05T2) at ℱ in degree zero. Nothing is assumed: the degree-zero isomorphism is 07AT (AlgebraicGeometry.Stack.LisseEtale.isIso_abelianSheafBaseChange) and the acyclicity of restricted injectives for f'_* is proved by descent (AlgebraicGeometry.Stack.LisseEtale.isZero_rightDerived_restriction_of_injective)”.

Stacks 0GR3, the lisse-étale case. Let f : 𝒳 ⟶ 𝒴 be a smooth 1-morphism of algebraic stacks, f' its restriction to the lisse-étale sites (Stacks 07AT) and g, g' the inclusions of the lisse-étale sites of 𝒴 and of 𝒳. For every abelian sheaf ℱ on 𝒳_étale the canonical base change map

g⁻¹ Rf_* ℱ ⟶ Rf'_* (g')⁻¹ ℱ

is an isomorphism in the bounded below derived category of abelian sheaves on the lisse-étale site of 𝒴, for any model of the derived categories. The map is Stacks.Cohomology.BoundedBelowComplexes.baseChangeMapPlus at the canonical map g⁻¹f_* ⟶ f'_*(g')⁻¹ of Sites, Section 06UM, evaluated at ℱ placed in degree zero.

theorem isIso_baseChangeMapPlus_app
    (ℱ : Sheaf (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B)) AddCommGrpCat.{u + 1}) :
    haveI := isCocontinuous_subsiteFunctor.{u, w} B S hS f hf
    haveI := (isContinuous_and_isCocontinuous_homFunctor_associatedTopology B S hS f
      (etaleTopology B)).2
    letI := Functor.sheafPushforwardCocontinuous_additive.{u + 1, u + 1, u, u, u + 1}
      f.hom.hom.toFunctor (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
      (associatedTopology B S hS 𝒴.val.val.p (etaleTopology B))
    letI := Functor.sheafPushforwardCocontinuous_additive.{u + 1, u + 1, u, u, u + 1}
      (SubsitePushforward.subsiteFunctor f.hom.hom.toFunctor (smoothObject.{u, w} B S hS 𝒳)
        (smoothObject_map.{u, w} B S hS f hf))
      (inclusionTopology.{u, w} B S hS 𝒳) (inclusionTopology.{u, w} B S hS 𝒴)
    IsIso ((Stacks.Cohomology.BoundedBelowComplexes.baseChangeMapPlus
      (subsiteRestriction B S hS 𝒳.val.val.p (etaleTopology B) (smoothObject.{u, w} B S hS 𝒳))
      (subsiteRestriction B S hS 𝒴.val.val.p (etaleTopology B) (smoothObject.{u, w} B S hS 𝒴))
      (f.hom.hom.toFunctor.sheafPushforwardCocontinuous AddCommGrpCat.{u + 1}
        (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
        (associatedTopology B S hS 𝒴.val.val.p (etaleTopology B)))
      ((SubsitePushforward.subsiteFunctor f.hom.hom.toFunctor (smoothObject.{u, w} B S hS 𝒳)
        (smoothObject_map.{u, w} B S hS f hf)).sheafPushforwardCocontinuous AddCommGrpCat.{u + 1}
          (inclusionTopology.{u, w} B S hS 𝒳) (inclusionTopology.{u, w} B S hS 𝒴))
      (SubsitePushforward.subsiteAbelianSheafBaseChange.{_, _, _, _, u + 1}
        f.hom.hom.toFunctor (smoothObject.{u, w} B S hS 𝒳) (smoothObject_map.{u, w} B S hS f hf)
        (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
        (associatedTopology B S hS 𝒴.val.val.p (etaleTopology B))
        (inclusionTopology.{u, w} B S hS 𝒳) (inclusionTopology.{u, w} B S hS 𝒴))).app
      ((DerivedCategory.Plus.singleFunctor _ 0).obj ℱ))

AlgebraicGeometry.Stack.FlatFppf.isIso_baseChangeMapPlus_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteDerivedBaseChangeMap.lean, line 330. The attribute's comment: “the flat-fppf case: the canonical base change map g⁻¹ Rf_ ℱ ⟶ Rf'_ (g')⁻¹ ℱ is an isomorphism for every abelian sheaf ℱ on 𝒳_fppf, in D⁺ for any model of the derived categories. The map is Stacks.Cohomology.BoundedBelowComplexes.baseChangeMapPlus (the identification g⁻¹ ∘ Rf_ = R(g⁻¹ ∘ f_) for the exact g⁻¹, the derived map of the canonical map g⁻¹f_ ⟶ f'_(g')⁻¹ of Sites 06UM, and the canonical comparison R(f'_ ∘ (g')⁻¹) ⟶ Rf'_ ∘ (g')⁻¹ of 05T2) at ℱ in degree zero. Nothing is assumed: the degree-zero isomorphism is 07AT (AlgebraicGeometry.Stack.FlatFppf.isIso_abelianSheafBaseChange) and the acyclicity of restricted injectives for f'_* is proved by descent (AlgebraicGeometry.Stack.FlatFppf.isZero_rightDerived_restriction_of_injective)”.

Stacks 0GR3, the flat-fppf case. Let f : 𝒳 ⟶ 𝒴 be a flat 1-morphism of algebraic stacks, f' its restriction to the flat-fppf sites (Stacks 07AT) and g, g' the inclusions of the flat-fppf sites of 𝒴 and of 𝒳. For every abelian sheaf ℱ on 𝒳_fppf the canonical base change map

g⁻¹ Rf_* ℱ ⟶ Rf'_* (g')⁻¹ ℱ

is an isomorphism in the bounded below derived category of abelian sheaves on the flat-fppf site of 𝒴, for any model of the derived categories. The map is Stacks.Cohomology.BoundedBelowComplexes.baseChangeMapPlus at the canonical map g⁻¹f_* ⟶ f'_*(g')⁻¹ of Sites, Section 06UM, evaluated at ℱ placed in degree zero.

theorem isIso_baseChangeMapPlus_app
    (ℱ : Sheaf (associatedTopology B S hS 𝒳.val.val.p B.topology) AddCommGrpCat.{u + 1}) :
    haveI := isCocontinuous_subsiteFunctor B S hS f hf
    haveI := (isContinuous_and_isCocontinuous_homFunctor B S hS f).2
    letI := Functor.sheafPushforwardCocontinuous_additive.{u + 1, u + 1, u, u, u + 1}
      f.hom.hom.toFunctor (associatedTopology B S hS 𝒳.val.val.p B.topology)
      (associatedTopology B S hS 𝒴.val.val.p B.topology)
    letI := Functor.sheafPushforwardCocontinuous_additive.{u + 1, u + 1, u, u, u + 1}
      (SubsitePushforward.subsiteFunctor f.hom.hom.toFunctor (flatObject B S hS 𝒳.val)
        (flatObject_map B S hS f hf))
      (inclusionTopology B S hS 𝒳) (inclusionTopology B S hS 𝒴)
    IsIso ((Stacks.Cohomology.BoundedBelowComplexes.baseChangeMapPlus
      (subsiteRestriction B S hS 𝒳.val.val.p B.topology (flatObject B S hS 𝒳.val))
      (subsiteRestriction B S hS 𝒴.val.val.p B.topology (flatObject B S hS 𝒴.val))
      (f.hom.hom.toFunctor.sheafPushforwardCocontinuous AddCommGrpCat.{u + 1}
        (associatedTopology B S hS 𝒳.val.val.p B.topology)
        (associatedTopology B S hS 𝒴.val.val.p B.topology))
      ((SubsitePushforward.subsiteFunctor f.hom.hom.toFunctor (flatObject B S hS 𝒳.val)
        (flatObject_map B S hS f hf)).sheafPushforwardCocontinuous AddCommGrpCat.{u + 1}
          (inclusionTopology B S hS 𝒳) (inclusionTopology B S hS 𝒴))
      (SubsitePushforward.subsiteAbelianSheafBaseChange.{_, _, _, _, u + 1}
        f.hom.hom.toFunctor (flatObject B S hS 𝒳.val) (flatObject_map B S hS f hf)
        (associatedTopology B S hS 𝒳.val.val.p B.topology)
        (associatedTopology B S hS 𝒴.val.val.p B.topology)
        (inclusionTopology B S hS 𝒳) (inclusionTopology B S hS 𝒴))).app
      ((DerivedCategory.Plus.singleFunctor _ 0).obj ℱ))

AlgebraicGeometry.Stack.LisseEtale.rightDerivedPushforwardRestrictionIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteDerivedPushforwardBaseChange.lean, line 308. The attribute's comment: “the lisse-étale case, as an isomorphism of functors R^p f_ ∘ g⁻¹ ≅ (g')⁻¹ ∘ R^p f'_ in every degree rather than as invertibility of the canonical base-change map, and conditional on two things: its degree-zero case — the identification f'_(g')⁻¹ = g⁻¹f_ of Stacks 07AT (1), which rests on the instance of Stacks 07AK whose hypotheses the source declines to verify — and restriction to the subsite preserving injective abelian sheaves, which is Stacks 07AS (3)”.

Stacks 0GR3, the lisse-étale case: degree zero implies every degree. Let f : 𝒳 ⟶ 𝒴 be a smooth 1-morphism of algebraic stacks, let g⁻¹ and (g')⁻¹ be restriction of abelian sheaves to the lisse-étale sites of 𝒴 and of 𝒳, and let f_* and f'_* be the direct images along f and along its restriction f' to the lisse-étale sites. Suppose (g')⁻¹ carries injective abelian sheaves to injective ones, and that the degree-zero identification f_* ∘ g⁻¹ ≅ (g')⁻¹ ∘ f'_* of Stacks 07AT (1) holds. Then the higher direct images satisfy

R^p f_* ∘ g⁻¹ ≅ (g')⁻¹ ∘ R^p f'_*

in every degree p, which is the conclusion of Stacks 0GR3.

theorem rightDerivedPushforwardRestrictionIso (p : ℕ) :
    letI : (SubsitePushforward.subsiteFunctor f.hom.hom.toFunctor
        (smoothObject.{u, w} B S hS 𝒳)
        (smoothObject_map.{u, w} B S hS f hf)).IsContinuous
          (inclusionTopology.{u, w} B S hS 𝒳) (inclusionTopology.{u, w} B S hS 𝒴) :=
      isContinuous_subsiteFunctor.{u, w} B S hS f hf
    letI : (SubsitePushforward.subsiteFunctor f.hom.hom.toFunctor
        (smoothObject.{u, w} B S hS 𝒳)
        (smoothObject_map.{u, w} B S hS f hf)).IsCocontinuous
          (inclusionTopology.{u, w} B S hS 𝒳) (inclusionTopology.{u, w} B S hS 𝒴) :=
      isCocontinuous_subsiteFunctor.{u, w} B S hS f hf
    letI : f.hom.hom.toFunctor.IsContinuous
        (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
        (associatedTopology B S hS 𝒴.val.val.p (etaleTopology B)) :=
      (isContinuous_and_isCocontinuous_homFunctor_associatedTopology B S hS f
        (etaleTopology B)).1
    letI : f.hom.hom.toFunctor.IsCocontinuous
        (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
        (associatedTopology B S hS 𝒴.val.val.p (etaleTopology B)) :=
      (isContinuous_and_isCocontinuous_homFunctor_associatedTopology B S hS f
        (etaleTopology B)).2
    letI : (f.hom.hom.toFunctor.sheafPushforwardCocontinuous AddCommGrpCat.{u + 1}
        (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
        (associatedTopology B S hS 𝒴.val.val.p (etaleTopology B))).Additive :=
      Functor.sheafPushforwardCocontinuous_additive.{u + 1, u + 1, u, u, u + 1} _ _ _
    letI : ((SubsitePushforward.subsiteFunctor f.hom.hom.toFunctor
          (smoothObject.{u, w} B S hS 𝒳)
          (smoothObject_map.{u, w} B S hS f hf)).sheafPushforwardCocontinuous
        AddCommGrpCat.{u + 1} (inclusionTopology.{u, w} B S hS 𝒳)
        (inclusionTopology.{u, w} B S hS 𝒴)).Additive :=
      Functor.sheafPushforwardCocontinuous_additive.{u + 1, u + 1, u, u, u + 1} _ _ _
    ∀ (_ : (subsiteRestriction B S hS 𝒳.val.val.p (etaleTopology B)
          (smoothObject.{u, w} B S hS 𝒳)).PreservesInjectiveObjects)
      (_ : f.hom.hom.toFunctor.sheafPushforwardCocontinuous AddCommGrpCat.{u + 1}
            (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
            (associatedTopology B S hS 𝒴.val.val.p (etaleTopology B)) ⋙
          subsiteRestriction B S hS 𝒴.val.val.p (etaleTopology B)
            (smoothObject.{u, w} B S hS 𝒴) ≅
        subsiteRestriction B S hS 𝒳.val.val.p (etaleTopology B)
            (smoothObject.{u, w} B S hS 𝒳) ⋙
          (SubsitePushforward.subsiteFunctor f.hom.hom.toFunctor
              (smoothObject.{u, w} B S hS 𝒳)
              (smoothObject_map.{u, w} B S hS f hf)).sheafPushforwardCocontinuous
            AddCommGrpCat.{u + 1} (inclusionTopology.{u, w} B S hS 𝒳)
            (inclusionTopology.{u, w} B S hS 𝒴)),
      Nonempty
        ((f.hom.hom.toFunctor.sheafPushforwardCocontinuous AddCommGrpCat.{u + 1}
                (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
                (associatedTopology B S hS 𝒴.val.val.p (etaleTopology B))).rightDerived p ⋙
            subsiteRestriction B S hS 𝒴.val.val.p (etaleTopology B)
              (smoothObject.{u, w} B S hS 𝒴) ≅
          subsiteRestriction B S hS 𝒳.val.val.p (etaleTopology B)
              (smoothObject.{u, w} B S hS 𝒳) ⋙
            ((SubsitePushforward.subsiteFunctor f.hom.hom.toFunctor
                  (smoothObject.{u, w} B S hS 𝒳)
                  (smoothObject_map.{u, w} B S hS f hf)).sheafPushforwardCocontinuous
                AddCommGrpCat.{u + 1} (inclusionTopology.{u, w} B S hS 𝒳)
                (inclusionTopology.{u, w} B S hS 𝒴)).rightDerived p)

AlgebraicGeometry.Stack.FlatFppf.rightDerivedPushforwardRestrictionIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteDerivedPushforwardBaseChange.lean, line 678. The attribute's comment: “the flat-fppf case, as an isomorphism of functors R^p f_ ∘ g⁻¹ ≅ (g')⁻¹ ∘ R^p f'_ in every degree rather than as invertibility of the canonical base-change map, and conditional on two things: its degree-zero case — the identification f'_(g')⁻¹ = g⁻¹f_ of Stacks 07AT (2), which rests on the instance of Stacks 07AK whose hypotheses the source declines to verify — and restriction to the subsite preserving injective abelian sheaves, which is Stacks 07AS (3)”.

Stacks 0GR3, the flat-fppf case: degree zero implies every degree. Let f : 𝒳 ⟶ 𝒴 be a flat 1-morphism of algebraic stacks, let g⁻¹ and (g')⁻¹ be restriction of abelian sheaves to the flat-fppf sites of 𝒴 and of 𝒳, and let f_* and f'_* be the direct images along f and along its restriction f' to the flat-fppf sites. Suppose (g')⁻¹ carries injective abelian sheaves to injective ones, and that the degree-zero identification f_* ∘ g⁻¹ ≅ (g')⁻¹ ∘ f'_* of Stacks 07AT (2) holds. Then the higher direct images satisfy

R^p f_* ∘ g⁻¹ ≅ (g')⁻¹ ∘ R^p f'_*

in every degree p, which is the conclusion of Stacks 0GR3.

theorem rightDerivedPushforwardRestrictionIso (p : ℕ) :
    letI : (SubsitePushforward.subsiteFunctor f.hom.hom.toFunctor
        (flatObject B S hS 𝒳.val)
        (flatObject_map B S hS f hf)).IsContinuous
          (inclusionTopology B S hS 𝒳) (inclusionTopology B S hS 𝒴) :=
      isContinuous_subsiteFunctor B S hS f hf
    letI : (SubsitePushforward.subsiteFunctor f.hom.hom.toFunctor
        (flatObject B S hS 𝒳.val)
        (flatObject_map B S hS f hf)).IsCocontinuous
          (inclusionTopology B S hS 𝒳) (inclusionTopology B S hS 𝒴) :=
      isCocontinuous_subsiteFunctor B S hS f hf
    letI : f.hom.hom.toFunctor.IsContinuous
        (associatedTopology B S hS 𝒳.val.val.p B.topology)
        (associatedTopology B S hS 𝒴.val.val.p B.topology) :=
      (isContinuous_and_isCocontinuous_homFunctor B S hS f).1
    letI : f.hom.hom.toFunctor.IsCocontinuous
        (associatedTopology B S hS 𝒳.val.val.p B.topology)
        (associatedTopology B S hS 𝒴.val.val.p B.topology) :=
      (isContinuous_and_isCocontinuous_homFunctor B S hS f).2
    letI : (f.hom.hom.toFunctor.sheafPushforwardCocontinuous AddCommGrpCat.{u + 1}
        (associatedTopology B S hS 𝒳.val.val.p B.topology)
        (associatedTopology B S hS 𝒴.val.val.p B.topology)).Additive :=
      Functor.sheafPushforwardCocontinuous_additive.{u + 1, u + 1, u, u, u + 1} _ _ _
    letI : ((SubsitePushforward.subsiteFunctor f.hom.hom.toFunctor
          (flatObject B S hS 𝒳.val)
          (flatObject_map B S hS f hf)).sheafPushforwardCocontinuous
        AddCommGrpCat.{u + 1} (inclusionTopology B S hS 𝒳)
        (inclusionTopology B S hS 𝒴)).Additive :=
      Functor.sheafPushforwardCocontinuous_additive.{u + 1, u + 1, u, u, u + 1} _ _ _
    ∀ (_ : (subsiteRestriction B S hS 𝒳.val.val.p B.topology
          (flatObject B S hS 𝒳.val)).PreservesInjectiveObjects)
      (_ : f.hom.hom.toFunctor.sheafPushforwardCocontinuous AddCommGrpCat.{u + 1}
            (associatedTopology B S hS 𝒳.val.val.p B.topology)
            (associatedTopology B S hS 𝒴.val.val.p B.topology) ⋙
          subsiteRestriction B S hS 𝒴.val.val.p B.topology
            (flatObject B S hS 𝒴.val) ≅
        subsiteRestriction B S hS 𝒳.val.val.p B.topology
            (flatObject B S hS 𝒳.val) ⋙
          (SubsitePushforward.subsiteFunctor f.hom.hom.toFunctor
              (flatObject B S hS 𝒳.val)
              (flatObject_map B S hS f hf)).sheafPushforwardCocontinuous
            AddCommGrpCat.{u + 1} (inclusionTopology B S hS 𝒳)
            (inclusionTopology B S hS 𝒴)),
      Nonempty
        ((f.hom.hom.toFunctor.sheafPushforwardCocontinuous AddCommGrpCat.{u + 1}
                (associatedTopology B S hS 𝒳.val.val.p B.topology)
                (associatedTopology B S hS 𝒴.val.val.p B.topology)).rightDerived p ⋙
            subsiteRestriction B S hS 𝒴.val.val.p B.topology
              (flatObject B S hS 𝒴.val) ≅
          subsiteRestriction B S hS 𝒳.val.val.p B.topology
              (flatObject B S hS 𝒳.val) ⋙
            ((SubsitePushforward.subsiteFunctor f.hom.hom.toFunctor
                  (flatObject B S hS 𝒳.val)
                  (flatObject_map B S hS f hf)).sheafPushforwardCocontinuous
                AddCommGrpCat.{u + 1} (inclusionTopology B S hS 𝒳)
                (inclusionTopology B S hS 𝒴)).rightDerived p)

Sources

• Section 103.15, Tag 0GR1
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.FlatFppf.siteFunctor · AlgebraicGeometry.Stack.FlatFppf.siteFunctor_isContinuous · AlgebraicGeometry.Stack.FlatFppf.siteFunctor_isCocontinuous · AlgebraicGeometry.Stack.LisseEtale.siteFunctor · AlgebraicGeometry.Stack.LisseEtale.siteFunctor_isContinuous · AlgebraicGeometry.Stack.LisseEtale.siteFunctor_isCocontinuous · AlgebraicGeometry.Stack.FlatFppf.primedPushforwardAmbientEquiv' · AlgebraicGeometry.Stack.LisseEtale.primedPushforwardAmbientEquiv'

Section103.16 Quasi-coherent modules and the lisse-étale and flat-fppf sites#

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

Tag 07AZ, a lemma

Tag 07AZ in the Stacks Project.

AlgebraicGeometry.Stack.isQuasicoherentOnSite_of_isSmooth_jointlySurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/JointlySurjectiveDescent.lean, line 317. The attribute's comment: “part (1): the smooth family on the étale site”.

Stacks 07AZ, part (1). Let f j : 𝒵 j ⟶ 𝒳 be a family of smooth 1-morphisms of algebraic stacks over S which is jointly surjective, that is |𝒳| = ⋃ j, |f j|(|𝒵 j|) for the points of Stacks 04XG, and let M be a sheaf of 𝒪_𝒳-modules on 𝒳_étale. If every inverse image f j^{-1} M is quasi-coherent, then so is M.

Joint surjectivity turns every object of 𝒳 into one covered, étale-locally, by images of objects of the members of the family; quasi-coherence of the inverse images presents M globally on a covering of each of those images, and quasi-coherence is local.

theorem isQuasicoherentOnSite_of_isSmooth_jointlySurjective
    (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)))
    (M : SheafOfModules.{u} (ringStructureSheafCore B S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids (B.baseTopology .etale)
      (B.baseTopology_le_topology .etale)))
    (hM : ∀ j, ((familyModulePullback B S hS 𝒵 f (B.baseTopology .etale)
      (B.baseTopology_le_topology .etale) j).obj M).IsQuasicoherentOnSite) :
    M.IsQuasicoherentOnSite

AlgebraicGeometry.Stack.isQuasicoherentOnSite_of_isFlat_isLfp_jointlySurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/JointlySurjectiveDescent.lean, line 341. The attribute's comment: “part (2): the flat, locally finitely presented family on the fppf site”.

Stacks 07AZ, part (2). Let f j : 𝒵 j ⟶ 𝒳 be a family of 1-morphisms of algebraic stacks over S which are each flat and locally of finite presentation and which is jointly surjective, that is |𝒳| = ⋃ j, |f j|(|𝒵 j|), and let M be a sheaf of 𝒪_𝒳-modules on 𝒳_fppf. If every inverse image f j^{-1} M is quasi-coherent, then so is M.

This is the argument of part (1) with "smooth" replaced by "flat and locally of finite presentation" and the étale covering of Stacks 06XH by the fppf covering of Stacks 07AN.

theorem isQuasicoherentOnSite_of_isFlat_isLfp_jointlySurjective
    (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)))
    (M : SheafOfModules.{u} (ringStructureSheafCore B S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids B.topology le_rfl))
    (hM : ∀ j, ((familyModulePullback B S hS 𝒵 f B.topology le_rfl j).obj
      M).IsQuasicoherentOnSite) :
    M.IsQuasicoherentOnSite

Tag 07B0, a lemma

Tag 07B0 in the Stacks Project.

AlgebraicGeometry.Stack.LisseEtale.isQuasicoherentClause_fppf_moduleLowerShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LowerShriekQuasicoherent.lean, line 215. The attribute's comment: “part (1): for every quasi-coherent module H on the lisse-étale site of an algebraic stack 𝒳, g_!H is a quasi-coherent module on 𝒳 — an fppf sheaf, quasi-coherent on (𝒳_fppf, O_𝒳) (the 06WG notion, read through the fppf clause of 0EM8)”.

Let 𝒳 be an algebraic stack and let H be a quasi-coherent O_{𝒳_{lisse,étale}}-module on the lisse-étale site of 𝒳. Then g_!H is a quasi-coherent module on 𝒳, where g_! is the lower shriek on sheaves of modules of Stacks 0789 (1).

A quasi-coherent module on 𝒳 is one in the sense of Stacks 06WG: a sheaf for the fppf topology which is quasi-coherent on (𝒳_fppf, O_𝒳). The conclusion is this property of the underlying presheaf of modules of the sheaf g_!H on 𝒳_étale, in the form of AlgebraicGeometry.FibredSite.IsQuasicoherentClause at .fppf (Stacks 0EM8).

theorem isQuasicoherentClause_fppf_moduleLowerShriek
    (H : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf (ringedTopos.{u, t} B S hS 𝒳
      (closedUnderSmoothMorphisms.{u, t} B S hS 𝒳)).O))
    (hH : H.IsQuasicoherentOnSite) :
    FibredSite.IsQuasicoherentClause B S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids .fppf
      ((moduleLowerShriek.{u, t} B S hS 𝒳).obj H).val

AlgebraicGeometry.Stack.FlatFppf.isQuasicoherentOnSite_moduleLowerShriek_of_isQuasicoherentOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LowerShriekQuasicoherent.lean, line 309. The attribute's comment: “part (2): for every quasi-coherent module H on the flat-fppf site of an algebraic stack 𝒳, g_!H is a quasi-coherent module on 𝒳, i.e. quasi-coherent on (𝒳_fppf, O_𝒳) (06WG)”.

Let 𝒳 be an algebraic stack and let H be a quasi-coherent O_{𝒳_{flat,fppf}}-module on the flat-fppf site of 𝒳. Then g_!H is a quasi-coherent module on 𝒳, where g_! is the lower shriek on sheaves of modules of Stacks 0789 (2): it is quasi-coherent on (𝒳_fppf, O_𝒳), the ambient site being 𝒳_fppf itself, which is quasi-coherence of a module on 𝒳 in the sense of Stacks 06WG.

theorem isQuasicoherentOnSite_moduleLowerShriek_of_isQuasicoherentOnSite
    (H : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf (subsiteRingedTopos B S hS
      𝒳.val.val.p 𝒳.val.isFiberedInGroupoids B.topology le_rfl (objectProperty B S hS 𝒳)).O))
    (hH : H.IsQuasicoherentOnSite) :
    ((moduleLowerShriek B S hS 𝒳).obj H).IsQuasicoherentOnSite

AlgebraicGeometry.Stack.LisseEtale.isQuasicoherentOnSite_moduleLowerShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/SubsiteLowerShriekQuasicoherent.lean, line 228. The attribute's comment: “the lisse-étale clause, for an H that has a global presentation, with conclusion quasi-coherence on 𝒳_étale. Three conditions: (a) H has a global presentation rather than being quasi-coherent — the source's reduction to this case, through 07AT, 07AZ and the base-change isomorphism for g_! on sheaves of modules, is not in the library; (b) 078A, g_!O = O_𝒳, as a hypothesis, which this library proves only from a localisation hypothesis with no producer; (c) essential smallness of the category underlying the stack. Passing from 𝒳_étale to 𝒳_fppf, the source's last sentence, is 0EM8 over an input left open there”.

Stacks 07B0 (1) for an H with a global presentation: if H is an O_{𝒳_{lisse,étale}}-module with a global presentation, then g_!H is quasi-coherent on (𝒳_étale, O_𝒳).

The three conditions are the ones named in the tag; see the module documentation for where each comes from and what is missing without it.

theorem isQuasicoherentOnSite_moduleLowerShriek
    (hO : IsIso (unitLowerShriekMap.{u, t} B S hS 𝒳))
    (H : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf (ringedTopos.{u, t} B S hS 𝒳
      (closedUnderSmoothMorphisms.{u, t} B S hS 𝒳)).O))
    (hH : H.IsPresentedByGlobalSections) :
    ((moduleLowerShriek.{u, t} B S hS 𝒳).obj H).IsQuasicoherentOnSite

AlgebraicGeometry.Stack.FlatFppf.isQuasicoherentOnSite_moduleLowerShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/SubsiteLowerShriekQuasicoherent.lean, line 261. The attribute's comment: “the flat-fppf clause, for an H that has a global presentation. Three conditions: (a) H has a global presentation rather than being quasi-coherent — the source's reduction to this case, through 07AT, 07AZ and the base-change isomorphism for g_! on sheaves of modules, is not in the library; (b) 078A, g_!O = O_𝒳, as a hypothesis, which this library proves only from a localisation hypothesis with no producer; (c) essential smallness of the category underlying the stack. The conclusion is the clause's own: quasi-coherence on 𝒳_fppf, i.e. of a module on 𝒳 in the sense of 06WG”.

Stacks 07B0 (2) for an H with a global presentation: if H is an O_{𝒳_{flat,fppf}}-module with a global presentation, then g_!H is a quasi-coherent module on 𝒳, that is, quasi-coherent on (𝒳_fppf, O_𝒳).

Here the ambient site is 𝒳_fppf already, so the conclusion is quasi-coherence of a module on 𝒳 in the sense of Stacks 06WG and nothing further is needed — the source's "In case (2) we are done". The three conditions are the ones named in the tag.

theorem isQuasicoherentOnSite_moduleLowerShriek
    (hO : IsIso (unitLowerShriekMap B S hS 𝒳))
    (H : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf (subsiteRingedTopos B S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids B.topology le_rfl (objectProperty B S hS 𝒳)).O))
    (hH : H.IsPresentedByGlobalSections) :
    ((moduleLowerShriek B S hS 𝒳).obj H).IsQuasicoherentOnSite

Tag 07B1, a lemma

Tag 07B1 in the Stacks Project.

AlgebraicGeometry.Stack.FlatFppf.quasicoherentEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatFppfQuasicoherentEquivalence.lean, line 125. The attribute's comment: “part (2)(a): g^{-1} and g_! are mutually inverse functors between QCoh(𝒪_𝒳) and QCoh(𝒳_{flat,fppf}, 𝒪_{𝒳_{flat,fppf}})”.

For an algebraic stack 𝒳, the functors g^{-1} and g_! are mutually inverse equivalences between QCoh(𝒪_𝒳) and QCoh(𝒳_{flat,fppf}, 𝒪_{𝒳_{flat,fppf}}). The functor of the equivalence is g^{-1} and its inverse is g_!, both on the nose (quasicoherentEquivalence_functor_comp_ι, quasicoherentEquivalence_inverse_comp_ι); the unit is the inverse of the counit g_!g^{-1}𝓖 ⟶ 𝓖 of g_! ⊣ g^{-1}, an isomorphism on quasi-coherent modules, and the counit is the inverse of its unit ℋ ⟶ g^{-1}g_!ℋ.

def quasicoherentEquivalence :
    AlgebraicStacks.quasicoherentModules B S hS 𝒳 ≌ quasicoherentSubsiteModules B S hS 𝒳

AlgebraicGeometry.Stack.FlatFppf.isQuasicoherentOnSite_modulePullback_of_lqcohSheafFbc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatFppfQuasicoherentEquivalence.lean, line 147. The attribute's comment: “part (2)(b): for F in LQCoh^fbc(𝒪_𝒳), g^{-1}F is in QCoh(𝒪_{𝒳_{flat,fppf}})”.

For 𝓕 in LQCoh^fbc(𝒪_𝒳), the module g^{-1}𝓕 on the flat-fppf site is quasi-coherent.

theorem isQuasicoherentOnSite_modulePullback_of_lqcohSheafFbc (F : fppfModules B S hS 𝒳)
    (hF : lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳 F) :
    ((modulePullback B S hS 𝒳).obj F).IsQuasicoherentOnSite

AlgebraicGeometry.Stack.FlatFppf.coheratorIsoLowerShriekModulePullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatFppfQuasicoherentEquivalence.lean, line 200. The attribute's comment: “part (2)(c): Q(F) = g_! g^{-1} F for F in LQCoh^fbc(𝒪_𝒳), Q the coherator of 0778”.

For 𝓕 in LQCoh^fbc(𝒪_𝒳), Q(𝓕) = g_!g^{-1}𝓕, naturally in 𝓕, where Q : LQCoh^fbc(𝒪_𝒳) ⥤ QCoh(𝒪_𝒳) is the coherator of Stacks 0778 (AlgebraicGeometry.Stack.AlgebraicStacks.lqcohFbcCoherator). The isomorphism at 𝓕 is g_!g^{-1} of the adjunction map Q(𝓕) ⟶ 𝓕, preceded by the inverse of the counit g_!g^{-1}Q(𝓕) ⟶ Q(𝓕).

def coheratorIsoLowerShriekModulePullback :
    AlgebraicStacks.lqcohFbcCoherator B E h S hS 𝒳 ⋙
        AlgebraicStacks.quasicoherentInclusion B S hS 𝒳 ≅
      (lqcohSheafFbcFppfModules.{u, w, u} B E h S hS 𝒳).ι ⋙ modulePullback B S hS 𝒳 ⋙
        moduleLowerShriek B S hS 𝒳

AlgebraicGeometry.Stack.LisseEtale.quasicoherentEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LisseEtaleQuasicoherentEquivalence.lean, line 193. The attribute's comment: “part (1)(a): g^{-1} and g_! are mutually inverse functors between QCoh(𝒪_𝒳) and QCoh(𝒳_{lisse,étale}, 𝒪_{𝒳_{lisse,étale}})”.

Stacks 07B1 (1)(a). For an algebraic stack 𝒳, the functors g^{-1} and g_! are mutually inverse equivalences between QCoh(𝒪_𝒳) and QCoh(𝒳_{lisse,étale}, 𝒪_{𝒳_{lisse,étale}}). The functor of the equivalence is g^{-1} and its inverse is g_!, both on the nose (quasicoherentEquivalence_functor_comp_ι, quasicoherentEquivalence_inverse_comp_ι, fppfModuleLowerShriek_obj_val); the unit is the inverse of the counit g_!g^{-1}𝓖 ⟶ 𝓖 of g_! ⊣ g^{-1}, an isomorphism on quasi-coherent modules, and the counit is the inverse of its unit ℋ ⟶ g^{-1}g_!ℋ.

def quasicoherentEquivalence :
    AlgebraicStacks.quasicoherentModules B S hS 𝒳 ≌ quasicoherentSubsiteModules.{u, w} B S hS 𝒳

AlgebraicGeometry.Stack.LisseEtale.isQuasicoherentOnSite_modulePullback_of_lqcohSheafFbc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LisseEtaleQuasicoherentEquivalence.lean, line 250. The attribute's comment: “part (1)(b): for F in LQCoh^fbc(𝒪_𝒳), g^{-1}F is in QCoh(𝒪_{𝒳_{lisse,étale}})”.

Stacks 07B1 (1)(b). For 𝓕 in LQCoh^fbc(𝒪_𝒳) ⊆ Mod(𝒳_étale, 𝒪_𝒳), the module g^{-1}𝓕 on the lisse-étale site is quasi-coherent.

theorem isQuasicoherentOnSite_modulePullback_of_lqcohSheafFbc
    (F : etaleTopologyModules B S hS 𝒳) (hF : lqcohSheafFbcEtaleModules.{u, w, u} B E h S hS 𝒳 F) :
    ((modulePullback.{u, w} B S hS 𝒳).obj F).IsQuasicoherentOnSite

AlgebraicGeometry.Stack.LisseEtale.coheratorIsoLowerShriekModulePullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LisseEtaleQuasicoherentEquivalence.lean, line 293. The attribute's comment: “part (1)(c): Q(F) = g_! g^{-1} F for F in LQCoh^fbc(𝒪_𝒳), Q the coherator of 0778”.

Stacks 07B1 (1)(c). For 𝓕 in LQCoh^fbc(𝒪_𝒳), Q(𝓕) = g_!g^{-1}𝓕, naturally in 𝓕, as objects of QCoh(𝒪_𝒳), where Q : LQCoh^fbc(𝒪_𝒳) ⥤ QCoh(𝒪_𝒳) is the coherator of Stacks 0778 (AlgebraicGeometry.Stack.AlgebraicStacks.lqcohFbcCoherator), g^{-1}𝓕 is quasi-coherent by (1)(b) and g_! is the inverse equivalence of (1)(a). The isomorphism at 𝓕 is the unit Q(𝓕) ≅ g_!g^{-1}Q(𝓕) of (1)(a) followed by g_!g^{-1} of the adjunction map Q(𝓕) ⟶ 𝓕.

def coheratorIsoLowerShriekModulePullback :
    AlgebraicStacks.lqcohFbcCoherator B E h S hS 𝒳 ≅
      lqcohFbcModulePullback B S hS 𝒳 E h ⋙ quasicoherentModuleLowerShriek B S hS 𝒳

Tag 07B4, a lemma

Tag 07B4 in the Stacks Project.

AlgebraicGeometry.Stack.FlatFppf.isWeakSerreClass_isQuasicoherentOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatFppfWeakSerre.lean, line 242. The attribute's comment: “part (2): QCoh(O_{X_{flat,fppf}}) is a weak Serre subcategory of Mod(O_{X_{flat,fppf}})”.

Stacks 07B4 (2). For an algebraic stack 𝒳, the quasi-coherent modules on the flat-fppf site 𝒳_{flat,fppf}, ringed by 𝒪_{𝒳_{flat,fppf}}, form a weak Serre subcategory of Mod(𝒪_{𝒳_{flat,fppf}}).

The flat objects over affine schemes are a cover-dense subsite of 𝒳_{flat,fppf} which, with the arrows over flat, locally finitely presented morphisms, has fibre products along its coverings, finite covers refining its covering sieves, and flat factorizations of its arrows; so Stacks.FlatAffineSite.isWeakSerreClass_isQuasicoherentOnSite_of_affineSubsite applies.

theorem isWeakSerreClass_isQuasicoherentOnSite :
    (SheafOfModules.isQuasicoherentOnSite (Stacks.SheafOfModules.Tensor.ringSheaf
      (subsiteRingedTopos B S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids B.topology le_rfl
        (objectProperty B S hS 𝒳)).O) :
      ObjectProperty (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf
        (subsiteRingedTopos B S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids B.topology le_rfl
          (objectProperty B S hS 𝒳)).O))).IsWeakSerreClass

AlgebraicGeometry.Stack.LisseEtale.isWeakSerreClass_isQuasicoherentOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LisseEtaleWeakSerre.lean, line 249. The attribute's comment: “part (1)”.

For every algebraic stack 𝒳, the quasi-coherent modules on the lisse-étale site 𝒳_{lisse,étale}, ringed by 𝒪_{𝒳_{lisse,étale}} (the restriction of the structure sheaf, AlgebraicGeometry.Stack.LisseEtale.ringedTopos'), form a weak Serre subcategory of Mod(𝒪_{𝒳_{lisse,étale}}).

theorem isWeakSerreClass_isQuasicoherentOnSite :
    (SheafOfModules.isQuasicoherentOnSite
        (Stacks.SheafOfModules.Tensor.ringSheaf (ringedTopos'.{u, t} B S hS 𝒳).O) :
      ObjectProperty (SheafOfModules.{u}
        (Stacks.SheafOfModules.Tensor.ringSheaf
          (ringedTopos'.{u, t} B S hS 𝒳).O))).IsWeakSerreClass

Sources

• Section 103.16, Tag 07AY
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.isQuasicoherentOnSite_of_isSmooth_jointlySurjective · AlgebraicGeometry.Stack.isQuasicoherentOnSite_of_isFlat_isLfp_jointlySurjective · AlgebraicGeometry.Stack.LisseEtale.isQuasicoherentClause_fppf_moduleLowerShriek · AlgebraicGeometry.Stack.FlatFppf.isQuasicoherentOnSite_moduleLowerShriek_of_isQuasicoherentOnSite · AlgebraicGeometry.Stack.LisseEtale.isQuasicoherentOnSite_moduleLowerShriek · AlgebraicGeometry.Stack.FlatFppf.isQuasicoherentOnSite_moduleLowerShriek · AlgebraicGeometry.Stack.FlatFppf.quasicoherentEquivalence · AlgebraicGeometry.Stack.FlatFppf.isQuasicoherentOnSite_modulePullback_of_lqcohSheafFbc

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.