75.3 Generalities to 75.9 Induction principle

Section75.3 Generalities#

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

Tag 08GE, a lemma

Tag 08GE in the Stacks Project.

AlgebraicGeometry.Space.derivedModulePushforwardEtaleRestrictIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/DerivedPushforwardEtaleRestriction.lean, line 227.

Stacks 08GE. Let S be a scheme, let f : X ⟶ Y be a morphism of algebraic spaces over S, let g : Y' ⟶ Y be an étale morphism, set X' = Y' ×_Y X and let f' : X' ⟶ Y' be the projection. Then restricting the unbounded derived direct image along g agrees with taking the derived direct image along f' after restricting along i: (Rf_*E)|_{Y'} ≅ Rf'_*(E|_{X'}) for E in D(𝒪_X).

The four derived functors are arbitrary choices equipped with their canonical units, so the result applies in particular to the standard Rf_* of AlgebraicGeometry.Space.hasRightDerivedFunctor_modulePushforward and to the exact restriction functors. Extension by zero along i enters as data, for the reason recorded in the implementation notes of this file and in Stacks 08HA; it is the only such input, because on the Rf ⋙ Rg side exactness of restriction along g already makes the comparison invertible.

def derivedModulePushforwardEtaleRestrictIso (sq : IsPullback i f' f g)
    (hg : IsEtale B S hS g.hom)
    {iShriek : Modules.{u, u} B S hS X'.1 X'.2 ⥤ Modules.{u, u} B S hS X.1 X.2}
    (adji : iShriek ⊣ etaleModulePullback.{u, u} B S hS i
      (isEtale_of_isPullback B S hS f' i g f sq.flip hg))
    [iShriek.Additive] [PreservesFiniteLimits iShriek] [PreservesFiniteColimits iShriek]
    [HasDerivedCategory.{u + 1} (Modules.{u, u} B S hS X.1 X.2)]
    [HasDerivedCategory.{u + 1} (Modules.{u, u} B S hS Y.1 Y.2)]
    [HasDerivedCategory.{u + 1} (Modules.{u, u} B S hS X'.1 X'.2)]
    [HasDerivedCategory.{u + 1} (Modules.{u, u} B S hS Y'.1 Y'.2)]
    (Rf : DerivedCategory (Modules.{u, u} B S hS X.1 X.2) ⥤
      DerivedCategory (Modules.{u, u} B S hS Y.1 Y.2))
    (Rf' : DerivedCategory (Modules.{u, u} B S hS X'.1 X'.2) ⥤
      DerivedCategory (Modules.{u, u} B S hS Y'.1 Y'.2))
    (Ri : DerivedCategory (Modules.{u, u} B S hS X.1 X.2) ⥤
      DerivedCategory (Modules.{u, u} B S hS X'.1 X'.2))
    (Rg : DerivedCategory (Modules.{u, u} B S hS Y.1 Y.2) ⥤
      DerivedCategory (Modules.{u, u} B S hS Y'.1 Y'.2))
    (αf : (modulePushforward B S hS f).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rf)
    (αf' : (modulePushforward B S hS f').mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rf')
    (αi : (etaleModulePullback.{u, u} B S hS i
          (isEtale_of_isPullback B S hS f' i g f sq.flip hg)).mapHomotopyCategory
        (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Ri)
    (αg : (etaleModulePullback.{u, u} B S hS g hg).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rg)
    [Rf.IsRightDerivedFunctor αf
      (HomotopyCategory.quasiIso (Modules.{u, u} B S hS X.1 X.2) (ComplexShape.up ℤ))]
    [Rf'.IsRightDerivedFunctor αf'
      (HomotopyCategory.quasiIso (Modules.{u, u} B S hS X'.1 X'.2) (ComplexShape.up ℤ))]
    [Ri.IsRightDerivedFunctor αi
      (HomotopyCategory.quasiIso (Modules.{u, u} B S hS X.1 X.2) (ComplexShape.up ℤ))]
    [Rg.IsRightDerivedFunctor αg
      (HomotopyCategory.quasiIso (Modules.{u, u} B S hS Y.1 Y.2) (ComplexShape.up ℤ))] :
    Rf ⋙ Rg ≅ Ri ⋙ Rf'

AlgebraicGeometry.Space.derivedModulePushforwardEtaleRestrictIsoOfIsEtale, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/DerivedPushforwardEtaleRestrictionNoShriekData.lean, line 61.

Let S be a scheme, let f : X ⟶ Y be a morphism of algebraic spaces over S, let g : Y' ⟶ Y be an étale morphism, set X' = Y' ×_Y X (the square sq is cartesian) and let f' : X' ⟶ Y' be the projection. Then (Rf_*E)|_{Y'} ≅ Rf'_*(E|_{X'}) naturally in E ∈ D(𝒪_X), where Rf, Rf', Ri and Rg are any right derived functors of the direct images along f, f' and of the restrictions along i, g, with units αf, αf', αi and αg.

def derivedModulePushforwardEtaleRestrictIsoOfIsEtale (sq : IsPullback i f' f g)
    (hg : IsEtale B S hS g.hom)
    [HasDerivedCategory.{u + 1} (Modules.{u, u} B S hS X.1 X.2)]
    [HasDerivedCategory.{u + 1} (Modules.{u, u} B S hS Y.1 Y.2)]
    [HasDerivedCategory.{u + 1} (Modules.{u, u} B S hS X'.1 X'.2)]
    [HasDerivedCategory.{u + 1} (Modules.{u, u} B S hS Y'.1 Y'.2)]
    (Rf : DerivedCategory (Modules.{u, u} B S hS X.1 X.2) ⥤
      DerivedCategory (Modules.{u, u} B S hS Y.1 Y.2))
    (Rf' : DerivedCategory (Modules.{u, u} B S hS X'.1 X'.2) ⥤
      DerivedCategory (Modules.{u, u} B S hS Y'.1 Y'.2))
    (Ri : DerivedCategory (Modules.{u, u} B S hS X.1 X.2) ⥤
      DerivedCategory (Modules.{u, u} B S hS X'.1 X'.2))
    (Rg : DerivedCategory (Modules.{u, u} B S hS Y.1 Y.2) ⥤
      DerivedCategory (Modules.{u, u} B S hS Y'.1 Y'.2))
    (αf : (modulePushforward B S hS f).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rf)
    (αf' : (modulePushforward B S hS f').mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rf')
    (αi : (etaleModulePullback.{u, u} B S hS i
          (isEtale_of_isPullback B S hS f' i g f sq.flip hg)).mapHomotopyCategory
        (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Ri)
    (αg : (etaleModulePullback.{u, u} B S hS g hg).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rg)
    [Rf.IsRightDerivedFunctor αf
      (HomotopyCategory.quasiIso (Modules.{u, u} B S hS X.1 X.2) (ComplexShape.up ℤ))]
    [Rf'.IsRightDerivedFunctor αf'
      (HomotopyCategory.quasiIso (Modules.{u, u} B S hS X'.1 X'.2) (ComplexShape.up ℤ))]
    [Ri.IsRightDerivedFunctor αi
      (HomotopyCategory.quasiIso (Modules.{u, u} B S hS X.1 X.2) (ComplexShape.up ℤ))]
    [Rg.IsRightDerivedFunctor αg
      (HomotopyCategory.quasiIso (Modules.{u, u} B S hS Y.1 Y.2) (ComplexShape.up ℤ))] :
    Rf ⋙ Rg ≅ Ri ⋙ Rf'
Tag 08GF, a definition

Tag 08GF in the Stacks Project.

AlgebraicGeometry.Space.CohomologySupportedOn, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DerivedSupport.lean, line 77.

Stacks 08GF. An object E of D(𝒪_F) is supported on a subset T of |F| when every one of its cohomology sheaves Hⁱ(E) is supported on T.

noncomputable abbrev CohomologySupportedOn
    [HasSheafify (smallEtaleRingedSite B S hS F hF).J AddCommGrpCat.{m}]
    [(smallEtaleRingedSite B S hS F hF).J.WEqualsLocallyBijective AddCommGrpCat.{m}]
    (T : Set (points B S hS F))
    (E : DerivedCategory (Modules.{u, m} B S hS F hF)) : Prop
Sources
LeanAlgebraicGeometry.Space.derivedModulePushforwardEtaleRestrictIso · AlgebraicGeometry.Space.derivedModulePushforwardEtaleRestrictIsoOfIsEtale · AlgebraicGeometry.Space.CohomologySupportedOn

Section75.4 Derived category of quasi-coherent modules on the small étale site#

Section 75.4 of the Stacks Project, Tag 071P. 3 tags here are carried by 8 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 08H7, an equation

Tag 08H7 in the Stacks Project.

AlgebraicGeometry.Space.representedToSchemeZariskiRingedToposHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RepresentedSchemeZariskiRingedToposHom.lean, line 283. The tag is given by the attribute command at StacksFrontier/AlgebraicGeometry/Spaces/RepresentedSchemeZariskiRingedToposHom.lean, line 296. The attribute's comment: “the morphism ε of the displayed equation, as a morphism of ringed topoi, for the small étale site of an algebraic space represented by a scheme — the same ε as AlgebraicGeometry.SmallEtale.toZariskiAbstractRingedToposHom, read along the equivalence of that site with the small étale site of the representing scheme”.

ε : (X_étale, 𝒪_X) ⟶ (X_{0, Zar}, 𝒪_{X_0}) as a morphism of ringed topoi, for X = h_U the algebraic space represented by an object U of the big fppf site over S and X_0 the scheme underlying U.

This is Equation 75.4.0.1 of Stacks Section 75.4, read on the small étale site of the algebraic space: the composite of the equivalence of that site with the small étale site of X_0 (AlgebraicGeometry.Space.representedEtaleRingedToposHom) with the comparison AlgebraicGeometry.SmallEtale.toZariskiAbstractRingedToposHom of the small étale and small Zariski sites of X_0.

Being a morphism of ringed topoi, it carries ε⁻¹ on sheaves of commutative rings (AlgebraicGeometry.Space.representedZariskiInverseImageCommRing) and the inverse-image form ε⁻¹𝒪_{X_0} ⟶ 𝒪_X of its structure map (AlgebraicGeometry.Space.representedZariskiStructureSharpInverseImage), which is what the canonical map of Stacks 0D0X is built from.

public def representedToSchemeZariskiRingedToposHom :
    AlgebraicGeometry.RingedToposHom
      (smallEtaleRingedTopos B S hS (representedAlgebraicSpace B S hS U))
      ((BigFppfOver.toScheme B S hS).obj U).zariskiRingedTopos

Declarations registered for the tag:

Tag 08H8, a lemma

Tag 08H8 in the Stacks Project.

AlgebraicGeometry.SmallEtale.preservesFiniteLimits_associatedModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtaleExactAssociatedModule.lean, line 93. The attribute's comment: “the exactness assertion: ε^* : Mod(𝒪_S) → Mod(𝒪_étale) is left exact, hence exact, right exactness being automatic for a left adjoint. The flatness assertion is carried by isFlatMapULift_inverseImageStructureMap; the zero-detection assertion ε^*𝓕 = 0 ⟹ 𝓕 = 0 is not carried here, and is available for a quasi-coherent module as isZero_of_isZero_associatedModule”.

The exactness assertion of Stacks 08H8. The associated-module functor ε^* = (𝓕 ↦ 𝓕^a) of Stacks 03DU (4) at τ = étale is left exact.

Stacks 08H8 deduces this from flatness of ε, which is Stacks 0GNA; the criterion is Stacks 04JC, available for the pullback of sheaves of modules along the four-field morphism of ringed topoi attached to ε, and that pullback is ε^* by AlgebraicGeometry.RingedSite.HomGeneral.pullbackModulesToposIsoGeneral.

public theorem preservesFiniteLimits_associatedModule :
    PreservesFiniteLimits (associatedModule B S hS)

AlgebraicGeometry.SmallEtale.isZero_of_isZero_associatedModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtaleFiniteType.lean, line 532. The attribute's comment: “the zero-detection assertion ε^*𝓕 = 0 ⟹ 𝓕 = 0, for quasi-coherent 𝓕, by a route needing no exactness. The flatness assertion is isFlatMapULift_inverseImageStructureMap, the exactness assertion is preservesFiniteLimits_associatedModule, and zero detection for an arbitrary 𝒪_X-module is isZero_of_isZero_associatedModule_general.”.

Stacks 08H8, the zero-detection assertion, for quasi-coherent modules. A quasi-coherent 𝒪_X-module 𝓕 whose pullback ε^*𝓕 along the morphism of ringed sites ε : (X_étale, 𝒪) ⟶ (X_Zar, 𝒪_X) is a zero object is itself a zero object.

The unit of the associated-module adjunction is a monomorphism at 𝓕, and it factors through ε_*ε^*𝓕, which vanishes with ε^*𝓕; so the identity of 𝓕 vanishes. The source instead computes the stalk of ε^*𝓕 at a geometric point as 𝓕_x ⊗_{𝒪_{X, x}} 𝒪_{étale, x̄} and appeals to faithful flatness of the strict henselization. For an arbitrary 𝒪_X-module the assertion is AlgebraicGeometry.SmallEtale.isZero_of_isZero_associatedModule_general.

theorem isZero_of_isZero_associatedModule (F : X.Modules) [F.IsQuasicoherent]
    (h : IsZero ((associatedModule B X hX).obj F)) : IsZero F

AlgebraicGeometry.SmallEtale.isFlatMapULift_inverseImageStructureMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtaleFlatInverseImage.lean, line 354. The attribute's comment: “the flatness assertion: ε is a flat morphism of ringed sites. The exactness of ε^* : Mod(𝒪_X) → Mod(𝒪_étale) is carried by AlgebraicGeometry.SmallEtale.exactFunctor_pullbackModules_toZariski; the faithfulness assertion ε^*𝓕 = 0 ⟹ 𝓕 = 0 is not carried here and is not in the library”.

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

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

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

AlgebraicGeometry.SmallEtale.isRightAdjoint_toZariskiModulePushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtalePullbackExact.lean, line 143. The attribute's comment: “the existence assertion: the direct image ε_* of sheaves of modules along ε has a left adjoint, i.e. ε^* : Mod(𝒪_S) ⟶ Mod(𝒪_{S_étale}) exists. Both functors are taken in the sense of Stacks 03D6 for the two-field morphism of ringed topoi of Stacks 01D3 (2) carrying ε, which is the library's spelling of the pair; the left adjoint is AlgebraicGeometry.SmallEtale.toZariskiModulePullback”.

Stacks 08H8, the existence assertion. The direct image ε_* of sheaves of modules along ε = id_{small, étale, Zar} : S_étale → S_Zar has a left adjoint, i.e. the pullback ε^* : Mod(𝒪_S) ⟶ Mod(𝒪_{S_étale}) exists.

The left adjoint is AlgebraicGeometry.SmallEtale.toZariskiModulePullback and the adjunction exhibiting it is AlgebraicGeometry.SmallEtale.toZariskiModulePullbackAdjPushforward.

public theorem isRightAdjoint_toZariskiModulePushforward :
    (toZariskiModulePushforward B S hS).IsRightAdjoint

AlgebraicGeometry.SmallEtale.exactFunctor_pullbackModules_toZariski, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtalePullbackExact.lean, line 168. The attribute's comment: “the exactness assertion: ε^* : Mod(𝒪_S) ⟶ Mod(𝒪_{S_étale}) is exact, for ε the morphism of ringed topoi of Equation 75.4.0.1 in the two-field shape of Stacks 01D3 (2). The flatness assertion is carried by AlgebraicGeometry.SmallEtale.isFlatMapULift_inverseImageStructureMap; the implication ε^*𝓕 = 0 ⟹ 𝓕 = 0 is not carried here”.

Stacks 08H8, the exactness assertion. The pullback ε^* of sheaves of modules along ε = id_{small, étale, Zar} : S_étale → S_Zar is exact: it preserves finite limits and finite colimits.

The flatness assertion of the same tag is AlgebraicGeometry.SmallEtale.isFlatMapULift_inverseImageStructureMap, which is Stacks 0GNA; the remaining assertion, that ε^*𝓕 = 0 implies 𝓕 = 0, is not carried here.

public theorem exactFunctor_pullbackModules_toZariski :
    exactFunctor
      (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf S.zariskiRingedTopos.O))
      (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf (ringedTopos B S hS).O))
      (toZariskiModulePullback B S hS)

AlgebraicGeometry.SmallEtale.isZero_of_isZero_toZariskiModulePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtalePullbackExact.lean, line 290. The attribute's comment: “the faithfulness assertion: ε^*𝓕 = 0 ⟹ 𝓕 = 0, for ε^* the pullback of sheaves of modules of Stacks 03D6 (2) along the two-field morphism of ringed topoi of Stacks 01D3 (2) carrying ε. The flatness assertion is carried by AlgebraicGeometry.SmallEtale.isFlatMapULift_inverseImageStructureMap, the exactness assertion by AlgebraicGeometry.SmallEtale.exactFunctor_pullbackModules_toZariski and the existence assertion by AlgebraicGeometry.SmallEtale.isRightAdjoint_toZariskiModulePushforward”.

Stacks 08H8, the faithfulness assertion. If the pullback ε^*𝓕 of a sheaf of 𝒪_S-modules along ε = id_{small, étale, Zar} : S_étale → S_Zar vanishes, then 𝓕 vanishes.

The pullback is the inverse image of Stacks 03D2 followed by extension of scalars along the structure map, and the two halves are reflected separately. Extension of scalars reflects the zero sheaf because the structure map is locally faithfully flat over the comparison presheaf (f : V → S) ↦ 𝒪_S(f(V)) (AlgebraicGeometry.SmallEtale.locallyFaithfullyFlat_imageSectionsRestriction), and the inverse image reflects it by AlgebraicGeometry.SmallEtale.isZero_of_isZero_inverseImageModules.

public theorem isZero_of_isZero_toZariskiModulePullback
    (𝓕 : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf S.zariskiRingedTopos.O))
    (h : IsZero ((toZariskiModulePullback B S hS).obj 𝓕)) : IsZero 𝓕
Tag 071Q, a lemma

Tag 071Q in the Stacks Project.

AlgebraicGeometry.SmallEtale.derivedAssociatedModule_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtaleDerivedEquivalence.lean, line 524.

Stacks 071Q. For a scheme S, the functor ε^* : D_QCoh(𝒪_S) ⟶ D_QCoh(S_étale, 𝒪) induced by the exact functor ε^* of Stacks 08H8 is an equivalence.

The quasi-inverse is Rε_*, AlgebraicGeometry.SmallEtale.derivedRestrictModuleQcoh, as in the source: the adjunction ε^* ⊣ Rε_* restricts to the two derived categories with quasi-coherent cohomology, where its unit and counit are isomorphisms because H^q(Rε_* E) = ε_* H^q(E) for E with quasi-coherent cohomology (Stacks 03DW, 01XB and 0BKZ) and ε^* and ε_* are mutually inverse on quasi-coherent modules (Stacks 03DX).

theorem derivedAssociatedModule_isEquivalence :
    (derivedAssociatedModule.{w} B S hS).IsEquivalence
Sources
LeanAlgebraicGeometry.Space.representedToSchemeZariskiRingedToposHom · AlgebraicGeometry.SmallEtale.toZariskiRingedToposHom · AlgebraicGeometry.SmallEtale.preservesFiniteLimits_associatedModule · AlgebraicGeometry.SmallEtale.isZero_of_isZero_associatedModule · AlgebraicGeometry.SmallEtale.isFlatMapULift_inverseImageStructureMap · AlgebraicGeometry.SmallEtale.isRightAdjoint_toZariskiModulePushforward · AlgebraicGeometry.SmallEtale.exactFunctor_pullbackModules_toZariski · AlgebraicGeometry.SmallEtale.isZero_of_isZero_toZariskiModulePullback

Section75.5 Derived category of quasi-coherent modules#

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

Tag 071X, a definition

Tag 071X in the Stacks Project.

AlgebraicGeometry.Space.QuasicoherentDerivedCategory, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentDerivedCategory.lean, line 66.

Stacks 071X. The category D_QCoh(𝒪_F): the full subcategory of the unbounded derived category of 𝒪_F-modules whose objects have quasi-coherent cohomology sheaves in every degree.

noncomputable abbrev QuasicoherentDerivedCategory
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    [HasSheafify (smallEtaleRingedSite B S hS F hF).J AddCommGrpCat.{m}]
    [(smallEtaleRingedSite B S hS F hF).J.WEqualsLocallyBijective AddCommGrpCat.{m}]
Tag 08F1, an equation

Tag 08F1 in the Stacks Project.

AlgebraicGeometry.Space.quasicoherentDerivedComparisonSchemeUniverse, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentDerivedComparison.lean, line 302.

Stacks 08F1, the comparison functor D(QCoh(𝒪_F)) ⥤ D_QCoh(𝒪_F) of an algebraic space, with its 𝒪_F-modules taken at the universe of the schemes, where the source assumes them.

It has no open input. What the functor needs of Properties of Spaces, Lemma 03M1 — the lemma Stacks 08F1 points at for the comparison to make sense — is the closure of quasi-coherence under kernels, under cokernels and under finite direct sums, and all three hold at this universe: the kernel clause is AlgebraicGeometry.Space.isClosedUnderKernels_quasicoherentSheaves_schemeUniverse, the cokernel clause is AlgebraicGeometry.Space.isClosedUnderCokernels_quasicoherentSheaves, and the direct-sum clause is the instance SheafOfModules.isQuasicoherentOnSite_isClosedUnderFiniteProducts.

noncomputable def quasicoherentDerivedComparisonSchemeUniverse :
    letI := isClosedUnderKernels_quasicoherentSheaves_schemeUniverse B S hS F hF
    letI := isClosedUnderCokernels_quasicoherentSheaves B S hS F hF
    DerivedCategory (QuasicoherentSheaves.{u, u} B S hS F hF) ⥤
      QuasicoherentDerivedCategory.{u, u} B S hS F hF
Tag 08F2, a lemma

Tag 08F2 in the Stacks Project.

AlgebraicGeometry.Space.derivedQuasicoherent_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentDerivedEtaleLocal.lean, line 200.

Stacks 08F2. Let E be an object of D(𝒪_X) on an algebraic space X. The following are equivalent: E lies in D_QCoh(𝒪_X); Lφ^*E lies in D_QCoh(𝒪_U) for every étale scheme chart φ : U → X with U affine; the same for every étale scheme chart; the same for one étale scheme chart surjective on points; and Lf^*E lies in D_QCoh(𝒪_Y) for one étale morphism f : Y ⟶ X of algebraic spaces surjective on points.

All five are the corresponding conditions of Stacks 03M0 applied to the cohomology sheaves of E, the passage between Hⁿ(Lf^*E) and f^*(HⁿE) being AlgebraicGeometry.Space.derivedQuasicoherentPullback_iff.

theorem derivedQuasicoherent_tfae (E : DerivedCategory (Modules.{u, u} B S hS X.1 X.2)) :
    List.TFAE
      [DerivedCategoryB.derivedCategoryB
          (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
            ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS X.1 X.2).O))) E,
        ∀ A : SmallEtale B S hS X.1,
          IsAffine ((BigFppfOver.toScheme B S hS).obj ((SmallEtale.toOver B S hS X.1).obj A)) →
          DerivedQuasicoherentPullback B S hS (chartToSpace B S hS X A)
            (isEtale_chartToSpace B S hS X A) E,
        ∀ A : SmallEtale B S hS X.1,
          DerivedQuasicoherentPullback B S hS (chartToSpace B S hS X A)
            (isEtale_chartToSpace B S hS X A) E,
        ∃ A : SmallEtale B S hS X.1, IsSurjective B S hS A.1.hom ∧
          DerivedQuasicoherentPullback B S hS (chartToSpace B S hS X A)
            (isEtale_chartToSpace B S hS X A) E,
        ∃ (Z : AlgebraicSpaces B S hS) (g : Z ⟶ X) (hg : IsEtale B S hS g.hom),
          IsSurjective B S hS g.hom ∧ DerivedQuasicoherentPullback B S hS g hg E]
Tag 08F3, a lemma

Tag 08F3 in the Stacks Project.

AlgebraicGeometry.Space.hasCoproducts_quasicoherentDerivedCategory_ringUniverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentDerivedDirectSums.lean, line 173.

Stacks 08F3. Let F be an algebraic space over a scheme S contained in a big fppf site B. Then D_QCoh(𝒪_F), the derived category of 𝒪_F-modules with quasi-coherent cohomology, has direct sums.

The tag lands at the module universe u of the structure rings, because the ← direction of Descent, Proposition 03DX(2) is available only there, and at a free module universe the direct-sum clause of Stacks 03M1 would have to be assumed instead of proved.

This is AlgebraicGeometry.Space.hasCoproducts_quasicoherentDerivedCategory with its hypothesis discharged by AlgebraicGeometry.Space.isQuasicoherentOnSite_sigma_of_h03DX, fed with AlgebraicGeometry.Space.isQuasicoherentOnSite_iff_isCartesianOnAffineCharts.

theorem hasCoproducts_quasicoherentDerivedCategory_ringUniverse :
    HasCoproducts.{u} (QuasicoherentDerivedCategory.{u, u} B S hS F hF)
Tag 0D3E, a lemma

Tag 0D3E in the Stacks Project.

AlgebraicGeometry.Space.isDerivedLimit_single_limit_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentDerivedLimits.lean, line 260. The attribute's comment: “clause (2): R lim H^q(K_n) = lim H^q(K_n); the source's two citations are carried as the named hypotheses hcover (the affine étale charts cover the small étale site) and h03DWab, h03DWepi (Stacks 03DW on an affine étale chart: vanishing of higher cohomology, and surjectivity on sections, for quasi-coherent modules)”.

Stacks Project, Tag 0D3E, clause (2). Let (K_n) be an inverse system of D_QCoh(𝒪_X) on an algebraic space X whose transition maps H^q(K_{n+1}) ⟶ H^q(K_n) on cohomology sheaves are surjective. Then R lim H^q(K_n) = lim H^q(K_n): the ordinary inverse limit of the degree-q cohomology sheaves, placed in degree zero, is a derived inverse limit of the system of those sheaves.

This is the first conclusion of Tag 0BKY, Stacks.Cohomology.SiteInverseLimits.isDerivedLimit_single_limit_of_acyclic_cover, on the small étale site of X.

theorem isDerivedLimit_single_limit_homology
    (K : ℕᵒᵖ ⥤ DerivedCategory (Modules.{u, m} B S hS F hF))
    (hqc : ∀ (n : ℕ) (q : ℤ), ((DerivedCategory.homologyFunctor
      (Modules.{u, m} B S hS F hF) q).obj (K.obj ⟨n⟩)).IsQuasicoherentOnSite)
    (hsurj : ∀ (n : ℕ) (q : ℤ), Epi ((DerivedCategory.homologyFunctor
      (Modules.{u, m} B S hS F hF) q).map (K.map (homOfLE (Nat.le_succ n)).op)))
    (hcover : (smallEtaleRingedSite B S hS F hF).J.HasEnoughObjects
      (IsAffineChart B S hS F))
    (h03DWab : ∀ U : SmallEtale B S hS F, IsAffineChart B S hS F U →
      ∀ M : Modules.{u, m} B S hS F hF, M.IsQuasicoherentOnSite → ∀ p : ℕ, 0 < p →
        IsZero (((Stacks.Cohomology.SiteInverseLimits.sectionsFunctor
          (smallEtaleRingedSite B S hS F hF) U).rightDerived p).obj M))
    (h03DWepi : ∀ U : SmallEtale B S hS F, IsAffineChart B S hS F U →
      ∀ M N : Modules.{u, m} B S hS F hF, M.IsQuasicoherentOnSite → N.IsQuasicoherentOnSite →
      ∀ f : M ⟶ N, Epi f →
        Epi ((Stacks.Cohomology.SiteInverseLimits.sectionsFunctor
          (smallEtaleRingedSite B S hS F hF) U).map f))
    (q : ℤ) :
    ∃ h : HasProduct (fun n : ℕ =>
        ((K ⋙ DerivedCategory.homologyFunctor (Modules.{u, m} B S hS F hF) q) ⋙
          DerivedCategory.singleFunctor (Modules.{u, m} B S hS F hF) 0).obj ⟨n⟩),
      @IsDerivedLimit (DerivedCategory (Modules.{u, m} B S hS F hF)) _ _ _ _ _ _
        ((K ⋙ DerivedCategory.homologyFunctor (Modules.{u, m} B S hS F hF) q) ⋙
          DerivedCategory.singleFunctor (Modules.{u, m} B S hS F hF) 0) h
        ((DerivedCategory.singleFunctor (Modules.{u, m} B S hS F hF) 0).obj
          (limit (K ⋙ DerivedCategory.homologyFunctor
            (Modules.{u, m} B S hS F hF) q)))

AlgebraicGeometry.Space.isZero_cohomology_limit_homology_of_isAffineChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentDerivedLimits.lean, line 307. The attribute's comment: “clause (3): H^p(U, lim H^q(K_n)) = 0 for p > 0 and U an affine étale chart; the source's two citations are carried as the named hypotheses hcover (the affine étale charts cover the small étale site) and h03DWab, h03DWepi (Stacks 03DW on an affine étale chart: vanishing of higher cohomology, and surjectivity on sections, for quasi-coherent modules)”.

Stacks Project, Tag 0D3E, clause (3). Under the same hypotheses, for every affine étale chart U of X and every p > 0 we have H^p(U, lim H^q(K_n)) = 0.

This is the second conclusion of Tag 0BKY, Stacks.Cohomology.SiteInverseLimits.isZero_cohomology_limit_of_acyclic_cover, on the small étale site of X. The source states the vanishing for an affine open of X; every affine open is an affine object of the small étale site, and the statement is given for all of them, as the source's own proof does.

theorem isZero_cohomology_limit_homology_of_isAffineChart
    (K : ℕᵒᵖ ⥤ DerivedCategory (Modules.{u, m} B S hS F hF))
    (hqc : ∀ (n : ℕ) (q : ℤ), ((DerivedCategory.homologyFunctor
      (Modules.{u, m} B S hS F hF) q).obj (K.obj ⟨n⟩)).IsQuasicoherentOnSite)
    (hsurj : ∀ (n : ℕ) (q : ℤ), Epi ((DerivedCategory.homologyFunctor
      (Modules.{u, m} B S hS F hF) q).map (K.map (homOfLE (Nat.le_succ n)).op)))
    (hcover : (smallEtaleRingedSite B S hS F hF).J.HasEnoughObjects
      (IsAffineChart B S hS F))
    (h03DWab : ∀ U : SmallEtale B S hS F, IsAffineChart B S hS F U →
      ∀ M : Modules.{u, m} B S hS F hF, M.IsQuasicoherentOnSite → ∀ p : ℕ, 0 < p →
        IsZero (((Stacks.Cohomology.SiteInverseLimits.sectionsFunctor
          (smallEtaleRingedSite B S hS F hF) U).rightDerived p).obj M))
    (h03DWepi : ∀ U : SmallEtale B S hS F, IsAffineChart B S hS F U →
      ∀ M N : Modules.{u, m} B S hS F hF, M.IsQuasicoherentOnSite → N.IsQuasicoherentOnSite →
      ∀ f : M ⟶ N, Epi f →
        Epi ((Stacks.Cohomology.SiteInverseLimits.sectionsFunctor
          (smallEtaleRingedSite B S hS F hF) U).map f))
    (q : ℤ) (U : SmallEtale B S hS F) (hU : IsAffineChart B S hS F U)
    (p : ℕ) (hp : 0 < p) :
    IsZero (((Stacks.Cohomology.SiteInverseLimits.sectionsFunctor
      (smallEtaleRingedSite B S hS F hF) U).rightDerived p).obj
      (limit (K ⋙ DerivedCategory.homologyFunctor
        (Modules.{u, m} B S hS F hF) q)))

AlgebraicGeometry.Space.isLimit_cohomology_of_isDerivedLimit_of_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentDerivedLimitsCohomology.lean, line 198. The attribute's comment: “clause (1): H^q(R lim K_n) = lim H^q(K_n), as the canonical limiting cone; the source's citation 0A09 is applied with its hypotheses on the affine étale charts of the space discharged (they cover the small étale site; a quasi-coherent module is acyclic on one; a surjection of quasi-coherent modules is surjective on its sections there). The module universe is the universe of the structure rings”.

Stacks Project, Tag 0D3E, clause (1). Let S be a scheme, let X be an algebraic space over S and let (K_n) be an inverse system in D_QCoh(𝒪_X) whose transition maps H^q(K_{n+1}) ⟶ H^q(K_n) on cohomology sheaves are surjective. If L is a derived inverse limit of the system then H^q(L) = lim H^q(K_n): the cone on the degree-q cohomology sheaves whose legs are induced by the projections of a derived-limit triangle for L is a limit cone.

This is Tag 0A09 — Stacks.Cohomology.DerivedLimitAcyclic.LargeSite.isLimit_cohomology_of_isDerivedLimit, its content with Tag 0BKZ supplied on a site whose objects live above its morphisms — on the small étale site of X, with the source's two checks on the affine objects of that site discharged: the affine étale charts cover it, and a quasi-coherent module both is acyclic on an affine chart and receives surjections on its sections there, which makes each tower of sections Mittag-Leffler and kills its first derived inverse limit.

theorem isLimit_cohomology_of_isDerivedLimit_of_epi
    (K : ℕᵒᵖ ⥤ DerivedCategory (Modules.{u, u} B S hS F hF))
    (hqc : ∀ (n : ℕ) (q : ℤ), ((DerivedCategory.homologyFunctor
      (Modules.{u, u} B S hS F hF) q).obj (K.obj ⟨n⟩)).IsQuasicoherentOnSite)
    (hsurj : ∀ (n : ℕ) (q : ℤ), Epi ((DerivedCategory.homologyFunctor
      (Modules.{u, u} B S hS F hF) q).map (K.map (homOfLE (Nat.le_succ n)).op)))
    (L : DerivedCategory (Modules.{u, u} B S hS F hF))
    (hL : IsDerivedLimit K L) (q : ℤ) :
    ∃ p : L ⟶ ∏ᶜ fun n : ℕ ↦ K.obj ⟨n⟩,
      (∃ δ : (∏ᶜ fun n : ℕ ↦ K.obj ⟨n⟩) ⟶ L⟦(1 : ℤ)⟧,
        Triangle.mk p (Pi.lift fun n : ℕ ↦
          Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) n -
            Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) (n + 1) ≫
              K.map (homOfLE (Nat.le_succ n)).op) δ ∈
          distTriang (DerivedCategory (Modules.{u, u} B S hS F hF))) ∧
      ∃ τ : (Functor.const ℕᵒᵖ).obj
          ((DerivedCategory.homologyFunctor (Modules.{u, u} B S hS F hF) q).obj L) ⟶
          K ⋙ DerivedCategory.homologyFunctor (Modules.{u, u} B S hS F hF) q,
        (∀ n : ℕ, τ.app ⟨n⟩ =
          (DerivedCategory.homologyFunctor (Modules.{u, u} B S hS F hF) q).map
            (p ≫ Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) n)) ∧
        Nonempty (IsLimit (Cone.mk _ τ))

AlgebraicGeometry.Space.isDerivedLimit_single_limit_homology_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentDerivedLimitsCohomology.lean, line 244. The attribute's comment: “clause (2): R lim H^q(K_n) = lim H^q(K_n); the source's citations are applied with their hypotheses on the affine étale charts of the space discharged (they cover the small étale site; a quasi-coherent module is acyclic on one; a surjection of quasi-coherent modules is surjective on its sections there). The module universe is the universe of the structure rings”.

Stacks Project, Tag 0D3E, clause (2). Under the same hypotheses, R lim H^q(K_n) = lim H^q(K_n): the ordinary inverse limit of the degree-q cohomology sheaves, placed in degree zero, is a derived inverse limit of the system of those sheaves.

This is AlgebraicGeometry.Space.isDerivedLimit_single_limit_homology with its three named hypotheses supplied: hcover by AlgebraicGeometry.Space.hasEnoughObjects_isAffineChart, h03DWab by AlgebraicGeometry.Space.isZero_rightDerived_sectionsFunctor_of_isAffineChart and h03DWepi by AlgebraicGeometry.Space.epi_sectionsFunctor_map_of_isQuasicoherentOnSite.

theorem isDerivedLimit_single_limit_homology_unconditional
    (K : ℕᵒᵖ ⥤ DerivedCategory (Modules.{u, u} B S hS F hF))
    (hqc : ∀ (n : ℕ) (q : ℤ), ((DerivedCategory.homologyFunctor
      (Modules.{u, u} B S hS F hF) q).obj (K.obj ⟨n⟩)).IsQuasicoherentOnSite)
    (hsurj : ∀ (n : ℕ) (q : ℤ), Epi ((DerivedCategory.homologyFunctor
      (Modules.{u, u} B S hS F hF) q).map (K.map (homOfLE (Nat.le_succ n)).op)))
    (q : ℤ) :
    ∃ h : HasProduct (fun n : ℕ =>
        ((K ⋙ DerivedCategory.homologyFunctor (Modules.{u, u} B S hS F hF) q) ⋙
          DerivedCategory.singleFunctor (Modules.{u, u} B S hS F hF) 0).obj ⟨n⟩),
      @IsDerivedLimit (DerivedCategory (Modules.{u, u} B S hS F hF)) _ _ _ _ _ _
        ((K ⋙ DerivedCategory.homologyFunctor (Modules.{u, u} B S hS F hF) q) ⋙
          DerivedCategory.singleFunctor (Modules.{u, u} B S hS F hF) 0) h
        ((DerivedCategory.singleFunctor (Modules.{u, u} B S hS F hF) 0).obj
          (limit (K ⋙ DerivedCategory.homologyFunctor
            (Modules.{u, u} B S hS F hF) q)))

AlgebraicGeometry.Space.isZero_cohomology_limit_homology_of_isAffineChart_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentDerivedLimitsCohomology.lean, line 280. The attribute's comment: “clause (3): H^p(U, lim H^q(K_n)) = 0 for p > 0 and U an affine étale chart; the source's citations are applied with their hypotheses on the affine étale charts of the space discharged (they cover the small étale site; a quasi-coherent module is acyclic on one; a surjection of quasi-coherent modules is surjective on its sections there). The module universe is the universe of the structure rings”.

Stacks Project, Tag 0D3E, clause (3). Under the same hypotheses, for every affine étale chart U of X and every p > 0 we have H^p(U, lim H^q(K_n)) = 0.

This is AlgebraicGeometry.Space.isZero_cohomology_limit_homology_of_isAffineChart with its three named hypotheses supplied, exactly as in AlgebraicGeometry.Space.isDerivedLimit_single_limit_homology_unconditional. The source states the vanishing for an affine open of X; every affine open is an affine object of the small étale site, and the statement is given for all of them, as the source's own proof is.

theorem isZero_cohomology_limit_homology_of_isAffineChart_unconditional
    (K : ℕᵒᵖ ⥤ DerivedCategory (Modules.{u, u} B S hS F hF))
    (hqc : ∀ (n : ℕ) (q : ℤ), ((DerivedCategory.homologyFunctor
      (Modules.{u, u} B S hS F hF) q).obj (K.obj ⟨n⟩)).IsQuasicoherentOnSite)
    (hsurj : ∀ (n : ℕ) (q : ℤ), Epi ((DerivedCategory.homologyFunctor
      (Modules.{u, u} B S hS F hF) q).map (K.map (homOfLE (Nat.le_succ n)).op)))
    (q : ℤ) (U : SmallEtale B S hS F) (hU : IsAffineChart B S hS F U)
    (p : ℕ) (hp : 0 < p) :
    IsZero (((Stacks.Cohomology.SiteInverseLimits.sectionsFunctor
      (smallEtaleRingedSite B S hS F hF) U).rightDerived p).obj
      (limit (K ⋙ DerivedCategory.homologyFunctor
        (Modules.{u, u} B S hS F hF) q)))
Tag 08F4, a lemma

Tag 08F4 in the Stacks Project.

AlgebraicGeometry.Space.derivedQuasicoherent_etaleModulePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentDerivedEtalePullback.lean, line 86. The attribute's comment: “for étale morphisms of algebraic spaces”.

Stacks 08F4 for an étale morphism of algebraic spaces. If E is an object of D(𝒪_X) all of whose cohomology sheaves are quasi-coherent and f : Y ⟶ X is étale, then every cohomology sheaf of Lf^*E is quasi-coherent.

The étale pullback is exact, so Hⁿ(Lf^*E) ≅ f^*(HⁿE), and f^* preserves quasi-coherence of a module by the (1) ⟹ (2) direction of Stacks 03M0.

theorem derivedQuasicoherent_etaleModulePullback (f : Y ⟶ X) (hf : IsEtale B S hS f.hom)
    (E : DerivedCategory (Modules.{u, u} B S hS X.1 X.2))
    (hE : DerivedCategoryB.derivedCategoryB
      (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
        ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS X.1 X.2).O))) E) :
    DerivedCategoryB.derivedCategoryB
      (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
        ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS Y.1 Y.2).O)))
      ((etaleModulePullback B S hS f hf).mapDerivedCategory.obj E)

