36.30 Cohomology and base… to 36.38 K-groups

Section36.30 Cohomology and base change, VI#

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

Tag 0A1H, a lemma

Tag 0A1H in the Stacks Project.

AlgebraicGeometry.isPerfect_derivedPushforward_tensor_and_isIso_tensorFlatBaseChangeMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/TensorFinitelyPresentedPerfect.lean, line 88.

[Stacks, Tag 0A1H]. Let f : X ⟶ S be a morphism of schemes of finite presentation, let E be a perfect object of D(𝒪_X) and let 𝒢^• be a bounded complex of finitely presented 𝒪_X-modules, flat over S, with support proper over S. Then K = Rf_*(E ⊗^L_{𝒪_X} 𝒢^•) is a perfect object of D(𝒪_S), and its formation commutes with arbitrary base change: for every cartesian square the canonical map Lg^*Rf_*(E ⊗^L 𝒢^•) ⟶ Rf'_*(L(g')^*E ⊗^L (g')^*𝒢^•) of AlgebraicGeometry.tensorFlatBaseChangeMap is an isomorphism.

theorem isPerfect_derivedPushforward_tensor_and_isIso_tensorFlatBaseChangeMap {X S : Scheme.{u}}
    (f : X ⟶ S) (hf : FinitePresentation f) (E : DerivedCategory X.Modules)
    (hE : RingedSpace.IsPerfect (X := X.toRingedSpace) E) (G : CochainComplex X.Modules ℤ)
    (hG : letI : LocallyOfFinitePresentation f := hf.locallyOfFinitePresentation
      FlatProperSupportFinitelyPresented f G) :
    RingedSpace.IsPerfect (X := S.toRingedSpace)
        ((derivedPushforward f.toLRSHom.toShHom).obj
          (((derivedTensorProductFunctor X.sheaf).obj E).obj (DerivedCategory.Q.obj G))) ∧
      ∀ {X' S' : Scheme.{u}} (g : S' ⟶ S) (f' : X' ⟶ S') (g' : X' ⟶ X)
        (hsq : IsPullback g' f' f g),
        IsIso (tensorFlatBaseChangeMap f g f' g' (comp_toShHom_of_comm hsq.w) E G)

Tag 0A1I, a remark

Tag 0A1I in the Stacks Project.

Stacks.AlgebraicGeometry.FinitePresentationGlobalSectionsModel.exists_finiteProjectiveModel_of_properSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/FinitePresentationGlobalSectionsModel.lean, line 149. The attribute's comment: “existence of the finite projective model M and the identification RGamma(X_{R'}, G_{R'}) = M tensor_R R' for every base change; naturality in R' NOT stated. CARRIED: the pseudo-coherence half of the perfection, as the named residue PseudoCoherentDerivedGlobalSectionsOfProperSupport, and separatedness of f, a narrowing. Proved: the finite-Tor-dimension half and the identification. Accounting in the docstring”.

Let R be a ring, let X be a scheme of finite presentation over R, separated over R, and let G be a finitely presented 𝒪_X-module, flat over R, whose support is proper over R. Assume hres, pseudo-coherence of RΓ(X, G) in this generality. Then there is a finite complex M of finite projective R-modules such that for every homomorphism φ : R ⟶ R' and every cartesian square exhibiting X' as the base change of X along Spec R' ⟶ Spec R,

RΓ(X_{R'}, G_{R'}) ≅ M ⊗_R R' in D(R').

Naturality of this identification in R' is not asserted.

