52.10 Algebraization of local… to 52.15 The completion functor

Section52.10 Algebraization of local cohomology, III#

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

Tag 0EFU, a situation

Tag 0EFU in the Stacks Project.

Stacks.Algebraization.BootstrapSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapSituation.lean, line 61.

The standing bootstrap situation for algebraization: a Noetherian ring with a dualizing complex, an ideal, a finite module, a specialization-stable subset of the adic locus, and the two integer bounds against which depth and cohomological dimension are measured.

public structure BootstrapSituation

Tag 0EID, a lemma

Tag 0EID in the Stacks Project.

Stacks.Algebraization.depth_localized_gt_of_no_intermediate_prime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapDepth.lean, line 93.

Stacks Project, Tag 0EID. In the bootstrap situation the depth at p exceeds s when no prime of V(I) \ T lies between p and a prime q of T.

public theorem depth_localized_gt_of_no_intermediate_prime
    (S : BootstrapSituation.{u, v, w})
    (p q : PrimeSpectrum S.A)
    (hpq : p.asIdeal ≤ q.asIdeal)
    (hp : p ∉ PrimeSpectrum.zeroLocus (S.I : Set S.A))
    (hq : q ∈ S.T)
    (h : ¬ ∃ r : PrimeSpectrum S.A,
      p.asIdeal ≤ r.asIdeal ∧ r.asIdeal ≤ q.asIdeal ∧
      r ∈ PrimeSpectrum.zeroLocus (S.I : Set S.A) ∧ r ∉ S.T) :
    enatToEInt
      (Module.depth (Localization.AtPrime p.asIdeal)
        (maximalIdeal (Localization.AtPrime p.asIdeal))
        (LocalizedModule p.asIdeal.primeCompl S.M)) > (S.s : EInt)

Tag 0EFV, a lemma

Tag 0EFV in the Stacks Project.

Stacks.Algebraization.finite_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapCompletion.lean, line 319. The attribute's comment: “completion”.

Stacks Project, Tag 0EFV (completion). The completed module of a bootstrap situation is finite over the completed ring.

public theorem finite_adicCompletion (S : BootstrapSituation.{u, v, w}) :
    Module.Finite (AdicCompletion S.I S.A) (AdicCompletion S.I S.M)

Stacks.Algebraization.subset_adicLocus_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapCompletion.lean, line 333. The attribute's comment: “completion”.

Stacks Project, Tag 0EFV (completion). The completed locus is contained in the adic locus of the extended ideal.

public theorem subset_adicLocus_adicCompletion (S : BootstrapSituation.{u, v, w}) :
    adicCompletionLocus S ⊆ PrimeSpectrum.zeroLocus
      ((S.I.map (algebraMap S.A (AdicCompletion S.I S.A))) :
        Set (AdicCompletion S.I S.A))

Stacks.Algebraization.stableUnderSpecialization_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapCompletion.lean, line 342. The attribute's comment: “completion”.

Stacks Project, Tag 0EFV (completion). The completed locus is stable under specialization.

public theorem stableUnderSpecialization_adicCompletion (S : BootstrapSituation.{u, v, w}) :
    StableUnderSpecialization (adicCompletionLocus S)

Stacks.Algebraization.dualizing_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapCompletion.lean, line 349. The attribute's comment: “completion”.

Stacks Project, Tag 0EFV (completion). Assumption (1) completes: the adic completion of a ring with a dualizing complex has one.

public theorem dualizing_adicCompletion (S : BootstrapSituation.{u, v, w}) :
    ∃ K : DerivedCategory (ModuleCat.{max u w} (AdicCompletion S.I S.A)),
      Dualizing.IsDualizingComplex K

Stacks.Algebraization.cohomologicalDimension_le_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapCompletion.lean, line 358. The attribute's comment: “completion”.

Stacks Project, Tag 0EFV (completion). Assumption (3) completes: cohomological dimension does not increase.

public theorem cohomologicalDimension_le_adicCompletion (S : BootstrapSituation.{u, v, w}) :
    Stacks.LocalCohomology.cohomologicalDimension (AdicCompletion S.I S.A)
      (S.I.map (algebraMap S.A (AdicCompletion S.I S.A)))
      (Ideal.fg_of_isNoetherianRing _) ≤ S.d

Stacks.Algebraization.completedLocalDepth_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapCompletion.lean, line 369. The attribute's comment: “completion”.

Stacks Project, Tag 0EFV (completion). Assumption (6) completes: the strict depth bound on completed localizations persists after adic completion.

