104 Derived Categories of Stacks

Chapter 104 of the Stacks Project, Derived Categories of Stacks, Tag 08MW: the 6 sections of its 8 with a tag that a declaration carries, one article each, in the Stacks Project's order. Their 17 tags are carried by 131 declarations of the repository (all in StacksFrontier).

Section104.3 The lisse-étale and the flat-fppf sites#

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

Tag 07AS, a lemma

Tag 07AS in the Stacks Project.

AlgebraicGeometry.Stack.FlatFppf.hasLeftDerivedFunctor_abelianLowerShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfDerivedLowerShriek.lean, line 275. The attribute's comment: “part (3), existence; conditional on the acyclicity statement of 07AC”.

Stacks 07AS (3), existence, in the form that asserts nothing about how Lg_! is computed: degreewise lower shriek of abelian sheaves, followed by the localization of the homotopy category of Ab(𝒳_{fppf}), has a left derived functor along the localization of the homotopy category of Ab(𝒳_{flat,fppf}). This is the weakening of AlgebraicGeometry.Stack.FlatFppf.hasPointwiseLeftDerivedFunctor_abelianLowerShriek that forgets pointwise-ness.

theorem hasLeftDerivedFunctor_abelianLowerShriek
    (hFP : AbelianLowerShriekAcyclic B S hS 𝒳) :
    haveI := isContinuous_inclusion B S hS 𝒳 flatClosure
    haveI := isCocontinuous_inclusion B S hS 𝒳 flatClosure
    haveI := abelianLowerShriek_additive B S hS 𝒳
    ((abelianLowerShriek B S hS 𝒳 flatClosure).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
        DerivedCategory.Qh).HasLeftDerivedFunctor
      (HomotopyCategory.quasiIso
        (Sheaf (inclusionTopology B S hS 𝒳) AbCat.{u, u + 1}) (ComplexShape.up ℤ))

AlgebraicGeometry.Stack.FlatFppf.derivedAbelianLowerShriekAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfDerivedLowerShriek.lean, line 320. The attribute's comment: “part (3), adjointness; conditional on the acyclicity statement of 07AC”.

Stacks 07AS (3), adjointness: the derived lower-shriek functor on abelian sheaves is left adjoint to derived restriction, conditional on the closure property and on the acyclicity statement. This is Stacks 09T5 on the unbounded derived category of the Grothendieck abelian category Ab(𝒳_{fppf}), whose two inputs — existence of Lg_! and its absoluteness — both come from the acyclicity statement.

def derivedAbelianLowerShriekAdjunction (hFP : AbelianLowerShriekAcyclic B S hS 𝒳) :
    derivedAbelianLowerShriek B S hS 𝒳 hFP ⊣
      derivedAbelianRestriction B S hS 𝒳

AlgebraicGeometry.Stack.FlatFppf.derivedAbelianLowerShriekRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfDerivedLowerShriek.lean, line 349. The attribute's comment: “part (3), g^{-1} Lg_! = id; conditional on the acyclicity statement of 07AC”.

Stacks 07AS (3), the last assertion g⁻¹ Lg_! = id: restriction after derived lower shriek is canonically the identity of D(𝒳_{flat,fppf}), conditional on the closure property and on the acyclicity statement.

The ordinary unit F ⟶ g⁻¹ g_! F is an isomorphism, the inclusion of the flat objects being continuous, cocontinuous and fully faithful — that is Stacks 077I, proved as AlgebraicGeometry.Stack.FlatFppf.isIso_abelianLowerShriek_unit — and uniqueness of left derived functors carries that to the unit of the derived adjunction.

def derivedAbelianLowerShriekRestrictionIso (hFP : AbelianLowerShriekAcyclic B S hS 𝒳) :
    derivedAbelianLowerShriek B S hS 𝒳 hFP ⋙
        derivedAbelianRestriction B S hS 𝒳 ≅
      𝟭 (DerivedCategory (Sheaf (inclusionTopology B S hS 𝒳) AbCat.{u, u + 1}))

AlgebraicGeometry.Stack.FlatFppf.abelianLowerShriek_hasLeftDerivedFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfDerivedLowerShriekUnconditional.lean, line 98. The attribute's comment: “part (3), existence of the unbounded left derived functor Lg_! on abelian sheaves for the flat-fppf site, with NO hypothesis. The acyclicity statement of Tag 07AC that AlgebraicGeometry.Stack.FlatFppf.hasLeftDerivedFunctor_abelianLowerShriek carries as the argument hFP is discharged here by AlgebraicGeometry.Stack.FlatFppf.abelianLowerShriekAcyclic, which is proved for every algebraic stack out of the object-level vanishing of Tag 0D6X; that theorem lives downstream of the file carrying the conditional form, which is why the conditional form could not cite it. The closure condition of Tag 07AK (1) is likewise a theorem here, not a hypothesis. Only part (3) is covered: parts (1), (2) and (4) are elsewhere”.

Stacks 07AS (3), existence of Lg_!, for every algebraic stack. Degreewise lower shriek of abelian sheaves, followed by the localization of the homotopy category of Ab(𝒳_{fppf}), has a left derived functor along the localization of the homotopy category of Ab(𝒳_{flat,fppf}).

theorem abelianLowerShriek_hasLeftDerivedFunctor :
    haveI := isContinuous_inclusion B S hS 𝒳 flatClosure
    haveI := isCocontinuous_inclusion B S hS 𝒳 flatClosure
    haveI := abelianLowerShriek_additive B S hS 𝒳
    ((abelianLowerShriek B S hS 𝒳 flatClosure).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
        DerivedCategory.Qh).HasLeftDerivedFunctor
      (HomotopyCategory.quasiIso
        (Sheaf (inclusionTopology B S hS 𝒳) AbCat.{u, u + 1}) (ComplexShape.up ℤ))

AlgebraicGeometry.Stack.FlatFppf.derivedAbelianLowerShriekFunctorAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfDerivedLowerShriekUnconditional.lean, line 121. The attribute's comment: “part (3), the adjunction Lg_! ⊣ g⁻¹ on abelian sheaves for the flat-fppf site, with NO hypothesis: the acyclicity statement of Tag 07AC that AlgebraicGeometry.Stack.FlatFppf.derivedAbelianLowerShriekAdjunction carries as hFP is discharged by AlgebraicGeometry.Stack.FlatFppf.abelianLowerShriekAcyclic. Only part (3)”.

Stacks 07AS (3), adjointness, for every algebraic stack. The unbounded derived lower-shriek functor on abelian sheaves is left adjoint to derived restriction.

def derivedAbelianLowerShriekFunctorAdjunction :
    derivedAbelianLowerShriekFunctor B S hS 𝒳 ⊣ derivedAbelianRestriction B S hS 𝒳

AlgebraicGeometry.Stack.FlatFppf.derivedAbelianLowerShriekFunctorRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfDerivedLowerShriekUnconditional.lean, line 131. The attribute's comment: “part (3), g⁻¹ ∘ Lg_! = id on abelian sheaves for the flat-fppf site, with NO hypothesis: the acyclicity statement of Tag 07AC that AlgebraicGeometry.Stack.FlatFppf.derivedAbelianLowerShriekRestrictionIso carries as hFP is discharged by AlgebraicGeometry.Stack.FlatFppf.abelianLowerShriekAcyclic. Only part (3)”.

Stacks 07AS (3), g⁻¹ Lg_! = id, for every algebraic stack. Restriction after derived lower shriek is canonically the identity of D(𝒳_{flat,fppf}).

def derivedAbelianLowerShriekFunctorRestrictionIso :
    derivedAbelianLowerShriekFunctor B S hS 𝒳 ⋙ derivedAbelianRestriction B S hS 𝒳 ≅
      𝟭 (DerivedCategory (Sheaf (inclusionTopology B S hS 𝒳) AbCat.{u, u + 1}))

AlgebraicGeometry.Stack.LisseEtale.abelianLowerShriek_hasLeftDerivedFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleDerivedLowerShriek.lean, line 306. The attribute's comment: “part (1), existence of the unbounded left derived functor Lg_! on abelian sheaves for the lisse-étale site, with NO hypothesis. The acyclicity statement of Tag 07AC is discharged by AlgebraicGeometry.Stack.LisseEtale.abelianLowerShriekAcyclic, which is proved for every algebraic stack out of the object-level vanishing of Tag 0D6X, AlgebraicGeometry.Stack.LisseEtale.objectAcyclic. The closure condition of Tag 07AK (1) for the smooth objects is likewise a theorem here, not a hypothesis, namely AlgebraicGeometry.Stack.LisseEtale.closedUnderSmoothMorphisms. Only the abelian-sheaf statement for the lisse-étale site is covered: parts (2) and (4) are the module-level statements, which the source does not know to agree with the abelian one, and part (3) is the flat-fppf site”.

Stacks 07AS (1), existence of Lg_!, for every algebraic stack. Degreewise lower shriek of abelian sheaves, followed by the localization of the homotopy category of Ab(𝒳_{étale}), has a left derived functor along the localization of the homotopy category of Ab(𝒳_{lisse,étale}). This is the weakening of AlgebraicGeometry.Stack.LisseEtale.abelianLowerShriek_hasPointwiseLeftDerivedFunctor that forgets pointwise-ness.

