35.9 Cohomology of… to 35.10 Quasi-coherent sheaves…

Section35.9 Cohomology of quasi-coherent modules and topologies #

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

Tag 03FI, a lemma

Tag 03FI in the Stacks Project.

Stacks.Adequate.BigSite.coproductCechComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/DisjointUnionCech.lean, line 232. The attribute's comment: “part (3), on a chosen big site over a scheme: the Čech complex of a finite family and of the one-member family of the morphism from its disjoint union agree, for an abelian sheaf on the site”.

[Stacks, Tag 03FI] (3) on a chosen big site. For an 𝒪-module F on a chosen big τ-site over S, a finite family E of morphisms of the site and a morphism f of the site whose image in the schemes over S is the morphism from the disjoint union of the image of E, the Čech cohomology of E with coefficients in the abelian sheaf underlying F is the Čech cohomology of the one-member family {f}, in every degree. This discharges Stacks.Adequate.BigSite.CoproductCechComparison.

public theorem BigSite.coproductCechComparison (B : BigSite τ S)
    (F : SheafOfModules.{max u m} B.structureSheaf) :
    B.CoproductCechComparison.{u, m} F

AlgebraicGeometry.IsStandardCovering.singleton_sigmaDesc_mem_fpqcPrecoverage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/StandardCoveringDisjointUnion.lean, line 139. The attribute's comment: “part (1), fpqc covering”.

The morphism from the disjoint union of a standard covering is an fpqc covering of the target, for each of the five topologies.

theorem IsStandardCovering.singleton_sigmaDesc_mem_fpqcPrecoverage (τ : CoveringTopology)
    {T : Scheme.{u}} [IsAffine T] {I : Type w} (U : I → Scheme.{u}) (f : ∀ i, U i ⟶ T)
    (h : IsStandardCovering τ U f) :
    letI : Finite I := h.finite_index
    Presieve.singleton (Sigma.desc f) ∈ Scheme.fpqcPrecoverage T

AlgebraicGeometry.IsStandardCovering.singleton_sigmaDesc_mem_precoverage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/StandardCoveringDisjointUnion.lean, line 159. The attribute's comment: “part (1), covering in the original topology”.

Outside the Zariski topology, the morphism from the disjoint union of a standard covering is itself a covering family for the topology the covering is standard for.

theorem IsStandardCovering.singleton_sigmaDesc_mem_precoverage (τ : CoveringTopology)
    (hτ : τ ≠ .zariski) {T : Scheme.{u}} [IsAffine T] {I : Type w} (U : I → Scheme.{u})
    (f : ∀ i, U i ⟶ T) (h : IsStandardCovering τ U f) :
    letI : Finite I := h.finite_index
    Presieve.singleton (Sigma.desc f) ∈ Scheme.precoverage (coveringMorphismProperty τ) T

AlgebraicGeometry.IsStandardCovering.sieve_sigmaDesc_mem_topology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/StandardCoveringDisjointUnion.lean, line 192. The attribute's comment: “part (1), covering sieve in every topology”.

In every one of the five topologies, the sieve generated by the morphism from the disjoint union of a standard covering is a covering sieve of the target.

theorem IsStandardCovering.sieve_sigmaDesc_mem_topology (τ : CoveringTopology) {T : Scheme.{u}}
    [IsAffine T] {I : Type w} (U : I → Scheme.{u}) (f : ∀ i, U i ⟶ T)
    (h : IsStandardCovering τ U f) :
    letI : Finite I := h.finite_index
    Sieve.generate (Presieve.singleton (Sigma.desc f)) ∈
      (Scheme.precoverage (coveringMorphismProperty τ)).toGrothendieck T

AlgebraicGeometry.isIso_cechComplexMap_coproductRefinement_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/StandardCoveringDisjointUnion.lean, line 284. The attribute's comment: “part (3), big site”.

For an abelian sheaf on a topology on Over S refining the big Zariski topology, the canonical refinement of a finite family by the morphism from its disjoint union induces an isomorphism of Čech complexes.

theorem isIso_cechComplexMap_coproductRefinement_over (S : Scheme.{u})
    (J : GrothendieckTopology (Over S)) (hJ : Scheme.zariskiTopology.over S ≤ J) {T : Over S}
    (E : PreZeroHypercover.{w} T) [Finite E.I₀] (F : (Over S)ᵒᵖ ⥤ Ab.{v})
    (hF : Presheaf.IsSheaf J F) :
    IsIso (Stacks.CechSite.cechComplexMap E
      (PreZeroHypercover.singleton.{w} (Sigma.desc E.f))
      (Stacks.CechSite.coproductRefinement E) (F ⋙ AddCommGrpCat.uliftFunctor.{w, v}))

AlgebraicGeometry.isIso_cechComplexMap_coproductRefinement_smallEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/StandardCoveringDisjointUnion.lean, line 297. The attribute's comment: “part (3), small étale site”.

For an abelian sheaf on the small étale site of S, the canonical refinement of a finite family by the morphism from its disjoint union induces an isomorphism of Čech complexes.

theorem isIso_cechComplexMap_coproductRefinement_smallEtale (S : Scheme.{u}) {T : S.Etale}
    (E : PreZeroHypercover.{w} T) [Finite E.I₀] (F : (S.Etale)ᵒᵖ ⥤ Ab.{v})
    (hF : Presheaf.IsSheaf (Scheme.smallEtaleTopology S) F) :
    IsIso (Stacks.CechSite.cechComplexMap E
      (PreZeroHypercover.singleton.{w} (Sigma.desc E.f))
      (Stacks.CechSite.coproductRefinement E) (F ⋙ AddCommGrpCat.uliftFunctor.{w, v}))

AlgebraicGeometry.IsStandardCovering.sieve_sigmaDesc_mem_smallEtaleTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/StandardCoveringDisjointUnion.lean, line 309. The attribute's comment: “part (1), small étale site”.

The morphism from the disjoint union of a standard étale covering of an object of the small étale site of S generates a covering sieve of that object.

theorem IsStandardCovering.sieve_sigmaDesc_mem_smallEtaleTopology (S : Scheme.{u})
    {T : S.Etale} [IsAffine T.left] (E : PreZeroHypercover.{u} T) [HasCoproduct E.X]
    (h : IsStandardCovering .etale (fun i : E.I₀ ↦ (E.X i).left) (fun i ↦ (E.f i).left)) :
    Sieve.ofArrows (fun _ : PUnit ↦ ∐ E.X) (fun _ : PUnit ↦ Sigma.desc E.f) ∈
      Scheme.smallEtaleTopology S T

AlgebraicGeometry.isIso_cechComplexMap_coproductRefinement_smallZariski, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Zariski/SmallSiteCechComparison.lean, line 48. The attribute's comment: “part (3), case (c)”.

Stacks Project, Tag 03FI part (3), case (c). For an abelian sheaf on the small Zariski site of a scheme, read on the big Zariski site through its extension, the refinement of a finite family of morphisms by the single morphism from the coproduct of its members induces an isomorphism of Čech complexes.

theorem isIso_cechComplexMap_coproductRefinement_smallZariski (S : Scheme.{u})
    (F : Sheaf (Opens.grothendieckTopology S) AddCommGrpCat.{max (u + 1) v})
    {T : Over S} (E : PreZeroHypercover.{w} T) [Finite E.I₀] :
    IsIso (Stacks.CechSite.cechComplexMap E
      (PreZeroHypercover.singleton.{w} (Sigma.desc E.f))
      (Stacks.CechSite.coproductRefinement E)
      ((SmallZariski.extension.{u, v} S F).obj ⋙
        AddCommGrpCat.uliftFunctor.{w, max (u + 1) v}))

AlgebraicGeometry.SmallZariski.extension_sections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Zariski/SmallSiteExtension.lean, line 562. The attribute's comment: “case (c), geometric extension formula”.

The value of the small-to-big Zariski extension on a scheme T over S is the global sections on T of the inverse image of the sheaf along its structure morphism.

public def extension_sections (S : Scheme.{u}) (T : Over S) :
    ((S.restrictFunctor).sheafPullback AddCommGrpCat.{max (u + 1) v}
        (Opens.grothendieckTopology S) (Scheme.zariskiTopology.over S)) ⋙
      (sheafSections (Scheme.zariskiTopology.over S)
        AddCommGrpCat.{max (u + 1) v}).obj (Opposite.op T) ≅
    ((Opens.map (Scheme.forgetToTop.map T.hom)).sheafPullback
        AddCommGrpCat.{max (u + 1) v}
        (Opens.grothendieckTopology S)
        (Opens.grothendieckTopology T.left)) ⋙
      Sheaf.Γ (Opens.grothendieckTopology T.left)
        AddCommGrpCat.{max (u + 1) v}

AlgebraicGeometry.SmallZariski.extension_sections_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Zariski/SmallSiteExtension.lean, line 771. The attribute's comment: “case (c), naturality of the geometric extension”.

The valuewise geometric comparison respects every morphism over S. Thus the small-to-big extension is identified with the presheaf of sections of the geometric inverse image, not merely with its values at each object.

