52.7 The theorem on formal… to 52.9 Algebraization of local…

Section52.7 The theorem on formal functions#

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

Tag 0A0I, an equation

Tag 0A0I in the Stacks Project.

AlgebraicGeometry.RingedSite.isIso_derivedCompletionPushforwardComparison_of_isDerivedComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletion.lean, line 500. The attribute's comment: “Equation 52.7.0.1 at the generality of a morphism of ringed sites and for a derived-complete object; the display's own setting, Section 52.7, is not formalized here”.

[Stacks, Tag 0A0G] at a derived-complete object. For K in D_comp(𝒪', ℐ') the canonical map (Rf_*K)^∧ ⟶ Rf_*(K^∧) is invertible, so Rf_*(K^∧) = Rf_*K = (Rf_*K)^∧: the unit K ⟶ K^∧ is invertible on a derived-complete K.

The general case of Tag 0A0G is not proved; see isIso_derivedCompletionPushforwardComparison_of_isIso_map_unit for the criterion that is, and the module documentation for the state of the four inputs of the source's proof. Three of them ([Stacks, Tags 0A0F, 0A0E, 0A07]) are now available; what is missing is the base case K = 𝒪[n] of the projection formula [Stacks, Tag 0944] on a ringed topos — the dévissage from it to a strictly perfect complex is available, and takes that case as a hypothesis — together with the identification of Lf^* of a Koszul complex with a Koszul complex. That is also why part (3) of [Stacks, Tag 099N] is registered here only for a derived-complete object.

This statement also carries [Stacks, Tag 0A0I], Equation 52.7.0.1 Rf_*(ℱ^∧) = (Rf_*ℱ)^∧, which the source justifies by citing Tag 0A0G: what is proved is that ringed-site statement, at a derived-complete object. The display's own setting — a proper morphism of schemes and a coherent module, Section 52.7 — is not formalized here. It also carries part (3) of [Stacks, Tag 099N], with the restrictions named on derivedCompletePushforward.