theorem abelianLowerShriek_hasLeftDerivedFunctor :
    haveI := isContinuous_inclusion.{u, w} B S hS 𝒳 (closedUnderSmoothMorphisms.{u, w} B S hS 𝒳)
    haveI := isCocontinuous_inclusion.{u, w} B S hS 𝒳 (closedUnderSmoothMorphisms.{u, w} B S hS 𝒳)
    haveI := abelianLowerShriek_additive.{u, w} B S hS 𝒳
    ((abelianLowerShriek.{u, w} B S hS 𝒳
      (closedUnderSmoothMorphisms.{u, w} B S hS 𝒳)).mapHomotopyCategory
        (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh).HasLeftDerivedFunctor
      (HomotopyCategory.quasiIso
        (Sheaf (inclusionTopology.{u, w} B S hS 𝒳) AbCat.{u, u + 1}) (ComplexShape.up ℤ))

AlgebraicGeometry.Stack.LisseEtale.derivedAbelianLowerShriekAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleDerivedLowerShriek.lean, line 391. The attribute's comment: “part (1), the adjunction Lg_! ⊣ g⁻¹ on abelian sheaves for the lisse-étale site, with NO hypothesis: the acyclicity statement of Tag 07AC that supplies both the existence of Lg_! and its absoluteness is discharged by AlgebraicGeometry.Stack.LisseEtale.abelianLowerShriekAcyclic, itself proved out of the object-level vanishing of Tag 0D6X, AlgebraicGeometry.Stack.LisseEtale.objectAcyclic, and the closure condition of Tag 07AK (1) by AlgebraicGeometry.Stack.LisseEtale.closedUnderSmoothMorphisms. Only the abelian-sheaf statement for the lisse-étale site: parts (2) and (4) are the module-level statements and part (3) is the flat-fppf site”.

Stacks 07AS (1), adjointness, for every algebraic stack. The unbounded derived lower-shriek functor on abelian sheaves is left adjoint to derived restriction. This is Stacks 09T5 on the unbounded derived category of the Grothendieck abelian category Ab(𝒳_{étale}), whose two inputs — existence of Lg_! and its absoluteness — both come from the acyclicity statement.

def derivedAbelianLowerShriekAdjunction :
    derivedAbelianLowerShriek.{u, w} B S hS 𝒳 ⊣ derivedAbelianRestriction.{u, w} B S hS 𝒳

AlgebraicGeometry.Stack.LisseEtale.derivedAbelianLowerShriekRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleDerivedLowerShriek.lean, line 419. The attribute's comment: “part (1), g⁻¹ ∘ Lg_! = id on abelian sheaves for the lisse-étale site, with NO hypothesis: the acyclicity statement of Tag 07AC is discharged by AlgebraicGeometry.Stack.LisseEtale.abelianLowerShriekAcyclic, out of the object-level vanishing of Tag 0D6X, AlgebraicGeometry.Stack.LisseEtale.objectAcyclic; the closure condition of Tag 07AK (1) by AlgebraicGeometry.Stack.LisseEtale.closedUnderSmoothMorphisms; and the invertibility of the ordinary unit is Tag 077I, AlgebraicGeometry.Stack.LisseEtale.isIso_abelianLowerShriek_unit. Only the abelian-sheaf statement for the lisse-étale site: parts (2) and (4) are the module-level statements and part (3) is the flat-fppf site”.

Stacks 07AS (1), g⁻¹ Lg_! = id, for every algebraic stack. Restriction after derived lower shriek is canonically the identity of D(𝒳_{lisse,étale}).

The ordinary unit F ⟶ g⁻¹ g_! F is an isomorphism, the inclusion of the smooth objects being continuous, cocontinuous and fully faithful — that is Stacks 077I, which for this inclusion is AlgebraicGeometry.Stack.LisseEtale.isIso_abelianLowerShriek_unit — and uniqueness of left derived functors carries that to the unit of the derived adjunction.

def derivedAbelianLowerShriekRestrictionIso :
    derivedAbelianLowerShriek.{u, w} B S hS 𝒳 ⋙ derivedAbelianRestriction.{u, w} B S hS 𝒳 ≅
      𝟭 (DerivedCategory (Sheaf (inclusionTopology.{u, w} B S hS 𝒳) AbCat.{u, u + 1}))

AlgebraicGeometry.Stack.LisseEtale.abelianLowerShriek_derived, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteAbelianDerivedLowerShriek.lean, line 67. The attribute's comment: “part (1), the whole of it: existence of the unbounded left derived functor Lg_! of g_! on abelian sheaves for the lisse-étale site, its adjunction Lg_! ⊣ g⁻¹ (with invertible unit), and g⁻¹ ∘ Lg_! = id, for every algebraic stack and with NO hypothesis. The acyclicity statement of Tag 07AC is the theorem AlgebraicGeometry.Stack.LisseEtale.abelianLowerShriekAcyclic and the invertibility of the ordinary unit is Tag 077I”.

Stacks 07AS (1), all three assertions, for every algebraic stack and with NO hypothesis. For g : Sh(𝒳_{lisse,étale}) ⟶ Sh(𝒳_{étale}) the comparison morphism of topoi of Stacks 0788 (1):

• the functor g_! : Ab(𝒳_{lisse,étale}) ⥤ Ab(𝒳_{étale}) has a left derived functor Lg_! : D(𝒳_{lisse,étale}) ⟶ D(𝒳_{étale}) — degreewise g_! followed by the localization of the homotopy category of Ab(𝒳_{étale}) has a pointwise left derived functor along the localization of the homotopy category of Ab(𝒳_{lisse,étale}), and Lg_! is that total left derived functor;
• Lg_! is left adjoint to g⁻¹, by an adjunction whose unit is an isomorphism;
• g⁻¹ ∘ Lg_! = id.

theorem abelianLowerShriek_derived :
    haveI := isContinuous_inclusion.{u, w} B S hS 𝒳 (closedUnderSmoothMorphisms.{u, w} B S hS 𝒳)
    haveI := isCocontinuous_inclusion.{u, w} B S hS 𝒳 (closedUnderSmoothMorphisms.{u, w} B S hS 𝒳)
    haveI := abelianLowerShriek_additive.{u, w} B S hS 𝒳
    ((abelianLowerShriek.{u, w} B S hS 𝒳
        (closedUnderSmoothMorphisms.{u, w} B S hS 𝒳)).mapHomotopyCategory
        (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh).HasPointwiseLeftDerivedFunctor
      (HomotopyCategory.quasiIso
        (Sheaf (inclusionTopology.{u, w} B S hS 𝒳) AbCat.{u, u + 1}) (ComplexShape.up ℤ)) ∧
    (∃ adj : derivedAbelianLowerShriek.{u, w} B S hS 𝒳 ⊣
        derivedAbelianRestriction.{u, w} B S hS 𝒳, IsIso adj.unit) ∧
    Nonempty (derivedAbelianLowerShriek.{u, w} B S hS 𝒳 ⋙
        derivedAbelianRestriction.{u, w} B S hS 𝒳 ≅
      𝟭 (DerivedCategory (Sheaf (inclusionTopology.{u, w} B S hS 𝒳) AbCat.{u, u + 1})))

AlgebraicGeometry.Stack.FlatFppf.abelianLowerShriek_derived, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteAbelianDerivedLowerShriek.lean, line 109. The attribute's comment: “part (3), the whole of it: existence of the unbounded left derived functor Lg_! of g_! on abelian sheaves for the flat-fppf site, its adjunction Lg_! ⊣ g⁻¹ (with invertible unit), and g⁻¹ ∘ Lg_! = id, for every algebraic stack and with NO hypothesis. The acyclicity statement of Tag 07AC is the theorem AlgebraicGeometry.Stack.FlatFppf.abelianLowerShriekAcyclic and the invertibility of the ordinary unit is Tag 077I”.

Stacks 07AS (3), all three assertions, for every algebraic stack and with NO hypothesis. For g : Sh(𝒳_{flat,fppf}) ⟶ Sh(𝒳_{fppf}) the comparison morphism of topoi of Stacks 0788 (2):

• the functor g_! : Ab(𝒳_{flat,fppf}) ⥤ Ab(𝒳_{fppf}) has a left derived functor Lg_! : D(𝒳_{flat,fppf}) ⟶ D(𝒳_{fppf}) — degreewise g_! followed by the localization of the homotopy category of Ab(𝒳_{fppf}) has a pointwise left derived functor along the localization of the homotopy category of Ab(𝒳_{flat,fppf}), and Lg_! is that total left derived functor;
• Lg_! is left adjoint to g⁻¹, by an adjunction whose unit is an isomorphism;
• g⁻¹ ∘ Lg_! = id.

theorem abelianLowerShriek_derived :
    haveI := isContinuous_inclusion B S hS 𝒳 flatClosure
    haveI := isCocontinuous_inclusion B S hS 𝒳 flatClosure
    haveI := abelianLowerShriek_additive B S hS 𝒳
    ((abelianLowerShriek B S hS 𝒳 flatClosure).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
        DerivedCategory.Qh).HasPointwiseLeftDerivedFunctor
      (HomotopyCategory.quasiIso
        (Sheaf (inclusionTopology B S hS 𝒳) AbCat.{u, u + 1}) (ComplexShape.up ℤ)) ∧
    (∃ adj : derivedAbelianLowerShriekFunctor B S hS 𝒳 ⊣ derivedAbelianRestriction B S hS 𝒳,
      IsIso adj.unit) ∧
    Nonempty (derivedAbelianLowerShriekFunctor B S hS 𝒳 ⋙ derivedAbelianRestriction B S hS 𝒳 ≅
      𝟭 (DerivedCategory (Sheaf (inclusionTopology B S hS 𝒳) AbCat.{u, u + 1})))

AlgebraicGeometry.Stack.FlatFppf.lowerShriekModules_derived, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteModuleDerivedLowerShriek.lean, line 443. The attribute's comment: “part (4), the whole of it: existence of the unbounded left derived functor Lg_! of g_! on sheaves of modules for the flat-fppf site, its adjunction Lg_! ⊣ g^* (with invertible unit), and g^* ∘ Lg_! = id, for every algebraic stack and with NO hypothesis. The structure sheaf is the one of Tag 06TV; the acyclicity statement of Tag 07AC is a theorem here, AlgebraicGeometry.Stack.subsiteLowerShriekModulesAcyclic, and the invertibility of the ordinary unit is Tag 077I”.

Stacks 07AS (4), all three assertions, for every algebraic stack and with NO hypothesis. For g : Sh(𝒳_{flat,fppf}) ⟶ Sh(𝒳_τ) the morphism of ringed topoi of Stacks 0788:

• the functor g_! : Mod(𝒪_{𝒳_{flat,fppf}}) ⥤ Mod(𝒪_𝒳) has a left derived functor Lg_! : D(𝒪_{𝒳_{flat,fppf}}) ⟶ D(𝒪_𝒳) — degreewise g_! followed by the localization of the homotopy category of Mod(𝒪_𝒳) has a pointwise left derived functor along the localization of the homotopy category of Mod(𝒪_{𝒳_{flat,fppf}}), and Lg_! is that total left derived functor;
• Lg_! is left adjoint to g^*, by an adjunction whose unit is an isomorphism;
• g^* ∘ Lg_! = id.

The structure sheaf is the one of Stacks 06TV, with sections in Type u, and the modules have their sections in Type (u+1).

theorem lowerShriekModules_derived :
    (FreeRingUniverse.lowerShriekOnHomotopy.{u + 1} (inclusionTopology B S hS 𝒳)
        (associatedTopology B S hS 𝒳.val.val.p B.topology) (objectProperty B S hS 𝒳).ι
        (moduleRing B S hS 𝒳) ⋙
      DerivedCategory.Qh).HasPointwiseLeftDerivedFunctor
        (FreeRingUniverse.sourceQuasiIso.{u + 1} (inclusionTopology B S hS 𝒳)
        (associatedTopology B S hS 𝒳.val.val.p B.topology) (objectProperty B S hS 𝒳).ι
        (moduleRing B S hS 𝒳)) ∧
    (∃ adj : derivedLowerShriekModules B S hS 𝒳 ⊣ derivedRestrictionModules B S hS 𝒳,
      IsIso adj.unit) ∧
    Nonempty (derivedLowerShriekModules B S hS 𝒳 ⋙ derivedRestrictionModules B S hS 𝒳 ≅
      𝟭 (DerivedCategory (SheafOfModules.{u + 1} (subsiteModuleRingFlat B S hS 𝒳))))

AlgebraicGeometry.Stack.LisseEtale.lowerShriekModules_derived, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteModuleDerivedLowerShriek.lean, line 572. The attribute's comment: “part (2), the whole of it: existence of the unbounded left derived functor Lg_! of g_! on sheaves of modules for the lisse-étale site, its adjunction Lg_! ⊣ g^* (with invertible unit), and g^* ∘ Lg_! = id, for every algebraic stack and with NO hypothesis. The structure sheaf is the one of Tag 06TV; the acyclicity statement of Tag 07AC is a theorem here, AlgebraicGeometry.Stack.subsiteLowerShriekModulesAcyclic, and the invertibility of the ordinary unit is Tag 077I”.

Stacks 07AS (2), all three assertions, for every algebraic stack and with NO hypothesis. For g : Sh(𝒳_{lisse,étale}) ⟶ Sh(𝒳_τ) the morphism of ringed topoi of Stacks 0788:

• the functor g_! : Mod(𝒪_{𝒳_{lisse,étale}}) ⥤ Mod(𝒪_𝒳) has a left derived functor Lg_! : D(𝒪_{𝒳_{lisse,étale}}) ⟶ D(𝒪_𝒳) — degreewise g_! followed by the localization of the homotopy category of Mod(𝒪_𝒳) has a pointwise left derived functor along the localization of the homotopy category of Mod(𝒪_{𝒳_{lisse,étale}}), and Lg_! is that total left derived functor;
• Lg_! is left adjoint to g^*, by an adjunction whose unit is an isomorphism;
• g^* ∘ Lg_! = id.

The structure sheaf is the one of Stacks 06TV, with sections in Type u, and the modules have their sections in Type (u+1).

theorem lowerShriekModules_derived :
    (FreeRingUniverse.lowerShriekOnHomotopy.{u + 1} (inclusionTopology.{u, w} B S hS 𝒳)
        (ambientTopology B S hS 𝒳) (smoothObject.{u, w} B S hS 𝒳).ι
        (moduleRing.{u, w} B S hS 𝒳) ⋙
      DerivedCategory.Qh).HasPointwiseLeftDerivedFunctor
        (FreeRingUniverse.sourceQuasiIso.{u + 1} (inclusionTopology.{u, w} B S hS 𝒳)
        (ambientTopology B S hS 𝒳) (smoothObject.{u, w} B S hS 𝒳).ι
        (moduleRing.{u, w} B S hS 𝒳)) ∧
    (∃ adj : derivedLowerShriekModules B S hS 𝒳 ⊣ derivedRestrictionModules B S hS 𝒳,
      IsIso adj.unit) ∧
    Nonempty (derivedLowerShriekModules B S hS 𝒳 ⋙ derivedRestrictionModules B S hS 𝒳 ≅
      𝟭 (DerivedCategory (SheafOfModules.{u + 1} (subsiteModuleRingSmooth B S hS 𝒳))))

Tag 07AV, a lemma

Tag 07AV in the Stacks Project.

AlgebraicGeometry.Stack.FlatFppf.derivedRestrictionBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfDerivedBaseChange.lean, line 112. The attribute's comment: “the flat-fppf case for abelian sheaves, first identity: g⁻¹ ∘ Rf_ = Rf'_ ∘ (g')⁻¹ on the unbounded derived categories, as an isomorphism (g')⁻¹ ⋙ Rf'_ ≅ Rf_ ⋙ g⁻¹ for any total right derived functors Rf_, Rf'_ of the two direct images, with no further hypothesis. The degree-zero square of Stacks 07AT (2) and the fact that restricted K-injective complexes compute Rf'_* (Stacks 07AK at the 2-fibre products V ×_y 𝒳, the content of Stacks 0GR3) are proved, not assumed”.

Stacks 07AV, first identity, for abelian sheaves on the flat-fppf sites: g⁻¹ ∘ Rf_* = Rf'_* ∘ (g')⁻¹. Let f : 𝒳 ⟶ 𝒴 be a flat 1-morphism of algebraic stacks, Rf_* and Rf'_* total right derived functors of the direct images along f and along its restriction f' to the flat-fppf sites, and g⁻¹, (g')⁻¹ restriction of abelian sheaves to the flat-fppf sites of 𝒴 and 𝒳. Then, on the unbounded derived categories,

(g')⁻¹ ⋙ Rf'_* ≅ Rf_* ⋙ g⁻¹.

No hypothesis is made beyond the right derived functor properties of Rf_* and Rf'_* (a right derived functor being determined only up to unique isomorphism). The isomorphism is Stacks.Cohomology.UnboundedComplexes.derivedBaseChangeIsoOfUnit at the degree-zero identification AlgebraicGeometry.Stack.FlatFppf.isIso_abelianSheafBaseChange and at AlgebraicGeometry.Stack.FlatFppf.isIso_derivedPushforwardUnit_restriction.

def derivedRestrictionBaseChangeIso
    (Rf : DerivedCategory (Sheaf (associatedTopology B S hS 𝒳.val.val.p B.topology)
        AddCommGrpCat.{u + 1}) ⥤
      DerivedCategory (Sheaf (associatedTopology B S hS 𝒴.val.val.p B.topology)
        AddCommGrpCat.{u + 1}))
    (Rf' : DerivedCategory (Sheaf (inclusionTopology B S hS 𝒳) AddCommGrpCat.{u + 1}) ⥤
      DerivedCategory (Sheaf (inclusionTopology B S hS 𝒴) AddCommGrpCat.{u + 1}))
    (αf : haveI := (isContinuous_and_isCocontinuous_homFunctor B S hS f).2
      haveI : (f.hom.hom.toFunctor.sheafPushforwardCocontinuous AddCommGrpCat.{u + 1}
          (associatedTopology B S hS 𝒳.val.val.p B.topology)
          (associatedTopology B S hS 𝒴.val.val.p B.topology)).Additive :=
        Functor.sheafPushforwardCocontinuous_additive.{u + 1, u + 1, u, u, u + 1} _ _ _
      (f.hom.hom.toFunctor.sheafPushforwardCocontinuous AddCommGrpCat.{u + 1}
          (associatedTopology B S hS 𝒳.val.val.p B.topology)
          (associatedTopology B S hS 𝒴.val.val.p B.topology)).mapHomotopyCategory
        (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rf)
    (αf' : haveI := isCocontinuous_subsiteFunctor B S hS f hf
      haveI : ((SubsitePushforward.subsiteFunctor f.hom.hom.toFunctor
          (flatObject B S hS 𝒳.val)
          (flatObject_map B S hS f hf)).sheafPushforwardCocontinuous
        AddCommGrpCat.{u + 1} (inclusionTopology B S hS 𝒳)
        (inclusionTopology B S hS 𝒴)).Additive :=
        Functor.sheafPushforwardCocontinuous_additive.{u + 1, u + 1, u, u, u + 1} _ _ _
      ((SubsitePushforward.subsiteFunctor f.hom.hom.toFunctor (flatObject B S hS 𝒳.val)
          (flatObject_map B S hS f hf)).sheafPushforwardCocontinuous
        AddCommGrpCat.{u + 1} (inclusionTopology B S hS 𝒳)
        (inclusionTopology B S hS 𝒴)).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
        DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rf')
    [hRf : Rf.IsRightDerivedFunctor αf (HomotopyCategory.quasiIso
      (Sheaf (associatedTopology B S hS 𝒳.val.val.p B.topology) AddCommGrpCat.{u + 1})
      (ComplexShape.up ℤ))]
    [hRf' : Rf'.IsRightDerivedFunctor αf' (HomotopyCategory.quasiIso
      (Sheaf (inclusionTopology B S hS 𝒳) AddCommGrpCat.{u + 1}) (ComplexShape.up ℤ))] :
    haveI := isContinuous_inclusion B S hS 𝒳 (closedUnderFlatMorphisms B S hS 𝒳)
    haveI := isContinuous_inclusion B S hS 𝒴 (closedUnderFlatMorphisms B S hS 𝒴)
    haveI := additive_subsiteRestriction B S hS 𝒳
    haveI := additive_subsiteRestriction B S hS 𝒴
    haveI := preservesFiniteLimits_subsiteRestriction B S hS 𝒳
    haveI := preservesFiniteLimits_subsiteRestriction B S hS 𝒴
    haveI := preservesFiniteColimits_subsiteRestriction B S hS 𝒳
    haveI := preservesFiniteColimits_subsiteRestriction B S hS 𝒴
    (subsiteRestriction B S hS 𝒳.val.val.p B.topology
        (flatObject B S hS 𝒳.val)).mapDerivedCategory ⋙ Rf' ≅
      Rf ⋙ (subsiteRestriction B S hS 𝒴.val.val.p B.topology
        (flatObject B S hS 𝒴.val)).mapDerivedCategory

AlgebraicGeometry.Stack.FlatFppf.derivedLowerShriekBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfDerivedBaseChange.lean, line 344. The attribute's comment: “the flat-fppf case for abelian sheaves, second identity: L(g')_! ∘ (f')⁻¹ = f⁻¹ ∘ Lg_! on the unbounded derived categories, as an isomorphism Lg_! ⋙ f⁻¹ ≅ (f')⁻¹ ⋙ L(g')_! of the canonical functors, with no hypothesis: the derived lower shrieks are those of Stacks 07AS (3), and the four derived adjunctions are constructed”.

Stacks 07AV, second identity, for abelian sheaves on the flat-fppf sites: L(g')_! ∘ (f')⁻¹ = f⁻¹ ∘ Lg_!. For a flat 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks, with Lg_! and L(g')_! the derived lower shrieks of Stacks 07AS (1) for 𝒴 and 𝒳, and f⁻¹, (f')⁻¹ the inverse images along f and along its restriction f' to the flat-fppf sites,

Lg_! ⋙ f⁻¹ ≅ (f')⁻¹ ⋙ L(g')_!

on the unbounded derived categories of abelian sheaves. All four functors are the canonical ones and no hypothesis is made. The isomorphism is the conjugate, under the composites of the derived adjunctions Lg_! ⊣ g⁻¹, L(g')_! ⊣ (g')⁻¹ of Stacks 07AS (3) and f⁻¹ ⊣ Rf_*, (f')⁻¹ ⊣ Rf'_* (exact left adjoints), of the first identity AlgebraicGeometry.Stack.FlatFppf.derivedRestrictionBaseChangeIso.

def derivedLowerShriekBaseChangeIso :
    derivedAbelianLowerShriekFunctor B S hS 𝒴 ⋙ derivedAbelianInverseImage B S hS f ≅
      derivedAbelianSubsiteInverseImage B S hS f hf ⋙ derivedAbelianLowerShriekFunctor B S hS 𝒳

AlgebraicGeometry.Stack.FlatFppf.moduleDerivedRestrictionBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfModuleDerivedBaseChange.lean, line 178. The attribute's comment: “the module case for the flat-fppf sites, first identity: g⁻¹ ∘ Rf_ = Rf'_ ∘ (g')⁻¹ on the unbounded derived categories of sheaves of modules, as an isomorphism (g')^ ⋙ Rf'_ ≅ Rf_ ⋙ g^ for any total right derived functors Rf_, Rf'_ of the two direct images, with no further hypothesis: the degree-zero square of Stacks 07AT (2) on modules and the fact that restricted K-injective complexes of modules compute Rf'_* (Stacks 0D6J with Stacks 07AK at the 2-fibre products V ×_y 𝒳) are proved, not assumed”.

Stacks 07AV, first identity, for sheaves of modules on the flat-fppf sites: g^* ∘ Rf_* = Rf'_* ∘ (g')^*. For a flat 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks, total right derived functors Rf_*, Rf'_* of the direct images of sheaves of modules along f and along its restriction f' to the flat-fppf sites, and g^*, (g')^* the restrictions of sheaves of modules to the flat-fppf sites (which are g⁻¹, (g')⁻¹),

(g')^* ⋙ Rf'_* ≅ Rf_* ⋙ g^*

on the unbounded derived categories, with no further hypothesis. It is Stacks.Cohomology.UnboundedComplexes.derivedBaseChangeIsoOfUnit at the degree-zero square AlgebraicGeometry.Stack.FlatFppf.isIso_moduleSquareComparison and at Stacks.SheafOfModules.isIso_derivedPushforwardUnit_inverseImage, fed with AlgebraicGeometry.Stack.FlatFppf.qh_map_bijective_directImageCorep_restriction.

def moduleDerivedRestrictionBaseChangeIso
    (Rf : DerivedCategory (_root_.SheafOfModules.{u + 1} (ambientRingStructureSheaf B S hS 𝒳)) ⥤
      DerivedCategory (_root_.SheafOfModules.{u + 1} (ambientRingStructureSheaf B S hS 𝒴)))
    (Rf' : DerivedCategory (_root_.SheafOfModules.{u + 1} (subsiteRingStructureSheaf B S hS 𝒳)) ⥤
      DerivedCategory (_root_.SheafOfModules.{u + 1} (subsiteRingStructureSheaf B S hS 𝒴)))
    (αf : (modulePushforward B S hS f).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rf)
    (αf' : (moduleSubsitePushforward B S hS f hf).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rf')
    [hRf : Rf.IsRightDerivedFunctor αf (HomotopyCategory.quasiIso
      (_root_.SheafOfModules.{u + 1} (ambientRingStructureSheaf B S hS 𝒳)) (ComplexShape.up ℤ))]
    [hRf' : Rf'.IsRightDerivedFunctor αf' (HomotopyCategory.quasiIso
      (_root_.SheafOfModules.{u + 1} (subsiteRingStructureSheaf B S hS 𝒳)) (ComplexShape.up ℤ))] :
    (moduleInverseImage B S hS 𝒳).mapDerivedCategory ⋙ Rf' ≅
      Rf ⋙ (moduleInverseImage B S hS 𝒴).mapDerivedCategory

AlgebraicGeometry.Stack.FlatFppf.moduleDerivedLowerShriekBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfModuleDerivedBaseChange.lean, line 353. The attribute's comment: “the module case for the flat-fppf sites, second identity: L(g')_! ∘ (f')⁻¹ = f⁻¹ ∘ Lg_! on the unbounded derived categories of sheaves of modules, as an isomorphism Lg_! ⋙ f⁻¹ ≅ (f')⁻¹ ⋙ L(g')_! for the actual derived lower shrieks and the exact inverse images, with no hypothesis: the adjunctions Lg_! ⊣ g⁻¹, f⁻¹ ⊣ Rf_* and their primed versions are constructed, and the first identity is proved”.

Stacks 07AV, the module case for the flat-fppf sites, second identity. Let f : 𝒳 ⟶ 𝒴 be a flat 1-morphism of algebraic stacks, f' its restriction to the flat-fppf sites, and Lg_!, L(g')_! the derived lower shrieks of sheaves of modules along the inclusions of the flat-fppf sites (AlgebraicGeometry.Stack.FlatFppf.derivedModuleLowerShriekSucc). Then

Lg_! ⋙ f^{-1} ≅ (f')^{-1} ⋙ L(g')_!

on the unbounded derived categories of sheaves of modules, that is, L(g')_! ∘ (f')^{-1} = f^{-1} ∘ Lg_!. Here f^{-1}, (f')^{-1} are the exact inverse images (Stacks 06WE, and restriction along f'), left adjoint to the canonical total right derived direct images Rf_*, Rf'_* (derivedAdjunctionOfExactLeftAdjoint on AlgebraicGeometry.Stack.FlatFppf.modulePullbackPushforwardAdjunction and AlgebraicGeometry.Stack.FlatFppf.moduleSubsiteInverseImageAdjunction), and the isomorphism is the conjugate, across the composed adjunctions, of the first identity AlgebraicGeometry.Stack.FlatFppf.moduleDerivedRestrictionBaseChangeIso.

def moduleDerivedLowerShriekBaseChangeIso :
    derivedModuleLowerShriekSucc B S hS 𝒴 ⋙ derivedModulePullback B S hS f ≅
      derivedModuleSubsiteInverseImage B S hS f hf ⋙ derivedModuleLowerShriekSucc B S hS 𝒳

AlgebraicGeometry.Stack.LisseEtale.derivedRestrictionBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleDerivedBaseChange.lean, line 163. The attribute's comment: “the lisse-étale case for abelian sheaves, first identity: g⁻¹ ∘ Rf_ = Rf'_ ∘ (g')⁻¹ on the unbounded derived categories, as an isomorphism (g')⁻¹ ⋙ Rf'_ ≅ Rf_ ⋙ g⁻¹ for any total right derived functors Rf_, Rf'_ of the two direct images, with no further hypothesis. The degree-zero square of Stacks 07AT (1) and the fact that restricted K-injective complexes compute Rf'_* (Stacks 07AK at the 2-fibre products V ×_y 𝒳, the content of Stacks 0GR3) are proved, not assumed”.

Stacks 07AV, first identity, for abelian sheaves on the lisse-étale sites: g⁻¹ ∘ Rf_* = Rf'_* ∘ (g')⁻¹. Let f : 𝒳 ⟶ 𝒴 be a smooth 1-morphism of algebraic stacks, Rf_* and Rf'_* total right derived functors of the direct images along f and along its restriction f' to the lisse-étale sites, and g⁻¹, (g')⁻¹ restriction of abelian sheaves to the lisse-étale sites of 𝒴 and 𝒳. Then, on the unbounded derived categories,

(g')⁻¹ ⋙ Rf'_* ≅ Rf_* ⋙ g⁻¹.

No hypothesis is made beyond the right derived functor properties of Rf_* and Rf'_* (a right derived functor being determined only up to unique isomorphism). The isomorphism is Stacks.Cohomology.UnboundedComplexes.derivedBaseChangeIsoOfUnit at the degree-zero identification AlgebraicGeometry.Stack.LisseEtale.isIso_abelianSheafBaseChange and at AlgebraicGeometry.Stack.LisseEtale.isIso_derivedPushforwardUnit_restriction.

def derivedRestrictionBaseChangeIso
    (Rf : DerivedCategory (Sheaf (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
        AddCommGrpCat.{u + 1}) ⥤
      DerivedCategory (Sheaf (associatedTopology B S hS 𝒴.val.val.p (etaleTopology B))
        AddCommGrpCat.{u + 1}))
    (Rf' : DerivedCategory (Sheaf (inclusionTopology.{u, w} B S hS 𝒳) AddCommGrpCat.{u + 1}) ⥤
      DerivedCategory (Sheaf (inclusionTopology.{u, w} B S hS 𝒴) AddCommGrpCat.{u + 1}))
    (αf : haveI := (isContinuous_and_isCocontinuous_homFunctor_associatedTopology B S hS f
        (etaleTopology B)).2
      haveI : (f.hom.hom.toFunctor.sheafPushforwardCocontinuous AddCommGrpCat.{u + 1}
          (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
          (associatedTopology B S hS 𝒴.val.val.p (etaleTopology B))).Additive :=
        Functor.sheafPushforwardCocontinuous_additive.{u + 1, u + 1, u, u, u + 1} _ _ _
      (f.hom.hom.toFunctor.sheafPushforwardCocontinuous AddCommGrpCat.{u + 1}
          (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
          (associatedTopology B S hS 𝒴.val.val.p (etaleTopology B))).mapHomotopyCategory
        (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rf)
    (αf' : haveI := isCocontinuous_subsiteFunctor.{u, w} B S hS f hf
      haveI : ((SubsitePushforward.subsiteFunctor f.hom.hom.toFunctor
          (smoothObject.{u, w} B S hS 𝒳)
          (smoothObject_map.{u, w} B S hS f hf)).sheafPushforwardCocontinuous
        AddCommGrpCat.{u + 1} (inclusionTopology.{u, w} B S hS 𝒳)
        (inclusionTopology.{u, w} B S hS 𝒴)).Additive :=
        Functor.sheafPushforwardCocontinuous_additive.{u + 1, u + 1, u, u, u + 1} _ _ _
      ((SubsitePushforward.subsiteFunctor f.hom.hom.toFunctor (smoothObject.{u, w} B S hS 𝒳)
          (smoothObject_map.{u, w} B S hS f hf)).sheafPushforwardCocontinuous
        AddCommGrpCat.{u + 1} (inclusionTopology.{u, w} B S hS 𝒳)
        (inclusionTopology.{u, w} B S hS 𝒴)).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
        DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rf')
    [hRf : Rf.IsRightDerivedFunctor αf (HomotopyCategory.quasiIso
      (Sheaf (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B)) AddCommGrpCat.{u + 1})
      (ComplexShape.up ℤ))]
    [hRf' : Rf'.IsRightDerivedFunctor αf' (HomotopyCategory.quasiIso
      (Sheaf (inclusionTopology.{u, w} B S hS 𝒳) AddCommGrpCat.{u + 1}) (ComplexShape.up ℤ))] :
    haveI := isContinuous_inclusion.{u, w} B S hS 𝒳 (closedUnderSmoothMorphisms.{u, w} B S hS 𝒳)
    haveI := isContinuous_inclusion.{u, w} B S hS 𝒴 (closedUnderSmoothMorphisms.{u, w} B S hS 𝒴)
    haveI := additive_subsiteRestriction B S hS 𝒳
    haveI := additive_subsiteRestriction B S hS 𝒴
    haveI := preservesFiniteLimits_subsiteRestriction B S hS 𝒳
    haveI := preservesFiniteLimits_subsiteRestriction B S hS 𝒴
    haveI := preservesFiniteColimits_subsiteRestriction B S hS 𝒳
    haveI := preservesFiniteColimits_subsiteRestriction B S hS 𝒴
    (subsiteRestriction B S hS 𝒳.val.val.p (etaleTopology B)
        (smoothObject.{u, w} B S hS 𝒳)).mapDerivedCategory ⋙ Rf' ≅
      Rf ⋙ (subsiteRestriction B S hS 𝒴.val.val.p (etaleTopology B)
        (smoothObject.{u, w} B S hS 𝒴)).mapDerivedCategory

AlgebraicGeometry.Stack.LisseEtale.derivedLowerShriekBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleDerivedBaseChange.lean, line 402. The attribute's comment: “the lisse-étale case for abelian sheaves, second identity: L(g')_! ∘ (f')⁻¹ = f⁻¹ ∘ Lg_! on the unbounded derived categories, as an isomorphism Lg_! ⋙ f⁻¹ ≅ (f')⁻¹ ⋙ L(g')_! of the canonical functors, with no hypothesis: the derived lower shrieks are those of Stacks 07AS (1), and the four derived adjunctions are constructed”.

Stacks 07AV, second identity, for abelian sheaves on the lisse-étale sites: L(g')_! ∘ (f')⁻¹ = f⁻¹ ∘ Lg_!. For a smooth 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks, with Lg_! and L(g')_! the derived lower shrieks of Stacks 07AS (1) for 𝒴 and 𝒳, and f⁻¹, (f')⁻¹ the inverse images along f and along its restriction f' to the lisse-étale sites,

Lg_! ⋙ f⁻¹ ≅ (f')⁻¹ ⋙ L(g')_!

on the unbounded derived categories of abelian sheaves. All four functors are the canonical ones and no hypothesis is made. The isomorphism is the conjugate, under the composites of the derived adjunctions Lg_! ⊣ g⁻¹, L(g')_! ⊣ (g')⁻¹ of Stacks 07AS (1) and f⁻¹ ⊣ Rf_*, (f')⁻¹ ⊣ Rf'_* (exact left adjoints), of the first identity AlgebraicGeometry.Stack.LisseEtale.derivedRestrictionBaseChangeIso.

def derivedLowerShriekBaseChangeIso :
    derivedAbelianLowerShriek.{u, w} B S hS 𝒴 ⋙ derivedAbelianInverseImage B S hS f ≅
      derivedAbelianSubsiteInverseImage B S hS f hf ⋙ derivedAbelianLowerShriek.{u, w} B S hS 𝒳

AlgebraicGeometry.Stack.LisseEtale.moduleDerivedRestrictionBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleModuleDerivedBaseChange.lean, line 331. The attribute's comment: “the module case for the lisse-étale sites, first identity: g⁻¹ ∘ Rf_ = Rf'_ ∘ (g')⁻¹ on the unbounded derived categories of sheaves of modules, as an isomorphism (g')^ ⋙ Rf'_ ≅ Rf_ ⋙ g^ for any total right derived functors Rf_, Rf'_ of the two direct images, with no further hypothesis: the degree-zero square of Stacks 07AT (1) on modules and the fact that restricted K-injective complexes of modules compute Rf'_* (Stacks 0D6J with Stacks 07AK at the 2-fibre products V ×_y 𝒳) are proved, not assumed”.

Stacks 07AV, first identity, for sheaves of modules on the lisse-étale sites: g^* ∘ Rf_* = Rf'_* ∘ (g')^*. For a smooth 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks, total right derived functors Rf_*, Rf'_* of the direct images of sheaves of modules along f and along its restriction f' to the lisse-étale sites, and g^*, (g')^* the restrictions of sheaves of modules to the lisse-étale sites (which are g⁻¹, (g')⁻¹),

(g')^* ⋙ Rf'_* ≅ Rf_* ⋙ g^*

on the unbounded derived categories, with no further hypothesis. It is Stacks.Cohomology.UnboundedComplexes.derivedBaseChangeIsoOfUnit at the degree-zero square AlgebraicGeometry.Stack.LisseEtale.isIso_moduleSquareComparison and at Stacks.SheafOfModules.isIso_derivedPushforwardUnit_inverseImage, fed with AlgebraicGeometry.Stack.LisseEtale.qh_map_bijective_directImageCorep_restriction.

def moduleDerivedRestrictionBaseChangeIso
    (Rf : DerivedCategory (_root_.SheafOfModules.{u + 1} (ambientRingStructureSheaf B S hS 𝒳)) ⥤
      DerivedCategory (_root_.SheafOfModules.{u + 1} (ambientRingStructureSheaf B S hS 𝒴)))
    (Rf' : DerivedCategory (_root_.SheafOfModules.{u + 1} (subsiteRingStructureSheaf B S hS 𝒳)) ⥤
      DerivedCategory (_root_.SheafOfModules.{u + 1} (subsiteRingStructureSheaf B S hS 𝒴)))
    (αf : (modulePushforward B S hS f).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rf)
    (αf' : (moduleSubsitePushforward B S hS f hf).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rf')
    [hRf : Rf.IsRightDerivedFunctor αf (HomotopyCategory.quasiIso
      (_root_.SheafOfModules.{u + 1} (ambientRingStructureSheaf B S hS 𝒳)) (ComplexShape.up ℤ))]
    [hRf' : Rf'.IsRightDerivedFunctor αf' (HomotopyCategory.quasiIso
      (_root_.SheafOfModules.{u + 1} (subsiteRingStructureSheaf B S hS 𝒳)) (ComplexShape.up ℤ))] :
    (moduleInverseImage B S hS 𝒳).mapDerivedCategory ⋙ Rf' ≅
      Rf ⋙ (moduleInverseImage B S hS 𝒴).mapDerivedCategory

AlgebraicGeometry.Stack.LisseEtale.moduleDerivedLowerShriekBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LisseEtaleModuleDerivedBaseChange.lean, line 513. The attribute's comment: “the module case for the lisse-étale sites, second identity: L(g')_! ∘ (f')⁻¹ = f⁻¹ ∘ Lg_! on the unbounded derived categories of sheaves of modules, as an isomorphism Lg_! ⋙ f⁻¹ ≅ (f')⁻¹ ⋙ L(g')_! for the actual derived lower shrieks and the exact inverse images, with no hypothesis: the adjunctions Lg_! ⊣ g⁻¹, f⁻¹ ⊣ Rf_* and their primed versions are constructed, and the first identity is proved”.

Stacks 07AV, the module case for the lisse-étale sites, second identity. Let f : 𝒳 ⟶ 𝒴 be a smooth 1-morphism of algebraic stacks, f' its restriction to the lisse-étale sites, and Lg_!, L(g')_! the derived lower shrieks of sheaves of modules along the inclusions of the lisse-étale sites (AlgebraicGeometry.Stack.LisseEtale.derivedModuleLowerShriekSucc). Then

Lg_! ⋙ f^{-1} ≅ (f')^{-1} ⋙ L(g')_!

on the unbounded derived categories of sheaves of modules, that is, L(g')_! ∘ (f')^{-1} = f^{-1} ∘ Lg_!. Here f^{-1}, (f')^{-1} are the exact inverse images (Stacks 06WE, and restriction along f'), left adjoint to the canonical total right derived direct images Rf_*, Rf'_* (derivedAdjunctionOfExactLeftAdjoint on AlgebraicGeometry.Stack.LisseEtale.modulePullbackPushforwardAdjunction and AlgebraicGeometry.Stack.LisseEtale.moduleSubsiteInverseImageAdjunction), and the isomorphism is the conjugate, across the composed adjunctions, of the first identity AlgebraicGeometry.Stack.LisseEtale.moduleDerivedRestrictionBaseChangeIso.

def moduleDerivedLowerShriekBaseChangeIso :
    derivedModuleLowerShriekSucc B S hS 𝒴 ⋙ derivedModulePullback B S hS f ≅
      derivedModuleSubsiteInverseImage B S hS f hf ⋙ derivedModuleLowerShriekSucc B S hS 𝒳

AlgebraicGeometry.Stack.FlatFppf.nonempty_moduleInverseImage_comp_derivedPushforward_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteDerivedModuleBaseChange.lean, line 471. The attribute's comment: “the module case for the flat-fppf site, first identity: g⁻¹ ∘ Rf_* ≅ Rf'_* ∘ (g')⁻¹ on the unbounded derived categories of sheaves of modules, where g, g' are the inclusions of the flat-fppf subsites of 𝒴 and of 𝒳 and f' is the restriction of f given by Stacks 07AT (2). An isomorphism rather than an equality, and asserted through Nonempty: a right derived functor is determined only up to a canonical isomorphism, so Rf_* and Rf'_* are carried as data together with their comparisons αf, αf' from the degreewise direct images and the IsRightDerivedFunctor property. Two hypotheses are granted. hzero is the degree-zero square f'_* ∘ (g')^* ≅ g^* ∘ f_* on sheaves of modules, which is the second assertion of Stacks 07AT (2) read on modules; the general base-change theorem Stacks 0FN3 would give it from a cofinality condition on the comparison functors of the index categories of Section 00XF, which is not available for this square. hKinj is that (g')^* preserves K-injectivity of complexes, which is the conclusion of Stacks 08BJ applied to the module-level adjunction g'_! ⊣ (g')^* of Stacks 0797, i.e. it follows from left exactness of the module g'_! — Stacks 0789 (2) with Stacks 07AS (4) — which this development has only conditionally. The abelian-sheaf case of the tag is not proved here.”.

Stacks 07AV for sheaves of modules on the flat-fppf site, first identity. Let f : 𝒳 ⟶ 𝒴 be a flat 1-morphism of algebraic stacks, let g and g' be the inclusions of the flat-fppf subsites of 𝒴 and of 𝒳, and let f' be the restriction of f to those subsites, Stacks 07AT (2). Suppose the degree-zero square f'_* ∘ (g')^* ≅ g^* ∘ f_* of sheaves of modules holds, and that (g')^* carries K-injective complexes to K-injective complexes. Then

Rf'_* ∘ (g')^* ≅ g^* ∘ Rf_*

on the unbounded derived categories of sheaves of modules.

theorem nonempty_moduleInverseImage_comp_derivedPushforward_iso
    (hzero : moduleInverseImage B S hS 𝒳 ⋙ restrictedModulePushforward B S hS f hf ≅
      modulePushforward B S hS f ⋙ moduleInverseImage B S hS 𝒴)
    (hKinj : ∀ I : CochainComplex
        (_root_.SheafOfModules.{u + 1} (ambientRingStructureSheaf B S hS 𝒳)) ℤ,
      I.IsKInjective → CochainComplex.IsKInjective
        (((moduleInverseImage B S hS 𝒳).mapHomologicalComplex (ComplexShape.up ℤ)).obj I)) :
    Nonempty ((moduleInverseImage B S hS 𝒳).mapDerivedCategory ⋙ Rf' ≅
      Rf ⋙ (moduleInverseImage B S hS 𝒴).mapDerivedCategory)

AlgebraicGeometry.Stack.FlatFppf.nonempty_derivedLowerShriek_comp_moduleInverseImage_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteDerivedModuleBaseChange.lean, line 520. The attribute's comment: “the module case for the flat-fppf site, second identity: L(g')_! ∘ (f')⁻¹ ≅ f⁻¹ ∘ Lg_! on the unbounded derived categories of sheaves of modules, where g, g' are the inclusions of the flat-fppf subsites of 𝒴 and of 𝒳 and f' is the restriction of f given by Stacks 07AT (2). An isomorphism rather than an equality, and asserted through Nonempty: it is the conjugate of the first identity, whose right-hand sides are right derived functors and so determined only up to a canonical isomorphism, with Rf_*, Rf'_* and their comparisons αf, αf' carried as data. The hypotheses granted are those of the first identity — hzero, the degree-zero square f'_* ∘ (g')^* ≅ g^* ∘ f_* of Stacks 07AT (2) read on modules, and hKinj, preservation of K-injectivity by (g')^*, which is Stacks 08BJ for the module-level adjunction g'_! ⊣ (g')^* of Stacks 0797 and so follows from left exactness of the module g'_!, Stacks 0789 (2) with Stacks 07AS (4) — together with the four derived adjunctions, which also carry the derived functors they name as data: adjg and adjg', Lg_! ⊣ g^* and L(g')_! ⊣ (g')^*, the derived form of Stacks 0789 (2) and Stacks 07AS (4), and adjf and adjf', f⁻¹ ⊣ Rf_* and (f')⁻¹ ⊣ Rf'_*. The abelian-sheaf case of the tag is not proved here.”.

Stacks 07AV for sheaves of modules on the flat-fppf site, second identity. In the situation of AlgebraicGeometry.Stack.FlatFppf.nonempty_moduleInverseImage_comp_derivedPushforward_iso, suppose moreover that f^* and (f')^* are left adjoint to Rf_* and Rf'_* and that Lg_! and L(g')_! are left adjoint to g^* and (g')^* on the derived categories. Then

f^* ∘ Lg_! ≅ L(g')_! ∘ (f')^*

on the unbounded derived categories of sheaves of modules.

theorem nonempty_derivedLowerShriek_comp_moduleInverseImage_iso
    (adjf : fStar ⊣ Rf) (adjf' : f'Star ⊣ Rf')
    (adjg : Lg ⊣ (moduleInverseImage B S hS 𝒴).mapDerivedCategory)
    (adjg' : Lg' ⊣ (moduleInverseImage B S hS 𝒳).mapDerivedCategory)
    (hzero : moduleInverseImage B S hS 𝒳 ⋙ restrictedModulePushforward B S hS f hf ≅
      modulePushforward B S hS f ⋙ moduleInverseImage B S hS 𝒴)
    (hKinj : ∀ I : CochainComplex
        (_root_.SheafOfModules.{u + 1} (ambientRingStructureSheaf B S hS 𝒳)) ℤ,
      I.IsKInjective → CochainComplex.IsKInjective
        (((moduleInverseImage B S hS 𝒳).mapHomologicalComplex (ComplexShape.up ℤ)).obj I)) :
    Nonempty (Lg ⋙ fStar ≅ f'Star ⋙ Lg')

AlgebraicGeometry.Stack.LisseEtale.nonempty_moduleInverseImage_comp_derivedPushforward_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteDerivedModuleBaseChange.lean, line 652. The attribute's comment: “the module case for the lisse-étale site, first identity: g⁻¹ ∘ Rf_* ≅ Rf'_* ∘ (g')⁻¹ on the unbounded derived categories of sheaves of modules, where g, g' are the inclusions of the lisse-étale subsites of 𝒴 and of 𝒳 and f' is the restriction of f given by Stacks 07AT (1). An isomorphism rather than an equality, and asserted through Nonempty: a right derived functor is determined only up to a canonical isomorphism, so Rf_* and Rf'_* are carried as data together with their comparisons αf, αf' from the degreewise direct images and the IsRightDerivedFunctor property. Two hypotheses are granted. hzero is the degree-zero square f'_* ∘ (g')^* ≅ g^* ∘ f_* on sheaves of modules, which is the second assertion of Stacks 07AT (1) read on modules; the general base-change theorem Stacks 0FN3 would give it from a cofinality condition on the comparison functors of the index categories of Section 00XF, which is not available for this square. hKinj is that (g')^* preserves K-injectivity of complexes, which is the conclusion of Stacks 08BJ applied to the module-level adjunction g'_! ⊣ (g')^* of Stacks 0797, i.e. it follows from left exactness of the module g'_! — Stacks 0789 (1) with Stacks 07AS (2) — which this development has only conditionally. The abelian-sheaf case of the tag is not proved here.”.

Stacks 07AV for sheaves of modules on the lisse-étale site, first identity. Let f : 𝒳 ⟶ 𝒴 be a smooth 1-morphism of algebraic stacks, let g and g' be the inclusions of the lisse-étale subsites of 𝒴 and of 𝒳, and let f' be the restriction of f to those subsites, Stacks 07AT (1). Suppose the degree-zero square f'_* ∘ (g')^* ≅ g^* ∘ f_* of sheaves of modules holds, and that (g')^* carries K-injective complexes to K-injective complexes. Then

Rf'_* ∘ (g')^* ≅ g^* ∘ Rf_*

on the unbounded derived categories of sheaves of modules.

theorem nonempty_moduleInverseImage_comp_derivedPushforward_iso
    (hzero : moduleInverseImage B S hS 𝒳 ⋙ restrictedModulePushforward B S hS f hf ≅
      modulePushforward B S hS f ⋙ moduleInverseImage B S hS 𝒴)
    (hKinj : ∀ I : CochainComplex
        (_root_.SheafOfModules.{u + 1} (ambientRingStructureSheaf B S hS 𝒳)) ℤ,
      I.IsKInjective → CochainComplex.IsKInjective
        (((moduleInverseImage B S hS 𝒳).mapHomologicalComplex (ComplexShape.up ℤ)).obj I)) :
    Nonempty ((moduleInverseImage B S hS 𝒳).mapDerivedCategory ⋙ Rf' ≅
      Rf ⋙ (moduleInverseImage B S hS 𝒴).mapDerivedCategory)

AlgebraicGeometry.Stack.LisseEtale.nonempty_derivedLowerShriek_comp_moduleInverseImage_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteDerivedModuleBaseChange.lean, line 702. The attribute's comment: “the module case for the lisse-étale site, second identity: L(g')_! ∘ (f')⁻¹ ≅ f⁻¹ ∘ Lg_! on the unbounded derived categories of sheaves of modules, where g, g' are the inclusions of the lisse-étale subsites of 𝒴 and of 𝒳 and f' is the restriction of f given by Stacks 07AT (1). An isomorphism rather than an equality, and asserted through Nonempty: it is the conjugate of the first identity, whose right-hand sides are right derived functors and so determined only up to a canonical isomorphism, with Rf_*, Rf'_* and their comparisons αf, αf' carried as data. The hypotheses granted are those of the first identity — hzero, the degree-zero square f'_* ∘ (g')^* ≅ g^* ∘ f_* of Stacks 07AT (1) read on modules, and hKinj, preservation of K-injectivity by (g')^*, which is Stacks 08BJ for the module-level adjunction g'_! ⊣ (g')^* of Stacks 0797 and so follows from left exactness of the module g'_!, Stacks 0789 (1) with Stacks 07AS (2) — together with the four derived adjunctions, which also carry the derived functors they name as data: adjg and adjg', Lg_! ⊣ g^* and L(g')_! ⊣ (g')^*, the derived form of Stacks 0789 (1) and Stacks 07AS (2), and adjf and adjf', f⁻¹ ⊣ Rf_* and (f')⁻¹ ⊣ Rf'_*. The abelian-sheaf case of the tag is not proved here.”.