public theorem extension_sections_naturality
    (S : Scheme.{u}) {T T' : Over S} (g : T' ⟶ T)
    (F : Sheaf (Opens.grothendieckTopology S)
      AddCommGrpCat.{max (u + 1) v}) :
    (extension_sections.{u, v} S T).hom.app F ≫
      pullbackSectionsRestriction.{u, v} S g F =
      ((extension.{u, v} S F).obj.map g.op) ≫
        (extension_sections.{u, v} S T').hom.app F

AlgebraicGeometry.SmallZariski.isIso_extension_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Zariski/SmallSiteExtension.lean, line 841. The attribute's comment: “case (c), the extension restricts to the given sheaf”.

Restricting the extension of an abelian sheaf on the small Zariski site back to the open subschemes returns the sheaf itself: the unit of the adjunction is an isomorphism. This pins AlgebraicGeometry.SmallZariski.extension as an extension of the given sheaf.

public theorem isIso_extension_unit (S : Scheme.{u})
    (F : Sheaf (Opens.grothendieckTopology S) AddCommGrpCat.{max (u + 1) v}) :
    IsIso ((adjunction.{u, v} S).unit.app F)

Stacks.CechSite.coproductRefinement, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Cech/CoproductRefinement.lean, line 60. The attribute's comment: “part (2)”.

The component inclusions of a coproduct exhibit a family of morphisms with fixed target as a refinement of the singleton family given by the induced morphism from the coproduct.

noncomputable def coproductRefinement {C : Type u} [Category.{v} C]
    {T : C} (E : PreZeroHypercover.{w} T) [HasCoproduct E.X] :
    E.HomOver (PreZeroHypercover.singleton (Sigma.desc E.f)) (𝟙 T)

Tag 03FJ, a lemma

Tag 03FJ in the Stacks Project.

AlgebraicGeometry.SmallEtale.isZero_cechCohomology_succ_associatedPresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/CechAmitsurBoundedSmallEtale.lean, line 124. The attribute's comment: “the Cech^p = 0 for p >= 1 clause on the cardinality-bounded small étale site”.

Vanishing of Čech cohomology on the cardinality-bounded small étale site of S. The Čech cohomology of the sections of Fᵃ on a standard covering of an object of AlgebraicGeometry.SmallEtale B S hS vanishes in every positive degree.

public theorem isZero_cechCohomology_succ_associatedPresheaf (F : S.Modules)
    [F.IsQuasicoherent] {T : SmallEtale B S hS} (E : PreZeroHypercover.{u} T)
    (h : IsBoundedStandardCovering B S hS E) (p : ℕ) (hp : 0 < p) :
    IsZero (cechCohomology E
      ((toOver B S hS).op ⋙ quasiCoherentPresheafFunctor S F) p)

AlgebraicGeometry.cechComplexIsoAmitsurQuasiCoherent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/CechAmitsurQuasiCoherent.lean, line 97. The attribute's comment: “the isomorphism of complexes, for the one-member covering 03FI reduces to”.

For U an object of Over S with affine total space and f : W ⟶ U with W.left affine, the Čech complex of the presheaf Fᵃ on the one-member covering {W → U} is the complex s((A/R)_• ⊗_R M), where R = Γ(U.left, 𝒪), A = Γ(W.left, 𝒪) and M = Fᵃ(U), with its R-module structure forgotten.

public def cechComplexIsoAmitsurQuasiCoherent (F : S.Modules) [F.IsQuasicoherent]
    {W : Over S} (f : W ⟶ U) [IsAffine W.left] :
    letI := overAffineSliceAlgebra U f
    cechComplex (PreZeroHypercover.singleton.{u} f) (quasiCoherentPresheafFunctor S F) ≅
      ((forget₂ (ModuleCat.{u} (Γ(U.left, ⊤) : Type u)) AddCommGrpCat.{u}).mapHomologicalComplex
          (ComplexShape.up ℕ)).obj
        (amitsurCochainComplex (Γ(U.left, ⊤) : Type u) (Γ(W.left, ⊤) : Type u)
          (Stacks.Sites.coeffModule S F (𝟭 (Over S)) U))

AlgebraicGeometry.cechComplexIsoAmitsurStandardCovering, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/CechAmitsurQuasiCoherent.lean, line 129. The attribute's comment: “the isomorphism of complexes, for an arbitrary standard covering”.

For a standard τ-covering 𝒰 = {U_i → U} of an object of Over S with affine total space, the Čech complex of Fᵃ is s((A/R)_• ⊗_R M), where R = Γ(U.left, 𝒪), A = Γ((∐ U_i).left, 𝒪) and M = Fᵃ(U).

public def cechComplexIsoAmitsurStandardCovering (τ : CoveringTopology) (F : S.Modules)
    [F.IsQuasicoherent] (𝒱 : PreZeroHypercover.{u} U)
    (h : IsStandardCovering τ (fun i ↦ (𝒱.X i).left) (fun i ↦ (𝒱.f i).left)) :
    letI : Finite 𝒱.I₀ := h.finite_index
    letI : IsAffine (∐ 𝒱.X).left := h.isAffine_left_sigmaObj τ S 𝒱
    letI := overAffineSliceAlgebra U (Sigma.desc 𝒱.f)
    cechComplex 𝒱 (quasiCoherentPresheafFunctor S F) ≅
      ((forget₂ (ModuleCat.{u} (Γ(U.left, ⊤) : Type u))
            AddCommGrpCat.{u}).mapHomologicalComplex (ComplexShape.up ℕ)).obj
        (amitsurCochainComplex (Γ(U.left, ⊤) : Type u) (Γ((∐ 𝒱.X).left, ⊤) : Type u)
          (Stacks.Sites.coeffModule S F (𝟭 (Over S)) U))

AlgebraicGeometry.cechComplexIsoAmitsurSmallEtale, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/CechAmitsurSmallSites.lean, line 102. The attribute's comment: “the isomorphism of complexes, case (b), the small étale site”.

For a small-étale-standard covering 𝒰 = {U_i → U} of an object of S_étale, the Čech complex of the presheaf Fᵃ is the complex s((A/R)_• ⊗_R M), where R = Γ(U, 𝒪), A = Γ(∐ U_i, 𝒪) and M = Fᵃ(U).

public def cechComplexIsoAmitsurSmallEtale (F : S.Modules) [F.IsQuasicoherent] {T : S.Etale}
    (𝒱 : PreZeroHypercover.{u} T) (h : IsSmallEtaleStandardCovering S 𝒱) :
    letI : IsAffine ((Scheme.Etale.forget S).obj T).left :=
      (IsSmallEtaleStandardCovering.isAffine S h).1
    letI : Finite (𝒱.map (Scheme.Etale.forget S)).I₀ :=
      IsSmallEtaleStandardCovering.finite S h
    letI := overAffineSliceAlgebra ((Scheme.Etale.forget S).obj T)
      (Sigma.desc (𝒱.map (Scheme.Etale.forget S)).f)
    cechComplex 𝒱 ((Scheme.Etale.forget S).op ⋙ quasiCoherentPresheafFunctor S F) ≅
      ((forget₂ (ModuleCat.{u} (Γ(((Scheme.Etale.forget S).obj T).left, ⊤) : Type u))
            AddCommGrpCat.{u}).mapHomologicalComplex (ComplexShape.up ℕ)).obj
        (amitsurCochainComplex (Γ(((Scheme.Etale.forget S).obj T).left, ⊤) : Type u)
          (Γ((∐ (𝒱.map (Scheme.Etale.forget S)).X).left, ⊤) : Type u)
          (Stacks.Sites.coeffModule S F (𝟭 (Over S)) ((Scheme.Etale.forget S).obj T)))

AlgebraicGeometry.isZero_cechCohomology_succ_quasiCoherentPresheaf_smallEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/CechAmitsurSmallSites.lean, line 126. The attribute's comment: “the Cech^p = 0 for p >= 1 clause, case (b), the small étale site”.

The Čech cohomology of Fᵃ on a small-étale-standard covering vanishes in every positive degree.

public theorem isZero_cechCohomology_succ_quasiCoherentPresheaf_smallEtale (F : S.Modules)
    [F.IsQuasicoherent] {T : S.Etale} (𝒱 : PreZeroHypercover.{u} T)
    (h : IsSmallEtaleStandardCovering S 𝒱) (p : ℕ) (hp : 0 < p) :
    IsZero (cechCohomology 𝒱
      ((Scheme.Etale.forget S).op ⋙ quasiCoherentPresheafFunctor S F) p)

AlgebraicGeometry.cechComplexIsoAmitsurSmallZariski, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/CechAmitsurSmallSites.lean, line 225. The attribute's comment: “the isomorphism of complexes, case (c), the small Zariski site”.

For a standard Zariski covering 𝒰 = {U_i → U} of an affine open U of S, the Čech complex in S_Zar of the presheaf Fᵃ, which on the small Zariski site is V ↦ Γ(V, F|_V), is the complex s((A/R)_• ⊗_R M), where R = Γ(U, 𝒪), A = Γ(∐ U_i, 𝒪) with the coproduct taken in Over S, and M = Fᵃ(U).

public def cechComplexIsoAmitsurSmallZariski (F : S.Modules) [F.IsQuasicoherent]
    {T : S.Opens} [IsAffine (S.restrictFunctor.obj T).left]
    (𝒱 : PreZeroHypercover.{u} T)
    [∀ (n : ℕ) (i : Fin (n + 1) → 𝒱.I₀), HasProduct (fun a ↦ Over.mk (𝒱.f (i a)))]
    (h : IsStandardCovering .zariski
      (fun i ↦ ((𝒱.map S.restrictFunctor).X i).left)
      (fun i ↦ ((𝒱.map S.restrictFunctor).f i).left)) :
    letI : Finite (𝒱.map S.restrictFunctor).I₀ := h.finite_index
    letI := overAffineSliceAlgebra (S.restrictFunctor.obj T)
      (Sigma.desc (𝒱.map S.restrictFunctor).f)
    cechComplex 𝒱 (S.restrictFunctor.op ⋙ quasiCoherentPresheafFunctor S F) ≅
      ((forget₂ (ModuleCat.{u} (Γ((S.restrictFunctor.obj T).left, ⊤) : Type u))
            AddCommGrpCat.{u}).mapHomologicalComplex (ComplexShape.up ℕ)).obj
        (amitsurCochainComplex (Γ((S.restrictFunctor.obj T).left, ⊤) : Type u)
          (Γ((∐ (𝒱.map S.restrictFunctor).X).left, ⊤) : Type u)
          (Stacks.Sites.coeffModule S F (𝟭 (Over S)) (S.restrictFunctor.obj T)))

AlgebraicGeometry.isZero_cechCohomology_succ_quasiCoherentPresheaf_smallZariski, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/CechAmitsurSmallSites.lean, line 248. The attribute's comment: “the Cech^p = 0 for p >= 1 clause, case (c), the small Zariski site”.

The Čech cohomology of Fᵃ on a standard Zariski covering of an affine open of S vanishes in every positive degree.

public theorem isZero_cechCohomology_succ_quasiCoherentPresheaf_smallZariski (F : S.Modules)
    [F.IsQuasicoherent] {T : S.Opens} [IsAffine (S.restrictFunctor.obj T).left]
    (𝒱 : PreZeroHypercover.{u} T)
    [∀ (n : ℕ) (i : Fin (n + 1) → 𝒱.I₀), HasProduct (fun a ↦ Over.mk (𝒱.f (i a)))]
    (h : IsStandardCovering .zariski
      (fun i ↦ ((𝒱.map S.restrictFunctor).X i).left)
      (fun i ↦ ((𝒱.map S.restrictFunctor).f i).left)) (p : ℕ) (hp : 0 < p) :
    IsZero (cechCohomology 𝒱
      (S.restrictFunctor.op ⋙ quasiCoherentPresheafFunctor S F) p)

AlgebraicGeometry.isZero_cechCohomology_singleton_succ_quasiCoherentPresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/CechVanishingStandardCovering.lean, line 133. The attribute's comment: “the Cech^p = 0 for p >= 1 clause, for the one-member covering 03FI reduces to; unconditional -- hcoeff, harrow and hcolim are all three discharged”.

Čech vanishing in positive degrees for the one-member covering of an affine object of Over S by an affine object whose coordinate ring is faithfully flat over that of the target, with the presheaf Fᵃ of [Stacks, Tag 03DS] as coefficients.

public theorem isZero_cechCohomology_singleton_succ_quasiCoherentPresheaf
    (F : S.Modules) [F.IsQuasicoherent] {W : Over S} (f : W ⟶ U) [IsAffine W.left]
    (hff : letI := overAffineSliceAlgebra U f
      Module.FaithfullyFlat (Γ(U.left, ⊤) : Type u) (Γ(W.left, ⊤) : Type u))
    (p : ℕ) :
    IsZero (cechCohomology (PreZeroHypercover.singleton.{u} f)
      (quasiCoherentPresheafFunctor S F) (p + 1))

AlgebraicGeometry.isZero_cechCohomology_succ_quasiCoherentPresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/CechVanishingStandardCovering.lean, line 170. The attribute's comment: “the Cech^p = 0 for p >= 1 clause, for an arbitrary standard covering; unconditional -- hcoeff, harrow and hcolim are all three discharged”.

Čech vanishing in positive degrees for a standard τ-covering of an affine object of Over S, with the presheaf Fᵃ of [Stacks, Tag 03DS] as coefficients, for each of the five topologies.

public theorem isZero_cechCohomology_succ_quasiCoherentPresheaf (τ : CoveringTopology)
    (F : S.Modules) [F.IsQuasicoherent] (𝒱 : PreZeroHypercover.{u} U)
    (h : IsStandardCovering τ (fun i ↦ (𝒱.X i).left) (fun i ↦ (𝒱.f i).left))
    (p : ℕ) (hp : 0 < p) :
    IsZero (cechCohomology 𝒱 (quasiCoherentPresheafFunctor S F) p)

Tag 03DW, a proposition

Tag 03DW in the Stacks Project.

AlgebraicGeometry.BigFppfOver.hZeroBaseAssociatedModuleAddEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModuleCohomologyDegreeZero.lean, line 209. The attribute's comment: “the case q = 0 of clause (1), for every one of the five topologies”.

[Stacks, Tag 03DW], clause (1), in the case q = 0. Let S be a scheme, let 𝓕 be a quasi-coherent 𝒪_S-module and let τ ∈ {Zariski, étale, smooth, syntomic, fppf}. There is a canonical isomorphism
H^0(S, 𝓕)  =  H^0((Sch/S)_τ, 𝓕^a).
Cohomology of a site in degree zero is the group of global sections, that is the sections over a terminal object; the open ⊤ of S is terminal both in the small Zariski site of S and, as an object of the big site, in (Sch/S)_τ. So the isomorphism is the identification Γ(S, 𝓕) = Γ(S, 𝓕^a) of AlgebraicGeometry.BigFppfOver.baseAssociatedModuleSectionsIso, which is the unit of the associated-module adjunction at a quasi-coherent module.

Only q = 0 is asserted by this declaration, and only on this site: the big site here is AlgebraicGeometry.BigFppfOver.baseOverTopology, five topologies on the one underlying category of a chosen big fppf site. Every degree q, on AlgebraicGeometry.overTopology, is AlgebraicGeometry.bigOverQuasiCoherentGlobalCohomologyIso, and clause (2) in its small étale half is AlgebraicGeometry.smallEtaleQuasiCoherentGlobalCohomologyIso; both carry the tag. For τ ≠ fppf those two sites are topologies on different categories, so this declaration is not subsumed by them and stays part of the covering set. The small Zariski half of clause (2) is AlgebraicGeometry.smallZariskiQuasiCoherentGlobalCohomologyIso (StacksFrontier/AlgebraicGeometry/Topologies/Zariski/SmallZariskiQuasiCoherentCohomology.lean), which carries the tag as well.

public noncomputable def hZeroBaseAssociatedModuleAddEquiv (τ : SiteKind) (F : S.Modules)
    [F.IsQuasicoherent]
    [HasExt.{w} (Sheaf (Opens.grothendieckTopology ↥S) AddCommGrpCat.{u})]
    [HasExt.{w} (Sheaf (baseOverTopology B S hS τ) AddCommGrpCat.{u})] :
    Sheaf.H.{w} ((SheafOfModules.toSheaf S.ringCatSheaf).obj F) 0 ≃+
      Sheaf.H.{w} ((SheafOfModules.toSheaf (FibredSite.baseRingStructureSheaf B S hS τ)).obj
        ((baseAssociatedModule B S hS τ).obj F)) 0

AlgebraicGeometry.bigOverQuasiCoherentSiteCohomologyAddEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentSiteCohomologyComparison.lean, line 130. The attribute's comment: “clause (1), in EVERY degree q and for all five τ at once (τ is a bound variable), in the source's own shape: both sides are the cohomology of a SITE, CategoryTheory.Sheaf.H, and not cohomology over an object of it. The Sheaf.H' carrier bigOverQuasiCoherentGlobalCohomologyIso states the same comparison over the object of the big site that ⊤ becomes; this is that statement composed with the terminal-object identification Stacks.Cohomology.TerminalCohomology.h'AddEquivH on both sides, the two objects being terminal by topIsTerminal and isTerminal_opensBelowToOver_top. Clause (2) is smallZariskiQuasiCoherentSiteCohomologyAddEquiv together with smallEtaleQuasiCoherentSiteCohomologyAddEquiv”.

[Stacks, Tag 03DW], clause (1). Let S be a scheme, let ℱ be a quasi-coherent 𝒪_S-module and let τ ∈ {Zariski, étale, smooth, syntomic, fppf}. In every degree q there is a canonical isomorphism
H^q(S, ℱ)  ≅  H^q((Sch/S)_τ, ℱᵃ),
the right-hand side being the cohomology of the localized big τ-site of S with values in the associated module of [Stacks, Tag 03DU].

τ is a bound variable, so this one declaration is all five topologies. It is AlgebraicGeometry.bigOverQuasiCoherentGlobalCohomologyIso — the same comparison stated for cohomology over the object of the site that ⊤ becomes — read through the identification of cohomology over a terminal object with cohomology of the site, on both sides.

public def bigOverQuasiCoherentSiteCohomologyAddEquiv (p : ℕ) :
    Sheaf.H.{u} ((SheafOfModules.toSheaf S.ringCatSheaf).obj F) p ≃+
      Sheaf.H.{u} (bigOverAssociatedSheaf S F τ B hS) p

AlgebraicGeometry.smallZariskiQuasiCoherentSiteCohomologyAddEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentSiteCohomologyComparison.lean, line 174. The attribute's comment: “clause (2), the small ZARISKI link H^q(S, F) = H^q(S_Zar, Fᵃ), in EVERY degree q, in the source's own shape: both sides are the cohomology of a SITE, CategoryTheory.Sheaf.H. The Sheaf.H' carrier smallZariskiQuasiCoherentGlobalCohomologyIso states the same comparison over the object of S_Zar that ⊤ becomes; this is that statement composed with Stacks.Cohomology.TerminalCohomology.h'AddEquivH on both sides, the two objects being terminal by topIsTerminal and isTerminal_opensToSmallZariski_top. The other link of clause (2) is smallEtaleQuasiCoherentSiteCohomologyAddEquiv and clause (1) is bigOverQuasiCoherentSiteCohomologyAddEquiv”.

[Stacks, Tag 03DW], clause (2), the small Zariski link. For a scheme S in a big Zariski site, a quasi-coherent 𝒪_S-module ℱ and a degree q there is a canonical isomorphism
H^q(S, ℱ)  ≅  H^q(S_Zar, ℱᵃ),
the right-hand side being the cohomology of the small Zariski site of [Stacks, Tag 020T] (2) with values in the associated module of [Stacks, Tag 03DU] (4) at τ = Zariski.

This is AlgebraicGeometry.smallZariskiQuasiCoherentGlobalCohomologyIso read through the identification of cohomology over a terminal object with cohomology of the site.

public def smallZariskiQuasiCoherentSiteCohomologyAddEquiv (p : ℕ) :
    Sheaf.H.{u} ((SheafOfModules.toSheaf S.ringCatSheaf).obj F) p ≃+
      Sheaf.H.{u} (smallZariskiAssociatedSheaf B S hS F) p

AlgebraicGeometry.smallEtaleQuasiCoherentSiteCohomologyAddEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentSiteCohomologyComparison.lean, line 215. The attribute's comment: “clause (2), the small ÉTALE link H^q(S, F) = H^q(S_étale, Fᵃ), in EVERY degree q, in the source's own shape: both sides are the cohomology of a SITE, CategoryTheory.Sheaf.H. The Sheaf.H' carrier smallEtaleQuasiCoherentGlobalCohomologyIso states the same comparison over the object of S_étale that ⊤ becomes; this is that statement composed with Stacks.Cohomology.TerminalCohomology.h'AddEquivH on both sides, the two objects being terminal by topIsTerminal and isTerminal_opensToEtale_top. The other link of clause (2) is smallZariskiQuasiCoherentSiteCohomologyAddEquiv and clause (1) is bigOverQuasiCoherentSiteCohomologyAddEquiv”.

[Stacks, Tag 03DW], clause (2), the small étale link. For a scheme S, a quasi-coherent 𝒪_S-module ℱ and a degree q there is a canonical isomorphism
H^q(S, ℱ)  ≅  H^q(S_étale, ℱᵃ),
the right-hand side being the cohomology of the small étale site of S with values in the associated module of [Stacks, Tag 03DU].

This is AlgebraicGeometry.smallEtaleQuasiCoherentGlobalCohomologyIso read through the identification of cohomology over a terminal object with cohomology of the site.

public def smallEtaleQuasiCoherentSiteCohomologyAddEquiv (p : ℕ) :
    Sheaf.H.{u} ((SheafOfModules.toSheaf S.ringCatSheaf).obj F) p ≃+
      Sheaf.H.{u} (smallEtaleAssociatedSheaf S F) p

AlgebraicGeometry.bigOverQuasiCoherentGlobalCohomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/CechComparison/BigSiteQuasiCoherentCohomology.lean, line 226. The attribute's comment: “clause (1), in EVERY degree q and for all five τ at once (τ is a bound variable) — the same statement as Tag 03P2 at 𝒞 = (Sch/S)_τ, Descent Proposition 35.9.3 and Étale Cohomology Theorem 59.22.4 being the same assertion in two chapters. In particular this is the POSITIVE-DEGREE case, which the q = 0 carrier BigFppfOver.hZeroBaseAssociatedModuleAddEquiv does not claim; the affine vanishing H^p(U, Fᵃ) = 0 that the source's proof passes through is isZero_sheafCohomology_succ_overAffine. The site here is overTopology on Over (base B S hS), not the BigFppfOver.baseOverTopology that the q = 0 carrier uses; the two are topologies on different categories for τ ≠ fppf and no bridge is claimed. Clause (2) is covered by smallEtaleQuasiCoherentGlobalCohomologyIso (the small étale half) together with smallZariskiQuasiCoherentGlobalCohomologyIso (the small Zariski half)”.

Zariski cohomology of a quasi-coherent module agrees with its big τ-site cohomology: for a quasi-coherent module F on a scheme S and a degree p,

H^p(S, ℱ) ≅ H^p_τ(S, Fᵃ).

This is AlgebraicGeometry.bigOverQuasiCoherentCohomologyIso at the whole scheme. The object it is taken over on the right, (opensBelowToOver hS).obj ⊤, is a final object of the big site by AlgebraicGeometry.isTerminal_opensBelowToOver_top, so the right-hand side is τ-cohomology of S itself.

This is [Stacks, Tag 03P2] in the case 𝒞 = (Sch/S)_τ, for all five τ at once. Together with AlgebraicGeometry.smallEtaleQuasiCoherentGlobalCohomologyIso, which is the case 𝒞 = S_étale, it is the covering set of the tag: the source lets 𝒞 be either of the two, and these are one declaration per case.

public def bigOverQuasiCoherentGlobalCohomologyIso (p : ℕ) :
    Sheaf.H' ((SheafOfModules.toSheaf S.ringCatSheaf).obj F) p ⊤ ≅
      Sheaf.H' (bigOverAssociatedSheaf S F τ B hS) p
        ((opensBelowToOver (κ := cutoff τ B) hS).obj ⊤)

AlgebraicGeometry.smallEtaleQuasiCoherentGlobalCohomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/CechComparison/SmallEtaleQuasiCoherentCohomology.lean, line 89. The attribute's comment: “clause (2), the small étale half, in EVERY degree q — the same statement as Tag 03P2 at 𝒞 = S_étale, Descent Proposition 35.9.3 and Étale Cohomology Theorem 59.22.4 being the same assertion in two chapters. In particular this is the POSITIVE-DEGREE case, which the q = 0 carrier BigFppfOver.hZeroBaseAssociatedModuleAddEquiv does not claim; the affine vanishing H^p(U, Fᵃ) = 0 that the source's proof passes through is isZero_sheafCohomology_succ_smallEtaleAffine. NOT covered here: the small ZARISKI half of clause (2), which is smallZariskiQuasiCoherentGlobalCohomologyIso; clause (1) is bigOverQuasiCoherentGlobalCohomologyIso”. References: SGA 4 VII (4.3).

For a quasi-coherent module F on a scheme S and a degree p, Zariski cohomology of F agrees with small étale cohomology of its associated module:

H^p(S, ℱ) ≅ H^p(S_étale, Fᵃ).

The right-hand side is taken over (opensToEtale S).obj ⊤, a final object of the small étale site, so it is étale cohomology of S itself.

public def smallEtaleQuasiCoherentGlobalCohomologyIso (p : ℕ) :
    Sheaf.H' ((SheafOfModules.toSheaf S.ringCatSheaf).obj F) p ⊤ ≅
      Sheaf.H' (smallEtaleAssociatedSheaf S F) p ((opensToEtale S).obj ⊤)

AlgebraicGeometry.smallZariskiQuasiCoherentGlobalCohomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Zariski/SmallZariskiQuasiCoherentCohomology.lean, line 367. The attribute's comment: “clause (2), the small ZARISKI half H^q(S, F) = H^q(S_Zar, Fᵃ), in EVERY degree q. S_Zar is the small Zariski site of Tag 020T (2) and Fᵃ the associated module of Tag 03DU (4) at τ = Zariski, SmallZariski.associatedModuleOfSections. The object the right-hand side is taken over, (opensToSmallZariski B S hS).obj ⊤, is a final object of the site by isTerminal_opensToSmallZariski_top, so that side is the cohomology of S_Zar itself. The other half of clause (2), H^q(S, F) = H^q(S_étale, Fᵃ), is smallEtaleQuasiCoherentGlobalCohomologyIso; clause (1) is bigOverQuasiCoherentGlobalCohomologyIso. No 03P2 attribute: that tag lets 𝒞 be a big τ-site or S_étale and does not include S_Zar”.

Zariski cohomology of a quasi-coherent module agrees with the cohomology of its associated module on the small Zariski site: for a quasi-coherent module F on a scheme S and a degree p,

H^p(S, ℱ) ≅ H^p(S_Zar, Fᵃ).

This is AlgebraicGeometry.smallZariskiQuasiCoherentCohomologyIso at the whole scheme. The object it is taken over on the right, (opensToSmallZariski B S hS).obj ⊤, is a final object of the small Zariski site by AlgebraicGeometry.isTerminal_opensToSmallZariski_top, so the right-hand side is the cohomology of S_Zar itself.

This is the small Zariski half of clause (2) of [Stacks, Tag 03DW], in every degree. Together with AlgebraicGeometry.smallEtaleQuasiCoherentGlobalCohomologyIso, the small étale half, it is the covering set of that clause.

public def smallZariskiQuasiCoherentGlobalCohomologyIso (p : ℕ) :
    Sheaf.H' ((SheafOfModules.toSheaf S.ringCatSheaf).obj F) p ⊤ ≅
      Sheaf.H' (smallZariskiAssociatedSheaf B S hS F) p
        ((opensToSmallZariski B S hS).obj ⊤)

Tag 03LC, a proposition

Tag 03LC in the Stacks Project.

AlgebraicGeometry.BigFppfOver.associatedModuleBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/ObjectFunctoriality.lean, line 415. The attribute's comment: “part (1) at τ = fppf”.

Stacks Project, Tag 03LC part (1), at τ = fppf. The equivalence of Stacks 03DX is compatible with pullback: for f : X ⟶ S the structure morphism of an object T of the big fppf category over S, with f_big the induced morphism of ringed big fppf sites of Stacks 021W, and 𝓕 a quasi-coherent module on S,
`f_big^*(𝓕^a) ≅ (f^*𝓕)^a`,
naturally in 𝓕. This is AlgebraicGeometry.BigFppfOver.associatedModuleObjRestrictNatIso with the restriction functor replaced by the inverse image of f_big through AlgebraicGeometry.BigFppfOver.objInverseImageIso.

The same clause for an arbitrary morphism of schemes rather than an object of the big site, and at all five τ rather than at fppf alone, is AlgebraicGeometry.BigFppfOver.associatedModuleBasePullbackIso (StacksFrontier/AlgebraicGeometry/Descent/AssociatedModulePullbackBigSites.lean); what this declaration adds over it is the identification of f_big^* with restriction to the big fppf site of the scheme of T, which is what the proof of Stacks 03DX (1) consumes.

public noncomputable def associatedModuleBaseChangeIso :
    associatedModule B S hS ⋙ SheafOfModules.pullback.{u} (objBaseChangeSharp B S hS T) ≅
      Scheme.Modules.pullback (objHom B S hS T) ⋙
        associatedModule B (objScheme B S hS T) (contains_objScheme B S hS T)

AlgebraicGeometry.associatedModule_pullback_compatible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/PullbackPushforwardParts.lean, line 70. The attribute's comment: “(1)”.

Stacks Project, Tag 03LC part (1). The equivalences of Proposition 03DX are compatible with pullback: for every morphism of schemes f and every module 𝓖 on the target, f_sites^*(𝓖^a) ≅ (f^*𝓖)^a, naturally in 𝓖, where f_sites is the induced morphism of ringed sites of Stacks 070R —

on the big sites, f_big : ((Sch/X)_τ, 𝒪) ⟶ ((Sch/Y)_τ, 𝒪) at each of τ ∈ {Zariski, étale, smooth, syntomic, fppf} (AlgebraicGeometry.BigFppfOver.associatedModuleBasePullbackIso);

on the small étale sites, f_small : X_étale ⟶ Y_étale (AlgebraicGeometry.SmallEtale.associatedModuleBaseChangeIso);

on the small Zariski sites, f_small : T_Zar ⟶ S_Zar (AlgebraicGeometry.SmallZariski.lcAssociatedModulePullbackIso).

The source states it for quasi-coherent 𝓖; it holds for every module.

theorem associatedModule_pullback_compatible :
    (∀ (B : BigFppfSite.{u}) {X Y : Scheme.{u}} (hX : B.Contains X) (hY : B.Contains Y)
        (f : X ⟶ Y) (τ : SiteKind),
      Nonempty (Scheme.Modules.pullback f ⋙ BigFppfOver.baseAssociatedModule B X hX τ ≅
        BigFppfOver.baseAssociatedModule B Y hY τ ⋙
          SheafOfModules.pullback.{u} (BigFppfOver.baseStructureComparison B hX hY f τ))) ∧
    (∀ (B : BigEtaleSite.{u}) {X Y : B.Scheme} (a : X ⟶ Y),
      Nonempty (Scheme.Modules.pullback (SmallEtale.schemeHom B a) ⋙
          SmallEtale.associatedModule B X.obj X.property ≅
        SmallEtale.associatedModule B Y.obj Y.property ⋙
          SheafOfModules.pullback.{u} (SmallEtale.smallEtaleStructureMapRing B a))) ∧
    (∀ (B : BigZariskiSite.{u}) {S T : B.Schemes} (f : T ⟶ S),
      Nonempty (Scheme.Modules.pullback (SmallZariski.lcSchemeHom B f) ⋙
          SmallZariski.associatedModule B T.1 T.property ≅
        SmallZariski.associatedModule B S.1 S.property ⋙
          SheafOfModules.pullback.{u} (SmallZariski.lcStructureMapRing B f)))

AlgebraicGeometry.associatedModule_pushforward_compatible_of_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/PullbackPushforwardParts.lean, line 102. The attribute's comment: “(3)”.

Stacks Project, Tag 03LC part (3). Let f be quasi-compact and quasi-separated and τ ∈ {Zariski, étale}. Then f_* preserves quasi-coherent modules (Stacks 01LC, AlgebraicGeometry.pushforward_isQuasicoherent), f_{small, *} preserves quasi-coherent 𝒪-modules on the small τ-sites, and the square of the two associated-module functors commutes, f_{small, *}(𝓕^a) ≅ (f_*𝓕)^a for every quasi-coherent 𝓕.

At τ = étale the last two conjuncts are AlgebraicGeometry.SmallEtale.isQuasicoherentOnSite_smallPushforward and AlgebraicGeometry.SmallEtale.associatedModuleSmallPushforwardIsoOfQcqs; at τ = Zariski they are AlgebraicGeometry.SmallZariski.lcIsQuasicoherentOnSite_smallPushforward and AlgebraicGeometry.SmallZariski.lcAssociatedModuleSmallPushforwardIso.

theorem associatedModule_pushforward_compatible_of_qcqs :
    (∀ (B : BigEtaleSite.{u}) {X Y : B.Scheme} (a : X ⟶ Y)
        [QuasiCompact (SmallEtale.schemeHom B a)] [QuasiSeparated (SmallEtale.schemeHom B a)],
      (∀ 𝓕 : X.obj.Modules, 𝓕.IsQuasicoherent →
        ((Scheme.Modules.pushforward (SmallEtale.schemeHom B a)).obj 𝓕).IsQuasicoherent) ∧
      (∀ 𝓖 : SheafOfModules.{u} (SmallEtale.structureSheaf B X.obj X.property),
        𝓖.IsQuasicoherentOnSite → ((SmallEtale.smallPushforward B a).obj 𝓖).IsQuasicoherentOnSite) ∧
      (∀ 𝓕 : X.obj.Modules, 𝓕.IsQuasicoherent →
        Nonempty ((SmallEtale.associatedModule B Y.obj Y.property).obj
            ((Scheme.Modules.pushforward (SmallEtale.schemeHom B a)).obj 𝓕) ≅
          (SmallEtale.smallPushforward B a).obj
            ((SmallEtale.associatedModule B X.obj X.property).obj 𝓕)))) ∧
    (∀ (B : BigZariskiSite.{u}) {S T : B.Schemes} (f : T ⟶ S)
        [QuasiCompact (SmallZariski.lcSchemeHom B f)]
        [QuasiSeparated (SmallZariski.lcSchemeHom B f)],
      (∀ 𝓕 : (T.1).Modules, 𝓕.IsQuasicoherent →
        ((Scheme.Modules.pushforward (SmallZariski.lcSchemeHom B f)).obj 𝓕).IsQuasicoherent) ∧
      (∀ 𝓖 : SheafOfModules.{u} (SmallZariski.structureSheaf B T.1 T.property),
        𝓖.IsQuasicoherentOnSite →
          ((SheafOfModules.pushforward.{u} (SmallZariski.lcStructureMapRing B f)).obj
            𝓖).IsQuasicoherentOnSite) ∧
      (∀ 𝓕 : (T.1).Modules, 𝓕.IsQuasicoherent →
        Nonempty ((SmallZariski.associatedModule B S.1 S.property).obj
            ((Scheme.Modules.pushforward (SmallZariski.lcSchemeHom B f)).obj 𝓕) ≅
          (SheafOfModules.pushforward.{u} (SmallZariski.lcStructureMapRing B f)).obj
            ((SmallZariski.associatedModule B T.1 T.property).obj 𝓕))))

AlgebraicGeometry.SmallEtale.associatedModuleBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtaleMorphismBaseChange.lean, line 388. The attribute's comment: “part (1) at τ = étale, for the small étale sites”.

The associated module of a pullback is the pullback of the associated module. For a : X ⟶ Y a morphism of schemes of the big étale site, with r the underlying morphism of schemes and ε_a the morphism of ringed sites of Stacks 070R (2),

(r^*𝓕)^a ≅ ε_a^*(𝓕^a),

naturally in the 𝒪_Y-module 𝓕, with no quasi-coherence hypothesis. This is Stacks 03LC part (1) at τ = étale, for the small étale sites of two schemes and a morphism between them: the equivalence of Stacks 03DX (2) at τ = étale is compatible with pullback. It is proved here for arbitrary modules, not only quasi-coherent ones.

Each side is a composite of two pullbacks of sheaves of modules round the square of ringed sites whose geometric half is AlgebraicGeometry.SmallEtale.baseChangeOpensIso and whose ring half is AlgebraicGeometry.SmallEtale.structureMap_comp_baseChangeOpensIso, so the two agree because a left adjoint is determined by its right adjoint.

This also carries Stacks 03FH (2) for the morphism f_{small} : X_étale ⟶ Y_étale of Remark 070R (2): that clause asserts (f^*𝓕)^a = f_{sites}^*𝓕^a for every f_{sites} of Remark 070R, and this is the small étale one. The big fppf one is AlgebraicGeometry.BigFppfOver.associatedModuleBigPullbackIso (StacksFrontier/AlgebraicGeometry/Descent/AssociatedModulePullbackBigFppf.lean); the big Zariski, étale, smooth and syntomic ones are AlgebraicGeometry.BigFppfOver.associatedModuleBasePullbackIso (StacksFrontier/AlgebraicGeometry/Descent/AssociatedModulePullbackBigSites.lean), and the small Zariski one is AlgebraicGeometry.SmallZariski.lcAssociatedModulePullbackIso (StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallZariskiPushforwardSquare.lean:458). (It was formerly cited as AlgebraicGeometry.SmallZariski.associatedModulePullbackIso, which states the commutation over the identity reading of 𝓕 ↦ 𝓕^a and is a tautology about 𝟭; that declaration is untagged, and naming it here made this enumeration a false completeness claim.) Those are every f_sites the enumeration of Remark 070R lists; the mixed-topology entries (Sch/X)_τ ⟶ (Sch/Y)_{τ'} with τ ≠ τ' of the Topologies, Section 03FE list that the remark's opening sentence also covers are not claimed.

public def associatedModuleBaseChangeIso :
    Scheme.Modules.pullback (schemeHom B a) ⋙ associatedModule B X.obj X.property ≅
      associatedModule B Y.obj Y.property ⋙
        SheafOfModules.pullback.{u} (smallEtaleStructureMapRing B a)

AlgebraicGeometry.SmallEtale.isQuasicoherentOnSite_smallPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtalePushforwardCartesian.lean, line 872. The attribute's comment: “part (3) at τ = étale, the second conjunct: f_{small, *} carries quasi-coherent 𝒪-modules on the small étale site of X to quasi-coherent 𝒪-modules on the small étale site of Y, for f quasi-compact and quasi-separated”.

Stacks 03LC part (3) at τ = étale, the second conjunct. For f : X ⟶ Y quasi-compact and quasi-separated, the direct image f_{small, *} along the morphism of ringed small étale sites of Stacks 070R (2) carries a quasi-coherent 𝒪-module on X_étale to a quasi-coherent 𝒪-module on Y_étale.

The reduction to the previous statement is Descent, Proposition 03DX (2) at τ = étale, which this development has unconditionally: a quasi-coherent 𝒪-module 𝓖 on X_étale restricts to a quasi-coherent module on the affine objects by Stacks 0GZX (3) ⇒ (2), so the counit of the associated-module adjunction of X_étale is an isomorphism at 𝓖 by AlgebraicGeometry.SmallEtale.isIso_counit_of_affineRestriction, exhibiting 𝓖 as the associated module of the quasi-coherent 𝒪_X-module ε_{X,*}𝓖.

public theorem isQuasicoherentOnSite_smallPushforward
    [QuasiCompact (schemeHom B a)] [QuasiSeparated (schemeHom B a)]
    (𝓖 : SheafOfModules.{u} (structureSheaf B X.obj X.property))
    (h𝓖 : 𝓖.IsQuasicoherentOnSite) :
    ((smallPushforward B a).obj 𝓖).IsQuasicoherentOnSite

AlgebraicGeometry.SmallEtale.associatedModuleSmallPushforwardIsoOfQcqs, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtalePushforwardCartesian.lean, line 899. The attribute's comment: “part (3) at τ = étale, the commuting square f_{small, }(𝓕^a) ≅ (f_𝓕)^a, at one module”.

Stacks 03LC part (3) at τ = étale, the commuting square, at one module and with no hypothesis beyond quasi-compactness and quasi-separatedness of f and quasi-coherence of 𝓕:
`(f_*𝓕)^a ≅ f_{small, *}(𝓕^a)`.
This is AlgebraicGeometry.SmallEtale.associatedModuleSmallPushwardIso with its hypothesis discharged by AlgebraicGeometry.SmallEtale.isQuasicoherentOnSite_smallPushforward_associatedModule.

public def associatedModuleSmallPushforwardIsoOfQcqs
    [QuasiCompact (schemeHom B a)] [QuasiSeparated (schemeHom B a)] :
    (associatedModule B Y.obj Y.property).obj
        ((Scheme.Modules.pushforward (schemeHom B a)).obj 𝓕) ≅
      (smallPushforward B a).obj ((associatedModule B X.obj X.property).obj 𝓕)

AlgebraicGeometry.SmallZariski.lcAssociatedModulePullbackIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallZariskiPushforwardSquare.lean, line 464. The attribute's comment: “part (1) at τ = Zariski, for the small Zariski sites: (f^𝓖)^a ≅ f_small^(𝓖^a), for an arbitrary morphism of schemes of the site and arbitrary modules”.

Stacks 03LC part (1) at τ = Zariski, for the small Zariski sites. The equivalence of Stacks 03DX (2) at τ = Zariski is compatible with pullback: for f : T ⟶ S a morphism of schemes of the big Zariski site, with f_small : (T_Zar, 𝒪) ⟶ (S_Zar, 𝒪) the morphism of ringed sites of Stacks 070R (2) and 𝓖 an 𝒪_S-module,
`(f^*𝓖)^a ≅ f_small^*(𝓖^a)`,
naturally in 𝓖 and with no quasi-coherence hypothesis.

Here 𝓖 ↦ 𝓖^a is AlgebraicGeometry.SmallZariski.associatedModule, the functor of Definition 03DU (4) at τ = Zariski over the structure sheaf T/S ↦ Γ(T, 𝒪_T) of the small Zariski site — not the identity reading introduced in StacksFrontier.AlgebraicGeometry.Descent.AssociatedModule.SmallZariskiFullyFaithful. That distinction is what gives this declaration its content. AlgebraicGeometry.SmallZariski.associatedModulePullbackIso states the corresponding commutation over the identity reading, and it does not state this clause: the identity reading is pullback along the identity morphism of ringed sites, isomorphic to 𝟭, so that statement reads f_small^* ⋙ 𝟭 ≅ 𝟭 ⋙ f_small^* and is proved by whiskering the two unit isomorphisms and applying the two unitors, never touching the coefficient sheaf T/S ↦ Γ(T, 𝒪_T) that clause (2) is about. It is accordingly untagged.

The proof is SheafOfModules.pullbackSquareIso, Stacks 03D8 for a square: the geometric half of the square is AlgebraicGeometry.SmallZariski.lcBaseChangeOpensIso, that the base change of the object chosen over an open V of S is the object chosen over f⁻¹(V), and the ring half is AlgebraicGeometry.SmallZariski.lcStructureMap_comp_baseChangeOpensIso.

This is also Stacks 03FH part (2) for the small Zariski f_small of Remark 070R (2). That clause asserts (f^*𝓕)^a = f_sites^*𝓕^a for every f_sites the enumeration of Remark 070R lists, and the two clauses coincide at this f_sites: both are the statement that the associated-module functor of Definition 03DU (4) at τ = Zariski commutes with pullback along the morphism of ringed small Zariski sites of Stacks 070R (2). The companions are AlgebraicGeometry.BigFppfOver.associatedModuleBasePullbackIso — which carries the same two clauses on one declaration — for the big site at each of the five topologies, and AlgebraicGeometry.SmallEtale.associatedModuleBaseChangeIso for the small étale f_small. Those are every f_sites of the enumeration; the mixed-topology entries (Sch/X)_τ ⟶ (Sch/Y)_{τ'} with τ ≠ τ' of Topologies, Section 03FE are not claimed.

public noncomputable def lcAssociatedModulePullbackIso :
    Scheme.Modules.pullback (lcSchemeHom B f) ⋙ associatedModule B T.1 T.property ≅
      associatedModule B S.1 S.property ⋙
        SheafOfModules.pullback.{u} (lcStructureMapRing B f)

AlgebraicGeometry.SmallZariski.lcAssociatedModuleSmallPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallZariskiPushforwardSquare.lean, line 537. The attribute's comment: “part (3) at τ = Zariski, the commuting square f_{small,}(𝓕^a) ≅ (f_𝓕)^a, at one module and with no hypothesis on f”.

Stacks 03LC part (3) at τ = Zariski, the commuting square, at one module and with no hypothesis on f: for every 𝒪_T-module 𝓕,
`(f_*𝓕)^a ≅ f_{small, *}(𝓕^a)`.
The isomorphism is the counit of the associated-module adjunction of the small Zariski site of S at f_{small, *}(𝓕^a), which is an isomorphism at every module by AlgebraicGeometry.isIso_counit_smallZariskiAssociatedModuleAdjunction, precomposed with the associated module of the identification AlgebraicGeometry.SmallZariski.lcRestrictModuleSmallPushforwardAssociatedModuleIso of its restriction with f_*𝓕.

The source states the square for f quasi-compact and quasi-separated, where it is a square of the categories of quasi-coherent modules; the isomorphism of modules holds without those hypotheses, and AlgebraicGeometry.SmallZariski.lcIsQuasicoherentOnSite_smallPushforward supplies the quasi-coherence of the two corners under them.

public noncomputable def lcAssociatedModuleSmallPushforwardIso (𝓕 : (T.1).Modules) :
    (associatedModule B S.1 S.property).obj
        ((Scheme.Modules.pushforward (lcSchemeHom B f)).obj 𝓕) ≅
      (SheafOfModules.pushforward.{u} (lcStructureMapRing B f)).obj
        ((associatedModule B T.1 T.property).obj 𝓕)

AlgebraicGeometry.SmallZariski.lcAssociatedModuleSmallPushforwardNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallZariskiPushforwardSquare.lean, line 566. The attribute's comment: “part (3) at τ = Zariski, the commuting square of the part, as an isomorphism of functors Mod(𝒪_T) ⥤ Mod(S_Zar, 𝒪) and with no hypothesis on f”.

Stacks 03LC part (3) at τ = Zariski, the commuting square as an isomorphism of functors. The square
  Mod(𝒪_T) ------ f_* ------> Mod(𝒪_S)
      |                          |
   𝓕 ↦ 𝓕^a                   𝓖 ↦ 𝓖^a
      v                          v
  Mod(T_Zar, 𝒪) - f_{small,*} -> Mod(S_Zar, 𝒪)
commutes up to the canonical natural isomorphism, with no hypothesis on f and on all modules. Its components are AlgebraicGeometry.SmallZariski.lcAssociatedModuleSmallPushforwardIso; the proof is the same three steps, read as isomorphisms of functors: the unit of the associated-module adjunction of T_Zar, the mate square AlgebraicGeometry.SmallZariski.lcRestrictModuleBaseChangeIso, and the counit of the associated-module adjunction of S_Zar, which is an isomorphism of functors because AlgebraicGeometry.SmallZariski.restrictModule is an equivalence.

public noncomputable def lcAssociatedModuleSmallPushforwardNatIso :
    Scheme.Modules.pushforward (lcSchemeHom B f) ⋙ associatedModule B S.1 S.property ≅
      associatedModule B T.1 T.property ⋙
        SheafOfModules.pushforward.{u} (lcStructureMapRing B f)

AlgebraicGeometry.SmallZariski.lcIsQuasicoherentOnSite_smallPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallZariskiPushforwardSquare.lean, line 591. The attribute's comment: “part (3) at τ = Zariski, f_{small,*} carries quasi-coherent 𝒪-modules on the small Zariski site to quasi-coherent 𝒪-modules on the small Zariski site”.

Stacks 03LC part (3) at τ = Zariski, the preservation of quasi-coherence by f_{small, *}. For f : T ⟶ S quasi-compact and quasi-separated, the direct image along f_small : (T_Zar, 𝒪) ⟶ (S_Zar, 𝒪) of a module quasi-coherent on the small Zariski site of T is quasi-coherent on the small Zariski site of S.

Every such module is an associated module: its restriction to the opens of T is quasi-coherent by AlgebraicGeometry.SmallZariski.isQuasicoherent_restrictModule and the counit exhibits the module as the associated module of that restriction. Its direct image is then (f_*𝓕)^a by AlgebraicGeometry.SmallZariski.lcAssociatedModuleSmallPushforwardIso, and f_*𝓕 is quasi-coherent by Stacks 01LC, so that associated module is quasi-coherent on the site by Stacks 03DV (2).

public theorem lcIsQuasicoherentOnSite_smallPushforward
    [QuasiCompact (lcSchemeHom B f)] [QuasiSeparated (lcSchemeHom B f)]
    (𝒢 : SheafOfModules.{u} (structureSheaf B T.1 T.property))
    (h𝒢 : 𝒢.IsQuasicoherentOnSite) :
    ((SheafOfModules.pushforward.{u} (lcStructureMapRing B f)).obj 𝒢).IsQuasicoherentOnSite

AlgebraicGeometry.BigFppfOver.associatedModuleBasePullbackIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModulePullbackBigSites.lean, line 220. The attribute's comment: “part (1) at every τ ∈ {Zariski, étale, smooth, syntomic, fppf}, for the big sites: (f^𝓖)^a ≅ f_big^(𝓖^a), for an arbitrary morphism of schemes and arbitrary modules”.

Stacks 03FH, part (2), for the morphism of big sites f_big : ((Sch/X)_τ, 𝒪_X) ⟶ ((Sch/Y)_τ, 𝒪_Y) of Stacks 070R (1), at each of the five topologies τ ∈ {Zariski, étale, smooth, syntomic, fppf}. The associated module of a pullback is the pullback of the associated module, (f^*𝓕)^a ≅ f_big^*(𝓕^a), naturally in the 𝒪_Y-module 𝓕.

No hypothesis: the morphism of ringed sites is AlgebraicGeometry.BigFppfOver.baseChange together with AlgebraicGeometry.BigFppfOver.baseStructureComparison, and the two provisos of SheafOfModules.pullbackSquareIso are AlgebraicGeometry.BigFppfOver.opensBaseChangeIso, which is topology-free, and AlgebraicGeometry.BigFppfOver.comparisonComp_baseOpensBaseChangeIso.

Together with AlgebraicGeometry.SmallEtale.associatedModuleBaseChangeIso (the small étale f_small) and AlgebraicGeometry.SmallZariski.lcAssociatedModulePullbackIso (the small Zariski f_small, StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallZariskiPushforwardSquare.lean:458) this is every f_sites the enumeration of Remark 070R lists: clause (1) of that remark gives the big site at each of these five topologies, and clause (2) the small site at the two topologies that have one. (The small Zariski entry was formerly cited as AlgebraicGeometry.SmallZariski.associatedModulePullbackIso, which states the commutation over the identity reading of 𝓕 ↦ 𝓕^a and is a tautology about 𝟭; it is untagged, and naming it here made this enumeration a false completeness claim.)

public noncomputable def associatedModuleBasePullbackIso :
    Scheme.Modules.pullback f ⋙ baseAssociatedModule B X hX τ ≅
      baseAssociatedModule B Y hY τ ⋙
        SheafOfModules.pullback.{u} (baseStructureComparison B hX hY f τ)

AlgebraicGeometry.BigFppfOver.associatedModuleBaseObjPullbackIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModulePullbackBigSites.lean, line 237. The attribute's comment: “part (1) at every τ ∈ {Zariski, étale, smooth, syntomic, fppf}, for the big sites, at one module: f_big^(𝓖^a) ≅ (f^𝓖)^a”.

Stacks 03FH, part (2), at one module: (f^*𝓕)^a ≅ f_big^*(𝓕^a) for the morphism of big sites f_big at each of the five topologies, read off from AlgebraicGeometry.BigFppfOver.associatedModuleBasePullbackIso.

public noncomputable def associatedModuleBaseObjPullbackIso (𝓕 : Y.Modules) :
    (baseAssociatedModule B X hX τ).obj ((Scheme.Modules.pullback f).obj 𝓕) ≅
      (SheafOfModules.pullback.{u} (baseStructureComparison B hX hY f τ)).obj
        ((baseAssociatedModule B Y hY τ).obj 𝓕)

Stacks.Examples.QcohPushforward.exists_isEmpty_iso_bigPushforward_associatedModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/QuasiCoherentPushforward/BigSitePushforward.lean, line 225. The attribute's comment: “(2)”.

Stacks Project, Tag 03LC part (2). The equivalences 𝓖 ↦ 𝓖^a of Proposition 03DX part (1) are not compatible with pushforward in general: there are a morphism of schemes f : X ⟶ Y, quasi-compact and quasi-separated, and a quasi-coherent 𝒪_X-module 𝓕 — so that f_*𝓕 is quasi-coherent and (f_*𝓕)^a is defined — such that on every big site (both schemes lie in every one) and at every τ ∈ {Zariski, étale, smooth, syntomic, fppf}
`f_{big, *}(𝓕^a) ≇ (f_*𝓕)^a`
as 𝒪-modules on (Sch/Y)_τ, where f_{big, *} is the pushforward along the morphism of ringed big sites f_big : ((Sch/X)_τ, 𝒪) ⟶ ((Sch/Y)_τ, 𝒪) of Stacks 070R (1).

The witness is the source's: the punctured plane U = Spec k[t][X] ∖ V(X, t) over Spec k[t][X], with k = ULift ℚ, and 𝓕 = 𝒪_U; the two sides differ over the origin Spec k ⟶ Spec k[t][X], which is where the base-change map of Stacks.Examples.QcohPushforward.exists_not_isIso_baseChangeNatTrans fails.

theorem exists_isEmpty_iso_bigPushforward_associatedModule :
    ∃ (X Y : Scheme.{u}) (f : X ⟶ Y) (F : X.Modules),
      QuasiCompact f ∧ QuasiSeparated f ∧ F.IsQuasicoherent ∧
        ((Scheme.Modules.pushforward f).obj F).IsQuasicoherent ∧
        (∀ B : BigFppfSite.{u}, B.Contains X ∧ B.Contains Y) ∧
        ∀ (B : BigFppfSite.{u}) (hX : B.Contains X) (hY : B.Contains Y) (τ : SiteKind),
          IsEmpty ((SheafOfModules.pushforward.{u}
              (BigFppfOver.baseStructureComparison B hX hY f τ)).obj
              ((BigFppfOver.baseAssociatedModule B X hX τ).obj F) ≅
            (BigFppfOver.baseAssociatedModule B Y hY τ).obj
              ((Scheme.Modules.pushforward f).obj F))

Declarations registered for the tag:

AlgebraicGeometry.pushforward_isQuasicoherent, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/ObjectFunctoriality.lean, line 455 (StacksFrontier): “part (3), ordinary pushforward preserves quasi-coherence”.

Tag 071N, a lemma

Tag 071N in the Stacks Project.

AlgebraicGeometry.SmallEtale.higherDirectImageAssociatedModuleIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtaleHigherDirectImageQcqs.lean, line 328. The attribute's comment: “the ÉTALE topology of the two the tag states ("for either the étale or Zariski topology"): for f quasi-compact and quasi-separated, in every degree i, as an isomorphism of functors on the quasi-coherent O_T-modules (hence natural in F). The ZARISKI topology is SmallZariski.higherDirectImageAssociatedModulePlusIntIso”.

For a morphism f : T ⟶ S of schemes of a big étale site whose underlying morphism of schemes is quasi-compact and quasi-separated, and every degree i, there is a canonical isomorphism

R ⁱ f_{small, *}(𝓕ᵃ) ≅ (R ⁱ f_* 𝓕)ᵃ

natural in the quasi-coherent 𝒪_T-module 𝓕, where f_small = ε_f is the morphism of small étale ringed sites of [Stacks, Tag 070R] (2), R ⁱ f_{small, *} is the right derived functor of its direct image of sheaves of modules, R ⁱ f_* that of the direct image of 𝒪_T-modules, and 𝓖 ↦ 𝓖ᵃ the associated module of [Stacks, Tag 03DU] (4) at τ = étale.

def higherDirectImageAssociatedModuleIso (i : ℕ) :
    associatedModuleOnQuasicoherent B (X := X) ⋙
        (SheafOfModules.pushforward.{u} (smallEtaleStructureMapRing B a)).rightDerived i ≅
      Stacks.Cohomology.AffineBase.quasicoherentInclusion X.obj ⋙
        (Scheme.Modules.pushforward (schemeHom B a)).rightDerived i ⋙
          associatedModule B Y.obj Y.property

AlgebraicGeometry.SmallEtale.higherDirectImageAssociatedSheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtaleZariskiBaseChange.lean, line 148. The attribute's comment: “the étale topology”.

Descent, Lemma 071N, for the étale topology: for a quasi-compact and quasi-separated morphism a of the big étale site and a quasi-coherent 𝒪_X-module 𝓕, R^p a_{small,*}(𝓕^a) ≅ (R^p a_* 𝓕)^a on the small étale site of Y, assembled by AlgebraicGeometry.SmallEtale.higherDirectImageAssociatedSheafIsoOfZariski from AlgebraicGeometry.SmallEtale.baseChangeCohomologyIso and its naturality.

def higherDirectImageAssociatedSheafIso (𝓕 : X.obj.Modules) [𝓕.IsQuasicoherent] (p : ℕ) :
    ((Stacks.HigherDirectImage.pushforward.{u, u} B a).rightDerived p).obj
        ((associatedSheaf B X).obj 𝓕) ≅
      (associatedSheaf B Y).obj
        (((Scheme.Modules.pushforward (schemeHom B a)).rightDerived p).obj 𝓕)

AlgebraicGeometry.SmallZariski.higherDirectImageAssociatedModulePlusIntIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallZariskiHigherDirectImageIntDegree.lean, line 181. The attribute's comment: “the ZARISKI topology of the two the tag states ("for either the étale or Zariski topology"), at every integer degree and naturally in the module, with the tag's hypotheses on f and on the module dropped rather than weakened. The ÉTALE topology, at the tag's hypotheses (f quasi-compact and quasi-separated, F quasi-coherent), in every degree and naturally in F, is SmallEtale.higherDirectImageAssociatedModuleIso”.

The Zariski half of [Stacks, Tag 071N] at an arbitrary integer degree. For every i : ℤ,

R ⁱ f_{small, *}(𝓕^a) ≅ (R ⁱ f_* 𝓕)^a,

naturally in 𝓕, in the ℤ-indexed derived-category convention of [Stacks, Tag 05U4] that the tag is read in.

In degrees 0 ≤ i this is AlgebraicGeometry.SmallZariski.higherDirectImageAssociatedModulePlusIntIsoOfNonneg, which is where the content is. In degrees i < 0 both sides are zero objects and this is the unique isomorphism between them; the statement is true there but says nothing, so a consumer that wants the comparison should prefer the nonnegative-degree form.

No hypothesis is placed on f or on 𝓕. [Stacks, Tag 071N] states the comparison for f quasi-compact and quasi-separated and 𝓕 quasi-coherent; those are what the tag needs in order that (R ⁱ f_* 𝓕)^a be formed on the étale site, where 𝓕 ↦ 𝓕^a is only defined on the quasi-coherent modules. On the Zariski site it is defined on all of Mod(𝒪_T) and the comparison holds with nothing assumed, so this is the tag's Zariski clause with its hypotheses dropped, not weakened.

public noncomputable def higherDirectImageAssociatedModulePlusIntIso (i : ℤ) :
    associatedModule B T.1 T.property ⋙
        (SheafOfModules.pushforward.{u} (structureMapRing B f)).rightDerivedPlus i ≅
      (Scheme.Modules.pushforward (schemeHom B f)).rightDerivedPlus i ⋙
        associatedModule B S.1 S.property

Declarations registered for the tag:

isQuasicoherent_higherDirectImage registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/HigherDirectImageQcqs/UniformVanishing.lean, line 601 (StacksFrontier): “quasi-coherence of the higher direct images”.

Sources

LeanStacks.Adequate.BigSite.coproductCechComparison · AlgebraicGeometry.IsStandardCovering.singleton_sigmaDesc_mem_fpqcPrecoverage · AlgebraicGeometry.IsStandardCovering.singleton_sigmaDesc_mem_precoverage · AlgebraicGeometry.IsStandardCovering.sieve_sigmaDesc_mem_topology · AlgebraicGeometry.isIso_cechComplexMap_coproductRefinement_over · AlgebraicGeometry.isIso_cechComplexMap_coproductRefinement_smallEtale · AlgebraicGeometry.IsStandardCovering.sieve_sigmaDesc_mem_smallEtaleTopology · AlgebraicGeometry.isIso_cechComplexMap_coproductRefinement_smallZariski

Section35.10 Quasi-coherent sheaves and topologies, II #

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

Tag 0GNA, a lemma

Tag 0GNA in the Stacks Project.

AlgebraicGeometry.SmallEtale.isFlatMapULift_inverseImageStructureMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtaleFlatInverseImage.lean, line 354.

Stacks 0GNA. The morphism of ringed sites ε = id_{small, étale, Zar} : S_étale → S_Zar is flat: 𝒪_{S_étale} is a flat module over ε⁻¹𝒪_{S_Zar}, the flatness being asserted for the structure map AlgebraicGeometry.SmallEtale.inverseImageStructureMap of ε in inverse-image form.

This is also the first assertion of Stacks 08H8, which states exactly that the ε of Equation 75.4.0.1 — AlgebraicGeometry.SmallEtale.toZariskiRingedToposHom, carrying Stacks 08H7 — is a flat morphism of ringed sites, and cites Descent, Lemma 35.10.1, which is 0GNA, for it. The second assertion of 08H8, exactness of ε^*, is carried by AlgebraicGeometry.SmallEtale.exactFunctor_pullbackModules_toZariski. The third, the implication ε^*𝓕 = 0 ⟹ 𝓕 = 0, is not carried by this statement and is not available in the library; the attribute clause records that scope.

public theorem isFlatMapULift_inverseImageStructureMap :
    AlgebraicGeometry.SheafOfModules.IsFlatMapULift.{u, u + 1, u}
      (inverseImageStructureMap B S hS)

Tag 06VE, a lemma

Tag 06VE in the Stacks Project.

AlgebraicGeometry.BigFppfOver.baseAssociatedModuleTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/BaseAssociatedModuleTensor.lean, line 177. The attribute's comment: “part (7), big site (Sch/S)_τ at every τ, for arbitrary 𝒪_S-modules”.

Descent, Lemma 06VE (7) for the big τ-site, at every τ ∈ {Zariski, étale, smooth, syntomic, fppf}. The comparison 𝓕 ↦ 𝓕^a of Descent, Proposition 03DX carries a tensor product of 𝒪_S-modules to the tensor product of their images: (𝓗 ⊗_{𝒪_S} 𝓘)^a ≅ 𝓗^a ⊗_𝒪 𝓘^a in Mod((Sch/S)_τ, 𝒪).

This is Stacks 03EL, Stacks.SheafOfModules.pullbackTensorIso, for the morphism of ringed topoi attached to the comparison of Stacks 070U, carried across AlgebraicGeometry.BigFppfOver.pullbackModulesIsoBaseAssociatedModule.

No hypothesis is carried, and in particular quasi-coherence is not needed: the statement holds for arbitrary 𝒪_S-modules. 06VE states it for QCoh(𝒪_S) only because that is the source category on which its functor is an equivalence, so this is the clause with its hypothesis dropped rather than added to.

The tensor products are (Stacks.SheafOfModules.Tensor.sheafTensor O).obj H, the sheafification of the objectwise tensor product of the underlying presheaves of modules (Stacks 05NB); that functor's value agrees with the bifunctor of Tag 01CA by AlgebraicGeometry.BigFppfOver.tensorSheafBifunctor_obj_eq.

public def baseAssociatedModuleTensorIso (τ : SiteKind) (H I : S.Modules) :
    (baseAssociatedModule B S hS τ).obj
        (((Stacks.SheafOfModules.Tensor.sheafTensor S.sheaf).obj H).obj I) ≅
      ((Stacks.SheafOfModules.Tensor.sheafTensor
            (FibredSite.baseStructureSheaf B S hS τ)).obj
          ((baseAssociatedModule B S hS τ).obj H)).obj
        ((baseAssociatedModule B S hS τ).obj I)

AlgebraicGeometry.BigFppfOver.essImage_X₂_of_shortExact_big, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/BaseExtensionEssImage.lean, line 118. The attribute's comment: “part (10), big site (Sch/S)_τ at every τ ∈ {Zariski, étale, smooth, syntomic, fppf}, for the PULLBACK-defined functor 𝓕 ↦ 𝓕ᵃ of Remark 03FH. The same clause for the sections-defined 𝓕ᵃ of Definition 03DU (3) is exists_isoSections_X₂_of_shortExact_big; the two sheaves are identified by baseAssociatedModuleIsoSections, Stacks 070S (1). The clause read as "the middle term is quasi-coherent", which names no functor, is clause (4) of Stacks 0GNC and sits on isQuasicoherentOnSite_shortExact_X₂_all”.

Stacks 06VE (10) on the big site (Sch/S)_τ, at every τ ∈ {Zariski, étale, smooth, syntomic, fppf} and with no hypothesis. Given a short exact sequence 0 → 𝓕₁ᵃ → 𝓔 → 𝓕₂ᵃ → 0 of 𝒪-modules on (Sch/S)_τ whose outer terms are quasi-coherent — which at every τ is the same as their being 𝓕ᵃ's, by Descent, Proposition 03DX (1) — the middle term 𝓔 is itself in the essential image of 𝓕 ↦ 𝓕ᵃ : QCoh(𝒪_S) ⥤ Mod((Sch/S)_τ, 𝒪), namely of 𝓔|_{S_Zar}.

The source's three steps are StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/BaseExtensionClosure.lean; of the two hypotheses they carry, essential surjectivity is AlgebraicGeometry.BigFppfOver.baseQuasicoherentIsEssImageAssociatedModule and right exactness of restriction to S_Zar is AlgebraicGeometry.BigFppfOver.epi_baseRestrictModule_map_all.

This is the clause for the pullback-defined 𝓕 ↦ 𝓕ᵃ of Remark 03FH; AlgebraicGeometry.BigFppfOver.exists_isoSections_X₂_of_shortExact_big is it for the sections-defined 𝓕ᵃ of Definition 03DU (3), which is the sheaf the source constructs.

public theorem essImage_X₂_of_shortExact_big (τ : SiteKind)
    {C : ShortComplex (SheafOfModules.{u} (FibredSite.baseRingStructureSheaf B S hS τ))}
    (hC : C.ShortExact) (h₁ : C.X₁.IsQuasicoherentOnSite) (h₃ : C.X₃.IsQuasicoherentOnSite) :
    (baseAssociatedModuleQcoh B S hS τ).essImage C.X₂

AlgebraicGeometry.BigFppfOver.exists_isoSections_X₂_of_shortExact_big, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/BaseExtensionEssImage.lean, line 176. The attribute's comment: “part (10), big site (Sch/S)_τ at every τ ∈ {Zariski, étale, smooth, syntomic, fppf}, for the SECTIONS-defined 𝓕ᵃ of Definition 03DU (3) — the τ-sheafification of (f : T → S) ↦ Γ(T, f^*𝓕). The same clause for the pullback-defined functor of Remark 03FH is essImage_X₂_of_shortExact_big; the two sheaves are identified by baseAssociatedModuleIsoSections, Stacks 070S (1)”.

Stacks 06VE (10) on the big site (Sch/S)_τ at every τ, for the sheaf the source constructs. Given a short exact sequence 0 → 𝓕₁ᵃ → 𝓔 → 𝓕₂ᵃ → 0 of 𝒪-modules on (Sch/S)_τ whose outer terms are quasi-coherent, there is a quasi-coherent 𝒪_S-module 𝓕 with 𝓔 ≅ 𝓕ᵃ, where 𝓕ᵃ is the sections-defined associated module of Stacks Definition 03DU (3) — the τ-sheafification of (f : T → S) ↦ Γ(T, f^*𝓕).

AlgebraicGeometry.BigFppfOver.essImage_X₂_of_shortExact_big is the same clause for the pullback-defined 𝓕ᵃ of Remark 03FH; this is it read through AlgebraicGeometry.BigFppfOver.baseAssociatedModuleIsoSections, Stacks 070S (1). The witness is 𝓕 = 𝓔|_{S_Zar}, quasi-coherent by AlgebraicGeometry.BigFppfOver.isQuasicoherent_baseRestrictModule_X₂, and the isomorphism is AlgebraicGeometry.BigFppfOver.sectionsIso_X₂_of_shortExact_big.

public theorem exists_isoSections_X₂_of_shortExact_big (τ : SiteKind)
    {C : ShortComplex (SheafOfModules.{u} (FibredSite.baseRingStructureSheaf B S hS τ))}
    (hC : C.ShortExact) (h₁ : C.X₁.IsQuasicoherentOnSite) (h₃ : C.X₃.IsQuasicoherentOnSite) :
    ∃ F : (SheafOfModules.isQuasicoherent S.ringCatSheaf).FullSubcategory,
      Nonempty (C.X₂ ≅ (PresheafOfModules.sheafification.{u}
          (𝟙 (FibredSite.baseRingStructureSheaf B S hS τ).obj)).obj
        (sectionsPresheafOfModules B S hS F.obj))

AlgebraicGeometry.BigFppfOver.fullyFaithfulBaseAssociatedModuleQcoh, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/BaseFullyFaithful.lean, line 208. The attribute's comment: “part (1), big site, every τ”.

Stacks 0GN7 for the big site, and clause (1) of Stacks 06VE for it. For every τ ∈ {Zariski, étale, smooth, syntomic, fppf} the functor 𝓕 ↦ 𝓕^a of Definition 03DU, from the quasi-coherent 𝒪_S-modules to the 𝒪-modules on the big site (Sch/S)_τ, is fully faithful.

The two tags assert one thing of one functor, and the clause strings record the scope this declaration proves — on one source line, because a tag registry that reads the attributes matches a second stacks clause only when it is on the same line as the first, and two clause strings plus the attribute syntax do not fit in a hundred characters unless both are short. The 0GN7 string therefore no longer ends ; small site S_τ untreated: that is information about where else the tag is registered, not about the scope proved, and big site (Sch/S)_τ, every τ already states the scope exactly. The other registrations are named in the last paragraph below.

06VE's first functor is QCoh(𝒪_S) → Mod((Sch/S)_τ, 𝒪), whose target is Mod — which is the target below on the nose, SheafOfModules over the structure sheaf of (Sch/S)_τ — so clause (1) of 06VE needs no reading through a subcategory. 0GN7 spells the same functor with target QCoh((Sch/S)_τ, 𝒪), and that too is the same statement: full faithfulness of a functor into a category is full faithfulness into any full subcategory containing its image, and the image does land in QCoh by Stacks 03DV (1), AlgebraicGeometry.BigFppfOver.isQuasicoherentOnSite_baseAssociatedModule_of_isQuasicoherent.

What is not claimed by either tag here is the source's second functor, QCoh(𝒪_S) → Mod(S_τ, 𝒪) into the small site of S for τ ∈ {Zariski, étale} — a different construction, Definition 03DU (4). It is claimed elsewhere, and 0GN7 quantifies over nothing beyond these: Definition 03DU gives a small site only at τ ∈ {Zariski, étale}, so this declaration together with AlgebraicGeometry.SmallZariski.fullyFaithfulAssociatedModuleQcoh (StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallZariskiRealFullyFaithful.lean) and AlgebraicGeometry.SmallEtale.fullyFaithfulAssociatedModuleQcoh' (StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtaleLocalBijectivity.lean) is every functor the lemma speaks of. At τ = Zariski the sections-defined form of the functor carries the tag too, as AlgebraicGeometry.SmallZariski.fullyFaithfulAssociatedSheafFunctor.

(The small étale functor is AlgebraicGeometry.SmallEtale.associatedModule, in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtaleRingedSite.lean, and its full faithfulness rests on AlgebraicGeometry.SmallEtale.unitIsoOnQuasicoherent of SmallEtaleLocalBijectivity.lean, which proves AlgebraicGeometry.SmallEtale.UnitIsoOnQuasicoherent with no hypothesis.)

public noncomputable def fullyFaithfulBaseAssociatedModuleQcoh (τ : SiteKind) :
    (baseAssociatedModuleQcoh B S hS τ).FullyFaithful

AlgebraicGeometry.AssociatedModuleNotExact.not_mono_map_two_nsmul_qcoh, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/BigSiteNotExact.lean, line 322. The attribute's comment: “part (6), the witness: at S = Spec(ℤ), on every big site and at every τ, the monomorphism 2 : 𝒪_S → 𝒪_S of QCoh(𝒪_S) has non-monomorphic image”.

Stacks 06VE (6), the witness. For S = Spec(ℤ), every big fppf site containing it and every τ ∈ {Zariski, étale, smooth, syntomic, fppf}, the monomorphism 2 : 𝒪_S → 𝒪_S of QCoh(𝒪_S) is carried by 𝓕 ↦ 𝓕^a to a morphism of Mod((Sch/S)_τ, 𝒪) that is not a monomorphism.

This is the example the source gives: 2 : 𝔽₂ → 𝔽₂ is not injective and Spec(𝔽₂) is an object of (Sch/S)_τ. Paired with AlgebraicGeometry.AssociatedModuleNotExact.mono_two_nsmul_unitQcoh, which says the source morphism is a monomorphism, it is the whole of clause (6).

public theorem not_mono_map_two_nsmul_qcoh :
    ¬ Mono ((associatedModuleQcoh B τ).map (2 • 𝟙 unitQcoh.{u}))

AlgebraicGeometry.AssociatedModuleNotExact.not_preservesMonomorphisms_baseAssociatedModuleQcoh, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/BigSiteNotExact.lean, line 333. The attribute's comment: “part (6), as the failure to preserve monomorphisms, at S = Spec(ℤ) on every big site and at every τ”.

Stacks 06VE (6), as the failure to preserve monomorphisms.

public theorem not_preservesMonomorphisms_baseAssociatedModuleQcoh :
    ¬ (associatedModuleQcoh B τ).PreservesMonomorphisms

AlgebraicGeometry.AssociatedModuleNotExact.not_preservesFiniteLimits_baseAssociatedModuleQcoh, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/BigSiteNotExact.lean, line 349. The attribute's comment: “part (6): the functor QCoh(𝒪_S) → Mod((Sch/S)_τ, 𝒪) is not left exact, at S = Spec(ℤ), on every big site and at every τ; with part (4) this is the failure of exactness”.

Stacks 06VE (6). The functor QCoh(𝒪_S) → Mod((Sch/S)_τ, 𝒪), 𝓕 ↦ 𝓕^a, is not exact in general: at S = Spec(ℤ) it does not preserve finite limits, on every big fppf site and at every τ ∈ {Zariski, étale, smooth, syntomic, fppf}.

By clause (4) the functor is always right exact, so this is exactly the failure of exactness the source asserts. A functor preserving finite limits preserves pullbacks, hence monomorphisms, which not_preservesMonomorphisms_baseAssociatedModuleQcoh of this namespace rules out.

public theorem not_preservesFiniteLimits_baseAssociatedModuleQcoh :
    ¬ Limits.PreservesFiniteLimits (associatedModuleQcoh B τ)

AlgebraicGeometry.AssociatedModuleSheafHomNotCommute.exists_isQuasicoherent_not_iso_sheafHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/BigSiteSheafHomNotCommute.lean, line 395. The attribute's comment: “part (9): the sheaf Hom does NOT commute with 𝓕 ↦ 𝓕ᵃ on the big site, at S = Spec ℤ, and not even when 𝓕 is of finite presentation”.

Stacks 06VE (9). Given two quasi-coherent 𝒪_S-modules 𝓕, 𝓖 one does not have (SheafHom_{𝒪_S}(𝓕, 𝓖))^a = SheafHom_𝒪(𝓕^a, 𝓖^a) in Mod((Sch/S)_τ, 𝒪) in general: at S = Spec(ℤ), on every big fppf site containing it and at every τ ∈ {Zariski, étale, smooth, syntomic, fppf}, the two are not isomorphic, for 𝓕 = Coker(2 : 𝒪_S → 𝒪_S) and 𝓖 = 𝒪_S.

This is the example the source gives, and the two halves are the two named statements of this file: the left-hand side is a zero object (AlgebraicGeometry.AssociatedModuleSheafHomNotCommute.isZero_associatedModule_sheafHomModules) and the right-hand side is not (…not_isZero_internalHomSheaf), the latter for the very reason clause (6) fails — Spec(𝔽₂) is an object of (Sch/S)_τ.

𝓕 is asserted to be of finite presentation, which is the source's "even if 𝓕 is of finite presentation": the failure is not repaired by the hypothesis under which clause (8) holds on the small sites. It holds by construction, 𝓕 being the cokernel of a map 𝒪_S → 𝒪_S (Stacks 0H96, Stacks.SheafOfModules.isFinitePresentation_cokernel). See the implementation notes for why the conjunct is needed and not merely true.

All three modules in play — 𝓕, 𝓖 and SheafHom_{𝒪_S}(𝓕, 𝓖) — are asserted to be quasi-coherent, so both sides of the clause are values of the functor QCoh(𝒪_S) → Mod((Sch/S)_τ, 𝒪) the clause is about and not of some extension of it to all 𝒪_S-modules; that functor is AlgebraicGeometry.AssociatedModuleNotExact.associatedModuleQcoh, and AlgebraicGeometry.AssociatedModuleSheafHomNotCommute.associatedModuleQcoh_obj says it agrees with the associatedModule written here on every quasi-coherent module, on the nose.

The universe lift is the canonical fully faithful Stacks.SheafOfModules.moduleULift: the internal Hom of Stacks 03EM on the big site raises the module universe by construction, so the two sides of the clause are objects of two different categories. See the implementation notes of this file; the zero/nonzero dichotomy above is universe-free and is the real content.

public theorem exists_isQuasicoherent_not_iso_sheafHom :
    ∃ F G : specInt.{u}.Modules, F.IsQuasicoherent ∧ G.IsQuasicoherent ∧
      F.IsFinitePresentation ∧ (sheafHomModules F G).IsQuasicoherent ∧
      ¬ Nonempty ((Stacks.SheafOfModules.moduleULift.{u + 1, u}
            (bigStructureSheaf B τ)).obj
            ((associatedModule B τ).obj (sheafHomModules F G)) ≅
          RingedSite.internalHomSheaf
            (BigFppfOver.baseRingedSite B specInt.{u} (contains_specInt B) τ)
            ((associatedModule B τ).obj F) ((associatedModule B τ).obj G))

AlgebraicGeometry.SmallEtale.associatedModuleTensorBifunctorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtaleAssociatedModuleTensorBifunctor.lean, line 99. The attribute's comment: “part (7), small site at τ = étale, for all 𝒪_S-modules; bifunctor form, whose components are the objectwise form in which the source states the clause”.

Stacks 06VE (7) at τ = étale. The functor 𝓕 ↦ 𝓕^a into the 𝒪-modules of the small étale site of S carries the tensor product of two 𝒪_S-modules to the tensor product of their images:

(𝓕 ⊗_{𝒪_S} 𝓖)^a ≅ 𝓕^a ⊗_𝒪 𝓖^a,

naturally in the pair (𝓕, 𝓖), with no hypothesis on 𝓕 or 𝓖.

This is Modules on Sites, Lemma 03EL — Stacks.SheafOfModules.pullbackTensorIso — for the morphism of ringed topoi underlying ε : (S_étale, 𝒪) ⟶ (S_Zar, 𝒪_S) of Stacks 070R and 08H7, conjugated on both sides by AlgebraicGeometry.SmallEtale.pullbackModulesToZariskiIso. Its component at a pair is the objectwise form in which the source states the clause, AlgebraicGeometry.SmallEtale.associatedModuleTensorIso, by AlgebraicGeometry.SmallEtale.associatedModuleTensorBifunctorIso_app.

With AlgebraicGeometry.SmallZariski.associatedModuleTensorIsoOfComparison at τ = Zariski and AlgebraicGeometry.BigFppfOver.baseAssociatedModuleTensorIso on the big sites, clause (7) is covered at every functor the lemma quantifies over.

def associatedModuleTensorBifunctorIso :
    Functor.uncurry.obj (Stacks.SheafOfModules.Tensor.sheafTensor.{u, u, u, u, u}
          S.zariskiRingedSite.toRingedTopos.O) ⋙ associatedModule B S hS ≅
      Functor.prod (associatedModule B S hS) (associatedModule B S hS) ⋙
        Functor.uncurry.obj (Stacks.SheafOfModules.Tensor.sheafTensor.{u + 1, u, u, u, u}
          (smallEtaleRingedSite B S hS).toRingedTopos.O)

AlgebraicGeometry.SmallEtale.fullyFaithfulAssociatedModuleQcoh', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtaleLocalBijectivity.lean, line 660. The attribute's comment: “part (1), small site at τ = étale”.

The small étale half of Stacks 0GN7 and of Stacks 06VE (1), with no hypothesis at all: the functor 𝓕 ↦ 𝓕^a of Definition 03DU (4) at τ = étale, from the quasi-coherent 𝒪_S-modules to the 𝒪-modules on S_étale, is fully faithful.

public noncomputable def fullyFaithfulAssociatedModuleQcoh' :
    (associatedModuleQcoh B S hS).FullyFaithful

AlgebraicGeometry.SmallEtale.essImage_X₂_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtaleRestrictionRightExact.lean, line 279. The attribute's comment: “part (10), small site at τ = étale”.

Stacks 06VE (10) at τ = étale. Given a short exact sequence 0 → 𝓕₁^a → 𝓔 → 𝓕₂^a → 0 of 𝒪-modules on the small étale site of S — the outer terms being given as quasi-coherent, which at τ = étale is the same as being in the essential image, by Stacks 03DX (2) — the middle term 𝓔 is in the essential image of QCoh(𝒪_S) ⥤ Mod(S_étale, 𝒪), 𝓕 ↦ 𝓕^a, namely of 𝓔|_{S_Zar}.

The source's three steps are StacksFrontier.AlgebraicGeometry.Descent.AssociatedModule.SmallEtaleExtensionReduction; the one they carried, right exactness of ε_*, is epi_restrictModule_map above.

public theorem essImage_X₂_of_shortExact (hC : C.ShortExact)
    (h₁ : C.X₁.IsQuasicoherentOnSite) (h₃ : C.X₃.IsQuasicoherentOnSite) :
    (associatedModuleQcoh B S hS).essImage C.X₂

AlgebraicGeometry.SmallEtale.associatedModuleInternalHomSheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallSiteSheafHomComparison.lean, line 182. The attribute's comment: “part (8), small site at τ = étale, for the pullback-defined functor 𝓕 ↦ 𝓕ᵃ of Remark 03FH and Tag 03EM's internal Hom on S_étale”.

Stacks 06VE (8) at τ = étale. For 𝒪_S-modules 𝓕, 𝓖 on a scheme S with 𝓖 quasi-coherent and 𝓕 of finite presentation — Stacks 03DL (7) on the site of opens of S —

(SheafHom_{𝒪_S}(𝓕, 𝓖))^a ≅ SheafHom_𝒪(𝓕^a, 𝓖^a) in Mod(S_étale, 𝒪),

where 𝓕 ↦ 𝓕^a is the functor of Definition 03DU (4) at τ = étale in its pullback description of Remark 03FH, AlgebraicGeometry.SmallEtale.associatedModule, and the internal Hom on the right is Tag 03EM's on the small étale site.

The proof is the one the module docstring describes: the mate of clause (7), AlgebraicGeometry.SmallEtale.restrictModuleInternalHomIso, computes the Zariski restriction of the right-hand side as SheafHom_{𝒪_S}(𝓕, ε_* 𝓖^a); the unit of the associated-module adjunction is an isomorphism at the quasi-coherent 𝓖, Stacks 0GN7, so that restriction is SheafHom_{𝒪_S}(𝓕, 𝓖); and the counit is an isomorphism at the right-hand side because that internal Hom is quasi-coherent, which is clause (6) of Stacks 0GNB and is where the finite presentation of 𝓕 is spent, through Stacks 03DO for the clause 03DL (7), AlgebraicGeometry.SmallEtale.isFinitePresentationOnSite_associatedModule.

Quasi-coherence of 𝓕 is not needed.

def associatedModuleInternalHomSheafIso (𝓕 𝓖 : S.Modules)
    (h𝓖 : SheafOfModules.IsQuasicoherent 𝓖)
    (h𝓕 : SheafOfModules.IsFinitePresentationOnSite 𝓕) :
    (associatedModule B S hS).obj
        (Stacks.AlgebraicGeometry.InternalHomModules.sheafHomModules 𝓕 𝓖) ≅
      internalHomSheaf B S hS ((associatedModule B S hS).obj 𝓕)
        ((associatedModule B S hS).obj 𝓖)

AlgebraicGeometry.SmallZariski.associatedModuleInternalHomSheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallSiteSheafHomComparisonZariski.lean, line 155. The attribute's comment: “part (8), small site at τ = Zariski, for the pullback-defined functor 𝓕 ↦ 𝓕ᵃ of Remark 03FH and Tag 03EM's internal Hom on S_Zar, for all 𝒪_S-modules”.

Stacks 06VE (8) at τ = Zariski. For 𝒪_S-modules 𝓕 and 𝓖 on a scheme S,

(SheafHom_{𝒪_S}(𝓕, 𝓖))^a ≅ SheafHom_𝒪(𝓕^a, 𝓖^a) in Mod(S_Zar, 𝒪),

where 𝓕 ↦ 𝓕^a is the functor of Definition 03DU (4) at τ = Zariski in its pullback description of Remark 03FH, AlgebraicGeometry.SmallZariski.associatedModule, and the internal Hom on the right is Tag 03EM's on the small Zariski site of schemes over S.

The proof is the source's: the mate of clause (7), AlgebraicGeometry.SmallZariski.restrictModuleInternalHomIso, computes the restriction of the right-hand side as SheafHom_{𝒪_S}(𝓕, ε_* 𝓖^a); the unit of the associated-module adjunction identifies ε_* 𝓖^a with 𝓖, so that restriction is the left-hand side's source; and the counit identifies the right-hand side with the associated module of its own restriction. Both unit and counit are isomorphisms because 𝓕 ↦ 𝓕^a is an equivalence at τ = Zariski, Stacks 03FG — which is the content of the source's one-sentence argument, and the only thing clause (8) needs at this topology.

Neither quasi-coherence nor finite presentation of 𝓕 is assumed: they are what the clause needs at τ = étale, where they buy the two isomorphisms that come for free here.

def associatedModuleInternalHomSheafIso (𝓕 𝓖 : S.Modules) :
    (associatedModule B S hS).obj
        (Stacks.AlgebraicGeometry.InternalHomModules.sheafHomModules 𝓕 𝓖) ≅
      RingedSite.internalHomSheafSmall.{u} (smallZariskiRingedSite B S hS)
        ((associatedModule B S hS).obj 𝓕) ((associatedModule B S hS).obj 𝓖)

AlgebraicGeometry.SmallZariski.preservesColimitsOfShape_discrete_associatedModuleQcohOfComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallZariskiRealClosureProperties.lean, line 188. The attribute's comment: “part (2), small site at τ = Zariski”.

Stacks 06VE (2) for the small site at τ = Zariski. The functor QCoh(𝒪_S) ⥤ Mod(S_Zar, 𝒪), 𝓕 ↦ 𝓕^a of Definition 03DU (4), commutes with direct sums: a direct sum is a colimit over a discrete index category, so this is the discrete case of clause (3).

Definition 03DU gives a small site only for τ ∈ {Zariski, étale}, so with AlgebraicGeometry.SmallEtale.preservesColimitsOfShape_discrete_associatedModuleQcoh (the small site at τ = étale) and AlgebraicGeometry.BigFppfOver.preservesColimitsOfShape_discrete_baseAssociatedModuleQcoh (the big site, every τ) this completes the covering set of the clause.

public theorem preservesColimitsOfShape_discrete_associatedModuleQcohOfComparison (I : Type u) :
    PreservesColimitsOfShape (Discrete I)
      (AlgebraicGeometry.SmallZariski.associatedModuleQcoh B S hS)

AlgebraicGeometry.SmallZariski.preservesColimitsOfSize_associatedModuleQcohOfComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallZariskiRealClosureProperties.lean, line 199. The attribute's comment: “part (3), small site at τ = Zariski”.

Stacks 06VE (3) for the small site at τ = Zariski. The functor QCoh(𝒪_S) ⥤ Mod(S_Zar, 𝒪), 𝓕 ↦ 𝓕^a of Definition 03DU (4), commutes with all colimits indexed at the size of the scheme.

Scope as on preservesColimitsOfShape_discrete_associatedModuleQcohOfComparison.

public theorem preservesColimitsOfSize_associatedModuleQcohOfComparison :
    PreservesColimitsOfSize.{u, u}
      (AlgebraicGeometry.SmallZariski.associatedModuleQcoh B S hS)

AlgebraicGeometry.SmallZariski.preservesFiniteColimits_associatedModuleQcohOfComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallZariskiRealClosureProperties.lean, line 212. The attribute's comment: “part (4), small site at τ = Zariski”.

Stacks 06VE (4) for the small site at τ = Zariski. The functor QCoh(𝒪_S) ⥤ Mod(S_Zar, 𝒪), 𝓕 ↦ 𝓕^a of Definition 03DU (4), is right exact, i.e. commutes with finite colimits.

As on the big site this is not read off clause (3) but assembled from the two factors, the inclusion of the quasi-coherent modules being right exact because they are a weak Serre subcategory.

public theorem preservesFiniteColimits_associatedModuleQcohOfComparison :
    PreservesFiniteColimits
      (AlgebraicGeometry.SmallZariski.associatedModuleQcoh B S hS)

AlgebraicGeometry.SmallZariski.essImage_X₂_of_shortExactOfComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallZariskiRealClosureProperties.lean, line 290. The attribute's comment: “part (10), small site at τ = Zariski”.

Stacks 06VE (10) for the small site at τ = Zariski. Given a short exact sequence 0 → 𝓕₁^a → 𝓔 → 𝓕₂^a → 0 of 𝒪-modules on the small Zariski site of S, with 𝓕₁ and 𝓕₂ quasi-coherent on S, the module 𝓔 is itself in the essential image of 𝓕 ↦ 𝓕^a.

Restriction along the morphism of ringed sites of Remark 03FH is an equivalence at τ = Zariski (Stacks 03FG), hence exact, so it carries the sequence to a short exact sequence of 𝒪_S-modules; by AlgebraicGeometry.SmallZariski.essImage_associatedModuleQcohOfComparison_iff its outer terms are quasi-coherent, so its middle term is too, quasi-coherent modules on a scheme being closed under extensions (Schemes, Section 01LA). The same lemma turns that back into membership of the essential image.

The clause at τ = étale and on the big sites is a different statement and is not implied by this one; see the implementation notes of this module.

public theorem essImage_X₂_of_shortExactOfComparison
    {C : ShortComplex (SheafOfModules.{u} (structureSheaf B S hS))} (hC : C.ShortExact)
    (h₁ : (associatedModuleQcoh B S hS).essImage C.X₁)
    (h₃ : (associatedModuleQcoh B S hS).essImage C.X₃) :
    (associatedModuleQcoh B S hS).essImage C.X₂

AlgebraicGeometry.SmallZariski.isQuasicoherentOnSite_X₂_of_shortExactOfComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallZariskiRealClosureProperties.lean, line 331. The attribute's comment: “part (10), small site at τ = Zariski, as quasi-coherence on the site”.

Stacks 06VE (10) for the small site at τ = Zariski, in the form the source states it: given a short exact sequence 0 → 𝓕₁ → 𝓕₂ → 𝓕₃ → 0 of 𝒪-modules on the small Zariski site of S whose outer terms are quasi-coherent, the middle term is quasi-coherent.

The source states clause (10) as "𝓔 is quasi-coherent, i.e. 𝓔 is in the essential image of the functor"; this is the first reading and AlgebraicGeometry.SmallZariski.essImage_X₂_of_shortExactOfComparison is the second. The two agree by Stacks 03DX (2) at τ = Zariski, essImage_associatedModuleQcohOfComparison_iff_isQuasicoherentOnSite. It is also the third case of Stacks 0GNB (4) and 0GNC (4) at this site.

public theorem isQuasicoherentOnSite_X₂_of_shortExactOfComparison
    {C : ShortComplex (SheafOfModules.{u} (structureSheaf B S hS))} (hC : C.ShortExact)
    (h₁ : C.X₁.IsQuasicoherentOnSite) (h₃ : C.X₃.IsQuasicoherentOnSite) :
    C.X₂.IsQuasicoherentOnSite

AlgebraicGeometry.SmallZariski.fullyFaithfulAssociatedModuleQcoh, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallZariskiRealFullyFaithful.lean, line 275. The attribute's comment: “part (1), small site at τ = Zariski”.

Stacks 0GN7 for the small site at τ = Zariski, and clause (1) of Stacks 06VE for it. The functor 𝓕 ↦ 𝓕^a of Definition 03DU (4) at τ = Zariski — the pullback of sheaves of modules along the morphism of ringed sites (S_Zar, 𝒪) → (S_Zar, 𝒪_S) of Remark 03FH, with the coefficient sheaf T/S ↦ Γ(T, 𝒪_T) of Definition 03DU (2) — from the quasi-coherent 𝒪_S-modules to the 𝒪-modules on the small Zariski site, is fully faithful.

Together with AlgebraicGeometry.BigFppfOver.fullyFaithfulBaseAssociatedModuleQcoh (the big site, every τ) and AlgebraicGeometry.SmallEtale.fullyFaithfulAssociatedModuleQcoh' (the small site at τ = étale) this completes the covering set of 0GN7: Definition 03DU gives a small site only for τ ∈ {Zariski, étale}, so those three statements are every functor the lemma quantifies over.

0GN7 spells the target QCoh(S_Zar, 𝒪) where this is Mod(S_Zar, 𝒪), and that is the same statement for the same reason as at τ = étale and on the big site: full faithfulness of a functor into a category is full faithfulness into any full subcategory containing its image, and the image lands in QCoh(S_Zar, 𝒪) by Stacks 03DV (2), AlgebraicGeometry.SmallZariski.isQuasicoherentOnSite_associatedModule_of_isQuasicoherent; the corestriction itself is AlgebraicGeometry.SmallZariski.fullyFaithfulAssociatedModuleQcohOnSite below. 06VE's second functor has target Mod(S_τ, 𝒪), which is the target here with nothing to read through.

public noncomputable def fullyFaithfulAssociatedModuleQcoh :
    (associatedModuleQcoh B S hS).FullyFaithful

AlgebraicGeometry.SmallZariski.preservesColimitsOfShape_discrete_associatedSheafFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallZariskiSectionsClosure.lean, line 236. The attribute's comment: “part (2), small site at τ = Zariski, for the SECTIONS-defined functor 𝓕 ↦ 𝓕ᵃ of Definition 03DU (4) — SmallZariski.associatedSheafFunctor. The same clause for the pullback-defined functor of Remark 03FH is preservesColimitsOfShape_discrete_associatedModuleQcohOfComparison; the two functors are identified by associatedModuleQcohIsoAssociatedSheafFunctor”.

[Stacks, Tag 06VE] (2) for the small site at τ = Zariski, for the functor the source defines. The sections-defined 𝓕 ↦ 𝓕ᵃ of [Stacks, Tag 03DU] (4), as a functor QCoh(𝒪_S) ⥤ Mod(S_Zar, 𝒪), commutes with direct sums.

AlgebraicGeometry.SmallZariski.preservesColimitsOfShape_discrete_associatedModuleQcohOfComparison is the same clause for the pullback-defined functor of [Stacks, Remark 03FH]; this is it read through AlgebraicGeometry.SmallZariski.associatedModuleQcohIsoAssociatedSheafFunctor. 06VE's second functor has target Mod(S_τ, 𝒪), which is the target here on the nose.

public theorem preservesColimitsOfShape_discrete_associatedSheafFunctor (I : Type u) :
    PreservesColimitsOfShape (Discrete I) (associatedSheafFunctor B S hS)

AlgebraicGeometry.SmallZariski.preservesColimitsOfSize_associatedSheafFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallZariskiSectionsClosure.lean, line 251. The attribute's comment: “part (3), small site at τ = Zariski, for the SECTIONS-defined functor 𝓕 ↦ 𝓕ᵃ of Definition 03DU (4) — SmallZariski.associatedSheafFunctor. The same clause for the pullback-defined functor of Remark 03FH is preservesColimitsOfSize_associatedModuleQcohOfComparison; the two functors are identified by associatedModuleQcohIsoAssociatedSheafFunctor”.

[Stacks, Tag 06VE] (3) for the small site at τ = Zariski, for the functor the source defines. The sections-defined 𝓕 ↦ 𝓕ᵃ commutes with all colimits indexed at the size of the scheme.

Scope and route as on AlgebraicGeometry.SmallZariski.preservesColimitsOfShape_discrete_associatedSheafFunctor.

public theorem preservesColimitsOfSize_associatedSheafFunctor :
    PreservesColimitsOfSize.{u, u} (associatedSheafFunctor B S hS)

AlgebraicGeometry.SmallZariski.preservesFiniteColimits_associatedSheafFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallZariskiSectionsClosure.lean, line 270. The attribute's comment: “part (4), small site at τ = Zariski, for the SECTIONS-defined functor 𝓕 ↦ 𝓕ᵃ of Definition 03DU (4) — SmallZariski.associatedSheafFunctor. The same clause for the pullback-defined functor of Remark 03FH is preservesFiniteColimits_associatedModuleQcohOfComparison; the two functors are identified by associatedModuleQcohIsoAssociatedSheafFunctor”.

[Stacks, Tag 06VE] (4) for the small site at τ = Zariski, for the functor the source defines. The sections-defined 𝓕 ↦ 𝓕ᵃ is right exact, i.e. commutes with finite colimits.

Scope and route as on AlgebraicGeometry.SmallZariski.preservesColimitsOfShape_discrete_associatedSheafFunctor; see the implementation notes of this module for why this is not read off clause (3).

public theorem preservesFiniteColimits_associatedSheafFunctor :
    PreservesFiniteColimits (associatedSheafFunctor B S hS)

AlgebraicGeometry.SmallZariski.essImage_X₂_of_shortExact_associatedSheafFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallZariskiSectionsClosure.lean, line 310. The attribute's comment: “part (10), small site at τ = Zariski, for the SECTIONS-defined functor 𝓕 ↦ 𝓕ᵃ of Definition 03DU (4) — SmallZariski.associatedSheafFunctor. The same clause for the pullback-defined functor of Remark 03FH is essImage_X₂_of_shortExactOfComparison; the two functors have the same essential image by essImage_associatedSheafFunctor_iff”.

[Stacks, Tag 06VE] (10) for the small site at τ = Zariski, for the functor the source defines. Given a short exact sequence 0 → 𝓕₁ᵃ → 𝓔 → 𝓕₂ᵃ → 0 of 𝒪-modules on the small Zariski site of S, with 𝓕₁ and 𝓕₂ quasi-coherent on S and 𝓕 ↦ 𝓕ᵃ the sections-defined functor of [Stacks, Tag 03DU] (4), the module 𝓔 is itself in the essential image of that functor.

AlgebraicGeometry.SmallZariski.essImage_X₂_of_shortExactOfComparison is the same clause for the pullback-defined functor of [Stacks, Remark 03FH]; the two functors have the same essential image by AlgebraicGeometry.SmallZariski.essImage_associatedSheafFunctor_iff, and all three hypotheses and the conclusion read across it.

The clause in the form the source states it — "𝓔 is quasi-coherent" — is AlgebraicGeometry.SmallZariski.isQuasicoherentOnSite_X₂_of_shortExactOfComparison, whose statement names no functor and so needs no sections-defined counterpart.

public theorem essImage_X₂_of_shortExact_associatedSheafFunctor
    {C : ShortComplex (SheafOfModules.{u} (structureSheaf B S hS))} (hC : C.ShortExact)
    (h₁ : (associatedSheafFunctor B S hS).essImage C.X₁)
    (h₃ : (associatedSheafFunctor B S hS).essImage C.X₃) :
    (associatedSheafFunctor B S hS).essImage C.X₂

AlgebraicGeometry.SmallZariski.fullyFaithfulAssociatedSheafFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallZariskiSectionsIso.lean, line 572. The attribute's comment: “part (1), small site at τ = Zariski, for the SECTIONS-defined functor 𝓕 ↦ 𝓕ᵃ of Definition 03DU (4) — SmallZariski.associatedSheafFunctor, whose target Mod(S_Zar, 𝒪) is the target 06VE spells for its second functor. The same clause for the pullback-defined functor of Remark 03FH is fullyFaithfulAssociatedModuleQcoh”.

[Stacks, Tag 0GN7] for the small site at τ = Zariski, for the functor the source defines: the assignment 𝓕 ↦ 𝓕ᵃ of [Stacks, Tag 03DU] (4) — the sheaf of 𝒪-modules on S_Zar whose sections over f : T → S are Γ(T, f^*𝓕), AlgebraicGeometry.SmallZariski.associatedSheafFunctor — is fully faithful on the quasi-coherent 𝒪_S-modules.

AlgebraicGeometry.SmallZariski.fullyFaithfulAssociatedModuleQcoh is the same statement for the pullback-defined functor of [Stacks, Remark 03FH]; this is it read through AlgebraicGeometry.SmallZariski.associatedModuleQcohIsoAssociatedSheafFunctor, which identifies the two. Both are 0GN7 at τ = Zariski, and the source's own statement is about the sections description, so the clause is only about the object the source names once this form exists.

0GN7 spells the target QCoh(S_Zar, 𝒪) where this is Mod(S_Zar, 𝒪); that is the same statement for the reason recorded on AlgebraicGeometry.SmallZariski.fullyFaithfulAssociatedModuleQcoh, full faithfulness into a category being full faithfulness into any full subcategory containing the image, and the image landing in QCoh(S_Zar, 𝒪) by [Stacks, Tag 03DV] (2).

This is also clause (1) of [Stacks, Tag 06VE] at τ = Zariski for the sections-defined functor, that clause being the same assertion of full faithfulness; its second functor has target Mod(S_τ, 𝒪), which is the target here with nothing to read through. The two attributes sit together for the same reason they do on AlgebraicGeometry.SmallZariski.fullyFaithfulAssociatedModuleQcoh for the pullback-defined functor.

public noncomputable def fullyFaithfulAssociatedSheafFunctor :
    (associatedSheafFunctor B S hS).FullyFaithful

AlgebraicGeometry.BigFppfOver.preservesColimitsOfShape_discrete_associatedModuleQcoh, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Descent/AssociatedModuleColimits.lean, line 252. The attribute's comment: “direct_sums, big site at τ = fppf only”.

Stacks 06VE (2). The functor 𝓕 ↦ 𝓕^a commutes with direct sums: a direct sum is a colimit over a discrete index category, so this is the discrete case of clause (3).

Stated for the big fppf site, which is what this declaration's functor is. The base's clause string "fppf only" is kept byte-identical (a base registration line is never rewritten); read it as the scope of this declaration, not of the library, since the reason the previous version gave for the restriction — that the clause's inputs were proved at fppf only — was false: AlgebraicGeometry.BigFppfOver.preservesColimitsOfSize_baseAssociatedModule (StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/BaseRingedSite.lean:317) is an instance at every τ : SiteKind. The clause at every τ is AlgebraicGeometry.BigFppfOver.preservesColimitsOfShape_discrete_baseAssociatedModuleQcoh, in StacksFrontier.AlgebraicGeometry.Stacks.Quasicoherent.Descent.BaseAssociatedModuleColimits, of which this is the τ = .fppf case.

The source's second functor, QCoh(𝒪_S) ⥤ Mod(S_τ, 𝒪) into a small site of S, is a different construction, and this clause holds for it too, at τ = étale: AlgebraicGeometry.SmallEtale.preservesColimitsOfShape_discrete_associatedModuleQcoh, over AlgebraicGeometry.SmallEtale.associatedModule (StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtaleRingedSite.lean:417). An earlier note here said "small site untreated"; that was true when written and is now false.

public theorem preservesColimitsOfShape_discrete_associatedModuleQcoh (I : Type u) :
    PreservesColimitsOfShape (Discrete I) (associatedModuleQcoh B S hS)

AlgebraicGeometry.BigFppfOver.preservesColimitsOfSize_associatedModuleQcoh, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Descent/AssociatedModuleColimits.lean, line 269. The attribute's comment: “colimits, big site at τ = fppf only”.

Stacks 06VE (3). The functor 𝓕 ↦ 𝓕^a commutes with all colimits indexed at the size of the site.

Stated for the big fppf site, as on AlgebraicGeometry.BigFppfOver.preservesColimitsOfShape_discrete_associatedModuleQcoh, and for the same reason: that is this declaration's functor. The clause at every τ is AlgebraicGeometry.BigFppfOver.preservesColimitsOfSize_baseAssociatedModuleQcoh, of which this is the τ = .fppf case; the clause's inputs are not specific to fppf.

The small-site functor of the source statement is treated at τ = étale, where this clause is AlgebraicGeometry.SmallEtale.preservesColimitsOfSize_associatedModuleQcoh. The clause string "fppf only" is kept byte-identical and reads as the scope of this declaration.

public theorem preservesColimitsOfSize_associatedModuleQcoh :
    PreservesColimitsOfSize.{u, u} (associatedModuleQcoh B S hS)

AlgebraicGeometry.BigFppfOver.preservesColimitsOfShape_discrete_baseAssociatedModuleQcoh, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Descent/BaseAssociatedModuleColimits.lean, line 125. The attribute's comment: “part (2), big site (Sch/S)_τ, every τ”.

Stacks 06VE (2), for every τ ∈ {Zariski, étale, smooth, syntomic, fppf}. The functor QCoh(𝒪_S) ⥤ Mod((Sch/S)_τ, 𝒪), 𝓕 ↦ 𝓕^a, commutes with direct sums: a direct sum is a colimit over a discrete index category, so this is the discrete case of clause (3).

The earlier AlgebraicGeometry.BigFppfOver.preservesColimitsOfShape_discrete_associatedModuleQcoh carries the clause string "big site at τ = fppf only", on the ground that the clause's inputs were proved at fppf only. They are not: the adjunction, and with it cocontinuity of 𝓕 ↦ 𝓕^a, exists at every τ as AlgebraicGeometry.BigFppfOver.preservesColimitsOfSize_baseAssociatedModule, and the other input is about QCoh(𝒪_S) alone. Hence this statement, which drops the restriction.

public theorem preservesColimitsOfShape_discrete_baseAssociatedModuleQcoh (I : Type u) :
    PreservesColimitsOfShape (Discrete I) (baseAssociatedModuleQcoh B S hS τ)

AlgebraicGeometry.BigFppfOver.preservesColimitsOfSize_baseAssociatedModuleQcoh, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Descent/BaseAssociatedModuleColimits.lean, line 136. The attribute's comment: “part (3), big site (Sch/S)_τ, every τ”.

Stacks 06VE (3), for every τ ∈ {Zariski, étale, smooth, syntomic, fppf}. The functor QCoh(𝒪_S) ⥤ Mod((Sch/S)_τ, 𝒪), 𝓕 ↦ 𝓕^a, commutes with all colimits indexed at the size of the site.

Scope as on AlgebraicGeometry.BigFppfOver.preservesColimitsOfShape_discrete_baseAssociatedModuleQcoh.

public theorem preservesColimitsOfSize_baseAssociatedModuleQcoh :
    PreservesColimitsOfSize.{u, u} (baseAssociatedModuleQcoh B S hS τ)

AlgebraicGeometry.BigFppfOver.preservesFiniteColimits_baseAssociatedModuleQcoh, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Descent/BaseAssociatedModuleColimits.lean, line 150. The attribute's comment: “part (4), big site (Sch/S)_τ, every τ”.

Stacks 06VE (4), for every τ ∈ {Zariski, étale, smooth, syntomic, fppf}. The functor QCoh(𝒪_S) ⥤ Mod((Sch/S)_τ, 𝒪), 𝓕 ↦ 𝓕^a, is right exact, i.e. commutes with finite colimits.

The source deduces this from clause (3); here it is the composite of the two factors' finite colimit preservation, because CategoryTheory.Limits.PreservesFiniteColimits quantifies over finite categories in Type 0 while clause (3) above is stated at the universe of the site, and neither statement contains the other.

public theorem preservesFiniteColimits_baseAssociatedModuleQcoh :
    PreservesFiniteColimits (baseAssociatedModuleQcoh B S hS τ)

AlgebraicGeometry.SmallEtale.preservesColimitsOfShape_discrete_associatedModuleQcoh, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Descent/SmallEtaleAssociatedModuleColimits.lean, line 186. The attribute's comment: “direct_sums, small site at τ = étale”.

Stacks 06VE (2) for the small site at τ = étale. The functor QCoh(𝒪_S) ⥤ Mod(S_étale, 𝒪), 𝓕 ↦ 𝓕^a, commutes with direct sums: a direct sum is a colimit over a discrete index category, so this is the discrete case of clause (3).

The clause string records exactly the scope proved: the second functor of 06VE, on the small site, at τ = étale. The functor is the one of Definition 03DU (4), which is defined for τ ∈ {Zariski, étale}; the Zariski half of this clause is a separate statement about AlgebraicGeometry.SmallZariski.associatedModule, which exists — see the implementation notes above. The big-site half of the same clause is AlgebraicGeometry.BigFppfOver.preservesColimitsOfShape_discrete_associatedModuleQcoh.

public theorem preservesColimitsOfShape_discrete_associatedModuleQcoh (I : Type u) :
    PreservesColimitsOfShape (Discrete I) (associatedModuleQcoh B S hS)

AlgebraicGeometry.SmallEtale.preservesColimitsOfSize_associatedModuleQcoh, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Descent/SmallEtaleAssociatedModuleColimits.lean, line 199. The attribute's comment: “colimits, small site at τ = étale”.

Stacks 06VE (3) for the small site at τ = étale. The functor QCoh(𝒪_S) ⥤ Mod(S_étale, 𝒪), 𝓕 ↦ 𝓕^a, commutes with all colimits indexed at the size of the scheme.

Scope as on AlgebraicGeometry.SmallEtale.preservesColimitsOfShape_discrete_associatedModuleQcoh; the big-site half is AlgebraicGeometry.BigFppfOver.preservesColimitsOfSize_associatedModuleQcoh.

public theorem preservesColimitsOfSize_associatedModuleQcoh :
    PreservesColimitsOfSize.{u, u} (associatedModuleQcoh B S hS)

AlgebraicGeometry.SmallEtale.preservesFiniteColimits_associatedModuleQcoh, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Descent/SmallEtaleAssociatedModuleExact.lean, line 78. The attribute's comment: “part (4), small site at τ = étale”.

Stacks 06VE (4) for the second functor of the lemma. The functor QCoh(𝒪_S) ⥤ Mod(S_étale, 𝒪), 𝓕 ↦ 𝓕^a, is right exact: the inclusion of the quasi-coherent modules is right exact, quasi-coherence on a scheme being a weak Serre class, and 𝓕 ↦ 𝓕^a is right exact because it is a left adjoint.

public theorem preservesFiniteColimits_associatedModuleQcoh :
    PreservesFiniteColimits (AlgebraicGeometry.SmallEtale.associatedModuleQcoh B S hS)

AlgebraicGeometry.SmallEtale.preservesFiniteLimits_associatedModuleQcoh, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Descent/SmallEtaleAssociatedModuleExact.lean, line 95. The attribute's comment: “part (5), left exactness half”.

The half of Stacks 06VE (5) that is special to the small étale site. The functor QCoh(𝒪_S) ⥤ Mod(S_étale, 𝒪), 𝓕 ↦ 𝓕^a, is left exact.

The inclusion of the quasi-coherent modules is left exact because quasi-coherence on a scheme is a weak Serre class, and 𝓕 ↦ 𝓕^a is left exact because ε : (S_étale, 𝒪) ⟶ (S_Zar, 𝒪_S) is flat — an étale morphism is flat, Morphisms, Lemma 02GS, which is Stacks 0GNA for ε and gives the exactness assertion of Stacks 08H8.

public theorem preservesFiniteLimits_associatedModuleQcoh :
    PreservesFiniteLimits (associatedModuleQcoh B S hS)

AlgebraicGeometry.SmallEtale.shortExact_map_associatedModuleQcoh, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Descent/SmallEtaleAssociatedModuleExact.lean, line 106. The attribute's comment: “part (5), as preservation of short exact sequences”.

Stacks 06VE (5). The functor QCoh(𝒪_S) ⥤ Mod(S_étale, 𝒪), 𝓕 ↦ 𝓕^a, is exact: it carries a short exact sequence of quasi-coherent 𝒪_S-modules to a short exact sequence of 𝒪-modules on the small étale site.

public theorem shortExact_map_associatedModuleQcoh
    {T : ShortComplex (SheafOfModules.isQuasicoherent S.ringCatSheaf).FullSubcategory}
    (hT : T.ShortExact) : (T.map (associatedModuleQcoh B S hS)).ShortExact

AlgebraicGeometry.SmallZariski.associatedModuleTensorIsoOfComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Descent/SmallZariskiAssociatedModuleTensor.lean, line 148. The attribute's comment: “part (7), small site at τ = Zariski, for the PULLBACK-defined functor 𝓕 ↦ 𝓕ᵃ of Remark 03FH, for all 𝒪_S-modules; bifunctor form”.

Stacks 06VE (7) at τ = Zariski. The functor 𝓕 ↦ 𝓕^a into the 𝒪-modules of the small Zariski site of S carries the tensor product of two 𝒪_S-modules to the tensor product of their images:

(𝓕 ⊗_{𝒪_S} 𝓖)^a ≅ 𝓕^a ⊗_𝒪 𝓖^a,

naturally in the pair (𝓕, 𝓖).

This is Modules on Sites, Lemma 03EL — Stacks.SheafOfModules.pullbackTensorIso — for the morphism of ringed topoi underlying id_{small, Zar, Zar} of Remark 03FH, conjugated on both sides by AlgebraicGeometry.SmallZariski.pullbackModulesIsoAssociatedModule.

The functor is the pullback description of Stacks 03DU (4); the clause for the sections description, which is the one 03DU (4) gives, is AlgebraicGeometry.SmallZariski.associatedModuleOfSectionsTensorObjIso. With AlgebraicGeometry.SmallEtale.associatedModuleTensorBifunctorIso (small site at τ = étale) and AlgebraicGeometry.BigFppfOver.baseAssociatedModuleTensorIso (big site, every τ) this completes clause (7) at every functor the lemma quantifies over.

public def associatedModuleTensorIsoOfComparison :
    Functor.uncurry.obj (Stacks.SheafOfModules.Tensor.sheafTensor.{u, u, u, u, u} S.sheaf) ⋙
        associatedModule B S hS ≅
      Functor.prod (associatedModule B S hS) (associatedModule B S hS) ⋙
        Functor.uncurry.obj (Stacks.SheafOfModules.Tensor.sheafTensor.{u + 1, u, u, u, u}
          (smallZariskiRingedSite B S hS).O)

AlgebraicGeometry.SmallZariski.associatedModuleTensorObjIsoOfComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Descent/SmallZariskiAssociatedModuleTensor.lean, line 164. The attribute's comment: “part (7), small site at τ = Zariski, for the PULLBACK-defined functor 𝓕 ↦ 𝓕ᵃ of Remark 03FH, for all 𝒪_S-modules; objectwise form”.

Stacks 06VE (7) at τ = Zariski, objectwise — the form in which the source states it: (𝓕 ⊗_{𝒪_S} 𝓖)^a = 𝓕^a ⊗_𝒪 𝓖^a, for the pullback description of 𝓕 ↦ 𝓕^a.

public def associatedModuleTensorObjIsoOfComparison (F G : S.Modules) :
    (associatedModule B S hS).obj
        ((Functor.uncurry.obj
            (Stacks.SheafOfModules.Tensor.sheafTensor.{u, u, u, u, u} S.sheaf)).obj (F, G)) ≅
      (Functor.uncurry.obj (Stacks.SheafOfModules.Tensor.sheafTensor.{u + 1, u, u, u, u}
          (smallZariskiRingedSite B S hS).O)).obj
        ((associatedModule B S hS).obj F, (associatedModule B S hS).obj G)

AlgebraicGeometry.SmallZariski.associatedModuleOfSectionsTensorObjIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Descent/SmallZariskiAssociatedModuleTensor.lean, line 186. The attribute's comment: “part (7), small site at τ = Zariski, for the SECTIONS-defined functor 𝓕 ↦ 𝓕ᵃ of Definition 03DU (4), for quasi-coherent 𝒪_S-modules”.

Stacks 06VE (7) at τ = Zariski, for the sections-defined 𝓕^a of Stacks 03DU (4). For quasi-coherent 𝒪_S-modules 𝓕, 𝓖,

(𝓕 ⊗_{𝒪_S} 𝓖)^a ≅ 𝓕^a ⊗_𝒪 𝓖^a,

where 𝓕^a is the sheaf on S_Zar whose sections over f : T → S are Γ(T, f^*𝓕).

This is AlgebraicGeometry.SmallZariski.associatedModuleTensorObjIsoOfComparison read through Remark 03FH (1), AlgebraicGeometry.SmallZariski.associatedModuleIsoOfSections, at the three modules involved. It is the description Stacks 03DU (4) gives, and so the description every statement of this tag is about.

public def associatedModuleOfSectionsTensorObjIso (F G : S.Modules)
    [F.IsQuasicoherent] [G.IsQuasicoherent] :
    associatedModuleOfSections B S hS
        ((Functor.uncurry.obj
            (Stacks.SheafOfModules.Tensor.sheafTensor.{u, u, u, u, u} S.sheaf)).obj (F, G)) ≅
      (Functor.uncurry.obj (Stacks.SheafOfModules.Tensor.sheafTensor.{u + 1, u, u, u, u}
          (smallZariskiRingedSite B S hS).O)).obj
        (associatedModuleOfSections B S hS F, associatedModuleOfSections B S hS G)

Tag 0GNB, a lemma

Tag 0GNB in the Stacks Project.

AlgebraicGeometry.SmallEtale.isQuasicoherentOnSite_of_isColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtaleQuasicoherentTransfer.lean, line 178. The attribute's comment: “part (2): colimits”.

Stacks 0GNB (2). A colimit of quasi-coherent 𝒪-modules on the small étale site of a scheme is quasi-coherent; the shape is indexed at the size of the scheme, as in Stacks 06VE (3) on the same site.

public theorem isQuasicoherentOnSite_of_isColimit {K : Type u} [SmallCategory K]
    {D : K ⥤ SheafOfModules.{u} (structureSheaf B S hS)}
    (hD : ∀ k, (D.obj k).IsQuasicoherentOnSite) {c : Cocone D} (hc : IsColimit c) :
    c.pt.IsQuasicoherentOnSite

AlgebraicGeometry.SmallEtale.isQuasicoherentOnSite_of_isColimit_cofan, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtaleQuasicoherentTransfer.lean, line 187. The attribute's comment: “part (1): direct sums”.

Stacks 0GNB (1). A direct sum of quasi-coherent 𝒪-modules on the small étale site of a scheme is quasi-coherent.

public theorem isQuasicoherentOnSite_of_isColimit_cofan {I : Type u}
    {F : I → SheafOfModules.{u} (structureSheaf B S hS)}
    (hF : ∀ i, (F i).IsQuasicoherentOnSite)
    {c : Cocone (Discrete.functor F)} (hc : IsColimit c) :
    c.pt.IsQuasicoherentOnSite

AlgebraicGeometry.SmallEtale.isQuasicoherentOnSite_of_isColimit_cokernelCofork, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtaleQuasicoherentTransfer.lean, line 199. The attribute's comment: “part (3): cokernels”.

Stacks 0GNB (3), the cokernel half. A cokernel of a morphism of quasi-coherent 𝒪-modules on the small étale site of a scheme is quasi-coherent.

public theorem isQuasicoherentOnSite_of_isColimit_cokernelCofork
    {M N : SheafOfModules.{u} (structureSheaf B S hS)} (f : M ⟶ N)
    (hM : M.IsQuasicoherentOnSite) (hN : N.IsQuasicoherentOnSite)
    {c : CokernelCofork f} (hc : IsColimit c) : c.pt.IsQuasicoherentOnSite

AlgebraicGeometry.SmallEtale.isQuasicoherentOnSite_of_isLimit_kernelFork, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtaleQuasicoherentTransfer.lean, line 209. The attribute's comment: “part (3): kernels”.

Stacks 0GNB (3), the kernel half. A kernel of a morphism of quasi-coherent 𝒪-modules on the small étale site of a scheme is quasi-coherent.

public theorem isQuasicoherentOnSite_of_isLimit_kernelFork
    {M N : SheafOfModules.{u} (structureSheaf B S hS)} (f : M ⟶ N)
    (hM : M.IsQuasicoherentOnSite) (hN : N.IsQuasicoherentOnSite)
    {c : KernelFork f} (hc : IsLimit c) : c.pt.IsQuasicoherentOnSite

AlgebraicGeometry.SmallEtale.isQuasicoherentOnSite_shortExact_X₁, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtaleQuasicoherentTransfer.lean, line 231. The attribute's comment: “part (4): the case of the sub, from the kernel clause”.

Stacks 0GNB (4), the case in which the quotient and the middle term are quasi-coherent. The kernel term of a short exact sequence of 𝒪-modules on the small étale site of a scheme is quasi-coherent when the other two are.

public theorem isQuasicoherentOnSite_shortExact_X₁
    {T : ShortComplex (SheafOfModules.{u} (structureSheaf B S hS))} (hT : T.ShortExact)
    (h₂ : T.X₂.IsQuasicoherentOnSite) (h₃ : T.X₃.IsQuasicoherentOnSite) :
    T.X₁.IsQuasicoherentOnSite

AlgebraicGeometry.SmallEtale.isQuasicoherentOnSite_shortExact_X₃, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtaleQuasicoherentTransfer.lean, line 241. The attribute's comment: “part (4): the case of the quotient, from the cokernel clause”.

Stacks 0GNB (4), the case in which the sub and the middle term are quasi-coherent. The quotient term of a short exact sequence of 𝒪-modules on the small étale site of a scheme is quasi-coherent when the other two are.

public theorem isQuasicoherentOnSite_shortExact_X₃
    {T : ShortComplex (SheafOfModules.{u} (structureSheaf B S hS))} (hT : T.ShortExact)
    (h₁ : T.X₁.IsQuasicoherentOnSite) (h₂ : T.X₂.IsQuasicoherentOnSite) :
    T.X₃.IsQuasicoherentOnSite

AlgebraicGeometry.SmallEtale.isQuasicoherentOnSite_shortExact_X₂, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtaleRestrictionRightExact.lean, line 291. The attribute's comment: “clause (4), third case: the middle term of a short exact sequence”.

The third case of Stacks 0GNB (4): the middle term of a short exact sequence of 𝒪-modules on the small étale site of a scheme is quasi-coherent when the outer two are.

The source derives this case not from clause (3) but from Stacks 06VE (10), and on this site the two are the same statement, by AlgebraicGeometry.SmallEtale.isQuasicoherentOnSite_iff_essImage_associatedModuleQcoh.

public theorem isQuasicoherentOnSite_shortExact_X₂ (hC : C.ShortExact)
    (h₁ : C.X₁.IsQuasicoherentOnSite) (h₃ : C.X₃.IsQuasicoherentOnSite) :
    SheafOfModules.IsQuasicoherentOnSite
      (R := AlgebraicGeometry.SmallEtale.structureSheaf B S hS) C.X₂

AlgebraicGeometry.SmallEtale.isQuasicoherentOnSite_internalHomSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SmallEtaleInternalHomFinitePresentation.lean, line 321. The attribute's comment: “clause (6): the internal Hom out of a module of finite presentation is quasi-coherent, small site at τ = étale”.

Clause (6) of Stacks 0GNB. The internal Hom 𝓗om_𝒪(𝓕, 𝓖) of two 𝒪-modules on the small étale site of a scheme S is quasi-coherent when 𝓕 is of finite presentation — Stacks 03DL (7) — and 𝓖 is quasi-coherent.

Quasi-coherence is local on the site (Stacks 03DN), so it is enough to produce a covering family of the final object on whose members the restriction of the internal Hom is quasi-coherent, and the objects carrying a finite global presentation of 𝓕 form one, by the finite-presentation hypothesis itself. On such an object the conclusion is isQuasicoherentOnSite_internalHomSheaf_of_hasFiniteGlobalPresentation of this namespace.

theorem isQuasicoherentOnSite_internalHomSheaf (hF : F.IsFinitePresentationOnSite)
    (hG : G.IsQuasicoherentOnSite) :
    (internalHomSheaf B S hS F G).IsQuasicoherentOnSite

AlgebraicGeometry.SmallEtale.tensorSheaf_isQuasicoherentOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/SmallEtaleQuasicoherentTensor.lean, line 72. The attribute's comment: “tensor_products”.

The tensor product clause of Stacks 0GNB. The tensor product of two quasi-coherent 𝒪-modules on the small étale site of a scheme is quasi-coherent.

public theorem tensorSheaf_isQuasicoherentOnSite
    (F G : SheafOfModules.{u} (structureSheaf B S hS))
    [F.IsQuasicoherentOnSite] [G.IsQuasicoherentOnSite] :
    SheafOfModules.IsQuasicoherentOnSite
      ((Functor.uncurry.obj (Stacks.SheafOfModules.Tensor.sheafTensor.{u + 1, u, u, u, u}
        (commRingStructureSheaf B S hS))).obj (F, G))

Declarations registered for the tag:

AlgebraicGeometry.tensorSheaf_isQuasicoherent, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/SmallEtaleTensorProduct.lean, line 66 (StacksFrontier): “tensor_products”.

Tag 0GNC, a lemma

Tag 0GNC in the Stacks Project.

AlgebraicGeometry.BigFppfOver.isQuasicoherentOnSite_shortExact_X₂_all, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/BaseRestrictionRightExactAll.lean, line 355. The attribute's comment: “part (4), big site at every τ ∈ {Zariski, étale, smooth, syntomic, fppf}, unconditionally”.

Clause (4) of Stacks 0GNC on the big τ-site of a scheme, at every τ ∈ {Zariski, étale, smooth, syntomic, fppf}. Given a short exact sequence 0 → 𝓕₁ → 𝓕₂ → 𝓕₃ → 0 of 𝒪-modules on (Sch/S)_τ with 𝓕₁ and 𝓕₃ quasi-coherent, the middle term 𝓕₂ is quasi-coherent.

The source's three steps are StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/BaseExtensionClosure.lean. Of the two hypotheses they carried, essential surjectivity of 𝓕 ↦ 𝓕^a is Descent, Proposition 03DX (1) and is AlgebraicGeometry.BigFppfOver.baseQuasicoherentIsEssImageAssociatedModule, and right exactness of restriction to S_Zar is AlgebraicGeometry.BigFppfOver.epi_baseRestrictModule_map_all above.

public theorem isQuasicoherentOnSite_shortExact_X₂_all (hC : C.ShortExact)
    (h₁ : C.X₁.IsQuasicoherentOnSite) (h₃ : C.X₃.IsQuasicoherentOnSite) :
    SheafOfModules.IsQuasicoherentOnSite
      (R := AlgebraicGeometry.FibredSite.baseRingStructureSheaf B S hS τ) C.X₂

AlgebraicGeometry.BigFppfOver.isClosedUnderExtensions_baseIsQuasicoherentOnSite_all, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/BaseRestrictionRightExactAll.lean, line 370. The attribute's comment: “part (4), big site at every τ, as a closure-under-extensions instance”.

Quasi-coherence of 𝒪-modules on the big τ-site of a scheme is closed under extensions, at every τ. This is clause (4) of Stacks 0GNC in the shape CategoryTheory.ObjectProperty.IsClosedUnderExtensions records; it has no hypothesis, so it is safe as an instance.

public instance isClosedUnderExtensions_baseIsQuasicoherentOnSite_all (τ : SiteKind) :
    (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
      (FibredSite.baseRingStructureSheaf B S hS τ)).IsClosedUnderExtensions

AlgebraicGeometry.BigFppfOver.isQuasicoherentOnSite_tensorSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentTopologiesTwo/BigSiteProperties.lean, line 133. The attribute's comment: “part (5)”.

Stacks 0GNC, part (5). The tensor product of two quasi-coherent 𝒪-modules on the big τ-site of a scheme S is quasi-coherent, for each of the five topologies.

The tensor product is the one of Stacks 0GMW, the sheafification of the objectwise tensor product of the underlying presheaves of modules. The statement is the quasi-coherent clause of Stacks 03L6 on a ringed site, Stacks.SheafOfModules.TensorLocalProperties.tensorSheaf_isQuasicoherentOnSite, read at this site: the two factors are globally presented on the members of two covering families, the objects admitting an arrow into a member of each again cover, and over such an object the tensor product of two globally presented modules is globally presented.

theorem isQuasicoherentOnSite_tensorSheaf (τ : SiteKind)
    (F G : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf (baseRingedSite B S hS τ).O))
    [SheafOfModules.IsQuasicoherentOnSite F] [SheafOfModules.IsQuasicoherentOnSite G] :
    SheafOfModules.IsQuasicoherentOnSite
      ((Functor.uncurry.obj (Stacks.SheafOfModules.Tensor.sheafTensor.{u + 1, u, u, u, u}
        (FibredSite.baseStructureSheaf B S hS τ))).obj (F, G))

AlgebraicGeometry.BigFppfOver.isQuasicoherentOnSite_internalHomSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentTopologiesTwo/BigSiteProperties.lean, line 156. The attribute's comment: “part (6)”.

Stacks 0GNC, part (6). The internal hom 𝓗om_𝒪(𝓕, 𝓖) of Stacks 03EM is quasi-coherent on the big τ-site of a scheme S, for each of the five topologies, when 𝓕 and 𝓖 are quasi-coherent and 𝓕 is finite locally free.

This is AlgebraicGeometry.RingedSite.internalHomSheaf_isQuasicoherent, the statement for an arbitrary ringed site, with its two sheafification hypotheses on the slice sites discharged: every slice of the big category of schemes over S is essentially small, so abelian presheaves on it have a sheafification whose weak equivalences are the locally bijective maps.

theorem isQuasicoherentOnSite_internalHomSheaf (τ : SiteKind)
    (F G : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf (baseRingedSite B S hS τ).O))
    [SheafOfModules.IsQuasicoherentOnSite F] [SheafOfModules.IsQuasicoherentOnSite G]
    [SheafOfModules.IsFiniteLocallyFree.{u, u, u + 1} F] :
    (RingedSite.internalHomSheaf (baseRingedSite B S hS τ) F G).IsQuasicoherentOnSite

AlgebraicGeometry.RingedSite.internalHomSheaf_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentTopologiesTwo/InternalHom.lean, line 432. The attribute's comment: “internal_hom”.

Internal Hom from a finite locally free quasi-coherent sheaf is quasi-coherent.

theorem internalHomSheaf_isQuasicoherent
    (X : RingedSite.{u, v, w})
    (F G : _root_.SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
    [∀ U : X.C, HasWeakSheafify (X.J.over U) AddCommGrpCat.{w}]
    [∀ U : X.C, (X.J.over U).WEqualsLocallyBijective AddCommGrpCat.{w}]
    [F.IsQuasicoherentOnSite] [G.IsQuasicoherentOnSite]
    [SheafOfModules.IsFiniteLocallyFree.{w, v, u} F] :
    (internalHomSheaf X F G).IsQuasicoherentOnSite

AlgebraicGeometry.BigFppfOver.isClosedUnderColimitsOfShape_baseIsQuasicoherentOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Descent/QuasicoherentColimitsBigSites.lean, line 121. The attribute's comment: “part (2), big site at every τ ∈ {Zariski, étale, smooth, syntomic, fppf}, unconditionally, for an index category K at an arbitrary universe”.

Stacks 0GNC (2) on the big τ-site of S, at every τ and with no hypothesis: quasi-coherence of 𝒪-modules on (Sch/S)_τ is closed under colimits of shape K, for K at an arbitrary universe.

This is the transfer the source performs with Lemma 06VE, carried out at every τ: the quasi-coherent modules of (Sch/S)_τ are the essential image of 𝓕 ↦ 𝓕^a, which is fully faithful (Stacks 0GN7) and preserves colimits (Stacks 06VE (3)) out of QCoh(𝒪_S), where the colimits exist and are quasi-coherent; so they are closed under those colimits. That the essential image is all the quasi-coherent modules is the essential-surjectivity half of Descent, Proposition 03DX (1) at (Sch/S)_τ, and is AlgebraicGeometry.BigFppfOver.baseQuasicoherentIsEssImageAssociatedModule.

public theorem isClosedUnderColimitsOfShape_baseIsQuasicoherentOnSite (τ : SiteKind)
    (K : Type uK) [Category.{uK} K]
    [∀ R : CommRingCat.{u}, HasColimitsOfShape K (ModuleCat.{u} R)]
    [HasColimitsOfShape K (SheafOfModules.{u} S.ringCatSheaf)] :
    (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
      (FibredSite.baseRingStructureSheaf B S hS τ)).IsClosedUnderColimitsOfShape K

AlgebraicGeometry.BigFppfOver.isClosedUnderColimitsOfShape_discrete_baseIsQuasicoherentOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Descent/QuasicoherentColimitsBigSites.lean, line 142. The attribute's comment: “part (1), big site at every τ ∈ {Zariski, étale, smooth, syntomic, fppf}, unconditionally”.

Stacks 0GNC (1) on the big τ-site of S, at every τ and with no hypothesis: a direct sum of quasi-coherent 𝒪-modules on (Sch/S)_τ is quasi-coherent. A direct sum is a colimit over a discrete index category, which is how the source argues it.

public theorem isClosedUnderColimitsOfShape_discrete_baseIsQuasicoherentOnSite (τ : SiteKind)
    (I : Type u) :
    (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
      (FibredSite.baseRingStructureSheaf B S hS τ)).IsClosedUnderColimitsOfShape
      (Discrete I)

AlgebraicGeometry.BigFppfOver.isClosedUnderColimitsOfShape_walkingParallelPair_baseIsQuasicoherentOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Descent/QuasicoherentColimitsBigSites.lean, line 155. The attribute's comment: “part (3), big site at every τ ∈ {Zariski, étale, smooth, syntomic, fppf}, unconditionally”.

Stacks 0GNC (3) on the big τ-site of S, at every τ and with no hypothesis: the cokernel of a morphism of quasi-coherent 𝒪-modules on (Sch/S)_τ is quasi-coherent. A cokernel is a colimit over CategoryTheory.Limits.WalkingParallelPair, and the source obtains clause (3) from clause (2) in exactly this way.

public theorem isClosedUnderColimitsOfShape_walkingParallelPair_baseIsQuasicoherentOnSite
    (τ : SiteKind) :
    (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
      (FibredSite.baseRingStructureSheaf B S hS τ)).IsClosedUnderColimitsOfShape
      WalkingParallelPair

AlgebraicGeometry.BigFppfOver.isClosedUnderColimitsOfShape_isQuasicoherentOnSite_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Descent/QuasicoherentColimitsFppfSite.lean, line 87. The attribute's comment: “part (2), big site at τ = fppf”.

Stacks 0GNC (2) for τ = fppf: a colimit of quasi-coherent 𝒪-modules on the big fppf site of a scheme S is quasi-coherent.

AlgebraicGeometry.BigFppfOver.isClosedUnderColimitsOfShape_baseIsQuasicoherentOnSite, the τ-indexed form of the clause, at τ = .fppf; the statement here is the one about the fppf structure sheaf itself, and the two agree because FibredSite.baseRingStructureSheaf B S hS .fppf = structureSheaf B S hS holds by rfl. This is the transfer the source performs with Lemma 06VE: the colimit is formed in QCoh(𝒪_S), where it exists and is quasi-coherent, and carried up by 𝓕 ↦ 𝓕^a, which preserves colimits and whose essential image is exactly the quasi-coherent modules of the site.

public theorem isClosedUnderColimitsOfShape_isQuasicoherentOnSite_unconditional
    (K : Type u) [Category.{u} K] :
    (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
      (structureSheaf B S hS)).IsClosedUnderColimitsOfShape K

AlgebraicGeometry.BigFppfOver.isClosedUnderColimitsOfShape_discrete_isQuasicoherentOnSite_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Descent/QuasicoherentColimitsFppfSite.lean, line 97. The attribute's comment: “part (1), big site at τ = fppf”.

Stacks 0GNC (1) for τ = fppf: a direct sum of quasi-coherent 𝒪-modules on the big fppf site of a scheme S is quasi-coherent. A direct sum is a colimit over a discrete index category, which is how the source argues it.

public theorem isClosedUnderColimitsOfShape_discrete_isQuasicoherentOnSite_unconditional
    (I : Type u) :
    (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
      (structureSheaf B S hS)).IsClosedUnderColimitsOfShape (Discrete I)

AlgebraicGeometry.BigFppfOver.isClosedUnderColimitsOfShape_walkingParallelPair_isQuasicoherentOnSite_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Descent/QuasicoherentColimitsFppfSite.lean, line 108. The attribute's comment: “part (3), big site at τ = fppf”.

Stacks 0GNC (3) for τ = fppf: the cokernel of a morphism of quasi-coherent 𝒪-modules on the big fppf site of a scheme S is quasi-coherent. A cokernel is a colimit over CategoryTheory.Limits.WalkingParallelPair, and the source obtains clause (3) from clause (2) in exactly this way.

public theorem
    isClosedUnderColimitsOfShape_walkingParallelPair_isQuasicoherentOnSite_unconditional :
    (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
      (structureSheaf B S hS)).IsClosedUnderColimitsOfShape WalkingParallelPair

AlgebraicGeometry.RingedSite.internalHomSheaf_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/QuasicoherentInternalHom.lean, line 321. The attribute's comment: “internal_hom”. References: EGA I (9.1.1), “special case”; SGA 3 III (0.6), “special case”.

On a ringed site whose slices admit sheafification of abelian sheaves, the internal Hom of Stacks 03EM from a finite locally free quasi-coherent module to a quasi-coherent module is quasi-coherent.

public theorem internalHomSheaf_isQuasicoherent
    [∀ U : X.C, HasWeakSheafify (X.J.over U) AddCommGrpCat.{w}]
    [∀ U : X.C, (X.J.over U).WEqualsLocallyBijective AddCommGrpCat.{w}]
    [F.IsQuasicoherentOnSite] [G.IsQuasicoherentOnSite]
    [SheafOfModules.IsFiniteLocallyFree.{w, v, u} F] :
    (X.internalHomSheaf F G).IsQuasicoherentOnSite

Tag 0GNE, a lemma

Tag 0GNE in the Stacks Project.

AlgebraicGeometry.BigFppfOver.hasColimitsOfSize_quasicoherentOnSite_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentTopologiesTwo/BigSiteColimitAgreement.lean, line 125. The attribute's comment: “part (1), existence: QCoh((Sch/S)_fppf, O) has colimits indexed at the size of the site”.

Stacks 0GNE (1), the existence half, with no hypothesis: the category of quasi-coherent 𝒪-modules on the big fppf site of S has all colimits indexed at the size of the site.

AlgebraicGeometry.BigFppfOver.hasColimitsOfSize_quasicoherentOnSite' with its essential-surjectivity hypothesis discharged by AlgebraicGeometry.BigFppfOver.quasicoherentIsEssImageAssociatedModule'.

public theorem hasColimitsOfSize_quasicoherentOnSite_fppf :
    HasColimitsOfSize.{u, u}
      (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
        (structureSheaf B S hS)).FullSubcategory

AlgebraicGeometry.BigFppfOver.preservesColimitsOfSize_quasicoherentOnSite_ι_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentTopologiesTwo/BigSiteColimitAgreement.lean, line 140. The attribute's comment: “part (1), agreement: the colimits of QCoh((Sch/S)_fppf, O) are the colimits taken in Mod((Sch/S)_fppf, O)”.

Stacks 0GNE (1), the agreement with Mod((Sch/S)_fppf, 𝒪), with no hypothesis: a colimit of quasi-coherent 𝒪-modules on (Sch/S)_fppf is the colimit of the same diagram taken in all 𝒪-modules on (Sch/S)_fppf.

AlgebraicGeometry.BigFppfOver.preservesColimitsOfSize_quasicoherentOnSite_ι' with its essential-surjectivity hypothesis discharged.

public theorem preservesColimitsOfSize_quasicoherentOnSite_ι_fppf :
    PreservesColimitsOfSize.{u, u}
      (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
        (structureSheaf B S hS)).ι

AlgebraicGeometry.BigFppfOver.preservesColimitsOfSize_quasicoherentOnSite_ι_comp_restrictTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentTopologiesTwo/BigSiteColimitAgreement.lean, line 194. The attribute's comment: “part (1), agreement: the colimits of QCoh((Sch/S)_fppf, O) are the colimits taken in Mod((Sch/S)_tau, O), for every one of the five topologies and for an arbitrary diagram”.

Stacks 0GNE (1), the agreement with Mod((Sch/S)_τ, 𝒪), over every shape indexed at the size of the site: the colimits of QCoh((Sch/S)_fppf, 𝒪) are the colimits taken in Mod((Sch/S)_τ, 𝒪), at every one of the five topologies and for an arbitrary diagram.

Together with AlgebraicGeometry.BigFppfOver.hasColimitsOfSize_quasicoherentOnSite_fppf and …preservesColimitsOfSize_quasicoherentOnSite_ι_fppf this is the source's clause (1): the colimits exist and agree with those computed in Mod((Sch/S)_Zar, 𝒪), Mod((Sch/S)_étale, 𝒪) and Mod((Sch/S)_fppf, 𝒪).

public theorem preservesColimitsOfSize_quasicoherentOnSite_ι_comp_restrictTopology :
    PreservesColimitsOfSize.{u, u}
      ((SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u} (structureSheaf B S hS)).ι ⋙
        restrictTopology B S hS τ)

AlgebraicGeometry.BigFppfOver.isFiniteLocallyFreeOnSite_restrictTopology_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentTopologiesTwo/BigSiteFiniteLocallyFreeAgreement.lean, line 414. The attribute's comment: “part (3), the parenthetical: finite local freeness agrees at τ = fppf, étale and Zariski”.

Descent, Lemma 0GNE (3), the parenthetical. A quasi-coherent 𝒪-module 𝓕 on the big fppf site of S is finite locally free there if and only if its reading as an 𝒪-module on (Sch/S)_τ is finite locally free, for every one of the five topologies — in particular for the étale and the Zariski topology, which are the two the source names alongside fppf.

The source's proof is run unchanged: 𝓕 = 𝓗ᵃ by the essential surjectivity half of Descent, Proposition 03DX (1) at τ = fppf (AlgebraicGeometry.BigFppfOver.essImage_associatedModuleQcoh_of_isQuasicoherentOnSite), and both sides are then compared with "𝓗 is finite locally free on S" by AlgebraicGeometry.BigFppfOver.isFiniteLocallyFreeOnSite_baseAssociatedModule_iff, the reading on (Sch/S)_τ of 𝓗ᵃ being 𝓗ᵃ computed on (Sch/S)_τ by AlgebraicGeometry.BigFppfOver.restrictTopologyAssociatedModuleIso.

The if half needs no quasi-coherence and no reduction at all: it is Stacks.SheafOfModules.isFiniteLocallyFreeOnSite_of_comparisonPushforward, valid for an arbitrary module and an arbitrary pair of topologies. Quasi-coherence is used only for the only if half, and it is the hypothesis the source's clause carries.

public theorem isFiniteLocallyFreeOnSite_restrictTopology_iff (τ : SiteKind)
    (𝓕 : SheafOfModules.{u} (structureSheaf B S hS))
    (h𝓕 : SheafOfModules.IsQuasicoherentOnSite.{u + 1, u, u, u} 𝓕) :
    SheafOfModules.IsFiniteLocallyFreeOnSite 𝓕 ↔
      SheafOfModules.IsFiniteLocallyFreeOnSite ((restrictTopology B S hS τ).obj 𝓕)

AlgebraicGeometry.BigFppfOver.restrictTopology_internalHomSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentTopologiesTwo/BigSiteInternalHomQuasicoherence.lean, line 94. The attribute's comment: “part (3), the internal homs computed on (Sch/S)_fppf and on (Sch/S)_tau agree, for arbitrary O-modules, at every one of the five topologies”.

Stacks 0GNE (3), the agreement, at the big sites of a scheme. For arbitrary 𝒪-modules 𝓕, 𝓖 on (Sch/S)_fppf, the internal hom 𝓗om_𝒪(𝓕, 𝓖) computed in Mod((Sch/S)_fppf, 𝒪) and read for the coarser topology is the internal hom of the readings computed in Mod((Sch/S)_τ, 𝒪), at every one of the five topologies — so in particular the Zariski, étale and fppf values of the source's statement agree.

This is AlgebraicGeometry.RingedSite.coarsenModules_internalHomSheaf, the statement for an arbitrary ringed site read with a coarser topology, at (Sch/S)_fppf and AlgebraicGeometry.BigFppfOver.baseOverTopology_le_fppf: the ringed site (Sch/S)_fppf read with the τ-topology is (Sch/S)_τ, the structure sheaves having the same underlying presheaf and a sheaf condition that is a proposition.

An equality of sheaves of modules, not an isomorphism: the internal hom of Stacks 03EM is a construction on presheaves of modules and the topology enters only in the proof that the result is a sheaf, so there is nothing to compare. No quasi-coherence and no finite local freeness are needed for the agreement; they are the hypotheses of the quasi-coherence clause below.

public theorem restrictTopology_internalHomSheaf (τ : SiteKind)
    (F G : SheafOfModules.{u} (structureSheaf B S hS)) :
    (restrictTopology B S hS τ).obj
        (RingedSite.internalHomSheaf (baseRingedSite B S hS .fppf) F G) =
      RingedSite.internalHomSheaf (baseRingedSite B S hS τ)
        ((restrictTopology B S hS τ).obj F) ((restrictTopology B S hS τ).obj G)

AlgebraicGeometry.BigFppfOver.isQuasicoherentOnSite_internalHomSheaf_of_isFiniteLocallyFreeOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentTopologiesTwo/BigSiteInternalHomQuasicoherence.lean, line 121. The attribute's comment: “part (3), quasi-coherence of the common value, on the big tau-site for every one of the five topologies, with finite local freeness in the sense of Modules on Sites 03DL (2)”.

Stacks 0GNE (3), the quasi-coherence of the common value, on the big τ-site of S for every τ ∈ {Zariski, étale, smooth, syntomic, fppf}, with finite local freeness in the sense of Modules on Sites, Definition 03DL (2) — the sense in which the source's part (3) states it.

At τ = fppf this is the source's "the common value is an object of QCoh((Sch/S)_fppf, 𝒪)"; the agreement of the values computed at the five topologies, which is what makes "the common value" a legitimate phrase, is AlgebraicGeometry.BigFppfOver.restrictTopology_internalHomSheaf above, an equality of sheaves of modules and not merely an isomorphism.

This is AlgebraicGeometry.BigFppfOver.isQuasicoherentOnSite_internalHomSheaf — Stacks 0GNC on the big τ-site — with its finite-local-freeness hypothesis supplied from the 03DL (2) form by AlgebraicGeometry.SheafOfModules.isFiniteLocallyFree_of_isFiniteLocallyFreeOnSite, whose two sheafification hypotheses on the slices of the big site are the instances AlgebraicGeometry.BigFppfOver.hasSheafify_baseOver and …wEqualsLocallyBijective_baseOver.

public theorem isQuasicoherentOnSite_internalHomSheaf_of_isFiniteLocallyFreeOnSite
    (τ : SiteKind)
      (F G : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf
        (baseRingedSite B S hS τ).O))
    [SheafOfModules.IsQuasicoherentOnSite F] [SheafOfModules.IsQuasicoherentOnSite G]
    (hF : SheafOfModules.IsFiniteLocallyFreeOnSite F) :
    (RingedSite.internalHomSheaf (baseRingedSite B S hS τ) F G).IsQuasicoherentOnSite