AlgebraicGeometry.Space.quasicoherentDerivedEtalePullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentDerivedEtalePullback.lean, line 103. The attribute's comment: “for étale morphisms of algebraic spaces, the restriction D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_Y)”.

Stacks 08F4 for an étale morphism of algebraic spaces, as a functor. The derived pullback along an étale morphism f : Y ⟶ X restricts to a functor D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_Y) between the derived categories of complexes with quasi-coherent cohomology.

noncomputable def quasicoherentDerivedEtalePullback (f : Y ⟶ X) (hf : IsEtale B S hS f.hom) :
    QuasicoherentDerivedCategory.{u, u} B S hS X.1 X.2 ⥤
      QuasicoherentDerivedCategory.{u, u} B S hS Y.1 Y.2

AlgebraicGeometry.Space.derivedQuasicoherent_smallEtaleDerivedModulePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentDerivedPullback.lean, line 188.

Let f : Y ⟶ X be a morphism of algebraic spaces over S. The derived pullback Lf^*, the total left derived functor AlgebraicGeometry.Space.smallEtaleDerivedModulePullback of degreewise pullback along the morphism of small étale ringed topoi of f, sends D_QCoh(𝒪_X) into D_QCoh(𝒪_Y): if every cohomology sheaf of E ∈ D(𝒪_X) is quasi-coherent, then so is every cohomology sheaf of Lf^*E.