Stacks 07AV for sheaves of modules on the lisse-étale site, second identity. In the situation of AlgebraicGeometry.Stack.LisseEtale.nonempty_moduleInverseImage_comp_derivedPushforward_iso, suppose moreover that f^* and (f')^* are left adjoint to Rf_* and Rf'_* and that Lg_! and L(g')_! are left adjoint to g^* and (g')^* on the derived categories. Then

f^* ∘ Lg_! ≅ L(g')_! ∘ (f')^*

on the unbounded derived categories of sheaves of modules.

theorem nonempty_derivedLowerShriek_comp_moduleInverseImage_iso
    (adjf : fStar ⊣ Rf) (adjf' : f'Star ⊣ Rf')
    (adjg : Lg ⊣ (moduleInverseImage B S hS 𝒴).mapDerivedCategory)
    (adjg' : Lg' ⊣ (moduleInverseImage B S hS 𝒳).mapDerivedCategory)
    (hzero : moduleInverseImage B S hS 𝒳 ⋙ restrictedModulePushforward B S hS f hf ≅
      modulePushforward B S hS f ⋙ moduleInverseImage B S hS 𝒴)
    (hKinj : ∀ I : CochainComplex
        (_root_.SheafOfModules.{u + 1} (ambientRingStructureSheaf B S hS 𝒳)) ℤ,
      I.IsKInjective → CochainComplex.IsKInjective
        (((moduleInverseImage B S hS 𝒳).mapHomologicalComplex (ComplexShape.up ℤ)).obj I)) :
    Nonempty (Lg ⋙ fStar ≅ f'Star ⋙ Lg')

AlgebraicGeometry.Stack.LisseEtale.derivedPushforwardRestrictionIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteDerivedPushforwardBaseChange.lean, line 436. The attribute's comment: “the lisse-étale case for abelian sheaves, first identity: Rf'_ ∘ (g')⁻¹ ≅ g⁻¹ ∘ Rf_ on the unbounded derived categories. An isomorphism rather than an equality, a right derived functor being determined only up to a canonical isomorphism; the two total right derived direct images, their comparisons from the degreewise direct images and the two IsRightDerivedFunctor properties are carried as data, as in Stacks 0FN6 and 0FN7. Granted: that restriction to the lisse-étale site carries K-injective cochain complexes to K-injective ones, which is Stacks 08BJ from exactness of g_! = Stacks 07AS (3); and the degree-zero identification f_ ∘ g⁻¹ ≅ (g')⁻¹ ∘ f'_ of Stacks 07AT (1). The module case is not proved here.”.

Stacks 07AV, the lisse-étale case for abelian sheaves: g⁻¹ ∘ Rf_* = Rf'_* ∘ (g')⁻¹. Let f : 𝒳 ⟶ 𝒴 be a smooth 1-morphism of algebraic stacks, let g⁻¹ and (g')⁻¹ be restriction of abelian sheaves to the lisse-étale sites of 𝒴 and of 𝒳, and let f_* and f'_* be the direct images along f and along its restriction f' to the lisse-étale sites. Suppose (g')⁻¹ carries K-injective cochain complexes to K-injective ones, and that the degree-zero identification f_* ∘ g⁻¹ ≅ (g')⁻¹ ∘ f'_* of Stacks 07AT (1) holds. Then, on the unbounded derived categories,

Rf'_* ∘ (g')⁻¹ ≅ g⁻¹ ∘ Rf_*.

Both restrictions are exact, so they act degreewise on derived categories, and the abelian sheaves on the two sites of 𝒳 are Grothendieck abelian, so both sides are right derived functors of one and the same functor out of the homotopy category; the isomorphism is the comparison that the universal property produces. This is Stacks.Cohomology.UnboundedComplexes.derivedBaseChangeIso at this square of sites.

theorem derivedPushforwardRestrictionIso :
    letI : (SubsitePushforward.subsiteFunctor f.hom.hom.toFunctor
        (smoothObject.{u, w} B S hS 𝒳)
        (smoothObject_map.{u, w} B S hS f hf)).IsContinuous
          (inclusionTopology.{u, w} B S hS 𝒳) (inclusionTopology.{u, w} B S hS 𝒴) :=
      isContinuous_subsiteFunctor.{u, w} B S hS f hf
    letI : (SubsitePushforward.subsiteFunctor f.hom.hom.toFunctor
        (smoothObject.{u, w} B S hS 𝒳)
        (smoothObject_map.{u, w} B S hS f hf)).IsCocontinuous
          (inclusionTopology.{u, w} B S hS 𝒳) (inclusionTopology.{u, w} B S hS 𝒴) :=
      isCocontinuous_subsiteFunctor.{u, w} B S hS f hf
    letI : f.hom.hom.toFunctor.IsContinuous
        (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
        (associatedTopology B S hS 𝒴.val.val.p (etaleTopology B)) :=
      (isContinuous_and_isCocontinuous_homFunctor_associatedTopology B S hS f
        (etaleTopology B)).1
    letI : f.hom.hom.toFunctor.IsCocontinuous
        (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
        (associatedTopology B S hS 𝒴.val.val.p (etaleTopology B)) :=
      (isContinuous_and_isCocontinuous_homFunctor_associatedTopology B S hS f
        (etaleTopology B)).2
    letI : (f.hom.hom.toFunctor.sheafPushforwardCocontinuous AddCommGrpCat.{u + 1}
        (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
        (associatedTopology B S hS 𝒴.val.val.p (etaleTopology B))).Additive :=
      Functor.sheafPushforwardCocontinuous_additive.{u + 1, u + 1, u, u, u + 1} _ _ _
    letI : ((SubsitePushforward.subsiteFunctor f.hom.hom.toFunctor
          (smoothObject.{u, w} B S hS 𝒳)
          (smoothObject_map.{u, w} B S hS f hf)).sheafPushforwardCocontinuous
        AddCommGrpCat.{u + 1} (inclusionTopology.{u, w} B S hS 𝒳)
        (inclusionTopology.{u, w} B S hS 𝒴)).Additive :=
      Functor.sheafPushforwardCocontinuous_additive.{u + 1, u + 1, u, u, u + 1} _ _ _
    ∀ (_hKinj : ∀ I : CochainComplex (Sheaf
            (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
            AddCommGrpCat.{u + 1}) ℤ, I.IsKInjective →
          CochainComplex.IsKInjective
            (((subsiteRestriction B S hS 𝒳.val.val.p (etaleTopology B)
              (smoothObject.{u, w} B S hS 𝒳)).mapHomologicalComplex
                (ComplexShape.up ℤ)).obj I))
      (_hzero : f.hom.hom.toFunctor.sheafPushforwardCocontinuous AddCommGrpCat.{u + 1}
              (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
              (associatedTopology B S hS 𝒴.val.val.p (etaleTopology B)) ⋙
            subsiteRestriction B S hS 𝒴.val.val.p (etaleTopology B)
              (smoothObject.{u, w} B S hS 𝒴) ≅
          subsiteRestriction B S hS 𝒳.val.val.p (etaleTopology B)
              (smoothObject.{u, w} B S hS 𝒳) ⋙
            (SubsitePushforward.subsiteFunctor f.hom.hom.toFunctor
                (smoothObject.{u, w} B S hS 𝒳)
                (smoothObject_map.{u, w} B S hS f hf)).sheafPushforwardCocontinuous
              AddCommGrpCat.{u + 1} (inclusionTopology.{u, w} B S hS 𝒳)
              (inclusionTopology.{u, w} B S hS 𝒴))
      (Rf : DerivedCategory (Sheaf
            (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
            AddCommGrpCat.{u + 1}) ⥤
          DerivedCategory (Sheaf (associatedTopology B S hS 𝒴.val.val.p (etaleTopology B))
            AddCommGrpCat.{u + 1}))
      (Rf' : DerivedCategory (Sheaf (inclusionTopology.{u, w} B S hS 𝒳)
            AddCommGrpCat.{u + 1}) ⥤
          DerivedCategory (Sheaf (inclusionTopology.{u, w} B S hS 𝒴) AddCommGrpCat.{u + 1}))
      (αf : (f.hom.hom.toFunctor.sheafPushforwardCocontinuous AddCommGrpCat.{u + 1}
              (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
              (associatedTopology B S hS 𝒴.val.val.p (etaleTopology B))).mapHomotopyCategory
            (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rf)
      (αf' : ((SubsitePushforward.subsiteFunctor f.hom.hom.toFunctor
                (smoothObject.{u, w} B S hS 𝒳)
                (smoothObject_map.{u, w} B S hS f hf)).sheafPushforwardCocontinuous
              AddCommGrpCat.{u + 1} (inclusionTopology.{u, w} B S hS 𝒳)
              (inclusionTopology.{u, w} B S hS 𝒴)).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
            DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rf')
      (_hRf : Rf.IsRightDerivedFunctor αf (HomotopyCategory.quasiIso
          (Sheaf (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
            AddCommGrpCat.{u + 1}) (ComplexShape.up ℤ)))
      (_hRf' : Rf'.IsRightDerivedFunctor αf' (HomotopyCategory.quasiIso
          (Sheaf (inclusionTopology.{u, w} B S hS 𝒳) AddCommGrpCat.{u + 1})
          (ComplexShape.up ℤ))),
      Nonempty ((subsiteRestriction B S hS 𝒳.val.val.p (etaleTopology B)
            (smoothObject.{u, w} B S hS 𝒳)).mapDerivedCategory ⋙ Rf' ≅
          Rf ⋙ (subsiteRestriction B S hS 𝒴.val.val.p (etaleTopology B)
            (smoothObject.{u, w} B S hS 𝒴)).mapDerivedCategory)

AlgebraicGeometry.Stack.LisseEtale.derivedShriekInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteDerivedPushforwardBaseChange.lean, line 549. The attribute's comment: “the lisse-étale case for abelian sheaves, second identity: f⁻¹ ∘ Lg_! ≅ L(g')_! ∘ (f')⁻¹ on the unbounded derived categories, obtained formally from the first identity as its conjugate under the composed adjunctions. An isomorphism rather than an equality, the derived functors being determined only up to canonical isomorphism and carried as data. Granted: the first identity itself, and the four derived adjunctions Lg_! ⊣ g⁻¹ and L(g')_! ⊣ (g')⁻¹ — which are Stacks 07AS (3) — together with f⁻¹ ⊣ Rf_ and (f')⁻¹ ⊣ Rf'_, which are standard. The module case is not proved here.”.

Stacks 07AV, the lisse-étale case for abelian sheaves: L(g')_! ∘ (f')⁻¹ = f⁻¹ ∘ Lg_!. Let Rf_* and Rf'_* be the total right derived direct images along a smooth 1-morphism f : 𝒳 ⟶ 𝒴 and along its restriction f' to the lisse-étale sites, let Lg_! and L(g')_! be the derived lower shrieks of Stacks 07AS (3) over 𝒴 and over 𝒳, left adjoint to the derived restrictions g⁻¹ and (g')⁻¹, and let f⁻¹ and (f')⁻¹ be the derived inverse images, left adjoint to Rf_* and Rf'_*. Then the base change isomorphism σ : Rf'_* ∘ (g')⁻¹ ≅ g⁻¹ ∘ Rf_* of AlgebraicGeometry.Stack.LisseEtale.derivedPushforwardRestrictionIso gives

f⁻¹ ∘ Lg_! ≅ L(g')_! ∘ (f')⁻¹.

This is the source's "the rest of the proof is formal": the two sides are left adjoint to the two sides of σ, by composing the adjunctions, and σ is the conjugate of the asserted isomorphism under CategoryTheory.conjugateIsoEquiv.

def derivedShriekInverseImageIso
    (Rf : DerivedCategory (Sheaf (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
        AddCommGrpCat.{u + 1}) ⥤
      DerivedCategory (Sheaf (associatedTopology B S hS 𝒴.val.val.p (etaleTopology B))
        AddCommGrpCat.{u + 1}))
    (Rf' : DerivedCategory (Sheaf (inclusionTopology.{u, w} B S hS 𝒳) AddCommGrpCat.{u + 1}) ⥤
      DerivedCategory (Sheaf (inclusionTopology.{u, w} B S hS 𝒴) AddCommGrpCat.{u + 1}))
    (Lg : DerivedCategory (Sheaf (inclusionTopology.{u, w} B S hS 𝒴) AddCommGrpCat.{u + 1}) ⥤
      DerivedCategory (Sheaf (associatedTopology B S hS 𝒴.val.val.p (etaleTopology B))
        AddCommGrpCat.{u + 1}))
    (Lg' : DerivedCategory (Sheaf (inclusionTopology.{u, w} B S hS 𝒳) AddCommGrpCat.{u + 1}) ⥤
      DerivedCategory (Sheaf (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
        AddCommGrpCat.{u + 1}))
    (finv : DerivedCategory (Sheaf (associatedTopology B S hS 𝒴.val.val.p (etaleTopology B))
        AddCommGrpCat.{u + 1}) ⥤
      DerivedCategory (Sheaf (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
        AddCommGrpCat.{u + 1}))
    (f'inv : DerivedCategory (Sheaf (inclusionTopology.{u, w} B S hS 𝒴) AddCommGrpCat.{u + 1}) ⥤
      DerivedCategory (Sheaf (inclusionTopology.{u, w} B S hS 𝒳) AddCommGrpCat.{u + 1}))
    (adjg : Lg ⊣ (subsiteRestriction B S hS 𝒴.val.val.p (etaleTopology B)
      (smoothObject.{u, w} B S hS 𝒴)).mapDerivedCategory)
    (adjg' : Lg' ⊣ (subsiteRestriction B S hS 𝒳.val.val.p (etaleTopology B)
      (smoothObject.{u, w} B S hS 𝒳)).mapDerivedCategory)
    (adjf : finv ⊣ Rf) (adjf' : f'inv ⊣ Rf')
    (σ : (subsiteRestriction B S hS 𝒳.val.val.p (etaleTopology B)
          (smoothObject.{u, w} B S hS 𝒳)).mapDerivedCategory ⋙ Rf' ≅
        Rf ⋙ (subsiteRestriction B S hS 𝒴.val.val.p (etaleTopology B)
          (smoothObject.{u, w} B S hS 𝒴)).mapDerivedCategory) :
    Lg ⋙ finv ≅ f'inv ⋙ Lg'

AlgebraicGeometry.Stack.FlatFppf.derivedPushforwardRestrictionIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteDerivedPushforwardBaseChange.lean, line 767. The attribute's comment: “the flat-fppf case for abelian sheaves, first identity: Rf'_ ∘ (g')⁻¹ ≅ g⁻¹ ∘ Rf_ on the unbounded derived categories. An isomorphism rather than an equality, a right derived functor being determined only up to a canonical isomorphism; the two total right derived direct images, their comparisons from the degreewise direct images and the two IsRightDerivedFunctor properties are carried as data, as in Stacks 0FN6 and 0FN7. Granted: that restriction to the flat-fppf site carries K-injective cochain complexes to K-injective ones, which is Stacks 08BJ from exactness of g_! = Stacks 07AS (3); and the degree-zero identification f_ ∘ g⁻¹ ≅ (g')⁻¹ ∘ f'_ of Stacks 07AT (2). The module case is not proved here.”.

Stacks 07AV, the flat-fppf case for abelian sheaves: g⁻¹ ∘ Rf_* = Rf'_* ∘ (g')⁻¹. Let f : 𝒳 ⟶ 𝒴 be a flat 1-morphism of algebraic stacks, let g⁻¹ and (g')⁻¹ be restriction of abelian sheaves to the flat-fppf sites of 𝒴 and of 𝒳, and let f_* and f'_* be the direct images along f and along its restriction f' to the flat-fppf sites. Suppose (g')⁻¹ carries K-injective cochain complexes to K-injective ones, and that the degree-zero identification f_* ∘ g⁻¹ ≅ (g')⁻¹ ∘ f'_* of Stacks 07AT (2) holds. Then, on the unbounded derived categories,

Rf'_* ∘ (g')⁻¹ ≅ g⁻¹ ∘ Rf_*.

Both restrictions are exact, so they act degreewise on derived categories, and the abelian sheaves on the two sites of 𝒳 are Grothendieck abelian, so both sides are right derived functors of one and the same functor out of the homotopy category; the isomorphism is the comparison that the universal property produces. This is Stacks.Cohomology.UnboundedComplexes.derivedBaseChangeIso at this square of sites.

theorem derivedPushforwardRestrictionIso :
    letI : (SubsitePushforward.subsiteFunctor f.hom.hom.toFunctor
        (flatObject B S hS 𝒳.val)
        (flatObject_map B S hS f hf)).IsContinuous
          (inclusionTopology B S hS 𝒳) (inclusionTopology B S hS 𝒴) :=
      isContinuous_subsiteFunctor B S hS f hf
    letI : (SubsitePushforward.subsiteFunctor f.hom.hom.toFunctor
        (flatObject B S hS 𝒳.val)
        (flatObject_map B S hS f hf)).IsCocontinuous
          (inclusionTopology B S hS 𝒳) (inclusionTopology B S hS 𝒴) :=
      isCocontinuous_subsiteFunctor B S hS f hf
    letI : f.hom.hom.toFunctor.IsContinuous
        (associatedTopology B S hS 𝒳.val.val.p B.topology)
        (associatedTopology B S hS 𝒴.val.val.p B.topology) :=
      (isContinuous_and_isCocontinuous_homFunctor B S hS f).1
    letI : f.hom.hom.toFunctor.IsCocontinuous
        (associatedTopology B S hS 𝒳.val.val.p B.topology)
        (associatedTopology B S hS 𝒴.val.val.p B.topology) :=
      (isContinuous_and_isCocontinuous_homFunctor B S hS f).2
    letI : (f.hom.hom.toFunctor.sheafPushforwardCocontinuous AddCommGrpCat.{u + 1}
        (associatedTopology B S hS 𝒳.val.val.p B.topology)
        (associatedTopology B S hS 𝒴.val.val.p B.topology)).Additive :=
      Functor.sheafPushforwardCocontinuous_additive.{u + 1, u + 1, u, u, u + 1} _ _ _
    letI : ((SubsitePushforward.subsiteFunctor f.hom.hom.toFunctor
          (flatObject B S hS 𝒳.val)
          (flatObject_map B S hS f hf)).sheafPushforwardCocontinuous
        AddCommGrpCat.{u + 1} (inclusionTopology B S hS 𝒳)
        (inclusionTopology B S hS 𝒴)).Additive :=
      Functor.sheafPushforwardCocontinuous_additive.{u + 1, u + 1, u, u, u + 1} _ _ _
    ∀ (_hKinj : ∀ I : CochainComplex (Sheaf
            (associatedTopology B S hS 𝒳.val.val.p B.topology)
            AddCommGrpCat.{u + 1}) ℤ, I.IsKInjective →
          CochainComplex.IsKInjective
            (((subsiteRestriction B S hS 𝒳.val.val.p B.topology
              (flatObject B S hS 𝒳.val)).mapHomologicalComplex
                (ComplexShape.up ℤ)).obj I))
      (_hzero : f.hom.hom.toFunctor.sheafPushforwardCocontinuous AddCommGrpCat.{u + 1}
              (associatedTopology B S hS 𝒳.val.val.p B.topology)
              (associatedTopology B S hS 𝒴.val.val.p B.topology) ⋙
            subsiteRestriction B S hS 𝒴.val.val.p B.topology
              (flatObject B S hS 𝒴.val) ≅
          subsiteRestriction B S hS 𝒳.val.val.p B.topology
              (flatObject B S hS 𝒳.val) ⋙
            (SubsitePushforward.subsiteFunctor f.hom.hom.toFunctor
                (flatObject B S hS 𝒳.val)
                (flatObject_map B S hS f hf)).sheafPushforwardCocontinuous
              AddCommGrpCat.{u + 1} (inclusionTopology B S hS 𝒳)
              (inclusionTopology B S hS 𝒴))
      (Rf : DerivedCategory (Sheaf
            (associatedTopology B S hS 𝒳.val.val.p B.topology)
            AddCommGrpCat.{u + 1}) ⥤
          DerivedCategory (Sheaf (associatedTopology B S hS 𝒴.val.val.p B.topology)
            AddCommGrpCat.{u + 1}))
      (Rf' : DerivedCategory (Sheaf (inclusionTopology B S hS 𝒳)
            AddCommGrpCat.{u + 1}) ⥤
          DerivedCategory (Sheaf (inclusionTopology B S hS 𝒴) AddCommGrpCat.{u + 1}))
      (αf : (f.hom.hom.toFunctor.sheafPushforwardCocontinuous AddCommGrpCat.{u + 1}
              (associatedTopology B S hS 𝒳.val.val.p B.topology)
              (associatedTopology B S hS 𝒴.val.val.p B.topology)).mapHomotopyCategory
            (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rf)
      (αf' : ((SubsitePushforward.subsiteFunctor f.hom.hom.toFunctor
                (flatObject B S hS 𝒳.val)
                (flatObject_map B S hS f hf)).sheafPushforwardCocontinuous
              AddCommGrpCat.{u + 1} (inclusionTopology B S hS 𝒳)
              (inclusionTopology B S hS 𝒴)).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
            DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rf')
      (_hRf : Rf.IsRightDerivedFunctor αf (HomotopyCategory.quasiIso
          (Sheaf (associatedTopology B S hS 𝒳.val.val.p B.topology)
            AddCommGrpCat.{u + 1}) (ComplexShape.up ℤ)))
      (_hRf' : Rf'.IsRightDerivedFunctor αf' (HomotopyCategory.quasiIso
          (Sheaf (inclusionTopology B S hS 𝒳) AddCommGrpCat.{u + 1})
          (ComplexShape.up ℤ))),
      Nonempty ((subsiteRestriction B S hS 𝒳.val.val.p B.topology
            (flatObject B S hS 𝒳.val)).mapDerivedCategory ⋙ Rf' ≅
          Rf ⋙ (subsiteRestriction B S hS 𝒴.val.val.p B.topology
            (flatObject B S hS 𝒴.val)).mapDerivedCategory)

AlgebraicGeometry.Stack.FlatFppf.derivedShriekInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteDerivedPushforwardBaseChange.lean, line 877. The attribute's comment: “the flat-fppf case for abelian sheaves, second identity: f⁻¹ ∘ Lg_! ≅ L(g')_! ∘ (f')⁻¹ on the unbounded derived categories, obtained formally from the first identity as its conjugate under the composed adjunctions. An isomorphism rather than an equality, the derived functors being determined only up to canonical isomorphism and carried as data. Granted: the first identity itself, and the four derived adjunctions Lg_! ⊣ g⁻¹ and L(g')_! ⊣ (g')⁻¹ — which are Stacks 07AS (3) — together with f⁻¹ ⊣ Rf_ and (f')⁻¹ ⊣ Rf'_, which are standard. The module case is not proved here.”.

Stacks 07AV, the flat-fppf case for abelian sheaves: L(g')_! ∘ (f')⁻¹ = f⁻¹ ∘ Lg_!. Let Rf_* and Rf'_* be the total right derived direct images along a flat 1-morphism f : 𝒳 ⟶ 𝒴 and along its restriction f' to the flat-fppf sites, let Lg_! and L(g')_! be the derived lower shrieks of Stacks 07AS (3) over 𝒴 and over 𝒳, left adjoint to the derived restrictions g⁻¹ and (g')⁻¹, and let f⁻¹ and (f')⁻¹ be the derived inverse images, left adjoint to Rf_* and Rf'_*. Then the base change isomorphism σ : Rf'_* ∘ (g')⁻¹ ≅ g⁻¹ ∘ Rf_* of AlgebraicGeometry.Stack.FlatFppf.derivedPushforwardRestrictionIso gives

f⁻¹ ∘ Lg_! ≅ L(g')_! ∘ (f')⁻¹.

This is the source's "the rest of the proof is formal": the two sides are left adjoint to the two sides of σ, by composing the adjunctions, and σ is the conjugate of the asserted isomorphism under CategoryTheory.conjugateIsoEquiv.

def derivedShriekInverseImageIso
    (Rf : DerivedCategory (Sheaf (associatedTopology B S hS 𝒳.val.val.p B.topology)
        AddCommGrpCat.{u + 1}) ⥤
      DerivedCategory (Sheaf (associatedTopology B S hS 𝒴.val.val.p B.topology)
        AddCommGrpCat.{u + 1}))
    (Rf' : DerivedCategory (Sheaf (inclusionTopology B S hS 𝒳) AddCommGrpCat.{u + 1}) ⥤
      DerivedCategory (Sheaf (inclusionTopology B S hS 𝒴) AddCommGrpCat.{u + 1}))
    (Lg : DerivedCategory (Sheaf (inclusionTopology B S hS 𝒴) AddCommGrpCat.{u + 1}) ⥤
      DerivedCategory (Sheaf (associatedTopology B S hS 𝒴.val.val.p B.topology)
        AddCommGrpCat.{u + 1}))
    (Lg' : DerivedCategory (Sheaf (inclusionTopology B S hS 𝒳) AddCommGrpCat.{u + 1}) ⥤
      DerivedCategory (Sheaf (associatedTopology B S hS 𝒳.val.val.p B.topology)
        AddCommGrpCat.{u + 1}))
    (finv : DerivedCategory (Sheaf (associatedTopology B S hS 𝒴.val.val.p B.topology)
        AddCommGrpCat.{u + 1}) ⥤
      DerivedCategory (Sheaf (associatedTopology B S hS 𝒳.val.val.p B.topology)
        AddCommGrpCat.{u + 1}))
    (f'inv : DerivedCategory (Sheaf (inclusionTopology B S hS 𝒴) AddCommGrpCat.{u + 1}) ⥤
      DerivedCategory (Sheaf (inclusionTopology B S hS 𝒳) AddCommGrpCat.{u + 1}))
    (adjg : Lg ⊣ (subsiteRestriction B S hS 𝒴.val.val.p B.topology
      (flatObject B S hS 𝒴.val)).mapDerivedCategory)
    (adjg' : Lg' ⊣ (subsiteRestriction B S hS 𝒳.val.val.p B.topology
      (flatObject B S hS 𝒳.val)).mapDerivedCategory)
    (adjf : finv ⊣ Rf) (adjf' : f'inv ⊣ Rf')
    (σ : (subsiteRestriction B S hS 𝒳.val.val.p B.topology
          (flatObject B S hS 𝒳.val)).mapDerivedCategory ⋙ Rf' ≅
        Rf ⋙ (subsiteRestriction B S hS 𝒴.val.val.p B.topology
          (flatObject B S hS 𝒴.val)).mapDerivedCategory) :
    Lg ⋙ finv ≅ f'inv ⋙ Lg'

Tag 07B3, a lemma

Tag 07B3 in the Stacks Project.

AlgebraicGeometry.Stack.FlatFppf.locallyQuasicoherentSheafFlatBaseChange_homology_derivedModuleLowerShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatFppfDerivedModuleLowerShriekSheafFlatBaseChange.lean, line 90. The attribute's comment: “part (2): for a quasi-coherent module H (Stacks 03DL) on the flat-fppf site of an arbitrary algebraic stack and every p, H^p(Lg_! H) is a locally quasi-coherent module with the flat base change property, the class LQCoh^fbc of Stacks 0762 read with the pullback of sheaves, for the actual derived lower shriek Lg_! of Stacks 07AS (4) at the universe of the rings, with no hypothesis”.

Let H be a quasi-coherent module on the flat-fppf site of an algebraic stack 𝒳. For every p, the cohomology sheaf H^p(Lg_! H) of the derived lower shriek of Stacks 07AS (4) is a locally quasi-coherent module with the flat base change property on 𝒳, the flat base change property of Stacks 0762 being read with the pullback of sheaves.

theorem locallyQuasicoherentSheafFlatBaseChange_homology_derivedModuleLowerShriek
    (H : flatFppfModules B S hS 𝒳) (hH : H.IsQuasicoherentOnSite) (p : ℤ) :
    letI := (SheafOfModules.instAbelian _ : Abelian (fppfModules B S hS 𝒳))
    letI := abelianFlatFppfModulesSpelling B S hS 𝒳
    letI := HasDerivedCategory.standard (flatFppfModules B S hS 𝒳)
    letI := HasDerivedCategory.standard (fppfModules B S hS 𝒳)
    lqcohSheafFbcFppfModules.{u, _, u} B E h S hS 𝒳
      ((DerivedCategory.homologyFunctor _ p).obj
        ((derivedModuleLowerShriek B S hS 𝒳).obj ((DerivedCategory.singleFunctor _ 0).obj H)))

AlgebraicGeometry.Stack.LisseEtale.isLocallyQuasicoherentWithSheafFlatBaseChange_homology_derivedModuleLowerShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LisseEtaleDerivedModuleLowerShriekSheafFlatBaseChange.lean, line 56. The attribute's comment: “part (1): for a quasi-coherent module H (Stacks 03DL) on the lisse-étale site of an arbitrary algebraic stack and every p, H^p(Lg_! H) is a locally quasi-coherent module with the flat base change property, the class LQCoh^fbc of Stacks 0762 read with the pullback of sheaves, for the actual derived lower shriek Lg_! of Stacks 07AS (2) at the universe of the rings, with no hypothesis”.

Let H be a quasi-coherent module on the lisse-étale site of an algebraic stack 𝒳. For every p, the cohomology sheaf H^p(Lg_! H) of the derived lower shriek Lg_! is a locally quasi-coherent module with the flat base change property on 𝒳, the flat base change property being read with the pullback of sheaves.

theorem isLocallyQuasicoherentWithSheafFlatBaseChange_homology_derivedModuleLowerShriek
    (H : SheafOfModules.{u} (lisseEtaleModuleRing B S hS 𝒳)) (hH : H.IsQuasicoherentOnSite)
    (p : ℤ) :
    letI := abelianEtaleModules B S hS 𝒳
    letI := abelianLisseEtaleModules B S hS 𝒳
    letI := HasDerivedCategory.standard (SheafOfModules.{u} (lisseEtaleModuleRing B S hS 𝒳))
    letI := HasDerivedCategory.standard (SheafOfModules.{u}
      (SmallModel.targetRing (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
        (associatedRingedTopos B S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids (etaleTopology B)
          (etaleTopology_le_topology B)).O))
    IsLocallyQuasicoherentWithSheafFlatBaseChange.{u, u + 1, u, u} B E h S hS
      𝒳.val.val.p 𝒳.val.isFiberedInGroupoids
      ((DerivedCategory.homologyFunctor _ p).obj
        ((derivedModuleLowerShriek B S hS 𝒳).obj
          ((DerivedCategory.singleFunctor _ 0).obj H))).val

AlgebraicGeometry.Stack.LisseEtale.isLocallyQuasicoherent_homology_derivedModuleLowerShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteDerivedModuleQuasicoherence.lean, line 170. The attribute's comment: “part (1), the local quasi-coherence half: for a quasi-coherent module H on the lisse-étale site of an algebraic stack 𝒳 and every p, the sheaf H^p(Lg_! H) is locally quasi-coherent (Stacks 06WJ) on 𝒳, read at section universe u + 1. Three hypotheses are carried. Lg is the functor Lg_! itself, carried as data because this library constructs no unbounded total left derived functor of the module-level g_! of Stacks 0789 (1); it stands for Stacks 07AS (2) and (4) on sheaves of modules, and is carried in the same shape as in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteDerivedModuleBaseChange.lean. hserre is Stacks 0771 part (2), the half saying that LQCoh^fbc is a weak Serre subcategory of Mod(𝒳_étale, 𝒪_𝒳); only part (3) of Stacks 0771 is proved here. hK and e say that Lg_! H is represented by a complex whose TERMS are quasi-coherent (Stacks 03DL), which is the computation of Lg_! H from a free resolution that the source performs before citing Stacks 0771, and hqc is Stacks 06WK, that a quasi-coherent module lies in LQCoh^fbc, which this library does not have in any form; the reduction of the general case to the affine case with a global presentation, by Stacks 07AQ and Stacks 07AV, is not carried out. The quasi-coherence hypothesis on H is the source's and is unweakened”.

Stacks 07B3 part (1), local quasi-coherence: for a quasi-coherent module H on the lisse-étale site of 𝒳, every cohomology sheaf of Lg_! H is locally quasi-coherent.

theorem isLocallyQuasicoherent_homology_derivedModuleLowerShriek
    (hH : H.IsQuasicoherentOnSite)
    (hserre : StackEtaleModuleRule.IsWeakSerre.{u, w} B S hS
      (locallyQuasicoherentFlatBaseChangeRule B E h S hS))
    (hqc : ∀ F : _root_.SheafOfModules.{u + 1} (ambientRingStructureSheaf B S hS 𝒳),
      F.IsQuasicoherentOnSite → locallyQuasicoherentFlatBaseChangeRule B E h S hS 𝒳.val.val.p
        𝒳.val.isFiberedInGroupoids F.val)
    (hK : ∀ m : ℤ, (K.X m).IsQuasicoherentOnSite)
    (e : Lg.obj ((DerivedCategory.singleFunctor _ 0).obj H) ≅ DerivedCategory.Q.obj K)
    (p : ℤ) :
    IsLocallyQuasicoherent B E h S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids
      ((DerivedCategory.homologyFunctor _ p).obj
        (Lg.obj ((DerivedCategory.singleFunctor _ 0).obj H))).val

AlgebraicGeometry.Stack.LisseEtale.hasFlatBaseChange_homology_derivedModuleLowerShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteDerivedModuleQuasicoherence.lean, line 201. The attribute's comment: “part (1), the flat base change half: for a quasi-coherent module H on the lisse-étale site of an algebraic stack 𝒳 and every p, the sheaf H^p(Lg_! H) has the flat base change property (Stacks 0762) on 𝒳, read at section universe u + 1 through HasFlatBaseChangePropertyUnivLE, the comparison map of Stacks 06WC pinning the other spelling to Type u. The same three hypotheses are carried as for the local quasi-coherence half. Lg is Lg_! carried as data, standing for Stacks 07AS (2) and (4) on sheaves of modules, no unbounded total left derived functor of the module-level g_! of Stacks 0789 (1) being constructed here. hserre is Stacks 0771 part (2) for Mod(𝒳_étale, 𝒪_𝒳); only part (3) of Stacks 0771 is proved here. hK and e say that Lg_! H is represented by a complex whose TERMS lie in LQCoh^fbc, the source's computation of Lg_! H from a free resolution; the reduction of the general case to the affine case with a global presentation, by Stacks 07AQ and Stacks 07AV, is not carried out. The quasi-coherence hypothesis on H is the source's and is unweakened”.

Stacks 07B3 part (1), the flat base change property: for a quasi-coherent module H on the lisse-étale site of 𝒳, every cohomology sheaf of Lg_! H has the flat base change property.

theorem hasFlatBaseChange_homology_derivedModuleLowerShriek
    (hH : H.IsQuasicoherentOnSite)
    (hserre : StackEtaleModuleRule.IsWeakSerre.{u, w} B S hS
      (locallyQuasicoherentFlatBaseChangeRule B E h S hS))
    (hqc : ∀ F : _root_.SheafOfModules.{u + 1} (ambientRingStructureSheaf B S hS 𝒳),
      F.IsQuasicoherentOnSite → locallyQuasicoherentFlatBaseChangeRule B E h S hS 𝒳.val.val.p
        𝒳.val.isFiberedInGroupoids F.val)
    (hK : ∀ m : ℤ, (K.X m).IsQuasicoherentOnSite)
    (e : Lg.obj ((DerivedCategory.singleFunctor _ 0).obj H) ≅ DerivedCategory.Q.obj K)
    (p : ℤ) :
    HasFlatBaseChangePropertyUnivLE B E h S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids
      (etaleTopology B) (etaleTopology_le_topology B)
      ((DerivedCategory.homologyFunctor _ p).obj
        (Lg.obj ((DerivedCategory.singleFunctor _ 0).obj H))).val

AlgebraicGeometry.Stack.FlatFppf.isLocallyQuasicoherent_homology_derivedModuleLowerShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteDerivedModuleQuasicoherence.lean, line 278. The attribute's comment: “part (2), the local quasi-coherence half: for a quasi-coherent module H on the flat-fppf site of an algebraic stack 𝒳 and every p, the sheaf H^p(Lg_! H) is locally quasi-coherent (Stacks 06WJ) on 𝒳, read at section universe u + 1. Three hypotheses are carried. Lg is the functor Lg_! itself, carried as data because this library constructs no unbounded total left derived functor of the module-level g_! of Stacks 0789 (2); it stands for Stacks 07AS (2) and (4) on sheaves of modules, and is carried in the same shape as in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteDerivedModuleBaseChange.lean. hserre is Stacks 0771 part (2), the half saying that LQCoh^fbc is a weak Serre subcategory of Mod(𝒪_𝒳), written out on the fppf site; only part (3) of Stacks 0771 is proved here. hK and e say that Lg_! H is represented by a complex whose TERMS lie in LQCoh^fbc, which is the computation of Lg_! H from a free resolution that the source performs before citing Stacks 0771; the reduction of the general case to the affine case with a global presentation, by Stacks 07AQ and Stacks 07AV, is not carried out. The quasi-coherence hypothesis on H is the source's and is unweakened”.

Stacks 07B3 part (2), local quasi-coherence: for a quasi-coherent module H on the flat-fppf site of 𝒳, every cohomology sheaf of Lg_! H is locally quasi-coherent.

theorem isLocallyQuasicoherent_homology_derivedModuleLowerShriek
    (hH : H.IsQuasicoherentOnSite)
    (hserre : ObjectProperty.IsWeakSerreClass
      (C := _root_.SheafOfModules.{u + 1} (ambientRingStructureSheaf B S hS 𝒳))
      (fun F => locallyQuasicoherentFlatBaseChangeRule B E h S hS 𝒳.val.val.p
        𝒳.val.isFiberedInGroupoids F.val))
    (hqc : ∀ F : _root_.SheafOfModules.{u + 1} (ambientRingStructureSheaf B S hS 𝒳),
      F.IsQuasicoherentOnSite → locallyQuasicoherentFlatBaseChangeRule B E h S hS 𝒳.val.val.p
        𝒳.val.isFiberedInGroupoids F.val)
    (hK : ∀ m : ℤ, (K.X m).IsQuasicoherentOnSite)
    (e : Lg.obj ((DerivedCategory.singleFunctor _ 0).obj H) ≅ DerivedCategory.Q.obj K)
    (p : ℤ) :
    IsLocallyQuasicoherent B E h S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids
      ((DerivedCategory.homologyFunctor _ p).obj
        (Lg.obj ((DerivedCategory.singleFunctor _ 0).obj H))).val

AlgebraicGeometry.Stack.FlatFppf.hasFlatBaseChange_homology_derivedModuleLowerShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteDerivedModuleQuasicoherence.lean, line 314. The attribute's comment: “part (2), the flat base change half: for a quasi-coherent module H on the flat-fppf site of an algebraic stack 𝒳 and every p, the sheaf H^p(Lg_! H) has the flat base change property (Stacks 0762) on 𝒳, read at section universe u + 1 through HasFlatBaseChangePropertyUnivLE, the comparison map of Stacks 06WC pinning the other spelling to Type u. The same three hypotheses are carried as for the local quasi-coherence half. Lg is Lg_! carried as data, standing for Stacks 07AS (2) and (4) on sheaves of modules, no unbounded total left derived functor of the module-level g_! of Stacks 0789 (2) being constructed here. hserre is Stacks 0771 part (2) for Mod(𝒪_𝒳), written out on the fppf site; only part (3) of Stacks 0771 is proved here. hK and e say that Lg_! H is represented by a complex whose TERMS are quasi-coherent (Stacks 03DL), the source's computation of Lg_! H from a free resolution, and hqc is Stacks 06WK, that a quasi-coherent module lies in LQCoh^fbc, which this library does not have in any form; the reduction of the general case to the affine case with a global presentation, by Stacks 07AQ and Stacks 07AV, is not carried out. The quasi-coherence hypothesis on H is the source's and is unweakened”.

Stacks 07B3 part (2), the flat base change property: for a quasi-coherent module H on the flat-fppf site of 𝒳, every cohomology sheaf of Lg_! H has the flat base change property.

theorem hasFlatBaseChange_homology_derivedModuleLowerShriek
    (hH : H.IsQuasicoherentOnSite)
    (hserre : ObjectProperty.IsWeakSerreClass
      (C := _root_.SheafOfModules.{u + 1} (ambientRingStructureSheaf B S hS 𝒳))
      (fun F => locallyQuasicoherentFlatBaseChangeRule B E h S hS 𝒳.val.val.p
        𝒳.val.isFiberedInGroupoids F.val))
    (hqc : ∀ F : _root_.SheafOfModules.{u + 1} (ambientRingStructureSheaf B S hS 𝒳),
      F.IsQuasicoherentOnSite → locallyQuasicoherentFlatBaseChangeRule B E h S hS 𝒳.val.val.p
        𝒳.val.isFiberedInGroupoids F.val)
    (hK : ∀ m : ℤ, (K.X m).IsQuasicoherentOnSite)
    (e : Lg.obj ((DerivedCategory.singleFunctor _ 0).obj H) ≅ DerivedCategory.Q.obj K)
    (p : ℤ) :
    HasFlatBaseChangePropertyUnivLE B E h S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids
      (etaleTopology B) (etaleTopology_le_topology B)
      ((DerivedCategory.homologyFunctor _ p).obj
        (Lg.obj ((DerivedCategory.singleFunctor _ 0).obj H))).val

Sources

• Section 104.3, Tag 08MZ
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.FlatFppf.hasLeftDerivedFunctor_abelianLowerShriek · AlgebraicGeometry.Stack.FlatFppf.derivedAbelianLowerShriekAdjunction · AlgebraicGeometry.Stack.FlatFppf.derivedAbelianLowerShriekRestrictionIso · AlgebraicGeometry.Stack.FlatFppf.abelianLowerShriek_hasLeftDerivedFunctor · AlgebraicGeometry.Stack.FlatFppf.derivedAbelianLowerShriekFunctorAdjunction · AlgebraicGeometry.Stack.FlatFppf.derivedAbelianLowerShriekFunctorRestrictionIso · AlgebraicGeometry.Stack.LisseEtale.abelianLowerShriek_hasLeftDerivedFunctor · AlgebraicGeometry.Stack.LisseEtale.derivedAbelianLowerShriekAdjunction

Section104.4 Cohomology and the lisse-étale and flat-fppf sites#

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

Tag 0H0Z, a lemma

Tag 0H0Z in the Stacks Project.

AlgebraicGeometry.Stack.FlatFppf.isIso_derivedAbelianLowerShriekAdjunction_counit_constantSheaf_of_isTerminal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfTerminalConstantSheaf.lean, line 50. The attribute's comment: “for the Lg_! of 07AS part (3), the flat-fppf site of an algebraic stack whose flat-fppf site has a terminal object whose image is terminal in the fppf site”.

For an algebraic stack 𝒳 whose flat-fppf site has a terminal object e whose image is terminal in the fppf site, the counit of the derived adjunction Lg_! ⊣ g⁻¹ is invertible at the constant sheaf ℤ of 𝒳_{fppf} in degree zero, so the canonical comparison Lg_! ℤ ⟶ ℤ is an isomorphism.

theorem isIso_derivedAbelianLowerShriekAdjunction_counit_constantSheaf_of_isTerminal
    {e : ObjectProperty.FullSubcategory (objectProperty B S hS 𝒳)} (he : IsTerminal e)
    (heX : IsTerminal ((objectProperty B S hS 𝒳).ι.obj e)) :
    IsIso ((derivedAbelianLowerShriekAdjunction B S hS 𝒳
          (abelianLowerShriekAcyclic B S hS 𝒳)).counit.app
        ((DerivedCategory.singleFunctor _ 0).obj
          ((constantSheaf (fppfTopology B S hS 𝒳) AddCommGrpCat.{u + 1}).obj
            (AddCommGrpCat.of (ULift.{u + 1} ℤ)))))

AlgebraicGeometry.Stack.FlatFppf.isIso_derivedAbelianLowerShriekAdjunction_counit_constantSheaf_schemeStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SchemeStackTerminalSubsite.lean, line 86. The attribute's comment: “for the Lg_! of 07AS part (3), the flat-fppf site of the stack of a scheme”.

For the stack of a scheme U, the counit of the derived adjunction Lg_! ⊣ g⁻¹ is invertible at the constant sheaf ℤ of (Sch/U)_{fppf} in degree zero, so the canonical comparison Lg_! ℤ ⟶ ℤ is an isomorphism.

theorem isIso_derivedAbelianLowerShriekAdjunction_counit_constantSheaf_schemeStack :
    IsIso ((derivedAbelianLowerShriekAdjunction B S hS (schemeStack.{u, w} B S hS U)
          (abelianLowerShriekAcyclic B S hS (schemeStack.{u, w} B S hS U))).counit.app
        ((DerivedCategory.singleFunctor _ 0).obj
          ((constantSheaf (fppfTopology B S hS (schemeStack.{u, w} B S hS U))
            AddCommGrpCat.{u + 1}).obj (AddCommGrpCat.of (ULift.{u + 1} ℤ)))))

AlgebraicGeometry.Stack.derivedAbelianLowerShriek_constantSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubsiteConstantSheafLowerShriek.lean, line 234. The attribute's comment: “both cases of the statement, for every algebraic stack and with nothing assumed: the Lg_! of 07AS part (1) (lisse-étale) and of 07AS part (3) (flat-fppf). For each, the first clause is Lg_!(ℤ[0]) ≅ ℤ[0] and the second is invertibility of the canonical map, the counit of Lg_! ⊣ g⁻¹ at ℤ[0]. Both Lg_! are the unconditional ones of 07AS (1) and (3); the cohomology comparison of 07AK that the proof runs on is the unconditional AlgebraicGeometry.Stack.LisseEtale.globalCohomologyIso resp. AlgebraicGeometry.Stack.FlatFppf.globalCohomologyIso, so neither g_!ℤ = ℤ nor the acyclicity of 0D6X is a hypothesis”.

Stacks 0H0Z. Let 𝒳 be an algebraic stack. Then Lg_! ℤ = ℤ, both for the Lg_! of Stacks 07AS part (1) — D(𝒳_{lisse,étale}) ⟶ D(𝒳_{étale}) — and for the Lg_! of part (3) — D(𝒳_{flat,fppf}) ⟶ D(𝒳_{fppf}).

For each of the two sites the statement has two clauses: the derived lower shriek of the constant sheaf ℤ of the subsite in degree zero is isomorphic to the constant sheaf ℤ of 𝒳 in degree zero, and the canonical map realizing this — the counit of Lg_! ⊣ g⁻¹ at ℤ[0], whose source is Lg_!(g⁻¹ℤ) = Lg_! ℤ — is an isomorphism. Nothing is assumed beyond 𝒳 being algebraic.

theorem derivedAbelianLowerShriek_constantSheaf :
    (Nonempty ((LisseEtale.derivedAbelianLowerShriek.{u, w} B S hS 𝒳).obj
        ((DerivedCategory.singleFunctor _ 0).obj
          ((constantSheaf (LisseEtale.inclusionTopology.{u, w} B S hS 𝒳)
            AddCommGrpCat.{u + 1}).obj (AddCommGrpCat.of (ULift.{u + 1} ℤ)))) ≅
      (DerivedCategory.singleFunctor _ 0).obj
        ((constantSheaf (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
          AddCommGrpCat.{u + 1}).obj (AddCommGrpCat.of (ULift.{u + 1} ℤ)))) ∧
      IsIso ((LisseEtale.derivedAbelianLowerShriekAdjunction.{u, w} B S hS 𝒳).counit.app
        ((DerivedCategory.singleFunctor _ 0).obj
          ((constantSheaf (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
            AddCommGrpCat.{u + 1}).obj (AddCommGrpCat.of (ULift.{u + 1} ℤ)))))) ∧
    (Nonempty ((FlatFppf.derivedAbelianLowerShriekFunctor B S hS 𝒳).obj
        ((DerivedCategory.singleFunctor _ 0).obj
          ((constantSheaf (FlatFppf.inclusionTopology B S hS 𝒳) AddCommGrpCat.{u + 1}).obj
            (AddCommGrpCat.of (ULift.{u + 1} ℤ)))) ≅
      (DerivedCategory.singleFunctor _ 0).obj
        ((constantSheaf (FlatFppf.fppfTopology B S hS 𝒳) AddCommGrpCat.{u + 1}).obj
          (AddCommGrpCat.of (ULift.{u + 1} ℤ)))) ∧
      IsIso ((FlatFppf.derivedAbelianLowerShriekFunctorAdjunction B S hS 𝒳).counit.app
        ((DerivedCategory.singleFunctor _ 0).obj
          ((constantSheaf (FlatFppf.fppfTopology B S hS 𝒳) AddCommGrpCat.{u + 1}).obj
            (AddCommGrpCat.of (ULift.{u + 1} ℤ))))))

Tag 0H10, a lemma

Tag 0H10 in the Stacks Project.

AlgebraicGeometry.Stack.FlatFppf.derivedGlobalSectionsRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DerivedGlobalSectionsOnSmoothAndFlatSites.lean, line 87. The attribute's comment: “part (2)(a) for complexes, at the flat-fppf site, with NO hypothesis: RΓ(𝒳_{flat,fppf}, g⁻¹K) = RΓ(𝒳_{fppf}, K), from Lg_! ℤ = ℤ (Tag 0H0Z, proved)”.

Stacks 0H10, part (2)(a), for complexes, with no hypothesis. Let 𝒳 be an algebraic stack and let g : Sh(𝒳_{flat,fppf}) ⟶ Sh(𝒳_{fppf}) be the comparison morphism of topoi of Stacks 08MZ, whose inverse image is restriction to the flat objects. For every K in the unbounded derived category of abelian sheaves on 𝒳_{fppf},

RΓ(𝒳_{flat,fppf}, g⁻¹K) = RΓ(𝒳_{fppf}, K),

naturally in K, where on each side RΓ is the total right derived functor of global sections (Sheaf.Γ, the right adjoint of the constant sheaf functor).

The proof is the source's: global sections are corepresented by ℤ, and Lg_! ℤ = ℤ (Stacks 0H0Z, isIso_derivedAbelianLowerShriekFunctorAdjunction_counit_constantSheaf) turns the derived adjunction Lg_! ⊣ g⁻¹ of Stacks 07AS (3) into the comparison.

def derivedGlobalSectionsRestrictionIso :
    Stacks.Cohomology.DerivedLowerShriek.derivedAbelianRestriction.{u + 1}
          (inclusionTopology B S hS 𝒳) (fppfTopology B S hS 𝒳) (objectProperty B S hS 𝒳).ι ⋙
        derivedGlobalSectionsOnFlatSite B S hS 𝒳 ≅
      AlgebraicGeometry.Stack.derivedGlobalSections.{u, u + 1} B S hS 𝒳.val

AlgebraicGeometry.Stack.LisseEtale.derivedGlobalSectionsRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DerivedGlobalSectionsOnSmoothAndFlatSites.lean, line 147. The attribute's comment: “part (1)(a) for complexes, at the lisse-étale site, with NO hypothesis: RΓ(𝒳_{lisse,étale}, g⁻¹K) = RΓ(𝒳_{étale}, K), from Lg_! ℤ = ℤ (Tag 0H0Z, proved)”.

Stacks 0H10, part (1)(a), for complexes, with no hypothesis. Let 𝒳 be an algebraic stack and let g : Sh(𝒳_{lisse,étale}) ⟶ Sh(𝒳_{étale}) be the comparison morphism of topoi of Stacks 08MZ, whose inverse image is restriction to the smooth objects. For every K in the unbounded derived category of abelian sheaves on 𝒳_{étale},

RΓ(𝒳_{lisse,étale}, g⁻¹K) = RΓ(𝒳_{étale}, K),

naturally in K, where on each side RΓ is the total right derived functor of global sections (Sheaf.Γ, the right adjoint of the constant sheaf functor).

The proof is the source's: global sections are corepresented by ℤ, and Lg_! ℤ = ℤ (Stacks 0H0Z, LisseEtale.isIso_derivedAbelianLowerShriekAdjunction_counit_constantSheaf) turns the derived adjunction Lg_! ⊣ g⁻¹ of Stacks 07AS (1) into the comparison.

def derivedGlobalSectionsRestrictionIso :
    derivedAbelianRestriction.{u, w} B S hS 𝒳 ⋙ derivedGlobalSections B S hS 𝒳 ≅
      derivedGlobalSectionsEtale B S hS 𝒳

AlgebraicGeometry.Stack.FlatFppf.derivedModuleGlobalSectionsRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DerivedModuleSectionsOnSmoothAndFlatSites.lean, line 119. The attribute's comment: “part (2)(a) for sheaves of modules (the closing sentence of the statement), with NO hypothesis: derived global sections on the flat-fppf site of g^*K, computed on complexes of modules, are those of K on the fppf site”.

Stacks 0H10, part (2)(a), for sheaves of modules. For every K in the unbounded derived category of sheaves of 𝒪_𝒳-modules on 𝒳_{fppf}, RΓ(𝒳_{flat,fppf}, g^*K) = RΓ(𝒳_{fppf}, K), naturally in K, both sides computed on complexes of modules; 𝒪_{𝒳_{flat,fppf}} = g⁻¹𝒪_𝒳 and g^* = g⁻¹.

def derivedModuleGlobalSectionsRestrictionIso :
    haveI := hasPointwiseRightKanExtension_inclusion_ab.{u, w, u + 1} B S hS 𝒳
    (Stacks.Cohomology.DerivedLowerShriek.BigSite.moduleInverseImage (inclusionTopology B S hS 𝒳)
        (fppfTopology B S hS 𝒳)
        (objectProperty B S hS 𝒳).ι (ambientRingStructureSheaf B S hS 𝒳)).mapDerivedCategory ⋙
        derivedModuleOf (restrictedRing (inclusionTopology B S hS 𝒳) (fppfTopology B S hS 𝒳)
          (objectProperty B S hS 𝒳).ι (ambientRingStructureSheaf B S hS 𝒳))
          (Sheaf.Γ (inclusionTopology B S hS 𝒳) AddCommGrpCat.{u + 1}) ≅
      derivedModuleOf (ambientRingStructureSheaf B S hS 𝒳)
        (Sheaf.Γ (fppfTopology B S hS 𝒳) AddCommGrpCat.{u + 1})

AlgebraicGeometry.Stack.FlatFppf.derivedModuleSectionsRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DerivedModuleSectionsOnSmoothAndFlatSites.lean, line 147. The attribute's comment: “part (2)(b) for sheaves of modules (the closing sentence of the statement), with NO hypothesis; cohomology over an object is the derived functor of sections over it”.

Stacks 0H10, part (2)(b), for sheaves of modules. For every object x of the flat-fppf site and every K in the unbounded derived category of sheaves of 𝒪_𝒳-modules on 𝒳_{fppf}, RΓ(x, g^*K) = RΓ(x, K), naturally in K, both sides computed on complexes of modules, cohomology over x being the derived functor of sections over x.

def derivedModuleSectionsRestrictionIso
    (x : ObjectProperty.FullSubcategory (objectProperty B S hS 𝒳)) :
    haveI := hasPointwiseRightKanExtension_inclusion_ab.{u, w, u + 1} B S hS 𝒳
    (Stacks.Cohomology.DerivedLowerShriek.BigSite.moduleInverseImage (inclusionTopology B S hS 𝒳)
        (fppfTopology B S hS 𝒳)
        (objectProperty B S hS 𝒳).ι (ambientRingStructureSheaf B S hS 𝒳)).mapDerivedCategory ⋙
        derivedModuleOf (restrictedRing (inclusionTopology B S hS 𝒳) (fppfTopology B S hS 𝒳)
          (objectProperty B S hS 𝒳).ι (ambientRingStructureSheaf B S hS 𝒳))
          (abelianSections.{u + 1} (inclusionTopology B S hS 𝒳) x) ≅
      derivedModuleOf (ambientRingStructureSheaf B S hS 𝒳)
        (abelianSections.{u + 1} (fppfTopology B S hS 𝒳) ((objectProperty B S hS 𝒳).ι.obj x))

AlgebraicGeometry.Stack.LisseEtale.derivedModuleGlobalSectionsRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DerivedModuleSectionsOnSmoothAndFlatSites.lean, line 228. The attribute's comment: “part (1)(a) for sheaves of modules (the closing sentence of the statement), with NO hypothesis: derived global sections on the lisse-étale site of g^*K, computed on complexes of modules, are those of K on the étale site”.

Stacks 0H10, part (1)(a), for sheaves of modules. For every K in the unbounded derived category of sheaves of 𝒪_𝒳-modules on 𝒳_{étale}, RΓ(𝒳_{lisse,étale}, g^*K) = RΓ(𝒳_{étale}, K), naturally in K, both sides computed on complexes of modules; 𝒪_{𝒳_{lisse,étale}} = g⁻¹𝒪_𝒳 and g^* = g⁻¹.

def derivedModuleGlobalSectionsRestrictionIso :
    haveI := isContinuous_inclusion.{u, w} B S hS 𝒳 (closedUnderSmoothMorphisms.{u, w} B S hS 𝒳)
    haveI := isCocontinuous_inclusion.{u, w} B S hS 𝒳
      (closedUnderSmoothMorphisms.{u, w} B S hS 𝒳)
    (Stacks.Cohomology.DerivedLowerShriek.BigSite.moduleInverseImage
        (inclusionTopology.{u, w} B S hS 𝒳)
        (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
        (smoothObject.{u, w} B S hS 𝒳).ι (ambientRingStructureSheaf B S hS 𝒳)).mapDerivedCategory ⋙
        derivedModuleOf (restrictedRing (inclusionTopology.{u, w} B S hS 𝒳)
          (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
          (smoothObject.{u, w} B S hS 𝒳).ι (ambientRingStructureSheaf B S hS 𝒳))
          (Sheaf.Γ (inclusionTopology.{u, w} B S hS 𝒳) AddCommGrpCat.{u + 1}) ≅
      derivedModuleOf (ambientRingStructureSheaf B S hS 𝒳)
        (Sheaf.Γ (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
          AddCommGrpCat.{u + 1})

AlgebraicGeometry.Stack.LisseEtale.derivedModuleSectionsRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DerivedModuleSectionsOnSmoothAndFlatSites.lean, line 262. The attribute's comment: “part (1)(b) for sheaves of modules (the closing sentence of the statement), with NO hypothesis; cohomology over an object is the derived functor of sections over it”.

Stacks 0H10, part (1)(b), for sheaves of modules. For every object x of the lisse-étale site and every K in the unbounded derived category of sheaves of 𝒪_𝒳-modules on 𝒳_{étale}, RΓ(x, g^*K) = RΓ(x, K), naturally in K, both sides computed on complexes of modules, cohomology over x being the derived functor of sections over x.

def derivedModuleSectionsRestrictionIso (x : LisseEtale.{u, w} B S hS 𝒳) :
    haveI := isContinuous_inclusion.{u, w} B S hS 𝒳 (closedUnderSmoothMorphisms.{u, w} B S hS 𝒳)
    haveI := isCocontinuous_inclusion.{u, w} B S hS 𝒳
      (closedUnderSmoothMorphisms.{u, w} B S hS 𝒳)
    (Stacks.Cohomology.DerivedLowerShriek.BigSite.moduleInverseImage
        (inclusionTopology.{u, w} B S hS 𝒳)
        (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
        (smoothObject.{u, w} B S hS 𝒳).ι (ambientRingStructureSheaf B S hS 𝒳)).mapDerivedCategory ⋙
        derivedModuleOf (restrictedRing (inclusionTopology.{u, w} B S hS 𝒳)
          (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
          (smoothObject.{u, w} B S hS 𝒳).ι (ambientRingStructureSheaf B S hS 𝒳))
          (abelianSections.{u + 1} (inclusionTopology.{u, w} B S hS 𝒳) x) ≅
      derivedModuleOf (ambientRingStructureSheaf B S hS 𝒳)
        (abelianSections.{u + 1} (associatedTopology B S hS 𝒳.val.val.p (etaleTopology B))
          ((smoothObject.{u, w} B S hS 𝒳).ι.obj x))

AlgebraicGeometry.Stack.FlatFppf.derivedSectionsRestrictionIsoOfFlatObject, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DerivedSectionsOverSmoothAndFlatObjects.lean, line 133. The attribute's comment: “part (2)(b) for complexes, at the flat-fppf site, with NO hypothesis: the half of Tag 0794 that AlgebraicGeometry.Stack.FlatFppf.derivedSectionsRestrictionIso carries as hgen is AlgebraicGeometry.Stack.FlatFppf.derivedLowerShriekComputesFlatGenerator. Cohomology over an object is the derived functor of sections over it (equal to cohomology of the slice site by Tag 03F3)”.

Stacks 0H10, part (2)(b), for complexes, with no hypothesis. Let 𝒳 be an algebraic stack and let g : Sh(𝒳_{flat,fppf}) ⟶ Sh(𝒳_{fppf}) be the comparison morphism of topoi of Stacks 08MZ, whose inverse image is restriction to the flat objects. For every object x of the flat-fppf site and every K in the unbounded derived category of abelian sheaves on 𝒳_{fppf},

RΓ(𝒳_{flat,fppf}/x, g⁻¹K) = RΓ(x, K),

naturally in K, where on each side cohomology over x is the right derived functor of sections over x on the respective site (the convention of Stacks 0DD8 here; it is cohomology of the slice site by Stacks 03F3). This is derivedSectionsRestrictionIso with its hypothesis hgen proved, by derivedLowerShriekComputesFlatGenerator.

def derivedSectionsRestrictionIsoOfFlatObject
    (x : ObjectProperty.FullSubcategory (objectProperty B S hS 𝒳)) :
    Stacks.Cohomology.DerivedLowerShriek.derivedAbelianRestriction.{u + 1}
          (inclusionTopology B S hS 𝒳) (fppfTopology B S hS 𝒳) (objectProperty B S hS 𝒳).ι ⋙
        derivedSections B S hS 𝒳 x ≅
      derivedSectionsFppf B S hS 𝒳 ((objectProperty B S hS 𝒳).ι.obj x)

AlgebraicGeometry.Stack.LisseEtale.derivedSectionsRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DerivedSectionsOverSmoothAndFlatObjects.lean, line 227. The attribute's comment: “part (1)(b) for complexes, at the lisse-étale site, with NO hypothesis. Cohomology over an object is the derived functor of sections over it (equal to cohomology of the slice site by Tag 03F3)”.

Stacks 0H10, part (1)(b), for complexes, with no hypothesis. Let 𝒳 be an algebraic stack and let g : Sh(𝒳_{lisse,étale}) ⟶ Sh(𝒳_{étale}) be the comparison morphism of topoi of Stacks 08MZ, whose inverse image is restriction to the smooth objects. For every object x of the lisse-étale site and every K in the unbounded derived category of abelian sheaves on 𝒳_{étale},

RΓ(𝒳_{lisse,étale}/x, g⁻¹K) = RΓ(x, K),

naturally in K, where on each side cohomology over x is the right derived functor of sections over x on the respective site (the convention of Stacks 0DD8 here; it is cohomology of the slice site by Stacks 03F3).

This is Stacks 0DD8 (1) on sites that need not be small, Stacks.Cohomology.DerivedLowerShriek.BigSite.derivedAbelianSectionsRestrictionIso, at the lisse-étale inclusion: continuity and cocontinuity come from AlgebraicGeometry.Stack.LisseEtale.closedUnderSmoothMorphisms, the existence and absoluteness of Lg_! from AlgebraicGeometry.Stack.LisseEtale.abelianLowerShriekAcyclic, and the counit at the generator from derivedLowerShriekComputesSmoothGenerator.

def derivedSectionsRestrictionIso (x : LisseEtale.{u, w} B S hS 𝒳) :
    derivedAbelianRestriction.{u, w} B S hS 𝒳 ⋙ derivedSections B S hS 𝒳 x ≅
      derivedSectionsEtale B S hS 𝒳 ((smoothObject.{u, w} B S hS 𝒳).ι.obj x)

AlgebraicGeometry.Stack.FlatFppf.derivedSectionsRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfDerivedSections.lean, line 147. The attribute's comment: “part (2)(b) for complexes, at the flat-fppf site, with cohomology over an object taken as the derived functor of sections over it; conditional only on the half of Stacks 0794 that computes Lg_! on a generator”.

Stacks 0H10, part (2)(b), for complexes. Let 𝒳 be an algebraic stack and let g : Sh(𝒳_{flat,fppf}) ⟶ Sh(𝒳_{fppf}) be the comparison morphism of topoi of Stacks 08MZ, whose inverse image is restriction to the flat objects. For every object x of the flat-fppf site and every K in the unbounded derived category of abelian sheaves on 𝒳_{fppf},

RΓ(x, g⁻¹K) = RΓ(x, K),

naturally in K, where on each side cohomology over x is the right derived functor of sections over x on the respective site (the convention of Stacks 0DD8 and Stacks 03YU here; see the module docstring on why not the slice site).

The closure condition of Stacks 07AK (1), the existence of g_! and g_*, Grothendieck abelianness of both categories of abelian sheaves, and the acyclicity statement of Stacks 07AC that Stacks 07AS (3) needs are all discharged, with no hypothesis on 𝒳. The single carried input is hgen.

def derivedSectionsRestrictionIso
    (x : ObjectProperty.FullSubcategory (objectProperty B S hS 𝒳))
    (hgen : DerivedLowerShriekComputesFlatGenerator B S hS 𝒳 x) :
    Stacks.Cohomology.DerivedLowerShriek.derivedAbelianRestriction.{u + 1}
          (inclusionTopology B S hS 𝒳)
          (fppfTopology B S hS 𝒳) (objectProperty B S hS 𝒳).ι ⋙
        derivedSections B S hS 𝒳 x ≅
      derivedSectionsFppf B S hS 𝒳 ((objectProperty B S hS 𝒳).ι.obj x)

Sources

• Section 104.4, Tag 0H0Y
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.FlatFppf.isIso_derivedAbelianLowerShriekAdjunction_counit_constantSheaf_of_isTerminal · AlgebraicGeometry.Stack.FlatFppf.isIso_derivedAbelianLowerShriekAdjunction_counit_constantSheaf_schemeStack · AlgebraicGeometry.Stack.derivedAbelianLowerShriek_constantSheaf · AlgebraicGeometry.Stack.FlatFppf.derivedGlobalSectionsRestrictionIso · AlgebraicGeometry.Stack.LisseEtale.derivedGlobalSectionsRestrictionIso · AlgebraicGeometry.Stack.FlatFppf.derivedModuleGlobalSectionsRestrictionIso · AlgebraicGeometry.Stack.FlatFppf.derivedModuleSectionsRestrictionIso · AlgebraicGeometry.Stack.LisseEtale.derivedModuleGlobalSectionsRestrictionIso

Section104.5 Derived categories of quasi-coherent modules#

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

Tag 07B6, a definition

Tag 07B6 in the Stacks Project.

AlgebraicGeometry.Stack.derivedCategoryQuasicoherent, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedQuasicoherent.lean, line 152. The attribute's comment: “the Verdier quotient D_QCoh(𝒪_𝒳) = D_LQCoh^fbc(𝒪_𝒳) / D_(Parasitic ∩ LQCoh^fbc)(𝒪_𝒳)”.

Stacks 07B6. The derived category of 𝒪_𝒳-modules with quasi-coherent cohomology sheaves of an algebraic stack 𝒳, that is the Verdier quotient

D_QCoh(𝒪_𝒳) = D_{LQCoh^fbc}(𝒪_𝒳) / D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳),

realized as the localization of D_{LQCoh^fbc}(𝒪_𝒳) at the morphisms whose cone lies in D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳).

abbrev derivedCategoryQuasicoherent

AlgebraicGeometry.Stack.toDerivedCategoryQuasicoherent, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedQuasicoherent.lean, line 157. The attribute's comment: “the quotient functor onto D_QCoh(𝒪_𝒳)”.

Stacks 07B6, the quotient functor D_{LQCoh^fbc}(𝒪_𝒳) ⟶ D_QCoh(𝒪_𝒳) of the Verdier quotient.

abbrev toDerivedCategoryQuasicoherent :
    (derivedLocallyQuasicoherentFlatBaseChange B E h S hS 𝒳).FullSubcategory ⥤
      derivedCategoryQuasicoherent B E h S hS 𝒳

AlgebraicGeometry.Stack.derivedCategoryQuasicoherentSheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedQuasicoherentCohomologySheaf.lean, line 265. The attribute's comment: “the Verdier quotient D_QCoh(𝒪_𝒳) = D_LQCoh^fbc(𝒪_𝒳) / D_(Parasitic ∩ LQCoh^fbc)(𝒪_𝒳), with the flat base change property of LQCoh^fbc read on sheaves of modules as in the source”.

Stacks 07B6, at the source's LQCoh^fbc(𝒪_𝒳): the derived category with quasi-coherent cohomology D_QCoh(𝒪_𝒳) = D_{LQCoh^fbc}(𝒪_𝒳) / D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳), the Verdier quotient of the triangulated subcategory of complexes of 𝒪_𝒳-modules with cohomology in LQCoh^fbc(𝒪_𝒳) (a weak Serre subcategory, Stacks 0771) by the one with cohomology in the parasitic modules of LQCoh^fbc(𝒪_𝒳).

abbrev derivedCategoryQuasicoherentSheaf

AlgebraicGeometry.Stack.toDerivedCategoryQuasicoherentSheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedQuasicoherentCohomologySheaf.lean, line 272. The attribute's comment: “the quotient functor D_LQCoh^fbc(𝒪_𝒳) ⟶ D_QCoh(𝒪_𝒳), with the flat base change property read on sheaves of modules as in the source”.

Stacks 07B6, at the source's LQCoh^fbc(𝒪_𝒳): the quotient functor.

abbrev toDerivedCategoryQuasicoherentSheaf :
    (DerivedCategoryB.derivedCategoryB (lqcFbcFppf B S hS 𝒳)).FullSubcategory ⥤
      derivedCategoryQuasicoherentSheaf B S hS 𝒳

Tag 07B7, an equation

Tag 07B7 in the Stacks Project.

AlgebraicGeometry.Stack.cohomologyDerivedCategoryQuasicoherent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedQuasicoherentCohomology.lean, line 327. The attribute's comment: “the cohomology functor H^i : D_QCoh(𝒪_𝒳) ⟶ QCoh(𝒪_𝒳)”.

Stacks 07B7. The cohomology functor

H^i : D_QCoh(𝒪_𝒳) ⟶ QCoh(𝒪_𝒳)

on the derived category of 𝒪_𝒳-modules with quasi-coherent cohomology sheaves of an algebraic stack 𝒳. It is the descent through the Verdier quotient of Stacks 07B6 of the functor Q ∘ H^i on D_{LQCoh^fbc}(𝒪_𝒳), which is possible because that functor inverts the morphisms the quotient inverts.

def cohomologyDerivedCategoryQuasicoherent (i : ℤ)
    (hhom : (cohomologyQuasicoherent B E h S hS 𝒳 hinc hclosed hpres hls hlsD hwp hsep
      i).IsHomological)
    (hQker : ∀ F : locallyQuasicoherentFlatBaseChangeModules.{u, u + 1, u} B E h S hS
        𝒳.val.val.p 𝒳.val.isFiberedInGroupoids,
      IsZero ((quasicoheratorOfStack B E h S hS 𝒳 hinc hclosed hpres hls hlsD hwp hsep).obj F) ↔
        IsParasitic B S hS 𝒳 .etale F.obj.val) :
    derivedCategoryQuasicoherent B E h S hS 𝒳 ⥤
      FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS 𝒳.val.val.p
        𝒳.val.isFiberedInGroupoids

AlgebraicGeometry.Stack.cohomologyDerivedCategoryQuasicoherentFac, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedQuasicoherentCohomology.lean, line 346. The attribute's comment: “the identity H^i ∘ (quotient functor) = Q ∘ H^i defining the cohomology functor”.

Stacks 07B7, the identity defining the cohomology functor: composed with the quotient functor D_{LQCoh^fbc}(𝒪_𝒳) ⟶ D_QCoh(𝒪_𝒳), the functor H^i of Stacks 07B7 is the functor Q ∘ H^i it descends.

def cohomologyDerivedCategoryQuasicoherentFac (i : ℤ)
    (hhom : (cohomologyQuasicoherent B E h S hS 𝒳 hinc hclosed hpres hls hlsD hwp hsep
      i).IsHomological)
    (hQker : ∀ F : locallyQuasicoherentFlatBaseChangeModules.{u, u + 1, u} B E h S hS
        𝒳.val.val.p 𝒳.val.isFiberedInGroupoids,
      IsZero ((quasicoheratorOfStack B E h S hS 𝒳 hinc hclosed hpres hls hlsD hwp hsep).obj F) ↔
        IsParasitic B S hS 𝒳 .etale F.obj.val) :
    toDerivedCategoryQuasicoherent B E h S hS 𝒳 ⋙
        cohomologyDerivedCategoryQuasicoherent B E h S hS 𝒳 hinc hclosed hpres hls hlsD hwp hsep
          i hhom hQker ≅
      cohomologyQuasicoherent B E h S hS 𝒳 hinc hclosed hpres hls hlsD hwp hsep i

AlgebraicGeometry.Stack.cohomologyDerivedCategoryQuasicoherentSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedQuasicoherentCohomologySheaf.lean, line 305. The attribute's comment: “the cohomology functor H^i : D_QCoh(𝒪_𝒳) ⟶ QCoh(𝒪_𝒳), descended from Q ∘ H^i with Q the coherator of 0778”.

Stacks 07B7: the cohomological functor H^i : D_QCoh(𝒪_𝒳) ⟶ QCoh(𝒪_𝒳), the functor Q ∘ H^i : D_{LQCoh^fbc}(𝒪_𝒳) ⟶ QCoh(𝒪_𝒳) descended to the Verdier quotient (Stacks 05RJ), Q being the coherator of Stacks 0778, which annihilates Parasitic(𝒪_𝒳) ∩ LQCoh^fbc(𝒪_𝒳) (Stacks 0779).

def cohomologyDerivedCategoryQuasicoherentSheaf (i : ℤ) :
    derivedCategoryQuasicoherentSheaf B S hS 𝒳 ⥤
      FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS 𝒳.val.val.p
        𝒳.val.isFiberedInGroupoids

AlgebraicGeometry.Stack.cohomologyDerivedCategoryQuasicoherentSheafFac, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedQuasicoherentCohomologySheaf.lean, line 314. The attribute's comment: “the identity H^i ∘ (quotient functor) = Q ∘ H^i defining the cohomology functor”.

Stacks 07B7: the defining identity H^i ∘ (quotient functor) ≅ Q ∘ H^i.

def cohomologyDerivedCategoryQuasicoherentSheafFac (i : ℤ) :
    toDerivedCategoryQuasicoherentSheaf B S hS 𝒳 ⋙
        cohomologyDerivedCategoryQuasicoherentSheaf B S hS 𝒳 i ≅
      DerivedCategoryB.cohomologyComp (lqcFbcFppf B S hS 𝒳)
        (flatGroupoidPresentation 𝒳).flatBaseChangeCoherator i

AlgebraicGeometry.Stack.isHomological_cohomologyDerivedCategoryQuasicoherentSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedQuasicoherentCohomologySheaf.lean, line 324. The attribute's comment: “the descended H^i : D_QCoh(𝒪_𝒳) ⟶ QCoh(𝒪_𝒳) is a cohomological functor”.

Stacks 07B7: H^i : D_QCoh(𝒪_𝒳) ⟶ QCoh(𝒪_𝒳) is a cohomological functor.

theorem isHomological_cohomologyDerivedCategoryQuasicoherentSheaf (i : ℤ) :
    (cohomologyDerivedCategoryQuasicoherentSheaf B S hS 𝒳 i).IsHomological

AlgebraicGeometry.Stack.isZero_iff_forall_isZero_cohomologyDerivedCategoryQuasicoherentSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedQuasicoherentCohomologySheaf.lean, line 332. The attribute's comment: “E is zero in D_QCoh(𝒪_𝒳) if and only if H^i(E) = 0 for every i”.

Stacks 07B7: an object E of D_QCoh(𝒪_𝒳) is zero exactly when H^i(E) = 0 for all i, the kernel of Q being exactly Parasitic(𝒪_𝒳) ∩ LQCoh^fbc(𝒪_𝒳) (Stacks 0779 (1)).

theorem isZero_iff_forall_isZero_cohomologyDerivedCategoryQuasicoherentSheaf
    (X : derivedCategoryQuasicoherentSheaf B S hS 𝒳) :
    IsZero X ↔ ∀ i : ℤ,
      IsZero ((cohomologyDerivedCategoryQuasicoherentSheaf B S hS 𝒳 i).obj X)

Tag 07B8, a lemma

Tag 07B8 in the Stacks Project.

AlgebraicGeometry.Stack.epsilonPullbackDerived, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedQuasicoherentEtaleComparison.lean, line 328. The attribute's comment: “the right-hand vertical arrow ε^* : D(𝒳_étale, 𝒪_𝒳) ⥤ D(𝒪_𝒳) of the diagram”.

The right-hand vertical arrow of the diagram of Stacks 07B8, the triangulated functor ε^* : D(𝒳_étale, 𝒪_𝒳) ⥤ D(𝒪_𝒳) induced by the exact functor ε^* on modules.

def epsilonPullbackDerived :
    DerivedCategory (etaleModules B S hS 𝒳) ⥤ DerivedCategory (fppfModules B S hS 𝒳)

AlgebraicGeometry.Stack.epsilonPullbackDerivedLocallyQuasicoherent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedQuasicoherentEtaleComparison.lean, line 400. The attribute's comment: “the middle vertical arrow ε^* : D_{LQCoh^fbc}(𝒳_étale, 𝒪_𝒳) ⥤ D_{LQCoh^fbc}(𝒪_𝒳) of the diagram”.

Stacks 07B8, the middle vertical arrow of the diagram. The functor

ε^* : D_{LQCoh^fbc}(𝒳_étale, 𝒪_𝒳) ⥤ D_{LQCoh^fbc}(𝒪_𝒳),

the corestriction to D_{LQCoh^fbc}(𝒪_𝒳) of ε^* on the ambient derived categories.

def epsilonPullbackDerivedLocallyQuasicoherent :
    (derivedLocallyQuasicoherentFlatBaseChangeEtale B E h S hS 𝒳).FullSubcategory ⥤
      (derivedLocallyQuasicoherentFlatBaseChange B E h S hS 𝒳).FullSubcategory

AlgebraicGeometry.Stack.epsilonPullbackDerivedParasitic, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedQuasicoherentEtaleComparison.lean, line 417. The attribute's comment: “the left vertical arrow ε^* : D_{𝒫_𝒳}(𝒳_étale, 𝒪_𝒳) ⥤ D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳) of the diagram”.

Stacks 07B8, the left vertical arrow of the diagram. The functor

ε^* : D_{𝒫_𝒳}(𝒳_étale, 𝒪_𝒳) ⥤ D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳),

the corestriction to D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳) of ε^* on the ambient derived categories.

def epsilonPullbackDerivedParasitic :
    (derivedParasiticLocallyQuasicoherentFlatBaseChangeEtale B E h S hS 𝒳).FullSubcategory ⥤
      (derivedParasiticLocallyQuasicoherentFlatBaseChange B E h S hS 𝒳).FullSubcategory

AlgebraicGeometry.Stack.epsilonPullbackDerived_rightSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedQuasicoherentEtaleComparison.lean, line 436. The attribute's comment: “the right-hand square of the diagram: the inclusion D_{LQCoh^fbc}(𝒳_étale, 𝒪_𝒳) ⊆ D(𝒳_étale, 𝒪_𝒳) followed by ε^ is ε^ followed by the inclusion D_{LQCoh^fbc}(𝒪_𝒳) ⊆ D(𝒪_𝒳)”.

Stacks 07B8, the right-hand square of the diagram commutes. Going along the bottom row from D_{LQCoh^fbc}(𝒳_étale, 𝒪_𝒳) into D(𝒳_étale, 𝒪_𝒳) and then up by ε^* is going up by ε^* into D_{LQCoh^fbc}(𝒪_𝒳) and then along the top row into D(𝒪_𝒳).

This is an equality of functors, not merely an isomorphism: the middle vertical arrow is by construction the corestriction of ε^*.

theorem epsilonPullbackDerived_rightSquare :
    (derivedLocallyQuasicoherentFlatBaseChangeEtale B E h S hS 𝒳).ι ⋙
        epsilonPullbackDerived B S hS 𝒳 =
      epsilonPullbackDerivedLocallyQuasicoherent B E h S hS 𝒳 hfppfSheaf ⋙
        (derivedLocallyQuasicoherentFlatBaseChange B E h S hS 𝒳).ι

AlgebraicGeometry.Stack.epsilonPullbackDerived_leftSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedQuasicoherentEtaleComparison.lean, line 450. The attribute's comment: “the left-hand square of the diagram: the inclusion D_{𝒫_𝒳}(𝒳_étale, 𝒪_𝒳) ⊆ D_{LQCoh^fbc}(𝒳_étale, 𝒪_𝒳) followed by ε^ is ε^ followed by the inclusion D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳) ⊆ D_{LQCoh^fbc}(𝒪_𝒳)”.

Stacks 07B8, the left-hand square of the diagram commutes. Going along the bottom row from D_{𝒫_𝒳}(𝒳_étale, 𝒪_𝒳) into D_{LQCoh^fbc}(𝒳_étale, 𝒪_𝒳) and then up by ε^* is going up by ε^* into D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳) and then along the top row into D_{LQCoh^fbc}(𝒪_𝒳).

theorem epsilonPullbackDerived_leftSquare :
    ObjectProperty.ιOfLE
          (derivedParasiticLocallyQuasicoherentFlatBaseChangeEtale_le B E h S hS 𝒳) ⋙
        epsilonPullbackDerivedLocallyQuasicoherent B E h S hS 𝒳 hfppfSheaf =
      epsilonPullbackDerivedParasitic B E h S hS 𝒳 hfppfSheaf ⋙
        ObjectProperty.ιOfLE
          (derivedParasiticLocallyQuasicoherentFlatBaseChange_le B E h S hS 𝒳)

AlgebraicGeometry.Stack.epsilonPullbackDerived_outerRectangle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedQuasicoherentEtaleComparison.lean, line 462. The attribute's comment: “the outer rectangle of the diagram, the composite of its two squares”.

Stacks 07B8, the outer rectangle of the diagram commutes: the composite of the two squares, read from D_{𝒫_𝒳}(𝒳_étale, 𝒪_𝒳) to D(𝒪_𝒳).

theorem epsilonPullbackDerived_outerRectangle :
    (derivedParasiticLocallyQuasicoherentFlatBaseChangeEtale B E h S hS 𝒳).ι ⋙
        epsilonPullbackDerived B S hS 𝒳 =
      epsilonPullbackDerivedParasitic B E h S hS 𝒳 hfppfSheaf ⋙
        (derivedParasiticLocallyQuasicoherentFlatBaseChange B E h S hS 𝒳).ι

AlgebraicGeometry.Stack.derivedCategoryQuasicoherentEtaleEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedQuasicoherentEtaleComparison.lean, line 524. The attribute's comment: “the last assertion: the induced equivalence D_{LQCoh^fbc}(𝒳_étale, 𝒪_𝒳) / D_{𝒫_𝒳}(𝒳_étale, 𝒪_𝒳) ⟶ D_QCoh(𝒪_𝒳), given that the middle vertical arrow is an equivalence matching the two inverted classes”.

Stacks 07B8, the last assertion. If the middle vertical arrow

ε^* : D_{LQCoh^fbc}(𝒳_étale, 𝒪_𝒳) ⥤ D_{LQCoh^fbc}(𝒪_𝒳)

is an equivalence of triangulated categories and matches the two classes of morphisms the Verdier quotients invert, then it descends to an equivalence

D_{LQCoh^fbc}(𝒳_étale, 𝒪_𝒳) / D_{𝒫_𝒳}(𝒳_étale, 𝒪_𝒳) ≌ D_QCoh(𝒪_𝒳).

The two hypotheses are the source's own "moreover": hG is "the middle vertical arrow is an equivalence of triangulated categories", which the source gets from Stacks 07A8 together with Stacks 0D7W — both of which the library has, but only for a site whose objects and morphisms share a universe; see the module docstring — and hW is the matching of the inverted classes, which comes from the compatibility of ε^* with the left vertical arrow, the verification the source explicitly omits.

Given them the descent is formal: ε^* followed by the quotient functor of Stacks 07B6 is again a localization at the étale class, by transport of a localization along an equivalence of the source category, and two localizations at one and the same class of morphisms are canonically equivalent.

def derivedCategoryQuasicoherentEtaleEquivalence
    (hG : (epsilonPullbackDerivedLocallyQuasicoherent B E h S hS 𝒳 hfppfSheaf).IsEquivalence)
    (hW : derivedQuasicoherentWEtale B E h S hS 𝒳 =
      (derivedQuasicoherentW B E h S hS 𝒳).inverseImage
        (epsilonPullbackDerivedLocallyQuasicoherent B E h S hS 𝒳 hfppfSheaf)) :
    derivedCategoryQuasicoherentEtale B E h S hS 𝒳 ≌
      derivedCategoryQuasicoherent B E h S hS 𝒳

AlgebraicGeometry.Stack.epsilonPullbackDerivedSheafFlatBaseChange, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/SheafFlatBaseChangeEtaleFppfDerivedEquivalence.lean, line 169. The attribute's comment: “the middle vertical arrow ε^* : D_{LQCoh^fbc}(𝒳_étale, 𝒪_𝒳) ⥤ D_{LQCoh^fbc}(𝒪_𝒳) of the diagram, for LQCoh^fbc with the flat base change property of Stacks 0762 read with the pullback of sheaves”.

Stacks 07B8, the middle vertical arrow of the diagram,

ε^* : D_{LQCoh^fbc}(𝒳_étale, 𝒪_𝒳) ⥤ D_{LQCoh^fbc}(𝒪_𝒳),

with LQCoh^fbc read with the flat base change property of Stacks 0762 for the pullback of sheaves: the corestriction of ε^* on the ambient derived categories.

abbrev epsilonPullbackDerivedSheafFlatBaseChange :
    (DerivedCategoryB.derivedCategoryB
        (locallyQuasicoherentSheafFlatBaseChangeEtaleModules B E h S hS 𝒳)).FullSubcategory ⥤
      (DerivedCategoryB.derivedCategoryB
        (lqcohSheafFbcFppfModules.{u, _, u} B E h S hS 𝒳)).FullSubcategory

AlgebraicGeometry.Stack.epsilonPullbackDerivedParasiticSheafFlatBaseChange, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/SheafFlatBaseChangeEtaleFppfDerivedEquivalence.lean, line 188. The attribute's comment: “the left vertical arrow ε^* : D_{𝒫_𝒳}(𝒳_étale, 𝒪_𝒳) ⥤ D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳) of the diagram, for LQCoh^fbc with the flat base change property of Stacks 0762 read with the pullback of sheaves”.

Stacks 07B8, the left vertical arrow of the diagram,

ε^* : D_{𝒫_𝒳}(𝒳_étale, 𝒪_𝒳) ⥤ D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳),

with LQCoh^fbc read with the flat base change property of Stacks 0762 for the pullback of sheaves: the corestriction of ε^* on the ambient derived categories.

abbrev epsilonPullbackDerivedParasiticSheafFlatBaseChange :
    (derivedInter (parasiticModules.{u, w, u} B S hS 𝒳 .etale)
        (locallyQuasicoherentSheafFlatBaseChangeEtaleModules B E h S hS 𝒳)).FullSubcategory ⥤
      (derivedInter (parasiticModules.{u, w, u} B S hS 𝒳 .fppf)
        (lqcohSheafFbcFppfModules.{u, _, u} B E h S hS 𝒳)).FullSubcategory

AlgebraicGeometry.Stack.epsilonPullbackDerivedSheafFlatBaseChange_rightSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/SheafFlatBaseChangeEtaleFppfDerivedEquivalence.lean, line 206. The attribute's comment: “the right-hand square of the diagram, for LQCoh^fbc with the flat base change property of Stacks 0762 read with the pullback of sheaves”.

Stacks 07B8, the right-hand square of the diagram commutes: the inclusion D_{LQCoh^fbc}(𝒳_étale, 𝒪_𝒳) ⊆ D(𝒳_étale, 𝒪_𝒳) followed by ε^* is ε^* followed by the inclusion D_{LQCoh^fbc}(𝒪_𝒳) ⊆ D(𝒪_𝒳), as an equality of functors.

theorem epsilonPullbackDerivedSheafFlatBaseChange_rightSquare :
    (DerivedCategoryB.derivedCategoryB
        (locallyQuasicoherentSheafFlatBaseChangeEtaleModules B E h S hS 𝒳)).ι ⋙
        epsilonPullbackDerived B S hS 𝒳 =
      epsilonPullbackDerivedSheafFlatBaseChange B E h S hS 𝒳 ⋙
        (DerivedCategoryB.derivedCategoryB
          (lqcohSheafFbcFppfModules.{u, _, u} B E h S hS 𝒳)).ι

AlgebraicGeometry.Stack.epsilonPullbackDerivedSheafFlatBaseChange_leftSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/SheafFlatBaseChangeEtaleFppfDerivedEquivalence.lean, line 241. The attribute's comment: “the left-hand square of the diagram, for LQCoh^fbc with the flat base change property of Stacks 0762 read with the pullback of sheaves”.

Stacks 07B8, the left-hand square of the diagram commutes: the inclusion D_{𝒫_𝒳}(𝒳_étale, 𝒪_𝒳) ⊆ D_{LQCoh^fbc}(𝒳_étale, 𝒪_𝒳) followed by ε^* is ε^* followed by the inclusion D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳) ⊆ D_{LQCoh^fbc}(𝒪_𝒳), as an equality of functors.

theorem epsilonPullbackDerivedSheafFlatBaseChange_leftSquare :
    ObjectProperty.ιOfLE (derivedParasiticSheafFlatBaseChangeEtale_le B E h S hS 𝒳) ⋙
        epsilonPullbackDerivedSheafFlatBaseChange B E h S hS 𝒳 =
      epsilonPullbackDerivedParasiticSheafFlatBaseChange B E h S hS 𝒳 ⋙
        ObjectProperty.ιOfLE (derivedParasiticSheafFlatBaseChange_le B E h S hS 𝒳)

AlgebraicGeometry.Stack.isEquivalence_epsilonPullbackDerivedSheafFlatBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/SheafFlatBaseChangeEtaleFppfDerivedEquivalence.lean, line 296. The attribute's comment: “the middle vertical arrow is an equivalence of triangulated categories, for LQCoh^fbc with the flat base change property of Stacks 0762 read with the pullback of sheaves”.

Stacks 07B8, the middle vertical arrow is an equivalence of triangulated categories:

ε^* : D_{LQCoh^fbc}(𝒳_étale, 𝒪_𝒳) ⥤ D_{LQCoh^fbc}(𝒪_𝒳)

is an equivalence, and it is a triangulated functor for the triangulated structures of the two strictly full triangulated subcategories, LQCoh^fbc being a weak Serre subcategory on both sites.

theorem isEquivalence_epsilonPullbackDerivedSheafFlatBaseChange :
    (epsilonPullbackDerivedSheafFlatBaseChange B E h S hS 𝒳).IsEquivalence ∧
      (epsilonPullbackDerivedSheafFlatBaseChange B E h S hS 𝒳).IsTriangulated

AlgebraicGeometry.Stack.isEquivalence_epsilonPullbackDerivedParasiticSheafFlatBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/SheafFlatBaseChangeEtaleFppfDerivedEquivalence.lean, line 345. The attribute's comment: “the left vertical arrow is an equivalence of triangulated categories, for LQCoh^fbc with the flat base change property of Stacks 0762 read with the pullback of sheaves”.

Stacks 07B8, the left vertical arrow is an equivalence of triangulated categories:

ε^* : D_{𝒫_𝒳}(𝒳_étale, 𝒪_𝒳) ⥤ D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳)

is an equivalence, and it is a triangulated functor, Parasitic ∩ LQCoh^fbc being a weak Serre subcategory on both sites. This includes the verification the source omits, that the equivalence of the middle arrow matches the complexes with parasitic cohomology sheaves.

theorem isEquivalence_epsilonPullbackDerivedParasiticSheafFlatBaseChange :
    (epsilonPullbackDerivedParasiticSheafFlatBaseChange B E h S hS 𝒳).IsEquivalence ∧
      (epsilonPullbackDerivedParasiticSheafFlatBaseChange B E h S hS 𝒳).IsTriangulated

AlgebraicGeometry.Stack.derivedCategoryQuasicoherentEtaleSheafFlatBaseChangeEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/SheafFlatBaseChangeEtaleFppfDerivedEquivalence.lean, line 364. The attribute's comment: “the last assertion: the induced equivalence D_{LQCoh^fbc}(𝒳_étale, 𝒪_𝒳) / D_{𝒫_𝒳}(𝒳_étale, 𝒪_𝒳) ≌ D_QCoh(𝒪_𝒳), for LQCoh^fbc with the flat base change property of Stacks 0762 read with the pullback of sheaves”.

Stacks 07B8, the last assertion: the equivalence

D_{LQCoh^fbc}(𝒳_étale, 𝒪_𝒳) / D_{𝒫_𝒳}(𝒳_étale, 𝒪_𝒳) ≌ D_QCoh(𝒪_𝒳)

induced by ε^*, where D_QCoh(𝒪_𝒳) is the Verdier quotient D_{LQCoh^fbc}(𝒪_𝒳) / D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳) of Stacks 07B6, AlgebraicGeometry.Stack.ParasiticQuotient.quotient. The middle vertical arrow is an equivalence matching the classes of morphisms the two Verdier quotients invert, because it matches the complexes with parasitic cohomology; see DerivedCategory.KernelColocalization.quotientEquivalenceOfExactFunctor. That it is induced by ε^* is toQuotientCompDerivedCategoryQuasicoherentEtaleSheafFlatBaseChangeEquivalenceIso.

def derivedCategoryQuasicoherentEtaleSheafFlatBaseChangeEquivalence :
    quotient (parasiticModules.{u, w, u} B S hS 𝒳 .etale)
        (locallyQuasicoherentSheafFlatBaseChangeEtaleModules B E h S hS 𝒳) ≌
      ParasiticQuotient.quotient B S hS 𝒳
        (lqcohSheafFbcFppfModules.{u, _, u} B E h S hS 𝒳)

Tag 07B9, a lemma

Tag 07B9 in the Stacks Project.

AlgebraicGeometry.Stack.FlatFppf.isZero_derivedModuleRestriction_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedFlatFppfRestriction.lean, line 288. The attribute's comment: “part (2)(b), the kernel of g^ on D_LQCoh^fbc(𝒪_𝒳): g^K = 0 exactly when K lies in D_(Parasitic ∩ LQCoh^fbc)(𝒪_𝒳), with g^* restriction to the flat-fppf site”.

Stacks 07B9 (2)(b). Let 𝒳 be an algebraic stack and set 𝒫_𝒳 = Parasitic(𝒪_𝒳) ∩ LQCoh^fbc(𝒪_𝒳). For a complex K of 𝒪_𝒳-modules lying in D_{LQCoh^fbc}(𝒪_𝒳), the restriction g^*K to the flat-fppf site of Stacks 0787 vanishes exactly when K lies in D_{𝒫_𝒳}(𝒪_𝒳).

Here g^* is restriction along the inclusion of the flat objects, which is pullback along the morphism of ringed topoi of Stacks 0788 (2) by Stacks 0788, flat_ringed, and which needs no derivation because it is exact. D_{𝒫_𝒳}(𝒪_𝒳) is AlgebraicGeometry.Stack.derivedParasiticLocallyQuasicoherentFlatBaseChange, the subcategory the Verdier quotient of Stacks 07B6 divides by.

The local quasi-coherence and flat base change half of the right-hand side is free given the hypothesis on K; the content is the parasitic half, which is AlgebraicGeometry.Stack.FlatFppf.isZero_derivedModuleRestriction_iff_forall_isParasitic.

theorem isZero_derivedModuleRestriction_iff {E : BigEtaleSite.{u}} {h : E.cutoff = B.cutoff}
    (K : DerivedCategory (fppfModules B S hS 𝒳))
    (hK : derivedLocallyQuasicoherentFlatBaseChange B E h S hS 𝒳 K) :
    IsZero ((derivedModuleRestriction B S hS 𝒳).obj K) ↔
      derivedParasiticLocallyQuasicoherentFlatBaseChange B E h S hS 𝒳 K

AlgebraicGeometry.Stack.FlatFppf.toDerivedCategoryQuasicoherentCompRestriction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedFlatFppfRestriction.lean, line 337. The attribute's comment: “part (2)(d), the functor c : D_QCoh(𝒪_𝒳) ⥤ D(𝒪_{𝒳_flat,fppf}) that g^* induces on the Verdier quotient of 07B6, together with its factorization through the quotient functor; the mutual inverseness of c with Lg_! is not covered”.

Stacks 07B9 (2)(d), the commutativity the functor c is characterized by: composing the quotient functor D_{LQCoh^fbc}(𝒪_𝒳) ⟶ D_QCoh(𝒪_𝒳) of Stacks 07B6 with c gives back restriction to the flat-fppf site. This is what pins c down; it is the "inner triangle commutes" of the source's proof.

def toDerivedCategoryQuasicoherentCompRestriction :
    toDerivedCategoryQuasicoherent B E h S hS 𝒳 ⋙
        derivedQuasicoherentModuleRestriction B S hS 𝒳 E h ≅
      (derivedLocallyQuasicoherentFlatBaseChange B E h S hS 𝒳).ι ⋙
        derivedModuleRestriction B S hS 𝒳

AlgebraicGeometry.Stack.FlatFppf.derivedCategoryB_derivedModuleLowerShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatFppfDerivedQuasicoherentLowerShriek.lean, line 68. The attribute's comment: “part (2)(c): Lg_! carries D_QCoh(𝒪_{𝒳_flat,fppf}) into D_LQCoh^fbc(𝒪_𝒳), for the derived lower shriek of Stacks 07AS (4) and LQCoh^fbc with the flat base change property of Stacks 0762 read with the pullback of sheaves, at module universe u, at the standard models of the derived categories”.

Stacks 07B9 (2)(c). Lg_! carries D_QCoh(𝒪_{𝒳_{flat,fppf}}) into D_{LQCoh^fbc}(𝒪_𝒳), the flat base change property of Stacks 0762 being read with the pullback of sheaves.

This is the dévissage of the source (AlgebraicGeometry.Stack.FlatFppf.derivedCategoryB_derivedModuleLowerShriek_of_single): Lg_! is triangulated, right t-exact and commutes with direct sums, LQCoh^fbc(𝒪_𝒳) is weak Serre and closed under colimits of sequences (Stacks 0771 (2), (5)), and on a quasi-coherent module in degree 0 it is Stacks 07B3 (2).

theorem derivedCategoryB_derivedModuleLowerShriek :
    letI := HasDerivedCategory.standard (fppfModules B S hS 𝒳)
    letI := HasDerivedCategory.standard (flatFppfModules B S hS 𝒳)
    ∀ H : DerivedCategory (flatFppfModules B S hS 𝒳),
      DerivedCategoryB.derivedCategoryB (flatQuasicoherentModules B S hS 𝒳) H →
        DerivedCategoryB.derivedCategoryB
          (lqcohSheafFbcFppfModules.{u, _, u} B E h S hS 𝒳)
          ((derivedModuleLowerShriek B S hS 𝒳).obj H)

AlgebraicGeometry.Stack.FlatFppf.derivedQuasicoherentEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatFppfDerivedQuasicoherentLowerShriek.lean, line 109. The attribute's comment: “part (2)(d): g^ and Lg_! define mutually inverse equivalences between D_QCoh(𝒪_𝒳), the Verdier quotient of Stacks 07B6, and D_QCoh(𝒪_{𝒳_flat,fppf}): the functor is induced by g^, the inverse is q ∘ Lg_!; for LQCoh^fbc with the flat base change property of Stacks 0762 read with the pullback of sheaves, at module universe u, at the standard models of the derived categories”.

Stacks 07B9 (2)(d). Restriction g^* to the flat-fppf site and Lg_! define mutually inverse equivalences between D_QCoh(𝒪_𝒳) — the Verdier quotient D_{LQCoh^fbc}(𝒪_𝒳) / D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳) of Stacks 07B6 — and D_QCoh(𝒪_{𝒳_{flat,fppf}}), the flat base change property of Stacks 0762 being read with the pullback of sheaves. The functor is the functor c induced by g^* (Stacks 07B9 (2)(a), (2)(b)), the inverse is q ∘ Lg_! (Stacks 07B9 (2)(c)); see AlgebraicGeometry.Stack.FlatFppf.derivedQuasicoherentEquivalenceOfSingle.

def derivedQuasicoherentEquivalence :
    letI := HasDerivedCategory.standard (fppfModules B S hS 𝒳)
    letI := HasDerivedCategory.standard (flatFppfModules B S hS 𝒳)
    ParasiticQuotient.quotient B S hS 𝒳
        (lqcohSheafFbcFppfModules.{u, _, u} B E h S hS 𝒳) ≌
      (DerivedCategoryB.derivedCategoryB (flatQuasicoherentModules B S hS 𝒳)).FullSubcategory

AlgebraicGeometry.Stack.FlatFppf.derivedCategoryB_derivedModuleRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatFppfDerivedQuasicoherentRestriction.lean, line 104. The attribute's comment: “part (2)(a): for K in D_LQCoh^fbc(𝒪_𝒳) the restriction g^*K to the flat-fppf site lies in D_QCoh(𝒪_{𝒳_flat,fppf}), for LQCoh^fbc with the flat base change property of Stacks 0762 read with the pullback of sheaves, at module universe u, for any models of the derived categories”.

Stacks 07B9 (2)(a). For K in D_{LQCoh^fbc}(𝒪_𝒳) (with the flat base change property of Stacks 0762 read with the pullback of sheaves), the restriction g^*K to the flat-fppf site lies in D_QCoh(𝒪_{𝒳_{flat,fppf}}): g^* is exact, so H^n(g^*K) = g^*H^n(K), which is quasi-coherent by Stacks 07B1 (2)(b).

theorem derivedCategoryB_derivedModuleRestriction (K : DerivedCategory (fppfModules B S hS 𝒳))
    (hK : DerivedCategoryB.derivedCategoryB
      (lqcohSheafFbcFppfModules.{u, _, u} B E h S hS 𝒳) K) :
    DerivedCategoryB.derivedCategoryB (flatQuasicoherentModules B S hS 𝒳)
      ((derivedModuleRestriction B S hS 𝒳).obj K)

AlgebraicGeometry.Stack.FlatFppf.isZero_derivedModuleRestriction_iff_derivedParasitic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatFppfDerivedQuasicoherentRestriction.lean, line 122. The attribute's comment: “part (2)(b): for K in D_LQCoh^fbc(𝒪_𝒳), g^*K = 0 if and only if K lies in D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳), for LQCoh^fbc with the flat base change property of Stacks 0762 read with the pullback of sheaves, at module universe u, for any models of the derived categories”.

For K in D_{LQCoh^fbc}(𝒪_𝒳) (with the flat base change property of Stacks 0762 read with the pullback of sheaves), g^*K = 0 exactly when K lies in D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳): g^*K = 0 exactly when every cohomology module of K is parasitic (isZero_derivedModuleRestriction_iff_forall_isParasitic, Stacks 07AR), and the LQCoh^fbc half is the hypothesis on K.

theorem isZero_derivedModuleRestriction_iff_derivedParasitic
    (K : DerivedCategory (fppfModules B S hS 𝒳))
    (hK : DerivedCategoryB.derivedCategoryB
      (lqcohSheafFbcFppfModules.{u, _, u} B E h S hS 𝒳) K) :
    IsZero ((derivedModuleRestriction B S hS 𝒳).obj K) ↔
      ParasiticQuotient.derivedParasitic B S hS 𝒳
        (lqcohSheafFbcFppfModules.{u, _, u} B E h S hS 𝒳) K

AlgebraicGeometry.Stack.LisseEtale.derivedQuasicoherentEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LisseEtaleDerivedQuasicoherentEquivalence.lean, line 122. The attribute's comment: “part (1)(d): g^ and Lg_! define mutually inverse equivalences between D_QCoh(𝒪_𝒳), the Verdier quotient of Stacks 07B6, and D_QCoh(𝒪_{𝒳_lisse,étale}), through the equivalence of Stacks 07B8; the inverse is q ∘ ε^ ∘ Lg_! (derivedQuasicoherentEquivalenceInverseIso); for LQCoh^fbc with the flat base change property of Stacks 0762 read with the pullback of sheaves, at module universe u, at the standard models of the derived categories”.

Stacks 07B9 (1)(d). Restriction g^* to the lisse-étale site and Lg_! define mutually inverse equivalences between D_QCoh(𝒪_𝒳) — the Verdier quotient D_{LQCoh^fbc}(𝒪_𝒳) / D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳) of Stacks 07B6 — and D_QCoh(𝒪_{𝒳_{lisse,étale}}), the flat base change property of Stacks 0762 being read with the pullback of sheaves.

As in the source, D_QCoh(𝒪_𝒳) is identified with D_{LQCoh^fbc}(𝒳_étale, 𝒪_𝒳) / D_{𝒫_𝒳}(𝒳_étale, 𝒪_𝒳) by Stacks 07B8 (AlgebraicGeometry.Stack.derivedCategoryQuasicoherentEtaleSheafFlatBaseChangeEquivalence, induced by ε^*), and on that quotient g^* and q ∘ Lg_! are mutually inverse (AlgebraicGeometry.Stack.LisseEtale.etaleQuotientDerivedQuasicoherentEquivalence). Stated at the standard models of the derived categories, where Stacks 07B3 (1) is.

def derivedQuasicoherentEquivalence :
    letI := HasDerivedCategory.standard (fppfModules B S hS 𝒳)
    letI := HasDerivedCategory.standard (SheafOfModules.{u} (lisseEtaleModuleRing B S hS 𝒳))
    ParasiticQuotient.quotient B S hS 𝒳
        (lqcohSheafFbcFppfModules.{u, _, u} B E h S hS 𝒳) ≌
      (DerivedCategoryB.derivedCategoryB (lisseQuasicoherentModules B S hS 𝒳)).FullSubcategory

AlgebraicGeometry.Stack.LisseEtale.derivedCategoryB_derivedModuleRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LisseEtaleDerivedQuasicoherentRestriction.lean, line 200. The attribute's comment: “part (1)(a): for F in D_LQCoh^fbc(𝒳_étale, 𝒪_𝒳) the restriction g^*F to the lisse-étale site lies in D_QCoh(𝒪_{𝒳_lisse,étale}), for LQCoh^fbc with the flat base change property of Stacks 0762 read with the pullback of sheaves, at module universe u, for any models of the derived categories”.

Stacks 07B9 (1)(a). For K in D_{LQCoh^fbc}(𝒳_étale, 𝒪_𝒳) (with the flat base change property of Stacks 0762 read with the pullback of sheaves), g^*K lies in D_QCoh(𝒪_{𝒳_{lisse,étale}}): H^n(g^*K) = g^*H^n(K) is quasi-coherent by Stacks 07B1 (1)(b).

theorem derivedCategoryB_derivedModuleRestriction
    (K : DerivedCategory (etaleModules B S hS 𝒳))
    (hK : DerivedCategoryB.derivedCategoryB
      (locallyQuasicoherentSheafFlatBaseChangeEtaleModules B E h S hS 𝒳) K) :
    DerivedCategoryB.derivedCategoryB (lisseQuasicoherentModules B S hS 𝒳)
      ((derivedModuleRestriction B S hS 𝒳).obj K)

AlgebraicGeometry.Stack.LisseEtale.isZero_derivedModuleRestriction_iff_derivedParasitic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LisseEtaleDerivedQuasicoherentRestriction.lean, line 216. The attribute's comment: “part (1)(b): for F in D_LQCoh^fbc(𝒳_étale, 𝒪_𝒳), g^*F = 0 if and only if F lies in D_{𝒫_𝒳}(𝒳_étale, 𝒪_𝒳), 𝒫_𝒳 = Parasitic ∩ LQCoh^fbc, for LQCoh^fbc with the flat base change property of Stacks 0762 read with the pullback of sheaves, at module universe u, for any models of the derived categories”.

Stacks 07B9 (1)(b). For K in D_{LQCoh^fbc}(𝒳_étale, 𝒪_𝒳), g^*K = 0 exactly when K lies in D_{Parasitic ∩ LQCoh^fbc}(𝒳_étale, 𝒪_𝒳).

theorem isZero_derivedModuleRestriction_iff_derivedParasitic
    (K : DerivedCategory (etaleModules B S hS 𝒳))
    (hK : DerivedCategoryB.derivedCategoryB
      (locallyQuasicoherentSheafFlatBaseChangeEtaleModules B E h S hS 𝒳) K) :
    IsZero ((derivedModuleRestriction B S hS 𝒳).obj K) ↔
      DerivedCategory.KernelColocalization.derivedInter (parasiticModules.{u, w, u} B S hS 𝒳 .etale)
        (locallyQuasicoherentSheafFlatBaseChangeEtaleModules B E h S hS 𝒳) K

AlgebraicGeometry.Stack.LisseEtale.derivedCategoryB_derivedModuleLowerShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LisseEtaleDerivedQuasicoherentRestriction.lean, line 280. The attribute's comment: “part (1)(c): Lg_! carries D_QCoh(𝒪_{𝒳_lisse,étale}) into D_LQCoh^fbc(𝒳_étale, 𝒪_𝒳), for the derived lower shriek of Stacks 07AS (2) and LQCoh^fbc with the flat base change property of Stacks 0762 read with the pullback of sheaves, at module universe u, at the standard models of the derived categories”.

Stacks 07B9 (1)(c). Lg_! carries D_QCoh(𝒪_{𝒳_{lisse,étale}}) into D_{LQCoh^fbc}(𝒳_étale, 𝒪_𝒳), the flat base change property of Stacks 0762 being read with the pullback of sheaves.

This is the dévissage of the source (DerivedCategory.derivedCategoryB_obj_of_isLE_obj): Lg_! is triangulated, right t-exact (its right adjoint g^* is exact) and commutes with direct sums; LQCoh^fbc is a weak Serre subcategory closed under colimits of sequences (Stacks 0771 (2), (5)); and on a quasi-coherent module in degree 0 it is Stacks 07B3 (1) (isLocallyQuasicoherentWithSheafFlatBaseChange_homology_derivedModuleLowerShriek). It is stated at the standard models of the derived categories, where Stacks 07B3 (1) is.

theorem derivedCategoryB_derivedModuleLowerShriek :
    letI := HasDerivedCategory.standard (SheafOfModules.{u} (lisseEtaleModuleRing B S hS 𝒳))
    letI := HasDerivedCategory.standard (SheafOfModules.{u} (lisseAmbientRing B S hS 𝒳))
    ∀ H : DerivedCategory (SheafOfModules.{u} (lisseEtaleModuleRing B S hS 𝒳)),
      DerivedCategoryB.derivedCategoryB (lisseQuasicoherentModules B S hS 𝒳) H →
        DerivedCategoryB.derivedCategoryB
          (fun F : SheafOfModules.{u} (lisseAmbientRing B S hS 𝒳) =>
            IsLocallyQuasicoherentWithSheafFlatBaseChange.{u, u + 1, u, u} B E h S hS
              𝒳.val.val.p 𝒳.val.isFiberedInGroupoids F.val)
          ((derivedModuleLowerShriek B S hS 𝒳).obj H)

Tag 07BA, a lemma

Tag 07BA in the Stacks Project.

AlgebraicGeometry.Stack.FlatFppf.leftOrthogonal_parasiticFreePart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/ParasiticColocalizationTriangle.lean, line 199. The attribute's comment: “the orthogonality: Hom_D(𝒪_𝒳)(E', P') = 0 for every P' in D_(Parasitic ∩ LQCoh^fbc)(𝒪_𝒳), at E' = Lg_! g^* E; conditional on the derived module-level Lg_! of 07AS (4), carried as the hypotheses Lsh and adj”.

Stacks 07BA, the orthogonality of the first term. Every morphism from K' = Lg_! g^* K to an object P' of D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳) vanishes, i.e. K' lies in the left orthogonal of D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳).

Indeed Hom(Lg_! g^* K, P') = Hom(g^* K, g^* P') by the adjunction, and g^* P' = 0 by Stacks 07B9 (2)(b), so the right-hand group vanishes.

theorem leftOrthogonal_parasiticFreePart (K : DerivedCategory (fppfModules B S hS 𝒳)) :
    (derivedParasiticLocallyQuasicoherentFlatBaseChange B E h S hS 𝒳).leftOrthogonal
      (parasiticFreePart B S hS 𝒳 Lsh K)

AlgebraicGeometry.Stack.FlatFppf.derivedParasitic_obj₃_of_distTriang_parasiticFreePartHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/ParasiticColocalizationTriangle.lean, line 225. The attribute's comment: “the cone: for E' = Lg_! g^* E and E' ⟶ E the counit, every distinguished triangle E' ⟶ E ⟶ P ⟶ E'[1] has P in D_(Parasitic ∩ LQCoh^fbc)(𝒪_𝒳), and all three terms in D_LQCoh^fbc(𝒪_𝒳); conditional on the derived module-level Lg_! of 07AS (4) and on 07B9 (2)(a), (2)(c), carried as the hypotheses Lsh, adj, hunit and hK'”.

Stacks 07BA, the third term of the triangle. Let K be an object of D_{LQCoh^fbc}(𝒪_𝒳) whose parasitic-free part K' = Lg_! g^* K again lies in D_{LQCoh^fbc}(𝒪_𝒳) — that is Stacks 07B9 (2)(a) followed by (2)(c), carried as the hypothesis hK'. Then every cone P on the canonical morphism ε_K : K' ⟶ K lies in D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳).

Local quasi-coherence with flat base change is two out of three in the triangle. For the parasitic half, g^* is exact hence triangulated, and it inverts ε_K, so the third term of the image triangle vanishes: g^* P = 0, which is the parasitic condition by Stacks 07B9 (2)(b).

theorem derivedParasitic_obj₃_of_distTriang_parasiticFreePartHom (hunit : IsIso adj.unit)
    (K : DerivedCategory (fppfModules B S hS 𝒳))
    (hK : derivedLocallyQuasicoherentFlatBaseChange B E h S hS 𝒳 K)
    (hK' : derivedLocallyQuasicoherentFlatBaseChange B E h S hS 𝒳
      (parasiticFreePart B S hS 𝒳 Lsh K))
    (P : DerivedCategory (fppfModules B S hS 𝒳)) (b : K ⟶ P)
    (c : P ⟶ (parasiticFreePart B S hS 𝒳 Lsh K)⟦(1 : ℤ)⟧)
    (hT : Triangle.mk (parasiticFreePartHom B S hS 𝒳 Lsh adj K) b c ∈
      distTriang (DerivedCategory (fppfModules B S hS 𝒳))) :
    derivedParasiticLocallyQuasicoherentFlatBaseChange B E h S hS 𝒳 P

AlgebraicGeometry.Stack.FlatFppf.extensionProduct_parasiticFreePart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/ParasiticColocalizationTriangle.lean, line 260. The attribute's comment: “the existence of the triangle: every E in D_LQCoh^fbc(𝒪_𝒳) is an extension of an object of D_(Parasitic ∩ LQCoh^fbc)(𝒪_𝒳) by an object of D_LQCoh^fbc(𝒪_𝒳) left orthogonal to it, the extension being the canonical one on Lg_! g^* E ⟶ E; conditional on the derived module-level Lg_! of 07AS (4) and on 07B9 (2)(a), (2)(c)”.

Stacks 07BA, in the shape the source states it. Every object K of D_{LQCoh^fbc}(𝒪_𝒳) whose parasitic-free part lies in D_{LQCoh^fbc}(𝒪_𝒳) fits in a distinguished triangle

K' ⟶ K ⟶ P ⟶ K'[1]

with P in D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳) and K' in D_{LQCoh^fbc}(𝒪_𝒳) and left orthogonal to D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳).

This is the existential reading of the two statements above, obtained by completing the canonical morphism ε_K to a distinguished triangle; K' and ε_K themselves are the AlgebraicGeometry.Stack.FlatFppf.parasiticFreePart and AlgebraicGeometry.Stack.FlatFppf.parasiticFreePartHom of the canonical triangle.

theorem extensionProduct_parasiticFreePart (hunit : IsIso adj.unit)
    (K : DerivedCategory (fppfModules B S hS 𝒳))
    (hK : derivedLocallyQuasicoherentFlatBaseChange B E h S hS 𝒳 K)
    (hK' : derivedLocallyQuasicoherentFlatBaseChange B E h S hS 𝒳
      (parasiticFreePart B S hS 𝒳 Lsh K)) :
    (((derivedParasiticLocallyQuasicoherentFlatBaseChange B E h S hS 𝒳).leftOrthogonal ⊓
        derivedLocallyQuasicoherentFlatBaseChange B E h S hS 𝒳).extensionProduct
      (derivedParasiticLocallyQuasicoherentFlatBaseChange B E h S hS 𝒳)) K

AlgebraicGeometry.Stack.FlatFppf.leftOrthogonal_sheafParasiticFreePart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/SheafFlatBaseChangeParasiticColocalization.lean, line 108. The attribute's comment: “the orthogonality: Hom_D(𝒪_𝒳)(E', P') = 0 for every P' in D_(Parasitic ∩ LQCoh^fbc)(𝒪_𝒳), at E' = Lg_! g^* E, for the faithful class LQCoh^fbc of Stacks 0762 (flat base change read with the pullback of sheaves), the actual derived lower shriek Lg_! of Stacks 07AS (4) and any models of the derived categories, with no hypothesis”.

Stacks 07BA, the orthogonality: Hom(Lg_! g^* E, P') = Hom(g^* E, g^* P') = 0 for every P' in D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳).

theorem leftOrthogonal_sheafParasiticFreePart (K : DerivedCategory (fppfModules B S hS 𝒳)) :
    (ParasiticQuotient.derivedParasitic B S hS 𝒳
      (lqcohSheafFbcFppfModules.{u, _, u} B E h S hS 𝒳)).leftOrthogonal
      (sheafParasiticFreePart B S hS 𝒳 K)

AlgebraicGeometry.Stack.FlatFppf.exists_iso_sheafParasiticColocalizationTriangle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/SheafFlatBaseChangeParasiticColocalization.lean, line 197. The attribute's comment: “the canonicity of the triangle: a distinguished triangle E'' ⟶ E ⟶ P'' ⟶ E''[1] with E'' left orthogonal to D_(Parasitic ∩ LQCoh^fbc)(𝒪_𝒳) and P'' in it is isomorphic to the triangle on Lg_! g^* E ⟶ E by an isomorphism which is the identity on E (Stacks 0CQP), for the faithful class LQCoh^fbc, any models of the derived categories, with no hypothesis”.

Stacks 07BA, canonicity ([Stacks, Tag 0CQP]): a distinguished triangle E'' ⟶ E ⟶ P'' ⟶ E''[1] with E'' left orthogonal to D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳) and P'' in it is isomorphic to any distinguished triangle on the canonical morphism Lg_! g^* E ⟶ E whose third term lies in D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳), by an isomorphism of triangles which is the identity on E.