theorem exists_finiteProjectiveModel_of_properSupport
    (hres : PseudoCoherentDerivedGlobalSectionsOfProperSupport.{u})
    {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) [IsSeparated f]
    (hf : FinitePresentation f) (G : X.Modules) (hGfp : G.IsFinitePresentation)
    (hflat : IsFlatOver f.toLRSHom.toShHom G)
    (hsupp : letI : LocallyOfFinitePresentation f := hf.locallyOfFinitePresentation
      ∃ Z : Closeds X, IsProperOver f Z ∧ SheafOfModules.supp G ⊆ (Z : Set X)) :
    ∃ (M : CochainComplex (ModuleCat.{u} R) ℤ) (a b : ℤ),
      M.IsStrictlyGE a ∧ M.IsStrictlyLE b ∧
        (∀ i : ℤ, Module.Finite R (M.X i)) ∧ (∀ i : ℤ, Module.Projective R (M.X i)) ∧
        ∀ {R' : Type u} [CommRing R'] (φ : R →+* R') {X' : Scheme.{u}}
          {f' : X' ⟶ Spec (.of R')} {g : X' ⟶ X}
          (_hsq : IsPullback g f' f (Spec.map (CommRingCat.ofHom φ))),
          Nonempty (derivedGlobalSectionsOverBase f' ((Scheme.Modules.pullback g).obj G) ≅
            DerivedCategory.Q.obj (extendScalarsComplex φ M))

Stacks.AlgebraicGeometry.ProperSupportModel.exists_finiteProjectiveModel_derivedGlobalSections_functorial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ProperSupportModel/FunctorialModel.lean, line 203. The attribute's comment: “the remark in full: one finite complex M of finite projective R-modules, the identification RGamma(X_{R'}, G_{R'}) = M tensor_R R' in D(R') for every base change, as a family of isomorphisms indexed by the ring map and the cartesian square and pinned to a single chain-level model over R, and the functoriality in R' as the cocycle square of the chain-level comparisons for two successive base changes; under exactly the source's hypotheses (X of finite presentation over R, not assumed separated; G finitely presented, flat over R, with proper support). The comparisons are Čech models of the scheme-theoretic support of G, which is proper over R; the cover is bound inside the existential”.

[Stacks, Tag 0A1I]. Let R be a ring, let X be a scheme of finite presentation over R and let G be a finitely presented 𝒪_X-module, flat over R, whose support is proper over R. Then there is a finite complex M of finite projective R-modules and, for every ring map φ : R ⟶ R' and every cartesian square exhibiting X' as X ×_R R', an identification

c(φ, square) : RΓ(X_{R'}, G_{R'}) ≅ M ⊗_R R' in D(R'),

functorial in R': there are a finite affine open cover U of the scheme-theoretic support Z of G and chain-level comparisons

Θ(φ, square) : M ⊗_R R' ⟶ Č_alt(Z_{R'}, U_{R'}, G'_{R'}),

G' = G|_Z, such that

• every Θ(φ, square) is a quasi-isomorphism;
• c(φ, square) is the identification Θ(φ, square) induces, through the Čech model of RΓ(Z_{R'}, G'_{R'}) and the canonical RΓ(Z_{R'}, G'_{R'}) ≅ RΓ(X_{R'}, G_{R'}) (supportComparisonIso);
• the comparisons are functorial in R': for a second ring map ψ : R' ⟶ R'' and a second cartesian square, the extension of scalars along ψ of Θ(φ, square), followed by the Čech base-change isomorphism of [Stacks, Tag 07VK] (2) for Z_{R''} = Z_{R'} ×_{R'} R'' and by the identifications of the modules and covers, is Θ(ψ ∘ φ, pasted square) read through (M ⊗_R R') ⊗_{R'} R'' ≅ M ⊗_R R''.

The hypotheses are exactly the source's: X is not assumed separated, and nothing about RΓ(X, G) is assumed. M comes from the perfection of RΓ(X, G), which is [Stacks, Tag 0A1H]; the identifications and their functoriality are computed on the support Z, which is proper and hence separated over R; see the module docstring.

theorem exists_finiteProjectiveModel_derivedGlobalSections_functorial
    {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R))
    (hf : FinitePresentation f) (G : X.Modules) (hGfp : G.IsFinitePresentation)
    (hflat : IsFlatOver f.toLRSHom.toShHom G)
    (hsupp : letI : LocallyOfFinitePresentation f := hf.locallyOfFinitePresentation
      ∃ Z : Closeds X, IsProperOver f Z ∧ SheafOfModules.supp G ⊆ (Z : Set X)) :
    haveI : G.IsQuasicoherent := Stacks.Modules.isQuasicoherent_of_isFinitePresentation G
    haveI : G.IsFiniteType := Stacks.StalkFiniteType.isFiniteType_of_isFinitePresentation G
    letI : LocallyOfFinitePresentation f := hf.locallyOfFinitePresentation
    haveI : IsProper (supportι G ≫ f) := isProper_supportι_comp G f hsupp
    ∃ (M : CochainComplex (ModuleCat.{u} R) ℤ) (a b : ℤ),
      M.IsStrictlyGE a ∧ M.IsStrictlyLE b ∧
        (∀ i : ℤ, Module.Finite R (M.X i)) ∧ (∀ i : ℤ, Module.Projective R (M.X i)) ∧
        ∃ (c : ∀ {R' : Type u} [CommRing R'] (φ : R →+* R') {X' : Scheme.{u}}
              {f' : X' ⟶ Spec (.of R')} {g : X' ⟶ X},
              IsPullback g f' f (Spec.map (CommRingCat.ofHom φ)) →
                (derivedGlobalSectionsOverBase f' ((Scheme.Modules.pullback g).obj G) ≅
                  DerivedCategory.Q.obj (extendScalarsComplex φ M)))
          (I : Type u) (hIfin : Finite I) (hIlin : LinearOrder I)
          (U : I → (supportScheme G).Opens) (hU : (⊤ : (supportScheme G).Opens) = ⨆ i, U i)
          (hUaff : ∀ i, IsAffineOpen (U i)),
          haveI : Finite I := hIfin
          letI : LinearOrder I := hIlin
          ∃ (_haff : ∀ (r : ℕ) (s : Fin (r + 1) → I), IsAffineOpen (⨅ k, U (s k)))
            (Θ : ∀ {R' : Type u} [CommRing R'] (φ : R →+* R') {X' : Scheme.{u}}
                {f' : X' ⟶ Spec (.of R')} {g : X' ⟶ X},
                IsPullback g f' f (Spec.map (CommRingCat.ofHom φ)) →
                  (extendScalarsComplex φ M ⟶
                    baseAlternatingCechComplex (supportSnd G g ≫ f')
                      (fun j => supportFst G g ⁻¹ᵁ U j) (top_eq_iSup_preimage _ U hU)
                      ((Scheme.Modules.pullback (supportFst G g)).obj (supportModule G)))),
            (∀ {R' : Type u} [CommRing R'] (φ : R →+* R') {X' : Scheme.{u}}
                {f' : X' ⟶ Spec (.of R')} {g : X' ⟶ X}
                (hsq : IsPullback g f' f (Spec.map (CommRingCat.ofHom φ))),
                QuasiIso (Θ φ hsq)) ∧
              (∀ {R' : Type u} [CommRing R'] (φ : R →+* R') {X' : Scheme.{u}}
                  {f' : X' ⟶ Spec (.of R')} {g : X' ⟶ X}
                  (hsq : IsPullback g f' f (Spec.map (CommRingCat.ofHom φ))),
                  (c φ hsq).inv =
                    (DerivedCategory.Q.map (Θ φ hsq) ≫
                      (alternatingCechIsoDerivedGlobalSectionsOverBase (supportSnd G g ≫ f')
                        (fun j => supportFst G g ⁻¹ᵁ U j) (top_eq_iSup_preimage _ U hU)
                        ((Scheme.Modules.pullback (supportFst G g)).obj (supportModule G))
                        (iInf_preimage_isAffineOpen φ (isPullback_support G g f φ hsq) U
                          hUaff)).hom) ≫
                      (supportComparisonIso G g f').hom) ∧
              (∀ {R' R'' : Type u} [CommRing R'] [CommRing R''] (φ : R →+* R') (ψ : R' →+* R'')
                  {X' X'' : Scheme.{u}} {f' : X' ⟶ Spec (.of R')} {f'' : X'' ⟶ Spec (.of R'')}
                  {g : X' ⟶ X} {g' : X'' ⟶ X'}
                  (hsq : IsPullback g f' f (Spec.map (CommRingCat.ofHom φ)))
                  (hsq' : IsPullback g' f'' f' (Spec.map (CommRingCat.ofHom ψ))),
                  haveI : IsSeparated (supportSnd G g ≫ f') :=
                    isSeparated_of_isPullback φ (isPullback_support G g f φ hsq)
                  ((ModuleCat.extendScalars.{u, u, u} ψ).mapHomologicalComplex
                          (ComplexShape.up ℤ)).map (Θ φ hsq) ≫
                      (baseAlternatingCechComplexBaseChangeIso ψ
                          (isPullback_supportTower G g g' ψ hsq')
                          ((Scheme.Modules.pullback (supportFst G g)).obj (supportModule G))
                          (fun j => supportFst G g ⁻¹ᵁ U j) (top_eq_iSup_preimage _ U hU)
                          (isAffineOpen_preimage φ (isPullback_support G g f φ hsq) U
                            hUaff)).hom ≫
                      (baseAlternatingCechComplexMapIso (supportSnd G (g' ≫ g) ≫ f'')
                        (fun j => (supportTowerMap G g g' ≫ supportFst G g) ⁻¹ᵁ U j)
                        (top_eq_iSup_preimage _ U hU)
                        ((Scheme.Modules.pullbackComp (supportTowerMap G g g')
                          (supportFst G g)).app (supportModule G))).hom ≫
                      (cechCongrIso (supportModule G) U hU (supportTowerMap_fst G g g')).hom =
                    (extendScalarsComplexCompIso φ ψ).hom.app M ≫
                      Θ (ψ.comp φ) (Stacks.Cech.isPullback_comp_specMap φ ψ f f' f'' g g' hsq
                        hsq'))

Tag 0CSC, a lemma

Tag 0CSC in the Stacks Project.

AlgebraicGeometry.isPseudoCoherent_derivedPushforward_tensor_and_isIso_tensorFlatBaseChangeMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/TensorPseudoCoherentPushforward.lean, line 368.

[Stacks, Tag 0CSC]. Let f : X ⟶ S be a morphism of schemes of finite presentation, let E be a pseudo-coherent object of D(𝒪_X) and let 𝒢^• be a bounded above complex of finitely presented 𝒪_X-modules, flat over S, with support proper over S. Then K = Rf_*(E ⊗^L_{𝒪_X} 𝒢^•) is a pseudo-coherent object of D(𝒪_S), and its formation commutes with arbitrary base change: for every cartesian square the canonical map Lg^*Rf_*(E ⊗^L 𝒢^•) ⟶ Rf'_*(L(g')^*E ⊗^L (g')^*𝒢^•) of AlgebraicGeometry.tensorFlatBaseChangeMap is an isomorphism.

Support proper over S means that a single closed subset of X proper over S contains the support of every term of 𝒢^•.

theorem isPseudoCoherent_derivedPushforward_tensor_and_isIso_tensorFlatBaseChangeMap
    (hf : FinitePresentation f)
    (E : DerivedCategory X.Modules) (hE : RingedSpace.IsPseudoCoherent (X := X.toRingedSpace) E)
    (G : CochainComplex X.Modules ℤ) (hGminus : CochainComplex.minus X.Modules G)
    (hfp : ∀ i : ℤ, (G.X i).IsFinitePresentation)
    (hflat : ∀ i : ℤ, IsFlatOver f.toLRSHom.toShHom (G.X i))
    (hsupp : letI : LocallyOfFinitePresentation f := hf.locallyOfFinitePresentation
      ∃ Z : Closeds X, IsProperOver f Z ∧ ∀ i : ℤ, SheafOfModules.supp (G.X i) ⊆ (Z : Set X)) :
    RingedSpace.IsPseudoCoherent (X := S.toRingedSpace)
        ((derivedPushforward f.toLRSHom.toShHom).obj
          (((derivedTensorProductFunctor X.sheaf).obj E).obj (DerivedCategory.Q.obj G))) ∧
      ∀ {X' S' : Scheme.{u}} (g : S' ⟶ S) (f' : X' ⟶ S') (g' : X' ⟶ X)
        (hsq : IsPullback g' f' f g),
        IsIso (tensorFlatBaseChangeMap f g f' g' (comp_toShHom_of_comm hsq.w) E G)

Tag 0B91, a lemma

Tag 0B91 in the Stacks Project.

AlgebraicGeometry.ProperFlatFibreEulerCharacteristic.perfectDerivedPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ProperFlatPerfection/Assembly.lean, line 95. The attribute's comment: “clause (2), the perfection half: for f proper of finite presentation and a module of finite presentation flat over S, Rf_*F is a perfect object of D(O_S), over an arbitrary base. Proved by Noetherian approximation of (f, F), the Noetherian case, base change and stability of perfection under derived pullback; nothing is granted”. References: SGA 6 IV (3.3.2), “3.3.2.3, special case”.

Let f : X ⟶ S be a proper morphism of finite presentation and ℱ an 𝒪_X-module of finite presentation, flat over S. Then Rf_*ℱ is a perfect object of D(𝒪_S).

theorem perfectDerivedPushforward : PerfectDerivedPushforward.{u}

AlgebraicGeometry.ProperFlatBaseChange.isIso_derivedBaseChangeMap_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ProperFlatPushforwardBaseChangeCanonical.lean, line 174. The attribute's comment: “clause (1), the base-change half only: for f flat (and quasi-compact and quasi-separated, which a proper morphism of finite presentation is) and E perfect, the canonical map Lg^Rf_E --> Rf'_L(g')^E of Tag 08HY is an isomorphism for every cartesian square. Nothing is granted. The perfection half of clause (1) is not proved”.

Let f : X ⟶ S be flat, proper and of finite presentation and let E be a perfect object of D(𝒪_X). For every cartesian square, the formation of Rf_*E commutes with base change: the canonical map Lg^*Rf_*E ⟶ Rf'_*L(g')^*E of [Stacks, Tag 08HY] is an isomorphism.

Only quasi-compactness and quasi-separatedness of f are used, besides flatness, so the statement is made under those; a proper morphism of finite presentation has both. That Rf_*E is perfect is not stated here.

theorem isIso_derivedBaseChangeMap_of_isPerfect (hsq : IsPullback g' f' f g) [QuasiCompact f]
    [QuasiSeparated f] [Flat f] (E : DerivedCategory X.Modules)
    (hE : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace) E) :
    IsIso (derivedBaseChangeMap g'.toLRSHom.toShHom f'.toLRSHom.toShHom f.toLRSHom.toShHom
      g.toLRSHom.toShHom (comp_toShHom_of_comm hsq.w) E)

AlgebraicGeometry.ProperFlatBaseChange.isIso_derivedBaseChangeComp_singleDegree_of_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ProperFlatPushforwardBaseChangeCanonical.lean, line 197. The attribute's comment: “clause (2), the base-change half only: for f quasi-compact and quasi-separated (which a proper morphism of finite presentation is) and G of finite presentation and flat over S, the canonical map Lg^Rf_G --> Rf'_L(g')^G --> Rf'_(g')^G (Tag 08HY followed by the derived-to-ordinary comparison) is an isomorphism for every cartesian square. Nothing is granted. The perfection half of clause (2) is perfectDerivedPushforward”.

Let f : X ⟶ S be proper of finite presentation and let 𝒢 be an 𝒪_X-module of finite presentation, flat over S. For every cartesian square, the formation of Rf_*𝒢 commutes with base change: the canonical map Lg^*Rf_*𝒢 ⟶ Rf'_*L(g')^*𝒢 ⟶ Rf'_*(g')^*𝒢 — the map of [Stacks, Tag 08HY] followed by Rf'_* of the derived-to-ordinary comparison, derivedBaseChangeComp — is an isomorphism.

Only quasi-compactness and quasi-separatedness of f are used, so the statement is made under those. That Rf_*𝒢 is perfect is AlgebraicGeometry.ProperFlatFibreEulerCharacteristic.perfectDerivedPushforward.

theorem isIso_derivedBaseChangeComp_singleDegree_of_isFinitePresentation
    (hsq : IsPullback g' f' f g) [QuasiCompact f] [QuasiSeparated f] (G : X.Modules)
    [G.IsFinitePresentation] (hGflat : IsFlatOver f.toLRSHom.toShHom G) :
    IsIso (derivedBaseChangeComp f g f' g' hsq.w (DerivedCategory.Q.obj (singleDegreeComplex G))
      (DerivedCategory.Q.obj ((pullbackComplex g'.toLRSHom.toShHom).obj (singleDegreeComplex G)))
      ((derivedPullbackNatTrans g'.toLRSHom.toShHom).app (singleDegreeComplex G)))

AlgebraicGeometry.isPerfect_derivedPushforward_and_isIso_derivedBaseChangeMap_of_flat_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ProperFlatPushforwardPerfect.lean, line 297. The attribute's comment: “clause (1) in full: perfectness of Rf_E, and invertibility of the canonical base change map Lg^Rf_E --> Rf'_L(g')^*E of Tag 08HY for every cartesian square, which is what 'its formation commutes with arbitrary base change' means; finite presentation of the proper f is spelled LocallyOfFinitePresentation, the quasi-compactness and quasi-separation it adds being part of properness”. References: SGA 6 IV (3.1.1), “special case”.

[Stacks, Tag 0B91] (1). Let f : X ⟶ S be a flat proper morphism of finite presentation and let E be a perfect object of D(𝒪_X). Then Rf_*E is a perfect object of D(𝒪_S), and its formation commutes with arbitrary base change: for every cartesian square

X' --g'--> X
|          |
f'         f
v          v
S' --g---> S

the canonical base change map Lg^*Rf_*E ⟶ Rf'_*L(g')^*E of [Stacks, Tag 08HY] is an isomorphism.

Perfectness is isPerfect_derivedPushforward_of_flat_of_isProper. For base change, f is flat, so X and S' are Tor independent over S, and E has quasi-coherent cohomology, so the canonical map is invertible by [Stacks, Tag 08IB].

theorem isPerfect_derivedPushforward_and_isIso_derivedBaseChangeMap_of_flat_of_isProper
    {X S : Scheme.{u}} (f : X ⟶ S) [Flat f] [IsProper f] [LocallyOfFinitePresentation f]
    (E : DerivedCategory X.Modules) (hE : IsPerfect (X := X.toRingedSpace) E) :
    IsPerfect (X := S.toRingedSpace) ((derivedPushforwardModules f).obj E) ∧
      ∀ {S' X' : Scheme.{u}} (g : S' ⟶ S) (f' : X' ⟶ S') (g' : X' ⟶ X)
        (sq : IsPullback g' f' f g),
        IsIso (Stacks.Cohomology.DerivedBaseChange.derivedBaseChangeMap g'.toLRSHom.toShHom
          f'.toLRSHom.toShHom f.toLRSHom.toShHom g.toLRSHom.toShHom
          (comp_toShHom_of_comm sq.w) E)

AlgebraicGeometry.ProperFlatBaseChange.isPerfect_derivedPushforward_and_isIso_baseChange_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ProperPushforwardPerfectAndBaseChange.lean, line 90. The attribute's comment: “both clauses in full: for f proper of finite presentation, (1) for f flat and E perfect, Rf_E is perfect and the canonical map Lg^Rf_E --> Rf'_L(g')^E of Tag 08HY is an isomorphism for every cartesian square; (2) for G of finite presentation and flat over S, Rf_G is perfect and the canonical map Lg^Rf_G --> Rf'_(g')^G is an isomorphism for every cartesian square”.

[Stacks, Tag 0B91]. Let f : X ⟶ S be a proper morphism of schemes of finite presentation.

1. Let E ∈ D(𝒪_X) be perfect and f flat. Then Rf_*E is a perfect object of D(𝒪_S), and its formation commutes with arbitrary base change: for every cartesian square X' = X ×_S S' the canonical map Lg^*Rf_*E ⟶ Rf'_*L(g')^*E of [Stacks, Tag 08HY] is an isomorphism.
2. Let 𝒢 be an 𝒪_X-module of finite presentation, flat over S. Then Rf_*𝒢 is a perfect object of D(𝒪_S), and its formation commutes with arbitrary base change: for every cartesian square the canonical map Lg^*Rf_*𝒢 ⟶ Rf'_*L(g')^*𝒢 ⟶ Rf'_*(g')^*𝒢 (the map of [Stacks, Tag 08HY] followed by Rf'_* of the derived-to-ordinary comparison) is an isomorphism.

Here 𝒢 is placed in degree zero as the complex singleDegreeComplex 𝒢, at which the base-change map of clause (2) is written.

theorem isPerfect_derivedPushforward_and_isIso_baseChange_of_isProper {X S : Scheme.{u}}
    (f : X ⟶ S) (hf : FinitePresentation f) (hproper : IsProper f) :
    (Flat f → ∀ E : DerivedCategory X.Modules, RingedSpace.IsPerfect (X := X.toRingedSpace) E →
      RingedSpace.IsPerfect (X := S.toRingedSpace)
          ((derivedPushforward f.toLRSHom.toShHom).obj E) ∧
        ∀ {X' S' : Scheme.{u}} (g : S' ⟶ S) (f' : X' ⟶ S') (g' : X' ⟶ X)
          (hsq : IsPullback g' f' f g),
          IsIso (derivedBaseChangeMap g'.toLRSHom.toShHom f'.toLRSHom.toShHom f.toLRSHom.toShHom
            g.toLRSHom.toShHom (comp_toShHom_of_comm hsq.w) E)) ∧
    (∀ G : X.Modules, G.IsFinitePresentation → IsFlatOver f.toLRSHom.toShHom G →
      RingedSpace.IsPerfect (X := S.toRingedSpace)
          ((derivedPushforward f.toLRSHom.toShHom).obj
            (DerivedCategory.Q.obj (singleDegreeComplex G))) ∧
        ∀ {X' S' : Scheme.{u}} (g : S' ⟶ S) (f' : X' ⟶ S') (g' : X' ⟶ X)
          (hsq : IsPullback g' f' f g),
          IsIso (derivedBaseChangeComp f g f' g' hsq.w
            (DerivedCategory.Q.obj (singleDegreeComplex G))
            (DerivedCategory.Q.obj ((pullbackComplex g'.toLRSHom.toShHom).obj
              (singleDegreeComplex G)))
            ((derivedPullbackNatTrans g'.toLRSHom.toShHom).app (singleDegreeComplex G))))

Tag 0CSD, a lemma

Tag 0CSD in the Stacks Project.

AlgebraicGeometry.isPseudoCoherent_derivedPushforward_and_isIso_derivedBaseChangeMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ProperFlatPushforwardPseudoCoherent.lean, line 77.

[Stacks, Tag 0CSD]. Let f : X ⟶ S be a flat proper morphism of schemes of finite presentation and let E ∈ D(𝒪_X) be pseudo-coherent. Then Rf_*E is a pseudo-coherent object of D(𝒪_S) and its formation commutes with arbitrary base change: for every cartesian square X' = X ×_S S' the base change map Lg^*Rf_*E ⟶ Rf'_*L(g')^*E of [Stacks, Tag 08HY] is an isomorphism.

theorem isPseudoCoherent_derivedPushforward_and_isIso_derivedBaseChangeMap [Flat f] [IsProper f]
    [LocallyOfFinitePresentation f]
    (E : DerivedCategory X.Modules) (hE : RingedSpace.IsPseudoCoherent (X := X.toRingedSpace) E) :
    RingedSpace.IsPseudoCoherent (X := S.toRingedSpace)
        ((derivedPushforward f.toLRSHom.toShHom).obj E) ∧
      ∀ {X' S' : Scheme.{u}} (g : S' ⟶ S) (f' : X' ⟶ S') (g' : X' ⟶ X)
        (sq : IsPullback g' f' f g),
        IsIso (derivedBaseChangeMap g'.toLRSHom.toShHom f'.toLRSHom.toShHom f.toLRSHom.toShHom
          g.toLRSHom.toShHom (comp_toShHom_of_comm sq.w) E)

Tag 0D2Q, a lemma

Tag 0D2Q in the Stacks Project.

Stacks.ProperFlatPullbackLimit.bijective_comp_singleFunctor_map_limitPost, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ProperFlatPullbackInverseLimit.lean, line 226. The attribute's comment: “the canonical map O_X ⊗_R lim M_n --> lim O_X ⊗_R M_n induces bijections Hom(E, source) --> Hom(E, target) for every E in D_QCoh(O_X), which is what the source's proof says the statement means; at every model of the derived category”.

Stacks Project, Tag 0D2Q, in the form the source's proof unfolds it. Let R be a ring, f : X ⟶ Spec R proper, flat and of finite presentation, and (Mₙ) an inverse system of R-modules with surjective transition maps. Then for every object E of D_QCoh(𝒪_X) the canonical map O_X ⊗_R (lim Mₙ) ⟶ lim (O_X ⊗_R Mₙ) induces a bijection

Hom(E, O_X ⊗_R (lim Mₙ)) ⟶ Hom(E, lim O_X ⊗_R Mₙ).

Here O_X ⊗_R M is f^*M^~, both modules are placed in degree zero, the limit on the right is the limit in 𝒪_X-modules and the canonical map is limit.post. The statement is made at an arbitrary model of the derived category of 𝒪_X-modules.

theorem bijective_comp_singleFunctor_map_limitPost (R : CommRingCat.{u}) {X : Scheme.{u}}
    (f : X ⟶ Spec R) [IsProper f] [Flat f] [LocallyOfFinitePresentation f]
    (M : ℕᵒᵖ ⥤ ModuleCat.{u} R) (hsurj : ∀ n : ℕ, Epi (M.map (homOfLE (Nat.le_succ n)).op))
    [HasDerivedCategory.{w} X.Modules] (E : DerivedCategory X.Modules)
    (hE : DerivedCategoryB.derivedCategoryB (A := X.Modules)
      (SheafOfModules.isQuasicoherent X.ringCatSheaf) E) :
    Function.Bijective (fun φ : E ⟶ (DerivedCategory.singleFunctor X.Modules 0).obj
        ((tilde.functor R ⋙ Scheme.Modules.pullback f).obj (limit M)) =>
      φ ≫ (DerivedCategory.singleFunctor X.Modules 0).map
        (limit.post M (tilde.functor R ⋙ Scheme.Modules.pullback f)))

Stacks.ProperFlatPullbackLimit.isIso_homEquiv_singleFunctor_map_limitPost, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ProperFlatPullbackInverseLimit.lean, line 266.

Stacks Project, Tag 0D2Q. Let R be a ring, f : X ⟶ Spec R proper, flat and of finite presentation, and (Mₙ) an inverse system of R-modules with surjective transition maps. Then the canonical map O_X ⊗_R (lim Mₙ) ⟶ lim (O_X ⊗_R Mₙ) induces an isomorphism from the source to DQ_X applied to the target: for every right adjoint DQ of the inclusion D_QCoh(𝒪_X) ⥤ D(𝒪_X) (one exists by [Stacks, Tag 0CR0]), the morphism O_X ⊗_R (lim Mₙ) ⟶ DQ(lim O_X ⊗_R Mₙ) adjoint to the canonical map is an isomorphism.

theorem isIso_homEquiv_singleFunctor_map_limitPost (R : CommRingCat.{u}) {X : Scheme.{u}}
    (f : X ⟶ Spec R) [IsProper f] [Flat f] [LocallyOfFinitePresentation f]
    (M : ℕᵒᵖ ⥤ ModuleCat.{u} R) (hsurj : ∀ n : ℕ, Epi (M.map (homOfLE (Nat.le_succ n)).op))
    {DQ : DerivedCategory X.Modules ⥤ Stacks.Duality.quasiCoherentDerivedCategory X}
    (adj : Stacks.Duality.Coherator.quasiCoherentι X ⊣ DQ) :
    IsIso (adj.homEquiv (pullbackTildeLimitQCoh f M) _
      ((DerivedCategory.singleFunctor X.Modules 0).map
        (limit.post M (tilde.functor R ⋙ Scheme.Modules.pullback f))))

Tag 0A1J, a lemma

Tag 0A1J in the Stacks Project.

AlgebraicGeometry.isIso_sheafHomFlatBaseChangeMap_of_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BaseChange/SheafHomFinitelyPresentedPushforwardBaseChange.lean, line 166. The attribute's comment: “the base-change half of the conclusion ONLY, for the canonical map sheafHomFlatBaseChangeMap of Stacks 08IE, with the ORDINARY pullback (g')^*𝒢^• on the right as the source's boldface demands. The perfection half -- that K is a perfect object of D(O_S) -- is NOT proved and is not stated: the library's result for it is Tag 0DJR, which assumes a Noetherian base, a locally-of-finite-type f and coherent terms, none of which Tag 0A1J grants, and the source closes that gap by a limit descent (Tags 01ZM, 01ZR, 05LY, 081G, 09RF) to a Noetherian stage that is not assembled in this library. Of what Tag 08IE case (1) asks beyond Tag 0A1J's hypotheses, all four are discharged here: quasi-compactness and quasi-separatedness of f from Tag 01TP part (3), commutativity of the square from the cartesian square, boundedness above of the complex from its two-sided boundedness, and quasi-coherence of its terms from their finite presentation by Tag 01BW. The perfectness of E is the source's own hypothesis, stated at the predicate Tag 08IE is written at, not a weaker stand-in. The three steps of the source proof of Tag 08IE are not assumed: Tag 08IE case (1) is proved outright in this library. What remains among this statement's own conditions is hK and hK', the quasi-coherence of the cohomology of the two derived internal homs, which Tag 0DJ9 asks of its complexes and which this library has at a spelling of the derived internal hom that does not line up with the one the comparison map is written at. The proper-support hypothesis on the complex is carried in the bundle and is not used by this half, the source's base-change argument not appealing to it”.

[Stacks, Tag 0A1J], the base-change half of the conclusion. Let f : X ⟶ S be a morphism of schemes of finite presentation, let E be a perfect object of D(𝒪_X) and let 𝒢^• be a bounded complex of finitely presented 𝒪_X-modules, flat over S, with support proper over S. For every cartesian base-change square the canonical map

Lg^*Rf_*R𝓗om_{𝒪_X}(E, 𝒢^•) ⟶ Rf'_*R𝓗om_{𝒪_{X'}}(L(g')^*E, (g')^*𝒢^•)

of AlgebraicGeometry.sheafHomFlatBaseChangeMap is an isomorphism — note the ordinary pullback of 𝒢^• on the right, as the source's boldface demands.

The perfection half of [Stacks, Tag 0A1J] is not proved; the implementation notes of this file say what it would need.

The proof is the reduction the source performs: finite presentation of f supplies the quasi-compactness and quasi-separatedness that case (1) of [Stacks, Tag 08IE] asks for, and the four conditions of AlgebraicGeometry.FlatProperSupportFinitelyPresented supply boundedness above of 𝒢^• and quasi-coherence and relative flatness of its terms. The source's proper-support hypothesis on 𝒢^• is part of that bundle and is not used by this half: the base-change argument does not appeal to it, and it is kept so that the hypothesis bundle is the one [Stacks, Tag 0A1J] states.

public theorem isIso_sheafHomFlatBaseChangeMap_of_finitePresentation
    {X X' S S' : Scheme.{u}} (f : X ⟶ S) (g : S' ⟶ S) (f' : X' ⟶ S') (g' : X' ⟶ X)
    (hsq : IsPullback g' f' f g)
    (sq : g'.toLRSHom.toShHom ≫ f.toLRSHom.toShHom =
      f'.toLRSHom.toShHom ≫ g.toLRSHom.toShHom)
    (hf : FinitePresentation f)
    (E : DerivedCategory X.Modules)
    (hEperfect : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace) E)
    (G : CochainComplex X.Modules ℤ)
    (hG : letI : LocallyOfFinitePresentation f := hf.locallyOfFinitePresentation
      FlatProperSupportFinitelyPresented f G)
    (hK : ∀ n : ℤ, ((DerivedCategory.homologyFunctor X.Modules n).obj
      (((derivedSheafHom X.sheaf).obj (op E)).obj
        (DerivedCategory.Q.obj G))).IsQuasicoherent)
    (hK' : ∀ n : ℤ, ((DerivedCategory.homologyFunctor X'.Modules n).obj
      (((derivedSheafHom X'.sheaf).obj
          (op ((derivedPullback g'.toLRSHom.toShHom).obj E))).obj
        (DerivedCategory.Q.obj
          ((pullbackComplex g'.toLRSHom.toShHom).obj G)))).IsQuasicoherent) :
    IsIso (sheafHomFlatBaseChangeMap f g f' g' sq E G)

AlgebraicGeometry.isPerfect_derivedPushforward_derivedSheafHom_and_isIso_sheafHomFlatBaseChangeMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SheafHomFinitelyPresentedPerfectBaseChange.lean, line 68.

[Stacks, Tag 0A1J]. Let f : X ⟶ S be a morphism of schemes of finite presentation, let E be a perfect object of D(𝒪_X) and let 𝒢^• be a bounded complex of finitely presented 𝒪_X-modules, flat over S, with support proper over S. Then K = Rf_*R𝓗om_{𝒪_X}(E, 𝒢^•) is a perfect object of D(𝒪_S), and its formation commutes with arbitrary base change: for every cartesian square the canonical map Lg^*Rf_*R𝓗om_{𝒪_X}(E, 𝒢^•) ⟶ Rf'_*R𝓗om_{𝒪_{X'}}(L(g')^*E, (g')^*𝒢^•) of AlgebraicGeometry.sheafHomFlatBaseChangeMap is an isomorphism.

theorem isPerfect_derivedPushforward_derivedSheafHom_and_isIso_sheafHomFlatBaseChangeMap
    {X S : Scheme.{u}} (f : X ⟶ S) (hf : FinitePresentation f) (E : DerivedCategory X.Modules)
    (hE : RingedSpace.IsPerfect (X := X.toRingedSpace) E) (G : CochainComplex X.Modules ℤ)
    (hG : letI : LocallyOfFinitePresentation f := hf.locallyOfFinitePresentation
      FlatProperSupportFinitelyPresented f G) :
    RingedSpace.IsPerfect (X := S.toRingedSpace)
        ((derivedPushforward f.toLRSHom.toShHom).obj
          (((derivedSheafHom X.sheaf).obj (op E)).obj (DerivedCategory.Q.obj G))) ∧
      ∀ {X' S' : Scheme.{u}} (g : S' ⟶ S) (f' : X' ⟶ S') (g' : X' ⟶ X)
        (hsq : IsPullback g' f' f g),
        IsIso (sheafHomFlatBaseChangeMap f g f' g' (comp_toShHom_of_comm hsq.w) E G)

Sources

• Section 36.30, Tag 0A1G
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.isPerfect_derivedPushforward_tensor_and_isIso_tensorFlatBaseChangeMap · Stacks.AlgebraicGeometry.FinitePresentationGlobalSectionsModel.exists_finiteProjectiveModel_of_properSupport · Stacks.AlgebraicGeometry.ProperSupportModel.exists_finiteProjectiveModel_derivedGlobalSections_functorial · AlgebraicGeometry.isPseudoCoherent_derivedPushforward_tensor_and_isIso_tensorFlatBaseChangeMap · AlgebraicGeometry.ProperFlatFibreEulerCharacteristic.perfectDerivedPushforward · AlgebraicGeometry.ProperFlatBaseChange.isIso_derivedBaseChangeMap_of_isPerfect · AlgebraicGeometry.ProperFlatBaseChange.isIso_derivedBaseChangeComp_singleDegree_of_isFinitePresentation · AlgebraicGeometry.isPerfect_derivedPushforward_and_isIso_derivedBaseChangeMap_of_flat_of_isProper

Section36.31 Perfect complexes#

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

Tag 0BDI, a lemma

Tag 0BDI in the Stacks Project.

AlgebraicGeometry.DerivedFibreBetti.isPseudoCoherent_derivedPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/DerivedFibreBettiBaseChange.lean, line 229. The attribute's comment: “base_change”.

Tag 0BDI, base change: the derived pullback of a pseudo-coherent object is pseudo-coherent. This is what makes the derived-fibre Betti function of Lf^* E available from the pseudo-coherence of E alone.

A single complex has to work for every m, so the representative is chosen once — DerivedCategory.Q.objPreimage — and Tag 09U7 is applied in each degree, its m-specific representative being transported onto that one choice by Tag 08CC part (2).

public theorem isPseudoCoherent_derivedPullback
    (E : DerivedCategory X.Modules)
    (hE : RingedSpace.IsPseudoCoherent (X := X.toRingedSpace) E) :
    RingedSpace.IsPseudoCoherent (X := Y.toRingedSpace)
      ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback f.toLRSHom.toShHom).obj E)

AlgebraicGeometry.DerivedFibreBetti.derivedFiberBetti_derivedPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/DerivedFibreBettiBaseChange.lean, line 256. The attribute's comment: “base_change”.

Tag 0BDI, base change: the derived-fibre Betti function commutes with base change. For a morphism of schemes f : Y ⟶ X the i-th derived-fibre Betti function of Lf^* E is the pullback along f of the i-th derived-fibre Betti function of E.

The pseudo-coherence of Lf^* E that the left-hand side needs is supplied by isPseudoCoherent_derivedPullback, so E's own pseudo-coherence is the only hypothesis. The function does not use its pseudo-coherence argument, so nothing is lost by fixing it: the underlying dimension equality is finrank_residueFibre_eq, which has no pseudo-coherence hypothesis at all.

public theorem derivedFiberBetti_derivedPullback
    (E : DerivedCategory X.Modules)
    (hE : RingedSpace.IsPseudoCoherent (X := X.toRingedSpace) E)
    (i : ℤ) :
    derivedFiberBetti Y ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
      f.toLRSHom.toShHom).obj E)
        (isPseudoCoherent_derivedPullback f E hE) i =
      derivedFiberBetti X E hE i ∘ f.base

AlgebraicGeometry.DerivedFibreBetti.isLocallyConstructible_derivedFiberBetti_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/DerivedFibreBettiConstructible.lean, line 104. The attribute's comment: “part (3): for E a pseudo-coherent object of D(O_X) on a scheme X, the level sets of the functions beta_i are locally constructible in X. beta_i is AlgebraicGeometry.DerivedFibreBetti.derivedFiberBetti, the dimension over the residue field of the degree-i cohomology of the derived fibre read through global sections on Spec kappa(x), the level set at n is the preimage of the singleton n, and pseudo-coherence of E is the only hypothesis. The affine case is proved, not assumed: it is StacksDraft.Perfect.isConstructible_fibreBetti_preimage, which runs the source's argument through the rank loci of a bounded-above finite free model -- over a field the ideal of r-by-r minors of a matrix is the unit ideal exactly when r is at most its rank (StacksDraft.MinorRank.minorIdeal_eq_top_iff_le_rank), so the locus where the rank at p is at least r is the complement of the zero locus of a finitely generated ideal and hence retrocompact, which is what semi-continuity does not give”.

[Stacks, Tag 0BDI], part (3): the level sets of the derived-fibre Betti functions are locally constructible. Let X be a scheme and let E be a pseudo-coherent object of D(𝒪_X). For every i and every n the set of points x with dim_{κ(x)} H^i(Li_x^* E) = n is locally constructible in X.

By [Stacks, Tag 054C] it is enough to check that the restriction to each affine open U is constructible. The open immersion hU.fromSpec : Spec Γ(X, U) ⟶ X is a homeomorphism onto the subspace U, so that restriction is constructible exactly when its preimage along fromSpec is; and that preimage is a level set of the derived-fibre Betti function of the derived pullback of E, by part (1) of the tag, to which the affine case applies.

public theorem isLocallyConstructible_derivedFiberBetti_preimage (X : Scheme.{u})
    (E : DerivedCategory X.Modules)
    (hE : RingedSpace.IsPseudoCoherent (X := X.toRingedSpace) E) (i : ℤ) (n : ℕ) :
    IsLocallyConstructible (derivedFiberBetti X E hE i ⁻¹' {n})

AlgebraicGeometry.DerivedFibreBetti.upperSemicontinuous_derivedFiberBetti, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/DerivedFibreBettiSemicontinuity.lean, line 84. The attribute's comment: “part (2): for E a pseudo-coherent object of D(O_X) on a scheme X, the function beta_i sending x to dim_{kappa(x)} H^i(Li_x^* E) is upper semi-continuous. beta_i is AlgebraicGeometry.DerivedFibreBetti.derivedFiberBetti, the dimension over the residue field of the degree-i cohomology of the derived fibre read through global sections on Spec kappa(x), and pseudo-coherence of E is the only hypothesis”.

[Stacks, Tag 0BDI], part (2): the derived-fibre Betti functions are upper semi-continuous. Let X be a scheme and let E be a pseudo-coherent object of D(𝒪_X). For every i the function x ↦ dim_{κ(x)} H^i(Li_x^* E) is upper semi-continuous on X.

Every point lies in an affine open U, and U is the image of the open immersion hU.fromSpec : Spec Γ(X, U) ⟶ X; the derived pullback of E along it is pseudo-coherent, so the affine case applies there, and upper semi-continuity is local on the source.

public theorem upperSemicontinuous_derivedFiberBetti (X : Scheme.{u})
    (E : DerivedCategory X.Modules)
    (hE : RingedSpace.IsPseudoCoherent (X := X.toRingedSpace) E) (i : ℤ) :
    UpperSemicontinuous (derivedFiberBetti X E hE i)

Tag 0BDJ, a lemma

Tag 0BDJ in the Stacks Project.

AlgebraicGeometry.DerivedFibreBetti.isLocallyConstant_chiDerivedFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/DerivedFibreEulerCharacteristic.lean, line 348. References: EGA III (7.9.3), “more general”; SGA 6 III (5.4.1), “a) rank, scheme case”; SGA 6 III (5.5), “(i), scheme case”.

Stacks 0BDJ. The derived-fibre Euler characteristic of a perfect object of D(𝒪_X) on a scheme is locally constant.

Near any point, Tag 0BCJ represents E by a bounded complex of finite free modules on an open V; base change along the open immersion V ⟶ X (Tag 0BDI) identifies the Euler characteristic on V with the restriction of the one on X, and on V it is the constant ∑ (-1)^i rank(P^i).

public theorem isLocallyConstant_chiDerivedFibre (X : Scheme.{u})
    (E : DerivedCategory X.Modules)
    (hE : RingedSpace.IsPerfect.{u, u + 1} (X := X.toRingedSpace) E) :
    IsLocallyConstant (chiDerivedFibre X E (isPseudoCoherent_of_isPerfect E hE))

Tag 0BDK, a lemma

Tag 0BDK in the Stacks Project.

AlgebraicGeometry.Scheme.Modules.nonempty_iso_singleFunctor_restrict_iff_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SingleDegreeRankOpen.lean, line 305. The attribute's comment: “the open description”.

The open subscheme of [stacks 0BDK] is characterised by the first description. An open of X is contained in singleDegreeRankOpen exactly when the restriction of E to it is isomorphic to a finite locally free module of rank r placed in degree i; so singleDegreeRankOpen is the largest open subscheme on which E has that shape.

theorem nonempty_iso_singleFunctor_restrict_iff_le (V : X.Opens) :
    (∃ M : V.toScheme.Modules,
        AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} M r ∧
          Nonempty ((restrictFunctor V.ι).mapDerivedCategory.obj E ≅
            (DerivedCategory.singleFunctor V.toScheme.Modules i).obj M)) ↔
      V ≤ singleDegreeRankOpen E i r

AlgebraicGeometry.Scheme.Modules.isZero_homology_singleDegreeRankOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SingleDegreeRankOpen.lean, line 316. The attribute's comment: “the open description”.

The cohomology of E vanishes outside degree i on the open subscheme of [stacks 0BDK].

theorem isZero_homology_singleDegreeRankOpen (j : ℤ) (hj : j ≠ i) :
    IsZero ((DerivedCategory.homologyFunctor
        (singleDegreeRankOpen E i r).toScheme.Modules j).obj
      ((restrictFunctor (singleDegreeRankOpen E i r).ι).mapDerivedCategory.obj E))

AlgebraicGeometry.Scheme.Modules.nonempty_iso_singleFunctor_restrict_singleDegreeRankOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SingleDegreeRankOpen.lean, line 327. The attribute's comment: “the open description”.

On the open subscheme of [stacks 0BDK] the derived module E is its own degree-i cohomology sheaf placed in degree i. This is the first half of description (1) of the tag.

theorem nonempty_iso_singleFunctor_restrict_singleDegreeRankOpen :
    Nonempty ((restrictFunctor (singleDegreeRankOpen E i r).ι).mapDerivedCategory.obj E ≅
      (DerivedCategory.singleFunctor (singleDegreeRankOpen E i r).toScheme.Modules i).obj
        ((DerivedCategory.homologyFunctor
            (singleDegreeRankOpen E i r).toScheme.Modules i).obj
          ((restrictFunctor (singleDegreeRankOpen E i r).ι).mapDerivedCategory.obj E)))

AlgebraicGeometry.Scheme.Modules.isFiniteLocallyFreeOfRank_homology_singleDegreeRankOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SingleDegreeRankOpen.lean, line 339. The attribute's comment: “the open description”.

On the open subscheme of [stacks 0BDK] the degree-i cohomology sheaf of E is finite locally free of rank r. This is the second half of description (1) of the tag.

theorem isFiniteLocallyFreeOfRank_homology_singleDegreeRankOpen :
    AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
      ((DerivedCategory.homologyFunctor
          (singleDegreeRankOpen E i r).toScheme.Modules i).obj
        ((restrictFunctor (singleDegreeRankOpen E i r).ι).mapDerivedCategory.obj E)) r

AlgebraicGeometry.Scheme.Modules.factorsThrough_singleDegreeRankOpen_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SingleDegreeRankOpen.lean, line 354. The attribute's comment: “the universal property for open immersions, restriction for the derived pullback”.

The universal property of the open subscheme of [stacks 0BDK], for open immersions. An open immersion f : Y ⟶ X factors through singleDegreeRankOpen exactly when the restriction of E along f is isomorphic to a finite locally free module of rank r placed in degree i.

This is description (2) of the tag for an open immersion, with the exact restriction functor along f in place of the derived pullback; the tag states it for an arbitrary morphism and the derived pullback.

theorem factorsThrough_singleDegreeRankOpen_iff {Y : Scheme.{u}} (f : Y ⟶ X)
    [IsOpenImmersion f] :
    (∃ g : Y ⟶ (singleDegreeRankOpen E i r).toScheme,
        g ≫ (singleDegreeRankOpen E i r).ι = f) ↔
      ∃ M : Y.Modules,
        AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} M r ∧
          Nonempty ((restrictFunctor f).mapDerivedCategory.obj E ≅
            (DerivedCategory.singleFunctor Y.Modules i).obj M)

AlgebraicGeometry.Scheme.Modules.existsUnique_opens_singleDegreeRank_int, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SingleDegreeRankOpenInt.lean, line 111. The attribute's comment: “THE WHOLE TAG, at the source's INTEGER rank: the existence of an open subscheme satisfying description (1), both of its clauses, and description (2) in both directions for an ARBITRARY morphism of schemes and the derived pullback Lf^*E, together with the UNIQUENESS that makes the two descriptions a characterisation. The only premise is the source's own, that E be perfect. The rank clause is read at each point, as the source states it; for a non-negative rank the witness is AlgebraicGeometry.Scheme.Modules.singleDegreeRankOpen and the statement is AlgebraicGeometry.Scheme.Modules.existsUnique_opens_singleDegreeRank, and for a negative rank the witness is the empty open subscheme”.

[Stacks, Tag 0BDK]. Let X be a scheme, let E ∈ D(𝒪_X) be perfect and let i, r be integers. There is a unique open subscheme U ⊆ X characterised by the following:

1. E|_U ≅ H^i(E|_U)[-i] and H^i(E|_U) is a locally free 𝒪_U-module of rank r,
2. a morphism f : Y ⟶ X factors through U if and only if Lf^* E is isomorphic to a locally free module of rank r placed in degree i.

"Locally free of rank r" for an integer r is read, as the source states it, at each point: a sheaf of modules has it when every point has a neighbourhood on which the sheaf is free of rank r. For r ≥ 0 that is finite local freeness of rank r and the statement is existsUnique_opens_singleDegreeRank with its witness singleDegreeRankOpen E i r; for r < 0 the condition forces the scheme to be empty, and the open subscheme is ⊥.

theorem existsUnique_opens_singleDegreeRank_int (E : DerivedCategory X.Modules)
    (hE : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace) E)
    (i r : ℤ) :
    ∃! U : X.Opens,
      (Nonempty ((restrictFunctor U.ι).mapDerivedCategory.obj E ≅
            (DerivedCategory.singleFunctor U.toScheme.Modules i).obj
              ((DerivedCategory.homologyFunctor U.toScheme.Modules i).obj
                ((restrictFunctor U.ι).mapDerivedCategory.obj E))) ∧
          ∀ _ : U.toScheme, ∃ n : ℕ, (n : ℤ) = r ∧
            AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
              ((DerivedCategory.homologyFunctor U.toScheme.Modules i).obj
                ((restrictFunctor U.ι).mapDerivedCategory.obj E)) n) ∧
        ∀ (Y : Scheme.{u}) (f : Y ⟶ X),
          (∃ g : Y ⟶ U.toScheme, g ≫ U.ι = f) ↔
            ∃ M : Y.Modules,
              (∀ _ : Y, ∃ n : ℕ, (n : ℤ) = r ∧
                  AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} M n) ∧
                Nonempty ((derivedPullback f.toLRSHom.toShHom).obj E ≅
                  (DerivedCategory.singleFunctor Y.Modules i).obj M)

AlgebraicGeometry.Scheme.Modules.factorsThrough_singleDegreeRankOpen_iff_derivedPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SingleDegreeRankOpenUniversal.lean, line 405. The attribute's comment: “part (2): the universal property along an arbitrary morphism, rank r : N”.

Let E be a perfect object of D(𝒪_X), i an integer and r a natural number. A morphism of schemes f : Y ⟶ X factors through singleDegreeRankOpen E i r exactly when Lf^*E is isomorphic to a finite locally free 𝒪_Y-module of rank r placed in degree i.

theorem factorsThrough_singleDegreeRankOpen_iff_derivedPullback
    (hE : RingedSpace.IsPerfect.{u, u + 1} (X := X.toRingedSpace) E) {Y : Scheme.{u}}
    (f : Y ⟶ X) :
    (∃ g : Y ⟶ (singleDegreeRankOpen E i r).toScheme,
        g ≫ (singleDegreeRankOpen E i r).ι = f) ↔
      ∃ M : Y.Modules,
        AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} M r ∧
          Nonempty ((derivedPullback f.toLRSHom.toShHom).obj E ≅
            (DerivedCategory.singleFunctor Y.Modules i).obj M)

Tag 0BDL, a lemma

Tag 0BDL in the Stacks Project.

AlgebraicGeometry.BottomRankStratum.isBottomRankStratum_fittingRankStratum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/BottomRankStratum.lean, line 335. The attribute's comment: “parts (1) and (2), for E a finite type quasi-coherent module placed in degree a”.

The rank s Fitting stratum is a bottom rank s stratum for a module placed in degree a. Its structural morphism is a locally closed immersion and it represents the rank s functor of F ([stacks 05P8]), which for a module placed in degree a is the condition of being universally of bottom rank s.

This is descriptions (1) and (2) of [stacks 0BDL] for an E which is a module placed in degree a.

public theorem isBottomRankStratum_fittingRankStratum (F : X.Modules) [F.IsFiniteType]
    [F.IsQuasicoherent] (a : ℤ) (s : ℕ) :
    IsBottomRankStratum ((DerivedCategory.singleFunctor X.Modules a).obj F) a s
      (fittingRankStratum F s).hom

AlgebraicGeometry.BottomRankStratum.pullbackHomologySingleCompIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/BottomRankStratum.lean, line 371. The attribute's comment: “part (3), for E a module placed in degree a”.

H^a(L(g ∘ j)^* E) ≅ g^* H^a(Lj^* E) for E a module placed in degree a. This is part (3) of [stacks 0BDL]: a morphism factoring as Y ⟶ Z ⟶ X has its degree-a cohomology of the derived pullback the ordinary pullback along g of the one on Z.

Both sides are identified with an ordinary pullback of F by pullbackHomologySingleIso, and the two ordinary pullbacks are identified by AlgebraicGeometry.Scheme.Modules.pullbackComp, so the isomorphism is a composite of canonical maps and not merely an abstract isomorphism of locally free modules of the same rank.

public def pullbackHomologySingleCompIso (F : X.Modules) (a : ℤ) {Y Z : Scheme.{u}} (j : Z ⟶ X)
    (g : Y ⟶ Z) :
    pullbackHomology ((DerivedCategory.singleFunctor X.Modules a).obj F) a (g ≫ j) ≅
      (Scheme.Modules.pullback g).obj
        (pullbackHomology ((DerivedCategory.singleFunctor X.Modules a).obj F) a j)

AlgebraicGeometry.BottomRankStratum.factorsThrough_fittingRankStratum_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/BottomRankStratum.lean, line 388. The attribute's comment: “part (4), (a) iff (b), for E a finite type quasi-coherent module in degree a”.

A morphism factors through the rank s Fitting stratum exactly when H^a(Lf^* E) is finite locally free of rank s. This is the equivalence of (a) and (b) in part (4) of [stacks 0BDL] for E a module placed in degree a.

No bound on the derived-fibre Betti numbers is needed: the quantification over further morphisms in description (2) costs nothing for a module placed in degree a, because the ordinary pullback of a finite locally free module of rank s is again one.

public theorem factorsThrough_fittingRankStratum_iff (F : X.Modules) [F.IsFiniteType]
    [F.IsQuasicoherent] (a : ℤ) (s : ℕ) {Y : Scheme.{u}} (f : Y ⟶ X) :
    (∃ g : Y ⟶ (fittingRankStratum F s).left, g ≫ (fittingRankStratum F s).hom = f) ↔
      AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
        (pullbackHomology ((DerivedCategory.singleFunctor X.Modules a).obj F) a f) s

AlgebraicGeometry.BottomRankStratum.isBottomRankStratum_finitePresentation_fittingRankStratum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/BottomRankStratum.lean, line 405. The attribute's comment: “parts (1), (2) and finite presentation, E a finitely presented module in degree a”.

The rank s Fitting stratum of a finitely presented module is a bottom rank s stratum whose structural morphism is of finite presentation. This is descriptions (1) and (2) of [stacks 0BDL] together with its assertion that j : Z ⟶ X is of finite presentation, for E a finitely presented module placed in degree a.

The finite presentation is AlgebraicGeometry.finitePresentation_fittingRankStratum; the two halves are stated together because the tag's "moreover" is about the same j that descriptions (1) and (2) characterise.

public theorem isBottomRankStratum_finitePresentation_fittingRankStratum (F : X.Modules)
    [F.IsFinitePresentation] (a : ℤ) (s : ℕ) :
    IsBottomRankStratum ((DerivedCategory.singleFunctor X.Modules a).obj F) a s
        (@fittingRankStratum X F (SheafOfModules.instIsFiniteTypeOfIsFinitePresentation F)
          (SheafOfModules.instIsQuasicoherentOfIsFinitePresentation F) s).hom ∧
      FinitePresentation
        (@fittingRankStratum X F (SheafOfModules.instIsFiniteTypeOfIsFinitePresentation F)
          (SheafOfModules.instIsQuasicoherentOfIsFinitePresentation F) s).hom

AlgebraicGeometry.BottomRankStratum.isClosedImmersion_fittingRankStratum_of_isGeneratedByNear, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/BottomRankStratum.lean, line 443. The attribute's comment: “part (4), closedness of j, E a module in degree a, Betti bound as generation”.

When the module is generated by s sections near every point, the rank s Fitting stratum is a closed subscheme. This is the closedness assertion of part (4) of [stacks 0BDL] for E a module placed in degree a, with the hypothesis β_a ≤ s in the form it takes for such an E: β_a(x) is the dimension of the fibre of F at x, so β_a(x) ≤ s says that F needs at most s generators near x.

Under that hypothesis the s-th Fitting ideal is the unit ideal, so the open subscheme cut out of the Fitting closed subscheme of index s - 1 by the generator open of index s is the whole of it, and the structural morphism of the stratum is that closed immersion up to an isomorphism.

public theorem isClosedImmersion_fittingRankStratum_of_isGeneratedByNear (F : X.Modules)
    [F.IsFiniteType] [F.IsQuasicoherent] (s : ℕ) (hgen : ∀ x : X, IsGeneratedByNear F s x) :
    IsClosedImmersion (fittingRankStratum F s).hom

AlgebraicGeometry.BottomRankStratum.exists_isBottomRankStratum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/BottomRankStratumMain.lean, line 355.

The bottom rank stratum of a perfect complex. Let E be perfect of Tor amplitude in [a, b] and r a natural number. There is a locally closed immersion j : Z ⟶ X with H^a(Lj^* E) finite locally free of rank r, through which a morphism f : Y ⟶ X factors exactly when H^a(L(g ∘ f)^* E) is finite locally free of rank r for every g : Y' ⟶ Y (IsBottomRankStratum). The morphism j is of finite presentation, and H^a(L(g ∘ j)^* E) ≅ g^* H^a(Lj^* E) for every g : Y ⟶ Z. If β_a ≤ r everywhere, then j is a closed immersion, a morphism f factors through Z exactly when H^a(Lf^* E) is finite locally free of rank r, and, when r = 1, exactly when the scalar action 𝒪_Y ⟶ SheafHom(H^a(Lf^* E), H^a(Lf^* E)) is a monomorphism.

theorem exists_isBottomRankStratum (E : DerivedCategory X.Modules)
    (hE : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace) E) (a b : ℤ)
    (htor : Stacks.Cohomology.TorAmplitude.HasTorAmplitude X.toRingedSpace E a b) (r : ℕ) :
    ∃ (Z : Scheme.{u}) (j : Z ⟶ X), IsBottomRankStratum E a r j ∧ FinitePresentation j ∧
      (∀ (Y : Scheme.{u}) (g : Y ⟶ Z), Nonempty (pullbackHomology E a (g ≫ j) ≅
        (Scheme.Modules.pullback g).obj (pullbackHomology E a j))) ∧
      ((∀ x : X, DerivedFibreBetti.derivedFiberBetti X E
          (Scheme.Modules.isPseudoCoherent_of_isPerfect E hE) a x ≤ r) →
        IsClosedImmersion j ∧
        (∀ (Y : Scheme.{u}) (f : Y ⟶ X), (∃ g : Y ⟶ Z, g ≫ j = f) ↔
          SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} (pullbackHomology E a f) r) ∧
        (r = 1 → ∀ (Y : Scheme.{u}) (f : Y ⟶ X), (∃ g : Y ⟶ Z, g ≫ j = f) ↔
          Mono (Stacks.SheafOfModules.scalarAction Y.toRingedSpace (pullbackHomology E a f)
            (Stacks.Cohomology.SheafHomComplex.sheafHom Y.sheaf _ _))))

Sources

• Section 36.31, Tag 0BDH
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.DerivedFibreBetti.isPseudoCoherent_derivedPullback · AlgebraicGeometry.DerivedFibreBetti.derivedFiberBetti_derivedPullback · AlgebraicGeometry.DerivedFibreBetti.isLocallyConstructible_derivedFiberBetti_preimage · AlgebraicGeometry.DerivedFibreBetti.upperSemicontinuous_derivedFiberBetti · AlgebraicGeometry.DerivedFibreBetti.isLocallyConstant_chiDerivedFibre · AlgebraicGeometry.Scheme.Modules.nonempty_iso_singleFunctor_restrict_iff_le · AlgebraicGeometry.Scheme.Modules.isZero_homology_singleDegreeRankOpen · AlgebraicGeometry.Scheme.Modules.nonempty_iso_singleFunctor_restrict_singleDegreeRankOpen

Section36.32 Applications#

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

Tag 0BDN, a lemma

Tag 0BDN in the Stacks Project.

AlgebraicGeometry.FibreBetti.fibreBetti_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/FibreBettiNumbers.lean, line 179. The attribute's comment: “part (1): formation of the Betti functions beta_i of the fibres commutes with arbitrary base change. The function beta_i is fibreBetti, dim over kappa(s) of H^i of the pullback of F to the scheme-theoretic fibre X_s, and all four hypotheses of the source are fields of IsFlatFamily, which CohomologyAndBaseChange extends. WHAT IS ASSUMED rather than proved: the source's cohomology-and-base-change step, carried as the fields isPseudoCoherent and fibreBetti_eq of CohomologyAndBaseChange (that Rf_F is pseudo-coherent and that beta_i is its derived-fibre Betti function) and as BaseChangeCompatible (that the formation of Rf_F commutes with the cartesian square). Both are consequences of Stacks 0B91, of which this library carries ONLY the base-change half of the conclusion and that half in the tensor form of the source's own reduction, namely AlgebraicGeometry.ProperFlatBaseChange.isIso_tensorFlatBaseChangeMap_module in StacksFrontier/AlgebraicGeometry/Perfect/ProperFlatPushforwardBaseChange.lean line 334, tagged at line 309: invertibility of tensorFlatBaseChangeMap at F in degree zero, hence for Rf_(O_X tensor^L F) and not for Rf_F, with the perfection half absent from the library altogether. WHAT IS PROVED here: the transport of the conclusion across those identifications, using derivedFiberBetti_eq_of_iso and part (1) of Stacks 0BDI, AlgebraicGeometry.DerivedFibreBetti.derivedFiberBetti_derivedPullback”.

The formation of β_i commutes with arbitrary base change: for a cartesian square whose right-hand vertical morphism is f : X ⟶ S and whose base is changed along an arbitrary g : S' ⟶ S, the i-th Betti-number function of the family (f', (g')^*ℱ) is the pullback along g of the i-th Betti-number function of (f, ℱ).

public theorem fibreBetti_baseChange {X S X' S' : Scheme.{u}} (f : X ⟶ S) (g : S' ⟶ S)
    (f' : X' ⟶ S') (g' : X' ⟶ X) (F : X.Modules)
    (h : CohomologyAndBaseChange f F)
    (h' : CohomologyAndBaseChange f' ((Scheme.Modules.pullback g').obj F))
    (hbc : BaseChangeCompatible f g f' g' F) (i : ℤ) :
    fibreBetti f' ((Scheme.Modules.pullback g').obj F) i = fibreBetti f F i ∘ g.base

AlgebraicGeometry.FibreBetti.upperSemicontinuous_fibreBetti, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/FibreBettiNumbers.lean, line 215. The attribute's comment: “part (2): the Betti functions beta_i of the fibres are upper semi-continuous, for beta_i the function fibreBetti and all four hypotheses of the source present as fields of IsFlatFamily. WHAT IS ASSUMED rather than proved: first the cohomology-and-base-change step, as the fields isPseudoCoherent and fibreBetti_eq of CohomologyAndBaseChange, which is the half of Stacks 0B91 this library does not carry (see the attribute on fibreBetti_baseChange and AlgebraicGeometry.ProperFlatBaseChange.isIso_tensorFlatBaseChangeMap_module in StacksFrontier/AlgebraicGeometry/Perfect/ProperFlatPushforwardBaseChange.lean line 334, tagged at line 309); and second part (2) of Stacks 0BDI for Rf_F, which is NOT in the library -- the only @[stacks 0BDI] attributes in the library are on its base-change half -- and which is assumed here in its LOCAL form only, as upper semi-continuity of the derived-fibre Betti function of the derived pullback of Rf_F to each affine open of S. The affine case of that input is available for an object of D(R) on PrimeSpectrum R as StacksDraft.Perfect.upperSemicontinuous_fibreBetti_of_isPseudoCoherent in StacksFrontier/Homology/Perfect/BettiSemicontinuity.lean line 395, but no bridge from it to AlgebraicGeometry.DerivedFibreBetti.derivedFiberBetti on Spec R exists in the library. WHAT IS PROVED here: the passage from that local form to upper semi-continuity on S, by the reduction AlgebraicGeometry.DerivedFibreBetti.upperSemicontinuous_derivedFiberBetti_of_openImmersions applied to the cover of S by its affine opens, and the transport of the conclusion to beta_i”.

The Betti-number function β_i is upper semi-continuous, provided that for every affine open U of S the derived-fibre Betti function of the restriction of Rf_*ℱ to U is upper semi-continuous.

public theorem upperSemicontinuous_fibreBetti {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules)
    (h : CohomologyAndBaseChange f F) (i : ℤ)
    (hloc : ∀ U : S.affineOpens, UpperSemicontinuous
      (DerivedFibreBetti.derivedFiberBetti U.1.toScheme
        ((derivedPullback U.1.ι.toLRSHom.toShHom).obj (totalDirectImage f F))
        (DerivedFibreBetti.isPseudoCoherent_derivedPullback U.1.ι (totalDirectImage f F)
          h.isPseudoCoherent) i)) :
    UpperSemicontinuous (fibreBetti f F i)

AlgebraicGeometry.FibreBetti.fibreBetti_baseChange_upperSemicontinuous_isLocallyConstructible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/FibreBettiNumbersCohomologyBaseChange.lean, line 187. References: SGA 6 III (5.7), “(ii), special case”.

[Stacks, Tag 0BDN]. Let f : X ⟶ S be a proper morphism of finite presentation and let ℱ be an 𝒪_X-module of finite presentation, flat over S. Fix i ∈ ℤ and let β_i be the function s ↦ dim_{κ(s)} H^i(X_s, ℱ_s) (AlgebraicGeometry.FibreBetti.fibreBetti). Then

1. the formation of β_i commutes with arbitrary base change: for every cartesian square with g : S' ⟶ S, f' : X' ⟶ S' and g' : X' ⟶ X, the function β_i of (f', (g')^*ℱ) is β_i ∘ g;
2. β_i is upper semi-continuous;
3. every level set β_i⁻¹{n} is locally constructible in S.

The proof is the source's. By [Stacks, Tag 0B91], β_i is the derived-fibre Betti function of the perfect object Rf_*ℱ (fibreBetti_eq_derivedFiberBetti), so the three parts are parts (1), (2) and (3) of [Stacks, Tag 0BDI].

public theorem fibreBetti_baseChange_upperSemicontinuous_isLocallyConstructible
    {X S : Scheme.{u}} (f : X ⟶ S) (hf : FinitePresentation f) [IsProper f] (F : X.Modules)
    [F.IsFinitePresentation] (hflat : IsFlatOver f.toLRSHom.toShHom F) (i : ℤ) :
    (∀ {X' S' : Scheme.{u}} (g : S' ⟶ S) (f' : X' ⟶ S') (g' : X' ⟶ X),
        IsPullback g' f' f g →
          fibreBetti f' ((Scheme.Modules.pullback g').obj F) i = fibreBetti f F i ∘ g.base) ∧
      UpperSemicontinuous (fibreBetti f F i) ∧
      ∀ n : ℕ, IsLocallyConstructible (fibreBetti f F i ⁻¹' {n})

Tag 0B9T, a lemma

Tag 0B9T in the Stacks Project.

AlgebraicGeometry.ProperFlatFibreEulerCharacteristic.isLocallyConstant_chiFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ProperFlatFibreEulerCharacteristic.lean, line 187. The attribute's comment: “the local constancy conclusion, with the function in the derived-fibre form s |-> sum (-1)^i dim_k(s) H^i(Rf_F tensor^L k(s)) that the source's proof passes to. Rf_F is perfect by Tag 0B91 (2), proved as isPerfect_derivedPushforward_singleFunctor_of_isProper, and the conclusion is Tag 0BDJ at Rf_*F. The identification with s |-> chi(X_s, F_s) and the statement in that form are in ProperFlatFibreEulerCharacteristicUnconditional.lean (isLocallyConstant_fibreEulerCharacteristic). The base-change conclusion is chiFibre_baseChange”.

[Stacks, Tag 0B9T], the first conclusion. For a proper morphism f : X ⟶ S of finite presentation and an 𝒪_X-module ℱ of finite presentation, flat over S, the Euler characteristic of the derived fibres of Rf_*ℱ is a locally constant function on S.

Rf_*ℱ is perfect by the perfection half of [Stacks, Tag 0B91] (2), isPerfect_derivedPushforward_singleFunctor_of_isProper, and this is [Stacks, Tag 0BDJ] at Rf_*ℱ.

public theorem isLocallyConstant_chiFibre
    {X S : Scheme.{u}} (f : X ⟶ S) (hf : FinitePresentation f) (hproper : IsProper f)
    (F : X.Modules) (hfp : F.IsFinitePresentation)
    (hflat : IsFlatOver f.toLRSHom.toShHom F) :
    IsLocallyConstant (chiFibre f F
      (DerivedFibreBetti.isPseudoCoherent_of_isPerfect _
        (isPerfect_derivedPushforward_singleFunctor_of_isProper f hf hproper F hfp hflat)))

AlgebraicGeometry.ProperFlatFibreEulerCharacteristic.chiFibre_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ProperFlatFibreEulerCharacteristic.lean, line 227. The attribute's comment: “the base-change conclusion ('formation of this function commutes with base change'), with the function in the derived-fibre form s |-> sum (-1)^i dim_k(s) H^i(Rf_F tensor^L k(s)), for every cartesian square. The isomorphism Lg^Rf_F = Rf'_(g')^*F is Tag 0B91 (2), proved as nonempty_derivedPullback_derivedPushforward_singleFunctor_iso; the conclusion is then Tag 0BDI summed over the degrees, chiDerivedFibre_derivedPullback, and invariance under isomorphism, chiDerivedFibre_congr. hpc and hpc' are the pseudo-coherence proofs the function is built from, and the equality holds for all of them. The statement for s |-> chi(X_s, F_s) itself is fibreEulerCharacteristic_baseChange in ProperFlatFibreEulerCharacteristicUnconditional.lean. The local constancy conclusion is isLocallyConstant_chiFibre”.

[Stacks, Tag 0B9T], the second conclusion. Formation of the Euler characteristic of the derived fibres of Rf_*ℱ commutes with base change: for a cartesian square

X' --g'--> X
|          |
f'         f
v          v
S' --g---> S

the function on S' attached to f' and (g')^*ℱ is the function on S attached to f and ℱ, composed with g.

The base-change isomorphism Lg^*Rf_*ℱ ≅ Rf'_*(g')^*ℱ is the base-change half of [Stacks, Tag 0B91] (2), nonempty_derivedPullback_derivedPushforward_singleFunctor_iso; with it, this is the base-change clause of [Stacks, Tag 0BDI] summed over the degrees, AlgebraicGeometry.DerivedFibreBetti.chiDerivedFibre_derivedPullback, together with the invariance of the derived-fibre Euler characteristic under isomorphism. The function is defined from a proof of pseudo-coherence of each object, hpc and hpc'; the equality holds for every such proof.

public theorem chiFibre_baseChange
    {X S X' S' : Scheme.{u}} (f : X ⟶ S) (g : S' ⟶ S) (f' : X' ⟶ S') (g' : X' ⟶ X)
    (hsq : IsPullback g' f' f g) (hf : FinitePresentation f) (hproper : IsProper f)
    (F : X.Modules) (hfp : F.IsFinitePresentation)
    (hflat : IsFlatOver f.toLRSHom.toShHom F)
    (hpc : RingedSpace.IsPseudoCoherent (X := S.toRingedSpace) (derivedPushforwardModule f F))
    (hpc' : RingedSpace.IsPseudoCoherent (X := S'.toRingedSpace)
      (derivedPushforwardModule f' ((Scheme.Modules.pullback g').obj F))) :
    chiFibre f' ((Scheme.Modules.pullback g').obj F) hpc' =
      chiFibre f F hpc ∘ g.base

AlgebraicGeometry.ProperFlatFibreEulerCharacteristic.isLocallyConstant_fibreEulerCharacteristic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ProperFlatFibreEulerCharacteristicUnconditional.lean, line 141. The attribute's comment: “local constancy of s |-> chi(X_s, F_s)”. References: EGA III (7.9.4), “special case”; EGA III (7.9.5), “special case”.

For f : X ⟶ S proper and of finite presentation and ℱ an 𝒪_X-module of finite presentation, flat over S, the function s ↦ χ(X_s, ℱ_s) is locally constant on S.

theorem isLocallyConstant_fibreEulerCharacteristic {X S : Scheme.{u}} (f : X ⟶ S)
    (hf : FinitePresentation f) [IsProper f] (F : X.Modules) (hF : F.IsFinitePresentation)
    (hflat : IsFlatOver f.toLRSHom.toShHom F) :
    IsLocallyConstant (fibreEulerCharacteristic f F)

AlgebraicGeometry.ProperFlatFibreEulerCharacteristic.fibreEulerCharacteristic_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ProperFlatFibreEulerCharacteristicUnconditional.lean, line 155. The attribute's comment: “formation of s |-> chi(X_s, F_s) commutes with base change”. References: EGA III (7.9.7), “special case”.

Formation of s ↦ χ(X_s, ℱ_s) commutes with base change: for a cartesian square with g : S' ⟶ S, the function attached to the base change f' : X' ⟶ S' and (g')^*ℱ is the function attached to f and ℱ, composed with g.

theorem fibreEulerCharacteristic_baseChange {X S X' S' : Scheme.{u}} (f : X ⟶ S) (g : S' ⟶ S)
    (f' : X' ⟶ S') (g' : X' ⟶ X) (hsq : IsPullback g' f' f g) (hf : FinitePresentation f)
    [IsProper f] (F : X.Modules) (hF : F.IsFinitePresentation)
    (hflat : IsFlatOver f.toLRSHom.toShHom F) :
    fibreEulerCharacteristic f' ((Scheme.Modules.pullback g').obj F) =
      fibreEulerCharacteristic f F ∘ g.base

Tag 0B9S, a lemma

Tag 0B9S in the Stacks Project.

AlgebraicGeometry.ProperFlatRankOpen.factorsThrough_rankOpen_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ProperFlatRankOpen.lean, line 240. The attribute's comment: “for an open immersion T --> S only, and with rank r : N; nothing is assumed -- the base-change input is proved here as openImmersionBaseChangeDerivedPushforward from Tag 08FE. See the declaration docstring”.

[Stacks, Tag 0B9S], the characterising property of the open subscheme, for an open immersion of the base. Let f : X ⟶ S be proper of finite presentation, let ℱ be an 𝒪_X-module of finite presentation, flat over S, and fix i and r. An open immersion g : T ⟶ S factors through rankOpen f ℱ i r exactly when Rf_{T,*}ℱ_T is isomorphic to a finite locally free module of rank r placed in degree i.

This is [Stacks, Tag 0BDK] at Rf_*ℱ, together with the base change of openImmersionBaseChangeDerivedPushforward.

Nothing is assumed. The base-change input — the half of [Stacks, Tag 0B91] clause (2) which identifies the restriction of Rf_*ℱ along g with Rf_{T,*}(g')^*ℱ — is proved here, as openImmersionBaseChangeDerivedPushforward, from [Stacks, Tag 08FE]: derived direct image commutes with restriction to an open of the base, which is available precisely because g is an open immersion. So neither the tensor form of Tag 0B91 nor the unit coherence of [Stacks, Tag 079U] is involved. The perfectness half of Tag 0B91 is likewise not needed: neither singleDegreeRankOpen nor its universal property for open immersions uses it.

Two scope restrictions, neither a carried hypothesis. First, the characterising property is delivered only for an open immersion T ⟶ S, not for an arbitrary morphism as the source states it: the universal property of the open subscheme of [Stacks, Tag 0BDK] is available in this library only for open immersions, as AlgebraicGeometry.Scheme.Modules.factorsThrough_singleDegreeRankOpen_iff, the description along an arbitrary morphism needing the pointwise description of that open through the Betti numbers of the derived fibres, which uses perfectness. Second, the rank r is a natural number where the source says i, r ∈ ℤ; this follows singleDegreeRankOpen, and for a negative r the open the source asserts is empty and the statement vacuous.

public theorem factorsThrough_rankOpen_iff
    (f : X ⟶ S) (hf : FinitePresentation f) (hproper : IsProper f)
    (F : X.Modules) (hfp : F.IsFinitePresentation)
    (hflat : IsFlatOver f.toLRSHom.toShHom F) (i : ℤ) (r : ℕ)
    {T XT : Scheme.{u}} (g : T ⟶ S) [IsOpenImmersion g] (fT : XT ⟶ T) (g' : XT ⟶ X)
    (hsq : IsPullback g' fT f g) :
    (∃ h : T ⟶ (rankOpen f F i r).toScheme, h ≫ (rankOpen f F i r).ι = g) ↔
      ∃ M : T.Modules,
        AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} M r ∧
          Nonempty (derivedPushforwardModule fT ((Scheme.Modules.pullback g').obj F) ≅
            (DerivedCategory.singleFunctor T.Modules i).obj M)

AlgebraicGeometry.ProperFlatRankOpen.exists_opens_factorsThrough_iff_derivedPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ProperFlatRankOpenBaseChange.lean, line 207.

[Stacks, Tag 0B9S]. Let f : X ⟶ S be a proper morphism of finite presentation, let ℱ be an 𝒪_X-module of finite presentation, flat over S, and fix i, r ∈ ℤ. Then there exists an open subscheme U ⊆ S with the following property: a morphism g : T ⟶ S factors through U if and only if Rf_{T,*}ℱ_T is isomorphic to a finite locally free module of rank r placed in degree i. Here, for any cartesian square

X_T --g'--> X
 |          |
f_T         f
 v          v
 T  --g---> S

ℱ_T = (g')^*ℱ and Rf_{T,*}ℱ_T is the derived direct image of ℱ_T placed in degree 0; the property holds for every such square.

For r ≥ 0 the open subscheme is rankOpen f ℱ i r and the property is factorsThrough_rankOpen_iff_baseChange. For r < 0 it is ∅: both sides say that T is empty, by factorsThrough_bot_iff and isEmpty_of_isFiniteLocallyFreeOfIntRank, and on an empty T the case of rank 0 supplies the module.

public theorem exists_opens_factorsThrough_iff_derivedPushforward
    (f : X ⟶ S) (hf : FinitePresentation f) (hproper : IsProper f)
    (F : X.Modules) (hfp : F.IsFinitePresentation)
    (hflat : IsFlatOver f.toLRSHom.toShHom F) (i r : ℤ) :
    ∃ U : S.Opens, ∀ {T XT : Scheme.{u}} (g : T ⟶ S) (fT : XT ⟶ T) (g' : XT ⟶ X),
      IsPullback g' fT f g →
        ((∃ h : T ⟶ U.toScheme, h ≫ U.ι = g) ↔
          ∃ M : T.Modules, IsFiniteLocallyFreeOfIntRank M r ∧
            Nonempty (derivedPushforwardModule fT ((Scheme.Modules.pullback g').obj F) ≅
              (DerivedCategory.singleFunctor T.Modules i).obj M))

AlgebraicGeometry.ProperFlatFibreEulerCharacteristic.exists_opens_factorsThrough_iff_hasDerivedPushforwardRank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ProperFlatRankOpenUnconditional.lean, line 50. The attribute's comment: “the rank r is a natural number: no module is locally free of negative rank, so for r < 0 the source's open is empty”.

[Stacks, Tag 0B9S]. Let π : Y ⟶ T be proper and of finite presentation, ℱ an 𝒪_Y-module of finite presentation flat over T, i an integer and r a natural number. There is an open U ⊆ T such that a morphism h : T' ⟶ T factors through U exactly when Rπ'_*(h'^*ℱ) is a finite locally free 𝒪_{T'}-module of rank r placed in degree i, for the base change π' : Y' ⟶ T' of π along h (any cartesian square).

theorem exists_opens_factorsThrough_iff_hasDerivedPushforwardRank {Y T : Scheme.{u}}
    (π : Y ⟶ T) (hfp : FinitePresentation π) [IsProper π] (F : Y.Modules)
    (hF : F.IsFinitePresentation) (hflat : IsFlatOver π.toLRSHom.toShHom F) (i : ℤ) (r : ℕ) :
    ∃ U : T.Opens, ∀ {Y' T' : Scheme.{u}} (h : T' ⟶ T) (π' : Y' ⟶ T') (h' : Y' ⟶ Y),
      IsPullback h' π' π h →
      ((∃ g : T' ⟶ U.toScheme, g ≫ U.ι = h) ↔
        HasDerivedPushforwardRank π' ((Scheme.Modules.pullback h').obj F) i r)

Tag 0D4E, a lemma

Tag 0D4E in the Stacks Project.

Stacks.AlgebraicGeometry.VanishingHigherDirectImages.isFiniteLocallyFree_pushforward_and_isIso_baseChange_of_isZero_higherDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/VanishingHigherDirectImagesLocallyFree.lean, line 85. The attribute's comment: “both conclusions: f_F is finite locally free, and for every cartesian square the canonical comparison g^f_F --> f'_(g')^*F (baseChangeNatTrans, the mate of the two pullback-pushforward adjunctions) is an isomorphism, which is the meaning the source's proof gives to commutes with arbitrary base change”. References: EGA III (7.9.10), “partial”; SGA 6 III (5.7), “(iii), special case”.

[Stacks, Tag 0D4E]. Let f : X ⟶ S be a morphism of schemes of finite presentation and let ℱ be an 𝒪_X-module of finite presentation, flat over S, whose support is proper over S. If R ⁱ f_* ℱ = 0 for all i > 0, then

1. f_* ℱ is a finite locally free 𝒪_S-module, and
2. the formation of f_* ℱ commutes with arbitrary base change: for every cartesian square with g' : X' ⟶ X, f' : X' ⟶ S' and g : S' ⟶ S, the canonical comparison map g^* f_* ℱ ⟶ f'_* (g')^* ℱ (Stacks.AlgebraicGeometry.AffinePushforward.baseChangeNatTrans) is an isomorphism.

The first conclusion is isFiniteLocallyFree_pushforward_of_isZero_higherDirectImage, the second isIso_baseChangeNatTrans_app_of_vanishing.

public theorem isFiniteLocallyFree_pushforward_and_isIso_baseChange_of_isZero_higherDirectImage
    {X S : Scheme.{u}} (f : X ⟶ S) (hf : FinitePresentation f) (F : X.Modules)
    [F.IsFinitePresentation] (hflat : IsFlatOver f.toLRSHom.toShHom F)
    (hsupp : letI : LocallyOfFinitePresentation f := hf.locallyOfFinitePresentation
      ∃ Z : Closeds X, IsProperOver f Z ∧ SheafOfModules.supp F ⊆ (Z : Set X))
    (hvanish : ∀ i : ℤ, 0 < i →
      IsZero (((Scheme.Modules.pushforward f).rightDerivedPlus i).obj F)) :
    _root_.AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u}
        (R := S.ringCatSheaf) ((Scheme.Modules.pushforward f).obj F) ∧
      ∀ {X' S' : Scheme.{u}} (g : S' ⟶ S) (f' : X' ⟶ S') (g' : X' ⟶ X)
        (hsq : IsPullback g' f' f g),
        IsIso ((Stacks.AlgebraicGeometry.AffinePushforward.baseChangeNatTrans hsq.w).app F)

Tag 0E62, a lemma

Tag 0E62 in the Stacks Project.

StacksDraft.Perfect.UnitSplitting.exists_localization_iso_single_homology_biprod_truncGE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ProperFlatFamily/AffineLocalSplitting.lean, line 187. The attribute's comment: “PART (b) ONLY, and only in its AFFINE-LOCAL ALGEBRAIC FORM: the statement is about an abstract pseudo-coherent object K of D(R) for a commutative ring R, standing for E = Rf_*O_X restricted to an affine open of S, and NOTHING HERE IDENTIFIES K WITH A DERIVED DIRECT IMAGE. The source's proof has four steps and the first, geometric one is NOT performed: cohomology and base change (Tag 0B91), which gives that E is perfect and that its formation commutes with arbitrary base change, is not invoked at all. What is assumed of K instead is exactly what the source's remaining three steps use of E: pseudo-coherence (the part of perfectness Tag 0A1U asks for); the vanishing of H^i(K) for i < 0 and of H^{-1}(K tensor^L k(p)), which are the two consequences of E has tor amplitude in [0, infinity) that the source uses, taken as two separate vanishing statements because StacksDraft.TorAmplitude.HasTorAmplitude carries the derived tensor product, its comparison and its universal property as explicit parameters and nothing stronger is needed; and surjectivity of H^0(K) tensor k(p) --> H^0(K tensor^L k(p)) at p, which is the source's second step. WITHIN part (b), THE FIRST SUMMAND IS NOT IDENTIFIED WITH O_S. What is delivered is the splitting K_g = H^0(K)_g[0] (+) tau_{>=1}K_g after localizing away from a single element g outside p, with tau_{>=1}K_g perfect of tor amplitude in [1, infinity) -- the source's step 3, Tag 0A1U -- and with H^0(K)_g FINITE FREE over R_g, which is the half of the source's step 4 that Tags 0658 and 00NX supply. The remaining half of step 4, that the unit O_S --> H^0(E) is an isomorphism, is NOT carried, and that is also exactly PART (a) of this tag, f_*O_X = O_S and this holds after any base change, WHICH IS NOT DELIVERED ANYWHERE in this file: carrying it needs the map H^0(epsilon) : R --> H^0(K) induced by a unit epsilon : R[0] --> K, which this statement does not take as data, and then the transport of the fibrewise bijectivity of that map from the primes of R to the primes of R_g so that the isomorphism locus of Algebra Tag 00O0 (3) can be read at the prime of R_g above p; that locus result IS carried in this library, as Stacks.FiniteProjective.MapLocus.isOpen_isoLocus_and_localized, but neither the induced map nor the transport is written here. The statement is algebraic rather than geometric because Tags 0A1U and 0A1V are carried in this library only over a commutative ring, as StacksDraft.Perfect results about D(R) in StacksFrontier/Homology/Perfect/FibreCriterion.lean -- no declaration anywhere in the library carries either tag for the derived category of modules on a scheme -- so the geometric statement would need in addition the affine-local comparison of D(O_S)|_U with D(R) for U = Spec R an affine open, and the identification of H^0(E tensor^L k(s)) with H^0(X_s, O_{X_s}), which the module documentation of StacksFrontier/AlgebraicGeometry/Perfect/ProperFlatFibreEulerCharacteristic.lean records as absent from this library. What is PROVED here, assuming nothing beyond the stated hypotheses on K: that the degree -1 base-change map is surjective because its target vanishes, so that Tag 0A1V applies at degree 0; that the vanishing of H^i(K) below degree 0 places the localization K_g in degrees >= 0 and so kills the summand tau_{<=-1}K_g of the three-term decomposition of Tag 0A1V; and the assembly of the remaining two summands into the two-term splitting the source states”.

The affine-local algebraic form of part (b) of [Stacks, Tag 0E62].

Let R be a commutative ring, p ⊂ R a prime, and K a pseudo-coherent object of D(R) -- standing for E = Rf_*𝒪_X restricted to an affine open of S. Assume

• Hⁱ(K) = 0 for i < 0 and H^{-1}(K ⊗_R^L κ(p)) = 0, and
• H⁰(K) ⊗_R κ(p) → H⁰(K ⊗_R^L κ(p)) is surjective.

Then there is g ∈ R, g ∉ p, such that over R_g the localization K_g = K ⊗_R R_g splits as

K_g ≅ H⁰(K)_g[0] ⊕ τ_{≥1}K_g,

where H⁰(K)_g is a finite free R_g-module and τ_{≥1}K_g is a perfect object of D(R_g) of Tor amplitude in [1, ∞), recorded by a bounded complex of finite projective R_g-modules concentrated in degrees ≥ 1 representing it whose termwise tensor products have no cohomology below degree 1.

theorem exists_localization_iso_single_homology_biprod_truncGE
    {R : Type u} [CommRing R] (p : Ideal R) [p.IsPrime]
    (K : DerivedCategory (ModuleCat.{max u v} R))
    (hK : StacksDraft.PseudoCoherence.IsPseudoCoherent K)
    (hneg : ∀ i : ℤ, i < 0 →
      IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{max u v} R) i).obj K))
    (hfib : FibreCohomologyVanishes.{u, v} p K (-1))
    (hbase : CohomologyBaseChangeSurjective.{u, v} p K 0) :
    ∃ g : R, g ∉ p ∧
      let Rg := Localization.Away g
      let Kg := (PseudoCoherence.localizationAwayFunctorAux.{u, v} g).obj K
      let upper := (DerivedCategory.TStructure.t.truncGE 1).obj Kg
      let H0g := (ModuleCat.extendScalars (algebraMap R Rg)).obj
        ((DerivedCategory.homologyFunctor (ModuleCat.{max u v} R) 0).obj K)
      Module.Finite Rg H0g ∧ Module.Free Rg H0g ∧ IsPerfect upper ∧
        (∃ (P : CochainComplex (ModuleCat.{max u v} Rg) ℤ) (b : ℤ),
          P.IsStrictlyGE 1 ∧ P.IsStrictlyLE b ∧
            (∀ j : ℤ, Module.Finite Rg (P.X j)) ∧
            (∀ j : ℤ, Module.Projective Rg (P.X j)) ∧
            Nonempty (upper ≅ DerivedCategory.Q.obj P) ∧
            ∀ (M : ModuleCat.{max u v} Rg) (j : ℤ), j < 1 →
              IsZero ((TorAmplitude.tensorComplex P M).homology j)) ∧
        Nonempty (Kg ≅
          (DerivedCategory.singleFunctor (ModuleCat.{max u v} Rg) 0).obj H0g ⊞ upper)

Stacks.AlgebraicGeometry.ProperFlatStructureSheafSplitting.properFlat_structureSheaf_splitting, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ProperFlatFamily/StructureSheafSplitting.lean, line 499.

[Stacks, Tag 0E62]. Let f : X ⟶ S be a morphism of schemes which is proper, flat and of finite presentation, and assume that for every s ∈ S the canonical map κ(s) → H⁰(X_s, 𝒪_{X_s}) is bijective. Then

• (a) f_*𝒪_X = 𝒪_S, and this holds after any base change: for every cartesian square X' = X ×_S S' the comparison 𝒪_{S'} ⟶ f'_*𝒪_{X'} of sheaves of rings is an isomorphism;
• (b) locally on S we have Rf_*𝒪_X ≅ 𝒪_S ⊕ P in D(𝒪_S) with P perfect of Tor amplitude in [1, ∞): every point of S lies in the image of an open immersion ι : V ⟶ S over which the restriction of Rf_*𝒪_X is isomorphic to 𝒪_V ⊕ P with P a perfect object of D(𝒪_V) of Tor amplitude in [1, b] for some b.

theorem properFlat_structureSheaf_splitting {X S : Scheme.{u}} (f : X ⟶ S) [IsProper f] [Flat f]
    (hfp : FinitePresentation f)
    (hfib : ∀ s : S, Function.Bijective ((Scheme.ΓSpecIso (S.residueField s)).inv ≫
      (f.fiberToSpecResidueField s).appTop)) :
    (IsIso f.c ∧
      ∀ {X' S' : Scheme.{u}} (g : S' ⟶ S) (f' : X' ⟶ S') (g' : X' ⟶ X),
        IsPullback g' f' f g → IsIso f'.c) ∧
    ∀ s : S, ∃ (V : Scheme.{u}) (ι : V ⟶ S) (_ : IsOpenImmersion ι)
      (P : DerivedCategory V.Modules),
      s ∈ Set.range ι ∧ RingedSpace.IsPerfect (X := V.toRingedSpace) P ∧
      (∃ b : ℤ, Stacks.Cohomology.TorAmplitude.HasTorAmplitude V.toRingedSpace P 1 b) ∧
      Nonempty ((Scheme.Modules.restrictFunctor ι).mapDerivedCategory.obj
          ((derivedPushforward f.toLRSHom.toShHom).obj
            ((DerivedCategory.singleFunctor X.Modules 0).obj (Scheme.unitModule X))) ≅
        ((DerivedCategory.singleFunctor V.Modules 0).obj (Scheme.unitModule V) ⊞ P :
          DerivedCategory V.Modules))

Tag 0E0L, a lemma

Tag 0E0L in the Stacks Project.

Stacks.AlgebraicGeometry.ProperFlatStructureSheaf.isIso_c_and_isIso_c_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ProperFlatFamily/GeometricFibresDirectImage.lean, line 64. The attribute's comment: “both conclusions: f_*O_X = O_S, as invertibility of the comparison f.c of sheaves of rings, and the same for every base change, stated for every cartesian square over S.”.

Stacks Project, Tag 0E0L. Let f : X ⟶ S be proper, flat and of finite presentation, with geometric fibres reduced and connected. Then f_*𝒪_X = 𝒪_S, i.e. f.c : 𝒪_S ⟶ f_*𝒪_X is invertible, and this holds after any base change: for every cartesian square

X' --g'--> X
|f'        |f
v          v
S' --g---> S

the comparison f'.c : 𝒪_{S'} ⟶ f'_*𝒪_{X'} is invertible.

Finite presentation is LocallyOfFinitePresentation f together with quasi-compactness and quasi-separatedness, which properness supplies. The geometric fibres being reduced and connected is GeometricallyReduced f and GeometricallyConnected f.

theorem isIso_c_and_isIso_c_of_isPullback [IsProper f] [Flat f]
    [LocallyOfFinitePresentation f] [GeometricallyReduced f] [GeometricallyConnected f] :
    IsIso f.c ∧ ∀ {X' S' : Scheme.{u}} {g : S' ⟶ S} {g' : X' ⟶ X} {f' : X' ⟶ S'},
      IsPullback g' f' f g → IsIso f'.c

Tag 0G7X, a lemma

Tag 0G7X in the Stacks Project.

Stacks.AlgebraicGeometry.Fibres.extendsOverNeighbourhood_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Fibres/IdempotentExtensionApproximation.lean, line 857.

[Stacks, Tag 0G7X]. An idempotent global function on a fibre of a proper morphism is the restriction of a section of the structure sheaf over the inverse image of an open neighbourhood of the base point; equivalently, it lies in the image of the stalk (f_* 𝒪_X)_s. Nothing is assumed on the base: its locally Noetherian case is Stacks.FormalFunctions.extendsOverNeighbourhood_of_isLocallyNoetherian, and the general case follows from it by the approximation argument above.

public theorem extendsOverNeighbourhood_of_isProper {X S : Scheme.{u}} (f : X ⟶ S) [IsProper f]
    (s : S) (e : Γ(f.fiber s, ⊤)) (he : IsIdempotentElem e) :
    ExtendsOverNeighbourhood f s e

Tag 0G7Y, a lemma

Tag 0G7Y in the Stacks Project.

StacksDraft.Perfect.GeomReducedFibre.exists_open_finiteEtale_and_derivedPushforward_splitting, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/GeomReducedFibre/Main.lean, line 115.

[Stacks, Tag 0G7Y]. Let f : X ⟶ S be proper, flat and of finite presentation and let s ∈ S be a point whose fibre X_s is geometrically reduced. Then there is an affine open neighbourhood U of s such that

• f_*𝒪_X is a finite etale 𝒪_S-algebra over U: for every affine open V ⊆ U the ring map Γ(S, V) → Γ(X, f⁻¹V) is finite and etale;
• Rf_*𝒪_X ≅ f_*𝒪_X ⊕ P in D(𝒪_U) with P perfect of Tor amplitude in [1, b] for some b (so in [1, ∞)), at every model of the derived categories.

theorem exists_open_finiteEtale_and_derivedPushforward_splitting {X S : Scheme.{u}} (f : X ⟶ S)
    (hfp : FinitePresentation f) [IsProper f] [Flat f] (s : S)
    (hred : GeometricallyReduced (f.fiberToSpecResidueField s)) :
    ∃ U : S.Opens, s ∈ U ∧ IsAffineOpen U ∧
      (∀ V : S.affineOpens, V.1 ≤ U →
        letI : Algebra Γ(S, V.1) Γ(X, f ⁻¹ᵁ V.1) := (f.app V.1).hom.toAlgebra
        Module.Finite Γ(S, V.1) Γ(X, f ⁻¹ᵁ V.1) ∧ Algebra.Etale Γ(S, V.1) Γ(X, f ⁻¹ᵁ V.1)) ∧
      ∃ b : ℤ, 1 ≤ b ∧ ∀ (hX : HasDerivedCategory.{w} (f ⁻¹ᵁ U).toScheme.Modules)
        (hU : HasDerivedCategory.{w} U.toScheme.Modules),
        letI := hX
        letI := hU
        letI : HasDerivedCategory.{w}
          (SheafOfModules.{u} (structureSheafRing (f ⁻¹ᵁ U).toScheme.toSheafedSpace)) := hX
        letI : HasDerivedCategory.{w}
          (SheafOfModules.{u} (structureSheafRing U.toScheme.toSheafedSpace)) := hU
        ∃ P : DerivedCategory U.toScheme.Modules,
          @Stacks.Cohomology.PerfectComplexes.IsPerfect U.toScheme.toRingedSpace hU P ∧
          @Stacks.Cohomology.TorAmplitude.HasTorAmplitude U.toScheme.toRingedSpace hU P 1 b ∧
          Nonempty ((DerivedCategory.singleFunctor U.toScheme.Modules 0).obj
              ((Scheme.Modules.pushforward (f ∣_ U)).obj
                (Scheme.unitModule (f ⁻¹ᵁ U).toScheme)) ⊞ P ≅
            (Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward
              (f ∣_ U).toLRSHom.toShHom).obj
              ((DerivedCategory.singleFunctor (f ⁻¹ᵁ U).toScheme.Modules 0).obj
                (Scheme.unitModule (f ⁻¹ᵁ U).toScheme)))

Sources

• Section 36.32, Tag 0BDM
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.FibreBetti.fibreBetti_baseChange · AlgebraicGeometry.FibreBetti.upperSemicontinuous_fibreBetti · AlgebraicGeometry.FibreBetti.fibreBetti_baseChange_upperSemicontinuous_isLocallyConstructible · AlgebraicGeometry.ProperFlatFibreEulerCharacteristic.isLocallyConstant_chiFibre · AlgebraicGeometry.ProperFlatFibreEulerCharacteristic.chiFibre_baseChange · AlgebraicGeometry.ProperFlatFibreEulerCharacteristic.isLocallyConstant_fibreEulerCharacteristic · AlgebraicGeometry.ProperFlatFibreEulerCharacteristic.fibreEulerCharacteristic_baseChange · AlgebraicGeometry.ProperFlatRankOpen.factorsThrough_rankOpen_iff

Section36.33 Other applications#

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

Tag 0EX6, a lemma

Tag 0EX6 in the Stacks Project.

Stacks.AlgebraicGeometry.CoherentBaseCohomology.isCoherent_cohomology_of_isPerfect_derivedGlobalSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/CoherentBaseCohomology.lean, line 168. The attribute's comment: “carrying as an explicit hypothesis Tag 0A1H: RΓ(X, G) is perfect over the base”.

[Stacks, Tag 0EX6]. Let R be a coherent ring, let f : X ⟶ Spec R be of finite presentation ([Stacks, Tag 01TP] (3), spelled out as its three constituent properties) and let G be an 𝒪_X-module of finite presentation, flat over R, whose support is proper over R. Then Hⁱ(X, G), with its R-action restricted along R ⟶ Γ(X, 𝒪_X), is a coherent R-module in every degree.

The proof is the source's: RΓ(X, G) is a perfect object of D(R) ([Stacks, Tag 0A1H] for E = 𝒪_X and the one-term complex G, carried here as the hypothesis hperf), a perfect object is pseudo-coherent ([Stacks, Tag 0658]), and over a coherent ring the cohomology modules of a bounded above pseudo-coherent object are coherent ([Stacks, Tag 0EWZ]); cohomologyIso identifies the cohomology of RΓ(X, G) with Hⁱ(X, G).

Carried hypothesis. hperf : StacksDraft.Perfect.IsPerfect (derivedGlobalSectionsOverBase f G) is Tag 0A1H over the affine base, the one input of the source's proof that this library does not prove. It is a statement about the complex RΓ(X, G), proved by Noetherian approximation, and not the conclusion — which is coherence of the single module Hⁱ(X, G) — restated. The source's own hypotheses are all present; when Tag 0A1H lands, hperf discharges by application.

theorem isCoherent_cohomology_of_isPerfect_derivedGlobalSections
    {R : Type u} [CommRing R] [IsCoherentRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R))
    [LocallyOfFinitePresentation f] [QuasiCompact f] [QuasiSeparated f]
    (G : X.Modules) [G.IsFinitePresentation]
    (_hflat : IsFlatOver f.toLRSHom.toShHom G)
    (_hsupp : ∃ Z : TopologicalSpace.Closeds X,
      (Z : Set X) = SheafOfModules.supp G ∧ IsProperOver f Z)
    (hperf : StacksDraft.Perfect.IsPerfect (derivedGlobalSectionsOverBase f G))
    (i : ℕ) :
    Module.IsCoherent R
      ((ModuleCat.restrictScalars (Stacks.Cech.globalRingHom f).hom).obj
        (((AlgebraicGeometry.moduleGlobalSections X).rightDerived i).obj G))

Stacks.AlgebraicGeometry.CoherentBaseCohomology.isCoherent_rightDerived_moduleGlobalSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/CoherentBaseCohomologyUnconditional.lean, line 68.

[Stacks, Tag 0EX6]. Let R be a coherent ring, let f : X ⟶ Spec R be of finite presentation and let G be an 𝒪_X-module of finite presentation, flat over R, whose support is proper over R. Then for every i the cohomology module Hⁱ(X, G), with its R-action restricted along R ⟶ Γ(X, 𝒪_X), is a coherent R-module.

The source's proof: RΓ(X, G) is a perfect object of D(R) by [Stacks, Tag 0A1H] (…ProperSupportGlobalSectionsPerfect.isPerfect_derivedGlobalSectionsOverBase_of_properSupport), and over a coherent ring the cohomology modules of a perfect complex are coherent by [Stacks, Tag 0658] and [Stacks, Tag 0EWZ] (isCoherent_cohomology_of_isPerfect_derivedGlobalSections).

theorem isCoherent_rightDerived_moduleGlobalSections
    {R : Type u} [CommRing R] [IsCoherentRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R))
    [LocallyOfFinitePresentation f] [QuasiCompact f] [QuasiSeparated f]
    (G : X.Modules) [G.IsFinitePresentation]
    (hflat : IsFlatOver f.toLRSHom.toShHom G)
    (hsupp : ∃ Z : TopologicalSpace.Closeds X,
      (Z : Set X) = SheafOfModules.supp G ∧ IsProperOver f Z)
    (i : ℕ) :
    Module.IsCoherent R
      ((ModuleCat.restrictScalars (Stacks.Cech.globalRingHom f).hom).obj
        (((AlgebraicGeometry.moduleGlobalSections X).rightDerived i).obj G))

Tag 0CRP, a lemma

Tag 0CRP in the Stacks Project.

Stacks.Cohomology.CountableSections.countable_cohomology_derivedTensor_and_ext_of_isCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/CountableExtAndTensor.lean, line 336.

[Stacks, Tag 0CRP]. Let X be a quasi-compact and quasi-separated scheme. Let K be an object of D_QCoh(𝒪_X) such that the cohomology sheaves H^i(K) have countable sets of sections over affine opens. Then for any quasi-compact open U ⊆ X and any perfect object E of D(𝒪_X) the sets H^i(U, K ⊗^L E) and Ext^i(E|_U, K|_U) are countable.

Quasi-compactness of X is not used, so it is not assumed: the statement holds on every quasi-separated scheme. H^i(U, -) is the cohomology of the right derived functor of sections over U (derivedSectionsOpen), ⊗^L is the derived tensor product of D(𝒪_X), perfectness is that of [Stacks, Tag 08CM], E|_U and K|_U are the restrictions along the open immersion U ⟶ X, and Ext^i is the group of degree-i morphisms in D(𝒪_U).

theorem countable_cohomology_derivedTensor_and_ext_of_isCompact [QuasiSeparatedSpace X]
    (K : DerivedCategory X.Modules)
    (hK : ∀ i : ℤ, ((DerivedCategory.homologyFunctor X.Modules i).obj K).IsQuasicoherent)
    (hKc : ∀ V : X.Opens, IsAffineOpen V → ∀ i : ℤ,
      Countable Γ((DerivedCategory.homologyFunctor X.Modules i).obj K, V))
    (U : X.Opens) (hU : IsCompact (U : Set X)) (E : DerivedCategory X.Modules)
    (hE : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace) E) (i : ℤ) :
    Countable ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} i).obj
        ((derivedSectionsOpen X.toRingedSpace U).obj
          (((Stacks.SheafOfModules.derivedTensor X.sheaf).obj K).obj E))) ∧
      Countable (ShiftedHom ((Scheme.Modules.restrictFunctor U.ι).mapDerivedCategory.obj E)
        ((Scheme.Modules.restrictFunctor U.ι).mapDerivedCategory.obj K) i)

Stacks.Cohomology.CountableSections.countable_cohomology_derivedTensor_of_isCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/CountableOverQuasiCompactOpens.lean, line 178. The attribute's comment: “countability of H^i(U, K ⊗^L E) over every quasi-compact open, from countable sections of the cohomology sheaves of K ⊗^L E over affine opens. Two inputs are hypotheses rather than proved. First, that the cohomology of an affine open is the sections of the cohomology sheaves there: the library has this only at another model of the derived category. Second, that the cohomology sheaves of K ⊗^L E inherit countable sections over affine opens from those of K when E is perfect, which is why perfectness of E does not appear. The Ext^i(E|_U, K|_U) half is not covered: it needs the isomorphism K ⊗^L E^∨ ≅ RHom(E, K) for perfect E, which is unproved here”.

Let X be a quasi-separated scheme and let K and E be objects of D(𝒪_X). Suppose the cohomology sheaves of K ⊗^L E have countable sets of sections over affine opens, and that over an affine open the cohomology of K ⊗^L E is computed by those sections. Then for every quasi-compact open U the set H^i(U, K ⊗^L E) is countable.

theorem countable_cohomology_derivedTensor_of_isCompact (X : Scheme.{u}) [QuasiSeparatedSpace X]
    (K E : DerivedCategory (ModuleSheaves X.toRingedSpace))
    (hsections : ∀ (V : X.Opens), IsAffineOpen V → ∀ i : ℤ,
      Countable ((cohomologySheafSectionsOpen X.toRingedSpace V i).obj
        (((Stacks.Cohomology.TorAmplitude.derTensor X.toRingedSpace).tensor.obj K).obj E)))
    (hcomparison : ∀ (V : X.Opens), IsAffineOpen V → ∀ i : ℤ,
      Nonempty ((cohomologyOpen X.toRingedSpace V i).obj
          (((Stacks.Cohomology.TorAmplitude.derTensor X.toRingedSpace).tensor.obj K).obj E) ≅
        (cohomologySheafSectionsOpen X.toRingedSpace V i).obj
          (((Stacks.Cohomology.TorAmplitude.derTensor X.toRingedSpace).tensor.obj K).obj E)))
    (U : X.Opens) (hU : IsCompact (U : Set X)) (i : ℤ) :
    Countable ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} i).obj
      ((derivedSectionsOpen X.toRingedSpace U).obj
        (((Stacks.Cohomology.TorAmplitude.derTensor X.toRingedSpace).tensor.obj K).obj E)))

Tag 0CRQ, a lemma

Tag 0CRQ in the Stacks Project.

Stacks.Cohomology.CountableSections.exists_isHomotopyColimit_isPerfect_iff_countable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/CountablePerfectHomotopyColimit.lean, line 395.

[Stacks, Tag 0CRQ]. Let X be a quasi-compact and quasi-separated scheme such that the sets of sections of 𝒪_X over affine opens are countable. Let K be an object of D_QCoh(𝒪_X). The following are equivalent:

1. K = hocolim Eₙ with Eₙ a perfect object of D(𝒪_X), and
2. the cohomology sheaves H^i(K) have countable sets of sections over affine opens.

hocolim is the derived colimit of [Stacks, Tag 090Z], perfectness is that of [Stacks, Tag 08CM], and the derived category is an arbitrary model of D(𝒪_X).

theorem exists_isHomotopyColimit_isPerfect_iff_countable {X : Scheme.{u}} [CompactSpace X]
    [QuasiSeparatedSpace X] [h : HasDerivedCategory.{w} X.Modules]
    (hO : ∀ V : X.Opens, IsAffineOpen V → Countable Γ(X, V))
    (K : DerivedCategory X.Modules)
    (hK : ∀ i : ℤ, ((DerivedCategory.homologyFunctor X.Modules i).obj K).IsQuasicoherent) :
    (∃ F : ℕ ⥤ DerivedCategory X.Modules,
      (∀ n, @Stacks.Cohomology.PerfectComplexes.IsPerfect X.toRingedSpace h (F.obj n)) ∧
        IsHomotopyColimit F K) ↔
      ∀ V : X.Opens, IsAffineOpen V → ∀ i : ℤ,
        Countable Γ((DerivedCategory.homologyFunctor X.Modules i).obj K, V)

Tag 0CRR, a lemma

Tag 0CRR in the Stacks Project.

Stacks.Cohomology.CountableSections.exists_isHomotopyColimitWith_derivedGlobalSectionsOver_derivedSheafHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/FlatPushforwardHomHomotopyColimit.lean, line 107. The attribute's comment: “(1)”.

Let A be a ring, X a scheme of finite presentation over A (p : X ⟶ Spec A) and f : U ⟶ X flat of finite presentation. There are an inverse system L : ℕᵒᵖ ⥤ D(𝒪_X) of perfect objects and maps

dₙ : RΓ(X, R𝓗om(Lₙ, -)) ⟶ RΓ(U, Lf^* -)

of functors D(𝒪_X) ⥤ D(A), compatible with the transition maps, such that for every K in D_QCoh(𝒪_X) the maps dₙ at K exhibit

RΓ(U, Lf^* K) = hocolim RΓ(X, R𝓗om(Lₙ, K)) = hocolim R Hom_X(Lₙ, K)

in D(A). The system L and the maps dₙ do not depend on K, and dₙ is natural in K: this is the source's "functorially in K in D_QCoh(𝒪_X)". Here RΓ(X, -) is the derived global sections functor into D(A), R𝓗om the derived internal Hom, Lf^* the derived pullback of [Stacks, Tag 06YJ], and hocolim the derived colimit of [Stacks, Tag 090Z].

Stated at HasDerivedCategory.standard, scoped to this declaration: part (2), biduality and [Stacks, Tag 08DQ] exist only at that model.

theorem exists_isHomotopyColimitWith_derivedGlobalSectionsOver_derivedSheafHom
    [LocallyOfFinitePresentation p] [QuasiCompact p] [QuasiSeparated p]
    [Flat f] [LocallyOfFinitePresentation f] [QuasiCompact f] [QuasiSeparated f] :
    ∃ (L : ℕᵒᵖ ⥤ DerivedCategory X.Modules)
      (d : ∀ n, (Stacks.SheafOfModules.derivedSheafHom X.sheaf).obj (op (L.obj (op n))) ⋙
          derivedGlobalSectionsOver p ⟶
        Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback f.toLRSHom.toShHom ⋙
          derivedGlobalSectionsOver (f ≫ p)),
      (∀ n, Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace) (L.obj (op n))) ∧
      (∀ n, Functor.whiskerRight ((Stacks.SheafOfModules.derivedSheafHom X.sheaf).map
          (L.map (homOfLE (Nat.le_succ n)).op).op) (derivedGlobalSectionsOver p) ≫ d (n + 1) =
          d n) ∧
      ∀ K : DerivedCategory X.Modules,
        (∀ i : ℤ, ((DerivedCategory.homologyFunctor X.Modules i).obj K).IsQuasicoherent) →
        IsHomotopyColimitWith
          (L.rightOp ⋙ (Stacks.SheafOfModules.derivedSheafHom X.sheaf).flip.obj K ⋙
            derivedGlobalSectionsOver p)
          ((derivedGlobalSectionsOver (f ≫ p)).obj
            ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
              f.toLRSHom.toShHom).obj K))
          (fun n => (d n).app K)

Stacks.Cohomology.CountableSections.exists_isHomotopyColimitWith_derivedGlobalSectionsOver_derivedTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/FlatPushforwardSectionsHomotopyColimit.lean, line 306. The attribute's comment: “(2)”.

[Stacks, Tag 0CRR] (2). Let A be a ring, X a scheme of finite presentation over A and f : U ⟶ X a flat morphism of finite presentation. Then there is a system E : ℕ ⥤ D(𝒪_X) of perfect objects such that

RΓ(U, Lf^* K) = hocolim RΓ(X, K ⊗^𝐋 Eₙ)

in D(A), functorially in K in D_QCoh(𝒪_X): there are maps cₙ : RΓ(X, - ⊗^𝐋 Eₙ) ⟶ RΓ(U, Lf^* -), natural in K and compatible with the transitions of the system, which for every K with quasi-coherent cohomology are the coprojections of a derived colimit. One system E serves every K.

RΓ(X, -) and RΓ(U, -) are the A-linear derived global sections along X ⟶ Spec A and U ⟶ X ⟶ Spec A, ⊗^𝐋 is the derived tensor product of [Stacks, Tag 06YU], Lf^* the derived pullback of [Stacks, Tag 06YJ], and hocolim the derived colimit of [Stacks, Tag 090Z].

Stated at HasDerivedCategory.standard, scoped to this declaration: the projection formula ([Stacks, Tag 08EU]), Tor independent base change ([Stacks, Tag 08IB]) and the Leray isomorphism exist only at that model.

theorem exists_isHomotopyColimitWith_derivedGlobalSectionsOver_derivedTensor
    [LocallyOfFinitePresentation p] [QuasiCompact p] [QuasiSeparated p]
    [Flat f] [LocallyOfFinitePresentation f] [QuasiCompact f] [QuasiSeparated f] :
    ∃ (E : ℕ ⥤ DerivedCategory X.Modules)
      (c : ∀ n, (Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor
          X.toRingedSpace.sheaf).flip.obj (E.obj n) ⋙ derivedGlobalSectionsOver p ⟶
        Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback f.toLRSHom.toShHom ⋙
          derivedGlobalSectionsOver (f ≫ p)),
      (∀ n, Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace) (E.obj n)) ∧
      (∀ n, Functor.whiskerRight ((Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor
          X.toRingedSpace.sheaf).flip.map (E.map (homOfLE (Nat.le_succ n))))
          (derivedGlobalSectionsOver p) ≫ c (n + 1) = c n) ∧
      ∀ K : DerivedCategory X.Modules,
        (∀ i : ℤ, ((DerivedCategory.homologyFunctor X.Modules i).obj K).IsQuasicoherent) →
        IsHomotopyColimitWith
          (E ⋙ (Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor
            X.toRingedSpace.sheaf).obj K ⋙ derivedGlobalSectionsOver p)
          ((derivedGlobalSectionsOver (f ≫ p)).obj
            ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
              f.toLRSHom.toShHom).obj K))
          (fun n => (c n).app K)

Sources

• Section 36.33, Tag 0CRN
• AxiomMath/Stacks at 5ed82d14

LeanStacks.AlgebraicGeometry.CoherentBaseCohomology.isCoherent_cohomology_of_isPerfect_derivedGlobalSections · Stacks.AlgebraicGeometry.CoherentBaseCohomology.isCoherent_rightDerived_moduleGlobalSections · Stacks.Cohomology.CountableSections.countable_cohomology_derivedTensor_and_ext_of_isCompact · Stacks.Cohomology.CountableSections.countable_cohomology_derivedTensor_of_isCompact · Stacks.Cohomology.CountableSections.exists_isHomotopyColimit_isPerfect_iff_countable · Stacks.Cohomology.CountableSections.exists_isHomotopyColimitWith_derivedGlobalSectionsOver_derivedSheafHom · Stacks.Cohomology.CountableSections.exists_isHomotopyColimitWith_derivedGlobalSectionsOver_derivedTensor

Section36.34 Characterizing pseudo-coherent complexes, II#

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

Tag 0CSF, a lemma

Tag 0CSF in the Stacks Project.

StacksDraft.PseudoCoherence.exists_boundedAboveFiniteFree_of_isPseudoCoherent_restrictScalars, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RestrictScalars/FiniteFreeAlgebra.lean, line 104.

Stacks 0CSF. If a derived right R-module is pseudo-coherent over A, where R is a possibly noncommutative A-algebra which is finite free over A, then it is represented by a bounded-above complex of finite free right R-modules.

theorem exists_boundedAboveFiniteFree_of_isPseudoCoherent_restrictScalars
    (A : Type uA) (R : Type uR) [CommRing A] [Ring R] [Algebra A R]
    (M : DerivedCategory (ModuleCat.{max uA uR v} Rᵐᵒᵖ))
    (hR : Module.Finite A R ∧ Module.Free A R)
    (hM : ∀ m : ℤ, IsPseudoCoherentFrom
      ((ModuleCat.restrictScalars.{max uA uR v} (algebraMap A Rᵐᵒᵖ)).mapDerivedCategory.obj M)
      m) :
    ∃ E : CochainComplex (ModuleCat.{max uA uR v} Rᵐᵒᵖ) ℤ,
      IsBoundedAboveFiniteFree E ∧ Nonempty (DerivedCategory.Q.obj E ≅ M)

Tag 0CSG, a lemma

Tag 0CSG in the Stacks Project.

AlgebraicGeometry.ProjectiveSpacePseudoCoherent.isPseudoCoherent_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ProjectiveSpacePseudoCoherent/Equivalences.lean, line 61.

[Stacks, Tag 0CSG]. Let A be a ring, n ≥ 0 and K ∈ D_QCoh(𝒪_{ℙⁿ_A}). The following are equivalent: 1. K is pseudo-coherent; 2. RΓ(ℙⁿ_A, E ⊗^𝐋 K) is a pseudo-coherent object of D(A) for each pseudo-coherent E of D(𝒪_{ℙⁿ_A}); 3. RΓ(ℙⁿ_A, E ⊗^𝐋 K) is a pseudo-coherent object of D(A) for each perfect E; 4. RHom_{ℙⁿ_A}(E, K) = RΓ(ℙⁿ_A, R𝓗om(E, K)) is a pseudo-coherent object of D(A) for each perfect E; 5. RΓ(ℙⁿ_A, K ⊗^𝐋 𝒪(d)) is a pseudo-coherent object of D(A) for d = 0, 1, …, n.

theorem isPseudoCoherent_tfae :
    letI : HasDerivedCategory (Proj (polyGrading A n)).Modules := HasDerivedCategory.standard _
    letI : HasDerivedCategory (StrictlyPerfect.OXMod (Proj (polyGrading A n)).toRingedSpace) :=
      HasDerivedCategory.standard _
    letI : HasDerivedCategory
        (Stacks.DerivedTensor.RingedSite.Modules (Proj (polyGrading A n)).sheaf) :=
      HasDerivedCategory.standard _
    letI : HasDerivedCategory (ModuleCat.{u} A) := HasDerivedCategory.standard _
    ∀ K : DerivedCategory (Proj (polyGrading A n)).Modules, quasicoherentObject A n K →
      List.TFAE
        [RingedSpace.IsPseudoCoherent (X := (Proj (polyGrading A n)).toRingedSpace) K,
          ∀ E : DerivedCategory (Proj (polyGrading A n)).Modules,
            RingedSpace.IsPseudoCoherent (X := (Proj (polyGrading A n)).toRingedSpace) E →
              StacksDraft.PseudoCoherence.IsPseudoCoherent
                ((derivedGlobalSectionsOver (projToSpecCoeff A n)).obj
                  (((derivedTensorProductFunctor (Proj (polyGrading A n)).sheaf).obj E).obj K)),
          ∀ E : DerivedCategory (Proj (polyGrading A n)).Modules,
            Stacks.Cohomology.PerfectComplexes.IsPerfect
                (X := (Proj (polyGrading A n)).toRingedSpace) E →
              StacksDraft.PseudoCoherence.IsPseudoCoherent
                ((derivedGlobalSectionsOver (projToSpecCoeff A n)).obj
                  (((derivedTensorProductFunctor (Proj (polyGrading A n)).sheaf).obj E).obj K)),
          ∀ E : DerivedCategory (Proj (polyGrading A n)).Modules,
            Stacks.Cohomology.PerfectComplexes.IsPerfect
                (X := (Proj (polyGrading A n)).toRingedSpace) E →
              StacksDraft.PseudoCoherence.IsPseudoCoherent
                ((derivedGlobalSectionsOver (projToSpecCoeff A n)).obj
                  (((Stacks.SheafOfModules.derivedSheafHom (Proj (polyGrading A n)).sheaf).obj
                    (Opposite.op E)).obj K)),
          ∀ d : Fin (n + 1), StacksDraft.PseudoCoherence.IsPseudoCoherent
            ((derivedGlobalSectionsOver (projToSpecCoeff A n)).obj
              (((derivedTensorProductFunctor (Proj (polyGrading A n)).sheaf).obj K).obj
                ((DerivedCategory.singleFunctor (Proj (polyGrading A n)).Modules 0).obj
                  (ProjectiveSpectrum.Proj.twistingSheaf (polyGrading A n) d))))]

Tag 0CSH, a lemma

Tag 0CSH in the Stacks Project.

AlgebraicGeometry.isPseudoCoherent_derivedGlobalSectionsOver_tensor_of_isPseudoCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/PerfectApproximation/DerivedSectionsTensorPseudoCoherence.lean, line 370.

[Stacks, Tag 0CSH]. Let A be a ring, let X be a quasi-compact and quasi-separated scheme over A (the structure morphism being f : X ⟶ Spec A), and let K ∈ D^-_QCoh(𝒪_X), i.e. K has quasi-coherent cohomology sheaves vanishing in all sufficiently large degrees. If RΓ(X, E ⊗^𝐋 K) is pseudo-coherent in D(A) for every perfect E in D(𝒪_X), then RΓ(X, E ⊗^𝐋 K) is pseudo-coherent in D(A) for every pseudo-coherent E in D(𝒪_X).

The proof is the source's: by [Stacks, Tag 08ES] a pseudo-coherent E is approximated, in any given degree, by a perfect P ⟶ E whose cone C has no cohomology from that degree on; tensoring with K raises the vanishing bound by an upper bound b of the cohomology of K and keeps it in D_QCoh ([Stacks, Tag 08DX]); RΓ(X, -) raises it by its cohomological dimension N ([Stacks, Tag 08D5]); so RΓ(X, P ⊗^𝐋 K) ⟶ RΓ(X, E ⊗^𝐋 K) is an isomorphism in high degrees and the pseudo-coherence of its source passes to its target degree by degree.

theorem isPseudoCoherent_derivedGlobalSectionsOver_tensor_of_isPseudoCoherent
    [CompactSpace X] [QuasiSeparatedSpace X]
    (K : DerivedCategory (StructureSheafModules X.sheaf))
    (hK : ∀ i : ℤ, ((DerivedCategory.homologyFunctor (StructureSheafModules X.sheaf) i).obj
      K).IsQuasicoherent)
    (hKb : ∃ b : ℤ, ∀ i : ℤ, b < i →
      IsZero ((DerivedCategory.homologyFunctor (StructureSheafModules X.sheaf) i).obj K))
    (hpc : ∀ E : DerivedCategory (StructureSheafModules X.sheaf),
      Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace) E →
        StacksDraft.PseudoCoherence.IsPseudoCoherent
          ((derivedGlobalSectionsOver f).obj (((derivedTensor X.sheaf).obj E).obj K)))
    (E : DerivedCategory (StructureSheafModules X.sheaf))
    (hE : RingedSpace.IsPseudoCoherent (X := X.toRingedSpace) E) :
    StacksDraft.PseudoCoherence.IsPseudoCoherent
      ((derivedGlobalSectionsOver f).obj (((derivedTensor X.sheaf).obj E).obj K))

Sources

• Section 36.34, Tag 0CSE
• AxiomMath/Stacks at 5ed82d14

LeanStacksDraft.PseudoCoherence.exists_boundedAboveFiniteFree_of_isPseudoCoherent_restrictScalars · AlgebraicGeometry.ProjectiveSpacePseudoCoherent.isPseudoCoherent_tfae · AlgebraicGeometry.isPseudoCoherent_derivedGlobalSectionsOver_tensor_of_isPseudoCoherent

Section36.35 Relatively perfect objects#

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

Tag 0DHZ, the section

Tag 0DHZ in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.IsPerfectRelativeTo, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectObject.lean, line 83. The attribute's comment: “the notion of a relatively perfect object, for a morphism flat and locally of finite presentation, generalised to an arbitrary family of certificates”. References: SGA 6 III (4.1), “flat, l.f.p. case”.

A generalisation of Stacks 0DI0. An object E of D(𝒪_X) is perfect relative to S when it is pseudo-coherent and, after restriction of scalars along f^{-1}𝒪_S ⟶ 𝒪_X, locally has finite Tor dimension on the inverse-image ringed space (X, f^{-1}𝒪_S).

The derived tensor product is read off the family of certificates D, one on each open subspace of the inverse-image ringed space, as in part (3) of Stacks 08CG. Since the underived half of a certificate is free data, this is weaker than Stacks 0DI0 at a general D, and it is Stacks 0DI0 — AlgebraicGeometry.Scheme.Hom.IsRelativelyPerfect — exactly when D is pinned to the tensor product of sheaves of modules; see AlgebraicGeometry.Scheme.Hom.isPerfectRelativeTo_iff_isRelativelyPerfect.

public def IsPerfectRelativeTo [Flat f] [LocallyOfFinitePresentation f]
    (D : ∀ U : TopologicalSpace.Opens
        (RingedSpace.inverseImage S.toRingedSpace f.base).carrier,
      RingedSpace.CertifiedDerivedSheafTensoring.{d', u}
        ((RingedSpace.inverseImage S.toRingedSpace f.base).restrict U.isOpenEmbedding))
    (E : DerivedCategory (OXMod.{u, u} X.toRingedSpace)) : Prop

Tag 0DI0, a definition

Tag 0DI0 in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.IsRelativelyPerfect, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectObjectCanonical.lean, line 90.

An object E of D(𝒪_X) is perfect relative to S when it is pseudo-coherent and, after restriction of scalars along f^{-1}𝒪_S ⟶ 𝒪_X, locally has finite Tor dimension on the inverse-image ringed space (X, f^{-1}𝒪_S).

Pseudo-coherence is part (3) of Stacks 08CB, and local finiteness of the Tor dimension is part (3) of Stacks 08CG taken against the derived tensor product - ⊗^{L}_{f^{-1}𝒪_S} - of Stacks 06YU on each open subspace, the total left derived functor of the tensor product of sheaves of modules.

public def IsRelativelyPerfect [Flat f] [LocallyOfFinitePresentation f]
    (E : DerivedCategory (OXMod.{u, u} X.toRingedSpace)) : Prop

Tag 0DI1, an example

Tag 0DI1 in the Stacks Project.

AlgebraicGeometry.isPerfectRelativeTo_dualNumberResidueComplex_and_not_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectNotFibrewise.lean, line 149. The attribute's comment: “relative perfectness over a field is not perfectness on the fibres”.

Stacks 0DI1, the closing warning. Over a field, relative perfectness is not perfectness on the fibres: the residue field of the dual numbers, sheafified and placed in degree zero, is Spec k-perfect on the scheme Spec k[ε] — which is of finite presentation over k, and whose only fibre over Spec k is itself — and it is not a perfect object of D(𝒪_{Spec k[ε]}).

The first half is Stacks 0DI1 itself, AlgebraicGeometry.isPerfectRelativeTo_canonical_iff_boundedCoherent, applied to a coherent module in degree zero. The second is Stacks 08EB, AlgebraicGeometry.isPerfect_tilde_iff, against AlgebraicGeometry.not_isPerfectModule_residueField_dualNumber.

public theorem isPerfectRelativeTo_dualNumberResidueComplex_and_not_isPerfect (k : Type u)
    [Field k] :
    (dualNumberStructureMap k).IsPerfectRelativeTo
        (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily
          (RingedSpace.inverseImage (Spec (CommRingCat.of k)).toRingedSpace
            (dualNumberStructureMap k).base))
        (dualNumberResidueComplex k) ∧
      ¬ Stacks.Cohomology.PerfectComplexes.IsPerfect
          (X := (Spec (CommRingCat.of (DualNumber k))).toRingedSpace)
          (dualNumberResidueComplex k)

AlgebraicGeometry.isBounded_and_isPseudoCoherent_iff_boundedCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectOverField.lean, line 461. The attribute's comment: “bounded pseudo-coherent objects are the bounded coherent ones”.

Stacks 0DI1, second equivalence, via Stacks 08E8. On a Noetherian scheme an object of D(𝒪_X) is bounded and pseudo-coherent if and only if it lies in D^b_Coh(𝒪_X), that is, if and only if it is bounded and all of its cohomology sheaves are coherent.

Together with AlgebraicGeometry.isPerfectRelativeTo_canonical_iff_isBounded_and_isPseudoCoherent and AlgebraicGeometry.isNoetherian_of_finitePresentation_over_field this identifies the objects of D(𝒪_X) perfect relative to a field with D^b_Coh(𝒪_X); see AlgebraicGeometry.isPerfectRelativeTo_canonical_iff_boundedCoherent.

Stacks 08E8 cuts D^b_Coh(𝒪_X) out inside D_QCoh(𝒪_X), and both sides here imply quasi-coherence of the cohomology sheaves: on the left it is Stacks 08E5 for a pseudo-coherent object, AlgebraicGeometry.isQuasicoherentDerived_of_isPseudoCoherent, and on the right it is Stacks 01BW, isQuasicoherent_of_isCoherent, applied degreewise.

public theorem isBounded_and_isPseudoCoherent_iff_boundedCoherent (X : Scheme.{u})
    [IsNoetherian X] (E : DerivedCategory (OXMod.{u, u} X.toRingedSpace)) :
    (DerivedCategoryB.IsBounded E ∧ RingedSpace.IsPseudoCoherent E) ↔
      DerivedCategoryB.derivedCategoryBBounded
        (fun M : OXMod.{u, u} X.toRingedSpace => M.IsCoherent) E

AlgebraicGeometry.isPerfectRelativeTo_canonical_iff_isBounded_and_isPseudoCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectOverField.lean, line 503. The attribute's comment: “first equivalence: at the 06YU derived tensor product, relative perfectness over a field is boundedness and pseudo-coherence”.

Stacks 0DI1, first equivalence, at the genuine derived tensor product. Let k be a field and let X be a scheme of finite presentation over k. An object E of D(𝒪_X) is perfect relative to Spec k — read at the derived tensor product of Stacks 06YU on each open subspace of (X, f⁻¹𝒪_{Spec k}), which is AlgebraicGeometry.RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily — if and only if it is bounded and pseudo-coherent.

This is AlgebraicGeometry.isPerfectRelativeTo_iff_isBounded_and_isPseudoCoherent at the canonical family, whose underived operation is - ⊗_{f⁻¹𝒪_{Spec k}} - by rfl.

public theorem isPerfectRelativeTo_canonical_iff_isBounded_and_isPseudoCoherent (k : Type u)
    [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [LocallyOfFinitePresentation f]
    [QuasiCompact f] (E : DerivedCategory (OXMod.{u, u} X.toRingedSpace)) :
    f.IsPerfectRelativeTo
        (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily
          (RingedSpace.inverseImage (Spec (.of k)).toRingedSpace f.base)) E ↔
      (DerivedCategoryB.IsBounded E ∧ RingedSpace.IsPseudoCoherent E)

AlgebraicGeometry.isPerfectRelativeTo_canonical_iff_boundedCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectOverField.lean, line 523. The attribute's comment: “the Spec k-perfect objects are exactly D^b_Coh(𝒪_X)”.

Stacks 0DI1. Let k be a field and let X be a scheme of finite presentation over k. An object E of D(𝒪_X) is Spec k-perfect if and only if it lies in D^b_Coh(𝒪_X), that is, if and only if it is bounded with coherent cohomology sheaves.

This is the example in one statement: relative perfectness is read at the derived tensor product of Stacks 06YU, and the cohomology sheaves are quasi-coherent by Stacks 08E5 and 01BW. It is the composite of AlgebraicGeometry.isPerfectRelativeTo_canonical_iff_isBounded_and_isPseudoCoherent with AlgebraicGeometry.isBounded_and_isPseudoCoherent_iff_boundedCoherent, the scheme being Noetherian by AlgebraicGeometry.isNoetherian_of_finitePresentation_over_field.

public theorem isPerfectRelativeTo_canonical_iff_boundedCoherent (k : Type u) [Field k]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [LocallyOfFinitePresentation f] [QuasiCompact f]
    (E : DerivedCategory (OXMod.{u, u} X.toRingedSpace)) :
    f.IsPerfectRelativeTo
        (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily
          (RingedSpace.inverseImage (Spec (.of k)).toRingedSpace f.base)) E ↔
      DerivedCategoryB.derivedCategoryBBounded
        (fun M : OXMod.{u, u} X.toRingedSpace => M.IsCoherent) E

Tag 0DI2, a lemma

Tag 0DI2 in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.isPerfectRelativeTo_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectAffineCriterion.lean, line 72.

Stacks 0DI2. Let f : X ⟶ S be a morphism of schemes which is flat and locally of finite presentation, and let E be an object of the derived category of 𝒪_X-modules all of whose cohomology sheaves are quasi-coherent. The following are equivalent:

1. E is S-perfect;
2. for every affine open U ⊆ X mapping into an affine open V ⊆ S, the complex RΓ(U, E) is 𝒪_S(V)-perfect;
3. there are an affine open covering S = ⋃ V i and, for each i, an affine open covering f⁻¹(V i) = ⋃ U i j such that RΓ(U i j, E) is 𝒪_S(V i)-perfect.

S-perfectness is read at the derived tensor product of Stacks 06YU on the open subspaces of (X, f⁻¹𝒪_S), and 𝒪_S(V)-perfectness of RΓ(U, E) is Stacks 0DHS for the chart ring map f.appLE V U e, which is flat and of finite presentation.

public theorem isPerfectRelativeTo_tfae [Flat f] [LocallyOfFinitePresentation f]
    (E : DerivedCategory X.Modules)
    (hE : ∀ i : ℤ, ((DerivedCategory.homologyFunctor X.Modules i).obj E).IsQuasicoherent) :
    List.TFAE
      [IsPerfectRelativeTo f
          (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily
            (RingedSpace.inverseImage S.toRingedSpace f.base)) E,
        ∀ (U : X.Opens) (hU : IsAffineOpen U) (V : S.Opens) (hV : IsAffineOpen V)
          (e : U ≤ f ⁻¹ᵁ V), SectionsRelativelyPerfect f E hV hU e,
        ∃ (ι : Type u) (V : ι → S.affineOpens),
          (⨆ i, (V i : S.Opens)) = ⊤ ∧
            ∀ i, ∃ (κ : Type u) (U : κ → X.affineOpens) (hle : ∀ j, (U j).1 ≤ f ⁻¹ᵁ (V i).1),
              (⨆ j, (U j : X.Opens)) = f ⁻¹ᵁ (V i).1 ∧
                ∀ j, SectionsRelativelyPerfect f E (V i).2 (U j).2 (hle j)]

AlgebraicGeometry.pseudoCoherent_derivedSections_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectDerivedSections.lean, line 150. The attribute's comment: “the pseudo-coherence clause”.

Stacks 0DI2, the pseudo-coherence clause. Let f : X ⟶ S be a morphism of schemes and let E be an object of the derived category of 𝒪_X-modules all of whose cohomology sheaves are quasi-coherent. Then the following are equivalent:

1. E is a pseudo-coherent object of D(𝒪_X);
2. for every affine open U ⊆ X whose image lies in an affine open V ⊆ S, the complex of Γ(X, U)-modules RΓ(U, E) is pseudo-coherent;
3. there are an affine open covering of S and, over each of its members V i, an affine open covering of f ⁻¹ᵁ V i such that RΓ(U, E) is pseudo-coherent for each member U of the latter.

This is the first of the two clauses of relative perfectness, with the part of the source's proof that concerns it: pseudo-coherence of E is the pseudo-coherence over Γ(X, U) of RΓ(U, E), by Stacks 08E7 and the affine presentation of E|_U of Stacks 06Z0, and the condition is local on X. Together with the second clause, locally finite Tor dimension over f^{-1}𝒪_S, this is assembled into Stacks 0DI2 in AlgebraicGeometry.Scheme.Hom.isPerfectRelativeTo_tfae.

public theorem pseudoCoherent_derivedSections_tfae (f : X ⟶ S)
    (E : DerivedCategory X.Modules)
    (hE : ∀ i : ℤ, ((DerivedCategory.homologyFunctor X.Modules i).obj E).IsQuasicoherent) :
    List.TFAE
      [RingedSpace.IsPseudoCoherent (X := X.toRingedSpace) E,
        ∀ (U : X.Opens), IsAffineOpen U → ∀ (V : S.Opens), IsAffineOpen V → U ≤ f ⁻¹ᵁ V →
          StacksDraft.PseudoCoherence.IsPseudoCoherent ((derivedSectionsUnbounded X U).obj E),
        ∃ (ι : Type u) (V : ι → S.affineOpens),
          (⨆ i, (V i : S.Opens)) = ⊤ ∧
            ∀ i, ∃ (κ : Type u) (U : κ → X.affineOpens),
              (⨆ j, (U j : X.Opens)) = f ⁻¹ᵁ (V i).1 ∧
                ∀ j, StacksDraft.PseudoCoherence.IsPseudoCoherent
                  ((derivedSectionsUnbounded X (U j).1).obj E)]

AlgebraicGeometry.Scheme.Hom.exists_affineCovering_sectionsRelativelyPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectSectionsChart.lean, line 143. The attribute's comment: “the implication (2) implies (3), at the source's own module-side condition and for BOTH of its conjuncts at once: if the complex of sections over every affine open U of X mapping into an affine open V of S is O_S(V)-perfect, then there are an affine open covering of S and, over each member V, an affine open covering of the preimage of V on whose members the same condition holds. The whole three-way equivalence is AlgebraicGeometry.Scheme.Hom.isPerfectRelativeTo_tfae”.

Stacks 0DI2, the implication (2) ⟹ (3): if RΓ(U, E) is Γ(S, V)-perfect for every affine open U ⊆ X mapping into an affine open V ⊆ S, then there are an affine open covering of S and, over each of its members V, an affine open covering of f⁻¹(V) on whose members the condition holds.

public theorem exists_affineCovering_sectionsRelativelyPerfect [Flat f]
    [LocallyOfFinitePresentation f] (E : DerivedCategory X.Modules)
    (h : ∀ (U : X.Opens) (hU : IsAffineOpen U) (V : S.Opens) (hV : IsAffineOpen V)
      (e : U ≤ f ⁻¹ᵁ V), SectionsRelativelyPerfect f E hV hU e) :
    ∃ (ι : Type u) (V : ι → S.affineOpens),
      (⨆ i, (V i : S.Opens)) = ⊤ ∧
        ∀ i, ∃ (κ : Type u) (U : κ → X.affineOpens) (hle : ∀ j, (U j).1 ≤ f ⁻¹ᵁ (V i).1),
          (⨆ j, (U j : X.Opens)) = f ⁻¹ᵁ (V i).1 ∧
            ∀ j, SectionsRelativelyPerfect f E (V i).2 (U j).2 (hle j)

AlgebraicGeometry.Scheme.Hom.chartHasFiniteTorDimension_of_locallyHasFiniteTorDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/TorDimensionNestedRestriction.lean, line 266. The attribute's comment: “the Tor-dimension clause, the implication (1) implies (2): if E locally has finite Tor dimension over f^{-1}O_S then its restriction to every affine open U of X has finite Tor dimension over f^{-1}O_S, for the derived tensor product of Stacks 06YU. The whole three-way equivalence, at the source's module-side conditions, is AlgebraicGeometry.Scheme.Hom.isPerfectRelativeTo_tfae”.

The implication (1) ⟹ (2) of the Tor-dimension clause of Stacks 0DI2. If E locally has finite Tor dimension over f⁻¹𝒪_S, then for every affine open U ⊆ X the restriction E|_U has finite Tor dimension over f⁻¹𝒪_S.

The three steps are: the certificate-carrying predicate at the canonical family is the pinned one (AlgebraicGeometry.RingedSpace.locallyHasFiniteTorDimension_canonicalCertificate_iff, which is Iff.rfl); locally finite Tor dimension is inherited by X|_U (Stacks.Cohomology.TorAmplitude.locallyHasFiniteTorDimension_derivedRestrictModules); and on X|_U, which is quasi-compact because U is affine, locally finite Tor dimension is finite Tor dimension (locallyHasFiniteTorDimension_iff_hasFiniteTorDimension of AlgebraicGeometry.AffineRelativeTorAmplitude).

The certificate family is named, not quantified. Unlike the two implications into condition (1) of AlgebraicGeometry.Scheme.Hom.locallyHasFiniteTorDimension_of_forall_chart and AlgebraicGeometry.Scheme.Hom.locallyHasFiniteTorDimension_of_exists_affineCovering, this implication is not available for an arbitrary family: the premise is tested against the certificates at the members of some covering and the conclusion against the certificate at U, and a family carries no relation between its members, so at an arbitrary family the two sides measure Tor amplitude against unrelated operations. It is stated at the genuine derived tensor product of Stacks 06YU, which is what the source means; a consumer holding another family with the same underived halves may use AlgebraicGeometry.RingedSpace.locallyHasFiniteTorDimension_iff_of_tensor_eq.

Affineness is used only through quasi-compactness, so the statement holds verbatim for a quasi-compact open; it is stated for an affine open because that is the chart condition of the source. The affine open V ⊆ S that clause (2) asks the chart to map into does not appear, because the sheaf-side condition does not refer to it; its module-side counterpart AlgebraicGeometry.Scheme.Hom.SectionsRelativelyPerfect does.

theorem chartHasFiniteTorDimension_of_locallyHasFiniteTorDimension
    (E : DerivedCategory (OXMod.{u, u} X.toRingedSpace))
    (h : RingedSpace.LocallyHasFiniteTorDimension
      (RingedSpace.inverseImage S.toRingedSpace f.base)
      (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily
        (RingedSpace.inverseImage S.toRingedSpace f.base))
      ((derivedScalarRestriction f).obj E))
    (U : TopologicalSpace.Opens
      (RingedSpace.inverseImage S.toRingedSpace f.base).carrier)
    (hU : IsAffineOpen (X := X) U) :
    ChartHasFiniteTorDimension f
      (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily
        (RingedSpace.inverseImage S.toRingedSpace f.base)) E U

Tag 0DI3, a lemma

Tag 0DI3 in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.isClosedUnderIsomorphisms_isPerfectRelativeTo_canonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectTriangulatedCanonical.lean, line 227. The attribute's comment: “the strict fullness clause, at the genuine derived tensor product”.

Stacks 0DI3. Strict fullness of the S-perfect objects, at the derived tensor product of Stacks 06YU.

This is AlgebraicGeometry.Scheme.Hom.isClosedUnderIsomorphisms_isPerfectRelativeTo, which holds for an arbitrary certificate family, read at the canonical one.

public theorem isClosedUnderIsomorphisms_isPerfectRelativeTo_canonical :
    (isPerfectRelativeTo f
      (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily
        (RingedSpace.inverseImage S.toRingedSpace f.base))).IsClosedUnderIsomorphisms

AlgebraicGeometry.Scheme.Hom.isSaturated_isPerfectRelativeTo_canonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectTriangulatedCanonical.lean, line 239. The attribute's comment: “the saturation clause, at the genuine derived tensor product”.

Stacks 0DI3. Saturation of the S-perfect objects, at the derived tensor product of Stacks 06YU: a direct summand of an S-perfect object is S-perfect.

This is AlgebraicGeometry.Scheme.Hom.isSaturated_isPerfectRelativeTo, which holds for an arbitrary certificate family, read at the canonical one.

public theorem isSaturated_isPerfectRelativeTo_canonical :
    (isPerfectRelativeTo f
      (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily
        (RingedSpace.inverseImage S.toRingedSpace f.base))).IsSaturated

AlgebraicGeometry.Scheme.Hom.isTriangulated_isPerfectRelativeTo_canonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectTriangulatedCanonical.lean, line 264. The attribute's comment: “the triangulated clause, at the genuine derived tensor product”.

Stacks 0DI3. For a flat, locally finitely presented morphism f : X ⟶ S of schemes, the S-perfect objects of D(𝒪_X) — read at the derived tensor product of Stacks 06YU on each open subspace of (X, f^{-1}𝒪_S), which is AlgebraicGeometry.RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily — form a triangulated subcategory: the property contains the zero object, is stable under all shifts, and is closed under extensions.

This is AlgebraicGeometry.Scheme.Hom.isTriangulated_isPerfectRelativeTo at the canonical family: there each - ⊗^{L} ℱ[0] commutes with the shift and is exact, these being fields of the derived tensor product, and finite Tor dimension restricts to smaller opens by Tag 09U8 at the inclusion of one open subspace in another.

The other two assertions of Stacks 0DI3 — strict fullness and saturation — hold for an arbitrary certificate family, and are AlgebraicGeometry.Scheme.Hom.isClosedUnderIsomorphisms_isPerfectRelativeTo and AlgebraicGeometry.Scheme.Hom.isSaturated_isPerfectRelativeTo; at the canonical family they are AlgebraicGeometry.Scheme.Hom.isClosedUnderIsomorphisms_isPerfectRelativeTo_canonical and AlgebraicGeometry.Scheme.Hom.isSaturated_isPerfectRelativeTo_canonical.

public theorem isTriangulated_isPerfectRelativeTo_canonical :
    (isPerfectRelativeTo f
      (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily
        (RingedSpace.inverseImage S.toRingedSpace f.base))).IsTriangulated

AlgebraicGeometry.Scheme.Hom.isSaturated_and_isTriangulated_isPerfectRelativeTo_canonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectTriangulatedCanonical.lean, line 279. The attribute's comment: “the whole statement: for f flat and locally of finite presentation, the S-perfect objects of D(O_X) form a strictly full, saturated, triangulated subcategory”.

Stacks 0DI3. Let f : X ⟶ S be a morphism of schemes which is flat and locally of finite presentation. The S-perfect objects of D(𝒪_X), read at the derived tensor product of Stacks 06YU on each open subspace of (X, f^{-1}𝒪_S), form a strictly full, saturated, triangulated subcategory of D(𝒪_X).

public theorem isSaturated_and_isTriangulated_isPerfectRelativeTo_canonical :
    (isPerfectRelativeTo f
        (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily
          (RingedSpace.inverseImage S.toRingedSpace f.base))).IsClosedUnderIsomorphisms ∧
      (isPerfectRelativeTo f
        (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily
          (RingedSpace.inverseImage S.toRingedSpace f.base))).IsSaturated ∧
      (isPerfectRelativeTo f
        (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily
          (RingedSpace.inverseImage S.toRingedSpace f.base))).IsTriangulated

Tag 0DI4, a lemma

Tag 0DI4 in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.isPerfectRelativeTo_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectPerfectObjects.lean, line 333. The attribute's comment: “a perfect object is perfect relative to the base”.

For a flat, locally finitely presented morphism of schemes f : X ⟶ S, every perfect object of D(𝒪_X) is perfect relative to S.

public theorem isPerfectRelativeTo_of_isPerfect
    (hamp : FlatRepresentativeBounds f D) (hflat : ScalarRestrictionFlat f)
    (E : DerivedCategory (OXMod.{u, u} X.toRingedSpace)) (hE : RingedSpace.IsPerfect E) :
    f.IsPerfectRelativeTo D E

AlgebraicGeometry.Scheme.Hom.isPerfectRelativeTo_derivedTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectPerfectObjects.lean, line 503. The attribute's comment: “tensoring an S-perfect object with a perfect object”.

For a flat, locally finitely presented morphism of schemes f : X ⟶ S, the derived tensor product of a perfect object K of D(𝒪_X) with an S-perfect object M is perfect relative to S.

public theorem isPerfectRelativeTo_derivedTensor
    (hrestricts : RingedSpace.FiniteTorDimensionRestricts
      (RingedSpace.inverseImage S.toRingedSpace f.base) D)
    (hind : StrictlyPerfectInduction.{u + 1, u})
    (hcl : Stacks.Cohomology.PseudoCoherentTensor.ComplexLevel.{u})
    (K M : DerivedCategory (OXMod.{u, u} X.toRingedSpace))
    (Θ : ∀ (V : TopologicalSpace.Opens
          (RingedSpace.inverseImage S.toRingedSpace f.base).carrier)
        (W : TopologicalSpace.Opens X.toRingedSpace.carrier), (∀ x, x ∈ V → x ∈ W) →
      DerivedCategory (OXMod.{u, u} (X.toRingedSpace.restrict W.isOpenEmbedding)) ⥤
        DerivedCategory (OXMod.{u, u}
          ((RingedSpace.inverseImage S.toRingedSpace f.base).restrict V.isOpenEmbedding)))
    (ΘcommShift : ∀ V W h, (Θ V W h).CommShift ℤ)
    (Θtriangulated : ∀ V W h, letI := ΘcommShift V W h; (Θ V W h).IsTriangulated)
    (Θunit : ∀ V W h, (Θ V W h).obj ((DerivedCategory.singleFunctor
        (OXMod.{u, u} (X.toRingedSpace.restrict W.isOpenEmbedding)) 0).obj
          (structureModule (X.toRingedSpace.restrict W.isOpenEmbedding))) ≅
      (RingedSpace.derivedRestrictModules
        (RingedSpace.inverseImage S.toRingedSpace f.base) V).obj
          ((derivedScalarRestriction f).obj M))
    (Θtensor : ∀ (V W h) (A : DerivedCategory (OXMod.{u, u} X.toRingedSpace)),
      (Θ V W h).obj ((RingedSpace.derivedRestrictModules X.toRingedSpace W).obj A) ≅
        (RingedSpace.derivedRestrictModules
          (RingedSpace.inverseImage S.toRingedSpace f.base) V).obj
            ((derivedScalarRestriction f).obj
          (((Stacks.Cohomology.PseudoCoherentTensor.derivedTensorProduct
            X.toRingedSpace).tensor.obj A).obj M)))
    (hK : RingedSpace.IsPerfect.{u, u + 1} K)
    (hM : f.IsPerfectRelativeTo D M) :
    f.IsPerfectRelativeTo D
      (((Stacks.Cohomology.PseudoCoherentTensor.derivedTensorProduct
        X.toRingedSpace).tensor.obj K).obj M)

AlgebraicGeometry.Scheme.Hom.isRelativelyPerfect_of_isPerfect_and_derivedTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectPerfectObjectsGenuine.lean, line 92.

Stacks 0DI4. Let f : X ⟶ S be a morphism of schemes which is flat and locally of finite presentation. A perfect object of D(𝒪_X) is S-perfect. If K, M ∈ D(𝒪_X), then K ⊗^{L}_{𝒪_X} M is S-perfect if K is perfect and M is S-perfect.

Here S-perfect is Stacks 0DI0, AlgebraicGeometry.Scheme.Hom.IsRelativelyPerfect, and the derived tensor product is the one of Stacks 06YU.

theorem isRelativelyPerfect_of_isPerfect_and_derivedTensor :
    (∀ E : DerivedCategory (OXMod.{u, u} X.toRingedSpace),
        RingedSpace.IsPerfect E → f.IsRelativelyPerfect E) ∧
      ∀ K M : DerivedCategory (OXMod.{u, u} X.toRingedSpace),
        RingedSpace.IsPerfect K → f.IsRelativelyPerfect M →
          f.IsRelativelyPerfect
            (((Stacks.Cohomology.PseudoCoherentTensor.derivedTensorProduct
              X.toRingedSpace).tensor.obj K).obj M)

Tag 0DI5, a lemma

Tag 0DI5 in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.isPseudoCoherent_derivedPullback_of_isPerfectRelativeTo, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectBaseChange.lean, line 117. The attribute's comment: “the pseudo-coherence conjunct of the conclusion”.

The pseudo-coherence conjunct of Stacks 0DI5. For f : X ⟶ S flat and locally of finite presentation, g : S' ⟶ S arbitrary, X' = S' ×_S X with projection g' : X' ⟶ X, and K an S-perfect object of D(𝒪_X), the derived pullback L(g')^*K is pseudo-coherent.

Only the pseudo-coherence conjunct of AlgebraicGeometry.Scheme.Hom.IsPerfectRelativeTo is used, so the family of derived tensor products on the inverse-image ringed space plays no role and is left arbitrary.

public theorem isPseudoCoherent_derivedPullback_of_isPerfectRelativeTo
    {X S S' X' : Scheme.{u}} (f : X ⟶ S) (g : S' ⟶ S) (g' : X' ⟶ X) (f' : X' ⟶ S')
    [Flat f] [LocallyOfFinitePresentation f] (_hpb : IsPullback g' f' f g)
    (D : ∀ U : TopologicalSpace.Opens
        (RingedSpace.inverseImage S.toRingedSpace f.base).carrier,
      RingedSpace.CertifiedDerivedSheafTensoring.{u + 1, u}
        ((RingedSpace.inverseImage S.toRingedSpace f.base).restrict U.isOpenEmbedding))
    (K : DerivedCategory (OXMod.{u, u} X.toRingedSpace))
    (hK : f.IsPerfectRelativeTo D K) :
    RingedSpace.IsPseudoCoherent (X := X'.toRingedSpace)
      ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
        g'.toLRSHom.toShHom).obj K)

AlgebraicGeometry.Scheme.Hom.isRelativelyPerfect_derivedPullback_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectBaseChangeCartesian.lean, line 138.

Stacks 0DI5. Let f : X ⟶ S be a morphism of schemes which is flat and locally of finite presentation, let g : S' ⟶ S be a morphism of schemes, and let X' with g' : X' ⟶ X and f' : X' ⟶ S' be a fibre product S' ×_S X. If K in D(𝒪_X) is S-perfect, then L(g')^*K is S'-perfect.

Relative perfectness is AlgebraicGeometry.Scheme.Hom.IsRelativelyPerfect, Stacks 0DI0 at the derived tensor product of Stacks 06YU, on both sides. Flat f' and LocallyOfFinitePresentation f', which the conclusion needs in order to be stated, are the base changes of the corresponding properties of f along g.

public theorem isRelativelyPerfect_derivedPullback_of_isPullback
    {X S S' X' : Scheme.{u}} {f : X ⟶ S} {g : S' ⟶ S} {g' : X' ⟶ X} {f' : X' ⟶ S'}
    (hpb : IsPullback g' f' f g) [Flat f] [LocallyOfFinitePresentation f]
    (K : DerivedCategory (OXMod.{u, u} X.toRingedSpace)) :
    haveI : Flat f' := MorphismProperty.of_isPullback (P := @Flat) hpb inferInstance
    haveI : LocallyOfFinitePresentation f' :=
      MorphismProperty.of_isPullback (P := @LocallyOfFinitePresentation) hpb inferInstance
    f.IsRelativelyPerfect K →
      f'.IsRelativelyPerfect
        ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
          g'.toLRSHom.toShHom).obj K)

AlgebraicGeometry.Scheme.Hom.isPerfectRelativeTo_derivedPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectBaseChangeFull.lean, line 81.

Stacks 0DI5. Let f : X ⟶ S be flat and locally of finite presentation, g : S' ⟶ S a morphism of schemes, and X' with g' : X' ⟶ X, f' : X' ⟶ S' the base change of f along g. If K in D(𝒪_X) is S-perfect, then L(g')^*K is S'-perfect.

Relative perfectness is read at the derived tensor product of Stacks 06YU on the open subspaces of the inverse-image ringed spaces.

theorem isPerfectRelativeTo_derivedPullback [Flat f] [LocallyOfFinitePresentation f]
    (hpb : IsPullback g' f' f g) (K : DerivedCategory X.Modules)
    (hK : f.IsPerfectRelativeTo
      (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily
        (RingedSpace.inverseImage S.toRingedSpace f.base)) K) :
    haveI : Flat f' := MorphismProperty.of_isPullback (P := @Flat) hpb (inferInstance : Flat f)
    haveI : LocallyOfFinitePresentation f' :=
      MorphismProperty.of_isPullback (P := @LocallyOfFinitePresentation) hpb
        (inferInstance : LocallyOfFinitePresentation f)
    f'.IsPerfectRelativeTo
      (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily
        (RingedSpace.inverseImage S'.toRingedSpace f'.base))
      ((derivedPullback g'.toLRSHom.toShHom).obj K)

Tag 0DI6, a situation

Tag 0DI6 in the Stacks Project.

AlgebraicGeometry.RelativeDescentSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfect.lean, line 45.

The relative descent situation: a directed inverse limit of quasi-compact, quasi-separated schemes with affine transition maps, together with a flat morphism of finite presentation over a fixed stage.

structure RelativeDescentSituation (I : Type v) [Preorder I] [IsDirected I (· ≤ ·)]

Tag 0DI7, a lemma

Tag 0DI7 in the Stacks Project.

AlgebraicGeometry.RelativeDescentSituation.homDescent_of_isPseudoCoherent_of_locallyHasFiniteTorDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativeDescentCapstone.lean, line 105.

Stacks 0DI7. In Situation 0DI6, let K₀ and L₀ be objects of D(𝒪_{X₀}) with K₀ pseudo-coherent and L₀ in D_QCoh(𝒪_{X₀}) of locally finite Tor dimension as an object of D((X₀ ⟶ S₀)⁻¹𝒪_{S₀}). Then colim_i Hom_{D(𝒪_{Xᵢ})}(Lf_{i0}^*K₀, Lf_{i0}^*L₀) ⟶ Hom_{D(𝒪_X)}(Lf₀^*K₀, Lf₀^*L₀) is bijective.

theorem homDescent_of_isPseudoCoherent_of_locallyHasFiniteTorDimension
    (hK₀ : RingedSpace.IsPseudoCoherent (X := D.X₀.left.toRingedSpace) K₀)
    (hL₀qc : ∀ n : ℤ,
      ((DerivedCategory.homologyFunctor D.X₀.left.Modules n).obj L₀).IsQuasicoherent)
    (hL₀tor : RingedSpace.LocallyHasFiniteTorDimension
      (RingedSpace.inverseImage (D.descent.system.obj (op D.descent.base)).toRingedSpace
        D.X₀.hom.base)
      (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily _)
      ((Scheme.Hom.derivedScalarRestriction D.X₀.hom).obj L₀)) :
    D.HomDescent K₀ L₀

Tag 0DI8, a lemma

Tag 0DI8 in the Stacks Project.

AlgebraicGeometry.AffinePerfectDescent.exists_isPerfectRelativeTo_stage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativeDescentAffineEssentialSurjectivity.lean, line 342. The attribute's comment: “essential surjectivity only, and only in the affine case of the filtered system of rings of Stacks 0DHX. Full faithfulness (Stacks 0DI7) is not reproved, and nothing is proved for a general Situation 0DI6; see the implementation notes.”.

The affine case of the essential-surjectivity half of Stacks 0DI8. Let R₀ be a ring, let i ↦ Rᵢ be a filtered diagram of R₀-algebras with colimit R, and let A₀ be a flat R₀-algebra of finite presentation. Put A = R ⊗_{R₀} A₀ and Aᵢ = Rᵢ ⊗_{R₀} A₀. Then every object of D(𝒪_{Spec A}) perfect relative to Spec R is, for some stage i, the derived pullback along Spec(Aᵢ → A) of an object of D(𝒪_{Spec Aᵢ}) perfect relative to Spec Rᵢ.

Relative perfectness is Stacks 0DI0 at the canonical certificate family on both sides. The object has quasi-coherent cohomology by Stacks 08E5, so Stacks 06Z0 presents it as the derived sheafification of a complex of A-modules; isPerfectRelativeTo_tildeObj_iff makes that complex perfect relative to R; Stacks 0DHX descends it to a stage; and derivedPullbackTildeObjIso, the affine comparison square of Stacks 08DW, identifies the derived pullback of the sheafification at that stage with the sheafification of the derived extension of scalars.

Stacks 0DI8 itself is AlgebraicGeometry.RelativeDescentSituation.isPerfectRelativeTo_colimit.

theorem exists_isPerfectRelativeTo_stage
    (E : DerivedCategory (OXMod.{u, u}
      (Spec (CommRingCat.of (c.pt ⊗[R₀] A₀))).toRingedSpace))
    (hE : (specMap c.pt (c.pt ⊗[R₀] A₀)).IsPerfectRelativeTo
      (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily _) E) :
    ∃ (i : I) (Ei : DerivedCategory (OXMod.{u, u}
        (Spec (CommRingCat.of (PseudoCoherence.stageAlgebra F A₀ i))).toRingedSpace)),
      (specMap (F.obj i) (PseudoCoherence.stageAlgebra F A₀ i)).IsPerfectRelativeTo
          (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily _) Ei ∧
        Nonempty ((derivedPullback (Spec.map (CommRingCat.ofHom
          (PseudoCoherence.stageToLimitMap c A₀ i))).toLRSHom.toShHom).obj Ei ≅ E)

AlgebraicGeometry.RelativeDescentSituation.isPerfectRelativeTo_colimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativeDescentPerfectColimit.lean, line 219.

Stacks 0DI8. In Situation 0DI6 the category of S-perfect objects of D(𝒪_X) is the colimit of the categories of Sᵢ-perfect objects of D(𝒪_{Xᵢ}): the transition functors Lf_{ji}^* and the comparison functors Lfᵢ^* carry relatively perfect objects to relatively perfect objects, the comparison out of the colimit is fully faithful, and it is essentially surjective.

theorem isPerfectRelativeTo_colimit :
    (∀ {i j : D.LaterIndex} (h : i.1 ≤ j.1)
        (E : DerivedCategory (OXMod.{u, u} (D.schemeAt i).toRingedSpace)),
        D.IsPerfectAt i E →
          D.IsPerfectAt j ((derivedPullback (D.transition h).toLRSHom.toShHom).obj E)) ∧
      (∀ (i : D.LaterIndex) (E : DerivedCategory (OXMod.{u, u} (D.schemeAt i).toRingedSpace)),
        D.IsPerfectAt i E →
          letI : Flat D.X₀.hom := D.flat
          letI : LocallyOfFinitePresentation D.X₀.hom :=
            D.finitePresentation.locallyOfFinitePresentation
          D.structureMapLimit.IsPerfectRelativeTo D.canonicalLimitCertificates
            ((derivedPullback (D.projection i).toLRSHom.toShHom).obj E)) ∧
      (∀ (i : D.LaterIndex) (K L : DerivedCategory (OXMod.{u, u} (D.schemeAt i).toRingedSpace)),
        D.IsPerfectAt i K → D.IsPerfectAt i L → D.HomDescentAt i K L) ∧
      D.PerfectEssentiallySurjectiveCanonical

Tag 0DJT, a lemma

Tag 0DJT in the Stacks Project.

Stacks.AlgebraicGeometry.RelativelyPerfectProperPushforward.isPerfect_derivedPushforward_of_isPerfectRelativeTo, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectProperPushforward.lean, line 256. The attribute's comment: “the perfectness clause only, over a Noetherian base: Rf_*E is perfect for E S-perfect and f proper, flat, locally of finite presentation. Three inputs are granted: Tag 02O5 (haff), quasi-coherence of the H^i(E) (hqc), and the Tor-dimension half of Tag 08EV quantified over the source complex (htor). The base-change clause is not proved here”.

[Stacks, Tag 0DJT], the perfectness clause, over a Noetherian base. Let S be a Noetherian scheme, let f : X ⟶ S be a proper, flat morphism of finite presentation and let E be an S-perfect object of D(𝒪_X) with quasi-coherent cohomology sheaves. Then Rf_*E is a perfect object of D(𝒪_S).

This is the converse implication of [Stacks, Tag 08CQ] applied to the pseudo-coherence proved above. The base-change clause of the tag — invertibility of the canonical derived base-change comparison — is a separate assertion and is not proved here.

The hypothesis htor is PushforwardTorDimensionResidue, the Tor-dimension half of [Stacks, Tag 08EV] quantified over the source complex, which is the half of that proof this library cannot carry out; haff is its named form of [Stacks, Tag 02O5]; and hqc is quasi-coherence of the cohomology sheaves of E.

theorem isPerfect_derivedPushforward_of_isPerfectRelativeTo (D : TensorFamily f)
    (hD : IsGenuineTensorFamily f D) (E : DerivedCategory X.Modules)
    (hE : f.IsPerfectRelativeTo D E)
    (hqc : ∀ j : ℤ, ((DerivedCategory.homologyFunctor X.Modules j).obj E).IsQuasicoherent)
    (haff : AlgebraicGeometry.ProperCoherentImage.HigherDirectImageIsCoherentOverAffineBase.{u})
    (htor : PushforwardTorDimensionResidue f D) :
    Stacks.Cohomology.PerfectComplexes.IsPerfect (X := S.toRingedSpace)
      ((derivedPushforwardModules f).obj E)

Stacks.AlgebraicGeometry.RelativelyPerfectProperPushforward.isPerfect_derivedPushforward_and_isIso_derivedBaseChangeMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectProperPushforwardBaseChange.lean, line 238.

[Stacks, Tag 0DJT]. Let f : X ⟶ S be a morphism of schemes which is flat, proper and of finite presentation, and let E ∈ D(𝒪_X) be S-perfect. Then Rf_*E is a perfect object of D(𝒪_S) and its formation commutes with arbitrary base change: for every cartesian square X' = X ×_S S' the base change map Lg^*Rf_*E ⟶ Rf'_*L(g')^*E of [Stacks, Tag 08HY] is an isomorphism.

theorem isPerfect_derivedPushforward_and_isIso_derivedBaseChangeMap {X S : Scheme.{u}}
    (f : X ⟶ S) [Flat f] [IsProper f] [LocallyOfFinitePresentation f]
    (E : DerivedCategory (StrictlyPerfect.OXMod.{u, u} X.toRingedSpace))
    (hE : f.IsPerfectRelativeTo
      (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily.{u + 1, u} _) E) :
    IsPerfect (X := S.toRingedSpace) ((derivedPushforwardModules f).obj E) ∧
      ∀ {X' S' : Scheme.{u}} (g : S' ⟶ S) (f' : X' ⟶ S') (g' : X' ⟶ X)
        (sq : IsPullback g' f' f g),
        IsIso (Stacks.Cohomology.DerivedBaseChange.derivedBaseChangeMap g'.toLRSHom.toShHom
          f'.toLRSHom.toShHom f.toLRSHom.toShHom g.toLRSHom.toShHom (comp_toShHom_of_comm sq.w)
          E)

Tag 0DJU, a lemma

Tag 0DJU in the Stacks Project.

Stacks.AlgebraicGeometry.RelativeDerivedHomDual.exists_isPseudoCoherent_pushforward_sheafHom_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativeDerivedHomDual.lean, line 333.

[Stacks, Tag 0DJU]. Let f : X ⟶ S be a morphism of schemes and E, K ∈ D(𝒪_X). Assume S is quasi-compact and quasi-separated, f is proper, flat and of finite presentation, E is S-perfect and K is pseudo-coherent. Then there is a pseudo-coherent L ∈ D(𝒪_S) with

Rf_* R𝓗om(K, E) ≅ R𝓗om(L, 𝒪_S),

and the same holds after arbitrary base change: for every cartesian square g' ≫ f = f' ≫ g with g : S' ⟶ S,

Rf'_* R𝓗om(L(g')^*K, L(g')^*E) ≅ R𝓗om(Lg^*L, 𝒪_{S'}).

The derived categories are read at the standard model CategoryTheory.HasDerivedCategory.standard (DStd), at which the derived direct image pushStd, the derived pullback pullStd, the derived internal Hom Stacks.SheafOfModules.derivedSheafHom and the structure sheaf in degree zero unitObj are taken; "of finite presentation" is LocallyOfFinitePresentation together with the quasi-compactness and quasi-separatedness that properness contains. L = hocolim Lₙ for the duals Lₙ = (Rf_* R𝓗om(Kₙ, E))^∨ of an approximation K = hocolim Kₙ by perfect objects; see exists_construction_isPseudoCoherent.

theorem exists_isPseudoCoherent_pushforward_sheafHom_iso [CompactSpace S] [QuasiSeparatedSpace S]
    [IsProper f] [Flat f] [LocallyOfFinitePresentation f] (E K : DStd X) (hE : IsRelPerfect f E)
    (hK : IsPseudoCoherentStd K) :
    ∃ L : DStd S, IsPseudoCoherentStd L ∧
      Nonempty ((pushStd f).obj (((derivedSheafHom X.sheaf).obj (op K)).obj E) ≅
        ((derivedSheafHom S.sheaf).obj (op L)).obj (unitObj S)) ∧
      ∀ {X' S' : Scheme.{u}} (g' : X' ⟶ X) (f' : X' ⟶ S') (g : S' ⟶ S), IsPullback g' f' f g →
        Nonempty ((pushStd f').obj (((derivedSheafHom X'.sheaf).obj
            (op ((pullStd g').obj K))).obj ((pullStd g').obj E)) ≅
          ((derivedSheafHom S'.sheaf).obj (op ((pullStd g).obj L))).obj (unitObj S'))

Tag 0DJV, a remark

Tag 0DJV in the Stacks Project.

Stacks.AlgebraicGeometry.RelativeExtCharacterization.exists_unique_relativeExt_representative_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativeExtCharacterization/AffineModuleLevel.lean, line 78. The attribute's comment: “module-level uniqueness, for S = Spec R affine: the complex L of Tag 0DJU is determined, up to an isomorphism inducing the identifications, among pseudo-coherent complexes L' by functorial isomorphisms Ext^i(L', F) = Ext^i(K, E (x)^L Lf^*F), F quasi-coherent, compatible with boundary maps. Proved for affine S only; the module-level form over a general quasi-compact quasi-separated S is open (see the module docstring)”.

[Stacks, Tag 0DJV], for S = Spec R affine, with the module-level uniqueness. Let f : X ⟶ Spec R be proper, flat and of finite presentation, E ∈ D(𝒪_X) perfect relative to Spec R and K ∈ D(𝒪_X) pseudo-coherent. The pseudo-coherent complex L on Spec R of [Stacks, Tag 0DJU], with Rf_*R𝓗om(K, E) ≅ R𝓗om(L, 𝒪), carries isomorphisms Ext^i(L, ℱ) ≃ Ext^i(K, E ⊗^L Lf^*ℱ) for quasi-coherent ℱ, functorial in ℱ and compatible with the boundary maps, induced by a natural identification θ on D^+_{QCoh} that characterizes L (all as in Stacks.AlgebraicGeometry.RelativeExtCharacterization.exists_unique_relativeExt_representative). Moreover L is characterized by the Ext isomorphisms alone, which is the module-level uniqueness of the remark: any pseudo-coherent L' with isomorphisms ε'_{ℱ,i} : Ext^i(L', ℱ) ≃ Ext^i(K, E ⊗^L Lf^*ℱ) for quasi-coherent ℱ, functorial in ℱ and compatible with the boundary maps, is isomorphic to L by an isomorphism g : L' ≅ L with ε'(g ∘ x) = ε(x).

theorem exists_unique_relativeExt_representative_spec [IsProper f] [Flat f]
    [LocallyOfFinitePresentation f] (E K : DStd X) (hE : IsRelPerfect f E)
    (hK : IsPseudoCoherentStd K) :
    ∃ L : DStd (Spec R), IsPseudoCoherentStd L ∧
      Nonempty ((pushStd f).obj (rhom K E) ≅ rhom L (unitObj (Spec R))) ∧
      ∃ θ : ShiftedHom.NaturalHomIdentification (𝟭 (DStd (Spec R))) (tensorPull f E) L K
          (boundedBelowQCoh (Spec R)),
        (∀ {F F' : (Spec R).Modules} (hF : F.IsQuasicoherent) (hF' : F'.IsQuasicoherent)
            (g : F ⟶ F') (i : ℤ)
            (x : ShiftedHom L ((RelativeDerivedHomDual.singleStd (Spec R) 0).obj F) i),
          extEquiv θ F' hF' i (x ≫ ((RelativeDerivedHomDual.singleStd (Spec R) 0).map g)⟦i⟧') =
            extEquiv θ F hF i x ≫
              ((tensorPull f E).map ((RelativeDerivedHomDual.singleStd (Spec R) 0).map g))⟦i⟧') ∧
        (∀ {T : ShortComplex (Spec R).Modules} (hT : T.ShortExact) (h₁ : T.X₁.IsQuasicoherent)
            (h₃ : T.X₃.IsQuasicoherent) (i j : ℤ) (hij : 1 + i = j)
            (x : ShiftedHom L ((RelativeDerivedHomDual.singleStd (Spec R) 0).obj T.X₃) i),
          extEquiv θ T.X₁ h₁ j (ShiftedHom.comp x (singleδStd hT) hij) =
            (extEquiv θ T.X₃ h₃ i x).comp (ShiftedHom.map (singleδStd hT) (tensorPull f E))
              hij) ∧
        (∀ (L' : DStd (Spec R)), IsPseudoCoherentStd L' →
          ∀ θ' : ShiftedHom.NaturalHomIdentification (𝟭 (DStd (Spec R))) (tensorPull f E) L' K
            (boundedBelowQCoh (Spec R)),
          ∃ φ : L' ≅ L, ∀ (N : DStd (Spec R)) (hN : boundedBelowQCoh (Spec R) N) (x : L ⟶ N),
            θ'.equiv N hN (φ.hom ≫ x) = θ.equiv N hN x) ∧
        ∀ (L' : DStd (Spec R)), IsPseudoCoherentStd L' →
          ∀ ε' : ∀ (F : (Spec R).Modules), F.IsQuasicoherent → ∀ i : ℤ,
              ShiftedHom L' ((RelativeDerivedHomDual.singleStd (Spec R) 0).obj F) i ≃+
                ShiftedHom K
                  ((tensorPull f E).obj ((RelativeDerivedHomDual.singleStd (Spec R) 0).obj F)) i,
          (∀ {F F' : (Spec R).Modules} (hF : F.IsQuasicoherent) (hF' : F'.IsQuasicoherent)
              (g : F ⟶ F') (i : ℤ)
              (x : ShiftedHom L' ((RelativeDerivedHomDual.singleStd (Spec R) 0).obj F) i),
            ε' F' hF' i (x ≫ ((RelativeDerivedHomDual.singleStd (Spec R) 0).map g)⟦i⟧') =
              ε' F hF i x ≫
                ((tensorPull f E).map ((RelativeDerivedHomDual.singleStd (Spec R) 0).map g))⟦i⟧') →
          (∀ {T : ShortComplex (Spec R).Modules} (hT : T.ShortExact) (h₁ : T.X₁.IsQuasicoherent)
              (h₃ : T.X₃.IsQuasicoherent) (i j : ℤ) (hij : 1 + i = j)
              (x : ShiftedHom L' ((RelativeDerivedHomDual.singleStd (Spec R) 0).obj T.X₃) i),
            ε' T.X₁ h₁ j (ShiftedHom.comp x (singleδStd hT) hij) =
              (ε' T.X₃ h₃ i x).comp (ShiftedHom.map (singleδStd hT) (tensorPull f E)) hij) →
          ∃ g : L' ≅ L, ∀ (F : (Spec R).Modules) (hF : F.IsQuasicoherent) (i : ℤ)
            (x : ShiftedHom L ((RelativeDerivedHomDual.singleStd (Spec R) 0).obj F) i),
            ε' F hF i (g.hom ≫ x) = extEquiv θ F hF i x

Stacks.AlgebraicGeometry.RelativeExtCharacterization.exists_unique_relativeExt_representative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativeExtCharacterization/Statement.lean, line 89. The attribute's comment: “the characterization of the complex L of Tag 0DJU by functorial isomorphisms Ext^i(L, F) = Ext^i(K, E (x)^L Lf^F) for F quasi-coherent, compatible with boundary maps: their existence, induced by a natural identification Hom(L, N) = Hom(K, E (x)^L Lf^N) on D^+_QCoh(O_S), and uniqueness of L among pseudo-coherent complexes carrying such an identification. Proved: existence in the source's shape, and uniqueness among L' carrying the D^+_QCoh identification. Open: the remark's module-level uniqueness (from the Ext delta-functor on QCoh alone), which is an Adams-type realizability question; see the module docstring”.

[Stacks, Tag 0DJV]. Let S be quasi-compact and quasi-separated, f : X ⟶ S proper, flat and of finite presentation, E ∈ D(𝒪_X) perfect relative to S and K ∈ D(𝒪_X) pseudo-coherent. The pseudo-coherent complex L on S of [Stacks, Tag 0DJU], with Rf_*R𝓗om(K, E) ≅ R𝓗om(L, 𝒪_S), carries isomorphisms

Ext^i_{𝒪_S}(L, ℱ) ≃ Ext^i_{𝒪_X}(K, E ⊗^L_{𝒪_X} Lf^*ℱ)

for all i and all quasi-coherent ℱ, functorial in ℱ and compatible with the boundary maps of short exact sequences of quasi-coherent modules (on the left, composition with the connecting morphism ℱ₃ ⟶ ℱ₁[1]; on the right, composition with its image under E ⊗^L Lf^*(-), the third morphism of a distinguished triangle by tensorPull_mapTriangle_singleTriangle). These isomorphisms are induced by a natural identification θ_N : Hom(L, N) ≃ Hom(K, E ⊗^L Lf^*N) for N in D^+_{QCoh}(𝒪_S) (the ℱ[i] being such N), and L is characterized by it: any pseudo-coherent L' carrying a natural identification θ' of the same kind is isomorphic to L, by an isomorphism φ with θ'(φ ∘ x) = θ(x).

The source leaves the statement imprecise ("If we ever need this we will formulate a precise result here"); the above is the precise form proved. Uniqueness from the module-level δ-functor alone, i.e. from natural isomorphisms of the Ext^i(-, ℱ) on quasi-coherent ℱ compatible with boundary maps but not coming from an identification on D^+_{QCoh}(𝒪_S), is not asserted: at f = 𝟙 and E = 𝒪 it is the statement that a pseudo-coherent complex on a quasi-compact quasi-separated scheme is determined by its δ-functor ℱ ↦ Ext^*(L, ℱ) on quasi-coherent modules, which is neither proved nor refuted here.

theorem exists_unique_relativeExt_representative [CompactSpace S] [QuasiSeparatedSpace S]
    [IsProper f] [Flat f] [LocallyOfFinitePresentation f] (E K : DStd X)
    (hE : IsRelPerfect f E) (hK : IsPseudoCoherentStd K) :
    ∃ L : DStd S, IsPseudoCoherentStd L ∧
      Nonempty ((pushStd f).obj (rhom K E) ≅ rhom L (unitObj S)) ∧
      ∃ θ : ShiftedHom.NaturalHomIdentification (𝟭 (DStd S)) (tensorPull f E) L K
          (boundedBelowQCoh S),
        (∀ {F F' : S.Modules} (hF : F.IsQuasicoherent) (hF' : F'.IsQuasicoherent)
            (g : F ⟶ F') (i : ℤ)
            (x : ShiftedHom L ((RelativeDerivedHomDual.singleStd S 0).obj F) i),
          extEquiv θ F' hF' i (x ≫ ((RelativeDerivedHomDual.singleStd S 0).map g)⟦i⟧') =
            extEquiv θ F hF i x ≫
              ((tensorPull f E).map ((RelativeDerivedHomDual.singleStd S 0).map g))⟦i⟧') ∧
        (∀ {T : ShortComplex S.Modules} (hT : T.ShortExact) (h₁ : T.X₁.IsQuasicoherent)
            (h₃ : T.X₃.IsQuasicoherent) (i j : ℤ) (hij : 1 + i = j)
            (x : ShiftedHom L ((RelativeDerivedHomDual.singleStd S 0).obj T.X₃) i),
          extEquiv θ T.X₁ h₁ j (ShiftedHom.comp x (singleδStd hT) hij) =
            (extEquiv θ T.X₃ h₃ i x).comp (ShiftedHom.map (singleδStd hT) (tensorPull f E))
              hij) ∧
        ∀ (L' : DStd S), IsPseudoCoherentStd L' →
          ∀ θ' : ShiftedHom.NaturalHomIdentification (𝟭 (DStd S)) (tensorPull f E) L' K
            (boundedBelowQCoh S),
          ∃ φ : L' ≅ L, ∀ (N : DStd S) (hN : boundedBelowQCoh S N) (x : L ⟶ N),
            θ'.equiv N hN (φ.hom ≫ x) = θ.equiv N hN x

Tag 0GEH, a lemma

Tag 0GEH in the Stacks Project.

AlgebraicGeometry.isLocallyBoundedBelow_of_isPerfectRelativeTo, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectBoundedBelow.lean, line 186. The attribute's comment: “condition (1) implies the first clause of condition (2): an S-perfect object is locally bounded below”.

Stacks 0GEH, condition (1) implies the first clause of condition (2). Let f : X ⟶ S be flat and locally of finite presentation. An object of D(𝒪_X) perfect relative to S is locally bounded below.

Relative perfectness gives an open covering of X on each member of which E, read over f⁻¹𝒪_S, has Tor amplitude in some interval [a, b]. The structure sheaf of the inverse-image ringed space is the unit of its tensor product, so that interval already bounds the cohomology of E|_U read over f⁻¹𝒪_S, and restriction of scalars along f⁻¹𝒪_S ⟶ 𝒪_X leaves the underlying sheaves unchanged.

The derived tensor product is a family of certificates, one on each open subspace of the inverse-image ringed space, pinned by the hypothesis that its underived tensor product is the genuine - ⊗_{f⁻¹𝒪_S} -.

public theorem isLocallyBoundedBelow_of_isPerfectRelativeTo {X S : Scheme.{u}} (f : X ⟶ S)
    [Flat f] [LocallyOfFinitePresentation f]
    [HasDerivedCategory.{d} (OXMod.{u, u} X.toRingedSpace)]
    [HasDerivedCategory.{d'} (OXMod.{u, u} (RingedSpace.inverseImage S.toRingedSpace f.base))]
    [∀ U : Opens (RingedSpace.inverseImage S.toRingedSpace f.base).carrier,
      HasDerivedCategory.{d'}
        (OXMod.{u, u} ((RingedSpace.inverseImage S.toRingedSpace f.base).restrict
          U.isOpenEmbedding))]
    (D : ∀ U : Opens (RingedSpace.inverseImage S.toRingedSpace f.base).carrier,
      RingedSpace.CertifiedDerivedSheafTensoring.{d', u}
        ((RingedSpace.inverseImage S.toRingedSpace f.base).restrict U.isOpenEmbedding))
    (hD : ∀ U : Opens (RingedSpace.inverseImage S.toRingedSpace f.base).carrier,
      (D U).tensor = Stacks.SheafOfModules.Tensor.sheafTensor
        ((RingedSpace.inverseImage S.toRingedSpace f.base).restrict U.isOpenEmbedding).sheaf)
    (E : DerivedCategory (OXMod.{u, u} X.toRingedSpace))
    (hE : f.IsPerfectRelativeTo D E) :
    RingedSpace.IsLocallyBoundedBelow X.toRingedSpace E

AlgebraicGeometry.isPerfectRelativeTo_iff_isLocallyBoundedBelow_and_fibres, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectFibres.lean, line 521.

Stacks 0GEH. Let f : X ⟶ S be a morphism of schemes which is flat and locally of finite presentation, and let E be a pseudo-coherent object of D(𝒪_X). The following are equivalent:

1. E is S-perfect (Stacks 0DI0);
2. E is locally bounded below and for every point s ∈ S the derived fibre L(X_s ⟶ X)^*E of D(𝒪_{X_s}) is locally bounded below, where X_s = X ×_S Spec κ(s).

Relative perfectness is read at the canonical certificate family AlgebraicGeometry.RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily, the genuine derived tensor product over f⁻¹𝒪_S.

theorem isPerfectRelativeTo_iff_isLocallyBoundedBelow_and_fibres
    (E : DerivedCategory (OXMod.{u, u} X.toRingedSpace))
    (hE : RingedSpace.IsPseudoCoherent (X := X.toRingedSpace) E) :
    f.IsPerfectRelativeTo (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily _) E ↔
      RingedSpace.IsLocallyBoundedBelow X.toRingedSpace E ∧
        ∀ s : S, RingedSpace.IsLocallyBoundedBelow
          (pullback f (S.fromSpecResidueField s)).toRingedSpace
          ((derivedPullback (pullback.fst f (S.fromSpecResidueField s)).toLRSHom.toShHom).obj
            E)

AlgebraicGeometry.Scheme.Hom.isRelativelyPerfect_of_isLocallyBoundedBelow_of_fibres, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectFromFibres.lean, line 58. The attribute's comment: “condition (2) implies condition (1): for f flat and locally of finite presentation and E pseudo-coherent, if E is locally bounded below and every derived fibre L(X_s ⟶ X)^*E is locally bounded below, then E is S-perfect”.

Stacks 0GEH, condition (2) implies condition (1). Let f : X ⟶ S be flat and locally of finite presentation and let E be a pseudo-coherent object of D(𝒪_X). If E is locally bounded below and for every point s of S the derived pullback L(X_s ⟶ X)^*E of E to the fibre X_s = X ×_S Spec κ(s) is locally bounded below, then E is S-perfect.

public theorem isRelativelyPerfect_of_isLocallyBoundedBelow_of_fibres
    {X S : Scheme.{u}} (f : X ⟶ S) [Flat f] [LocallyOfFinitePresentation f]
    (E : DerivedCategory X.Modules)
    (hpc : RingedSpace.IsPseudoCoherent (X := X.toRingedSpace) E)
    (hE : RingedSpace.IsLocallyBoundedBelow X.toRingedSpace E)
    (hfib : ∀ s : S, RingedSpace.IsLocallyBoundedBelow
      (Limits.pullback f (S.fromSpecResidueField s)).toRingedSpace
      ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
        (Limits.pullback.fst f (S.fromSpecResidueField s)).toLRSHom.toShHom).obj E)) :
    f.IsRelativelyPerfect E

Tag 0DI9, a remark

Tag 0DI9 in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.isRelativelyPerfect_iff_isLocallyBoundedFlatFinitePresentation_and_isTriangulated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectLieblich.lean, line 572. References: SGA 6 III (4.2), “(B)”.

Stacks 0DI9. Let f : X ⟶ S be a morphism of schemes.

1. If f is flat and locally of finite presentation (so that Definition 0DI0 applies), an object E of D(𝒪_X) is S-perfect exactly when it satisfies Lieblich's condition (A): locally on X, E is quasi-isomorphic to a finite complex of S-flat, finitely presented 𝒪_X-modules.
2. If f is locally of finite type, condition (B) — E is pseudo-coherent relative to S and locally has finite Tor dimension as an object of D(f⁻¹𝒪_S) — defines a strictly full triangulated subcategory of D(𝒪_X).
3. Condition (B) is the natural generalisation of Definition 0DI0: when f is flat and locally of finite presentation, (B) holds exactly for the S-perfect objects.

theorem isRelativelyPerfect_iff_isLocallyBoundedFlatFinitePresentation_and_isTriangulated :
    (∀ [Flat f] [LocallyOfFinitePresentation f]
        (E : DerivedCategory (OXMod.{u, u} X.toRingedSpace)),
      f.IsRelativelyPerfect E ↔ f.IsLocallyBoundedFlatFinitePresentation E) ∧
    (∀ [LocallyOfFiniteType f],
      f.isPseudoCoherentOfLocallyFiniteTorDimensionOver.IsClosedUnderIsomorphisms ∧
        f.isPseudoCoherentOfLocallyFiniteTorDimensionOver.IsTriangulated) ∧
    (∀ [Flat f] [LocallyOfFinitePresentation f]
        (E : DerivedCategory (OXMod.{u, u} X.toRingedSpace)),
      f.isPseudoCoherentOfLocallyFiniteTorDimensionOver E ↔ f.IsRelativelyPerfect E)

AlgebraicGeometry.Scheme.Hom.isClosedUnderIsomorphisms_isPseudoCoherentOfFiniteTorDimensionRelativeTo, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectTriangulated.lean, line 647. The attribute's comment: “condition (B) defines a triangulated subcategory”.

Stacks 0DI9, condition (B). For a morphism of schemes f : X ⟶ S which is only assumed locally of finite type, the objects of D(𝒪_X) satisfying condition (B) form a strictly full subcategory: both clauses are invariant under isomorphism in D(𝒪_X).

public theorem isClosedUnderIsomorphisms_isPseudoCoherentOfFiniteTorDimensionRelativeTo :
    (isPseudoCoherentOfFiniteTorDimensionRelativeTo f D).IsClosedUnderIsomorphisms

AlgebraicGeometry.Scheme.Hom.isTriangulated_isPseudoCoherentOfFiniteTorDimensionRelativeTo, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectTriangulated.lean, line 719. The attribute's comment: “condition (B) defines a triangulated subcategory”.

Stacks 0DI9, condition (B). For a morphism of schemes f : X ⟶ S which is only assumed locally of finite type — neither flat nor locally of finite presentation — the objects of D(𝒪_X) that are pseudo-coherent relative to S and of locally finite Tor dimension in D(f⁻¹𝒪_S) form a triangulated subcategory: the property contains the zero object, is stable under all shifts, and is closed under extensions.

Both clauses are triangulated subcategories separately — relative pseudo-coherence by Stacks 09UL, finite Tor dimension by Stacks 08CJ — and their intersection is one again. Exactness of each - ⊗^{L} ℱ[0] and locality of finite Tor dimension are hypotheses, both of them properties of the genuine derived tensor product that an arbitrary certificate need not have.

public theorem isTriangulated_isPseudoCoherentOfFiniteTorDimensionRelativeTo :
    (isPseudoCoherentOfFiniteTorDimensionRelativeTo f D).IsTriangulated

Sources

• Section 36.35, Tag 0DHZ
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Scheme.Hom.IsPerfectRelativeTo · AlgebraicGeometry.Scheme.Hom.IsRelativelyPerfect · AlgebraicGeometry.isPerfectRelativeTo_dualNumberResidueComplex_and_not_isPerfect · AlgebraicGeometry.isBounded_and_isPseudoCoherent_iff_boundedCoherent · AlgebraicGeometry.isPerfectRelativeTo_canonical_iff_isBounded_and_isPseudoCoherent · AlgebraicGeometry.isPerfectRelativeTo_canonical_iff_boundedCoherent · AlgebraicGeometry.Scheme.Hom.isPerfectRelativeTo_tfae · AlgebraicGeometry.pseudoCoherent_derivedSections_tfae

Section36.36 The resolution property#

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

Tag 0F86, a definition

Tag 0F86 in the Stacks Project.

AlgebraicGeometry.HasResolutionProperty, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ResolutionProperty.lean, line 46.

A scheme has the resolution property if every finite type quasi-coherent module on it is a quotient of a finite locally free module.

class HasResolutionProperty (X : Scheme.{u}) : Prop

Tag 0F87, a lemma

Tag 0F87 in the Stacks Project.

AlgebraicGeometry.hasResolutionProperty_of_isAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ResolutionPropertyAmple.lean, line 128.

A scheme carrying an ample invertible module has the resolution property: every finite type quasi-coherent module on it is a quotient of a finite locally free module.

theorem hasResolutionProperty_of_isAmple {X : Scheme.{u}} (L : X.Modules)
    [IsInvertibleModule X L] (hL : IsAmple X L) : HasResolutionProperty X

Tag 0FDD, a lemma

Tag 0FDD in the Stacks Project.

AlgebraicGeometry.hasResolutionProperty_of_isRelativelyAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ResolutionPropertyRelativelyAmple.lean, line 450.

Stacks Tag 0FDD. If f : X ⟶ Y is a morphism of schemes, Y is quasi-compact, quasi-separated and has the resolution property, and L is an invertible 𝒪_X-module ample relative to f, then X has the resolution property.

theorem hasResolutionProperty_of_isRelativelyAmple {X Y : Scheme.{u}} (f : X ⟶ Y)
    [CompactSpace Y] [QuasiSeparatedSpace Y] [HasResolutionProperty Y]
    (L : X.Modules) [Stacks.Ample.IsInvertibleModule X L]
    (hL : Stacks.RelativeAmple.IsRelativelyAmple f L) : HasResolutionProperty X

Tag 0F88, a lemma

Tag 0F88 in the Stacks Project.

AlgebraicGeometry.hasResolutionProperty_of_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ResolutionPropertyAffineHom.lean, line 91. The attribute's comment: “the affine case”.

The affine case of [Stacks, Tag 0F88]. The source of an affine morphism onto a quasi-compact, quasi-separated scheme with the resolution property has the resolution property.

The quasi-affine case is AlgebraicGeometry.hasResolutionProperty_of_isQuasiAffineHom, by way of [Stacks, Tag 0FDD] — so the tag below carries the clause string naming the case that is.

theorem hasResolutionProperty_of_isAffineHom {X Y : Scheme.{u}} (f : X ⟶ Y) [IsAffineHom f]
    [CompactSpace Y] [QuasiSeparatedSpace Y] [HasResolutionProperty Y] :
    HasResolutionProperty X

AlgebraicGeometry.hasResolutionProperty_of_isAffineHom_or_isQuasiAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ResolutionPropertyQuasiAffineHom.lean, line 60. The attribute's comment: “affine or quasi-affine f; the whole statement”.

Stacks 0F88. Let f : X ⟶ Y be an affine or quasi-affine morphism of schemes with Y quasi-compact and quasi-separated. If Y has the resolution property, so does X.

theorem hasResolutionProperty_of_isAffineHom_or_isQuasiAffineHom {X Y : Scheme.{u}} (f : X ⟶ Y)
    (hf : IsAffineHom f ∨ IsQuasiAffineHom f) [CompactSpace Y] [QuasiSeparatedSpace Y]
    [HasResolutionProperty Y] : HasResolutionProperty X

Tag 0GTC, a lemma

Tag 0GTC in the Stacks Project.

AlgebraicGeometry.hasResolutionProperty_of_surjective_isFiniteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ResolutionPropertyFiniteLocallyFree.lean, line 276.

Stacks Project, Tag 0GTC. If f : X ⟶ Y is a surjective finite locally free morphism of schemes and X has the resolution property, then so does Y.

theorem hasResolutionProperty_of_surjective_isFiniteLocallyFree {X Y : Scheme.{u}} (f : X ⟶ Y)
    [Surjective f] [Stacks.Morphisms.IsFiniteLocallyFree f] [HasResolutionProperty X] :
    HasResolutionProperty Y

Tag 0F89, a lemma

Tag 0F89 in the Stacks Project.

AlgebraicGeometry.exists_isFiniteLocallyFree_epi_of_isIdealAffineCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ResolutionPropertyIdealCovering.lean, line 105. The attribute's comment: “the direction that is immediate: resolution property implies each ideal is a finite-locally-free quotient”.

Let X be a scheme with a finite affine open covering U and finite type quasi-coherent sheaves of ideals I j whose vanishing loci are the complements of the U j. If X has the resolution property then each I j is the quotient of a finite locally free 𝒪_X-module.

theorem exists_isFiniteLocallyFree_epi_of_isIdealAffineCovering [HasResolutionProperty X] {m : ℕ}
    {U : Fin m → X.Opens} {I : Fin m → X.IdealSheafData} (h : IsIdealAffineCovering X U I)
    (j : Fin m) :
    ∃ (E : X.Modules)
      (_ : SheafOfModules.IsFiniteLocallyFree (R := X.ringCatSheaf) E)
      (q : E ⟶ idealPow (I j) 1), Epi q

AlgebraicGeometry.hasResolutionProperty_iff_forall_exists_epi_idealPow_of_isIdealAffineCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ResolutionPropertyIdealCoveringConverse.lean, line 61.

[Stacks, Tag 0F89]. Let X be a scheme with 1. a finite affine open covering X = U 0 ∪ ⋯ ∪ U (m - 1), and 2. finite type quasi-coherent sheaves of ideals I j with V(I j) = X ∖ U j.

Then X has the resolution property if and only if each I j is the quotient of a finite locally free 𝒪_X-module.

The forward direction is exists_isFiniteLocallyFree_epi_of_isIdealAffineCovering, the converse hasResolutionProperty_of_isIdealAffineCovering.

theorem hasResolutionProperty_iff_forall_exists_epi_idealPow_of_isIdealAffineCovering {m : ℕ}
    {U : Fin m → X.Opens} {I : Fin m → X.IdealSheafData} (h : IsIdealAffineCovering X U I) :
    HasResolutionProperty X ↔
      ∀ j, ∃ (E : X.Modules)
        (_ : SheafOfModules.IsFiniteLocallyFree (R := X.ringCatSheaf) E)
        (q : E ⟶ idealPow (I j) 1), Epi q

AlgebraicGeometry.hasResolutionProperty_of_isIdealAffineCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ResolutionPropertyIdealCoveringSubstantial.lean, line 234. The attribute's comment: “the substantial direction, at the source's generality: finite-locally-free quotients of the ideals give the resolution property”.

The substantial direction of [Stacks, Tag 0F89]. Let X be a scheme with a finite affine open covering U and finite type quasi-coherent sheaves of ideals I j whose vanishing loci are the complements of the U j. If each I j is the quotient of a finite locally free 𝒪_X-module then X has the resolution property.

X need not be Noetherian: this is the tag at the generality the source states it. Together with AlgebraicGeometry.exists_isFiniteLocallyFree_epi_of_isIdealAffineCovering, which is the direction the source calls trivial, it is the equivalence the tag asserts.

theorem hasResolutionProperty_of_isIdealAffineCovering {X : Scheme.{u}} {m : ℕ}
    {U : Fin m → X.Opens} {I : Fin m → X.IdealSheafData} (h : IsIdealAffineCovering X U I)
    (E : Fin m → X.Modules)
    (hE : ∀ j, SheafOfModules.IsFiniteLocallyFree (R := X.ringCatSheaf) (E j))
    (q : ∀ j, E j ⟶ idealPow (I j) 1) (hq : ∀ j, Epi (q j)) :
    HasResolutionProperty X

Tag 0GMM, a lemma

Tag 0GMM in the Stacks Project.

AlgebraicGeometry.Scheme.IsAmpleFamily.hasResolutionProperty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ResolutionPropertyAmpleFamilyIdealCovering.lean, line 197. References: EGA III (7.7.9), “(ii)”.

[Stacks, Tag 0GMM]. A scheme carrying an ample family of invertible modules has the resolution property.

The ample family supplies a finite covering of X by affine opens U k = X_{s k}, the nonvanishing loci of global sections s k of positive tensor powers M k of members of the family. The image of evaluation at s k, a morphism M k ^∨ ⟶ 𝒪_X out of the invertible, hence finite locally free, dual, is a finite type quasi-coherent sheaf of ideals whose vanishing locus is the complement of U k, and it is a quotient of M k ^∨. The substantial direction of [Stacks, Tag 0F89] then gives the resolution property.

theorem Scheme.IsAmpleFamily.hasResolutionProperty {ι : Type v} {X : Scheme.{u}}
    {L : ι → X.Modules} (hL : X.IsAmpleFamily L) : HasResolutionProperty X

Tag 0F8A, a lemma

Tag 0F8A in the Stacks Project.

AlgebraicGeometry.IsRegular.hasResolutionProperty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ResolutionPropertyAmpleFamilyIdealCovering.lean, line 229. References: SGA 3 VIB (13.3), “more general”.

[Stacks, Tag 0F8A]. A quasi-compact regular scheme with affine diagonal has the resolution property.

Quasi-compactness is CompactSpace X, the affine diagonal is IsAffineHom (pullback.diagonal (terminal.from X)), and regularity is AlgebraicGeometry.IsRegular ([Stacks, Tag 02IS]); these are exactly the conditions of the source.

The proof is the one of StacksFrontier/AlgebraicGeometry/Perfect/ResolutionPropertyRegular.lean: regularity gives Noetherianness and unique factorization in the local rings, a regular scheme is normal so every point lies in a dense affine open, [Stacks, Tag 0EGJ] cuts out the complement of each of those by an effective Cartier divisor, quasi-compactness makes the covering finite, and AlgebraicGeometry.hasResolutionProperty_of_isNoetherian_of_isEffectiveCartierDivisor concludes.

theorem IsRegular.hasResolutionProperty (X : Scheme.{u}) [CompactSpace X]
    [IsAffineHom
      (CategoryTheory.Limits.pullback.diagonal (CategoryTheory.Limits.terminal.from X))]
    (hX : IsRegular X) : HasResolutionProperty X

Tag 0F8B, a lemma

Tag 0F8B in the Stacks Project.

AlgebraicGeometry.hasResolutionProperty_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ResolutionPropertyLimit.lean, line 59. The attribute's comment: “the direction that is immediate: if a stage of the diagram has the resolution property then so does the limit”.

Let c be a limit cone over a cofiltered diagram D of quasi-compact, quasi-separated schemes with affine transition morphisms. If some stage D.obj i has the resolution property, then so does the limit c.pt.

The projection c.π.app i : c.pt ⟶ D.obj i is affine, so this is the affine case of [Stacks, Tag 0F88]; it is one direction of [Stacks, Tag 0F8B] (AlgebraicGeometry.hasResolutionProperty_iff_exists_of_isLimit).

theorem hasResolutionProperty_of_isLimit [IsCofiltered I]
    [∀ {i j : I} (g : i ⟶ j), IsAffineHom (D.map g)] (hc : IsLimit c)
    [∀ i : I, CompactSpace (D.obj i)] [∀ i : I, QuasiSeparatedSpace (D.obj i)]
    (i : I) [HasResolutionProperty (D.obj i)] :
    HasResolutionProperty c.pt

AlgebraicGeometry.hasResolutionProperty_iff_exists_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ResolutionPropertyLimitStageQcqs.lean, line 197.

[Stacks, Tag 0F8B]. Let c be a limit cone over a cofiltered diagram D of quasi-compact, quasi-separated schemes with affine transition morphisms. The limit c.pt has the resolution property if and only if some stage D.obj i has it.

theorem hasResolutionProperty_iff_exists_of_isLimit (hc : IsLimit c) :
    HasResolutionProperty c.pt ↔ ∃ i, HasResolutionProperty (D.obj i)

Tag 0F8C, a lemma

Tag 0F8C in the Stacks Project.

AlgebraicGeometry.HasResolutionProperty.isAffineHom_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ResolutionPropertyAffineDiagonal.lean, line 734.

Stacks Project, Tag 0F8C. A quasi-compact and quasi-separated scheme with the resolution property has affine diagonal.

This is AlgebraicGeometry.isAffineHom_diagonal_of_exists_isAffineHom_isNoetherian_hasResolutionProperty composed with AlgebraicGeometry.exists_isAffineHom_isNoetherian_hasResolutionProperty, which supplies the required affine morphism from the converse of AlgebraicGeometry.hasResolutionProperty_of_isLimit at Noetherian stages (AlgebraicGeometry.hasResolutionProperty_stage).

theorem HasResolutionProperty.isAffineHom_diagonal (X : Scheme.{u})
    [CompactSpace X] [QuasiSeparatedSpace X] [HasResolutionProperty X] :
    IsAffineHom (pullback.diagonal (terminal.from X))

Sources

• Section 36.36, Tag 0F85
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.HasResolutionProperty · AlgebraicGeometry.hasResolutionProperty_of_isAmple · AlgebraicGeometry.hasResolutionProperty_of_isRelativelyAmple · AlgebraicGeometry.hasResolutionProperty_of_isAffineHom · AlgebraicGeometry.hasResolutionProperty_of_isAffineHom_or_isQuasiAffineHom · AlgebraicGeometry.hasResolutionProperty_of_surjective_isFiniteLocallyFree · AlgebraicGeometry.exists_isFiniteLocallyFree_epi_of_isIdealAffineCovering · AlgebraicGeometry.hasResolutionProperty_iff_forall_exists_epi_idealPow_of_isIdealAffineCovering

Section36.37 The resolution property and perfect complexes#

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

Tag 0F8E, a lemma

Tag 0F8E in the Stacks Project.

Stacks.Perfect.BoundedLocallyFreeComplexes.exists_boundedFiniteLocallyFree_quasiIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/BoundedLocallyFreeComplexes/FiniteLocallyFreeReplacement.lean, line 1029.

Stacks Project, Tag 0F8E. On a quasi-compact and quasi-separated scheme with the resolution property, a bounded below complex of quasi-coherent modules representing a perfect object of the derived category receives a quasi-isomorphism from a bounded complex of finite locally free modules.

theorem exists_boundedFiniteLocallyFree_quasiIso (X : Scheme.{u})
    [CompactSpace X] [QuasiSeparatedSpace X] [AlgebraicGeometry.HasResolutionProperty X]
    (F : CochainComplex X.Modules ℤ)
    (hFplus : CochainComplex.plus X.Modules F)
    (hFqc : ∀ i : ℤ, (F.X i).IsQuasicoherent)
    (hFperf : IsPerfect (X := X.toRingedSpace) (DerivedCategory.Q.obj F)) :
    ∃ (E : CochainComplex X.Modules ℤ) (f : E ⟶ F),
      boundedFiniteLocallyFreeComplex X E ∧ QuasiIso f

Tag 0F8F, a lemma

Tag 0F8F in the Stacks Project.

Stacks.Perfect.BoundedLocallyFreeComplexes.exists_boundedFiniteLocallyFree_iso_of_hasResolutionProperty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/BoundedLocallyFreeComplexes/PerfectRepresentative.lean, line 81.

[Stacks, Tag 0F8F]. Let X be a quasi-compact and quasi-separated scheme with the resolution property. Every perfect object of D(𝒪_X) is isomorphic to the image of a bounded complex of finite locally free 𝒪_X-modules.

The three assumptions on X are exactly the source's. The affine diagonal used in the proof comes from [Stacks, Tag 0F8C], AlgebraicGeometry.HasResolutionProperty.isAffineHom_diagonal.

theorem exists_boundedFiniteLocallyFree_iso_of_hasResolutionProperty (X : Scheme.{u})
    [CompactSpace X] [QuasiSeparatedSpace X] [HasResolutionProperty X]
    (K : DerivedCategory X.Modules) (hK : IsPerfect (X := X.toRingedSpace) K) :
    ∃ E : CochainComplex X.Modules ℤ, boundedFiniteLocallyFreeComplex X E ∧
      Nonempty (DerivedCategory.Q.obj E ≅ K)

Tag 0F8G, a lemma

Tag 0F8G in the Stacks Project.

Stacks.Perfect.BoundedLocallyFreeComplexes.exists_boundedFiniteLocallyFree_roof_of_hasResolutionProperty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/BoundedLocallyFreeComplexes/DerivedRoof.lean, line 183.

[Stacks, Tag 0F8G]. Let X be a quasi-compact and quasi-separated scheme with the resolution property and let ℰ^•, ℱ^• be finite complexes of finite locally free 𝒪_X-modules. Every morphism α : ℰ^• ⟶ ℱ^• of D(𝒪_X) is represented by a diagram ℰ^• ← 𝒢^• → ℱ^• with 𝒢^• a bounded complex of finite locally free 𝒪_X-modules and 𝒢^• → ℰ^• a quasi-isomorphism.

The assumptions on X are exactly the source's. The affine diagonal used in the proof comes from [Stacks, Tag 0F8C], AlgebraicGeometry.HasResolutionProperty.isAffineHom_diagonal.

theorem exists_boundedFiniteLocallyFree_roof_of_hasResolutionProperty (X : Scheme.{u})
    [CompactSpace X] [QuasiSeparatedSpace X] [HasResolutionProperty X]
    (E F : CochainComplex X.Modules ℤ)
    (hE : boundedFiniteLocallyFreeComplex X E) (hF : boundedFiniteLocallyFreeComplex X F)
    (α : DerivedCategory.Q.obj E ⟶ DerivedCategory.Q.obj F) :
    ∃ (G : CochainComplex X.Modules ℤ) (p : G ⟶ E) (_ : QuasiIso p) (q : G ⟶ F),
      boundedFiniteLocallyFreeComplex X G ∧
        inv (DerivedCategory.Q.map p) ≫ DerivedCategory.Q.map q = α

Tag 0F8H, a lemma

Tag 0F8H in the Stacks Project.

Stacks.Perfect.BoundedLocallyFreeComplexes.exists_boundedFiniteLocallyFree_homotopy_of_hasResolutionProperty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/BoundedLocallyFreeComplexes/DerivedHomotopy.lean, line 209.

Let X be a quasi-compact and quasi-separated scheme with the resolution property and let ℰ^•, ℱ^• be finite complexes of finite locally free 𝒪_X-modules. If two maps of complexes α^•, β^• : ℰ^• ⟶ ℱ^• define the same morphism of D(𝒪_X), then there is a quasi-isomorphism γ^• : 𝒢^• ⟶ ℰ^• with 𝒢^• a bounded complex of finite locally free 𝒪_X-modules such that α^• ∘ γ^• and β^• ∘ γ^• are homotopic.

theorem exists_boundedFiniteLocallyFree_homotopy_of_hasResolutionProperty (X : Scheme.{u})
    [CompactSpace X] [QuasiSeparatedSpace X] [HasResolutionProperty X]
    (E F : CochainComplex X.Modules ℤ)
    (hE : boundedFiniteLocallyFreeComplex X E) (hF : boundedFiniteLocallyFreeComplex X F)
    (α β : E ⟶ F) (h : DerivedCategory.Q.map α = DerivedCategory.Q.map β) :
    ∃ (G : CochainComplex X.Modules ℤ) (γ : G ⟶ E) (_ : QuasiIso γ),
      boundedFiniteLocallyFreeComplex X G ∧ Nonempty (Homotopy (γ ≫ α) (γ ≫ β))

Tag 0F8I, a proposition

Tag 0F8I in the Stacks Project.

Stacks.Perfect.BoundedLocallyFreeComplexes.perfectDerivedProperty_isTriangulated, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/BoundedLocallyFreeComplexes/CanonicalFunctor.lean, line 58. The attribute's comment: “perfect objects form a triangulated subcategory”. References: SGA 6 I (5.8.4), “special case”; SGA 6 III (4.2), “Identity-morphism case”.

Perfect objects form a triangulated subcategory of D(O_X). This is the ringed-space statement Stacks.Cohomology.PerfectTriangulatedSubcategory.isTriangulated_isPerfect, read on the ringed space underlying X.

instance perfectDerivedProperty_isTriangulated (X : Scheme.{u}) :
    (show ObjectProperty (DerivedCategory X.Modules) from
      fun K => IsPerfect (X := X.toRingedSpace) K).IsTriangulated

Stacks.Perfect.BoundedLocallyFreeComplexes.perfectComplexFunctor_isTriangulated, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/BoundedLocallyFreeComplexes/CanonicalFunctor.lean, line 124. The attribute's comment: “exactness of the canonical functor”.

The canonical functor K^b(A) ⥤ D_perf(O_X) is exact. The composite K^b(A) ⥤ K(O_X) ⥤ D(O_X) is exact, being the inclusion of a triangulated subcategory followed by the localization functor of the derived category, and the canonical functor is its lift along the perfectness of its values, which is exact because D_perf(O_X) is a triangulated subcategory.

instance perfectComplexFunctor_isTriangulated (X : Scheme.{u}) :
    (perfectComplexFunctor X).IsTriangulated

Stacks.Perfect.BoundedLocallyFreeComplexes.BoundedFiniteLocallyFreeHomotopyCategory, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/BoundedLocallyFreeComplexes/Defs.lean, line 88. The attribute's comment: “the category K^b(A)”.

The homotopy category K^b(A) of bounded complexes of finite locally free modules.

abbrev BoundedFiniteLocallyFreeHomotopyCategory (X : Scheme.{u})

Stacks.Perfect.BoundedLocallyFreeComplexes.PerfectDerivedCategory, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/BoundedLocallyFreeComplexes/Defs.lean, line 93. The attribute's comment: “the category of perfect objects”.

The full subcategory D_perf(O_X) of perfect objects of the derived category.

abbrev PerfectDerivedCategory (X : Scheme.{u})

Stacks.Perfect.BoundedLocallyFreeComplexes.quasiIsomorphisms, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/BoundedLocallyFreeComplexes/Defs.lean, line 99. The attribute's comment: “the system S of quasi-isomorphisms”.

The system S of quasi-isomorphisms of K^b(A).

abbrev quasiIsomorphisms (X : Scheme.{u}) :
    MorphismProperty (BoundedFiniteLocallyFreeHomotopyCategory X)

Stacks.Perfect.BoundedLocallyFreeComplexes.perfectDerivedProperty_isClosedUnderIsomorphisms, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/BoundedLocallyFreeComplexes/Defs.lean, line 109. The attribute's comment: “perfect objects are closed under isomorphism”.

Perfect objects form a strictly full subcategory of D(O_X).

instance perfectDerivedProperty_isClosedUnderIsomorphisms (X : Scheme.{u}) :
    ObjectProperty.IsClosedUnderIsomorphisms
      (fun K : DerivedCategory X.Modules => IsPerfect (X := X.toRingedSpace) K)

Stacks.Perfect.BoundedLocallyFreeComplexes.quasiIsomorphisms_isInvertedBy_perfectComplexFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/BoundedLocallyFreeComplexes/InvertsQuasiIsomorphisms.lean, line 75. The attribute's comment: “the canonical functor inverts the system S of quasi-isomorphisms, so that it factors through S⁻¹K^b(A); this is the first field of Functor.IsLocalization, for every scheme X”.

The canonical functor K^b(A) ⥤ D_perf(O_X) inverts the quasi-isomorphisms of K^b(A). A morphism of K^b(A) is a quasi-isomorphism exactly when its image in K(O_X) is one, so CategoryTheory.DerivedCategory.Qh sends it to an isomorphism; that image is the image of the morphism under the fully faithful inclusion of D_perf(O_X), which therefore reflects the invertibility.

theorem quasiIsomorphisms_isInvertedBy_perfectComplexFunctor (X : Scheme.{u}) :
    (quasiIsomorphisms X).IsInvertedBy (perfectComplexFunctor X)

Stacks.Perfect.BoundedLocallyFreeComplexes.perfectComplexFunctor_isLocalization_of_hasResolutionProperty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/BoundedLocallyFreeComplexes/Localization.lean, line 150. The attribute's comment: “the canonical functor presents the perfect derived category as the localization of the bounded homotopy category at the quasi-isomorphisms”.

The equivalence clause of [Stacks, Tag 0F8I]. On a quasi-compact and quasi-separated scheme with the resolution property, the canonical functor K^b(A) ⥤ D_perf(𝒪_X) presents D_perf(𝒪_X) as the localization of K^b(A) at the quasi-isomorphisms.

The three assumptions on X are exactly the source's. The affine diagonal is supplied by [Stacks, Tag 0F8C] (AlgebraicGeometry.HasResolutionProperty.isAffineHom_diagonal), which rests on the converse of [Stacks, Tag 0F8B] at Noetherian stages (AlgebraicGeometry.hasResolutionProperty_stage).

theorem perfectComplexFunctor_isLocalization_of_hasResolutionProperty (X : Scheme.{u})
    [CompactSpace X] [QuasiSeparatedSpace X] [HasResolutionProperty X] :
    (perfectComplexFunctor X).IsLocalization (quasiIsomorphisms X)

Stacks.Perfect.BoundedLocallyFreeComplexes.perfect_of_boundedFiniteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/BoundedLocallyFreeComplexes/Perfectness.lean, line 99. The attribute's comment: “the functor lands in perfect objects”.

K^b(A) lands in D_perf(O_X). A bounded complex of finite locally free modules is strictly perfect on a small enough neighbourhood of each point of X, so it is perfect in the sense of Tag 08CM with the identity as the local quasi-isomorphism, and it represents its own image in the derived category.

theorem perfect_of_boundedFiniteLocallyFree (X : Scheme.{u})
    (E : BoundedFiniteLocallyFreeHomotopyCategory X) :
    IsPerfect (X := X.toRingedSpace) (DerivedCategory.Qh.obj E.obj)

Stacks.Perfect.BoundedLocallyFreeComplexes.isSaturated_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/BoundedLocallyFreeComplexes/Saturation.lean, line 63. The attribute's comment: “D_perf(O_X) is a saturated subcategory of D(O_X) -- the adjective saturated of the source's item (3), which is closure under direct summands, on any ringed space”.

Perfectness is a saturated property of objects of D(O_X) on a ringed space. Both summands of a perfect biproduct are perfect by [Stacks, Tag 08CS], and perfectness is closed under isomorphism, so the isomorphism closure in the definition of saturation is the property itself. For a scheme X, whose X.Modules is OXMod of X.toRingedSpace, this is the saturation clause of Tag 0F8I: a direct summand of a perfect object of D(O_X) is perfect.

theorem isSaturated_isPerfect {X : RingedSpace.{u, u}}
    [HasDerivedCategory.{d} (OXMod.{u, u} X)] :
    ObjectProperty.IsSaturated
      (fun K : DerivedCategory (OXMod.{u, u} X) => IsPerfect K)

Stacks.Perfect.BoundedLocallyFreeComplexes.boundedFiniteLocallyFreeHomotopyProperty_isTriangulated, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/BoundedLocallyFreeComplexes/Triangulated.lean, line 269. The attribute's comment: “the homotopy subcategory is triangulated”.

K^b(A) is a triangulated subcategory of K(O_X). The property of being a bounded complex with finite locally free terms holds of the zero complex, is stable under shift, and is stable under mapping cones; the last because (mappingCone f).X i is K.X (i + 1) ⊞ L.X i.

instance boundedFiniteLocallyFreeHomotopyProperty_isTriangulated
    (X : Scheme.{u}) :
    (boundedFiniteLocallyFreeHomotopyProperty X).IsTriangulated

Stacks.Perfect.BoundedLocallyFreeComplexes.perfectComplexFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/BoundedLocallyFreeComplexes/Triangulated.lean, line 335. The attribute's comment: “the canonical functor”.

The canonical functor K^b(A) ⥤ D_perf(O_X). It is DerivedCategory.Qh restricted to K^b(A), lifted to the full subcategory of perfect objects along Stacks.Perfect.BoundedLocallyFreeComplexes.perfect_of_boundedFiniteLocallyFree.

def perfectComplexFunctor (X : Scheme.{u}) :
    BoundedFiniteLocallyFreeHomotopyCategory X ⥤ PerfectDerivedCategory X

Stacks.Perfect.BoundedLocallyFreeComplexes.quasiIsomorphisms_isSaturated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/BoundedLocallyFreeComplexes/Triangulated.lean, line 367. The attribute's comment: “saturation of the quasi-isomorphism system”.

The system S of quasi-isomorphisms of K^b(A) is saturated.

theorem quasiIsomorphisms_isSaturated (X : Scheme.{u}) :
    (quasiIsomorphisms X).IsSaturated

Stacks.Perfect.BoundedLocallyFreeComplexes.quasiIsomorphisms_isCompatibleWithTriangulation, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/BoundedLocallyFreeComplexes/Triangulated.lean, line 374. The attribute's comment: “compatibility of quasi-isomorphisms with triangulation”.

The system S of quasi-isomorphisms of K^b(A) is compatible with the triangulated structure.

instance quasiIsomorphisms_isCompatibleWithTriangulation (X : Scheme.{u}) :
    (quasiIsomorphisms X).IsCompatibleWithTriangulation

Sources

• Section 36.37, Tag 0F8D
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Perfect.BoundedLocallyFreeComplexes.exists_boundedFiniteLocallyFree_quasiIso · Stacks.Perfect.BoundedLocallyFreeComplexes.exists_boundedFiniteLocallyFree_iso_of_hasResolutionProperty · Stacks.Perfect.BoundedLocallyFreeComplexes.exists_boundedFiniteLocallyFree_roof_of_hasResolutionProperty · Stacks.Perfect.BoundedLocallyFreeComplexes.exists_boundedFiniteLocallyFree_homotopy_of_hasResolutionProperty · Stacks.Perfect.BoundedLocallyFreeComplexes.perfectDerivedProperty_isTriangulated · Stacks.Perfect.BoundedLocallyFreeComplexes.perfectComplexFunctor_isTriangulated · Stacks.Perfect.BoundedLocallyFreeComplexes.BoundedFiniteLocallyFreeHomotopyCategory · Stacks.Perfect.BoundedLocallyFreeComplexes.PerfectDerivedCategory

Section36.38 K-groups#

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

Tag 0FDF, a lemma

Tag 0FDF in the Stacks Project.

AlgebraicGeometry.exists_addEquiv_coherentKZero_K0, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/GrothendieckGroup.lean, line 77. The attribute's comment: “the identification K₀(Coh(𝒪_X)) = K₀(D^b_Coh(𝒪_X)), the source's second equality. The source's middle group K₀(D^b(Coh(𝒪_X))) is AlgebraicGeometry.exists_addEquiv_coherentKZero_K0_bounded”. References: SGA 6 IV (2.4), “special case”; SGA 6 IV (3.2.3), “more general”.

Stacks Project, Tag 0FDF. The Grothendieck group K'₀(X) of coherent sheaves on a scheme X is the zeroth K-group of D^b_Coh(𝒪_X), the bounded objects of D(𝒪_X) with coherent cohomology sheaves, by an isomorphism sending the class of a coherent sheaf to the class of that sheaf placed in degree 0; and that property determines it.

theorem exists_addEquiv_coherentKZero_K0 (X : Scheme.{u})
    [HasDerivedCategory.{d} (SheafOfModules.{u} X.ringCatSheaf)] :
    ∃ e : CoherentKZero X ≃+ Pretriangulated.K0 (DerivedCategoryB.derivedCategoryBBounded
        (Stacks.SheafOfModules.coherentModules X.ringCatSheaf)).FullSubcategory,
      (∀ F : Stacks.SheafOfModules.CoherentModules X.ringCatSheaf,
          ∃ K : (DerivedCategoryB.derivedCategoryBBounded
              (Stacks.SheafOfModules.coherentModules X.ringCatSheaf)).FullSubcategory,
            Nonempty (K.obj ≅ (DerivedCategory.singleFunctor
              (SheafOfModules.{u} X.ringCatSheaf) 0).obj F.obj)) ∧
        ∀ (F : Stacks.SheafOfModules.CoherentModules X.ringCatSheaf)
          (K : (DerivedCategoryB.derivedCategoryBBounded
              (Stacks.SheafOfModules.coherentModules X.ringCatSheaf)).FullSubcategory),
          (K.obj ≅ (DerivedCategory.singleFunctor
              (SheafOfModules.{u} X.ringCatSheaf) 0).obj F.obj) →
            e (KZero.mk _ F) = QuotientAddGroup.mk (FreeAbelianGroup.of K)

AlgebraicGeometry.exists_addEquiv_coherentKZero_K0_bounded, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/GrothendieckGroupBoundedCoherent.lean, line 62. The attribute's comment: “the identification K₀(Coh(𝒪_X)) = K₀(D^b(Coh(𝒪_X))), the source's first equality”. References: SGA 6 IV (1.5), “(1.5.3), special case”.

Stacks Project, Tag 0FDF. The Grothendieck group K'₀(X) of coherent sheaves on a scheme X is the zeroth K-group of D^b(Coh(𝒪_X)), the bounded derived category of the abelian category of coherent 𝒪_X-modules, by an isomorphism sending the class of a coherent sheaf to the class of that sheaf placed in degree 0.

theorem exists_addEquiv_coherentKZero_K0_bounded (X : Scheme.{u})
    [HasDerivedCategory.{d} (Stacks.SheafOfModules.CoherentModules X.ringCatSheaf)] :
    ∃ e : CoherentKZero X ≃+ Pretriangulated.K0
        (DerivedCategory.Bounded (Stacks.SheafOfModules.CoherentModules X.ringCatSheaf)),
      ∀ F : Stacks.SheafOfModules.CoherentModules X.ringCatSheaf,
        e (KZero.mk _ F) = QuotientAddGroup.mk (FreeAbelianGroup.of
          (⟨(DerivedCategory.singleFunctor
                (Stacks.SheafOfModules.CoherentModules X.ringCatSheaf) 0).obj F,
            ⟨⟨0, inferInstance⟩, ⟨0, inferInstance⟩⟩⟩ :
            DerivedCategory.Bounded (Stacks.SheafOfModules.CoherentModules X.ringCatSheaf)))

AlgebraicGeometry.exists_addEquiv_K0_bounded_K0_boundedCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/GrothendieckGroupBoundedCoherent.lean, line 82. The attribute's comment: “the identification K₀(D^b(Coh(𝒪_X))) = K₀(D^b_Coh(𝒪_X)) of the source's two outer groups”.

Stacks Project, Tag 0FDF. For a scheme X the two outer groups of the chain of Tag 0FDF agree: the zeroth K-group of D^b(Coh(𝒪_X)), the bounded derived category of the abelian category of coherent 𝒪_X-modules, is isomorphic to the zeroth K-group of D^b_Coh(𝒪_X), the bounded objects of D(𝒪_X) whose cohomology sheaves are coherent. The isomorphism matches the classes of a coherent sheaf placed in degree 0 on the two sides: it carries the class of F in D^b(Coh(𝒪_X)) to the class of any object of D^b_Coh(𝒪_X) isomorphic to F in degree 0.

theorem exists_addEquiv_K0_bounded_K0_boundedCoherent (X : Scheme.{u})
    [HasDerivedCategory.{d} (SheafOfModules.{u} X.ringCatSheaf)]
    [HasDerivedCategory.{d'} (Stacks.SheafOfModules.CoherentModules X.ringCatSheaf)] :
    ∃ e : Pretriangulated.K0
        (DerivedCategory.Bounded (Stacks.SheafOfModules.CoherentModules X.ringCatSheaf)) ≃+
      Pretriangulated.K0 (DerivedCategoryB.derivedCategoryBBounded
        (Stacks.SheafOfModules.coherentModules X.ringCatSheaf)).FullSubcategory,
      ∀ (F : Stacks.SheafOfModules.CoherentModules X.ringCatSheaf)
        (K : (DerivedCategoryB.derivedCategoryBBounded
            (Stacks.SheafOfModules.coherentModules X.ringCatSheaf)).FullSubcategory),
        (K.obj ≅ (DerivedCategory.singleFunctor
            (SheafOfModules.{u} X.ringCatSheaf) 0).obj F.obj) →
          e (QuotientAddGroup.mk (FreeAbelianGroup.of
              (⟨(DerivedCategory.singleFunctor
                    (Stacks.SheafOfModules.CoherentModules X.ringCatSheaf) 0).obj F,
                ⟨⟨0, inferInstance⟩, ⟨0, inferInstance⟩⟩⟩ :
                DerivedCategory.Bounded
                  (Stacks.SheafOfModules.CoherentModules X.ringCatSheaf)))) =
            QuotientAddGroup.mk (FreeAbelianGroup.of K)

Tag 0FDG, a definition

Tag 0FDG in the Stacks Project.

Stacks.Perfect.BoundedLocallyFreeComplexes.perfectDerivedProperty_isTriangulated, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/BoundedLocallyFreeComplexes/CanonicalFunctor.lean, line 58. The attribute's comment: “(1) D_perf(𝒪_X) is TRIANGULATED in D(𝒪_X) — the adjective of Definition 0FDG (1) that makes K₀ of the subcategory defined at all, CategoryTheory.Pretriangulated.K0 taking a [Pretriangulated] instance. The definitional clause itself is AlgebraicGeometry.PerfectKZero”. References: SGA 6 I (5.8.4), “special case”; SGA 6 III (4.2), “Identity-morphism case”.

Perfect objects form a triangulated subcategory of D(O_X). This is the ringed-space statement Stacks.Cohomology.PerfectTriangulatedSubcategory.isTriangulated_isPerfect, read on the ringed space underlying X.

instance perfectDerivedProperty_isTriangulated (X : Scheme.{u}) :
    (show ObjectProperty (DerivedCategory X.Modules) from
      fun K => IsPerfect (X := X.toRingedSpace) K).IsTriangulated

Stacks.Perfect.BoundedLocallyFreeComplexes.perfectDerivedProperty_isClosedUnderIsomorphisms, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/BoundedLocallyFreeComplexes/Defs.lean, line 109. The attribute's comment: “(1) D_perf(𝒪_X) is STRICTLY FULL in D(𝒪_X) — the first of the three adjectives Definition 0FDG (1) attaches to the subcategory whose K-group it names. The definitional clause itself is AlgebraicGeometry.PerfectKZero”.

Perfect objects form a strictly full subcategory of D(O_X).

instance perfectDerivedProperty_isClosedUnderIsomorphisms (X : Scheme.{u}) :
    ObjectProperty.IsClosedUnderIsomorphisms
      (fun K : DerivedCategory X.Modules => IsPerfect (X := X.toRingedSpace) K)

AlgebraicGeometry.coherentModulesAbelian, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/GrothendieckGroup.lean, line 58. The attribute's comment: “coherent_abelian”. References: SGA 6 II (2.2.1), “Coh(S) abelian”.

Stacks Project, Tag 0FDG. Coherent sheaves of modules on a scheme form an abelian category.

noncomputable instance coherentModulesAbelian (X : Scheme.{u}) :
    Abelian (Stacks.SheafOfModules.CoherentModules X.ringCatSheaf)

AlgebraicGeometry.CoherentKZero, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/GrothendieckGroup.lean, line 65. The attribute's comment: “coherent_k0”. References: SGA 6 X (1.1); SGA 6 IV (2.2), “K_•(A_X)_naif”.

Stacks Project, Tag 0FDG (2). The Grothendieck group K'₀(X) of coherent sheaves on a scheme X.

noncomputable abbrev CoherentKZero (X : Scheme.{u}) : Type _

Stacks.Perfect.BoundedLocallyFreeComplexes.perfectDerivedProperty_isSaturated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/GrothendieckGroupPerfect.lean, line 80. The attribute's comment: “(1) D_perf(𝒪_X) is SATURATED in D(𝒪_X) — the third of the three adjectives Definition 0FDG (1) attaches to the subcategory whose K-group it names, and the only one the definition does not consume as an instance. The definitional clause itself is AlgebraicGeometry.PerfectKZero”.

D_perf(𝒪_X) is a saturated subcategory of D(𝒪_X): both summands of a perfect biproduct are perfect. This is Tag 08CS, read on the ringed space underlying X at the standard derived-category universe, fed to Stacks.Perfect.BoundedLocallyFreeComplexes.isSaturated_isPerfect_of_biprod.

theorem perfectDerivedProperty_isSaturated (X : Scheme.{u}) :
    (show ObjectProperty (DerivedCategory X.Modules) from
      fun K => IsPerfect (X := X.toRingedSpace) K).IsSaturated

AlgebraicGeometry.PerfectKZero, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/GrothendieckGroupPerfect.lean, line 105. The attribute's comment: “(1) the DEFINITIONAL clause: K₀(X) := K₀(D_perf(𝒪_X)). Being a definition this states nothing on its own; the three adjectives the source attaches to D_perf(𝒪_X) are the assertional part of (1) and are registered separately, on perfectDerivedProperty_isClosedUnderIsomorphisms (strictly full), perfectDerivedProperty_isTriangulated (triangulated) and perfectDerivedProperty_isSaturated (saturated)”.

Stacks Project, Tag 0FDG (1). The Grothendieck group K₀(X) of a scheme X: the zeroth K-group of the strictly full, saturated, triangulated subcategory D_perf(𝒪_X) of D(𝒪_X) consisting of the perfect objects.

abbrev PerfectKZero (X : Scheme.{u}) : Type _

Tag 0FDH, a lemma

Tag 0FDH in the Stacks Project.

Stacks.AlgebraicGeometry.GrothendieckGroupAffine.affineCoherentKZeroEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/GrothendieckGroupAffine/Basic.lean, line 325. The attribute's comment: “affine_k0_prime”.

The coherent Grothendieck group of Spec R is canonically isomorphic to the Grothendieck group of finite R-modules.

def affineCoherentKZeroEquiv (R : Type u) [CommRing R] [IsNoetherianRing R] :
    AlgebraicGeometry.CoherentKZero (Spec (CommRingCat.of R)) ≃+ KPrime0 R

Stacks.AlgebraicGeometry.GrothendieckGroupAffine.affineCoherentKZeroEquiv_mk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/GrothendieckGroupAffine/Basic.lean, line 332. The attribute's comment: “affine_k0_prime”.

The affine comparison sends the class of a coherent sheaf associated to a finite module to the class of that module.

theorem affineCoherentKZeroEquiv_mk (R : Type u) [CommRing R] [IsNoetherianRing R]
    (M : FinModule R)
    (F : Stacks.SheafOfModules.CoherentModules (Spec (CommRingCat.of R)).ringCatSheaf)
    (hF : Nonempty (F.obj ≅
      AlgebraicGeometry.tilde (ModuleCat.of (CommRingCat.of R) M.carrier))) :
    affineCoherentKZeroEquiv R (KZero.mk _ F) = M.cls

Stacks.AlgebraicGeometry.GrothendieckGroupAffine.exists_addEquiv_K0_perfectDerivedCategory_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/GrothendieckGroupAffine/Perfect.lean, line 185. The attribute's comment: “affine_k0”. References: SGA 6 0 (3.1), “special case”; SGA 6 VII (2.6), “special case”.

[Stacks, Tag 0FDH], the clause K₀(Spec R) = K₀(R). For a commutative ring R the Grothendieck group K₀(Spec R) = K₀(D_perf(𝒪_{Spec R})) of the affine scheme Spec R is isomorphic to the Grothendieck group K₀(R) of finite projective R-modules, by the isomorphism taking the class of a perfect object K of D(𝒪_{Spec R}) which is isomorphic to M̃ to the alternating sum of the classes of the terms of a bounded complex of finite projective R-modules representing M.

perfEquiv identifies D_perf(R) with D_perf(𝒪_{Spec R}), CategoryTheory.Pretriangulated.K0.mapEquiv turns that into an isomorphism of K-groups, and K0.exists_k0_perfectDerivedCategory_addEquiv ([Stacks, Tag 0FCU]) identifies K₀(D_perf(R)) with K₀(R) by the Euler characteristic, which is where the alternating sum comes from.

theorem exists_addEquiv_K0_perfectDerivedCategory_spec :
    ∃ e : Pretriangulated.K0 (PerfectDerivedCategory (Spec R)) ≃+ K0 (R : Type u),
      ∀ (K : PerfectDerivedCategory (Spec R)) (M : DerivedCategory (ModuleCat.{u} R))
        (Q : CochainComplex (ModuleCat.{u} (R : Type u)) ℤ) (a b : ℤ),
        Q.IsStrictlyGE a → Q.IsStrictlyLE b →
        (hfinite : ∀ i : ℤ, Module.Finite (R : Type u) (Q.X i)) →
        (hprojective : ∀ i : ℤ, Module.Projective (R : Type u) (Q.X i)) →
        Nonempty (M ≅ DerivedCategory.Q.obj Q) →
        Nonempty (K.obj ≅ (tilde.functor R).mapDerivedCategory.obj M) →
        e (Pretriangulated.K0.cls K) = ∑ i ∈ Finset.Icc a b,
          (i.negOnePow : ℤ) • K0.mk
            ({ carrier := Q.X i, finite := hfinite i, projective := hprojective i } :
              FGProj (R : Type u))

Tag 0FDI, a lemma

Tag 0FDI in the Stacks Project.

AlgebraicGeometry.exists_addEquiv_K0_coherentKZero_of_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RegularKGroupComparison.lean, line 88. References: SGA 6 IV (2.5), “(i), special case”.

[Stacks, Tag 0FDI]. Let X be a Noetherian regular scheme. Then the canonical map K₀(X) ⟶ K'₀(X) from the Grothendieck group of perfect complexes to the Grothendieck group of coherent sheaves is an isomorphism.

Every coherent sheaf placed in degree zero is a perfect complex, the comparison map takes the class of such a complex to the class of the sheaf, and it is the only additive homomorphism K₀(X) ⟶ K'₀(X) which does so.

theorem exists_addEquiv_K0_coherentKZero_of_isRegular (X : Scheme.{u}) [IsNoetherian X]
    (hX : IsRegular X) :
    ∃ e : Pretriangulated.K0 (PerfectDerivedCategory X) ≃+ CoherentKZero X,
      (∀ F : Stacks.SheafOfModules.CoherentModules X.ringCatSheaf,
          ∃ K : PerfectDerivedCategory X,
            Nonempty (K.obj ≅ (DerivedCategory.singleFunctor X.Modules 0).obj F.obj)) ∧
        (∀ (F : Stacks.SheafOfModules.CoherentModules X.ringCatSheaf)
            (K : PerfectDerivedCategory X),
            (K.obj ≅ (DerivedCategory.singleFunctor X.Modules 0).obj F.obj) →
              e (Pretriangulated.K0.cls K) = KZero.mk _ F) ∧
          ∀ φ : Pretriangulated.K0 (PerfectDerivedCategory X) →+ CoherentKZero X,
            (∀ (F : Stacks.SheafOfModules.CoherentModules X.ringCatSheaf)
                (K : PerfectDerivedCategory X),
                (K.obj ≅ (DerivedCategory.singleFunctor X.Modules 0).obj F.obj) →
                  φ (Pretriangulated.K0.cls K) = KZero.mk _ F) → φ = e.toAddMonoidHom

Tag 0FDJ, a lemma

Tag 0FDJ in the Stacks Project.

Stacks.Perfect.BoundedLocallyFreeComplexes.bijective_comparisonAddHom_of_hasResolutionProperty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/VectorBundleComparisonBijectiveUnconditional.lean, line 143. References: SGA 6 0 (3.1), “more general”.

Stacks Project, Tag 0FDJ. On a quasi-compact and quasi-separated scheme with the resolution property the canonical homomorphism K₀(Vect(X)) ⟶ K₀(X) = K₀(D_perf(𝒪_X)), which sends the class of a finite locally free 𝒪_X-module to the class of that module placed in degree zero, is an isomorphism: it is bijective, and it is a homomorphism of abelian groups by construction.

Surjectivity is Stacks.Perfect.BoundedLocallyFreeComplexes.surjective_comparisonAddHom, which reads off the class of a bounded complex of finite locally free modules as the alternating sum of the classes of its terms. Injectivity is the source's inverse map, the Euler characteristic Σᵢ (-1)ⁱ [ℰⁱ]; it is well defined because two bounded complexes of finite locally free modules isomorphic in D(𝒪_X) are connected by a roof of such complexes ([Stacks, Tag 0F8G]) and because the Euler characteristic of a bounded acyclic such complex vanishes, the modules of cycles being finite locally free.

The affine diagonal that both halves need is [Stacks, Tag 0F8C] at these same three conditions, AlgebraicGeometry.HasResolutionProperty.isAffineHom_diagonal.

theorem bijective_comparisonAddHom_of_hasResolutionProperty (X : Scheme.{u}) [CompactSpace X]
    [QuasiSeparatedSpace X] [HasResolutionProperty X] :
    Function.Bijective (comparisonAddHom X)

Stacks.Perfect.BoundedLocallyFreeComplexes.surjective_comparisonAddHom_of_isNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/VectorBundleComparisonSurjective.lean, line 577. The attribute's comment: “surjectivity of K₀(Vect(X)) ⟶ K₀(X), for a Noetherian scheme in place of an arbitrary quasi-compact one: the affine diagonal that the proof needs is deduced from the resolution property by the Noetherian case of Tag 0F8C”. References: SGA 6 IV (2.9), “(i)”.

The surjectivity half of [Stacks, Tag 0FDJ]. On a Noetherian, quasi-separated scheme with the resolution property the canonical homomorphism K₀(Vect(X)) ⟶ K₀(X) = K₀(D_perf(𝒪_X)), which sends the class of a finite locally free 𝒪_X-module to the class of that module placed in degree zero, is surjective.

The scheme has affine diagonal by the Noetherian case of [Stacks, Tag 0F8C], AlgebraicGeometry.isAffineHom_diagonal_of_hasResolutionProperty_of_isNoetherian, so Stacks.Perfect.BoundedLocallyFreeComplexes.exists_boundedFiniteLocallyFree_iso_of_affineDiagonal — [Stacks, Tag 0F8F] with the affine diagonal assumed rather than deduced — writes every perfect object of D(𝒪_X) as the image of a bounded complex of finite locally free modules. That is the hypothesis of Stacks.Perfect.BoundedLocallyFreeComplexes.surjective_comparisonAddHom, which reads off the class of such a complex as the alternating sum of the classes of its terms.

The whole tag, on a quasi-compact and quasi-separated scheme with the resolution property and with the comparison homomorphism an isomorphism, is Stacks.Perfect.BoundedLocallyFreeComplexes.bijective_comparisonAddHom_of_hasResolutionProperty of StacksFrontier.AlgebraicGeometry.Perfect.VectorBundleComparisonBijectiveUnconditional.

theorem surjective_comparisonAddHom_of_isNoetherian (X : Scheme.{u})
    [AlgebraicGeometry.IsNoetherian X] [QuasiSeparatedSpace X]
    [AlgebraicGeometry.HasResolutionProperty X] :
    Function.Surjective (comparisonAddHom X)

Tag 0FDK, a remark

Tag 0FDK in the Stacks Project.

AlgebraicGeometry.derivedCategoryBBounded_coherentModules_derivedTensor_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/CoherentKGroupModule.lean, line 127. The attribute's comment: “the bifunctor D_perf × D^b_Coh ⟶ D^b_Coh”.

Stacks Project, Tag 0FDK. Let X be a Noetherian scheme. The derived tensor product of a perfect object of D(𝒪_X) with an object of D^b_Coh(𝒪_X) is an object of D^b_Coh(𝒪_X): the derived tensor product produces the bifunctor ⊗^𝐋_{𝒪_X} : D_perf(𝒪_X) × D^b_Coh(𝒪_X) ⟶ D^b_Coh(𝒪_X).

theorem derivedCategoryBBounded_coherentModules_derivedTensor_of_isPerfect
    (K L : DerivedCategory (SheafOfModules.{u} X.ringCatSheaf))
    (hK : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace) K)
    (hL : DerivedCategoryB.derivedCategoryBBounded
      (Stacks.SheafOfModules.coherentModules X.ringCatSheaf) L) :
    DerivedCategoryB.derivedCategoryBBounded
      (Stacks.SheafOfModules.coherentModules X.ringCatSheaf)
      (((TorFormula.derivedTensor X).obj K).obj L)

AlgebraicGeometry.exists_derivedTensorProduct_module, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/CoherentKGroupModule.lean, line 227. The attribute's comment: “K₀(D^b_Coh(𝒪_X)) is a module over the Grothendieck ring K₀(D_perf(𝒪_X))”.

Stacks Project, Tag 0FDK. Let X be a Noetherian scheme. The zeroth K-group K₀(D^b_Coh(𝒪_X)) of the cohomologically bounded objects of D(𝒪_X) with coherent cohomology sheaves carries a module structure over the Grothendieck ring K₀(D_perf(𝒪_X)) of the perfect objects for which the scalar multiple of the class of an object of D^b_Coh(𝒪_X) by the class of a perfect object is the class of their derived tensor product. In particular that scalar multiplication is bilinear.

The ring acting is the commutative ring of AlgebraicGeometry.RingedSpace.exists_derivedTensorProduct_commRing (perfectTensorStructureScheme_eq), and the group acted on is K'₀(X) by [Stacks, Tag 0FDF].

theorem exists_derivedTensorProduct_module :
    letI := (perfectTensorStructureScheme X).commRing
    ∃ m : Module (K0 (perfectAtScheme X).FullSubcategory)
        (K0 (boundedCoherentAtScheme X).FullSubcategory),
      ∀ (K L : DerivedCategory (SheafOfModules.{u} X.ringCatSheaf))
        (hK : perfectAtScheme X K) (hL : boundedCoherentAtScheme X L)
        (h : boundedCoherentAtScheme X (((TorFormula.derivedTensor X).obj K).obj L)),
        letI := m
        K0.cls (⟨K, hK⟩ : (perfectAtScheme X).FullSubcategory) •
            K0.cls (⟨L, hL⟩ : (boundedCoherentAtScheme X).FullSubcategory) =
          K0.cls (⟨((TorFormula.derivedTensor X).obj K).obj L, h⟩ :
            (boundedCoherentAtScheme X).FullSubcategory)

AlgebraicGeometry.exists_module_coherentKZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/CoherentKGroupModule.lean, line 254. The attribute's comment: “K'₀(X) is a module over the Grothendieck ring K₀(X)”. References: SGA 6 IV (3.2.3).

Stacks Project, Tag 0FDK. Let X be a Noetherian scheme. The Grothendieck group K'₀(X) of coherent 𝒪_X-modules is a module over the Grothendieck ring K₀(X) = K₀(D_perf(𝒪_X)): there is a module structure on K'₀(X) and an isomorphism of abelian groups K'₀(X) ≅ K₀(D^b_Coh(𝒪_X)) which takes the class of a coherent module to the class of that module placed in degree zero — the isomorphism of [Stacks, Tag 0FDF] — and which carries the scalar multiple of the class of a coherent sheaf ℱ by the class of a perfect object K to the class of their derived tensor product K ⊗^𝐋_{𝒪_X} ℱ[0].

theorem exists_module_coherentKZero :
    letI := (perfectTensorStructureScheme X).commRing
    ∃ (m : Module (K0 (perfectAtScheme X).FullSubcategory) (CoherentKZero X))
      (e : CoherentKZero X ≃+ K0 (boundedCoherentAtScheme X).FullSubcategory),
      (∀ F : Stacks.SheafOfModules.CoherentModules X.ringCatSheaf,
          ∃ K : (boundedCoherentAtScheme X).FullSubcategory,
            Nonempty (K.obj ≅ (DerivedCategory.singleFunctor
              (SheafOfModules.{u} X.ringCatSheaf) 0).obj F.obj)) ∧
      (∀ (F : Stacks.SheafOfModules.CoherentModules X.ringCatSheaf)
          (K : (boundedCoherentAtScheme X).FullSubcategory),
          (K.obj ≅ (DerivedCategory.singleFunctor
              (SheafOfModules.{u} X.ringCatSheaf) 0).obj F.obj) →
            e (KZero.mk _ F) = K0.cls K) ∧
      ∀ (K : (perfectAtScheme X).FullSubcategory)
        (F : Stacks.SheafOfModules.CoherentModules X.ringCatSheaf)
        (L : (boundedCoherentAtScheme X).FullSubcategory)
        (_ : L.obj ≅ (DerivedCategory.singleFunctor
          (SheafOfModules.{u} X.ringCatSheaf) 0).obj F.obj)
        (h : boundedCoherentAtScheme X (((TorFormula.derivedTensor X).obj K.obj).obj L.obj)),
        letI := m
        e (K0.cls K • KZero.mk _ F) =
          K0.cls (⟨((TorFormula.derivedTensor X).obj K.obj).obj L.obj, h⟩ :
            (boundedCoherentAtScheme X).FullSubcategory)

AlgebraicGeometry.RingedSpace.exists_derivedTensorProduct_commRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/PerfectKGroupRing.lean, line 187. The attribute's comment: “perfect_k_ring”. References: SGA 6 IV (2.7), “b) ring str. on K'”.

Stacks Project, Tag 0FDK. The Grothendieck group K₀(D_perf(𝒪_X)) of the perfect objects of D(𝒪_X) carries a commutative ring structure whose additive group is the one it already has, whose product of the classes of two perfect objects is the class of their derived tensor product, and whose unit is the class of the structure sheaf in degree zero.

The source states this for a scheme; it holds for any ringed space, and for an arbitrary derived tensor product of 𝒪_X-modules, which is the generality Tag 09J5 is stated in.

theorem exists_derivedTensorProduct_commRing :
    ∃ r : CommRing (K0 (ObjectProperty.FullSubcategory
        (Stacks.Cohomology.PerfectComplexes.IsPerfect.{u, u, d} (X := X)))),
      r.toAddCommGroup = (inferInstance : AddCommGroup (K0 (ObjectProperty.FullSubcategory
        (Stacks.Cohomology.PerfectComplexes.IsPerfect.{u, u, d} (X := X))))) ∧
      (∀ (K L : ObjectProperty.FullSubcategory
            (Stacks.Cohomology.PerfectComplexes.IsPerfect.{u, u, d} (X := X)))
          (h : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X)
            ((T.tensor.obj K.obj).obj L.obj)),
        r.mul (K0.cls K) (K0.cls L) = K0.cls ⟨(T.tensor.obj K.obj).obj L.obj, h⟩) ∧
      (∀ h : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X)
          ((DerivedCategory.Q (C := Mod X.sheaf)).obj
            ((CochainComplex.singleFunctor (Mod X.sheaf) 0).obj
              (SheafOfModules.unit (Stacks.SheafOfModules.Tensor.ringSheaf.{u, u, u} X.sheaf)))),
        r.one = K0.cls ⟨_, h⟩)

AlgebraicGeometry.existsUnique_comparisonRingHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/VectorBundleComparison.lean, line 321. The attribute's comment: “vector_bundle_comparison_ring_map”. References: SGA 6 IV (2.7), “b) K'_naif→K' ring”.

There is a unique ring homomorphism from the Grothendieck ring of vector bundles on a scheme X to the Grothendieck ring of perfect objects of D(𝒪_X) which sends the class of a finite locally free module to the class of that module placed in degree zero.

The ring structure on the target is the one of AlgebraicGeometry.RingedSpace.exists_derivedTensorProduct_commRing, for the given derived tensor product.

theorem existsUnique_comparisonRingHom :
    letI := (RingedSpace.perfectTensorStructure X.toRingedSpace T).commRing
    ∃! f : VectorBundleKZero X →+*
        K0 (ObjectProperty.FullSubcategory
          (Stacks.Cohomology.PerfectComplexes.IsPerfect.{u, u, d} (X := X.toRingedSpace))),
      ∀ (M : X.Modules) (_ : IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf) M)
        (h : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace)
          ((DerivedCategory.singleFunctor X.Modules 0).obj M)),
        f (VectorBundleKZero.classOf X M) = K0.cls ⟨_, h⟩

AlgebraicGeometry.VectorBundleKZero.exists_tensorProduct_commRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/VectorBundleKGroup.lean, line 588. The attribute's comment: “vector_bundle_grothendieck_ring”. References: SGA 6 IV (2.7), “b) K'_naif ring str.”.

Stacks Project, Tag 0FDK. K₀(Vect(X)) carries a commutative ring structure whose additive group is the one it already has, whose multiplication is the tensor product of finite locally free modules, and whose unit is the class of the structure sheaf.

theorem exists_tensorProduct_commRing (X : Scheme.{u}) :
    ∃ r : CommRing (VectorBundleKZero X),
      r.toAddCommGroup = (inferInstance : AddCommGroup (VectorBundleKZero X)) ∧
        (∀ M N : X.Modules, IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf) M →
          IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf) N →
            r.mul (classOf X M) (classOf X N) =
              classOf X (Scheme.Modules.tensorObjRingedSpace X M N)) ∧
        classOf X (SheafOfModules.unit X.ringCatSheaf) = r.one

Tag 0FDL, a remark

Tag 0FDL in the Stacks Project.

AlgebraicGeometry.ProperPushforwardKZero.properPushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/GrothendieckGroupProperPushforward.lean, line 611. The attribute's comment: “the map f_ : K'₀(X) ⟶ K'₀(Y). All three of the source's reasons for well definedness are proved: coherence of the R ⁱ f_ ℱ (Tag 02O5), local finiteness of the nonzero ones, and the long exact sequence of the R ⁱ f_ with its terms collected by the parity of the degree (hasParityHexagons). The remark's quasi-compact restatement f_[ℱ] = ∑ (-1)ⁱ [R ⁱ f_ ℱ] = [Rf_ ℱ] is AlgebraicGeometry.ProperPushforwardKZero.properPushforward_mk_eq_finsum and AlgebraicGeometry.ProperPushforwardKZero.properPushforward_mk_eq_derivedClass”. References: SGA 6 0 (3.1); SGA 6 X (1.1.8).

[Stacks, Tag 0FDL]: proper pushforward on K'₀. For a proper morphism f : X ⟶ Y of locally Noetherian schemes, the homomorphism f_* : K'₀(X) ⟶ K'₀(Y) of Grothendieck groups of coherent sheaves determined by f_*[ℱ] = [⨁_{i ≥ 0} R ²ⁱ f_* ℱ] − [⨁_{i ≥ 0} R ²ⁱ⁺¹ f_* ℱ].

Its existence is KZero.lift applied to parityClass_add_of_shortExact; the coherence of the two sums, which is what makes the right-hand side a difference of classes in K'₀(Y), is isCoherent_parityDirectImageSum.

def properPushforward (f : X ⟶ Y) [IsLocallyNoetherian X] [IsLocallyNoetherian Y] [IsProper f] :
    CoherentKZero X →+ CoherentKZero Y

AlgebraicGeometry.ProperPushforwardKZero.properPushforward_mk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/GrothendieckGroupProperPushforward.lean, line 621. The attribute's comment: “the value f_[ℱ] = [⨁ R ²ⁱ f_ ℱ] - [⨁ R ²ⁱ⁺¹ f_ ℱ] of f_ on the class of a coherent sheaf, the first assertion of the remark”.

[Stacks, Tag 0FDL]: the value of f_* on the class of a coherent sheaf. For coherent 𝒪_Y-modules E and O isomorphic to ⨁_{i ≥ 0} R ²ⁱ f_* ℱ and ⨁_{i ≥ 0} R ²ⁱ⁺¹ f_* ℱ,

f_*[ℱ] = [E] − [O].

theorem properPushforward_mk (f : X ⟶ Y) [IsLocallyNoetherian X] [IsLocallyNoetherian Y]
    [IsProper f]
    (F : Stacks.SheafOfModules.CoherentModules X.ringCatSheaf)
    (E O : Stacks.SheafOfModules.CoherentModules Y.ringCatSheaf)
    (hE : E.obj ≅ parityDirectImageSum f F.obj 0)
    (hO : O.obj ≅ parityDirectImageSum f F.obj 1) :
    properPushforward f (KZero.mk _ F) = KZero.mk _ E - KZero.mk _ O

AlgebraicGeometry.ProperPushforwardKZero.existsUnique_properPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/GrothendieckGroupProperPushforward.lean, line 645. The attribute's comment: “the existence and uniqueness of the map f_* : K'₀(X) ⟶ K'₀(Y) with the value the remark prescribes on the class of a coherent sheaf”.

[Stacks, Tag 0FDL]. For a proper morphism f : X ⟶ Y of locally Noetherian schemes there is exactly one homomorphism f_* : K'₀(X) ⟶ K'₀(Y) with

f_*[ℱ] = [⨁_{i ≥ 0} R ²ⁱ f_* ℱ] − [⨁_{i ≥ 0} R ²ⁱ⁺¹ f_* ℱ]

for every coherent 𝒪_X-module ℱ, the two sums being read at any coherent 𝒪_Y-modules isomorphic to them.

theorem existsUnique_properPushforward (f : X ⟶ Y) [IsLocallyNoetherian X]
    [IsLocallyNoetherian Y] [IsProper f] :
    ∃! φ : CoherentKZero X →+ CoherentKZero Y,
      ∀ (F : Stacks.SheafOfModules.CoherentModules X.ringCatSheaf)
        (E O : Stacks.SheafOfModules.CoherentModules Y.ringCatSheaf),
        (E.obj ≅ parityDirectImageSum f F.obj 0) →
        (O.obj ≅ parityDirectImageSum f F.obj 1) →
          φ (KZero.mk _ F) = KZero.mk _ E - KZero.mk _ O

AlgebraicGeometry.ProperPushforwardKZero.properPushforward_mk_eq_finsum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/GrothendieckGroupProperPushforwardDerived.lean, line 286. The attribute's comment: “the quasi-compact restatement f_[ℱ] = ∑ (-1)ⁱ [R ⁱ f_ ℱ] of the remark”.

[Stacks, Tag 0FDL]: the quasi-compact restatement f_*[ℱ] = ∑ (−1)ⁱ [R ⁱ f_* ℱ]. For a proper morphism f : X ⟶ Y of locally Noetherian schemes with Y quasi-compact, the proper pushforward of the class of a coherent 𝒪_X-module is the alternating sum of the classes of its higher direct images; the sum is finite because they vanish in all large degrees.

The value of f_* on [ℱ] is [⨁_{i ≥ 0} R ²ⁱ f_* ℱ] − [⨁_{i ≥ 0} R ²ⁱ⁺¹ f_* ℱ] (properPushforward_mk); each of the two sums has only finitely many nonzero summands by exists_isZero_higherDirectImage_of_compactSpace, so mk_eq_sum_range_of_iso_sigma expands its class as a finite sum, and alternating_sum_range recombines the two finite sums by parity.

theorem properPushforward_mk_eq_finsum (f : X ⟶ Y) [IsLocallyNoetherian X]
    [IsLocallyNoetherian Y] [IsProper f] [CompactSpace Y]
    (F : Stacks.SheafOfModules.CoherentModules X.ringCatSheaf) :
    properPushforward f (KZero.mk _ F) =
      ∑ᶠ i : ℕ, ((i : ℤ).negOnePow : ℤ) • KZero.mk _ (coherentHigherDirectImage f F i)

AlgebraicGeometry.ProperPushforwardKZero.properPushforward_mk_eq_derivedClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/GrothendieckGroupProperPushforwardDerived.lean, line 659. The attribute's comment: “the quasi-compact restatement f_[ℱ] = [Rf_ ℱ] of the remark, under the identification K'₀(Y) = K₀(D^b_Coh(𝒪_Y)) of Tag 0FDF”.

[Stacks, Tag 0FDL]: the quasi-compact restatement f_*[ℱ] = [Rf_* ℱ]. For a proper morphism f : X ⟶ Y of locally Noetherian schemes with Y quasi-compact and a coherent 𝒪_X-module ℱ, the total derived direct image Rf_*(ℱ[0]) is an object of D^b_Coh(𝒪_Y), and under every identification K'₀(Y) = K₀(D^b_Coh(𝒪_Y)) which sends the class of a coherent sheaf to the class of that sheaf placed in degree 0 — the identification of [Stacks, Tag 0FDF] — the class f_*[ℱ] is the class of Rf_*(ℱ[0]).

The identity f_*[ℱ] = ∑ (−1)ⁱ [R ⁱ f_* ℱ] is properPushforward_mk_eq_finsum, and ∑ (−1)ⁱ [H ⁱ(K)] ↦ [K] is the inverse of the identification: the homomorphism φ of [Stacks, Tag 0FCR] for the zeroth homology functor takes [K] to ∑ (−1)ⁱ [H ⁱ(K)], and the composite of the identification with φ is the identity on the classes of coherent sheaves, hence the identity.

theorem properPushforward_mk_eq_derivedClass (f : X ⟶ Y) [IsLocallyNoetherian X]
    [IsLocallyNoetherian Y] [IsProper f] [CompactSpace Y]
    (F : Stacks.SheafOfModules.CoherentModules X.ringCatSheaf) :
    ∃ E : (DerivedCategoryB.derivedCategoryBBounded
        (Stacks.SheafOfModules.coherentModules Y.ringCatSheaf)).FullSubcategory,
      Nonempty (E.obj ≅ (derivedPushforwardModules f).obj
          ((DerivedCategory.singleFunctor X.Modules 0).obj F.obj)) ∧
        ∀ e : CoherentKZero Y ≃+ Pretriangulated.K0 (DerivedCategoryB.derivedCategoryBBounded
            (Stacks.SheafOfModules.coherentModules Y.ringCatSheaf)).FullSubcategory,
          (∀ (G : Stacks.SheafOfModules.CoherentModules Y.ringCatSheaf)
              (D : (DerivedCategoryB.derivedCategoryBBounded
                (Stacks.SheafOfModules.coherentModules Y.ringCatSheaf)).FullSubcategory),
              (D.obj ≅ (DerivedCategory.singleFunctor
                (SheafOfModules.{u} Y.ringCatSheaf) 0).obj G.obj) →
                e (KZero.mk _ G) = Pretriangulated.K0.cls D) →
            e (properPushforward f (KZero.mk _ F)) = Pretriangulated.K0.cls E

AlgebraicGeometry.ProperPushforwardKZero.exists_addEquiv_properPushforward_eq_derivedClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/GrothendieckGroupProperPushforwardDerived.lean, line 685. The attribute's comment: “the quasi-compact restatement f_[ℱ] = [Rf_ ℱ] of the remark, with the identification K'₀(Y) = K₀(D^b_Coh(𝒪_Y)) of Tag 0FDF exhibited”.

[Stacks, Tag 0FDL]: the quasi-compact restatement f_*[ℱ] = [Rf_* ℱ], with the identification K'₀(Y) = K₀(D^b_Coh(𝒪_Y)) of [Stacks, Tag 0FDF] exhibited.

theorem exists_addEquiv_properPushforward_eq_derivedClass (f : X ⟶ Y) [IsLocallyNoetherian X]
    [IsLocallyNoetherian Y] [IsProper f] [CompactSpace Y] :
    ∃ e : CoherentKZero Y ≃+ Pretriangulated.K0 (DerivedCategoryB.derivedCategoryBBounded
        (Stacks.SheafOfModules.coherentModules Y.ringCatSheaf)).FullSubcategory,
      (∀ (G : Stacks.SheafOfModules.CoherentModules Y.ringCatSheaf)
          (D : (DerivedCategoryB.derivedCategoryBBounded
            (Stacks.SheafOfModules.coherentModules Y.ringCatSheaf)).FullSubcategory),
          (D.obj ≅ (DerivedCategory.singleFunctor
            (SheafOfModules.{u} Y.ringCatSheaf) 0).obj G.obj) →
            e (KZero.mk _ G) = Pretriangulated.K0.cls D) ∧
        ∀ F : Stacks.SheafOfModules.CoherentModules X.ringCatSheaf,
          ∃ E : (DerivedCategoryB.derivedCategoryBBounded
              (Stacks.SheafOfModules.coherentModules Y.ringCatSheaf)).FullSubcategory,
            Nonempty (E.obj ≅ (derivedPushforwardModules f).obj
                ((DerivedCategory.singleFunctor X.Modules 0).obj F.obj)) ∧
              e (properPushforward f (KZero.mk _ F)) = Pretriangulated.K0.cls E

Tag 0FDM, a lemma

Tag 0FDM in the Stacks Project.

AlgebraicGeometry.properPushforward_perfectCoherentSMul_perfectPullbackKZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ProjectionFormulaKZero/ProjectionFormula.lean, line 153.

[Stacks, Tag 0FDM]: the projection formula on K-groups. Let f : X ⟶ Y be a proper morphism of locally Noetherian schemes. Then

f_*(α · f^*β) = f_*α · β

for α ∈ K'₀(X) and β ∈ K₀(Y). Here f_* : K'₀(X) ⟶ K'₀(Y) is the proper pushforward of [Stacks, Tag 0FDL] (AlgebraicGeometry.ProperPushforwardKZero.properPushforward), f^* : K₀(Y) ⟶ K₀(X) is induced by the derived pullback of perfect objects (AlgebraicGeometry.RingedSpace.perfectPullbackKZero), and K₀(X) × K'₀(X) ⟶ K'₀(X) is the product of [Stacks, Tag 0FDK] given by the derived tensor product (AlgebraicGeometry.ParityEulerClass.perfectCoherentSMul); on a Noetherian scheme that product is the scalar multiplication of the module structure of AlgebraicGeometry.exists_module_coherentKZero (AlgebraicGeometry.ParityEulerClass.perfectCoherentSMul_eq_smul).

Both sides are biadditive, so it suffices to treat α = [ℱ] and β = [P], which is AlgebraicGeometry.ParityEulerClass.properPushforward_perfectCoherentSMul_cls_mk: the derived projection formula Rf_*(ℱ ⊗^𝐋 Lf^*P) ≅ Rf_*ℱ ⊗^𝐋 P of [Stacks, Tag 08EU], here at a perfect object P where it is [Stacks, Tag 0B54], read through the identification f_*[ℱ] = [Rf_*ℱ] of Remark 0FDL and the definition of the product in Remark 0FDK.

theorem properPushforward_perfectCoherentSMul_perfectPullbackKZero {X Y : Scheme.{u}}
    (f : X ⟶ Y) [IsLocallyNoetherian X] [IsLocallyNoetherian Y] [IsProper f]
    (α : CoherentKZero X) (β : PerfectKZero Y) :
    ProperPushforwardKZero.properPushforward f
        (perfectCoherentSMul X (RingedSpace.perfectPullbackKZero f.toLRSHom.toShHom β) α) =
      perfectCoherentSMul Y β (ProperPushforwardKZero.properPushforward f α)

Tag 0FDN, a remark

Tag 0FDN in the Stacks Project.

AlgebraicGeometry.supportedPerfectDerivedCategory, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/KGroups/Basic.lean, line 62. The attribute's comment: “supported_perfect_definition”.

The strictly full subcategory of perfect derived objects whose every cohomology sheaf is set-theoretically supported on a closed subscheme.

public abbrev supportedPerfectDerivedCategory {X Z : Scheme.{u}} (i : Z ⟶ X)
    [IsClosedImmersion i] [HasDerivedCategory.{d} (OXMod.{u} X.toRingedSpace)]

AlgebraicGeometry.isClosedUnderIsomorphisms_supportedPerfect, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/KGroups/Basic.lean, line 81. The attribute's comment: “strict fullness of the supported perfect subcategory”.

Supported perfect objects form a strictly full subcategory. Perfectness only depends on the isomorphism class, and an isomorphism of derived objects induces an isomorphism of each cohomology sheaf, which has no effect on its support.

instance isClosedUnderIsomorphisms_supportedPerfect {X Z : Scheme.{u}} (i : Z ⟶ X)
    [IsClosedImmersion i] [HasDerivedCategory.{d} (OXMod.{u, u} X.toRingedSpace)] :
    ObjectProperty.IsClosedUnderIsomorphisms
      (show ObjectProperty (DerivedCategory (OXMod.{u, u} X.toRingedSpace)) from
        fun K => RingedSpace.IsPerfect K ∧
          ∀ n : ℤ, SheafOfModules.supp
            ((DerivedCategory.homologyFunctor (OXMod.{u, u} X.toRingedSpace) n).obj K) ⊆
              Set.range i.base)

AlgebraicGeometry.isTriangulated_supportedPerfect, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/KGroups/Basic.lean, line 103. The attribute's comment: “triangulatedness of the supported perfect subcategory”. References: SGA 6 I (5.8.4), “5.8.4 a), special case”.

Perfect complexes supported on a closed subscheme form a triangulated subcategory of the derived category of O_X-modules: the subcategory D_{Z, perf}(O_X) contains a zero object, is stable under all shifts, and the middle object of a distinguished triangle whose other two objects are perfect and supported on Z is again perfect and supported on Z.

Saturation, the remaining adjective of the source, is AlgebraicGeometry.isSaturated_supportedPerfect; its perfect half is Tag 08CS.

instance isTriangulated_supportedPerfect {X Z : Scheme.{u}} (i : Z ⟶ X)
    [IsClosedImmersion i] [HasDerivedCategory.{d} (OXMod.{u, u} X.toRingedSpace)] :
    ObjectProperty.IsTriangulated
      (show ObjectProperty (DerivedCategory (OXMod.{u, u} X.toRingedSpace)) from
        fun K => RingedSpace.IsPerfect K ∧
          ∀ n : ℤ, SheafOfModules.supp
            ((DerivedCategory.homologyFunctor (OXMod.{u, u} X.toRingedSpace) n).obj K) ⊆
              Set.range i.base)

AlgebraicGeometry.exists_supportedPerfect_not_exists_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/KGroups/NoUnit.lean, line 580. The attribute's comment: “in general K_0(D_{Z, perf}(O_X)) has no unit: for X = Spec ℤ and Z = Spec(ℤ/2) the multiplication given by the derived tensor product exists, and no multiplication on K_0(D_{Z, perf}(O_X)) distributive over its addition and computing the derived tensor product on classes has a unit”.

In general K₀(D_{Z, perf}(𝒪_X)) has no unit. There are a scheme X and a closed subscheme Z for which K₀(D_{Z, perf}(𝒪_X)) carries a multiplication — a non-unital commutative ring structure on its additive group whose product of two classes is the class of the derived tensor product — and no multiplication of that kind has a unit. Here X = Spec ℤ and Z = Spec(ℤ/2); the general statement is AlgebraicGeometry.SupportedPerfectNoUnit.not_exists_unit, for V(f) in the spectrum of any Noetherian domain of dimension at most one and any nonzero nonunit f.

theorem exists_supportedPerfect_not_exists_unit :
    ∃ (X Z : Scheme.{u}) (i : Z ⟶ X) (_ : IsClosedImmersion i),
      (∃ r : NonUnitalCommRing (K0 (supportedPerfectDerivedCategory i)),
        r.toAddCommGroup = (inferInstance : AddCommGroup (K0 (supportedPerfectDerivedCategory i))) ∧
          ∀ K L : supportedPerfectDerivedCategory i,
            r.mul (K0.cls K) (K0.cls L) = K0.cls (supportedPerfectTensorObj i K L)) ∧
      ∀ r : NonUnitalCommRing (K0 (supportedPerfectDerivedCategory i)),
        r.toAddCommGroup = (inferInstance : AddCommGroup (K0 (supportedPerfectDerivedCategory i))) →
          (∀ K L : supportedPerfectDerivedCategory i,
            r.mul (K0.cls K) (K0.cls L) = K0.cls (supportedPerfectTensorObj i K L)) →
          ¬ ∃ e, ∀ a, r.mul e a = a

AlgebraicGeometry.exists_supportedPerfect_nonUnitalCommRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/KGroups/Ring.lean, line 271. The attribute's comment: “the multiplication on K_0(D_{Z, perf}(O_X)) given by the derived tensor product, together with its associativity and commutativity -- the fields of NonUnitalCommRing. Stated at the standard derived-category model, which the source does not fix. The absence of a unit in general is AlgebraicGeometry.exists_supportedPerfect_not_exists_unit; the definition of the subcategory and its three adjectives are in StacksFrontier/AlgebraicGeometry/Perfect/KGroups/Basic.lean and StacksFrontier/AlgebraicGeometry/Perfect/KGroups/Saturation.lean”.

Stacks Project, Tag 0FDN. The K-group K₀(D_{Z, perf}(𝒪_X)) of the perfect objects of D(𝒪_X) supported on a closed subscheme Z carries a non-unital commutative ring structure: its additive group is the one K₀ already has, and the product of the classes of two objects is the class of their derived tensor product. Associativity, commutativity and distributivity are the fields of NonUnitalCommRing; no unit is asserted, and none exists in general: AlgebraicGeometry.exists_supportedPerfect_not_exists_unit.

theorem exists_supportedPerfect_nonUnitalCommRing :
    ∃ r : NonUnitalCommRing (K0 (supportedPerfectDerivedCategory i)),
      r.toAddCommGroup = (inferInstance : AddCommGroup (K0 (supportedPerfectDerivedCategory i))) ∧
        ∀ K L : supportedPerfectDerivedCategory i,
          r.mul (K0.cls K) (K0.cls L) = K0.cls (supportedPerfectTensorObj i K L)

AlgebraicGeometry.isSaturated_supportedPerfect, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/KGroups/Saturation.lean, line 68. The attribute's comment: “saturation of the supported perfect subcategory -- the adjective saturated of the source, which is closure under direct summands (Tag 05RB). The two other adjectives, strict fullness and triangulatedness, and the definition of the subcategory itself, are in StacksFrontier/AlgebraicGeometry/Perfect/KGroups/Basic.lean. The multiplication on K_0(D_{Z, perf}(O_X)) is in StacksFrontier/AlgebraicGeometry/Perfect/KGroups/Ring.lean and the absence of a unit in general in StacksFrontier/AlgebraicGeometry/Perfect/KGroups/NoUnit.lean”.

Perfect complexes supported on a closed subscheme form a saturated subcategory of D(O_X): if a binary biproduct is perfect with all its cohomology sheaves supported on Z, then so is each of its two summands.

Together with AlgebraicGeometry.isClosedUnderIsomorphisms_supportedPerfect and AlgebraicGeometry.isTriangulated_supportedPerfect this gives all three adjectives the source attaches to D_{Z, perf}(O_X): strictly full, saturated, triangulated.

instance isSaturated_supportedPerfect {X Z : Scheme.{u}} (i : Z ⟶ X)
    [IsClosedImmersion i] [HasDerivedCategory.{d} (OXMod.{u, u} X.toRingedSpace)] :
    ObjectProperty.IsSaturated
      (show ObjectProperty (DerivedCategory (OXMod.{u, u} X.toRingedSpace)) from
        fun K => RingedSpace.IsPerfect K ∧
          ∀ n : ℤ, SheafOfModules.supp
            ((DerivedCategory.homologyFunctor (OXMod.{u, u} X.toRingedSpace) n).obj K) ⊆
              Set.range i.base)

Sources

• Section 36.38, Tag 0FDE
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.exists_addEquiv_coherentKZero_K0 · AlgebraicGeometry.exists_addEquiv_coherentKZero_K0_bounded · AlgebraicGeometry.exists_addEquiv_K0_bounded_K0_boundedCoherent · Stacks.Perfect.BoundedLocallyFreeComplexes.perfectDerivedProperty_isTriangulated · Stacks.Perfect.BoundedLocallyFreeComplexes.perfectDerivedProperty_isClosedUnderIsomorphisms · AlgebraicGeometry.coherentModulesAbelian · AlgebraicGeometry.CoherentKZero · Stacks.Perfect.BoundedLocallyFreeComplexes.perfectDerivedProperty_isSaturated

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.