theorem isIso_derivedCompletionPushforwardComparison_of_isDerivedComplete
    {K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))}
    (hK : IsDerivedComplete.{u, u, u, u} X I' K) :
    IsIso ((derivedCompletionPushforwardComparison f I I' hI).app K)

AlgebraicGeometry.RingedSite.isIso_derivedCompletionPushforwardComparison_generatedIdealSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionCanonical.lean, line 428. The attribute's comment: “Equation 52.7.0.1 as an invertibility of the canonical comparison map (Rf_*ℱ)^∧ ⟶ Rf_*(ℱ^∧), for an arbitrary object of D(𝒪'), at a morphism of ringed sites and at ℐ = (t_1, …, t_r) ⊂ 𝒪 and ℐ' = (f^♯t_1, …, f^♯t_r) ⊂ 𝒪' generated by finitely many global sections, out of which both derived completion functors are built. The equation's two sides are therefore identified by the map [Stacks, Tag 0A0G] names, and not merely abstractly isomorphic”.

[Stacks, Tag 0A0G] for the canonical comparison map and an arbitrary object, at two sheaves of ideals generated by finitely many global sections. Let f : (Sh(𝒟), 𝒪') ⟶ (Sh(𝒞), 𝒪) be a morphism of ringed sites, let t_1, …, t_r be global sections of 𝒪 generating ℐ ⊂ 𝒪, let g_i = f^♯(t_i) generate ℐ' ⊂ 𝒪', and let K ∈ D(𝒪') be arbitrary. Then the canonical map

(Rf_*K)^∧ ⟶ Rf_*(K^∧)

of AlgebraicGeometry.RingedSite.derivedCompletionPushforwardComparisonGeneratedIdealSheaf is invertible: Rf_* commutes with derived completion, through the map the tag says it does.

Both derived completion functors are the reflector of [Stacks, Tag 099F], produced from the generators by AlgebraicGeometry.RingedSite.isRightAdjoint_ι_isDerivedComplete_generatedIdealSheaf, so no conclusion of that tag is an input; and the relation PushforwardIdealCompatible between the two sheaves of ideals that the comparison map needs is proved from hg, by AlgebraicGeometry.RingedSite.pushforwardIdealCompatible_of_pushGlobalSectionsCompatible.

The proof is isIso_derivedCompletionPushforwardComparison_of_nonempty_iso fed with AlgebraicGeometry.RingedSite.derivedPushforwardDerivedCompletionGeneratedIdealSheafIso of PushforwardCommutesCompletionCech.lean, which runs the source's own computation through the Čech presentation of the two completions and gives the display at every object. The Koszul Hom-tower form of the display, RingedSite.nonempty_iso_derivedPushforward_derivedCompletion_generatedIdealSheaf, would serve equally except that it carries Limits.HasCoproduct on the two Koszul towers as instance binders — countable coproducts of a derived category, which K-injective resolutions do not produce — and the Čech form needs no coproduct in a derived category at all, so this statement carries no such binder.

The source's ℐ is of finite type, hence only locally generated by finitely many sections; [Stacks, Tag 099F] at such an ℐ rests on [Stacks, Tags 099D and 099E], and the module documentation of PushforwardCommutesCompletionGenerated.lean records what stands in the way of the local-to-global descent.

theorem isIso_derivedCompletionPushforwardComparison_generatedIdealSheaf
    (K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
    IsIso ((derivedCompletionPushforwardComparisonGeneratedIdealSheaf f g t
      (pushforwardIdealCompatible_of_pushGlobalSectionsCompatible f t g hg)).app K)

AlgebraicGeometry.RingedSite.isIso_derivedCompletionPushforwardComparison_inverseImageIdealSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionCanonical.lean, line 515. The attribute's comment: “Equation 52.7.0.1 as an invertibility of the canonical comparison map (Rf_*ℱ)^∧ ⟶ Rf_*(ℱ^∧), for an arbitrary object of D(𝒪'), at the display's own pair of sheaves of ideals: ℐ = (t_1, …, t_r) ⊂ 𝒪 generated by finitely many global sections and ℐ' = f^{-1}ℐ · 𝒪_X built from f and t. The morphism of ringed sites carries a terminal object of the target site to a terminal object, as at ringed spaces and at schemes, and both derived completion functors are built from the generators of ℐ. The two sides of the equation are identified by the map [Stacks, Tag 0A0G] names”.

[Stacks, Tag 0A0G] for the canonical comparison map and an arbitrary object, at the source's own ideal sheaf ℐ' = f^{-1}ℐ · 𝒪_X. Let f : (Sh(𝒟), 𝒪') ⟶ (Sh(𝒞), 𝒪) be a morphism of ringed sites carrying a terminal object T of the target site to a terminal object, let ℐ = (t_1, …, t_r) ⊂ 𝒪 be generated by finitely many global sections, and let K ∈ D(𝒪') be arbitrary. Then the canonical map (Rf_*K)^∧ ⟶ Rf_*(K^∧) is invertible, the completion on the source being taken along ℐ' = f^{-1}ℐ · 𝒪_X.

That ideal sheaf is built here from f and t, as the one generated by f^♯t_1, …, f^♯t_r, and is the source's own: it receives f^♯(f^{-1}ℐ) and is least among those that do, by AlgebraicGeometry.RingedSite.eq_generatedIdealSheaf_pushGlobalSections. The terminal objects are what make a global section of 𝒪 transportable along a general morphism of sites; they are present at ringed spaces and at schemes, where f.u is Opens.map and carries ⊤ to ⊤.

This is isIso_derivedCompletionPushforwardComparison_generatedIdealSheaf at g = pushGlobalSections f hT' t, whose relation to t is AlgebraicGeometry.RingedSite.pushGlobalSectionsCompatible_pushGlobalSections.

theorem isIso_derivedCompletionPushforwardComparison_inverseImageIdealSheaf
    (K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
    IsIso ((derivedCompletionPushforwardComparisonInverseImageIdealSheaf f hT hT' t).app K)

AlgebraicGeometry.RingedSite.derivedPushforwardDerivedCompletionGeneratedIdealSheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionCech.lean, line 201. The attribute's comment: “Equation 52.7.0.1 for an arbitrary object of D(𝒪'), at sheaves of ideals ℐ = (t_1, …, t_r) ⊂ 𝒪 and ℐ' = (f^♯t_1, …, f^♯t_r) ⊂ 𝒪' generated by finitely many global sections, out of which both derived completion functors are built, so that no part of [Stacks, Tag 099F] is an input. The equation is obtained as an explicit isomorphism from the Čech presentation of the two completions, the identification Lf^*Č(𝒪, t) ≅ Č(𝒪', g) of the pulled-back Čech complexes, and the adjoint formula Rf_* R𝓗om_{𝒪'}(Lf^*-, M) ≅ R𝓗om_𝒪(-, Rf_*M). What is restricted is the data; the object ranges over all of D(𝒪')”.

[Stacks, Tags 0A0G and 0A0I] for an arbitrary object, at two sheaves of ideals generated by finitely many global sections. Let f : (Sh(𝒟), 𝒪') ⟶ (Sh(𝒞), 𝒪) be a morphism of ringed sites, let t_1, …, t_r be global sections of 𝒪 generating ℐ ⊂ 𝒪, let g_i = f^♯(t_i) generate ℐ' ⊂ 𝒪', and let K ∈ D(𝒪') be arbitrary. Then

Rf_*(K^∧) ≅ (Rf_*K)^∧:

Rf_* commutes with derived completion. Both derived completion functors are the reflector of [Stacks, Tag 099F], produced from the generators by AlgebraicGeometry.RingedSite.isRightAdjoint_ι_isDerivedComplete_generatedIdealSheaf, so no part of that tag is an input.

The reflector at a globally generated ideal sheaf is the Čech completion R𝓗om(Č(-), -) of [Stacks, Tag 099B] (AlgebraicGeometry.RingedSite.reflectorIsoCompletionFunctor), the source's Čech complex is the derived inverse image of the target's, and the adjoint formula moves Rf_* across the internal Hom. No countable coproduct in a derived category is assumed, and the isomorphism is produced rather than shown to exist; see the module documentation for the comparison with the derived-limit form.

def derivedPushforwardDerivedCompletionGeneratedIdealSheafIso
    (K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
    (derivedPushforward.{u} f.toRingedToposSiteHom).obj
        ((derivedCompletion X (generatedIdealSheaf g)).obj K) ≅
      (derivedCompletion Y (generatedIdealSheaf t)).obj
        ((derivedPushforward.{u} f.toRingedToposSiteHom).obj K)

AlgebraicGeometry.RingedSite.isDerivedComplete_derivedPushforward_derivedCompletion_inverseImageIdealSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionConstructedIdeal.lean, line 331. The attribute's comment: “the left hand side Rf_*(ℱ^∧) of Equation 52.7.0.1 is derived complete along ℐ, for an arbitrary object, at a morphism of ringed sites sending a terminal object of the target site to a terminal object of the source site, for ℐ generated by finitely many global sections of 𝒪 and the completion on the source taken along the ideal sheaf f^{-1}ℐ · 𝒪_X that Section 52.7 builds out of ℐ — identified as that ideal sheaf by AlgebraicGeometry.RingedSite.eq_generatedIdealSheaf_pushGlobalSections, and built here from f and the generators of ℐ. The derived completion functor is produced from those same generators, by AlgebraicGeometry.RingedSite.isRightAdjoint_ι_isDerivedComplete_generatedIdealSheaf, so no part of [Stacks, Tag 099F] is an input. What is restricted is the data: the source's ℐ is of finite type, hence only locally generated by finitely many sections; that case is proved, at a morphism of ringed spaces and at a morphism of schemes, in PushforwardCommutesCompletionFiniteType.lean, where the derived completion functor comes from [Stacks, Tag 099F] at a sheaf of ideals of finite type”.

[Stacks, Tag 0A0I], the left hand side of the display, at the source's own ideal sheaves. Rf_*(K^∧) is derived complete along ℐ = (t_1, …, t_s), for an arbitrary K ∈ D(𝒪'), the completion on the source being taken along ℐ' = f^{-1}ℐ · 𝒪_X.

This is RingedSite.isDerivedComplete_derivedPushforward_derivedCompletion_generatedIdealSheaf at the ideal sheaf the source builds: the generators of ℐ' are f^♯t_1, …, f^♯t_s, and the relation between the two sheaves of ideals that the general statement takes in is here proved, by pushforwardIdealCompatible_pushGlobalSections. So the statement depends on f, on the two terminal objects and on t, and on nothing else.

theorem isDerivedComplete_derivedPushforward_derivedCompletion_inverseImageIdealSheaf
    (K : DerivedCategory (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O)))) :
    IsDerivedComplete.{u, u, u, u} Y (generatedIdealSheaf t)
      ((derivedPushforward.{u} f.toRingedToposSiteHom).obj
        ((derivedCompletion X (generatedIdealSheaf (pushGlobalSections f hT' t))).obj K))

AlgebraicGeometry.RingedSite.isIso_derivedCompletionPushforwardComparison_inverseImageIdealSheaf_of_isDerivedComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionConstructedIdeal.lean, line 438. The attribute's comment: “Equation 52.7.0.1 at a morphism of ringed sites sending a terminal object of the target site to a terminal object of the source site, for a derived-complete object, with ℐ generated by finitely many global sections of 𝒪 and the completion on the source taken along the ideal sheaf f^{-1}ℐ · 𝒪_X that Section 52.7 builds out of ℐ, rather than along an unrelated sheaf of ideals. The display at the source's own data, sheaves of ideals of finite type, is in PushforwardCommutesCompletionFiniteType.lean, at a morphism of ringed spaces and at a morphism of schemes; the display for an arbitrary object is the invertibility half of [Stacks, Tag 0A0G]”.

[Stacks, Tags 0A0G and 0A0I] at a derived-complete object, at the source's own ideal sheaves. The comparison map (Rf_*K)^∧ ⟶ Rf_*(K^∧) is invertible for every K ∈ D(𝒪') derived complete along ℐ' = f^{-1}ℐ · 𝒪_X, so that Rf_*(K^∧) = Rf_*K = (Rf_*K)^∧ there.

This is RingedSite.isIso_derivedCompletionPushforwardComparison_generatedIdealSheaf_of_isDerivedComplete at ℐ' = f^{-1}ℐ · 𝒪_X. The same invertibility holds for an arbitrary K at this very pair of sheaves of ideals, by AlgebraicGeometry.RingedSite.isIso_derivedCompletionPushforwardComparison_inverseImageIdealSheaf of PushforwardCommutesCompletionCanonical.lean; the point of the statement below is that at a derived-complete K it needs none of that computation.

theorem isIso_derivedCompletionPushforwardComparison_inverseImageIdealSheaf_of_isDerivedComplete
    {K : DerivedCategory (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O)))}
    (hK : IsDerivedComplete.{u, u, u, u} X
      (generatedIdealSheaf (pushGlobalSections f hT' t)) K) :
    IsIso ((derivedCompletionPushforwardComparisonInverseImageIdealSheaf f hT hT' t).app K)

Stacks.RingedSpace.isDerivedComplete_derivedPushforward_derivedCompletion_inverseImageIdealSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionConstructedIdeal.lean, line 482. The attribute's comment: “the left hand side Rf_*(ℱ^∧) of Equation 52.7.0.1 is derived complete along ℐ, for an arbitrary object, at a morphism of ringed spaces read on its small Zariski sites, with ℐ generated by finitely many global sections of 𝒪_Y and the completion on X taken along the ideal sheaf f^{-1}ℐ · 𝒪_X that Section 52.7 builds out of ℐ, built here from f and the generators of ℐ. The derived completion functor is produced from those generators rather than received. The source's ℐ is quasi-coherent of finite type, hence only locally generated by finitely many sections; that case is Stacks.RingedSpace``.isDerivedComplete_derivedPushforward_derivedCompletion_of_isFiniteType of PushforwardCommutesCompletionFiniteType.lean, where the derived completion functor comes from [Stacks, Tag 099F] at a sheaf of ideals of finite type”.

[Stacks, Tag 0A0I], the left hand side of the display, at a morphism of ringed spaces and at the source's own ideal sheaves. Rf_*(ℱ^∧) is derived complete along ℐ = (t_1, …, t_s), for an arbitrary ℱ ∈ D(𝒪_X), the completion on X being taken along f^{-1}ℐ · 𝒪_X.

This is the ringed-site statement RingedSite.isDerivedComplete_derivedPushforward_derivedCompletion_inverseImageIdealSheaf read at the small Zariski sites of X and Y, where the terminal object is ⊤ and f.u ⊤ = f^{-1}⊤ = ⊤, so that both terminality inputs are CategoryTheory.Limits.isTerminalTop.

theorem isDerivedComplete_derivedPushforward_derivedCompletion_inverseImageIdealSheaf
    (K : DerivedCategory (_root_.SheafOfModules.{u}
      ((Stacks.SheafOfModules.Tensor.ringSheaf (toRingedSite X).O)))) :
    RingedSite.IsDerivedComplete.{u, u, u, u} (toRingedSite Y) (generatedIdealSheaf t)
      ((derivedPushforward.{u} (toRingedSiteHom f).toRingedToposSiteHom).obj
        ((RingedSite.derivedCompletion (toRingedSite X)
          (generatedIdealSheaf (pushGlobalSections (T := ⊤) (toRingedSiteHom f)
            isTerminalTop t))).obj K))

Stacks.RingedSpace.isIso_derivedCompletionPushforwardComparison_inverseImageIdealSheaf_of_isDerivedComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionConstructedIdeal.lean, line 515. The attribute's comment: “Equation 52.7.0.1 at a morphism of ringed spaces read on its small Zariski sites, for a derived-complete object, with ℐ generated by finitely many global sections of 𝒪_Y and the completion on X taken along the ideal sheaf f^{-1}ℐ · 𝒪_X that Section 52.7 builds out of ℐ, rather than along an unrelated sheaf of ideals; both derived completion functors are produced from the generators of ℐ. The display at the source's own data, two sheaves of ideals of finite type, is Stacks.RingedSpace``.isIso_derivedCompletionPushforwardComparison_of_isFiniteType_of_isDerivedComplete of PushforwardCommutesCompletionFiniteType.lean, of which this is an instance; the display for an arbitrary object is the invertibility half of [Stacks, Tag 0A0G]”.

[Stacks, Tag 0A0I] at a morphism of ringed spaces, for a derived-complete object, at the source's own ideal sheaves. The comparison (Rf_*ℱ)^∧ ⟶ Rf_*(ℱ^∧) is invertible whenever ℱ is derived complete along ℐ' = f^{-1}ℐ · 𝒪_X.

This is the statement of the same name in the namespace AlgebraicGeometry.RingedSite, read at the small Zariski sites. The restriction to a derived-complete ℱ is the tag's own content and remains; the invertibility for an arbitrary ℱ is the assertion of [Stacks, Tag 0A0G].

The same statement at the source's own data, two sheaves of ideals of finite type, is RingedSpace.isIso_derivedCompletionPushforwardComparison_of_isFiniteType_of_isDerivedComplete of PushforwardCommutesCompletionFiniteType.lean, and this one is an instance of it: the ideal sheaf f^{-1}ℐ · 𝒪_X built here is of finite type, by Stacks.RingedSpace.isFiniteType_generatedIdealSheaf there, as is ℐ.

theorem isIso_derivedCompletionPushforwardComparison_inverseImageIdealSheaf_of_isDerivedComplete
    {K : DerivedCategory (_root_.SheafOfModules.{u}
      ((Stacks.SheafOfModules.Tensor.ringSheaf (toRingedSite X).O)))}
    (hK : RingedSite.IsDerivedComplete.{u, u, u, u} (toRingedSite X)
      (generatedIdealSheaf (pushGlobalSections (T := ⊤) (toRingedSiteHom f)
        isTerminalTop t)) K) :
    IsIso ((RingedSite.derivedCompletionPushforwardComparisonInverseImageIdealSheaf
      (toRingedSiteHom f) isTerminalTop isTerminalTop t).app K)

AlgebraicGeometry.Scheme.isDerivedComplete_derivedPushforward_derivedCompletion_inverseImageIdealSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionConstructedIdeal.lean, line 562. The attribute's comment: “the left hand side Rf_*(ℱ^∧) of Equation 52.7.0.1 is derived complete along ℐ, for an arbitrary object, at a morphism of schemes — the display's own setting — with ℐ generated by finitely many global sections of 𝒪_S and the completion on X taken along the ideal sheaf f^{-1}ℐ · 𝒪_X that Section 52.7 builds out of ℐ, built here from f and the generators of ℐ. The derived completion functor is produced from those generators, so no part of [Stacks, Tag 099F] is an input, and neither quasi-coherence nor finite type of ℐ nor quasi-coherence of ℱ is needed. The same statement at a merely finite-type ℐ is AlgebraicGeometry.Scheme``.isDerivedComplete_derivedPushforward_derivedCompletion_of_isFiniteType of PushforwardCommutesCompletionFiniteType.lean, where the derived completion functor comes from [Stacks, Tag 099F] at a sheaf of ideals of finite type”.

[Stacks, Tag 0A0I], the left hand side of the display, in the display's own setting and at the source's own ideal sheaves. For a morphism of schemes f : X ⟶ S and ℐ = (t_1, …, t_s) generated by finitely many global sections of 𝒪_S, the object Rf_*(ℱ^∧) is derived complete along ℐ for an arbitrary ℱ ∈ D(𝒪_X), the completion on X being taken along f^{-1}ℐ · 𝒪_X.

theorem isDerivedComplete_derivedPushforward_derivedCompletion_inverseImageIdealSheaf
    (K : DerivedCategory (_root_.SheafOfModules.{u}
      ((Stacks.SheafOfModules.Tensor.ringSheaf
        (Stacks.RingedSpace.toRingedSite X.toRingedSpace).O)))) :
    RingedSite.IsDerivedComplete.{u, u, u, u}
        (Stacks.RingedSpace.toRingedSite S.toRingedSpace) (generatedIdealSheaf t)
      ((derivedPushforward.{u} (toRingedSiteHom f).toRingedToposSiteHom).obj
        ((RingedSite.derivedCompletion (Stacks.RingedSpace.toRingedSite X.toRingedSpace)
          (generatedIdealSheaf (pushGlobalSections (T := ⊤) (toRingedSiteHom f)
            isTerminalTop t))).obj K))

AlgebraicGeometry.Scheme.isIso_derivedCompletionPushforwardComparison_inverseImageIdealSheaf_of_isDerivedComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionConstructedIdeal.lean, line 601. The attribute's comment: “Equation 52.7.0.1 in the display's own setting, a morphism of schemes, for a derived-complete object, with ℐ generated by finitely many global sections of 𝒪_S and the completion on X taken along the ideal sheaf f^{-1}ℐ · 𝒪_X that Section 52.7 builds out of ℐ — so the two sheaves of ideals are the source's own pair and not an unrelated one. Both derived completion functors are produced from the generators of ℐ, so no part of [Stacks, Tag 099F] is an input, and neither quasi-coherence nor finite type of ℐ nor quasi-coherence of ℱ is needed. The display at a merely finite-type ℐ is AlgebraicGeometry.Scheme``.isIso_derivedCompletionPushforwardComparison_of_isFiniteType_of_isDerivedComplete of PushforwardCommutesCompletionFiniteType.lean, of which this is an instance; the display for an arbitrary object is the invertibility half of [Stacks, Tag 0A0G]”.

[Stacks, Tag 0A0I] in the display's own setting, for a derived-complete object, at the source's own ideal sheaves. Let f : X ⟶ S be a morphism of schemes and let ℐ = (t_1, …, t_s) ⊆ 𝒪_S be the sheaf of ideals generated by finitely many global sections. Then (Rf_*ℱ)^∧ ⟶ Rf_*(ℱ^∧) is invertible for every ℱ ∈ D(𝒪_X) derived complete along ℐ' = f^{-1}ℐ · 𝒪_X, the ideal sheaf of the display itself.

Both derived completion functors are produced from the generators of ℐ, so [Stacks, Tag 099F] is nowhere an input; neither quasi-coherence nor finite type of ℐ nor quasi-coherence of ℱ is needed either, those entering the source only through that tag. The restriction to a derived-complete ℱ is the tag's own content and remains; the invertibility for an arbitrary ℱ is the assertion of [Stacks, Tag 0A0G]. The descent from a globally generated ℐ to a finite-type one is Scheme.isIso_derivedCompletionPushforwardComparison_of_isFiniteType_of_isDerivedComplete of PushforwardCommutesCompletionFiniteType.lean, of which this statement is an instance: both ℐ and the f^{-1}ℐ · 𝒪_X built here are of finite type, by Stacks.RingedSpace.isFiniteType_generatedIdealSheaf there.

theorem isIso_derivedCompletionPushforwardComparison_inverseImageIdealSheaf_of_isDerivedComplete
    {K : DerivedCategory (_root_.SheafOfModules.{u}
      ((Stacks.SheafOfModules.Tensor.ringSheaf
        (Stacks.RingedSpace.toRingedSite X.toRingedSpace).O)))}
    (hK : RingedSite.IsDerivedComplete.{u, u, u, u}
      (Stacks.RingedSpace.toRingedSite X.toRingedSpace)
      (generatedIdealSheaf (pushGlobalSections (T := ⊤) (toRingedSiteHom f)
        isTerminalTop t)) K) :
    IsIso ((RingedSite.derivedCompletionPushforwardComparisonInverseImageIdealSheaf
      (toRingedSiteHom f) isTerminalTop isTerminalTop t).app K)

AlgebraicGeometry.RingedSite.derivedCompletionPushforwardObjIsoOfIsFiniteType, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionDisplay.lean, line 195. The attribute's comment: “Equation 52.7.0.1, Rf_*(ℱ^∧) = (Rf_*ℱ)^∧, as an isomorphism (Rf_*K)^∧ ≅ Rf_*(K^∧) for an arbitrary object of D(𝒪'), at a sheaf of ideals ℐ ⊂ 𝒪 of finite type and the ideal sheaf ℐ' = f^{-1}ℐ · 𝒪_X that Section 52.7 builds out of it. The two sides of the equation are identified by the canonical comparison map [Stacks, Tag 0A0G] names, and the identification is the component of an isomorphism of functors, hence natural in the object. No hypothesis on the object and none on the generating family”.

Equation 52.7.0.1 of [Stacks, Tag 0A0I], Rf_*(ℱ^∧) = (Rf_*ℱ)^∧, as an isomorphism

(Rf_*K)^∧ ≅ Rf_*(K^∧)

for an arbitrary object K of D(𝒪'), at a sheaf of ideals ℐ ⊂ 𝒪 of finite type and ℐ' = f^{-1}ℐ · 𝒪_X. The isomorphism is the component at K of the isomorphism of functors derivedCompletionPushforwardIsoOfIsFiniteType, hence natural in K, and its underlying morphism is the canonical comparison map that [Stacks, Tag 0A0G] names.

def derivedCompletionPushforwardObjIsoOfIsFiniteType
    (K : DerivedCategory (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O)))) :
    (derivedCompletion Y I).obj ((derivedPushforward.{u} f.toRingedToposSiteHom).obj K) ≅
      (derivedPushforward.{u} f.toRingedToposSiteHom).obj
        ((derivedCompletion X (inverseImageIdealSheaf f I)).obj K)

Stacks.RingedSpace.isDerivedComplete_derivedPushforward_derivedCompletion_of_isFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionFiniteType.lean, line 242. The attribute's comment: “the left hand side Rf_*(ℱ^∧) of Equation 52.7.0.1 is derived complete along ℐ, for an arbitrary object, at a morphism of ringed spaces read on its small Zariski sites, at the source's own data: a sheaf of ideals ℐ of finite type, the completion on X being taken along a sheaf of ideals ℐ' of finite type receiving f^♯(f^{-1}ℐ), as the display's f^{-1}ℐ · 𝒪_X does. The derived completion functor is produced from the finite-type hypothesis by [Stacks, Tag 099F], so it is an output here and not an input. Quasi-coherence of ℐ and of ℱ is not needed”.

[Stacks, Tag 0A0I], the left hand side of the display, at a morphism of ringed spaces and sheaves of ideals of finite type. Rf_*(ℱ^∧) is derived complete along ℐ, for an arbitrary ℱ ∈ D(𝒪_X), the completion on X being taken along any sheaf of ideals ℐ' of finite type receiving f^♯(f^{-1}ℐ) — in particular along the display's own f^{-1}ℐ · 𝒪_X.

The derived completion functor on D(𝒪_X) is produced from the finite-type hypothesis, by Stacks.RingedSpace.isRightAdjoint_ι_isDerivedComplete_of_isFiniteType, which is [Stacks, Tag 099F] — the step the source takes before writing the display down. The statement itself is then [Stacks, Tag 099J]: AlgebraicGeometry.RingedSite.isDerivedComplete_derivedPushforward_derivedCompletion read at the small Zariski sites of X and Y.

theorem isDerivedComplete_derivedPushforward_derivedCompletion_of_isFiniteType
    [I'.toSheafOfModules.IsFiniteType]
    (K : DerivedCategory (_root_.SheafOfModules.{u}
      ((Stacks.SheafOfModules.Tensor.ringSheaf (toRingedSite X).O)))) :
    RingedSite.IsDerivedComplete.{u, u, u, u} (toRingedSite Y) I
      ((@derivedPushforward.{u} _ _ _ _ _ _ _ (toRingedSiteHom f).toRingedToposSiteHom (_) (_)).obj
        ((RingedSite.derivedCompletion (toRingedSite X) I').obj K))

Stacks.RingedSpace.isIso_derivedCompletionPushforwardComparison_of_isFiniteType_of_isDerivedComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionFiniteType.lean, line 277. The attribute's comment: “Equation 52.7.0.1 at a morphism of ringed spaces read on its small Zariski sites, for a derived-complete object, at the source's own data: two sheaves of ideals of finite type, ℐ ⊆ 𝒪_Y and ℐ' ⊆ 𝒪_X with f^♯(f^{-1}ℐ) ⊆ ℐ', as the display's pair ℐ, f^{-1}ℐ · 𝒪_X is. Both derived completion functors are produced from those finite-type hypotheses by [Stacks, Tag 099F], so no part of that tag is an input, and quasi-coherence of ℐ and of ℱ is not needed. The display for an arbitrary object is the invertibility half of [Stacks, Tag 0A0G]”.

[Stacks, Tag 0A0I] at a morphism of ringed spaces and sheaves of ideals of finite type, for a derived-complete object. The comparison (Rf_*ℱ)^∧ ⟶ Rf_*(ℱ^∧) is invertible for every ℱ ∈ D(𝒪_X) derived complete along ℐ', where ℐ ⊆ 𝒪_Y and ℐ' ⊆ 𝒪_X are sheaves of ideals of finite type with f^♯(f^{-1}ℐ) ⊆ ℐ'.

Both derived completion functors are produced from the finite-type hypotheses by [Stacks, Tag 099F], Stacks.RingedSpace.isRightAdjoint_ι_isDerivedComplete_of_isFiniteType, so the data this statement takes is the source's own; quasi-coherence of ℐ and of ℱ is not needed. The underlying statement is AlgebraicGeometry.RingedSite.isIso_derivedCompletionPushforwardComparison_of_isDerivedComplete read at the small Zariski sites.

The restriction to a derived-complete ℱ is on the object: the invertibility for an arbitrary ℱ is the assertion of [Stacks, Tag 0A0G], and it is proved — at a morphism of ringed sites and at the constructed ℐ' = f^{-1}ℐ · 𝒪_X rather than at an independent parameter ℐ' — by RingedSite.isIso_derivedCompletionPushforwardComparison_inverseImageIdealSheaf_of_isFiniteType, and at a morphism of schemes and a quasi-coherent ℐ of finite type by Scheme.isIso_derivedCompletionPushforwardComparison_idealSheafData_inverseImageIdealSheaf.

theorem isIso_derivedCompletionPushforwardComparison_of_isFiniteType_of_isDerivedComplete
    [I.toSheafOfModules.IsFiniteType] [I'.toSheafOfModules.IsFiniteType]
    {K : DerivedCategory (_root_.SheafOfModules.{u}
      ((Stacks.SheafOfModules.Tensor.ringSheaf (toRingedSite X).O)))}
    (hK : RingedSite.IsDerivedComplete.{u, u, u, u} (toRingedSite X) I' K) :
    IsIso ((RingedSite.derivedCompletionPushforwardComparison
      (toRingedSiteHom f) I I' hI).app K)

AlgebraicGeometry.Scheme.isDerivedComplete_derivedPushforward_derivedCompletion_of_isFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionFiniteType.lean, line 321. The attribute's comment: “the left hand side Rf_*(ℱ^∧) of Equation 52.7.0.1 is derived complete along ℐ, for an arbitrary object, at a morphism of schemes — the display's own setting — and at the source's own data: a sheaf of ideals ℐ ⊆ 𝒪_S of finite type, with the completion on X taken along a sheaf of ideals ℐ' of finite type receiving f^♯(f^{-1}ℐ), as the display's f^{-1}ℐ · 𝒪_X does. The derived completion functor is produced from the finite-type hypothesis by [Stacks, Tag 099F], so no part of that tag is an input; quasi-coherence of ℐ and of ℱ is not needed, those entering the source only through that tag”.

[Stacks, Tag 0A0I], the left hand side of the display, in the display's own setting and at the source's own data. Let f : X ⟶ S be a morphism of schemes, ℐ ⊆ 𝒪_S a sheaf of ideals of finite type and ℐ' ⊆ 𝒪_X a sheaf of ideals of finite type with f^♯(f^{-1}ℐ) ⊆ ℐ', which the display's f^{-1}ℐ · 𝒪_X is. Then Rf_*(ℱ^∧) is derived complete along ℐ for an arbitrary ℱ ∈ D(𝒪_X).

Quasi-coherence of ℐ and of ℱ is not needed, and the derived completion functor on D(𝒪_X) is produced from the finite-type hypothesis by [Stacks, Tag 099F].

theorem isDerivedComplete_derivedPushforward_derivedCompletion_of_isFiniteType
    [I'.toSheafOfModules.IsFiniteType]
    (K : DerivedCategory (_root_.SheafOfModules.{u}
      ((Stacks.SheafOfModules.Tensor.ringSheaf
        (Stacks.RingedSpace.toRingedSite X.toRingedSpace).O)))) :
    RingedSite.IsDerivedComplete.{u, u, u, u}
        (Stacks.RingedSpace.toRingedSite S.toRingedSpace) I
      ((@derivedPushforward.{u} _ _ _ _ _ _ _ (toRingedSiteHom f).toRingedToposSiteHom (_) (_)).obj
        ((RingedSite.derivedCompletion
          (Stacks.RingedSpace.toRingedSite X.toRingedSpace) I').obj K))

AlgebraicGeometry.Scheme.isIso_derivedCompletionPushforwardComparison_of_isFiniteType_of_isDerivedComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionFiniteType.lean, line 387. The attribute's comment: “Equation 52.7.0.1 in the display's own setting, a morphism of schemes, for a derived-complete object, at the source's own data: a sheaf of ideals ℐ ⊆ 𝒪_S of finite type and a sheaf of ideals ℐ' ⊆ 𝒪_X of finite type with f^♯(f^{-1}ℐ) ⊆ ℐ', as the display's pair ℐ, f^{-1}ℐ · 𝒪_X is. Both derived completion functors are produced from those finite-type hypotheses by [Stacks, Tag 099F], so no part of that tag is an input, and quasi-coherence of ℐ and of ℱ is not needed — in the source those enter only through that tag — so the statement covers every quasi-coherent ℐ of finite type and every quasi-coherent ℱ derived complete along ℐ'. The display for an arbitrary object is the invertibility half of [Stacks, Tag 0A0G]”.

Equation 52.7.0.1 of [Stacks, Tag 0A0I] in the display's own setting and at the source's own data, for a derived-complete object. Let f : X ⟶ S be a morphism of schemes, let ℐ ⊆ 𝒪_S be a sheaf of ideals of finite type and let ℐ' ⊆ 𝒪_X be a sheaf of ideals of finite type with f^♯(f^{-1}ℐ) ⊆ ℐ' — which the display's f^{-1}ℐ · 𝒪_X is. Then (Rf_*ℱ)^∧ ⟶ Rf_*(ℱ^∧) is invertible for every ℱ ∈ D(𝒪_X) derived complete along ℐ'.

This is the display at the hypotheses Section 52.7 writes it under. The source asks ℐ to be a quasi-coherent sheaf of ideals of finite type and ℱ to be quasi-coherent, and uses those hypotheses only through [Stacks, Tag 099F], to know the two derived completion functors exist; here finite type alone produces them, by Stacks.RingedSpace.isRightAdjoint_ι_isDerivedComplete_of_isFiniteType, so quasi-coherence is not needed and the statement applies in particular to every quasi-coherent ℐ of finite type and every complex of quasi-coherent modules derived complete along ℐ'.

Because ℱ ranges over all the objects of D(𝒪_X) derived complete along ℐ', this is also the analogue of the display for complexes of quasi-coherent modules that the fifth and last sentence of [Stacks, Tag 0AKL] attributes to [HL-P, Theorem 6.5], at a morphism of schemes. At a morphism of algebraic stacks, for an arbitrary object, that analogue is AlgebraicGeometry.Stack.isIso_derivedCompletionPushforwardComparison_of_isAlgebraicStack of PushforwardCommutesCompletionAlgebraicStacks.lean; derived algebraic stacks, the other half of the setting of that reference, are not defined in this library.

The restriction to a derived-complete ℱ is on the object, not on the data: the invertibility for an arbitrary ℱ is the assertion of [Stacks, Tag 0A0G], and it is proved — at a morphism of ringed sites and at the constructed ℐ' = f^{-1}ℐ · 𝒪_X rather than at an independent parameter ℐ' — by RingedSite.isIso_derivedCompletionPushforwardComparison_inverseImageIdealSheaf_of_isFiniteType, and at a morphism of schemes and a quasi-coherent ℐ of finite type by Scheme.isIso_derivedCompletionPushforwardComparison_idealSheafData_inverseImageIdealSheaf.

theorem isIso_derivedCompletionPushforwardComparison_of_isFiniteType_of_isDerivedComplete
    [I.toSheafOfModules.IsFiniteType] [I'.toSheafOfModules.IsFiniteType]
    {K : DerivedCategory (_root_.SheafOfModules.{u}
      ((Stacks.SheafOfModules.Tensor.ringSheaf
        (Stacks.RingedSpace.toRingedSite X.toRingedSpace).O)))}
    (hK : RingedSite.IsDerivedComplete.{u, u, u, u}
      (Stacks.RingedSpace.toRingedSite X.toRingedSpace) I' K) :
    IsIso ((RingedSite.derivedCompletionPushforwardComparison
      (toRingedSiteHom f) I I' hI).app K)

AlgebraicGeometry.Scheme.isDerivedComplete_derivedPushforward_derivedCompletion_idealSheafData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionFiniteType.lean, line 432. The attribute's comment: “the left hand side Rf_*(ℱ^∧) of Equation 52.7.0.1 is derived complete along ℐ, for an arbitrary object, at Section 52.7's own data: a morphism of schemes, a quasi-coherent sheaf of ideals ℐ ⊆ 𝒪_S of finite type — an AlgebraicGeometry.Scheme.IdealSheafData whose ringed-site reading is of finite type — and the completion on X taken along a quasi-coherent sheaf of ideals ℐ' of finite type receiving f^♯(f^{-1}ℐ), as the display's f^{-1}ℐ · 𝒪_X does. The derived completion functor is produced from the finite-type hypothesis by [Stacks, Tag 099F], so no part of that tag is an input; on a locally Noetherian scheme the finite-type hypothesis is itself automatic”.

[Stacks, Tag 0A0I], the left hand side of the display, at Section 52.7's own data: quasi-coherent sheaves of ideals of finite type. Let f : X ⟶ S be a morphism of schemes, let ℐ ⊆ 𝒪_S be a quasi-coherent sheaf of ideals of finite type and let ℐ' ⊆ 𝒪_X be a quasi-coherent sheaf of ideals of finite type with f^♯(f^{-1}ℐ) ⊆ ℐ', which the display's f^{-1}ℐ · 𝒪_X is. Then Rf_*(ℱ^∧) is derived complete along ℐ for an arbitrary ℱ ∈ D(𝒪_X).

A quasi-coherent sheaf of ideals is an AlgebraicGeometry.Scheme.IdealSheafData, read on the small Zariski ringed site by Stacks.Algebraization.idealSheafSiteSubmodule; "of finite type" is SheafOfModules.IsFiniteType, which is the source's hypothesis — locally generated by finitely many sections. On a locally Noetherian scheme it is automatic, by the instance Stacks.Algebraization.isFiniteType_idealSheafSiteSubmodule, so there the two binders need no argument.

theorem isDerivedComplete_derivedPushforward_derivedCompletion_idealSheafData
    [(idealSheafSiteSubmodule I').toSheafOfModules.IsFiniteType]
    (K : DerivedCategory (_root_.SheafOfModules.{u}
      ((Stacks.SheafOfModules.Tensor.ringSheaf
        (Stacks.RingedSpace.toRingedSite X.toRingedSpace).O)))) :
    RingedSite.IsDerivedComplete.{u, u, u, u}
        (Stacks.RingedSpace.toRingedSite S.toRingedSpace) (idealSheafSiteSubmodule I)
      ((@derivedPushforward.{u} _ _ _ _ _ _ _ (toRingedSiteHom f).toRingedToposSiteHom (_) (_)).obj
        ((RingedSite.derivedCompletion (Stacks.RingedSpace.toRingedSite X.toRingedSpace)
          (idealSheafSiteSubmodule I')).obj K))

AlgebraicGeometry.Scheme.isIso_derivedCompletionPushforwardComparison_idealSheafData_of_isDerivedComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionFiniteType.lean, line 496. The attribute's comment: “Equation 52.7.0.1 at Section 52.7's own data, for a derived-complete object: a morphism of schemes f : X ⟶ S, a quasi-coherent sheaf of ideals ℐ ⊆ 𝒪_S of finite type and a quasi-coherent sheaf of ideals ℐ' ⊆ 𝒪_X of finite type with f^♯(f^{-1}ℐ) ⊆ ℐ', as the display's pair ℐ, f^{-1}ℐ · 𝒪_X is. A quasi-coherent sheaf of ideals is an AlgebraicGeometry.Scheme.IdealSheafData read on the small Zariski ringed site, and of finite type is SheafOfModules.IsFiniteType, locally generated by finitely many sections, which is the source's own hypothesis; on a locally Noetherian scheme it is automatic. Both derived completion functors are produced from it by [Stacks, Tag 099F], so no part of that tag is an input. The display for an arbitrary object is the invertibility half of [Stacks, Tag 0A0G]”.

Equation 52.7.0.1 of [Stacks, Tag 0A0I] at Section 52.7's own data, for a derived-complete object. Let f : X ⟶ S be a morphism of schemes, let ℐ ⊆ 𝒪_S be a quasi-coherent sheaf of ideals of finite type and let ℐ' ⊆ 𝒪_X be a quasi-coherent sheaf of ideals of finite type with f^♯(f^{-1}ℐ) ⊆ ℐ' — which the display's f^{-1}ℐ · 𝒪_X is. Then (Rf_*ℱ)^∧ ⟶ Rf_*(ℱ^∧) is invertible for every ℱ ∈ D(𝒪_X) derived complete along ℐ', in particular for every such complex of quasi-coherent modules.

This is the display written at the hypotheses Section 52.7 states it under, in the library's own scheme-theoretic vocabulary: ℐ and ℐ' are AlgebraicGeometry.Scheme.IdealSheafData, so quasi-coherent, and the finite-type hypothesis is SheafOfModules.IsFiniteType — locally generated by finitely many sections. It is isIso_derivedCompletionPushforwardComparison_of_isFiniteType_of_isDerivedComplete above at those sheaves of ideals, and the only thing the hypotheses are used for is [Stacks, Tag 099F], which is what produces the two derived completion functors.

Because ℱ ranges over the objects of D(𝒪_X) derived complete along ℐ' and not over quasi-coherent sheaves alone, this is also the analogue of the display for complexes of quasi-coherent modules that the fifth and last sentence of [Stacks, Tag 0AKL] attributes to [HL-P, Theorem 6.5], at a morphism of schemes.

The restriction to a derived-complete ℱ is on the object, not on the data: the invertibility for an arbitrary ℱ is the assertion of [Stacks, Tag 0A0G], and it is proved — at a morphism of ringed sites and at the constructed ℐ' = f^{-1}ℐ · 𝒪_X rather than at an independent parameter ℐ' — by RingedSite.isIso_derivedCompletionPushforwardComparison_inverseImageIdealSheaf_of_isFiniteType, and at a morphism of schemes and a quasi-coherent ℐ of finite type by Scheme.isIso_derivedCompletionPushforwardComparison_idealSheafData_inverseImageIdealSheaf.

theorem isIso_derivedCompletionPushforwardComparison_idealSheafData_of_isDerivedComplete
    [(idealSheafSiteSubmodule I).toSheafOfModules.IsFiniteType]
    [(idealSheafSiteSubmodule I').toSheafOfModules.IsFiniteType]
    {K : DerivedCategory (_root_.SheafOfModules.{u}
      ((Stacks.SheafOfModules.Tensor.ringSheaf
        (Stacks.RingedSpace.toRingedSite X.toRingedSpace).O)))}
    (hK : RingedSite.IsDerivedComplete.{u, u, u, u}
      (Stacks.RingedSpace.toRingedSite X.toRingedSpace) (idealSheafSiteSubmodule I') K) :
    IsIso ((RingedSite.derivedCompletionPushforwardComparison
      (toRingedSiteHom f) (idealSheafSiteSubmodule I) (idealSheafSiteSubmodule I') hI).app K)

AlgebraicGeometry.Scheme.isIso_derivedCompletionPushforwardComparison_idealSheafData_inverseImageIdealSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionFiniteType.lean, line 559. The attribute's comment: “Equation 52.7.0.1 in the display's own setting and at Section 52.7's own data, for an arbitrary object, as an invertibility of the canonical comparison map (Rf_*ℱ)^∧ ⟶ Rf_*(ℱ^∧): a morphism of schemes f : X ⟶ S, a quasi-coherent sheaf of ideals ℐ ⊆ 𝒪_S of finite type — an AlgebraicGeometry.Scheme.IdealSheafData read on the small Zariski ringed site — and the completion on X taken along the sheaf of ideals f^{-1}ℐ · 𝒪_X built out of ℐ, the image of f^*ℐ ⟶ 𝒪_X. No restriction on ℱ: every object of D(𝒪_X), in particular every quasi-coherent ℱ. That f^♯(f^{-1}ℐ) ⊆ f^{-1}ℐ · 𝒪_X and that this sheaf of ideals is of finite type, so that [Stacks, Tag 099F] produces the derived completion along it, are theorems about the construction, not hypotheses”.

Equation 52.7.0.1 of [Stacks, Tag 0A0I] at Section 52.7's own data, for an arbitrary object — and so the analogue for complexes of quasi-coherent modules of [Stacks, Tag 0AKL]. Let f : X ⟶ S be a morphism of schemes, let ℐ ⊆ 𝒪_S be a quasi-coherent sheaf of ideals of finite type and let ℐ' = f^{-1}ℐ · 𝒪_X be the sheaf of ideals Section 52.7 builds out of it. Then the canonical comparison map

(Rf_*K)^∧ ⟶ Rf_*(K^∧)

is invertible for every object K of D(𝒪_X), the completion on S being taken along ℐ and the one on X along ℐ'. In particular it is invertible for every complex of quasi-coherent 𝒪_X-modules, with no derived-completeness or nilpotence restriction.

ℐ is an AlgebraicGeometry.Scheme.IdealSheafData, read on the small Zariski ringed site by Stacks.Algebraization.idealSheafSiteSubmodule, and "of finite type" is SheafOfModules.IsFiniteType (automatic on a locally Noetherian scheme, by Stacks.Algebraization.isFiniteType_idealSheafSiteSubmodule). The sheaf of ideals ℐ' is AlgebraicGeometry.RingedSite.inverseImageIdealSheaf, the image of f^*ℐ ⟶ 𝒪_X; that f^♯ carries f^{-1}ℐ into it is AlgebraicGeometry.RingedSite.pushforwardIdealCompatible_inverseImageIdealSheaf, and that it is of finite type — so that the derived completion along it exists, by [Stacks, Tag 099F] — is AlgebraicGeometry.RingedSite.isFiniteType_inverseImageIdealSheaf. Neither is a hypothesis.

This is RingedSite.isIso_derivedCompletionPushforwardComparison_inverseImageIdealSheaf_of_isFiniteType, the ringed-sites case of [Stacks, Tag 0A0G], at the morphism of ringed sites AlgebraicGeometry.Scheme.toRingedSiteHom f underlying f.

theorem isIso_derivedCompletionPushforwardComparison_idealSheafData_inverseImageIdealSheaf
    [(idealSheafSiteSubmodule I).toSheafOfModules.IsFiniteType]
    (K : DerivedCategory (_root_.SheafOfModules.{u}
      ((Stacks.SheafOfModules.Tensor.ringSheaf
        (Stacks.RingedSpace.toRingedSite X.toRingedSpace).O)))) :
    IsIso ((RingedSite.derivedCompletionPushforwardComparison (toRingedSiteHom f)
      (idealSheafSiteSubmodule I)
      (RingedSite.inverseImageIdealSheaf.{u} (toRingedSiteHom f) (idealSheafSiteSubmodule I))
      (RingedSite.pushforwardIdealCompatible_inverseImageIdealSheaf.{u} (toRingedSiteHom f)
        (idealSheafSiteSubmodule I))).app K)

AlgebraicGeometry.RingedSite.isDerivedComplete_derivedPushforward_derivedCompletion_generatedIdealSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionGenerated.lean, line 172. The attribute's comment: “the left hand side Rf_*(ℱ^∧) of Equation 52.7.0.1 is derived complete along ℐ, for an arbitrary object, at a morphism of ringed sites whose two sheaves of ideals are generated by finitely many global sections of the respective structure sheaves. The derived completion functor is produced from those generators, by AlgebraicGeometry.RingedSite.isRightAdjoint_ι_isDerivedComplete_generatedIdealSheaf, and not assumed, so no part of [Stacks, Tag 099F] is a hypothesis. What is restricted is the data: the source's ℐ is of finite type, hence only locally generated by finitely many sections. That case is proved, at a morphism of ringed spaces and at a morphism of schemes, in PushforwardCommutesCompletionFiniteType.lean, where [Stacks, Tag 099F] at a sheaf of ideals of finite type produces the derived completion functor”.

[Stacks, Tag 0A0I], the left hand side of the display, at ideal sheaves generated by global sections. Rf_*(K^∧) is derived complete along ℐ = (t_1, …, t_s), for an arbitrary K ∈ D(𝒪'), the completion being taken along ℐ' = (g_1, …, g_r).

This is AlgebraicGeometry.RingedSite.isDerivedComplete_derivedPushforward_derivedCompletion with its instance hypothesis discharged: the derived completion functor on D(𝒪') is produced from the generators by isRightAdjoint_ι_isDerivedComplete_generatedIdealSheaf, so nothing of [Stacks, Tag 099F] is assumed. The mathematical content is [Stacks, Tag 099J], that Rf_* preserves derived completeness, applied to the derived-complete object K^∧.

What is restricted is the data — the source's ℐ is of finite type, hence only locally generated by finitely many sections — and not the object.

theorem isDerivedComplete_derivedPushforward_derivedCompletion_generatedIdealSheaf
    (K : DerivedCategory (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O)))) :
    IsDerivedComplete.{u, u, u, u} Y (generatedIdealSheaf t)
      ((derivedPushforward.{u} f.toRingedToposSiteHom).obj
        ((derivedCompletion X (generatedIdealSheaf g)).obj K))

AlgebraicGeometry.RingedSite.isIso_derivedCompletionPushforwardComparison_generatedIdealSheaf_of_isDerivedComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionGenerated.lean, line 276. The attribute's comment: “Equation 52.7.0.1 at a morphism of ringed sites, for a derived-complete object, with the two sheaves of ideals generated by finitely many global sections and both derived completion functors produced from those generators. The display at the source's own data, sheaves of ideals of finite type, is in PushforwardCommutesCompletionFiniteType.lean, at a morphism of ringed spaces and at a morphism of schemes; the display for an arbitrary object is the invertibility half of [Stacks, Tag 0A0G]”.

[Stacks, Tags 0A0G and 0A0I] at a derived-complete object, with nothing assumed. At ideal sheaves generated by finitely many global sections, the comparison map (Rf_*K)^∧ ⟶ Rf_*(K^∧) is invertible for every K ∈ D(𝒪') that is derived complete along ℐ', so that Rf_*(K^∧) = Rf_*K = (Rf_*K)^∧ there.

This is isIso_derivedCompletionPushforwardComparison_of_isDerivedComplete with both instance hypotheses discharged from the generators. What it asks of the object it does not ask of the data: the two generating families are independent, related only by hI. For an arbitrary object the two families have to correspond, g_i = f^♯(t_i), and then the display holds by AlgebraicGeometry.RingedSite.isIso_derivedCompletionPushforwardComparison_generatedIdealSheaf of PushforwardCommutesCompletionCanonical.lean.

theorem isIso_derivedCompletionPushforwardComparison_generatedIdealSheaf_of_isDerivedComplete
    {K : DerivedCategory (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O)))}
    (hK : IsDerivedComplete.{u, u, u, u} X (generatedIdealSheaf g) K) :
    IsIso ((derivedCompletionPushforwardComparison f (generatedIdealSheaf t)
      (generatedIdealSheaf g) hI).app K)

Stacks.RingedSpace.isDerivedComplete_derivedPushforward_derivedCompletion_generatedIdealSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionGenerated.lean, line 342. The attribute's comment: “the left hand side Rf_*(ℱ^∧) of Equation 52.7.0.1 is derived complete along ℐ, for an arbitrary object, at a morphism of ringed spaces read on its small Zariski sites, with the two sheaves of ideals generated by finitely many global sections. The derived completion functor is produced from those generators rather than assumed. The source's ℐ is quasi-coherent of finite type, hence only locally generated by finitely many sections; that case is Stacks.RingedSpace``.isDerivedComplete_derivedPushforward_derivedCompletion_of_isFiniteType of PushforwardCommutesCompletionFiniteType.lean, where the derived completion functor comes from [Stacks, Tag 099F] at a sheaf of ideals of finite type”.

[Stacks, Tag 0A0I], the left hand side of the display, at a morphism of ringed spaces and ideal sheaves generated by global sections. Rf_*(ℱ^∧) is derived complete along ℐ = (t_1, …, t_s), for an arbitrary ℱ ∈ D(𝒪_X).

This is the ringed-site statement RingedSite.isDerivedComplete_derivedPushforward_derivedCompletion_generatedIdealSheaf read at the small Zariski sites of X and Y. Nothing is assumed: the derived completion functor on D(𝒪_X) is produced from the generators of ℐ'.

theorem isDerivedComplete_derivedPushforward_derivedCompletion_generatedIdealSheaf
    (K : DerivedCategory (_root_.SheafOfModules.{u}
      ((Stacks.SheafOfModules.Tensor.ringSheaf (toRingedSite X).O)))) :
    RingedSite.IsDerivedComplete.{u, u, u, u} (toRingedSite Y) (generatedIdealSheaf t)
      ((derivedPushforward.{u} (toRingedSiteHom f).toRingedToposSiteHom).obj
        ((RingedSite.derivedCompletion (toRingedSite X) (generatedIdealSheaf g)).obj K))

Stacks.RingedSpace.isIso_derivedCompletionPushforwardComparison_generatedIdealSheaf_of_isDerivedComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionGenerated.lean, line 375. The attribute's comment: “Equation 52.7.0.1 at a morphism of ringed spaces read on its small Zariski sites, for a derived-complete object, with the two sheaves of ideals generated by finitely many global sections and both derived completion functors produced from those generators rather than assumed. The display at the source's own data, two sheaves of ideals of finite type, is Stacks.RingedSpace``.isIso_derivedCompletionPushforwardComparison_of_isFiniteType_of_isDerivedComplete of PushforwardCommutesCompletionFiniteType.lean, of which this is the globally generated case; the display for an arbitrary object is the invertibility half of [Stacks, Tag 0A0G]”.

[Stacks, Tag 0A0I] at a morphism of ringed spaces, for a derived-complete object, with nothing assumed. For ideal sheaves generated by finitely many global sections, the comparison (Rf_*ℱ)^∧ ⟶ Rf_*(ℱ^∧) is invertible whenever ℱ is derived complete along ℐ'.

This is RingedSite.isIso_derivedCompletionPushforwardComparison_generatedIdealSheaf_of_isDerivedComplete read at the small Zariski sites; both derived completion functors are produced from the generators, so no part of [Stacks, Tag 099F] is a hypothesis. The restriction to a derived-complete ℱ is the tag's own content and remains; the invertibility for an arbitrary ℱ is the assertion of [Stacks, Tag 0A0G].

The same statement at the source's own data, two sheaves of ideals of finite type, is isIso_derivedCompletionPushforwardComparison_of_isFiniteType_of_isDerivedComplete of PushforwardCommutesCompletionFiniteType.lean; this one is the case of it in which the sheaves of ideals are generated by global sections, by Stacks.RingedSpace.isFiniteType_generatedIdealSheaf there.

theorem isIso_derivedCompletionPushforwardComparison_generatedIdealSheaf_of_isDerivedComplete
    {K : DerivedCategory (_root_.SheafOfModules.{u}
      ((Stacks.SheafOfModules.Tensor.ringSheaf (toRingedSite X).O)))}
    (hK : RingedSite.IsDerivedComplete.{u, u, u, u} (toRingedSite X)
      (generatedIdealSheaf g) K) :
    IsIso ((RingedSite.derivedCompletionPushforwardComparison (toRingedSiteHom f)
      (generatedIdealSheaf t) (generatedIdealSheaf g) hI).app K)

AlgebraicGeometry.Scheme.isIso_derivedCompletionPushforwardComparison_generatedIdealSheaf_of_isDerivedComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionGenerated.lean, line 472. The attribute's comment: “Equation 52.7.0.1 in the display's own setting, a morphism of schemes, for a derived-complete object, with the two sheaves of ideals generated by finitely many global sections of the structure sheaves. Both derived completion functors are produced from those generators rather than assumed, so no part of [Stacks, Tag 099F] is a hypothesis, and neither quasi-coherence nor finite type of ℐ nor quasi-coherence of ℱ is needed. The display at the source's own data, two sheaves of ideals of finite type, is AlgebraicGeometry.Scheme``.isIso_derivedCompletionPushforwardComparison_of_isFiniteType_of_isDerivedComplete of PushforwardCommutesCompletionFiniteType.lean, of which this is the globally generated case; the display for an arbitrary object is the invertibility half of [Stacks, Tag 0A0G]”.

[Stacks, Tag 0A0I] in the display's own setting, for a derived-complete object, with nothing assumed. Let f : X ⟶ S be a morphism of schemes, let ℐ = (t_1, …, t_s) ⊆ 𝒪_S and ℐ' = (g_1, …, g_r) ⊆ 𝒪_X be the sheaves of ideals generated by finitely many global sections of the two structure sheaves, with f^♯(f^{-1}ℐ) ⊆ ℐ' — which the display's f^{-1}ℐ · 𝒪_X satisfies. Then (Rf_*ℱ)^∧ ⟶ Rf_*(ℱ^∧) is invertible for every ℱ ∈ D(𝒪_X) derived complete along ℐ'.

Both derived completion functors are produced from the generators, by AlgebraicGeometry.RingedSite.isRightAdjoint_ι_isDerivedComplete_generatedIdealSheaf, so [Stacks, Tag 099F] is nowhere a hypothesis; neither quasi-coherence nor finite type nor quasi-coherence of ℱ is assumed either, those entering the source only through that tag. The restriction to a derived-complete ℱ is the tag's own content and remains; the invertibility for an arbitrary ℱ is the assertion of [Stacks, Tag 0A0G]. The descent from a globally generated ℐ to a finite-type one is carried out in PushforwardCommutesCompletionFiniteType.lean, where the derived completion functors come from [Stacks, Tag 099F] at a sheaf of ideals of finite type; this statement is the case of AlgebraicGeometry.Scheme .isIso_derivedCompletionPushforwardComparison_of_isFiniteType_of_isDerivedComplete there in which the two sheaves of ideals are generated by global sections.

Because ℱ ranges over the derived-complete objects of D(𝒪_X) and not over quasi-coherent sheaves alone, this is also the analogue of the display for complexes of quasi-coherent modules that the fifth and last sentence of [Stacks, Tag 0AKL] attributes to [HL-P, Theorem 6.5]; related statements are isIso_derivedCompletionPushforwardComparison_of_isFiniteType_of_isDerivedComplete of PushforwardCommutesCompletionFiniteType.lean, the same statement at two sheaves of ideals of finite type, and AlgebraicGeometry.Scheme.isIso_derivedCompletionPushforwardComparison_of_forall_isNilpotent of PushforwardCommutesCompletionSpaces.lean, which takes an arbitrary object in the nilpotent regime and whose module documentation accounts for the remark sentence by sentence.

theorem isIso_derivedCompletionPushforwardComparison_generatedIdealSheaf_of_isDerivedComplete
    {K : DerivedCategory (_root_.SheafOfModules.{u}
      ((Stacks.SheafOfModules.Tensor.ringSheaf
        (Stacks.RingedSpace.toRingedSite X.toRingedSpace).O)))}
    (hK : RingedSite.IsDerivedComplete.{u, u, u, u}
      (Stacks.RingedSpace.toRingedSite X.toRingedSpace) (generatedIdealSheaf g) K) :
    IsIso ((RingedSite.derivedCompletionPushforwardComparison (toRingedSiteHom f)
      (generatedIdealSheaf t) (generatedIdealSheaf g) hI).app K)

AlgebraicGeometry.RingedSite.nonempty_iso_derivedPushforward_derivedCompletion_generatedIdealSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionHomTower.lean, line 242. The attribute's comment: “Equation 52.7.0.1 for an arbitrary object of D(𝒪'), at any morphism of ringed sites and at sheaves of ideals ℐ = (t_1, …, t_r) ⊂ 𝒪 and ℐ' = (f^♯t_1, …, f^♯t_r) ⊂ 𝒪' generated by finitely many global sections, out of which both derived completion functors are built, so that no part of [Stacks, Tag 099F] is an input. The equation is obtained as the source obtains it, from the Koszul Hom-tower presentation of the two completions, the exchange of Rf_* with R lim, and the identification of the two towers through the adjoint formula Rf_* R𝓗om_{𝒪'}(Lf^*-, M) ≅ R𝓗om_𝒪(-, Rf_*M) and the pulled-back Koszul complexes. What is restricted is the data; the object ranges over all of D(𝒪')”.

[Stacks, Tags 0A0G and 0A0I] for an arbitrary object, at two sheaves of ideals generated by finitely many global sections. Let f : (Sh(𝒟), 𝒪') ⟶ (Sh(𝒞), 𝒪) be a morphism of ringed sites, let t_1, …, t_r be global sections of 𝒪 generating ℐ ⊂ 𝒪, let g_1, …, g_r be global sections of 𝒪' with g_i = f^♯(t_i) generating ℐ' ⊂ 𝒪', and let K ∈ D(𝒪') be arbitrary. Then

Rf_*(K^∧) ≅ (Rf_*K)^∧:

Rf_* commutes with derived completion. Both derived completion functors are the reflector of [Stacks, Tag 099F], produced from the generators by AlgebraicGeometry.RingedSite.isRightAdjoint_ι_isDerivedComplete_generatedIdealSheaf, so no part of that tag is an input here.

The proof is the source's own. K^∧ is the derived limit of the Koszul Hom tower n ↦ R𝓗om_{𝒪'}(K(𝒪', g^{n+1}), K) by isDerivedLimit_derivedSheafHomSystem_derivedCompletion ([Stacks, Tag 0A0E]); Rf_* carries that derived limit to one of the pushed-forward tower by Stacks.Cohomology.DerivedPushforwardOnRingedTopoi.isDerivedLimit_map_derivedPushforward ([Stacks, Tag 0A07]); derivedPushforwardKoszulSheafHomSystemIso identifies the pushed-forward tower with n ↦ R𝓗om_𝒪(K(𝒪, t^{n+1}), Rf_*K), whose derived limit is (Rf_*K)^∧ by the same presentation on the target; and two derived limits of isomorphic towers are isomorphic, by Rlim.Pro.nonempty_iso_of_isDerivedLimit_of_natIso ([Stacks, Tag 0H9L]).

The conclusion is the display as the source writes it, an isomorphism of the two objects, rather than invertibility of the canonical comparison map AlgebraicGeometry.RingedSite.derivedCompletionPushforwardComparison: the uniqueness of derived limits produces a non-canonical isomorphism. The source's ℐ is of finite type, hence only locally generated by finitely many sections; [Stacks, Tag 099F] at such an ℐ rests on [Stacks, Tags 099D and 099E].

theorem nonempty_iso_derivedPushforward_derivedCompletion_generatedIdealSheaf
    (K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    [HasCoproduct ((koszulPowerSystem X g ⋙ DerivedCategory.Q).obj)]
    [HasCoproduct ((koszulPowerSystem Y t ⋙ DerivedCategory.Q).obj)] :
    Nonempty ((derivedPushforward.{u} f.toRingedToposSiteHom).obj
        ((derivedCompletion X (generatedIdealSheaf g)).obj K) ≅
      (derivedCompletion Y (generatedIdealSheaf t)).obj
        ((derivedPushforward.{u} f.toRingedToposSiteHom).obj K))

AlgebraicGeometry.RingedSite.nonempty_iso_derivedPushforward_derivedCompletion_pushGlobalSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionHomTower.lean, line 381. The attribute's comment: “Equation 52.7.0.1 for an arbitrary object of D(𝒪'), at the display's own pair of sheaves of ideals: ℐ = (t_1, …, t_r) ⊂ 𝒪 generated by finitely many global sections and ℐ' = f^{-1}ℐ · 𝒪_X, the latter constructed from f and t as the ideal sheaf generated by f^♯t_1, …, f^♯t_r and characterised as the least one receiving f^♯(f^{-1}ℐ). The morphism of ringed sites carries a terminal object of the target site to a terminal object, as at ringed spaces and at schemes, and nothing further is asked of it; both derived completion functors are built from the generators of ℐ, so no part of [Stacks, Tag 099F] is an input. The object ranges over all of D(𝒪')”.

[Stacks, Tags 0A0G and 0A0I] for an arbitrary object, at the source's own ideal sheaf ℐ' = f^{-1}ℐ · 𝒪_X. Let f : (Sh(𝒟), 𝒪') ⟶ (Sh(𝒞), 𝒪) be a morphism of ringed sites carrying a terminal object T of the target site to a terminal object, let ℐ = (t_1, …, t_r) ⊂ 𝒪 be generated by finitely many global sections, and let K ∈ D(𝒪') be arbitrary. Then

Rf_*(K^∧) ≅ (Rf_*K)^∧,

the completion on the source being taken along the ideal sheaf generated by f^♯t_1, …, f^♯t_r.

That ideal sheaf is the source's ℐ' = f^{-1}ℐ · 𝒪_X: it receives f^♯(f^{-1}ℐ), by AlgebraicGeometry.RingedSite.pushforwardIdealCompatible_pushGlobalSections, and is least among those that do, by AlgebraicGeometry.RingedSite.generatedIdealSheaf_pushGlobalSections_le, which together pin it down — AlgebraicGeometry.RingedSite.eq_generatedIdealSheaf_pushGlobalSections. So the relation between the two sheaves of ideals is built from f and t here rather than given, and the statement depends only on f, on the two terminal objects and on t.

The terminal objects are what makes a global section of 𝒪 transportable along a general morphism of sites: f^♯ produces sections only over objects in the image of f.u, and a section over a terminal object is a global section. They are present at ringed spaces and at schemes, where f.u is Opens.map and carries ⊤ to ⊤.

This is nonempty_iso_derivedPushforward_derivedCompletion_generatedIdealSheaf at g = pushGlobalSections f hT' t, whose relation to t is pushGlobalSectionsCompatible_pushGlobalSections.

theorem nonempty_iso_derivedPushforward_derivedCompletion_pushGlobalSections
    (K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    [HasCoproduct ((koszulPowerSystem X (pushGlobalSections f hT' t) ⋙
      DerivedCategory.Q).obj)]
    [HasCoproduct ((koszulPowerSystem Y t ⋙ DerivedCategory.Q).obj)] :
    Nonempty ((derivedPushforward.{u} f.toRingedToposSiteHom).obj
        ((derivedCompletion X (generatedIdealSheaf (pushGlobalSections f hT' t))).obj K) ≅
      (derivedCompletion Y (generatedIdealSheaf t)).obj
        ((derivedPushforward.{u} f.toRingedToposSiteHom).obj K))

AlgebraicGeometry.RingedSite.isIso_derivedCompletionPushforwardComparison_inverseImageIdealSheaf_of_isFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionLocalToGlobal.lean, line 266. The attribute's comment: “Equation 52.7.0.1 as an invertibility of the canonical comparison map (Rf_*ℱ)^∧ ⟶ Rf_*(ℱ^∧), for an arbitrary object of D(𝒪'), at a sheaf of ideals of finite type and the ideal sheaf f^{-1}ℐ · 𝒪_X that Section 52.7 builds out of it. The two sides of the equation are therefore identified by the map [Stacks, Tag 0A0G] names, and not merely abstractly isomorphic”.

[Stacks, Tag 0A0G] at a sheaf of ideals of finite type, for an arbitrary object. Let f : (Sh(𝒟), 𝒪') ⟶ (Sh(𝒞), 𝒪) be a morphism of ringed sites, let ℐ ⊂ 𝒪 be a sheaf of ideals of finite type and let ℐ' = f^{-1}ℐ · 𝒪_X be the ideal sheaf Section 52.7 builds out of ℐ. Then the canonical comparison map

(Rf_*K)^∧ ⟶ Rf_*(K^∧)

is invertible for every object K of D(𝒪'), the completion on the target being taken along ℐ and the one on the source along ℐ'.

The proof is the source's own localization. ℐ of finite type is generated by finitely many sections above a covering family {V_i} of the final object of the target site (exists_coversTop_eq_generatedIdealSheaf_of_isFiniteType); on each 𝒟/V_i the comparison map of the localized morphism of [Stacks, Tag 04J0] at (ℐ|_{V_i}, ℐ'|_{u(V_i)}) is invertible, because both of those sheaves of ideals are globally generated there (isIso_derivedCompletionPushforwardComparison_localized_overIdeal); the restriction coherence derivedCompletionPushforwardComparison_localized identifies the restriction of the comparison map of f with it up to three isomorphisms — the two comparison maps of [Stacks, Tag 0A0F], invertible because ℐ and ℐ' are of finite type, and [Stacks, Tag 0D6G]; and invertibility in the derived category of sheaves of modules is local on the site (Stacks.SheafOfModules.isIso_of_coversTop_mapDerivedCategory).

Finite type of ℐ' is not a hypothesis: it is AlgebraicGeometry.RingedSite.isFiniteType_inverseImageIdealSheaf, and it is what makes the derived completion functor along ℐ' exist at all, by [Stacks, Tag 099F].

theorem isIso_derivedCompletionPushforwardComparison_inverseImageIdealSheaf_of_isFiniteType
    (K : DerivedCategory (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O)))) :
    IsIso ((derivedCompletionPushforwardComparison f I (inverseImageIdealSheaf f I)
      (pushforwardIdealCompatible_inverseImageIdealSheaf f I)).app K)

Stacks.RingedSpace.isIso_derivedCompletionPushforwardComparison_of_forall_isNilpotent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionSpaces.lean, line 265. The attribute's comment: “Equation 52.7.0.1 at a morphism of ringed spaces read on its small Zariski sites, for an arbitrary object, when the local sections of both sheaves of ideals are nilpotent — a restriction on the data, not on the object, from which the two derived completion functors are produced rather than assumed, so that no part of [Stacks, Tag 099F] is a hypothesis here. The display at the source's own data, two sheaves of ideals of finite type, is Stacks.RingedSpace .isIso_derivedCompletionPushforwardComparison_of_isFiniteType_of_isDerivedComplete of PushforwardCommutesCompletionFiniteType.lean, for an object derived complete along ℐ'”.

The display [Stacks, Tag 0A0I] at a morphism of ringed spaces, for an arbitrary object, when the local sections of ℐ and of ℐ' are nilpotent: the comparison (Rf_*ℱ)^∧ ⟶ Rf_*(ℱ^∧) is invertible for every ℱ ∈ D(𝒪_X).

The restriction is on the two sheaves of ideals, not on the object, and it discharges the conclusion of [Stacks, Tag 099F] on X and on Y rather than assuming it: this statement has no instance hypothesis. Nilpotence makes every object derived complete, by AlgebraicGeometry.RingedSite.isDerivedComplete_of_forall_isNilpotent, so this is AlgebraicGeometry.RingedSite.isIso_derivedCompletionPushforwardComparison_of_isDerivedComplete with its hypothesis discharged.

theorem isIso_derivedCompletionPushforwardComparison_of_forall_isNilpotent
    (hnil : ∀ (V : Opens X.carrier)
      (g : ((Stacks.SheafOfModules.Tensor.ringSheaf (toRingedSite X).O)).obj.obj (op V)),
      g ∈ I'.toSubmodule.obj (op V) → IsNilpotent g)
    (hnil' : ∀ (W : Opens Y.carrier)
      (s : ((Stacks.SheafOfModules.Tensor.ringSheaf (toRingedSite Y).O)).obj.obj (op W)),
      s ∈ I.toSubmodule.obj (op W) → IsNilpotent s)
    (K : DerivedCategory (_root_.SheafOfModules.{u}
      ((Stacks.SheafOfModules.Tensor.ringSheaf (toRingedSite X).O)))) :
    letI : (ObjectProperty.ι (RingedSite.IsDerivedComplete.{u, u, u, u}
        (toRingedSite X) I')).IsRightAdjoint :=
      RingedSite.isRightAdjoint_ι_isDerivedComplete_of_forall_isNilpotent
        (toRingedSite X) I' hnil
    letI : (ObjectProperty.ι (RingedSite.IsDerivedComplete.{u, u, u, u}
        (toRingedSite Y) I)).IsRightAdjoint :=
      RingedSite.isRightAdjoint_ι_isDerivedComplete_of_forall_isNilpotent
        (toRingedSite Y) I hnil'
    IsIso ((RingedSite.derivedCompletionPushforwardComparison
      (toRingedSiteHom f) I I' hI).app K)

AlgebraicGeometry.Scheme.isIso_derivedCompletionPushforwardComparison_of_forall_isNilpotent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionSpaces.lean, line 411. The attribute's comment: “Equation 52.7.0.1 in the display's own setting, a morphism of schemes, for an arbitrary object — in particular for an arbitrary quasi-coherent sheaf — when the local sections of both sheaves of ideals are nilpotent. A restriction on the data, not on the object, and the two derived completion functors are produced from it rather than assumed, so that no part of [Stacks, Tag 099F] is a hypothesis here. The display at the source's own data, two sheaves of ideals of finite type, is AlgebraicGeometry.Scheme .isIso_derivedCompletionPushforwardComparison_of_isFiniteType_of_isDerivedComplete of PushforwardCommutesCompletionFiniteType.lean, for an object derived complete along ℐ'”.

Equation 52.7.0.1 of [Stacks, Tag 0A0I] in the display's own setting, for an arbitrary object, when the local sections of ℐ and of ℐ' are nilpotent: the comparison (Rf_*ℱ)^∧ ⟶ Rf_*(ℱ^∧) is invertible for every ℱ ∈ D(𝒪_X), in particular for every quasi-coherent ℱ, with no hypothesis on ℱ.

The restriction is on the two sheaves of ideals, not on ℱ, and it discharges the conclusion of [Stacks, Tag 099F] on X and on S rather than assuming it: this statement has no instance hypothesis. It is not the general case of the display — nilpotence is not the source's hypothesis, and in that regime both derived completion functors are the identity. The display at the source's own data, two sheaves of ideals of finite type, is AlgebraicGeometry.Scheme .isIso_derivedCompletionPushforwardComparison_of_isFiniteType_of_isDerivedComplete of PushforwardCommutesCompletionFiniteType.lean, for an object derived complete along ℐ'. An arbitrary object, at a quasi-coherent sheaf of ideals ℐ of finite type and ℐ' = f^{-1}ℐ · 𝒪_X, is Scheme.isIso_derivedCompletionPushforwardComparison_idealSheafData_inverseImageIdealSheaf of the same file.

Because ℱ ranges over all of D(𝒪_X), this is also the analogue of the display for complexes of quasi-coherent modules that the fifth and last sentence of [Stacks, Tag 0AKL] attributes to [HL-P, Theorem 6.5], in the nilpotent regime. The derived-complete case of that remark is, at two sheaves of ideals of finite type, AlgebraicGeometry.Scheme .isIso_derivedCompletionPushforwardComparison_of_isFiniteType_of_isDerivedComplete of PushforwardCommutesCompletionFiniteType.lean, and at ideal sheaves generated by finitely many global sections, AlgebraicGeometry.Scheme .isIso_derivedCompletionPushforwardComparison_generatedIdealSheaf_of_isDerivedComplete of PushforwardCommutesCompletionGenerated.lean.

theorem isIso_derivedCompletionPushforwardComparison_of_forall_isNilpotent
    (hnil : ∀ (V : TopologicalSpace.Opens X.toRingedSpace.carrier)
      (g : ((Stacks.SheafOfModules.Tensor.ringSheaf
        (Stacks.RingedSpace.toRingedSite X.toRingedSpace).O)).obj.obj (op V)),
      g ∈ I'.toSubmodule.obj (op V) → IsNilpotent g)
    (hnil' : ∀ (W : TopologicalSpace.Opens S.toRingedSpace.carrier)
      (s : ((Stacks.SheafOfModules.Tensor.ringSheaf
        (Stacks.RingedSpace.toRingedSite S.toRingedSpace).O)).obj.obj (op W)),
      s ∈ I.toSubmodule.obj (op W) → IsNilpotent s)
    (K : DerivedCategory (_root_.SheafOfModules.{u}
      ((Stacks.SheafOfModules.Tensor.ringSheaf
        (Stacks.RingedSpace.toRingedSite X.toRingedSpace).O)))) :
    letI : (ObjectProperty.ι (RingedSite.IsDerivedComplete.{u, u, u, u}
        (Stacks.RingedSpace.toRingedSite X.toRingedSpace) I')).IsRightAdjoint :=
      RingedSite.isRightAdjoint_ι_isDerivedComplete_of_forall_isNilpotent
        (Stacks.RingedSpace.toRingedSite X.toRingedSpace) I' hnil
    letI : (ObjectProperty.ι (RingedSite.IsDerivedComplete.{u, u, u, u}
        (Stacks.RingedSpace.toRingedSite S.toRingedSpace) I)).IsRightAdjoint :=
      RingedSite.isRightAdjoint_ι_isDerivedComplete_of_forall_isNilpotent
        (Stacks.RingedSpace.toRingedSite S.toRingedSpace) I hnil'
    IsIso ((RingedSite.derivedCompletionPushforwardComparison
      (toRingedSiteHom f) I I' hI).app K)

AlgebraicGeometry.RingedToposHom.isIso_derivedCompletionPushforwardComparison_inverseImageIdealSheaf_of_isFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionToposGlobal.lean, line 236. The attribute's comment: “Equation 52.7.0.1 for a morphism of ringed topoi, as an invertibility of the canonical comparison map (Rf_*ℱ)^∧ ⟶ Rf_*(ℱ^∧), for an arbitrary object of D(𝒪'), at a sheaf of ideals of finite type and the ideal sheaf f^{-1}ℐ · 𝒪_X that Section 52.7 builds out of it. The two sides of the equation are therefore identified by the map [Stacks, Tag 0A0G] names, and are isomorphic through it rather than merely abstractly”.

[Stacks, Tag 0A0G]. Let f : (Sh(𝒟), 𝒪') ⟶ (Sh(𝒞), 𝒪) be a morphism of ringed topoi, let ℐ ⊂ 𝒪 be a sheaf of ideals of finite type and let ℐ' = f^{-1}ℐ · 𝒪_X be the sheaf of ideals generated by f^♯(f^{-1}ℐ) that Section 52.7 builds out of ℐ. Then the canonical comparison map

(Rf_*K)^∧ ⟶ Rf_*(K^∧)

is invertible for every object K of D(𝒪'), the completion on the target being taken along ℐ and the one on the source along ℐ'.

Both of the properties ℐ' has to have are theorems about the construction rather than hypotheses: the relation of [Stacks, Tag 099J] between ℐ and ℐ', which the comparison map needs in order to exist, is AlgebraicGeometry.RingedToposHom.idealCompatible_inverseImageIdealSheaf, and finite type of ℐ' — which is what makes the derived completion functor along it exist at all, by [Stacks, Tag 099F] — is AlgebraicGeometry.RingedToposHom.isFiniteType_inverseImageIdealSheaf.

The proof is the source's reduction to a morphism of ringed sites by [Stacks, Tag 03CR]; see the module documentation.

theorem isIso_derivedCompletionPushforwardComparison_inverseImageIdealSheaf_of_isFiniteType
    (K : DerivedCategory
      (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf X.toRingedSite.O)))) :
    IsIso ((derivedCompletionPushforwardComparison f I (inverseImageIdealSheaf.{u} f I)
      (idealCompatible_inverseImageIdealSheaf.{u} f I)).app K)

Tag 0A0L, a lemma

Tag 0A0L in the Stacks Project.

Stacks.Algebraization.adicCompletion_homology_derivedSections_iso_derivedCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/Completion/FormalFunctionsPseudoCoherent.lean, line 151. The attribute's comment: “the second equality lim H^p(U, K)/IⁿH^p(U, K) = H^p(U, K)^∧, the right hand completion being the derived completion of the module H^p(U, K) along I = 𝓘(U); the first equality is homology_derivedSections_derivedCompletion_iso_adicCompletion”.

Stacks Project, Tag 0A0L, the second equality. Let X be a locally Noetherian scheme, 𝓘 ⊂ 𝒪_X a quasi-coherent sheaf of ideals and K a pseudo-coherent object of D(𝒪_X). For an affine open U, with A = Γ(X, U) and I = 𝓘(U), and any left adjoint C to the inclusion of the derived-complete objects of D(A), the I-adic completion lim H^p(U, K)/IⁿH^p(U, K) of H^p(U, K) is the derived I-adic completion of the A-module H^p(U, K), read in degree zero.

This is [Stacks, Tag 0A06] for the complex H^p(U, K)[0], which is legitimate because H^p(U, K) is a finite module.

public theorem adicCompletion_homology_derivedSections_iso_derivedCompletion
    (X : Scheme.{u}) [IsLocallyNoetherian X] (𝓘 : X.IdealSheafData)
    (K : DerivedCategory X.Modules)
    (hK : RingedSpace.IsPseudoCoherent (X := X.toRingedSpace) K)
    (U : X.affineOpens)
    (C : DerivedCategory (ModuleCat.{u} Γ(X, U.1)) ⥤
      (show ObjectProperty (DerivedCategory (ModuleCat.{u} Γ(X, U.1))) from
        fun L ↦ IsDerivedComplete (𝓘.ideal U) L).FullSubcategory)
    (adj : C ⊣ (show ObjectProperty (DerivedCategory (ModuleCat.{u} Γ(X, U.1))) from
      fun L ↦ IsDerivedComplete (𝓘.ideal U) L).ι)
    (p : ℤ) :
    Nonempty
      (ModuleCat.of Γ(X, U.1) (AdicCompletion (𝓘.ideal U)
          ((DerivedCategory.homologyFunctor (ModuleCat.{u} Γ(X, U.1)) p).obj
            ((derivedSections (structureSheafRing X.toRingedSpace) U.1).obj K))) ≅
        (DerivedCategory.homologyFunctor (ModuleCat.{u} Γ(X, U.1)) 0).obj
          ((C ⋙ (show ObjectProperty (DerivedCategory (ModuleCat.{u} Γ(X, U.1))) from
              fun L ↦ IsDerivedComplete (𝓘.ideal U) L).ι).obj
            ((DerivedCategory.singleFunctor (ModuleCat.{u} Γ(X, U.1)) 0).obj
              ((DerivedCategory.homologyFunctor (ModuleCat.{u} Γ(X, U.1)) p).obj
                ((derivedSections (structureSheafRing X.toRingedSpace) U.1).obj K)))))

Stacks.Algebraization.homology_derivedCompletion_derivedSections_iso_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/Completion/FormalFunctionsPseudoCoherentModuleSide.lean, line 157. The attribute's comment: “the first equality H^p(RΓ(U, K)^∧) = lim H^p(U, K)/IⁿH^p(U, K) on the module side: its left hand side read at the derived completion in D(A) of the derived sections RΓ(U, K), for A = Γ(X, U) and I = 𝓘(U), which is [Stacks, Tag 0A06] applied to RΓ(U, K) together with the finiteness of the H^n(U, K); the second equality is exists_adjunction_and_adicCompletion_homology_derivedSections_iso_derivedCompletion”.

Stacks Project, Tag 0A0L, the first equality, read on the module side. Let X be a locally Noetherian scheme, 𝓘 ⊂ 𝒪_X a quasi-coherent sheaf of ideals and K a pseudo-coherent object of D(𝒪_X). For an affine open U, with A = Γ(X, U) and I = 𝓘(U), the degree-p cohomology of the derived completion in D(A) of RΓ(U, K) is the I-adic completion lim H^p(U, K)/IⁿH^p(U, K) of H^p(U, K).

Everything the source's first equality needs beyond the identification RΓ(U, K^∧) = RΓ(U, K)^∧: A is Noetherian and H^n(U, K) is a finite A-module in every degree (Stacks.Algebraization.finite_homology_derivedSections_of_isPseudoCoherent, which is where pseudo-coherence and the locally Noetherian hypothesis of the tag are used), so [Stacks, Tag 0A06] applies to RΓ(U, K) along I = 𝓘(U).

The derived completion of A-modules is produced, not assumed: the first conjunct exhibits a left adjoint C to the inclusion of the derived-complete objects of D(A), by Stacks.Algebraization.exists_derivedCompletionAdjunction, and the second conjunct holds for every such C, so no choice of reflector enters.

The left hand side is the cohomology of C(RΓ(U, K)), not of RΓ(U, K^∧); passing between the two is [Stacks, Tag 0CQI], which exists_adjunction_and_homology_derivedSections_derivedCompletion_iso_adicCompletion below takes as an input and Stacks.Algebraization.exists_iso_homology_derivedSections_derivedCompletion_whole of Completion/FormalFunctionsPseudoCoherentWhole.lean discharges.

public theorem homology_derivedCompletion_derivedSections_iso_adicCompletion
    (X : Scheme.{u}) [IsLocallyNoetherian X] (𝓘 : X.IdealSheafData)
    (K : DerivedCategory X.Modules)
    (hK : RingedSpace.IsPseudoCoherent (X := X.toRingedSpace) K)
    (U : X.affineOpens) (p : ℤ) :
    let P : ObjectProperty (DerivedCategory (ModuleCat.{u} Γ(X, U.1))) :=
      fun L ↦ IsDerivedComplete (𝓘.ideal U) L
    (∃ C : DerivedCategory (ModuleCat.{u} Γ(X, U.1)) ⥤ P.FullSubcategory,
        Nonempty (C ⊣ P.ι)) ∧
      ∀ C : DerivedCategory (ModuleCat.{u} Γ(X, U.1)) ⥤ P.FullSubcategory, (C ⊣ P.ι) →
        Nonempty
          ((DerivedCategory.homologyFunctor (ModuleCat.{u} Γ(X, U.1)) p).obj
              ((C ⋙ P.ι).obj
                ((derivedSections (structureSheafRing X.toRingedSpace) U.1).obj K)) ≅
            ModuleCat.of Γ(X, U.1) (AdicCompletion (𝓘.ideal U)
              ((DerivedCategory.homologyFunctor (ModuleCat.{u} Γ(X, U.1)) p).obj
                ((derivedSections (structureSheafRing X.toRingedSpace) U.1).obj K))))

Stacks.Algebraization.exists_iso_homology_derivedSections_derivedCompletion_whole, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/Completion/FormalFunctionsPseudoCoherentWhole.lean, line 223. The attribute's comment: “the whole lemma, at the source's own hypotheses — X a locally Noetherian scheme, 𝓘 ⊂ 𝒪_X a quasi-coherent sheaf of ideals and K a pseudo-coherent object of D(𝒪_X): for every affine open U, with A = Γ(X, U) and I = 𝓘(U), and every p, both equalities H^p(U, K^∧) = lim H^p(U, K)/IⁿH^p(U, K) = H^p(U, K)^∧, the right hand completion being the derived completion of the A-module H^p(U,K) along I read in degree zero. The left hand side is read at the derived completion K^∧ on D(𝒪_X) along 𝓘 itself, which exists because a quasi-coherent sheaf of ideals of a locally Noetherian scheme is of finite type, so [Stacks, Tag 099F] applies; the passage RΓ(U, K^∧) = RΓ(U, K)^∧ is [Stacks, Tag 0CQI] at an affine open, where the chosen generating family spans 𝓘(U) itself. The reflector onto the derived-complete objects of D(A) is produced out of [Stacks, Tag 0920] and the conclusion quantifies over it”.

Stacks Project, Tag 0A0L. Let X be a locally Noetherian scheme, ℐ ⊂ 𝒪_X a quasi-coherent sheaf of ideals and K a pseudo-coherent object of D(𝒪_X) with derived completion K^∧. Then for every affine open U ⊂ X, with A = Γ(X, U) and I = ℐ(U), and every p,

H^p(U, K^∧) = lim H^p(U, K)/IⁿH^p(U, K) = H^p(U, K)^∧,

the completion on the right being the derived completion of the A-module H^p(U, K) along I, read in degree zero.

Both equalities, at the source's own hypotheses. The first is exists_adjunction_and_homology_derivedSections_derivedCompletion_iso_adicCompletion with its input — the identification RΓ(U, K^∧) = RΓ(U, K)^∧ of [Stacks, Tag 0CQI] — discharged by Stacks.Algebraization.nonempty_iso_derivedSections_derivedCompletion_affine; the second is Stacks.Algebraization.adicCompletion_homology_derivedSections_iso_derivedCompletion, which is [Stacks, Tag 0A06] for the finite module H^p(U, K) placed in degree zero. Pseudo-coherence and the locally Noetherian hypothesis enter through the finiteness of H^n(U, K), which is Stacks.Algebraization.finite_homology_derivedSections_of_isPseudoCoherent.

Derived completion of A-modules is produced, not assumed: the first conjunct exhibits a left adjoint C to the inclusion of the derived-complete objects of D(A), by Stacks.Algebraization.exists_derivedCompletionAdjunction, and the second holds for every such C, so no choice of reflector enters. The derived completion K^∧ on D(𝒪_X) is produced too: ℐ is of finite type on a locally Noetherian scheme (Stacks.Algebraization.isFiniteType_idealSheafSiteSubmodule), so the reflector of [Stacks, Tag 099F] exists along the tag's own ideal sheaf.

theorem exists_iso_homology_derivedSections_derivedCompletion_whole
    (hK : RingedSpace.IsPseudoCoherent (X := X.toRingedSpace) K) (p : ℤ) :
    let P : ObjectProperty (DerivedCategory (ModuleCat.{u} Γ(X, U.1))) :=
      fun L ↦ IsDerivedComplete (𝓘.ideal U) L
    let Hp := fun (L : DerivedCategory X.Modules) ↦
      (DerivedCategory.homologyFunctor (ModuleCat.{u} Γ(X, U.1)) p).obj
        ((derivedSections (structureSheafRing X.toRingedSpace) U.1).obj L)
    (∃ C : DerivedCategory (ModuleCat.{u} Γ(X, U.1)) ⥤ P.FullSubcategory,
        Nonempty (C ⊣ P.ι)) ∧
      ∀ (C : DerivedCategory (ModuleCat.{u} Γ(X, U.1)) ⥤ P.FullSubcategory) (_ : C ⊣ P.ι),
        Nonempty
          (Hp ((AlgebraicGeometry.RingedSite.derivedCompletion (opensRingedSite X.sheaf)
              (idealSheafSiteSubmodule 𝓘)).obj K) ≅
            ModuleCat.of Γ(X, U.1) (AdicCompletion (𝓘.ideal U) (Hp K))) ∧
        Nonempty
          (ModuleCat.of Γ(X, U.1) (AdicCompletion (𝓘.ideal U) (Hp K)) ≅
            (DerivedCategory.homologyFunctor (ModuleCat.{u} Γ(X, U.1)) 0).obj
              ((C ⋙ P.ι).obj
                ((DerivedCategory.singleFunctor (ModuleCat.{u} Γ(X, U.1)) 0).obj (Hp K))))

Tag 0A0K, a lemma

Tag 0A0K in the Stacks Project.

Stacks.Algebraization.isDerivedLimit_single_limit_powerQuotients, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/Completion/AdicQuotientDerivedLimit.lean, line 390. The attribute's comment: “part (4), lim ℱ/𝓘ⁿℱ = R lim ℱ/𝓘ⁿℱ: for a coherent module ℱ on a locally Noetherian scheme and an arbitrary quasi-coherent sheaf of ideals 𝓘, the ordinary inverse limit of the adic quotient tower, placed in degree zero, is a derived inverse limit of that tower, with nothing assumed. The terms of the tower are quasi-coherent, hence acyclic on the affine opens, and its transitions are surjective on affine sections, hence Mittag-Leffler, and those are the two hypotheses [Stacks, Tag 0BKS] consumes. Existence of the product the derived limit is written with is part of the conclusion rather than a hypothesis”.

Stacks Project, Tag 0A0K, part (4). The ordinary inverse limit of the coherent adic quotient tower, placed in degree zero, is its derived inverse limit.

public theorem isDerivedLimit_single_limit_powerQuotients
    {X : Scheme.{u}} [IsLocallyNoetherian X]
    (I : X.IdealSheafData) (F : X.Modules) [F.IsCoherent] :
    let S := (powerQuotientSystem I F
      (isQuasicoherent_of_isCoherent F)).system
    ∃ h : HasProduct (fun n : ℕ =>
        (S ⋙ DerivedCategory.singleFunctor X.Modules 0).obj ⟨n⟩),
      @IsDerivedLimit (DerivedCategory X.Modules) _ _ _ _ _ _
        (S ⋙ DerivedCategory.singleFunctor X.Modules 0) h
        ((DerivedCategory.singleFunctor X.Modules 0).obj (limit S))

Stacks.Algebraization.isZero_cohomology_limit_powerQuotients_of_isAffineOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/Completion/AdicQuotientDerivedLimit.lean, line 431. The attribute's comment: “part (5), H^p(U, ℱ^∧) = 0 for p ≠ 0 and U ⊂ X affine open, read on the ordinary limit lim ℱ/ℐⁿℱ — the object [Stacks, Tag 0A0K] part (3) names ℱ^∧ — for a coherent module ℱ on a locally Noetherian scheme and an arbitrary quasi-coherent sheaf of ideals ℐ, with nothing assumed: the terms of the adic quotient tower are quasi-coherent, hence acyclic on the affine opens, and its transitions are surjective on affine sections, hence Mittag-Leffler, and those are the two hypotheses [Stacks, Tag 0BKS] consumes”.

Stacks Project, Tag 0A0K, part (5). On a locally Noetherian scheme the ordinary inverse limit lim ℱ/ℐⁿℱ of the adic quotient tower of a coherent module has no cohomology in positive degree over an affine open.

The terms of the tower are quasi-coherent, so Serre vanishing gives their acyclicity on the affine opens, and the transition maps are epimorphisms of quasi-coherent modules, hence surjective on affine sections, so Mittag-Leffler gives the vanishing of R¹ lim of the sections there. Those are exactly the two hypotheses of Stacks.Cohomology.SpaceInverseLimits.isZero_cohomology_limit_of_isBasis on the basis of affine opens.

The object is the ordinary limit lim ℱ/ℐⁿℱ, which is what the source's own argument for this part is about: parts (4) and (5) are both read off [Stacks, Tag 0A0J] for the quotient tower, and it is the tag's part (3) that then names that limit ℱ^∧. In this library part (3) at the tag's own hypotheses is Stacks.Algebraization.isIso_comparisonDerivedCompletionLimitAdicQuotient of Completion/AdicQuotientSliceTowerKoszul.lean, and part (5) stated on the derived completion ℱ^∧ itself, in every degree p ≠ 0 of either sign, is Stacks.Algebraization.isZero_homology_derivedSections_derivedCompletion_of_isAffineOpen of Completion/CoherentCompletionAffineVanishing.lean, which is derived from this statement through that isomorphism.

public theorem isZero_cohomology_limit_powerQuotients_of_isAffineOpen
    {X : Scheme.{u}} [IsLocallyNoetherian X]
    (I : X.IdealSheafData) (F : X.Modules) [F.IsCoherent]
    (U : X.affineOpens) (p : ℕ) (hp : 0 < p) :
    IsZero (Hgroup X.ringCatSheaf U.1 p
      (show X.Modules from limit (adicQuotientSystem I F)))

Stacks.Algebraization.nonempty_iso_homology_derivedCompletion_limit_adicQuotientSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/Completion/AdicQuotientLimitSheafIso.lean, line 512. The attribute's comment: “part (2), H^q(K^∧) = lim H^q(K)/𝓘ⁿ H^q(K): for a pseudo-coherent object K of D(𝒪_X) on a locally Noetherian scheme X and an arbitrary quasi-coherent sheaf of ideals 𝓘, the degree-q cohomology sheaf of the derived completion K^∧ is isomorphic to the inverse limit of the adic quotient tower of the coherent module H^q(K), with nothing further assumed — no quasi-compactness of X, no generation of 𝓘 by global sections, no Mittag-Leffler hypothesis and no appeal to part (1) of the tag. The limit is the same object parts (3), (4) and (5) are registered over, Stacks.Algebraization.adicQuotientSystem, read at the coherent module the tag's own footnote names. The isomorphism is non-canonical in the statement only because the source's canonical maps go the other way; it is produced by gluing the canonical affine comparisons, which are unique”.

Part (2) of [Stacks, Tag 0A0K]. For a pseudo-coherent object K of D(𝒪_X) on a locally Noetherian scheme X and an arbitrary quasi-coherent sheaf of ideals 𝓘,

H^q(K^∧) ≅ lim_n H^q(K)/𝓘ⁿ H^q(K).

The isomorphism is Stacks.BasisRestriction.moduleSheafIsoOfBasisSectionsIso applied to the affine comparisons Stacks.Algebraization.adicQuotientLimitSectionsComparison, which are bijective and compatible with restriction, against the unit of sheafification on the degree-q hypercohomology presheaf of K^∧; the sheafification of that presheaf is the cohomology sheaf by [Stacks, Tag 0BKV].

theorem nonempty_iso_homology_derivedCompletion_limit_adicQuotientSystem :
    Nonempty ((DerivedCategory.homologyFunctor X.Modules q).obj
          ((AlgebraicGeometry.RingedSite.derivedCompletion (opensRingedSite X.sheaf)
            (idealSheafSiteSubmodule 𝓘)).obj K) ≅
        limit (C := X.Modules)
          (adicQuotientSystem 𝓘 (homologyCoherentModule K hK q).obj))

Stacks.Algebraization.isIso_comparisonDerivedCompletionLimitAdicQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/Completion/AdicQuotientSliceTowerKoszul.lean, line 497. The attribute's comment: “part (3), ℱ^∧ = lim ℱ/𝓘ⁿℱ with an ordinary limit, at the source's own hypotheses: for a coherent module ℱ on a locally Noetherian scheme X, which is not assumed quasi-compact, and an arbitrary quasi-coherent sheaf of ideals 𝓘 — with no global generating family — the canonical comparison c : ℱ^∧ ⟶ (lim ℱ/𝓘ⁿℱ)[0] from the derived completion of ℱ along 𝓘 to the ordinary inverse limit of the adic quotients ℱ/𝓘ⁿℱ, placed in degree zero, is an isomorphism. The comparison is the unique map compatible with the completion unit and the limit lift, so the statement identifies a named map rather than asserting an abstract isomorphism. The source's = is also read as such an abstract isomorphism by nonempty_iso_completion_limit_adicQuotientSystem, which buys quasi-compactness of the scheme and a global generating family for the ideal sheaf”.

Part (3) of [Stacks, Tag 0A0K]: ℱ^∧ = lim ℱ/𝓘ⁿℱ with an ordinary inverse limit. Let X be a locally Noetherian scheme — not assumed quasi-compact — let 𝓘 ⊂ 𝒪_X be an arbitrary quasi-coherent sheaf of ideals and let ℱ be a coherent 𝒪_X-module. Then the canonical comparison

c : ℱ^∧ ⟶ (lim ℱ/𝓘ⁿℱ)[0]

from the derived completion of ℱ along 𝓘 to the ordinary inverse limit of the adic quotients, placed in degree zero, is an isomorphism.

The comparison is the unique map compatible with the completion unit of ℱ and the limit lift ℱ ⟶ lim ℱ/𝓘ⁿℱ (Stacks.Algebraization .existsUnique_comparison_derivedCompletion_limit_adicQuotientSystem), so the statement is about a named map and not merely the existence of an isomorphism — which is what makes it provable at these hypotheses at all, invertibility of a named map being local on the site (Stacks.SheafOfModules.isIso_of_coversTop_mapDerivedCategory).

Stacks.Algebraization.isIso_comparison_of_affineOpens_sliceTower reduces it to the per-affine- slice presentation Stacks.Algebraization .exists_isDerivedLimitWithProjections_completionToAdicQuotientSliceTower, which is the Koszul chain of DerivedCompletionRinged/ run on the slice over an affine open, where the restricted ideal sheaf is generated by finitely many sections and the Artin–Rees level is computed once over a single Noetherian model.

Stacks.Algebraization.nonempty_iso_completion_limit_adicQuotientSystem of Completion/KoszulAdicCompletionLimit.lean is the other registration of this part: it runs the same chain on X itself, which costs [CompactSpace X] and a global generating family for 𝓘 and delivers the non-canonical isomorphism of [Stacks, Tag 0H9L] in place of the invertibility of c.

theorem isIso_comparisonDerivedCompletionLimitAdicQuotient :
    IsIso (comparisonDerivedCompletionLimitAdicQuotient I ℱ)

Stacks.Algebraization.isDerivedLimit_adicReductionTower_derivedCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/Completion/AdicReductionTowerDerivedLimit.lean, line 95. The attribute's comment: “part (1), K^∧ = R lim (K ⊗^𝐋_𝒪 𝒪/𝓘ⁿ), at the source's own hypotheses: on a locally Noetherian scheme Y, for an arbitrary quasi-coherent sheaf of ideals 𝓘 and an arbitrary object K of D(𝒪_Y), the derived completion K^∧ along 𝓘 (the reflector of Tag 099F) is a derived limit of the tower n ↦ K ⊗^𝐋_{𝒪_Y} 𝒪_Y/𝓘ⁿ⁺¹. No quasi-compactness of Y and no generation of 𝓘 by global sections is assumed. R lim is a predicate rather than a functor, so the source's equality is read as K^∧ being a derived limit of that tower, the same reading as the tag's part (4); the tower over the positive powers 𝓘ⁿ⁺¹ is cofinal in the one over all powers”.

Part (1) of [Stacks, Tag 0A0K]. On a locally Noetherian scheme Y, for an arbitrary quasi-coherent sheaf of ideals 𝓘 and an arbitrary object K of D(𝒪_Y), the derived completion K^∧ along 𝓘 is a derived limit of the tower n ↦ K ⊗^𝐋_{𝒪_Y} 𝒪_Y/𝓘ⁿ⁺¹.

See the module documentation for the proof.

theorem isDerivedLimit_adicReductionTower_derivedCompletion
    (K : DerivedCategory (_root_.SheafOfModules.{u}
      ((Stacks.SheafOfModules.Tensor.ringSheaf
        (Stacks.SheafOfModules.opensRingedSite Y.sheaf).O)))) :
    IsDerivedLimit
      (adicReductionTower (Stacks.SheafOfModules.opensRingedSite Y.sheaf)
        (idealSheafSiteSubmodule 𝓘) K)
      ((derivedCompletion (Stacks.SheafOfModules.opensRingedSite Y.sheaf)
        (idealSheafSiteSubmodule 𝓘)).obj K)

Stacks.Algebraization.isZero_homology_derivedSections_derivedCompletion_of_isAffineOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/Completion/CoherentCompletionAffineVanishing.lean, line 84. The attribute's comment: “part (5), H^p(U, ℱ^∧) = 0 for p ≠ 0 and U ⊂ X affine open, on the derived completion itself: for a coherent module ℱ on a locally Noetherian scheme X, which is not required to be quasi-compact, and an arbitrary quasi-coherent sheaf of ideals 𝓘, the degree-p hypercohomology over an affine open U of the derived completion ℱ^∧ of ℱ along 𝓘, an object of D(𝒪_X), vanishes for every integer p ≠ 0, negative degrees included. The proof reads ℱ^∧ as lim ℱ/𝓘ⁿℱ in degree zero by part (3) and applies the vanishing on that limit”.

Part (5) of [Stacks, Tag 0A0K]: H^p(U, ℱ^∧) = 0 for p ≠ 0 and U ⊂ X affine open. Let X be a locally Noetherian scheme — not assumed quasi-compact — let 𝓘 ⊂ 𝒪_X be an arbitrary quasi-coherent sheaf of ideals and let ℱ be a coherent 𝒪_X-module. Then for every affine open U ⊂ X and every integer p ≠ 0 the degree-p hypercohomology over U of the derived completion ℱ^∧ of ℱ along 𝓘, an object of D(𝒪_X), vanishes.

Part (3) (Stacks.Algebraization.isIso_comparisonDerivedCompletionLimitAdicQuotient) identifies ℱ^∧ with (lim ℱ/𝓘ⁿℱ)[0]; below degree zero the vanishing is left t-exactness of RΓ(U, -), and above it is the vanishing of the higher cohomology of lim ℱ/𝓘ⁿℱ over an affine open, Stacks.Algebraization.isZero_cohomology_limit_powerQuotients_of_isAffineOpen.

theorem isZero_homology_derivedSections_derivedCompletion_of_isAffineOpen
    {X : Scheme.{u}} [IsLocallyNoetherian X] (I : X.IdealSheafData) (ℱ : X.Modules)
    [ℱ.IsCoherent] (U : X.affineOpens) (p : ℤ) (hp : p ≠ 0) :
    IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{u} Γ(X, U.1)) p).obj
      ((derivedSections (structureSheafRing X.toRingedSpace) U.1).obj
        ((AlgebraicGeometry.RingedSite.derivedCompletion (opensRingedSite X.sheaf)
            (idealSheafSiteSubmodule I)).obj
          ((DerivedCategory.singleFunctor X.Modules 0).obj ℱ))))

Stacks.Algebraization.nonempty_iso_completion_limit_adicQuotientSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/Completion/KoszulAdicCompletionLimit.lean, line 308. The attribute's comment: “part (3), ℱ^∧ = lim ℱ/𝓘ⁿℱ with an ordinary limit: for a coherent module ℱ on a quasi-compact locally Noetherian scheme Y and the quasi-coherent sheaf of ideals 𝓘 generated by global sections f_1, …, f_r of 𝒪_Y, the derived completion ℱ^∧ along 𝓘 is isomorphic in D(𝒪_Y) to the ordinary inverse limit of the adic quotients ℱ/𝓘ⁿℱ, placed in degree zero. The ideal sheaf is the extension to Y of the ideal those global sections span, so its generation by them is a definition and not a hypothesis, and every ideal sheaf so generated equals it. The isomorphism is non-canonical because a derived limit is, which is the form [Stacks, Tag 0H9L] takes”.

Stacks Project, Tag 0A0K, part (3). Let Y be a quasi-compact locally Noetherian scheme, let ℐ ⊂ 𝒪_Y be a quasi-coherent sheaf of ideals generated by the global sections f_1, …, f_r, and let ℱ be a coherent 𝒪_Y-module. Then the derived completion ℱ^∧ of ℱ along ℐ is isomorphic, in D(𝒪_Y), to the ordinary inverse limit lim ℱ/ℐⁿℱ of the adic quotients, placed in degree zero.

R lim is a predicate rather than a functor here, and a derived limit is unique only up to a non-canonical isomorphism, which is why the conclusion is Nonempty of an isomorphism — exactly as in [Stacks, Tag 0H9L], _root_.Rlim.Pro.nonempty_iso_of_isDerivedLimit_of_pro_isomorphism, which is the last step of the proof.

The ideal sheaf is not a parameter with a generation hypothesis: it is Stacks.Algebraization.koszulIdealSheafData, the extension to Y of the ideal of global functions spanned by f_1, …, f_r, whose affine components are computed by Stacks.Algebraization.koszulIdealSheafData_ideal. Nothing is lost by fixing it, because an IdealSheafData is determined by its affine components and so every ideal sheaf generated by those sections equals this one, which is Stacks.Algebraization.eq_koszulIdealSheafData.

[CompactSpace Y] is a genuine hypothesis and not an artefact: the Artin–Rees level behind the pro-vanishing of the Koszul cohomology sheaves below the top degree is produced one per member of an affine cover, and the proof takes the maximum over a finite cover. See the section "The hypotheses, and what they are for" of this file. The source asks neither for quasi-compactness nor for ℐ to be globally generated; the module documentation of Completion/AdicQuotientDerivedLimit.lean records what a proof at the source's own hypotheses would take, namely a canonical comparison, which is what this route does not produce.

theorem nonempty_iso_completion_limit_adicQuotientSystem :
    Nonempty
      ((RingedSite.completionFunctor (Stacks.SheafOfModules.opensRingedSite Y.sheaf) f).obj
          (DerivedCategory.Q.obj (RingedSite.singleSheafComplex
            (Stacks.SheafOfModules.opensRingedSite Y.sheaf) ℱ)) ≅
        (DerivedCategory.singleFunctor Y.Modules 0).obj
          (limit (adicQuotientSystem (koszulIdealSheafData Y f) ℱ)))

Stacks.Algebraization.isDerivedLimit_derivedTensor_adicQuotientSystem_completion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/Completion/KoszulAdicDerivedTensorLimit.lean, line 216. The attribute's comment: “part (1), K^∧ = R lim (K ⊗^𝐋_𝒪 𝒪/𝓘ⁿ): for an arbitrary object K of D(𝒪_Y) on a quasi-compact locally Noetherian scheme Y and the quasi-coherent sheaf of ideals 𝓘 generated by global sections f_1, …, f_r of 𝒪_Y, the derived completion K^∧ along 𝓘 is a derived limit of the tower n ↦ K ⊗^𝐋_{𝒪_Y} 𝒪_Y/𝓘ⁿ. R lim is a predicate rather than a functor, so the source's equality is read as K^∧ being a derived limit of that tower, which is the same reading the tag's part (4) is registered with. The ideal sheaf is the extension to Y of the ideal those global sections span, so its generation by them is a definition and not a hypothesis, and every ideal sheaf so generated equals it. The object K carries no hypothesis”.

Stacks Project, Tag 0A0K, part (1). Let Y be a quasi-compact locally Noetherian scheme, let ℐ ⊂ 𝒪_Y be the quasi-coherent sheaf of ideals generated by the global sections f_1, …, f_r, and let K be an arbitrary object of D(𝒪_Y). Then the derived completion K^∧ of K along ℐ is a derived limit of the tower n ↦ K ⊗^𝐋_{𝒪_Y} 𝒪_Y/ℐⁿ:

K^∧ = R lim (K ⊗^𝐋_{𝒪_Y} 𝒪_Y/ℐⁿ).

R lim is a predicate rather than a functor here, exactly as in the tag's part (4) Stacks.Algebraization.isDerivedLimit_single_limit_powerQuotients, so the source's equality is read as the object K^∧ being a derived limit of the tower; no comparison map has to be produced, and nothing is weakened by that reading.

The proof is [Stacks, Tag 0A0E] — K^∧ is a derived limit of n ↦ K ⊗^𝐋 (K^n)^∨ — together with the pro-isomorphism of the dual Koszul tower with n ↦ 𝒪/ℐⁿ, whiskered by K ⊗^𝐋 -. The coefficient object enters both towers as that same whiskering functor, so the two meet with no constraint of the derived tensor product used.

[CompactSpace Y] is a genuine hypothesis of this route and not an artefact: the Artin–Rees level behind the pro-vanishing of the Koszul cohomology sheaves below the top degree is produced one per member of an affine cover and the proof maximises over a finite cover. See the section "The hypotheses, and what they are for" of this file. The source asks neither for quasi-compactness nor for ℐ to be globally generated; Completion/AdicQuotientDerivedLimit.lean records what a proof at the source's own hypotheses would take.

theorem isDerivedLimit_derivedTensor_adicQuotientSystem_completion
    (K : DerivedCategory Y.Modules) :
    IsDerivedLimit
      ((adicQuotientSystem (koszulIdealSheafData Y f)
            (SheafOfModules.unit
              (Stacks.SheafOfModules.Tensor.ringSheaf
                (Stacks.SheafOfModules.opensRingedSite Y.sheaf).O)) ⋙
          DerivedCategory.singleFunctor Y.Modules 0) ⋙
        (Stacks.SheafOfModules.canonicalDerivedTensorProduct
          (Stacks.SheafOfModules.opensRingedSite Y.sheaf)).tensor.obj K)
      ((RingedSite.completionFunctor
        (Stacks.SheafOfModules.opensRingedSite Y.sheaf) f).obj K)

Tag 0A0M, a lemma

Tag 0A0M in the Stacks Project.

Stacks.Algebraization.exists_shortExact_adicCompletion_cohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/Completion/CohomologyAdicCompletion.lean, line 124. The attribute's comment: “the exact sequence, granted the identification of [Stacks, Tag 0BLX] of the derived global sections of the formal completion with the derived I-adic completion of the derived global sections, carried as the hypothesis hBLX”.

Stacks Project, Tag 0A0M, the short exact sequence, granted [Stacks, Tag 0BLX].

Let A be a Noetherian ring, I ⊆ A an ideal, f : X ⟶ Spec A a Noetherian scheme over A and ℱ a coherent 𝒪_X-module whose cohomology modules H^p(X, ℱ) are finite over A. Write 𝓘 = I · 𝒪_X. Then for every p the I-adic completion of H^p(X, ℱ) sits in a short exact sequence of A-modules 0 ⟶ R¹lim H^{p-1}(X, ℱ/𝓘ⁿℱ) ⟶ H^p(X, ℱ)^∧ ⟶ lim H^p(X, ℱ/𝓘ⁿℱ) ⟶ 0 whose left term is the cokernel of 1 - shift on the product of the degree-(p-1) cohomology tower and whose right term is the inverse limit of the degree-p cohomology tower.

Derived I-adic completion is represented by an arbitrary left adjoint C to the inclusion of the derived-complete objects of D(A). The hypothesis hBLX is [Stacks, Tag 0BLX] for f: the derived global sections of the formal completion lim ℱ/𝓘ⁿℱ are the derived I-adic completion of the derived global sections of ℱ.

public theorem exists_shortExact_adicCompletion_cohomology
    (A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A)
    {X : Scheme.{u}} [IsNoetherian X] (f : X ⟶ Spec (.of A))
    (F : X.Modules) [F.IsCoherent]
    (hfinite : ∀ p : ℤ, Module.Finite A
      ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) p).obj
        ((derivedGlobalSectionsOver f).obj
          ((DerivedCategory.singleFunctor X.Modules 0).obj F))))
    (C : DerivedCategory (ModuleCat.{u} A) ⥤
      (show ObjectProperty (DerivedCategory (ModuleCat.{u} A)) from
        fun L ↦ IsDerivedComplete I L).FullSubcategory)
    (adj : C ⊣ (show ObjectProperty (DerivedCategory (ModuleCat.{u} A)) from
      fun L ↦ IsDerivedComplete I L).ι)
    (hBLX : Nonempty
      ((C.obj ((derivedGlobalSectionsOver f).obj
          ((DerivedCategory.singleFunctor X.Modules 0).obj F))).obj ≅
        (derivedGlobalSectionsOver f).obj
          ((DerivedCategory.singleFunctor X.Modules 0).obj
            (limit (adicQuotientSystem
              (Stacks.Cohomology.FormalFunctions.baseIdealSheaf A I f) F)))))
    (p : ℤ) :
    let T : ℕᵒᵖ ⥤ DerivedCategory (ModuleCat.{u} A) :=
      adicQuotientSystem (Stacks.Cohomology.FormalFunctions.baseIdealSheaf A I f) F ⋙
        DerivedCategory.singleFunctor X.Modules 0 ⋙ derivedGlobalSectionsOver f
    let H : ℤ → DerivedCategory (ModuleCat.{u} A) ⥤ ModuleCat.{u} A := fun q ↦
      DerivedCategory.homologyFunctor (ModuleCat.{u} A) q
    ∃ (i : CompletionSequences.firstDerivedLimit A (T ⋙ H (p - 1)) ⟶
        ModuleCat.of A (AdicCompletion I
          ((H p).obj ((derivedGlobalSectionsOver f).obj
            ((DerivedCategory.singleFunctor X.Modules 0).obj F)))))
      (q : ModuleCat.of A (AdicCompletion I
          ((H p).obj ((derivedGlobalSectionsOver f).obj
            ((DerivedCategory.singleFunctor X.Modules 0).obj F)))) ⟶
        limit (T ⋙ H p))
      (w : i ≫ q = 0),
      (ShortComplex.mk i q w).ShortExact

Stacks.Algebraization.exists_shortExact_cohomology_limit_adicQuotients, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/Completion/FormalCompletionCohomologySequence.lean, line 145. The attribute's comment: “for every p, the short exact sequence of A-modules 0 → R¹lim H^{p-1}(X, ℱ/𝓘ⁿℱ) → H^p(X, lim ℱ/𝓘ⁿℱ) → lim H^p(X, ℱ/𝓘ⁿℱ) → 0, the second displayed sequence of the source's proof, whose outer two terms are those of the source's conclusion; together with the identification H^p(C(RΓ(X,ℱ))) = H^p(X,ℱ)^∧ of the cohomology of the derived I-adic completion of RΓ(X,ℱ) with the I-adic completion of H^p(X,ℱ), for every reflector C onto the derived-complete objects of D(A), which is the step at which finiteness of H^p(X,ℱ) over A enters. Proved under the source's own hypotheses; the reflector is produced in the proof and the conclusion quantifies over it. The source's whole statement — the same sequence with H^p(X,ℱ)^∧ in the middle, together with the vanishing of the R¹lim term for a proper f — is Stacks.Algebraization.exists_shortExact_adicCompletion_cohomology_whole of Completion/GeneralCohomologyAdicCompletion.lean, which transports this sequence along the isomorphism RΓ(X, lim ℱ/𝓘ⁿℱ) ≅ C(RΓ(X,ℱ)) of [Stacks, Tag 0BLX]”.

Stacks Project, Tag 0A0M, the exact sequence at the formal completion.

Let A be a Noetherian ring, I ⊆ A an ideal, f : X ⟶ Spec A a Noetherian scheme over A and ℱ a coherent 𝒪_X-module whose cohomology modules H^p(X, ℱ) are finite over A — the hypotheses of the source, and nothing else. Write 𝓘 = I · 𝒪_X. Then for every p:

• there is a short exact sequence of A-modules 0 ⟶ R¹lim H^{p-1}(X, ℱ/𝓘ⁿℱ) ⟶ H^p(X, lim ℱ/𝓘ⁿℱ) ⟶ lim H^p(X, ℱ/𝓘ⁿℱ) ⟶ 0, whose left term is the cokernel of 1 - shift on the product of the degree-(p-1) cohomology tower and whose right term is the inverse limit of the degree-p cohomology tower — the two outer terms of the source's conclusion, related exactly as the source relates them; and
• for every reflector C onto the derived-complete objects of D(A), the p-th cohomology of the derived I-adic completion C(RΓ(X, ℱ)) is the I-adic completion of H^p(X, ℱ). This is [Stacks, Tag 0A06] and is the step at which the source uses the finiteness of H^p(X, ℱ) over A.

Derived I-adic completion is not assumed: A is Noetherian, so a reflector exists by [Stacks, Tag 0920], and the second part is stated for every one of them.

The middle term of this sequence is H^p(X, lim ℱ/𝓘ⁿℱ) rather than H^p(X, ℱ)^∧; identifying the two is the composite of the second part above with the isomorphism RΓ(X, lim ℱ/𝓘ⁿℱ) ≅ C(RΓ(X, ℱ)) of [Stacks, Tag 0BLX], along which exists_shortExact_adicCompletion_cohomology below transports the sequence. That isomorphism is proved for an arbitrary ideal I in Completion/GeneralCohomologyAdicCompletion.lean, as Stacks.Algebraization.hBLX_baseIdealSheaf, and the source's whole statement — the sequence with H^p(X, ℱ)^∧ in the middle, and the vanishing of the R¹lim term for a proper f — is Stacks.Algebraization.exists_shortExact_adicCompletion_cohomology_whole there.

public theorem exists_shortExact_cohomology_limit_adicQuotients
    (A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A)
    {X : Scheme.{u}} [IsNoetherian X] (f : X ⟶ Spec (.of A))
    (F : X.Modules) [F.IsCoherent]
    (hfinite : ∀ p : ℤ, Module.Finite A
      ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) p).obj
        ((derivedGlobalSectionsOver f).obj
          ((DerivedCategory.singleFunctor X.Modules 0).obj F))))
    (p : ℤ) :
    let T : ℕᵒᵖ ⥤ DerivedCategory (ModuleCat.{u} A) :=
      adicQuotientSystem (Stacks.Cohomology.FormalFunctions.baseIdealSheaf A I f) F ⋙
        DerivedCategory.singleFunctor X.Modules 0 ⋙ derivedGlobalSectionsOver f
    let H : ℤ → DerivedCategory (ModuleCat.{u} A) ⥤ ModuleCat.{u} A := fun q ↦
      DerivedCategory.homologyFunctor (ModuleCat.{u} A) q
    (∃ (i : CompletionSequences.firstDerivedLimit A (T ⋙ H (p - 1)) ⟶
        (H p).obj ((derivedGlobalSectionsOver f).obj
          ((DerivedCategory.singleFunctor X.Modules 0).obj
            (limit (adicQuotientSystem
              (Stacks.Cohomology.FormalFunctions.baseIdealSheaf A I f) F)))))
      (q : (H p).obj ((derivedGlobalSectionsOver f).obj
          ((DerivedCategory.singleFunctor X.Modules 0).obj
            (limit (adicQuotientSystem
              (Stacks.Cohomology.FormalFunctions.baseIdealSheaf A I f) F)))) ⟶
        limit (T ⋙ H p))
      (w : i ≫ q = 0),
      (ShortComplex.mk i q w).ShortExact) ∧
    ∀ (C : DerivedCategory (ModuleCat.{u} A) ⥤
        (show ObjectProperty (DerivedCategory (ModuleCat.{u} A)) from
          fun L ↦ IsDerivedComplete I L).FullSubcategory)
        (_ : C ⊣ (show ObjectProperty (DerivedCategory (ModuleCat.{u} A)) from
          fun L ↦ IsDerivedComplete I L).ι),
      Nonempty
        ((H p).obj ((C.obj ((derivedGlobalSectionsOver f).obj
              ((DerivedCategory.singleFunctor X.Modules 0).obj F))).obj) ≅
          ModuleCat.of A (AdicCompletion I
            ((H p).obj ((derivedGlobalSectionsOver f).obj
              ((DerivedCategory.singleFunctor X.Modules 0).obj F)))))

Stacks.Algebraization.exists_shortExact_adicCompletion_cohomology_whole, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/Completion/GeneralCohomologyAdicCompletion.lean, line 298. The attribute's comment: “the whole lemma, at the source's own hypotheses — A Noetherian, I ⊆ A an ideal, f : X ⟶ Spec A a Noetherian scheme over A and ℱ a coherent 𝒪_X-module with every H^p(X, ℱ) finite over A: for every p the short exact sequence of A-modules 0 → R¹lim H^{p-1}(X, ℱ/𝓘ⁿℱ) → H^p(X,ℱ)^∧ → lim H^p(X, ℱ/𝓘ⁿℱ) → 0 whose middle term is the I-adic completion of the A-module H^p(X,ℱ), together with the vanishing of the R¹lim term for a proper f. The ideal is arbitrary: the identification of the middle term is the identity RΓ(X,ℱ)^∧ = RΓ(X, lim ℱ/𝓘ⁿℱ) of [Stacks, Tag 0BLX], got from the Koszul identity of that tag at the ideal sheaf generated by the images of a generating family of I — which a Noetherian A provides — and part (3) of [Stacks, Tag 0A0K]. The properness clause is the Mittag-Leffler condition of [Stacks, Tag 02OB], discharged from [Stacks, Tag 02O8]. The reflector onto the derived-complete objects of D(A) is produced in the proof out of [Stacks, Tag 0920]”.

Stacks Project, Tag 0A0M. Let A be a Noetherian ring, I ⊆ A an ideal, f : X ⟶ Spec A a Noetherian scheme over A and ℱ a coherent 𝒪_X-module whose cohomology modules H^p(X, ℱ) are finite over A — the hypotheses of the source, and nothing else. Write 𝓘 = I · 𝒪_X. Then for every p:

• the I-adic completion of the A-module H^p(X, ℱ) sits in a short exact sequence of A-modules

0 ⟶ R¹lim H^{p-1}(X, ℱ/𝓘ⁿℱ) ⟶ H^p(X, ℱ)^∧ ⟶ lim H^p(X, ℱ/𝓘ⁿℱ) ⟶ 0,

whose left term is the cokernel of 1 - shift on the product of the degree-(p-1) cohomology tower and whose right term is the inverse limit of the degree-p cohomology tower; and * if f is proper the R¹lim term is zero.

Both are the source's own assertions, at the source's own hypotheses, with nothing assumed. The sequence is Stacks.Algebraization.exists_shortExact_adicCompletion_cohomology, whose single input — the identification RΓ(X, ℱ)^∧ ≅ RΓ(X, lim ℱ/𝓘ⁿℱ) of [Stacks, Tag 0BLX] — is supplied by Stacks.Algebraization.hBLX_baseIdealSheaf: A being Noetherian, I = (a_1, …, a_r), and I · 𝒪_X is then the ideal sheaf generated by the global sections ρ a_i, where the Koszul identity of [Stacks, Tag 0BLX] and part (3) of [Stacks, Tag 0A0K] are both available. The properness clause is Stacks.Algebraization.isZero_firstDerivedLimit_cohomology_adicQuotients_of_isProper_int, which rests on the Mittag-Leffler condition of [Stacks, Tag 02OB] and through it on the proper mapping theorem [Stacks, Tag 02O5].

Derived I-adic completion is never introduced as data: a reflector onto the derived-complete objects of D(A) exists by [Stacks, Tag 0920] and is produced inside the proof.

theorem exists_shortExact_adicCompletion_cohomology_whole
    [IsNoetherianRing A] (I : Ideal A) [IsNoetherian X] (F : X.Modules) [F.IsCoherent]
    (hfinite : ∀ p : ℤ, Module.Finite A
      ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) p).obj
        ((derivedGlobalSectionsOver f).obj
          ((DerivedCategory.singleFunctor X.Modules 0).obj F))))
    (p : ℤ) :
    let T : ℕᵒᵖ ⥤ DerivedCategory (ModuleCat.{u} A) :=
      adicQuotientSystem (baseIdealSheaf A I f) F ⋙
        DerivedCategory.singleFunctor X.Modules 0 ⋙ derivedGlobalSectionsOver f
    let H : ℤ → DerivedCategory (ModuleCat.{u} A) ⥤ ModuleCat.{u} A := fun q ↦
      DerivedCategory.homologyFunctor (ModuleCat.{u} A) q
    (∃ (i : CompletionSequences.firstDerivedLimit A (T ⋙ H (p - 1)) ⟶
        ModuleCat.of A (AdicCompletion I
          ((H p).obj ((derivedGlobalSectionsOver f).obj
            ((DerivedCategory.singleFunctor X.Modules 0).obj F)))))
      (q : ModuleCat.of A (AdicCompletion I
          ((H p).obj ((derivedGlobalSectionsOver f).obj
            ((DerivedCategory.singleFunctor X.Modules 0).obj F)))) ⟶
        limit (T ⋙ H p))
      (w : i ≫ q = 0),
      (ShortComplex.mk i q w).ShortExact) ∧
    (AlgebraicGeometry.IsProper f →
      IsZero (CompletionSequences.firstDerivedLimit A (T ⋙ H (p - 1))))

Stacks.Algebraization.exists_shortExact_adicCompletion_cohomology_principal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/Completion/PrincipalCohomologyAdicCompletion.lean, line 159. The attribute's comment: “the source's full conclusion for a principal ideal I = (a): for every p the short exact sequence of A-modules 0 → R¹lim H^{p-1}(X, ℱ/𝓘ⁿℱ) → H^p(X,ℱ)^∧ → lim H^p(X, ℱ/𝓘ⁿℱ) → 0 whose middle term is the I-adic completion of the A-module H^p(X,ℱ), proved under the source's own hypotheses on A, X and ℱ, the reflector onto the derived-complete objects of D(A) being produced in the proof out of [Stacks, Tag 0920]. The middle term is identified by the comparison of the two adic towers of ℱ at a principal ideal — the tower n ↦ ℱ/((a)𝒪_X)ⁿℱ of quotients by the ideal-power subsheaves and the tower n ↦ ℱ/aⁿ⁺¹ℱ of cokernels of the iterates of multiplication by a, shown to have the same inverse limit in Stacks.Algebraization.PrincipalAdicTower.limitTowerIso — together with [Stacks, Tag 0BLD], whose stabilization of the a-power torsion of ℱ is supplied by Stacks.Algebraization.stabilizes_mulF_of_isCoherent for a coherent sheaf on a Noetherian scheme and whose countable-product side conditions are supplied by Stacks.Algebraization.hasProductsOfShape_nat_derivedCategory_modules. The same sequence at an arbitrary ideal, together with the properness clause, is Stacks.Algebraization.exists_shortExact_adicCompletion_cohomology_whole of Completion/GeneralCohomologyAdicCompletion.lean; what this registration adds is the principal case by the independent route through [Stacks, Tag 0BLD], which needs neither quasi-compactness nor the Koszul machinery of the ringed site”.

Stacks Project, Tag 0A0M for a principal ideal.

Let A be a Noetherian ring, a ∈ A, f : X ⟶ Spec A a Noetherian scheme over A and ℱ a coherent 𝒪_X-module whose cohomology modules H^p(X, ℱ) are finite over A — the hypotheses of the source, and nothing else. Write I = (a) and 𝓘 = I · 𝒪_X. Then for every p the I-adic completion of the A-module H^p(X, ℱ) sits in a short exact sequence of A-modules

0 ⟶ R¹lim H^{p-1}(X, ℱ/𝓘ⁿℱ) ⟶ H^p(X, ℱ)^∧ ⟶ lim H^p(X, ℱ/𝓘ⁿℱ) ⟶ 0,

whose left term is the cokernel of 1 - shift on the product of the degree-(p-1) cohomology tower and whose right term is the inverse limit of the degree-p cohomology tower. This is the source's conclusion.

Derived I-adic completion is not data here: A is Noetherian, so a reflector onto the derived-complete objects of D(A) exists by [Stacks, Tag 0920] and is produced inside the proof. The isomorphism RΓ(X, ℱ)^∧ ≅ RΓ(X, lim ℱ/𝓘ⁿℱ) of [Stacks, Tag 0BLX], which the source's proof derives, is proved for this I from [Stacks, Tag 0BLD] and the comparison of the two adic towers of ℱ at a principal ideal, Stacks.Algebraization.PrincipalAdicTower.limitTowerIso.

This is the source's sequence at a principal ideal, by a route that goes through [Stacks, Tag 0BLD]. At an arbitrary ideal the same sequence, together with the properness clause, is Stacks.Algebraization.exists_shortExact_adicCompletion_cohomology_whole of Completion/GeneralCohomologyAdicCompletion.lean, which discharges hBLX from the Koszul identity of [Stacks, Tag 0BLX] and part (3) of [Stacks, Tag 0A0K] instead.

public theorem exists_shortExact_adicCompletion_cohomology_principal
    (A : Type u) [CommRing A] [IsNoetherianRing A] (a : A)
    {X : Scheme.{u}} [IsNoetherian X] (f : X ⟶ Spec (.of A))
    (F : X.Modules) [F.IsCoherent]
    (hfinite : ∀ p : ℤ, Module.Finite A
      ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) p).obj
        ((derivedGlobalSectionsOver f).obj
          ((DerivedCategory.singleFunctor X.Modules 0).obj F))))
    (p : ℤ) :
    let T : ℕᵒᵖ ⥤ DerivedCategory (ModuleCat.{u} A) :=
      adicQuotientSystem
          (Stacks.Cohomology.FormalFunctions.baseIdealSheaf A (Ideal.span {a}) f) F ⋙
        DerivedCategory.singleFunctor X.Modules 0 ⋙ derivedGlobalSectionsOver f
    let H : ℤ → DerivedCategory (ModuleCat.{u} A) ⥤ ModuleCat.{u} A := fun q ↦
      DerivedCategory.homologyFunctor (ModuleCat.{u} A) q
    ∃ (i : CompletionSequences.firstDerivedLimit A (T ⋙ H (p - 1)) ⟶
        ModuleCat.of A (AdicCompletion (Ideal.span {a})
          ((H p).obj ((derivedGlobalSectionsOver f).obj
            ((DerivedCategory.singleFunctor X.Modules 0).obj F)))))
      (q : ModuleCat.of A (AdicCompletion (Ideal.span {a})
          ((H p).obj ((derivedGlobalSectionsOver f).obj
            ((DerivedCategory.singleFunctor X.Modules 0).obj F)))) ⟶
        limit (T ⋙ H p))
      (w : i ≫ q = 0),
      (ShortComplex.mk i q w).ShortExact

Tag 0AKL, a remark

Tag 0AKL in the Stacks Project.

AlgebraicGeometry.Stack.isIso_derivedCompletionPushforwardComparison_of_isAlgebraicStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionAlgebraicStacks.lean, line 193. The attribute's comment: “the mathematical content of Remark 52.7.4, which is its fifth and last sentence: the analogue of Equation 52.7.0.1 of [Stacks, Tag 0A0I] for complexes of quasi-coherent modules, [HL-P, Theorem 6.5], here for a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S. For the morphism of ringed topoi (Sh(𝒳_τ), 𝒪_𝒳) ⟶ (Sh(𝒴_τ), 𝒪_𝒴) that f induces, at any topology τ coarser than the fppf one, a sheaf of ideals ℐ ⊂ 𝒪_𝒴 of finite type and ℐ' = f^{-1}ℐ · 𝒪_𝒳, the canonical comparison map (Rf_*K)^∧ ⟶ Rf_*(K^∧) is invertible for every object K of D(𝒪_𝒳), so in particular for every complex of quasi-coherent modules, and every quasi-coherent sheaf of ideals of finite type is an admissible ℐ. The proof is [Stacks, Tag 0A0G] for an arbitrary morphism of ringed topoi, AlgebraicGeometry.RingedToposHom.isIso_derivedCompletionPushforwardComparison_inverseImageIdealSheaf_of_isFiniteType, at the morphism of ringed topoi of [Stacks, Tag 06TW], AlgebraicGeometry.Stack.fullRingedToposHom; it holds for every 1-morphism of categories fibred in groupoids over the big fppf site, AlgebraicGeometry.Stack.isIso_derivedCompletionPushforwardComparison_fullRingedToposHom. The stacks have objects and morphisms in Type (u + 1) and the structure sheaves sections in Type (u + 1), the seating at which the library's derived completion on a ringed topos is defined. The remark's first four sentences are bibliography — pointers to [lurie-thesis, Theorem 6.3.1] for a derived formal functions theorem for proper maps, to [dag12, Chapter 4] with the cross-reference to More on Algebra, Section 091N for the affine story, and to [G-R, Section 2.9] for proper base change and derived completion via (ind) coherent modules — and carry no formalizable statement. [HL-P, Theorem 6.5] is also stated for morphisms of derived algebraic stacks; derived algebraic stacks are not defined in this library, so that part of the reference's setting is outside it”.

The analogue of [Stacks, Tag 0A0I] for morphisms of algebraic stacks, [HL-P, Theorem 6.5], which is the content of the last sentence of [Stacks, Tag 0AKL]. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S, let τ be a topology coarser than the fppf one (any of the Zariski, étale, smooth, syntomic and fppf topologies), and consider the morphism of ringed topoi (Sh(𝒳_τ), 𝒪_𝒳) ⟶ (Sh(𝒴_τ), 𝒪_𝒴) that f induces (Stacks 06TW). Let ℐ ⊂ 𝒪_𝒴 be a sheaf of ideals of finite type and let ℐ' = f^{-1}ℐ · 𝒪_𝒳. Then the canonical comparison map

(Rf_*K)^∧ ⟶ Rf_*(K^∧)

is invertible for every object K of D(𝒪_𝒳), the completion on 𝒴 being taken along ℐ and the one on 𝒳 along ℐ'. In particular Rf_*(ℱ^∧) = (Rf_*ℱ)^∧ for every complex of quasi-coherent 𝒪_𝒳-modules ℱ, which is the form in which the remark states it, and every quasi-coherent sheaf of ideals of finite type is an admissible ℐ.

The ideal ℐ' is AlgebraicGeometry.RingedToposHom.inverseImageIdealSheaf, the sheaf of ideals generated by f^♯(f^{-1}ℐ); the relation between ℐ and ℐ' that the comparison map needs, and finite type of ℐ', are theorems about that construction. The two algebraic stacks are taken with objects and morphisms in Type (u + 1) and the structure sheaves with sections in Type (u + 1); see the module documentation for why.

It is AlgebraicGeometry.Stack.isIso_derivedCompletionPushforwardComparison_fullRingedToposHom, which needs only that 𝒳 and 𝒴 are fibred in groupoids — the first clause of AlgebraicGeometry.Stack.IsAlgebraicStack.

theorem isIso_derivedCompletionPushforwardComparison_of_isAlgebraicStack
    {𝒳 𝒴 : BasedCategory.{u + 1, u + 1} (BigFppfOver B S hS)}
    (h𝒳 : IsAlgebraicStack.{u, w} B S hS 𝒳) (h𝒴 : IsAlgebraicStack.{u, w} B S hS 𝒴)
    (f : 𝒳 ⥤ᵇ 𝒴)
    (I : SheafOfModules.Submodule (SheafOfModules.unit (Stacks.SheafOfModules.Tensor.ringSheaf
      (fullRingedTopos.{u, u + 1, u + 1} B S hS 𝒴.p τ
        (liftedStructureSheaf.{u, u + 1, u + 1} B S hS 𝒴.p τ h𝒴.fst hτ)).toRingedSite.O)))
    [I.toSheafOfModules.IsFiniteType]
    (K : letI := HasDerivedCategory.standard; DerivedCategory (SheafOfModules.{u + 1}
      (Stacks.SheafOfModules.Tensor.ringSheaf
        (fullRingedTopos.{u, u + 1, u + 1} B S hS 𝒳.p τ
          (liftedStructureSheaf.{u, u + 1, u + 1} B S hS 𝒳.p τ h𝒳.fst hτ)).toRingedSite.O))) :
    IsIso ((RingedToposHom.derivedCompletionPushforwardComparison
      (fullRingedToposHom B S hS 𝒳.p 𝒴.p f.toFunctor h𝒳.fst h𝒴.fst τ hτ
        (.of_isFiberedInGroupoids h𝒴.fst f.w)) I
      (RingedToposHom.inverseImageIdealSheaf.{u + 1}
        (fullRingedToposHom B S hS 𝒳.p 𝒴.p f.toFunctor h𝒳.fst h𝒴.fst τ hτ
          (.of_isFiberedInGroupoids h𝒴.fst f.w)) I)
      (RingedToposHom.idealCompatible_inverseImageIdealSheaf.{u + 1}
        (fullRingedToposHom B S hS 𝒳.p 𝒴.p f.toFunctor h𝒳.fst h𝒴.fst τ hτ
          (.of_isFiberedInGroupoids h𝒴.fst f.w)) I)).app K)

AlgebraicGeometry.Scheme.isIso_derivedCompletionPushforwardComparison_of_isFiniteType_of_isDerivedComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionFiniteType.lean, line 387. The attribute's comment: “the mathematical content of Remark 52.7.4, which is its fifth and last sentence: the analogue of Equation 52.7.0.1 for complexes of quasi-coherent modules, [HL-P, Theorem 6.5]. What is proved here is that analogue at a morphism of schemes, at the source's own data — two sheaves of ideals of finite type, ℐ ⊆ 𝒪_S and ℐ' ⊆ 𝒪_X with f^♯(f^{-1}ℐ) ⊆ ℐ' — for every object of D(𝒪_X) derived complete along ℐ', hence for every complex of quasi-coherent modules derived complete along ℐ', with both derived completion functors produced from the finite-type hypotheses by [Stacks, Tag 099F]. The remark's first four sentences are bibliography — pointers to [lurie-thesis, Theorem 6.3.1] for a derived formal functions theorem for proper maps, to [dag12, Chapter 4] with the cross-reference to More on Algebra, Section 091N for the affine story, and to [G-R, Section 2.9] for proper base change and derived completion via (ind) coherent modules — and carry no formalizable statement. At a morphism of algebraic stacks the analogue is AlgebraicGeometry.Stack.isIso_derivedCompletionPushforwardComparison_of_isAlgebraicStack; derived algebraic stacks, the other half of the setting of [HL-P, Theorem 6.5], are not defined in this library”.

Equation 52.7.0.1 of [Stacks, Tag 0A0I] in the display's own setting and at the source's own data, for a derived-complete object. Let f : X ⟶ S be a morphism of schemes, let ℐ ⊆ 𝒪_S be a sheaf of ideals of finite type and let ℐ' ⊆ 𝒪_X be a sheaf of ideals of finite type with f^♯(f^{-1}ℐ) ⊆ ℐ' — which the display's f^{-1}ℐ · 𝒪_X is. Then (Rf_*ℱ)^∧ ⟶ Rf_*(ℱ^∧) is invertible for every ℱ ∈ D(𝒪_X) derived complete along ℐ'.

This is the display at the hypotheses Section 52.7 writes it under. The source asks ℐ to be a quasi-coherent sheaf of ideals of finite type and ℱ to be quasi-coherent, and uses those hypotheses only through [Stacks, Tag 099F], to know the two derived completion functors exist; here finite type alone produces them, by Stacks.RingedSpace.isRightAdjoint_ι_isDerivedComplete_of_isFiniteType, so quasi-coherence is not needed and the statement applies in particular to every quasi-coherent ℐ of finite type and every complex of quasi-coherent modules derived complete along ℐ'.

Because ℱ ranges over all the objects of D(𝒪_X) derived complete along ℐ', this is also the analogue of the display for complexes of quasi-coherent modules that the fifth and last sentence of [Stacks, Tag 0AKL] attributes to [HL-P, Theorem 6.5], at a morphism of schemes. At a morphism of algebraic stacks, for an arbitrary object, that analogue is AlgebraicGeometry.Stack.isIso_derivedCompletionPushforwardComparison_of_isAlgebraicStack of PushforwardCommutesCompletionAlgebraicStacks.lean; derived algebraic stacks, the other half of the setting of that reference, are not defined in this library.

The restriction to a derived-complete ℱ is on the object, not on the data: the invertibility for an arbitrary ℱ is the assertion of [Stacks, Tag 0A0G], and it is proved — at a morphism of ringed sites and at the constructed ℐ' = f^{-1}ℐ · 𝒪_X rather than at an independent parameter ℐ' — by RingedSite.isIso_derivedCompletionPushforwardComparison_inverseImageIdealSheaf_of_isFiniteType, and at a morphism of schemes and a quasi-coherent ℐ of finite type by Scheme.isIso_derivedCompletionPushforwardComparison_idealSheafData_inverseImageIdealSheaf.

theorem isIso_derivedCompletionPushforwardComparison_of_isFiniteType_of_isDerivedComplete
    [I.toSheafOfModules.IsFiniteType] [I'.toSheafOfModules.IsFiniteType]
    {K : DerivedCategory (_root_.SheafOfModules.{u}
      ((Stacks.SheafOfModules.Tensor.ringSheaf
        (Stacks.RingedSpace.toRingedSite X.toRingedSpace).O)))}
    (hK : RingedSite.IsDerivedComplete.{u, u, u, u}
      (Stacks.RingedSpace.toRingedSite X.toRingedSpace) I' K) :
    IsIso ((RingedSite.derivedCompletionPushforwardComparison
      (toRingedSiteHom f) I I' hI).app K)

AlgebraicGeometry.Scheme.isIso_derivedCompletionPushforwardComparison_idealSheafData_of_isDerivedComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionFiniteType.lean, line 496. The attribute's comment: “the mathematical content of Remark 52.7.4, which is its fifth and last sentence: the analogue of Equation 52.7.0.1 for complexes of quasi-coherent modules, [HL-P, Theorem 6.5]. What is proved here is that analogue at a morphism of schemes and at Section 52.7's own data — two quasi-coherent sheaves of ideals of finite type, ℐ ⊆ 𝒪_S and ℐ' ⊆ 𝒪_X with f^♯(f^{-1}ℐ) ⊆ ℐ' — for every object of D(𝒪_X) derived complete along ℐ', hence for every complex of quasi-coherent modules derived complete along ℐ'. Both derived completion functors are produced from the finite-type hypothesis by [Stacks, Tag 099F]. The remark's first four sentences are bibliography — pointers to [lurie-thesis, Theorem 6.3.1] for a derived formal functions theorem for proper maps, to [dag12, Chapter 4] with the cross-reference to More on Algebra, Section 091N for the affine story, and to [G-R, Section 2.9] for proper base change and derived completion via (ind) coherent modules — and carry no formalizable statement. At a morphism of algebraic stacks the analogue is AlgebraicGeometry.Stack.isIso_derivedCompletionPushforwardComparison_of_isAlgebraicStack; derived algebraic stacks, the other half of the setting of [HL-P, Theorem 6.5], are not defined in this library”.

Equation 52.7.0.1 of [Stacks, Tag 0A0I] at Section 52.7's own data, for a derived-complete object. Let f : X ⟶ S be a morphism of schemes, let ℐ ⊆ 𝒪_S be a quasi-coherent sheaf of ideals of finite type and let ℐ' ⊆ 𝒪_X be a quasi-coherent sheaf of ideals of finite type with f^♯(f^{-1}ℐ) ⊆ ℐ' — which the display's f^{-1}ℐ · 𝒪_X is. Then (Rf_*ℱ)^∧ ⟶ Rf_*(ℱ^∧) is invertible for every ℱ ∈ D(𝒪_X) derived complete along ℐ', in particular for every such complex of quasi-coherent modules.

This is the display written at the hypotheses Section 52.7 states it under, in the library's own scheme-theoretic vocabulary: ℐ and ℐ' are AlgebraicGeometry.Scheme.IdealSheafData, so quasi-coherent, and the finite-type hypothesis is SheafOfModules.IsFiniteType — locally generated by finitely many sections. It is isIso_derivedCompletionPushforwardComparison_of_isFiniteType_of_isDerivedComplete above at those sheaves of ideals, and the only thing the hypotheses are used for is [Stacks, Tag 099F], which is what produces the two derived completion functors.

Because ℱ ranges over the objects of D(𝒪_X) derived complete along ℐ' and not over quasi-coherent sheaves alone, this is also the analogue of the display for complexes of quasi-coherent modules that the fifth and last sentence of [Stacks, Tag 0AKL] attributes to [HL-P, Theorem 6.5], at a morphism of schemes.

The restriction to a derived-complete ℱ is on the object, not on the data: the invertibility for an arbitrary ℱ is the assertion of [Stacks, Tag 0A0G], and it is proved — at a morphism of ringed sites and at the constructed ℐ' = f^{-1}ℐ · 𝒪_X rather than at an independent parameter ℐ' — by RingedSite.isIso_derivedCompletionPushforwardComparison_inverseImageIdealSheaf_of_isFiniteType, and at a morphism of schemes and a quasi-coherent ℐ of finite type by Scheme.isIso_derivedCompletionPushforwardComparison_idealSheafData_inverseImageIdealSheaf.

theorem isIso_derivedCompletionPushforwardComparison_idealSheafData_of_isDerivedComplete
    [(idealSheafSiteSubmodule I).toSheafOfModules.IsFiniteType]
    [(idealSheafSiteSubmodule I').toSheafOfModules.IsFiniteType]
    {K : DerivedCategory (_root_.SheafOfModules.{u}
      ((Stacks.SheafOfModules.Tensor.ringSheaf
        (Stacks.RingedSpace.toRingedSite X.toRingedSpace).O)))}
    (hK : RingedSite.IsDerivedComplete.{u, u, u, u}
      (Stacks.RingedSpace.toRingedSite X.toRingedSpace) (idealSheafSiteSubmodule I') K) :
    IsIso ((RingedSite.derivedCompletionPushforwardComparison
      (toRingedSiteHom f) (idealSheafSiteSubmodule I) (idealSheafSiteSubmodule I') hI).app K)

AlgebraicGeometry.Scheme.isIso_derivedCompletionPushforwardComparison_idealSheafData_inverseImageIdealSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionFiniteType.lean, line 559. The attribute's comment: “the mathematical content of Remark 52.7.4, which is its fifth and last sentence: the analogue of Equation 52.7.0.1 for complexes of quasi-coherent modules, [HL-P, Theorem 6.5]. Proved here at a morphism of schemes f : X ⟶ S and at Section 52.7's own data — a quasi-coherent sheaf of ideals ℐ ⊆ 𝒪_S of finite type and the sheaf of ideals ℐ' = f^{-1}ℐ · 𝒪_X built out of it — for an arbitrary object of D(𝒪_X), hence for every complex of quasi-coherent modules, with no derived-completeness or nilpotence restriction: the canonical comparison map (Rf_*K)^∧ ⟶ Rf_*(K^∧) is invertible. That f^♯(f^{-1}ℐ) ⊆ ℐ' and that ℐ' is of finite type are theorems about the construction, not hypotheses. The remark's first four sentences are bibliography — pointers to [lurie-thesis, Theorem 6.3.1] for a derived formal functions theorem for proper maps, to [dag12, Chapter 4] with the cross-reference to More on Algebra, Section 091N for the affine story, and to [G-R, Section 2.9] for proper base change and derived completion via (ind) coherent modules — and carry no formalizable statement. At a morphism of algebraic stacks the analogue is AlgebraicGeometry.Stack.isIso_derivedCompletionPushforwardComparison_of_isAlgebraicStack; derived algebraic stacks, the other half of the setting of [HL-P, Theorem 6.5], are not defined in this library”.

Equation 52.7.0.1 of [Stacks, Tag 0A0I] at Section 52.7's own data, for an arbitrary object — and so the analogue for complexes of quasi-coherent modules of [Stacks, Tag 0AKL]. Let f : X ⟶ S be a morphism of schemes, let ℐ ⊆ 𝒪_S be a quasi-coherent sheaf of ideals of finite type and let ℐ' = f^{-1}ℐ · 𝒪_X be the sheaf of ideals Section 52.7 builds out of it. Then the canonical comparison map

(Rf_*K)^∧ ⟶ Rf_*(K^∧)

is invertible for every object K of D(𝒪_X), the completion on S being taken along ℐ and the one on X along ℐ'. In particular it is invertible for every complex of quasi-coherent 𝒪_X-modules, with no derived-completeness or nilpotence restriction.

ℐ is an AlgebraicGeometry.Scheme.IdealSheafData, read on the small Zariski ringed site by Stacks.Algebraization.idealSheafSiteSubmodule, and "of finite type" is SheafOfModules.IsFiniteType (automatic on a locally Noetherian scheme, by Stacks.Algebraization.isFiniteType_idealSheafSiteSubmodule). The sheaf of ideals ℐ' is AlgebraicGeometry.RingedSite.inverseImageIdealSheaf, the image of f^*ℐ ⟶ 𝒪_X; that f^♯ carries f^{-1}ℐ into it is AlgebraicGeometry.RingedSite.pushforwardIdealCompatible_inverseImageIdealSheaf, and that it is of finite type — so that the derived completion along it exists, by [Stacks, Tag 099F] — is AlgebraicGeometry.RingedSite.isFiniteType_inverseImageIdealSheaf. Neither is a hypothesis.

This is RingedSite.isIso_derivedCompletionPushforwardComparison_inverseImageIdealSheaf_of_isFiniteType, the ringed-sites case of [Stacks, Tag 0A0G], at the morphism of ringed sites AlgebraicGeometry.Scheme.toRingedSiteHom f underlying f.

theorem isIso_derivedCompletionPushforwardComparison_idealSheafData_inverseImageIdealSheaf
    [(idealSheafSiteSubmodule I).toSheafOfModules.IsFiniteType]
    (K : DerivedCategory (_root_.SheafOfModules.{u}
      ((Stacks.SheafOfModules.Tensor.ringSheaf
        (Stacks.RingedSpace.toRingedSite X.toRingedSpace).O)))) :
    IsIso ((RingedSite.derivedCompletionPushforwardComparison (toRingedSiteHom f)
      (idealSheafSiteSubmodule I)
      (RingedSite.inverseImageIdealSheaf.{u} (toRingedSiteHom f) (idealSheafSiteSubmodule I))
      (RingedSite.pushforwardIdealCompatible_inverseImageIdealSheaf.{u} (toRingedSiteHom f)
        (idealSheafSiteSubmodule I))).app K)

AlgebraicGeometry.Scheme.isIso_derivedCompletionPushforwardComparison_generatedIdealSheaf_of_isDerivedComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionGenerated.lean, line 472. The attribute's comment: “the mathematical content of Remark 52.7.4 — its fifth and last sentence, the analogue of Equation 52.7.0.1 for complexes of quasi-coherent modules, [HL-P, Theorem 6.5] — in the second of the two regimes this library reaches for it. Proved here: that analogue at a morphism of schemes, for an object of D(𝒪_X) that is derived complete along ℐ', with ℐ and ℐ' generated by finitely many global sections of the two structure sheaves, out of which both derived completion functors are built. The objects covered are therefore the derived-complete complexes of quasi-coherent modules, at ideal sheaves on which the only demand is those generators. The same analogue at two sheaves of ideals of finite type, which is the source's own hypothesis on the data, is AlgebraicGeometry.Scheme``.isIso_derivedCompletionPushforwardComparison_of_isFiniteType_of_isDerivedComplete of PushforwardCommutesCompletionFiniteType.lean, and for an arbitrary complex, at a quasi-coherent ℐ of finite type and ℐ' = f^{-1}ℐ · 𝒪_X, it is AlgebraicGeometry.Scheme``.isIso_derivedCompletionPushforwardComparison_idealSheafData_inverseImageIdealSheaf of the same file. At a morphism of algebraic stacks the analogue is AlgebraicGeometry.Stack.isIso_derivedCompletionPushforwardComparison_of_isAlgebraicStack of PushforwardCommutesCompletionAlgebraicStacks.lean; derived algebraic stacks, the other half of the setting of [HL-P, Theorem 6.5], are not defined in this library. The remark's first four sentences are bibliography — pointers to [lurie-thesis, Theorem 6.3.1] for a derived formal functions theorem for proper maps, to [dag12, Chapter 4] with the cross-reference to More on Algebra, Section 091N for the affine story, and to [G-R, Section 2.9] for proper base change and derived completion via (ind) coherent modules — and carry no formalizable statement. A further registration, which takes an arbitrary object in the regime where the local sections of both ideal sheaves are nilpotent, is in PushforwardCommutesCompletionSpaces.lean”.

[Stacks, Tag 0A0I] in the display's own setting, for a derived-complete object, with nothing assumed. Let f : X ⟶ S be a morphism of schemes, let ℐ = (t_1, …, t_s) ⊆ 𝒪_S and ℐ' = (g_1, …, g_r) ⊆ 𝒪_X be the sheaves of ideals generated by finitely many global sections of the two structure sheaves, with f^♯(f^{-1}ℐ) ⊆ ℐ' — which the display's f^{-1}ℐ · 𝒪_X satisfies. Then (Rf_*ℱ)^∧ ⟶ Rf_*(ℱ^∧) is invertible for every ℱ ∈ D(𝒪_X) derived complete along ℐ'.

Both derived completion functors are produced from the generators, by AlgebraicGeometry.RingedSite.isRightAdjoint_ι_isDerivedComplete_generatedIdealSheaf, so [Stacks, Tag 099F] is nowhere a hypothesis; neither quasi-coherence nor finite type nor quasi-coherence of ℱ is assumed either, those entering the source only through that tag. The restriction to a derived-complete ℱ is the tag's own content and remains; the invertibility for an arbitrary ℱ is the assertion of [Stacks, Tag 0A0G]. The descent from a globally generated ℐ to a finite-type one is carried out in PushforwardCommutesCompletionFiniteType.lean, where the derived completion functors come from [Stacks, Tag 099F] at a sheaf of ideals of finite type; this statement is the case of AlgebraicGeometry.Scheme .isIso_derivedCompletionPushforwardComparison_of_isFiniteType_of_isDerivedComplete there in which the two sheaves of ideals are generated by global sections.

Because ℱ ranges over the derived-complete objects of D(𝒪_X) and not over quasi-coherent sheaves alone, this is also the analogue of the display for complexes of quasi-coherent modules that the fifth and last sentence of [Stacks, Tag 0AKL] attributes to [HL-P, Theorem 6.5]; related statements are isIso_derivedCompletionPushforwardComparison_of_isFiniteType_of_isDerivedComplete of PushforwardCommutesCompletionFiniteType.lean, the same statement at two sheaves of ideals of finite type, and AlgebraicGeometry.Scheme.isIso_derivedCompletionPushforwardComparison_of_forall_isNilpotent of PushforwardCommutesCompletionSpaces.lean, which takes an arbitrary object in the nilpotent regime and whose module documentation accounts for the remark sentence by sentence.

theorem isIso_derivedCompletionPushforwardComparison_generatedIdealSheaf_of_isDerivedComplete
    {K : DerivedCategory (_root_.SheafOfModules.{u}
      ((Stacks.SheafOfModules.Tensor.ringSheaf
        (Stacks.RingedSpace.toRingedSite X.toRingedSpace).O)))}
    (hK : RingedSite.IsDerivedComplete.{u, u, u, u}
      (Stacks.RingedSpace.toRingedSite X.toRingedSpace) (generatedIdealSheaf g) K) :
    IsIso ((RingedSite.derivedCompletionPushforwardComparison (toRingedSiteHom f)
      (generatedIdealSheaf t) (generatedIdealSheaf g) hI).app K)

AlgebraicGeometry.Scheme.isIso_derivedCompletionPushforwardComparison_of_forall_isNilpotent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletionSpaces.lean, line 411. The attribute's comment: “the mathematical content of Remark 52.7.4, which is its fifth and last sentence: the analogue of Equation 52.7.0.1 for complexes of quasi-coherent modules, [HL-P, Theorem 6.5]. What is proved here is that analogue at a morphism of schemes for an arbitrary object of D(𝒪_X), hence for an arbitrary complex of quasi-coherent modules, in the regime where the local sections of both sheaves of ideals are nilpotent — the regime in which this library builds the two derived completion functors out of the data, which is why this statement has no instance argument. The same analogue at the source's own data, two sheaves of ideals of finite type, is AlgebraicGeometry.Scheme .isIso_derivedCompletionPushforwardComparison_of_isFiniteType_of_isDerivedComplete of PushforwardCommutesCompletionFiniteType.lean, for a complex derived complete along ℐ'. An arbitrary complex at a quasi-coherent sheaf of ideals of finite type and ℐ' = f^{-1}ℐ · 𝒪_X is AlgebraicGeometry.Scheme .isIso_derivedCompletionPushforwardComparison_idealSheafData_inverseImageIdealSheaf of PushforwardCommutesCompletionFiniteType.lean. At a morphism of algebraic stacks it is AlgebraicGeometry.Stack.isIso_derivedCompletionPushforwardComparison_of_isAlgebraicStack of PushforwardCommutesCompletionAlgebraicStacks.lean; derived algebraic stacks, the other half of the setting of [HL-P, Theorem 6.5], are not defined in this library. The remark's first four sentences are bibliography — pointers to [lurie-thesis, Theorem 6.3.1] for a derived formal functions theorem for proper maps, to [dag12, Chapter 4] with the cross-reference to More on Algebra, Section 091N for the affine story, and to [G-R, Section 2.9] for proper base change and derived completion via (ind) coherent modules — and carry no formalizable statement. A third registration, at a derived-complete object and ideal sheaves generated by finitely many global sections, is in PushforwardCommutesCompletionGenerated.lean”.

Equation 52.7.0.1 of [Stacks, Tag 0A0I] in the display's own setting, for an arbitrary object, when the local sections of ℐ and of ℐ' are nilpotent: the comparison (Rf_*ℱ)^∧ ⟶ Rf_*(ℱ^∧) is invertible for every ℱ ∈ D(𝒪_X), in particular for every quasi-coherent ℱ, with no hypothesis on ℱ.

The restriction is on the two sheaves of ideals, not on ℱ, and it discharges the conclusion of [Stacks, Tag 099F] on X and on S rather than assuming it: this statement has no instance hypothesis. It is not the general case of the display — nilpotence is not the source's hypothesis, and in that regime both derived completion functors are the identity. The display at the source's own data, two sheaves of ideals of finite type, is AlgebraicGeometry.Scheme .isIso_derivedCompletionPushforwardComparison_of_isFiniteType_of_isDerivedComplete of PushforwardCommutesCompletionFiniteType.lean, for an object derived complete along ℐ'. An arbitrary object, at a quasi-coherent sheaf of ideals ℐ of finite type and ℐ' = f^{-1}ℐ · 𝒪_X, is Scheme.isIso_derivedCompletionPushforwardComparison_idealSheafData_inverseImageIdealSheaf of the same file.

Because ℱ ranges over all of D(𝒪_X), this is also the analogue of the display for complexes of quasi-coherent modules that the fifth and last sentence of [Stacks, Tag 0AKL] attributes to [HL-P, Theorem 6.5], in the nilpotent regime. The derived-complete case of that remark is, at two sheaves of ideals of finite type, AlgebraicGeometry.Scheme .isIso_derivedCompletionPushforwardComparison_of_isFiniteType_of_isDerivedComplete of PushforwardCommutesCompletionFiniteType.lean, and at ideal sheaves generated by finitely many global sections, AlgebraicGeometry.Scheme .isIso_derivedCompletionPushforwardComparison_generatedIdealSheaf_of_isDerivedComplete of PushforwardCommutesCompletionGenerated.lean.

theorem isIso_derivedCompletionPushforwardComparison_of_forall_isNilpotent
    (hnil : ∀ (V : TopologicalSpace.Opens X.toRingedSpace.carrier)
      (g : ((Stacks.SheafOfModules.Tensor.ringSheaf
        (Stacks.RingedSpace.toRingedSite X.toRingedSpace).O)).obj.obj (op V)),
      g ∈ I'.toSubmodule.obj (op V) → IsNilpotent g)
    (hnil' : ∀ (W : TopologicalSpace.Opens S.toRingedSpace.carrier)
      (s : ((Stacks.SheafOfModules.Tensor.ringSheaf
        (Stacks.RingedSpace.toRingedSite S.toRingedSpace).O)).obj.obj (op W)),
      s ∈ I.toSubmodule.obj (op W) → IsNilpotent s)
    (K : DerivedCategory (_root_.SheafOfModules.{u}
      ((Stacks.SheafOfModules.Tensor.ringSheaf
        (Stacks.RingedSpace.toRingedSite X.toRingedSpace).O)))) :
    letI : (ObjectProperty.ι (RingedSite.IsDerivedComplete.{u, u, u, u}
        (Stacks.RingedSpace.toRingedSite X.toRingedSpace) I')).IsRightAdjoint :=
      RingedSite.isRightAdjoint_ι_isDerivedComplete_of_forall_isNilpotent
        (Stacks.RingedSpace.toRingedSite X.toRingedSpace) I' hnil
    letI : (ObjectProperty.ι (RingedSite.IsDerivedComplete.{u, u, u, u}
        (Stacks.RingedSpace.toRingedSite S.toRingedSpace) I)).IsRightAdjoint :=
      RingedSite.isRightAdjoint_ι_isDerivedComplete_of_forall_isNilpotent
        (Stacks.RingedSpace.toRingedSite S.toRingedSpace) I hnil'
    IsIso ((RingedSite.derivedCompletionPushforwardComparison
      (toRingedSiteHom f) I I' hI).app K)

AlgebraicGeometry.RingedSite.isDerivedComplete_derivedPushforward_derivedSheafHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCompletionComplete.lean, line 113. The attribute's comment: “the mathematical content of the remark, which is its fifth and last sentence: the analogue of the displayed equation (0A0I) for complexes of quasi-coherent modules, [HL-P, Theorem 6.5]. The first four sentences are bibliography and carry no mathematical statement — a pointer to [lurie-thesis, Theorem 6.3.1] for a derived formal functions theorem for proper maps, one to [dag12, Chapter 4] together with the cross-reference to More on Algebra, Section 091N for the affine story, and one to [G-R, Section 2.9] for proper base change and derived completion via (ind) coherent modules. Covered here and in isDerivedComplete_derivedSheafHom_derivedPushforward: that both sides of (0A0I) are derived complete, for an arbitrary coefficient object of the derived category of modules, which subsumes the complexes of quasi-coherent modules the sentence speaks of. This is the step of the proof of Tag 0A0G that makes the comparison between the two sides canonical. NOT covered: the comparison isomorphism itself, which cannot be stated while Tag 099B and Tag 099F leave the derived completion without the universal property that pins the map down, nor proved while Tag 0944 and Tag 0A0E are unavailable; and not the setting of (derived) algebraic stacks in which [HL-P, Theorem 6.5] is stated. See the module documentation.”.

The pushed-forward completion is derived complete. Let f : (Sh(𝒟), 𝒪') ⟶ (Sh(𝒞), 𝒪) be a morphism of ringed sites and let ℐ ⊂ 𝒪, ℐ' ⊂ 𝒪' be sheaves of ideals such that f^♯ sends f^{-1}ℐ into ℐ'. If K in D(𝒪') is derived complete along ℐ', then for every M in D(𝒪') the object Rf_*(R𝑆heafHom_{𝒪'}(M, K)) is derived complete along ℐ.

Taking M to be the extended alternating Čech complex of a finite family of global sections generating ℐ', so that R𝑆heafHom_{𝒪'}(M, K) is the derived completion K^∧ of [Stacks, Tag 099B], this says that the left-hand side Rf_*(K^∧) of the displayed equation of [Stacks, Tag 0A0I] is derived complete.

[Stacks, Tag 099A] puts R𝑆heafHom_{𝒪'}(M, K) in D_comp(𝒪', ℐ'), and [Stacks, Tag 099J] carries it from there into D_comp(𝒪, ℐ).

theorem isDerivedComplete_derivedPushforward_derivedSheafHom
    (I : SheafOfModules.Submodule
      (SheafOfModules.unit ((Stacks.SheafOfModules.Tensor.ringSheaf Y.O))))
    (I' : SheafOfModules.Submodule
      (SheafOfModules.unit ((Stacks.SheafOfModules.Tensor.ringSheaf X.O))))
    (hI : ∀ (W : Y.C) (s : ((Stacks.SheafOfModules.Tensor.ringSheaf Y.O)).obj.obj (op W)),
      s ∈ I.toSubmodule.obj (op W) →
        fSharpSection f W s ∈ I'.toSubmodule.obj (op (f.u.obj W)))
    (M K : DerivedCategory (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O))))
    (hK : IsDerivedComplete.{u, u, u, u} X I' K) :
    IsDerivedComplete.{u, u, u, u} Y I
      ((derivedPushforward.{u} f.toRingedToposSiteHom).obj
        (((derivedSheafHomBifunctor X).obj (op M)).obj K))

AlgebraicGeometry.RingedSite.isDerivedComplete_derivedSheafHom_derivedPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCompletionComplete.lean, line 142. The attribute's comment: “the second half of the covered statement; see isDerivedComplete_derivedPushforward_derivedSheafHom for the full accounting of which sentences of the remark carry mathematical content and of what is and is not covered.”.

The completion of a pushforward is derived complete. In the situation of isDerivedComplete_derivedPushforward_derivedSheafHom, for every N in D(𝒪) the object R𝑆heafHom_𝒪(N, Rf_*K) is derived complete along ℐ.

Taking N to be the extended alternating Čech complex of a finite family of global sections generating ℐ, this says that the right-hand side (Rf_*K)^∧ of the displayed equation of [Stacks, Tag 0A0I] is derived complete.

The two inputs are used in the opposite order to the companion result: [Stacks, Tag 099J] puts Rf_*K in D_comp(𝒪, ℐ) and [Stacks, Tag 099A] keeps the derived internal Hom into it there.

theorem isDerivedComplete_derivedSheafHom_derivedPushforward
    (I : SheafOfModules.Submodule
      (SheafOfModules.unit ((Stacks.SheafOfModules.Tensor.ringSheaf Y.O))))
    (I' : SheafOfModules.Submodule
      (SheafOfModules.unit ((Stacks.SheafOfModules.Tensor.ringSheaf X.O))))
    (hI : ∀ (W : Y.C) (s : ((Stacks.SheafOfModules.Tensor.ringSheaf Y.O)).obj.obj (op W)),
      s ∈ I.toSubmodule.obj (op W) →
        fSharpSection f W s ∈ I'.toSubmodule.obj (op (f.u.obj W)))
    (N : DerivedCategory (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf Y.O))))
    (K : DerivedCategory (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O))))
    (hK : IsDerivedComplete.{u, u, u, u} X I' K) :
    IsDerivedComplete.{u, u, u, u} Y I
      (((derivedSheafHomBifunctor Y).obj (op N)).obj
        ((derivedPushforward.{u} f.toRingedToposSiteHom).obj K))

Sources

• Section 52.7, Tag 0A0H
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.RingedSite.isIso_derivedCompletionPushforwardComparison_of_isDerivedComplete · AlgebraicGeometry.RingedSite.isIso_derivedCompletionPushforwardComparison_generatedIdealSheaf · AlgebraicGeometry.RingedSite.isIso_derivedCompletionPushforwardComparison_inverseImageIdealSheaf · AlgebraicGeometry.RingedSite.derivedPushforwardDerivedCompletionGeneratedIdealSheafIso · AlgebraicGeometry.RingedSite.isDerivedComplete_derivedPushforward_derivedCompletion_inverseImageIdealSheaf · AlgebraicGeometry.RingedSite.isIso_derivedCompletionPushforwardComparison_inverseImageIdealSheaf_of_isDerivedComplete · Stacks.RingedSpace.isDerivedComplete_derivedPushforward_derivedCompletion_inverseImageIdealSheaf · Stacks.RingedSpace.isIso_derivedCompletionPushforwardComparison_inverseImageIdealSheaf_of_isDerivedComplete

Section52.8 Algebraization of local cohomology, I#

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

Tag 0EFG, an equation

Tag 0EFG in the Stacks Project.

Stacks.Algebraization.associatedSubset, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AssociatedSubset.lean, line 42.

The primes whose specializations in V(I) all belong to V(J) ∩ V(I).

This is the subset denoted by T in Stacks Project, Tag 0EFG.

def associatedSubset (I J : Ideal A) : Set (PrimeSpectrum A)

Tag 0EFH, a lemma

Tag 0EFH in the Stacks Project.

Stacks.Algebraization.exists_notMem_mem_annihilator_homology_derivedCompletion_localCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/AnnihilatorCompletedLocalCohomology.lean, line 143. The attribute's comment: “the full statement: an element outside p annihilating the cohomology of the derived I-adic completion of RΓ_{V(J)}(M) in every degree ≤ s”.

Let I and J be ideals of a Noetherian ring A with a dualizing complex, let M be a finite A-module, and let p be a prime outside V(J) ∩ V(I) with cd(A, I) ≤ d. If depth_{A_{p'}}(M_{p'}) + dim((A/p')_q) > s + d for all primes p' ⊆ p and all q ∈ V(p') ∩ V(J) ∩ V(I), then some f ∈ A outside p annihilates the degree-i cohomology of the derived I-adic completion of RΓ_{V(J)}(M) for every i ≤ s.

theorem exists_notMem_mem_annihilator_homology_derivedCompletion_localCohomology
    (A : Type u) [CommRing A] [IsNoetherianRing A]
    (M : Type u) [AddCommGroup M] [Module A M] [Module.Finite A M]
    (I J : Ideal A) (p : PrimeSpectrum A) (s d : ℤ)
    (omega : DerivedCategory (ModuleCat.{u} A))
    (homega : Dualizing.IsDualizingComplex (A := A) (K := omega))
    (hp : p ∉ PrimeSpectrum.zeroLocus (J : Set A) ∩ PrimeSpectrum.zeroLocus (I : Set A))
    (hcd : Stacks.LocalCohomology.cohomologicalDimension A I I.fg_of_isNoetherianRing ≤ d)
    (hdepth : ∀ x y : PrimeSpectrum A, x.asIdeal ≤ p.asIdeal →
      y ∈ PrimeSpectrum.zeroLocus (J : Set A) ∩ PrimeSpectrum.zeroLocus (I : Set A) →
      x.asIdeal ≤ y.asIdeal →
      enatToEInt
          (Module.depth (Localization.AtPrime x.asIdeal)
            (maximalIdeal (Localization.AtPrime x.asIdeal))
            (LocalizedModule x.asIdeal.primeCompl M)) +
        krullDimToEInt
          (ringKrullDim ((Localization.AtPrime y.asIdeal) ⧸
            x.asIdeal.map (algebraMap A (Localization.AtPrime y.asIdeal)))) >
        ((s + d : ℤ) : EInt))
    {r : ℕ} (gen : Fin r → A) (hgen : Ideal.span (Set.range gen) = I) :
    ∃ f : A, f ∉ p.asIdeal ∧ ∀ i : ℤ, i ≤ s →
      f ∈ Module.annihilator A
        ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).obj
          ((DerivedCompletion.derivedCompletionFunctor A gen).obj
            ((Dualizing.derivedPowerTorsionProperty A J J.fg_of_isNoetherianRing).ι.obj
              ((Dualizing.localCohomologyFunctor.{u, u} A J J.fg_of_isNoetherianRing).obj
                ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
                  (ModuleCat.of A M))))))

Stacks.Algebraization.prod_smul_id_derivedHom_homology_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/AnnihilatorTruncationReduction.lean, line 325. The attribute's comment: “the quantitative form of the truncation reduction, with the explicit product of per-degree annihilators”.

The engine. For P concentrated in degrees ≤ d and Q in degrees ≥ a, the product of scalars annihilating H^j(Q) for a ≤ j ≤ s + d annihilates H^i(RHom_A(P, Q)) for every i ≤ s.

public theorem prod_smul_id_derivedHom_homology_eq_zero {A : Type u} [CommRing A] (f : ℤ → A)
    (a d s : ℤ) (P Q : DerivedCategory (ModuleCat.{u} A)) [P.IsLE d] [Q.IsGE a]
    (hQ : ∀ j : ℤ, j ≤ s + d →
      f j • 𝟙 ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) j).obj Q) = 0)
    (i : ℤ) (hi : i ≤ s) :
    (∏ j ∈ Finset.range ((s + d - a).toNat + 1), f (a + j)) • 𝟙
      ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).obj
        ((StacksDraft.DerivedHom.derivedHomAdjunction (R := A)).hom.obj
          (Opposite.op P, Q))) = 0

Stacks.Algebraization.exists_notMem_mem_annihilator_homology_derivedHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/AnnihilatorTruncationReduction.lean, line 364. The attribute's comment: “the homological-algebra reduction: after the two identifications of the first paragraph, the canonical-truncation argument producing an element outside p annihilating H^i(RHom(P, Q)) for i ≤ s”.

Stacks 0EFH, the homological reduction. Let P have cohomology concentrated in degrees ≤ d and Q in degrees ≥ a. If for each j ≤ s + d some element outside a prime p annihilates H^j(Q), then one element outside p annihilates H^i(RHom_A(P, Q)) for all i ≤ s.

public theorem exists_notMem_mem_annihilator_homology_derivedHom {A : Type u} [CommRing A]
    (p : PrimeSpectrum A) (a d s : ℤ) (P Q : DerivedCategory (ModuleCat.{u} A)) [Q.IsGE a]
    (hP : ∀ i : ℤ, d < i →
      IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).obj P))
    (hQ : ∀ j : ℤ, j ≤ s + d → ∃ f : A, f ∉ p.asIdeal ∧
      f ∈ Module.annihilator A
        ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) j).obj Q)) :
    ∃ g : A, g ∉ p.asIdeal ∧ ∀ i : ℤ, i ≤ s →
      g ∈ Module.annihilator A
        ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).obj
          ((StacksDraft.DerivedHom.derivedHomAdjunction (R := A)).hom.obj
            (Opposite.op P, Q)))

Stacks.LocalCohomology.isLE_localCohomologyDerived_single_of_cohomologicalDimension_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/LocalCohomologyAnnihilatorInputs.lean, line 108. The attribute's comment: “the use of hypothesis (3): H^i(RΓ_I(A)) = 0 for i > d when cd(A, I) ≤ d”.

A bound d on the cohomological dimension of I places the local cohomology RΓ_{V(I)}(M[0]) of Stacks 0A6Q in degrees ≤ d.

theorem isLE_localCohomologyDerived_single_of_cohomologicalDimension_le
    (A : Type u) [CommRing A] (I : Ideal A) (hI : I.FG) (d : ℤ)
    (hcd : cohomologicalDimension A I hI ≤ d) (M : ModuleCat.{u} A) :
    ((Dualizing.derivedPowerTorsionProperty A I hI).ι.obj
      ((Dualizing.localCohomologyFunctor A I hI).obj
        ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj M))).IsLE d

Stacks.LocalCohomology.isGE_localCohomologyDerived_single, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/LocalCohomologyAnnihilatorInputs.lean, line 152. The attribute's comment: “the boundedness the truncation reduction needs: RΓ_{V(I)}(M[0]) lies in degrees ≥ 0”.

The local cohomology RΓ_{V(I)}(M[0]) of Stacks 0A6Q of a module placed in degree zero lies in degrees ≥ 0.

theorem isGE_localCohomologyDerived_single
    (A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A) (hI : I.FG)
    (M : ModuleCat.{u} A) :
    ((Dualizing.derivedPowerTorsionProperty A I hI).ι.obj
      ((Dualizing.localCohomologyFunctor A I hI).obj
        ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj M))).IsGE 0

Stacks.LocalCohomology.exists_notMem_mem_annihilator_localCohomologyWithSupportIn_sup, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/LocalCohomologyAnnihilatorInputs.lean, line 202. The attribute's comment: “the per-degree annihilator input: a single element outside p annihilating H^j_{V(I+J)}(M) for every j ≤ s + d”.

The per-degree annihilator input of Stacks 0EFH, in the support-indexed model. For M finite over a Noetherian ring A with a dualizing complex and p a prime outside V(J) ∩ V(I), the depth-plus-dimension inequality in the range s + d gives one element of A outside p annihilating H^j_{V(I+J)}(M) for every j ≤ s + d.

theorem exists_notMem_mem_annihilator_localCohomologyWithSupportIn_sup
    (A : Type u) [CommRing A] [IsNoetherianRing A]
    (M : Type u) [AddCommGroup M] [Module A M] [Module.Finite A M]
    (I J : Ideal A) (p : PrimeSpectrum A) (s d : ℤ)
    (omega : DerivedCategory (ModuleCat.{u} A))
    (homega : Dualizing.IsDualizingComplex (A := A) (K := omega))
    (hp : p ∉ PrimeSpectrum.zeroLocus (J : Set A) ∩ PrimeSpectrum.zeroLocus (I : Set A))
    (hdepth : ∀ x y : PrimeSpectrum A, x.asIdeal ≤ p.asIdeal →
      y ∈ PrimeSpectrum.zeroLocus (J : Set A) ∩ PrimeSpectrum.zeroLocus (I : Set A) →
      x.asIdeal ≤ y.asIdeal →
      enatToEInt
          (Module.depth (Localization.AtPrime x.asIdeal)
            (maximalIdeal (Localization.AtPrime x.asIdeal))
            (LocalizedModule x.asIdeal.primeCompl M)) +
        krullDimToEInt
          (ringKrullDim ((Localization.AtPrime y.asIdeal) ⧸
            x.asIdeal.map (algebraMap A (Localization.AtPrime y.asIdeal)))) >
        ((s + d : ℤ) : EInt)) :
    ∃ f : A, f ∉ p.asIdeal ∧ ∀ j : ℤ, j ≤ s + d →
      f ∈ Module.annihilator A
        (localCohomologyWithSupportIn.{u, u} A
          (PrimeSpectrum.zeroLocus ((I ⊔ J : Ideal A) : Set A))
          ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj (ModuleCat.of A M)) j)

Stacks.LocalCohomology.exists_notMem_mem_annihilator_localCohomologyModule_sup, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/LocalCohomologyAnnihilatorInputs.lean, line 246. The attribute's comment: “the per-degree annihilator input, in the RΓ_{V(I+J)} coreflection model”.

The per-degree annihilator input of Stacks 0EFH, in the coreflection model. The annihilator of the previous statement, transported to the local cohomology RΓ_{V(I+J)} of Stacks 0A6Q along the comparison of Stacks 0955.

theorem exists_notMem_mem_annihilator_localCohomologyModule_sup
    (A : Type u) [CommRing A] [IsNoetherianRing A]
    (M : Type u) [AddCommGroup M] [Module A M] [Module.Finite A M]
    (I J : Ideal A) (p : PrimeSpectrum A) (s d : ℤ)
    (omega : DerivedCategory (ModuleCat.{u} A))
    (homega : Dualizing.IsDualizingComplex (A := A) (K := omega))
    (hp : p ∉ PrimeSpectrum.zeroLocus (J : Set A) ∩ PrimeSpectrum.zeroLocus (I : Set A))
    (hdepth : ∀ x y : PrimeSpectrum A, x.asIdeal ≤ p.asIdeal →
      y ∈ PrimeSpectrum.zeroLocus (J : Set A) ∩ PrimeSpectrum.zeroLocus (I : Set A) →
      x.asIdeal ≤ y.asIdeal →
      enatToEInt
          (Module.depth (Localization.AtPrime x.asIdeal)
            (maximalIdeal (Localization.AtPrime x.asIdeal))
            (LocalizedModule x.asIdeal.primeCompl M)) +
        krullDimToEInt
          (ringKrullDim ((Localization.AtPrime y.asIdeal) ⧸
            x.asIdeal.map (algebraMap A (Localization.AtPrime y.asIdeal)))) >
        ((s + d : ℤ) : EInt)) :
    ∃ f : A, f ∉ p.asIdeal ∧ ∀ j : ℤ, j ≤ s + d →
      f ∈ Module.annihilator A
        (localCohomologyModule A (I ⊔ J) (I ⊔ J).fg_of_isNoetherianRing
          (ModuleCat.of A M) j)

Stacks.Algebraization.derivedCompletionLocalCohomologySupIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/LocalCohomologyCompletionComparison.lean, line 114. The attribute's comment: “the first identification of the proof: RΓ_J(-)^∧ = RΓ_{I+J}(-)^∧, which is what lets J be replaced by I + J”.

For ideals I and J of A with I generated by the finite family f, derived I-adic completion does not distinguish RΓ_{V(J)} from RΓ_{V(J + I)}: there is a natural isomorphism RΓ_{V(J)}(-)^∧ ≅ RΓ_{V(J + I)}(-)^∧.

def derivedCompletionLocalCohomologySupIso (A : Type u) [CommRing A] (I J : Ideal A)
    (hI : I.FG) (hJ : J.FG) {r : ℕ} (f : Fin r → A) (hf : Ideal.span (Set.range f) = I) :
    Dualizing.localCohomologyFunctor.{u, u} A J hJ ⋙
        (Dualizing.derivedPowerTorsionProperty A J hJ).ι ⋙
          DerivedCompletion.derivedCompletionFunctor A f ≅
      Dualizing.localCohomologyFunctor.{u, u} A (J + I) (Submodule.FG.sup hJ hI) ⋙
        (Dualizing.derivedPowerTorsionProperty A (J + I) (Submodule.FG.sup hJ hI)).ι ⋙
          DerivedCompletion.derivedCompletionFunctor A f

Stacks.Algebraization.derivedCompletionIsoDerivedHomLocalCohomology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/LocalCohomologyCompletionComparison.lean, line 150. The attribute's comment: “the second identification of the proof: derived I-adic completion is RHom out of RΓ_{V(I)}(A)”.

For a finite family f generating I, derived I-adic completion is derived Hom out of the local cohomology RΓ_{V(I)}(A) of the ring: K^∧ ≅ RHom_A(RΓ_{V(I)}(A), K).

def derivedCompletionIsoDerivedHomLocalCohomology (A : Type u) [CommRing A] (I : Ideal A)
    (hI : I.FG) {r : ℕ} (f : Fin r → A) (hf : Ideal.span (Set.range f) = I)
    (K : DerivedCategory (ModuleCat.{u} A)) :
    (DerivedCompletion.derivedCompletionFunctor A f).obj K ≅
      (StacksDraft.DerivedHom.derivedHomAdjunction (R := A)).hom.obj
        (Opposite.op ((Stacks.LocalCohomology.localCohomologyOnModules.{u, u} A I hI).obj
          (ModuleCat.of A A)), K)

Stacks.Algebraization.derivedCompletionIsoDerivedHomDerivedPowerTorsion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/LocalCohomologyCompletionComparison.lean, line 165. The attribute's comment: “the second identification of the proof, written with RΓ_I(A) over a Noetherian ring”.

Over a Noetherian ring derived I-adic completion is derived Hom out of derived I-power torsion of the ring: K^∧ ≅ RHom_A(RΓ_I(A), K).

def derivedCompletionIsoDerivedHomDerivedPowerTorsion (A : Type u) [CommRing A]
    [IsNoetherianRing A] (I : Ideal A) {r : ℕ} (f : Fin r → A)
    (hf : Ideal.span (Set.range f) = I) (K : DerivedCategory (ModuleCat.{u} A)) :
    (DerivedCompletion.derivedCompletionFunctor A f).obj K ≅
      (StacksDraft.DerivedHom.derivedHomAdjunction (R := A)).hom.obj
        (Opposite.op (Stacks.LocalCohomology.derivedPowerTorsionObj.{u, u} A I
          (Ideal.fg_of_isNoetherianRing I) (ModuleCat.of A A)), K)

Stacks.Algebraization.derivedCompletionLocalCohomologyIsoDerivedHomSup, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/LocalCohomologyCompletionComparison.lean, line 180. The attribute's comment: “the two identifications of the first paragraph of the proof, composed into the form the truncation reduction consumes”.

For ideals I and J of A with I generated by the finite family f, the derived I-adic completion of RΓ_{V(J)}(K) is RHom_A(RΓ_{V(I)}(A), RΓ_{V(J + I)}(K)).

def derivedCompletionLocalCohomologyIsoDerivedHomSup (A : Type u) [CommRing A] (I J : Ideal A)
    (hI : I.FG) (hJ : J.FG) {r : ℕ} (f : Fin r → A) (hf : Ideal.span (Set.range f) = I)
    (K : DerivedCategory (ModuleCat.{u} A)) :
    (DerivedCompletion.derivedCompletionFunctor A f).obj
        ((Dualizing.derivedPowerTorsionProperty A J hJ).ι.obj
          ((Dualizing.localCohomologyFunctor.{u, u} A J hJ).obj K)) ≅
      (StacksDraft.DerivedHom.derivedHomAdjunction (R := A)).hom.obj
        (Opposite.op ((Stacks.LocalCohomology.localCohomologyOnModules.{u, u} A I hI).obj
            (ModuleCat.of A A)),
          (Dualizing.derivedPowerTorsionProperty A (J + I) (Submodule.FG.sup hJ hI)).ι.obj
            ((Dualizing.localCohomologyFunctor.{u, u} A (J + I)
              (Submodule.FG.sup hJ hI)).obj K))

Tag 0EFI, a lemma

Tag 0EFI in the Stacks Project.

Stacks.Algebraization.stabilizingIdeal_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/Stabilization.lean, line 318. The attribute's comment: “the stabilizing ideal is contained in J”.

Stacks 0EFI. The stabilizing ideal is contained in the ideal it shrinks.

public theorem stabilizingIdeal_le :
    stabilizingIdeal I J s d omega H ≤ J

Stacks.Algebraization.zeroLocus_stabilizingIdeal_inter, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/Stabilization.lean, line 328. The attribute's comment: “V(J₀) ∩ V(I) = V(J) ∩ V(I) for the stabilizing ideal”.

Stacks 0EFI. Shrinking J to the stabilizing ideal does not change the intersection of the zero locus with V(I).

public theorem zeroLocus_stabilizingIdeal_inter :
    PrimeSpectrum.zeroLocus (stabilizingIdeal I J s d omega H : Set A) ∩
        PrimeSpectrum.zeroLocus (I : Set A) =
      PrimeSpectrum.zeroLocus (J : Set A) ∩
        PrimeSpectrum.zeroLocus (I : Set A)

Stacks.Algebraization.exists_isStabilizingData_of_nonpos, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/StabilizationExistence/CandidateIdeal.lean, line 499. The attribute's comment: “the existence of the stabilizing data, for s ≤ 0”.

Stacks 0EFI for s ≤ 0. Let I and J be ideals of a Noetherian ring A and let M be a finite A-module. For every integer s ≤ 0 there is a pair (J₀, n) with the stabilization property of Stacks 0EFI: J₀ ≤ J and V(J₀) ∩ V(I) = V(J) ∩ V(I), every further ideal J' ≤ J₀ with V(J') ∩ V(I) = V(J) ∩ V(I) has RΓ_{J₀}(M) → RΓ_{J'}(M) an isomorphism on cohomology in degrees ≤ s, and (J₀ I) ^ n annihilates all of those cohomology modules.

The ideal is the one the source constructs, J₀ = J ⊓ I(B) for B the set of primes outside V(I) lying in T at which the depth of M is at most s. In this range the hypotheses (1)–(4) of the source — a dualizing complex and bounds on depth and relative dimension — are not needed: the semicontinuity argument of Claim I is replaced by the nonnegativity of depth, and the annihilator criterion Stacks 0EFC of Claim III by the finiteness of H⁰_{J₀}(M).

For s ≥ 1 the hypotheses are needed; see Stacks.Algebraization.exists_isStabilizingData.

public theorem exists_isStabilizingData_of_nonpos
    {A : Type u} [CommRing A] [IsNoetherianRing A]
    {M : Type v} [AddCommGroup M] [Module A M] [Module.Finite A M]
    (I J : Ideal A) (s : ℤ) (hs : s ≤ 0) :
    ∃ p : Ideal A × ℕ, IsStabilizingData (M := M) I J s p

Stacks.Algebraization.exists_isStabilizingData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/StabilizationExistence/UniformAnnihilation.lean, line 354. The attribute's comment: “the existence of the stabilizing data, given hypotheses (1)-(4) and 0 ≤ d”.

Stacks 0EFI. Let I and J be ideals of a Noetherian ring A, let M be a finite A-module, and let s and d be integers with 0 ≤ d. Under hypotheses (1)–(4) of the source there is a pair (J₀, n) with the stabilization property: J₀ ≤ J and V(J₀) ∩ V(I) = V(J) ∩ V(I), every further ideal J' ≤ J₀ with V(J') ∩ V(I) = V(J) ∩ V(I) has RΓ_{J₀}(M) → RΓ_{J'}(M) an isomorphism on cohomology in degrees ≤ s, and (J₀ I) ^ n annihilates all of those cohomology modules.

The proof is the source's. The ideal is J ⊓ I(B) for B the set of primes outside V(I) lying in T at which the depth of M is at most s, shrunk once more at the end to absorb the annihilator ideal; Claim I is the semicontinuity of depth + δ, Claim II the comparison criterion Stacks 0DWV, and Claim III Faltings' annihilator theorem Stacks 0EFC.

0 ≤ d belongs to the statement of 0EFI: the source's wording omits it, uses it silently in Claim III, and is false without it, by the counterexample Stacks.Algebraization.not_forall_exists_isStabilizingData_of_neg (StacksFrontier/AlgebraicGeometry/FormalGeometry/StabilizationCounterexample.lean:451). It is not recorded by Stacks.Algebraization.StabilizationHypotheses and does not follow from it. See Stacks.Algebraization.exists_isStabilizingData_iff_of_neg for what the conclusion amounts to when d < 0, and the module docstring for the erratum.

public theorem exists_isStabilizingData
    {A : Type u} [CommRing A] [IsNoetherianRing A]
    {M : Type u} [AddCommGroup M] [Module A M] [Module.Finite A M]
    (I J : Ideal A) (s d : ℤ) (hd : 0 ≤ d)
    (omega : DerivedCategory (ModuleCat.{u} A))
    (H : StabilizationHypotheses (M := M) I J s d omega) :
    ∃ p : Ideal A × ℕ, IsStabilizingData (M := M) I J s p

Tag 0EFJ, a lemma

Tag 0EFJ in the Stacks Project.

Stacks.Algebraization.finite_localCohomologyModule_stabilizingIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/StabilizationFiniteness.lean, line 183. The attribute's comment: “H^i_{J₀}(M) is a finite A-module for i ≤ s, given the annihilation clause of 0EFI”.

Stacks 0EFJ. Under hypothesis (2') the local cohomology of M supported in the stabilizing ideal J₀ of Stacks 0EFI is a finite A-module in every degree i ≤ s.

The annihilation of H^i_{J₀}(M) by a power of J₀ I for i ≤ s is carried as a hypothesis here; it is the clause Stacks.Algebraization.IsStabilizingData.pow_mul_le_annihilator of the conclusion of Stacks 0EFI. For the form of Stacks 0EFJ in which it is proved rather than assumed, see Stacks.Algebraization.finite_localCohomologyModule_stabilizingIdeal_of_nonneg.

public theorem finite_localCohomologyModule_stabilizingIdeal
    (h2 : DepthAddDimGtOnZeroLocus (M := M) I J s) (hs : 0 ≤ s)
    (hann : ∃ n : ℕ, ∀ i : ℤ, i ≤ s →
      ((stabilizingIdeal I J s d omega H * I) ^ n : Ideal A) ≤ Module.annihilator A
        (localCohomologyModule A (stabilizingIdeal I J s d omega H)
          (Ideal.fg_of_isNoetherianRing (stabilizingIdeal I J s d omega H))
          (ModuleCat.of A M) i))
    (i : ℤ) (hi : i ≤ s) :
    Module.Finite A
      (localCohomologyModule A (stabilizingIdeal I J s d omega H)
        (Ideal.fg_of_isNoetherianRing (stabilizingIdeal I J s d omega H))
        (ModuleCat.of A M) i)

Stacks.Algebraization.finite_localCohomologyModule_stabilizingIdeal_of_nonneg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/StabilizationFiniteness.lean, line 227. The attribute's comment: “H^i_{J₀}(M) is a finite A-module for i ≤ s, for 0 ≤ d”.

Stacks 0EFJ. Under hypotheses (1), (3), (4) of Stacks 0EFI together with hypothesis (2') in place of its empty hypothesis (2), the local cohomology of M supported in the stabilizing ideal J₀ of Stacks 0EFI is a finite A-module in every degree i ≤ s.

Nothing is assumed about H^i_{J₀}(M): the annihilation of those modules by a power of J₀ I for i ≤ s, which the source takes from Stacks 0EFI, is proved here from Stacks.Algebraization.exists_isStabilizingData, the existence statement of that lemma. The only hypothesis beyond those of the source is 0 ≤ d, which Stacks 0EFI needs and which the source uses silently when it reads depth + dim > d + s as depth + dim > s; see the module documentation. In particular 0 ≤ s is not assumed: in degrees i ≤ s < 0 local cohomology vanishes, so the statement is free there.

public theorem finite_localCohomologyModule_stabilizingIdeal_of_nonneg
    (h2 : DepthAddDimGtOnZeroLocus (M := M) I J s) (hd : 0 ≤ d)
    (i : ℤ) (hi : i ≤ s) :
    Module.Finite A
      (localCohomologyModule A (stabilizingIdeal I J s d omega H)
        (Ideal.fg_of_isNoetherianRing (stabilizingIdeal I J s d omega H))
        (ModuleCat.of A M) i)

Stacks.Algebraization.IsStabilizingData.finite_localCohomologyModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/StabilizationFinitenessGeneral.lean, line 82. The attribute's comment: “H^i_{J₀}(M) is a finite A-module for i ≤ s, for every ideal J₀ with the conclusions of 0EFI”.

Stacks 0EFJ. Let A be a Noetherian ring with a dualizing complex omega, let I, J be ideals, M a finite A-module and s an integer, and assume hypothesis (2'): for 𝔭 ∈ V(I) outside V(J) ∩ V(I), depth(M_𝔭) + dim((A/𝔭)_𝔮) > s for every 𝔮 ∈ V(𝔭) ∩ V(J) ∩ V(I). Then for every ideal J₀ with the conclusion of Stacks 0EFI — J₀ ⊆ J, V(J₀) ∩ V(I) = V(J) ∩ V(I), stability of H^i_{J'}(M) for i ≤ s under further shrinking J' ⊆ J₀ with the same trace on V(I), and annihilation of these modules by (J₀ I) ^ n — the module H^i_{J₀}(M) is finite for every i ≤ s.

Hypotheses (3) and (4) of Stacks 0EFI are not needed here: they enter only in producing J₀. No pair (J₀, n) need exist when d < 0, where Stacks 0EFI fails; there the statement is vacuous.

public theorem IsStabilizingData.finite_localCohomologyModule {I J J₀ : Ideal A} {s : ℤ}
    {n : ℕ} (hJ₀ : IsStabilizingData (M := M) I J s (J₀, n))
    (omega : letI := HasDerivedCategory.standard (ModuleCat.{u} A)
      DerivedCategory (ModuleCat.{u} A))
    (homega : letI := HasDerivedCategory.standard (ModuleCat.{u} A)
      Dualizing.IsDualizingComplex (A := A) (K := omega))
    (h2 : DepthAddDimGtOnZeroLocus (M := M) I J s) (i : ℤ) (hi : i ≤ s) :
    Module.Finite A
      (localCohomologyModule A J₀ J₀.fg_of_isNoetherianRing (ModuleCat.of A M) i)

Tag 0EFK, a lemma

Tag 0EFK in the Stacks Project.

Stacks.Algebraization.isIso_homologyMap_localCohomologyComparison_stabilizingIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/StabilizationDepthCollapse.lean, line 290. The attribute's comment: “H^i_{J₀}(M) = H^i_J(M) for i ≤ s”.

Under hypothesis (6) of Stacks 0EFK the local cohomology of M supported in the stabilizing ideal J₀ of Stacks 0EFI agrees with the local cohomology supported in J in all degrees i ≤ s.

public theorem isIso_homologyMap_localCohomologyComparison_stabilizingIdeal
    (h6 : DepthGtOnAssociatedSubset (M := M) I J s) (i : ℤ) (hi : i ≤ s) :
    IsIso ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).map
      (localCohomologyComparison A J (stabilizingIdeal I J s d omega H)
        (Ideal.fg_of_isNoetherianRing J)
        (Ideal.fg_of_isNoetherianRing (stabilizingIdeal I J s d omega H))
        (stabilizingIdeal_le I J s d omega H)
        ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj (ModuleCat.of A M))))

Stacks.Algebraization.isIso_homologyMap_localCohomologyComparison_sup, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/StabilizationDepthCollapse.lean, line 315. The attribute's comment: “H^i_J(M) = H^i_{J + I}(M) for i ≤ s”.

Under hypothesis (6) of Stacks 0EFK the local cohomology of M supported in J agrees with the local cohomology supported in J + I in all degrees i ≤ s.

public theorem isIso_homologyMap_localCohomologyComparison_sup
    (h6 : DepthGtOnAssociatedSubset (M := M) I J s) (i : ℤ) (hi : i ≤ s) :
    IsIso ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).map
      (localCohomologyComparison A (J ⊔ I) J
        (Ideal.fg_of_isNoetherianRing (J ⊔ I)) (Ideal.fg_of_isNoetherianRing J) le_sup_left
        ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj (ModuleCat.of A M))))

Stacks.Algebraization.exists_pow_le_annihilator_localCohomologyModule_sup, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/StabilizationDepthCollapse.lean, line 330. The attribute's comment: “H^i_{J + I}(M) is annihilated by a power of I for i ≤ s”.

Under hypothesis (6) of Stacks 0EFK a single power of I annihilates H^i_{J + I}(M) in every degree i ≤ s.

public theorem exists_pow_le_annihilator_localCohomologyModule_sup
    (h6 : DepthGtOnAssociatedSubset (M := M) I J s) (hs : 0 ≤ s) (hd : 0 ≤ d) :
    ∃ n : ℕ, ∀ i : ℤ, i ≤ s →
      I ^ n ≤ Module.annihilator A
        (localCohomologyModule A (J ⊔ I) (Ideal.fg_of_isNoetherianRing (J ⊔ I))
          (ModuleCat.of A M) i)

Stacks.Algebraization.exists_pow_le_annihilator_localCohomologyModule_stabilizingIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/StabilizationDepthCollapse.lean, line 384. The attribute's comment: “H^i_{J₀}(M) is annihilated by a power of I for i ≤ s”.

Under hypothesis (6) of Stacks 0EFK a single power of I annihilates the local cohomology of M supported in the stabilizing ideal J₀ of Stacks 0EFI, in every degree i ≤ s.

public theorem exists_pow_le_annihilator_localCohomologyModule_stabilizingIdeal
    (h6 : DepthGtOnAssociatedSubset (M := M) I J s) (hs : 0 ≤ s) (hd : 0 ≤ d) :
    ∃ n : ℕ, ∀ i : ℤ, i ≤ s →
      I ^ n ≤ Module.annihilator A
        (localCohomologyModule A (stabilizingIdeal I J s d omega H)
          (Ideal.fg_of_isNoetherianRing (stabilizingIdeal I J s d omega H))
          (ModuleCat.of A M) i)

Tag 0EFL, a lemma

Tag 0EFL in the Stacks Project.

Stacks.Algebraization.isAlgebraizationIdeal_of_zeroLocus_inter_eq_empty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationComparison.lean, line 936. The attribute's comment: “existence of J₀ in the case V(J) ∩ V(I) = ∅, which the δmax and δmin fields of AlgebraizationHypotheses exclude and the source does not: the source's condition (5), the only one naming δ, is guarded by V(𝔭) ∩ V(J) ∩ V(I) ≠ ∅ and so is vacuous here. J₀ = J serves, for every s and on I-adic completeness alone. With exists_isAlgebraizationIdeal, which is the nonempty case, this covers the tag”.

Stacks 0EFL when V(J) ∩ V(I) is empty. For an I-adically complete Noetherian ring and ideals with V(J) ∩ V(I) = ∅, the ideal J itself has the property asserted of J₀, in every degree and for every finite module.

This is the case of the source that the extreme values δmax and δmin of Stacks.Algebraization.AlgebraizationHypotheses exclude, and it is not vacuous: J = A is an instance. The source's conditions hold in it with no constraint beyond (1), because its condition (5), the only one mentioning δ, is guarded by V(𝔭) ∩ V(J) ∩ V(I) ≠ ∅.

Completeness is what makes the case true. Since I lies in the Jacobson radical of an I-adically complete ring, every prime has a specialization in V(I), so an admissible shrinking J' has V(J') ∩ V(I) = ∅ only if V(J') is empty — that is, only for J' = A. Then RΓ_{J'}(M) is supported on the empty set, hence already derived I-complete, so the unit of derived completion is invertible at it; both sides are in fact zero.

public theorem isAlgebraizationIdeal_of_zeroLocus_inter_eq_empty
    {M : Type u} [AddCommGroup M] [Module A M] [Module.Finite A M]
    (I J : Ideal A) (s : ℤ) (hcomplete : IsAdicComplete I A)
    (hJI : PrimeSpectrum.zeroLocus (J : Set A) ∩ PrimeSpectrum.zeroLocus (I : Set A) = ∅) :
    IsAlgebraizationIdeal (M := M) I J s J

Stacks.Algebraization.exists_isAlgebraizationIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationComparison.lean, line 979. The attribute's comment: “existence of J₀ in the case V(J) ∩ V(I) ≠ ∅, which is what the δmax and δmin fields of AlgebraizationHypotheses presuppose; the empty case, where the source's condition (5) is vacuous, is isAlgebraizationIdeal_of_zeroLocus_inter_eq_empty, and the two together are the tag. The dualizing complex is taken in the ring's own module universe”.

Stacks 0EFL. Let I and J be ideals of a Noetherian ring A, let M be a finite A-module and let s and d be integers. Under conditions (1), (3), (4) and (5) of the source there is an ideal J₀ ⊆ J with V(J₀) ∩ V(I) = V(J) ∩ V(I) such that for every further ideal J' ⊆ J₀ with the same intersection with V(I) the canonical map

RΓ_{J'}(M) ⟶ RΓ_J(M)^∧

is an isomorphism on cohomology in all degrees ≤ s.

The proof is the source's induction on s; the arrow is Stacks.Algebraization.localCohomologyToCompletedLocalCohomology, the composite of the unit of derived I-adic completion with the identification RΓ_{J'}(M)^∧ ≅ RΓ_J(M)^∧ of the opening paragraph of the source, and the latter is invertible, so the assertion is exactly that the unit is invertible on cohomology in degrees ≤ s. The case s < 0, where both sides vanish in the relevant degrees and J₀ = J serves, is Stacks.Algebraization.isAlgebraizationIdeal_of_lt_zero.

public theorem exists_isAlgebraizationIdeal
    {M : Type u} [AddCommGroup M] [Module A M] [Module.Finite A M]
    (I J : Ideal A) (s d : ℤ) (omega : DerivedCategory (ModuleCat.{u} A))
    (δ : PrimeSpectrum A → ℤ) (δmax δmin : ℤ)
    (H : AlgebraizationHypotheses (M := M) I J s d omega δ δmax δmin) :
    ∃ J₀ : Ideal A, IsAlgebraizationIdeal (M := M) I J s J₀

Stacks.Algebraization.exists_isAlgebraizationIdeal_of_sourceHypotheses, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationComparisonSource.lean, line 73.

Stacks 0EFL. Let I, J be ideals of a Noetherian ring A, let M be a finite A-module, let s, d be integers, and let T = {𝔭 : V(𝔭) ∩ V(I) ⊆ V(J) ∩ V(I)}. Assume 1. A is I-adically complete and has a dualizing complex; 2. (no condition at primes of V(I)); 3. cd(A, I) ≤ d; 4. if 𝔭 ∉ V(I), 𝔭 ∉ T, then depth(M_𝔭) ≥ s or depth(M_𝔭) + dim((A/𝔭)_𝔮) > d + s for all 𝔮 ∈ V(𝔭) ∩ V(J) ∩ V(I); 5. for a dimension function δ, with δmax and δmin the maximum and the minimum of δ on V(J) ∩ V(I): if 𝔭 ∉ V(I), 𝔭 ∉ T, V(𝔭) ∩ V(J) ∩ V(I) ≠ ∅ and depth(M_𝔭) < s, then (a) dim(Supp(M_𝔭)) < s + 2, or (b) δ(𝔭) > d + δmax - 1, or (c) depth(M_𝔭) + dim((A/𝔭)_𝔮) > d + s + δmax - δmin - 2 for all 𝔮 ∈ V(𝔭) ∩ V(J) ∩ V(I).

Then there is an ideal J₀ ⊆ J with V(J₀) ∩ V(I) = V(J) ∩ V(I) such that for every J' ⊆ J₀ with V(J') ∩ V(I) = V(J) ∩ V(I) the map RΓ_{J'}(M) → RΓ_J(M)^∧ is an isomorphism on cohomology in degrees ≤ s (Stacks.Algebraization.IsAlgebraizationIdeal).

The proof is by cases. If V(J) ∩ V(I) is empty, J₀ = J serves (isAlgebraizationIdeal_of_zeroLocus_inter_eq_empty). Otherwise the extreme values of δ on V(J) ∩ V(I) exist (exists_isGreatest_isLeast_image_dimensionFunction, using that A has finite Krull dimension by Stacks 0A80), and exists_isAlgebraizationIdeal applies.

public theorem exists_isAlgebraizationIdeal_of_sourceHypotheses (I J : Ideal A) (s d : ℤ)
    (hcomplete : IsAdicComplete I A)
    (hdual : ∃ ω : DerivedCategory (ModuleCat.{u} A), Dualizing.IsDualizingComplex ω)
    (hcd : Stacks.LocalCohomology.cohomologicalDimension A I I.fg_of_isNoetherianRing ≤ d)
    (h4 : ∀ p : PrimeSpectrum A,
      p ∉ PrimeSpectrum.zeroLocus (I : Set A) →
      p ∉ associatedSubset I J →
      ((enatToEInt
          (Module.depth (Localization.AtPrime p.asIdeal)
            (maximalIdeal (Localization.AtPrime p.asIdeal))
            (LocalizedModule p.asIdeal.primeCompl M)) ≥ (s : EInt)) ∨
        (∀ q : PrimeSpectrum A,
          q ∈ (PrimeSpectrum.zeroLocus (p.asIdeal : Set A) ∩
            PrimeSpectrum.zeroLocus (J : Set A)) ∩
            PrimeSpectrum.zeroLocus (I : Set A) →
          enatToEInt
              (Module.depth (Localization.AtPrime p.asIdeal)
                (maximalIdeal (Localization.AtPrime p.asIdeal))
                (LocalizedModule p.asIdeal.primeCompl M)) +
              krullDimToEInt
                (ringKrullDim ((Localization.AtPrime q.asIdeal) ⧸
                  p.asIdeal.map (algebraMap A (Localization.AtPrime q.asIdeal)))) >
            ((d + s : ℤ) : EInt))))
    (h5 : ∃ δ : TopologicalSpace.DimensionFunction (PrimeSpectrum A),
      ∀ δmax δmin : ℤ,
      IsGreatest (δ.toFun '' (PrimeSpectrum.zeroLocus (J : Set A) ∩
        PrimeSpectrum.zeroLocus (I : Set A))) δmax →
      IsLeast (δ.toFun '' (PrimeSpectrum.zeroLocus (J : Set A) ∩
        PrimeSpectrum.zeroLocus (I : Set A))) δmin →
      ∀ p : PrimeSpectrum A,
      p ∉ PrimeSpectrum.zeroLocus (I : Set A) →
      p ∉ associatedSubset I J →
      ((PrimeSpectrum.zeroLocus (p.asIdeal : Set A) ∩
        PrimeSpectrum.zeroLocus (J : Set A)) ∩
        PrimeSpectrum.zeroLocus (I : Set A)).Nonempty →
      enatToEInt
          (Module.depth (Localization.AtPrime p.asIdeal)
            (maximalIdeal (Localization.AtPrime p.asIdeal))
            (LocalizedModule p.asIdeal.primeCompl M)) < (s : EInt) →
      (krullDimToEInt (Module.supportDim (Localization.AtPrime p.asIdeal)
            (LocalizedModule p.asIdeal.primeCompl M)) < ((s + 2 : ℤ) : EInt) ∨
        (d + δmax - 1 < δ.toFun p) ∨
        (∀ q : PrimeSpectrum A,
          q ∈ (PrimeSpectrum.zeroLocus (p.asIdeal : Set A) ∩
            PrimeSpectrum.zeroLocus (J : Set A)) ∩
            PrimeSpectrum.zeroLocus (I : Set A) →
          enatToEInt
              (Module.depth (Localization.AtPrime p.asIdeal)
                (maximalIdeal (Localization.AtPrime p.asIdeal))
                (LocalizedModule p.asIdeal.primeCompl M)) +
              krullDimToEInt
                (ringKrullDim ((Localization.AtPrime q.asIdeal) ⧸
                  p.asIdeal.map (algebraMap A (Localization.AtPrime q.asIdeal)))) >
            ((d + s + δmax - δmin - 2 : ℤ) : EInt)))) :
    ∃ J₀ : Ideal A, IsAlgebraizationIdeal (M := M) I J s J₀

Tag 0EFM, an example

Tag 0EFM in the Stacks Project.

Stacks.Algebraization.MittagLefflerFailure.pow_mul_pow_mem_modIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationMittagLefflerFailure.lean, line 314. The attribute's comment: “the containment (yⁿ) ⊆ the image: xⁿyⁿ = pⁿ in M”.

xⁿyⁿ = pⁿ in M, so xⁿyⁿ lies in (xy - p, pⁿ).

theorem pow_mul_pow_mem_modIdeal (n : ℕ) : varX p ^ n * varY p ^ n ∈ modIdeal p n

Stacks.Algebraization.MittagLefflerFailure.mem_span_of_pow_mul_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationMittagLefflerFailure.lean, line 401. The attribute's comment: “the containment image ⊆ (yⁿ): an x-power-torsion element mod (xy - p, pⁿ) lies in (p, xy, yⁿ)”.

The x-power-torsion of A/(xy - p, pⁿ⁺¹) is carried by (xy - p, yⁿ⁺¹). If x^k f ∈ (xy - p, pⁿ⁺¹) then f ∈ (p, xy, yⁿ⁺¹).

theorem mem_span_of_pow_mul_mem (n k : ℕ) (f : MvPowerSeries (Fin 2) ℤ_[p])
    (hf : varX p ^ k * f ∈ modIdeal p (n + 1)) :
    f ∈ Ideal.span {((p : ℕ) : MvPowerSeries (Fin 2) ℤ_[p]), varX p * varY p,
      varY p ^ (n + 1)}

Stacks.Algebraization.MittagLefflerFailure.imageSections_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationMittagLefflerFailure.lean, line 458. The attribute's comment: “the example: the image of H⁰_J(M/pⁿM) ⟶ H⁰_J(M/pM) is the ideal generated by yⁿ in M/pM = A/(p, xy), for A = ℤ_p[[x,y]], I = (p), J = (p, x) and M = A/(xy - p)”.

Stacks 0EFM. The image of H⁰_J(M/pⁿM) → H⁰_J(M/pM) is the ideal generated by yⁿ in M/pM = A/(p, xy), for A = ℤ_p[[x, y]], I = (p), J = (p, x) and M = A/(xy - p).

theorem imageSections_eq (n : ℕ) :
    imageSections p n = Submodule.restrictScalars (MvPowerSeries (Fin 2) ℤ_[p])
      (Ideal.span {Ideal.Quotient.mk (modIdeal p 1) (varY p ^ (n + 1))})

Stacks.Algebraization.MittagLefflerFailure.not_mittagLeffler, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationMittagLefflerFailure.lean, line 514. The attribute's comment: “the point of the example: the inverse system H⁰_J(M/pⁿM) does NOT satisfy the Mittag-Leffler condition, so the hypothesis of Lemma 0EFL cannot be dropped”.

The inverse system n ↦ H⁰_J(M/pⁿM) is not Mittag-Leffler. The images of its transition maps into H⁰_J(M/pM) never stabilise.

theorem not_mittagLeffler :
    ¬ ∃ m : ℕ, ∀ k, m ≤ k → imageSections p k = imageSections p m

Sources

• Section 52.8, Tag 0EFF
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Algebraization.associatedSubset · Stacks.Algebraization.exists_notMem_mem_annihilator_homology_derivedCompletion_localCohomology · Stacks.Algebraization.prod_smul_id_derivedHom_homology_eq_zero · Stacks.Algebraization.exists_notMem_mem_annihilator_homology_derivedHom · Stacks.LocalCohomology.isLE_localCohomologyDerived_single_of_cohomologicalDimension_le · Stacks.LocalCohomology.isGE_localCohomologyDerived_single · Stacks.LocalCohomology.exists_notMem_mem_annihilator_localCohomologyWithSupportIn_sup · Stacks.LocalCohomology.exists_notMem_mem_annihilator_localCohomologyModule_sup

Section52.9 Algebraization of local cohomology, II#

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

Tag 0DXK, a lemma

Tag 0DXK in the Stacks Project.

Stacks.Algebraization.exists_notMem_mem_annihilator_homology_derivedCompletion_localCohomology_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/AnnihilatorCompletedLocalCohomology.lean, line 396. The attribute's comment: “the full statement: an element outside p annihilating the cohomology of the derived I-adic completion of RΓ_{V(𝔪)}(M) in every degree ≤ s”.

Let (A, 𝔪) be a Noetherian local ring with a dualizing complex, let I be an ideal with cd(A, I) ≤ d, let M be a finite A-module and let p be a prime with depth_{A_p}(M_p) + dim(A/p) > d + s. Then some f ∈ A outside p annihilates the degree-i cohomology of the derived I-adic completion of RΓ_{V(𝔪)}(M) for every i ≤ s.

theorem exists_notMem_mem_annihilator_homology_derivedCompletion_localCohomology_maximalIdeal
    (A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    (M : Type u) [AddCommGroup M] [Module A M] [Module.Finite A M]
    (I : Ideal A) (p : PrimeSpectrum A) (s d : ℤ)
    (omega : DerivedCategory (ModuleCat.{u} A))
    (homega : Dualizing.IsDualizingComplex (A := A) (K := omega))
    (hcd : Stacks.LocalCohomology.cohomologicalDimension A I I.fg_of_isNoetherianRing ≤ d)
    (hdepth : enatToEInt
          (Module.depth (Localization.AtPrime p.asIdeal)
            (maximalIdeal (Localization.AtPrime p.asIdeal))
            (LocalizedModule p.asIdeal.primeCompl M)) +
        krullDimToEInt (ringKrullDim (A ⧸ p.asIdeal)) > ((d + s : ℤ) : EInt))
    {r : ℕ} (gen : Fin r → A) (hgen : Ideal.span (Set.range gen) = I) :
    ∃ f : A, f ∉ p.asIdeal ∧ ∀ i : ℤ, i ≤ s →
      f ∈ Module.annihilator A
        ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).obj
          ((DerivedCompletion.derivedCompletionFunctor A gen).obj
            ((Dualizing.derivedPowerTorsionProperty A (maximalIdeal A)
                (maximalIdeal A).fg_of_isNoetherianRing).ι.obj
              ((Dualizing.localCohomologyFunctor.{u, u} A (maximalIdeal A)
                  (maximalIdeal A).fg_of_isNoetherianRing).obj
                ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
                  (ModuleCat.of A M))))))

Tag 0DXM, a lemma

Tag 0DXM in the Stacks Project.

Stacks.Algebraization.localStabilizationHypotheses_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/StabilizationMaximalIdeal.lean, line 200. The attribute's comment: “the hypotheses, identified with those of Stacks 0EFI at J = 𝔪”.

Stacks 0DXM. Hypotheses (1)–(4) of the lemma are exactly the properness of I together with the hypotheses of Stacks 0EFI for J = 𝔪.

This biconditional is the content of the source's proof, which reads "this is a special case of Lemma 0EFI": at J = 𝔪 the set V(𝔭) ∩ V(𝔪) ∩ V(I) of Stacks 0EFI is the single point 𝔪, where its relative dimension dim((A/𝔭)_𝔮) is dim(A/𝔭).

public theorem localStabilizationHypotheses_iff (I : Ideal A) (s d : ℤ)
    (omega : DerivedCategory (ModuleCat.{w} A)) :
    LocalStabilizationHypotheses (M := M) I s d omega ↔
      (I ≠ ⊤ ∧ StabilizationHypotheses (M := M) I (maximalIdeal A) s d omega)

Stacks.Algebraization.zeroLocus_stabilizingIdeal_maximalIdeal_inter, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/StabilizationMaximalIdeal.lean, line 250. The attribute's comment: “the ideal J₀, with V(J₀) ∩ V(I) = {𝔪}”.

Stacks 0DXM. The ideal that Stacks 0EFI selects at J = 𝔪 meets V(I) in the closed point only, which is the first clause of the conclusion of the lemma.

public theorem zeroLocus_stabilizingIdeal_maximalIdeal_inter (I : Ideal A) (s d : ℤ)
    (omega : DerivedCategory (ModuleCat.{w} A))
    (H : LocalStabilizationHypotheses (M := M) I s d omega) :
    PrimeSpectrum.zeroLocus
          ((stabilizingIdeal I (maximalIdeal A) s d omega
            H.toStabilizationHypotheses : Ideal A) : Set A) ∩
        PrimeSpectrum.zeroLocus (I : Set A) = {closedPoint A}

Stacks.Algebraization.exists_stabilization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/StabilizationMaximalIdealExistence.lean, line 315. The attribute's comment: “the conclusion: an ideal J₀ and one exponent n such that every J ⊆ J₀ with V(J) ∩ V(I) = {𝔪} has RΓ_{J₀}(M) → RΓ_J(M) an isomorphism on cohomology in degrees ≤ s and (J₀ I) ^ n annihilating those modules”.

Stacks 0DXM. Let (A, 𝔪) be a Noetherian local ring, let I ⊂ A be an ideal, let M be a finite A-module and let s and d be integers. Under hypotheses (1)–(4) of the lemma there is an ideal J₀ with V(J₀) ∩ V(I) = {𝔪} such that for every ideal J ⊆ J₀ with V(J) ∩ V(I) = {𝔪} the comparison RΓ_{J₀}(M) → RΓ_J(M) induces an isomorphism in cohomology in degrees ≤ s, and one power of J₀ I annihilates all of those cohomology modules.

This is Stacks.Algebraization.exists_stabilization_of_exists with its hypothesis discharged by Stacks.Algebraization.exists_isStabilizingData_maximalIdeal. Taking J = J₀ gives the annihilation of H^i_{J₀}(M) by a power of J₀ I.

public theorem exists_stabilization (I : Ideal A) (s d : ℤ)
    (omega : DerivedCategory (ModuleCat.{u} A))
    (H : LocalStabilizationHypotheses (M := M) I s d omega) :
    ∃ J₀ : Ideal A, ∃ n : ℕ,
      PrimeSpectrum.zeroLocus (J₀ : Set A) ∩ PrimeSpectrum.zeroLocus (I : Set A) =
          {closedPoint A} ∧
        ∀ J : Ideal A, ∀ hJ : J ≤ J₀,
          PrimeSpectrum.zeroLocus (J : Set A) ∩ PrimeSpectrum.zeroLocus (I : Set A) =
            {closedPoint A} →
          ∀ i : ℤ, i ≤ s →
            IsIso ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).map
                (localCohomologyComparison A J₀ J J₀.fg_of_isNoetherianRing
                  J.fg_of_isNoetherianRing hJ
                  ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
                    (ModuleCat.of A M)))) ∧
              (J₀ * I) ^ n ≤ Module.annihilator A
                ↥((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).obj
                  ((Dualizing.localCohomologyFunctor A J J.fg_of_isNoetherianRing).obj
                    ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
                      (ModuleCat.of A M))).obj)

Tag 0DXN, a lemma

Tag 0DXN in the Stacks Project.

Stacks.Algebraization.exists_stabilization_finite_localCohomologyModule_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/LocalStabilizationFiniteness.lean, line 171.

Stacks 0DXN. Let (A, 𝔪) be a Noetherian local ring, I ⊂ A an ideal, M a finite A-module and s, d integers. Assume (1) A has a dualizing complex, (2') every prime 𝔭 ∈ V(I) other than 𝔪 has depth(M_𝔭) + dim(A/𝔭) > s, (3) every prime 𝔭 ∉ V(I) with V(𝔭) ∩ V(I) = {𝔪} has dim(A/𝔭) ≤ d, and (4) every prime 𝔭 ∉ V(I) with V(𝔭) ∩ V(I) ≠ {𝔪} has depth(M_𝔭) ≥ s or depth(M_𝔭) + dim(A/𝔭) > d + s. Then there is an ideal J₀ with V(J₀) ∩ V(I) = {𝔪} such that for every J ⊆ J₀ with V(J) ∩ V(I) = {𝔪} the map RΓ_{J₀}(M) → RΓ_J(M) is an isomorphism on cohomology in degrees ≤ s and one power of J₀ I annihilates those cohomology modules (the conclusion of Stacks 0DXM), and moreover H^i_{J₀}(M) is a finite A-module for every i ≤ s.

Hypotheses (1), (3), (4) and the source's standing assumption I ≠ A (without which V(J₀) ∩ V(I) = {𝔪} is unattainable) are LocalStabilizationHypotheses; (2') is DepthAddDimGtAtMaximalIdeal. The integers s and d are arbitrary. For s < 0 the finiteness is the vanishing of local cohomology in negative degrees; for d < 0 the hypotheses force I to be nilpotent (LocalStabilizationHypotheses.mem_zeroLocus_of_neg).

public theorem exists_stabilization_finite_localCohomologyModule_maximalIdeal
    (I : Ideal A) (s d : ℤ) (omega : DerivedCategory (ModuleCat.{u} A))
    (H : LocalStabilizationHypotheses (M := M) I s d omega)
    (h2 : DepthAddDimGtAtMaximalIdeal (M := M) I s) :
    ∃ J₀ : Ideal A, ∃ n : ℕ,
      PrimeSpectrum.zeroLocus (J₀ : Set A) ∩ PrimeSpectrum.zeroLocus (I : Set A) =
          {closedPoint A} ∧
        (∀ J : Ideal A, ∀ hJ : J ≤ J₀,
          PrimeSpectrum.zeroLocus (J : Set A) ∩ PrimeSpectrum.zeroLocus (I : Set A) =
            {closedPoint A} →
          ∀ i : ℤ, i ≤ s →
            IsIso ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).map
                (localCohomologyComparison A J₀ J J₀.fg_of_isNoetherianRing
                  J.fg_of_isNoetherianRing hJ
                  ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
                    (ModuleCat.of A M)))) ∧
              (J₀ * I) ^ n ≤ Module.annihilator A
                ↥((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).obj
                  ((Dualizing.localCohomologyFunctor A J J.fg_of_isNoetherianRing).obj
                    ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
                      (ModuleCat.of A M))).obj)) ∧
        ∀ i : ℤ, i ≤ s →
          Module.Finite A
            (localCohomologyModule A J₀ J₀.fg_of_isNoetherianRing (ModuleCat.of A M) i)

Stacks.Algebraization.depthAddDimGtOnZeroLocus_maximalIdeal_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/StabilizationMaximalIdealFiniteness.lean, line 117. The attribute's comment: “hypothesis (2') is hypothesis (2') of Stacks 0EFJ at J = 𝔪, for every ideal I”.

Stacks 0DXN. Hypothesis (2') of the lemma is hypothesis (2') of Stacks 0EFJ at J = 𝔪, for every ideal I.

This biconditional is the content of the source's proof, which reads "this is a special case of Lemma 0EFJ": at J = 𝔪 the set V(𝔪) ∩ V(I) is the single point 𝔪, so a prime of V(I) lies outside it exactly when it differs from 𝔪, and the only specialization of it available in V(𝔪) ∩ V(I) is 𝔪 itself, where dim((A/𝔭)_𝔪) is dim(A/𝔭).

That reading of V(𝔪) ∩ V(I) uses 𝔪 ∈ V(I), the source's standing assumption that I is proper. It is not needed for the equivalence itself: for I = A the locus V(I) is empty, so both conditions quantify over nothing.

public theorem depthAddDimGtOnZeroLocus_maximalIdeal_iff {I : Ideal A} (s : ℤ) :
    DepthAddDimGtOnZeroLocus (M := M) I (maximalIdeal A) s ↔
      DepthAddDimGtAtMaximalIdeal (M := M) I s

Stacks.Algebraization.finite_localCohomologyModule_stabilizingIdeal_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/StabilizationMaximalIdealFiniteness.lean, line 153. The attribute's comment: “H^i_{J₀}(M) is a finite A-module for i ≤ s, given the annihilation clause of Stacks 0DXM and 0 ≤ s”.

Stacks 0DXN. Under hypotheses (1), (3), (4) of Stacks 0DXM together with hypothesis (2') in place of its empty hypothesis (2), the local cohomology of M supported in the ideal J₀ that Stacks 0DXM selects is a finite A-module in every degree i ≤ s.

This is Stacks 0EFJ at J = 𝔪. The annihilation of H^i_{J₀}(M) by a power of J₀ I for i ≤ s is a clause of the conclusion of Stacks 0DXM and is carried as a hypothesis, as it is in Stacks 0EFJ.

public theorem finite_localCohomologyModule_stabilizingIdeal_maximalIdeal
    (h2 : DepthAddDimGtAtMaximalIdeal (M := M) I s) (hs : 0 ≤ s)
    (hann : ∃ n : ℕ, ∀ j : ℤ, j ≤ s →
      ((stabilizingIdeal I (maximalIdeal A) s d omega H.toStabilizationHypotheses * I) ^ n
        : Ideal A) ≤ Module.annihilator A
        (localCohomologyModule A
          (stabilizingIdeal I (maximalIdeal A) s d omega H.toStabilizationHypotheses)
          (Ideal.fg_of_isNoetherianRing
            (stabilizingIdeal I (maximalIdeal A) s d omega H.toStabilizationHypotheses))
          (ModuleCat.of A M) j))
    (i : ℤ) (hi : i ≤ s) :
    Module.Finite A
      (localCohomologyModule A
        (stabilizingIdeal I (maximalIdeal A) s d omega H.toStabilizationHypotheses)
        (Ideal.fg_of_isNoetherianRing
          (stabilizingIdeal I (maximalIdeal A) s d omega H.toStabilizationHypotheses))
        (ModuleCat.of A M) i)

Stacks.Algebraization.finite_localCohomologyModule_stabilizingIdeal_maximalIdeal_of_exists, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/StabilizationMaximalIdealFiniteness.lean, line 181. The attribute's comment: “H^i_{J₀}(M) is a finite A-module for i ≤ s, for 0 ≤ s and 0 ≤ d”.

Stacks 0DXN. The same finiteness, with the annihilation clause of Stacks 0DXM proved from Stacks 0EFI.

The hypotheses are then exactly those of Stacks 0DXM with its empty hypothesis (2) replaced by (2'), together with 0 ≤ s and the hypothesis 0 ≤ d that Stacks 0EFI needs and the source of Stacks 0DXM uses silently; see the module documentation.

public theorem finite_localCohomologyModule_stabilizingIdeal_maximalIdeal_of_exists
    (h2 : DepthAddDimGtAtMaximalIdeal (M := M) I s) (hs : 0 ≤ s) (hd : 0 ≤ d)
    (i : ℤ) (hi : i ≤ s) :
    Module.Finite A
      (localCohomologyModule A
        (stabilizingIdeal I (maximalIdeal A) s d omega H.toStabilizationHypotheses)
        (Ideal.fg_of_isNoetherianRing
          (stabilizingIdeal I (maximalIdeal A) s d omega H.toStabilizationHypotheses))
        (ModuleCat.of A M) i)

Tag 0EFQ, a lemma

Tag 0EFQ in the Stacks Project.

Stacks.Algebraization.isIso_homologyMap_localCohomologyComparison_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/StabilizationMaximalIdealCollapse.lean, line 203. The attribute's comment: “H^i_J(M) = H^i_𝔪(M) for i ≤ s, for every J with V(J) ∩ V(I) = {𝔪}”.

Under hypothesis (6) the local cohomology of M supported in any ideal J with V(J) ∩ V(I) = {𝔪} agrees with the local cohomology supported in 𝔪 in all degrees i ≤ s: H^i_J(M) = H^i_𝔪(M).

public theorem isIso_homologyMap_localCohomologyComparison_maximalIdeal
    (I J : Ideal A) (s : ℤ) (h6 : DepthGtAtMaximalIdeal (M := M) I s)
    (hJ : PrimeSpectrum.zeroLocus (J : Set A) ∩ PrimeSpectrum.zeroLocus (I : Set A) =
      {closedPoint A})
    (i : ℤ) (hi : i ≤ s) :
    IsIso ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).map
      (localCohomologyComparison A (maximalIdeal A) J
        (Ideal.fg_of_isNoetherianRing (maximalIdeal A)) (Ideal.fg_of_isNoetherianRing J)
        (le_maximalIdeal_of_zeroLocus_inter_eq_closedPoint hJ).1
        ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj (ModuleCat.of A M))))

Stacks.Algebraization.isIso_homologyMap_localCohomologyComparison_stabilizingIdeal_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/StabilizationMaximalIdealCollapse.lean, line 241. The attribute's comment: “H^i_{J₀}(M) = H^i_𝔪(M) for i ≤ s”.

Under hypothesis (6) the local cohomology of M supported in the ideal J₀ produced by Stacks 0DXM agrees with the local cohomology supported in 𝔪 in all degrees i ≤ s: H^i_{J₀}(M) = H^i_𝔪(M).

public theorem isIso_homologyMap_localCohomologyComparison_stabilizingIdeal_maximalIdeal
    (h6 : DepthGtAtMaximalIdeal (M := M) I s) (i : ℤ) (hi : i ≤ s) :
    IsIso ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).map
      (localCohomologyComparison A (maximalIdeal A)
        (stabilizingIdeal I (maximalIdeal A) s d omega H.toStabilizationHypotheses)
        (Ideal.fg_of_isNoetherianRing (maximalIdeal A))
        (Ideal.fg_of_isNoetherianRing
          (stabilizingIdeal I (maximalIdeal A) s d omega H.toStabilizationHypotheses))
        (stabilizingIdeal_le I (maximalIdeal A) s d omega H.toStabilizationHypotheses)
        ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj (ModuleCat.of A M))))

Stacks.Algebraization.isIso_homologyMap_localCohomologyComparison_stabilizingIdeal_of_depthGt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/StabilizationMaximalIdealCollapse.lean, line 260. The attribute's comment: “H^i_{J₀}(M) = H^i_J(M) for i ≤ s”.

Under hypothesis (6) the local cohomology of M supported in the ideal J₀ produced by Stacks 0DXM agrees with the local cohomology supported in any further ideal J ⊆ J₀ with V(J) ∩ V(I) = {𝔪}, in all degrees i ≤ s: H^i_{J₀}(M) = H^i_J(M).

public theorem isIso_homologyMap_localCohomologyComparison_stabilizingIdeal_of_depthGt
    (h6 : DepthGtAtMaximalIdeal (M := M) I s) (J : Ideal A)
    (hJle : J ≤ stabilizingIdeal I (maximalIdeal A) s d omega H.toStabilizationHypotheses)
    (hJ : PrimeSpectrum.zeroLocus (J : Set A) ∩ PrimeSpectrum.zeroLocus (I : Set A) =
      {closedPoint A})
    (i : ℤ) (hi : i ≤ s) :
    IsIso ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).map
      (localCohomologyComparison A
        (stabilizingIdeal I (maximalIdeal A) s d omega H.toStabilizationHypotheses) J
        (Ideal.fg_of_isNoetherianRing
          (stabilizingIdeal I (maximalIdeal A) s d omega H.toStabilizationHypotheses))
        (Ideal.fg_of_isNoetherianRing J) hJle
        ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj (ModuleCat.of A M))))

Stacks.Algebraization.exists_pow_le_annihilator_localCohomologyModule_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/StabilizationMaximalIdealCollapse.lean, line 282. The attribute's comment: “the annihilation assertion through Stacks 0EFK, in the numerical range 0 ≤ s and 0 ≤ d in which that lemma is stated”.

Under hypothesis (6), 0 ≤ s and 0 ≤ d, a single power of I annihilates H^i_J(M) in every degree i ≤ s, uniformly in every ideal J with V(J) ∩ V(I) = {𝔪}.

public theorem exists_pow_le_annihilator_localCohomologyModule_maximalIdeal
    (h6 : DepthGtAtMaximalIdeal (M := M) I s) (hs : 0 ≤ s) (hd : 0 ≤ d) :
    ∃ n : ℕ, ∀ J : Ideal A,
      PrimeSpectrum.zeroLocus (J : Set A) ∩ PrimeSpectrum.zeroLocus (I : Set A) =
        {closedPoint A} →
      ∀ i : ℤ, i ≤ s →
        I ^ n ≤ Module.annihilator A
          (localCohomologyModule A J (Ideal.fg_of_isNoetherianRing J)
            (ModuleCat.of A M) i)

Stacks.Algebraization.exists_pow_le_annihilator_localCohomologyModule_maximalIdeal_of_depthGt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/StabilizationMaximalIdealCollapse.lean, line 323. The attribute's comment: “the annihilation assertion: a power of I annihilates H^i_J(M) for i ≤ s, for every J with V(J) ∩ V(I) = {𝔪}, with no hypothesis beyond the tag's”.

Under hypothesis (6) a single power of I annihilates H^i_J(M) in every degree i ≤ s, uniformly in every ideal J with V(J) ∩ V(I) = {𝔪}; this includes J = 𝔪 and J = J₀, by zeroLocus_maximalIdeal_inter and zeroLocus_stabilizingIdeal_maximalIdeal_inter.

public theorem exists_pow_le_annihilator_localCohomologyModule_maximalIdeal_of_depthGt
    (h6 : DepthGtAtMaximalIdeal (M := M) I s) :
    ∃ n : ℕ, ∀ J : Ideal A,
      PrimeSpectrum.zeroLocus (J : Set A) ∩ PrimeSpectrum.zeroLocus (I : Set A) =
        {closedPoint A} →
      ∀ i : ℤ, i ≤ s →
        I ^ n ≤ Module.annihilator A
          (localCohomologyModule A J (Ideal.fg_of_isNoetherianRing J)
            (ModuleCat.of A M) i)

Tag 0DXP, a lemma

Tag 0DXP in the Stacks Project.

Stacks.Algebraization.exists_isLocalAlgebraizationIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationComparisonLocal.lean, line 329. The attribute's comment: “existence of J₀”.

Stacks 0DXP. Let (A, 𝔪) be a Noetherian local ring, let I ⊆ A be a proper ideal, let M be a finite A-module and let s and d be integers. Assume A is I-adically complete with a dualizing complex, that cd(A, I) ≤ d, and that every prime 𝔭 ∉ V(I) with V(𝔭) ∩ V(I) ≠ {𝔪} has depth(M_𝔭) ≥ s or depth(M_𝔭) + dim(A/𝔭) > d + s. Then there is an ideal J₀ with V(J₀) ∩ V(I) = {𝔪} such that for every ideal J ⊆ J₀ with V(J) ∩ V(I) = {𝔪} the canonical map

RΓ_J(M) ⟶ RΓ_𝔪(M)^∧

is an isomorphism on cohomology in all degrees ≤ s.

This is the source's own proof: the case s < 0 is Stacks.Algebraization.isLocalAlgebraizationIdeal_of_lt_zero, and for 0 ≤ s the statement is the case J = 𝔪 of Stacks 0EFL, by Stacks.Algebraization.LocalAlgebraizationHypotheses.toAlgebraizationHypotheses on the hypotheses and Stacks.Algebraization.isLocalAlgebraizationIdeal_of_isAlgebraizationIdeal on the conclusion.

Condition (5) of Stacks 0EFL is stated against a dimension function on Spec(A), which the statement of Stacks 0DXP does not mention. No such datum is assumed here: hypothesis (1) provides a dualizing complex, and the dimension function attached to one by Stacks 0A7Z is Dualizing.dualizingDimensionFunctionOfArbitraryUniverse.

public theorem exists_isLocalAlgebraizationIdeal (I : Ideal A) (s d : ℤ)
    (omega : DerivedCategory (ModuleCat.{u} A))
    (H : LocalAlgebraizationHypotheses (M := M) I s d omega) :
    ∃ J₀ : Ideal A, IsLocalAlgebraizationIdeal (M := M) I H.ne_top s J₀

Sources

• Section 52.9, Tag 0EFP
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Algebraization.exists_notMem_mem_annihilator_homology_derivedCompletion_localCohomology_maximalIdeal · Stacks.Algebraization.localStabilizationHypotheses_iff · Stacks.Algebraization.zeroLocus_stabilizingIdeal_maximalIdeal_inter · Stacks.Algebraization.exists_stabilization · Stacks.Algebraization.exists_stabilization_finite_localCohomologyModule_maximalIdeal · Stacks.Algebraization.depthAddDimGtOnZeroLocus_maximalIdeal_iff · Stacks.Algebraization.finite_localCohomologyModule_stabilizingIdeal_maximalIdeal · Stacks.Algebraization.finite_localCohomologyModule_stabilizingIdeal_maximalIdeal_of_exists

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.