theorem exists_iso_sheafParasiticColocalizationTriangle
    (K : DerivedCategory (fppfModules B S hS 𝒳))
    (P : DerivedCategory (fppfModules B S hS 𝒳)) (b : K ⟶ P)
    (c : P ⟶ (sheafParasiticFreePart B S hS 𝒳 K)⟦(1 : ℤ)⟧)
    (hT : Triangle.mk (sheafParasiticFreePartHom B S hS 𝒳 K) b c ∈
      distTriang (DerivedCategory (fppfModules B S hS 𝒳)))
    (hP : ParasiticQuotient.derivedParasitic B S hS 𝒳
      (lqcohSheafFbcFppfModules.{u, _, u} B E h S hS 𝒳) P)
    {E'' P'' : DerivedCategory (fppfModules B S hS 𝒳)} (f'' : E'' ⟶ K) (g'' : K ⟶ P'')
    (h'' : P'' ⟶ E''⟦(1 : ℤ)⟧)
    (hT'' : Triangle.mk f'' g'' h'' ∈ distTriang (DerivedCategory (fppfModules B S hS 𝒳)))
    (hE'' : (ParasiticQuotient.derivedParasitic B S hS 𝒳
      (lqcohSheafFbcFppfModules.{u, _, u} B E h S hS 𝒳)).leftOrthogonal E'')
    (hP'' : ParasiticQuotient.derivedParasitic B S hS 𝒳
      (lqcohSheafFbcFppfModules.{u, _, u} B E h S hS 𝒳) P'') :
    ∃ e : Triangle.mk (sheafParasiticFreePartHom B S hS 𝒳 K) b c ≅ Triangle.mk f'' g'' h'',
      e.hom.hom₂ = 𝟙 K