AlgebraicGeometry.BigFppfOver.tensorAgreementQuasicoherentOnSite, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentTopologiesTwo/BigSiteTensorAgreement.lean, line 288. The attribute's comment: “part (2), the tensor products computed on (Sch/S)_fppf and on (Sch/S)_tau agree, for an arbitrary pair of quasi-coherent O-modules on (Sch/S)_fppf, at every one of the five topologies”.

Stacks 0GNE (2), the agreement, at the source's own scope. For an arbitrary pair 𝓕, 𝓖 of quasi-coherent 𝒪-modules on (Sch/S)_fppf, the tensor product 𝓕 ⊗_𝒪 𝓖 computed in Mod((Sch/S)_fppf, 𝒪), read for the coarser topology, is the tensor product computed in Mod((Sch/S)_τ, 𝒪) — at every one of the five topologies, so in particular the Zariski, étale and fppf values of the source's statement agree.

AlgebraicGeometry.BigFppfOver.tensorAgreementAssociatedModule is this for 𝓕 = 𝓗^a and 𝓖 = 𝓘^a; the reduction of an arbitrary pair to that case is Stacks 03DX (1) at τ = fppf together with the functoriality of the tensor product in both arguments — see the implementation notes. The comparison itself is the same one, the inverse of the unit of "sheafify for fppf" ⊣ "read an fppf sheaf for τ", so this is not a transported isomorphism but the canonical one with its invertibility now known at every quasi-coherent pair.