theorem derivedQuasicoherent_smallEtaleDerivedModulePullback (f : Y ⟶ X)
    (E : DerivedCategory (SheafOfModules.{u} (ringedToposStructureRingSheaf B S hS X)))
    (hE : DerivedCategoryB.derivedCategoryB
      (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
        ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS X.1 X.2).O))) E) :
    DerivedCategoryB.derivedCategoryB
      (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
        ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS Y.1 Y.2).O)))
      ((smallEtaleDerivedModulePullback B S hS f).obj E)

AlgebraicGeometry.Space.quasicoherentDerivedPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentDerivedPullback.lean, line 227. The attribute's comment: “the restriction D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_Y) of Lf^*, for an arbitrary morphism”.

The derived pullback Lf^* along an arbitrary morphism f : Y ⟶ X of algebraic spaces restricts to a functor D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_Y) between the full subcategories of complexes with quasi-coherent cohomology (Stacks 071X).

noncomputable def quasicoherentDerivedPullback (f : Y ⟶ X) :
    (DerivedCategoryB.derivedCategoryB
        (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
          ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS X.1 X.2).O))) :
      ObjectProperty (DerivedCategory
        (SheafOfModules.{u} (ringedToposStructureRingSheaf B S hS X)))).FullSubcategory ⥤
    (DerivedCategoryB.derivedCategoryB
        (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
          ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS Y.1 Y.2).O))) :
      ObjectProperty (DerivedCategory
        (SheafOfModules.{u} (ringedToposStructureRingSheaf B S hS Y)))).FullSubcategory
Tag 08F5, a lemma

Tag 08F5 in the Stacks Project.

AlgebraicGeometry.Space.derivedQuasicoherent_derivedTensor_single, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentDerivedTensor.lean, line 319. The attribute's comment: “the case of two quasi-coherent modules placed in degree zero, the left one K-flat”.

Stacks 08F5 for two quasi-coherent modules placed in degree zero, the left one K-flat. Let X be an algebraic space, let T be a derived tensor product on 𝒪_X, and let M and N be quasi-coherent 𝒪_X-modules with M[0] K-flat. Then M[0] ⊗^L_{𝒪_X} N[0] lies in D_QCoh(𝒪_X).

Membership in D_QCoh(𝒪_X) is the object property DerivedCategoryB.derivedCategoryB for quasi-coherence that AlgebraicGeometry.Space.QuasicoherentDerivedCategory of Stacks 071X is the full subcategory on, so no new predicate appears. The content is Stacks.SheafOfModules.DerivedTensorProduct.isQuasicoherentOnSite_homology_tensor_single on the small étale ringed site of X; the general case of Stacks 08F5 is not proved, and the module docstring records the four missing inputs.

theorem derivedQuasicoherent_derivedTensor_single
    (T : DerivedTensorProduct.{u + 1, u, u, d} (smallEtaleRingedSite B S hS F hF))
    (M N : Modules.{u, u} B S hS F hF)
    (hM : Stacks.SheafOfModules.IsKFlat (smallEtaleRingedSite B S hS F hF).O
      ((CochainComplex.singleFunctor (Modules.{u, u} B S hS F hF) 0).obj M))
    (hMq : M.IsQuasicoherentOnSite) (hNq : N.IsQuasicoherentOnSite) :
    DerivedCategoryB.derivedCategoryB
      (_root_.SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
        ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS F hF).O)))
      ((T.tensor.obj
          ((DerivedCategory.singleFunctor (Modules.{u, u} B S hS F hF) 0).obj M)).obj
        ((DerivedCategory.singleFunctor (Modules.{u, u} B S hS F hF) 0).obj N))

AlgebraicGeometry.Space.derivedQuasicoherent_derivedTensor_single', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentDerivedTensor.lean, line 337. The attribute's comment: “the case of two quasi-coherent modules placed in degree zero, the right one K-flat”.

Stacks 08F5 for two quasi-coherent modules placed in degree zero, the right one K-flat. The mirror of AlgebraicGeometry.Space.derivedQuasicoherent_derivedTensor_single, read through Stacks.SheafOfModules.DerivedTensorProduct.isQuasicoherentOnSite_homology_tensor_single'.

theorem derivedQuasicoherent_derivedTensor_single'
    (T : DerivedTensorProduct.{u + 1, u, u, d} (smallEtaleRingedSite B S hS F hF))
    (M N : Modules.{u, u} B S hS F hF)
    (hN : Stacks.SheafOfModules.IsKFlat (smallEtaleRingedSite B S hS F hF).O
      ((CochainComplex.singleFunctor (Modules.{u, u} B S hS F hF) 0).obj N))
    (hMq : M.IsQuasicoherentOnSite) (hNq : N.IsQuasicoherentOnSite) :
    DerivedCategoryB.derivedCategoryB
      (_root_.SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
        ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS F hF).O)))
      ((T.tensor.obj
          ((DerivedCategory.singleFunctor (Modules.{u, u} B S hS F hF) 0).obj M)).obj
        ((DerivedCategory.singleFunctor (Modules.{u, u} B S hS F hF) 0).obj N))

AlgebraicGeometry.Space.derivedQuasicoherent_derivedTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentDerivedTensorArbitrary.lean, line 214.

Stacks 08F5. Let X be an algebraic space over a scheme S. For objects K, L of D_QCoh(𝒪_X) the derived tensor product K ⊗^𝐋_{𝒪_X} L is in D_QCoh(𝒪_X).

Here 𝒪_X-modules are the sheaves of modules on the small étale ringed site of X, D_QCoh(𝒪_X) is AlgebraicGeometry.Space.QuasicoherentDerivedCategory of Stacks 071X, the full subcategory of the unbounded derived category on the objects with quasi-coherent cohomology sheaves, and ⊗^𝐋_{𝒪_X} is an arbitrary derived tensor product datum T on that ringed site — for instance the canonical one, Stacks.SheafOfModules.canonicalDerivedTensorProduct of Stacks 06YU. K and L are arbitrary objects of D_QCoh(𝒪_X), with no boundedness.

The proof represents K by a K-flat complex P (Stacks 06YS) and L by any complex L', so that K ⊗^𝐋 L ≅ Q(Tot(P ⊗ L')) by the K-flat comparison of T, and concludes by AlgebraicGeometry.Space.isQuasicoherentOnSite_homology_tensorComplex; see the module docstring.

theorem derivedQuasicoherent_derivedTensor
    (T : Stacks.SheafOfModules.DerivedTensorProduct.{u + 1, u, u, u + 1}
      (smallEtaleRingedSite B S hS F hF))
    (K L : QuasicoherentDerivedCategory.{u, u} B S hS F hF) :
    DerivedCategoryB.derivedCategoryB
      (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
        ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS F hF).O)))
      ((T.tensor.obj K.obj).obj L.obj)

AlgebraicGeometry.Space.qcohDerived_smallEtaleDerivedTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentDerivedTensorClosed.lean, line 136.

Stacks 08F5. Let X be an algebraic space over a scheme S. For objects K, L of D_QCoh(𝒪_X) the derived tensor product K ⊗^L_{𝒪_X} L is in D_QCoh(𝒪_X).

theorem qcohDerived_smallEtaleDerivedTensor (X : AlgebraicSpaces B S hS)
    (K L : DerivedCategory (Modules.{u, u} B S hS X.1 X.2))
    (hK : QcohDerived B S hS X K) (hL : QcohDerived B S hS X L) :
    QcohDerived B S hS X (((smallEtaleDerivedTensor B S hS X).obj K).obj L)
Tag 08F6, a lemma

Tag 08F6 in the Stacks Project.

AlgebraicGeometry.Space.isIso_of_isDerivedLimit_truncGETower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentDerivedLimits.lean, line 203. The attribute's comment: “the source's proof, with its two citations carried as the named hypotheses hcover (the affine étale charts cover the small étale site) and h03DW (Stacks 03DW: a quasi-coherent module has no higher cohomology on an affine étale chart)”.

Stacks Project, Tag 08F6. Let S be a scheme, let X be an algebraic space over S and let E be an object of D_QCoh(𝒪_X). Then the canonical map from E to a derived limit L of the tower n ↦ τ_{≥ -n} E of canonical truncations from below is an isomorphism.

The derived limit is presented by its structural morphism p to the product of the tower and the distinguished triangle hL characterising it; the map c out of E is the canonical one because its composites with the product projections are required to be the truncation maps.

This is Spaltenstein's local criterion in the form Stacks.Cohomology.AcyclicCover.isIso_to_isDerivedLimit_truncGETower_of_acyclic, Tag 0D6P with d = 0, applied on the small étale site of X: the affine étale charts cover it, which is the hypothesis hcover, and a quasi-coherent module has no higher cohomology on an affine chart, which is the hypothesis h03DW.

theorem isIso_of_isDerivedLimit_truncGETower
    [EnoughInjectives (Modules.{u, m} B S hS F hF)]
    (E : DerivedCategory (Modules.{u, m} B S hS F hF))
    (hE : ∀ q : ℤ, ((DerivedCategory.homologyFunctor
      (Modules.{u, m} B S hS F hF) q).obj E).IsQuasicoherentOnSite)
    (hcover : (smallEtaleRingedSite B S hS F hF).J.HasEnoughObjects
      (IsAffineChart B S hS F))
    (h03DW : ∀ U : SmallEtale B S hS F, IsAffineChart B S hS F U →
      ∀ M : Modules.{u, m} B S hS F hF, M.IsQuasicoherentOnSite → ∀ p : ℕ, 0 < p →
        IsZero (((SheafOfModules.evaluation.{m}
          (Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS F hF).O)
          (op U)).rightDerived p).obj M))
    [HasProduct fun n : ℕ ↦ (Stacks.DerivedLimit.truncGETower
      (Modules.{u, m} B S hS F hF) E).obj ⟨n⟩]
    (L : DerivedCategory (Modules.{u, m} B S hS F hF))
    (c : E ⟶ L)
    (p : L ⟶ ∏ᶜ fun n : ℕ ↦ (Stacks.DerivedLimit.truncGETower
      (Modules.{u, m} B S hS F hF) E).obj ⟨n⟩)
    (δ : (∏ᶜ fun n : ℕ ↦ (Stacks.DerivedLimit.truncGETower
      (Modules.{u, m} B S hS F hF) E).obj ⟨n⟩) ⟶ L⟦(1 : ℤ)⟧)
    (hL : Triangle.mk p (Pi.lift fun n : ℕ ↦
      Pi.π (fun n : ℕ ↦ (Stacks.DerivedLimit.truncGETower
        (Modules.{u, m} B S hS F hF) E).obj ⟨n⟩) n -
        Pi.π (fun n : ℕ ↦ (Stacks.DerivedLimit.truncGETower
          (Modules.{u, m} B S hS F hF) E).obj ⟨n⟩) (n + 1) ≫
          (Stacks.DerivedLimit.truncGETower
            (Modules.{u, m} B S hS F hF) E).map (homOfLE (Nat.le_succ n)).op) δ ∈
        distTriang (DerivedCategory (Modules.{u, m} B S hS F hF)))
    (hc : ∀ n : ℕ, c ≫ p ≫ Pi.π (fun n : ℕ ↦ (Stacks.DerivedLimit.truncGETower
      (Modules.{u, m} B S hS F hF) E).obj ⟨n⟩) n =
        (DerivedCategory.TStructure.t.truncGEπ (-(n : ℤ))).app E) :
    IsIso c

AlgebraicGeometry.Space.isIso_of_isDerivedLimit_truncGETower_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentDerivedLimitsUnconditional.lean, line 81. The attribute's comment: “the source's statement, with both of its citations discharged: the affine étale charts cover the small étale site (04JS, at the index universe HasEnoughObjects asks for) and a quasi-coherent module has no higher cohomology on an affine étale chart (the étale-site analogue of 01XB that the source cites 03DW for). The module universe is the universe of the structure rings”.

Stacks Project, Tag 08F6, with no hypothesis. Let S be a scheme, let X be an algebraic space over S and let E be an object of D_QCoh(𝒪_X). Then the canonical map from E to a derived limit L of the tower n ↦ τ_{≥ -n} E of canonical truncations from below is an isomorphism.

This is AlgebraicGeometry.Space.isIso_of_isDerivedLimit_truncGETower with its two named hypotheses discharged: hcover by AlgebraicGeometry.Space.hasEnoughObjects_isAffineChart and h03DW by AlgebraicGeometry.Space.isZero_rightDerived_evaluation_of_isAffineChart. As there, the derived limit is presented by its structural morphism p to the product of the tower together with the distinguished triangle hL characterising it, and the map c out of E is the canonical one because its composites with the product projections are required to be the truncation maps.