AlgebraicGeometry.Stack.FlatFppf.derivedParasitic_obj₃_of_distTriang_sheafParasiticFreePartHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/SheafFlatBaseChangeParasiticColocalization.lean, line 235. The attribute's comment: “the cone: for E' = Lg_! g^ E and E' ⟶ E the counit of Lg_! ⊣ g^, every distinguished triangle E' ⟶ E ⟶ P ⟶ E'[1] with E in D_LQCoh^fbc(𝒪_𝒳) has P in D_(Parasitic ∩ LQCoh^fbc)(𝒪_𝒳), for the faithful class LQCoh^fbc of Stacks 0762 and the actual derived lower shriek of Stacks 07AS (4) at the standard models of the derived categories, with no hypothesis (Stacks 07B9 (2)(a), (2)(c) and 07B3 (2) are proved, not assumed)”.

Stacks 07BA, the cone: for E in D_{LQCoh^fbc}(𝒪_𝒳), every cone P on the canonical morphism Lg_! g^* E ⟶ E lies in D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳).

theorem derivedParasitic_obj₃_of_distTriang_sheafParasiticFreePartHom :
    letI := HasDerivedCategory.standard (fppfModules B S hS 𝒳)
    letI := HasDerivedCategory.standard (flatFppfModules B S hS 𝒳)
    ∀ (K : DerivedCategory (fppfModules B S hS 𝒳)),
      DerivedCategoryB.derivedCategoryB
        (lqcohSheafFbcFppfModules.{u, _, u} B E h S hS 𝒳) K →
      ∀ (P : DerivedCategory (fppfModules B S hS 𝒳)) (b : K ⟶ P)
        (c : P ⟶ (sheafParasiticFreePart B S hS 𝒳 K)⟦(1 : ℤ)⟧),
        Triangle.mk (sheafParasiticFreePartHom B S hS 𝒳 K) b c ∈
          distTriang (DerivedCategory (fppfModules B S hS 𝒳)) →
        ParasiticQuotient.derivedParasitic B S hS 𝒳
          (lqcohSheafFbcFppfModules.{u, _, u} B E h S hS 𝒳) P