def tensorAgreementQuasicoherentOnSite
    (hF : F.IsQuasicoherentOnSite) (hG : G.IsQuasicoherentOnSite) :
    (restrictTopology B S hS τ).obj
        ((Functor.uncurry.obj (Stacks.SheafOfModules.Tensor.sheafTensor
            (FibredSite.baseStructureSheaf B S hS .fppf))).obj (F, G)) ≅
      (Functor.uncurry.obj
          (Stacks.SheafOfModules.Tensor.sheafTensor (FibredSite.baseStructureSheaf B S hS τ))).obj
        ((restrictTopology B S hS τ).obj F, (restrictTopology B S hS τ).obj G)

AlgebraicGeometry.BigFppfOver.isQuasicoherentOnSite_tensorRestrictTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentTopologiesTwo/BigSiteTensorAgreement.lean, line 311. The attribute's comment: “part (2), quasi-coherence of the common value, for an arbitrary pair of quasi-coherent O-modules on (Sch/S)_fppf, at every one of the five topologies”.

Stacks 0GNE (2), the quasi-coherence of the common value, at the source's own scope. For an arbitrary pair of quasi-coherent 𝒪-modules on (Sch/S)_fppf, the common value of the tensor products — the right-hand side of AlgebraicGeometry.BigFppfOver.tensorAgreementQuasicoherentOnSite — is quasi-coherent on (Sch/S)_τ, at every one of the five topologies; at τ = fppf this is the source's "the common value is an object of QCoh((Sch/S)_fppf, 𝒪)".