theorem isIso_of_isDerivedLimit_truncGETower_unconditional
    (E : DerivedCategory (Modules.{u, u} B S hS F hF))
    (hE : ∀ q : ℤ, ((DerivedCategory.homologyFunctor
      (Modules.{u, u} B S hS F hF) q).obj E).IsQuasicoherentOnSite)
    [HasProduct fun n : ℕ ↦ (Stacks.DerivedLimit.truncGETower
      (Modules.{u, u} B S hS F hF) E).obj ⟨n⟩]
    (L : DerivedCategory (Modules.{u, u} B S hS F hF))
    (c : E ⟶ L)
    (p : L ⟶ ∏ᶜ fun n : ℕ ↦ (Stacks.DerivedLimit.truncGETower
      (Modules.{u, u} B S hS F hF) E).obj ⟨n⟩)
    (δ : (∏ᶜ fun n : ℕ ↦ (Stacks.DerivedLimit.truncGETower
      (Modules.{u, u} B S hS F hF) E).obj ⟨n⟩) ⟶ L⟦(1 : ℤ)⟧)
    (hL : Triangle.mk p (Pi.lift fun n : ℕ ↦
      Pi.π (fun n : ℕ ↦ (Stacks.DerivedLimit.truncGETower
        (Modules.{u, u} B S hS F hF) E).obj ⟨n⟩) n -
        Pi.π (fun n : ℕ ↦ (Stacks.DerivedLimit.truncGETower
          (Modules.{u, u} B S hS F hF) E).obj ⟨n⟩) (n + 1) ≫
          (Stacks.DerivedLimit.truncGETower
            (Modules.{u, u} B S hS F hF) E).map (homOfLE (Nat.le_succ n)).op) δ ∈
        distTriang (DerivedCategory (Modules.{u, u} B S hS F hF)))
    (hc : ∀ n : ℕ, c ≫ p ≫ Pi.π (fun n : ℕ ↦ (Stacks.DerivedLimit.truncGETower
      (Modules.{u, u} B S hS F hF) E).obj ⟨n⟩) n =
        (DerivedCategory.TStructure.t.truncGEπ (-(n : ℤ))).app E) :
    IsIso c
Tag 08F7, a lemma

Tag 08F7 in the Stacks Project.

AlgebraicGeometry.Space.isZero_homology_rightDerived_of_isZero_lt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentDerivedFunctorAmplitude.lean, line 132. The attribute's comment: “the i < a half of assertion (3); the upper bound b + N - 1, where the integer N and the hypotheses (2), (3) on F enter, is not proved — it needs the clause q > 0 of Stacks 03DW, which this repository does not carry”.

Stacks 08F7, the i < a half of assertion (3). Let S be a scheme, let X be an algebraic space over S, let F : Mod(𝒪_X) ⥤ Ab be an additive functor and let (RF, α) be a right derived functor of F on D(𝒪_X). Let E be an object of D_QCoh(𝒪_X) with H ^ j (E) = 0 for j < a. Then H ^ i (RF E) = 0 for i < a.

This is the half of assertion (3) that bounds RF E from below. The source gets it from assertion (1); here it is the left t-exactness of a right derived functor out of a Grothendieck abelian category with enough injectives, Stacks.SmallDerivedCategory.isGE_obj_of_isGE, which is Stacks 05TC part (1).

Neither the quasi-coherence of E, nor the source's hypotheses (2) and (3) on F, nor the integer N is used: N governs only the upper bound b + N - 1, which is the other half of assertion (3).

theorem isZero_homology_rightDerived_of_isZero_lt
    (E : DerivedCategory (Modules.{u, m} B S hS X hX))
    (hqc : ∀ q : ℤ, ((DerivedCategory.homologyFunctor
      (Modules.{u, m} B S hS X hX) q).obj E).IsQuasicoherentOnSite)
    (a : ℤ)
    (hE : ∀ j : ℤ, j < a → IsZero ((DerivedCategory.homologyFunctor
      (Modules.{u, m} B S hS X hX) j).obj E))
    (i : ℤ) (hi : i < a) :
    IsZero ((DerivedCategory.homologyFunctor AddCommGrpCat.{m} i).obj (RF.obj E))

AlgebraicGeometry.Space.isIso_homologyFunctor_map_rightDerived_truncLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentDerivedFunctorAmplitude.lean, line 165. The attribute's comment: “assertion (1), as the source proves it, by citing Derived Categories 05TC; the hypotheses (2), (3) on F and the integer N play no part in that assertion and are not binders”.

Stacks 08F7, assertion (1). Let S be a scheme, let X be an algebraic space over S, let F : Mod(𝒪_X) ⥤ Ab be an additive functor and let (RF, α) be a right derived functor of F on D(𝒪_X). Then for every object E of D_QCoh(𝒪_X) and every i ≤ a the canonical truncation map τ_{≤ a} E ⟶ E induces an isomorphism H ^ i (RF (τ_{≤ a} E)) ⟶ H ^ i (RF E).

The argument is the source's, which cites Derived Categories, Lemma [Stacks, Tag 05TC]. The functor RF is triangulated, so it carries the canonical truncation triangle τ_{≤ a} E ⟶ E ⟶ τ_{≥ a + 1} E to a distinguished triangle; its third vertex lies in degrees ≥ a + 1 by left t-exactness of RF, so H ^ i and H ^ (i - 1) vanish on it for i ≤ a, and the long exact homology sequence makes the first map invertible on H ^ i.

Neither the quasi-coherence of E, nor the source's hypotheses (2) and (3) on F, nor the integer N is used — none of them occurs in Tag 05TC either.

theorem isIso_homologyFunctor_map_rightDerived_truncLE
    (E : DerivedCategory (Modules.{u, m} B S hS X hX))
    (hqc : ∀ q : ℤ, ((DerivedCategory.homologyFunctor
      (Modules.{u, m} B S hS X hX) q).obj E).IsQuasicoherentOnSite)
    (a i : ℤ) (hi : i ≤ a) :
    IsIso ((DerivedCategory.homologyFunctor AddCommGrpCat.{m} i).map
      (RF.map ((DerivedCategory.TStructure.t.truncLEι a).app E)))

AlgebraicGeometry.Space.isZero_homology_rightDerived_of_isZero_gt_unbounded, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentDerivedFunctorAmplitudeUnbounded.lean, line 447. The attribute's comment: “assertion (3), the upper bound b + N - 1, and the sole registration of that half: H^i(RF E) = 0 for i > b + N - 1 once H^j(E) = 0 for j > b, for every E of D_QCoh with no boundedness hypothesis, so for a = -infinity too. Hypothesis (2) on F is the binder PreservesLimitsOfShape (Discrete N) F, hypothesis (3) is hRF, hypothesis (1) is unused”.

Stacks 08F7, assertion (3), the upper bound, for every E of D_QCoh(𝒪_X). Let S be a scheme, let X be an algebraic space over S, let F : Mod(𝒪_X) ⥤ Ab be an additive functor commuting with countable direct products and let (RF, α) be a right derived functor of F on D(𝒪_X). Let N ≥ 0 be an integer such that R^pF(ℱ) = 0 for every quasi-coherent ℱ and every p ≥ N, which is the source's hypothesis (3). Let E be an object of D_QCoh(𝒪_X) with H ^ j (E) = 0 for j > b. Then H ^ i (RF E) = 0 for i > b + N - 1.

Nothing is assumed about the lower endpoint a of the source's range -∞ ≤ a ≤ b ≤ ∞, so this is the case a = -∞ as well; the vanishing for i < a when a is finite is the other half of assertion (3) and is AlgebraicGeometry.Space.isZero_homology_rightDerived_of_isZero_lt. The source's hypothesis (2) on F is the binder [PreservesLimitsOfShape (Discrete ℕ) F]; it is used, unlike in the bounded statements, because the proof passes through the derived limit E = R lim τ_{≥ -n} E.

This is the sole registration of the upper bound of assertion (3); no form of that clause assuming in addition that E is bounded below is stated in the library, the bounded case being confined to the private ingredient AlgebraicGeometry.Space.isLE_rightDerived_obj_of_bounded.

theorem isZero_homology_rightDerived_of_isZero_gt_unbounded (N : ℕ)
    (hRF : ∀ M : Modules.{u, u} B S hS X hX, M.IsQuasicoherentOnSite →
      ∀ p : ℤ, (N : ℤ) ≤ p → IsZero ((F.rightDerivedPlus p).obj M))
    (E : DerivedCategory (Modules.{u, u} B S hS X hX))
    (hqc : ∀ q : ℤ, ((DerivedCategory.homologyFunctor
      (Modules.{u, u} B S hS X hX) q).obj E).IsQuasicoherentOnSite)
    (b : ℤ)
    (hEb : ∀ j : ℤ, b < j → IsZero ((DerivedCategory.homologyFunctor
      (Modules.{u, u} B S hS X hX) j).obj E))
    (i : ℤ) (hi : b + (N : ℤ) - 1 < i) :
    IsZero ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} i).obj (RF.obj E))

AlgebraicGeometry.Space.isIso_homologyFunctor_map_rightDerived_truncGE_unbounded, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentDerivedFunctorAmplitudeUnbounded.lean, line 485. The attribute's comment: “assertion (2), and the sole registration of it: H^i(RF E) -> H^i(RF(tau_{>= b - N + 1} E)) is an isomorphism for i >= b, for every E of D_QCoh with no boundedness hypothesis. Hypothesis (2) on F is the binder PreservesLimitsOfShape (Discrete N) F, hypothesis (3) is hRF, hypothesis (1) is unused”.

Stacks 08F7, assertion (2), for every E of D_QCoh(𝒪_X). Let S be a scheme, let X be an algebraic space over S, let F : Mod(𝒪_X) ⥤ Ab be an additive functor commuting with countable direct products and let (RF, α) be a right derived functor of F on D(𝒪_X). Let N ≥ 0 be an integer such that R^pF(ℱ) = 0 for every quasi-coherent ℱ and every p ≥ N, the source's hypothesis (3). Then for every object E of D_QCoh(𝒪_X) and every i ≥ b the canonical truncation map E ⟶ τ_{≥ b - N + 1} E induces an isomorphism H ^ i (RF E) ⟶ H ^ i (RF (τ_{≥ b - N + 1} E)).

No boundedness hypothesis on E is made. The canonical truncation triangle τ_{≤ b - N} E ⟶ E ⟶ τ_{≥ b - N + 1} E is carried by RF to a distinguished triangle, RF being triangulated; its first vertex lies in degrees ≤ b - 1 by AlgebraicGeometry.Space.isLE_rightDerived_obj_of_isLE, which needs no lower bound, so H ^ i and H ^ (i + 1) vanish on it for i ≥ b, and the long exact homology sequence makes the second map invertible on H ^ i.

This is the sole registration of assertion (2); no form of it assuming in addition that E is bounded below is stated in the library, the bounded case being confined to the private ingredient AlgebraicGeometry.Space.isLE_rightDerived_obj_of_bounded.

theorem isIso_homologyFunctor_map_rightDerived_truncGE_unbounded (N : ℕ)
    (hRF : ∀ M : Modules.{u, u} B S hS X hX, M.IsQuasicoherentOnSite →
      ∀ p : ℤ, (N : ℤ) ≤ p → IsZero ((F.rightDerivedPlus p).obj M))
    (E : DerivedCategory (Modules.{u, u} B S hS X hX))
    (hqc : ∀ q : ℤ, ((DerivedCategory.homologyFunctor
      (Modules.{u, u} B S hS X hX) q).obj E).IsQuasicoherentOnSite)
    (b i : ℤ) (hi : b ≤ i) :
    IsIso ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} i).map
      (RF.map ((DerivedCategory.TStructure.t.truncGEπ (b - (N : ℤ) + 1)).app E)))
Sources
LeanAlgebraicGeometry.Space.QuasicoherentDerivedCategory · AlgebraicGeometry.Space.quasicoherentDerivedComparisonSchemeUniverse · AlgebraicGeometry.Space.derivedQuasicoherent_tfae · AlgebraicGeometry.Space.hasCoproducts_quasicoherentDerivedCategory_ringUniverse · AlgebraicGeometry.Space.isDerivedLimit_single_limit_homology · AlgebraicGeometry.Space.isZero_cohomology_limit_homology_of_isAffineChart · AlgebraicGeometry.Space.isLimit_cohomology_of_isDerivedLimit_of_epi · AlgebraicGeometry.Space.isDerivedLimit_single_limit_homology_unconditional

Section75.6 Total direct image#

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

Tag 08FA, a lemma

Tag 08FA in the Stacks Project.

AlgebraicGeometry.Space.exists_isZero_homology_derivedModulePushforward_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentDerivedPushforwardBound.lean, line 487. The attribute's comment: “part (3)”.