AlgebraicGeometry.Stack.FlatFppf.exists_sheafParasiticColocalizationTriangle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/SheafFlatBaseChangeParasiticColocalization.lean, line 262. The attribute's comment: “the existence of the triangle: every E in D_LQCoh^fbc(𝒪_𝒳) sits in a distinguished triangle E' ⟶ E ⟶ P ⟶ E'[1] with E' = Lg_! g^* E and E' ⟶ E the counit, E' and P in D_LQCoh^fbc(𝒪_𝒳), P in D_(Parasitic ∩ LQCoh^fbc)(𝒪_𝒳) and Hom(E', P') = 0 for every P' in D_(Parasitic ∩ LQCoh^fbc)(𝒪_𝒳), for the faithful class LQCoh^fbc of Stacks 0762 and the actual derived lower shriek of Stacks 07AS (4) at the standard models of the derived categories, with no hypothesis”.

Stacks 07BA: every E in D_{LQCoh^fbc}(𝒪_𝒳) sits in a distinguished triangle E' ⟶ E ⟶ P ⟶ E'[1] of D_{LQCoh^fbc}(𝒪_𝒳), E' ⟶ E the canonical morphism Lg_! g^* E ⟶ E, with P in D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳) and E' left orthogonal to D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳).

theorem exists_sheafParasiticColocalizationTriangle :
    letI := HasDerivedCategory.standard (fppfModules B S hS 𝒳)
    letI := HasDerivedCategory.standard (flatFppfModules B S hS 𝒳)
    ∀ (K : DerivedCategory (fppfModules B S hS 𝒳)),
      DerivedCategoryB.derivedCategoryB
        (lqcohSheafFbcFppfModules.{u, _, u} B E h S hS 𝒳) K →
      ∃ (P : DerivedCategory (fppfModules B S hS 𝒳)) (b : K ⟶ P)
        (c : P ⟶ (sheafParasiticFreePart B S hS 𝒳 K)⟦(1 : ℤ)⟧),
        Triangle.mk (sheafParasiticFreePartHom B S hS 𝒳 K) b c ∈
            distTriang (DerivedCategory (fppfModules B S hS 𝒳)) ∧
          DerivedCategoryB.derivedCategoryB
            (lqcohSheafFbcFppfModules.{u, _, u} B E h S hS 𝒳)
            (sheafParasiticFreePart B S hS 𝒳 K) ∧
          DerivedCategoryB.derivedCategoryB
            (lqcohSheafFbcFppfModules.{u, _, u} B E h S hS 𝒳) P ∧
          ParasiticQuotient.derivedParasitic B S hS 𝒳
            (lqcohSheafFbcFppfModules.{u, _, u} B E h S hS 𝒳) P ∧
          (ParasiticQuotient.derivedParasitic B S hS 𝒳
            (lqcohSheafFbcFppfModules.{u, _, u} B E h S hS 𝒳)).leftOrthogonal
            (sheafParasiticFreePart B S hS 𝒳 K)

AlgebraicGeometry.Stack.FlatFppf.hasColocalizations_locallyQuasicoherentSheafFlatBaseChangeFppfModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/SheafFlatBaseChangeParasiticColocalization.lean, line 294. The attribute's comment: “the triangle as the colocalization of D_LQCoh^fbc(𝒪_𝒳) by D_(Parasitic ∩ LQCoh^fbc)(𝒪_𝒳): every object receives Lg_! g^* E ⟶ E, a morphism with cone in D_(Parasitic ∩ LQCoh^fbc)(𝒪_𝒳) out of an object left orthogonal to it, for the faithful class LQCoh^fbc and the actual Lg_! at the standard models of the derived categories, with no hypothesis”.

Stacks 07BA, in the form of the colocalization hypothesis of the Verdier quotient D_{LQCoh^fbc}(𝒪_𝒳) / D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳) (D_QCoh(𝒪_𝒳) of Stacks 07B6).

theorem hasColocalizations_locallyQuasicoherentSheafFlatBaseChangeFppfModules :
    letI := HasDerivedCategory.standard (fppfModules B S hS 𝒳)
    DerivedCategoryB.HasColocalizations
      (lqcohSheafFbcFppfModules.{u, _, u} B E h S hS 𝒳)
      (ParasiticQuotient.parasitic B S hS 𝒳 ⊓
        lqcohSheafFbcFppfModules.{u, _, u} B E h S hS 𝒳)

Tag 0H11, a remark

Tag 0H11 in the Stacks Project.

AlgebraicGeometry.Stack.isSaturated_derivedParasiticFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedQuasicoherentAdmissibility.lean, line 343. The attribute's comment: “the last assertion for D(𝒳_fppf, 𝒪_𝒳): 𝒜, hence D_QCoh(𝒪_𝒳), read inside D(𝒳_fppf, 𝒪_𝒳) is a strictly full saturated triangulated subcategory there”.

Stacks 0H11, last assertion, inside D(𝒳_{fppf}, 𝒪_𝒳). The subcategory 𝒜 read in D(𝒳_{fppf}, 𝒪_𝒳), that is the locally quasi-coherent complexes with flat base change which are left orthogonal to the parasitic ones, is a strictly full, saturated ([Stacks, Tag 05RB]), triangulated subcategory of D(𝒳_{fppf}, 𝒪_𝒳).

Strict fullness and triangulatedness are those of a left orthogonal ([Stacks, Tag 0FXC] and [Stacks, Tag 0CQR]) intersected with D_{LQCoh^fbc}(𝒪_𝒳), and saturation is stability under retracts of a left orthogonal, again [Stacks, Tag 0FXC], intersected with the carried stability under retracts of D_{LQCoh^fbc}(𝒪_𝒳).

theorem isSaturated_derivedParasiticFree :
    (derivedParasiticFree B E h S hS 𝒳).IsClosedUnderIsomorphisms ∧
      (derivedParasiticFree B E h S hS 𝒳).IsSaturated ∧
      (derivedParasiticFree B E h S hS 𝒳).IsTriangulated

AlgebraicGeometry.Stack.parasiticInLQCoh_isLeftAdmissible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentSemiorthogonalDecomposition.lean, line 143. The attribute's comment: “the first assertion: D_(Parasitic ∩ LQCoh^fbc)(𝒪_𝒳) ⊂ D_LQCoh^fbc(𝒪_𝒳) is a left admissible subcategory”.

Stacks 0H11, first assertion. The subcategory D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳) ⊂ D_{LQCoh^fbc}(𝒪_𝒳) is left admissible: a strictly full triangulated subcategory whose inclusion has a left adjoint.

theorem parasiticInLQCoh_isLeftAdmissible :
    letI := HasDerivedCategory.standard (fppfModules B S hS 𝒳)
    (ParasiticQuotient.parasiticIn B S hS 𝒳
      (𝓛 B E h S hS 𝒳)).IsLeftAdmissible

AlgebraicGeometry.Stack.parasiticFreeInLQCoh_isRightAdmissible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentSemiorthogonalDecomposition.lean, line 154. The attribute's comment: “the second assertion: the left orthogonal 𝒜 of D_(Parasitic ∩ LQCoh^fbc)(𝒪_𝒳) is right admissible in D_LQCoh^fbc(𝒪_𝒳)”.

Stacks 0H11, second assertion. The left orthogonal 𝒜 of D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳) in D_{LQCoh^fbc}(𝒪_𝒳) is right admissible: a strictly full triangulated subcategory whose inclusion has a right adjoint.

theorem parasiticFreeInLQCoh_isRightAdmissible :
    letI := HasDerivedCategory.standard (fppfModules B S hS 𝒳)
    (ParasiticQuotient.parasiticFreeIn B S hS 𝒳
      (𝓛 B E h S hS 𝒳)).IsRightAdmissible

AlgebraicGeometry.Stack.parasiticFreeInLQCoh_ι_comp_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentSemiorthogonalDecomposition.lean, line 177. The attribute's comment: “the third assertion: the composition 𝒜 ⟶ D_LQCoh^fbc(𝒪_𝒳) ⟶ D_QCoh(𝒪_𝒳) of the inclusion with the Verdier quotient functor of 07B6 is an equivalence”.

Stacks 0H11, third assertion. The composition

𝒜 ⟶ D_{LQCoh^fbc}(𝒪_𝒳) ⟶ D_QCoh(𝒪_𝒳)

of the inclusion of the left orthogonal 𝒜 with the Verdier quotient functor of Stacks 07B6 is an equivalence of categories.

theorem parasiticFreeInLQCoh_ι_comp_isEquivalence :
    letI := HasDerivedCategory.standard (fppfModules B S hS 𝒳)
    ((ParasiticQuotient.parasiticFreeIn B S hS 𝒳
        (𝓛 B E h S hS 𝒳)).ι ⋙
      ParasiticQuotient.toQuotient B S hS 𝒳
        (𝓛 B E h S hS 𝒳)).IsEquivalence

AlgebraicGeometry.Stack.parasiticFreeInLQCoh_isSaturated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentSemiorthogonalDecomposition.lean, line 191. The attribute's comment: “the last assertion for D_LQCoh^fbc(𝒪_𝒳): 𝒜, hence D_QCoh(𝒪_𝒳), is a strictly full saturated triangulated subcategory of D_LQCoh^fbc(𝒪_𝒳)”.

Stacks 0H11, last assertion, inside D_{LQCoh^fbc}(𝒪_𝒳). The left orthogonal 𝒜, which AlgebraicGeometry.Stack.parasiticFreeInLQCoh_ι_comp_isEquivalence identifies with D_QCoh(𝒪_𝒳), is a strictly full, saturated ([Stacks, Tag 05RB]), triangulated subcategory of D_{LQCoh^fbc}(𝒪_𝒳).

theorem parasiticFreeInLQCoh_isSaturated :
    letI := HasDerivedCategory.standard (fppfModules B S hS 𝒳)
    (ParasiticQuotient.parasiticFreeIn B S hS 𝒳
        (𝓛 B E h S hS 𝒳)).IsClosedUnderIsomorphisms ∧
      (ParasiticQuotient.parasiticFreeIn B S hS 𝒳
        (𝓛 B E h S hS 𝒳)).IsSaturated ∧
      (ParasiticQuotient.parasiticFreeIn B S hS 𝒳
        (𝓛 B E h S hS 𝒳)).IsTriangulated