By the reduction it is the reading of (𝓗 ⊗_{𝒪_S} 𝓘)^a, which is quasi-coherent by Stacks 01CE (3) and Stacks 03DV at every τ.

theorem isQuasicoherentOnSite_tensorRestrictTopology
    (hF : F.IsQuasicoherentOnSite) (hG : G.IsQuasicoherentOnSite) :
    ((Functor.uncurry.obj
        (Stacks.SheafOfModules.Tensor.sheafTensor (FibredSite.baseStructureSheaf B S hS τ))).obj
      ((restrictTopology B S hS τ).obj F,
        (restrictTopology B S hS τ).obj G)).IsQuasicoherentOnSite

Stacks.SheafOfModules.tensorLeftFactorization, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentTopologiesTwo/TopologyIndependence.lean, line 424. The attribute's comment: “part (2), the tensor product for the finer topology is the sheafification of the one for the coarser topology, for an arbitrary pair of topologies on one category”.

Stacks 0GNE (2), the comparison. The tensor product of two sheaves of modules for the finer topology is the sheafification, for the finer topology, of their tensor product taken for the coarser one. Both are sheafifications of the objectwise tensor product of the two underlying presheaves of modules, which does not mention a topology, so this is one component of Stacks.SheafOfModules.sheafificationFactorization.