public theorem completedLocalDepth_adicCompletion (S : BootstrapSituation.{u, v, w}) :
    ∀ q : PrimeSpectrum (AdicCompletion S.I S.A), q ∈ adicCompletionLocus S →
      let Aq := Localization.AtPrime q.asIdeal
      let Iq := (S.I.map (algebraMap S.A (AdicCompletion S.I S.A))).map
        (algebraMap (AdicCompletion S.I S.A) Aq)
      let Mq := LocalizedModule q.asIdeal.primeCompl (AdicCompletion S.I S.M)
      let A' := AdicCompletion Iq Aq
      let I' := Iq.map (algebraMap Aq A')
      let m' := (maximalIdeal Aq).map (algebraMap Aq A')
      ∀ p' : PrimeSpectrum A',
        ¬ I' ≤ p'.asIdeal →
        {r' : Ideal A' | r'.IsPrime ∧ p'.asIdeal ≤ r' ∧ I' ≤ r'} = {m'} →
        enatToEInt
          (Module.depth (Localization.AtPrime p'.asIdeal)
            (maximalIdeal (Localization.AtPrime p'.asIdeal))
            (LocalizedModule p'.asIdeal.primeCompl (AdicCompletion Iq Mq))) >
          (S.s : EInt)

Stacks.Algebraization.exists_localAlgebraizationHypotheses_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapCompletionLocal.lean, line 194. The attribute's comment: “parts (G) and (D) for T = {𝔪}: the hypotheses of Stacks 0DXP hold for the I-adic completion A', I', M' of A, I, M, whose locus is the closed point of A'”.

In a bootstrap situation with A local and T = {𝔪}, there is an object omega of the derived category of A'-modules for which the I-adic completions A', I', M' satisfy the hypotheses Stacks.Algebraization.LocalAlgebraizationHypotheses of the local algebraization theorem.

public theorem exists_localAlgebraizationHypotheses_adicCompletion [IsLocalRing S.A]
    (hT : S.T = {closedPoint S.A}) :
    letI := BootstrapSituation.isLocalRing_adicCompletion_self S hT
    letI : Module.Finite (AdicCompletion S.I S.A) (AdicCompletion S.I S.M) :=
      finite_adicCompletion S
    ∃ omega : DerivedCategory (ModuleCat.{u} (AdicCompletion S.I S.A)),
      LocalAlgebraizationHypotheses (M := AdicCompletion S.I S.M)
        (S.I.map (algebraMap S.A (AdicCompletion S.I S.A))) S.s S.d omega

Stacks.Algebraization.depth_or_depth_add_dimension_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapCompletionSituation.lean, line 52. The attribute's comment: “completion”.

Stacks Project, Tag 0EFV (G), assumption (4). The chain-of-primes depth estimate of a bootstrap situation persists after I-adic completion, for the completed locus.

public theorem depth_or_depth_add_dimension_adicCompletion (S : BootstrapSituation.{u, v, w}) :
    ∀ p r q : PrimeSpectrum (AdicCompletion S.I S.A),
      p.asIdeal ≤ r.asIdeal → r.asIdeal ≤ q.asIdeal →
      p ∉ PrimeSpectrum.zeroLocus
        ((S.I.map (algebraMap S.A (AdicCompletion S.I S.A))) : Set (AdicCompletion S.I S.A)) →
      r ∈ PrimeSpectrum.zeroLocus
        ((S.I.map (algebraMap S.A (AdicCompletion S.I S.A))) : Set (AdicCompletion S.I S.A)) →
      r ∉ adicCompletionLocus S → q ∈ adicCompletionLocus S →
      (enatToEInt
          (Module.depth (Localization.AtPrime p.asIdeal)
            (maximalIdeal (Localization.AtPrime p.asIdeal))
            (LocalizedModule p.asIdeal.primeCompl (AdicCompletion S.I S.M))) ≥ (S.s : EInt)) ∨
      (enatToEInt
          (Module.depth (Localization.AtPrime p.asIdeal)
            (maximalIdeal (Localization.AtPrime p.asIdeal))
            (LocalizedModule p.asIdeal.primeCompl (AdicCompletion S.I S.M))) +
        krullDimToEInt
          (ringKrullDim ((Localization.AtPrime q.asIdeal) ⧸
            p.asIdeal.map (algebraMap (AdicCompletion S.I S.A)
              (Localization.AtPrime q.asIdeal)))) >
        ((S.d + S.s : ℤ) : EInt))

Stacks.Algebraization.BootstrapSituation.adicCompletion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapCompletionSituation.lean, line 103. The attribute's comment: “part (G): the completed quadruple is again a situation as in Stacks 0EFU”.

Stacks Project, Tag 0EFV (G). The I-adic completion of a bootstrap situation: the completed ring A^∧, the extended ideal I A^∧, the completed module M^∧ and the preimage of the locus, with the same bounds.

public def adicCompletion (S : BootstrapSituation.{u, v, w}) : BootstrapSituation.{u, v, w}

Stacks.Algebraization.depthGtOnAssociatedSubset_of_le_jacobson, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapHypotheses.lean, line 115. The attribute's comment: “part (A), hypothesis (6) of Stacks 0EFK for A, I, 𝔞, M”.

Stacks Project, Tag 0EFV, hypothesis (6) of Stacks 0EFK. In a bootstrap situation whose ideal I lies in the Jacobson radical, a prime 𝔭 ∉ V(I) all of whose specializations on V(I) lie on V(𝔞) has depth(M_𝔭) > s.

A maximal ideal containing 𝔭 contains I, so V(𝔭) ∩ V(I) has a point 𝔮, which lies on V(𝔞) and hence in T. No prime of V(I) \ T lies between 𝔭 and 𝔮, since any prime of V(𝔭) ∩ V(I) lies on V(𝔞) ⊆ T; so Stacks 0EID gives the strict bound.

public theorem depthGtOnAssociatedSubset_of_le_jacobson
    (S : BootstrapSituation.{u, u, w}) (a : Ideal S.A) (_hIa : S.I ≤ a)
    (haT : PrimeSpectrum.zeroLocus (a : Set S.A) ⊆ S.T)
    (hjac : S.I ≤ (⊥ : Ideal S.A).jacobson) :
    DepthGtOnAssociatedSubset (M := S.M) S.I a S.s

Stacks.Algebraization.exists_mem_zeroLocus_dimension_le_of_le_jacobson, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapHypotheses.lean, line 137. The attribute's comment: “part (A), hypothesis (3) of Stacks 0EFI for A, I, 𝔞, M”.

Stacks Project, Tag 0EFV, hypothesis (3) of Stacks 0EFI. In a bootstrap situation whose ideal I lies in the Jacobson radical, a prime 𝔭 ∉ V(I) all of whose specializations on V(I) lie on V(𝔞) has one along which the relative dimension is at most d.

This is Stacks 0DXF: a minimal prime 𝔮 of 𝔭 + I has dim((A/𝔭)_𝔮) ≤ cd(A, I) ≤ d, and it lies on V(𝔞) because it lies on V(𝔭) ∩ V(I).

public theorem exists_mem_zeroLocus_dimension_le_of_le_jacobson
    (S : BootstrapSituation.{u, v, w}) (a : Ideal S.A)
    (hjac : S.I ≤ (⊥ : Ideal S.A).jacobson)
    (p : PrimeSpectrum S.A)
    (hpT : p ∈ associatedSubset S.I a) :
    ∃ q : PrimeSpectrum S.A,
      q ∈ (PrimeSpectrum.zeroLocus (p.asIdeal : Set S.A) ∩
          PrimeSpectrum.zeroLocus (a : Set S.A)) ∩
          PrimeSpectrum.zeroLocus (S.I : Set S.A) ∧
      krullDimToEInt
        (ringKrullDim ((Localization.AtPrime q.asIdeal) ⧸
          p.asIdeal.map (algebraMap S.A (Localization.AtPrime q.asIdeal)))) ≤
        (S.d : EInt)

Stacks.Algebraization.stabilizationHypotheses_and_depthGtOnAssociatedSubset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapHypotheses.lean, line 164. The attribute's comment: “part (A): all hypotheses of Stacks 0EFI and Stacks 0EFK for A, I, 𝔞, M”.

Stacks Project, Tag 0EFV, part (A). Let S be a bootstrap situation whose ideal I is contained in the Jacobson radical of A, and let I ⊆ 𝔞 be an ideal with V(𝔞) ⊆ T. Then all hypotheses of Stacks 0EFI and of Stacks 0EFK hold for A, I, 𝔞, M.

Hypothesis (1) is assumption (1) of the situation, hypothesis (2) is empty, hypothesis (3) is Stacks.Algebraization.exists_mem_zeroLocus_dimension_le_of_le_jacobson, hypothesis (4) is Stacks.Algebraization.depth_or_depth_add_dimension_of_mem_zeroLocus, and the extra hypothesis (6) of Stacks 0EFK is Stacks.Algebraization.depthGtOnAssociatedSubset_of_le_jacobson.

public theorem stabilizationHypotheses_and_depthGtOnAssociatedSubset
    (S : BootstrapSituation.{u, u, w}) (a : Ideal S.A) (hIa : S.I ≤ a)
    (haT : PrimeSpectrum.zeroLocus (a : Set S.A) ⊆ S.T)
    (hjac : S.I ≤ (⊥ : Ideal S.A).jacobson) :
    (∃ omega : DerivedCategory (ModuleCat.{max u w} S.A),
        StabilizationHypotheses (M := S.M) S.I a S.s S.d omega) ∧
      DepthGtOnAssociatedSubset (M := S.M) S.I a S.s

Stacks.Algebraization.algebraizationHypotheses_of_supplementaryBound, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapHypotheses.lean, line 190. The attribute's comment: “part (B): all hypotheses of Stacks 0EFL except possibly (5) for A, I, 𝔞, M”.

Stacks Project, Tag 0EFV, part (B). Let S be a bootstrap situation whose ring is I-adically complete, and let I ⊆ 𝔞 be an ideal with V(𝔞) ⊆ T. Then all hypotheses of Stacks 0EFL except possibly (5) hold for A, I, 𝔞, M: given a dimension function with its extreme values on V(𝔞) ∩ V(I) and given condition (5), the hypotheses of that lemma hold in full.

Condition (1) is the completeness together with assumption (1) of the situation, condition (2) is empty, condition (3) is assumption (3) of the situation, and condition (4) is the same as condition (4) of Stacks 0EFI, proved in part (A).

public theorem algebraizationHypotheses_of_supplementaryBound
    (S : BootstrapSituation.{u, u, w}) (a : Ideal S.A) (_hIa : S.I ≤ a)
    (haT : PrimeSpectrum.zeroLocus (a : Set S.A) ⊆ S.T)
    (hcomplete : IsAdicComplete S.I S.A)
    (δ : PrimeSpectrum S.A → ℤ) (δmax δmin : ℤ)
    (hδ : IsDimensionFunctionProp δ)
    (hmax : IsGreatest (δ '' (PrimeSpectrum.zeroLocus (a : Set S.A) ∩
      PrimeSpectrum.zeroLocus (S.I : Set S.A))) δmax)
    (hmin : IsLeast (δ '' (PrimeSpectrum.zeroLocus (a : Set S.A) ∩
      PrimeSpectrum.zeroLocus (S.I : Set S.A))) δmin)
    (h5 : ∀ p : PrimeSpectrum S.A,
      p ∉ PrimeSpectrum.zeroLocus (S.I : Set S.A) →
      p ∉ associatedSubset S.I a →
      ((PrimeSpectrum.zeroLocus (p.asIdeal : Set S.A) ∩
        PrimeSpectrum.zeroLocus (a : Set S.A)) ∩
        PrimeSpectrum.zeroLocus (S.I : Set S.A)).Nonempty →
      enatToEInt
          (Module.depth (Localization.AtPrime p.asIdeal)
            (maximalIdeal (Localization.AtPrime p.asIdeal))
            (LocalizedModule p.asIdeal.primeCompl S.M)) < (S.s : EInt) →
      (krullDimToEInt (Module.supportDim (Localization.AtPrime p.asIdeal)
            (LocalizedModule p.asIdeal.primeCompl S.M)) < ((S.s + 2 : ℤ) : EInt) ∨
        (S.d + δmax - 1 < δ p) ∨
        (∀ q : PrimeSpectrum S.A,
          q ∈ (PrimeSpectrum.zeroLocus (p.asIdeal : Set S.A) ∩
            PrimeSpectrum.zeroLocus (a : Set S.A)) ∩
            PrimeSpectrum.zeroLocus (S.I : Set S.A) →
          enatToEInt
              (Module.depth (Localization.AtPrime p.asIdeal)
                (maximalIdeal (Localization.AtPrime p.asIdeal))
                (LocalizedModule p.asIdeal.primeCompl S.M)) +
              krullDimToEInt
                (ringKrullDim ((Localization.AtPrime q.asIdeal) ⧸
                  p.asIdeal.map (algebraMap S.A (Localization.AtPrime q.asIdeal)))) >
            ((S.d + S.s + δmax - δmin - 2 : ℤ) : EInt)))) :
    ∃ omega : DerivedCategory (ModuleCat.{max u w} S.A),
      AlgebraizationHypotheses (M := S.M) S.I a S.s S.d omega δ δmax δmin

Stacks.Algebraization.localStabilizationHypotheses_and_depthGtAtMaximalIdeal_of_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapHypotheses.lean, line 260. The attribute's comment: “part (C): all hypotheses of Stacks 0DXM and Stacks 0EFQ for A, 𝔪, I, M”.

Stacks Project, Tag 0EFV, part (C). Let S be a bootstrap situation whose ring is local with maximal ideal 𝔪, and suppose 𝔪 ∈ T, which is the standing hypothesis V(𝔞) ⊆ T at 𝔞 = 𝔪. Then all hypotheses of Stacks 0DXM and of Stacks 0EFQ hold for A, 𝔪, I, M.

This is part (A) at 𝔞 = 𝔪: in a local ring the Jacobson radical is the maximal ideal, which contains I because the closed point lies in T ⊆ V(I). The hypotheses of Stacks 0DXM are those of Stacks 0EFI at J = 𝔪 by localStabilizationHypotheses_iff, and hypothesis (6) of Stacks 0EFQ is hypothesis (6) of Stacks 0EFK there by depthGtOnAssociatedSubset_maximalIdeal_iff.

public theorem localStabilizationHypotheses_and_depthGtAtMaximalIdeal_of_mem
    (hmT : closedPoint S.A ∈ S.T) :
    (∃ omega : DerivedCategory (ModuleCat.{max u w} S.A),
        LocalStabilizationHypotheses (M := S.M) S.I S.s S.d omega) ∧
      DepthGtAtMaximalIdeal (M := S.M) S.I S.s

Stacks.Algebraization.localAlgebraizationHypotheses_of_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapHypotheses.lean, line 281. The attribute's comment: “part (D): all hypotheses of Stacks 0DXP for A, 𝔪, I, M”.

Stacks Project, Tag 0EFV, part (D). Let S be a bootstrap situation whose ring is local with maximal ideal 𝔪 and I-adically complete, and suppose 𝔪 ∈ T, which is the standing hypothesis V(𝔞) ⊆ T at 𝔞 = 𝔪. Then all hypotheses of Stacks 0DXP hold for A, 𝔪, I, M.

Conditions (1) and (2) are the completeness together with assumption (1) of the situation, condition (3) is assumption (3) of the situation, and condition (4) is the same as condition (4) of Stacks 0DXM, proved in part (C).

public theorem localAlgebraizationHypotheses_of_mem
    (hcomplete : IsAdicComplete S.I S.A) (hmT : closedPoint S.A ∈ S.T) :
    ∃ omega : DerivedCategory (ModuleCat.{max u w} S.A),
      LocalAlgebraizationHypotheses (M := S.M) S.I S.s S.d omega

Stacks.Algebraization.localStabilizationHypotheses_and_depthGtAtMaximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapLocalCohomologyLimit.lean, line 167. The attribute's comment: “part (C) for T = {𝔪}: the hypotheses of Stacks 0DXM and hypothesis (6) of Stacks 0EFQ, with the dualizing complex of Situation 0EFU supplied as the witness omega”.

In the bootstrap situation of Stacks 0EFU with A local and T = {𝔪}, the hypotheses (1)–(4) of Stacks 0DXM and hypothesis (6) of Stacks 0EFQ hold for A, I, 𝔪, M, for every dualizing complex omega.

public theorem localStabilizationHypotheses_and_depthGtAtMaximalIdeal [IsLocalRing S.A]
    (hT : S.T = {closedPoint S.A}) (omega : DerivedCategory (ModuleCat.{u} S.A))
    (homega : Dualizing.IsDualizingComplex omega) :
    LocalStabilizationHypotheses (M := S.M) S.I S.s S.d omega ∧
      DepthGtAtMaximalIdeal (M := S.M) S.I S.s

Stacks.Algebraization.subset_adicLocus_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapLocalization.lean, line 454. The attribute's comment: “localization”.

The localized locus is contained in the adic locus of the extended ideal.

public theorem subset_adicLocus_localization
    (X : BootstrapSituation.{u, v, w}) (S : Submonoid X.A) :
    locus X S ⊆ PrimeSpectrum.zeroLocus
      ((X.I.map (algebraMap X.A (Localization S))) : Set (Localization S))

Stacks.Algebraization.stableUnderSpecialization_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapLocalization.lean, line 462. The attribute's comment: “localization”.

The localized locus is stable under specialization.

public theorem stableUnderSpecialization_localization
    (X : BootstrapSituation.{u, v, w}) (S : Submonoid X.A) :
  StableUnderSpecialization (locus X S)

Stacks.Algebraization.dualizing_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapLocalization.lean, line 469. The attribute's comment: “localization”.

Assumption (1) localizes: a localization of a ring with a dualizing complex has one.

public theorem dualizing_localization
    (X : BootstrapSituation.{u, v, w}) (S : Submonoid X.A) :
    ∃ K : DerivedCategory (ModuleCat.{max u w} (Localization S)),
      Dualizing.IsDualizingComplex K

Stacks.Algebraization.cohomologicalDimension_le_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapLocalization.lean, line 478. The attribute's comment: “localization”.

Assumption (3) localizes: cohomological dimension does not increase.

public theorem cohomologicalDimension_le_localization
    (X : BootstrapSituation.{u, v, w}) (S : Submonoid X.A) :
    Stacks.LocalCohomology.cohomologicalDimension (Localization S)
      (X.I.map (algebraMap X.A (Localization S)))
      (Ideal.fg_of_isNoetherianRing _) ≤ X.d

Stacks.Algebraization.depth_or_depth_add_dimension_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapLocalization.lean, line 489. The attribute's comment: “localization”.

Assumption (4) localizes: the chain-of-primes depth estimate holds for the localized data.

public theorem depth_or_depth_add_dimension_localization
    (X : BootstrapSituation.{u, v, w}) (S : Submonoid X.A) :
    ∀ p r q : PrimeSpectrum (Localization S),
      p.asIdeal ≤ r.asIdeal → r.asIdeal ≤ q.asIdeal →
      p ∉ PrimeSpectrum.zeroLocus
        ((X.I.map (algebraMap X.A (Localization S))) : Set (Localization S)) →
      r ∈ PrimeSpectrum.zeroLocus
        ((X.I.map (algebraMap X.A (Localization S))) : Set (Localization S)) →
      r ∉ locus X S → q ∈ locus X S →
      (enatToEInt
          (Module.depth (Localization.AtPrime p.asIdeal)
            (maximalIdeal (Localization.AtPrime p.asIdeal))
            (LocalizedModule p.asIdeal.primeCompl (LocalizedModule S X.M))) ≥
          (X.s : EInt)) ∨
      (enatToEInt
          (Module.depth (Localization.AtPrime p.asIdeal)
            (maximalIdeal (Localization.AtPrime p.asIdeal))
            (LocalizedModule p.asIdeal.primeCompl (LocalizedModule S X.M))) +
        krullDimToEInt
          (ringKrullDim ((Localization.AtPrime q.asIdeal) ⧸
            p.asIdeal.map (algebraMap (Localization S)
              (Localization.AtPrime q.asIdeal)))) >
        ((X.d + X.s : ℤ) : EInt))

Stacks.Algebraization.completedLocalDepth_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapLocalization.lean, line 532. The attribute's comment: “localization”.

Assumption (6) localizes: the strict depth bound on completed localizations persists.

public theorem completedLocalDepth_localization
    (X : BootstrapSituation.{u, v, w}) (S : Submonoid X.A) :
    ∀ q : PrimeSpectrum (Localization S), q ∈ locus X S →
      let Aq := Localization.AtPrime q.asIdeal
      let Iq := (X.I.map (algebraMap X.A (Localization S))).map
        (algebraMap (Localization S) Aq)
      let Mq := LocalizedModule q.asIdeal.primeCompl (LocalizedModule S X.M)
      let A' := AdicCompletion Iq Aq
      let I' := Iq.map (algebraMap Aq A')
      let m' := (maximalIdeal Aq).map (algebraMap Aq A')
      ∀ p' : PrimeSpectrum A',
        ¬ I' ≤ p'.asIdeal →
        {r' : Ideal A' | r'.IsPrime ∧ p'.asIdeal ≤ r' ∧ I' ≤ r'} = {m'} →
      enatToEInt
          (Module.depth (Localization.AtPrime p'.asIdeal)
            (maximalIdeal (Localization.AtPrime p'.asIdeal))
            (LocalizedModule p'.asIdeal.primeCompl (AdicCompletion Iq Mq))) >
          (X.s : EInt)

Stacks.Algebraization.BootstrapSituation.localize, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapLocalization.lean, line 727. The attribute's comment: “part (F): for a multiplicative subset S ⊆ A the quadruple S⁻¹A, S⁻¹I, T', S⁻¹M, with T' the inverse image of T, is again a situation as in Stacks 0EFU”.

Stacks Project, Tag 0EFV, part (F). The localization of a bootstrap situation at a multiplicative subset S ⊆ A: the quadruple S⁻¹A, S⁻¹I, T', S⁻¹M, with T' the inverse image of T in V(S⁻¹I), again satisfies every assumption of Situation 0EFU, with the same bounds s and d.

public def localize
    (X : BootstrapSituation.{u, v, w}) (S : Submonoid X.A) :
    BootstrapSituation.{u, max u v, w}

Stacks.Algebraization.depth_or_depth_add_dimension_of_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapShrink.lean, line 42. The attribute's comment: “shrinking_t”.

Stacks Project, Tag 0EFV (shrinking T). The chain-of-primes depth estimate of a bootstrap situation persists after restricting its locus to any subset.

public theorem depth_or_depth_add_dimension_of_subset
    (S : BootstrapSituation.{u, v, w})
    (T' : Set (PrimeSpectrum S.A)) (hsub : T' ⊆ S.T) :
    ∀ p r q : PrimeSpectrum S.A,
      p.asIdeal ≤ r.asIdeal → r.asIdeal ≤ q.asIdeal →
      p ∉ PrimeSpectrum.zeroLocus (S.I : Set S.A) →
      r ∈ PrimeSpectrum.zeroLocus (S.I : Set S.A) → r ∉ T' → q ∈ T' →
      (enatToEInt
          (Module.depth (Localization.AtPrime p.asIdeal)
            (maximalIdeal (Localization.AtPrime p.asIdeal))
            (LocalizedModule p.asIdeal.primeCompl S.M)) ≥ (S.s : EInt)) ∨
      (enatToEInt
          (Module.depth (Localization.AtPrime p.asIdeal)
            (maximalIdeal (Localization.AtPrime p.asIdeal))
            (LocalizedModule p.asIdeal.primeCompl S.M)) +
        krullDimToEInt
          (ringKrullDim ((Localization.AtPrime q.asIdeal) ⧸
            p.asIdeal.map (algebraMap S.A (Localization.AtPrime q.asIdeal)))) >
        ((S.d + S.s : ℤ) : EInt))

Stacks.Algebraization.BootstrapSituation.shrink, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapShrink.lean, line 74. The attribute's comment: “part (E): for a smaller specialization-stable T' ⊆ T the quadruple A, I, T', M is again a situation as in Stacks 0EFU”.

Stacks Project, Tag 0EFV, part (E). The bootstrap situation obtained by restricting the locus of S to a smaller specialization-stable subset: A, I, T', M with T' ⊆ T again satisfies every assumption of Situation 0EFU, with the same bounds s and d.

public def BootstrapSituation.shrink
    (S : BootstrapSituation.{u, v, w})
    (T' : Set (PrimeSpectrum S.A)) (hsub : T' ⊆ S.T)
    (hstable : StableUnderSpecialization T') :
    BootstrapSituation.{u, v, w}

Tag 0EFR, a lemma

Tag 0EFR in the Stacks Project.

Stacks.Algebraization.exists_pow_le_annihilator_localCohomologyModule_of_eq_closedPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapLocalCohomologyLimit.lean, line 207. The attribute's comment: “the annihilation assertion: Hⁱ_𝔪(M) is annihilated by a power of I for i ≤ s”.

In the bootstrap situation of Stacks 0EFU with A local and T = {𝔪}, a single power of I annihilates Hⁱ_𝔪(M) in every degree i ≤ s.

public theorem exists_pow_le_annihilator_localCohomologyModule_of_eq_closedPoint
    [IsLocalRing S.A] (hT : S.T = {closedPoint S.A}) :
    ∃ n : ℕ, ∀ i : ℤ, i ≤ S.s →
      S.I ^ n ≤ Module.annihilator S.A
        (Stacks.LocalCohomology.localCohomologyModule S.A (maximalIdeal S.A)
          (Ideal.fg_of_isNoetherianRing _) (ModuleCat.of S.A S.M) i)

Stacks.Algebraization.isIso_localCohomologyToAdicQuotientLimit_of_isAdicComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapLocalCohomologyLimit.lean, line 341. The attribute's comment: “both assertions, with no carried hypothesis, for I-adically complete A”.

In the bootstrap situation of Stacks 0EFU with A local, I-adically complete and T = {𝔪}, the map Hⁱ_𝔪(M) ⟶ lim Hⁱ_𝔪(M/IⁿM) is an isomorphism for i ≤ s and a single power of I annihilates these modules.

public theorem isIso_localCohomologyToAdicQuotientLimit_of_isAdicComplete
    [IsLocalRing S.A] [IsAdicComplete S.I S.A] (hT : S.T = {closedPoint S.A}) :
    (∀ i : ℤ, i ≤ S.s →
        IsIso (localCohomologyToAdicQuotientLimit S.A S.I (maximalIdeal S.A)
          (maximalIdeal S.A) (ModuleCat.of S.A S.M) rfl i)) ∧
      ∃ n : ℕ, ∀ i : ℤ, i ≤ S.s →
        S.I ^ n ≤ Module.annihilator S.A
          (Stacks.LocalCohomology.localCohomologyModule S.A (maximalIdeal S.A)
            (Ideal.fg_of_isNoetherianRing _) (ModuleCat.of S.A S.M) i)

Stacks.Algebraization.isIso_localCohomologyToAdicQuotientLimit_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapLocalCohomologyLimit.lean, line 387. The attribute's comment: “both assertions read over the I-adic completion A', I', M' of the situation, for an arbitrary A: Hⁱ_{𝔪'}(M') → lim Hⁱ_{𝔪'}(M'/(I')ⁿM') is an isomorphism for i ≤ s and a power of I' annihilates these modules. No completeness assumption on A; this is the statement the source's proof establishes over the completion”.

In the bootstrap situation with A local and T = {𝔪}, over the I-adic completion A', I', M': the map Hⁱ_{𝔪'}(M') ⟶ lim Hⁱ_{𝔪'}(M'/(I')ⁿM') is an isomorphism for i ≤ s, and a single power of I' annihilates these modules. Nothing is assumed about A beyond Situation 0EFU and the locality of the locus.

public theorem isIso_localCohomologyToAdicQuotientLimit_adicCompletion
    [IsLocalRing S.A] (hT : S.T = {closedPoint S.A}) :
    letI : IsLocalRing S.adicCompletion.A :=
      BootstrapSituation.isLocalRing_adicCompletion S hT
    (∀ i : ℤ, i ≤ S.adicCompletion.s →
        IsIso (localCohomologyToAdicQuotientLimit S.adicCompletion.A S.adicCompletion.I
          (maximalIdeal S.adicCompletion.A) (maximalIdeal S.adicCompletion.A)
          (ModuleCat.of S.adicCompletion.A S.adicCompletion.M) rfl i)) ∧
      ∃ n : ℕ, ∀ i : ℤ, i ≤ S.adicCompletion.s →
        S.adicCompletion.I ^ n ≤ Module.annihilator S.adicCompletion.A
          (Stacks.LocalCohomology.localCohomologyModule S.adicCompletion.A
            (maximalIdeal S.adicCompletion.A) (Ideal.fg_of_isNoetherianRing _)
            (ModuleCat.of S.adicCompletion.A S.adicCompletion.M) i)

Stacks.Algebraization.isIso_localCohomologyToAdicQuotientLimit_closedPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/CompletionUnitDescent.lean, line 621. The attribute's comment: “both assertions over A itself for every Noetherian local ring: in Situation 0EFU with A local and T = {𝔪}, the map Hⁱ_𝔪(M) → lim Hⁱ_𝔪(M/IⁿM) is an isomorphism for i ≤ s and a single power of I annihilates these modules”.

Stacks 0EFR. In the bootstrap situation of Stacks 0EFU with A local and T = {𝔪}, the map Hⁱ_𝔪(M) ⟶ lim Hⁱ_𝔪(M/IⁿM) is an isomorphism for i ≤ s, and a single power of I annihilates these modules. Nothing is assumed about A beyond Situation 0EFU and the locality of the locus; in particular A need not be I-adically complete.

The isomorphism is the composite of the two displays of the source's proof. The first, Hⁱ_𝔪(M) ≅ Hⁱ(RΓ_𝔪(M)^∧), is Stacks.Algebraization.isIso_homology_localCohomologyToCompletedLocalCohomology_closedPoint, which obtains it over the I-adic completion from Stacks 0DXP and Stacks 0EFQ and descends it; the second, Hⁱ(RΓ_𝔪(M)^∧) ≅ lim Hⁱ_𝔪(M/IⁿM), is Stacks 0DXJ. The annihilation assertion is Stacks.Algebraization.exists_pow_le_annihilator_localCohomologyModule_of_eq_closedPoint, which needs only Stacks 0EFQ over A itself.

public theorem isIso_localCohomologyToAdicQuotientLimit_closedPoint
    [IsLocalRing S.A] (hT : S.T = {closedPoint S.A}) :
    (∀ i : ℤ, i ≤ S.s →
        IsIso (localCohomologyToAdicQuotientLimit S.A S.I (maximalIdeal S.A)
          (maximalIdeal S.A) (ModuleCat.of S.A S.M) rfl i)) ∧
      ∃ n : ℕ, ∀ i : ℤ, i ≤ S.s →
        S.I ^ n ≤ Module.annihilator S.A
          (Stacks.LocalCohomology.localCohomologyModule S.A (maximalIdeal S.A)
            (Ideal.fg_of_isNoetherianRing _) (ModuleCat.of S.A S.M) i)

Tag 0EFW, a lemma

Tag 0EFW in the Stacks Project.

Stacks.Algebraization.exists_bootstrapSituation_of_depth_gt_or_depth_add_dim_gt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/AlgebraizationLocalCohomologyIIIBootstrapCriterion.lean, line 160.

Stacks Project, Tag 0EFW. Let I ⊆ 𝔞 be ideals of a Noetherian ring A admitting a dualizing complex, let M be a finite A-module and let s, d be integers with cd(A, I) ≤ d. If for every prime p ∉ V(I) and every q ∈ V(p) ∩ V(𝔞) either depth(M_p) > s or depth(M_p) + dim((A/p)_q) > d + s, then A, I, V(𝔞), M, s, d are as in the bootstrap situation of Stacks 0EFU.

public theorem exists_bootstrapSituation_of_depth_gt_or_depth_add_dim_gt
    {A : Type u} [CommRing A] [IsNoetherianRing A]
    (I a : Ideal A) (hIa : I ≤ a)
    {M : Type v} [AddCommGroup M] [Module A M] [Module.Finite A M]
    (s d : ℤ)
    (hdual : ∃ K : DerivedCategory (ModuleCat.{max u w} A), Dualizing.IsDualizingComplex K)
    (hcd : Stacks.LocalCohomology.cohomologicalDimension A I
      (Ideal.fg_of_isNoetherianRing I) ≤ d)
    (hdepth : ∀ p q : PrimeSpectrum A,
      p.asIdeal ≤ q.asIdeal →
      p ∉ PrimeSpectrum.zeroLocus (I : Set A) →
      q ∈ PrimeSpectrum.zeroLocus (a : Set A) →
      (enatToEInt
          (Module.depth (Localization.AtPrime p.asIdeal)
            (maximalIdeal (Localization.AtPrime p.asIdeal))
            (LocalizedModule p.asIdeal.primeCompl M)) > (s : EInt)) ∨
      (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))) :
    ∃ S : BootstrapSituation.{u, v, w},
      S.A = A ∧
      HEq S.commRing (inferInstance : CommRing A) ∧
      HEq S.isNoetherianRing (inferInstance : IsNoetherianRing A) ∧
      HEq S.I I ∧ S.M = M ∧
      HEq S.addCommGroup (inferInstance : AddCommGroup M) ∧
      HEq S.module (inferInstance : Module A M) ∧
      HEq S.finite (inferInstance : Module.Finite A M) ∧
      HEq S.T (PrimeSpectrum.zeroLocus (a : Set A)) ∧
      S.s = s ∧ S.d = d

Tag 0EFX, a lemma

Tag 0EFX in the Stacks Project.

Stacks.Algebraization.exists_map_idealPowerTower_eq_zero_closedPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapClosedPointProZero.lean, line 525. The attribute's comment: “the pro-zero assertion for i ≤ s at T = {𝔪} over a Noetherian local ring in Situation 0EFU”.

Stacks Project, Tag 0EFX, the pro-zero assertion, at T = {𝔪}. In Situation [Stacks, Tag 0EFU] with A local and T = {𝔪}, the inverse system {H^i_𝔪(IⁿM)} is pro-zero for every i ≤ s: for every m some transition map H^i_𝔪(IᵏM) ⟶ H^i_𝔪(IᵐM) vanishes.

This is the first paragraph of the source's proof, carried out at this locus. Its two inputs are isIso_limitLift_localCohomologyAdicCone_closedPoint, which is part (4) of [Stacks, Tag 0EFY] and the isomorphism assertion of [Stacks, Tag 0EFR] in the set-indexed model, and the Artinianness of local cohomology at the closed point of a finite module, which supplies both part (1) of [Stacks, Tag 0EFY] (through a descending chain of kernels) and the Mittag-Leffler condition in the range form that the eventual-range lemma consumes. Nothing beyond the situation is assumed; in particular A need not be I-adically complete.

The source's T is an arbitrary specialization-stable subset of V(I). The general case is the last paragraph of the source's proof: it needs the per-prime assertion uniformly in 𝔮 ∈ T, which the source gets by transporting the vanishing to the finite Ext modules Ext^j_A(IⁿM, ω_A^•) by local duality and spreading it out. The statement proved here is exactly the per-prime input of that argument at a single prime, since Stacks.Algebraization.BootstrapSituation.localize and Stacks.Algebraization.BootstrapSituation.shrink turn a situation and a 𝔮 ∈ T into a situation over A_𝔮 with locus the closed point.

theorem exists_map_idealPowerTower_eq_zero_closedPoint [IsLocalRing S.A]
    (hT : S.T = {closedPoint S.A}) (i : ℤ) (hi : i ≤ S.s) (m : ℕ) :
    ∃ k : ℕ, ∃ h : m ≤ k,
      (localCohomologyWithSupportInModuleFunctor.{u, u} S.A S.T i).map
        ((idealPowerTower.{u, u} S.I (ModuleCat.of S.A S.M)).map (homOfLE h).op) = 0

Stacks.Algebraization.hasStableImageIdealPowerCohomology_closedPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapClosedPointProZero.lean, line 556. The attribute's comment: “the stable-image assertion in degree s + 1 at T = {𝔪} over a Noetherian local ring in Situation 0EFU”.

Stacks Project, Tag 0EFX, the stable-image assertion, at T = {𝔪}. In Situation [Stacks, Tag 0EFU] with A local and T = {𝔪}, the stable-image assertion of the tag holds in degree s + 1, based at m₀ = 0: for every m there is a c ≥ m such that for k ≥ c the image of H^{s+1}_𝔪(IᵏM) ⟶ H^{s+1}_𝔪(IᵐM) maps injectively to H^{s+1}_𝔪(I⁰M).

Its single input is the invertibility of the limit comparison in degree s itself, which is inside the range i ≤ s of isIso_limitLift_localCohomologyAdicCone_closedPoint; the Artinianness of the terms turns it into the containment of the stable images in the image of H^s_𝔪(M), and the naturality of the connecting map of 0 → IⁿM → M → M/IⁿM → 0 does the rest. Nothing beyond the situation is assumed.

As with the pro-zero assertion, the general specialization-stable T needs the uniformity in 𝔮 ∈ T of the source's last paragraph; see exists_map_idealPowerTower_eq_zero_closedPoint.

theorem hasStableImageIdealPowerCohomology_closedPoint [IsLocalRing S.A]
    (hT : S.T = {closedPoint S.A}) :
    HasStableImageIdealPowerCohomology.{u, u} S.T S.I (ModuleCat.of S.A S.M) (S.s + 1) 0

Stacks.Algebraization.exists_map_idealPowerTower_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapUniformProZero.lean, line 280. The attribute's comment: “the pro-zero assertion in degrees 0 ≤ i ≤ s at a general specialization-stable T in Situation 0EFU”.

Stacks Project, Tag 0EFX, the pro-zero assertion, at a general specialization-stable T. In Situation [Stacks, Tag 0EFU] the inverse system {H^i_T(IⁿM)} is pro-zero for every i ≤ s: for every m some transition map H^i_T(IᵏM) ⟶ H^i_T(IᵐM) vanishes.

This is the source's proof carried out in full. The per-prime assertion at each 𝔮 ∈ T is Stacks.Algebraization.exists_localized_localCohomology_idealPowerTower_map_eq_zero; its bound is made independent of 𝔮 by Stacks.Algebraization.exists_forall_localized_localCohomology_map_eq_zero, which is the local-duality paragraph; and the passage from the uniform per-prime statement to the global one is Stacks.Algebraization.exists_map_idealPowerTower_eq_zero_of_uniform, i.e. Lemma [Stacks, Tag 0EF9]. Nothing is assumed beyond the data of Situation [Stacks, Tag 0EFU].

theorem exists_map_idealPowerTower_eq_zero (S : BootstrapSituation.{u, u, u}) (i : ℕ)
    (hi : (i : ℤ) ≤ S.s) (m : ℕ) :
    ∃ k : ℕ, ∃ h : m ≤ k,
      (localCohomologyWithSupportInModuleFunctor.{u, u} S.A S.T (i : ℤ)).map
        ((idealPowerTower.{u, u} S.I (ModuleCat.of S.A S.M)).map (homOfLE h).op) = 0

Stacks.Algebraization.isProZeroIdealPowerCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapUniformProZero.lean, line 301. The attribute's comment: “the pro-zero assertion in every degree i ≤ s at a general specialization-stable T in Situation 0EFU”.

Stacks Project, Tag 0EFX, the pro-zero assertion, in every degree i ≤ s and at a general specialization-stable T. In Situation [Stacks, Tag 0EFU] the inverse system {H^i_T(IⁿM)} is pro-zero for every i ≤ s: for every m some transition map H^i_T(IᵏM) ⟶ H^i_T(IᵐM) vanishes.

In negative degrees the system vanishes term by term (Stacks.LocalCohomology.exists_map_idealPowerTower_eq_zero_of_neg); in degrees 0 ≤ i ≤ s this is Stacks.Algebraization.exists_map_idealPowerTower_eq_zero, whose proof is the source's own, the local-duality paragraph included. This is also the form in which the consequences of [Stacks, Tag 0EFY] consume the assertion.

theorem isProZeroIdealPowerCohomology (S : BootstrapSituation.{u, u, u}) (i : ℤ)
    (hi : i ≤ S.s) :
    IsProZeroIdealPowerCohomology.{u, u} S.T S.I (ModuleCat.of S.A S.M) i

Stacks.Algebraization.exists_hasStableImageIdealPowerCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapUniformStableImage.lean, line 274. The attribute's comment: “the stable-image assertion in degree s + 1 at a general specialization-stable T in Situation 0EFU”.

Stacks Project, Tag 0EFX, the stable-image assertion, at a general specialization-stable T. In Situation [Stacks, Tag 0EFU] there is an m₀ such that for every m ≥ m₀ there is an m'(m) ≥ m with: for k ≥ m'(m) the image of H^{s+1}_T(IᵏM) ⟶ H^{s+1}_T(IᵐM) maps injectively into H^{s+1}_T(I^{m₀}M).

This is the source's proof carried out in full. The per-prime assertion at each 𝔮 ∈ T is Stacks.Algebraization.exists_localized_ker_le_ker_idealPowerTower; its bound is made independent of 𝔮 by Stacks.Algebraization.exists_forall_localized_ker_le_ker_idealPowerTower, which is the local-duality paragraph in the degree the tag states this assertion in; and the passage from the uniform per-prime statement to the global one is Lemma [Stacks, Tag 0EFA]. In negative degrees the system vanishes term by term. Nothing is assumed beyond the data of Situation [Stacks, Tag 0EFU].

theorem exists_hasStableImageIdealPowerCohomology (S : BootstrapSituation.{u, u, u}) :
    ∃ m₀ : ℕ, HasStableImageIdealPowerCohomology.{u, u} S.T S.I (ModuleCat.of S.A S.M)
      (S.s + 1) m₀

Stacks.Algebraization.isProZero_and_hasStableImage_idealPowerCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapUniformStableImage.lean, line 307.

Stacks Project, Tag 0EFX at a general specialization-stable T: both assertions. In Situation [Stacks, Tag 0EFU] the inverse systems {H^i_T(IⁿM)} are pro-zero for i ≤ s, and there is an m₀ such that for every m ≥ m₀ there is an m'(m) ≥ m with: for k ≥ m'(m) the image of H^{s+1}_T(IᵏM) ⟶ H^{s+1}_T(IᵐM) maps injectively into H^{s+1}_T(I^{m₀}M).

The first assertion is Stacks.Algebraization.isProZeroIdealPowerCohomology and the second Stacks.Algebraization.exists_hasStableImageIdealPowerCohomology. Both are the source's own proof, the local-duality paragraph included; nothing beyond the data of Situation [Stacks, Tag 0EFU] is assumed.

theorem isProZero_and_hasStableImage_idealPowerCohomology (S : BootstrapSituation.{u, u, u}) :
    (∀ i ≤ S.s, IsProZeroIdealPowerCohomology.{u, u} S.T S.I (ModuleCat.of S.A S.M) i) ∧
      ∃ m₀ : ℕ, HasStableImageIdealPowerCohomology.{u, u} S.T S.I (ModuleCat.of S.A S.M)
        (S.s + 1) m₀

Stacks.LocalCohomology.exists_map_idealPowerTower_eq_zero_of_local, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/IdealPowerProZero.lean, line 199. The attribute's comment: “the pro-zero assertion, from the per-prime vanishing taken as an explicit hypothesis; that per-prime vanishing is the local-duality half of the source's proof and is not proved here”.

Stacks Project, Tag 0EFX, the pro-zero assertion, globalized. If for every m the transition maps H^i_{𝔭A_𝔭}((IᵏM)_𝔭) → H^i_{𝔭A_𝔭}((IᵐM)_𝔭) vanish for every 𝔭 ∈ T and every k ≥ m'(m), then the inverse system {H^i_T(IⁿM)} is pro-zero: for every m some transition map into the m-th term is zero.

This is the last paragraph of the source's proof, which reduces the lemma to the per-prime assertion: the reduction is Lemma [Stacks, Tag 0EF9], applied to the tower {IⁿM}. The per-prime assertion itself, which the source proves by local duality, is the hypothesis hlocal.

theorem exists_map_idealPowerTower_eq_zero_of_local [IsNoetherianRing A]
    (hdim : ringKrullDim A < ⊤) (T : Set (PrimeSpectrum A)) (hT : StableUnderSpecialization T)
    (I : Ideal A) (M : ModuleCat.{max u v} A) (i : ℕ) (m' : ℕ → ℕ) (hm' : ∀ m, m ≤ m' m)
    (hlocal : ∀ (m k : ℕ) (_hbound : m' m ≤ k), ∀ p : PrimeSpectrum A, p ∈ T →
      ((ModuleCat.localizedModuleFunctor.{max u v} p.asIdeal.primeCompl ⋙
        localCohomologyModuleFunctor (Localization p.asIdeal.primeCompl) (i : ℤ)).map
        ((idealPowerTower.{u, v} I M).map (homOfLE ((hm' m).trans _hbound)).op) = 0))
    (m : ℕ) :
    ∃ k : ℕ, ∃ h : m ≤ k,
      (localCohomologyWithSupportInModuleFunctor.{u, v} A T (i : ℤ)).map
        ((idealPowerTower.{u, v} I M).map (homOfLE h).op) = 0

Stacks.LocalCohomology.exists_eventually_injective_image_idealPowerTower_of_local, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/IdealPowerProZero.lean, line 228. The attribute's comment: “the stable-image assertion in degree s + 1, from the per-prime stable-image hypothesis taken as an explicit hypothesis; that per-prime hypothesis is the local-duality half of the source's proof and is not proved here”.

Stacks Project, Tag 0EFX, the stable-image assertion, globalized. If for every m there is a c ≥ m such that at every 𝔭 ∈ T and for every k ≥ c the transition map of {H^{i-1}_{𝔭A_𝔭}((IⁿM)_𝔭)} vanishes, the transition image of {H^i_{𝔭A_𝔭}((IⁿM)_𝔭)} is independent of k and that image injects into the zeroth term, then there is an m₀ such that for every m ≥ m₀ the image of H^i_T(IᵏM) → H^i_T(IᵐM) injects into H^i_T(I^{m₀}M) for all large k.

This is the reduction Lemma [Stacks, Tag 0EFA], applied to the tower {IⁿM}; in the source it is applied in degree i = s + 1. The per-prime hypothesis hloc is the local-duality half of the source's proof and is not proved here.

theorem exists_eventually_injective_image_idealPowerTower_of_local [IsNoetherianRing A]
    (hdim : ringKrullDim A < ⊤) (T : Set (PrimeSpectrum A)) (hT : StableUnderSpecialization T)
    (I : Ideal A) (M : ModuleCat.{max u v} A) (i : ℕ)
    (hloc : ∀ m : ℕ, ∃ c : ℕ, ∃ hmc : m ≤ c, ∀ p ∈ T, ∀ (k : ℕ) (hck : c ≤ k),
      ((idealPowerTower.{u, v} I M ⋙ ModuleCat.localizedModuleFunctor.{max u v}
        p.asIdeal.primeCompl ⋙ localCohomologyModuleFunctor
          (Localization p.asIdeal.primeCompl) ((i : ℤ) - 1)).map
            (homOfLE (hmc.trans hck)).op = 0) ∧
      (LinearMap.range ((idealPowerTower.{u, v} I M ⋙ ModuleCat.localizedModuleFunctor.{max u v}
          p.asIdeal.primeCompl ⋙ localCohomologyModuleFunctor
            (Localization p.asIdeal.primeCompl) (i : ℤ)).map (homOfLE (hmc.trans hck)).op).hom =
        LinearMap.range ((idealPowerTower.{u, v} I M ⋙ ModuleCat.localizedModuleFunctor.{max u v}
          p.asIdeal.primeCompl ⋙ localCohomologyModuleFunctor
            (Localization p.asIdeal.primeCompl) (i : ℤ)).map (homOfLE hmc).op).hom) ∧
      (∀ x : (idealPowerTower.{u, v} I M ⋙ ModuleCat.localizedModuleFunctor.{max u v}
          p.asIdeal.primeCompl ⋙ localCohomologyModuleFunctor
            (Localization p.asIdeal.primeCompl) (i : ℤ)).obj (op k),
        ((idealPowerTower.{u, v} I M ⋙ ModuleCat.localizedModuleFunctor.{max u v}
          p.asIdeal.primeCompl ⋙ localCohomologyModuleFunctor
            (Localization p.asIdeal.primeCompl) (i : ℤ)).map
              (homOfLE (hmc.trans hck)).op).hom x ∈
          LinearMap.ker ((idealPowerTower.{u, v} I M ⋙ ModuleCat.localizedModuleFunctor.{max u v}
            p.asIdeal.primeCompl ⋙ localCohomologyModuleFunctor
              (Localization p.asIdeal.primeCompl) (i : ℤ)).map
                (homOfLE (Nat.zero_le m)).op).hom →
        ((idealPowerTower.{u, v} I M ⋙ ModuleCat.localizedModuleFunctor.{max u v}
          p.asIdeal.primeCompl ⋙ localCohomologyModuleFunctor
            (Localization p.asIdeal.primeCompl) (i : ℤ)).map
              (homOfLE (hmc.trans hck)).op).hom x = 0)) :
    ∃ m₀ : ℕ, ∀ (m : ℕ) (hm₀m : m₀ ≤ m), ∃ c : ℕ, ∃ hmc : m ≤ c, ∀ (k : ℕ) (hck : c ≤ k),
      ∀ x : (idealPowerTower.{u, v} I M ⋙
          localCohomologyWithSupportInModuleFunctor.{u, v} A T (i : ℤ)).obj (op k),
        ((idealPowerTower.{u, v} I M ⋙
          localCohomologyWithSupportInModuleFunctor.{u, v} A T (i : ℤ)).map
            (homOfLE (hmc.trans hck)).op).hom x ∈
          LinearMap.ker ((idealPowerTower.{u, v} I M ⋙
            localCohomologyWithSupportInModuleFunctor.{u, v} A T (i : ℤ)).map
              (homOfLE hm₀m).op).hom →
        ((idealPowerTower.{u, v} I M ⋙
          localCohomologyWithSupportInModuleFunctor.{u, v} A T (i : ℤ)).map
            (homOfLE (hmc.trans hck)).op).hom x = 0

Stacks.LocalCohomology.exists_map_idealPowerTower_eq_zero_of_neg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/IdealPowerProZero.lean, line 275. The attribute's comment: “the pro-zero assertion in negative degrees, unconditionally”.

Stacks Project, Tag 0EFX in negative degrees, with no hypothesis. For i < 0 every term of {H^i_T(IⁿM)} vanishes, so every transition map is zero and the system is pro-zero.

theorem exists_map_idealPowerTower_eq_zero_of_neg (T : Set (PrimeSpectrum A)) (I : Ideal A)
    (M : ModuleCat.{max u v} A) (i : ℤ) (hi : i < 0) (m : ℕ) :
    ∃ k : ℕ, ∃ h : m ≤ k,
      (localCohomologyWithSupportInModuleFunctor.{u, v} A T i).map
        ((idealPowerTower.{u, v} I M).map (homOfLE h).op) = 0

Stacks.LocalCohomology.exists_eventually_injective_image_idealPowerTower_of_neg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/IdealPowerProZeroLowDegree.lean, line 188. The attribute's comment: “the stable-image assertion in negative degrees, unconditionally”.

Stacks Project, Tag 0EFX, the stable-image assertion, in negative degrees and with no hypothesis. The assertion is that there is an m₀ such that for every m ≥ m₀ there is a c ≥ m beyond which the image of H^i_T(IᵏM) → H^i_T(IᵐM) maps injectively to H^i_T(I^{m₀}M). For i < 0 every term H^i_T(IⁿM) of the system vanishes, so m₀ = 0 serves and the injectivity is automatic.

This is the companion of exists_map_idealPowerTower_eq_zero_of_neg, and it covers the degree s + 1 at which the source states the stable-image assertion exactly when s < -1. The conclusion is the conclusion of exists_eventually_injective_image_idealPowerTower_of_local verbatim, so the two theorems prove the same assertion in complementary ranges of the degree.

theorem exists_eventually_injective_image_idealPowerTower_of_neg (T : Set (PrimeSpectrum A))
    (I : Ideal A) (M : ModuleCat.{max u v} A) (i : ℤ) (hi : i < 0) :
    ∃ m₀ : ℕ, ∀ (m : ℕ) (hm₀m : m₀ ≤ m), ∃ c : ℕ, ∃ hmc : m ≤ c, ∀ (k : ℕ) (hck : c ≤ k),
      ∀ x : (idealPowerTower.{u, v} I M ⋙
          localCohomologyWithSupportInModuleFunctor.{u, v} A T i).obj (op k),
        ((idealPowerTower.{u, v} I M ⋙
          localCohomologyWithSupportInModuleFunctor.{u, v} A T i).map
            (homOfLE (hmc.trans hck)).op).hom x ∈
          LinearMap.ker ((idealPowerTower.{u, v} I M ⋙
            localCohomologyWithSupportInModuleFunctor.{u, v} A T i).map
              (homOfLE hm₀m).op).hom →
        ((idealPowerTower.{u, v} I M ⋙
          localCohomologyWithSupportInModuleFunctor.{u, v} A T i).map
            (homOfLE (hmc.trans hck)).op).hom x = 0

Stacks.LocalCohomology.exists_map_idealPowerTower_eq_zero_of_le_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/IdealPowerProZeroLowDegree.lean, line 296. The attribute's comment: “the pro-zero assertion in degrees i ≤ 0, for A Noetherian, M finite and T ⊆ V(I)”.

Stacks Project, Tag 0EFX, the pro-zero assertion in degrees i ≤ 0, with no hypothesis beyond the data of Situation [Stacks, Tag 0EFU]: A Noetherian, M finite and T ⊆ V(I). For i < 0 every term of {H^i_T(IⁿM)} vanishes; in degree 0 the terms vanish from some index on, by exists_isZero_localCohomologyWithSupportIn_idealPowerTower_zero. In either case a transition map out of a vanishing term is zero.

Together with the stable-image companion exists_eventually_injective_image_idealPowerTower_of_le_zero this proves both assertions of the tag whenever s < 0: the pro-zero assertion is asserted for i ≤ s and the stable-image assertion in degree s + 1.

theorem exists_map_idealPowerTower_eq_zero_of_le_zero [IsNoetherianRing A]
    (T : Set (PrimeSpectrum A)) (I : Ideal A)
    (hT : T ⊆ PrimeSpectrum.zeroLocus (I : Set A)) (M : ModuleCat.{max u v} A)
    [Module.Finite A M] (i : ℤ) (hi : i ≤ 0) (m : ℕ) :
    ∃ k : ℕ, ∃ h : m ≤ k,
      (localCohomologyWithSupportInModuleFunctor.{u, v} A T i).map
        ((idealPowerTower.{u, v} I M).map (homOfLE h).op) = 0

Stacks.LocalCohomology.exists_eventually_injective_image_idealPowerTower_of_le_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/IdealPowerProZeroLowDegree.lean, line 323. The attribute's comment: “the stable-image assertion in degrees i ≤ 0, for A Noetherian, M finite and T ⊆ V(I)”.

Stacks Project, Tag 0EFX, the stable-image assertion in degrees i ≤ 0, with no hypothesis beyond the data of Situation [Stacks, Tag 0EFU]: A Noetherian, M finite and T ⊆ V(I). The assertion is that there is an m₀ such that for every m ≥ m₀ there is a c ≥ m beyond which the image of H^i_T(IᵏM) → H^i_T(IᵐM) maps injectively to H^i_T(I^{m₀}M).

For i < 0 every term vanishes and m₀ = 0 serves. In degree 0 the terms vanish from the index c of exists_isZero_localCohomologyWithSupportIn_idealPowerTower_zero on, so m₀ = c serves: every class in a vanishing target is zero. The conclusion is the conclusion of exists_eventually_injective_image_idealPowerTower_of_local verbatim.

This covers the degree s + 1 at which the source states the stable-image assertion exactly when s < 0.

theorem exists_eventually_injective_image_idealPowerTower_of_le_zero [IsNoetherianRing A]
    (T : Set (PrimeSpectrum A)) (I : Ideal A)
    (hT : T ⊆ PrimeSpectrum.zeroLocus (I : Set A)) (M : ModuleCat.{max u v} A)
    [Module.Finite A M] (i : ℤ) (hi : i ≤ 0) :
    ∃ m₀ : ℕ, ∀ (m : ℕ) (hm₀m : m₀ ≤ m), ∃ c : ℕ, ∃ hmc : m ≤ c, ∀ (k : ℕ) (hck : c ≤ k),
      ∀ x : (idealPowerTower.{u, v} I M ⋙
          localCohomologyWithSupportInModuleFunctor.{u, v} A T i).obj (op k),
        ((idealPowerTower.{u, v} I M ⋙
          localCohomologyWithSupportInModuleFunctor.{u, v} A T i).map
            (homOfLE (hmc.trans hck)).op).hom x ∈
          LinearMap.ker ((idealPowerTower.{u, v} I M ⋙
            localCohomologyWithSupportInModuleFunctor.{u, v} A T i).map
              (homOfLE hm₀m).op).hom →
        ((idealPowerTower.{u, v} I M ⋙
          localCohomologyWithSupportInModuleFunctor.{u, v} A T i).map
            (homOfLE (hmc.trans hck)).op).hom x = 0

Tag 0EFY, a lemma

Tag 0EFY in the Stacks Project.

Stacks.Algebraization.isIso_localCohomologyAdicQuotientToLimit_closedPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapCanonicalAdicLimit.lean, line 140. The attribute's comment: “part (4) at T = {𝔪} over a Noetherian local ring in Situation 0EFU, read at the canonical comparison Hⁱ_𝔪(M) ⟶ lim Hⁱ_𝔪(M/IⁿM), in the range i ≤ s and with no completeness assumption on A”.

The canonical comparison Hⁱ_𝔪(M) ⟶ lim Hⁱ_𝔪(M/IⁿM) is an isomorphism for i ≤ s. In Situation [Stacks, Tag 0EFU] with A local and T = {𝔪}, with nothing assumed beyond the situation — in particular A need not be I-adically complete.

The map is Stacks.Algebraization.localCohomologyAdicQuotientToLimit, the limit comparison of the cone whose n-th leg is Hⁱ_𝔪 of the quotient map M ⟶ M/IⁿM. This is the isomorphism assertion of [Stacks, Tag 0EFR] read at that map, which is what a consumer reasoning about the individual projections needs; Stacks.Algebraization.localCohomologyToAdicQuotientLimit, the arrow Tag 0EFR is registered on, is instead built from an unpinned derived-limit witness.

This is also part (4) of [Stacks, Tag 0EFY] at T = {𝔪}, in the wider range i ≤ s that contains that part's range i < s. It improves the registration of that part carried by Stacks.Algebraization.isIso_localCohomologyToAdicQuotientLimit_of_isAdicComplete (StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapLocalCohomologyLimit.lean) in two ways: the I-adic completeness of A is not assumed, and the arrow is the canonical comparison. The source's T is an arbitrary specialization-stable subset of V(I); T = {𝔪} over a local ring is one such, and the general case rests on [Stacks, Tag 0EFX], whose state in the library is recorded in StacksFrontier/RingTheory/LocalCohomology/IdealPowerProZero.lean.

public theorem isIso_localCohomologyAdicQuotientToLimit_closedPoint
    [IsLocalRing S.A] (hT : S.T = {closedPoint S.A}) (i : ℤ) (hi : i ≤ S.s) :
    IsIso (localCohomologyAdicQuotientToLimit S.A S.I (maximalIdeal S.A)
      (Ideal.fg_of_isNoetherianRing _) (ModuleCat.of S.A S.M) i)

Stacks.Algebraization.injective_and_smul_mem_range_localCohomologyAdicQuotientToLimit_closedPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapCanonicalAdicLimit.lean, line 162. The attribute's comment: “part (6) at T = {𝔪} over a Noetherian local ring in Situation 0EFU: the canonical map Hˢ_𝔪(M) ⟶ lim Hˢ_𝔪(M/IⁿM) is injective and each element of I^{m₀} carries the limit into its image, for every m₀”.

Part (6) of [Stacks, Tag 0EFY] at T = {𝔪}. In Situation [Stacks, Tag 0EFU] with A local and T = {𝔪}, the canonical map Hˢ_𝔪(M) ⟶ lim Hˢ_𝔪(M/IⁿM) is injective, and every element of I^{m₀} carries an element of the limit into its image — that is, the cokernel is killed by I^{m₀}, for every m₀ whatsoever.

The part is immediate from isIso_localCohomologyAdicQuotientToLimit_closedPoint read in degree exactly s, which is inside the range i ≤ s of that theorem: the comparison is then an isomorphism, hence injective and surjective, so the cokernel is zero and m₀ plays no role. The source asserts the two halves separately because at a general specialization-stable T the comparison in the top degree s need not be surjective; what makes the top degree accessible here is that T = {𝔪} puts it inside the range of [Stacks, Tag 0EFR].

public theorem injective_and_smul_mem_range_localCohomologyAdicQuotientToLimit_closedPoint
    [IsLocalRing S.A] (hT : S.T = {closedPoint S.A}) (m₀ : ℕ) :
    Function.Injective (localCohomologyAdicQuotientToLimit S.A S.I (maximalIdeal S.A)
        (Ideal.fg_of_isNoetherianRing _) (ModuleCat.of S.A S.M) S.s).hom ∧
      ∀ a ∈ S.I ^ m₀, ∀ y, ∃ x, (localCohomologyAdicQuotientToLimit S.A S.I (maximalIdeal S.A)
        (Ideal.fg_of_isNoetherianRing _) (ModuleCat.of S.A S.M) S.s).hom x = a • y

Stacks.Algebraization.exists_forall_injective_localCohomologyAdicQuotientMap_closedPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapCanonicalAdicLimit.lean, line 195. The attribute's comment: “part (1) at T = {𝔪} over a Noetherian local ring in Situation 0EFU: a single m₀ beyond which Hⁱ_𝔪(M) ⟶ Hⁱ_𝔪(M/IⁿM) is injective for every i ≤ s at once”.

Part (1) of [Stacks, Tag 0EFY] at T = {𝔪}, with nothing assumed beyond Situation [Stacks, Tag 0EFU]. There is an integer m₀ such that the canonical map Hⁱ_𝔪(M) ⟶ Hⁱ_𝔪(M/IⁿM) is injective for every i ≤ s and every n ≥ m₀.

The kernels of the canonical maps form a descending chain in the Artinian module Hⁱ_𝔪(M) whose intersection is the kernel of the canonical comparison to the limit, and that comparison is injective by isIso_localCohomologyAdicQuotientToLimit_closedPoint; so the chain reaches 0. The pinned derived-limit presentation that argument consumes is Dualizing.isDerivedLimitWithProjections_completedLocalCohomologyProjection_of_finite.

This improves exists_forall_injective_homology_localCohomologyAdicQuotientMap_of_eq_closedPoint of StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapAdicProjectionInjectivity.lean by dropping both its [IsAdicComplete] instance and its hproj hypothesis.

The source's T is an arbitrary specialization-stable subset of V(I); T = {𝔪} over a local ring is one such, and the general case rests on the pro-zero assertion of [Stacks, Tag 0EFX], whose state in the library is recorded in StacksFrontier/RingTheory/LocalCohomology/IdealPowerProZero.lean.

public theorem exists_forall_injective_localCohomologyAdicQuotientMap_closedPoint
    [IsLocalRing S.A] (hT : S.T = {closedPoint S.A}) :
    ∃ m₀ : ℕ, ∀ i : ℤ, i ≤ S.s → ∀ n : ℕ, m₀ ≤ n →
      Function.Injective ((DerivedCategory.homologyFunctor (ModuleCat.{u} S.A) i).map
        (Dualizing.localCohomologyAdicQuotientMap S.A S.I (maximalIdeal S.A)
          (Ideal.fg_of_isNoetherianRing _) (ModuleCat.of S.A S.M) n)).hom

Stacks.Algebraization.exists_smul_id_firstDerivedLimitLocalCohomologyAdicTower_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapFirstDerivedLimitAnnihilation.lean, line 148. The attribute's comment: “part (7) at a general specialization-stable T in Situation 0EFU: I^{m₀} annihilates R¹lim Hˢ_T(M/IⁿM)”.

In Situation [Stacks, Tag 0EFU], at a general specialization-stable T, there is an integer m₀ such that every element of I^{m₀} annihilates R¹lim H^s_T(M/IⁿM).

theorem exists_smul_id_firstDerivedLimitLocalCohomologyAdicTower_eq_zero
    (S : BootstrapSituation.{u, u, u}) :
    ∃ m₀ : ℕ, ∀ a ∈ S.I ^ m₀,
      a • 𝟙 (firstDerivedLimitLocalCohomologyAdicTower.{u, u} S.T S.I
        (ModuleCat.of S.A S.M) S.s) = 0

Stacks.Algebraization.exists_bound_adicLocalCohomologyComparisons, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapFirstDerivedLimitAnnihilation.lean, line 172.

At a general specialization-stable T, in Situation [Stacks, Tag 0EFU] there is an integer m₀ ≥ 0 such that

1. H^i_T(M) ⟶ H^i_T(M/IⁿM) is injective for all i ≤ s and n ≥ m₀;
2. {H^i_T(M/IⁿM)} satisfies the Mittag-Leffler condition for i < s;
3. {H^i_T(I^{m₀}M/I^{n+m₀}M)} satisfies the Mittag-Leffler condition for i ≤ s;
4. H^i_T(M) ⟶ lim H^i_T(M/IⁿM) is an isomorphism for i < s;
5. H^s_T(I^{m₀}M) ⟶ lim H^s_T(I^{m₀}M/I^{n+m₀}M) is an isomorphism;
6. H^s_T(M) ⟶ lim H^s_T(M/IⁿM) is injective with cokernel killed by I^{m₀}; and
7. R¹lim H^s_T(M/IⁿM) is killed by I^{m₀}.

Parts (3) and (5) are the source's statements for the subquotients I^{m₀}M/IⁿM, n ≥ m₀, read along the cofinal shift n ↦ n + m₀, the n-th term of the tower of adic quotients of I^{m₀}M being I^{m₀}M/I^{n+m₀}M (Stacks.Algebraization.map_subtype_pow_smul_top); the limits and the transition maps are the same.

theorem exists_bound_adicLocalCohomologyComparisons (S : BootstrapSituation.{u, u, u}) :
    ∃ m₀ : ℕ,
      (∀ i ≤ S.s, ∀ n : ℕ, m₀ ≤ n →
        Function.Injective ((localCohomologyAdicCone.{u, u} S.A S.T S.I i
          (ModuleCat.of S.A S.M)).π.app (op n)).hom) ∧
      (∀ i : ℤ, i + 1 ≤ S.s → IsMittagLefflerCategorical
        (localCohomologyAdicTower.{u, u} S.A S.T S.I i (ModuleCat.of S.A S.M))) ∧
      (∀ i ≤ S.s, IsMittagLefflerCategorical (localCohomologyAdicTower.{u, u} S.A S.T S.I i
        (ModuleCat.of S.A ↥(S.I ^ m₀ • (⊤ : Submodule S.A S.M))))) ∧
      (∀ i : ℤ, i + 1 ≤ S.s → IsIso (limit.lift
        (localCohomologyAdicTower.{u, u} S.A S.T S.I i (ModuleCat.of S.A S.M))
        (localCohomologyAdicCone.{u, u} S.A S.T S.I i (ModuleCat.of S.A S.M)))) ∧
      IsIso (limit.lift
        (localCohomologyAdicTower.{u, u} S.A S.T S.I S.s
          (ModuleCat.of S.A ↥(S.I ^ m₀ • (⊤ : Submodule S.A S.M))))
        (localCohomologyAdicCone.{u, u} S.A S.T S.I S.s
          (ModuleCat.of S.A ↥(S.I ^ m₀ • (⊤ : Submodule S.A S.M))))) ∧
      (Function.Injective (limit.lift
          (localCohomologyAdicTower.{u, u} S.A S.T S.I S.s (ModuleCat.of S.A S.M))
          (localCohomologyAdicCone.{u, u} S.A S.T S.I S.s (ModuleCat.of S.A S.M))).hom ∧
        ∀ a ∈ S.I ^ m₀, ∀ z : (limit (localCohomologyAdicTower.{u, u} S.A S.T S.I S.s
            (ModuleCat.of S.A S.M)) : ModuleCat.{u} S.A),
          a • z ∈ LinearMap.range (limit.lift
            (localCohomologyAdicTower.{u, u} S.A S.T S.I S.s (ModuleCat.of S.A S.M))
            (localCohomologyAdicCone.{u, u} S.A S.T S.I S.s (ModuleCat.of S.A S.M))).hom) ∧
      (∀ a ∈ S.I ^ m₀, a • 𝟙 (firstDerivedLimitLocalCohomologyAdicTower.{u, u} S.T S.I
        (ModuleCat.of S.A S.M) S.s) = 0)

Stacks.Algebraization.exists_forall_injective_and_isIso_limitLift_localCohomologyAdicCone_closedPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapIdealPowerAdicLimit.lean, line 135. The attribute's comment: “part (5) at T = {𝔪} over a Noetherian local ring in Situation 0EFU, at the very m₀ that part (1) produces: Hˢ_𝔪(I^{m₀}M) ⟶ lim Hˢ_𝔪(I^{m₀}M/IⁿM) is an isomorphism”.

Parts (1) and (5) of [Stacks, Tag 0EFY] at T = {𝔪}, at one and the same m₀. In Situation [Stacks, Tag 0EFU] with A local and T = {𝔪}, there is an integer m₀ such that

• Hⁱ_𝔪(M) ⟶ Hⁱ_𝔪(M/IⁿM) is injective for every i ≤ s and every n ≥ m₀ — part (1); and
• Hˢ_𝔪(I^{m₀}M) ⟶ lim_n Hˢ_𝔪(I^{m₀}M/IⁿM) is an isomorphism — part (5), at that m₀.

The second item is the statement of part (5) read for the module I^{m₀}M: the n-th term of its tower of adic quotients is I^{m₀}M/I^{n+m₀}M (Stacks.Algebraization.map_subtype_pow_smul_top), so the tower is the source's system {I^{m₀}M/IⁿM}_{n ≥ m₀} along the cofinal shift n ↦ n + m₀ and the limits agree.

Nothing beyond the situation is assumed; in particular A need not be I-adically complete. Part (1) comes from the pro-zero assertion of [Stacks, Tag 0EFX] at this locus through Stacks.LocalCohomology.exists_forall_injective_localCohomologyAdicProjection_of_proZero, and part (5) holds at that m₀ because isIso_limitLift_localCohomologyAdicCone_idealPowerSubmodule_closedPoint proves it for every exponent, the situation being stable under M ↦ IᵏM.

The source's T is an arbitrary specialization-stable subset of V(I), and the general case rests on [Stacks, Tag 0EFX] for that T, which is proved in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapUniformStableImage.lean; parts (1), (3) and (5) at a general locus, at one and the same m₀, are Stacks.Algebraization.exists_forall_injective_and_isMittagLeffler_and_isIso_limitLift.

public theorem exists_forall_injective_and_isIso_limitLift_localCohomologyAdicCone_closedPoint
    [IsLocalRing S.A] (hT : S.T = {closedPoint S.A}) :
    ∃ m₀ : ℕ,
      (∀ i ≤ S.s, ∀ n : ℕ, m₀ ≤ n →
        Function.Injective ((localCohomologyAdicCone.{u, u} S.A S.T S.I i
          (ModuleCat.of S.A S.M)).π.app (op n)).hom) ∧
      IsIso (limit.lift
        (localCohomologyAdicTower.{u, u} S.A S.T S.I S.s
          (ModuleCat.of S.A ↥(S.I ^ m₀ • (⊤ : Submodule S.A S.M))))
        (localCohomologyAdicCone.{u, u} S.A S.T S.I S.s
          (ModuleCat.of S.A ↥(S.I ^ m₀ • (⊤ : Submodule S.A S.M)))))

Stacks.Algebraization.isIso_localCohomologyToAdicQuotientLimit_of_isAdicComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapLocalCohomologyLimit.lean, line 341. The attribute's comment: “part (4) at T = {𝔪} over an I-adically complete Noetherian local ring in Situation 0EFU: Hⁱ_𝔪(M) ⟶ lim Hⁱ_𝔪(M/IⁿM) is an isomorphism, in the range i ≤ s, which contains the range i < s of that part”.

In the bootstrap situation of Stacks 0EFU with A local, I-adically complete and T = {𝔪}, the map Hⁱ_𝔪(M) ⟶ lim Hⁱ_𝔪(M/IⁿM) is an isomorphism for i ≤ s and a single power of I annihilates these modules.

public theorem isIso_localCohomologyToAdicQuotientLimit_of_isAdicComplete
    [IsLocalRing S.A] [IsAdicComplete S.I S.A] (hT : S.T = {closedPoint S.A}) :
    (∀ i : ℤ, i ≤ S.s →
        IsIso (localCohomologyToAdicQuotientLimit S.A S.I (maximalIdeal S.A)
          (maximalIdeal S.A) (ModuleCat.of S.A S.M) rfl i)) ∧
      ∃ n : ℕ, ∀ i : ℤ, i ≤ S.s →
        S.I ^ n ≤ Module.annihilator S.A
          (Stacks.LocalCohomology.localCohomologyModule S.A (maximalIdeal S.A)
            (Ideal.fg_of_isNoetherianRing _) (ModuleCat.of S.A S.M) i)

Stacks.Algebraization.exists_forall_injective_and_isMittagLeffler_and_isIso_limitLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapStableImageShift.lean, line 254. The attribute's comment: “parts (1), (3) and (5) at a general specialization-stable T in Situation 0EFU, at one and the same m₀: the projections are injective from m₀ on, {Hⁱ_T(I^{m₀}M/IⁿM)} is Mittag-Leffler for i ≤ s, and Hˢ_T(I^{m₀}M) ⟶ lim Hˢ_T(I^{m₀}M/IⁿM) is an isomorphism”.

Stacks Project, Tag 0EFY, parts (1), (3) and (5), at a general specialization-stable T, at one and the same m₀. In Situation [Stacks, Tag 0EFU] there is an integer m₀ such that

• H^i_T(M) ⟶ H^i_T(M/IⁿM) is injective for every i ≤ s and every n ≥ m₀ — part (1);
• {H^i_T(I^{m₀}M/I^{n+m₀}M)} satisfies the Mittag-Leffler condition for every i ≤ s — part (3), at that m₀; and
• H^s_T(I^{m₀}M) ⟶ lim_n H^s_T(I^{m₀}M/I^{n+m₀}M) is an isomorphism — part (5), at that m₀.

The last two items are the source's statements for the module I^{m₀}M: the n-th term of its tower of adic quotients is I^{m₀}M/I^{n+m₀}M (Stacks.Algebraization.map_subtype_pow_smul_top), so the tower is the source's system {I^{m₀}M/IⁿM}_{n ≥ m₀} along the cofinal shift n ↦ n + m₀ and the limits agree — the reading the registrants at T = {𝔪} use as well.

Stating the three at a common m₀ matters: ∃ m₀, part (5) at m₀ alone is satisfiable at m₀ = 0, where part (5) degenerates into part (4) read in degree s. The m₀ exhibited here is a bound for part (1) and for the base of the stable-image assertion of [Stacks, Tag 0EFX] simultaneously. Nothing beyond the data of Situation [Stacks, Tag 0EFU] is assumed.

theorem exists_forall_injective_and_isMittagLeffler_and_isIso_limitLift :
    ∃ m₀ : ℕ,
      (∀ i ≤ S.s, ∀ n : ℕ, m₀ ≤ n →
        Function.Injective ((localCohomologyAdicCone.{u, u} S.A S.T S.I i
          (ModuleCat.of S.A S.M)).π.app (op n)).hom) ∧
      (∀ i ≤ S.s, IsMittagLefflerCategorical (localCohomologyAdicTower.{u, u} S.A S.T S.I i
        (ModuleCat.of S.A ↥(S.I ^ m₀ • (⊤ : Submodule S.A S.M))))) ∧
      IsIso (limit.lift
        (localCohomologyAdicTower.{u, u} S.A S.T S.I S.s
          (ModuleCat.of S.A ↥(S.I ^ m₀ • (⊤ : Submodule S.A S.M))))
        (localCohomologyAdicCone.{u, u} S.A S.T S.I S.s
          (ModuleCat.of S.A ↥(S.I ^ m₀ • (⊤ : Submodule S.A S.M)))))

Stacks.Algebraization.exists_forall_injective_localCohomologyAdicProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapUniformProZero.lean, line 323. The attribute's comment: “part (1) at a general specialization-stable T in Situation 0EFU: one m₀ beyond which Hⁱ_T(M) ⟶ Hⁱ_T(M/IⁿM) is injective for every i ≤ s”.

Stacks Project, Tag 0EFY, part (1), at a general specialization-stable T. In Situation [Stacks, Tag 0EFU] there is an m₀ such that H^i_T(M) ⟶ H^i_T(M/IⁿM) is injective for every i ≤ s and every n ≥ m₀.

This is Stacks.LocalCohomology.exists_forall_injective_localCohomologyAdicProjection_of_proZero with its hypothesis discharged by Stacks.Algebraization.isProZeroIdealPowerCohomology.

theorem exists_forall_injective_localCohomologyAdicProjection
    (S : BootstrapSituation.{u, u, u}) :
    ∃ m₀ : ℕ, ∀ i ≤ S.s, ∀ n : ℕ, m₀ ≤ n →
      Function.Injective ((localCohomologyAdicCone.{u, u} S.A S.T S.I i
        (ModuleCat.of S.A S.M)).π.app (op n)).hom

Stacks.Algebraization.isMittagLefflerCategorical_localCohomologyAdicTower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapUniformProZero.lean, line 340. The attribute's comment: “part (2) at a general specialization-stable T in Situation 0EFU: the Mittag-Leffler condition for {Hⁱ_T(M/IⁿM)} in every degree i < s”.

Stacks Project, Tag 0EFY, part (2), at a general specialization-stable T. In Situation [Stacks, Tag 0EFU] the inverse system {H^i_T(M/IⁿM)} satisfies the Mittag-Leffler condition for i < s.

This is Stacks.LocalCohomology.isMittagLefflerCategorical_localCohomologyAdicTower_of_proZero with its hypothesis — pro-zero-ness in degree i + 1, which is ≤ s exactly when i < s — discharged by Stacks.Algebraization.isProZeroIdealPowerCohomology.

theorem isMittagLefflerCategorical_localCohomologyAdicTower
    (S : BootstrapSituation.{u, u, u}) (i : ℤ) (hi : i + 1 ≤ S.s) :
    IsMittagLefflerCategorical (localCohomologyAdicTower.{u, u} S.A S.T S.I i
      (ModuleCat.of S.A S.M))

Stacks.Algebraization.isIso_limitLift_localCohomologyAdicCone, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapUniformProZero.lean, line 356. The attribute's comment: “part (4) at a general specialization-stable T in Situation 0EFU: Hⁱ_T(M) ⟶ lim Hⁱ_T(M/IⁿM) is an isomorphism in every degree i < s”.

Stacks Project, Tag 0EFY, part (4), at a general specialization-stable T. In Situation [Stacks, Tag 0EFU] the canonical map H^i_T(M) ⟶ lim H^i_T(M/IⁿM) is an isomorphism for i < s.

This is Stacks.LocalCohomology.isIso_limitLift_localCohomologyAdicCone_of_proZero with both of its hypotheses — pro-zero-ness in degrees i and i + 1, both ≤ s exactly when i < s — discharged by Stacks.Algebraization.isProZeroIdealPowerCohomology.

theorem isIso_limitLift_localCohomologyAdicCone
    (S : BootstrapSituation.{u, u, u}) (i : ℤ) (hi : i + 1 ≤ S.s) :
    IsIso (limit.lift (localCohomologyAdicTower.{u, u} S.A S.T S.I i (ModuleCat.of S.A S.M))
      (localCohomologyAdicCone.{u, u} S.A S.T S.I i (ModuleCat.of S.A S.M)))

Stacks.Algebraization.exists_injective_limitLift_and_smul_mem_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapUniformStableImage.lean, line 326. The attribute's comment: “part (6) at a general specialization-stable T in Situation 0EFU: Hˢ_T(M) ⟶ lim Hˢ_T(M/IⁿM) is injective with cokernel killed by I^{m₀}”.

Stacks Project, Tag 0EFY, part (6), at a general specialization-stable T. In Situation [Stacks, Tag 0EFU] there is an m₀ such that H^s_T(M) ⟶ lim H^s_T(M/IⁿM) is injective with cokernel killed by I^{m₀}.

This is Stacks.LocalCohomology.exists_injective_limitLift_and_smul_mem_range with both of its hypotheses — the two assertions of [Stacks, Tag 0EFX] — discharged by Stacks.Algebraization.isProZeroIdealPowerCohomology and Stacks.Algebraization.exists_hasStableImageIdealPowerCohomology.

theorem exists_injective_limitLift_and_smul_mem_range (S : BootstrapSituation.{u, u, u}) :
    ∃ m₀ : ℕ,
      Function.Injective (limit.lift
          (localCohomologyAdicTower.{u, u} S.A S.T S.I S.s (ModuleCat.of S.A S.M))
          (localCohomologyAdicCone.{u, u} S.A S.T S.I S.s (ModuleCat.of S.A S.M))).hom ∧
        ∀ a ∈ S.I ^ m₀, ∀ z : (limit (localCohomologyAdicTower.{u, u} S.A S.T S.I S.s
            (ModuleCat.of S.A S.M)) : ModuleCat.{u} S.A),
          a • z ∈ LinearMap.range (limit.lift
            (localCohomologyAdicTower.{u, u} S.A S.T S.I S.s (ModuleCat.of S.A S.M))
            (localCohomologyAdicCone.{u, u} S.A S.T S.I S.s (ModuleCat.of S.A S.M))).hom

Stacks.LocalCohomology.isMittagLefflerCategorical_homologyAdicQuotientLocalCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/CompletedLimitComparison.lean, line 106. The attribute's comment: “part (2) at T = {𝔪} over a Noetherian local ring, in every degree”.

The local cohomology of the adic quotients of a finite module is Mittag-Leffler. For a finite module M over a Noetherian local ring, the inverse system n ↦ Hⁱ_𝔪(M/IⁿM) satisfies the Mittag-Leffler condition, since each M/IⁿM is again a finite module.

This is part (2) of [Stacks, Tag 0EFY] at the support T = {𝔪} of a Noetherian local ring. In that case it holds in every degree and draws nothing from Situation [Stacks, Tag 0EFU]: local cohomology at 𝔪 of a finite module over a Noetherian local ring is Artinian, and a descending chain of submodules of an Artinian module stabilizes, which is the Mittag-Leffler condition. A general specialization-stable T ⊆ V(I) lies beyond that argument, the modules Hⁱ_T(M/IⁿM) being in general neither finite nor Artinian; the source obtains part (2) there from the pro-zero assertion of [Stacks, Tag 0EFX] instead.

theorem isMittagLefflerCategorical_homologyAdicQuotientLocalCohomology
    [IsLocalRing A] [IsNoetherianRing A] (I : Ideal A) (M : ModuleCat.{u} A)
    [Module.Finite A M] (i : ℤ) :
    IsMittagLefflerCategorical
      (Dualizing.adicQuotientLocalCohomologySystem A I (IsLocalRing.maximalIdeal A)
          (IsLocalRing.maximalIdeal A).fg_of_isNoetherianRing M ⋙
        DerivedCategory.homologyFunctor (ModuleCat.{u} A) i)

Stacks.LocalCohomology.isMittagLefflerCategorical_homologyAdicQuotientLocalCohomology_smul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/CompletedLimitComparison.lean, line 128. The attribute's comment: “part (3) at T = {𝔪} over a Noetherian local ring, for the submodule IᵏM”.

Part (3) of [Stacks, Tag 0EFY] at the support T = {𝔪}. For a finite module M over a Noetherian local ring, an ideal I and a k : ℕ, the inverse system n ↦ Hⁱ_𝔪(IᵏM/Iⁿ⁺ᵏM) of the local cohomologies of the adic quotients of the submodule IᵏM satisfies the Mittag-Leffler condition, in every degree.

The source indexes that system by n ≥ k and writes its terms Hⁱ_𝔪(IᵏM/IⁿM); the index here runs over all of ℕ instead, which replaces IⁿM by Iⁿ(IᵏM) = Iⁿ⁺ᵏM and so gives the same family of modules and the same transition maps, read along the cofinal shift n ↦ n + k.

IᵏM is a submodule of a finite module over a Noetherian ring, hence itself finite, so this is isMittagLefflerCategorical_homologyAdicQuotientLocalCohomology applied to it.

theorem isMittagLefflerCategorical_homologyAdicQuotientLocalCohomology_smul
    [IsLocalRing A] [IsNoetherianRing A] (I : Ideal A) (M : ModuleCat.{u} A)
    [Module.Finite A M] (k : ℕ) (i : ℤ) :
    IsMittagLefflerCategorical
      (Dualizing.adicQuotientLocalCohomologySystem A I (IsLocalRing.maximalIdeal A)
          (IsLocalRing.maximalIdeal A).fg_of_isNoetherianRing
          (ModuleCat.of A ↥(I ^ k • (⊤ : Submodule A M))) ⋙
        DerivedCategory.homologyFunctor (ModuleCat.{u} A) i)

Stacks.LocalCohomology.smul_id_firstDerivedLimitLocalCohomologyAdicTower_eq_zero_closedPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/IdealPowerFirstDerivedLimit.lean, line 408. The attribute's comment: “part (7) at T = {𝔪} over a Noetherian local ring: I^{m₀} annihilates R¹lim Hˢ_𝔪(M/IⁿM), for every m₀ and in every degree”.

Part (7) of [Stacks, Tag 0EFY] at T = {𝔪} over a Noetherian local ring. Every element of I^{m₀} annihilates R¹lim H^s_𝔪(M/IⁿM), for every m₀ and every degree s.

The system {H^s_𝔪(M/IⁿM)} is itself Mittag-Leffler here, by isMittagLefflerCategorical_localCohomologyAdicTower_closedPoint, so its Milnor difference is an epimorphism and the first derived inverse limit — the cokernel of that difference — vanishes outright; annihilation by I^{m₀} follows for every m₀, and the degree plays no role either.

That is a stronger conclusion than the part asserts, and it is available only because of the locus: over a Noetherian local ring with T = {𝔪} the modules H^s_𝔪(M/IⁿM) are Artinian. At a general specialization-stable T they are neither finite nor Artinian, the source obtains the Mittag-Leffler condition only for the subsystem Aₙ of part (3), and the content of part (7) is then genuinely the annihilation and not a vanishing; that route is smul_id_firstDerivedLimitLocalCohomologyAdicTower_eq_zero_of_isMittagLeffler above, run on Stacks.LocalCohomology.isMittagLefflerCategorical_adicTowerCollapseKernelTower_of_stableImage.

theorem smul_id_firstDerivedLimitLocalCohomologyAdicTower_eq_zero_closedPoint (A : Type u)
    [CommRing A] [IsLocalRing A] [IsNoetherianRing A] (J : Ideal A) (N : ModuleCat.{u} A)
    [Module.Finite A N] (i : ℤ) (m₀ : ℕ) {a : A} (ha : a ∈ J ^ m₀) :
    a • 𝟙 (firstDerivedLimitLocalCohomologyAdicTower.{u, u}
      {IsLocalRing.closedPoint A} J N i) = 0

Stacks.LocalCohomology.exists_forall_injective_localCohomologyAdicProjection_of_proZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/IdealPowerProZero.lean, line 339. The attribute's comment: “part (1): the injectivity of H^i_T(M) → H^i_T(M/I^nM) for i ≤ s and n ≫ 0, derived from the pro-zero assertion of Lemma 0EFX taken as an explicit hypothesis; that assertion is not proved here”.

Stacks Project, Tag 0EFY, part (1). There is an integer m₀ such that H^i_T(M) → H^i_T(M/IⁿM) is injective for all i ≤ s and all n ≥ m₀.

Argument. Fix i ≤ s. By the pro-zero assertion of Tag 0EFX there are k and a transition map IᵏM → M of the tower {IⁿM} with vanishing H^i_T; since IⁿM ⊆ M factors through IᵏM for n ≥ k, the map H^i_T(IⁿM) → H^i_T(M) is then zero for every n ≥ k, and the long exact sequence of 0 → IⁿM → M → M/IⁿM → 0 makes H^i_T(M) → H^i_T(M/IⁿM) injective. A single m₀ serving every i ≤ s is the supremum of the finitely many k for 0 ≤ i ≤ s, together with the vanishing of H^i_T in negative degrees.

Only the pro-zero assertion of Tag 0EFX is used, and it is a hypothesis here; it is not proved in the library.

theorem exists_forall_injective_localCohomologyAdicProjection_of_proZero
    (T : Set (PrimeSpectrum A)) (I : Ideal A) (M : ModuleCat.{max u v} A) (s : ℤ)
    (hpro : ∀ i ≤ s, ∃ k : ℕ, ∃ h : 0 ≤ k,
      (localCohomologyWithSupportInModuleFunctor.{u, v} A T i).map
        ((idealPowerTower.{u, v} I M).map (homOfLE h).op) = 0) :
    ∃ m₀ : ℕ, ∀ i ≤ s, ∀ n : ℕ, m₀ ≤ n →
      Function.Injective ((localCohomologyAdicCone.{u, v} A T I i M).π.app (op n)).hom

Tag 0EIE, a theorem

Tag 0EIE in the Stacks Project.

Stacks.LocalCohomology.Bootstrap.essentiallyConstant_and_consequences, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/EssentiallyConstantBootstrap.lean, line 66.

Stacks Project, Tag 0EIE. In Situation 0EFU, for i ≤ s the inverse system {H^i_T(M/IⁿM)}_{n ≥ 0} is essentially constant with value H^i_T(M) (with respect to the cone of the maps H^i_T(M) → H^i_T(M/IⁿM) induced by the quotient maps). In particular it is Mittag-Leffler, H^i_T(M) is annihilated by a power of I, and the canonical maps exhibit H^i_T(M) as lim H^i_T(M/IⁿM).

theorem essentiallyConstant_and_consequences (S : BootstrapSituation.{u, u, w}) (i : ℤ)
    (hi : i ≤ S.s) :
    (∃ (j : ℕᵒᵖ) (σ : (tower.{u, u} S i).obj j ⟶ (cone.{u, u} S i).pt),
        EssentiallyConstantPro.IsEssentiallyConstantWith (tower.{u, u} S i) (cone.{u, u} S i)
          j σ) ∧
      IsMittagLefflerCategorical (tower.{u, u} S i) ∧
      (∃ n : ℕ, ∀ a ∈ S.I ^ n,
        ∀ x : (localCohomologyWithSupportInModuleFunctor.{u, u} S.A S.T i).obj
          (ModuleCat.of S.A S.M), a • x = 0) ∧
      Nonempty (IsLimit (cone.{u, u} S i))

Stacks.LocalCohomology.isEssentiallyConstantWith_localCohomologyAdicCone_of_neg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/EssentiallyConstantConsequences.lean, line 464. The attribute's comment: “the negative-degree range, unconditionally: for i < 0 the system is essentially constant with value H^i_T(M) = 0”.

Stacks Project, Tag 0EIE in negative degrees, with no hypothesis. For i < 0 the system {H^i_T(M/IⁿM)} is essentially constant with value H^i_T(M): local cohomology with support in T of a module vanishes in negative degrees (Stacks.LocalCohomology.isZero_localCohomologyWithSupportIn_single_of_neg), so every term of the system and the value are zero and the zero morphism is a witness. The three consequences in this range follow by composing with the implications above.

theorem isEssentiallyConstantWith_localCohomologyAdicCone_of_neg (I : Ideal A) (i : ℤ)
    (hi : i < 0) (M : ModuleCat.{max u v} A) :
    EssentiallyConstantPro.IsEssentiallyConstantWith
      (localCohomologyAdicTower.{u, v} A T I i M) (localCohomologyAdicCone.{u, v} A T I i M)
      (op 0) 0

Stacks.LocalCohomology.exists_isEssentiallyConstantWith_localCohomologyAdicCone_of_pow_smul_top_eq_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/EssentiallyConstantConsequences.lean, line 490. The attribute's comment: “the range where I acts nilpotently on M: if I^N M = 0 then in every degree the system is essentially constant with value H^i_T(M), for an arbitrary ring, subset of the spectrum and module”.

Stacks Project, Tag 0EIE when I acts nilpotently on M, with no hypothesis and in every degree. If IᴺM = 0 then the quotient maps M → M/IᵐM are isomorphisms for every m ≥ N, hence so are their images under H^i_T, and a cone whose projections are invertible from an index on carries essential-constancy data (CategoryTheory.EssentiallyConstantPro.exists_isEssentiallyConstantWith_of_isIso_π). The three consequences in this range follow by composing with the implications above.

No Noetherian, finiteness or support hypothesis is used: A is an arbitrary commutative ring, T an arbitrary subset of its spectrum and M an arbitrary module.

theorem exists_isEssentiallyConstantWith_localCohomologyAdicCone_of_pow_smul_top_eq_bot
    (I : Ideal A) (i : ℤ) (M : ModuleCat.{max u v} A) {N : ℕ}
    (hN : I ^ N • (⊤ : Submodule A M) = ⊥) :
    ∃ (j : ℕᵒᵖ) (σ : (localCohomologyAdicTower.{u, v} A T I i M).obj j ⟶
        (localCohomologyAdicCone.{u, v} A T I i M).pt),
      EssentiallyConstantPro.IsEssentiallyConstantWith
        (localCohomologyAdicTower.{u, v} A T I i M) (localCohomologyAdicCone.{u, v} A T I i M)
        j σ

Stacks.LocalCohomology.Bootstrap.isEssentiallyConstantWith_of_depthBound_neg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/EssentiallyConstantConsequences.lean, line 673. The attribute's comment: “the essential-constancy assertion, and with it the four consequences, for a bootstrap situation whose depth bound s is negative”.

Stacks Project, Tag 0EIE for a bootstrap situation whose depth bound is negative. Every degree i ≤ s < 0 is negative, so each term of {H^i_T(M/IⁿM)} and the value H^i_T(M) vanish and the zero morphism witnesses essential constancy with value H^i_T(M). The four consequences above apply to this witness, and so hold with no hypothesis in this range.

theorem isEssentiallyConstantWith_of_depthBound_neg (hs : S.s < 0) (hi : i ≤ S.s) :
    EssentiallyConstantPro.IsEssentiallyConstantWith
      (tower.{u, v} S i) (cone.{u, v} S i) (op 0) 0

Stacks.LocalCohomology.Bootstrap.exists_isEssentiallyConstantWith_of_pow_smul_top_eq_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/EssentiallyConstantConsequences.lean, line 685. The attribute's comment: “the essential-constancy assertion for a bootstrap situation in which I acts nilpotently on M, with no hypothesis and in every degree”.

Stacks Project, Tag 0EIE for a bootstrap situation in which I acts nilpotently on M, with no hypothesis and in every degree. The quotient maps M → M/IᵐM are isomorphisms from the nilpotency exponent on, so the canonical cone's projections are, and a cone whose projections are invertible from an index on carries essential-constancy data.

theorem exists_isEssentiallyConstantWith_of_pow_smul_top_eq_bot {N : ℕ}
    (hN : S.I ^ N • (⊤ : Submodule S.A S.M) = ⊥) :
    ∃ (j : ℕᵒᵖ) (σ : (tower.{u, v} S i).obj j ⟶ (cone.{u, v} S i).pt),
      EssentiallyConstantPro.IsEssentiallyConstantWith
        (tower.{u, v} S i) (cone.{u, v} S i) j σ

Stacks.LocalCohomology.Bootstrap.isMittagLeffler_of_pow_smul_top_eq_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/EssentiallyConstantConsequences.lean, line 697. The attribute's comment: “the Mittag-Leffler consequence for a bootstrap situation in which I acts nilpotently on M, with no hypothesis and in every degree”.

Stacks Project, Tag 0EIE, the Mittag-Leffler consequence for a bootstrap situation in which I acts nilpotently on M, with no hypothesis and in every degree.

theorem isMittagLeffler_of_pow_smul_top_eq_bot {N : ℕ}
    (hN : S.I ^ N • (⊤ : Submodule S.A S.M) = ⊥) :
    IsMittagLefflerCategorical (tower.{u, v} S i)

Stacks.LocalCohomology.Bootstrap.exists_pow_smul_eq_zero_of_pow_smul_top_eq_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/EssentiallyConstantConsequences.lean, line 707. The attribute's comment: “the annihilation consequence for a bootstrap situation in which I acts nilpotently on M, with no hypothesis and in every degree”.

Stacks Project, Tag 0EIE, the annihilation consequence for a bootstrap situation in which I acts nilpotently on M, with no hypothesis and in every degree.

theorem exists_pow_smul_eq_zero_of_pow_smul_top_eq_bot {N : ℕ}
    (hN : S.I ^ N • (⊤ : Submodule S.A S.M) = ⊥) :
    ∃ n : ℕ, ∀ a ∈ S.I ^ n,
      ∀ x : (localCohomologyWithSupportInModuleFunctor.{u, v} S.A S.T i).obj
        (ModuleCat.of S.A S.M), a • x = 0

Stacks.LocalCohomology.Bootstrap.isLimit_of_pow_smul_top_eq_bot, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/EssentiallyConstantConsequences.lean, line 720. The attribute's comment: “the limit consequence H^i_T(M) = lim H^i_T(M/I^nM) for a bootstrap situation in which I acts nilpotently on M, with no hypothesis and in every degree”.

Stacks Project, Tag 0EIE, the limit consequence for a bootstrap situation in which I acts nilpotently on M, with no hypothesis and in every degree: the quotient maps exhibit H^i_T(M) as lim H^i_T(M/IⁿM).

def isLimit_of_pow_smul_top_eq_bot {N : ℕ}
    (hN : S.I ^ N • (⊤ : Submodule S.A S.M) = ⊥) :
    IsLimit (cone.{u, v} S i)

Stacks.LocalCohomology.Bootstrap.isMittagLeffler_of_eq_closedPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/EssentiallyConstantConsequences.lean, line 748. The attribute's comment: “the Mittag-Leffler consequence for a bootstrap situation whose ring is local and whose locus T is the closed point, with no hypothesis and in every degree”.

Stacks Project, Tag 0EIE, the Mittag-Leffler consequence for a bootstrap situation whose ring is local and whose locus is the closed point, with no hypothesis. The terms H^i_T(M/IⁿM) are then local cohomology at the maximal ideal of finite modules over a Noetherian local ring, hence Artinian, and an inverse system of Artinian modules is Mittag-Leffler. No degree restriction is needed either.

theorem isMittagLeffler_of_eq_closedPoint [IsLocalRing S.A]
    (hT : S.T = {IsLocalRing.closedPoint S.A}) :
    IsMittagLefflerCategorical (tower.{u, u} S i)

Tag 0EG0, a lemma

Tag 0EG0 in the Stacks Project.

Stacks.Algebraization.exists_ideal_isIso_localCohomologyToAdicQuotientLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapLocalCohomologyLimit.lean, line 443. The attribute's comment: “for the maximal ideal of a Noetherian local ring: the tag's conclusion in full at 𝔞 = 𝔪 -- the same ideal J₀ ≤ 𝔪, the same locus condition V(J₀) ∩ V(I) = V(𝔪), the same ∀ J ≤ J₀ with V(J) ∩ V(I) = V(𝔪), the same degree s+1, IsIso -- with the source's condition (2) in full as H. The statement has no support-ideal parameter: 𝔪 is substituted throughout. The source's condition (1) is used only to obtain Mittag-Leffler-ness of {H^s_𝔞(M/IⁿM)} from 0EIE, which at the maximal ideal follows from the finiteness of the M/IⁿM and the Artinianness of local cohomology there, via Stacks.LocalCohomology.isMittagLefflerCategorical_homologyAdicQuotientLocalCohomology, so (1) is not needed. The general support ideal is not covered; it needs 0EIE, which the library has only as consequences of its own essential-constancy assertion (RingTheory/LocalCohomology/EssentiallyConstantConsequences.lean). The specialisation is not vacuous: V(𝔪) is the closed point, and J ranges over the ideals with V(J) ∩ V(I) = {𝔪}, which include ideals strictly inside 𝔪”.

Let A be a Noetherian local ring with maximal ideal 𝔪, let I ⊆ 𝔪 be an ideal, let M be a finite A-module and let s and d be integers. Assume that A, I, 𝔪, M satisfy the conditions of Stacks 0EFL for s + 1 and d with J = 𝔪. Then there is an ideal J₀ ⊆ 𝔪 with V(J₀) ∩ V(I) = V(𝔪) such that for every ideal J ⊆ J₀ with V(J) ∩ V(I) = V(𝔪) the map

H^{s+1}_J(M) ⟶ lim H^{s+1}_𝔪(M/IⁿM)

is an isomorphism.

public theorem exists_ideal_isIso_localCohomologyToAdicQuotientLimit [IsLocalRing A]
    (I : Ideal A) (hIa : I ≤ maximalIdeal A) (s d : ℤ)
    (omega : DerivedCategory (ModuleCat.{u} A)) (δ : PrimeSpectrum A → ℤ) (δmax δmin : ℤ)
    (H : AlgebraizationHypotheses (M := M) I (maximalIdeal A) (s + 1) d omega δ δmax δmin) :
    ∃ J₀ : Ideal A, J₀ ≤ maximalIdeal A ∧
      PrimeSpectrum.zeroLocus (J₀ : Set A) ∩ PrimeSpectrum.zeroLocus (I : Set A) =
        PrimeSpectrum.zeroLocus ((maximalIdeal A : Ideal A) : Set A) ∧
      ∀ J : Ideal A, J ≤ J₀ →
        ∀ hJ : PrimeSpectrum.zeroLocus (J : Set A) ∩ PrimeSpectrum.zeroLocus (I : Set A) =
          PrimeSpectrum.zeroLocus ((maximalIdeal A : Ideal A) : Set A),
          IsIso (localCohomologyToAdicQuotientLimit A I (maximalIdeal A) J (ModuleCat.of A M)
            (hJ.trans (zeroLocus_inter_eq_self_of_le hIa).symm) (s + 1))

Stacks.Algebraization.BootstrapSituation.exists_ideal_isIso_localCohomologyToAdicQuotientLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/BootstrapLocalCohomologySupportLimit.lean, line 117.

Stacks Project, Tag 0EG0. Let I ⊆ 𝔞 be ideals of a Noetherian ring A, let M be a finite A-module and let s and d be integers. Assume

1. A, I, V(𝔞), M satisfy the assumptions of Situation [Stacks, Tag 0EFU] for s and d — the bootstrap situation S, with locus V(𝔞);
2. A, I, 𝔞, M satisfy the conditions of [Stacks, Tag 0EFL] for s + 1 and d with J = 𝔞 — the hypothesis H.

Then there is an ideal J₀ ⊆ 𝔞 with V(J₀) ∩ V(I) = V(𝔞) such that for every J ⊆ J₀ with V(J) ∩ V(I) = V(𝔞) the map H^{s+1}_J(M) ⟶ lim H^{s+1}_𝔞(M/IⁿM) is an isomorphism.

Stacks 0EFL supplies J₀ together with the identification H^{s+1}_J(M) = H^{s+1}(RΓ_𝔞(M)^∧); Stacks 0EEW puts H^{s+1}(RΓ_𝔞(M)^∧) in a short exact sequence with R¹lim H^s_𝔞(M/IⁿM) on the left and lim H^{s+1}_𝔞(M/IⁿM) on the right; and the left-hand term vanishes because {H^s_𝔞(M/IⁿM)} is Mittag-Leffler by Theorem [Stacks, Tag 0EIE].

Condition (2) is the disjunction of the two cases in which the library states Stacks 0EFL. Stacks.Algebraization.AlgebraizationHypotheses names the extreme values of a dimension function on V(𝔞) ∩ V(I) = V(𝔞), so it can only hold when V(𝔞) is nonempty; when V(𝔞) is empty, that is 𝔞 = A, the source's condition (5), the only one naming the dimension function, is guarded by V(𝔭) ∩ V(𝔞) ∩ V(I) ≠ ∅ and is vacuous, and of the source's conditions only the I-adic completeness of A is used, through Stacks.Algebraization.isAlgebraizationIdeal_of_zeroLocus_inter_eq_empty. Either disjunct follows from the source's condition (2), so the hypothesis asks for nothing beyond it.

public theorem BootstrapSituation.exists_ideal_isIso_localCohomologyToAdicQuotientLimit
    (S : BootstrapSituation.{u, u, u}) (a : Ideal S.A) (hIa : S.I ≤ a)
    (hT : S.T = PrimeSpectrum.zeroLocus (a : Set S.A))
    (omega : DerivedCategory (ModuleCat.{u} S.A)) (δ : PrimeSpectrum S.A → ℤ) (δmax δmin : ℤ)
    (H : AlgebraizationHypotheses (M := S.M) S.I a (S.s + 1) S.d omega δ δmax δmin ∨
      (IsAdicComplete S.I S.A ∧ PrimeSpectrum.zeroLocus (a : Set S.A) = ∅)) :
    ∃ J₀ : Ideal S.A, J₀ ≤ a ∧
      PrimeSpectrum.zeroLocus (J₀ : Set S.A) ∩ PrimeSpectrum.zeroLocus (S.I : Set S.A) =
        PrimeSpectrum.zeroLocus (a : Set S.A) ∧
      ∀ J : Ideal S.A, J ≤ J₀ →
        ∀ hJ : PrimeSpectrum.zeroLocus (J : Set S.A) ∩ PrimeSpectrum.zeroLocus (S.I : Set S.A) =
          PrimeSpectrum.zeroLocus (a : Set S.A),
          IsIso (localCohomologyToAdicQuotientLimit S.A S.I a J (ModuleCat.of S.A S.M)
            (hJ.trans (zeroLocus_inter_eq_self_of_le hIa).symm) (S.s + 1))

Sources

• Section 52.10, Tag 0EFT
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Algebraization.BootstrapSituation · Stacks.Algebraization.depth_localized_gt_of_no_intermediate_prime · Stacks.Algebraization.finite_adicCompletion · Stacks.Algebraization.subset_adicLocus_adicCompletion · Stacks.Algebraization.stableUnderSpecialization_adicCompletion · Stacks.Algebraization.dualizing_adicCompletion · Stacks.Algebraization.cohomologicalDimension_le_adicCompletion · Stacks.Algebraization.completedLocalDepth_adicCompletion

Section52.11 Algebraization of formal sections, I#

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

Tag 0DXI, a lemma

Tag 0DXI in the Stacks Project.

Stacks.Algebraization.isIso_toLimit_homology_puncturedSpectrumSections_of_two_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/PuncturedSpectrumCohomologyMittagLeffler.lean, line 672. The attribute's comment: “degrees i ≥ 2, for RΓ(U, ℒ) with ℒ a derived limit of ℱ/Iⁿℱ in D(𝒪_U), which is RΓ(U, ℱ)^∧ only by [Stacks, Tag 0BLX] + [Stacks, Tag 0A0K]; the Mittag-Leffler input of [Stacks, Tag 0DX1] part (2) is proved here, not assumed”.

Stacks Project, Tag 0DXI in degrees i ≥ 2, with no Mittag-Leffler hypothesis. Let (A, 𝔪) be a Noetherian local ring, let U = Spec A ∖ {𝔪} be its punctured spectrum, let ℱ be a coherent 𝒪_U-module and let I ⊆ A be an ideal. Let S be the adic quotient tower n ↦ ℱ/Iⁿℱ, pinned down by the quotient maps π through the universal property of killing multiplication by Iⁿ, and let ℒ be a derived limit of that tower in D(𝒪_U) — by [Stacks, Tag 0A0K] that is the derived completion ℱ^∧. Then for every i ≥ 2 the comparison map Hⁱ(RΓ(U, ℒ)) ⟶ lim_n Hⁱ(U, ℱ/Iⁿℱ), characterized by its composites with the limit projections, is an isomorphism.

This is Stacks.Algebraization.isIso_toLimit_homology_puncturedSpectrumSections with its hypothesis hML discharged by Stacks.Algebraization.isMittagLefflerCategorical_puncturedSpectrumCohomologySystem, which is [Stacks, Tag 0DX1] part (2). The degree restriction is the one that lemma imposes: the Milnor sequence in degree i consumes the Mittag-Leffler condition in degree i - 1, and Tag 0DX1 part (2) supplies it for i - 1 > 0. As in that earlier statement the left-hand side is named by ℒ, which is RΓ(U, ℱ)^∧ only by [Stacks, Tag 0BLX]; see the module documentation. The form recording the Milnor triangle that a fits into is Stacks.Algebraization .exists_milnorTriangle_isIso_toLimit_homology_puncturedSpectrumSections_of_two_le.

theorem isIso_toLimit_homology_puncturedSpectrumSections_of_two_le
    [IsNoetherianRing A] (I : Ideal A)
    (F : SheafOfModules.{u} (structureSheafRing (puncturedSpectrumRingedSpace A)))
    [SheafOfModules.IsCoherent F]
    (S : ℕᵒᵖ ⥤ SheafOfModules.{u} (structureSheafRing (puncturedSpectrumRingedSpace A)))
    (hScoherent : ∀ n : ℕᵒᵖ, SheafOfModules.IsCoherent (S.obj n))
    (π : ∀ n : ℕᵒᵖ, F ⟶ S.obj n)
    (hπ_epi : ∀ n : ℕᵒᵖ, Epi (π n))
    (hπ_nat : ∀ {m n : ℕᵒᵖ} (h : m ⟶ n), π m ≫ S.map h = π n)
    (hπ_smul : ∀ (n : ℕ) (a : A), a ∈ I ^ n →
      (baseSmul (puncturedSpectrumRingedSpace A) (puncturedSpectrumScalars A) a).asHom.app F ≫
        π (op n) = 0)
    (hπ_univ : ∀ (n : ℕ)
      (G : SheafOfModules.{u} (structureSheafRing (puncturedSpectrumRingedSpace A))) (f : F ⟶ G),
      (∀ a ∈ I ^ n,
        (baseSmul (puncturedSpectrumRingedSpace A) (puncturedSpectrumScalars A) a).asHom.app F ≫
          f = 0) →
      ∃ g : S.obj (op n) ⟶ G, π (op n) ≫ g = f)
    (L : DerivedCategory (SheafOfModules.{u} (structureSheafRing (puncturedSpectrumRingedSpace A))))
    (hL : IsDerivedLimit (S ⋙ DerivedCategory.singleFunctor
      (SheafOfModules.{u} (structureSheafRing (puncturedSpectrumRingedSpace A))) 0) L)
    (i : ℤ) (hi : 2 ≤ i) :
    let Hi := DerivedCategory.homologyFunctor (ModuleCat.{u} A) i
    let RΓS : ℕᵒᵖ ⥤ DerivedCategory (ModuleCat.{u} A) :=
      S ⋙ DerivedCategory.singleFunctor
          (SheafOfModules.{u} (structureSheafRing (puncturedSpectrumRingedSpace A))) 0 ⋙
        puncturedSpectrumDerivedSections A
    let Y : ℕ → DerivedCategory (ModuleCat.{u} A) := fun n ↦ RΓS.obj (op n)
    ∃ (a : (puncturedSpectrumDerivedSections A).obj L ⟶ ∏ᶜ Y)
      (q : Hi.obj ((puncturedSpectrumDerivedSections A).obj L) ⟶
        limit (puncturedSpectrumCohomologySystem A S i)),
      (∀ n : ℕ, q ≫ limit.π (puncturedSpectrumCohomologySystem A S i) (op n) =
        Hi.map a ≫ Hi.map (Pi.π Y n)) ∧ IsIso q

Stacks.Algebraization.isIso_toLimit_homology_puncturedSpectrumSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/PuncturedSpectrumCompletedSections.lean, line 324. The attribute's comment: “for RΓ(U, ℒ) with ℒ a derived limit of the tower ℱ/Iⁿℱ in D(𝒪_U), which is RΓ(U, ℱ)^∧ only by [Stacks, Tag 0BLX] + [Stacks, Tag 0A0K]; the Mittag-Leffler condition of [Stacks, Tag 0DX1] part (2) is carried as the hypothesis hML, neither it nor [Stacks, Tag 0BLX] being available in this library”.

Stacks Project, Tag 0DXI, for the derived sections of a derived limit of the adic quotient tower. Let (A, 𝔪) be a Noetherian local ring, let U = Spec A ∖ {𝔪} be its punctured spectrum, let ℱ be a coherent 𝒪_U-module and let I ⊆ A be an ideal. Let S be the adic quotient tower n ↦ ℱ/Iⁿℱ, pinned down by the quotient maps π through the universal property of killing multiplication by Iⁿ, and let ℒ be a derived limit of that tower in D(𝒪_U) — by [Stacks, Tag 0A0K] that is the derived completion ℱ^∧. Then for every i the comparison map Hⁱ(RΓ(U, ℒ)) ⟶ lim_n Hⁱ(U, ℱ/Iⁿℱ), characterized by its composites with the limit projections, is an isomorphism.

The R¹lim term of the Milnor short exact sequence of [Stacks, Tag 0D60] vanishes because the inverse system n ↦ H^{i-1}(U, ℱ/Iⁿℱ) is Mittag-Leffler, which is the hypothesis hML — asked for in that one degree only, so that for i ≥ 2 it is exactly what [Stacks, Tag 0DX1] part (2) would supply; that part of Tag 0DX1 is unavailable in this library. By [Stacks, Tag 0BLX] RΓ(U, ℱ^∧) is the derived I-adic completion RΓ(U, ℱ)^∧, which is how the source names the left-hand side; that identity is also unavailable here, so the left-hand side is named by ℒ instead. See the module documentation.

theorem isIso_toLimit_homology_puncturedSpectrumSections
    [IsNoetherianRing A] (I : Ideal A)
    (F : SheafOfModules.{u} (structureSheafRing (puncturedSpectrumRingedSpace A)))
    [SheafOfModules.IsCoherent F]
    (S : ℕᵒᵖ ⥤ SheafOfModules.{u} (structureSheafRing (puncturedSpectrumRingedSpace A)))
    (hScoherent : ∀ n : ℕᵒᵖ, SheafOfModules.IsCoherent (S.obj n))
    (π : ∀ n : ℕᵒᵖ, F ⟶ S.obj n)
    (hπ_epi : ∀ n : ℕᵒᵖ, Epi (π n))
    (hπ_nat : ∀ {m n : ℕᵒᵖ} (h : m ⟶ n), π m ≫ S.map h = π n)
    (hπ_smul : ∀ (n : ℕ) (a : A), a ∈ I ^ n →
      (baseSmul (puncturedSpectrumRingedSpace A) (puncturedSpectrumScalars A) a).asHom.app F ≫
        π (op n) = 0)
    (hπ_univ : ∀ (n : ℕ)
      (G : SheafOfModules.{u} (structureSheafRing (puncturedSpectrumRingedSpace A))) (f : F ⟶ G),
      (∀ a ∈ I ^ n,
        (baseSmul (puncturedSpectrumRingedSpace A) (puncturedSpectrumScalars A) a).asHom.app F ≫
          f = 0) →
      ∃ g : S.obj (op n) ⟶ G, π (op n) ≫ g = f)
    (L : DerivedCategory (SheafOfModules.{u} (structureSheafRing (puncturedSpectrumRingedSpace A))))
    (hL : IsDerivedLimit (S ⋙ DerivedCategory.singleFunctor
      (SheafOfModules.{u} (structureSheafRing (puncturedSpectrumRingedSpace A))) 0) L)
    (i : ℤ)
    (hML : IsMittagLefflerCategorical (puncturedSpectrumCohomologySystem A S (i - 1))) :
    let Hi := DerivedCategory.homologyFunctor (ModuleCat.{u} A) i
    let RΓS : ℕᵒᵖ ⥤ DerivedCategory (ModuleCat.{u} A) :=
      S ⋙ DerivedCategory.singleFunctor
          (SheafOfModules.{u} (structureSheafRing (puncturedSpectrumRingedSpace A))) 0 ⋙
        puncturedSpectrumDerivedSections A
    let Y : ℕ → DerivedCategory (ModuleCat.{u} A) := fun n ↦ RΓS.obj (op n)
    ∃ (a : (puncturedSpectrumDerivedSections A).obj L ⟶ ∏ᶜ Y)
      (q : Hi.obj ((puncturedSpectrumDerivedSections A).obj L) ⟶
        limit (puncturedSpectrumCohomologySystem A S i)),
      (∀ n : ℕ, q ≫ limit.π (puncturedSpectrumCohomologySystem A S i) (op n) =
        Hi.map a ≫ Hi.map (Pi.π Y n)) ∧ IsIso q

Stacks.Algebraization.isIso_toLimit_homology_derivedCompletion_puncturedSpectrumSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/PuncturedSpectrumDerivedCompletion.lean, line 213. The attribute's comment: “the whole lemma: for (A, 𝔪) Noetherian local with punctured spectrum U, a coherent 𝒪_U-module ℱ and an ideal I ⊆ A, the comparison map Hⁱ(RΓ(U,ℱ)^∧) ⟶ lim_n Hⁱ(U, ℱ/Iⁿℱ) is an isomorphism in every degree i, the left-hand side being the derived I-adic completion in D(A) of the derived sections RΓ(U,ℱ) and the tower on the right being the adic quotient tower at I𝒪_U. The map shown invertible is the comparison map, characterized by the limit projections through an α required to exhibit RΓ(U,ℱ)^∧ as a derived limit of n ↦ RΓ(U, ℱ/Iⁿℱ)”.

Stacks Project, Tag 0DXI. Let (A, 𝔪) be a Noetherian local ring, let U = Spec A ∖ {𝔪} be its punctured spectrum, let ℱ be a coherent 𝒪_U-module and let I ⊆ A be an ideal, presented by a finite generating family a_1, …, a_r. Then for every i the comparison map

Hⁱ(RΓ(U, ℱ)^∧) ⟶ lim_n Hⁱ(U, ℱ/Iⁿℱ)

is an isomorphism, where RΓ(U, ℱ)^∧ is the derived I-adic completion of RΓ(U, ℱ) in D(A) and ℱ/Iⁿℱ is the adic quotient tower at the sheaf of ideals I𝒪_U.

The comparison map is the one determined by the Milnor triangle: it is characterized by its composites with the limit projections through a morphism α : RΓ(U, ℱ)^∧ ⟶ ∏ₙ RΓ(U, ℱ/Iⁿℱ) which is required to exhibit RΓ(U, ℱ)^∧ as a derived limit of n ↦ RΓ(U, ℱ/Iⁿℱ), so the conclusion is about the comparison map and not about some map.

Nothing is assumed: the derived limit of the tower, the identification of its derived sections with RΓ(U, ℱ)^∧ and the Mittag-Leffler condition that makes the comparison invertible are all produced — by [Stacks, Tag 0A0K] parts (3) and (4), by [Stacks, Tag 0BLX], and by [Stacks, Tag 0DX1] part (2) together with its degree-zero and negative-degree companions.

theorem isIso_toLimit_homology_derivedCompletion_puncturedSpectrumSections
    (ha : Ideal.span (Set.range a) = I) (i : ℤ) :
    let S := puncturedSpectrumAdicQuotientSystem A a F
    let Hi := DerivedCategory.homologyFunctor (ModuleCat.{u} A) i
    let C := (DerivedCompletion.derivedCompletionFunctor A a).obj
      ((puncturedSpectrumDerivedSections A).obj ((DerivedCategory.singleFunctor
        (SheafOfModules.{u} (structureSheafRing (puncturedSpectrumRingedSpace A))) 0).obj F))
    let RΓS : ℕᵒᵖ ⥤ DerivedCategory (ModuleCat.{u} A) :=
      S ⋙ DerivedCategory.singleFunctor
          (SheafOfModules.{u} (structureSheafRing (puncturedSpectrumRingedSpace A))) 0 ⋙
        puncturedSpectrumDerivedSections A
    let Y : ℕ → DerivedCategory (ModuleCat.{u} A) := fun n ↦ RΓS.obj (op n)
    let d : (∏ᶜ Y) ⟶ ∏ᶜ Y := Pi.lift fun n : ℕ ↦
      Pi.π Y n - Pi.π Y (n + 1) ≫ RΓS.map (homOfLE (Nat.le_succ n)).op
    ∃ (α : C ⟶ ∏ᶜ Y) (β : (∏ᶜ Y) ⟶ C⟦(1 : ℤ)⟧),
      Triangle.mk α d β ∈ distTriang (DerivedCategory (ModuleCat.{u} A)) ∧
      ∃ q : Hi.obj C ⟶ limit (puncturedSpectrumCohomologySystem A S i),
        (∀ n : ℕ, q ≫ limit.π (puncturedSpectrumCohomologySystem A S i) (op n) =
          Hi.map α ≫ Hi.map (Pi.π Y n)) ∧ IsIso q

Stacks.Algebraization.exists_homologyIso_limit_derivedCompletion_puncturedSpectrumSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/PuncturedSpectrumDerivedCompletion.lean, line 290. The attribute's comment: “the whole lemma read as an isomorphism of A-modules: Hⁱ(RΓ(U,ℱ)^∧) ≅ lim_n Hⁱ(U, ℱ/Iⁿℱ) in every degree i, for (A, 𝔪) Noetherian local with punctured spectrum U, a coherent 𝒪_U-module ℱ and an ideal I ⊆ A. The isomorphism is the comparison map, characterized by the limit projections through an α required to exhibit RΓ(U,ℱ)^∧ as a derived limit of n ↦ RΓ(U, ℱ/Iⁿℱ)”.

Stacks Project, Tag 0DXI, read as an isomorphism of A-modules. In the situation of Stacks.Algebraization.isIso_toLimit_homology_derivedCompletion_puncturedSpectrumSections, the degree-i cohomology of the derived I-adic completion of RΓ(U, ℱ) is isomorphic to the inverse limit of the A-modules Hⁱ(U, ℱ/Iⁿℱ).

The isomorphism keeps the characterization by the limit projections and α is still required to be a derived-limit structure map of n ↦ RΓ(U, ℱ/Iⁿℱ), so what is asserted is that the comparison map is invertible and not merely that the two modules are abstractly isomorphic.

theorem exists_homologyIso_limit_derivedCompletion_puncturedSpectrumSections
    (ha : Ideal.span (Set.range a) = I) (i : ℤ) :
    let S := puncturedSpectrumAdicQuotientSystem A a F
    let Hi := DerivedCategory.homologyFunctor (ModuleCat.{u} A) i
    let C := (DerivedCompletion.derivedCompletionFunctor A a).obj
      ((puncturedSpectrumDerivedSections A).obj ((DerivedCategory.singleFunctor
        (SheafOfModules.{u} (structureSheafRing (puncturedSpectrumRingedSpace A))) 0).obj F))
    let RΓS : ℕᵒᵖ ⥤ DerivedCategory (ModuleCat.{u} A) :=
      S ⋙ DerivedCategory.singleFunctor
          (SheafOfModules.{u} (structureSheafRing (puncturedSpectrumRingedSpace A))) 0 ⋙
        puncturedSpectrumDerivedSections A
    let Y : ℕ → DerivedCategory (ModuleCat.{u} A) := fun n ↦ RΓS.obj (op n)
    let d : (∏ᶜ Y) ⟶ ∏ᶜ Y := Pi.lift fun n : ℕ ↦
      Pi.π Y n - Pi.π Y (n + 1) ≫ RΓS.map (homOfLE (Nat.le_succ n)).op
    ∃ (α : C ⟶ ∏ᶜ Y) (β : (∏ᶜ Y) ⟶ C⟦(1 : ℤ)⟧),
      Triangle.mk α d β ∈ distTriang (DerivedCategory (ModuleCat.{u} A)) ∧
      ∃ eq : Hi.obj C ≅ limit (puncturedSpectrumCohomologySystem A S i),
        ∀ n : ℕ, eq.hom ≫ limit.π (puncturedSpectrumCohomologySystem A S i) (op n) =
          Hi.map α ≫ Hi.map (Pi.π Y n)

Tag 0DXQ, a theorem

Tag 0DXQ in the Stacks Project.

Stacks.Algebraization.coherentFormalAlgebraization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CoherentSheafPuncturedAlgebraization.lean, line 216.

Stacks 0DXQ. Let (A, 𝔪) be a Noetherian local ring which has a dualizing complex and is complete with respect to an ideal I. Set X = Spec A, Y = V(I) and U = X ∖ {𝔪}, and let ℱ be a coherent sheaf on U. Assume

1. cd(A, I) ≤ d, and
2. for any x ∈ X ∖ Y whose closure in X meets U ∩ Y, depth(ℱ_x) ≥ s or depth(ℱ_x) + dim(closure of x) > d + s,

Then there is an open V₀ ⊆ U containing U ∩ Y such that for any open V ⊆ V₀ containing U ∩ Y the map

H^i(V, ℱ) ⟶ lim_n H^i(U, ℱ/Iⁿℱ)

is an isomorphism for i < s. If in addition depth(ℱ_x) + dim(closure of x) > s for all x ∈ U ∩ Y, then these cohomology groups are finite A-modules.

Concretely: there is a finite A-module M with ℱ ≅ M̃|_U and ℱ/Iⁿℱ ≅ (M/IⁿM)~|_U as towers, and an ideal J₀ with V(J₀) ∩ V(I) = {𝔪} — that is, the open V₀ = X ∖ V(J₀) ⊆ U containing U ∩ Y — such that for every ideal J ⊆ J₀ with V(J) ∩ V(I) = {𝔪} — that is, for every open V = X ∖ V(J) ⊆ V₀ containing U ∩ Y — and every degree i < s, the canonical map H^i(V, M̃) ⟶ lim_n H^i(U, (M/IⁿM)~) is an isomorphism, and H^i(V, M̃) is a finite A-module whenever the extra depth bound holds.

Both groups of that map are identified with the source's own, so that nothing is left to the reader:

• H^i(V, M̃) is H^i(V, ℱ|_V), the cohomology on V of the sheaf ℱ itself, by the conjunct built from Stacks.Algebraization.openCohomologyBaseRestrictIso;
• the tower n ↦ H^i(U, (M/IⁿM)~) whose limit the map lands in is the tower n ↦ H^i(U, ℱ/Iⁿℱ), transition maps included, by the conjunct built from Stacks.Algebraization.quotientSystemOpenCohomologyNatIso. An isomorphism of towers is stronger than the isomorphism of limits it induces, so this pins the right-hand side without either limit having to be formed again.

The division of the two clauses is the source's. The comparison is asserted under assumptions (1) and (2) alone; the extra bound depth(ℱ_x) + dim(closure of x) > s on U ∩ Y appears only as the hypothesis of the finiteness clause, where the source puts it ("If in addition …"). One ideal J₀ serves both, by the case distinction carried out in Stacks.Algebraization.PuncturedNeighbourhood.comparison_and_finiteness.

Nothing beyond the hypotheses of the theorem is assumed. The module M is produced by Stacks 0BK0 (1), the ideal J₀ by Stacks 0DXP and Stacks 0DXN, the stabilizing data of Stacks 0EFI and the bound 0 ≤ d from assumption (1), and the localization triangle data of the degree-zero case from a finite generating family of J. Properness of I — the source's standing 𝔪 ∈ V(I), without which V(I) is empty — is derived too, not assumed: over a local ring I = A would make A ⊤-adically Hausdorff, hence zero.

The two cohomology groups of the conclusion are named through the presentation ℱ ≅ M̃|_U and the tower isomorphism ℱ/Iⁿℱ ≅ (M/IⁿM)~|_U, both of which the statement exhibits; this is the reading the source itself uses, its proof opening with the choice of such an M. The statement also carries out that reading, exhibiting each of the two groups of the comparison map as the corresponding group of ℱ — see the two conjuncts described above.

theorem coherentFormalAlgebraization (I : Ideal A) (s d : ℤ)
    (omega : DerivedCategory (ModuleCat.{u} A))
    (hcomplete : IsAdicComplete I A)
    (hdualizing : Dualizing.IsDualizingComplex omega)
    (hcd : Stacks.LocalCohomology.cohomologicalDimension A I
      (Ideal.fg_of_isNoetherianRing I) ≤ d)
    (F : (complementZeroLocus A (maximalIdeal A) : Scheme).Modules) [F.IsCoherent]
    (h2 : StalkDepthOrDimensionBound I F s d) :
    ∃ M : ModuleCat.{u} A, Module.Finite A M ∧
      Nonempty (F ≅ ((tilde.functor (CommRingCat.of A)).obj M).restrict
        (complementZeroLocus A (maximalIdeal A)).ι) ∧
      Nonempty (quotientSystemNearVanishing A I (maximalIdeal A) F ≅
        (adicQuotientModuleSystem A I M ⋙ tilde.functor (CommRingCat.of A)) ⋙
          Scheme.Modules.restrictFunctor (complementZeroLocus A (maximalIdeal A)).ι) ∧
      (∀ i : ℕ, Nonempty (quotientSystemNearVanishing A I (maximalIdeal A) F ⋙
          openCohomologyBaseFunctor A (complementZeroLocus A (maximalIdeal A)) i ≅
        adicQuotientModuleSystem A I M ⋙
          complementCohomologyBaseFunctor (A := CommRingCat.of A) (maximalIdeal A) i)) ∧
      ∃ J₀ : Ideal A,
        PrimeSpectrum.zeroLocus (J₀ : Set A) ∩ PrimeSpectrum.zeroLocus (I : Set A) =
            {closedPoint A} ∧
          ∀ J : Ideal A, J ≤ J₀ →
            ∀ hV : PrimeSpectrum.zeroLocus (J : Set A) ∩ PrimeSpectrum.zeroLocus (I : Set A) =
              {closedPoint A},
            ∀ i : ℕ, (i : ℤ) < s →
              IsIso (PuncturedNeighbourhood.neighbourhoodToPuncturedLimit I J M hV i) ∧
                Nonempty (openCohomologyBase A (complementZeroLocus A J)
                    ((Scheme.Modules.restrictFunctor
                      ((Spec (CommRingCat.of A)).homOfLE
                        (le_complementZeroLocus_maximalIdeal
                          (PuncturedNeighbourhood.le_maximalIdeal_of_zeroLocus_inter hV)))).obj F)
                      i ≅
                  complementCohomologyBase (A := CommRingCat.of A) J M i) ∧
                (StalkDepthAddDimGt I F s →
                  Module.Finite A
                    (complementCohomologyBase (A := CommRingCat.of A) J M i))

Stacks.Algebraization.PuncturedNeighbourhood.exists_ideal_finite_neighbourhoodCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/PuncturedNeighbourhoodCohomologyFiniteness.lean, line 270. The attribute's comment: “finiteness of H^i(V, ℱ) for i < s, with ℱ = M̃|_U”.

Stacks 0DXQ, the finiteness clause. Let (A, 𝔪) be a Noetherian local ring which has a dualizing complex and is I-adically complete, let M be a finite A-module, and assume assumptions (1) and (2) of the theorem together with depth(M_𝔭) + dim(A/𝔭) > s for every prime 𝔭 ∈ V(I) other than 𝔪 — the theorem's extra finiteness assumption, read at the points of U ∩ Y. Then there is an ideal J₀ with V(J₀) ∩ V(I) = {𝔪}, that is an open V₀ = Spec A ∖ V(J₀) of the punctured spectrum containing U ∩ V(I), such that for every J ⊆ J₀ with V(J) ∩ V(I) = {𝔪} — that is, for every open V = Spec A ∖ V(J) inside V₀ containing U ∩ V(I) — the A-module H^i(V, M̃) is finite in every degree i < s.

Nothing beyond the hypotheses of the theorem is assumed: the stabilizing data of Stacks 0EFI is constructed, not assumed, from assumption (1); see the module documentation.

public theorem exists_ideal_finite_neighbourhoodCohomology (I : Ideal A) (s d : ℤ)
    (omega : DerivedCategory (ModuleCat.{u} A)) (H : Hypotheses (M := M) I s d omega)
    (hdepth : DepthAddDimGtAtMaximalIdeal (M := M) I s) :
    ∃ J₀ : Ideal A,
      PrimeSpectrum.zeroLocus (J₀ : Set A) ∩ PrimeSpectrum.zeroLocus (I : Set A) =
          {closedPoint A} ∧
        ∀ J : Ideal A, J ≤ J₀ →
          PrimeSpectrum.zeroLocus (J : Set A) ∩ PrimeSpectrum.zeroLocus (I : Set A) =
            {closedPoint A} →
          ∀ i : ℕ, (i : ℤ) < s → Module.Finite A (neighbourhoodCohomology (M := M) J i)

Stacks.Algebraization.PuncturedNeighbourhood.finite_neighbourhoodCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/PuncturedNeighbourhoodCohomologyFiniteness.lean, line 354. The attribute's comment: “finiteness of H^i(V, ℱ) for i < s, with ℱ = M̃|_U, on the carried existence statement of Stacks 0EFI”.

Stacks 0DXQ, the finiteness clause. Let (A, 𝔪) be a Noetherian local ring which has a dualizing complex and is I-adically complete, let M be a finite A-module, and assume assumptions (1) and (2) of the theorem together with depth(M_𝔭) + dim(A/𝔭) > s for every prime 𝔭 ∈ V(I) other than 𝔪 — the theorem's extra finiteness assumption, read at the points of U ∩ Y. Then there is an ideal J₀ with V(J₀) ∩ V(I) = {𝔪}, that is an open V₀ = Spec A ∖ V(J₀) of the punctured spectrum containing U ∩ V(I), such that for every J ⊆ J₀ with V(J) ∩ V(I) = {𝔪} — that is, for every open V = Spec A ∖ V(J) inside V₀ containing U ∩ V(I) — the A-module H^i(V, M̃) is finite in every degree i < s.

The hypothesis hex is the existence statement of Stacks 0EFI, carried as a general statement about its own data; it is unused, the same conclusion being exists_ideal_finite_neighbourhoodCohomology with nothing carried.

public theorem finite_neighbourhoodCohomology (I : Ideal A) (s d : ℤ)
    (omega : DerivedCategory (ModuleCat.{u} A)) (H : Hypotheses (M := M) I s d omega)
    (hdepth : DepthAddDimGtAtMaximalIdeal (M := M) I s) (hex : StabilizingDataExists.{u}) :
    ∃ J₀ : Ideal A,
      PrimeSpectrum.zeroLocus (J₀ : Set A) ∩ PrimeSpectrum.zeroLocus (I : Set A) =
          {closedPoint A} ∧
        ∀ J : Ideal A, J ≤ J₀ →
          PrimeSpectrum.zeroLocus (J : Set A) ∩ PrimeSpectrum.zeroLocus (I : Set A) =
            {closedPoint A} →
          ∀ i : ℕ, (i : ℤ) < s → Module.Finite A (neighbourhoodCohomology (M := M) J i)

Tag 0DXR, a lemma

Tag 0DXR in the Stacks Project.

Stacks.Algebraization.mono_comparisonMap_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/PuncturedSpectrumFormalSections.lean, line 233. The attribute's comment: “the injectivity half of the displayed map, proved with none of the source's hypotheses beyond Noetherian and coherent; the surjectivity half and the finiteness of the two modules hold at the source's own hypotheses, by Stacks.Algebraization.isIso_comparisonModuleMap_and_finite_maximalIdeal”.

Stacks 0DXR, the injectivity half. The canonical map from the sections of a coherent module ℱ on the punctured spectrum U = Spec(A) ∖ {𝔪} defined near U ∩ V(I) to the compatible families of sections of ℱ / Iⁿ ℱ on all of U is injective. No hypothesis beyond A Noetherian and ℱ coherent is used: neither completeness, nor the dualizing complex, nor the dimension bound at the associated points.

The surjectivity half, and with it the whole of the source's conclusion — the map is an isomorphism and both of its sides are finite A-modules — is Stacks.Algebraization.isIso_comparisonModuleMap_and_finite_maximalIdeal of PuncturedSpectrumFormalSectionsWhole.lean, at the source's own hypotheses.

public theorem mono_comparisonMap_maximalIdeal [F.IsCoherent] :
    Mono (comparisonMap A I (maximalIdeal A) F)

Stacks.Algebraization.mono_comparisonModuleMap_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/PuncturedSpectrumFormalSections.lean, line 259. The attribute's comment: “the two sides of the displayed map are A-modules and the map is A-linear, and injective as a map of A-modules; its underlying map of abelian groups is the tag's map, by forget₂_comparisonModuleMap. The surjectivity half and the finiteness of the two A-modules hold at the source's own hypotheses, by Stacks.Algebraization.isIso_comparisonModuleMap_and_finite_maximalIdeal”.

Stacks 0DXR, the A-module structures and the A-linearity of the displayed map. The source states its conclusion as an isomorphism of finite A-modules, so the two sides carry A-module structures and the map between them is A-linear. The two sides of Stacks.Algebraization.comparisonMap are a colimit and a limit of groups of sections, hence abelian groups; the A-module structures are Stacks.Algebraization.sectionsNearVanishingColimit and Stacks.Algebraization.formalSectionsLimit, obtained from the multiplication by A on sections induced by A ⟶ Γ(U, 𝒪_U), and the displayed map is A-linear for them, by Stacks.Algebraization.comparisonMap_comp_smul. The statement below is that this A-linear map — whose underlying map of abelian groups is the tag's map, by Stacks.Algebraization.forget₂_comparisonModuleMap — is injective, that is, that the injectivity half holds in the category of A-modules.

The source's surjectivity half and the finiteness of the two A-modules are supplied, for this same A-linear map and at the source's own hypotheses, by Stacks.Algebraization.isIso_comparisonModuleMap_and_finite_maximalIdeal of PuncturedSpectrumFormalSectionsWhole.lean.

public theorem mono_comparisonModuleMap_maximalIdeal [F.IsCoherent] :
    Mono (comparisonModuleMap A I (maximalIdeal A) F)

Stacks.Algebraization.isIso_comparisonModuleMap_and_finite_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/PuncturedSpectrumFormalSectionsWhole.lean, line 298. The attribute's comment: “the whole statement: the displayed map colim_V H⁰(V, ℱ) ⟶ lim_n H⁰(U, ℱ/Iⁿℱ) is an isomorphism of A-modules, and both of its two sides are finite A-modules”.

Stacks 0DXR. Let (A, 𝔪) be a Noetherian local ring which has a dualizing complex and is complete with respect to an ideal I. Put X = Spec(A), Y = V(I) and U = X ∖ {𝔪}, and let ℱ be a coherent module on U such that every associated point x ∈ U of ℱ satisfies dim(closure {x}) > cd(A, I) + 1, the closure being taken in X. Then the canonical map

colim_V H⁰(V, ℱ) ⟶ lim_n H⁰(U, ℱ / Iⁿ ℱ),

the colimit being over the opens V ⊆ U containing U ∩ Y, is an isomorphism of finite A-modules.

The two sides are the A-modules Stacks.Algebraization.sectionsNearVanishingColimit and Stacks.Algebraization.formalSectionsLimit; the map is Stacks.Algebraization.comparisonModuleMap, whose underlying map of abelian groups is Stacks.Algebraization.comparisonMap by Stacks.Algebraization.forget₂_comparisonModuleMap. The source's dimension hypothesis is stated with dim(closure {x}) = dim(A/𝔭), exactly as the source states it.

The proof is the source's: apply Stacks 0DXQ with s = 1, getting the finiteness too. Stacks 0BK0 (1) presents ℱ as M̃|_U for a finite A-module M; the associated points of M̃|_U are the associated primes of M, so the dimension hypothesis becomes the hypothesis of Stacks 0DXP, which supplies an ideal J₀, and of the finiteness clause of Stacks 0DXQ, which supplies an ideal J₁. At J = J₀ ∩ J₁ both apply: the canonical map H¹_J(M) ⟶ lim_n H¹_J(M/IⁿM) is onto by Stacks 0DXP together with the pinned form of Stacks 0DXJ, so the four-term diagram chase makes the comparison at the neighbourhood X ∖ V(J) onto; the displayed map is injective with no hypothesis beyond Noetherian and coherent, hence an isomorphism; and the colimit is a quotient of H⁰(X ∖ V(J), ℱ), which is finite.

public theorem isIso_comparisonModuleMap_and_finite_maximalIdeal
    (hcomplete : IsAdicComplete I A)
    (hdualizing : ∃ K : DerivedCategory (ModuleCat.{u} A), Dualizing.IsDualizingComplex K)
    (F : (complementZeroLocus A (maximalIdeal A) : Scheme).Modules) [F.IsCoherent]
    (hdim : ∀ x : (complementZeroLocus A (maximalIdeal A) : Scheme),
      x ∈ Stacks.Divisors.associatedPoints F →
      ((cohomologicalDimension A I I.fg_of_isNoetherianRing + 1 : ℤ) : EInt) <
        krullDimToEInt (ringKrullDim (A ⧸ x.1.asIdeal))) :
    IsIso (comparisonModuleMap A I (maximalIdeal A) F) ∧
      Module.Finite A (sectionsNearVanishingColimit A I (maximalIdeal A) F) ∧
        Module.Finite A (formalSectionsLimit A I (maximalIdeal A) F)

Sources

• Section 52.11, Tag 0DXH
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Algebraization.isIso_toLimit_homology_puncturedSpectrumSections_of_two_le · Stacks.Algebraization.isIso_toLimit_homology_puncturedSpectrumSections · Stacks.Algebraization.isIso_toLimit_homology_derivedCompletion_puncturedSpectrumSections · Stacks.Algebraization.exists_homologyIso_limit_derivedCompletion_puncturedSpectrumSections · Stacks.Algebraization.coherentFormalAlgebraization · Stacks.Algebraization.PuncturedNeighbourhood.exists_ideal_finite_neighbourhoodCohomology · Stacks.Algebraization.PuncturedNeighbourhood.finite_neighbourhoodCohomology · Stacks.Algebraization.mono_comparisonMap_maximalIdeal

Section52.12 Algebraization of formal sections, II#

Section 52.12 of the Stacks Project, Tag 0EG1. 7 tags here are carried by 13 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0H48, a lemma

Tag 0H48 in the Stacks Project.

Stacks.Algebraization.isIso_comparisonMap_first_of_middle_and_third, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/ComparisonShortExact.lean, line 281. The attribute's comment: “first comparison”.

For a short exact sequence 0 → F' → F → F'' → 0 of coherent modules on U = Spec(A) ∖ V(𝔞) with A Noetherian, if the comparison maps of Stacks.Algebraization.comparisonMap for F and F'' are isomorphisms, so is that for F'.

theorem isIso_comparisonMap_first_of_middle_and_third
    (A : Type u) [CommRing A] [IsNoetherianRing A] (I a : Ideal A)
    (S : ShortComplex (complementZeroLocus A a : Scheme).Modules) (hS : S.ShortExact)
    [S.X₁.IsCoherent] [S.X₂.IsCoherent] [S.X₃.IsCoherent]
    (h₂ : IsIso (comparisonMap A I a S.X₂)) (h₃ : IsIso (comparisonMap A I a S.X₃)) :
    IsIso (comparisonMap A I a S.X₁)

Stacks.Algebraization.isIso_comparisonMap_middle_of_ends, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/ComparisonShortExactMiddle.lean, line 1037. The attribute's comment: “middle comparison”.

Stacks 0H48, the middle comparison. For a short exact sequence 0 → F' → F → F'' → 0 of coherent modules on U = Spec(A) ∖ V(𝔞) with A Noetherian, if the comparison maps of Stacks.Algebraization.comparisonMap for F' and F'' are isomorphisms, so is that for F.

theorem isIso_comparisonMap_middle_of_ends (A : Type u) [CommRing A] [IsNoetherianRing A]
    (I a : Ideal A) (S : ShortComplex (complementZeroLocus A a : Scheme).Modules)
    (hS : S.ShortExact) [S.X₁.IsCoherent] [S.X₂.IsCoherent] [S.X₃.IsCoherent]
    (h₁ : IsIso (comparisonMap A I a S.X₁)) (h₃ : IsIso (comparisonMap A I a S.X₃)) :
    IsIso (comparisonMap A I a S.X₂)

Tag 0EIF, a lemma

Tag 0EIF in the Stacks Project.

Stacks.Algebraization.isIso_comparisonMap_of_formalSectionsHypotheses, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/FormalSectionsAlgebraizationTheorem.lean, line 78.

Stacks 0EIF. Let I ⊆ 𝔞 be ideals of a Noetherian ring A and let F be a coherent module on U = Spec(A) ∖ V(𝔞). Assume that A is I-adically complete and has a dualizing complex; that every associated point x of F outside V(I) whose closure meets V(I) outside V(𝔞) has dim(𝒪_{closure {x}, z}) > cd(A, I) + 1 at every z ∈ closure {x} ∩ V(𝔞); and that either F|_{U ∖ V(I)} satisfies (S₁) or the values on V(𝔞) of a dimension function on Spec(A) differ by at most 2 (Stacks.Algebraization.FormalSectionsHypotheses). Then the map colim_V H⁰(V, F) ⟶ lim_n H⁰(U, F/IⁿF), the colimit over the opens V ⊆ U containing U ∩ V(I), is an isomorphism.

public theorem isIso_comparisonMap_of_formalSectionsHypotheses {A : Type u} [CommRing A]
    [IsNoetherianRing A] (I a : Ideal A) (hIa : I ≤ a)
    (F : (complementZeroLocus A a : Scheme).Modules) [F.IsCoherent]
    (h : FormalSectionsHypotheses A I a F) :
    IsIso (comparisonMap A I a F)

Stacks.Algebraization.isIso_comparisonMap_iff_realized, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/FormalSectionsSerreOneAlternative.lean, line 142. The attribute's comment: “REDUCED, not proved: the conclusion holds exactly when every formal section is realized on one neighbourhood. Injectivity is proved outright here; the realization half is NOT proved and NOT assumed — it is the right-hand side of this equivalence. See the coverage note”.

The comparison map is an isomorphism exactly when every compatible family of sections of F / Iⁿ F on U is the comparison of a section of F over a single open V ⊆ U containing U ∩ V(I).

public theorem isIso_comparisonMap_iff_realized [IsNoetherianRing A] [F.IsCoherent] :
    IsIso (comparisonMap A I a F) ↔
      ∀ s : ToType (limit (formalSections A I a F)),
        ∃ (V : OpensNearVanishing A I a) (t : ToType ((sectionsNearVanishing A I a F).obj V)),
          ConcreteCategory.hom (comparisonAt A I a F V) t = s

Tag 0EG2, a proposition

Tag 0EG2 in the Stacks Project.

Stacks.Algebraization.isIso_comparisonMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AssociatedPointInductionComparison.lean, line 384. The attribute's comment: “the third condition of Stacks 0EIF removed, by induction on the associated points off V(I). Carried, each in its own generality and none of them this conclusion: Stacks 0EIF (SerreOneAlternativeComparison), the middle clause of Stacks 0H48 (MiddleComparisonOfShortExact), and the short exact sequence the source builds from Stacks 0BK0, 0DX3 and 0AW0 (AssociatedPointSplitting, in which no comparison map occurs). Proved here: the induction, the base case, and the descent of the measure and of conditions (1) and (2) to a submodule”.

Stacks 0EG2. Let I ⊆ 𝔞 be ideals of a Noetherian ring A and let F be a coherent module on U = Spec(A) ∖ V(𝔞). Assume

1. A is I-adically complete and has a dualizing complex, and
2. whenever x is an associated point of F outside V(I) whose closure meets V(I) outside V(𝔞), every z ∈ closure {x} ∩ V(𝔞) has dim(𝒪_{closure {x}, z}) > cd(A, I) + 1.

Then the comparison map Stacks.Algebraization.comparisonMap A I 𝔞 F, from the sections of F on arbitrarily small open neighbourhoods of U ∩ V(I) to the compatible families of sections of F / Iⁿ F on all of U, is an isomorphism.

The source's third condition, present in Stacks 0EIF, is absent here; that is the whole content of this proposition, and it is obtained by induction on the number of associated points of F off V(I) over Stacks 0EIF, the middle clause of Stacks 0H48, and the splitting the source assembles from Stacks 0BK0, 0DX3 and 0AW0.

public theorem isIso_comparisonMap [IsNoetherianRing A]
    (F : (complementZeroLocus A a : Scheme).Modules) [hFc : F.IsCoherent]
    (hF : BootstrapHypotheses A I a F)
    (hEIF : SerreOneAlternativeComparison.{u}) (h48 : MiddleComparisonOfShortExact.{u})
    (hsplit : AssociatedPointSplitting A I a) :
    IsIso (comparisonMap A I a F)

Stacks.Algebraization.isIso_comparisonMap_of_associatedPointsClosureDimensionBound, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/FormalSectionsAssociatedPointInduction.lean, line 78.

Stacks 0EG2. Let I ⊆ 𝔞 be ideals of a Noetherian ring A and let F be a coherent module on U = Spec(A) ∖ V(𝔞). Assume

1. A is I-adically complete and has a dualizing complex, and
2. whenever x is an associated point of F outside V(I) whose closure meets V(I) outside V(𝔞), every z ∈ closure {x} ∩ V(𝔞) has dim(𝒪_{closure {x}, z}) > cd(A, I) + 1.

Then the comparison map colim_V H⁰(V, F) ⟶ lim_n H⁰(U, F/IⁿF), where the colimit is over the opens V ⊆ U containing U ∩ V(I), is an isomorphism.

public theorem isIso_comparisonMap_of_associatedPointsClosureDimensionBound
    {A : Type u} [CommRing A] [IsNoetherianRing A] (I a : Ideal A) (hIa : I ≤ a)
    (hcomplete : IsAdicComplete I A)
    (hdualizing : ∃ K : DerivedCategory (ModuleCat.{u} A), Dualizing.IsDualizingComplex K)
    (F : (complementZeroLocus A a : Scheme).Modules) [F.IsCoherent]
    (hdim : AssociatedPointsClosureDimensionBound A I a F) :
    IsIso (comparisonMap A I a F)

Tag 0EIG, a lemma

Tag 0EIG in the Stacks Project.

Stacks.Algebraization.FormalSectionsII.globalToFormalSections_proj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/FormalSectionsAlgebraizationII.lean, line 252. The attribute's comment: “canonicality of the displayed arrow: its n-th component is reduction mod I^n”.

The arrow of Stacks 0EIG is canonical: its n-th component is reduction modulo Iⁿ of a global section of F on U, not an arbitrary arrow into the limit.

theorem globalToFormalSections_proj (n : ℕ) :
    globalToFormalSections A I a F ≫ limit.π (formalSections A I a F) (op n) =
      (adicProj (idealSheafNearVanishing A I a) F (op n)).app ⊤

Stacks.Algebraization.FormalSectionsII.isIso_globalToFormalSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/FormalSectionsAlgebraizationII.lean, line 312. The attribute's comment: “H^0(U,F) = lim H^0(U,F/I^nF); 0EG2 applied, its 3 hypotheses passed through”.

Stacks 0EIG. Let I ⊆ 𝔞 be ideals of a Noetherian ring A and let F be a coherent module on U = Spec(A) ∖ V(𝔞). Assume

1. A is I-adically complete and has a dualizing complex,
2. whenever x is an associated point of F outside V(I) whose closure meets V(I) outside V(𝔞), every z ∈ closure {x} ∩ V(𝔞) has dim(𝒪_{closure {x}, z}) > cd(A, I) + 1, and
3. depth(F_x) ≥ 2 for every x ∈ U whose closure meets V(I) only inside V(𝔞).

Then H⁰(U, F) ⟶ lim H⁰(U, F / Iⁿ F) is an isomorphism.

What is proved here is the content of Stacks 0EIG over Stacks 0EG2: a point of U missed by a neighbourhood V of the formal locus has its closure meeting V(I) only inside V(𝔞), so condition (3) bounds the depth of F below by 2 on all of U ∖ V, Hartogs extension for coherent modules — Stacks 0E9I — makes every restriction Γ(U, F) ⟶ Γ(V, F) an isomorphism, and the colimit therefore collapses onto its value at U.

Conditions (1) and (2) are consumed only by Stacks.Algebraization.isIso_comparisonMap, the library's Stacks 0EG2, which is applied here: they assemble into its Stacks.Algebraization.BootstrapHypotheses on the nose. The three remaining arguments are that statement's own carried hypotheses, passed through unchanged and granting nothing about Stacks 0EIG:

• Stacks.Algebraization.SerreOneAlternativeComparison grants Stacks 0EIF — the comparison map is an isomorphism for a coherent module that additionally satisfies the third condition of that lemma, the condition Stacks 0EG2 removes;
• Stacks.Algebraization.MiddleComparisonOfShortExact grants the middle clause of Stacks 0H48 — the middle comparison of a short exact sequence is an isomorphism once the outer two are;
• Stacks.Algebraization.AssociatedPointSplitting grants the short exact sequence the source assembles from Stacks 0BK0, 0DX3 and 0AW0, in which no comparison map occurs at all.

None of the three mentions the global sections Γ(U, F), so none of them is this conclusion; and since they are exactly the hypotheses the library's Stacks 0EG2 already carries, this statement adds no assumption of its own beyond conditions (1), (2) and (3).

theorem isIso_globalToFormalSections [IsNoetherianRing A] [F.IsCoherent]
    (hIa : I ≤ a) (hcomplete : IsAdicComplete I A)
    (hdualizing : ∃ K : DerivedCategory (ModuleCat.{u} A), Dualizing.IsDualizingComplex K)
    (hdim : AssociatedPointsClosureDimensionBound A I a F)
    (hdepth : DepthTwoOffFormalLocus A I a F)
    (hEIF : SerreOneAlternativeComparison.{u}) (h48 : MiddleComparisonOfShortExact.{u})
    (hsplit : AssociatedPointSplitting A I a) :
    IsIso (globalToFormalSections A I a F)

Stacks.Algebraization.FormalSectionsII.isIso_globalToFormalSections_of_depthTwoOffFormalLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/FormalSectionsGlobalAlgebraization.lean, line 75.

Stacks 0EIG. Let I ⊆ 𝔞 be ideals of a Noetherian ring A and let F be a coherent module on U = Spec(A) ∖ V(𝔞). Assume

1. A is I-adically complete and has a dualizing complex,
2. whenever x is an associated point of F outside V(I) whose closure meets V(I) outside V(𝔞), every z ∈ closure {x} ∩ V(𝔞) has dim(𝒪_{closure {x}, z}) > cd(A, I) + 1, and
3. depth(F_x) ≥ 2 for every x ∈ U whose closure meets V(I) only inside V(𝔞).

Then the arrow H⁰(U, F) ⟶ lim H⁰(U, F / Iⁿ F), whose n-th component is reduction modulo Iⁿ, is an isomorphism.

Conditions (1) and (2) make the comparison map of Stacks 0EG2 an isomorphism; condition (3) and Stacks 0E9I identify H⁰(V, F) with H⁰(U, F) for every open V ⊆ U containing U ∩ V(I).

theorem isIso_globalToFormalSections_of_depthTwoOffFormalLocus
    (A : Type u) [CommRing A] [IsNoetherianRing A] (I a : Ideal A)
    (F : (complementZeroLocus A a : Scheme).Modules) [F.IsCoherent]
    (hIa : I ≤ a) (hcomplete : IsAdicComplete I A)
    (hdualizing : ∃ K : DerivedCategory (ModuleCat.{u} A), Dualizing.IsDualizingComplex K)
    (hdim : AssociatedPointsClosureDimensionBound A I a F)
    (hdepth : DepthTwoOffFormalLocus A I a F) :
    IsIso (globalToFormalSections A I a F)

Tag 0EIH, a lemma

Tag 0EIH in the Stacks Project.

Stacks.Algebraization.mono_principalComparisonMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/PrincipalFormalLocusTagInjectivity.lean, line 219. The attribute's comment: “injectivity”.

Stacks 0EIH, the injectivity half. Let A be a Noetherian ring, let f ∈ A, let 𝔞 ⊆ A be an ideal and let M be a finite A-module. Then the map

colim_V Γ(V, M̃) ⟶ lim Γ(U, (M/fⁿM)~)

of the source, the colimit being over the opens V ⊆ U = Spec(A) ∖ V(𝔞) containing U ∩ V(f), is a monomorphism.

None of the three hypotheses of the source is needed for this half: A is not assumed f-adically complete, f is not assumed a nonzerodivisor on M, H¹_𝔞(M/fM) is not assumed finite, and f is not assumed to lie in 𝔞.

theorem mono_principalComparisonMap (A : Type u) [CommRing A] [IsNoetherianRing A] (f : A)
    (a : Ideal A) (M : ModuleCat.{u} A) [Module.Finite A M] :
    Mono (principalComparisonMap A f a M)

Stacks.Algebraization.FormalSections.isIso_formalComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/PrincipalFormalSections/Algebraization.lean, line 597.

Let A be a Noetherian ring, let f ∈ 𝔞 ⊆ A be an element of an ideal of A, and let M be a finite A-module. Assume

1. A is f-adically complete,
2. f is a nonzerodivisor on M,
3. H¹_𝔞(M/fM) is a finite A-module.

Then, with U = Spec(A) ∖ V(𝔞), the canonical map

colim_V Γ(V, M̃) ⟶ lim_n Γ(U, (M/fⁿM)~)

is an isomorphism, the colimit being over the opens V ⊆ U containing U ∩ V(f).

The map is Stacks.Algebraization.FormalSections.formalComparison: on a neighbourhood V of the formal locus it reduces a section of M̃ modulo fⁿ and extends the result back to U, which is legitimate because (M/fⁿM)~ vanishes on D(f) ⊇ U ∖ V. The quotient M/fM is written Stacks.Algebraization.FormalSections.Quot f M 1, which is M modulo the submodule fM; see Stacks.Algebraization.FormalSections.powSmul_one.

The membership f ∈ 𝔞 is carried but not consumed: the proof below uses only the other three hypotheses, so the conclusion holds for every f and every ideal 𝔞.

theorem isIso_formalComparison (A : Type u) [CommRing A] [IsNoetherianRing A] (f : A)
    (a : Ideal A) (hfa : f ∈ a) (M : ModuleCat.{u} A) [Module.Finite A (M : Type u)]
    [IsAdicComplete (Ideal.span {f}) A] (hf : IsSMulRegular (M : Type u) f)
    (hH1 : Module.Finite A
      (localCohomologyModule A a (Ideal.fg_of_isNoetherianRing a) (Quot f M 1) 1)) :
    IsIso (ModuleCat.ofHom (formalComparison A a f M))

Tag 0H49, a proposition

Tag 0H49 in the Stacks Project.

Stacks.Algebraization.isIso_comparisonMap_span_singleton_of_two_lt_closureLocalDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/PrincipalFormalLocusAlgebraization.lean, line 260.

Stacks Project, Tag 0H49. Let A be a Noetherian ring, let f ∈ 𝔞 ⊆ A and let ℱ be a coherent module on U = Spec(A) ∖ V(𝔞). Assume A is f-adically complete and has a dualizing complex, and that whenever x is an associated point of ℱ with f ∉ 𝔭_x, whose closure meets V(f) outside V(𝔞), and z ∈ closure{x} ∩ V(𝔞), the local ring of closure{x} at z has dimension greater than two. Then the comparison map

colim_V Γ(V, ℱ) ⟶ lim Γ(U, ℱ / fⁿ ℱ)

is an isomorphism, the colimit being over the opens V ⊆ U containing U ∩ V(f).

The closure of x in Spec(A) is V(𝔭_x), so "closure{x} ∩ V(f) ⊄ V(𝔞)" is the existence of a prime y ⊇ 𝔭_x with f ∈ y and 𝔞 ⊄ y, and "z ∈ closure{x} ∩ V(𝔞)" is 𝔭_x ≤ z and 𝔞 ≤ z. The dimension of 𝒪_{closure{x}, z} is the Krull dimension of the primes of A between 𝔭_x and z, which is Stacks.Algebraization.closureLocalDimension A 𝔭_x z. No hypothesis supplying the surjectivity half of Stacks 0EG2 (Stacks.Algebraization.ComparisonSurjectivity) is assumed.

The dualizing complex enters through its two consequences used by the source, universal catenarity (Stacks 0A80) and Gorenstein, hence (S₁), formal fibres (Stacks 0AWY); see the module documentation for the rest of the argument.

theorem isIso_comparisonMap_span_singleton_of_two_lt_closureLocalDimension
    (A : Type u) [CommRing A] [IsNoetherianRing A] (a : Ideal A) (f : A) (_hf : f ∈ a)
    (F : (complementZeroLocus A a : Scheme).Modules) [F.IsCoherent]
    (hcomplete : IsAdicComplete (Ideal.span {f}) A)
    (hdualizing : ∃ K : DerivedCategory (ModuleCat.{v} A), Dualizing.IsDualizingComplex K)
    (hdimension : ∀ x : (complementZeroLocus A a : Scheme),
      x ∈ Stacks.Divisors.associatedPoints F → f ∉ x.1.asIdeal →
      (∃ y : PrimeSpectrum A,
        x.1.asIdeal ≤ y.asIdeal ∧ f ∈ y.asIdeal ∧ ¬ a ≤ y.asIdeal) →
      ∀ z : PrimeSpectrum A, x.1.asIdeal ≤ z.asIdeal → a ≤ z.asIdeal →
        (2 : WithBot ℕ∞) < closureLocalDimension A x.1 z) :
    IsIso (comparisonMap A (Ideal.span {f}) a F)

Stacks.Algebraization.mono_comparisonMap_span_singleton, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/PrincipalFormalLocusDimensionCriterion.lean, line 136. The attribute's comment: “injectivity”.

Stacks 0H49, the injectivity half. For a coherent module ℱ on U = Spec(A) ∖ V(𝔞) over a Noetherian ring A and an element f ∈ A, the map

colim_V Γ(V, ℱ) ⟶ lim Γ(U, ℱ / fⁿ ℱ)

of the tag, the colimit being over the opens V ⊆ U containing U ∩ V(f), is a monomorphism.

None of the tag's hypotheses is needed: A is not assumed f-adically complete, no dualizing complex is assumed, f is not assumed to lie in 𝔞, and no bound on the local dimensions along the associated points of ℱ is assumed. This is Stacks.Algebraization.mono_comparisonMap at the principal ideal (f).

theorem mono_comparisonMap_span_singleton (A : Type u) [CommRing A] [IsNoetherianRing A]
    (a : Ideal A) (f : A) (F : (complementZeroLocus A a : Scheme).Modules) [F.IsCoherent] :
    Mono (comparisonMap A (Ideal.span {f}) a F)

Tag 0EII, a lemma

Tag 0EII in the Stacks Project.

Declarations registered for the tag:

• Stacks.Algebraization.ComplementTower.sectionsToLimit_isIso, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/FormalGeometry/PrincipalFormalLocus.lean, line 235 (StacksFrontier).

Sources

• Section 52.12, Tag 0EG1
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Algebraization.isIso_comparisonMap_first_of_middle_and_third · Stacks.Algebraization.isIso_comparisonMap_middle_of_ends · Stacks.Algebraization.isIso_comparisonMap_of_formalSectionsHypotheses · Stacks.Algebraization.isIso_comparisonMap_iff_realized · Stacks.Algebraization.isIso_comparisonMap · Stacks.Algebraization.isIso_comparisonMap_of_associatedPointsClosureDimensionBound · Stacks.Algebraization.FormalSectionsII.globalToFormalSections_proj · Stacks.Algebraization.FormalSectionsII.isIso_globalToFormalSections

Section52.13 Algebraization of formal sections, III#

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

Tag 0EG4, a proposition

Tag 0EG4 in the Stacks Project.

Stacks.Algebraization.adicLimit_allDegrees, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSectionsAlgebraization/AdicLimitTheorem.lean, line 152.

Stacks Project, Tag 0EG4. Let I ⊆ 𝔞 be ideals of a Noetherian ring A, let F be a coherent module on U = Spec(A) ∖ V(𝔞) and let s ≥ 0. Assume

1. A is I-adically complete and has a dualizing complex,
2. Stacks.Algebraization.SourceSheafDepthHypothesis: for x ∈ U ∖ V(I), depth(F_x) > s or depth(F_x) + dim(𝒪_{closure {x}, z}) > cd(A, I) + s + 1 for all z ∈ V(𝔞) ∩ closure {x},
3. Stacks.Algebraization.SourceSerreOrDimensionHypothesis: the restriction of F to U ∖ V(I) is (S_{s+1}), or the difference of the maximal and minimal values of a dimension function on V(𝔞) is at most 2.

Then the maps H^i(U, F) → lim H^i(U, F/IⁿF) are isomorphisms for i < s, and colim_V H^s(V, F) → lim H^s(U, F/IⁿF) is an isomorphism, the colimit being over the opens V ⊆ U containing U ∩ V(I).

Here H^i(V, -) is Stacks.LocalCohomology.complementOpenCohomology, the i-th right derived functor of the sections over V of 𝒪_U-modules, read over A; the first map is the comparison induced by the quotient maps F → F/IⁿF; the second is the descent of Stacks.Algebraization.nearVanishingCocone, whose component at V is reduction modulo Iⁿ on V followed by the inverse of the restriction isomorphism H^s(U, F/IⁿF) ≅ H^s(V, F/IⁿF).

theorem adicLimit_allDegrees
    (F : (complementZeroLocus A a : Scheme).Modules) [F.IsCoherent] (s : ℕ)
    (hcomplete : IsAdicComplete I A)
    (hdual : ∃ K : DerivedCategory (ModuleCat.{u} A), Dualizing.IsDualizingComplex K)
    (hdepth : SourceSheafDepthHypothesis A I a F s)
    (h3 : SourceSerreOrDimensionHypothesis A I a F s) :
    (∀ i : ℕ, i < s →
      IsIso (limit.lift (quotientSystemNearVanishing A I a F ⋙ complementOpenCohomology A a ⊤ i)
        ((complementOpenCohomology A a ⊤ i).mapCone
          (adicQuotientCone (idealSheafNearVanishing A I a) F)))) ∧
    IsIso (colimit.desc (nearVanishingCohomology A I a F s) (nearVanishingCocone A I a F s))

Stacks.Algebraization.isIso_comparisonMap_of_sourceSheafDepthHypothesis, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSectionsAlgebraization/DegreeZeroAdicLimit.lean, line 213. The attribute's comment: “the case s = 0: the first assertion is empty there and the colim/lim assertion in degree 0 is IsIso (comparisonMap A I a F), by Proposition 0EG2 as in the source. Hypotheses (1) and (2) of the source are present, (2) at s = 0 in the source's shape; hypothesis (3) is absent because 0EG2 removes it. Every s, with every conclusion, is Stacks.Algebraization.adicLimit_allDegrees in AdicLimitTheorem.lean”.

Stacks Project, Tag 0EG4 for s = 0. Let I ⊆ 𝔞 be ideals of a Noetherian ring A and let F be a coherent module on U = Spec(A) ∖ V(𝔞). Assume A is I-adically complete and has a dualizing complex, and assume hypothesis (2) of the source at s = 0. Then

colim_V H^0(V, F) ⟶ lim H^0(U, F/IⁿF)

is an isomorphism, the colimit being over the opens V ⊆ U containing U ∩ V(I); that map is Stacks.Algebraization.comparisonMap A I 𝔞 F.

This is the proposition's colim/lim assertion in degree s = 0, the first assertion being empty for s = 0. It is the case the source disposes of by citing Proposition 0EG2, and the proof is that citation: hypothesis (2) at s = 0 gives condition (2) of 0EG2 because the depth of a stalk at an associated point is zero. Hypothesis (3) of the source is absent, being the condition 0EG2 removes.

public theorem isIso_comparisonMap_of_sourceSheafDepthHypothesis [F.IsCoherent] (hIa : I ≤ a)
    (hcomplete : IsAdicComplete I A)
    (hdual : ∃ K : DerivedCategory (ModuleCat.{u} A), Dualizing.IsDualizingComplex K)
    (hdepth : SourceSheafDepthHypothesis A I a F 0) :
    IsIso (comparisonMap A I a F)

Tag 0EKM, a lemma

Tag 0EKM in the Stacks Project.

Stacks.Algebraization.HigherComplementTower.bijective_toTowerSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/ComplementFormalFunctionsHigher.lean, line 398. The attribute's comment: “with H^i(U, -) the cohomology of derived sections on U = Spec(A) ∖ V(𝔞) in the Čech model of a finite generating family of 𝔞, and the inverse limit taken as the compatible sequences of the tower of the H^i(U, (M/fⁿM)~)”.

Let A be a Noetherian ring, let f ∈ 𝔞 be an element of a finitely generated ideal of A, let M be a finite A-module and let s ≥ 0. Assume A is f-adically complete and H^k_𝔞(M) is annihilated by a power of f for k ≤ s + 1. Then with U = Spec(A) ∖ V(𝔞) the canonical map H^i(U, M̃) ⟶ lim_n H^i(U, (M/fⁿM)̃) is a bijection for every i < s.

In degree zero the source is complete by the extension argument of Stacks 0EII; in a positive degree i < s it equals H^{i+1}_𝔞(M), which is killed by a power of f because i + 1 ≤ s + 1, and a module killed by a power of f is complete. In both cases H^{i+1}(U, M̃) = H^{i+2}_𝔞(M) is killed by a power of f because i + 2 ≤ s + 1.

theorem bijective_toTowerSections {A : Type u} [CommRing A] [IsNoetherianRing A]
    {I : Ideal A} (hI : I.FG) {r : ℕ} (fam : Fin r → A)
    (hfam : Ideal.span (Set.range fam) = I) (f : A) (hf : f ∈ I) (M : ModuleCat.{u} A)
    [Module.Finite A M] [IsAdicComplete (Ideal.span {f}) A] (s : ℕ)
    (hann : ∀ k : ℕ, k ≤ s + 1 →
      ∃ c : ℕ, ∀ x : localCohomologyModule A I hI M (k : ℤ), f ^ c • x = 0)
    (i : ℕ) (hi : i < s) :
    Function.Bijective (toTowerSections fam f M (i : ℤ))

Sources

• Section 52.13, Tag 0EIJ
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Algebraization.adicLimit_allDegrees · Stacks.Algebraization.isIso_comparisonMap_of_sourceSheafDepthHypothesis · Stacks.Algebraization.HigherComplementTower.bijective_toTowerSections

Section52.14 Application to connectedness#

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

Tag 0ECR, a lemma

Tag 0ECR in the Stacks Project.

Stacks.Algebraization.isConnected_zeroLocus_diff_and_isConnected_puncturedSpectrum_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/VarbaroConnectedness.lean, line 615. The attribute's comment: “both assertions: the connectedness of Y ∖ Z for closed Z ⊆ Y with dim(Z) < min(c, d - 1) - cd(A, I), and of the punctured spectrum of A/I when cd(A, I) < min(c, d - 1)”. References: SGA 2 XIII (2.1), “more general”.

Stacks Project, Tag 0ECR (Varbaro, Theorem 1.6). Let (A, 𝔪) be a Noetherian complete local ring and I a proper ideal of A. Set X = Spec(A) and Y = V(I), and denote by

1. d the minimal dimension of an irreducible component of X (minDimIrreducibleComponent), and
2. c the minimal dimension of a closed subset Z ⊆ X such that X ∖ Z is disconnected (minDimDisconnectingClosed).

Then for Z ⊆ Y closed, Y ∖ Z is connected if dim(Z) < min(c, d - 1) - cd(A, I). In particular, the punctured spectrum of A/I is connected if cd(A, I) < min(c, d - 1).

Both minima are attained (exists_irreducibleComponent_topologicalKrullDim_eq_minDim, exists_isClosed_not_isConnected_compl_topologicalKrullDim_eq_minDim). The dimension of Z is its Krull dimension, ⊥ for Z = ∅, compared with the integer min(c, d - 1) - cd(A, I) in the extended integers. The punctured spectrum of A/I is the set of its non-maximal primes.

theorem isConnected_zeroLocus_diff_and_isConnected_puncturedSpectrum_quotient
    [IsAdicComplete (maximalIdeal A) A] (I : Ideal A) (hI : I ≠ ⊤) :
    (∀ Z : Set (PrimeSpectrum A), IsClosed Z → Z ⊆ zeroLocus (I : Set A) →
      krullDimToEInt (topologicalKrullDim Z) <
        ((min (minDimDisconnectingClosed (PrimeSpectrum A) : ℤ)
            ((minDimIrreducibleComponent (PrimeSpectrum A) : ℤ) - 1) -
          cohomologicalDimension A I I.fg_of_isNoetherianRing : ℤ) : EInt) →
      IsConnected (zeroLocus (I : Set A) \ Z)) ∧
    (cohomologicalDimension A I I.fg_of_isNoetherianRing <
        min (minDimDisconnectingClosed (PrimeSpectrum A) : ℤ)
          ((minDimIrreducibleComponent (PrimeSpectrum A) : ℤ) - 1) →
      IsConnected {p : PrimeSpectrum (A ⧸ I) | ¬ p.asIdeal.IsMaximal})

Tag 0EG5, a lemma

Tag 0EG5 in the Stacks Project.

Stacks.Algebraization.eq_empty_or_isConnected_zeroLocus_sdiff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/ConnectednessApplication.lean, line 702. The attribute's comment: “V(I) minus V(a) is empty or connected; hcmp carries 0EIF, the one hypothesis 0EG2 still has”.

Stacks Project, Tag 0EG5. Let I ⊆ 𝔞 be ideals of a Noetherian ring A. Assume

1. A is I-adically complete and has a dualizing complex K,
2. if 𝔭 is a minimal prime of A not contained in V(I) and 𝔮 ∈ V(𝔭) ∩ V(𝔞), then dim((A/𝔭)_𝔮) > cd(A, I) + 1, and
3. every nonempty open V ⊆ Spec(A) containing V(I) ∖ V(𝔞) is connected.

Then V(I) ∖ V(𝔞) is either empty or connected.

The proof replaces A by its reduction, where the inequality in (2) holds at every associated point of the structure sheaf of U = Spec(A) ∖ V(𝔞), and applies Stacks 0EG2 to that structure sheaf. A disconnection of V(I) ∖ V(𝔞) is turned into a compatible family of sections of 𝒪_U / Iⁿ 𝒪_U which is 1 on one piece and 0 on the other — the nontrivial idempotent of the source — and Stacks 0EG2 realizes it as a function on a single open neighbourhood V of V(I) ∖ V(𝔞), whose germs along that locus take the two values 1 and 0; the two opens where they are attained disconnect a neighbourhood of V(I) ∖ V(𝔞), contradicting (3).

The hypothesis hcmp carries the one input Stacks 0EG2 still needs, quantified over every Noetherian ring and every pair of ideals, because the reduction step applies Stacks 0EG2 to the reduction of A rather than to A. Its only field is Stacks 0EIF (serreOneAlternative), which is neither this conclusion nor the conclusion of Stacks 0EG2. The middle clause of Stacks 0H48, which Stacks 0EG2 also consumes, is supplied by Stacks.Algebraization.middleComparisonOfShortExact, and the short exact sequence by Stacks.Algebraization.associatedPointSplitting. Everything this adds over Stacks 0EG2 is proved here: the reduction to the reduced case, that minimal primes give condition (2) of Stacks 0EG2, the construction of the idempotent, and the passage from a realized idempotent to a disconnection of a neighbourhood.

public theorem eq_empty_or_isConnected_zeroLocus_sdiff (A : Type u) [CommRing A]
    [IsNoetherianRing A] (I a : Ideal A) (hIa : I ≤ a) [IsAdicComplete I A]
    (K : DerivedCategory (ModuleCat.{u} A)) (hK : Dualizing.IsDualizingComplex K)
    (hdim : ∀ p q : PrimeSpectrum A, p.asIdeal ∈ minimalPrimes A → ¬ I ≤ p.asIdeal →
      p.asIdeal ≤ q.asIdeal → a ≤ q.asIdeal →
      ((cohomologicalDimension A I I.fg_of_isNoetherianRing + 1 : ℤ) : EInt) <
        krullDimToEInt (ringKrullDim ((Localization.AtPrime q.asIdeal) ⧸
          p.asIdeal.map (algebraMap A (Localization.AtPrime q.asIdeal)))))
    (hconn : ∀ V : Set (PrimeSpectrum A), IsOpen V → V.Nonempty →
      PrimeSpectrum.zeroLocus (I : Set A) \ PrimeSpectrum.zeroLocus (a : Set A) ⊆ V →
      _root_.IsConnected V)
    (hcmp : ConnectednessComparisonInput.{u}) :
    PrimeSpectrum.zeroLocus (I : Set A) \ PrimeSpectrum.zeroLocus (a : Set A) = ∅ ∨
      _root_.IsConnected
        (PrimeSpectrum.zeroLocus (I : Set A) \ PrimeSpectrum.zeroLocus (a : Set A))

Stacks.Algebraization.eq_empty_or_isConnected_zeroLocus_sdiff_of_isDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/FormalLocusConnected.lean, line 89.

Stacks Project, Tag 0EG5. Let I ⊆ 𝔞 be ideals of a Noetherian ring A. Assume

1. A is I-adically complete and has a dualizing complex,
2. if 𝔭 is a minimal prime of A not contained in V(I) and 𝔮 ∈ V(𝔭) ∩ V(𝔞), then dim((A/𝔭)_𝔮) > cd(A, I) + 1, and
3. every nonempty open V ⊆ Spec(A) containing V(I) ∖ V(𝔞) is connected.

Then V(I) ∖ V(𝔞) is either empty or connected.

The proof replaces A by its reduction, where the inequality in (2) holds at every associated point of the structure sheaf of U = Spec(A) ∖ V(𝔞), and applies Stacks 0EG2 to that structure sheaf. A disconnection of V(I) ∖ V(𝔞) is turned into a compatible family of sections of 𝒪_U / Iⁿ 𝒪_U which is 1 on one piece and 0 on the other, the nontrivial idempotent of the source; Stacks 0EG2 realizes it as a function on an open neighbourhood V of V(I) ∖ V(𝔞) whose germs along that locus take the two values 1 and 0, and the two opens where they are attained disconnect a neighbourhood of V(I) ∖ V(𝔞), contradicting (3).

public theorem eq_empty_or_isConnected_zeroLocus_sdiff_of_isDualizingComplex (A : Type u)
    [CommRing A] [IsNoetherianRing A] (I a : Ideal A) (hIa : I ≤ a) [IsAdicComplete I A]
    (hdualizing : ∃ K : DerivedCategory (ModuleCat.{u} A), Dualizing.IsDualizingComplex K)
    (hdim : ∀ p q : PrimeSpectrum A, p.asIdeal ∈ minimalPrimes A → ¬ I ≤ p.asIdeal →
      p.asIdeal ≤ q.asIdeal → a ≤ q.asIdeal →
      ((cohomologicalDimension A I I.fg_of_isNoetherianRing + 1 : ℤ) : EInt) <
        krullDimToEInt (ringKrullDim ((Localization.AtPrime q.asIdeal) ⧸
          p.asIdeal.map (algebraMap A (Localization.AtPrime q.asIdeal)))))
    (hconn : ∀ V : Set (PrimeSpectrum A), IsOpen V → V.Nonempty →
      PrimeSpectrum.zeroLocus (I : Set A) \ PrimeSpectrum.zeroLocus (a : Set A) ⊆ V →
      _root_.IsConnected V) :
    PrimeSpectrum.zeroLocus (I : Set A) \ PrimeSpectrum.zeroLocus (a : Set A) = ∅ ∨
      _root_.IsConnected
        (PrimeSpectrum.zeroLocus (I : Set A) \ PrimeSpectrum.zeroLocus (a : Set A))

Tag 0EG3, a lemma

Tag 0EG3 in the Stacks Project.

Stacks.Algebraization.isConnected_zeroLocus_singleton_sdiff_of_isDomain, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/PrincipalFormalLocusConnected.lean, line 81. The attribute's comment: “the whole statement: Y minus Z is connected, at the source's hypotheses”.

Stacks Project, Tag 0EG3. Let A be a Noetherian domain which has a dualizing complex and which is complete with respect to a nonzero f ∈ A. Let f ∈ 𝔞 ⊆ A be an ideal. Assume every irreducible component of Z = V(𝔞) has codimension > 2 in X = Spec(A), that is, 2 < ht(𝔮) for every minimal prime 𝔮 of 𝔞. Then Y ∖ Z is connected, where Y = V(f).

The dualizing complex may be taken in any model of D(A). The hypothesis f ≠ 0 is the source's; the argument does not use it.

public theorem isConnected_zeroLocus_singleton_sdiff_of_isDomain (A : Type u) [CommRing A]
    [IsDomain A] [IsNoetherianRing A] [HasDerivedCategory.{w} (ModuleCat.{u} A)]
    (hdualizing : ∃ K : DerivedCategory (ModuleCat.{u} A), Dualizing.IsDualizingComplex K)
    (f : A) (_hf : f ≠ 0) [IsAdicComplete (Ideal.span {f}) A] (a : Ideal A) (hfa : f ∈ a)
    (hcodim : ∀ q ∈ a.minimalPrimes, 2 < q.height) :
    _root_.IsConnected
      (PrimeSpectrum.zeroLocus ({f} : Set A) \ PrimeSpectrum.zeroLocus (a : Set A))

Sources

• Section 52.14, Tag 0ECQ
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Algebraization.isConnected_zeroLocus_diff_and_isConnected_puncturedSpectrum_quotient · Stacks.Algebraization.eq_empty_or_isConnected_zeroLocus_sdiff · Stacks.Algebraization.eq_empty_or_isConnected_zeroLocus_sdiff_of_isDualizingComplex · Stacks.Algebraization.isConnected_zeroLocus_singleton_sdiff_of_isDomain

Section52.15 The completion functor#

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

Tag 0EKP, a lemma

Tag 0EKP in the Stacks Project.

Stacks.Algebraization.quasiAffine_sectionsComplete_implies_amplePower_sectionsComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionFullyFaithful/Basic.lean, line 358. The attribute's comment: “(1) implies (2)”.

Stacks 0EKP, (1) implies (2). On a quasi-affine scheme the structure sheaf is itself an ample invertible module, and every tensor power of it is again the structure sheaf, so section completeness on the infinitesimal neighbourhoods transports to all powers.

public theorem quasiAffine_sectionsComplete_implies_amplePower_sectionsComplete
    {X Y : Scheme.{u}} (i : Y ⟶ X) [IsClosedImmersion i] [IsNoetherian X]
    (hX : Scheme.IsQuasiAffine X)
    (h : IsInfinitesimalSectionsComplete i (SheafOfModules.unit X.ringCatSheaf)) :
    ∃ (L : X.Modules)
      (hL : AlgebraicGeometry.SheafOfModules.IsInvertible X.toRingedSpace.presheaf
        (structureSheafRing X.toRingedSpace).property L),
      letI := hL
      AlgebraicGeometry.Scheme.Modules.IsAmple X L ∧
        ∃ N : ℕ, ∀ m : ℕ, N ≤ m →
          IsInfinitesimalSectionsComplete i
            (Stacks.SheafOfModules.Invertible.tensorPower X.toRingedSpace.presheaf
              (structureSheafRing X.toRingedSpace).property L (m : ℤ))

Stacks.Algebraization.sectionsComplete_chain, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionFullyFaithful/Chain.lean, line 148.

Let X be a Noetherian scheme, let Y ⊆ X be a closed subscheme and let Y_n ⊆ X be the n-th infinitesimal neighbourhood of Y in X. Consider the conditions

1. X is quasi-affine and Γ(X, 𝒪_X) → lim Γ(Y_n, 𝒪_{Y_n}) is an isomorphism;
2. X has an ample invertible module L and Γ(X, L^{⊗ m}) → lim Γ(Y_n, L^{⊗ m}|_{Y_n}) is an isomorphism for all m ≫ 0;
3. for every finite locally free 𝒪_X-module ℰ the map Γ(X, ℰ) → lim Γ(Y_n, ℰ|_{Y_n}) is an isomorphism;
4. the completion functor Coh(𝒪_X) → Coh(X, I) is fully faithful on the full subcategory of finite locally free objects.

Then (1) ⇒ (2) ⇒ (3) ⇒ (4) and (4) ⇒ (3).

public theorem sectionsComplete_chain {X Y : Scheme.{u}} (i : Y ⟶ X) [IsClosedImmersion i]
    [IsNoetherian X] :
    (SectionsCompleteQuasiAffine i → SectionsCompleteAmplePowers i) ∧
      (SectionsCompleteAmplePowers i → SectionsCompleteFiniteLocallyFree i) ∧
      (SectionsCompleteFiniteLocallyFree i →
        CompletionFullyFaithfulOnFiniteLocallyFree X i.ker) ∧
      (CompletionFullyFaithfulOnFiniteLocallyFree X i.ker →
        SectionsCompleteFiniteLocallyFree i)

Tag 0EK2, a lemma

Tag 0EK2 in the Stacks Project.

Stacks.Algebraization.NeighbourhoodCompletion.implications_among_conditions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionFullyFaithful/NeighbourhoodCompletion.lean, line 269.

[Stacks, Tag 0EK2]. Let X be a Noetherian scheme and let Y ⊂ X be a closed subscheme with ideal sheaf ℐ ⊂ 𝒪_X. Let Y_n ⊂ X be the n-th infinitesimal neighbourhood of Y in X, and let 𝒱 be the set of open subschemes V ⊂ X containing Y, ordered by reverse inclusion. Consider the conditions

1. X is quasi-affine and colim_𝒱 Γ(V, 𝒪_V) ⟶ lim Γ(Y_n, 𝒪_{Y_n}) is an isomorphism;
2. X has an ample invertible module ℒ and colim_𝒱 Γ(V, ℒ^{⊗ m}) ⟶ lim Γ(Y_n, ℒ^{⊗ m}|_{Y_n}) is an isomorphism for all m ≫ 0;
3. for every V ∈ 𝒱 and every finite locally free 𝒪_V-module ℰ the map colim_{V' ≥ V} Γ(V', ℰ|_{V'}) ⟶ lim Γ(Y_n, ℰ|_{Y_n}) is an isomorphism;
4. the completion functor colim_𝒱 Coh(𝒪_V) ⟶ Coh(X, ℐ), ℱ ↦ ℱ^∧, is fully faithful on the full subcategory of finite locally free objects.

Then (1) ⇒ (2) ⇒ (3) ⇒ (4) and (4) ⇒ (3).

The source proves (1) ⇒ (2) from the ampleness of 𝒪_X on a quasi-affine scheme, (2) ⇒ (3) from a universally exact sequence 0 → ℰ → (ℒ^{⊗ p})^{⊕ r}|_V → (ℒ^{⊗ q})^{⊕ s}|_V, and (3) ⇒ (4) by applying (3) to the internal hom; it omits the proof of (4) ⇒ (3), which is (4) applied to the pair (𝒪_V, ℰ), read through the identification of a section of ℰ with a morphism 𝒪 ⟶ ℰ.

public theorem implications_among_conditions [IsNoetherian X] :
    (IsQuasiAffineComplete i → HasAmpleComplete i) ∧
      (HasAmpleComplete i → FiniteLocallyFreeComplete i) ∧
      (FiniteLocallyFreeComplete i → CompletionFullyFaithfulComplete i) ∧
      (CompletionFullyFaithfulComplete i → FiniteLocallyFreeComplete i)

Stacks.Algebraization.quasiAffine_neighbourhoodSectionsComplete_implies_amplePower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionFullyFaithful/Neighbourhoods.lean, line 248. The attribute's comment: “(1) implies (2)”.

Condition (1) implies condition (2). Let i : Y ⟶ X be a closed immersion into a Noetherian quasi-affine scheme such that the colimit of the sections of 𝒪_X over the open neighbourhoods of Y is the limit of its sections on the infinitesimal neighbourhoods. Then X carries an ample invertible module L for which the same holds for every tensor power L^{⊗ m} with m large enough.

public theorem quasiAffine_neighbourhoodSectionsComplete_implies_amplePower
    {X Y : Scheme.{u}} (i : Y ⟶ X) [IsClosedImmersion i] [IsNoetherian X]
    (hX : Scheme.IsQuasiAffine X)
    (h : IsNeighbourhoodSectionsComplete i (SheafOfModules.unit X.ringCatSheaf)) :
    ∃ (L : X.Modules)
      (hL : AlgebraicGeometry.SheafOfModules.IsInvertible X.toRingedSpace.presheaf
        (structureSheafRing X.toRingedSpace).property L),
      letI := hL
      AlgebraicGeometry.Scheme.Modules.IsAmple X L ∧
        ∃ N : ℕ, ∀ m : ℕ, N ≤ m →
          IsNeighbourhoodSectionsComplete i
            (Stacks.SheafOfModules.Invertible.tensorPower X.toRingedSpace.presheaf
              (structureSheafRing X.toRingedSpace).property L (m : ℤ))

Tag 0EIQ, a lemma

Tag 0EIQ in the Stacks Project.

Stacks.Coherent.coherentAdicToPro_fullyFaithful, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CoherentAdicPro.lean, line 1144.

A coherent adic system has exactly the morphisms of its associated pro-quasi-coherent object.

public theorem coherentAdicToPro_fullyFaithful
    (X : Scheme.{u}) (I : X.IdealSheafData) :
    Nonempty (coherentAdicToPro X I).FullyFaithful

Tag 0EKQ, a lemma

Tag 0EKQ in the Stacks Project.

Stacks.Algebraization.completionFullyFaithful_of_associatedPrimes_of_depth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionFullyFaithful/DimensionDepthCriterion.lean, line 256.

Stacks 0EKQ. Let I ⊆ 𝔞 be ideals of a Noetherian ring A and let U = Spec(A) ∖ V(𝔞). Assume

1. A is I-adically complete and has a dualizing complex,
2. for every associated prime 𝔭 of A with 𝔭 ∉ V(I) and V(𝔭) ∩ V(I) ⊄ V(𝔞), and every 𝔮 ∈ V(𝔭) ∩ V(𝔞), one has dim((A/𝔭)_𝔮) > cd(A, I) + 1,
3. for every prime 𝔭 with 𝔭 ∉ V(I) and V(𝔭) ∩ V(I) ⊆ V(𝔞), one has depth(A_𝔭) ≥ 2.

Then the completion functor Coh(𝒪_U) ⟶ Coh(U, I𝒪_U), ℱ ↦ ℱ^∧, is fully faithful on the full subcategory of finite locally free objects.

The dimension dim((A/𝔭)_𝔮) is written as the Krull dimension of A_𝔮 / 𝔭 A_𝔮, which is the same ring.

theorem completionFullyFaithful_of_associatedPrimes_of_depth
    (A : Type u) [CommRing A] [IsNoetherianRing A] (I a : Ideal A) (hIa : I ≤ a)
    (hcomplete : IsAdicComplete I A)
    (hdualizing : ∃ K : DerivedCategory (ModuleCat.{u} A), Dualizing.IsDualizingComplex K)
    (hdim : ∀ p : PrimeSpectrum A, p.asIdeal ∈ associatedPrimes A A → ¬ I ≤ p.asIdeal →
      ¬ (PrimeSpectrum.zeroLocus (p.asIdeal : Set A) ∩ PrimeSpectrum.zeroLocus (I : Set A) ⊆
        PrimeSpectrum.zeroLocus (a : Set A)) →
      ∀ q ∈ PrimeSpectrum.zeroLocus (p.asIdeal : Set A) ∩ PrimeSpectrum.zeroLocus (a : Set A),
        ((cohomologicalDimension A I I.fg_of_isNoetherianRing + 1 : ℤ) : EInt) <
          krullDimToEInt (ringKrullDim ((Localization.AtPrime q.asIdeal) ⧸
            p.asIdeal.map (algebraMap A (Localization.AtPrime q.asIdeal)))))
    (hdepth : ∀ p : PrimeSpectrum A, ¬ I ≤ p.asIdeal →
      PrimeSpectrum.zeroLocus (p.asIdeal : Set A) ∩ PrimeSpectrum.zeroLocus (I : Set A) ⊆
        PrimeSpectrum.zeroLocus (a : Set A) →
      (2 : ℕ∞) ≤ Module.depth (Localization.AtPrime p.asIdeal)
        (maximalIdeal (Localization.AtPrime p.asIdeal)) (Localization.AtPrime p.asIdeal)) :
    CompletionFullyFaithfulOnFiniteLocallyFree (complementZeroLocus A a : Scheme)
      (idealSheafNearVanishing A I a)

Stacks.Algebraization.completionFullyFaithfulOnFiniteLocallyFree_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionFullyFaithful/InternalHomCriterion.lean, line 170. The attribute's comment: “REDUCED, not proved: full faithfulness on the finite locally free objects holds exactly when the formal-functions comparison is an isomorphism for the internal homs. That half is Stacks 0EIG, which the library has at Stacks 0EG2's hypotheses and for another spelling of the comparison; it is neither proved nor assumed here, being one side of this equivalence. Conditions (1)-(3) of the tag are not consumed”.

Stacks 0EKQ, reduced to the theorem on formal functions in degree zero. For ideals I ⊆ 𝔞 of a Noetherian ring A and U = Spec(A) ∖ V(𝔞), completion along I𝒪_U is fully faithful on the finite locally free coherent sheaves on U exactly when Γ(U, ℋ) ⟶ lim_n Γ(U, ℋ / Iⁿ ℋ) is an isomorphism for every ℋ = SheafHom(ℱ, 𝒢).

public theorem completionFullyFaithfulOnFiniteLocallyFree_iff
    (A : Type u) [CommRing A] [IsNoetherianRing A] (I a : Ideal A) :
    CompletionFullyFaithfulOnFiniteLocallyFree (complementZeroLocus A a : Scheme)
        (idealSheafNearVanishing A I a) ↔
      ∀ P Q : AlgebraicGeometry.SheafOfModules.CoherentModules
          (complementZeroLocus A a : Scheme).ringCatSheaf,
        AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} P.obj →
        AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} Q.obj →
        IsIso (globalSectionsToLimit (idealSheafNearVanishing A I a)
          (internalHomCoherent (complementZeroLocus A a : Scheme) P Q))

Tag 0EKS, a lemma

Tag 0EKS in the Stacks Project.

Stacks.Algebraization.completionFullyFaithful_of_annihilated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionFullyFaithful/AnnihilatedCriterion.lean, line 91.

Let A be a Noetherian ring, let f ∈ 𝔞 ⊆ A and let U = Spec(A) ∖ V(𝔞). If A is f-adically complete and H¹_𝔞(A) and H²_𝔞(A) are annihilated by powers of f, then the completion functor Coh(𝒪_U) ⟶ Coh(U, (f)𝒪_U), ℱ ↦ ℱ^∧, is fully faithful on the full subcategory of finite locally free objects.

public theorem completionFullyFaithful_of_annihilated (hf : f ∈ a)
    (hcomplete : IsAdicComplete (Ideal.span {f}) A)
    (h1 : ∃ n, ∀ x : localCohomologyModule A a (Ideal.fg_of_isNoetherianRing a)
      (ModuleCat.of A A) 1, f ^ n • x = 0)
    (h2 : ∃ n, ∀ x : localCohomologyModule A a (Ideal.fg_of_isNoetherianRing a)
      (ModuleCat.of A A) 2, f ^ n • x = 0) :
    CompletionFullyFaithfulOnFiniteLocallyFree (complementZeroLocus A a : Scheme)
      (complementPrincipalIdealSheaf A a f)

Stacks.Algebraization.completionFullyFaithfulOnFiniteLocallyFree_of_isAdicComplete_of_annihilated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionFullyFaithful/CompleteCriteria.lean, line 78.

[Stacks, Tag 0EKS]. Let A be a Noetherian ring, let f ∈ 𝔞 ⊆ A and let U = Spec(A) ∖ V(𝔞). If A is f-adically complete and H¹_𝔞(A) and H²_𝔞(A) are annihilated by a power of f, then the completion functor Coh(𝒪_U) ⟶ Coh(U, (f)𝒪_U) is fully faithful on the finite locally free objects.

The ideal sheaf (f)𝒪_U is complementPrincipalIdealSheaf A 𝔞 f, and full faithfulness on the finite locally free objects is CompletionFullyFaithfulOnFiniteLocallyFree. The proof is completionFullyFaithful_of_isAdicComplete_of_annihilated, Stacks 0EII followed by the chain (1) ⇒ (4) of Stacks 0EKP, with that chain supplied by completionFullyFaithfulOnFiniteLocallyFree_of_bijective_sectionsToLimit.

public theorem completionFullyFaithfulOnFiniteLocallyFree_of_isAdicComplete_of_annihilated
    (A : Type u) [CommRing A] [IsNoetherianRing A] (a : Ideal A) (f : A) (hf : f ∈ a)
    (hcomplete : IsAdicComplete (Ideal.span {f}) A)
    (h1 : ∃ n, ∀ x : localCohomologyModule A a (Ideal.fg_of_isNoetherianRing a)
      (ModuleCat.of A A) 1, f ^ n • x = 0)
    (h2 : ∃ n, ∀ x : localCohomologyModule A a (Ideal.fg_of_isNoetherianRing a)
      (ModuleCat.of A A) 2, f ^ n • x = 0) :
    CompletionFullyFaithfulOnFiniteLocallyFree (complementZeroLocus A a : Scheme)
      (complementPrincipalIdealSheaf A a f)

Tag 0EKT, a lemma

Tag 0EKT in the Stacks Project.

Stacks.Algebraization.completionFullyFaithfulOnFiniteLocallyFree_of_isAdicComplete_of_depth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionFullyFaithful/CompleteCriteria.lean, line 108.

[Stacks, Tag 0EKT]. Let A be a Noetherian ring, let f ∈ 𝔞 ⊆ A and let U = Spec(A) ∖ V(𝔞). Assume

1. A has a dualizing complex and is complete with respect to f, and
2. depth(A_𝔭) + dim((A/𝔭)_𝔮) > 2 for every prime 𝔭 ⊆ A with f ∉ 𝔭 and every 𝔮 ∈ V(𝔭) ∩ V(𝔞).

Then the completion functor Coh(𝒪_U) ⟶ Coh(U, (f)𝒪_U) is fully faithful on the finite locally free objects.

Hypothesis (1) is hdual together with hcomplete. In hypothesis (2), 𝔮 ∈ V(𝔭) ∩ V(𝔞) is 𝔞 ≤ 𝔮 and 𝔭 ≤ 𝔮, (A/𝔭)_𝔮 is A_𝔮 / 𝔭A_𝔮, and the inequality is read in the extended integers through enatToEInt and krullDimToEInt, as in completionFullyFaithful_of_isAdicComplete_of_depth. The proof is that theorem — Faltings' annihilator theorem, Stacks 0EFC, followed by Stacks 0EKS — with the chain (1) ⇒ (4) of Stacks 0EKP supplied by completionFullyFaithfulOnFiniteLocallyFree_of_bijective_sectionsToLimit.

public theorem completionFullyFaithfulOnFiniteLocallyFree_of_isAdicComplete_of_depth
    (A : Type u) [CommRing A] [IsNoetherianRing A] (a : Ideal A) (f : A) (hf : f ∈ a)
    (hdual : ∃ omega : DerivedCategory (ModuleCat.{u} A), Dualizing.IsDualizingComplex omega)
    (hcomplete : IsAdicComplete (Ideal.span {f}) A)
    (hdepth : ∀ p q : PrimeSpectrum A, f ∉ p.asIdeal → a ≤ q.asIdeal →
      p.asIdeal ≤ q.asIdeal →
      enatToEInt
          (Module.depth (Localization.AtPrime p.asIdeal)
            (maximalIdeal (Localization.AtPrime p.asIdeal))
            (LocalizedModule p.asIdeal.primeCompl A)) +
        krullDimToEInt
          (ringKrullDim ((Localization.AtPrime q.asIdeal) ⧸
            p.asIdeal.map (algebraMap A (Localization.AtPrime q.asIdeal)))) > ((2 : ℤ) : EInt)) :
    CompletionFullyFaithfulOnFiniteLocallyFree (complementZeroLocus A a : Scheme)
      (complementPrincipalIdealSheaf A a f)

Stacks.Algebraization.completionFullyFaithful_of_depth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionFullyFaithful/DepthCriterion.lean, line 206.

Stacks 0EKT. Let A be a Noetherian ring, let f ∈ 𝔞 ⊆ A and let U = Spec(A) ∖ V(𝔞). If A has a dualizing complex and is f-adically complete, and if depth(A_𝔭) + dim((A/𝔭)_𝔮) > 2 for every prime 𝔭 with f ∉ 𝔭 and every 𝔮 ∈ V(𝔭) ∩ V(𝔞), then the completion functor Coh(𝒪_U) ⟶ Coh(U, (f)𝒪_U) is fully faithful on the full subcategory of finite locally free objects.

public theorem completionFullyFaithful_of_depth (A : Type u) [CommRing A] [IsNoetherianRing A]
    (a : Ideal A) (f : A) (hf : f ∈ a)
    (omega : DerivedCategory (ModuleCat.{u} A))
    (homega : Dualizing.IsDualizingComplex (A := A) (K := omega))
    (hcomplete : IsAdicComplete (Ideal.span {f}) A)
    (hdepth : ∀ p q : PrimeSpectrum A, f ∉ p.asIdeal → a ≤ q.asIdeal →
      p.asIdeal ≤ q.asIdeal →
      enatToEInt
          (Module.depth (Localization.AtPrime p.asIdeal)
            (maximalIdeal (Localization.AtPrime p.asIdeal))
            (LocalizedModule p.asIdeal.primeCompl A)) +
        krullDimToEInt
          (ringKrullDim ((Localization.AtPrime q.asIdeal) ⧸
            p.asIdeal.map (algebraMap A (Localization.AtPrime q.asIdeal)))) > ((2 : ℤ) : EInt)) :
    CompletionFullyFaithfulOnFiniteLocallyFree (complementZeroLocus A a : Scheme)
      (complementPrincipalIdealSheaf A a f)

Tag 0EKU, a lemma

Tag 0EKU in the Stacks Project.

Stacks.Algebraization.completionFullyFaithful_finiteLocallyFree_on, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionFunctor/NeighbourhoodHomsOnBijective.lean, line 120.

Stacks 0EKU. Let I ⊆ 𝔞 ⊆ A be ideals of a Noetherian ring A, put U = Spec(A) ∖ V(𝔞) and let 𝒱 be the set of open subschemes of U containing U ∩ V(I), ordered by reverse inclusion. Assume

1. A is I-adically complete and has a dualizing complex, and
2. for every associated prime 𝔭 of A with I ⊄ 𝔭 and V(𝔭) ∩ V(I) ⊄ V(𝔞), and every 𝔮 ∈ V(𝔭) ∩ V(𝔞), we have dim((A/𝔭)_𝔮) > cd(A, I) + 1.

Then the completion functor colim_𝒱 Coh(𝒪_V) ⟶ Coh(U, I𝒪_U) is fully faithful on the full subcategory of finite locally free objects: for every V ∈ 𝒱 and all finite locally free coherent 𝒪_V-modules G, F, the map colim_{V' ≥ V} Hom_{V'}(G|_{V'}, F|_{V'}) ⟶ Hom_{Coh(V, I𝒪_V)}(G^∧, F^∧) is bijective.

Two objects of the colimit category given on members V₁, V₂ of 𝒱 are compared on V₁ ∩ V₂ ∈ 𝒱, so "for every V" is full faithfulness. The target Coh(V, I𝒪_V) is Coh(U, I𝒪_U) on morphisms by Stacks.Algebraization.bijective_restrictCompletionHom. The source's condition (2) on the associated primes of A gives condition (2) of Stacks 0EIV for a finite locally free F, whose associated points are associated points of V (Stacks.Algebraization.associatedPointsClosureDimensionBoundOn_of_isFiniteLocallyFree); the finite local freeness of G is not needed.

theorem completionFullyFaithful_finiteLocallyFree_on (hIa : I ≤ a)
    (hcomplete : IsAdicComplete I A)
    (hdualizing : ∃ K : DerivedCategory (ModuleCat.{u} A), Dualizing.IsDualizingComplex K)
    (hdim : ∀ p : PrimeSpectrum A, IsAssociatedPrimeStacks A A p.asIdeal →
      ¬ I ≤ p.asIdeal →
      (∃ y : PrimeSpectrum A, p.asIdeal ≤ y.asIdeal ∧ I ≤ y.asIdeal ∧ ¬ a ≤ y.asIdeal) →
      ∀ z : PrimeSpectrum A, p.asIdeal ≤ z.asIdeal → a ≤ z.asIdeal →
        ((cohomologicalDimension A I I.fg_of_isNoetherianRing + 1 : ℤ) : EInt) <
          krullDimToEInt (closureLocalDimension A p z))
    (V : OpensNearVanishing A I a)
    (G F : AlgebraicGeometry.SheafOfModules.CoherentModules V.openSet.toScheme.ringCatSheaf)
    (_hG : Scheme.Modules.IsFiniteLocallyFree G.obj)
    (hF : Scheme.Modules.IsFiniteLocallyFree F.obj) :
    Function.Bijective (nbhdHomComparisonOn V G F)

Tag 0EKV, a lemma

Tag 0EKV in the Stacks Project.

Stacks.Algebraization.completionFullyFaithfulComplete_principal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionFullyFaithful/PrincipalFullyFaithful.lean, line 189.

[Stacks, Tag 0EKV]. Let A be a Noetherian ring, let f ∈ 𝔞 ⊆ A, put U = Spec(A) ∖ V(𝔞) and let 𝒱 be the open subschemes of U containing U ∩ V(f), ordered by reverse inclusion. Assume

1. A is complete with respect to the f-adic topology,
2. f is a nonzerodivisor, and
3. H¹_𝔞(A/fA) is a finite A-module.

Then the completion functor colim_𝒱 Coh(𝒪_V) ⟶ Coh(U, f𝒪_U), ℱ ↦ ℱ^∧, is fully faithful on the full subcategory of finite locally free objects.

An object of colim_𝒱 Coh(𝒪_V) is a coherent module on some V ∈ 𝒱, and a morphism between two of them is an element of colim_{W ⊆ V} Hom_{𝒪_W}(𝒢|_W, ℱ|_W); so the conclusion is Stacks.Algebraization.NeighbourhoodCompletion.CompletionFullyFaithfulComplete, which quantifies over every V ∈ 𝒱 and all finite locally free 𝒪_V-modules 𝒢, ℱ, and asserts that colim_{W ⊆ V} Hom_{𝒪_W}(𝒢|_W, ℱ|_W) ⟶ lim_n Hom_{𝒪_{Y_n}}(𝒢|_{Y_n}, ℱ|_{Y_n}) is bijective. The quantifier here is the tag's own — an arbitrary member V of 𝒱, not the single member V = U — which matters because a finite locally free module on a small V need not extend to U. That is full faithfulness: an object of Coh(U, f𝒪_U) is an inverse system of coherent modules, 𝒢^∧ is the system (𝒢|_{Y_n}) of restrictions to the infinitesimal neighbourhoods of U ∩ V(f), and a morphism 𝒢^∧ ⟶ ℱ^∧ is a compatible family of morphisms of the restrictions.

The source's proof is two citations: by [Stacks, Tag 0EK2] it suffices that colim_𝒱 Γ(V, 𝒪_V) = lim_n Γ(U, 𝒪_U / fⁿ 𝒪_U), which is [Stacks, Tag 0EIH] at the module A. Both are available: the equality is Stacks.Algebraization.isQuasiAffineComplete_principal, condition (1) of [Stacks, Tag 0EK2], and the chain (1) ⇒ (2) ⇒ (3) ⇒ (4) is Stacks.Algebraization.NeighbourhoodCompletion.implications_among_conditions. No step of the argument needs the pair 𝒢, ℱ to extend from V to U: the implication (2) ⇒ (3) embeds a finite locally free module on V into a finite direct sum of restrictions to V of high twists of the ample module 𝒪_U, which is what carries the comparison from U down to V.

public theorem completionFullyFaithfulComplete_principal (hf : f ∈ a)
    [IsAdicComplete (Ideal.span {f}) A] (hnzd : f ∈ nonZeroDivisors A)
    (hH1 : Module.Finite A
      (localCohomologyModule A a (Ideal.fg_of_isNoetherianRing a)
        (Quot f (ModuleCat.of A A) 1) 1)) :
    NeighbourhoodCompletion.CompletionFullyFaithfulComplete (principalFormalLocusι A a f)

Tag 0EIV, a lemma

Tag 0EIV in the Stacks Project.

Stacks.Algebraization.NeighbourhoodHoms.sectionsNearVanishing_internalHomNear, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionFunctor/NeighbourhoodHoms.lean, line 402. The attribute's comment: “at the member V = U: the source is the colimit over the whole family”.

The source of the comparison of Stacks 0EIV is the colimit of the morphisms of the restrictions. A section of the internal hom SheafHom(𝒢, ℱ) over an open neighbourhood V of the formal locus is, on the nose, a morphism 𝒢|_V ⟶ ℱ|_V of modules on the site of opens below V. So the source of nbhdHomComparison is colim_{V ∈ 𝒱} Hom_V(𝒢|_V, ℱ|_V).

public theorem sectionsNearVanishing_internalHomNear
    (V : OpensNearVanishing A I a) :
    ToType ((sectionsNearVanishing A I a (internalHomNear A a G F).obj).obj V) =
      ((_root_.restrFun (complementZeroLocus A a : Scheme).sheaf.obj V.openSet).obj
          G.obj.val ⟶
        (_root_.restrFun (complementZeroLocus A a : Scheme).sheaf.obj V.openSet).obj
          F.obj.val)

Stacks.Algebraization.NeighbourhoodHoms.nbhdHomComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionFunctor/NeighbourhoodHoms.lean, line 422. The attribute's comment: “at V = U: the canonical map from germs of morphisms to the completions”.

The map of Stacks 0EIV. The canonical map from the morphisms 𝒢|_{V'} ⟶ ℱ|_{V'} defined on arbitrarily small open neighbourhoods V' of the formal locus U ∩ V(I) to the morphisms of the completions 𝒢^∧ ⟶ ℱ^∧ in Coh(U, I𝒪_U).

It is the composite of three canonical maps: the comparison of Stacks 0EG2 for the internal hom H = SheafHom(𝒢, ℱ), which lands in the compatible families of sections of H / Iⁿ H on U; the identification of that limit with the limit of the global sections of the completion of H, which is adicCompletionLimitIso on the tower and sectionsAbLimitIso on sections; and the identification of Stacks 0882 of the latter with the morphisms of the completions.

public def nbhdHomComparison :
    ToType (colimit (C := Ab.{u})
        (sectionsNearVanishing A I a (internalHomNear A a G F).obj)) →
      ((completionFunctor (complementZeroLocus A a : Scheme)
          (idealSheafNearVanishing A I a)).obj G ⟶
        (completionFunctor (complementZeroLocus A a : Scheme)
          (idealSheafNearVanishing A I a)).obj F)

Stacks.Algebraization.nbhdHomComparisonOn_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionFunctor/NeighbourhoodHomsOnBijective.lean, line 89.

Stacks 0EIV. Let I ⊆ 𝔞 be ideals of a Noetherian ring A, put U = Spec(A) ∖ V(𝔞) and let 𝒱 be the set of open subschemes of U containing U ∩ V(I), ordered by reverse inclusion. Let G, F be coherent 𝒪_V-modules for some V ∈ 𝒱. The map colim_{V' ≥ V} Hom_{V'}(G|_{V'}, F|_{V'}) ⟶ Hom_{Coh(V, I𝒪_V)}(G^∧, F^∧) is bijective if

1. A is I-adically complete and has a dualizing complex, and
2. whenever x is an associated point of F outside V(I) whose closure meets V(I) outside V(𝔞), every z ∈ closure {x} ∩ V(𝔞) has dim(𝒪_{closure {x}, z}) > cd(A, I) + 1.

The target is the category of coherent adic systems on V along I 𝒪_V; restriction from U to V identifies the morphisms of completions there with those in Coh(U, I𝒪_U) (Stacks.Algebraization.bijective_restrictCompletionHom), the terms being supported in U ∩ V(I) ⊆ V.

theorem nbhdHomComparisonOn_bijective (hIa : I ≤ a) (hcomplete : IsAdicComplete I A)
    (hdualizing : ∃ K : DerivedCategory (ModuleCat.{u} A), Dualizing.IsDualizingComplex K)
    (V : OpensNearVanishing A I a)
    (G F : AlgebraicGeometry.SheafOfModules.CoherentModules V.openSet.toScheme.ringCatSheaf)
    (hdim : AssociatedPointsClosureDimensionBoundOn V F.obj) :
    Function.Bijective (nbhdHomComparisonOn V G F)

Sources

• Section 52.15, Tag 0EKN
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Algebraization.quasiAffine_sectionsComplete_implies_amplePower_sectionsComplete · Stacks.Algebraization.sectionsComplete_chain · Stacks.Algebraization.NeighbourhoodCompletion.implications_among_conditions · Stacks.Algebraization.quasiAffine_neighbourhoodSectionsComplete_implies_amplePower · Stacks.Coherent.coherentAdicToPro_fullyFaithful · Stacks.Algebraization.completionFullyFaithful_of_associatedPrimes_of_depth · Stacks.Algebraization.completionFullyFaithfulOnFiniteLocallyFree_iff · Stacks.Algebraization.completionFullyFaithful_of_annihilated

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.