AlgebraicGeometry.Stack.parasiticFreeInDerivedFppf_isSaturated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentSemiorthogonalDecomposition.lean, line 211. The attribute's comment: “the last assertion for D(𝒳_fppf, 𝒪_𝒳): 𝒜, hence D_QCoh(𝒪_𝒳), read inside D(𝒳_fppf, 𝒪_𝒳) is a strictly full saturated triangulated subcategory there”.

Stacks 0H11, last assertion, inside D(𝒳_{fppf}, 𝒪_𝒳). The subcategory 𝒜 read in D(𝒳_{fppf}, 𝒪_𝒳) — the complexes with cohomology in LQCoh^fbc(𝒪_𝒳) admitting no nonzero morphism to D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳) — is a strictly full, saturated, triangulated subcategory of D(𝒳_{fppf}, 𝒪_𝒳).

theorem parasiticFreeInDerivedFppf_isSaturated [HasDerivedCategory (fppfModules B S hS 𝒳)] :
    (ParasiticQuotient.parasiticFree B S hS 𝒳
        (𝓛 B E h S hS 𝒳)).IsClosedUnderIsomorphisms ∧
      (ParasiticQuotient.parasiticFree B S hS 𝒳
        (𝓛 B E h S hS 𝒳)).IsSaturated ∧
      (ParasiticQuotient.parasiticFree B S hS 𝒳
        (𝓛 B E h S hS 𝒳)).IsTriangulated

AlgebraicGeometry.Stack.parasiticFreeToLQCoh_comp_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentSemiorthogonalDecomposition.lean, line 226. The attribute's comment: “the embedding into D(𝒳_fppf, 𝒪_𝒳): the composition of the inclusion of 𝒜, presented as a subcategory of D(𝒳_fppf, 𝒪_𝒳), with the Verdier quotient functor of 07B6 is an equivalence”.

Stacks 0H11, the realization of D_QCoh(𝒪_𝒳) inside D(𝒳_{fppf}, 𝒪_𝒳): the inclusion of 𝒜, presented as a subcategory of D(𝒳_{fppf}, 𝒪_𝒳), followed by the Verdier quotient functor of Stacks 07B6 is an equivalence.

theorem parasiticFreeToLQCoh_comp_isEquivalence :
    letI := HasDerivedCategory.standard (fppfModules B S hS 𝒳)
    (ParasiticQuotient.parasiticFreeToClass B S hS 𝒳
        (𝓛 B E h S hS 𝒳) ⋙
      ParasiticQuotient.toQuotient B S hS 𝒳
        (𝓛 B E h S hS 𝒳)).IsEquivalence

Sources

• Section 104.5, Tag 07B5
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.derivedCategoryQuasicoherent · AlgebraicGeometry.Stack.toDerivedCategoryQuasicoherent · AlgebraicGeometry.Stack.derivedCategoryQuasicoherentSheaf · AlgebraicGeometry.Stack.toDerivedCategoryQuasicoherentSheaf · AlgebraicGeometry.Stack.cohomologyDerivedCategoryQuasicoherent · AlgebraicGeometry.Stack.cohomologyDerivedCategoryQuasicoherentFac · AlgebraicGeometry.Stack.cohomologyDerivedCategoryQuasicoherentSheaf · AlgebraicGeometry.Stack.cohomologyDerivedCategoryQuasicoherentSheafFac

Section104.6 Derived pushforward of quasi-coherent modules#

Section 104.6 of the Stacks Project, Tag 07BB. 1 tag here is carried by 18 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07BC, a proposition

Tag 07BC in the Stacks Project.

AlgebraicGeometry.Stack.derivedPushforwardQuasicoherentPlus_comp_plusCohomology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedPushforwardCohomologyComparison.lean, line 211. The attribute's comment: “the final assertion of the tag: the functors Rⁱf_QCoh of Stacks 077A are Hⁱ ∘ Rf_(QCoh,), read as the identification of Q_𝒳 ⋙ Rf_(QCoh,) ⋙ Hⁱ with Rf_*^LQCoh ⋙ (Q ∘ Hⁱ) over the defining identity (104.5.1.1) of Hⁱ, at the module universe u + 1 that the derived direct image of Stacks 06WE on an algebraic stack lives in”.

Stacks 07BC, the final assertion. For a quasi-compact and quasi-separated 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks, the cohomology functor Hⁱ of Stacks 07B7 composed with the induced functor Rf_{QCoh,*} : D⁺_QCoh(𝒪_𝒳) ⥤ D⁺_QCoh(𝒪_𝒴) is the higher direct image of Stacks 077A: precomposed with the quotient functor of 𝒳 it is the middle vertical functor Rf_*^{LQCoh} of the diagram of Stacks 07BC followed by Q ∘ Hⁱ, which is Q ∘ Rⁱf_*.

Hⁱ is taken here as any functor on D⁺_QCoh(𝒪_𝒴) equipped with the defining identity α (104.5.1.1); AlgebraicGeometry.Stack.plusCohomologyDerivedCategoryQuasicoherent is one.

def derivedPushforwardQuasicoherentPlus_comp_plusCohomology (i : ℤ)
    (H : derivedCategoryQuasicoherentPlus B E h S hS 𝒴 ⥤
      AlgebraicStacks.fppfQuasicoherentModules B S hS 𝒴)
    (α : toDerivedCategoryQuasicoherentPlus B E h S hS 𝒴 ⋙ H ≅
      plusCohomologyQuasicoherent B E h S hS 𝒴 hclosed hwp hsep i) :
    toDerivedCategoryQuasicoherentPlus B E h S hS 𝒳 ⋙
        derivedPushforwardQuasicoherentPlus B E h S hS f hf hdist hpar ⋙ H ≅
      derivedPushforwardPlusLocallyQuasicoherentFlatBaseChange B E h S hS f hf ⋙
        plusCohomologyQuasicoherent B E h S hS 𝒴 hclosed hwp hsep i

AlgebraicGeometry.Stack.derivedPushforwardQuasicoherentPlus_comp_plusCohomologyDerivedCategory, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedPushforwardCohomologyComparison.lean, line 230. The attribute's comment: “the final assertion of the tag for the cohomology functor Hⁱ built as the descent of Q ∘ Hⁱ through the quotient of Stacks 07B6”.

Stacks 07BC, the final assertion, for the cohomology functor AlgebraicGeometry.Stack.plusCohomologyDerivedCategoryQuasicoherent built here: its defining identity is AlgebraicGeometry.Stack.plusCohomologyDerivedCategoryQuasicoherentFac.

def derivedPushforwardQuasicoherentPlus_comp_plusCohomologyDerivedCategory (i : ℤ)
    (hinv : (derivedQuasicoherentWPlus B E h S hS 𝒴).IsInvertedBy
      (plusCohomologyQuasicoherent B E h S hS 𝒴 hclosed hwp hsep i)) :
    toDerivedCategoryQuasicoherentPlus B E h S hS 𝒳 ⋙
        derivedPushforwardQuasicoherentPlus B E h S hS f hf hdist hpar ⋙
          plusCohomologyDerivedCategoryQuasicoherent B E h S hS 𝒴 hclosed hwp hsep i hinv ≅
      derivedPushforwardPlusLocallyQuasicoherentFlatBaseChange B E h S hS f hf ⋙
        plusCohomologyQuasicoherent B E h S hS 𝒴 hclosed hwp hsep i

AlgebraicGeometry.Stack.derivedLocallyQuasicoherentFlatBaseChangePlus_derivedPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedPushforwardQuasicoherent.lean, line 294. The attribute's comment: “for a quasi-compact quasi-separated f, the clause Rf_* carries D⁺_LQCoh^fbc(𝒪_𝒳) into D⁺_LQCoh^fbc(𝒪_𝒴), by the source's own argument over the spectral sequence Rⁱf_Hʲ(E) ⇒ Rⁱ⁺ʲf_E with a page in LQCoh^fbc (Stacks 0771) and the weak Serre condition on LQCoh^fbc (Stacks 0771 part (2), fppf half), neither of which this library has”.

For a quasi-compact and quasi-separated 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks, if LQCoh^fbc(𝒪_𝒴) is a weak Serre subcategory and the spectral sequence Rⁱf_*Hʲ(K) ⇒ Rⁱ⁺ʲf_*K has a page in LQCoh^fbc(𝒪_𝒴), then the total derived direct image Rf_* carries D⁺_{LQCoh^fbc}(𝒪_𝒳) into D⁺_{LQCoh^fbc}(𝒪_𝒴).

theorem derivedLocallyQuasicoherentFlatBaseChangePlus_derivedPushforward
    [(locallyQuasicoherentFlatBaseChangeFppfModulesUnivLE.{u, w, u + 1} B E h S hS
      𝒴).IsWeakSerreClass]
    (f : 𝒳 ⟶ 𝒴)
    (hss : IsQuasiCompactMorphism B S hS f → AlgebraicStacks.IsQuasiSeparated B S hS f →
      HasPushforwardCohomologySpectralSequence B S hS f
        (derivedLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒳)
        (locallyQuasicoherentFlatBaseChangeFppfModulesUnivLE.{u, w, u + 1} B E h S hS 𝒴))
    (hqc : IsQuasiCompactMorphism B S hS f)
    (hqs : AlgebraicStacks.IsQuasiSeparated B S hS f)
    (K : DerivedCategory.Plus (fppfModulesUnivLE.{u, w, u + 1} B S hS 𝒳))
    (hK : derivedLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒳 K) :
    derivedLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒴
      ((fppfDerivedPushforwardPlusOfStacks B S hS f).obj K)

AlgebraicGeometry.Stack.derivedParasiticLocallyQuasicoherentFlatBaseChangePlus_derivedPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedPushforwardQuasicoherent.lean, line 320. The attribute's comment: “for a quasi-compact quasi-separated f, the clause Rf_* carries D⁺_(Parasitic ∩ LQCoh^fbc)(𝒪_𝒳) into D⁺_(Parasitic ∩ LQCoh^fbc)(𝒪_𝒴), by the source's own argument over the same spectral sequence with a page in Parasitic ∩ LQCoh^fbc (Stacks 0775 with Stacks 0771) and the weak Serre condition on it (Stacks 0774 part (2), which this library has, with Stacks 0771 part (2), which it does not)”.

For a quasi-compact and quasi-separated 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks, if Parasitic ∩ LQCoh^fbc(𝒪_𝒴) is a weak Serre subcategory and the spectral sequence Rⁱf_*Hʲ(K) ⇒ Rⁱ⁺ʲf_*K has a page in it, then the total derived direct image Rf_* carries D⁺_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳) into D⁺_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒴).

theorem derivedParasiticLocallyQuasicoherentFlatBaseChangePlus_derivedPushforward
    [(parasiticModules.{u, w, u + 1} B S hS 𝒴 .fppf ⊓
      locallyQuasicoherentFlatBaseChangeFppfModulesUnivLE.{u, w, u + 1} B E h S hS
        𝒴).IsWeakSerreClass]
    (f : 𝒳 ⟶ 𝒴)
    (hss : IsQuasiCompactMorphism B S hS f → AlgebraicStacks.IsQuasiSeparated B S hS f →
      HasPushforwardCohomologySpectralSequence B S hS f
        (derivedParasiticLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒳)
        (parasiticModules.{u, w, u + 1} B S hS 𝒴 .fppf ⊓
          locallyQuasicoherentFlatBaseChangeFppfModulesUnivLE.{u, w, u + 1} B E h S hS 𝒴))
    (hqc : IsQuasiCompactMorphism B S hS f)
    (hqs : AlgebraicStacks.IsQuasiSeparated B S hS f)
    (K : DerivedCategory.Plus (fppfModulesUnivLE.{u, w, u + 1} B S hS 𝒳))
    (hK : derivedParasiticLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒳 K) :
    derivedParasiticLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒴
      ((fppfDerivedPushforwardPlusOfStacks B S hS f).obj K)

AlgebraicGeometry.Stack.derivedPushforwardPlusLocallyQuasicoherentFlatBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedPushforwardQuasicoherent.lean, line 346. The attribute's comment: “the middle vertical functor D⁺_LQCoh^fbc(𝒪_𝒳) ⥤ D⁺_LQCoh^fbc(𝒪_𝒴) of the diagram, over the preservation clause it restricts”.

The restriction of Rf_* : D⁺(𝒪_𝒳) ⥤ D⁺(𝒪_𝒴) to a functor D⁺_{LQCoh^fbc}(𝒪_𝒳) ⥤ D⁺_{LQCoh^fbc}(𝒪_𝒴), given that Rf_* carries the one into the other.

def derivedPushforwardPlusLocallyQuasicoherentFlatBaseChange (f : 𝒳 ⟶ 𝒴)
    (hf : ∀ K, derivedLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒳 K →
      derivedLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒴
        ((fppfDerivedPushforwardPlusOfStacks B S hS f).obj K)) :
    (derivedLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒳).FullSubcategory ⥤
      (derivedLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒴).FullSubcategory

AlgebraicGeometry.Stack.derivedPushforwardPlusLocallyQuasicoherentFlatBaseChange_comp_ι, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedPushforwardQuasicoherent.lean, line 362. The attribute's comment: “the middle-to-right commuting square of the diagram, READ IN D⁺(𝒪_𝒳) AND NOT IN THE SOURCE'S UNBOUNDED D(𝒪_𝒳): the unbounded right derived direct image is not constructed in this library”.

The middle vertical functor followed by the inclusion of D⁺_{LQCoh^fbc}(𝒪_𝒴) into D⁺(𝒪_𝒴) is the inclusion of D⁺_{LQCoh^fbc}(𝒪_𝒳) followed by Rf_*.

def derivedPushforwardPlusLocallyQuasicoherentFlatBaseChange_comp_ι (f : 𝒳 ⟶ 𝒴)
    (hf : ∀ K, derivedLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒳 K →
      derivedLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒴
        ((fppfDerivedPushforwardPlusOfStacks B S hS f).obj K)) :
    derivedPushforwardPlusLocallyQuasicoherentFlatBaseChange B E h S hS f hf ⋙
        (derivedLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒴).ι ≅
      (derivedLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒳).ι ⋙
        fppfDerivedPushforwardPlusOfStacks B S hS f

AlgebraicGeometry.Stack.derivedPushforwardPlusParasiticLocallyQuasicoherentFlatBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedPushforwardQuasicoherent.lean, line 391. The attribute's comment: “the left vertical functor D⁺_(Parasitic ∩ LQCoh^fbc)(𝒪_𝒳) ⥤ D⁺_(Parasitic ∩ LQCoh^fbc)(𝒪_𝒴) of the diagram, over the two preservation clauses it restricts”.

The restriction of the middle vertical functor to a functor D⁺_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳) ⥤ D⁺_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒴), given that Rf_* carries the one into the other.

def derivedPushforwardPlusParasiticLocallyQuasicoherentFlatBaseChange (f : 𝒳 ⟶ 𝒴)
    (hf : ∀ K, derivedLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒳 K →
      derivedLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒴
        ((fppfDerivedPushforwardPlusOfStacks B S hS f).obj K))
    (hpar : ∀ K, derivedParasiticLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒳 K →
      derivedParasiticLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒴
        ((fppfDerivedPushforwardPlusOfStacks B S hS f).obj K)) :
    (parasiticInDerivedLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒳).FullSubcategory ⥤
      (parasiticInDerivedLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒴).FullSubcategory

AlgebraicGeometry.Stack.derivedPushforwardPlusParasiticLocallyQuasicoherentFlatBaseChange_comp_ι, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedPushforwardQuasicoherent.lean, line 409. The attribute's comment: “the left-to-middle commuting square of the diagram”.

The left vertical functor followed by the inclusion of D⁺_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒴) into D⁺_{LQCoh^fbc}(𝒪_𝒴) is the inclusion of D⁺_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳) followed by the middle vertical functor.

def derivedPushforwardPlusParasiticLocallyQuasicoherentFlatBaseChange_comp_ι (f : 𝒳 ⟶ 𝒴)
    (hf : ∀ K, derivedLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒳 K →
      derivedLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒴
        ((fppfDerivedPushforwardPlusOfStacks B S hS f).obj K))
    (hpar : ∀ K, derivedParasiticLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒳 K →
      derivedParasiticLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒴
        ((fppfDerivedPushforwardPlusOfStacks B S hS f).obj K)) :
    derivedPushforwardPlusParasiticLocallyQuasicoherentFlatBaseChange B E h S hS f hf hpar ⋙
        (parasiticInDerivedLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒴).ι ≅
      (parasiticInDerivedLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒳).ι ⋙
        derivedPushforwardPlusLocallyQuasicoherentFlatBaseChange B E h S hS f hf

AlgebraicGeometry.Stack.derivedPushforwardQuasicoherentPlus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedPushforwardQuasicoherent.lean, line 469. The attribute's comment: “the induced functor Rf_(QCoh,) : D⁺_QCoh(𝒪_𝒳) ⥤ D⁺_QCoh(𝒪_𝒴) on the Verdier quotients of Stacks 07B6, over the two preservation clauses and over the triangulatedness of Rf_ (a Mathlib TODO for rightDerivedFunctorPlus)”.

The derived direct image

Rf_{QCoh,*} : D⁺_QCoh(𝒪_𝒳) ⥤ D⁺_QCoh(𝒪_𝒴)

that Rf_* induces on the bounded-below Verdier quotients of Stacks 07B6: the functor out of the localization through which D⁺_{LQCoh^fbc}(𝒪_𝒳) ⥤ D⁺_{LQCoh^fbc}(𝒪_𝒴) ⥤ D⁺_QCoh(𝒪_𝒴) factors.

def derivedPushforwardQuasicoherentPlus (f : 𝒳 ⟶ 𝒴)
    (hf : ∀ K, derivedLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒳 K →
      derivedLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒴
        ((fppfDerivedPushforwardPlusOfStacks B S hS f).obj K))
    (hdist : DerivedPushforwardMapsDistinguished B S hS f)
    (hpar : ∀ K, derivedParasiticLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒳 K →
      derivedParasiticLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒴
        ((fppfDerivedPushforwardPlusOfStacks B S hS f).obj K)) :
    derivedCategoryQuasicoherentPlus B E h S hS 𝒳 ⥤
      derivedCategoryQuasicoherentPlus B E h S hS 𝒴

AlgebraicGeometry.Stack.toDerivedCategoryQuasicoherentPlus_comp_derivedPushforwardQuasicoherentPlus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedPushforwardQuasicoherent.lean, line 489. The attribute's comment: “the square identifying the induced functor on quotient categories, Q_𝒳 ⋙ Rf_(QCoh,) = Rf_^LQCoh ⋙ Q_𝒴”.

The functor Rf_{QCoh,*} on the Verdier quotients is induced by Rf_*: precomposing it with the quotient functor of 𝒳 gives the middle vertical functor followed by the quotient functor of 𝒴.

theorem toDerivedCategoryQuasicoherentPlus_comp_derivedPushforwardQuasicoherentPlus
    (f : 𝒳 ⟶ 𝒴)
    (hf : ∀ K, derivedLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒳 K →
      derivedLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒴
        ((fppfDerivedPushforwardPlusOfStacks B S hS f).obj K))
    (hdist : DerivedPushforwardMapsDistinguished B S hS f)
    (hpar : ∀ K, derivedParasiticLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒳 K →
      derivedParasiticLocallyQuasicoherentFlatBaseChangePlus B E h S hS 𝒴
        ((fppfDerivedPushforwardPlusOfStacks B S hS f).obj K)) :
    toDerivedCategoryQuasicoherentPlus B E h S hS 𝒳 ⋙
        derivedPushforwardQuasicoherentPlus B E h S hS f hf hdist hpar =
      derivedPushforwardPlusLocallyQuasicoherentFlatBaseChange B E h S hS f hf ⋙
        toDerivedCategoryQuasicoherentPlus B E h S hS 𝒴

AlgebraicGeometry.Stack.sheafFlatBaseChangeDerivedPushforwardPlus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentDerivedPushforward.lean, line 145. The attribute's comment: “the middle vertical arrow Rf_* : D⁺_LQCoh^fbc(𝒪_𝒳) ⥤ D⁺_LQCoh^fbc(𝒪_𝒴) of the diagram, for the faithful LQCoh^fbc (flat base change with the sheaf pullback, Stacks 0762), at module universe u + 1”.

Stacks 07BC, the middle vertical arrow Rf_* : D⁺_{LQCoh^fbc}(𝒪_𝒳) ⥤ D⁺_{LQCoh^fbc}(𝒪_𝒴) for a quasi-compact quasi-separated f: the restriction of Rf_*.

def sheafFlatBaseChangeDerivedPushforwardPlus :
    (DerivedCategoryB.derivedCategoryBInPlus
      (lqcohSheafFbcFppfModules.{u, w, u + 1} B E h S hS
        𝒳)).FullSubcategory ⥤
      (DerivedCategoryB.derivedCategoryBInPlus
        (lqcohSheafFbcFppfModules.{u, w, u + 1} B E h S hS
          𝒴)).FullSubcategory

AlgebraicGeometry.Stack.parasiticSheafFlatBaseChangeDerivedPushforwardPlus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentDerivedPushforward.lean, line 160. The attribute's comment: “the left vertical arrow Rf_* : D⁺_(Parasitic ∩ LQCoh^fbc)(𝒪_𝒳) ⥤ D⁺_(Parasitic ∩ LQCoh^fbc)(𝒪_𝒴) of the diagram”.

Stacks 07BC, the left vertical arrow Rf_* : D⁺_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳) ⥤ D⁺_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒴) for a quasi-compact quasi-separated f: the restriction of Rf_* (the parasitic half is Stacks 0775 (2)).

def parasiticSheafFlatBaseChangeDerivedPushforwardPlus :
    (DerivedCategoryB.derivedCategoryBInPlus
      (parasiticModules.{u, w, u + 1} B S hS 𝒳 .fppf ⊓
        lqcohSheafFbcFppfModules.{u, w, u + 1} B E h S hS
          𝒳)).FullSubcategory ⥤
      (DerivedCategoryB.derivedCategoryBInPlus
        (parasiticModules.{u, w, u + 1} B S hS 𝒴 .fppf ⊓
          lqcohSheafFbcFppfModules.{u, w, u + 1} B E h S hS
            𝒴)).FullSubcategory

AlgebraicGeometry.Stack.ιOfLE_comp_sheafFlatBaseChangeDerivedPushforwardPlus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentDerivedPushforward.lean, line 176. The attribute's comment: “the left square of the diagram commutes (an equality of functors)”.

Stacks 07BC, the left square of the diagram commutes: the inclusion D⁺_{Parasitic ∩ LQCoh^fbc} ⊆ D⁺_{LQCoh^fbc} followed by the middle arrow is the left arrow followed by the inclusion.

theorem ιOfLE_comp_sheafFlatBaseChangeDerivedPushforwardPlus :
    ObjectProperty.ιOfLE (derivedCategoryBInPlus_parasiticSheafFlatBaseChange_le B E h S hS 𝒳) ⋙
        sheafFlatBaseChangeDerivedPushforwardPlus B E h S hS f hqc hqs =
      parasiticSheafFlatBaseChangeDerivedPushforwardPlus B E h S hS f hqc hqs ⋙
        ObjectProperty.ιOfLE
          (derivedCategoryBInPlus_parasiticSheafFlatBaseChange_le B E h S hS 𝒴)

AlgebraicGeometry.Stack.sheafFlatBaseChangeDerivedPushforwardPlusCompιIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentDerivedPushforward.lean, line 190. The attribute's comment: “the right square of the diagram, into the unbounded D(𝒪) with the unbounded Rf_, commutes up to the canonical isomorphism Rf_⁺ ⋙ ι ≅ ι ⋙ Rf_*”.

Stacks 07BC, the right square of the diagram commutes: the middle arrow followed by the inclusion D⁺_{LQCoh^fbc}(𝒪_𝒴) ⊆ D(𝒪_𝒴) is the inclusion D⁺_{LQCoh^fbc}(𝒪_𝒳) ⊆ D(𝒪_𝒳) followed by the unbounded Rf_* : D(𝒪_𝒳) ⥤ D(𝒪_𝒴), up to the canonical isomorphism identifying the bounded below Rf_* with the restriction of the unbounded one.

def sheafFlatBaseChangeDerivedPushforwardPlusCompιIso :
    sheafFlatBaseChangeDerivedPushforwardPlus B E h S hS f hqc hqs ⋙
        (DerivedCategoryB.derivedCategoryBInPlus
          (lqcohSheafFbcFppfModules.{u, w, u + 1} B E h S hS
            𝒴)).ι ⋙ DerivedCategory.Plus.ι ≅
      (DerivedCategoryB.derivedCategoryBInPlus
          (lqcohSheafFbcFppfModules.{u, w, u + 1} B E h S hS
            𝒳)).ι ⋙ DerivedCategory.Plus.ι ⋙ fppfDerivedPushforwardOfStacks B S hS f

AlgebraicGeometry.Stack.quasicoherentDerivedPushforwardPlus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentDerivedPushforward.lean, line 218. The attribute's comment: “the induced functor Rf_(QCoh,*) : D⁺_QCoh(𝒪_𝒳) ⥤ D⁺_QCoh(𝒪_𝒴) on the quotient categories D⁺_LQCoh^fbc / D⁺_(Parasitic ∩ LQCoh^fbc)”.

Stacks 07BC, the induced functor Rf_{QCoh,*} : D⁺_QCoh(𝒪_𝒳) ⥤ D⁺_QCoh(𝒪_𝒴) on the quotients D⁺_QCoh = D⁺_{LQCoh^fbc} / D⁺_{Parasitic ∩ LQCoh^fbc} of Stacks 07B6, for a quasi-compact quasi-separated f.

def quasicoherentDerivedPushforwardPlus :
    (DerivedCategoryB.serreQuotientWPlus
      (lqcohSheafFbcFppfModules.{u, w, u + 1} B E h S hS 𝒳)
      (parasiticModules.{u, w, u + 1} B S hS 𝒳 .fppf ⊓
        lqcohSheafFbcFppfModules.{u, w, u + 1} B E h S hS
          𝒳)).Localization ⥤
      (DerivedCategoryB.serreQuotientWPlus
        (lqcohSheafFbcFppfModules.{u, w, u + 1} B E h S hS 𝒴)
        (parasiticModules.{u, w, u + 1} B S hS 𝒴 .fppf ⊓
          lqcohSheafFbcFppfModules.{u, w, u + 1} B E h S hS
            𝒴)).Localization

AlgebraicGeometry.Stack.toSerreQuotient_comp_quasicoherentDerivedPushforwardPlus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentDerivedPushforward.lean, line 236. The attribute's comment: “Rf_(QCoh,) is the functor induced by Rf_ on the quotient categories: the quotient square commutes (an equality of functors)”.

Stacks 07BC: Rf_{QCoh,*} is induced by Rf_* — the quotient functor of 𝒳 followed by Rf_{QCoh,*} is the middle arrow followed by the quotient functor of 𝒴.

theorem toSerreQuotient_comp_quasicoherentDerivedPushforwardPlus :
    (DerivedCategoryB.serreQuotientWPlus
        (lqcohSheafFbcFppfModules.{u, w, u + 1} B E h S hS 𝒳)
        (parasiticModules.{u, w, u + 1} B S hS 𝒳 .fppf ⊓
          lqcohSheafFbcFppfModules.{u, w, u + 1} B E h S hS
            𝒳)).Q ⋙
        quasicoherentDerivedPushforwardPlus B E h S hS f hqc hqs =
      sheafFlatBaseChangeDerivedPushforwardPlus B E h S hS f hqc hqs ⋙
        (DerivedCategoryB.serreQuotientWPlus
          (lqcohSheafFbcFppfModules.{u, w, u + 1} B E h S hS 𝒴)
          (parasiticModules.{u, w, u + 1} B S hS 𝒴 .fppf ⊓
            lqcohSheafFbcFppfModules.{u, w, u + 1} B E h S hS
              𝒴)).Q

AlgebraicGeometry.Stack.quasicoherentDerivedPushforwardPlusCohomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentDerivedPushforward.lean, line 301. The attribute's comment: “the final assertion: the functors Rⁱf_QCoh of Stacks 077A are Hⁱ ∘ Rf_(QCoh,*) with Hⁱ of Stacks 07B7, as a natural isomorphism of functors QCoh(𝒪_𝒳) ⥤ QCoh(𝒪_𝒴) (𝓜 placed in degree zero)”.

Stacks 07BC, the final assertion: Rⁱf_QCoh = Hⁱ ∘ Rf_{QCoh,*}. For a quasi-coherent 𝓜 on 𝒳, placed in degree zero of D⁺_QCoh(𝒪_𝒳), Hⁱ(Rf_{QCoh,*}(𝓜[0])) ≅ Rⁱf_QCoh(𝓜), naturally in 𝓜, with Hⁱ the cohomology functor of Stacks 07B7 and Rⁱf_QCoh the functor of Stacks 077A.

def quasicoherentDerivedPushforwardPlusCohomologyIso (i : ℕ) :
    ObjectProperty.ιOfLE
          (isQuasicoherentOnSite_le_locallyQuasicoherentSheafFlatBaseChangeFppfModules_succ
            B E h S hS 𝒳) ⋙
        sheafFlatBaseChangeSingleFunctor B E h S hS 𝒳 ⋙
        (DerivedCategoryB.serreQuotientWPlus
          (lqcohSheafFbcFppfModules.{u, w, u + 1} B E h S hS 𝒳)
          (parasiticModules.{u, w, u + 1} B S hS 𝒳 .fppf ⊓
            lqcohSheafFbcFppfModules.{u, w, u + 1} B E h S hS
              𝒳)).Q ⋙
          quasicoherentDerivedPushforwardPlus B E h S hS f hqc hqs ⋙
            plusQuasicoherentCohomology B E h S hS i ≅
      sheafFlatBaseChangeQuasicoherentHigherDirectImage B E h S hS f hqc hqs i

AlgebraicGeometry.Stack.toSerreQuotient_comp_quasicoherentDerivedPushforwardPlusCohomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentDerivedPushforward.lean, line 324. The attribute's comment: “the final assertion on D⁺_LQCoh^fbc(𝒪_𝒳): Hⁱ ∘ Rf_(QCoh,) ∘ (quotient functor) ≅ Q ∘ Hⁱ ∘ Rf_, the identity the source reads off the definition of Hⁱ”.

Stacks 07BC, the final assertion on all of D⁺_{LQCoh^fbc}(𝒪_𝒳): Hⁱ ∘ Rf_{QCoh,*} composed with the quotient functor of 𝒳 is Q ∘ Hⁱ ∘ Rf_*, with Hⁱ the cohomology functor of Stacks 07B7 and Q the coherator of Stacks 0778.

def toSerreQuotient_comp_quasicoherentDerivedPushforwardPlusCohomologyIso (i : ℤ) :
    (DerivedCategoryB.serreQuotientWPlus
        (lqcohSheafFbcFppfModules.{u, w, u + 1} B E h S hS 𝒳)
        (parasiticModules.{u, w, u + 1} B S hS 𝒳 .fppf ⊓
          lqcohSheafFbcFppfModules.{u, w, u + 1} B E h S hS
            𝒳)).Q ⋙
        quasicoherentDerivedPushforwardPlus B E h S hS f hqc hqs ⋙
          plusQuasicoherentCohomology B E h S hS i ≅
      sheafFlatBaseChangeDerivedPushforwardPlus B E h S hS f hqc hqs ⋙
        sheafFlatBaseChangeHomologyFunctor B E h S hS 𝒴 i ⋙
          coherator (isQuasicoherentOnSite_moduleLowerShriekSucc_moduleInverseImage
            (isQuasicoherentOnSite_moduleLowerShriekSucc B S hS 𝒴)
            (isQuasicoherentOnSite_moduleInverseImage_of_sheafFlatBaseChangeModulesSucc
              B E h S hS 𝒴))

Sources

• Section 104.6, Tag 07BB
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.derivedPushforwardQuasicoherentPlus_comp_plusCohomology · AlgebraicGeometry.Stack.derivedPushforwardQuasicoherentPlus_comp_plusCohomologyDerivedCategory · AlgebraicGeometry.Stack.derivedLocallyQuasicoherentFlatBaseChangePlus_derivedPushforward · AlgebraicGeometry.Stack.derivedParasiticLocallyQuasicoherentFlatBaseChangePlus_derivedPushforward · AlgebraicGeometry.Stack.derivedPushforwardPlusLocallyQuasicoherentFlatBaseChange · AlgebraicGeometry.Stack.derivedPushforwardPlusLocallyQuasicoherentFlatBaseChange_comp_ι · AlgebraicGeometry.Stack.derivedPushforwardPlusParasiticLocallyQuasicoherentFlatBaseChange · AlgebraicGeometry.Stack.derivedPushforwardPlusParasiticLocallyQuasicoherentFlatBaseChange_comp_ι