noncomputable def tensorLeftFactorization :
    ((Stacks.SheafOfModules.Tensor.sheafTensor (J := J) (R)).obj F).obj G ≅
      (comparisonPullback.{u, v, w, m} h ((Stacks.SheafOfModules.Tensor.ringSheaf (J := J)) R)).obj
        (((Stacks.SheafOfModules.Tensor.sheafTensor (J := K) ((commRingOfLe h R))).obj
            ((comparisonPushforward.{u, v, w, m} h ((Stacks.SheafOfModules.Tensor.ringSheaf (J := J)) R)).obj F)).obj
          ((comparisonPushforward.{u, v, w, m} h ((Stacks.SheafOfModules.Tensor.ringSheaf (J := J)) R)).obj G))

Stacks.SheafOfModules.tensorLeftAgreement, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentTopologiesTwo/TopologyIndependence.lean, line 450. The attribute's comment: “part (2), the two tensor products agree once the coarser one is a sheaf for the finer topology”.

Towards Stacks 0GNE (2), the agreement. The tensor product computed for the finer topology, read for the coarser one, is the tensor product computed for the coarser topology, as soon as the latter is already a sheaf for the finer topology — which is what invertibility of the unit at it says.

hunit is a hypothesis the source does not have, and the clause string of the stacks attribute below says so: what is proved here is the implication. It is discharged at the big sites of a scheme, by Stacks 06VE (7), in AlgebraicGeometry.BigFppfOver.isIso_comparisonUnit_tensorRestrictTopology (StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentTopologiesTwo/BigSiteTensorAgreement.lean), and the 0GNE (2) attribute for the clause without that hypothesis sits there, on …tensorAgreementQuasicoherentOnSite, which is this declaration with hunit supplied for an arbitrary pair of quasi-coherent modules on (Sch/S)_fppf — note that the arbitrary pair is reached by widening hunit, so the isomorphism it returns is still this canonical one. The half of part (2) that needs no hypothesis at all is Stacks.SheafOfModules.tensorLeftFactorization, which carries the tag here.