Stacks 08FA, part (3). Let f : X ⟶ Y be a quasi-compact and quasi-separated morphism of algebraic spaces over S, with Y quasi-compact. There is an integer N such that for every morphism of algebraic spaces Y' ⟶ Y, with base change f' : X' ⟶ Y' of f, and every E in D_QCoh(𝒪_{X'}) with H^m(E) = 0 for m > 0, we have H^m(Rf'_*E) = 0 for m ≥ N.

theorem exists_isZero_homology_derivedModulePushforward_baseChange {X Y : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (hfqc : IsQuasiCompact B S hS f.hom) (hfqs : IsQuasiSeparated B S hS f.hom)
    (hY : IsQuasiCompactSpace B S hS Y.1) :
    ∃ N : ℤ, ∀ (Y' X' : AlgebraicSpaces B S hS) (g : Y' ⟶ Y) (g' : X' ⟶ X) (f' : X' ⟶ Y'),
      IsPullback g' f' f g →
      ∀ E : DerivedCategory (Modules.{u, u} B S hS X'.1 X'.2), QcohDerived B S hS X' E →
        (∀ m : ℤ, 0 < m → IsZero ((DerivedCategory.homologyFunctor _ m).obj E)) →
        ∀ m : ℤ, N ≤ m → IsZero ((DerivedCategory.homologyFunctor _ m).obj
          ((derivedModulePushforward B S hS f').obj E))

AlgebraicGeometry.Space.exists_isZero_homology_derivedModulePushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentDerivedPushforwardBound.lean, line 516. The attribute's comment: “part (2)”.

Stacks 08FA, part (2). Let f : X ⟶ Y be a quasi-compact and quasi-separated morphism of algebraic spaces over S, with Y quasi-compact. There is an integer N such that for every E in D_QCoh(𝒪_X) with H^m(E) = 0 for m > 0, we have H^m(Rf_*E) = 0 for m ≥ N.

theorem exists_isZero_homology_derivedModulePushforward {X Y : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (hfqc : IsQuasiCompact B S hS f.hom) (hfqs : IsQuasiSeparated B S hS f.hom)
    (hY : IsQuasiCompactSpace B S hS Y.1) :
    ∃ N : ℤ, ∀ E : DerivedCategory (Modules.{u, u} B S hS X.1 X.2), QcohDerived B S hS X E →
      (∀ m : ℤ, 0 < m → IsZero ((DerivedCategory.homologyFunctor _ m).obj E)) →
      ∀ m : ℤ, N ≤ m → IsZero ((DerivedCategory.homologyFunctor _ m).obj
        ((derivedModulePushforward B S hS f).obj E))

Declarations registered for the tag:

Tag 08FB, a lemma

Tag 08FB in the Stacks Project.

Declarations registered for the tag:

Tag 08GH, a remark

Tag 08GH in the Stacks Project.

AlgebraicGeometry.Space.nonempty_representedQuasicoherentDerivedPullbackIso_and_pushforwardIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RepresentedQuasicoherentDerivedSquare.lean, line 633.

Stacks 08GH. Let g : T' ⟶ T be a morphism of the big fppf site over S, so that f = h_g : X' ⟶ X is a morphism of representable algebraic spaces represented by the morphism of schemes g_0 : X'_0 ⟶ X_0. Under the equivalences D_QCoh(𝒪_{X_0}) ≌ D_QCoh(𝒪_X) of Stacks 071Q,

  1. Lg_0^* : D_QCoh(𝒪_{X_0}) ⥤ D_QCoh(𝒪_{X'_0}) corresponds to Lf^* : D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_{X'}), and
  2. if f is quasi-compact and quasi-separated, Rg_{0,*} : D_QCoh(𝒪_{X'_0}) ⥤ D_QCoh(𝒪_{X_0}) corresponds to Rf_* : D_QCoh(𝒪_{X'}) ⥤ D_QCoh(𝒪_X).
theorem nonempty_representedQuasicoherentDerivedPullbackIso_and_pushforwardIso :
    Nonempty (Stacks.Duality.quasiCoherentDerivedPullback' (B.inclusion.map g.left) ⋙
        (representedDualityQuasicoherentDerivedEquivalence B S hS T').functor ≅
      (representedDualityQuasicoherentDerivedEquivalence B S hS T).functor ⋙
        quasicoherentDerivedModulePullback (representedSpaceMap B S hS g)) ∧
    ∀ (hfqc : IsQuasiCompact B S hS (representedSpaceMap B S hS g).hom)
      (hfqs : IsQuasiSeparated B S hS (representedSpaceMap B S hS g).hom),
      Nonempty (Stacks.Duality.quasiCoherentDerivedPushforward (B.inclusion.map g.left)
          (isQuasicoherent_homology_derivedPushforward_representedSchemeMap g hfqc hfqs) ⋙
          (representedDualityQuasicoherentDerivedEquivalence B S hS T).functor ≅
        (representedDualityQuasicoherentDerivedEquivalence B S hS T').functor ⋙
          quasicoherentDerivedPushforward B S hS (representedSpaceMap B S hS g) hfqc hfqs)
Tag 08II, a lemma

Tag 08II in the Stacks Project.

AlgebraicGeometry.Space.reflectsIsomorphisms_affineQuasicoherentDerivedPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineDerivedPushforwardReflectsIsomorphisms.lean, line 327.

[Stacks, Tag 08II]. Let S be a scheme and let f : X ⟶ Y be an affine morphism of algebraic spaces over S. Then Rf_* : D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_Y) reflects isomorphisms.

Here Rf_* is any total right derived functor of the direct image of 𝒪_X-modules, with its derivation unit α, restricted to D_QCoh as AlgebraicGeometry.Space.affineQuasicoherentDerivedPushforward. The proof is AlgebraicGeometry.Space.isIso_of_isIso_derivedModulePushforward_map_of_isAffineHom: the cone C of a morphism E ⟶ F of D_QCoh(𝒪_X) lies in D_QCoh(𝒪_X), Rf_*C = 0 when Rf_* of the morphism is invertible, and H^i(Rf_*C) = f_*H^i(C) with f_* conservative on quasi-coherent modules forces C = 0.

theorem reflectsIsomorphisms_affineQuasicoherentDerivedPushforward :
    (affineQuasicoherentDerivedPushforward B S hS f hf Rf α).ReflectsIsomorphisms
Tag 08IJ, a lemma

Tag 08IJ in the Stacks Project.

AlgebraicGeometry.Space.isIso_affinePullPushMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineDerivedPullPush.lean, line 200.

Stacks 08IJ. Let f : X ⟶ Y be an affine morphism of algebraic spaces over S. For E in D_QCoh(𝒪_Y) the canonical map E ⊗^L f_*𝒪_X ⟶ Rf_*Lf^*E is an isomorphism, so Rf_*Lf^*E = E ⊗^L_{𝒪_Y} f_*𝒪_X.

theorem isIso_affinePullPushMap (f : X ⟶ Y) (hf : IsAffineHom B S hS f.hom)
    (E : DerivedCategory (SheafOfModules.{u} (ringedToposStructureRingSheaf B S hS Y)))
    (hE : QcohDerived B S hS Y E) :
    IsIso (affinePullPushMap f hf E)
Sources
LeanAlgebraicGeometry.Space.exists_isZero_homology_derivedModulePushforward_baseChange · AlgebraicGeometry.Space.exists_isZero_homology_derivedModulePushforward · AlgebraicGeometry.Space.qcohDerived_derivedModulePushforward_obj · AlgebraicGeometry.Space.preservesCoproducts_quasicoherentDerivedPushforward · AlgebraicGeometry.Space.nonempty_representedQuasicoherentDerivedPullbackIso_and_pushforwardIso · AlgebraicGeometry.Space.reflectsIsomorphisms_affineQuasicoherentDerivedPushforward · AlgebraicGeometry.Space.isIso_affinePullPushMap

Section75.7 Being proper over a base#

Section 75.7 of the Stacks Project, Tag 0CZB. 11 tags here are carried by 23 declarations of the repository (all in StacksFrontier) and 14 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0CZB, the section

Tag 0CZB in the Stacks Project.

AlgebraicGeometry.Space.not_tfae_isProper_closedSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/ProperOverBase.lean, line 189. The attribute's comment: “the remark after Definition 0CZD: Lemma 0CZC is false if f is not locally of finite type”.

Lemma 0CZC fails without local finite type (the remark after Definition 0CZD, Section 0CZB). Over every big fppf site there are a scheme S, a morphism f : X ⟶ Y of algebraic spaces over S which is not locally of finite type, and a closed subset T ⊆ |X| for which the three conditions of Lemma 0CZC are not equivalent: (1) the reduced induced closed subspace on T is proper over Y, (2) some closed subspace with points T is, (3) every one is.

theorem not_tfae_isProper_closedSubspace (B : BigFppfSite.{u}) :
    ∃ (S : Scheme.{u}) (hS : B.Contains S) (X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
      (hX : IsAlgebraicSpace B S hS X) (_hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
      (T : Set (points B S hS X)) (hT : IsClosed T),
      ¬ IsLocallyOfFiniteType B S hS f ∧
      ¬ [IsProper B S hS ((reducedClosedSubspace B S hS X hX T hT).ι ≫ f),
          ∃ (Z : Subfunctor X) (_ : IsClosedSubspace B S hS Z),
            Set.range (pointsMap B S hS Z.toFunctor Z.ι) = T ∧ IsProper B S hS (Z.ι ≫ f),
          ∀ (Z : Subfunctor X) (_ : IsClosedSubspace B S hS Z),
            Set.range (pointsMap B S hS Z.toFunctor Z.ι) = T →
              IsProper B S hS (Z.ι ≫ f)].TFAE

Declarations registered for the tag:

Tag 0CZC, a lemma

Tag 0CZC in the Stacks Project.

AlgebraicGeometry.Space.isProper_reducedClosedSubspace_iff_exists, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Properness/ProperClosedSubset.lean, line 414. The attribute's comment: “conditions (1) and (2)”. References: EGA II (5.4.10), “indep. of subscheme”.

Stacks 0CZC, conditions (1) and (2). For a morphism of algebraic spaces over S locally of finite type and a closed set T of points of the source, the reduced induced closed subspace on T is proper over the target exactly when some closed subspace with set of points T is proper over the target.

The forward implication must exhibit a closed subspace with set of points T, which is the existence clause of Stacks 03IQ. That clause is now available unconditionally: the reduced induced subspace is a closed subspace by AlgebraicGeometry.Space.isClosedSubspace_reducedClosedSubspace_of_closedImmersionDescent applied to AlgebraicGeometry.Space.isEffectiveDescentAlongSurjectiveEtale_isClosedImmersion, which is Stacks 02W8 at the closed immersions.

theorem isProper_reducedClosedSubspace_iff_exists (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsLocallyOfFiniteType B S hS f)
    (T : Set (points B S hS X)) (hT : IsClosed T) :
    IsProperOver B S hS hX hY f hf T hT ↔
      ∃ (Z : Subfunctor X) (_ : IsClosedSubspace B S hS Z),
        Set.range (pointsMap B S hS Z.toFunctor Z.ι) = T ∧ IsProper B S hS (Z.ι ≫ f)

AlgebraicGeometry.Space.exists_isProper_closedSubspace_iff_forall, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Properness/ProperClosedSubset.lean, line 439. The attribute's comment: “conditions (2) and (3)”. References: EGA II (5.4.10), “indep. of subscheme”.

Stacks 0CZC, conditions (2) and (3). If one closed subspace with a given closed set of points is proper over the target, then every closed subspace with that set of points is.

The implication from (3) to (2) must exhibit a closed subspace with set of points T, which is the existence clause of Stacks 03IQ. That clause is now available unconditionally: the reduced induced subspace is a closed subspace by AlgebraicGeometry.Space.isClosedSubspace_reducedClosedSubspace_of_closedImmersionDescent applied to AlgebraicGeometry.Space.isEffectiveDescentAlongSurjectiveEtale_isClosedImmersion, which is Stacks 02W8 at the closed immersions.

theorem exists_isProper_closedSubspace_iff_forall (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsLocallyOfFiniteType B S hS f)
    (T : Set (points B S hS X)) (hT : IsClosed T) :
    (∃ (Z : Subfunctor X) (_ : IsClosedSubspace B S hS Z),
        Set.range (pointsMap B S hS Z.toFunctor Z.ι) = T ∧ IsProper B S hS (Z.ι ≫ f)) ↔
      ∀ (Z : Subfunctor X) (_ : IsClosedSubspace B S hS Z),
        Set.range (pointsMap B S hS Z.toFunctor Z.ι) = T → IsProper B S hS (Z.ι ≫ f)
Tag 0CZD, a definition

Tag 0CZD in the Stacks Project.

AlgebraicGeometry.Space.IsProperOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/ProperClosedSubset.lean, line 60.

Stacks 0CZD. A closed subset of the points of an algebraic space X is proper over Y when the reduced induced closed subspace of X supported on it is proper over Y.

abbrev IsProperOver (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (_hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (_hf : IsLocallyOfFiniteType B S hS f) (T : Set (points B S hS X))
    (hT : IsClosed T) : Prop
Tag 0CZE, a lemma

Tag 0CZE in the Stacks Project.

AlgebraicGeometry.Space.isProperOver_of_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperClosedSubset.lean, line 169.

Stacks 0CZE. A closed subset of a closed subset proper over the base is proper over the base.

The reduced closed subspace on the smaller set is a subfunctor of the one on the larger set, so the inclusion between them is a closed immersion and hence proper; composing with properness over Y of the larger one gives the result.

theorem isProperOver_of_subset (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsLocallyOfFiniteType B S hS f)
    (T' T : Set (points B S hS X)) (hT' : _root_.IsClosed T') (hT : _root_.IsClosed T)
    (hsub : T' ⊆ T) (hproper : IsProperOver B S hS hX hY f hf T hT) :
    IsProperOver B S hS hX hY f hf T' hT'
Tag 0CZF, a lemma

Tag 0CZF in the Stacks Project.

AlgebraicGeometry.Space.isProperOver_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Properness/ProperClosedSubsetBaseChange.lean, line 135. The attribute's comment: “properness”.

Stacks 0CZF, properness. In a cartesian square of algebraic spaces over S whose right vertical morphism is locally of finite type, the inverse image of a closed subset proper over the base is proper over the new base.

theorem isProperOver_preimage {X' X Y' Y : AlgebraicSpaces B S hS}
    {g' : X' ⟶ X} {f' : X' ⟶ Y'} {f : X ⟶ Y} {g : Y' ⟶ Y}
    (sq : IsPullback g' f' f g) (hf : IsLocallyOfFiniteType B S hS f.hom)
    (T : Set (points B S hS X.1)) (hT : IsClosed T)
    (hproper : IsProperOver B S hS X.property Y.property f.hom hf T hT) :
    IsProperOver B S hS X'.property Y'.property f'.hom
      ((isLocallyOfFiniteType_isStableUnderBaseChange B S hS).of_isPullback sq hf)
      (pointsMap B S hS X'.1 g'.hom ⁻¹' T)
      (isClosed_preimage_pointsMap B S hS X'.property X.property g'.hom hT)

Declarations registered for the tag:

Tag 0CZG, a lemma

Tag 0CZG in the Stacks Project.

AlgebraicGeometry.Space.isClosed_image_of_universallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Properness/ProperClosedSubsetImage.lean, line 187. The attribute's comment: “image_universally_closed”.

Stacks 0CZG, closedness of the image under a universally closed morphism. A universally closed morphism of algebraic spaces over S carries closed subsets of its space of points to closed subsets: it is closed, by Stacks 03HI.

theorem isClosed_image_of_universallyClosed (_hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : UniversallyClosed B S hS f)
    (T : Set (points B S hS X)) (hT : IsClosed T) :
    IsClosed (pointsMap B S hS X f '' T)

AlgebraicGeometry.Space.isProperOver_image_of_universallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Properness/ProperClosedSubsetImage.lean, line 200. The attribute's comment: “image_universally_closed”.

Stacks 0CZG, properness of the image under a universally closed morphism. The image of a closed subset proper over the base under a universally closed morphism is proper over the base.

The restriction of a universally closed morphism to the reduced induced subspace is universally closed, the inclusion of that subspace being universally closed, so AlgebraicGeometry.Space.isProper_ι_comp_of_universallyClosed_ι_comp applies.

theorem isProperOver_image_of_universallyClosed (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (hA : IsAlgebraicSpace B S hS A)
    (f : X ⟶ Y) (g : Y ⟶ A) (hf : UniversallyClosed B S hS f)
    (hXft : IsLocallyOfFiniteType B S hS (f ≫ g))
    (hYft : IsLocallyOfFiniteType B S hS g)
    (T : Set (points B S hS X)) (hT : IsClosed T)
    (hTproper : IsProperOver B S hS hX hA (f ≫ g) hXft T hT) :
    IsProperOver B S hS hY hA g hYft (pointsMap B S hS X f '' T)
      (isClosed_image_of_universallyClosed B S hS hX hY f hf T hT)

AlgebraicGeometry.Space.isClosed_image_of_isProperOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Properness/ProperClosedSubsetImage.lean, line 236. The attribute's comment: “image_separated”.

Stacks 0CZG, closedness of the image in a separated target. If the structure morphism of Y is separated and the closed subset T of the points of X is proper over the base, then the image of T in the points of Y is closed.

The reduced induced subspace on T is universally closed over the base, so its morphism to Y is universally closed by Stacks 04NX, the structure morphism of Y being separated.

theorem isClosed_image_of_isProperOver (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (hA : IsAlgebraicSpace B S hS A)
    (f : X ⟶ Y) (pX : X ⟶ A) (pY : Y ⟶ A) (hcomm : f ≫ pY = pX)
    (hpX : IsLocallyOfFiniteType B S hS pX) (_hpY : IsLocallyOfFiniteType B S hS pY)
    (hsep : IsSeparated B S hS pY)
    (T : Set (points B S hS X)) (hT : IsClosed T)
    (hproper : IsProperOver B S hS hX hA pX hpX T hT) :
    IsClosed (pointsMap B S hS X f '' T)

AlgebraicGeometry.Space.isProperOver_image_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Properness/ProperClosedSubsetImage.lean, line 256. The attribute's comment: “image_separated”.

Stacks 0CZG, properness of the image in a separated target. The image in Y of a closed subset of X proper over the base is proper over the base when the structure morphism of Y is separated.

As for closedness, the reduced induced subspace on T is universally closed over Y by Stacks 04NX, so AlgebraicGeometry.Space.isProper_ι_comp_of_universallyClosed_ι_comp applies. The closedness of the image is an explicit hypothesis, as AlgebraicGeometry.Space.IsProperOver is a predicate on closed subsets.

theorem isProperOver_image_of_isSeparated (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (hA : IsAlgebraicSpace B S hS A)
    (f : X ⟶ Y) (pX : X ⟶ A) (pY : Y ⟶ A) (hcomm : f ≫ pY = pX)
    (hpX : IsLocallyOfFiniteType B S hS pX) (hpY : IsLocallyOfFiniteType B S hS pY)
    (hsep : IsSeparated B S hS pY)
    (T : Set (points B S hS X)) (hT : IsClosed T)
    (hproper : IsProperOver B S hS hX hA pX hpX T hT)
    (hImage : IsClosed (pointsMap B S hS X f '' T)) :
    IsProperOver B S hS hY hA pY hpY (pointsMap B S hS X f '' T) hImage

AlgebraicGeometry.Space.isProperOver_preimage_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Properness/ProperClosedSubsetImage.lean, line 280. The attribute's comment: “inverse_image_proper”.

Stacks 0CZG, properness of the inverse image. The inverse image of a closed subset proper over the base under a proper morphism is proper over the base.

theorem isProperOver_preimage_of_isProper (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (hA : IsAlgebraicSpace B S hS A)
    (f : X ⟶ Y) (g : Y ⟶ A) (hf : IsProper B S hS f)
    (hXft : IsLocallyOfFiniteType B S hS (f ≫ g))
    (hYft : IsLocallyOfFiniteType B S hS g)
    (T : Set (points B S hS Y)) (hT : IsClosed T)
    (hTproper : IsProperOver B S hS hY hA g hYft T hT) :
    IsProperOver B S hS hX hA (f ≫ g) hXft (pointsMap B S hS X f ⁻¹' T)
      (isClosed_preimage_pointsMap B S hS hX hY f hT)

Declarations registered for the tag:

Tag 0CZH, a lemma

Tag 0CZH in the Stacks Project.

AlgebraicGeometry.Space.isProperOver_iUnion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Properness/ProperClosedSubsetUnion.lean, line 228.

Stacks 0CZH. A finite union of closed subsets of the points of X, each proper over Y, is proper over Y.

theorem isProperOver_iUnion {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) (hf : IsLocallyOfFiniteType B S hS f)
    {ι : Type v} [Finite ι] (T : ι → Set (points B S hS X))
    (hT : ∀ i, IsClosed (T i))
    (hproper : ∀ i, IsProperOver B S hS hX hY f hf (T i) (hT i)) :
    IsProperOver B S hS hX hY f hf (⋃ i, T i) (isClosed_iUnion_of_finite hT)
Tag 0CZI, a lemma

Tag 0CZI in the Stacks Project.

AlgebraicGeometry.Space.hasProperSupport_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/ProperModuleSupport.lean, line 223.

Stacks 0CZI. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is locally of finite type and let F be a finite type quasi-coherent 𝒪_X-module. The following are equivalent:

  1. the support of F is proper over Y;
  2. the scheme-theoretic support of F, Stacks 07U1, is proper over Y;
  3. there are a closed subspace Z ⊆ X and a finite type quasi-coherent 𝒪_Z-module G with Z → Y proper and (Z → X)_* G = F.

The support of F is closed by Stacks 07TZ, so Definition 0CZD applies to it; the scheme-theoretic support is a closed subspace whose set of points is that support by Stacks 07U0 part (4), so (1) and (2) agree by Stacks 0CZC, which says that properness over the base of a closed subspace depends only on its set of points. (2) implies (3) by the existence clause of Stacks 07U0, together with part (3) of the same lemma for finite type of the module. (3) implies (1) because the support of F is contained in the set of points of Z, which is proper over Y by Stacks 0CZC, so Stacks 0CZE applies.

theorem hasProperSupport_tfae (F : Modules.{u, u} B S hS X.1 X.2)
    (hF : F.IsQuasicoherentOnSite) (hFft : SheafOfModules.IsFiniteTypeOnSite F)
    (hft : PresheafOfModules.IsFiniteType (smallEtaleRingedSite B S hS X.1 X.2).J F.val) :
    List.TFAE
      [HasProperSupport B S hS X.2 Y.2 f hf ((SheafOfModules.toSheaf _).obj F),
        IsProper B S hS ((schemeTheoreticSupport B S hS X F).ι ≫ f),
        ∃ (Z : ClosedSubspaces B S hS X.1)
          (G : Modules.{u, u} B S hS (closedSubspaceToSpace B S hS X Z).1
            (closedSubspaceToSpace B S hS X Z).2),
          G.IsQuasicoherentOnSite ∧ SheafOfModules.IsFiniteTypeOnSite G ∧
            IsProper B S hS (Z.1.ι ≫ f) ∧
            Nonempty ((modulePushforward B S hS
              (closedSubspaceInclusion B S hS X Z)).obj G ≅ F)]
Tag 0CZJ, a lemma

Tag 0CZJ in the Stacks Project.

AlgebraicGeometry.Space.isProperOver_supportOfSheaf_modulePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Properness/ModuleSupportProperBaseChange.lean, line 60.

In a cartesian square of algebraic spaces over S whose right vertical morphism f is locally of finite type, the support of the pullback along the upper horizontal morphism of a finite type, quasi-coherent 𝒪_X-module whose support is proper over Y is proper over Y'. It takes the quasi-coherence of F (_hqc), its finite type (hft) and the properness of its support over Y (hproper) as hypotheses.

theorem isProperOver_supportOfSheaf_modulePullback {X' X Y' Y : AlgebraicSpaces B S hS}
    {g' : X' ⟶ X} {f' : X' ⟶ Y'} {f : X ⟶ Y} {g : Y' ⟶ Y}
    (sq : IsPullback g' f' f g) (hf : IsLocallyOfFiniteType B S hS f.hom)
    (F : Modules.{u, u} B S hS X.1 X.2)
    (_hqc : SheafOfModules.IsQuasicoherentOnSite F)
    (hft : SheafOfModules.IsFiniteTypeOnSite F)
    (hproper : IsProperOver B S hS X.property Y.property f.hom hf
      (supportOfSheaf B S hS X.1 ((SheafOfModules.toSheaf _).obj F))
      (letI := hft; isClosed_supportOfSheaf_of_isFiniteTypeOnSite B S hS X.1 X.property F)) :
    IsProperOver B S hS X'.property Y'.property f'.hom
      ((isLocallyOfFiniteType_isStableUnderBaseChange B S hS).of_isPullback sq hf)
      (supportOfSheaf B S hS X'.1
        ((SheafOfModules.toSheaf _).obj ((modulePullback B S hS g').obj F)))
      (isClosed_supportOfSheaf_modulePullback B S hS g' F hft)
Tag 0CZK, a lemma

Tag 0CZK in the Stacks Project.

AlgebraicGeometry.Space.hasProperSupport_of_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentAdicSystemProperSupport.lean, line 108. The attribute's comment: “part (1), quotients”.

Stacks 0CZK, part (1), the quotient clause. A quotient of an 𝒪_X-module of finite type whose support is proper over Y again has support proper over Y.

The quotient is of finite type by Stacks 03DL(5), so its support is closed by Stacks 07TZ; an epimorphism of sheaves of modules is a local surjection, so that support is contained in the support of the source by Stacks 04KB(5); and a closed subset of a closed subset proper over the base is proper over the base by Stacks 0CZE.

theorem hasProperSupport_of_epi (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsLocallyOfFiniteType B S hS f)
    {M N : Modules.{u, u} B S hS X hX} (p : M ⟶ N) [Epi p]
    (hMft : SheafOfModules.IsFiniteTypeOnSite M)
    (hM : HasProperSupport B S hS hX hY f hf ((SheafOfModules.toSheaf _).obj M)) :
    HasProperSupport B S hS hX hY f hf ((SheafOfModules.toSheaf _).obj N)

AlgebraicGeometry.Space.hasProperSupport_toSheaf_of_sectionwiseSplit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Properness/ProperSupport.lean, line 225. The attribute's comment: “part (1), direct sums”.

Stacks 0CZK, part (1), the direct sum clause. A direct sum of two 𝒪_X-modules whose supports are proper over Y again has support proper over Y.

The support of a module is the support of its underlying abelian sheaf, and the two inclusions, the two projections and the three identities they satisfy on sections carry over to the underlying abelian sheaves unchanged, so this is AlgebraicGeometry.Space.hasProperSupport_of_sectionwiseSplit read off the sections of the modules.

theorem hasProperSupport_toSheaf_of_sectionwiseSplit (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsLocallyOfFiniteType B S hS f)
    {P M N : Modules.{u, v} B S hS X hX}
    (i₁ : M ⟶ P) (i₂ : N ⟶ P) (p₁ : P ⟶ M) (p₂ : P ⟶ N)
    (hi₁ : ∀ (U : SmallEtale B S hS X) (σ : M.val.obj (op U)),
      p₁.val.app (op U) (i₁.val.app (op U) σ) = σ)
    (hi₂ : ∀ (U : SmallEtale B S hS X) (σ : N.val.obj (op U)),
      p₂.val.app (op U) (i₂.val.app (op U) σ) = σ)
    (htotal : ∀ (U : SmallEtale B S hS X) (τ : P.val.obj (op U)),
      i₁.val.app (op U) (p₁.val.app (op U) τ) +
        i₂.val.app (op U) (p₂.val.app (op U) τ) = τ)
    (hM : HasProperSupport B S hS hX hY f hf ((SheafOfModules.toSheaf _).obj M))
    (hN : HasProperSupport B S hS hX hY f hf ((SheafOfModules.toSheaf _).obj N)) :
    HasProperSupport B S hS hX hY f hf ((SheafOfModules.toSheaf _).obj P)

AlgebraicGeometry.Space.hasProperSupport_X₂_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Properness/ProperSupportSerre.lean, line 163. The attribute's comment: “part (1), extensions”.

Stacks 0CZK, part (1), the extension clause. An extension of 𝒪_X-modules whose supports are proper over Y again has support proper over Y: the middle term of a short exact sequence of 𝒪_X-modules whose outer terms have support proper over Y has support proper over Y.

The support of the middle term is exactly the union of the supports of the outer two. It is contained in that union by AlgebraicGeometry.Space.supportOfSheaf_middle_subset_union; it contains the support of the first term because the first map is a monomorphism and the support of the third because the second map is an epimorphism, hence a local surjection, which are the two halves of Stacks 04KB. So the support is closed, being a union of two closed supports, and a finite union of closed subsets proper over Y is proper over Y by Stacks 0CZH.

No finiteness hypothesis appears: as for a direct sum, the containment of supports is an equality, so closedness of the support of the extension comes from the two given supports and not from the finite type closure of Stacks 05VR.

theorem hasProperSupport_X₂_of_shortExact (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsLocallyOfFiniteType B S hS f)
    {T : ShortComplex (Modules.{u, u} B S hS X hX)} (hT : T.ShortExact)
    (h₁ : HasProperSupport B S hS hX hY f hf ((SheafOfModules.toSheaf _).obj T.X₁))
    (h₃ : HasProperSupport B S hS hX hY f hf ((SheafOfModules.toSheaf _).obj T.X₃)) :
    HasProperSupport B S hS hX hY f hf ((SheafOfModules.toSheaf _).obj T.X₂)

AlgebraicGeometry.Space.hasProperSupport_cokernel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Properness/ProperSupportSerre.lean, line 201. The attribute's comment: “part (1), cokernels”.

Stacks 0CZK, part (1), the cokernel clause. The cokernel of a map u : M ⟶ N of 𝒪_X-modules whose target is of finite type and has support proper over Y again has support proper over Y.

The cokernel is a quotient of N, so this is the quotient clause AlgebraicGeometry.Space.hasProperSupport_of_epi. Stacks 0CZK assumes proper support of both M and N; the source of u plays no part.

theorem hasProperSupport_cokernel (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsLocallyOfFiniteType B S hS f)
    {M N : Modules.{u, u} B S hS X hX} (u : M ⟶ N)
    (hNft : SheafOfModules.IsFiniteTypeOnSite N)
    (hN : HasProperSupport B S hS hX hY f hf ((SheafOfModules.toSheaf _).obj N)) :
    HasProperSupport B S hS hX hY f hf ((SheafOfModules.toSheaf _).obj
      (cokernel (C := Modules.{u, u} B S hS X hX) u))

AlgebraicGeometry.Space.hasProperSupport_abelianImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Properness/ProperSupportSerre.lean, line 222. The attribute's comment: “part (1), images”.

Stacks 0CZK, part (1), the image clause. The image of a map u : M ⟶ N of 𝒪_X-modules whose source is of finite type and has support proper over Y again has support proper over Y.

CategoryTheory.Abelian.coimage u is by definition cokernel (kernel.ι u), hence a quotient of M, so it has support proper over Y by the quotient clause AlgebraicGeometry.Space.hasProperSupport_of_epi; and CategoryTheory.Abelian.coimageIsoImage identifies it with the image, whose support is therefore the same by Stacks 04KB. Stacks 0CZK assumes proper support of both M and N; the target of u plays no part.

theorem hasProperSupport_abelianImage (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsLocallyOfFiniteType B S hS f)
    {M N : Modules.{u, u} B S hS X hX} (u : M ⟶ N)
    (hMft : SheafOfModules.IsFiniteTypeOnSite M)
    (hM : HasProperSupport B S hS hX hY f hf ((SheafOfModules.toSheaf _).obj M)) :
    HasProperSupport B S hS hX hY f hf ((SheafOfModules.toSheaf _).obj
      (Abelian.image (C := Modules.{u, u} B S hS X hX) u))

AlgebraicGeometry.Space.isSerreClass_isCoherentProperOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Properness/ProperSupportSerre.lean, line 259. The attribute's comment: “part (2), the Serre subcategory; the locally Noetherian hypothesis on Y is absent because the abelian structure on Coh(O_X) is Stacks 07UC in the hypothesis-free form AlgebraicGeometry.Space.coherentModules_abelian_of_closure”.

Stacks 0CZK, part (2). The coherent 𝒪_X-modules whose support is proper over Y form a Serre subcategory of the abelian category Coh(𝒪_X) of coherent 𝒪_X-modules.

The property is AlgebraicGeometry.Space.isCoherentProperOver, the one cutting out the source of equation 76.42.5.1, and the abelian structure on Coh(𝒪_X) is Stacks 07UC in the form AlgebraicGeometry.Space.coherentModules_abelian_of_closure, which needs no locally Noetherian hypothesis in this tree; the hypothesis of the source is therefore absent.

By Stacks 02MP it is enough to exhibit one object with the property and to show that the middle term of an exact sequence whose outer terms have the property has it. The zero module has empty support. For the exactness condition: the kernel K of T.X₂ ⟶ T.X₃, formed in the ambient category of all 𝒪_X-modules, is a quotient of T.X₁ because the sequence is exact, so it has support proper over Y by the quotient clause of part (1); the support of T.X₂ is contained in the union of the support of K and the support of T.X₃, by AlgebraicGeometry.Space.supportOfSheaf_subset_union_kernel; and the support of T.X₂ is closed because a coherent module is of finite type, by Stacks 07TZ. Stacks 0CZH and 0CZE then finish, in the form AlgebraicGeometry.Space.hasProperSupport_of_subset_union.

theorem isSerreClass_isCoherentProperOver (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsLocallyOfFiniteType B S hS f) :
    letI : Abelian (CoherentModules.{u, u} B S hS X hX) :=
      coherentModules_abelian_of_closure B S hS X hX
    (isCoherentProperOver B S hS hX hY f hf).IsSerreClass
Tag 08GC, a lemma

Tag 08GC in the Stacks Project.

AlgebraicGeometry.Space.isCoherent_rightDerived_modulePushforward_of_hasProperSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/ProperSupportCoherentPushforward.lean, line 206. The attribute's comment: “granted three named hypotheses, none of them this conclusion. (1) h08AR, Stacks 08AR itself — coherence of the higher direct images of a coherent module along a proper morphism to Y — which has no presence in this library, nor has its scheme-level counterpart Stacks 02O5, the dévissage for coherent modules, Chow's lemma and the vanishing for relatively ample invertible sheaves that would prove it all being absent; it is carried in its own shape, with the module coherent and the conclusion coherent. (2) h0734, the degeneration of the relative Leray spectral sequence of Stacks 0734 that the source's last step is, namely R^p f_(i_ G) = R^p (f ∘ i)_* G when the higher direct images along i vanish; the formalized Stacks 0734 is stated for ringed topoi with all three universes equal and the small étale ringed topos of an algebraic space is RingedTopos u (u+1) u, so it does not apply, and the vanishing that h0734 asks for is discharged here from Stacks 07UH. (3) h03DW, the étale-affine case of Stacks 03DW, which is the hypothesis of the vanishing half of the formalized Stacks 07UH and is quoted in the form that lemma takes it. Stacks 0CZI, Stacks 07UH, Stacks 081Y, Stacks 04ZK and the coherence step of Stacks 07UG are applied and not assumed, so the source's hypotheses are all consumed: proper support is the input of Stacks 0CZI, and f locally of finite type together with Y locally Noetherian give local Noetherianity of X by Stacks 04ZK, which is what makes the module of Stacks 0CZI coherent”.

Stacks 08GC. Let S be a scheme, let f : X ⟶ Y be a morphism of algebraic spaces over S which is locally of finite type with Y locally Noetherian, and let 𝓕 be a coherent 𝒪_X-module whose support is proper over Y. Then R^p f_*𝓕 is a coherent 𝒪_Y-module for every p.

The proof is the source's. Properness of the support feeds Stacks 0CZI, AlgebraicGeometry.Space.hasProperSupport_tfae, whose third condition produces a closed subspace Z ⊆ X proper over Y and a quasi-coherent 𝒪_Z-module 𝓖 of finite type with i_*𝓖 ≅ 𝓕, where i : Z → X is the inclusion; 𝓖 is coherent because X is locally Noetherian by Stacks 04ZK, which is where hf and hY are used, so that the step of Stacks 07UG applies. A closed immersion is finite by Stacks 081Y, so the higher direct images along i vanish by the vanishing half of Stacks 07UH; h0734 then identifies R^p f_*(i_*𝓖) with R^p (i ≫ f)_*𝓖, which h08AR makes coherent, and coherence transports along the two isomorphisms because it is invariant under isomorphism of modules.

The three carried inputs are h03DW, the input of the vanishing half of Stacks 07UH; h08AR, Stacks 08AR; and h0734, the degeneration of the relative Leray spectral sequence. See the module documentation for each.

theorem isCoherent_rightDerived_modulePushforward_of_hasProperSupport
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hf : IsLocallyOfFiniteType B S hS f.hom)
    (hY : HasEtaleLocalProperty B S hS Y.1 (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : IsCoherent B S hS X.1 X.2 F)
    (hsupp : HasProperSupport B S hS X.2 Y.2 f.hom hf ((SheafOfModules.toSheaf _).obj F))
    (h03DW : ∀ (Z : ClosedSubspaces B S hS X.1)
      (hrep : yoneda.relativelyRepresentable (closedSubspaceInclusion B S hS X Z).hom)
      (G : Modules.{u, u} B S hS (closedSubspaceToSpace B S hS X Z).1
        (closedSubspaceToSpace B S hS X Z).2) (n : ℕ),
      ChartwiseIsZeroHigherDirectImage B S hS (closedSubspaceInclusion B S hS X Z) hrep G n)
    (h08AR : CoherentHigherDirectImageOfProper B S hS Y)
    (h0734 : HigherDirectImageCompOfAcyclic B S hS f) (p : ℕ) :
    have := hasInjectiveResolutions_modules B S hS X.1 X.2
    IsCoherent B S hS Y.1 Y.2 (((modulePushforward B S hS f).rightDerived p).obj F)

AlgebraicGeometry.Space.isCoherent_higherDirectImage_of_hasProperSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/ProperSupportHigherDirectImageCoherence.lean, line 155. References: EGA III (3.2.1), “more general”; EGA III (4.1.10), “more general”.

Stacks 08GC. Let S be a scheme, let f : X ⟶ Y be a morphism of algebraic spaces over S which is locally of finite type with Y locally Noetherian, and let 𝓕 be a coherent 𝒪_X-module whose support is proper over Y. Then R^p f_*𝓕 is a coherent 𝒪_Y-module for every p.

By AlgebraicGeometry.Space.exists_closedSubspace_higherDirectImage_iso, R^p f_*𝓕 ≅ R^p (i ≫ f)_*𝓖 for a closed subspace i : Z → X proper over Y and a coherent 𝒪_Z-module 𝓖; that is coherent by Stacks 08AR.

theorem isCoherent_higherDirectImage_of_hasProperSupport (f : X ⟶ Y)
    (hf : IsLocallyOfFiniteType B S hS f.hom)
    (hY : HasEtaleLocalProperty B S hS Y.1 (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : IsCoherent B S hS X.1 X.2 F)
    (hsupp : HasProperSupport B S hS X.2 Y.2 f.hom hf ((SheafOfModules.toSheaf _).obj F))
    (p : ℕ) :
    have := hasInjectiveResolutions_modules B S hS X.1 X.2
    IsCoherent B S hS Y.1 Y.2 (((modulePushforward B S hS f).rightDerived p).obj F)

AlgebraicGeometry.Space.isCoherent_rightDerived_modulePushforward_of_properSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/ProperSupportHigherDirectImageCoherent.lean, line 49.

Let f : X ⟶ Y be a morphism of algebraic spaces over S which is locally of finite type, with Y locally Noetherian, and let 𝓕 be a coherent 𝒪_X-module with support proper over Y. Then R^p f_*𝓕 is a coherent 𝒪_Y-module for every p.

theorem isCoherent_rightDerived_modulePushforward_of_properSupport
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hf : IsLocallyOfFiniteType B S hS f.hom)
    (hY : HasEtaleLocalProperty B S hS Y.1 (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : IsCoherent B S hS X.1 X.2 F)
    (hsupp : HasProperSupport B S hS X.2 Y.2 f.hom hf ((SheafOfModules.toSheaf _).obj F))
    (p : ℕ) :
    have := hasInjectiveResolutions_modules B S hS X.1 X.2
    IsCoherent B S hS Y.1 Y.2 (((modulePushforward B S hS f).rightDerived p).obj F)
Sources
LeanAlgebraicGeometry.Space.not_tfae_isProper_closedSubspace · AlgebraicGeometry.Space.IsProperOver · AlgebraicGeometry.Space.isProper_reducedClosedSubspace_iff_exists · AlgebraicGeometry.Space.exists_isProper_closedSubspace_iff_forall · AlgebraicGeometry.Space.isProperOver_of_subset · AlgebraicGeometry.Space.isProperOver_preimage · AlgebraicGeometry.Space.isProperOver_image_of_universallyClosed · AlgebraicGeometry.Space.isProperOver_image_of_isSeparated

Section75.8 Derived category of coherent modules#

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

Tag 08GJ, an equation

Tag 08GJ in the Stacks Project.

AlgebraicGeometry.Space.coherentDerivedComparison_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentDerivedComparison.lean, line 210. The attribute's comment: “well-definedness”.

Stacks 08GJ, well-definedness. The derived functor of the inclusion of the coherent 𝒪_F-modules has coherent cohomology in every degree: the inclusion is exact, so it commutes with cohomology.

theorem coherentDerivedComparison_mem (K : DerivedCategory (CoherentModules.{u, u} B S hS F hF)) :
    DerivedCategoryB.derivedCategoryB (isCoherent.{u, u} B S hS F hF)
      ((isCoherent.{u, u} B S hS F hF).ι.mapDerivedCategory.obj K)

AlgebraicGeometry.Space.coherentDerivedComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentDerivedComparison.lean, line 226.

Stacks 08GJ. The canonical functor from the derived category of the coherent 𝒪_F-modules to the derived category of all 𝒪_F-modules with coherent cohomology,

D(Coh(𝒪_F)) ⟶ D_Coh(𝒪_F),

obtained by factoring the derived functor of the exact inclusion Coh(𝒪_F) ⥤ Mod(𝒪_F) through D_Coh(𝒪_F).

noncomputable def coherentDerivedComparison :
    DerivedCategory (CoherentModules.{u, u} B S hS F hF) ⥤
      CoherentDerivedCategory.{u} B S hS F hF

AlgebraicGeometry.Space.coherentDerivedComparisonCompιIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentDerivedComparison.lean, line 237. The attribute's comment: “canonical comparison”.

Stacks 08GJ, the canonical comparison. The functor D(Coh(𝒪_F)) ⥤ D_Coh(𝒪_F) followed by the inclusion of D_Coh(𝒪_F) into D(𝒪_F) is the derived functor of the inclusion Coh(𝒪_F) ⥤ Mod(𝒪_F); that is, the comparison is a factorisation of the latter.

noncomputable def coherentDerivedComparisonCompιIso :
    coherentDerivedComparison B S hS F hF ⋙
        (DerivedCategoryB.derivedCategoryB (isCoherent.{u, u} B S hS F hF)).ι ≅
      (isCoherent.{u, u} B S hS F hF).ι.mapDerivedCategory
Tag 08GK, a lemma

Tag 08GK in the Stacks Project.

AlgebraicGeometry.Space.derivedCategoryBBounded_derivedModulePushforward_of_hasProperSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/DerivedPushforwardCoherentProperSupport.lean, line 154.

Let S be a scheme and f : X ⟶ Y a morphism of algebraic spaces over S which is locally of finite type, with Y Noetherian. Let E ∈ D^b_{Coh}(𝒪_X) be such that the support of H^i(E) is proper over Y for all i. Then Rf_*E ∈ D^b_{Coh}(𝒪_Y).

theorem derivedCategoryBBounded_derivedModulePushforward_of_hasProperSupport
    (hTop : B.Contains (⊤_ Scheme.{u})) (f : X ⟶ Y) (hf : IsLocallyOfFiniteType B S hS f.hom)
    (hY : IsNoetherian B S hS hTop Y.1)
    (E : DerivedCategory (Modules.{u, u} B S hS X.1 X.2))
    (hE : derivedCategoryBBounded (isCoherent.{u, u} B S hS X.1 X.2) E)
    (hsupp : ∀ i : ℤ, HasProperSupport B S hS X.2 Y.2 f.hom hf
      ((SheafOfModules.toSheaf _).obj
        ((DerivedCategory.homologyFunctor (Modules.{u, u} B S hS X.1 X.2) i).obj E))) :
    derivedCategoryBBounded (isCoherent.{u, u} B S hS Y.1 Y.2)
      ((Stacks.DerivedFunctor.totalRightDerived (modulePushforward B S hS f)).obj E)
Tag 0D0R, a lemma

Tag 0D0R in the Stacks Project.

AlgebraicGeometry.Space.derivedCategoryBPlus_derivedModulePushforward_of_hasProperSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/DerivedPushforwardCoherentProperSupport.lean, line 182. The attribute's comment: “with the support of each H^i(E) proper over Y: proper over S, as printed, the statement fails (the open immersion of one chart P^1 into the projective line with doubled origin over a field, with E = O_X), and Y is what the source's proof, through 08GK, uses”.

Let S be a scheme and f : X ⟶ Y a morphism of algebraic spaces over S which is locally of finite type, with Y Noetherian. Let E ∈ D^+_{Coh}(𝒪_X) be such that the support of H^i(E) is proper over Y for all i. Then Rf_*E ∈ D^+_{Coh}(𝒪_Y). (With the support only proper over S the statement is false; see the module documentation.)

theorem derivedCategoryBPlus_derivedModulePushforward_of_hasProperSupport
    (hTop : B.Contains (⊤_ Scheme.{u})) (f : X ⟶ Y) (hf : IsLocallyOfFiniteType B S hS f.hom)
    (hY : IsNoetherian B S hS hTop Y.1)
    (E : DerivedCategory (Modules.{u, u} B S hS X.1 X.2))
    (hE : derivedCategoryBPlus (isCoherent.{u, u} B S hS X.1 X.2) E)
    (hsupp : ∀ i : ℤ, HasProperSupport B S hS X.2 Y.2 f.hom hf
      ((SheafOfModules.toSheaf _).obj
        ((DerivedCategory.homologyFunctor (Modules.{u, u} B S hS X.1 X.2) i).obj E))) :
    derivedCategoryBPlus (isCoherent.{u, u} B S hS Y.1 Y.2)
      ((Stacks.DerivedFunctor.totalRightDerived (modulePushforward B S hS f)).obj E)
Tag 0D0S, a lemma

Tag 0D0S in the Stacks Project.

AlgebraicGeometry.Space.isBoundedBelow_sheafHomComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentDerivedInternalHom.lean, line 269. The attribute's comment: “the bounded-below clause, on a pair of models and with no Noetherian or coherence hypothesis”.

Stacks 0D0S, the bounded-below clause, on a pair of models. If A is concentrated in degrees ≤ d and J in degrees ≥ b, the class of the internal Hom complex SheafHom(A, J) in D(𝒪_X) is cohomologically bounded below.

For A a model of K and J a K-injective model of L this object is RSheafHom(K, L), so this is the D⁺ half of the tag, with no hypothesis beyond the two bounds — neither local Noetherianity nor coherence of the cohomology of K and L.

public theorem isBoundedBelow_sheafHomComplex
    (d b : ℤ) (A J : CochainComplex (Modules.{u, max (u + 1) m} B S hS F hF) ℤ)
    [CochainComplex.IsStrictlyLE A d] [CochainComplex.IsStrictlyGE J b] :
    DerivedCategoryB.IsBoundedBelow
      (DerivedCategory.Q.obj
        (sheafHomComplex (smallEtaleRingedSite B S hS F hF) A J).obj)

AlgebraicGeometry.Space.isBoundedBelow_derivedSheafHomOnSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentDerivedInternalHom.lean, line 319. The attribute's comment: “the bounded-below clause, for K and L themselves and with no Noetherian hypothesis”.

Stacks 0D0S, the bounded-below clause. Let X be an algebraic space over S. If K is in D⁻_Coh(𝒪_X) and L is in D⁺_Coh(𝒪_X), then RSheafHom(K, L) is cohomologically bounded below.

RSheafHom(K, L) is the class of the internal Hom complex SheafHom(A, J) of a model A of K and a K-injective model J of L; such a pair exists by AlgebraicGeometry.Space.exists_isStrictlyLE_isStrictlyGE_isKInjective_model, and the conclusion holds for it, by AlgebraicGeometry.Space.isBoundedBelow_sheafHomComplex.

Only the boundedness halves of hK and hL are used, and local Noetherianity of X is not needed.

public theorem isBoundedBelow_derivedSheafHomOnSpace
    (K L : DerivedCategory (Modules.{u, max (u + 1) m} B S hS F hF))
    (hK : DerivedCategoryB.derivedCategoryBMinus
      (fun N : Modules.{u, max (u + 1) m} B S hS F hF =>
        SheafOfModules.IsCoherentOnSite N) K)
    (hL : DerivedCategoryB.derivedCategoryBPlus
      (fun N : Modules.{u, max (u + 1) m} B S hS F hF =>
        SheafOfModules.IsCoherentOnSite N) L) :
    ∃ A J : CochainComplex (Modules.{u, max (u + 1) m} B S hS F hF) ℤ,
      CochainComplex.IsKInjective J ∧ Nonempty (DerivedCategory.Q.obj A ≅ K) ∧
        Nonempty (DerivedCategory.Q.obj J ≅ L) ∧
        DerivedCategoryB.IsBoundedBelow
          (DerivedCategory.Q.obj
            (sheafHomComplex (smallEtaleRingedSite B S hS F hF) A J).obj)

AlgebraicGeometry.Space.derivedCategoryBPlus_isCoherentOnSite_sheafHomComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentDerivedInternalHomCoherentCohomology.lean, line 151. The attribute's comment: “read on a model of K and a K-injective model of L”.

Stacks 0D0S. On a locally Noetherian algebraic space, RSheafHom(K, L) lies in D⁺_Coh(𝒪_X) for K in D⁻_Coh(𝒪_X) and L in D⁺_Coh(𝒪_X), read on a model A of K and a K-injective model J of L.

theorem derivedCategoryBPlus_isCoherentOnSite_sheafHomComplex
    [HasDerivedCategory.{t} (Modules.{u, u + 1} B S hS X.1 X.2)]
    (hN : HasEtaleLocalProperty B S hS X.1 (fun V : Scheme.{u} ↦ IsLocallyNoetherian V))
    (d b : ℤ) (A J : CochainComplex (Modules.{u, u} B S hS X.1 X.2) ℤ)
    [CochainComplex.IsStrictlyLE A d] [CochainComplex.IsKInjective J]
    [CochainComplex.IsStrictlyGE J b]
    (hA : ∀ i, SheafOfModules.IsCoherentOnSite (A.homology i))
    (hJ : ∀ i, SheafOfModules.IsCoherentOnSite (J.homology i)) :
    DerivedCategoryB.derivedCategoryBPlus
      (fun N : Modules.{u, u + 1} B S hS X.1 X.2 => SheafOfModules.IsCoherentOnSite N)
      (DerivedCategory.Q.obj
        (sheafHomComplex (smallEtaleRingedSite B S hS X.1 X.2) A J).obj)
Tag 0D0T, a lemma

Tag 0D0T in the Stacks Project.

AlgebraicGeometry.Space.moduleFinite_hom_shift_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperExtFiniteComplexes.lean, line 223.

Stacks 0D0T. Let A be a Noetherian ring and X an algebraic space over A proper over A. Let K ∈ D⁻_Coh(𝒪_X) and L ∈ D⁺_Coh(𝒪_X). Then Ext^n_X(K, L) = Hom_{D(𝒪_X)}(K, L[n]) is a finite A-module for every n ∈ ℤ.

theorem moduleFinite_hom_shift_of_isProper [IsNoetherianRing A]
    (f : X ⟶ yoneda.obj (baseObject A B hA)) (hf : IsProper B (Spec (.of A)) hA f)
    (K L : DerivedCategory (Modules.{u, u} B (Spec (.of A)) hA X hX))
    (hK : DerivedCategoryB.derivedCategoryBMinus (isCoherent.{u, u} B (Spec (.of A)) hA X hX) K)
    (hL : DerivedCategoryB.derivedCategoryBPlus (isCoherent.{u, u} B (Spec (.of A)) hA X hX) L)
    (n : ℤ) : Module.Finite A (K ⟶ L⟦n⟧)
Sources
LeanAlgebraicGeometry.Space.coherentDerivedComparison_mem · AlgebraicGeometry.Space.coherentDerivedComparison · AlgebraicGeometry.Space.coherentDerivedComparisonCompιIso · AlgebraicGeometry.Space.derivedCategoryBBounded_derivedModulePushforward_of_hasProperSupport · AlgebraicGeometry.Space.derivedCategoryBPlus_derivedModulePushforward_of_hasProperSupport · AlgebraicGeometry.Space.isBoundedBelow_sheafHomComplex · AlgebraicGeometry.Space.isBoundedBelow_derivedSheafHomOnSpace · AlgebraicGeometry.Space.derivedCategoryBPlus_isCoherentOnSite_sheafHomComplex

Section75.9 Induction principle#

Section 75.9 of the Stacks Project, Tag 08GL. 6 tags here are carried by 27 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 08GM, a definition

Tag 08GM in the Stacks Project.

AlgebraicGeometry.Space.IsElementaryDistinguishedSquare, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/ElementaryDistinguishedSquare.lean, line 100.

Stacks 08GM. An open subspace U of an algebraic space W together with an étale morphism f : V ⟶ W which is an isomorphism over the reduced closed subspace on the complement of U form an elementary distinguished square.

structure IsElementaryDistinguishedSquare (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {W V : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hW : IsAlgebraicSpace B S hS W) (U : Subfunctor W) (f : V ⟶ W) : Prop

AlgebraicGeometry.Space.isElementaryDistinguishedSquare_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/ElementaryDistinguishedSquare.lean, line 121. The attribute's comment: “characterization”.

An elementary distinguished square is exactly an open subspace together with an étale morphism which is an isomorphism over the reduced closed complement of that subspace.

theorem isElementaryDistinguishedSquare_iff (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {W V : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hW : IsAlgebraicSpace B S hS W) (U : Subfunctor W) (f : V ⟶ W) :
    IsElementaryDistinguishedSquare B S hS hW U f ↔
      (IsAlgebraicSpace B S hS V ∧ IsOpenSubspace B S hS U ∧ IsEtale B S hS f ∧
        ∃ hT : IsClosed (Set.range (pointsMap B S hS U.toFunctor U.ι))ᶜ,
          IsIso ((reducedClosedSubspace B S hS W hW
            (Set.range (pointsMap B S hS U.toFunctor U.ι))ᶜ hT).fromPreimage f))
Tag 08GN, a lemma

Tag 08GN in the Stacks Project.

AlgebraicGeometry.Space.isElementaryDistinguishedSquare_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/ElementaryDistinguishedSquare.lean, line 165. The attribute's comment: “base_change”.

Stacks 08GN, part (2). An elementary distinguished square stays elementary distinguished after base change along any morphism of algebraic spaces: the open subspace is replaced by its preimage and the étale morphism by its base change.

theorem isElementaryDistinguishedSquare_preimage (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S)
    {W V W' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hW : IsAlgebraicSpace B S hS W)
    (hW' : IsAlgebraicSpace B S hS W') (U : Subfunctor W) (f : V ⟶ W)
    (h : IsElementaryDistinguishedSquare B S hS hW U f) (p : W' ⟶ W) :
    IsElementaryDistinguishedSquare B S hS hW' (U.preimage p) (Limits.pullback.snd f p)

AlgebraicGeometry.Space.isElementaryDistinguishedSquare_openRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/ElementaryDistinguishedSquare.lean, line 267. The attribute's comment: “open_restriction”.

Stacks 08GN, restriction to open subspaces. Let U ⊆ U' be open subspaces of W and let V' be an open subspace of V. The union of the point set of U' with the image of the point set of V' is the point set of an open subspace W' of W; the morphism V' ⟶ W factors through W', and the square formed by U' inside W' and that factorisation is again elementary distinguished.

The union is described by its set of points rather than as the range of V'.ι ≫ f, which need not be an open subspace, and U' is presented inside W' as the range of the canonical inclusion U' ⟶ W'.

theorem isElementaryDistinguishedSquare_openRestriction (B : BigFppfSite.{u})
    (S : Scheme.{u}) (hS : B.Contains S)
    {W V : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hW : IsAlgebraicSpace B S hS W)
    (U : Subfunctor W) (f : V ⟶ W)
    (hsq : IsElementaryDistinguishedSquare B S hS hW U f)
    (V' : Subfunctor V) (hV' : IsOpenSubspace B S hS V')
    (U' : Subfunctor W) (hU' : IsOpenSubspace B S hS U') (hUU' : U ≤ U') :
    ∃ (W' : Subfunctor W) (hW' : IsOpenSubspace B S hS W') (hU'W' : U' ≤ W')
      (f' : V'.toFunctor ⟶ W'.toFunctor),
      (Set.range (pointsMap B S hS W'.toFunctor W'.ι) =
        Set.range (pointsMap B S hS U'.toFunctor U'.ι) ∪
          Set.range (pointsMap B S hS V'.toFunctor (V'.ι ≫ f))) ∧
      (f' ≫ W'.ι = V'.ι ≫ f) ∧
      IsElementaryDistinguishedSquare B S hS hW'.1
        (Subfunctor.range (Subfunctor.homOfLe hU'W')) f'

AlgebraicGeometry.Space.isElementaryDistinguishedSquare_relocalizeRestrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/ElementaryDistinguishedSquare.lean, line 701. The attribute's comment: “scheme_change”.

Stacks 08GN, change of base scheme. An elementary distinguished square over S stays elementary distinguished after restriction along a morphism g : S' ⟶ S of the site: the open subspace is replaced by the image of the restricted inclusion and the étale morphism by its restriction.

theorem isElementaryDistinguishedSquare_relocalizeRestrict (B : BigFppfSite.{u})
    (S S' : Scheme.{u}) (hS : B.Contains S) (hS' : B.Contains S')
    (g : B.obj hS' ⟶ B.obj hS) {W V : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hW : IsAlgebraicSpace B S hS W) (U : Subfunctor W) (f : V ⟶ W)
    (h : IsElementaryDistinguishedSquare B S hS hW U f) :
    IsElementaryDistinguishedSquare B S' hS'
      (isAlgebraicSpace_relocalizeRestrict B S' S hS' hS g W hW)
      (Subfunctor.range ((OverShriek.relocalizeRestrict g).map U.ι))
      ((OverShriek.relocalizeRestrict g).map f)
Tag 08GP, a lemma

Tag 08GP in the Stacks Project.

AlgebraicGeometry.Space.qcqs_induction_on, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/InductionPrinciple/QcqsInduction.lean, line 333. The attribute's comment: “every quasi-compact quasi-separated étale object”.

Stacks 08GP. Induction on the quasi-compact quasi-separated objects of the spaces-étale site of a quasi-compact quasi-separated algebraic space X: a property of algebraic spaces étale over X which holds on the affine ones and is inherited across an elementary distinguished square with affine étale member holds on all of them.

public theorem qcqs_induction_on
    (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (hZ : B.Contains (⊤_ Scheme.{u}))
    (X : AlgebraicSpaces B S hS)
    (hXqc : IsQuasiCompactSpace B S hS X.1)
    (hXqs : IsAbsolutelyQuasiSeparated B S hS hZ X.1)
    (P : (Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) →
      (Y ⟶ X.1) → Prop)
    (haff : ∀ V : SpacesEtale B S hS X,
      IsAffineSpace B S hS V.1.left.1 →
        P V.1.left.1 V.1.hom.hom)
    (hstep : ∀ (W V : SpacesEtale B S hS X)
      (U : Subfunctor W.1.left.1)
      (f : V.1.left.1 ⟶ W.1.left.1),
      (f ≫ W.1.hom.hom = V.1.hom.hom) →
      IsElementaryDistinguishedSquare B S hS W.1.left.property U f →
      IsQuasiCompactSpace B S hS W.1.left.1 →
      IsAbsolutelyQuasiSeparated B S hS hZ W.1.left.1 →
      IsQuasiCompactSpace B S hS U.toFunctor →
      IsAffineSpace B S hS V.1.left.1 →
      P U.toFunctor (U.ι ≫ W.1.hom.hom) →
      P V.1.left.1 V.1.hom.hom →
      P (pullback U.ι f)
        (pullback.fst U.ι f ≫ U.ι ≫ W.1.hom.hom) →
      P W.1.left.1 W.1.hom.hom) :
    ∀ Y : SpacesEtale B S hS X,
      IsQuasiCompactSpace B S hS Y.1.left.1 →
      IsAbsolutelyQuasiSeparated B S hS hZ Y.1.left.1 →
      P Y.1.left.1 Y.1.hom.hom

AlgebraicGeometry.Space.qcqs_induction_on_self, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/InductionPrinciple/QcqsInduction.lean, line 454. The attribute's comment: “the base space”.

Stacks 08GP for the base space: a property of algebraic spaces étale over a quasi-compact quasi-separated algebraic space X which holds on the affine ones and is inherited across an elementary distinguished square with affine étale member holds for X itself, taken with its identity morphism.

public theorem qcqs_induction_on_self
    (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (hZ : B.Contains (⊤_ Scheme.{u}))
    (X : AlgebraicSpaces B S hS)
    (hXqc : IsQuasiCompactSpace B S hS X.1)
    (hXqs : IsAbsolutelyQuasiSeparated B S hS hZ X.1)
    (P : (Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) →
      (Y ⟶ X.1) → Prop)
    (haff : ∀ V : SpacesEtale B S hS X,
      IsAffineSpace B S hS V.1.left.1 →
        P V.1.left.1 V.1.hom.hom)
    (hstep : ∀ (W V : SpacesEtale B S hS X)
      (U : Subfunctor W.1.left.1)
      (f : V.1.left.1 ⟶ W.1.left.1),
      (f ≫ W.1.hom.hom = V.1.hom.hom) →
      IsElementaryDistinguishedSquare B S hS W.1.left.property U f →
      IsQuasiCompactSpace B S hS W.1.left.1 →
      IsAbsolutelyQuasiSeparated B S hS hZ W.1.left.1 →
      IsQuasiCompactSpace B S hS U.toFunctor →
      IsAffineSpace B S hS V.1.left.1 →
      P U.toFunctor (U.ι ≫ W.1.hom.hom) →
      P V.1.left.1 V.1.hom.hom →
      P (pullback U.ι f)
        (pullback.fst U.ι f ≫ U.ι ≫ W.1.hom.hom) →
      P W.1.left.1 W.1.hom.hom) :
    P X.1 (𝟙 X.1)
Tag 08GQ, a lemma

Tag 08GQ in the Stacks Project.

AlgebraicGeometry.Space.qcqs_induction_on_collection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/InductionPrinciple/QcqsInduction.lean, line 491.

Stacks 08GQ. Induction inside a collection 𝓑 of objects of the spaces-étale site of a quasi-compact quasi-separated algebraic space X: a property of the members of 𝓑 holds throughout 𝓑 as soon as 𝓑 consists of quasi-compact quasi-separated objects, is closed under quasi-compact open subspaces and contains every affine object, the property holds on the affine objects, and it is inherited across an elementary distinguished square whose ambient object lies in 𝓑 and whose étale member is affine.

public theorem qcqs_induction_on_collection
    (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (hZ : B.Contains (⊤_ Scheme.{u}))
    (X : AlgebraicSpaces B S hS)
    (hXqc : IsQuasiCompactSpace B S hS X.1)
    (hXqs : IsAbsolutelyQuasiSeparated B S hS hZ X.1)
    (𝓑 P : (Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) →
      (Y ⟶ X.1) → Prop)
    (hBqcqs : ∀ W : SpacesEtale B S hS X,
      𝓑 W.1.left.1 W.1.hom.hom →
      IsQuasiCompactSpace B S hS W.1.left.1 ∧
        IsAbsolutelyQuasiSeparated B S hS hZ W.1.left.1)
    (hBopen : ∀ (W : SpacesEtale B S hS X)
      (U : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (i : U ⟶ W.1.left.1),
      𝓑 W.1.left.1 W.1.hom.hom →
      IsAlgebraicSpace B S hS U →
      IsOpenImmersion B S hS i →
      IsQuasiCompactSpace B S hS U →
      𝓑 U (i ≫ W.1.hom.hom))
    (hBaff : ∀ V : SpacesEtale B S hS X,
      IsAffineSpace B S hS V.1.left.1 →
        𝓑 V.1.left.1 V.1.hom.hom)
    (hPaff : ∀ V : SpacesEtale B S hS X,
      IsAffineSpace B S hS V.1.left.1 →
        P V.1.left.1 V.1.hom.hom)
    (hstep : ∀ (W V : SpacesEtale B S hS X)
      (U : Subfunctor W.1.left.1)
      (f : V.1.left.1 ⟶ W.1.left.1),
      (f ≫ W.1.hom.hom = V.1.hom.hom) →
      IsElementaryDistinguishedSquare B S hS W.1.left.property U f →
      𝓑 W.1.left.1 W.1.hom.hom →
      IsQuasiCompactSpace B S hS U.toFunctor →
      IsAffineSpace B S hS V.1.left.1 →
      P U.toFunctor (U.ι ≫ W.1.hom.hom) →
      P V.1.left.1 V.1.hom.hom →
      P (pullback U.ι f)
        (pullback.fst U.ι f ≫ U.ι ≫ W.1.hom.hom) →
      P W.1.left.1 W.1.hom.hom) :
    ∀ W : SpacesEtale B S hS X,
      𝓑 W.1.left.1 W.1.hom.hom →
      P W.1.left.1 W.1.hom.hom
Tag 08GR, a remark

Tag 08GR in the Stacks Project.

AlgebraicGeometry.Space.IsQuasiCompactSeparated, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/InductionCollections.lean, line 228. The attribute's comment: “separated_objects”.

The quasi-compact separated algebraic spaces in the spaces-étale site.

public abbrev IsQuasiCompactSeparated
    (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (hZ : B.Contains (⊤_ Scheme.{u}))
    (Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) : Prop

AlgebraicGeometry.Space.isQuasiCompactSeparated_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/InductionCollections.lean, line 237. The attribute's comment: “separated_objects”.

The base algebraic space belongs to the collection.

public theorem isQuasiCompactSeparated_base
    (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (hZ : B.Contains (⊤_ Scheme.{u}))
    (X : AlgebraicSpaces B S hS)
    (hXqc : IsQuasiCompactSpace B S hS X.1)
    (hXsep : IsAbsolutelySeparated B S hS hZ X.1) :
    IsQuasiCompactSeparated B S hS hZ X.1

AlgebraicGeometry.Space.IsQuasiCompactSeparated.isAbsolutelyQuasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/InductionCollections.lean, line 247. The attribute's comment: “separated_objects”.

Every member of the collection is quasi-separated.

public theorem IsQuasiCompactSeparated.isAbsolutelyQuasiSeparated
    (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (hZ : B.Contains (⊤_ Scheme.{u}))
    (Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hY : IsQuasiCompactSeparated B S hS hZ Y) :
    IsAbsolutelyQuasiSeparated B S hS hZ Y

AlgebraicGeometry.Space.IsQuasiCompactSeparated.of_openImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/InductionCollections.lean, line 257. The attribute's comment: “separated_objects”.

A quasi-compact open subspace of a member is again a member.

public theorem IsQuasiCompactSeparated.of_openImmersion
    (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (hZ : B.Contains (⊤_ Scheme.{u}))
    (X : AlgebraicSpaces B S hS)
    (W : SpacesEtale B S hS X)
    (U : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (i : U ⟶ W.1.left.1)
    (hW : IsQuasiCompactSeparated B S hS hZ W.1.left.1)
    (hUspace : IsAlgebraicSpace B S hS U)
    (hi : IsOpenImmersion B S hS i)
    (hUqc : IsQuasiCompactSpace B S hS U) :
    IsQuasiCompactSeparated B S hS hZ U

AlgebraicGeometry.Space.isQuasiCompactSeparated_of_isAffineSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/InductionCollections.lean, line 284. The attribute's comment: “separated_objects”.

Every affine object of the spaces-étale site belongs to the collection.

public theorem isQuasiCompactSeparated_of_isAffineSpace
    (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (hZ : B.Contains (⊤_ Scheme.{u}))
    (X : AlgebraicSpaces B S hS)
    (V : SpacesEtale B S hS X)
    (hV : IsAffineSpace B S hS V.1.left.1) :
    IsQuasiCompactSeparated B S hS hZ V.1.left.1

AlgebraicGeometry.Space.qcqs_induction_on_quasiCompactSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/InductionCollections.lean, line 296. The attribute's comment: “separated_objects”.

Induction on quasi-compact separated objects of the spaces-étale site.

public theorem qcqs_induction_on_quasiCompactSeparated
    (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (hZ : B.Contains (⊤_ Scheme.{u}))
    (X : AlgebraicSpaces B S hS)
    (hXqc : IsQuasiCompactSpace B S hS X.1)
    (hXsep : IsAbsolutelySeparated B S hS hZ X.1)
    (P : (Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) →
      (Y ⟶ X.1) → Prop)
    (hPaff : ∀ V : SpacesEtale B S hS X,
      IsAffineSpace B S hS V.1.left.1 →
        P V.1.left.1 V.1.hom.hom)
    (hstep : ∀ (W V : SpacesEtale B S hS X)
      (U : Subfunctor W.1.left.1)
      (f : V.1.left.1 ⟶ W.1.left.1),
      (f ≫ W.1.hom.hom = V.1.hom.hom) →
      IsElementaryDistinguishedSquare B S hS W.1.left.property U f →
      IsQuasiCompactSeparated B S hS hZ W.1.left.1 →
      IsQuasiCompactSpace B S hS U.toFunctor →
      IsAffineSpace B S hS V.1.left.1 →
      P U.toFunctor (U.ι ≫ W.1.hom.hom) →
      P V.1.left.1 V.1.hom.hom →
      P (pullback U.ι f)
        (pullback.fst U.ι f ≫ U.ι ≫ W.1.hom.hom) →
      P W.1.left.1 W.1.hom.hom) :
    ∀ W : SpacesEtale B S hS X,
      IsQuasiCompactSeparated B S hS hZ W.1.left.1 →
        P W.1.left.1 W.1.hom.hom

AlgebraicGeometry.Space.IsQuasiCompactWithAffineDiagonal, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/InductionCollections.lean, line 406. The attribute's comment: “affine_diagonal_objects”.

A quasi-compact algebraic space with affine absolute diagonal.

public abbrev IsQuasiCompactWithAffineDiagonal
    (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (hZ : B.Contains (⊤_ Scheme.{u}))
    (Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) : Prop

AlgebraicGeometry.Space.isQuasiCompactWithAffineDiagonal_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/InductionCollections.lean, line 417. The attribute's comment: “affine_diagonal_objects”.

The base algebraic space belongs to the collection.

public theorem isQuasiCompactWithAffineDiagonal_base
    (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (hZ : B.Contains (⊤_ Scheme.{u}))
    (X : AlgebraicSpaces B S hS)
    (hXqc : IsQuasiCompactSpace B S hS X.1)
    (hXdiag : IsAffineHom B (⊤_ Scheme.{u}) hZ
      (diag (viewOverIntegers B S hS hZ X.1))) :
    IsQuasiCompactWithAffineDiagonal B S hS hZ X.1

AlgebraicGeometry.Space.IsQuasiCompactWithAffineDiagonal.isAbsolutelyQuasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/InductionCollections.lean, line 428. The attribute's comment: “affine_diagonal_objects”.

Every member of the collection is quasi-separated.

public theorem IsQuasiCompactWithAffineDiagonal.isAbsolutelyQuasiSeparated
    (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (hZ : B.Contains (⊤_ Scheme.{u}))
    (X : AlgebraicSpaces B S hS)
    (W : SpacesEtale B S hS X)
    (hW : IsQuasiCompactWithAffineDiagonal B S hS hZ W.1.left.1) :
    IsAbsolutelyQuasiSeparated B S hS hZ W.1.left.1

AlgebraicGeometry.Space.IsQuasiCompactWithAffineDiagonal.of_openImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/InductionCollections.lean, line 448. The attribute's comment: “affine_diagonal_objects”.

A quasi-compact open subspace of a member is again a member.

public theorem IsQuasiCompactWithAffineDiagonal.of_openImmersion
    (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (hZ : B.Contains (⊤_ Scheme.{u}))
    (X : AlgebraicSpaces B S hS)
    (W : SpacesEtale B S hS X)
    (U : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (i : U ⟶ W.1.left.1)
    (hW : IsQuasiCompactWithAffineDiagonal B S hS hZ W.1.left.1)
    (_hUspace : IsAlgebraicSpace B S hS U)
    (hi : IsOpenImmersion B S hS i)
    (hUqc : IsQuasiCompactSpace B S hS U) :
    IsQuasiCompactWithAffineDiagonal B S hS hZ U

AlgebraicGeometry.Space.isQuasiCompactWithAffineDiagonal_of_isAffineSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/InductionCollections.lean, line 469. The attribute's comment: “affine_diagonal_objects”.

Every affine object of the spaces-étale site belongs to the collection.

public theorem isQuasiCompactWithAffineDiagonal_of_isAffineSpace
    (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (hZ : B.Contains (⊤_ Scheme.{u}))
    (X : AlgebraicSpaces B S hS)
    (V : SpacesEtale B S hS X)
    (hV : IsAffineSpace B S hS V.1.left.1) :
    IsQuasiCompactWithAffineDiagonal B S hS hZ V.1.left.1

AlgebraicGeometry.Space.IsBasicEtaleObject, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/InductionCollections.lean, line 511. The attribute's comment: “smallest_collection”.

A quasi-compact open subspace of X or of an affine étale object over X.

public def IsBasicEtaleObject
    (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (X : AlgebraicSpaces B S hS)
    (Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (g : Y ⟶ X.1) : Prop

AlgebraicGeometry.Space.isBasicEtaleObject_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/InductionCollections.lean, line 551. The attribute's comment: “smallest_collection”.

The base belongs to the basic collection.

public theorem isBasicEtaleObject_base
    (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (X : AlgebraicSpaces B S hS)
    (hXqc : IsQuasiCompactSpace B S hS X.1) :
    IsBasicEtaleObject B S hS X X.1 (𝟙 X.1)

AlgebraicGeometry.Space.IsBasicEtaleObject.isQuasiCompactSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/InductionCollections.lean, line 560. The attribute's comment: “smallest_collection”.

A basic étale object is quasi-compact.

public theorem IsBasicEtaleObject.isQuasiCompactSpace
    (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (X : AlgebraicSpaces B S hS)
    (W : SpacesEtale B S hS X)
    (hW : IsBasicEtaleObject B S hS X W.1.left.1 W.1.hom.hom) :
    IsQuasiCompactSpace B S hS W.1.left.1

AlgebraicGeometry.Space.IsBasicEtaleObject.isAbsolutelyQuasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/InductionCollections.lean, line 569. The attribute's comment: “smallest_collection”.

A basic étale object is quasi-separated when X is.

public theorem IsBasicEtaleObject.isAbsolutelyQuasiSeparated
    (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (hZ : B.Contains (⊤_ Scheme.{u}))
    (X : AlgebraicSpaces B S hS)
    (hXqs : IsAbsolutelyQuasiSeparated B S hS hZ X.1)
    (W : SpacesEtale B S hS X)
    (hW : IsBasicEtaleObject B S hS X W.1.left.1 W.1.hom.hom) :
    IsAbsolutelyQuasiSeparated B S hS hZ W.1.left.1

AlgebraicGeometry.Space.IsBasicEtaleObject.of_openImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/InductionCollections.lean, line 586. The attribute's comment: “smallest_collection”.

Quasi-compact open subspaces of basic objects are basic.

public theorem IsBasicEtaleObject.of_openImmersion
    (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (X : AlgebraicSpaces B S hS)
    (W : SpacesEtale B S hS X)
    (U : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (i : U ⟶ W.1.left.1)
    (hW : IsBasicEtaleObject B S hS X W.1.left.1 W.1.hom.hom)
    (hUspace : IsAlgebraicSpace B S hS U)
    (hi : IsOpenImmersion B S hS i)
    (hUqc : IsQuasiCompactSpace B S hS U) :
    IsBasicEtaleObject B S hS X U (i ≫ W.1.hom.hom)

AlgebraicGeometry.Space.isBasicEtaleObject_of_isAffineSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/InductionCollections.lean, line 606. The attribute's comment: “smallest_collection”.

Every affine object of the étale site is basic.

public theorem isBasicEtaleObject_of_isAffineSpace
    (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (X : AlgebraicSpaces B S hS)
    (V : SpacesEtale B S hS X)
    (hV : IsAffineSpace B S hS V.1.left.1) :
    IsBasicEtaleObject B S hS X V.1.left.1 V.1.hom.hom

AlgebraicGeometry.Space.IsAdmissibleCollection.mem_of_isBasicEtaleObject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/InductionCollections.lean, line 630. The attribute's comment: “smallest_collection”.

Every admissible collection contains all basic objects.

public theorem IsAdmissibleCollection.mem_of_isBasicEtaleObject
    (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (hZ : B.Contains (⊤_ Scheme.{u}))
    (X : AlgebraicSpaces B S hS)
    (C : (Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) →
      (Y ⟶ X.1) → Prop)
    (hC : IsAdmissibleCollection B S hS hZ X C)
    (W : SpacesEtale B S hS X)
    (hW : IsBasicEtaleObject B S hS X W.1.left.1 W.1.hom.hom) :
    C W.1.left.1 W.1.hom.hom
Tag 09IT, a lemma

Tag 09IT in the Stacks Project.

AlgebraicGeometry.Space.qcqs_induction_on_enlargement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/InductionPrinciple/EnlargementInduction.lean, line 34.

Stacks 09IT. Let X be a quasi-compact quasi-separated algebraic space and let W ⊆ X be a quasi-compact open subspace. A property P of the quasi-compact open subspaces of X which holds for W, and which for every elementary distinguished square (W₁ ⊆ W₂, f : V ⟶ W₂) with W₁, W₂ quasi-compact open subspaces of X containing W and V affine passes from W₁ to W₂, holds for X.

public theorem qcqs_induction_on_enlargement
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (hZ : B.Contains (⊤_ Scheme.{u}))
    (X : AlgebraicSpaces B S hS)
    (hXqc : IsQuasiCompactSpace B S hS X.1)
    (hXqs : IsAbsolutelyQuasiSeparated B S hS hZ X.1)
    (W : Subfunctor X.1) (hWopen : IsOpenSubspace B S hS W)
    (hWqc : IsQuasiCompactSpace B S hS W.toFunctor)
    (P : Subfunctor X.1 → Prop) (hPW : P W)
    (hstep : ∀ (W₁ W₂ : Subfunctor X.1) (hW₁ : IsOpenSubspace B S hS W₁)
      (hW₂ : IsOpenSubspace B S hS W₂),
      IsQuasiCompactSpace B S hS W₁.toFunctor →
      IsQuasiCompactSpace B S hS W₂.toFunctor →
      ∀ hle : W₁ ≤ W₂, W ≤ W₁ →
      ∀ {V : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : V ⟶ W₂.toFunctor),
        IsAffineSpace B S hS V →
        IsElementaryDistinguishedSquare B S hS hW₂.1
          (Subfunctor.range (Subfunctor.homOfLe hle)) f →
        P W₁ → P W₂) :
    P (⊤ : Subfunctor X.1)
Sources
LeanAlgebraicGeometry.Space.IsElementaryDistinguishedSquare · AlgebraicGeometry.Space.isElementaryDistinguishedSquare_iff · AlgebraicGeometry.Space.isElementaryDistinguishedSquare_preimage · AlgebraicGeometry.Space.isElementaryDistinguishedSquare_openRestriction · AlgebraicGeometry.Space.isElementaryDistinguishedSquare_relocalizeRestrict · AlgebraicGeometry.Space.qcqs_induction_on · AlgebraicGeometry.Space.qcqs_induction_on_self · AlgebraicGeometry.Space.qcqs_induction_on_collection

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.