Section104.7 Derived pullback of quasi-coherent modules#

Section 104.7 of the Stacks Project, Tag 07BD. 1 tag here is carried by 13 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07BE, a proposition

Tag 07BE in the Stacks Project.

AlgebraicGeometry.Stack.derivedLocallyQuasicoherentFlatBaseChange_derivedFppfModulePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedQuasicoherentPullback.lean, line 213. The attribute's comment: “the first assertion, that f^ carries D_LQCoh^fbc(𝒪_𝒴) into D_LQCoh^fbc(𝒪_𝒳), on objects; conditional on the module-level statement that f^ maps LQCoh^fbc(𝒪_𝒴) into LQCoh^fbc(𝒪_𝒳) (Stacks 0771 part (3), the source's Cohomology of Stacks, Proposition 103.8.1), carried as the hypothesis hpres”.

Stacks 07BE, the first assertion, on objects. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks and let K be an object of D_{LQCoh^fbc}(𝒪_𝒴). Then f^*K is an object of D_{LQCoh^fbc}(𝒪_𝒳).

Since f^* is exact its cohomology modules are the inverse images of those of K, so the statement reduces degree by degree to the module-level Stacks 0771 part (3) — that f^* maps LQCoh^fbc(𝒪_𝒴) into LQCoh^fbc(𝒪_𝒳) — which is the hypothesis hpres.

theorem derivedLocallyQuasicoherentFlatBaseChange_derivedFppfModulePullback
    (hpres : ∀ F : fppfModules B S hS 𝒴,
      locallyQuasicoherentFlatBaseChangeFppfModules B E hE S hS 𝒴 F →
        locallyQuasicoherentFlatBaseChangeFppfModules B E hE S hS 𝒳
          ((fppfModulesPullback B S hS f).obj F))
    (K : DerivedCategory (fppfModules B S hS 𝒴))
    (hK : derivedLocallyQuasicoherentFlatBaseChange B E hE S hS 𝒴 K) :
    derivedLocallyQuasicoherentFlatBaseChange B E hE S hS 𝒳
      ((derivedFppfModulePullback B S hS f).obj K)

AlgebraicGeometry.Stack.derivedLocallyQuasicoherentPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedQuasicoherentPullback.lean, line 234. The attribute's comment: “the first assertion, the induced functor D_LQCoh^fbc(𝒪_𝒴) ⥤ D_LQCoh^fbc(𝒪_𝒳); conditional on the module-level Stacks 0771 part (3), carried as the hypothesis hpres”.

Stacks 07BE, the first assertion. The induced functor f^* : D_{LQCoh^fbc}(𝒪_𝒴) ⥤ D_{LQCoh^fbc}(𝒪_𝒳), the left vertical arrow of the square of the source. Its composite with the inclusion of D_{LQCoh^fbc}(𝒪_𝒳) into D(𝒪_𝒳) is the composite of the inclusion of D_{LQCoh^fbc}(𝒪_𝒴) with f^* : D(𝒪_𝒴) ⥤ D(𝒪_𝒳), which is the commutativity of the square; see AlgebraicGeometry.Stack.derivedLocallyQuasicoherentPullback_comp_ι.

def derivedLocallyQuasicoherentPullback
    (hpres : ∀ F : fppfModules B S hS 𝒴,
      locallyQuasicoherentFlatBaseChangeFppfModules B E hE S hS 𝒴 F →
        locallyQuasicoherentFlatBaseChangeFppfModules B E hE S hS 𝒳
          ((fppfModulesPullback B S hS f).obj F)) :
    (derivedLocallyQuasicoherentFlatBaseChange B E hE S hS 𝒴).FullSubcategory ⥤
      (derivedLocallyQuasicoherentFlatBaseChange B E hE S hS 𝒳).FullSubcategory

AlgebraicGeometry.Stack.derivedLocallyQuasicoherentPullback_comp_ι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedQuasicoherentPullback.lean, line 253. The attribute's comment: “the commutativity of the square: the induced functor on D_LQCoh^fbc, followed by the inclusion into D(𝒪_𝒳), is the inclusion into D(𝒪_𝒴) followed by f^*; conditional on the module-level Stacks 0771 part (3), carried as the hypothesis hpres”.

Stacks 07BE, the commutativity of the square. Restricting f^* to the subcategories of complexes with locally quasi-coherent cohomology and flat base change and then including into D(𝒪_𝒳) is the same as including into D(𝒪_𝒴) and applying f^*.

theorem derivedLocallyQuasicoherentPullback_comp_ι
    (hpres : ∀ F : fppfModules B S hS 𝒴,
      locallyQuasicoherentFlatBaseChangeFppfModules B E hE S hS 𝒴 F →
        locallyQuasicoherentFlatBaseChangeFppfModules B E hE S hS 𝒳
          ((fppfModulesPullback B S hS f).obj F)) :
    derivedLocallyQuasicoherentPullback B E hE S hS f hpres ⋙
        (derivedLocallyQuasicoherentFlatBaseChange B E hE S hS 𝒳).ι =
      (derivedLocallyQuasicoherentFlatBaseChange B E hE S hS 𝒴).ι ⋙
        derivedFppfModulePullback B S hS f

AlgebraicGeometry.Stack.isLeftDerivable_toDerivedCategoryQuasicoherent_comp_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedQuasicoherentPullback.lean, line 324. The attribute's comment: “the second assertion, that q_𝒳 ∘ f^ is left derivable with respect to the localization D_LQCoh^fbc(𝒪_𝒴) → D_QCoh(𝒪_𝒴) of 07B6, i.e. that LF is defined at every object; conditional on the Bousfield colocalization of 07BA, carried as the hypothesis hres, and on 0771 and 0774, carried as the triangulated-subcategory instances. The adjointness of Lf^_QCoh with Rf_QCoh,* is NOT proved”.

Stacks 07BE, the second assertion. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks. If every object of D_{LQCoh^fbc}(𝒪_𝒴) receives a morphism of the inverted class from an object left orthogonal to D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒴) — the Bousfield colocalization of Stacks 07BA — then every functor out of D_{LQCoh^fbc}(𝒪_𝒴), in particular the composite

D_{LQCoh^fbc}(𝒪_𝒴) --f^*--> D_{LQCoh^fbc}(𝒪_𝒳) --q_𝒳--> D_QCoh(𝒪_𝒳)

the source names, is left derivable with respect to the class of morphisms that the Verdier quotient D_{LQCoh^fbc}(𝒪_𝒴) ⟶ D_QCoh(𝒪_𝒴) of Stacks 07B6 inverts, in the sense of Stacks 05SV: the left derived functor is defined at every object.

The resolution is an initial object of the index category S/E of Stacks 05S9, which is the source's assertion that E' ⟶ E is cofinal in S/E; see CategoryTheory.ObjectProperty.isLeftDerivable_trW_of_leftOrthogonal_resolutions.

theorem isLeftDerivable_toDerivedCategoryQuasicoherent_comp_pullback
    [HasDerivedCategory.{t} (fppfModules B S hS 𝒳)]
    [PreservesFiniteColimits (fppfModulesPullback B S hS f)]
    [(locallyQuasicoherentFlatBaseChangeFppfModules B E hE S hS 𝒳).IsClosedUnderIsomorphisms]
    (hpres : ∀ F : fppfModules B S hS 𝒴,
      locallyQuasicoherentFlatBaseChangeFppfModules B E hE S hS 𝒴 F →
        locallyQuasicoherentFlatBaseChangeFppfModules B E hE S hS 𝒳
          ((fppfModulesPullback B S hS f).obj F))
    (hres : ∀ K : (derivedLocallyQuasicoherentFlatBaseChange B E hE S hS 𝒴).FullSubcategory,
      ∃ (K' : (derivedLocallyQuasicoherentFlatBaseChange B E hE S hS 𝒴).FullSubcategory)
        (s : K' ⟶ K), derivedQuasicoherentW B E hE S hS 𝒴 s ∧
          (derivedParasiticInLocallyQuasicoherent B E hE S hS (𝒴 := 𝒴)).leftOrthogonal K') :
    (derivedLocallyQuasicoherentPullback B E hE S hS f hpres ⋙
        toDerivedCategoryQuasicoherent B E hE S hS 𝒳).IsLeftDerivable
      (derivedQuasicoherentW B E hE S hS 𝒴)

AlgebraicGeometry.Stack.FlatFppf.isLeftDerivable_of_parasiticFreePart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedQuasicoherentPullback.lean, line 374. The attribute's comment: “the second assertion, that q_𝒳 ∘ f^ is left derivable with respect to the localization D_LQCoh^fbc(𝒪_𝒴) → D_QCoh(𝒪_𝒴) of 07B6, with the colocalization input supplied by 07BA; conditional on the derived module-level Lg_! of 07AS (4) and on 07B9 (2)(a), (2)(c), carried as Lsh, adj, hunit and hK', on the module-level 0771 (3), carried as hpres, and on 0771 and 0774, carried as the triangulated-subcategory instances. The adjointness of Lf^_QCoh with Rf_QCoh,* is NOT proved”.

Stacks 07BE, the second assertion, over Stacks 07BA. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks and let g : Sh(𝒴_{flat,fppf}) ⟶ Sh(𝒴_{fppf}) be the morphism of ringed topoi of Stacks 0788 (2). Given the derived lower shriek Lg_! of Stacks 07AS part (4) — carried, as in Stacks 07BA, as a functor Lsh, an adjunction Lsh ⊣ g^* and the invertibility of its unit — and given that the parasitic-free part Lg_! g^* K of an object K of D_{LQCoh^fbc}(𝒪_𝒴) is again in D_{LQCoh^fbc}(𝒪_𝒴) (Stacks 07B9 (2)(a), (2)(c), carried as hK'), the composite

D_{LQCoh^fbc}(𝒪_𝒴) --f^*--> D_{LQCoh^fbc}(𝒪_𝒳) --q_𝒳--> D_QCoh(𝒪_𝒳)

is left derivable with respect to the localization of Stacks 07B6.

The resolution hypothesis of AlgebraicGeometry.Stack.isLeftDerivable_toDerivedCategoryQuasicoherent_comp_pullback is discharged from Stacks 07BA, AlgebraicGeometry.Stack.FlatFppf.extensionProduct_parasiticFreePart, through AlgebraicGeometry.Stack.exists_derivedQuasicoherentW_leftOrthogonal_of_extensionProduct.

theorem isLeftDerivable_of_parasiticFreePart
    [HasDerivedCategory.{t} (fppfModules B S hS 𝒳)]
    [HasDerivedCategory.{t'} (flatFppfModules B S hS 𝒴)]
    [PreservesFiniteColimits (fppfModulesPullback B S hS f)]
    [(locallyQuasicoherentFlatBaseChangeFppfModules B E hE S hS 𝒳).IsClosedUnderIsomorphisms]
    [(derivedLocallyQuasicoherentFlatBaseChange B E hE S hS 𝒴).IsClosedUnderIsomorphisms]
    (Lsh : DerivedCategory (flatFppfModules B S hS 𝒴) ⥤ DerivedCategory (fppfModules B S hS 𝒴))
    (adj : Lsh ⊣ derivedModuleRestriction B S hS 𝒴) (hunit : IsIso adj.unit)
    (hpres : ∀ F : fppfModules B S hS 𝒴,
      locallyQuasicoherentFlatBaseChangeFppfModules B E hE S hS 𝒴 F →
        locallyQuasicoherentFlatBaseChangeFppfModules B E hE S hS 𝒳
          ((fppfModulesPullback B S hS f).obj F))
    (hK' : ∀ K : DerivedCategory (fppfModules B S hS 𝒴),
      derivedLocallyQuasicoherentFlatBaseChange B E hE S hS 𝒴 K →
        derivedLocallyQuasicoherentFlatBaseChange B E hE S hS 𝒴
          (parasiticFreePart B S hS 𝒴 Lsh K)) :
    (derivedLocallyQuasicoherentPullback B E hE S hS f hpres ⋙
        toDerivedCategoryQuasicoherent B E hE S hS 𝒳).IsLeftDerivable
      (derivedQuasicoherentW B E hE S hS 𝒴)

AlgebraicGeometry.Stack.FlatFppf.derivedSheafFlatBaseChangePullbackSucc, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedQuasicoherentPullbackSheafFlatBaseChange.lean, line 134. The attribute's comment: “the first assertion: the exact functor f^* induces D_LQCoh^fbc(𝒪_𝒴) ⥤ D_LQCoh^fbc(𝒪_𝒳), with LQCoh^fbc the class of Stacks 0762 (flat base change for the pullback of sheaves), at module universe u + 1, for any models of the derived categories”.

The functor D_{LQCoh^fbc}(𝒪_𝒴) ⥤ D_{LQCoh^fbc}(𝒪_𝒳) induced by the exact functor f^* : D(𝒪_𝒴) ⥤ D(𝒪_𝒳).

def derivedSheafFlatBaseChangePullbackSucc :
    (DerivedCategoryB.derivedCategoryB
        (sheafFlatBaseChangeModulesSucc B E h S hS 𝒴)).FullSubcategory ⥤
      (DerivedCategoryB.derivedCategoryB
        (sheafFlatBaseChangeModulesSucc B E h S hS 𝒳)).FullSubcategory

AlgebraicGeometry.Stack.FlatFppf.derivedSheafFlatBaseChangePullbackSucc_comp_ι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedQuasicoherentPullbackSheafFlatBaseChange.lean, line 147. The attribute's comment: “the commutative square of the first assertion, at module universe u + 1, for the class of Stacks 0762 read with the pullback of sheaves, for any models of the derived categories”.

The induced functor followed by the inclusion D_{LQCoh^fbc}(𝒪_𝒳) ⊆ D(𝒪_𝒳) is the inclusion D_{LQCoh^fbc}(𝒪_𝒴) ⊆ D(𝒪_𝒴) followed by f^* : D(𝒪_𝒴) ⥤ D(𝒪_𝒳).

theorem derivedSheafFlatBaseChangePullbackSucc_comp_ι :
    derivedSheafFlatBaseChangePullbackSucc B E h S hS f ⋙
        (DerivedCategoryB.derivedCategoryB (sheafFlatBaseChangeModulesSucc B E h S hS 𝒳)).ι =
      (DerivedCategoryB.derivedCategoryB (sheafFlatBaseChangeModulesSucc B E h S hS 𝒴)).ι ⋙
        (modulePullbackSucc B S hS f).mapDerivedCategory

AlgebraicGeometry.Stack.FlatFppf.isLeftDerivable_derivedSheafFlatBaseChangePullbackSucc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedQuasicoherentPullbackSheafFlatBaseChange.lean, line 207. The attribute's comment: “the second assertion: q_𝒳 ∘ f^* : D_LQCoh^fbc(𝒪_𝒴) ⥤ D_QCoh(𝒪_𝒳) is left derivable with respect to D_LQCoh^fbc(𝒪_𝒴) ⥤ D_QCoh(𝒪_𝒴) (Stacks 05SV), at module universe u + 1, for the class of Stacks 0762 read with the pullback of sheaves, at the standard models of the derived categories”.

The composite D_{LQCoh^fbc}(𝒪_𝒴) --f^*--> D_{LQCoh^fbc}(𝒪_𝒳) --q_𝒳--> D_QCoh(𝒪_𝒳) is left derivable with respect to the localization D_{LQCoh^fbc}(𝒪_𝒴) ⥤ D_QCoh(𝒪_𝒴) of Stacks 07B6, in the sense of Stacks 05SV.

theorem isLeftDerivable_derivedSheafFlatBaseChangePullbackSucc :
    (derivedSheafFlatBaseChangePullbackSucc B E h S hS f ⋙
        (DerivedCategoryB.serreQuotientW (sheafFlatBaseChangeModulesSucc B E h S hS 𝒳)
          (parasiticSheafFlatBaseChangeModulesSucc B E h S hS 𝒳)).Q).IsLeftDerivable
      (DerivedCategoryB.serreQuotientW (sheafFlatBaseChangeModulesSucc B E h S hS 𝒴)
        (parasiticSheafFlatBaseChangeModulesSucc B E h S hS 𝒴))

AlgebraicGeometry.Stack.FlatFppf.derivedQuasicoherentPullbackSucc, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedQuasicoherentPullbackSheafFlatBaseChange.lean, line 220. The attribute's comment: “Lf^_QCoh : D_QCoh(𝒪_𝒴) ⥤ D_QCoh(𝒪_𝒳), the left derived functor of q_𝒳 ∘ f^, at module universe u + 1, at the standard models of the derived categories”.

Lf^*_QCoh : D_QCoh(𝒪_𝒴) ⥤ D_QCoh(𝒪_𝒳), the left derived functor of q_𝒳 ∘ f^* with respect to the quotient functor of 𝒴 (Stacks 05S9, 05SV).

def derivedQuasicoherentPullbackSucc :
    (DerivedCategoryB.serreQuotientW (sheafFlatBaseChangeModulesSucc B E h S hS 𝒴)
        (parasiticSheafFlatBaseChangeModulesSucc B E h S hS 𝒴)).Localization ⥤
      (DerivedCategoryB.serreQuotientW (sheafFlatBaseChangeModulesSucc B E h S hS 𝒳)
        (parasiticSheafFlatBaseChangeModulesSucc B E h S hS 𝒳)).Localization

AlgebraicGeometry.Stack.FlatFppf.isLeftDerivedFunctor_derivedQuasicoherentPullbackSucc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedQuasicoherentPullbackSheafFlatBaseChange.lean, line 243. The attribute's comment: “Lf^_QCoh is the (total) left derived functor of q_𝒳 ∘ f^, with counit derivedQuasicoherentPullbackSuccCounit, at module universe u + 1”.

Lf^*_QCoh is the left derived functor of q_𝒳 ∘ f^*.

instance isLeftDerivedFunctor_derivedQuasicoherentPullbackSucc :
    (derivedQuasicoherentPullbackSucc B E h S hS f).IsLeftDerivedFunctor
      (derivedQuasicoherentPullbackSuccCounit B E h S hS f)
      (DerivedCategoryB.serreQuotientW (sheafFlatBaseChangeModulesSucc B E h S hS 𝒴)
        (parasiticSheafFlatBaseChangeModulesSucc B E h S hS 𝒴))

AlgebraicGeometry.Stack.FlatFppf.derivedQuasicoherentPullbackSuccHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedQuasicoherentPullbackSheafFlatBaseChange.lean, line 351. The attribute's comment: “the third assertion: for f quasi-compact and quasi-separated, Hom_D_QCoh(𝒪_𝒳)(Lf^_QCoh A, B) = Hom_D_QCoh(𝒪_𝒴)(A, Rf_QCoh, B) for A in D_QCoh(𝒪_𝒴) and B in D⁺_QCoh(𝒪_𝒳), at module universe u + 1, for the class of Stacks 0762 read with the pullback of sheaves, at the standard models of the derived categories”.

For a quasi-compact quasi-separated 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks, A ∈ D_QCoh(𝒪_𝒴) and B ∈ D⁺_QCoh(𝒪_𝒳),

Hom_{D_QCoh(𝒪_𝒳)}(Lf^*_QCoh A, B) ≃ Hom_{D_QCoh(𝒪_𝒴)}(A, Rf_{QCoh,*} B),

D⁺_QCoh being read inside D_QCoh through the functor induced by the inclusion.

def derivedQuasicoherentPullbackSuccHomEquiv
    (A : (DerivedCategoryB.serreQuotientW (sheafFlatBaseChangeModulesSucc B E h S hS 𝒴)
      (parasiticSheafFlatBaseChangeModulesSucc B E h S hS 𝒴)).Localization)
    (Bq : (DerivedCategoryB.serreQuotientWPlus (sheafFlatBaseChangeModulesSucc B E h S hS 𝒳)
      (parasiticSheafFlatBaseChangeModulesSucc B E h S hS 𝒳)).Localization) :
    ((derivedQuasicoherentPullbackSucc B E h S hS f).obj A ⟶
        (DerivedCategoryB.serreQuotientPlusToSerreQuotient
          (sheafFlatBaseChangeModulesSucc B E h S hS 𝒳)
          (parasiticSheafFlatBaseChangeModulesSucc B E h S hS 𝒳)).obj Bq) ≃
      (A ⟶ (DerivedCategoryB.serreQuotientPlusToSerreQuotient
          (sheafFlatBaseChangeModulesSucc B E h S hS 𝒴)
          (parasiticSheafFlatBaseChangeModulesSucc B E h S hS 𝒴)).obj
        ((derivedPushforwardQuasicoherentPlusSucc B E h S hS f hqc hqs).obj Bq))

AlgebraicGeometry.Stack.FlatFppf.derivedQuasicoherentPullbackSuccHomEquiv_naturality_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedQuasicoherentPullbackSheafFlatBaseChange.lean, line 381. The attribute's comment: “the third assertion: naturality of the adjointness in A”.

Naturality of the adjointness of Stacks 07BE in A.

theorem derivedQuasicoherentPullbackSuccHomEquiv_naturality_left
    {A A' : (DerivedCategoryB.serreQuotientW (sheafFlatBaseChangeModulesSucc B E h S hS 𝒴)
      (parasiticSheafFlatBaseChangeModulesSucc B E h S hS 𝒴)).Localization} (e : A' ⟶ A)
    (Bq : (DerivedCategoryB.serreQuotientWPlus (sheafFlatBaseChangeModulesSucc B E h S hS 𝒳)
      (parasiticSheafFlatBaseChangeModulesSucc B E h S hS 𝒳)).Localization)
    (g : (derivedQuasicoherentPullbackSucc B E h S hS f).obj A ⟶
      (DerivedCategoryB.serreQuotientPlusToSerreQuotient
        (sheafFlatBaseChangeModulesSucc B E h S hS 𝒳)
        (parasiticSheafFlatBaseChangeModulesSucc B E h S hS 𝒳)).obj Bq) :
    derivedQuasicoherentPullbackSuccHomEquiv B E h S hS f hqc hqs A' Bq
        ((derivedQuasicoherentPullbackSucc B E h S hS f).map e ≫ g) =
      e ≫ derivedQuasicoherentPullbackSuccHomEquiv B E h S hS f hqc hqs A Bq g

AlgebraicGeometry.Stack.FlatFppf.derivedQuasicoherentPullbackSuccHomEquiv_naturality_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/DerivedQuasicoherentPullbackSheafFlatBaseChange.lean, line 397. The attribute's comment: “the third assertion: naturality of the adjointness in B”.

Naturality of the adjointness of Stacks 07BE in B.

theorem derivedQuasicoherentPullbackSuccHomEquiv_naturality_right
    (A : (DerivedCategoryB.serreQuotientW (sheafFlatBaseChangeModulesSucc B E h S hS 𝒴)
      (parasiticSheafFlatBaseChangeModulesSucc B E h S hS 𝒴)).Localization)
    {Bq Bq' : (DerivedCategoryB.serreQuotientWPlus (sheafFlatBaseChangeModulesSucc B E h S hS 𝒳)
      (parasiticSheafFlatBaseChangeModulesSucc B E h S hS 𝒳)).Localization} (k : Bq ⟶ Bq')
    (g : (derivedQuasicoherentPullbackSucc B E h S hS f).obj A ⟶
      (DerivedCategoryB.serreQuotientPlusToSerreQuotient
        (sheafFlatBaseChangeModulesSucc B E h S hS 𝒳)
        (parasiticSheafFlatBaseChangeModulesSucc B E h S hS 𝒳)).obj Bq) :
    derivedQuasicoherentPullbackSuccHomEquiv B E h S hS f hqc hqs A Bq'
        (g ≫ (DerivedCategoryB.serreQuotientPlusToSerreQuotient
          (sheafFlatBaseChangeModulesSucc B E h S hS 𝒳)
          (parasiticSheafFlatBaseChangeModulesSucc B E h S hS 𝒳)).map k) =
      derivedQuasicoherentPullbackSuccHomEquiv B E h S hS f hqc hqs A Bq g ≫
        (DerivedCategoryB.serreQuotientPlusToSerreQuotient
          (sheafFlatBaseChangeModulesSucc B E h S hS 𝒴)
          (parasiticSheafFlatBaseChangeModulesSucc B E h S hS 𝒴)).map
          ((derivedPushforwardQuasicoherentPlusSucc B E h S hS f hqc hqs).map k)

Sources

• Section 104.7, Tag 07BD
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.derivedLocallyQuasicoherentFlatBaseChange_derivedFppfModulePullback · AlgebraicGeometry.Stack.derivedLocallyQuasicoherentPullback · AlgebraicGeometry.Stack.derivedLocallyQuasicoherentPullback_comp_ι · AlgebraicGeometry.Stack.isLeftDerivable_toDerivedCategoryQuasicoherent_comp_pullback · AlgebraicGeometry.Stack.FlatFppf.isLeftDerivable_of_parasiticFreePart · AlgebraicGeometry.Stack.FlatFppf.derivedSheafFlatBaseChangePullbackSucc · AlgebraicGeometry.Stack.FlatFppf.derivedSheafFlatBaseChangePullbackSucc_comp_ι · AlgebraicGeometry.Stack.FlatFppf.isLeftDerivable_derivedSheafFlatBaseChangePullbackSucc

Section104.8 Quasi-coherent objects in the derived category#

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

Tag 0H13, a lemma

Tag 0H13 in the Stacks Project.

AlgebraicGeometry.Stack.FlatFppf.isZero_derivedSectionsFppf_of_parasitic_cohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatFppfParasiticVanishingUnconditional.lean, line 69. The attribute's comment: “cohomology over an object taken as the derived functor of sections over it, and the parasitic condition of Stacks 0773 written out on abelian sheaves”.

Stacks 0H13. Let 𝒳 be an algebraic stack and let K be an object of D(𝒳_{fppf}) whose cohomology sheaves are parasitic — the sections of every cohomology sheaf of K vanish at every object of 𝒳 lying over a scheme U such that U → 𝒳 is flat (Stacks 0773). Then RΓ(x, K) = 0 for every such object x.

Cohomology over an object is the right derived functor of sections over it. The proof is the source's: by Stacks 0H10 (2)(b), RΓ(x, K) = RΓ(x, g⁻¹K), and g⁻¹K = 0 because its cohomology sheaves are the restrictions of those of K to the flat objects.

theorem isZero_derivedSectionsFppf_of_parasitic_cohomology
    (K : DerivedCategory (Sheaf (fppfTopology B S hS 𝒳) AddCommGrpCat.{u + 1}))
    (hK : ∀ n : ℤ, ∀ y : 𝒳.val.val.obj, flatObject B S hS 𝒳.val y →
      Subsingleton (((DerivedCategory.homologyFunctor
        (Sheaf (fppfTopology B S hS 𝒳) AddCommGrpCat.{u + 1}) n).obj K).obj.obj (op y)))
    (x : 𝒳.val.val.obj) (hx : flatObject B S hS 𝒳.val x) :
    IsZero ((derivedSectionsFppf B S hS 𝒳 x).obj K)

Tag 0H14, a lemma

Tag 0H14 in the Stacks Project.

AlgebraicGeometry.Stack.FlatFppf.isZero_cohomology_of_isZero_derivedSectionsFppf_flatAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatAffineCohomologyVanishing.lean, line 112. The attribute's comment: “unconditional. Cohomology over an object is the derived functor of sections over it (Tag 0DD8 convention, equal to cohomology of the slice site by Tag 03F3)”.

Stacks 0H14. Let 𝒳 be an algebraic stack and let K be an object of D(𝒳_{fppf}) such that RΓ(x, K) = 0 for every object x of 𝒳 lying over an affine scheme U with U → 𝒳 flat. Then H^i(𝒳, K) = 0 for all i.

Here RΓ(x, -) is the right derived functor of sections over x (the convention of Stacks 0DD8 and Stacks 0H10 (2)(b) in this library), and H^i(𝒳, K) is the i-th cohomology of the unbounded derived global sections RΓ(𝒳_{fppf}, K).

This is the source's proof: g⁻¹K = 0 because its derived sections vanish on a family covering the flat-fppf site (Stacks 0H10 (2)(b)), so RΓ(𝒳_{flat,fppf}, g⁻¹K) = 0, which is RΓ(𝒳_{fppf}, K) by Stacks 0H10 (2)(a).

theorem isZero_cohomology_of_isZero_derivedSectionsFppf_flatAffine
    (K : DerivedCategory (Sheaf (fppfTopology B S hS 𝒳) AddCommGrpCat.{u + 1}))
    (hK : ∀ x : 𝒳.val.val.obj, flatObject B S hS 𝒳.val x →
      IsAffine ((BigFppfOver.toScheme B S hS).obj (𝒳.val.val.p.obj x)) →
      IsZero ((derivedSectionsFppf B S hS 𝒳 x).obj K))
    (i : ℤ) :
    IsZero ((DerivedCategory.homologyFunctor AddCommGrpCat.{u + 1} i).obj
      ((AlgebraicGeometry.Stack.derivedGlobalSections.{u, u + 1} B S hS 𝒳.val).obj K))

Tag 0H15, a lemma

Tag 0H15 in the Stacks Project.

AlgebraicGeometry.Stack.FlatFppf.hasAffineDerivedSectionsBaseChange_derivedModuleLowerShriekSucc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasiCoherentDerivedEquivalenceOfStack.lean, line 69.

Stacks 0H15. Let 𝒳 be an algebraic stack and H an object of D_QCoh(𝒪_{𝒳_{flat, fppf}}) (module universe u + 1). Then Lg_! H has the following property: for every morphism x ⟶ x' of 𝒳_{affine} the map RΓ(x', Lg_! H) ⊗^L_{𝒪(x')} 𝒪(x) ⟶ RΓ(x, Lg_! H) is a quasi-isomorphism (HasAffineDerivedSectionsBaseChange). The derived categories are the standard models.

theorem hasAffineDerivedSectionsBaseChange_derivedModuleLowerShriekSucc :
    letI := HasDerivedCategory.standard
      (SheafOfModules.{u + 1} (subsiteRingStructureSheaf B S hS 𝒳))
    letI := HasDerivedCategory.standard
      (SheafOfModules.{u + 1} (ambientRingStructureSheaf B S hS 𝒳))
    ∀ H : DerivedCategory (SheafOfModules.{u + 1} (subsiteRingStructureSheaf B S hS 𝒳)),
      DerivedCategoryB.derivedCategoryB (flatQuasicoherentModulesSucc B S hS 𝒳) H →
        HasAffineDerivedSectionsBaseChange B S hS 𝒳
          ((derivedModuleLowerShriekSucc B S hS 𝒳).obj H)

Tag 0H16, a proposition

Tag 0H16 in the Stacks Project.

AlgebraicGeometry.Stack.FlatFppf.quasiCoherentDerivedEquivalenceSucc, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasiCoherentDerivedEquivalenceOfStack.lean, line 98.

Stacks 0H16. For an algebraic stack 𝒳, QC(𝒳) is canonically equivalent to D_QCoh(𝒪_𝒳), both at module universe u + 1 (see the module docstring for why u + 1): QC(𝒳) ≌ Q_𝒳 by Stacks 0H0X and 0H0C, Q_𝒳 = 𝒜 by Stacks 0H15, and 𝒜 ≌ D_QCoh(𝒪_𝒳) by Stacks 0H11, where D_QCoh(𝒪_𝒳) is the quotient of D_{LQCoh^fbc}(𝒪_𝒳) by D_{Parasitic ∩ LQCoh^fbc}(𝒪_𝒳) (Stacks 07B6).

def quasiCoherentDerivedEquivalenceSucc :
    quasiCoherentDerived.{u, u + 1, u, u + 1} B S hS 𝒳.val.val.p ≌
      DerivedCategory.KernelColocalization.quotient (parasiticModulesSucc B S hS 𝒳)
        (sheafFlatBaseChangeModulesSucc B E h S hS 𝒳)

Sources

• Section 104.8, Tag 0H12
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.FlatFppf.isZero_derivedSectionsFppf_of_parasitic_cohomology · AlgebraicGeometry.Stack.FlatFppf.isZero_cohomology_of_isZero_derivedSectionsFppf_flatAffine · AlgebraicGeometry.Stack.FlatFppf.hasAffineDerivedSectionsBaseChange_derivedModuleLowerShriekSucc · AlgebraicGeometry.Stack.FlatFppf.quasiCoherentDerivedEquivalenceSucc

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.