noncomputable def tensorLeftAgreement
    (hunit : IsIso ((comparisonAdjunction.{u, v, w, m} h
        ((Stacks.SheafOfModules.Tensor.ringSheaf (J := J)) R)).unit.app
      (((Stacks.SheafOfModules.Tensor.sheafTensor (J := K) ((commRingOfLe h R))).obj
          ((comparisonPushforward.{u, v, w, m} h ((Stacks.SheafOfModules.Tensor.ringSheaf (J := J)) R)).obj F)).obj
        ((comparisonPushforward.{u, v, w, m} h ((Stacks.SheafOfModules.Tensor.ringSheaf (J := J)) R)).obj G)))) :
    (comparisonPushforward.{u, v, w, m} h ((Stacks.SheafOfModules.Tensor.ringSheaf (J := J)) R)).obj
        (((Stacks.SheafOfModules.Tensor.sheafTensor (J := J) (R)).obj F).obj G) ≅
      ((Stacks.SheafOfModules.Tensor.sheafTensor (J := K) ((commRingOfLe h R))).obj
          ((comparisonPushforward.{u, v, w, m} h ((Stacks.SheafOfModules.Tensor.ringSheaf (J := J)) R)).obj F)).obj
        ((comparisonPushforward.{u, v, w, m} h ((Stacks.SheafOfModules.Tensor.ringSheaf (J := J)) R)).obj G)

AlgebraicGeometry.RingedSite.coarsenModules_internalHomSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentTopologiesTwo/TopologyIndependence.lean, line 498. The attribute's comment: “part (3), the internal homs computed for two topologies agree, for arbitrary sheaves of modules on a ringed site”.

Stacks 0GNE (3), the agreement clause. The internal hom of two sheaves of modules computed on a ringed site, read for a coarser topology, is the internal hom of their readings computed for the coarser topology.

This is the source's own argument for part (3): the internal hom of Stacks 03EM is a construction on presheaves of modules, and the topology enters only in the proof that the result is a sheaf, which needs the sheaf condition on the target alone. So no comparison map is involved — the two sheaves of modules have the same underlying presheaf of modules, and their sheaf conditions are propositions.

theorem coarsenModules_internalHomSheaf (X : RingedSite.{u, v, w})
    {J' : GrothendieckTopology X.C} (h : J' ≤ X.J)
    (A B : SheafOfModules.{m} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) :
    (coarsenModules X h).obj (internalHomSheaf X A B) =
      internalHomSheaf (X.ofLE h) ((coarsenModules X h).obj A)
        ((coarsenModules X h).obj B)

AlgebraicGeometry.BigFppfOver.restrictTopologyAssociatedModuleIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentTopologiesTwo/TopologyIndependence.lean, line 602. The attribute's comment: “the key to the proof: the associated-module functor is given by one formula for all five topologies, so its values for the five topologies agree”.

The key to Stacks 0GNE. The functor 𝓕 ↦ 𝓕^a is given by the same formula for every τ ∈ {Zariski, étale, smooth, syntomic, fppf}: the associated module of a quasi-coherent 𝒪_S-module on (Sch/S)_τ is the associated module on (Sch/S)_fppf, read for the coarser topology.

Every clause of the source's lemma is deduced from this, which is why it carries the tag: the source's proof of all three parts is "the equivalence of Proposition 03DX is given by the same formula independent of the choice of the topology", applied to a colimit, to a tensor product and to an internal hom.

noncomputable def restrictTopologyAssociatedModuleIso (τ : SiteKind) (F : S.Modules)
    [F.IsQuasicoherent] :
    (restrictTopology B S hS τ).obj ((associatedModule B S hS).obj F) ≅
      (baseAssociatedModule B S hS τ).obj F

AlgebraicGeometry.BigFppfOver.isColimitMapCoconeBaseAssociatedModuleQcoh, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentTopologiesTwo/TopologyIndependence.lean, line 762. The attribute's comment: “part (1), the colimit of a diagram of associated modules computed in Mod((Sch/S)_τ, O), for every one of the five topologies”.

Stacks 0GNE (1), the comparison with the modules of (Sch/S)_τ, every τ. A colimit of a diagram of quasi-coherent modules on S is carried by 𝓕 ↦ 𝓕^a to a colimit in Mod((Sch/S)_τ, 𝒪). Together with AlgebraicGeometry.BigFppfOver.restrictTopologyAssociatedModuleIso, which identifies the vertex at τ with the vertex at fppf read for the coarser topology, this says that the colimits computed in the five module categories agree.

The source states the clause for a diagram in QCoh((Sch/S)_fppf, 𝒪), and reduces it to a diagram in QCoh(𝒪_S) by the essential surjectivity of 𝓕 ↦ 𝓕^a; the diagram here is the reduced one. That reduction is now available, and the clause for an arbitrary diagram is AlgebraicGeometry.BigFppfOver.preservesColimitsOfSize_quasicoherentOnSite_ι_comp_restrictTopology (StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentTopologiesTwo/BigSiteColimitAgreement.lean).

noncomputable def isColimitMapCoconeBaseAssociatedModuleQcoh
    {D : K ⥤ (SheafOfModules.isQuasicoherent S.ringCatSheaf).FullSubcategory}
    {c : Cocone D} (hc : IsColimit c) :
    IsColimit ((baseAssociatedModuleQcoh B S hS τ).mapCocone c)

Declarations registered for the tag:

AlgebraicGeometry.RingedSite.internalHomSheaf_isQuasicoherent, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentTopologiesTwo/TopologyIndependence.lean, line 811 (StacksFrontier): “part (3), quasi-coherence of the common value”.

Sources

LeanAlgebraicGeometry.SmallEtale.isFlatMapULift_inverseImageStructureMap · AlgebraicGeometry.BigFppfOver.baseAssociatedModuleTensorIso · AlgebraicGeometry.BigFppfOver.essImage_X₂_of_shortExact_big · AlgebraicGeometry.BigFppfOver.exists_isoSections_X₂_of_shortExact_big · AlgebraicGeometry.BigFppfOver.fullyFaithfulBaseAssociatedModuleQcoh · AlgebraicGeometry.AssociatedModuleNotExact.not_mono_map_two_nsmul_qcoh · AlgebraicGeometry.AssociatedModuleNotExact.not_preservesMonomorphisms_baseAssociatedModuleQcoh · AlgebraicGeometry.AssociatedModuleNotExact.not_preservesFiniteLimits_baseAssociatedModuleQcoh

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

35.9 Cohomology of… to 35.10 Quasi-coherent sheaves…

Section35.9 Cohomology of quasi-coherent modules and topologies#

Tag 03FI, a lemma

Tag 03FJ, a lemma

Tag 03DW, a proposition

Tag 03LC, a proposition

Tag 071N, a lemma

Sources

Section35.10 Quasi-coherent sheaves and topologies, II#

Tag 0GNA, a lemma

Tag 06VE, a lemma

Tag 0GNB, a lemma

Tag 0GNC, a lemma

Tag 0GNE, a lemma

Sources

Section35.9 Cohomology of quasi-coherent modules and topologies #

Section35.10 Quasi-coherent sheaves and topologies, II #